Rust mid-level IR Abstract Interpreter

Related tags

Utilities MIRAI
Overview

MIRAI Build Status 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.

Using MIRAI

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

To run MIRAI, use cargo with RUSTC_WRAPPER set to mirai. Use rustup override set nightly-YYYY-MM-DD to make Cargo use the same version of Rust as MIRAI. See the above installation instruction to determine which version to use. If you forget to do that or use the wrong version, you'll see an error message complaining about a dynamic load library not being found.

The easiest way to get started is to first build your project in the normal way (with one exception: set RUSTFLAGS="-Z always_encode_mir" to force the rust compiler to include MIR into its compiled output). Refer to 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:

touch src/lib.rs
RUSTC_WRAPPER=mirai cargo build

The touch command (which needs to reference a real file in your project) forces Cargo to re-run rustc and to not assume that its cached error messages are still correct.

This will likely produce a lot of warnings, which you can then fix by adding annotations declared in this crate. Keep re-touching and running cargo build 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.

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

  • --test_only: instructs MIRAI to analyze only test methods in your crate. You must also provide the --tests option to the cargo build command to include those tests actually into your build.
  • --diag=relaxed|strict|paranoid: configures level of diagnostics. With relaxed (the default) MIRAI will not report errors which are potential 'false positives'. With strict it will report such errors. With paranoid it will flag any direct or indirect call as a potential error.
  • --single_func <name>: the name of a specific function you want to analyze.
  • --: 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.

Using MIRAI together with the Rust design by contracts crate

Preliminary support for MIRAI is available in the design by contracts crate. There is currently no official release containing this support on crates.io, so you must directly refer to the gitlab repo using a dependency like below in your Cargo.toml:

contracts = { git = "https://gitlab.com/karroffel/contracts.git", branch = "master", features = [ "mirai_assertions" ]}

See the shopping cart example for usage.

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.
  • Summaries for intrinsics and standard library functions without MIR.
  • Loop discovery
  • Explicit loop invariants
  • Loop invariant inference
  • Model (ghost) variables
  • Quantifiers
  • Publish MIRAI to crates.io
  • Support linting interfaces
  • Tutorials and worked examples

Join the MIRAI community

See the CONTRIBUTING file for how to help out.

License

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

