Improved support for foundry tests

.github/workflows/ci.yml

@@ -232,11 +232,13 @@ jobs:
     steps:
       - name: Checkout
         uses: actions/checkout@v6
+        with:
+          submodules: recursive
 
       - name: Setup Python
         uses: actions/setup-python@v6
         with:
-          python-version: '3.8'
+          python-version: '3.10'
 
       - name: Install dependencies
         shell: bash

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "tests/solidity/foundry/forge-std"]
+	path = tests/solidity/foundry/forge-std
+	url = https://github.com/foundry-rs/forge-std

README.md

@@ -54,6 +54,17 @@ $ echidna tests/solidity/basic/flags.sol
 
 Echidna should find a call sequence that falsifies `echidna_sometimesfalse` and should be unable to find a falsifying input for `echidna_alwaystrue`.
 
+### Testing modes
+
+The example above uses the default **property** mode, but Echidna supports several testing modes, configured via `testMode` in the config file or `--test-mode` on the CLI:
+
+* **`property`** (default): Test `echidna_`-prefixed functions that return `bool`.
+* **`assertion`**: Detect assertion failures from `assert()` and Foundry's `assertX` helpers (`assertTrue`, `assertEq`, etc.).
+* **`foundry`**: Run Foundry-style `test`-prefixed unit tests and `invariant_`-prefixed stateful invariants.
+* **`overflow`**: Detect integer over/underflows (Solidity >= 0.8.0).
+* **`optimization`**: Maximize the return value of `echidna_opt_`-prefixed functions.
+* **`exploration`**: Collect coverage without checking properties.
+
 ### Collecting and visualizing coverage
 
 After finishing a campaign, Echidna can save a coverage maximizing **corpus** in a special directory specified with the `corpusDir` config option. This directory will contain two entries: (1) a directory named `coverage` with JSON files that can be replayed by Echidna and (2) a plain-text file named `covered.txt`, a copy of the source code with coverage annotations.
@@ -143,8 +154,8 @@ Transaction = {
 
 `Coverage` is a dict describing certain coverage-increasing calls. These interfaces are
 subject to change to be slightly more user-friendly at a later date. `testType`
-will either be `property` or `assertion`, and `status` always takes on either
-`fuzzing`, `shrinking`, `solved`, `passed`, or `error`.
+will be one of `property`, `assertion`, `optimization`, `exploration`, or `call`,
+and `status` always takes on either `fuzzing`, `shrinking`, `solved`, `passed`, or `error`.
 
 ### Debugging Performance Problems
 

lib/Echidna.hs

@@ -58,11 +58,12 @@ prepareContract
   -> IO (VM Concrete, Env, GenDict)
 prepareContract cfg solFiles buildOutput selectedContract seed = do
   let solConf = cfg.solConf
+      campaignConf = cfg.campaignConf
       (Contracts contractMap) = buildOutput.contracts
       contracts = Map.elems contractMap
 
   mainContract <- selectMainContract solConf selectedContract contracts
-  tests <- mkTests solConf mainContract
+  tests <- mkTests solConf campaignConf mainContract
   signatureMap <- mkSignatureMap solConf mainContract contracts
 
   -- run processors

lib/Echidna/Output/Foundry.hs

@@ -76,7 +76,10 @@ foundryTx senders tx =
         prelude =
           (if time > 0 || blocks > 0 then "    _delay(" ++ show time ++ ", " ++ show blocks ++ ");\n" else "") ++
           "    _setUpActor(" ++ senderName ++ ");"
-        call = "    Target." ++ unpack name ++ "(" ++ foundryArgs (map abiValueToString args) ++ ");"
+        -- Handle fallback function (empty name).
+        call = if unpack name == ""
+          then "    address(Target).call(\"\");"
+          else "    Target." ++ unpack name ++ "(" ++ foundryArgs (map abiValueToString args) ++ ");"
       in Just $ object ["prelude" .= prelude, "call" .= call]
     _ -> Nothing
 

lib/Echidna/Solidity.hs

@@ -41,7 +41,7 @@ import Echidna.ABI
 import Echidna.Deploy (deployContracts, deployBytecodes)
 import Echidna.Exec (execTx, execTxWithCov, initialVM)
 import Echidna.SourceAnalysis.Slither
-import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isDapptestMode)
+import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isFoundryMode)
 import Echidna.Types.Campaign (CampaignConf(..))
 import Echidna.Types.Config (EConfig(..), Env(..))
 import Echidna.Types.Signature
