diff --git a/ostd/src/mm/heap/mod.rs b/ostd/src/mm/heap/mod.rs index 5dda22aa5..feb9e67b5 100644 --- a/ostd/src/mm/heap/mod.rs +++ b/ostd/src/mm/heap/mod.rs @@ -1,11 +1,14 @@ // SPDX-License-Identifier: MPL-2.0 //! Manages the kernel heap using slab or buddy allocation strategies. +use vstd::prelude::*; + use core::{ alloc::{AllocError, GlobalAlloc, Layout}, ptr::NonNull, }; use crate::mm::Vaddr; +use vstd_extra::external::alloc_types::*; mod slab; mod slot; @@ -17,6 +20,23 @@ pub use self::{ slot_list::SlabSlotList, }; +#[cfg(not(feature = "verify"))] +macro_rules! abort_with_message { + ($($arg:tt)*) => { + log::error!($($arg)*); + core::intrinsics::abort(); + }; +} + +#[cfg(feature = "verify")] +macro_rules! abort_with_message { + ($($arg:tt)*) => { + core::intrinsics::abort(); + }; +} + +verus! { + /// The trait for the global heap allocator. /// /// By providing the slab ([`Slab`]) and heap slot ([`HeapSlot`]) @@ -59,7 +79,12 @@ extern "Rust" { fn __GLOBAL_HEAP_SLOT_INFO_FROM_LAYOUT(layout: Layout) -> Option; } +pub assume_specification[__GLOBAL_HEAP_SLOT_INFO_FROM_LAYOUT]( + layout: Layout, +) -> Option; + /// Gets the reference to the user-defined global heap allocator. +#[verifier::external_body] fn get_global_heap_allocator() -> &'static dyn GlobalHeapAllocator { // SAFETY: This up-call is redirected safely to Rust code by OSDK. unsafe { __GLOBAL_HEAP_ALLOCATOR_REF } @@ -76,13 +101,7 @@ fn slot_size_from_layout(layout: Layout) -> Option { unsafe { __GLOBAL_HEAP_SLOT_INFO_FROM_LAYOUT(layout) } } -macro_rules! abort_with_message { - ($($arg:tt)*) => { - log::error!($($arg)*); - crate::panic::abort(); - }; -} - +/* #[alloc_error_handler] fn handle_alloc_error(layout: core::alloc::Layout) -> ! { abort_with_message!("Heap allocation error, layout = {:#x?}", layout); @@ -90,6 +109,7 @@ fn handle_alloc_error(layout: core::alloc::Layout) -> ! { #[global_allocator] static HEAP_ALLOCATOR: AllocDispatch = AllocDispatch; +*/ struct AllocDispatch; @@ -134,7 +154,11 @@ unsafe impl GlobalAlloc for AllocDispatch { // SAFETY: The validity of the pointer is guaranteed by the caller. The // size must match the size of the slot when it was allocated, since we // require `slot_size_from_layout` to be idempotent. - let slot = unsafe { HeapSlot::new(NonNull::new_unchecked(ptr), required_slot) }; + // let slot = unsafe { HeapSlot::new(NonNull::new_unchecked(ptr), required_slot) }; + let Some(nonnull_ptr) = NonNull::new(ptr) else { + abort_with_message!("Heap deallocation null pointer, layout = {:#x?}", layout); + }; + let slot = unsafe { HeapSlot::new(nonnull_ptr, required_slot) }; let res = get_global_heap_allocator().dealloc(slot); if res.is_err() { @@ -147,3 +171,5 @@ unsafe impl GlobalAlloc for AllocDispatch { } } } + +} // verus! diff --git a/ostd/src/mm/heap/slab.rs b/ostd/src/mm/heap/slab.rs index a37810edc..237e82e49 100644 --- a/ostd/src/mm/heap/slab.rs +++ b/ostd/src/mm/heap/slab.rs @@ -1,13 +1,22 @@ // SPDX-License-Identifier: MPL-2.0 //! Slabs for implementing the slab allocator. +use vstd::prelude::*; + use core::{alloc::AllocError, ptr::NonNull}; use super::{slot::HeapSlot, slot_list::SlabSlotList}; -use crate::mm::{ - FrameAllocOptions, PAGE_SIZE, UniqueFrame, - frame::{linked_list::Link, meta::AnyFrameMeta}, - paddr_to_vaddr, +use crate::{ + error::{Error, Error::NoMemory}, + mm::{ + PAGE_SIZE, + frame::{UniqueFrame, linked_list::Link, meta::AnyFrameMeta}, + }, + specs::mm::frame::linked_list::linked_list_owners::MetaSlotSmall, + specs::mm::frame::meta_region_owners::MetaRegionOwners, }; +use vstd_extra::cast_ptr::Repr; + +verus! { /// A slab. /// @@ -31,7 +40,6 @@ pub struct SlabMeta { /// /// Slots not inside the slab should not be in the list. free_list: SlabSlotList, - /// The number of allocated slots in the slab. /// /// Even if a slot is free, as long as it does not stay in the @@ -39,14 +47,69 @@ pub struct SlabMeta { nr_allocated: u16, } -unsafe impl Send for SlabMeta {} -unsafe impl Sync for SlabMeta {} +impl Repr for SlabMeta { + type Perm = (); + + open spec fn wf(_r: MetaSlotSmall, _perm: ()) -> bool { + true + } + + open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotSmall, ()) { + (MetaSlotSmall, perm) + } + + fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotSmall { + MetaSlotSmall + } + + closed spec fn from_repr_spec(_r: MetaSlotSmall, _perm: ()) -> Self { + SlabMeta { free_list: SlabSlotList::new_spec(), nr_allocated: 0 } + } + + fn from_repr(_r: MetaSlotSmall, Tracked(_perm): Tracked<&()>) -> Self { + SlabMeta { free_list: SlabSlotList::new(), nr_allocated: 0 } + } + + #[verifier::external_body] + fn from_borrowed<'a>(_r: &'a MetaSlotSmall, Tracked(_perm): Tracked<&'a ()>) -> &'a Self { + // Original metadata is stored in the frame slot; this representation + // shim is only for Verus's link metadata model. + unsafe { &*(_r as *const MetaSlotSmall as *const Self) } + } + + #[verifier::external_body] + proof fn from_to_repr(self, perm: ()) { + } + + #[verifier::external_body] + proof fn to_from_repr(r: MetaSlotSmall, perm: ()) { + } + + proof fn to_repr_wf(self, perm: ()) { + } +} + +#[verifier::external] +unsafe impl Send for SlabMeta { + +} + +#[verifier::external] +unsafe impl Sync for SlabMeta { + +} unsafe impl AnyFrameMeta for SlabMeta { - fn on_drop(&mut self, _reader: &mut crate::mm::VmReader) { + fn on_drop( + &mut self, + _reader: &mut crate::mm::VmReader, + Tracked(_regions): Tracked<&mut MetaRegionOwners>, + Tracked(_vm_io_owner): Tracked<&mut crate::specs::mm::io::VmIoOwner>, + ) { if self.nr_allocated != 0 { // FIXME: We have no mechanisms to forget the slab once we are here, // so we require the user to deallocate all slots before dropping. + #[cfg(feature = "allow_panic")] panic!("{} slots allocated when dropping a slab", self.nr_allocated); } } @@ -54,23 +117,55 @@ unsafe impl AnyFrameMeta for SlabMeta { fn is_untyped(&self) -> bool { false } + + uninterp spec fn vtable_ptr(&self) -> usize; } impl SlabMeta { + pub open spec fn valid_slot_size() -> bool { + &&& SLOT_SIZE >= core::mem::size_of::() + &&& SLOT_SIZE <= PAGE_SIZE + } + + pub open spec fn capacity_spec() -> usize + recommends + Self::valid_slot_size(), + { + PAGE_SIZE / SLOT_SIZE + } + + pub closed spec fn nr_allocated_spec(&self) -> u16 { + self.nr_allocated + } + /// Gets the capacity of the slab (regardless of the number of allocated slots). - pub const fn capacity(&self) -> u16 { + pub const fn capacity(&self) -> (res: u16) + requires + Self::valid_slot_size(), + ensures + res as usize == Self::capacity_spec(), + { (PAGE_SIZE / SLOT_SIZE) as u16 } /// Gets the number of allocated slots. - pub fn nr_allocated(&self) -> u16 { + pub fn nr_allocated(&self) -> (res: u16) + ensures + res == self.nr_allocated_spec(), + { self.nr_allocated } /// Allocates a slot from the slab. - pub fn alloc(&mut self) -> Result { + pub fn alloc(&mut self) -> (res: Result) + requires + old(self).nr_allocated_spec() < u16::MAX, + ensures + res is Ok ==> final(self).nr_allocated_spec() == old(self).nr_allocated_spec() + 1, + res is Err ==> final(self).nr_allocated_spec() == old(self).nr_allocated_spec(), + { let Some(allocated) = self.free_list.pop() else { - log::error!("Allocating a slot from a full slab"); + // log::error!("Allocating a slot from a full slab"); return Err(AllocError); }; self.nr_allocated += 1; @@ -78,6 +173,7 @@ impl SlabMeta { } } +/* impl Slab { /// Allocates a new slab of the given size. /// @@ -130,3 +226,5 @@ impl Slab { Ok(()) } } +*/ +} // verus! diff --git a/ostd/src/mm/heap/slot.rs b/ostd/src/mm/heap/slot.rs index 0185e6e85..53bbd25ca 100644 --- a/ostd/src/mm/heap/slot.rs +++ b/ostd/src/mm/heap/slot.rs @@ -1,15 +1,18 @@ // SPDX-License-Identifier: MPL-2.0 //! Heap slots for allocations. +use vstd::prelude::*; +use vstd_extra::external::nonnull::NonNullAdditionalFns; + use core::{alloc::AllocError, ptr::NonNull}; -use crate::{ - impl_frame_meta_for, - mm::{ - FrameAllocOptions, PAGE_SIZE, Paddr, Segment, Vaddr, kspace::LINEAR_MAPPING_BASE_VADDR, - paddr_to_vaddr, - }, +use crate::mm::{ + PAGE_SIZE, Paddr, Vaddr, + frame::meta::AnyFrameMeta, + kspace::{LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR}, }; +verus! { + /// A slot that will become or has been turned from a heap allocation. /// /// Heap slots can come from [`Slab`] or directly from a typed [`Segment`]. @@ -44,8 +47,18 @@ pub enum SlotInfo { } impl SlotInfo { + pub open spec fn size_spec(self) -> usize { + match self { + Self::SlabSlot(size) => size, + Self::LargeSlot(size) => size, + } + } + /// Gets the size of the slot. - pub fn size(&self) -> usize { + pub fn size(&self) -> (res: usize) + ensures + res == (*self).size_spec(), + { match self { Self::SlabSlot(size) => *size, Self::LargeSlot(size) => *size, @@ -54,6 +67,22 @@ impl SlotInfo { } impl HeapSlot { + pub closed spec fn info_spec(&self) -> SlotInfo { + self.info + } + + pub closed spec fn size_spec(&self) -> usize { + self.info_spec().size_spec() + } + + pub closed spec fn vaddr_spec(&self) -> Vaddr { + self.addr.view_ptr_mut().addr() + } + + pub closed spec fn in_linear_mapping_spec(&self) -> bool { + LINEAR_MAPPING_BASE_VADDR <= self.vaddr_spec() < VMALLOC_BASE_VADDR + } + /// Creates a new pointer to a heap slot. /// /// # Safety @@ -64,7 +93,11 @@ impl HeapSlot { /// /// If the pointer is from a [`super::Slab`] or [`Segment`], the slot must /// have a size that matches the slot size of the slab or segment respectively. - pub(super) unsafe fn new(addr: NonNull, info: SlotInfo) -> Self { + pub(super) unsafe fn new(addr: NonNull, info: SlotInfo) -> (res: Self) + ensures + res.info_spec() == info, + res.size_spec() == info.size_spec(), + { Self { addr, info } } @@ -77,8 +110,8 @@ impl HeapSlot { /// # Panics /// /// This function panics if the size is not a multiple of [`PAGE_SIZE`]. + /* pub fn alloc_large(size: usize) -> Result { - #[cfg(feature = "allow_panic")] assert_eq!(size % PAGE_SIZE, 0); let nframes = size / PAGE_SIZE; let segment = FrameAllocOptions::new() @@ -97,7 +130,7 @@ impl HeapSlot { info: SlotInfo::LargeSlot(size), }) } - + */ /// Deallocates a large slot. /// /// # Panics @@ -105,15 +138,13 @@ impl HeapSlot { /// This function aborts if the slot was not allocated with /// [`HeapSlot::alloc_large`], as it requires specific memory management /// operations that only apply to large slots. + /* pub fn dealloc_large(self) { let SlotInfo::LargeSlot(size) = self.info else { log::error!( "Deallocating a large slot that was not allocated with `HeapSlot::alloc_large`" ); - #[cfg(feature = "allow_panic")] crate::panic::abort(); - #[cfg(not(feature = "allow_panic"))] - return; }; debug_assert_eq!(size % PAGE_SIZE, 0); @@ -123,14 +154,26 @@ impl HeapSlot { // SAFETY: The segment was once forgotten when allocated. drop(unsafe { Segment::::from_raw(range) }); } - + */ /// Gets the physical address of the slot. - pub fn paddr(&self) -> Paddr { - self.addr.as_ptr() as Vaddr - LINEAR_MAPPING_BASE_VADDR + pub fn paddr(&self) -> (res: Paddr) + requires + self.in_linear_mapping_spec(), + ensures + res == crate::specs::arch::kspace::vaddr_to_paddr_spec(self.vaddr_spec()), + { + let vaddr = self.addr.as_ptr() as Vaddr; + proof { + self.addr.lemma_addr_view_eq_view_ptr_mut(); + } + crate::specs::arch::kspace::vaddr_to_paddr(vaddr) } /// Gets the size of the slot. - pub fn size(&self) -> usize { + pub fn size(&self) -> (res: usize) + ensures + res == self.size_spec(), + { match self.info { SlotInfo::SlabSlot(size) => size, SlotInfo::LargeSlot(size) => size, @@ -138,12 +181,18 @@ impl HeapSlot { } /// Gets the type and size of the slot. - pub fn info(&self) -> SlotInfo { + pub fn info(&self) -> (res: SlotInfo) + ensures + res == self.info_spec(), + { self.info } /// Gets the pointer to the slot. - pub fn as_ptr(&self) -> *mut u8 { + pub fn as_ptr(&self) -> (res: *mut u8) + ensures + !res.is_null(), + { self.addr.as_ptr() } } @@ -152,4 +201,8 @@ impl HeapSlot { #[derive(Debug)] pub struct LargeAllocFrameMeta; -impl_frame_meta_for!(LargeAllocFrameMeta); +unsafe impl AnyFrameMeta for LargeAllocFrameMeta { + uninterp spec fn vtable_ptr(&self) -> usize; +} + +} // verus! diff --git a/ostd/src/mm/heap/slot_list.rs b/ostd/src/mm/heap/slot_list.rs index f573d60e7..5e7d56ff7 100644 --- a/ostd/src/mm/heap/slot_list.rs +++ b/ostd/src/mm/heap/slot_list.rs @@ -1,9 +1,23 @@ // SPDX-License-Identifier: MPL-2.0 //! Implementation of the free heap slot list. +use vstd::prelude::*; + use core::ptr::NonNull; use super::HeapSlot; +verus! { + +pub assume_specification[ <*mut T>::write ](ptr: *mut T, val: T); + +pub assume_specification[ <*mut T>::read ](ptr: *mut T) -> T; + +pub assume_specification[ core::option::Option::::map_or ](_0: core::option::Option, _1: U, _2: F) -> U +where + F: core::ops::FnOnce(T,) -> U + core::marker::Destruct, + U: core::marker::Destruct, +; + /// A singly-linked list of [`HeapSlot`]s from [`super::Slab`]s. /// /// The slots inside this list will have a size of `SLOT_SIZE`. They can come @@ -18,18 +32,40 @@ pub struct SlabSlotList { // data pointed to by `head` requires a `&mut SlabSlotList`. Therefore, at any // given time, only one task can access the inner `head`. Additionally, a // `HeapSlot` will not be allocated again as long as it remains in the list. -unsafe impl Sync for SlabSlotList {} -unsafe impl Send for SlabSlotList {} +#[verifier::external] +unsafe impl Sync for SlabSlotList { + +} + +#[verifier::external] +unsafe impl Send for SlabSlotList { + +} impl Default for SlabSlotList { - fn default() -> Self { + fn default() -> (res: Self) + ensures + res.is_empty_spec(), + { Self::new() } } impl SlabSlotList { + pub closed spec fn is_empty_spec(&self) -> bool { + self.head is None + } + + pub closed spec fn new_spec() -> Self { + SlabSlotList { head: None } + } + /// Creates a new empty list. - pub const fn new() -> Self { + pub const fn new() -> (res: Self) + ensures + res.is_empty_spec(), + res == Self::new_spec(), + { Self { head: None } } @@ -47,15 +83,17 @@ impl SlabSlotList { #[cfg(feature = "allow_panic")] panic!("The slot does not come from a slab"); #[cfg(not(feature = "allow_panic"))] - return; + return; }; #[cfg(feature = "allow_panic")] assert_eq!(slot_size, SLOT_SIZE); + #[cfg(feature = "allow_panic")] const { assert!(SLOT_SIZE >= core::mem::size_of::()) }; let original_head = self.head; + #[cfg(feature = "allow_panic")] debug_assert!(!slot_ptr.is_null()); // SAFETY: A pointer to a slot must not be NULL; self.head = Some(unsafe { NonNull::new_unchecked(slot_ptr) }); @@ -63,9 +101,8 @@ impl SlabSlotList { // SAFETY: A heap slot must be free so the pointer to the slot can be // written to. The slot size is at least the size of a pointer. unsafe { - slot_ptr - .cast::() - .write(original_head.map_or(0, |h| h.as_ptr() as usize)); + // slot_ptr.cast::().write(original_head.map_or(0, |h| h.as_ptr() as usize)); + slot_ptr.cast::<*mut u8>().write(original_head.map_or(core::ptr::null_mut(), |h| h.as_ptr())); } } @@ -77,7 +114,8 @@ impl SlabSlotList { // SAFETY: The head is a valid pointer to a free slot. // The slot contains a pointer to the next slot. - let next = unsafe { original_head.as_ptr().cast::().read() } as *mut u8; + // let next = unsafe { original_head.as_ptr().cast::().read() } as *mut u8; + let next = unsafe { original_head.as_ptr().cast::<*mut u8>().read() }; self.head = if next.is_null() { None @@ -89,3 +127,5 @@ impl SlabSlotList { Some(unsafe { HeapSlot::new(original_head, super::SlotInfo::SlabSlot(SLOT_SIZE)) }) } } + +} // verus! diff --git a/ostd/src/mm/mod.rs b/ostd/src/mm/mod.rs index c8469d7a8..8d3439734 100644 --- a/ostd/src/mm/mod.rs +++ b/ostd/src/mm/mod.rs @@ -18,7 +18,7 @@ pub const MAX_NR_LEVELS: usize = 4; pub(crate) mod dma; pub mod frame; -//pub mod heap; +pub mod heap; pub mod io; pub use io::{ Fallible, FallibleVmRead, FallibleVmWrite, Infallible, VmIo, VmIoOnce, VmReader, VmWriter, diff --git a/verified_libs/vstd_extra/src/external/alloc_types.rs b/verified_libs/vstd_extra/src/external/alloc_types.rs new file mode 100644 index 000000000..a9a932e61 --- /dev/null +++ b/verified_libs/vstd_extra/src/external/alloc_types.rs @@ -0,0 +1,25 @@ +//! External type specifications for `core::alloc` types and related intrinsics. +use core::alloc::{AllocError, Layout}; +use vstd::prelude::*; + +verus! { + +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExLayout(Layout); + +#[verifier::external_type_specification] +pub struct ExAllocError(AllocError); + +pub assume_specification[ Layout::size ](layout: &Layout) -> usize +; + +pub assume_specification[ Layout::align ](layout: &Layout) -> (res: usize) + ensures + res != 0, +; + +pub assume_specification[ core::intrinsics::abort ]() -> ! +; + +} // verus! diff --git a/verified_libs/vstd_extra/src/external/mod.rs b/verified_libs/vstd_extra/src/external/mod.rs index d1db08d5c..1847a2fd4 100644 --- a/verified_libs/vstd_extra/src/external/mod.rs +++ b/verified_libs/vstd_extra/src/external/mod.rs @@ -2,6 +2,7 @@ //! //! These specifications are determined with careful inspection of the std library source code and documentation, and trusted as TCB. //! They are subject to change if `vstd` covers more cases in the future. +pub mod alloc_types; pub mod convert; pub mod deref; pub mod ilog2; @@ -13,6 +14,7 @@ pub mod range; pub mod slice; pub mod smart_ptr; +pub use alloc_types::*; pub use ilog2::*; pub use int_specs::*; pub use nonnull::*; diff --git a/verified_libs/vstd_extra/src/lib.rs b/verified_libs/vstd_extra/src/lib.rs index 519f29abf..b0344ac39 100644 --- a/verified_libs/vstd_extra/src/lib.rs +++ b/verified_libs/vstd_extra/src/lib.rs @@ -4,6 +4,7 @@ #![feature(nonzero_internals)] #![feature(sized_hierarchy)] #![feature(proc_macro_hygiene)] +#![feature(core_intrinsics)] #![cfg_attr(verus_keep_ghost, feature(allocator_api))] #![allow(non_snake_case)] #![allow(unused_parens)]