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::*;
9use vstd_extra::ownership::OwnerOf;
10
11use crate::specs::{
12    arch::{lemma_max_paddr_range, lemma_paddr_to_vaddr_properties},
13    mm::{frame::meta_owners::MetaSlotStorage, io::VmIoOwner, virt_mem::VirtPtr},
14};
15
16use super::*;
17use crate::mm::{
18    io::{Infallible, VmReader, VmWriter},
19    kspace::{KERNEL_BASE_VADDR, KERNEL_END_VADDR, LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR},
20    paddr_to_vaddr,
21};
22
23verus! {
24
25/// The metadata of untyped frame.
26///
27/// If a structure `M` implements [`AnyUFrameMeta`], it can be used as the
28/// metadata of a type of untyped frames [`Frame<M>`]. All frames of such type
29/// will be accessible as untyped memory.
30///
31/// `Repr<MetaSlotStorage>` is required so that `Frame<M>` is well-formed (it
32/// is no longer an `AnyFrameMeta` supertrait). This makes `AnyUFrameMeta`
33/// itself dyn-incompatible — `Segment<dyn AnyUFrameMeta>` (the `USegment`
34/// alias below) was already in an unsatisfiable state under the old
35/// supertrait chain, so this doesn't lose anything in practice.
36pub trait AnyUFrameMeta: AnyFrameMeta + vstd_extra::cast_ptr::Repr<MetaSlotStorage> {
37
38}
39
40/// A smart pointer to an untyped frame with any metadata.
41///
42/// The metadata of the frame is not known at compile time but the frame must
43/// be an untyped one. An [`UFrame`] as a parameter accepts any type of
44/// untyped frame metadata.
45///
46/// The usage of this frame will not be changed while this object is alive.
47/// Verus doesn't let us do very much with `dyn` traits, so instead of a `dyn AnyFrameMeta`
48/// we use `MetaSlotStorage`, a type that is a tagged union of the metadata types we've worked with so far.
49pub type UFrame = Frame<MetaSlotStorage>;
50
51/*
52/// Makes a structure usable as untyped frame metadata.
53///
54/// If this macro is used for built-in typed frame metadata, it won't compile.
55#[macro_export]
56macro_rules! impl_untyped_frame_meta_for {
57    // Implement without specifying the drop behavior.
58    ($t:ty) => {
59        // SAFETY: Untyped frames can be safely read.
60        unsafe impl $crate::mm::frame::meta::AnyFrameMeta for $t {
61            fn is_untyped(&self) -> bool {
62                true
63            }
64        }
65        impl $crate::mm::frame::untyped::AnyUFrameMeta for $t {}
66    };
67    // Implement with a customized drop function.
68    ($t:ty, $body:expr) => {
69        // SAFETY: Untyped frames can be safely read.
70        unsafe impl $crate::mm::frame::meta::AnyFrameMeta for $t {
71            fn on_drop(&mut self, reader: &mut $crate::mm::VmReader<$crate::mm::Infallible>) {
72                $body
73            }
74
75            fn is_untyped(&self) -> bool {
76                true
77            }
78        }
79        impl $crate::mm::frame::untyped::AnyUFrameMeta for $t {}
80    };
81}
82
83// A special case of untyped metadata is the unit type.
84impl_untyped_frame_meta_for!(()); */
85
86/// A physical memory range that is untyped.
87///
88/// Untyped frames or segments can be safely read and written by the kernel or
89/// the user.
90///
91/// TODO: Perhaps we also need to define this?
92pub trait UntypedMem {
93    /// Borrows a reader that can read the untyped memory.
94    fn reader(&self) -> VmReader<'_, Infallible>;
95
96    /// Borrows a writer that can write the untyped memory.
97    fn writer(&self) -> VmWriter<'_, Infallible>;
98}
99
100#[verus_verify]
101impl<M: AnyUFrameMeta + OwnerOf> Segment<M> {
102    #[inline(always)]
103    #[verus_spec(r =>
104        with
105            -> owner: Tracked<VmIoOwner>,
106        requires
107            self.inv(),
108        ensures
109            r.inv(),
110            owner@.inv(),
111            r.wf(owner@),
112            r.cursor.vaddr == paddr_to_vaddr(self.start_paddr()),
113            r.remain_spec() == self.size(),
114            owner@.is_kernel,
115    )]
116    pub fn reader(&self) -> VmReader<'_, Infallible> {
117        proof_decl! {
118            let ghost id: nat;
119            let tracked owner: VmIoOwner;
120        }
121        proof {
122            lemma_max_paddr_range();
123        }
124
125        let vaddr = paddr_to_vaddr(self.start_paddr());
126        let len = self.size();
127        let ghost range = vaddr..(vaddr + len) as usize;
128        let ptr = VirtPtr { vaddr, range: Ghost(range) };
129        proof {
130            lemma_paddr_to_vaddr_properties(self.start_paddr());
131            assert(KERNEL_BASE_VADDR > 0) by (compute_only);
132            assert(VMALLOC_BASE_VADDR <= KERNEL_END_VADDR) by (compute_only);
133        }
134
135        let reader = unsafe {
136            #[verus_spec(with Ghost(id) => Tracked(owner))]
137            VmReader::from_kernel_space(ptr, len)
138        };
139
140        proof_with!(|= Tracked(owner));
141        reader
142    }
143
144    #[inline(always)]
145    #[verus_spec(r =>
146        with
147            -> owner: Tracked<VmIoOwner>,
148        requires
149            self.inv(),
150        ensures
151            r.inv(),
152            owner@.inv(),
153            r.wf(owner@),
154            r.cursor.vaddr == paddr_to_vaddr(self.start_paddr()),
155            r.avail_spec() == self.size(),
156            owner@.is_kernel,
157            !owner@.is_fallible,
158    )]
159    pub fn writer(&self) -> VmWriter<'_, Infallible> {
160        proof_decl! {
161            let ghost id: nat;
162            let tracked owner: VmIoOwner;
163        }
164        proof {
165            lemma_max_paddr_range();
166        }
167
168        let vaddr = paddr_to_vaddr(self.start_paddr());
169        let len = self.size();
170        let ghost range = vaddr..(vaddr + len) as usize;
171        let ptr = VirtPtr { vaddr, range: Ghost(range) };
172        proof {
173            lemma_paddr_to_vaddr_properties(self.start_paddr());
174            assert(KERNEL_BASE_VADDR > 0) by (compute_only);
175            assert(VMALLOC_BASE_VADDR <= KERNEL_END_VADDR) by (compute_only);
176        }
177
178        let writer = unsafe {
179            #[verus_spec(with Ghost(id), Tracked(false) => Tracked(owner))]
180            VmWriter::from_kernel_space(ptr, len)
181        };
182
183        proof_with!(|= Tracked(owner));
184        writer
185    }
186}
187
188/*
189// Original impl_untyped_for! macro and its invocations (removed during Verus migration):
190// This macro provided UntypedMem + VmIo implementations for both Frame<UM> and Segment<UM>.
191
192macro_rules! impl_untyped_for {
193    ($t:ident) => {
194        impl<UM: AnyUFrameMeta + ?Sized> UntypedMem for $t<UM> {
195            fn reader(&self) -> VmReader<'_, Infallible> {
196                let ptr = paddr_to_vaddr(self.start_paddr()) as *const u8;
197                unsafe { VmReader::from_kernel_space(ptr, self.size()) }
198            }
199
200            fn writer(&self) -> VmWriter<'_, Infallible> {
201                let ptr = paddr_to_vaddr(self.start_paddr()) as *mut u8;
202                unsafe { VmWriter::from_kernel_space(ptr, self.size()) }
203            }
204        }
205
206        impl<UM: AnyUFrameMeta + ?Sized> VmIo for $t<UM> {
207            fn read(&self, offset: usize, writer: &mut VmWriter) -> Result<()> {
208                let read_len = writer.avail().min(self.size().saturating_sub(offset));
209                let max_offset = offset.checked_add(read_len).ok_or(Error::Overflow)?;
210                if max_offset > self.size() {
211                    return Err(Error::InvalidArgs);
212                }
213                let len = self
214                    .reader()
215                    .skip(offset)
216                    .read_fallible(writer)
217                    .map_err(|(e, _)| e)?;
218                debug_assert!(len == read_len);
219                Ok(())
220            }
221
222            fn write(&self, offset: usize, reader: &mut VmReader) -> Result<()> {
223                let write_len = reader.remain().min(self.size().saturating_sub(offset));
224                let max_offset = offset.checked_add(write_len).ok_or(Error::Overflow)?;
225                if max_offset > self.size() {
226                    return Err(Error::InvalidArgs);
227                }
228                let len = self
229                    .writer()
230                    .skip(offset)
231                    .write_fallible(reader)
232                    .map_err(|(e, _)| e)?;
233                debug_assert!(len == write_len);
234                Ok(())
235            }
236        }
237    };
238}
239
240impl_untyped_for!(Frame);
241impl_untyped_for!(Segment);
242*/
243} // verus!
ostd/mm/frame/untyped.rs

ostd/mm/frame/
untyped.rs
