Merge pull request #411 from ethereum/fixing-mem-explode

Fixing mem explosion issue

CHANGELOG.md

@@ -52,6 +52,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - CopySlice+WriteWord+ConcreteBuf now truncates ConcreteBuf in special cases
 - Better simplification of Eq IR elements
 - Run a toplevel constant folding reasoning system on branch conditions
+- Mem explosion in `writeWord` function was possible in case `offset` was close to 2^256. Fixed.
 
 ## API Changes
 

src/EVM/Expr.hs

@@ -374,13 +374,13 @@ writeByte offset byte src = WriteByte offset byte src
 
 writeWord :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf
 writeWord o@(Lit offset) (WAddr (LitAddr val)) b@(ConcreteBuf _)
-  | offset + 32 < maxBytes
+  | offset < maxBytes && offset + 32 < maxBytes
   = writeWord o (Lit $ into val) b
 writeWord (Lit offset) (Lit val) (ConcreteBuf "")
-  | offset + 32 < maxBytes
+  | offset < maxBytes && offset + 32 < maxBytes
   = ConcreteBuf $ BS.replicate (unsafeInto offset) 0 <> word256Bytes val
 writeWord o@(Lit offset) v@(Lit val) buf@(ConcreteBuf src)
-  | offset + 32 < maxBytes
+  | offset < maxBytes && offset + 32 < maxBytes
     = ConcreteBuf $ (padRight (unsafeInto offset) $ BS.take (unsafeInto offset) src)
                  <> word256Bytes val
                  <> BS.drop ((unsafeInto offset) + 32) src