# Changelog

All notable changes to this project will be documented in this file.

The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).

## [0.50.4] - 2023-03-17

### Fixed

- The `--solvers` cli option is now respected (previously we always used Z3)
- The `equivalence` command now fails with the correct status code when counterexamples are found
- The `equivalence` command now respects the given `--sig` argument
- Correct symbolic execution for the `SGT` opcode

### Changed

- The `equivalence` command now pretty prints discovered counterexamples

### Added

- Implemented a shrinking algorithm for counterexamples
- A new differential fuzzing test harness that compares the concrete semantics, as well as parts of the symbolic semantics against the geth evm implementation
- The `hevm` library can now be built on Windows systems.
- Support for function pointers in ABI
- `equivalence` can now be checked for fully or partially concrete calldata

## [0.50.3] - 2023-02-17

### Fixed

- `hevm symbolic` exits with status code `1` if counterexamples or timeouts are found
- Calldata reads beyond calldata size are provably equal to zero.

### Added

- New cheatcode `prank(address)` that sets `msg.sender` to the specified address for the next call.
- Improved equivalence checker that avoids checking similar branches more than once.
- Improved simplification for arithmetic expressions
- Construction of storage counterexamples based on the model returned by the SMT solver.
- Static binaries for macos

### Changed
- SMT encoding of buffer length without using uninterpreted functions.

## [0.50.2] - 2023-01-06

### Fixed

