From 985751aaa7a89ed4ec648ed61e1c1dc67c715ac8 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 17 Feb 2025 19:28:32 +0100
Subject: [PATCH] Fixing bug #664

---
 src/EVM/SMT.hs | 10 +++++++++-
 test/test.hs   |  7 +++++++
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index 5f46cd789..03cf34ff1 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -420,12 +420,20 @@ discoverMaxReads props benv senv = bufMap
 
 -- | Returns an SMT2 object with all buffers referenced from the input props declared, and with the appropriate cex extraction metadata attached
 declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2
-declareBufs props bufEnv storeEnv = SMT2 ("; buffers" : fmap declareBuf allBufs <> ("; buffer lengths" : fmap declareLength allBufs)) cexvars mempty
+declareBufs props bufEnv storeEnv =
+  SMT2 (smtBufNames <> smtBufLengths <> smtEmptyRelations) cexvars mempty
   where
+    smtBufNames = "; buffers" : fmap declareBuf allBufs
+    smtBufLengths = "; buffer lengths" : fmap declareLength allBufs
+    smtEmptyRelations = "; empty buffer relations" : concatMap emptyRelation allBufs
     cexvars = (mempty :: CexVars){ buffers = discoverMaxReads props bufEnv storeEnv }
     allBufs = fmap fromLazyText $ Map.keys cexvars.buffers
     declareBuf n = "(declare-fun " <> n <> " () (Array (_ BitVec 256) (_ BitVec 8)))"
     declareLength n = "(declare-fun " <> n <> "_length" <> " () (_ BitVec 256))"
+    emptyRelation buf =
+      let bufLen = buf <> "_length"
+      in  ["(assert (=> (= " <> bufLen <> " (_ bv0 256)) (= " <> buf <> " ((as const Buf) #b00000000)) ))"
+          , "(assert (=> (= " <> buf <> " ((as const Buf) #b00000000)) (= " <> bufLen <> " (_ bv0 256)) ))" ]
 
 -- Given a list of variable names, create an SMT2 object with the variables declared
 declareVars :: [Builder] -> SMT2
diff --git a/test/test.hs b/test/test.hs
index 6f881c02c..726ce332d 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -515,6 +515,13 @@ 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-empty-buflength" $ do
+      let e = PEq (BufLength (AbstractBuf "mybuf")) (Lit 0)
+      let simp = Expr.simplifyProp e
+      let simpExpected = PEq (AbstractBuf "mybuf") (ConcreteBuf "")
+      assertEqualM "buflen-to-empty" simp simpExpected
+      ret <- checkEquivPropAndLHS e simpExpected
+      assertBoolM "Must be equivalent" ret
     , test "simp-max-buflength" $ do
       let simp = Expr.simplify $ Max (Lit 0) (BufLength (AbstractBuf "txdata"))
       assertEqualM "max-buflength rules" simp $ BufLength (AbstractBuf "txdata")