Skip to content

hevm 0.58.0

Latest
Latest

Choose a tag to compare

View all tags
@msooseth msooseth released this 29 Jun 12:37
release/0.58.0
8963e3d
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

hevm 0.58.0 introduces several notable features:

  • More cheat codes: additional implementations matching Foundry's documentation (etch, expectRevert, the assertApprox* family), plus string-message variants of existing assertions where the trailing string is an optional failure description shown when the assertion fails.
  • State merging: in some cases this collapses an exponential number of explored states into a linear number, which can yield large speedups in proofs.
  • Concurrent solving: solvers now run in their own thread and report counterexamples as soon as they're found, so you no longer have to wait for the full run to finish before seeing them.
  • Calldata concretization: dynamic arrays in calldata can now be concretized up to N values, making it possible to prove functions that take dynamic arrays as input, bounded to a fixed size.
  • Improved Osaka support: the new CLZ (count leading zeros) opcode is now implemented, and the test suite draws Osaka tests from ethereum/execution-spec-tests.

Added

  • RPC retry with exponential backoff and a shared cooldown across workers, so transient
    network errors and rate limits (e.g. HTTP 429) no longer abort symbolic execution
  • Support for a subset of the expectRevert family of foundry cheatcodes:
    • expectRevert()
    • expectRevert(bytes)
    • expectRevert(bytes4)
    • expectRevert(address)
    • expectRevert(bytes4,address)
    • expectRevert(bytes,address)
    • expectPartialRevert(bytes4)
    • expectPartialRevert(bytes4,address)
  • Support for Foundry/Hardhat console.log — calls to the console address are intercepted and decoded in traces
  • Source location info (file, line, code snippet) is now shown in state merge debug messages
  • New opcode: CLZ
  • New POr/PAnd/PImpl/Or/And simplification rules
  • Support for --early-abort flag that aborts symbolic execution as soon as a counterexample is found
  • Support for vm.etch(address, bytecode) cheatcode to set the code of a contract at a given address
  • State merging via speculative execution of both branches of a JUMPI, joining the
    resulting states whenever possible. Amount of speculative execution is
    controlled via merge-max-budget
  • Missing simplifications for Eq, Mod, SMod, XOR, SHL, SHR, and Or
  • A few more simplification rules around Eq, SHL/SHR, Sub+Add combos, and Xor
  • Symbolic execution now supports dynamic bytes/string calldata arguments,
    with their length bounded by --max-dyn-size (default 64). When such a bound
    is applied the result carries a program-wide [CAVEAT] noting that
    counterexamples requiring longer inputs may be missed (rather than a per-path
    Partial)
  • readWord disjointness rule for WriteWord (Add (Lit c) X) … with bounded X.

Changed

  • Simplifier now rewrites Mul(-1, x) and ~x + 1 to Sub(0, x)
  • AbiFunction and AbiBytes parser is now more strict
  • We now check length of AbiArrayDynamic and don't crash in case it's too large
  • SMT queries now run in separate processes, which allows us to better manage
    timeouts and memory usage by the SMT solver.
  • We now allow limiting the SMT solver's memory usage via --smt-memory (in MB).
  • The option --smttimeout is now called --smt-timeout for consistency with other
    options.
  • We now abort VM run on a failed assume.
  • Removed SHA256 from the Expr since it was not being used
  • When doing CopySlice of exactly one concrete byte, we now correctly simplify

