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 zero
Abstract: 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 to x.
function roll(uint x) public Sets the block number to x.
function assume(bool b) public Add the condition b to the assumption base for the current branch. This functions almost identically to require.
function deal(uint usr, uint amt) public Sets the eth balance of usr to amt. Note that if usr 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 slot loc of contract c to val.
function load(address c, bytes32 loc) public returns (bytes32 val) Reads the slot loc of contract c.
function sign(uint sk, bytes32 digest) public returns (uint8 v, bytes32 r, bytes32 s) Signs the digest using the private key sk. Note that signatures produced via hevm.sign will leak the private key.
function addr(uint sk) public returns (address addr) Derives an ethereum address from the private key sk. Note that hevm.addr(0) will fail with BadCheatCode as 0 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 to dapp test, for this reason all calls to ffi will fail unless the --ffi flag is passed.
function prank(address sender) public Sets msg.sender to the specified sender for the next call.