manticore icon indicating copy to clipboard operation
manticore copied to clipboard

Delay smt-solving until it is absolutely necessary in EVM

Open gustavo-grieco opened this issue 4 years ago • 2 comments

This PR contains:

  • A lazy evaluation mode for jumpi constraints enabled by default (so we can see the effects in the tests). This mode cannot be used if the code contains a loop. There is no automatic detection of that, so the user should be careful when using this mode. It is unclear how to handle that in the middle of a manticore run.
  • Various fixed for the evm tests to make sure the states are always sound.
  • test_jmpdest_check test was disabled.
  • Some tests using plugins require lazy mode to be disabled.

The last two bullets should be discussed before merging this PR.

gustavo-grieco avatar Apr 06 '21 18:04 gustavo-grieco

@ggrieco-tob I can't replicate the failing tests locally. I believe you had the same problem as well. I'd say let's hold this one back from the next release? That will give us more time to figure out what's going on.

ehennenfent avatar Jun 09 '21 23:06 ehennenfent

CLA assistant check
Thank you for your submission! We really appreciate it. Like many open source projects, we ask that you all sign our Contributor License Agreement before we can accept your contribution.
1 out of 2 committers have signed the CLA.

:white_check_mark: ggrieco-tob
:x: Eric Hennenfent


Eric Hennenfent seems not to be a GitHub user. You need a GitHub account to be able to sign the CLA. If you have already a GitHub account, please add the email address used for this commit to your account.
You have signed the CLA already but the status is still pending? Let us recheck it.

CLAassistant avatar Jun 01 '22 05:06 CLAassistant