Fix bug in SMT encoding of reading multiple consecutive bytes

The current encoding in function `assertReads` asserted, for a read of
more than one (and not 32) bytes, that the same expression is equal to
multiple different constants. This caused some problems to be trivially
unsatisfiable, possibly hiding other bugs.

The new encoding should hopefully fix that.
After running our test suite, it seems like this actually affected some
of our tests, because the overall runtime increased noticeably.

CHANGELOG.md

@@ -48,6 +48,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Multi-threaded running of Tracing.hs was not possible due to IO race. Fixed.
 - 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
 
 ## [0.53.0] - 2024-02-23
 

src/EVM/SMT.hs

@@ -404,12 +404,9 @@ assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop]
 assertReads props benv senv = concatMap assertRead allReads
   where
     assertRead :: (Expr EWord, Expr EWord, Expr Buf) -> [Prop]
+    assertRead (_, Lit 0, _) = []
     assertRead (idx, Lit 32, buf) = [PImpl (PGEq idx (bufLength buf)) (PEq (ReadWord idx buf) (Lit 0))]
-    assertRead (idx, Lit sz, buf) =
-      fmap
-        -- TODO: unsafeInto instead fromIntegral here makes symbolic tests fail
-        (PImpl (PGEq idx (bufLength buf)) . PEq (ReadByte idx buf) . LitByte . fromIntegral)
-        [(0::Int)..unsafeInto sz-1]
+    assertRead (idx, Lit sz, buf) = [PImpl (PGEq (Expr.add idx $ Lit offset) (bufLength buf)) (PEq (ReadByte (Expr.add idx $ Lit offset) buf) (LitByte 0)) | offset <- [(0::W256).. sz-1]]
     assertRead (_, _, _) = internalError "Cannot generate assertions for accesses of symbolic size"
 
     allReads = filter keepRead $ nubOrd $ findBufferAccess props <> findBufferAccess (Map.elems benv) <> findBufferAccess (Map.elems senv)

test/test.hs

@@ -545,7 +545,7 @@ tests = testGroup "hevm"
           b = Expr.simplify a
         ret <- checkEquiv a b
         assertBoolM "must be equivalent" ret
-    , ignoreTest $ test "read-beyond-bound (negative-test)" $ do
+    , test "read-beyond-bound (negative-test)" $ do
       let
         e1 = CopySlice (Lit 1) (Lit 0) (Lit 2) (ConcreteBuf "a") (ConcreteBuf "")
         e2 = ConcreteBuf "Definitely not the same!"