Reworked symbolic execution code (#1394)

* removed old solc versions, use 0.8.x only instead

* fixed harvey test

* started to fix symexec using latest hevm

* added RPC support for symbolic execution + some clean up

* better constraints for block timestamp and number

* improved and simplified symexec code

* removed useless code

* some test fixes

* increase the number of random symbolic transaction if the corpus is empty

* added comments on why we only take one method from the shuffle list when doing symbolic exploration

* allow user to select smt solver

* use slither to filter functions with assert, if any

* started adding full verification mode for stateless campaigns

* refactored tons of code

* improved code for exploration/verification

* finished implementation and get back to hevm master

* fixed issue in addBlockConstraints and upgraded hevm

* disable debug mode when using interactive mode

* corrected array size in symbolic output

* fix decoding of negative numbers

* simplified code for decoding of negative numbers

* removed initialize field from default

* use verification mode for sym-assert test

* added some basic verification tests

* make the harvey test more reliable

* simplified exploration code and added shrinking

* added new test for exploration mode (but disabled so far)

* worker related refactoring code to allow other parts of the codebase to send events

* make sure symExecTarget is used to select methods

* keccak preimage support enabled

* reduced code duplication

* added documentation

* use new types in Types/Config.hs

* removed killed-related files

.github/workflows/ci.yml

@@ -220,15 +220,9 @@ jobs:
           - ubuntu-latest
           - windows-latest
         solc:
-          - "0.4.25"
-          - "0.5.7"
-          - "0.6.12"
-          - "0.7.5"
+          - "0.8.10"
+          - "0.8.25"
         include:
-          - solc: "0.6.12"
-            experimental: true
-          - solc: "0.7.5"
-            experimental: true
           - os: windows-latest
             experimental: true
 

flake.nix

@@ -55,8 +55,8 @@
           (pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "ethereum";
             repo = "hevm";
-            rev = "release/0.55.0";
-            sha256 = "sha256-DVwQisTwgSjZQkQSn5s7ZN3SS1z2EfISA6Lw0ruUg6Y=";
+            rev = "1ee94f7772d42154fcf8df16681d3c6f25a4ecdd";
+            sha256 = "sha256-UgdkkFw1BVjzqRz69FGpwfk/iPqtU5IUqybfAQIhXk8=";
           }) { secp256k1 = pkgs.secp256k1; })
           ([
             pkgs.haskell.lib.compose.dontCheck

lib/Echidna.hs

@@ -23,7 +23,7 @@ import Echidna.Onchain as Onchain
 import Echidna.Output.Corpus
 import Echidna.SourceAnalysis.Slither
 import Echidna.Solidity
-import Echidna.Symbolic (forceAddr)
+import Echidna.SymExec.Symbolic (forceAddr)
 import Echidna.Types.Campaign
 import Echidna.Types.Config
 import Echidna.Types.Random

lib/Echidna/Campaign.hs

@@ -18,12 +18,13 @@ import Data.ByteString.Lazy qualified as LBS
 import Data.IORef (readIORef, atomicModifyIORef', writeIORef)
 import Data.Foldable (foldlM)
 import Data.List qualified as List
+import Data.List.NonEmpty qualified as NEList
 import Data.Map qualified as Map
 import Data.Map (Map, (\\))
-import Data.Maybe (isJust, mapMaybe)
+import Data.Maybe (isJust, mapMaybe, fromJust)
 import Data.Set (Set)
 import Data.Set qualified as Set
-import Data.Text (Text)
+import Data.Text (Text, unpack)
 import Data.Time (LocalTime)
 import System.Random (mkStdGen)
 
@@ -31,25 +32,31 @@ import EVM (cheatCode)
 import EVM.ABI (getAbi, AbiType(AbiAddressType), AbiValue(AbiAddress))
 import EVM.Dapp (DappInfo(..))
 import EVM.Types hiding (Env, Frame(state), Gas)
+import EVM.Solidity (SolcContract(..), Method(..))
 
 import Echidna.ABI
 import Echidna.Events (extractEventValues)
 import Echidna.Exec
 import Echidna.Mutator.Corpus
 import Echidna.Shrink (shrinkTest)
-import Echidna.Symbolic (forceAddr)
-import Echidna.SymExec (createSymTx)
+import Echidna.Solidity (chooseContract)
+import Echidna.SymExec.Common (extractTxs, extractErrors)
+import Echidna.SymExec.Symbolic (forceAddr)
+import Echidna.SymExec.Exploration (exploreContract, getTargetMethodFromTx, getRandomTargetMethod)
+import Echidna.SymExec.Verification (verifyMethod)
 import Echidna.Test
 import Echidna.Transaction
 import Echidna.Types.Campaign
 import Echidna.Types.Corpus (Corpus, corpusSize)
 import Echidna.Types.Coverage (coverageStats)
 import Echidna.Types.Config
+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.Utility (getTimestamp)
+import Echidna.Types.Worker
+import Echidna.Worker 
 
 instance MonadThrow m => MonadThrow (RandT g m) where
   throwM = lift . throwM
@@ -109,7 +116,7 @@ runSymWorker
   -- ^ Initial corpus of transactions
   -> Maybe Text -- ^ Specified contract name
   -> m (WorkerStopReason, WorkerState)
-runSymWorker callback vm dict workerId initialCorpus name = do
+runSymWorker callback vm dict workerId _ name = do
   cfg <- asks (.cfg)
   let nworkers = getNFuzzWorkers cfg.campaignConf -- getNFuzzWorkers, NOT getNWorkers
   eventQueue <- asks (.eventQueue)
@@ -117,12 +124,13 @@ runSymWorker callback vm dict workerId initialCorpus name = do
 
   flip runStateT initialState $
     flip evalRandT (mkStdGen effectiveSeed) $ do -- unused but needed for callseq
-      lift callback
-      void $ replayCorpus vm initialCorpus
-      symexecTxs []
-      mapM_ (symexecTxs . snd) initialCorpus
-      listenerLoop listenerFunc chan nworkers
-      pure SymbolicDone
+      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
 
@@ -143,49 +151,164 @@ runSymWorker callback vm dict workerId initialCorpus name = do
   -- chains where each transaction results in new coverage.
   listenerFunc (_, WorkerEvent _ _ (NewCoverage {transactions})) = do
     void $ callseq vm transactions
-    symexecTxs transactions
+    symexecTxs False transactions
+    shrinkAndRandomlyExplore transactions (10 :: Int)
   listenerFunc _ = pure ()
 
-  symexecTxs txs = mapM_ symexecTx =<< txsToTxAndVms txs
+  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:
-  -- (maybe txn to concolic execute on, vm to symexec on, list of txns we're on top of)
-  txsToTxAndVms txs = do
-    isConc <- asks (.cfg.campaignConf.symExecConcolic)
-    if isConc
-      then txsToTxAndVmsConc txs vm []
-      else txsToTxAndVmsSym txs
+  -- (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 isJust targets then
+      pure [(Nothing, rvm, rtxs)]
+    else
+      pure [(Just ltx, ivm, txs), (Nothing, rvm, rtxs)]
 
-  txsToTxAndVmsConc [] _ _ = pure []
-  txsToTxAndVmsConc (h:t) vm' txsBase = do
-    (_, vm'') <- execTx vm' h
-    rest <- txsToTxAndVmsConc t vm'' (txsBase <> [h])
-    pure $ case h of
-             (Tx { call = SolCall _ }) -> (Just h,vm',txsBase):rest
-             _ -> rest
+  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)]
 
-  txsToTxAndVmsSym txs = do
-    vm' <- foldlM (\vm' tx -> snd <$> execTx vm' tx) vm txs
-    pure [(Nothing,vm',txs)]
 
   symexecTx (tx, vm', txsBase) = do
-    cfg <- asks (.cfg)
+    conf <- asks (.cfg)
     dapp <- asks (.dapp)
-    let compiledContracts = Map.elems dapp.solcByName
-    (threadId, symTxsChan) <- liftIO $ createSymTx cfg name compiledContracts tx vm'
-
+    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 <- liftIO $ takeMVar symTxsChan
+    (symTxs, partials) <- liftIO $ takeMVar symTxsChan
 
     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 (txsBase <> [symTx])) symTxs
+    let txs = extractTxs symTxs
+    let errors = extractErrors symTxs
 
-    unless (newCoverage || null symTxs) (pushWorkerEvent SymNoNewCoverage)
+    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
+    mapM_ (symExecMethod contract) allMethods
+
+  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
+    let methodSignature = unpack method.methodSignature
+    if not (null partials) || not (null errors) then 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
+    else 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
+
+      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."))
 
 -- | Run a fuzzing campaign given an initial universe state, some tests, and an
 -- optional dictionary to generate calls with. Return the 'Campaign' state once
@@ -474,6 +597,14 @@ updateTests f = do
       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)
@@ -520,21 +651,6 @@ updateOpenTest vm reproducer test = do
       -- not an open test, skip
       pure Nothing
 
-pushWorkerEvent
-  :: (MonadReader Env m, MonadState WorkerState m, MonadIO m)
-  => WorkerEvent
-  -> m ()
-pushWorkerEvent event = do
-  workerId <- gets (.workerId)
-  env <- ask
-  let workerType = workerIDToType env.cfg.campaignConf workerId
-  liftIO $ pushCampaignEvent env (WorkerEvent workerId workerType event)
-
-pushCampaignEvent :: Env -> CampaignEvent -> IO ()
-pushCampaignEvent env event = do
-  time <- liftIO getTimestamp
-  writeChan env.eventQueue (time, event)
-
 -- | 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.

lib/Echidna/Config.hs

@@ -14,6 +14,7 @@ import Data.Text (isPrefixOf)
 import Data.Yaml qualified as Y
 
 import EVM.Types (VM(..), W256)
+import EVM.Solvers (Solver(..))
 
 import Echidna.Mutator.Corpus (defaultMutationConsts)
 import Echidna.Test
@@ -99,12 +100,20 @@ instance FromJSON EConfigWithUsage where
         <*> v ..:? "workers"
         <*> v ..:? "server"
         <*> v ..:? "symExec"            ..!= False
-        <*> v ..:? "symExecConcolic"    ..!= True
+        <*> smtSolver
         <*> v ..:? "symExecTargets"     ..!= Nothing
         <*> v ..:? "symExecTimeout"     ..!= defaultSymExecTimeout
         <*> v ..:? "symExecNSolvers"    ..!= defaultSymExecNWorkers
         <*> v ..:? "symExecMaxIters"    ..!= defaultSymExecMaxIters
         <*> v ..:? "symExecAskSMTIters" ..!= defaultSymExecAskSMTIters
+        <*> v ..:? "symExecMaxExplore"  ..!= defaultSymExecMaxExplore
+        where
+        smtSolver = v ..:? "symExecSMTSolver" >>= \case
+          Just ("z3" :: String)  -> pure Z3
+          Just "cvc5"            -> pure CVC5
+          Just "bitwuzla"        -> pure Bitwuzla
+          Just s                 -> fail $ "Unrecognized SMT solver: " <> s
+          Nothing                -> pure Bitwuzla
 
       solConfParser = SolConf
         <$> v ..:? "contractAddr"    ..!= defaultContractAddr

lib/Echidna/Events.hs

@@ -26,7 +26,7 @@ import EVM.Format (showValues, showError, contractNamePart)
 import EVM.Solidity (SolcContract(..))
 import EVM.Types
 
-import Echidna.Symbolic (forceWord, forceBuf)
+import Echidna.SymExec.Symbolic (forceWord, forceBuf)
 
 type EventMap = Map W256 Event
 type Events = [Text]

lib/Echidna/Exec.hs

@@ -35,7 +35,7 @@ import EVM.Types hiding (Env, Gas)
 import Echidna.Events (emptyEvents)
 import Echidna.Onchain (safeFetchContractFrom, safeFetchSlotFrom)
 import Echidna.SourceMapping (lookupUsingCodehashOrInsert)
-import Echidna.Symbolic (forceBuf)
+import Echidna.SymExec.Symbolic (forceBuf)
 import Echidna.Transaction
 import Echidna.Types (ExecException(..), fromEVM, emptyAccount)
 import Echidna.Types.Config (Env(..), EConfig(..), UIConf(..), OperationMode(..), OutputFormat(Text))

lib/Echidna/Mutator/Corpus.hs

@@ -1,7 +1,6 @@
 module Echidna.Mutator.Corpus where
 
 import Control.Monad.Random.Strict (MonadRandom, getRandomR, weighted)
-import Data.Set (Set)
 import Data.Set qualified as Set
 
 import Echidna.Mutator.Array
@@ -63,7 +62,7 @@ selectAndCombine f ql corpus gtxs = do
 
 selectFromCorpus
   :: MonadRandom m
-  => Set (Int, [Tx])
+  => Corpus
   -> m [Tx]
 selectFromCorpus =
   weighted . map (\(i, txs) -> (txs, fromIntegral i)) . Set.toDescList

lib/Echidna/Onchain.hs

@@ -33,7 +33,7 @@ import EVM.Solidity (SourceCache(..), SolcContract (..))
 import EVM.Types hiding (Env)
 
 import Echidna.Orphans.JSON ()
-import Echidna.Symbolic (forceWord, forceBuf)
+import Echidna.SymExec.Symbolic (forceWord, forceBuf)
 import Echidna.Types (emptyAccount)
 import Echidna.Types.Campaign (CampaignConf(..))
 import Echidna.Types.Config (Env(..), EConfig(..))

lib/Echidna/Output/Corpus.hs

@@ -11,11 +11,12 @@ import Data.Time (LocalTime)
 import System.Directory (createDirectoryIfMissing, makeRelativeToCurrentDirectory, doesFileExist)
 import System.FilePath ((</>), (<.>))
 
-import Echidna.Campaign (pushCampaignEvent)
 import Echidna.Types.Config
 import Echidna.Types.Campaign
 import Echidna.Types.Test (EchidnaTest(..))
+import Echidna.Types.Worker 
 import Echidna.Types.Tx (Tx)
+import Echidna.Worker (pushCampaignEvent)
 import Echidna.Utility (listDirectory, withCurrentDirectory)
 
 saveTxs :: Env -> FilePath -> [[Tx]] -> IO ()

lib/Echidna/Output/JSON.hs

@@ -68,10 +68,11 @@ instance ToJSON TestType where
   toJSON Property = "property"
   toJSON Assertion = "assertion"
 
-data TestStatus = Fuzzing | Shrinking | Solved | Passed | Error
+data TestStatus = Fuzzing | Shrinking | Solved | Verified | Passed | Error
 
 instance ToJSON TestStatus where
   toJSON Fuzzing = "fuzzing"
+  toJSON Verified = "verified"
   toJSON Shrinking = "shrinking"
   toJSON Solved = "solved"
   toJSON Passed = "passed"
@@ -127,6 +128,7 @@ mapTest dappInfo test =
   mapTestState T.Open _ = (Fuzzing, Nothing, Nothing)
   mapTestState T.Passed _ = (Passed, Nothing, Nothing)
   mapTestState T.Solved txs = (Solved, Just $ mapTx <$> txs, Nothing)
+  mapTestState T.Unsolvable _ = (Verified, Nothing, Nothing)
   mapTestState (T.Large _) txs = (Shrinking, Just $ mapTx <$> txs, Nothing)
   mapTestState (T.Failed e) _ = (Error, Nothing, Just $ show e) -- TODO add (show e)
 

lib/Echidna/Server.hs

@@ -10,8 +10,9 @@ import Data.Word (Word16)
 import Network.Wai.EventSource (ServerEvent(..), eventSourceAppIO)
 import Network.Wai.Handler.Warp (run)
 
-import Echidna.Types.Campaign
+import Echidna.Worker()
 import Echidna.Types.Config (Env(..))
+import Echidna.Types.Worker
 
 newtype SSE = SSE (LocalTime, CampaignEvent)
 
@@ -52,7 +53,8 @@ runSSEServer serverStopVar env port nworkers = do
                     TestFalsified _ -> "test_falsified"
                     TestOptimized _ -> "test_optimized"
                     NewCoverage {} -> "new_coverage"
-                    SymNoNewCoverage -> "sym_no_new_coverage"
+                    SymExecLog _ -> "sym_exec_log"
+                    SymExecError _ -> "sym_exec_error"
                     TxSequenceReplayed {} -> "tx_sequence_replayed"
                     TxSequenceReplayFailed {} -> "tx_sequence_replay_failed"
                     WorkerStopped _ -> "worker_stopped"

lib/Echidna/Solidity.hs

@@ -347,6 +347,7 @@ mkWorld SolConf{sender, testMode} sigMap maybeContract slitherInfo contracts =
   let
     eventMap = Map.unions $ map (.eventMap) contracts
     payableSigs = filterResults maybeContract slitherInfo.payableFunctions
+    assertSigs = filterResults maybeContract (assertFunctionList <$> slitherInfo.asserts)
     as = if isAssertionMode testMode then filterResults maybeContract (assertFunctionList <$> slitherInfo.asserts) else []
     cs = if isDapptestMode testMode then [] else filterResults maybeContract slitherInfo.constantFunctions \\ as
     (highSignatureMap, lowSignatureMap) = prepareHashMaps cs as $
@@ -355,6 +356,7 @@ mkWorld SolConf{sender, testMode} sigMap maybeContract slitherInfo contracts =
            , highSignatureMap
            , lowSignatureMap
            , payableSigs
+           , assertSigs
            , eventMap
            }
 

lib/Echidna/SourceMapping.hs

@@ -9,7 +9,7 @@ import Data.Map.Strict qualified as Map
 import Data.Map.Strict (Map)
 import Data.Maybe (mapMaybe)
 import Data.Vector qualified as V
-import Echidna.Symbolic (forceWord)
+import Echidna.SymExec.Symbolic (forceWord)
 import EVM.Dapp (DappInfo(..), findSrc)
 import EVM.Expr (maybeLitByteSimp)
 import EVM.Solidity (SolcContract(..))

lib/Echidna/SymExec.hs

@@ -1,258 +0,0 @@
-{-# OPTIONS_GHC -Wno-gadt-mono-local-binds #-}
-
-module Echidna.SymExec (createSymTx) where
-
-import Control.Applicative ((<|>))
-import Control.Concurrent.Async (mapConcurrently)
-import Control.Concurrent (ThreadId, forkIO)
-import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar)
-import Control.Monad (forM)
-import Control.Monad.IO.Class (liftIO)
-import Control.Monad.Reader (runReaderT)
-import Data.ByteString.Lazy qualified as BS
-import Data.Foldable (fold)
-import Data.Function ((&))
-import Data.List (singleton)
-import Data.Map qualified as Map
-import Data.Maybe (fromMaybe, mapMaybe, isJust, fromJust)
-import Data.Set (Set)
-import Data.Set qualified as Set
-import Data.Text (Text)
-import Data.Text qualified as T
-import Data.Vector (toList, fromList)
-import Optics.Core ((.~), (%))
-import Echidna.Solidity (chooseContract)
-import Echidna.Types (fromEVM)
-import Echidna.Types.Campaign (CampaignConf(..))
-import Echidna.Types.Config (EConfig(..))
-import Echidna.Types.Solidity (SolConf(..))
-import EVM.ABI (AbiValue(..), AbiType(..), Sig(..), decodeAbiValue)
-import EVM.Expr (simplify)
-import EVM.Fetch qualified as Fetch
-import EVM (loadContract, resetState)
-import EVM.Effects (defaultEnv)
-import EVM.Solidity (SolcContract(..), Method(..))
-import EVM.Solvers (withSolvers, Solver(Z3), SolverGroup, checkSatWithProps)
-import EVM.SymExec (interpret, runExpr, abstractVM, mkCalldata, IterConfig(..), LoopHeuristic (Naive), flattenExpr, extractProps)
-import EVM.Types (Addr, VM(..), Frame(..), FrameState(..), VMType(..), Env(..), Expr(..), EType(..), Query(..), Prop(..), SMTCex(..), SMTResult, ProofResult(..), BranchCondition(..), W256, word256Bytes, word)
-import EVM.Traversals (mapExpr)
-import Control.Monad.ST (stToIO, RealWorld)
-import Control.Monad.State.Strict (execState, runStateT)
-import Echidna.Types.Tx (Tx(..), TxCall(..), maxGasPerBlock)
-
-
--- | Uses symbolic execution to find transactions which would increase coverage.
--- Spawns a new thread; returns its thread ID as the first return value.
--- The second return value is an MVar which is populated with transactions
---   once the symbolic execution is finished.
--- Also takes an optional Tx argument; this is used as the transaction
---   to follow during concolic execution. If none is provided, we do full
---   symbolic execution.
---   The Tx argument, if present, must have a .call value of type SolCall.
-createSymTx :: EConfig -> Maybe Text -> [SolcContract] -> Maybe Tx -> VM Concrete RealWorld -> IO (ThreadId, MVar [Tx])
-createSymTx cfg name cs tx vm = do
-  mainContract <- chooseContract cs name
-  exploreContract cfg mainContract tx vm
-
-exploreContract :: EConfig -> SolcContract -> Maybe Tx -> VM Concrete RealWorld -> IO (ThreadId, MVar [Tx])
-exploreContract conf contract tx vm = do
-  let
-    isConc = isJust tx
-    allMethods = Map.elems contract.abiMap
-    filterMethod name method = method.name == name &&
-      case conf.campaignConf.symExecTargets of
-        Just ms -> name `elem` ms
-        _       -> True
-    concMethods (Tx { call = SolCall (methodName, _) }) = filter (filterMethod methodName) allMethods
-    concMethods _ = error "`exploreContract` should only be called with Nothing or Just Tx{call=SolCall _} for its tx argument"
-    methods = maybe allMethods concMethods tx
-    timeout = Just (fromIntegral conf.campaignConf.symExecTimeout)
-    maxIters = if isConc then Nothing else Just conf.campaignConf.symExecMaxIters
-    askSmtIters = if isConc then 0 else conf.campaignConf.symExecAskSMTIters
-    iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = Naive }
-    rpcInfo = Nothing
-    defaultSender = fromJust $ fmap (.dst) tx <|> Set.lookupMin conf.solConf.sender <|> Just 0
-
-  threadIdChan <- newEmptyMVar
-  doneChan <- newEmptyMVar
-  resultChan <- newEmptyMVar
-
-  flip runReaderT defaultEnv $ withSolvers Z3 (fromIntegral conf.campaignConf.symExecNSolvers) 1 timeout $ \solvers -> do
-    threadId <- liftIO $ forkIO $ flip runReaderT defaultEnv $ do
-      res <- forM methods $ \method -> do
-        let
-          fetcher = concOrSymFetcher tx solvers rpcInfo
-          dst = conf.solConf.contractAddr
-        calldata@(cd, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
-        vmSym <- liftIO $ stToIO $ abstractVM calldata contract.runtimeCode Nothing False
-        vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm
-        let vm' = vmReset & execState (loadContract (LitAddr dst))
-                          & vmMakeSymbolic
-                          & #constraints .~ constraints
-                          & #state % #callvalue .~ TxValue
-                          & #state % #caller .~ SymAddr "caller"
-                          & #state % #calldata .~ cd
-                          & #env % #contracts .~ Map.union vmSym.env.contracts vm.env.contracts
-        -- TODO we might want to switch vm's state.baseState value to AbstractBase eventually.
-        -- Doing so might mess up concolic execution.
-        exprInter <- interpret fetcher iterConfig vm' runExpr
-        models <- liftIO $ mapConcurrently (\props -> runReaderT (checkSatWithProps solvers props) defaultEnv) $ manipulateExprInter isConc exprInter
-        pure $ mapMaybe (modelToTx dst method conf.solConf.sender defaultSender . fst) models
-      liftIO $ putMVar resultChan $ concat res
-      liftIO $ putMVar doneChan ()
-    liftIO $ putMVar threadIdChan threadId
-    liftIO $ takeMVar doneChan
-
-  threadId <- takeMVar threadIdChan
-  pure (threadId, resultChan)
-
--- | Turn the expression returned by `interpret` into Prop values to feed into the solver
-manipulateExprInter :: Bool -> Expr End -> [[Prop]]
-manipulateExprInter isConc = middleStep . map (extractProps . simplify) . flattenExpr . simplify where
-  middleStep = if isConc then middleStepConc else id
-  middleStepConc = map singleton . concatMap (go (PBool True))
-  go :: Prop -> [Prop] -> [Prop]
-  go _ [] = []
-  go acc (h:t) = (PNeg h `PAnd` acc) : go (h `PAnd` acc) t
-
--- | Sets result to Nothing, and sets gas to ()
-vmMakeSymbolic :: VM Concrete s -> VM Symbolic s
-vmMakeSymbolic vm
-  = VM
-  { result         = Nothing
-  , state          = frameStateMakeSymbolic vm.state
-  , frames         = map frameMakeSymbolic vm.frames
-  , env            = vm.env
-  , block          = vm.block
-  , tx             = vm.tx
-  , logs           = vm.logs
-  , traces         = vm.traces
-  , cache          = vm.cache
-  , burned         = ()
-  , iterations     = vm.iterations
-  , constraints    = vm.constraints
-  , config         = vm.config
-  , forks          = vm.forks
-  , currentFork    = vm.currentFork
-  , labels         = vm.labels
-  , osEnv          = vm.osEnv
-  , freshVar       = vm.freshVar
-  , exploreDepth   = vm.exploreDepth
-  }
-
-frameStateMakeSymbolic :: FrameState Concrete s -> FrameState Symbolic s
-frameStateMakeSymbolic fs
-  = FrameState
-  { contract     = fs.contract
-  , codeContract = fs.codeContract
-  , code         = fs.code
-  , pc           = fs.pc
-  , stack        = fs.stack
-  , memory       = fs.memory
-  , memorySize   = fs.memorySize
-  , calldata     = fs.calldata
-  , callvalue    = fs.callvalue
-  , caller       = fs.caller
-  , gas          = ()
-  , returndata   = fs.returndata
-  , static       = fs.static
-  , overrideCaller = fs.overrideCaller
-  , resetCaller  = fs.resetCaller
-  }
-
-frameMakeSymbolic :: Frame Concrete s -> Frame Symbolic s
-frameMakeSymbolic fr = Frame { context = fr.context, state = frameStateMakeSymbolic fr.state }
-
-modelToTx :: Addr -> Method -> Set Addr -> Addr -> SMTResult -> Maybe Tx
-modelToTx dst method senders fallbackSender result =
-  case result of
-    Cex cex ->
-      let
-        args = zipWith grabArg (snd <$> method.inputs) ["arg" <> T.pack (show n) | n <- [1..] :: [Int]]
-
-        grabArg t
-          = case t of
-              AbiUIntType _ -> grabNormalArg t
-              AbiIntType _ -> grabNormalArg t
-              AbiBoolType -> grabNormalArg t
-              AbiBytesType _ -> grabNormalArg t
-              AbiAddressType -> grabAddressArg
-              AbiArrayType n mt -> grabArrayArg n mt
-              AbiTupleType mt -> grabTupleArg mt
-              _ -> error "Unexpected ABI type in `modelToTx`"
-
-        grabNormalArg argType name
-          = case Map.lookup (Var name) cex.vars of
-              Just w ->
-                decodeAbiValue argType (BS.fromStrict (word256Bytes w))
-              Nothing -> -- put a placeholder
-                decodeAbiValue argType (BS.repeat 0)
-
-        grabAddressArg name = AbiAddress $ fromMaybe 0 $ Map.lookup (SymAddr name) cex.addrs
-
-        grabArrayArg nElem memberType name = AbiArray nElem memberType $ fromList [grabArg memberType $ name <> "-a-" <> T.pack (show n) | n <- [0..nElem] :: [Int]]
-
-        grabTupleArg memberTypes name = AbiTuple $ fromList [grabArg t $ name <> "-t-" <> T.pack (show n) | (n, t) <- zip ([0..] :: [Int]) (toList memberTypes)]
-
-        src_ = fromMaybe 0 $ Map.lookup (SymAddr "sender") cex.addrs
-        src = if Set.member src_ senders then src_ else fallbackSender
-
-        value = fromMaybe 0 $ Map.lookup TxValue cex.txContext
-
-      in Just Tx
-        { call = SolCall (method.name, args)
-        , src = src
-        , dst = dst
-        , gasprice = 0
-        , gas = maxGasPerBlock
-        , value = value
-        , delay = (0, 0)
-        }
-
-    _ -> Nothing
-
--- | Symbolic variable -> concrete value mapping used during concolic execution.
--- The third member in the tuple is the transaction value.
-type Substs = ([(Text, W256)], [(Text, Addr)], W256)
-
--- | Mirrors hevm's `symAbiArg` function; whenever that changes, we need to change this too
-genSubsts :: Tx -> Substs
-genSubsts (Tx { call = SolCall (_, abiVals), src, value }) = addOnFinalValues $ fold $ zipWith genVal abiVals (T.pack . ("arg" <>) . show <$> ([1..] :: [Int])) where
-  addOnFinalValues (a, b) = (a, ("sender", src):b, value)
-  genVal (AbiUInt _ i) name = ([(name, fromIntegral i)], [])
-  genVal (AbiInt _ i) name = ([(name, fromIntegral i)], [])
-  genVal (AbiBool b) name = ([(name, if b then 1 else 0)], [])
-  genVal (AbiAddress addr) name = ([], [(name, addr)])
-  genVal (AbiBytes n b) name | n > 0 && n <= 32 = ([(name, word b)], [])
-  genVal (AbiArray _ _ vals) name = fold $ zipWith genVal (toList vals) [name <> "-a-" <> T.pack (show n) | n <- [0..] :: [Int]]
-  genVal (AbiTuple vals) name = fold $ zipWith genVal (toList vals) [name <> "-t-" <> T.pack (show n) | n <- [0..] :: [Int]]
-  genVal _ _ = error "`genSubsts` is not implemented for all API types, mirroring hevm's `symAbiArg` function"
-genSubsts _ = error "`genSubsts` should only be called with a `SolCall` transaction argument"
-
--- | Apply substitutions into an expression
-substExpr :: Substs -> Expr a -> Expr a
-substExpr (sw, sa, val) = mapExpr go where
-  go v@(Var t) = maybe v Lit (lookup t sw)
-  go v@(SymAddr t) = maybe v LitAddr (lookup t sa)
-  go TxValue = Lit val
-  go e = e
-
--- | Fetcher used during concolic execution.
--- This is the most important function for concolic execution;
--- it determines what branch `interpret` should take.
--- We ensure that this fetcher is always used by setting askSMTIter to 0.
--- We determine what branch to take by substituting concrete values into
--- the provided `Prop`, and then simplifying.
--- We fall back on `Fetch.oracle`.
-concFetcher :: Substs -> SolverGroup -> Fetch.RpcInfo -> Fetch.Fetcher t m s
-concFetcher substs s r (PleaseAskSMT branchcondition pathconditions continue) =
-  case simplify (substExpr substs branchcondition) of
-    Lit n -> pure (continue (Case (n/=0)))
-    simplifiedExpr -> Fetch.oracle s r (PleaseAskSMT simplifiedExpr pathconditions continue)
-concFetcher _ s r q = Fetch.oracle s r q
-
--- | Depending on whether we're doing concolic or full symbolic execution,
--- choose a fetcher to be used in `interpret` (either `concFetcher` or `Fetch.oracle`).
-concOrSymFetcher :: Maybe Tx -> SolverGroup -> Fetch.RpcInfo -> Fetch.Fetcher t m s
-concOrSymFetcher (Just c) = concFetcher $ genSubsts c
-concOrSymFetcher Nothing = Fetch.oracle

lib/Echidna/SymExec/Common.hs

@@ -0,0 +1,249 @@
+module Echidna.SymExec.Common where
+
+import Control.Monad.IO.Unlift (MonadUnliftIO, liftIO)
+import Data.ByteString.Lazy qualified as BS
+import Data.Function ((&))
+import Data.Map qualified as Map
+import Data.Maybe (fromMaybe, mapMaybe)
+import Data.Set (Set)
+import Data.Set qualified as Set
+import Data.Text qualified as T
+import Data.Vector (toList, fromList)
+import GHC.IORef (IORef, readIORef)
+import Optics.Core ((.~), (%), (%~))
+import EVM.ABI (abiKind, AbiKind(Dynamic), AbiValue(..), AbiType(..), Sig(..), decodeAbiValue)
+import EVM.Fetch qualified as Fetch
+import EVM (loadContract, resetState, forceLit)
+import EVM.Effects (TTY, ReadConfig)
+import EVM.Solidity (SolcContract(..), Method(..))
+import EVM.Solvers (SolverGroup)
+import EVM.SymExec (abstractVM, mkCalldata, verifyInputs, VeriOpts(..), checkAssertions)
+import EVM.Types (Addr, Frame(..), FrameState(..), VMType(..), EType(..), Expr(..), word256Bytes, Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), Query(..))
+import qualified EVM.Types (VM(..), Env(..))
+import EVM.Format (formatPartial)
+import Control.Monad.ST (stToIO, RealWorld)
+import Control.Monad.State.Strict (execState, runStateT)
+
+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]
+
+data TxOrError = TxFromResult Tx | SMTErrorFromResult String
+  deriving (Show)
+
+extractTxs :: [TxOrError] -> [Tx]
+extractTxs = mapMaybe (\case
+  TxFromResult tx -> Just tx
+  _ -> Nothing)
+
+extractErrors :: [TxOrError] -> [String]
+extractErrors = mapMaybe (\case
+  SMTErrorFromResult err -> Just err
+  _ -> Nothing)
+
+suitableForSymExec :: Method -> Bool
+suitableForSymExec m = not $ null m.inputs 
+  && null (filter (\(_, t) -> abiKind t == Dynamic) m.inputs) 
+  && not (T.isInfixOf "_no_symexec" m.name)
+
+-- | Sets result to Nothing, and sets gas to ()
+vmMakeSymbolic :: W256 -> W256 -> EVM.Types.VM Concrete s -> EVM.Types.VM Symbolic s
+vmMakeSymbolic maxTimestampDiff maxNumberDiff vm
+  = EVM.Types.VM
+  { result         = Nothing
+  , state          = frameStateMakeSymbolic vm.state
+  , frames         = map frameMakeSymbolic vm.frames
+  , env            = vm.env
+  , block          = blockMakeSymbolic vm.block
+  , tx             = vm.tx
+  , logs           = vm.logs
+  , traces         = vm.traces
+  , cache          = vm.cache
+  , burned         = ()
+  , iterations     = vm.iterations
+  , constraints    = addBlockConstraints maxTimestampDiff maxNumberDiff vm.block vm.constraints
+  , config         = vm.config
+  , forks          = vm.forks
+  , currentFork    = vm.currentFork
+  , labels         = vm.labels
+  , osEnv          = vm.osEnv
+  , freshVar       = vm.freshVar
+  , exploreDepth   = 0
+  , keccakPreImgs  = vm.keccakPreImgs
+  }
+
+blockMakeSymbolic :: Block -> Block
+blockMakeSymbolic b
+  = b {
+      timestamp = Var "symbolic_block_timestamp"
+    , number = Var "symbolic_block_number"
+  }
+
+addBlockConstraints :: W256 -> W256 -> Block -> [Prop] -> [Prop]
+addBlockConstraints maxTimestampDiff maxNumberDiff block cs =
+  cs ++ [
+    PGEq (Var "symbolic_block_timestamp") (block.timestamp), PLEq (Sub (Var "symbolic_block_timestamp") (block.timestamp)) $ Lit maxTimestampDiff,
+    PGEq (Var "symbolic_block_number") (block.number), PLEq (Sub (Var "symbolic_block_number") (block.number)) $ Lit maxNumberDiff
+  ]
+
+senderConstraints :: Set Addr -> [Prop]
+senderConstraints as = [foldr (\a b -> POr b (PEq (SymAddr "caller") (LitAddr a))) (PBool False) $ Set.toList as]
+
+frameStateMakeSymbolic :: FrameState Concrete s -> FrameState Symbolic s
+frameStateMakeSymbolic fs
+  = FrameState
+  { contract     = fs.contract
+  , codeContract = fs.codeContract
+  , code         = fs.code
+  , pc           = fs.pc
+  , stack        = fs.stack
+  , memory       = fs.memory
+  , memorySize   = fs.memorySize
+  , calldata     = fs.calldata
+  , callvalue    = fs.callvalue
+  , caller       = fs.caller
+  , gas          = ()
+  , returndata   = fs.returndata
+  , static       = fs.static
+  , overrideCaller = fs.overrideCaller
+  , resetCaller  = fs.resetCaller
+  }
+
+frameMakeSymbolic :: Frame Concrete s -> Frame Symbolic s
+frameMakeSymbolic fr = Frame { context = fr.context, state = frameStateMakeSymbolic fr.state }
+
+-- | Convert a n-bit unsigned integer to a n-bit signed integer.
+uintToInt :: W256 -> Integer
+uintToInt w = fromIntegral (w - 2 ^ (256 :: Int))
+
+modelToTx :: Addr -> Expr EWord -> Expr EWord -> Method -> Set Addr -> Addr -> ProofResult SMTCex String -> TxOrError
+modelToTx dst oldTimestamp oldNumber method senders fallbackSender result =
+  case result of
+    Cex cex ->
+      let
+        args = zipWith grabArg (snd <$> method.inputs) ["arg" <> T.pack (show n) | n <- [1..] :: [Int]]
+
+        grabArg t
+          = case t of
+              AbiUIntType _ -> grabNormalArg t
+              AbiIntType _ -> grabNormalArgInt t
+              AbiBoolType -> grabNormalArg t
+              AbiBytesType _ -> grabNormalArg t
+              AbiAddressType -> grabAddressArg
+              AbiArrayType n mt -> grabArrayArg n mt
+              AbiTupleType mt -> grabTupleArg mt
+              _ -> error "Unexpected ABI type in `modelToTx`"
+
+        grabNormalArg argType name
+          = case Map.lookup (Var name) cex.vars of
+              Just w ->
+                decodeAbiValue argType (BS.fromStrict (word256Bytes w))
+              Nothing -> -- put a placeholder
+                decodeAbiValue argType (BS.repeat 0)
+
+        grabNormalArgInt argType name
+          = case Map.lookup (Var name) cex.vars of
+              Just w ->
+                case argType of
+                  AbiIntType n -> AbiInt n (fromIntegral (uintToInt w))
+                  _ -> error "Expected AbiIntType"
+              Nothing -> -- put a placeholder
+                decodeAbiValue argType (BS.repeat 0)
+
+        grabAddressArg name = AbiAddress $ fromMaybe 0 $ Map.lookup (SymAddr name) cex.addrs
+
+        grabArrayArg nElem memberType name = AbiArray nElem memberType $ fromList [grabArg memberType $ name <> "-a-" <> T.pack (show n) | n <- [0..nElem - 1] :: [Int]]
+
+        grabTupleArg memberTypes name = AbiTuple $ fromList [grabArg t $ name <> "-t-" <> T.pack (show n) | (n, t) <- zip ([0..] :: [Int]) (toList memberTypes)]
+
+        src_ = fromMaybe 0 $ Map.lookup (SymAddr "caller") cex.addrs
+        src = if Set.member src_ senders then src_ else fallbackSender
+        value = fromMaybe 0 $ Map.lookup TxValue cex.txContext
+
+        -- If symbolic values for delay (timestamp, number) are unconstrained, no delay is applied
+        newTimestamp = fromMaybe 0 $ Map.lookup (Var "symbolic_block_timestamp") cex.vars
+        diffTimestamp = if newTimestamp == 0 then 0 else newTimestamp - forceLit oldTimestamp
+
+        newNumber = fromMaybe 0 $ Map.lookup (Var "symbolic_block_number") cex.vars
+        diffNumber = if newNumber == 0 then 0 else newNumber - forceLit oldNumber
+
+      in TxFromResult $ Tx
+        { call = SolCall (method.name, args)
+        , src = src
+        , dst = dst
+        , gasprice = 0
+        , gas = maxGasPerBlock
+        , value = value
+        , delay = (diffTimestamp, diffNumber)
+        }
+
+    Error err -> SMTErrorFromResult err
+    Unknown err -> SMTErrorFromResult err
+    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
+  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 info
+
+rpcFetcher :: Functor f =>
+  f a -> Maybe W256 -> f (Fetch.BlockNumber, a)
+
+rpcFetcher rpc block = (,) block' <$> rpc
+  where block' = maybe Fetch.Latest Fetch.BlockNumber block
+
+removeUnknownResults :: [ProofResult SMTCex String] -> ([ProofResult SMTCex String], [ProofResult SMTCex String])
+removeUnknownResults results =
+  let
+    known = filter (\case Unknown _ -> False ; _ -> True) results
+    unknown = filter (\case Unknown _ -> True; _ -> False) results
+  in (known, unknown)
+
+getUnknownLogs :: [ProofResult SMTCex String] -> [T.Text]
+getUnknownLogs = mapMaybe (\case
+  Error err -> Just $ T.pack err
+  _ -> Nothing)
+
+exploreMethod :: (MonadUnliftIO m, ReadConfig m, TTY m) =>
+  Method -> SolcContract -> EVM.Types.VM Concrete RealWorld -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> IORef ContractCache -> IORef SlotCache -> m ([TxOrError], PartialsLogs)
+  
+exploreMethod method contract vm defaultSender conf veriOpts solvers rpcInfo contractCacheRef slotCacheRef = do
+  --liftIO $ putStrLn ("Exploring: " ++ T.unpack method.methodSignature)
+  --pushWorkerEvent undefined
+  calldataSym@(cd, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
+  let
+    fetcher = cachedOracle contractCacheRef slotCacheRef solvers rpcInfo
+    dst = conf.solConf.contractAddr
+    vmSym = abstractVM calldataSym contract.runtimeCode Nothing False
+  vmSym' <- liftIO $ stToIO vmSym
+  vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm
+  let vm' = vmReset & execState (loadContract (LitAddr dst))
+                    & vmMakeSymbolic conf.txConf.maxTimeDelay conf.txConf.maxBlockDelay
+                    & #constraints %~ (++ constraints ++ (senderConstraints conf.solConf.sender))
+                    & #state % #callvalue .~ TxValue
+                    & #state % #caller .~ SymAddr "caller"
+                    & #state % #calldata .~ cd
+                    & #env % #contracts .~ (Map.union vmSym'.env.contracts vm.env.contracts)
+  -- TODO we might want to switch vm's state.baseState value to to AbstractBase eventually.
+  -- Doing so might mess up concolic execution.
+  (_, models, partials) <- verifyInputs solvers veriOpts fetcher vm' (Just $ checkAssertions [0x1])
+  let results = map fst models
+  --liftIO $ mapM_ TIO.putStrLn partials
+  return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender) results, map formatPartial partials)

lib/Echidna/SymExec/Exploration.hs

@@ -0,0 +1,122 @@
+{-# OPTIONS_GHC -Wno-gadt-mono-local-binds #-}
+
+module Echidna.SymExec.Exploration where
+
+import Control.Applicative ((<|>))
+import Control.Concurrent (ThreadId, forkIO)
+import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar)
+import Control.Monad.Catch (MonadThrow(..))
+import Control.Monad.IO.Class (MonadIO)
+import Control.Monad.Reader (MonadReader, ask, asks, runReaderT, liftIO)
+import Control.Monad.State.Strict (MonadState)
+import Data.Map qualified as Map
+import Data.Maybe (fromJust)
+import Data.Set qualified as Set
+import Data.Text (unpack, Text)
+import Data.Text.Encoding (encodeUtf8)
+import Data.List.NonEmpty (fromList) 
+import EVM.Effects (defaultEnv, defaultConfig, Config(..), Env(..))
+import EVM.Solidity (SolcContract(..), Method(..))
+import EVM.Solvers (withSolvers)
+import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..), defaultVeriOpts)
+import EVM.Types (abiKeccak, FunctionSelector, VMType(..))
+import qualified EVM.Types (VM(..))
+import Control.Monad.ST (RealWorld)
+
+import Echidna.Types.Campaign (CampaignConf(..), WorkerState)
+import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..))
+import Echidna.Types.World (World(..))
+import Echidna.Types.Solidity (SolConf(..))
+import Echidna.Types.Tx (Tx(..), TxCall(..))
+import Echidna.Types.Worker (WorkerEvent(..))
+import Echidna.Types.Random (rElem)
+import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, rpcFetcher, TxOrError(..), PartialsLogs)
+import Echidna.Worker (pushWorkerEvent)
+
+-- | Uses symbolic execution to find transactions which would increase coverage.
+-- Spawns a new thread; returns its thread ID as the first return value.
+-- The second return value is an MVar which is populated with transactions
+--   once the symbolic execution is finished.
+-- Also takes an optional Tx argument; this is used as the transaction
+--   to symbolize. If none is provided, we do full
+--   symbolic execution.
+--   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 (methodName, _) }) contract failedProperties = do
+  env <- ask  
+  let allMethods = Map.assocs contract.abiMap
+      assertSigs = env.world.assertSigs
+      (selector, method) = case filter (\(_, m) -> m.name == methodName) allMethods of
+        [] -> error $ "Method " ++ show methodName ++ " not found in contract ABI"
+        (x:_) -> x
+
+  if (null assertSigs || selector `elem` assertSigs) && suitableForSymExec method && (unpack method.methodSignature) `notElem` failedProperties 
+  then return $ Just method
+  else return Nothing
+
+getTargetMethodFromTx _ _ _ = return Nothing
+
+-- This function selects a random method from the contract's ABI to explore.
+-- It uses the campaign configuration to determine which methods are suitable for symbolic execution.
+-- Additionally, it filter methods that are associated with failed properties, if any.
+getRandomTargetMethod :: (MonadIO m, MonadReader Echidna.Types.Config.Env m) => SolcContract -> Maybe [Text] -> [String] -> m (Maybe Method)
+getRandomTargetMethod contract targets failedProperties = do
+  env <- ask
+  let allMethods = Map.assocs contract.abiMap
+      assertSigs = env.world.assertSigs
+      filterFunc (selector, method) = (null assertSigs || selector `elem` assertSigs) && suitableForSymExec method && (unpack method.methodSignature) `notElem` failedProperties
+      filteredMethods = filter filterFunc allMethods
+  
+  case (targets, filteredMethods) of
+    (Just ms, _) -> liftIO $ rElem (fromList $ map (Just . snd) $ filter (\(_, m) -> m.name `elem` ms) allMethods)
+    (_,      []) -> return Nothing
+    _            -> liftIO $ rElem (fromList $ map (Just . snd) filteredMethods)
+
+
+-- | Filters methods based on the campaign configuration.
+-- If symExecTargets is Just, it filters methods by their name.
+-- If symExecTargets is Nothing, it filters methods by their signature and checks if they are suitable for symbolic execution.
+-- If the list of assertSigs is empty, it does not filter by signature (to workaround a potential bug in Slither).
+filterTarget :: Maybe [Text] -> [FunctionSelector] -> Maybe Tx -> Method -> Bool
+filterTarget symExecTargets assertSigs tx method =
+  case (symExecTargets, tx) of
+    (Just ms, _)                                       -> method.name `elem` ms
+    (_,  Just (Tx { call = SolCall (methodName, _) })) -> (null assertSigs || methodSig `elem` assertSigs) && method.name == methodName && suitableForSymExec method
+    _                                                  -> (null assertSigs || methodSig `elem` assertSigs) && suitableForSymExec method
+ where methodSig = abiKeccak $ encodeUtf8 method.methodSignature
+
+exploreContract :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) => SolcContract -> Method -> EVM.Types.VM Concrete RealWorld -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+exploreContract contract method vm = do
+  conf <- asks (.cfg)
+  contractCacheRef <- asks (.fetchContractCache)
+  slotCacheRef <- asks (.fetchSlotCache)
+  let
+    timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout)
+    maxIters = Just conf.campaignConf.symExecMaxIters
+    maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore)
+    askSmtIters = conf.campaignConf.symExecAskSMTIters
+    rpcInfo = rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock)
+    defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0
+
+  threadIdChan <- liftIO newEmptyMVar
+  doneChan <- liftIO newEmptyMVar
+  resultChan <- liftIO newEmptyMVar
+  let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = Naive}
+  let veriOpts = defaultVeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo}
+  let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text
+  let runtimeEnv = defaultEnv { config = defaultConfig { maxWidth = 5, maxDepth = maxExplore, maxBufSize = 12, promiseNoReent = True, debug = isNonInteractive, dumpQueries = False, numCexFuzz = 100 } }
+  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 vm defaultSender conf veriOpts solvers rpcInfo contractCacheRef slotCacheRef
+      liftIO $ putMVar resultChan res
+      liftIO $ putMVar doneChan ()
+    liftIO $ putMVar threadIdChan threadId
+    liftIO $ takeMVar doneChan
+
+  threadId <- liftIO $ takeMVar threadIdChan
+  pure (threadId, resultChan)

