Do we do "the right thing" for these test cases?

[braxtonhall]

And if not, why?

• fold.vpr
• AVLTree.iterative.vpr

Edit: Yes and no. fold.vpr starts to fail but we believe that this behaviour is now correct.

• [ ] Talk about this in the testing section. Also maybe limitations because the user may now just have less information.

[jyoo980]

• fold.vpr We obtain the same result (assertion might fail) when we run it on vanilla Viper and the our plugin-enabled build

[jyoo980]

Looks like there might be an issue with invariant expansions with while loops. The following is the result of running our plugin (post expansion)

field root1: Ref

field key: Int

field left: Ref

field right: Ref

field parent: Ref

field leftDown: Bool

field root: Ref

predicate valid1(this: Ref) {
  acc(this.root1, write) && ((this.root1 != null ==> acc(valid(this.root1), write)) && ((this.root1 != null ==> acc(this.root1.parent, write)) && ((this.root1 != null ==> this.root1.parent == null) && ((this.root1 != null ==> acc(this.root1.root, 1 / 2)) && (this.root1 != null ==> this.root1.root == this.root1)))))
}

predicate valid(this: Ref) {
  acc(validRest(this), write) && (acc(leftValid(this), write) && acc(rightValid(this), write))
}

predicate validRest(this: Ref) {
  acc(this.key, write) && (acc(this.root, 3 / 10) && (acc(this.left, 3 / 4) && (acc(this.right, 3 / 4) && (acc(this.leftDown, write) && (this.right != this.left || this.right == null)))))
}

predicate rightValid(this: Ref) {
  acc(this.right, 1 / 4) && (acc(this.root, 1 / 10) && ((this.right != null ==> acc(valid(this.right), write)) && ((this.right != null ==> acc(this.right.parent, write)) && ((this.right != null ==> this.right.parent == this) && ((this.right != null ==> acc(this.right.root, 1 / 2)) && (this.right != null ==> this.right.root == this.root))))))
}

predicate leftValid(this: Ref) {
  acc(this.left, 1 / 4) && (acc(this.root, 1 / 10) && ((this.left != null ==> acc(valid(this.left), write)) && ((this.left != null ==> acc(this.left.parent, write)) && ((this.left != null ==> this.left.parent == this) && ((this.left != null ==> acc(this.left.root, 1 / 2)) && (this.left != null ==> this.left.root == this.root))))))
}

predicate leftOpen(this: Ref) {
  acc(this.left, 1 / 4) && (acc(this.root, 1 / 10) && ((this.left != null ==> acc(this.left.parent, 1 / 2)) && (this.left != null ==> this.left.parent == this)))
}

predicate rightOpen(this: Ref) {
  acc(this.right, 1 / 4) && (acc(this.root, 1 / 10) && ((this.right != null ==> acc(this.right.parent, 1 / 2)) && (this.right != null ==> this.right.parent == this)))
}

predicate udParentValid(this: Ref) {
  acc(this.parent, 1 / 2) && (acc(this.root, 1 / 10) && ((this.parent != null ==> acc(udValid(this.parent), write)) && ((this.parent != null ==> acc(this.parent.leftDown, 1 / 2)) && ((this.parent != null ==> acc(this.parent.left, 1 / 2)) && ((this.parent != null ==> this.parent.leftDown == (this.parent.left == this)) && ((this.parent != null ==> acc(this.parent.right, 1 / 2)) && ((this.parent != null ==> !this.parent.leftDown == (this.parent.right == this)) && ((this.parent != null ==> acc(this.parent.root, 1 / 2)) && ((this.parent != null ==> this.root == this.parent.root) && (this.parent == null ==> this.root == this))))))))))
}

predicate udValid(this: Ref) {
  acc(this.key, write) && (acc(this.leftDown, 1 / 2) && (acc(this.left, 1 / 4) && (acc(this.right, 1 / 4) && (acc(this.root, 1 / 5) && ((this.leftDown ==> acc(rightValid(this), write)) && ((this.leftDown ==> acc(leftOpen(this), write)) && (((this.leftDown ==> false) ==> acc(leftValid(this), write)) && (((this.leftDown ==> false) ==> acc(rightOpen(this), write)) && acc(udParentValid(this), write)))))))))
}

method init(this: Ref)
  requires acc(this.root1, write)
  ensures acc(this.root1, write) && ((this.root1 != null ==> acc(valid(this.root1), write)) && ((this.root1 != null ==> acc(this.root1.parent, write)) && ((this.root1 != null ==> this.root1.parent == null) && ((this.root1 != null ==> acc(this.root1.root, write)) && (this.root1 != null ==> this.root1.root == this.root1)))))
{
  this.root1 := null
}

