-
Notifications
You must be signed in to change notification settings - Fork 54
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Experiment: Less duplication, more aggressive let simplification #860
base: scala-2
Are you sure you want to change the base?
Conversation
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 @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
|
Thanks, that's very interesting! Viktor actually mentioned something like 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 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 |
@@ -199,7 +199,8 @@ trait TreeDeconstructor extends inox.ast.TreeDeconstructor { | |||
case s.RecursiveType(id, tps, e) => (Seq(id), Seq(), Seq(e), tps, Seq(), (ids, _, es, ntps, _) => t.RecursiveType(ids(0), ntps, es(0))) | |||
case s.ValueType(tpe) => (Seq(), Seq(), Seq(), Seq(tpe), Seq(), (_, _, _, tps, _) => t.ValueType(tps(0))) | |||
case s.AnnotatedType(tpe, flags) => | |||
(Seq(), Seq(), Seq(), Seq(tpe), flags, (_, _, _, tps, flags) => t.AnnotatedType(tps(0), flags)) | |||
(Seq(), Seq(), Seq(), Seq(tpe), flags, | |||
(_, _, _, tps, flags) => if (flags.nonEmpty) t.AnnotatedType(tps(0), flags) else tps(0)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We usually try not to simplify within the Deconstructor to make sure transformations are as predictable as possible. You could add the corresponding transformation within one of the various simplify procedures.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Okay, I'll see if I can find some simplification that's already applied anyways. I guess I'd still like to add an assertion in AnnotatedType
that ensures we never end up with an empty list of annotations (which is impossible to spot in the pretty-printed tree!).
} | ||
|
||
// NOTE(gsps): Keeping the old, code-duplicating behavior here, since index annotations on | ||
// types are not propagated through `expr.getType`, breaking the Streams example. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess an alternative would be to replicate part of the type inference logic from the type checker. In the long run, it probably makes more sense to move all the assertion checks there anyway.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You mean add the assertion check for ADTSelector
in TypeChecker
directly?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well, all of the assertion checks injected in this class, really. It's not quite as good in terms of separation of concerns, but it makes sense to centralize all the checking.
Using let-bindings with type inference would also be reasonable and possibly not that difficult to implement. Actually, it would be great if we could add a simple locale type inference phrase to Stainless to compensate a bit for the lack of dependent types in Scala.
Astonishingly, this is almost merge-able, but I guess it's not clear if we want it? |
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.