Bot releases are visible (Hide)
--root
option for the test
subcommandhevm test
now has a num-solvers
parameter that controls how many solver instances to spawn--num-cex-fuzz
createFork
, selectFork
, and activeFork
--incremental
flag to work properly in abstraction-refinement modePublished by github-actions[bot] 12 months ago
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.
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.
vm.deal
vm.assume
(this is semantically identical to using require
, but does simplify thecheck
prefix now recognized for symbolic testshevm test
now takes a --number
argument to specify which block should be used when making rpc queriessolidity 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.
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:
--cache
/ --state
flags)DAPP_TEST
variables are no longer observed--initial-storage
flag no longer accepts a concrete prestore (valid values are now Empty
or Abstract
)This release also includes many small bugfixes:
test
now falls back to displaying an unecoded bytestring for calldata when the model returned by the solver has a different length the length of the arguments in the test signature.vm.prank
now works correctly when passed a symbolic addressforge build
if it is availableAdding 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).
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.
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.
UnexpectedSymbolicArg
.evalProp
is renamed to simplifyProp
for consistencywriteWord
function was possible in case offset
was close to 2^256. Fixed.VMOpts
no longer takes an initial store, and instead takes a baseState
EmptyBase
or AbstractBase
. This controls whetherCREATE
/CREATE2
have zero initialized storage.Published by github-actions[bot] over 1 year ago
-f debug
to add debug flags to cabal/GHCPublished by github-actions[bot] over 1 year ago
hevm version
prove_
testsPublished by github-actions[bot] over 1 year ago
out
directoriesPublished by github-actions[bot] over 1 year ago
hevm
can now execute unit tests in foundry projects. Just run hevm test
from the root of a foundry repo, and all unit tests will be executed (including prove tests).prove
testshevm dapp-test
has been replaced with hevm test --project-type DappTools
.hevm test
no longer supports parsing solidity output in the combined json format.--ask-smt-iterations
has been changed to 1--max-iterations
is respected in cases where path conditions have become inconsistent--max-iterations
is now respected for loops with a concrete branch conditionPublished by github-actions[bot] over 1 year ago
--storage-model
parameter has been replaced with --initial-storage
--smttimeout
argument now expects a value in seconds not millisecondshevm symbolic
now searches only for user defined assertions by defaultprank
cheatcode now transfers value from the correct addressEVM.Debug.srcMapCodePos
Published by github-actions[bot] over 1 year ago
--solvers
cli option is now respected (previously we always used Z3)equivalence
command now fails with the correct status code when counterexamples are foundequivalence
command now respects the given --sig
argumentSGT
opcodeequivalence
command now pretty prints discovered counterexampleshevm
library can now be built on Windows systems.equivalence
can now be checked for fully or partially concrete calldataPublished by github-actions[bot] over 1 year ago
hevm symbolic
exits with status code 1
if counterexamples or timeouts are foundprank(address)
that sets msg.sender
to the specified address for the next call.Published by github-actions[bot] almost 2 years ago
hevm exec
no longer fails with hevm: No match in record selector smttimeout
gas
, gaslimit
, priorityfee
, and gasprice
cli options are now respectedPublished by github-actions[bot] almost 2 years ago
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.
The following cli commands have been removed:
abiencode
rlp
flatten
strip-metadata