vstd/
simple_pptr.rs

1use super::layout::*;
2use super::prelude::*;
3use super::raw_ptr;
4use super::raw_ptr::*;
5use core::marker::PhantomData;
6
7verus! {
8
9/// `PPtr` (which stands for "permissioned pointer")
10/// is a wrapper around a raw pointer to a heap-allocated `V`.
11/// This is designed to be simpler to use that Verus's
12/// [more general pointer support](`crate::raw_ptr`),
13/// but also to serve as a better introductory point.
14/// Historically, `PPtr` was positioned as a "trusted primitive" of Verus,
15/// but now, it is implemented and verified from the more general pointer support,
16/// which operates on similar principles, but which is much precise to Rust's
17/// pointer semantics.
18///
19/// A `PPtr` is equvialent to its `usize`-based address. The type paramter `V` technically
20/// doesn't matter, and you can freely convert between `PPtr<V>` and `PPtr<W>` by casting
21/// to and from the `usize` address. What _really_ matters is the type paramter of the
22/// `PointsTo<V>`.
23///
24/// In order to access (read or write) the value behind the pointer, the user needs
25/// a special _ghost permission token_, [`PointsTo<V>`](PointsTo). This object is `tracked`,
26/// which means that it is "only a proof construct" that does not appear in compiled code,
27/// but its uses _are_ checked by the borrow-checker. This ensures memory safety,
28/// data-race-freedom, prohibits use-after-free, etc.
29///
30/// ### PointsTo objects.
31///
32/// The [`PointsTo`] object represents both the ability to access (read or write)
33/// the data behind the pointer _and_ the ability to free it
34/// (return it to the memory allocator).
35///
36/// The `perm: PointsTo<V>` object tracks two pieces of data:
37///  * [`perm.pptr()`](PointsTo::pptr) is the pointer that the permission is associated to.
38///  * [`perm.mem_contents()`](PointsTo::mem_contents) is the memory contents, which is one of either:
39///     * [`MemContents::Uninit`](raw_ptr::MemContents::Uninit) if the memory pointed-to by
40///       by the pointer is uninitialized.
41///     * [`MemContents::Init(v)`](raw_ptr::MemContents::Init) if the memory points-to the
42///       the value `v`.
43///
44/// Your access to the `PointsTo` object determines what operations you can safely perform
45/// with the pointer:
46///  * You can _read_ from the pointer as long as you have read access to the `PointsTo` object,
47///     e.g., `&PointsTo<V>`.
48///  * You can _write_ to the pointer as long as you have mutable access to the `PointsTo` object,
49///     e.g., `&mut PointsTo<V>`
50///  * You can call `free` to deallocate the memory as long as you have full onwership
51///     of the `PointsTo` object (i.e., the ability to move it).
52///
53/// For those familiar with separation logic, the `PointsTo` object plays a role
54/// similar to that of the "points-to" operator, _ptr_ ↦ _value_.
55///
56/// ### Example
57///
58/// ```rust,ignored
59/// fn main() {
60///     unsafe {
61///         // ALLOCATE
62///         // p: PPtr<u64>, points_to: PointsTo<u64>
63///         let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();
64///
65///         assert(points_to.mem_contents() === MemContents::Uninit);
66///         assert(points_to.pptr() == p);
67///
68///         // unsafe { *p = 5; }
69///         p.write(Tracked(&mut points_to), 5);
70///
71///         assert(points_to.mem_contents() === MemContents::Init(5));
72///         assert(points_to.pptr() == p);
73///
74///         // let x = unsafe { *p };
75///         let x = p.read(Tracked(&points_to));
76///
77///         assert(x == 5);
78///
79///         // DEALLOCATE
80///         let y = p.into_inner(Tracked(points_to));
81///
82///         assert(y == 5);
83///     }
84/// }
85/// ```
86///
87/// ### Examples of incorrect usage
88///
89/// The following code has a use-after-free bug, and it is rejected by Verus because
90/// it fails to satisfy Rust's ownership-checker.
91///
92/// ```rust,ignored
93/// fn main() {
94///     unsafe {
95///         // ALLOCATE
96///         // p: PPtr<u64>, points_to: PointsTo<u64>
97///         let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();
98///
99///         // unsafe { *p = 5; }
100///         p.write(Tracked(&mut points_to), 5);
101///
102///         // let x = unsafe { *p };
103///         let x = p.read(Tracked(&points_to));
104///
105///         // DEALLOCATE
106///         p.free(Tracked(points_to));                 // `points_to` is moved here
107///
108///         // READ-AFTER-FREE
109///         let x2 = p.read(Tracked(&mut points_to));   // so it can't be used here
110///     }
111/// }
112/// ```
113///
114/// The following doesn't violate Rust's ownership-checking, but it "mixes up" the `PointsTo`
115/// objects, attempting to use the wrong `PointsTo` for the given pointer.
116/// This violates the precondition on [`p.read()`](PPtr::read).
117///
118/// ```rust,ignored
119/// fn main() {
120///     unsafe {
121///         // ALLOCATE p
122///         let (p, Tracked(mut perm_p)) = PPtr::<u64>::empty();
123///
124///         // ALLOCATE q
125///         let (q, Tracked(mut perm_q)) = PPtr::<u64>::empty();
126///
127///         // DEALLOCATE p
128///         p.free(Tracked(perm_p));
129///
130///         // READ-AFTER-FREE (read from p, try to use q's permission object)
131///         let x = p.read(Tracked(&mut perm_q));
132///     }
133/// }
134/// ```
135///
136/// ### Differences from `PCell`.
137///
138/// `PPtr` is similar to [`cell::PCell`](crate::cell::PCell), but has a few key differences:
139///  * In `PCell<V>`, the type `V` is placed internally to the `PCell`, whereas with `PPtr`,
140///    the type `V` is placed at some location on the heap.
141///  * Since `PPtr` is just a pointer (represented by an integer), it can be `Copy`.
142///  * The `ptr::PointsTo` token represents not just the permission to read/write
143///    the contents, but also to deallocate.
144///
145/// ### Simplifications relative to more general pointer API
146///
147///  * Pointers are only represented by addresses and don't have a general notion of provenance
148///  * Pointers are untyped (only `PointsTo` is typed).
149///  * The `PointsTo` also encapsulates the permission to free a pointer.
150///  * `PointsTo` tokens are non-fungible. They can't be broken up or made variable-sized.
151// We want PPtr's fields to be public so the solver knows that equality of addresses
152// implies equality of PPtrs
153pub struct PPtr<V>(pub usize, pub PhantomData<V>);
154
155/// A `tracked` ghost object that gives the user permission to dereference a pointer
156/// for reading or writing, or to free the memory at that pointer.
157///
158/// The meaning of a `PointsTo` object is given by the data in its
159/// `View` object, [`PointsToData`].
160///
161/// See the [`PPtr`] documentation for more details.
162pub tracked struct PointsTo<V> {
163    points_to: raw_ptr::PointsTo<V>,
164    exposed: raw_ptr::IsExposed,
165    dealloc: Option<raw_ptr::Dealloc>,
166}
167
168#[verusfmt::skip]
169broadcast use {
170    super::raw_ptr::group_raw_ptr_axioms,
171    super::set_lib::group_set_lib_default,
172    super::set::group_set_axioms};
173
174impl<V> PPtr<V> {
175    /// Use `addr()` instead
176    #[verifier::inline]
177    pub open spec fn spec_addr(p: PPtr<V>) -> usize {
178        p.0
179    }
180
181    /// Cast a pointer to an integer.
182    #[inline(always)]
183    #[verifier::when_used_as_spec(spec_addr)]
184    pub fn addr(self) -> (u: usize)
185        ensures
186            u == self.addr(),
187    {
188        self.0
189    }
190
191    /// Cast an integer to a pointer.
192    ///
193    /// Note that this does _not_ require or ensure that the pointer is valid.
194    /// Of course, if the user creates an invalid pointer, they would still not be able to
195    /// create a valid [`PointsTo`] token for it, and thus they would never
196    /// be able to access the data behind the pointer.
197    ///
198    /// This is analogous to normal Rust, where casting to a pointer is always possible,
199    /// but dereferencing a pointer is an `unsafe` operation.
200    /// With PPtr, casting to a pointer is likewise always possible,
201    /// while dereferencing it is only allowed when the right preconditions are met.
202    #[inline(always)]
203    pub fn from_addr(u: usize) -> (s: Self)
204        ensures
205            u == s.addr(),
206    {
207        PPtr(u, PhantomData)
208    }
209
210    #[doc(hidden)]
211    #[inline(always)]
212    pub fn from_usize(u: usize) -> (s: Self)
213        ensures
214            u == s.addr(),
215    {
216        PPtr(u, PhantomData)
217    }
218}
219
220impl<V> PointsTo<V> {
221    #[verifier::inline]
222    pub open spec fn pptr(&self) -> PPtr<V> {
223        PPtr(self.addr(), PhantomData)
224    }
225
226    pub closed spec fn addr(self) -> usize {
227        self.points_to.ptr().addr()
228    }
229
230    #[verifier::type_invariant]
231    closed spec fn wf(self) -> bool {
232        &&& self.points_to.ptr()@.provenance == self.exposed.provenance()
233        &&& match self.dealloc {
234            Some(dealloc) => {
235                &&& dealloc.addr() == self.points_to.ptr().addr()
236                &&& dealloc.size() == size_of::<V>()
237                &&& dealloc.align() == align_of::<V>()
238                &&& dealloc.provenance() == self.points_to.ptr()@.provenance
239                &&& size_of::<V>() > 0
240            },
241            None => { size_of::<V>() == 0 },
242        }
243        &&& self.points_to.ptr().addr() != 0
244    }
245
246    pub closed spec fn mem_contents(&self) -> MemContents<V> {
247        self.points_to.opt_value()
248    }
249
250    #[doc(hidden)]
251    #[verifier::inline]
252    pub open spec fn opt_value(&self) -> MemContents<V> {
253        self.mem_contents()
254    }
255
256    #[verifier::inline]
257    pub open spec fn is_init(&self) -> bool {
258        self.mem_contents().is_init()
259    }
260
261    #[verifier::inline]
262    pub open spec fn is_uninit(&self) -> bool {
263        self.mem_contents().is_uninit()
264    }
265
266    #[verifier::inline]
267    pub open spec fn value(&self) -> V
268        recommends
269            self.is_init(),
270    {
271        self.mem_contents().value()
272    }
273
274    /// Guarantee that the `PointsTo` points to a non-null address.
275    pub proof fn is_nonnull(tracked &self)
276        ensures
277            self.addr() != 0,
278    {
279        use_type_invariant(self);
280    }
281
282    /// "Forgets" about the value stored behind the pointer.
283    /// Updates the `PointsTo` value to [`MemContents::Uninit`](MemContents::Uninit).
284    /// Note that this is a `proof` function, i.e., it is operationally a no-op in executable code.
285    pub proof fn leak_contents(tracked &mut self)
286        ensures
287            self.pptr() == old(self).pptr(),
288            self.is_uninit(),
289    {
290        use_type_invariant(&*self);
291        self.points_to.leak_contents();
292    }
293
294    /// Guarantees that two distinct `PointsTo<V>` objects point to disjoint ranges of memory.
295    /// If both S and V are non-zero-sized, then this also implies the pointers
296    /// have distinct addresses.
297    pub proof fn is_disjoint<S>(tracked &mut self, tracked other: &PointsTo<S>)
298        ensures
299            *old(self) == *self,
300            self.addr() + size_of::<V>() <= other.addr() || other.addr() + size_of::<S>()
301                <= self.addr(),
302    {
303        use_type_invariant(&*self);
304        self.points_to.is_disjoint(&other.points_to);
305    }
306
307    /// Guarantees that two distinct, non-ZST `PointsTo<V>` objects point to different
308    /// addresses. This is a corollary of [`PointsTo::is_disjoint`].
309    pub proof fn is_distinct<S>(tracked &mut self, tracked other: &PointsTo<S>)
310        requires
311            size_of::<V>() != 0,
312            size_of::<S>() != 0,
313        ensures
314            *old(self) == *self,
315            self.addr() != other.addr(),
316    {
317        use_type_invariant(&*self);
318        self.points_to.is_disjoint(&other.points_to);
319    }
320}
321
322impl<V> Clone for PPtr<V> {
323    fn clone(&self) -> (res: Self)
324        ensures
325            res == *self,
326    {
327        PPtr(self.0, PhantomData)
328    }
329}
330
331impl<V> Copy for PPtr<V> {
332
333}
334
335impl<V> PPtr<V> {
336    /// Allocates heap memory for type `V`, leaving it uninitialized.
337    #[cfg(feature = "std")]
338    pub fn empty() -> (pt: (PPtr<V>, Tracked<PointsTo<V>>))
339        ensures
340            pt.1@.pptr() == pt.0,
341            pt.1@.is_uninit(),
342        opens_invariants none
343    {
344        layout_for_type_is_valid::<V>();
345        if core::mem::size_of::<V>() != 0 {
346            let (p, Tracked(points_to_raw), Tracked(dealloc)) = allocate(
347                core::mem::size_of::<V>(),
348                core::mem::align_of::<V>(),
349            );
350            let Tracked(exposed) = expose_provenance(p);
351            let tracked points_to = points_to_raw.into_typed::<V>(p.addr());
352            proof {
353                points_to.is_nonnull();
354            }
355            let tracked pt = PointsTo { points_to, exposed, dealloc: Some(dealloc) };
356            let pptr = PPtr(p as usize, PhantomData);
357
358            return (pptr, Tracked(pt));
359        } else {
360            let p = core::mem::align_of::<V>();
361            assert(p % p == 0) by (nonlinear_arith)
362                requires
363                    p != 0,
364            ;
365            let tracked emp = PointsToRaw::empty(Provenance::null());
366            let tracked points_to = emp.into_typed(p);
367            let tracked pt = PointsTo { points_to, exposed: IsExposed::null(), dealloc: None };
368            let pptr = PPtr(p, PhantomData);
369
370            return (pptr, Tracked(pt));
371        }
372    }
373
374    /// Allocates heap memory for type `V`, leaving it initialized
375    /// with the given value `v`.
376    #[cfg(feature = "std")]
377    pub fn new(v: V) -> (pt: (PPtr<V>, Tracked<PointsTo<V>>))
378        ensures
379            pt.1@.pptr() == pt.0,
380            pt.1@.mem_contents() == MemContents::Init(v),
381        opens_invariants none
382    {
383        let (p, Tracked(mut pt)) = PPtr::<V>::empty();
384        p.put(Tracked(&mut pt), v);
385        (p, Tracked(pt))
386    }
387
388    /// Free the memory pointed to be `perm`.
389    /// Requires the memory to be uninitialized.
390    ///
391    /// This consumes `perm`, since it will no longer be safe to access
392    /// that memory location.
393    pub fn free(self, Tracked(perm): Tracked<PointsTo<V>>)
394        requires
395            perm.pptr() == self,
396            perm.is_uninit(),
397        opens_invariants none
398    {
399        proof {
400            use_type_invariant(&perm);
401        }
402        if core::mem::size_of::<V>() != 0 {
403            let ptr: *mut u8 = with_exposed_provenance(self.0, Tracked(perm.exposed));
404            let tracked PointsTo { points_to, dealloc: dea, exposed } = perm;
405            let tracked points_to_raw = points_to.into_raw();
406            deallocate(
407                ptr,
408                core::mem::size_of::<V>(),
409                core::mem::align_of::<V>(),
410                Tracked(points_to_raw),
411                Tracked(dea.tracked_unwrap()),
412            );
413        }
414    }
415
416    /// Free the memory pointed to be `perm` and return the
417    /// value that was previously there.
418    /// Requires the memory to be initialized.
419    /// This consumes the [`PointsTo`] token, since the user is giving up
420    /// access to the memory by freeing it.
421    #[inline(always)]
422    pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> (v: V)
423        requires
424            perm.pptr() == self,
425            perm.is_init(),
426        ensures
427            v == perm.value(),
428        opens_invariants none
429    {
430        let tracked mut perm = perm;
431        let v = self.take(Tracked(&mut perm));
432        self.free(Tracked(perm));
433        v
434    }
435
436    /// Moves `v` into the location pointed to by the pointer `self`.
437    /// Requires the memory to be uninitialized, and leaves it initialized.
438    ///
439    /// In the ghost perspective, this updates `perm.mem_contents()`
440    /// from `MemContents::Uninit` to `MemContents::Init(v)`.
441    #[inline(always)]
442    pub fn put(self, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V)
443        requires
444            old(perm).pptr() == self,
445            old(perm).mem_contents() == MemContents::Uninit::<V>,
446        ensures
447            perm.pptr() == old(perm).pptr(),
448            perm.mem_contents() == MemContents::Init(v),
449        opens_invariants none
450        no_unwind
451    {
452        proof {
453            use_type_invariant(&*perm);
454        }
455        let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
456        ptr_mut_write(ptr, Tracked(&mut perm.points_to), v);
457    }
458
459    /// Moves `v` out of the location pointed to by the pointer `self`
460    /// and returns it.
461    /// Requires the memory to be initialized, and leaves it uninitialized.
462    ///
463    /// In the ghost perspective, this updates `perm.value`
464    /// from `Some(v)` to `None`,
465    /// while returning the `v` as an `exec` value.
466    #[inline(always)]
467    pub fn take(self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> (v: V)
468        requires
469            old(perm).pptr() == self,
470            old(perm).is_init(),
471        ensures
472            perm.pptr() == old(perm).pptr(),
473            perm.mem_contents() == MemContents::Uninit::<V>,
474            v == old(perm).value(),
475        opens_invariants none
476        no_unwind
477    {
478        proof {
479            use_type_invariant(&*perm);
480        }
481        let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
482        ptr_mut_read(ptr, Tracked(&mut perm.points_to))
483    }
484
485    /// Swaps the `in_v: V` passed in as an argument with the value in memory.
486    /// Requires the memory to be initialized, and leaves it initialized with the new value.
487    #[inline(always)]
488    pub fn replace(self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> (out_v: V)
489        requires
490            old(perm).pptr() == self,
491            old(perm).is_init(),
492        ensures
493            perm.pptr() == old(perm).pptr(),
494            perm.mem_contents() == MemContents::Init(in_v),
495            out_v == old(perm).value(),
496        opens_invariants none
497        no_unwind
498    {
499        proof {
500            use_type_invariant(&*perm);
501        }
502        let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
503        let out_v = ptr_mut_read(ptr, Tracked(&mut perm.points_to));
504        ptr_mut_write(ptr, Tracked(&mut perm.points_to), in_v);
505        out_v
506    }
507
508    /// Given a shared borrow of the `PointsTo<V>`, obtain a shared borrow of `V`.
509    #[inline(always)]
510    pub fn borrow<'a>(self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> (v: &'a V)
511        requires
512            perm.pptr() == self,
513            perm.is_init(),
514        ensures
515            *v === perm.value(),
516        opens_invariants none
517        no_unwind
518    {
519        proof {
520            use_type_invariant(&*perm);
521        }
522        let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
523        ptr_ref(ptr, Tracked(&perm.points_to))
524    }
525
526    #[inline(always)]
527    pub fn write(self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) where V: Copy
528        requires
529            old(perm).pptr() == self,
530        ensures
531            perm.pptr() === old(perm).pptr(),
532            perm.mem_contents() === MemContents::Init(in_v),
533        opens_invariants none
534        no_unwind
535    {
536        proof {
537            use_type_invariant(&*perm);
538            perm.leak_contents();
539        }
540        self.put(Tracked(&mut *perm), in_v);
541    }
542
543    #[inline(always)]
544    pub fn read(self, Tracked(perm): Tracked<&PointsTo<V>>) -> (out_v: V) where V: Copy
545        requires
546            perm.pptr() == self,
547            perm.is_init(),
548        ensures
549            out_v == perm.value(),
550        opens_invariants none
551        no_unwind
552    {
553        *self.borrow(Tracked(&*perm))
554    }
555}
556
557pub use raw_ptr::MemContents;
558
559} // verus!