Struct PointsToRaw

Source

pub struct PointsToRaw { /* private fields */ }

Expand description

Variable-sized uninitialized memory.

Permission is for an arbitrary set of addresses, not necessarily contiguous, and with a given provenance.

Implementations§

Source §

impl PointsToRaw

Source

pub uninterp fn provenance(self) -> Provenance

Provenance of the PointsToRaw permission; this corresponds to the original allocation and does not change.

Source

pub uninterp fn dom(self) -> Set<int>

Memory addresses (domain) that the PointsToRaw permission gives access to. This set may be split apart and/or recombined, in order to create permissions to smaller pieces of the allocation.

Source

pub open spec fn is_range(self, start: int, len: int) -> bool

{ super::set_lib::set_int_range(start, start + len) =~= self.dom() }

Returns true if the domain of this permission is exactly the range [start, start + len).

Source

pub open spec fn contains_range(self, start: int, len: int) -> bool

{ super::set_lib::set_int_range(start, start + len) <= self.dom() }

Returns true if the domain of this permission contains the range [start, start + len).

Source

pub proof fn empty(provenance: Provenance) -> tracked points_to_raw : Self

ensures

points_to_raw.dom() == Set::<int>::empty(),

points_to_raw.provenance() == provenance,

Constructs a PointsToRaw permission over an empty domain with the given provenance.

Source

pub proof fn split(tracked self, range: Set<int>) -> tracked res : (Self, Self)

requires

range.subset_of(self.dom()),

ensures

res.0.provenance() == self.provenance(),

res.1.provenance() == self.provenance(),

res.0.dom() == range,

res.1.dom() == self.dom().difference(range),

Splits the current PointsToRaw permission into a permission with domain range and a permission containing the rest of the domain, provided that range is contained in the domain of the current permission.

Source

pub proof fn join(tracked self, tracked other: Self) -> tracked joined : Self

requires

self.provenance() == other.provenance(),

ensures

joined.provenance() == self.provenance(),

joined.dom() == self.dom() + other.dom(),

Joins two PointsToRaw permissions into one, provided that they have the same provenance. The memory addresses of the new permission is the union of the domains of self and other.

Source

pub proof fn into_typed<V>(tracked self, start: usize) -> tracked points_to : PointsTo<V>

requires

start as int % align_of::<V>() as int == 0,

self.is_range(start as int, size_of::<V>() as int),

ensures

points_to.ptr()
    == ptr_mut_from_data::<
        V,
    >(PtrData {
        addr: start,
        provenance: self.provenance(),
        metadata: (),
    }),

points_to.is_uninit(),

Creates a PointsTo<V> permission from a PointsToRaw permission with address start and the same provanance as the PointsToRaw permission, provided that start is aligned to V and that the domain of the PointsToRaw permission matches the size of V.

In combination with PointsToRaw::empty(), this lets us create a PointsTo for a ZST for any aligned pointer (any address and provenance, even null).