Symbolic Execution Tutorial

Symbolic execution mode of hevm checks whether any call to the contract could result in an assertion violation. Let's see a simple contract, in file contract-symb-1.sol:

//SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract MyContract {
  function simple_symb() public pure {
    uint i;
    i = 1;
    assert(i == 2);
  }
}

Let's first compile it with solc:

$ solc --bin-runtime contract-symb-1.sol
======= contract-symb-1.sol:MyContract =======
Binary:
6080604052348015600e575f80f....

Now let's symbolically execute it:

$ hevm symbolic --sig "simple_symb()" --code "6080604052348015...."

Discovered the following counterexamples:

Calldata:
  0x881fc77c

Storage:
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0

Symbolically executing a specific function

When there are more than one functions in the code, the system will try to symbolically execute all. Let's take the file contract-symb-2.sol:

//SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract MyContract {
  uint i;
  function simple_symb1() public view {
    assert(i == 2);
  }
  function simple_symb2() public view {
    assert(i == 3);
  }
}

And compile it with solc:


$ solc --bin-runtime contract-symb-2.sol

======= contract-symb-2.sol:MyContract =======
Binary of the runtime part:
6080604052348015600e57....

Now execute the bytecode symbolically with hevm:

$ hevm symbolic --code "608060405234...."

Discovered the following counterexamples:

Calldata:
  0x85c2fc71

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x0)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0


Calldata:
  0x86ae3309

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x0)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0

Notice that hevm discovered two issues. The calldata in each case is the function signature that cast from foundry gives for the two functions:

$ cast sig "simple_symb1()"
0x85c2fc71

$cast sig "simple_symb2()"
0x86ae3309

In case you only want to execute only a particular function, you can ask hevm to only execute a particular function signature via the --sig option:

$ hevm symbolic --sig "simple_symb1()" --code "6080604052348015600...."


Discovered the following counterexamples:

Calldata:
  0x85c2fc71

Storage:
  Addr SymAddr "entrypoint": [(0x0,0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Abstract versus empty starting storage

The initial store state of hevm is completely abstract. This means that the functions are explored for all possible values of the state. Let's take the following contract contract-symb-3.sol:

//SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract MyContract {
  uint i;
  function simple_symb() public view {
    assert(i == 0);
  }
}

Let's compile with solc:

solc --bin-runtime contract-symb-3.sol

======= contract-symb-3.sol:MyContract =======
Binary of the runtime part:
6080604052348015600e575f80fd5b50600436106026575f3560e01c806388....

With default symbolic execution, a counterexample is found:

$ cabal hevm symbolic --initial-storage Empty --code "60806040523...."

Discovered the following counterexamples:

Calldata:
  0x881fc77c

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x1)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0

However, notice that the counterexample has 1 as the value for i storage variable. However, this contract can never actually assign i to any value. Running this contract with --initial-state Empty ensures that the default value, 0, is assigned, and the assert can never fail:

cabal run exe:hevm -- symbolic --initial-storage Empty --code "60806040...."

QED: No reachable property violations discovered

Here, no counterexamples are discovered, because with empty default state, the value of i is zero, and therefore assert(i == 0) will all never trigger.

Using forge to build your project for symbolic execution

Forge can also be used to build your project and run symbolic execution on it. This fits in well with standard development practices. You can use forge to build and then jq to extract the runtime bytecode. Let's say we have the following contract:

contract AbsStorage {
    uint256 public a;
    function not2() public {
      assert(a != 2);
    }
}

Notice that this contract cannot set a to 2, hence the assert will never fail in the real world. However, in symbolic mode, hevm allows the state to be symbolic, hence it can explore all possible values of a, even ones that are not possible in the real world. Let's compile this contract with forge and then run symbolic execution on it:

$ forge build --ast
[⠒] Compiling...
[⠢] Compiling 1 files with Solc 0.8.19
[⠆] Solc 0.8.19 finished in 11.46ms

$ hevm symbolic --code $(jq -r '.deployedBytecode.object' out/abs_storage.sol/AbsStorage.json )
Discovered the following 1 counterexample(s):

Calldata:
  0xb1712ffd

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x2)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0

The calldata provided by hevm is the function signature of not2(). This can be checked via cast, which is installed as part of foundry:

cast keccak "not2()"
0xb1712ffd...

We can get all the details of the state and context led to the counterexample by using the --get-models flag. While there will be a number of branches displayed, only one will be relevant to the counterexample. Here is the relevant branch:

=== Models for 8 branches ===
[...]

--- Branch ---

Inputs:

  Calldata:
    0xb1712ffd

  Storage:
    Addr SymAddr "entrypoint": [(0x0,0x2)]

  Transaction Context:
    TxValue: 0x0


End State:

  (Failure
    Error:
      (Revert
        (ConcreteBuf
          Length: 36 (0x24) bytes
          0000:   4e 48 7b 71  00 00 00 00  00 00 00 00  00 00 00 00   NH{q............
          0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
          0020:   00 00 00 01                                          ....
        )
      )
      [...]

Here, the storage variable is set to 2, which is the value that the assert tested for. Notice that the panic exception is of type 01, which is what's expected for an assert failure in solidity.