From 95ba40cd577d21762d840dbf7a0d83b30d26dba9 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Sun, 5 Apr 2026 09:03:14 +0200 Subject: [PATCH 1/4] allow to disable testing of view/pure function, except prefix ones in property mode --- lib/Echidna/Config.hs | 1 + lib/Echidna/Solidity.hs | 35 +++++++++++++++++------ lib/Echidna/Types/Solidity.hs | 1 + src/test/Common.hs | 8 ++++++ src/test/Tests/Integration.hs | 7 ++++- tests/solidity/basic/excludeviewpure.sol | 27 +++++++++++++++++ tests/solidity/basic/excludeviewpure.yaml | 4 +++ 7 files changed, 74 insertions(+), 9 deletions(-) create mode 100644 tests/solidity/basic/excludeviewpure.sol create mode 100644 tests/solidity/basic/excludeviewpure.yaml diff --git a/lib/Echidna/Config.hs b/lib/Echidna/Config.hs index 8ce9323b6..618985871 100644 --- a/lib/Echidna/Config.hs +++ b/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 diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs index a74c44a89..ec6903746 100644 --- a/lib/Echidna/Solidity.hs +++ b/lib/Echidna/Solidity.hs @@ -275,11 +275,22 @@ 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 @@ -287,7 +298,10 @@ mkSignatureMap solConf mainContract contracts = do 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 diff --git a/lib/Echidna/Types/Solidity.hs b/lib/Echidna/Types/Solidity.hs index 3e18c78fb..f8341a79a 100644 --- a/lib/Echidna/Types/Solidity.hs +++ b/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 diff --git a/src/test/Common.hs b/src/test/Common.hs index 1921f4a57..2a3011010 100644 --- a/src/test/Common.hs +++ b/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 diff --git a/src/test/Tests/Integration.hs b/src/test/Tests/Integration.hs index bd7c9fdcd..25ad6cdae 100644 --- a/src/test/Tests/Integration.hs +++ b/src/test/Tests/Integration.hs @@ -6,7 +6,7 @@ import Test.Tasty (TestTree, testGroup) import EVM.ABI (AbiValue(..)) -import Common (testContract, testContractV, solcV, testContract', checkConstructorConditions, passed, solved, solvedLen, solvedWith, solvedWithout) +import Common (testContract, testContractV, solcV, testContract', checkConstructorConditions, passed, notPresent, solved, solvedLen, solvedWith, solvedWithout) import Echidna.Types.Tx (TxCall(..)) import Echidna.Types.Worker (WorkerType(..)) @@ -35,6 +35,11 @@ integrationTests = testGroup "Solidity Integration Testing" , ("echidna_revert_always failed", passed "echidna_revert_always") , ("echidna_sometimesfalse passed", passed "echidna_sometimesfalse") ] + , testContract "basic/excludeviewpure.sol" (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", diff --git a/tests/solidity/basic/excludeviewpure.sol b/tests/solidity/basic/excludeviewpure.sol new file mode 100644 index 000000000..2cd8175ef --- /dev/null +++ b/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; + } +} diff --git a/tests/solidity/basic/excludeviewpure.yaml b/tests/solidity/basic/excludeviewpure.yaml new file mode 100644 index 000000000..86d482e82 --- /dev/null +++ b/tests/solidity/basic/excludeviewpure.yaml @@ -0,0 +1,4 @@ +testMode: property +excludeViewPure: true +seed: 123 +testLimit: 5000 From 02ce40224809fd391f17019acd64cac3e7d67d8b Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Wed, 17 Jun 2026 07:42:55 +0200 Subject: [PATCH 2/4] removed unused import --- src/test/Tests/Integration.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/Tests/Integration.hs b/src/test/Tests/Integration.hs index 25ad6cdae..87cf2b00c 100644 --- a/src/test/Tests/Integration.hs +++ b/src/test/Tests/Integration.hs @@ -6,7 +6,7 @@ import Test.Tasty (TestTree, testGroup) import EVM.ABI (AbiValue(..)) -import Common (testContract, testContractV, solcV, testContract', checkConstructorConditions, passed, notPresent, solved, solvedLen, solvedWith, solvedWithout) +import Common (testContract, testContractV, solcV, testContract', checkConstructorConditions, passed, solved, solvedLen, solvedWith, solvedWithout) import Echidna.Types.Tx (TxCall(..)) import Echidna.Types.Worker (WorkerType(..)) From 76aec674e3b1cc3882cc66a117419cbace69d4a1 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Wed, 17 Jun 2026 08:11:33 +0200 Subject: [PATCH 3/4] test/config: fix remaining CI failures for excludeViewPure - default.yaml: add excludeViewPure (the config test requires every option be listed; it was failing with 'unset options: fromList ["excludeViewPure"]') - Tests/Integration: pin basic/excludeviewpure.sol to solc >= 0.8.0 (pragma ^0.8.0), so it is skipped on the <0.8 solc CI matrix instead of failing to compile. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/test/Tests/Integration.hs | 2 +- tests/solidity/basic/default.yaml | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/test/Tests/Integration.hs b/src/test/Tests/Integration.hs index 87cf2b00c..122bff481 100644 --- a/src/test/Tests/Integration.hs +++ b/src/test/Tests/Integration.hs @@ -35,7 +35,7 @@ integrationTests = testGroup "Solidity Integration Testing" , ("echidna_revert_always failed", passed "echidna_revert_always") , ("echidna_sometimesfalse passed", passed "echidna_sometimesfalse") ] - , testContract "basic/excludeviewpure.sol" (Just "basic/excludeviewpure.yaml") + , 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") diff --git a/tests/solidity/basic/default.yaml b/tests/solidity/basic/default.yaml index efd692c59..512a05acf 100644 --- a/tests/solidity/basic/default.yaml +++ b/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 From 0bcf626c1768659644447a1e0b27b638ab27a19d Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Mon, 20 Jul 2026 20:12:46 +0200 Subject: [PATCH 4/4] test: prove view/pure functions are excluded, using notPresent Addresses review feedback: excludeviewpure.sol gains a view function with a planted assert(false), and a new assertion-mode run checks that no assertion test is created for any view/pure function (via the previously unused notPresent helper), so the planted assert can never fire. A control run without excludeViewPure proves the assert IS found otherwise and pins the test names the notPresent checks look up. Co-Authored-By: Claude Fable 5 --- src/test/Tests/Integration.hs | 18 +++++++++++++++++- .../basic/excludeviewpure-assert-control.yaml | 3 +++ .../solidity/basic/excludeviewpure-assert.yaml | 4 ++++ tests/solidity/basic/excludeviewpure.sol | 8 ++++++++ 4 files changed, 32 insertions(+), 1 deletion(-) create mode 100644 tests/solidity/basic/excludeviewpure-assert-control.yaml create mode 100644 tests/solidity/basic/excludeviewpure-assert.yaml diff --git a/src/test/Tests/Integration.hs b/src/test/Tests/Integration.hs index 122bff481..931d028f7 100644 --- a/src/test/Tests/Integration.hs +++ b/src/test/Tests/Integration.hs @@ -6,7 +6,7 @@ import Test.Tasty (TestTree, testGroup) import EVM.ABI (AbiValue(..)) -import Common (testContract, testContractV, solcV, testContract', checkConstructorConditions, passed, solved, solvedLen, solvedWith, solvedWithout) +import Common (testContract, testContractV, solcV, testContract', checkConstructorConditions, notPresent, passed, solved, solvedLen, solvedWith, solvedWithout) import Echidna.Types.Tx (TxCall(..)) import Echidna.Types.Worker (WorkerType(..)) @@ -40,6 +40,22 @@ integrationTests = testGroup "Solidity Integration Testing" -- (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") ] + , testContractV "basic/excludeviewpure.sol" (Just (>= solcV (0,8,0))) (Just "basic/excludeviewpure-assert.yaml") + -- in assertion mode excludeViewPure must not create tests for view/pure + -- functions, so neverCalled()'s planted assert(false) can never fire + [ ("view assertion test must not be created", notPresent "neverCalled") + , ("view assertion test must not be created", notPresent "getCounter") + , ("pure assertion test must not be created", notPresent "getConst") + , ("non-view function must still be tested", passed "increment") + ] + , testContractV "basic/excludeviewpure.sol" (Just (>= solcV (0,8,0))) (Just "basic/excludeviewpure-assert-control.yaml") + -- control: without excludeViewPure the planted assert IS reachable and + -- the view/pure functions ARE tested, proving the notPresent checks + -- above are not vacuous (and pinning the test names they look up) + [ ("planted view assert must be found without excludeViewPure", solved "neverCalled") + , ("view function must be tested without excludeViewPure", passed "getCounter") + , ("pure function must be tested without excludeViewPure", passed "getConst") + ] , 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", diff --git a/tests/solidity/basic/excludeviewpure-assert-control.yaml b/tests/solidity/basic/excludeviewpure-assert-control.yaml new file mode 100644 index 000000000..9399a9c14 --- /dev/null +++ b/tests/solidity/basic/excludeviewpure-assert-control.yaml @@ -0,0 +1,3 @@ +testMode: assertion +seed: 123 +testLimit: 5000 diff --git a/tests/solidity/basic/excludeviewpure-assert.yaml b/tests/solidity/basic/excludeviewpure-assert.yaml new file mode 100644 index 000000000..b8cc86a41 --- /dev/null +++ b/tests/solidity/basic/excludeviewpure-assert.yaml @@ -0,0 +1,4 @@ +testMode: assertion +excludeViewPure: true +seed: 123 +testLimit: 5000 diff --git a/tests/solidity/basic/excludeviewpure.sol b/tests/solidity/basic/excludeviewpure.sol index 2cd8175ef..362d35185 100644 --- a/tests/solidity/basic/excludeviewpure.sol +++ b/tests/solidity/basic/excludeviewpure.sol @@ -24,4 +24,12 @@ contract ViewPureProperty { function getConst() external pure returns (uint256) { return 42; } + + // planted failing assert: with excludeViewPure no assertion test may be + // created for it (and the fuzzer must never call it); without the flag + // its assertion test must be found immediately + function neverCalled() external view returns (uint256) { + assert(false); + return counter; + } }