Comments
  • Validation fails on Ubuntu 20.04

    Validation fails on Ubuntu 20.04

    Issue

    Generally speaking, MIRAI cannot work well on Ubuntu 20.04. It cannot verify for some programs. So I tried to run validate.sh and it failed on the integration test. I was thinking it's because of my environment is not clean enough, so I also tried to use it in docker (ubuntu:latest) and it also failed.

    Steps to Reproduce

    1. Start a container of ubuntu:latest and run necessary components like pkg-config, z3, openssl and clang

    2. Insatll MIRAI following the steps documented in documentation/linux.md

    3. Run validate.sh

    Expected Behavior

    exit without error

    Actual Results

    error: test failed, to rerun pass '-p mirai --test integration_tests'
    
    Caused by:
      process didn't exit successfully: `/home/v_chenhongbo04/MIRAI/target/debug/deps/integration_tests-a0b61660615a641b` (signal: 11, SIGSEGV: invalid memory reference)
    

    Environment

    rustc 1.60.0-nightly (bfe156467 2022-01-22)

    opened by ya0guang 12
  • Adding set operations to TagPropagationSet

    Adding set operations to TagPropagationSet

    Description

    This adds two convenience functions for constructing taint propagation masks easier. E.g. adding and removing propagation types from existing masks

    Type of change

    • [ ] Bug fix (non-breaking change which fixes an issue)
    • [x] New feature (non-breaking change which adds functionality)
    • [ ] Breaking change (fix or feature that would cause existing functionality to not work as expected)
    • [x] API change with a documentation update
    • [ ] Additional test coverage
    • [ ] Code cleanup or just keeping up with the latest Rustc nightly

    How Has This Been Tested?

    I added two test cases, one for each function that verifies the basic functionality

    Checklist:

    • [x] Fork the repo and create your branch from main.
    • [x] If you've added code that should be tested, add tests.
    • [x] If you've changed APIs, update the documentation.
    • [x] Ensure the test suite passes.
    • [x] Make sure your code lints.
    • [x] If you haven't already, complete your CLA here: https://code.facebook.com/cla
    CLA Signed 
    opened by JustusAdam 9
  • Debug MIRAI in CLion

    Debug MIRAI in CLion

    Hi everyone! I've just heard about MIRAI. The project is very exciting and I hope it will eventually become a part of IntelliJ Rust and RLS code analysis! However, while reading the documentation I was surprised to see that CLion doesn't support debugging MIRAI ([1] and [2]).

    I've just tried it out and seems like it works fine: Screenshot 2019-03-30 at 12 21 02

    All I have to do is to provide the DYLD_LIBRARY_PATH as specified: Screenshot 2019-03-30 at 12 35 29

    Also [3],

    debugging support for Rust is pretty much non existent

    I'm sorry to hear that. I'm working on new lldb formatters for Rust; in CLion, they are enabled by default and configurable via Preferences | Build, Execution, Deployment | Debugger | Data Views | Rust. I hope debugging support gets better, though there is no Evaluate expression for Rust yet. So I really want to know if something related to debugging frontend doesn't work properly or if you have some ideas to improve it (at frontend level, like formatters, watches, remote debugging and so on). If so, you can open an issue here.

    question 
    opened by ortem 9
  • Encode tag checks as SMT queries

    Encode tag checks as SMT queries

    Description

    This commit implements Z3 encoding for tag checks. To ensure that the expression domain is precise enough to reduce tag checks to SMT queries, UnknownTagCheck expressions now record values instead of paths. On the Z3 side, I declare a top-level logical predicate has_tag in a way that has_tag(path, tag) encodes an uninterpreted Boolean-valued function call that checks whether path is attached with tag or not. When MIRAI generates a Z3 AST for UnknownTagCheck { operand, tag, .. }, it invokes the general_has_tag(operand, tag) routine, which recursively synthesizes a tag-check query from sub-expressions. This routine works similar to AbstractValue::get_tags.

    This commit also includes several tests that indicate bugs or loss of precision. One is that when we tag a function parameter that is a struct, we don't know paths rooted at it so we don't tag its fields. The other is that the current methodology for copy_or_move_elements and attach_tag_to_elements only tries to split a path after enumerating paths rooted at the target path, so updating if ... { local1 } else { local2 } would not update local1.field or local2.field.

    Type of change

    • [ ] Bug fix (non-breaking change which fixes an issue)
    • [x] New feature (non-breaking change which adds functionality)
    • [ ] Breaking change (fix or feature that would cause existing functionality to not work as expected)
    • [ ] API change with a documentation update
    • [ ] Additional test coverage
    • [ ] Code cleanup or just keeping up with the latest Rustc nightly

    How Has This Been Tested?

    ./validate.sh ran MIRAI over Libra

    CLA Signed 
    opened by stonebuddha 7
  • How does the static analyzer work?

    How does the static analyzer work?

    I couldn't find the instructions for enabling the static analyzer in the documentation. For example, I want the compiler to raise an error in the following example:

    #[pre(i < a.len())]
    #[post(*a[i] == v)]
    fn update(a: &mut [Box<i32>], i: usize, v: i32) {
        *a[i] = v + 1;
    }
    

    Is it possible?

    opened by mhoseinzadeh 7
  • [Building MIRAI]  wrapper.h:1:10: fatal error: 'z3.h' file not found

    [Building MIRAI] wrapper.h:1:10: fatal error: 'z3.h' file not found

    Issue

    Run cargo install --locked --path ./checker failed due to

    failed to run custom build command for `z3-sys v0.7.1`
    

    Caused by

    process didn't exit successfully: `<PATHTOMIRAI>/target/release/build/z3-sys-1ee5d02118b012a6/build-script-build` (exit status: 101)
      --- stdout
      cargo:rerun-if-changed=build.rs
      cargo:rerun-if-changed=wrapper.h
    
      --- stderr
      wrapper.h:1:10: fatal error: 'z3.h' file not found
      wrapper.h:1:10: fatal error: 'z3.h' file not found, err: true
      thread 'main' panicked at 'Unable to generate bindings: ()', ~/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/build.rs:33:14
      note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
    error: failed to compile `mirai v1.1.0 (<PATHTOMIRAI>/checker)`, intermediate artifacts can be found at `<PATHTOMIRAI>/target`
    

    Steps to Reproduce

    1. brew info z3
    z3: stable 4.8.17 (bottled), HEAD
    High-performance theorem prover
    https://github.com/Z3Prover/z3
    /usr/local/Cellar/z3/4.8.17 (135 files, 94.9MB) *
      Poured from bottle on 2022-06-17 at 00:26:16
    
    1. git clone https://github.com/facebookexperimental/MIRAI.git
    2. cd MIRAI
    3. ./setup.sh
    4. cp binaries/libz3.dylib /usr/local/lib
    cp: /usr/local/lib/libz3.dylib: Permission denied
    

    manually copy succeeded, replaced the original libz3.dylib in /usr/local/lib 6. cargo install --locked --path ./checker

    Expected Behavior

    Successful build of MIRAI

    Actual Results

    Panic

    Environment

    macOS Monterey v12.3.1, Intel processor. Rust version: rustc 1.63.0-nightly (4c5f6e627 2022-05-17)

    opened by yanliu18 6
  • "Sorts (_ BitVec 128) and Int are incompatible"

    I tried to run MIRAI on one of our crate, but I got this error message:

    Error: Sorts (_ BitVec 128) and Int are incompatible
    error: could not compile `chain-core`.
    
    To learn more, run the command again with --verbose.
    

    I follow the doc to install recent MIRAI, runs something like this:

    $ export RUSTFLAGS="-Z always_encode_mir"
    $ cargo build -p chain-core
    $ touch $CRATE/src/lib.rs
    $ RUSTC_WRAPPER=mirai cargo build -p chain-core
    
    opened by yihuang 6
  • Lack of support for bitwise negation

    Lack of support for bitwise negation

    Issue

    MIRAI seems to treat all expressions like !e as logical negation, while Rust does support bitwise negation operation. This makes Z3 crash due to typing errors.

    Steps to Reproduce

    Run MIRAI for the utf8-range crate (v1.0.3) reproduces the crash. More specifically, the crash is triggered when analyzing the function Utf8Sequences::next.

    Expected Behavior

    The analysis should terminate without errors.

    Actual Results

    An error message from Z3 before crash: Error: Sort mismatch at argument #1 for function (declare-fun not (Bool) Bool) supplied sort is Int

    Environment

    Rust version 1.37.0-nightly (5f3656ce9 2019-06-11)

    opened by uraj 6
  • Add support for Windows installation

    Add support for Windows installation

    Description

    Added z3.lib to the binaries directory for Windows installation and added a build.rs file to allow Rust to locate the lib on Windows. Updated InstallationGuide.md to reflect this. Added Windows to .travis.yml build matrix.

    (Also changed "OSX" to "macOS" in InstallationGuide.md to reflect official renaming).

    Fixes: N/A

    Type of change

    • [ ] Bug fix (non-breaking change which fixes an issue)
    • [x] New feature (non-breaking change which adds functionality)
    • [ ] Breaking change (fix or feature that would cause existing functionality to not work as expected)
    • [ ] API change with a documentation update
    • [ ] Additional test coverage

    How Has This Been Tested?

    Installation with the change has been tested locally on both a Windows and on a macOS machine.

    Checklist:

    • [x] Fork the repo and create your branch from master.
    • [ ] If you've added code that should be tested, add tests.
    • [ ] If you've changed APIs, update the documentation.
    • [x] Ensure the test suite passes.
    • [x] Make sure your code lints.
    • [x] If you haven't already, complete your CLA here: https://code.facebook.com/cla
    CLA Signed 
    opened by darioncassel 6
  • [Discussion] Abstract heap

    [Discussion] Abstract heap

    I think we need an abstract model of heap. What is on your mind? @hermanventer

    Another question to clarify is how to abstract heap pointer values, a.k.a. Box<T>. Is there another wrapper of heap-allocated object in Rust?

    I checked the source and there is only pub environment: &'a mut HashTrieMap<Path, AbstractValue>.

    question 
    opened by izgzhen 6
  • How to verify tag when type changes

    How to verify tag when type changes

    Issue

    I want to verify a typestate program but I'm hindered by some unexpected output. So I start with a minimal reproducible example.

    When I have two structs (say A and B for example) and have a function converting from A to B. How should I maintain and propagate the tag? I checked annotations/lib.rs and found SubComponent and SuperComponent, but the output is not as what I expected. In the example below I verified the tag after executing a_to_b and has the same postcondition in a_to_b, however only the postcondition is not always satisfied.

    Steps to Reproduce

    // main.rs
    #![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]
    
    extern crate mirai_annotations;
    
    use mirai_annotations::*;
    
    #[cfg(mirai)]
    use mirai_annotations::TagPropagationSet;
    
    #[cfg(mirai)]
    struct SecretTaintKind<const MASK: TagPropagationSet> {}
    
    #[cfg(mirai)]
    const SECRET_TAINT: TagPropagationSet = TAG_PROPAGATION_ALL;
    
    #[cfg(mirai)]
    type SecretTaint = SecretTaintKind<SECRET_TAINT>;
    
    #[cfg(not(mirai))]
    type SecretTaint = ();
    
    struct A(u32);
    struct B(u32);
    
    fn a_to_b(a: A) -> B {
        precondition!(has_tag!(&a, SecretTaint));
        let b = B(a.0 + 1);
        postcondition!(has_tag!(&b, SecretTaint));
        b
    }
    
    fn main() {
        let a = A(1);
        add_tag!(&a, SecretTaint);
        let b = a_to_b(a);
        verify!(has_tag!(&b, SecretTaint));
    }
    

    run cargo mirai.

    Expected Behavior

    no warning.

    Actual Results

     test-mirai git:(master) ✗ cargo mirai
        Checking test-mirai v0.1.0 (/Users/ya0guang/test-mirai)
    [2022-02-02T02:16:39Z INFO  mirai] MIRAI options from environment: Options { single_func: None, test_only: false, diag_level: Default, constant_time_tag_name: None, max_analysis_time_for_body: 30, max_analysis_time_for_crate: 240, statistics: false, call_graph_config: None }
    [2022-02-02T02:16:39Z INFO  mirai] MIRAI options modified by command line: Options { single_func: None, test_only: false, diag_level: Default, constant_time_tag_name: None, max_analysis_time_for_body: 30, max_analysis_time_for_crate: 240, statistics: false, call_graph_config: None }
    [2022-02-02T02:16:39Z INFO  mirai::callbacks] Processing input file: src/main.rs
    [2022-02-02T02:16:39Z INFO  mirai::callbacks] storing summaries for src/main.rs at /var/folders/cv/mtjnjfxs14lbt801r9vm8sd40000gp/T/.tmpAuiOal/.summary_store.sled
    [2022-02-02T02:16:39Z INFO  mirai::summaries] creating a new summary store from the embedded tar file
    [2022-02-02T02:16:39Z INFO  mirai::crate_visitor] analyzing function test_mirai.main
    warning: possible unsatisfied postcondition
      --> src/main.rs:28:5
       |
    28 |     postcondition!(has_tag!(&b, SecretTaint));
       |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    
    warning: `test-mirai` (bin "test-mirai") generated 1 warning
        Finished dev [unoptimized + debuginfo] target(s) in 0.68s
    

    Besides, from the comments in annotations/lib.rs, I think postcondition! is flow-sensitive, but verify! is not when using them in the same place in the function.

    Environment

    rustc 1.60.0-nightly (bfe156467 2022-01-22)

    opened by ya0guang 5
  • Problems in tag analysis for vector operations

    Problems in tag analysis for vector operations

    Issue

    1. Adding tag to a vector doesn't propagate the tag to the elements in this vector.
    2. Unexpected tag analysis result when using into_iter() to iterate a vector of struct.

    Steps to Reproduce

    For problem 1, I found this test which exactly meets my verification conditions. MIRAI should not complain about this but it actually complains. However, this line is commented and I don't know why. I'd be more than grateful if you can provide more details.

    For the second problem, I create a vector of struct I and tag each element. When iterating the vector using into_iter, MIRAI can detect that elements have tags (provably false verification condition in the following snippet). However, when the lines are uncommented, MIRAI doesn't complain anymore, and I think this is problematic.

    #![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]
    extern crate mirai_annotations;
    use mirai_annotations::*;
    
    #[cfg(mirai)]
    use mirai_annotations::TagPropagationSet;
    #[cfg(mirai)]
    pub struct SecretTaintKind<const MASK: TagPropagationSet> {}
    #[cfg(mirai)]
    const SECRET_TAINT: TagPropagationSet = TAG_PROPAGATION_ALL;
    #[cfg(mirai)]
    pub type SecretTaint = SecretTaintKind<SECRET_TAINT>;
    
    use std::vec::Vec;
    
    struct I(u32);
    
    fn main() {
        let va = vec![I(1), I(2), I(3)];
    
        for i in va.iter() {
            add_tag!(i, SecretTaint);
        }
        let mut vb: Vec<I> = Vec::new();
        // let mut vb: Vec<i32> = Vec::new();
    
        for i in va.into_iter() {
            verify!(does_not_have_tag!(&i, SecretTaint));
            // vb.push(i);
        }
    }
    

    Expected Behavior

    When the commented lines are uncommented, MIRAI should complain at verify!(does_not_have_tag!(&i, SecretTaint));.

    Actual Results

    When the commented lines are uncommented, MIRAI doesn't complain.

    Environment

    rustc 1.61.0-nightly (c84f39e6c 2022-03-20)

    opened by ya0guang 0
  • Verify tag propagation for multiple type changes

    Verify tag propagation for multiple type changes

    Issue

    MIRAI cannot produce correct result in tag propagation when types are changing multiple times. In my previous issue #1131 , the problem is solved when there is one type change. However, when there are more than one type changes, MIRAI doesn't work.

    Steps to Reproduce

    #![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]
    extern crate mirai_annotations;
    use mirai_annotations::*;
    
    #[cfg(mirai)]
    use mirai_annotations::TagPropagationSet;
    #[cfg(mirai)]
    struct SecretTaintKind<const MASK: TagPropagationSet> {}
    #[cfg(mirai)]
    const SECRET_TAINT: TagPropagationSet = TAG_PROPAGATION_ALL;
    #[cfg(mirai)]
    type SecretTaint = SecretTaintKind<SECRET_TAINT>;
    #[cfg(not(mirai))]
    type SecretTaint = ();
    
    struct A(u32);
    struct B(u32);
    struct C(u32);
    
    fn a_to_b(a: A) -> B {
        precondition!(has_tag!(&a, SecretTaint));
        let b = B(a.0 + 1);
        b
    }
    
    fn b_to_c(b: B) -> C {
        precondition!(has_tag!(&b, SecretTaint));
        let c = C(b.0 + 1);
        c
    }
    
    fn main() {
        let a = A(1);
        add_tag!(&a, SecretTaint);
        let b = a_to_b(a);
        verify!(has_tag!(&b, SecretTaint));
        let c = b_to_c(b);
        verify!(has_tag!(&c, SecretTaint));
        println!("reachable?");
    }
    

    Expected Behavior

    Satisfied verification

    Actual Results

    MIRAI complains:

    $ cargo mirai
        Checking mirai_test v0.1.0 (/Users/v_chenhongbo04/Code/mirai_test)
    warning: unsatisfied precondition
      --> src/main.rs:43:13
       |
    43 |     let c = b_to_c(b);
       |             ^^^^^^^^^
       |
    note: related location
      --> src/main.rs:33:5
       |
    33 |     precondition!(has_tag!(&b, SecretTaint));
       |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
       = note: this warning originates in the macro `precondition` (in Nightly builds, run with -Z macro-backtrace for more info)
    
    warning: this is unreachable, mark it as such by using the verify_unreachable! macro
      --> src/main.rs:44:5
       |
    44 |     verify!(has_tag!(&c, SecretTaint));
       |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    
    warning: `mirai_test` (bin "mirai_test") generated 2 warnings
        Finished dev [unoptimized + debuginfo] target(s) in 0.72s
    

    Environment

    rustc 1.61.0-nightly (c84f39e6c 2022-03-20)

    I'm using the latest MIRAI with the same rust toolchain version.

    opened by ya0guang 0
  • Make k-limits into command line options

    Make k-limits into command line options

    Issue

    Currently a set of constants in checker/src/k_limits.rs provides limits on how much computation MIRAI will do in various places. With these limits in place, largish crates can be analyzed in a somewhat reasonable time frame. The limits do, however, impact on precision and may lead to false negatives. By making these into variables that can be set via command line options, it will become possible to schedule longer runs that may find more issues than more limited runs. The greater precision allowed by such runs can also be used to weed out false positives.

    The recommended way to complete this task is to turn the constants in k_limits into the fields of a struct and to provide a constructor that sets the fields to default values, along with a command line processor that updates the values from options in the command line.

    The limits struct should then be made part of the visitor state (checker/src/visitor.rs).

    Ideally, there should also be a way to set these options to non default values for integration test cases. See also #52.

    enhancement good first issue 
    opened by hermanventer 2
  • Meta Meta Issue: Create meta issues

    Meta Meta Issue: Create meta issues

    Issue

    We need more issues. Create some meta issues to spur the creation of more issues.

    Steps to Reproduce

    Look at the issues tab.

    Expected Behavior

    There should be more issues and meta issues.

    Actual Results

    Not enough issues.

    opened by hermanventer 0
  • Meta Issue: Code Coverage

    Meta Issue: Code Coverage

    Issue

    Some parts of the MIRAI code base are not covered by integration tests. You task here is to find such bits of code and to create an issue for each of them. Ideally follow up with a PR that contains a test case that covers that bit of code.

    Steps to Reproduce

    As you read through the code base to get to know it, click on the coverage button so see code coverage. The code coverage tools is not quite perfect, so you might see lines that are marked as not covered when they obviously are, but there will be some cases that are not obviously covered. You can verify that a line of code is not covered by setting a break point on it and running the integration tests from the debugger.

    If you are going to follow up with a PR to fix this omission, the next step would be to set some breakpoints in the surrounding covered code to find the test cases that reach then and then try to mutate one or more of those test cases to instead or also reach the uncovered code.

    Expected Behavior

    Every executable source line should be reached by an integration test case.

    Actual Results

    Some code lines are not so covered.

    good first issue 
    opened by hermanventer 0
  • Meta Issue: Fix developer instructions

    Meta Issue: Fix developer instructions

    Issue

    If you like compilers and related tools, you are a meta-programmer, so you should like meta issues as well. This issue is a task to create tasks.

    Since you are new here, please keep track of all of the surprises you've encountered and the things you had to find out the hard way. Then make an issue to get the fixed.

    Ideally, follow that up with PR in which you fix it. Many thanks for doing that!

    Steps to Reproduce

    Read the developer documentation and try to fix an issue.

    Expected Behavior

    You got going with no problems and everything is crystal clear.

    Actual Results

    You muttered WTF on several occasions.

    good first issue 
    opened by hermanventer 0
