From 80acdf5d748a0d15e22bf4010e915ddc64278a0d Mon Sep 17 00:00:00 2001
From: Gustavo Grieco <31542053+ggrieco-tob@users.noreply.github.com>
Date: Tue, 28 May 2024 19:28:48 +0200
Subject: [PATCH] Allow to use specific filter for direct symexec (#1251)

* Allow to use specific filter for direct symexec

* Update default.yaml
---
 lib/Echidna/Campaign.hs           | 2 +-
 lib/Echidna/Config.hs             | 1 +
 lib/Echidna/SymExec.hs            | 6 +++++-
 lib/Echidna/Types/Campaign.hs     | 1 +
 src/Main.hs                       | 5 +++++
 tests/solidity/basic/default.yaml | 3 +++
 6 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs
index 7e95b1f83..1b07cfa1e 100644
--- a/lib/Echidna/Campaign.hs
+++ b/lib/Echidna/Campaign.hs
@@ -185,7 +185,7 @@ runSymWorker callback vm dict workerId initialCorpus name cs = 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])) symTxs
 
-    unless newCoverage (pushWorkerEvent SymNoNewCoverage)
+    unless (newCoverage || null symTxs) (pushWorkerEvent SymNoNewCoverage)
 
 -- | Run a fuzzing campaign given an initial universe state, some tests, and an
 -- optional dictionary to generate calls with. Return the 'Campaign' state once
diff --git a/lib/Echidna/Config.hs b/lib/Echidna/Config.hs
index ac332f17d..cbe6ca17e 100644
--- a/lib/Echidna/Config.hs
+++ b/lib/Echidna/Config.hs
@@ -100,6 +100,7 @@ instance FromJSON EConfigWithUsage where
         <*> v ..:? "server"
         <*> v ..:? "symExec"            ..!= False
         <*> v ..:? "symExecConcolic"    ..!= True
+        <*> v ..:? "symExecTargets"     ..!= Nothing
         <*> v ..:? "symExecTimeout"     ..!= defaultSymExecTimeout
         <*> v ..:? "symExecNSolvers"    ..!= defaultSymExecNWorkers
         <*> v ..:? "symExecMaxIters"    ..!= defaultSymExecMaxIters
diff --git a/lib/Echidna/SymExec.hs b/lib/Echidna/SymExec.hs
index 3c0b973d2..996a5cd7a 100644
--- a/lib/Echidna/SymExec.hs
+++ b/lib/Echidna/SymExec.hs
@@ -60,7 +60,11 @@ exploreContract conf contract tx vm = do
   let
     isConc = isJust tx
     allMethods = Map.elems contract.abiMap
-    concMethods (Tx { call = SolCall (methodName, _) }) = filter (\method -> method.name == methodName) allMethods
+    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)
diff --git a/lib/Echidna/Types/Campaign.hs b/lib/Echidna/Types/Campaign.hs
index c0b1e3351..6a9a1521a 100644
--- a/lib/Echidna/Types/Campaign.hs
+++ b/lib/Echidna/Types/Campaign.hs
@@ -49,6 +49,7 @@ data CampaignConf = CampaignConf
   , symExecConcolic    :: Bool
     -- ^ Whether symbolic execution will be concolic (vs full symbolic execution)
     -- Only relevant if symExec is True
+  , symExecTargets     :: Maybe [Text]
   , symExecTimeout     :: Int
     -- ^ Timeout for symbolic execution SMT solver.
     -- Only relevant if symExec is True
diff --git a/src/Main.hs b/src/Main.hs
index 312c805d3..36e33665c 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -140,6 +140,7 @@ data Options = Options
   , cliCryticArgs       :: Maybe String
   , cliSolcArgs         :: Maybe String
   , cliSymExec          :: Maybe Bool
+  , cliSymExecTargets   :: Maybe Text
   , cliSymExecTimeout   :: Maybe Int
   , cliSymExecNSolvers  :: Maybe Int
   }
@@ -220,6 +221,9 @@ options = Options
   <*> optional (option bool $ long "sym-exec"
     <> metavar "BOOL"
     <> help "Whether to enable the experimental symbolic execution feature.")
+  <*> optional (option str $ long "sym-exec-target"
+    <> metavar "SELECTOR"
+    <> help "Target for the symbolic execution run (assuming sym-exec is enabled). Default is all functions")
   <*> optional (option auto $ long "sym-exec-timeout"
     <> metavar "INTEGER"
     <> help ("Timeout for each symbolic execution run, in seconds (assuming sym-exec is enabled). Default is " ++ show defaultSymExecTimeout))
@@ -268,6 +272,7 @@ overrideConfig config Options{..} = do
       , workers = cliWorkers <|> campaignConf.workers
       , serverPort = cliServerPort <|> campaignConf.serverPort
       , symExec = fromMaybe campaignConf.symExec cliSymExec
+      , symExecTargets = (\ t -> Just [t]) =<< cliSymExecTargets
       , symExecTimeout = fromMaybe campaignConf.symExecTimeout cliSymExecTimeout
       , symExecNSolvers = fromMaybe campaignConf.symExecNSolvers cliSymExecNSolvers
       }
diff --git a/tests/solidity/basic/default.yaml b/tests/solidity/basic/default.yaml
index 818156fa6..1a9458bd9 100644
--- a/tests/solidity/basic/default.yaml
+++ b/tests/solidity/basic/default.yaml
@@ -110,3 +110,6 @@ 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
 symExecAskSMTIters: 1
+# List of whitelisted functions for using symbolic/concolic exploration
+# only relevant if symExec is true
+symExecTargets: null