Generate Foundry reproducers in property mode

lib/Echidna/Config.hs

@@ -14,7 +14,7 @@ import Data.Text (isPrefixOf)
 import Data.Yaml qualified as Y
 
 import EVM.Solvers (Solver(..))
-import EVM.Types (VM(..), W256)
+import EVM.Types (Addr, VM(..), W256)
 
 import Echidna.Mutator.Corpus (defaultMutationConsts)
 import Echidna.Test
@@ -82,7 +82,7 @@ instance FromJSON EConfigWithUsage where
         <*> getWord256 "maxValue" 100000000000000000000 -- 100 eth
 
       testConfParser = do
-        psender <- v ..:? "psender" ..!= 0x10000
+        psender <- v ..:? "psender" ..!= defaultPsender
         fprefix <- v ..:? "prefix"  ..!= "echidna_"
         let goal fname = if (fprefix <> "revert_") `isPrefixOf` fname then ResRevert else ResTrue
             classify fname vm = maybe ResOther classifyRes vm.result == goal fname
@@ -159,6 +159,10 @@ instance FromJSON EConfigWithUsage where
         Nothing -> pure Nothing
         _ -> fail "Unrecognized format type (should be text, json, or none)")
 
+-- | Default address for the property test sender.
+defaultPsender :: Addr
+defaultPsender = 0x10000
+
 -- | The default config used by Echidna (see the 'FromJSON' instance for values used).
 defaultConfig :: EConfig
 defaultConfig = either (error "Config parser got messed up :(") id $ Y.decodeEither' ""

lib/Echidna/Output/Foundry.hs

@@ -5,6 +5,7 @@
 module Echidna.Output.Foundry (foundryTest) where
 
 import Data.Aeson (Value(..), object, (.=))
+import Data.Functor ((<&>))
 import Data.List (elemIndex, nub)
 import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Text (Text, unpack)
@@ -27,28 +28,38 @@ template :: Template
 template = $(embedTemplate ["lib/Echidna/Output/assets"] "foundry.mustache")
 
 -- | Generate a Foundry test from an EchidnaTest result.
-foundryTest :: Maybe Text -> EchidnaTest -> TL.Text
-foundryTest mContractName test =
+-- For property tests, psender is the address used to call the property function.
+foundryTest :: Maybe Text -> Addr -> EchidnaTest -> TL.Text
+foundryTest mContractName psender test =
   case test.testType of
     AssertionTest{} ->
-      let testData = createTestData mContractName test
+      let testData = createTestData mContractName Nothing test
+      in fromStrict $ substituteValue template (toMustache testData)
+    PropertyTest name _ ->
+      let testData = createTestData mContractName (Just (name, psender)) test
       in fromStrict $ substituteValue template (toMustache testData)
     _ -> ""
 
 -- | Create an Aeson Value from test data for the Mustache template.
-createTestData :: Maybe Text -> EchidnaTest -> Value
-createTestData mContractName test =
+-- When a property name and psender are provided, a final assertion is added
+-- to call the property from psender and check it returns false.
+createTestData :: Maybe Text -> Maybe (Text, Addr) -> EchidnaTest -> Value
+createTestData mContractName mProperty test =
   let
     senders = nub $ map (.src) test.reproducer
     actors = zipWith actorObject senders [1..]
     repro = mapMaybe (foundryTx senders) test.reproducer
     cName = fromMaybe "YourContract" mContractName
+    propAssertion = mProperty <&> \(name, addr) ->
+      "        vm.stopPrank();\n        vm.prank(" ++ formatAddr addr ++ ");\n"
+      ++ "        assertFalse(Target." ++ unpack name ++ "());"
   in
   object
     [ "testName"     .= ("FoundryTest" :: Text)
     , "contractName" .= cName
     , "actors"       .= actors
     , "reproducer"   .= repro
+    , "propertyAssertion" .= propAssertion
     ]
 
 -- | Create a JSON object for an actor.

lib/Echidna/Output/assets/foundry.mustache

