Added

• When a staticcall is made to a contract that does not exist, we overapproximate
  and return symbolic values
• More simplification rules for Props
• JoinBytes simplification rule
• New simplification rule to help deal with abi.encodeWithSelector
• More simplification rules for Props
• Using the SMT solver to get a single concrete value for a symbolic expression
  and continue running, whenever possible
• STATICCALL abstraction is now performed in case of symbolic arguments
• Better error messages for JSON parsing
• Multiple solutions are allowed for a single symbolic expression, and they are
  generated via iterative calls to the SMT solver for quicker solving
• Aliasing works much better for symbolic and concrete addresses
• Constant propagation for symbolic values
• Allow reading bytecode via --code-file or --code-a-file/--code-b-file. Strips
  \n, spaces, and ignores leading 0x to make it easier to use via e.g.
  jq '.deplayedBytecode.object file.json > file.txt' to parse Forge JSON output
  This alleviates the issue when the contract is large and does not fit the command line
  limit of 8192 characters
• Two more simplification rules: ReadByte & ReadWord when the CopySlice
  it is reading from is writing after the position being read, so the
  CopySlice can be ignored
• More simplification rules that help avoid symbolic copyslice in case of
  STATICCALL overapproximation
• Test to make sure we don't accidentally overapproximate a working, good STATICCALL
• Allow EXTCODESIZE/HASH, BALANCE to be abstracted to a symbolic value.
• Allow CALL to be extracted in case --promise-no-reent is given, promising
  no reentrancy of contracts. This may skip over reentrancy vulnerabilities
  but allows much more thorough exploration of the contract
• Allow controlling the max buffer sizes via --max-buf-size to something smaller than 2**64
  so we don't get too large buffers as counterexamples
• More symbolic overapproximation for Balance and ExtCodeHash opcodes, fixing
  CodeHash SMT representation
• Add deployment code flag to the equivalenceCheck function
• PNeg + PGT/PGEq/PLeq/PLT simplification rules
• We no longer dispatch Props to SMT that can be solved by a simplification
• Allow user to change the verbosity level via --verb. For the moment, this is only to
  print some warnings related to zero-address dereference and to print hemv test's
  output in case of failure
• Simple test cases for the CLI
• Allow limiting the branch depth and width limitation via --max-depth and --max-width
• When there are zero solutions to a multi-solution query it means that the
  currently executed branch is in fact impossible. In these cases, unwind all
  frames and return a Revert with empty returndata.
• More rewrite rules for PEq, PNeg, missing eqByte call, and distributivity for And
• Allow changing of the prefix from "prove" via --prefix in test mode
• More complete simplification during interpretation
• SMT-based resolving of addresses now works for delegatecall and staticcall
  opcodes as well
• UNSAT cache is now in Solvers.hs and is therefore shared across all threads.
  Hence, it is now active even during branch queries.
• Rewrite rule to deal with some forms of argument packing by Solidity
  via masking
• More rewrite rules for (PLT (Lit 0) _) and (PEq (Lit 1) _)
• Simplification can now be turned off from the cli via --no-simplify
• When doing Keccak concretization, and simplification is enabled,
  we do both until fixedpoint
• When gathering Keccak axioms, we simplify the bytestring that
  the keccak is applied to
• More rewrite rules for MulMod, AddMod, SHL, SHR, SLT, and SignExtend
• PLEq is now concretized in case it can be computed
• More SignExtend test cases
• Rewrite rules to deal with specific exponentiation patterns
• Added missing simplification and concretization of the SAR instruction

Fixed

• We now try to simplify expressions fully before trying to cast them to a concrete value
  This should improve issues when "Unexpected Symbolic Arguments to Opcode" was
  unnecessarily output
• Not all testcases ran due to incorrect filtering, fixed
• Removed dead code related to IOAct in the now deprecated and removed debugger
• Base case of exponentiation to 0 was not handled, leading to infinite loop
• Better exponential simplification
• Dumping of END states (.prop) files is now default for --debug
• When cheatcode is missing, we produce a partial execution warning
• Size of calldata can be up to 2**64, not 256. This is now reflected in the documentation
• We now have less noise during test runs, and assert more about symbolic copyslice tests
• CopySlice rewrite rule is now less strict while still being sound
• Assumptions about reading from buffer after its size are now the same in all cases.
  Previously, they were too weak in case of reading 32 bytes.
