Skip to content

Fix compiler_builtins upstream monomorphizations errors by inlining kani_contract_mode #4312

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
zjp-CN wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Fix compiler_builtins upstream monomorphizations errors by inlining kani_contract_mode #4312

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion library/kani_macros/src/sysroot/contracts/bootstrap.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ impl<'a> ContractConditionsHandler<'a> {
}
// Dummy function that we replace to pick the contract mode.
// By default, return ORIGINAL
#[inline(never)]
#[inline]

@tautschnig tautschnig Aug 22, 2025

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@zjp-CN zjp-CN Aug 22, 2025

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@tautschnig tautschnig Aug 22, 2025

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 zjp-CN Aug 24, 2025

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 zjp-CN Aug 26, 2025

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What efforts are needed to have this merged?

@zhassan-aws zhassan-aws Aug 26, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@tautschnig are we good here?

@feliperodri feliperodri Aug 16, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

#[kanitool::fn_marker = "kani_contract_mode"]
const fn kani_contract_mode() -> kani::internal::Mode {
kani::internal::ORIGINAL
Expand Down
Loading