ethereum/hevm

symbolic EVM evaluator

hevm

hevm is an implementation of the Ethereum virtual machine (EVM) made for symbolic execution, equivalence checking, and unit testing of smart contracts. hevm can symbolically execute smart contracts, run unit tests, and run arbitrary EVM code. It can run on state set up in a ds-test testing harness, or fetched on demand from live network using rpc calls.

hevm was originally developed as part of the dapptools project, and was forked to this repo by the formal methods team at the Ethereum Foundation in August 2022.

Documentation & Support

User facing documentation can be found in the hevm book.

We have a public matrix chat room here.

Installation

Static Binaries

Static binaries for x86 linux and macos are available for each release. These binaries expect to be able to find the following programs on PATH:

• solc
• z3
• (optionally) cvc5
• (optionally) bitwuzla

nixpkgs

hevm is available in nixpkgs, and can be installed via:

• flakes: nix profile install nixpkgs#haskellPackages.hevm
• legacy: nix-env -iA haskellPackages.hevm

nix flakes

hevm can be installed directly from the main branch of this repo via the following command:

nix profile install github:ethereum/hevm

Development

We use nix to manage project dependencies. To start hacking on hevm you should first install nix.

Once nix is installed you can run nix-shell (or nix develop if you use flakes) from the repo root to enter a development shell containing all required dev dependencies. If you use direnv, then you can run direnv allow, and the shell will be automatically entered each time you cd in the project repo.

Once in the shell you can use the usual cabal commands to build and test hevm:

$ cabal build          # build the hevm library
$ cabal build exe:hevm # build the cli binary
$ cabal build test     # build the test binary
$ cabal build bench    # build the benchmarks

$ cabal repl lib:hevm  # enter a repl for the library
$ cabal repl exe:hevm  # enter a repl for the cli
$ cabal repl test      # enter a repl for the tests
$ cabal repl bench     # enter a repl for the benchmarks

$ cabal run hevm       # run the cli binary
$ cabal run test       # run the test binary
$ cabal run bench      # run the benchmarks

# run the cli binary with profiling enabled
$ cabal run --enable-profiling hevm -- <CLI SUBCOMMAND> +RTS -s -p -RTS

# run the test binary with profiling enabled
$ cabal run --enable-profiling test -- +RTS -s -p -RTS

# run the benchmarks with profiling enabled
$ cabal run --enable-profiling bench -- +RTS -s -p -RTS

A high level overview of the architecture can be found in architecture.md.

hevm's Issues

Fully abstract VM

Some parts of the VM state are still concrete only. All data types should be an Expr instance, allowing for a completely symbolic execution environment.

For the case of gas, we can cheat a little and use a partially symbolic gas model (i.e. gas is either concrete, or unknown). This will allow us to support symbolic dynamic data without having to build a (slow & complex) symbolic gas model.

Update readme and docs to reflect new post dapptools reality

[Bug] Failed to install following command in Readme

I tried to install using nix profile install github:ethereum/hevm command from Readme file but it fails with the below message everytime. Failed on both Environments : Ubuntu 20.04.4 LTS and docker nixos/nix
Error message:

error: builder for '/nix/store/azhxxmjq083wpw82b6pc290vs86lwai5-hevm-0.50.0.drv' failed with exit code 1;
       last 10 log lines:
       >     eq-sol-exp-cex:                                  Equivalence checking 11 combinations
       > OK (0.09s)
       >     eq-all-yul-optimization-tests:                   FAIL
       >       Exception: solidity/test/libyul/yulOptimizerTests: getDirectoryContents:openDirStream: does not exist (No such file or directory)
       >       Use -p '/eq-all-yul-optimization-tests/' to rerun this test only.
       >
       > 1 out of 137 tests failed (434.31s)
       > Test suite test: FAIL
       > Test suite logged to: dist/test/hevm-0.50.0-test.log
       > 0 of 1 test suites (0 of 1 test cases) passed.

EOF

Assuming all client devs have a fully tested imentation of EOF in time for the next ACD call (Jan 5th), EOF will be included in the shanghai hardfork (march 2023).

This is the biggest change to the EVM in a while and will require non trivial changes on our side. It will also likely make symbolic analysis of EVM code significantly easier.

