pub unsafe trait NonNullPtr: Sized + 'static {
type Target;
type Permission: Inv;
const ALIGN_BITS: u32;
// Required methods
exec fn into_raw(self) -> (NonNull<Self::Target>, Tracked<Self::Permission>);
unsafe fn from_raw(
ptr: NonNull<Self::Target>,
perm: Tracked<Self::Permission>,
) -> Self;
spec fn ptr_perm_match(
ptr: NonNull<Self::Target>,
perm: Self::Permission,
) -> bool;
spec fn rel_perm(self, perm: Self::Permission) -> bool;
proof fn lemma_align_bits_range();
}Expand description
A trait that abstracts non-null pointers.
All common smart pointer types such as Box<T>, Arc<T>, and Weak<T>
implement this trait as they can be converted to and from the raw pointer
type of *const T.
§Safety
This trait must be implemented correctly (according to the doc comments for
each method). Types like Rcu rely on this assumption to safely use the
raw pointers.
Required Associated Constants§
Sourceconst ALIGN_BITS: u32
const ALIGN_BITS: u32
The power of two of the pointer alignment.
Required Associated Types§
Sourcetype Permission: Inv
type Permission: Inv
A verification-only permission type that represents the ownership of the memory managed by the pointer.
Required Methods§
Sourceexec fn into_raw(self) -> (NonNull<Self::Target>, Tracked<Self::Permission>)
exec fn into_raw(self) -> (NonNull<Self::Target>, Tracked<Self::Permission>)
Self::ptr_perm_match(res_ptr, perm@),self.rel_perm(perm@),perm@.inv(),res_ptr.view_ptr_mut().addr() % (1usize << Self::ALIGN_BITS) == 0,Converts to a raw pointer.
Each call to into_raw must be paired with a call to from_raw
in order to avoid memory leakage.
The lower Self::ALIGN_BITS of the raw pointer is guaranteed to
be zero. In other words, the pointer is guaranteed to be aligned to
1 << Self::ALIGN_BITS.
VERUS LIMITATION: the #[verus_spec] attribute does not support with in trait yet.
Sourceunsafe exec fn from_raw(
ptr: NonNull<Self::Target>,
perm: Tracked<Self::Permission>,
) -> ret : Self
unsafe exec fn from_raw( ptr: NonNull<Self::Target>, perm: Tracked<Self::Permission>, ) -> ret : Self
Self::ptr_perm_match(ptr, perm@),perm@.inv(),ret.rel_perm(perm@),Converts back from a raw pointer.
§Safety
- The raw pointer must have been previously returned by a call to
into_raw. - The raw pointer must not be used after calling
from_raw.
Note that the second point is a hard requirement: Even if the
resulting value has not (yet) been dropped, the pointer cannot be
used because it may break Rust aliasing rules (e.g., Box<T>
requires the pointer to be unique and thus never aliased).
VERIFICATION DESIGN: It’s easy to verify the second point by consuming the permission produced by into_raw,
so we can do nothing with the raw pointer because of the absence of permission.
VERUS LIMITATION: the #[verus_spec] attribute does not support with in trait yet.
Sourcespec fn ptr_perm_match(ptr: NonNull<Self::Target>, perm: Self::Permission) -> bool
spec fn ptr_perm_match(ptr: NonNull<Self::Target>, perm: Self::Permission) -> bool
A specification function that constraints the nonnull pointer and the permission returned by into_raw.
This design is to support the tagged pointer trick used in Either.
Sourcespec fn rel_perm(self, perm: Self::Permission) -> bool
spec fn rel_perm(self, perm: Self::Permission) -> bool
A specification function that relates the original smart pointer and the permission.
Sourceproof fn lemma_align_bits_range()
proof fn lemma_align_bits_range()
Self::ALIGN_BITS < usize::BITS,The ALIGN_BITS must be less than usize::BITS.
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl<T: 'static> NonNullPtr for Box<T>
impl<T: 'static> NonNullPtr for Box<T>
Source§unsafe exec fn from_raw(
ptr: NonNull<Self::Target>,
verus_tmp_perm: Tracked<Self::Permission>,
) -> Self
unsafe exec fn from_raw( ptr: NonNull<Self::Target>, verus_tmp_perm: Tracked<Self::Permission>, ) -> Self
Source§open spec fn ptr_perm_match(ptr: NonNull<Self::Target>, perm: Self::Permission) -> bool
open spec fn ptr_perm_match(ptr: NonNull<Self::Target>, perm: Self::Permission) -> bool
{ ptr.view_ptr_mut() == perm.ptr() }Source§open spec fn rel_perm(self, perm: Self::Permission) -> bool
open spec fn rel_perm(self, perm: Self::Permission) -> bool
{ perm.view_target() == *self }Source§proof fn lemma_align_bits_range()
proof fn lemma_align_bits_range()
const ALIGN_BITS: u32
type Target = T
type Permission = BoxPointsTo<T>
Source§impl<T: 'static> NonNullPtr for Arc<T>
impl<T: 'static> NonNullPtr for Arc<T>
Source§unsafe exec fn from_raw(
ptr: NonNull<Self::Target>,
verus_tmp_perm: Tracked<Self::Permission>,
) -> Self
unsafe exec fn from_raw( ptr: NonNull<Self::Target>, verus_tmp_perm: Tracked<Self::Permission>, ) -> Self
Source§open spec fn ptr_perm_match(ptr: NonNull<Self::Target>, perm: Self::Permission) -> bool
open spec fn ptr_perm_match(ptr: NonNull<Self::Target>, perm: Self::Permission) -> bool
{ ptr.view_ptr_mut() == perm.ptr() }Source§open spec fn rel_perm(self, perm: Self::Permission) -> bool
open spec fn rel_perm(self, perm: Self::Permission) -> bool
{ perm.view_target() == *self }