manticore
manticore copied to clipboard
Delay smt-solving until it is absolutely necessary in EVM
This PR contains:
- A lazy evaluation mode for
jumpiconstraints 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_checktest was disabled.- Some tests using plugins require lazy mode to be disabled.
The last two bullets should be discussed before merging this PR.
@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.
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.