Eliminate source of caller_location warnings in kani library

[zhassan-aws]

Description of changes:

Currently, running Kani on any program involving kani::any() results in a caller_location warning (see #2010). Turns out this intrinsic is brought in by the Kani library itself, more specifically due to the body of the kani::any_raw_inner function:

    unimplemented!("Kani any_raw_inner");

This macro ends up calling panic!, which calls panic_fmt, which calls std::panic::Location::caller which in turn calls std::intrinsics::caller_location. Thus, this PR replaces this call by another construct (empty loop) that does not result in the same call stack.

As a side effect, Kani compilation is sped up a bit. Even on this tiny program:

#[kani::proof]
fn main() {
    let _x: bool = kani::any();
}

I was noticing a slight pause when running Kani, which this PR eliminates. More specifically, before this change:

$ /usr/bin/time -p kani test.rs
...

real 0.91
user 0.75
sys 0.16

and after this change:

$ /usr/bin/time -p kani test.rs
...

real 0.15
user 0.12
sys 0.03

Another nice side effect is that the generated MIR is significantly smaller. Before this change:

$ RUSTFLAGS="--emit mir" kani test.rs
$ wc test.kani.mir
  7010  49876 865082 test.kani.mir

and after this change:

$ RUSTFLAGS="--emit mir" kani test.rs
$ wc test.kani.mir
  163  1019 10329 test.kani.mir

Resolved issues:

Resolves #2010

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

I could not find a way to test this. I tried creating a test with #![deny(warnings)], but even without the change, it doesn't fail, apparently because it's a Kani warning and not a compiler warning.

Testing:

• How is this change tested? See callout

• 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.

[celinval]

You could replace the empty loop by a call to an extern function, but that works for me.

[zhassan-aws]

You could replace the empty loop by a call to an extern function, but that works for me.

I couldn't figure out how to do that given that the function has a generic parameter. I'll merge this for the time being, but I'm open to suggestions as a follow-up PR.