From 62049c52f7e0bdd9516234fe760065291579c925 Mon Sep 17 00:00:00 2001 From: David Terry Date: Thu, 26 Oct 2023 13:37:50 +0200 Subject: [PATCH] prepare 0.52.0 --- CHANGELOG.md | 107 +++++++++++++++++++++++++++++++++++---------------- hevm.cabal | 2 +- 2 files changed, 75 insertions(+), 34 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 423f7ff0f..b3262586c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,16 +5,63 @@ 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). -## Unreleased +## [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 -- `vm.prank` now handles symbolic addresses -- added `vm.deal` cheatcode -- added `vm.assume` cheatcode +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 + +- Support for `vm.deal` +- Support for `vm.assume` (this is semantically identical to using `require`, but does simplify the + process of porting exisitng fuzz tests to be symbolic) +- the `check` prefix now recognized for symbolic tests +- `hevm test` now takes a `--number` argument to specify which block should be used when making rpc queries + +## 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: + +- The visual debugger has been removed +- All concrete ds-test executors have been removed (i.e. plain, fuzzer, invariant) +- Rpc caching and state serialization has been removed (i.e. all `--cache` / `--state` flags) +- The various `DAPP_TEST` variables are no longer observed +- The `--initial-storage` flag no longer accepts a concrete prestore (valid values are now `Empty` or `Abstract`) ## Fixed +This release also includes many small bugfixes: + - CopySlice wraparound issue especially during CopyCallBytesToMemory - Contracts deployed during symbolic execution are created with an empty storage (instead of abstract in previous versions) - EVM.Solidity.toCode to include contractName in error string @@ -26,24 +73,34 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - `vm.prank` now works correctly when passed a symbolic address - storage layout information will now be parsed from the output of `forge build` if it is available -## Changed +## API Changes -- Less noisy console output during tracing +### Reworked Storage Model / Symbolic Addresses -### UI +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). -- `check` prefix now recognized for symbolic tests -- solidity tests no longer consider reverts to be a failure, and check only for the ds-test failed bit or unser defined assertion failures (i.e. `Panic(0x01)`). A positive (i.e. non `proveFail`) test with no rechable assertion violations that does not have any succesful branches will still be considered a failure. -- `test` now takes a `--number` argument to specify which block should be used when making rpc queries -- The `--initial-storage` flag no longer accepts a concrete prestore (valid values are now `Empty` or `Abstract`) -- The visual debugger has been removed -- All concrete ds-test executors have been removed (i.e. plain, fuzzer, invariant) -- Rpc caching and state serialization has been removed (i.e. all `--cache` / `--state` flags) -- The various `DAPP_TEST` variables are no longer observed +### 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 -### Internals +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 -- Contract addresses can now be fully symbolic - Contract balances can now be fully symbolic - Contract code can now be fully abstract. Calls into contracts with unknown code will fail with `UnexpectedSymbolicArg`. - Run expression simplification on branch conditions @@ -55,22 +112,6 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - `evalProp` is renamed to `simplifyProp` for consistency - Mem explosion in `writeWord` function was possible in case `offset` was close to 2^256. Fixed. - BufLength was not simplified via bufLength function. Fixed. - -## API Changes - -Support for fully symbolic contract addresses required some very extensive changes to our storage model: - -- A new type has been added to `Expr` that can represent concrete or symbolic addresses -- The contracts mapping is now keyed on terms of type `Expr EAddr` (instead of `Addr`) -- Storage has been moved from a global storage mapping in `vm.env` into a per contract one -- Terms of type `Expr Storage` now model a per contract store (i.e. W256 -> W256) -- A new type has been added to `Expr`: `EContract`. It has one constructor that - is a simplified view of the full `Contract` typed used in the `VM` storage mapping. -- `Success` nodes in `Expr End` now return a mapping from `Expr EAddr` to `Expr EContract` instead of an `Expr Storage`. -- Nonces are now modeled as a `Maybe Word64` (where `Nothing` can be read as "symbolic"). -- `Expr Storage` no longer has an `EmptyStore` constructor (use `ConcreteStore mempty` instead) -- Contract balances are now fully symbolic -- Contract code can now be unknown. There is a new constructor for `ContractCode` to represent this (`UnknownCode`) - `VMOpts` no longer takes an initial store, and instead takes a `baseState` which can be either `EmptyBase` or `AbstractBase`. This controls whether storage should be inialized as empty or fully abstract. Regardless of this diff --git a/hevm.cabal b/hevm.cabal index 2ebc62b61..bfd8ff855 100644 --- a/hevm.cabal +++ b/hevm.cabal @@ -2,7 +2,7 @@ cabal-version: 3.0 name: hevm version: - 0.51.3 + 0.52.0 synopsis: Symbolic EVM Evaluator homepage: