RFC: allow to concretize dynamic arrays in calldata up to N values

cli/cli.hs

@@ -102,6 +102,7 @@ data CommonOptions = CommonOptions
   , cacheDir      ::Maybe String
   , earlyAbort    ::Bool
   , mergeMaxBudget :: Int
+  , maxDynSize    ::Int
   }
 
 commonOptions :: Parser CommonOptions
@@ -133,6 +134,7 @@ commonOptions = CommonOptions
   <*> (optional $ strOption $ long "cache-dir" <> help "Directory to save and load RPC cache")
   <*> (switch $  long "early-abort" <> help "Stop exploration immediately upon finding the first counterexample")
   <*> (option auto $ long "merge-max-budget" <> showDefault <> value 100 <> help "Max instructions for speculative merge exploration during path merging")
+  <*> (option auto $ long "max-dyn-size" <> showDefault <> value 64 <> help "Max byte length for concretized dynamic types (bytes, string) in symbolic arguments")
 
 data CommonExecOptions = CommonExecOptions
   { address       ::Maybe Addr
@@ -377,6 +379,7 @@ main = do
         , onlyDeployed = cOpts.onlyDeployed
         , earlyAbort = cOpts.earlyAbort
         , mergeMaxBudget = cOpts.mergeMaxBudget
+        , maxDynSize = cOpts.maxDynSize
         } }
 
 

src/EVM/Effects.hs

@@ -48,6 +48,7 @@ data Config = Config
   , onlyDeployed     :: Bool
   , earlyAbort       :: Bool
   , mergeMaxBudget   :: Int        -- ^ Max instructions for speculative merge exploration
+  , maxDynSize       :: Int        -- ^ Max byte length for concretized dynamic types (bytes, string)
   }
   deriving (Show, Eq)
 
@@ -69,6 +70,7 @@ defaultConfig = Config
   , onlyDeployed = False
   , earlyAbort = False
   , mergeMaxBudget = 100
+  , maxDynSize = 64
   }
 
 -- Write to the console

src/EVM/Format.hs

@@ -521,6 +521,10 @@ formatPartial = \case
       , "contract addr: " <> pack (show addr)
       , "program counter: " <> pack (show pc)]
     ]
+  DynamicArgBounded maxSz -> T.unlines
+    ["Dynamic argument (bytes/string) concretized to max " <> pack (show maxSz) <> " bytes."
+    , indent 2 "Counterexamples beyond this bound may be missed."
+    ]
 
 
 formatPartialDetailed :: Maybe SrcLookup -> Map.Map (Expr EAddr) Contract -> PartialExec -> Text
@@ -533,6 +537,7 @@ formatPartialDetailed srcLookupM contracts p =
     CheatCodeMissing {..}      -> "Cheat code not recognized: " <> T.pack (show selector) <> toTxt addr pc
     PrecompileMissing {..}     -> "Precompile at address " <> pack (show preAddr) <> " does not exist, called from" <> toTxt addr pc
     BranchTooDeep {..}         -> "Branches too deep" <> toTxt addr pc
+    DynamicArgBounded {..}     -> "Dynamic argument (bytes/string) concretized to max " <> pack (show maxSize) <> " bytes; counterexamples beyond this bound may be missed"
 
 formatSomeExpr :: SomeExpr -> Text
 formatSomeExpr (SomeExpr e) = formatExpr $ Expr.simplify e

src/EVM/SymExec.hs

@@ -116,8 +116,8 @@ extractCex _ = Nothing
 
 
 -- | Abstract calldata argument generation
-symAbiArg :: Text -> AbiType -> CalldataFragment
-symAbiArg name = \case
+symAbiArg :: Int -> Text -> AbiType -> CalldataFragment
+symAbiArg maxDynSize name = \case
   AbiUIntType n ->
     if n `mod` 8 == 0 && n <= 256
     then St [] v
@@ -133,16 +133,29 @@ symAbiArg name = \case
     then St [] v
     else internalError "bad type"
   AbiArrayType sz tps -> do
