an intermediate symbolic execution engine for EVM bytecode
initial commit
author
vm.fail
date
(Jan 20, 2026, 11:26 PM UTC)
commit
c5e349d7
c5e349d7afaf687eb5ee9507e7ebc0c564f09c3c
vm.fail
date
(Jan 20, 2026, 11:26 PM UTC)
commit
c5e349d7
c5e349d7afaf687eb5ee9507e7ebc0c564f09c3c
+963
+56
README.md
+56
README.md
···
1
+
# symevm
2
+
3
+
symbolic 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
8
+
import SymbolicExpression
9
+
import SymbolicState
10
+
import Executor
11
+
import qualified Data.ByteString as BS
12
+
13
+
let bytecode = BS.pack [0x33, 0x61, 0x12, 0x34, 0x14, 0x60, 0x0b, 0x57, ...]
14
+
let paths = explore bytecode (initState BS.empty) 1000
15
+
16
+
mapM_ analyzeConstraints paths
17
+
```
18
+
19
+
**Single path execution**:
20
+
```haskell
21
+
run :: ByteString -> ExecState -> Int -> [ExecState]
22
+
```
23
+
24
+
**Path exploration**:
25
+
```haskell
26
+
explore :: ByteString -> ExecState -> Int -> [ExecState]
27
+
```
28
+
## Build
29
+
30
+
```bash
31
+
cabal build
32
+
cabal run symevm
33
+
```
34
+
35
+
## Example
36
+
37
+
```haskell
38
+
let 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
+
50
+
let paths = explore code (initState BS.empty) 50
51
+
```
52
+
53
+
Yields 2 paths:
54
+
55
+
Path 1: `calldataload(0) > 100` → PC=10, halted
56
+
Path 2: `calldataload(0) <= 100` → reverted
+60
app/Main.hs
+60
app/Main.hs
···
1
+
module Main where
2
+
3
+
import SymbolicExpression
4
+
import SymbolicState
5
+
import Executor
6
+
import qualified Data.ByteString as BS
7
+
import qualified Data.Map.Strict as Map
8
+
9
+
main :: IO ()
10
+
main = do
11
+
let bytecode = BS.pack
12
+
[ 0x33
13
+
, 0x61, 0x12, 0x34
14
+
, 0x14
15
+
, 0x60, 0x0b
16
+
, 0x57
17
+
, 0x60, 0xc8
18
+
, 0x60, 0x0f
19
+
, 0x56
20
+
, 0x5b
21
+
, 0x60, 0x64
22
+
, 0x5b
23
+
, 0x00
24
+
]
25
+
26
+
let results = explore bytecode (initState BS.empty) 50
27
+
28
+
putStrLn $ "Paths: " ++ show (length results)
29
+
mapM_ printResult results
30
+
31
+
printResult :: ExecState -> IO ()
32
+
printResult state = do
33
+
putStrLn ""
34
+
putStrLn $ "PC: " ++ show (pc state)
35
+
putStrLn $ "Halted: " ++ show (halted state)
36
+
putStrLn $ "Reverted: " ++ show (reverted state)
37
+
38
+
let SymStack stackItems = stack state
39
+
when (not $ null stackItems) $ do
40
+
putStrLn "Stack:"
41
+
mapM_ (\(i, expr) -> putStrLn $ " [" ++ show i ++ "] " ++ prettyExpr expr)
42
+
(zip [0..] stackItems)
43
+
44
+
let SymStorage stor = storage state
45
+
when (not $ null $ Map.toList stor) $ do
46
+
putStrLn "Storage:"
47
+
mapM_ (\(k, v) -> putStrLn $ " " ++ prettyExpr k ++ " => " ++ prettyExpr v)
48
+
(Map.toList stor)
49
+
50
+
when (not $ null $ constraints state) $ do
51
+
putStrLn "Constraints:"
52
+
mapM_ (\c -> putStrLn $ " " ++ prettyConstraint c) (reverse $ constraints state)
53
+
54
+
case returnData state of
55
+
Just val -> putStrLn $ "Return: " ++ prettyExpr val
56
+
Nothing -> return ()
57
+
58
+
when :: Bool -> IO () -> IO ()
59
+
when True action = action
60
+
when False _ = return ()
+223
src/Executor.hs
+223
src/Executor.hs
···
1
+
{-# LANGUAGE LambdaCase #-}
2
+
3
+
module Executor where
4
+
5
+
import SymbolicExpression
6
+
import SymbolicState
7
+
import Opcode
8
+
import Data.ByteString (ByteString)
9
+
import qualified Data.ByteString as BS
10
+
import Data.Maybe (fromMaybe)
11
+
import Control.Monad (foldM)
12
+
import Prelude hiding (LT, GT, EQ)
13
+
14
+
data StepResult
15
+
= Continue ExecState
16
+
| Branch ExecState ExecState
17
+
| Halt ExecState
18
+
| Error String
19
+
deriving (Show)
20
+
21
+
executeOpcode :: ByteString -> Opcode -> ExecState -> StepResult
22
+
executeOpcode code op state = case op of
23
+
ADD -> binOp mkAdd state
24
+
MUL -> binOp mkMul state
25
+
SUB -> binOp mkSub state
26
+
DIV -> binOp mkDiv state
27
+
MOD -> binOp mkMod state
28
+
29
+
LT -> binOp mkLt state
30
+
GT -> binOp mkGt state
31
+
EQ -> binOp mkEq state
32
+
ISZERO -> unOp mkIsZero state
33
+
34
+
AND -> binOp mkAnd state
35
+
OR -> binOp mkOr state
36
+
XOR -> binOp mkXor state
37
+
NOT -> unOp mkNot state
38
+
39
+
POP -> case popStack (stack state) of
40
+
Just (_, s') -> Continue state { stack = s', pc = pc state + 1 }
41
+
Nothing -> Error "Stack underflow"
42
+
43
+
_ | Just n <- dupDepth op -> case dupStack n (stack state) of
44
+
Just s' -> Continue state { stack = s', pc = pc state + 1 }
45
+
Nothing -> Error "Stack underflow on DUP"
46
+
47
+
_ | Just n <- swapDepth op -> case swapStack n (stack state) of
48
+
Just s' -> Continue state { stack = s', pc = pc state + 1 }
49
+
Nothing -> Error "Stack underflow on SWAP"
50
+
51
+
MLOAD -> case popStack (stack state) of
52
+
Just (offset, s') ->
53
+
let value = case offset of
54
+
Concrete n -> mload n (memory state)
55
+
_ -> Symbolic "mload" (symbolicId state)
56
+
state' = state { symbolicId = symbolicId state + 1 }
57
+
in case pushStack value s' of
58
+
Just s'' -> Continue state' { stack = s'', pc = pc state' + 1 }
59
+
Nothing -> Error "Stack overflow"
60
+
Nothing -> Error "Stack underflow"
61
+
62
+
MSTORE -> case popStackN 2 (stack state) of
63
+
Just ([offset, value], s') ->
64
+
let mem' = case offset of
65
+
Concrete n -> mstore n value (memory state)
66
+
_ -> memory state
67
+
in Continue state { stack = s', memory = mem', pc = pc state + 1 }
68
+
_ -> Error "Stack underflow"
69
+
70
+
MSTORE8 -> case popStackN 2 (stack state) of
71
+
Just ([offset, value], s') ->
72
+
let mem' = case offset of
73
+
Concrete n -> mstore8 n value (memory state)
74
+
_ -> memory state
75
+
in Continue state { stack = s', memory = mem', pc = pc state + 1 }
76
+
_ -> Error "Stack underflow"
77
+
78
+
SLOAD -> case popStack (stack state) of
79
+
Just (key, s') ->
80
+
let value = sload key (storage state)
81
+
in case pushStack value s' of
82
+
Just s'' -> Continue state { stack = s'', pc = pc state + 1 }
83
+
Nothing -> Error "Stack overflow"
84
+
Nothing -> Error "Stack underflow"
85
+
86
+
SSTORE -> case popStackN 2 (stack state) of
87
+
Just ([key, value], s') ->
88
+
let stor' = sstore key value (storage state)
89
+
in Continue state { stack = s', storage = stor', pc = pc state + 1 }
90
+
_ -> Error "Stack underflow"
91
+
92
+
JUMP -> case popStack (stack state) of
93
+
Just (Concrete dest, s') ->
94
+
Continue state { stack = s', pc = fromInteger dest }
95
+
Just (_, _) -> Error "Symbolic jump destination not supported"
96
+
Nothing -> Error "Stack underflow"
97
+
98
+
JUMPI -> case popStackN 2 (stack state) of
99
+
Just ([Concrete dest, cond], s') ->
100
+
let trueBranch = addConstraint (CTrue cond) $
101
+
state { stack = s', pc = fromInteger dest }
102
+
falseBranch = addConstraint (CFalse cond) $
103
+
state { stack = s', pc = pc state + 1 }
104
+
in case cond of
105
+
Concrete 0 -> Continue falseBranch
106
+
Concrete _ -> Continue trueBranch
107
+
_ -> Branch trueBranch falseBranch
108
+
Just ([_, cond], s') -> Error "Symbolic jump destination not supported"
109
+
_ -> Error "Stack underflow"
110
+
111
+
JUMPDEST -> Continue state { pc = pc state + 1 }
112
+
113
+
PC -> case pushStack (Concrete $ fromIntegral $ pc state) (stack state) of
114
+
Just s' -> Continue state { stack = s', pc = pc state + 1 }
115
+
Nothing -> Error "Stack overflow"
116
+
117
+
CALLER -> case pushStack Caller (stack state) of
118
+
Just s' -> Continue state { stack = s', pc = pc state + 1 }
119
+
Nothing -> Error "Stack overflow"
120
+
121
+
CALLVALUE -> case pushStack CallValue (stack state) of
122
+
Just s' -> Continue state { stack = s', pc = pc state + 1 }
123
+
Nothing -> Error "Stack overflow"
124
+
125
+
CALLDATALOAD -> case popStack (stack state) of
126
+
Just (offset, s') ->
127
+
let value = case offset of
128
+
Concrete n -> loadCalldata (calldata state) n
129
+
_ -> CallDataLoad offset
130
+
in case pushStack value s' of
131
+
Just s'' -> Continue state { stack = s'', pc = pc state + 1 }
132
+
Nothing -> Error "Stack overflow"
133
+
Nothing -> Error "Stack underflow"
134
+
135
+
CALLDATASIZE -> case pushStack CallDataSize (stack state) of
136
+
Just s' -> Continue state { stack = s', pc = pc state + 1 }
137
+
Nothing -> Error "Stack overflow"
138
+
139
+
STOP -> Halt state { halted = True }
140
+
141
+
RETURN -> case popStackN 2 (stack state) of
142
+
Just ([offset, size], s') ->
143
+
let retVal = case (offset, size) of
144
+
(Concrete o, Concrete s) -> mload o (memory state)
145
+
_ -> Symbolic "return" (symbolicId state)
146
+
in Halt state { stack = s', returnData = Just retVal, halted = True }
147
+
_ -> Error "Stack underflow"
148
+
149
+
REVERT -> Halt state { reverted = True, halted = True }
150
+
151
+
INVALID -> Halt state { reverted = True, halted = True }
152
+
153
+
_ -> Error $ "Unsupported opcode: " ++ show op
154
+
155
+
binOp :: (SymExpr -> SymExpr -> SymExpr) -> ExecState -> StepResult
156
+
binOp f state = case popStackN 2 (stack state) of
157
+
Just ([a, b], s') ->
158
+
case pushStack (f a b) s' of
159
+
Just s'' -> Continue state { stack = s'', pc = pc state + 1 }
160
+
Nothing -> Error "Stack overflow"
161
+
_ -> Error "Stack underflow"
162
+
163
+
unOp :: (SymExpr -> SymExpr) -> ExecState -> StepResult
164
+
unOp f state = case popStack (stack state) of
165
+
Just (a, s') ->
166
+
case pushStack (f a) s' of
167
+
Just s'' -> Continue state { stack = s'', pc = pc state + 1 }
168
+
Nothing -> Error "Stack overflow"
169
+
Nothing -> Error "Stack underflow"
170
+
171
+
loadCalldata :: ByteString -> Integer -> SymExpr
172
+
loadCalldata cd offset
173
+
| offset >= 0 && offset < fromIntegral (BS.length cd) =
174
+
let bytes = BS.drop (fromInteger offset) cd
175
+
value = foldl (\acc b -> acc * 256 + fromIntegral b) 0 (BS.unpack $ BS.take 32 bytes)
176
+
in Concrete value
177
+
| otherwise = Concrete 0
178
+
179
+
step :: ByteString -> ExecState -> StepResult
180
+
step code state
181
+
| halted state = Halt state
182
+
| pc state < 0 || pc state >= BS.length code = Halt state { halted = True }
183
+
| otherwise =
184
+
let byte = BS.index code (pc state)
185
+
opcode = decodeOpcode byte
186
+
in if isPush opcode
187
+
then
188
+
let n = pushBytes opcode
189
+
value = readBytes code (pc state + 1) n
190
+
in case pushStack (Concrete value) (stack state) of
191
+
Just s' -> Continue state { stack = s', pc = pc state + 1 + n }
192
+
Nothing -> Error "Stack overflow"
193
+
else executeOpcode code opcode state
194
+
195
+
run :: ByteString -> ExecState -> Int -> [ExecState]
196
+
run code state maxSteps = go state 0
197
+
where
198
+
go st n
199
+
| n >= maxSteps = [st]
200
+
| halted st = [st]
201
+
| otherwise = case step code st of
202
+
Continue st' -> go st' (n + 1)
203
+
Halt st' -> [st']
204
+
Branch _ _ -> [st]
205
+
Error msg -> [st { halted = True, reverted = True }]
206
+
207
+
explore :: ByteString -> ExecState -> Int -> [ExecState]
208
+
explore code initialState maxSteps = go [initialState] 0
209
+
where
210
+
go states n
211
+
| n >= maxSteps = states
212
+
| all halted states = states
213
+
| otherwise =
214
+
let states' = concatMap stepOne states
215
+
in go states' (n + 1)
216
+
217
+
stepOne st
218
+
| halted st = [st]
219
+
| otherwise = case step code st of
220
+
Continue st' -> [st']
221
+
Halt st' -> [st']
222
+
Branch st1 st2 -> [st1, st2]
223
+
Error msg -> [st { halted = True, reverted = True }]
+274
src/Opcode.hs
+274
src/Opcode.hs
···
1
+
{-# LANGUAGE LambdaCase #-}
2
+
3
+
module Opcode where
4
+
5
+
import Data.Word
6
+
import Data.ByteString (ByteString)
7
+
import qualified Data.ByteString as BS
8
+
import Prelude hiding (LT, GT, EQ)
9
+
10
+
data Opcode
11
+
= STOP | ADD | MUL | SUB | DIV | SDIV | MOD | SMOD
12
+
| ADDMOD | MULMOD | EXP | SIGNEXTEND
13
+
| LT | GT | SLT | SGT | EQ | ISZERO
14
+
| AND | OR | XOR | NOT | BYTE | SHL | SHR | SAR
15
+
| SHA3
16
+
| ADDRESS | BALANCE | ORIGIN | CALLER | CALLVALUE
17
+
| CALLDATALOAD | CALLDATASIZE | CALLDATACOPY
18
+
| CODESIZE | CODECOPY
19
+
| GASPRICE | EXTCODESIZE | EXTCODECOPY | RETURNDATASIZE | RETURNDATACOPY
20
+
| EXTCODEHASH
21
+
| BLOCKHASH | COINBASE | TIMESTAMP | NUMBER | DIFFICULTY | GASLIMIT
22
+
| CHAINID | SELFBALANCE | BASEFEE
23
+
| POP | MLOAD | MSTORE | MSTORE8 | SLOAD | SSTORE | JUMP | JUMPI
24
+
| PC | MSIZE | GAS | JUMPDEST
25
+
| PUSH1 | PUSH2 | PUSH3 | PUSH4 | PUSH5 | PUSH6 | PUSH7 | PUSH8
26
+
| PUSH9 | PUSH10 | PUSH11 | PUSH12 | PUSH13 | PUSH14 | PUSH15 | PUSH16
27
+
| PUSH17 | PUSH18 | PUSH19 | PUSH20 | PUSH21 | PUSH22 | PUSH23 | PUSH24
28
+
| PUSH25 | PUSH26 | PUSH27 | PUSH28 | PUSH29 | PUSH30 | PUSH31 | PUSH32
29
+
| DUP1 | DUP2 | DUP3 | DUP4 | DUP5 | DUP6 | DUP7 | DUP8
30
+
| DUP9 | DUP10 | DUP11 | DUP12 | DUP13 | DUP14 | DUP15 | DUP16
31
+
| SWAP1 | SWAP2 | SWAP3 | SWAP4 | SWAP5 | SWAP6 | SWAP7 | SWAP8
32
+
| SWAP9 | SWAP10 | SWAP11 | SWAP12 | SWAP13 | SWAP14 | SWAP15 | SWAP16
33
+
| LOG0 | LOG1 | LOG2 | LOG3 | LOG4
34
+
| CREATE | CALL | CALLCODE | RETURN | DELEGATECALL | CREATE2
35
+
| STATICCALL | REVERT | INVALID | SELFDESTRUCT
36
+
| UNKNOWN Word8
37
+
deriving (Show, Eq)
38
+
39
+
decodeOpcode :: Word8 -> Opcode
40
+
decodeOpcode = \case
41
+
0x00 -> STOP
42
+
0x01 -> ADD
43
+
0x02 -> MUL
44
+
0x03 -> SUB
45
+
0x04 -> DIV
46
+
0x05 -> SDIV
47
+
0x06 -> MOD
48
+
0x07 -> SMOD
49
+
0x08 -> ADDMOD
50
+
0x09 -> MULMOD
51
+
0x0a -> EXP
52
+
0x0b -> SIGNEXTEND
53
+
0x10 -> LT
54
+
0x11 -> GT
55
+
0x12 -> SLT
56
+
0x13 -> SGT
57
+
0x14 -> EQ
58
+
0x15 -> ISZERO
59
+
0x16 -> AND
60
+
0x17 -> OR
61
+
0x18 -> XOR
62
+
0x19 -> NOT
63
+
0x1a -> BYTE
64
+
0x1b -> SHL
65
+
0x1c -> SHR
66
+
0x1d -> SAR
67
+
0x20 -> SHA3
68
+
0x30 -> ADDRESS
69
+
0x31 -> BALANCE
70
+
0x32 -> ORIGIN
71
+
0x33 -> CALLER
72
+
0x34 -> CALLVALUE
73
+
0x35 -> CALLDATALOAD
74
+
0x36 -> CALLDATASIZE
75
+
0x37 -> CALLDATACOPY
76
+
0x38 -> CODESIZE
77
+
0x39 -> CODECOPY
78
+
0x3a -> GASPRICE
79
+
0x3b -> EXTCODESIZE
80
+
0x3c -> EXTCODECOPY
81
+
0x3d -> RETURNDATASIZE
82
+
0x3e -> RETURNDATACOPY
83
+
0x3f -> EXTCODEHASH
84
+
0x40 -> BLOCKHASH
85
+
0x41 -> COINBASE
86
+
0x42 -> TIMESTAMP
87
+
0x43 -> NUMBER
88
+
0x44 -> DIFFICULTY
89
+
0x45 -> GASLIMIT
90
+
0x46 -> CHAINID
91
+
0x47 -> SELFBALANCE
92
+
0x48 -> BASEFEE
93
+
0x50 -> POP
94
+
0x51 -> MLOAD
95
+
0x52 -> MSTORE
96
+
0x53 -> MSTORE8
97
+
0x54 -> SLOAD
98
+
0x55 -> SSTORE
99
+
0x56 -> JUMP
100
+
0x57 -> JUMPI
101
+
0x58 -> PC
102
+
0x59 -> MSIZE
103
+
0x5a -> GAS
104
+
0x5b -> JUMPDEST
105
+
0x60 -> PUSH1
106
+
0x61 -> PUSH2
107
+
0x62 -> PUSH3
108
+
0x63 -> PUSH4
109
+
0x64 -> PUSH5
110
+
0x65 -> PUSH6
111
+
0x66 -> PUSH7
112
+
0x67 -> PUSH8
113
+
0x68 -> PUSH9
114
+
0x69 -> PUSH10
115
+
0x6a -> PUSH11
116
+
0x6b -> PUSH12
117
+
0x6c -> PUSH13
118
+
0x6d -> PUSH14
119
+
0x6e -> PUSH15
120
+
0x6f -> PUSH16
121
+
0x70 -> PUSH17
122
+
0x71 -> PUSH18
123
+
0x72 -> PUSH19
124
+
0x73 -> PUSH20
125
+
0x74 -> PUSH21
126
+
0x75 -> PUSH22
127
+
0x76 -> PUSH23
128
+
0x77 -> PUSH24
129
+
0x78 -> PUSH25
130
+
0x79 -> PUSH26
131
+
0x7a -> PUSH27
132
+
0x7b -> PUSH28
133
+
0x7c -> PUSH29
134
+
0x7d -> PUSH30
135
+
0x7e -> PUSH31
136
+
0x7f -> PUSH32
137
+
0x80 -> DUP1
138
+
0x81 -> DUP2
139
+
0x82 -> DUP3
140
+
0x83 -> DUP4
141
+
0x84 -> DUP5
142
+
0x85 -> DUP6
143
+
0x86 -> DUP7
144
+
0x87 -> DUP8
145
+
0x88 -> DUP9
146
+
0x89 -> DUP10
147
+
0x8a -> DUP11
148
+
0x8b -> DUP12
149
+
0x8c -> DUP13
150
+
0x8d -> DUP14
151
+
0x8e -> DUP15
152
+
0x8f -> DUP16
153
+
0x90 -> SWAP1
154
+
0x91 -> SWAP2
155
+
0x92 -> SWAP3
156
+
0x93 -> SWAP4
157
+
0x94 -> SWAP5
158
+
0x95 -> SWAP6
159
+
0x96 -> SWAP7
160
+
0x97 -> SWAP8
161
+
0x98 -> SWAP9
162
+
0x99 -> SWAP10
163
+
0x9a -> SWAP11
164
+
0x9b -> SWAP12
165
+
0x9c -> SWAP13
166
+
0x9d -> SWAP14
167
+
0x9e -> SWAP15
168
+
0x9f -> SWAP16
169
+
0xa0 -> LOG0
170
+
0xa1 -> LOG1
171
+
0xa2 -> LOG2
172
+
0xa3 -> LOG3
173
+
0xa4 -> LOG4
174
+
0xf0 -> CREATE
175
+
0xf1 -> CALL
176
+
0xf2 -> CALLCODE
177
+
0xf3 -> RETURN
178
+
0xf4 -> DELEGATECALL
179
+
0xf5 -> CREATE2
180
+
0xfa -> STATICCALL
181
+
0xfd -> REVERT
182
+
0xfe -> INVALID
183
+
0xff -> SELFDESTRUCT
184
+
b -> UNKNOWN b
185
+
186
+
pushBytes :: Opcode -> Int
187
+
pushBytes PUSH1 = 1
188
+
pushBytes PUSH2 = 2
189
+
pushBytes PUSH3 = 3
190
+
pushBytes PUSH4 = 4
191
+
pushBytes PUSH5 = 5
192
+
pushBytes PUSH6 = 6
193
+
pushBytes PUSH7 = 7
194
+
pushBytes PUSH8 = 8
195
+
pushBytes PUSH9 = 9
196
+
pushBytes PUSH10 = 10
197
+
pushBytes PUSH11 = 11
198
+
pushBytes PUSH12 = 12
199
+
pushBytes PUSH13 = 13
200
+
pushBytes PUSH14 = 14
201
+
pushBytes PUSH15 = 15
202
+
pushBytes PUSH16 = 16
203
+
pushBytes PUSH17 = 17
204
+
pushBytes PUSH18 = 18
205
+
pushBytes PUSH19 = 19
206
+
pushBytes PUSH20 = 20
207
+
pushBytes PUSH21 = 21
208
+
pushBytes PUSH22 = 22
209
+
pushBytes PUSH23 = 23
210
+
pushBytes PUSH24 = 24
211
+
pushBytes PUSH25 = 25
212
+
pushBytes PUSH26 = 26
213
+
pushBytes PUSH27 = 27
214
+
pushBytes PUSH28 = 28
215
+
pushBytes PUSH29 = 29
216
+
pushBytes PUSH30 = 30
217
+
pushBytes PUSH31 = 31
218
+
pushBytes PUSH32 = 32
219
+
pushBytes _ = 0
220
+
221
+
isPush :: Opcode -> Bool
222
+
isPush op = pushBytes op > 0
223
+
224
+
dupDepth :: Opcode -> Maybe Int
225
+
dupDepth DUP1 = Just 1
226
+
dupDepth DUP2 = Just 2
227
+
dupDepth DUP3 = Just 3
228
+
dupDepth DUP4 = Just 4
229
+
dupDepth DUP5 = Just 5
230
+
dupDepth DUP6 = Just 6
231
+
dupDepth DUP7 = Just 7
232
+
dupDepth DUP8 = Just 8
233
+
dupDepth DUP9 = Just 9
234
+
dupDepth DUP10 = Just 10
235
+
dupDepth DUP11 = Just 11
236
+
dupDepth DUP12 = Just 12
237
+
dupDepth DUP13 = Just 13
238
+
dupDepth DUP14 = Just 14
239
+
dupDepth DUP15 = Just 15
240
+
dupDepth DUP16 = Just 16
241
+
dupDepth _ = Nothing
242
+
243
+
swapDepth :: Opcode -> Maybe Int
244
+
swapDepth SWAP1 = Just 1
245
+
swapDepth SWAP2 = Just 2
246
+
swapDepth SWAP3 = Just 3
247
+
swapDepth SWAP4 = Just 4
248
+
swapDepth SWAP5 = Just 5
249
+
swapDepth SWAP6 = Just 6
250
+
swapDepth SWAP7 = Just 7
251
+
swapDepth SWAP8 = Just 8
252
+
swapDepth SWAP9 = Just 9
253
+
swapDepth SWAP10 = Just 10
254
+
swapDepth SWAP11 = Just 11
255
+
swapDepth SWAP12 = Just 12
256
+
swapDepth SWAP13 = Just 13
257
+
swapDepth SWAP14 = Just 14
258
+
swapDepth SWAP15 = Just 15
259
+
swapDepth SWAP16 = Just 16
260
+
swapDepth _ = Nothing
261
+
262
+
readBytecode :: ByteString -> Int -> Maybe Word8
263
+
readBytecode code pc
264
+
| pc >= 0 && pc < BS.length code = Just (BS.index code pc)
265
+
| otherwise = Nothing
266
+
267
+
readBytes :: ByteString -> Int -> Int -> Integer
268
+
readBytes code start n = go 0 0
269
+
where
270
+
go acc i
271
+
| i >= n = acc
272
+
| otherwise = case readBytecode code (start + i) of
273
+
Just b -> go (acc * 256 + fromIntegral b) (i + 1)
274
+
Nothing -> acc
+160
src/SymbolicExpression.hs
+160
src/SymbolicExpression.hs
···
1
+
{-# LANGUAGE DeriveGeneric #-}
2
+
{-# LANGUAGE DeriveAnyClass #-}
3
+
4
+
module SymbolicExpression where
5
+
6
+
import Data.Word
7
+
import Data.Map.Strict (Map)
8
+
import qualified Data.Map.Strict as Map
9
+
import GHC.Generics (Generic)
10
+
import Data.Bits hiding (And, Xor)
11
+
12
+
data SymExpr
13
+
= Concrete Integer
14
+
| Symbolic String Int
15
+
| Add SymExpr SymExpr
16
+
| Sub SymExpr SymExpr
17
+
| Mul SymExpr SymExpr
18
+
| Div SymExpr SymExpr
19
+
| Mod SymExpr SymExpr
20
+
| Exp SymExpr SymExpr
21
+
| SDiv SymExpr SymExpr
22
+
| SMod SymExpr SymExpr
23
+
| Lt SymExpr SymExpr
24
+
| Gt SymExpr SymExpr
25
+
| SLt SymExpr SymExpr
26
+
| SGt SymExpr SymExpr
27
+
| Eq SymExpr SymExpr
28
+
| IsZero SymExpr
29
+
| And SymExpr SymExpr
30
+
| Or SymExpr SymExpr
31
+
| Xor SymExpr SymExpr
32
+
| Not SymExpr
33
+
| Byte SymExpr SymExpr
34
+
| Shl SymExpr SymExpr
35
+
| Shr SymExpr SymExpr
36
+
| Sar SymExpr SymExpr
37
+
| Sha3 SymExpr SymExpr
38
+
| Address
39
+
| Balance SymExpr
40
+
| Origin
41
+
| Caller
42
+
| CallValue
43
+
| CallDataLoad SymExpr
44
+
| CallDataSize
45
+
| CodeSize
46
+
| GasPrice
47
+
| BlockHash SymExpr
48
+
| Coinbase
49
+
| Timestamp
50
+
| Number
51
+
| Difficulty
52
+
| GasLimit
53
+
| ChainId
54
+
| SelfBalance
55
+
| BaseFee
56
+
deriving (Eq, Ord, Generic, Show)
57
+
58
+
data Constraint
59
+
= CTrue SymExpr
60
+
| CFalse SymExpr
61
+
| CEq SymExpr SymExpr
62
+
| CNeq SymExpr SymExpr
63
+
| CLt SymExpr SymExpr
64
+
| CGt SymExpr SymExpr
65
+
deriving (Eq, Ord, Show)
66
+
67
+
mkAdd :: SymExpr -> SymExpr -> SymExpr
68
+
mkAdd (Concrete 0) e = e
69
+
mkAdd e (Concrete 0) = e
70
+
mkAdd (Concrete a) (Concrete b) = Concrete ((a + b) `mod` (2^256))
71
+
mkAdd a b = Add a b
72
+
73
+
mkSub :: SymExpr -> SymExpr -> SymExpr
74
+
mkSub e (Concrete 0) = e
75
+
mkSub (Concrete a) (Concrete b) = Concrete ((a - b) `mod` (2^256))
76
+
mkSub a b = Sub a b
77
+
78
+
mkMul :: SymExpr -> SymExpr -> SymExpr
79
+
mkMul (Concrete 0) _ = Concrete 0
80
+
mkMul _ (Concrete 0) = Concrete 0
81
+
mkMul (Concrete 1) e = e
82
+
mkMul e (Concrete 1) = e
83
+
mkMul (Concrete a) (Concrete b) = Concrete ((a * b) `mod` (2^256))
84
+
mkMul a b = Mul a b
85
+
86
+
mkDiv :: SymExpr -> SymExpr -> SymExpr
87
+
mkDiv _ (Concrete 0) = Concrete 0
88
+
mkDiv e (Concrete 1) = e
89
+
mkDiv (Concrete a) (Concrete b) = if b == 0 then Concrete 0 else Concrete (a `div` b)
90
+
mkDiv a b = Div a b
91
+
92
+
mkMod :: SymExpr -> SymExpr -> SymExpr
93
+
mkMod _ (Concrete 0) = Concrete 0
94
+
mkMod (Concrete a) (Concrete b) = if b == 0 then Concrete 0 else Concrete (a `mod` b)
95
+
mkMod a b = Mod a b
96
+
97
+
mkLt :: SymExpr -> SymExpr -> SymExpr
98
+
mkLt (Concrete a) (Concrete b) = Concrete (if a < b then 1 else 0)
99
+
mkLt a b = Lt a b
100
+
101
+
mkGt :: SymExpr -> SymExpr -> SymExpr
102
+
mkGt (Concrete a) (Concrete b) = Concrete (if a > b then 1 else 0)
103
+
mkGt a b = Gt a b
104
+
105
+
mkEq :: SymExpr -> SymExpr -> SymExpr
106
+
mkEq a b | a == b = Concrete 1
107
+
mkEq (Concrete a) (Concrete b) = Concrete (if a == b then 1 else 0)
108
+
mkEq a b = Eq a b
109
+
110
+
mkIsZero :: SymExpr -> SymExpr
111
+
mkIsZero (Concrete 0) = Concrete 1
112
+
mkIsZero (Concrete _) = Concrete 0
113
+
mkIsZero e = IsZero e
114
+
115
+
mkAnd :: SymExpr -> SymExpr -> SymExpr
116
+
mkAnd (Concrete 0) _ = Concrete 0
117
+
mkAnd _ (Concrete 0) = Concrete 0
118
+
mkAnd (Concrete a) (Concrete b) = Concrete (a .&. b)
119
+
mkAnd a b = And a b
120
+
121
+
mkOr :: SymExpr -> SymExpr -> SymExpr
122
+
mkOr (Concrete a) (Concrete b) = Concrete (a .|. b)
123
+
mkOr a b = Or a b
124
+
125
+
mkXor :: SymExpr -> SymExpr -> SymExpr
126
+
mkXor (Concrete a) (Concrete b) = Concrete (xor a b)
127
+
mkXor a b = Xor a b
128
+
129
+
mkNot :: SymExpr -> SymExpr
130
+
mkNot (Concrete a) = Concrete ((2^256 - 1) - a)
131
+
mkNot e = Not e
132
+
133
+
prettyExpr :: SymExpr -> String
134
+
prettyExpr (Concrete n) = show n
135
+
prettyExpr (Symbolic name id) = name ++ "_" ++ show id
136
+
prettyExpr (Add a b) = "(" ++ prettyExpr a ++ " + " ++ prettyExpr b ++ ")"
137
+
prettyExpr (Sub a b) = "(" ++ prettyExpr a ++ " - " ++ prettyExpr b ++ ")"
138
+
prettyExpr (Mul a b) = "(" ++ prettyExpr a ++ " * " ++ prettyExpr b ++ ")"
139
+
prettyExpr (Div a b) = "(" ++ prettyExpr a ++ " / " ++ prettyExpr b ++ ")"
140
+
prettyExpr (Mod a b) = "(" ++ prettyExpr a ++ " % " ++ prettyExpr b ++ ")"
141
+
prettyExpr (Lt a b) = "(" ++ prettyExpr a ++ " < " ++ prettyExpr b ++ ")"
142
+
prettyExpr (Gt a b) = "(" ++ prettyExpr a ++ " > " ++ prettyExpr b ++ ")"
143
+
prettyExpr (Eq a b) = "(" ++ prettyExpr a ++ " == " ++ prettyExpr b ++ ")"
144
+
prettyExpr (IsZero a) = "IsZero(" ++ prettyExpr a ++ ")"
145
+
prettyExpr (And a b) = "(" ++ prettyExpr a ++ " & " ++ prettyExpr b ++ ")"
146
+
prettyExpr (Or a b) = "(" ++ prettyExpr a ++ " | " ++ prettyExpr b ++ ")"
147
+
prettyExpr (Not a) = "~" ++ prettyExpr a
148
+
prettyExpr Caller = "caller"
149
+
prettyExpr CallValue = "callvalue"
150
+
prettyExpr (CallDataLoad offset) = "calldataload(" ++ prettyExpr offset ++ ")"
151
+
prettyExpr CallDataSize = "calldatasize"
152
+
prettyExpr _ = "<expr>"
153
+
154
+
prettyConstraint :: Constraint -> String
155
+
prettyConstraint (CTrue e) = prettyExpr e ++ " != 0"
156
+
prettyConstraint (CFalse e) = prettyExpr e ++ " == 0"
157
+
prettyConstraint (CEq a b) = prettyExpr a ++ " == " ++ prettyExpr b
158
+
prettyConstraint (CNeq a b) = prettyExpr a ++ " != " ++ prettyExpr b
159
+
prettyConstraint (CLt a b) = prettyExpr a ++ " < " ++ prettyExpr b
160
+
prettyConstraint (CGt a b) = prettyExpr a ++ " > " ++ prettyExpr b
+154
src/SymbolicState.hs
+154
src/SymbolicState.hs
···
1
+
{-# LANGUAGE DeriveGeneric #-}
2
+
3
+
module SymbolicState where
4
+
5
+
import SymbolicExpression
6
+
import Data.Map.Strict (Map)
7
+
import qualified Data.Map.Strict as Map
8
+
import Data.Word
9
+
import Data.ByteString (ByteString)
10
+
import qualified Data.ByteString as BS
11
+
import GHC.Generics (Generic)
12
+
13
+
newtype SymStack = SymStack [SymExpr]
14
+
deriving (Show, Eq)
15
+
16
+
newtype SymMemory = SymMemory (Map Integer SymExpr)
17
+
deriving (Show, Eq)
18
+
19
+
newtype SymStorage = SymStorage (Map SymExpr SymExpr)
20
+
deriving (Show, Eq)
21
+
22
+
data ExecState = ExecState
23
+
{ stack :: SymStack
24
+
, memory :: SymMemory
25
+
, storage :: SymStorage
26
+
, pc :: Int
27
+
, gas :: Integer
28
+
, constraints :: [Constraint]
29
+
, calldata :: ByteString
30
+
, returnData :: Maybe SymExpr
31
+
, reverted :: Bool
32
+
, halted :: Bool
33
+
, symbolicId :: Int
34
+
} deriving (Show)
35
+
36
+
initState :: ByteString -> ExecState
37
+
initState cd = ExecState
38
+
{ stack = emptyStack
39
+
, memory = emptyMemory
40
+
, storage = emptyStorage
41
+
, pc = 0
42
+
, gas = 1000000
43
+
, constraints = []
44
+
, calldata = cd
45
+
, returnData = Nothing
46
+
, reverted = False
47
+
, halted = False
48
+
, symbolicId = 0
49
+
}
50
+
51
+
emptyStack :: SymStack
52
+
emptyStack = SymStack []
53
+
54
+
pushStack :: SymExpr -> SymStack -> Maybe SymStack
55
+
pushStack expr (SymStack xs)
56
+
| length xs >= 1024 = Nothing
57
+
| otherwise = Just (SymStack (expr : xs))
58
+
59
+
popStack :: SymStack -> Maybe (SymExpr, SymStack)
60
+
popStack (SymStack []) = Nothing
61
+
popStack (SymStack (x:xs)) = Just (x, SymStack xs)
62
+
63
+
popStackN :: Int -> SymStack -> Maybe ([SymExpr], SymStack)
64
+
popStackN n (SymStack xs)
65
+
| n > length xs = Nothing
66
+
| otherwise = Just (take n xs, SymStack (drop n xs))
67
+
68
+
peekStack :: Int -> SymStack -> Maybe SymExpr
69
+
peekStack n (SymStack xs)
70
+
| n >= length xs = Nothing
71
+
| otherwise = Just (xs !! n)
72
+
73
+
dupStack :: Int -> SymStack -> Maybe SymStack
74
+
dupStack n s = do
75
+
expr <- peekStack (n - 1) s
76
+
pushStack expr s
77
+
78
+
swapStack :: Int -> SymStack -> Maybe SymStack
79
+
swapStack n (SymStack xs)
80
+
| n >= length xs = Nothing
81
+
| otherwise = Just (SymStack (xs0 : (take (n-1) xs1) ++ [xn] ++ (drop n xs1)))
82
+
where
83
+
xs0 = head xs
84
+
xs1 = tail xs
85
+
xn = xs !! n
86
+
87
+
stackSize :: SymStack -> Int
88
+
stackSize (SymStack xs) = length xs
89
+
90
+
emptyMemory :: SymMemory
91
+
emptyMemory = SymMemory Map.empty
92
+
93
+
mstore :: Integer -> SymExpr -> SymMemory -> SymMemory
94
+
mstore offset value (SymMemory m) = SymMemory (Map.insert offset value m)
95
+
96
+
mstore8 :: Integer -> SymExpr -> SymMemory -> SymMemory
97
+
mstore8 = mstore
98
+
99
+
mload :: Integer -> SymMemory -> SymExpr
100
+
mload offset (SymMemory m) = Map.findWithDefault (Concrete 0) offset m
101
+
102
+
emptyStorage :: SymStorage
103
+
emptyStorage = SymStorage Map.empty
104
+
105
+
sstore :: SymExpr -> SymExpr -> SymStorage -> SymStorage
106
+
sstore key value (SymStorage s) = SymStorage (Map.insert key value s)
107
+
108
+
sload :: SymExpr -> SymStorage -> SymExpr
109
+
sload key (SymStorage s) = Map.findWithDefault (Concrete 0) key s
110
+
111
+
addConstraint :: Constraint -> ExecState -> ExecState
112
+
addConstraint c state = state { constraints = c : constraints state }
113
+
114
+
newSymbolic :: String -> ExecState -> (SymExpr, ExecState)
115
+
newSymbolic name state =
116
+
let sid = symbolicId state
117
+
sym = Symbolic name sid
118
+
state' = state { symbolicId = sid + 1 }
119
+
in (sym, state')
120
+
121
+
prettyStack :: SymStack -> String
122
+
prettyStack (SymStack xs) = unlines $
123
+
[ "[" ++ show i ++ "] " ++ prettyExpr expr
124
+
| (i, expr) <- zip [0..] xs ]
125
+
126
+
prettyMemory :: SymMemory -> String
127
+
prettyMemory (SymMemory m) = unlines $
128
+
[ " 0x" ++ showHex offset ++ ": " ++ prettyExpr value
129
+
| (offset, value) <- Map.toList m ]
130
+
131
+
prettyStorage :: SymStorage -> String
132
+
prettyStorage (SymStorage s) = unlines $
133
+
[ " " ++ prettyExpr key ++ " => " ++ prettyExpr value
134
+
| (key, value) <- Map.toList s ]
135
+
136
+
showHex :: Integer -> String
137
+
showHex n = reverse $ take 4 $ reverse (go n) ++ repeat '0'
138
+
where
139
+
go 0 = "0"
140
+
go n = let (q, r) = n `divMod` 16
141
+
digit = "0123456789abcdef" !! fromIntegral r
142
+
in if q == 0 then [digit] else go q ++ [digit]
143
+
144
+
prettyState :: ExecState -> String
145
+
prettyState state = unlines
146
+
[ "PC: " ++ show (pc state)
147
+
, "Gas: " ++ show (gas state)
148
+
, "Halted: " ++ show (halted state)
149
+
, "Reverted: " ++ show (reverted state)
150
+
, "Stack:"
151
+
, prettyStack (stack state)
152
+
, "Constraints: " ++ show (length (constraints state))
153
+
, unlines [" " ++ prettyConstraint c | c <- reverse (constraints state)]
154
+
]
+36
symevm.cabal
+36
symevm.cabal
···
1
+
cabal-version: 2.4
2
+
name: symevm
3
+
version: 0.1.0.0
4
+
synopsis: Symbolic EVM Evaluator
5
+
description: An intermediate-level symbolic execution engine for EVM bytecode
6
+
license: MIT
7
+
author: Anonymous
8
+
maintainer: example@example.com
9
+
category: Blockchain
10
+
build-type: Simple
11
+
12
+
common warnings
13
+
ghc-options: -Wall
14
+
15
+
library
16
+
import: warnings
17
+
exposed-modules: SymbolicExpression
18
+
, SymbolicState
19
+
, Opcode
20
+
, Executor
21
+
build-depends: base >=4.16 && <5
22
+
, bytestring >=0.11 && <0.13
23
+
, containers >=0.6 && <0.8
24
+
hs-source-dirs: src
25
+
default-language: Haskell2010
26
+
27
+
executable symevm
28
+
import: warnings
29
+
main-is: Main.hs
30
+
build-depends: base >=4.16 && <5
31
+
, symevm
32
+
, bytestring >=0.11 && <0.13
33
+
, containers >=0.6 && <0.8
34
+
hs-source-dirs: app
35
+
default-language: Haskell2010
36
+
ghc-options: -threaded -rtsopts -with-rtsopts=-N