Closed jwkai closed 2 months ago
marcoeilers
commented
2 months ago Hi, thank you for your contribution and sorry it took so very long to get a response. It took me a bit to understand both why the change helps and why the rewriting is equivalent, but I'm convinced now, and the code looks good to me as well. Out of curiosity, do you have a "real" (as in, not artificial) example for which this leads to a significant speedup? I'd be interested in having a look at one if you do.
jwkai
commented
2 months ago Hi Marco,
No worries, I admit it took me a while to understand (and even longer to implement) as well! Alex Summers is really to credit for this idea.
Below is a "real" example of Viper code that led to this axiom modification. There is a Viper source (arrayTestChainIrrel3.viper), the Boogie file generated by Carbon (arrayTestChainIrrel3_sk.bpl) and the modified Boogie file with Skolemization (arrayTestChainIrrel3_nosk.bpl)
It's rather unreadable, but I believe the Viper should verify (under Carbon only, not Silicon, since it relies on heap-dependent triggers). And the Skolemized Boogie code should verify faster than the original. Please let me know if otherwise, this was all automatically generated code (even the Viper, by a plug-in that I'm working on).
The basic idea is: we increment the values of an array a at indices contained in two sets is: Set[Int] and js: Set[Int]. Each of these increment statements defines a new Heap in Boogie. Finally, we assume that is and js are disjoint, and then sum the array over only the indices contained in js, using the heap-dependent function __snap_Int_Int_Int_val(..., js).
So every increment statement of some index in the set is is "irrelevant" to our final assertion. By using this "relaxed Skolem function" for the heap framing axiom, we should avoid having to produce multiple framing arguments that __snap_Int_Int_Int_val(..., js) is unchanged across the intermediate heaps generated by loc(a, i_).val := loc(a, i_).val + 1 statements. I ran several examples where I added more and more "relevant" and "irrelevant" statements, and my benchmarks seem to indicate that that the verification times scale roughly with the "relevant" statements only.
Here's a "schematic" version of the code (you can interpret hfold[add()](arrayRec(a).val | js) as a heap-dependent function over the set js) :
method test1(a:Array)
requires access_array(a, 0, len(a))
requires len(a) > 10
{
var js: Set[Int]
var is: Set[Int]
assume js subset allInt(0, len(a))
assume is subset allInt(0, len(a))
var j1 : Int
assume j1 in js
var j2 : Int
assume j2 in js
var j3 : Int
assume j3 in js
var i1 : Int
assume i1 in is
var i2 : Int
assume i2 in is
var i3 : Int
assume i3 in is
var i4 : Int
assume i4 in is
var i5 : Int
assume i5 in is
var i6 : Int
assume i6 in is
loc(a,i1).val := loc(a,i1).val + 1
loc(a,j1).val := loc(a,j1).val + 1
loc(a,i2).val := loc(a,i2).val + 1
loc(a,i3).val := loc(a,i3).val + 1
loc(a,j2).val := loc(a,j2).val + 1
loc(a,i4).val := loc(a,i4).val + 1
loc(a,i5).val := loc(a,i5).val + 1
loc(a,j3).val := loc(a,j3).val + 1
loc(a,i6).val := loc(a,i6).val + 1
assume (js intersection is) == Set[Int]()
assert hfold[add()](arrayRec(a).val | js) ==
old(hfold[add()](arrayRec(a).val | js)) + 3
}arrayTestChainIrrel3.vpr.txt arrayTestChainIrrel3_nosk.bpl.txt arrayTestChainIrrel3_sk.bpl.txt
marcoeilers
commented
2 months ago Thanks!
This modifies the axiom used to frame heap-dependent functions and predicates with
Setarguments based on quantified permissions.The following explanation also exists in #522. We noticed that in the existing generated axiom, the LHS quantified formula that will become a negated existential on the left of a disjunction. For example:
This generates new Skolemized indices for
a: Refandi: Intfor each triggering of the outer quantified variablesHeap2Heap: HeapType, Heap1Heap: HeapType, vas: (Set Ref), vis: (Set int).However, there may be some prior equalities between the given heap-dependent term across other heaps. For example, if
then it is undesirable to generate distinct Skolemized indices for both triggerings of the QP axiom:
and
My modification defines a more general Skolem function for each quantified variable, taking applications of the heap-dependent function or predicate, in order to share witness indices. It substitutes these Skolem functions for the quantified variables in the LHS of the implication. For example:
We tested this on examples with heap-modifying statements both relevant and irrelevant to a given heap-dependent function application. We found that the verification times scale roughly with the number of relevant heap-modifying statements, whereas the original axiom scales with the total (relevant and irrelevant) number of heap-modifying statements.