pub unsafe trait AnyFrameMeta: Send + Sync {
// Required method
spec fn vtable_ptr(&self) -> usize
where Self: Sized;
// Provided methods
open spec fn on_drop_pre(
&self,
reader: VmReader<'_, Infallible>,
regions: MetaRegionOwners,
vm_io_owner: VmIoOwner,
) -> bool { ... }
fn on_drop(
&mut self,
_reader: &mut VmReader<'_, Infallible>,
verus_tmp__regions: Tracked<&mut MetaRegionOwners>,
verus_tmp__vm_io_owner: Tracked<&mut VmIoOwner>,
) { ... }
fn is_untyped(&self) -> bool { ... }
}Expand description
All frame metadata types must implement this trait.
If a frame type needs specific drop behavior, it should specify
when implementing this trait. When we drop the last handle to
this frame, the on_drop method will be called. The on_drop
method is called with the physical address of the frame.
The implemented structure should have a size less than or equal to
[FRAME_METADATA_MAX_SIZE] and an alignment less than or equal to
FRAME_METADATA_MAX_ALIGN. Otherwise, the metadata type cannot
be used because storing it will fail compile-time assertions.
§Safety
If on_drop reads the page using the provided VmReader, the
implementer must ensure that the frame is safe to read.
Required Methods§
Sourcespec fn vtable_ptr(&self) -> usizewhere
Self: Sized,
spec fn vtable_ptr(&self) -> usizewhere
Self: Sized,
Provided Methods§
Sourceopen spec fn on_drop_pre(
&self,
reader: VmReader<'_, Infallible>,
regions: MetaRegionOwners,
vm_io_owner: VmIoOwner,
) -> bool
open spec fn on_drop_pre( &self, reader: VmReader<'_, Infallible>, regions: MetaRegionOwners, vm_io_owner: VmIoOwner, ) -> bool
{ true }Per-impl precondition for Self::on_drop. Default is true.
Impls that need richer caller-side invariants (e.g. the PT-node’s
reader/region invariants) override this; the trait method’s
requires clause calls it.
Sourceexec fn on_drop(
&mut self,
_reader: &mut VmReader<'_, Infallible>,
verus_tmp__regions: Tracked<&mut MetaRegionOwners>,
verus_tmp__vm_io_owner: Tracked<&mut VmIoOwner>,
)
exec fn on_drop( &mut self, _reader: &mut VmReader<'_, Infallible>, verus_tmp__regions: Tracked<&mut MetaRegionOwners>, verus_tmp__vm_io_owner: Tracked<&mut VmIoOwner>, )
old(_regions).inv(),old(_reader).inv(),old(_vm_io_owner).inv(),old(_reader).wf(*old(_vm_io_owner)),old(self).on_drop_pre(*old(_reader), *old(_regions), *old(_vm_io_owner)),final(_regions).inv(),final(_reader).inv(),final(_vm_io_owner).inv(),final(_reader).wf(*final(_vm_io_owner)),Sourceexec fn is_untyped(&self) -> res : bool
exec fn is_untyped(&self) -> res : bool
Implementors§
impl AnyFrameMeta for MetaSlotStorage
MetaSlotStorage is an inductive tagged union of all of the frame meta types that
we work with in this development. So, it should itself implement AnyFrameMeta, and
it can then be used to stand in for dyn AnyFrameMeta.