Merge pull request #582 from ethereum/make-hash-take-two-args

Fix keccak + sha256 to take 2 params: buf + len

CHANGELOG.md

@@ -32,7 +32,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - More verbose error messages in case of symbolic arguments to opcode
 - Tests to enforce that in Expr and Prop, constants are on the LHS whenever possible
 - Support for MCOPY and TSTORE/TLOAD, i.e. EIP 5656 + 1153 + 4788
-* Fuzz via both SAT and UNSAT, not just UNSAT
+- All fuzz tests now run twice, once with expected SAT and once with expected UNSAT to check
+  against incorrectly trivial UNSAT queries
 
 ## Fixed
 - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing
@@ -50,6 +51,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Fixed multi-threading bug in symbolic interpretation
 - Fixed simplification of concrete CopySlice with destination offset beyond destination size
 - Fixed a bug in our SMT encoding of reading multiple consecutive bytes from concrete index
+- Fixed bug in SMT encoding that caused empty and all-zero byte arrays to be considered equal
+  and hence lead to false negatives through trivially UNSAT SMT expressions
 
 ## [0.53.0] - 2024-02-23
 

src/EVM/SMT.hs

@@ -509,9 +509,11 @@ prelude =  SMT2 src mempty mempty mempty
   ; slot -> value
   (define-sort Storage () (Array Word Word))
 
-  ; hash functions
-  (declare-fun keccak (Buf) Word)
-  (declare-fun sha256 (Buf) Word)
+  ; hash functions. They take buffer and a buffer size, and return a Word
+  (declare-fun keccak (Buf Word) Word)
+  (declare-fun sha256 (Buf Word) Word)
+
+  ; helper functions
   (define-fun max ((a (_ BitVec 256)) (b (_ BitVec 256))) (_ BitVec 256) (ite (bvult a b) b a))
 
   ; word indexing
@@ -788,12 +790,14 @@ exprToSMT = \case
   EqByte a b ->
     let cond = op2 "=" a b in
     "(ite " <> cond `sp` one `sp` zero <> ")"
-  Keccak a ->
-    let enc = exprToSMT a in
-    "(keccak " <> enc <> ")"
-  SHA256 a ->
-    let enc = exprToSMT a in
-    "(sha256 " <> enc <> ")"
+  Keccak a -> let
+      enc = exprToSMT a
+      sz = exprToSMT $ Expr.bufLength a
+    in "(keccak " <> enc <> " " <> sz <> ")"
+  SHA256 a -> let
+      enc = exprToSMT a
+      sz = exprToSMT $ Expr.bufLength a
+    in "(sha256 " <> enc <> " " <> sz <> ")"
 
   TxValue -> fromString "txvalue"
   Balance a -> fromString "balance_" <> formatEAddr a

test/test.hs

@@ -562,7 +562,7 @@ tests = testGroup "hevm"
   -- applying some simplification rules, and then using the smt encoding to
   -- check that the simplified version is semantically equivalent to the
   -- unsimplified one
-  , adjustOption (\(Test.Tasty.QuickCheck.QuickCheckTests n) -> Test.Tasty.QuickCheck.QuickCheckTests (min n 50)) $ testGroup "SimplifierTests"
+  , adjustOption (\(Test.Tasty.QuickCheck.QuickCheckTests n) -> Test.Tasty.QuickCheck.QuickCheckTests (div n 2)) $ testGroup "SimplifierTests"
     [ testProperty  "buffer-simplification" $ \(expr :: Expr Buf) -> prop $ do
         let simplified = Expr.simplify expr
         checkEquivAndLHS expr simplified
@@ -692,6 +692,12 @@ tests = testGroup "hevm"
         let s2 = Expr.structureArraySlots s
         let simplified = Expr.simplify s2
         checkEquivAndLHS s2 simplified
+    , test "storage-slot-single" $ do
+        -- this tests that "" and "0"x32 is not equivalent in Keccak
+        let x = SLoad (Add (Keccak (ConcreteBuf "")) (Lit 1)) (SStore (Keccak (ConcreteBuf "\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL")) (Lit 0) (AbstractStore (SymAddr "stuff") Nothing))
+        let simplified = Expr.simplify x
+        y <- checkEquivAndLHS x simplified
+        assertBoolM "Must be equal" y
     ]
   , testGroup "isUnsat-concrete-tests" [
       test "disjunction-left-false" $ do