method has(this: Ref, k: Int) returns (b: Bool)
  requires acc(this.root1, write) && ((this.root1 != null ==> acc(valid(this.root1), write)) && ((this.root1 != null ==> acc(this.root1.parent, write)) && ((this.root1 != null ==> this.root1.parent == null) && ((this.root1 != null ==> acc(this.root1.root, write)) && (this.root1 != null ==> this.root1.root == this.root1)))))
  ensures acc(this.root1, write) && ((this.root1 != null ==> acc(valid(this.root1), write)) && ((this.root1 != null ==> acc(this.root1.parent, write)) && ((this.root1 != null ==> this.root1.parent == null) && ((this.root1 != null ==> acc(this.root1.root, write)) && (this.root1 != null ==> this.root1.root == this.root1)))))
{
  var n: Ref
  var end: Bool
  var p: Ref
  var q: Ref
  var r: Ref
  if (this.root1 == null) {
    b := false
  } else {
    n := this.root1
    b := false
    end := false
    fold acc(udParentValid(n), write)
    while (!end)
      invariant acc(this.root1, write)
      invariant this.root1 != null && acc(this.root1.parent, 1 / 2)
      invariant n != null
      invariant acc(valid(n), write)
      invariant acc(n.root, 4 / 10)
      invariant acc(udParentValid(n), write)
      invariant (unfolding acc(valid(n), write) in n.root == this.root1)
      invariant this.root1 != null 
    {
      unfold acc(valid(n), write)
      if (n.key == k) {
        b := true
        fold acc(valid(n), write)
        end := true
      } elseif (n.key < k) {
        if (n.left == null) {
          end := true
          fold acc(valid(n), write)
        } else {
          p := n
          unfold acc(leftValid(p), write)
          n := p.left
          p.leftDown := true
          fold acc(udValid(p), write)
          fold acc(udParentValid(n), write)
        }
      } elseif (n.right == null) {
        end := true
        fold acc(valid(n), write)
      } else {
        q := n
        unfold acc(rightValid(q), write)
        n := q.right
        q.leftDown := false
        fold acc(udValid(q), write)
        fold acc(udParentValid(n), write)
      }
    }
    end := false
    while (!end)
      invariant acc(this.root1, write)
      invariant this.root1 != null && acc(this.root1.parent, 1 / 2)
      invariant n != null
      invariant acc(valid(n), write)
      invariant acc(udParentValid(n), write)
      invariant acc(n.root, 4 / 10)
      invariant (unfolding acc(valid(n), write) in n.root == this.root1)
      invariant this.root1 != null
      invariant end ==> (unfolding acc(udParentValid(n), write) in n.parent == null) 
    {
      unfold acc(udParentValid(n), write)
      r := n.parent
      if (r == null) {
        end := true
        fold acc(udParentValid(n), write)
      } else {
        unfold acc(udValid(r), write)
        if (r.left == n) {
          fold acc(leftValid(r), write)
        } else {
          fold acc(rightValid(r), write)
        }
        fold acc(valid(r), write)
        n := r
      }
    }
    unfold acc(udParentValid(n), write)
  }
}

method init_2(this: Ref, k: Int)
  requires acc(this.key, write)
  requires acc(this.left, write)
  requires acc(this.right, write)
  requires acc(this.leftDown, write)
  requires acc(this.root, write)
  ensures acc(valid(this), write)
{
  this.left := null
  this.right := null
  this.key := k
  fold acc(leftValid(this), write)
  fold acc(rightValid(this), write)
  fold acc(valid(this), write)
}

The lack of expansion in the body of the while is likely due to this line of code where we don't look into the body.

I'm not sure why invariant rewriting isn't happening though. Any ideas @ionathanch ?

[jyoo980]

Ah, it's because some of recursive predicates,

[udValid, leftValid, rightValid, udParentValid, valid] are mutually recursive predicates and will not be inlined.

[ionathanch]

(Gotta make that warning message print out in big bold red letters or smth) The file's rly big I'm feeling rly lazy rn is there anything I need 2 look at

[jyoo980]

It looks like the first if inside the while is complaining about access

[ionathanch]

Looks like the problem is with nested predicates inside of recursive predicates. Here's a minimal example:

field f: Int

predicate F(this: Ref) {
  acc(this.f)
}

predicate loop(this: Ref) {
  loop(this) && F(this)
}

method nestedPred(this: Ref)
  requires loop(this)
{
  unfold loop(this)
  unfold F(this)
  this.f := 0
}

The method nestedPred after inlining becomes this:

method nestedPred(this: Ref)
  requires loop(this)
{
  unfold loop(this)
  this.f := 0
}

So the problem is that F was removed because we remove all unfolds of non-recursive predicates, but it shouldn't have been, since loop was never inlined to allow that access to its F inside. I think the solution would be to exclude all predicates referred to by (mutually) recursive predicates from the list of ones not unfold/fold?

[ionathanch]

Apparently propagating access values like in #19 is not so simple Essentially what's going wrong with the AVL file after #36 is that we overwrite predicate access values when maybe we shouldn't Example:

field i: Int

predicate int(this: Ref) {
  acc(this.i, 1/2)
}

