creusot_std/std/
ptr.rs

1#[cfg(creusot)]
2use crate::std::mem::{align_of_logic, size_of_logic, size_of_val_logic};
3use crate::{
4    ghost::perm::{Container, Perm},
5    prelude::*,
6};
7#[cfg(creusot)]
8use core::ptr::Pointee;
9
10#[cfg(not(feature = "std"))]
11use alloc::boxed::Box;
12
13/// Metadata of a pointer in logic.
14///
15/// [`std::ptr::metadata`] in logic.
16#[logic(opaque)]
17pub fn metadata_logic<T: ?Sized>(_: *const T) -> <T as Pointee>::Metadata {
18    dead
19}
20
21/// Check that a value is compatible with some metadata.
22///
23/// If the value is a slice, this predicate asserts that the metadata equals the length of the slice,
24/// and that the total size of the slice is no more than `isize::MAX`. This latter property is assumed
25/// by pointer primitives such as [`slice::from_raw_parts`][from_raw_parts].
26///
27/// - For `T = [U]`, specializes to [`metadata_matches_slice`].
28/// - For `T = str`, specializes to [`metadata_matches_str`].
29/// - For `T: Sized`, specializes to `true`.
30///
31/// Why did we not make this a function `fn metadata_of(value: T) -> <T as Pointee>::Metadata`?
32/// Because this way is shorter: this corresponds to a single predicate in Why3 per type `T`.
33/// Defining a logic function that returns `usize` for slices is not so
34/// straightforward because almost every number wants to be `Int`.
35/// We would need to generate one abstract Why3 function `metadata_of : T -> Metadata`
36/// and an axiom `view_usize (metadata_of value) = len (Slice.view value)`,
37/// so two Why3 declarations instead of one.
38///
39/// [from_raw_parts]: https://doc.rust-lang.org/core/slice/fn.from_raw_parts.html
40#[logic(open, inline)]
41#[intrinsic("metadata_matches")]
42pub fn metadata_matches<T: ?Sized>(_value: T, _metadata: <T as Pointee>::Metadata) -> bool {
43    dead
44}
45
46/// Definition of [`metadata_matches`] for slices.
47#[allow(unused)]
48#[logic]
49#[intrinsic("metadata_matches_slice")]
50fn metadata_matches_slice<T>(value: [T], len: usize) -> bool {
51    pearlite! { value@.len() == len@ }
52}
53
54/// Definition of [`metadata_matches`] for string slices.
55#[allow(unused)]
56#[logic]
57#[intrinsic("metadata_matches_str")]
58fn metadata_matches_str(value: str, len: usize) -> bool {
59    pearlite! { value@.to_bytes().len() == len@ }
60}
61
62/// Whether a pointer is aligned.
63///
64/// This is a logic version of [`<*const T>::is_aligned`][is_aligned],
65/// but extended with an additional rule for `[U]`. We make use of this property
66/// in [`ghost::perm::Perm<*const T>`] to define a more precise invariant for slice pointers.
67///
68/// - For `T: Sized`, specializes to [`is_aligned_logic_sized`].
69/// - For `T = [U]`, specializes to [`is_aligned_logic_slice`].
70/// - For `T = str`, specializes to `true`.
71///
72/// [is_aligned]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned
73#[allow(unused_variables)]
74#[logic(open, inline)]
75#[intrinsic("is_aligned_logic")]
76pub fn is_aligned_logic<T: ?Sized>(ptr: *const T) -> bool {
77    dead
78}
79
80/// Definition of [`is_aligned_logic`] for `T: Sized`.
81#[allow(unused)]
82#[logic]
83#[intrinsic("is_aligned_logic_sized")]
84fn is_aligned_logic_sized<T>(ptr: *const T) -> bool {
85    ptr.is_aligned_to_logic(align_of_logic::<T>())
86}
87
88/// Definition of [`is_aligned_logic`] for `[T]`.
89#[allow(unused)]
90#[logic]
91#[intrinsic("is_aligned_logic_slice")]
92fn is_aligned_logic_slice<T>(ptr: *const [T]) -> bool {
93    ptr.is_aligned_to_logic(align_of_logic::<T>())
94}
95
96/// We conservatively model raw pointers as having an address *plus some hidden
97/// metadata*.
98///
99/// This is to account for provenance
100/// (<https://doc.rust-lang.org/std/ptr/index.html#[check(ghost)]sing-strict-provenance>) and
101/// wide pointers. See e.g.
102/// <https://doc.rust-lang.org/std/primitive.pointer.html#method.is_null>: "unsized
103/// types have many possible null pointers, as only the raw data pointer is
104/// considered, not their length, vtable, etc. Therefore, two pointers that are
105/// null may still not compare equal to each other."
106#[allow(dead_code)]
107pub struct PtrDeepModel {
108    pub addr: usize,
109    runtime_metadata: usize,
110}
111
112impl<T: ?Sized> DeepModel for *mut T {
113    type DeepModelTy = PtrDeepModel;
114    #[trusted]
115    #[logic(opaque)]
116    #[ensures(result.addr == self.addr_logic())]
117    fn deep_model(self) -> Self::DeepModelTy {
118        dead
119    }
120}
121
122impl<T: ?Sized> DeepModel for *const T {
123    type DeepModelTy = PtrDeepModel;
124    #[trusted]
125    #[logic(opaque)]
126    #[ensures(result.addr == self.addr_logic())]
127    fn deep_model(self) -> Self::DeepModelTy {
128        dead
129    }
130}
131
132/// Extension trait for pointers
133pub trait PointerExt<T: ?Sized>: Sized {
134    /// _logical_ address of the pointer
135    #[logic]
136    fn addr_logic(self) -> usize;
137
138    /// `true` if the pointer is null.
139    #[logic(open, sealed)]
140    fn is_null_logic(self) -> bool {
141        self.addr_logic() == 0usize
142    }
143
144    /// Logic counterpart to [`<*const T>::is_aligned_to`][is_aligned_to]
145    ///
146    /// [is_aligned_to]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned_to
147    #[logic(open, sealed)]
148    fn is_aligned_to_logic(self, align: usize) -> bool {
149        pearlite! { self.addr_logic() & (align - 1usize) == 0usize }
150    }
151
152    /// Logic counterpart to [`<*const T>::is_aligned`][is_aligned]
153    ///
154    /// This is defined as [`is_aligned_logic`] (plus a noop coercion for `*mut T`).
155    ///
156    /// [is_aligned]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned
157    #[logic]
158    fn is_aligned_logic(self) -> bool;
159}
160
161impl<T: ?Sized> PointerExt<T> for *const T {
162    #[logic]
163    #[cfg_attr(target_pointer_width = "16", builtin("creusot.prelude.Ptr$BW$.addr_logic_u16"))]
164    #[cfg_attr(target_pointer_width = "32", builtin("creusot.prelude.Ptr$BW$.addr_logic_u32"))]
165    #[cfg_attr(target_pointer_width = "64", builtin("creusot.prelude.Ptr$BW$.addr_logic_u64"))]
166    fn addr_logic(self) -> usize {
167        dead
168    }
169
170    #[logic(open, inline)]
171    fn is_aligned_logic(self) -> bool {
172        is_aligned_logic(self)
173    }
174}
175
176impl<T: ?Sized> PointerExt<T> for *mut T {
177    #[logic]
178    #[cfg_attr(target_pointer_width = "16", builtin("creusot.prelude.Ptr$BW$.addr_logic_u16"))]
179    #[cfg_attr(target_pointer_width = "32", builtin("creusot.prelude.Ptr$BW$.addr_logic_u32"))]
180    #[cfg_attr(target_pointer_width = "64", builtin("creusot.prelude.Ptr$BW$.addr_logic_u64"))]
181    fn addr_logic(self) -> usize {
182        dead
183    }
184
185    #[logic(open, inline)]
186    fn is_aligned_logic(self) -> bool {
187        is_aligned_logic(self)
188    }
189}
190
191/// Extension methods for `*const T` where `T: Sized`.
192pub trait SizedPointerExt<T>: PointerExt<T> {
193    /// Pointer offset in logic
194    ///
195    /// The current contract only describes the effect on `addr_logic` in the absence of overflow.
196    #[logic]
197    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@)]
198    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
199    fn offset_logic(self, offset: Int) -> Self;
200
201    /// Offset by zero is the identity
202    #[logic(law)]
203    #[ensures(self.offset_logic(0) == self)]
204    fn offset_logic_zero(self);
205
206    /// Offset is associative
207    #[logic(law)]
208    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
209    fn offset_logic_assoc(self, offset1: Int, offset2: Int);
210
211    /// Pointer subtraction
212    ///
213    /// Note: we don't have `ptr1 + (ptr2 - ptr1) == ptr2`, because pointer subtraction discards provenance.
214    #[logic]
215    fn sub_logic(self, rhs: Self) -> Int;
216
217    #[logic(law)]
218    #[ensures(self.sub_logic(self) == 0)]
219    fn sub_logic_refl(self);
220
221    #[logic(law)]
222    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
223    fn sub_offset_logic(self, offset: Int);
224}
225
226impl<T> SizedPointerExt<T> for *const T {
227    #[trusted]
228    #[logic(opaque)]
229    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@)]
230    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
231    fn offset_logic(self, offset: Int) -> Self {
232        dead
233    }
234
235    #[trusted]
236    #[logic(law)]
237    #[ensures(self.offset_logic(0) == self)]
238    fn offset_logic_zero(self) {}
239
240    #[trusted]
241    #[logic(law)]
242    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
243    fn offset_logic_assoc(self, offset1: Int, offset2: Int) {}
244
245    #[allow(unused)]
246    #[trusted]
247    #[logic(opaque)]
248    fn sub_logic(self, rhs: Self) -> Int {
249        dead
250    }
251
252    #[trusted]
253    #[logic(law)]
254    #[ensures(self.sub_logic(self) == 0)]
255    fn sub_logic_refl(self) {}
256
257    #[trusted]
258    #[logic(law)]
259    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
260    fn sub_offset_logic(self, offset: Int) {}
261}
262
263/// Extension methods for `*const [T]`
264///
265/// `thin` and `len_logic` are wrappers around `_ as *const T` and `metadata_logic`
266/// that also pull in the `slice_ptr_ext` axiom when used.
267pub trait SlicePointerExt<T>: PointerExt<[T]> {
268    /// Remove metadata.
269    #[logic]
270    fn thin(self) -> *const T;
271
272    /// Get the metadata.
273    #[logic]
274    fn len_logic(self) -> usize;
275
276    /// Extensionality law.
277    #[logic(law)]
278    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
279    fn slice_ptr_ext(self, other: Self);
280}
281
282impl<T> SlicePointerExt<T> for *const [T] {
283    /// Convert `*const [T]` to `*const T`.
284    #[logic(open, inline)]
285    fn thin(self) -> *const T {
286        self as *const T
287    }
288
289    /// Get the length metadata of the pointer.
290    #[logic(open, inline)]
291    fn len_logic(self) -> usize {
292        pearlite! { metadata_logic(self) }
293    }
294
295    /// Extensionality of slice pointers.
296    #[trusted]
297    #[logic(law)]
298    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
299    fn slice_ptr_ext(self, other: Self) {}
300}
301
302extern_spec! {
303    impl<T: ?Sized> *const T {
304        #[check(ghost)]
305        #[ensures(result == self.addr_logic())]
306        fn addr(self) -> usize;
307
308        #[check(ghost)]
309        #[ensures(result == self.is_null_logic())]
310        fn is_null(self) -> bool;
311
312        #[check(ghost)]
313        #[erasure]
314        #[ensures(result == self as _)]
315        fn cast<U>(self) -> *const U {
316            self as _
317        }
318
319        #[check(terminates)]
320        #[erasure]
321        #[ensures(result == self.is_aligned_logic())]
322        fn is_aligned(self) -> bool
323            where T: Sized,
324        {
325            self.is_aligned_to(core::mem::align_of::<T>())
326        }
327
328        #[check(ghost)]
329        #[erasure]
330        #[bitwise_proof]
331        #[requires(align != 0usize && align & (align - 1usize) == 0usize)]
332        #[ensures(result == self.is_aligned_to_logic(align))]
333        fn is_aligned_to(self, align: usize) -> bool
334        {
335            if !align.is_power_of_two() {
336                ::core::panic::panic_2021!("is_aligned_to: align is not a power-of-two");
337            }
338            self.addr() & (align - 1) == 0
339        }
340    }
341
342    impl<T: ?Sized> *mut T {
343        #[check(ghost)]
344        #[ensures(result == self.addr_logic())]
345        fn addr(self) -> usize;
346
347        #[check(ghost)]
348        #[ensures(result == self.is_null_logic())]
349        fn is_null(self) -> bool;
350
351        #[check(ghost)]
352        #[erasure]
353        #[ensures(result == self as _)]
354        fn cast<U>(self) -> *mut U {
355            self as _
356        }
357
358        #[check(terminates)]
359        #[erasure]
360        #[ensures(result == self.is_aligned_logic())]
361        fn is_aligned(self) -> bool
362            where T: Sized,
363        {
364            self.is_aligned_to(core::mem::align_of::<T>())
365        }
366
367        #[check(ghost)]
368        #[erasure]
369        #[bitwise_proof]
370        #[requires(align != 0usize && align & (align - 1usize) == 0usize)]
371        #[ensures(result == self.is_aligned_to_logic(align))]
372        fn is_aligned_to(self, align: usize) -> bool
373        {
374            if !align.is_power_of_two() {
375                ::core::panic::panic_2021!("is_aligned_to: align is not a power-of-two");
376            }
377            self.addr() & (align - 1) == 0
378        }
379    }
380
381    impl<T> *const [T] {
382        #[ensures(result == metadata_logic(self))]
383        fn len(self) -> usize;
384    }
385
386    impl<T> *mut [T] {
387        #[ensures(result == metadata_logic(self))]
388        fn len(self) -> usize;
389    }
390
391    mod core {
392        mod ptr {
393            #[check(ghost)]
394            #[ensures(result.is_null_logic())]
395            fn null<T>() -> *const T
396            where
397                T: core::ptr::Thin + ?Sized;
398
399            #[check(ghost)]
400            #[ensures(result.is_null_logic())]
401            fn null_mut<T>() -> *mut T
402            where
403                T: core::ptr::Thin + ?Sized;
404
405            #[check(ghost)]
406            #[ensures(result == (p.addr_logic() == q.addr_logic()))]
407            fn addr_eq<T, U>(p: *const T, q: *const U) -> bool
408            where
409                T: ?Sized, U: ?Sized;
410
411            #[check(ghost)]
412            #[ensures(result == metadata_logic(ptr))]
413            fn metadata<T: ?Sized>(ptr: *const T) -> <T as Pointee>::Metadata;
414
415            // Postulate `check(ghost)`.
416            // It is used in a `#[trusted]` primitive in `peano`.
417            #[check(ghost)]
418            #[ensures(false)]
419            unsafe fn read_volatile<T>(src: *const T) -> T;
420
421            #[ensures(result as *const T == data && result.len_logic() == len)]
422            fn slice_from_raw_parts<T>(data: *const T, len: usize) -> *const [T];
423
424            #[ensures(result as *mut T == data && result.len_logic() == len)]
425            fn slice_from_raw_parts_mut<T>(data: *mut T, len: usize) -> *mut [T];
426        }
427    }
428
429    impl<T> Clone for *mut T {
430        #[check(ghost)]
431        #[ensures(result == *self)]
432        fn clone(&self) -> *mut T {
433            *self
434        }
435    }
436
437    impl<T> Clone for *const T {
438        #[check(ghost)]
439        #[ensures(result == *self)]
440        fn clone(&self) -> *const T {
441            *self
442        }
443    }
444}
445
446impl<T: ?Sized> Container for *const T {
447    type Value = T;
448
449    #[logic(open, inline)]
450    fn is_disjoint(&self, self_val: &T, other: &Self, other_val: &T) -> bool {
451        pearlite! {
452            size_of_val_logic(*self_val) != 0 && size_of_val_logic(*other_val) != 0 ==>
453            self.addr_logic() != other.addr_logic()
454        }
455    }
456}
457
458impl<T: ?Sized> Invariant for Perm<*const T> {
459    #[logic(open, prophetic)]
460    fn invariant(self) -> bool {
461        pearlite! {
462            !self.ward().is_null_logic()
463                && self.ptr_is_aligned_opaque()
464                && metadata_matches(*self.val(), metadata_logic(*self.ward()))
465                // Allocations can never be larger than `isize` (source: https://doc.rust-lang.org/std/ptr/index.html#allocation)
466                && size_of_val_logic(*self.val()) <= isize::MAX@
467                // The allocation fits in the address space
468                // (this is needed to verify (a `Perm` variant of) `<*const T>::add`, which checks this condition)
469                && self.ward().addr_logic()@ + size_of_val_logic(*self.val()) <= usize::MAX@
470                && inv(self.val())
471        }
472    }
473}
474
475impl<T: ?Sized> Perm<*const T> {
476    /// Creates a new `Perm<*const T>` and associated `*const` by allocating a new memory
477    /// cell initialized with `v`.
478    #[check(terminates)] // can overflow the number of available pointer adresses
479    #[ensures(*result.1.ward() == result.0 && *result.1.val() == v)]
480    pub fn new(v: T) -> (*mut T, Ghost<Box<Perm<*const T>>>)
481    where
482        T: Sized,
483    {
484        Self::from_box(Box::new(v))
485    }
486
487    /// Creates a ghost `Perm<*const T>` and associated `*const` from an existing [`Box`].
488    #[trusted]
489    #[check(terminates)] // can overflow the number of available pointer adresses
490    #[ensures(*result.1.ward() == result.0 && *result.1.val() == *val)]
491    #[erasure(Box::into_raw)]
492    pub fn from_box(val: Box<T>) -> (*mut T, Ghost<Box<Perm<*const T>>>) {
493        (Box::into_raw(val), Ghost::conjure())
494    }
495
496    /// Decompose a shared reference into a raw pointer and a ghost `Perm<*const T>`.
497    ///
498    /// # Erasure
499    ///
500    /// This function erases to a raw reborrow of a reference.
501    ///
502    /// ```ignore
503    /// Perm::from_ref(r)
504    /// // erases to
505    /// r as *const T
506    /// ```
507    #[trusted]
508    #[check(terminates)] // can overflow the number of available pointer adresses
509    #[ensures(*result.1.ward() == result.0)]
510    #[ensures(*result.1.val() == *r)]
511    #[intrinsic("perm_from_ref")]
512    pub fn from_ref(r: &T) -> (*const T, Ghost<&Perm<*const T>>) {
513        (r, Ghost::conjure())
514    }
515
516    /// Decompose a mutable reference into a raw pointer and a ghost `Perm<*const T>`.
517    ///
518    /// # Erasure
519    ///
520    /// This function erases to a raw reborrow of a reference.
521    ///
522    /// ```ignore
523    /// Perm::from_mut(r)
524    /// // erases to
525    /// r as *mut T
526    /// ```
527    #[trusted]
528    #[check(terminates)] // can overflow the number of available pointer adresses
529    #[ensures(*result.1.ward() == result.0)]
530    #[ensures(*result.1.val() == *r)]
531    #[ensures(*(^result.1.inner_logic()).val() == ^r)]
532    #[intrinsic("perm_from_mut")]
533    pub fn from_mut(r: &mut T) -> (*mut T, Ghost<&mut Perm<*const T>>) {
534        (r, Ghost::conjure())
535    }
536
537    /// Immutably borrows the underlying `T`.
538    ///
539    /// # Safety
540    ///
541    /// Safety requirements are the same as a direct dereference: `&*ptr`.
542    ///
543    /// Creusot will check that all calls to this function are indeed safe: see the
544    /// [type documentation](Perm).
545    ///
546    /// # Erasure
547    ///
548    /// This function erases to a cast from raw pointer to shared reference.
549    ///
550    /// ```ignore
551    /// Perm::as_ref(ptr, own)
552    /// // erases to
553    /// & *ptr
554    /// ```
555    #[trusted]
556    #[check(terminates)]
557    #[requires(ptr == *own.ward())]
558    #[ensures(*result == *own.val())]
559    #[allow(unused_variables)]
560    #[intrinsic("perm_as_ref")]
561    pub unsafe fn as_ref(ptr: *const T, own: Ghost<&Perm<*const T>>) -> &T {
562        unsafe { &*ptr }
563    }
564
565    /// Mutably borrows the underlying `T`.
566    ///
567    /// # Safety
568    ///
569    /// Safety requirements are the same as a direct dereference: `&mut *ptr`.
570    ///
571    /// Creusot will check that all calls to this function are indeed safe: see the
572    /// [type documentation](Perm).
573    ///
574    /// # Erasure
575    ///
576    /// This function erases to a cast from raw pointer to mutable reference.
577    ///
578    /// ```ignore
579    /// Perm::as_mut(ptr, own)
580    /// // erases to
581    /// &mut *ptr
582    /// ```
583    #[trusted]
584    #[check(terminates)]
585    #[allow(unused_variables)]
586    #[requires(ptr as *const T == *own.ward())]
587    #[ensures(*result == *own.val())]
588    #[ensures((^own).ward() == own.ward())]
589    #[ensures(*(^own).val() == ^result)]
590    #[intrinsic("perm_as_mut")]
591    pub unsafe fn as_mut(ptr: *mut T, own: Ghost<&mut Perm<*const T>>) -> &mut T {
592        unsafe { &mut *ptr }
593    }
594
595    /// Transfers ownership of `own` back into a [`Box`].
596    ///
597    /// # Safety
598    ///
599    /// Safety requirements are the same as [`Box::from_raw`].
600    ///
601    /// Creusot will check that all calls to this function are indeed safe: see the
602    /// [type documentation](Perm).
603    #[trusted]
604    #[check(terminates)]
605    #[requires(ptr as *const T == *own.ward())]
606    #[ensures(*result == *own.val())]
607    #[allow(unused_variables)]
608    #[erasure(Box::from_raw)]
609    pub unsafe fn to_box(ptr: *mut T, own: Ghost<Box<Perm<*const T>>>) -> Box<T> {
610        unsafe { Box::from_raw(ptr) }
611    }
612
613    /// Deallocates the memory pointed by `ptr`.
614    ///
615    /// # Safety
616    ///
617    /// Safety requirements are the same as [`Box::from_raw`].
618    ///
619    /// Creusot will check that all calls to this function are indeed safe: see the
620    /// [type documentation](Perm).
621    #[check(terminates)]
622    #[requires(ptr as *const T == *own.ward())]
623    pub unsafe fn drop(ptr: *mut T, own: Ghost<Box<Perm<*const T>>>) {
624        let _ = unsafe { Self::to_box(ptr, own) };
625    }
626
627    /// The pointer of a `Perm<*const T>` is always aligned.
628    #[check(ghost)]
629    #[ensures(self.ward().is_aligned_logic())]
630    pub fn ptr_is_aligned_lemma(&self) {}
631
632    /// Opaque wrapper around [`std::ptr::is_aligned_logic`].
633    /// We use this to hide alignment logic by default in `invariant` because it confuses SMT solvers sometimes.
634    /// The underlying property is exposed by [`Perm::ptr_is_aligned_lemma`].
635    #[logic(open(self))]
636    pub fn ptr_is_aligned_opaque(self) -> bool {
637        self.ward().is_aligned_logic()
638    }
639}
creusot_std/std/ptr.rs

creusot_std/std/
ptr.rs