lib/Echidna/SymExec/Symbolic.hs

@@ -1,7 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 
-module Echidna.Symbolic where
+module Echidna.SymExec.Symbolic where
 
 import Data.ByteString (ByteString)
 import EVM.Types (Expr(..), EType(..), W256, Addr)

lib/Echidna/SymExec/Verification.hs

@@ -0,0 +1,58 @@
+module Echidna.SymExec.Verification where
+
+import Control.Applicative ((<|>))
+import Control.Concurrent (ThreadId, forkIO)
+import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar)
+import Control.Monad.Catch (MonadThrow(..))
+import Control.Monad.IO.Class (MonadIO)
+import Control.Monad.Reader (MonadReader, asks, runReaderT, liftIO)
+import Control.Monad.State.Strict (MonadState)
+import Data.Maybe (fromJust)
+import Data.Set qualified as Set
+import EVM.Effects (defaultEnv, defaultConfig, Config(..), Env(..))
+import EVM.Solidity (SolcContract(..), Method(..))
+import EVM.Solvers (withSolvers)
+import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..), defaultVeriOpts)
+import EVM.Types (VMType(..))
+import qualified EVM.Types (VM(..))
+import Control.Monad.ST (RealWorld)
+
+import Echidna.Types.Campaign (CampaignConf(..), WorkerState)
+import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..))
+import Echidna.Types.Solidity (SolConf(..))
+import Echidna.Types.Worker (WorkerEvent(..))
+import Echidna.SymExec.Common (rpcFetcher, exploreMethod, TxOrError(..), PartialsLogs)
+import Echidna.Worker (pushWorkerEvent)
+
+verifyMethod :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m) => Method -> SolcContract -> EVM.Types.VM Concrete RealWorld -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+verifyMethod method contract vm = do
+  conf <- asks (.cfg)
+  contractCacheRef <- asks (.fetchContractCache)
+  slotCacheRef <- asks (.fetchSlotCache)  
+  let
+    timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout)
+    maxIters = Just conf.campaignConf.symExecMaxIters
+    maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore)
+    askSmtIters = conf.campaignConf.symExecAskSMTIters
+    rpcInfo = rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock)
+    defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0
+
+  threadIdChan <- liftIO newEmptyMVar
+  doneChan <- liftIO newEmptyMVar
+  resultChan <- liftIO newEmptyMVar
+  let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = Naive}
+  let veriOpts = defaultVeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo}
+  let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text
+  let runtimeEnv = defaultEnv { config = defaultConfig { maxWidth = 5, maxDepth = maxExplore, maxBufSize = 12, promiseNoReent = False, debug = isNonInteractive, numCexFuzz = 100 } }
+  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 vm defaultSender conf veriOpts solvers rpcInfo contractCacheRef slotCacheRef
+      liftIO $ putMVar resultChan (res, partials)
+      liftIO $ putMVar doneChan ()
+    liftIO $ putMVar threadIdChan threadId
+    liftIO $ takeMVar doneChan
+
+  threadId <- liftIO $ takeMVar threadIdChan
+  pure (threadId, resultChan)

