Struct vstd::ptr::PPtr

source · 
#[repr(C)]
pub struct PPtr<V> {
    pub uptr: *mut 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)
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.pptr is the pointer that the permission is associated to, given by ptr.id().
  • perm.value tracks 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.value data is updated.

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 type T is placed internally to the PCell, whereas with PPtr, the type T 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.

§Example (TODO)

Fields§

§uptr: *mut 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)

Implementations§

source§

impl<V> PPtr<V>

source

pub 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)
ensures
u as int == self.id(),

Cast a pointer to an integer.

source

pub 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)

integer address of the pointer

source

pub 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)
ensures
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.

source

pub 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)
ensures
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.

source

pub 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)
requires
valid_layout(size, align),
ensures
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,
source

pub 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)
requires
self.id() === old(perm)@.pptr,
old(perm)@.value === None,
ensures
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).

source

pub 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)
requires
self.id() === old(perm)@.pptr,
old(perm)@.value.is_Some(),
ensures
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.

source

pub 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)
requires
self.id() === old(perm)@.pptr,
old(perm)@.value.is_Some(),
ensures
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.

source

pub 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)
requires
self.id() === perm@.pptr,
perm@.value.is_Some(),
ensures
*v === perm@.value.get_Some_0(),

Given a shared borrow of the PointsTo<V>, obtain a shared borrow of V.

source

pub 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)
requires
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.

source

pub 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)
requires
perm.is_range(self.id(), size as int),
dealloc@.pptr === self.id(),
dealloc@.size === size as nat,
dealloc@.align === align as nat,
source

pub 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)
requires
self.id() === perm@.pptr,
perm@.pptr == dealloc@.pptr,
perm@.value.is_Some(),
ensures
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.

source

pub 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)
ensures
(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>

source

pub 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)
requires
self.id() === old(perm)@.pptr,
ensures
perm@.pptr === old(perm)@.pptr,
perm@.value === Some(in_v),
source

pub 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)
requires
self.id() === perm@.pptr,
perm@.value.is_Some(),
ensures
perm@.value === Some(out_v),

Trait Implementations§

source§

impl<A> Clone for PPtr<A>

source§

exec fn clone(&self) -> s : Self

ensures
s == *self,
1.0.0 · source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
source§

impl<A> Copy for PPtr<A>

source§

impl<T> Send for PPtr<T>

source§

impl<T> Sync for PPtr<T>

Auto Trait Implementations§

§

impl<V> Freeze for PPtr<V>

§

impl<V> RefUnwindSafe for PPtr<V>
where V: RefUnwindSafe,

§

impl<V> Unpin for PPtr<V>

§

impl<V> UnwindSafe for PPtr<V>
where V: RefUnwindSafe,

Blanket Implementations§

source§

impl<T> Any for T
where T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for T
where T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T, U> Into<U> for T
where U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T> ToOwned for T
where T: Clone,

§

type Owned = T

The resulting type after obtaining ownership.
source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

§

type Error = Infallible

The type returned in the event of a conversion error.
source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.