@@ -146,11 +146,19 @@ filterMethods contractName (Whitelist ic) ms =
 filterMethods contractName (Blacklist ig) ms =
   NE.filter (\s -> encodeSigWithName contractName s `notElem` ig) ms
 
--- | Filter methods with arguments, used for dapptest mode
+-- | Filter methods for foundry mode. Per Foundry conventions:
+-- - Functions prefixed with "test" are test functions (unit or fuzz).
+--   Fuzz tests are distinguished by having at least one parameter.
+--   See: https://book.getfoundry.sh/forge/fuzz-testing
+-- - Functions prefixed with "invariant_" are invariant tests, called in
+--   randomized sequences to verify properties that must always hold.
+--   See: https://book.getfoundry.sh/forge/invariant-testing
+-- - Other functions with arguments are kept as callable targets for
+--   invariant test campaigns.
 filterMethodsWithArgs :: NonEmpty SolSignature -> NonEmpty SolSignature
 filterMethodsWithArgs ms =
-  case NE.filter (\(n, xs) -> T.isPrefixOf "invariant_" n || not (null xs)) ms of
-    [] -> error "No dapptest tests found"
+  case NE.filter (\(n, xs) -> T.isPrefixOf "test" n || (T.isPrefixOf "invariant_" n || not (null xs))) ms of
+    [] -> error "No foundry tests found"
     fs -> NE.fromList fs
 
 abiOf :: Text -> SolcContract -> NonEmpty SolSignature
@@ -223,16 +231,17 @@ loadSpecified env mainContract cs = do
                                            solConf.contractAddr
                                            unlimitedGasPerBlock
                                            (0, 0)
-    vm4 <- if isDapptestMode solConf.testMode && setUpFunction `elem` abi
+    vm4 <- if is_testFunction `elem` abi && setUpFunction `elem` abi
               then snd <$> transaction
               else pure vm3
 
     case vm4.result of
-      Just (VMFailure _) -> throwM SetUpCallFailed
+      Just (VMFailure _) -> throwM $ SetUpCallFailed $ showTraceTree env.dapp vm4
       _ -> pure vm4
 
   where
     setUpFunction = ("setUp", [])
+    is_testFunction = ("IS_TEST", [])
 
 
 selectMainContract
@@ -259,7 +268,7 @@ mkSignatureMap
 mkSignatureMap solConf mainContract contracts = do
   let
     -- Filter ABI according to the config options
-    fabiOfc = if isDapptestMode solConf.testMode
+    fabiOfc = if isFoundryMode solConf.testMode
                 then NE.toList $ filterMethodsWithArgs (abiOf solConf.prefix mainContract)
                 else filterMethods mainContract.contractName solConf.methodFilter $
                        abiOf solConf.prefix mainContract
@@ -276,22 +285,23 @@ mkSignatureMap solConf mainContract contracts = do
         case NE.nonEmpty fabiOfc of
           Just ne -> Map.singleton mainContract.runtimeCodehash ne
           Nothing -> mempty
-  when (null abiMapping && isDapptestMode solConf.testMode) $
+  when (null abiMapping && isFoundryMode solConf.testMode) $
     throwM NoTests
   when (Map.null abiMapping) $
     throwM $ InvalidMethodFilters solConf.methodFilter
   pure abiMapping
 
 mkTests
   :: SolConf
+  -> CampaignConf
   -> SolcContract
   -> IO [EchidnaTest]
-mkTests solConf mainContract = do
+mkTests solConf campaignConf mainContract = do
   let
     -- generate the complete abi mapping
     abi = Map.elems mainContract.abiMap <&> \method -> (method.name, snd <$> method.inputs)
     (tests, funs) = partition (isPrefixOf solConf.prefix . fst) abi
