Skip to content

Commit d276757

Browse files
msoosethmsooseth
authored
Merge pull request #690 from ethereum/improve-docs
Improve docs
2 parents 936c175 + 00c5f6f commit d276757

File tree

6 files changed

+255
-195
lines changed

6 files changed

+255
-195
lines changed

‎doc/src/SUMMARY.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,3 +17,4 @@
1717
- [Symbolic unit execution](./symbolic.md)
1818
- [Equivalence checking](./equivalence.md)
1919
- [Concrete execution](./exec.md)
20+
- [Common options](./common-options.md)

‎doc/src/common-options.md‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
# Common options
2+
3+
The subcommands of hevm present a number
4+
of common options. Here, we document these options in detail.
5+
6+
## Maximum Buffer Size, ``--max-buf-size``
7+
8+
The buffers in hevm are limited to a maximum size of 2^N bytes, where N is by
9+
default 64, but adjustable via the `--max-buf-size` flag. This helps to prevent
10+
the system from creating buffers that are too large and would exceed the gas
11+
limit. Limiting this value further to e.g. 20 can help to force the system to
12+
generate counterexamples that are easier to examine and understand.
13+
14+
## Choice of Solver, ``--solver``
15+
16+
hevm can use any SMT solver that supports the AUFBV theory and incremental
17+
solving. Currently, z3, cvc5, and bitwuzla's interfaces are implemented. While
18+
any of these solvers work, we recommend using bitwuzla as it is in general
19+
extremely fast, almost always significantly faster than e.g. z3.
20+
21+
## Number of Solvers, ``--num-solvers``
22+
23+
hevm can run multiple solvers in parallel and will run as many solvers as it
24+
detects the number of CPU cores on the machine. However, in some cases, that
25+
may lead to memory outs, in case the solver happens to get queries that are
26+
memory-intensive. In these cases, the number of solvers can be limited to a a
27+
specific (low) number via the `--num-solvers` flag.
28+
29+
## Promising no reentrancy, ``--promise-no-reent``
30+
31+
hevm can be instructed to assume that no reentrancy will occur during the
32+
execution of the contract. This is currently neccessary to fully explore
33+
certain contracts. This is because value transfer is usually done via a `CALL`,
34+
which can be reentrant. By promising no reentrancy, the system can assume that
35+
no reentrancy will occur and can explore the contract more fully.
36+
37+
## Timeout for SMT queries, ``--smttimeout``
38+
39+
Some queries take too long. With a timeout, we ensure that hevm eventually
40+
terminates. However, endstates where the timeout was reached are considered
41+
inditerminate, and will lead to a `WARNING` in the output. It is worthwhile
42+
trying to switch to a different SMT solver such as bitwuzla, or increasing the
43+
timeout if this happens.
44+
45+
## Loop Iteration Limit, ``--ask-smt-iterations``
46+
47+
Loops in the code cause a challenge to symbolic execution framework. In order
48+
to not run indefinitely, hevm will only explore a certain number of iterations
49+
of a loop before consideing abandoning the exploration of that branch. This
50+
number can be set via the `--ask-smt-iterations` flag.

‎doc/src/equivalence.md‎

Lines changed: 141 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -1,53 +1,152 @@
11
# `hevm equivalence`
22