lib/Echidna/Test.hs

@@ -20,7 +20,7 @@ import EVM.Types hiding (Env)
 import Echidna.ABI
 import Echidna.Events (Events, extractEvents)
 import Echidna.Exec
-import Echidna.Symbolic (forceBuf)
+import Echidna.SymExec.Symbolic (forceBuf)
 import Echidna.Types.Config
 import Echidna.Types.Signature (SolSignature)
 import Echidna.Types.Test

lib/Echidna/Transaction.hs

@@ -27,7 +27,7 @@ import EVM.Types hiding (Env, Gas, VMOpts(timestamp, gasprice))
 import Echidna.ABI
 import Echidna.Orphans.JSON ()
 import Echidna.SourceMapping (lookupUsingCodehash)
-import Echidna.Symbolic (forceWord, forceAddr)
+import Echidna.SymExec.Symbolic (forceWord, forceAddr)
 import Echidna.Types (fromEVM, Gas)
 import Echidna.Types.Config (Env(..), EConfig(..))
 import Echidna.Types.Random

lib/Echidna/Types/Cache.hs

@@ -0,0 +1,9 @@
+module Echidna.Types.Cache where
+
+import Data.Map (Map)
+import Data.Text (Text)
+import EVM.Types (W256, Addr, Contract)
+
+type ContractCache = Map Addr (Maybe Contract)
+type SlotCache = Map Addr (Map W256 (Maybe W256))
+type ContractNameCache = Map W256 Text

