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)

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

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:

All I have to do is to provide the DYLD_LIBRARY_PATH as specified:

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.

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

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?

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

2. git clone https://github.com/facebookexperimental/MIRAI.git
3. cd MIRAI
4. ./setup.sh
5. 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)

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

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)

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

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>.

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)

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)

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.

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.

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.

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.

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.