We should keep a watch on the implementation status and probably start working on support early next year if it's still on track for the shanghai hard fork then.

EOF spec: https://notes.ethereum.org/@ipsilon/eof1-unified-specification

December 8th ACD call summary: https://www.galaxy.com/research/insights/ethereum-all-core-developers-call-151/

Adapt `src/dapp-tests` to the new repo format

The integration tests in src/dapp-tests should be adapted to the new repo format. Ideally we would just run these using the normal haskell testing infrastructure.

Fix `prove_loop` in `dsProvePass`

This test will only pass with some maxIter set. We should hook up the maxIter setting and make sure it is respected when executing prove tests.

Replace Arrays With Uninterpreted Functions in the SMT encodings

We currently use nested and constant arrays which severly limits the solvers we can use (currenlty only Z3). If we instead use UF's with axioms, we can use cvc5, bitwuzla, yices and stp, all of which should be more performant than Z3.

Static Binaries for MacOS

Running nix-build on macos currently fails with:

> ld: library not found for -lm
> clang-11: error: linker command failed with exit code 1 (use -v to see invocation)
> `cc' failed in phase `Linker'. (Exit code: 1)

This seems to related to: https://github.com/NixOS/nixpkgs/blob/master/pkgs/os-specific/darwin/apple-source-releases/Libm/default.nix.

We should fix this and start producing static binaries for macos (ideally both aarch64 and x86_64).

SMT: Display Counterexamples for Storage

We model storage in SMT as a nested array:

  (define-sort Storage () (Array Word (Array Word Word)))

Where the key of the outer array is an address, and the key on the inner array is a storage slot.

When producing models for a given Storage instance, the solver will often return an array defined using as_const (meaning every key is mapped to the same value). Since there are 2^512 values in a given storage array, it is not possible to store such a response using e.g. a haskell Map instance.

In order to present useful counterexamples for storage to users, we will probably need to do some kind of analysis over an Expr instance to determine which storage values are actually read in any given program, and then generate individual counterexamples for each storage read (similar to the procedure we use for generating keccak constraints).

Better counterexamples & logging for prove tests

The output from the prove test runner is currently not super friendly. We should build a nice counterexample string that can be pasted directly into a solidity test file, as well as displaying the execution trace from that branch.

Move to using API for SMT solvers instead of using their textual interface

We shouldn't be calling SMT solvers through their text interfaces. Instead, we should be using their APIs. We could use:

https://github.com/stanford-centaur/smt-switch

to have a single API for different SMT solvers. However, to make a Haskell binding for it, we'd need a (minimal) C API for smt-switch. It's not too hard to do. One template is: https://github.com/meelgroup/breakid/blob/master/src/breakid_c.h (and associated https://github.com/meelgroup/breakid/blob/master/src/breakid_c.cpp ). These two make a C API from a C++ API, with minimal work.

Dump SMT Queries From Test Suite in SMTComp Format

We are collaborating with the centaur lab at stanford (developers of cvc5 & bitwuzla), and we need to produce a set of benchmarks that they can use to start optimising cvc5 / bitwuzla for our use case.

We should start by dumping all the queries from our existing test suite in a format as close to the SMTComp format as possible and put them into a separate git repo that we can give to stanford.

Ideally this procedure should be automated within hevm so we can easily update the bechmark repo as the test suite expands.

Incorrect logs emitted when downcasting to `bytes2` or `bytes1`

I initially submitted this issue to the Trail of Bits Echidna repo.

What is the problem?

Logs emitted by dapp test -vvv are incorrect when downcasting from bytes32 to bytes2 or bytes1.

Here is an example test that showcases this issue (you can find the repository on my GitHub):

