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
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]
Copy link
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?

Copy link
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?

Copy link
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.

Copy link
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.

Copy link
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?

Copy link
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?

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