cargo mirai never warns me about anything.

[hermanventer]

Issue

False positive suppression leads to false negatives.

Steps to Reproduce

For example:

use argh::FromArgs;

#[derive(FromArgs)]
/// some args
struct Args {
    /// a value
    #[argh(positional)]
    a: usize,
}

pub fn main() {
    let args: Args = argh::from_env();
    let mut v: Vec<usize> = vec!();
    v.push(0);
    println!("{}", v[args.a]);
}

Following the instructions, I did:

git clone https://github.com/facebookexperimental/MIRAI.git
cd MIRAI
cargo install --locked --path ./checker
cd /path/to/crate
cargo mirai

Expected Behavior

It ought to object strenuously to v[args.a], but I get nothing!

Actual Results

No error.

Environment

rustc 1.70.0-nightly (22f247c6f 2023-03-13)

[johnperry-math]

Thanks for opening this issue! so I wasn't doing something wrong?

[hermanventer]

@johnperry-math

Instead of cargo mirai run MIRAI_FLAGS=--diag=verify cargo mirai.

Then you'll see

warning: possible index out of bounds
    --> examples/argh/src/main.rs:15:20
     |
15   |     println!("{}", v[args.a]);
     |                    ^^^^^^^^^
     |
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs:2703:9
     |
2703 |         Index::index(&**self, index)
     |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/slice/index.rs:261:10
     |
261  |         &(*slice)[self]
     |          ^^^^^^^^^^^^^^

warning: `arghtest` (bin "arghtest") generated 1 warning

Why? --diag=paranoid will tell you (sort of):

 MIRAI_FLAGS=--diag=paranoid cargo mirai
    Checking arghtest v0.1.0 (/Users/hermanventer/MIRAI/examples/argh)
**warning: the called function did not resolve to an implementation with a MIR body**
   --> /Users/hermanventer/.cargo/registry/src/index.crates.io-6f17d22bba15001f/argh-0.1.10/src/lib.rs:672:32
    |
672 |     let strings: Vec<String> = std::env::args_os()
    |                                ^^^^^^^^^^^^^^^^^^^

warning: the called function did not resolve to an implementation with a MIR body
    --> /Users/hermanventer/.cargo/registry/src/index.crates.io-6f17d22bba15001f/argh-0.1.10/src/lib.rs:1031:9
     |
1031 |         self.slot.fill_slot("", arg).map_err(|s| {
     |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: the called function did not resolve to an implementation with a MIR body
    --> /Users/hermanventer/.cargo/registry/src/index.crates.io-6f17d22bba15001f/argh-0.1.10/src/lib.rs:1083:17
     |
1083 |                 (self.parse_func)(&command, remaining_args)?;
     |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: possible unsatisfied precondition
    --> /Users/hermanventer/.cargo/registry/src/index.crates.io-6f17d22bba15001f/argh-0.1.10/src/lib.rs:1096:5
     |
1096 |     [&["help"], args].concat()
     |     ^^^^^^^^^^^^^^^^^^^^^^^^^^
     |
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/slice.rs:561:9
     |
561  |         Concat::concat(self)
     |         ^^^^^^^^^^^^^^^^^^^^
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/slice.rs:714:13
     |
714  |             result.extend_from_slice(v.borrow())
     |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs:2398:9
     |
2398 |         self.spec_extend(other.iter())
     |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/vec/spec_extend.rs:55:18
     |
55   |         unsafe { self.append_elements(slice) };
     |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs:1952:9
     |
1952 |         self.reserve(count);
     |         ^^^^^^^^^^^^^^^^^^^
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs:912:18
     |
912  |         self.buf.reserve(self.len, additional);
     |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/raw_vec.rs:290:28
     |
290  |             handle_reserve(slf.grow_amortized(len, additional));
     |                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/raw_vec.rs:405:43
     |
405  |         let ptr = finish_grow(new_layout, self.current_memory(), &mut self.alloc)?;
     |                                           ^^^^^^^^^^^^^^^^^^^^^
note: related location
    --> /Users/hermanventer/.rustup/toolchains/nightly-2023-03-14-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/raw_vec.rs:251:48
     |
251  |                 let size = mem::size_of::<T>().unchecked_mul(self.cap);
     |                                                ^^^^^^^^^^^^^^^^^^^^^^^

warning: `arghtest` (bin "arghtest") generated 4 warnings

The subtle answer lies in the warning: the called function did not resolve to an implementation with a MIR body messages. Since MIRAI has no idea what these functions are doing, all diagnostics produced for this function is somewhat suspect. So, by default, when you are presumably just looking for things that most likely are real errors, MIRAI decides to suppress any diagnostics for function main because the analysis is not sound due the unknown functions it calls.

This kind of trade-off is very tricky and perhaps the default needs to change. Ultimately that is really up to users.

So there are really two issues here:

1. The documentation issue: We need some tutorials that systematically explain these trade-offs.
2. MIRAI can do a better job here by adding "models" for the unknown functions to its builtin list of known functions.

[johnperry-math]

I confirm that setting this environment variable makes MIRAI emit the warnings I expect.

I'm not quite sure what you mean by the rest. If I read it correctly, you're saying that the issue was simply that MIRAI doesn't check main(). I'm pretty sure I'm not reading that correctly, because the issue first arose with MIRAI not complaining about a different, non-main() test function I'd written that wasn't emitting any warnings, and should have. Setting the environment variable does make MIRAI emit warnings on that other function.

That said, the test function was defined in the main.rs file of a bin crate. Is it possible that, had I defined it in a separate crate / module, MIRAI would have emitted warnings?

PS edited, hopefully for clarity

[hermanventer]

Its a bit more complicated: MIRAI does "whole program analysis", starting from "entry points". In this case the entry point is main and MIRAI checks all of the code that may be reachable from main.

The --diag flag controls the kind of error messages you'll see. The basic idea is that there are different kinds of audiences with different needs and expectations.

In default mode, very few warnings are displayed. Essentially only those for which there is a high probability that they show up a real error. The problem is how to decide if an error is real or not.

When the whole program analysis encounters a function with an unknown body, such as std::env::args_os, it does not know what effect this function will have on the state of the heap, so it goes into conservative mode and suppresses errors that depend on the heap state. In this case the value of args.a.

This is, of course, not the outcome we really want for this example and MIRAI needs fixing. I'll see what I can do over the weekend.

[johnperry-math]

I deleted the previous two comments when I realized that MIRAI wasn't warning about that library file precisely because there was nothing to warn. Apparently the function triggered a false positive when in main.rs.

I can elaborate if you want, but effectively I was looking at a different function than the one above. Adding an undeniably naughty function did trigger the expected warnings.

Sorry for the noise.