#[repr(C)]pub struct PPtr<V> {
pub uptr: *mut V,
}PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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 VPPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)Implementations§
source§impl<V> PPtr<V>
impl<V> PPtr<V>
sourcepub exec fn to_usize(&self) -> u : usize
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn to_usize(&self) -> u : usize
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)u as int == self.id(),Cast a pointer to an integer.
sourcepub spec fn id(&self) -> int
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub spec fn id(&self) -> int
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)integer address of the pointer
sourcepub exec fn from_usize(u: usize) -> p : Self
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn from_usize(u: usize) -> p : Self
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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() -> pt : (PPtr<V>, Tracked<PointsTo<V>>, Tracked<Dealloc<V>>)
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn empty() -> pt : (PPtr<V>, Tracked<PointsTo<V>>, Tracked<Dealloc<V>>)
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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
) -> pt : (PPtr<V>, Tracked<PointsToRaw>, Tracked<DeallocRaw>)
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn alloc( size: usize, align: usize ) -> pt : (PPtr<V>, Tracked<PointsToRaw>, Tracked<DeallocRaw>)
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V)
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn put(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V)
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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, Tracked(perm): Tracked<&mut PointsTo<V>>) -> v : V
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn take(&self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> v : V
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> out_v : V
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn replace(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> out_v : V
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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, Tracked(perm): Tracked<&'a PointsTo<V>>) -> v : &'a V
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn borrow<'a>(&self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> v : &'a V
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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>>
)
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn dispose( &self, verus_tmp_perm: Tracked<PointsTo<V>>, verus_tmp_dealloc: Tracked<Dealloc<V>> )
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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>
)
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn dealloc( &self, size: usize, align: usize, verus_tmp_perm: Tracked<PointsToRaw>, verus_tmp_dealloc: Tracked<DeallocRaw> )
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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 : V
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn into_inner( self, verus_tmp_perm: Tracked<PointsTo<V>>, verus_tmp_dealloc: Tracked<Dealloc<V>> ) -> v : V
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)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.
sourcepub exec fn new(v: V) -> pt : (PPtr<V>, Tracked<PointsTo<V>>, Tracked<Dealloc<V>>)
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn new(v: V) -> pt : (PPtr<V>, Tracked<PointsTo<V>>, Tracked<Dealloc<V>>)
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)(pt.1@@
=== PointsToData {
pptr: pt.0.id(),
value: Some(v),
}),(pt.2@@ === DeallocData { pptr: pt.0.id() }),Allocates heap memory for type V, leaving it initialized
with the given value v.
source§impl<V: Copy> PPtr<V>
impl<V: Copy> PPtr<V>
sourcepub exec fn write(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V)
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn write(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V)
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)self.id() === old(perm)@.pptr,perm@.pptr === old(perm)@.pptr,perm@.value === Some(in_v),sourcepub exec fn read(&self, Tracked(perm): Tracked<&PointsTo<V>>) -> out_v : V
👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
– PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)
pub exec fn read(&self, Tracked(perm): Tracked<&PointsTo<V>>) -> out_v : V
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)self.id() === perm@.pptr,perm@.value.is_Some(),perm@.value === Some(out_v),