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

…compiles
ethereum · Sep 13, 2023 · 2b2e911 · 2b2e911
1 parent f8a63d9
commit 2b2e911
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
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

diff --git a/test/test.hs b/test/test.hs
@@ -1062,31 +1062,31 @@ tests = testGroup "hevm"
           [i|
             contract A {
               function f() external {
-                assert(msg.sender != address(0x0));
+                assert(msg.sender != address(0x10));
               }
             }
           |]
         Just b <- solcRuntime "B"
           [i|
             contract B {
               function f() external {
-                assert(block.coinbase != address(0x1));
+                assert(block.coinbase != address(0x11));
               }
             }
           |]
         Just c <- solcRuntime "C"
           [i|
             contract C {
               function f() external {
-                assert(tx.origin != address(0x2));
+                assert(tx.origin != address(0x12));
               }
             }
           |]
         Just d <- solcRuntime "D"
           [i|
             contract D {
               function f() external {
-                assert(address(this) != address(0x3));
+                assert(address(this) != address(0x13));
               }
             }
           |]