Releases(v1.1.3)
  • v1.1.3(Nov 29, 2022)

  • v1.1.2(Sep 29, 2022)

  • v1.1.0(Dec 21, 2021)

  • libra_v1.0.4(Sep 19, 2019)

    Use separate lock file to avoid panic in Sled. Only share the persistent store between crates if flag is present. Contracts for variants of rand.Rng.gen_range and rand.Rng.gen_bool. Give diagnostics if non public function is a call tree root. MIR assertions now treated just like verify.

    Source code(tar.gz)
    Source code(zip)
  • v1.0.3(Sep 11, 2019)

    Make --sysroot available for the command line. Add a rust-toolchain Make core::slice::Iter methods generic. Add def ids for un-summarized functions in the call graph being analyzed. Add (assume|verify)_unreachable macros. Make the result of an uninterpreted call more complete to allow better refinement. Promote pre/post conditions for async functions.

    Source code(tar.gz)
    Source code(zip)
  • libra_v1.0.3(Sep 11, 2019)

    Make --sysroot available for the command line. Add a rust-toolchain Make core::slice::Iter methods generic. Add def ids for un-summarized functions in the call graph being analyzed. Add (assume|verify)_unreachable macros. Make the result of an uninterpreted call more complete to allow better refinement. Promote pre/post conditions for async functions.

    Source code(tar.gz)
    Source code(zip)
  • v1.0.2(Aug 27, 2019)

    Standard library summaries for cmp::max. Use joins for conditional expressions with conditions that are TOP. Fix bug in refinement of conditional expressions. Apply binary operation distribution recursively during expression simplification. Discard join condition when joining backward branches (keeps path conditions simpler during fixed point loops).

    Source code(tar.gz)
    Source code(zip)
  • v1.0.1(Aug 16, 2019)

    Fixes a bug with name mangling when macros are involved. More standard library contracts. Updates dependencies. Ignores predecessor blocks that are known not to reach a block after round 1 of the fixed point loop. Fixes diagnostic formatting that resulted in "possible possible ..." messages.

    Source code(tar.gz)
    Source code(zip)
  • v1.0.0(Aug 2, 2019)

