EVM: Support exp aka pow #1361
Merged
EVM: Support exp aka pow #1361
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Adds support for EXP aka POW, with concrete or solvable exponent, fixing #1005 effectively. Not sure if we can do it any better - it seems z3 doesn't have exp/pow for bitvectors.
disconnect3d
changed the base branch from
py3-exp-unit-test
to
symbolic-tests
…to support-exp-pow * 'support-exp-pow' of github.com:trailofbits/manticore: Update evm.py Update operators.py
ehennenfent
pushed a commit
that referenced
this pull request
May 17, 2019
* Add assertions to auto test gen * Add symbolic tests * Make calldata symbolic * EVM: Support exp aka pow (#1361) * EVM: Add support for EXP with concrete/solvable exponent Adds support for EXP aka POW, with concrete or solvable exponent, fixing #1005 effectively. Not sure if we can do it any better - it seems z3 doesn't have exp/pow for bitvectors. * Update operators.py * Update evm.py * Use concretized_args * Move Operators.POW to EVM._exp * Extend travis wait for output to 30m * Extend travis build to 60m... * Fix Operators.ITE -> Operators.ITEBV * Split ethereum travis job to two jobs * EVM.EXP: concretize base=SAMPLED * Fix concrete tests: use to_constant * Fix set storage in concrete tests * Split ethereum_vm tests into concrete and symbolic * Fix travis tests * Split symbolic tests into two jobs * Split VMTests even more * More tests split * [WIP][WIP][WIP] Moving executor functionality to ManticoreBase and refactor concurrency shared data * Workspace locks * Concurrency flavor configurable from commandline * Asserts and refactorrrrrrrs * Remove unused callback * Some CC * Some CC * Some CC * Fix solver vs Z3Solver * Make solver a singleton based on tid/pid. REfactor m._save. Fix some tests * typo and evm bugfix * Fix some tests referecing global solver * Fix concolic tests and more global solver refs * Fix tests * CC fixes * Fix tests. Fix testcase id generation * Move profiling to a plugin and fix tests * Add solver intance ref to mem test * Fix mem workspace tests * Fix output checking tests * Fix z3solver ref * Relax verbosity/log tests * Moved Workers to its own file * Relax output tests * Relax output tests * Fix profiling test * Fix more tests * Default multiprocessing * Try to clean mcore __del__ * Change Worker life span * Fix Single mode * CC * revert verbosity travis * CC and solver ref fix * Relax ouput checking tests and some bugfixes * running -> ready * Fixing teeests * add weak cache to _load * del debug prints * Adding config.py support for Enums * Try/Remove generate_testcase event as it never occurs online. Fix tests * Fix CC * Kill the cache when start/stop run. Remove debugprints. clean tests * Fix travis test _other_ * Fix native tests and timeout * Fix state.must_be_true * fix CC * Changing fstat tets...: ~' * LLLLLLLLinux tests * Skip unicorn concrete test for now * Try fix CodeClimate * Try fix CodeClimate * Update evm examples to newest solidity * Complete transformation of consts.mprocessing to enum * Add blank line (codeclimate) * Using the enum instead of the string * Using the enum instead of the string * Merge and fix * CC and debug print * Move fee consumption to checkpoint so it is not done twice. Fix frontier test generator * Fix Job Count (and force travis rebuild) ``` 0.02s$ ./cc-test-reporter sum-coverage --output - --parts $JOB_COUNT coverage/codeclimate.*.json | ./cc-test-reporter upload-coverage --input - Error: expected 3 parts, received 4 parts ``` * Add tx number to testcase log * Del test verbosity
ehennenfent
added a commit
that referenced
this pull request
May 21, 2019
* Add assertions to auto test gen * Add symbolic tests * Make calldata symbolic * EVM: Support exp aka pow (#1361) * EVM: Add support for EXP with concrete/solvable exponent Adds support for EXP aka POW, with concrete or solvable exponent, fixing #1005 effectively. Not sure if we can do it any better - it seems z3 doesn't have exp/pow for bitvectors. * Update operators.py * Update evm.py * Use concretized_args * Move Operators.POW to EVM._exp * Extend travis wait for output to 30m * Extend travis build to 60m... * Fix Operators.ITE -> Operators.ITEBV * Split ethereum travis job to two jobs * EVM.EXP: concretize base=SAMPLED * Fix concrete tests: use to_constant * Fix set storage in concrete tests * Split ethereum_vm tests into concrete and symbolic * Fix travis tests * Split symbolic tests into two jobs * Split VMTests even more * More tests split * [WIP][WIP][WIP] Moving executor functionality to ManticoreBase and refactor concurrency shared data * Workspace locks * Concurrency flavor configurable from commandline * Asserts and refactorrrrrrrs * Remove unused callback * Some CC * Some CC * Some CC * Fix solver vs Z3Solver * Make solver a singleton based on tid/pid. REfactor m._save. Fix some tests * typo and evm bugfix * Fix some tests referecing global solver * Fix concolic tests and more global solver refs * Fix tests * CC fixes * Fix tests. Fix testcase id generation * Move profiling to a plugin and fix tests * Add solver intance ref to mem test * Fix mem workspace tests * Fix output checking tests * Fix z3solver ref * Relax verbosity/log tests * Moved Workers to its own file * Relax output tests * Relax output tests * Fix profiling test * Fix more tests * Default multiprocessing * Try to clean mcore __del__ * Change Worker life span * Fix Single mode * CC * revert verbosity travis * CC and solver ref fix * Relax ouput checking tests and some bugfixes * running -> ready * Fixing teeests * add weak cache to _load * del debug prints * Adding config.py support for Enums * Try/Remove generate_testcase event as it never occurs online. Fix tests * Fix CC * Kill the cache when start/stop run. Remove debugprints. clean tests * Fix travis test _other_ * Fix native tests and timeout * Fix state.must_be_true * fix CC * Changing fstat tets...: ~' * LLLLLLLLinux tests * Skip unicorn concrete test for now * Try fix CodeClimate * Try fix CodeClimate * Update evm examples to newest solidity * Complete transformation of consts.mprocessing to enum * Add blank line (codeclimate) * Using the enum instead of the string * Using the enum instead of the string * Merge and fix * CC and debug print * Move fee consumption to checkpoint so it is not done twice. Fix frontier test generator * Fix Job Count (and force travis rebuild) ``` 0.02s$ ./cc-test-reporter sum-coverage --output - --parts $JOB_COUNT coverage/codeclimate.*.json | ./cc-test-reporter upload-coverage --input - Error: expected 3 parts, received 4 parts ``` * Add tx number to testcase log * Attempt to do vmtests on the fly * Del test verbosity * Update .travis.yml Co-Authored-By: Eric Hennenfent <ecapstone@gmail.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Adds support for EXP aka POW, with concrete or solvable exponent, fixing #1005 effectively.
Not sure if we can do it any better - it seems z3 doesn't have exp/pow for bitvectors.
This change is