contract WeirdLogsTest is DSTest {
    // This is the default Echidna contractAddr
    // see: https://github.com/crytic/echidna/wiki/Config
    address weirdLogs = address(0x00a329c0648769A73afAc7F9381E08FB43dBEA72);

    bytes32 originalHash = keccak256(abi.encodePacked(weirdLogs));

    event OriginalHash(bytes32 originalHash);
    event HashCastedToBytes16(bytes16 originalHash);
    event HashCastedToBytes8(bytes8 originalHash);
    event HashCastedToBytes4(bytes4 originalHash);
    event HashCastedToBytes3(bytes3 originalHash);
    event HashCastedToBytes2(bytes2 originalHash);
    event HashCastedToBytes1(bytes1 orignalHash);

    function test_always_false() public {
        emit OriginalHash(originalHash);
        emit HashCastedToBytes16(bytes16(originalHash));
        emit HashCastedToBytes8(bytes8(originalHash));
        emit HashCastedToBytes4(bytes4(originalHash));
        emit HashCastedToBytes3(bytes3(originalHash));
        emit HashCastedToBytes2(bytes2(originalHash));
        emit HashCastedToBytes1(bytes1(originalHash));
        assert(false);
    }
}

Running this test with dapp test -vvv results in the following output:

Running 1 tests for src/WeirdLogs.t.sol:WeirdLogsTest
[BAIL] test_always_false()

Failure: test_always_false
  src/WeirdLogs.t.sol:WeirdLogsTest
   ├╴constructor
   └╴test_always_false()
      ├╴OriginalHash(0x6662c13a7c344b8f8c0c3d766a8b6ca60a12a25c96208453b9bb163d6c8ecb56) (src/WeirdLogs.t.sol:24)
      ├╴HashCastedToBytes16(0x6662c13a7c344b8f8c0c3d766a8b6ca6) (src/WeirdLogs.t.sol:25)
      ├╴HashCastedToBytes8(0x6662c13a7c344b8f) (src/WeirdLogs.t.sol:26)
      ├╴HashCastedToBytes4(0x6662c13a) (src/WeirdLogs.t.sol:27)
      ├╴HashCastedToBytes3(0x6662c1) (src/WeirdLogs.t.sol:28)
      ├╴HashCastedToBytes2(«fb») (src/WeirdLogs.t.sol:29)
      ├╴HashCastedToBytes1(«f») (src/WeirdLogs.t.sol:30)
      └╴error Revert 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 <source not found>

The last two logs (HashCastedToBytes2 and HashCastedToBytes1) print values «fb» and «f». This is not the correct result.

I've created the same example in Foundry and this is the result of running forge test -vvv:

Running 1 test for test/WeirdLogs.t.sol:WeirdLogsTest
[FAIL. Reason: Assertion violated] test_always_false() (gas: 10386)
Traces:
  [10386] WeirdLogsTest::test_always_false() 
    ├─ emit OriginalHash(originalHash: 0x6662c13a7c344b8f8c0c3d766a8b6ca60a12a25c96208453b9bb163d6c8ecb56)
    ├─ emit HashCastedToBytes16(originalHash: 0x6662c13a7c344b8f8c0c3d766a8b6ca6)
    ├─ emit HashCastedToBytes8(originalHash: 0x6662c13a7c344b8f)
    ├─ emit HashCastedToBytes4(originalHash: 0x6662c13a)
    ├─ emit HashCastedToBytes3(originalHash: 0x6662c1)
    ├─ emit HashCastedToBytes2(originalHash: 0x6662)
    ├─ emit HashCastedToBytes1(orignalHash: 0x66)
    └─ ← "Assertion violated"

Test result: FAILED. 0 passed; 1 failed; finished in 242.42µs

Failing tests:
Encountered 1 failing test in src/WeirdLogs.sol:WeirdLogs
[FAIL. Reason: Assertion violated] test_always_false() (gas: 10386)

As you can see, the result for the last two logs is correct: 0x6662 and 0x66, respectively.

As mentioned in #crytic/echidna/issues/860 this might already be fixed in the EF HEVM repository.

Thanks!

Foundry Integration

We should be able to run hevm from the top level of a foundry project and execute all discovered unit tests (both concrete and symbolic).

The required work items here are roughly:

1. adapt hevm to understand the foundry directory structure
2. adapt hevm to understand the foundry solc output
3. add all new foundry cheatcodes (or at least the most used ones)

Fix counterexample generation

With this diff:

+        testCase "assert-fail" $ do
+          Just c <- solcRuntime "AssertFail"
+            [i|
+            contract AssertFail {
+              function fun(uint256 deposit_count) external pure {
+                assert(deposit_count == 1);
+                assert(deposit_count == 0);
+              }
+             }
+            |]
+          putStrLn "-----------------------\n"
+          [Cex a, Cex b] <- withSolvers Z3 1 $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) []
+          print a
+          print b
+          putStrLn "expected counterexample found"
+        ,

