More precise smt address encoding

src/EVM.hs

@@ -1805,23 +1805,30 @@ create :: (?op :: Word8)
   -> W256 -> Word64 -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM s ()
 create self this xSize xGas xValue xs newAddr initCode = do
   vm0 <- get
+  -- are we exceeding the max init code size
   if xSize > vm0.block.maxCodeSize * 2
   then do
     assign (#state % #stack) (Lit 0 : xs)
     assign (#state % #returndata) mempty
     vmError $ MaxInitCodeSizeExceeded (vm0.block.maxCodeSize * 2) xSize
+  -- are we overflowing the nonce
   else if this.nonce == Just maxBound
   then do
     assign (#state % #stack) (Lit 0 : xs)
     assign (#state % #returndata) mempty
     pushTrace $ ErrorTrace NonceOverflow
     next
+  -- are we overflowing the stack
   else if length vm0.frames >= 1024
   then do
     assign (#state % #stack) (Lit 0 : xs)
     assign (#state % #returndata) mempty
     pushTrace $ ErrorTrace CallDepthLimitReached
     next
+  -- are we deploying to an address that already has a contract?
+  -- note: the symbolic interpreter generates constraints ensuring that
+  -- symbolic storage keys cannot alias other storage keys, making this check
+  -- safe to perform statically
   else if collision $ Map.lookup newAddr vm0.env.contracts
   then burn xGas $ do
     assign (#state % #stack) (Lit 0 : xs)
@@ -1837,7 +1844,6 @@ create self this xSize xGas xValue xs newAddr initCode = do
         next
         touchAccount self
         touchAccount newAddr
-      -- are we overflowing the nonce
       False -> burn xGas $ do
         -- unfortunately we have to apply some (pretty hacky)
         -- heuristics here to parse the unstructured buffer read

src/EVM/Expr.hs

@@ -1087,6 +1087,10 @@ isPartial = \case
   Partial {} -> True
   _ -> False
 
+isSymAddr :: Expr EAddr -> Bool
+isSymAddr (SymAddr _) = True
+isSymAddr _ = False
+
 -- | Returns the byte at idx from the given word.
 indexWord :: Expr EWord -> Expr EWord -> Expr Byte
 -- Simplify masked reads:

src/EVM/SMT.hs

@@ -411,9 +411,11 @@ declareVars names = SMT2 (["; variables"] <> fmap declare names) mempty 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) mempty cexvars
+declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names <> fmap assume names) mempty 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

src/EVM/SymExec.hs

@@ -454,14 +454,18 @@ verifyContract solvers theCode signature' concreteArgs opts maybepre maybepost =
 runExpr :: Stepper.Stepper RealWorld (Expr End)
 runExpr = do
   vm <- Stepper.runFully
-  let asserts = vm.keccakEqs <> vm.constraints
+  let asserts = vm.keccakEqs <> vm.constraints <> consistentStorageKeys vm.env.contracts
       traces = Traces (Zipper.toForest vm.traces) vm.env.contracts
   pure $ case vm.result of
     Just (VMSuccess buf) -> Success asserts traces buf (fmap toEContract vm.env.contracts)
     Just (VMFailure e) -> Failure asserts traces e
     Just (Unfinished p) -> Partial asserts traces p
     _ -> internalError "vm in intermediate state after call to runFully"
 
+-- build constraints that ensure that symbolic storage keys cannot alias other storage keys
+consistentStorageKeys :: Map (Expr EAddr) Contract -> [Prop]
+consistentStorageKeys (Map.keys -> addrs) = [a ./= b | a <- addrs, b <- filter Expr.isSymAddr addrs]
+
 toEContract :: Contract -> Expr EContract
 toEContract c = C c.code c.storage c.balance c.nonce
 

test/test.hs

@@ -1101,8 +1101,7 @@ tests = testGroup "hevm"
         Just c <- solcRuntime "C" src
         res <- reachableUserAsserts c Nothing
         assertBool "unexpected cex" (isRight res)
-    -- TODO: implement missing aliasing rules
-    , expectFail $ testCase "deployed-contract-addresses-cannot-alias" $ do
+    , testCase "deployed-contract-addresses-cannot-alias" $ do
         Just c <- solcRuntime "C"
           [i|
             contract A {}
@@ -1298,36 +1297,50 @@ tests = testGroup "hevm"
         Right e <- reachableUserAsserts c Nothing
         -- TODO: this should work one day
         assertBool "should be partial" (Expr.containsNode isPartial e)
+    , testCase "symbolic-addresses-cannot-be-zero-or-precompiles" $ do
+        let addrs = [T.pack . show . Addr $ a | a <- [0x0..0x09]]
+            mkC a = fromJust <$> solcRuntime "A"
+              [i|
+                contract A {
+                  function f() external {
+                    assert(msg.sender != address(${a}));
+                  }
+                }
+              |]
+        codes <- mapM mkC addrs
+        results <- mapM (flip reachableUserAsserts (Just (Sig "f()" []))) codes
+        let ok = and $ fmap (isRight) results
+        assertBool "unexpected cex" ok
     , testCase "addresses-in-context-are-symbolic" $ do
         Just a <- solcRuntime "A"
           [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));
               }
             }
           |]