-
Notifications
You must be signed in to change notification settings - Fork 45
Guide for running KEVM tests with custom backends
JKTKops edited this page Jul 26, 2021
·
4 revisions
- Clone the KEVM semantics repo but don't follow the build instructions there.
-
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
.
- (Optional) Open the primary Makefile in a text editor. Change the variables
TEST_CONCRETE_BACKEND
andTEST_SYMBOLIC_BACKEND
to have the valuehaskell
like so:
# Tests
# -----
TEST_CONCRETE_BACKEND := haskell
TEST_SYMBOLIC_BACKEND := haskell
- Put
path/to/evm-semantics/.build/usr/bin
on yourPATH
. If you need to edit thekevm
script, you'll have to also rebuild KEVM, as that process copies./kevm
to.build/usr/bin/kevm
. - 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. - Identify the KEVM
make
target that you want to run. Runmake target TEST_SYMBOLIC_BACKEND=haskell --dry-run
. - 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 andkore-prof
. This will output an eventlog and akore-prof
'd.json
file in the same directory as the proof's spec. - 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
. Runexport PATH=$PATH:path/to/kore/.build/kore/bin
replacingpath/to/kore
by the path to your custom clone of the repo. Remember that this will add the right executables toPATH
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:
- 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). - Use
kore-prof
on that eventlog as needed. - 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.