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.