vm.fail
an intermediate symbolic execution engine for EVM bytecode
1.2 kB
56 lines
1# symevm
2
3symbolic EVM implin Haskell for smart contract analysis/ equivalence checking and verification that tracks path constraints through JUMPI branches, maintains symbolic state (stack, memory, storage) and has constraint analysis of contract behavior
4
5## Usage
6
7```haskell
8import SymbolicExpression
9import SymbolicState
10import Executor
11import qualified Data.ByteString as BS
12
13let bytecode = BS.pack [0x33, 0x61, 0x12, 0x34, 0x14, 0x60, 0x0b, 0x57, ...]
14let paths = explore bytecode (initState BS.empty) 1000
15
16mapM_ analyzeConstraints paths
17```
18
19**Single path execution**:
20```haskell
21run :: ByteString -> ExecState -> Int -> [ExecState]
22```
23
24**Path exploration**:
25```haskell
26explore :: ByteString -> ExecState -> Int -> [ExecState]
27```
28## Build
29
30```bash
31cabal build
32cabal run symevm
33```
34
35## Example
36
37```haskell
38let code = BS.pack [
39 0x60, 0x00,
40 0x35,
41 0x60, 0x64,
42 0x11,
43 0x60, 0x0a,
44 0x57,
45 0xfd,
46 0x5b,
47 0x00
48 ]
49
50let paths = explore code (initState BS.empty) 50
51```
52
53Yields 2 paths:
54
55 Path 1: `calldataload(0) > 100` → PC=10, halted
56 Path 2: `calldataload(0) <= 100` → reverted