Skip to content
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

Delay smt-solving until it is absolutely necessary in EVM #2425

Open
wants to merge 27 commits into
base: master
Choose a base branch
from

Conversation

ggrieco-tob
Copy link
Contributor

@ggrieco-tob ggrieco-tob commented Apr 6, 2021

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.

@ggrieco-tob ggrieco-tob marked this pull request as ready for review April 9, 2021 21:48
@ehennenfent ehennenfent added this to In progress in Manticore via automation Apr 13, 2021
@ehennenfent ehennenfent moved this from In progress to Review in progress in Manticore Apr 13, 2021
manticore/core/state.py Outdated Show resolved Hide resolved
manticore/core/state.py Outdated Show resolved Hide resolved
manticore/platforms/evm.py Outdated Show resolved Hide resolved
manticore/platforms/evm.py Show resolved Hide resolved
manticore/ethereum/manticore.py Outdated Show resolved Hide resolved
ggrieco-tob and others added 4 commits June 8, 2021 16:34
It's already disabled and we want to look at these tests again if we enable it by default in the future.
@ehennenfent
Copy link
Contributor

@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 ehennenfent moved this from Review in progress to To do in Manticore Sep 7, 2021
@CLAassistant
Copy link

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.

✅ ggrieco-tob
❌ 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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
Manticore
  
To do
Development

Successfully merging this pull request may close these issues.

None yet

3 participants