Running Kontrol with custom evm-semantics/pyk

[ehildenb]

When developing python code for Kontrol, you usually may need a custom pyk or evm-semantics to run against. To do this, you need to modify pyproject.toml to point at the custom version.

In particular, you will need:

• A checkout of pyk, perhaps at /home/dev/src/pyk.
• A checkout of evm-semantics, perhaps at /home/dev/src/evm-semantics
• A checkout of kontrol, perhaps at /home/dev/src/kontrol.

NOTE: Make sure to follow all the steps of the build instructions on the README files of the pyk, evm-semantics and kontrol repos when first setting up your local working copies. In particular, make sure to install the dependencies, checkout the submodules and run the kdist commands to build the definitions. If you get errors when building one of the projects, go back and check if you didn't miss a step.

Then you need to:

• Modify evm-semantics to point at the custom pyk:

diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index 3c55a49ce..65f8ce137 100644
--- a/kevm-pyk/pyproject.toml
+++ b/kevm-pyk/pyproject.toml
@@ -13,7 +13,8 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.592" }
+pyk = { path = "/home/dev/src/pyk", develop = true }
 tomlkit = "^0.11.6"

 [tool.poetry.group.dev.dependencies]

• Ensure that evm-semantics builds correctly with this change: cd kevm-pyk && make
• Modify kontrol to point at the custom evm-semantics:

diff --git a/pyproject.toml b/pyproject.toml
index 601660d..65662b4 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -12,7 +12,8 @@ authors = [

 [tool.poetry.dependencies]
 python = "^3.10"
-kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.431", subdirectory = "kevm-pyk" }
+# kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.431", subdirectory = "kevm-pyk" }
+kevm-pyk = { path = "/home/dev/src/evm-semantics/kevm-pyk", develop = true }

 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

• Ensure that kontrol builds correctly with this change: make

Then, you should be all setup to work on Kontrol and make changes that may also require changes to KEVM and pyk.

[lucasmt]

• It might be necessary to run poetry update after editing the pyproject.toml files, although make may take care of that automatically.
• Use poetry run -- kontrol in your local checkout of kontrol to run the version with your custom changes (rather than the one installed through kup, for instance).

[anvacaru]

from @ehildenb You can add TEST_ARGS="--timemout 600" to a pytest command, for example, to tell it to timeout individual tests after 10 minutes. There isn't another way to timeout individual tests with timeout.

[anvacaru]

Running the kontrol test suite using docker containers to update the expected output

# from kontrol repo root, export aux vars

export K_VERSION=$(cat deps/k_release)
export Z3_VERSION=$(cat deps/z3)
export IMAGE_TAG="kontrol-image"

# FYI, docker might need sudo rights

# #clean first
# docker container stop kontrol-container
# docker container rm kontrol-container
# docker image rm ${IMAGE_TAG}

# build kontrol docker image
sudo docker build . --tag ${IMAGE_TAG} --build-arg K_VERSION=${K_VERSION} --build-arg Z3_VERSION=${Z3_VERSION}

#start a container using the newly created image
sudo docker run --name kontrol-container --rm --interactive --tty --detach --user root ${IMAGE_TAG}

#copy kontrol repo files to container
sudo docker cp . kontrol-container:/home/user/

# run poetry install in container
sudo docker exec kontrol-container /bin/bash -c 'poetry install'

#build kontrol from source in container
sudo docker exec kontrol-container /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'

#run test stage, with `--update-expected-output`
docker exec kontrol-container make cov-integration TEST_ARGS='--numprocesses=8 -vv -k "not test_kontrol_cse" -k "not test_foundry_minimize_proof" --update-expected-output'

#run test stage, with `--update-expected-output`
docker exec kontrol-container make cov-integration TEST_ARGS='--numprocesses=8 -vv -k "test_kontrol_cse" -k "test_foundry_minimize_proof" --update-expected-output'

#copy back files
docker cp kontrol-container:/home/user/src .