Verification error when verifying fully specified correct program

[cliu369]

Verifying the attached program results in the following error:

[error] Exception in thread "main" gvc.VerificationException: Loop invariant acc(maxSeg(list, y, max), write) && acc(acyclic(y), write) might not hold on entry. 
There might be insufficient permission to access maxSeg(list, y, max). (<no position>)

The same error occurs for both versions: the .c0 file with gvc0 and the .vpr file with silicon-gv.
The program verifies correctly on Viper example page and the VSCode Viper IDE.

• list_max.vpr
• list_max.c0

[pgupta751]

For list_max.vpr, updating acyclic as follows:
predicate acyclic(s: Ref) { s == null ? true : acc(s.val) && acc(s.next) && s != s.next && acyclic(s.next) }
fixes the issue. I think that fold maxSeg(list, y, $result) on line 55 of list_max.vpr was not working as intended as the symbolic state at that point does not have information on whether list == y. The change to acyclic predicate ensures list != y at line 54-55.
I think that when using https://viper.ethz.ch/examples/blank-example.html or VSCode Viper IDE, s != s.next is not needed because of some implementation difference. I'm not sure but I suspect it may be something to do with how recursive predicates or the separating conjunction && are dealt with.

On the other hand, adding && s != s->next to acyclic predicate in list_max.c0 results in a new error:

[error] Exception in thread "main" gvc.VerificationException: Conditional statement might fail. There might be insufficient permission to access y.Node$val. ()

The following .vpr file gets generated from the updated list_max.c0:
list_max-generated.vpr.txt
Running this file through the verifier results in the following error:

[0] Conditional statement might fail. There might be insufficient permission to access y.Node$val. ([email protected])

I am looking into this issue as well. There is no unfold acyclic(y) at the beginning of the while loop body in findmax() in the generated .vpr file. This might be because predicates in loop invariants before entering loops are not treated iso-recursively (mentioned in Gradual C0 paper section 4.3.7) to my understanding. I'm not sure, I may be missing something.

[pgupta751]

The second issue (with list_max.c0) turned out to be more straightforward. There is a typo in line 57 // @unfold acyclic(y); should instead be //@unfold acyclic(y);. Currently, the line is being parsed as a comment.
Fixing that and adding && s != s->next to acyclic predicate should be sufficient.

[cliu369]

Update: The root cause of the issue appears to be the same as #33 - requiring permission to a predicate to match exactly, so if a predicate has permission greater than 1 in the heap, then consuming it will always fail.

The following program is a minimal failing example:

field next: Ref

predicate acyclicSeg(s: Ref, e: Ref) {
    s == e ? true: acc(s.next) && acyclicSeg(s.next, e)
}

method minimal(list: Ref)
    requires acc(list.next) 
{
    var y: Ref
    y := list.next

    fold acyclicSeg(list.next, y) 
    fold acyclicSeg(list, list.next) 
    
    assert acyclicSeg(list, y) // This assert fails when it should succeed
}

The reason why adding s != s.next to the acyclic predicate or analogously adding list != list.next to the precondition in this minimal example fixes the issue is because it forces the verifier down the successful branch.

When folding acyclicSeg(list, list.next) since the verifier does not know whether list aliases with list.next, it will branch across two execution paths for the two cases. In the case where they do not equal, it succeeds, but in the case where they equal, it fails.

It fails because if list == list.next, then acyclicSeg(list, list.next) = acyclicSeg(list.next, y)= acyclicSeg(list, y), so it would have permission 2 in the heap. Then, when asserting acyclicSeg(list, y), it tries to consume but fails because consuming a predicate requires that the permissions match exactly.