0.50.4

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

release/0.50.3

Fixed

• hevm symbolic exits with status code 1 if counterexamples or timeouts are found

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

0.50.2

Fixed

• Arithmetic overflow in concrete SAR edge case (#163)
• Unexpected abstract term application during fully concrete execution (#163)

0.50.1

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, #152)

0.50.0

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:

• abiencode
• rlp
• flatten
• strip-metadata