Skip to content

Large EVM refactor #843

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 146 commits into from
May 25, 2018
Merged

Large EVM refactor #843

merged 146 commits into from
May 25, 2018

Conversation

feliam
Copy link
Contributor

@feliam feliam commented Mar 23, 2018 •
edited
Loading

WIP
It make storage and memory be raw smtlib arrays.

  • This enables to have unconstrained symbolic indexes. (previously we solved symbolic indexes eagerly)
  • EVM internal api evm_cpu vs evm_world improved
  • EVM basic block to smtlib. Arbitrary reasoning over EVM traces.
  • Initial symbolic gas support. Gas restricts memory access on a memory read over a free symbolic index. Example: With a gas budget of 99, MREAD(free_symbolic_index) can not really read any memory offset but jjust the ones that it has enough gas for.
  • world.transactions history can be queried from API/Detectors
  • Instructions continuations. For example CALL has 2 versions one that runs before the tx and one that runs after it.
  • Detector for simple integration test
    Fixes symbolic memory research #736
  • LInk with special Manticore Library (like klee special functions)
$ python asm_to_smtlib.py 
CODE:
	0 PUSH1 0x60
	2 PUSH1 0x40
	4 MSTORE
	5 PUSH1 0x0
	7 DUP1
	8 PUSH1 0x14
	10 PUSH2 0x100
	13 EXP
	14 DUP2
	15 SLOAD
	16 DUP2
	17 PUSH1 0xff
	19 MUL
	20 NOT
	21 AND
	22 SWAP1
	23 DUP4
	24 ISZERO
	25 ISZERO
	26 MUL
	27 OR
	28 SWAP1
	29 SSTORE
	30 POP
	31 CALLVALUE
	32 ISZERO
	33 PUSH2 0x29
	36 JUMPI
