0.54.2

[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