Skip to content

Guide for running KEVM tests with custom backends

Jump to bottom
JKTKops edited this page Jul 29, 2021 · 4 revisions

Running Proofs Without Profiling

This page is written with the assumption that you want to profile the proofs you are running. If you only want to run the proofs with a custom version of the backend, follow steps 1, 2, 3, and 4, then make your target normally. Step 8 may help fix PATH-related errors.

Running Only One Proof With no Options to the Backend

  1. Clone the KEVM semantics repo but don't follow the build instructions there.
  2. cd into your clone of KEVM and do the following:
rm -r deps .build # if you've build KEVM in this folder before
make deps SKIP_HASKELL=true
make build -j4

Additionally, make sure your custom backend's executables are on your PATH. If your build of the backend is older than 04dd2a2 (Build with -eventlog by default, Jun 15 2021), you will also have to re-build it with the GHC option -eventlog.

  1. (Optional) Open the primary Makefile in a text editor. Change the variables TEST_CONCRETE_BACKEND and TEST_SYMBOLIC_BACKEND to have the value haskell like so:
# Tests
# -----

TEST_CONCRETE_BACKEND := haskell
TEST_SYMBOLIC_BACKEND := haskell
  1. Just to be sure, remove the executables kore-exec kore-format kore-parser kore-prof kore-repl from your standard frontend distribution so that the ones from your custom backend will be run instead.
  2. Put path/to/evm-semantics/.build/usr/bin on your PATH. If you need to edit the kevm script, you'll have to also rebuild KEVM, as that process copies ./kevm to .build/usr/bin/kevm.
  3. Identify the KEVM make target that you want to run. Run make target TEST_SYMBOLIC_BACKEND=haskell --dry-run.
  4. Copy the kevm command that make outputs. Run this command and add --profile. You can also add --profile-timeout <timeout-spec> and --kore-prof-args "..." to control timeouts and kore-prof. This will output an eventlog and a kore-prof'd .json file in the same directory as the proof's spec.
  5. If you see any error at any point about not being able to find one of the executables above, your backend executables aren't on your PATH. Run export PATH=$PATH:path/to/kore/.build/kore/bin replacing path/to/kore by the path to your custom clone of the repo. Remember that this will add the right executables to PATH for this terminal session only.

Multiple Proofs

If you want to run a whole suite, you can modify the Makefile's kevm invocations to add the --profile option.

Passing Options to the Backend

Be aware that the --haskell-backend-command option will mess with the profiling options passed to the backend by kevm. If you need to pass options to the backend, you'll probably be better off not using kevm's --profile option(s). To do this:

  1. Run env GHCRTS='-l' make target. This will output an eventlog in the current working directory (I think, so if you do this, please confirm and then update this page).
  2. Use kore-prof on that eventlog as needed.
  3. You may want to set that target to only one single test at a time (followed by a manual save of the eventlog/prof produced) rather than an entire test-suite as that might give back eventlogs/profiles that are mashed together.
Clone this wiki locally