-    -- Filter again for dapptest tests or assertions checking if enabled
+    -- Filter again for foundry tests or assertions checking if enabled
     neFuns = filterMethods mainContract.contractName
                            solConf.methodFilter
                            (fallback NE.:| funs)
@@ -309,6 +319,7 @@ mkTests solConf mainContract = do
   pure $ createTests solConf.testMode
                      solConf.testDestruction
                      testNames
+                     campaignConf.seqLen
                      solConf.contractAddr
                      neFuns
 
@@ -348,7 +359,7 @@ mkWorld SolConf{sender, testMode} sigMap maybeContract slitherInfo 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 isDapptestMode testMode then [] else filterResults maybeContract slitherInfo.constantFunctions \\ as
+    cs = if isFoundryMode testMode 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/SourceAnalysis/Slither.hs

@@ -3,6 +3,7 @@
 module Echidna.SourceAnalysis.Slither where
 
 import Control.Applicative ((<|>))
+import Control.Monad (unless)
 import Data.Aeson ((.:), (.:?), (.!=), eitherDecode, parseJSON, withEmbeddedJSON, withObject)
 import Data.Aeson.Types (FromJSON, Parser, Value(String))
 import Data.ByteString.Base16 qualified as BS16 (decode)
@@ -147,16 +148,18 @@ instance FromJSON SlitherInfo where
 runSlither :: FilePath -> SolConf -> IO SlitherInfo
 runSlither fp solConf = if solConf.disableSlither
   then do
-    hPutStrLn stderr $
-        "WARNING: Slither was explicitly disabled. Echidna uses Slither (https://github.com/crytic/slither)"
-        <> " to perform source analysis, which makes fuzzing more effective. You should enable it."
+    unless solConf.quiet $
+      hPutStrLn stderr
+        ( "WARNING: Slither was explicitly disabled. Echidna uses Slither (https://github.com/crytic/slither)"
+        <> " to perform source analysis, which makes fuzzing more effective. You should enable it." )
     pure emptySlitherInfo
   else findExecutable "slither" >>= \case
     Nothing -> do
-      hPutStrLn stderr $
-        "WARNING: slither not found. Echidna uses Slither (https://github.com/crytic/slither)"
-        <> " to perform source analysis, which makes fuzzing more effective. You should install it with"
-        <> " 'pip3 install slither-analyzer --user'"
+      unless solConf.quiet $
+        hPutStrLn stderr
+          ( "WARNING: slither not found. Echidna uses Slither (https://github.com/crytic/slither)"
+          <> " to perform source analysis, which makes fuzzing more effective. You should install it with"
+          <> " 'pip3 install slither-analyzer --user'" )
       pure emptySlitherInfo
     Just path -> do
       let args = ["--ignore-compile", "--print", "echidna", "--json", "-"]

lib/Echidna/SymExec/Common.hs

@@ -1,7 +1,13 @@
+{-# LANGUAGE GADTs #-}
+
 module Echidna.SymExec.Common where
 
 import Control.Monad.IO.Unlift (MonadUnliftIO, liftIO)
 import Control.Monad.State.Strict (execState, runStateT)
+import Data.ByteString (ByteString)
+import Data.ByteString qualified as BS
+import Data.DoubleWord (Word256)
+import Data.List (foldl')
 import Data.Function ((&))
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, mapMaybe)
@@ -11,22 +17,57 @@ import Data.Text qualified as T
 import Optics.Core ((.~), (%), (%~))
 
 import EVM (loadContract, resetState, symbolify)
-import EVM.ABI (abiKind, AbiKind(Dynamic), Sig(..), decodeBuf, AbiVals(..))
+import EVM.ABI (abiKind, AbiKind(Dynamic), Sig(..), decodeBuf, AbiVals(..), selector, encodeAbiValue, AbiValue(..))
 import EVM.Effects (TTY, ReadConfig)
 import EVM.Expr qualified
 import EVM.Fetch qualified as Fetch
 import EVM.Format (formatPartialDetailed)
 import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..), WarningData(..))
 import EVM.Solvers (SolverGroup)
