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!