ostd::specs::mm::frame::meta_owners

Struct Metadata

pub struct Metadata<M: AnyFrameMeta> {
    pub metadata: M,
    pub ref_count: u64,
    pub vtable_ptr: MemContents<usize>,
    pub in_list: u64,
}

Fields§

§metadata: M§ref_count: u64§vtable_ptr: MemContents<usize>§in_list: u64

Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Metadata<M>

Source

pub uninterp fn metadata_from_inner_perms(perm: PointsTo<MetaSlotStorage>) -> M

The metadata value is an abstract function of the inner permissions, since extracting M from MetaSlotStorage requires M::Perm which is not stored in MetadataInnerPerms.

Trait Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> From<Metadata<Link<M>>> for MetadataAsLink<M>

Source §

exec fn from(m: Metadata<Link<M>>) -> Self

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> From<MetadataAsLink<M>> for Metadata<Link<M>>

Source §

exec fn from(m: MetadataAsLink<M>) -> Self

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> FromSpecImpl<Metadata<Link<M>>> for MetadataAsLink<M>

Source §

open spec fn obeys_from_spec() -> bool

{ true }

Source §

open spec fn from_spec(m: Metadata<Link<M>>) -> MetadataAsLink<M>

{
    MetadataAsLink {
        metadata: m.metadata.meta,
        next: match m.metadata.next {
            Some(repr_ptr) => Some(repr_ptr.ptr),
            None => None,
        },
        prev: match m.metadata.prev {
            Some(repr_ptr) => Some(repr_ptr.ptr),
            None => None,
        },
        ref_count: m.ref_count,
        vtable_ptr: m.vtable_ptr,
        in_list: m.in_list,
    }
}

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> FromSpecImpl<MetadataAsLink<M>> for Metadata<Link<M>>

Source §

open spec fn obeys_from_spec() -> bool

{ true }

Source §

open spec fn from_spec(m: MetadataAsLink<M>) -> Metadata<Link<M>>

{
    Metadata {
        metadata: Link {
            next: match m.next {
                Some(pptr) => {
                    Some(ReprPtr {
                        addr: pptr.addr(),
                        ptr: pptr,
                        _T: PhantomData,
                    })
                }
                None => None,
            },
            prev: match m.prev {
                Some(pptr) => {
                    Some(ReprPtr {
                        addr: pptr.addr(),
                        ptr: pptr,
                        _T: PhantomData,
                    })
                }
                None => None,
            },
            meta: m.metadata,
        },
        ref_count: m.ref_count,
        vtable_ptr: m.vtable_ptr,
        in_list: m.in_list,
    }
}

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Repr<MetaSlot> for Metadata<M>

Source §

open spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool

{
    &&& perm.storage.id() == r.storage.id()
    &&& perm.ref_count.id() == r.ref_count.id()
    &&& perm.vtable_ptr.pptr() == r.vtable_ptr
    &&& perm.in_list.id() == r.in_list.id()

}

Source §

uninterp fn to_repr_spec( self, perm: MetadataInnerPerms, ) -> (MetaSlot, MetadataInnerPerms)

Source §

exec fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot

Source §

open spec fn from_repr_spec(r: MetaSlot, perm: MetadataInnerPerms) -> Self

{
    Metadata {
        metadata: Self::metadata_from_inner_perms(perm.storage),
        ref_count: perm.ref_count.value(),
        vtable_ptr: perm.vtable_ptr.mem_contents(),
        in_list: perm.in_list.value(),
    }
}

Source §