search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
431 stars 82 forks source link

Unused declarations and axioms slowing down verification #370

Open zvonimir opened 6 years ago

zvonimir commented 6 years ago

There are indications that unused axioms and declarations sometimes slow down verification. On top of that, they make our generated Boogie files daunting to read, especially for novice users. I think we should be generating only axioms and declarations that are actually needed for a given file. The analysis should be simple and purely syntactical, not semantical. For example, we generate iN integer axioms for a large set of Ns, most of which are typically needed. With the recent move to generate prelude from Python, this should be doable.

I suggest we track all integer types as they are being generated by llvm2bpl, and we only generate axioms for the types that actually appear in the program.

shaobo-he commented 6 years ago

Symbooglix has a pass to remove unused axioms and declarations. Although that pass is buggy, since we add Symbooglix to the support, can we add an option to invoke this pass before verification?