lib/Echidna/Types/Campaign.hs

@@ -1,17 +1,15 @@
 module Echidna.Types.Campaign where
 
 import Control.Concurrent (ThreadId)
-import Data.Aeson
 import Data.Text (Text)
-import Data.Text qualified as T
 import Data.Word (Word8, Word16)
 import GHC.Conc (numCapabilities)
 
-import Echidna.ABI (GenDict, emptyDict, encodeSig)
+import EVM.Solvers (Solver(..))
+
+import Echidna.ABI (GenDict, emptyDict)
 import Echidna.Types
 import Echidna.Types.Coverage (CoverageFileType, CoverageMap)
-import Echidna.Types.Test (TestType (..), EchidnaTest(..))
-import Echidna.Types.Tx (Tx)
 
 -- | Configuration for running an Echidna 'Campaign'.
 data CampaignConf = CampaignConf
@@ -43,10 +41,12 @@ data CampaignConf = CampaignConf
     -- ^ Server-Sent Events HTTP port number, if missing server is not ran
   , symExec            :: Bool
     -- ^ Whether to add an additional symbolic execution worker
-  , symExecConcolic    :: Bool
-    -- ^ Whether symbolic execution will be concolic (vs full symbolic execution)
-    -- Only relevant if symExec is True
+  , symExecSMTSolver   :: Solver
+    -- ^ SMT solver to use for symbolic execution.
+    -- Supported solvers: "cvc5", "z3" and "bitwuzla"
   , symExecTargets     :: Maybe [Text]
