[DRAFT] Zero-sized arrays imply the default, empty array, and vica versa

CHANGELOG.md

@@ -35,6 +35,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Dumping of END states (.prop) files is now default for `--debug`
 - When cheatcode is missing, we produce a partial execution warning
 - Size of calldata can be up to 2**64, not 256. This is now reflected in the documentation
+- Zero-length buffers actually imply all-zero buffer, and vica-versa. This
+  was assumed but not encoded. Fixed.
 
 ## Changed
 - Warnings now lead printing FAIL. This way, users don't accidentally think that

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

test/test.hs

@@ -545,6 +545,13 @@ tests = testGroup "hevm"
           simp = Expr.simplify e
       res <- checkEquiv e simp
       assertEqualM "readWord simplification"  res True
+    , 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")