Use single conf.verb, warn users on zero-address use

CHANGELOG.md

@@ -42,6 +42,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Add deployment code flag to the `equivalenceCheck` function
 - PNeg + PGT/PGEq/PLeq/PLT simplification rules
 - We no longer dispatch Props to SMT that can be solved by a simplification
+- Allow user to change the verbosity level via `--verb`. For the moment, this is only to
+  print some warnings related to zero-address dereference and to print `hemv test`'s
+  output in case of failure
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value
@@ -71,6 +74,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Expressions that are commutative are now canonicalized to have the smaller
   value on the LHS. This can significantly help with simplifications, automatically
   determining when (Eq a b) is true when a==b modulo commutativity
+- `hevm test`'s flag ` --verbose` is now `--verb`, which also increases verbosity
+  for other elements of the system
 
 ## [0.54.2] - 2024-12-12
 

cli/cli.hs

@@ -109,6 +109,7 @@ data Command w
       , maxBranch     :: w ::: Int                <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
       , promiseNoReent:: w ::: Bool               <!> "Promise no reentrancy is possible into the contract(s) being examined"
       , maxBufSize    :: w ::: Int                <!> "64" <?> "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)"
+      , verb          :: w ::: Int                <!> "1" <?> "Verbosity level (default: 1)"
       }
   | Equivalence -- prove equivalence between two programs
       { codeA         :: w ::: Maybe ByteString   <?> "Bytecode of the first program"
@@ -134,6 +135,7 @@ data Command w
       , maxBranch     :: w ::: Int              <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
       , maxBufSize    :: w ::: Int              <!> "64" <?> "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)"
       , promiseNoReent:: w ::: Bool             <!> "Promise no reentrancy is possible into the contract(s) being examined"
+      , verb          :: w ::: Int              <!> "1" <?> "Verbosity level (default: 1)"
       , create        :: w ::: Bool             <?> "Tx: creation"
       }
   | Exec -- Execute a given program with specified env & calldata
@@ -164,14 +166,14 @@ data Command w
       , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"
       , projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
       , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
+      , verb        :: w ::: Int               <!> "1" <?> "Verbosity level (default: 1)"
       }
   | Test -- Run Foundry unit tests
       { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"
       , projectType   :: w ::: Maybe ProjectType        <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
       , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
       , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"
       , number        :: w ::: Maybe W256               <?> "Block: number"
-      , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"
       , coverage      :: w ::: Bool                     <?> "Coverage analysis"
       , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"
       , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
@@ -190,6 +192,7 @@ data Command w
       , askSmtIterations :: w ::: Integer               <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
       , maxBufSize    :: w ::: Int                      <!> "64" <?> "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)"
       , promiseNoReent:: w ::: Bool                     <!> "Promise no reentrancy is possible into the contract(s) being examined"
+      , verb          :: w ::: Int                      <!> "1" <?> "Verbosity level (default: 1)"
       }
   | Version
 
@@ -247,6 +250,7 @@ main = withUtf8 $ do
     , maxBranch = cmd.maxBranch
     , promiseNoReent = cmd.promiseNoReent
     , maxBufSize = getMaxBufSize 64 cmd
+    , verb = cmd.verb
     } }
   case cmd of
     Version {} ->putStrLn getFullVersion
@@ -726,7 +730,6 @@ unitTestOptions cmd solvers buildOutput = do
     , askSmtIters = cmd.askSmtIterations
     , smtTimeout = cmd.smttimeout
     , solver = cmd.solver
-    , verbose = cmd.verbose
     , match = T.pack $ fromMaybe ".*" cmd.match
     , testParams = params
     , dapp = srcInfo

doc/src/test.md

