Verification aborted exceptionally: pure quantifier and unfolding expression in function body

[gauravpartha]

The following program leads to Silicon aborting verification exceptionally:

field elem: Int
field next: Ref

predicate list2(this: Ref, i: Int) {
  acc(this.elem) && acc(this.next) &&
  (this.next != null ==> list2(this.next, i))
}

function foo(l:Ref, i: Int) : Bool
  requires list2(l, i)
{ 
  forall j:Int ::
        i == j ==> unfolding list2(l,j) in l.next == null ? true : foo(l.next, j) 
}

Silicon's output is:

Verification aborted exceptionally: java.util.concurrent.ExecutionException: viper.silicon.reporting.Z3InteractionFailed: Unexpected output of Z3. Expected 'success' but found: (error "line 737 column 68: unknown constant
j")
Cause: viper.silicon.reporting.Z3InteractionFailed: Unexpected output of Z3. Expected 'success' but found: (error "line 737 column 68: unknown constant j")
Silicon found 1 error in 4.68s:
[0] Interaction with Z3 (instance 00) failed: Unexpected output of Z3. Expected 'success' but found: (error "line 737 column 68: unknown constant j")

[mschwerhoff]

Will hopefully all get fixed by Mauro Bringolf's current work on redesigning Silicon's snapshots.

[maurobringolf]

Interesting! My fork produces the same error and as far as I can tell it comes from the following predicate-based trigger of foo's definitional axiom.

Since the function unfolds list2(l,j), Silicon adds an extra trigger to the function axiom:

{foo%stateless(l,i), list2%trigger(s,l,j) }

where s is the snapshot that was unfolded. So unfortunately, the j can escape its scope via this mechanism. The intended trigger term would contain list2%trigger(s,l,i) instead of the one with j. My fork only changes the shape of snapshots but not this predicate-based trigger mechanism, so in this case my predicate snapshot also contains a syntactic j and runs into the same problem. I think the issue here is independent of my work.

I am not sure how difficult it is to solve this problem in general, but maybe one can tweak how Silicon remembers the unfolded predicates from a function body such that the argument would resolve to the desired i instead of the syntactic j.

• https://github.com/viperproject/silicon/blob/master/src/main/scala/supporters/functions/FunctionData.scala#L210
• https://github.com/viperproject/silicon/blob/master/src/main/scala/supporters/functions/FunctionData.scala#L169-L197

[mschwerhoff]

@maurobringolf Thanks for looking into this. I'll think about how a general solution should look here.

[mschwerhoff]

@maurobringolf Running Z3 on logfile-00.smt2 generated for this example shows invalid pattern warnings (for pattern {foo%limited(...)}), which appear to result from the way function snapshots are currently built. This issue, however, should be resolved by your changed, right? Or am I again too optimistic here ...?

[mschwerhoff]

Resolved with commit c8d4c96.

The aforementioned problem of generating invalid patterns persists.

[maurobringolf]

I am not sure, but I will have another look at what my fork does with this (and your changes), then report back in the next meeting in person.

[maurobringolf]

@mschwerhoff I am looking into this again and added Silver pull request with an extension of the test case.

[maurobringolf]

A fix

@mschwerhoff You were right, semantic snapshots can fix this problem but it took me a while to figure out how. It is now implemented and tested in my fork. The idea is to add j to the function axiom quantifier which at first glance seems to widen the trigger to { foo(l,i), list(l,j) } for any j instead of just { foo(l,i), list(l,i) }. But looking at the generated trigger pattern shows that it is much more precise than that:

∀ h, l, i, j. { foo%stateless(l,i), list2%trigger(PHeap.lookup_list2(h, l, j), l, j) } ...

The second part of the pattern makes sure that only combinations of j and h are possible where h (semantically) contains the instance list2(l,j) and the predicate tag (list%trigger) for that instance is available. And since the precondition only includes list2(l,i), I believe this can in fact only be instantiated with j = i as desired. I tried to modify the example here to check this, but found it difficult to obtain the desired terms through the Viper level. But maybe one can construct a different example which better shows the triggering behavior.

The corresponding commit is mschwerhoff@bc21fea.