Allow to disable testing of view/pure function, except prefix ones in property mode

lib/Echidna/Config.hs

@@ -141,6 +141,7 @@ instance FromJSON EConfigWithUsage where
         <*> v ..:? "testDestruction" ..!= False
         <*> v ..:? "allowFFI"        ..!= False
         <*> fnFilter
+        <*> v ..:? "excludeViewPure" ..!= False
         where
         mode = v ..:? "testMode" >>= \case
           Just s  -> pure $ validateTestMode s

lib/Echidna/Solidity.hs

@@ -275,19 +275,33 @@ mkSignatureMap
   -> IO SignatureMap
 mkSignatureMap solConf mainContract contracts = do
   let
+    -- Optionally exclude view/pure functions from the ABI, but never
+    -- exclude prefixed functions (e.g. echidna_*) as they may be properties
+    filterViewPure contract sigs
+      | solConf.excludeViewPure =
+          let viewPureNames = map (.name) $ filter (\m -> m.mutability == View || m.mutability == Pure)
+                                                   (Map.elems contract.abiMap)
+          in NE.filter (\(n, _) -> isPrefixOf solConf.prefix n || n `notElem` viewPureNames) sigs
+      | otherwise = NE.toList sigs
     -- Filter ABI according to the config options
     fabiOfc = if isFoundryMode solConf.testMode
                 then NE.toList $ filterMethodsWithArgs (abiOf solConf.prefix mainContract)
-                else filterMethods mainContract.contractName solConf.methodFilter $
-                       abiOf solConf.prefix mainContract
+                else let base = filterMethods mainContract.contractName solConf.methodFilter $
+                                  abiOf solConf.prefix mainContract
+                     in case NE.nonEmpty base of
+                       Just ne -> filterViewPure mainContract ne
+                       Nothing -> base
     -- Construct ABI mapping for World
     abiMapping =
       if solConf.allContracts then
         Map.fromList $ mapMaybe (\contract ->
             let filtered = filterMethods contract.contractName
                                          solConf.methodFilter
                                          (abiOf solConf.prefix contract)
-            in (contract.runtimeCodehash,) <$> NE.nonEmpty filtered)
+                filtered' = case NE.nonEmpty filtered of
+                  Just ne -> filterViewPure contract ne
+                  Nothing -> filtered
+            in (contract.runtimeCodehash,) <$> NE.nonEmpty filtered')
           contracts
       else
         case NE.nonEmpty fabiOfc of
@@ -310,9 +324,14 @@ mkTests solConf campaignConf mainContract = do
     abi = Map.elems mainContract.abiMap <&> \method -> (method.name, snd <$> method.inputs)
     (tests, funs) = partition (isPrefixOf solConf.prefix . fst) abi
     -- Filter again for foundry tests or assertions checking if enabled
-    neFuns = filterMethods mainContract.contractName
-                           solConf.methodFilter
-                           (fallback NE.:| funs)
+    neFuns' = filterMethods mainContract.contractName
+                            solConf.methodFilter
+                            (fallback NE.:| funs)
+    neFuns = if solConf.excludeViewPure
+             then let viewPureNames = map (.name) $ filter (\m -> m.mutability == View || m.mutability == Pure)
+                                                           (Map.elems mainContract.abiMap)
+                  in filter (\(n, _) -> isPrefixOf solConf.prefix n || n `notElem` viewPureNames) neFuns'
+             else neFuns'
     testNames = fst <$> tests
 
   when (null abi) $
@@ -373,13 +392,13 @@ mkWorld
   -> SlitherInfo
   -> [SolcContract]
   -> World
