creusot_contracts/std/
mem.rs

1use crate::prelude::*;
2use std::mem::*;
3
4extern_spec! {
5    mod std {
6        mod mem {
7            #[check(ghost)]
8            #[ensures(^dest == src)]
9            #[ensures(result == *dest)]
10            fn replace<T>(dest: &mut T, src: T) -> T {
11                let mut src = src;
12                swap(dest, &mut src);
13                src
14            }
15
16            #[check(ghost)]
17            #[ensures(^x == *y)]
18            #[ensures(^y == *x)]
19            fn swap<T>(x: &mut T, y: &mut T);
20
21            #[ensures(result == *dest)]
22            #[ensures(T::default.postcondition((), ^dest))]
23            fn take<T: Default>(dest: &mut T) -> T {
24                replace(dest, T::default())
25            }
26
27            #[check(ghost)]
28            #[ensures(resolve(t))]
29            fn drop<T>(t: T) {}
30
31            #[check(ghost)]
32            #[ensures(resolve(t))]
33            fn forget<T>(t: T) {}
34
35            // This is not `#[check(ghost)]` because `size_of` overflows are only caught at codegen time
36            // which ghost code doesn't reach.
37            #[check(terminates)]
38            #[ensures(result@ == size_of_logic::<T>())]
39            fn size_of<T>() -> usize;
40
41            // This is not `#[check(ghost)]` because `size_of_val` overflows are only caught at codegen time
42            // which ghost code doesn't reach.
43            #[check(terminates)]
44            #[ensures(result@ == size_of_val_logic::<T>(*val))]
45            fn size_of_val<T: ?Sized>(val: &T) -> usize;
46
47            // This is not `#[check(ghost)]` because `align_of` overflows are only caught at codegen time
48            // which ghost code doesn't reach.
49            //
50            // Alignment values may range from 1 to 2^29
51            // ([source](https://doc.rust-lang.org/reference/type-layout.html#r-layout.repr.alignment.constraint-alignment)),
52            // which may overflow on 16-bit archs.
53            #[check(terminates)]
54            #[ensures(result == align_of_logic::<T>())]
55            fn align_of<T>() -> usize;
56        }
57    }
58}
59
60/// [`size_of`] as a logic `Int` value.
61///
62/// The definition of `size_of_logic` guarantees at least the following,
63/// based on the documentation of [`size_of`]:
64///
65/// - `()`, `bool`, `char`, primitive integers and floats are known constants.
66/// - For `T: Sized`, the pointer and reference types `*const T`, `*mut T`,
67///   `&T`, `&mut T`, `Box<T>`, `Option<&T>`, `Option<&mut T>`, and
68///   `Option<Box<T>>` have the same size as `usize`.
69/// - `[T; N]` has size `N * size_of_logic::<T>()`.
70///
71/// `size_of_logic` for `repr(C)` types is not yet implemented.
72///
73/// See also [the Rust Reference section on Type Layout][RRTL].
74///
75/// Note that the value of `size_of`/`size_of_logic` may depend on the version of rustc, notably
76/// for ADTs with the default representation `repr(Rust)`.
77///
78/// [`size_of`]: https://doc.rust-lang.org/std/mem/fn.size_of.html
79/// [RRTL]: https://doc.rust-lang.org/stable/reference/type-layout.html
80#[trusted]
81#[logic(open, inline)]
82#[intrinsic("size_of_logic")]
83#[ensures(0 <= result)]
84pub fn size_of_logic<T>() -> Int {
85    dead
86}
87
88/// [`size_of_val`] as a logic `Int` value.
89#[trusted]
90#[logic(open, inline)]
91#[intrinsic("size_of_val_logic")]
92#[ensures(0 <= result)]
93pub fn size_of_val_logic<T: ?Sized>(val: T) -> Int {
94    dead
95}
96
97#[allow(unused)]
98#[logic]
99#[intrinsic("size_of_val_logic_sized")]
100fn size_of_val_logic_sized<T>(_val: T) -> Int {
101    size_of_logic::<T>()
102}
103
104#[allow(unused)]
105#[logic]
106#[intrinsic("size_of_val_logic_slice")]
107fn size_of_val_logic_slice<T>(val: [T]) -> Int {
108    pearlite! { size_of_logic::<T>() * val@.len() }
109}
110
111#[allow(unused)]
112#[logic]
113#[intrinsic("size_of_val_logic_str")]
114fn size_of_val_logic_str(val: str) -> Int {
115    pearlite! { val@.to_bytes().len() }
116}
117
118/// [`align_of`] as a logic `Int` value.
119///
120/// [`align_of`]: https://doc.rust-lang.org/std/mem/fn.align_of.html
121#[trusted]
122#[logic(open, inline)]
123#[intrinsic("align_of_logic")]
124#[ensures(0usize != result && result & (result - 1usize) == 0usize)]
125#[ensures(size_of_logic::<T>() % result@ == 0)]
126pub fn align_of_logic<T>() -> usize {
127    dead
128}
creusot_contracts/std/mem.rs

creusot_contracts/std/
mem.rs
