gradual viper backend seems to conflate predicates that are very similar

[JonathanAldrich]

Expected behavior: the file avl-bug4.c0.txt should verify.

Observed behavior: the fold on line 80 fails.

Tweak that surprisingly makes verification succeed: change the 0 on lines 35 and 79 to both be 1.

Theory: the back end maybe can't distinguish avlh(node->left, 0) from avlh(node->right, 0) properly. Changing one of the parameters to "1" avoids this problem by making the predicates more different.

You can also observe this problem with the predicate avl(...) instead of avlh(...). I just created avlh(...) on the theory that maybe the prover was having a hard time distinguishing two similar uses of avl(...).

[jennalwise]

Here is what the problem is, it is a backend issue: avlh(node->left, 0) symbolically evaluates to avlh(null, 0), and similarly avlh(node->right, 0) symbolically evaluates to avlh(null, 0) as well. So, the back to back folds //@ fold avlh(node->left, 0); and //@ fold avlh(node->right, 0); on lines 78 and 79 create a symbolic state with acc(avlh(null,0), 2) in the heap, notice the 2 permission value which is greater than 1. When the backend tries to consume avlh(node->left, 0) to satisfy //@ fold avlh(node, 0); (line 80) it requires that the permission to acc(avlh(null,0),1) be 1 rather than 2. This is also true for field accesses. I believe Viper itself only makes this restriction for fields and not predicates. So, the question is whether or not we are being to restrictive on write permissions for predicates. I think we can relax this constraint as well, but I would need to spend time making sure relaxing this constraint does not pose problems elsewhere (particularly where imprecision is concerned).

Note: this would verify successfully if any of symbolic values sent as arguments to avlh were different across the two predicates.

[JonathanAldrich]

Interesting. So if I assigned node->left to a "tree" generated by a different function that happens to return null (but the fact that it is null isn't in that other function's spec), the verifier wouldn't know that and the example would go through. Essentially it breaks because the verifier knows too much.

In the medium term it would be great to see if there's a way to fix this, perhaps via the approach you mention. This would probably be quite confusing to someone who doesn't understand how the verifier works. In the meantime we can work around it.