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

ostd/mm/frame/
untyped.rs
