#[repr(C)]pub struct PPtr<V> {
pub uptr: *mut V,
}Expand description
PPtr<V> (which stands for “permissioned pointer”)
is a wrapper around a raw pointer to V on the heap.
Technically, it is a wrapper around *mut mem::MaybeUninit<V>, that is, the object
it points to may be uninitialized.
In order to access (read or write) the value behind the pointer, the user needs
a special ghost permission token, PointsTo<V>. This object is tracked,
which means that it is “only a proof construct” that does not appear in 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 the data behind the
pointer and the ability to free it (return it to the memory allocator).
In particular:
- When the user owns a
PointsTo<V>object associated to a given pointer, they can either read or write its contents, or deallocate (“free”) it. - When the user has a shared borrow,
&PointsTo<V>, they can read the contents (i.e., obtained a shared borrow&V).
The perm: PointsTo<V> object tracks two pieces of data:
perm.pptris the pointer that the permission is associated to, given byptr.id().perm.valuetracks the data that is behind the pointer. Thereby:- When the user uses the permission to read a value, they always
read the value as given by the
perm.value. - When the user uses the permission to write a value, the
perm.valuedata is updated.
- When the user uses the permission to read a value, they always
read the value as given by the
For those familiar with separation logic, the PointsTo object plays a role
similar to that of the “points-to” operator, ptr ↦ value.
Differences from PCell.
PPtr is similar to cell::PCell, but has a few key differences:
- In
PCell<T>, the typeTis placed internally to thePCell, whereas withPPtr, the typeTis placed at some location on the heap. - Since
PPtris just a pointer (represented by an integer), it can beCopy. - The
ptr::PointsTotoken represents not just the permission to read/write the contents, but also to deallocate.
Example (TODO)
Fields§
§uptr: *mut VImplementations§
source§impl<V> PPtr<V>
impl<V> PPtr<V>
sourcepub exec fn to_usize(&self) -> usize
pub exec fn to_usize(&self) -> usize
u as int == self.id(),Cast a pointer to an integer.
sourcepub exec fn from_usize(u: usize) -> Self
pub exec fn from_usize(u: usize) -> Self
p.id() == u as int,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.
In Verus, casting to a pointer is likewise always possible,
while dereferencing it is only allowed when the right preconditions are met.
sourcepub exec fn empty() -> (PPtr<V>, Tracked<PointsTo<V>>, Tracked<Dealloc<V>>)
pub exec fn empty() -> (PPtr<V>, Tracked<PointsTo<V>>, Tracked<Dealloc<V>>)
pt.1@@
=== (PointsToData {
pptr: pt.0.id(),
value: None,
}),pt.2@@ === (DeallocData { pptr: pt.0.id() }),Allocates heap memory for type V, leaving it uninitialized.
sourcepub exec fn alloc(
size: usize,
align: usize
) -> (PPtr<V>, Tracked<PointsToRaw>, Tracked<DeallocRaw>)
pub exec fn alloc( size: usize, align: usize ) -> (PPtr<V>, Tracked<PointsToRaw>, Tracked<DeallocRaw>)
valid_layout(size, align),pt.1@.is_range(pt.0.id(), size as int),pt.2@@
=== (DeallocRawData {
pptr: pt.0.id(),
size: size as nat,
align: align as nat,
}),pt.0.id() % align as int == 0,sourcepub exec fn put(&self, verus_tmp_perm: Tracked<&mut PointsTo<V>>, v: V)
pub exec fn put(&self, verus_tmp_perm: Tracked<&mut PointsTo<V>>, v: V)
self.id() === old(perm)@.pptr,old(perm)@.value === None,perm@.pptr === old(perm)@.pptr,perm@.value === Some(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.value
from None to Some(v).
sourcepub exec fn take(&self, verus_tmp_perm: Tracked<&mut PointsTo<V>>) -> V
pub exec fn take(&self, verus_tmp_perm: Tracked<&mut PointsTo<V>>) -> V
self.id() === old(perm)@.pptr,old(perm)@.value.is_Some(),perm@.pptr === old(perm)@.pptr,perm@.value === None,v === old(perm)@.value.get_Some_0(),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.
sourcepub exec fn replace(&self, verus_tmp_perm: Tracked<&mut PointsTo<V>>, in_v: V) -> V
pub exec fn replace(&self, verus_tmp_perm: Tracked<&mut PointsTo<V>>, in_v: V) -> V
self.id() === old(perm)@.pptr,old(perm)@.value.is_Some(),perm@.pptr === old(perm)@.pptr,perm@.value === Some(in_v),out_v === old(perm)@.value.get_Some_0(),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.
sourcepub exec fn borrow<'a>(&self, verus_tmp_perm: Tracked<&'a PointsTo<V>>) -> &'a V
pub exec fn borrow<'a>(&self, verus_tmp_perm: Tracked<&'a PointsTo<V>>) -> &'a V
self.id() === perm@.pptr,perm@.value.is_Some(),*v === perm@.value.get_Some_0(),Given a shared borrow of the PointsTo<V>, obtain a shared borrow of V.
sourcepub exec fn dispose(
&self,
verus_tmp_perm: Tracked<PointsTo<V>>,
verus_tmp_dealloc: Tracked<Dealloc<V>>
)
pub exec fn dispose( &self, verus_tmp_perm: Tracked<PointsTo<V>>, verus_tmp_dealloc: Tracked<Dealloc<V>> )
self.id() === perm@.pptr,perm@.value === None,perm@.pptr == dealloc@.pptr,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.
sourcepub exec fn dealloc(
&self,
size: usize,
align: usize,
verus_tmp_perm: Tracked<PointsToRaw>,
verus_tmp_dealloc: Tracked<DeallocRaw>
)
pub exec fn dealloc( &self, size: usize, align: usize, verus_tmp_perm: Tracked<PointsToRaw>, verus_tmp_dealloc: Tracked<DeallocRaw> )
perm.is_range(self.id(), size as int),dealloc@.pptr === self.id(),dealloc@.size === size as nat,dealloc@.align === align as nat,sourcepub exec fn into_inner(
self,
verus_tmp_perm: Tracked<PointsTo<V>>,
verus_tmp_dealloc: Tracked<Dealloc<V>>
) -> V
pub exec fn into_inner( self, verus_tmp_perm: Tracked<PointsTo<V>>, verus_tmp_dealloc: Tracked<Dealloc<V>> ) -> V
self.id() === perm@.pptr,perm@.pptr == dealloc@.pptr,perm@.value.is_Some(),v === perm@.value.get_Some_0(),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.