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::kspace::{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(vaddr > 0);
135            assert(VMALLOC_BASE_VADDR <= KERNEL_END_VADDR) by (compute_only);
136            assert(ptr.inv());
137        }
138
139        let reader = unsafe {
140            #[verus_spec(with Ghost(id) => Tracked(owner))]
141            VmReader::from_kernel_space(ptr, len)
142        };
143
144        proof_with!(|= Tracked(owner));
145        reader
146    }
147
148    #[inline(always)]
149    #[verus_spec(r =>
150        with
151            -> owner: Tracked<VmIoOwner>,
152        requires
153            self.inv(),
154        ensures
155            r.inv(),
156            owner@.inv(),
157            r.wf(owner@),
158            r.cursor.vaddr == paddr_to_vaddr_spec(self.start_paddr()),
159            r.avail_spec() == self.size(),
160            owner@.is_kernel,
161            !owner@.is_fallible,
162    )]
163    pub fn writer(&self) -> VmWriter<'_, Infallible> {
164        proof_decl! {
165            let ghost id: nat;
166            let tracked owner: VmIoOwner;
167        }
168        proof {
169            lemma_max_paddr_range();
170        }
171
172        let vaddr = paddr_to_vaddr(self.start_paddr());
173        let len = self.size();
174        let ghost range = vaddr..(vaddr + len) as usize;
175        let ptr = VirtPtr { vaddr, range: Ghost(range) };
176        proof {
177            lemma_paddr_to_vaddr_properties(self.start_paddr());
178            assert(KERNEL_BASE_VADDR > 0) by (compute_only);
179            assert(vaddr > 0);
180            assert(VMALLOC_BASE_VADDR <= KERNEL_END_VADDR) by (compute_only);
181            assert(ptr.inv());
182        }
183
184        let writer = unsafe {
185            #[verus_spec(with Ghost(id), Tracked(false) => Tracked(owner))]
186            VmWriter::from_kernel_space(ptr, len)
187        };
188
189        proof_with!(|= Tracked(owner));
190        writer
191    }
192}
193
194/*
195// Original impl_untyped_for! macro and its invocations (removed during Verus migration):
196// This macro provided UntypedMem + VmIo implementations for both Frame<UM> and Segment<UM>.
197
198macro_rules! impl_untyped_for {
199    ($t:ident) => {
200        impl<UM: AnyUFrameMeta + ?Sized> UntypedMem for $t<UM> {
201            fn reader(&self) -> VmReader<'_, Infallible> {
202                let ptr = paddr_to_vaddr(self.start_paddr()) as *const u8;
203                unsafe { VmReader::from_kernel_space(ptr, self.size()) }
204            }
205
206            fn writer(&self) -> VmWriter<'_, Infallible> {
207                let ptr = paddr_to_vaddr(self.start_paddr()) as *mut u8;
208                unsafe { VmWriter::from_kernel_space(ptr, self.size()) }
209            }
210        }
211
212        impl<UM: AnyUFrameMeta + ?Sized> VmIo for $t<UM> {
213            fn read(&self, offset: usize, writer: &mut VmWriter) -> Result<()> {
214                let read_len = writer.avail().min(self.size().saturating_sub(offset));
215                let max_offset = offset.checked_add(read_len).ok_or(Error::Overflow)?;
216                if max_offset > self.size() {
217                    return Err(Error::InvalidArgs);
218                }
219                let len = self
220                    .reader()
221                    .skip(offset)
222                    .read_fallible(writer)
223                    .map_err(|(e, _)| e)?;
224                debug_assert!(len == read_len);
225                Ok(())
226            }
227
228            fn write(&self, offset: usize, reader: &mut VmReader) -> Result<()> {
229                let write_len = reader.remain().min(self.size().saturating_sub(offset));
230                let max_offset = offset.checked_add(write_len).ok_or(Error::Overflow)?;
231                if max_offset > self.size() {
232                    return Err(Error::InvalidArgs);
233                }
234                let len = self
235                    .writer()
236                    .skip(offset)
237                    .write_fallible(reader)
238                    .map_err(|(e, _)| e)?;
239                debug_assert!(len == write_len);
240                Ok(())
241            }
242        }
243    };
244}
245
246impl_untyped_for!(Frame);
247impl_untyped_for!(Segment);
248*/
249} // verus!
ostd/mm/frame/untyped.rs

ostd/mm/frame/
untyped.rs
