creusot_contracts/std/
ptr.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use crate::std::mem::{align_of_logic, size_of_logic};
4use std::ptr::*;
5
6/// Metadata of a pointer in logic.
7///
8/// [`std::ptr::metadata`] in logic.
9#[logic(opaque)]
10pub fn metadata_logic<T: ?Sized>(_: *const T) -> <T as Pointee>::Metadata {
11    dead
12}
13
14/// Check that a value is compatible with some metadata.
15///
16/// If the value is a slice, this predicate asserts that the metadata equals the length of the slice,
17/// and that the total size of the slice is no more than `isize::MAX`. This latter property is assumed
18/// by pointer primitives such as [`slice::from_raw_parts`][from_raw_parts].
19///
20/// - For `T = [U]`, specializes to [`metadata_matches_slice`].
21/// - For `T = str`, specializes to [`metadata_matches_str`].
22/// - For `T: Sized`, specializes to `true`.
23///
24/// Why did we not make this a function `fn metadata_of(value: T) -> <T as Pointee>::Metadata`?
25/// Because this way is shorter: this corresponds to a single predicate in Why3 per type `T`.
26/// Defining a logic function that returns `usize` for slices is not so
27/// straightforward because almost every number wants to be `Int`.
28/// We would need to generate one abstract Why3 function `metadata_of : T -> Metadata`
29/// and an axiom `view_usize (metadata_of value) = len (Slice.view value)`,
30/// so two Why3 declarations instead of one.
31///
32/// [from_raw_parts]: https://doc.rust-lang.org/core/slice/fn.from_raw_parts.html
33#[logic(open, inline)]
34#[intrinsic("metadata_matches")]
35pub fn metadata_matches<T: ?Sized>(_value: T, _metadata: <T as Pointee>::Metadata) -> bool {
36    dead
37}
38
39/// Definition of [`metadata_matches`] for slices.
40#[allow(unused)]
41#[logic]
42#[intrinsic("metadata_matches_slice")]
43fn metadata_matches_slice<T>(value: [T], len: usize) -> bool {
44    pearlite! { value@.len() == len@ }
45}
46
47/// Definition of [`metadata_matches`] for string slices.
48#[allow(unused)]
49#[logic]
50#[intrinsic("metadata_matches_str")]
51fn metadata_matches_str(value: str, len: usize) -> bool {
52    pearlite! { value@.to_bytes().len() == len@ }
53}
54
55/// Whether a pointer is aligned.
56///
57/// This is a logic version of [`<*const T>::is_aligned`][is_aligned],
58/// but extended with an additional rule for `[U]`. We make use of this property
59/// in [`ghost::PtrOwn`] to define a more precise invariant for slice pointers.
60///
61/// - For `T: Sized`, specializes to [`is_aligned_logic_sized`].
62/// - For `T = [U]`, specializes to [`is_aligned_logic_slice`].
63/// - For `T = str`, specializes to `true`.
64///
65/// [is_aligned]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned
66#[allow(unused_variables)]
67#[logic(open, inline)]
68#[intrinsic("is_aligned_logic")]
69pub fn is_aligned_logic<T: ?Sized>(ptr: *const T) -> bool {
70    dead
71}
72
73/// Definition of [`is_aligned_logic`] for `T: Sized`.
74#[allow(unused)]
75#[logic]
76#[intrinsic("is_aligned_logic_sized")]
77fn is_aligned_logic_sized<T>(ptr: *const T) -> bool {
78    ptr.is_aligned_to_logic(align_of_logic::<T>())
79}
80
81/// Definition of [`is_aligned_logic`] for `[T]`.
82#[allow(unused)]
83#[logic]
84#[intrinsic("is_aligned_logic_slice")]
85fn is_aligned_logic_slice<T>(ptr: *const [T]) -> bool {
86    ptr.is_aligned_to_logic(align_of_logic::<T>())
87}
88
89/// We conservatively model raw pointers as having an address *plus some hidden
90/// metadata*.
91///
92/// This is to account for provenance
93/// (<https://doc.rust-lang.org/std/ptr/index.html#[check(ghost)]sing-strict-provenance>) and
94/// wide pointers. See e.g.
95/// <https://doc.rust-lang.org/std/primitive.pointer.html#method.is_null>: "unsized
96/// types have many possible null pointers, as only the raw data pointer is
97/// considered, not their length, vtable, etc. Therefore, two pointers that are
98/// null may still not compare equal to each other."
99#[allow(dead_code)]
100pub struct PtrDeepModel {
101    pub addr: usize,
102    runtime_metadata: usize,
103}
104
105impl<T: ?Sized> DeepModel for *mut T {
106    type DeepModelTy = PtrDeepModel;
107    #[trusted]
108    #[logic(opaque)]
109    #[ensures(result.addr == self.addr_logic())]
110    fn deep_model(self) -> Self::DeepModelTy {
111        dead
112    }
113}
114
115impl<T: ?Sized> DeepModel for *const T {
116    type DeepModelTy = PtrDeepModel;
117    #[trusted]
118    #[logic(opaque)]
119    #[ensures(result.addr == self.addr_logic())]
120    fn deep_model(self) -> Self::DeepModelTy {
121        dead
122    }
123}
124
125pub trait PointerExt<T: ?Sized>: Sized {
126    /// _logical_ address of the pointer
127    #[logic]
128    fn addr_logic(self) -> usize;
129
130    /// `true` if the pointer is null.
131    #[logic(open, sealed)]
132    fn is_null_logic(self) -> bool {
133        self.addr_logic() == 0usize
134    }
135
136    /// Logic counterpart to [`<*const T>::is_aligned_to`][is_aligned_to]
137    ///
138    /// [is_aligned_to]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned_to
139    #[logic(open, sealed)]
140    fn is_aligned_to_logic(self, align: usize) -> bool {
141        pearlite! { self.addr_logic() & (align - 1usize) == 0usize }
142    }
143
144    /// Logic counterpart to [`<*const T>::is_aligned`][is_aligned]
145    ///
146    /// This is defined as [`is_aligned_logic`] (plus a noop coercion for `*mut T`).
147    ///
148    /// [is_aligned]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned
149    #[logic]
150    fn is_aligned_logic(self) -> bool;
151}
152
153impl<T: ?Sized> PointerExt<T> for *const T {
154    #[logic]
155    #[cfg_attr(target_pointer_width = "16", builtin("creusot.prelude.Ptr$BW$.addr_logic_u16"))]
156    #[cfg_attr(target_pointer_width = "32", builtin("creusot.prelude.Ptr$BW$.addr_logic_u32"))]
157    #[cfg_attr(target_pointer_width = "64", builtin("creusot.prelude.Ptr$BW$.addr_logic_u64"))]
158    fn addr_logic(self) -> usize {
159        dead
160    }
161
162    #[logic(open, inline)]
163    fn is_aligned_logic(self) -> bool {
164        is_aligned_logic(self)
165    }
166}
167
168impl<T: ?Sized> PointerExt<T> for *mut T {
169    #[logic]
170    #[cfg_attr(target_pointer_width = "16", builtin("creusot.prelude.Ptr$BW$.addr_logic_u16"))]
171    #[cfg_attr(target_pointer_width = "32", builtin("creusot.prelude.Ptr$BW$.addr_logic_u32"))]
172    #[cfg_attr(target_pointer_width = "64", builtin("creusot.prelude.Ptr$BW$.addr_logic_u64"))]
173    fn addr_logic(self) -> usize {
174        dead
175    }
176
177    #[logic(open, inline)]
178    fn is_aligned_logic(self) -> bool {
179        is_aligned_logic(self)
180    }
181}
182
183/// Extension methods for `*const T` where `T: Sized`.
184pub trait SizedPointerExt<T>: PointerExt<T> {
185    /// Pointer offset in logic
186    ///
187    /// The current contract only describes the effect on `addr_logic` in the absence of overflow.
188    #[logic]
189    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@)]
190    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
191    fn offset_logic(self, offset: Int) -> Self;
192
193    /// Offset by zero is the identity
194    #[logic(law)]
195    #[ensures(self.offset_logic(0) == self)]
196    fn offset_logic_zero(self);
197
198    /// Offset is associative
199    #[logic(law)]
200    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
201    fn offset_logic_assoc(self, offset1: Int, offset2: Int);
202
203    /// Pointer subtraction
204    ///
205    /// Note: we don't have `ptr1 + (ptr2 - ptr1) == ptr2`, because pointer subtraction discards provenance.
206    #[logic]
207    fn sub_logic(self, rhs: Self) -> Int;
208
209    #[logic(law)]
210    #[ensures(self.sub_logic(self) == 0)]
211    fn sub_logic_refl(self);
212
213    #[logic(law)]
214    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
215    fn sub_offset_logic(self, offset: Int);
216}
217
218impl<T> SizedPointerExt<T> for *const T {
219    #[trusted]
220    #[logic(opaque)]
221    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@)]
222    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
223    fn offset_logic(self, offset: Int) -> Self {
224        dead
225    }
226
227    #[trusted]
228    #[logic(law)]
229    #[ensures(self.offset_logic(0) == self)]
230    fn offset_logic_zero(self) {}
231
232    #[trusted]
233    #[logic(law)]
234    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
235    fn offset_logic_assoc(self, offset1: Int, offset2: Int) {}
236
237    #[allow(unused)]
238    #[trusted]
239    #[logic(opaque)]
240    fn sub_logic(self, rhs: Self) -> Int {
241        dead
242    }
243
244    #[trusted]
245    #[logic(law)]
246    #[ensures(self.sub_logic(self) == 0)]
247    fn sub_logic_refl(self) {}
248
249    #[trusted]
250    #[logic(law)]
251    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
252    fn sub_offset_logic(self, offset: Int) {}
253}
254
255/// Extension methods for `*const [T]`
256///
257/// `thin` and `len_logic` are wrappers around `_ as *const T` and `metadata_logic`
258/// that also pull in the `slice_ptr_ext` axiom when used.
259pub trait SlicePointerExt<T>: PointerExt<[T]> {
260    /// Remove metadata.
261    #[logic]
262    fn thin(self) -> *const T;
263
264    /// Get the metadata.
265    #[logic]
266    fn len_logic(self) -> usize;
267
268    /// Extensionality law.
269    #[logic(law)]
270    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
271    fn slice_ptr_ext(self, other: Self);
272}
273
274impl<T> SlicePointerExt<T> for *const [T] {
275    /// Convert `*const [T]` to `*const T`.
276    #[logic(open, inline)]
277    fn thin(self) -> *const T {
278        self as *const T
279    }
280
281    /// Get the length metadata of the pointer.
282    #[logic(open, inline)]
283    fn len_logic(self) -> usize {
284        pearlite! { metadata_logic(self) }
285    }
286
287    /// Extensionality of slice pointers.
288    #[trusted]
289    #[logic(law)]
290    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
291    fn slice_ptr_ext(self, other: Self) {}
292}
293
294extern_spec! {
295    impl<T: ?Sized> *const T {
296        #[check(ghost)]
297        #[ensures(result == self.addr_logic())]
298        fn addr(self) -> usize;
299
300        #[check(ghost)]
301        #[ensures(result == self.is_null_logic())]
302        fn is_null(self) -> bool;
303
304        #[check(ghost)]
305        #[erasure]
306        #[ensures(result == self as _)]
307        fn cast<U>(self) -> *const U {
308            self as _
309        }
310
311        #[check(terminates)]
312        #[erasure]
313        #[ensures(result == self.is_aligned_logic())]
314        fn is_aligned(self) -> bool
315            where T: Sized,
316        {
317            self.is_aligned_to(std::mem::align_of::<T>())
318        }
319
320        #[check(ghost)]
321        #[erasure]
322        #[bitwise_proof]
323        #[requires(align != 0usize && align & (align - 1usize) == 0usize)]
324        #[ensures(result == self.is_aligned_to_logic(align))]
325        fn is_aligned_to(self, align: usize) -> bool
326        {
327            if !align.is_power_of_two() {
328                ::core::panic::panic_2021!("is_aligned_to: align is not a power-of-two");
329            }
330            self.addr() & (align - 1) == 0
331        }
332    }
333
334    impl<T: ?Sized> *mut T {
335        #[check(ghost)]
336        #[ensures(result == self.addr_logic())]
337        fn addr(self) -> usize;
338
339        #[check(ghost)]
340        #[ensures(result == self.is_null_logic())]
341        fn is_null(self) -> bool;
342
343        #[check(ghost)]
344        #[erasure]
345        #[ensures(result == self as _)]
346        fn cast<U>(self) -> *mut U {
347            self as _
348        }
349
350        #[check(terminates)]
351        #[erasure]
352        #[ensures(result == self.is_aligned_logic())]
353        fn is_aligned(self) -> bool
354            where T: Sized,
355        {
356            self.is_aligned_to(std::mem::align_of::<T>())
357        }
358
359        #[check(ghost)]
360        #[erasure]
361        #[bitwise_proof]
362        #[requires(align != 0usize && align & (align - 1usize) == 0usize)]
363        #[ensures(result == self.is_aligned_to_logic(align))]
364        fn is_aligned_to(self, align: usize) -> bool
365        {
366            if !align.is_power_of_two() {
367                ::core::panic::panic_2021!("is_aligned_to: align is not a power-of-two");
368            }
369            self.addr() & (align - 1) == 0
370        }
371    }
372
373    impl<T> *const [T] {
374        #[ensures(result == metadata_logic(self))]
375        fn len(self) -> usize;
376    }
377
378    impl<T> *mut [T] {
379        #[ensures(result == metadata_logic(self))]
380        fn len(self) -> usize;
381    }
382
383    mod std {
384        mod ptr {
385            #[check(ghost)]
386            #[ensures(result.is_null_logic())]
387            fn null<T>() -> *const T
388            where
389                T: std::ptr::Thin + ?Sized;
390
391            #[check(ghost)]
392            #[ensures(result.is_null_logic())]
393            fn null_mut<T>() -> *mut T
394            where
395                T: std::ptr::Thin + ?Sized;
396
397            #[check(ghost)]
398            #[ensures(result == (p.addr_logic() == q.addr_logic()))]
399            fn addr_eq<T, U>(p: *const T, q: *const U) -> bool
400            where
401                T: ?Sized, U: ?Sized;
402
403            #[check(ghost)]
404            #[ensures(result == metadata_logic(ptr))]
405            fn metadata<T: ?Sized>(ptr: *const T) -> <T as Pointee>::Metadata;
406
407            // Postulate `check(ghost)`.
408            // It is used in a `#[trusted]` primitive in `peano`.
409            #[check(ghost)]
410            #[ensures(false)]
411            unsafe fn read_volatile<T>(src: *const T) -> T;
412
413            #[ensures(result as *const T == data && result.len_logic() == len)]
414            fn slice_from_raw_parts<T>(data: *const T, len: usize) -> *const [T];
415
416            #[ensures(result as *mut T == data && result.len_logic() == len)]
417            fn slice_from_raw_parts_mut<T>(data: *mut T, len: usize) -> *mut [T];
418        }
419    }
420
421    impl<T> Clone for *mut T {
422        #[check(ghost)]
423        #[ensures(result == *self)]
424        fn clone(&self) -> *mut T {
425            *self
426        }
427    }
428
429    impl<T> Clone for *const T {
430        #[check(ghost)]
431        #[ensures(result == *self)]
432        fn clone(&self) -> *const T {
433            *self
434        }
435    }
436}
creusot_contracts/std/ptr.rs

creusot_contracts/std/
ptr.rs
