From a95cc98d1c30a61bd01470ab248cc114223e0453 Mon Sep 17 00:00:00 2001 From: msooseth <99662964+msooseth@users.noreply.github.com> Date: Mon, 9 Dec 2024 16:21:27 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20ethereum?= =?UTF-8?q?/hevm@879a7320952e879f606aa4b721d0ef1ee51929c0=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- equivalence.html | 12 ------------ print.html | 24 ------------------------ searchindex.js | 2 +- searchindex.json | 2 +- test.html | 12 ------------ 5 files changed, 2 insertions(+), 50 deletions(-) diff --git a/equivalence.html b/equivalence.html index f0b3abe2b..987b16d54 100644 --- a/equivalence.html +++ b/equivalence.html @@ -215,18 +215,6 @@

hevm Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive (default: StackBased) - --abstract-arithmetic Use abstraction-refinement for complicated arithmetic - functions such as MulMod. This runs the solver first - with abstraction turned on, and if it returns a - potential counterexample, the counterexample is - refined to make sure it is a counterexample for the - actual (not the abstracted) problem - --abstract-memory Use abstraction-refinement for Memory. This runs the - solver first with abstraction turned on, and if it - returns a potential counterexample, the - counterexample is refined to make sure it is a - counterexample for the actual (not the abstracted) - problem

Symbolically execute both the code given in --code-a and --code-b and try to prove equivalence between their outputs and storages. Extracting bytecode diff --git a/print.html b/print.html index 832e3a410..72cc22578 100644 --- a/print.html +++ b/print.html @@ -1182,18 +1182,6 @@

