Skip to content

Guide for running KEVM tests with custom backends

Jump to bottom
JKTKops edited this page Jul 26, 2021 · 4 revisions
  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 https://github.com/kframework/kore/commit/04dd2a2f7662dfb6f27d31190d7046e78e2b0291, 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. 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.
  2. 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.
  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.

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

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

  1. Run env GHCRTS='-p -l-au' 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