+    -- ^ List of target functions for symbolic execution.
+    -- If this is 'Nothing', all functions are considered targets.
   , symExecTimeout     :: Int
     -- ^ Timeout for symbolic execution SMT solver queries.
     -- Only relevant if symExec is True
@@ -55,102 +55,16 @@ data CampaignConf = CampaignConf
     -- Only relevant if symExec is True
   , symExecMaxIters    :: Integer
     -- ^ Number of times we may revisit a particular branching point.
-    -- Only relevant if symExec is True and symExecConcolic is False
+    -- Only relevant if symExec is True
   , symExecAskSMTIters :: Integer
     -- ^ Number of times we may revisit a particular branching point
     -- before we consult the SMT solver to check reachability.
-    -- Only relevant if symExec is True and symExecConcolic is False
+    -- Only relevant if symExec is True
+  , symExecMaxExplore :: Integer
+    -- ^ Maximum number of states to explore before we stop exploring it.
+    -- Only relevant if symExec is True
   }
 
-data WorkerType = FuzzWorker | SymbolicWorker deriving (Eq)
-
-type WorkerId = Int
-
-data CampaignEvent
-  = WorkerEvent WorkerId WorkerType WorkerEvent
-  | Failure String
-  | ReproducerSaved String -- filename
-
-data WorkerEvent
-  = TestFalsified !EchidnaTest
-  | TestOptimized !EchidnaTest
-  | NewCoverage { points :: !Int, numCodehashes :: !Int, corpusSize :: !Int, transactions :: [Tx] }
-  | SymNoNewCoverage
-  | TxSequenceReplayed FilePath !Int !Int
-  | TxSequenceReplayFailed FilePath Tx
-  | WorkerStopped WorkerStopReason
-  -- ^ This is a terminal event. Worker exits and won't push any events after
-  -- this one
-  deriving Show
-
-instance ToJSON WorkerEvent where
-  toJSON = \case
-    TestFalsified test -> toJSON test
-    TestOptimized test -> toJSON test
-    NewCoverage { points, numCodehashes, corpusSize } ->
-      object [ "coverage" .= points, "contracts" .= numCodehashes, "corpus_size" .= corpusSize]
-    SymNoNewCoverage -> object []
-    TxSequenceReplayed file current total ->
-      object [ "file" .= file, "current" .= current, "total" .= total ]
-    TxSequenceReplayFailed file tx ->
-      object [ "file" .= file, "tx" .= tx ]
-    WorkerStopped reason -> object [ "reason" .= show reason ]
-
-data WorkerStopReason
-  = TestLimitReached
-  | SymbolicDone
-  | TimeLimitReached
-  | FastFailed
-  | Killed !String
-  | Crashed !String
-  deriving Show
-
-ppCampaignEvent :: CampaignEvent -> String
-ppCampaignEvent = \case
-  WorkerEvent _ _ e -> ppWorkerEvent e
-  Failure err -> err
-  ReproducerSaved f -> "Saved reproducer to " <> f
-
-ppWorkerEvent :: WorkerEvent -> String
-ppWorkerEvent = \case
-  TestFalsified test ->
-    "Test " <> T.unpack (showTest test) <> " falsified!"
-  TestOptimized test ->
-    let name = case test.testType of OptimizationTest n _ -> n; _ -> error "fixme"
-    in "New maximum value of " <> T.unpack name <> ": " <> show test.value
-  NewCoverage { points, numCodehashes, corpusSize } ->
-    "New coverage: " <> show points <> " instr, "
-      <> show numCodehashes <> " contracts, "
-      <> show corpusSize <> " seqs in corpus"
-  SymNoNewCoverage ->
-    "Symbolic execution finished with no new coverage."
-  TxSequenceReplayed file current total ->
-    "Sequence replayed from corpus file " <> file <> " (" <> show current <> "/" <> show total <> ")"
-  TxSequenceReplayFailed file tx ->
-    "WARNING: Sequence replay from corpus file " <> file <> " failed. " <>
-    "The destination contract is not deployed for this transaction: " <> show tx <> ". " <>
-    "Remove the file or the transaction to fix the issue."
-  WorkerStopped TestLimitReached ->
-    "Test limit reached. Stopping."
-  WorkerStopped SymbolicDone ->
-    "Symbolic worker ran out of transactions to work on. Stopping."
-  WorkerStopped TimeLimitReached ->
-    "Time limit reached. Stopping."
-  WorkerStopped FastFailed ->
-    "A test was falsified. Stopping."
-  WorkerStopped (Killed e) ->
-    "Killed (" <> e <>"). Stopping."
-  WorkerStopped (Crashed e) ->
-    "Crashed:\n\n" <>
-    e <>
-    "\n\nPlease report it to https://github.com/crytic/echidna/issues"
-  where
-    showTest test = case test.testType of
-      PropertyTest n _ -> n
-      AssertionTest _ n _ -> encodeSig n
-      CallTest n _ -> n
-      _ -> error "impossible"
-
 -- | The state of a fuzzing campaign.
 data WorkerState = WorkerState
   { workerId    :: !Int
@@ -196,8 +110,11 @@ defaultSymExecTimeout = 30
 defaultSymExecNWorkers :: Int
 defaultSymExecNWorkers = 1
 
+defaultSymExecMaxExplore :: Integer
+defaultSymExecMaxExplore = 10
+
 defaultSymExecMaxIters :: Integer
-defaultSymExecMaxIters = 10
+defaultSymExecMaxIters = 5
 
 -- | Same default as in hevm, "everything else is unsound"
 -- (https://github.com/ethereum/hevm/pull/252)
@@ -213,10 +130,3 @@ getNFuzzWorkers conf = maybe defaultN fromIntegral conf.workers
     n = numCapabilities
     maxN = max 1 n
     defaultN = min 4 maxN -- capped at 4 by default
-
--- | Number of workers, including SymExec worker if there is one
-getNWorkers :: CampaignConf -> Int
-getNWorkers conf = getNFuzzWorkers conf + (if conf.symExec then 1 else 0)
-
-workerIDToType :: CampaignConf -> WorkerId -> WorkerType
-workerIDToType conf wid = if conf.symExec && wid == (getNWorkers conf - 1) then SymbolicWorker else FuzzWorker

lib/Echidna/Types/Config.hs

@@ -3,23 +3,24 @@ module Echidna.Types.Config where
 import Control.Concurrent (Chan)
 import Data.Aeson.Key (Key)
 import Data.IORef (IORef)
-import Data.Map (Map)
 import Data.Set (Set)
 import Data.Text (Text)
 import Data.Time (LocalTime)
 import Data.Word (Word64)
 
 import EVM.Dapp (DappInfo)
-import EVM.Types (Addr, Contract, W256)
+import EVM.Types (Addr, W256)
 
 import Echidna.SourceAnalysis.Slither (SlitherInfo)
 import Echidna.SourceMapping (CodehashMap)
-import Echidna.Types.Campaign (CampaignConf, CampaignEvent)
+import Echidna.Types.Campaign (CampaignConf)
+import Echidna.Types.Worker (CampaignEvent)
 import Echidna.Types.Corpus (Corpus)
 import Echidna.Types.Coverage (CoverageMap)
 import Echidna.Types.Solidity (SolConf)
 import Echidna.Types.Test (TestConf, EchidnaTest)
 import Echidna.Types.Tx (TxConf)
+import Echidna.Types.Cache 
 import Echidna.Types.World (World)
 
 data OperationMode = Interactive | NonInteractive OutputFormat deriving (Show, Eq)
@@ -78,9 +79,9 @@ data Env = Env
 
   , slitherInfo :: Maybe SlitherInfo
   , codehashMap :: CodehashMap
-  , fetchContractCache :: IORef (Map Addr (Maybe Contract))
-  , fetchSlotCache :: IORef (Map Addr (Map W256 (Maybe W256)))
-  , contractNameCache :: IORef (Map W256 Text)
+  , fetchContractCache :: IORef ContractCache
+  , fetchSlotCache :: IORef SlotCache
+  , contractNameCache :: IORef ContractNameCache
   , chainId :: Maybe W256
   , world :: World
   }

lib/Echidna/Types/Random.hs

@@ -1,7 +1,8 @@
 module Echidna.Types.Random where
 
 import Prelude hiding ((!!))
-import Control.Monad.Random.Strict (MonadRandom, getRandomR, weighted)
+import Control.Monad.Random.Strict (MonadRandom, RandT, StdGen, getRandomR, weighted, evalRandT, getStdGen, forM_, liftIO)
+import Data.Array.IO (IOArray, newListArray, readArray, writeArray, getElems)
 import Data.List.NonEmpty ((!!), NonEmpty(..))
 import Data.Set (Set)
 import Data.Set qualified as S
@@ -24,3 +25,26 @@ usuallyRarely u r = weighted [(u, 100), (r, 1)]
 
 usuallyVeryRarely :: MonadRandom m => a -> a -> m a
 usuallyVeryRarely u r = weighted [(u, 1000), (r, 1)]
+
+-- Helper to explicitly type the array creation
+createIOArray :: [a] -> IO (IOArray Int a)
+createIOArray xs = newListArray (1, length xs) xs
+
+-- Fisher-Yates shuffle using RandT + IOArray
+shuffle :: [a] -> RandT StdGen IO [a]
+shuffle xs = do
+    arr <- liftIO $ createIOArray xs
+    let n = length xs
+    forM_ [n, n - 1 .. 2] $ \i -> do
+        j <- getRandomR (1, i)
+        liftIO $ swap arr i j
+    liftIO $ getElems arr
+  where
+    swap arr i j = do
+        vi <- readArray arr i
+        vj <- readArray arr j
+        writeArray arr i vj
+        writeArray arr j vi
+
+shuffleIO :: [a] -> IO [a]
+shuffleIO xs = evalRandT (shuffle xs) =<< getStdGen

lib/Echidna/Types/Test.hs

@@ -7,7 +7,7 @@ import Control.Monad.ST (RealWorld)
 import Data.Aeson
 import Data.DoubleWord (Int256)
 import Data.Maybe (maybeToList)
-import Data.Text (Text)
+import Data.Text (Text, unpack)
 import GHC.Generics (Generic)
 
 import EVM.Dapp (DappInfo)
@@ -16,6 +16,7 @@ import EVM.Types (Addr, VM, VMType(Concrete))
 import Echidna.Types (ExecException)
 import Echidna.Types.Signature (SolSignature)
 import Echidna.Types.Tx (Tx, TxResult)
+import Echidna.ABI (encodeSig)
 
 -- | Test mode is parsed from a string
 type TestMode = String
@@ -36,6 +37,7 @@ data TestState
   = Open
   | Large !Int -- ^ Solved, maybe shrinkable, tracking shrinks tried
   | Passed     -- ^ Presumed unsolvable
+  | Unsolvable -- ^ Formally verified as unsolvable
   | Solved     -- ^ Solved with no need for shrinking
   | Failed ExecException -- ^ Broke the execution environment
   deriving Show
@@ -88,11 +90,12 @@ instance ToJSON TestType where
       object [ "type" .= ("exploration_test" :: String) ]
 
 instance Eq TestState where
-  Open    == Open    = True
-  Large i == Large j = i == j
-  Passed  == Passed  = True
-  Solved  == Solved  = True
-  _       == _       = False
+  Open       == Open       = True
+  Large i    == Large j    = i == j
+  Passed     == Passed     = True
+  Solved     == Solved     = True
+  Unsolvable == Unsolvable = True
+  _          == _          = False
 
 -- | An Echidna test is represented with the following data record
 data EchidnaTest = EchidnaTest
@@ -119,6 +122,18 @@ isOptimizationTest :: EchidnaTest -> Bool
 isOptimizationTest EchidnaTest{testType = OptimizationTest _ _} = True
 isOptimizationTest _ = False
 
+isAssertionTest :: EchidnaTest -> Bool
+isAssertionTest EchidnaTest{testType = AssertionTest {}} = True
+isAssertionTest _ = False
+
+getAssertionSignature :: EchidnaTest -> String
+getAssertionSignature EchidnaTest{testType = AssertionTest _ sig _} = unpack $ encodeSig sig
+getAssertionSignature _ = error "Not an assertion test"
+
+getAssertionFunctionName :: EchidnaTest -> String
+getAssertionFunctionName EchidnaTest{testType = AssertionTest _ (name, _) _} = unpack name
+getAssertionFunctionName _ = error "Not an assertion test"
+
 isOpen :: EchidnaTest -> Bool
 isOpen t = case t.state of
   Open -> True
@@ -135,6 +150,11 @@ isPassed t = case t.state of
   Passed -> True
   _      -> False
 
+isVerified :: EchidnaTest -> Bool
+isVerified t = case t.state of
+  Unsolvable -> True
+  _          -> False
+
 instance ToJSON TestState where
   toJSON s =
     object $ ("passed", toJSON passed) : maybeToList desc
@@ -142,6 +162,7 @@ instance ToJSON TestState where
     (passed, desc) = case s of
       Open     -> (True, Nothing)
       Passed   -> (True, Nothing)
+      Unsolvable -> (True, Nothing)
       Large _  -> (False, Nothing)
       Solved   -> (False, Nothing)
       Failed e -> (False, Just ("exception", toJSON $ show e))

lib/Echidna/Types/Tx.hs

@@ -21,7 +21,7 @@ import EVM.ABI (encodeAbiValue, AbiValue(..), AbiType)
 import EVM.Types
 
 import Echidna.Orphans.JSON ()
-import Echidna.Symbolic (forceBuf)
+import Echidna.SymExec.Symbolic (forceBuf)
 import Echidna.Types.Signature (SolCall)
 import Control.DeepSeq (NFData)
 import GHC.Generics (Generic)

lib/Echidna/Types/Worker.hs

@@ -0,0 +1,37 @@
+module Echidna.Types.Worker where
+
+import Echidna.Types.Test
+import Echidna.Types.Tx
+
+data WorkerType = FuzzWorker | SymbolicWorker deriving (Eq)
+
+type WorkerId = Int
+
+data CampaignEvent
+  = WorkerEvent WorkerId WorkerType WorkerEvent
+  | Failure String
+  | ReproducerSaved String -- filename
+
+data WorkerEvent
+  = TestFalsified !EchidnaTest
+  | TestOptimized !EchidnaTest
+  | NewCoverage { points :: !Int, numCodehashes :: !Int, corpusSize :: !Int, transactions :: [Tx] }
+  | SymExecError !String
+  | SymExecLog !String
+  | TxSequenceReplayed FilePath !Int !Int
+  | TxSequenceReplayFailed FilePath Tx
+  | WorkerStopped WorkerStopReason
+  -- ^ This is a terminal event. Worker exits and won't push any events after
+  -- this one
+  deriving Show
+
+data WorkerStopReason
+  = TestLimitReached
+  | SymbolicExplorationDone
+  | SymbolicVerificationDone
+  | TimeLimitReached
+  | FastFailed
+  | Killed !String
+  | Crashed !String
+  deriving Show
+

lib/Echidna/Types/World.hs

@@ -17,6 +17,7 @@ data World = World
   , highSignatureMap :: SignatureMap
   , lowSignatureMap  :: Maybe SignatureMap
   , payableSigs      :: [FunctionSelector]
+  , assertSigs       :: [FunctionSelector]
   , eventMap         :: EventMap
   }
   deriving Show

