vm.fail
an intermediate symbolic execution engine for EVM bytecode
1{-# LANGUAGE LambdaCase #-}
2
3module Executor where
4
5import SymbolicExpression
6import SymbolicState
7import Opcode
8import Data.ByteString (ByteString)
9import qualified Data.ByteString as BS
10import Data.Maybe (fromMaybe)
11import Control.Monad (foldM)
12import Prelude hiding (LT, GT, EQ)
13
14data StepResult
15 = Continue ExecState
16 | Branch ExecState ExecState
17 | Halt ExecState
18 | Error String
19 deriving (Show)
20
21executeOpcode :: ByteString -> Opcode -> ExecState -> StepResult
22executeOpcode 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
155binOp :: (SymExpr -> SymExpr -> SymExpr) -> ExecState -> StepResult
156binOp 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
163unOp :: (SymExpr -> SymExpr) -> ExecState -> StepResult
164unOp 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
171loadCalldata :: ByteString -> Integer -> SymExpr
172loadCalldata 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
179step :: ByteString -> ExecState -> StepResult
180step 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
195run :: ByteString -> ExecState -> Int -> [ExecState]
196run 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
207explore :: ByteString -> ExecState -> Int -> [ExecState]
208explore 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 }]