From 2e67e73f99027408f1fff4a98a4bdcb6c34160eb Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 10:09:05 +0100 Subject: [PATCH 01/14] allow to properly use symbolic execution in property mode --- lib/Echidna/Campaign.hs | 85 +++++++- lib/Echidna/SymExec/Common.hs | 13 +- lib/Echidna/SymExec/Property.hs | 192 +++++++++++++++++++ lib/Echidna/Types/Test.hs | 12 ++ src/test/Tests/Symbolic.hs | 10 +- tests/solidity/symbolic/verify-property.sol | 46 +++++ tests/solidity/symbolic/verify-property.yaml | 7 + 7 files changed, 356 insertions(+), 9 deletions(-) create mode 100644 lib/Echidna/SymExec/Property.hs create mode 100644 tests/solidity/symbolic/verify-property.sol create mode 100644 tests/solidity/symbolic/verify-property.yaml diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs index 0543822f6..8ab11e043 100644 --- a/lib/Echidna/Campaign.hs +++ b/lib/Echidna/Campaign.hs @@ -43,6 +43,7 @@ import Echidna.Solidity (chooseContract) import Echidna.SymExec.Common (extractTxs, extractErrors) import Echidna.SymExec.Exploration (exploreContract, getTargetMethodFromTx, getRandomTargetMethod) import Echidna.SymExec.Symbolic (forceAddr) +import Echidna.SymExec.Property (verifyMethodForProperty, isSuitableForPropertyMode) import Echidna.SymExec.Verification (verifyMethod, isSuitableToVerifyMethod) import Echidna.Test import Echidna.Transaction @@ -52,6 +53,7 @@ import Echidna.Types.Corpus (Corpus, corpusSize) import Echidna.Types.Coverage (coverageStats) import Echidna.Types.Random (rElem) import Echidna.Types.Signature (FunctionName) +import Echidna.Types.Solidity (SolConf(..)) import Echidna.Types.Test import Echidna.Types.Test qualified as Test import Echidna.Types.Tx (TxCall(..), Tx(..)) @@ -273,12 +275,83 @@ runSymWorker callback vm dict workerId _ name = do contract <- chooseContract cs name let allMethods = contract.abiMap conf <- asks (.cfg) - forM_ allMethods (\method -> do - isSuitable <- isSuitableToVerifyMethod contract method conf.campaignConf.symExecTargets - if isSuitable - then symExecMethod contract method - else pushWorkerEvent $ SymExecError ("Skipped verification of method " <> unpack method.methodSignature) - ) + if isPropertyMode conf.solConf.testMode + then verifyMethodsProperty contract allMethods + else forM_ allMethods (\method -> do + isSuitable <- isSuitableToVerifyMethod contract method conf.campaignConf.symExecTargets + if isSuitable + then symExecMethod contract method + else pushWorkerEvent $ SymExecError ("Skipped verification of method " <> unpack method.methodSignature) + ) + + -- | Property mode verification: symbolically execute each state-changing + -- method to find concrete inputs, then check property functions against + -- the resulting VM states. + verifyMethodsProperty contract allMethods = do + conf <- asks (.cfg) + let prefix = conf.solConf.prefix + targets = conf.campaignConf.symExecTargets + methods = Map.elems allMethods + stateChangingMethods = filter (\m -> isSuitableForPropertyMode m prefix targets) methods + + when (null stateChangingMethods) $ + pushWorkerEvent $ SymExecError "No suitable state-changing methods found for property verification" + + forM_ stateChangingMethods $ \method -> + symExecMethodProperty contract method + + pushWorkerEvent $ SymExecLog ("Property mode symbolic verification finished for contract " <> unpack (fromJust name)) + + -- | Symbolically execute a method in property mode: find concrete inputs + -- for all reachable paths, then check each against all property tests. + symExecMethodProperty contract method = do + lift callback + (threadId, symTxsChan) <- verifyMethodForProperty method contract vm + + modify' (\ws -> ws { runningThreads = [threadId] }) + lift callback + + (symTxs, partials) <- liftIO $ takeMVar symTxsChan + let txs = extractTxs symTxs + let errors = extractErrors symTxs + + modify' (\ws -> ws { runningThreads = [] }) + lift callback + + let methodSignature = unpack method.methodSignature + + pushWorkerEvent $ SymExecLog ("Property mode: found " <> show (length txs) <> " concrete tx(es) for method " <> methodSignature <> ", " <> show (length errors) <> " error(s), " <> show (length partials) <> " partial(s)") + + -- For each concrete tx from symbolic execution, execute it and check properties + forM_ txs $ \symTx -> do + (_, vm') <- execTx vm symTx + pushWorkerEvent $ SymExecLog ("Property mode: executed tx " <> show symTx.call) + case vm'.result of + Just (VMSuccess _) -> do + -- Check all open property tests against the post-transaction state + updateTests $ \test -> do + if isOpen test && isPropertyTest test then do + (testValue, vm'') <- checkETest test vm' + pushWorkerEvent $ SymExecLog ("Property mode: checked property, value = " <> show testValue) + case testValue of + BoolValue False -> do + wid <- Just <$> gets (.workerId) + let test' = test { Test.state = Large 0 + , reproducer = [symTx] + , vm = Just vm' + , result = getResultFromVM vm'' + , Test.workerId = wid + } + pushWorkerEvent (TestFalsified test') + pure $ Just test' + _ -> pure Nothing + else pure Nothing + _ -> pure () + + unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during property verification of method " <> methodSignature <> ": " <> show e)) errors + unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during property verification of method " <> methodSignature <> ": " <> unpack e)) partials + + pushWorkerEvent $ SymExecLog ("Property mode symbolic execution finished for method " <> methodSignature) symExecMethod contract method = do lift callback diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs index cae5d8d17..331e4dc21 100644 --- a/lib/Echidna/SymExec/Common.hs +++ b/lib/Echidna/SymExec/Common.hs @@ -166,8 +166,14 @@ getUnknownLogs = mapMaybe (\case 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 = exploreMethodWith Nothing -exploreMethod method _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do +-- | Like 'exploreMethod' but accepts a custom postcondition. When 'Nothing', +-- uses the default assertion-checking postcondition. +exploreMethodWith :: (MonadUnliftIO m, ReadConfig m, TTY m) => + Maybe Postcondition -> Method -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs) + +exploreMethodWith customPost method _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) [] let cd = fst calldataSym @@ -190,7 +196,10 @@ exploreMethod method _contract _sources vm defaultSender conf veriOpts solvers r -- TODO we might want to switch vm's state.baseState value to to AbstractBase eventually. -- Doing so might mess up concolic execution. let foundry = isFoundryMode conf.solConf.testMode - (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (checkAssertions [0x1] foundry) Nothing + let postcondition = case customPost of + Just p -> p + Nothing -> checkAssertions [0x1] foundry + (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' postcondition Nothing let results = filter (\(r, _) -> not (isQed r)) models & map fst --liftIO $ mapM_ print partials return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (\(p, _) -> formatPartialDetailed Nothing Map.empty p) partials) diff --git a/lib/Echidna/SymExec/Property.hs b/lib/Echidna/SymExec/Property.hs new file mode 100644 index 000000000..a3c6ee3af --- /dev/null +++ b/lib/Echidna/SymExec/Property.hs @@ -0,0 +1,192 @@ +{-# LANGUAGE GADTs #-} + +module Echidna.SymExec.Property where + +import Control.Applicative ((<|>)) +import Control.Concurrent (ThreadId, forkIO) +import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar) +import Control.Monad.Catch (MonadThrow(..)) +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.IO.Unlift (MonadUnliftIO, liftIO) +import Control.Monad.Reader (MonadReader, asks, runReaderT) +import Control.Monad.State.Strict (MonadState, execState, runStateT) +import Data.Function ((&)) +import Data.Map qualified as Map +import Data.Maybe (fromJust) +import Data.Set qualified as Set +import Data.Text qualified as Text + +import EVM (initialContract, loadContract, resetState, symbolify) +import EVM.ABI (Sig(..), selector) +import EVM.Dapp (DappInfo(..)) +import EVM.Effects (TTY, ReadConfig, defaultEnv, defaultConfig, Config(..), Env(..)) +import EVM.Fetch qualified as Fetch +import EVM.Fetch (RpcInfo(..)) +import EVM.Format (formatPartialDetailed) +import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..)) +import EVM.Solvers (SolverGroup, defMemLimit, withSolvers) +import EVM.SymExec (mkCalldata, verifyInputsWithHandler, IterConfig(..), LoopHeuristic(..), VeriOpts(..), Postcondition) +import EVM.Types (Addr, Contract(..), VMType(..), EType(..), Expr(..), Block(..), Prop(..), isQed) +import qualified EVM.Types (VM(..)) + +import Echidna.SymExec.Common + ( rpcFetcher, modelToTx, suitableForSymExec + , blockMakeSymbolic, addBlockConstraints, senderConstraints + , TxOrError(..), PartialsLogs + ) +import Echidna.Test (isFoundryMode) +import Echidna.Types (fromEVM) +import Echidna.Types.Campaign (CampaignConf(..), WorkerState) +import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..)) +import Echidna.Types.Solidity (SolConf(..)) +import Echidna.Types.Tx (TxConf(..)) +import Echidna.Types.Worker (WorkerEvent(..)) +import Echidna.Worker (pushWorkerEvent) +import Optics.Core ((.~), (%), (%~)) + +-- | Convert a symbolic contract expression (from a Success leaf) to a +-- concrete Contract value suitable for use in a VM's env.contracts map. +fromEContract :: Expr EContract -> Contract +fromEContract (C code storage tStorage balance nonce) = + initialContract code + & #storage .~ storage + & #tStorage .~ tStorage + & #balance .~ balance + & #nonce .~ nonce +fromEContract _ = error "fromEContract: unexpected non-C expression" + +-- | Postcondition for property mode phase 2: check if property function +-- returned false (i.e., return value is 0). A return value of 0 means the +-- property was violated. +checkPropertyReturn :: Postcondition +checkPropertyReturn _ = \case + Success _ _ returnBuf _ -> + -- Property should return true (non-zero). If it returns 0 (false), + -- we have a violation. The postcondition says "this should hold", + -- so we express "return != 0". + PNeg (PEq (ReadWord (Lit 0) returnBuf) (Lit 0)) + _ -> PBool True -- reverts/failures are not property violations + +-- | Check if a method is suitable for property mode verification. +-- In property mode, we want to symbolically execute state-changing functions +-- (not the property functions themselves). Property functions are identified +-- by the configured prefix (e.g., "echidna_"). +isSuitableForPropertyMode :: Method -> Text.Text -> [Text.Text] -> Bool +isSuitableForPropertyMode method prefix symExecTargets = + if null symExecTargets + then not (Text.isPrefixOf prefix method.name) && suitableForSymExec method + else method.name `elem` symExecTargets + +-- | Two-phase symbolic execution for property mode. +-- +-- Phase 1: Symbolically execute a state-changing method with a trivially-true +-- postcondition (no solver calls). This collects all reachable Success leaves, +-- each containing symbolic contract states and path constraints. +-- +-- Phase 2: For each Success leaf and each property method, reconstruct a VM +-- with the symbolic contract states, execute the property function, and check +-- if it can return false. The solver finds concrete values for phase 1's +-- symbolic variables (calldata, caller, etc.) that cause the property to fail. +exploreMethodForProperty :: (MonadUnliftIO m, ReadConfig m, TTY m) => + Method -> [Method] -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs) + +exploreMethodForProperty method propertyMethods _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do + -- Phase 1: Execute state-changing method symbolically + calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) [] + let + cd = fst calldataSym + fetcher = Fetch.oracle solvers (Just session) rpcInfo + dst = conf.solConf.contractAddr + vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm + let + vm' = vmReset & execState (loadContract (LitAddr dst)) + & #tx % #isCreate .~ False + & #state % #callvalue .~ (if isFoundryMode conf.solConf.testMode then Lit 0 else TxValue) + & #state % #caller .~ SymAddr "caller" + & #state % #calldata .~ cd + + vm'' = symbolify vm' + & #block %~ blockMakeSymbolic + & #constraints %~ (addBlockConstraints conf.txConf.maxTimeDelay conf.txConf.maxBlockDelay vm'.block) + & #constraints %~ (++ constraints ++ senderConstraints conf.solConf.sender) + + -- Phase 1: PBool True postcondition → no solver calls, all Success paths return Qed + (phase1Models, phase1Partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (\_ _ -> PBool True) Nothing + + -- Extract Success leaves with their path constraints and symbolic contract states + let successLeaves = [(props, contracts) | (_, Success props _ _ contracts) <- phase1Models] + + -- Phase 2: For each Success leaf, check each property function + allResults <- concat <$> mapM (checkLeaf fetcher dst vm cd method conf defaultSender solvers veriOpts propertyMethods) successLeaves + + let allPartialLogs = map (\(p, _) -> formatPartialDetailed Nothing Map.empty p) phase1Partials + return (allResults, allPartialLogs) + + where + + -- | Phase 2 for a single Success leaf: check all property methods + checkLeaf fetcher dst vm0 cd method0 conf0 defaultSender0 solvers0 veriOpts0 propMethods (leafConstraints, leafContracts) = do + let convertedContracts = Map.map fromEContract leafContracts + concat <$> mapM (checkProperty fetcher dst vm0 cd method0 conf0 defaultSender0 solvers0 veriOpts0 convertedContracts leafConstraints) propMethods + + -- | Phase 2 for a single (leaf, property) pair + checkProperty fetcher dst vm0 cd method0 conf0 defaultSender0 solvers0 veriOpts0 convertedContracts leafConstraints propMethod = do + vmReset2 <- liftIO $ snd <$> runStateT (fromEVM resetState) vm0 + let + propCd = ConcreteBuf (selector propMethod.methodSignature) + -- Replace contracts with phase 1's symbolic state, keeping originals as fallback + vm2 = vmReset2 & #env % #contracts %~ Map.union convertedContracts + & execState (loadContract (LitAddr dst)) + & #tx % #isCreate .~ False + & #state % #callvalue .~ Lit 0 + & #state % #caller .~ SymAddr "caller" + & #state % #calldata .~ propCd + -- Carry over phase 1's path constraints so the solver must satisfy both phases + vm2' = symbolify vm2 + & #constraints .~ leafConstraints + + (phase2Models, _) <- verifyInputsWithHandler solvers0 veriOpts0 fetcher vm2' checkPropertyReturn Nothing + let results2 = filter (\(r, _) -> not (isQed r)) phase2Models & map fst + return $ map (modelToTx dst vm0.block.timestamp vm0.block.number method0 conf0.solConf.sender defaultSender0 cd) results2 + +-- | Two-phase symbolic verification for property mode. +-- Phase 1: Symbolically execute the state-changing method to collect all +-- reachable symbolic states (no solver calls). +-- Phase 2: For each symbolic state, execute each property function and use +-- the solver to find inputs that make the property return false. +verifyMethodForProperty :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) => Method -> SolcContract -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) +verifyMethodForProperty method contract vm = do + conf <- asks (.cfg) + dappInfo <- asks (.dapp) + let + timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout) + maxIters = Just conf.campaignConf.symExecMaxIters + maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore) + askSmtIters = conf.campaignConf.symExecAskSMTIters + rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock)) + defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0 + -- Find property methods: functions with the configured prefix (e.g., "echidna_") + prefix = conf.solConf.prefix + propertyMethods = filter (\m -> Text.isPrefixOf prefix m.name) $ Map.elems contract.abiMap + + threadIdChan <- liftIO newEmptyMVar + doneChan <- liftIO newEmptyMVar + 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 veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo} + let runtimeEnv = defaultEnv { config = hevmConfig } + session <- asks (.fetchSession) + pushWorkerEvent $ SymExecLog ("Verifying (property mode) " <> (show method.name)) + + liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do + threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do + (res, partials) <- exploreMethodForProperty method propertyMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + liftIO $ putMVar resultChan (res, partials) + liftIO $ putMVar doneChan () + liftIO $ putMVar threadIdChan threadId + liftIO $ takeMVar doneChan + + threadId <- liftIO $ takeMVar threadIdChan + pure (threadId, resultChan) diff --git a/lib/Echidna/Types/Test.hs b/lib/Echidna/Types/Test.hs index 1e998a8c9..4b189210a 100644 --- a/lib/Echidna/Types/Test.hs +++ b/lib/Echidna/Types/Test.hs @@ -117,6 +117,18 @@ instance ToJSON EchidnaTest where , "result" .= result ] +isPropertyTest :: EchidnaTest -> Bool +isPropertyTest EchidnaTest{testType = PropertyTest _ _} = True +isPropertyTest _ = False + +getPropertyName :: EchidnaTest -> Text +getPropertyName EchidnaTest{testType = PropertyTest n _} = n +getPropertyName _ = error "Not a property test" + +getPropertyAddr :: EchidnaTest -> Addr +getPropertyAddr EchidnaTest{testType = PropertyTest _ a} = a +getPropertyAddr _ = error "Not a property test" + isOptimizationTest :: EchidnaTest -> Bool isOptimizationTest EchidnaTest{testType = OptimizationTest _ _} = True isOptimizationTest _ = False diff --git a/src/test/Tests/Symbolic.hs b/src/test/Tests/Symbolic.hs index e3392078b..95f0ef9f8 100644 --- a/src/test/Tests/Symbolic.hs +++ b/src/test/Tests/Symbolic.hs @@ -2,7 +2,7 @@ module Tests.Symbolic (symbolicTests) where import Test.Tasty (TestTree, testGroup) -import Common (testContract', solcV, solved, verified) +import Common (testContract', solcV, solved, passed, verified) import Echidna.Types.Worker (WorkerType(..)) symbolicTests :: TestTree @@ -17,6 +17,14 @@ symbolicTests = testGroup "Symbolic tests" $ , ("correct not verified", verified "correct") ] ) ["symbolic/verify.yaml", "symbolic/verify.bitwuzla.yaml"] + ++ [ + testContract' "symbolic/verify-property.sol" (Just "PropertyVerifyTest") (Just (>= solcV (0,6,9))) (Just "symbolic/verify-property.yaml") True SymbolicWorker + [ ("echidna_x_is_not_ten falsified", solved "echidna_x_is_not_ten") + , ("echidna_x_is_not_one passed", passed "echidna_x_is_not_one") + , ("echidna_y_below_40 falsified", solved "echidna_y_below_40") + , ("echidna_locked_before_1000 falsified", solved "echidna_locked_before_1000") + ] + ] ++ ([ -- 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. diff --git a/tests/solidity/symbolic/verify-property.sol b/tests/solidity/symbolic/verify-property.sol new file mode 100644 index 000000000..41970b7fe --- /dev/null +++ b/tests/solidity/symbolic/verify-property.sol @@ -0,0 +1,46 @@ +contract PropertyVerifyTest { + uint256 public x; + uint256 public y; + uint256 public lockedUntil; + + function set_x(uint256 _x) public { + // Only values 5 <= _x <= 20 are accepted. + require(_x >= 5, "too low"); + require(_x <= 20, "too high"); + x = _x; + } + + function set_y(uint256 _y) public { + // Only even values accepted + require(_y % 2 == 0, "must be even"); + require(_y > 0, "must be positive"); + y = _y; + } + + function lock(uint256 duration) public { + require(duration > 0 && duration <= 365 days, "bad duration"); + lockedUntil = block.timestamp + duration; + } + + // Should be FALSIFIED: set_x(10) passes the requires and sets x == 10 + function echidna_x_is_not_ten() public returns (bool) { + return x != 10; + } + + // Should HOLD: set_x requires _x >= 5, so x can never be 1 + function echidna_x_is_not_one() public returns (bool) { + return x != 1; + } + + // Should be FALSIFIED: set_y(42) passes both requires + function echidna_y_below_40() public returns (bool) { + return y < 40; + } + + // Should be FALSIFIED: lock() sets lockedUntil = block.timestamp + duration, + // and block.timestamp is symbolic, so the solver can pick a timestamp where + // lockedUntil > 1000. + function echidna_locked_before_1000() public returns (bool) { + return lockedUntil <= 1000; + } +} diff --git a/tests/solidity/symbolic/verify-property.yaml b/tests/solidity/symbolic/verify-property.yaml new file mode 100644 index 000000000..2ef986085 --- /dev/null +++ b/tests/solidity/symbolic/verify-property.yaml @@ -0,0 +1,7 @@ +testMode: property +symExec: true +symExecSMTSolver: z3 +workers: 0 +seqLen: 1 + +disableSlither: true From f34c10fc0247f6e41580a4df6c33f930ee452bd5 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 13:48:17 +0100 Subject: [PATCH 02/14] extend to assertions --- lib/Echidna/Campaign.hs | 155 +++++++++++++-- lib/Echidna/SymExec/Common.hs | 87 ++++++++- lib/Echidna/SymExec/Exploration.hs | 41 +++- lib/Echidna/SymExec/Property.hs | 177 ++++++------------ src/test/Common.hs | 51 ++++- src/test/Tests/Symbolic.hs | 12 +- tests/solidity/symbolic/motiv-explore.yaml | 6 + tests/solidity/symbolic/motiv.sol | 30 +++ tests/solidity/symbolic/motiv.yaml | 6 + .../symbolic/verify-assertion-noarg.sol | 35 ++++ .../symbolic/verify-assertion-noarg.yaml | 6 + 11 files changed, 465 insertions(+), 141 deletions(-) create mode 100644 tests/solidity/symbolic/motiv-explore.yaml create mode 100644 tests/solidity/symbolic/motiv.sol create mode 100644 tests/solidity/symbolic/motiv.yaml create mode 100644 tests/solidity/symbolic/verify-assertion-noarg.sol create mode 100644 tests/solidity/symbolic/verify-assertion-noarg.yaml diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs index 8ab11e043..fd07eabd6 100644 --- a/lib/Echidna/Campaign.hs +++ b/lib/Echidna/Campaign.hs @@ -23,7 +23,7 @@ import Data.Map qualified as Map import Data.Maybe (isJust, mapMaybe, fromJust) import Data.Set (Set) import Data.Set qualified as Set -import Data.Text (Text, unpack) +import Data.Text (Text, pack, unpack) import Data.Time (LocalTime) import Data.Vector qualified as V import System.Random (mkStdGen) @@ -40,10 +40,10 @@ import Echidna.Exec import Echidna.Mutator.Corpus import Echidna.Shrink (shrinkTest) import Echidna.Solidity (chooseContract) -import Echidna.SymExec.Common (extractTxs, extractErrors) -import Echidna.SymExec.Exploration (exploreContract, getTargetMethodFromTx, getRandomTargetMethod) +import Echidna.SymExec.Common (extractTxs, extractErrors, suitableForSymExec) +import Echidna.SymExec.Exploration (exploreContract, exploreContractTwoPhase, getTargetMethodFromTx, getRandomTargetMethod) import Echidna.SymExec.Symbolic (forceAddr) -import Echidna.SymExec.Property (verifyMethodForProperty, isSuitableForPropertyMode) +import Echidna.SymExec.Property (verifyMethodForProperty, verifyMethodForAssertion, isSuitableForPropertyMode, isNoArgAssertionTarget) import Echidna.SymExec.Verification (verifyMethod, isSuitableToVerifyMethod) import Echidna.Test import Echidna.Transaction @@ -56,7 +56,7 @@ import Echidna.Types.Signature (FunctionName) import Echidna.Types.Solidity (SolConf(..)) import Echidna.Types.Test import Echidna.Types.Test qualified as Test -import Echidna.Types.Tx (TxCall(..), Tx(..)) +import Echidna.Types.Tx (TxCall(..), Tx(..), basicTx, maxGasPerBlock) import Echidna.Types.Worker import Echidna.Worker @@ -235,18 +235,24 @@ runSymWorker callback vm dict workerId _ name = do contract <- chooseContract cs name failedTests <- findFailedTests let failedTestSignatures = map getAssertionSignature failedTests + -- Single-phase exploration: only methods matching assertSigs filter case tx of Nothing -> getRandomTargetMethod contract conf.campaignConf.symExecTargets failedTestSignatures >>= \case - Nothing -> do - return () + Nothing -> pure () Just method -> exploreAndVerify contract method vm' txsBase Just t -> getTargetMethodFromTx t contract failedTestSignatures >>= \case - Nothing -> do - return () - Just method -> do - exploreAndVerify contract method vm' txsBase + Nothing -> pure () + Just method -> exploreAndVerify contract method vm' txsBase + -- Two-phase exploration: any state-changing method → no-arg assertion targets + let noArgTargets = filter isNoArgAssertionTarget $ Map.elems contract.abiMap + stateChanging = filter suitableForSymExec $ Map.elems contract.abiMap + unless (null noArgTargets || null stateChanging) $ do + -- Pick a random state-changing method for two-phase + method <- liftIO $ rElem (NEList.fromList stateChanging) + exploreAndVerifyTwoPhase contract method noArgTargets vm' txsBase exploreAndVerify contract method vm' txsBase = do + -- Single-phase exploration (existing) (threadId, symTxsChan) <- exploreContract contract method vm' modify' (\ws -> ws { runningThreads = [threadId] }) lift callback @@ -269,6 +275,49 @@ runSymWorker callback vm dict workerId _ name = do pushWorkerEvent $ SymExecError "No errors but symbolic execution found valid txs breaking assertions. Something is wrong.") unless newCoverage (pushWorkerEvent $ SymExecLog "Symbolic execution finished with no new coverage.") + exploreAndVerifyTwoPhase contract method targets vm' txsBase = do + conf <- asks (.cfg) + let dst = conf.solConf.contractAddr + (threadId2, symTxsChan2) <- exploreContractTwoPhase contract method targets vm' + modify' (\ws -> ws { runningThreads = [threadId2] }) + lift callback + + (symTxs2, partials2) <- liftIO $ takeMVar symTxsChan2 + let txs2 = extractTxs symTxs2 + let errors2 = extractErrors symTxs2 + + modify' (\ws -> ws { runningThreads = [] }) + lift callback + + -- For each concrete tx, execute it then check assertion functions + forM_ txs2 $ \symTx -> do + (_, vmAfter) <- execTx vm' symTx + case vmAfter.result of + Just (VMSuccess _) -> + updateTests $ \test -> do + if isOpen test && isAssertionTest test then do + let fnName = pack (getAssertionFunctionName test) + assertTx = basicTx fnName [] symTx.src dst maxGasPerBlock (0, 0) + (_, vmCheck) <- execTx vmAfter assertTx + (testValue, vmCheck') <- checkETest test vmCheck + case testValue of + BoolValue False -> do + wid <- Just <$> gets (.workerId) + let test' = test { Test.state = Large 0 + , reproducer = txsBase <> [symTx, assertTx] + , vm = Just vmAfter + , result = getResultFromVM vmCheck' + , Test.workerId = wid + } + pushWorkerEvent (TestFalsified test') + pure $ Just test' + _ -> pure Nothing + else pure Nothing + _ -> pure () + + unless (null errors2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during two-phase exploration: " <> show e)) errors2 + unless (null partials2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during two-phase exploration: " <> unpack e)) partials2 + verifyMethods = do dapp <- asks (.dapp) let cs = Map.elems dapp.solcByName @@ -277,12 +326,84 @@ runSymWorker callback vm dict workerId _ name = do conf <- asks (.cfg) if isPropertyMode conf.solConf.testMode then verifyMethodsProperty contract allMethods - else forM_ allMethods (\method -> do - isSuitable <- isSuitableToVerifyMethod contract method conf.campaignConf.symExecTargets - if isSuitable - then symExecMethod contract method - else pushWorkerEvent $ SymExecError ("Skipped verification of method " <> unpack method.methodSignature) - ) + else verifyMethodsAssertion contract allMethods + + -- | Assertion mode verification: single-phase for methods with args, + -- two-phase for no-arg assertion functions that can only fail via state. + verifyMethodsAssertion contract allMethods = do + conf <- asks (.cfg) + let methods = Map.elems allMethods + -- No-arg assertion functions: need two-phase + noArgAssertions = filter isNoArgAssertionTarget methods + -- State-changing methods with args: used as phase 1 targets + stateChangingMethods = filter suitableForSymExec methods + + -- Single-phase for methods with args + forM_ allMethods $ \method -> do + isSuitable <- isSuitableToVerifyMethod contract method conf.campaignConf.symExecTargets + if isSuitable + then symExecMethod contract method + else pushWorkerEvent $ SymExecError ("Skipped verification of method " <> unpack method.methodSignature) + + -- Two-phase for no-arg assertion functions + unless (null noArgAssertions || null stateChangingMethods) $ do + pushWorkerEvent $ SymExecLog ("Two-phase assertion: " <> show (length noArgAssertions) <> " no-arg target(s), " <> show (length stateChangingMethods) <> " state-changing method(s)") + forM_ stateChangingMethods $ \method -> + symExecMethodAssertion contract method noArgAssertions + + -- | Two-phase assertion mode: execute a state-changing method symbolically, + -- then check no-arg assertion functions against the resulting states. + symExecMethodAssertion contract method assertionTargets = do + lift callback + (threadId, symTxsChan) <- verifyMethodForAssertion assertionTargets method contract vm + + modify' (\ws -> ws { runningThreads = [threadId] }) + lift callback + + (symTxs, partials) <- liftIO $ takeMVar symTxsChan + let txs = extractTxs symTxs + let errors = extractErrors symTxs + + modify' (\ws -> ws { runningThreads = [] }) + lift callback + + let methodSignature = unpack method.methodSignature + + pushWorkerEvent $ SymExecLog ("Assertion two-phase: found " <> show (length txs) <> " concrete tx(es) for method " <> methodSignature) + + conf <- asks (.cfg) + let dst = conf.solConf.contractAddr + + -- For each concrete tx, execute it then explicitly call each assertion function + forM_ txs $ \symTx -> do + (_, vm') <- execTx vm symTx + case vm'.result of + Just (VMSuccess _) -> do + -- Re-execute each assertion function on the post-tx state, + -- then use checkETest which already handles all assertion patterns + updateTests $ \test -> do + if isOpen test && isAssertionTest test then do + let fnName = pack (getAssertionFunctionName test) + assertTx = basicTx fnName [] symTx.src dst maxGasPerBlock (0, 0) + (_, vm'') <- execTx vm' assertTx + (testValue, vm''') <- checkETest test vm'' + case testValue of + BoolValue False -> do + wid <- Just <$> gets (.workerId) + let test' = test { Test.state = Large 0 + , reproducer = [symTx, assertTx] + , vm = Just vm' + , result = getResultFromVM vm''' + , Test.workerId = wid + } + pushWorkerEvent (TestFalsified test') + pure $ Just test' + _ -> pure Nothing + else pure Nothing + _ -> pure () + + unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during assertion two-phase for method " <> methodSignature <> ": " <> show e)) errors + unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during assertion two-phase for method " <> methodSignature <> ": " <> unpack e)) partials -- | Property mode verification: symbolically execute each state-changing -- method to find concrete inputs, then check property functions against diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs index 331e4dc21..4bce00aa6 100644 --- a/lib/Echidna/SymExec/Common.hs +++ b/lib/Echidna/SymExec/Common.hs @@ -16,7 +16,7 @@ import Data.Set qualified as Set import Data.Text qualified as T import Optics.Core ((.~), (%), (%~)) -import EVM (loadContract, resetState, symbolify) +import EVM (initialContract, loadContract, resetState, symbolify) import EVM.ABI (abiKind, AbiKind(Dynamic), Sig(..), decodeBuf, AbiVals(..), selector, encodeAbiValue, AbiValue(..)) import EVM.Effects (TTY, ReadConfig) import EVM.Expr qualified @@ -25,7 +25,7 @@ import EVM.Format (formatPartialDetailed) import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..)) import EVM.Solvers (SolverGroup) import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), subModel, defaultSymbolicValues, Postcondition) -import EVM.Types (Addr, VMType(..), EType(..), EvmError(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed) +import EVM.Types (Addr, Contract(..), VMType(..), EType(..), EvmError(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed) import qualified EVM.Types (VM(..)) import Echidna.Test (isFoundryMode) @@ -203,3 +203,86 @@ exploreMethodWith customPost method _contract _sources vm defaultSender conf ver let results = filter (\(r, _) -> not (isQed r)) models & map fst --liftIO $ mapM_ print partials return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (\(p, _) -> formatPartialDetailed Nothing Map.empty p) partials) + +-- | Convert a symbolic contract expression (from a Success leaf) to a +-- concrete Contract value suitable for use in a VM's env.contracts map. +fromEContract :: Expr EContract -> Contract +fromEContract (C code storage tStorage balance nonce) = + initialContract code + & #storage .~ storage + & #tStorage .~ tStorage + & #balance .~ balance + & #nonce .~ nonce +fromEContract _ = error "fromEContract: unexpected non-C expression" + +-- | Two-phase symbolic execution. +-- +-- Phase 1: Symbolically execute a state-changing method with a trivially-true +-- postcondition (no solver calls). This collects all reachable Success leaves, +-- each containing symbolic contract states and path constraints. +-- +-- Phase 2: For each Success leaf and each target method, reconstruct a VM +-- with the symbolic contract states, execute the target, and check the given +-- postcondition. The solver finds concrete values for phase 1's symbolic +-- variables (calldata, caller, etc.) that cause a violation. +exploreMethodTwoPhase :: (MonadUnliftIO m, ReadConfig m, TTY m) => + Postcondition -> Method -> [Method] -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs) + +exploreMethodTwoPhase phase2Post method targetMethods _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do + -- Phase 1: Execute state-changing method symbolically + calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) [] + let + cd = fst calldataSym + fetcher = Fetch.oracle solvers (Just session) rpcInfo + dst = conf.solConf.contractAddr + vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm + let + vm' = vmReset & execState (loadContract (LitAddr dst)) + & #tx % #isCreate .~ False + & #state % #callvalue .~ (if isFoundryMode conf.solConf.testMode then Lit 0 else TxValue) + & #state % #caller .~ SymAddr "caller" + & #state % #calldata .~ cd + + vm'' = symbolify vm' + & #block %~ blockMakeSymbolic + & #constraints %~ (addBlockConstraints conf.txConf.maxTimeDelay conf.txConf.maxBlockDelay vm'.block) + & #constraints %~ (++ constraints ++ senderConstraints conf.solConf.sender) + + -- Phase 1: PBool True postcondition → no solver calls, all Success paths return Qed + (phase1Models, phase1Partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (\_ _ -> PBool True) Nothing + + -- Extract Success leaves with their path constraints and symbolic contract states + let successLeaves = [(props, contracts) | (_, Success props _ _ contracts) <- phase1Models] + + -- Phase 2: For each Success leaf, check each target method + allResults <- concat <$> mapM (checkLeaf fetcher dst vm cd) successLeaves + + let allPartialLogs = map (\(p, _) -> formatPartialDetailed Nothing Map.empty p) phase1Partials + return (allResults, allPartialLogs) + + where + + -- | Phase 2 for a single Success leaf: check all target methods + checkLeaf fetcher dst vm0 cd (leafConstraints, leafContracts) = do + let convertedContracts = Map.map fromEContract leafContracts + concat <$> mapM (checkTarget fetcher dst vm0 cd convertedContracts leafConstraints) targetMethods + + -- | Phase 2 for a single (leaf, target) pair + checkTarget fetcher dst vm0 cd convertedContracts leafConstraints targetMethod = do + vmReset2 <- liftIO $ snd <$> runStateT (fromEVM resetState) vm0 + let + targetCd = ConcreteBuf (selector targetMethod.methodSignature) + -- Replace contracts with phase 1's symbolic state, keeping originals as fallback + vm2 = vmReset2 & #env % #contracts %~ Map.union convertedContracts + & execState (loadContract (LitAddr dst)) + & #tx % #isCreate .~ False + & #state % #callvalue .~ Lit 0 + & #state % #caller .~ SymAddr "caller" + & #state % #calldata .~ targetCd + -- Carry over phase 1's path constraints so the solver must satisfy both phases + vm2' = symbolify vm2 + & #constraints .~ leafConstraints + + (phase2Models, _) <- verifyInputsWithHandler solvers veriOpts fetcher vm2' phase2Post Nothing + let results2 = filter (\(r, _) -> not (isQed r)) phase2Models & map fst + return $ map (modelToTx dst vm0.block.timestamp vm0.block.number method conf.solConf.sender defaultSender cd) results2 diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index fd4b2907b..6817d8993 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -24,7 +24,8 @@ import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..)) import EVM.Types (VMType(..)) import qualified EVM.Types (VM(..)) -import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, rpcFetcher, TxOrError(..), PartialsLogs) +import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, exploreMethodTwoPhase, checkAssertions, rpcFetcher, TxOrError(..), PartialsLogs) +import Echidna.Test (isFoundryMode) import Echidna.Types.Campaign (CampaignConf(..), WorkerState) import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..)) import Echidna.Types.Random (rElem) @@ -116,3 +117,41 @@ exploreContract contract method vm = do threadId <- liftIO $ takeMVar threadIdChan pure (threadId, resultChan) + +-- | Like 'exploreContract' but uses two-phase symbolic execution. +-- Phase 1 explores the given method, phase 2 checks the given target methods +-- (typically no-arg assertion functions) for violations. +exploreContractTwoPhase :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) + => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) +exploreContractTwoPhase contract method targetMethods vm = do + conf <- asks (.cfg) + dappInfo <- asks (.dapp) + let + isFoundry = isFoundryMode conf.solConf.testMode + timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout) + maxIters = Just conf.campaignConf.symExecMaxIters + maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore) + askSmtIters = conf.campaignConf.symExecAskSMTIters + rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock)) + defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0 + + threadIdChan <- liftIO newEmptyMVar + doneChan <- liftIO newEmptyMVar + 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 veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo } + let runtimeEnv = defaultEnv { config = hevmConfig } + session <- asks (.fetchSession) + pushWorkerEvent $ SymExecLog ("Two-phase exploring " <> show method.name <> " against " <> show (length targetMethods) <> " assertion target(s)") + liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do + threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do + res <- exploreMethodTwoPhase (checkAssertions [0x1] isFoundry) method targetMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + liftIO $ putMVar resultChan res + liftIO $ putMVar doneChan () + liftIO $ putMVar threadIdChan threadId + liftIO $ takeMVar doneChan + + threadId <- liftIO $ takeMVar threadIdChan + pure (threadId, resultChan) diff --git a/lib/Echidna/SymExec/Property.hs b/lib/Echidna/SymExec/Property.hs index a3c6ee3af..786ae6855 100644 --- a/lib/Echidna/SymExec/Property.hs +++ b/lib/Echidna/SymExec/Property.hs @@ -7,182 +7,121 @@ import Control.Concurrent (ThreadId, forkIO) import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar) import Control.Monad.Catch (MonadThrow(..)) import Control.Monad.IO.Class (MonadIO) -import Control.Monad.IO.Unlift (MonadUnliftIO, liftIO) -import Control.Monad.Reader (MonadReader, asks, runReaderT) -import Control.Monad.State.Strict (MonadState, execState, runStateT) -import Data.Function ((&)) +import Control.Monad.Reader (MonadReader, asks, runReaderT, liftIO) +import Control.Monad.State.Strict (MonadState) import Data.Map qualified as Map import Data.Maybe (fromJust) import Data.Set qualified as Set import Data.Text qualified as Text -import EVM (initialContract, loadContract, resetState, symbolify) -import EVM.ABI (Sig(..), selector) import EVM.Dapp (DappInfo(..)) -import EVM.Effects (TTY, ReadConfig, defaultEnv, defaultConfig, Config(..), Env(..)) -import EVM.Fetch qualified as Fetch +import EVM.Effects (defaultEnv, defaultConfig, Config(..), Env(..)) import EVM.Fetch (RpcInfo(..)) -import EVM.Format (formatPartialDetailed) -import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..)) -import EVM.Solvers (SolverGroup, defMemLimit, withSolvers) -import EVM.SymExec (mkCalldata, verifyInputsWithHandler, IterConfig(..), LoopHeuristic(..), VeriOpts(..), Postcondition) -import EVM.Types (Addr, Contract(..), VMType(..), EType(..), Expr(..), Block(..), Prop(..), isQed) +import EVM.Solidity (SolcContract(..), Method(..)) +import EVM.Solvers (defMemLimit, withSolvers) +import EVM.SymExec (IterConfig(..), LoopHeuristic(..), VeriOpts(..), Postcondition) +import EVM.Types (Expr(..), Prop(..), VMType(..)) import qualified EVM.Types (VM(..)) import Echidna.SymExec.Common - ( rpcFetcher, modelToTx, suitableForSymExec - , blockMakeSymbolic, addBlockConstraints, senderConstraints + ( rpcFetcher, checkAssertions, suitableForSymExec + , exploreMethodTwoPhase , TxOrError(..), PartialsLogs ) import Echidna.Test (isFoundryMode) -import Echidna.Types (fromEVM) import Echidna.Types.Campaign (CampaignConf(..), WorkerState) import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..)) import Echidna.Types.Solidity (SolConf(..)) -import Echidna.Types.Tx (TxConf(..)) import Echidna.Types.Worker (WorkerEvent(..)) import Echidna.Worker (pushWorkerEvent) -import Optics.Core ((.~), (%), (%~)) - --- | Convert a symbolic contract expression (from a Success leaf) to a --- concrete Contract value suitable for use in a VM's env.contracts map. -fromEContract :: Expr EContract -> Contract -fromEContract (C code storage tStorage balance nonce) = - initialContract code - & #storage .~ storage - & #tStorage .~ tStorage - & #balance .~ balance - & #nonce .~ nonce -fromEContract _ = error "fromEContract: unexpected non-C expression" -- | Postcondition for property mode phase 2: check if property function --- returned false (i.e., return value is 0). A return value of 0 means the --- property was violated. +-- returned false (i.e., return value is 0). checkPropertyReturn :: Postcondition checkPropertyReturn _ = \case Success _ _ returnBuf _ -> - -- Property should return true (non-zero). If it returns 0 (false), - -- we have a violation. The postcondition says "this should hold", - -- so we express "return != 0". PNeg (PEq (ReadWord (Lit 0) returnBuf) (Lit 0)) - _ -> PBool True -- reverts/failures are not property violations + _ -> PBool True --- | Check if a method is suitable for property mode verification. --- In property mode, we want to symbolically execute state-changing functions --- (not the property functions themselves). Property functions are identified --- by the configured prefix (e.g., "echidna_"). +-- | Check if a method is suitable as a phase 1 target in property mode. isSuitableForPropertyMode :: Method -> Text.Text -> [Text.Text] -> Bool isSuitableForPropertyMode method prefix symExecTargets = if null symExecTargets then not (Text.isPrefixOf prefix method.name) && suitableForSymExec method else method.name `elem` symExecTargets --- | Two-phase symbolic execution for property mode. --- --- Phase 1: Symbolically execute a state-changing method with a trivially-true --- postcondition (no solver calls). This collects all reachable Success leaves, --- each containing symbolic contract states and path constraints. --- --- Phase 2: For each Success leaf and each property method, reconstruct a VM --- with the symbolic contract states, execute the property function, and check --- if it can return false. The solver finds concrete values for phase 1's --- symbolic variables (calldata, caller, etc.) that cause the property to fail. -exploreMethodForProperty :: (MonadUnliftIO m, ReadConfig m, TTY m) => - Method -> [Method] -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs) +-- | Check if a method is a no-argument assertion function suitable for +-- two-phase verification. +isNoArgAssertionTarget :: Method -> Bool +isNoArgAssertionTarget m = null m.inputs + && not (Text.isInfixOf "_no_symexec" m.name) -exploreMethodForProperty method propertyMethods _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do - -- Phase 1: Execute state-changing method symbolically - calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) [] - let - cd = fst calldataSym - fetcher = Fetch.oracle solvers (Just session) rpcInfo - dst = conf.solConf.contractAddr - vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm +-- | Spawn a thread for two-phase property mode verification. +verifyMethodForProperty :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) + => Method -> SolcContract -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) +verifyMethodForProperty method contract vm = do + conf <- asks (.cfg) + dappInfo <- asks (.dapp) let - vm' = vmReset & execState (loadContract (LitAddr dst)) - & #tx % #isCreate .~ False - & #state % #callvalue .~ (if isFoundryMode conf.solConf.testMode then Lit 0 else TxValue) - & #state % #caller .~ SymAddr "caller" - & #state % #calldata .~ cd - - vm'' = symbolify vm' - & #block %~ blockMakeSymbolic - & #constraints %~ (addBlockConstraints conf.txConf.maxTimeDelay conf.txConf.maxBlockDelay vm'.block) - & #constraints %~ (++ constraints ++ senderConstraints conf.solConf.sender) - - -- Phase 1: PBool True postcondition → no solver calls, all Success paths return Qed - (phase1Models, phase1Partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (\_ _ -> PBool True) Nothing - - -- Extract Success leaves with their path constraints and symbolic contract states - let successLeaves = [(props, contracts) | (_, Success props _ _ contracts) <- phase1Models] - - -- Phase 2: For each Success leaf, check each property function - allResults <- concat <$> mapM (checkLeaf fetcher dst vm cd method conf defaultSender solvers veriOpts propertyMethods) successLeaves - - let allPartialLogs = map (\(p, _) -> formatPartialDetailed Nothing Map.empty p) phase1Partials - return (allResults, allPartialLogs) - - where + propertyMethods = filter (\m -> Text.isPrefixOf conf.solConf.prefix m.name) $ Map.elems contract.abiMap + timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout) + maxIters = Just conf.campaignConf.symExecMaxIters + maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore) + askSmtIters = conf.campaignConf.symExecAskSMTIters + rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock)) + defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0 - -- | Phase 2 for a single Success leaf: check all property methods - checkLeaf fetcher dst vm0 cd method0 conf0 defaultSender0 solvers0 veriOpts0 propMethods (leafConstraints, leafContracts) = do - let convertedContracts = Map.map fromEContract leafContracts - concat <$> mapM (checkProperty fetcher dst vm0 cd method0 conf0 defaultSender0 solvers0 veriOpts0 convertedContracts leafConstraints) propMethods + threadIdChan <- liftIO newEmptyMVar + doneChan <- liftIO newEmptyMVar + 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 veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo } + let runtimeEnv = defaultEnv { config = hevmConfig } + session <- asks (.fetchSession) + pushWorkerEvent $ SymExecLog ("Two-phase property verification: " <> show method.name) - -- | Phase 2 for a single (leaf, property) pair - checkProperty fetcher dst vm0 cd method0 conf0 defaultSender0 solvers0 veriOpts0 convertedContracts leafConstraints propMethod = do - vmReset2 <- liftIO $ snd <$> runStateT (fromEVM resetState) vm0 - let - propCd = ConcreteBuf (selector propMethod.methodSignature) - -- Replace contracts with phase 1's symbolic state, keeping originals as fallback - vm2 = vmReset2 & #env % #contracts %~ Map.union convertedContracts - & execState (loadContract (LitAddr dst)) - & #tx % #isCreate .~ False - & #state % #callvalue .~ Lit 0 - & #state % #caller .~ SymAddr "caller" - & #state % #calldata .~ propCd - -- Carry over phase 1's path constraints so the solver must satisfy both phases - vm2' = symbolify vm2 - & #constraints .~ leafConstraints + liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do + threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do + (res, partials) <- exploreMethodTwoPhase checkPropertyReturn method propertyMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + liftIO $ putMVar resultChan (res, partials) + liftIO $ putMVar doneChan () + liftIO $ putMVar threadIdChan threadId + liftIO $ takeMVar doneChan - (phase2Models, _) <- verifyInputsWithHandler solvers0 veriOpts0 fetcher vm2' checkPropertyReturn Nothing - let results2 = filter (\(r, _) -> not (isQed r)) phase2Models & map fst - return $ map (modelToTx dst vm0.block.timestamp vm0.block.number method0 conf0.solConf.sender defaultSender0 cd) results2 + threadId <- liftIO $ takeMVar threadIdChan + pure (threadId, resultChan) --- | Two-phase symbolic verification for property mode. --- Phase 1: Symbolically execute the state-changing method to collect all --- reachable symbolic states (no solver calls). --- Phase 2: For each symbolic state, execute each property function and use --- the solver to find inputs that make the property return false. -verifyMethodForProperty :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) => Method -> SolcContract -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) -verifyMethodForProperty method contract vm = do +-- | Spawn a thread for two-phase assertion mode verification (no-arg functions). +verifyMethodForAssertion :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) + => [Method] -> Method -> SolcContract -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) +verifyMethodForAssertion assertionMethods method contract vm = do conf <- asks (.cfg) dappInfo <- asks (.dapp) let + isFoundry = isFoundryMode conf.solConf.testMode timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout) maxIters = Just conf.campaignConf.symExecMaxIters maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore) askSmtIters = conf.campaignConf.symExecAskSMTIters rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock)) defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0 - -- Find property methods: functions with the configured prefix (e.g., "echidna_") - prefix = conf.solConf.prefix - propertyMethods = filter (\m -> Text.isPrefixOf prefix m.name) $ Map.elems contract.abiMap threadIdChan <- liftIO newEmptyMVar doneChan <- liftIO newEmptyMVar resultChan <- liftIO newEmptyMVar let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text - let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = StackBased} + 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 veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo} + let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo } let runtimeEnv = defaultEnv { config = hevmConfig } session <- asks (.fetchSession) - pushWorkerEvent $ SymExecLog ("Verifying (property mode) " <> (show method.name)) + pushWorkerEvent $ SymExecLog ("Two-phase assertion verification: " <> show method.name) liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do - (res, partials) <- exploreMethodForProperty method propertyMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + (res, partials) <- exploreMethodTwoPhase (checkAssertions [0x1] isFoundry) method assertionMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session liftIO $ putMVar resultChan (res, partials) liftIO $ putMVar doneChan () liftIO $ putMVar threadIdChan threadId diff --git a/src/test/Common.hs b/src/test/Common.hs index fc8ef8e79..9182c88d8 100644 --- a/src/test/Common.hs +++ b/src/test/Common.hs @@ -1,10 +1,12 @@ module Common ( testConfig , runContract + , runContractMultiWorker , testContract , testContractV , solcV , testContract' + , testContractMultiWorker , testContractNamed , checkConstructorConditions , optimized @@ -23,6 +25,8 @@ module Common , gasConsumedGt ) where +import Control.Concurrent (forkIO) +import Control.Concurrent.MVar (newEmptyMVar, putMVar, takeMVar) import Control.Monad (forM_) import Control.Monad.Random (getRandomR) import Control.Monad.Reader (runReaderT) @@ -44,6 +48,9 @@ import EVM.Types hiding (Env, Gas) import Echidna (mkEnv, prepareContract) import Echidna.Campaign (runWorker) +import Echidna.Types.Campaign (getNFuzzWorkers) +import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..)) +import Echidna.Worker (pushCampaignEvent) import Echidna.Config (parseConfig, defaultConfig) import Echidna.Solidity (selectMainContract, mkTests, loadSpecified, compileContracts) import Echidna.Test (checkETest) @@ -53,7 +60,6 @@ import Echidna.Types.Signature (ContractName) import Echidna.Types.Solidity (SolConf(..)) import Echidna.Types.Test import Echidna.Types.Tx (Tx(..), TxCall(..)) -import Echidna.Types.Worker (WorkerType(..)) import Echidna.Types.World (World(..)) testConfig :: EConfig @@ -103,6 +109,49 @@ runContract f selectedContract cfg workerType = do -- be IO pure (env, finalState) +-- | Run a contract with multiple workers (fuzz + symbolic) concurrently. +-- Returns the env and the symbolic worker's state. +runContractMultiWorker :: FilePath -> Maybe ContractName -> EConfig -> IO (Env, WorkerState) +runContractMultiWorker f selectedContract cfg = do + seed <- maybe (getRandomR (0, maxBound)) pure cfg.campaignConf.seed + buildOutput <- compileContracts cfg.solConf (f :| []) + (vm, env, dict) <- prepareContract cfg (f :| []) buildOutput selectedContract seed + let nFuzz = getNFuzzWorkers cfg.campaignConf + -- Spawn fuzz workers, push WorkerStopped when done + forM_ [0..nFuzz-1] $ \wid -> + forkIO $ do + (stopReason, _) <- flip runReaderT env $ + runWorker FuzzWorker (pure ()) vm dict wid [] cfg.campaignConf.testLimit selectedContract + pushCampaignEvent env (WorkerEvent wid FuzzWorker (WorkerStopped stopReason)) + -- Spawn symbolic worker (last worker ID) + let symWid = nFuzz + symResult <- newEmptyMVar + _ <- forkIO $ do + result <- flip runReaderT env $ + runWorker SymbolicWorker (pure ()) vm dict symWid [] cfg.campaignConf.testLimit selectedContract + putMVar symResult result + -- Wait for symbolic worker (it exits after all fuzz workers send WorkerStopped) + (_stopReason, finalState) <- takeMVar symResult + pure (env, finalState) + +testContractMultiWorker + :: FilePath + -> Maybe ContractName + -> Maybe SolcVersionComp + -> Maybe FilePath + -> [(String, (Env, WorkerState) -> IO Bool)] + -> TestTree +testContractMultiWorker fp n v configPath expectations = testCase fp $ withSolcVersion v $ do + c <- case configPath of + Just path -> do + parsed <- parseConfig path + pure parsed.econfig + Nothing -> pure testConfig + let c' = c & overrideQuiet + result <- runContractMultiWorker fp n c' + forM_ expectations $ \(message, assertion) -> do + assertion result >>= assertBool message + testContract :: FilePath -> Maybe FilePath diff --git a/src/test/Tests/Symbolic.hs b/src/test/Tests/Symbolic.hs index 95f0ef9f8..0a5eaaaea 100644 --- a/src/test/Tests/Symbolic.hs +++ b/src/test/Tests/Symbolic.hs @@ -2,7 +2,7 @@ module Tests.Symbolic (symbolicTests) where import Test.Tasty (TestTree, testGroup) -import Common (testContract', solcV, solved, passed, verified) +import Common (testContract', testContractMultiWorker, solcV, solved, passed, verified) import Echidna.Types.Worker (WorkerType(..)) symbolicTests :: TestTree @@ -24,6 +24,16 @@ symbolicTests = testGroup "Symbolic tests" $ , ("echidna_y_below_40 falsified", solved "echidna_y_below_40") , ("echidna_locked_before_1000 falsified", solved "echidna_locked_before_1000") ] + , testContract' "symbolic/verify-assertion-noarg.sol" (Just "AssertionNoArgTest") (Just (>= solcV (0,6,9))) (Just "symbolic/verify-assertion-noarg.yaml") True SymbolicWorker + [ ("check_x_not_ten falsified", solved "check_x_not_ten") + , ("check_y_below_100 falsified", solved "check_y_below_100") + , ("check_x_not_one passed", passed "check_x_not_one") + ] + ] + ++ [ + testContractMultiWorker "symbolic/motiv.sol" (Just "Motiv") (Just (>= solcV (0,6,9))) (Just "symbolic/motiv-explore.yaml") + [ ("h() falsified", solved "h") + ] ] ++ ([ -- This test is commented out because it requires a specific setup where both the FuzzWorker and SymbolicWorker are used. diff --git a/tests/solidity/symbolic/motiv-explore.yaml b/tests/solidity/symbolic/motiv-explore.yaml new file mode 100644 index 000000000..2f8678d5f --- /dev/null +++ b/tests/solidity/symbolic/motiv-explore.yaml @@ -0,0 +1,6 @@ +testMode: assertion +symExec: true +symExecSMTSolver: z3 +workers: 2 +testLimit: 50000 +seed: 1 diff --git a/tests/solidity/symbolic/motiv.sol b/tests/solidity/symbolic/motiv.sol new file mode 100644 index 000000000..a691a42fb --- /dev/null +++ b/tests/solidity/symbolic/motiv.sol @@ -0,0 +1,30 @@ +// SPDX-License-Identifier: MIT +pragma solidity >=0.6.9; + +// Adapted from Smartian's motivating example. +// Requires a 3-step chain: f(x) → g(y) → h() +// where x % 32 == 1 and y == 72. +contract Motiv { + address owner; + uint private stateA = 0; + uint private stateB = 0; + uint CONST = 32; + + constructor() public { + owner = msg.sender; + } + + function f(uint x) public { + if (msg.sender == owner) { stateA = x; } + } + + function g(uint y) public { + if (stateA % CONST == 1) { + stateB = y - 10; + } + } + + function h() public view { + assert(stateB != 62); + } +} diff --git a/tests/solidity/symbolic/motiv.yaml b/tests/solidity/symbolic/motiv.yaml new file mode 100644 index 000000000..a5e2a935b --- /dev/null +++ b/tests/solidity/symbolic/motiv.yaml @@ -0,0 +1,6 @@ +testMode: assertion +symExec: true +symExecSMTSolver: z3 +workers: 0 +seqLen: 1 +disableSlither: true diff --git a/tests/solidity/symbolic/verify-assertion-noarg.sol b/tests/solidity/symbolic/verify-assertion-noarg.sol new file mode 100644 index 000000000..330f24884 --- /dev/null +++ b/tests/solidity/symbolic/verify-assertion-noarg.sol @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: MIT +pragma solidity >=0.6.9; + +// Test contract for two-phase assertion mode: no-arg assertion functions +// that can only be falsified via state set by other functions. +contract AssertionNoArgTest { + uint256 public x; + uint256 public y; + + function set_x(uint256 _x) public { + require(_x >= 5, "too low"); + require(_x <= 20, "too high"); + x = _x; + } + + function set_y(uint256 _y) public { + require(_y > 0, "must be positive"); + y = _y; + } + + // No-arg assertion: should be falsified when x == 10 + function check_x_not_ten() public view { + assert(x != 10); + } + + // No-arg assertion: should be falsified when y >= 100 + function check_y_below_100() public view { + assert(y < 100); + } + + // No-arg assertion: should never be falsified (x can't be 1 due to require >= 5) + function check_x_not_one() public view { + assert(x != 1); + } +} diff --git a/tests/solidity/symbolic/verify-assertion-noarg.yaml b/tests/solidity/symbolic/verify-assertion-noarg.yaml new file mode 100644 index 000000000..a5e2a935b --- /dev/null +++ b/tests/solidity/symbolic/verify-assertion-noarg.yaml @@ -0,0 +1,6 @@ +testMode: assertion +symExec: true +symExecSMTSolver: z3 +workers: 0 +seqLen: 1 +disableSlither: true From 097ada87a01c12d05272cc57cdc0f5ab1ed3a7df Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 14:07:06 +0100 Subject: [PATCH 03/14] fix --- src/test/Common.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/test/Common.hs b/src/test/Common.hs index 9182c88d8..6005348c8 100644 --- a/src/test/Common.hs +++ b/src/test/Common.hs @@ -48,7 +48,6 @@ import EVM.Types hiding (Env, Gas) import Echidna (mkEnv, prepareContract) import Echidna.Campaign (runWorker) -import Echidna.Types.Campaign (getNFuzzWorkers) import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..)) import Echidna.Worker (pushCampaignEvent) import Echidna.Config (parseConfig, defaultConfig) From b2dab45596650ab2f55655e0a0048933000ab4f3 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 14:14:58 +0100 Subject: [PATCH 04/14] better status messages --- lib/Echidna/Campaign.hs | 19 ++++++++----------- lib/Echidna/SymExec/Exploration.hs | 5 +++-- lib/Echidna/SymExec/Property.hs | 6 ++++-- lib/Echidna/SymExec/Verification.hs | 2 +- 4 files changed, 16 insertions(+), 16 deletions(-) diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs index fd07eabd6..cccd1aa9f 100644 --- a/lib/Echidna/Campaign.hs +++ b/lib/Echidna/Campaign.hs @@ -347,7 +347,8 @@ runSymWorker callback vm dict workerId _ name = do -- Two-phase for no-arg assertion functions unless (null noArgAssertions || null stateChangingMethods) $ do - pushWorkerEvent $ SymExecLog ("Two-phase assertion: " <> show (length noArgAssertions) <> " no-arg target(s), " <> show (length stateChangingMethods) <> " state-changing method(s)") + let targetNames = unwords $ map (unpack . (.methodSignature)) noArgAssertions + pushWorkerEvent $ SymExecLog ("Two-phase assertion verification for [" <> targetNames <> "]") forM_ stateChangingMethods $ \method -> symExecMethodAssertion contract method noArgAssertions @@ -369,7 +370,7 @@ runSymWorker callback vm dict workerId _ name = do let methodSignature = unpack method.methodSignature - pushWorkerEvent $ SymExecLog ("Assertion two-phase: found " <> show (length txs) <> " concrete tx(es) for method " <> methodSignature) + pushWorkerEvent $ SymExecLog ("Assertion two-phase " <> methodSignature <> ": " <> show (length txs) <> " tx(es)") conf <- asks (.cfg) let dst = conf.solConf.contractAddr @@ -421,7 +422,7 @@ runSymWorker callback vm dict workerId _ name = do forM_ stateChangingMethods $ \method -> symExecMethodProperty contract method - pushWorkerEvent $ SymExecLog ("Property mode symbolic verification finished for contract " <> unpack (fromJust name)) + pushWorkerEvent $ SymExecLog "Property verification finished" -- | Symbolically execute a method in property mode: find concrete inputs -- for all reachable paths, then check each against all property tests. @@ -441,19 +442,17 @@ runSymWorker callback vm dict workerId _ name = do let methodSignature = unpack method.methodSignature - pushWorkerEvent $ SymExecLog ("Property mode: found " <> show (length txs) <> " concrete tx(es) for method " <> methodSignature <> ", " <> show (length errors) <> " error(s), " <> show (length partials) <> " partial(s)") + pushWorkerEvent $ SymExecLog ("Property two-phase " <> methodSignature <> ": " <> show (length txs) <> " tx(es)") -- For each concrete tx from symbolic execution, execute it and check properties forM_ txs $ \symTx -> do (_, vm') <- execTx vm symTx - pushWorkerEvent $ SymExecLog ("Property mode: executed tx " <> show symTx.call) case vm'.result of Just (VMSuccess _) -> do -- Check all open property tests against the post-transaction state updateTests $ \test -> do if isOpen test && isPropertyTest test then do (testValue, vm'') <- checkETest test vm' - pushWorkerEvent $ SymExecLog ("Property mode: checked property, value = " <> show testValue) case testValue of BoolValue False -> do wid <- Just <$> gets (.workerId) @@ -469,10 +468,8 @@ runSymWorker callback vm dict workerId _ name = do else pure Nothing _ -> pure () - unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during property verification of method " <> methodSignature <> ": " <> show e)) errors - unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during property verification of method " <> methodSignature <> ": " <> unpack e)) partials - - pushWorkerEvent $ SymExecLog ("Property mode symbolic execution finished for method " <> methodSignature) + unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error during property verification of " <> methodSignature <> ": " <> show e)) errors + unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial path during property verification of " <> methodSignature <> ": " <> unpack e)) partials symExecMethod contract method = do lift callback @@ -508,7 +505,7 @@ runSymWorker callback vm dict workerId _ name = do else pure $ Just test - pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction.") + pushWorkerEvent $ SymExecLog "Assertion verification finished" -- | Run a fuzzing campaign given an initial universe state, some tests, and an -- optional dictionary to generate calls with. Return the 'Campaign' state once diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index 6817d8993..da963938e 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -103,7 +103,7 @@ exploreContract contract method vm = do let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo} let runtimeEnv = defaultEnv { config = hevmConfig } session <- asks (.fetchSession) - pushWorkerEvent $ SymExecLog ("Exploring " <> (show method.name)) + pushWorkerEvent $ SymExecLog ("Exploring " <> unpack method.methodSignature) liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do -- For now, we will be exploring a single method at a time. @@ -144,7 +144,8 @@ exploreContractTwoPhase contract method targetMethods vm = do let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo } let runtimeEnv = defaultEnv { config = hevmConfig } session <- asks (.fetchSession) - pushWorkerEvent $ SymExecLog ("Two-phase exploring " <> show method.name <> " against " <> show (length targetMethods) <> " assertion target(s)") + let targetNames = unwords $ map (unpack . (.methodSignature)) targetMethods + pushWorkerEvent $ SymExecLog ("Two-phase exploring " <> unpack method.methodSignature <> " -> [" <> targetNames <> "]") liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do res <- exploreMethodTwoPhase (checkAssertions [0x1] isFoundry) method targetMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session diff --git a/lib/Echidna/SymExec/Property.hs b/lib/Echidna/SymExec/Property.hs index 786ae6855..e5339b67d 100644 --- a/lib/Echidna/SymExec/Property.hs +++ b/lib/Echidna/SymExec/Property.hs @@ -80,7 +80,8 @@ verifyMethodForProperty method contract vm = do let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo } let runtimeEnv = defaultEnv { config = hevmConfig } session <- asks (.fetchSession) - pushWorkerEvent $ SymExecLog ("Two-phase property verification: " <> show method.name) + let propertyNames = unwords $ map (Text.unpack . (.methodSignature)) propertyMethods + pushWorkerEvent $ SymExecLog ("Verifying property: " <> Text.unpack method.methodSignature <> " -> [" <> propertyNames <> "]") liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do @@ -117,7 +118,8 @@ verifyMethodForAssertion assertionMethods method contract vm = do let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo } let runtimeEnv = defaultEnv { config = hevmConfig } session <- asks (.fetchSession) - pushWorkerEvent $ SymExecLog ("Two-phase assertion verification: " <> show method.name) + let targetNames = unwords $ map (Text.unpack . (.methodSignature)) assertionMethods + pushWorkerEvent $ SymExecLog ("Verifying assertion: " <> Text.unpack method.methodSignature <> " -> [" <> targetNames <> "]") liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do diff --git a/lib/Echidna/SymExec/Verification.hs b/lib/Echidna/SymExec/Verification.hs index 7a3e80ed5..fc490369d 100644 --- a/lib/Echidna/SymExec/Verification.hs +++ b/lib/Echidna/SymExec/Verification.hs @@ -66,7 +66,7 @@ verifyMethod method contract vm = do let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo} let runtimeEnv = defaultEnv { config = hevmConfig } session <- asks (.fetchSession) - pushWorkerEvent $ SymExecLog ("Verifying " <> (show method.name)) + pushWorkerEvent $ SymExecLog ("Verifying " <> Text.unpack method.methodSignature) liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do From 9ff231cd955eb2b3d79f13719e11ef87adf628d6 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 14:48:07 +0100 Subject: [PATCH 05/14] fixes --- lib/Echidna/Campaign.hs | 71 ++++++++++++++++++++++++++---- lib/Echidna/SymExec/Exploration.hs | 23 +++++++--- 2 files changed, 80 insertions(+), 14 deletions(-) diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs index cccd1aa9f..2eeb38e23 100644 --- a/lib/Echidna/Campaign.hs +++ b/lib/Echidna/Campaign.hs @@ -20,10 +20,10 @@ import Data.List qualified as List import Data.List.NonEmpty qualified as NEList import Data.Map (Map, (\\)) import Data.Map qualified as Map -import Data.Maybe (isJust, mapMaybe, fromJust) +import Data.Maybe (isJust, mapMaybe) import Data.Set (Set) import Data.Set qualified as Set -import Data.Text (Text, pack, unpack) +import Data.Text (Text, isPrefixOf, pack, unpack) import Data.Time (LocalTime) import Data.Vector qualified as V import System.Random (mkStdGen) @@ -41,7 +41,7 @@ import Echidna.Mutator.Corpus import Echidna.Shrink (shrinkTest) import Echidna.Solidity (chooseContract) import Echidna.SymExec.Common (extractTxs, extractErrors, suitableForSymExec) -import Echidna.SymExec.Exploration (exploreContract, exploreContractTwoPhase, getTargetMethodFromTx, getRandomTargetMethod) +import Echidna.SymExec.Exploration (exploreContract, exploreContractTwoPhase, exploreContractTwoPhaseProperty, getTargetMethodFromTx, getRandomTargetMethod) import Echidna.SymExec.Symbolic (forceAddr) import Echidna.SymExec.Property (verifyMethodForProperty, verifyMethodForAssertion, isSuitableForPropertyMode, isNoArgAssertionTarget) import Echidna.SymExec.Verification (verifyMethod, isSuitableToVerifyMethod) @@ -243,13 +243,26 @@ runSymWorker callback vm dict workerId _ name = do Just t -> getTargetMethodFromTx t contract failedTestSignatures >>= \case Nothing -> pure () Just method -> exploreAndVerify contract method vm' txsBase - -- Two-phase exploration: any state-changing method → no-arg assertion targets - let noArgTargets = filter isNoArgAssertionTarget $ Map.elems contract.abiMap + -- Two-phase exploration: any state-changing method → no-arg targets + -- Filter to only targets that have registered open tests + testRefs <- asks (.testRefs) + tests <- liftIO $ traverse readIORef testRefs + let prefix = conf.solConf.prefix stateChanging = filter suitableForSymExec $ Map.elems contract.abiMap + noArgTargets + | isPropertyMode conf.solConf.testMode = + -- Property mode: only echidna_ functions that have open property tests + let propNames = [n | t <- tests, isOpen t, isPropertyTest t, PropertyTest n _ <- [t.testType]] + in filter (\m -> null m.inputs && m.name `elem` propNames) $ Map.elems contract.abiMap + | otherwise = + -- Assertion mode: only no-arg functions that have open assertion tests + let assertSigs = [getAssertionSignature t | t <- tests, isOpen t, isAssertionTest t] + in filter (\m -> isNoArgAssertionTarget m && unpack m.methodSignature `elem` assertSigs) $ Map.elems contract.abiMap unless (null noArgTargets || null stateChanging) $ do - -- Pick a random state-changing method for two-phase method <- liftIO $ rElem (NEList.fromList stateChanging) - exploreAndVerifyTwoPhase contract method noArgTargets vm' txsBase + if isPropertyMode conf.solConf.testMode + then exploreAndVerifyTwoPhaseProperty contract method noArgTargets vm' txsBase + else exploreAndVerifyTwoPhase contract method noArgTargets vm' txsBase exploreAndVerify contract method vm' txsBase = do -- Single-phase exploration (existing) @@ -315,8 +328,48 @@ runSymWorker callback vm dict workerId _ name = do else pure Nothing _ -> pure () - unless (null errors2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during two-phase exploration: " <> show e)) errors2 - unless (null partials2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during two-phase exploration: " <> unpack e)) partials2 + unless (null errors2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error during two-phase assertion exploration: " <> show e)) errors2 + unless (null partials2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial path during two-phase assertion exploration: " <> unpack e)) partials2 + + -- | Two-phase exploration for property mode: execute a state-changing method + -- symbolically, then check property functions against the resulting states. + exploreAndVerifyTwoPhaseProperty contract method targets vm' txsBase = do + (threadId2, symTxsChan2) <- exploreContractTwoPhaseProperty contract method targets vm' + modify' (\ws -> ws { runningThreads = [threadId2] }) + lift callback + + (symTxs2, partials2) <- liftIO $ takeMVar symTxsChan2 + let txs2 = extractTxs symTxs2 + let errors2 = extractErrors symTxs2 + + modify' (\ws -> ws { runningThreads = [] }) + lift callback + + -- For each concrete tx, execute it and check property functions + forM_ txs2 $ \symTx -> do + (_, vmAfter) <- execTx vm symTx + case vmAfter.result of + Just (VMSuccess _) -> + updateTests $ \test -> do + if isOpen test && isPropertyTest test then do + (testValue, vmCheck) <- checkETest test vmAfter + case testValue of + BoolValue False -> do + wid <- Just <$> gets (.workerId) + let test' = test { Test.state = Large 0 + , reproducer = txsBase <> [symTx] + , vm = Just vmAfter + , result = getResultFromVM vmCheck + , Test.workerId = wid + } + pushWorkerEvent (TestFalsified test') + pure $ Just test' + _ -> pure Nothing + else pure Nothing + _ -> pure () + + unless (null errors2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error during two-phase property exploration: " <> show e)) errors2 + unless (null partials2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial path during two-phase property exploration: " <> unpack e)) partials2 verifyMethods = do dapp <- asks (.dapp) diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index da963938e..08c526e53 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -24,7 +24,10 @@ import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..)) import EVM.Types (VMType(..)) import qualified EVM.Types (VM(..)) +import EVM.SymExec (Postcondition) + import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, exploreMethodTwoPhase, checkAssertions, rpcFetcher, TxOrError(..), PartialsLogs) +import Echidna.SymExec.Property (checkPropertyReturn) import Echidna.Test (isFoundryMode) import Echidna.Types.Campaign (CampaignConf(..), WorkerState) import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..)) @@ -118,16 +121,26 @@ exploreContract contract method vm = do threadId <- liftIO $ takeMVar threadIdChan pure (threadId, resultChan) --- | Like 'exploreContract' but uses two-phase symbolic execution. --- Phase 1 explores the given method, phase 2 checks the given target methods --- (typically no-arg assertion functions) for violations. +-- | Two-phase exploration for assertion mode. exploreContractTwoPhase :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) exploreContractTwoPhase contract method targetMethods vm = do + conf <- asks (.cfg) + let isFoundry = isFoundryMode conf.solConf.testMode + exploreContractTwoPhaseWith (checkAssertions [0x1] isFoundry) contract method targetMethods vm + +-- | Two-phase exploration for property mode. +exploreContractTwoPhaseProperty :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) + => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) +exploreContractTwoPhaseProperty = exploreContractTwoPhaseWith checkPropertyReturn + +-- | Two-phase exploration parameterized by postcondition. +exploreContractTwoPhaseWith :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) + => Postcondition -> SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) +exploreContractTwoPhaseWith postcondition contract method targetMethods vm = do conf <- asks (.cfg) dappInfo <- asks (.dapp) let - isFoundry = isFoundryMode conf.solConf.testMode timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout) maxIters = Just conf.campaignConf.symExecMaxIters maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore) @@ -148,7 +161,7 @@ exploreContractTwoPhase contract method targetMethods vm = do pushWorkerEvent $ SymExecLog ("Two-phase exploring " <> unpack method.methodSignature <> " -> [" <> targetNames <> "]") liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do - res <- exploreMethodTwoPhase (checkAssertions [0x1] isFoundry) method targetMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + res <- exploreMethodTwoPhase postcondition method targetMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session liftIO $ putMVar resultChan res liftIO $ putMVar doneChan () liftIO $ putMVar threadIdChan threadId From db2aa50cae2531d068024b78ff38ea5ce5cf192f Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 14:49:44 +0100 Subject: [PATCH 06/14] fixes --- lib/Echidna/SymExec/Exploration.hs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index 08c526e53..6855faa0c 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -20,12 +20,10 @@ import EVM.Effects (defaultEnv, defaultConfig, Config(..), Env(..)) import EVM.Fetch (RpcInfo(..)) import EVM.Solidity (SolcContract(..), Method(..)) import EVM.Solvers (defMemLimit, withSolvers) -import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..)) +import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..), Postcondition) import EVM.Types (VMType(..)) import qualified EVM.Types (VM(..)) -import EVM.SymExec (Postcondition) - import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, exploreMethodTwoPhase, checkAssertions, rpcFetcher, TxOrError(..), PartialsLogs) import Echidna.SymExec.Property (checkPropertyReturn) import Echidna.Test (isFoundryMode) From a279861e3a75acc696d05b4fa597503f52e99a1c Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 14:52:43 +0100 Subject: [PATCH 07/14] fixes --- lib/Echidna/Campaign.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs index 2eeb38e23..3c3751577 100644 --- a/lib/Echidna/Campaign.hs +++ b/lib/Echidna/Campaign.hs @@ -23,7 +23,7 @@ import Data.Map qualified as Map import Data.Maybe (isJust, mapMaybe) import Data.Set (Set) import Data.Set qualified as Set -import Data.Text (Text, isPrefixOf, pack, unpack) +import Data.Text (Text, pack, unpack) import Data.Time (LocalTime) import Data.Vector qualified as V import System.Random (mkStdGen) @@ -247,8 +247,7 @@ runSymWorker callback vm dict workerId _ name = do -- Filter to only targets that have registered open tests testRefs <- asks (.testRefs) tests <- liftIO $ traverse readIORef testRefs - let prefix = conf.solConf.prefix - stateChanging = filter suitableForSymExec $ Map.elems contract.abiMap + let stateChanging = filter suitableForSymExec $ Map.elems contract.abiMap noArgTargets | isPropertyMode conf.solConf.testMode = -- Property mode: only echidna_ functions that have open property tests From 1a3e526e7f1ce61cd16791c966e6d071e0f2ed21 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 16:34:15 +0100 Subject: [PATCH 08/14] better logging --- lib/Echidna/Campaign.hs | 20 ++++++++++++------ lib/Echidna/SymExec/Common.hs | 5 +++-- lib/Echidna/SymExec/Exploration.hs | 33 ++++++++++++++++-------------- lib/Echidna/SymExec/Property.hs | 29 +++++++++++++++----------- 4 files changed, 52 insertions(+), 35 deletions(-) diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs index 3c3751577..5ad61fa7b 100644 --- a/lib/Echidna/Campaign.hs +++ b/lib/Echidna/Campaign.hs @@ -228,6 +228,13 @@ runSymWorker callback vm dict workerId _ name = do pure [(Nothing, rvm, rtxs)] + txsBaseLabel txs = case txs of + [] -> "initial state" + _ -> show (length txs) <> "-tx sequence ending with " <> showTxCall (last txs) + where showTxCall t = case t.call of + SolCall (n, _) -> unpack n + _ -> "unknown" + symexecTx (tx, vm', txsBase) = do conf <- asks (.cfg) dapp <- asks (.dapp) @@ -259,9 +266,10 @@ runSymWorker callback vm dict workerId _ name = do in filter (\m -> isNoArgAssertionTarget m && unpack m.methodSignature `elem` assertSigs) $ Map.elems contract.abiMap unless (null noArgTargets || null stateChanging) $ do method <- liftIO $ rElem (NEList.fromList stateChanging) + let baseLabel = txsBaseLabel txsBase if isPropertyMode conf.solConf.testMode - then exploreAndVerifyTwoPhaseProperty contract method noArgTargets vm' txsBase - else exploreAndVerifyTwoPhase contract method noArgTargets vm' txsBase + then exploreAndVerifyTwoPhaseProperty contract method noArgTargets vm' txsBase baseLabel + else exploreAndVerifyTwoPhase contract method noArgTargets vm' txsBase baseLabel exploreAndVerify contract method vm' txsBase = do -- Single-phase exploration (existing) @@ -287,10 +295,10 @@ runSymWorker callback vm dict workerId _ name = do pushWorkerEvent $ SymExecError "No errors but symbolic execution found valid txs breaking assertions. Something is wrong.") unless newCoverage (pushWorkerEvent $ SymExecLog "Symbolic execution finished with no new coverage.") - exploreAndVerifyTwoPhase contract method targets vm' txsBase = do + exploreAndVerifyTwoPhase contract method targets vm' txsBase baseLabel = do conf <- asks (.cfg) let dst = conf.solConf.contractAddr - (threadId2, symTxsChan2) <- exploreContractTwoPhase contract method targets vm' + (threadId2, symTxsChan2) <- exploreContractTwoPhase contract method targets vm' baseLabel modify' (\ws -> ws { runningThreads = [threadId2] }) lift callback @@ -332,8 +340,8 @@ runSymWorker callback vm dict workerId _ name = do -- | Two-phase exploration for property mode: execute a state-changing method -- symbolically, then check property functions against the resulting states. - exploreAndVerifyTwoPhaseProperty contract method targets vm' txsBase = do - (threadId2, symTxsChan2) <- exploreContractTwoPhaseProperty contract method targets vm' + exploreAndVerifyTwoPhaseProperty contract method targets vm' txsBase baseLabel = do + (threadId2, symTxsChan2) <- exploreContractTwoPhaseProperty contract method targets vm' baseLabel modify' (\ws -> ws { runningThreads = [threadId2] }) lift callback diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs index 4bce00aa6..762114bd7 100644 --- a/lib/Echidna/SymExec/Common.hs +++ b/lib/Echidna/SymExec/Common.hs @@ -226,9 +226,9 @@ fromEContract _ = error "fromEContract: unexpected non-C expression" -- postcondition. The solver finds concrete values for phase 1's symbolic -- variables (calldata, caller, etc.) that cause a violation. exploreMethodTwoPhase :: (MonadUnliftIO m, ReadConfig m, TTY m) => - Postcondition -> Method -> [Method] -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs) + Postcondition -> (Method -> m ()) -> Method -> [Method] -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs) -exploreMethodTwoPhase phase2Post method targetMethods _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do +exploreMethodTwoPhase phase2Post logTarget method targetMethods _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do -- Phase 1: Execute state-changing method symbolically calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) [] let @@ -269,6 +269,7 @@ exploreMethodTwoPhase phase2Post method targetMethods _contract _sources vm defa -- | Phase 2 for a single (leaf, target) pair checkTarget fetcher dst vm0 cd convertedContracts leafConstraints targetMethod = do + logTarget targetMethod vmReset2 <- liftIO $ snd <$> runStateT (fromEVM resetState) vm0 let targetCd = ConcreteBuf (selector targetMethod.methodSignature) diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index 6855faa0c..5e40bb8b3 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -8,7 +8,7 @@ import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar) import Control.Monad.Catch (MonadThrow(..)) import Control.Monad.IO.Class (MonadIO) import Control.Monad.Reader (MonadReader, ask, asks, runReaderT, liftIO) -import Control.Monad.State.Strict (MonadState) +import Control.Monad.State.Strict (MonadState, gets) import Data.List.NonEmpty (fromList) import Data.Map qualified as Map import Data.Maybe (fromJust) @@ -27,14 +27,14 @@ import qualified EVM.Types (VM(..)) import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, exploreMethodTwoPhase, checkAssertions, rpcFetcher, TxOrError(..), PartialsLogs) import Echidna.SymExec.Property (checkPropertyReturn) import Echidna.Test (isFoundryMode) -import Echidna.Types.Campaign (CampaignConf(..), WorkerState) +import Echidna.Types.Campaign (CampaignConf(..), WorkerState(..)) import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..)) import Echidna.Types.Random (rElem) import Echidna.Types.Solidity (SolConf(..)) import Echidna.Types.Tx (Tx(..), TxCall(..)) -import Echidna.Types.Worker (WorkerEvent(..)) +import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..)) import Echidna.Types.World (World(..)) -import Echidna.Worker (pushWorkerEvent) +import Echidna.Worker (pushWorkerEvent, pushCampaignEvent) -- | Uses symbolic execution to find transactions which would increase coverage. -- Spawns a new thread; returns its thread ID as the first return value. @@ -121,22 +121,25 @@ exploreContract contract method vm = do -- | Two-phase exploration for assertion mode. exploreContractTwoPhase :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) - => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) -exploreContractTwoPhase contract method targetMethods vm = do + => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) +exploreContractTwoPhase contract method targetMethods vm baseLabel = do conf <- asks (.cfg) let isFoundry = isFoundryMode conf.solConf.testMode - exploreContractTwoPhaseWith (checkAssertions [0x1] isFoundry) contract method targetMethods vm + exploreContractTwoPhaseWith (checkAssertions [0x1] isFoundry) contract method targetMethods vm baseLabel -- | Two-phase exploration for property mode. exploreContractTwoPhaseProperty :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) - => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) -exploreContractTwoPhaseProperty = exploreContractTwoPhaseWith checkPropertyReturn + => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) +exploreContractTwoPhaseProperty = + exploreContractTwoPhaseWith checkPropertyReturn -- | Two-phase exploration parameterized by postcondition. exploreContractTwoPhaseWith :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) - => Postcondition -> SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) -exploreContractTwoPhaseWith postcondition contract method targetMethods vm = do - conf <- asks (.cfg) + => Postcondition -> SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) +exploreContractTwoPhaseWith postcondition contract method targetMethods vm baseLabel = do + env <- ask + wid <- gets (.workerId) + let conf = env.cfg dappInfo <- asks (.dapp) let timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout) @@ -155,11 +158,11 @@ exploreContractTwoPhaseWith postcondition contract method targetMethods vm = do let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo } let runtimeEnv = defaultEnv { config = hevmConfig } session <- asks (.fetchSession) - let targetNames = unwords $ map (unpack . (.methodSignature)) targetMethods - pushWorkerEvent $ SymExecLog ("Two-phase exploring " <> unpack method.methodSignature <> " -> [" <> targetNames <> "]") + let methodSig = unpack method.methodSignature + logTarget target = liftIO $ pushCampaignEvent env (WorkerEvent wid SymbolicWorker (SymExecLog ("Two-phase " <> baseLabel <> ": " <> methodSig <> " -> " <> unpack target.methodSignature))) liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do - res <- exploreMethodTwoPhase postcondition method targetMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + res <- exploreMethodTwoPhase postcondition logTarget method targetMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session liftIO $ putMVar resultChan res liftIO $ putMVar doneChan () liftIO $ putMVar threadIdChan threadId diff --git a/lib/Echidna/SymExec/Property.hs b/lib/Echidna/SymExec/Property.hs index e5339b67d..f9a69900c 100644 --- a/lib/Echidna/SymExec/Property.hs +++ b/lib/Echidna/SymExec/Property.hs @@ -7,8 +7,8 @@ import Control.Concurrent (ThreadId, forkIO) import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar) import Control.Monad.Catch (MonadThrow(..)) import Control.Monad.IO.Class (MonadIO) -import Control.Monad.Reader (MonadReader, asks, runReaderT, liftIO) -import Control.Monad.State.Strict (MonadState) +import Control.Monad.Reader (MonadReader, ask, asks, runReaderT, liftIO) +import Control.Monad.State.Strict (MonadState, gets) import Data.Map qualified as Map import Data.Maybe (fromJust) import Data.Set qualified as Set @@ -29,11 +29,12 @@ import Echidna.SymExec.Common , TxOrError(..), PartialsLogs ) import Echidna.Test (isFoundryMode) -import Echidna.Types.Campaign (CampaignConf(..), WorkerState) +import Echidna.Types.Campaign (CampaignConf(..), WorkerState(..)) import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..)) import Echidna.Types.Solidity (SolConf(..)) import Echidna.Types.Worker (WorkerEvent(..)) -import Echidna.Worker (pushWorkerEvent) +import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..)) +import Echidna.Worker (pushWorkerEvent, pushCampaignEvent) -- | Postcondition for property mode phase 2: check if property function -- returned false (i.e., return value is 0). @@ -60,7 +61,9 @@ isNoArgAssertionTarget m = null m.inputs verifyMethodForProperty :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) => Method -> SolcContract -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) verifyMethodForProperty method contract vm = do - conf <- asks (.cfg) + env <- ask + wid <- gets (.workerId) + let conf = env.cfg dappInfo <- asks (.dapp) let propertyMethods = filter (\m -> Text.isPrefixOf conf.solConf.prefix m.name) $ Map.elems contract.abiMap @@ -80,12 +83,12 @@ verifyMethodForProperty method contract vm = do let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo } let runtimeEnv = defaultEnv { config = hevmConfig } session <- asks (.fetchSession) - let propertyNames = unwords $ map (Text.unpack . (.methodSignature)) propertyMethods - pushWorkerEvent $ SymExecLog ("Verifying property: " <> Text.unpack method.methodSignature <> " -> [" <> propertyNames <> "]") + let methodSig = Text.unpack method.methodSignature + logTarget target = liftIO $ pushCampaignEvent env (WorkerEvent wid SymbolicWorker (SymExecLog ("Verifying property: " <> methodSig <> " -> " <> Text.unpack target.methodSignature))) liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do - (res, partials) <- exploreMethodTwoPhase checkPropertyReturn method propertyMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + (res, partials) <- exploreMethodTwoPhase checkPropertyReturn logTarget method propertyMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session liftIO $ putMVar resultChan (res, partials) liftIO $ putMVar doneChan () liftIO $ putMVar threadIdChan threadId @@ -98,7 +101,9 @@ verifyMethodForProperty method contract vm = do verifyMethodForAssertion :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) => [Method] -> Method -> SolcContract -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) verifyMethodForAssertion assertionMethods method contract vm = do - conf <- asks (.cfg) + env <- ask + wid <- gets (.workerId) + let conf = env.cfg dappInfo <- asks (.dapp) let isFoundry = isFoundryMode conf.solConf.testMode @@ -118,12 +123,12 @@ verifyMethodForAssertion assertionMethods method contract vm = do let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo } let runtimeEnv = defaultEnv { config = hevmConfig } session <- asks (.fetchSession) - let targetNames = unwords $ map (Text.unpack . (.methodSignature)) assertionMethods - pushWorkerEvent $ SymExecLog ("Verifying assertion: " <> Text.unpack method.methodSignature <> " -> [" <> targetNames <> "]") + let methodSig' = Text.unpack method.methodSignature + logTarget target = liftIO $ pushCampaignEvent env (WorkerEvent wid SymbolicWorker (SymExecLog ("Verifying assertion: " <> methodSig' <> " -> " <> Text.unpack target.methodSignature))) liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do - (res, partials) <- exploreMethodTwoPhase (checkAssertions [0x1] isFoundry) method assertionMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + (res, partials) <- exploreMethodTwoPhase (checkAssertions [0x1] isFoundry) logTarget method assertionMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session liftIO $ putMVar resultChan (res, partials) liftIO $ putMVar doneChan () liftIO $ putMVar threadIdChan threadId From 591153c188bde98e574f3dc441abf4511723187c Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 16:39:24 +0100 Subject: [PATCH 09/14] fix --- lib/Echidna/SymExec/Property.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/lib/Echidna/SymExec/Property.hs b/lib/Echidna/SymExec/Property.hs index f9a69900c..d52f55e77 100644 --- a/lib/Echidna/SymExec/Property.hs +++ b/lib/Echidna/SymExec/Property.hs @@ -32,7 +32,6 @@ import Echidna.Test (isFoundryMode) import Echidna.Types.Campaign (CampaignConf(..), WorkerState(..)) import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..)) import Echidna.Types.Solidity (SolConf(..)) -import Echidna.Types.Worker (WorkerEvent(..)) import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..)) import Echidna.Worker (pushWorkerEvent, pushCampaignEvent) From dc7e5483d95a7f4120fcdfcc2edbccefcd212610 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 16:50:28 +0100 Subject: [PATCH 10/14] fix --- lib/Echidna/SymExec/Property.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Echidna/SymExec/Property.hs b/lib/Echidna/SymExec/Property.hs index d52f55e77..be8d0c7b9 100644 --- a/lib/Echidna/SymExec/Property.hs +++ b/lib/Echidna/SymExec/Property.hs @@ -33,7 +33,7 @@ import Echidna.Types.Campaign (CampaignConf(..), WorkerState(..)) import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..)) import Echidna.Types.Solidity (SolConf(..)) import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..)) -import Echidna.Worker (pushWorkerEvent, pushCampaignEvent) +import Echidna.Worker (pushCampaignEvent) -- | Postcondition for property mode phase 2: check if property function -- returned false (i.e., return value is 0). From fb001aa6e89dfab92484648111c04dd43c2354cb Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 17:53:16 +0100 Subject: [PATCH 11/14] correct senders --- lib/Echidna/SymExec/Common.hs | 10 +++++++--- lib/Echidna/SymExec/Exploration.hs | 24 ++++++++++++++---------- lib/Echidna/SymExec/Property.hs | 7 +++++-- 3 files changed, 26 insertions(+), 15 deletions(-) diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs index 762114bd7..0f56de485 100644 --- a/lib/Echidna/SymExec/Common.hs +++ b/lib/Echidna/SymExec/Common.hs @@ -226,9 +226,9 @@ fromEContract _ = error "fromEContract: unexpected non-C expression" -- postcondition. The solver finds concrete values for phase 1's symbolic -- variables (calldata, caller, etc.) that cause a violation. exploreMethodTwoPhase :: (MonadUnliftIO m, ReadConfig m, TTY m) => - Postcondition -> (Method -> m ()) -> Method -> [Method] -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs) + Postcondition -> Expr EAddr -> (Method -> m ()) -> Method -> [Method] -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs) -exploreMethodTwoPhase phase2Post logTarget method targetMethods _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do +exploreMethodTwoPhase phase2Post phase2Caller logTarget method targetMethods _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do -- Phase 1: Execute state-changing method symbolically calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) [] let @@ -278,11 +278,15 @@ exploreMethodTwoPhase phase2Post logTarget method targetMethods _contract _sourc & execState (loadContract (LitAddr dst)) & #tx % #isCreate .~ False & #state % #callvalue .~ Lit 0 - & #state % #caller .~ SymAddr "caller" + & #state % #caller .~ phase2Caller & #state % #calldata .~ targetCd -- Carry over phase 1's path constraints so the solver must satisfy both phases + -- Reset exploration state so phase 2 gets fresh budget vm2' = symbolify vm2 & #constraints .~ leafConstraints + & #iterations .~ mempty + & #pathsVisited .~ mempty + & #exploreDepth .~ 0 (phase2Models, _) <- verifyInputsWithHandler solvers veriOpts fetcher vm2' phase2Post Nothing let results2 = filter (\(r, _) -> not (isQed r)) phase2Models & map fst diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index 5e40bb8b3..70d155499 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -21,7 +21,7 @@ import EVM.Fetch (RpcInfo(..)) import EVM.Solidity (SolcContract(..), Method(..)) import EVM.Solvers (defMemLimit, withSolvers) import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..), Postcondition) -import EVM.Types (VMType(..)) +import EVM.Types (Addr, VMType(..), EType(..), Expr(..)) import qualified EVM.Types (VM(..)) import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, exploreMethodTwoPhase, checkAssertions, rpcFetcher, TxOrError(..), PartialsLogs) @@ -29,6 +29,7 @@ import Echidna.SymExec.Property (checkPropertyReturn) import Echidna.Test (isFoundryMode) import Echidna.Types.Campaign (CampaignConf(..), WorkerState(..)) import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..)) +import Echidna.Types.Test (TestConf(..)) import Echidna.Types.Random (rElem) import Echidna.Types.Solidity (SolConf(..)) import Echidna.Types.Tx (Tx(..), TxCall(..)) @@ -119,24 +120,27 @@ exploreContract contract method vm = do threadId <- liftIO $ takeMVar threadIdChan pure (threadId, resultChan) --- | Two-phase exploration for assertion mode. +-- | Two-phase exploration for assertion mode (symbolic caller). exploreContractTwoPhase :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) exploreContractTwoPhase contract method targetMethods vm baseLabel = do conf <- asks (.cfg) let isFoundry = isFoundryMode conf.solConf.testMode - exploreContractTwoPhaseWith (checkAssertions [0x1] isFoundry) contract method targetMethods vm baseLabel + exploreContractTwoPhaseWith (checkAssertions [0x1] isFoundry) (SymAddr "caller") contract method targetMethods vm baseLabel --- | Two-phase exploration for property mode. +-- | Two-phase exploration for property mode (concrete test sender). exploreContractTwoPhaseProperty :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) -exploreContractTwoPhaseProperty = - exploreContractTwoPhaseWith checkPropertyReturn +exploreContractTwoPhaseProperty contract method targetMethods vm baseLabel = do + conf <- asks (.cfg) + let dst = conf.solConf.contractAddr + propertySender = LitAddr (conf.testConf.testSender dst) + exploreContractTwoPhaseWith checkPropertyReturn propertySender contract method targetMethods vm baseLabel --- | Two-phase exploration parameterized by postcondition. +-- | Two-phase exploration parameterized by postcondition and phase 2 caller. exploreContractTwoPhaseWith :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) - => Postcondition -> SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) -exploreContractTwoPhaseWith postcondition contract method targetMethods vm baseLabel = do + => Postcondition -> Expr EAddr -> SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs)) +exploreContractTwoPhaseWith postcondition phase2Caller contract method targetMethods vm baseLabel = do env <- ask wid <- gets (.workerId) let conf = env.cfg @@ -162,7 +166,7 @@ exploreContractTwoPhaseWith postcondition contract method targetMethods vm baseL logTarget target = liftIO $ pushCampaignEvent env (WorkerEvent wid SymbolicWorker (SymExecLog ("Two-phase " <> baseLabel <> ": " <> methodSig <> " -> " <> unpack target.methodSignature))) liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do - res <- exploreMethodTwoPhase postcondition logTarget method targetMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + res <- exploreMethodTwoPhase postcondition phase2Caller logTarget method targetMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session liftIO $ putMVar resultChan res liftIO $ putMVar doneChan () liftIO $ putMVar threadIdChan threadId diff --git a/lib/Echidna/SymExec/Property.hs b/lib/Echidna/SymExec/Property.hs index be8d0c7b9..78025b72b 100644 --- a/lib/Echidna/SymExec/Property.hs +++ b/lib/Echidna/SymExec/Property.hs @@ -31,6 +31,7 @@ import Echidna.SymExec.Common import Echidna.Test (isFoundryMode) import Echidna.Types.Campaign (CampaignConf(..), WorkerState(..)) import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..)) +import Echidna.Types.Test (TestConf(..)) import Echidna.Types.Solidity (SolConf(..)) import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..)) import Echidna.Worker (pushCampaignEvent) @@ -86,8 +87,10 @@ verifyMethodForProperty method contract vm = do logTarget target = liftIO $ pushCampaignEvent env (WorkerEvent wid SymbolicWorker (SymExecLog ("Verifying property: " <> methodSig <> " -> " <> Text.unpack target.methodSignature))) liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do + let dst = conf.solConf.contractAddr + propertySender = LitAddr (conf.testConf.testSender dst) threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do - (res, partials) <- exploreMethodTwoPhase checkPropertyReturn logTarget method propertyMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + (res, partials) <- exploreMethodTwoPhase checkPropertyReturn propertySender logTarget method propertyMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session liftIO $ putMVar resultChan (res, partials) liftIO $ putMVar doneChan () liftIO $ putMVar threadIdChan threadId @@ -127,7 +130,7 @@ verifyMethodForAssertion assertionMethods method contract vm = do liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do - (res, partials) <- exploreMethodTwoPhase (checkAssertions [0x1] isFoundry) logTarget method assertionMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session + (res, partials) <- exploreMethodTwoPhase (checkAssertions [0x1] isFoundry) (SymAddr "caller") logTarget method assertionMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session liftIO $ putMVar resultChan (res, partials) liftIO $ putMVar doneChan () liftIO $ putMVar threadIdChan threadId From 6cff3044ae1edffff2aaa502367380182e2416e4 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 19:30:20 +0100 Subject: [PATCH 12/14] fix --- lib/Echidna/SymExec/Exploration.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index 70d155499..191741340 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -21,7 +21,7 @@ import EVM.Fetch (RpcInfo(..)) import EVM.Solidity (SolcContract(..), Method(..)) import EVM.Solvers (defMemLimit, withSolvers) import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..), Postcondition) -import EVM.Types (Addr, VMType(..), EType(..), Expr(..)) +import EVM.Types (VMType(..), EType(..), Expr(..)) import qualified EVM.Types (VM(..)) import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, exploreMethodTwoPhase, checkAssertions, rpcFetcher, TxOrError(..), PartialsLogs) From 006a10b3ebd9d2ce98a00da65dca73789a33fe8a Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 20:23:21 +0100 Subject: [PATCH 13/14] fix --- lib/Echidna/SymExec/Common.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs index 0f56de485..758f2795f 100644 --- a/lib/Echidna/SymExec/Common.hs +++ b/lib/Echidna/SymExec/Common.hs @@ -83,7 +83,8 @@ extractErrors = mapMaybe (\case _ -> Nothing) suitableForSymExec :: Method -> Bool -suitableForSymExec m = not $ null m.inputs +suitableForSymExec m = + not (null m.inputs) && null (filter (\(_, t) -> abiKind t == Dynamic) m.inputs) && not (T.isInfixOf "_no_symexec" m.name) From 358ba8ba3899eb0283d58109d96eac7d6088c452 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 14 Mar 2026 21:37:49 +0100 Subject: [PATCH 14/14] sample properties in exploration mode --- lib/Echidna/Campaign.hs | 40 ++++++++++++++-------- lib/Echidna/Config.hs | 1 + lib/Echidna/Types/Campaign.hs | 6 ++++ tests/solidity/symbolic/motiv-explore.yaml | 4 +-- 4 files changed, 35 insertions(+), 16 deletions(-) diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs index 5ad61fa7b..c98c74cf8 100644 --- a/lib/Echidna/Campaign.hs +++ b/lib/Echidna/Campaign.hs @@ -5,7 +5,7 @@ module Echidna.Campaign where import Control.Concurrent import Control.DeepSeq (force) -import Control.Monad (replicateM, when, unless, void, forM_) +import Control.Monad (replicateM, replicateM_, when, unless, void, forM_) import Control.Monad.Catch (MonadThrow(..)) import Control.Monad.Random.Strict (MonadRandom, RandT, evalRandT) import Control.Monad.Reader (MonadReader, asks, liftIO, ask) @@ -118,7 +118,7 @@ runSymWorker -- ^ Initial corpus of transactions -> Maybe Text -- ^ Specified contract name -> m (WorkerStopReason, WorkerState) -runSymWorker callback vm dict workerId _ name = do +runSymWorker callback vm dict workerId initialCorpus name = do cfg <- asks (.cfg) let nworkers = getNFuzzWorkers cfg.campaignConf -- getNFuzzWorkers, NOT getNWorkers eventQueue <- asks (.eventQueue) @@ -130,6 +130,15 @@ runSymWorker callback vm dict workerId _ name = do verifyMethods -- No arguments, everything is in this environment pure SymbolicVerificationDone else do + -- Run two-phase on initial corpus before listening for events + unless (null initialCorpus) $ do + pushWorkerEvent $ SymExecLog ("Two-phase on initial corpus (" <> show (length initialCorpus) <> " entries)") + forM_ initialCorpus $ \(_, txs) -> unless (null txs) $ + replicateM_ cfg.campaignConf.symExecSeqSamples $ do + i <- rElem $ NEList.fromList [0 .. length txs] + let prefix = take i txs + vm' <- foldlM (\v tx -> snd <$> execTx v tx) vm prefix + symexecTx (Nothing, vm', prefix) lift callback listenerLoop listenerFunc chan nworkers pure SymbolicExplorationDone @@ -201,7 +210,8 @@ runSymWorker callback vm dict workerId _ name = do pure Nothing shrinkLoop (n - 1) - symexecTxs onlyRandom txs = mapM_ symexecTx =<< txsToTxAndVmsSym onlyRandom txs + symexecTxs onlyRandom txs = + mapM_ symexecTx =<< txsToTxAndVmsSym onlyRandom txs -- | Turn a list of transactions into inputs for symexecTx: -- (list of txns we're on top of) @@ -250,26 +260,28 @@ runSymWorker callback vm dict workerId _ name = do Just t -> getTargetMethodFromTx t contract failedTestSignatures >>= \case Nothing -> pure () Just method -> exploreAndVerify contract method vm' txsBase - -- Two-phase exploration: any state-changing method → no-arg targets - -- Filter to only targets that have registered open tests + -- Two-phase exploration for no-arg targets testRefs <- asks (.testRefs) tests <- liftIO $ traverse readIORef testRefs - let stateChanging = filter suitableForSymExec $ Map.elems contract.abiMap + let nSamples = conf.campaignConf.symExecSeqSamples + stateChanging = filter suitableForSymExec $ Map.elems contract.abiMap noArgTargets | isPropertyMode conf.solConf.testMode = - -- Property mode: only echidna_ functions that have open property tests let propNames = [n | t <- tests, isOpen t, isPropertyTest t, PropertyTest n _ <- [t.testType]] in filter (\m -> null m.inputs && m.name `elem` propNames) $ Map.elems contract.abiMap | otherwise = - -- Assertion mode: only no-arg functions that have open assertion tests let assertSigs = [getAssertionSignature t | t <- tests, isOpen t, isAssertionTest t] in filter (\m -> isNoArgAssertionTarget m && unpack m.methodSignature `elem` assertSigs) $ Map.elems contract.abiMap - unless (null noArgTargets || null stateChanging) $ do - method <- liftIO $ rElem (NEList.fromList stateChanging) - let baseLabel = txsBaseLabel txsBase - if isPropertyMode conf.solConf.testMode - then exploreAndVerifyTwoPhaseProperty contract method noArgTargets vm' txsBase baseLabel - else exploreAndVerifyTwoPhase contract method noArgTargets vm' txsBase baseLabel + unless (null noArgTargets || null stateChanging) $ + replicateM_ nSamples $ do + method <- liftIO $ rElem (NEList.fromList stateChanging) + -- Sample ~20% of targets per iteration to avoid being too slow + let nTargetSamples = max 1 (length noArgTargets `div` 5) + sampledTargets <- List.nub <$> replicateM nTargetSamples (liftIO $ rElem (NEList.fromList noArgTargets)) + let baseLabel = txsBaseLabel txsBase + if isPropertyMode conf.solConf.testMode + then exploreAndVerifyTwoPhaseProperty contract method sampledTargets vm' txsBase baseLabel + else exploreAndVerifyTwoPhase contract method sampledTargets vm' txsBase baseLabel exploreAndVerify contract method vm' txsBase = do -- Single-phase exploration (existing) diff --git a/lib/Echidna/Config.hs b/lib/Echidna/Config.hs index fcb1978ca..5578ab36b 100644 --- a/lib/Echidna/Config.hs +++ b/lib/Echidna/Config.hs @@ -111,6 +111,7 @@ instance FromJSON EConfigWithUsage where <*> v ..:? "symExecMaxIters" ..!= defaultSymExecMaxIters <*> v ..:? "symExecAskSMTIters" ..!= defaultSymExecAskSMTIters <*> v ..:? "symExecMaxExplore" ..!= defaultSymExecMaxExplore + <*> v ..:? "symExecSeqSamples" ..!= defaultSymExecSeqSamples where smtSolver = v ..:? "symExecSMTSolver" >>= \case Just ("z3" :: String) -> pure Z3 diff --git a/lib/Echidna/Types/Campaign.hs b/lib/Echidna/Types/Campaign.hs index 77dce6564..372eca198 100644 --- a/lib/Echidna/Types/Campaign.hs +++ b/lib/Echidna/Types/Campaign.hs @@ -67,6 +67,9 @@ data CampaignConf = CampaignConf , symExecMaxExplore :: Integer -- ^ Maximum number of states to explore before we stop exploring it. -- Only relevant if symExec is True + , symExecSeqSamples :: Int + -- ^ Number of random (method, split) samples for two-phase exploration + -- per coverage event. Only relevant if symExec is True } -- | The state of a fuzzing campaign. @@ -117,6 +120,9 @@ defaultSymExecNWorkers = 1 defaultSymExecMaxExplore :: Integer defaultSymExecMaxExplore = 10 +defaultSymExecSeqSamples :: Int +defaultSymExecSeqSamples = 3 + defaultSymExecMaxIters :: Integer defaultSymExecMaxIters = 5 diff --git a/tests/solidity/symbolic/motiv-explore.yaml b/tests/solidity/symbolic/motiv-explore.yaml index 2f8678d5f..85a162625 100644 --- a/tests/solidity/symbolic/motiv-explore.yaml +++ b/tests/solidity/symbolic/motiv-explore.yaml @@ -1,6 +1,6 @@ testMode: assertion symExec: true symExecSMTSolver: z3 +symExecSeqSamples: 10 workers: 2 -testLimit: 50000 -seed: 1 +testLimit: 100000