Maps and Arrays cannot match + masking rewrite rule

CHANGELOG.md

@@ -55,6 +55,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - More complete simplification during interpretation
 - SMT-based resolving of addresses now works for delegatecall and staticcall
   opcodes as well
+- Rewrite rule to deal with some forms of argument packing by Solidity
+  via masking
+- More rewrite rules for array and map lookups.
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value

src/EVM/Expr.hs

@@ -643,16 +643,25 @@ readStorage w st = go (simplifyNoLitToKeccak w) (simplifyNoLitToKeccak st)
       (MappingSlot idA _, MappingSlot idB _)       | isMap' idB, isMap' idA, idsDontMatch idA idB  -> go slot prev
       (MappingSlot idA keyA, MappingSlot idB keyB) | isMap' idB, isMap' idA, surelyNotEqual keyA keyB -> go slot prev
 
-      -- special case of array + map -> skip write
+      -- special case of: array + map -> skip write OR map + array with offset zero -> skip write
+      -- Note that none of these allow to "Add" an offset, only to overwrite the input to
+      -- Keccak. Hence to clash, one would need to find 2 inputs to keccak of
+      -- different lengths that clash when keccak-ed
       (ArraySlotWithOffs idA _, Keccak k)          | isMap k, isArray idA -> go slot prev
       (ArraySlotWithOffs2 idA _ _, Keccak k)       | isMap k, isArray idA -> go slot prev
       (ArraySlotZero idA, Keccak k)                | isMap k, isArray idA -> go slot prev
-
-      -- special case of map + array -> skip write
-      (Keccak k, ArraySlotWithOffs idA _)          | isMap k, isArray idA -> go slot prev
-      (Keccak k, ArraySlotWithOffs2 idA _ _)       | isMap k, isArray idA -> go slot prev
-      (ArraySlotWithOffs idA _, Keccak k)          | isMap k, isArray idA -> go slot prev
-      (ArraySlotWithOffs2 idA _ _, Keccak k)       | isMap k, isArray idA -> go slot prev
+      (MappingSlot idA _, ArraySlotZero idB)          | isMap' idA, isArray idB  -> go slot prev
+      (Keccak idA, ArraySlotZero idB)                 | isMap idA, isArray idB -> go slot prev
+      (ArraySlotZero idA, MappingSlot idB _)          | isArray idA, isMap' idB  -> go slot prev
+      (ArraySlotZero idA, Keccak idB)                 | isArray idA, isMap idB  -> go slot prev
+
+      -- as above, but with low concrete offset
+      -- NOTE: ArraySlotWithOffs2 could only be rewritten if both offsets are Lit (i.e. concrete)
+      --       but then the simplifier rewrites it to ArraySlotWithOffs
+      (MappingSlot idA _, ArraySlotWithOffs idB (Lit offs)) | isMap' idA, isArray idB, offs < 1000  -> go slot prev
+      (Keccak idA, ArraySlotWithOffs idB (Lit offs))        | isMap idA, isArray idB, offs < 1000 -> go slot prev
+      (ArraySlotWithOffs idA (Lit offs), Keccak idB)        | isArray idA, isMap idB, offs < 1000 -> go slot prev
+      (ArraySlotWithOffs idA (Lit offs), MappingSlot idB _) | isArray idA, isMap' idB, offs < 1000 -> go slot prev
 
       -- Fixed SMALL value will never match Keccak (well, it might, but that's VERY low chance)
       (Lit a, Keccak _) | a < 256 -> go slot prev
@@ -1079,6 +1088,10 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
       | x == 0 = b
       | otherwise = a
 
+    -- Masking as as per Solidity bit-packing of e.g. function parameters
+    go (And (Lit mask1) (Or (And (Lit mask2) _) x)) | (mask1 .&. mask2 == 0)
+         = And (Lit mask1) x
+
     -- address masking
     go (And (Lit 0xffffffffffffffffffffffffffffffffffffffff) a@(WAddr _)) = a
 

src/EVM/Solvers.hs

@@ -161,6 +161,7 @@ getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCo
       writeChan r Nothing
     Right _ -> do
       sat <- liftIO $ sendLine inst "(check-sat)"
+      when conf.dumpQueries $ liftIO $ writeSMT2File smt2 (show fileCounter <> "-origquery")
       subRun [] smt2 sat
   -- put the instance back in the list of available instances
   liftIO $ writeChan availableInstances inst

test/test.hs

@@ -2471,6 +2471,29 @@ tests = testGroup "hevm"
       putStrLnM $ "successfully explored: " <> show (Expr.numBranches expr) <> " paths"
       assertBoolM "The expression is NOT error" $ not $ any isError ret
       assertBoolM "The expression is NOT partial" $ not $ Expr.containsNode isPartial expr
+    , test "no-overapprox-when-present" $ do
+      Just c <- solcRuntime "C" [i|
+        contract ERC20 {
+          function f() public {
+          }
+        }
+
+        contract C {
+          address token;
+
+          function no_overapp() public {
+            token = address(new ERC20());
+            token.delegatecall(abi.encodeWithSignature("f()"));
+          }
+        } |]
+      let sig2 = Just (Sig "no_overapp()" [])
+      (expr, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig2 [] defaultVeriOpts
+      putStrLnM $ "expr: " <> show expr
+      putStrLnM $ "successfully explored: " <> show (Expr.numBranches expr) <> " paths"
+      assertBoolM "The expression is NOT error" $ not $ any isError ret
+      assertBoolM "The expression is NOT partial" $ not $ Expr.containsNode isPartial expr
+      let numCexes = sum $ map (fromEnum . isCex) ret
+      assertEqualM "number of counterexamples" 0 numCexes
     -- NOTE: below used to be symbolic copyslice copy error before new copyslice
     --       simplifications in Expr.simplify
     , test "overapproximates-undeployed-contract-symbolic" $ do
@@ -3953,8 +3976,7 @@ tests = testGroup "hevm"
                           _ -> False
           assertBoolM "Did not find expected storage cex" testCex
           putStrLnM "expected counterexample found"
-        ,
-        expectFail $ test "calling unique contracts (read from storage)" $ do
+        , test "calling-unique-contracts--read-from-storage" $ do
           Just c <- solcRuntime "C"
             [i|
               contract C {