ostd/mm/frame/
untyped.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Untyped physical memory management.
3//!
4//! As detailed in [`crate::mm::frame`], untyped memory can be accessed with
5//! relaxed rules but we cannot create references to them. This module provides
6//! the declaration of untyped frames and segments, and the implementation of
7//! extra functionalities (such as [`VmIo`]) for them.
8use vstd::prelude::*;
9
10use super::*;
11use crate::mm::{
12    io::{VmIoOwner, VmReader, VmWriter},
13    kspace::{
14        paddr_to_vaddr_spec, KERNEL_BASE_VADDR, KERNEL_END_VADDR, LINEAR_MAPPING_BASE_VADDR,
15        VMALLOC_BASE_VADDR,
16    },
17    paddr_to_vaddr,
18};
19use crate::specs::arch::kspace::{lemma_max_paddr_range, lemma_paddr_to_vaddr_properties};
20use crate::specs::mm::frame::meta_owners::MetaSlotStorage;
21use crate::specs::mm::virt_mem_newer::VirtPtr;
22use vstd_extra::ownership::OwnerOf;
23
24verus! {
25
26/// The metadata of untyped frame.
27///
28/// If a structure `M` implements [`AnyUFrameMeta`], it can be used as the
29/// metadata of a type of untyped frames [`Frame<M>`]. All frames of such type
30/// will be accessible as untyped memory.
31pub trait AnyUFrameMeta: AnyFrameMeta {
32
33}
34
35/// A smart pointer to an untyped frame with any metadata.
36///
37/// The metadata of the frame is not known at compile time but the frame must
38/// be an untyped one. An [`UFrame`] as a parameter accepts any type of
39/// untyped frame metadata.
40///
41/// The usage of this frame will not be changed while this object is alive.
42/// Verus doesn't let us do very much with `dyn` traits, so instead of a `dyn AnyFrameMeta`
43/// we use `MetaSlotStorage`, a type that is a tagged union of the metadata types we've worked with so far.
44pub type UFrame = Frame<MetaSlotStorage>;
45
46/// A physical memory range that is untyped.
47///
48/// Untyped frames or segments can be safely read and written by the kernel or
49/// the user.
50///
51/// TODO: Perhaps we also need to define this?
52pub trait UntypedMem {
53    /// Borrows a reader that can read the untyped memory.
54    fn reader(&self) -> VmReader<'_>;
55
56    /// Borrows a writer that can write the untyped memory.
57    fn writer(&self) -> VmWriter<'_>;
58}
59
60#[verus_verify]
61impl<M: AnyUFrameMeta + OwnerOf> Segment<M> {
62    #[inline(always)]
63    #[verus_spec(r =>
64        with
65            -> owner: Tracked<VmIoOwner<'_>>,
66        requires
67            self.inv(),
68        ensures
69            r.inv(),
70            owner@.inv(),
71            r.wf(owner@),
72            r.cursor.vaddr == paddr_to_vaddr_spec(self.start_paddr_spec()),
73            r.remain_spec() == self.size_spec(),
74            owner@.is_kernel,
75    )]
76    pub fn reader(&self) -> VmReader<'_> {
77        proof_decl! {
78            let ghost id: nat;
79            let tracked owner: VmIoOwner<'_>;
80        }
81        proof {
82            lemma_max_paddr_range();
83        }
84
85        let vaddr = paddr_to_vaddr(self.start_paddr());
86        let len = self.size();
87        let ghost range = vaddr..(vaddr + len) as usize;
88        let ptr = VirtPtr { vaddr, range: Ghost(range) };
89        proof {
90            lemma_paddr_to_vaddr_properties(self.start_paddr_spec());
91            assert(KERNEL_BASE_VADDR > 0) by (compute_only);
92            assert(vaddr > 0);
93            assert(VMALLOC_BASE_VADDR <= KERNEL_END_VADDR) by (compute_only);
94            assert(ptr.inv());
95        }
96
97        let reader = unsafe {
98            #[verus_spec(with Ghost(id) => Tracked(owner))]
99            VmReader::from_kernel_space(ptr, len)
100        };
101
102        proof_with!(|= Tracked(owner));
103        reader
104    }
105
106    #[inline(always)]
107    #[verus_spec(r =>
108        with
109            -> owner: Tracked<VmIoOwner<'_>>,
110        requires
111            self.inv(),
112        ensures
113            r.inv(),
114            owner@.inv(),
115            r.wf(owner@),
116            r.cursor.vaddr == paddr_to_vaddr_spec(self.start_paddr_spec()),
117            r.avail_spec() == self.size_spec(),
118            owner@.is_kernel,
119            !owner@.is_fallible,
120    )]
121    pub fn writer(&self) -> VmWriter<'_> {
122        proof_decl! {
123            let ghost id: nat;
124            let tracked owner: VmIoOwner<'_>;
125        }
126        proof {
127            lemma_max_paddr_range();
128        }
129
130        let vaddr = paddr_to_vaddr(self.start_paddr());
131        let len = self.size();
132        let ghost range = vaddr..(vaddr + len) as usize;
133        let ptr = VirtPtr { vaddr, range: Ghost(range) };
134        proof {
135            lemma_paddr_to_vaddr_properties(self.start_paddr_spec());
136            assert(KERNEL_BASE_VADDR > 0) by (compute_only);
137            assert(vaddr > 0);
138            assert(VMALLOC_BASE_VADDR <= KERNEL_END_VADDR) by (compute_only);
139            assert(ptr.inv());
140        }
141
142        let writer = unsafe {
143            #[verus_spec(with Ghost(id), Tracked(false) => Tracked(owner))]
144            VmWriter::from_kernel_space(ptr, len)
145        };
146
147        proof_with!(|= Tracked(owner));
148        writer
149    }
150}
151
152} // verus!
ostd/mm/frame/untyped.rs

ostd/mm/frame/
untyped.rs
