creusot_contracts/ghost/
ptr_own.rs

1//! Raw pointers with ghost code
2
3use std::marker::PhantomData;
4
5use crate::prelude::*;
6#[cfg(creusot)]
7use crate::std::{
8    mem::{size_of_logic, size_of_val_logic},
9    ptr::{metadata_logic, metadata_matches},
10};
11
12/// Token that represents the ownership of a memory cell
13///
14/// A `PtrOwn` value only exists in the ghost world, but can be used
15/// in combination with a corresponding `*const` to access and modify memory.
16///
17/// A warning regarding memory leaks: dropping a `Ghost<PtrOwn<T>>` (we only
18/// ever handle ghost `PtrOwn` values) cannot deallocate the memory
19/// corresponding to the pointer because it is a ghost value. One must thus
20/// remember to explicitly call [`drop`] in order to free the memory tracked by a
21/// `PtrOwn` token.
22///
23/// # Safety
24///
25/// When using Creusot to verify the code, all methods should be safe to call. Indeed,
26/// Creusot ensures that every operation on the inner value uses the right [`PtrOwn`] object
27/// created by [`PtrOwn::new`], ensuring safety in a manner similar to [ghost_cell](https://docs.rs/ghost-cell/latest/ghost_cell/).
28///
29/// # `#[check(terminates)]`
30///
31/// `PtrOwn` methods, particularly constructors (`new`, `from_box`, `from_ref`,
32/// `from_mut`), are marked `check(terminates)` rather than `check(ghost)`
33/// to prevent two things from happening in ghost code:
34/// 1. running out of pointer addresses;
35/// 2. allocating too large objects.
36///
37/// Note that we already can't guard against these issues in program code.
38/// But preventing them in ghost code is even more imperative to ensure soundness.
39///
40/// Specifically, creating too many pointers contradicts the [`PtrOwn::disjoint_lemma`],
41/// and allocating too large objects contradicts the [`PtrOwn::invariant`] that
42/// allocations have size at most `isize::MAX`.
43#[allow(dead_code)]
44#[opaque]
45pub struct PtrOwn<T: ?Sized>(PhantomData<T>);
46
47impl<T: ?Sized> PtrOwn<T> {
48    /// The raw pointer whose ownership is tracked by this `PtrOwn`
49    #[logic(opaque)]
50    pub fn ptr(self) -> *const T {
51        dead
52    }
53
54    /// The value currently stored at address [`self.ptr()`](Self::ptr)
55    #[logic(opaque)]
56    pub fn val<'a>(self) -> &'a T {
57        dead
58    }
59}
60
61impl<T: ?Sized> Invariant for PtrOwn<T> {
62    #[logic(open, prophetic)]
63    fn invariant(self) -> bool {
64        pearlite! {
65            !self.ptr().is_null_logic()
66                && self.ptr_is_aligned_opaque()
67                && metadata_matches(*self.val(), metadata_logic(self.ptr()))
68                // Allocations can never be larger than `isize` (source: https://doc.rust-lang.org/std/ptr/index.html#allocation)
69                && size_of_val_logic(*self.val()) <= isize::MAX@
70                // The allocation fits in the address space
71                // (this is needed to verify (a `PtrOwn` variant of) `<*const T>::add`, which checks this condition)
72                && self.ptr().addr_logic()@ + size_of_val_logic(*self.val()) <= usize::MAX@
73                && inv(self.val())
74        }
75    }
76}
77
78impl<T> PtrOwn<T> {
79    /// Creates a new `PtrOwn` and associated `*const` by allocating a new memory
80    /// cell initialized with `v`.
81    #[check(terminates)] // can overflow the number of available pointer adresses
82    #[ensures(result.1.ptr() == result.0 && *result.1.val() == v)]
83    pub fn new(v: T) -> (*mut T, Ghost<PtrOwn<T>>) {
84        Self::from_box(Box::new(v))
85    }
86
87    /// If one owns two `PtrOwn`s for non-zero sized types, then they are for different pointers.
88    #[trusted]
89    #[check(ghost)]
90    #[requires(size_of_logic::<T>() != 0)]
91    #[ensures(own1.ptr().addr_logic() != own2.ptr().addr_logic())]
92    #[ensures(*own1 == ^own1)]
93    #[allow(unused_variables)]
94    pub fn disjoint_lemma(own1: &mut PtrOwn<T>, own2: &PtrOwn<T>) {}
95}
96
97impl<T: ?Sized> PtrOwn<T> {
98    /// Creates a ghost `PtrOwn` and associated `*const` from an existing [`Box`].
99    #[trusted]
100    #[check(terminates)] // can overflow the number of available pointer adresses
101    #[ensures(result.1.ptr() == result.0 && *result.1.val() == *val)]
102    #[erasure(Box::into_raw)]
103    pub fn from_box(val: Box<T>) -> (*mut T, Ghost<PtrOwn<T>>) {
104        (Box::into_raw(val), Ghost::conjure())
105    }
106
107    /// Decompose a shared reference into a raw pointer and a ghost `PtrOwn`.
108    ///
109    /// # Erasure
110    ///
111    /// This function erases to a raw reborrow of a reference.
112    ///
113    /// ```ignore
114    /// PtrOwn::from_ref(r)
115    /// // erases to
116    /// r as *const T  // or *mut T (both are allowed)
117    /// ```
118    #[trusted]
119    #[check(terminates)] // can overflow the number of available pointer adresses
120    #[ensures(result.1.ptr() == result.0)]
121    #[ensures(*result.1.val() == *r)]
122    #[intrinsic("ptr_own_from_ref")]
123    pub fn from_ref(r: &T) -> (*const T, Ghost<&PtrOwn<T>>) {
124        (r, Ghost::conjure())
125    }
126
127    /// Decompose a mutable reference into a raw pointer and a ghost `PtrOwn`.
128    ///
129    /// # Erasure
130    ///
131    /// This function erases to a raw reborrow of a reference.
132    ///
133    /// ```ignore
134    /// PtrOwn::from_mut(r)
135    /// // erases to
136    /// r as *const T  // or *mut T (both are allowed)
137    /// ```
138    #[trusted]
139    #[check(terminates)] // can overflow the number of available pointer adresses
140    #[ensures(result.1.ptr() == result.0)]
141    #[ensures(*result.1.val() == *r)]
142    #[ensures(*(^result.1.inner_logic()).val() == ^r)]
143    #[intrinsic("ptr_own_from_mut")]
144    pub fn from_mut(r: &mut T) -> (*mut T, Ghost<&mut PtrOwn<T>>) {
145        (r, Ghost::conjure())
146    }
147
148    /// Immutably borrows the underlying `T`.
149    ///
150    /// # Safety
151    ///
152    /// Safety requirements are the same as a direct dereference: `&*ptr`.
153    ///
154    /// Creusot will check that all calls to this function are indeed safe: see the
155    /// [type documentation](PtrOwn).
156    ///
157    /// # Erasure
158    ///
159    /// This function erases to a cast from raw pointer to shared reference.
160    ///
161    /// ```ignore
162    /// PtrOwn::as_ref(ptr, own)
163    /// // erases to
164    /// & *ptr
165    /// ```
166    #[trusted]
167    #[check(terminates)]
168    #[requires(ptr == own.ptr())]
169    #[ensures(*result == *own.val())]
170    #[allow(unused_variables)]
171    #[intrinsic("ptr_own_as_ref")]
172    pub unsafe fn as_ref(ptr: *const T, own: Ghost<&PtrOwn<T>>) -> &T {
173        unsafe { &*ptr }
174    }
175
176    /// Mutably borrows the underlying `T`.
177    ///
178    /// # Safety
179    ///
180    /// Safety requirements are the same as a direct dereference: `&mut *ptr`.
181    ///
182    /// Creusot will check that all calls to this function are indeed safe: see the
183    /// [type documentation](PtrOwn).
184    ///
185    /// # Erasure
186    ///
187    /// This function erases to a cast from raw pointer to mutable reference.
188    ///
189    /// ```ignore
190    /// PtrOwn::as_mut(ptr, own)
191    /// // erases to
192    /// &mut *ptr
193    /// ```
194    #[trusted]
195    #[check(terminates)]
196    #[allow(unused_variables)]
197    #[requires(ptr as *const T == own.ptr())]
198    #[ensures(*result == *own.val())]
199    #[ensures((^own).ptr() == own.ptr())]
200    #[ensures(*(^own).val() == ^result)]
201    #[intrinsic("ptr_own_as_mut")]
202    pub unsafe fn as_mut(ptr: *mut T, own: Ghost<&mut PtrOwn<T>>) -> &mut T {
203        unsafe { &mut *ptr }
204    }
205
206    /// Transfers ownership of `own` back into a [`Box`].
207    ///
208    /// # Safety
209    ///
210    /// Safety requirements are the same as [`Box::from_raw`].
211    ///
212    /// Creusot will check that all calls to this function are indeed safe: see the
213    /// [type documentation](PtrOwn).
214    #[trusted]
215    #[check(terminates)]
216    #[requires(ptr as *const T == own.ptr())]
217    #[ensures(*result == *own.val())]
218    #[allow(unused_variables)]
219    #[erasure(Box::from_raw)]
220    pub unsafe fn to_box(ptr: *mut T, own: Ghost<PtrOwn<T>>) -> Box<T> {
221        unsafe { Box::from_raw(ptr) }
222    }
223
224    /// Deallocates the memory pointed by `ptr`.
225    ///
226    /// # Safety
227    ///
228    /// Safety requirements are the same as [`Box::from_raw`].
229    ///
230    /// Creusot will check that all calls to this function are indeed safe: see the
231    /// [type documentation](PtrOwn).
232    #[check(terminates)]
233    #[requires(ptr as *const T == own.ptr())]
234    pub unsafe fn drop(ptr: *mut T, own: Ghost<PtrOwn<T>>) {
235        let _ = unsafe { Self::to_box(ptr, own) };
236    }
237
238    /// The pointer of a `PtrOwn` is always aligned.
239    #[check(ghost)]
240    #[ensures(self.ptr().is_aligned_logic())]
241    pub fn ptr_is_aligned_lemma(&self) {}
242
243    /// Opaque wrapper around [`std::ptr::is_aligned_logic`].
244    /// We use this to hide alignment logic by default in `invariant` because it confuses SMT solvers sometimes.
245    /// The underlying property is exposed by [`PtrOwn::ptr_is_aligned_lemma`].
246    #[logic(open(self))]
247    pub fn ptr_is_aligned_opaque(self) -> bool {
248        self.ptr().is_aligned_logic()
249    }
250}
creusot_contracts/ghost/ptr_own.rs

creusot_contracts/ghost/
ptr_own.rs
