Skip to content

Latest commit

 

History

History
263 lines (174 loc) · 13.2 KB

README.md

File metadata and controls

263 lines (174 loc) · 13.2 KB
Raw

Symbolic Execution Engine for the K Framework

Structure of this project

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.

Kompiling a K definition and running the RPC server

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

Building

Besides git, you will need stack or cabal to build the project.

stack build all
# or
cabal build all

You 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.

Developing

Developers will require all the dependencies listed above, in addition to the requirements and recommendations below.

Required dependencies

For integration testing, we require:

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

Recommended dependencies

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.

Running Haskell Language Server

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:

  1. Install the Haskell extension
  2. Go to Extension Settings and pick GHCup in the Manage HLS dropdown
  3. (Optional) Manually set the GHCup executable path
  4. (Extra) Set Formatting Provider to fourmolu for 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.

Developing with Nix

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.

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.

Formatting

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 to run

nix run .#format

This will format all the haskell files in the given folder and all sub-folders. You can cd into a particular subfolder and run the command there, or if you only want to format a specific file, you can provide it as an argument to the above command:

nix run .#format Foo.hs

Nix dev shell

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 and then calling stack build/test/etc.

Nix-direnv

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" > .envrc

Finally, 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.

Upgrading dependencies

We use stack.yaml (and hence stack.yaml.lock) as the source of truth about the Haskell package set the project is built with. The Nix flake uses stacklock2nix to make the packages specified by the lock file available to cabal-install inside Nix.

Any GHC or resolver upgrades must double-check the ghcVersion value in the flake.nix file.

It may also be required to update all-cabal-hashes.

To support the scenario of building the project with cabal-install outside of Nix, We use a cabal.project.freeze file to pin the dependencies to what the current stack resolver is using. The script scripts/freeze-cabal-to-stack-resolver.sh should do most of that work, and scripts/check-cabal-stack-sync.sh checks the result. Some manual adjustments will still be necessary for the nix builds in CI and locally to work.

Integration tests

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$

Integration/Performance tests of downstream projects

scripts/performance-tests-{kevm, kontrol, mx}.sh

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.

scripts/booster-analysis.sh

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

Generating an integration test from a bug-report.tar.gz

  1. Rename bug-report.tar.gz to something more descriptive like issue-123.tar.gz
  2. Copy the tar file into test/rpc-integration/
  3. Run ./generateDirectoryTest.sh issue-123.tar.gz. This will copy the definition files into resources/ and rpc commands into test-issue-123/
  4. 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.

Pretty printing KORE JSON

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)