vm.fail
an intermediate symbolic execution engine for EVM bytecode
1{-# LANGUAGE DeriveGeneric #-}
2
3module SymbolicState where
4
5import SymbolicExpression
6import Data.Map.Strict (Map)
7import qualified Data.Map.Strict as Map
8import Data.Word
9import Data.ByteString (ByteString)
10import qualified Data.ByteString as BS
11import GHC.Generics (Generic)
12
13newtype SymStack = SymStack [SymExpr]
14 deriving (Show, Eq)
15
16newtype SymMemory = SymMemory (Map Integer SymExpr)
17 deriving (Show, Eq)
18
19newtype SymStorage = SymStorage (Map SymExpr SymExpr)
20 deriving (Show, Eq)
21
22data 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
36initState :: ByteString -> ExecState
37initState 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
51emptyStack :: SymStack
52emptyStack = SymStack []
53
54pushStack :: SymExpr -> SymStack -> Maybe SymStack
55pushStack expr (SymStack xs)
56 | length xs >= 1024 = Nothing
57 | otherwise = Just (SymStack (expr : xs))
58
59popStack :: SymStack -> Maybe (SymExpr, SymStack)
60popStack (SymStack []) = Nothing
61popStack (SymStack (x:xs)) = Just (x, SymStack xs)
62
63popStackN :: Int -> SymStack -> Maybe ([SymExpr], SymStack)
64popStackN n (SymStack xs)
65 | n > length xs = Nothing
66 | otherwise = Just (take n xs, SymStack (drop n xs))
67
68peekStack :: Int -> SymStack -> Maybe SymExpr
69peekStack n (SymStack xs)
70 | n >= length xs = Nothing
71 | otherwise = Just (xs !! n)
72
73dupStack :: Int -> SymStack -> Maybe SymStack
74dupStack n s = do
75 expr <- peekStack (n - 1) s
76 pushStack expr s
77
78swapStack :: Int -> SymStack -> Maybe SymStack
79swapStack 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
87stackSize :: SymStack -> Int
88stackSize (SymStack xs) = length xs
89
90emptyMemory :: SymMemory
91emptyMemory = SymMemory Map.empty
92
93mstore :: Integer -> SymExpr -> SymMemory -> SymMemory
94mstore offset value (SymMemory m) = SymMemory (Map.insert offset value m)
95
96mstore8 :: Integer -> SymExpr -> SymMemory -> SymMemory
97mstore8 = mstore
98
99mload :: Integer -> SymMemory -> SymExpr
100mload offset (SymMemory m) = Map.findWithDefault (Concrete 0) offset m
101
102emptyStorage :: SymStorage
103emptyStorage = SymStorage Map.empty
104
105sstore :: SymExpr -> SymExpr -> SymStorage -> SymStorage
106sstore key value (SymStorage s) = SymStorage (Map.insert key value s)
107
108sload :: SymExpr -> SymStorage -> SymExpr
109sload key (SymStorage s) = Map.findWithDefault (Concrete 0) key s
110
111addConstraint :: Constraint -> ExecState -> ExecState
112addConstraint c state = state { constraints = c : constraints state }
113
114newSymbolic :: String -> ExecState -> (SymExpr, ExecState)
115newSymbolic name state =
116 let sid = symbolicId state
117 sym = Symbolic name sid
118 state' = state { symbolicId = sid + 1 }
119 in (sym, state')
120
121prettyStack :: SymStack -> String
122prettyStack (SymStack xs) = unlines $
123 [ "[" ++ show i ++ "] " ++ prettyExpr expr
124 | (i, expr) <- zip [0..] xs ]
125
126prettyMemory :: SymMemory -> String
127prettyMemory (SymMemory m) = unlines $
128 [ " 0x" ++ showHex offset ++ ": " ++ prettyExpr value
129 | (offset, value) <- Map.toList m ]
130
131prettyStorage :: SymStorage -> String
132prettyStorage (SymStorage s) = unlines $
133 [ " " ++ prettyExpr key ++ " => " ++ prettyExpr value
134 | (key, value) <- Map.toList s ]
135
136showHex :: Integer -> String
137showHex 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
144prettyState :: ExecState -> String
145prettyState 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 ]