-mkWorld SolConf{sender, testMode} sigMap maybeContract slitherInfo contracts =
+mkWorld SolConf{sender, testMode, excludeViewPure} 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 isFoundryMode testMode then [] else filterResults maybeContract slitherInfo.constantFunctions \\ as
+    cs = if isFoundryMode testMode || excludeViewPure then [] else filterResults maybeContract slitherInfo.constantFunctions \\ as
     (highSignatureMap, lowSignatureMap) = prepareHashMaps cs as $
       filterFallbacks slitherInfo.fallbackDefined slitherInfo.receiveDefined contracts sigMap
   in World { senders = sender

lib/Echidna/Types/Solidity.hs

@@ -82,6 +82,7 @@ data SolConf = SolConf
   , testDestruction :: Bool             -- ^ Whether or not to add a property to detect contract destruction
   , allowFFI        :: Bool             -- ^ Whether or not to allow FFI hevm cheatcode
   , methodFilter    :: Filter           -- ^ List of methods to avoid or include calling during a campaign
+  , excludeViewPure :: Bool             -- ^ Whether to exclude view/pure functions from fuzzing
   }
 
 defaultContractAddr :: Addr

src/test/Common.hs

@@ -17,6 +17,7 @@ module Common
   , solvedWith
   , solvedWithout
   , solvedUsing
+  , notPresent
   , countCorpus
   , overrideQuiet
   , loadSolTests
@@ -232,6 +233,13 @@ passed n (env, _) = do
     Nothing             -> error ("no test was found with name: " ++ show n)
     _                   -> False
 
+notPresent :: Text -> (Env, WorkerState) -> IO Bool
+notPresent n (env, _) = do
+  tests <- traverse readIORef env.testRefs
+  pure $ case getResult n tests of
+    Nothing -> True
+    _       -> False
+
 verified :: Text -> (Env, WorkerState) -> IO Bool
 verified n (env, _) = do
   tests <- traverse readIORef env.testRefs

src/test/Tests/Integration.hs

@@ -35,6 +35,11 @@ integrationTests = testGroup "Solidity Integration Testing"
       , ("echidna_revert_always failed",                   passed      "echidna_revert_always")
       , ("echidna_sometimesfalse passed",                  passed      "echidna_sometimesfalse")
       ]
+  , testContractV "basic/excludeviewpure.sol" (Just (>= solcV (0,8,0))) (Just "basic/excludeviewpure.yaml")
+      -- echidna_counter_small is a view property: must not be excluded, and must be solved
+      -- (which also proves increment() is still being called by the fuzzer)
+      [ ("view property must not be excluded and should be solved", solved "echidna_counter_small")
+      ]
   , testContract "basic/revert.sol" Nothing
       [ ("echidna_fails_on_revert passed", solved "echidna_fails_on_revert")
       , ("echidna_fails_on_revert didn't shrink to one transaction",

tests/solidity/basic/default.yaml

@@ -74,6 +74,8 @@ maxBlockDelay: 60480
 filterFunctions: []
 # by default, blacklist methods in filterFunctions
 filterBlacklist: true
+# exclude view/pure functions from fuzzing (prefixed property tests are kept)
+excludeViewPure: false
 # enable or disable ffi HEVM cheatcode
 allowFFI: false
 #directory to save the corpus; by default is disabled

tests/solidity/basic/excludeviewpure.sol

@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+// Tests that excludeViewPure does NOT exclude prefixed view/pure functions
+// in property mode, since those are property tests.
+contract ViewPureProperty {
+    uint256 public counter;
+
+    function increment() external {
+        counter++;
+    }
+
+    // view property — must NOT be excluded even with excludeViewPure: true
+    function echidna_counter_small() public view returns (bool) {
+        return counter < 10;
+    }
+
+    // non-prefixed view — should be excluded
+    function getCounter() external view returns (uint256) {
+        return counter;
+    }
+
+    // non-prefixed pure — should be excluded
+    function getConst() external pure returns (uint256) {
+        return 42;
+    }
+}

tests/solidity/basic/excludeviewpure.yaml

@@ -0,0 +1,4 @@
+testMode: property
+excludeViewPure: true
+seed: 123
+testLimit: 5000