Owner
Facebook Experimental
These are Facebook projects that are not necessarily used in production but are being developed in the open nevertheless.
Facebook Experimental
a wasm interpreter written by rust

wai (WebAssembly interpreter) A simple wasm interpreter This is an ongoing project DEMO 2021-06-27.10.23.18.mov Install Install via Homebrew brew inst

nasa 69 Dec 6, 2022
A simple interpreter for the mathematical random-access machine

Random-access machine runner A simple Rust RAM program runner. Lexer/Parser Program executor Code formatter Web Compiled to WASM to run in the browser

Marcin Wojnarowski 5 Jan 14, 2023
A high level diffing library for rust based on diffs

Similar: A Diffing Library Similar is a dependency free crate for Rust that implements different diffing algorithms and high level interfaces for it.

Armin Ronacher 617 Dec 30, 2022
High level rust abstractions for the libretro API

libretro-rs Design Philosophy The approach to this crate can best be summarized as wanting to expose all functionality, even if not idiomatically. The

null 9 Dec 25, 2022
Mononym is a library for creating unique type-level names for each value in Rust.

Mononym is a library for creating unique type-level names for each value in Rust.

MaybeVoid 52 Dec 16, 2022
Low level access to ATmega32U4 registers in Rust

Deprecation Note: This crate will soon be deprecated in favor of avr-device. The approach of generating the svd from hand-written register definitions

