KMIR — MIR's Operational Semantics in K

🛠️Work in progress🛠️

MIR is the mid-level internal representation of Rust program in rust compiler.

The KMIR project defines MIR semantics formally in K and attempts build a scalable testing and verification tool for real world Rust programs.

Quick Start

Installation

• Install the kup package manager:

  bash <(curl https://kframework.org/install)

• install the latest version of KMIR.

  kup install kmir

You can refer to kup -h for more options. For example,

• kup list kmir: list available KMIR versions.
• kup install kmir --version 366f8fb: install a paricular version of KMIR.

Using KMIR

At the current stage, KMIR is to be used as a command-line tool. We list the main functions in the following, while users are recommended to explore the latest options using kmir -h or more options of a command using kmir {cmd} -h.

Parsing a MIR file

The kmir parse command invokes the parser generated by K and outputs a KAST representation of MIR abstract syntax parsed from a MIR file.

For example,

kmir parse demo/assert-true.mir

Execute a MIR program

The kmir run command will interpret a MIR program according to the predefined operational rules of MIR. This command invokes the LLVM interpreter generated by K and execute the MIR code in the file.

For example,

kmir run demo/assert-true.mir

Prove a MIR program

(Under development, command interface unstable )

KMIR provides the command kmir prove to prove the claims in the provided specification file.

kmir prove demo/simple-spec.k

This proof results are by default stored in the same directory as the spec-file. User could specify a specific directory using the flag --save-directory.

Display a proof in the tree view

kmir show-proof SIMPLE-SPEC.statement.1 --proof-dir demo

Display a proof in an interative tree format

kmir view-proof SIMPLE-SPEC.statement.1 --proof-dir demo

Build from source

Getting source code

Using the following command to clone this repository, including its submodules:

git clone --recurse-submodules git@github.com:runtimeverification/mir-semantics.git

Build KMIR

Prerequsites: python 3.8.*, pip >= 20.0.2, poetry >= 1.3.2. Users are referred to the tool's installation page for more details:

• Installing Python
• Installing pip: It usually comes with Python installation.
• Installing poetry

The build system of KMIR is a mixture of poetry + kbuild + make:

• poetry handles Python dependencies, see pyproject.toml for Python-related configuration
• kbuild handles K dependencies and build targets, see kbuild.toml
• make build ties the two together

cd kmir
make build

Global Installation of KMIR with pip

source set_env.sh
pip install dist/*.whl

Local Installation of KMIR with poetry

Alternatively, you can also install kmir locally and running it with poetry.

poetry install

In a local installation, we suggest calling kmir via Poetry's poetry run command. This ensures that you are calling the feshly built kmir. For example:

poetry run kmir parse --definition-dir $(kbuild which llvm) ../demo/assert-true.mir --output pretty

Alternative, you can spawn a one-off shell that will allow you to interact with kmir directly by executing the command

poetry shell

In the shell, execute kmir as

kmir parse --definition-dir $(kbuild which llvm) ../demo/assert-true.mir --output pretty

Additionally, the Haskell build needs to be supplied when calling kmir prove. For example,

poetry run kmir prove --definition-dir $(kbuild which llvm) --haskell-dir $(kbuild which haskell) --spec-file src/tests/integration/test-data/prove-rs/simple-spec.k

Note: Since kmir is just a thin Python script and does not do any heavy-lifting itself, it needs access the K definition of MIR. The kbuild tool handles compiling the K code and provides a which command to output the path to the compiled definition, which we give to kmir. We also provide a script, set_env.sh to set the path to the definitions, KMIR_LLVM_DIR and KMIR_HASKELL_DIR, globally. Consequently, the --definition-dir can be omitted. Run the script as

source set_env.sh

Working with Docker

We provide a Docker image for isolated testing, locally and in CI. NOTE: Mac Silicon hardware not supported.

From the root of the repository:

• Build the docker image (the ./deps/k_release file pins the K version):

docker build . --tag kmir-tests --build-arg K_COMMIT=$(cat deps/k_release) --file .github/workflows/Dockerfile

• Run the integration tests in a container:

docker run --name kmir-container --rm --interactive --tty --detach --workdir /home/user kmir-tests &&
docker cp . kmir-container:/home/user &&
docker exec kmir-container chown -R user:user /home/user &&
docker exec --user user kmir-container make -C kmir test-integration

Note: you may need to run the docker commands with sudo, or start a superuser shell with sudo -s.

We use a similar workflow in CI actions defined in the .github/ directory.

Working with KMIR

kmir is a Python package and CLI tool that leverages the pyk library to provide a Python interface for the K semantics. While the K semantics can be also used directly with K framework, the kmir tool makes it more accessible for people not familiar with K.

Working on the Python files

The Python source code of the kmir tool and library resides in kmir/src/. The entry point to the tool is src/kmir/__main__.py.

Use make to run common tasks (see the Makefile for a complete list of available targets).

• make build: Build wheel
• make check: Check code style
• make format: Format code
• make test-unit: Run unit tests
• make test-integration: Run integration tests
• make test-integration TEST_ARGS="--update-expected-output": Run integration tests, updating expected results for show-proof tests

Working on the K files

The K source code of the semantics resides in k-src.

Working on the semantics roughly comprises the following steps:

0. Pick a MIR/Rust program as a running example, or a several of them
1. Modify K files
2. Rebuild the K definition
3. Testout the new definition on the running example
4. Running integration tests

However, from step 3, the following alternative steps avoids rebuilding from scratch:

1. Run poetry run kbuild kompile llvm to re-kompile the semantics
2. Run poetry run kbuild kompile haskell additionally if you are working on a proof
3. Test the running example with a targetted kmir <command> <path to example.mir>
4. Once happy with the step 3 goes, run a part of the integration tests by calling:

   TEST_ARGS="-k test_handwritten" make test-integration-{parse, run, prove etc.}
   

   Modify the command as necessary to include the tests you want.
5. Once happy with the step 4 goes, run the complete integration test suite:

   make test-integration-run
   

   This time, do not include the --kbuild-dir option to re-kompile everything in a temporary directory.

Submitting a PR

Make sure the manual is updated with your new feature, the integration tests passed and the nix tests output updated in case there is K definition changes.

Update nix tests output

When there are changes to the K definition of MIR, the nix tests should be re-executed to update the expected output. We provide a Makefile to make this update easy.

Before running the tests, it would expect a latest built kmir and kbuild DIR's being updated (see the note above on the set_env.sh script).

cd src/tests/nix
make

References

• You may refer to K tutorial to learn more about using K.
• MIR language reference