Module raw_ptr 

Tools and reasoning principles for raw pointers. The tools here are meant to address “real Rust pointers, including all their subtleties on the Rust Abstract Machine, to the largest extent that is reasonable.”

For a gentler introduction to some of the concepts here, see PPtr, which uses a much-simplified pointer model.

Pointer model

A pointer consists of an address (ptr.addr() or ptr as usize), a provenance ptr@.provenance, and metadata ptr@.metadata (which is trivial except for pointers to non-sized types). Note that in spec code, pointer equality requires all 3 to be equal, whereas runtime equality (eq) only compares addresses and metadata.

*mut T vs. *const T do not have any semantic difference and Verus treats them as the same; they can be seamlessly cast to and fro.

Structs

Dealloc

Permission to perform a deallocation with the global allocator.

DeallocData

Data associated with a Dealloc permission.

FakeMetadata

IsExposed

Tracked object that indicates a given provenance has been exposed.

PointsTo

Permission to access possibly-initialized, typed memory.

PointsToData

Data associated with a PointsTo permission. We keep track of both the pointer and the (potentially uninitialized) value it points to.

PointsToRaw

Variable-sized uninitialized memory.

Provenance

Provenance

SharedReference

This is meant to be a replacement for &'a T that allows Verus to keep track of not just the T value but the pointer as well. It would be better to get rid of this and use normal reference types &'a T, but there are a lot of unsolved implementation questions. The existence of SharedReference<'a, T> is a stop-gap.

Enums

MemContents

Represents (typed) contents of memory.

Functions

allocate

Allocate with the global allocator. The precondition should be consistent with the documented safety conditions on alloc. Returns a pointer with a corresponding PointsToRaw and Dealloc permissions.

cast_array_ptr_to_slice_ptr

Cast a pointer to an array of length N to a slice pointer. Address and provenance are preserved; metadata has length N.

cast_ptr_to_thin_ptr

Cast a pointer to a thin pointer. Address and provenance are preserved; metadata is now thin.

cast_ptr_to_usize

Cast the address of a pointer to a usize.

cast_slice_ptr_to_slice_ptr

Cast a slice pointer to another slice pointer. Length is preserved even if the size of the elements changes.

cast_slice_ptr_to_str_ptr

Cast a slice pointer to a str pointer. Length is preserved even if the size of the elements changes.

cast_str_ptr_to_slice_ptr

Cast a str pointer to a slice pointer. Length is preserved even if the size of the elements changes.

deallocate

Deallocate with the global allocator.

expose_provenance

Perform a provenance expose operation.

group_raw_ptr_axioms

ptr_mut_read

Calls core::ptr::read to read from the memory pointed to by ptr, using the permission perm.

ptr_mut_ref

Equivalent to &mut *X, passing in a permission perm to ensure safety. The memory pointed to by ptr must be initialized.

ptr_mut_write

Calls core::ptr::write to write the value v to the memory location pointed to by ptr, using the permission perm.

ptr_ref

Equivalent to &*ptr, passing in a permission perm to ensure safety. The memory pointed to by ptr must be initialized.

ptr_ref2

Like ptr_ref but returns a SharedReference so it keeps track of the relationship between the pointers. Note the resulting reference’s pointers does NOT have the same provenance. This is because in Rust models like Stacked Borrows / Tree Borrows, the pointer gets a new tag.

with_exposed_provenance

Construct a pointer with the given provenance from a usize address. The provenance must have previously been exposed.

Type Aliases

Metadata