Changelog for hevm-0.53.0

[0.53.0] - 2024-02-23

Changelog

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

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

Changed

Added

Fixed

[0.52.0] - 2023-10-26

This is a major breaking release that removes several user facing features and includes non trivial breakage for library users. These changes mean the code is significantly simpler, more performant, and allow support for new features like fully symbolic addresses.

In addition to the changes below, this release includes significant work on performance optimization for symbolic execution.

Added

The major new user facing feature in this release is support for fully symbolic addresses (including fully symbolic addresses for deployed contracts). This allows tests to be writen that call vm.prank with a symbolic value, making some tests (e.g. access control, token transfer logic) much more comprehensive.

Some restrictions around reading balances from and transfering value between symbolic addresses are currently in place. Currently, if the address is symbolic, then you will only be able to read it's balance, or transfer value to/from it, if it is the address of a contract that is actually deployed. This is required to ensure soundness in the face of aliasing between symbolic addresses. We intend to lift this restriction in a future release.

Other

Changed

Revert Semantics in Solidity Tests

solidity tests no longer consider reverts to be a failure, and check only for the ds-test failed bit or user defined assertion failures (i.e. Panic(0x01)). This makes writing tests much easier as users no longer have to consider trivial reverts (e.g. arithmetic overflow).

A positive (i.e. prove/check) test with no rechable assertion violations that does not have any succesful branches will still be considered a failure.

Removed

hevm has been around for a while, and over time has accumulated many features. We decided to remove some of these features in the interest of focusing our attention, increasing our iteration speed and simplifying maintainance. The following user facing features have been removed from this release:

Fixed

This release also includes many small bugfixes:

API Changes

Reworked Storage Model / Symbolic Addresses

Adding symbolic addresses required some fairly significant changes to the way that we model storage. We introduced a new address type to Expr (Expr EAddr), that allows us to model fully symbolic addresses. Instead of modelling storage as a global symbolic 2D map (address -> word -> word) in vm.env, each contract now has it's own symbolic 1D map (word -> word), that is stored in the vm.contracts mapping. vm.contracts is now keyed on Expr EAddr instead of Addr. Addresses that are keys to the vm.contracts mapping are asserted to be distinct in our smt encoding. This allows us to support symbolic addresses in a fully static manner (i.e. we do not currently need to make any extra smt queries when looking up storage for a symbolic address).

Mutable Memory & ST

We now use a mutable representation of memory if it is currently completely concrete. This is a significant performance improvement, and fixed a particulary egregious memory leak. It does entail the use of the ST monad, and introduces a new type parameter to the VM type that tags a given instance with it's thread local state. Library users will now need to either use the ST moand and runST or stToIO to compose and sequence vm executions.

GHC 9.4

Hevm is now built with ghc9.4. While earlier compiler versions may continue to work for now, they are no longer explicitly tested or supported.

Other

[0.51.3] - 2023-07-14

Fixed

Changed

Added

[0.51.2] - 2023-07-11

Fixed

Changed

Added

[0.51.1] - 2023-06-02

Fixed

Changed

[0.51.0] - 2023-04-27

Added

Changed

Fixed

Fixed

[0.50.5] - 2023-04-18

Changed

Fixed

[0.50.4] - 2023-03-17

Fixed

Changed

Added

[0.50.3] - 2023-02-17

Fixed

Added

Changed

[0.50.2] - 2023-01-06

Fixed

[0.50.1] - 2022-12-29

Fixed

Changed

[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 docs.

Removed

The following cli commands have been removed:

[0.49.0] - 2021-11-12

Added

Changed

Fixed

[0.48.1] - 2021-09-08

Added

Changed

Fixed

0.48.0 - 2021-08-03

Changed

0.47.0 - 2021-07-01

Added

Changed

Fixed

0.46.0 - 2021-04-29

Added

Fixed

0.45.0 - 2021-03-22

Added

Fixed

Changed

0.44.1 - 2020-02-02

Changed

0.44.0 - 2020-01-26

Added

Fixed

Changed

0.43.2 - 2020-12-10

Changed

0.43.1 - 2020-12-10

Changed

Fixed

0.43.0 - 2020-11-29

Added

Changed

0.42.0 - 2020-10-31

Changed

Added

0.41.0 - 2020-08-19

Changed

Added

0.40 - 2020-07-22

Changed

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

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

Added

New cli commands:

See the README for details on usage.

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

Removed

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

0.39 - 2020-07-13

0.38 - 2020-04-23

0.37 - 2020-03-24

0.36 - 2020-01-07

0.35 - 2019-11-02

0.34 - 2019-08-28

0.33 - 2019-08-06

0.32 - 2019-06-14

0.31 - 2019-05-29

0.30 - 2019-05-09

0.29 - 2019-04-03

0.28 - 2019-03-22

0.27 - 2019-02-06

0.26 - 2019-02-05

0.25 - 2019-02-04

0.24 - 2019-01-23

0.23 - 2018-12-12

0.22 - 2018-11-13

0.21 - 2018-10-29

0.20 - 2018-10-27

0.19 - 2018-10-09

0.18 - 2018-10-09

0.17 - 2018-10-05

0.16 - 2018-09-19

[0.15] - 2018-05-09

[0.14.1] - 2018-04-17

[0.14] - 2018-03-08

[0.13] - 2018-02-28

[0.12.3] - 2017-12-19

[0.12.2] - 2017-12-17

[0.12.1] - 2017-11-28

0.12 - 2017-11-14

0.11.5 - 2017-11-14

0.11.4 - 2017-11-12

0.11.3 - 2017-11-08

0.11.2 - 2017-11-04

0.11.1 - 2017-11-02

0.11 - 2017-10-31

0.10.9 - 2017-10-23

0.10.7 - 2017-10-19

0.10.6 - 2017-10-19

0.10.5 - 2017-10-17

0.10 - 2017-10-10

0.9.5 - 2017-10-06

0.9 - 2017-09-29

0.8.5 - 2017-09-22

0.8 - 2017-09-21

0.7 - 2017-09-07

0.6.5 - 2017-09-01

0.6.1 - 2017-08-03

0.6 - 2017-08-03

0.5 - 2017-08-02

0.4 - 2017-07-31

0.3.2 - 2017-06-17

0.3.0 - 2017-06-14

0.2.0 - 2017-06-13

0.1.0.1 - 2017-03-31

0.1.0.0 - 2017-03-29