We get two counterexamples for the two asserts,but instead of the value, we get an error:

(Revert (ConcreteBuf "NH{q\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\SOH"),["((txdata ((as const (Array (_ BitVec 256) (_ BitVec 8))) #x00)))\n","(error \"line 179 column 12: unknown constant storage\")\n"])

(Revert (ConcreteBuf "NH{q\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\SOH"),["((txdata ((as const (Array (_ BitVec 256) (_ BitVec 8))) #x00)))\n","(error \"line 357 column 12: unknown constant storage\")\n"])

The Counterexample requesting is incorrect and so we get an error instead of a value.

Notes

Apparently, counterexample generation is in checkSat' in SMT.hs.

Better error handling

NOTE: This is an issue to store some accumulated knowledge and keep a record of where we are at. Not some must-do/etc.

Perhaps we could do better error handling in HEVM. There seem to be two types of errors/failres in HEVM, which is also slightly confusing.

In Types.hs:

-- EVM errors
data Error
  = Invalid
  | IllegalOverflow
  | StackLimitExceeded
  | InvalidMemoryAccess
  | BadJumpDestination
  | StackUnderrun
  | SelfDestruct
  | TmpErr String
  deriving (Show, Eq, Ord)

Notice the TmpErr which can hide quite a bit of stuff.

And one in EVM.hs, here:

-- | EVM failure modes
data Error
  = BalanceTooLow W256 W256
  | UnrecognizedOpcode Word8
  | SelfDestruction
  | StackUnderrun
  | BadJumpDestination
  | Revert (Expr Buf)
  | OutOfGas Word64 Word64
  | BadCheatCode (Maybe Word32)
  | StackLimitExceeded
  | IllegalOverflow
  | Query Query
  | Choose Choose
  | StateChangeWhileStatic
  | InvalidMemoryAccess
  | CallDepthLimitReached
  | MaxCodeSizeExceeded W256 W256
  | InvalidFormat
  | PrecompileFailure
  | forall a . UnexpectedSymbolicArg Int String [Expr a]
  | DeadPath
  | NotUnique (Expr EWord)
  | SMTTimeout
  | FFI [AbiValue]
  | NonceOverflow
deriving instance (Show) Error
instance Exception Error

Notice that the text here is a bit misleading, because UnexpectedSymbolicArg is not actually an EVM failure mode, it's an HEVM failure mode, I think? There is also quite a bit of overlap, though TmpErr is missing from the second one. Not sure if this is ideal, perhaps better comments would be helpful, or perhaps they could be merged(?).

When fuzzing, e.g. the flattenExpr will error with UnexpectedSymbolicArg quite often, which really ought not to be caught. However, as discussed with David, doing throw & catch may also not be ideal (though could be done by making these Error-s instance of Exception from Control.Exception. Likely we should use Either, instead of using exceptions.

Adapt unit testing framework for Expr

UnitTest.hs does not currently compile with the new Expr reality. Fix this :)

Move to nix flakes

We should modernize the nix infra here by moving to nix flakes

UnitTest: Display traces for failing prove tests

We should display the traces for failing prove tests as we do for failing concrete tests. To do this we will need to add a field to Expr End leaf types that contains the contents of the traces field in the VM type and then display this as part of symFailure in UnitTest.hs.

Fix parsing of Cex-s

The Cex-s should look like:

calldata: 0x123134234243

storage:

  0xfffff:
    0: 0x01

block context:

  timestamp: 12343428942

tx context:

  value: 101010

[note: tx.origin -> top level transaction signer]

This requires passing to checkSat a datastruct like:

data Cex = Cex
  { calldata: String
  , storage: [String]
  , blockContext: [String]
  , txContext: [String]
  }

Basically:

1. build a structured representation of variable names that we want to get values for
2. pass this into checkSat
3. if we get Sat, then we read all these values, and parse them into some human readable form
4. pass back the parsed values as part of the return value from checkSat

Useful links:

