Overview
The hevm
project is an implementation of the Ethereum Virtual Machine (EVM) focused on symbolic
analysis of evm bytecode. It can:
- symbolically execute a smart contract and find reachable assertion violations
- prove equivalence of two different bytecode objects
- execute symbolic solidity tests written using
ds-test
(a.k.a "foundry tests") - fetch remote state via rpc
- automatically create test cases
It was originally developed as part of the dapptools project, and was forked to this repo by the formal methods team at the Ethereum Foundation in August 2022.
hevm symbolic
Usage: hevm symbolic [--code TEXT] [--calldata TEXT] [--address ADDR]
[--caller ADDR] [--origin ADDR] [--coinbase ADDR]
[--value W256] [--nonce WORD64] [--gas WORD64]
[--number W256] [--timestamp W256] [--basefee W256]
[--priority-fee W256] [--gaslimit WORD64] [--gasprice W256]
[--create] [--maxcodesize W256] [--prev-randao W256]
[--chainid W256] [--rpc TEXT] [--block W256]
[--root STRING] [--project-type PROJECTTYPE]
[--initial-storage INITIALSTORAGE] [--sig TEXT]
[--arg STRING]... [--get-models] [--show-tree]
[--show-reachable-tree] [--smttimeout NATURAL]
[--max-iterations INTEGER] [--solver TEXT] [--smtdebug]
[--assertions [WORD256]] [--ask-smt-iterations INTEGER]
[--num-solvers NATURAL]
[--loop-detection-heuristic LOOPHEURISTIC]
Available options:
-h,--help Show this help text
--code TEXT Program bytecode
--calldata TEXT Tx: calldata
--address ADDR Tx: address
--caller ADDR Tx: caller
--origin ADDR Tx: origin
--coinbase ADDR Block: coinbase
--value W256 Tx: Eth amount
--nonce WORD64 Nonce of origin
--gas WORD64 Tx: gas amount
--number W256 Block: number
--timestamp W256 Block: timestamp
--basefee W256 Block: base fee
--priority-fee W256 Tx: priority fee
--gaslimit WORD64 Tx: gas limit
--gasprice W256 Tx: gas price
--create Tx: creation
--maxcodesize W256 Block: max code size
--prev-randao W256 Block: prevRandao
--chainid W256 Env: chainId
--rpc TEXT Fetch state from a remote node
--block W256 Block state is be fetched from
--root STRING Path to project root directory (default: . )
--project-type PROJECTTYPE
Is this a Foundry or DappTools project (default:
Foundry)
--initial-storage INITIALSTORAGE
Starting state for storage: Empty, Abstract (default
Abstract)
--sig TEXT Signature of types to decode / encode
--arg STRING Values to encode
--get-models Print example testcase for each execution path
--show-tree Print branches explored in tree view
--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
--solver TEXT Used SMT solver: z3 (default) or cvc5
--smtdebug Print smt queries sent to the solver
--assertions [WORD256] Comma separated list of solc panic codes to check for
(default: user defined assertion violations only)
--ask-smt-iterations INTEGER
Number of times we may revisit a particular branching
point before we consult the smt solver to check
reachability (default: 1) (default: 1)
--num-solvers NATURAL Number of solver instances to use (default: number of
cpu cores)
--loop-detection-heuristic LOOPHEURISTIC
Which heuristic should be used to determine if we are
in a loop: StackBased (default) or Naive
(default: StackBased)
Run a symbolic execution against the given parameters, searching for assertion violations.
Counterexamples will be returned for any reachable assertion violations. Where an assertion
violation is defined as either an execution of the invalid opcode (0xfe
), or a revert with a
message of the form abi.encodeWithSelector('Panic(uint256)', errCode)
with errCode
being one of
the predefined solc assertion codes defined
here.
By default hevm ignores assertion violations that result from arithmetic overflow (Panic(0x11)
),
although this behaviour can be customised via the --assertions
flag. For example, the following
will return counterexamples for arithmetic overflow (0x11
) and user defined assertions (0x01
):
hevm symbolic --code $CODE --assertions '[0x01, 0x11]'
The default value for calldata
and caller
are symbolic values, but can be specialized to concrete functions with their corresponding flags.
One can also specialize specific arguments to a function signature, while leaving others abstract.
If --sig
is given, calldata is assumed to be of the form suggested by the function signature. With this flag, specific arguments can be instantiated to concrete values via the --arg
flag.
This is best illustrated through a few examples:
Calldata specialized to the bytestring 0xa9059cbb
followed by 64 symbolic bytes:
hevm symbolic --sig "transfer(address,uint256)" --code $(<dstoken.bin-runtime)
Calldata specialized to the bytestring 0xa9059cbb0000000000000000000000007cfa93148b0b13d88c1dce8880bd4e175fb0dedf
followed by 32 symbolic bytes.
hevm symbolic --sig "transfer(address,uint256)" --arg 0x7cFA93148B0B13d88c1DcE8880bd4e175fb0DeDF --code $(<dstoken.bin-runtime)
Calldata specialized to the bytestring 0xa9059cbb
followed by 32 symbolic bytes, followed by the bytestring 0000000000000000000000000000000000000000000000000000000000000000
:
hevm symbolic --sig "transfer(address,uint256)" --arg "<symbolic>" --arg 0 --code $(<dstoken.bin-runtime)
If the --get-models
flag is given, example input values will be returned for each possible execution path.
This can be useful for automatic test case generation.
The default timeout for SMT queries is no timeout. If your program is taking longer than a couple of minutes to run,
you can experiment with configuring the timeout to somewhere around 10s by doing --smttimeout 10000
Storage can be initialized in two ways:
Empty
: all storage slots for all contracts are initialized to zeroAbstract
: all storage slots are initialized as unconstrained abstract values
hevm
uses an eager approach for symbolic execution, meaning that it will first attempt to explore
all branches in the program (without querying the smt solver to check if they are reachable or not).
Once the full execution tree has been explored, the postcondition is checked against all leaves, and
the solver is invoked to check reachability for branches where a postcondition violation could
occur. While our tests have shown this approach to be significantly faster, when applied without
limits it would always result in infinite exploration of code involving loops, so after some
predefined number of iterations (controlled by the --ask-smt-iterations
flag), the solver will be
invoked to check whether a given loop branch is reachable. In cases where the number of loop
iterations is known in advance, you may be able to speed up execution by setting this flag to an
appropriate value.
hevm equivalence
Usage: hevm equivalence --code-a TEXT --code-b TEXT [--sig TEXT]
[--arg STRING]... [--calldata TEXT]
[--smttimeout NATURAL] [--max-iterations INTEGER]
[--solver TEXT] [--smtoutput] [--smtdebug]
[--ask-smt-iterations INTEGER]
[--loop-detection-heuristic LOOPHEURISTIC]
Available options:
-h,--help Show this help text
--code-a TEXT Bytecode of the first program
--code-b TEXT Bytecode of the second program
--sig TEXT Signature of types to decode / encode
--arg STRING Values to encode
--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
--solver TEXT Used SMT solver: z3 (default) or cvc5
--smtoutput Print verbose smt output
--smtdebug Print smt queries sent to the solver
--ask-smt-iterations INTEGER
Number of times we may revisit a particular branching
point before we consult the smt solver to check
reachability (default: 1) (default: 1)
--loop-detection-heuristic LOOPHEURISTIC
Which heuristic should be used to determine if we are
in a loop: StackBased (default) or Naive
(default: StackBased)
Symbolically execute both the code given in --code-a
and --code-b
and try to prove equivalence between their outputs and storages.
If --sig
is given, calldata is assumed to take the form of the function given.
If left out, calldata is a fully abstract buffer of at most 256 bytes.
hevm exec
Run an EVM computation using specified parameters, using an interactive debugger when --debug
flag is given.
Usage: hevm exec [--code TEXT] [--calldata TEXT] [--address ADDR]
[--caller ADDR] [--origin ADDR] [--coinbase ADDR]
[--value W256] [--nonce WORD64] [--gas WORD64] [--number W256]
[--timestamp W256] [--basefee W256] [--priority-fee W256]
[--gaslimit WORD64] [--gasprice W256] [--create]
[--maxcodesize W256] [--prev-randao W256] [--chainid W256]
[--trace] [--rpc TEXT] [--block W256] [--root STRING]
[--project-type PROJECTTYPE]
Available options:
-h,--help Show this help text
--code TEXT Program bytecode
--calldata TEXT Tx: calldata
--address ADDR Tx: address
--caller ADDR Tx: caller
--origin ADDR Tx: origin
--coinbase ADDR Block: coinbase
--value W256 Tx: Eth amount
--nonce WORD64 Nonce of origin
--gas WORD64 Tx: gas amount
--number W256 Block: number
--timestamp W256 Block: timestamp
--basefee W256 Block: base fee
--priority-fee W256 Tx: priority fee
--gaslimit WORD64 Tx: gas limit
--gasprice W256 Tx: gas price
--create Tx: creation
--maxcodesize W256 Block: max code size
--prev-randao W256 Block: prevRandao
--chainid W256 Env: chainId
--trace Dump trace
--rpc TEXT Fetch state from a remote node
--block W256 Block state is be fetched from
--root STRING Path to project root directory (default: . )
--project-type PROJECTTYPE
Is this a Foundry or DappTools project (default:
Foundry)
Minimum required flags:
--code
or (--rpc
and --address
).
If the execution returns an output, it will be written to stdout.
Exit code indicates whether the execution was successful or errored/reverted.
Simple example usage:
hevm exec --code 0x647175696e6550383480393834f3 --gas 0xff
Execute a mainnet transaction (older transactions require archive node):
export ETH_RPC_URL=https://mainnet.infura.io/v3/YOUR_API_KEY_HERE
export TXHASH=0xd2235b9554e51e8ff5b3de62039d5ab6e591164b593d892e42b2ffe0e3e4e426
hevm exec --caller $(seth tx $TXHASH from) --address $(seth tx $TXHASH to) --calldata $(seth tx $TXHASH input) --rpc $ETH_RPC_URL --block $(($(seth tx $TXHASH blockNumber)-1)) --gas $(seth tx $TXHASH gas)
dapp-test
controlling the unit testing environment
Cheat codes
Since Hevm is an EVM implementation mainly dedicated to testing and exploration, it features a set of cheat codes
which can manipulate the environment in which the execution is run.
These can be accessed by calling into a contract (typically called Vm
) at address 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D
, which implements the following methods:
-
function warp(uint x) public
Sets the block timestamp tox
. -
function roll(uint x) public
Sets the block number tox
. -
function assume(bool b) public
Add the conditionb
to the assumption base for the current branch. This functions almost identically torequire
. -
function deal(uint usr, uint amt) public
Sets the eth balance ofusr
toamt
. Note that ifusr
is a symbolic address, then it must be the address of a contract that has already been deployed. This restriction is in place to ensure soundness of our symbolic address encoding with respect to potential aliasing of symbolic addresses. -
function store(address c, bytes32 loc, bytes32 val) public
Sets the slotloc
of contractc
toval
. -
function load(address c, bytes32 loc) public returns (bytes32 val)
Reads the slotloc
of contractc
. -
function sign(uint sk, bytes32 digest) public returns (uint8 v, bytes32 r, bytes32 s)
Signs thedigest
using the private keysk
. Note that signatures produced viahevm.sign
will leak the private key. -
function addr(uint sk) public returns (address addr)
Derives an ethereum address from the private keysk
. Note thathevm.addr(0)
will fail withBadCheatCode
as0
is an invalid ECDSA private key. -
function ffi(string[] calldata) external returns (bytes memory)
Executes the arguments as a command in the system shell and returns stdout. Expects abi encoded values to be returned from the shell or an error will be thrown. Note that this cheatcode means test authors can execute arbitrary code on user machines as part of a call todapp test
, for this reason all calls toffi
will fail unless the--ffi
flag is passed. -
function prank(address sender) public
Setsmsg.sender
to the specifiedsender
for the next call.