Skip to content

Allow changing prefix from prove via --prefix in test mode #745

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
May 19, 2025
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
currently executed branch is in fact impossible. In these cases, unwind all
frames and return a Revert with empty returndata.
- More rewrite rules for PEq, PNeg, missing eqByte call, and distributivity for And
- Allow changing of the prefix from "prove" via --prefix in `test` mode

## Fixed
- We now try to simplify expressions fully before trying to cast them to a concrete value
Expand Down Expand Up @@ -105,6 +106,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
increases which hurt concrete execution performance due to their linear cost.
- The concrete MCOPY implementation has been optimized to avoid freezing the whole
EVM memory.
- We no longer accept `check` as a prefix for test cases by default.

## [0.54.2] - 2024-12-12

Expand Down
5 changes: 4 additions & 1 deletion cli/cli.hs
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,7 @@ data TestOptions = TestOptions
, number ::Maybe W256
, coverage ::Bool
, match ::Maybe String
, prefix ::String
, ffi ::Bool
}

Expand All @@ -188,6 +189,7 @@ testOptions = TestOptions
<*> (optional $ option auto $ long "number" <> help "Block: number")
<*> (switch $ long "coverage" <> help "Coverage analysis")
<*> (optional $ strOption $ long "match" <> help "Test case filter - only run methods matching regex")
<*> (strOption $ long "prefix" <> showDefault <> value "prove" <> help "Prefix for test cases to prove")
<*> (switch $ long "ffi" <> help "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)")


Expand Down Expand Up @@ -257,7 +259,7 @@ commandParser :: Parser Command
commandParser = subparser
( command "test"
(info (Test <$> testOptions <*> commonOptions <**> helper)
(progDesc "Prove Foundry unit tests marked with `prove_`"
(progDesc "Prove Foundry unit tests prefixed with `prove` by default"
<> footer "For more help: https://hevm.dev/std-test-tutorial.html" ))
<> command "equivalence"
(info (Equal <$> eqOptions <*> commonOptions <**> helper)
Expand Down Expand Up @@ -815,6 +817,7 @@ unitTestOptions testOpts cOpts solvers buildOutput = do
, askSmtIters = cOpts.askSmtIterations
, smtTimeout = Just cOpts.smttimeout
, match = T.pack $ fromMaybe ".*" testOpts.match
, prefix = T.pack testOpts.prefix
, testParams = params
, dapp = srcInfo
, ffiAllowed = testOpts.ffi
Expand Down
30 changes: 12 additions & 18 deletions src/EVM/Dapp.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,6 @@ data DappInfo = DappInfo
, solcByHash :: Map W256 (CodeType, SolcContract)
, solcByCode :: [(Code, SolcContract)] -- for contracts with `immutable` vars.
, sources :: SourceCache
, unitTests :: [(Text, [Sig])]
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was actually unused

, abiMap :: Map FunctionSelector Method
, eventMap :: Map W256 Event
, errorMap :: Map W256 SolError
Expand Down Expand Up @@ -57,7 +56,6 @@ dappInfo root (BuildOutput (Contracts cs) sources) =

in DappInfo
{ root = root
, unitTests = findAllUnitTests solcs
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was actually unused, and so findAllUnitTests was also unused.

, sources = sources
, solcByName = cs
, solcByHash =
Expand Down Expand Up @@ -92,37 +90,33 @@ emptyDapp = dappInfo "" mempty
unitTestMarkerAbi :: FunctionSelector
unitTestMarkerAbi = abiKeccak (encodeUtf8 "IS_TEST()")

findAllUnitTests :: [SolcContract] -> [(Text, [Sig])]
findAllUnitTests = findUnitTests ".*:.*\\.(check|prove).*"

Comment on lines -95 to -97
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This function was unused.

mkSig :: Method -> Maybe Sig
mkSig method
| "prove" `isPrefixOf` testname = Just (Sig testname argtypes)
| "check" `isPrefixOf` testname = Just (Sig testname argtypes)
mkSig :: Text -> Method -> Maybe Sig
mkSig prefix method
| prefix `isPrefixOf` testname = Just (Sig testname argtypes)
| otherwise = Nothing
where
testname = method.name
argtypes = snd <$> method.inputs

findUnitTests :: Text -> ([SolcContract] -> [(Text, [Sig])])
findUnitTests match =
findUnitTests :: Text -> Text -> ([SolcContract] -> [(Text, [Sig])])
findUnitTests prefix match =
concatMap $ \c ->
case Map.lookup unitTestMarkerAbi c.abiMap of
Nothing -> []
Just _ ->
let testNames = unitTestMethodsFiltered (regexMatches match) c
let testNames = unitTestMethodsFiltered prefix (regexMatches match) c
in [(c.contractName, testNames) | not (BS.null c.runtimeCode) && not (null testNames)]

unitTestMethodsFiltered :: (Text -> Bool) -> (SolcContract -> [Sig])
unitTestMethodsFiltered matcher c =
unitTestMethodsFiltered :: Text -> (Text -> Bool) -> (SolcContract -> [Sig])
unitTestMethodsFiltered prefix matcher c =
let testName (Sig n _) = c.contractName <> "." <> n
in filter (matcher . testName) (unitTestMethods c)
in filter (matcher . testName) (unitTestMethods prefix c)

unitTestMethods :: SolcContract -> [Sig]
unitTestMethods =
unitTestMethods :: Text -> SolcContract -> [Sig]
unitTestMethods prefix =
(.abiMap)
>>> Map.elems
>>> mapMaybe mkSig
>>> mapMaybe (mkSig prefix)

traceSrcMap :: DappInfo -> Trace -> Maybe SrcMap
traceSrcMap dapp trace = srcMap dapp trace.contract trace.opIx
Expand Down
3 changes: 2 additions & 1 deletion src/EVM/UnitTest.hs
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ data UnitTestOptions s = UnitTestOptions
, askSmtIters :: Integer
, smtTimeout :: Maybe Natural
, match :: Text
, prefix :: Text
, dapp :: DappInfo
, testParams :: TestVMParams
, ffiAllowed :: Bool
Expand Down Expand Up @@ -112,7 +113,7 @@ makeVeriOpts opts =
-- | Returns tuple of (No Cex, No warnings)
unitTest :: App m => UnitTestOptions RealWorld -> Contracts -> m (Bool, Bool)
unitTest opts (Contracts cs) = do
let unitTestContrs = findUnitTests opts.match $ Map.elems cs
let unitTestContrs = findUnitTests opts.prefix opts.match $ Map.elems cs
conf <- readConfig
when conf.debug $ liftIO $ do
putStrLn $ "Found " ++ show (length unitTestContrs) ++ " unit test contract(s) to test:"
Expand Down
Loading