@@ -21,6 +21,9 @@ contract {{testName}} is Test {
     {{{prelude}}}
     {{{call}}}
 {{/reproducer}}
+{{#propertyAssertion}}
+{{{.}}}
+{{/propertyAssertion}}
   }
 
   function _setUpActor(address actor) internal {

src/Main.hs

@@ -45,7 +45,7 @@ import Echidna.Test (validateTestMode)
 import Echidna.Types.Campaign
 import Echidna.Types.Config
 import Echidna.Types.Solidity
-import Echidna.Types.Test (TestMode, EchidnaTest(..), TestType(..), TestState(..))
+import Echidna.Types.Test (TestMode, EchidnaTest(..), TestConf(..), TestType(..), TestState(..))
 import Echidna.UI
 import Echidna.Utility (measureIO)
 
@@ -93,16 +93,19 @@ main = withUtf8 $ withCP65001 $ do
           isLargeOrSolved _ = False
       measureIO cfg.solConf.quiet "Saving foundry reproducers" $ do
         let foundryDir = dir </> "foundry"
-        liftIO $ createDirectoryIfMissing True foundryDir
-        forM_ tests $ \test ->
-          case (test.testType, test.state) of
-            (AssertionTest{}, state) | isLargeOrSolved state ->
-              do
+            TestConf{testSender} = cfg.testConf
+            psender = testSender 0
+            saveRepro test = do
               let
                 reproducerHash = (show . abs . hash) test.reproducer
                 fileName = foundryDir </> "Test." ++ reproducerHash <.> "sol"
-                content = foundryTest cliSelectedContract test
+                content = foundryTest cliSelectedContract psender test
               liftIO $ writeFile fileName (TL.unpack content)
+        liftIO $ createDirectoryIfMissing True foundryDir
+        forM_ tests $ \test ->
+          case (test.testType, test.state) of
+            (AssertionTest{}, state) | isLargeOrSolved state -> saveRepro test
+            (PropertyTest{}, state) | isLargeOrSolved state -> saveRepro test
             _ -> pure ()
 
 

src/test/Tests/FoundryTestGen.hs

@@ -15,6 +15,7 @@ import System.Process (readProcessWithExitCode)
 import Text.Read (readMaybe)
 
 import Common (solved, passed, testContract, testContractNamed)
+import Echidna.Config (defaultPsender)
 import Echidna.Types.Config (Env)
 import Echidna.Types.Campaign (WorkerState)
 import EVM.ABI (AbiValue(..))
@@ -29,6 +30,7 @@ foundryTestGenTests = testGroup "Foundry test generation"
   , testCase "correctly encodes bytes1" testBytes1Encoding
   , testCase "fallback function syntax" testFallbackSyntax
   , testCase "null bytes in arguments" testNullBytes
+  , testCase "property test generates assertFalse" testPropertyTestGen
   , testGroup "Concrete execution (fuzzing)"
       [ testForgeStd "solves assertTrue"
           "foundry/FoundryAsserts.sol"
@@ -159,6 +161,9 @@ foundryTestGenTests = testGroup "Foundry test generation"
           FuzzWorker
           [ ("vm.assume should not be treated as test failure", passed "test_assume_filters")
           ]
+      , testContract "foundry/PropertyRepro.sol" (Just "foundry/PropertyRepro.yaml")
+          [ ("property test should be detected", solved "echidna_counter_is_zero")
+          ]
       ]
   , testGroup "Symbolic execution (SMT solving)"
       [ testForgeStd "solves assertTrue"
@@ -287,7 +292,7 @@ testForgeCompiles tmpDirSuffix contractName testData outputFile = do
           copyFile contractPath (tmpDir ++ "/src/" ++ contractFile)
 
           -- Generate test and add contract import after forge-std import
-          let generated = TL.unpack $ foundryTest (Just (pack contractName)) testData
+          let generated = TL.unpack $ foundryTest (Just (pack contractName)) defaultPsender testData
               forgeStdImport = pack "import \"forge-std/Test.sol\";"
               contractImport = pack $ "import \"../src/" ++ contractFile ++ "\";"
               testWithImport = unpack $ replace forgeStdImport
@@ -318,11 +323,38 @@ testBytes1Encoding = do
       , delay = (0, 0)
       }
     test = mkMinimalTest { reproducer = [reproducerTx] }
-    generated = TL.unpack $ foundryTest (Just "FoundryTestTarget") test
+    generated = TL.unpack $ foundryTest (Just "FoundryTestTarget") defaultPsender test
   if "hex\"92\"" `isInfixOf` generated
     then pure ()
     else assertFailure $ "bytes1 not correctly encoded: " ++ generated
 
+-- | Test that property mode tests generate assertFalse with psender prank.
+testPropertyTestGen :: IO ()
+testPropertyTestGen = do
+  let
+    reproducerTx = Tx
+      { call = SolCall ("inc", [])
+      , src = 0x10000
+      , dst = 0
+      , value = 0
+      , gas = 0
+      , gasprice = 0
+      , delay = (0, 0)
+      }
+    test = mkMinimalTest
+      { testType = PropertyTest "echidna_counter_is_zero" 0
+      , reproducer = [reproducerTx]
+      }
+    generated = TL.unpack $ foundryTest (Just "PropertyRepro") defaultPsender test
+  assertBool ("should contain assertFalse call, got: " ++ generated)
+    ("assertFalse(Target.echidna_counter_is_zero())" `isInfixOf` generated)
+  assertBool ("should contain vm.prank for psender, got: " ++ generated)
+    ("vm.prank(" `isInfixOf` generated)
+  assertBool ("should contain vm.stopPrank, got: " ++ generated)
+    ("vm.stopPrank()" `isInfixOf` generated)
+  assertBool ("should contain inc() call, got: " ++ generated)
+    ("Target.inc()" `isInfixOf` generated)
+
 -- | Wrapper for testContractNamed that skips if solc < 0.8.13.
 testForgeStd :: String -> FilePath -> Maybe String -> Maybe FilePath -> WorkerType -> [(String, (Env, WorkerState) -> IO Bool)] -> TestTree
 testForgeStd name fp contract config workerType checks =

tests/solidity/foundry/PropertyRepro.sol

@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+contract PropertyRepro {
+    uint256 public counter;
+
+    function inc() public {
+        counter++;
+    }
+
+    function echidna_counter_is_zero() public view returns (bool) {
+        return counter == 0;
+    }
+}

tests/solidity/foundry/PropertyRepro.yaml

@@ -0,0 +1,3 @@
+testMode: property
+seed: 1234
+disableSlither: true