3-
```
4-
Usage: hevm equivalence --code-a TEXT --code-b TEXT [--sig TEXT]
5-
[--arg STRING]... [--calldata TEXT]
6-
[--smttimeout NATURAL] [--max-iterations INTEGER]
7-
[--solver TEXT] [--smtoutput] [--smtdebug] [--debug]
8-
[--trace] [--ask-smt-iterations INTEGER]
9-
[--num-cex-fuzz INTEGER]
10-
[--loop-detection-heuristic LOOPHEURISTIC]
11-
[--abstract-arithmetic] [--abstract-memory]
12-
13-
Available options:
14-
-h,--help Show this help text
15-
--code-a TEXT Bytecode of the first program
16-
--code-b TEXT Bytecode of the second program
17-
--sig TEXT Signature of types to decode / encode
18-
--arg STRING Values to encode
19-
--calldata TEXT Tx: calldata
20-
--smttimeout NATURAL Timeout given to SMT solver in seconds (default: 300)
21-
--max-iterations INTEGER Number of times we may revisit a particular branching
22-
point. Default is 5. Setting to -1 allows infinite looping
23-
--solver TEXT Used SMT solver: z3 (default), cvc5, or bitwuzla
24-
--smtoutput Print verbose smt output
25-
--smtdebug Print smt queries sent to the solver
26-
--debug Debug printing of internal behaviour
27-
--trace Dump trace
28-
--ask-smt-iterations INTEGER
29-
Number of times we may revisit a particular branching
30-
point before we consult the smt solver to check
31-
reachability (default: 1) (default: 1)
32-
--num-cex-fuzz INTEGER Number of fuzzing tries to do to generate a
33-
counterexample (default: 3) (default: 3)
34-
--loop-detection-heuristic LOOPHEURISTIC
35-
Which heuristic should be used to determine if we are
36-
in a loop: StackBased (default) or Naive
37-
(default: StackBased)
3+
```plain
4+
Usage: hevm equivalence [--code-a TEXT] [--code-b TEXT] [--code-a-file STRING]
5+
[--code-b-file STRING] [--sig TEXT] [--arg STRING]...
6+
[--calldata TEXT] [--smttimeout NATURAL]
7+
[--max-iterations INTEGER] [--solver TEXT]
8+
[--num-solvers NATURAL] ...
389
```
3910

4011
Symbolically execute both the code given in `--code-a` and `--code-b` and try
41-
to prove equivalence between their outputs and storages. Extracting bytecode
42-
from solidity contracts can be done via, e.g.:
12+
to prove equivalence between their outputs and storages. For a full listing of
13+
options, see `hevm equivalence --help`. For common options, see
14+
[here](./common-options.md).
4315

16+
## Simple example usage
17+
18+
```shell
19+
$ solc --bin-runtime "contract1.sol" | tail -n1 > a.bin
20+
$ solc --bin-runtime "contract2.sol" | tail -n1 > b.bin
21+
$ hevm equivalence --code-a-file a.bin --code-b-file b.bin
4422
```
45-
hevm equivalence \
46-
--code-a $(solc --bin-runtime "contract1.sol" | tail -n1) \
47-
--code-b $(solc --bin-runtime "contract2.sol" | tail -n1)
48-
```
23+
24+
## Calldata size limits
25+
4926
If `--sig` is given, calldata is assumed to take the form of the function
5027
given. If `--calldata` is provided, a specific, concrete calldata is used. If
5128
neither is provided, a fully abstract calldata of at most `2**64` byte is
5229
assumed. Note that a `2**64` byte calldata would go over the gas limit, and
53-
hence should cover all meaningful cases.
30+
hence should cover all meaningful cases. You can limit the buffer size via
31+
`--max-buf-size`, which sets the exponent of the size, i.e. 10 would limit the
32+
calldata to `2**10` bytes.
33+
34+
## What constitutes equivalence
35+
36+
The equivalence checker considers two contracts equivalent if given the
37+
same calldata they:
38+
- return the same value
39+
- have the same storage
40+
- match on the success/failure of the execution
41+
Importantly, logs are *not* considered in the equivalence check. Hence,
42+
it is possible that two contracts are considered equivalent by `hevm equivalence` but
43+
they emit different log items. Furthermore, gas is explicitly not considered,
44+
as in many cases, the point of the equivalence check is to ensure that the
45+
contracts are functionally equivalent, but one of them is more gas efficient.
46+
47+
For example, two contracts that are:
48+
49+
```
50+
PUSH1 3
51+
```
52+
53+
And
54+
55+
```
56+
PUSH1 4
57+
```
58+
59+
Are considered *equivalent*, because they don't put anything in the return
60+
data, are not different in their success/fail attribute, and don't touch
61+
storage. However, these two are considered different:
62+
63+
```
64+
PUSH1 3
65+
PUSH1 0x20
66+
MSTORE
67+
PUSH1 0x40
68+
PUSH1 0x00
69+
RETURN
70+
```
71+
72+
and:
73+
74+
75+
```
76+
PUSH1 4
77+
PUSH1 0x20
78+
MSTORE
79+
PUSH1 0x40
80+
PUSH1 0x00
81+
RETURN
82+
```
83+
84+
Since one of them returns a 3 and the other a 4. We also consider contracts different when
85+
they differ in success/fail. So these two contracts:
86+
87+
```
88+
PUSH1 0x00
89+
PUSH1 0x00
90+
RETURN
91+
```
92+
93+
and:
94+
95+
```
96+
PUSH1 0x00
97+
PUSH1 0x00
98+
REVERT
99+
```
100+
101+
Are considered different, as one of them reverts (i.e. fails) and the other
102+
succeeds.
103+
104+
## Creation code equivalence
105+
106+
If you want to check the equivalence of not just the runtime code, but also the
107+
creation code of two contracts, you can use the `--creation` flag. For example
108+
these two contracts:
109+
110+
```solidity
111+
contract C {
112+
uint private immutable NUMBER;
113+
constructor(uint a) {
114+
NUMBER = 2;
115+
}
116+
function stuff(uint b) public returns (uint256) {
117+
unchecked{return 2+NUMBER+b;}
118+
}
119+
}
120+
```
121+
122+
And:
123+
124+
```solidity
125+
contract C {
126+
uint private immutable NUMBER;
127+
constructor(uint a) {
128+
NUMBER = 4;
129+
}
130+
function stuff(uint b) public returns (uint256) {
131+
unchecked {return NUMBER+b;}
132+
}
133+
}
134+
```
135+
136+
Will compare equal when compared with `--create` flag:
137+
138+
```shell
139+
solc --bin a.sol | tail -n1 > a.bin
140+
solc --bin b.sol | tail -n1 > b.bin
141+
cabal run exe:hevm equivalence -- --code-a-file a.bin --code-b-file b.bin --create
142+
```
143+
144+
Notice that we used `--bin` and not `--bin-runtime` for solc here. Also note that
145+
in case `NUMBER` is declared `public`, the two contracts will not be considered
146+
equivalent, since solidity will generate a getter for `NUMBER`, which will
147+
return 2/4 respectively.
148+
149+
## Further reading
150+
151+
For a tutorial on how to use `hevm equivalence`, see the [equivalence checking
152+
tutorial](symbolic-execution-tutorial.html).