method test(this: Ref)
  requires int(this) {}

Output:

method test(this: Ref)
  requires acc(this.i, 1) {}

Even though we have write access to the int predicate, that still doesn't give us write access to the field i, because the predicate only lets us have read access

[jyoo980]

So basically, the threaded value shouldn't overwrite the original value in the predicate?

[ionathanch]

From the tutorial:

Folding or unfolding a fraction of a predicate effectively multiplies all permission amounts used for resources in the predicate body by the corresponding fraction.

Which means that, for instance,

method test(this: Ref)
  requires acc(int(this), 1/2) {}

Should expand to:

method test(this: Ref)
  requires acc(this.i, 1/4) {}

Guess I should've read the tutorial more closely :facepalm: who knew it has such a bounty of information

[ionathanch]

I don't think it should be that hard to implement, it'll just need to use a custom context when traversing. I'll try fixing this one

[jyoo980]

@braxtonhall

NOW WE DO

👌👀👌👀👌👀👌👀👌👀 good shit go౦ԁ sHit👌 thats ✔ some good👌👌shit right👌👌there👌👌👌 right✔there ✔✔if i do ƽaү so my self 💯 i say so 💯 thats what im talking about right there right there (chorus: ʳᶦᵍʰᵗ ᵗʰᵉʳᵉ) mMMMMᎷМ💯 👌👌 👌НO0ОଠOOOOOОଠଠOoooᵒᵒᵒᵒᵒᵒᵒᵒᵒ👌 👌👌 👌 💯 👌 👀 👀 👀 👌👌Good shit

Remember to pull down latest master for silver

[braxtonhall]

holy

[braxtonhall]

wait for fold.vpr I'm still having a problem

2 errors

The following outputs were expected according to the test annotations, but did not occur during testing:
  unfold.failed:insufficient.permission (fold.vpr:34)
  fold.failed:assertion.false (fold.vpr:26)

[jyoo980]

~No that's what we want, it also fails on a vanilla build of VIper~

Oh shit i get what you're saying

[jyoo980]

hmm.. might be an error with the test.

When I run it locally, I get

jyoo@lambda silicon % ./silicon.sh --z3Exe '/Users/jyoo/dev/oss/z3-z3-4.3.2/build/z3'  ~/dev/oss/silver/vpr-test-files/fold.vpr
Silicon 1.1-SNAPSHOT (f52b14f8+)
Silicon found 1 error in 3.38s:
  [0] Assert might fail. Assertion false might not hold. (fold.vpr@18.5)
jyoo@lambda silicon % 

or are you running with Carbon?

[braxtonhall]

Running with Silicon :/

I can't get the test suite running with Carbon properly

[jyoo980]

I think we can ignore it, it's clearly failing when I run it manually. Not sure what's up with the test.

[braxtonhall]

The thing is, there are supposed to be three errors

[jyoo980]

I think it's failing early for our build i.e. when it sees that false error it freaks out and dies

[ionathanch]

t2 and t3 stop failing because there's assertions in the predicates being folded/unfolded that used to fail but no longer do because we've removed those statements idk how to fix tbh, the reasoning we had for why we remove them is still legitimate to me imo

[braxtonhall]

You don't think it has something to do with the fact that those are fold and unfold statements it's ignoring? edit: i'm too slow

[braxtonhall]

t2 and t3 stop failing because there's assertions in the predicates being folded/unfolded that used to fail but no longer do because we've removed those statements idk how to fix tbh, the reasoning we had for why we remove them is still legitimate to me imo

OK this is good to know I was hoping to have something like this thanks.

[ionathanch]

Okay I wasn't gonna think about this but now I'm thinking about it so there's no stopping. So I was thinking, let's say we have the usual tuple(this) that gets expanded into acc(this.left) && acc(this.right) in the precondition. Then at the moment where the unfold statement would occur, we should already have permission to this.left and this.right. And similarly, if that's expanded in a postcondition, then when we go to fold it up again, we need those permission in order to fold them.

So here's my idea: what if we replace every fold and unfold statement with an assert statement? Then that would fix those should-be-failing tests, since the assertion would check those predicate bodies. And since asserts don't do anything with permissions except to check that we have them, they shouldn't interfere with any sort of permissions around them.

[braxtonhall]

This sounds like a giant brain solution

[braxtonhall]

40 Seems to be resolved by this. The test still fails because it returns the wrong error message to the user but that's a different issue entirely

[ionathanch]

What changes in the error message? I'm guessing fold.failed and unfold.failed become assert.failed?

[braxtonhall]

Here's an example

The following outputs were expected according to the test annotations, but did not occur during testing:
  fold.failed:insufficient.permission (0049.vpr:38)

The following output occurred during testing, but should not have according to the test annotations:
  [assert.failed:insufficient.permission] [assert.failed:insufficient.permission] Assert might fail. There might be insufficient permission to access this.Cellx$ (0049.vpr@38.3)