Skip to main content

query_embedded

ostd::specs::mm::embedding::kvirt_store

Function query_embedded 

Source 
pub proof fn query_embedded<'rcu>(
    range: Range<Vaddr>,
    addr: Vaddr,
tracked     regions: &mut MetaRegionOwners,
tracked     kernel_pt: &mut PageTableOwner<KernelPtConfig>,
tracked     guards: &mut Guards<'rcu>,
    root_guard: PageTableGuard<'rcu, KernelPtConfig>,
) -> res : Option<MappedItem>
Expand description
requires
KERNEL_BASE_VADDR <= range.start,
range.end <= FRAME_METADATA_BASE_VADDR,
range.start % PAGE_SIZE == 0,
range.end % PAGE_SIZE == 0,
range.start <= range.end,
range.start <= addr < range.end,
old(regions).inv(),
old(kernel_pt).inv(),
old(kernel_pt).metaregion_sound(*old(regions)),
!(KVirtArea { range })
    .query_panic_condition(
        KVirtAreaOwner {
            pt_owner: *old(kernel_pt),
        },
        addr,
        *old(regions),
    ),
ensures
final(regions).inv(),
final(kernel_pt).inv(),
final(kernel_pt).metaregion_sound(*final(regions)),
({
    let area = KVirtArea { range };
    let owner = KVirtAreaOwner {
        pt_owner: *old(kernel_pt),
    };
    &&& area.query_some_condition(owner, addr)
        ==> area.query_some_ensures(owner, addr, res)
    &&& !area.query_some_condition(owner, addr) ==> KVirtArea::query_none_ensures(res)

}),

Trusted reflection of the (checkout/checkin-rewired, verified) [KVirtArea::query]. Mirrors its ensures verbatim, but threads the kernel page-table ownership by &mut (kernel_pt) instead of consuming a KVirtAreaOwner and returning it — so a KVmStore can keep kernel_pt across the call. The query clones the resolved leaf (bumping its slot’s refcount), then unlock_range hands the ownership back sound (inv() + metaregion_sound over the bumped region map). The query_panic_condition precondition is required false here: the embedding models only the non-panicking query.