Skip to content

A false negative bug in MIRAI #36

@stoneman258

Description

@stoneman258

Issue

While using MIRAI to analyze a project, I observed that it attempts to consolidate two calls the same function (which lead to out-of-bounds access) into a single warning report, but these two calls are not on the same control flow path.

Steps to Reproduce

Here is the test case:

fn main() {

}
fn pure_oob(s: &[i32]) -> i32 {
    s[0]  
}
fn third(s: &[i32]) -> i32 {
    s[2]  
}

fn thirdp(s: &[i32]) -> i32 {
    s[3]  
}

pub fn test(cond: bool) {
    let s = [0;2];
    if cond {
        let a = pure_oob(&s);
    } else {
        let b = third(&s);
    }
    let c = third(&s); //if call thirdp here, the report will have the call to thirdp.
} 

Then run cargo mirai in test case.

Expected Behavior

If I change the call in line 22 to thirdp, MIRAI will report 2 warnings about out of bounds.

warning: [MIRAI] index out of bounds
  --> src/main.rs:20:17
   |
20 |         let b = third(&s);
   |                 ^^^^^^^^^
   |
note: related location
  --> src/main.rs:8:5
   |
8  |     s[2]  
   |     ^^^^

warning: [MIRAI] index out of bounds
  --> src/main.rs:22:13
   |
22 |     let c = thirdp(&s);
   |             ^^^^^^^^^^
   |
note: related location
  --> src/main.rs:12:5
   |
12 |     s[3]  
   |     ^^^^

Thus I think the call chain to line 8 will be 2 warnings when call third in line 22.

Actual Results

MIRAI only report the call to third in line 20, but miss the call in line 22.

warning: [MIRAI] index out of bounds
  --> src/main.rs:20:17
   |
20 |         let b = third(&s);
   |                 ^^^^^^^^^
   |
note: related location
  --> src/main.rs:8:5
   |
8  |     s[2]  
   |     ^^^^

Environment

Rust version (rustc --version)
rustc 1.86.0-nightly (824759493 2025-01-09)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions