Skip to content

Commit e2f1a8e

Browse files
committed
Add contracts for all functions in Alignment
Uses the contracts syntax introduced in rust-lang#128045.
1 parent 57e620e commit e2f1a8e

File tree

3 files changed

+33
-0
lines changed

3 files changed

+33
-0
lines changed

library/core/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,7 @@
106106
#![feature(const_cmp)]
107107
#![feature(const_destruct)]
108108
#![feature(const_eval_select)]
109+
#![feature(contracts)]
109110
#![feature(core_intrinsics)]
110111
#![feature(coverage_attribute)]
111112
#![feature(disjoint_bitor)]

library/core/src/mem/mod.rs

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

library/core/src/ptr/alignment.rs

Lines changed: 30 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,12 @@ impl Alignment {
7683
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
7784
#[inline]
7885
#[track_caller]
86+
#[rustc_allow_const_fn_unstable(contracts)]
87+
#[allow(unused_parens)]
88+
#[core::contracts::requires(align.is_power_of_two())]
89+
#[core::contracts::ensures(
90+
move |result: &Alignment|
91+
result.as_usize() == align && result.as_usize().is_power_of_two())]
7992
pub const unsafe fn new_unchecked(align: usize) -> Self {
8093
assert_unsafe_precondition!(
8194
check_language_ub,
@@ -91,13 +104,19 @@ impl Alignment {
91104
/// Returns the alignment as a [`usize`].
92105
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
93106
#[inline]
107+
#[rustc_allow_const_fn_unstable(contracts)]
108+
#[core::contracts::ensures(|result: &usize| result.is_power_of_two())]
94109
pub const fn as_usize(self) -> usize {
95110
self.0 as usize
96111
}
97112

98113
/// Returns the alignment as a <code>[NonZero]<[usize]></code>.
99114
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
100115
#[inline]
116+
#[rustc_allow_const_fn_unstable(contracts)]
117+
#[core::contracts::ensures(
118+
move |result: &NonZero<usize>|
119+
result.get().is_power_of_two() && result.get() == self.as_usize())]
101120
pub const fn as_nonzero(self) -> NonZero<usize> {
102121
// This transmutes directly to avoid the UbCheck in `NonZero::new_unchecked`
103122
// since there's no way for the user to trip that check anyway -- the
@@ -123,6 +142,12 @@ impl Alignment {
123142
/// ```
124143
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
125144
#[inline]
145+
#[rustc_const_unstable(feature = "contracts", issue = "128044")]
146+
#[allow(unused_parens)]
147+
#[core::contracts::requires(self.as_usize().is_power_of_two())]
148+
#[core::contracts::ensures(
149+
move |result: &u32|
150+
*result < usize::BITS && (1usize << *result) == self.as_usize())]
126151
pub const fn log2(self) -> u32 {
127152
self.as_nonzero().trailing_zeros()
128153
}
@@ -152,6 +177,11 @@ impl Alignment {
152177
/// ```
153178
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
154179
#[inline]
180+
#[rustc_const_unstable(feature = "contracts", issue = "128044")]
181+
#[core::contracts::ensures(
182+
move |result: &usize|
183+
*result > 0 && *result == !(self.as_usize() -1) &&
184+
self.as_usize() & *result == self.as_usize())]
155185
pub const fn mask(self) -> usize {
156186
// SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
157187
!(unsafe { self.as_usize().unchecked_sub(1) })

0 commit comments

Comments
 (0)