Reduce the number of calls to the SMT solver in EVM #2411
Conversation
| Concretize a symbolic :class:`~manticore.core.smtlib.expression.Expression` into | ||
| one solution. | ||
| :param exprs: An iterable of manticore.core.smtlib.Expression | ||
| :param bool constrain: If True, constrain expr to solved solution value |
There was a problem hiding this comment.
It might be worth documenting that when constrain=True, the order of the expressions passed in could matter.
There was a problem hiding this comment.
To be honest, I haven't look on that parameter and I haven't change how other code call this. If you say this is expected behavior, I will modify the comment.
There was a problem hiding this comment.
Right, this is the expected behavior, but the comment makes no mention of it. This could be confusing to users because if you call solve_one_n_batched with contradictory constraints in exprs, which expressions are unsat will depend on which ones are solved first. It's been that way for as long as I can remember, so this is just a "as long as you're editing this function anyway..." suggestion
| @@ -658,7 +658,7 @@ def save_constraints(testcase, state: StateBase): | |||
| @staticmethod | |||
| def save_input_symbols(testcase, state: StateBase): | |||
| with testcase.open_stream("input") as f: | |||
| for symbol in state.input_symbols: | |||
| bufs = state.solve_one_n_batched(state.input_symbols) | |||
| for symbol, buf in zip(state.input_symbols, bufs): | |||
| # TODO - constrain=False here, so the extra migration shouldn't cause problems, right? | |||
There was a problem hiding this comment.
I think this comment might need to be moved to right before the state.solve_one_n_batched
Or maybe just removed?
There was a problem hiding this comment.
I'm not 100% sure about that comment. Do you know what it means?
There was a problem hiding this comment.
I don't know exactly, but I think it's referencing the default argument constrain=False in state.solve_one
* master: Install pinned version of truffle to fix CI (#2467) Use fixed owner and attacker accounts in multi_tx_analysis (#2464) Manticore 0.3.6 (#2456) Fix IntrospectionAPIPlugin Name (#2459) Portfolio of parallel solvers (#2420) Replace Quick mode with Thorough mode (#2457) Fix incorrect comparison for symbolic file wildcards (#2454) Reduce the number of calls to the SMT solver in EVM (#2411) Fixes to Unicorn emulation - start/stop/resume (#1796) Add support for multiple compilation units (#2444) Basic solver stats (#2415)
* master: (35 commits) Track last_pc in StateDescriptors (#2471) Expose Result Register for Native CPU (#2470) Install pinned version of truffle to fix CI (#2467) Use fixed owner and attacker accounts in multi_tx_analysis (#2464) Manticore 0.3.6 (#2456) Fix IntrospectionAPIPlugin Name (#2459) Portfolio of parallel solvers (#2420) Replace Quick mode with Thorough mode (#2457) Fix incorrect comparison for symbolic file wildcards (#2454) Reduce the number of calls to the SMT solver in EVM (#2411) Fixes to Unicorn emulation - start/stop/resume (#1796) Add support for multiple compilation units (#2444) Basic solver stats (#2415) Fix the generation of EVM tests (#2426) Disabled EVM events in testcases by default (#2417) added proper timeouts for cvc4 and boolector (#2418) Removed use of global solver from Native Memory (#2414) Support to use boolector as the SMT solver (#2410) Update CI and suggest to use pip3 instead of pip (#2409) Expressions use keyword-only arguments for init (#2395) ...
This PR reduces the number of solver queries allowing to use a list of expressions to concretize, instead of a single one.