@@ -2,6 +2,8 @@ use crate::num::NonZero;
2
2
use crate :: ub_checks:: assert_unsafe_precondition;
3
3
use crate :: { cmp, fmt, hash, mem, num} ;
4
4
5
+ #![ feature( contracts) ]
6
+
5
7
/// A type storing a `usize` which is a power of two, and thus
6
8
/// represents a possible alignment in the Rust abstract machine.
7
9
///
@@ -43,6 +45,8 @@ impl Alignment {
43
45
#[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
44
46
#[ inline]
45
47
#[ must_use]
48
+ #[ contracts:: requires( mem:: align_of:: <T >( ) . is_power_of_two( ) ) ]
49
+ #[ contracts:: ensures( |result| result. as_usize( ) . is_power_of_two( ) ) ]
46
50
pub const fn of < T > ( ) -> Self {
47
51
// This can't actually panic since type alignment is always a power of two.
48
52
const { Alignment :: new ( mem:: align_of :: < T > ( ) ) . unwrap ( ) }
@@ -54,6 +58,8 @@ impl Alignment {
54
58
/// Note that `0` is not a power of two, nor a valid alignment.
55
59
#[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
56
60
#[ 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) ]
57
63
pub const fn new ( align : usize ) -> Option < Self > {
58
64
if align. is_power_of_two ( ) {
59
65
// SAFETY: Just checked it only has one bit set
@@ -73,6 +79,9 @@ impl Alignment {
73
79
/// It must *not* be zero.
74
80
#[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
75
81
#[ 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( ) ) ]
76
85
pub const unsafe fn new_unchecked ( align : usize ) -> Self {
77
86
assert_unsafe_precondition ! (
78
87
check_language_ub,
@@ -88,13 +97,16 @@ impl Alignment {
88
97
/// Returns the alignment as a [`usize`].
89
98
#[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
90
99
#[ inline]
100
+ #[ contracts:: ensures( |result| result. is_power_of_two( ) ) ]
91
101
pub const fn as_usize ( self ) -> usize {
92
102
self . 0 as usize
93
103
}
94
104
95
105
/// Returns the alignment as a <code>[NonZero]<[usize]></code>.
96
106
#[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
97
107
#[ inline]
108
+ #[ contracts:: ensures( |result| result. get( ) . is_power_of_two( ) ) ]
109
+ #[ contracts:: ensures( |result| result. get( ) == self . as_usize( ) ) ]
98
110
pub const fn as_nonzero ( self ) -> NonZero < usize > {
99
111
// This transmutes directly to avoid the UbCheck in `NonZero::new_unchecked`
100
112
// since there's no way for the user to trip that check anyway -- the
@@ -120,6 +132,9 @@ impl Alignment {
120
132
/// ```
121
133
#[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
122
134
#[ 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( ) ) ]
123
138
pub const fn log2 ( self ) -> u32 {
124
139
self . as_nonzero ( ) . trailing_zeros ( )
125
140
}
@@ -149,6 +164,9 @@ impl Alignment {
149
164
/// ```
150
165
#[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
151
166
#[ 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( ) ) ]
152
170
pub const fn mask ( self ) -> usize {
153
171
// SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
154
172
!( unsafe { self . as_usize ( ) . unchecked_sub ( 1 ) } )
0 commit comments