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

creusot_std/std/
ptr.rs
