Expand description
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.
- Dealloc
Data - Data associated with a
Dealloc
permission. - IsExposed
- Tracked object that indicates a given provenance has been exposed.
- Points
To - Permission to access possibly-initialized, typed memory.
- Points
ToData - Data associated with a
PointsTo
permission. We keep track of both the pointer and the (potentially uninitialized) value it points to. - Points
ToRaw - Variable-sized uninitialized memory.
- Provenance
- Provenance
- PtrData
- Model of a pointer
*mut T
or*const T
in Rust’s abstract machine. In addition to the address, each pointer has its corresponding provenance and metadata. - Shared
Reference - This is meant to be a replacement for
&'a T
that allows Verus to keep track of not just theT
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 ofSharedReference<'a, T>
is a stop-gap.
Enums§
- MemContents
- Represents (typed) contents of memory.
Functions§
- _verus_
external_ ⚠fn_ specification_ 3__ 60__ 32__ 42__ 32_ mut_ 32_ T_ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32__ 42__ 32_ mut_ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ eq - _verus_
external_ ⚠fn_ specification_ 4__ 60__ 32__ 42__ 32_ const_ 32_ T_ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32__ 42__ 32_ const_ 32_ T_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ eq - _verus_
external_ ⚠fn_ specification_ 5_ core_ 32__ 58__ 58__ 32_ ptr_ 32__ 58__ 58__ 32_ null - _verus_
external_ ⚠fn_ specification_ 6_ core_ 32__ 58__ 58__ 32_ ptr_ 32__ 58__ 58__ 32_ null__ mut - allocate
- axiom_
ptr_ mut_ from_ data - cast_
array_ ptr_ to_ slice_ ptr - cast_
ptr_ to_ thin_ ptr - cast_
ptr_ to_ usize - deallocate
- expose_
provenance - group_
raw_ ptr_ axioms - ptr_
from_ data - ptr_
mut_ from_ data - ptr_
mut_ read - ptr_
mut_ write - ptr_
null - ptr_
null_ mut - ptr_ref
- ptr_
ref2 - ptrs_
mut_ eq - ptrs_
mut_ eq_ sized - spec_
cast_ array_ ptr_ to_ slice_ ptr - spec_
cast_ ptr_ to_ thin_ ptr - spec_
cast_ ptr_ to_ usize - with_
exposed_ provenance
Type Aliases§
- Metadata
- Metadata