Allow to use specific filter for direct symexec (#1251)

* Allow to use specific filter for direct symexec * Update default.yaml
crytic · May 28, 2024 · 80acdf5 · 80acdf5
1 parent 53a0a91
commit 80acdf5
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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