-import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), checkAssertions, subModel, defaultSymbolicValues)
-import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
+import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), subModel, defaultSymbolicValues, Postcondition)
+import EVM.Types (Addr, VMType(..), EType(..), EvmError(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
 import qualified EVM.Types (VM(..))
 
+import Echidna.Test (assumeMagicReturnCode, isFoundryMode)
 import Echidna.Types (fromEVM)
 import Echidna.Types.Config (EConfig(..))
 import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Tx (Tx(..), TxCall(..), TxConf(..), maxGasPerBlock)
 
+panicMsg :: Word256 -> ByteString
+panicMsg err = selector "Panic(uint256)" <> encodeAbiValue (AbiUInt 256 err)
+
+-- | Postcondition for symbolic execution verification.
+-- In foundry mode, all reverts are failures except vm.assume failures.
+-- In assertion mode, only assertion failures (0xfe opcode, Error(string)
+-- "assertion failed", or Panic codes) are detected.
+checkAssertions :: [Word256] -> Bool -> Postcondition
+checkAssertions errs isFoundry _ vmres
+  | isFoundry = case vmres of
+      -- vm.assume failures should not be treated as test failures
+      Failure _ _ (Revert (ConcreteBuf bs))
+        | assumeMagicReturnCode `BS.isSuffixOf` bs -> PBool True
+      -- All other failures are test failures in foundry mode
+      Failure {} -> PBool False
+      _ -> PBool True
+  | otherwise = case vmres of
+      -- Solidity assert() opcode (0xfe)
+      Failure _ _ (UnrecognizedOpcode 0xfe) -> PBool False
+      -- Concrete revert: check for "assertion failed" message or panic code
+      Failure _ _ (Revert (ConcreteBuf msg)) ->
+        -- NOTE: assertTrue/assertFalse does not have the double colon after "assertion failed"
+        let assertFail = selector "Error(string)" `BS.isPrefixOf` msg
+              && "assertion failed" `BS.isPrefixOf` BS.drop txtOffset msg
+        in PBool $ not (assertFail || msg `elem` fmap panicMsg errs)
+      -- Symbolic revert: check symbolically against panic messages
+      -- TODO: also check for Error(string) "assertion failed" in partially-symbolic
+      -- buffers, similar to hevm's symbolicFail in EVM.UnitTest
+      Failure _ _ (Revert b) ->
+        foldl' PAnd (PBool True) (fmap (PNeg . PEq b . ConcreteBuf . panicMsg) errs)
+      _ -> PBool True
+  where
+    txtOffset = 4 + 32 + 32 -- selector + offset + length
+
 type PartialsLogs = [T.Text]
 
 data TxOrError = TxFromResult Tx | SMTErrorFromResult String
@@ -137,7 +178,8 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
   let
     vm' = vmReset & execState (loadContract (LitAddr dst))
                   & #tx % #isCreate .~ False
-                  & #state % #callvalue .~ TxValue
+                  -- Foundry tests cannot accept ether, force callvalue to zero
+                  & #state % #callvalue .~ (if isFoundryMode conf.solConf.testMode then Lit 0 else TxValue)
                   & #state % #caller .~ SymAddr "caller"
                   & #state % #calldata .~ cd
 
@@ -148,8 +190,9 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
 
   -- TODO we might want to switch vm's state.baseState value to to AbstractBase eventually.
   -- Doing so might mess up concolic execution.
-  (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (checkAssertions [0x1]) Nothing
+  let foundry = isFoundryMode conf.solConf.testMode
+  (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (checkAssertions [0x1] foundry) Nothing
   let results = filter (\(r, _) -> not (isQed r)) models & map fst
   let warnData = Just $ WarningData contract sources vm'
-  --liftIO $ mapM_ TIO.putStrLn partials
+  --liftIO $ mapM_ print partials
   return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (formatPartialDetailed warnData . fst) partials)