Optional Snapshot Generation in Consume

[mlimbeck]

During the execution of certain statements, consume generates snapshots that are unused. For consuming QP-Chunks, this results in unnecessary snapshot map definitions being triggered, increasing the number of quantifier instantiations and negatively impacting performance.

To address this, snapshot generation is now prevented for these cases. While the primary performance improvement applies to consuming QP-Chunks, the change is also applied to consuming non-QP-Chunks to ensure consistent behavior across all scenarios.

Example:

var rs: Set[Ref]
var x: Ref
var val: Int
assume x in rs
inhale forall r: Ref :: r in rs ==> acc(r.f)

val := x.f // This will trigger all snapshot map definitions related to x.f.

exhale forall r: Ref :: r in rs ==> acc(r.f, 1/3) 
exhale forall r: Ref :: r in rs ==> acc(r.f, 1/3) 
// The exhales will create new snapshot map definitions which are never needed but still triggered.

Affected Statements:

Field assignments
Method calls (consume of pres)
Exhale statements
Assert statements
While loops (consume of invariants)

[jcp19]

I wonder, did you benchmark this on sth like scion or sth generated by Prusti? I wonder what are the implications in performance (and potentially completeness)

[marcoeilers]

Completeness should not be impacted in any way, the snapshots are only omitted when they definitely won't be used.

[marcoeilers]

Thanks!
I marked three things, everything else looks fine to me.

[mlimbeck]

I wonder, did you benchmark this on sth like scion or sth generated by Prusti? I wonder what are the implications in performance (and potentially completeness)

For the moment there are no measurable benefits for Scion. However, I expect it will improve the performance of run().

As an illustrative example, consider a case where we sum over n arrays. The following table demonstrates how the number of quantifier instantiations is reduced when using this approach:

Arrays	with snapshots	without snapshots
5	2.556	1.876
10	25.700	16.443
15	77.481	59.156

Example Code

method sum(a0: IArray, n: Int) returns (res:Int)
requires forall j: Int :: {loc(a0, j)}  0 <= j && j < n ==> acc(loc(a0, j).val, 1/2)
requires len(a0) == n
ensures forall j: Int :: {loc(a0, j)}  0 <= j && j < n ==> acc(loc(a0, j).val, 1/2)
ensures len(a0) == n
{
	var i: Int
	i := 0 
	res := 0 
	while(i < n )
        invariant forall j: Int :: {loc(a0, j)}  0 <= j && j < n ==> acc(loc(a0, j).val, 1/2)
        invariant len(a0) == n
        invariant  0 <= i && i <= n
        {
	   res := res + loc(a0, i).val
	    i := i + 1
      }
}