Merge pull request #926 from argotorg/simplifications-cleanup

Expr: Remove expensive unnecessary simplification

Author: blishko

CHANGELOG.md

@@ -18,6 +18,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   node via `--cache-dir dir`.
 - Changed `verify*` methods to always require postcodition.
 - Removed type parameter of mutable memory from VM definition.
+- Removed simplification that were rewriting concrete bytes-to-be-overwritten
+  with zero bytes. Benefits were unclear while it had negative effect on
+  analysis' performance.
 
 ## [0.56.0] - 2025-10-13
 

src/EVM/Expr.hs

@@ -1001,20 +1001,6 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
     go (ReadByte idx buf) = readByte idx buf
     go (BufLength buf) = bufLength buf
 
-    -- We can zero out any bytes in a base ConcreteBuf that we know will be overwritten by a later write
-    -- TODO: make this fully general for entire write chains, not just a single write.
-    go o@(WriteWord (Lit idx) val (ConcreteBuf b))
-      | idx >= maxBytes = o
-      | BS.length b >= (unsafeInto idx + 32) =
-          let
-            slot = BS.take 32 (BS.drop (unsafeInto idx) b)
-            isSlotZero = BS.all (== 0) slot
-            content = if isSlotZero
-              then b
-              else (BS.take (unsafeInto idx) b)
-                <> (BS.replicate 32 0)
-                <> (BS.drop (unsafeInto idx + 32) b)
-          in writeWord (Lit idx) val (ConcreteBuf content)
     go (WriteWord a b c) = writeWord a b c
 
     go (WriteByte a b c) = writeByte a b c