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

creusot_std/std/
ptr.rs