https://hackage.haskell.org/package/smt2-parser
https://github.com/crvdgc/smt2-parser/blob/master/src/Language/SMT2/Syntax.hs
https://github.com/crvdgc/smt2-parser/blob/5abbc3e8c021b572b3b157b12be14b80a6485f3f/src/Language/SMT2/Syntax.hs#L244

Clash with reserved word in `AbstractBuf` leads to SMT2 error

Example to reproduce is to go into cabal repl test and then:

a = ReadWord (Lit 0x18) (AbstractBuf "as")
b = ReadWord (Lit 0x32) (AbstractBuf "bimm")
checkEquiv a b
Error "Unable to parse solver output: (error \"line 225 column 16: invalid constant declaration, symbol expected\")"

Notice the AbstractBuf "as" which is what triggers the error. What happens in the SMT2 is that we have a buffer declared as:

(declare-const as (Array (_ BitVec 256) (_ BitVec 8)))

But as is a reserved word in SMT2. This could happen with others, e.g. buffer, or select etc. We likely want to have them numbered. I'll try to fix this and see how it goes :)

Not a huge blocker, just a minor bug. It was found by quickcheck, actually. One of the builds failed and I was curious why.

Move src/hevm to the top level

We only have hevm in this repo now, so we can just move it to the top level of the repo and not have to always cd src/hevm....

SMT: counterexample shrinking

Currently we often get counterexamples for the calldata buffer back from the solver that are too large to represent in a haskell ByteString.

If we encounter such a case, we should implement some form of counterexample shrinking, until we get a result that is small enough to be presented to users.

Update symbolic unit tests for Expr compatibility

Many of the hevm unit tests are currently still written for the old symbolic execution backend, we should finish updating them all to run with the new backend

Fuzz tests for equivalence checker

We can fuzz the equivalence checker (and the solc optimizer) by:

1. generating random yul
2. running the optimizer on it
3. compile both optimized & unoptimized yul to bytecode and run the equivalence checker

[Bug] hevm: UnexpectedSymbolicArg

I tried to run the --get-models option of hevm 0.5. However, the below error happens. It works fine on the last release though (hevm/0.48.1).
The contract:

pragma solidity ^0.8.0;
contract Branching {
    function test(uint input) public payable{
        require (input*2 == 8888888888 && msg.value  == 12345);
        payable(msg.sender).transfer(1 ether);
    }
}

I get bin-runtime from the above source code and run the command:

hevm symbolic --code 0x60806040526004361061001e5760003560e01c806329e99f0714610023575b600080fd5b61003d600480360381019061003891906100d0565b61003f565b005b640211d1ae3860028261005291906100f9565b148015610060575061303934145b61006957600080fd5b3373ffffffffffffffffffffffffffffffffffffffff166108fc670de0b6b3a76400009081150290604051600060405180830381858888f193505050501580156100b7573d6000803e3d6000fd5b5050565b6000813590506100ca8161018c565b92915050565b6000602082840312156100e257600080fd5b60006100f0848285016100bb565b91505092915050565b600061010482610153565b915061010f83610153565b9250817fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff04831182151516156101485761014761015d565b5b828202905092915050565b6000819050919050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b61019581610153565b81146101a057600080fd5b5056fea2646970667358221220beda54481fd74ab8985de2ba16205888ed0d8015f70eded76b7d5a8565affbf264736f6c63430008000033 --get-models
Exploring contract
Simplifying expression
Explored contract (8 branches)
hevm: UnexpectedSymbolicArg 161 "cannot delegateCall with symbolic target or context" [And (Lit 0xffffffffffffffffffffffffffffffffffffffff) (Caller 0),And (Lit 0xffffffffffffffffffffffffffffffffffffffff) (Caller 0)]
CallStack (from HasCallStack):
  error, called at src/EVM/SymExec.hs:363:21 in hevm-0.50.0-inplace:EVM.SymExec

Fix rpc regressions and add test harness for remote state fetching

We should add some tests that exercise the remote state features, and fix any regressions that we discover.

Eliminate `fromIntegral`

We currently make extensive use of fromIntegral (aliased to num). Which will happily downcast from larger types to smaller ones without warning. This has been a source of quite a few overflow issues (and presumably there are many more latent ones hiding in the codebase).

We should:

1. Introduce (or find) some conversion routines that allow unchecked upcasting only
2. Introduce (or find) some conversion routines for checked downcasting

