ostd/boot/
memory_region.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Information of memory regions in the boot phase.
3use vstd::prelude::*;
4use vstd_extra::prelude::*;
5
6use crate::specs::arch::*;
7
8use crate::mm::{Paddr, Vaddr};
9use align_ext::AlignExt;
10use core::ops::Deref;
11
12//use crate::mm::{kspace::kernel_loaded_offset, Paddr, Vaddr, PAGE_SIZE};
13
14/// The type of initial memory regions that are needed for the kernel.
15#[verus_verify]
16#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Debug)]
17pub enum MemoryRegionType {
18    /// Maybe points to an unplugged DIMM module. It's bad anyway.
19    BadMemory = 0,
20    /// Some holes not specified by the bootloader/firmware. It may be used for
21    /// I/O memory but we don't know for sure.
22    Unknown = 1,
23    /// In ACPI spec, this area needs to be preserved when sleeping.
24    NonVolatileSleep = 2,
25    /// Reserved by BIOS or bootloader, do not use.
26    Reserved = 3,
27    /// The place where kernel sections are loaded.
28    Kernel = 4,
29    /// The place where kernel modules (e.g. initrd) are loaded, could be reused.
30    Module = 5,
31    /// The memory region provided as the framebuffer.
32    Framebuffer = 6,
33    /// Once used in the boot phase. Kernel can reclaim it after initialization.
34    Reclaimable = 7,
35    /// Directly usable by the frame allocator.
36    Usable = 8,
37}
38
39/// The information of initial memory regions that are needed by the kernel.
40/// The sections are **not** guaranteed to not overlap. The region must be page aligned.
41#[verus_verify]
42#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Debug)]
43pub struct MemoryRegion {
44    base: usize,
45    len: usize,
46    typ: MemoryRegionType,
47}
48
49verus! {
50
51impl MemoryRegion {
52    #[verifier::type_invariant]
53    closed spec fn type_inv(self) -> bool {
54        self.base + self.len <= MAX_PADDR
55    }
56
57    /// Whether `self` is contained in `old_region`, with the same type.
58    pub closed spec fn is_sub_region(self, old_region: Self) -> bool {
59        self.typ == old_region.typ && old_region.base <= self.base && self.base + self.len
60            <= old_region.base + old_region.len
61    }
62
63    /// Whether the region shares no address with `region`.
64    pub closed spec fn is_separate(self, region: Self) -> bool {
65        self.base + self.len <= region.base || region.base + region.len <= self.base
66    }
67
68    /// Whether both boundaries of the region are multiples of `align`.
69    pub closed spec fn aligned(self, align: int) -> bool {
70        self.base as int % align == 0 && (self.base + self.len) % align == 0
71    }
72}
73
74} // verus!
75#[verus_verify]
76impl MemoryRegion {
77    /// Constructs a valid memory region.
78    #[verus_verify(dual_spec)]
79    #[verus_spec(
80        requires
81            base + len <= MAX_PADDR,
82        returns
83            Self::new(base, len, typ),
84    )]
85    pub const fn new(base: Paddr, len: usize, typ: MemoryRegionType) -> Self {
86        MemoryRegion { base, len, typ }
87    }
88
89    /// Constructs a bad memory region.
90    #[verus_verify(dual_spec)]
91    #[verus_spec(returns Self::bad())]
92    pub const fn bad() -> Self {
93        MemoryRegion {
94            base: 0,
95            len: 0,
96            typ: MemoryRegionType::BadMemory,
97        }
98    }
99
100    /*
101    /// Constructs a memory region where kernel sections are loaded.
102    ///
103    /// Most boot protocols do not mark the place where the kernel loads as unusable. In this case,
104    /// we need to explicitly construct and append this memory region.
105    pub fn kernel() -> Self {
106        // These are physical addresses provided by the linker script.
107        extern "C" {
108            fn __kernel_start();
109            fn __kernel_end();
110        }
111        MemoryRegion {
112            base: __kernel_start as usize - kernel_loaded_offset(),
113            len: __kernel_end as usize - __kernel_start as usize,
114            typ: MemoryRegionType::Kernel,
115        }
116    }
117
118    /// Constructs a framebuffer memory region.
119    pub fn framebuffer(fb: &crate::boot::BootloaderFramebufferArg) -> Self {
120        Self {
121            base: fb.address,
122            len: (fb.width * fb.height * fb.bpp).div_ceil(8), // round up when divide with 8 (bits/Byte)
123            typ: MemoryRegionType::Framebuffer,
124        }
125    }
126
127    /// Constructs a module memory region from a byte slice that lives in the linear mapping.
128    ///
129    /// # Panics
130    ///
131    /// This method will panic if the byte slice does not live in the linear mapping.
132    pub fn module(bytes: &[u8]) -> Self {
133        let vaddr = bytes.as_ptr() as Vaddr;
134        assert!(crate::mm::kspace::LINEAR_MAPPING_VADDR_RANGE.contains(&vaddr));
135
136        Self {
137            base: vaddr - crate::mm::kspace::LINEAR_MAPPING_BASE_VADDR,
138            len: bytes.len(),
139            typ: MemoryRegionType::Reclaimable,
140        }
141    } */
142
143    /// The physical address of the base of the region.
144    #[verus_verify(dual_spec)]
145    #[verus_spec(returns self.base())]
146    pub fn base(&self) -> Paddr {
147        self.base
148    }
149
150    /// The length in bytes of the region.
151    #[verus_verify(dual_spec)]
152    #[verus_spec(returns self.len())]
153    pub fn len(&self) -> usize {
154        self.len
155    }
156
157    /// The physical address of the end of the region.
158    #[verus_verify(dual_spec)]
159    #[verus_spec(returns self.end())]
160    pub fn end(&self) -> Paddr {
161        proof! {
162            use_type_invariant(self);
163        }
164        self.base + self.len
165    }
166
167    /// Checks whether the region is empty
168    #[verus_verify(dual_spec)]
169    #[verus_spec(returns self.is_empty())]
170    pub fn is_empty(&self) -> bool {
171        self.len == 0
172    }
173
174    /// The type of the region.
175    #[verus_verify(dual_spec)]
176    #[verus_spec(returns self.typ())]
177    pub fn typ(&self) -> MemoryRegionType {
178        self.typ
179    }
180
181    /// Returns the region with boundaries rounded to `PAGE_SIZE` boundaries:
182    /// inward for `Usable` regions, outward for the others.
183    #[verus_spec(ret =>
184        requires
185            self.typ == MemoryRegionType::Usable
186                ==> nat_align_up(self.base as nat, PAGE_SIZE as nat)
187                    <= nat_align_down((self.base + self.len) as nat, PAGE_SIZE as nat),
188        ensures
189            ret.typ == self.typ,
190            ret.aligned(PAGE_SIZE as int),
191            self.typ == MemoryRegionType::Usable
192                ==> ret.base == nat_align_up(self.base as nat, PAGE_SIZE as nat),
193            self.typ == MemoryRegionType::Usable
194                ==> ret.base + ret.len
195                    == nat_align_down((self.base + self.len) as nat, PAGE_SIZE as nat),
196            self.typ != MemoryRegionType::Usable
197                ==> ret.base == nat_align_down(self.base as nat, PAGE_SIZE as nat),
198            self.typ != MemoryRegionType::Usable
199                ==> ret.base + ret.len
200                    == nat_align_up((self.base + self.len) as nat, PAGE_SIZE as nat),
201            self.typ == MemoryRegionType::Usable
202                ==> ret.is_sub_region(*self),
203            self.typ != MemoryRegionType::Usable
204                ==> self.is_sub_region(ret),
205    )]
206    fn as_aligned(&self) -> Self {
207        proof! {
208            use_type_invariant(self);
209            lemma_pow2_is_pow2_to64();
210        }
211        let (base, end) = match self.typ() {
212            MemoryRegionType::Usable => (
213                self.base().align_up(PAGE_SIZE),
214                self.end().align_down(PAGE_SIZE),
215            ),
216            _ => (
217                self.base().align_down(PAGE_SIZE),
218                self.end().align_up(PAGE_SIZE),
219            ),
220        };
221        MemoryRegion {
222            base,
223            len: end - base,
224            typ: self.typ,
225        }
226    }
227}
228
229/// The maximum number of regions that can be handled.
230///
231/// The choice of 512 is probably fine since old Linux boot protocol only
232/// allows 128 regions.
233//
234// TODO: confirm the number or make it configurable.
235#[verus_verify]
236pub const MAX_REGIONS: usize = 512;
237
238/// A heapless set of memory regions.
239///
240/// The set cannot contain more than `LEN` regions.
241#[verus_verify]
242pub struct MemoryRegionArray<const LEN: usize = MAX_REGIONS> {
243    regions: [MemoryRegion; LEN],
244    count: usize,
245}
246
247verus! {
248
249impl<const LEN: usize> MemoryRegionArray<LEN> {
250    #[verifier::type_invariant]
251    closed spec fn type_inv(self) -> bool {
252        self.count <= LEN
253    }
254}
255
256impl<const LEN: usize> View for MemoryRegionArray<LEN> {
257    type V = Seq<MemoryRegion>;
258
259    closed spec fn view(&self) -> Seq<MemoryRegion> {
260        Seq::new(self.count as nat, |i: int| self.regions[i])
261    }
262}
263
264} // verus!
265#[verus_verify]
266impl<const LEN: usize> Default for MemoryRegionArray<LEN> {
267    #[verus_spec(ret =>
268        ensures
269            ret@ == Seq::<MemoryRegion>::empty()
270    )]
271    fn default() -> Self {
272        Self::new()
273    }
274}
275#[verus_verify]
276impl<const LEN: usize> Deref for MemoryRegionArray<LEN> {
277    type Target = [MemoryRegion];
278
279    #[verus_spec(ret =>
280        ensures
281            ret@ == self@,
282    )]
283    fn deref(&self) -> &Self::Target {
284        proof! {
285            use_type_invariant(self);
286        }
287        &self.regions[..self.count]
288    }
289}
290#[verus_verify]
291impl<const LEN: usize> MemoryRegionArray<LEN> {
292    /// Constructs an empty set.
293    #[verus_spec(ret =>
294        ensures
295            ret@ == Seq::<MemoryRegion>::empty(),
296    )]
297    pub const fn new() -> Self {
298        let ret = Self {
299            regions: [MemoryRegion::bad(); LEN],
300            count: 0,
301        };
302
303        proof! {
304            assert(ret@ == Seq::<MemoryRegion>::empty());
305        };
306
307        ret
308    }
309
310    /// Appends a region to the set.
311    ///
312    /// If the set is full, an error is returned.
313    #[verus_spec(ret =>
314        ensures
315            old(self)@.len() < LEN ==> {
316                &&& final(self)@ == old(self)@.push(region)
317                &&& ret.is_ok()
318            },
319            old(self)@.len() == LEN ==> {
320                &&& final(self)@ == old(self)@
321                &&& ret.is_err()
322            },
323    )]
324    pub fn push(&mut self, region: MemoryRegion) -> Result<(), &'static str> {
325        proof! {
326            use_type_invariant(&*self);
327        }
328        if self.count < self.regions.len() {
329            self.regions[self.count] = region;
330            self.count = self.count + 1;
331            proof! {
332                assert(self@ == old(self)@.push(region)) by {
333                    assert (forall |i: int| 0 <= i < self@.len() ==> #[trigger] self@[i] == old(self)@.push(region)[i]);
334                };
335            };
336            Ok(())
337        } else {
338            Err("MemoryRegionArray is full")
339        }
340    }
341    /*
342    /// Sorts the regions and returns a full set of non-overlapping regions.
343    ///
344    /// If an address is in multiple regions, the region with the lowest
345    /// usability will be its type.
346    ///
347    /// All the addresses between 0 and the end of the last region will be in
348    /// the resulting set. If an address is not in any region, it will be marked
349    /// as [`MemoryRegionType::Unknown`].
350    ///
351    /// If any of the region boundaries are not page-aligned, they will be aligned
352    /// according to the type of the region.
353    ///
354    /// # Panics
355    ///
356    /// This method will panic if the number of output regions is greater than `LEN`.
357    pub fn into_non_overlapping(mut self) -> Self {
358        let max_addr = self
359            .iter()
360            .map(|r| r.end())
361            .max()
362            .unwrap_or(0)
363            .align_down(PAGE_SIZE);
364        self.regions.iter_mut().for_each(|r| *r = r.as_aligned());
365
366        let mut result = MemoryRegionArray::<LEN>::new();
367
368        let mut cur_right = 0;
369
370        while cur_right < max_addr {
371            // Find the most restrictive type.
372            let typ = self
373                .iter()
374                .filter(|region| (region.base()..region.end()).contains(&cur_right))
375                .map(|region| region.typ())
376                .min()
377                .unwrap_or(MemoryRegionType::Unknown);
378
379            // Find the right boundary.
380            let right = self
381                .iter()
382                .filter_map(|region| {
383                    if region.base() > cur_right {
384                        Some(region.base())
385                    } else if region.end() > cur_right {
386                        Some(region.end())
387                    } else {
388                        None
389                    }
390                })
391                .min()
392                .unwrap();
393
394            result
395                .push(MemoryRegion::new(cur_right, right - cur_right, typ))
396                .unwrap();
397
398            cur_right = right;
399        }
400
401        // Merge the adjacent regions with the same type.
402        let mut merged_count = 1;
403        for i in 1..result.count {
404            if result[i].typ() == result.regions[merged_count - 1].typ() {
405                result.regions[merged_count - 1] = MemoryRegion::new(
406                    result.regions[merged_count - 1].base(),
407                    result.regions[merged_count - 1].len() + result[i].len(),
408                    result.regions[merged_count - 1].typ(),
409                );
410            } else {
411                result.regions[merged_count] = result[i];
412                merged_count += 1;
413            }
414        }
415        result.count = merged_count;
416
417        result
418    }*/
419}
420
421#[cfg(ktest)]
422mod test {
423    use super::*;
424    use crate::prelude::ktest;
425
426    #[ktest]
427    fn test_sort_full_non_overlapping() {
428        let mut regions = MemoryRegionArray::<64>::new();
429        // Regions that can be combined.
430        regions
431            .push(MemoryRegion::new(
432                0,
433                PAGE_SIZE + 1,
434                MemoryRegionType::Usable,
435            ))
436            .unwrap();
437        regions
438            .push(MemoryRegion::new(
439                PAGE_SIZE - 1,
440                PAGE_SIZE + 2,
441                MemoryRegionType::Usable,
442            ))
443            .unwrap();
444        regions
445            .push(MemoryRegion::new(
446                PAGE_SIZE * 2,
447                PAGE_SIZE * 5,
448                MemoryRegionType::Usable,
449            ))
450            .unwrap();
451        // A punctured region.
452        regions
453            .push(MemoryRegion::new(
454                PAGE_SIZE * 3 + 1,
455                PAGE_SIZE - 2,
456                MemoryRegionType::BadMemory,
457            ))
458            .unwrap();
459        // A far region that left a hole in the middle.
460        regions
461            .push(MemoryRegion::new(
462                PAGE_SIZE * 9,
463                PAGE_SIZE * 2,
464                MemoryRegionType::Usable,
465            ))
466            .unwrap();
467
468        let regions = regions.into_non_overlapping();
469
470        assert_eq!(regions.count, 5);
471        assert_eq!(regions[0].base(), 0);
472        assert_eq!(regions[0].len(), PAGE_SIZE * 3);
473        assert_eq!(regions[0].typ(), MemoryRegionType::Usable);
474
475        assert_eq!(regions[1].base(), PAGE_SIZE * 3);
476        assert_eq!(regions[1].len(), PAGE_SIZE);
477        assert_eq!(regions[1].typ(), MemoryRegionType::BadMemory);
478
479        assert_eq!(regions[2].base(), PAGE_SIZE * 4);
480        assert_eq!(regions[2].len(), PAGE_SIZE * 3);
481        assert_eq!(regions[2].typ(), MemoryRegionType::Usable);
482
483        assert_eq!(regions[3].base(), PAGE_SIZE * 7);
484        assert_eq!(regions[3].len(), PAGE_SIZE * 2);
485        assert_eq!(regions[3].typ(), MemoryRegionType::Unknown);
486
487        assert_eq!(regions[4].base(), PAGE_SIZE * 9);
488        assert_eq!(regions[4].len(), PAGE_SIZE * 2);
489        assert_eq!(regions[4].typ(), MemoryRegionType::Usable);
490    }
491}
ostd/boot/memory_region.rs

ostd/boot/
memory_region.rs