STORAGE = (store STORAGE #x0000000000000000000000000000000000000000000000000000000000000000 (bvand (select STORAGE #x0000000000000000000000000000000000000000000000000000000000000000) #xffffffffffffffffffffff00ffffffffffffffffffffffffffffffffffffffff))
MEM = (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store EMPTY_MEMORY_13 #x0000000000000000000000000000000000000000000000000000000000000040 #x00) #x0000000000000000000000000000000000000000000000000000000000000041 #x00) #x0000000000000000000000000000000000000000000000000000000000000042 #x00) #x0000000000000000000000000000000000000000000000000000000000000043 #x00) #x0000000000000000000000000000000000000000000000000000000000000044 #x00) #x0000000000000000000000000000000000000000000000000000000000000045 #x00) #x0000000000000000000000000000000000000000000000000000000000000046 #x00) #x0000000000000000000000000000000000000000000000000000000000000047 #x00) #x0000000000000000000000000000000000000000000000000000000000000048 #x00) #x0000000000000000000000000000000000000000000000000000000000000049 #x00) #x000000000000000000000000000000000000000000000000000000000000004a #x00) #x000000000000000000000000000000000000000000000000000000000000004b #x00) #x000000000000000000000000000000000000000000000000000000000000004c #x00) #x000000000000000000000000000000000000000000000000000000000000004d #x00) #x000000000000000000000000000000000000000000000000000000000000004e #x00) #x000000000000000000000000000000000000000000000000000000000000004f #x00) #x0000000000000000000000000000000000000000000000000000000000000050 #x00) #x0000000000000000000000000000000000000000000000000000000000000051 #x00) #x0000000000000000000000000000000000000000000000000000000000000052 #x00) #x0000000000000000000000000000000000000000000000000000000000000053 #x00) #x0000000000000000000000000000000000000000000000000000000000000054 #x00) #x0000000000000000000000000000000000000000000000000000000000000055 #x00) #x0000000000000000000000000000000000000000000000000000000000000056 #x00) #x0000000000000000000000000000000000000000000000000000000000000057 #x00) #x0000000000000000000000000000000000000000000000000000000000000058 #x00) #x0000000000000000000000000000000000000000000000000000000000000059 #x00) #x000000000000000000000000000000000000000000000000000000000000005a #x00) #x000000000000000000000000000000000000000000000000000000000000005b #x00) #x000000000000000000000000000000000000000000000000000000000000005c #x00) #x000000000000000000000000000000000000000000000000000000000000005d #x00) #x000000000000000000000000000000000000000000000000000000000000005e #x00) #x000000000000000000000000000000000000000000000000000000000000005f #x60)
CONSTRAINTS:

PC: [41, 37]

This change is Reviewable

feliam added 30 commits February 2, 2018 16:14
@feliam
Array value configurable. 8,16,32..256 bits (not prefixed to 8)
58cefb7
@feliam
Test Array256->256
986d595
@feliam
Remove old 8 bit assumptions
69c083b
@feliam
Add arrayProxy copy constructors and remove old 8 bit assumptions
ae0747d
@feliam
remove old 8 bit assumptions
cd2c403
@feliam
remove old 8 bit assumptions
01bce9f
@feliam
Better ArrayProxy special case handling
de7b509
@feliam
WiP-research Use raw no-optimized smtlib generic arrays as memory and…
a7e8482 
… storage
@feliam
remove pdebug print:
d59fe7d
@feliam
Fix tests
5ba7634
@feliam
Merge branch 'dev-smt-generic-arrays' into dev-evm-arraystorage
23c9716
@feliam
Review fixes
b5b0cbd
@feliam
review fix
cbbadb0
@feliam
merge
4cbd7c3
@feliam
fix gas variable
7a911e5
@feliam
Review fixes
4ef56c4
@feliam
git hell
ce48c25
@feliam
Access global storage trough internal api
47ca192
@feliam
fix asm_to_smtlib
0cb35f1
@feliam
Fix vm.gas access
aef91db
@feliam
Merge branch 'dev-smt-generic-arrays' into dev-evm-arraystorage
92719f6
@feliam
Merge branch 'master' into dev-evm-arraystorage
3f01003
@feliam
getvalue hack
e82bc9b
@feliam
Merge branch 'dev-evm-arraystorage' of github.com:trailofbits/mantico…
3b5233c 
…re into dev-evm-arraystorage
@feliam
Improve internal API
41ac7b6
@feliam
solver.can_be_true(cs, True) must check that cs is feasible
0dad2d3
@feliam
Simpler callstack code
5142a4f
@feliam
merge
5212d5f
@feliam
Fix merge and tests
e84dad6
@feliam
Merge branch 'master' into dev-evm-arraystorage
04ed0f0
yan and others added 20 commits May 25, 2018 16:48
@yan
Merge branch 'dev-evm-reservoir-of-awesomeness' of github.com:trailof…
5771dff 
…bits/manticore into dev-evm-reservoir-of-awesomeness
@offlinemark
remove more questionable tests
66689e5 
same thing as with the blockhash thing. we're doing things a little more symbolically now so comparing to concrete will not work
@yan
Accomodate our chubby State class
d6ccd99
@yan
Merge branch 'dev-evm-reservoir-of-awesomeness' of github.com:trailof…
b46827e 
…bits/manticore into dev-evm-reservoir-of-awesomeness
@feliam
Keep moving the refunds
bba32a2
@feliam
Merge branch 'dev-evm-reservoir-of-awesomeness' of github.com:trailof…
afb714a 
…bits/manticore into dev-evm-reservoir-of-awesomeness
@feliam
Disble reachability test for now
5c689c6
@feliam
Remove double declaring log for now
b5a4043
@offlinemark
Fix coverage calculation
5d1251c 
was prev creating a generator, which you can't do `in` on??
@offlinemark
require 1 tx for int overflow test
13fd9e6
@feliam
Fix path tests
3a9f258
@feliam
Merge branch 'dev-evm-reservoir-of-awesomeness' of github.com:trailof…
6b3f689 
…bits/manticore into dev-evm-reservoir-of-awesomeness
@feliam
Remove debug print in tests
8193754
@yan
Only enable gas when necessary
21e274a
@yan
codeclimate fixes
c95c5e9
@feliam
Fix concretize_args
a787731
@feliam
Merge branch 'dev-evm-reservoir-of-awesomeness' of github.com:trailof…
49ff9eb 
…bits/manticore into dev-evm-reservoir-of-awesomeness
@offlinemark
only 1 tx
d67dc9e
@yan
Disable max/min support in solver
5b117dc
@yan
Merge branch 'master' into dev-evm-reservoir-of-awesomeness
08d8ff9
offlinemark
offlinemark approved these changes May 25, 2018
View reviewed changes
Copy link
Contributor

@offlinemark offlinemark left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱

@feliam feliam merged commit c29c3cc into master May 25, 2018
@feliam feliam deleted the dev-evm-reservoir-of-awesomeness branch May 25, 2018 23:22
@feliam feliam removed their assignment May 26, 2018
@dguido dguido changed the title [WIP] Large EVM refactor Large EVM refactor May 29, 2018
This was referenced Jun 7, 2018
Merged
Merged
This was referenced Jul 5, 2018
Closed
Closed
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@disconnect3d disconnect3d disconnect3d left review comments

+1 more reviewer

@offlinemark offlinemark offlinemark approved these changes

Reviewers whose approvals may not affect merge requirements
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@feliam @offlinemark @disconnect3d @yan