• The equivalence checker now is able to prove that an empty store is
  equivalent to a store with all slots initialized to 0.
• Equivalence checking was incorrectly assuming that overapproximated values
  were sequentially equivalent. We now distinguish these symbolic values with
  A- and B-
• Buffer of all zeroes was interpreted as an empty buffer during parsing SMT model.
  The length of the buffer is now properly taken into account.
• It was possible to enter an infinite recursion when trying to shrink a buffer found by
  the SMT solver. We now properly detect that it is not possible to shrink the buffer.
• Pretty printing of buffers is now more robust. Instead of throwing an internal error,
  we now try best to print everything we can, and print an appropriate error message
  instead of crashing.
• We no longer produce duplicate SMT assertions regarding concrete keccak values.
• Ord is now correctly implemented for Prop.
• Signed and unsigned integers have more refined ranges.
• Symbolic interpretation of assertGe/Gt/Le/Lt over signed integers now works correctly.
• SignExtend is now correctly being constant-folded
• Some of our property-based testing was ineffective because of inadvertent
  simplification happening before calling the SMT solver. This has now been fixed.
• When pranking an address, we used the non-pranked address' nonce
  to calculate the new address. This was incorrect, and lead to address clash,
  as the nonce was never incremented.
• We only report FAIL in test mode for assertion failures that match the
  string prefix "assertion failed", or match function selector Panic(uint256)
  with a parameter 0x1. Previously, require(a==b, "reason") was a cause for
  FAIL in case a!=b was possible. This has now been fixed.
• Out of bounds reads could occur in Haskell when trying to determine
  valid jump destinations. This has now been fixed.

Changed

• Warnings now lead printing FAIL. This way, users don't accidentally think that
  their contract is correct when there were cases/branches that hevm could not
  fully explore. Printing of issues is also now much more organized
• Expressions that are commutative are now canonicalized to have the smaller
  value on the LHS. This can significantly help with simplifications, automatically
  determining when (Eq a b) is true when a==b modulo commutativity
• hevm test's flag --verbose is now --verb, which also increases verbosity
  for other elements of the system
• Add --arrays-exp to cvc5 options.
• We now use Options.Applicative and a rather different way of parsing CLI options.
  This should give us much better control over the CLI options and their parsing.
• block.number can now be symbolic. This only affects library use of hevm
• Removed --smtoutput since it was never used
• We now build with -DCMAKE_POLICY_VERSION_MINIMUM=3.5 libff, as cmake deprecated 3.5
• CheckSatResult has now been unified with ProofResult via SMTResult
• If counterexample would require a buffer that's larger than 1GB, we abandon
  shrinking it.
• If solver is not able to solve a query while attempting to shrink the model, we
  abandon the attempt gracefully instead of crashing with internal error.
• Buffers are now handled more lazily when inspecting a model, which avoids some
  unnecesary internal errors.
• EVM memory is now grown on demand using a 2x factor, to avoid repeated smaller
  increases which hurt concrete execution performance due to their linear cost.
• The concrete MCOPY implementation has been optimized to avoid freezing the whole
  EVM memory.
• We no longer accept check as a prefix for test cases by default.
• The way we print warnings for symbolic mode now matches that of test mode.

PRs merged

• Adding a note about prank and delegatecall by @msooseth in #623
• There is no interactive debugger by @msooseth in #627
• Cleanups in preparation of GHC 9.8 by @elopez in #612
• Fixing missing concKeccakSimpExpr for wordToAddr, maybeLitByte, etc. by @msooseth in #619
• More Prop simplification rules by @msooseth in #628
• Allow dealing with abi.encodeWithSelector by @msooseth in #625
• Use the SMT solver to convert symbolic to concrete value(s) by @msooseth in #629
• Overapproximate staticcall in case we can't resolve callee by @msooseth in #620
• Removing IOAct which was not used by @msooseth in #630
• Adding an example using raw bytecodes to equivalence checking tutorial by @msooseth in #635
• Fixing staticcall abstraction, test case search, and commenting out bug with solidity by @msooseth in https://github.com/ethereum/h...

