From 8750b78c0b824a60d2c3ef606c49f8f7a16beb58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emilio=20L=C3=B3pez?= Date: Tue, 30 Sep 2025 12:04:10 -0300 Subject: [PATCH 01/17] Upgrade `hevm` to `95b5e074c9f27f970011ed53f38f1643d70c3c8a` --- flake.nix | 4 ++-- lib/Echidna/Onchain.hs | 15 +++++++++++---- lib/Echidna/SymExec/Common.hs | 9 +++++---- lib/Echidna/SymExec/Exploration.hs | 2 +- lib/Echidna/SymExec/Verification.hs | 2 +- stack.yaml | 2 +- 6 files changed, 21 insertions(+), 13 deletions(-) diff --git a/flake.nix b/flake.nix index 6849fc447..44c71aa8d 100644 --- a/flake.nix +++ b/flake.nix @@ -54,8 +54,8 @@ (pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub { owner = "ethereum"; repo = "hevm"; - rev = "87fe0eec5abb69c0b54c097784dfd8712a36de70"; - sha256 = "sha256-cgfrP+K5NoXvVPRN6XRnTkdOIJztc/4wrto9nQ/9tnY="; + rev = "95b5e074c9f27f970011ed53f38f1643d70c3c8a"; + sha256 = "sha256-UqTg476msbyiDyy45dK1zYYbH4GiIE45R4wa0Nn2TUA="; }) { secp256k1 = pkgs.secp256k1; }) ([ pkgs.haskell.lib.compose.dontCheck diff --git a/lib/Echidna/Onchain.hs b/lib/Echidna/Onchain.hs index 8041632cc..89d15ce09 100644 --- a/lib/Echidna/Onchain.hs +++ b/lib/Echidna/Onchain.hs @@ -40,6 +40,7 @@ import Echidna.Types.Campaign (CampaignConf(..)) import Echidna.Types.Config (Env(..), EConfig(..)) import Echidna.Output.Source (saveCoverages) import Control.Monad (when, forM_) +import Control.Concurrent.MVar (newMVar) rpcUrlEnv :: IO (Maybe Text) rpcUrlEnv = do @@ -59,15 +60,21 @@ etherscanApiKey = do -- TODO: temporary solution, handle errors gracefully safeFetchContractFrom :: EVM.Fetch.BlockNumber -> Text -> Addr -> IO (Maybe Contract) safeFetchContractFrom rpcBlock rpcUrl addr = do - catch - (EVM.Fetch.fetchContractFrom defaultConfig rpcBlock rpcUrl addr) + catch (do + sess <- Session.newAPISession + let emptyCache = EVM.Fetch.FetchCache Map.empty Map.empty Map.empty + cache <- newMVar emptyCache + latestBlockNum <- newMVar Nothing + let session = EVM.Fetch.Session sess latestBlockNum cache + EVM.Fetch.fetchContractWithSession defaultConfig session rpcBlock rpcUrl addr) (\(_ :: HttpException) -> pure $ Just emptyAccount) -- TODO: temporary solution, handle errors gracefully safeFetchSlotFrom :: EVM.Fetch.BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256) safeFetchSlotFrom rpcBlock rpcUrl addr slot = - catch - (EVM.Fetch.fetchSlotFrom defaultConfig rpcBlock rpcUrl addr slot) + catch (do + sess <- Session.newAPISession + EVM.Fetch.fetchSlotWithSession sess rpcBlock rpcUrl addr slot) (\(_ :: HttpException) -> pure $ Just 0) data FetchedContractData = FetchedContractData diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs index 63ff788a3..b5fca2c0f 100644 --- a/lib/Echidna/SymExec/Common.hs +++ b/lib/Echidna/SymExec/Common.hs @@ -109,8 +109,8 @@ modelToTx dst oldTimestamp oldNumber method senders fallbackSender calldata resu r -> error ("Unexpected value in `modelToTx`: " ++ show r) -cachedOracle :: IORef ContractCache -> IORef SlotCache -> SolverGroup -> Fetch.RpcInfo -> Fetch.Fetcher t m s -cachedOracle contractCacheRef slotCacheRef solvers info q = do +cachedOracle :: IORef ContractCache -> IORef SlotCache -> SolverGroup -> Maybe Fetch.Session -> Fetch.RpcInfo -> Fetch.Fetcher t m s +cachedOracle contractCacheRef slotCacheRef solvers session info q = do case q of PleaseFetchContract addr _ continue -> do cache <- liftIO $ readIORef contractCacheRef @@ -124,7 +124,7 @@ cachedOracle contractCacheRef slotCacheRef solvers info q = do _ -> oracle q _ -> oracle q - where oracle = Fetch.oracle solvers info + where oracle = Fetch.oracle solvers session info rpcFetcher :: Functor f => f a -> Maybe W256 -> f (Fetch.BlockNumber, a) @@ -151,8 +151,9 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) [] let cd = fst calldataSym + session <- Fetch.mkSession let - fetcher = cachedOracle contractCacheRef slotCacheRef solvers rpcInfo + fetcher = cachedOracle contractCacheRef slotCacheRef solvers (Just session) rpcInfo dst = conf.solConf.contractAddr vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm let diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index 56f02279e..d70094761 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -99,7 +99,7 @@ exploreContract contract method vm = do resultChan <- liftIO newEmptyMVar let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = Naive} - let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive, dumpQueries = False, numCexFuzz = 0 } + let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive, dumpQueries = False } let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo} let runtimeEnv = defaultEnv { config = hevmConfig } pushWorkerEvent $ SymExecLog ("Exploring " <> (show method.name)) diff --git a/lib/Echidna/SymExec/Verification.hs b/lib/Echidna/SymExec/Verification.hs index 210f042a7..ebbbb03a9 100644 --- a/lib/Echidna/SymExec/Verification.hs +++ b/lib/Echidna/SymExec/Verification.hs @@ -64,7 +64,7 @@ verifyMethod method contract vm = do resultChan <- liftIO newEmptyMVar let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = Naive} - let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, dumpExprs = True, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive, numCexFuzz = 0 } + let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, dumpExprs = True, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive } let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo} let runtimeEnv = defaultEnv { config = hevmConfig } pushWorkerEvent $ SymExecLog ("Verifying " <> (show method.name)) diff --git a/stack.yaml b/stack.yaml index e72298b3a..bc55412f7 100644 --- a/stack.yaml +++ b/stack.yaml @@ -6,7 +6,7 @@ packages: extra-deps: - git: https://github.com/argotorg/hevm.git - commit: 87fe0eec5abb69c0b54c097784dfd8712a36de70 + commit: 95b5e074c9f27f970011ed53f38f1643d70c3c8a - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162 From ffdd9a60fabaebcb3eea6317433139b80494246c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emilio=20L=C3=B3pez?= Date: Tue, 30 Sep 2025 12:59:43 -0300 Subject: [PATCH 02/17] Refactor cache use after hevm upgrade --- lib/Echidna.hs | 15 +++-- lib/Echidna/Exec.hs | 90 +++++++++++------------------ lib/Echidna/Onchain.hs | 70 ++++++++-------------- lib/Echidna/SymExec/Common.hs | 29 ++-------- lib/Echidna/SymExec/Exploration.hs | 5 +- lib/Echidna/SymExec/Verification.hs | 5 +- lib/Echidna/Types/Config.hs | 4 +- lib/Echidna/UI.hs | 8 ++- 8 files changed, 87 insertions(+), 139 deletions(-) diff --git a/lib/Echidna.hs b/lib/Echidna.hs index edd0ddb4e..5f2dec47e 100644 --- a/lib/Echidna.hs +++ b/lib/Echidna.hs @@ -1,7 +1,10 @@ module Echidna where import Control.Concurrent (newChan) +import Control.Concurrent.MVar (newMVar) import Control.Monad.Catch (MonadThrow(..)) +import Control.Monad.IO.Class (liftIO) +import Network.Wreq.Session qualified as NetSession import Control.Monad.ST (RealWorld) import Data.IORef (newIORef) import Data.List (find, nub) @@ -15,6 +18,7 @@ import System.FilePath (()) import EVM (cheatCode) import EVM.ABI (AbiValue(AbiAddress)) import EVM.Dapp (dappInfo) +import EVM.Fetch qualified import EVM.Solidity (BuildOutput(..), Contracts(Contracts), Method(..), Mutability(..), SolcContract(..)) import EVM.Types hiding (Env) @@ -116,13 +120,16 @@ mkEnv cfg buildOutput tests world slitherInfo = do coverageRefRuntime <- newIORef mempty corpusRef <- newIORef mempty testRefs <- traverse newIORef tests - (contractCache, slotCache) <- Onchain.loadRpcCache cfg - fetchContractCache <- newIORef contractCache - fetchSlotCache <- newIORef slotCache + -- Create session manually since mkSession needs App context + sess <- liftIO NetSession.newAPISession + let emptyCache = EVM.Fetch.FetchCache Map.empty Map.empty Map.empty + cache <- liftIO $ newMVar emptyCache + latestBlockNum <- liftIO $ newMVar Nothing + let fetchSession = EVM.Fetch.Session sess latestBlockNum cache contractNameCache <- newIORef mempty -- TODO put in real path let dapp = dappInfo "/" buildOutput - pure $ Env { cfg, dapp, codehashMap, fetchContractCache, fetchSlotCache, contractNameCache + pure $ Env { cfg, dapp, codehashMap, fetchSession, contractNameCache , chainId, eventQueue, coverageRefInit, coverageRefRuntime, corpusRef, testRefs, world , slitherInfo } diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs index e2279e7d0..a96048ffc 100644 --- a/lib/Echidna/Exec.hs +++ b/lib/Echidna/Exec.hs @@ -113,68 +113,48 @@ execTxWith executeTx tx = do case getQuery vmResult of -- A previously unknown contract is required Just q@(PleaseFetchContract addr _ continuation) -> do - cacheRef <- asks (.fetchContractCache) - cache <- liftIO $ readIORef cacheRef - case Map.lookup addr cache of - Just (Just contract) -> fromEVM (continuation contract) - Just Nothing -> do - v <- get - v' <- liftIO $ stToIO $ execStateT (continuation emptyAccount) v - put v' - Nothing -> do - logMsg $ "INFO: Performing RPC: " <> show q - case config.rpcUrl of - Just rpcUrl -> do - ret <- liftIO $ safeFetchContractFrom rpcBlock rpcUrl addr - case ret of - -- TODO: fix hevm to not return an empty contract in case of an error - Just contract | contract.code /= RuntimeCode (ConcreteRuntimeCode "") -> do - fromEVM (continuation contract) - liftIO $ atomicWriteIORef cacheRef $ Map.insert addr (Just contract) cache - _ -> do - -- TODO: better error reporting in HEVM, when intermittent - -- network error then retry - liftIO $ atomicWriteIORef cacheRef $ Map.insert addr Nothing cache - logMsg $ "ERROR: Failed to fetch contract: " <> show q - -- TODO: How should we fail here? It could be a network error, - -- RPC server returning junk etc. - fromEVM (continuation emptyAccount) - Nothing -> do - liftIO $ atomicWriteIORef cacheRef $ Map.insert addr Nothing cache - logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q - -- TODO: How should we fail here? RPC is not configured but VM - -- wants to fetch + logMsg $ "INFO: Performing RPC: " <> show q + case config.rpcUrl of + Just rpcUrl -> do + session <- asks (.fetchSession) + ret <- liftIO $ safeFetchContractFrom session rpcBlock rpcUrl addr + case ret of + -- TODO: fix hevm to not return an empty contract in case of an error + Just contract | contract.code /= RuntimeCode (ConcreteRuntimeCode "") -> do + fromEVM (continuation contract) + _ -> do + -- TODO: better error reporting in HEVM, when intermittent + -- network error then retry + logMsg $ "ERROR: Failed to fetch contract: " <> show q + -- TODO: How should we fail here? It could be a network error, + -- RPC server returning junk etc. fromEVM (continuation emptyAccount) + Nothing -> do + logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q + -- TODO: How should we fail here? RPC is not configured but VM + -- wants to fetch + fromEVM (continuation emptyAccount) runFully -- resume execution -- A previously unknown slot is required Just q@(PleaseFetchSlot addr slot continuation) -> do - cacheRef <- asks (.fetchSlotCache) - cache <- liftIO $ readIORef cacheRef - case Map.lookup addr cache >>= Map.lookup slot of - Just (Just value) -> fromEVM (continuation value) - Just Nothing -> fromEVM (continuation 0) - Nothing -> do - logMsg $ "INFO: Performing RPC: " <> show q - case config.rpcUrl of - Just rpcUrl -> do - ret <- liftIO $ safeFetchSlotFrom rpcBlock rpcUrl addr slot - case ret of - Just value -> do - fromEVM (continuation value) - liftIO $ atomicWriteIORef cacheRef $ - Map.insertWith Map.union addr (Map.singleton slot (Just value)) cache - Nothing -> do - -- TODO: How should we fail here? It could be a network error, - -- RPC server returning junk etc. - logMsg $ "ERROR: Failed to fetch slot: " <> show q - liftIO $ atomicWriteIORef cacheRef $ - Map.insertWith Map.union addr (Map.singleton slot Nothing) cache - fromEVM (continuation 0) + logMsg $ "INFO: Performing RPC: " <> show q + case config.rpcUrl of + Just rpcUrl -> do + session <- asks (.fetchSession) + ret <- liftIO $ safeFetchSlotFrom session rpcBlock rpcUrl addr slot + case ret of + Just value -> do + fromEVM (continuation value) Nothing -> do - logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q - -- Use the zero slot + -- TODO: How should we fail here? It could be a network error, + -- RPC server returning junk etc. + logMsg $ "ERROR: Failed to fetch slot: " <> show q fromEVM (continuation 0) + Nothing -> do + logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q + -- Use the zero slot + fromEVM (continuation 0) runFully -- resume execution -- Execute a FFI call diff --git a/lib/Echidna/Onchain.hs b/lib/Echidna/Onchain.hs index 89d15ce09..11c2eaef9 100644 --- a/lib/Echidna/Onchain.hs +++ b/lib/Echidna/Onchain.hs @@ -40,7 +40,7 @@ import Echidna.Types.Campaign (CampaignConf(..)) import Echidna.Types.Config (Env(..), EConfig(..)) import Echidna.Output.Source (saveCoverages) import Control.Monad (when, forM_) -import Control.Concurrent.MVar (newMVar) +import Control.Concurrent.MVar (newMVar, readMVar) rpcUrlEnv :: IO (Maybe Text) rpcUrlEnv = do @@ -58,23 +58,17 @@ etherscanApiKey = do pure (Text.pack <$> val) -- TODO: temporary solution, handle errors gracefully -safeFetchContractFrom :: EVM.Fetch.BlockNumber -> Text -> Addr -> IO (Maybe Contract) -safeFetchContractFrom rpcBlock rpcUrl addr = do - catch (do - sess <- Session.newAPISession - let emptyCache = EVM.Fetch.FetchCache Map.empty Map.empty Map.empty - cache <- newMVar emptyCache - latestBlockNum <- newMVar Nothing - let session = EVM.Fetch.Session sess latestBlockNum cache - EVM.Fetch.fetchContractWithSession defaultConfig session rpcBlock rpcUrl addr) +safeFetchContractFrom :: EVM.Fetch.Session -> EVM.Fetch.BlockNumber -> Text -> Addr -> IO (Maybe Contract) +safeFetchContractFrom session rpcBlock rpcUrl addr = do + catch + (EVM.Fetch.fetchContractWithSession defaultConfig session rpcBlock rpcUrl addr) (\(_ :: HttpException) -> pure $ Just emptyAccount) -- TODO: temporary solution, handle errors gracefully -safeFetchSlotFrom :: EVM.Fetch.BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256) -safeFetchSlotFrom rpcBlock rpcUrl addr slot = - catch (do - sess <- Session.newAPISession - EVM.Fetch.fetchSlotWithSession sess rpcBlock rpcUrl addr slot) +safeFetchSlotFrom :: EVM.Fetch.Session -> EVM.Fetch.BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256) +safeFetchSlotFrom session rpcBlock rpcUrl addr slot = + catch + (EVM.Fetch.fetchSlotWithSession session.sess rpcBlock rpcUrl addr slot) (\(_ :: HttpException) -> pure $ Just 0) data FetchedContractData = FetchedContractData @@ -176,22 +170,9 @@ externalSolcContract env addr c = do -- TODO: This should happen continuously event-based saveRpcCache :: Env -> IO () -saveRpcCache env = do - contractsCache <- readIORef env.fetchContractCache - slotsCache <- readIORef env.fetchSlotCache - case env.cfg.campaignConf.corpusDir of - Nothing -> pure () - Just dir -> do - let cacheDir = dir "cache" - case env.cfg.rpcBlock of - Just block -> do - -- Save fetched data, it's okay to override as the cache only grows - JSON.encodeFile (cacheDir "block_" <> show block <> "_fetch_cache_contracts.json") - (toFetchedContractData <$> Map.mapMaybe id contractsCache) - JSON.encodeFile (cacheDir "block_" <> show block <> "_fetch_cache_slots.json") - slotsCache - Nothing -> - pure () +saveRpcCache _env = do + -- Cache saving is now handled automatically by hevm's session cache + pure () saveCoverageReport :: Env -> Int -> IO () saveCoverageReport env runId = do @@ -201,20 +182,19 @@ saveCoverageReport env runId = do -- coverage reports for external contracts, we only support -- Ethereum Mainnet for now when (env.chainId == Just 1) $ do - contractsCache <- readIORef env.fetchContractCache - forM_ (Map.toList contractsCache) $ \(addr, mc) -> - case mc of - Just contract -> do - r <- externalSolcContract env addr contract - case r of - Just (externalSourceCache, solcContract) -> do - let dir' = dir show addr - saveCoverages env - runId - dir' - externalSourceCache - [solcContract] - Nothing -> pure () + -- Get contracts from hevm session cache + sessionCache <- readMVar env.fetchSession.sharedCache + let contractsCache = sessionCache.contractCache + forM_ (Map.toList contractsCache) $ \(addr, contract) -> do + r <- externalSolcContract env addr contract + case r of + Just (externalSourceCache, solcContract) -> do + let dir' = dir show addr + saveCoverages env + runId + dir' + externalSourceCache + [solcContract] Nothing -> pure () fetchChainIdFrom :: Maybe Text -> IO (Maybe W256) diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs index b5fca2c0f..0aab3b644 100644 --- a/lib/Echidna/SymExec/Common.hs +++ b/lib/Echidna/SymExec/Common.hs @@ -7,7 +7,6 @@ import Data.Maybe (fromMaybe, mapMaybe) import Data.Set (Set) import Data.Set qualified as Set import Data.Text qualified as T -import GHC.IORef (IORef, readIORef) import Optics.Core ((.~), (%), (%~)) import EVM.ABI (abiKind, AbiKind(Dynamic), Sig(..), decodeBuf, AbiVals(..)) import EVM.Fetch qualified as Fetch @@ -17,7 +16,7 @@ import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..), WarningData( import EVM.Solvers (SolverGroup) import EVM.SymExec (mkCalldata, verifyInputs, VeriOpts(..), checkAssertions, subModel, defaultSymbolicValues) import EVM.Expr qualified -import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), Query(..), forceLit) +import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit) import qualified EVM.Types (VM(..)) import EVM.Format (formatPartialDetailed) import Control.Monad.ST (RealWorld) @@ -27,7 +26,6 @@ import Echidna.Types (fromEVM) import Echidna.Types.Config (EConfig(..)) import Echidna.Types.Solidity (SolConf(..)) import Echidna.Types.Tx (Tx(..), TxCall(..), TxConf(..), maxGasPerBlock) -import Echidna.Types.Cache (ContractCache, SlotCache) type PartialsLogs = [T.Text] @@ -109,22 +107,7 @@ modelToTx dst oldTimestamp oldNumber method senders fallbackSender calldata resu r -> error ("Unexpected value in `modelToTx`: " ++ show r) -cachedOracle :: IORef ContractCache -> IORef SlotCache -> SolverGroup -> Maybe Fetch.Session -> Fetch.RpcInfo -> Fetch.Fetcher t m s -cachedOracle contractCacheRef slotCacheRef solvers session info q = do - case q of - PleaseFetchContract addr _ continue -> do - cache <- liftIO $ readIORef contractCacheRef - case Map.lookup addr cache of - Just (Just contract) -> pure $ continue contract - _ -> oracle q - PleaseFetchSlot addr slot continue -> do - cache <- liftIO $ readIORef slotCacheRef - case Map.lookup addr cache >>= Map.lookup slot of - Just (Just value) -> pure $ continue value - _ -> oracle q - _ -> oracle q - - where oracle = Fetch.oracle solvers session info +-- cachedOracle removed - hevm session handles all caching now rpcFetcher :: Functor f => f a -> Maybe W256 -> f (Fetch.BlockNumber, a) @@ -145,15 +128,13 @@ getUnknownLogs = mapMaybe (\case _ -> Nothing) exploreMethod :: (MonadUnliftIO m, ReadConfig m, TTY m) => - Method -> SolcContract -> SourceCache -> EVM.Types.VM Concrete RealWorld -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> IORef ContractCache -> IORef SlotCache -> m ([TxOrError], PartialsLogs) + Method -> SolcContract -> SourceCache -> EVM.Types.VM Concrete RealWorld -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs) -exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpcInfo contractCacheRef slotCacheRef = do +exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpcInfo session = do calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) [] let cd = fst calldataSym - session <- Fetch.mkSession - let - fetcher = cachedOracle contractCacheRef slotCacheRef solvers (Just session) rpcInfo + fetcher = Fetch.oracle solvers (Just session) rpcInfo dst = conf.solConf.contractAddr vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm let diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index d70094761..340bfa66b 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -84,8 +84,6 @@ exploreContract :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.En exploreContract contract method vm = do conf <- asks (.cfg) dappInfo <- asks (.dapp) - contractCacheRef <- asks (.fetchContractCache) - slotCacheRef <- asks (.fetchSlotCache) let timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout) maxIters = Just conf.campaignConf.symExecMaxIters @@ -102,13 +100,14 @@ exploreContract contract method vm = do let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive, dumpQueries = False } let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo} let runtimeEnv = defaultEnv { config = hevmConfig } + session <- asks (.fetchSession) pushWorkerEvent $ SymExecLog ("Exploring " <> (show method.name)) liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) 1 timeoutSMT $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do -- For now, we will be exploring a single method at a time. -- In some cases, this methods list will have only one method, but in other cases, it will have several methods. -- This is to improve the user experience, as it will produce results more often, instead having to wait for exploring several - res <- exploreMethod method contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo contractCacheRef slotCacheRef + res <- exploreMethod method contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session liftIO $ putMVar resultChan res liftIO $ putMVar doneChan () liftIO $ putMVar threadIdChan threadId diff --git a/lib/Echidna/SymExec/Verification.hs b/lib/Echidna/SymExec/Verification.hs index ebbbb03a9..7e54f942e 100644 --- a/lib/Echidna/SymExec/Verification.hs +++ b/lib/Echidna/SymExec/Verification.hs @@ -49,8 +49,6 @@ verifyMethod :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m verifyMethod method contract vm = do conf <- asks (.cfg) dappInfo <- asks (.dapp) - contractCacheRef <- asks (.fetchContractCache) - slotCacheRef <- asks (.fetchSlotCache) let timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout) maxIters = Just conf.campaignConf.symExecMaxIters @@ -67,11 +65,12 @@ verifyMethod method contract vm = do let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, dumpExprs = True, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive } let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo} let runtimeEnv = defaultEnv { config = hevmConfig } + session <- asks (.fetchSession) pushWorkerEvent $ SymExecLog ("Verifying " <> (show method.name)) liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) 1 timeoutSMT $ \solvers -> do threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do - (res, partials) <- exploreMethod method contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo contractCacheRef slotCacheRef + (res, partials) <- exploreMethod method contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session liftIO $ putMVar resultChan (res, partials) liftIO $ putMVar doneChan () liftIO $ putMVar threadIdChan threadId diff --git a/lib/Echidna/Types/Config.hs b/lib/Echidna/Types/Config.hs index 637fd5959..b62c868aa 100644 --- a/lib/Echidna/Types/Config.hs +++ b/lib/Echidna/Types/Config.hs @@ -10,6 +10,7 @@ import Data.Word (Word64) import EVM.Dapp (DappInfo) import EVM.Types (Addr, W256) +import EVM.Fetch qualified as Fetch import Echidna.SourceAnalysis.Slither (SlitherInfo) import Echidna.SourceMapping (CodehashMap) @@ -79,8 +80,7 @@ data Env = Env , slitherInfo :: Maybe SlitherInfo , codehashMap :: CodehashMap - , fetchContractCache :: IORef ContractCache - , fetchSlotCache :: IORef SlotCache + , fetchSession :: Fetch.Session , contractNameCache :: IORef ContractNameCache , chainId :: Maybe W256 , world :: World diff --git a/lib/Echidna/UI.hs b/lib/Echidna/UI.hs index 326e7d78e..f0e4b95e4 100644 --- a/lib/Echidna/UI.hs +++ b/lib/Echidna/UI.hs @@ -6,6 +6,7 @@ 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 @@ -113,8 +114,9 @@ ui vm dict initialCorpus cliSelectedContract = do writeBChan uiChannel (CampaignUpdated now tests states) -- TODO: remove and use events for this - c <- readIORef env.fetchContractCache - s <- readIORef env.fetchSlotCache + -- For now, return empty cache data since accessing hevm's internal cache is complex + let c = mempty :: Map Addr (Maybe Contract) + let s = mempty :: Map Addr (Map W256 (Maybe W256)) writeBChan uiChannel (FetchCacheUpdated c s) -- UI initialization @@ -212,7 +214,7 @@ ui vm dict initialCorpus cliSelectedContract = do when (isJust conf.campaignConf.serverPort) $ do -- wait until we send all SSE events liftIO $ putStrLn "Waiting until all SSE are received..." - readMVar serverStopVar + liftIO $ Control.Concurrent.MVar.readMVar serverStopVar states <- liftIO $ workerStates workers From 9a626f56805520d915cb8f82e4d5d60077985b1f Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Fri, 3 Oct 2025 12:44:30 -0300 Subject: [PATCH 03/17] fixes --- lib/Echidna/Exec.hs | 2 +- lib/Echidna/Onchain.hs | 3 +-- stack.yaml | 1 + 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs index a96048ffc..3e65e1bc4 100644 --- a/lib/Echidna/Exec.hs +++ b/lib/Echidna/Exec.hs @@ -14,7 +14,7 @@ import Control.Monad.Reader (MonadReader, ask, asks) import Control.Monad.ST (ST, stToIO, RealWorld) import Data.Bits import Data.ByteString qualified as BS -import Data.IORef (readIORef, atomicWriteIORef, newIORef, writeIORef, modifyIORef') +import Data.IORef (readIORef, newIORef, writeIORef, modifyIORef') import Data.Map qualified as Map import Data.Maybe (fromMaybe, fromJust) import Data.Text qualified as T diff --git a/lib/Echidna/Onchain.hs b/lib/Echidna/Onchain.hs index 11c2eaef9..5f3a9d575 100644 --- a/lib/Echidna/Onchain.hs +++ b/lib/Echidna/Onchain.hs @@ -9,7 +9,6 @@ import Data.ByteString (ByteString) import Data.ByteString qualified as BS import Data.ByteString.UTF8 qualified as UTF8 import Data.Functor ((<&>)) -import Data.IORef (readIORef) import Data.Map (Map) import Data.Map qualified as Map import Data.Maybe (isJust, fromJust, fromMaybe) @@ -40,7 +39,7 @@ import Echidna.Types.Campaign (CampaignConf(..)) import Echidna.Types.Config (Env(..), EConfig(..)) import Echidna.Output.Source (saveCoverages) import Control.Monad (when, forM_) -import Control.Concurrent.MVar (newMVar, readMVar) +import Control.Concurrent.MVar (readMVar) rpcUrlEnv :: IO (Maybe Text) rpcUrlEnv = do diff --git a/stack.yaml b/stack.yaml index bc55412f7..b5c23909a 100644 --- a/stack.yaml +++ b/stack.yaml @@ -12,4 +12,5 @@ extra-deps: - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162 - spool-0.1@sha256:77780cbfc2c0be23ff2ea9e474062f3df97fcd9db946ee0b3508280a923b83e2,1461 - strip-ansi-escape-0.1.0.0@sha256:08f2ed93b16086a837ec46eab7ce8d27cf39d47783caaeb818878ea33c2ff75f,1628 +- jsonl-0.2.0.0@sha256:35f8a3816f0b93830008709a8e64c0c69b9bc632a92c54b3be3345bfccba4a5c,1465 - vty-windows-0.2.0.3@sha256:0c010b1086a725046a8bb08bb1e6bfdfdb3cfe1c72d6fa77c37306ef9ec774d8,2844 From b5b3b88784f2fdc72aa003ce8b6071a9cf036500 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 11 Oct 2025 08:40:19 -0300 Subject: [PATCH 04/17] Added rpc cache serialization code and fixes --- lib/Echidna.hs | 18 ++++++++----- lib/Echidna/Onchain.hs | 50 ++++++++--------------------------- lib/Echidna/SymExec/Common.hs | 2 +- lib/Etherscan.hs | 5 ++-- stack.yaml | 2 +- 5 files changed, 28 insertions(+), 49 deletions(-) diff --git a/lib/Echidna.hs b/lib/Echidna.hs index 5f2dec47e..c6b5a17fc 100644 --- a/lib/Echidna.hs +++ b/lib/Echidna.hs @@ -4,6 +4,7 @@ import Control.Concurrent (newChan) import Control.Concurrent.MVar (newMVar) import Control.Monad.Catch (MonadThrow(..)) import Control.Monad.IO.Class (liftIO) +import Control.Monad.Reader (runReaderT) import Network.Wreq.Session qualified as NetSession import Control.Monad.ST (RealWorld) import Data.IORef (newIORef) @@ -21,6 +22,9 @@ import EVM.Dapp (dappInfo) import EVM.Fetch qualified import EVM.Solidity (BuildOutput(..), Contracts(Contracts), Method(..), Mutability(..), SolcContract(..)) import EVM.Types hiding (Env) +import EVM.Effects (TTY(..), ReadConfig(..), defaultConfig) +import Data.Text qualified as T +import System.IO (stderr, hPutStrLn) import Echidna.ABI import Echidna.Onchain as Onchain @@ -111,6 +115,13 @@ loadInitialCorpus env = do ctxs2 <- loadTxs (dir "coverage") pure (ctxs1 ++ ctxs2) +instance TTY IO where + writeOutput = liftIO . putStrLn . T.unpack + writeErr = liftIO . hPutStrLn stderr . T.unpack + +instance ReadConfig IO where + readConfig = pure defaultConfig + mkEnv :: EConfig -> BuildOutput -> [EchidnaTest] -> World -> Maybe SlitherInfo -> IO Env mkEnv cfg buildOutput tests world slitherInfo = do codehashMap <- newIORef mempty @@ -120,12 +131,7 @@ mkEnv cfg buildOutput tests world slitherInfo = do coverageRefRuntime <- newIORef mempty corpusRef <- newIORef mempty testRefs <- traverse newIORef tests - -- Create session manually since mkSession needs App context - sess <- liftIO NetSession.newAPISession - let emptyCache = EVM.Fetch.FetchCache Map.empty Map.empty Map.empty - cache <- liftIO $ newMVar emptyCache - latestBlockNum <- liftIO $ newMVar Nothing - let fetchSession = EVM.Fetch.Session sess latestBlockNum cache + fetchSession <- EVM.Fetch.mkSession cfg.campaignConf.corpusDir contractNameCache <- newIORef mempty -- TODO put in real path let dapp = dappInfo "/" buildOutput diff --git a/lib/Echidna/Onchain.hs b/lib/Echidna/Onchain.hs index 5f3a9d575..fc4c0558d 100644 --- a/lib/Echidna/Onchain.hs +++ b/lib/Echidna/Onchain.hs @@ -4,14 +4,11 @@ module Echidna.Onchain where import Control.Exception (catch) import Data.Aeson (ToJSON, FromJSON) -import Data.Aeson qualified as JSON import Data.ByteString (ByteString) import Data.ByteString qualified as BS import Data.ByteString.UTF8 qualified as UTF8 -import Data.Functor ((<&>)) -import Data.Map (Map) import Data.Map qualified as Map -import Data.Maybe (isJust, fromJust, fromMaybe) +import Data.Maybe (isJust, fromJust) import Data.Text qualified as Text import Data.Text (Text) import Data.Vector qualified as Vector @@ -20,7 +17,7 @@ import Etherscan qualified import GHC.Generics (Generic) import Network.HTTP.Simple (HttpException) import Optics (view) -import System.Directory (createDirectoryIfMissing, doesFileExist) +import System.Directory (doesFileExist) import System.Environment (lookupEnv) import System.FilePath (()) import Network.Wreq.Session qualified as Session @@ -32,7 +29,6 @@ import EVM.Fetch qualified import EVM.Solidity (SourceCache(..), SolcContract (..)) import EVM.Types hiding (Env) -import Echidna.Orphans.JSON () import Echidna.SymExec.Symbolic (forceWord, forceBuf) import Echidna.Types (emptyAccount) import Echidna.Types.Campaign (CampaignConf(..)) @@ -41,6 +37,14 @@ import Echidna.Output.Source (saveCoverages) import Control.Monad (when, forM_) import Control.Concurrent.MVar (readMVar) +saveRpcCache :: Env -> IO () +saveRpcCache env = do + case env.fetchSession.cacheDir of + Just dir -> do + cache <- readMVar env.fetchSession.sharedCache + EVM.Fetch.saveCache dir cache + Nothing -> pure () + rpcUrlEnv :: IO (Maybe Text) rpcUrlEnv = do val <- lookupEnv "ECHIDNA_RPC_URL" @@ -67,7 +71,7 @@ safeFetchContractFrom session rpcBlock rpcUrl addr = do safeFetchSlotFrom :: EVM.Fetch.Session -> EVM.Fetch.BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256) safeFetchSlotFrom session rpcBlock rpcUrl addr slot = catch - (EVM.Fetch.fetchSlotWithSession session.sess rpcBlock rpcUrl addr slot) + (EVM.Fetch.fetchSlotWithCache defaultConfig session rpcBlock rpcUrl addr slot) (\(_ :: HttpException) -> pure $ Just 0) data FetchedContractData = FetchedContractData @@ -96,33 +100,6 @@ toFetchedContractData contract = , balance = forceWord contract.balance } --- | Try to load the persisted RPC cache. --- TODO: we use the corpus dir for now, think about where to place it -loadRpcCache - :: EConfig - -> IO ( Map Addr (Maybe Contract) - , Map Addr (Map W256 (Maybe W256)) - ) -loadRpcCache cfg = - case cfg.campaignConf.corpusDir of - Nothing -> pure (mempty, mempty) - Just dir -> do - let cache_dir = dir "cache" - createDirectoryIfMissing True cache_dir - case cfg.rpcBlock of - Just block -> do - parsedContracts :: Maybe (Map Addr FetchedContractData) <- - readFileIfExists (cache_dir "block_" <> show block <> "_fetch_cache_contracts.json") - <&> (>>= JSON.decodeStrict) - parsedSlots :: Maybe (Map Addr (Map W256 (Maybe W256))) <- - readFileIfExists (cache_dir "block_" <> show block <> "_fetch_cache_slots.json") - <&> (>>= JSON.decodeStrict) - pure - ( maybe mempty (Map.map (Just . fromFetchedContractData)) parsedContracts - , fromMaybe mempty parsedSlots - ) - Nothing -> - pure (mempty, mempty) readFileIfExists :: FilePath -> IO (Maybe BS.ByteString) readFileIfExists path = do @@ -167,11 +144,6 @@ externalSolcContract env addr c = do } pure (sourceCache, solcContract) --- TODO: This should happen continuously event-based -saveRpcCache :: Env -> IO () -saveRpcCache _env = do - -- Cache saving is now handled automatically by hevm's session cache - pure () saveCoverageReport :: Env -> Int -> IO () saveCoverageReport env runId = do diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs index 0aab3b644..30316e0f9 100644 --- a/lib/Echidna/SymExec/Common.hs +++ b/lib/Echidna/SymExec/Common.hs @@ -77,7 +77,7 @@ modelToTx dst oldTimestamp oldNumber method senders fallbackSender calldata resu Left e -> Left e args = case argdata of Right argdata' -> case decodeBuf types argdata' of - CAbi v -> v + (CAbi v, _) -> v _ -> [] Left _ -> [] diff --git a/lib/Etherscan.hs b/lib/Etherscan.hs index 1c2526159..8cde150b2 100644 --- a/lib/Etherscan.hs +++ b/lib/Etherscan.hs @@ -24,8 +24,9 @@ data SourceCode = SourceCode fetchContractSource :: Maybe Text -> Addr -> IO (Maybe SourceCode) fetchContractSource apiKey addr = do - url <- parseRequest $ "https://api.etherscan.io/api?" - <> "module=contract" + url <- parseRequest $ "https://api.etherscan.io/v2/api?" + <> "&chainid=1" + <> "&module=contract" <> "&action=getsourcecode" <> "&address=" <> show addr <> T.unpack (maybe "" ("&apikey=" <>) apiKey) diff --git a/stack.yaml b/stack.yaml index b5c23909a..7c64a59ae 100644 --- a/stack.yaml +++ b/stack.yaml @@ -6,7 +6,7 @@ packages: extra-deps: - git: https://github.com/argotorg/hevm.git - commit: 95b5e074c9f27f970011ed53f38f1643d70c3c8a + commit: 62a65743a0f840fb96dc101a3c176ee8da73c382 - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162 From 83f5dd4a7bfd0c146d0fa6ad53e0fcaaf17ace84 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 11 Oct 2025 08:43:48 -0300 Subject: [PATCH 05/17] fixes --- lib/Echidna.hs | 3 --- 1 file changed, 3 deletions(-) diff --git a/lib/Echidna.hs b/lib/Echidna.hs index c6b5a17fc..70f92575c 100644 --- a/lib/Echidna.hs +++ b/lib/Echidna.hs @@ -1,11 +1,8 @@ module Echidna where import Control.Concurrent (newChan) -import Control.Concurrent.MVar (newMVar) import Control.Monad.Catch (MonadThrow(..)) import Control.Monad.IO.Class (liftIO) -import Control.Monad.Reader (runReaderT) -import Network.Wreq.Session qualified as NetSession import Control.Monad.ST (RealWorld) import Data.IORef (newIORef) import Data.List (find, nub) From bdd501f2babb0be15b9f774387ab3030a914bc14 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 11 Oct 2025 10:18:00 -0300 Subject: [PATCH 06/17] fixes --- flake.nix | 4 ++-- lib/Echidna/Types/Tx.hs | 2 ++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 44c71aa8d..25dcf096b 100644 --- a/flake.nix +++ b/flake.nix @@ -54,8 +54,8 @@ (pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub { owner = "ethereum"; repo = "hevm"; - rev = "95b5e074c9f27f970011ed53f38f1643d70c3c8a"; - sha256 = "sha256-UqTg476msbyiDyy45dK1zYYbH4GiIE45R4wa0Nn2TUA="; + rev = "62a65743a0f840fb96dc101a3c176ee8da73c38"; + sha256 = "sha256-UqTg476msbyiDyy45dK1zYYbH4GiIF45R4wa0Nn2TUA="; }) { secp256k1 = pkgs.secp256k1; }) ([ pkgs.haskell.lib.compose.dontCheck diff --git a/lib/Echidna/Types/Tx.hs b/lib/Echidna/Types/Tx.hs index e5bf266b9..0e1a37a4a 100644 --- a/lib/Echidna/Types/Tx.hs +++ b/lib/Echidna/Types/Tx.hs @@ -194,6 +194,7 @@ data TxResult | ErrorNonceOverflow | ErrorReturnDataOutOfBounds | ErrorNonexistentFork + | ErrorNonexistentPrecompile deriving (Eq, Ord, Show, Enum) $(deriveJSON defaultOptions ''TxResult) @@ -259,6 +260,7 @@ getResult = \case VMFailure NonceOverflow -> ErrorNonceOverflow VMFailure ReturnDataOutOfBounds -> ErrorReturnDataOutOfBounds VMFailure (NonexistentFork _) -> ErrorNonexistentFork + VMFailure (NonexistentPrecompile _) -> ErrorNonexistentPrecompile makeSingleTx :: Addr -> Addr -> W256 -> TxCall -> [Tx] makeSingleTx a d v (SolCall c) = [Tx (SolCall c) a d maxGasPerBlock 0 v (0, 0)] From 1d40bd0c47ca4b18d2f5e45fd1f4e3b07a16c900 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 11 Oct 2025 10:43:42 -0300 Subject: [PATCH 07/17] fixes --- flake.nix | 2 +- package.yaml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 25dcf096b..805cfa898 100644 --- a/flake.nix +++ b/flake.nix @@ -55,7 +55,7 @@ owner = "ethereum"; repo = "hevm"; rev = "62a65743a0f840fb96dc101a3c176ee8da73c38"; - sha256 = "sha256-UqTg476msbyiDyy45dK1zYYbH4GiIF45R4wa0Nn2TUA="; + sha256 = "sha256-uprCikW55t6sjbEW/K8j4W74RrCKSlO8KsiXDSwgR8Q="; }) { secp256k1 = pkgs.secp256k1; }) ([ pkgs.haskell.lib.compose.dontCheck diff --git a/package.yaml b/package.yaml index 996d04502..6e519db4b 100644 --- a/package.yaml +++ b/package.yaml @@ -3,7 +3,7 @@ name: echidna author: Trail of Bits maintainer: Trail of Bits -version: 2.2.7 +version: 2.3.0 ghc-options: - -O2 From 25b025a47bed806d4175b72057a8211ff8314e5c Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 11 Oct 2025 12:32:55 -0300 Subject: [PATCH 08/17] refactor verification code to make sure tests are correctly labeled when the verifiction finishes --- lib/Echidna/Campaign.hs | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs index be7372ebf..ec41cfbf4 100644 --- a/lib/Echidna/Campaign.hs +++ b/lib/Echidna/Campaign.hs @@ -297,24 +297,26 @@ runSymWorker callback vm dict workerId _ name = do -- 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 newCoverage $ do unless (null txs) $ error "No new coverage but symbolic execution found valid txs. Something is wrong." - updateTests $ \test -> do - if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then - pure $ Just $ test { Test.state = Unsolvable } - else - pure $ Just test - pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction.")) - + 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 - 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 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. From 8d746d60ed394da6e085b14cf59eeef360768753 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sat, 11 Oct 2025 12:50:03 -0300 Subject: [PATCH 09/17] revert b899481b65685d42d2683f758e3d59821e5a9e1f --- .github/scripts/install-z3.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/scripts/install-z3.sh b/.github/scripts/install-z3.sh index f79f532b3..924b2ae77 100755 --- a/.github/scripts/install-z3.sh +++ b/.github/scripts/install-z3.sh @@ -3,14 +3,14 @@ set -eux -o pipefail if [ "$HOST_OS" = "Linux" ]; then if [ $(uname -m) = "aarch64" ]; then - curl -fsSL -o z3.zip https://github.com/Z3Prover/z3/releases/download/z3-4.12.6/z3-4.12.6-arm64-glibc-2.35.zip + curl -fsSL -o z3.zip https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-arm64-glibc-2.34.zip elif [ $(uname -m) = "x86_64" ]; then - curl -fsSL -o z3.zip https://github.com/Z3Prover/z3/releases/download/z3-4.12.6/z3-4.12.6-x64-glibc-2.35.zip + curl -fsSL -o z3.zip https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-x64-glibc-2.39.zip fi unzip z3.zip cp -a z3-*/bin/z3 "$HOME/.local/bin/" rm -rf z3-*/ z3.zip fi if [ "$HOST_OS" = "Windows" ]; then - choco install z3 --version=4.12.6 + choco install z3 fi From c1d085533747df1e60473515cd635de82167b2fb Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sun, 12 Oct 2025 09:07:18 -0300 Subject: [PATCH 10/17] disable RPC logs --- lib/Echidna/Exec.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs index 3e65e1bc4..cabdf5203 100644 --- a/lib/Echidna/Exec.hs +++ b/lib/Echidna/Exec.hs @@ -113,7 +113,7 @@ execTxWith executeTx tx = do case getQuery vmResult of -- A previously unknown contract is required Just q@(PleaseFetchContract addr _ continuation) -> do - logMsg $ "INFO: Performing RPC: " <> show q + --logMsg $ "INFO: Performing RPC: " <> show q case config.rpcUrl of Just rpcUrl -> do session <- asks (.fetchSession) @@ -130,7 +130,7 @@ execTxWith executeTx tx = do -- RPC server returning junk etc. fromEVM (continuation emptyAccount) Nothing -> do - logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q + --logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q -- TODO: How should we fail here? RPC is not configured but VM -- wants to fetch fromEVM (continuation emptyAccount) @@ -138,7 +138,7 @@ execTxWith executeTx tx = do -- A previously unknown slot is required Just q@(PleaseFetchSlot addr slot continuation) -> do - logMsg $ "INFO: Performing RPC: " <> show q + --logMsg $ "INFO: Performing RPC: " <> show q case config.rpcUrl of Just rpcUrl -> do session <- asks (.fetchSession) @@ -152,7 +152,7 @@ execTxWith executeTx tx = do logMsg $ "ERROR: Failed to fetch slot: " <> show q fromEVM (continuation 0) Nothing -> do - logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q + --logMsg $ "ERROR: Requested RPC but it is not configured: " <> show q -- Use the zero slot fromEVM (continuation 0) runFully -- resume execution From 4c4e96f7816957cf267c5ad17907f471f6ebc453 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Mon, 20 Oct 2025 12:54:31 -0300 Subject: [PATCH 11/17] update to the latest hevm --- lib/Echidna.hs | 2 +- lib/Echidna/Onchain.hs | 11 ++++++----- lib/Echidna/SymExec/Exploration.hs | 2 +- lib/Echidna/SymExec/Verification.hs | 2 +- stack.yaml | 2 +- 5 files changed, 10 insertions(+), 9 deletions(-) diff --git a/lib/Echidna.hs b/lib/Echidna.hs index 70f92575c..cb0c26187 100644 --- a/lib/Echidna.hs +++ b/lib/Echidna.hs @@ -128,7 +128,7 @@ mkEnv cfg buildOutput tests world slitherInfo = do coverageRefRuntime <- newIORef mempty corpusRef <- newIORef mempty testRefs <- traverse newIORef tests - fetchSession <- EVM.Fetch.mkSession cfg.campaignConf.corpusDir + fetchSession <- EVM.Fetch.mkSession cfg.campaignConf.corpusDir (fromIntegral <$> cfg.rpcBlock) contractNameCache <- newIORef mempty -- TODO put in real path let dapp = dappInfo "/" buildOutput diff --git a/lib/Echidna/Onchain.hs b/lib/Echidna/Onchain.hs index fc4c0558d..24d71d394 100644 --- a/lib/Echidna/Onchain.hs +++ b/lib/Echidna/Onchain.hs @@ -39,11 +39,12 @@ import Control.Concurrent.MVar (readMVar) saveRpcCache :: Env -> IO () saveRpcCache env = do - case env.fetchSession.cacheDir of - Just dir -> do - cache <- readMVar env.fetchSession.sharedCache - EVM.Fetch.saveCache dir cache - Nothing -> pure () + case (env.fetchSession.cacheDir, env.cfg.rpcBlock) of + (Just dir, Just n) -> do + cache <- readMVar (env.fetchSession.sharedCache) + EVM.Fetch.saveCache dir (fromIntegral n) cache + (_, Nothing) -> putStrLn "Warning: cannot save RPC cache without a specified block number." + (Nothing, _) -> pure () rpcUrlEnv :: IO (Maybe Text) rpcUrlEnv = do diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index 340bfa66b..f3bfec436 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -89,7 +89,7 @@ exploreContract contract method vm = do maxIters = Just conf.campaignConf.symExecMaxIters maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore) askSmtIters = conf.campaignConf.symExecAskSMTIters - rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock)) Nothing Nothing Nothing + rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock)) defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0 threadIdChan <- liftIO newEmptyMVar diff --git a/lib/Echidna/SymExec/Verification.hs b/lib/Echidna/SymExec/Verification.hs index 7e54f942e..81b5df66e 100644 --- a/lib/Echidna/SymExec/Verification.hs +++ b/lib/Echidna/SymExec/Verification.hs @@ -54,7 +54,7 @@ verifyMethod method contract vm = do maxIters = Just conf.campaignConf.symExecMaxIters maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore) askSmtIters = conf.campaignConf.symExecAskSMTIters - rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock)) Nothing Nothing Nothing + rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock)) defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0 threadIdChan <- liftIO newEmptyMVar diff --git a/stack.yaml b/stack.yaml index 7c64a59ae..f06d2668a 100644 --- a/stack.yaml +++ b/stack.yaml @@ -6,7 +6,7 @@ packages: extra-deps: - git: https://github.com/argotorg/hevm.git - commit: 62a65743a0f840fb96dc101a3c176ee8da73c382 + commit: 0d9e2744903d160b175cd9e727660b493d9fac6f - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162 From 1a55e49ecbe2aefc6261bd59ccb74fc90d5dfdf7 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Mon, 20 Oct 2025 14:09:31 -0300 Subject: [PATCH 12/17] updated flake --- flake.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 805cfa898..0ab53da0c 100644 --- a/flake.nix +++ b/flake.nix @@ -54,8 +54,8 @@ (pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub { owner = "ethereum"; repo = "hevm"; - rev = "62a65743a0f840fb96dc101a3c176ee8da73c38"; - sha256 = "sha256-uprCikW55t6sjbEW/K8j4W74RrCKSlO8KsiXDSwgR8Q="; + rev = "0d9e2744903d160b175cd9e727660b493d9fac6f"; + sha256 = "sha256-uprCikW55t6sjbEW/K8j4W74RrCKFlO8KsiXDSwgR8Q="; }) { secp256k1 = pkgs.secp256k1; }) ([ pkgs.haskell.lib.compose.dontCheck From 31d5ef3acac70073bc1a50cc08f974929186744f Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Mon, 20 Oct 2025 14:17:12 -0300 Subject: [PATCH 13/17] updated flake --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 0ab53da0c..ffe2bd548 100644 --- a/flake.nix +++ b/flake.nix @@ -55,7 +55,7 @@ owner = "ethereum"; repo = "hevm"; rev = "0d9e2744903d160b175cd9e727660b493d9fac6f"; - sha256 = "sha256-uprCikW55t6sjbEW/K8j4W74RrCKFlO8KsiXDSwgR8Q="; + sha256 = "sha256-SYqhjlvGKdWf55JjGZ8BPFtXqbkL81os5FB9j4Nj40A="; }) { secp256k1 = pkgs.secp256k1; }) ([ pkgs.haskell.lib.compose.dontCheck From 987627d4bba707a6b4d321168e4b9146859b1db1 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Wed, 22 Oct 2025 10:26:07 -0300 Subject: [PATCH 14/17] avoid crashing when trying to do symbolic execution in fallback --- lib/Echidna/SymExec/Exploration.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index f3bfec436..44fc1f2f8 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -44,6 +44,7 @@ import Echidna.Worker (pushWorkerEvent) -- The Tx argument, if present, must have a .call value of type SolCall. getTargetMethodFromTx :: (MonadIO m, MonadReader Echidna.Types.Config.Env m) => Tx -> SolcContract -> [String] -> m (Maybe Method) +getTargetMethodFromTx (Tx { call = SolCall ("", _) }) _ _ = return Nothing getTargetMethodFromTx (Tx { call = SolCall (methodName, _) }) contract failedProperties = do env <- ask let allMethods = Map.assocs contract.abiMap From d41ee3298d691067a9a0f8a5dc929de72ddbec6f Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Wed, 29 Oct 2025 11:05:06 +0100 Subject: [PATCH 15/17] silence RPC warning when there is no RPC configured --- lib/Echidna/Onchain.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lib/Echidna/Onchain.hs b/lib/Echidna/Onchain.hs index 24d71d394..6a8da7f78 100644 --- a/lib/Echidna/Onchain.hs +++ b/lib/Echidna/Onchain.hs @@ -43,7 +43,9 @@ saveRpcCache env = do (Just dir, Just n) -> do cache <- readMVar (env.fetchSession.sharedCache) EVM.Fetch.saveCache dir (fromIntegral n) cache - (_, Nothing) -> putStrLn "Warning: cannot save RPC cache without a specified block number." + (_, Nothing) -> if (env.cfg.rpcUrl /= Nothing) + then putStrLn "Warning: cannot save RPC cache without a specified block number." + else pure () (Nothing, _) -> pure () rpcUrlEnv :: IO (Maybe Text) From a2b222486db9459734dac66f02d5c2a6c4fe560a Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Wed, 29 Oct 2025 11:18:11 +0100 Subject: [PATCH 16/17] hlint fixes --- lib/Echidna/Onchain.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/lib/Echidna/Onchain.hs b/lib/Echidna/Onchain.hs index 6a8da7f78..0bc967e03 100644 --- a/lib/Echidna/Onchain.hs +++ b/lib/Echidna/Onchain.hs @@ -43,9 +43,8 @@ saveRpcCache env = do (Just dir, Just n) -> do cache <- readMVar (env.fetchSession.sharedCache) EVM.Fetch.saveCache dir (fromIntegral n) cache - (_, Nothing) -> if (env.cfg.rpcUrl /= Nothing) - then putStrLn "Warning: cannot save RPC cache without a specified block number." - else pure () + (_, Nothing) -> when (isJust (env.cfg.rpcUrl)) + $ putStrLn "Warning: cannot save RPC cache without a specified block number." (Nothing, _) -> pure () rpcUrlEnv :: IO (Maybe Text) From 0406e4fffcc384ce5454e8c9e6ad16e9ba2c59df Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Fri, 31 Oct 2025 13:25:56 +0100 Subject: [PATCH 17/17] switch to stack based loop detection --- lib/Echidna/SymExec/Exploration.hs | 2 +- lib/Echidna/SymExec/Verification.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs index 44fc1f2f8..379e3fd55 100644 --- a/lib/Echidna/SymExec/Exploration.hs +++ b/lib/Echidna/SymExec/Exploration.hs @@ -97,7 +97,7 @@ exploreContract contract method vm = do doneChan <- liftIO newEmptyMVar resultChan <- liftIO newEmptyMVar let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text - let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = Naive} + let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = StackBased} let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive, dumpQueries = False } let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo} let runtimeEnv = defaultEnv { config = hevmConfig } diff --git a/lib/Echidna/SymExec/Verification.hs b/lib/Echidna/SymExec/Verification.hs index 81b5df66e..fceecc459 100644 --- a/lib/Echidna/SymExec/Verification.hs +++ b/lib/Echidna/SymExec/Verification.hs @@ -61,7 +61,7 @@ verifyMethod method contract vm = do doneChan <- liftIO newEmptyMVar resultChan <- liftIO newEmptyMVar let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text - let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = Naive} + let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = StackBased} let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, dumpExprs = True, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive } let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo} let runtimeEnv = defaultEnv { config = hevmConfig }