Changing default maxIters to 1

CHANGELOG.md

@@ -9,6 +9,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Improved printing of results. Should be more intuitive to understand what hevm found.
 - More complete and precise array/mapping slot rewrite, along with a copySlice improvement
 - Use a let expression in copySlice to decrease expression size
+- Default max iterations is 1 now. `--max-iters -1` now signals no bound. This change is to match other
+  symbolic execution frameworks' default bound and to not go into an infinite loop by default when
+  there could be other, interesting and reachable bugs in the code
 
 ## Added
 - More POr and PAnd rules

cli/cli.hs

@@ -85,7 +85,7 @@ data Command w
       , showTree      :: w ::: Bool               <?> "Print branches explored in tree view"
       , showReachableTree :: w ::: Bool           <?> "Print only reachable branches explored in tree view"
       , smttimeout    :: w ::: Maybe Natural      <?> "Timeout given to SMT solver in seconds (default: 300)"
-      , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"
+      , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point. For no bound, set -1 (default: 1)"
       , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"
       , debug         :: w ::: Bool               <?> "Debug printing of internal behaviour"
@@ -106,7 +106,7 @@ data Command w
       , arg           :: w ::: [String]         <?> "Values to encode"
       , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"
       , smttimeout    :: w ::: Maybe Natural    <?> "Timeout given to SMT solver in seconds (default: 300)"
-      , maxIterations :: w ::: Maybe Integer    <?> "Number of times we may revisit a particular branching point"
+      , maxIterations :: w ::: Maybe Integer    <?> "Number of times we may revisit a particular branching point. For no bound, set -1 (default: 1)"
       , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
       , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"
       , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"
@@ -161,7 +161,7 @@ data Command w
       , 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)"
-      , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"
+      , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point. For no bound, set -1 (default: 1)"
       , loopDetectionHeuristic :: w ::: LoopHeuristic   <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
       , abstractArithmetic    :: w ::: Bool             <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"
       , abstractMemory    :: w ::: Bool                      <?> "Use abstraction-refinement for Memory. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"
@@ -241,7 +241,7 @@ equivalence cmd = do
   let bytecodeA = hexByteString "--code" . strip0x $ cmd.codeA
       bytecodeB = hexByteString "--code" . strip0x $ cmd.codeB
       veriOpts = VeriOpts { simp = True
-                          , maxIter = cmd.maxIterations
+                          , maxIter = parseMaxIters cmd.maxIterations
                           , askSmtIters = cmd.askSmtIterations
                           , loopHeuristic = cmd.loopDetectionHeuristic
                           , rpcInfo = Nothing
@@ -295,6 +295,10 @@ getProjectType cmd = fromMaybe Foundry cmd.projectType
 getRoot :: Command Options.Unwrapped -> IO FilePath
 getRoot cmd = maybe getCurrentDirectory makeAbsolute (cmd.root)
 
+parseMaxIters :: Maybe Integer -> Maybe Integer
+parseMaxIters i = if num < 0 then Nothing else Just num
+  where
+    num = (fromMaybe (1::Integer) i)
 
 -- | Builds a buffer representing calldata based on the given cli arguments
 buildCalldata :: Command Options.Unwrapped -> IO (Expr Buf, [Prop])
@@ -325,13 +329,13 @@ assert cmd = do
   let solverCount = fromMaybe cores cmd.numSolvers
   solver <- liftIO $ getSolver cmd
   withSolvers solver solverCount cmd.smttimeout $ \solvers -> do
-    let opts = VeriOpts { simp = True
-                        , maxIter = cmd.maxIterations
+    let veriOpts = VeriOpts { simp = True
+                        , maxIter = parseMaxIters cmd.maxIterations
                         , askSmtIters = cmd.askSmtIterations
                         , loopHeuristic = cmd.loopDetectionHeuristic
                         , rpcInfo = rpcinfo
     }
-    (expr, res) <- verify solvers opts preState (Just $ checkAssertions errCodes)
+    (expr, res) <- verify solvers veriOpts preState (Just $ checkAssertions errCodes)
     case res of
       [Qed _] -> do
         liftIO $ putStrLn "\nQED: No reachable property violations discovered\n"
@@ -607,7 +611,7 @@ unitTestOptions cmd solvers buildOutput = do
     , rpcInfo = case cmd.rpc of
          Just url -> Just (block', url)
          Nothing  -> Nothing
-    , maxIter = cmd.maxIterations
+    , maxIter = parseMaxIters cmd.maxIterations
     , askSmtIters = cmd.askSmtIterations
     , smtTimeout = cmd.smttimeout
     , solver = cmd.solver

doc/src/equivalence.md

@@ -19,7 +19,7 @@ Available options:
   --calldata TEXT          Tx: calldata
   --smttimeout NATURAL     Timeout given to SMT solver in seconds (default: 300)
   --max-iterations INTEGER Number of times we may revisit a particular branching
-                           point
+                           point. Default is 1. Setting to -1 allows infinite looping
   --solver TEXT            Used SMT solver: z3 (default), cvc5, or bitwuzla
   --smtoutput              Print verbose smt output
   --smtdebug               Print smt queries sent to the solver

doc/src/symbolic.md

@@ -54,7 +54,7 @@ Available options:
   --show-reachable-tree    Print only reachable branches explored in tree view
   --smttimeout NATURAL     Timeout given to SMT solver in seconds (default: 300)
   --max-iterations INTEGER Number of times we may revisit a particular branching
-                           point
+                           point. Default is 1. Setting to -1 allows infinite looping
   --solver TEXT            Used SMT solver: z3 (default), cvc5, or bitwuzla
   --smtdebug               Print smt queries sent to the solver
   --assertions [WORD256]   Comma separated list of solc panic codes to check for

doc/src/test.md

@@ -32,7 +32,7 @@ Available options:
                            your machine)
   --smttimeout NATURAL     Timeout given to SMT solver in seconds (default: 300)
   --max-iterations INTEGER Number of times we may revisit a particular branching
-                           point
+                           point. Default is 1. Setting to -1 allows infinite looping
   --loop-detection-heuristic LOOPHEURISTIC
                            Which heuristic should be used to determine if we are
                            in a loop: StackBased (default) or Naive

src/EVM/Format.hs

@@ -464,7 +464,7 @@ formatPartial = \case
       , indent 2 $ T.unlines . fmap formatSomeExpr $ args
       ]
     ]
-  MaxIterationsReached pc addr -> "Max Iterations Reached in contract: " <> formatAddr addr <> " pc: " <> pack (show pc)
+  MaxIterationsReached pc addr -> "Max Iterations Reached in contract: " <> formatAddr addr <> " pc: " <> pack (show pc) <> " To increase the maximum, set a fixed large (or negative) value for `--max-iterations` on the command line"
   JumpIntoSymbolicCode pc idx -> "Encountered a jump into a potentially symbolic code region while executing initcode. pc: " <> pack (show pc) <> " jump dst: " <> pack (show idx)
 
 formatSomeExpr :: SomeExpr -> Text