replace all uses of fromIntegral and num with instances of the above routines.

Adapt equivalence checker to Expr and integrate it's test suite into Tasty

Set up benchmarks

We need a solid set of symbolic benchmarks that we can use to optimize our simplification pipeline & smt encoding

Fix `testbadFFI()` in `cheatCodes.sol`

The testBadFFI() function is currently failing due to an unexpected internal exception. We should fix it.

Update for merge hardfork

Investigate which (if any) changes to hevm will be required to remain compatible post merge

Integrate SMTChecker tests into Tasty

There are a set of tests that compare the SMTChecker to hevm symbolic under nix/hevm-tests/smt-checker.nix. The test harness should be adapted so it can be run directly from tasty, instead of via the nix harness that currently exists.

Fix static binaries

The build for the static binaries (run nix-build from the repo root) currently fails.

Adapt debugger to use Expr

Polish documentation

We should expand and polish our documentation site (especially by filling out the currently missing tutorials)

Starting REPL fails on MacOS

Starting a REPL instance on MacOs 12.4 fails with the following error

[nix-shell:~/Repos/hevm/src/hevm]$ cabal v2-repl
Build profile: -w ghc-9.0.2 -O1
In order, the following will be built (use -v for more details):
 - hevm-0.49.0 (lib) (ephemeral targets)
Preprocessing library for hevm-0.49.0..
GHCi, version 9.0.2: https://www.haskell.org/ghc/  :? for help
<command line>: User-specified static library could not be loaded (/nix/store/gvhyj1bb5p0dcz2rhxbfgi8p49xwaz11-clang-wrapper-11.1.0/bin/c++)
Loading static libraries is not supported in this configuration.
Try using a dynamic library instead.

cabal: repl failed for hevm-0.49.0.

but cabal v2-build seems to be working fine.

Also cabal v2-build test fails with