-    Comp . V.toList . V.imap (\(T.pack . show -> i) tp -> symAbiArg (name <> "-a-" <> i) tp) $ (V.replicate sz tps)
+    Comp . V.toList . V.imap (\(T.pack . show -> i) tp -> symAbiArg maxDynSize (name <> "-a-" <> i) tp) $ (V.replicate sz tps)
   AbiTupleType tps ->
-    Comp . V.toList . V.imap (\(T.pack . show -> i) tp -> symAbiArg (name <> "-t-" <> i) tp) $ tps
+    Comp . V.toList . V.imap (\(T.pack . show -> i) tp -> symAbiArg maxDynSize (name <> "-t-" <> i) tp) $ tps
+  -- Dynamic bytes/string: concretize with bounded symbolic length + abstract buffer
+  AbiBytesDynamicType ->
+    let bufName = AbstractBuf (name <> "-bytes")
+        len = Var (name <> "-bytes-length")
+        maxLit = Lit (fromIntegral maxDynSize)
+        sizeBound = [PLEq len maxLit]
+    in Dy sizeBound len maxDynSize bufName
+  AbiStringType ->
+    let bufName = AbstractBuf (name <> "-string")
+        len = Var (name <> "-string-length")
+        maxLit = Lit (fromIntegral maxDynSize)
+        sizeBound = [PLEq len maxLit]
+    in Dy sizeBound len maxDynSize bufName
   t -> internalError $ "TODO: symbolic abi encoding for " <> show t
   where
     v = Var name
 
 data CalldataFragment
   = St [Prop] (Expr EWord)
-  | Dy [Prop] (Expr EWord) (Expr Buf)
+  | Dy [Prop] (Expr EWord) Int (Expr Buf) -- ^ props, symbolic length, max concrete size, buffer
   | Comp [CalldataFragment]
   deriving (Show, Eq)
 
@@ -156,7 +169,7 @@ symCalldata sig typesignature concreteArgs base = do
   let
     args = concreteArgs <> replicate (length typesignature - length concreteArgs) "<symbolic>"
     mkArg :: AbiType -> String -> Int -> CalldataFragment
-    mkArg typ "<symbolic>" n = symAbiArg (T.pack $ "arg" <> show n) typ
+    mkArg typ "<symbolic>" n = symAbiArg conf.maxDynSize (T.pack $ "arg" <> show n) typ
     mkArg typ arg _ =
       case makeAbiValue typ arg of
         AbiUInt _ w -> St [] . Lit . into $ w
@@ -173,14 +186,29 @@ symCalldata sig typesignature concreteArgs base = do
   pure (withSelector, sizeConstraints : props)
 
 cdLen :: [CalldataFragment] -> Expr EWord
-cdLen = go (Lit 4)
+cdLen frags = Expr.add (headLen frags) (tailLen frags)
   where
-    go acc = \case
-      [] -> acc
-      (hd:tl) -> case hd of
-                   St _ _ -> go (Expr.add acc (Lit 32)) tl
-                   Comp xs | all isSt xs -> go acc (xs <> tl)
-                   _ -> internalError "unsupported"
+    -- Head: 4 bytes selector + 32 bytes per top-level arg (static or dynamic pointer)
+    headLen = go (Lit 4)
+      where
+        go acc = \case
+          [] -> acc
+          (hd:tl) -> case hd of
+            St _ _  -> go (Expr.add acc (Lit 32)) tl
+            Dy {}   -> go (Expr.add acc (Lit 32)) tl
+            Comp xs | all isSt xs -> go acc (xs <> tl)
+            _ -> internalError "unsupported"
+    -- Tail: for each Dy fragment, 32 bytes (length word) + padded data
+    tailLen = go (Lit 0)
+      where
+        go acc = \case
+          [] -> acc
+          (hd:tl) -> case hd of
+            Dy _ _ maxSz _ ->
+              let paddedMax = ((maxSz + 31) `Prelude.div` 32) * 32
+              in go (Expr.add acc (Lit (fromIntegral (32 + paddedMax)))) tl
+            Comp xs | all isSt xs -> go acc (xs <> tl)
+            _ -> go acc tl
 
 writeSelector :: Expr Buf -> Text -> Expr Buf
 writeSelector buf sig =
@@ -190,17 +218,48 @@ writeSelector buf sig =
     writeSel idx = Expr.writeByte idx (Expr.readByte idx sel)
 
 combineFragments :: [CalldataFragment] -> Expr Buf -> (Expr Buf, [Prop])
