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::GuardedBorrow,
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        #[ensures(result == self.addr_logic())]
366        fn addr(self) -> usize;
367
368        #[check(ghost)]
369        #[ensures(result == self.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        #[ensures(result == self.addr_logic())]
412        fn addr(self) -> usize;
413
414        #[check(ghost)]
415        #[ensures(result == self.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() == |p: &mut Perm<*const T>| *p.ward() == result.0)]
601    #[ensures(*result.1.borrow.val_unsized() == *r)]
602    #[ensures(*(^result.1.borrow).val_unsized() == ^r)]
603    #[intrinsic("perm_from_mut")]
604    pub fn from_mut<'a>(r: &'a mut T) -> (*mut T, Ghost<GuardedBorrow<'a, Perm<*const T>>>) {
605        (r, Ghost::conjure())
606    }
607
608    /// Immutably borrows the underlying `T`.
609    ///
610    /// # Safety
611    ///
612    /// Safety requirements are the same as a direct dereference: `&*ptr`.
613    ///
614    /// Creusot will check that all calls to this function are indeed safe: see the
615    /// [type documentation](Perm).
616    ///
617    /// # Erasure
618    ///
619    /// This function erases to a cast from raw pointer to shared reference.
620    ///
621    /// ```ignore
622    /// Perm::as_ref(ptr, own)
623    /// // erases to
624    /// & *ptr
625    /// ```
626    #[trusted]
627    #[check(terminates)]
628    #[requires(ptr == *own.ward())]
629    #[ensures(*result == *own.val_unsized())]
630    #[allow(unused_variables)]
631    #[intrinsic("perm_as_ref")]
632    pub unsafe fn as_ref(ptr: *const T, own: Ghost<&Perm<*const T>>) -> &T {
633        unsafe { &*ptr }
634    }
635
636    /// Mutably borrows the underlying `T`.
637    ///
638    /// # Safety
639    ///
640    /// Safety requirements are the same as a direct dereference: `&mut *ptr`.
641    ///
642    /// Creusot will check that all calls to this function are indeed safe: see the
643    /// [type documentation](Perm).
644    ///
645    /// # Erasure
646    ///
647    /// This function erases to a cast from raw pointer to mutable reference.
648    ///
649    /// ```ignore
650    /// Perm::as_mut(ptr, own)
651    /// // erases to
652    /// &mut *ptr
653    /// ```
654    #[trusted]
655    #[check(terminates)]
656    #[allow(unused_variables)]
657    #[requires(ptr as *const T == *own.ward())]
658    #[ensures(*result == *own.val_unsized())]
659    #[ensures((^own).ward() == own.ward())]
660    #[ensures(*(^own).val_unsized() == ^result)]
661    #[intrinsic("perm_as_mut")]
662    pub unsafe fn as_mut(ptr: *mut T, own: Ghost<&mut Perm<*const T>>) -> &mut T {
663        unsafe { &mut *ptr }
664    }
665
666    /// Transfers ownership of `own` back into a [`Box`].
667    ///
668    /// # Safety
669    ///
670    /// Safety requirements are the same as [`Box::from_raw`].
671    ///
672    /// Creusot will check that all calls to this function are indeed safe: see the
673    /// [type documentation](Perm).
674    #[trusted]
675    #[check(terminates)]
676    #[requires(ptr as *const T == *own.ward())]
677    #[ensures(*result == *own.val_unsized())]
678    #[allow(unused_variables)]
679    #[erasure(Box::from_raw)]
680    #[cfg(feature = "std")]
681    pub unsafe fn to_box(ptr: *mut T, own: Ghost<Perm<*const T>>) -> Box<T> {
682        unsafe { Box::from_raw(ptr) }
683    }
684
685    /// Deallocates the memory pointed by `ptr`.
686    ///
687    /// # Safety
688    ///
689    /// Safety requirements are the same as [`Box::from_raw`].
690    ///
691    /// Creusot will check that all calls to this function are indeed safe: see the
692    /// [type documentation](Perm).
693    #[check(terminates)]
694    #[requires(ptr as *const T == *own.ward())]
695    #[cfg(feature = "std")]
696    pub unsafe fn drop(ptr: *mut T, own: Ghost<Perm<*const T>>) {
697        let _ = unsafe { Self::to_box(ptr, own) };
698    }
699}
700
701/// # Permissions for slice pointers
702///
703/// Core methods:
704///
705/// - To split a `&Perm<*const [T]>`: [`split_at`](Perm::split_at), [`split_at_mut`](Perm::split_at_mut).
706/// - To index a `&Perm<*const [T]>` into `&Perm<*const T>`: [`elements`](Perm::elements), [`elements_mut`](Perm::elements_mut).
707/// - To extract a [`PtrLive<T>`][PtrLive] (evidence used by pointer arithmetic): [`live`](Perm::live), [`live_mut`](Perm::live_mut).
708impl<T> Perm<*const [T]> {
709    /// The number of elements in the slice.
710    #[logic(open, inline)]
711    pub fn len(self) -> Int {
712        pearlite! { self.val_unsized()@.len() }
713    }
714
715    /// Split a `&Perm<*const [T]>` into two subslices of lengths `index` and `self.len() - index`.
716    #[trusted]
717    #[check(ghost)]
718    #[requires(0 <= index && index <= self.len())]
719    #[ensures(self.ward().thin() == result.0.ward().thin())]
720    #[ensures(self.ward().thin().offset_logic(index) == result.1.ward().thin())]
721    #[ensures(self.val_unsized()@[..index] == result.0.val_unsized()@)]
722    #[ensures(self.val_unsized()@[index..] == result.1.val_unsized()@)]
723    pub fn split_at(&self, index: Int) -> (&Self, &Self) {
724        let _ = index;
725        panic!("called ghost function in normal code")
726    }
727
728    /// Split a `&mut Perm<*const [T]>` into two subslices of lengths `index` and `self.len() - index`.
729    #[trusted]
730    #[check(ghost)]
731    #[requires(0 <= index && index <= self.len())]
732    #[ensures(result.0.guard() == |p: &mut Perm<*const [T]>| p.ward().thin() == self.ward().thin())]
733    #[ensures(result.1.guard() == |p: &mut Perm<*const [T]>| p.ward().thin() == self.ward().thin().offset_logic(index))]
734    #[ensures(self.val_unsized()@[..index] == result.0.borrow.val_unsized()@)]
735    #[ensures(self.val_unsized()@[index..] == result.1.borrow.val_unsized()@)]
736    #[ensures((^self).ward() == self.ward())]
737    #[ensures((^result.0.borrow).val_unsized()@.len() == index)]
738    #[ensures((^self).val_unsized()@ == (^result.0.borrow).val_unsized()@.concat((^result.1.borrow).val_unsized()@))]
739    pub fn split_at_mut<'a>(
740        &'a mut self,
741        #[allow(unused)] index: Int,
742    ) -> (GuardedBorrow<'a, Perm<*const [T]>>, GuardedBorrow<'a, Perm<*const [T]>>) {
743        panic!("called ghost function in normal code")
744    }
745
746    /// Split `&Perm<*const [T]>` into a sequence of `&Perm<*const T>` for each element.
747    #[trusted]
748    #[check(ghost)]
749    #[ensures(result.len() == self.len())]
750    #[ensures(forall<i> 0 <= i && i < self.len()
751        ==> *result[i].ward() == self.ward().thin().offset_logic(i)
752        && *result[i].val_unsized() == self.val_unsized()@[i])]
753    pub fn elements(&self) -> Seq<&Perm<*const T>> {
754        panic!("called ghost function in normal code")
755    }
756
757    /// Split `&mut Perm<*const [T]>` into a sequence of `&mut Perm<*const T>` for each element.
758    #[trusted]
759    #[check(ghost)]
760    #[ensures(result.len() == self.len())]
761    #[ensures(forall<i> 0 <= i && i < self.len() ==>
762        *result[i].borrow.val_unsized() == self.val_unsized()@[i] &&
763        result[i].guard() == |p: &mut Perm<*const T>| *p.ward() == self.ward().thin().offset_logic(i)
764    )]
765    #[ensures((^self).ward() == self.ward())]
766    #[ensures(forall<i> 0 <= i && i < self.len() ==> *(^result[i].borrow).val_unsized() == (^self).val_unsized()@[i])]
767    pub fn elements_mut<'a>(&'a mut self) -> Seq<GuardedBorrow<'a, Perm<*const T>>> {
768        panic!("called ghost function in normal code")
769    }
770
771    /// Index a `&Perm<*const [T]>` into a `&Perm<*const T>`.
772    #[check(ghost)]
773    #[requires(0 <= index && index < self.len())]
774    #[ensures(*result.ward() == self.ward().thin().offset_logic(index))]
775    #[ensures(*result.val_unsized() == self.val_unsized()@[index])]
776    pub fn index(&self, index: Int) -> &Perm<*const T> {
777        let mut r = self.elements();
778        r.split_off_ghost(index).pop_front_ghost().unwrap()
779    }
780
781    /// Index a `&mut Perm<*const [T]>` into a `&mut Perm<*const T>`.
782    #[check(ghost)]
783    #[requires(0 <= index && index < self.len())]
784    #[ensures(result.guard() == |p: &mut Perm<*const T>| *p.ward() == self.ward().thin().offset_logic(index))]
785    #[ensures(*result.borrow.val_unsized() == self.val_unsized()@[index])]
786    #[ensures((^self).ward() == self.ward())]
787    #[ensures(*(^result.borrow).val_unsized() == (^self).val_unsized()@[index])]
788    #[ensures(forall<k: Int> 0 <= k && k < self.len() && k != index ==> (^self).val_unsized()@[k] == self.val_unsized()@[k])]
789    pub fn index_mut<'a>(&'a mut self, index: Int) -> GuardedBorrow<'a, Perm<*const T>> {
790        let mut r = self.elements_mut();
791        proof_assert! { forall<k> index < k && k < r.len() ==> r[k].borrow.val_unsized() == r[index..].tail()[k-index-1].borrow.val_unsized() };
792        let _r = snapshot! { r };
793        let result = r.split_off_ghost(index).pop_front_ghost().unwrap();
794        proof_assert! { forall<i> 0 <= i && i < index ==> r[i] == _r[i] }; // Unfolding of ensures of split_off_ghost r == _r[..index]
795        result
796    }
797
798    /// Extract `PtrLive<'a, T>` from `&'a Perm<*const [T]>`.
799    #[trusted]
800    #[check(ghost)]
801    #[ensures(result.ward() == self.ward().thin())]
802    #[ensures(result.len()@ == self.len())]
803    pub fn live(&self) -> PtrLive<'_, T> {
804        panic!("called ghost function in normal code")
805    }
806
807    /// Extract `PtrLive<'a, T>` from `&'a mut Perm<*const [T]>`.
808    #[trusted]
809    #[check(ghost)]
810    #[ensures(result.ward() == self.ward().thin())]
811    #[ensures(result.len()@ == self.len())]
812    pub fn live_mut<'a, 'b>(self: &'b &'a mut Self) -> PtrLive<'a, T> {
813        panic!("called ghost function in normal code")
814    }
815}
816
817/// Evidence that a range of memory is alive.
818///
819/// This evidence enables taking pointer offsets (see [`PtrAddExt`])
820/// without ownership of that range of memory (*i.e.*, not using [`Perm`]).
821///
822/// Its lifetime is bounded by some `&Perm<*const [T]>` (via `Perm::live`
823/// or `Perm::live_mut`) so it can't outlive the associated allocation.
824#[opaque]
825pub struct PtrLive<'a, T>(PhantomData<&'a T>);
826
827impl<T> Clone for PtrLive<'_, T> {
828    #[trusted]
829    #[check(ghost)]
830    #[ensures(result == *self)]
831    fn clone(&self) -> Self {
832        panic!("called ghost function in normal code")
833    }
834}
835
836impl<T> Copy for PtrLive<'_, T> {}
837
838impl<T> Invariant for PtrLive<'_, T> {
839    #[logic(open, prophetic)]
840    fn invariant(self) -> bool {
841        pearlite! {
842            // Allocations can never be larger than `isize` bytes
843            // (source: <https://doc.rust-lang.org/std/ptr/index.html#allocation>)
844            self.len()@ * size_of_logic::<T>() <= isize::MAX@
845            // The allocation fits in the address space
846            // (for example, this is needed to verify (a `Perm`-aware variant of)
847            // `<*const T>::add`, which checks this condition)
848            && self.ward().addr_logic()@ + self.len()@ * size_of_logic::<T>() <= usize::MAX@
849            // The pointer of a `Perm` is always aligned.
850            && self.ward().is_aligned_logic()
851        }
852    }
853}
854
855impl<T> PtrLive<'_, T> {
856    /// Base pointer, start of the range
857    #[trusted]
858    #[logic(opaque)]
859    pub fn ward(self) -> *const T {
860        dead
861    }
862
863    /// The number of elements (of type `T`) in the range.
864    ///
865    /// The length in bytes is thus `self.len()@ * size_of_logic::<T>()`.
866    #[trusted]
867    #[logic(opaque)]
868    pub fn len(self) -> usize {
869        dead
870    }
871
872    /// Range inclusion.
873    ///
874    /// The live range `self.ward()..=(self.ward() + self.len())` contains
875    /// the range `ptr..=(ptr + len)`.
876    ///
877    /// Note that the out-of-bounds pointer `self.ward() + self.len()`
878    /// is included.
879    /// The provenance of `ptr` must be the same as `self.ward()`.
880    #[logic(open, inline)]
881    pub fn contains_range(self, ptr: *const T, len: Int) -> bool {
882        pearlite! {
883            let offset = ptr.sub_logic(self.ward());
884            // This checks that the provenance is the same.
885            ptr == self.ward().offset_logic(offset)
886            && 0 <= offset && offset <= self.len()@
887            && 0 <= offset + len && offset + len <= self.len()@
888        }
889    }
890}
891
892/// Pointer offsets with [`PtrLive`] permissions.
893///
894/// This trait provides wrappers around the offset functions:
895///
896/// - [`<*const T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add)
897/// - [`<*const T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset)
898/// - [`<*mut T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add-1)
899/// - [`<*mut T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset-1)
900///
901/// with ghost permission tokens (`PtrLive`) that allow proving their safety conditions.
902///
903/// # Safety
904///
905/// Source: <https://doc.rust-lang.org/core/intrinsics/fn.offset.html>
906///
907/// > 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.
908/// > If either pointer is out of bounds or arithmetic overflow occurs then this operation is undefined behavior.
909///
910/// The preconditions ensure that the `live` witness contains the range between `dst` and `dst + offset`,
911/// which prevents out-of-bounds access and overflow.
912pub trait PtrAddExt<'a, T> {
913    /// Implementations refine this with a non-trivial precondition.
914    #[requires(false)]
915    unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self;
916
917    /// Implementations refine this with a non-trivial precondition.
918    #[requires(false)]
919    unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self;
920}
921
922impl<'a, T> PtrAddExt<'a, T> for *const T {
923    /// Permission-aware wrapper around [`<*const T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add)
924    #[trusted]
925    #[erasure(<*const T>::add)]
926    #[requires(live.contains_range(self, offset@))]
927    #[ensures(result == self.offset_logic(offset@))]
928    unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self {
929        let _ = live;
930        unsafe { self.add(offset) }
931    }
932
933    /// Permission-aware wrapper around [`<*const T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset)
934    #[trusted]
935    #[erasure(<*const T>::offset)]
936    #[requires(live.contains_range(self, offset@))]
937    #[ensures(result == self.offset_logic(offset@))]
938    unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self {
939        let _ = live;
940        unsafe { self.offset(offset) }
941    }
942}
943
944impl<'a, T> PtrAddExt<'a, T> for *mut T {
945    /// Permission-aware wrapper around [`<*mut T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add-1)
946    #[trusted]
947    #[erasure(<*mut T>::add)]
948    #[requires(live.contains_range(self, offset@))]
949    #[ensures(result == self.offset_logic(offset@))]
950    unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self {
951        let _ = live;
952        unsafe { self.add(offset) }
953    }
954
955    /// Permission-aware wrapper around [`<*mut T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset-1)
956    #[trusted]
957    #[erasure(<*mut T>::offset)]
958    #[requires(live.contains_range(self, offset@))]
959    #[ensures(result == self.offset_logic(offset@))]
960    unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self {
961        let _ = live;
962        unsafe { self.offset(offset) }
963    }
964}
creusot_std/std/ptr.rs

creusot_std/std/
ptr.rs
