SMT: assume that symbolic addresses cannot be the zero address or pre…

…compiles
ethereum · Sep 11, 2023 · 60f3655 · 60f3655
1 parent f8a63d9
commit 60f3655
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
@@ -350,9 +350,11 @@ declareVars names = SMT2 (["; variables"] <> fmap declare names) cexvars
 
 -- Given a list of variable names, create an SMT2 object with the variables declared
 declareAddrs :: [Builder] -> SMT2
-declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) cexvars
+declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names <> fmap assume names) cexvars
   where
     declare n = "(declare-const " <> n <> " Addr)"
+    -- assume that symbolic addresses do not collide with the zero address or precompiles
+    assume n = "(assert (bvugt " <> n <> " (_ bv9 160)))"
     cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names }
 
 declareFrameContext :: [(Builder, [Prop])] -> SMT2