lib/Echidna/UI.hs

@@ -43,9 +43,11 @@ import Echidna.Types.Corpus qualified as Corpus
 import Echidna.Types.Coverage (coverageStats)
 import Echidna.Types.Test (EchidnaTest(..), didFail, isOptimizationTest)
 import Echidna.Types.Tx (Tx)
+import Echidna.Types.Worker 
 import Echidna.UI.Report
 import Echidna.UI.Widgets
 import Echidna.Utility (timePrefix, getTimestamp)
+import Echidna.Worker (getNWorkers, workerIDToType)
 
 data UIEvent =
   CampaignUpdated LocalTime [EchidnaTest] [WorkerState]

lib/Echidna/UI/Report.hs

@@ -15,14 +15,16 @@ import Optics
 import Echidna.ABI (GenDict(..), encodeSig)
 import Echidna.Pretty (ppTxCall)
 import Echidna.SourceMapping (findSrcByMetadata, lookupCodehash)
-import Echidna.Symbolic (forceWord)
+import Echidna.SymExec.Symbolic (forceWord)
 import Echidna.Types.Campaign
 import Echidna.Types.Config
 import Echidna.Types.Corpus (corpusSize)
 import Echidna.Types.Coverage (coverageStats)
 import Echidna.Types.Test (EchidnaTest(..), TestState(..), TestType(..))
 import Echidna.Types.Tx (Tx(..), TxCall(..), TxConf(..))
