Struct PtrOwn 

pub struct PtrOwn<T: ?Sized>(/* private fields */);

Token that represents the ownership of a memory cell

A PtrOwn value only exists in the ghost world, but can be used in combination with a corresponding *const to access and modify memory.

A warning regarding memory leaks: dropping a Ghost<PtrOwn<T>> (we only ever handle ghost PtrOwn values) cannot deallocate the memory corresponding to the pointer because it is a ghost value. One must thus remember to explicitly call drop in order to free the memory tracked by a PtrOwn token.

Safety

When using Creusot to verify the code, all methods should be safe to call. Indeed, Creusot ensures that every operation on the inner value uses the right PtrOwn object created by PtrOwn::new, ensuring safety in a manner similar to ghost_cell.

#[check(terminates)]

PtrOwn methods, particularly constructors (new, from_box, from_ref, from_mut), are marked check(terminates) rather than check(ghost) to prevent two things from happening in ghost code:

1. running out of pointer addresses;
2. allocating too large objects.

Note that we already can’t guard against these issues in program code. But preventing them in ghost code is even more imperative to ensure soundness.

Specifically, creating too many pointers contradicts the PtrOwn::disjoint_lemma, and allocating too large objects contradicts the PtrOwn::invariant that allocations have size at most isize::MAX.

Implementations

impl<T: ?Sized> PtrOwn<T>

pub fn ptr(self) -> *const T

The raw pointer whose ownership is tracked by this PtrOwn

(opaque)

pub fn val<'a>(self) -> &'a T

The value currently stored at address self.ptr()

(opaque)

impl<T> PtrOwn<T>

pub fn new(v: T) -> (*mut T, Ghost<PtrOwn<T>>)

Creates a new PtrOwn and associated *const by allocating a new memory cell initialized with v.

terminates

ensures

result.1.ptr() == result.0 && *result.1.val() == v

pub fn disjoint_lemma(own1: &mut PtrOwn<T>, own2: &PtrOwn<T>)

If one owns two PtrOwns for non-zero sized types, then they are for different pointers.

terminates

ghost

requires

size_of_logic::<T>() != 0

ensures

own1.ptr().addr_logic() != own2.ptr().addr_logic()

ensures

*own1 == ^own1

impl<T: ?Sized> PtrOwn<T>

pub fn from_box(val: Box<T>) -> (*mut T, Ghost<PtrOwn<T>>)

Creates a ghost PtrOwn and associated *const from an existing Box.

terminates

ensures

result.1.ptr() == result.0 && *result.1.val() == *val

erasure

Box::into_raw

pub fn from_ref(r: &T) -> (*const T, Ghost<&PtrOwn<T>>)

Decompose a shared reference into a raw pointer and a ghost PtrOwn.

Erasure

This function erases to a raw reborrow of a reference.

PtrOwn::from_ref(r)
// erases to
r as *const T  // or *mut T (both are allowed)

terminates

ensures

result.1.ptr() == result.0

ensures

*result.1.val() == *r

pub fn from_mut(r: &mut T) -> (*mut T, Ghost<&mut PtrOwn<T>>)

Decompose a mutable reference into a raw pointer and a ghost PtrOwn.

Erasure

This function erases to a raw reborrow of a reference.

PtrOwn::from_mut(r)
// erases to
r as *const T  // or *mut T (both are allowed)

terminates

ensures

result.1.ptr() == result.0

ensures

*result.1.val() == *r

ensures

*(^result.1.inner_logic()).val() == ^r

pub unsafe fn as_ref(ptr: *const T, own: Ghost<&PtrOwn<T>>) -> &T

Immutably borrows the underlying T.

Safety

Safety requirements are the same as a direct dereference: &*ptr.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

Erasure

This function erases to a cast from raw pointer to shared reference.

PtrOwn::as_ref(ptr, own)
// erases to
& *ptr

terminates

requires

ptr == own.ptr()

ensures

*result == *own.val()

pub unsafe fn as_mut(ptr: *mut T, own: Ghost<&mut PtrOwn<T>>) -> &mut T

Mutably borrows the underlying T.

Safety

Safety requirements are the same as a direct dereference: &mut *ptr.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

Erasure

This function erases to a cast from raw pointer to mutable reference.

PtrOwn::as_mut(ptr, own)
// erases to
&mut *ptr

terminates

requires

ptr as *const T == own.ptr()

ensures

*result == *own.val()

ensures

(^own).ptr() == own.ptr()

ensures

*(^own).val() == ^result

pub unsafe fn to_box(ptr: *mut T, own: Ghost<PtrOwn<T>>) -> Box<T>

Transfers ownership of own back into a Box.

Safety

Safety requirements are the same as Box::from_raw.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

terminates

requires

ptr as *const T == own.ptr()

ensures

*result == *own.val()

erasure

Box::from_raw

pub unsafe fn drop(ptr: *mut T, own: Ghost<PtrOwn<T>>)

Deallocates the memory pointed by ptr.

Safety

Safety requirements are the same as Box::from_raw.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

terminates

requires

ptr as *const T == own.ptr()

pub fn ptr_is_aligned_lemma(&self)

The pointer of a PtrOwn is always aligned.

terminates

ghost

ensures

self.ptr().is_aligned_logic()

pub fn ptr_is_aligned_opaque(self) -> bool

Opaque wrapper around [std::ptr::is_aligned_logic]. We use this to hide alignment logic by default in invariant because it confuses SMT solvers sometimes. The underlying property is exposed by PtrOwn::ptr_is_aligned_lemma.

(open(pub(self)))

Trait Implementations

impl<T: ?Sized> Invariant for PtrOwn<T>

fn invariant(self) -> bool

(open, prophetic)

pearlite! {
    !self.ptr().is_null_logic()
        && self.ptr_is_aligned_opaque()
        && metadata_matches(*self.val(), metadata_logic(self.ptr()))
        // Allocations can never be larger than `isize` (source: https://doc.rust-lang.org/std/ptr/index.html#allocation)
        && size_of_val_logic(*self.val()) <= isize::MAX@
        // The allocation fits in the address space
        // (this is needed to verify (a `PtrOwn` variant of) `<*const T>::add`, which checks this condition)
        && self.ptr().addr_logic()@ + size_of_val_logic(*self.val()) <= usize::MAX@
        && inv(self.val())
}