Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601use super::layout::*;use super::prelude::*;use super::raw_ptr;use super::raw_ptr::*;use core::marker::PhantomData;
verus! {
/// `PPtr` (which stands for "permissioned pointer")/// is a wrapper around a raw pointer to a heap-allocated `V`./// This is designed to be simpler to use that Verus's/// [more general pointer support](`crate::raw_ptr`),/// but also to serve as a better introductory point./// Historically, `PPtr` was positioned as a "trusted primitive" of Verus,/// but now, it is implemented and verified from the more general pointer support,/// which operates on similar principles, but which is much precise to Rust's/// pointer semantics.////// A `PPtr` is equvialent to its `usize`-based address. The type paramter `V` technically/// doesn't matter, and you can freely convert between `PPtr<V>` and `PPtr<W>` by casting/// to and from the `usize` address. What _really_ matters is the type paramter of the/// `PointsTo<V>`.////// In order to access (read or write) the value behind the pointer, the user needs/// a special _ghost permission token_, [`PointsTo<V>`](PointsTo). This object is `tracked`,/// which means that it is "only a proof construct" that does not appear in compiled code,/// but its uses _are_ checked by the borrow-checker. This ensures memory safety,/// data-race-freedom, prohibits use-after-free, etc.////// ### PointsTo objects.////// The [`PointsTo`] object represents both the ability to access (read or write)/// the data behind the pointer _and_ the ability to free it/// (return it to the memory allocator).////// The `perm: PointsTo<V>` object tracks two pieces of data:/// * [`perm.pptr()`](PointsTo::pptr) is the pointer that the permission is associated to./// * [`perm.mem_contents()`](PointsTo::mem_contents) is the memory contents, which is one of either:/// * [`MemContents::Uninit`] if the memory pointed-to by/// by the pointer is uninitialized./// * [`MemContents::Init(v)`](raw_ptr::MemContents::Init) if the memory points-to the/// the value `v`.////// Your access to the `PointsTo` object determines what operations you can safely perform/// with the pointer:/// * You can _read_ from the pointer as long as you have read access to the `PointsTo` object,/// e.g., `&PointsTo<V>`./// * You can _write_ to the pointer as long as you have mutable access to the `PointsTo` object,/// e.g., `&mut PointsTo<V>`/// * You can call `free` to deallocate the memory as long as you have full onwership/// of the `PointsTo` object (i.e., the ability to move it).////// For those familiar with separation logic, the `PointsTo` object plays a role/// similar to that of the "points-to" operator, _ptr_ ↦ _value_.////// ### Example////// ```rust,ignored/// fn main() {/// unsafe {/// // ALLOCATE/// // p: PPtr<u64>, points_to: PointsTo<u64>/// let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();////// assert(points_to.mem_contents() == MemContents::Uninit);/// assert(points_to.pptr() == p);////// // unsafe { *p = 5; }/// p.write(Tracked(&mut points_to), 5);////// assert(points_to.mem_contents() == MemContents::Init(5));/// assert(points_to.pptr() == p);////// // let x = unsafe { *p };/// let x = p.read(Tracked(&points_to));////// assert(x == 5);////// // DEALLOCATE/// let y = p.into_inner(Tracked(points_to));////// assert(y == 5);/// }/// }/// ```////// ### Examples of incorrect usage////// The following code has a use-after-free bug, and it is rejected by Verus because/// it fails to satisfy Rust's ownership-checker.////// ```rust,ignored/// fn main() {/// unsafe {/// // ALLOCATE/// // p: PPtr<u64>, points_to: PointsTo<u64>/// let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();////// // unsafe { *p = 5; }/// p.write(Tracked(&mut points_to), 5);////// // let x = unsafe { *p };/// let x = p.read(Tracked(&points_to));////// // DEALLOCATE/// p.free(Tracked(points_to)); // `points_to` is moved here////// // READ-AFTER-FREE/// let x2 = p.read(Tracked(&mut points_to)); // so it can't be used here/// }/// }/// ```////// The following doesn't violate Rust's ownership-checking, but it "mixes up" the `PointsTo`/// objects, attempting to use the wrong `PointsTo` for the given pointer./// This violates the precondition on [`p.read()`](PPtr::read).////// ```rust,ignored/// fn main() {/// unsafe {/// // ALLOCATE p/// let (p, Tracked(mut perm_p)) = PPtr::<u64>::empty();////// // ALLOCATE q/// let (q, Tracked(mut perm_q)) = PPtr::<u64>::empty();////// // DEALLOCATE p/// p.free(Tracked(perm_p));////// // READ-AFTER-FREE (read from p, try to use q's permission object)/// let x = p.read(Tracked(&mut perm_q));/// }/// }/// ```////// ### Differences from `PCell`.////// `PPtr` is similar to [`cell::PCell`](crate::cell::PCell), but has a few key differences:/// * In `PCell<V>`, the type `V` is placed internally to the `PCell`, whereas with `PPtr`,/// the type `V` is placed at some location on the heap./// * Since `PPtr` is just a pointer (represented by an integer), it can be `Copy`./// * The `ptr::PointsTo` token represents not just the permission to read/write/// the contents, but also to deallocate.////// ### Simplifications relative to more general pointer API////// * Pointers are only represented by addresses and don't have a general notion of provenance/// * Pointers are untyped (only `PointsTo` is typed)./// * The `PointsTo` also encapsulates the permission to free a pointer./// * `PointsTo` tokens are non-fungible. They can't be broken up or made variable-sized.// We want PPtr's fields to be public so the solver knows that equality of addresses// implies equality of PPtrspub struct PPtr<V>(pub usize, pub PhantomData<V>);
/// A `tracked` ghost object that gives the user permission to dereference a pointer/// for reading or writing, or to free the memory at that pointer.////// The meaning of a `PointsTo` object is given by the data in its/// `View` object, [`PointsToData`].////// See the [`PPtr`] documentation for more details.pub tracked struct PointsTo<V> { points_to: raw_ptr::PointsTo<V>, exposed: raw_ptr::IsExposed, dealloc: Option<raw_ptr::Dealloc>,}
#[verusfmt::skip]broadcast use { super::raw_ptr::group_raw_ptr_axioms, super::set_lib::group_set_lib_default, super::set::group_set_lemmas};
impl<V> PPtr<V> { /// Use `addr()` instead #[verifier::inline] pub open spec fn spec_addr(p: PPtr<V>) -> usize { p.0 }
/// Cast a pointer to an integer. #[inline(always)] #[verifier::when_used_as_spec(spec_addr)] pub fn addr(self) -> (u: usize) ensures u == self.addr(), { self.0 }
/// Cast an integer to a pointer. /// /// Note that this does _not_ require or ensure that the pointer is valid. /// Of course, if the user creates an invalid pointer, they would still not be able to /// create a valid [`PointsTo`] token for it, and thus they would never /// be able to access the data behind the pointer. /// /// This is analogous to normal Rust, where casting to a pointer is always possible, /// but dereferencing a pointer is an `unsafe` operation. /// With PPtr, casting to a pointer is likewise always possible, /// while dereferencing it is only allowed when the right preconditions are met. #[inline(always)] pub fn from_addr(u: usize) -> (s: Self) ensures u == s.addr(), { PPtr(u, PhantomData) }
#[doc(hidden)] #[inline(always)] pub fn from_usize(u: usize) -> (s: Self) ensures u == s.addr(), { PPtr(u, PhantomData) }}
impl<V> PointsTo<V> { #[verifier::inline] pub open spec fn pptr(&self) -> PPtr<V> { PPtr(self.addr(), PhantomData) }
pub closed spec fn addr(self) -> usize { self.points_to.ptr().addr() }
#[verifier::type_invariant] closed spec fn wf(self) -> bool { &&& self.points_to.ptr()@.provenance == self.exposed.provenance() &&& match self.dealloc { Some(dealloc) => { &&& dealloc.addr() == self.points_to.ptr().addr() &&& dealloc.size() == size_of::<V>() &&& dealloc.align() == align_of::<V>() &&& dealloc.provenance() == self.points_to.ptr()@.provenance &&& size_of::<V>() > 0 }, None => { size_of::<V>() == 0 }, } &&& self.points_to.ptr().addr() != 0 }
pub closed spec fn mem_contents(&self) -> MemContents<V> { self.points_to.opt_value() }
#[doc(hidden)] #[verifier::inline] pub open spec fn opt_value(&self) -> MemContents<V> { self.mem_contents() }
#[verifier::inline] pub open spec fn is_init(&self) -> bool { self.mem_contents().is_init() }
#[verifier::inline] pub open spec fn is_uninit(&self) -> bool { self.mem_contents().is_uninit() }
#[verifier::inline] pub open spec fn value(&self) -> V recommends self.is_init(), { self.mem_contents().value() }
/// Guarantee that the `PointsTo` points to a non-null address. pub proof fn is_nonnull(tracked &self) ensures self.addr() != 0, { use_type_invariant(self); }
/// "Forgets" about the value stored behind the pointer. /// Updates the `PointsTo` value to [`MemContents::Uninit`]. /// Note that this is a `proof` function, i.e., it is operationally a no-op in executable code. pub proof fn leak_contents(tracked &mut self) ensures final(self).pptr() == old(self).pptr(), final(self).is_uninit(), { use_type_invariant(&*self); self.points_to.leak_contents(); }
/// Guarantees that two distinct, non-ZST `PointsTo<V>` objects point to disjoint ranges of memory. /// Since both S and V are non-zero-sized, this also implies the pointers /// have distinct addresses. /// /// Note: If either S or T is zero-sized, we get disjointness "for free" without having to call this proof, /// since the empty memory range corresponding to a ZST cannot possibly intersect with any other memory. /// However, note that if one type is a ZST and the other is a non-ZST, /// the disjointness definition as stated here here does not hold, /// since the ZST pointer could be in the middle of the non-ZST's range. pub proof fn is_disjoint<S>(tracked &mut self, tracked other: &PointsTo<S>) requires size_of::<V>() != 0, size_of::<S>() != 0, ensures *old(self) == *final(self), final(self).addr() + size_of::<V>() <= other.addr() || other.addr() + size_of::<S>() <= final(self).addr(), { use_type_invariant(&*self); self.points_to.is_disjoint(&other.points_to); }
/// Guarantees that two distinct, non-ZST `PointsTo<V>` objects point to different /// addresses. This is a corollary of [`PointsTo::is_disjoint`]. pub proof fn is_distinct<S>(tracked &mut self, tracked other: &PointsTo<S>) requires size_of::<V>() != 0, size_of::<S>() != 0, ensures *old(self) == *final(self), final(self).addr() != other.addr(), { use_type_invariant(&*self); self.points_to.is_disjoint(&other.points_to); }}
impl<V> Clone for PPtr<V> { fn clone(&self) -> (res: Self) ensures res == *self, { PPtr(self.0, PhantomData) }}
impl<V> Copy for PPtr<V> {
}
impl<V> PPtr<V> { /// Allocates heap memory for type `V`, leaving it uninitialized. #[cfg(feature = "std")] pub fn empty() -> (pt: (PPtr<V>, Tracked<PointsTo<V>>)) ensures pt.1@.pptr() == pt.0, pt.1@.is_uninit(), opens_invariants none { layout_for_type_is_valid::<V>(); if core::mem::size_of::<V>() != 0 { let (p, Tracked(points_to_raw), Tracked(dealloc)) = allocate( core::mem::size_of::<V>(), core::mem::align_of::<V>(), ); let Tracked(exposed) = expose_provenance(p); let tracked points_to = points_to_raw.into_typed::<V>(p.addr()); proof { points_to.is_nonnull(); } let tracked pt = PointsTo { points_to, exposed, dealloc: Some(dealloc) }; let pptr = PPtr(p as usize, PhantomData);
return (pptr, Tracked(pt)); } else { let p = core::mem::align_of::<V>(); assert(p % p == 0) by (nonlinear_arith) requires p != 0, ; let tracked emp = PointsToRaw::empty(Provenance::null()); proof { assert forall|i: int| #[trigger] Set::<int>::range(p as int, p as int).contains(i) == Set::< int, >::empty().contains(i) by {} super::set::axiom_set_ext_equal( Set::<int>::range(p as int, p as int), Set::<int>::empty(), ); assert(emp.is_range(p as int, 0)); } let tracked points_to = emp.into_typed(p); let tracked pt = PointsTo { points_to, exposed: IsExposed::null(), dealloc: None }; let pptr = PPtr(p, PhantomData);
return (pptr, Tracked(pt)); } }
/// Allocates heap memory for type `V`, leaving it initialized /// with the given value `v`. #[cfg(feature = "std")] pub fn new(v: V) -> (pt: (PPtr<V>, Tracked<PointsTo<V>>)) ensures pt.1@.pptr() == pt.0, pt.1@.mem_contents() == MemContents::Init(v), opens_invariants none { let (p, Tracked(mut pt)) = PPtr::<V>::empty(); p.put(Tracked(&mut pt), v); (p, Tracked(pt)) }
/// Free the memory pointed to be `perm`. /// Requires the memory to be uninitialized. /// /// This consumes `perm`, since it will no longer be safe to access /// that memory location. pub fn free(self, Tracked(perm): Tracked<PointsTo<V>>) requires perm.pptr() == self, perm.is_uninit(), opens_invariants none { proof { use_type_invariant(&perm); } if core::mem::size_of::<V>() != 0 { let ptr: *mut u8 = with_exposed_provenance(self.0, Tracked(perm.exposed)); let tracked PointsTo { points_to, dealloc: dea, exposed } = perm; let tracked points_to_raw = points_to.into_raw(); deallocate( ptr, core::mem::size_of::<V>(), core::mem::align_of::<V>(), Tracked(points_to_raw), Tracked(dea.tracked_unwrap()), ); } }
/// Free the memory pointed to be `perm` and return the /// value that was previously there. /// Requires the memory to be initialized. /// This consumes the [`PointsTo`] token, since the user is giving up /// access to the memory by freeing it. #[inline(always)] pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> (v: V) requires perm.pptr() == self, perm.is_init(), ensures v == perm.value(), opens_invariants none { let tracked mut perm = perm; let v = self.take(Tracked(&mut perm)); self.free(Tracked(perm)); v }
/// Moves `v` into the location pointed to by the pointer `self`. /// Requires the memory to be uninitialized, and leaves it initialized. /// /// In the ghost perspective, this updates `perm.mem_contents()` /// from `MemContents::Uninit` to `MemContents::Init(v)`. #[inline(always)] pub fn put(self, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V) requires old(perm).pptr() == self, old(perm).mem_contents() == MemContents::Uninit::<V>, ensures final(perm).pptr() == old(perm).pptr(), final(perm).mem_contents() == MemContents::Init(v), opens_invariants none no_unwind { proof { use_type_invariant(&*perm); } let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed)); ptr_mut_write(ptr, Tracked(&mut perm.points_to), v); }
/// Moves `v` out of the location pointed to by the pointer `self` /// and returns it. /// Requires the memory to be initialized, and leaves it uninitialized. /// /// In the ghost perspective, this updates `perm.value` /// from `Some(v)` to `None`, /// while returning the `v` as an `exec` value. #[inline(always)] pub fn take(self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> (v: V) requires old(perm).pptr() == self, old(perm).is_init(), ensures final(perm).pptr() == old(perm).pptr(), final(perm).mem_contents() == MemContents::Uninit::<V>, v == old(perm).value(), opens_invariants none no_unwind { proof { use_type_invariant(&*perm); } let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed)); ptr_mut_read(ptr, Tracked(&mut perm.points_to)) }
/// Swaps the `in_v: V` passed in as an argument with the value in memory. /// Requires the memory to be initialized, and leaves it initialized with the new value. #[inline(always)] pub fn replace(self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> (out_v: V) requires old(perm).pptr() == self, old(perm).is_init(), ensures final(perm).pptr() == old(perm).pptr(), final(perm).mem_contents() == MemContents::Init(in_v), out_v == old(perm).value(), opens_invariants none no_unwind { proof { use_type_invariant(&*perm); } let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed)); let out_v = ptr_mut_read(ptr, Tracked(&mut perm.points_to)); ptr_mut_write(ptr, Tracked(&mut perm.points_to), in_v); out_v }
/// Given a shared borrow of the `PointsTo<V>`, obtain a shared borrow of `V`. #[inline(always)] pub fn borrow<'a>(self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> (v: &'a V) requires perm.pptr() == self, perm.is_init(), ensures *v == perm.value(), opens_invariants none no_unwind { proof { use_type_invariant(&*perm); } let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed)); ptr_ref(ptr, Tracked(&perm.points_to)) }
/// Given a shared borrow of the `PointsTo<V>`, obtain a shared borrow of `V`. #[inline(always)] pub fn borrow_mut<'a>(self, Tracked(perm): Tracked<&'a mut PointsTo<V>>) -> (v: &'a mut V) requires perm.pptr() == self, perm.is_init(), ensures final(perm).pptr() == self, final(perm).is_init(), *v == old(perm).value(), final(perm).value() == *final(v), opens_invariants none no_unwind { proof { use_type_invariant(&*perm); } let ptr: *mut V = with_exposed_provenance(self.0, Tracked(perm.exposed)); ptr_mut_ref(ptr, Tracked(&mut perm.points_to)) }
#[inline(always)] pub fn write(self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) where V: Copy requires old(perm).pptr() == self, ensures final(perm).pptr() == old(perm).pptr(), final(perm).mem_contents() == MemContents::Init(in_v), opens_invariants none no_unwind { proof { use_type_invariant(&*perm); perm.leak_contents(); } self.put(Tracked(&mut *perm), in_v); }
#[inline(always)] pub fn read(self, Tracked(perm): Tracked<&PointsTo<V>>) -> (out_v: V) where V: Copy requires perm.pptr() == self, perm.is_init(), ensures out_v == perm.value(), opens_invariants none no_unwind { *self.borrow(Tracked(&*perm)) }}
pub use raw_ptr::MemContents;
} // verus!