-
Notifications
You must be signed in to change notification settings - Fork 13.7k
Add contracts for all functions in Alignment
#136578
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.
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
base: master
Are you sure you want to change the base?
Changes from all commits
85c9f58
6f71cb1
1025874
f4a8289
1e82a9b
23fefad
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -506,6 +506,8 @@ pub const fn align_of<T>() -> usize { | |
#[must_use] | ||
#[stable(feature = "rust1", since = "1.0.0")] | ||
#[rustc_const_stable(feature = "const_align_of_val", since = "1.85.0")] | ||
#[rustc_allow_const_fn_unstable(contracts)] | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I wonder if we should add There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Which functions would that affect? Ah, #136925 anyway needs to be resolved first. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'd still like to find a solution that does not require There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. @tautschnig did you try to make this change? |
||
#[core::contracts::ensures(|result: &usize| result.is_power_of_two())] | ||
pub const fn align_of_val<T: ?Sized>(val: &T) -> usize { | ||
// SAFETY: val is a reference, so it's a valid raw pointer | ||
unsafe { intrinsics::align_of_val(val) } | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -4,8 +4,8 @@ | |
|
||
// This function *looks* like it contains a call, but that call will be optimized out by MIR | ||
// optimizations. | ||
pub fn leaf_fn() -> String { | ||
String::new() | ||
pub fn leaf_fn() -> bool { | ||
Some(0).is_some() | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Is this the way we want to handle the test failure? Surely, we don't want contracts to affect the inlining? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Well, I think UB checks already do. IMO the important case is that trivial getters and setters that literally only do a field access get made cross-crate-inlineable. Also managing to detect functions that optimize to just a load or store is gravy. It's impossible in the general case, because of the limitations of the current compilation model and query system. And it's sometimes undesirable because making a function cross-crate-inlineable increases the amount of code that dependent crates need to compile, which can regress incremental build times. ... Wouldn't hurt to have that sort of explanation in the codebase. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. In addition, I think there's a possible future extension to the cross-crate-inlineable analysis that excludes code underneath a UB check or contract check from the cost model. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I believe disabled contracts should have zero runtime penalties, since they serve a different purpose to UB checks or any other form of existing runtime assertion. Their role is more akin to doctests: documentation that can be executed for testing purposes. Additionally contracts are a means to facilitate formal verification. These are the goals of contracts stated by the draft RFC.
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm not sure you understood what I was saying, so I'm rephrasing. UB checks currently have an impact on optimizations (that look exactly like the diff we are commenting on) even when they are completely disabled at runtime. In an ideal world, they wouldn't. But the actual consequences here are very minimal in practice, so we haven't yet invested very heavily in making the compiler perfect. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
But anyway it seems you want There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ah... please don't spread the discussion over multiple PRs, that will be impossible to follow. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Probably best to mark this PR here as a draft and suspend it until #144438 is done. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
I think this is an unreasonable criteria, and I tried to explain why by referring to the |
||
} | ||
|
||
// This function contains a call, even after MIR optimizations. It is only eligible for | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It seems that no backend actually overwrites this intrinsic. Why is it an intrinsic in the first place...? (Same for
contract_check_ensures
.)There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Other verification tools might tho. I need to ping the compiler team about design review of the existing design and long term solution.