Eliminate a source of code bloat in the kani library

[zhassan-aws]

Description of changes:

Same trick applied in #2032, but this time to the kani::panic function. In addition to eliminating the caller_location warning on a small program like this one:

#[kani::proof]
fn main() {
    panic!("Some message");
}

it also results in a speedup and a significant reduction in the MIR size.

Before:

$ /usr/bin/time -p kani simp_panic.rs
...
real 3.92
user 3.54
sys 0.37

$ RUSTFLAGS="--emit mir" kani simp_panic.rs
$ wc simp_panic.kani.mir 
  33248  237545 4173632 simp_panic.kani.mir

After:

$ /usr/bin/time -p kani simp_panic.rs
...
real 0.15
user 0.11
sys 0.04

$ RUSTFLAGS="--emit mir" kani simp_panic.rs
$ wc simp_panic.kani.mir 
  86  530 5399 simp_panic.kani.mir

Resolved issues:

Resolves #2010

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

Testing:

• How is this change tested? Couldn't find a way to test this.

• Is this a refactor change? No

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tedinski]

I'm slightly concerned about playing whack-a-mole with this.

With assess, I think we also see a lot of code bloat and caller_location. I haven't looked into it yet, but it'd be nice if we could integrate a hook or something in Kani that fixed all this everywhere, and then we could revert these back to being basic unreachable!() or whatever.

[tedinski]

#[doc(hidden)] for things we don't want customer-facing.

[zhassan-aws]

Is this needed for a private function?

[tedinski]

Oh, good point. Nevermind then :)

[celinval]

I don't think hooks will help here, since it would run after the reachability analysis. We could potentially plug hooks into the reachability analysis or use stubs here.

For the caller location warning, we should probably just fix it.

[celinval]

Also, I mentioned this to @zhassan-aws. Fixing our library is not really going to fix the problem in real user code, since any call to the std library that may eventually panic will bring in all that code. E.g.: unwrap().

[zhassan-aws]

Fixing our library is not really going to fix the problem in real user code, since any call to the std library that may eventually panic will bring in all that code. E.g.: unwrap().

True. One interesting thing though is that panic in particular seems to be excessively causing a MIR code bloat:

$ cat simp_panic.rs 
#[kani::proof]
fn main() {
    panic!("Some message");
}
$ RUSTFLAGS="--emit mir" kani simp_panic.rs
$ wc simp_panic.kani.mir 
  33248  237545 4173632 simp_panic.kani.mir

$ cat simp_unwrap.rs
#[kani::proof]
fn main() {
    let x: Option<i32> = kani::any();
    x.unwrap();
}
$ RUSTFLAGS="--emit mir" kani simp_unwrap.rs
$ wc simp_unwrap.kani.mir 
  1083   7418 124029 simp_unwrap.kani.mir

I'm not sure what else panic brings other than formatting code (which unwrap also bring as @celinval pointed out) that is causing the number of lines of MIR to be 33X that of the unwrap program.

These numbers are using c135fa9.

[zhassan-aws]

I evaluated the impact of this change on a few customer tests and found the reduction in the MIR size to be minimal. Abandoning this PR.