-combineFragments fragments base = go (Lit 4) fragments (base, [])
+combineFragments fragments base =
+  let headBytes = countHeadBytes fragments
+      tailStart = Expr.add (Lit 4) headBytes
+  in go headBytes (Lit 4) tailStart (Lit 0) fragments (base, [])
   where
-    go :: Expr EWord -> [CalldataFragment] -> (Expr Buf, [Prop]) -> (Expr Buf, [Prop])
-    go _ [] acc = acc
-    go idx (f:rest) (buf, ps) =
+    -- Each top-level fragment occupies 32 bytes in the head (value or offset pointer)
+    countHeadBytes :: [CalldataFragment] -> Expr EWord
+    countHeadBytes = foldl' countFrag (Lit 0)
+      where
+        countFrag acc (St _ _)  = Expr.add acc (Lit 32)
+        countFrag acc (Dy {})   = Expr.add acc (Lit 32)
+        countFrag acc (Comp xs) | all isSt xs = foldl' countFrag acc xs
+        countFrag _ s = internalError $ "unsupported cd fragment: " <> show s
+
+    go :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
+       -> [CalldataFragment] -> (Expr Buf, [Prop]) -> (Expr Buf, [Prop])
+    go _ _ _ _ [] acc = acc
+    go headSz idx tailBase tailAcc (f:rest) (buf, ps) =
       case f of
         -- static fragments get written as a word in place
-        St p w -> go (Expr.add idx (Lit 32)) rest (Expr.writeWord idx w buf, p <> ps)
+        St p w -> go headSz (Expr.add idx (Lit 32)) tailBase tailAcc rest
+                    (Expr.writeWord idx w buf, p <> ps)
         -- compound fragments that contain only static fragments get written in place
-        Comp xs | all isSt xs -> go idx (xs <> rest) (buf,ps)
-        -- dynamic fragments are not yet supported... :/
+        Comp xs | all isSt xs -> go headSz idx tailBase tailAcc (xs <> rest) (buf, ps)
+        -- dynamic fragments: write offset pointer in head, data in tail
+        Dy p len maxSz dynBuf ->
+          let paddedMax = ((maxSz + 31) `Prelude.div` 32) * 32
+              -- ABI offset is relative to the start of the args (byte 4)
+              offset = Expr.add headSz tailAcc
+              -- Write the offset pointer in the head area
+              buf1 = Expr.writeWord idx offset buf
+              -- Write the length word at the tail position
+              dynPos = Expr.add tailBase tailAcc
+              buf2 = Expr.writeWord dynPos len buf1
+              -- Copy maxDynSize bytes from the abstract buffer using concrete
+              -- size to avoid symbolic CopySlice issues
+              dataPos = Expr.add dynPos (Lit 32)
+              buf3 = Expr.copySlice (Lit 0) dataPos (Lit (fromIntegral maxSz)) dynBuf buf2
+              -- Advance tail by 32 (length word) + paddedMax
+              newTailAcc = Expr.add tailAcc (Lit (fromIntegral (32 + paddedMax)))
+          in go headSz (Expr.add idx (Lit 32)) tailBase newTailAcc rest
+               (buf3, p <> ps)
         s -> internalError $ "unsupported cd fragment: " <> show s
 
 isSt :: CalldataFragment -> Bool
@@ -682,10 +741,18 @@ verifyContract :: forall m . App m
   -> Postcondition
   -> m ([Expr End], [VerifyResult])
 verifyContract solvers theCode signature' concreteArgs opts maybepre post = do
+  conf <- readConfig
   calldata <- mkCalldata signature' concreteArgs
   preState <- liftIO $ stToIO $ abstractVM calldata theCode maybepre False
   let fetcher = Fetch.oracle solvers Nothing opts.rpcInfo
