-
Notifications
You must be signed in to change notification settings - Fork 49
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
Add configuration in a monadic way, for now used only to configure SMT2 debugging #405
Conversation
990a76b
to
1662425
Compare
Note, as part of the Keccak PR I am making, I am moving more things to the |
Co-authored-by: dxo <[email protected]>
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.
just a few small nits, but otherwise looks great!
cc @arcz this is a breaking change that may impact echidna.
Description
This is a rather big change. It adds a monad that allows us to pass a global configuration down. This can be extremely helpful, e.g. also for abstraction-refinement, Expr debugging, and a bunch of other things. It required a bit of change here-and-there, but it's not that bad. It will allow us to pass a lot less parameters around for global configs.
This also adds dumping of SMT2 queries. This is done by adding one more field to the SMT2 datatype, the
Expr
that it was generated from. This is essential, otherwise we don't know from that place the SMT2 is coming from. It helps significantly with debugging the SMT2. Passing thisExpr
in any other way is not really possible, not in a clean way as far as I can see. It really does belong with the SMT2, I think.Configurations supported:
Checklist