+import Echidna.Types.Worker
 import Echidna.Utility (timePrefix)
+import Echidna.Worker
 
 import EVM.Format (showTraceTree, contractNamePart)
 import EVM.Solidity (SolcContract(..))
@@ -174,6 +176,7 @@ ppTS (Failed e) _ _  = pure $ "could not evaluate ☣\n  " <> show e
 ppTS Solved     vm l = ppFail Nothing vm l
 ppTS Passed     _ _  = pure " passed! 🎉"
 ppTS Open      _ []  = pure "passing"
+ppTS Unsolvable _ _ = pure "verified ✅"
 ppTS Open      vm r  = ppFail Nothing vm r
 ppTS (Large n) vm l  = do
   m <- asks (.cfg.campaignConf.shrinkLimit)
@@ -183,6 +186,7 @@ ppOPT :: (MonadReader Env m, MonadIO m) => TestState -> VM Concrete RealWorld ->
 ppOPT (Failed e) _ _  = pure $ "could not evaluate ☣\n  " <> show e
 ppOPT Solved     vm l = ppOptimized Nothing vm l
 ppOPT Passed     _ _  = pure " passed! 🎉"
+ppOPT Unsolvable _ _ = error "unreachable: optimization tests should not be unsolvable"
 ppOPT Open      vm r  = ppOptimized Nothing vm r
 ppOPT (Large n) vm l  = do
   m <- asks (.cfg.campaignConf.shrinkLimit)

lib/Echidna/UI/Widgets.hs

@@ -31,8 +31,10 @@ import Echidna.Types.Campaign
 import Echidna.Types.Config
 import Echidna.Types.Test
 import Echidna.Types.Tx (Tx(..))
+import Echidna.Types.Worker 
 import Echidna.UI.Report
 import Echidna.Utility (timePrefix)
+import Echidna.Worker (ppCampaignEvent)
 
 import EVM.Format (showTraceTree)
 import EVM.Types (Addr, Contract, W256, VM(..), VMType(Concrete))
@@ -334,6 +336,7 @@ tsWidget (Failed e) _    = pure (str "could not evaluate", str $ show e)
 tsWidget Solved     test = failWidget Nothing test
 tsWidget Passed     _    = pure (success $ str "PASSED!", emptyWidget)
 tsWidget Open       _    = pure (success $ str "passing", emptyWidget)
+tsWidget Unsolvable _    = pure (success $ str "VERIFIED!", emptyWidget)
 tsWidget (Large n)  test = do
   m <- asks (.cfg.campaignConf.shrinkLimit)
   failWidget (if n < m then Just (n,m) else Nothing) test
@@ -377,6 +380,7 @@ optWidget
   -> m (Widget Name, Widget Name)
 optWidget (Failed e) _ = pure (str "could not evaluate", str $ show e)
 optWidget Solved     _ = error "optimization tests cannot be solved"
