/MIRAI

Rust mid-level IR Abstract Interpreter

Primary LanguageRustMIT LicenseMIT

MIRAI Build Status codecov

MIRAI is an abstract interpreter for the Rust compiler's mid-level intermediate representation (MIR). It is intended to become a widely used static analysis tool for Rust. The initial focus will be on taint analysis.

Using MIRAI

You'll need to install MIRAI as described here.

To run mirai, use cargo with RUSTC_WRAPPER set to mirai. Use rustup override to make Cargo use the same version of Rust as MIRAI as described in the Installation Guide.

The easiest way to get started is to first build your project in the normal way. Refer this link for details on compiling a cargo project. When there are no compile errors, no lint errors and no test failures, you can proceed to the next step and run MIRAI. For example:

cargo clean -p my_crate_name
RUSTC_WRAPPER=mirai cargo check

This will likely produce a lot of warnings, which you can then fix by adding annotations using this crate. Keep running cargo check as above until there are no more warnings.

At this stage your code will be better documented and more readable. Perhaps you'll also have found and fixed a few bugs.

Set the verbosity level of output from MIRAI by setting the environment variable MIRAI_LOG to one of info, warn, debug, or trace.

To go beyond this, super lint + better documentation phase, you'll need to be aware of a lot more things.

Developing MIRAI

See the developer guide for instructions on how to build, run and debug MIRAI.

Full documentation

Road map

  • Stabilize MIRAI and get rid of crashing bugs and OOMs
  • Model (ghost) variables
  • Quantifiers
  • Explicit loop invariants
  • Structure invariants
  • More standard library contracts
  • Upgrade log message that affect soundness into compiler warnings
  • Publish MIRAI to crates.io
  • Support linting interfaces
  • Tutorials and worked examples
  • Loop discovery
  • Loop invariant inference
  • Make MIRAI work on Linux

Join the MIRAI community

See the CONTRIBUTING file for how to help out.

License

MIRAI is MIT licensed, as found in the LICENSE file.