uint) balances; function prove_add_value(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n} Notice that this function has a bug: the require and the assert both check for <, but the if checks for >, which should instead be >=. Let's see if hevm can find this bug. In order to do that, we have to prepend the function name with prove_, which we did.","breadcrumbs":"Getting Started » Practical Scenario","id":"1","title":"Practical Scenario"},"10":{"body":"Fuzzing tests usually have a set of (sometimes implicit) pre- and postconditions, but the actual action (e.g. function call) is performed by an external entity, the fuzzer. For C/C++ fuzzing, the implicit postcondition is often e.g. that the system does not throw a segmentation fault. For EVM bytecode, postconditions need to be explicit. Let's see an example: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\nimport \"forge-std/Test.sol\"; contract MyContract is Test { uint balance; function test_overflow(uint amt) public { unchecked { balance += amt; } assert(balance >= amt); }\n} This function is easy to break by picking an amt that overflows balance, so that the postcondition balance > amt will not hold. A fuzzer finds this kind of bug very easily. However, fuzzers have trouble finding bugs that are either specifically hidden (e.g. by a malicious developer), or that have a complicated code path towards them. Let's see a simple one: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\nimport \"foge-std/Test.sol\"; contract MyContract is Test { uint balance; function prove_multiply(uint amt, uint amt2) public { require(amt != 1); require(amt2 != 1); require(amt < amt2); uint tmp; tmp = amt * amt2; if (tmp == 119274257) balance = 1337; else balance += tmp; assert(balance >= tmp); }\n} Calling this contract with amt = 9479 and amt2 = 12583 will set the balance to 1337 which is less than amt*amt2, breaking the postcondition. However, a fuzzer, e.g. Echidna will likely not find those numbers, because uint has a potential range of 2**256 and so it'd be looking for a needle in a haystack, when looking randomly. Here's how to run Echidna on the multiplication test: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { // the rest is the same\n} Then run: echidna --test-mode assertion src/multiply-test.sol Echidna will terminate after 50k runs, with all tests passing. Notice that the difference here, compared to the previous example, is that the overflow example has many different inputs that can break the postcondition, whereas here only one can. Hevm finds the bug in both of these functions. This is because hevm (and symbolic execution frameworks in general) try to find the bug via proof-directed search rather than using random inputs. In hevm, we try to prove that there are no inputs to the test case such that given the preconditions, the postconditions can be broken. While trying to construct this mathematical proof, hevm finds a countereexample , an input that breaks the postconditions: $ hevm test\nChecking 1 function(s) in contract src/multiply-test.sol:MyContract\n[RUNNING] prove_multiply(uint256,uint256) [FAIL] prove_multiply(uint256,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_multiply(9479,12583) Checking 1 function(s) in contract src/overflow-test.sol:MyContract\n[RUNNING] prove_overflow(uint256) [FAIL] prove_overflow(uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_overflow(00000000000000000000000000000000000000000000000100000000000000000182dad8c17bd5e89e8043a08ada90a6d5efdee4425f85cb863109783e158ba4fba908a0e6fae6c6b51002)","breadcrumbs":"When to Use » Fuzzing versus Symbolic Execution","id":"10","title":"Fuzzing versus Symbolic Execution"},"11":{"body":"Fuzzers are exceedingly fast and efficient when there are many potential faults with a function/contract, or if the faults are of a type that's easy to search for (e.g. off-by-one). However, they rarely, if ever, find cases where the bug is hidden deep in the branch logic, or needs very specific input parameters. Hence, it is best to use fuzzers at first to find easy-to-find bugs, as fuzzers are very efficient at that. Then, once the tests pass the fuzzer, it is recommended to use a symbolic execution engine such as hevm. hevm is similar to Halmos and Kontrol in its approach. However, it is quite different from static code analysis tools such as Oyente , Slither , and Mythril . While these 3 tools typically use some form of symbolic execution to try to validate their results, their main method of operation is not via symbolic execution, and they can, and do, report false positives. Notice that static code analysis tools can find bugs that the author(s) didn't write a test case for, as they typically have a (large) set of preconfigured test-cases that they can report on, if they can find a way to violate them. Hence, it may be valuable to run static analysis tools alongside symbolic execution tools such as hevm. Finally, SMTChecker may also be interesting to run alongside hevm. SMTChecker is very different from both approaches detailed above. While SMTChecker is capable of reliably finding both reentrancy and loop-related bugs, the tools above can only do so on a best effort basis. Hevm often reports a warning of incompleteness for such problems, while static code analysis tools either report potential positives or may even not discover them at all. Tool Approach Primary Method Notes hevm Symbolic analysis of EVM bytecode Symbolic execution Focuses on exploring all execution possibilities, identifying potential assertion violations, and optimizing gas usage. Can prove equivalence between bytecodes. Halmos Similar to hevm Not specified Approach similar to hevm, but the document does not detail specific methodologies or differences. Kontrol Similar to hevm Not specified Approach similar to hevm, with a focus presumably on symbolic analysis as well, but further details are not provided in the document. Oyente Static code analysis Partial symbolic execution Uses symbolic execution to validate results but primarily relies on static analysis. Can report false positives. Slither Static code analysis Partial symbolic execution Similar to Oyente, uses static analysis as its main method, complemented by symbolic execution for validation. Known for reporting false positives. Mythril Static code analysis Partial symbolic execution Combines static code analysis with symbolic execution for result validation. Like Oyente and Slither, can report false positives. SMTChecker Different from both hevm and static code analysis tools SMT solving Capable of finding reentrancy and loop-related bugs reliably, which other tools might miss or report incompletely. Offers a distinct approach from symbolic execution.","breadcrumbs":"When to Use » Similarities and Differences to Other Tools","id":"11","title":"Similarities and Differences to Other Tools"},"12":{"body":"Symbolic execution in general, and hevm in particular, have a number of known limitations. Many of these limitations can be worked around without too much effort. This document describes some of the most common limitations and workarounds.","breadcrumbs":"Limitations and Workarounds » Limitations and Workarounds","id":"12","title":"Limitations and Workarounds"},"13":{"body":"The most important issue related to symbolic execution is to do with loops and recursion. For example, the following code is hard to deal with in a symbolic context: function loop(uint n) { for(uint i = 0; i < n; i++) { mystate[i]++; }\n} When such a function is called, and n is a symbolic parameter (e.g. parameter to a function prove_, such as prove_correct(uint n)), hevm would need to create a new execution path for each potential value of n, which can be very large. The same principle applies to recursion, where the depth of the recursion may be unbounded or bounded only by a potentially very large number. Hence, hevm only explores loops and recursions up to fixed depth k, a parameter that can be adjusted from the command line via the --max-iterations k parameter. Whenever the limit is hit, hevm warns of the incomplete exploration: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Max Iterations Reached in contract: 0x[...] pc: [...] In general, the workaround suggested is to try to write code without loops, if possible, or to have a limit on the number of iterations. For example, by using max(k,n) instead of n in the loop condition, where k is a fixed number. Unbounded loops are a problem for digital contracts, as they may be forced by an attacker to exhaust gas, thereby potentially e.g. deadlocking the contract. This can lock in (large) funds, which can be a very serious issue. Hence, limiting loop iterations is a good practice in general -- not only for symbolic execution. Best Practices : Try to write code without loops, if possible. Use max(k,n) instead of n in the loop condition, where k is a fixed number. Avoid unbounded loops to prevent potential gas exhaustion attacks","breadcrumbs":"Limitations and Workarounds » Loops and recursion","id":"13","title":"Loops and recursion"},"14":{"body":"Gas is hard to symbolically track, due to certain opcodes, such as SLOAD, having different cost depending on the parameters to the opcode. Many symbolic execution systems, including hevm, solve this by not fully tracking gas. This means that hevm may report that an assertion failure can occur through a particular execution trace, but that trace would cost more to execute than the allowable gas limit. In general, it is possible to check whether the issue can be hit by running the hevm-provided counterexample in a concrete execution setting, thereby filtering out false positives. However, it is strongly advisable to fix potential issues that are only guarded due to gas exhaustion, as they may become exploitable in the future, when gas costs change. Best Practices : Don't rely on gas exhaustion as a security mechanism. Check potential issues by running the hevm-provided counterexample in a concrete execution setting.","breadcrumbs":"Limitations and Workarounds » Gas costs","id":"14","title":"Gas costs"},"15":{"body":"When a symbolic argument is passed to an EVM opcode that hevm cannot deal with symbolically, an error is raised. There are number of such EVM opcodes, for example JUMP, JUMPI, CALL, CALLCODE, DELEGATECALL, STATICCALL, CREATE, CREATE2, SELFDESTRUCT, etc. If any of these are called with an argument that is symbolic, hevm raises an error, such as: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Attempting to transfer eth to a symbolic address that is not present in the state There is no single workaround for this class of issues, as it depends on the specific circumstances of the code. In general, we suggest trying to concretize the call to the code, such that only what is truly needed to be symbolic is left symbolic. For example, you may be able to force partial concrete execution via require() statements, thereby concretizing the potential symbolic value. Similarly, dynamically computed JUMP destinations can be avoided via pre-computed jump tables, etc. Best Practices : Use require() statements to concretize symbolic values Avoid dynamically computed jumps -- use pre-computed jump-tables, if neccesary","breadcrumbs":"Limitations and Workarounds » Symbolic arguments to certain EVM opcodes","id":"15","title":"Symbolic arguments to certain EVM opcodes"},"16":{"body":"Jumping into symbolic code is not supported by hevm. This can happen when, e.g. a function creates a contract based on a symbolic value, and then jumps into the code of that contract. In these cases, you will get a warning like the following: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Encountered a jump into a potentially symbolic code region while executing initcode. pc: [...] jump dst: [...] For these cases, we suggest concretizing the call that creates the contract, such that the bytecode created and later jumped to, is not symbolic.","breadcrumbs":"Limitations and Workarounds » Jumping into symbolic code","id":"16","title":"Jumping into symbolic code"},"17":{"body":"To get an idea about what hevm is, see CAV'24 paper . You can also check out a few presentations by @msooseth .","breadcrumbs":"For hevm Developers » General overview","id":"17","title":"General overview"},"18":{"body":"","breadcrumbs":"For hevm Developers » Debugging","id":"18","title":"Debugging"},"19":{"body":"Haskell offers a way to print messages anywhere in the code with Debug.Trace . The simplest is trace which takes a string and a value and returns the same value while printing the string. For example add x y = trace \"Hello from add!\" (x + y)","breadcrumbs":"For hevm Developers » Printf-style debugging","id":"19","title":"Printf-style debugging"},"2":{"body":"We now need a copy of hevm (see releases ) and the SMT solver z3, which can be installed e.g. with apt-get on ubuntu/debian or homebrew on Mac, and a copy of Foundry : $ sudo apt-get install z3 # install z3\n$ curl -L https://foundry.paradigm.xyz | bash # install foundryup\n$ foundryup # install forge and other foundry binaries\n$ mkdir mytest && cd mytest\n$ wget https://github.com/ethereum/hevm/releases/download/release/0.53.0/hevm-x86_64-linux\n$ chmod +x ./hevm-x86_64-linux\n$ forge init .\n$ cat < src/contract.sol\npragma solidity ^0.8.19;\nimport \"forge-std/Test.sol\"; contract MyContract is Test { mapping (address => uint) balances; function prove_add_value(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n}\nEOF\n$ forge build --ast\n[⠊] Compiling...\n[⠒] Compiling 1 files with 0.8.19\n[⠢] Solc 0.8.19 finished in 14.27ms\nCompiler run successful!","breadcrumbs":"Getting Started » Building","id":"2","title":"Building"},"20":{"body":"hevm uses Tasty framework for running tests, including QuickCheck for property-based testing.","breadcrumbs":"For hevm Developers » Testing","id":"20","title":"Testing"},"21":{"body":"The basic command to run the tests is: cabal run test For development, it might be beneficial to pass devel flag: cabal run -f devel test This should enable parallel compilation and test runs (see the config file hevm.cabal). Additional parameters can be passed to the test runner after --. For example cabal run test -- --help will list all the additional parameters. Some of the interesting options are -p to filter only some of the tests and --quickcheck-tests to control how many tests quickcheck will generate for each property test.","breadcrumbs":"For hevm Developers » Running tests","id":"21","title":"Running tests"},"22":{"body":"There are a few ways to control how many tests Quickcheck will generate per property. By default, it generates 100 tests (satisfying the precondition). This can be controlled by maxSuccess argument passed to Quickcheck, or, in Tasty framework, using localOption (QuickCheckTests ). Passing --quickcheck-tests to the binary will change this value to . This value can be dynamically adjusted for a test group or a specific test. For example, instead of localOption it is possible to use adjustOption for a test group. The following ensures that for the following test group, the maximal value of the QuickCheckTests option is 50 (but if the current value is lower, it will be left unchanged). adjustOption (\\(Test.Tasty.QuickCheck.QuickCheckTests n) -> Test.Tasty.QuickCheck.QuickCheckTests (min n 50)) Similarly, the maxSuccess value can be modified for a single test. The following sets the number of tests generated to 20 for the particular test: testProperty $ withMaxSuccess 20 $ ...","breadcrumbs":"For hevm Developers » On property-based testing","id":"22","title":"On property-based testing"},"23":{"body":"","breadcrumbs":"For hevm Developers » Profiling","id":"23","title":"Profiling"},"24":{"body":"NOTE: Most of the time will likely be spent in the solver, and that will not show up when profiling Haskell application. In order to build the application with profiling information, we need to pass --enable-profiling to cabal. If we want to profile the test suite, we could run cabal run test --enable-profiling -- +RTS -p Note that +RTS means the next arguments will be passed to GHC and -p instructs the program to create a time profile report. This report is written into the .prof file. If we want to pass arguments to our executable, we have to indicate this with -RTS, for example, to profile run of only some tests, we would use cabal run test --enable-profiling -- +RTS -p -RTS -p ","breadcrumbs":"For hevm Developers » Profiling Haskell code","id":"24","title":"Profiling Haskell code"},"25":{"body":"Test cases must be prepended with prove_ and the testing contract must inherit from Test from Forge's standard test library . First, import Test: import {Test} from \"forge-std/Test.sol\"; and then inherit from it via ... is Test. This allows hevm to discover the test cases it needs to run. Like so: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract BadVaultTest is Test { function prove_mytest() { // environment setup, preconditions // call(s) to test // postcondition checks }\n} Once you have written such a test case, you need to compile with forge build --ast (see forge documentation for more details) and then: $ hevm test\nChecking 1 function(s) in contract src/badvault-test.sol:BadVault\n[RUNNING] prove_mytest(uint256) [PASS] prove_mytest(uint256) Here, hevm discovered the test case, and automatically checked it for violations.","breadcrumbs":"Forge std-test tutorial » Forge std-test Usage Tutorial","id":"25","title":"Forge std-test Usage Tutorial"},"26":{"body":"Tests usually need to set up the environment in a particular way, such as contract address, storage, etc. This can be done via Cheat Codes that can change the address of the caller, set block number, etc. See Cheat Codes below for a range of cheat codes supported. Cheat Codes are a standard method used by other tools, such as Foundry , so you should be able to re-use your existing setup. An example setup could be: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract BadVaultTest is Test { MyVault vault; function setUp() public { // Set up environment vault = new BadVault(); address user1 = address(1); vm.deal(user1, 1 ether); vm.prank(user1); vault.deposit{value: 1 ether}(); address user2 = address(2); vm.deal(user2, 1 ether); vm.prank(user2); vault.deposit{value: 1 ether}(); address attacker = address(42); vm.prank(attacker); // call(s) to test // postcondition checks }\n} The postconditions should check the state of the contract after the call(s) are complete. In particular, it should check that the changes that the function applied did not break any of the (invariants)[https://en.wikipedia.org/wiki/Invariant_(mathematics)] of the contract, such as total number of tokens. You can read more about testing and cheat codes in the (Foundry Book)[https://book.getfoundry.sh/forge/cheatcodes] and you can see the hevm-supported cheat codes below .","breadcrumbs":"Forge std-test tutorial » Setting Up Tests","id":"26","title":"Setting Up Tests"},"27":{"body":"When hevm discovers a failure, it prints an example call how to trigger the failure. Let's see the following simple solidity code: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { mapping (address => uint) balances; function prove_single_fail(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n} When compiling our foundry project, we must either always pass the --ast flag to forge build, or, much better, set the ast = true flag in the foundry.toml file: ast = true In case neither --ast was passed, nor ast = true was set in the foundry.toml file, we will get an error such as: Error: unable to parse Foundry project JSON: [...]/out/Base.sol/CommonBase.json Contract: \"CommonBase\" In these cases, issue forge clean and run forge build --ast again. Once the project has been correctly built, we can run hevm test, and get: $ hevm test\nChecking 1 function(s) in contract src/contract-fail.sol:MyContract\n[RUNNING] prove_single_fail(address,uint256) [FAIL] prove_single_fail(address,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_single_fail(0x0000000000000000000000000000000000000000,100) Here, hevm provided us with a calldata, where the receiver happens to be the zero address, and the value sent is exactly 100. This indeed is the boundary condition where the function call fails. The function should have had a >= rather than a > in the if. Notice that in this case, while hevm filled in the address to give a complete call, the address itself is irrelevant, although this is not explicitly mentioned.","breadcrumbs":"Forge std-test tutorial » Understanding Counterexamples","id":"27","title":"Understanding Counterexamples"},"28":{"body":"In test mode, hevm runs with the starting state set to concrete values. This means that with the solidity-generated default constructor of contracts, state variables will be zero, and arrays and mappings will be empty. If you need a different starting state, such as e.g. tokens already distributed to some addresses, you can set that up in the setup phase of your test. This can be done via the beforeTestSetup function, as documented in the Foundry Book . In case you need a symbolic starting state, see the Symbolic execution tutorial . Note that if all you need is a symbolic calldata, then you don't need to run hevm in symbolic mode, you can simply run hevm test and hevm will provide you with a symbolic calldata.","breadcrumbs":"Forge std-test tutorial » Starting State is Always Concrete","id":"28","title":"Starting State is Always Concrete"},"29":{"body":"Hevm assumes that a test case should not always revert. If you have such a test case, hevm will warn you and return a FAIL. For example this toy contract: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { uint256 cntr; function prove_allrevert(uint256 val) public { if(val < 0) { unchecked { cntr = val; } revert(); } else revert(); }\n} When compiled with forge and then ran under hevm with hevm test, hevm returns: Checking 1 function(s) in contract src/contract-allrevert.sol:MyContract\n[RUNNING] prove_allrevert(uint256) [FAIL] prove_allrevert(uint256) Reason: No reachable assertion violations, but all branches reverted Prefix this testname with `proveFail` if this is expected This is sometimes undesirable. In these cases, prefix your contract with proveFail_ instead of prove_: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { uint256 cntr; function proveFail_allrevert_expected(uint256 val) public { if(val < 0) { unchecked { cntr = val; cntr += 1; } revert(); } else revert(); }\n} When this is compiled with forge and then checked with hevm, it leads to: Checking 1 function(s) in contract src/contract-allrevert-expected.sol:MyContract\n[RUNNING] proveFail_allrevert_expected(uint256) [PASS] proveFail_allrevert_expected(uint256) Which is now the expected outcome.","breadcrumbs":"Forge std-test tutorial » Test Cases that Must Always Revert","id":"29","title":"Test Cases that Must Always Revert"},"3":{"body":"Now let's run hevm to see if it finds the bug: $ hevm test --solver z3\nRunning 1 tests for src/contract.sol:MyContract\n[FAIL] prove_add_value(address,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_add_value(0x0000000000000000000000000000000000000000,100)","breadcrumbs":"Getting Started » Finding the Bug","id":"3","title":"Finding the Bug"},"30":{"body":"Since hevm is an EVM implementation mainly dedicated to testing and exploration, it features a set of \"cheat codes\" which can manipulate the environment in which the execution is run. These can be accessed by calling into a contract (typically called Vm) at address 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D, which happens to be keccak(\"hevm cheat code\"), implementing the following methods: Function Description function prank(address sender) public Sets msg.sender to the specified sender for the next call. function startPrank(address sender) public Sets msg.sender to the specified sender until stopPrank() is called. function stopPrank() public Resets msg.sender to the default sender. function deal(address usr, uint amt) public Sets the eth balance of usr to amt. Note that if usr is a symbolic address, then it must be the address of a contract that has already been deployed. This restriction is in place to ensure soundness of our symbolic address encoding with respect to potential aliasing of symbolic addresses. function store(address c, bytes32 loc, bytes32 val) public Sets the slot loc of contract c to val. function warp(uint x) public Sets the block timestamp to x. function roll(uint x) public Sets the block number to x. function assume(bool b) public Add the condition b to the assumption base for the current branch. This functions almost identically to require. For most users, require is preferable. However, in case you wish to understand & modify the internal IR of hevm, you may want to use assume. function load(address c, bytes32 loc) public returns (bytes32 val) Reads the slot loc of contract c. function sign(uint sk, bytes32 digest) public returns (uint8 v, bytes32 r, bytes32 s) Signs the digest using the private key sk. Note that signatures produced via hevm.sign will leak the private key. function addr(uint sk) public returns (address addr) Derives an ethereum address from the private key sk. Note that hevm.addr(0) will fail with BadCheatCode as 0 is an invalid ECDSA private key. function ffi(string[] calldata) external returns (bytes memory) Executes the arguments as a command in the system shell and returns stdout. Expects abi encoded values to be returned from the shell or an error will be thrown. Note that this cheatcode means test authors can execute arbitrary code on user machines as part of a call to dapp test, for this reason all calls to ffi will fail unless the --ffi flag is passed. function createFork(string calldata urlOrAlias) external returns (uint256) Creates a new fork with the given endpoint and the latest block and returns the identifier of the fork. function selectFork(uint256 forkId) external Takes a fork identifier created by createFork and sets the corresponding forked state as active. function activeFork() external returns (uint256) Returns the identifier of the current fork. function label(address addr, string calldata label) external Labels the address in traces","breadcrumbs":"Forge std-test tutorial » Supported Cheat Codes","id":"30","title":"Supported Cheat Codes"},"31":{"body":"Equivalence checking allows to check whether two bytecodes do the same thing under all input circumstances. This allows to e.g. create two functions, one that is known to be good, and another that uses less gas, but is hard to check for correctness. Then, with equivalence checking, one can check whether the two behave the same. The notion of equivalence in hevm is defined as follows. Two contracts are equivalent if for all possible calldata and state, after execution has finished, their observable storage state is equivalent and they return the same value. In particular, the following is NOT checked when checking for equivalence: Gas consumption Events emitted Maximum stack depth Maximum memory usage Note that in the Solidity ABI, the calldata's first 4 bytes are the function selector which decide which function is being called, along with the potential fallback function mechanism. Hence, treating calldata as symbolic covers all possible function calls, including fallback functions. While not all contracts follow the Solidity ABI , since hevm's symbolic equivalence checker does not distinguish between function selector and function parameter bytes in the calldata, it will still correctly check the equivalence of such non-conforming contracts.","breadcrumbs":"Equivalence checking tutorial » Equivalence Checking Tutorial","id":"31","title":"Equivalence Checking Tutorial"},"32":{"body":"Let's see this toy contract, in file contract1.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt; }\n} And this, slightly modified one, in file contract2.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt/2; balances[recv] += amt/2; }\n} Now ask hevm if they are equivalent. First, let's compile both contracts and get their bytecode: bytecode1=$(solc --bin-runtime \"contract1.sol\" | tail -n1)\nbytecode2=$(solc --bin-runtime \"contract2.sol\" | tail -n1) Let's ask hevm to compare the two: $ hevm equivalence \\ --code-a $(solc --bin-runtime \"contract1.sol\" | tail -n1) \\ --code-b $(solc --bin-runtime \"contract2.sol\" | tail -n1)\nFound 90 total pairs of endstates\nAsking the SMT solver for 58 pairs\nReuse of previous queries was Useful in 0 cases\nNot equivalent. The following inputs result in differing behaviours:\n-----\nCalldata: 0xafc2c94900000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000023\nStorage: Addr SymAddr \"entrypoint\": [(0x0,0x10)]\nTransaction Context: TxValue: 0x0 This tells us that with a value of 0x23 being sent, which corresponds to 35, the two are not equivalent. This is indeed the case: one will add 35 div 2 = 17 twice, which is 34, the other will add 35.","breadcrumbs":"Equivalence checking tutorial » Finding Discrepancies","id":"32","title":"Finding Discrepancies"},"33":{"body":"Let's fix the above issue by incrementing the balance by 1 in case it's an odd value. Let's call this contract3.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt/2; balances[recv] += amt/2; if (amt % 2 != 0) balances[recv]++; }\n} Let's check whether this new contract is indeed equivalent: $ hevm equivalence \\ --code-a $(solc --bin-runtime \"contract1.sol\" | tail -n1) \\ --code-b $(solc --bin-runtime \"contract3.sol\" | tail -n1)\nFound 108 total pairs of endstates\nAsking the SMT solver for 74 pairs\nReuse of previous queries was Useful in 0 cases\nNo discrepancies found Hevm reports that the two are now equivalent, even though they clearly don't consume the same amount of gas and have widely different EVM bytecodes. Yet for an outside observer, they behave the same. Notice that hevm didn't simply fuzz the contract and within a given out of time it didn't find a counterexample. Instead, it proved the two equivalent from an outside observer perspective.","breadcrumbs":"Equivalence checking tutorial » Fixing and Proving Correctness","id":"33","title":"Fixing and Proving Correctness"},"34":{"body":"If the contracts have already been compiled into a hex string, you can paste them into files a.txt and b.txt and compare them via: $ hevm equivalence --code-a \"$(= 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); } Let's re-build with forge and check with hevm once again: $ forge build --ast\n[⠰] Compiling...\n[⠔] Compiling 1 files with 0.8.19\n[⠒] Solc 0.8.19 finished in 985.32ms\nCompiler run successful! $ hevm test --solver z3\nRunning 1 tests for src/contract.sol:MyContract\n[PASS] prove_add_value(address,uint256) We now get a PASS. Notice that this doesn't only mean that hevm couldn't find a bug within a given time frame. Instead, it means that there is surely no call to prove_add_value such that our assertion can be violated. However, it does not check for things that it was not asked to check for. In particular, it does not check that e.g. the sender's balance is decremented. There is no such test and so this omission is not detected.","breadcrumbs":"Getting Started » Fixing the Bug","id":"4","title":"Fixing the Bug"},"40":{"body":"Usage: hevm symbolic [--code TEXT] [--calldata TEXT] [--address ADDR] [--caller ADDR] [--origin ADDR] [--coinbase ADDR] [--value W256] [--nonce WORD64] [--gas WORD64] [--number W256] [--timestamp W256] [--basefee W256] [--priority-fee W256] [--gaslimit WORD64] [--gasprice W256] [--create] [--maxcodesize W256] [--prev-randao W256] [--chainid W256] [--rpc TEXT] [--block W256] [--root STRING] [--project-type PROJECTTYPE] [--initial-storage INITIALSTORAGE] [--sig TEXT] [--arg STRING]... [--get-models] [--show-tree] [--show-reachable-tree] [--smttimeout NATURAL] [--max-iterations INTEGER] [--solver TEXT] [--smtdebug] [--assertions [WORD256]] [--ask-smt-iterations INTEGER] [--num-solvers NATURAL] [--loop-detection-heuristic LOOPHEURISTIC] Available options: -h,--help Show this help text --code TEXT Program bytecode --calldata TEXT Tx: calldata --address ADDR Tx: address --caller ADDR Tx: caller --origin ADDR Tx: origin --coinbase ADDR Block: coinbase --value W256 Tx: Eth amount --nonce WORD64 Nonce of origin --gas WORD64 Tx: gas amount --number W256 Block: number --timestamp W256 Block: timestamp --basefee W256 Block: base fee --priority-fee W256 Tx: priority fee --gaslimit WORD64 Tx: gas limit --gasprice W256 Tx: gas price --create Tx: creation --maxcodesize W256 Block: max code size --prev-randao W256 Block: prevRandao --chainid W256 Env: chainId --rpc TEXT Fetch state from a remote node --block W256 Block state is be fetched from --root STRING Path to project root directory (default: . ) --project-type PROJECTTYPE Foundry or CombinedJSON project --initial-storage INITIALSTORAGE Starting state for storage: Empty, Abstract (default Abstract) --sig TEXT Signature of types to decode / encode --arg STRING Values to encode --get-models Print example testcase for each execution path --show-tree Print branches explored in tree view --show-reachable-tree Print only reachable branches explored in tree view --smttimeout NATURAL Timeout given to SMT solver in seconds (default: 300) --max-iterations INTEGER Number of times we may revisit a particular branching point. Default is 5. Setting to -1 allows infinite looping --solver TEXT Used SMT solver: z3 (default), cvc5, or bitwuzla --smtdebug Print smt queries sent to the solver --assertions [WORD256] Comma separated list of solc panic codes to check for (default: user defined assertion violations only) --ask-smt-iterations INTEGER Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1) (default: 1) --num-solvers NATURAL Number of solver instances to use (default: number of cpu cores) --loop-detection-heuristic LOOPHEURISTIC Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive (default: StackBased) Run a symbolic execution against the given parameters, searching for assertion violations. Counterexamples will be returned for any reachable assertion violations. Where an assertion violation is defined as either an execution of the invalid opcode (0xfe), or a revert with a message of the form abi.encodeWithSelector('Panic(uint256)', errCode) with errCode being one of the predefined solc assertion codes defined here . By default hevm ignores assertion violations that result from arithmetic overflow (Panic(0x11)), although this behaviour can be customised via the --assertions flag. For example, the following will return counterexamples for arithmetic overflow (0x11) and user defined assertions (0x01): hevm symbolic --code $CODE --assertions '[0x01, 0x11]' The default value for calldata and caller are symbolic values, but can be specialized to concrete functions with their corresponding flags. One can also specialize specific arguments to a function signature, while leaving others abstract. If --sig is given, calldata is assumed to be of the form suggested by the function signature. With this flag, specific arguments can be instantiated to concrete values via the --arg flag. This is best illustrated through a few examples: Calldata specialized to the bytestring 0xa9059cbb followed by 64 symbolic bytes: hevm symbolic --sig \"transfer(address,uint256)\" --code $(\" --arg 0 --code $( uint) balances; function prove_add_value(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n} Notice that this function has a bug: the require and the assert both check for <, but the if checks for >, which should instead be >=. Let's see if hevm can find this bug. In order to do that, we have to prepend the function name with prove_, which we did.","breadcrumbs":"Getting Started » Practical Scenario","id":"1","title":"Practical Scenario"},"10":{"body":"Fuzzing tests usually have a set of (sometimes implicit) pre- and postconditions, but the actual action (e.g. function call) is performed by an external entity, the fuzzer. For C/C++ fuzzing, the implicit postcondition is often e.g. that the system does not throw a segmentation fault. For EVM bytecode, postconditions need to be explicit. Let's see an example: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\nimport \"forge-std/Test.sol\"; contract MyContract is Test { uint balance; function test_overflow(uint amt) public { unchecked { balance += amt; } assert(balance >= amt); }\n} This function is easy to break by picking an amt that overflows balance, so that the postcondition balance > amt will not hold. A fuzzer finds this kind of bug very easily. However, fuzzers have trouble finding bugs that are either specifically hidden (e.g. by a malicious developer), or that have a complicated code path towards them. Let's see a simple one: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\nimport \"foge-std/Test.sol\"; contract MyContract is Test { uint balance; function prove_multiply(uint amt, uint amt2) public { require(amt != 1); require(amt2 != 1); require(amt < amt2); uint tmp; tmp = amt * amt2; if (tmp == 119274257) balance = 1337; else balance += tmp; assert(balance >= tmp); }\n} Calling this contract with amt = 9479 and amt2 = 12583 will set the balance to 1337 which is less than amt*amt2, breaking the postcondition. However, a fuzzer, e.g. Echidna will likely not find those numbers, because uint has a potential range of 2**256 and so it'd be looking for a needle in a haystack, when looking randomly. Here's how to run Echidna on the multiplication test: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { // the rest is the same\n} Then run: echidna --test-mode assertion src/multiply-test.sol Echidna will terminate after 50k runs, with all tests passing. Notice that the difference here, compared to the previous example, is that the overflow example has many different inputs that can break the postcondition, whereas here only one can. Hevm finds the bug in both of these functions. This is because hevm (and symbolic execution frameworks in general) try to find the bug via proof-directed search rather than using random inputs. In hevm, we try to prove that there are no inputs to the test case such that given the preconditions, the postconditions can be broken. While trying to construct this mathematical proof, hevm finds a countereexample , an input that breaks the postconditions: $ hevm test\nChecking 1 function(s) in contract src/multiply-test.sol:MyContract\n[RUNNING] prove_multiply(uint256,uint256) [FAIL] prove_multiply(uint256,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_multiply(9479,12583) Checking 1 function(s) in contract src/overflow-test.sol:MyContract\n[RUNNING] prove_overflow(uint256) [FAIL] prove_overflow(uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_overflow(00000000000000000000000000000000000000000000000100000000000000000182dad8c17bd5e89e8043a08ada90a6d5efdee4425f85cb863109783e158ba4fba908a0e6fae6c6b51002)","breadcrumbs":"When to Use » Fuzzing versus Symbolic Execution","id":"10","title":"Fuzzing versus Symbolic Execution"},"11":{"body":"Fuzzers are exceedingly fast and efficient when there are many potential faults with a function/contract, or if the faults are of a type that's easy to search for (e.g. off-by-one). However, they rarely, if ever, find cases where the bug is hidden deep in the branch logic, or needs very specific input parameters. Hence, it is best to use fuzzers at first to find easy-to-find bugs, as fuzzers are very efficient at that. Then, once the tests pass the fuzzer, it is recommended to use a symbolic execution engine such as hevm. hevm is similar to Halmos and Kontrol in its approach. However, it is quite different from static code analysis tools such as Oyente , Slither , and Mythril . While these 3 tools typically use some form of symbolic execution to try to validate their results, their main method of operation is not via symbolic execution, and they can, and do, report false positives. Notice that static code analysis tools can find bugs that the author(s) didn't write a test case for, as they typically have a (large) set of preconfigured test-cases that they can report on, if they can find a way to violate them. Hence, it may be valuable to run static analysis tools alongside symbolic execution tools such as hevm. Finally, SMTChecker may also be interesting to run alongside hevm. SMTChecker is very different from both approaches detailed above. While SMTChecker is capable of reliably finding both reentrancy and loop-related bugs, the tools above can only do so on a best effort basis. Hevm often reports a warning of incompleteness for such problems, while static code analysis tools either report potential positives or may even not discover them at all. Tool Approach Primary Method Notes hevm Symbolic analysis of EVM bytecode Symbolic execution Focuses on exploring all execution possibilities, identifying potential assertion violations, and optimizing gas usage. Can prove equivalence between bytecodes. Halmos Similar to hevm Not specified Approach similar to hevm, but the document does not detail specific methodologies or differences. Kontrol Similar to hevm Not specified Approach similar to hevm, with a focus presumably on symbolic analysis as well, but further details are not provided in the document. Oyente Static code analysis Partial symbolic execution Uses symbolic execution to validate results but primarily relies on static analysis. Can report false positives. Slither Static code analysis Partial symbolic execution Similar to Oyente, uses static analysis as its main method, complemented by symbolic execution for validation. Known for reporting false positives. Mythril Static code analysis Partial symbolic execution Combines static code analysis with symbolic execution for result validation. Like Oyente and Slither, can report false positives. SMTChecker Different from both hevm and static code analysis tools SMT solving Capable of finding reentrancy and loop-related bugs reliably, which other tools might miss or report incompletely. Offers a distinct approach from symbolic execution.","breadcrumbs":"When to Use » Similarities and Differences to Other Tools","id":"11","title":"Similarities and Differences to Other Tools"},"12":{"body":"Symbolic execution in general, and hevm in particular, have a number of known limitations. Many of these limitations can be worked around without too much effort. This document describes some of the most common limitations and workarounds.","breadcrumbs":"Limitations and Workarounds » Limitations and Workarounds","id":"12","title":"Limitations and Workarounds"},"13":{"body":"The most important issue related to symbolic execution is to do with loops and recursion. For example, the following code is hard to deal with in a symbolic context: function loop(uint n) { for(uint i = 0; i < n; i++) { mystate[i]++; }\n} When such a function is called, and n is a symbolic parameter (e.g. parameter to a function prove_, such as prove_correct(uint n)), hevm would need to create a new execution path for each potential value of n, which can be very large. The same principle applies to recursion, where the depth of the recursion may be unbounded or bounded only by a potentially very large number. Hence, hevm only explores loops and recursions up to fixed depth k, a parameter that can be adjusted from the command line via the --max-iterations k parameter. Whenever the limit is hit, hevm warns of the incomplete exploration: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Max Iterations Reached in contract: 0x[...] pc: [...] In general, the workaround suggested is to try to write code without loops, if possible, or to have a limit on the number of iterations. For example, by using max(k,n) instead of n in the loop condition, where k is a fixed number. Unbounded loops are a problem for digital contracts, as they may be forced by an attacker to exhaust gas, thereby potentially e.g. deadlocking the contract. This can lock in (large) funds, which can be a very serious issue. Hence, limiting loop iterations is a good practice in general -- not only for symbolic execution. Best Practices : Try to write code without loops, if possible. Use max(k,n) instead of n in the loop condition, where k is a fixed number. Avoid unbounded loops to prevent potential gas exhaustion attacks","breadcrumbs":"Limitations and Workarounds » Loops and recursion","id":"13","title":"Loops and recursion"},"14":{"body":"Gas is hard to symbolically track, due to certain opcodes, such as SLOAD, having different cost depending on the parameters to the opcode. Many symbolic execution systems, including hevm, solve this by not fully tracking gas. This means that hevm may report that an assertion failure can occur through a particular execution trace, but that trace would cost more to execute than the allowable gas limit. In general, it is possible to check whether the issue can be hit by running the hevm-provided counterexample in a concrete execution setting, thereby filtering out false positives. However, it is strongly advisable to fix potential issues that are only guarded due to gas exhaustion, as they may become exploitable in the future, when gas costs change. Best Practices : Don't rely on gas exhaustion as a security mechanism. Check potential issues by running the hevm-provided counterexample in a concrete execution setting.","breadcrumbs":"Limitations and Workarounds » Gas costs","id":"14","title":"Gas costs"},"15":{"body":"When a symbolic argument is passed to an EVM opcode that hevm cannot deal with symbolically, an error is raised. There are number of such EVM opcodes, for example JUMP, JUMPI, CALL, CALLCODE, DELEGATECALL, STATICCALL, CREATE, CREATE2, SELFDESTRUCT, etc. If any of these are called with an argument that is symbolic, hevm raises an error, such as: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Attempting to transfer eth to a symbolic address that is not present in the state There is no single workaround for this class of issues, as it depends on the specific circumstances of the code. In general, we suggest trying to concretize the call to the code, such that only what is truly needed to be symbolic is left symbolic. For example, you may be able to force partial concrete execution via require() statements, thereby concretizing the potential symbolic value. Similarly, dynamically computed JUMP destinations can be avoided via pre-computed jump tables, etc. Best Practices : Use require() statements to concretize symbolic values Avoid dynamically computed jumps -- use pre-computed jump-tables, if neccesary","breadcrumbs":"Limitations and Workarounds » Symbolic arguments to certain EVM opcodes","id":"15","title":"Symbolic arguments to certain EVM opcodes"},"16":{"body":"Jumping into symbolic code is not supported by hevm. This can happen when, e.g. a function creates a contract based on a symbolic value, and then jumps into the code of that contract. In these cases, you will get a warning like the following: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Encountered a jump into a potentially symbolic code region while executing initcode. pc: [...] jump dst: [...] For these cases, we suggest concretizing the call that creates the contract, such that the bytecode created and later jumped to, is not symbolic.","breadcrumbs":"Limitations and Workarounds » Jumping into symbolic code","id":"16","title":"Jumping into symbolic code"},"17":{"body":"To get an idea about what hevm is, see CAV'24 paper . You can also check out a few presentations by @msooseth .","breadcrumbs":"For hevm Developers » General overview","id":"17","title":"General overview"},"18":{"body":"","breadcrumbs":"For hevm Developers » Debugging","id":"18","title":"Debugging"},"19":{"body":"Haskell offers a way to print messages anywhere in the code with Debug.Trace . The simplest is trace which takes a string and a value and returns the same value while printing the string. For example add x y = trace \"Hello from add!\" (x + y)","breadcrumbs":"For hevm Developers » Printf-style debugging","id":"19","title":"Printf-style debugging"},"2":{"body":"We now need a copy of hevm (see releases ) and the SMT solver z3, which can be installed e.g. with apt-get on ubuntu/debian or homebrew on Mac, and a copy of Foundry : $ sudo apt-get install z3 # install z3\n$ curl -L https://foundry.paradigm.xyz | bash # install foundryup\n$ foundryup # install forge and other foundry binaries\n$ mkdir mytest && cd mytest\n$ wget https://github.com/ethereum/hevm/releases/download/release/0.53.0/hevm-x86_64-linux\n$ chmod +x ./hevm-x86_64-linux\n$ forge init .\n$ cat < src/contract.sol\npragma solidity ^0.8.19;\nimport \"forge-std/Test.sol\"; contract MyContract is Test { mapping (address => uint) balances; function prove_add_value(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n}\nEOF\n$ forge build --ast\n[⠊] Compiling...\n[⠒] Compiling 1 files with 0.8.19\n[⠢] Solc 0.8.19 finished in 14.27ms\nCompiler run successful!","breadcrumbs":"Getting Started » Building","id":"2","title":"Building"},"20":{"body":"hevm uses Tasty framework for running tests, including QuickCheck for property-based testing.","breadcrumbs":"For hevm Developers » Testing","id":"20","title":"Testing"},"21":{"body":"The basic command to run the tests is: cabal run test For development, it might be beneficial to pass devel flag: cabal run -f devel test This should enable parallel compilation and test runs (see the config file hevm.cabal). Additional parameters can be passed to the test runner after --. For example cabal run test -- --help will list all the additional parameters. Some of the interesting options are -p to filter only some of the tests and --quickcheck-tests to control how many tests quickcheck will generate for each property test.","breadcrumbs":"For hevm Developers » Running tests","id":"21","title":"Running tests"},"22":{"body":"There are a few ways to control how many tests Quickcheck will generate per property. By default, it generates 100 tests (satisfying the precondition). This can be controlled by maxSuccess argument passed to Quickcheck, or, in Tasty framework, using localOption (QuickCheckTests ). Passing --quickcheck-tests to the binary will change this value to . This value can be dynamically adjusted for a test group or a specific test. For example, instead of localOption it is possible to use adjustOption for a test group. The following ensures that for the following test group, the maximal value of the QuickCheckTests option is 50 (but if the current value is lower, it will be left unchanged). adjustOption (\\(Test.Tasty.QuickCheck.QuickCheckTests n) -> Test.Tasty.QuickCheck.QuickCheckTests (min n 50)) Similarly, the maxSuccess value can be modified for a single test. The following sets the number of tests generated to 20 for the particular test: testProperty $ withMaxSuccess 20 $ ...","breadcrumbs":"For hevm Developers » On property-based testing","id":"22","title":"On property-based testing"},"23":{"body":"","breadcrumbs":"For hevm Developers » Profiling","id":"23","title":"Profiling"},"24":{"body":"NOTE: Most of the time will likely be spent in the solver, and that will not show up when profiling Haskell application. In order to build the application with profiling information, we need to pass --enable-profiling to cabal. If we want to profile the test suite, we could run cabal run test --enable-profiling -- +RTS -p Note that +RTS means the next arguments will be passed to GHC and -p instructs the program to create a time profile report. This report is written into the .prof file. If we want to pass arguments to our executable, we have to indicate this with -RTS, for example, to profile run of only some tests, we would use cabal run test --enable-profiling -- +RTS -p -RTS -p ","breadcrumbs":"For hevm Developers » Profiling Haskell code","id":"24","title":"Profiling Haskell code"},"25":{"body":"Test cases must be prepended with prove_ and the testing contract must inherit from Test from Forge's standard test library . First, import Test: import {Test} from \"forge-std/Test.sol\"; and then inherit from it via ... is Test. This allows hevm to discover the test cases it needs to run. Like so: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract BadVaultTest is Test { function prove_mytest() { // environment setup, preconditions // call(s) to test // postcondition checks }\n} Once you have written such a test case, you need to compile with forge build --ast (see forge documentation for more details) and then: $ hevm test\nChecking 1 function(s) in contract src/badvault-test.sol:BadVault\n[RUNNING] prove_mytest(uint256) [PASS] prove_mytest(uint256) Here, hevm discovered the test case, and automatically checked it for violations.","breadcrumbs":"Forge std-test tutorial » Forge std-test Usage Tutorial","id":"25","title":"Forge std-test Usage Tutorial"},"26":{"body":"Tests usually need to set up the environment in a particular way, such as contract address, storage, etc. This can be done via Cheat Codes that can change the address of the caller, set block number, etc. See Cheat Codes below for a range of cheat codes supported. Cheat Codes are a standard method used by other tools, such as Foundry , so you should be able to re-use your existing setup. An example setup could be: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract BadVaultTest is Test { MyVault vault; function setUp() public { // Set up environment vault = new BadVault(); address user1 = address(1); vm.deal(user1, 1 ether); vm.prank(user1); vault.deposit{value: 1 ether}(); address user2 = address(2); vm.deal(user2, 1 ether); vm.prank(user2); vault.deposit{value: 1 ether}(); address attacker = address(42); vm.prank(attacker); // call(s) to test // postcondition checks }\n} The postconditions should check the state of the contract after the call(s) are complete. In particular, it should check that the changes that the function applied did not break any of the (invariants)[https://en.wikipedia.org/wiki/Invariant_(mathematics)] of the contract, such as total number of tokens. You can read more about testing and cheat codes in the (Foundry Book)[https://book.getfoundry.sh/forge/cheatcodes] and you can see the hevm-supported cheat codes below .","breadcrumbs":"Forge std-test tutorial » Setting Up Tests","id":"26","title":"Setting Up Tests"},"27":{"body":"When hevm discovers a failure, it prints an example call how to trigger the failure. Let's see the following simple solidity code: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { mapping (address => uint) balances; function prove_single_fail(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n} When compiling our foundry project, we must either always pass the --ast flag to forge build, or, much better, set the ast = true flag in the foundry.toml file: ast = true In case neither --ast was passed, nor ast = true was set in the foundry.toml file, we will get an error such as: Error: unable to parse Foundry project JSON: [...]/out/Base.sol/CommonBase.json Contract: \"CommonBase\" In these cases, issue forge clean and run forge build --ast again. Once the project has been correctly built, we can run hevm test, and get: $ hevm test\nChecking 1 function(s) in contract src/contract-fail.sol:MyContract\n[RUNNING] prove_single_fail(address,uint256) [FAIL] prove_single_fail(address,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_single_fail(0x0000000000000000000000000000000000000000,100) Here, hevm provided us with a calldata, where the receiver happens to be the zero address, and the value sent is exactly 100. This indeed is the boundary condition where the function call fails. The function should have had a >= rather than a > in the if. Notice that in this case, while hevm filled in the address to give a complete call, the address itself is irrelevant, although this is not explicitly mentioned.","breadcrumbs":"Forge std-test tutorial » Understanding Counterexamples","id":"27","title":"Understanding Counterexamples"},"28":{"body":"In test mode, hevm runs with the starting state set to concrete values. This means that with the solidity-generated default constructor of contracts, state variables will be zero, and arrays and mappings will be empty. If you need a different starting state, such as e.g. tokens already distributed to some addresses, you can set that up in the setup phase of your test. This can be done via the beforeTestSetup function, as documented in the Foundry Book . In case you need a symbolic starting state, see the Symbolic execution tutorial . Note that if all you need is a symbolic calldata, then you don't need to run hevm in symbolic mode, you can simply run hevm test and hevm will provide you with a symbolic calldata.","breadcrumbs":"Forge std-test tutorial » Starting State is Always Concrete","id":"28","title":"Starting State is Always Concrete"},"29":{"body":"Hevm assumes that a test case should not always revert. If you have such a test case, hevm will warn you and return a FAIL. For example this toy contract: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { uint256 cntr; function prove_allrevert(uint256 val) public { if(val < 0) { unchecked { cntr = val; } revert(); } else revert(); }\n} When compiled with forge and then ran under hevm with hevm test, hevm returns: Checking 1 function(s) in contract src/contract-allrevert.sol:MyContract\n[RUNNING] prove_allrevert(uint256) [FAIL] prove_allrevert(uint256) Reason: No reachable assertion violations, but all branches reverted Prefix this testname with `proveFail` if this is expected This is sometimes undesirable. In these cases, prefix your contract with proveFail_ instead of prove_: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { uint256 cntr; function proveFail_allrevert_expected(uint256 val) public { if(val < 0) { unchecked { cntr = val; cntr += 1; } revert(); } else revert(); }\n} When this is compiled with forge and then checked with hevm, it leads to: Checking 1 function(s) in contract src/contract-allrevert-expected.sol:MyContract\n[RUNNING] proveFail_allrevert_expected(uint256) [PASS] proveFail_allrevert_expected(uint256) Which is now the expected outcome.","breadcrumbs":"Forge std-test tutorial » Test Cases that Must Always Revert","id":"29","title":"Test Cases that Must Always Revert"},"3":{"body":"Now let's run hevm to see if it finds the bug: $ hevm test --solver z3\nRunning 1 tests for src/contract.sol:MyContract\n[FAIL] prove_add_value(address,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_add_value(0x0000000000000000000000000000000000000000,100)","breadcrumbs":"Getting Started » Finding the Bug","id":"3","title":"Finding the Bug"},"30":{"body":"Since hevm is an EVM implementation mainly dedicated to testing and exploration, it features a set of \"cheat codes\" which can manipulate the environment in which the execution is run. These can be accessed by calling into a contract (typically called Vm) at address 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D, which happens to be keccak(\"hevm cheat code\"), implementing the following methods: Function Description function prank(address sender) public Sets msg.sender to the specified sender for the next call. function startPrank(address sender) public Sets msg.sender to the specified sender until stopPrank() is called. function stopPrank() public Resets msg.sender to the default sender. function deal(address usr, uint amt) public Sets the eth balance of usr to amt. Note that if usr is a symbolic address, then it must be the address of a contract that has already been deployed. This restriction is in place to ensure soundness of our symbolic address encoding with respect to potential aliasing of symbolic addresses. function store(address c, bytes32 loc, bytes32 val) public Sets the slot loc of contract c to val. function warp(uint x) public Sets the block timestamp to x. function roll(uint x) public Sets the block number to x. function assume(bool b) public Add the condition b to the assumption base for the current branch. This functions almost identically to require. For most users, require is preferable. However, in case you wish to understand & modify the internal IR of hevm, you may want to use assume. function load(address c, bytes32 loc) public returns (bytes32 val) Reads the slot loc of contract c. function sign(uint sk, bytes32 digest) public returns (uint8 v, bytes32 r, bytes32 s) Signs the digest using the private key sk. Note that signatures produced via hevm.sign will leak the private key. function addr(uint sk) public returns (address addr) Derives an ethereum address from the private key sk. Note that hevm.addr(0) will fail with BadCheatCode as 0 is an invalid ECDSA private key. function ffi(string[] calldata) external returns (bytes memory) Executes the arguments as a command in the system shell and returns stdout. Expects abi encoded values to be returned from the shell or an error will be thrown. Note that this cheatcode means test authors can execute arbitrary code on user machines as part of a call to dapp test, for this reason all calls to ffi will fail unless the --ffi flag is passed. function createFork(string calldata urlOrAlias) external returns (uint256) Creates a new fork with the given endpoint and the latest block and returns the identifier of the fork. function selectFork(uint256 forkId) external Takes a fork identifier created by createFork and sets the corresponding forked state as active. function activeFork() external returns (uint256) Returns the identifier of the current fork. function label(address addr, string calldata label) external Labels the address in traces","breadcrumbs":"Forge std-test tutorial » Supported Cheat Codes","id":"30","title":"Supported Cheat Codes"},"31":{"body":"Equivalence checking allows to check whether two bytecodes do the same thing under all input circumstances. This allows to e.g. create two functions, one that is known to be good, and another that uses less gas, but is hard to check for correctness. Then, with equivalence checking, one can check whether the two behave the same. The notion of equivalence in hevm is defined as follows. Two contracts are equivalent if for all possible calldata and state, after execution has finished, their observable storage state is equivalent and they return the same value. In particular, the following is NOT checked when checking for equivalence: Gas consumption Events emitted Maximum stack depth Maximum memory usage Note that in the Solidity ABI, the calldata's first 4 bytes are the function selector which decide which function is being called, along with the potential fallback function mechanism. Hence, treating calldata as symbolic covers all possible function calls, including fallback functions. While not all contracts follow the Solidity ABI , since hevm's symbolic equivalence checker does not distinguish between function selector and function parameter bytes in the calldata, it will still correctly check the equivalence of such non-conforming contracts.","breadcrumbs":"Equivalence checking tutorial » Equivalence Checking Tutorial","id":"31","title":"Equivalence Checking Tutorial"},"32":{"body":"Let's see this toy contract, in file contract1.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt; }\n} And this, slightly modified one, in file contract2.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt/2; balances[recv] += amt/2; }\n} Now ask hevm if they are equivalent. First, let's compile both contracts and get their bytecode: bytecode1=$(solc --bin-runtime \"contract1.sol\" | tail -n1)\nbytecode2=$(solc --bin-runtime \"contract2.sol\" | tail -n1) Let's ask hevm to compare the two: $ hevm equivalence \\ --code-a $(solc --bin-runtime \"contract1.sol\" | tail -n1) \\ --code-b $(solc --bin-runtime \"contract2.sol\" | tail -n1)\nFound 90 total pairs of endstates\nAsking the SMT solver for 58 pairs\nReuse of previous queries was Useful in 0 cases\nNot equivalent. The following inputs result in differing behaviours:\n-----\nCalldata: 0xafc2c94900000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000023\nStorage: Addr SymAddr \"entrypoint\": [(0x0,0x10)]\nTransaction Context: TxValue: 0x0 This tells us that with a value of 0x23 being sent, which corresponds to 35, the two are not equivalent. This is indeed the case: one will add 35 div 2 = 17 twice, which is 34, the other will add 35.","breadcrumbs":"Equivalence checking tutorial » Finding Discrepancies","id":"32","title":"Finding Discrepancies"},"33":{"body":"Let's fix the above issue by incrementing the balance by 1 in case it's an odd value. Let's call this contract3.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt/2; balances[recv] += amt/2; if (amt % 2 != 0) balances[recv]++; }\n} Let's check whether this new contract is indeed equivalent: $ hevm equivalence \\ --code-a $(solc --bin-runtime \"contract1.sol\" | tail -n1) \\ --code-b $(solc --bin-runtime \"contract3.sol\" | tail -n1)\nFound 108 total pairs of endstates\nAsking the SMT solver for 74 pairs\nReuse of previous queries was Useful in 0 cases\nNo discrepancies found Hevm reports that the two are now equivalent, even though they clearly don't consume the same amount of gas and have widely different EVM bytecodes. Yet for an outside observer, they behave the same. Notice that hevm didn't simply fuzz the contract and within a given out of time it didn't find a counterexample. Instead, it proved the two equivalent from an outside observer perspective.","breadcrumbs":"Equivalence checking tutorial » Fixing and Proving Correctness","id":"33","title":"Fixing and Proving Correctness"},"34":{"body":"If the contracts have already been compiled into a hex string, you can paste them into files a.txt and b.txt and compare them via: $ hevm equivalence --code-a \"$(= 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); } Let's re-build with forge and check with hevm once again: $ forge build --ast\n[⠰] Compiling...\n[⠔] Compiling 1 files with 0.8.19\n[⠒] Solc 0.8.19 finished in 985.32ms\nCompiler run successful! $ hevm test --solver z3\nRunning 1 tests for src/contract.sol:MyContract\n[PASS] prove_add_value(address,uint256) We now get a PASS. Notice that this doesn't only mean that hevm couldn't find a bug within a given time frame. Instead, it means that there is surely no call to prove_add_value such that our assertion can be violated. However, it does not check for things that it was not asked to check for. In particular, it does not check that e.g. the sender's balance is decremented. There is no such test and so this omission is not detected.","breadcrumbs":"Getting Started » Fixing the Bug","id":"4","title":"Fixing the Bug"},"40":{"body":"Usage: hevm symbolic [--code TEXT] [--calldata TEXT] [--address ADDR] [--caller ADDR] [--origin ADDR] [--coinbase ADDR] [--value W256] [--nonce WORD64] [--gas WORD64] [--number W256] [--timestamp W256] [--basefee W256] [--priority-fee W256] [--gaslimit WORD64] [--gasprice W256] [--create] [--maxcodesize W256] [--prev-randao W256] [--chainid W256] [--rpc TEXT] [--block W256] [--root STRING] [--project-type PROJECTTYPE] [--initial-storage INITIALSTORAGE] [--sig TEXT] [--arg STRING]... [--get-models] [--show-tree] [--show-reachable-tree] [--smttimeout NATURAL] [--max-iterations INTEGER] [--solver TEXT] [--smtdebug] [--assertions [WORD256]] [--ask-smt-iterations INTEGER] [--num-solvers NATURAL] [--loop-detection-heuristic LOOPHEURISTIC] Available options: -h,--help Show this help text --code TEXT Program bytecode --calldata TEXT Tx: calldata --address ADDR Tx: address --caller ADDR Tx: caller --origin ADDR Tx: origin --coinbase ADDR Block: coinbase --value W256 Tx: Eth amount --nonce WORD64 Nonce of origin --gas WORD64 Tx: gas amount --number W256 Block: number --timestamp W256 Block: timestamp --basefee W256 Block: base fee --priority-fee W256 Tx: priority fee --gaslimit WORD64 Tx: gas limit --gasprice W256 Tx: gas price --create Tx: creation --maxcodesize W256 Block: max code size --prev-randao W256 Block: prevRandao --chainid W256 Env: chainId --rpc TEXT Fetch state from a remote node --block W256 Block state is be fetched from --root STRING Path to project root directory (default: . ) --project-type PROJECTTYPE Foundry or CombinedJSON project --initial-storage INITIALSTORAGE Starting state for storage: Empty, Abstract (default Abstract) --sig TEXT Signature of types to decode / encode --arg STRING Values to encode --get-models Print example testcase for each execution path --show-tree Print branches explored in tree view --show-reachable-tree Print only reachable branches explored in tree view --smttimeout NATURAL Timeout given to SMT solver in seconds (default: 300) --max-iterations INTEGER Number of times we may revisit a particular branching point. Default is 5. Setting to -1 allows infinite looping --solver TEXT Used SMT solver: z3 (default), cvc5, or bitwuzla --smtdebug Print smt queries sent to the solver --assertions [WORD256] Comma separated list of solc panic codes to check for (default: user defined assertion violations only) --ask-smt-iterations INTEGER Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1) (default: 1) --num-solvers NATURAL Number of solver instances to use (default: number of cpu cores) --loop-detection-heuristic LOOPHEURISTIC Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive (default: StackBased) Run a symbolic execution against the given parameters, searching for assertion violations. Counterexamples will be returned for any reachable assertion violations. Where an assertion violation is defined as either an execution of the invalid opcode (0xfe), or a revert with a message of the form abi.encodeWithSelector('Panic(uint256)', errCode) with errCode being one of the predefined solc assertion codes defined here . By default hevm ignores assertion violations that result from arithmetic overflow (Panic(0x11)), although this behaviour can be customised via the --assertions flag. For example, the following will return counterexamples for arithmetic overflow (0x11) and user defined assertions (0x01): hevm symbolic --code $CODE --assertions '[0x01, 0x11]' The default value for calldata and caller are symbolic values, but can be specialized to concrete functions with their corresponding flags. One can also specialize specific arguments to a function signature, while leaving others abstract. If --sig is given, calldata is assumed to be of the form suggested by the function signature. With this flag, specific arguments can be instantiated to concrete values via the --arg flag. This is best illustrated through a few examples: Calldata specialized to the bytestring 0xa9059cbb followed by 64 symbolic bytes: hevm symbolic --sig \"transfer(address,uint256)\" --code $(\" --arg 0 --code $( uint) balances; function prove_add_value(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n} Notice that this function has a bug: the require and the assert both check for <, but the if checks for >, which should instead be >=. Let's see if hevm can find this bug. In order to do that, we have to prepend the function name with prove_, which we did.","breadcrumbs":"Getting Started » Practical Scenario","id":"1","title":"Practical Scenario"},"10":{"body":"Fuzzing tests usually have a set of (sometimes implicit) pre- and postconditions, but the actual action (e.g. function call) is performed by an external entity, the fuzzer. For C/C++ fuzzing, the implicit postcondition is often e.g. that the system does not throw a segmentation fault. For EVM bytecode, postconditions need to be explicit. Let's see an example: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\nimport \"forge-std/Test.sol\"; contract MyContract is Test { uint balance; function test_overflow(uint amt) public { unchecked { balance += amt; } assert(balance >= amt); }\n} This function is easy to break by picking an amt that overflows balance, so that the postcondition balance > amt will not hold. A fuzzer finds this kind of bug very easily. However, fuzzers have trouble finding bugs that are either specifically hidden (e.g. by a malicious developer), or that have a complicated code path towards them. Let's see a simple one: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\nimport \"foge-std/Test.sol\"; contract MyContract is Test { uint balance; function prove_multiply(uint amt, uint amt2) public { require(amt != 1); require(amt2 != 1); require(amt < amt2); uint tmp; tmp = amt * amt2; if (tmp == 119274257) balance = 1337; else balance += tmp; assert(balance >= tmp); }\n} Calling this contract with amt = 9479 and amt2 = 12583 will set the balance to 1337 which is less than amt*amt2, breaking the postcondition. However, a fuzzer, e.g. Echidna will likely not find those numbers, because uint has a potential range of 2**256 and so it'd be looking for a needle in a haystack, when looking randomly. Here's how to run Echidna on the multiplication test: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { // the rest is the same\n} Then run: echidna --test-mode assertion src/multiply-test.sol Echidna will terminate after 50k runs, with all tests passing. Notice that the difference here, compared to the previous example, is that the overflow example has many different inputs that can break the postcondition, whereas here only one can. Hevm finds the bug in both of these functions. This is because hevm (and symbolic execution frameworks in general) try to find the bug via proof-directed search rather than using random inputs. In hevm, we try to prove that there are no inputs to the test case such that given the preconditions, the postconditions can be broken. While trying to construct this mathematical proof, hevm finds a countereexample , an input that breaks the postconditions: $ hevm test\nChecking 1 function(s) in contract src/multiply-test.sol:MyContract\n[RUNNING] prove_multiply(uint256,uint256) [FAIL] prove_multiply(uint256,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_multiply(9479,12583) Checking 1 function(s) in contract src/overflow-test.sol:MyContract\n[RUNNING] prove_overflow(uint256) [FAIL] prove_overflow(uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_overflow(00000000000000000000000000000000000000000000000100000000000000000182dad8c17bd5e89e8043a08ada90a6d5efdee4425f85cb863109783e158ba4fba908a0e6fae6c6b51002)","breadcrumbs":"When to Use » Fuzzing versus Symbolic Execution","id":"10","title":"Fuzzing versus Symbolic Execution"},"11":{"body":"Fuzzers are exceedingly fast and efficient when there are many potential faults with a function/contract, or if the faults are of a type that's easy to search for (e.g. off-by-one). However, they rarely, if ever, find cases where the bug is hidden deep in the branch logic, or needs very specific input parameters. Hence, it is best to use fuzzers at first to find easy-to-find bugs, as fuzzers are very efficient at that. Then, once the tests pass the fuzzer, it is recommended to use a symbolic execution engine such as hevm. hevm is similar to Halmos and Kontrol in its approach. However, it is quite different from static code analysis tools such as Oyente , Slither , and Mythril . While these 3 tools typically use some form of symbolic execution to try to validate their results, their main method of operation is not via symbolic execution, and they can, and do, report false positives. Notice that static code analysis tools can find bugs that the author(s) didn't write a test case for, as they typically have a (large) set of preconfigured test-cases that they can report on, if they can find a way to violate them. Hence, it may be valuable to run static analysis tools alongside symbolic execution tools such as hevm. Finally, SMTChecker may also be interesting to run alongside hevm. SMTChecker is very different from both approaches detailed above. While SMTChecker is capable of reliably finding both reentrancy and loop-related bugs, the tools above can only do so on a best effort basis. Hevm often reports a warning of incompleteness for such problems, while static code analysis tools either report potential positives or may even not discover them at all. Tool Approach Primary Method Notes hevm Symbolic analysis of EVM bytecode Symbolic execution Focuses on exploring all execution possibilities, identifying potential assertion violations, and optimizing gas usage. Can prove equivalence between bytecodes. Halmos Similar to hevm Not specified Approach similar to hevm, but the document does not detail specific methodologies or differences. Kontrol Similar to hevm Not specified Approach similar to hevm, with a focus presumably on symbolic analysis as well, but further details are not provided in the document. Oyente Static code analysis Partial symbolic execution Uses symbolic execution to validate results but primarily relies on static analysis. Can report false positives. Slither Static code analysis Partial symbolic execution Similar to Oyente, uses static analysis as its main method, complemented by symbolic execution for validation. Known for reporting false positives. Mythril Static code analysis Partial symbolic execution Combines static code analysis with symbolic execution for result validation. Like Oyente and Slither, can report false positives. SMTChecker Different from both hevm and static code analysis tools SMT solving Capable of finding reentrancy and loop-related bugs reliably, which other tools might miss or report incompletely. Offers a distinct approach from symbolic execution.","breadcrumbs":"When to Use » Similarities and Differences to Other Tools","id":"11","title":"Similarities and Differences to Other Tools"},"12":{"body":"Symbolic execution in general, and hevm in particular, have a number of known limitations. Many of these limitations can be worked around without too much effort. This document describes some of the most common limitations and workarounds.","breadcrumbs":"Limitations and Workarounds » Limitations and Workarounds","id":"12","title":"Limitations and Workarounds"},"13":{"body":"The most important issue related to symbolic execution is to do with loops and recursion. For example, the following code is hard to deal with in a symbolic context: function loop(uint n) { for(uint i = 0; i < n; i++) { mystate[i]++; }\n} When such a function is called, and n is a symbolic parameter (e.g. parameter to a function prove_, such as prove_correct(uint n)), hevm would need to create a new execution path for each potential value of n, which can be very large. The same principle applies to recursion, where the depth of the recursion may be unbounded or bounded only by a potentially very large number. Hence, hevm only explores loops and recursions up to fixed depth k, a parameter that can be adjusted from the command line via the --max-iterations k parameter. Whenever the limit is hit, hevm warns of the incomplete exploration: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Max Iterations Reached in contract: 0x[...] pc: [...] In general, the workaround suggested is to try to write code without loops, if possible, or to have a limit on the number of iterations. For example, by using max(k,n) instead of n in the loop condition, where k is a fixed number. Unbounded loops are a problem for digital contracts, as they may be forced by an attacker to exhaust gas, thereby potentially e.g. deadlocking the contract. This can lock in (large) funds, which can be a very serious issue. Hence, limiting loop iterations is a good practice in general -- not only for symbolic execution. Best Practices : Try to write code without loops, if possible. Use max(k,n) instead of n in the loop condition, where k is a fixed number. Avoid unbounded loops to prevent potential gas exhaustion attacks","breadcrumbs":"Limitations and Workarounds » Loops and recursion","id":"13","title":"Loops and recursion"},"14":{"body":"Gas is hard to symbolically track, due to certain opcodes, such as SLOAD, having different cost depending on the parameters to the opcode. Many symbolic execution systems, including hevm, solve this by not fully tracking gas. This means that hevm may report that an assertion failure can occur through a particular execution trace, but that trace would cost more to execute than the allowable gas limit. In general, it is possible to check whether the issue can be hit by running the hevm-provided counterexample in a concrete execution setting, thereby filtering out false positives. However, it is strongly advisable to fix potential issues that are only guarded due to gas exhaustion, as they may become exploitable in the future, when gas costs change. Best Practices : Don't rely on gas exhaustion as a security mechanism. Check potential issues by running the hevm-provided counterexample in a concrete execution setting.","breadcrumbs":"Limitations and Workarounds » Gas costs","id":"14","title":"Gas costs"},"15":{"body":"When a symbolic argument is passed to an EVM opcode that hevm cannot deal with symbolically, an error is raised. There are number of such EVM opcodes, for example JUMP, JUMPI, CALL, CALLCODE, DELEGATECALL, STATICCALL, CREATE, CREATE2, SELFDESTRUCT, etc. If any of these are called with an argument that is symbolic, hevm raises an error, such as: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Attempting to transfer eth to a symbolic address that is not present in the state There is no single workaround for this class of issues, as it depends on the specific circumstances of the code. In general, we suggest trying to concretize the call to the code, such that only what is truly needed to be symbolic is left symbolic. For example, you may be able to force partial concrete execution via require() statements, thereby concretizing the potential symbolic value. Similarly, dynamically computed JUMP destinations can be avoided via pre-computed jump tables, etc. Best Practices : Use require() statements to concretize symbolic values Avoid dynamically computed jumps -- use pre-computed jump-tables, if neccesary","breadcrumbs":"Limitations and Workarounds » Symbolic arguments to certain EVM opcodes","id":"15","title":"Symbolic arguments to certain EVM opcodes"},"16":{"body":"Jumping into symbolic code is not supported by hevm. This can happen when, e.g. a function creates a contract based on a symbolic value, and then jumps into the code of that contract. In these cases, you will get a warning like the following: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Encountered a jump into a potentially symbolic code region while executing initcode. pc: [...] jump dst: [...] For these cases, we suggest concretizing the call that creates the contract, such that the bytecode created and later jumped to, is not symbolic.","breadcrumbs":"Limitations and Workarounds » Jumping into symbolic code","id":"16","title":"Jumping into symbolic code"},"17":{"body":"To get an idea about what hevm is, see CAV'24 paper . You can also check out a few presentations by @msooseth .","breadcrumbs":"For hevm Developers » General overview","id":"17","title":"General overview"},"18":{"body":"","breadcrumbs":"For hevm Developers » Debugging","id":"18","title":"Debugging"},"19":{"body":"Haskell offers a way to print messages anywhere in the code with Debug.Trace . The simplest is trace which takes a string and a value and returns the same value while printing the string. For example add x y = trace \"Hello from add!\" (x + y)","breadcrumbs":"For hevm Developers » Printf-style debugging","id":"19","title":"Printf-style debugging"},"2":{"body":"We now need a copy of hevm (see releases ) and the SMT solver z3, which can be installed e.g. with apt-get on ubuntu/debian or homebrew on Mac, and a copy of Foundry : $ sudo apt-get install z3 # install z3\n$ curl -L https://foundry.paradigm.xyz | bash # install foundryup\n$ foundryup # install forge and other foundry binaries\n$ mkdir mytest && cd mytest\n$ wget https://github.com/ethereum/hevm/releases/download/release/0.53.0/hevm-x86_64-linux\n$ chmod +x ./hevm-x86_64-linux\n$ forge init .\n$ cat < src/contract.sol\npragma solidity ^0.8.19;\nimport \"forge-std/Test.sol\"; contract MyContract is Test { mapping (address => uint) balances; function prove_add_value(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n}\nEOF\n$ forge build --ast\n[⠊] Compiling...\n[⠒] Compiling 1 files with 0.8.19\n[⠢] Solc 0.8.19 finished in 14.27ms\nCompiler run successful!","breadcrumbs":"Getting Started » Building","id":"2","title":"Building"},"20":{"body":"hevm uses Tasty framework for running tests, including QuickCheck for property-based testing.","breadcrumbs":"For hevm Developers » Testing","id":"20","title":"Testing"},"21":{"body":"The basic command to run the tests is: cabal run test For development, it might be beneficial to pass devel flag: cabal run -f devel test This should enable parallel compilation and test runs (see the config file hevm.cabal). Additional parameters can be passed to the test runner after --. For example cabal run test -- --help will list all the additional parameters. Some of the interesting options are -p to filter only some of the tests and --quickcheck-tests to control how many tests quickcheck will generate for each property test.","breadcrumbs":"For hevm Developers » Running tests","id":"21","title":"Running tests"},"22":{"body":"There are a few ways to control how many tests Quickcheck will generate per property. By default, it generates 100 tests (satisfying the precondition). This can be controlled by maxSuccess argument passed to Quickcheck, or, in Tasty framework, using localOption (QuickCheckTests ). Passing --quickcheck-tests to the binary will change this value to . This value can be dynamically adjusted for a test group or a specific test. For example, instead of localOption it is possible to use adjustOption for a test group. The following ensures that for the following test group, the maximal value of the QuickCheckTests option is 50 (but if the current value is lower, it will be left unchanged). adjustOption (\\(Test.Tasty.QuickCheck.QuickCheckTests n) -> Test.Tasty.QuickCheck.QuickCheckTests (min n 50)) Similarly, the maxSuccess value can be modified for a single test. The following sets the number of tests generated to 20 for the particular test: testProperty $ withMaxSuccess 20 $ ...","breadcrumbs":"For hevm Developers » On property-based testing","id":"22","title":"On property-based testing"},"23":{"body":"","breadcrumbs":"For hevm Developers » Profiling","id":"23","title":"Profiling"},"24":{"body":"NOTE: Most of the time will likely be spent in the solver, and that will not show up when profiling Haskell application. In order to build the application with profiling information, we need to pass --enable-profiling to cabal. If we want to profile the test suite, we could run cabal run test --enable-profiling -- +RTS -p Note that +RTS means the next arguments will be passed to GHC and -p instructs the program to create a time profile report. This report is written into the .prof file. If we want to pass arguments to our executable, we have to indicate this with -RTS, for example, to profile run of only some tests, we would use cabal run test --enable-profiling -- +RTS -p -RTS -p ","breadcrumbs":"For hevm Developers » Profiling Haskell code","id":"24","title":"Profiling Haskell code"},"25":{"body":"Test cases must be prepended with prove_ and the testing contract must inherit from Test from Forge's standard test library . First, import Test: import {Test} from \"forge-std/Test.sol\"; and then inherit from it via ... is Test. This allows hevm to discover the test cases it needs to run. Like so: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract BadVaultTest is Test { function prove_mytest() { // environment setup, preconditions // call(s) to test // postcondition checks }\n} Once you have written such a test case, you need to compile with forge build --ast (see forge documentation for more details) and then: $ hevm test\nChecking 1 function(s) in contract src/badvault-test.sol:BadVault\n[RUNNING] prove_mytest(uint256) [PASS] prove_mytest(uint256) Here, hevm discovered the test case, and automatically checked it for violations.","breadcrumbs":"Forge std-test tutorial » Forge std-test Usage Tutorial","id":"25","title":"Forge std-test Usage Tutorial"},"26":{"body":"Tests usually need to set up the environment in a particular way, such as contract address, storage, etc. This can be done via Cheat Codes that can change the address of the caller, set block number, etc. See Cheat Codes below for a range of cheat codes supported. Cheat Codes are a standard method used by other tools, such as Foundry , so you should be able to re-use your existing setup. An example setup could be: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract BadVaultTest is Test { MyVault vault; function setUp() public { // Set up environment vault = new BadVault(); address user1 = address(1); vm.deal(user1, 1 ether); vm.prank(user1); vault.deposit{value: 1 ether}(); address user2 = address(2); vm.deal(user2, 1 ether); vm.prank(user2); vault.deposit{value: 1 ether}(); address attacker = address(42); vm.prank(attacker); // call(s) to test // postcondition checks }\n} The postconditions should check the state of the contract after the call(s) are complete. In particular, it should check that the changes that the function applied did not break any of the (invariants)[https://en.wikipedia.org/wiki/Invariant_(mathematics)] of the contract, such as total number of tokens. You can read more about testing and cheat codes in the (Foundry Book)[https://book.getfoundry.sh/forge/cheatcodes] and you can see the hevm-supported cheat codes below .","breadcrumbs":"Forge std-test tutorial » Setting Up Tests","id":"26","title":"Setting Up Tests"},"27":{"body":"When hevm discovers a failure, it prints an example call how to trigger the failure. Let's see the following simple solidity code: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { mapping (address => uint) balances; function prove_single_fail(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n} When compiling our foundry project, we must either always pass the --ast flag to forge build, or, much better, set the ast = true flag in the foundry.toml file: ast = true In case neither --ast was passed, nor ast = true was set in the foundry.toml file, we will get an error such as: Error: unable to parse Foundry project JSON: [...]/out/Base.sol/CommonBase.json Contract: \"CommonBase\" In these cases, issue forge clean and run forge build --ast again. Once the project has been correctly built, we can run hevm test, and get: $ hevm test\nChecking 1 function(s) in contract src/contract-fail.sol:MyContract\n[RUNNING] prove_single_fail(address,uint256) [FAIL] prove_single_fail(address,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_single_fail(0x0000000000000000000000000000000000000000,100) Here, hevm provided us with a calldata, where the receiver happens to be the zero address, and the value sent is exactly 100. This indeed is the boundary condition where the function call fails. The function should have had a >= rather than a > in the if. Notice that in this case, while hevm filled in the address to give a complete call, the address itself is irrelevant, although this is not explicitly mentioned.","breadcrumbs":"Forge std-test tutorial » Understanding Counterexamples","id":"27","title":"Understanding Counterexamples"},"28":{"body":"In test mode, hevm runs with the starting state set to concrete values. This means that with the solidity-generated default constructor of contracts, state variables will be zero, and arrays and mappings will be empty. If you need a different starting state, such as e.g. tokens already distributed to some addresses, you can set that up in the setup phase of your test. This can be done via the beforeTestSetup function, as documented in the Foundry Book . In case you need a symbolic starting state, see the Symbolic execution tutorial . Note that if all you need is a symbolic calldata, then you don't need to run hevm in symbolic mode, you can simply run hevm test and hevm will provide you with a symbolic calldata.","breadcrumbs":"Forge std-test tutorial » Starting State is Always Concrete","id":"28","title":"Starting State is Always Concrete"},"29":{"body":"Hevm assumes that a test case should not always revert. If you have such a test case, hevm will warn you and return a FAIL. For example this toy contract: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { uint256 cntr; function prove_allrevert(uint256 val) public { if(val < 0) { unchecked { cntr = val; } revert(); } else revert(); }\n} When compiled with forge and then ran under hevm with hevm test, hevm returns: Checking 1 function(s) in contract src/contract-allrevert.sol:MyContract\n[RUNNING] prove_allrevert(uint256) [FAIL] prove_allrevert(uint256) Reason: No reachable assertion violations, but all branches reverted Prefix this testname with `proveFail` if this is expected This is sometimes undesirable. In these cases, prefix your contract with proveFail_ instead of prove_: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { uint256 cntr; function proveFail_allrevert_expected(uint256 val) public { if(val < 0) { unchecked { cntr = val; cntr += 1; } revert(); } else revert(); }\n} When this is compiled with forge and then checked with hevm, it leads to: Checking 1 function(s) in contract src/contract-allrevert-expected.sol:MyContract\n[RUNNING] proveFail_allrevert_expected(uint256) [PASS] proveFail_allrevert_expected(uint256) Which is now the expected outcome.","breadcrumbs":"Forge std-test tutorial » Test Cases that Must Always Revert","id":"29","title":"Test Cases that Must Always Revert"},"3":{"body":"Now let's run hevm to see if it finds the bug: $ hevm test --solver z3\nRunning 1 tests for src/contract.sol:MyContract\n[FAIL] prove_add_value(address,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_add_value(0x0000000000000000000000000000000000000000,100)","breadcrumbs":"Getting Started » Finding the Bug","id":"3","title":"Finding the Bug"},"30":{"body":"Since hevm is an EVM implementation mainly dedicated to testing and exploration, it features a set of \"cheat codes\" which can manipulate the environment in which the execution is run. These can be accessed by calling into a contract (typically called Vm) at address 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D, which happens to be keccak(\"hevm cheat code\"), implementing the following methods: Function Description function prank(address sender) public Sets msg.sender to the specified sender for the next call. function startPrank(address sender) public Sets msg.sender to the specified sender until stopPrank() is called. function stopPrank() public Resets msg.sender to the default sender. function deal(address usr, uint amt) public Sets the eth balance of usr to amt. Note that if usr is a symbolic address, then it must be the address of a contract that has already been deployed. This restriction is in place to ensure soundness of our symbolic address encoding with respect to potential aliasing of symbolic addresses. function store(address c, bytes32 loc, bytes32 val) public Sets the slot loc of contract c to val. function warp(uint x) public Sets the block timestamp to x. function roll(uint x) public Sets the block number to x. function assume(bool b) public Add the condition b to the assumption base for the current branch. This functions almost identically to require. For most users, require is preferable. However, in case you wish to understand & modify the internal IR of hevm, you may want to use assume. function load(address c, bytes32 loc) public returns (bytes32 val) Reads the slot loc of contract c. function sign(uint sk, bytes32 digest) public returns (uint8 v, bytes32 r, bytes32 s) Signs the digest using the private key sk. Note that signatures produced via hevm.sign will leak the private key. function addr(uint sk) public returns (address addr) Derives an ethereum address from the private key sk. Note that hevm.addr(0) will fail with BadCheatCode as 0 is an invalid ECDSA private key. function ffi(string[] calldata) external returns (bytes memory) Executes the arguments as a command in the system shell and returns stdout. Expects abi encoded values to be returned from the shell or an error will be thrown. Note that this cheatcode means test authors can execute arbitrary code on user machines as part of a call to dapp test, for this reason all calls to ffi will fail unless the --ffi flag is passed. function createFork(string calldata urlOrAlias) external returns (uint256) Creates a new fork with the given endpoint and the latest block and returns the identifier of the fork. function selectFork(uint256 forkId) external Takes a fork identifier created by createFork and sets the corresponding forked state as active. function activeFork() external returns (uint256) Returns the identifier of the current fork. function label(address addr, string calldata label) external Labels the address in traces","breadcrumbs":"Forge std-test tutorial » Supported Cheat Codes","id":"30","title":"Supported Cheat Codes"},"31":{"body":"Equivalence checking allows to check whether two bytecodes do the same thing under all input circumstances. This allows to e.g. create two functions, one that is known to be good, and another that uses less gas, but is hard to check for correctness. Then, with equivalence checking, one can check whether the two behave the same. The notion of equivalence in hevm is defined as follows. Two contracts are equivalent if for all possible calldata and state, after execution has finished, their observable storage state is equivalent and they return the same value. In particular, the following is NOT checked when checking for equivalence: Gas consumption Events emitted Maximum stack depth Maximum memory usage Note that in the Solidity ABI, the calldata's first 4 bytes are the function selector which decide which function is being called, along with the potential fallback function mechanism. Hence, treating calldata as symbolic covers all possible function calls, including fallback functions. While not all contracts follow the Solidity ABI , since hevm's symbolic equivalence checker does not distinguish between function selector and function parameter bytes in the calldata, it will still correctly check the equivalence of such non-conforming contracts.","breadcrumbs":"Equivalence checking tutorial » Equivalence Checking Tutorial","id":"31","title":"Equivalence Checking Tutorial"},"32":{"body":"Let's see this toy contract, in file contract1.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt; }\n} And this, slightly modified one, in file contract2.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt/2; balances[recv] += amt/2; }\n} Now ask hevm if they are equivalent. First, let's compile both contracts and get their bytecode: bytecode1=$(solc --bin-runtime \"contract1.sol\" | tail -n1)\nbytecode2=$(solc --bin-runtime \"contract2.sol\" | tail -n1) Let's ask hevm to compare the two: $ hevm equivalence \\ --code-a $(solc --bin-runtime \"contract1.sol\" | tail -n1) \\ --code-b $(solc --bin-runtime \"contract2.sol\" | tail -n1)\nFound 90 total pairs of endstates\nAsking the SMT solver for 58 pairs\nReuse of previous queries was Useful in 0 cases\nNot equivalent. The following inputs result in differing behaviours:\n-----\nCalldata: 0xafc2c94900000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000023\nStorage: Addr SymAddr \"entrypoint\": [(0x0,0x10)]\nTransaction Context: TxValue: 0x0 This tells us that with a value of 0x23 being sent, which corresponds to 35, the two are not equivalent. This is indeed the case: one will add 35 div 2 = 17 twice, which is 34, the other will add 35.","breadcrumbs":"Equivalence checking tutorial » Finding Discrepancies","id":"32","title":"Finding Discrepancies"},"33":{"body":"Let's fix the above issue by incrementing the balance by 1 in case it's an odd value. Let's call this contract3.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt/2; balances[recv] += amt/2; if (amt % 2 != 0) balances[recv]++; }\n} Let's check whether this new contract is indeed equivalent: $ hevm equivalence \\ --code-a $(solc --bin-runtime \"contract1.sol\" | tail -n1) \\ --code-b $(solc --bin-runtime \"contract3.sol\" | tail -n1)\nFound 108 total pairs of endstates\nAsking the SMT solver for 74 pairs\nReuse of previous queries was Useful in 0 cases\nNo discrepancies found Hevm reports that the two are now equivalent, even though they clearly don't consume the same amount of gas and have widely different EVM bytecodes. Yet for an outside observer, they behave the same. Notice that hevm didn't simply fuzz the contract and within a given out of time it didn't find a counterexample. Instead, it proved the two equivalent from an outside observer perspective.","breadcrumbs":"Equivalence checking tutorial » Fixing and Proving Correctness","id":"33","title":"Fixing and Proving Correctness"},"34":{"body":"If the contracts have already been compiled into a hex string, you can paste them into files a.txt and b.txt and compare them via: $ hevm equivalence --code-a \"$(= 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); } Let's re-build with forge and check with hevm once again: $ forge build --ast\n[⠰] Compiling...\n[⠔] Compiling 1 files with 0.8.19\n[⠒] Solc 0.8.19 finished in 985.32ms\nCompiler run successful! $ hevm test --solver z3\nRunning 1 tests for src/contract.sol:MyContract\n[PASS] prove_add_value(address,uint256) We now get a PASS. Notice that this doesn't only mean that hevm couldn't find a bug within a given time frame. Instead, it means that there is surely no call to prove_add_value such that our assertion can be violated. However, it does not check for things that it was not asked to check for. In particular, it does not check that e.g. the sender's balance is decremented. There is no such test and so this omission is not detected.","breadcrumbs":"Getting Started » Fixing the Bug","id":"4","title":"Fixing the Bug"},"40":{"body":"Usage: hevm symbolic [--code TEXT] [--calldata TEXT] [--address ADDR] [--caller ADDR] [--origin ADDR] [--coinbase ADDR] [--value W256] [--nonce WORD64] [--gas WORD64] [--number W256] [--timestamp W256] [--basefee W256] [--priority-fee W256] [--gaslimit WORD64] [--gasprice W256] [--create] [--maxcodesize W256] [--prev-randao W256] [--chainid W256] [--rpc TEXT] [--block W256] [--root STRING] [--project-type PROJECTTYPE] [--initial-storage INITIALSTORAGE] [--sig TEXT] [--arg STRING]... [--get-models] [--show-tree] [--show-reachable-tree] [--smttimeout NATURAL] [--max-iterations INTEGER] [--solver TEXT] [--smtdebug] [--assertions [WORD256]] [--ask-smt-iterations INTEGER] [--num-solvers NATURAL] [--loop-detection-heuristic LOOPHEURISTIC] Available options: -h,--help Show this help text --code TEXT Program bytecode --calldata TEXT Tx: calldata --address ADDR Tx: address --caller ADDR Tx: caller --origin ADDR Tx: origin --coinbase ADDR Block: coinbase --value W256 Tx: Eth amount --nonce WORD64 Nonce of origin --gas WORD64 Tx: gas amount --number W256 Block: number --timestamp W256 Block: timestamp --basefee W256 Block: base fee --priority-fee W256 Tx: priority fee --gaslimit WORD64 Tx: gas limit --gasprice W256 Tx: gas price --create Tx: creation --maxcodesize W256 Block: max code size --prev-randao W256 Block: prevRandao --chainid W256 Env: chainId --rpc TEXT Fetch state from a remote node --block W256 Block state is be fetched from --root STRING Path to project root directory (default: . ) --project-type PROJECTTYPE Foundry or CombinedJSON project --initial-storage INITIALSTORAGE Starting state for storage: Empty, Abstract (default Abstract) --sig TEXT Signature of types to decode / encode --arg STRING Values to encode --get-models Print example testcase for each execution path --show-tree Print branches explored in tree view --show-reachable-tree Print only reachable branches explored in tree view --smttimeout NATURAL Timeout given to SMT solver in seconds (default: 300) --max-iterations INTEGER Number of times we may revisit a particular branching point. Default is 5. Setting to -1 allows infinite looping --solver TEXT Used SMT solver: z3 (default), cvc5, or bitwuzla --smtdebug Print smt queries sent to the solver --assertions [WORD256] Comma separated list of solc panic codes to check for (default: user defined assertion violations only) --ask-smt-iterations INTEGER Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1) (default: 1) --num-solvers NATURAL Number of solver instances to use (default: number of cpu cores) --loop-detection-heuristic LOOPHEURISTIC Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive (default: StackBased) Run a symbolic execution against the given parameters, searching for assertion violations. Counterexamples will be returned for any reachable assertion violations. Where an assertion violation is defined as either an execution of the invalid opcode (0xfe), or a revert with a message of the form abi.encodeWithSelector('Panic(uint256)', errCode) with errCode being one of the predefined solc assertion codes defined here . By default hevm ignores assertion violations that result from arithmetic overflow (Panic(0x11)), although this behaviour can be customised via the --assertions flag. For example, the following will return counterexamples for arithmetic overflow (0x11) and user defined assertions (0x01): hevm symbolic --code $CODE --assertions '[0x01, 0x11]' The default value for calldata and caller are symbolic values, but can be specialized to concrete functions with their corresponding flags. One can also specialize specific arguments to a function signature, while leaving others abstract. If --sig is given, calldata is assumed to be of the form suggested by the function signature. With this flag, specific arguments can be instantiated to concrete values via the --arg flag. This is best illustrated through a few examples: Calldata specialized to the bytestring 0xa9059cbb followed by 64 symbolic bytes: hevm symbolic --sig \"transfer(address,uint256)\" --code $(\" --arg 0 --code $( uint) balances; function prove_add_value(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n} Notice that this function has a bug: the require and the assert both check for <, but the if checks for >, which should instead be >=. Let's see if hevm can find this bug. In order to do that, we have to prepend the function name with prove_, which we did.","breadcrumbs":"Getting Started » Practical Scenario","id":"1","title":"Practical Scenario"},"10":{"body":"Fuzzing tests usually have a set of (sometimes implicit) pre- and postconditions, but the actual action (e.g. function call) is performed by an external entity, the fuzzer. For C/C++ fuzzing, the implicit postcondition is often e.g. that the system does not throw a segmentation fault. For EVM bytecode, postconditions need to be explicit. Let's see an example: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\nimport \"forge-std/Test.sol\"; contract MyContract is Test { uint balance; function test_overflow(uint amt) public { unchecked { balance += amt; } assert(balance >= amt); }\n} This function is easy to break by picking an amt that overflows balance, so that the postcondition balance > amt will not hold. A fuzzer finds this kind of bug very easily. However, fuzzers have trouble finding bugs that are either specifically hidden (e.g. by a malicious developer), or that have a complicated code path towards them. Let's see a simple one: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\nimport \"foge-std/Test.sol\"; contract MyContract is Test { uint balance; function prove_multiply(uint amt, uint amt2) public { require(amt != 1); require(amt2 != 1); require(amt < amt2); uint tmp; tmp = amt * amt2; if (tmp == 119274257) balance = 1337; else balance += tmp; assert(balance >= tmp); }\n} Calling this contract with amt = 9479 and amt2 = 12583 will set the balance to 1337 which is less than amt*amt2, breaking the postcondition. However, a fuzzer, e.g. Echidna will likely not find those numbers, because uint has a potential range of 2**256 and so it'd be looking for a needle in a haystack, when looking randomly. Here's how to run Echidna on the multiplication test: // SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { // the rest is the same\n} Then run: echidna --test-mode assertion src/multiply-test.sol Echidna will terminate after 50k runs, with all tests passing. Notice that the difference here, compared to the previous example, is that the overflow example has many different inputs that can break the postcondition, whereas here only one can. Hevm finds the bug in both of these functions. This is because hevm (and symbolic execution frameworks in general) try to find the bug via proof-directed search rather than using random inputs. In hevm, we try to prove that there are no inputs to the test case such that given the preconditions, the postconditions can be broken. While trying to construct this mathematical proof, hevm finds a countereexample , an input that breaks the postconditions: $ hevm test\nChecking 1 function(s) in contract src/multiply-test.sol:MyContract\n[RUNNING] prove_multiply(uint256,uint256) [FAIL] prove_multiply(uint256,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_multiply(9479,12583) Checking 1 function(s) in contract src/overflow-test.sol:MyContract\n[RUNNING] prove_overflow(uint256) [FAIL] prove_overflow(uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_overflow(00000000000000000000000000000000000000000000000100000000000000000182dad8c17bd5e89e8043a08ada90a6d5efdee4425f85cb863109783e158ba4fba908a0e6fae6c6b51002)","breadcrumbs":"When to Use » Fuzzing versus Symbolic Execution","id":"10","title":"Fuzzing versus Symbolic Execution"},"11":{"body":"Fuzzers are exceedingly fast and efficient when there are many potential faults with a function/contract, or if the faults are of a type that's easy to search for (e.g. off-by-one). However, they rarely, if ever, find cases where the bug is hidden deep in the branch logic, or needs very specific input parameters. Hence, it is best to use fuzzers at first to find easy-to-find bugs, as fuzzers are very efficient at that. Then, once the tests pass the fuzzer, it is recommended to use a symbolic execution engine such as hevm. hevm is similar to Halmos and Kontrol in its approach. However, it is quite different from static code analysis tools such as Oyente , Slither , and Mythril . While these 3 tools typically use some form of symbolic execution to try to validate their results, their main method of operation is not via symbolic execution, and they can, and do, report false positives. Notice that static code analysis tools can find bugs that the author(s) didn't write a test case for, as they typically have a (large) set of preconfigured test-cases that they can report on, if they can find a way to violate them. Hence, it may be valuable to run static analysis tools alongside symbolic execution tools such as hevm. Finally, SMTChecker may also be interesting to run alongside hevm. SMTChecker is very different from both approaches detailed above. While SMTChecker is capable of reliably finding both reentrancy and loop-related bugs, the tools above can only do so on a best effort basis. Hevm often reports a warning of incompleteness for such problems, while static code analysis tools either report potential positives or may even not discover them at all. Tool Approach Primary Method Notes hevm Symbolic analysis of EVM bytecode Symbolic execution Focuses on exploring all execution possibilities, identifying potential assertion violations, and optimizing gas usage. Can prove equivalence between bytecodes. Halmos Similar to hevm Not specified Approach similar to hevm, but the document does not detail specific methodologies or differences. Kontrol Similar to hevm Not specified Approach similar to hevm, with a focus presumably on symbolic analysis as well, but further details are not provided in the document. Oyente Static code analysis Partial symbolic execution Uses symbolic execution to validate results but primarily relies on static analysis. Can report false positives. Slither Static code analysis Partial symbolic execution Similar to Oyente, uses static analysis as its main method, complemented by symbolic execution for validation. Known for reporting false positives. Mythril Static code analysis Partial symbolic execution Combines static code analysis with symbolic execution for result validation. Like Oyente and Slither, can report false positives. SMTChecker Different from both hevm and static code analysis tools SMT solving Capable of finding reentrancy and loop-related bugs reliably, which other tools might miss or report incompletely. Offers a distinct approach from symbolic execution.","breadcrumbs":"When to Use » Similarities and Differences to Other Tools","id":"11","title":"Similarities and Differences to Other Tools"},"12":{"body":"Symbolic execution in general, and hevm in particular, have a number of known limitations. Many of these limitations can be worked around without too much effort. This document describes some of the most common limitations and workarounds.","breadcrumbs":"Limitations and Workarounds » Limitations and Workarounds","id":"12","title":"Limitations and Workarounds"},"13":{"body":"The most important issue related to symbolic execution is to do with loops and recursion. For example, the following code is hard to deal with in a symbolic context: function loop(uint n) { for(uint i = 0; i < n; i++) { mystate[i]++; }\n} When such a function is called, and n is a symbolic parameter (e.g. parameter to a function prove_, such as prove_correct(uint n)), hevm would need to create a new execution path for each potential value of n, which can be very large. The same principle applies to recursion, where the depth of the recursion may be unbounded or bounded only by a potentially very large number. Hence, hevm only explores loops and recursions up to fixed depth k, a parameter that can be adjusted from the command line via the --max-iterations k parameter. Whenever the limit is hit, hevm warns of the incomplete exploration: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Max Iterations Reached in contract: 0x[...] pc: [...] In general, the workaround suggested is to try to write code without loops, if possible, or to have a limit on the number of iterations. For example, by using max(k,n) instead of n in the loop condition, where k is a fixed number. Unbounded loops are a problem for digital contracts, as they may be forced by an attacker to exhaust gas, thereby potentially e.g. deadlocking the contract. This can lock in (large) funds, which can be a very serious issue. Hence, limiting loop iterations is a good practice in general -- not only for symbolic execution. Best Practices : Try to write code without loops, if possible. Use max(k,n) instead of n in the loop condition, where k is a fixed number. Avoid unbounded loops to prevent potential gas exhaustion attacks","breadcrumbs":"Limitations and Workarounds » Loops and recursion","id":"13","title":"Loops and recursion"},"14":{"body":"Gas is hard to symbolically track, due to certain opcodes, such as SLOAD, having different cost depending on the parameters to the opcode. Many symbolic execution systems, including hevm, solve this by not fully tracking gas. This means that hevm may report that an assertion failure can occur through a particular execution trace, but that trace would cost more to execute than the allowable gas limit. In general, it is possible to check whether the issue can be hit by running the hevm-provided counterexample in a concrete execution setting, thereby filtering out false positives. However, it is strongly advisable to fix potential issues that are only guarded due to gas exhaustion, as they may become exploitable in the future, when gas costs change. Best Practices : Don't rely on gas exhaustion as a security mechanism. Check potential issues by running the hevm-provided counterexample in a concrete execution setting.","breadcrumbs":"Limitations and Workarounds » Gas costs","id":"14","title":"Gas costs"},"15":{"body":"When a symbolic argument is passed to an EVM opcode that hevm cannot deal with symbolically, an error is raised. There are number of such EVM opcodes, for example JUMP, JUMPI, CALL, CALLCODE, DELEGATECALL, STATICCALL, CREATE, CREATE2, SELFDESTRUCT, etc. If any of these are called with an argument that is symbolic, hevm raises an error, such as: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Attempting to transfer eth to a symbolic address that is not present in the state There is no single workaround for this class of issues, as it depends on the specific circumstances of the code. In general, we suggest trying to concretize the call to the code, such that only what is truly needed to be symbolic is left symbolic. For example, you may be able to force partial concrete execution via require() statements, thereby concretizing the potential symbolic value. Similarly, dynamically computed JUMP destinations can be avoided via pre-computed jump tables, etc. Best Practices : Use require() statements to concretize symbolic values Avoid dynamically computed jumps -- use pre-computed jump-tables, if neccesary","breadcrumbs":"Limitations and Workarounds » Symbolic arguments to certain EVM opcodes","id":"15","title":"Symbolic arguments to certain EVM opcodes"},"16":{"body":"Jumping into symbolic code is not supported by hevm. This can happen when, e.g. a function creates a contract based on a symbolic value, and then jumps into the code of that contract. In these cases, you will get a warning like the following: WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s): - Encountered a jump into a potentially symbolic code region while executing initcode. pc: [...] jump dst: [...] For these cases, we suggest concretizing the call that creates the contract, such that the bytecode created and later jumped to, is not symbolic.","breadcrumbs":"Limitations and Workarounds » Jumping into symbolic code","id":"16","title":"Jumping into symbolic code"},"17":{"body":"To get an idea about what hevm is, see CAV'24 paper . You can also check out a few presentations by @msooseth .","breadcrumbs":"For hevm Developers » General overview","id":"17","title":"General overview"},"18":{"body":"","breadcrumbs":"For hevm Developers » Debugging","id":"18","title":"Debugging"},"19":{"body":"Haskell offers a way to print messages anywhere in the code with Debug.Trace . The simplest is trace which takes a string and a value and returns the same value while printing the string. For example add x y = trace \"Hello from add!\" (x + y)","breadcrumbs":"For hevm Developers » Printf-style debugging","id":"19","title":"Printf-style debugging"},"2":{"body":"We now need a copy of hevm (see releases ) and the SMT solver z3, which can be installed e.g. with apt-get on ubuntu/debian or homebrew on Mac, and a copy of Foundry : $ sudo apt-get install z3 # install z3\n$ curl -L https://foundry.paradigm.xyz | bash # install foundryup\n$ foundryup # install forge and other foundry binaries\n$ mkdir mytest && cd mytest\n$ wget https://github.com/ethereum/hevm/releases/download/release/0.53.0/hevm-x86_64-linux\n$ chmod +x ./hevm-x86_64-linux\n$ forge init .\n$ cat < src/contract.sol\npragma solidity ^0.8.19;\nimport \"forge-std/Test.sol\"; contract MyContract is Test { mapping (address => uint) balances; function prove_add_value(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n}\nEOF\n$ forge build --ast\n[⠊] Compiling...\n[⠒] Compiling 1 files with 0.8.19\n[⠢] Solc 0.8.19 finished in 14.27ms\nCompiler run successful!","breadcrumbs":"Getting Started » Building","id":"2","title":"Building"},"20":{"body":"hevm uses Tasty framework for running tests, including QuickCheck for property-based testing.","breadcrumbs":"For hevm Developers » Testing","id":"20","title":"Testing"},"21":{"body":"The basic command to run the tests is: cabal run test For development, it might be beneficial to pass devel flag: cabal run -f devel test This should enable parallel compilation and test runs (see the config file hevm.cabal). Additional parameters can be passed to the test runner after --. For example cabal run test -- --help will list all the additional parameters. Some of the interesting options are -p to filter only some of the tests and --quickcheck-tests to control how many tests quickcheck will generate for each property test.","breadcrumbs":"For hevm Developers » Running tests","id":"21","title":"Running tests"},"22":{"body":"There are a few ways to control how many tests Quickcheck will generate per property. By default, it generates 100 tests (satisfying the precondition). This can be controlled by maxSuccess argument passed to Quickcheck, or, in Tasty framework, using localOption (QuickCheckTests ). Passing --quickcheck-tests to the binary will change this value to . This value can be dynamically adjusted for a test group or a specific test. For example, instead of localOption it is possible to use adjustOption for a test group. The following ensures that for the following test group, the maximal value of the QuickCheckTests option is 50 (but if the current value is lower, it will be left unchanged). adjustOption (\\(Test.Tasty.QuickCheck.QuickCheckTests n) -> Test.Tasty.QuickCheck.QuickCheckTests (min n 50)) Similarly, the maxSuccess value can be modified for a single test. The following sets the number of tests generated to 20 for the particular test: testProperty $ withMaxSuccess 20 $ ...","breadcrumbs":"For hevm Developers » On property-based testing","id":"22","title":"On property-based testing"},"23":{"body":"","breadcrumbs":"For hevm Developers » Profiling","id":"23","title":"Profiling"},"24":{"body":"NOTE: Most of the time will likely be spent in the solver, and that will not show up when profiling Haskell application. In order to build the application with profiling information, we need to pass --enable-profiling to cabal. If we want to profile the test suite, we could run cabal run test --enable-profiling -- +RTS -p Note that +RTS means the next arguments will be passed to GHC and -p instructs the program to create a time profile report. This report is written into the .prof file. If we want to pass arguments to our executable, we have to indicate this with -RTS, for example, to profile run of only some tests, we would use cabal run test --enable-profiling -- +RTS -p -RTS -p ","breadcrumbs":"For hevm Developers » Profiling Haskell code","id":"24","title":"Profiling Haskell code"},"25":{"body":"Test cases must be prepended with prove_ and the testing contract must inherit from Test from Forge's standard test library . First, import Test: import {Test} from \"forge-std/Test.sol\"; and then inherit from it via ... is Test. This allows hevm to discover the test cases it needs to run. Like so: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract BadVaultTest is Test { function prove_mytest() { // environment setup, preconditions // call(s) to test // postcondition checks }\n} Once you have written such a test case, you need to compile with forge build --ast (see forge documentation for more details) and then: $ hevm test\nChecking 1 function(s) in contract src/badvault-test.sol:BadVault\n[RUNNING] prove_mytest(uint256) [PASS] prove_mytest(uint256) Here, hevm discovered the test case, and automatically checked it for violations.","breadcrumbs":"Forge std-test tutorial » Forge std-test Usage Tutorial","id":"25","title":"Forge std-test Usage Tutorial"},"26":{"body":"Tests usually need to set up the environment in a particular way, such as contract address, storage, etc. This can be done via Cheat Codes that can change the address of the caller, set block number, etc. See Cheat Codes below for a range of cheat codes supported. Cheat Codes are a standard method used by other tools, such as Foundry , so you should be able to re-use your existing setup. An example setup could be: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract BadVaultTest is Test { MyVault vault; function setUp() public { // Set up environment vault = new BadVault(); address user1 = address(1); vm.deal(user1, 1 ether); vm.prank(user1); vault.deposit{value: 1 ether}(); address user2 = address(2); vm.deal(user2, 1 ether); vm.prank(user2); vault.deposit{value: 1 ether}(); address attacker = address(42); vm.prank(attacker); // call(s) to test // postcondition checks }\n} The postconditions should check the state of the contract after the call(s) are complete. In particular, it should check that the changes that the function applied did not break any of the (invariants)[https://en.wikipedia.org/wiki/Invariant_(mathematics)] of the contract, such as total number of tokens. You can read more about testing and cheat codes in the (Foundry Book)[https://book.getfoundry.sh/forge/cheatcodes] and you can see the hevm-supported cheat codes below .","breadcrumbs":"Forge std-test tutorial » Setting Up Tests","id":"26","title":"Setting Up Tests"},"27":{"body":"When hevm discovers a failure, it prints an example call how to trigger the failure. Let's see the following simple solidity code: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { mapping (address => uint) balances; function prove_single_fail(address recv, uint amt) public { require(balances[recv] < 100); if (balances[recv] + amt > 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); }\n} When compiling our foundry project, we must either always pass the --ast flag to forge build, or, much better, set the ast = true flag in the foundry.toml file: ast = true In case neither --ast was passed, nor ast = true was set in the foundry.toml file, we will get an error such as: Error: unable to parse Foundry project JSON: [...]/out/Base.sol/CommonBase.json Contract: \"CommonBase\" In these cases, issue forge clean and run forge build --ast again. Once the project has been correctly built, we can run hevm test, and get: $ hevm test\nChecking 1 function(s) in contract src/contract-fail.sol:MyContract\n[RUNNING] prove_single_fail(address,uint256) [FAIL] prove_single_fail(address,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_single_fail(0x0000000000000000000000000000000000000000,100) Here, hevm provided us with a calldata, where the receiver happens to be the zero address, and the value sent is exactly 100. This indeed is the boundary condition where the function call fails. The function should have had a >= rather than a > in the if. Notice that in this case, while hevm filled in the address to give a complete call, the address itself is irrelevant, although this is not explicitly mentioned.","breadcrumbs":"Forge std-test tutorial » Understanding Counterexamples","id":"27","title":"Understanding Counterexamples"},"28":{"body":"In test mode, hevm runs with the starting state set to concrete values. This means that with the solidity-generated default constructor of contracts, state variables will be zero, and arrays and mappings will be empty. If you need a different starting state, such as e.g. tokens already distributed to some addresses, you can set that up in the setup phase of your test. This can be done via the beforeTestSetup function, as documented in the Foundry Book . In case you need a symbolic starting state, see the Symbolic execution tutorial . Note that if all you need is a symbolic calldata, then you don't need to run hevm in symbolic mode, you can simply run hevm test and hevm will provide you with a symbolic calldata.","breadcrumbs":"Forge std-test tutorial » Starting State is Always Concrete","id":"28","title":"Starting State is Always Concrete"},"29":{"body":"Hevm assumes that a test case should not always revert. If you have such a test case, hevm will warn you and return a FAIL. For example this toy contract: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { uint256 cntr; function prove_allrevert(uint256 val) public { if(val < 0) { unchecked { cntr = val; } revert(); } else revert(); }\n} When compiled with forge and then ran under hevm with hevm test, hevm returns: Checking 1 function(s) in contract src/contract-allrevert.sol:MyContract\n[RUNNING] prove_allrevert(uint256) [FAIL] prove_allrevert(uint256) Reason: No reachable assertion violations, but all branches reverted Prefix this testname with `proveFail` if this is expected This is sometimes undesirable. In these cases, prefix your contract with proveFail_ instead of prove_: pragma solidity ^0.8.19;\nimport {Test} from \"forge-std/Test.sol\";\ncontract MyContract is Test { uint256 cntr; function proveFail_allrevert_expected(uint256 val) public { if(val < 0) { unchecked { cntr = val; cntr += 1; } revert(); } else revert(); }\n} When this is compiled with forge and then checked with hevm, it leads to: Checking 1 function(s) in contract src/contract-allrevert-expected.sol:MyContract\n[RUNNING] proveFail_allrevert_expected(uint256) [PASS] proveFail_allrevert_expected(uint256) Which is now the expected outcome.","breadcrumbs":"Forge std-test tutorial » Test Cases that Must Always Revert","id":"29","title":"Test Cases that Must Always Revert"},"3":{"body":"Now let's run hevm to see if it finds the bug: $ hevm test --solver z3\nRunning 1 tests for src/contract.sol:MyContract\n[FAIL] prove_add_value(address,uint256) Counterexample: result: Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 calldata: prove_add_value(0x0000000000000000000000000000000000000000,100)","breadcrumbs":"Getting Started » Finding the Bug","id":"3","title":"Finding the Bug"},"30":{"body":"Since hevm is an EVM implementation mainly dedicated to testing and exploration, it features a set of \"cheat codes\" which can manipulate the environment in which the execution is run. These can be accessed by calling into a contract (typically called Vm) at address 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D, which happens to be keccak(\"hevm cheat code\"), implementing the following methods: Function Description function prank(address sender) public Sets msg.sender to the specified sender for the next call. function startPrank(address sender) public Sets msg.sender to the specified sender until stopPrank() is called. function stopPrank() public Resets msg.sender to the default sender. function deal(address usr, uint amt) public Sets the eth balance of usr to amt. Note that if usr is a symbolic address, then it must be the address of a contract that has already been deployed. This restriction is in place to ensure soundness of our symbolic address encoding with respect to potential aliasing of symbolic addresses. function store(address c, bytes32 loc, bytes32 val) public Sets the slot loc of contract c to val. function warp(uint x) public Sets the block timestamp to x. function roll(uint x) public Sets the block number to x. function assume(bool b) public Add the condition b to the assumption base for the current branch. This functions almost identically to require. For most users, require is preferable. However, in case you wish to understand & modify the internal IR of hevm, you may want to use assume. function load(address c, bytes32 loc) public returns (bytes32 val) Reads the slot loc of contract c. function sign(uint sk, bytes32 digest) public returns (uint8 v, bytes32 r, bytes32 s) Signs the digest using the private key sk. Note that signatures produced via hevm.sign will leak the private key. function addr(uint sk) public returns (address addr) Derives an ethereum address from the private key sk. Note that hevm.addr(0) will fail with BadCheatCode as 0 is an invalid ECDSA private key. function ffi(string[] calldata) external returns (bytes memory) Executes the arguments as a command in the system shell and returns stdout. Expects abi encoded values to be returned from the shell or an error will be thrown. Note that this cheatcode means test authors can execute arbitrary code on user machines as part of a call to dapp test, for this reason all calls to ffi will fail unless the --ffi flag is passed. function createFork(string calldata urlOrAlias) external returns (uint256) Creates a new fork with the given endpoint and the latest block and returns the identifier of the fork. function selectFork(uint256 forkId) external Takes a fork identifier created by createFork and sets the corresponding forked state as active. function activeFork() external returns (uint256) Returns the identifier of the current fork. function label(address addr, string calldata label) external Labels the address in traces","breadcrumbs":"Forge std-test tutorial » Supported Cheat Codes","id":"30","title":"Supported Cheat Codes"},"31":{"body":"Equivalence checking allows to check whether two bytecodes do the same thing under all input circumstances. This allows to e.g. create two functions, one that is known to be good, and another that uses less gas, but is hard to check for correctness. Then, with equivalence checking, one can check whether the two behave the same. The notion of equivalence in hevm is defined as follows. Two contracts are equivalent if for all possible calldata and state, after execution has finished, their observable storage state is equivalent and they return the same value. In particular, the following is NOT checked when checking for equivalence: Gas consumption Events emitted Maximum stack depth Maximum memory usage Note that in the Solidity ABI, the calldata's first 4 bytes are the function selector which decide which function is being called, along with the potential fallback function mechanism. Hence, treating calldata as symbolic covers all possible function calls, including fallback functions. While not all contracts follow the Solidity ABI , since hevm's symbolic equivalence checker does not distinguish between function selector and function parameter bytes in the calldata, it will still correctly check the equivalence of such non-conforming contracts.","breadcrumbs":"Equivalence checking tutorial » Equivalence Checking Tutorial","id":"31","title":"Equivalence Checking Tutorial"},"32":{"body":"Let's see this toy contract, in file contract1.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt; }\n} And this, slightly modified one, in file contract2.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt/2; balances[recv] += amt/2; }\n} Now ask hevm if they are equivalent. First, let's compile both contracts and get their bytecode: bytecode1=$(solc --bin-runtime \"contract1.sol\" | tail -n1)\nbytecode2=$(solc --bin-runtime \"contract2.sol\" | tail -n1) Let's ask hevm to compare the two: $ hevm equivalence \\ --code-a $(solc --bin-runtime \"contract1.sol\" | tail -n1) \\ --code-b $(solc --bin-runtime \"contract2.sol\" | tail -n1)\nFound 90 total pairs of endstates\nAsking the SMT solver for 58 pairs\nReuse of previous queries was Useful in 0 cases\nNot equivalent. The following inputs result in differing behaviours:\n-----\nCalldata: 0xafc2c94900000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000023\nStorage: Addr SymAddr \"entrypoint\": [(0x0,0x10)]\nTransaction Context: TxValue: 0x0 This tells us that with a value of 0x23 being sent, which corresponds to 35, the two are not equivalent. This is indeed the case: one will add 35 div 2 = 17 twice, which is 34, the other will add 35.","breadcrumbs":"Equivalence checking tutorial » Finding Discrepancies","id":"32","title":"Finding Discrepancies"},"33":{"body":"Let's fix the above issue by incrementing the balance by 1 in case it's an odd value. Let's call this contract3.sol : //SPDX-License-Identifier: MIT\npragma solidity ^0.8.19;\ncontract MyContract { mapping (address => uint) balances; function my_adder(address recv, uint amt) public { if (balances[recv] + amt >= 100) { revert(); } balances[recv] += amt/2; balances[recv] += amt/2; if (amt % 2 != 0) balances[recv]++; }\n} Let's check whether this new contract is indeed equivalent: $ hevm equivalence \\ --code-a $(solc --bin-runtime \"contract1.sol\" | tail -n1) \\ --code-b $(solc --bin-runtime \"contract3.sol\" | tail -n1)\nFound 108 total pairs of endstates\nAsking the SMT solver for 74 pairs\nReuse of previous queries was Useful in 0 cases\nNo discrepancies found Hevm reports that the two are now equivalent, even though they clearly don't consume the same amount of gas and have widely different EVM bytecodes. Yet for an outside observer, they behave the same. Notice that hevm didn't simply fuzz the contract and within a given out of time it didn't find a counterexample. Instead, it proved the two equivalent from an outside observer perspective.","breadcrumbs":"Equivalence checking tutorial » Fixing and Proving Correctness","id":"33","title":"Fixing and Proving Correctness"},"34":{"body":"If the contracts have already been compiled into a hex string, you can paste them into files a.txt and b.txt and compare them via: $ hevm equivalence --code-a \"$(= 100) { revert(); } balances[recv] += amt; assert(balances[recv] < 100); } Let's re-build with forge and check with hevm once again: $ forge build --ast\n[⠰] Compiling...\n[⠔] Compiling 1 files with 0.8.19\n[⠒] Solc 0.8.19 finished in 985.32ms\nCompiler run successful! $ hevm test --solver z3\nRunning 1 tests for src/contract.sol:MyContract\n[PASS] prove_add_value(address,uint256) We now get a PASS. Notice that this doesn't only mean that hevm couldn't find a bug within a given time frame. Instead, it means that there is surely no call to prove_add_value such that our assertion can be violated. However, it does not check for things that it was not asked to check for. In particular, it does not check that e.g. the sender's balance is decremented. There is no such test and so this omission is not detected.","breadcrumbs":"Getting Started » Fixing the Bug","id":"4","title":"Fixing the Bug"},"40":{"body":"Usage: hevm symbolic [--code TEXT] [--calldata TEXT] [--address ADDR] [--caller ADDR] [--origin ADDR] [--coinbase ADDR] [--value W256] [--nonce WORD64] [--gas WORD64] [--number W256] [--timestamp W256] [--basefee W256] [--priority-fee W256] [--gaslimit WORD64] [--gasprice W256] [--create] [--maxcodesize W256] [--prev-randao W256] [--chainid W256] [--rpc TEXT] [--block W256] [--root STRING] [--project-type PROJECTTYPE] [--initial-storage INITIALSTORAGE] [--sig TEXT] [--arg STRING]... [--get-models] [--show-tree] [--show-reachable-tree] [--smttimeout NATURAL] [--max-iterations INTEGER] [--solver TEXT] [--smtdebug] [--assertions [WORD256]] [--ask-smt-iterations INTEGER] [--num-solvers NATURAL] [--loop-detection-heuristic LOOPHEURISTIC] Available options: -h,--help Show this help text --code TEXT Program bytecode --calldata TEXT Tx: calldata --address ADDR Tx: address --caller ADDR Tx: caller --origin ADDR Tx: origin --coinbase ADDR Block: coinbase --value W256 Tx: Eth amount --nonce WORD64 Nonce of origin --gas WORD64 Tx: gas amount --number W256 Block: number --timestamp W256 Block: timestamp --basefee W256 Block: base fee --priority-fee W256 Tx: priority fee --gaslimit WORD64 Tx: gas limit --gasprice W256 Tx: gas price --create Tx: creation --maxcodesize W256 Block: max code size --prev-randao W256 Block: prevRandao --chainid W256 Env: chainId --rpc TEXT Fetch state from a remote node --block W256 Block state is be fetched from --root STRING Path to project root directory (default: . ) --project-type PROJECTTYPE Foundry or CombinedJSON project --initial-storage INITIALSTORAGE Starting state for storage: Empty, Abstract (default Abstract) --sig TEXT Signature of types to decode / encode --arg STRING Values to encode --get-models Print example testcase for each execution path --show-tree Print branches explored in tree view --show-reachable-tree Print only reachable branches explored in tree view --smttimeout NATURAL Timeout given to SMT solver in seconds (default: 300) --max-iterations INTEGER Number of times we may revisit a particular branching point. Default is 5. Setting to -1 allows infinite looping --solver TEXT Used SMT solver: z3 (default), cvc5, or bitwuzla --smtdebug Print smt queries sent to the solver --assertions [WORD256] Comma separated list of solc panic codes to check for (default: user defined assertion violations only) --ask-smt-iterations INTEGER Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1) (default: 1) --num-solvers NATURAL Number of solver instances to use (default: number of cpu cores) --loop-detection-heuristic LOOPHEURISTIC Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive (default: StackBased) Run a symbolic execution against the given parameters, searching for assertion violations. Counterexamples will be returned for any reachable assertion violations. Where an assertion violation is defined as either an execution of the invalid opcode (0xfe), or a revert with a message of the form abi.encodeWithSelector('Panic(uint256)', errCode) with errCode being one of the predefined solc assertion codes defined here . By default hevm ignores assertion violations that result from arithmetic overflow (Panic(0x11)), although this behaviour can be customised via the --assertions flag. For example, the following will return counterexamples for arithmetic overflow (0x11) and user defined assertions (0x01): hevm symbolic --code $CODE --assertions '[0x01, 0x11]' The default value for calldata and caller are symbolic values, but can be specialized to concrete functions with their corresponding flags. One can also specialize specific arguments to a function signature, while leaving others abstract. If --sig is given, calldata is assumed to be of the form suggested by the function signature. With this flag, specific arguments can be instantiated to concrete values via the --arg flag. This is best illustrated through a few examples: Calldata specialized to the bytestring 0xa9059cbb followed by 64 symbolic bytes: hevm symbolic --sig \"transfer(address,uint256)\" --code $(\" --arg 0 --code $(hevm test