Coder Social home page Coder Social logo

mirai's Introduction

MIRAI codecov deps.rs

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.

Who should use MIRAI

MIRAI can be used as a linter that finds panics that may be unintentional or are not the best way to terminate a program. This use case generally requires no annotations and is best realized by integrating MIRAI into a CI pipeline.

MIRAI can also be used to verify correctness properties. Such properties need to be encoded into annotations of the source program.

A related use is to better document an API via explicit precondition annotations and then use MIRAI to check that the annotations match the code.

Finally, MIRAI can be used to look for security bugs via taint analysis (information leaks, code injection bugs, etc.) and constant time analysis (information leaks via side channels). Unintentional (or ill-considered) panics can also become security problems (denial of service, undefined behavior).

How to use MIRAI

You'll need to install MIRAI as described here for MacOS and Windows and here for Linux.

Then use cargo mirai to run MIRAI over your current package. This works much like cargo check but uses MIRAI rather than rustc to analyze the targets of your current package.

This will likely produce some warnings. Some of these will be real issues (true positives) that you'll fix by changing the offending code. Other warnings will be due to limitations of MIRAI and you can silence them by adding annotations declared in this crate.

Once MIRAI gives your code a clean bill of health, your code will be better documented and more readable. Perhaps you'll also have found and fixed a few bugs.

You can use the environment variable MIRAI_FLAGS to get cargo to provide command line options to MIRAI. The value is a string which can contain any of the following flags:

  • --diag=default|verify|library|paranoid: configures level of diagnostics. With default MIRAI will not report errors which are potential 'false positives'. With verify it will point out functions that may contain such errors. With library it will require explicit preconditions. With paranoid it will flag any issue that may be an error.
  • --single_func <name>: the name of a specific function you want to analyze.
  • --body_analysis_timeout <seconds>: the maximum number of seconds to spend analyzing a function body.
  • --call_graph_config <path_to_config>: path to configuration file for call graph generator (see Call Graph Generator documentation). No call graph will be generated if this is not specified.
  • --: any arguments after this marker are passed on to rustc.

You can get some insight into the inner workings of MIRAI by setting the verbosity level of log output to one of warn, info, debug, or trace, via the environment variable MIRAI_LOG.

Developing MIRAI

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

Full documentation

Join the MIRAI community

See the CONTRIBUTING file for how to help out.

License

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

mirai's People

Contributors

darioncassel avatar stonebuddha avatar wrwg avatar t-rasmud avatar huitseeker avatar sblackshear avatar a-malyshev avatar arilotter avatar disconnect3d avatar lihram avatar ya0guang avatar jsgf avatar hauntsaninja avatar ototot avatar vakaras avatar izgzhen avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.