How does the static analyzer work?

[mhoseinzadeh]

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?

[wrwg]

I assume you already found the instructions to run MIRAI in general in the README of the repo under Using MIRAI. Please be sure you also touch the source to force cargo the re-analyze (this is all a bit rudimentary as the system is in an early state; eventually we will have some cargo extension to run MIRAI).

If you are beyond that point, please try to set the env variable MIRAI_LOG=info with your run of MIRAI. This will give some diagnostics. If you are still not seeing what you expect, please add the log output to this thread so we can take a look.

[wrwg]

PS. Also please note that if you are using the experimental feature of using MIRAI together with annotations from the contracts crate, you must refer to the contracts crate in your Cargo.toml using features = [ "mirai_assertions" ].

[mhoseinzadeh]

Thanks. Now, I can see the analysis. Just one other issue is that how can we define none deterministic abstract values. For instance, in the code snippet of the question, if we receive i from the user, MIRAI can't analyze the main() function and gives the following:

[2019-12-06T21:49:11Z INFO  mirai::callbacks] Processing input file: examples/example1/src/main.rs
[2019-12-06T21:49:11Z INFO  mirai::callbacks] storing summaries for examples/example1/src/main.rs at /tmp/mirai_temp_dir.HO4aV4lJajzf/.summary_store.sled
[2019-12-06T21:49:11Z INFO  mirai::summaries] creating a non default new summary store
[2019-12-06T21:49:11Z INFO  mirai::callbacks] analyzing("example1.main")
[2019-12-06T21:49:11Z INFO  mirai::visitors] function main can't be analyzed because it calls function std.env.args which has no body and no summary (foreign fn argument key: _)
[2019-12-06T21:49:11Z INFO  mirai::callbacks] analyzing("example1.update.closure")
[2019-12-06T21:49:11Z INFO  mirai::callbacks] analyzing("example1.update")
    Finished dev [unoptimized + debuginfo] target(s) in 0.02s

The body of main() function is

pub fn main() {
    let args: Vec<String> = env::args().collect();

    let num = &args[1];
    let number: usize = if let Ok(n) = num.parse() {n} else {0};
    let mut x = [Box::new(2), Box::new(3)];
    update(&mut x, number, 8);
    println!("{:?}", x);
}

What type should I use for number?

[hermanventer]

The basic problem here is that there is no built in model for std.env.args. This is probably something that we should fix in MIRAI itself.

[mhoseinzadeh]

Thank you for you reply. Apart from std::env::args(), is there any way to specify a value as non-deterministic? If there was some type wrapper such as NonDeter<T>, it would be awesome. So, for the functions without models, we may capture the output in form of NonDeter generic type. Something like the following:

let number = NonDeter<usize>::from(if let Ok(n) = num.parse() {n} else {0});

Currently, how can we provide proofs for universal quantifiers? I mean, how it is possible to prove that a function (in this case, update()) is correct (or is not) for all inputs?

[hermanventer]

Currently the only way to create a non determinist value is by using result!(). This is not what you want because it can only be used inside a model. It should be easy enough to add a function like the one you want to mirai_annotations.

As for quantifiers: there is currently no support for them and they are not coming in the next few months. Our current focus is on bug finding and not on verification.

Contributions are very welcome, of course.

[hermanventer]

See #398 for support on how to create a non deterministic value.