Skip to content

Commit 3ed5f6e

Browse files
author
dwightguth
authored
refactor disassembly (#432)
* evm: refactor precompiled contracts * evm: remove PUSH data from OpCode sort * evm: add all opcodes to #dasmOpCode * Dockerfile: improve caching of maven * Makefile: fix proof tests * evm: fixup dasmOpCodes * evm: fix symbolic version of dasmOpCodes * fix damsOpCodes for symbolic backends * Makefile, driver, asm: add assembler for EVM OpCodes to ByteArray * driver: use assembler when user specifies OpCodes as input * tests/specs: update sum-to-n-spec * asm: ensure different klabels * asm: don't use owise on symbolic path * tests/specs: update sum to n spec * tests/interactive: update kast * tests/interactive/search: update output for search tests * Dockerfile, asm, evm, tests/sum-to-n: formatting fixes * evm: don't make #precompiled? a function * evm: fix compile error * Makefile: fix merge error * deps/k: revert haskell backend
1 parent 28b1d32 commit 3ed5f6e

File tree

10 files changed

+338
-73
lines changed

10 files changed

+338
-73
lines changed

‎Dockerfile

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,5 +43,18 @@ ADD --chown=user:user deps/k/haskell-backend/src/main/native/haskell-backend/kor
4343
RUN cd /home/user/.tmp-haskell \
4444
&& stack build --only-snapshot
4545

46+
ADD deps/k/pom.xml /home/user/.tmp-maven/
47+
ADD deps/k/ktree/pom.xml /home/user/.tmp-maven/ktree/
48+
ADD deps/k/llvm-backend/pom.xml /home/user/.tmp-maven/llvm-backend/
49+
ADD deps/k/llvm-backend/src/main/native/llvm-backend/matching/pom.xml /home/user/.tmp-maven/llvm-backend/src/main/native/llvm-backend/matching/
50+
ADD deps/k/haskell-backend/pom.xml /home/user/.tmp-maven/haskell-backend/
51+
ADD deps/k/ocaml-backend/pom.xml /home/user/.tmp-maven/ocaml-backend/
52+
ADD deps/k/kernel/pom.xml /home/user/.tmp-maven/kernel/
53+
ADD deps/k/java-backend/pom.xml /home/user/.tmp-maven/java-backend/
54+
ADD deps/k/k-distribution/pom.xml /home/user/.tmp-maven/k-distribution/
55+
ADD deps/k/kore/pom.xml /home/user/.tmp-maven/kore/
56+
RUN cd /home/user/.tmp-maven \
57+
&& mvn dependency:go-offline
58+
4659
ENV LD_LIBRARY_PATH=/usr/local/lib
4760
ENV PATH=/home/user/.local/bin:/home/user/.cargo/bin:$PATH

‎Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -175,7 +175,7 @@ concrete_tangle:=.k:not(.node):not(.symbolic),.standalone,.concrete
175175
symbolic_tangle:=.k:not(.node):not(.concrete),.standalone,.symbolic
176176
node_tangle:=.k:not(.standalone):not(.symbolic),.node,.concrete
177177

178-
k_files=driver.k data.k network.k evm.k krypto.k edsl.k evm-node.k web3.k
178+
k_files=driver.k data.k network.k evm.k krypto.k edsl.k evm-node.k web3.k asm.k
179179
EXTRA_K_FILES+=$(MAIN_DEFN_FILE).k
180180
ALL_K_FILES:=$(k_files) $(EXTRA_K_FILES)
181181

‎asm.md

Lines changed: 189 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,189 @@
1+
Ethereum Assembler
2+
==================
3+
4+
This file contains an assembler from EVM opcodes to byte strings.
5+
6+
Note that due to the design of EVM, which depends on the binary representation of a smart contract, it is **not** the case that disassembling and then reassembling the same contract will yield the same sequence of bytes.
7+
As a simple counterexample, consider the contract `0x60`.
8+
Disassembling and then reassembling this contract will yield `0x6000`.
9+
10+
As such, assembly is not considered part of the semantics of EVM, but is provided merely as a sample implementation to ease readability and make it easier to write inputs to the KEVM semantics.
11+
12+
```k
13+
module EVM-ASSEMBLY
14+
imports EVM
15+
16+
syntax OpCode ::= PUSH(Int, Int) [klabel(PUSHAsm)]
17+
// --------------------------------------------------
18+
19+
syntax ByteArray ::= #asmOpCodes ( OpCodes ) [function]
20+
// -------------------------------------------------------
21+
```
22+
23+
```{.k .symbolic}
24+
syntax ByteArray ::= #asmOpCodes ( OpCodes, ByteArray ) [function, klabel(#asmOpCodesAux)]
25+
// ------------------------------------------------------------------------------------------
26+
rule #asmOpCodes( OPS ) => #asmOpCodes(#revOps(OPS), .ByteArray)
27+
28+
rule #asmOpCodes( PUSH(N, W) ; OCS, WS ) => #asmOpCodes(OCS, #asmOpCode(PUSH(N)) : {#padToWidth(N, #asByteStack(W)) ++ WS}:>WordStack)
29+
rule #asmOpCodes( OP ; OCS, WS ) => #asmOpCodes(OCS, #asmOpCode(OP) : WS) requires PUSH(_, _) :/=K OP
30+
rule #asmOpCodes( .OpCodes, WS ) => WS
31+
```
32+
33+
```{.k .concrete}
34+
syntax ByteArray ::= #asmOpCodes ( OpCodes, StringBuffer ) [function, klabel(#asmOpCodesAux)]
35+
// ---------------------------------------------------------------------------------------------
36+
rule #asmOpCodes( OPS ) => #asmOpCodes(OPS, .StringBuffer)
37+
38+
rule #asmOpCodes( PUSH(N, W) ; OCS, SB ) => #asmOpCodes(OCS, (SB +String chrChar(#asmOpCode(PUSH(N)))) +String Bytes2String(Int2Bytes(N, W, BE)))
39+
rule #asmOpCodes( OP ; OCS, SB ) => #asmOpCodes(OCS, SB +String chrChar(#asmOpCode(OP))) [owise]
40+
rule #asmOpCodes( .OpCodes, SB ) => String2Bytes(StringBuffer2String(SB))
41+
```
42+
43+
```k
44+
syntax Int ::= #asmOpCode ( OpCode ) [function]
45+
// -----------------------------------------------
46+
rule #asmOpCode( STOP ) => 0
47+
rule #asmOpCode( ADD ) => 1
48+
rule #asmOpCode( MUL ) => 2
49+
rule #asmOpCode( SUB ) => 3
50+
rule #asmOpCode( DIV ) => 4
51+
rule #asmOpCode( SDIV ) => 5
52+
rule #asmOpCode( MOD ) => 6
53+
rule #asmOpCode( SMOD ) => 7
54+
rule #asmOpCode( ADDMOD ) => 8
55+
rule #asmOpCode( MULMOD ) => 9
56+
rule #asmOpCode( EXP ) => 10
57+
rule #asmOpCode( SIGNEXTEND ) => 11
58+
rule #asmOpCode( LT ) => 16
59+
rule #asmOpCode( GT ) => 17
60+
rule #asmOpCode( SLT ) => 18
61+
rule #asmOpCode( SGT ) => 19
62+
rule #asmOpCode( EQ ) => 20
63+
rule #asmOpCode( ISZERO ) => 21
64+
rule #asmOpCode( AND ) => 22
65+
rule #asmOpCode( EVMOR ) => 23
66+
rule #asmOpCode( XOR ) => 24
67+
rule #asmOpCode( NOT ) => 25
68+
rule #asmOpCode( BYTE ) => 26
69+
rule #asmOpCode( SHL ) => 27
70+
rule #asmOpCode( SHR ) => 28
71+
rule #asmOpCode( SAR ) => 29
72+
rule #asmOpCode( SHA3 ) => 32
73+
rule #asmOpCode( ADDRESS ) => 48
74+
rule #asmOpCode( BALANCE ) => 49
75+
rule #asmOpCode( ORIGIN ) => 50
76+
rule #asmOpCode( CALLER ) => 51
77+
rule #asmOpCode( CALLVALUE ) => 52
78+
rule #asmOpCode( CALLDATALOAD ) => 53
79+
rule #asmOpCode( CALLDATASIZE ) => 54
80+
rule #asmOpCode( CALLDATACOPY ) => 55
81+
rule #asmOpCode( CODESIZE ) => 56
82+
rule #asmOpCode( CODECOPY ) => 57
83+
rule #asmOpCode( GASPRICE ) => 58
84+
rule #asmOpCode( EXTCODESIZE ) => 59
85+
rule #asmOpCode( EXTCODECOPY ) => 60
86+
rule #asmOpCode( RETURNDATASIZE ) => 61
87+
rule #asmOpCode( RETURNDATACOPY ) => 62
88+
rule #asmOpCode( EXTCODEHASH ) => 63
89+
rule #asmOpCode( BLOCKHASH ) => 64
90+
rule #asmOpCode( COINBASE ) => 65
91+
rule #asmOpCode( TIMESTAMP ) => 66
92+
rule #asmOpCode( NUMBER ) => 67
93+
rule #asmOpCode( DIFFICULTY ) => 68
94+
rule #asmOpCode( GASLIMIT ) => 69
95+
rule #asmOpCode( POP ) => 80
96+
rule #asmOpCode( MLOAD ) => 81
97+
rule #asmOpCode( MSTORE ) => 82
98+
rule #asmOpCode( MSTORE8 ) => 83
99+
rule #asmOpCode( SLOAD ) => 84
100+
rule #asmOpCode( SSTORE ) => 85
101+
rule #asmOpCode( JUMP ) => 86
102+
rule #asmOpCode( JUMPI ) => 87
103+
rule #asmOpCode( PC ) => 88
104+
rule #asmOpCode( MSIZE ) => 89
105+
rule #asmOpCode( GAS ) => 90
106+
rule #asmOpCode( JUMPDEST ) => 91
107+
rule #asmOpCode( PUSH(1) ) => 96
108+
rule #asmOpCode( PUSH(2) ) => 97
109+
rule #asmOpCode( PUSH(3) ) => 98
110+
rule #asmOpCode( PUSH(4) ) => 99
111+
rule #asmOpCode( PUSH(5) ) => 100
112+
rule #asmOpCode( PUSH(6) ) => 101
113+
rule #asmOpCode( PUSH(7) ) => 102
114+
rule #asmOpCode( PUSH(8) ) => 103
115+
rule #asmOpCode( PUSH(9) ) => 104
116+
rule #asmOpCode( PUSH(10) ) => 105
117+
rule #asmOpCode( PUSH(11) ) => 106
118+
rule #asmOpCode( PUSH(12) ) => 107
119+
rule #asmOpCode( PUSH(13) ) => 108
120+
rule #asmOpCode( PUSH(14) ) => 109
121+
rule #asmOpCode( PUSH(15) ) => 110
122+
rule #asmOpCode( PUSH(16) ) => 111
123+
rule #asmOpCode( PUSH(17) ) => 112
124+
rule #asmOpCode( PUSH(18) ) => 113
125+
rule #asmOpCode( PUSH(19) ) => 114
126+
rule #asmOpCode( PUSH(20) ) => 115
127+
rule #asmOpCode( PUSH(21) ) => 116
128+
rule #asmOpCode( PUSH(22) ) => 117
129+
rule #asmOpCode( PUSH(23) ) => 118
130+
rule #asmOpCode( PUSH(24) ) => 119
131+
rule #asmOpCode( PUSH(25) ) => 120
132+
rule #asmOpCode( PUSH(26) ) => 121
133+
rule #asmOpCode( PUSH(27) ) => 122
134+
rule #asmOpCode( PUSH(28) ) => 123
135+
rule #asmOpCode( PUSH(29) ) => 124
136+
rule #asmOpCode( PUSH(30) ) => 125
137+
rule #asmOpCode( PUSH(31) ) => 126
138+
rule #asmOpCode( PUSH(32) ) => 127
139+
rule #asmOpCode( DUP(1) ) => 128
140+
rule #asmOpCode( DUP(2) ) => 129
141+
rule #asmOpCode( DUP(3) ) => 130
142+
rule #asmOpCode( DUP(4) ) => 131
143+
rule #asmOpCode( DUP(5) ) => 132
144+
rule #asmOpCode( DUP(6) ) => 133
145+
rule #asmOpCode( DUP(7) ) => 134
146+
rule #asmOpCode( DUP(8) ) => 135
147+
rule #asmOpCode( DUP(9) ) => 136
148+
rule #asmOpCode( DUP(10) ) => 137
149+
rule #asmOpCode( DUP(11) ) => 138
150+
rule #asmOpCode( DUP(12) ) => 139
151+
rule #asmOpCode( DUP(13) ) => 140
152+
rule #asmOpCode( DUP(14) ) => 141
153+
rule #asmOpCode( DUP(15) ) => 142
154+
rule #asmOpCode( DUP(16) ) => 143
155+
rule #asmOpCode( SWAP(1) ) => 144
156+
rule #asmOpCode( SWAP(2) ) => 145
157+
rule #asmOpCode( SWAP(3) ) => 146
158+
rule #asmOpCode( SWAP(4) ) => 147
159+
rule #asmOpCode( SWAP(5) ) => 148
160+
rule #asmOpCode( SWAP(6) ) => 149
161+
rule #asmOpCode( SWAP(7) ) => 150
162+
rule #asmOpCode( SWAP(8) ) => 151
163+
rule #asmOpCode( SWAP(9) ) => 152
164+
rule #asmOpCode( SWAP(10) ) => 153
165+
rule #asmOpCode( SWAP(11) ) => 154
166+
rule #asmOpCode( SWAP(12) ) => 155
167+
rule #asmOpCode( SWAP(13) ) => 156
168+
rule #asmOpCode( SWAP(14) ) => 157
169+
rule #asmOpCode( SWAP(15) ) => 158
170+
rule #asmOpCode( SWAP(16) ) => 159
171+
rule #asmOpCode( LOG(0) ) => 160
172+
rule #asmOpCode( LOG(1) ) => 161
173+
rule #asmOpCode( LOG(2) ) => 162
174+
rule #asmOpCode( LOG(3) ) => 163
175+
rule #asmOpCode( LOG(4) ) => 164
176+
rule #asmOpCode( CREATE ) => 240
177+
rule #asmOpCode( CALL ) => 241
178+
rule #asmOpCode( CALLCODE ) => 242
179+
rule #asmOpCode( RETURN ) => 243
180+
rule #asmOpCode( DELEGATECALL ) => 244
181+
rule #asmOpCode( CREATE2 ) => 245
182+
rule #asmOpCode( STATICCALL ) => 250
183+
rule #asmOpCode( REVERT ) => 253
184+
rule #asmOpCode( INVALID ) => 254
185+
rule #asmOpCode( SELFDESTRUCT ) => 255
186+
rule #asmOpCode( UNDEFINED(W) ) => W
187+
188+
endmodule
189+
```

‎deps/k

Submodule k updated from 824ffc8 to 677104b

‎driver.md

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,11 @@ requires "evm-node.k"
1010

1111
```k
1212
requires "evm.k"
13+
requires "asm.k"
1314
1415
module ETHEREUM-SIMULATION
1516
imports EVM
17+
imports EVM-ASSEMBLY
1618
```
1719

1820
```{.k .node}
@@ -508,7 +510,7 @@ Here we load the environmental information.
508510
rule <k> load "exec" : { "data" : ((DATA:String) => #parseByteStack(DATA)) } ... </k>
509511
// -------------------------------------------------------------------------------------
510512
rule <k> load "exec" : { "data" : (DATA:ByteArray) } => . ... </k> <callData> _ => DATA </callData>
511-
rule <k> load "exec" : { "code" : (CODE:OpCodes) } => . ... </k> <program> _ => #asMapOpCodes(CODE) </program>
513+
rule <k> load "exec" : { "code" : (CODE:OpCodes) } => . ... </k> <program> _ => #asMapOpCodes(#dasmOpCodes(#asmOpCodes(CODE), SCHED)) </program> <programBytes> _ => #asmOpCodes(CODE) </programBytes> <schedule> SCHED </schedule>
512514
rule <k> load "exec" : { "code" : (CODE:ByteArray) } => . ... </k> <program> _ => #asMapOpCodes(#dasmOpCodes(CODE, SCHED)) </program> <programBytes> _ => CODE </programBytes> <schedule> SCHED </schedule>
513515
```
514516

0 commit comments

Comments
 (0)