Skip to content

runtimeverification/stable-mir-json

Repository files navigation

Rust Stable MIR Pretty Printing

This package provides a program that will emit a JSON serialisation of the Stable MIR of a Rust program

Building

cargo build

NOTE: requries rustup

The build.rs script will ensure that the correct version of rust and the required components are installed and defaulted. What rustup commands are run can be seen by adding verbosity flag -vv to cargo.

Usage

Use the wrapper script run.sh (or cargo run, but this may also initiate a build). The options that this tool accepts are identical to rustc. To generate stable MIR output without building a binary, you can invoke the tool as follows:

cargo run -- <rustc_flags> <path_from_crate_root>

There is experimental support for rendering the Stable-MIR items and their basic blocks as a call graph in graphviz' dot format.

To produce a dot file *.smir.dot (instead of *.smir.json), one can invoke the driver with first argument --dot. When using --json as the first argument, the *.smir.json file will be written. Any other strings given as first argument will be passed to the compiler (like all subsequent arguments).

There are a few environment variables that can be set to control the tools output:

  1. LINK_ITEMS - add entries to the link-time functions map for each monomorphic item in the crate;
  2. LINK_INST - use a richer key-structure for the link-time functions map which uses keys that are pairs of a function type (Ty) and an function instance kind (InstanceKind)
  3. DEBUG - serialize additional data in the JSON file and dump logs to stdout

Development

To ensure code quality, all code is required to pass cargo clippy and cargo fmt without warning to pass CI.

Tests

Integration tests for stable-mir-pretty consist of compiling a number of (small) programs with the wrapper compiler, and checking the output against expected JSON data ("golden" tests).

The tests are stored in src/tests/integration/programs.

To compensate for any non-determinism in the output, the JSON file is first processed to sort the array contents and remove data which changes with dependencies (such as the crate hash suffix in the symbol names).

The JSON post-processing is performed with jq using the script in src/tests/integration/normalise-filter.jq.

Some tests have non-deterministic output and are therefore expected to fail. These tests are stored in src/tests/integration/failing.

Running the Tests

To run the tests, do the following:

make integration-test