Merge pull request #655 from ethereum/more-simpl-as-needed

Two simplifications that will be needed to deal with @zoep's issues regarding initcode equivalence

CHANGELOG.md

@@ -20,6 +20,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   generated via iterative calls to the SMT solver for quicker solving
 - Aliasing works much better for symbolic and concrete addresses
 - Constant propagation for symbolic values
+- Two more simplification rules: `ReadByte` & `ReadWord` when the `CopySlice`
+  it is reading from is writing after the position being read, so the
+  `CopySlice` can be ignored
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value

src/EVM/Expr.hs

@@ -243,6 +243,9 @@ readByte i@(Lit x) (WriteWord (Lit idx) val src)
            (Lit _) -> indexWord (Lit $ x - idx) val
            _ -> IndexWord (Lit $ x - idx) val
     else readByte i src
+-- reading a byte that is lower than the dstOffset of a CopySlice, so it's just reading from dst
+readByte i@(Lit x) (CopySlice _ (Lit dstOffset) _ _ dst) | dstOffset > x =
+  readByte i dst
 readByte i@(Lit x) (CopySlice (Lit srcOffset) (Lit dstOffset) (Lit size) src dst)
   = if x - dstOffset < size
     then readByte (Lit $ x - (dstOffset - srcOffset)) src
@@ -279,6 +282,9 @@ readWord idx b@(WriteWord idx' val buf)
     -- we do not have enough information to statically determine whether or not
     -- the region we want to read overlaps the WriteWord
     _ -> readWordFromBytes idx b
+-- reading a Word that is lower than the dstOffset-32 of a CopySlice, so it's just reading from dst
+readWord i@(Lit x) (CopySlice _ (Lit dstOffset) _ _ dst) | dstOffset > x+32 =
+  readWord i dst
 readWord (Lit idx) b@(CopySlice (Lit srcOff) (Lit dstOff) (Lit size) src dst)
   -- the region we are trying to read is enclosed in the sliced region
   | (idx - dstOff) < size && 32 <= size - (idx - dstOff) = readWord (Lit $ srcOff + (idx - dstOff)) src

test/test.hs

@@ -515,6 +515,36 @@ tests = testGroup "hevm"
         let e = BufLength (CopySlice (Lit 0x2) (Lit 0x2) (Lit 0x1) (ConcreteBuf "") (ConcreteBuf ""))
         b <- checkEquiv e (Expr.simplify e)
         assertBoolM "Simplifier failed" b
+    , test "simp-readByte1" $ do
+      let srcOffset = (ReadWord (Lit 0x1) (AbstractBuf "stuff1"))
+          size = (ReadWord (Lit 0x1) (AbstractBuf "stuff2"))
+          src = (AbstractBuf "stuff2")
+          e = ReadByte (Lit 0x0) (CopySlice srcOffset (Lit 0x10) size src (AbstractBuf "dst"))
+          simp = Expr.simplify e
+      assertEqualM "readByte simplification" simp (ReadByte (Lit 0x0) (AbstractBuf "dst"))
+    , test "simp-readByte2" $ do
+      let srcOffset = (ReadWord (Lit 0x1) (AbstractBuf "stuff1"))
+          size = (Lit 0x1)
+          src = (AbstractBuf "stuff2")
+          e = ReadByte (Lit 0x0) (CopySlice srcOffset (Lit 0x10) size src (AbstractBuf "dst"))
+          simp = Expr.simplify e
+      res <- checkEquiv e simp
+      assertEqualM "readByte simplification"  res True
+    , test "simp-readWord1" $ do
+      let srcOffset = (ReadWord (Lit 0x1) (AbstractBuf "stuff1"))
+          size = (ReadWord (Lit 0x1) (AbstractBuf "stuff2"))
+          src = (AbstractBuf "stuff2")
+          e = ReadWord (Lit 0x1) (CopySlice srcOffset (Lit 0x40) size src (AbstractBuf "dst"))
+          simp = Expr.simplify e
+      assertEqualM "readWord simplification" simp (ReadWord (Lit 0x1) (AbstractBuf "dst"))
+    , test "simp-readWord2" $ do
+      let srcOffset = (ReadWord (Lit 0x12) (AbstractBuf "stuff1"))
+          size = (Lit 0x1)
+          src = (AbstractBuf "stuff2")
+          e = ReadWord (Lit 0x12) (CopySlice srcOffset (Lit 0x50) size src (AbstractBuf "dst"))
+          simp = Expr.simplify e
+      res <- checkEquiv e simp
+      assertEqualM "readWord simplification"  res True
     , test "simp-max-buflength" $ do
       let simp = Expr.simplify $ Max (Lit 0) (BufLength (AbstractBuf "txdata"))
       assertEqualM "max-buflength rules" simp $ BufLength (AbstractBuf "txdata")
@@ -562,10 +592,6 @@ tests = testGroup "hevm"
         a = BufLength (ConcreteBuf "ab")
         simp = Expr.simplify a
       assertEqualM "Must be simplified down to a Lit" simp (Lit 2)
-    , test "CopySlice-overflow" $ do
-        let e = ReadWord (Lit 0x0) (CopySlice (Lit 0x0) (Lit 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc) (Lit 0x6) (ConcreteBuf "\255\255\255\255\255\255") (ConcreteBuf ""))
-        b <- checkEquiv e (Expr.simplify e)
-        assertBoolM "Simplifier failed" b
     , test "stripWrites-overflow" $ do
         -- below eventually boils down to
         -- unsafeInto (0xf0000000000000000000000000000000000000000000000000000000000000+1) :: Int