Generating easier-to-understand verification conditions

[shazqadeer]

@barrettcw has indicated that it is really difficult to understand the verification conditions generated by Boogie when debugging performance problems at the SMT level. There are many issues including:

• mangling of names
• inlining of functions
• encoding of control flow in non-obvious ways

@barrettcw will chime in with thoughts on the major (and possibly ranked) pain points. He might also want to chime in on low-hanging fruit that is likely to have large impact on debugging.

[barrettcw]

One easy thing to do is for Boogie users to prefer {:define} to {:inline} for functions. {:define} is a new feature I added maybe a year ago. It adds a function definition instead of inlining. SMT solvers then have the choice to inline or not.

[barrettcw]

For name mangling, it would be great if there was an easy way to trace back a name to where it came from in the Boogie source. Some suggestions include adding comments to the SMT file and using names from the Boogie source whenever possible.

[barrettcw]

Another suggestion is to have SMT assertions match Boogie lines of code whenever possible. More specifically, instead of taking an entire procedure and turning it into a single assertion that spans multiple lines, can we instead generate a single assertion for each line in the procedure, and annotate each assertion with its source line number? This would go a long way towards making the SMT files readable.

[barrettcw]

In general, it would be great if some thought were given to the look and feel of generated SMT files. I know that Boogie users hope to never look at those files, but if there's an issue in the solver interface or a performance problem in the solver, it's really hard to debug with the currently generated files.