The hevm project is an implementation of the Ethereum virtual machine (EVM) made specifically for symbolic execution, unit testing and debugging of smart contracts. It is developed by DappHub and integrates especially well with the dapp tool suite. The hevm command line program can symbolically execute smart contracts, run unit tests, interactively debug contracts while showing the Solidity source, or run arbitrary EVM code. Computations can be performed using local state set up in a dapp testing harness, or fetched on demand from live networks using rpc calls.
Note: some hevm commands (dapp-test) assume the use of the ds-test framework for Solidity unit tests and the dapp tool suite, while others (exec, symbolic, ...) are available as standalone commands.
hevm -- Ethereum evaluator
Usage: hevm [<options>] <command>
or: hevm <command> --help
Commands:
symbolic Execute symbolically, exploring all possible execution paths
exec Execute a given program with specified env & calldata
equivalence Prove equivalence between two programs using symbolic execution
dapp-test Run unit tests
bc-test Run an Ethereum Blockchain/GeneralState test
merkle-test Run a merkle test file and ensure the root matches
compliance Run Blockchain compliance report
emacs Emacs console
version Show hevm version
flatten Concat all dependencies for a given source file
rlp Decode a RLP encoded bytestring
strip-metadata Remove metadata from contract code bytestring
Esc: exit debuggera: step to starte: step to endn: step forwards by one instructionp: step backwards by one instruction0: choose the branch which does not jump1: choose the branch which does jumpN: step to the next source positionP: step previous source positionC-n: step to the next source position and don't enterCALLorCREATEC-p: step previous source position without enteringm: toggle memory viewDown: step to next entry in the callstack / Scroll memory pane\n" <>Up: step to previous entry in the callstack / Scroll memory pane\n" <>h: show key-binding help
Usage: hevm symbolic [--code TEXT] [--calldata TEXT] [--address ADDR]
[--caller ADDR] [--origin ADDR] [--coinbase ADDR]
[--value W256] [--nonce W256] [--gas W256] [--number W256]
[--timestamp W256] [--gaslimit W256] [--gasprice W256]
[--create] [--maxcodesize W256] [--difficulty W256]
[--chainid W256] [--rpc TEXT] [--block W256]
[--state STRING] [--cache STRING] [--json-file STRING]
[--dapp-root STRING] [--storage-model STORAGEMODEL]
[--sig TEXT] [--arg STRING]... [--debug] [--get-models]
[--show-tree] [--smttimeout INTEGER]
[--max-iterations INTEGER] [--solver TEXT] [--smtdebug]
[--assertions [WORD256]] [--ask-smt-iterations INTEGER]
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 W256 Nonce of origin
--gas W256 Tx: gas amount
--number W256 Block: number
--timestamp W256 Block: timestamp
--gaslimit W256 Tx: gas limit
--gasprice W256 Tx: gas price
--create Tx: creation
--maxcodesize W256 Block: max code size
--difficulty W256 Block: difficulty
--chainid W256 Env: chainId
--rpc TEXT Fetch state from a remote node
--block W256 Block state is be fetched from
--state STRING Path to state repository
--cache STRING Path to rpc cache repository
--json-file STRING Filename or path to dapp build output (default:
out/*.solc.json)
--dapp-root STRING Path to dapp project root directory (default: . )
--storage-model STORAGEMODEL
Select storage model: ConcreteS, SymbolicS (default)
or InitialS
--sig TEXT Signature of types to decode / encode
--arg STRING Values to encode
--debug Run interactively
--get-models Print example testcase for each execution path
--show-tree Print branches explored in tree view
--smttimeout INTEGER Timeout given to SMT solver in milliseconds (default:
60000)
--max-iterations INTEGER Number of times we may revisit a particular branching
point
--solver TEXT Used SMT solver: z3 (default) or cvc4
--smtdebug Print smt queries sent to the solver
--assertions [WORD256] Comma seperated list of solc panic codes to check for
(default: everything except arithmetic overflow)
--ask-smt-iterations INTEGER
Number of times we may revisit a particular branching
point before we consult the smt solver to check
reachability (default: 5)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 counterexmaples for arithmetic overflow (0x11) and user defined assertions (0x01):
hevm symbolic --code $CODE --assertions '[0x01, 0x11]'
--debug enters an interactive debugger where the user can navigate the full execution space.
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 take one of three forms, defaulting to SymbolicS unless --create is provided, in which case it defaults to InitialS:
SymbolicS: The default value of SLOAD is a symbolic value without further constraints. SLOAD and SSTORE can operate on symbolic locations.InitialS: The default value of SLOAD is zero. SLOAD and SSTORE can operate on symbolic locations.ConcreteS: Storage defaults to zero or fetched from an rpc node if--rpcis provided. SLOAD or SSTOREs on symbolic locations will result in a runtime error.
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 infitie 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.
Minimum required flags:
--code or (--rpc and --address).
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 W256] [--gas W256]
[--number W256] [--timestamp W256] [--gaslimit W256]
[--gasprice W256] [--create] [--maxcodesize W256]
[--difficulty W256] [--debug] [--state STRING] [--rpc TEXT]
[--block W256] [--json-file STRING]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 0xffDebug 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) --debugIf --state is provided, hevm will load and save state to the directory provided. Git is used as a storage model, with each hevm run creating a new commit. The directory provided must be a non empty git repository. After a run you can see the state diff by simply looking at the commit (for example git show HEAD).
mkdir mystate
cd mystate && git init && git commit --allow-empty -m "init" && cd ..
hevm exec --code 0x600160015500 --state mystate --gas 0xffffff
cd mystate && git show HEADUsage: hevm equivalence --code-a TEXT --code-b TEXT [--sig TEXT]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.
Usage: hevm dapp-test [--json-file STRING] [--dapp-root STRING] [--debug]
[--fuzz-runs INT] [--replay (TEXT,BYTESTRING)] [--depth INT]
[--rpc TEXT] [--verbose INT] [--coverage] [--state STRING]
[--match STRING] [--smttimeout INT] [--max-iterations INT]
[--solver STRING] [--cache STRING] [--cov-match STRING]
Run any ds-test testing functions. Run under the hood whenever dapp test or dapp debug is called. Testing functions prefixed with test will be executed concretely. If concrete test functions have been given arguments, they will be randomly instantiated and run --fuzz-runs number of times. If testing functions are prefixed with prove they will be symbolically executed. In --debug mode, property based tests will not be available unless given specific arguments using --replay.
The smttimeout, max-iterations and solver options have the same semantics as in hevm symbolic
These environment variables can be used to control block parameters:
| Variable | Default | Synopsis |
|---|---|---|
DAPP_TEST_ADDRESS |
0xb4c79daB8f259C7Aee6E5b2Aa729821864227e84 |
The address to deploy the test contract to |
DAPP_TEST_CALLER |
0x00a329c0648769a73afac7f9381e08fb43dbea72 |
The address to set msg.sender to when calling into the test contract |
DAPP_TEST_ORIGIN |
0x00a329c0648769a73afac7f9381e08fb43dbea72 |
The address to set tx.orgin to when calling into the test contract |
DAPP_TEST_GAS_CREATE |
0xffffffffffff |
The gas to provide when creating the testing contract |
DAPP_TEST_GAS_CALL |
0xffffffffffff |
The gas to provide to each call made to the testing contract |
DAPP_TEST_BALANCE |
0xffffffffffffffffffffffff |
The balance to provide to DAPP_TEST_ADDRESS |
DAPP_TEST_COINBASE |
0x0000000000000000000000000000000000000000 |
The coinbase address. Will be set to the coinbase for the block at DAPP_TEST_NUMBER if rpc is enabled |
DAPP_TEST_NUMBER |
0 |
The block number. Will be set to the latest block if rpc is enabled |
DAPP_TEST_TIMESTAMP |
0 |
The block timestamp. Will be set to the timestamp for the block at DAPP_TEST_NUMBER if rpc is enabled |
DAPP_TEST_GAS_LIMIT |
0 |
The block gas limit to use |
DAPP_TEST_GAS_PRICE |
0 |
The gas price to use |
DAPP_TEST_DIFFICULTY |
0 |
The block difficulty. Will be set to the difficulty for the the block at DAPP_TEST_NUMBER if rpc is enabled |
hevm is distributed as part of the Dapp tools suite.
If you can't or won't use Nix, the easiest way especially if you don't have GHC (the Haskell compiler) installed already, is to use Stack, which can take care of installing GHC for you. These commands should work:
$ curl -sSL https://get.haskellstack.org/ | sh
$ git clone https://github.com/dapphub/dapptools.git
$ cd dapptools/src/hevm && stack setup && stack install
Also, hevm is in Hackage so you can execute stack install hevm to get it up and running.
If you prefer to use your own installation of GHC and the basic Haskell package manager, Cabal, simply run:
$ git clone https://github.com/dapphub/dapptools.git
$ cd dapptools/src/hevm && cabal v2-update && cabal v2-configure && cabal v2-install
Note: If you are on macOS when building with Stack, you will first need to install the secp256k1 and libff libraries. These commands should be enough:
$ brew install automake
$ git clone https://github.com/bitcoin-core/secp256k1.git
$ cd secp256k1
$ ./autogen.sh
$ ./configure --enable-module-recovery # for generating secp256k1_recovery.h
$ make
$ sudo make install
$ cd .. && rm -rf secp256k1 # optional (cleanup)
$ brew install openssl
$ git clone https://github.com/scipr-lab/libff --recursive
$ cd libff
$ export LDFLAGS=-L/usr/local/opt/openssl/lib
$ export CPPFLAGS=-I/usr/local/opt/openssl/include
$ export CXXFLAGS=-I/usr/local/opt/openssl/include
$ ARGS="-DWITH_PROCPS=OFF -DOPENSSL_INCLUDE_DIR=/usr/local/opt/openssl/include/openssl -DCURVE=ALT_BN128"
$ sed -i '' 's/STATIC/SHARED/' libff/CMakeLists.txt
$ sed -i '' 's/STATIC/SHARED/' depends/CMakeLists.txt
$ mkdir build
$ cd build
$ CXXFLAGS="-fPIC $CXXFLAGS" OPENSSL_ROOT_DIR=/usr/local/opt/openssl cmake $ARGS ..
$ make && sudo make install
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 Hevm) at address 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D, which implements the following methods:
-
function warp(uint x) publicSets the block timestamp tox. -
function roll(uint x) publicSets the block number tox. -
function store(address c, bytes32 loc, bytes32 val) publicSets the slotlocof contractctoval. -
function load(address c, bytes32 loc) public returns (bytes32 val)Reads the slotlocof contractc. -
function sign(uint sk, bytes32 digest) public returns (uint8 v, bytes32 r, bytes32 s)Signs thedigestusing the private keysk. Note that signatures produced viahevm.signwill 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 withBadCheatCodeas0is 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 toffiwill fail unless the--ffiflag is passed.
You can find us in the DappHub chat at https://dapphub.chat/, especially the #dev channel.