Fix #1082: resolve symbolic-key SLOAD over a ConcreteStore

CHANGELOG.md

@@ -8,6 +8,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 
 ## Fixed
+- A symbolic-key `SLOAD` over a `ConcreteStore` is now resolved during execution
+  instead of being carried into a fork as an unresolved read: an empty store
+  reads 0 at every slot, and a symbolic mapping read filters out concrete
+  entries whose recorded keccak preimage identifies a different mapping
+  (keccak injectivity). Fixes non-termination/blowup on symbolic mapping reads
+  over concretely-initialized storage ([#1082](https://github.com/argotorg/hevm/issues/1082))
 - Cheatcode string arguments are now decoded leniently instead of crashing on
   invalid UTF-8: ABI `string` values are raw bytes, so e.g. `vm.setEnv`,
   `vm.envString` and `vm.label` no longer abort the whole run when handed a

src/EVM.hs

@@ -795,7 +795,9 @@ exec1 conf = do
 
                 symbolicRead :: EVM t () = if this.external
                   then accessStorage self x finalizeLoad
-                  else finalizeLoad $ Expr.readStorage' (Expr.concKeccakOnePass x) this.storage
+                  else let slot = Expr.concKeccakOnePass x
+                           preMap = Map.fromList [ (h, bs) | (bs, h) <- toList vm.keccakPreImgs ]
+                       in finalizeLoad $ Expr.readStorage' slot (Expr.filterStoreByReadSlot preMap slot this.storage)
 
                 concreteRead :: EVM t () = do
                   acc <- accessStorageForGas self (forceLit x)

src/EVM/Expr.hs

@@ -74,6 +74,7 @@ module EVM.Expr
     -- * Storage
   , readStorage'
   , readStorage
+  , filterStoreByReadSlot
   , writeStorage
   , concStoreContains
   , getAddr
@@ -809,9 +810,33 @@ simplifyReads = \case
 
 readStorage' :: Expr EWord -> Expr Storage -> Expr EWord
 readStorage' loc store = case readStorage loc store of
+                           -- an empty ConcreteStore is total: every slot, even a symbolic one,
+                           -- reads 0. Not in readStorage: accessStorage needs the Nothing/SLoad
+                           -- results there to drive lazy RPC slot fetching (partial caches).
+                           Just (SLoad _ (ConcreteStore m)) | Map.null m -> Lit 0
                            Just v -> v
                            Nothing -> Lit 0
 
+-- | The mapping slot (idx) of a symbolic mapping read keccak(key . idx), for both shapes hevm produces
+readMappingIdx :: Expr EWord -> Maybe W256
+readMappingIdx (MappingSlot idx _)
+  | BS.length idx == 64 = Just (W256 (word256 (BS.takeEnd 32 idx)))
+readMappingIdx (Keccak (CopySlice (Lit 0) (Lit 0) (Lit 0x40) (WriteWord (Lit 0) _ (ConcreteBuf idx)) _))
+  | BS.length idx >= 64 = Just (W256 (word256 (BS.take 32 (BS.drop 32 idx))))
+readMappingIdx _ = Nothing
+
+-- | Drop ConcreteStore entries that cannot alias a symbolic mapping read: a concrete key whose
+-- recorded keccak preimage identifies a different mapping slot cannot equal keccak(key . idx),
+-- by injectivity. Keys with unknown preimage are kept. `preMap` maps hash -> preimage.
+filterStoreByReadSlot :: Map.Map W256 ByteString -> Expr EWord -> Expr Storage -> Expr Storage
+filterStoreByReadSlot preMap slot (ConcreteStore m)
+  | Just readSlot <- readMappingIdx slot =
+      let keep k = case Map.lookup k preMap of
+                     Just bs | BS.length bs == 64 -> W256 (word256 (BS.takeEnd 32 bs)) == readSlot
+                     _ -> True
+      in ConcreteStore (Map.filterWithKey (\k _ -> keep k) m)
+filterStoreByReadSlot _ _ st = st
+
 -- | Reads the word at the given slot from the given storage expression.
 --
 -- Note that we return a Nothing instead of a 0x0 if we are reading from a

test/EVM/Expr/ExprTests.hs

@@ -63,6 +63,36 @@ storageTests = testGroup "Storage tests"
     , testCase "read-past-write" $ assertEqual errorMsg
         (Lit 0xab)
         (Expr.readStorage' (Lit 0x0) (SStore (Lit 0x1) (Var "b") (ConcreteStore $ Map.fromList [(0x0, 0xab)])))
+    -- #1082: an empty ConcreteStore is total, so a symbolic slot reads 0
+    , testCase "read-symbolic-slot-empty-concrete-store" $ assertEqual errorMsg
+        (Lit 0)
+        (Expr.readStorage' (Var "x") (ConcreteStore mempty))
+    -- accessStorage relies on Nothing here to drive lazy RPC slot fetching;
+    -- the empty-store => 0 rule lives in readStorage' only
+    , testCase "readStorage-keeps-nothing-on-concrete-miss" $ assertEqual errorMsg
+        Nothing
+        (Expr.readStorage (Lit 0x5) (ConcreteStore mempty))
+    -- a concrete-valued write would instead be folded into the store
+    , testCase "read-symbolic-slot-stripped-to-empty-concrete-store" $ assertEqual errorMsg
+        (Lit 0)
+        (Expr.readStorage' (mappingRead 1 "k") (SStore (Lit 0x5) (Var "b") (ConcreteStore mempty)))
+    , testCase "filter-store-drops-other-mapping-entries" $ assertEqual errorMsg
+        (ConcreteStore $ Map.fromList [(0x5, 0x222)])
+        (Expr.filterStoreByReadSlot preImgs (mappingRead 1 "k")
+          (ConcreteStore $ Map.fromList [(preImgHash, 0x111), (0x5, 0x222)]))
+    , testCase "filter-store-keeps-same-mapping-entries" $ assertEqual errorMsg
+        (ConcreteStore $ Map.fromList [(preImgHash, 0x111), (0x5, 0x222)])
+        (Expr.filterStoreByReadSlot preImgs (mappingRead 0 "k")
+          (ConcreteStore $ Map.fromList [(preImgHash, 0x111), (0x5, 0x222)]))
+    , testCase "filter-store-ignores-non-mapping-reads" $ assertEqual errorMsg
+        (ConcreteStore $ Map.fromList [(preImgHash, 0x111)])
+        (Expr.filterStoreByReadSlot preImgs (Var "x")
+          (ConcreteStore $ Map.fromList [(preImgHash, 0x111)]))
+    , testCase "read-unrelated-mapping-filters-to-zero" $ assertEqual errorMsg
+        (Lit 0)
+        (Expr.readStorage' (mappingRead 1 "k")
+          (Expr.filterStoreByReadSlot preImgs (mappingRead 1 "k")
+            (ConcreteStore $ Map.fromList [(preImgHash, 0x111)])))
     , testCase "simplify-storage-wordToAddr" $ do
        let a = "0x000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a"
            store = ConcreteStore (Map.fromList[(W256 0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,W256 0x5842cf)])
@@ -82,7 +112,15 @@ storageTests = testGroup "Storage tests"
            simp = Expr.concKeccakSimpExpr outer
        assertEqual "Expression should simplify to value." simp (Lit 0xacab)
   ]
-  where errorMsg = "Storage read expression not simplified correctly"
+  where
+    errorMsg = "Storage read expression not simplified correctly"
+    -- a symbolic read of the mapping at storage slot n: keccak(key . n)
+    mappingRead n key = Keccak (WriteWord (Lit 0) (Var key) (ConcreteBuf (mapSlotBuf n)))
+    mapSlotBuf n = BS.pack (replicate 63 0 ++ [n])
+    -- recorded preimage of a write to the mapping at slot 0 with key 0xaa
+    preImgBytes = BS.pack (replicate 31 0 ++ [0xaa] ++ replicate 32 0)
+    preImgHash = keccak' preImgBytes
+    preImgs = Map.fromList [(preImgHash, preImgBytes)]
 
 copySliceTests :: TestTree
 copySliceTests = testGroup "CopySlice tests"
@@ -353,7 +391,8 @@ basicSimplificationTests = testGroup "Basic simplification tests"
       -- near-collision in the keccak hash
       let x = (SLoad (Keccak (AbstractBuf "es")) (SStore (Add (Keccak (ConcreteBuf "")) (Lit 0x1)) (Lit 0xacab) (ConcreteStore (Map.empty))))
       let simplified = Expr.simplify x
-      let expected = (SLoad (Keccak (AbstractBuf "es")) (ConcreteStore (Map.empty))) -- TODO: This should be simplified to (Lit 0)
+      -- the write is stripped and the residual read over an empty ConcreteStore is 0 (#1082)
+      let expected = Lit 0
       assertEqual "Must be equal, given keccak distance axiom" expected simplified
   , testCase "expr-simp-and-commut-assoc" $ do
       let

test/EVM/Test/FoundryTests.hs

@@ -124,6 +124,15 @@ tests = testGroup "Foundry tests"
     , test "Keccak" $ do
         let testFile = "test/contracts/pass/keccak.sol"
         executeSingleMethod testFile "prove_access" >>= assertEqualM "test result" (True, True)
+    , test "Symbolic-Key-SLoad" $ do
+        -- #1082: without the fix the untouched-mapping read does not complete
+        let testFile = "test/contracts/pass/symbolicKeySload.sol"
+        executeSingleMethod testFile "prove_symbolic_key_empty_store" >>= assertEqualM "empty store reads zero" (True, True)
+        executeSingleMethod testFile "prove_symbolic_key_untouched_mapping" >>= assertEqualM "untouched mapping reads zero" (True, True)
+    , test "Symbolic-Key-SLoad-Fail" $ do
+        -- #1082 soundness: same-mapping entries must be kept, so this falsifies
+        let testFile = "test/contracts/fail/symbolicKeySload.sol"
+        executeSingleMethod testFile "prove_same_mapping_falsifiable" >>= assertEqualM "same-mapping read must falsify" (False, True)
     , test "AssertApproxEqAbs-Pass" $ do
         let testFile = "test/contracts/pass/assertApproxEqAbs.sol"
         executeAllMethodsWithPrefix testFile "prove" >>= assertEqualM "test result" (True, True)

test/contracts/fail/symbolicKeySload.sol

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+// #1082 soundness guard: entries of the mapping being read must be kept,
+// so this assert is falsifiable (e.g. populated[0] = 1).
+contract SymbolicKeySloadFail {
+    bool public constant IS_TEST = true;
+    mapping(uint256 => uint256) populated;
+
+    function setUp() public {
+        for (uint256 i = 0; i < 10; i++) {
+            populated[i] = i + 1;
+        }
+    }
+
+    function prove_same_mapping_falsifiable(uint256 x) public view {
+        assert(populated[x] == 0);
+    }
+}

test/contracts/pass/symbolicKeySload.sol

@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+// Regression tests for #1082: a symbolic-key SLOAD over a ConcreteStore must
+// resolve during execution instead of forking on an unresolved read.
+
+contract SymbolicKeyEmptyStore {
+    bool public constant IS_TEST = true;
+    mapping(uint256 => uint256) s;
+
+    function prove_symbolic_key_empty_store(uint256 x) public view {
+        assert(s[x] == 0);
+    }
+}
+
+// setUp populates one mapping; a symbolic read of the untouched mapping
+// filters out all 600 entries (their recorded keccak preimages identify a
+// different mapping) and resolves to 0. Without the fix it does not complete.
+contract SymbolicKeyFiltered {
+    bool public constant IS_TEST = true;
+    mapping(uint256 => uint256) populated;
+    mapping(uint256 => uint256) untouched;
+
+    function setUp() public {
+        for (uint256 i = 0; i < 600; i++) {
+            populated[i] = i + 1;
+        }
+    }
+
+    function prove_symbolic_key_untouched_mapping(uint256 x) public view {
+        assert(untouched[x] == 0);
+    }
+}