simplified exploration code and added shrinking

Author: gustavo-grieco

lib/Echidna/Campaign.hs

@@ -5,7 +5,7 @@ module Echidna.Campaign where
 
 import Control.Concurrent
 import Control.DeepSeq (force)
-import Control.Monad (replicateM, replicateM_, when, unless, void, forM_)
+import Control.Monad (replicateM, when, unless, void, forM_)
 import Control.Monad.Catch (MonadThrow(..))
 import Control.Monad.Random.Strict (MonadRandom, RandT, evalRandT)
 import Control.Monad.Reader (MonadReader, asks, liftIO, ask)
@@ -42,7 +42,7 @@ import Echidna.Shrink (shrinkTest)
 import Echidna.Solidity (chooseContract)
 import Echidna.SymExec.Common (extractTxs, extractErrors)
 import Echidna.SymExec.Symbolic (forceAddr)
-import Echidna.SymExec.Exploration (exploreContract)
+import Echidna.SymExec.Exploration (exploreContract, getTargetMethodFromTx, getRandomTargetMethod)
 import Echidna.SymExec.Verification (verifyMethod)
 import Echidna.Test
 import Echidna.Transaction
@@ -51,7 +51,7 @@ import Echidna.Types.Campaign
 import Echidna.Types.Corpus (Corpus, corpusSize)
 import Echidna.Types.Coverage (coverageStats)
 import Echidna.Types.Config
-import Echidna.Types.Random (rElem, shuffleIO)
+import Echidna.Types.Random (rElem)
 import Echidna.Types.Signature (FunctionName)
 import Echidna.Types.Test
 import Echidna.Types.Test qualified as Test
@@ -116,8 +116,7 @@ runSymWorker
   -- ^ Initial corpus of transactions
   -> Maybe Text -- ^ Specified contract name
   -> m (WorkerStopReason, WorkerState)
-runSymWorker callback vm dict workerId initialCorpus name = do
-  shuffleCorpus <- liftIO $ shuffleIO initialCorpus
+runSymWorker callback vm dict workerId _ name = do
   cfg <- asks (.cfg)
   let nworkers = getNFuzzWorkers cfg.campaignConf -- getNFuzzWorkers, NOT getNWorkers
   eventQueue <- asks (.eventQueue)
@@ -134,13 +133,6 @@ runSymWorker callback vm dict workerId initialCorpus name = do
       flip evalRandT (mkStdGen effectiveSeed) $ do -- unused but needed for callseq
         lift callback
         listenerLoop listenerFunc chan nworkers
-        void $ replayCorpus vm initialCorpus
-        if null shuffleCorpus then
-          replicateM_ 10 $ symexecTxs True [] -- TODO: determine how many times to symexec here
-        else
-          mapM_ (symexecTxs False . snd) shuffleCorpus
-        liftIO $ putStrLn "Symbolic exploration started purely random!"
-        replicateM_ 100 $ mapM_ (symexecTxs True . snd) shuffleCorpus
         pure SymbolicExplorationDone
 
   where
@@ -164,8 +156,53 @@ runSymWorker callback vm dict workerId initialCorpus name = do
   listenerFunc (_, WorkerEvent _ _ (NewCoverage {transactions})) = do
     void $ callseq vm transactions
     symexecTxs False transactions
+    shrinkAndRandomlyExplore transactions (10 :: Int)
   listenerFunc _ = pure ()
 
+  shrinkAndRandomlyExplore _ 0 = do 
+    testRefs <- asks (.testRefs)
+    tests <- liftIO $ traverse readIORef testRefs
+    CampaignConf{shrinkLimit} <- asks (.cfg.campaignConf)
+    if any shrinkable tests then shrinkLoop shrinkLimit else return ()
+
+  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:
@@ -198,8 +235,21 @@ runSymWorker callback vm dict workerId initialCorpus name = do
     dapp <- asks (.dapp)
     let cs = Map.elems dapp.solcByName
     contract <- chooseContract cs name
-    (threadId, symTxsChan) <- exploreContract contract tx vm'
-
+    failedTests <- findFailedTests
+    let failedTestSignatures = map getAssertionSignature failedTests
+    case tx of 
+      Nothing -> getRandomTargetMethod contract failedTestSignatures >>= \case
+        Nothing -> do
+          error "No suitable method found for symbolic execution"
+        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
 
