creusot_std/std/
ptr.rs

1mod nonnull;
2
3pub use self::nonnull::NonNullExt;
4#[cfg(creusot)]
5use crate::std::mem::{align_of_logic, size_of_logic, size_of_val_logic};
6use crate::{
7    ghost::{NotObjective, Perm, perm::PermTarget},
8    invariant::Guarded,
9    prelude::*,
10};
11use core::marker::PhantomData;
12#[cfg(creusot)]
13use core::ptr::Pointee;
14
15/// Metadata of a pointer in logic.
16///
17/// [`std::ptr::metadata`] in logic.
18#[logic(opaque)]
19pub fn metadata_logic<T: ?Sized>(_: *const T) -> <T as Pointee>::Metadata {
20    dead
21}
22
23/// Check that a value is compatible with some metadata.
24///
25/// If the value is a slice, this predicate asserts that the metadata equals the length of the slice,
26/// and that the total size of the slice is no more than `isize::MAX`. This latter property is assumed
27/// by pointer primitives such as [`slice::from_raw_parts`][from_raw_parts].
28///
29/// - For `T = [U]`, specializes to [`metadata_matches_slice`].
30/// - For `T = str`, specializes to [`metadata_matches_str`].
31/// - For `T: Sized`, specializes to `true`.
32///
33/// Why did we not make this a function `fn metadata_of(value: T) -> <T as Pointee>::Metadata`?
34/// Because this way is shorter: this corresponds to a single predicate in Why3 per type `T`.
35/// Defining a logic function that returns `usize` for slices is not so
36/// straightforward because almost every number wants to be `Int`.
37/// We would need to generate one abstract Why3 function `metadata_of : T -> Metadata`
38/// and an axiom `view_usize (metadata_of value) = len (Slice.view value)`,
39/// so two Why3 declarations instead of one.
40///
41/// [from_raw_parts]: https://doc.rust-lang.org/core/slice/fn.from_raw_parts.html
42#[logic(open, inline)]
43#[intrinsic("metadata_matches")]
44pub fn metadata_matches<T: ?Sized>(_value: T, _metadata: <T as Pointee>::Metadata) -> bool {
45    dead
46}
47
48/// Definition of [`metadata_matches`] for slices.
49#[allow(unused)]
50#[logic]
51#[intrinsic("metadata_matches_slice")]
52fn metadata_matches_slice<T>(value: [T], len: usize) -> bool {
53    pearlite! { value@.len() == len@ }
54}
55
56/// Definition of [`metadata_matches`] for string slices.
57#[allow(unused)]
58#[logic]
59#[intrinsic("metadata_matches_str")]
60fn metadata_matches_str(value: str, len: usize) -> bool {
61    pearlite! { value@.to_bytes().len() == len@ }
62}
63
64/// Whether a pointer is aligned.
65///
66/// This is a logic version of [`<*const T>::is_aligned`][is_aligned],
67/// but extended with an additional rule for `[U]`. We make use of this property
68/// in [`ghost::perm::Perm<*const T>`] to define a more precise invariant for slice pointers.
69///
70/// - For `T: Sized`, specializes to [`is_aligned_logic_sized`].
71/// - For `T = [U]`, specializes to [`is_aligned_logic_slice`].
72/// - For `T = str`, specializes to `true`.
73///
74/// [is_aligned]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned
75#[allow(unused_variables)]
76#[logic(open, inline)]
77#[intrinsic("is_aligned_logic")]
78pub fn is_aligned_logic<T: ?Sized>(ptr: *const T) -> bool {
79    dead
80}
81
82/// Definition of [`is_aligned_logic`] for `T: Sized`.
83#[allow(unused)]
84#[logic]
85#[intrinsic("is_aligned_logic_sized")]
86fn is_aligned_logic_sized<T>(ptr: *const T) -> bool {
87    ptr.is_aligned_to_logic(align_of_logic::<T>())
88}
89
90/// Definition of [`is_aligned_logic`] for `[T]`.
91#[allow(unused)]
92#[logic]
93#[intrinsic("is_aligned_logic_slice")]
94fn is_aligned_logic_slice<T>(ptr: *const [T]) -> bool {
95    ptr.is_aligned_to_logic(align_of_logic::<T>())
96}
97
98/// We conservatively model raw pointers as having an address *plus some hidden
99/// metadata*.
100///
101/// This is to account for provenance
102/// (<https://doc.rust-lang.org/std/ptr/index.html#[check(ghost)]sing-strict-provenance>) and
103/// wide pointers. See e.g.
104/// <https://doc.rust-lang.org/std/primitive.pointer.html#method.is_null>: "unsized
105/// types have many possible null pointers, as only the raw data pointer is
106/// considered, not their length, vtable, etc. Therefore, two pointers that are
107/// null may still not compare equal to each other."
108#[allow(dead_code)]
109pub struct PtrDeepModel {
110    pub addr: usize,
111    runtime_metadata: usize,
112}
113
114impl<T: ?Sized> DeepModel for *mut T {
115    type DeepModelTy = PtrDeepModel;
116    #[trusted]
117    #[logic(opaque)]
118    #[ensures(result.addr == self.addr_logic())]
119    fn deep_model(self) -> Self::DeepModelTy {
120        dead
121    }
122}
123
124impl<T: ?Sized> DeepModel for *const T {
125    type DeepModelTy = PtrDeepModel;
126    #[trusted]
127    #[logic(opaque)]
128    #[ensures(result.addr == self.addr_logic())]
129    fn deep_model(self) -> Self::DeepModelTy {
130        dead
131    }
132}
133
134/// Extension trait for pointers
135pub trait PointerExt<T: ?Sized>: Sized {
136    /// _logical_ address of the pointer
137    #[logic]
138    fn addr_logic(self) -> usize;
139
140    /// `true` if the pointer is null.
141    #[logic(open, sealed)]
142    fn is_null_logic(self) -> bool {
143        self.addr_logic() == 0usize
144    }
145
146    /// Logic counterpart to [`<*const T>::is_aligned_to`][is_aligned_to]
147    ///
148    /// [is_aligned_to]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned_to
149    #[logic(open, sealed)]
150    fn is_aligned_to_logic(self, align: usize) -> bool {
151        pearlite! { self.addr_logic() & (align - 1usize) == 0usize }
152    }
153
154    /// Logic counterpart to [`<*const T>::is_aligned`][is_aligned]
155    ///
156    /// This is defined as [`is_aligned_logic`] (plus a noop coercion for `*mut T`).
157    ///
158    /// [is_aligned]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned
159    #[logic]
160    fn is_aligned_logic(self) -> bool;
161}
162
163impl<T: ?Sized> PointerExt<T> for *const T {
164    #[logic]
165    #[cfg_attr(target_pointer_width = "16", builtin("creusot.prelude.Ptr$BW$.addr_logic_u16"))]
166    #[cfg_attr(target_pointer_width = "32", builtin("creusot.prelude.Ptr$BW$.addr_logic_u32"))]
167    #[cfg_attr(target_pointer_width = "64", builtin("creusot.prelude.Ptr$BW$.addr_logic_u64"))]
168    fn addr_logic(self) -> usize {
169        dead
170    }
171
172    #[logic(open, inline)]
173    fn is_aligned_logic(self) -> bool {
174        is_aligned_logic(self)
175    }
176}
177
178impl<T: ?Sized> PointerExt<T> for *mut T {
179    #[logic]
180    #[cfg_attr(target_pointer_width = "16", builtin("creusot.prelude.Ptr$BW$.addr_logic_u16"))]
181    #[cfg_attr(target_pointer_width = "32", builtin("creusot.prelude.Ptr$BW$.addr_logic_u32"))]
182    #[cfg_attr(target_pointer_width = "64", builtin("creusot.prelude.Ptr$BW$.addr_logic_u64"))]
183    fn addr_logic(self) -> usize {
184        dead
185    }
186
187    #[logic(open, inline)]
188    fn is_aligned_logic(self) -> bool {
189        is_aligned_logic(self)
190    }
191}
192
193/// Extension methods for `*const T` where `T: Sized`.
194pub trait SizedPointerExt<T>: PointerExt<T> {
195    /// Pointer offset in logic
196    ///
197    /// The current contract only describes the effect on `addr_logic` in the absence of overflow.
198    #[logic]
199    #[requires(0 <= self.addr_logic()@ + offset * size_of_logic::<T>())]
200    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() <= usize::MAX@)]
201    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
202    fn offset_logic(self, offset: Int) -> Self;
203
204    /// Offset by zero is the identity
205    #[logic(law)]
206    #[ensures(self.offset_logic(0) == self)]
207    fn offset_logic_zero(self);
208
209    /// Offset is associative
210    #[logic(law)]
211    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
212    fn offset_logic_assoc(self, offset1: Int, offset2: Int);
213
214    /// Pointer subtraction
215    ///
216    /// Note: we don't have `ptr1 + (ptr2 - ptr1) == ptr2`, because pointer subtraction discards provenance.
217    #[logic]
218    fn sub_logic(self, rhs: Self) -> Int;
219
220    #[logic(law)]
221    #[ensures(self.sub_logic(self) == 0)]
222    fn sub_logic_refl(self);
223
224    #[logic(law)]
225    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
226    #[ensures(self.sub_logic(self.offset_logic(offset)) == - offset)]
227    fn sub_offset_logic(self, offset: Int);
228}
229
230impl<T> SizedPointerExt<T> for *const T {
231    #[trusted]
232    #[logic(opaque)]
233    #[requires(0 <= self.addr_logic()@ + offset * size_of_logic::<T>())]
234    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() <= usize::MAX@)]
235    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
236    fn offset_logic(self, offset: Int) -> Self {
237        dead
238    }
239
240    #[trusted]
241    #[logic(law)]
242    #[ensures(self.offset_logic(0) == self)]
243    fn offset_logic_zero(self) {}
244
245    #[trusted]
246    #[logic(law)]
247    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
248    fn offset_logic_assoc(self, offset1: Int, offset2: Int) {}
249
250    #[allow(unused)]
251    #[trusted]
252    #[logic(opaque)]
253    fn sub_logic(self, rhs: Self) -> Int {
254        dead
255    }
256
257    #[trusted]
258    #[logic(law)]
259    #[ensures(self.sub_logic(self) == 0)]
260    fn sub_logic_refl(self) {}
261
262    #[trusted]
263    #[logic(law)]
264    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
265    #[ensures(self.sub_logic(self.offset_logic(offset)) == - offset)]
266    fn sub_offset_logic(self, offset: Int) {}
267}
268
269// Implemented using the impl for `*const T`
270impl<T> SizedPointerExt<T> for *mut T {
271    #[logic(open, inline)]
272    #[requires(0 <= self.addr_logic()@ + offset * size_of_logic::<T>())]
273    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() <= usize::MAX@)]
274    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
275    fn offset_logic(self, offset: Int) -> Self {
276        pearlite! { (self as *const T).offset_logic(offset) as *mut T }
277    }
278
279    #[logic(law)]
280    #[ensures(self.offset_logic(0) == self)]
281    fn offset_logic_zero(self) {}
282
283    #[logic(law)]
284    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
285    fn offset_logic_assoc(self, offset1: Int, offset2: Int) {}
286
287    #[logic(open, inline)]
288    fn sub_logic(self, rhs: Self) -> Int {
289        pearlite! { (self as *const T).sub_logic(rhs as *const T) }
290    }
291
292    #[logic(law)]
293    #[ensures(self.sub_logic(self) == 0)]
294    fn sub_logic_refl(self) {}
295
296    #[logic(law)]
297    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
298    #[ensures(self.sub_logic(self.offset_logic(offset)) == - offset)]
299    fn sub_offset_logic(self, offset: Int) {}
300}
301
302/// Extension methods for `*const [T]`
303///
304/// `thin` and `len_logic` are wrappers around `_ as *const T` and `metadata_logic`
305/// that also pull in the `slice_ptr_ext` axiom when used.
306pub trait SlicePointerExt<T>: PointerExt<[T]> {
307    /// Remove metadata.
308    #[logic]
309    fn thin(self) -> *const T;
310
311    /// Get the metadata.
312    #[logic]
313    fn len_logic(self) -> usize;
314
315    /// Extensionality law.
316    #[logic(law)]
317    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
318    fn slice_ptr_ext(self, other: Self);
319}
320
321impl<T> SlicePointerExt<T> for *const [T] {
322    /// Convert `*const [T]` to `*const T`.
323    #[logic(open, inline)]
324    fn thin(self) -> *const T {
325        self as *const T
326    }
327
328    /// Get the length metadata of the pointer.
329    #[logic(open, inline)]
330    fn len_logic(self) -> usize {
331        pearlite! { metadata_logic(self) }
332    }
333
334    /// Extensionality of slice pointers.
335    #[trusted]
336    #[logic(law)]
337    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
338    fn slice_ptr_ext(self, other: Self) {}
339}
340
341impl<T> SlicePointerExt<T> for *mut [T] {
342    /// Convert `*const [T]` to `*const T`.
343    #[logic(open, inline)]
344    fn thin(self) -> *const T {
345        self as *const T
346    }
347
348    /// Get the length metadata of the pointer.
349    #[logic(open, inline)]
350    fn len_logic(self) -> usize {
351        pearlite! { metadata_logic(self as *const [T]) }
352    }
353
354    /// Extensionality of slice pointers.
355    #[logic(law)]
356    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
357    fn slice_ptr_ext(self, other: Self) {
358        (self as *const [T]).slice_ptr_ext(other as *const [T])
359    }
360}
361
362extern_spec! {
363    impl<T: ?Sized> *const T {
364        #[check(ghost)]
365        #[logic_alias(<*const T>::addr_logic)]
366        fn addr(self) -> usize;
367
368        #[check(ghost)]
369        #[logic_alias(<*const T>::is_null_logic)]
370        fn is_null(self) -> bool;
371
372        #[check(ghost)]
373        #[erasure]
374        #[ensures(result == self as _)]
375        fn cast<U>(self) -> *const U {
376            self as _
377        }
378
379        #[check(ghost)]
380        #[erasure]
381        #[ensures(result == self as _)]
382        const fn cast_mut(self) -> *mut T {
383            self as _
384        }
385
386        #[check(terminates)]
387        #[erasure]
388        #[ensures(result == self.is_aligned_logic())]
389        fn is_aligned(self) -> bool
390            where T: Sized,
391        {
392            self.is_aligned_to(core::mem::align_of::<T>())
393        }
394
395        #[check(ghost)]
396        #[erasure]
397        #[bitwise_proof]
398        #[requires(align != 0usize && align & (align - 1usize) == 0usize)]
399        #[ensures(result == self.is_aligned_to_logic(align))]
400        fn is_aligned_to(self, align: usize) -> bool
401        {
402            if !align.is_power_of_two() {
403                ::core::panic::panic_2021!("is_aligned_to: align is not a power-of-two");
404            }
405            self.addr() & (align - 1) == 0
406        }
407    }
408
409    impl<T: ?Sized> *mut T {
410        #[check(ghost)]
411        #[logic_alias(<*mut T>::addr_logic)]
412        fn addr(self) -> usize;
413
414        #[check(ghost)]
415        #[logic_alias(<*mut T>::is_null_logic)]
416        fn is_null(self) -> bool;
417
418        #[check(ghost)]
419        #[erasure]
420        #[ensures(result == self as _)]
421        fn cast<U>(self) -> *mut U {
422            self as _
423        }
424
425        #[check(ghost)]
426        #[erasure]
427        #[ensures(result == self as _)]
428        fn cast_const(self) -> *const T {
429            self as _
430        }
431
432        #[check(terminates)]
433        #[erasure]
434        #[ensures(result == self.is_aligned_logic())]
435        fn is_aligned(self) -> bool
436            where T: Sized,
437        {
438            self.is_aligned_to(core::mem::align_of::<T>())
439        }
440
441        #[check(ghost)]
442        #[erasure]
443        #[bitwise_proof]
444        #[requires(align != 0usize && align & (align - 1usize) == 0usize)]
445        #[ensures(result == self.is_aligned_to_logic(align))]
446        fn is_aligned_to(self, align: usize) -> bool
447        {
448            if !align.is_power_of_two() {
449                ::core::panic::panic_2021!("is_aligned_to: align is not a power-of-two");
450            }
451            self.addr() & (align - 1) == 0
452        }
453    }
454
455    impl<T> *const [T] {
456        #[ensures(result == metadata_logic(self))]
457        fn len(self) -> usize;
458    }
459
460    impl<T> *mut [T] {
461        #[ensures(result == metadata_logic(self))]
462        fn len(self) -> usize;
463    }
464
465    mod core {
466        mod ptr {
467            #[check(ghost)]
468            #[ensures(result.is_null_logic())]
469            fn null<T: core::ptr::Thin + ?Sized>() -> *const T;
470
471            #[check(ghost)]
472            #[ensures(result.is_null_logic())]
473            fn null_mut<T: core::ptr::Thin + ?Sized>() -> *mut T;
474
475            #[check(ghost)]
476            #[ensures(result == (p.addr_logic() == q.addr_logic()))]
477            fn addr_eq<T: ?Sized, U: ?Sized>(p: *const T, q: *const U) -> bool;
478
479            #[check(ghost)]
480            #[ensures(result == metadata_logic(ptr))]
481            fn metadata<T: ?Sized>(ptr: *const T) -> <T as Pointee>::Metadata;
482
483            // Postulate `check(ghost)`.
484            // It is used in a `#[trusted]` primitive in `peano`.
485            #[check(ghost)]
486            #[ensures(false)]
487            unsafe fn read_volatile<T>(src: *const T) -> T;
488
489            #[ensures(result as *const T == data && result.len_logic() == len)]
490            fn slice_from_raw_parts<T>(data: *const T, len: usize) -> *const [T];
491
492            #[ensures(result as *mut T == data && result.len_logic() == len)]
493            fn slice_from_raw_parts_mut<T>(data: *mut T, len: usize) -> *mut [T];
494        }
495    }
496
497    impl<T> Clone for *mut T {
498        #[check(ghost)]
499        #[ensures(result == *self)]
500        fn clone(&self) -> *mut T {
501            *self
502        }
503    }
504
505    impl<T> Clone for *const T {
506        #[check(ghost)]
507        #[ensures(result == *self)]
508        fn clone(&self) -> *const T {
509            *self
510        }
511    }
512}
513
514impl<T: ?Sized> PermTarget for *const T {
515    type Value = T;
516    type Objectiveness = NotObjective;
517
518    /// Two pointers to distinct non-empty allocations are disjoint.
519    ///
520    /// Note that this definition also implies that a pointer to a ZST is
521    /// disjoint with itself.
522    #[logic(open, inline)]
523    fn is_disjoint(&self, self_val: &T, other: &Self, other_val: &T) -> bool {
524        pearlite! {
525            size_of_val_logic(*self_val) != 0 && size_of_val_logic(*other_val) != 0 ==>
526            self.addr_logic() != other.addr_logic()
527        }
528    }
529}
530
531impl<T: ?Sized> Invariant for Perm<*const T> {
532    #[logic(open, prophetic)]
533    fn invariant(self) -> bool {
534        pearlite! {
535            !self.ward().is_null_logic()
536                && metadata_matches(*self.val_unsized(), metadata_logic(*self.ward()))
537                && inv(self.val_unsized())
538        }
539    }
540}
541
542impl<T: ?Sized> Perm<*const T> {
543    /// Creates a new `Perm<*const T>` and associated `*const` by allocating a new memory
544    /// cell initialized with `v`.
545    #[check(terminates)] // can overflow the number of available pointer adresses
546    #[ensures(*result.1.ward() == result.0 && result.1.val() == v)]
547    #[cfg(feature = "std")]
548    pub fn new(v: T) -> (*mut T, Ghost<Perm<*const T>>)
549    where
550        T: Sized,
551    {
552        Self::from_box(Box::new(v))
553    }
554
555    /// Creates a ghost `Perm<*const T>` and associated `*const` from an existing [`Box`].
556    #[trusted]
557    #[check(terminates)] // can overflow the number of available pointer adresses
558    #[ensures(*result.1.ward() == result.0 && *result.1.val_unsized() == *val)]
559    #[erasure(Box::into_raw)]
560    #[cfg(feature = "std")]
561    pub fn from_box(val: Box<T>) -> (*mut T, Ghost<Perm<*const T>>) {
562        (Box::into_raw(val), Ghost::conjure())
563    }
564
565    /// Decompose a shared reference into a raw pointer and a ghost `Perm<*const T>`.
566    ///
567    /// # Erasure
568    ///
569    /// This function erases to a raw reborrow of a reference.
570    ///
571    /// ```ignore
572    /// Perm::from_ref(r)
573    /// // erases to
574    /// r as *const T
575    /// ```
576    #[trusted]
577    #[check(terminates)] // can overflow the number of available pointer adresses
578    #[ensures(*result.1.ward() == result.0)]
579    #[ensures(*result.1.val_unsized() == *r)]
580    #[intrinsic("perm_from_ref")]
581    pub fn from_ref(r: &T) -> (*const T, Ghost<&Perm<*const T>>) {
582        (r, Ghost::conjure())
583    }
584
585    /// Decompose a mutable reference into a raw pointer and a ghost `Perm<*const T>`.
586    ///
587    /// # Erasure
588    ///
589    /// This function erases to a raw reborrow of a reference.
590    ///
591    /// ```ignore
592    /// Perm::from_mut(r)
593    /// // erases to
594    /// r as *mut T
595    /// ```
596    #[trusted]
597    // can overflow the number of available pointer adresses
598    #[check(terminates)]
599    // Ensures that the permission is not stolen (via e.g. `std::mem::replace`)
600    #[ensures(result.1.guard() == result.0)]
601    #[ensures(*result.1.inner.val_unsized() == *r)]
602    #[ensures(*(^result.1.inner).val_unsized() == ^r)]
603    #[intrinsic("perm_from_mut")]
604    pub fn from_mut<'a>(
605        r: &'a mut T,
606    ) -> (*mut T, Ghost<Guarded<&'a mut Perm<*const T>, *const T>>) {
607        (r, Ghost::conjure())
608    }
609
610    /// Immutably borrows the underlying `T`.
611    ///
612    /// # Safety
613    ///
614    /// Safety requirements are the same as a direct dereference: `&*ptr`.
615    ///
616    /// Creusot will check that all calls to this function are indeed safe: see the
617    /// [type documentation](Perm).
618    ///
619    /// # Erasure
620    ///
621    /// This function erases to a cast from raw pointer to shared reference.
622    ///
623    /// ```ignore
624    /// Perm::as_ref(ptr, own)
625    /// // erases to
626    /// & *ptr
627    /// ```
628    #[trusted]
629    #[check(terminates)]
630    #[requires(ptr == *own.ward())]
631    #[ensures(*result == *own.val_unsized())]
632    #[allow(unused_variables)]
633    #[intrinsic("perm_as_ref")]
634    pub unsafe fn as_ref(ptr: *const T, own: Ghost<&Perm<*const T>>) -> &T {
635        unsafe { &*ptr }
636    }
637
638    /// Mutably borrows the underlying `T`.
639    ///
640    /// # Safety
641    ///
642    /// Safety requirements are the same as a direct dereference: `&mut *ptr`.
643    ///
644    /// Creusot will check that all calls to this function are indeed safe: see the
645    /// [type documentation](Perm).
646    ///
647    /// # Erasure
648    ///
649    /// This function erases to a cast from raw pointer to mutable reference.
650    ///
651    /// ```ignore
652    /// Perm::as_mut(ptr, own)
653    /// // erases to
654    /// &mut *ptr
655    /// ```
656    #[trusted]
657    #[check(terminates)]
658    #[allow(unused_variables)]
659    #[requires(ptr as *const T == *own.ward())]
660    #[ensures(*result == *own.val_unsized())]
661    #[ensures((^own).ward() == own.ward())]
662    #[ensures(*(^own).val_unsized() == ^result)]
663    #[intrinsic("perm_as_mut")]
664    pub unsafe fn as_mut(ptr: *mut T, own: Ghost<&mut Perm<*const T>>) -> &mut T {
665        unsafe { &mut *ptr }
666    }
667
668    /// Transfers ownership of `own` back into a [`Box`].
669    ///
670    /// # Safety
671    ///
672    /// Safety requirements are the same as [`Box::from_raw`].
673    ///
674    /// Creusot will check that all calls to this function are indeed safe: see the
675    /// [type documentation](Perm).
676    #[trusted]
677    #[check(terminates)]
678    #[requires(ptr as *const T == *own.ward())]
679    #[ensures(*result == *own.val_unsized())]
680    #[allow(unused_variables)]
681    #[erasure(Box::from_raw)]
682    #[cfg(feature = "std")]
683    pub unsafe fn to_box(ptr: *mut T, own: Ghost<Perm<*const T>>) -> Box<T> {
684        unsafe { Box::from_raw(ptr) }
685    }
686
687    /// Deallocates the memory pointed by `ptr`.
688    ///
689    /// # Safety
690    ///
691    /// Safety requirements are the same as [`Box::from_raw`].
692    ///
693    /// Creusot will check that all calls to this function are indeed safe: see the
694    /// [type documentation](Perm).
695    #[check(terminates)]
696    #[requires(ptr as *const T == *own.ward())]
697    #[cfg(feature = "std")]
698    pub unsafe fn drop(ptr: *mut T, own: Ghost<Perm<*const T>>) {
699        let _ = unsafe { Self::to_box(ptr, own) };
700    }
701}
702
703/// # Permissions for slice pointers
704///
705/// Core methods:
706///
707/// - To split a `&Perm<*const [T]>`: [`split_at`](Perm::split_at), [`split_at_mut`](Perm::split_at_mut).
708/// - To index a `&Perm<*const [T]>` into `&Perm<*const T>`: [`elements`](Perm::elements), [`elements_mut`](Perm::elements_mut).
709/// - To extract a [`PtrLive<T>`][PtrLive] (evidence used by pointer arithmetic): [`live`](Perm::live), [`live_mut`](Perm::live_mut).
710impl<T> Perm<*const [T]> {
711    /// The number of elements in the slice.
712    #[logic(open, inline)]
713    pub fn len(self) -> Int {
714        pearlite! { self.val_unsized()@.len() }
715    }
716
717    /// Split a `&Perm<*const [T]>` into two subslices of lengths `index` and `self.len() - index`.
718    #[trusted]
719    #[check(ghost)]
720    #[requires(0 <= index && index <= self.len())]
721    #[ensures(self.ward().thin() == result.0.ward().thin())]
722    #[ensures(self.ward().thin().offset_logic(index) == result.1.ward().thin())]
723    #[ensures(self.val_unsized()@[..index] == result.0.val_unsized()@)]
724    #[ensures(self.val_unsized()@[index..] == result.1.val_unsized()@)]
725    pub fn split_at(&self, index: Int) -> (&Self, &Self) {
726        let _ = index;
727        panic!("called ghost function in normal code")
728    }
729
730    /// Split a `&mut Perm<*const [T]>` into two subslices of lengths `index` and `self.len() - index`.
731    #[trusted]
732    #[check(ghost)]
733    #[requires(0 <= index && index <= self.len())]
734    #[ensures(result.0.guard().thin() == self.ward().thin())]
735    #[ensures(result.1.guard().thin() == self.ward().thin().offset_logic(index))]
736    #[ensures(self.val_unsized()@[..index] == result.0.inner.val_unsized()@)]
737    #[ensures(self.val_unsized()@[index..] == result.1.inner.val_unsized()@)]
738    #[ensures((^self).ward() == self.ward())]
739    #[ensures((^result.0.inner).val_unsized()@.len() == index)]
740    #[ensures((^self).val_unsized()@ == (^result.0.inner).val_unsized()@.concat((^result.1.inner).val_unsized()@))]
741    pub fn split_at_mut<'a>(
742        &'a mut self,
743        #[allow(unused)] index: Int,
744    ) -> (
745        Guarded<&'a mut Perm<*const [T]>, *const [T]>,
746        Guarded<&'a mut Perm<*const [T]>, *const [T]>,
747    ) {
748        panic!("called ghost function in normal code")
749    }
750
751    /// Split `&Perm<*const [T]>` into a sequence of `&Perm<*const T>` for each element.
752    #[trusted]
753    #[check(ghost)]
754    #[ensures(result.len() == self.len())]
755    #[ensures(forall<i> 0 <= i && i < self.len()
756        ==> *result[i].ward() == self.ward().thin().offset_logic(i)
757        && *result[i].val_unsized() == self.val_unsized()@[i])]
758    pub fn elements(&self) -> Seq<&Perm<*const T>> {
759        panic!("called ghost function in normal code")
760    }
761
762    /// Split `&mut Perm<*const [T]>` into a sequence of `&mut Perm<*const T>` for each element.
763    #[trusted]
764    #[check(ghost)]
765    #[ensures(result.len() == self.len())]
766    #[ensures(forall<i> 0 <= i && i < self.len() ==>
767        *result[i].inner.val_unsized() == self.val_unsized()@[i] &&
768        result[i].guard() == self.ward().thin().offset_logic(i)
769    )]
770    #[ensures((^self).ward() == self.ward())]
771    #[ensures(forall<i> 0 <= i && i < self.len() ==> *(^result[i].inner).val_unsized() == (^self).val_unsized()@[i])]
772    pub fn elements_mut<'a>(&'a mut self) -> Seq<Guarded<&'a mut Perm<*const T>, *const T>> {
773        panic!("called ghost function in normal code")
774    }
775
776    /// Index a `&Perm<*const [T]>` into a `&Perm<*const T>`.
777    #[check(ghost)]
778    #[requires(0 <= index && index < self.len())]
779    #[ensures(*result.ward() == self.ward().thin().offset_logic(index))]
780    #[ensures(*result.val_unsized() == self.val_unsized()@[index])]
781    pub fn index(&self, index: Int) -> &Perm<*const T> {
782        let mut r = self.elements();
783        r.split_off(index).pop_front().unwrap()
784    }
785
786    /// Index a `&mut Perm<*const [T]>` into a `&mut Perm<*const T>`.
787    #[check(ghost)]
788    #[requires(0 <= index && index < self.len())]
789    #[ensures(result.guard() == self.ward().thin().offset_logic(index))]
790    #[ensures(*result.inner.val_unsized() == self.val_unsized()@[index])]
791    #[ensures((^self).ward() == self.ward())]
792    #[ensures(*(^result.inner).val_unsized() == (^self).val_unsized()@[index])]
793    #[ensures(forall<k: Int> 0 <= k && k < self.len() && k != index ==> (^self).val_unsized()@[k] == self.val_unsized()@[k])]
794    pub fn index_mut<'a>(&'a mut self, index: Int) -> Guarded<&'a mut Perm<*const T>, *const T> {
795        let mut r = self.elements_mut();
796        proof_assert! { forall<k> index < k && k < r.len() ==> r[k].inner.val_unsized() == r[index..].tail()[k-index-1].inner.val_unsized() };
797        let _r = snapshot! { r };
798        let result = r.split_off(index).pop_front().unwrap();
799        proof_assert! { forall<i> 0 <= i && i < index ==> r[i] == _r[i] }; // Unfolding of ensures of split_off r == _r[..index]
800        result
801    }
802
803    /// Extract `PtrLive<'a, T>` from `&'a Perm<*const [T]>`.
804    #[trusted]
805    #[check(ghost)]
806    #[ensures(result.ward() == self.ward().thin())]
807    #[ensures(result.len()@ == self.len())]
808    pub fn live(&self) -> PtrLive<'_, T> {
809        panic!("called ghost function in normal code")
810    }
811
812    /// Extract `PtrLive<'a, T>` from `&'a mut Perm<*const [T]>`.
813    #[trusted]
814    #[check(ghost)]
815    #[ensures(result.ward() == self.ward().thin())]
816    #[ensures(result.len()@ == self.len())]
817    pub fn live_mut<'a, 'b>(self: &'b &'a mut Self) -> PtrLive<'a, T> {
818        panic!("called ghost function in normal code")
819    }
820}
821
822/// Evidence that a range of memory is alive.
823///
824/// This evidence enables taking pointer offsets (see [`PtrAddExt`])
825/// without ownership of that range of memory (*i.e.*, not using [`Perm`]).
826///
827/// Its lifetime is bounded by some `&Perm<*const [T]>` (via `Perm::live`
828/// or `Perm::live_mut`) so it can't outlive the associated allocation.
829#[opaque]
830pub struct PtrLive<'a, T>(PhantomData<&'a T>);
831
832impl<T> Clone for PtrLive<'_, T> {
833    #[trusted]
834    #[check(ghost)]
835    #[ensures(result == *self)]
836    fn clone(&self) -> Self {
837        panic!("called ghost function in normal code")
838    }
839}
840
841impl<T> Copy for PtrLive<'_, T> {}
842
843impl<T> Invariant for PtrLive<'_, T> {
844    #[logic(open, prophetic)]
845    fn invariant(self) -> bool {
846        pearlite! {
847            // Allocations can never be larger than `isize` bytes
848            // (source: <https://doc.rust-lang.org/std/ptr/index.html#allocation>)
849            self.len()@ * size_of_logic::<T>() <= isize::MAX@
850            // The allocation fits in the address space
851            // (for example, this is needed to verify (a `Perm`-aware variant of)
852            // `<*const T>::add`, which checks this condition)
853            && self.ward().addr_logic()@ + self.len()@ * size_of_logic::<T>() <= usize::MAX@
854            // The pointer of a `Perm` is always aligned.
855            && self.ward().is_aligned_logic()
856        }
857    }
858}
859
860impl<T> PtrLive<'_, T> {
861    /// Base pointer, start of the range
862    #[trusted]
863    #[logic(opaque)]
864    pub fn ward(self) -> *const T {
865        dead
866    }
867
868    /// The number of elements (of type `T`) in the range.
869    ///
870    /// The length in bytes is thus `self.len()@ * size_of_logic::<T>()`.
871    #[trusted]
872    #[logic(opaque)]
873    pub fn len(self) -> usize {
874        dead
875    }
876
877    /// Range inclusion.
878    ///
879    /// The live range `self.ward()..=(self.ward() + self.len())` contains
880    /// the range `ptr..=(ptr + len)`.
881    ///
882    /// Note that the out-of-bounds pointer `self.ward() + self.len()`
883    /// is included.
884    /// The provenance of `ptr` must be the same as `self.ward()`.
885    #[logic(open, inline)]
886    pub fn contains_range(self, ptr: *const T, len: Int) -> bool {
887        pearlite! {
888            let offset = ptr.sub_logic(self.ward());
889            // This checks that the provenance is the same.
890            ptr == self.ward().offset_logic(offset)
891            && 0 <= offset && offset <= self.len()@
892            && 0 <= offset + len && offset + len <= self.len()@
893        }
894    }
895}
896
897/// Pointer offsets with [`PtrLive`] permissions.
898///
899/// This trait provides wrappers around the offset functions:
900///
901/// - [`<*const T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add)
902/// - [`<*const T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset)
903/// - [`<*mut T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add-1)
904/// - [`<*mut T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset-1)
905///
906/// with ghost permission tokens (`PtrLive`) that allow proving their safety conditions.
907///
908/// # Safety
909///
910/// Source: <https://doc.rust-lang.org/core/intrinsics/fn.offset.html>
911///
912/// > If the computed offset is non-zero, then both the starting and resulting pointer must be either in bounds or at the end of an allocation.
913/// > If either pointer is out of bounds or arithmetic overflow occurs then this operation is undefined behavior.
914///
915/// The preconditions ensure that the `live` witness contains the range between `dst` and `dst + offset`,
916/// which prevents out-of-bounds access and overflow.
917pub trait PtrAddExt<'a, T> {
918    /// Implementations refine this with a non-trivial precondition.
919    #[requires(false)]
920    unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self;
921
922    /// Implementations refine this with a non-trivial precondition.
923    #[requires(false)]
924    unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self;
925}
926
927impl<'a, T> PtrAddExt<'a, T> for *const T {
928    /// Permission-aware wrapper around [`<*const T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add)
929    #[trusted]
930    #[erasure(<*const T>::add)]
931    #[requires(live.contains_range(self, offset@))]
932    #[ensures(result == self.offset_logic(offset@))]
933    unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self {
934        let _ = live;
935        unsafe { self.add(offset) }
936    }
937
938    /// Permission-aware wrapper around [`<*const T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset)
939    #[trusted]
940    #[erasure(<*const T>::offset)]
941    #[requires(live.contains_range(self, offset@))]
942    #[ensures(result == self.offset_logic(offset@))]
943    unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self {
944        let _ = live;
945        unsafe { self.offset(offset) }
946    }
947}
948
949impl<'a, T> PtrAddExt<'a, T> for *mut T {
950    /// Permission-aware wrapper around [`<*mut T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add-1)
951    #[trusted]
952    #[erasure(<*mut T>::add)]
953    #[requires(live.contains_range(self, offset@))]
954    #[ensures(result == self.offset_logic(offset@))]
955    unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self {
956        let _ = live;
957        unsafe { self.add(offset) }
958    }
959
960    /// Permission-aware wrapper around [`<*mut T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset-1)
961    #[trusted]
962    #[erasure(<*mut T>::offset)]
963    #[requires(live.contains_range(self, offset@))]
964    #[ensures(result == self.offset_logic(offset@))]
965    unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self {
966        let _ = live;
967        unsafe { self.offset(offset) }
968    }
969}
creusot_std/std/ptr.rs

creusot_std/std/
ptr.rs
