diff --git a/flake.nix b/flake.nix index c227e9320..6880ceb49 100644 --- a/flake.nix +++ b/flake.nix @@ -69,8 +69,15 @@ pkgs.haskell.lib.compose.dontCheck ]); + mcp-server = pkgs: pkgs.haskellPackages.callCabal2nix "mcp-server" (pkgs.fetchFromGitHub { + owner = "gustavo-grieco"; + repo = "haskell-mcp-server"; + rev = "9fd60af428b96ae4bc63a133b3960ed934494189"; + sha256 = "sha256-lh65Gy8a43xbDDFPONOJ2UBUS1xWOW2UUx3wYFTG8Xg="; + }) {}; + echidna = pkgs: with pkgs; lib.pipe - (haskellPackages.callCabal2nix "echidna" ./. { hevm = hevm pkgs; }) + (haskellPackages.callCabal2nix "echidna" ./. { hevm = hevm pkgs; mcp-server = mcp-server pkgs; }) ([ # FIXME: figure out solc situation, it conflicts with the one from # solc-select that is installed with slither, disable tests in the meantime diff --git a/lib/Echidna.hs b/lib/Echidna.hs index d77eac4e6..f4265914c 100644 --- a/lib/Echidna.hs +++ b/lib/Echidna.hs @@ -1,6 +1,7 @@ module Echidna where import Control.Concurrent (newChan) +import Control.Concurrent.STM (newBroadcastTChanIO) import Control.Monad.Catch (MonadThrow(..)) import Control.Monad.IO.Class (liftIO) import Data.IORef (newIORef) @@ -86,7 +87,7 @@ prepareContract cfg solFiles buildOutput selectedContract seed = do <> staticAddresses solConf <> deployedAddresses deployedSolcContracts = nub $ mapMaybe (findSrcForReal env.dapp) $ Map.elems vm.env.contracts - nonViewPureSigs = concatMap (mapMaybe (\ (Method {name, inputs, mutability}) -> + nonViewPureSigs = concatMap (mapMaybe (\ (Method {name, inputs, mutability}) -> case mutability of View -> Nothing Pure -> Nothing @@ -123,6 +124,7 @@ mkEnv cfg buildOutput tests world slitherInfo = do codehashMap <- newIORef mempty chainId <- Onchain.fetchChainIdFrom cfg.rpcUrl eventQueue <- newChan + bus <- newBroadcastTChanIO coverageRefInit <- newIORef mempty coverageRefRuntime <- newIORef mempty corpusRef <- newIORef mempty @@ -131,7 +133,8 @@ mkEnv cfg buildOutput tests world slitherInfo = do contractNameCache <- newIORef mempty -- TODO put in real path let dapp = dappInfo "/" buildOutput - pure $ Env { cfg, dapp, codehashMap, fetchSession, contractNameCache - , chainId, eventQueue, coverageRefInit, coverageRefRuntime, corpusRef, testRefs, world + sourceCache = buildOutput.sources + pure $ Env { cfg, dapp, sourceCache, codehashMap, fetchSession, contractNameCache + , chainId, eventQueue, bus, coverageRefInit, coverageRefRuntime, corpusRef, testRefs, world , slitherInfo } diff --git a/lib/Echidna/Agent/Fuzzer.hs b/lib/Echidna/Agent/Fuzzer.hs new file mode 100644 index 000000000..45d137d23 --- /dev/null +++ b/lib/Echidna/Agent/Fuzzer.hs @@ -0,0 +1,325 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE MultiWayIf #-} + +module Echidna.Agent.Fuzzer where + +import Control.Concurrent.STM (atomically, tryReadTChan, dupTChan, putTMVar) +import Control.Monad (replicateM, void, forM_, when) +import Control.Monad.Reader (runReaderT, liftIO, asks, MonadReader, ask) +import Control.Monad.State.Strict (runStateT, get, gets, modify', MonadState) +import Control.Monad.Random.Strict (evalRandT, MonadRandom, RandT, getRandom, getRandomR) +import Control.Monad.Catch (MonadThrow(..)) +import Control.Monad.Trans (lift) +import Control.Monad.IO.Class (MonadIO) +import System.Random (mkStdGen) +import Data.IORef (IORef, writeIORef, readIORef, atomicModifyIORef') +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Data.Set as Set +import Data.Text (Text) +import System.Directory (getCurrentDirectory) + +import Echidna.Output.Source (saveLcovHook) +import EVM.Dapp (DappInfo(..)) +import EVM.Types (VM(..), VMType(Concrete), Expr(..), EType(..), Contract) +import qualified EVM.Types as EVM + +import EVM.ABI (AbiValue) +import Echidna.ABI (GenDict(..)) +import Echidna.Execution (replayCorpus, callseq, updateTests) +import Echidna.Mutator.Corpus (getCorpusMutation, seqMutatorsStateless, seqMutatorsStateful, fromConsts) +import Echidna.Shrink (shrinkTest) +import Echidna.Transaction (genTx, genTxFromPrototype) +import Echidna.Types.Random (rElem) +import qualified Data.List.NonEmpty as NE +import Echidna.Types.Agent +import Echidna.Types.Campaign (WorkerState(..), CampaignConf(..)) +import Echidna.Types.Config (Env(..), EConfig(..)) +import Echidna.Types.InterWorker (AgentId(..), Bus, WrappedMessage(..), Message(..), FuzzerCmd(..)) +import Echidna.Types.Test (EchidnaTest(..), TestState(..), TestType(..), isOpen, isOptimizationTest) +import Echidna.Types.Tx (Tx) +import Echidna.Types.Worker (WorkerEvent(..), WorkerType(..), CampaignEvent(..), WorkerStopReason(..)) +import qualified Echidna.Types.Worker as Worker +import Echidna.Worker (pushCampaignEvent) + +instance (MonadThrow m) => MonadThrow (RandT g m) where + throwM = lift . throwM + +data FuzzerAgent = FuzzerAgent + { fuzzerId :: Int + , initialVm :: VM Concrete + , initialDict :: GenDict + , initialCorpus :: [(FilePath, [Tx])] + , testLimit :: Int + , stateRef :: IORef WorkerState + } + +instance Show FuzzerAgent where + show agent = "FuzzerAgent { fuzzerId = " ++ show agent.fuzzerId ++ " }" + +instance Agent FuzzerAgent where + getAgentId agent = FuzzerId agent.fuzzerId + + runAgent agent bus env = do + let workerId = agent.fuzzerId + vm = agent.initialVm + dict = agent.initialDict + corpus = agent.initialCorpus + limit = agent.testLimit + ref = agent.stateRef + + effectiveSeed = dict.defSeed + workerId + effectiveGenDict = dict { defSeed = effectiveSeed } + + initialState = WorkerState + { workerId + , genDict = effectiveGenDict + , newCoverage = False + , ncallseqs = 0 + , ncalls = 0 + , totalGas = 0 + , runningThreads = [] + , prioritizedSequences = [] + } + + -- Callback to update the IORef with the current state + let callback = get >>= liftIO . writeIORef ref + + (reason, _) <- flip evalRandT (mkStdGen effectiveSeed) $ + flip runReaderT env $ + flip runStateT initialState $ do + liftIO $ pushCampaignEvent env (WorkerEvent workerId FuzzWorker (Worker.Log ("Starting FuzzerAgent " ++ show workerId))) + callback + void $ replayCorpus vm corpus + workerChan <- liftIO $ atomically $ dupTChan bus + fuzzerLoop callback vm limit workerChan + + liftIO $ pushCampaignEvent env (WorkerEvent workerId FuzzWorker (WorkerStopped reason)) + + return () + +fuzzerLoop + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => m () -- ^ Callback + -> VM Concrete + -> Int -- ^ Test limit + -> Bus + -> m WorkerStopReason +fuzzerLoop callback vm testLimit bus = do + -- Check for messages + -- TODO: Properly handle messages. For now we just check if we should stop? + -- But runAgent doesn't return until done. + + -- We can peek the bus. But standard fuzzer might be busy. + -- Maybe check bus every N iterations? + + run + where + run = do + checkMessages + + testRefs <- asks (.testRefs) + tests <- liftIO $ traverse readIORef testRefs + CampaignConf{stopOnFail, shrinkLimit} <- asks (.cfg.campaignConf) + ncalls <- gets (.ncalls) + workerId <- gets (.workerId) + + let + shrinkable test = + case test.state of + -- we shrink only tests which were solved on this + -- worker + Large n | test.workerId == Just workerId -> + n < shrinkLimit + _ -> False + + final test = + case test.state of + Solved -> True + Failed _ -> True + _ -> False + + closeOptimizationTest test = + case test.testType of + OptimizationTest _ _ -> + test { state = Large 0 + , workerId = Just workerId + } + _ -> test + + if | stopOnFail && any final tests -> + callback >> pure FastFailed + + -- we shrink first before going back to fuzzing + | any shrinkable tests -> + shrink >> callback >> run + + -- no shrinking work, fuzz + | (null tests || any isOpen tests) && ncalls < testLimit -> + fuzz >> callback >> run + + -- NOTE: this is a hack which forces shrinking of optimization tests + -- after test limit is reached + | ncalls >= testLimit && any (\t -> isOpen t && isOptimizationTest t) tests -> do + liftIO $ forM_ testRefs $ \testRef -> + atomicModifyIORef' testRef (\test -> (closeOptimizationTest test, ())) + callback >> run + + -- no more work to do, means we reached the test limit, exit + | otherwise -> + callback >> pure TestLimitReached + + fuzz = randseq vm.env.contracts >>= fmap fst . (\txs -> callseq vm txs False) + + shrink = do + wid <- gets (.workerId) + updateTests $ \test -> do + if test.workerId == Just wid then + shrinkTest vm test + else + pure Nothing + + checkMessages = do + -- Non-blocking read + msg <- liftIO $ atomically $ tryReadTChan bus + case msg of + Just (WrappedMessage _ (ToFuzzer tid (SolutionFound _))) -> do + workerId <- gets (.workerId) + when (tid == workerId) $ do + -- Received help! + pure () + Just (WrappedMessage _ (ToFuzzer tid DumpLcov)) -> do + workerId <- gets (.workerId) + when (tid == workerId) $ do + env <- ask + liftIO $ do + let contracts = Map.elems env.dapp.solcByName + dir <- maybe getCurrentDirectory pure env.cfg.campaignConf.corpusDir + void $ saveLcovHook env dir env.sourceCache contracts + putStrLn $ "Fuzzer " ++ show workerId ++ ": dumped LCOV coverage." + pure () + Just (WrappedMessage _ (ToFuzzer tid (FuzzSequence txs prob))) -> do + workerId <- gets (.workerId) + when (tid == workerId) $ do + modify' $ \s -> s { prioritizedSequences = (prob, txs) : s.prioritizedSequences } + pure () + Just (WrappedMessage _ (ToFuzzer tid ClearPrioritization)) -> do + workerId <- gets (.workerId) + when (tid == workerId) $ do + modify' $ \s -> s { prioritizedSequences = [] } + pure () + Just (WrappedMessage _ (ToFuzzer tid (ExecuteSequence txs replyVar))) -> do + workerId <- gets (.workerId) + when (tid == workerId) $ do + (_, newCov) <- callseq vm txs False + liftIO $ case replyVar of + Just var -> atomically $ putTMVar var newCov + Nothing -> pure () + pure () + _ -> pure () + +-- | Generate a new sequences of transactions, either using the corpus or with +-- randomly created transactions +randseq + :: (MonadRandom m, MonadReader Env m, MonadState WorkerState m, MonadIO m) + => Map (Expr 'EAddr) Contract + -> m [Tx] +randseq deployedContracts = do + -- 1. Check for prioritized sequences injected via tools + prioritized <- gets (.prioritizedSequences) + + mbSeq <- if null prioritized + then pure Nothing + else do + -- Select a prioritized sequence based on probability + (prob, seqPrototype) <- rElem (NE.fromList prioritized) + useIt <- (<= prob) <$> getRandom + pure $ if useIt then Just seqPrototype else Nothing + + case mbSeq of + Just seqPrototype -> genPrioritizedSeq deployedContracts seqPrototype + Nothing -> genStandardSeq deployedContracts + +-- | Generate a sequence of transactions based on a prioritized prototype +genPrioritizedSeq + :: (MonadRandom m, MonadReader Env m, MonadState WorkerState m, MonadIO m) + => Map (Expr 'EAddr) Contract + -> [(Text, [Maybe AbiValue])] + -> m [Tx] +genPrioritizedSeq deployedContracts seqPrototype = do + env <- ask + let world = env.world + seqLen = env.cfg.campaignConf.seqLen + + -- 2. If a prioritized sequence is selected: + -- Expand the prototype into concrete transactions + let expandPrototype [] = return [] + expandPrototype [p] = do + tx <- genTxFromPrototype world deployedContracts p + return [tx] + expandPrototype (p:ps) = do + tx <- genTxFromPrototype world deployedContracts p + -- Insert random transactions between prototype transactions to increase fuzzing diversity + n <- getRandomR (0, 3) + rndTxs <- replicateM n (genTx world deployedContracts) + rest <- expandPrototype ps + return ((tx : rndTxs) ++ rest) + + expandedTxs <- expandPrototype seqPrototype + corpusSet <- liftIO $ readIORef env.corpusRef + wid <- gets (.workerId) + + -- Select a prefix from the existing corpus + -- Special handling for worker 0: always use empty prefix (position 0) + prefix <- if Set.null corpusSet || wid == 0 + then pure [] + else do + -- Pick a random sequence from corpus + idx <- getRandomR (0, Set.size corpusSet - 1) + let (_, cTxs) = Set.elemAt idx corpusSet + let middleLen = length expandedTxs + let maxPrefix = seqLen - middleLen + if maxPrefix <= 0 + then pure [] + else do + -- Take a random prefix length + k <- getRandomR (0, min (length cTxs) maxPrefix) + pure (take k cTxs) + + let combined = prefix ++ expandedTxs + let len = length combined + + -- Pad with random transactions if sequence is too short + if len < seqLen + then do + paddingTxs <- replicateM (seqLen - len) (genTx world deployedContracts) + pure (combined ++ paddingTxs) + else + pure (take seqLen combined) + +-- | Generate a sequence of transactions using standard fuzzing techniques +genStandardSeq + :: (MonadRandom m, MonadReader Env m, MonadState WorkerState m, MonadIO m) + => Map (Expr 'EAddr) Contract + -> m [Tx] +genStandardSeq deployedContracts = do + env <- ask + let world = env.world + mutConsts = env.cfg.campaignConf.mutConsts + seqLen = env.cfg.campaignConf.seqLen + + -- 3. Standard fuzzing behavior (no prioritized sequence selected) + -- Generate new random transactions + randTxs <- replicateM seqLen (genTx world deployedContracts) + -- Generate a random mutator + cmut <- if seqLen == 1 then seqMutatorsStateless (fromConsts mutConsts) + else seqMutatorsStateful (fromConsts mutConsts) + -- Fetch the mutator + let mut = getCorpusMutation cmut + corpus <- liftIO $ readIORef env.corpusRef + if null corpus + then pure randTxs -- Use the generated random transactions + else mut seqLen corpus randTxs -- Apply the mutator diff --git a/lib/Echidna/Agent/Symbolic.hs b/lib/Echidna/Agent/Symbolic.hs new file mode 100644 index 000000000..b62611d6b --- /dev/null +++ b/lib/Echidna/Agent/Symbolic.hs @@ -0,0 +1,444 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedRecordDot #-} + +module Echidna.Agent.Symbolic where + +import Control.Concurrent (takeMVar) +import Control.Concurrent.STM (atomically, readTChan, writeTChan, dupTChan, TChan) +import Control.Monad (when, void, unless, forM_) +import Control.Monad.Reader (runReaderT, liftIO, asks, MonadReader) +import Control.Monad.State.Strict (runStateT, get, gets, MonadState, modify') +import Control.Monad.Random.Strict (evalRandT, MonadRandom, RandT) +import Control.Monad.Catch (MonadThrow(..)) +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.Trans (lift) +import System.Random (mkStdGen) +import Data.IORef (IORef, writeIORef, readIORef) +import Data.Foldable (foldlM) +import Data.List.NonEmpty qualified as NEList +import Data.Map qualified as Map +import Data.Maybe (fromJust) +import Data.Text (Text, unpack) + +import EVM.Types (VM(..), VMType(Concrete)) +import EVM.Solidity (SolcContract(..), Method(..)) +import EVM.Dapp (DappInfo(..)) + +import Echidna.Types.Solidity (SolConf(..)) +import Echidna.ABI (GenDict(..)) +import qualified Echidna.Exec +import Echidna.Execution (callseq, updateTests) +import Echidna.Shrink (shrinkTest) +import Echidna.Solidity (chooseContract) +import Echidna.SymExec.Common (extractTxs, extractErrors) +import Echidna.SymExec.Exploration (exploreContract, getTargetMethodFromTx, getRandomTargetMethod) +import Echidna.SymExec.Verification (verifyMethod, isSuitableToVerifyMethod) +import Echidna.Types.Agent +import Echidna.Types.Campaign (WorkerState(..), CampaignConf(..), getNFuzzWorkers) +import Echidna.Types.Config (Env(..), EConfig(..)) +import Echidna.Types.InterWorker (AgentId(..), Bus, WrappedMessage(..), Message(..), SymbolicCmd(..), FuzzerCmd(..), BroadcastMsg(NewCoverageInfo)) +import qualified Echidna.Types.InterWorker as InterWorker +import Echidna.Types.Random (rElem) +import Echidna.Test (isVerificationMode) +import Echidna.Types.Test (EchidnaTest(..), TestState(..), isAssertionTest, getAssertionSignature, isOpen, didFail) +import qualified Echidna.Types.Test as Test +import Echidna.Types.Tx (Tx) +import Echidna.Types.Worker (WorkerEvent(..), WorkerType(..), CampaignEvent(..), WorkerStopReason(..)) +import Echidna.Worker (pushCampaignEvent, pushWorkerEvent) + +instance (MonadThrow m) => MonadThrow (RandT g m) where + throwM = lift . throwM + +data SymbolicAgent = SymbolicAgent + { initialVm :: VM Concrete + , initialDict :: GenDict + , initialCorpus :: [(FilePath, [Tx])] + , contractName :: Maybe Text + , stateRef :: IORef WorkerState + } + +instance Show SymbolicAgent where + show agent = "SymbolicAgent { contractName = " ++ show agent.contractName ++ " }" + +instance Agent SymbolicAgent where + getAgentId _ = SymbolicId + + runAgent agent bus env = do + let workerId = 0 -- Symbolic agent usually has ID 0 + vm = agent.initialVm + dict = agent.initialDict + name = agent.contractName + ref = agent.stateRef + + effectiveSeed = dict.defSeed + workerId + effectiveGenDict = dict { defSeed = effectiveSeed } + + initialState = WorkerState + { workerId + , genDict = effectiveGenDict + , newCoverage = False + , ncallseqs = 0 + , ncalls = 0 + , totalGas = 0 + , runningThreads = [] + , prioritizedSequences = [] + } + + let callback = get >>= liftIO . writeIORef ref + let cfg = env.cfg + let nworkers = getNFuzzWorkers cfg.campaignConf + + -- We create a specific channel for this agent to read from bus (broadcasts) + workerChan <- atomically $ dupTChan bus + + (reason, _) <- flip evalRandT (mkStdGen effectiveSeed) $ + flip runReaderT env $ + flip runStateT initialState $ do + liftIO $ pushCampaignEvent env (WorkerEvent workerId SymbolicWorker (Log ("Starting SymbolicAgent " ++ show workerId))) + + -- Check for stateless verification mode + if isVerificationMode cfg.solConf.testMode then do + verifyMethods vm name callback + pure SymbolicVerificationDone + else do + callback + busListenerLoop bus workerChan callback vm name nworkers + pure SymbolicExplorationDone + + liftIO $ pushCampaignEvent env (WorkerEvent workerId SymbolicWorker (WorkerStopped reason)) + + return () + +busListenerLoop + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => Bus + -> TChan WrappedMessage + -> m () + -> VM Concrete + -> Maybe Text + -> Int + -> m () +busListenerLoop bus chan callback vm name workersAlive = + when (workersAlive > 0) $ do + msg <- liftIO $ atomically $ readTChan chan + handleMessage bus msg callback vm name + case msg of + WrappedMessage _ (Broadcast (InterWorker.WorkerStopped _)) -> + busListenerLoop bus chan callback vm name (workersAlive - 1) + _ -> busListenerLoop bus chan callback vm name workersAlive + +handleMessage + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => Bus + -> WrappedMessage + -> m () + -> VM Concrete + -> Maybe Text + -> m () +handleMessage _ (WrappedMessage _ (Broadcast (NewCoverageInfo _ txs _))) callback vm name = do + void $ callseq vm txs False + symexecTxs callback vm False name txs + shrinkAndRandomlyExplore callback vm txs (10 :: Int) + +handleMessage bus (WrappedMessage from (ToSymbolic (SolveThis txs))) callback vm name = do + -- Received a request to solve constraints or generate inputs based on txs + -- We can use symexecTxs to try to explore around these txs + -- But we need to return the result to 'from' + + -- For now, let's try to run symbolic execution on these txs + -- and if we find new valid transactions, send them back. + + -- This is a simplified implementation. Real implementation would need to hook into the solver results. + -- symexecTxs pushes events and updates coverage. + + -- TODO: We need a way to capture the "Solution" from symexecTxs + -- Currently symexecTxs calls exploreAndVerify which calls exploreContract which pushes to symTxsChan. + -- We could refactor exploreAndVerify to return the found txs. + + symexecTxs callback vm False name txs + + -- If we found something, we should probably send it back. + -- But symexecTxs updates the global state/coverage directly. + -- Maybe we can send a "SolutionFound" with empty list just to ack? + -- Or we can assume that if new coverage is found, it is broadcasted, so the requester will see it. + + -- However, the requester asked for help. Maybe they want a specific transaction that solves a branch. + -- The PoC says "The symbolic worker should be able to answer with some solved constraints / generator". + + -- Let's just send a message saying we tried. + case from of + FuzzerId fid -> + liftIO $ atomically $ writeTChan bus (WrappedMessage SymbolicId (ToFuzzer fid (SolutionFound []))) + _ -> pure () + +handleMessage _ _ _ _ _ = pure () + +shrinkAndRandomlyExplore + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => m () + -> VM Concrete + -> [Tx] + -> Int + -> m () +shrinkAndRandomlyExplore callback vm _ 0 = do + testRefs <- asks (.testRefs) + tests <- liftIO $ traverse readIORef testRefs + CampaignConf{shrinkLimit} <- asks (.cfg.campaignConf) + when (any shrinkable tests) $ shrinkLoop callback vm shrinkLimit + where + shrinkable test = + case test.state of + Large _ -> True -- Symbolic worker can shrink any large test? Origin logic: test.workerId == Just workerId + _ -> False + +shrinkAndRandomlyExplore callback vm txs n = do + testRefs <- asks (.testRefs) + tests <- liftIO $ traverse readIORef testRefs + CampaignConf{stopOnFail, shrinkLimit} <- asks (.cfg.campaignConf) + if stopOnFail && any final tests then + callback -- >> pure FastFailed + else if any shrinkable tests then do + shrinkLoop callback vm shrinkLimit + shrinkAndRandomlyExplore callback vm txs n + else do + symexecTxs callback vm False Nothing txs + shrinkAndRandomlyExplore callback vm txs (n - 1) + where + shrinkable test = + case test.state of + Large _ -> True -- Simplified + _ -> False + final test = + case test.state of + Solved -> True + Failed _ -> True + _ -> False + +shrinkLoop + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => m () + -> VM Concrete + -> Int + -> m () +shrinkLoop _ _ 0 = return () +shrinkLoop callback vm n = do + callback + workerId <- gets (.workerId) + updateTests $ \test -> do + -- Logic from Campaign.hs: test.workerId == Just workerId + -- But symbolic worker has workerId=0. Maybe it shares work? + -- For now, allow shrinking if we own it or if it's unassigned? + if test.workerId == Just workerId then + shrinkTest vm test + else + pure Nothing + shrinkLoop callback vm (n - 1) + +symexecTxs + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => m () + -> VM Concrete + -> Bool -- ^ onlyRandom + -> Maybe Text -- ^ Contract name + -> [Tx] + -> m () +symexecTxs callback vm onlyRandom name txs = mapM_ (symexecTx callback vm name) =<< txsToTxAndVmsSym vm onlyRandom txs + +txsToTxAndVmsSym + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => VM Concrete + -> Bool + -> [Tx] + -> m [(Maybe Tx, VM Concrete, [Tx])] +txsToTxAndVmsSym vm _ [] = pure [(Nothing, vm, [])] +txsToTxAndVmsSym vm False txs = do + -- Separate the last tx, which should be the one increasing coverage + let (itxs, ltx) = (init txs, last txs) + -- TODO: execTx is in Execution.hs but not exported or we need to import it. + -- Execution.hs exports callseq and execTxOptC. + -- We can use EVM.Exec.exec or Echidna.Exec.execTx? + -- Echidna.Exec has execTx. + + -- Wait, Echidna.Exec.execTx returns (VMResult, VM). + -- We need to import Echidna.Exec. + + -- Using a fold to execute transactions + -- We need execTx from Echidna.Exec + let execTx' v t = snd <$> Echidna.Exec.execTx v t + + ivm <- foldlM execTx' vm itxs + + -- Split the sequence randomly and select any next transaction + i <- if length txs == 1 then pure 0 else rElem $ NEList.fromList [1 .. length txs - 1] + let rtxs = take i txs + rvm <- foldlM execTx' vm rtxs + cfg <- asks (.cfg) + let targets = cfg.campaignConf.symExecTargets + if null targets + then pure [(Just ltx, ivm, txs), (Nothing, rvm, rtxs)] + else pure [(Nothing, rvm, rtxs)] + +txsToTxAndVmsSym vm True txs = do + let execTx' v t = snd <$> Echidna.Exec.execTx v t + -- Split the sequence randomly and select any next transaction + i <- if length txs == 1 then pure 0 else rElem $ NEList.fromList [1 .. length txs - 1] + let rtxs = take i txs + rvm <- foldlM execTx' vm rtxs + pure [(Nothing, rvm, rtxs)] + +symexecTx + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => m () + -> VM Concrete + -> Maybe Text + -> (Maybe Tx, VM Concrete, [Tx]) + -> m () +symexecTx callback vm name (tx, vm', txsBase) = do + conf <- asks (.cfg) + dapp <- asks (.dapp) + let cs = Map.elems dapp.solcByName + contract <- chooseContract cs name + failedTests <- findFailedTests + let failedTestSignatures = map getAssertionSignature failedTests + case tx of + Nothing -> getRandomTargetMethod contract conf.campaignConf.symExecTargets failedTestSignatures >>= \case + Nothing -> do + return () + Just method -> exploreAndVerify callback vm contract method vm' txsBase + Just t -> getTargetMethodFromTx t contract failedTestSignatures >>= \case + Nothing -> do + return () + Just method -> do + exploreAndVerify callback vm contract method vm' txsBase + +exploreAndVerify + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => m () + -> VM Concrete + -> SolcContract + -> Method + -> VM Concrete + -> [Tx] + -> m () +exploreAndVerify callback vm contract method vm' txsBase = do + -- exploreContract returns (ThreadId, MVar ([SymTx], [Text])) + (threadId, symTxsChan) <- exploreContract contract method vm' + modify' (\ws -> ws { runningThreads = [threadId] }) + callback + + (symTxs, partials) <- liftIO $ takeMVar symTxsChan + + modify' (\ws -> ws { runningThreads = [] }) + callback + + let txs = extractTxs symTxs + let errors = extractErrors symTxs + + unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during symbolic exploration: " <> show e)) errors + unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic exploration: " <> unpack e)) partials + + -- We can't do callseq vm' [symTx] because callseq might post the full call sequence as an event + -- callseq expects [Tx] + -- symTx is a Tx (from extractTxs) + + -- We need to run callseq on (txsBase + [symTx]) for each symTx + -- And we need to get the original VM (not vm' which is intermediate) + -- Actually we need the starting VM of the campaign? + -- No, callseq takes a VM. + + -- In Campaign.hs: callseq vm (txsBase <> [symTx]) + -- 'vm' was the initial VM of the worker. + -- Here 'vm' in runAgent is the initial VM. + -- But exploreAndVerify doesn't have access to initial VM easily unless passed down. + -- In Campaign.hs, 'vm' was in scope from runSymWorker. + + -- We need to pass the initial VM to exploreAndVerify. + -- But wait, runSymWorker passed 'vm' (initial) to symexecTxs? No. + -- symexecTxs took vm (initial) in my adaptation? Yes. + -- But exploreAndVerify is taking vm' (intermediate). + + -- I need to access the initial VM. I'll store it in Reader or State? + -- Or just pass it. + -- I'll modify symexecTxs and exploreAndVerify to take 'initialVm'. + + -- For now, let's assume I can get it. + -- I'll pass it from runAgent -> busListenerLoop -> handleMessage -> symexecTxs -> symexecTx -> exploreAndVerify + + newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm (txsBase <> [symTx]) False) txs + + when (not newCoverage && null errors && not (null txs)) ( + 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.") + +verifyMethods + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => VM Concrete + -> Maybe Text + -> m () + -> m () +verifyMethods vm name callback = do + dapp <- asks (.dapp) + let cs = Map.elems dapp.solcByName + 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 vm name callback contract method + else pushWorkerEvent $ SymExecError ("Skipped verification of method " <> unpack method.methodSignature) + ) + +symExecMethod + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => VM Concrete + -> Maybe Text + -> m () + -> SolcContract + -> Method + -> m () +symExecMethod vm name callback contract method = do + callback + (threadId, symTxsChan) <- verifyMethod method contract vm + + modify' (\ws -> ws { runningThreads = [threadId] }) + callback + + (symTxs, partials) <- liftIO $ takeMVar symTxsChan + let txs = extractTxs symTxs + let errors = extractErrors symTxs + + modify' (\ws -> ws { runningThreads = [] }) + callback + + newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm [symTx] False) txs + let methodSignature = unpack method.methodSignature + unless newCoverage $ do + unless (null txs) $ error "No new coverage but symbolic execution found valid txs. Something is wrong." + when (null errors && null partials) $ do + updateTests $ \test -> do + if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then + pure $ Just $ test { Test.state = Unsolvable } + else + pure $ Just test + + unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) solving constraints produced by method " <> methodSignature <> ": " <> show e)) errors + unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic verification of method " <> methodSignature <> ": " <> unpack e)) partials + when (not (null partials) || not (null errors)) $ do + updateTests $ \test -> do + if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then + pure $ Just $ test {Test.state = Passed} + else + pure $ Just test + + pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction.") + +findFailedTests + :: (MonadIO m, MonadReader Env m, MonadState WorkerState m) + => m [EchidnaTest] +findFailedTests = do + testRefs <- asks (.testRefs) + tests <- liftIO $ traverse readIORef testRefs + pure $ filter didFail tests diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs index 0543822f6..1d76f4ba4 100644 --- a/lib/Echidna/Campaign.hs +++ b/lib/Echidna/Campaign.hs @@ -1,65 +1,21 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE OverloadedRecordDot #-} module Echidna.Campaign where -import Control.Concurrent -import Control.DeepSeq (force) -import Control.Monad (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) -import Control.Monad.State.Strict - (MonadState(..), StateT(..), gets, MonadIO, modify') -import Control.Monad.Trans (lift) -import Data.Binary.Get (runGetOrFail) -import Data.ByteString.Lazy qualified as LBS -import Data.Foldable (foldlM) -import Data.IORef (readIORef, atomicModifyIORef', writeIORef) -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.Set (Set) -import Data.Set qualified as Set -import Data.Text (Text, unpack) +import Control.Concurrent (forkFinally, dupChan, readChan, newEmptyMVar, putMVar, MVar, Chan) +import Control.Monad (void, when) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.Reader (MonadReader, asks) import Data.Time (LocalTime) -import Data.Vector qualified as V -import System.Random (mkStdGen) -import EVM (cheatCode) -import EVM.ABI (getAbi, AbiType(AbiAddressType, AbiTupleType), AbiValue(AbiAddress, AbiTuple), abiValueType) -import EVM.Dapp (DappInfo(..)) -import EVM.Solidity (SolcContract(..), Method(..)) -import EVM.Types hiding (Env, Frame(state), Gas) - -import Echidna.ABI -import Echidna.Events (extractEventValues) -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.Symbolic (forceAddr) -import Echidna.SymExec.Verification (verifyMethod, isSuitableToVerifyMethod) -import Echidna.Test -import Echidna.Transaction -import Echidna.Types.Campaign -import Echidna.Types.Config -import Echidna.Types.Corpus (Corpus, corpusSize) -import Echidna.Types.Coverage (coverageStats) -import Echidna.Types.Random (rElem) -import Echidna.Types.Signature (FunctionName) -import Echidna.Types.Test -import Echidna.Types.Test qualified as Test -import Echidna.Types.Tx (TxCall(..), Tx(..)) -import Echidna.Types.Worker -import Echidna.Worker - -instance MonadThrow m => MonadThrow (RandT g m) where - throwM = lift . throwM +import Echidna.Types.Campaign () -- For instances if any +import Echidna.Types.Config (Env(..), EConfig(..)) +import Echidna.Types.Test (EchidnaTest(..), TestState(..)) +import Echidna.Types.Worker (CampaignEvent(..), WorkerEvent(..)) +import Echidna.Worker (getNWorkers) -- | Given a 'Campaign', check if the test results should be reported as a -- success or a failure. @@ -67,608 +23,6 @@ isSuccessful :: [EchidnaTest] -> Bool isSuccessful = all (\case { Passed -> True; Open -> True; _ -> False; } . (.state)) --- | Run all the transaction sequences from the corpus and accumulate campaign --- state. Can be used to minimize corpus as the final campaign state will --- contain minimized corpus without sequences that didn't increase the coverage. -replayCorpus - :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) - => VM Concrete -- ^ VM to start replaying from - -> [(FilePath, [Tx])] -- ^ corpus to replay - -> m () -replayCorpus vm txSeqs = - forM_ (zip [1..] txSeqs) $ \(i, (file, txSeq)) -> do - let maybeFaultyTx = - List.find (\tx -> LitAddr tx.dst `notElem` Map.keys vm.env.contracts) $ - List.filter (\case Tx { call = NoCall } -> False; _ -> True) txSeq - case maybeFaultyTx of - Nothing -> do - _ <- callseq vm txSeq - pushWorkerEvent (TxSequenceReplayed file i (length txSeqs)) - Just faultyTx -> - pushWorkerEvent (TxSequenceReplayFailed file faultyTx) - -runWorker - :: (MonadIO m, MonadThrow m, MonadReader Env m) - => WorkerType - -> StateT WorkerState m () - -- ^ Callback to run after each state update (for instrumentation) - -> VM Concrete -- ^ Initial VM state - -> GenDict -- ^ Generation dictionary - -> Int -- ^ Worker id starting from 0 - -> [(FilePath, [Tx])] - -- ^ Initial corpus of transactions - -> Int -- ^ Test limit for this worker - -> Maybe Text -- ^ Specified contract name - -> m (WorkerStopReason, WorkerState) -runWorker SymbolicWorker callback vm dict workerId initialCorpus _ name = - runSymWorker callback vm dict workerId initialCorpus name -runWorker FuzzWorker callback vm dict workerId initialCorpus testLimit _ = - runFuzzWorker callback vm dict workerId initialCorpus testLimit - -runSymWorker - :: (MonadIO m, MonadThrow m, MonadReader Env m) - => StateT WorkerState m () - -- ^ Callback to run after each state update (for instrumentation) - -> VM Concrete -- ^ Initial VM state - -> GenDict -- ^ Generation dictionary - -> Int -- ^ Worker id starting from 0 - -> [(FilePath, [Tx])] - -- ^ Initial corpus of transactions - -> Maybe Text -- ^ Specified contract name - -> m (WorkerStopReason, WorkerState) -runSymWorker callback vm dict workerId _ name = do - cfg <- asks (.cfg) - let nworkers = getNFuzzWorkers cfg.campaignConf -- getNFuzzWorkers, NOT getNWorkers - eventQueue <- asks (.eventQueue) - chan <- liftIO $ dupChan eventQueue - - flip runStateT initialState $ - flip evalRandT (mkStdGen effectiveSeed) $ do -- unused but needed for callseq - if (cfg.campaignConf.workers == Just 0) && (cfg.campaignConf.seqLen == 1) then do - verifyMethods -- No arguments, everything is in this environment - pure SymbolicVerificationDone - else do - lift callback - listenerLoop listenerFunc chan nworkers - pure SymbolicExplorationDone - - where - - effectiveSeed = dict.defSeed + workerId - effectiveGenDict = dict { defSeed = effectiveSeed } - initialState = - WorkerState { workerId - , genDict = effectiveGenDict - , newCoverage = False - , ncallseqs = 0 - , ncalls = 0 - , totalGas = 0 - , runningThreads = [] - } - - -- We could pattern match on workerType here to ignore WorkerEvents from SymbolicWorkers, - -- but it may be useful to symexec on top of symexec results to produce multi-transaction - -- chains where each transaction results in new coverage. - listenerFunc (_, WorkerEvent _ _ (NewCoverage {transactions})) = do - void $ callseq vm transactions - symexecTxs False transactions - shrinkAndRandomlyExplore transactions (10 :: Int) - listenerFunc _ = pure () - - shrinkAndRandomlyExplore _ 0 = do - testRefs <- asks (.testRefs) - tests <- liftIO $ traverse readIORef testRefs - CampaignConf{shrinkLimit} <- asks (.cfg.campaignConf) - when (any shrinkable tests) $ shrinkLoop shrinkLimit - - shrinkAndRandomlyExplore txs n = do - testRefs <- asks (.testRefs) - tests <- liftIO $ traverse readIORef testRefs - CampaignConf{stopOnFail, shrinkLimit} <- asks (.cfg.campaignConf) - if stopOnFail && any final tests then - lift callback -- >> pure FastFailed - else if any shrinkable tests then do - shrinkLoop shrinkLimit - shrinkAndRandomlyExplore txs n - else do - symexecTxs False txs - shrinkAndRandomlyExplore txs (n - 1) - - - shrinkable test = - case test.state of - -- we shrink only tests which were solved on this - -- worker, see 'updateOpenTest' - Large _ | test.workerId == Just workerId -> True - _ -> False - - final test = - case test.state of - Solved -> True - Failed _ -> True - _ -> False - - - shrinkLoop 0 = return () - shrinkLoop n = do - lift callback - updateTests $ \test -> do - if test.workerId == Just workerId then - shrinkTest vm test - else - pure Nothing - shrinkLoop (n - 1) - - 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) - txsToTxAndVmsSym _ [] = pure [(Nothing, vm, [])] - txsToTxAndVmsSym False txs = do - -- Separate the last tx, which should be the one increasing coverage - let (itxs, ltx) = (init txs, last txs) - ivm <- foldlM (\vm' tx -> snd <$> execTx vm' tx) vm itxs - -- Split the sequence randomly and select any next transaction - i <- if length txs == 1 then pure 0 else rElem $ NEList.fromList [1 .. length txs - 1] - let rtxs = take i txs - rvm <- foldlM (\vm' tx -> snd <$> execTx vm' tx) vm rtxs - cfg <- asks (.cfg) - let targets = cfg.campaignConf.symExecTargets - if null targets - then pure [(Just ltx, ivm, txs), (Nothing, rvm, rtxs)] - else pure [(Nothing, rvm, rtxs)] - - txsToTxAndVmsSym True txs = do - -- Split the sequence randomly and select any next transaction - i <- if length txs == 1 then pure 0 else rElem $ NEList.fromList [1 .. length txs - 1] - let rtxs = take i txs - rvm <- foldlM (\vm' tx -> snd <$> execTx vm' tx) vm rtxs - pure [(Nothing, rvm, rtxs)] - - - symexecTx (tx, vm', txsBase) = do - conf <- asks (.cfg) - dapp <- asks (.dapp) - let cs = Map.elems dapp.solcByName - contract <- chooseContract cs name - failedTests <- findFailedTests - let failedTestSignatures = map getAssertionSignature failedTests - case tx of - Nothing -> getRandomTargetMethod contract conf.campaignConf.symExecTargets failedTestSignatures >>= \case - Nothing -> do - return () - 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 - - exploreAndVerify contract method vm' txsBase = do - (threadId, symTxsChan) <- exploreContract contract method vm' - modify' (\ws -> ws { runningThreads = [threadId] }) - lift callback - - (symTxs, partials) <- liftIO $ takeMVar symTxsChan - - modify' (\ws -> ws { runningThreads = [] }) - lift callback - - let txs = extractTxs symTxs - let errors = extractErrors symTxs - - unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during symbolic exploration: " <> show e)) errors - unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic exploration: " <> unpack e)) partials - - -- We can't do callseq vm' [symTx] because callseq might post the full call sequence as an event - newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm (txsBase <> [symTx])) txs - - when (not newCoverage && null errors && not (null txs)) ( - 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.") - - verifyMethods = do - dapp <- asks (.dapp) - let cs = Map.elems dapp.solcByName - 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) - ) - - symExecMethod contract method = do - lift callback - (threadId, symTxsChan) <- verifyMethod 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 - -- We can't do callseq vm' [symTx] because callseq might post the full call sequence as an event - newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm [symTx]) txs - let methodSignature = unpack method.methodSignature - unless newCoverage $ do - unless (null txs) $ error "No new coverage but symbolic execution found valid txs. Something is wrong." - when (null errors && null partials) $ do - updateTests $ \test -> do - if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then - pure $ Just $ test { Test.state = Unsolvable } - else - pure $ Just test - - unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) solving constraints produced by method " <> methodSignature <> ": " <> show e)) errors - unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic verification of method " <> methodSignature <> ": " <> unpack e)) partials - when (not (null partials) || not (null errors)) $ do - updateTests $ \test -> do - if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then - pure $ Just $ test {Test.state = Passed} - else - pure $ Just test - - pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction.") - --- | Run a fuzzing campaign given an initial universe state, some tests, and an --- optional dictionary to generate calls with. Return the 'Campaign' state once --- we can't solve or shrink anything. -runFuzzWorker - :: (MonadIO m, MonadThrow m, MonadReader Env m) - => StateT WorkerState m () - -- ^ Callback to run after each state update (for instrumentation) - -> VM Concrete -- ^ Initial VM state - -> GenDict -- ^ Generation dictionary - -> Int -- ^ Worker id starting from 0 - -> [(FilePath, [Tx])] - -- ^ Initial corpus of transactions - -> Int -- ^ Test limit for this worker - -> m (WorkerStopReason, WorkerState) -runFuzzWorker callback vm dict workerId initialCorpus testLimit = do - let - effectiveSeed = dict.defSeed + workerId - effectiveGenDict = dict { defSeed = effectiveSeed } - initialState = - WorkerState { workerId - , genDict = effectiveGenDict - , newCoverage = False - , ncallseqs = 0 - , ncalls = 0 - , totalGas = 0 - , runningThreads = [] - } - - flip runStateT initialState $ do - flip evalRandT (mkStdGen effectiveSeed) $ do - lift callback - void $ replayCorpus vm initialCorpus - run - - where - run = do - testRefs <- asks (.testRefs) - tests <- liftIO $ traverse readIORef testRefs - CampaignConf{stopOnFail, shrinkLimit} <- asks (.cfg.campaignConf) - ncalls <- gets (.ncalls) - - let - shrinkable test = - case test.state of - -- we shrink only tests which were solved on this - -- worker, see 'updateOpenTest' - Large n | test.workerId == Just workerId -> - n < shrinkLimit - _ -> False - - final test = - case test.state of - Solved -> True - Failed _ -> True - _ -> False - - closeOptimizationTest test = - case test.testType of - OptimizationTest _ _ -> - test { Test.state = Large 0 - , workerId = Just workerId - } - _ -> test - - if | stopOnFail && any final tests -> - lift callback >> pure FastFailed - - -- we shrink first before going back to fuzzing - | any shrinkable tests -> - shrink >> lift callback >> run - - -- no shrinking work, fuzz - | (null tests || any isOpen tests) && ncalls < testLimit -> - fuzz >> lift callback >> run - - -- NOTE: this is a hack which forces shrinking of optimization tests - -- after test limit is reached - | ncalls >= testLimit && any (\t -> isOpen t && isOptimizationTest t) tests -> do - liftIO $ forM_ testRefs $ \testRef -> - atomicModifyIORef' testRef (\test -> (closeOptimizationTest test, ())) - lift callback >> run - - -- no more work to do, means we reached the test limit, exit - | otherwise -> - lift callback >> pure TestLimitReached - - fuzz = randseq vm.env.contracts >>= fmap fst . callseq vm - - -- To avoid contention we only shrink tests that were falsified by this - -- worker. Tests are marked with a worker in 'updateOpenTest'. - -- - -- TODO: This makes some workers run longer as they work less on their - -- test limit portion during shrinking. We should move to a test limit shared - -- between workers to avoid that. This way other workers will "drain" - -- the work queue. - shrink = updateTests $ \test -> do - if test.workerId == Just workerId then - shrinkTest vm test - else - pure Nothing - --- | Generate a new sequences of transactions, either using the corpus or with --- randomly created transactions -randseq - :: (MonadRandom m, MonadReader Env m, MonadState WorkerState m, MonadIO m) - => Map (Expr 'EAddr) Contract - -> m [Tx] -randseq deployedContracts = do - env <- ask - let world = env.world - - let - mutConsts = env.cfg.campaignConf.mutConsts - seqLen = env.cfg.campaignConf.seqLen - - -- TODO: include reproducer when optimizing - --let rs = filter (not . null) $ map (.testReproducer) $ ca._tests - - -- Generate new random transactions - randTxs <- replicateM seqLen (genTx world deployedContracts) - -- Generate a random mutator - cmut <- if seqLen == 1 then seqMutatorsStateless (fromConsts mutConsts) - else seqMutatorsStateful (fromConsts mutConsts) - -- Fetch the mutator - let mut = getCorpusMutation cmut - corpus <- liftIO $ readIORef env.corpusRef - if null corpus - then pure randTxs -- Use the generated random transactions - else mut seqLen corpus randTxs -- Apply the mutator - --- TODO callseq ideally shouldn't need to be MonadRandom - --- | Runs a transaction sequence and checks if any test got falsified or can be --- minimized. Stores any useful data in the campaign state if coverage increased. --- Returns resulting VM, as well as whether any new coverage was found. -callseq - :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) - => VM Concrete - -> [Tx] - -> m (VM Concrete, Bool) -callseq vm txSeq = do - env <- ask - -- First, we figure out whether we need to execute with or without coverage - -- optimization and gas info, and pick our execution function appropriately - let - conf = env.cfg.campaignConf - coverageEnabled = isJust conf.knownCoverage - execFunc = if coverageEnabled then execTxOptC else execTx - - -- Run each call sequentially. This gives us the result of each call - -- and the new state - (results, vm') <- evalSeq vm execFunc txSeq - - -- If there is new coverage, add the transaction list to the corpus - newCoverage <- gets (.newCoverage) - when newCoverage $ do - ncallseqs <- gets (.ncallseqs) - -- Even if this takes a bit of time, this is okay as finding new coverage - -- is expected to be infrequent in the long term - newSize <- liftIO $ atomicModifyIORef' env.corpusRef $ \corp -> - -- Corpus is a bit too lazy, force the evaluation to reduce the memory usage - let !corp' = force $ addToCorpus (ncallseqs + 1) results corp - in (corp', corpusSize corp') - - (points, numCodehashes) <- liftIO $ coverageStats env.coverageRefInit env.coverageRefRuntime - pushWorkerEvent NewCoverage { points - , numCodehashes - , corpusSize = newSize - , transactions = fst <$> results - } - - modify' $ \workerState -> - - let - -- compute the addresses not present in the old VM via set difference - newAddrs = Map.keys $ vm'.env.contracts \\ vm.env.contracts - -- and construct a set to union to the constants table - diffs = Map.fromList [(AbiAddressType, Set.fromList $ AbiAddress . forceAddr <$> newAddrs)] - -- Now we try to parse the return values as solidity constants, and add them to 'GenDict' - resultMap = returnValues results workerState.genDict.rTypes - -- compute the new events to be stored - eventDiffs = extractEventValues env.dapp vm vm' - -- union the return results with the new addresses - additions = Map.unionsWith Set.union [resultMap, eventDiffs, diffs] - -- append to the constants dictionary - updatedDict = workerState.genDict - { constants = Map.unionWith Set.union workerState.genDict.constants additions - , dictValues = Set.union (mkDictValues $ Set.unions $ Map.elems additions) - workerState.genDict.dictValues - } - - -- Update the worker state - in workerState - { genDict = updatedDict - -- Reset the new coverage flag - , newCoverage = False - -- Keep track of the number of calls to `callseq` - , ncallseqs = workerState.ncallseqs + 1 - } - - pure (vm', newCoverage) - - where - -- Given a list of transactions and a return typing rule, checks whether we - -- know the return type for each function called. If yes, try to parse the - -- return value as a value of that type. Returns a 'GenDict' style Map. - returnValues - :: [(Tx, VMResult Concrete)] - -> (FunctionName -> Maybe AbiType) - -> Map AbiType (Set AbiValue) - returnValues txResults returnTypeOf = - Map.unionsWith Set.union . mapMaybe extractValues $ txResults - where - extractValues (tx, result) = case result of - VMSuccess (ConcreteBuf buf) -> do - fname <- case tx.call of - SolCall (fname, _) -> Just fname - _ -> Nothing - type' <- returnTypeOf fname - case runGetOrFail (getAbi type') (LBS.fromStrict buf) of - Right (_, _, abiValue) -> - if isTuple type' - then Just $ Map.fromListWith Set.union - [ (abiValueType val, Set.singleton val) - | val <- filter (/= AbiAddress (forceAddr cheatCode)) $ V.toList $ getTupleVector abiValue - ] - else if abiValue /= AbiAddress (forceAddr cheatCode) - then Just $ Map.singleton type' (Set.singleton abiValue) - else Nothing - _ -> Nothing - _ -> Nothing - - isTuple (AbiTupleType _) = True - isTuple _ = False - getTupleVector (AbiTuple ts) = ts - getTupleVector _ = error "Not a tuple!" - - -- | Add transactions to the corpus, discarding reverted ones - addToCorpus :: Int -> [(Tx, VMResult Concrete)] -> Corpus -> Corpus - addToCorpus n res corpus = - if null rtxs then corpus else Set.insert (n, rtxs) corpus - where rtxs = fst <$> res - --- | Execute a transaction, capturing the PC and codehash of each instruction --- executed, saving the transaction if it finds new coverage. -execTxOptC - :: (MonadIO m, MonadReader Env m, MonadState WorkerState m, MonadThrow m) - => VM Concrete -> Tx - -> m (VMResult Concrete, VM Concrete) -execTxOptC vm tx = do - ((res, grew), vm') <- runStateT (execTxWithCov tx) vm - when grew $ do - modify' $ \workerState -> - let - dict' = case tx.call of - SolCall c -> gaddCalls (Set.singleton c) workerState.genDict - _ -> workerState.genDict - in workerState { newCoverage = True, genDict = dict' } - pure (res, vm') - --- | Given an initial 'VM' state and a way to run transactions, evaluate a list --- of transactions, constantly checking if we've solved any tests. -evalSeq - :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) - => VM Concrete -- ^ Initial VM - -> (VM Concrete -> Tx -> m (result, VM Concrete)) - -> [Tx] - -> m ([(Tx, result)], VM Concrete) -evalSeq vm0 execFunc = go vm0 [] where - go vm executedSoFar toExecute = do - -- NOTE: we do reverse here because we build up this list by prepending, - -- see the last line of this function. - updateTests (updateOpenTest vm (reverse executedSoFar)) - modify' $ \workerState -> workerState { ncalls = workerState.ncalls + 1 } - case toExecute of - [] -> pure ([], vm) - (tx:remainingTxs) -> do - (result, vm') <- execFunc vm tx - modify' $ \workerState -> workerState { totalGas = workerState.totalGas + fromIntegral (vm'.burned - vm.burned) } - -- NOTE: we don't use the intermediate VMs, just the last one. If any of - -- the intermediate VMs are needed, they can be put next to the result - -- of each transaction - `m ([(Tx, result, VM)])` - (remaining, vm'') <- go vm' (tx:executedSoFar) remainingTxs - pure ((tx, result) : remaining, vm'') - --- | Update tests based on the return value from the given function. --- Nothing skips the update. -updateTests - :: (MonadIO m, MonadReader Env m, MonadState WorkerState m) - => (EchidnaTest -> m (Maybe EchidnaTest)) - -> m () -updateTests f = do - testRefs <- asks (.testRefs) - forM_ testRefs $ \testRef -> do - test <- liftIO $ readIORef testRef - f test >>= \case - Just test' -> liftIO $ writeIORef testRef test' - Nothing -> pure () - -findFailedTests - :: (MonadIO m, MonadReader Env m, MonadState WorkerState m) - => m [EchidnaTest] -findFailedTests = do - testRefs <- asks (.testRefs) - tests <- liftIO $ traverse readIORef testRefs - pure $ filter didFail tests - --- | Update an open test after checking if it is falsified by the 'reproducer' -updateOpenTest - :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) - => VM Concrete -- ^ VM after applying potential reproducer - -> [Tx] -- ^ potential reproducer - -> EchidnaTest - -> m (Maybe EchidnaTest) -updateOpenTest vm reproducer test = do - case test.state of - Open -> do - (testValue, vm') <- checkETest test vm - let result = getResultFromVM vm' - case testValue of - BoolValue False -> do - workerId <- Just <$> gets (.workerId) - let test' = test { Test.state = Large 0 - , reproducer - , vm = Just vm - , result - , workerId - } - pushWorkerEvent (TestFalsified test') - pure $ Just test' - - IntValue value' | value' > value -> do - let test' = test { reproducer - , value = IntValue value' - , vm = Just vm - , result - } - pushWorkerEvent (TestOptimized test') - pure $ Just test' - where - value = - case test.value of - IntValue x -> x - -- TODO: fix this with proper types - _ -> error "Invalid type of value for optimization" - - _ -> - -- no luck with fuzzing this time - pure Nothing - _ -> - -- not an open test, skip - pure Nothing - -- | Listener reads events and runs the given 'handler' function. It exits after -- receiving all 'WorkerStopped' events and sets the returned 'MVar' so the -- parent thread can safely block on listener until all events are processed. diff --git a/lib/Echidna/Config.hs b/lib/Echidna/Config.hs index fcb1978ca..938a2b5b8 100644 --- a/lib/Echidna/Config.hs +++ b/lib/Echidna/Config.hs @@ -25,9 +25,21 @@ import Echidna.Types.Solidity import Echidna.Types.Test (TestConf(..)) import Echidna.Types.Tx (TxConf(TxConf), maxGasPerBlock, defaultTimeDelay, defaultBlockDelay) +adjustForVerificationMode :: EConfig -> EConfig +adjustForVerificationMode cfg = + if isVerificationMode cfg.solConf.testMode then + cfg { campaignConf = cfg.campaignConf + { workers = Just 0 + , seqLen = 1 + , symExec = True + } + } + else + cfg + instance FromJSON EConfig where -- retrieve the config from the key usage annotated parse - parseJSON x = (.econfig) <$> parseJSON @EConfigWithUsage x + parseJSON x = adjustForVerificationMode . (.econfig) <$> parseJSON @EConfigWithUsage x instance FromJSON EConfigWithUsage where -- this runs the parser in a StateT monad which keeps track of the keys diff --git a/lib/Echidna/Execution.hs b/lib/Echidna/Execution.hs new file mode 100644 index 000000000..69f4e7e5a --- /dev/null +++ b/lib/Echidna/Execution.hs @@ -0,0 +1,291 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE DataKinds #-} + +module Echidna.Execution where + +import Control.Concurrent.STM (atomically, writeTChan) +import Control.DeepSeq (force) +import Control.Monad (when, forM_) +import Control.Monad.Catch (MonadThrow(..)) +import Control.Monad.Random.Strict (MonadRandom) +import Control.Monad.Reader (MonadReader, asks, liftIO, ask) +import Control.Monad.State.Strict + (MonadState(..), StateT(..), gets, MonadIO, modify') +import Data.Binary.Get (runGetOrFail) +import Data.ByteString.Lazy qualified as LBS +import Data.IORef (readIORef, atomicModifyIORef', writeIORef) +import Data.List qualified as List +import Data.Map (Map, (\\)) +import Data.Map qualified as Map +import Data.Maybe (isJust, mapMaybe) +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Vector qualified as V + +import EVM (cheatCode) +import EVM.ABI (getAbi, AbiType(AbiAddressType, AbiTupleType), AbiValue(AbiAddress, AbiTuple), abiValueType) +import EVM.Types (VM(..), VMResult(..), VMType(..), Expr(..)) +import EVM.Types qualified as EVM + +import Echidna.ABI +import Echidna.Events (extractEventValues) +import Echidna.Exec +import Echidna.Types.Campaign +import Echidna.Types.Config +import Echidna.Types.Corpus (Corpus, corpusSize) +import Echidna.Types.Coverage (coverageStats) +import Echidna.Types.InterWorker (WrappedMessage(..), Message(..), BroadcastMsg(NewCoverageInfo), AgentId(..)) +import Echidna.SymExec.Symbolic (forceAddr) +import Echidna.Types.Signature (FunctionName) +import Echidna.Types.Test +import Echidna.Test (checkETest, getResultFromVM) +import Echidna.Types.Test qualified as Test +import Echidna.Types.Tx (TxCall(..), Tx(..)) +import Echidna.Types.Worker (WorkerEvent(..)) +import Echidna.Worker (pushWorkerEvent) + +-- | Run all the transaction sequences from the corpus and accumulate campaign +-- state. Can be used to minimize corpus as the final campaign state will +-- contain minimized corpus without sequences that didn't increase the coverage. +replayCorpus + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => VM Concrete -- ^ VM to start replaying from + -> [(FilePath, [Tx])] -- ^ corpus to replay + -> m () +replayCorpus vm txSeqs = + forM_ (zip [1..] txSeqs) $ \(i, (file, txSeq)) -> do + let maybeFaultyTx = + List.find (\tx -> LitAddr tx.dst `notElem` Map.keys vm.env.contracts) $ + List.filter (\case Tx { call = NoCall } -> False; _ -> True) txSeq + case maybeFaultyTx of + Nothing -> do + _ <- callseq vm txSeq True + pushWorkerEvent (TxSequenceReplayed file i (length txSeqs)) + Just faultyTx -> + pushWorkerEvent (TxSequenceReplayFailed file faultyTx) + +-- | Runs a transaction sequence and checks if any test got falsified or can be +-- minimized. Stores any useful data in the campaign state if coverage increased. +-- Returns resulting VM, as well as whether any new coverage was found. +callseq + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => VM Concrete + -> [Tx] + -> Bool + -> m (VM Concrete, Bool) +callseq vm txSeq isReplaying = do + env <- ask + -- First, we figure out whether we need to execute with or without coverage + -- optimization and gas info, and pick our execution function appropriately + let + conf = env.cfg.campaignConf + coverageEnabled = isJust conf.knownCoverage + execFunc = if coverageEnabled then execTxOptC else execTx + + -- Run each call sequentially. This gives us the result of each call + -- and the new state + (results, vm') <- evalSeq vm execFunc txSeq + + -- If there is new coverage, add the transaction list to the corpus + newCoverage <- gets (.newCoverage) + when newCoverage $ do + ncallseqs <- gets (.ncallseqs) + -- Even if this takes a bit of time, this is okay as finding new coverage + -- is expected to be infrequent in the long term + newSize <- liftIO $ atomicModifyIORef' env.corpusRef $ \corp -> + -- Corpus is a bit too lazy, force the evaluation to reduce the memory usage + let !corp' = force $ addToCorpus (ncallseqs + 1) results corp + in (corp', corpusSize corp') + + (points, numCodehashes) <- liftIO $ coverageStats env.coverageRefInit env.coverageRefRuntime + pushWorkerEvent NewCoverage { points + , numCodehashes + , corpusSize = newSize + , transactions = fst <$> results + } + + -- Broadcast new coverage to other agents (e.g. Symbolic) + workerId <- gets (.workerId) + liftIO $ atomically $ writeTChan env.bus (WrappedMessage (FuzzerId workerId) (Broadcast (NewCoverageInfo points (fst <$> results) isReplaying))) + + modify' $ \workerState -> + + let + -- compute the addresses not present in the old VM via set difference + newAddrs = Map.keys $ vm'.env.contracts \\ vm.env.contracts + -- and construct a set to union to the constants table + diffs = Map.fromList [(AbiAddressType, Set.fromList $ AbiAddress . forceAddr <$> newAddrs)] + -- Now we try to parse the return values as solidity constants, and add them to 'GenDict' + resultMap = returnValues results workerState.genDict.rTypes + -- compute the new events to be stored + eventDiffs = extractEventValues env.dapp vm vm' + -- union the return results with the new addresses + additions = Map.unionsWith Set.union [resultMap, eventDiffs, diffs] + -- append to the constants dictionary + updatedDict = workerState.genDict + { constants = Map.unionWith Set.union workerState.genDict.constants additions + , dictValues = Set.union (mkDictValues $ Set.unions $ Map.elems additions) + workerState.genDict.dictValues + } + + -- Update the worker state + in workerState + { genDict = updatedDict + -- Reset the new coverage flag + , newCoverage = False + -- Keep track of the number of calls to `callseq` + , ncallseqs = workerState.ncallseqs + 1 + } + + pure (vm', newCoverage) + + where + -- Given a list of transactions and a return typing rule, checks whether we + -- know the return type for each function called. If yes, try to parse the + -- return value as a value of that type. Returns a 'GenDict' style Map. + returnValues + :: [(Tx, VMResult Concrete)] + -> (FunctionName -> Maybe AbiType) + -> Map AbiType (Set AbiValue) + returnValues txResults returnTypeOf = + Map.unionsWith Set.union . mapMaybe extractValues $ txResults + where + extractValues (tx, result) = case result of + VMSuccess (ConcreteBuf buf) -> do + fname <- case tx.call of + SolCall (fname, _) -> Just fname + _ -> Nothing + type' <- returnTypeOf fname + case runGetOrFail (getAbi type') (LBS.fromStrict buf) of + Right (_, _, abiValue) -> + if isTuple type' + then Just $ Map.fromListWith Set.union + [ (abiValueType val, Set.singleton val) + | val <- filter (/= AbiAddress (forceAddr cheatCode)) $ V.toList $ getTupleVector abiValue + ] + else if abiValue /= AbiAddress (forceAddr cheatCode) + then Just $ Map.singleton type' (Set.singleton abiValue) + else Nothing + _ -> Nothing + _ -> Nothing + + isTuple (AbiTupleType _) = True + isTuple _ = False + getTupleVector (AbiTuple ts) = ts + getTupleVector _ = error "Not a tuple!" + + -- | Add transactions to the corpus, discarding reverted ones + addToCorpus :: Int -> [(Tx, VMResult Concrete)] -> Corpus -> Corpus + addToCorpus n res corpus = + if null rtxs then corpus else Set.insert (n, rtxs) corpus + where rtxs = fst <$> res + +-- | Execute a transaction, capturing the PC and codehash of each instruction +-- executed, saving the transaction if it finds new coverage. +execTxOptC + :: (MonadIO m, MonadReader Env m, MonadState WorkerState m, MonadThrow m) + => VM Concrete -> Tx + -> m (VMResult Concrete, VM Concrete) +execTxOptC vm tx = do + ((res, grew), vm') <- runStateT (execTxWithCov tx) vm + when grew $ do + modify' $ \workerState -> + let + dict' = case tx.call of + SolCall c -> gaddCalls (Set.singleton c) workerState.genDict + _ -> workerState.genDict + in workerState { newCoverage = True, genDict = dict' } + pure (res, vm') + +-- | Given an initial 'VM' state and a way to run transactions, evaluate a list +-- of transactions, constantly checking if we've solved any tests. +evalSeq + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => VM Concrete -- ^ Initial VM + -> (VM Concrete -> Tx -> m (result, VM Concrete)) + -> [Tx] + -> m ([(Tx, result)], VM Concrete) +evalSeq vm0 execFunc = go vm0 [] where + go vm executedSoFar toExecute = do + -- NOTE: we do reverse here because we build up this list by prepending, + -- see the last line of this function. + updateTests (updateOpenTest vm (reverse executedSoFar)) + modify' $ \workerState -> workerState { ncalls = workerState.ncalls + 1 } + case toExecute of + [] -> pure ([], vm) + (tx:remainingTxs) -> do + (result, vm') <- execFunc vm tx + modify' $ \workerState -> workerState { totalGas = workerState.totalGas + fromIntegral (vm'.burned - vm.burned) } + -- NOTE: we don't use the intermediate VMs, just the last one. If any of + -- the intermediate VMs are needed, they can be put next to the result + -- of each transaction - `m ([(Tx, result, VM)])` + (remaining, vm'') <- go vm' (tx:executedSoFar) remainingTxs + pure ((tx, result) : remaining, vm'') + +-- | Update tests based on the return value from the given function. +-- Nothing skips the update. +updateTests + :: (MonadIO m, MonadReader Env m, MonadState WorkerState m) + => (EchidnaTest -> m (Maybe EchidnaTest)) + -> m () +updateTests f = do + testRefs <- asks (.testRefs) + forM_ testRefs $ \testRef -> do + test <- liftIO $ readIORef testRef + f test >>= \case + Just test' -> liftIO $ writeIORef testRef test' + Nothing -> pure () + +findFailedTests + :: (MonadIO m, MonadReader Env m, MonadState WorkerState m) + => m [EchidnaTest] +findFailedTests = do + testRefs <- asks (.testRefs) + tests <- liftIO $ traverse readIORef testRefs + pure $ filter didFail tests + +-- | Update an open test after checking if it is falsified by the 'reproducer' +updateOpenTest + :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m) + => VM Concrete -- ^ VM after applying potential reproducer + -> [Tx] -- ^ potential reproducer + -> EchidnaTest + -> m (Maybe EchidnaTest) +updateOpenTest vm reproducer test = do + case test.state of + Open -> do + (testValue, vm') <- checkETest test vm + let result = getResultFromVM vm' + case testValue of + BoolValue False -> do + workerId <- Just <$> gets (.workerId) + let test' = test { Test.state = Large 0 + , reproducer + , vm = Just vm + , result + , workerId + } + pushWorkerEvent (TestFalsified test') + pure $ Just test' + + IntValue value' | value' > value -> do + let test' = test { reproducer + , value = IntValue value' + , vm = Just vm + , result + } + pushWorkerEvent (TestOptimized test') + pure $ Just test' + where + value = + case test.value of + IntValue x -> x + -- TODO: fix this with proper types + _ -> error "Invalid type of value for optimization" + + _ -> + -- no luck with fuzzing this time + pure Nothing + _ -> + -- not an open test, skip + pure Nothing diff --git a/lib/Echidna/MCP.hs b/lib/Echidna/MCP.hs new file mode 100644 index 000000000..8c810b636 --- /dev/null +++ b/lib/Echidna/MCP.hs @@ -0,0 +1,468 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE OverloadedRecordDot #-} + +module Echidna.MCP where + +import Control.Concurrent (forkIO) +import Control.Monad (forever, unless) +import Control.Concurrent.STM +import Data.IORef (readIORef, modifyIORef', newIORef, IORef, atomicModifyIORef') +import Data.List (find, isPrefixOf, isSuffixOf, sort, intercalate) +import qualified Data.Maybe +import qualified Data.Set as Set +import qualified Data.Vector as Vector +import Data.Text (Text, pack, unpack) +import qualified Data.Text as T +import Data.Time (UTCTime, getCurrentTime, diffUTCTime) +import Text.Printf (printf) +import qualified Data.Map as Map +import Text.Read (readMaybe) +import System.Directory (getCurrentDirectory) +import Data.Char (isSpace, toLower) + +import MCP.Server +import EVM.Dapp (DappInfo(..)) +import EVM.Solidity (SolcContract(..), Method(..)) +import EVM.Types (Addr) +import EVM.ABI (AbiValue(..), AbiType(..), abiValueType) +import Echidna.Types.Test (EchidnaTest(..), didFail, isOptimizationTest) +import Echidna.Types.Tx (Tx(..), TxCall(..)) +import Echidna.Types.Coverage (CoverageFileType(..), mergeCoverageMaps, coverageStats) +import Echidna.Output.Source (ppCoveredCode, saveLcovHook) +import Echidna.Output.Corpus (loadTxs) + +import Echidna.Types.Config (Env(..), EConfig(..)) +import Echidna.Types.World (World(..)) +import Echidna.Types.Campaign (getNFuzzWorkers, CampaignConf(..), WorkerState(..)) +import Echidna.Types.InterWorker (Bus, Message(..), WrappedMessage(..), AgentId(..), FuzzerCmd(..), BroadcastMsg(..)) + +-- | Status state to track coverage info +data StatusState = StatusState + { lastCoverageTime :: Maybe UTCTime + , coveredFunctions :: [Text] + } + +-- | MCP Tool Definition +-- Simulates the definition of a tool exposed by an MCP server. +type ToolExecution = [(Text, Text)] -> Env -> Bus -> IORef [Text] -> IO String + +data Tool = Tool + { toolName :: String + , toolDescription :: String + , execute :: ToolExecution + } + +-- | Helper to get function name from Tx +getFunctionName :: Tx -> Text +getFunctionName tx = case tx.call of + SolCall (name, _) -> name + _ -> "unknown" + +-- | Implementation of status tool +statusTool :: [IORef WorkerState] -> IORef StatusState -> ToolExecution +statusTool workerRefs statusRef _ env _ _ = do + c <- readIORef env.corpusRef + st <- readIORef statusRef + now <- getCurrentTime + + -- Iterations + workers <- mapM readIORef workerRefs + let iterations = sum $ map (.ncalls) workers + let maxIterations = env.cfg.campaignConf.testLimit + + -- Coverage + (covPoints, _) <- coverageStats env.coverageRefInit env.coverageRefRuntime + + -- Tests + tests <- mapM readIORef env.testRefs + let failedCount = length $ filter didFail tests + let totalCount = length tests + + -- Optimization values + let optTests = filter isOptimizationTest tests + optValues = map (\(EchidnaTest {testType = ty, value = val}) -> printf "%s: %s" (show ty) (show val)) optTests + optStr = if null optValues then "None" else intercalate ", " optValues + + let timeStr = case st.lastCoverageTime of + Nothing -> "Never" + Just t -> show (round (diffUTCTime now t) :: Integer) + + funcs = if null st.coveredFunctions + then "None" + else unpack $ T.intercalate "\n- " st.coveredFunctions + + return $ printf "Corpus Size: %d\nIterations: %d/%d\nCoverage: %d\nTests: %d/%d\nOptimization Values: %s\nTime since last coverage: %s\nLast 10 covered functions:\n- %s" + (Set.size c) iterations maxIterations covPoints failedCount totalCount optStr timeStr funcs + +-- | Helper functions for inject_transaction +trim :: String -> String +trim = f . f + where f = reverse . dropWhile isSpace + +splitOn :: Char -> String -> [String] +splitOn _ "" = [] +splitOn c s = case break (== c) s of + (chunk, rest) -> chunk : case rest of + [] -> [] + (_:r) -> splitOn c r + +splitArgs :: String -> [String] +splitArgs s = go s 0 "" + where + go :: String -> Int -> String -> [String] + go [] _ current = [reverse current] + go (c:cs) level current + | c == '[' = go cs (level + 1) (c:current) + | c == ']' = go cs (level - 1) (c:current) + | c == ',' && level == 0 = reverse current : go cs level "" + | otherwise = go cs level (c:current) + +parsePrimitive :: String -> Maybe AbiValue +parsePrimitive s = + let s' = trim s + lowerS = map toLower s' + in if lowerS == "true" + then Just (AbiBool True) + else if lowerS == "false" + then Just (AbiBool False) + else if "0x" `isPrefixOf` s' + then AbiAddress . fromIntegral <$> (readMaybe s' :: Maybe Integer) + else AbiUInt 256 . fromIntegral <$> (readMaybe s' :: Maybe Integer) + +parseArray :: String -> Maybe AbiValue +parseArray s = do + let content = trim (drop 1 (take (length s - 1) s)) + let parts = if null content then [] else splitOn ',' content + vals <- mapM parsePrimitive parts + let vec = Vector.fromList vals + if Vector.null vec + then return $ AbiArrayDynamic (AbiUIntType 256) vec + else do + let t = abiValueType (Vector.head vec) + if all (\v -> abiValueType v == t) vals + then return $ AbiArrayDynamic t vec + else Nothing + +parseArg :: String -> Maybe AbiValue +parseArg s = + let s' = trim s + in if "[" `isPrefixOf` s' && "]" `isSuffixOf` s' + then parseArray s' + else parsePrimitive s' + +parseFuzzArg :: String -> Maybe (Maybe AbiValue) +parseFuzzArg s = + let s' = trim s + in if s' == "?" + then Just Nothing + else Just <$> parseArg s' + +parseFuzzCall :: String -> Maybe (Text, [Maybe AbiValue]) +parseFuzzCall s = do + let (fname, rest) = break (== '(') s + if null rest then Nothing else do + let argsS = take (length rest - 2) (drop 1 rest) -- remove parens + let argParts = if all isSpace argsS then [] else splitArgs argsS + args <- mapM parseFuzzArg argParts + return (pack fname, args) + +parseFuzzSequence :: String -> Maybe [(Text, [Maybe AbiValue])] +parseFuzzSequence s = mapM (parseFuzzCall . trim) (splitOn ';' s) + +parseCall :: String -> Maybe (String, [AbiValue]) +parseCall s = do + let (fname, rest) = break (== '(') s + if null rest then Nothing else do + let argsS = take (length rest - 2) (drop 1 rest) -- remove parens + let argParts = if all isSpace argsS then [] else splitArgs argsS + args <- mapM parseArg argParts + return (fname, args) + +readAddr :: String -> Maybe Addr +readAddr s = fromIntegral <$> (readMaybe s :: Maybe Integer) + +parseTx :: Maybe Tx -> String -> Maybe Tx +parseTx ctx s = do + let parts = words s + case parts of + (srcS:dstS:valS:_:_) | length parts >= 4 -> do + src <- readAddr srcS + dst <- readAddr dstS + val <- readMaybe valS + (fname, args) <- parseCall (unwords (drop 3 parts)) + return $ Tx (SolCall (pack fname, args)) src dst 1000000 0 val (0,0) + _ -> do + (fname, args) <- parseCall s + let (src, dst) = case ctx of + Just t -> (t.src, t.dst) + Nothing -> (0x1000, 0x2000) + return $ Tx (SolCall (pack fname, args)) src dst 1000000 0 0 (0,0) + +-- | Implementation of reload_corpus tool +reloadCorpusTool :: ToolExecution +reloadCorpusTool _ env _ _ = do + dir <- maybe getCurrentDirectory pure env.cfg.campaignConf.corpusDir + loadedSeqs <- loadTxs dir -- returns [(FilePath, [Tx])] + + if null loadedSeqs + then return "No transaction sequences found in corpus directory." + else do + currentCorpus <- readIORef env.corpusRef + let existingTxs = Set.map snd currentCorpus + + let newSeqs = map snd loadedSeqs + let uniqueNewSeqs = filter (`Set.notMember` existingTxs) newSeqs + + if null uniqueNewSeqs + then return "No NEW transaction sequences found in corpus directory." + else do + let maxId = if Set.null currentCorpus + then 0 + else fst (Set.findMax currentCorpus) + + let indexedNewSeqs = zip [maxId + 1 ..] uniqueNewSeqs + let newCorpus = Set.union currentCorpus (Set.fromList indexedNewSeqs) + + atomicModifyIORef' env.corpusRef $ const (newCorpus, ()) + return $ printf "Reloaded %d new transaction sequences from %s" (length uniqueNewSeqs) dir + +-- | Implementation of dump_lcov tool +dumpLcovTool :: ToolExecution +dumpLcovTool _ env _ _ = do + let contracts = Map.elems env.dapp.solcByName + dir <- maybe getCurrentDirectory pure env.cfg.campaignConf.corpusDir + filename <- saveLcovHook env dir env.sourceCache contracts + return $ "Dumped LCOV coverage to " ++ filename + +-- | Implementation of inject_fuzz_transactions tool +fuzzTransactionTool :: ToolExecution +fuzzTransactionTool args env bus _ = do + let txStr = Data.Maybe.fromMaybe "" (lookup "transactions" args) + case parseFuzzSequence (unpack txStr) of + Nothing -> return "Error: Failed to parse transaction sequence string." + Just seqPrototype -> do + -- Validate function names and argument counts + let dapp = env.dapp + methods = Map.elems dapp.abiMap + + methodsByName = Map.fromListWith (++) [(m.name, [m]) | m <- methods] + + validateCall (name, callArgs) = + case Map.lookup name methodsByName of + Nothing -> Just $ printf "Function '%s' not found." (unpack name) + Just ms -> + if any (\m -> length m.inputs == length callArgs) ms + then Nothing + else Just $ printf "Function '%s' found but with different argument count. Expected: %s, Got: %d" (unpack name) (show $ map (length . (.inputs)) ms) (length callArgs) + + errors = Data.Maybe.mapMaybe validateCall seqPrototype + + if not (null errors) + then return $ "Error:\n" ++ unlines errors + else do + let nWorkers = getNFuzzWorkers env.cfg.campaignConf + calcProb i + -- Worker 0 always injects transactions at position 0 with a probability of 90% + | i == 0 = 0.9 + -- For small campaigns (<= 2 workers), all workers share a low probability (20%) + | nWorkers <= 2 = 0.2 + -- For larger campaigns, scale probability linearly from 20% to 90% for other workers + | otherwise = 0.2 + fromIntegral (i - 1) * (0.7 / fromIntegral (nWorkers - 2)) + + mapM_ (\i -> atomically $ writeTChan bus (WrappedMessage AIId (ToFuzzer i (FuzzSequence seqPrototype (calcProb i))))) [0 .. nWorkers - 1] + return $ printf "Requested fuzzing of transaction sequence '%s' on %d fuzzers" (unpack txStr) nWorkers + +-- | Implementation of clear_fuzz_priorities tool +clearPrioritiesTool :: ToolExecution +clearPrioritiesTool _ env bus _ = do + let nWorkers = getNFuzzWorkers env.cfg.campaignConf + mapM_ (\i -> atomically $ writeTChan bus (WrappedMessage AIId (ToFuzzer i ClearPrioritization))) [0 .. nWorkers - 1] + return $ printf "Requested clearing priorities on %d fuzzers" nWorkers + +-- | Implementation of read_logs tool +readLogsTool :: ToolExecution +readLogsTool _ _ _ logsRef = do + logs <- readIORef logsRef + -- Get last 100 logs + -- logs is [Newest, ..., Oldest] + -- We want to take the 100 newest, and show them in chronological order + let logsToShow = reverse $ take 100 logs + return $ unpack $ T.unlines logsToShow + +-- | Implementation of target tool +targetTool :: ToolExecution +targetTool _ env _ _ = do + let contracts = env.dapp.solcByName + world = env.world + + -- Helper to check if a contract is a target + isTarget :: SolcContract -> Bool + isTarget c = c.runtimeCodehash `Map.member` world.highSignatureMap + + -- Find candidates + candidates = filter (isTarget . snd) (Map.toList contracts) + + case candidates of + [] -> return "Error: No target contract found." + ((name, contract):_) -> do + let signatures = map (.methodSignature) (Map.elems contract.abiMap) + sortedSigs = sort signatures + return $ printf "Contract: %s\nFunctions:\n- %s" (unpack name) (unpack $ T.intercalate "\n- " sortedSigs) + + +-- | Implementation of show_coverage tool +showCoverageTool :: ToolExecution +showCoverageTool args env _ _ = do + let contractName = Data.Maybe.fromMaybe "" (lookup "contract" args) + if T.null contractName + then return "Error: No contract name provided" + else do + let dapp = env.dapp + let matches = Map.filterWithKey (\k _ -> k == contractName || (":" <> contractName) `T.isSuffixOf` k) dapp.solcByName + case Map.toList matches of + [] -> return $ printf "Error: Contract '%s' not found" (unpack contractName) + [(k, solc)] -> do + covMap <- mergeCoverageMaps dapp env.coverageRefInit env.coverageRefRuntime + let sc = env.sourceCache + + -- Identify relevant files: only the file defining the contract + let relevantFiles = Set.singleton $ unpack $ T.dropEnd 1 $ fst $ T.breakOnEnd ":" k + + -- Use all active contracts to generate coverage + -- This allows showing coverage for a parent contract (e.g. EchidnaTest) + -- derived from the execution of a child contract (e.g. Echidna). + let activeContracts = filter (\c -> c.runtimeCodehash `Map.member` covMap) (Map.elems dapp.solcByName) + -- If no contracts are active (e.g. no coverage yet), use the requested contract to at least show the source + let contractsToUse = if null activeContracts then [solc] else activeContracts + + -- Generate full report using all active contracts, then filter by relevant files + let fullReport = ppCoveredCode Txt sc contractsToUse covMap Nothing "" [] + let filterReport text = + let ls = T.lines text + splitSections [] = [] + splitSections (l:rest) = + let (content, next) = span (" " `T.isPrefixOf`) rest + in (l:content) : splitSections next + sections = splitSections ls + keepSection (header:content) = + if unpack header `Set.member` relevantFiles + then header : content + else [] + keepSection [] = [] + in T.unlines $ concatMap keepSection sections + + return $ "```\n" ++ unpack (filterReport fullReport) ++ "\n```" + candidates -> return $ printf "Error: Ambiguous contract name '%s'. Found: %s" (unpack contractName) (unpack $ T.intercalate ", " $ map fst candidates) + +-- | Registry of available tools +availableTools :: [IORef WorkerState] -> IORef StatusState -> [Tool] +availableTools workerRefs statusRef = + [ Tool "status" "Show fuzzing campaign status" (statusTool workerRefs statusRef) + , Tool "target" "Show the name and the ABI of the target contract" targetTool + , Tool "reload_corpus" "Reload the transactions from the corpus, but without replay them" reloadCorpusTool + , Tool "dump_lcov" "Dump coverage in LCOV format" dumpLcovTool + , Tool "inject_fuzz_transactions" "Inject a sequence of transaction to fuzz with optional concrete arguments" fuzzTransactionTool + , Tool "clear_fuzz_priorities" "Clear the function prioritization list used in fuzzing" clearPrioritiesTool + --, Tool "read_logs" "Read the last 100 log messages" readLogsTool + , Tool "show_coverage" "Show coverage report for a particular contract" showCoverageTool + ] + +-- | Run the MCP Server +runMCPServer :: Env -> [IORef WorkerState] -> Int -> IORef [Text] -> IO () +runMCPServer env workerRefs port logsRef = do + statusRef <- newIORef (StatusState Nothing []) + + -- Spawn listener for coverage events + myBus <- atomically $ dupTChan env.bus + _ <- forkIO $ forever $ do + msg <- atomically $ readTChan myBus + case msg of + WrappedMessage _ (Broadcast (NewCoverageInfo _ txs isReplaying)) -> do + unless isReplaying $ do + now <- getCurrentTime + let funcNames = map getFunctionName txs + lastFunc = if null funcNames then "unknown" else last funcNames + + modifyIORef' statusRef $ \st -> st + { lastCoverageTime = Just now + , coveredFunctions = take 10 (lastFunc : st.coveredFunctions) + } + _ -> return () + + let toolsList = availableTools workerRefs statusRef + + let httpConfig = HttpConfig + { httpPort = port + , httpHost = "127.0.0.1" + , httpEndpoint = "/mcp" + , httpVerbose = False + } + + let serverInfo = McpServerInfo + { serverName = "Echidna MCP Server" + , serverVersion = "1.0.0" + , serverInstructions = "Echidna Agent Interface. Available tools: status, target, reload_corpus, dump_lcov, inject_fuzz_transactions, clear_fuzz_priorities, show_coverage" + } + + let mkToolDefinition :: Tool -> ToolDefinition + mkToolDefinition t = ToolDefinition + { toolDefinitionName = pack t.toolName + , toolDefinitionDescription = pack t.toolDescription + , toolDefinitionInputSchema = case t.toolName of + "dump_lcov" -> InputSchemaDefinitionObject + { properties = [] + , required = [] + } + "target" -> InputSchemaDefinitionObject + { properties = [] + , required = [] + } + "inject_fuzz_transactions" -> InputSchemaDefinitionObject + { properties = [("transactions", InputSchemaDefinitionProperty "string" "The transaction sequence string separated by ';' (e.g. 'func1();func2(arg1, ?)')")] + , required = ["transactions"] + } + "clear_fuzz_priorities" -> InputSchemaDefinitionObject + { properties = [] + , required = [] + } + "show_coverage" -> InputSchemaDefinitionObject + { properties = [("contract", InputSchemaDefinitionProperty "string" "The name of the contract")] + , required = ["contract"] + } + --"read_logs" -> InputSchemaDefinitionObject + -- { properties = [] + -- , required = [] + -- } + "status" -> InputSchemaDefinitionObject + { properties = [] + , required = [] + } + "reload_corpus" -> InputSchemaDefinitionObject + { properties = [] + , required = [] + } + _ -> InputSchemaDefinitionObject + { properties = [] + , required = [] + } + , toolDefinitionTitle = Nothing + , toolDefinitionMeta = Nothing + } + + let toolDefs = map mkToolDefinition toolsList + + let handleToolCall :: ToolName -> [(ArgumentName, ArgumentValue)] -> IO (Either Error Content) + handleToolCall name args = do + case find (\t -> pack t.toolName == name) toolsList of + Nothing -> return $ Left $ UnknownTool name + Just tool -> do + result <- tool.execute args env env.bus logsRef + return $ Right $ ContentText $ pack result + + let handlers = McpServerHandlers + { prompts = Nothing + , resources = Nothing + , tools = Just (return toolDefs, handleToolCall) + } + + runMcpServerHttpWithConfig httpConfig serverInfo handlers diff --git a/lib/Echidna/Output/Source.hs b/lib/Echidna/Output/Source.hs index 66f757bcf..b38d9e9d1 100644 --- a/lib/Echidna/Output/Source.hs +++ b/lib/Echidna/Output/Source.hs @@ -90,6 +90,24 @@ coverageFileExtension Lcov = ".lcov" coverageFileExtension Html = ".html" coverageFileExtension Txt = ".txt" +-- | Save only LCOV coverage triggered by HTTP hook, with timestamp in filename +saveLcovHook + :: Env + -> FilePath + -> SourceCache + -> [SolcContract] + -> IO FilePath +saveLcovHook env d sc cs = do + coverage <- mergeCoverageMaps env.dapp env.coverageRefInit env.coverageRefRuntime + currentTime <- getCurrentTime + let timestamp = formatTime defaultTimeLocale "%Y%m%d_%H%M%S" currentTime + fn = d "hook_" <> timestamp <> ".lcov" + excludePatterns = env.cfg.campaignConf.coverageExcludes + cc = ppCoveredCode Lcov sc cs coverage Nothing (T.pack timestamp) excludePatterns + createDirectoryIfMissing True d + writeFile fn cc + pure fn + -- | Pretty-print the covered code ppCoveredCode :: CoverageFileType -> SourceCache -> [SolcContract] -> FrozenCoverageMap -> Maybe Text -> Text -> [Text] -> Text ppCoveredCode fileType sc cs s projectName timestamp excludePatterns @@ -148,10 +166,9 @@ markLines fileType codeLines runtimeLines resultMap = cssClass = if n `elem` runtimeLines then getCSSClass markers else "n" -- fallback to 'neutral' class. result = case fileType of Lcov -> pack $ printf "DA:%d,%d" n (length results) - _ -> pack $ printf " %*d | %-4s| %s" lineNrSpan n markers (wrapLine codeLine) + _ -> pack $ printf " %-4s %s" markers (wrapLine codeLine) in result - lineNrSpan = length . show $ V.length codeLines + 1 getCSSClass :: String -> Text getCSSClass markers = diff --git a/lib/Echidna/Pretty.hs b/lib/Echidna/Pretty.hs index c9415e5a0..6994b8f6f 100644 --- a/lib/Echidna/Pretty.hs +++ b/lib/Echidna/Pretty.hs @@ -10,7 +10,7 @@ import EVM.Types (Addr) import Echidna.ABI (ppAbiValue) import Echidna.Types.Signature (SolCall) -import Echidna.Types.Tx (TxCall(..)) +import Echidna.Types.Tx (TxCall(..), Tx(..)) -- | Pretty-print some 'AbiCall'. ppSolCall :: Map Addr Text -> SolCall -> String @@ -24,3 +24,7 @@ ppTxCall _ (SolCreate _) = "" ppTxCall labels (SolCall x) = ppSolCall labels x ppTxCall _ NoCall = "*wait*" ppTxCall _ (SolCalldata x) = BSC8.unpack $ "0x" <> BS16.encode x + +-- | Pretty-print some 'Tx' +ppTx :: Map Addr Text -> Tx -> String +ppTx labels tx = ppTxCall labels (tx.call) diff --git a/lib/Echidna/Server.hs b/lib/Echidna/Server.hs index 60cf57d73..271b20f4f 100644 --- a/lib/Echidna/Server.hs +++ b/lib/Echidna/Server.hs @@ -36,6 +36,10 @@ instance ToJSON SSE where object [ "timestamp" .= time , "filename" .= filename ] + toJSON (SSE (time, ServerLog msg)) = + object [ "timestamp" .= time + , "data" .= msg + ] runSSEServer :: MVar () -> Env -> Word16 -> Int -> IO () runSSEServer serverStopVar env port nworkers = do @@ -52,12 +56,14 @@ runSSEServer serverStopVar env port nworkers = do TestOptimized _ -> "test_optimized" NewCoverage {} -> "new_coverage" SymExecLog _ -> "sym_exec_log" + Log _ -> "log" SymExecError _ -> "sym_exec_error" TxSequenceReplayed {} -> "tx_sequence_replayed" TxSequenceReplayFailed {} -> "tx_sequence_replay_failed" WorkerStopped _ -> "worker_stopped" Failure _err -> "failure" ReproducerSaved _ -> "saved_reproducer" + ServerLog _ -> "server_log" let serverEvent = ServerEvent { eventName = Just (eventName campaignEvent) diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs index fb13c636e..abbf51722 100644 --- a/lib/Echidna/Test.hs +++ b/lib/Echidna/Test.hs @@ -52,7 +52,7 @@ createTest m = EchidnaTest Open m v [] Stop Nothing Nothing validateTestModeError :: String validateTestModeError = - "Invalid test mode (should be property, assertion, dapptest, optimization, overflow or exploration)" + "Invalid test mode (should be property, assertion, dapptest, optimization, overflow, exploration or verify)" validateTestMode :: String -> TestMode validateTestMode s = case s of @@ -62,12 +62,17 @@ validateTestMode s = case s of "exploration" -> s "overflow" -> s "optimization" -> s + "verification" -> s _ -> error validateTestModeError isAssertionMode :: TestMode -> Bool isAssertionMode "assertion" = True isAssertionMode _ = False +isVerificationMode :: TestMode -> Bool +isVerificationMode "verification" = True +isVerificationMode _ = False + isExplorationMode :: TestMode -> Bool isExplorationMode "exploration" = True isExplorationMode _ = False @@ -99,6 +104,8 @@ createTests m td ts r ss = case m of "assertion" -> map (\s -> createTest (AssertionTest False s r)) (filter (/= fallback) ss) ++ [createTest (CallTest "AssertionFailed(..)" checkAssertionTest)] + "verification" -> + map (\s -> createTest (AssertionTest False s r)) (filter (/= fallback) ss) "dapptest" -> map (\s -> createTest (AssertionTest True s r)) (filter (\(n, xs) -> T.isPrefixOf "invariant_" n || not (null xs)) ss) diff --git a/lib/Echidna/Transaction.hs b/lib/Echidna/Transaction.hs index 2d9b37286..06a02a4f9 100644 --- a/lib/Echidna/Transaction.hs +++ b/lib/Echidna/Transaction.hs @@ -3,12 +3,13 @@ module Echidna.Transaction where -import Control.Monad (join, when) +import Control.Monad (join, when, zipWithM) import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad.Random.Strict (MonadRandom, getRandomR, uniform) import Control.Monad.Reader (MonadReader, ask) import Control.Monad.State.Strict (MonadState, gets, modify', execState) import Data.ByteString qualified as BS +import qualified Data.List.NonEmpty as NE import Data.Map (Map, toList) import Data.Maybe (catMaybes) import Data.Set (Set) @@ -17,8 +18,9 @@ import Data.Vector qualified as V import Optics.Core import Optics.State.Operators +import Data.Text (Text) import EVM (ceilDiv, initialContract, loadContract, resetState) -import EVM.ABI (abiValueType) +import EVM.ABI (abiValueType, AbiValue) import EVM.FeeSchedule (FeeSchedule(..)) import EVM.Transaction (setupTx) import EVM.Types hiding (Env, Gas, VMOpts(timestamp, gasprice)) @@ -68,8 +70,65 @@ genTx world deployedContracts = do sigMap <- getSignatures world.highSignatureMap world.lowSignatureMap sender <- rElem' world.senders contractAList <- liftIO $ mapM (toContractA env sigMap) (toList deployedContracts) - (dstAddr, dstAbis) <- rElem' $ Set.fromList $ catMaybes contractAList - solCall <- genInteractionsM genDict dstAbis + let allContracts = catMaybes contractAList + + (addr, sigs) <- rElem' $ Set.fromList allContracts + solCall <- genInteractionsM genDict sigs + + value <- genValue txConf.maxValue genDict.dictValues world.payableSigs solCall + ts <- (,) <$> genDelay txConf.maxTimeDelay genDict.dictValues + <*> genDelay txConf.maxBlockDelay genDict.dictValues + pure $ Tx { call = SolCall solCall + , src = sender + , dst = addr + , gas = txConf.txGas + , gasprice = txConf.maxGasprice + , value = value + , delay = level ts + } + where + toContractA :: Env -> SignatureMap -> (Expr EAddr, Contract) -> IO (Maybe ContractA) + toContractA env sigMap (addr, c) = + fmap (forceAddr addr,) . snd <$> lookupUsingCodehash env.codehashMap c env.dapp sigMap + +genTxFromPrototype + :: (MonadIO m, MonadRandom m, MonadState WorkerState m, MonadReader Env m) + => World + -> Map (Expr EAddr) Contract + -> (Text, [Maybe AbiValue]) + -> m Tx +genTxFromPrototype world deployedContracts (pName, pArgs) = do + env <- ask + let txConf = env.cfg.txConf + genDict <- gets (.genDict) + sigMap <- getSignatures world.highSignatureMap world.lowSignatureMap + sender <- rElem' world.senders + contractAList <- liftIO $ mapM (toContractA env sigMap) (toList deployedContracts) + let allContracts = catMaybes contractAList + + -- Find contracts containing this function with matching arity + let isMatch (_, sigs) = any (\(n, ts) -> n == pName && length ts == length pArgs) sigs + matchingContracts = filter isMatch allContracts + + (dstAddr, solCall) <- if null matchingContracts + then do + -- Fallback if not found: random tx + (addr, sigs) <- rElem' $ Set.fromList allContracts + call <- genInteractionsM genDict sigs + pure (addr, call) + else do + (addr, sigs) <- rElem' $ Set.fromList matchingContracts + -- Pick the matching signature + let matchingSigs = NE.filter (\(n, ts) -> n == pName && length ts == length pArgs) sigs + (name, types) <- rElem (NE.fromList matchingSigs) + + -- Generate arguments + let genArg (Just val) _ = pure val + genArg Nothing t = genAbiValueM' genDict name 0 t + + vals <- zipWithM genArg pArgs types + pure (addr, (name, vals)) + value <- genValue txConf.maxValue genDict.dictValues world.payableSigs solCall ts <- (,) <$> genDelay txConf.maxTimeDelay genDict.dictValues <*> genDelay txConf.maxBlockDelay genDict.dictValues diff --git a/lib/Echidna/Types/Agent.hs b/lib/Echidna/Types/Agent.hs new file mode 100644 index 000000000..8848a463c --- /dev/null +++ b/lib/Echidna/Types/Agent.hs @@ -0,0 +1,9 @@ +module Echidna.Types.Agent where + +import Echidna.Types.Config (Env) +import Echidna.Types.InterWorker + +-- | The Agent Typeclass +class Show a => Agent a where + getAgentId :: a -> AgentId + runAgent :: a -> Bus -> Env -> IO () diff --git a/lib/Echidna/Types/Campaign.hs b/lib/Echidna/Types/Campaign.hs index 77dce6564..410eb1362 100644 --- a/lib/Echidna/Types/Campaign.hs +++ b/lib/Echidna/Types/Campaign.hs @@ -6,6 +6,7 @@ import Data.Word (Word8, Word16) import GHC.Conc (numCapabilities) import EVM.Solvers (Solver(..)) +import EVM.ABI (AbiValue) import Echidna.ABI (GenDict, emptyDict) import Echidna.Types @@ -86,6 +87,8 @@ data WorkerState = WorkerState , runningThreads :: [ThreadId] -- ^ Extra threads currently being run, -- aside from the main worker thread + , prioritizedSequences :: ![(Double, [(Text, [Maybe AbiValue])])] + -- ^ Sequences of functions to prioritize during fuzzing } initialWorkerState :: WorkerState @@ -97,6 +100,7 @@ initialWorkerState = , ncalls = 0 , totalGas = 0 , runningThreads = [] + , prioritizedSequences = [] } defaultTestLimit :: Int diff --git a/lib/Echidna/Types/Config.hs b/lib/Echidna/Types/Config.hs index 536191e6d..a449ae6d5 100644 --- a/lib/Echidna/Types/Config.hs +++ b/lib/Echidna/Types/Config.hs @@ -4,12 +4,14 @@ import Control.Concurrent (Chan) import Data.Aeson.Key (Key) import Data.IORef (IORef) import Data.Set (Set) +import Echidna.Types.InterWorker (Bus) import Data.Text (Text) import Data.Time (LocalTime) import Data.Word (Word64) import EVM.Dapp (DappInfo) import EVM.Fetch qualified as Fetch +import EVM.Solidity (SourceCache) import EVM.Types (Addr, W256) import Echidna.SourceAnalysis.Slither (SlitherInfo) @@ -70,10 +72,12 @@ data EConfigWithUsage = EConfigWithUsage data Env = Env { cfg :: EConfig , dapp :: DappInfo + , sourceCache :: SourceCache -- | Shared between all workers. Events are fairly rare so contention is -- minimal. , eventQueue :: Chan (LocalTime, CampaignEvent) + , bus :: Bus , testRefs :: [IORef EchidnaTest] , coverageRefInit :: IORef CoverageMap diff --git a/lib/Echidna/Types/InterWorker.hs b/lib/Echidna/Types/InterWorker.hs new file mode 100644 index 000000000..6487ce923 --- /dev/null +++ b/lib/Echidna/Types/InterWorker.hs @@ -0,0 +1,60 @@ +module Echidna.Types.InterWorker where + +import Control.Concurrent.STM +import Data.Text (Text) + +import EVM.ABI (AbiValue) +import Echidna.Types.Tx (Tx) +import Echidna.Types.Test (EchidnaTest) + +-- | Agent Identities +data AgentId = FuzzerId Int | SymbolicId | AIId + deriving (Show, Eq, Ord) + +-- | Fuzzer specific commands +data FuzzerCmd + = DumpLcov + | SolutionFound [Tx] + | FuzzSequence [(Text, [Maybe AbiValue])] Double + | ClearPrioritization + | ExecuteSequence [Tx] (Maybe (TMVar Bool)) + +instance Show FuzzerCmd where + show DumpLcov = "DumpLcov" + show (SolutionFound txs) = "SolutionFound " ++ show txs + show (FuzzSequence s p) = "FuzzSequence " ++ show s ++ " (" ++ show p ++ ")" + show ClearPrioritization = "ClearPrioritization" + show (ExecuteSequence txs _) = "ExecuteSequence " ++ show txs + +-- | Symbolic specific commands +newtype SymbolicCmd + = SolveThis [Tx] + deriving (Show) + +-- | Message Protocol +data Message + = Broadcast BroadcastMsg + | ToFuzzer Int FuzzerCmd + | ToSymbolic SymbolicCmd + | Request RequestMsg + deriving (Show) + +data BroadcastMsg + = NewCoverageInfo Int [Tx] Bool -- points, transactions, isReplaying + | FoundBug EchidnaTest + | StrategyUpdate Text + | WorkerStopped AgentId + deriving (Show) + +data RequestMsg + = HelpMe + deriving (Show) + +-- | Message Envelope +data WrappedMessage = WrappedMessage + { from :: AgentId + , content :: Message + } deriving (Show) + +-- | Shared Communication Bus +type Bus = TChan WrappedMessage diff --git a/lib/Echidna/Types/Worker.hs b/lib/Echidna/Types/Worker.hs index be56a7c62..8bc9ff7c5 100644 --- a/lib/Echidna/Types/Worker.hs +++ b/lib/Echidna/Types/Worker.hs @@ -11,6 +11,7 @@ data CampaignEvent = WorkerEvent WorkerId WorkerType WorkerEvent | Failure String | ReproducerSaved String -- filename + | ServerLog String data WorkerEvent = TestFalsified !EchidnaTest @@ -18,6 +19,7 @@ data WorkerEvent | NewCoverage { points :: !Int, numCodehashes :: !Int, corpusSize :: !Int, transactions :: [Tx] } | SymExecError !String | SymExecLog !String + | Log !String | TxSequenceReplayed FilePath !Int !Int | TxSequenceReplayFailed FilePath Tx | WorkerStopped WorkerStopReason @@ -34,4 +36,3 @@ data WorkerStopReason | Killed !String | Crashed !String deriving Show - diff --git a/lib/Echidna/UI.hs b/lib/Echidna/UI.hs index dca6f9ad2..1cb4c6412 100644 --- a/lib/Echidna/UI.hs +++ b/lib/Echidna/UI.hs @@ -6,7 +6,6 @@ import Brick import Brick.BChan import Brick.Widgets.Dialog qualified as B import Control.Concurrent (killThread, threadDelay) -import Control.Concurrent.MVar (readMVar) import Control.Exception (AsyncException) import Control.Monad import Control.Monad.Catch @@ -15,9 +14,9 @@ import Control.Monad.State.Strict hiding (state) import Data.ByteString.Lazy qualified as BS import Data.List.Split (chunksOf) import Data.Map (Map) -import Data.Maybe (isJust, mapMaybe) +import Data.Maybe (mapMaybe) import Data.Sequence ((|>)) -import Data.Text (Text) +import Data.Text (Text, pack) import Data.Time import Graphics.Vty qualified as Vty import Graphics.Vty.Config (VtyUserConfig, defaultConfig, configInputMap) @@ -26,17 +25,20 @@ import Graphics.Vty.Input.Events import System.Console.ANSI (hNowSupportsANSI) import System.Signal import UnliftIO - ( MonadUnliftIO, IORef, newIORef, readIORef, hFlush, stdout , writeIORef, timeout) + ( MonadUnliftIO, IORef, newIORef, readIORef, hFlush, stdout , writeIORef, timeout, atomicModifyIORef') import UnliftIO.Concurrent hiding (killThread, threadDelay) import EVM.Fetch qualified import EVM.Types (Addr, Contract, VM, VMType(Concrete), W256) import Echidna.ABI -import Echidna.Campaign (runWorker, spawnListener) +import Echidna.Campaign (spawnListener) import Echidna.Output.Corpus (saveCorpusEvent) import Echidna.Output.JSON qualified -import Echidna.Server (runSSEServer) +import Echidna.Types.Agent (runAgent) +import Echidna.Agent.Fuzzer (FuzzerAgent(..)) +import Echidna.Agent.Symbolic (SymbolicAgent(..)) +import Echidna.MCP (runMCPServer) import Echidna.SourceAnalysis.Slither (isEmptySlitherInfo) import Echidna.Types.Campaign import Echidna.Types.Config @@ -48,7 +50,7 @@ import Echidna.Types.Worker import Echidna.UI.Report import Echidna.UI.Widgets import Echidna.Utility (timePrefix, getTimestamp) -import Echidna.Worker (getNWorkers, workerIDToType) +import Echidna.Worker (getNWorkers, workerIDToType, pushCampaignEvent) data UIEvent = CampaignUpdated LocalTime [EchidnaTest] [WorkerState] @@ -96,15 +98,27 @@ ui vm dict initialCorpus cliSelectedContract = do corpusSaverStopVar <- spawnListener (saveCorpusEvent env) workers <- forM (zip corpusChunks [0..(nworkers-1)]) $ - uncurry (spawnWorker env perWorkerTestLimit) + liftIO . uncurry (spawnWorker env perWorkerTestLimit) case effectiveMode of Interactive -> do -- Channel to push events to update UI uiChannel <- liftIO $ newBChan 1000 - let forwardEvent = void . writeBChanNonBlocking uiChannel . EventReceived + logBuffer <- newIORef [] + + let forwardEvent ev = do + msg <- runReaderT (ppLogLine vm ev) env + liftIO $ atomicModifyIORef' logBuffer (\logs -> (pack msg : logs, ())) + void $ writeBChanNonBlocking uiChannel $ EventReceived ev + uiEventsForwarderStopVar <- spawnListener forwardEvent + case conf.campaignConf.serverPort of + Just port -> do + liftIO $ pushCampaignEvent env (ServerLog ("MCP Server running at http://127.0.0.1:" ++ show port ++ "/mcp")) + void $ liftIO $ forkIO $ runMCPServer env (map snd workers) (fromIntegral port) logBuffer + Nothing -> pure () + ticker <- liftIO . forkIO . forever $ do threadDelay 200_000 -- 200 ms @@ -179,7 +193,12 @@ ui vm dict initialCorpus cliSelectedContract = do void $ tryPutMVar serverStopVar () in installHandler sig handler - let forwardEvent ev = putStrLn =<< runReaderT (ppLogLine vm ev) env + logBuffer <- newIORef [] + + let forwardEvent ev = do + msg <- runReaderT (ppLogLine vm ev) env + liftIO $ atomicModifyIORef' logBuffer (\logs -> (pack msg : logs, ())) + putStrLn msg uiEventsForwarderStopVar <- spawnListener forwardEvent -- Track last update time and gas for delta calculation @@ -190,11 +209,15 @@ ui vm dict initialCorpus cliSelectedContract = do states <- liftIO $ workerStates workers time <- timePrefix <$> getTimestamp line <- statusLine env states lastUpdateRef - putStrLn $ time <> "[status] " <> line + let statusMsg = time <> "[status] " <> line + putStrLn statusMsg hFlush stdout + liftIO $ atomicModifyIORef' logBuffer (\logs -> (pack statusMsg : logs, ())) case conf.campaignConf.serverPort of - Just port -> liftIO $ runSSEServer serverStopVar env port nworkers + Just port -> do + liftIO $ pushCampaignEvent env (ServerLog ("MCP Server running at http://127.0.0.1:" ++ show port ++ "/mcp")) + void $ liftIO $ forkIO $ runMCPServer env (map snd workers) (fromIntegral port) logBuffer Nothing -> pure () ticker <- liftIO . forkIO . forever $ do @@ -209,11 +232,6 @@ ui vm dict initialCorpus cliSelectedContract = do -- print final status regardless of the last scheduled update liftIO printStatus - when (isJust conf.campaignConf.serverPort) $ do - -- wait until we send all SSE events - liftIO $ putStrLn "Waiting until all SSE are received..." - liftIO $ Control.Concurrent.MVar.readMVar serverStopVar - states <- liftIO $ workerStates workers case outputFormat of @@ -229,27 +247,37 @@ ui vm dict initialCorpus cliSelectedContract = do spawnWorker env testLimit corpusChunk workerId = do stateRef <- newIORef initialWorkerState + let bus = env.bus threadId <- forkIO $ do -- TODO: maybe figure this out with forkFinally? let workerType = workerIDToType env.cfg.campaignConf workerId - stopReason <- catches (do + maybeStopReason <- catches (do let timeoutUsecs = maybe (-1) (*1_000_000) env.cfg.uiConf.maxTime corpus = if workerType == SymbolicWorker then initialCorpus else corpusChunk - maybeResult <- timeout timeoutUsecs $ - runWorker workerType (get >>= writeIORef stateRef) - vm dict workerId corpus testLimit cliSelectedContract + + maybeResult <- timeout timeoutUsecs $ case workerType of + FuzzWorker -> do + let agent = FuzzerAgent workerId vm dict corpus testLimit stateRef + runAgent agent bus env + SymbolicWorker -> do + let agent = SymbolicAgent vm dict corpus cliSelectedContract stateRef + runAgent agent bus env + pure $ case maybeResult of - Just (stopReason, _finalState) -> stopReason - Nothing -> TimeLimitReached + Just () -> Nothing -- Agent finished and pushed event + Nothing -> Just TimeLimitReached ) - [ Handler $ \(e :: AsyncException) -> pure $ Killed (show e) - , Handler $ \(e :: SomeException) -> pure $ Crashed (show e) + [ Handler $ \(e :: AsyncException) -> pure $ Just (Killed (show e)) + , Handler $ \(e :: SomeException) -> pure $ Just (Crashed (show e)) ] - time <- liftIO getTimestamp - writeChan env.eventQueue (time, WorkerEvent workerId workerType (WorkerStopped stopReason)) + case maybeStopReason of + Just stopReason -> do + time <- liftIO getTimestamp + liftIO $ writeChan env.eventQueue (time, WorkerEvent workerId workerType (WorkerStopped stopReason)) + Nothing -> pure () pure (threadId, stateRef) diff --git a/lib/Echidna/UI/Report.hs b/lib/Echidna/UI/Report.hs index 2733c20da..61438ca75 100644 --- a/lib/Echidna/UI/Report.hs +++ b/lib/Echidna/UI/Report.hs @@ -34,6 +34,8 @@ ppLogLine vm (time, event@(WorkerEvent workerId FuzzWorker _)) = ((timePrefix time <> "[Worker " <> show workerId <> "] ") <>) <$> ppCampaignEventLog vm event ppLogLine vm (time, event@(WorkerEvent workerId SymbolicWorker _)) = ((timePrefix time <> "[Worker " <> show workerId <> ", symbolic] ") <>) <$> ppCampaignEventLog vm event +ppLogLine vm (time, event@(ServerLog _)) = + ((timePrefix time <> "[Server] ") <>) <$> ppCampaignEventLog vm event ppLogLine vm (time, event) = ((timePrefix time <> " ") <>) <$> ppCampaignEventLog vm event diff --git a/lib/Echidna/Worker.hs b/lib/Echidna/Worker.hs index 5e0ec5766..4fbc8a9a8 100644 --- a/lib/Echidna/Worker.hs +++ b/lib/Echidna/Worker.hs @@ -6,6 +6,7 @@ import Control.Monad.State.Strict(MonadState(..), gets) import Data.Aeson import Data.Text (unpack) +import Echidna.Types.Tx (Tx(..), TxCall(..)) import Echidna.ABI (encodeSig) import Echidna.Types.Campaign import Echidna.Types.Config (Env(..), EConfig(..)) @@ -28,6 +29,7 @@ instance ToJSON WorkerEvent where object [ "coverage" .= points, "contracts" .= numCodehashes, "corpus_size" .= corpusSize] SymExecError msg -> object [ "msg" .= msg ] SymExecLog msg -> object [ "msg" .= msg ] + Log msg -> object [ "msg" .= msg ] TxSequenceReplayed file current total -> object [ "file" .= file, "current" .= current, "total" .= total ] TxSequenceReplayFailed file tx -> @@ -54,6 +56,7 @@ ppCampaignEvent = \case WorkerEvent _ _ e -> ppWorkerEvent e Failure err -> err ReproducerSaved f -> "Saved reproducer to " <> f + ServerLog msg -> msg ppWorkerEvent :: WorkerEvent -> String ppWorkerEvent = \case @@ -62,14 +65,23 @@ ppWorkerEvent = \case TestOptimized test -> let name = case test.testType of OptimizationTest n _ -> n; _ -> error "fixme" in "New maximum value of " <> unpack name <> ": " <> show test.value - NewCoverage { points, numCodehashes, corpusSize } -> - "New coverage: " <> show points <> " instr, " + NewCoverage { points, numCodehashes, corpusSize, transactions } -> + let funcName = case reverse transactions of + (tx:_) -> case tx.call of + SolCall (name, _) -> unpack name + SolCreate _ -> "constructor" + SolCalldata _ -> "fallback" + NoCall -> "no call" + [] -> "init" + in "New coverage: " <> show points <> " instr, " <> show numCodehashes <> " contracts, " - <> show corpusSize <> " seqs in corpus" + <> show corpusSize <> " seqs in corpus (" <> funcName <> ")" SymExecError err -> "Symbolic execution failed: " <> err SymExecLog msg -> "Symbolic execution log: " <> msg + Log msg -> + msg TxSequenceReplayed file current total -> "Sequence replayed from corpus file " <> file <> " (" <> show current <> "/" <> show total <> ")" TxSequenceReplayFailed file tx -> diff --git a/package.yaml b/package.yaml index 29a6a6431..5d1151154 100644 --- a/package.yaml +++ b/package.yaml @@ -59,6 +59,7 @@ library: - html-entities - http-conduit - ListLike + - mcp-server - mustache - optics - optics-core @@ -68,6 +69,7 @@ library: - semver - signal - split + - stm - strip-ansi-escape - time - unliftio @@ -123,6 +125,7 @@ tests: - process - semver - split + - stm - tasty - tasty-hunit - tasty-quickcheck diff --git a/src/Main.hs b/src/Main.hs index 5e5c15cc9..5335f91f7 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -54,7 +54,8 @@ main = withUtf8 $ withCP65001 $ do opts@Options{..} <- execParser optsParser EConfigWithUsage loadedCfg ks _ <- maybe (pure (EConfigWithUsage defaultConfig mempty mempty)) parseConfig cliConfigFilepath - cfg <- overrideConfig loadedCfg opts + cfg' <- overrideConfig loadedCfg opts + let cfg = adjustForVerificationMode cfg' printProjectName cfg.projectName diff --git a/src/test/Common.hs b/src/test/Common.hs index a9cb7eb26..ff5c6bdc4 100644 --- a/src/test/Common.hs +++ b/src/test/Common.hs @@ -22,6 +22,7 @@ module Common , gasConsumedGt ) where +import Control.Concurrent.STM (newBroadcastTChanIO) import Control.Monad (forM_) import Control.Monad.Random (getRandomR) import Control.Monad.Reader (runReaderT) @@ -42,10 +43,12 @@ import EVM.Solidity (Contracts(..), BuildOutput(..), SolcContract(..)) import EVM.Types hiding (Env, Gas) import Echidna (mkEnv, prepareContract) -import Echidna.Campaign (runWorker) +import Echidna.Agent.Fuzzer (FuzzerAgent(..)) +import Echidna.Agent.Symbolic (SymbolicAgent(..)) import Echidna.Config (parseConfig, defaultConfig) import Echidna.Solidity (selectMainContract, mkTests, loadSpecified, compileContracts) import Echidna.Test (checkETest) +import Echidna.Types.Agent (runAgent) import Echidna.Types.Campaign import Echidna.Types.Config (Env(..), EConfig(..), EConfigWithUsage(..)) import Echidna.Types.Signature (ContractName) @@ -95,8 +98,30 @@ runContract f selectedContract cfg workerType = do (vm, env, dict) <- prepareContract cfg (f :| []) buildOutput selectedContract seed - (_stopReason, finalState) <- flip runReaderT env $ - runWorker workerType (pure ()) vm dict 0 [] cfg.campaignConf.testLimit selectedContract + bus <- newBroadcastTChanIO + stateRef <- newIORef (error "WorkerState not initialized") + case workerType of + FuzzWorker -> do + let agent = FuzzerAgent + { fuzzerId = 0 + , initialVm = vm + , initialDict = dict + , initialCorpus = [] + , testLimit = cfg.campaignConf.testLimit + , stateRef = stateRef + } + runAgent agent bus env + SymbolicWorker -> do + let agent = SymbolicAgent + { initialVm = vm + , initialDict = dict + , initialCorpus = [] + , contractName = selectedContract + , stateRef = stateRef + } + runAgent agent bus env + + finalState <- readIORef stateRef -- TODO: consider snapshotting the state so checking functions don't need to -- be IO diff --git a/stack.yaml b/stack.yaml index 0059055f2..f5b012264 100644 --- a/stack.yaml +++ b/stack.yaml @@ -6,7 +6,9 @@ packages: extra-deps: - git: https://github.com/argotorg/hevm.git - commit: 5ec225475d5ba9cda24c5fb303acb76c88412553 + commit: 9ba5e52fc7ec7ae6f7f3a25d5ee426625d2aa9d3 +- git: https://github.com/gustavo-grieco/haskell-mcp-server.git + commit: 9fd60af428b96ae4bc63a133b3960ed934494189 - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162 diff --git a/tests/solidity/symbolic/verify.bitwuzla.yaml b/tests/solidity/symbolic/verify.bitwuzla.yaml index fe32d9ba7..e49c55483 100644 --- a/tests/solidity/symbolic/verify.bitwuzla.yaml +++ b/tests/solidity/symbolic/verify.bitwuzla.yaml @@ -1,5 +1,4 @@ -testMode: assertion -symExec: true +testMode: verification symExecSMTSolver: bitwuzla workers: 0 seqLen: 1 diff --git a/tests/solidity/symbolic/verify.yaml b/tests/solidity/symbolic/verify.yaml index 3ac1b6cdc..da7cc6af0 100644 --- a/tests/solidity/symbolic/verify.yaml +++ b/tests/solidity/symbolic/verify.yaml @@ -1,5 +1,4 @@ -testMode: assertion -symExec: true +testMode: verification symExecSMTSolver: z3 workers: 0 seqLen: 1