Fix suitableForSymExec precedence inversion

flake.nix

@@ -62,8 +62,8 @@
           (pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "argotorg";
             repo = "hevm";
-            rev = "8b2cb6266413f7f964e49053a278a895a21dc507";
-            sha256 = "sha256-wHkH26sfGLEL6XFYl+qZUPdWRZLnoftTqpufy5ASX7k=";
+            rev = "408bf3100f1edbfc489b21b5218332e583e503a7";
+            sha256 = "sha256-iJwO0tXuHe5dbPuzIdLHMVW8U4TwAqrC0VKmZcuz9S4=";
           }) { secp256k1 = pkgs.secp256k1; })
           ([
             pkgs.haskell.lib.compose.dontCheck

lib/Echidna/SymExec/Common.hs

@@ -17,7 +17,7 @@ import Data.Text qualified as T
 import Optics.Core ((.~), (%), (%~))
 
 import EVM (loadContract, resetState, symbolify)
-import EVM.ABI (abiKind, AbiKind(Dynamic), Sig(..), decodeBuf, AbiVals(..), selector, encodeAbiValue, AbiValue(..))
+import EVM.ABI (Sig(..), decodeBuf, AbiVals(..), selector, encodeAbiValue, AbiValue(..))
 import EVM.Effects (TTY, ReadConfig)
 import EVM.Expr qualified
 import EVM.Fetch qualified as Fetch
@@ -83,8 +83,12 @@ extractErrors = mapMaybe (\case
   _ -> Nothing)
 
 suitableForSymExec :: Method -> Bool
-suitableForSymExec m = not $ null m.inputs
-  && null (filter (\(_, t) -> abiKind t == Dynamic) m.inputs)
+suitableForSymExec m =
+  -- the method must take arguments (otherwise there is nothing to solve for)
+  -- and must not opt out via a `_no_symexec` name. Dynamic ABI types
+  -- (bytes/string/dynamic arrays) are now supported: hevm concretizes them to a
+  -- bounded length (see maxDynSize), so they no longer disqualify a method.
+  not (null m.inputs)
   && not (T.isInfixOf "_no_symexec" m.name)
 
 
@@ -168,8 +172,11 @@ exploreMethod :: (MonadUnliftIO m, ReadConfig m, TTY m) =>
   Method -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs)
 
 exploreMethod method _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do
-  calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
+  -- hevm's mkCalldata now returns ((calldata, constraints), caveats); the
+  -- caveats (e.g. bounded dynamic args) are not surfaced through echidna yet.
+  (calldataSym, _caveats) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
   let
+    constraints = snd calldataSym
     cd = fst calldataSym
     fetcher = Fetch.oracle solvers (Just session) rpcInfo
     dst = conf.solConf.contractAddr

lib/Echidna/SymExec/Exploration.hs

@@ -98,7 +98,7 @@ exploreContract contract method vm = do
   resultChan <- liftIO newEmptyMVar
   let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text
   let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = StackBased}
-  let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive, dumpQueries = False }
+  let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, maxBufSize = 12, maxDynSize = 128, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive, dumpQueries = False }
   let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo}
   let runtimeEnv = defaultEnv { config = hevmConfig }
   session <- asks (.fetchSession)

lib/Echidna/SymExec/Verification.hs

@@ -62,7 +62,7 @@ verifyMethod method contract vm = do
   resultChan <- liftIO newEmptyMVar
   let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text
   let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = StackBased}
-  let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, dumpExprs = True, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive }
+  let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, dumpExprs = True, maxBufSize = 12, maxDynSize = 128, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive }
   let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo}
   let runtimeEnv = defaultEnv { config = hevmConfig }
   session <- asks (.fetchSession)

src/test/Tests/Symbolic.hs

@@ -18,6 +18,10 @@ symbolicTests = testGroup "Symbolic tests" $
       ]
   ) ["symbolic/verify.yaml", "symbolic/verify.bitwuzla.yaml"]
   ++ ([
+    -- dynamic (bytes) calldata: hevm concretizes it up to maxDynSize (128 bytes),
+    -- so the symbolic worker can solve it. Run under bitwuzla only.
+    testContract' "symbolic/verify.sol" (Just "VulnerableContract") (Just (>= solcV (0,6,9))) (Just "symbolic/verify.bitwuzla.yaml") True SymbolicWorker
+      [ ("dynamic passed", solved "dynamic") ]
     -- This test is commented out because it requires a specific setup where both the FuzzWorker and SymbolicWorker are used.
     -- If you run the symbolic worker alone, it will hang indefinitely.
     --, testContract' "symbolic/explore.sol" Nothing Nothing (Just "symbolic/explore.yaml") True SymbolicWorker

stack.yaml

@@ -6,7 +6,7 @@ packages:
 
 extra-deps:
 - git: https://github.com/argotorg/hevm.git
-  commit: 8b2cb6266413f7f964e49053a278a895a21dc507
+  commit: 408bf3100f1edbfc489b21b5218332e583e503a7
 
 - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421
 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162

tests/solidity/symbolic/verify.sol

@@ -39,4 +39,12 @@ contract VulnerableContract {
     assert(y != 42);
   }
 
+  // dynamic (bytes) input: hevm concretizes it up to maxDynSize (128 bytes).
+  // Solvable, since the bug only needs the first two bytes to be 0xde 0xad.
+  function dynamic(bytes calldata data) public {
+    if (data.length >= 2) {
+      assert(data[0] != 0xde || data[1] != 0xad); // BUG
+    }
+  }
+
 }