Echidna 2.3 RC

.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

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 = "0d9e2744903d160b175cd9e727660b493d9fac6f";
+            sha256 = "sha256-SYqhjlvGKdWf55JjGZ8BPFtXqbkL81os5FB9j4Nj40A=";
           }) { secp256k1 = pkgs.secp256k1; })
           ([
             pkgs.haskell.lib.compose.dontCheck

lib/Echidna.hs

@@ -2,6 +2,7 @@ module Echidna where
 
 import Control.Concurrent (newChan)
 import Control.Monad.Catch (MonadThrow(..))
+import Control.Monad.IO.Class (liftIO)
 import Control.Monad.ST (RealWorld)
 import Data.IORef (newIORef)
 import Data.List (find, nub)
@@ -15,8 +16,12 @@ 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)
+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
@@ -107,6 +112,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
@@ -116,13 +128,11 @@ 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
+  fetchSession <- EVM.Fetch.mkSession cfg.campaignConf.corpusDir (fromIntegral <$> cfg.rpcBlock)
   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
              }

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.

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
@@ -114,68 +114,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

lib/Echidna/Onchain.hs

@@ -4,15 +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.IORef (readIORef)
-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
@@ -21,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
@@ -33,13 +29,23 @@ 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(..))
 import Echidna.Types.Config (Env(..), EConfig(..))
 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, env.cfg.rpcBlock) of
+    (Just dir, Just n) -> do
+      cache <- readMVar (env.fetchSession.sharedCache)
+      EVM.Fetch.saveCache dir (fromIntegral n) cache
+    (_, Nothing) -> when (isJust (env.cfg.rpcUrl))
+      $ putStrLn "Warning: cannot save RPC cache without a specified block number."
+    (Nothing, _) -> pure ()
 
 rpcUrlEnv :: IO (Maybe Text)
 rpcUrlEnv = do
@@ -57,17 +63,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
+safeFetchContractFrom :: EVM.Fetch.Session -> EVM.Fetch.BlockNumber -> Text -> Addr -> IO (Maybe Contract)
+safeFetchContractFrom session rpcBlock rpcUrl addr = do
   catch
-    (EVM.Fetch.fetchContractFrom defaultConfig rpcBlock rpcUrl addr)
+    (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 =
+safeFetchSlotFrom :: EVM.Fetch.Session -> EVM.Fetch.BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256)
+safeFetchSlotFrom session rpcBlock rpcUrl addr slot =
   catch
-    (EVM.Fetch.fetchSlotFrom defaultConfig rpcBlock rpcUrl addr slot)
+    (EVM.Fetch.fetchSlotWithCache defaultConfig session rpcBlock rpcUrl addr slot)
     (\(_ :: HttpException) -> pure $ Just 0)
 
 data FetchedContractData = FetchedContractData
@@ -96,33 +102,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,24 +146,6 @@ externalSolcContract env addr c = do
         }
     pure (sourceCache, solcContract)
 
--- 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 ()
 
 saveCoverageReport :: Env -> Int -> IO ()
 saveCoverageReport env runId = do
@@ -194,20 +155,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)