Point-to-analysis fail if an instance does not have a body

[celinval]

I tried this code:

#[kani::proof]
fn check_sz() {
    let refstr = "hello";
    let ptr = refstr as *const _;
    assert_eq!(size_of_val(&ptr), 4);
}

using the following command line invocation:

kani check_sz.rs -Z uninit-checks

with Kani version:

I expected to see this happen: Verification succeeds

Instead, this happened: Kani crashes

Kani Rust Verifier 0.54.0 (standalone)
thread 'rustc' panicked at kani-compiler/src/kani_middle/points_to/points_to_analysis.rs:449:54:
called `Option::unwrap()` on a `None` value
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] no current codegen item.
[Kani] no current codegen location.

[artemagvanian]

That's weird. It seems like the error is caused by following this if branch:

kani/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs

Lines 208 to 210 in e6f8a62

	if self.tcx.is_mir_available(def_id) {
	self.apply_regular_call_effect(state, instance, args, destination);
	} else {

However, we later fail to obtain the actual body for the intrinsic here:

kani/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs

Lines 446 to 450 in e6f8a62

	let new_body = {
	let stable_instance = rustc_internal::stable(instance);
	let stable_body = stable_instance.body().unwrap();
	stable_body.internal_mir(self.tcx)
	};

I think we should be getting the body via instance_mir instead of jumping into StableMIR and back.

[celinval]

I believe the problem here is that is_mir_available is not sufficient since you also need to check if the intrinsic has to be overwritten.

StableMIR already includes both checks.

[celinval]

See https://github.com/rust-lang/rust/blob/4fe1e2bd5bf5a6f1cb245f161a5e9d315766f103/compiler/rustc_smir/src/rustc_smir/mod.rs#L74-L81

[artemagvanian]

Thanks! That's good to know. It turned out I only had to add support for 3 intrinsics to get rid of is_mir_available check altogether.