-
Notifications
You must be signed in to change notification settings - Fork 14.1k
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: main
Are you sure you want to change the base?
Add contracts for all functions in Alignment
#136578
Conversation
|
Thanks for the pull request, and welcome! The Rust team is excited to review your changes, and you should hear from @tgross35 (or someone else) some time within the next two weeks. Please see the contribution instructions for more information. Namely, in order to ensure the minimum review times lag, PR authors and assigned reviewers should ensure that the review label (
|
This comment has been minimized.
This comment has been minimized.
|
You could also tag in a comment / PR description. |
|
Could you say some more about the motivation? This feature was merged only a number of hours ago, that seems soon to start using in std. Even once it is more stable, what should and shouldn't get contracts is probably something that needs to get discussed. @rust-lang/libs any thoughts here? |
|
Yeah, this was only approved as a lang experiment on the lang/compiler side, no idea what the situation is libs side (which certainly should be discussed). cc @pnkfelix @nikomatsakis @celinval (lang liason and ppl who were implementing this feature compiler side) |
|
I'll libs nominate this for discussion (this should only be discussed after the contracts people mentioned above have replied). |
|
Totally worth discussion, and it would be great to get some feedback on the features that are needed to meet the libs team bar. I am especially curious to see how you think contracts and |
|
It would be useful to know what your plan/intention is with adding contracts here. Is it just to try them out or is annotating the standard library with contracts for downstream consumers part of the goal of contracts? |
As far as the motivation is concerned: we're working towards https://rust-lang.github.io/rust-project-goals/2025h1/std-contracts.html, and I created this (draft) PR with the hope to initiate discussion while knowing there is a lot more work to be done on our end. As I am new contributor: is there other information that I can provide or another forum that I should use rather than this PR? |
Our current goal is https://rust-lang.github.io/rust-project-goals/2025h1/std-contracts.html, though we are in early stages and it indeed is about trying out what works best. Eventually we want to enable verification of downstream consumers, but a lot more work will be required before we get there. |
d46f868 to
7288286
Compare
This comment has been minimized.
This comment has been minimized.
Are there any docs on how contracts work as they exist today? Ignoring the stability question, we need something to refer to about how to use these properly, e.g. in https://doc.rust-lang.org/nightly/unstable-book/. Also, how are contracts that get merged into r-l/rust being verified? The linked page is somewhat vague about what this means for Bringing this up on the libs zulip would be a good idea to get the ball rolling https://rust-lang.zulipchat.com/#narrow/channel/219381-t-libs. |
library/core/src/ptr/alignment.rs
Outdated
| #[unstable(feature = "ptr_alignment_type", issue = "102070")] | ||
| #[inline] | ||
| #[must_use] | ||
| #[cfg_attr(not(bootstrap), contracts::requires(mem::align_of::<T>().is_power_of_two()))] |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
7288286 to
c180bd0
Compare
This comment has been minimized.
This comment has been minimized.
c180bd0 to
4322394
Compare
This comment has been minimized.
This comment has been minimized.
|
We discussed this in the libs meeting today. We're happy to add contracts to the standard library as an experiment, as long as this doesn't get in the way of normal standard library development. Depending on how the contracts feature evolves, we may reconsider our level of support. |
Updated via `./x.py test mir-opt --bless --stage 1` plus a manual tweak of `tests/mir-opt/gvn_ptr_eq_with_constant.main.GVN.diff`.
b7ba176 to
17e2c8a
Compare
|
This PR was rebased onto a different master commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
|
@bors try @rust-timer queue |
This comment has been minimized.
This comment has been minimized.
|
@tautschnig: 🔑 Insufficient privileges: not in try users |
|
@bors try @rust-timer queue |
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
Add contracts for all functions in `Alignment`
This comment has been minimized.
This comment has been minimized.
|
Finished benchmarking commit (061e529): comparison URL. Overall result: ❌✅ regressions and improvements - please read the text belowBenchmarking this pull request means it may be perf-sensitive – we'll automatically label it not fit for rolling up. You can override this, but we strongly advise not to, due to possible changes in compiler perf. Next Steps: If you can justify the regressions found in this try perf run, please do so in sufficient writing along with @bors rollup=never Instruction countOur most reliable metric. Used to determine the overall result above. However, even this metric can be noisy.
Max RSS (memory usage)Results (primary -1.4%, secondary 3.5%)A less reliable metric. May be of interest, but not used to determine the overall result above.
CyclesResults (secondary -2.4%)A less reliable metric. May be of interest, but not used to determine the overall result above.
Binary sizeResults (primary -0.1%, secondary 0.1%)A less reliable metric. May be of interest, but not used to determine the overall result above.
Bootstrap: 475.886s -> 473.036s (-0.60%) |
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.
The contract bits in alignment.rs seem fine to me, but it doesn't look like Ralf's comment about avoiding rustc_allow_const_fn_unstable at #136578 (comment) hasn't been resolved - is there something to do there?
Ralf is more involve with all of this than I, so
r? RalfJung
| #[rustc_const_unstable(feature = "contracts", issue = "128044")] | ||
| #[core::contracts::ensures( | ||
| move |result: &usize| | ||
| *result > 0 && *result == !(self.as_usize() -1) && |
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.
| *result > 0 && *result == !(self.as_usize() -1) && | |
| *result > 0 && *result == !(self.as_usize() - 1) && |
Formatting nit
@rustbot author |
|
Reminder, once the PR becomes ready for a review, use |
| #[inline] | ||
| #[must_use] | ||
| #[rustc_allow_const_fn_unstable(contracts)] | ||
| #[core::contracts::ensures(|result: &Alignment| result.as_usize().is_power_of_two())] |
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.
This is an odd contract, since the statement is true about all Alignment. Shouldn't it be a postcondition of as_usize instead?
| #[core::contracts::ensures( | ||
| move |result: &Option<Alignment>| | ||
| align.is_power_of_two() == result.is_some() && | ||
| (result.is_none() || result.unwrap().as_usize() == align))] |
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.
The formatting here is not great, with the code having the same indentation level as the closure header. What about something like this?
| #[core::contracts::ensures( | |
| move |result: &Option<Alignment>| | |
| align.is_power_of_two() == result.is_some() && | |
| (result.is_none() || result.unwrap().as_usize() == align))] | |
| #[core::contracts::ensures(move |result: &Option<Alignment>| | |
| align.is_power_of_two() == result.is_some() && | |
| (result.is_none() || result.unwrap().as_usize() == align) | |
| )] |
| #[rustc_allow_const_fn_unstable(contracts)] | ||
| #[core::contracts::ensures( | ||
| move |result: &NonZero<usize>| | ||
| result.get().is_power_of_two() && result.get() == self.as_usize())] |
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.
result.get() == self.as_usize() implies result.get().is_power_of_two()... seems odd to repeat that? If we always repeat the transitive closure of everything that can be deduced, that surely won't scale.^^
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.
What we really need is Type invariant. This is basically repeating the type invariant which should be implied.
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.
Well that would be even nicer, sure. But even with the status quo, I don't get the point of this contract. To make use of the is_power_of_two fact I have to call self.as_usize(), and at that point the is_power_of_two will be asserted. So what is the point of repeating it everywhere?
| #[core::contracts::requires(align.is_power_of_two())] | ||
| #[core::contracts::ensures( | ||
| move |result: &Alignment| | ||
| result.as_usize() == align && result.as_usize().is_power_of_two())] |
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.
result.as_usize().is_power_of_two() is redundant, it follows from the precondition and the first conjunct.
…ng, r=oli-obk Guard HIR lowered contracts with `contract_checks` Refactor contract HIR lowering to ensure no contract code is executed when contract-checks are disabled. The call to `contract_checks` is moved to inside the lowered fn body, and contract closures are built conditionally, ensuring no side-effects present in contracts occur when those are disabled. This partially addresses rust-lang#139548, i.e. the bad behavior no longer happens with contract checks disabled (`-Zcontract-checks=no`). The change is made in preparation for adding contract variable declarations - variables declared before the `requires` assertion, and accessible from both `requires` and `ensures`, but not in the function body (PR rust-lang#144444). As those declarations may also have side-effects, it's good to guard them with `contract_checks` - the new lowering approach allows for this to be done easily. Contracts tracking issue: rust-lang#128044 **Known limiatations**: - It is still possible to early return from the *function* from within a contract, e.g. ```rust #[ensures({if x > 0 { return 0 }; |_| true})] fn foo(x: u32) -> i32 { 42 } ``` When `foo` is called with an argument greater than 0, instead of `42`, `0` will be returned. As this is not a regression, it is not addressed in this PR. However, it may be worth revisiting later down the line, as users may expect a form of early return from *contract specifications*, and so returning from the entire *function* could cause confusion. - ~Contracts are still not optimised out when disabled. Currently, even when contracts are disabled, the code generated causes existing optimisations to fail, meaning even disabled contracts could impact runtime performance. This issue is blocking rust-lang#136578, and has not been addressed in this PR, i.e. the `mir-opt` and `codegen` tests that fail in rust-lang#136578 still fail with these new HIR lowering changes.~ Contracts should now be optimised out when disabled, however some regressions tests still need to be added to be sure that is indeed the case.
Uses the contracts syntax introduced in #128045.