Skip to content

Commit 061e529

Browse files
rust-bors[bot]rust-bors[bot]
authored
Auto merge of #136578 - tautschnig:upstream-contracts/alignment, r=<try>
Add contracts for all functions in `Alignment`
2 parents 8205e6b + 17e2c8a commit 061e529

17 files changed

+266
-57
lines changed

‎library/core/src/intrinsics/mod.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2647,6 +2647,7 @@ pub const unsafe fn const_make_global(ptr: *mut u8) -> *const u8 {
26472647
// doesn't honor `#[allow_internal_unstable]`, so for the const feature gate we use the user-facing
26482648
// `contracts` feature rather than the perma-unstable `contracts_internals`
26492649
#[rustc_const_unstable(feature = "contracts", issue = "128044")]
2650+
#[miri::intrinsic_fallback_is_spec]
26502651
#[lang = "contract_check_requires"]
26512652
#[rustc_intrinsic]
26522653
pub const fn contract_check_requires<C: Fn() -> bool + Copy>(cond: C) {
@@ -2676,6 +2677,7 @@ pub const fn contract_check_requires<C: Fn() -> bool + Copy>(cond: C) {
26762677
// `contracts` feature rather than the perma-unstable `contracts_internals`.
26772678
// Const-checking doesn't honor allow_internal_unstable logic used by contract expansion.
26782679
#[rustc_const_unstable(feature = "contracts", issue = "128044")]
2680+
#[miri::intrinsic_fallback_is_spec]
26792681
#[lang = "contract_check_ensures"]
26802682
#[rustc_intrinsic]
26812683
pub const fn contract_check_ensures<C: Fn(&Ret) -> bool + Copy, Ret>(

‎library/core/src/lib.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,7 @@
107107
#![feature(const_destruct)]
108108
#![feature(const_eval_select)]
109109
#![feature(const_select_unpredictable)]
110+
#![feature(contracts)]
110111
#![feature(core_intrinsics)]
111112
#![feature(coverage_attribute)]
112113
#![feature(disjoint_bitor)]

‎library/core/src/mem/mod.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -507,6 +507,8 @@ pub const fn align_of<T>() -> usize {
507507
#[must_use]
508508
#[stable(feature = "rust1", since = "1.0.0")]
509509
#[rustc_const_stable(feature = "const_align_of_val", since = "1.85.0")]
510+
#[rustc_allow_const_fn_unstable(contracts)]
511+
#[core::contracts::ensures(|result: &usize| result.is_power_of_two())]
510512
pub const fn align_of_val<T: ?Sized>(val: &T) -> usize {
511513
// SAFETY: val is a reference, so it's a valid raw pointer
512514
unsafe { intrinsics::align_of_val(val) }

‎library/core/src/ptr/alignment.rs‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,8 @@ impl Alignment {
4545
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
4646
#[inline]
4747
#[must_use]
48+
#[rustc_allow_const_fn_unstable(contracts)]
49+
#[core::contracts::ensures(|result: &Alignment| result.as_usize().is_power_of_two())]
4850
pub const fn of<T>() -> Self {
4951
// This can't actually panic since type alignment is always a power of two.
5052
const { Alignment::new(align_of::<T>()).unwrap() }
@@ -56,6 +58,11 @@ impl Alignment {
5658
/// Note that `0` is not a power of two, nor a valid alignment.
5759
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
5860
#[inline]
61+
#[rustc_allow_const_fn_unstable(contracts)]
62+
#[core::contracts::ensures(
63+
move |result: &Option<Alignment>|
64+
align.is_power_of_two() == result.is_some() &&
65+
(result.is_none() || result.unwrap().as_usize() == align))]
5966
pub const fn new(align: usize) -> Option<Self> {
6067
if align.is_power_of_two() {
6168
// SAFETY: Just checked it only has one bit set
@@ -76,6 +83,11 @@ impl Alignment {
7683
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
7784
#[inline]
7885
#[track_caller]
86+
#[rustc_allow_const_fn_unstable(contracts)]
87+
#[core::contracts::requires(align.is_power_of_two())]
88+
#[core::contracts::ensures(
89+
move |result: &Alignment|
90+
result.as_usize() == align && result.as_usize().is_power_of_two())]
7991
pub const unsafe fn new_unchecked(align: usize) -> Self {
8092
assert_unsafe_precondition!(
8193
check_language_ub,
@@ -91,13 +103,19 @@ impl Alignment {
91103
/// Returns the alignment as a [`usize`].
92104
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
93105
#[inline]
106+
#[rustc_allow_const_fn_unstable(contracts)]
107+
#[core::contracts::ensures(|result: &usize| result.is_power_of_two())]
94108
pub const fn as_usize(self) -> usize {
95109
self.0 as usize
96110
}
97111

98112
/// Returns the alignment as a <code>[NonZero]<[usize]></code>.
99113
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
100114
#[inline]
115+
#[rustc_allow_const_fn_unstable(contracts)]
116+
#[core::contracts::ensures(
117+
move |result: &NonZero<usize>|
118+
result.get().is_power_of_two() && result.get() == self.as_usize())]
101119
pub const fn as_nonzero(self) -> NonZero<usize> {
102120
// This transmutes directly to avoid the UbCheck in `NonZero::new_unchecked`
103121
// since there's no way for the user to trip that check anyway -- the
@@ -123,6 +141,11 @@ impl Alignment {
123141
/// ```
124142
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
125143
#[inline]
144+
#[rustc_const_unstable(feature = "contracts", issue = "128044")]
145+
#[core::contracts::requires(self.as_usize().is_power_of_two())]
146+
#[core::contracts::ensures(
147+
move |result: &u32|
148+
*result < usize::BITS && (1usize << *result) == self.as_usize())]
126149
pub const fn log2(self) -> u32 {
127150
self.as_nonzero().trailing_zeros()
128151
}
@@ -152,6 +175,11 @@ impl Alignment {
152175
/// ```
153176
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
154177
#[inline]
178+
#[rustc_const_unstable(feature = "contracts", issue = "128044")]
179+
#[core::contracts::ensures(
180+
move |result: &usize|
181+
*result > 0 && *result == !(self.as_usize() -1) &&
182+
self.as_usize() & *result == self.as_usize())]
155183
pub const fn mask(self) -> usize {
156184
// SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
157185
!(unsafe { self.as_usize().unchecked_sub(1) })

‎tests/mir-opt/dataflow-const-prop/default_boxed_slice.main.DataflowConstProp.32bit.panic-abort.diff‎

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,21 +18,37 @@
1818
scope 5 (inlined NonNull::<[bool; 0]>::dangling) {
1919
let mut _6: std::num::NonZero<usize>;
2020
scope 6 {
21-
scope 8 (inlined std::ptr::Alignment::as_nonzero) {
21+
scope 12 (inlined std::ptr::Alignment::as_nonzero) {
22+
scope 13 {
23+
scope 14 {
24+
scope 15 {
25+
}
26+
}
27+
}
28+
scope 16 (inlined core::contracts::build_check_ensures::<NonZero<usize>, {closure@std::ptr::Alignment::as_nonzero::{closure#0}}>) {
29+
}
2230
}
23-
scope 9 (inlined NonNull::<[bool; 0]>::without_provenance) {
31+
scope 17 (inlined NonNull::<[bool; 0]>::without_provenance) {
2432
let _7: *const [bool; 0];
25-
scope 10 {
33+
scope 18 {
2634
}
27-
scope 11 (inlined NonZero::<usize>::get) {
35+
scope 19 (inlined NonZero::<usize>::get) {
2836
}
29-
scope 12 (inlined std::ptr::without_provenance::<[bool; 0]>) {
30-
scope 13 (inlined without_provenance_mut::<[bool; 0]>) {
37+
scope 20 (inlined std::ptr::without_provenance::<[bool; 0]>) {
38+
scope 21 (inlined without_provenance_mut::<[bool; 0]>) {
3139
}
3240
}
3341
}
3442
}
3543
scope 7 (inlined std::ptr::Alignment::of::<[bool; 0]>) {
44+
scope 8 {
45+
scope 9 {
46+
scope 10 {
47+
}
48+
}
49+
}
50+
scope 11 (inlined core::contracts::build_check_ensures::<std::ptr::Alignment, {closure@std::ptr::Alignment::of<[bool; 0]>::{closure#0}}>) {
51+
}
3652
}
3753
}
3854
}

‎tests/mir-opt/dataflow-const-prop/default_boxed_slice.main.DataflowConstProp.32bit.panic-unwind.diff‎

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,21 +18,37 @@
1818
scope 5 (inlined NonNull::<[bool; 0]>::dangling) {
1919
let mut _6: std::num::NonZero<usize>;
2020
scope 6 {
21-
scope 8 (inlined std::ptr::Alignment::as_nonzero) {
21+
scope 12 (inlined std::ptr::Alignment::as_nonzero) {
22+
scope 13 {
23+
scope 14 {
24+
scope 15 {
25+
}
26+
}
27+
}
28+
scope 16 (inlined core::contracts::build_check_ensures::<NonZero<usize>, {closure@std::ptr::Alignment::as_nonzero::{closure#0}}>) {
29+
}
2230
}
23-
scope 9 (inlined NonNull::<[bool; 0]>::without_provenance) {
31+
scope 17 (inlined NonNull::<[bool; 0]>::without_provenance) {
2432
let _7: *const [bool; 0];
25-
scope 10 {
33+
scope 18 {
2634
}
27-
scope 11 (inlined NonZero::<usize>::get) {
35+
scope 19 (inlined NonZero::<usize>::get) {
2836
}
29-
scope 12 (inlined std::ptr::without_provenance::<[bool; 0]>) {
30-
scope 13 (inlined without_provenance_mut::<[bool; 0]>) {
37+
scope 20 (inlined std::ptr::without_provenance::<[bool; 0]>) {
38+
scope 21 (inlined without_provenance_mut::<[bool; 0]>) {
3139
}
3240
}
3341
}
3442
}
3543
scope 7 (inlined std::ptr::Alignment::of::<[bool; 0]>) {
44+
scope 8 {
45+
scope 9 {
46+
scope 10 {
47+
}
48+
}
49+
}
50+
scope 11 (inlined core::contracts::build_check_ensures::<std::ptr::Alignment, {closure@std::ptr::Alignment::of<[bool; 0]>::{closure#0}}>) {
51+
}
3652
}
3753
}
3854
}

‎tests/mir-opt/dataflow-const-prop/default_boxed_slice.main.DataflowConstProp.64bit.panic-abort.diff‎

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,21 +18,37 @@
1818
scope 5 (inlined NonNull::<[bool; 0]>::dangling) {
1919
let mut _6: std::num::NonZero<usize>;
2020
scope 6 {
21-
scope 8 (inlined std::ptr::Alignment::as_nonzero) {
21+
scope 12 (inlined std::ptr::Alignment::as_nonzero) {
22+
scope 13 {
23+
scope 14 {
24+
scope 15 {
25+
}
26+
}
27+
}
28+
scope 16 (inlined core::contracts::build_check_ensures::<NonZero<usize>, {closure@std::ptr::Alignment::as_nonzero::{closure#0}}>) {
29+
}
2230
}
23-
scope 9 (inlined NonNull::<[bool; 0]>::without_provenance) {
31+
scope 17 (inlined NonNull::<[bool; 0]>::without_provenance) {
2432
let _7: *const [bool; 0];
25-
scope 10 {
33+
scope 18 {
2634
}
27-
scope 11 (inlined NonZero::<usize>::get) {
35+
scope 19 (inlined NonZero::<usize>::get) {
2836
}
29-
scope 12 (inlined std::ptr::without_provenance::<[bool; 0]>) {
30-
scope 13 (inlined without_provenance_mut::<[bool; 0]>) {
37+
scope 20 (inlined std::ptr::without_provenance::<[bool; 0]>) {
38+
scope 21 (inlined without_provenance_mut::<[bool; 0]>) {
3139
}
3240
}
3341
}
3442
}
3543
scope 7 (inlined std::ptr::Alignment::of::<[bool; 0]>) {
44+
scope 8 {
45+
scope 9 {
46+
scope 10 {
47+
}
48+
}
49+
}
50+
scope 11 (inlined core::contracts::build_check_ensures::<std::ptr::Alignment, {closure@std::ptr::Alignment::of<[bool; 0]>::{closure#0}}>) {
51+
}
3652
}
3753
}
3854
}

‎tests/mir-opt/dataflow-const-prop/default_boxed_slice.main.DataflowConstProp.64bit.panic-unwind.diff‎

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,21 +18,37 @@
1818
scope 5 (inlined NonNull::<[bool; 0]>::dangling) {
1919
let mut _6: std::num::NonZero<usize>;
2020
scope 6 {
21-
scope 8 (inlined std::ptr::Alignment::as_nonzero) {
21+
scope 12 (inlined std::ptr::Alignment::as_nonzero) {
22+
scope 13 {
23+
scope 14 {
24+
scope 15 {
25+
}
26+
}
27+
}
28+
scope 16 (inlined core::contracts::build_check_ensures::<NonZero<usize>, {closure@std::ptr::Alignment::as_nonzero::{closure#0}}>) {
29+
}
2230
}
23-
scope 9 (inlined NonNull::<[bool; 0]>::without_provenance) {
31+
scope 17 (inlined NonNull::<[bool; 0]>::without_provenance) {
2432
let _7: *const [bool; 0];
25-
scope 10 {
33+
scope 18 {
2634
}
27-
scope 11 (inlined NonZero::<usize>::get) {
35+
scope 19 (inlined NonZero::<usize>::get) {
2836
}
29-
scope 12 (inlined std::ptr::without_provenance::<[bool; 0]>) {
30-
scope 13 (inlined without_provenance_mut::<[bool; 0]>) {
37+
scope 20 (inlined std::ptr::without_provenance::<[bool; 0]>) {
38+
scope 21 (inlined without_provenance_mut::<[bool; 0]>) {
3139
}
3240
}
3341
}
3442
}
3543
scope 7 (inlined std::ptr::Alignment::of::<[bool; 0]>) {
44+
scope 8 {
45+
scope 9 {
46+
scope 10 {
47+
}
48+
}
49+
}
50+
scope 11 (inlined core::contracts::build_check_ensures::<std::ptr::Alignment, {closure@std::ptr::Alignment::of<[bool; 0]>::{closure#0}}>) {
51+
}
3652
}
3753
}
3854
}

‎tests/mir-opt/dataflow-const-prop/default_boxed_slice.main.GVN.32bit.panic-abort.diff‎

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,21 +18,37 @@
1818
scope 5 (inlined NonNull::<[bool; 0]>::dangling) {
1919
let mut _6: std::num::NonZero<usize>;
2020
scope 6 {
21-
scope 8 (inlined std::ptr::Alignment::as_nonzero) {
21+
scope 12 (inlined std::ptr::Alignment::as_nonzero) {
22+
scope 13 {
23+
scope 14 {
24+
scope 15 {
25+
}
26+
}
27+
}
28+
scope 16 (inlined core::contracts::build_check_ensures::<NonZero<usize>, {closure@std::ptr::Alignment::as_nonzero::{closure#0}}>) {
29+
}
2230
}
23-
scope 9 (inlined NonNull::<[bool; 0]>::without_provenance) {
31+
scope 17 (inlined NonNull::<[bool; 0]>::without_provenance) {
2432
let _7: *const [bool; 0];
25-
scope 10 {
33+
scope 18 {
2634
}
27-
scope 11 (inlined NonZero::<usize>::get) {
35+
scope 19 (inlined NonZero::<usize>::get) {
2836
}
29-
scope 12 (inlined std::ptr::without_provenance::<[bool; 0]>) {
30-
scope 13 (inlined without_provenance_mut::<[bool; 0]>) {
37+
scope 20 (inlined std::ptr::without_provenance::<[bool; 0]>) {
38+
scope 21 (inlined without_provenance_mut::<[bool; 0]>) {
3139
}
3240
}
3341
}
3442
}
3543
scope 7 (inlined std::ptr::Alignment::of::<[bool; 0]>) {
44+
scope 8 {
45+
scope 9 {
46+
scope 10 {
47+
}
48+
}
49+
}
50+
scope 11 (inlined core::contracts::build_check_ensures::<std::ptr::Alignment, {closure@std::ptr::Alignment::of<[bool; 0]>::{closure#0}}>) {
51+
}
3652
}
3753
}
3854
}

‎tests/mir-opt/dataflow-const-prop/default_boxed_slice.main.GVN.32bit.panic-unwind.diff‎

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,21 +18,37 @@
1818
scope 5 (inlined NonNull::<[bool; 0]>::dangling) {
1919
let mut _6: std::num::NonZero<usize>;
2020
scope 6 {
21-
scope 8 (inlined std::ptr::Alignment::as_nonzero) {
21+
scope 12 (inlined std::ptr::Alignment::as_nonzero) {
22+
scope 13 {
23+
scope 14 {
24+
scope 15 {
25+
}
26+
}
27+
}
28+
scope 16 (inlined core::contracts::build_check_ensures::<NonZero<usize>, {closure@std::ptr::Alignment::as_nonzero::{closure#0}}>) {
29+
}
2230
}
23-
scope 9 (inlined NonNull::<[bool; 0]>::without_provenance) {
31+
scope 17 (inlined NonNull::<[bool; 0]>::without_provenance) {
2432
let _7: *const [bool; 0];
25-
scope 10 {
33+
scope 18 {
2634
}
27-
scope 11 (inlined NonZero::<usize>::get) {
35+
scope 19 (inlined NonZero::<usize>::get) {
2836
}
29-
scope 12 (inlined std::ptr::without_provenance::<[bool; 0]>) {
30-
scope 13 (inlined without_provenance_mut::<[bool; 0]>) {
37+
scope 20 (inlined std::ptr::without_provenance::<[bool; 0]>) {
38+
scope 21 (inlined without_provenance_mut::<[bool; 0]>) {
3139
}
3240
}
3341
}
3442
}
3543
scope 7 (inlined std::ptr::Alignment::of::<[bool; 0]>) {
44+
scope 8 {
45+
scope 9 {
46+
scope 10 {
47+
}
48+
}
49+
}
50+
scope 11 (inlined core::contracts::build_check_ensures::<std::ptr::Alignment, {closure@std::ptr::Alignment::of<[bool; 0]>::{closure#0}}>) {
51+
}
3652
}
3753
}
3854
}

0 commit comments

Comments
 (0)