Module raw_ptr

Source
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.
DeallocData
Data associated with a Dealloc permission.
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
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.
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§

_verus_external_fn_specification_3__60__32__42__32_mut_32_T_32_as_32_PartialEq_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_PartialEq_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