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?

[feliperodri]

@tautschnig I dug into this to try to settle it, since the concern is the right one to raise. Short answer: inlining does not break mode replacement, but not quite for the reason given above (and it's worth writing down).

The mechanism. set_mode scans the MIR blocks for a Call terminator whose callee carries the kani_contract_mode marker, and .unwrap()s the result:

https://github.com/model-checking/kani/blob/main/kani-compiler/src/kani_middle/transform/contracts.rs#L419-L440

So the failure mode you were worried about is a loud panic, not a silently wrong mode. @zjp-CN is right that the existing contract tests would catch it.

Where the "not inlined until codegen" argument is incomplete. Kani overrides optimized_mir (kani_middle/provide.rs:20-21) and reads bodies via tcx.instance_mir, so it sees MIR after rustc's MIR passes, which include the MIR Inline pass. #[inline] is not merely a codegen-time hint from Kani's point of view. The reason it is safe is more specific: that pass is off at the optimization level Kani compiles with.

Measured on nightly-2026-03-02, dumping the runtime-optimized MIR (what optimized_mir returns) for a #[inline] callee:

flags	call site survives?
(default, what Kani uses)	yes
-Zmir-opt-level=2	yes
-O	no — _0 = const 7_u8; scope 1 (inlined marker)
-Zinline-mir=yes	no
-O -Zmir-enable-passes=-Inline	yes

Kani passes no -C opt-level, so the default applies and the call is still there for set_mode to find. Note it is -O/-Zinline-mir that matters, not -Zmir-opt-level on its own.

Test evidence. With this PR merged onto today's main: expected/function-contract 109 passed / 0 failed, and the kani suite's Contract tests 8 passed / 0 failed. Since set_mode unwraps, a lost call is an immediate ICE, so these passing is direct evidence that both CHECK and REPLACE still find their marker.

The one caveat, which cuts the other way. base_rustc_flags appends the user's RUSTFLAGS verbatim (call_single_file.rs:290), so a user can turn the inliner on. I ran that A/B on a contract harness with proof_for_contract + stub_verified:

• main today (#[inline(never)]) + -Zinline-mir=yes → ICE: panicked at codegen/contract.rs:135: Function '_RNCNCNvCs..._1c7add_ones0_0s_0B5_' is not declared
• this PR (#[inline]) + -Zinline-mir=yes → clean diagnostic: error: The function specified in the proof_for_contract attribute, add_one, is not reachable from the harness

Same with -O. So contracts are already broken under MIR inlining on main, this PR does not introduce that, and it happens to turn an ICE into an actionable error. In neither case did set_mode's unwrap fire; under inlining the contracted function itself gets inlined into the harness and the reachability check fires first.

Why the other markers are fine, which @zjp-CN flagged as unexplained. kani_force_fn_once, kani_force_fn_once_with_args and kani_register_contract are all generic, so they are monomorphized into whichever crate calls them and never go through an upstream instantiation. kani_contract_mode is the only non-generic one, so its single instantiation lives in the defining crate and a call from compiler_builtins is exactly the upstream monomorphization that rustc rejects. #[inline] makes rustc emit a local copy in each CGU that needs it. That makes the fix principled rather than incidental and it suggests making the function generic would work too, though #[inline] is the smaller change.

Two optional hardenings, both better as separate PRs. Kani could pass -Zmir-enable-passes=-Inline so the invariant holds regardless of what a user puts in RUSTFLAGS (verified above that it preserves the call even under -O), and set_mode's .unwrap() could become a diagnostic that names the function instead of a panic. Neither is needed for this PR to be correct today.

One thing I did not verify: that this actually fixes the original compiler_builtins error, since I could not reproduce that build locally. That part still rests on @zjp-CN's report.

[feliperodri]

@zjp-CN could you add a code comment explaining why #[inline]? There is no test in Kani's suite that can catch a regression here, because reproducing it needs a compiler_builtins build. And #[inline(never)] is the intuitive choice for a marker function that must survive into MIR exactly what a future contributor would "fix" it back to. Something like:

  // `#[inline]`, not `#[inline(never)]`: this marker is the only non-generic one here, so
  // its single instantiation would live in the defining crate, and `compiler_builtins`
  // cannot call through an upstream monomorphization (rust-lang/rust#137222). `#[inline]`
  // makes rustc emit a local copy in each CGU. Kani still finds the call in MIR because
  // the MIR `Inline` pass is off at Kani's default opt level.