Slow verification with trivial quantified permissions

[bobismijnnaam]

Dear Viper team,

Summary: A common pattern for specifying permissions in VerCors seems to lead to slow verification, even on what seems like simple programs & contracts. Is this an intrinsic limitation, and should we just use not more than 5 quantified permissions per method (that would be pretty bad honestly, but at least now we finally know about it...?), or did I still do something wrong and can I fix it by changing the code/spec? Please have a look at the minified example, flame graph, and comments on the silicon implementation.

Long question: the following program (triggerTest_small.vpr.txt) only inhales and exhales quantified permissions. It does not actually mutate state, or shift the ranges of the quantified permissions. All quantified permissions look like this:

ensures acc(d.a, write)
ensures d.a != (none1(): Option[Array])
ensures (forall preferred_list_i__: Int ::
    { aloc(optGet1(d.a), preferred_list_i__) }
    0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(d.a)) ==>
    acc(aloc(optGet1(d.a), preferred_list_i__).int, write))

Repeated 9 times as pre/postconditions, for fields a, b, and c, for variables c, d, and e.

The main program is as follows:

method foo1(c1: Ref, d: Ref, e: Ref)
// ... spec ommitted ...
{
  bar1(c1)
  bar1(d)
}

bar1 requires permission for fields a, b and c of the argument, and permissions of all indices of fields a, b, and c (in the frontend input file, a, b and c are of type int[]). Without bar1(d), verification is pretty much instant. With bar1(d), verification takes around 5 minutes. This time almost entirely spent exhaling the quantified permissions in the postcondition of foo. As more postconditions are exhaled, verification time increases, even though these postconditions and the quantifiers look like something viper could easily handle. The last quantified permission takes around 2 minutes, the one before that 74s, etc.

After some investigation (basically printf-style debugging using VerCors' pprof support), it seems these are the places where silicon spends a lot of time. These are all located in QuantifiedChunkSupport.scala:

• In the precomputedData foreach loop silicon spends 15 seconds:
  • 7 seconds of this is the chunkDepleted check
  • 7 seconds for the intermediate check at the end of the loop iteration
  • This duration becomes 15 seconds early on, and then seems to stop growing
• The "Final check if taken enough permissions" takes up even more time: 110 seconds for the final quantified permission. However, for earlier quantified permissions, it is a lot smaller (2s), and the precomputedData loop dominates verification time (8s)
  • Early on, the duration of this check is pretty quick, but the last 3 quantified permissions growth speeds up dramatically

Ideally, perhaps naively, I'd like to solve both of these bottlenecks somehow, by either adding more annotations, or improving silicon.

This is the flame graph produced by pprof/VerCors (input file: profile.pprof.gz, view "flame graph (old)", measure "wall"):

Is there a strategy to resolve this? As far as I can see the triggers for these quantified permissions are good. Perhaps our array ADT has a problem? But as far as I know it is pretty much a standard formulation. Are universal quantifiers needed to reason about quantified permissions messing with the proof search? From what I've seen in Malte's thesis, they don't look to complicated either, so I am not sure what is going wrong...

(Side note: interestingly this problem only turns up when you decouple writing programs from writing annotations needed for these programs. E.g. a student of mine ran into this because he was basically stacking macros to describe all the permissions he needed for an industrial case study, which exploded the number of QPs, which made verification slow, even though his triggers did not look to bad. Also a few times improving triggers did not improve the verification time. Now, similarly, I am working on (very simple) permission generation in VeyMont/VerCors, and I run into this program that has three variables that each have three fields of type int[]. And suddenly verification becomes unbearable. In other words, I would've never written this program if I also had been required to write the annotations for it. And then I would not have run into this problem. Very interesting.)

Thanks for any help or insight you can offer!

Edit: here's some z3 statistics of before & after the "final check" z3 interaction. Quantifier instantiations and arithmetic is quite high; not sure what to do about that...

[marcoeilers]

I just set up a PR that changes the heuristics that determine in which order quantified chunks are processed. With that change, the attached example verifies in Silicon in ca. 5 seconds (same as in Carbon), at the cost of only a tiny bit of additional overhead for ordering the chunks.
Hopefully, many similar examples should be sped up as well; it would be great to hear if this is the case or not.
If you have other examples that should be simple to verify but take way too long, it'd be great to get those as well; there may be similarly simple solutions.

[bobismijnnaam]

Thanks a lot! On the one example I have this works very well. I'll have a look if this saves time in general. Oh, there are many, but I'm not sure if we can isolate the problem as nicely as we've done here...