‎doc/src/exec.md‎

Lines changed: 11 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -2,57 +2,28 @@
22

33
Run an EVM computation using specified parameters.
44

5-
```
6-
Usage: hevm exec [--code TEXT] [--calldata TEXT] [--address ADDR]
5+
```plain
6+
Usage: hevm exec [--code TEXT] [--code-file STRING] [--calldata TEXT] [--address ADDR]
77
[--caller ADDR] [--origin ADDR] [--coinbase ADDR]
88
[--value W256] [--nonce WORD64] [--gas WORD64] [--number W256]
99
[--timestamp W256] [--basefee W256] [--priority-fee W256]
10-
[--gaslimit WORD64] [--gasprice W256] [--create]
10+
[--gaslimit WORD64] [--gasprice W256]
1111
[--maxcodesize W256] [--prev-randao W256] [--chainid W256]
12-
[--debug] [--trace] [--rpc TEXT] [--block W256] [--root STRING]
13-
[--project-type PROJECTTYPE]
14-
15-
Available options:
16-
-h,--help Show this help text
17-
--code TEXT Program bytecode
18-
--calldata TEXT Tx: calldata
19-
--address ADDR Tx: address
20-
--caller ADDR Tx: caller
21-
--origin ADDR Tx: origin
22-
--coinbase ADDR Block: coinbase
23-
--value W256 Tx: Eth amount
24-
--nonce WORD64 Nonce of origin
25-
--gas WORD64 Tx: gas amount
26-
--number W256 Block: number
27-
--timestamp W256 Block: timestamp
28-
--basefee W256 Block: base fee
29-
--priority-fee W256 Tx: priority fee
30-
--gaslimit WORD64 Tx: gas limit
31-
--gasprice W256 Tx: gas price
32-
--create Tx: creation
33-
--maxcodesize W256 Block: max code size
34-
--prev-randao W256 Block: prevRandao
35-
--chainid W256 Env: chainId
36-
--debug Debug printing of internal behaviour
37-
--trace Dump trace
38-
--rpc TEXT Fetch state from a remote node
39-
--block W256 Block state is be fetched from
40-
--root STRING Path to project root directory (default: . )
41-
--project-type PROJ Foundry or CombinedJSON project (default: Foundry)
42-
--assertion-type ASSERT Assertions as per Forge or DSTest (default: Forge)
12+
[--trace] [--rpc TEXT] [--block W256] ...
4313
```
4414

45-
Minimum required flags: either you must provide `--code` or you must both pass
46-
`--rpc` and `--address`.
15+
Concretely execute a given EVM bytecode with the specified parameters. Minimum
16+
required flags: either you must provide `--code` or you must both pass `--rpc`
17+
and `--address`. For a full listing of options, see `hevm exec --help`.
4718

4819
If the execution returns an output, it will be written
4920
to stdout. Exit code indicates whether the execution was successful or
5021
errored/reverted.
5122

52-
Simple example usage:
23+
## Simple example usage
5324

54-
```
55-
hevm exec --code 0x647175696e6550383480393834f3 --gas 0xff
25+
```shell
26+
$ hevm exec --code 0x647175696e6550383480393834f3 --gas 0xff
5627
"Return: 0x647175696e6550383480393834f3"
5728
```
5829

@@ -61,7 +32,7 @@ Virtual Machine will put `0x647175696e6550383480393834f3` in the RETURNDATA.
6132

6233
To execute a mainnet transaction:
6334

64-
```
35+
```shell
6536
# install seth as per
6637
# https://github.com/makerdao/developerguides/blob/master/devtools/seth/seth-guide/seth-guide.md
6738
$ export ETH_RPC_URL=https://mainnet.infura.io/v3/YOUR_API_KEY_HERE

0 commit comments

Comments
 (0)