vm.fail
an intermediate symbolic execution engine for EVM bytecode
1{-# LANGUAGE DeriveGeneric #-}
2{-# LANGUAGE DeriveAnyClass #-}
3
4module SymbolicExpression where
5
6import Data.Word
7import Data.Map.Strict (Map)
8import qualified Data.Map.Strict as Map
9import GHC.Generics (Generic)
10import Data.Bits hiding (And, Xor)
11
12data 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
58data 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
67mkAdd :: SymExpr -> SymExpr -> SymExpr
68mkAdd (Concrete 0) e = e
69mkAdd e (Concrete 0) = e
70mkAdd (Concrete a) (Concrete b) = Concrete ((a + b) `mod` (2^256))
71mkAdd a b = Add a b
72
73mkSub :: SymExpr -> SymExpr -> SymExpr
74mkSub e (Concrete 0) = e
75mkSub (Concrete a) (Concrete b) = Concrete ((a - b) `mod` (2^256))
76mkSub a b = Sub a b
77
78mkMul :: SymExpr -> SymExpr -> SymExpr
79mkMul (Concrete 0) _ = Concrete 0
80mkMul _ (Concrete 0) = Concrete 0
81mkMul (Concrete 1) e = e
82mkMul e (Concrete 1) = e
83mkMul (Concrete a) (Concrete b) = Concrete ((a * b) `mod` (2^256))
84mkMul a b = Mul a b
85
86mkDiv :: SymExpr -> SymExpr -> SymExpr
87mkDiv _ (Concrete 0) = Concrete 0
88mkDiv e (Concrete 1) = e
89mkDiv (Concrete a) (Concrete b) = if b == 0 then Concrete 0 else Concrete (a `div` b)
90mkDiv a b = Div a b
91
92mkMod :: SymExpr -> SymExpr -> SymExpr
93mkMod _ (Concrete 0) = Concrete 0
94mkMod (Concrete a) (Concrete b) = if b == 0 then Concrete 0 else Concrete (a `mod` b)
95mkMod a b = Mod a b
96
97mkLt :: SymExpr -> SymExpr -> SymExpr
98mkLt (Concrete a) (Concrete b) = Concrete (if a < b then 1 else 0)
99mkLt a b = Lt a b
100
101mkGt :: SymExpr -> SymExpr -> SymExpr
102mkGt (Concrete a) (Concrete b) = Concrete (if a > b then 1 else 0)
103mkGt a b = Gt a b
104
105mkEq :: SymExpr -> SymExpr -> SymExpr
106mkEq a b | a == b = Concrete 1
107mkEq (Concrete a) (Concrete b) = Concrete (if a == b then 1 else 0)
108mkEq a b = Eq a b
109
110mkIsZero :: SymExpr -> SymExpr
111mkIsZero (Concrete 0) = Concrete 1
112mkIsZero (Concrete _) = Concrete 0
113mkIsZero e = IsZero e
114
115mkAnd :: SymExpr -> SymExpr -> SymExpr
116mkAnd (Concrete 0) _ = Concrete 0
117mkAnd _ (Concrete 0) = Concrete 0
118mkAnd (Concrete a) (Concrete b) = Concrete (a .&. b)
119mkAnd a b = And a b
120
121mkOr :: SymExpr -> SymExpr -> SymExpr
122mkOr (Concrete a) (Concrete b) = Concrete (a .|. b)
123mkOr a b = Or a b
124
125mkXor :: SymExpr -> SymExpr -> SymExpr
126mkXor (Concrete a) (Concrete b) = Concrete (xor a b)
127mkXor a b = Xor a b
128
129mkNot :: SymExpr -> SymExpr
130mkNot (Concrete a) = Concrete ((2^256 - 1) - a)
131mkNot e = Not e
132
133prettyExpr :: SymExpr -> String
134prettyExpr (Concrete n) = show n
135prettyExpr (Symbolic name id) = name ++ "_" ++ show id
136prettyExpr (Add a b) = "(" ++ prettyExpr a ++ " + " ++ prettyExpr b ++ ")"
137prettyExpr (Sub a b) = "(" ++ prettyExpr a ++ " - " ++ prettyExpr b ++ ")"
138prettyExpr (Mul a b) = "(" ++ prettyExpr a ++ " * " ++ prettyExpr b ++ ")"
139prettyExpr (Div a b) = "(" ++ prettyExpr a ++ " / " ++ prettyExpr b ++ ")"
140prettyExpr (Mod a b) = "(" ++ prettyExpr a ++ " % " ++ prettyExpr b ++ ")"
141prettyExpr (Lt a b) = "(" ++ prettyExpr a ++ " < " ++ prettyExpr b ++ ")"
142prettyExpr (Gt a b) = "(" ++ prettyExpr a ++ " > " ++ prettyExpr b ++ ")"
143prettyExpr (Eq a b) = "(" ++ prettyExpr a ++ " == " ++ prettyExpr b ++ ")"
144prettyExpr (IsZero a) = "IsZero(" ++ prettyExpr a ++ ")"
145prettyExpr (And a b) = "(" ++ prettyExpr a ++ " & " ++ prettyExpr b ++ ")"
146prettyExpr (Or a b) = "(" ++ prettyExpr a ++ " | " ++ prettyExpr b ++ ")"
147prettyExpr (Not a) = "~" ++ prettyExpr a
148prettyExpr Caller = "caller"
149prettyExpr CallValue = "callvalue"
150prettyExpr (CallDataLoad offset) = "calldataload(" ++ prettyExpr offset ++ ")"
151prettyExpr CallDataSize = "calldatasize"
152prettyExpr _ = "<expr>"
153
154prettyConstraint :: Constraint -> String
155prettyConstraint (CTrue e) = prettyExpr e ++ " != 0"
156prettyConstraint (CFalse e) = prettyExpr e ++ " == 0"
157prettyConstraint (CEq a b) = prettyExpr a ++ " == " ++ prettyExpr b
158prettyConstraint (CNeq a b) = prettyExpr a ++ " != " ++ prettyExpr b
159prettyConstraint (CLt a b) = prettyExpr a ++ " < " ++ prettyExpr b
160prettyConstraint (CGt a b) = prettyExpr a ++ " > " ++ prettyExpr b