[0.54.2] - 2024-12-12

Changed

• Improved printing of results. Should be more intuitive to understand what hevm found.
• More complete and precise array/mapping slot rewrite, along with a copySlice improvement
• Use a let expression in copySlice to decrease expression size
• The --debug flag now dumps the internal expressions as well
• hevm now uses the forge-std library's way of detecting failures, i.e. through
  reverting with a specific error code unless --assertion-type DSTest is passed
• Default max iterations is 5 now. --max-iters -1 now signals no bound. This change is to match other
  symbolic execution frameworks' default bound and to not go into an infinite loop by default when
  there could be other, interesting and reachable bugs in the code
• Update to GHC version 9.6.5
• Abstraction-refinement is no longer an option, it was never really useful and not well-tested

Added

• More POr and PAnd rules
• Array/Map slot decomposition can be turned off via a flag
• More PEq, PLEq, and PLT rules
• New label cheatcode.
• Updated Bitwuzla to newer version
• New cheatcodes startPrank() & stopPrank()
• ARM64 and x86_64 Mac along with Linux x86_64 static binaries for releases
• Tutorial for symbolic execution
• PAnd props are now recursively flattened
• Double negation in Prop are removed
• Updated forge to modern version, thereby fixing JSON parsing of new forge JSONs
• Fixed RPC fetching of contract data
• Symbolic ABI encoding for tuples, fuzzer for encoder
• Printing Addrs when running symbolic for counterexamples and reachable end states
• Improved symbolic execution tutorial
• More Mod, SMod, Div, and SDiv simplification rules
• Add freshAddresses field in VMOpts so that initial fresh address can be given as input
• Add documentation about limitations and workarounds
• More verbose error messages in case of symbolic arguments to opcode
• Tests to enforce that in Expr and Prop, constants are on the LHS whenever possible
• Support for MCOPY and TSTORE/TLOAD, i.e. EIP 5656 + 1153 + 4788
• All fuzz tests now run twice, once with expected SAT and once with expected UNSAT to check
  against incorrectly trivial UNSAT queries
• Allow --num-solvers option for equivalence checking, use num cores by default
• Preliminary support for multi-threaded Z3
• Skip over SMT generation issues due to e.g. CopySlice with symbolic arguments, and return
  partial results instead of erroring out
• Fix interpreter's MCOPY handling so that it doesn't error out on symbolic arguments
• More desciptive errors in case of a cheatcode issue
• Better and more pretty debug messages
• Many env* cheatcodes are now supported

Fixed

• vm.prank is now respected during calls to create
• concat is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing
  with declare-fun
• CVC5 needs --incremental flag to work properly in abstraction-refinement mode
• cli.hs now uses with-utf8 so no release binary will have locale issues anymore
• Took ideas for simplification rules from "Super-optimization of Smart Contracts" paper by Albert et al.
• Printing panic uint256 as hex, not as int
• Decomposition does not take place when entire states are compared, as that would necessitate
  a different approach.
• initial-storage option of hevm symbolic is respected
• caller option of hevm symbolic is now respected
• Thanks to the new simplification rules, we can now enable more conformance tests
• Multi-threaded running of Tracing.hs was not possible due to IO race. Fixed.
• Fixed multi-threading bug in symbolic interpretation
• Fixed simplification of concrete CopySlice with destination offset beyond destination size
• Fixed a bug in our SMT encoding of reading multiple consecutive bytes from concrete index
• Fixed bug in SMT encoding that caused empty and all-zero byte arrays to be considered equal
  and hence lead to false negatives through trivially UNSAT SMT expressions
• Respect --smt-timeout in equivalence checking
• Fixed the handling of returndata with an abstract size during transaction finalization
• Error handling for user-facing cli commands is much improved
• Fixed call signature generation for test cases
• Fixing prank so it doesn't override the sender address on lower call frames
• Fixed GitHub release action to upload release binaries

Changed