-  verify solvers fetcher opts preState post Nothing
+  (ends, results) <- verify solvers fetcher opts preState post Nothing
+  -- If the signature has dynamic types, the exploration is bounded by maxDynSize.
+  -- Inject a Partial end state so the user knows the result may be incomplete.
+  let hasDynArgs = case signature' of
+        Just (Sig _ types) -> any (\t -> abiKind t == Dynamic) types
+        Nothing -> False
+      dynPartial = [Partial [] (TraceContext mempty mempty mempty) (DynamicArgBounded conf.maxDynSize)]
+  pure (if hasDynArgs then ends <> dynPartial else ends, results)
 
 -- Used only in testing
 exploreContract :: forall m . App m

src/EVM/Types.hs

@@ -598,6 +598,7 @@ data PartialExec
   | PrecompileMissing     { pc :: Int, addr :: Expr EAddr, preAddr :: Addr }
   | CheatCodeMissing      { pc :: Int, addr :: Expr EAddr, selector :: FunctionSelector }
   | BranchTooDeep         { pc :: Int, addr :: Expr EAddr}
+  | DynamicArgBounded     { maxSize :: Int }
   deriving (Show, Eq, Ord)
 
 -- | Effect types used by the vm implementation for side effects & control flow

src/EVM/UnitTest.hs

@@ -281,8 +281,13 @@ symRun opts@UnitTestOptions{..} vm sig@(Sig testName types) sourceCache = do
     -- check postconditions against vm
     let fetcherSym = Fetch.oracle solvers (Just sess) rpcInfo
     let symVm = symbolify vm' & set #srcLookup (Just $ makeSrcLookup dapp sourceCache)
-    (ends, results) <- verify solvers fetcherSym (makeVeriOpts opts) symVm postcondition (Just $ cexHandler cd fetcherConc)
+    (ends0, results) <- verify solvers fetcherSym (makeVeriOpts opts) symVm postcondition (Just $ cexHandler cd fetcherConc)
     conf <- readConfig
+    -- If the signature has dynamic types, exploration is bounded by maxDynSize.
+    -- Inject a Partial end state so the user knows the result may be incomplete.
+    let hasDynArgs = any (\t -> abiKind t == Dynamic) types
+        dynPartial = Partial [] (TraceContext mempty mempty mempty) (DynamicArgBounded conf.maxDynSize)
+        ends = if hasDynArgs then ends0 <> [dynPartial] else ends0
     when (conf.debug) $ liftIO $ do
       putStrLn $ "   \x1b[94m[EXPLORATION COMPLETE]\x1b[0m " <> Text.unpack testName <> " -- explored " <> show (length ends) <> " paths."
       when (conf.verb >= 2) $ do

test/test.hs

@@ -477,7 +477,7 @@ tests = testGroup "hevm"
                 AbiTuple (V.toList -> [e]) -> e
                 _ -> internalError "AbiTuple expected"
           let
-              frag = [symAbiArg "y" (AbiTupleType $ V.fromList [abiValueType y])]
+              frag = [symAbiArg 64 "y" (AbiTupleType $ V.fromList [abiValueType y])]
               (hevmEncoded, _) = first (Expr.drop 4) $ combineFragments frag (ConcreteBuf "")
               expectedVals = expectedConcVals "y" (AbiTuple . V.fromList $ [y])
               hevmConcretePre = fromRight (error "cannot happen") $ subModel expectedVals hevmEncoded
@@ -536,6 +536,117 @@ tests = testGroup "hevm"
           assertEqualM "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)
     ]
 
