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::ptr::*;
8
9#[cfg(not(feature = "std"))]
10use alloc::boxed::Box;
11
12/// Metadata of a pointer in logic.
13///
14/// [`std::ptr::metadata`] in logic.
15#[logic(opaque)]
16pub fn metadata_logic<T: ?Sized>(_: *const T) -> <T as Pointee>::Metadata {
17    dead
18}
19
20/// Check that a value is compatible with some metadata.
21///
22/// If the value is a slice, this predicate asserts that the metadata equals the length of the slice,
23/// and that the total size of the slice is no more than `isize::MAX`. This latter property is assumed
24/// by pointer primitives such as [`slice::from_raw_parts`][from_raw_parts].
25///
26/// - For `T = [U]`, specializes to [`metadata_matches_slice`].
27/// - For `T = str`, specializes to [`metadata_matches_str`].
28/// - For `T: Sized`, specializes to `true`.
29///
30/// Why did we not make this a function `fn metadata_of(value: T) -> <T as Pointee>::Metadata`?
31/// Because this way is shorter: this corresponds to a single predicate in Why3 per type `T`.
32/// Defining a logic function that returns `usize` for slices is not so
33/// straightforward because almost every number wants to be `Int`.
34/// We would need to generate one abstract Why3 function `metadata_of : T -> Metadata`
35/// and an axiom `view_usize (metadata_of value) = len (Slice.view value)`,
36/// so two Why3 declarations instead of one.
37///
38/// [from_raw_parts]: https://doc.rust-lang.org/core/slice/fn.from_raw_parts.html
39#[logic(open, inline)]
40#[intrinsic("metadata_matches")]
41pub fn metadata_matches<T: ?Sized>(_value: T, _metadata: <T as Pointee>::Metadata) -> bool {
42    dead
43}
44
45/// Definition of [`metadata_matches`] for slices.
46#[allow(unused)]
47#[logic]
48#[intrinsic("metadata_matches_slice")]
49fn metadata_matches_slice<T>(value: [T], len: usize) -> bool {
50    pearlite! { value@.len() == len@ }
51}
52
53/// Definition of [`metadata_matches`] for string slices.
54#[allow(unused)]
55#[logic]
56#[intrinsic("metadata_matches_str")]
57fn metadata_matches_str(value: str, len: usize) -> bool {
58    pearlite! { value@.to_bytes().len() == len@ }
59}
60
61/// Whether a pointer is aligned.
62///
63/// This is a logic version of [`<*const T>::is_aligned`][is_aligned],
64/// but extended with an additional rule for `[U]`. We make use of this property
65/// in [`ghost::perm::Perm<*const T>`] to define a more precise invariant for slice pointers.
66///
67/// - For `T: Sized`, specializes to [`is_aligned_logic_sized`].
68/// - For `T = [U]`, specializes to [`is_aligned_logic_slice`].
69/// - For `T = str`, specializes to `true`.
70///
71/// [is_aligned]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned
72#[allow(unused_variables)]
73#[logic(open, inline)]
74#[intrinsic("is_aligned_logic")]
75pub fn is_aligned_logic<T: ?Sized>(ptr: *const T) -> bool {
76    dead
77}
78
79/// Definition of [`is_aligned_logic`] for `T: Sized`.
80#[allow(unused)]
81#[logic]
82#[intrinsic("is_aligned_logic_sized")]
83fn is_aligned_logic_sized<T>(ptr: *const T) -> bool {
84    ptr.is_aligned_to_logic(align_of_logic::<T>())
85}
86
87/// Definition of [`is_aligned_logic`] for `[T]`.
88#[allow(unused)]
89#[logic]
90#[intrinsic("is_aligned_logic_slice")]
91fn is_aligned_logic_slice<T>(ptr: *const [T]) -> bool {
92    ptr.is_aligned_to_logic(align_of_logic::<T>())
93}
94
95/// We conservatively model raw pointers as having an address *plus some hidden
96/// metadata*.
97///
98/// This is to account for provenance
99/// (<https://doc.rust-lang.org/std/ptr/index.html#[check(ghost)]sing-strict-provenance>) and
100/// wide pointers. See e.g.
101/// <https://doc.rust-lang.org/std/primitive.pointer.html#method.is_null>: "unsized
102/// types have many possible null pointers, as only the raw data pointer is
103/// considered, not their length, vtable, etc. Therefore, two pointers that are
104/// null may still not compare equal to each other."
105#[allow(dead_code)]
106pub struct PtrDeepModel {
107    pub addr: usize,
108    runtime_metadata: usize,
109}
110
111impl<T: ?Sized> DeepModel for *mut T {
112    type DeepModelTy = PtrDeepModel;
113    #[trusted]
114    #[logic(opaque)]
115    #[ensures(result.addr == self.addr_logic())]
116    fn deep_model(self) -> Self::DeepModelTy {
117        dead
118    }
119}
120
121impl<T: ?Sized> DeepModel for *const T {
122    type DeepModelTy = PtrDeepModel;
123    #[trusted]
124    #[logic(opaque)]
125    #[ensures(result.addr == self.addr_logic())]
126    fn deep_model(self) -> Self::DeepModelTy {
127        dead
128    }
129}
130
131pub trait PointerExt<T: ?Sized>: Sized {
132    /// _logical_ address of the pointer
133    #[logic]
134    fn addr_logic(self) -> usize;
135
136    /// `true` if the pointer is null.
137    #[logic(open, sealed)]
138    fn is_null_logic(self) -> bool {
139        self.addr_logic() == 0usize
140    }
141
142    /// Logic counterpart to [`<*const T>::is_aligned_to`][is_aligned_to]
143    ///
144    /// [is_aligned_to]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned_to
145    #[logic(open, sealed)]
146    fn is_aligned_to_logic(self, align: usize) -> bool {
147        pearlite! { self.addr_logic() & (align - 1usize) == 0usize }
148    }
149
150    /// Logic counterpart to [`<*const T>::is_aligned`][is_aligned]
151    ///
152    /// This is defined as [`is_aligned_logic`] (plus a noop coercion for `*mut T`).
153    ///
154    /// [is_aligned]: https://doc.rust-lang.org/std/primitive.pointer.html#method.is_aligned
155    #[logic]
156    fn is_aligned_logic(self) -> bool;
157}
158
159impl<T: ?Sized> PointerExt<T> for *const T {
160    #[logic]
161    #[cfg_attr(target_pointer_width = "16", builtin("creusot.prelude.Ptr$BW$.addr_logic_u16"))]
162    #[cfg_attr(target_pointer_width = "32", builtin("creusot.prelude.Ptr$BW$.addr_logic_u32"))]
163    #[cfg_attr(target_pointer_width = "64", builtin("creusot.prelude.Ptr$BW$.addr_logic_u64"))]
164    fn addr_logic(self) -> usize {
165        dead
166    }
167
168    #[logic(open, inline)]
169    fn is_aligned_logic(self) -> bool {
170        is_aligned_logic(self)
171    }
172}
173
174impl<T: ?Sized> PointerExt<T> for *mut T {
175    #[logic]
176    #[cfg_attr(target_pointer_width = "16", builtin("creusot.prelude.Ptr$BW$.addr_logic_u16"))]
177    #[cfg_attr(target_pointer_width = "32", builtin("creusot.prelude.Ptr$BW$.addr_logic_u32"))]
178    #[cfg_attr(target_pointer_width = "64", builtin("creusot.prelude.Ptr$BW$.addr_logic_u64"))]
179    fn addr_logic(self) -> usize {
180        dead
181    }
182
183    #[logic(open, inline)]
184    fn is_aligned_logic(self) -> bool {
185        is_aligned_logic(self)
186    }
187}
188
189/// Extension methods for `*const T` where `T: Sized`.
190pub trait SizedPointerExt<T>: PointerExt<T> {
191    /// Pointer offset in logic
192    ///
193    /// The current contract only describes the effect on `addr_logic` in the absence of overflow.
194    #[logic]
195    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@)]
196    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
197    fn offset_logic(self, offset: Int) -> Self;
198
199    /// Offset by zero is the identity
200    #[logic(law)]
201    #[ensures(self.offset_logic(0) == self)]
202    fn offset_logic_zero(self);
203
204    /// Offset is associative
205    #[logic(law)]
206    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
207    fn offset_logic_assoc(self, offset1: Int, offset2: Int);
208
209    /// Pointer subtraction
210    ///
211    /// Note: we don't have `ptr1 + (ptr2 - ptr1) == ptr2`, because pointer subtraction discards provenance.
212    #[logic]
213    fn sub_logic(self, rhs: Self) -> Int;
214
215    #[logic(law)]
216    #[ensures(self.sub_logic(self) == 0)]
217    fn sub_logic_refl(self);
218
219    #[logic(law)]
220    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
221    fn sub_offset_logic(self, offset: Int);
222}
223
224impl<T> SizedPointerExt<T> for *const T {
225    #[trusted]
226    #[logic(opaque)]
227    #[requires(self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@)]
228    #[ensures(result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>())]
229    fn offset_logic(self, offset: Int) -> Self {
230        dead
231    }
232
233    #[trusted]
234    #[logic(law)]
235    #[ensures(self.offset_logic(0) == self)]
236    fn offset_logic_zero(self) {}
237
238    #[trusted]
239    #[logic(law)]
240    #[ensures(self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2))]
241    fn offset_logic_assoc(self, offset1: Int, offset2: Int) {}
242
243    #[allow(unused)]
244    #[trusted]
245    #[logic(opaque)]
246    fn sub_logic(self, rhs: Self) -> Int {
247        dead
248    }
249
250    #[trusted]
251    #[logic(law)]
252    #[ensures(self.sub_logic(self) == 0)]
253    fn sub_logic_refl(self) {}
254
255    #[trusted]
256    #[logic(law)]
257    #[ensures(self.offset_logic(offset).sub_logic(self) == offset)]
258    fn sub_offset_logic(self, offset: Int) {}
259}
260
261/// Extension methods for `*const [T]`
262///
263/// `thin` and `len_logic` are wrappers around `_ as *const T` and `metadata_logic`
264/// that also pull in the `slice_ptr_ext` axiom when used.
265pub trait SlicePointerExt<T>: PointerExt<[T]> {
266    /// Remove metadata.
267    #[logic]
268    fn thin(self) -> *const T;
269
270    /// Get the metadata.
271    #[logic]
272    fn len_logic(self) -> usize;
273
274    /// Extensionality law.
275    #[logic(law)]
276    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
277    fn slice_ptr_ext(self, other: Self);
278}
279
280impl<T> SlicePointerExt<T> for *const [T] {
281    /// Convert `*const [T]` to `*const T`.
282    #[logic(open, inline)]
283    fn thin(self) -> *const T {
284        self as *const T
285    }
286
287    /// Get the length metadata of the pointer.
288    #[logic(open, inline)]
289    fn len_logic(self) -> usize {
290        pearlite! { metadata_logic(self) }
291    }
292
293    /// Extensionality of slice pointers.
294    #[trusted]
295    #[logic(law)]
296    #[ensures(self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other)]
297    fn slice_ptr_ext(self, other: Self) {}
298}
299
300extern_spec! {
301    impl<T: ?Sized> *const T {
302        #[check(ghost)]
303        #[ensures(result == self.addr_logic())]
304        fn addr(self) -> usize;
305
306        #[check(ghost)]
307        #[ensures(result == self.is_null_logic())]
308        fn is_null(self) -> bool;
309
310        #[check(ghost)]
311        #[erasure]
312        #[ensures(result == self as _)]
313        fn cast<U>(self) -> *const U {
314            self as _
315        }
316
317        #[check(terminates)]
318        #[erasure]
319        #[ensures(result == self.is_aligned_logic())]
320        fn is_aligned(self) -> bool
321            where T: Sized,
322        {
323            self.is_aligned_to(core::mem::align_of::<T>())
324        }
325
326        #[check(ghost)]
327        #[erasure]
328        #[bitwise_proof]
329        #[requires(align != 0usize && align & (align - 1usize) == 0usize)]
330        #[ensures(result == self.is_aligned_to_logic(align))]
331        fn is_aligned_to(self, align: usize) -> bool
332        {
333            if !align.is_power_of_two() {
334                ::core::panic::panic_2021!("is_aligned_to: align is not a power-of-two");
335            }
336            self.addr() & (align - 1) == 0
337        }
338    }
339
340    impl<T: ?Sized> *mut T {
341        #[check(ghost)]
342        #[ensures(result == self.addr_logic())]
343        fn addr(self) -> usize;
344
345        #[check(ghost)]
346        #[ensures(result == self.is_null_logic())]
347        fn is_null(self) -> bool;
348
349        #[check(ghost)]
350        #[erasure]
351        #[ensures(result == self as _)]
352        fn cast<U>(self) -> *mut U {
353            self as _
354        }
355
356        #[check(terminates)]
357        #[erasure]
358        #[ensures(result == self.is_aligned_logic())]
359        fn is_aligned(self) -> bool
360            where T: Sized,
361        {
362            self.is_aligned_to(core::mem::align_of::<T>())
363        }
364
365        #[check(ghost)]
366        #[erasure]
367        #[bitwise_proof]
368        #[requires(align != 0usize && align & (align - 1usize) == 0usize)]
369        #[ensures(result == self.is_aligned_to_logic(align))]
370        fn is_aligned_to(self, align: usize) -> bool
371        {
372            if !align.is_power_of_two() {
373                ::core::panic::panic_2021!("is_aligned_to: align is not a power-of-two");
374            }
375            self.addr() & (align - 1) == 0
376        }
377    }
378
379    impl<T> *const [T] {
380        #[ensures(result == metadata_logic(self))]
381        fn len(self) -> usize;
382    }
383
384    impl<T> *mut [T] {
385        #[ensures(result == metadata_logic(self))]
386        fn len(self) -> usize;
387    }
388
389    mod core {
390        mod ptr {
391            #[check(ghost)]
392            #[ensures(result.is_null_logic())]
393            fn null<T>() -> *const T
394            where
395                T: core::ptr::Thin + ?Sized;
396
397            #[check(ghost)]
398            #[ensures(result.is_null_logic())]
399            fn null_mut<T>() -> *mut T
400            where
401                T: core::ptr::Thin + ?Sized;
402
403            #[check(ghost)]
404            #[ensures(result == (p.addr_logic() == q.addr_logic()))]
405            fn addr_eq<T, U>(p: *const T, q: *const U) -> bool
406            where
407                T: ?Sized, U: ?Sized;
408
409            #[check(ghost)]
410            #[ensures(result == metadata_logic(ptr))]
411            fn metadata<T: ?Sized>(ptr: *const T) -> <T as Pointee>::Metadata;
412
413            // Postulate `check(ghost)`.
414            // It is used in a `#[trusted]` primitive in `peano`.
415            #[check(ghost)]
416            #[ensures(false)]
417            unsafe fn read_volatile<T>(src: *const T) -> T;
418
419            #[ensures(result as *const T == data && result.len_logic() == len)]
420            fn slice_from_raw_parts<T>(data: *const T, len: usize) -> *const [T];
421
422            #[ensures(result as *mut T == data && result.len_logic() == len)]
423            fn slice_from_raw_parts_mut<T>(data: *mut T, len: usize) -> *mut [T];
424        }
425    }
426
427    impl<T> Clone for *mut T {
428        #[check(ghost)]
429        #[ensures(result == *self)]
430        fn clone(&self) -> *mut T {
431            *self
432        }
433    }
434
435    impl<T> Clone for *const T {
436        #[check(ghost)]
437        #[ensures(result == *self)]
438        fn clone(&self) -> *const T {
439            *self
440        }
441    }
442}
443
444impl<T: ?Sized> Container for *const T {
445    type Value = T;
446
447    #[logic(open, inline)]
448    fn is_disjoint(&self, self_val: &T, other: &Self, other_val: &T) -> bool {
449        pearlite! {
450            size_of_val_logic(*self_val) != 0 && size_of_val_logic(*other_val) != 0 ==>
451            self.addr_logic() != other.addr_logic()
452        }
453    }
454}
455
456impl<T: ?Sized> Invariant for Perm<*const T> {
457    #[logic(open, prophetic)]
458    fn invariant(self) -> bool {
459        pearlite! {
460            !self.ward().is_null_logic()
461                && self.ptr_is_aligned_opaque()
462                && metadata_matches(*self.val(), metadata_logic(*self.ward()))
463                // Allocations can never be larger than `isize` (source: https://doc.rust-lang.org/std/ptr/index.html#allocation)
464                && size_of_val_logic(*self.val()) <= isize::MAX@
465                // The allocation fits in the address space
466                // (this is needed to verify (a `Perm` variant of) `<*const T>::add`, which checks this condition)
467                && self.ward().addr_logic()@ + size_of_val_logic(*self.val()) <= usize::MAX@
468                && inv(self.val())
469        }
470    }
471}
472
473impl<T: ?Sized> Perm<*const T> {
474    /// Creates a new `Perm<*const T>` and associated `*const` by allocating a new memory
475    /// cell initialized with `v`.
476    #[check(terminates)] // can overflow the number of available pointer adresses
477    #[ensures(*result.1.ward() == result.0 && *result.1.val() == v)]
478    pub fn new(v: T) -> (*mut T, Ghost<Box<Perm<*const T>>>)
479    where
480        T: Sized,
481    {
482        Self::from_box(Box::new(v))
483    }
484
485    /// Creates a ghost `Perm<*const T>` and associated `*const` from an existing [`Box`].
486    #[trusted]
487    #[check(terminates)] // can overflow the number of available pointer adresses
488    #[ensures(*result.1.ward() == result.0 && *result.1.val() == *val)]
489    #[erasure(Box::into_raw)]
490    pub fn from_box(val: Box<T>) -> (*mut T, Ghost<Box<Perm<*const T>>>) {
491        (Box::into_raw(val), Ghost::conjure())
492    }
493
494    /// Decompose a shared reference into a raw pointer and a ghost `Perm<*const T>`.
495    ///
496    /// # Erasure
497    ///
498    /// This function erases to a raw reborrow of a reference.
499    ///
500    /// ```ignore
501    /// Perm::from_ref(r)
502    /// // erases to
503    /// r as *const T  // or *mut T (both are allowed)
504    /// ```
505    #[trusted]
506    #[check(terminates)] // can overflow the number of available pointer adresses
507    #[ensures(*result.1.ward() == result.0)]
508    #[ensures(*result.1.val() == *r)]
509    #[intrinsic("perm_from_ref")]
510    pub fn from_ref(r: &T) -> (*const T, Ghost<&Perm<*const T>>) {
511        (r, Ghost::conjure())
512    }
513
514    /// Decompose a mutable reference into a raw pointer and a ghost `Perm<*const T>`.
515    ///
516    /// # Erasure
517    ///
518    /// This function erases to a raw reborrow of a reference.
519    ///
520    /// ```ignore
521    /// Perm::from_mut(r)
522    /// // erases to
523    /// r as *const T  // or *mut T (both are allowed)
524    /// ```
525    #[trusted]
526    #[check(terminates)] // can overflow the number of available pointer adresses
527    #[ensures(*result.1.ward() == result.0)]
528    #[ensures(*result.1.val() == *r)]
529    #[ensures(*(^result.1.inner_logic()).val() == ^r)]
530    #[intrinsic("perm_from_mut")]
531    pub fn from_mut(r: &mut T) -> (*mut T, Ghost<&mut Perm<*const T>>) {
532        (r, Ghost::conjure())
533    }
534
535    /// Immutably borrows the underlying `T`.
536    ///
537    /// # Safety
538    ///
539    /// Safety requirements are the same as a direct dereference: `&*ptr`.
540    ///
541    /// Creusot will check that all calls to this function are indeed safe: see the
542    /// [type documentation](Perm).
543    ///
544    /// # Erasure
545    ///
546    /// This function erases to a cast from raw pointer to shared reference.
547    ///
548    /// ```ignore
549    /// Perm::as_ref(ptr, own)
550    /// // erases to
551    /// & *ptr
552    /// ```
553    #[trusted]
554    #[check(terminates)]
555    #[requires(ptr == *own.ward())]
556    #[ensures(*result == *own.val())]
557    #[allow(unused_variables)]
558    #[intrinsic("perm_as_ref")]
559    pub unsafe fn as_ref(ptr: *const T, own: Ghost<&Perm<*const T>>) -> &T {
560        unsafe { &*ptr }
561    }
562
563    /// Mutably borrows the underlying `T`.
564    ///
565    /// # Safety
566    ///
567    /// Safety requirements are the same as a direct dereference: `&mut *ptr`.
568    ///
569    /// Creusot will check that all calls to this function are indeed safe: see the
570    /// [type documentation](Perm).
571    ///
572    /// # Erasure
573    ///
574    /// This function erases to a cast from raw pointer to mutable reference.
575    ///
576    /// ```ignore
577    /// Perm::as_mut(ptr, own)
578    /// // erases to
579    /// &mut *ptr
580    /// ```
581    #[trusted]
582    #[check(terminates)]
583    #[allow(unused_variables)]
584    #[requires(ptr as *const T == *own.ward())]
585    #[ensures(*result == *own.val())]
586    #[ensures((^own).ward() == own.ward())]
587    #[ensures(*(^own).val() == ^result)]
588    #[intrinsic("perm_as_mut")]
589    pub unsafe fn as_mut(ptr: *mut T, own: Ghost<&mut Perm<*const T>>) -> &mut T {
590        unsafe { &mut *ptr }
591    }
592
593    /// Transfers ownership of `own` back into a [`Box`].
594    ///
595    /// # Safety
596    ///
597    /// Safety requirements are the same as [`Box::from_raw`].
598    ///
599    /// Creusot will check that all calls to this function are indeed safe: see the
600    /// [type documentation](Perm).
601    #[trusted]
602    #[check(terminates)]
603    #[requires(ptr as *const T == *own.ward())]
604    #[ensures(*result == *own.val())]
605    #[allow(unused_variables)]
606    #[erasure(Box::from_raw)]
607    pub unsafe fn to_box(ptr: *mut T, own: Ghost<Box<Perm<*const T>>>) -> Box<T> {
608        unsafe { Box::from_raw(ptr) }
609    }
610
611    /// Deallocates the memory pointed by `ptr`.
612    ///
613    /// # Safety
614    ///
615    /// Safety requirements are the same as [`Box::from_raw`].
616    ///
617    /// Creusot will check that all calls to this function are indeed safe: see the
618    /// [type documentation](Perm).
619    #[check(terminates)]
620    #[requires(ptr as *const T == *own.ward())]
621    pub unsafe fn drop(ptr: *mut T, own: Ghost<Box<Perm<*const T>>>) {
622        let _ = unsafe { Self::to_box(ptr, own) };
623    }
624
625    /// The pointer of a `Perm<*const T>` is always aligned.
626    #[check(ghost)]
627    #[ensures(self.ward().is_aligned_logic())]
628    pub fn ptr_is_aligned_lemma(&self) {}
629
630    /// Opaque wrapper around [`std::ptr::is_aligned_logic`].
631    /// We use this to hide alignment logic by default in `invariant` because it confuses SMT solvers sometimes.
632    /// The underlying property is exposed by [`Perm::ptr_is_aligned_lemma`].
633    #[logic(open(self))]
634    pub fn ptr_is_aligned_opaque(self) -> bool {
635        self.ward().is_aligned_logic()
636    }
637}
creusot_std/std/ptr.rs

creusot_std/std/
ptr.rs
