Working with rustc

Kani is developed on the top of the Rust compiler, which is not distributed on crates.io and depends on bootstrapping mechanisms to properly build its components. Thus, our dependency on rustc crates are not declared in our Cargo.toml.

Below are a few hacks that will make it easier to develop on the top of rustc.

Code analysis for rustc definitions

IDEs rely on cargo to find dependencies and sources to provide proper code analysis and code completion. In order to get these features working for rustc crates, you can do the following:

VSCode

Add the following to the rust-analyzer extension settings in settings.json:

    "rust-analyzer.rustc.source": "discover",
    "rust-analyzer.workspace.symbol.search.scope": "workspace_and_dependencies",

Ensure that any packages that use rustc data structures have the following line set in their Cargo.toml

[package.metadata.rust-analyzer]
# This package uses rustc crates.
rustc_private=true

You may also need to install the rustc-dev package using rustup

rustup toolchain install nightly --component rustc-dev

Debugging in VS code

To debug Kani in VS code, first install the CodeLLDB extension. Then add the following lines at the start of the main function (see the CodeLLDB manual for details):

{
    let url = format!(
        "vscode://vadimcn.vscode-lldb/launch/config?{{'request':'attach','sourceLanguages':['rust'],'waitFor':true,'pid':{}}}",
        std::process::id()
    );
    std::process::Command::new("code").arg("--open-url").arg(url).output().unwrap();
}

Note that pretty printing for the Rust nightly toolchain (which Kani uses) is not very good as of June 2022. For example, a vector may be displayed as vec![{...}, {...}] on nightly Rust, when it would be displayed as vec![Some(0), None] on stable Rust. Hopefully, this will be fixed soon.

CLion / IntelliJ

