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`] 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_lemmas};
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 final(self).pptr() == old(self).pptr(),
288 final(self).is_uninit(),
289 {
290 use_type_invariant(&*self);
291 self.points_to.leak_contents();
292 }
293
294 /// Guarantees that two distinct, non-ZST `PointsTo<V>` objects point to disjoint ranges of memory.
295 /// Since both S and V are non-zero-sized, this also implies the pointers
296 /// have distinct addresses.
297 ///
298 /// Note: If either S or T is zero-sized, we get disjointness "for free" without having to call this proof,
299 /// since the empty memory range corresponding to a ZST cannot possibly intersect with any other memory.
300 /// However, note that if one type is a ZST and the other is a non-ZST,
301 /// the disjointness definition as stated here here does not hold,
302 /// since the ZST pointer could be in the middle of the non-ZST's range.
303 pub proof fn is_disjoint<S>(tracked &mut self, tracked other: &PointsTo<S>)
304 requires
305 size_of::<V>() != 0,
306 size_of::<S>() != 0,
307 ensures
308 *old(self) == *final(self),
309 final(self).addr() + size_of::<V>() <= other.addr() || other.addr() + size_of::<S>()
310 <= final(self).addr(),
311 {
312 use_type_invariant(&*self);
313 self.points_to.is_disjoint(&other.points_to);
314 }
315
316 /// Guarantees that two distinct, non-ZST `PointsTo<V>` objects point to different
317 /// addresses. This is a corollary of [`PointsTo::is_disjoint`].
318 pub proof fn is_distinct<S>(tracked &mut self, tracked other: &PointsTo<S>)
319 requires
320 size_of::<V>() != 0,
321 size_of::<S>() != 0,
322 ensures
323 *old(self) == *final(self),
324 final(self).addr() != other.addr(),
325 {
326 use_type_invariant(&*self);
327 self.points_to.is_disjoint(&other.points_to);
328 }
329}
330
331impl<V> Clone for PPtr<V> {
332 fn clone(&self) -> (res: Self)
333 ensures
334 res == *self,
335 {
336 PPtr(self.0, PhantomData)
337 }
338}
339
340impl<V> Copy for PPtr<V> {
341
342}
343
344impl<V> PPtr<V> {
345 /// Allocates heap memory for type `V`, leaving it uninitialized.
346 #[cfg(feature = "std")]
347 pub fn empty() -> (pt: (PPtr<V>, Tracked<PointsTo<V>>))
348 ensures
349 pt.1@.pptr() == pt.0,
350 pt.1@.is_uninit(),
351 opens_invariants none
352 {
353 layout_for_type_is_valid::<V>();
354 if core::mem::size_of::<V>() != 0 {
355 let (p, Tracked(points_to_raw), Tracked(dealloc)) = allocate(
356 core::mem::size_of::<V>(),
357 core::mem::align_of::<V>(),
358 );
359 let Tracked(exposed) = expose_provenance(p);
360 let tracked points_to = points_to_raw.into_typed::<V>(p.addr());
361 proof {
362 points_to.is_nonnull();
363 }
364 let tracked pt = PointsTo { points_to, exposed, dealloc: Some(dealloc) };
365 let pptr = PPtr(p as usize, PhantomData);
366
367 return (pptr, Tracked(pt));
368 } else {
369 let p = core::mem::align_of::<V>();
370 assert(p % p == 0) by (nonlinear_arith)
371 requires
372 p != 0,
373 ;
374 let tracked emp = PointsToRaw::empty(Provenance::null());
375 proof {
376 assert forall|i: int| #[trigger]
377 Set::<int>::range(p as int, p as int).contains(i) == Set::<
378 int,
379 >::empty().contains(i) by {}
380 super::set::axiom_set_ext_equal(
381 Set::<int>::range(p as int, p as int),
382 Set::<int>::empty(),
383 );
384 assert(emp.is_range(p as int, 0));
385 }
386 let tracked points_to = emp.into_typed(p);
387 let tracked pt = PointsTo { points_to, exposed: IsExposed::null(), dealloc: None };
388 let pptr = PPtr(p, PhantomData);
389
390 return (pptr, Tracked(pt));
391 }
392 }
393
394 /// Allocates heap memory for type `V`, leaving it initialized
395 /// with the given value `v`.
396 #[cfg(feature = "std")]
397 pub fn new(v: V) -> (pt: (PPtr<V>, Tracked<PointsTo<V>>))
398 ensures
399 pt.1@.pptr() == pt.0,
400 pt.1@.mem_contents() == MemContents::Init(v),
401 opens_invariants none
402 {
403 let (p, Tracked(mut pt)) = PPtr::<V>::empty();
404 p.put(Tracked(&mut pt), v);
405 (p, Tracked(pt))
406 }
407
408 /// Free the memory pointed to be `perm`.
409 /// Requires the memory to be uninitialized.
410 ///
411 /// This consumes `perm`, since it will no longer be safe to access
412 /// that memory location.
413 pub fn free(self, Tracked(perm): Tracked<PointsTo<V>>)
414 requires
415 perm.pptr() == self,
416 perm.is_uninit(),
417 opens_invariants none
418 {
419 proof {
420 use_type_invariant(&perm);
421 }
422 if core::mem::size_of::<V>() != 0 {
423 let ptr: *mut u8 = with_exposed_provenance(self.0, Tracked(perm.exposed));
424 let tracked PointsTo { points_to, dealloc: dea, exposed } = perm;
425 let tracked points_to_raw = points_to.into_raw();
426 deallocate(
427 ptr,
428 core::mem::size_of::<V>(),
429 core::mem::align_of::<V>(),
430 Tracked(points_to_raw),
431 Tracked(dea.tracked_unwrap()),
432 );
433 }
434 }
435
436 /// Free the memory pointed to be `perm` and return the
437 /// value that was previously there.
438 /// Requires the memory to be initialized.
439 /// This consumes the [`PointsTo`] token, since the user is giving up
440 /// access to the memory by freeing it.
441 #[inline(always)]
442 pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> (v: V)
443 requires
444 perm.pptr() == self,
445 perm.is_init(),
446 ensures
447 v == perm.value(),
448 opens_invariants none
449 {
450 let tracked mut perm = perm;
451 let v = self.take(Tracked(&mut perm));
452 self.free(Tracked(perm));
453 v
454 }
455
456 /// Moves `v` into the location pointed to by the pointer `self`.
457 /// Requires the memory to be uninitialized, and leaves it initialized.
458 ///
459 /// In the ghost perspective, this updates `perm.mem_contents()`
460 /// from `MemContents::Uninit` to `MemContents::Init(v)`.
461 #[inline(always)]
462 pub fn put(self, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V)
463 requires
464 old(perm).pptr() == self,
465 old(perm).mem_contents() == MemContents::Uninit::<V>,
466 ensures
467 final(perm).pptr() == old(perm).pptr(),
468 final(perm).mem_contents() == MemContents::Init(v),
469 opens_invariants none
470 no_unwind
471 {
472 proof {
473 use_type_invariant(&*perm);
474 }
475 let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
476 ptr_mut_write(ptr, Tracked(&mut perm.points_to), v);
477 }
478
479 /// Moves `v` out of the location pointed to by the pointer `self`
480 /// and returns it.
481 /// Requires the memory to be initialized, and leaves it uninitialized.
482 ///
483 /// In the ghost perspective, this updates `perm.value`
484 /// from `Some(v)` to `None`,
485 /// while returning the `v` as an `exec` value.
486 #[inline(always)]
487 pub fn take(self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> (v: V)
488 requires
489 old(perm).pptr() == self,
490 old(perm).is_init(),
491 ensures
492 final(perm).pptr() == old(perm).pptr(),
493 final(perm).mem_contents() == MemContents::Uninit::<V>,
494 v == old(perm).value(),
495 opens_invariants none
496 no_unwind
497 {
498 proof {
499 use_type_invariant(&*perm);
500 }
501 let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
502 ptr_mut_read(ptr, Tracked(&mut perm.points_to))
503 }
504
505 /// Swaps the `in_v: V` passed in as an argument with the value in memory.
506 /// Requires the memory to be initialized, and leaves it initialized with the new value.
507 #[inline(always)]
508 pub fn replace(self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> (out_v: V)
509 requires
510 old(perm).pptr() == self,
511 old(perm).is_init(),
512 ensures
513 final(perm).pptr() == old(perm).pptr(),
514 final(perm).mem_contents() == MemContents::Init(in_v),
515 out_v == old(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 let out_v = ptr_mut_read(ptr, Tracked(&mut perm.points_to));
524 ptr_mut_write(ptr, Tracked(&mut perm.points_to), in_v);
525 out_v
526 }
527
528 /// Given a shared borrow of the `PointsTo<V>`, obtain a shared borrow of `V`.
529 #[inline(always)]
530 pub fn borrow<'a>(self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> (v: &'a V)
531 requires
532 perm.pptr() == self,
533 perm.is_init(),
534 ensures
535 *v == perm.value(),
536 opens_invariants none
537 no_unwind
538 {
539 proof {
540 use_type_invariant(&*perm);
541 }
542 let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
543 ptr_ref(ptr, Tracked(&perm.points_to))
544 }
545
546 /// Given a shared borrow of the `PointsTo<V>`, obtain a shared borrow of `V`.
547 #[inline(always)]
548 pub fn borrow_mut<'a>(self, Tracked(perm): Tracked<&'a mut PointsTo<V>>) -> (v: &'a mut V)
549 requires
550 perm.pptr() == self,
551 perm.is_init(),
552 ensures
553 final(perm).pptr() == self,
554 final(perm).is_init(),
555 *v == old(perm).value(),
556 final(perm).value() == *final(v),
557 opens_invariants none
558 no_unwind
559 {
560 proof {
561 use_type_invariant(&*perm);
562 }
563 let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
564 ptr_mut_ref(ptr, Tracked(&mut perm.points_to))
565 }
566
567 #[inline(always)]
568 pub fn write(self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) where V: Copy
569 requires
570 old(perm).pptr() == self,
571 ensures
572 final(perm).pptr() == old(perm).pptr(),
573 final(perm).mem_contents() == MemContents::Init(in_v),
574 opens_invariants none
575 no_unwind
576 {
577 proof {
578 use_type_invariant(&*perm);
579 perm.leak_contents();
580 }
581 self.put(Tracked(&mut *perm), in_v);
582 }
583
584 #[inline(always)]
585 pub fn read(self, Tracked(perm): Tracked<&PointsTo<V>>) -> (out_v: V) where V: Copy
586 requires
587 perm.pptr() == self,
588 perm.is_init(),
589 ensures
590 out_v == perm.value(),
591 opens_invariants none
592 no_unwind
593 {
594 *self.borrow(Tracked(&*perm))
595 }
596}
597
598pub use raw_ptr::MemContents;
599
600} // verus!