@@ -2,6 +2,8 @@ use crate::num::NonZero;
22use crate :: ub_checks:: assert_unsafe_precondition;
33use crate :: { cmp, fmt, hash, mem, num} ;
44
5+ #![ feature( contracts) ]
6+
57/// A type storing a `usize` which is a power of two, and thus
68/// represents a possible alignment in the Rust abstract machine.
79///
@@ -43,6 +45,8 @@ impl Alignment {
4345 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
4446 #[ inline]
4547 #[ must_use]
48+ #[ contracts:: requires( mem:: align_of:: <T >( ) . is_power_of_two( ) ) ]
49+ #[ contracts:: ensures( |result| 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,8 @@ 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+ #[ contracts:: ensures( |result| align. is_power_of_two( ) == result. is_some( ) ) ]
62+ #[ contracts:: ensures( |result| result. is_none( ) || result. unwrap( ) . as_usize( ) == align) ]
5763 pub const fn new ( align : usize ) -> Option < Self > {
5864 if align. is_power_of_two ( ) {
5965 // SAFETY: Just checked it only has one bit set
@@ -73,6 +79,9 @@ impl Alignment {
7379 /// It must *not* be zero.
7480 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
7581 #[ inline]
82+ #[ contracts:: requires( align > 0 && ( align & ( align - 1 ) ) == 0 ) ]
83+ #[ contracts:: ensures( |result| result. as_usize( ) == align) ]
84+ #[ contracts:: ensures( |result| result. as_usize( ) . is_power_of_two( ) ) ]
7685 pub const unsafe fn new_unchecked ( align : usize ) -> Self {
7786 assert_unsafe_precondition ! (
7887 check_language_ub,
@@ -88,13 +97,16 @@ impl Alignment {
8897 /// Returns the alignment as a [`usize`].
8998 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
9099 #[ inline]
100+ #[ contracts:: ensures( |result| result. is_power_of_two( ) ) ]
91101 pub const fn as_usize ( self ) -> usize {
92102 self . 0 as usize
93103 }
94104
95105 /// Returns the alignment as a <code>[NonZero]<[usize]></code>.
96106 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
97107 #[ inline]
108+ #[ contracts:: ensures( |result| result. get( ) . is_power_of_two( ) ) ]
109+ #[ contracts:: ensures( |result| result. get( ) == self . as_usize( ) ) ]
98110 pub const fn as_nonzero ( self ) -> NonZero < usize > {
99111 // This transmutes directly to avoid the UbCheck in `NonZero::new_unchecked`
100112 // since there's no way for the user to trip that check anyway -- the
@@ -120,6 +132,9 @@ impl Alignment {
120132 /// ```
121133 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
122134 #[ inline]
135+ #[ contracts:: requires( self . as_usize( ) . is_power_of_two( ) ) ]
136+ #[ contracts:: ensures( |result| ( * result as usize ) < mem:: size_of:: <usize >( ) * 8 ) ]
137+ #[ contracts:: ensures( |result| 1usize << * result == self . as_usize( ) ) ]
123138 pub const fn log2 ( self ) -> u32 {
124139 self . as_nonzero ( ) . trailing_zeros ( )
125140 }
@@ -149,6 +164,9 @@ impl Alignment {
149164 /// ```
150165 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
151166 #[ inline]
167+ #[ contracts:: ensures( |result| * result > 0 ) ]
168+ #[ contracts:: ensures( |result| * result == !( self . as_usize( ) -1 ) ) ]
169+ #[ contracts:: ensures( |result| self . as_usize( ) & * result == self . as_usize( ) ) ]
152170 pub const fn mask ( self ) -> usize {
153171 // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
154172 !( unsafe { self . as_usize ( ) . unchecked_sub ( 1 ) } )
0 commit comments