creusot_std/std/
mem.rs

1use crate::prelude::*;
2use core::mem::*;
3
4impl<T> View for MaybeUninit<T> {
5    type ViewTy = Option<T>;
6
7    #[logic(opaque)]
8    fn view(self) -> Option<T> {
9        dead
10    }
11}
12
13extern_spec! {
14    mod core {
15        mod mem {
16            #[check(ghost)]
17            #[ensures(^dest == src)]
18            #[ensures(result == *dest)]
19            fn replace<T>(dest: &mut T, src: T) -> T {
20                let mut src = src;
21                swap(dest, &mut src);
22                src
23            }
24
25            #[check(ghost)]
26            #[ensures(^x == *y)]
27            #[ensures(^y == *x)]
28            fn swap<T>(x: &mut T, y: &mut T);
29
30            #[ensures(result == *dest)]
31            #[ensures(T::default.postcondition((), ^dest))]
32            fn take<T: Default>(dest: &mut T) -> T {
33                replace(dest, T::default())
34            }
35
36            #[check(ghost)]
37            #[ensures(resolve(t))]
38            fn drop<T>(t: T) {}
39
40            #[check(ghost)]
41            #[ensures(resolve(t))]
42            fn forget<T>(t: T) {}
43
44            // This is not `#[check(ghost)]` because `size_of` overflows are only caught at codegen time
45            // which ghost code doesn't reach.
46            #[check(terminates)]
47            #[ensures(result@ == size_of_logic::<T>())]
48            fn size_of<T>() -> usize;
49
50            // This is not `#[check(ghost)]` because `size_of_val` overflows are only caught at codegen time
51            // which ghost code doesn't reach.
52            #[check(terminates)]
53            #[ensures(result@ == size_of_val_logic::<T>(*val))]
54            fn size_of_val<T: ?Sized>(val: &T) -> usize;
55
56            // This is not `#[check(ghost)]` because `align_of` overflows are only caught at codegen time
57            // which ghost code doesn't reach.
58            //
59            // Alignment values may range from 1 to 2^29
60            // ([source](https://doc.rust-lang.org/reference/type-layout.html#r-layout.repr.alignment.constraint-alignment)),
61            // which may overflow on 16-bit archs.
62            #[check(terminates)]
63            #[ensures(result == align_of_logic::<T>())]
64            fn align_of<T>() -> usize;
65        }
66    }
67
68    impl<T> MaybeUninit<T> {
69        #[ensures(result@ == Some(val))]
70        #[check(ghost)]
71        fn new(val: T) -> Self;
72
73        #[ensures(result@ == None)]
74        #[check(ghost)]
75        fn uninit() -> Self;
76
77        #[requires(self@ == None)] // NOTE: we could allow calling this on an initialized `MaybeUninit`, but this would leak the contents.
78        #[ensures(*result == val)]
79        #[ensures((^self)@ == Some(^result))]
80        #[check(ghost)]
81        fn write(&mut self, val: T) -> &mut T;
82
83        #[requires(self@ != None)]
84        #[ensures(self@ == Some(result))]
85        #[check(ghost)]
86        const unsafe fn assume_init(self) -> T;
87
88        #[requires(self@ != None)]
89        #[ensures((^self)@ == None)]
90        #[check(ghost)]
91        unsafe fn assume_init_drop(&mut self);
92
93        #[requires(self@ != None)]
94        #[ensures(self@ == Some(*result))]
95        #[check(ghost)]
96        const unsafe fn assume_init_ref(&self) -> &T;
97
98        #[requires(self@ != None)]
99        #[ensures((*self)@ == Some(*result) && (^self)@ == Some(^result))]
100        #[check(ghost)]
101        const unsafe fn assume_init_mut(&mut self) -> &mut T;
102    }
103}
104
105/// [`size_of`] as a logic `Int` value.
106///
107/// The definition of `size_of_logic` guarantees at least the following, based
108/// on the documentation of [`size_of`]:
109///
110/// - `()`, `bool`, `char`, primitive integers and floats are known constants.
111/// - For `T: Sized`, the pointer and reference types `*const T`, `*mut T`,
112///   `&T`, `&mut T`, `Box<T>`, `Option<&T>`, `Option<&mut T>`, and
113///   `Option<Box<T>>` have the same size as `usize`.
114/// - `[T; N]` has size `N * size_of_logic::<T>()`.
115///
116/// See also [the Rust Reference section on Type Layout][RRTL].
117///
118/// # Stability of `size_of_logic`
119///
120/// Note that the size of `usize`, references, pointers… is platform-dependent:
121/// if you want to verify your code against a specific architecture, you need to
122/// use Creusot with the exact same architecture.
123///
124/// Additionally, for `repr(Rust)` types, the value of `size_of`/`size_of_logic`
125/// is not guaranteed to stay the same across compilations.
126///
127/// [`size_of`]: https://doc.rust-lang.org/std/mem/fn.size_of.html
128/// [RRTL]: https://doc.rust-lang.org/stable/reference/type-layout.html
129#[trusted]
130#[logic(open, inline)]
131#[intrinsic("size_of_logic")]
132#[ensures(0 <= result)]
133pub fn size_of_logic<T>() -> Int {
134    dead
135}
136
137/// [`size_of_val`] as a logic `Int` value.
138#[trusted]
139#[logic(open, inline)]
140#[intrinsic("size_of_val_logic")]
141#[ensures(0 <= result)]
142pub fn size_of_val_logic<T: ?Sized>(val: T) -> Int {
143    dead
144}
145
146#[allow(unused)]
147#[logic]
148#[intrinsic("size_of_val_logic_sized")]
149fn size_of_val_logic_sized<T>(_val: T) -> Int {
150    size_of_logic::<T>()
151}
152
153#[allow(unused)]
154#[logic]
155#[intrinsic("size_of_val_logic_slice")]
156fn size_of_val_logic_slice<T>(val: [T]) -> Int {
157    pearlite! { size_of_logic::<T>() * val@.len() }
158}
159
160#[allow(unused)]
161#[logic]
162#[intrinsic("size_of_val_logic_str")]
163fn size_of_val_logic_str(val: str) -> Int {
164    pearlite! { val@.to_bytes().len() }
165}
166
167/// [`align_of`] as a logic `Int` value.
168///
169/// [`align_of`]: https://doc.rust-lang.org/std/mem/fn.align_of.html
170#[trusted]
171#[logic(open, inline)]
172#[intrinsic("align_of_logic")]
173#[ensures(0usize != result && result & (result - 1usize) == 0usize)]
174#[ensures(size_of_logic::<T>() % result@ == 0)]
175pub fn align_of_logic<T>() -> usize {
176    dead
177}
creusot_std/std/mem.rs

creusot_std/std/
mem.rs
