Skip to content

Commit 4322394

Browse files
committed
Add contracts for all functions in Alignment
Uses the contracts syntax introduced in #128045.
1 parent 69482e8 commit 4322394

File tree

2 files changed

+25
-0
lines changed

2 files changed

+25
-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/ptr/alignment.rs

+24
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,10 @@ impl Alignment {
4343
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
4444
#[inline]
4545
#[must_use]
46+
#[cfg_attr(not(bootstrap), core::contracts::requires(
47+
mem::align_of::<T>().is_power_of_two()))]
48+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
49+
|result: &Alignment| result.as_usize().is_power_of_two()))]
4650
pub const fn of<T>() -> Self {
4751
// This can't actually panic since type alignment is always a power of two.
4852
const { Alignment::new(mem::align_of::<T>()).unwrap() }
@@ -54,6 +58,9 @@ impl Alignment {
5458
/// Note that `0` is not a power of two, nor a valid alignment.
5559
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
5660
#[inline]
61+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
62+
|result: &Option<Alignment>| align.is_power_of_two() == result.is_some() &&
63+
(result.is_none() || result.unwrap().as_usize() == align)))]
5764
pub const fn new(align: usize) -> Option<Self> {
5865
if align.is_power_of_two() {
5966
// SAFETY: Just checked it only has one bit set
@@ -73,6 +80,10 @@ impl Alignment {
7380
/// It must *not* be zero.
7481
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
7582
#[inline]
83+
#[cfg_attr(not(bootstrap), core::contracts::requires(align > 0 && (align & (align - 1)) == 0))]
84+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
85+
|result: &Alignment| result.as_usize() == align &&
86+
result.as_usize().is_power_of_two()))]
7687
pub const unsafe fn new_unchecked(align: usize) -> Self {
7788
assert_unsafe_precondition!(
7889
check_language_ub,
@@ -88,13 +99,18 @@ impl Alignment {
8899
/// Returns the alignment as a [`usize`].
89100
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
90101
#[inline]
102+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
103+
|result: &usize| result.is_power_of_two()))]
91104
pub const fn as_usize(self) -> usize {
92105
self.0 as usize
93106
}
94107

95108
/// Returns the alignment as a <code>[NonZero]<[usize]></code>.
96109
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
97110
#[inline]
111+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
112+
|result: &NonZero<usize>| result.get().is_power_of_two() &&
113+
result.get() == self.as_usize()))]
98114
pub const fn as_nonzero(self) -> NonZero<usize> {
99115
// This transmutes directly to avoid the UbCheck in `NonZero::new_unchecked`
100116
// since there's no way for the user to trip that check anyway -- the
@@ -120,6 +136,10 @@ impl Alignment {
120136
/// ```
121137
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
122138
#[inline]
139+
#[cfg_attr(not(bootstrap), core::contracts::requires(self.as_usize().is_power_of_two()))]
140+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
141+
|result: &u32| (*result as usize) < mem::size_of::<usize>() * 8 &&
142+
(1usize << *result) == self.as_usize()))]
123143
pub const fn log2(self) -> u32 {
124144
self.as_nonzero().trailing_zeros()
125145
}
@@ -149,6 +169,10 @@ impl Alignment {
149169
/// ```
150170
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
151171
#[inline]
172+
#[cfg_attr(not(bootstrap), core::contracts::ensures(
173+
|result: &usize| *result > 0 &&
174+
*result == !(self.as_usize() -1) &&
175+
self.as_usize() & *result == self.as_usize()))]
152176
pub const fn mask(self) -> usize {
153177
// SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
154178
!(unsafe { self.as_usize().unchecked_sub(1) })

0 commit comments

Comments
 (0)