@@ -217,10 +267,8 @@ runSymWorker callback vm dict workerId initialCorpus 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 (txsBase <> [symTx])) txs
 
-    when (not newCoverage && null errors && not (null txs)) ( do
-      liftIO $ mapM_ print txsBase
-      liftIO $ putStrLn $ "Last txs: " <> show txs
-      error "No errors but symbolic execution found valid txs breaking assertions. Something is wrong.")
+    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 SymNoNewCoverage)
 
   verifyMethods = do
@@ -574,6 +622,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)

lib/Echidna/SymExec/Exploration.hs

@@ -5,15 +5,15 @@ module Echidna.SymExec.Exploration where
 import Control.Applicative ((<|>))
 import Control.Concurrent (ThreadId, forkIO)
 import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar)
-import Control.Monad (forM)
 import Control.Monad.Catch (MonadThrow(..))
 import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.Reader (MonadReader, ask, asks, runReaderT, liftIO)
 import Data.Map qualified as Map
 import Data.Maybe (fromJust)
 import Data.Set qualified as Set
-import Data.Text (Text)
+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)
@@ -24,10 +24,10 @@ import Control.Monad.ST (RealWorld)
 
 import Echidna.Types.Campaign (CampaignConf(..))
 import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..))
-import Echidna.Types.Random (shuffleIO)
 import Echidna.Types.World (World(..))
 import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Tx (Tx(..), TxCall(..))
+import Echidna.Types.Random (rElem)
 import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, rpcFetcher, TxOrError(..), PartialsLogs)
 
 -- | Uses symbolic execution to find transactions which would increase coverage.
@@ -39,6 +39,40 @@ import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, rpcFetcher, Tx
 --   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 -> [String] -> m (Maybe Method)
+getRandomTargetMethod contract failedProperties = do
+  env <- ask
+  let allMethods = Map.assocs contract.abiMap
+      assertSigs = env.world.assertSigs
+      --(selector, method) = case filter (\(_, m) -> m.name == method.name) allMethods of
+      --  [] -> error $ "Method " ++ show methodName ++ " not found in contract ABI"
+      --  (x:_) -> x
+      filterFunc (selector, method) = (null assertSigs || selector `elem` assertSigs) && suitableForSymExec method && (unpack $ method.methodSignature) `notElem` failedProperties
+      filteredMethods = filter filterFunc allMethods
+  
+  case filteredMethods of
+    [] -> 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.
@@ -51,22 +85,18 @@ filterTarget symExecTargets assertSigs tx 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) => SolcContract -> Maybe Tx -> EVM.Types.VM Concrete RealWorld -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
-exploreContract contract tx vm = do
+exploreContract :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m) => SolcContract -> Method -> EVM.Types.VM Concrete RealWorld -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+exploreContract contract method vm = do
   conf <- asks (.cfg)
-  env <- ask
   contractCacheRef <- asks (.fetchContractCache)
   slotCacheRef <- asks (.fetchSlotCache)
   let
-    allMethods = Map.elems contract.abiMap
-    filteredMethods = filter (filterTarget conf.campaignConf.symExecTargets env.world.assertSigs tx) allMethods
-    methods = filteredMethods
     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 $ fmap (.dst) tx <|> Set.lookupMin conf.solConf.sender <|> Just 0
+    defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0
 
   threadIdChan <- liftIO newEmptyMVar
   doneChan <- liftIO newEmptyMVar
@@ -78,12 +108,11 @@ exploreContract contract tx vm = do
 
   liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) 1 timeoutSMT $ \solvers -> do
     threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do
-      shuffleMethods <- liftIO $ shuffleIO methods
       -- 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 <- forM (take 1 shuffleMethods) $ \method -> exploreMethod method contract vm defaultSender conf veriOpts solvers rpcInfo contractCacheRef slotCacheRef
-      liftIO $ putMVar resultChan (concatMap fst res, concatMap snd res)
+      res <- exploreMethod method contract vm defaultSender conf veriOpts solvers rpcInfo contractCacheRef slotCacheRef
+      liftIO $ putMVar resultChan res
       --liftIO $ print "done"
       liftIO $ putMVar doneChan ()
     liftIO $ putMVar threadIdChan threadId

lib/Echidna/Types/Test.hs

@@ -130,6 +130,10 @@ 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

stack.yaml

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