From 016f3ec187170c53720a637876eb5394ad42fcea Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 25 Oct 2023 14:52:37 +0200
Subject: [PATCH] Fixing verbosity

---
 cli/cli.hs         | 10 +++++-----
 src/EVM/Effects.hs |  4 ++--
 test/test.hs       |  4 ++--
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/cli/cli.hs b/cli/cli.hs
index 365852252..eaa4f5490 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -86,7 +86,7 @@ data Command w
       , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"
       , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc5"
       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"
-      , verbose       :: w ::: Maybe Bool         <?> "More verbose printing of internal behaviour"
+      , verbose       :: w ::: Maybe Int          <?> "Verbose printing of internal behaviour (default:0)"
       , assertions    :: w ::: Maybe [Word256]    <?> "Comma separated list of solc panic codes to check for (default: user defined assertion violations only)"
       , 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)"
       , numSolvers    :: w ::: Maybe Natural      <?> "Number of solver instances to use (default: number of cpu cores)"
@@ -105,7 +105,7 @@ data Command w
       , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default) or cvc5"
       , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"
       , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"
-      , verbose       :: w ::: Maybe Bool       <?> "More verbose printing of internal behaviour"
+      , verbose       :: w ::: Maybe Int        <?> "Verbose printing of internal behaviour (default:0)"
       , trace         :: w ::: Bool             <?> "Dump trace"
       , 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)"
       , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
@@ -147,7 +147,7 @@ data Command w
       , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"
       , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc5"
       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"
-      , verbose       :: w ::: Maybe Bool               <?> "More verbose printing of internal behaviour"
+      , verbose       :: w ::: Maybe Int                <?> "Verbose printing of internal behaviour (default:0)"
       , trace         :: w ::: Bool                     <?> "Dump trace"
       , ffi           :: w ::: Bool                     <?> "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)"
       , smttimeout    :: w ::: Maybe Natural            <?> "Timeout given to SMT solver in seconds (default: 300)"
@@ -193,7 +193,7 @@ main = do
   cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"
   let env = Env { config = defaultConfig
     { dumpQueries = cmd.smtdebug
-    , verbose = fromMaybe False cmd.verbose
+    , verbose = fromMaybe 0 cmd.verbose
     , abstRefineMem = cmd.abstractMemory
     , abstRefineArith = cmd.abstractArithmetic
     , dumpTrace = cmd.trace
@@ -595,7 +595,7 @@ unitTestOptions cmd solvers buildOutput = do
     , askSmtIters = cmd.askSmtIterations
     , smtTimeout = cmd.smttimeout
     , solver = cmd.solver
-    , verbose = cmd.verbose
+    , verbose = fromMaybe 0 cmd.verbose
     , match = T.pack $ fromMaybe ".*" cmd.match
     , testParams = params
     , dapp = srcInfo
diff --git a/src/EVM/Effects.hs b/src/EVM/Effects.hs
index 09a31e46d..3256b9ce8 100644
--- a/src/EVM/Effects.hs
+++ b/src/EVM/Effects.hs
@@ -46,7 +46,7 @@ data Config = Config
   { dumpQueries     :: Bool
   , dumpExprs       :: Bool
   , dumpEndStates   :: Bool
-  , verbose         :: Bool
+  , verbose         :: Int
   , abstRefineArith :: Bool
   , abstRefineMem   :: Bool
   , dumpTrace       :: Bool
@@ -58,7 +58,7 @@ defaultConfig = Config
   { dumpQueries = False
   , dumpExprs = False
   , dumpEndStates = False
-  , verbose = False
+  , verbose = 0
   , abstRefineArith = False
   , abstRefineMem   = False
   , dumpTrace = False
diff --git a/test/test.hs b/test/test.hs
index a21f68d37..11387fb40 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -73,7 +73,7 @@ testEnv = Env { config = defaultConfig {
   dumpQueries = False
   , dumpExprs = False
   , dumpEndStates = False
-  , verbose = False
+  , verbose = 0
   , abstRefineArith = False
   , abstRefineMem   = False
   , dumpTrace = False
@@ -3122,7 +3122,7 @@ tests = testGroup "hevm"
           start <- liftIO $ getCurrentTime
           putStrLnM $ "Checking file: " <> f
           conf <- readConfig
-          when conf.verbose $ liftIO $ do
+          when (conf.verbose > 0) $ liftIO $ do
             putStrLnM "-------------Original Below-----------------"
             mapM_ putStrLn unfiltered
             putStrLnM "------------- Filtered A + Symb below-----------------"