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,
108/// based 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/// `size_of_logic` for `repr(C)` types is not yet implemented.
117///
118/// See also [the Rust Reference section on Type Layout][RRTL].
119///
120/// Note that the value of `size_of`/`size_of_logic` may depend on the version of rustc, notably
121/// for ADTs with the default representation `repr(Rust)`.
122///
123/// [`size_of`]: https://doc.rust-lang.org/std/mem/fn.size_of.html
124/// [RRTL]: https://doc.rust-lang.org/stable/reference/type-layout.html
125#[trusted]
126#[logic(open, inline)]
127#[intrinsic("size_of_logic")]
128#[ensures(0 <= result)]
129pub fn size_of_logic<T>() -> Int {
130    dead
131}
132
133/// [`size_of_val`] as a logic `Int` value.
134#[trusted]
135#[logic(open, inline)]
136#[intrinsic("size_of_val_logic")]
137#[ensures(0 <= result)]
138pub fn size_of_val_logic<T: ?Sized>(val: T) -> Int {
139    dead
140}
141
142#[allow(unused)]
143#[logic]
144#[intrinsic("size_of_val_logic_sized")]
145fn size_of_val_logic_sized<T>(_val: T) -> Int {
146    size_of_logic::<T>()
147}
148
149#[allow(unused)]
150#[logic]
151#[intrinsic("size_of_val_logic_slice")]
152fn size_of_val_logic_slice<T>(val: [T]) -> Int {
153    pearlite! { size_of_logic::<T>() * val@.len() }
154}
155
156#[allow(unused)]
157#[logic]
158#[intrinsic("size_of_val_logic_str")]
159fn size_of_val_logic_str(val: str) -> Int {
160    pearlite! { val@.to_bytes().len() }
161}
162
163/// [`align_of`] as a logic `Int` value.
164///
165/// [`align_of`]: https://doc.rust-lang.org/std/mem/fn.align_of.html
166#[trusted]
167#[logic(open, inline)]
168#[intrinsic("align_of_logic")]
169#[ensures(0usize != result && result & (result - 1usize) == 0usize)]
170#[ensures(size_of_logic::<T>() % result@ == 0)]
171pub fn align_of_logic<T>() -> usize {
172    dead
173}
creusot_std/std/mem.rs

creusot_std/std/
mem.rs
