This project implements the tools for symbolically executing programs in languages specified using the K Framework. The symbolic execution is performed at the level of Kore --- an intermediate representation produced by the K compiled from a language specification.
The K framework is a term rewriting-based specification language, and therefore its symbolic execution backend implements a symbolic term rewriter. Such a rewriter is implemented by the kore-rpc-booster executable --- a JSON RPC-based server that implements the KORE RPC protocol.
The kore-rpc executable is a legacy version of the RPC-based rewriter that implements the same protocol. Finally, kore-exec and kore-repl are the deprecated non-RPC entry points.
Note that this project is low-level and is not intended to be a user-facing tool. For the Python-based theorem prover based on the KORE RPC protocol, see the pyk package in the K Framework repository.
The kore-rpc-booster binary takes a kore file definition, parses and internalises it and then launches an RPC server, which executes requests agains this definition. It additionally accepts a path to a dynamic library compiled by the LLVM backend, which is used for simplification of bool sorted terms. In order to build the kore definition and the shared library out of a K definition, first call
kompile --llvm-kompile-type c my_defintion.k
and then launch the server via
kore-rpc-booster ./my_defintion-kompiled/definition.kore --module MY-DEFINITION --llvm-backend-library ./my_defintion-kompiled/interpreter
Besides git, you will need stack or cabal to build the project.
stack build all
# or
cabal build allYou may pass --fast to stack build or -O0 to cabal build in order to
disable compiler optimizations and make build faster at the cost of slower runtime.
Developers will require all the dependencies listed above, in addition to the requirements and recommendations below.
For integration testing, we require:
- GNU make
- The K Framework frontend (its version should be the one stated in /deps/k_release)
- Python 3.x with the
jsonrpcclientlibrary installed
You can install/have access to K by either:
- using kup
- using a pre-built binary (see the releases page in the K repository)
- if you use Nix, see the section below
- or by just building K from source
For setting up a development environment, we recommend:
- direnv to make the project's tools available in shells and editors.
- ghcup or Nix for managing required Haskell tooling
- hlint and fourmolu for compliance with project guidelines.
ghcup provides a straightforward way of installing the language server, if you prefer to use Nix please refer to the relevant resources on how to set up your Nix environment to build the server. Note: HLS has to be built with the project's GHC version.
Prequisite: build the project with either Stack or Cabal.
Instructions on integrating with VSCode:
- Install the Haskell extension
- Go to
Extension Settingsand pickGHCupin theManage HLSdropdown - (Optional) Manually set the GHCup executable path
- (Extra) Set
Formatting Providertofourmolufor correct formatting
You may also need to install the nix-env-selector extension.
The nix-env-selector extension may prompt for the workspace to be re-loaded. Once re-loaded, HLS should start working.
To build and run nix based packages at RV, please follow these instructions to set up nix:
We are using nix flakes in all our repos. What this means at a high level is that some of the commands for building packages look a bit different. See also the runtimeverification/rv-nix-tools repository.
To set up nix flakes you will need to install nix 2.4 or higher.If you are on a standard Linux distribution, such as Ubuntu, first install nix
and then enable flakes by editing either ~/.config/nix/nix.conf or /etc/nix/nix.conf and adding:
experimental-features = nix-command flakes
Note that if this is your first time using Nix you will have to manually create one of the .conf files.
This is needed to expose the Nix 2.0 CLI and flakes support that are hidden behind feature-flags. (If you are on a different system like nixOS, see instructions for enabling flakes here: https://nixos.wiki/wiki/Flakes)
By default, Nix will build any project and its transitive dependencies from source, which can take a very long time. We therefore need to set up some binary caches to speed up the build process. First, install cachix
nix profile install github:cachix/cachix/v1.1
and then add the k-framework cachix cache
cachix use k-framework
Next, we need to set up the cache for our haskell infrastructure, by adding the following sections to /etc/nix/nix.conf or, if you are a trusted user, ~/.config/nix/nix.conf (if you don't know what a "trusted user" is, you probably want to do the former):
trusted-public-keys = ... hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
substituters = ... https://cache.iog.io
i.e. if the file was originally
substituters = https://cache.nixos.org
trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
it will now read
substituters = https://cache.nixos.org https://cache.iog.io
trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
Make sure that the file wasn't overwritten, if it was add the experimental-features again.
The CI requires all Haskell files to be formatted via fourmolu.
If using VSCode, please refer to the language server section above. If not, the easiest way to do this locally is by using the nix development shell #style, which provides fourmolu in the version used by CI for checking the format.
nix develop .#style --command scripts/fourmolu.sh
This script will run fourmolu to format all Haskell files in the project. You can also leave out the --command ... part and use fourmolu in the interactive nix develop shell to format particular files or subfolders:
$ nix develop .#style
<nix-develop>$ fourmolu path/to/Foo.hs
... outputs the formatted file
<nix-develop>$ cd a/sub/directory && fourmolu
We provide a development nix shell with a suitable development environment and a binary cache at runtimeverification.cachix.org.
The development can be launched via nix develop .#cabal and then calling cabal build/test/etc.
Using a version of direnv that works with nix (https://github.com/nix-community/nix-direnv) allows seamless loading and unloading of the nix shell, which adds all the required packages such as cabal, hpack, fourmolu, etc. Use the above link to install nix-direnv, making sure to hook direnv into whichever shell you are using (https://direnv.net/docs/hook.html). You can use the default nix shell (currently GHC version 9.6.4) by running
echo "use flake" > .envrcFinally, run direnv allow inside the repo folder to load up the nix shell.
Note that only cabal currently works within the nix shell and since it does not support the HPack package.yaml file format, any changes to this file will require running hpack before they are picked up by cabal. The *.cabal files are checked in but not intended for manual editing if a package.yaml exists.
We aim to use stack.yaml and its chosen LTS resolver as the source of truth for the Haskell package set the projectis built with.
However, the nix flake uses cabal2nix to build cabal projects, using Haskell packages from nixpkgs and overriden with packages from Hackage with source overrides. nixpkgs provides some packages in slightly different versions, but the discrepancies are minor and mainly in test dependencies.
A cabal.project.freeze file has been added to ensure the consistent use of known dependency versions when building outside nix.
To optimize the build time of overriden packages, some-cabal-hashes is utilized when overriding sources.
An upgrade to the stack resolver will therefore require a complete revision of the dependencies, starting with the GHC version (specified in the nix flake under ghcVer, and revising the overrides in flake.nix.
As a starting point to this process, the script scripts/freeze-cabal-to-stack-resolver.sh can be used to generate a new cabal.project.freeze file which pins the dependencies to what the current stack resolver is using. Some manual adjustments will usually be necessary for the nix builds in CI and locally to work.
Haskell-backend provides an integration shell for running integration tests, which compile the K framework (of a specified version) against your current version of haskell backend and brings K into scope of your current shell.
The integration shell is part of the k repository, but invoked from the local tree, adding additional tools (see nix/integration-shell.nix and ../k/flake.nix). Its haskell-backend dependency must be overridden to use the haskell-backend dependency from the current checked-out tree, and the k version will usually be the one from deps/k_release.
To use this nix shell, execute
me@somewhere:haskell-backend$ nix develop \
github:runtimeverification/k/v$(cat deps/k_release)#kore-integration-tests \
--override-input haskell-backend . --update-input haskell-backend
...
...(nix output)
integration-shell:me@somewhere:haskell-backend$(This will take some time the first time you run it for a specific K framework version...)
A specific commit or version tag of the K framework github repository can be used instead of $(cat deps/k_release).
Running this command will add all of the K binaries like kompile or kast into the PATH of your current shell. This is not permanent and will only persist in your current shell window until you exit the active nix shell).
integration-shell:me@somewhere:haskell-backend$ make -C test/issue-3344 test
...
...(make output)
integration-shell:me@somewhere:haskell-backend$ exit
me@somewhere:haskell-backend$
Call these scripts from the root of the repo to obtain performance numbers for the KEVM and Kontrol test suites. These are necessary for any new feature which is expected to modify the perfromance of the booster and the timings should be includedf in the PR.
This scipt can be used with any folder containing bug reports to build an anlysis of fallback/abort reasons in the booster. To obtain bug reports, first run PYTEST_PARALLEL=8 scripts/performance-tests-kevm.sh --bug-report, which will generate tarballs for all the tests and drop them into scripts/bug-reports/. Then call scripts/booster-analysis.sh scripts/booster-analysis.sh scripts/bug-reports/kevm-v1.0.417-main
- Rename
bug-report.tar.gzto something more descriptive likeissue-123.tar.gz - Copy the tar file into
test/rpc-integration/ - Run
./generateDirectoryTest.sh issue-123.tar.gz. This will copy the definition files intoresources/and rpc commands intotest-issue-123/ - Run the test via
./runDirectoryTest test-issue-123
Note that it is also possible to run a test directly from a tarball with runDirectoryTest.sh, skipping the unpacking step. This is useful in automated workflows that involve running several tarballs.
There is a simple utility called pretty which can be used to pretty print a KORE JSON term from a bug report, which does not contain the original K definition:
cabal run pretty -- ../definition.kore <(jq '.result.state' XXX_response.json)