+  , testGroup "Dynamic-bytes-concretization"
+    [ test "bytes-length-cex" $ do
+        -- A function that asserts bytes.length == 0 should have a counterexample
+        Just c <- solcRuntime "C" [i|
+            contract C {
+              function fun(bytes calldata data) public pure {
+                assert(data.length == 0);
+              }
+            } |]
+        let sig = Just $ Sig "fun(bytes)" [AbiBytesDynamicType]
+        (e, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        -- bytes args always produce a partial (bounded concretization)
+        assertBoolM "should be partial due to bounded bytes" $ any isPartial e
+        let numCexes = sum $ map (fromEnum . isCex) ret
+        assertEqualM "should find counterexample" 1 numCexes
+    , test "bytes-content-cex" $ do
+        -- Should find bytes starting with 0xdead
+        Just c <- solcRuntime "C" [i|
+            contract C {
+              function fun(bytes calldata data) public pure {
+                if (data.length >= 2) {
+                  assert(data[0] != 0xde || data[1] != 0xad);
+                }
+              }
+            } |]
+        let sig = Just $ Sig "fun(bytes)" [AbiBytesDynamicType]
+        (e, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        assertBoolM "should be partial due to bounded bytes" $ any isPartial e
+        let numCexes = sum $ map (fromEnum . isCex) ret
+        assertEqualM "should find counterexample" 1 numCexes
+    , test "bytes-no-cex" $ do
+        -- A trivially true assertion should have no counterexample (but still partial)
+        Just c <- solcRuntime "C" [i|
+            contract C {
+              function fun(bytes calldata data) public pure {
+                assert(data.length <= data.length);
+              }
+            } |]
+        let sig = Just $ Sig "fun(bytes)" [AbiBytesDynamicType]
+        (e, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        assertBoolM "should be partial due to bounded bytes" $ any isPartial e
+        let numCexes = sum $ map (fromEnum . isCex) ret
+        assertEqualM "should have no counterexample" 0 numCexes
+    , test "bytes-with-uint-arg" $ do
+        -- bytes alongside a uint256 argument
+        Just c <- solcRuntime "C" [i|
+            contract C {
+              function fun(uint256 x, bytes calldata data) public pure {
+                if (data.length > 0 && x == 42) {
+                  assert(false);
+                }
+              }
+            } |]
+        let sig = Just $ Sig "fun(uint256,bytes)" [AbiUIntType 256, AbiBytesDynamicType]
+        (e, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        assertBoolM "should be partial due to bounded bytes" $ any isPartial e
+        let numCexes = sum $ map (fromEnum . isCex) ret
+        assertEqualM "should find counterexample" 1 numCexes
+    -- Tests that bugs beyond maxDynSize are reported as partial, not as false passes
+    , test "bytes-beyond-bound-length-check" $ do
+        -- Bug only triggers when bytes.length > 100; with default maxDynSize=64, should NOT find cex
+        -- but must report partial exploration
+        Just c <- solcRuntime "C" [i|
+            contract C {
+              function fun(bytes calldata data) public pure {
+                if (data.length > 100) {
+                  assert(false);
+                }
+              }
+            } |]
+        let sig = Just $ Sig "fun(bytes)" [AbiBytesDynamicType]
+        (e, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        assertBoolM "must report partial due to bounded bytes" $ any isPartial e
+        let numCexes = sum $ map (fromEnum . isCex) ret
+        assertEqualM "should not find cex (bug is beyond bound)" 0 numCexes
+    , test "bytes-beyond-bound-content-check" $ do
+        -- Bug triggers only when byte at index 80 has a specific value; beyond default maxDynSize=64
+        Just c <- solcRuntime "C" [i|
+            contract C {
+              function fun(bytes calldata data) public pure {
+                if (data.length > 80 && data[80] == 0xff) {
+                  assert(false);
+                }
+              }
+            } |]
+        let sig = Just $ Sig "fun(bytes)" [AbiBytesDynamicType]
+        (e, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        assertBoolM "must report partial due to bounded bytes" $ any isPartial e
+        let numCexes = sum $ map (fromEnum . isCex) ret
+        assertEqualM "should not find cex (bug is beyond bound)" 0 numCexes
+    , test "bytes-beyond-bound-sum-check" $ do
+        -- Bug triggers when sum of first 128 bytes overflows; requires > 64 bytes
+        Just c <- solcRuntime "C" [i|
+            contract C {
+              function fun(bytes calldata data) public pure {
+                if (data.length >= 128) {
+                  uint256 sum = 0;
+                  for (uint i = 0; i < 128; i++) {
+                    sum += uint8(data[i]);
+                  }
+                  assert(sum < 1000);
+                }
+              }
+            } |]
+        let sig = Just $ Sig "fun(bytes)" [AbiBytesDynamicType]
+        (e, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        assertBoolM "must report partial due to bounded bytes" $ any isPartial e
+        let numCexes = sum $ map (fromEnum . isCex) ret
+        assertEqualM "should not find cex (bug requires 128 bytes, bound is 64)" 0 numCexes
+    ]
+
   , testGroup "Precompiled contracts"
       [ testGroup "Example (reverse)"
           [ test "success" $