Fix compiler_builtins upstream monomorphizations errors by inlining kani_contract_mode

[zjp-CN]

Resolves model-checking/verify-rust-std#477
Resolves os-checker/distributed-verification#111

kani_contract_mode with inline(never) will instantiate in libcore rather than compiler_builtins, which breaks the requirement that calls in compiler_builtins must be instantiated inside compiler_builtins. Rustc tools like dv will codegen such calls, while kani won't, so verify-rust-std doesn't have the error.

error: `compiler_builtins` cannot call functions through upstream monomorphizations; 
encountered invalid call from `core::ops::index_range::IndexRange::next_unchecked` 
to `core::ops::index_range::IndexRange::next_unchecked::kani_contract_mode`
   --> /home/gh-zjp-CN/distributed-verification/verify-rust-std/library/core/src/ops/index_range.rs:63:5
    |
 63 |     #[cfg_attr(kani, kani::modifies(self))] // 👈 annotated on core::ops::index_range::IndexRange::next_unchecked
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this attribute macro expansion

This PR make kani_contract_mode inline to make kani annotated APIs that are called in compiler_builtins be instantiated in compiler_builtins rather than libcore. I've tested the fix and it works for me.

Not sure why functions like kani_force_fn_once are fine even if they're marked #[inline(never)] to cause the trouble.

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

[tautschnig]

Wouldn't inlining break Kani's ability to replace the function by a mode set at Kani runtime?

[zjp-CN]

I have no idea on this. Is there a test for your concern?

[tautschnig]

I hope we do; the code of concern is the following:

kani/kani-compiler/src/kani_middle/transform/contracts.rs

Lines 424 to 435 in 8b8b897

	if let TerminatorKind::Call { func, target, destination, .. } = &bb.terminator.kind
	{
	let (callee, _) = func.ty(new_body.locals()).unwrap().kind().fn_def()?;
	let marker = KaniAttributes::for_def_id(tcx, callee.def_id()).fn_marker();
	if marker.is_some_and(|s| s.as_str() == "kani_contract_mode") {
	return Some((
	SourceInstruction::Terminator { bb: bb_idx },
	destination.clone(),
	target.unwrap(),
	));
	}
	}

I don't think this would continue to work if the call had been inlined.

[zjp-CN]

I think kani tests have already covered this logic, because the referenced snippet is from iterator.find_map(__find__kani_contract_mode__).unwrap(), meaning if kani_contract_mode call is not found, kani will panic and current tests will fail.

inline is a codegen attribute, while kani is an alternative rustc backend. I think code won't be eagerly "inlined" until codegen, so kani will see kani_contract_mode in MIR the Rust IR that only exists before codegen.

[zjp-CN]

What efforts are needed to have this merged?

[zhassan-aws]

@tautschnig are we good here?