Merge pull request #597 from ethereum/revert-wrapping-semantics

Revert wraparound semantics for reading from buffers

CHANGELOG.md

@@ -60,7 +60,6 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   and hence lead to false negatives through trivially UNSAT SMT expressions
 - Respect --smt-timeout in equivalence checking
 - Fixed the handling of returndata with an abstract size during transaction finalization
-- Fixed handling of indices overflowing 2^256 when reading from buffers
 - Error handling for user-facing cli commands is much improved
 
 ## [0.53.0] - 2024-02-23

src/EVM/Expr.hs

@@ -290,16 +290,10 @@ readWord i b = readWordFromBytes i b
 -- Attempts to read a concrete word from a buffer by reading 32 individual bytes and joining them together
 -- returns an abstract ReadWord expression if a concrete word cannot be constructed
 readWordFromBytes :: Expr EWord -> Expr Buf -> Expr EWord
-readWordFromBytes (Lit idx) (ConcreteBuf bs)
-  | idx + 32 < idx = let
-    -- Overflowing, part of the read will be from the beginning of src
-      hd = BS.replicate (unsafeInto (maxWord256 - idx) + 1) 0
-      tl = BS.take (32 - BS.length hd) bs
-    in Lit $ word $ hd <> tl
-  | otherwise =
-    case tryInto idx of
-      Left _ -> Lit 0
-      Right i -> Lit $ word $ padRight 32 $ BS.take 32 $ BS.drop i bs
+readWordFromBytes (Lit idx) (ConcreteBuf bs) =
+  case tryInto idx of
+    Left _ -> Lit 0
+    Right i -> Lit $ word $ padRight 32 $ BS.take 32 $ BS.drop i bs
 readWordFromBytes i@(Lit idx) buf = let
     bytes = [readByte (Lit i') buf | i' <- [idx .. idx + 31]]
   in if all isLitByte bytes
@@ -344,16 +338,7 @@ copySlice a@(Lit srcOffset) b@(Lit dstOffset) c@(Lit size) d@(ConcreteBuf src) e
   , size < maxBytes =
       let hd = padRight (unsafeInto dstOffset) $ BS.take (unsafeInto dstOffset) dst
           sl = if srcOffset > unsafeInto (BS.length src)
-            then
-              if srcOffset + size < srcOffset -- overflow, read will continue from begining of the buffer
-                then
-                  let headSize = (maxWord256 - srcOffset) + 1
-                      tailSize = size - headSize
-                      sliceHead = BS.replicate (unsafeInto headSize) 0
-                      sliceTail = padRight (unsafeInto tailSize) $ BS.take (unsafeInto tailSize) src
-                   in
-                    sliceHead <> sliceTail
-                else BS.replicate (unsafeInto size) 0
+            then BS.replicate (unsafeInto size) 0
             else padRight (unsafeInto size) $ BS.take (unsafeInto size) (BS.drop (unsafeInto srcOffset) src)
           tl = BS.drop (unsafeInto dstOffset + unsafeInto size) dst
       in ConcreteBuf $ hd <> sl <> tl

test/test.hs

@@ -705,6 +705,11 @@ tests = testGroup "hevm"
         y <- checkEquivAndLHS x simplified
         assertBoolM "Must be equal" y
     ]
+  {- NOTE: These tests were designed to test behaviour on reading from a buffer such that the indices overflow 2^256.
+           However, such scenarios are impossible in the real world (the operation would run out of gas). The problem
+           is that the behaviour of bytecode interpreters does not match the semantics of SMT. Intrepreters just
+           return all zeroes for any read beyond buffer size, while in SMT reading multiple bytes may lead to overflow
+           on indices and subsequently to reading from the beginning of the buffer (wrap-around semantics).
   , testGroup "concrete-buffer-simplification-large-index" [
       test "copy-slice-large-index-nooverflow" $ do
         let
@@ -736,13 +741,8 @@ tests = testGroup "hevm"
           s = Expr.simplify e
         equal <- checkEquiv e s
         assertEqualM "Must be equal" True equal
-    , test "copy-slice-overflowing-into-too-short-buffer" $ do
-        let
-          e = BufLength (CopySlice (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) (Lit 0x00) (Lit 0x02) (ConcreteBuf "") (ConcreteBuf ""))
-          s = Expr.simplify e
-        equal <- checkEquiv e s
-        assertEqualM "Must be equal" True equal
   ]
+  -}
   , testGroup "isUnsat-concrete-tests" [
       test "disjunction-left-false" $ do
         let