From a2b359efe9786144f969b776549a28be30f4f07e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emilio=20L=C3=B3pez?= Date: Fri, 14 Aug 2026 17:38:28 -0300 Subject: [PATCH 1/2] feat: replay a concrete sequence and report on it Add ExecuteSequence, the command that answers "what does this sequence of calls actually do?". A caller hands a worker a concrete sequence and gets back a JSON report: what each call was, whether it completed, reverted or failed an assertion, the gas it burned and the events it emitted, then the block number and timestamp the sequence ended on and, if asked for, the EVM trace. The replay goes through execTx rather than callseq, so the campaign is left exactly as it was: no coverage recorded, nothing added to the corpus, no test falsified. Answering a question about the contract must not change what the campaign does next, and a test pins that down. The report summarises the sequence by its worst transaction rather than its first failure. An assertion failure anywhere outranks a revert, even one that happened earlier -- reverts are common enough in a random sequence that reporting one would bury the thing the caller was looking for. Assertion failures are recognised with checkAssertionEvent and checkPanicEvent, the same pair an assertion test uses, so both the emit-AssertionFailed convention and solc's Panic(1) are covered; the tests exercise one path each. The command is addressed to a single worker, which answers through a one-shot Reply channel. The replay runs on that worker's own thread, so it stops fuzzing for as long as the caller is waiting on it. Nothing sends this command yet; the MCP server that does arrives next. Co-authored-by: gustavo-grieco --- lib/Echidna/Types/InterWorker.hs | 16 +++- lib/Echidna/Worker/Command.hs | 45 ++++++--- lib/Echidna/Worker/Fuzz.hs | 2 +- lib/Echidna/Worker/Replay.hs | 126 ++++++++++++++++++++++++ src/test/Spec.hs | 2 + src/test/Tests/Replay.hs | 160 +++++++++++++++++++++++++++++++ 6 files changed, 337 insertions(+), 14 deletions(-) create mode 100644 lib/Echidna/Worker/Replay.hs create mode 100644 src/test/Tests/Replay.hs diff --git a/lib/Echidna/Types/InterWorker.hs b/lib/Echidna/Types/InterWorker.hs index a5a164823..0a0a28998 100644 --- a/lib/Echidna/Types/InterWorker.hs +++ b/lib/Echidna/Types/InterWorker.hs @@ -10,10 +10,11 @@ module Echidna.Types.InterWorker , Bus , FuzzerCmd(..) , Message(..) + , Reply(..) , WrappedMessage(..) ) where -import Control.Concurrent.STM (TChan) +import Control.Concurrent.STM (TChan, TMVar) import Data.Text (Text) import Echidna.Types.Signature (SolCallPrototype) @@ -24,6 +25,14 @@ import Echidna.Types.Worker (WorkerId) data AgentId = FuzzerId WorkerId | SymbolicId deriving (Show, Eq, Ord) +-- | The channel a command answers on, filled exactly once by whoever handles +-- the command. Shown opaquely, so that carrying one does not cost a command +-- its derived 'Show'. +newtype Reply a = Reply (TMVar a) + +instance Show (Reply a) where + show _ = "" + -- | A command addressed to a single fuzzing worker. data FuzzerCmd = EnableSampling Text @@ -36,6 +45,11 @@ data FuzzerCmd -- probability in place of a corpus-mutated one. | ClearPrioritization -- ^ Forget every prioritized sequence. + | ExecuteSequence [Tx] Bool (Reply Text) + -- ^ Replay a sequence of transactions and report on what it did, without + -- perturbing the campaign. The flag asks for the EVM trace to be part of + -- the report; the reply is the JSON report itself. See + -- 'Echidna.Worker.Replay.executeSeq'. deriving Show -- | A message every agent gets to see. diff --git a/lib/Echidna/Worker/Command.hs b/lib/Echidna/Worker/Command.hs index f52be8d28..89820aa0b 100644 --- a/lib/Echidna/Worker/Command.hs +++ b/lib/Echidna/Worker/Command.hs @@ -1,12 +1,19 @@ -- | Commands a fuzzing worker accepts over the inter-worker bus. module Echidna.Worker.Command (checkMessages) where -import Control.Concurrent.STM (TChan, atomically, tryReadTChan) +import Control.Concurrent.STM (TChan, atomically, putTMVar, tryReadTChan) +import Control.Monad.Catch (MonadThrow) +import Control.Monad.Reader (MonadReader) import Control.Monad.State.Strict (MonadIO, MonadState, gets, liftIO, modify') import Data.Map qualified as Map +import EVM.Types (VM, VMType(Concrete)) + import Echidna.Types.Campaign -import Echidna.Types.InterWorker (FuzzerCmd(..), Message(..), WrappedMessage(..)) +import Echidna.Types.Config (Env) +import Echidna.Types.InterWorker + (FuzzerCmd(..), Message(..), Reply(..), WrappedMessage(..)) +import Echidna.Worker.Replay (executeSeq) -- | Run every command addressed to this worker that is currently waiting on -- the bus, then return. @@ -16,22 +23,29 @@ import Echidna.Types.InterWorker (FuzzerCmd(..), Message(..), WrappedMessage(..) -- behind would let a worker's view of the bus grow without bound while a burst -- of coverage is being found. Commands only ever originate outside the -- campaign, at the pace of whoever is driving it, so draining cannot starve --- fuzzing. +-- fuzzing -- though a command that runs transactions of its own does hold this +-- worker up while it does. checkMessages - :: (MonadIO m, MonadState WorkerState m) - => TChan WrappedMessage + :: (MonadIO m, MonadThrow m, MonadReader Env m, MonadState WorkerState m) + => VM Concrete + -- ^ The worker's initial VM, for commands that run transactions of their own + -> TChan WrappedMessage -> m () -checkMessages chan = do +checkMessages vm chan = do workerId <- gets (.workerId) let loop = liftIO (atomically (tryReadTChan chan)) >>= \case Nothing -> pure () Just (WrappedMessage _ (ToFuzzer tid cmd)) | tid == workerId -> - handleCmd cmd >> loop + handleCmd vm cmd >> loop Just _ -> loop loop -handleCmd :: MonadState WorkerState m => FuzzerCmd -> m () -handleCmd (EnableSampling sig) = +handleCmd + :: (MonadIO m, MonadThrow m, MonadReader Env m, MonadState WorkerState m) + => VM Concrete + -> FuzzerCmd + -> m () +handleCmd _ (EnableSampling sig) = modify' $ \workerState -> if Map.size workerState.sampledFunctions >= maxSampledFunctions || Map.member sig workerState.sampledFunctions @@ -41,13 +55,20 @@ handleCmd (EnableSampling sig) = Map.insert sig emptySampleStats workerState.sampledFunctions } -handleCmd ClearSampling = +handleCmd _ ClearSampling = modify' $ \workerState -> workerState { sampledFunctions = Map.empty } -handleCmd (FuzzSequence prototypes prob) = +handleCmd _ (FuzzSequence prototypes prob) = modify' $ \workerState -> workerState { prioritizedSequences = (prob, prototypes) : workerState.prioritizedSequences } -handleCmd ClearPrioritization = +handleCmd _ ClearPrioritization = modify' $ \workerState -> workerState { prioritizedSequences = [] } + +-- The command is addressed to a single worker, so this replies exactly once and +-- 'putTMVar' cannot block. The replay runs on the worker's own thread: the +-- caller waits for it, and this worker stops fuzzing until it is done. +handleCmd vm (ExecuteSequence txs includeTrace (Reply replyVar)) = do + report <- executeSeq includeTrace vm txs + liftIO $ atomically $ putTMVar replyVar report diff --git a/lib/Echidna/Worker/Fuzz.hs b/lib/Echidna/Worker/Fuzz.hs index 636b3f697..0ba19e87c 100644 --- a/lib/Echidna/Worker/Fuzz.hs +++ b/lib/Echidna/Worker/Fuzz.hs @@ -67,7 +67,7 @@ runFuzzWorker callback vm dict workerId initialCorpus testLimit = do where run chan = do - checkMessages chan + checkMessages vm chan testRefs <- asks (.testRefs) tests <- liftIO $ traverse readIORef testRefs CampaignConf{stopOnFail, shrinkLimit} <- asks (.cfg.campaignConf) diff --git a/lib/Echidna/Worker/Replay.hs b/lib/Echidna/Worker/Replay.hs new file mode 100644 index 000000000..f6fdfd0b7 --- /dev/null +++ b/lib/Echidna/Worker/Replay.hs @@ -0,0 +1,126 @@ +-- | Replaying a concrete transaction sequence to report on it, rather than to +-- fuzz with it. +module Echidna.Worker.Replay (executeSeq) where + +import Control.Applicative ((<|>)) +import Control.Monad.Catch (MonadThrow) +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.Reader (MonadReader, asks) +import Data.Aeson (ToJSON(..), object, (.=)) +import Data.Aeson.Text (encodeToLazyText) +import Data.List qualified as List +import Data.String.AnsiEscapeCodes.Strip.Text (stripAnsiEscapeCodes) +import Data.Text (Text) +import Data.Text.Lazy qualified as LT +import Data.Word (Word64) + +import EVM.Format (showTraceTree) +import EVM.Types (Block(..), VM(..), VMType(Concrete), forceLit) + +import Echidna.Events (Events, extractEvents) +import Echidna.Exec (execTx) +import Echidna.Test (checkAssertionEvent, checkPanicEvent) +import Echidna.Types.Config (Env(..)) +import Echidna.Types.Tx (Tx, TxResult(..), getResult) +import Echidna.UI.Report (ppTx) + +-- | How a single transaction of the sequence ended. Assertion failures are +-- kept apart from ordinary reverts because they mean different things: a +-- revert is usually just an input the contract rejected, an assertion failure +-- is the contract contradicting itself. +data TxStatus = Completed | Reverted | AssertionFailed + deriving Eq + +instance ToJSON TxStatus where + toJSON Completed = "completed" + toJSON Reverted = "reverted" + toJSON AssertionFailed = "assertion_failed" + +-- | What replaying one transaction produced. +data TxOutcome = TxOutcome + { index :: Int -- ^ Position in the sequence, counting from one + , call :: String + , status :: TxStatus + , result :: TxResult + , gasUsed :: Word64 + , logs :: Events + } + +instance ToJSON TxOutcome where + toJSON outcome = object + [ "index" .= outcome.index + , "call" .= outcome.call + , "status" .= outcome.status + , "result" .= outcome.result + , "gas_used" .= outcome.gasUsed + , "logs" .= outcome.logs + ] + +-- | Replay a concrete sequence of transactions and describe what happened as a +-- JSON report. +-- +-- The transactions run through 'execTx', which leaves the campaign alone: no +-- coverage is recorded, nothing reaches the corpus, and no test is falsified. +-- The point is to answer a question about the contract without changing what +-- the campaign does next. +executeSeq + :: (MonadIO m, MonadReader Env m, MonadThrow m) + => Bool -- ^ Whether to include the EVM trace of the replay + -> VM Concrete -- ^ VM to replay from + -> [Tx] + -> m Text +executeSeq includeTrace vm0 txs = do + dapp <- asks (.dapp) + (outcomes, finalVm) <- go dapp vm0 (zip [1..] txs) + let + -- Summarise the sequence by its worst transaction. An assertion failure + -- anywhere is what the caller is looking for, so it outranks a revert even + -- when something reverted earlier; reverts are common enough in a random + -- sequence that reporting one would bury it. + notable = + List.find ((== AssertionFailed) . (.status)) outcomes + <|> List.find ((/= Completed) . (.status)) outcomes + traceFields + -- Traces are cleared before each transaction unless `allEvents` is set, + -- so this is the trace of the last transaction alone in the usual case. + -- 'showTraceTree' colours its output; whoever reads the report is not a + -- terminal, so the escape codes are only tokens wasted. + | includeTrace && not (null txs) = + ["trace" .= stripAnsiEscapeCodes (showTraceTree dapp finalVm)] + | otherwise = [] + pure $ LT.toStrict $ encodeToLazyText $ object $ + [ "status" .= maybe Completed (.status) notable + , "transaction_count" .= length txs + , "failed_tx_index" .= ((.index) <$> notable) + , "final_block_number" .= show (forceLit finalVm.block.number) + , "final_timestamp" .= show (forceLit finalVm.block.timestamp) + , "transactions" .= outcomes + ] ++ traceFields + + where + -- Recursing rather than folding keeps the report in execution order, and + -- hands back the final VM for the summary. + go _ vm [] = pure ([], vm) + go dapp vm ((index, tx):rest) = do + (vmResult, vm') <- execTx vm tx + call <- ppTx vm' False tx + let + result = getResult vmResult + logs = extractEvents True dapp vm' + outcome = TxOutcome { index + , call + , status = txStatus result logs + , result + , gasUsed = fromIntegral (vm'.burned - vm.burned) + , logs + } + (outcomes, finalVm) <- go dapp vm' rest + pure (outcome : outcomes, finalVm) + +-- | Classify how a transaction ended, detecting assertion failures the same +-- way an assertion test does. +txStatus :: TxResult -> Events -> TxStatus +txStatus result logs + | checkAssertionEvent logs || checkPanicEvent "1" logs = AssertionFailed + | result `elem` [ReturnTrue, ReturnFalse, Stop] = Completed + | otherwise = Reverted diff --git a/src/test/Spec.hs b/src/test/Spec.hs index bab031579..f388c088e 100644 --- a/src/test/Spec.hs +++ b/src/test/Spec.hs @@ -12,6 +12,7 @@ import Tests.FoundryTestGen (foundryTestGenTests) import Tests.Integration (integrationTests) import Tests.Optimization (optimizationTests) import Tests.Overflow (overflowTests) +import Tests.Replay (replayTests) import Tests.Research (researchTests) import Tests.Sample (sampleTests) import Tests.Seed (seedTests) @@ -35,6 +36,7 @@ main = withCurrentDirectory "./tests/solidity" . defaultMain $ , foundryTests , encodingJSONTests , sampleTests + , replayTests , foundryTestGenTests , cheatTests , symbolicTests diff --git a/src/test/Tests/Replay.hs b/src/test/Tests/Replay.hs new file mode 100644 index 000000000..87566d648 --- /dev/null +++ b/src/test/Tests/Replay.hs @@ -0,0 +1,160 @@ +module Tests.Replay (replayTests) where + +import Control.Monad.Reader (runReaderT) +import Data.Aeson (FromJSON(..), eitherDecodeStrict, withObject, (.:), (.:?)) +import Data.IORef (readIORef) +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Maybe (fromMaybe, isJust) +import Data.Set qualified as Set +import Data.Text (Text) +import Data.Text qualified as T +import Data.Text.Encoding (encodeUtf8) +import Data.Word (Word64) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (assertBool, assertFailure, testCase, (@?=)) + +import EVM.ABI (AbiValue(..)) +import EVM.Types (VM, VMType(Concrete)) + +import Echidna.Solidity (compileContracts) +import Echidna.Types.Config (EConfig(..), Env(..)) +import Echidna.Types.Corpus (corpusSize) +import Echidna.Types.Coverage (coverageStats) +import Echidna.Types.Solidity (SolConf(..)) +import Echidna.Types.Tx (Tx, TxConf(..), basicTx) +import Echidna.Worker.Replay (executeSeq) + +import Common (loadSolTests, solcV, testConfig, withSolcVersion) + +-- | The parts of the report the assertions below look at. +data Report = Report + { status :: Text + , transactionCount :: Int + , failedTxIndex :: Maybe Int + , transactions :: [TxReport] + , trace :: Maybe Text + } + +instance FromJSON Report where + parseJSON = withObject "report" $ \o -> Report + <$> o .: "status" + <*> o .: "transaction_count" + <*> o .: "failed_tx_index" + <*> o .: "transactions" + <*> o .:? "trace" + +data TxReport = TxReport + { index :: Int + , call :: Text + , status :: Text + , result :: Text + , gasUsed :: Word64 + , logs :: [Text] + } + +instance FromJSON TxReport where + parseJSON = withObject "transaction" $ \o -> TxReport + <$> o .: "index" + <*> o .: "call" + <*> o .: "status" + <*> o .: "result" + <*> o .: "gas_used" + <*> o .: "logs" + +replayTests :: TestTree +replayTests = testGroup "Sequence replay" + [ testCase "reports every transaction of the sequence" $ do + (vm, env, txs) <- loadReverting + report <- replay env False vm txs + + report.status @?= "assertion_failed" + report.transactionCount @?= 3 + map (.index) report.transactions @?= [1, 2, 3] + map (.status) report.transactions + @?= ["completed", "reverted", "assertion_failed"] + map (.result) report.transactions + @?= ["Stop", "ErrorRevert", "ErrorRevert"] + assertBool "every transaction reports the gas it burned" $ + all ((> 0) . (.gasUsed)) report.transactions + assertBool "the call is spelled out" $ + all (T.isInfixOf "assert" . (.call)) report.transactions + assertBool "the assertion failure shows up in the logs" $ + any (T.isInfixOf "AssertionFailed") (last report.transactions).logs + + -- An assertion failure is what the caller is after, so it is reported + -- even though the sequence reverted earlier. + report.failedTxIndex @?= Just 3 + + , testCase "counts a failed solidity assert as an assertion failure" $ + withSolcVersion (Just (>= solcV (0,8,0))) $ do + (vm, env, call) <- load "assert/assert-0.8.sol" + report <- replay env False vm [call "direct_assert" [AbiInt 256 100]] + report.status @?= "assertion_failed" + assertBool "the panic is spelled out" $ + any (T.isInfixOf "Panic(1)") (head report.transactions).logs + + , testCase "leaves the campaign's coverage and corpus alone" $ do + (vm, env, txs) <- loadReverting + coverageBefore <- coverageStats env.coverageRefInit env.coverageRefRuntime + corpusBefore <- corpusSize <$> readIORef env.corpusRef + + _ <- replay env False vm txs + + coverageAfter <- coverageStats env.coverageRefInit env.coverageRefRuntime + corpusAfter <- corpusSize <$> readIORef env.corpusRef + coverageAfter @?= coverageBefore + corpusAfter @?= corpusBefore + + , testCase "includes the EVM trace only when asked" $ do + (vm, env, txs) <- loadReverting + without <- replay env False vm txs + with <- replay env True vm txs + without.trace @?= Nothing + assertBool "asking for the trace produces one" (isJust with.trace) + assertBool "the trace is not coloured" $ + not (T.isInfixOf "\ESC[" (fromMaybe "" with.trace)) + + , testCase "reports an empty sequence as completed" $ do + (vm, env, _) <- loadReverting + report <- replay env True vm [] + report.status @?= "completed" + report.transactionCount @?= 0 + report.failedTxIndex @?= Nothing + assertBool "nothing to report on" (null report.transactions) + -- Nothing ran, so there is no trace to show even though one was asked for. + report.trace @?= Nothing + ] + where + -- Compile a fixture and return a way to call functions on it. These fixtures + -- report failures with events or panics rather than with echidna_ properties, + -- so they need assertion mode to have any tests at all. + load :: FilePath -> IO (VM Concrete, Env, Text -> [AbiValue] -> Tx) + load fixture = do + let cfg = testConfig + { solConf = testConfig.solConf { testMode = "assertion" } } + buildOutput <- compileContracts cfg.solConf (fixture :| []) + (vm, env, _) <- loadSolTests cfg buildOutput Nothing + let solConf = env.cfg.solConf + pure ( vm + , env + , \name args -> + basicTx name args (Set.elemAt 0 solConf.sender) solConf.contractAddr + env.cfg.txConf.txGas (0, 0) + ) + + -- A sequence that completes, reverts, and fails an assertion, in that order. + loadReverting :: IO (VM Concrete, Env, [Tx]) + loadReverting = do + (vm, env, call) <- load "assert/revert.sol" + pure ( vm + , env + , [ call "assert_revert" [AbiUInt 256 1] + , call "assert_unreachable" [] + , call "assert_revert" [AbiUInt 256 200] + ] + ) + + replay :: Env -> Bool -> VM Concrete -> [Tx] -> IO Report + replay env includeTrace vm txs = do + json <- runReaderT (executeSeq includeTrace vm txs) env + either assertFailure pure $ eitherDecodeStrict (encodeUtf8 json) From dfd9d65230f480c53a027b1346c2168d67a96006 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emilio=20L=C3=B3pez?= Date: Fri, 14 Aug 2026 19:25:34 -0300 Subject: [PATCH 2/2] fix: drop a partial head from the replay tests GHC 9.8 turned head into a -Wall warning, and CI builds the test suite with -Werror, so the single-transaction assertion in the Panic(1) test failed the Windows and Linux builds. Match on the list instead. The test replays exactly one transaction, so pinning that down says what the assertion already assumed and reports a useful failure if it ever stops holding. --- src/test/Tests/Replay.hs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/test/Tests/Replay.hs b/src/test/Tests/Replay.hs index 87566d648..2db98bedd 100644 --- a/src/test/Tests/Replay.hs +++ b/src/test/Tests/Replay.hs @@ -90,8 +90,11 @@ replayTests = testGroup "Sequence replay" (vm, env, call) <- load "assert/assert-0.8.sol" report <- replay env False vm [call "direct_assert" [AbiInt 256 100]] report.status @?= "assertion_failed" - assertBool "the panic is spelled out" $ - any (T.isInfixOf "Panic(1)") (head report.transactions).logs + case report.transactions of + [tx] -> assertBool "the panic is spelled out" $ + any (T.isInfixOf "Panic(1)") tx.logs + txs -> assertFailure $ + "expected one transaction, got " <> show (length txs) , testCase "leaves the campaign's coverage and corpus alone" $ do (vm, env, txs) <- loadReverting