Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit e40222d

Browse files
committedMar 13, 2025
Add contracts for all functions in Alignment
Uses the contracts syntax introduced in #128045.
1 parent 93257e2 commit e40222d

File tree

3 files changed

+37
-0
lines changed

3 files changed

+37
-0
lines changed
 

‎library/core/src/lib.rs

+1
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,7 @@
108108
//
109109
// Library features:
110110
// tidy-alphabetical-start
111+
#![cfg_attr(not(bootstrap), feature(contracts))]
111112
#![feature(array_ptr_get)]
112113
#![feature(asm_experimental_arch)]
113114
#![feature(bigint_helper_methods)]

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

+2
Original file line numberDiff line numberDiff line change
@@ -476,6 +476,8 @@ pub const fn align_of<T>() -> usize {
476476
#[stable(feature = "rust1", since = "1.0.0")]
477477
#[rustc_const_stable(feature = "const_align_of_val", since = "1.85.0")]
478478
#[allow(deprecated)]
479+
#[rustc_allow_const_fn_unstable(contracts)]
480+
#[cfg_attr(not(bootstrap), core::contracts::ensures(|result: &usize| result.is_power_of_two()))]
479481
pub const fn align_of_val<T: ?Sized>(val: &T) -> usize {
480482
// SAFETY: val is a reference, so it's a valid raw pointer
481483
unsafe { intrinsics::min_align_of_val(val) }

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

+34
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,9 @@ impl Alignment {
4343
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
4444
#[inline]
4545
#[must_use]
46+
#[rustc_allow_const_fn_unstable(contracts)]
47+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
48+
|result: &Alignment| result.as_usize().is_power_of_two()))]
4649
pub const fn of<T>() -> Self {
4750
// This can't actually panic since type alignment is always a power of two.
4851
const { Alignment::new(align_of::<T>()).unwrap() }
@@ -54,6 +57,11 @@ impl Alignment {
5457
/// Note that `0` is not a power of two, nor a valid alignment.
5558
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
5659
#[inline]
60+
#[rustc_allow_const_fn_unstable(contracts)]
61+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
62+
move
63+
|result: &Option<Alignment>| align.is_power_of_two() == result.is_some() &&
64+
(result.is_none() || result.unwrap().as_usize() == align)))]
5765
pub const fn new(align: usize) -> Option<Self> {
5866
if align.is_power_of_two() {
5967
// SAFETY: Just checked it only has one bit set
@@ -73,6 +81,12 @@ impl Alignment {
7381
/// It must *not* be zero.
7482
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
7583
#[inline]
84+
#[cfg_attr(not(bootstrap), rustc_const_unstable(feature = "contracts", issue = "128044"))]
85+
#[cfg_attr(not(bootstrap), core::contracts::requires(align.is_power_of_two()))]
86+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
87+
move
88+
|result: &Alignment| result.as_usize() == align &&
89+
result.as_usize().is_power_of_two()))]
7690
pub const unsafe fn new_unchecked(align: usize) -> Self {
7791
assert_unsafe_precondition!(
7892
check_language_ub,
@@ -88,13 +102,21 @@ impl Alignment {
88102
/// Returns the alignment as a [`usize`].
89103
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
90104
#[inline]
105+
#[rustc_allow_const_fn_unstable(contracts)]
106+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
107+
|result: &usize| result.is_power_of_two()))]
91108
pub const fn as_usize(self) -> usize {
92109
self.0 as usize
93110
}
94111

95112
/// Returns the alignment as a <code>[NonZero]<[usize]></code>.
96113
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
97114
#[inline]
115+
#[rustc_allow_const_fn_unstable(contracts)]
116+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
117+
move
118+
|result: &NonZero<usize>| result.get().is_power_of_two() &&
119+
result.get() == self.as_usize()))]
98120
pub const fn as_nonzero(self) -> NonZero<usize> {
99121
// This transmutes directly to avoid the UbCheck in `NonZero::new_unchecked`
100122
// since there's no way for the user to trip that check anyway -- the
@@ -120,6 +142,12 @@ impl Alignment {
120142
/// ```
121143
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
122144
#[inline]
145+
#[cfg_attr(not(bootstrap), rustc_const_unstable(feature = "contracts", issue = "128044"))]
146+
#[cfg_attr(not(bootstrap), core::contracts::requires(self.as_usize().is_power_of_two()))]
147+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
148+
move
149+
|result: &u32| *result < usize::BITS &&
150+
(1usize << *result) == self.as_usize()))]
123151
pub const fn log2(self) -> u32 {
124152
self.as_nonzero().trailing_zeros()
125153
}
@@ -149,6 +177,12 @@ impl Alignment {
149177
/// ```
150178
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
151179
#[inline]
180+
#[cfg_attr(not(bootstrap), rustc_const_unstable(feature = "contracts", issue = "128044"))]
181+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
182+
move
183+
|result: &usize| *result > 0 &&
184+
*result == !(self.as_usize() -1) &&
185+
self.as_usize() & *result == self.as_usize()))]
152186
pub const fn mask(self) -> usize {
153187
// SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
154188
!(unsafe { self.as_usize().unchecked_sub(1) })

0 commit comments

Comments
 (0)
Failed to load comments.