@@ -2,7 +2,7 @@
 
 ```
 Usage: hevm test [--root STRING] [--project-type PROJECTTYPE] [--rpc TEXT]
-                 [--number W256] [--verbose INT] [--coverage] [--match STRING]
+                 [--number W256] [--coverage] [--match STRING]
                  [--solver TEXT] [--num-solvers NATURAL] [--smtdebug] [--debug]
                  [--trace] [--ffi] [--smttimeout NATURAL]
                  [--max-iterations INTEGER]
@@ -16,7 +16,6 @@ Available options:
   --project-type PROJECTTYPE Foundry or CombinedJSON project
   --rpc TEXT               Fetch state from a remote node
   --number W256            Block: number
-  --verbose INT            Append call trace: {1} failures {2} all
   --coverage               Coverage analysis
   --match STRING           Test case filter - only run methods matching regex
   --solver TEXT            Used SMT solver: z3 (default), cvc5, or bitwuzla

src/EVM/Effects.hs

@@ -46,6 +46,7 @@ data Config = Config
   , maxBranch     :: Int
   , promiseNoReent   :: Bool
   , maxBufSize       :: Int
+  , verb        :: Int
   }
   deriving (Show, Eq)
 
@@ -62,6 +63,7 @@ defaultConfig = Config
   , maxBranch = 100
   , promiseNoReent = False
   , maxBufSize = 64
+  , verb = 0
   }
 
 -- Write to the console

src/EVM/Fetch.hs

@@ -217,6 +217,7 @@ oracle solvers info q = do
     PleaseFetchContract addr base continue -> do
       conf <- readConfig
       when (conf.debug) $ liftIO $ putStrLn $ "Fetching contract at " ++ show addr
+      when (addr == 0 && conf.verb > 0) $ liftIO $ putStrLn "Warning: fetching contract at address 0"
       contract <- case info of
         Nothing -> let
           c = case base of
@@ -231,6 +232,7 @@ oracle solvers info q = do
     PleaseFetchSlot addr slot continue -> do
       conf <- readConfig
       when (conf.debug) $ liftIO $ putStrLn $ "Fetching slot " <> (show slot) <> " at " <> (show addr)
+      when (addr == 0 && conf.verb > 0) $ liftIO $ putStrLn "Warning: fetching slot from a contract at address 0"
       case info of
         Nothing -> pure (continue 0)
         Just (n, url) ->

src/EVM/UnitTest.hs

@@ -48,7 +48,6 @@ import Witch (unsafeInto, into)
 data UnitTestOptions s = UnitTestOptions
   { rpcInfo     :: Fetch.RpcInfo
   , solvers     :: SolverGroup
-  , verbose     :: Maybe Int
   , maxIter     :: Maybe Integer
   , askSmtIters :: Integer
   , smtTimeout  :: Maybe Natural
@@ -181,10 +180,11 @@ runUnitTestContract
         Stepper.evm get
 
       writeTraceDapp dapp vm1
+      failOut <- failOutput vm1 opts "setUp()"
       case vm1.result of
         Just (VMFailure _) -> liftIO $ do
           Text.putStrLn "   \x1b[31m[BAIL]\x1b[0m setUp() "
-          tick $ indentLines 3 $ failOutput vm1 opts "setUp()"
+          tick $ indentLines 3 failOut
           pure [(True, False)]
         Just (VMSuccess _) -> do
           forM testSigs $ \s -> symRun opts vm1 s
@@ -240,22 +240,23 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     let allReverts = not . (any Expr.isSuccess) $ ends
     let unexpectedAllRevert = allReverts && not shouldFail
     when conf.debug $ liftIO $ putStrLn $ "symRun -- (cex,warnings,unexpectedAllRevert): " <> show (any isCex results, warnings, unexpectedAllRevert)
-    liftIO $ case (any isCex results, warnings, unexpectedAllRevert) of
+    txtResult <- case (any isCex results, warnings, unexpectedAllRevert) of
       (False, False, False) -> do
         -- happy case
-        putStr $ "   \x1b[32m[PASS]\x1b[0m " <> Text.unpack testName <> "\n"
+        pure $ "   \x1b[32m[PASS]\x1b[0m " <> Text.unpack testName <> "\n"
       (True, _, _) -> do
         -- there are counterexamples (and maybe other things, but Cex is most important)
         let x = mapMaybe extractCex results
-            y = symFailure opts testName (fst cd) types x
-        putStr $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n" <> Text.unpack y
+        y <- symFailure opts testName (fst cd) types x
+        pure $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n" <> Text.unpack y
       (_, True, _) -> do
         -- There are errors/unknowns/partials, we fail them
-        putStr $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n"
+        pure $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n"
       (_, _, True) -> do
         -- No cexes/errors/unknowns/partials, but all branches reverted
-        putStr $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n"
+        pure $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n"
           <> "   No reachable assertion violations, but all branches reverted\n"
+    liftIO $ putStr txtResult
     liftIO $ printWarnings ends results t
     pure (not (any isCex results), not (warnings || unexpectedAllRevert))
 
@@ -268,28 +269,26 @@ printWarnings e results testName = do
     forM_ (groupPartials e) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
   putStrLn ""
 
-symFailure :: UnitTestOptions RealWorld -> Text -> Expr Buf -> [AbiType] -> [(Expr End, SMTCex)] -> Text
-symFailure UnitTestOptions {..} testName cd types failures' =
-  mconcat
-    [ Text.concat $ indentLines 3 . mkMsg <$> failures'
-    ]
-    where
+symFailure :: App m => UnitTestOptions RealWorld -> Text -> Expr Buf -> [AbiType] -> [(Expr End, SMTCex)] -> m Text
+symFailure UnitTestOptions {..} testName cd types failures' = do
+  conf <- readConfig
+  pure $ mconcat [ Text.concat $ indentLines 3 . mkMsg conf <$> failures' ]
+  where
       showRes = \case
         Success _ _ _ _ -> if "proveFail" `isPrefixOf` testName
                            then "Successful execution"
                            else "Failed: Test Assertion Violation"
         res ->
           let ?context = dappContext (traceContext res)
           in Text.pack $ prettyvmresult res
-      mkMsg (leaf, cex) = intercalate "\n" $
+      mkMsg conf (leaf, cex) = intercalate "\n" $
         ["Counterexample:"
         ,"  calldata: " <> let ?context = dappContext (traceContext leaf)
                            in prettyCalldata cex cd testName types
         ,"  result:   " <> showRes leaf
-        ] <> verbText leaf
-      verbText leaf = case verbose of
-            Just _ -> [Text.unlines [ indentLines 2 (showTraceTree' dapp leaf)]]
-            _ -> mempty
+        ] <> verbText conf leaf
+      verbText conf leaf = if conf.verb <= 1 then mempty
+                           else [Text.unlines [ indentLines 2 (showTraceTree' dapp leaf)]]
       dappContext TraceContext { contracts, labels } =
         DappContext { info = dapp, contracts, labels }
 
@@ -298,37 +297,20 @@ indentLines n s =
   let p = Text.replicate n " "
   in Text.unlines (map (p <>) (Text.lines s))
 
-passOutput :: VM t s -> UnitTestOptions s -> Text -> Text
-passOutput vm UnitTestOptions { .. } testName =
-  let ?context = DappContext { info = dapp
-                             , contracts = vm.env.contracts
-                             , labels = vm.labels }
-  in let v = fromMaybe 0 verbose
-  in if (v > 1) then
-    mconcat
-      [ "Success: "
-      , fromMaybe "" (stripSuffix "()" testName)
-      , "\n"
-      , if (v > 2) then indentLines 2 (showTraceTree dapp vm) else ""
-      , indentLines 2 (formatTestLogs dapp.eventMap vm.logs)
-      , "\n"
-      ]
-    else ""
-
-failOutput :: VM t s -> UnitTestOptions s -> Text -> Text
-failOutput vm UnitTestOptions { .. } testName =
+failOutput :: App m => VM t s -> UnitTestOptions s -> Text -> m Text
+failOutput vm UnitTestOptions { .. } testName = do
+  conf <- readConfig
   let ?context = DappContext { info = dapp
                              , contracts = vm.env.contracts
                              , labels = vm.labels }
-  in mconcat
-  [ "Failure: "
-  , fromMaybe "" (stripSuffix "()" testName)
-  , "\n"
-  , case verbose of
-      Just _ -> indentLines 2 (showTraceTree dapp vm)
-      _ -> ""
-  , indentLines 2 (formatTestLogs dapp.eventMap vm.logs)
-  ]
+  pure $ mconcat
+    [ "Failure: "
+    , fromMaybe "" (stripSuffix "()" testName)
+    , "\n"
+    , if conf.verb <= 1 then ""
+      else indentLines 2 (showTraceTree dapp vm)
+    , indentLines 2 (formatTestLogs dapp.eventMap vm.logs)
+    ]
 
 formatTestLogs :: (?context :: DappContext) => Map W256 Event -> [Expr Log] -> Text
 formatTestLogs events xs =

test/EVM/Test/Utils.hs

@@ -59,7 +59,6 @@ testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do
     , askSmtIters = 1
     , smtTimeout = Nothing
     , solver = Nothing
-    , verbose = Just 1
     , match = match
     , testParams = params
     , dapp = srcInfo