Skip to content

Commit

Permalink
refactor disassembly (#432)
Browse files Browse the repository at this point in the history 
* 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
  • Loading branch information
dwightguth authored Aug 19, 2019
1 parent 28b1d32 commit 3ed5f6e
Show file tree
Hide file tree
Showing 10 changed files with 338 additions and 73 deletions.
13 changes: 13 additions & 0 deletions Dockerfile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,5 +43,18 @@ ADD --chown=user:user deps/k/haskell-backend/src/main/native/haskell-backend/kor
RUN cd /home/user/.tmp-haskell \
&& stack build --only-snapshot

ADD deps/k/pom.xml /home/user/.tmp-maven/
ADD deps/k/ktree/pom.xml /home/user/.tmp-maven/ktree/
ADD deps/k/llvm-backend/pom.xml /home/user/.tmp-maven/llvm-backend/
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/
ADD deps/k/haskell-backend/pom.xml /home/user/.tmp-maven/haskell-backend/
ADD deps/k/ocaml-backend/pom.xml /home/user/.tmp-maven/ocaml-backend/
ADD deps/k/kernel/pom.xml /home/user/.tmp-maven/kernel/
ADD deps/k/java-backend/pom.xml /home/user/.tmp-maven/java-backend/
ADD deps/k/k-distribution/pom.xml /home/user/.tmp-maven/k-distribution/
ADD deps/k/kore/pom.xml /home/user/.tmp-maven/kore/
RUN cd /home/user/.tmp-maven \
&& mvn dependency:go-offline

ENV LD_LIBRARY_PATH=/usr/local/lib
ENV PATH=/home/user/.local/bin:/home/user/.cargo/bin:$PATH
2 changes: 1 addition & 1 deletion Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -175,7 +175,7 @@ concrete_tangle:=.k:not(.node):not(.symbolic),.standalone,.concrete
symbolic_tangle:=.k:not(.node):not(.concrete),.standalone,.symbolic
node_tangle:=.k:not(.standalone):not(.symbolic),.node,.concrete

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

Expand Down
189 changes: 189 additions & 0 deletions asm.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,189 @@
Ethereum Assembler
==================

This file contains an assembler from EVM opcodes to byte strings.

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.
As a simple counterexample, consider the contract `0x60`.
Disassembling and then reassembling this contract will yield `0x6000`.

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.

```k
module EVM-ASSEMBLY
imports EVM
syntax OpCode ::= PUSH(Int, Int) [klabel(PUSHAsm)]
// --------------------------------------------------
syntax ByteArray ::= #asmOpCodes ( OpCodes ) [function]
// -------------------------------------------------------
```

```{.k .symbolic}
syntax ByteArray ::= #asmOpCodes ( OpCodes, ByteArray ) [function, klabel(#asmOpCodesAux)]
// ------------------------------------------------------------------------------------------
rule #asmOpCodes( OPS ) => #asmOpCodes(#revOps(OPS), .ByteArray)
rule #asmOpCodes( PUSH(N, W) ; OCS, WS ) => #asmOpCodes(OCS, #asmOpCode(PUSH(N)) : {#padToWidth(N, #asByteStack(W)) ++ WS}:>WordStack)
rule #asmOpCodes( OP ; OCS, WS ) => #asmOpCodes(OCS, #asmOpCode(OP) : WS) requires PUSH(_, _) :/=K OP
rule #asmOpCodes( .OpCodes, WS ) => WS
```

```{.k .concrete}
syntax ByteArray ::= #asmOpCodes ( OpCodes, StringBuffer ) [function, klabel(#asmOpCodesAux)]
// ---------------------------------------------------------------------------------------------
rule #asmOpCodes( OPS ) => #asmOpCodes(OPS, .StringBuffer)
rule #asmOpCodes( PUSH(N, W) ; OCS, SB ) => #asmOpCodes(OCS, (SB +String chrChar(#asmOpCode(PUSH(N)))) +String Bytes2String(Int2Bytes(N, W, BE)))
rule #asmOpCodes( OP ; OCS, SB ) => #asmOpCodes(OCS, SB +String chrChar(#asmOpCode(OP))) [owise]
rule #asmOpCodes( .OpCodes, SB ) => String2Bytes(StringBuffer2String(SB))
```

```k
syntax Int ::= #asmOpCode ( OpCode ) [function]
// -----------------------------------------------
rule #asmOpCode( STOP ) => 0
rule #asmOpCode( ADD ) => 1
rule #asmOpCode( MUL ) => 2
rule #asmOpCode( SUB ) => 3
rule #asmOpCode( DIV ) => 4
rule #asmOpCode( SDIV ) => 5
rule #asmOpCode( MOD ) => 6
rule #asmOpCode( SMOD ) => 7
rule #asmOpCode( ADDMOD ) => 8
rule #asmOpCode( MULMOD ) => 9
rule #asmOpCode( EXP ) => 10
rule #asmOpCode( SIGNEXTEND ) => 11
rule #asmOpCode( LT ) => 16
rule #asmOpCode( GT ) => 17
rule #asmOpCode( SLT ) => 18
rule #asmOpCode( SGT ) => 19
rule #asmOpCode( EQ ) => 20
rule #asmOpCode( ISZERO ) => 21
rule #asmOpCode( AND ) => 22
rule #asmOpCode( EVMOR ) => 23
rule #asmOpCode( XOR ) => 24
rule #asmOpCode( NOT ) => 25
rule #asmOpCode( BYTE ) => 26
rule #asmOpCode( SHL ) => 27
rule #asmOpCode( SHR ) => 28
rule #asmOpCode( SAR ) => 29
rule #asmOpCode( SHA3 ) => 32
rule #asmOpCode( ADDRESS ) => 48
rule #asmOpCode( BALANCE ) => 49
rule #asmOpCode( ORIGIN ) => 50
rule #asmOpCode( CALLER ) => 51
rule #asmOpCode( CALLVALUE ) => 52
rule #asmOpCode( CALLDATALOAD ) => 53
rule #asmOpCode( CALLDATASIZE ) => 54
rule #asmOpCode( CALLDATACOPY ) => 55
rule #asmOpCode( CODESIZE ) => 56
rule #asmOpCode( CODECOPY ) => 57
rule #asmOpCode( GASPRICE ) => 58
rule #asmOpCode( EXTCODESIZE ) => 59
rule #asmOpCode( EXTCODECOPY ) => 60
rule #asmOpCode( RETURNDATASIZE ) => 61
rule #asmOpCode( RETURNDATACOPY ) => 62
rule #asmOpCode( EXTCODEHASH ) => 63
rule #asmOpCode( BLOCKHASH ) => 64
rule #asmOpCode( COINBASE ) => 65
rule #asmOpCode( TIMESTAMP ) => 66
rule #asmOpCode( NUMBER ) => 67
rule #asmOpCode( DIFFICULTY ) => 68
rule #asmOpCode( GASLIMIT ) => 69
rule #asmOpCode( POP ) => 80
rule #asmOpCode( MLOAD ) => 81
rule #asmOpCode( MSTORE ) => 82
rule #asmOpCode( MSTORE8 ) => 83
rule #asmOpCode( SLOAD ) => 84
rule #asmOpCode( SSTORE ) => 85
rule #asmOpCode( JUMP ) => 86
rule #asmOpCode( JUMPI ) => 87
rule #asmOpCode( PC ) => 88
rule #asmOpCode( MSIZE ) => 89
rule #asmOpCode( GAS ) => 90
rule #asmOpCode( JUMPDEST ) => 91
rule #asmOpCode( PUSH(1) ) => 96
rule #asmOpCode( PUSH(2) ) => 97
rule #asmOpCode( PUSH(3) ) => 98
rule #asmOpCode( PUSH(4) ) => 99
rule #asmOpCode( PUSH(5) ) => 100
rule #asmOpCode( PUSH(6) ) => 101
rule #asmOpCode( PUSH(7) ) => 102
rule #asmOpCode( PUSH(8) ) => 103
rule #asmOpCode( PUSH(9) ) => 104
rule #asmOpCode( PUSH(10) ) => 105
rule #asmOpCode( PUSH(11) ) => 106
rule #asmOpCode( PUSH(12) ) => 107
rule #asmOpCode( PUSH(13) ) => 108
rule #asmOpCode( PUSH(14) ) => 109
rule #asmOpCode( PUSH(15) ) => 110
rule #asmOpCode( PUSH(16) ) => 111
rule #asmOpCode( PUSH(17) ) => 112
rule #asmOpCode( PUSH(18) ) => 113
rule #asmOpCode( PUSH(19) ) => 114
rule #asmOpCode( PUSH(20) ) => 115
rule #asmOpCode( PUSH(21) ) => 116
rule #asmOpCode( PUSH(22) ) => 117
rule #asmOpCode( PUSH(23) ) => 118
rule #asmOpCode( PUSH(24) ) => 119
rule #asmOpCode( PUSH(25) ) => 120
rule #asmOpCode( PUSH(26) ) => 121
rule #asmOpCode( PUSH(27) ) => 122
rule #asmOpCode( PUSH(28) ) => 123
rule #asmOpCode( PUSH(29) ) => 124
rule #asmOpCode( PUSH(30) ) => 125
rule #asmOpCode( PUSH(31) ) => 126
rule #asmOpCode( PUSH(32) ) => 127
rule #asmOpCode( DUP(1) ) => 128
rule #asmOpCode( DUP(2) ) => 129
rule #asmOpCode( DUP(3) ) => 130
rule #asmOpCode( DUP(4) ) => 131
rule #asmOpCode( DUP(5) ) => 132
rule #asmOpCode( DUP(6) ) => 133
rule #asmOpCode( DUP(7) ) => 134
rule #asmOpCode( DUP(8) ) => 135
rule #asmOpCode( DUP(9) ) => 136
rule #asmOpCode( DUP(10) ) => 137
rule #asmOpCode( DUP(11) ) => 138
rule #asmOpCode( DUP(12) ) => 139
rule #asmOpCode( DUP(13) ) => 140
rule #asmOpCode( DUP(14) ) => 141
rule #asmOpCode( DUP(15) ) => 142
rule #asmOpCode( DUP(16) ) => 143
rule #asmOpCode( SWAP(1) ) => 144
rule #asmOpCode( SWAP(2) ) => 145
rule #asmOpCode( SWAP(3) ) => 146
rule #asmOpCode( SWAP(4) ) => 147
rule #asmOpCode( SWAP(5) ) => 148
rule #asmOpCode( SWAP(6) ) => 149
rule #asmOpCode( SWAP(7) ) => 150
rule #asmOpCode( SWAP(8) ) => 151
rule #asmOpCode( SWAP(9) ) => 152
rule #asmOpCode( SWAP(10) ) => 153
rule #asmOpCode( SWAP(11) ) => 154
rule #asmOpCode( SWAP(12) ) => 155
rule #asmOpCode( SWAP(13) ) => 156
rule #asmOpCode( SWAP(14) ) => 157
rule #asmOpCode( SWAP(15) ) => 158
rule #asmOpCode( SWAP(16) ) => 159
rule #asmOpCode( LOG(0) ) => 160
rule #asmOpCode( LOG(1) ) => 161
rule #asmOpCode( LOG(2) ) => 162
rule #asmOpCode( LOG(3) ) => 163
rule #asmOpCode( LOG(4) ) => 164
rule #asmOpCode( CREATE ) => 240
rule #asmOpCode( CALL ) => 241
rule #asmOpCode( CALLCODE ) => 242
rule #asmOpCode( RETURN ) => 243
rule #asmOpCode( DELEGATECALL ) => 244
rule #asmOpCode( CREATE2 ) => 245
rule #asmOpCode( STATICCALL ) => 250
rule #asmOpCode( REVERT ) => 253
rule #asmOpCode( INVALID ) => 254
rule #asmOpCode( SELFDESTRUCT ) => 255
rule #asmOpCode( UNDEFINED(W) ) => W
endmodule
```
2 changes: 1 addition & 1 deletion deps/k
Submodule k updated from 824ffc to 677104
4 changes: 3 additions & 1 deletion driver.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,11 @@ requires "evm-node.k"

```k
requires "evm.k"
requires "asm.k"
module ETHEREUM-SIMULATION
imports EVM
imports EVM-ASSEMBLY
```

```{.k .node}
Expand Down Expand Up @@ -508,7 +510,7 @@ Here we load the environmental information.
rule <k> load "exec" : { "data" : ((DATA:String) => #parseByteStack(DATA)) } ... </k>
// -------------------------------------------------------------------------------------
rule <k> load "exec" : { "data" : (DATA:ByteArray) } => . ... </k> <callData> _ => DATA </callData>
rule <k> load "exec" : { "code" : (CODE:OpCodes) } => . ... </k> <program> _ => #asMapOpCodes(CODE) </program>
rule <k> load "exec" : { "code" : (CODE:OpCodes) } => . ... </k> <program> _ => #asMapOpCodes(#dasmOpCodes(#asmOpCodes(CODE), SCHED)) </program> <programBytes> _ => #asmOpCodes(CODE) </programBytes> <schedule> SCHED </schedule>
rule <k> load "exec" : { "code" : (CODE:ByteArray) } => . ... </k> <program> _ => #asMapOpCodes(#dasmOpCodes(CODE, SCHED)) </program> <programBytes> _ => CODE </programBytes> <schedule> SCHED </schedule>
```

Expand Down
Loading

0 comments on commit 3ed5f6e

Please sign in to comment.