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

creusot_std/std/
mem.rs
