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.
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.
See the developer guide for instructions on how to build, run and debug MIRAI.
- 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
See the CONTRIBUTING file for how to help out.
MIRAI is MIT licensed, as found in the LICENSE file.