Getting Started
The hevm project is an implementation of the Ethereum Virtual Machine (EVM) focused on symbolic analysis of EVM bytecode. This essentially means that hevm can try out all execution possibilities of your contract and see it can somehow violate some assertions you have. These assertions can be e.g. the total number of tokens must always be X, some value must never be greater than Y, some value must never overflow, etc.
In some sense, hevm is similar to a fuzzer, but instead of only trying with random values to trigger faults, it instead computes whether a fault is possible. If it is possible, it gives an example call to trigger the fault, and if it isn't possible, it mathematically proves it so, and tells the user the contract is safe. Note that while great pains have gone into making sure hevm's results can be trusted, there can always be bugs in hevm or the libraries and tools it uses.
Hevm can not only be used to find bugs in programs, but can also help to make sure that two programs behave equivalently from the outside. This may be advantageous when one may be more efficient (use less gas) to execute, but harder to reason about. This can be done via (equivalence checking)[#equivalence-checking] where hevm either proves that the behaviour of the two bytecodes is the same, or gives inputs where they differ.
Practical Scenario
Let's say we have a function that allows transfer of money, but no balance can be larger than or equal to 100. Let's see the contract and its associated check:
pragma solidity ^0.8.19;
import "ds-test/test.sol";
contract MyContract is DSTest {
mapping (address => uint) balances;
function prove_add_value(address recv, uint amt) public {
require(balances[recv] < 100);
if (balances[recv] + amt > 100) {
revert();
}
balances[recv] += amt;
assert(balances[recv] < 100);
}
}
Notice that this function has a bug: the require
and the assert
both check
for <
, but the if
checks for >
, which should instead be >=
. Let's see
if hevm
can find this bug. In order to do that, we have to prepend the
function name with prove_
, which we did.
Building
We now need a copy of hevm (see
releases) and the SMT solver z3,
which can be installed e.g. with apt-get
on ubuntu/debian or homebrew
on Mac,
and a copy of Foundry:
$ sudo apt-get install z3 # install z3
$ curl -L https://foundry.paradigm.xyz | bash # install foundryup
$ foundryup # install forge and other foundry binaries
$ mkdir mytest && cd mytest
$ wget https://github.com/ethereum/hevm/releases/download/release/0.53.0/hevm-x86_64-linux
$ chmod +x ./hevm-x86_64-linux
$ forge init .
$ cat <<EOF > src/contract.sol
pragma solidity ^0.8.19;
import "ds-test/test.sol";
contract MyContract is DSTest {
mapping (address => uint) balances;
function prove_add_value(address recv, uint amt) public {
require(balances[recv] < 100);
if (balances[recv] + amt > 100) {
revert();
}
balances[recv] += amt;
assert(balances[recv] < 100);
}
}
EOF
$ forge build
[⠊] Compiling...
[⠒] Compiling 1 files with 0.8.19
[⠢] Solc 0.8.19 finished in 14.27ms
Compiler run successful!
Finding the Bug
Now let's run hevm
to see if it finds the bug:
$ hevm test --solver z3
Running 1 tests for src/contract.sol:MyContract
[FAIL] prove_add_value(address,uint256)
Counterexample:
result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
calldata: prove_add_value(0x0000000000000000000000000000000000000000,100)
Fixing the Bug
This counterexample tells us that when sending exactly 100 to an empty account, the new
balance will violate the < 100
assumption. Let's fix this bug, the new prove_add_value
should now say:
function prove_add_value(address recv, uint amt) public {
require(balances[recv] < 100);
if (balances[recv] + amt >= 100) {
revert();
}
balances[recv] += amt;
assert(balances[recv] < 100);
}
Let's re-build with forge and check with hevm once again:
$ forge build
[⠰] Compiling...
[⠔] Compiling 1 files with 0.8.19
[⠒] Solc 0.8.19 finished in 985.32ms
Compiler run successful!
$ hevm test --solver z3
Running 1 tests for src/contract.sol:MyContract
[PASS] prove_add_value(address,uint256)
We now get a PASS
. Notice that this doesn't only mean that hevm couldn't find
a bug within a given time frame. Instead, it means that there is surely no call
to prove_add_value
such that our assertion can be violated. However, it does
not check for things that it was not asked to check for. In particular, it
does not check that e.g. the sender's balance is decremented. There is no such
test and so this omission is not detected.
Capabilities
- Symbolic execution of solidity tests written using
ds-test
(a.k.a "foundry tests"). This allows one to find all potential failure modes of a function. - Fetch remote state via RPC so your tests can be rooted in the real-world, calling out to other, existing contracts, with existing state and already deloyed bytecode.
- Prove equivalence of two different bytecode objects such as two functions or even entire contracts.
History
Hevm was originally developed as part of the dapptools project, and was forked to this repo by the Formal Verification team at the Ethereum Foundation in August 2022.
Quick Installation Guide
To fastest way to start using hevm is to install Foundry, e.g. via
curl -L https://foundry.paradigm.xyz | bash
Next, you need to have either Z3 or CVC5 installed. Often, these can be installed via:
$ sudo apt-get install z3
or similar. If you installed CVC5 instead, you will need to pass the flag "--solver cvc5" to "hevm test" later.
Finally, download the static hevm binary from the github repository for your platform and put it in your path so it can be executed via typing "hevm".
How to Check if it Works
Once you have the above, you can go to the root of your forge-based project and build it:
$ forge build
[⠒] Compiling...
[⠆] Compiling 34 files with 0.8.19
[⠔] Solc 0.8.19 finished in 2.12s
Compiler run successful.
Then run hevm on all functions prefixed with prove_
as such:
$ hevm test
Checking 1 function(s) in contract src/contract-pass.sol:MyContract
[RUNNING] prove_pass(address,uint256)
[PASS] prove_pass(address,uint256)
See ds-test Tutorial for details.
Note that Foundry provides the solidity compiler, hence there is no need to install solidity separately.
When to use Symbolic Execution
In the cryptocurrency world, it is exceedingly easy to lose a lot of assets due to bugs. While fuzz testing can help find potential issues with digital contracts, it is a tool that can only execute the program concretely, one execution at a time. In contrast, Symbolic Execution can execute all potential values in a decision path "in one go", creating a symbolic expression out of a path, and checking whether it can trigger a fault. Hence, Symbolic Execution tends to be more efficient at finding bugs than fuzzing when the bugs are rare, or explicitly (i.e. maliciously) hidden. Symbolic Execution can also prove that no postcondition can be violated, increasing the overall confidence in the contract. Note, however, that Symbolic Execution does not automatically generate postconditions for well-known bug classes like static code analysis tools do. Instead, these postconditions, and their sometimes associated preconditions, need to be explicitly written.
Fuzzing versus Symbolic Execution
Fuzzing tests usually have a set of (sometimes implicit) pre- and postconditions, but the actual action (e.g. function call) is performed by an external entity, the fuzzer. For C/C++ fuzzing, the implicit postcondition is often e.g. that the system does not throw a segmentation fault. For EVM bytecode, postconditions need to be explicit. Let's see an example:
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
import "ds-test/test.sol";
contract MyContract is DSTest {
uint balance;
function test_overflow(uint amt) public {
unchecked {
balance += amt;
}
assert(balance >= amt);
}
}
This function is easy to break by picking an amt
that overflows balance
,
so that the postcondition balance > amt
will not hold. A
fuzzer finds this kind of bug very
easily. However, fuzzers have trouble finding bugs that are either specifically
hidden (e.g. by a malicious developer), or that have a complicated code path
towards them. Let's see a simple one:
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
import "ds-test/test.sol";
contract MyContract is DSTest {
uint balance;
function prove_multiply(uint amt, uint amt2) public {
require(amt != 1);
require(amt2 != 1);
require(amt < amt2);
uint tmp;
tmp = amt * amt2;
if (tmp == 119274257) balance = 1337;
else balance += tmp;
assert(balance >= tmp);
}
}
Calling this contract with amt = 9479
and amt2 = 12583
will set the balance
to 1337 which is less than amt*amt2
, breaking the postcondition. However, a
fuzzer, e.g. Echidna will likely not find
those numbers, because uint
has a potential range of 2**256
and so it'd be
looking for a needle in a haystack, when looking randomly. Here's how to run
Echidna on the multiplication test:
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract MyContract {
// the rest is the same
}
Then run:
echidna --test-mode assertion src/multiply-test.sol
Echidna will terminate after 50k runs, with all tests passing. Notice that the difference here, compared to the previous example, is that the overflow example has many different inputs that can break the postcondition, whereas here only one can.
Hevm finds the bug in both of these functions. This is because hevm (and symbolic execution frameworks in general) try to find the bug via proof-directed search rather than using random inputs. In hevm, we try to prove that there are no inputs to the test case such that given the preconditions, the postconditions can be broken. While trying to construct this mathematical proof, hevm finds a countereexample, an input that breaks the postconditions:
$ hevm test
Checking 1 function(s) in contract src/multiply-test.sol:MyContract
[RUNNING] prove_multiply(uint256,uint256)
[FAIL] prove_multiply(uint256,uint256)
Counterexample:
result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
calldata: prove_multiply(9479,12583)
Checking 1 function(s) in contract src/overflow-test.sol:MyContract
[RUNNING] prove_overflow(uint256)
[FAIL] prove_overflow(uint256)
Counterexample:
result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
calldata: prove_overflow(00000000000000000000000000000000000000000000000100000000000000000182dad8c17bd5e89e8043a08ada90a6d5efdee4425f85cb863109783e158ba4fba908a0e6fae6c6b51002)
Similarities and Differences to Other Tools
Fuzzers are exceedingly fast and efficient when there are many potential faults with a function/contract, or if the faults are of a type that's easy to search for (e.g. off-by-one). However, they rarely, if ever, find cases where the bug is hidden deep in the branch logic, or needs very specific input parameters. Hence, it is best to use fuzzers at first to find easy-to-find bugs, as fuzzers are very efficient at that. Then, once the tests pass the fuzzer, it is recommended to use a symbolic execution engine such as hevm.
hevm is similar to Halmos and Kontrol in its approach. However, it is quite different from static code analysis tools such as Oyente, Slither, and Mythril. While these 3 tools typically use some form of symbolic execution to try to validate their results, their main method of operation is not via symbolic execution, and they can, and do, report false positives.
Notice that static code analysis tools can find bugs that the author(s) didn't write a test case for, as they typically have a (large) set of preconfigured test-cases that they can report on, if they can find a way to violate them. Hence, it may be valuable to run static analysis tools alongside symbolic execution tools such as hevm.
Finally, SMTChecker may also be interesting to run alongside hevm. SMTChecker is very different from both approaches detailed above. While SMTChecker is capable of reliably finding both reentrancy and loop-related bugs, the tools above can only do so on a best effort basis. Hevm often reports a warning of incompleteness for such problems, while static code analysis tools either report potential positives or may even not discover them at all.
Tool | Approach | Primary Method | Notes |
---|---|---|---|
hevm | Symbolic analysis of EVM bytecode | Symbolic execution | Focuses on exploring all execution possibilities, identifying potential assertion violations, and optimizing gas usage. Can prove equivalence between bytecodes. |
Halmos | Similar to hevm | Not specified | Approach similar to hevm, but the document does not detail specific methodologies or differences. |
Kontrol | Similar to hevm | Not specified | Approach similar to hevm, with a focus presumably on symbolic analysis as well, but further details are not provided in the document. |
Oyente | Static code analysis | Partial symbolic execution | Uses symbolic execution to validate results but primarily relies on static analysis. Can report false positives. |
Slither | Static code analysis | Partial symbolic execution | Similar to Oyente, uses static analysis as its main method, complemented by symbolic execution for validation. Known for reporting false positives. |
Mythril | Static code analysis | Partial symbolic execution | Combines static code analysis with symbolic execution for result validation. Like Oyente and Slither, can report false positives. |
SMTChecker | Different from both hevm and static code analysis tools | SMT solving | Capable of finding reentrancy and loop-related bugs reliably, which other tools might miss or report incompletely. Offers a distinct approach from symbolic execution. |
ds-test Tutorial
Test cases must be prepended with prove_
and the testing contract must
inherit from Test
from Forge's standard test
library. First, import Test:
import {Test} from "forge-std/Test.sol";
and then inherit from it via ... is Test
. This allows hevm to discover the test cases it needs to run. Like so:
pragma solidity ^0.8.19;
import {Test} from "forge-std/Test.sol";
contract BadVaultTest is Test {
function prove_mytest() {
// environment setup, preconditions
// call(s) to test
// postcondition checks
}
}
Once you have written such a test case, you need to compile with forge build
(see forge documentation for more
details) and then:
$ hevm test
Checking 1 function(s) in contract src/badvault-test.sol:BadVault
[RUNNING] prove_mytest(uint256)
[PASS] prove_mytest(uint256)
Here, hevm discovered the test case, and automatically checked it for violations.
Setting Up Tests
Tests usually need to set up the environment in a particular way, such as contract address, storage, etc. This can be done via Cheat Codes that can change the address of the caller, set block number, etc. See Cheat Codes below for a range of cheat codes supported. Cheat Codes are a standard method used by other tools, such as Foundry, so you should be able to re-use your existing setup. An example setup could be:
pragma solidity ^0.8.19;
import {Test} from "forge-std/Test.sol";
contract BadVaultTest is Test {
MyVault vault;
function setUp() public {
// Set up environment
vault = new BadVault();
address user1 = address(1);
vm.deal(user1, 1 ether);
vm.prank(user1);
vault.deposit{value: 1 ether}();
address user2 = address(2);
vm.deal(user2, 1 ether);
vm.prank(user2);
vault.deposit{value: 1 ether}();
address attacker = address(42);
vm.prank(attacker);
// call(s) to test
// postcondition checks
}
}
The postconditions should check the state of the contract after the call(s) are complete. In particular, it should check that the changes that the function applied did not break any of the (invariants)[https://en.wikipedia.org/wiki/Invariant_(mathematics)] of the contract, such as total number of tokens.
You can read more about testing and cheat codes in the (Foundry Book)[https://book.getfoundry.sh/forge/cheatcodes] and you can see the hevm-supported cheat codes below.
Understanding Counterexamples
When hevm discovers a failure, it prints an example call how to trigger the failure. Let's see the following simple solidity code:
pragma solidity ^0.8.19;
import {Test} from "forge-std/Test.sol";
contract MyContract is Test {
mapping (address => uint) balances;
function prove_single_fail(address recv, uint amt) public {
require(balances[recv] < 100);
if (balances[recv] + amt > 100) { revert(); }
balances[recv] += amt;
assert(balances[recv] < 100);
}
}
After compiling with forge build
, when ran under hevm, we get:
$ hevm test
Checking 1 function(s) in contract src/contract-fail.sol:MyContract
[RUNNING] prove_single_fail(address,uint256)
[FAIL] prove_single_fail(address,uint256)
Counterexample:
result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
calldata: prove_single_fail(0x0000000000000000000000000000000000000000,100)
Here, hevm provided us with a calldata, where the receiver happens to be the
zero address, and the value sent is exactly 100. This indeed is the boundary
condition where the function call fails. The function should have had a >=
rather than a >
in the if
. Notice that in this case, while hevm filled in
the address
to give a complete call, the address itself is irrelevant,
although this is not explicitly mentioned.
Test Cases that Must Always Revert
Hevm assumes that a test case should not always revert. If you have such a test case, hevm will warn you and return a FAIL. For example this toy contract:
pragma solidity ^0.8.19;
import {Test} from "forge-std/Test.sol";
contract MyContract is Test {
uint256 cntr;
function prove_allrevert(uint256 val) public {
if(val < 0) {
unchecked { cntr = val; }
revert();
} else revert();
}
}
When compiled with forge and then ran under hevm with hevm test
, hevm returns:
Checking 1 function(s) in contract src/contract-allrevert.sol:MyContract
[RUNNING] prove_allrevert(uint256)
[FAIL] prove_allrevert(uint256)
Reason:
No reachable assertion violations, but all branches reverted
Prefix this testname with `proveFail` if this is expected
This is sometimes undesirable. In these cases, prefix your contract with
proveFail_
instead of prove_
:
pragma solidity ^0.8.19;
import {Test} from "forge-std/Test.sol";
contract MyContract is Test {
uint256 cntr;
function proveFail_allrevert_expected(uint256 val) public {
if(val < 0) {
unchecked {
cntr = val;
cntr += 1;
}
revert();
}
else revert();
}
}
When this is compiled with forge and then checked with hevm, it leads to:
Checking 1 function(s) in contract src/contract-allrevert-expected.sol:MyContract
[RUNNING] proveFail_allrevert_expected(uint256)
[PASS] proveFail_allrevert_expected(uint256)
Which is now the expected outcome.
Supported 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 happens to be keccak("hevm cheat code"),
implementing the following methods:
Function | Description |
---|---|
function prank(address sender) public | Sets msg.sender to the specified sender for the next call. |
function deal(address 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 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 . For most users, require is preferable. However, in case you wish to understand & modify the internal IR of hevm, you may want to use assume . |
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 createFork(string calldata urlOrAlias) external returns (uint256) | Creates a new fork with the given endpoint and the latest block and returns the identifier of the fork. |
function selectFork(uint256 forkId) external | Takes a fork identifier created by createFork and sets the corresponding forked state as active. |
function activeFork() external returns (uint256) | Returns the identifier of the current fork. |
function label(address addr, string calldata label) external | Labels the address in traces |
Equivalence Checking Tutorial
Equivalence checking allows to check whether two bytecodes do the same thing under all input circumstances. This allows to e.g. create two functions, one that is known to be good, and another that uses less gas, but is hard to check for correctness. Then, with equivalence checking, one can check whether the two behave the same.
Finding Discrepancies
Let's see this toy contract, in file contract1.sol:
//SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract MyContract {
mapping (address => uint) balances;
function my_adder(address recv, uint amt) public {
if (balances[recv] + amt >= 100) { revert(); }
balances[recv] += amt;
}
}
And this, slightly modified one, in file contract2.sol:
//SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract MyContract {
mapping (address => uint) balances;
function my_adder(address recv, uint amt) public {
if (balances[recv] + amt >= 100) { revert(); }
balances[recv] += amt/2;
balances[recv] += amt/2;
}
}
Now ask hevm if they are equivalent. First, let's compile both contracts and get their bytecode:
bytecode1=$(solc --bin-runtime "contract1.sol" | tail -n1)
bytecode2=$(solc --bin-runtime "contract2.sol" | tail -n1)
Let's ask hevm to compare the two:
$ hevm equivalence \
--code-a $(solc --bin-runtime "contract1.sol" | tail -n1) \
--code-b $(solc --bin-runtime "contract2.sol" | tail -n1)
Found 90 total pairs of endstates
Asking the SMT solver for 58 pairs
Reuse of previous queries was Useful in 0 cases
Not equivalent. The following inputs result in differing behaviours:
-----
Calldata:
0xafc2c94900000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000023
Storage:
Addr SymAddr "entrypoint": [(0x0,0x10)]
Transaction Context:
TxValue: 0x0
This tells us that with a value of 0x23 being sent, which corresponds
to 35, the two are not equivalent. This is indeed the case: one will add 35 div 2 = 17
twice, which is 34, the other will add 35.
Fixing and Proving Correctness
Let's fix the above issue by incrementing the balance by 1 in case it's an odd value. Let's call this contract3.sol:
//SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract MyContract {
mapping (address => uint) balances;
function my_adder(address recv, uint amt) public {
if (balances[recv] + amt >= 100) { revert(); }
balances[recv] += amt/2;
balances[recv] += amt/2;
if (amt % 2 != 0) balances[recv]++;
}
}
Let's check whether this new contract is indeed equivalent:
$ hevm equivalence \
--code-a $(solc --bin-runtime "contract1.sol" | tail -n1) \
--code-b $(solc --bin-runtime "contract3.sol" | tail -n1)
Found 108 total pairs of endstates
Asking the SMT solver for 74 pairs
Reuse of previous queries was Useful in 0 cases
No discrepancies found
Hevm reports that the two are now equivalent, even though they clearly don't consume the same amount of gas and have widely different EVM bytecodes. Yet for an outside observer, they behave the same. Notice that hevm didn't simply fuzz the contract and within a given out of time it didn't find a counterexample. Instead, it proved the two equivalent from an outside observer perspective.
hevm test
Usage: hevm test [--root STRING] [--project-type PROJECTTYPE] [--rpc TEXT]
[--number W256] [--verbose INT] [--coverage] [--match STRING]
[--solver TEXT] [--num-solvers NATURAL] [--smtdebug] [--debug]
[--trace] [--ffi] [--smttimeout NATURAL]
[--max-iterations INTEGER]
[--loop-detection-heuristic LOOPHEURISTIC]
[--abstract-arithmetic] [--abstract-memory]
[--num-cex-fuzz INTEGER] [--ask-smt-iterations INTEGER]
Available options:
-h,--help Show this help text
--root STRING Path to project root directory (default: . )
--project-type PROJECTTYPE
Is this a Foundry or DappTools project (default:
Foundry)
--rpc TEXT Fetch state from a remote node
--number W256 Block: number
--verbose INT Append call trace: {1} failures {2} all
--coverage Coverage analysis
--match STRING Test case filter - only run methods matching regex
--solver TEXT Used SMT solver: z3 (default), cvc5, or bitwuzla
--num-solvers NATURAL Number of solver instances to use (default: number of
cpu cores)
--smtdebug Print smt queries sent to the solver
--debug Debug printing of internal behaviour
--trace Dump trace
--ffi Allow the usage of the hevm.ffi() cheatcode (WARNING:
this allows test authors to execute arbitrary code on
your machine)
--smttimeout NATURAL Timeout given to SMT solver in seconds (default: 300)
--max-iterations INTEGER Number of times we may revisit a particular branching
point
--loop-detection-heuristic LOOPHEURISTIC
Which heuristic should be used to determine if we are
in a loop: StackBased (default) or Naive
(default: StackBased)
--abstract-arithmetic Use abstraction-refinement for complicated arithmetic
functions such as MulMod. This runs the solver first
with abstraction turned on, and if it returns a
potential counterexample, the counterexample is
refined to make sure it is a counterexample for the
actual (not the abstracted) problem
--abstract-memory Use abstraction-refinement for Memory. This runs the
solver first with abstraction turned on, and if it
returns a potential counterexample, the
counterexample is refined to make sure it is a
counterexample for the actual (not the abstracted)
problem
--num-cex-fuzz INTEGER Number of fuzzing tries to do to generate a
counterexample (default: 3) (default: 3)
--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)
hevm test
executes all solidity unit tests that make use of the ds-test
assertion library
(a.k.a Foundry tests). It
supports both foundry based (the default) and dapptools based projects.
A more detailed introduction to symbolic unit tests with hevm
can be found
here. An
overview of using ds-test for solidity testing can be found in the foundry
book.
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), cvc5, or bitwuzla
--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] [--debug]
[--trace] [--ask-smt-iterations INTEGER]
[--num-cex-fuzz INTEGER]
[--loop-detection-heuristic LOOPHEURISTIC]
[--abstract-arithmetic] [--abstract-memory]
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), cvc5, or bitwuzla
--smtoutput Print verbose smt output
--smtdebug Print smt queries sent to the solver
--debug Debug printing of internal behaviour
--trace Dump trace
--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-cex-fuzz INTEGER Number of fuzzing tries to do to generate a
counterexample (default: 3) (default: 3)
--loop-detection-heuristic LOOPHEURISTIC
Which heuristic should be used to determine if we are
in a loop: StackBased (default) or Naive
(default: StackBased)
--abstract-arithmetic Use abstraction-refinement for complicated arithmetic
functions such as MulMod. This runs the solver first
with abstraction turned on, and if it returns a
potential counterexample, the counterexample is
refined to make sure it is a counterexample for the
actual (not the abstracted) problem
--abstract-memory Use abstraction-refinement for Memory. This runs the
solver first with abstraction turned on, and if it
returns a potential counterexample, the
counterexample is refined to make sure it is a
counterexample for the actual (not the abstracted)
problem
Symbolically execute both the code given in --code-a
and --code-b
and try
to prove equivalence between their outputs and storages. Extracting bytecode
from solidity contracts can be done via, e.g.:
hevm equivalence \
--code-a $(solc --bin-runtime "contract1.sol" | tail -n1) \
--code-b $(solc --bin-runtime "contract2.sol" | tail -n1)
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]
[--debug] [--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
--debug Debug printing of internal behaviour
--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: either you must provide --code
or you must both pass
--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
"Return: 0x647175696e6550383480393834f3"
Which says that given the EVM bytecode 0x647175696e6550383480393834f3
, the Ethereum
Virtual Machine will put 0x647175696e6550383480393834f3
in the RETURNDATA.
To execute a mainnet transaction:
# install seth as per
# https://github.com/makerdao/developerguides/blob/master/devtools/seth/seth-guide/seth-guide.md
$ 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)