stainless
stainless copied to clipboard
epfl-lara
Experiment: Less duplication, more aggressive let simplification
This PR adds let-bindings in favor of duplicating code in two more places (match desugaring and assertions for ADT field selections). Conversely, it also adds an additional let-simplifications step in InoxEncoder, as encoded functions would so far not benefit from such simplifications and end up in queries to solvers.
The change doesn't seem to have any tremendous impact on performance. Integration tests run in roughly the same amount of time, while non-integration tests might be marginally slower.
It seems the sbt test step (i.e. non-integration tests) previously consistently took around 2m30s, while on the two CI runs here it took ~30s longer, but this is obviously not a great benchmark. I manually looked at the newly-introduced verification.simplify timer for the examples run in sbt test and there are only two occasions on which it takes more than 50ms. So I'm not sure where these slowdowns -- if they're real -- even come from.
@samarion Did we ever have a proper CI for verification times?
No, but I believe the main blocker is performance inconsistency within the SMT solvers. The solvers are typically fairly deterministic but rely on the input SMT-LIB to "seed" their heuristics. Since the Stainless transformation pipeline isn't 100% deterministic (because of non-deterministic ordering of identifier freshening), the performance can vary quite a bit for no good reason.
About these simplifications: I also worked on (and fiddled with) the simplifier infrastructure quite a bit and my main take-away was that making the input simpler for humans (as in less duplication and smaller ASTs) doesn't actually help the SMT solvers that much. IIRC, the only simplifications which really made a difference were
- Reducing the exponential growth of unfoldings. There were two main transformations which helped for this, namely a. merging function calls which appear in multiple branches (see mergeFunctions in Inox), and b. dropping function calls from assertions which aren't in the VC context (but this also somewhat weakens the solving procedure).
- Introducing domain-knowledge assertions, e.g. that function calls don't depend on ghost argument values (used in Stainless type encoding IIRC).
Thanks, that's very interesting! Viktor actually mentioned something like mergeFunctions the other day, so I shouldn't be surprised to discover that you actually foresaw this :-)
The changes in this PR remove some exponential growth, but at least the tweak for scrutinees probably doesn't apply to many of our (existing) test cases. I did stumble on the issue while working on imperative code, where a simple x.field match { ... } can grow quite dramatically due to Imperative + TypeEncoding + AssertionInjector. In that context it scraped ~8s off a 30s VC, so it seemed quite worthwhile.
Despite this PR not making a significant dent in our CI runtime, I'm still leaning toward merging it, if only to make everyone's life easier in reading the resulting TIP files.
There are, however, some reservations wrt. Streams, since let-binding intermediate expressions drops RecursiveTypes in some places (we drop them in computeType, @jad-hamza pointed out). This seems like a general source of brittleness in the Inox type-system, so I didn't intend to solve it on this PR.
Astonishingly, this is almost merge-able, but I guess it's not clear if we want it?