+optWidget Unsolvable _ = error "optimization tests cannot be unsolvable"
 optWidget Passed     t = pure (str $ "max value found: " ++ show t.value, emptyWidget)
 optWidget Open       t =
   pure (withAttr (attrName "working") $ str $

lib/Echidna/Worker.hs

@@ -0,0 +1,100 @@
+module Echidna.Worker where
+
+import Control.Concurrent
+import Control.Monad.Reader (MonadReader, MonadIO, liftIO, ask)
+import Control.Monad.State.Strict(MonadState(..), gets)
+import Data.Aeson
+import Data.Text (unpack)
+
+import Echidna.ABI (encodeSig)
+import Echidna.Types.Test
+import Echidna.Types.Campaign
+import Echidna.Types.Config (Env(..), EConfig(..))
+import Echidna.Types.Worker
+import Echidna.Utility (getTimestamp)
+
+-- | Number of workers, including SymExec worker if there is one
+getNWorkers :: CampaignConf -> Int
+getNWorkers conf = getNFuzzWorkers conf + (if conf.symExec then 1 else 0)
+
+workerIDToType :: CampaignConf -> WorkerId -> WorkerType
+workerIDToType conf wid = if conf.symExec && wid == (getNWorkers conf - 1) then SymbolicWorker else FuzzWorker
+
+instance ToJSON WorkerEvent where
+  toJSON = \case
+    TestFalsified test -> toJSON test
+    TestOptimized test -> toJSON test
+    NewCoverage { points, numCodehashes, corpusSize } ->
+      object [ "coverage" .= points, "contracts" .= numCodehashes, "corpus_size" .= corpusSize]
+    SymExecError msg -> object [ "msg" .= msg ]
+    SymExecLog msg -> object [ "msg" .= msg ]
+    TxSequenceReplayed file current total ->
+      object [ "file" .= file, "current" .= current, "total" .= total ]
+    TxSequenceReplayFailed file tx ->
+      object [ "file" .= file, "tx" .= tx ]
+    WorkerStopped reason -> object [ "reason" .= show reason ]
+
+pushWorkerEvent
+  :: (MonadReader Env m, MonadState WorkerState m, MonadIO m)
+  => WorkerEvent
+  -> m ()
+pushWorkerEvent event = do
+  workerId <- gets (.workerId)
+  env <- ask
+  let workerType = workerIDToType env.cfg.campaignConf workerId
+  liftIO $ pushCampaignEvent env (WorkerEvent workerId workerType event)
+
+pushCampaignEvent :: Env -> CampaignEvent -> IO ()
+pushCampaignEvent env event = do
+  time <- liftIO getTimestamp
+  writeChan env.eventQueue (time, event)
+
+ppCampaignEvent :: CampaignEvent -> String
+ppCampaignEvent = \case
+  WorkerEvent _ _ e -> ppWorkerEvent e
+  Failure err -> err
+  ReproducerSaved f -> "Saved reproducer to " <> f
+
+ppWorkerEvent :: WorkerEvent -> String
+ppWorkerEvent = \case
+  TestFalsified test ->
+    "Test " <> unpack (showTest test) <> " falsified!"
+  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, "
+      <> show numCodehashes <> " contracts, "
+      <> show corpusSize <> " seqs in corpus"
+  SymExecError err ->
+    "Symbolic execution failed: " <> err
+  SymExecLog msg ->
+    "Symbolic execution log: " <> msg
+  TxSequenceReplayed file current total ->
+    "Sequence replayed from corpus file " <> file <> " (" <> show current <> "/" <> show total <> ")"
+  TxSequenceReplayFailed file tx ->
+    "WARNING: Sequence replay from corpus file " <> file <> " failed. " <>
+    "The destination contract is not deployed for this transaction: " <> show tx <> ". " <>
+    "Remove the file or the transaction to fix the issue."
+  WorkerStopped TestLimitReached ->
+    "Test limit reached. Stopping."
+  WorkerStopped SymbolicExplorationDone ->
+    "Symbolic worker ran out of transactions to explore. Stopping."
+  WorkerStopped SymbolicVerificationDone ->
+    "Symbolic worker finished with the list of methods to verify. Stopping."
+  WorkerStopped TimeLimitReached ->
+    "Time limit reached. Stopping."
+  WorkerStopped FastFailed ->
+    "A test was falsified. Stopping."
+  WorkerStopped (Killed e) ->
+    "Killed (" <> e <>"). Stopping."
+  WorkerStopped (Crashed e) ->
+    "Crashed:\n\n" <>
+    e <>
+    "\n\nPlease report it to https://github.com/crytic/echidna/issues"
+  where
+    showTest test = case test.testType of
+      PropertyTest n _ -> n
+      AssertionTest _ n _ -> encodeSig n
+      CallTest n _ -> n
+      _ -> error "impossible"

package.yaml

@@ -42,7 +42,7 @@ library:
   source-dirs: lib/
   dependencies:
     - ansi-terminal
-    - async
+    - array
     - base16-bytestring
     - binary
     - brick
@@ -69,6 +69,7 @@ library:
     - strip-ansi-escape
     - time
     - unliftio
+    - unliftio-core
     - utf8-string
     - vector
     - vty

src/test/Common.hs

@@ -10,6 +10,7 @@ module Common
   , solnFor
   , solved
   , passed
+  , verified
   , solvedLen
   , solvedWith
   , solvedWithout
@@ -37,6 +38,9 @@ import Data.SemVer (Version, version, fromText)
 import Data.Text (Text, pack)
 import System.Process (readProcess)
 
+import EVM.Solidity (Contracts(..), BuildOutput(..), SolcContract(..))
+import EVM.Types hiding (Env, Gas)
+
 import Echidna (mkEnv, prepareContract)
 import Echidna.Config (parseConfig, defaultConfig)
 import Echidna.Campaign (runWorker)
@@ -48,11 +52,9 @@ import Echidna.Types.Signature (ContractName)
 import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Test
 import Echidna.Types.Tx (Tx(..), TxCall(..))
+import Echidna.Types.Worker (WorkerType(..))
 import Echidna.Types.World (World(..))
 
-import EVM.Solidity (Contracts(..), BuildOutput(..), SolcContract(..))
-import EVM.Types hiding (Env, Gas)
-
 testConfig :: EConfig
 testConfig = defaultConfig & overrideQuiet
                            & overrideLimits
@@ -151,7 +153,7 @@ loadSolTests cfg buildOutput name = do
       (Contracts contractMap) = buildOutput.contracts
       contracts = Map.elems contractMap
       eventMap = Map.unions $ map (.eventMap) contracts
-      world = World solConf.sender mempty Nothing [] eventMap
+      world = World solConf.sender mempty Nothing [] [] eventMap
   mainContract <- selectMainContract solConf name contracts
   echidnaTests <- mkTests solConf mainContract
   env <- mkEnv cfg buildOutput echidnaTests world Nothing
@@ -216,6 +218,15 @@ passed n (env, _) = do
     Nothing             -> error ("no test was found with name: " ++ show n)
     _                   -> False
 
+verified :: Text -> (Env, WorkerState) -> IO Bool
+verified n (env, _) = do
+  tests <- traverse readIORef env.testRefs
+  pure $ case getResult n tests of
+    Just t | isVerified t -> True
+    Just t | isOpen t     -> True
+    Nothing               -> error ("no test was found with name: " ++ show n)
+    _                     -> False
+
 solvedLen :: Int -> Text -> (Env, WorkerState) -> IO Bool
 solvedLen i t final = (== Just i) . fmap length <$> solnFor t final
 

src/test/Tests/Assertion.hs

@@ -4,7 +4,7 @@ import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract, testContract', testContractV, solcV, solved, solvedUsing, passed)
 
-import Echidna.Types.Campaign (WorkerType(..))
+import Echidna.Types.Worker (WorkerType(..))
 
 assertionTests :: TestTree
 assertionTests = testGroup "Assertion-based Integration Testing"

src/test/Tests/Cheat.hs

@@ -4,7 +4,7 @@ import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract', solcV, solved, passed)
 
-import Echidna.Types.Campaign (WorkerType(..))
+import Echidna.Types.Worker (WorkerType(..))
 
 cheatTests :: TestTree
 cheatTests =

src/test/Tests/Dapptest.hs

@@ -4,7 +4,7 @@ import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract', solcV, solved, passed)
 
-import Echidna.Types.Campaign (WorkerType(..))
+import Echidna.Types.Worker (WorkerType(..))
 
 dapptestTests :: TestTree
 dapptestTests = testGroup "Dapptest Integration Testing"

src/test/Tests/Integration.hs

@@ -5,7 +5,7 @@ import Test.Tasty (TestTree, testGroup)
 import Common (testContract, testContractV, solcV, testContract', checkConstructorConditions, passed, solved, solvedLen, solvedWith, solvedWithout)
 import Data.Functor ((<&>))
 import Data.Text (unpack)
-import Echidna.Types.Campaign (WorkerType(..))
+import Echidna.Types.Worker (WorkerType(..))
 import Echidna.Types.Tx (TxCall(..))
 import EVM.ABI (AbiValue(..))
 
@@ -86,9 +86,7 @@ integrationTests = testGroup "Solidity Integration Testing"
   , testContract "basic/gaslimit.sol"  Nothing
       [ ("echidna_gaslimit passed",                passed      "echidna_gaslimit") ]
   , testContract "basic/gasleft.sol"     (Just "basic/gasleft.yaml")
-      [ ("unexpected gas left",                   passed      "echidna_expected_gasleft") ]
-  ,  testContractV "basic/killed.sol"      (Just (< solcV (0,8,0))) (Just "basic/killed.yaml")
-      [ ("echidna_still_alive failed",             solved      "echidna_still_alive") ]
+      [ ("unexpected gas left",                    passed      "echidna_expected_gasleft") ]
   ,  checkConstructorConditions "basic/codesize.sol"
       "invalid codesize"
   , testContractV "basic/eip-170.sol" (Just (>= solcV (0,5,0))) (Just "basic/eip-170.yaml")

src/test/Tests/Research.hs

@@ -4,13 +4,13 @@ import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract, testContract', solcV, solved)
 
-import Echidna.Types.Campaign (WorkerType(..))
+import Echidna.Types.Worker (WorkerType(..))
 
 researchTests :: TestTree
 researchTests = testGroup "Research-based Integration Testing"
   [ testContract "research/harvey_foo.sol" Nothing
       [ ("echidna_assert failed",     solved "echidna_assert") ]
-  , testContract' "research/harvey_baz.sol" Nothing Nothing Nothing False FuzzWorker
+  , testContract' "research/harvey_baz.sol" Nothing Nothing (Just "research/harvey.yaml") False FuzzWorker 
       [ ("echidna_all_states failed", solved "echidna_all_states") ]
   , testContract' "research/ilf_crowdsale.sol" Nothing (Just (\v -> v >= solcV (0,5,0) && v < solcV (0,6,0))) (Just "research/ilf_crowdsale.yaml") False FuzzWorker
       [ ("echidna_assert failed", solved "withdraw") ]

src/test/Tests/Seed.hs

@@ -12,6 +12,7 @@ import Echidna.Types.Campaign
 import Echidna.Types.Config (Env(..), EConfig(..))
 import Echidna.Types.Coverage (CoverageFileType(..))
 import Echidna.Types.Test
+import Echidna.Types.Worker (WorkerType(..))
 
 seedTests :: TestTree
 seedTests =

src/test/Tests/Symbolic.hs

@@ -1,15 +1,22 @@
 module Tests.Symbolic (symbolicTests) where
 
 import Test.Tasty (TestTree, testGroup)
-import Common (testContract', solved, passed)
-import Echidna.Types.Campaign (WorkerType(..))
+import Common (testContract', solved, verified)
+import Echidna.Types.Worker (WorkerType(..))
 
 symbolicTests :: TestTree
 symbolicTests = testGroup "Symbolic tests"
-  [ testContract' "symbolic/sym.sol" Nothing Nothing (Just "symbolic/sym.yaml") True SymbolicWorker
-      [ ("echidna_sym passed", passed "echidna_sym") ]
-
-  , testContract' "symbolic/sym-assert.sol" Nothing Nothing (Just "symbolic/sym-assert.yaml") True SymbolicWorker
-      [ ("func_one passed", solved "func_one")
-      , ("func_two passed", solved "func_two") ]
+  [ testContract' "symbolic/verify.sol" Nothing Nothing (Just "symbolic/verify.yaml") True SymbolicWorker
+      [ ("simple passed", solved "simple")
+      , ("array passed", solved "array")
+      , ("negative passed", solved "negative")
+      , ("close passed", solved "close")
+      , ("far not verified", verified "far")
+      , ("correct not verified", verified "correct") 
+    ] 
+    -- This test is commented out because it requires a specific setup where both the FuzzWorker and SymbolicWorker are used.
+    -- If you run the symbolic worker alone, it will hang indefinitely.
+    --, testContract' "symbolic/explore.sol" Nothing Nothing (Just "symbolic/explore.yaml") True SymbolicWorker
+    --  [ ("f passed", solved "f")
+    --]
   ]

src/test/Tests/Values.hs

@@ -4,7 +4,7 @@ import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract, testContract', solved, solvedLen)
 
-import Echidna.Types.Campaign (WorkerType(..))
+import Echidna.Types.Worker (WorkerType(..))
 
 valuesTests :: TestTree
 valuesTests = testGroup "Value extraction tests"

stack.yaml

@@ -6,7 +6,7 @@ packages:
 
 extra-deps:
 - git: https://github.com/ethereum/hevm.git
-  commit: 2931f09fcbbca68911421fbe2f2f21ebebdb5332
+  commit: 1ee94f7772d42154fcf8df16681d3c6f25a4ecdd
 
 - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421
 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162

tests/solidity/basic/default.yaml

@@ -95,9 +95,6 @@ workers: null
 server: null
 # whether to add an additional symbolic execution worker
 symExec: false
-# whether symbolic execution will be concolic (vs full symbolic execution)
-# only relevant if symExec is true
-symExecConcolic: true
 # number of SMT solvers used in symbolic execution
 # only relevant if symExec is true
 symExecNSolvers: 1
@@ -105,11 +102,17 @@ symExecNSolvers: 1
 # only relevant if symExec is true
 symExecTimeout: 30
 # Number of times we may revisit a particular branching point
-# only relevant if symExec is true and symExecConcolic is false
+# only relevant if symExec is true
 symExecMaxIters: 10
 # Number of times we may revisit a particular branching point before we consult the smt solver to check reachability
-# only relevant if symExec is true and symExecConcolic is false
+# only relevant if symExec is true
 symExecAskSMTIters: 1
-# List of whitelisted functions for using symbolic/concolic exploration
+# List of whitelisted functions for using symbolic exploration
 # only relevant if symExec is true
 symExecTargets: null
+# List the max number of states to explore when using symbolc execution
+# only relevant if symExec is true
+symExecMaxExplore: 10
+# Select the SMT solver when using symbolic execution. Valid values are: "cvc5", "z3" and "bitwuzla"
+# only relevant if symExec is true
+symExecSMTSolver: bitwuzla

tests/solidity/basic/killed.sol

@@ -1,22 +0,0 @@
-contract C {
-  constructor() public payable {}
-
-  uint private state = 0;
-  function f(uint x) public {
-    state = x;
-  }
-
-  function kill_me() public {
-    require(state > 256);
-    selfdestruct(msg.sender);
-  }
-
-  function echidna_still_alive() public returns (bool) {
-    return address(this).balance > 0;
-  }
-
-  function echidna_revert_still_alive() public returns (bool) {
-    revert();
-  }
-
-}

tests/solidity/basic/killed.yaml

@@ -1 +0,0 @@
-balanceContract: 100

tests/solidity/research/harvey.yaml

@@ -0,0 +1,2 @@
+testLimit: 100000
+shrinkLimit: 100

tests/solidity/symbolic/explore.sol

@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+contract C {
+  address owner;
+  int private stateA = 0;
+  int private stateB = 0;
+  int constant CONST = 30007;
+
+  function f(int x) public {
+    if (x % CONST == 4565) { 
+      stateA = x; 
+    }
+  }
+
+  function g(int y) public {
+    if (stateA > 0) {
+      stateB = stateA ^ 4555666644 + y;
+      assert(stateB != 62);
+    }
+  }
+}

tests/solidity/symbolic/explore.yaml

@@ -0,0 +1,5 @@
+testMode: assertion
+stopOnFail: true
+symExec: true
+testLimit: 50000
+workers: 1

tests/solidity/symbolic/sym-assert.sol

@@ -1,15 +0,0 @@
-contract VulnerableContract {
-    mapping (uint256 => uint256) a;
-    function func_one(uint256 x) public payable {
-        a[12323] = ((x >> 5) / 7777);
-        if (a[12323] == 2222) {
-            assert(false); // BUG
-        }
-    }
-
-    function func_two(uint256 x) public payable {
-        if ((x >> 5) / 7777 == 2222) {
-            assert(false); // BUG
-        }
-    }
-}

tests/solidity/symbolic/sym.sol

@@ -1,21 +0,0 @@
-contract VulnerableContract {
-    mapping (uint256 => uint256) a;
-    bool y;
-    bool z;
-    function func_one(uint256 x) public payable {
-        a[12323] = ((x >> 5) / 7777);
-        if (a[12323] == 2222) {
-            y = true;
-        }
-    }
-
-    function func_two(uint256 x) public payable {
-        if ((x >> 5) / 7777 == 2222) {
-            z = true;
-        }
-    }
-
-    function echidna_sym() public returns (bool) {
-        return !(y && z);
-    }
-}

tests/solidity/symbolic/sym.yaml

@@ -1,3 +0,0 @@
-symExec: true
-workers: 0
-symExecConcolic: false

tests/solidity/symbolic/verify.sol

@@ -0,0 +1,30 @@
+contract VulnerableContract {
+    mapping (uint256 => uint256) a;
+    uint256 private last_number = block.number;
+    function simple(uint256 x) public payable {
+        a[12323] = ((x >> 5) / 7777);
+        if (a[12323] == 2222) {
+            assert(false); // BUG
+        }
+    }
+  function array(uint256[3] calldata xs) public {
+    assert(xs[0] != xs[2] + 1);
+  }
+  
+  function negative(int24 x) public {
+    assert(x != -42);
+  }
+
+  function correct(int24 x) public {
+    assert(int256(x) != type(int256).max);
+  }
+
+  function close(uint256 x) public {
+    assert(block.number != last_number + 123);
+  }
+
+  function far(uint256 x) public {
+    assert(block.number != type(uint256).max);
+  }
+
+}

tests/solidity/symbolic/verify.yaml

@@ -1,4 +1,5 @@
 testMode: assertion
 symExec: true
-symExecConcolic: false
+symExecSMTSolver: z3
 workers: 0
+seqLen: 1