Rahix 9 Jan 27, 2021
A Rust framework to develop and use plugins within your project, without worrying about the low-level details.

VPlugin: A plugin framework for Rust. Website | Issues | Documentation VPlugin is a Rust framework to develop and use plugins on applications and libr

VPlugin 11 Dec 31, 2022
A low-ish level tool for easily writing and hosting WASM based plugins.

A low-ish level tool for easily writing and hosting WASM based plugins. The goal of wasm_plugin is to make communicating across the host-plugin bounda

Alec Deason 62 Sep 20, 2022
A low-level I/O ownership and borrowing library

This library introduces OwnedFd, BorrowedFd, and supporting types and traits, and corresponding features for Windows, which implement safe owning and

Dan Gohman 74 Jan 2, 2023
High-level documentation for rerun

rerun-docs This is the high-level documentation for rerun that is hosted at https://www.rerun.io/docs Other documentation API-level documentation for

rerun.io 9 Feb 19, 2023
k-mer counter in Rust using the rust-bio and rayon crates

krust is a k-mer counter written in Rust and run from the command line that will output canonical k-mers and their frequency across the records in a f

null 14 Jan 7, 2023
Experimental Rust tool for generating FFI definitions allowing many other languages to call Rust code

Diplomat is an experimental Rust tool for generating FFI definitions allowing many other languages to call Rust code. With Diplomat, you can simply define Rust APIs to be exposed over FFI and get high-level C, C++, and JavaScript bindings automatically!