This is not a great solution, but it works for now (see https://github.com/intellij-rust/intellij-rust/issues/1618 for more details). Edit the Cargo.toml of the package that you're working on and add artificial dependencies on the rustc packages that you would like to explore.

# This configuration doesn't exist so it shouldn't affect your build.
[target.'cfg(KANI_DEV)'.dependencies]
# Adjust the path here to point to a local copy of the rust compiler.
# The best way is to use the rustup path. Replace <toolchain> with the
# proper name to your toolchain.
rustc_driver = { path = "~/.rustup/toolchains/<toolchain>/lib/rustlib/rustc-src/rust/compiler/rustc_driver" }
rustc_interface = { path = "~/.rustup/toolchains/<toolchain>/lib/rustlib/rustc-src/rust/compiler/rustc_interface" }

Don't forget to rollback the changes before you create your PR.

EMACS (with use-package)

First, Cargo.toml and rustup toolchain steps are identical to VS Code. Install Rust-analyzer binary under ~/.cargo/bin/.

On EMACS, add the following to your EMACS lisp files. They will install the necessary packages using the use-package manager.

;; Install LSP
(use-package lsp-mode
  :commands lsp)
(use-package lsp-ui)

;; Install Rust mode
(use-package toml-mode)
(use-package rust-mode)

(setq lsp-rust-server 'rust-analyzer)
(setenv "PATH" (concat (getenv "PATH") ":/home/USER/.cargo/bin/"))

If EMACS complains that it cannot find certain packages, try running M-x package-refresh-contents.

For LSP to be able to find rustc_private files used by Kani, you will need to modify variable lsp-rust-analyzer-rustc-source. Run M-x customize-variable, type in lsp-rust-analyzer-rustc-source, click Value Menu and change it to Path. Paste in the path to Cargo.toml of rustc's source code. You can find the source code under .rustup, and the path should end with compiler/rustc/Cargo.toml. Important: make sure that this rustc is the same version and architecture as what Kani uses. If not, LSP features like definition lookup may be break.

This ends the basic install for EMACS. You can test your configuration with the following steps.

  1. Opening up a rust file with at least one rustc_private import.
  2. Activate LSP mode with M-x lsp.
  3. When asked about the root of the project, pick one of them. Make sure that whichever root you pick has a Cargo.toml with rustc_private=true added.
  4. If LSP asks if you want to watch all files, select yes. For less powerful machines, you may want to adjust that later.
  5. On the file with rustc_private imports, do the following. If both work, then you are set up.
    • Hover mouse over the rustc_private import. If LSP is working, you should get information about the imported item.
    • With text cursor over the same rustc_private import, run M-x lsp-find-definition. This should jump to the definition within rustc's source code.

LSP mode can integrate with flycheck for instant error checking and company for auto-complete. Consider adding the following to the configuration.

(use-package flycheck
  :hook (prog-mode . flycheck-mode))

(use-package company
  :hook (prog-mode . company-mode)
  :config
   (global-company-mode))

clippy linter can be added by changing the LSP install to:

(use-package lsp-mode
  :commands lsp
  :custom
  (lsp-rust-analyzer-cargo-watch-command "clippy"))

Finally lsp-mode can run rust-analyzer via TRAMP for remote development. We found this way of using rust-analyzer to be unstable as of 2022-06. If you want to give it a try you will need to add a new LSP client for that remote with the following code.

(lsp-register-client
  (make-lsp-client
	:new-connection (lsp-tramp-connection "/full/path/to/remote/machines/rust-analyzer")
	:major-modes '(rust-mode)
	:remote? t
	:server-id 'rust-analyzer-remote))

For further details, please see https://emacs-lsp.github.io/lsp-mode/page/remote/.

Custom rustc

There are a few reasons why you may want to use your own copy of rustc. E.g.:

  • Enable more verbose logs.
  • Use a debug build to allow you to step through rustc code.
  • Test changes to rustc.

We will assume that you already have a Kani setup and that the variable KANI_WORKSPACE contains the path to your Kani workspace.

It's highly recommended that you start from the commit that corresponds to the current rustc version from your workspace. To get that information, run the following command:

cd ${KANI_WORKSPACE} # Go to your Kani workspace.
rustc --version # This will print the commit id. Something like:
# rustc 1.60.0-nightly (0c292c966 2022-02-08)
#                       ^^^^^^^^^ this is used as the ${COMMIT_ID} below
# E.g.:
COMMIT_ID=0c292c966

First you need to clone and build stage 2 of the compiler. You should tweak the configuration to satisfy your use case. For more details, see https://rustc-dev-guide.rust-lang.org/building/how-to-build-and-run.html and https://rustc-dev-guide.rust-lang.org/building/suggested.html.

git clone https://github.com/rust-lang/rust.git
cd rust
git checkout ${COMMIT_ID:?"Missing rustc commit id"}
./configure --enable-extended --tools=src,rustfmt,cargo --enable-debug --set=llvm.download-ci-llvm=true
./x.py build -i --stage 2

Now create a custom toolchain (here we name it custom-toolchain):

# Use x86_64-apple-darwin for MacOs
rustup toolchain link custom-toolchain build/x86_64-unknown-linux-gnu/stage2
cp build/x86_64-unknown-linux-gnu/stage2-tools-bin/* build/x86_64-unknown-linux-gnu/stage2/bin/

Finally, override the current toolchain in your kani workspace and rebuild kani:

cd ${KANI_WORKSPACE}
rustup override set custom-toolchain
cargo clean
cargo build-dev

Rust compiler utilities to debug kani-compiler

Enable rustc logs

In order to enable logs, you can just define the RUSTC_LOG variable, as documented here: https://rustc-dev-guide.rust-lang.org/tracing.html.

Note that, depending on the level of logs you would like to get (debug and trace are not enabled by default), you'll need to build your own version of rustc as described above. For logs that are related to kani-compiler code, use the KANI_LOG variable.

Debugging type layout

In order to print the type layout computed by the Rust compiler, you can pass the following flag to rustc: -Zprint-type-sizes. This flag can be passed to kani or cargo kani by setting the RUSTFLAG environment variable.

RUSTFLAGS=-Zprint-type-sizes kani test.rs

When enabled, the compiler will print messages that look like:

print-type-size type: `std::option::Option<bool>`: 1 bytes, alignment: 1 bytes
print-type-size     variant `Some`: 1 bytes
print-type-size         field `.0`: 1 bytes
print-type-size     variant `None`: 0 bytes

Inspecting the MIR

You can easily visualize the MIR that is used as an input to code generation by setting the Rust flag --emit mir. I.e.:

RUSTFLAGS=--emit=mir kani test.rs

The compiler will generate a few files, but we recommend looking at the files that have the following suffix: kani.mir. Those files will include the entire MIR collected by our reachability analysis. It will include functions from all dependencies, including the std library. One limitation is that we dump one copy of each specialization of the MIR function, even though the MIR body itself doesn't change.