- Arithmetic overflow in concrete `SAR` edge case ([#163](https://github.com/ethereum/hevm/pull/163))
- Unexpected abstract term application during fully concrete execution ([#163](https://github.com/ethereum/hevm/pull/163))

## [0.50.1] - 2022-12-29

### Fixed

- `hevm exec` no longer fails with `hevm: No match in record selector smttimeout`
- the `gas`, `gaslimit`, `priorityfee`, and `gasprice` cli options are now respected
- cleaner formatting for the gas value in the visual debugger

### Changed

- we now build with ghc 9.2.4 by default
- various perf improvements for concrete execution ([#157](https://github.com/ethereum/hevm/pull/157), [#152](https://github.com/ethereum/hevm/pull/152))

## [0.50.0] - 2022-12-19

### Changed

The symbolic execution engine has been rewritten. We have removed our dependency on sbv, and now
symbolic execution decompiles bytecode into a custom IR, and smt queries are constructed based on
the structure of the term in this IR.

This gives us much deeper control over the encoding, and makes custom static analysis and
simplification passes much easier to implement.

The symbolic execution engine is now parallel by default, and will distribute granular SMT queries
across a pool of solvers, allowing analysis to be scaled out horizontally across many CPUs.

more details can be found in the [architecuture](../../architecture.md) docs.

### Removed

The following cli commands have been removed:

- `abiencode`
- `rlp`
- `flatten`
- `strip-metadata`

## [0.49.0] - 2021-11-12

### Added

- Support for solc 0.8.10
- Support for solc 0.8.11

### Changed

- Clearer display for the invalid opcode (`0xfe`) in debug view
- Better error messages when trying to deploy unlinked bytecode
- `bytesX` arguments to `hevm abiencode` are automatically padded

### Fixed

- Test contracts with no code (e.g. `abstract` contracts) are now skipped
- Replay data for invariant tests is now displayed in a form that does not cause errors when used with `dapp test --replay`

## [0.48.1] - 2021-09-08

### Added

- Support for 0.8.4 custom error types in stack traces

### Changed

- Contract feching happens synchronously again.
- Invariants checked before calling methods from targetContracts.

### Fixed

- The block gas limit and basefee are now correctly fetched when running tests via rpc

## 0.48.0 - 2021-08-03

### Changed

- Updated to London hard fork!
- The configuration variable `DAPP_TEST_BALANCE_CREATE` has been renamed to `DAPP_TEST_BALANCE`
- Default `smttimeout` has been increased to 1 minute.
- A new flag has been added to hevm (`--ask-smt-iterations`) that controls the number of iterations
  at which the symbolic execution engine will stop eager evaluation and begin to query the smt
  solver whether a given branch is reachable or not.
- Contract fetching now happens asynchronously.
- Fixed no contract definition crashes
- Removed NoSuchContract failures

## 0.47.0 - 2021-07-01

### Added

- A new test runner for checking invariants against random reachable contract states.
- `hevm symbolic` can search for solc 0.8 style assertion violations, and a new `--assertions` flag
  has been added allowing users to customize which assertions should be reported
- A new cheatcode `ffi(string[])` that executes an arbitrary command in the system shell

### Changed

- Z3 is once again the default smt solver
- Updated nixpkgs to the `21.05` channel

### Fixed

- Sourcemaps for contracts containing `immutable` are now shown in the debug view.

## 0.46.0 - 2021-04-29

### Added

- Updated to Berlin! Conformant with GeneralStateTests at commit hash `644967e345bbc6642fab613e1b1737abbe131f78`.

### Fixed

- ADDMOD and MULMOD by zero yields zero.
- Address calculation for newly created contracts.
- Accomodated for the notorious "anomolies on the main network" (see yellow paper Appendix K for trivia)
- A hevm crash when debugging a SELFDESTRUCT contract.

## 0.45.0 - 2021-03-22

### Added

- Two new cheatcodes were added: `sign(uint sk, bytes message)` and `addr(uint sk)`. Taken together
  these should allow for much more ergonomic testing of code that handles signed messages.
- Symbolic execution can deal with partially symbolic bytecode, allowing for symbolic constructor arguments to be given in tests.

### Fixed

- Fixed a bug in the abiencoding.
- Fixed the range being generated by ints.
- `hevm flatten` combines the SPDX license identifiers of all source files.

### Changed

- updated `nixpkgs` to the `20.09` channel
- Arbitrary instance of AbiType can no longer generate a tuple

## 0.44.1 - 2020-02-02

### Changed

- hevm cheatcodes now accept symbolic arguments, allowing e.g. symbolic jumps in time in unit tests
- More efficient arithmetic overflow checks by translating queries to a more [intelligent form](www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf).

## 0.44.0 - 2020-01-26

### Added

- `hevm` now accepts solidity json output built via `--standard-json` as
  well as `--combined-json`.
- addresses in the trace output are prefixed with `ContractName@0x...`
  if there is a corresponding contract and `@0x...` otherwise.

### Fixed

- Symbolic execution now generates calldata arguments restricted to the proper ranges,
  following the semantics of fuzzing.
- If the `--address` flag is present in `hevm exec` or `hevm symbolic`,
  it overrides the contract address at which a contract will be created.
- Address pretty printing
- Updated sbv to `8.9.5` to fix "non-const in array declaration" cvc4 issue with ds-test.

### Changed

- Use cvc4 as default smt solver

## 0.43.2 - 2020-12-10

### Changed

- The default smttimeout has been increased from 20s to 30s

## 0.43.1 - 2020-12-10

### Changed

- Counterexamples from symbolic tests now show clearer failure reasons

### Fixed

- Symbolic tests now work with RPC
- Branch selection is working again in the interactive debugger

## 0.43.0 - 2020-11-29

### Added

- A `--show-tree` option to `hevm symbolic` which prints the execution tree explored.
- Some symbolic terms are displayed with richer semantic information, instead of the black box `<symbolic>`.
- `hevm dapp-test` now supports symbolic execution of test methods that are prefixed with `prove` or `proveFail`
- The `hevm interactive` alias has been removed, as it is equivalent to `hevm dapp-test --debug`
- `hevm dapp-test --match` now matches on contract name and file path, as well as test name
- Step through the callstack in debug mode using the arrow keys

### Changed

- `dapp-test` trace output now detects ds-note events and shows `LogNote`
- create addresses are shown with `@<address>` in the trace
- `DSTest.setUp()` is only run if it exists, rather than failing
- support new ds-test `log_named_x(string, x)` (previously bytes32 keys)
- return arguments are fully displayed in the trace (previously only a single word)
- return/revert trace will now show the correct source position

## 0.42.0 - 2020-10-31

### Changed

- z3 updated to 4.8.8
- optimize SMT queries
- More useful trace output for unknown calls
- Default to on chain values for `coinbase`, `timestamp`, `difficulty`, `blocknumber` when rpc is provided
- Perform tx initialization (gas payment, value transfer) in `hevm exec`, `hevm symbolic` and `hevm dapp-test`.

### Added

- TTY commands `P` and `c-p` for taking larger steps backwards in the debuger.
- `--cache` flag for `dapp-test`, `exec`, `symbolic`, `interactive`,
  enabling caching of contracts received by rpc.
- `load(address,bytes32)` cheat code allowing storage reads from arbitrary contracts.

## 0.41.0 - 2020-08-19

### Changed

- Switched to [PVP](https://github.com/haskell/pvp/blob/master/pvp-faq.md) for version control, starting now at `0.41.0` (MAJOR.MAJOR.MINOR).
- z3 updated to 4.8.7
- Generate more interesting values in property based testing,
  and implement proper shrinking for all abi values.
- Fixed soundness bug when using KECCAK or SHA256 opcode/precompile
- Fixed an issue in debug mode where backstepping could cause path information to be forgotten
- Ensure that pathconditions are consistent when branching, and end the execution with VMFailure: DeadPath if this is not the case
- Fixed a soundness bug where nonzero jumpconditions were assumed to equal one.
- default `--smttimeout` changed from unlimited to 20 seconds
- `hevm symbolic --debug` now respects `--max-iterations`

### Added

- `hevm exec --trace` flag to dump a trace
- Faster backstepping in interactive mode by saving multiple snapshot states.
- Support for symbolic storage for multiple contracts

## 0.40 - 2020-07-22

- hevm is now capable of symbolic execution!

### Changed

As a result, the types of several registers of the EVM have changed to admit symbolic values as well as concrete ones.

- state.stack: `Word` -> `SymWord`.
- state.memory: `ByteString` -> `[SWord 8]`.
- state.callvalue: `W256` -> `SymWord`.
- state.caller: `Addr` -> `SAddr`.
- state.returndata: `ByteString` -> `[SWord 8]`.
- state.calldata: `ByteString` -> `([SWord 8], (SWord 32))`. The first element is a list of symbolic bytes, the second is the length of calldata. We have `fst calldata !! i .== 0` for all `snd calldata < i`.

- tx.value: `W256` -> `SymWord`.

- contract.storage: `Map Word Word` -> `Storage`, defined as:

```hs
data Storage
  = Concrete (Map Word SymWord)
  | Symbolic (SArray (WordN 256) (WordN 256))
  deriving (Show)
```

### Added

New cli commands:

- `hevm symbolic`: search for assertion violations, or step through a symbolic execution in debug mode.
- `hevm equivalence`: compare two programs for equivalence.

See the README for details on usage.

The new module `EVM.SymExec` exposes several library functions dealing with symbolic execution.
In particular,

- `SymExec.interpret`: implements an operational monad script similar to `TTY.interpret` and `Stepper.interpret`, but returns a list of final VM states rather than a single VM.
- `SymExec.verify`: takes a prestate and a postcondition, symbolically executes the prestate and checks that all final states matches the postcondition.

### Removed

The concrete versions of a lot of arithmetic operations, replaced with their more general symbolic counterpart.

## 0.39 - 2020-07-13

- Exposes abi encoding to cli
- Added cheat code `hevm.store(address a, bytes32 location, bytes32 value)`
- Removes `ExecMode`, always running as `ExecuteAsBlockchainTest`. This means that `hevm exec` now finalizes transactions as well.
- `--code` is now entirely optional. Not supplying it returns an empty contract, or whatever is stored in `--state`.

## 0.38 - 2020-04-23

- Exposes metadata stripping of bytecode to the cli: `hevm strip-metadata --code X`. [357](https://github.com/dapphub/dapptools/pull/357).
- Fixes a bug in the srcmap parsing introduced in 0.37 [356](https://github.com/dapphub/dapptools/pull/356).
- Fixes a bug in the abi-encoding of `bytes` with size > 32[358](https://github.com/dapphub/dapptools/pull/358).

## 0.37 - 2020-03-24

- Sourcemap parser now admits `solc-0.6.0` compiled `.sol.json` files.

## 0.36 - 2020-01-07

- Implement Istanbul support [318](https://github.com/dapphub/dapptools/pull/318)
- Fix a bug introduced in [280](https://github.com/dapphub/dapptools/pull/280) of rlp encoding of transactions and sender address [320](https://github.com/dapphub/dapptools/pull/320/).
- Make InvalidTx a fatal error for vm tests and ci.
- Suport property based testing in unit tests. [313](https://github.com/dapphub/dapptools/pull/313) Arguments to test functions are randomly generated based on the function abi. Fuzz tests are not present in the graphical debugger.
- Added flags `--replay` and `--fuzz-run` to `hevm dapp-test`, allowing for particular fuzz run cases to be rerun, or for configuration of how many fuzz tests are run.
- Correct gas readouts for unit tests
- Prevent crash when trying to jump to next source code point if source code is missing

## 0.35 - 2019-11-02

- Merkle Patricia trie support [280](https://github.com/dapphub/dapptools/pull/280)
- RLP encoding and decoding functions [280](https://github.com/dapphub/dapptools/pull/280)
- Extended support for Solidity ABI encoding [259](https://github.com/dapphub/dapptools/pull/259)
- Bug fixes surrounding unit tests and gas accounting (https://github.com/dapphub/dapptools/commit/574ef401d3e744f2dcf994da056810cf69ef84fe, https://github.com/dapphub/dapptools/commit/5257574dd9df14edc29410786b75e9fb9c59069f)

## 0.34 - 2019-08-28

- handle new solc bzzr metadata in codehash for source map
- show VM hex outputs as hexadecimal
- rpc defaults to latest block
- `hevm interactive`:
- fix rpc fetch
- scrollable memory pane
- Fix regression in VMTest compliance.
- `hevm exec` ergonomics:
- Allow code/calldata prefixed with 0x
- create transactions with specific caller nonce
- interactive help pane
- memory pane scrolling

## 0.33 - 2019-08-06

- Full compliance with the [General State Tests][245] (with the
  BlockchainTest format), using the Yellow and Jello papers as
  reference, for Constantinople Fix (aka Petersburg). Including:
- full precompile support
- correct substate accounting, including touched accounts,
  selfdestructs and refunds
- memory read/write semantics
- many gas cost corrections
- Show more information for non solc bytecode in interactive view
  (trace and storage)
- Help text for all cli options
- Enable `--debug` flag in `hevm dapp-test`

[245]: https://github.com/dapphub/dapptools/pull/245

## 0.32 - 2019-06-14

- Fix dapp-test [nonce initialisation bug][224]

[224]: https://github.com/dapphub/dapptools/pull/224

## 0.31 - 2019-05-29

- Precompiles: SHA256, RIPEMD, IDENTITY, MODEXP, ECADD, ECMUL,
  ECPAIRING, MODEXP
- Show the hevm version with `hevm version`
- Interactive mode:
- no longer exits on reaching halt
- new shortcuts: 'a' / 'e' for start / end
- allow returning to test picker screen
- Exact integer formatting in dapp-test and tty

## 0.30 - 2019-05-09

- Adjustable verbosity level for `dapp-test` with `--verbose={0,1,2}`
- Working stack build

## 0.29 - 2019-04-03

- Significant jump in compliance with client tests
- Add support for running GeneralStateTests

## 0.28 - 2019-03-22

- Fix delegatecall gas metering, as reported in
  https://github.com/dapphub/dapptools/issues/34

## 0.27 - 2019-02-06

- Fix [hevm flatten issue](https://github.com/dapphub/dapptools/issues/127)
  related to SemVer ranges in Solidity version pragmas

## 0.26 - 2019-02-05

- Format Solidity Error(string) messages in trace

## 0.25 - 2019-02-04

- Add SHL, SHR and SAR opcodes

## 0.24 - 2019-01-23

- Fix STATICCALL for precompiled contracts
- Assume Solidity 0.5.2 in tests

## 0.23 - 2018-12-12

- Show passing test traces with --verbose flag

## 0.22 - 2018-11-13

- Simple memory view in TTY

## 0.21 - 2018-10-29

- Fix Hackage package by including C header files for ethjet

## 0.20 - 2018-10-27

- Parse constructor inputs from Solidity AST

## 0.19 - 2018-10-09

- Enable experimental 'cheat' address, allowing for modification of the
  EVM environment from within the tests. Currently just the block
  timestamp can be adjusted.

## 0.18 - 2018-10-09

- Fix [duplicate address bug](https://github.com/dapphub/dapptools/issues/70)

## 0.17 - 2018-10-05

- Semigroup/Monoid fix

## 0.16 - 2018-09-19

- Move ethjet into hevm

## [0.15] - 2018-05-09

- Fix SDIV/SMOD definitions for extreme case

## [0.14.1] - 2018-04-17

- Improve PC display in TTY

## [0.14] - 2018-03-08

- Implement STATICCALL

## [0.13] - 2018-02-28

- Require specific block number for RPC debugging
- Implement RETURNDATACOPY and RETURNDATASIZE
- Fix bug where created contracts didn't get their balance

## [0.12.3] - 2017-12-19

- More useful RPC debugging because we strip the entire BZZR metadata

## [0.12.2] - 2017-12-17

- Experimental new ecrecover implementation via libethjet
- Correct error checking for setUp() invocations

## [0.12.1] - 2017-11-28

- Test name regex matching via --match
- Fixed source map parsing bug when used with solc --optimize
- TTY: fix a padding-related display glitch

## [0.12] - 2017-11-14

- Use 13 different environment variables to control block parameters
  for unit testing, e.g. block number, timestamp, initial balance, etc.

  Full list:

  - `DAPP_TEST_ADDRESS`
  - `DAPP_TEST_CALLER`
  - `DAPP_TEST_ORIGIN`
  - `DAPP_TEST_GAS_CREATE`
  - `DAPP_TEST_GAS_CALL`
  - `DAPP_TEST_BALANCE_CREATE`
  - `DAPP_TEST_BALANCE_CALL`
  - `DAPP_TEST_COINBASE`
  - `DAPP_TEST_NUMBER`
  - `DAPP_TEST_TIMESTAMP`
  - `DAPP_TEST_GAS_LIMIT`
  - `DAPP_TEST_GAS_PRICE`
  - `DAPP_TEST_DIFFICULTY`

## [0.11.5] - 2017-11-14

- Use --state with --exec --debug

## [0.11.4] - 2017-11-12

- Fix bug when unit test contract has creations in constructor

## [0.11.3] - 2017-11-08

- Fix array support in ABI module

## [0.11.2] - 2017-11-04

- TTY: show a help bar with key bindings at the bottom

## [0.11.1] - 2017-11-02

- TTY: fix a display glitch
- TTY: improve display of ABI hashes on the stack

## [0.11] - 2017-10-31

- Add "hevm flatten" for Etherscan-ish source code concatenation
- Simplify code by removing concrete/symbolic machine abstraction

## [0.10.9] - 2017-10-23

- Fix bugs in ABI formatting

## [0.10.7] - 2017-10-19

- Fix library linking bug
- Fix gas consumption of DELEGATECALL
- Better error tracing
- Experimental "contract browser" (stupid list of addresses)

## [0.10.6] - 2017-10-19

- Enable library linking for unit tests and debugger
- Use the same default gas/balance values as `ethrun`

## [0.10.5] - 2017-10-17

- Better trace output including arguments and return values
- Proof of concept coverage analysis via `dapp-test --coverage`

## [0.10] - 2017-10-10

- Enable new trace output by default for failing tests
- Exit with failure code from test runner when tests fail
- More fixes to improve Ethereum test suite compliance

## [0.9.5] - 2017-10-06

- Prototype of new trace output with `hevm dapp-test --verbose`
- Nicer trace tree in the TTY debugger
- Many fixes to improve Ethereum test suite compliance

## [0.9] - 2017-09-29

- Integrates with live chains via RPC (read-only)
- Exposes a special contract address with test-related functionality (time warp)

## [0.8.5] - 2017-09-22

- Renames `hevm` from its maiden name `hsevm` :sparkles:

## [0.8] - 2017-09-21

- Implements gas metering (Metropolis rules by default)
- Shows gas counter in the terminal interface
- Enables debugger for consensus test executions
- Consensus test runner script with HTML reporting
- Passes 564 of the `VMTests`; fails 115 (see [0.8 test report])
- Command line options for specifying initial gas amounts and balances
- Improved TTY UI layout

## [0.7] - 2017-09-07

- Can save and load contract states to disk using a Git-backed store (only `--exec`)
- Can debug raw EVM bytecode using `exec --debug`
- Fixes `exec --value`
- Has smarter defaults for command line when running tests or debugging
- Fixes bug with `MSIZE` in `CALL` context

## [0.6.5] - 2017-09-01

- Fixes `exec` with regards to exit codes and error messages

## [0.6.1] - 2017-08-03

- TTY: Adds command `C-n` in TTY for "stepping over"

## [0.6] - 2017-08-03

- TTY: Adds second line to stack entries with humanized formatting
- TTY: Gets rid of the separate log pane in favor of a unified trace pane

## [0.5] - 2017-08-02

- TTY: Adds `p` command for stepping backwards
- Adds ability to track origins of stack and heap words
- Tracks Keccak preimage for words that come from the `SHA3` instruction

## [0.4] - 2017-07-31

- Parallelizes unit test runner
- Improves speed by changing representation of memory
- Internal refactoring for future support of symbolic execution
- Adds logs to the trace pane

## [0.3.2] - 2017-06-17

- Adds `REVERT` opcode
- Sets `TIMESTAMP` value to `1` in unit tests

## [0.3.0] - 2017-06-14

- Reverts contract state after `CALL` fails
- Improves test runner console output

## [0.2.0] - 2017-06-13

- Fixes bug in `CALL`

## [0.1.0.1] - 2017-03-31

- Highlights Solidity exactly on character level
- Adds `N` command for stepping by Solidity source position instead of by opcode

## 0.1.0.0 - 2017-03-29

- First release

[0.8 test report]: https://hydra.dapp.tools/build/135/download/1/index.html
[0.12]: https://github.com/dapphub/hevm/compare/0.11.5...0.12
[0.11.5]: https://github.com/dapphub/hevm/compare/0.11.4...0.11.5
[0.11.4]: https://github.com/dapphub/hevm/compare/0.11.3...0.11.4
[0.11.3]: https://github.com/dapphub/hevm/compare/0.11.2...0.11.3
[0.11.2]: https://github.com/dapphub/hevm/compare/0.11.1...0.11.2
[0.11.1]: https://github.com/dapphub/hevm/compare/0.11...0.11.1
[0.11]: https://github.com/dapphub/hevm/compare/0.10.9...0.11
[0.10.9]: https://github.com/dapphub/hevm/compare/0.10.7...0.10.9
[0.10.7]: https://github.com/dapphub/hevm/compare/0.10.6...0.10.7
[0.10.6]: https://github.com/dapphub/hevm/compare/0.10.5...0.10.6
[0.10.5]: https://github.com/dapphub/hevm/compare/0.10...0.10.5
[0.10]: https://github.com/dapphub/hevm/compare/0.9.5...0.10
[0.9.5]: https://github.com/dapphub/hevm/compare/0.9...0.9.5
[0.9]: https://github.com/dapphub/hevm/compare/v0.8.5...v0.9
[0.8.5]: https://github.com/dapphub/hevm/compare/v0.8...v0.8.5
[0.8]: https://github.com/dapphub/hevm/compare/v0.7...v0.8
[0.7]: https://github.com/dapphub/hevm/compare/v0.6.5...v0.7
[0.6.5]: https://github.com/dapphub/hevm/compare/v0.6.1...v0.6.5
[0.6.1]: https://github.com/dapphub/hevm/compare/v0.6...v0.6.1
[0.6]: https://github.com/dapphub/hevm/compare/v0.5...v0.6
[0.5]: https://github.com/dapphub/hevm/compare/v0.4...v0.5
[0.4]: https://github.com/dapphub/hevm/compare/v0.3.2...v0.4
[0.3.2]: https://github.com/dapphub/hevm/compare/v0.3.0...v0.3.2
[0.3.0]: https://github.com/dapphub/hevm/compare/v0.2.0...v0.3.0
[0.2.0]: https://github.com/dapphub/hevm/compare/v0.1.0.1...v0.2.0
[0.1.0.1]: https://github.com/dapphub/hevm/compare/v0.1.0.0...v0.1.0.1