• Minimum distance requirements are now asserted for Keccak function calls. They assert that it's hard to generate two Keccak's that are less than 256 afar.
• Keccak concretization is now done only after all simplifications are performed. This helps with simplification pre-concretization
• Added an IllegalOverflow error in case the system tries to allocate a large amount of memory during
  abstract gas execution but concrete running. In these cases, the interpreter can out-of-heap
  as the only check is that the size allocated is less than $2**{64}$, but that is too large to fit in memory. Now,
  we check more stringently, and still return an IllegalOverflow
• Fixed --root option for the test subcommand

Added

• Optimized smt queries that significantly improve performance when dealing with solidity mappings and arrays
• Support for using Bitwuzla as a solver
• More efficient encoding for failure in ds-test style tests
• Symbolic tests now support statically sized arrays as parameters
• hevm test now has a num-solvers parameter that controls how many solver instances to spawn
• New solc-specific simplification rules that should make the final Props a lot more readable
• Prop is now correctly ordered, better BufLength and Max simplifications of Expr,
  and further solc-specific simplifications of Expr
• Simplify earlier and don't check reachability for things statically determined to be FALSE
• New concrete fuzzer that can be controlled via --num-cex-fuzz
• Partial support for dynamic jumps when the jump destination can be computed
  given already available information
• Added three forking cheatcodes: createFork, selectFork, and activeFork

Fixed

• Traces now correctly perform source mapping to display contract details
• Event traces now correctly display indexed arguments and argument names
• JSON reading of foundry JSONs was dependent on locale and did not work with many locales.
• CVC5 needs --incremental flag to work properly in abstraction-refinement mode

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

• 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 reachable assertion violations that does not have any successful 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 maintenance. 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
• Better cex reconstruction in cases where branches do not refer to all input variables in calldata
• Correctly handle empty bytestring compiled contracts' JSON
• No more false positives when keccak is called with inputs of different sizes
• 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.
• we now generate correct counterexamples for branches where only a subset of input variables are referenced by the path conditions
• 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

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

• 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
• SLoad/SStore simplifications based on assumptions regarding Keccak non-collision&preimage
• Improved Prop simplification
• CopySlice+WriteWord+ConcreteBuf now truncates ConcreteBuf in special cases
• Better simplification of Eq IR elements
• Run a toplevel constant folding reasoning system on branch conditions
• 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.
• 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
  setting contracts that are deployed at runtime via a call to
  CREATE/CREATE2 have zero initialized storage.

Fixed

• Path joining on Windows
• Fixed overflow issue in stripWrites
• Automatic tests are now more reproducible

Changed

• Removed sha3Crack which has been deprecated for keccakEqs

Added

• Added flag -f debug to add debug flags to cabal/GHC

Fixed

• SMT encoding of Expr now has assertions for the range of environment values that are less than word size (256 bits).
• Trace now contains the cheat code calls
• More consistent error messages

Changed

• SMT2 scripts are now being reprocessed to put one sexpr per line. Having sepxrs that span across multiple lines trigers a bug in CVC5.
• Removing long-running tests so we can finish all unit tests in approx 10 minutes on a current-gen laptop CPU
• Added git revision to hevm version

Added

• execution traces are now shown for failed prove_ tests

Fixed

• hevm now gracefully handles missing out directories
• Constraints are correctly propogated to the final output expression during symbolic execution

Changed

• HEVM is now fully compliant with the Shanghai hard fork

Added

• 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).
• A new stack based loop detection heuristic
• Analysis of partial execution traces is now supported
• Stack traces are displayed for counterexamples from prove tests

Changed

• hevm dapp-test has been replaced with hevm test --project-type DappTools.
• hevm test no longer supports parsing solidity output in the combined json format.
• The default value for --ask-smt-iterations has been changed to 1
• The SMT solver is never queried for branch conditions that do not occur in a loop (as determined by the loop detection heuristic)

Fixed

• --max-iterations is respected in cases where path conditions have become inconsistent
• --max-iterations is now respected for loops with a concrete branch condition
• Fixed a bug where underflow was possible when transfering eth

Changed

• The --storage-model parameter has been replaced with --initial-storage
• The --smttimeout argument now expects a value in seconds not milliseconds
• The default smt timeout has been set to 5 minutes
• hevm symbolic now searches only for user defined assertions by default

Fixed

• The prank cheatcode now transfers value from the correct address
• Fixed an off-by-one error in EVM.Debug.srcMapCodePos

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