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_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, 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) == *self,
309 self.addr() + size_of::<V>() <= other.addr() || other.addr() + size_of::<S>()
310 <= 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) == *self,
324 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 let tracked points_to = emp.into_typed(p);
376 let tracked pt = PointsTo { points_to, exposed: IsExposed::null(), dealloc: None };
377 let pptr = PPtr(p, PhantomData);
378
379 return (pptr, Tracked(pt));
380 }
381 }
382
383 /// Allocates heap memory for type `V`, leaving it initialized
384 /// with the given value `v`.
385 #[cfg(feature = "std")]
386 pub fn new(v: V) -> (pt: (PPtr<V>, Tracked<PointsTo<V>>))
387 ensures
388 pt.1@.pptr() == pt.0,
389 pt.1@.mem_contents() == MemContents::Init(v),
390 opens_invariants none
391 {
392 let (p, Tracked(mut pt)) = PPtr::<V>::empty();
393 p.put(Tracked(&mut pt), v);
394 (p, Tracked(pt))
395 }
396
397 /// Free the memory pointed to be `perm`.
398 /// Requires the memory to be uninitialized.
399 ///
400 /// This consumes `perm`, since it will no longer be safe to access
401 /// that memory location.
402 pub fn free(self, Tracked(perm): Tracked<PointsTo<V>>)
403 requires
404 perm.pptr() == self,
405 perm.is_uninit(),
406 opens_invariants none
407 {
408 proof {
409 use_type_invariant(&perm);
410 }
411 if core::mem::size_of::<V>() != 0 {
412 let ptr: *mut u8 = with_exposed_provenance(self.0, Tracked(perm.exposed));
413 let tracked PointsTo { points_to, dealloc: dea, exposed } = perm;
414 let tracked points_to_raw = points_to.into_raw();
415 deallocate(
416 ptr,
417 core::mem::size_of::<V>(),
418 core::mem::align_of::<V>(),
419 Tracked(points_to_raw),
420 Tracked(dea.tracked_unwrap()),
421 );
422 }
423 }
424
425 /// Free the memory pointed to be `perm` and return the
426 /// value that was previously there.
427 /// Requires the memory to be initialized.
428 /// This consumes the [`PointsTo`] token, since the user is giving up
429 /// access to the memory by freeing it.
430 #[inline(always)]
431 pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> (v: V)
432 requires
433 perm.pptr() == self,
434 perm.is_init(),
435 ensures
436 v == perm.value(),
437 opens_invariants none
438 {
439 let tracked mut perm = perm;
440 let v = self.take(Tracked(&mut perm));
441 self.free(Tracked(perm));
442 v
443 }
444
445 /// Moves `v` into the location pointed to by the pointer `self`.
446 /// Requires the memory to be uninitialized, and leaves it initialized.
447 ///
448 /// In the ghost perspective, this updates `perm.mem_contents()`
449 /// from `MemContents::Uninit` to `MemContents::Init(v)`.
450 #[inline(always)]
451 pub fn put(self, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V)
452 requires
453 old(perm).pptr() == self,
454 old(perm).mem_contents() == MemContents::Uninit::<V>,
455 ensures
456 perm.pptr() == old(perm).pptr(),
457 perm.mem_contents() == MemContents::Init(v),
458 opens_invariants none
459 no_unwind
460 {
461 proof {
462 use_type_invariant(&*perm);
463 }
464 let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
465 ptr_mut_write(ptr, Tracked(&mut perm.points_to), v);
466 }
467
468 /// Moves `v` out of the location pointed to by the pointer `self`
469 /// and returns it.
470 /// Requires the memory to be initialized, and leaves it uninitialized.
471 ///
472 /// In the ghost perspective, this updates `perm.value`
473 /// from `Some(v)` to `None`,
474 /// while returning the `v` as an `exec` value.
475 #[inline(always)]
476 pub fn take(self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> (v: V)
477 requires
478 old(perm).pptr() == self,
479 old(perm).is_init(),
480 ensures
481 perm.pptr() == old(perm).pptr(),
482 perm.mem_contents() == MemContents::Uninit::<V>,
483 v == old(perm).value(),
484 opens_invariants none
485 no_unwind
486 {
487 proof {
488 use_type_invariant(&*perm);
489 }
490 let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
491 ptr_mut_read(ptr, Tracked(&mut perm.points_to))
492 }
493
494 /// Swaps the `in_v: V` passed in as an argument with the value in memory.
495 /// Requires the memory to be initialized, and leaves it initialized with the new value.
496 #[inline(always)]
497 pub fn replace(self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> (out_v: V)
498 requires
499 old(perm).pptr() == self,
500 old(perm).is_init(),
501 ensures
502 perm.pptr() == old(perm).pptr(),
503 perm.mem_contents() == MemContents::Init(in_v),
504 out_v == old(perm).value(),
505 opens_invariants none
506 no_unwind
507 {
508 proof {
509 use_type_invariant(&*perm);
510 }
511 let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
512 let out_v = ptr_mut_read(ptr, Tracked(&mut perm.points_to));
513 ptr_mut_write(ptr, Tracked(&mut perm.points_to), in_v);
514 out_v
515 }
516
517 /// Given a shared borrow of the `PointsTo<V>`, obtain a shared borrow of `V`.
518 #[inline(always)]
519 pub fn borrow<'a>(self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> (v: &'a V)
520 requires
521 perm.pptr() == self,
522 perm.is_init(),
523 ensures
524 *v === perm.value(),
525 opens_invariants none
526 no_unwind
527 {
528 proof {
529 use_type_invariant(&*perm);
530 }
531 let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed));
532 ptr_ref(ptr, Tracked(&perm.points_to))
533 }
534
535 #[inline(always)]
536 pub fn write(self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) where V: Copy
537 requires
538 old(perm).pptr() == self,
539 ensures
540 perm.pptr() === old(perm).pptr(),
541 perm.mem_contents() === MemContents::Init(in_v),
542 opens_invariants none
543 no_unwind
544 {
545 proof {
546 use_type_invariant(&*perm);
547 perm.leak_contents();
548 }
549 self.put(Tracked(&mut *perm), in_v);
550 }
551
552 #[inline(always)]
553 pub fn read(self, Tracked(perm): Tracked<&PointsTo<V>>) -> (out_v: V) where V: Copy
554 requires
555 perm.pptr() == self,
556 perm.is_init(),
557 ensures
558 out_v == perm.value(),
559 opens_invariants none
560 no_unwind
561 {
562 *self.borrow(Tracked(&*perm))
563 }
564}
565
566pub use raw_ptr::MemContents;
567
568} // verus!