smack
smack copied to clipboard
smackers
Behavior of unroll flag with Boogie
Currently it seems that it is impossible to invoke Boogie in modular verification mode (i.e., no unrolling) from the SMACK script. It is unclear what the best solution to this problem would be. Maybe introducing a new flag that turns on modular verification?
I had a different idea in mind: selective unrolling.
The idea was that the command-line interface remains the same, and by default all loops are unrolled, and procedures inlined. Any loops which are annotated with invariants are not unrolled, and any procedures which are annotated with specifications are not inlined. “Modular verification” thus happens only where there are procedure specifications or loop invariants.
Currently, in Boogie-verification mode, this might be implemented by removing the {:inline} annotation on procedures with specifications, and extracting invariant-annotated loops to procedure calls — again, without the {:inline} annotation — whose specifications are derived from the invariant annotations.
I do not know how this could be implemented in Corral mode.
Actually, I guess there is a more general implementation that handles both Corral- and Boogie-verification modes: move the implementation of each procedure which is subject to modular verification to a separate Boogie file.
Not sure whether there is an easier way to stop Corral from inlining (?).
Sorry, but how would moving procedures into separate files help? Also, for large projects we would be generating hundreds of such files. So even if this would help, I think it should be implemented behind some kind of a command line flag. Finally, does Corral even support annotations? I think we asked Akash that at some point, but I don't remember what the conclusion was.
If the implementation of each procedure p to be modularly verified were annotated with {:entrypoint} in its own separate file p.bpl, and its declaration but not its implementation were in the remaining *.bpl files, then Corral would verify p separately when running corral p.bpl, and use p’s specification only when verifying the remaining *.bpl files.
Not saying anything complicated :-)
Even if Corral does not support requires and ensures specifications, those can easily be translated to assume and assert statements.
If we want to go the selective unrolling road — and personally I think it is the most sensible — then adding a command-line flag seems a bit redundant or possibly conflicting. For example, if I write an invariant for loop L and don’t specify --selective-unrolling then should we unroll loop L? To me, the fact that I’ve given an invariant for L means that I want to abstract L with my invariant, and I do not want it unrolled. But I could probably be convinced otherwise.
I think it would be good to clarify what Corral exactly does in the presence of annotations. Clearly it does use pre- and post-conditions during verification (at least at call sites) since it works with our NO_REUSE memory model. So I think that we should first clarify with Akash exactly what happens when Corral encounters various kinds of annotations. For example, I am not sure what Corral would do if it encounters a loop with a loop invariant provided. Unless you already fully understand the extent to which annotations are supported in Corral.
Another thing to note - we have been working on adding symbooglix as another backend verifier option. It is probably unlikely that whatever strategy we come up with here for Corral would work with symbooglix. Thinking more about this, it seems that this effort is turning into us encoding modular verification within SMACK. This is clearly doable, but I do wonder if that is something we should actually be doing. Instead, that should probably be a functionality of backend verifiers.
Ok, we should do something about this. I had another thought recently related to this. Basically, our back-ends are not totally compatible, and will probably never be. For example, Boogie does not support concurrency and so --pthread option will not work with Boogie. Also, Corral currently does not support floats, and so --float will not work with Corral, while it will with Boogie. I am sure that when we add symbooglix soon, there will be similar issues.
So I think we need a general way to deal with these discrepancies between back-ends in the long run. Any suggestions?
I thought maybe we could introduce some kind of a "capability matrix" in our Python scripts, or something like that. And then if you select a command line option that is not supported by the selected back-end, an error is reported.