ghc: loadArchive: Neither an archive, nor a fat archive: `/nix/store/gvhyj1bb5p0dcz2rhxbfgi8p49xwaz11-clang-wrapper-11.1.0/bin/clang++'
ghc: panic! (the 'impossible' happened)
  (GHC version 9.0.2:
	loadArchive "/nix/store/gvhyj1bb5p0dcz2rhxbfgi8p49xwaz11-clang-wrapper-11.1.0/bin/clang++": failed

Integrate VMTests into Tasty

We should run the full set of state tests in ethereum/tests as part of CI.

Make ethereum tests pass

• Hook up the hevm compliance cli endpoint
• Run all the VM Tests
• Fix all failures

`cabal run hevm` out of gas error bug

bash run cabal run -- hevm -- exec --code 0x647175696e6550 --gas 0xffffffff --state ./mystate --debug
but got error Out of gas 0 3

debug showed gas = 0, it seems like command --gas 0xffffffff didn't work. plz tell me how to fix it, thanks!

keccak of `abi.encodePacked` of string works for memory but not for storage

This:

            contract A {
              function f(uint x) external {
                string memory a;
                assert(keccak256(abi.encodePacked(a)) == keccak256(abi.encodePacked(a)));
              }
            }

works and we get a QED. But:

            contract A {
              string a;
              function f(uint x) external {
                assert(keccak256(abi.encodePacked(a)) == keccak256(abi.encodePacked(a)));
              }
            }

hangs right after Exploring contract from:

  putStrLn "Exploring contract"

  exprInter <- evalStateT (interpret (Fetch.oracle solvers rpcinfo) (maxIter opts) (askSmtIters opts) runExpr) preState
  when (debug opts) $ T.writeFile "unsimplified.expr" (formatExpr exprInter)

  putStrLn "Simplifying expression"

As discussed with @zoep

Calls Into Unknown Code (Overapproximated)

We currently don't handle calls into unknown code. One relatively easy way to deal with this would be to:

1. replace the result of the call with an abstract term (i.e. one of the *Call expr terms)
2. after the call, replace the returndata buffer with a fully abstract buf
3. after the call, reset parts of the state that could have been affected (e.g. storage, gas, balances, nonces, ...) to a fully abstract state
4. continue execution

Note that this is an overaproximation, and could produce spurious counterexamples e.g. in the case that some parts of the contract state are protected by a mutex.

A more refined analysis could conditionally reset parts of the state that can be shown to be touched by a reentrant call. An example of such a routine is here: ethereum/act#18

Simplification seems incorrect on a specific query

In current main, rev ad3265f we have:

ghci> a = ReadByte (Lit 0x12) (CopySlice (Lit 0xc) (ReadWord (Lit 0xb) (CopySlice (Lit 0x29) (Lit 0x3a) (Lit 0x63) (ConcreteBuf "\t2\190\FS\242\140\176\174~\235\ETB\134\147\218\128\224\208:\179@\163\242V\188\138\189B\174\156\185\182\138") (ConcreteBuf "\242\213\191\SUB)\218\140\178L\206a\r\180]>\168\203W\215\139X\239E\255\194"))) (Lit 0x41) (ConcreteBuf "\233\195r(\238\154\235") (ConcreteBuf "\DEL<?\ESC\160\EM\146d\186 \148\181\auz\182.\243 9\b\210\173,\141\&7\215\237\228\a;\210\\^.7p\252h\204\193@j\132\147\194\145iu\192Gp\"/\ESCPrQ\216\129\246\179\128\192b\a\198\171\226\155\146N\FSX\240ky\RS"))
ghci> checkEquiv a (Expr.simplify a)
Sat (SMTCex {calldata = fromList [], storage = "", blockContext = "", txContext = ""})
False

This triggered on my PR that does something different. Saving it here so we can get back to it. NOTE, it also works with:

a = ReadByte (Lit 0x12) (CopySlice (Lit 0xc) (ReadWord (Lit 0xb) (CopySlice (Lit 0x29) (Lit 0x3a) (Lit 0x63) (ConcreteBuf "") (ConcreteBuf "abcdefaaaaaaaaaaaaaaaaaa"))) (Lit 0x41) (ConcreteBuf "") (ConcreteBuf "abcdefaaaaaaaaaaaaaaaaaa"))

Also by this (smaller):

a = ReadByte (Lit 0x12) (CopySlice (Lit 0xc) (ReadWord (Lit 0xb) (CopySlice (Lit 0x29) (Lit 0x3a) (Lit 0x63) (ConcreteBuf "abcdefa") (ConcreteBuf "abcdefaaaaaaaaaaaaaaaaaa"))) (Lit 0x41) (ConcreteBuf "") (ConcreteBuf "abcdefaaaaaaaaaaaaaaaaaa"))

Even smaller:

a = ReadByte (Lit 0x12) (CopySlice (Lit 0xc) (Lit 0x6161616161616161616161616100000000000000000000000000000000000000) (Lit 0x41) (ConcreteBuf "") (ConcreteBuf "abcdefaaaaaaaaaaaaaaaaaa"))

---

This crashes the repl:

a = ReadByte (Lit 0x12) (CopySlice (Lit 0xc) (Lit 0x1000000000) (Lit 0x41) (ConcreteBuf "") (ConcreteBuf "abcdefaaaaaaaaaaaaaaaaaa"))
Expr.simplify a

And this causes heap overflow:

a = ReadByte (Lit 0x12) (CopySlice (Lit 0xc) (Lit 0x1000000000000000) (Lit 0x41) (ConcreteBuf "") (ConcreteBuf "abcdefaaaaaaaaaaaaaaaaaa"))
simplify a

And this is wrong:

a = ReadByte (Lit 0x12) (CopySlice (Lit 0xc) (Lit 0x10000000000000000000000) (Lit 0x41) (ConcreteBuf "") (ConcreteBuf "abcdefaaaaaaaaaaaaaaaaaa"))
checkEquiv a (Expr.simplify a)

Mate

Advanced Fuzzing Pipelines

Just noting some ideas that @msooseth and I discussed for nice fuzzing pipelines that we could write if had an Expr -> EVM compiler.

Compiling an Expr End into EVM bytecode should be fairly simple, especially if we produce yul instead of bytecode directly. Each ITE can be an if-then-else block, and translating return / revert leaves into return / revert statements in yul shouldn't be too hard.

Concrete Evaulation vs Geth

1. Generate a random Expr End
2. Compile that into evm
3. Execute both against some concrete input value and compare the result

This would test our smt encoding to make sure that it matches the concrete semantics (we could use the concrete semantics from hevm or from geth).

Symbolic Exec vs Equivalence Checker

1. Generate random bytecode
2. Symbolically exec to produce an Expr
3. Compile the Expr into EVM
4. Run the equivalence checker against both

This would test the symbolic execution engine (and Expr -> EVM compiler) against the equivalence checker.

Add json tracing endpoint back to the cli

We are still missing the --json-trace cli flag when running hevm exec

Benchmarking

We should add a set of benchmark tests that give us a good base to start optimizing both concrete and symbolic execution.

For concrete execution, the VMTests should serve as a good starting point.
For symbolic execution, we should use a set of interesting real world contracts (e.g. an ERC20, the deposit contract, the Vat from maker).

Adapt `nix/hevm-tests` to new repo format

The tests for hevm in nix/hevm-tests should be adapted to the new repo format. Ideally we would remove the nix dependency here and just run these using the usual haskell testing infrastructure.

Fix all compiler warnings and enforce a clean compilation in CI

We currently have tons of compiler warnings when building. Some of these are trivial, and some are important. main should always compile without warnings and we should enforce that in CI.

`indexWordN` potential issue

Prelude on Endianness

EVM is big-endian (Yellow Paper, Appendix H:: "When interpreting 256-bit binary values as integers, the representation is big-endian."). So MSB is rightmost byte (not leftmost, as in x86). However, my understanding is that bitvectors in SMT are little-endian (i.e. MSB is leftmost byte).

The BYTE instruction

The 0x1A (i.e. BYTE) opcode says at https://ethervm.io/#1A : "ith byte of (u)int256 x, counting from most significant byte". Notice that to get MSB, you'd need to pass 0 here.

This is where this gets ingested in EMV.hs:

        0x1a -> stackOp2 (const g_verylow) (\(i, w) -> Expr.padByte $ Expr.indexWord i w)

Now, this gets translated to IndexWord, eventually in Expr.hs:

indexWord idx w = IndexWord idx w

Which then becomes:

IndexWord w idx -> case idx of
    Lit n -> if n >= 0 && n < 32
             then do
              enc <- exprToSMT w
              pure $ "(indexWord" <> (T.pack . show $ n) <> " " <> enc <> ")"

Which then is defined in the prelude in SMT.hs as:

  ; word indexing
  (define-fun indexWord0 ((w Word)) Byte ((_ extract 7 0) w))
  (define-fun indexWord1 ((w Word)) Byte ((_ extract 15 8) w))
  (define-fun indexWord2 ((w Word)) Byte ((_ extract 23 16) w))
  (define-fun indexWord3 ((w Word)) Byte ((_ extract 31 24) w))
[etc]

Hence, BYTE 0, VAL will get translated to roughly indexWord0 val, but in SMT that's the LSB, not the MSB, right?

Other uses of indexWord/IndexWord

All other uses of Indexword/indexWord seem fine, though, given the above setup:

MSTORE8 usage

MSTORE8 in EVM.hs:

        -- op: MSTORE8
        0x53 ->
          case stk of
            (x':y:xs) -> forceConcrete x' "MSTORE8" $ \x ->
              burn g_verylow $
                accessMemoryRange fees x 1 $ do
                  let yByte = indexWord (Lit 31) y

Here, (Lit 31) will extract the LSB 8 bits in the current interpretation.

readByte usage

Similarly, readByte in Expr.hs:

readByte i@(Lit x) (WriteWord (Lit idx) val src)
  = if idx <= x && x <= idx + 31
    then case val of
           (Lit _) -> indexWord (Lit $ x - idx) val
           _ -> IndexWord (Lit $ x - idx) val

If x=idx=0 and write to EmptyBuf, we have: readByte (Lit 0) (WriteWord (Lit 0) val EmptyBuf), which results in indexWord (Lit 0) val -- which is the MSB in our current interpretation, and that's correct, that's the 1st byte, since EVM is big-endian.

writeWord usage

indexWord is also used in the definition of writeWord. This currently matches that of indexWord, so in the current implementation, seems good.

Hook up CLI interface to match existing behaviour

Much of hevm-cli.hs still needs to be adapted to the new Expr format. We should retain backwards compatibility here.