Merge pull request #674 from ethereum/limit-num-branches

Limiting the branching factor and the depth of branching

Author: msooseth

CHANGELOG.md

@@ -46,6 +46,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   print some warnings related to zero-address dereference and to print `hemv test`'s
   output in case of failure
 - Simple test cases for the CLI
+- Allow limiting the branch depth and width limitation via --max-depth and --max-width
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value

cli/cli.hs

@@ -76,7 +76,6 @@ data CommonOptions = CommonOptions
   { askSmtIterations ::Integer
   , loopDetectionHeuristic ::LoopHeuristic
   , noDecompose   ::Bool
-  , maxBranch     ::Int
   , solver        ::Text
   , debug         ::Bool
   , calldata      ::Maybe ByteString
@@ -92,6 +91,8 @@ data CommonOptions = CommonOptions
   , maxIterations ::Integer
   , promiseNoReent::Bool
   , maxBufSize    ::Int
+  , maxWidth      ::Int
+  , maxDepth      ::Maybe Int
   }
 
 commonOptions :: Parser CommonOptions
@@ -101,7 +102,6 @@ commonOptions = CommonOptions
   <*> option auto (long "loop-detection-heuristic" <> showDefault <> value StackBased <>
     help "Which heuristic should be used to determine if we are in a loop: StackBased or Naive")
   <*> (switch $ long "no-decompose"         <> help "Don't decompose storage slots into separate arrays")
-  <*> (option auto $ long "max-branch"      <> showDefault <> value 100 <> help "Max number of branches to explore when encountering a symbolic value")
   <*> (strOption $ long "solver"            <> value "z3" <> help "Used SMT solver: z3, cvc5, or bitwuzla")
   <*> (switch $ long "debug"                <> help "Debug printing of internal behaviour, and dump internal expressions")
   <*> (optional $ strOption $ long "calldata" <> help "Tx: calldata")
@@ -117,6 +117,8 @@ commonOptions = CommonOptions
   <*> (option auto $ long "max-iterations"  <> showDefault <> value 5 <> help "Number of times we may revisit a particular branching point. For no bound, set -1")
   <*> (switch $ long "promise-no-reent"     <> help "Promise no reentrancy is possible into the contract(s) being examined")
   <*> (option auto $ long "max-buf-size"    <> value 64 <> help "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)")
+  <*> (option auto $ long "max-width"      <> showDefault <> value 100 <> help "Max number of concrete values to explore when encountering a symbolic value. This is a form of branch width limitation per symbolic value")
+  <*> (optional $ option auto $ long "max-depth" <> help "Limit maximum depth of branching during exploration (default: unlimited)")
 
 data CommonExecOptions = CommonExecOptions
   { address       ::Maybe Addr
@@ -346,9 +348,10 @@ main = do
         , numCexFuzz = cOpts.numCexFuzz
         , dumpTrace = cOpts.trace
         , decomposeStorage = Prelude.not cOpts.noDecompose
-        , maxBranch = cOpts.maxBranch
         , promiseNoReent = cOpts.promiseNoReent
         , maxBufSize = cOpts.maxBufSize
+        , maxWidth = cOpts.maxWidth
+        , maxDepth = cOpts.maxDepth
         , verb = cOpts.verb
         } }
 

doc/src/common-options.md

@@ -48,3 +48,25 @@ Loops in the code cause a challenge to symbolic execution framework. In order
 to not run indefinitely, hevm will only explore a certain number of iterations
 of a loop before consideing abandoning the exploration of that branch. This
 number can be set via the `--ask-smt-iterations` flag.
+
+## Maximum Branch Width Limit, ``--max-width``
+
+Limits the number of potential concrete values that are explored in case a
+symbolic value is encountered, thus limiting branching width. For example, if a
+JUMP instruction is called with a symbolic expression, the system will explore
+all possible valid jump destinations, which may be too many. This option limits
+the branching factor in these cases. Default is 100.
+
+If there are more than the given maximum number of possible values, the system
+will try to deal with the symbolic value, if possible, e.g. via
+over-approximation. If over-approximation is not possible, symbolic execution
+will terminate with a `Partial` node, which is often displayed as "Unexpected
+Symbolic Arguments to Opcode" to the user when e.g. running `hevm test`.
+
+## Maximum Branch Depth Limit, ``--max-depth``
+
+Limits the number of branching points on all paths during symbolic execution.
+This is helpful to prevent the exploration from running for too long. Useful in
+scenarios where you use e.g. both symbolic execution and fuzzing, and don't
+want the symbolic execution to run for too long. It will often read to
+WARNING-s related to `Branches too deep at program counter`.