What's Changed

  • Fix Windows build failure by @elopez in #960
  • ci: add arm64-linux release build by @charles-cooper in #961
  • CI: Use action to clean up space in more jobs by @blishko in #967
  • --early-abort flag to abort symbolic execution only by @msooseth in #965
  • CI: Add build on arm linux by @blishko in #966
  • SymEx: Introduce a type synonym and noop helper for path handler by @blishko in #968
  • Test: Initial refactoring of our large monolithic test module by @blishko in #972
  • Implement etch() cheatcode + Support Bytes dynamic type by @msooseth in #971
  • Test: Collect more Expr/Prop related tests to a dedicated test module by @blishko in #975
  • [DRAFT] Better function ABI parsing + enforce Bytes is >=1 && <=32 by @msooseth in #974
  • Test: Small cleanup by @blishko in #976
  • Small fix in --debug printing: it should say "potential" cex by @msooseth in #977
  • Solidity: Consolidate solc helpers by @blishko in #978
  • Solvers.hs should run separate processes for each query by @msooseth in #964
  • Add support for etching fresh addresses by @elopez in #982
  • SMT: Do not mix MaybeT IO a and IO (Maybe a) computations by @blishko in #983
  • Test: Add framework for concrete execution test by @blishko in #984
  • Solvers: Do not specify bv-solver option for bitwuzla by @blishko in #987
  • EVM: Fix coinbase reward by @blishko in #989
  • Fix sender extraction for EIP-155 transactions by @elopez in #990
  • Replace cryptonite with crypton by @elopez in #991
  • EVM: fix MCOPY stack corruption on out-of-gas in nested calls by @elopez in #992
  • EVM: EIP-1153: preserve transient storage in replaceCode by @elopez in #993
  • Test: Move more Expr tests to dedicated module by @blishko in #994
  • Cheat: Abort VM on failed assume by @blishko in #986
  • Move from ethereum/tests to ethereum/execution-spec-tests by @elopez in #988
  • Test: Refactor and adjust property tests for Expr/Prop by @blishko in #997
  • Switch tests to Osaka by @elopez in #998
  • Test: Update RPC API by @blishko in #1001
  • Tests: Signal failure when we inadvertently lose some ethereum tests by @blishko in #999
  • EVM: Introduce deafult VMOpts by @blishko in #1003
  • Nix: replace fetchTarball with fetchzip by @elopez in #1002
  • Implement CLZ opcode by @elopez in #940
  • More refactoring of Expr/Prop related tests by @blishko in #1004
  • Don't crash on large array by @msooseth in #981
  • Test: Increase gas limit lower bound in fuzz tests by @blishko in #1006
  • SymExec: Reuse existing functionality by @blishko in #1011
  • Tests: Move equivalence tests to dedicated module (and simplify) by @blishko in #1008
  • Fixing misleading comment by @msooseth in #1012
  • State merging by @gustavo-grieco in #973
  • CI: Unify solidity version by @blishko in #1015
  • Test: Small cleanup in equivalence checking of yul optimizations by @blishko in #1013
  • Test: Enable even more yul equivalence tests by @blishko in #1018
  • Add 2 more Expr simplifications related to negative numbers, enable NOT concretization by @msooseth in #1017
  • More prop and expr simplification rules by @msooseth in #1020
  • Test: Fix processing of yul object files in equivalence checking by @blishko in #1021
  • Add missing simplifications, add tests for all concretizations, remove SHA256 by @msooseth in #1019
  • New simplifications: Eq, SHL/SHR, Sub+Add combos, and Xor by @msooseth in #1022
  • Expr: Add another simplification rule for CopySlice by @blishko in #1023
  • Test: Less verbose test runs by @blishko in #1024
  • Test: Move more tests to dedicated modules by @blishko in #1026
  • SymExec: Fix dumping formatted expression to file by @blishko in #1025
  • Compare solidity repo and solc versions between CI jobs by @elopez in #1030
  • flake: keep only part of the execution spec test fixture by @elopez in #1029
  • Test: Small cleanup in storage tests by @blishko in #1027
  • Test: Move more tests to dedicated module by @blishko in #1031
  • Test: Move more symbolic execution tests by @blishko in #1032
  • Implement EIP-{7623,7823,7825,7883} by @elopez in #1028
  • Test: Add tests for div and mod operations by @blishko in #1034
  • Source code lines displayed during state merging by @msooseth in #1033
  • Expr: Fix unsigned wrapping bugs in expression simplifier by @elopez in #1036
  • Expr: Do not use readWordFromBytes outside of Expr module by @blishko in #1037
  • Expr: Make Expr exports explicit by @blishko in #1038
  • Test: Move Foundry tests to a dedicated module by @blishko in #1040
  • Test: Fix issue with how we run Foundry tests by @blishko in #1041
  • Test: Disallow FFI in forge tests by default by @blishko in #1042
  • ci: check-dependencies: add go-ethereum dependency check by @elopez in #1046
  • Optional Echidna compatibility check as a Github Action by @gustavo-grieco in #1039
  • EVM: optimize OpSwap to use direct list manipulation by @elopez in #1044
  • Tweak default RTS options by @elopez in #1047
  • EVM: inline getOp for execution speedup by @elopez in #1043
  • libff: fix header installation with CMake 4.3+ by @elopez in #1053
  • Added two variants of assertApproxEqAbs by @gustavo-grieco in #1054
  • fix for issue #895: source not found for Panic traces by @gustavo-grieco in #1056
  • Parse correctly enumerated types by @gustavo-grieco in #1055
  • Use RPC key from github secrets by @gustavo-grieco in #1060
  • Support for hardhat/foundry console output by @gustavo-grieco in #1050
  • Expect revert by @d-xo in #1061
  • Add RPC retry with exponential backoff and shared cooldown by @msooseth in #1062
  • Expr: sound disjointness rule for readWord/WriteWord with bounded offset by @msooseth in #1065
  • Fix pranked CREATE2 address preimage by @forkforkdog in #1069
  • Add assertApproxEqRel cheatcode (uint256 and int256) by @gustavo-grieco in #1067
  • Fix copyslice in case the copy is exactly ONE byte. by @msooseth in #1071
  • Allow to concretize dynamic arrays in calldata up to N values by @gustavo-grieco in #1057
  • Revert "ci: add arm64-linux release build" by @elopez in #1077

New Contributors

Full Changelog: release/0.57.0...release/0.58.0

Contributors

elopez, charles-cooper, and 5 other contributors
Assets 5
Loading