null 255 Dec 30, 2022
Aws-sdk-rust - AWS SDK for the Rust Programming Language

The AWS SDK for Rust This repo contains the new AWS SDK for Rust (the SDK) and its public roadmap. Please Note: The SDK is currently released as a dev

Amazon Web Services - Labs 2k Jan 3, 2023
Rust + Yew + Axum + Tauri, full-stack Rust development for Desktop apps.

rust-yew-axum-tauri-desktop template Rust + Yew + Axum + Tauri, full-stack Rust development for Desktop apps. Crates frontend: Yew frontend app for de

Jet Li 54 Dec 23, 2022
A lightning fast version of tmux-fingers written in Rust, copy/pasting tmux like vimium/vimperator

tmux-thumbs A lightning fast version of tmux-fingers written in Rust for copy pasting with vimium/vimperator like hints. Usage Press ( prefix + Space

Ferran Basora 598 Jan 2, 2023
A command-line tool collection to assist development written in RUST

dtool dtool is a command-line tool collection to assist development Table of Contents Description Usage Tips Installation Description Now dtool suppor

GB 314 Dec 18, 2022
Migrate C code to Rust

C2Rust helps you migrate C99-compliant code to Rust. The translator (or transpiler) produces unsafe Rust code that closely mirrors the input C code. T

Immunant 3k Jan 8, 2023
C to Rust translator

Corrode: Automatic semantics-preserving translation from C to Rust This program reads a C source file and prints an equivalent module in Rust syntax.

Jamey Sharp 2.1k Dec 14, 2022
Astronomical algorithms in Rust

astro-rust Contents API Docs About Usage Contributing References About astro-rust is a library of advanced astronomical algorithms for the Rust progra

Saurav Sachidanand 213 Jan 7, 2023