Skip to content

Commit

Permalink
Merge pull request #6 from endorlabs/readme
Browse files Browse the repository at this point in the history
Update documentation
  • Loading branch information
hermanventer authored Oct 18, 2024
2 parents 197430e + 6cb404d commit 02d4c5c
Show file tree
Hide file tree
Showing 18 changed files with 42 additions and 66 deletions.
5 changes: 0 additions & 5 deletions CODE_OF_CONDUCT.md

This file was deleted.

10 changes: 0 additions & 10 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -30,20 +30,10 @@ We actively welcome your pull requests.
5. Make sure your code lints.
6. If you haven't already, complete the Contributor License Agreement ("CLA").

## Contributor License Agreement ("CLA")
In order to accept your pull request, we need you to submit a CLA. You only need
to do this once to work on any of Facebook's open source projects.

Complete your CLA here: <https://code.facebook.com/cla>

## Issues
We use GitHub issues to track public bugs. Please ensure your description is
clear and has sufficient instructions to be able to reproduce the issue.

Facebook has a [bounty program](https://www.facebook.com/whitehat/) for the safe
disclosure of security bugs. In those cases, please go through the process
outlined on that page and do not file a public issue.

## Coding Style
We use the [Rust style guide](https://github.com/rust-lang-nursery/fmt-rfcs/blob/master/guide/guide.md)

Expand Down
1 change: 0 additions & 1 deletion PULL_REQUEST_TEMPLATE.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,5 +22,4 @@ Fixes # (issue)
- [ ] If you've changed APIs, update the documentation.
- [ ] Ensure the test suite passes.
- [ ] Make sure your code lints.
- [ ] If you haven't already, complete your CLA here: <https://code.facebook.com/cla>

28 changes: 10 additions & 18 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,16 +1,8 @@
# MIRAI [![codecov](https://codecov.io/gh/facebookexperimental/MIRAI/branch/main/graph/badge.svg?token=q4jzL09Ahl)](https://codecov.io/gh/facebookexperimental/MIRAI) [![deps.rs](https://deps.rs/repo/github/facebookexperimental/MIRAI/status.svg)](https://deps.rs/repo/github/facebookexperimental/MIRAI)
# MIRAI [![codecov](https://codecov.io/gh/endorlabs/MIRAI/branch/main/graph/badge.svg?token=q4jzL09Ahl)](https://codecov.io/gh/endorlabs/MIRAI) [![deps.rs](https://deps.rs/repo/github/endorlabs/MIRAI/status.svg)](https://deps.rs/repo/github/endorlabs/MIRAI)
MIRAI is an abstract interpreter for the [Rust](https://www.rust-lang.org/) compiler's [mid-level intermediate
representation](https://github.com/rust-lang/rfcs/blob/master/text/1211-mir.md) (MIR).
It is intended to become a widely used static analysis tool for Rust.

## Request for Proposals

The Web3 Foundation has an
[RFP](https://github.com/w3f/Grants-Program/blob/master/docs/RFPs/Open/Static-Analysis-for-Runtime-Pallets.md)
for extending MIRAI. If you are interested in making a proposal, feel free to do so and expect to count on support
with design reviews, coding and merging your contributions. Contact [email protected] if you want to discuss this
further.

## 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
Expand All @@ -29,13 +21,13 @@ become security problems (denial of service, undefined behavior).
## How to use MIRAI

You'll need to install MIRAI as described
[here](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/InstallationGuide.md).
[here](https://github.com/endorlabs/MIRAI/blob/main/documentation/InstallationGuide.md).

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.

`cargo mirai` does a top-down full-program path sensitive analysis of the
[entry points](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Overview.md#entry-points) of your
[entry points](https://github.com/endorlabs/MIRAI/blob/main/documentation/Overview.md#entry-points) of your
package. To analyze test functions instead, use `cargo mirai --tests`.

This will likely produce some warnings. Some of these will be real issues (true positives) that you'll fix by changing
Expand All @@ -62,21 +54,21 @@ You can get some insight into the inner workings of MIRAI by setting the verbosi
`warn`, `info`, `debug`, or `trace`, via the environment variable `MIRAI_LOG`.

## Developing MIRAI
See the [developer guide](https://github.com/facebookexperimental/MIRAI/blob/main/documentation//DeveloperGuide.md)
See the [developer guide](https://github.com/endorlabs/MIRAI/blob/main/documentation//DeveloperGuide.md)
for instructions on how to build, run and debug MIRAI.

## Full documentation
* [Overview of project](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Overview.md).
* [Architecture](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Architecture.md).
* [Design discussions](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/DesignDiscussions.md).
* [Further reading](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/FurtherReading.md).
* [Overview of project](https://github.com/endorlabs/MIRAI/blob/main/documentation/Overview.md).
* [Architecture](https://github.com/endorlabs/MIRAI/blob/main/documentation/Architecture.md).
* [Design discussions](https://github.com/endorlabs/MIRAI/blob/main/documentation/DesignDiscussions.md).
* [Further reading](https://github.com/endorlabs/MIRAI/blob/main/documentation/FurtherReading.md).

## Join the MIRAI community
<!-- * Website:
* Facebook page:
* Mailing list
* irc: -->
See the [CONTRIBUTING](https://github.com/facebookexperimental/MIRAI/blob/main/CONTRIBUTING.md) file for how to help out.
See the [CONTRIBUTING](https://github.com/endorlabs/MIRAI/blob/main/CONTRIBUTING.md) file for how to help out.

## License
MIRAI is MIT licensed, as found in the [LICENSE](https://github.com/facebookexperimental/MIRAI/blob/main/LICENSE) file.
MIRAI is MIT licensed, as found in the [LICENSE](https://github.com/endorlabs/MIRAI/blob/main/LICENSE) file.
2 changes: 1 addition & 1 deletion annotations/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ name = "mirai-annotations"
version = "1.12.1"
authors = ["Herman Venter <[email protected]>"]
description = "Macros that provide source code annotations for MIRAI"
repository = "https://github.com/facebookexperimental/MIRAI"
repository = "https://github.com/endorlabs/MIRAI"
readme = "README.md"
license = "MIT"
edition = "2021"
Expand Down
2 changes: 1 addition & 1 deletion annotations/README.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
# MIRAI Annotations

This crate provides a set of macros that can be used in the place of the standard RUST assert and debug_assert macros.
They add value by allowing [MIRAI](https://github.com/facebookexperimental/MIRAI) to:
They add value by allowing [MIRAI](https://github.com/endorlabs/MIRAI) to:
* distinguish between path conditions and verification conditions
* distinguish between conditions that it should assume as true and conditions that it should verify
* check conditions at compile time that should not be checked at runtime because they are too expensive
Expand Down
2 changes: 1 addition & 1 deletion checker/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ name = "mirai"
version = "1.1.9"
authors = ["Herman Venter <[email protected]>"]
description = "A static analysis tool for Rust, based on Abstract Interpretation of MIR"
repository = "https://github.com/facebookexperimental/MIRAI"
repository = "https://github.com/endorlabs/MIRAI"
readme = "../README.md"
license = "MIT"
edition = "2021"
Expand Down
2 changes: 1 addition & 1 deletion checker/src/abstract_value.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ use crate::path::{Path, PathEnum, PathSelector};
use crate::path::{PathRefinement, PathRoot};
use crate::tag_domain::{Tag, TagDomain};

// See https://github.com/facebookexperimental/MIRAI/blob/main/documentation/AbstractValues.md.
// See https://github.com/endorlabs/MIRAI/blob/main/documentation/AbstractValues.md.

/// Mirai is an abstract interpreter and thus produces abstract values.
/// In general, an abstract value is a value that is not fully known.
Expand Down
2 changes: 1 addition & 1 deletion checker/src/options.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ fn make_options_parser(running_test_harness: bool) -> Command {
.long("call_graph_config")
.num_args(1)
.help("Path call graph config.")
.long_help(r#"Path to a JSON file that configures call graph output. Please see the documentation for details (https://github.com/facebookexperimental/MIRAI/blob/main/documentation/CallGraph.md)."#))
.long_help(r#"Path to a JSON file that configures call graph output. Please see the documentation for details (https://github.com/endorlabs/MIRAI/blob/main/documentation/CallGraph.md)."#))
.arg(Arg::new("print_function_names")
.long("print_function_names")
.num_args(0)
Expand Down
6 changes: 3 additions & 3 deletions documentation/Decisions.md
Original file line number Diff line number Diff line change
Expand Up @@ -196,7 +196,7 @@ trickier because of the dependency on a nightly build of the compiler.
Not a good idea for such a complicated language, but this is pretty much what has been done for C++.
#### Analyze the output of the rust compiler.
For example LLVM bitcode. This is not a terrible idea, but see
[Why plug into the Rust compiler?](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/WhyPlugIn.md).
[Why plug into the Rust compiler?](https://github.com/endorlabs/MIRAI/blob/main/documentation/WhyPlugIn.md).

## Use MIR
The Mid-level Intermediate Representation is the last intermediate data structure produced by the rust compiler before
Expand All @@ -221,7 +221,7 @@ more functions.
### Alternatives
#### Use LLVM bitcode
But see
[Why plug into the Rust compiler?](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/WhyPlugIn.md).
[Why plug into the Rust compiler?](https://github.com/endorlabs/MIRAI/blob/main/documentation/WhyPlugIn.md).
#### Lower MIR into a well-defined and stable LIR where operations are simple
For example, the Common Intermediate Language of .NET.

Expand Down Expand Up @@ -293,7 +293,7 @@ abstract domains.

## Symbolic expression domain
The abstract domain used by default uses a symbolic expression as its representation.
See [Abstract Values](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/AbstractValues.md).
See [Abstract Values](https://github.com/endorlabs/MIRAI/blob/main/documentation/AbstractValues.md).
### Positives
The most precise way to specify which values an expression can result in is the expression itself.
### Negatives
Expand Down
16 changes: 8 additions & 8 deletions documentation/DesignDiscussions.md
Original file line number Diff line number Diff line change
@@ -1,20 +1,20 @@
# Design Discussions

[Abstract Values](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/AbstractValues.md)
[Abstract Values](https://github.com/endorlabs/MIRAI/blob/main/documentation/AbstractValues.md)

[Caching](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Caching.md)
[Caching](https://github.com/endorlabs/MIRAI/blob/main/documentation/Caching.md)

[Incremental Analysis](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/IncrementalAnalysis.md)
[Incremental Analysis](https://github.com/endorlabs/MIRAI/blob/main/documentation/IncrementalAnalysis.md)

[Parallelism](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Parallelism.md)
[Parallelism](https://github.com/endorlabs/MIRAI/blob/main/documentation/Parallelism.md)

[Why MIR?](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/WhyMir.md)
[Why MIR?](https://github.com/endorlabs/MIRAI/blob/main/documentation/WhyMir.md)

[Why plug into the Rust compiler?](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/WhyPlugIn.md)
[Why plug into the Rust compiler?](https://github.com/endorlabs/MIRAI/blob/main/documentation/WhyPlugIn.md)

[Why Rust?](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/WhyRust.md)
[Why Rust?](https://github.com/endorlabs/MIRAI/blob/main/documentation/WhyRust.md)

[Why top down?](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/WhyTopDown.md)
[Why top down?](https://github.com/endorlabs/MIRAI/blob/main/documentation/WhyTopDown.md)

Devirtualization

Expand Down
6 changes: 3 additions & 3 deletions documentation/DeveloperGuide.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
# Developer Guide

Install MIRAI following the instructions in the
[installation guide](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/InstallationGuide.md).
[installation guide](https://github.com/endorlabs/MIRAI/blob/main/documentation/InstallationGuide.md).

Also make sure that the correct version of rustc is installed, along with some optional components

Expand Down Expand Up @@ -43,7 +43,7 @@ To run mirai on a crate, as if it were rustc, just set the `RUSTC_WRAPPER` envir
When running `RUSTC_WRAPPER=~/mirai/target/debug/mirai cargo build` on a crate make sure to either:

1. Set Rust to use the same nightly as MIRAI in the crate's directory (via `rustup override`, or by linking to
MIRAI's [rust-toolchain](https://github.com/facebookexperimental/MIRAI/blob/main/rust-toolchain) file).
MIRAI's [rust-toolchain](https://github.com/endorlabs/MIRAI/blob/main/rust-toolchain) file).
2. Or set `DYLD_LIBRARY_PATH=/Users/$USER/.rustup/toolchains/nightly-YYYY-MM-DD-TA/lib/` before running
`RUSTC_WRAPPER=mirai cargo build`.
- (Be sure to fill `YYYY-MM-DD` with the correctly nightly date and to replace TA with the appropriate target
Expand Down Expand Up @@ -171,7 +171,7 @@ into the JSON format needed by VSCode.

Since Mirai makes use of a private and unstable API with sparse documentation, it can be very helpful to debug Mirai
while seeing the actual rustc sources in the debugger. By default, this does not happen. To make it happen, see
[debugging](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/DebuggingRustc.md) with Rustc sources.
[debugging](https://github.com/endorlabs/MIRAI/blob/main/documentation/DebuggingRustc.md) with Rustc sources.

## Testing

Expand Down
6 changes: 3 additions & 3 deletions documentation/IncrementalAnalysis.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,16 +4,16 @@ Ideally, Mirai should just become a regular part of the Rust Language Service (R
are being edited.

If this is to happen, Mirai should be fast, which is not something one typically associates with program verification
tools. Furthermore, as discussed [here]((https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Parallelism.md)),
tools. Furthermore, as discussed [here]((https://github.com/endorlabs/MIRAI/blob/main/documentation/Parallelism.md)),
parallelism is not going to help.

As discussed [here](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Caching.md), caching
As discussed [here](https://github.com/endorlabs/MIRAI/blob/main/documentation/Caching.md), caching
function summaries helps to avoid some exponential behavior during analysis. Caching also helps make the analysis
incremental, which is going to be the key to integrating MIRAI into the RLS.

Even so, the analysis of even a single function body can become exponential when it contains many loops and/or makes
many calls to functions that have large summaries. Imposing
[k-limits](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/K-limits.md) helps to keep things
[k-limits](https://github.com/endorlabs/MIRAI/blob/main/documentation/K-limits.md) helps to keep things
responsive, but at the cost of increasing the number of false negatives.

It seems interesting to pursue more incrementalism in this case, possibly by retaining the environments computed for
Expand Down
4 changes: 2 additions & 2 deletions documentation/InstallationGuide.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ Please ensure that all of the following dependencies are installed:
The best way to install MIRAI into cargo is to clone the MIRAI repository:

```bash
git clone https://github.com/facebookexperimental/MIRAI.git
git clone https://github.com/endorlabs/MIRAI.git
cd MIRAI
```

Expand All @@ -28,4 +28,4 @@ cargo install --locked --path ./checker
## Contributing to MIRAI

If you want to help develop MIRAI see
the [developer guide](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/DeveloperGuide.md)
the [developer guide](https://github.com/endorlabs/MIRAI/blob/main/documentation/DeveloperGuide.md)
8 changes: 4 additions & 4 deletions documentation/Overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ investigated and fixed as appropriate. There are currently no plans for a v2.

## How to use MIRAI

You'll need to build and install MIRAI as described [here](https://github.com/facebookexperimental/MIRAI#using-mirai).
You'll need to build and install MIRAI as described [here](https://github.com/endorlabs/MIRAI#using-mirai).
That done, just run `cargo mirai` in the root directory of your project.

When run this way, MIRAI, will statically analyze all the code reachable from entry
Expand Down Expand Up @@ -184,7 +184,7 @@ is missing or the good tag is present.
To prevent intermediate code from accidentally adding "good" tags, this can be made a privileged operation by making
the tag constructor private.

More details and examples can be found [here](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/TagAnalysis.md).
More details and examples can be found [here](https://github.com/endorlabs/MIRAI/blob/main/documentation/TagAnalysis.md).

## Constant time analysis

Expand Down Expand Up @@ -316,7 +316,7 @@ thus never trigger the path with the unresolvable call.

The approached used to deal with to these hard problems is to infer preconditions that preclude the unresolvable calls
from being reached, as already discussed
[above](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Overview.md#incomplete-analysis).
[above](https://github.com/endorlabs/MIRAI/blob/main/documentation/Overview.md#incomplete-analysis).

## Foreign functions

Expand All @@ -327,7 +327,7 @@ written in languages other than Rust, or just calls to Rust standard library fun

These functions need to have some kind of "model" that can be summarized and used in the analysis when calls to them
are encountered. Models for many of the standard library foreign functions are included with the MIRAI sources and
can be found [here](https://github.com/facebookexperimental/MIRAI/blob/main/standard_contracts/src/foreign_contracts.rs).
can be found [here](https://github.com/endorlabs/MIRAI/blob/main/standard_contracts/src/foreign_contracts.rs).

Most of these are uninteresting because they have no preconditions and their results are inputs to the program and must
thus be treated as fully unknown by the analysis. Others are just trivial re-implementations of the library functions.
Expand Down
2 changes: 1 addition & 1 deletion documentation/Parallelism.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,5 +16,5 @@ analysis of pathological functions that are widely used will quickly cause other
duplicate work.

Pursuing this at the moment does not seem to be the best use of resources. Future work should probably concentrate on
[incremental analysis](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/IncrementalAnalysis.md).
[incremental analysis](https://github.com/endorlabs/MIRAI/blob/main/documentation/IncrementalAnalysis.md).

4 changes: 2 additions & 2 deletions documentation/WhyMir.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,9 @@ the [High-Level Intermediate Representation](https://rustc-dev-guide.rust-lang.o
All of these approaches would require some form of lowering in order to perform an analysis of the execution of the
project of interest. This would provide flexibility and more control, but it also involves a substantial amount
of largely duplicated work
([see also](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/WhyPlugIn.md)).
([see also](https://github.com/endorlabs/MIRAI/blob/main/documentation/WhyPlugIn.md)).

There is another consideration: Unlike the AST, HIR and THIR, MIR is
serialized into the compiler output for dependencies. Since MIRAI does a top-down analysis
([see also](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/WhyTopDown.md)), the convenience
([see also](https://github.com/endorlabs/MIRAI/blob/main/documentation/WhyTopDown.md)), the convenience
and performance benefit of not re-compiling every dependency, are factors of overriding importance.
2 changes: 1 addition & 1 deletion standard_contracts/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ name = "mirai-standard-contracts"
version = "0.0.1"
authors = ["Herman Venter <[email protected]>"]
description = "Specifications of standard library functions for MIRAI"
repository = "https://github.com/facebookexperimental/MIRAI"
repository = "https://github.com/endorlabs/MIRAI"
readme = "README.md"
license = "MIT"
edition = "2021"
Expand Down

0 comments on commit 02d4c5c

Please sign in to comment.