SymExec: add aliasing constraints for contract mapping keys

Adds constraints that ensure that symbolic addresses that are used to
key the contracts mapping cannot alias any other keys.

src/EVM.hs

@@ -1826,8 +1826,9 @@ create self this xSize xGas xValue xs newAddr initCode = do
     pushTrace $ ErrorTrace CallDepthLimitReached
     next
   -- are we deploying to an address that already has a contract?
-  -- note: this check is only sound to do statically if symbolic addresses
-  -- cannot have the value of any existing concrete addresses in the state.
+  -- 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)

src/EVM/Expr.hs

@@ -963,6 +963,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/SymExec.hs

@@ -437,14 +437,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

@@ -860,8 +860,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 {}
@@ -1057,6 +1056,20 @@ 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|