Common options
The subcommands of hevm present a number of common options. Here, we document these options in detail.
Maximum Buffer Size, --max-buf-size
The buffers in hevm are limited to a maximum size of 2^N bytes, where N is by
default 64, but adjustable via the --max-buf-size
flag. This helps to prevent
the system from creating buffers that are too large and would exceed the gas
limit. Limiting this value further to e.g. 20 can help to force the system to
generate counterexamples that are easier to examine and understand.
Choice of Solver, --solver
hevm can use any SMT solver that supports the AUFBV theory and incremental solving. Currently, z3, cvc5, and bitwuzla's interfaces are implemented. While any of these solvers work, we recommend using bitwuzla as it is in general extremely fast, almost always significantly faster than e.g. z3.
Number of Solvers, --num-solvers
hevm can run multiple solvers in parallel and will run as many solvers as it
detects the number of CPU cores on the machine. However, in some cases, that
may lead to memory outs, in case the solver happens to get queries that are
memory-intensive. In these cases, the number of solvers can be limited to a a
specific (low) number via the --num-solvers
flag.
Promising no reentrancy, --promise-no-reent
hevm can be instructed to assume that no reentrancy will occur during the
execution of the contract. This is currently neccessary to fully explore
certain contracts. This is because value transfer is usually done via a CALL
,
which can be reentrant. By promising no reentrancy, the system can assume that
no reentrancy will occur and can explore the contract more fully.
Timeout for SMT queries, --smttimeout
Some queries take too long. With a timeout, we ensure that hevm eventually
terminates. However, endstates where the timeout was reached are considered
inditerminate, and will lead to a WARNING
in the output. It is worthwhile
trying to switch to a different SMT solver such as bitwuzla, or increasing the
timeout if this happens.
Loop Iteration Limit, --ask-smt-iterations
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
.