Differences on function calls emitted by HIR and MIR

[zjp-CN]

HIR and MIR can emit different function calls for the same body:

#[kani::proof]
fn standard_proof() {
    let val: u8 = kani::any();
    assert_eq!(val, 1, "Not eq to 1.");
}

(- was from HIR, + was from StableMIR)

             "func": "fn standard_proof() {\n        let val: u8 = kani::any();\n        assert_eq!(val, 1, \"Not eq to 1.\");\n    }",
             "callees": [
-              "DefId(3:10310 ~ core[abab]::panicking::panic_fmt)",
-              "DefId(20:281 ~ kani[75bd]::assert)",
-              "DefId(20:283 ~ kani[75bd]::any)"
+              "FnDef(DefId { id: 5, name: \"kani::any\" })",
+              "FnDef(DefId { id: 6, name: \"kani::assert\" })"

core[abab]::panicking::panic_fmt is omitted by stable mir, which is confusing.

---

// StableMIR
fn verify::standard_proof() -> () {
    let mut _0: ();
    let  _1: u8;
    let  _2: ();
    let mut _3: bool;
    let mut _4: bool;
    let mut _5: bool;
    debug val => _1;
    bb0: {
        _1 = kani::any::<u8>() -> [return: bb1, unwind continue];
    }
    bb1: {
        _5 = Eq(_1, 1_u8);
        _4 = Not(move _5);
        _3 = Not(move _4);
        _2 = kani::assert(move _3, "\"Not eq to 1.\"") -> [return: bb2, unwind continue];
    }
    bb2: {
        return;
    }
}

[zjp-CN]

With Kani's reachability analysis, I got all nested callees of standard_proof:

[src/functions/kani/reachability.rs:79:5] item_names = [
    "kani::kani_intrinsic::<u8>",
    "kani::assert",
    "kani::any_raw::<u8>",
    "verify::standard_proof",
    "kani::any_raw_internal::<u8>",
    "kani::any::<u8>",
    "<u8 as kani::Arbitrary>::any",
]

Hooray!

But still no core[abab]::panicking::panic_fmt. (I didn't mean to incorporate it, just pointing out the difference.)

[celinval]

@zjp-CN, Kani overrides the definition of panic_eq macro here.

So what happens is that the following statement

assert_eq!(val, 1, "Not eq to 1.");

is being expanded to

kani::assert(val == 1);
if false {
  format!("Not eq to 1")
}

You can see this by setting RUSTFLAGS=-Zunpretty=expanded.

I'm assuming that MIR optimization passes are removing the obviously dead code, so the format call does not show up in StableMIR.

[zjp-CN]

Thanks for the explanation.

And RUSTFLAGS=-Zunpretty=expanded is the flag I'm looking for, with that, I can see core::panicking::panic_fmt and false branch as you said:

    #[allow(dead_code)]
    #[kanitool::proof]
    fn standard_proof() {
        let val: u8 = kani::any();
        {
            {
                kani::assert(!!((val) == (1)), "\"Not eq to 1.\"");
                if false {
                        if !true {
                                {
                                    ::core::panicking::panic_fmt(format_args!("Not eq to 1."));
                                }
                            };
                    }
            };
        };
    }

It's really helpful!