creusot_std/std/
ptr.rs

1#[cfg(creusot)]
2use crate::std::mem::{align_of_logic, size_of_logic, size_of_val_logic};
3use crate::{
4    ghost::perm::{Container, Perm},
5    prelude::*,
6};
7use core::marker::PhantomData;
8#[cfg(creusot)]
9use core::ptr::Pointee;
10
11#[cfg(not(feature = "std"))]
12use alloc::boxed::Box;
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(self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@)]
199    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
200    fn offset_logic(self, offset: Int) -> Self;
201
202    /// Offset by zero is the identity
203    #[logic(law)]
204    #[ensures(self.offset_logic(0) == self)]
205    fn offset_logic_zero(self);
206
207    /// Offset is associative
208    #[logic(law)]
209    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
210    fn offset_logic_assoc(self, offset1: Int, offset2: Int);
211
212    /// Pointer subtraction
213    ///
214    /// Note: we don't have `ptr1 + (ptr2 - ptr1) == ptr2`, because pointer subtraction discards provenance.
215    #[logic]
216    fn sub_logic(self, rhs: Self) -> Int;
217
218    #[logic(law)]
219    #[ensures(self.sub_logic(self) == 0)]
220    fn sub_logic_refl(self);
221
222    #[logic(law)]
223    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
224    fn sub_offset_logic(self, offset: Int);
225}
226
227impl<T> SizedPointerExt<T> for *const T {
228    #[trusted]
229    #[logic(opaque)]
230    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@)]
231    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
232    fn offset_logic(self, offset: Int) -> Self {
233        dead
234    }
235
236    #[trusted]
237    #[logic(law)]
238    #[ensures(self.offset_logic(0) == self)]
239    fn offset_logic_zero(self) {}
240
241    #[trusted]
242    #[logic(law)]
243    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
244    fn offset_logic_assoc(self, offset1: Int, offset2: Int) {}
245
246    #[allow(unused)]
247    #[trusted]
248    #[logic(opaque)]
249    fn sub_logic(self, rhs: Self) -> Int {
250        dead
251    }
252
253    #[trusted]
254    #[logic(law)]
255    #[ensures(self.sub_logic(self) == 0)]
256    fn sub_logic_refl(self) {}
257
258    #[trusted]
259    #[logic(law)]
260    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
261    fn sub_offset_logic(self, offset: Int) {}
262}
263
264// Implemented using the impl for `*const T`
265impl<T> SizedPointerExt<T> for *mut T {
266    #[logic(open, inline)]
267    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@)]
268    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
269    fn offset_logic(self, offset: Int) -> Self {
270        pearlite! { (self as *const T).offset_logic(offset) as *mut T }
271    }
272
273    #[logic(law)]
274    #[ensures(self.offset_logic(0) == self)]
275    fn offset_logic_zero(self) {}
276
277    #[logic(law)]
278    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
279    fn offset_logic_assoc(self, offset1: Int, offset2: Int) {}
280
281    #[logic(open, inline)]
282    fn sub_logic(self, rhs: Self) -> Int {
283        pearlite! { (self as *const T).sub_logic(rhs as *const T) }
284    }
285
286    #[logic(law)]
287    #[ensures(self.sub_logic(self) == 0)]
288    fn sub_logic_refl(self) {}
289
290    #[logic(law)]
291    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
292    fn sub_offset_logic(self, offset: Int) {}
293}
294
295/// Extension methods for `*const [T]`
296///
297/// `thin` and `len_logic` are wrappers around `_ as *const T` and `metadata_logic`
298/// that also pull in the `slice_ptr_ext` axiom when used.
299pub trait SlicePointerExt<T>: PointerExt<[T]> {
300    /// Remove metadata.
301    #[logic]
302    fn thin(self) -> *const T;
303
304    /// Get the metadata.
305    #[logic]
306    fn len_logic(self) -> usize;
307
308    /// Extensionality law.
309    #[logic(law)]
310    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
311    fn slice_ptr_ext(self, other: Self);
312}
313
314impl<T> SlicePointerExt<T> for *const [T] {
315    /// Convert `*const [T]` to `*const T`.
316    #[logic(open, inline)]
317    fn thin(self) -> *const T {
318        self as *const T
319    }
320
321    /// Get the length metadata of the pointer.
322    #[logic(open, inline)]
323    fn len_logic(self) -> usize {
324        pearlite! { metadata_logic(self) }
325    }
326
327    /// Extensionality of slice pointers.
328    #[trusted]
329    #[logic(law)]
330    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
331    fn slice_ptr_ext(self, other: Self) {}
332}
333
334impl<T> SlicePointerExt<T> for *mut [T] {
335    /// Convert `*const [T]` to `*const T`.
336    #[logic(open, inline)]
337    fn thin(self) -> *const T {
338        self as *const T
339    }
340
341    /// Get the length metadata of the pointer.
342    #[logic(open, inline)]
343    fn len_logic(self) -> usize {
344        pearlite! { metadata_logic(self as *const [T]) }
345    }
346
347    /// Extensionality of slice pointers.
348    #[logic(law)]
349    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
350    fn slice_ptr_ext(self, other: Self) {
351        (self as *const [T]).slice_ptr_ext(other as *const [T])
352    }
353}
354
355extern_spec! {
356    impl<T: ?Sized> *const T {
357        #[check(ghost)]
358        #[ensures(result == self.addr_logic())]
359        fn addr(self) -> usize;
360
361        #[check(ghost)]
362        #[ensures(result == self.is_null_logic())]
363        fn is_null(self) -> bool;
364
365        #[check(ghost)]
366        #[erasure]
367        #[ensures(result == self as _)]
368        fn cast<U>(self) -> *const U {
369            self as _
370        }
371
372        #[check(ghost)]
373        #[erasure]
374        #[ensures(result == self as _)]
375        const fn cast_mut(self) -> *mut T {
376            self as _
377        }
378
379        #[check(terminates)]
380        #[erasure]
381        #[ensures(result == self.is_aligned_logic())]
382        fn is_aligned(self) -> bool
383            where T: Sized,
384        {
385            self.is_aligned_to(core::mem::align_of::<T>())
386        }
387
388        #[check(ghost)]
389        #[erasure]
390        #[bitwise_proof]
391        #[requires(align != 0usize && align & (align - 1usize) == 0usize)]
392        #[ensures(result == self.is_aligned_to_logic(align))]
393        fn is_aligned_to(self, align: usize) -> bool
394        {
395            if !align.is_power_of_two() {
396                ::core::panic::panic_2021!("is_aligned_to: align is not a power-of-two");
397            }
398            self.addr() & (align - 1) == 0
399        }
400    }
401
402    impl<T: ?Sized> *mut T {
403        #[check(ghost)]
404        #[ensures(result == self.addr_logic())]
405        fn addr(self) -> usize;
406
407        #[check(ghost)]
408        #[ensures(result == self.is_null_logic())]
409        fn is_null(self) -> bool;
410
411        #[check(ghost)]
412        #[erasure]
413        #[ensures(result == self as _)]
414        fn cast<U>(self) -> *mut U {
415            self as _
416        }
417
418        #[check(ghost)]
419        #[erasure]
420        #[ensures(result == self as _)]
421        fn cast_const(self) -> *const T {
422            self as _
423        }
424
425        #[check(terminates)]
426        #[erasure]
427        #[ensures(result == self.is_aligned_logic())]
428        fn is_aligned(self) -> bool
429            where T: Sized,
430        {
431            self.is_aligned_to(core::mem::align_of::<T>())
432        }
433
434        #[check(ghost)]
435        #[erasure]
436        #[bitwise_proof]
437        #[requires(align != 0usize && align & (align - 1usize) == 0usize)]
438        #[ensures(result == self.is_aligned_to_logic(align))]
439        fn is_aligned_to(self, align: usize) -> bool
440        {
441            if !align.is_power_of_two() {
442                ::core::panic::panic_2021!("is_aligned_to: align is not a power-of-two");
443            }
444            self.addr() & (align - 1) == 0
445        }
446    }
447
448    impl<T> *const [T] {
449        #[ensures(result == metadata_logic(self))]
450        fn len(self) -> usize;
451    }
452
453    impl<T> *mut [T] {
454        #[ensures(result == metadata_logic(self))]
455        fn len(self) -> usize;
456    }
457
458    mod core {
459        mod ptr {
460            #[check(ghost)]
461            #[ensures(result.is_null_logic())]
462            fn null<T>() -> *const T
463            where
464                T: core::ptr::Thin + ?Sized;
465
466            #[check(ghost)]
467            #[ensures(result.is_null_logic())]
468            fn null_mut<T>() -> *mut T
469            where
470                T: core::ptr::Thin + ?Sized;
471
472            #[check(ghost)]
473            #[ensures(result == (p.addr_logic() == q.addr_logic()))]
474            fn addr_eq<T, U>(p: *const T, q: *const U) -> bool
475            where
476                T: ?Sized, U: ?Sized;
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> Container for *const T {
514    type Value = T;
515
516    #[logic(open, inline)]
517    fn is_disjoint(&self, self_val: &T, other: &Self, other_val: &T) -> bool {
518        pearlite! {
519            size_of_val_logic(*self_val) != 0 && size_of_val_logic(*other_val) != 0 ==>
520            self.addr_logic() != other.addr_logic()
521        }
522    }
523}
524
525impl<T: ?Sized> Invariant for Perm<*const T> {
526    #[logic(open, prophetic)]
527    fn invariant(self) -> bool {
528        pearlite! {
529            !self.ward().is_null_logic()
530                && metadata_matches(*self.val(), metadata_logic(*self.ward()))
531                && inv(self.val())
532        }
533    }
534}
535
536impl<T: ?Sized> Perm<*const T> {
537    /// Creates a new `Perm<*const T>` and associated `*const` by allocating a new memory
538    /// cell initialized with `v`.
539    #[check(terminates)] // can overflow the number of available pointer adresses
540    #[ensures(*result.1.ward() == result.0 && *result.1.val() == v)]
541    pub fn new(v: T) -> (*mut T, Ghost<Box<Perm<*const T>>>)
542    where
543        T: Sized,
544    {
545        Self::from_box(Box::new(v))
546    }
547
548    /// Creates a ghost `Perm<*const T>` and associated `*const` from an existing [`Box`].
549    #[trusted]
550    #[check(terminates)] // can overflow the number of available pointer adresses
551    #[ensures(*result.1.ward() == result.0 && *result.1.val() == *val)]
552    #[erasure(Box::into_raw)]
553    pub fn from_box(val: Box<T>) -> (*mut T, Ghost<Box<Perm<*const T>>>) {
554        (Box::into_raw(val), Ghost::conjure())
555    }
556
557    /// Decompose a shared reference into a raw pointer and a ghost `Perm<*const T>`.
558    ///
559    /// # Erasure
560    ///
561    /// This function erases to a raw reborrow of a reference.
562    ///
563    /// ```ignore
564    /// Perm::from_ref(r)
565    /// // erases to
566    /// r as *const T
567    /// ```
568    #[trusted]
569    #[check(terminates)] // can overflow the number of available pointer adresses
570    #[ensures(*result.1.ward() == result.0)]
571    #[ensures(*result.1.val() == *r)]
572    #[intrinsic("perm_from_ref")]
573    pub fn from_ref(r: &T) -> (*const T, Ghost<&Perm<*const T>>) {
574        (r, Ghost::conjure())
575    }
576
577    /// Decompose a mutable reference into a raw pointer and a ghost `Perm<*const T>`.
578    ///
579    /// # Erasure
580    ///
581    /// This function erases to a raw reborrow of a reference.
582    ///
583    /// ```ignore
584    /// Perm::from_mut(r)
585    /// // erases to
586    /// r as *mut T
587    /// ```
588    #[trusted]
589    #[check(terminates)] // can overflow the number of available pointer adresses
590    #[ensures(*result.1.ward() == result.0)]
591    #[ensures(*result.1.val() == *r)]
592    #[ensures(*(^result.1.inner_logic()).val() == ^r)]
593    #[intrinsic("perm_from_mut")]
594    pub fn from_mut(r: &mut T) -> (*mut T, Ghost<&mut Perm<*const T>>) {
595        (r, Ghost::conjure())
596    }
597
598    /// Immutably borrows the underlying `T`.
599    ///
600    /// # Safety
601    ///
602    /// Safety requirements are the same as a direct dereference: `&*ptr`.
603    ///
604    /// Creusot will check that all calls to this function are indeed safe: see the
605    /// [type documentation](Perm).
606    ///
607    /// # Erasure
608    ///
609    /// This function erases to a cast from raw pointer to shared reference.
610    ///
611    /// ```ignore
612    /// Perm::as_ref(ptr, own)
613    /// // erases to
614    /// & *ptr
615    /// ```
616    #[trusted]
617    #[check(terminates)]
618    #[requires(ptr == *own.ward())]
619    #[ensures(*result == *own.val())]
620    #[allow(unused_variables)]
621    #[intrinsic("perm_as_ref")]
622    pub unsafe fn as_ref(ptr: *const T, own: Ghost<&Perm<*const T>>) -> &T {
623        unsafe { &*ptr }
624    }
625
626    /// Mutably borrows the underlying `T`.
627    ///
628    /// # Safety
629    ///
630    /// Safety requirements are the same as a direct dereference: `&mut *ptr`.
631    ///
632    /// Creusot will check that all calls to this function are indeed safe: see the
633    /// [type documentation](Perm).
634    ///
635    /// # Erasure
636    ///
637    /// This function erases to a cast from raw pointer to mutable reference.
638    ///
639    /// ```ignore
640    /// Perm::as_mut(ptr, own)
641    /// // erases to
642    /// &mut *ptr
643    /// ```
644    #[trusted]
645    #[check(terminates)]
646    #[allow(unused_variables)]
647    #[requires(ptr as *const T == *own.ward())]
648    #[ensures(*result == *own.val())]
649    #[ensures((^own).ward() == own.ward())]
650    #[ensures(*(^own).val() == ^result)]
651    #[intrinsic("perm_as_mut")]
652    pub unsafe fn as_mut(ptr: *mut T, own: Ghost<&mut Perm<*const T>>) -> &mut T {
653        unsafe { &mut *ptr }
654    }
655
656    /// Transfers ownership of `own` back into a [`Box`].
657    ///
658    /// # Safety
659    ///
660    /// Safety requirements are the same as [`Box::from_raw`].
661    ///
662    /// Creusot will check that all calls to this function are indeed safe: see the
663    /// [type documentation](Perm).
664    #[trusted]
665    #[check(terminates)]
666    #[requires(ptr as *const T == *own.ward())]
667    #[ensures(*result == *own.val())]
668    #[allow(unused_variables)]
669    #[erasure(Box::from_raw)]
670    pub unsafe fn to_box(ptr: *mut T, own: Ghost<Box<Perm<*const T>>>) -> Box<T> {
671        unsafe { Box::from_raw(ptr) }
672    }
673
674    /// Deallocates the memory pointed by `ptr`.
675    ///
676    /// # Safety
677    ///
678    /// Safety requirements are the same as [`Box::from_raw`].
679    ///
680    /// Creusot will check that all calls to this function are indeed safe: see the
681    /// [type documentation](Perm).
682    #[check(terminates)]
683    #[requires(ptr as *const T == *own.ward())]
684    pub unsafe fn drop(ptr: *mut T, own: Ghost<Box<Perm<*const T>>>) {
685        let _ = unsafe { Self::to_box(ptr, own) };
686    }
687}
688
689/// # Permissions for slice pointers
690///
691/// Core methods:
692///
693/// - To split a `&Perm<*const [T]>`: [`split_at`](Perm::split_at), [`split_at_mut`](Perm::split_at_mut).
694/// - To index a `&Perm<*const [T]>` into `&Perm<*const T>`: [`elements`](Perm::elements), [`elements_mut`](Perm::elements_mut).
695/// - To extract a [`PtrLive<T>`][PtrLive] (evidence used by pointer arithmetic): [`live`](Perm::live), [`live_mut`](Perm::live_mut).
696impl<T> Perm<*const [T]> {
697    /// The number of elements in the slice.
698    #[logic(open, inline)]
699    pub fn len(self) -> Int {
700        pearlite! { self.val()@.len() }
701    }
702
703    /// Split a `&Perm<*const [T]>` into two subslices of lengths `index` and `self.len() - index`.
704    #[trusted]
705    #[check(ghost)]
706    #[requires(0 <= index && index <= self.len())]
707    #[ensures(self.ward().thin() == result.0.ward().thin())]
708    #[ensures(self.ward().thin().offset_logic(index) == result.1.ward().thin())]
709    #[ensures(self.val()@[..index] == result.0.val()@)]
710    #[ensures(self.val()@[index..] == result.1.val()@)]
711    pub fn split_at(&self, index: Int) -> (&Self, &Self) {
712        let _ = index;
713        panic!("called ghost function in normal code")
714    }
715
716    /// Split a `&mut Perm<*const [T]>` into two subslices of lengths `index` and `self.len() - index`.
717    #[trusted]
718    #[check(ghost)]
719    #[requires(0 <= index && index <= self.len())]
720    #[ensures(self.ward().thin() == result.0.ward().thin())]
721    #[ensures(self.ward().thin().offset_logic(index) == result.1.ward().thin())]
722    #[ensures(self.val()@[..index] == result.0.val()@)]
723    #[ensures(self.val()@[index..] == result.1.val()@)]
724    #[ensures((^self).ward() == self.ward())]
725    #[ensures((^result.0).val()@.len() == index)]
726    #[ensures((^self).val()@ == (^result.0).val()@.concat((^result.1).val()@))]
727    pub fn split_at_mut(&mut self, index: Int) -> (&mut Perm<*const [T]>, &mut Perm<*const [T]>) {
728        let _ = index;
729        panic!("called ghost function in normal code")
730    }
731
732    /// Split `&Perm<*const [T]>` into a sequence of `&Perm<*const T>` for each element.
733    #[trusted]
734    #[check(ghost)]
735    #[ensures(result.len() == self.len())]
736    #[ensures(forall<i> 0 <= i && i < self.len()
737        ==> *result[i].ward() == self.ward().thin().offset_logic(i)
738        && *result[i].val() == self.val()@[i])]
739    pub fn elements(&self) -> Seq<&Perm<*const T>> {
740        panic!("called ghost function in normal code")
741    }
742
743    /// Split `&mut Perm<*const [T]>` into a sequence of `&mut Perm<*const T>` for each element.
744    #[trusted]
745    #[check(ghost)]
746    #[ensures(result.len() == self.len())]
747    #[ensures(forall<i> 0 <= i && i < self.len()
748        ==> *result[i].ward() == self.ward().thin().offset_logic(i)
749        && *result[i].val() == self.val()@[i])]
750    #[ensures((^self).ward() == self.ward())]
751    #[ensures(forall<i> 0 <= i && i < self.len() ==> *(^result[i]).val() == (^self).val()@[i])]
752    pub fn elements_mut(&mut self) -> Seq<&mut Perm<*const T>> {
753        panic!("called ghost function in normal code")
754    }
755
756    /// Index a `&Perm<*const [T]>` into a `&Perm<*const T>`.
757    #[check(ghost)]
758    #[requires(0 <= index && index < self.len())]
759    #[ensures(*result.ward() == self.ward().thin().offset_logic(index))]
760    #[ensures(*result.val() == self.val()@[index])]
761    pub fn index(&self, index: Int) -> &Perm<*const T> {
762        let mut r = self.elements();
763        r.split_off_ghost(index).pop_front_ghost().unwrap()
764    }
765
766    /// Index a `&mut Perm<*const [T]>` into a `&mut Perm<*const T>`.
767    #[check(ghost)]
768    #[requires(0 <= index && index < self.len())]
769    #[ensures(*result.ward() == self.ward().thin().offset_logic(index))]
770    #[ensures(*result.val() == self.val()@[index])]
771    #[ensures((^self).ward() == self.ward())]
772    #[ensures(*(^result).val() == (^self).val()@[index])]
773    #[ensures(forall<k: Int> 0 <= k && k < self.len() && k != index ==> (^self).val()@[k] == self.val()@[k])]
774    pub fn index_mut(&mut self, index: Int) -> &mut Perm<*const T> {
775        let mut r = self.elements_mut();
776        proof_assert! { forall<k> index < k && k < r.len() ==> r[k].val() == r[index..].tail()[k-index-1].val() };
777        let _r = snapshot! { r };
778        let result = r.split_off_ghost(index).pop_front_ghost().unwrap();
779        proof_assert! { forall<i> 0 <= i && i < index ==> r[i] == _r[i] }; // Unfolding of ensures of split_off_ghost r == _r[..index]
780        result
781    }
782
783    /// Extract `PtrLive<'a, T>` from `&'a Perm<*const [T]>`.
784    #[trusted]
785    #[check(ghost)]
786    #[ensures(result.ward() == self.ward().thin())]
787    #[ensures(result.len()@ == self.len())]
788    pub fn live(&self) -> PtrLive<'_, T> {
789        panic!("called ghost function in normal code")
790    }
791
792    /// Extract `PtrLive<'a, T>` from `&'a mut Perm<*const [T]>`.
793    #[trusted]
794    #[check(ghost)]
795    #[ensures(result.ward() == self.ward().thin())]
796    #[ensures(result.len()@ == self.len())]
797    pub fn live_mut<'a, 'b>(self: &'b &'a mut Self) -> PtrLive<'a, T> {
798        panic!("called ghost function in normal code")
799    }
800}
801
802/// Evidence that a range of memory is alive.
803///
804/// This evidence enables taking pointer offsets (see [`PtrAddExt`])
805/// without ownership of that range of memory (*i.e.*, not using [`Perm`]).
806///
807/// Its lifetime is bounded by some `&Perm<*const [T]>` (via `Perm::live`
808/// or `Perm::live_mut`) so it can't outlive the associated allocation.
809#[opaque]
810pub struct PtrLive<'a, T>(PhantomData<&'a T>);
811
812impl<T> Clone for PtrLive<'_, T> {
813    #[trusted]
814    #[check(ghost)]
815    #[ensures(result == *self)]
816    fn clone(&self) -> Self {
817        panic!("called ghost function in normal code")
818    }
819}
820
821impl<T> Copy for PtrLive<'_, T> {}
822
823impl<T> Invariant for PtrLive<'_, T> {
824    #[logic(open, prophetic)]
825    fn invariant(self) -> bool {
826        pearlite! {
827            // Allocations can never be larger than `isize` bytes
828            // (source: <https://doc.rust-lang.org/std/ptr/index.html#allocation>)
829            self.len()@ * size_of_logic::<T>() <= isize::MAX@
830            // The allocation fits in the address space
831            // (for example, this is needed to verify (a `Perm`-aware variant of)
832            // `<*const T>::add`, which checks this condition)
833            && self.ward().addr_logic()@ + self.len()@ * size_of_logic::<T>() <= usize::MAX@
834            // The pointer of a `Perm` is always aligned.
835            && self.ward().is_aligned_logic()
836        }
837    }
838}
839
840impl<T> PtrLive<'_, T> {
841    /// Base pointer, start of the range
842    #[trusted]
843    #[logic(opaque)]
844    pub fn ward(self) -> *const T {
845        dead
846    }
847
848    /// The number of elements (of type `T`) in the range.
849    ///
850    /// The length in bytes is thus `self.len()@ * size_of_logic::<T>()`.
851    #[trusted]
852    #[logic(opaque)]
853    pub fn len(self) -> usize {
854        dead
855    }
856
857    /// Range inclusion.
858    ///
859    /// The live range `self.ward()..=(self.ward() + self.len())` contains
860    /// the range `ptr..=(ptr + len)`.
861    ///
862    /// Note that the out-of-bounds pointer `self.ward() + self.len()`
863    /// is included.
864    /// The provenance of `ptr` must be the same as `self.ward()`.
865    #[logic(open, inline)]
866    pub fn contains_range(self, ptr: *const T, len: Int) -> bool {
867        pearlite! {
868            let offset = ptr.sub_logic(self.ward());
869            // This checks that the provenance is the same.
870            ptr == self.ward().offset_logic(offset)
871            && 0 <= offset && offset <= self.len()@
872            && 0 <= offset + len && offset + len <= self.len()@
873        }
874    }
875}
876
877/// Pointer offsets with [`PtrLive`] permissions.
878///
879/// This trait provides wrappers around the offset functions:
880///
881/// - [`<*const T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add)
882/// - [`<*const T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset)
883/// - [`<*mut T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add-1)
884/// - [`<*mut T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset-1)
885///
886/// with ghost permission tokens (`PtrLive`) that allow proving their safety conditions.
887///
888/// # Safety
889///
890/// Source: <https://doc.rust-lang.org/core/intrinsics/fn.offset.html>
891///
892/// > 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.
893/// > If either pointer is out of bounds or arithmetic overflow occurs then this operation is undefined behavior.
894///
895/// The preconditions ensure that the `live` witness contains the range between `dst` and `dst + offset`,
896/// which prevents out-of-bounds access and overflow.
897pub trait PtrAddExt<'a, T> {
898    /// Implementations refine this with a non-trivial precondition.
899    #[requires(false)]
900    unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self;
901
902    /// Implementations refine this with a non-trivial precondition.
903    #[requires(false)]
904    unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self;
905}
906
907impl<'a, T> PtrAddExt<'a, T> for *const T {
908    /// Permission-aware wrapper around [`<*const T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add)
909    #[trusted]
910    #[erasure(<*const T>::add)]
911    #[requires(live.contains_range(self, offset@))]
912    #[ensures(result == self.offset_logic(offset@))]
913    unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self {
914        let _ = live;
915        unsafe { self.add(offset) }
916    }
917
918    /// Permission-aware wrapper around [`<*const T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset)
919    #[trusted]
920    #[erasure(<*const T>::offset)]
921    #[requires(live.contains_range(self, offset@))]
922    #[ensures(result == self.offset_logic(offset@))]
923    unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self {
924        let _ = live;
925        unsafe { self.offset(offset) }
926    }
927}
928
929impl<'a, T> PtrAddExt<'a, T> for *mut T {
930    /// Permission-aware wrapper around [`<*mut T>::add`](https://doc.rust-lang.org/core/primitive.pointer.html#method.add-1)
931    #[trusted]
932    #[erasure(<*mut T>::add)]
933    #[requires(live.contains_range(self, offset@))]
934    #[ensures(result == self.offset_logic(offset@))]
935    unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self {
936        let _ = live;
937        unsafe { self.add(offset) }
938    }
939
940    /// Permission-aware wrapper around [`<*mut T>::offset`](https://doc.rust-lang.org/core/primitive.pointer.html#method.offset-1)
941    #[trusted]
942    #[erasure(<*mut T>::offset)]
943    #[requires(live.contains_range(self, offset@))]
944    #[ensures(result == self.offset_logic(offset@))]
945    unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self {
946        let _ = live;
947        unsafe { self.offset(offset) }
948    }
949}
creusot_std/std/ptr.rs

creusot_std/std/
ptr.rs
