diff --git a/Cargo.lock b/Cargo.lock index 3dc567b7e..212960889 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -674,6 +674,7 @@ version = "0.1.0" dependencies = [ "bitvec", "vstd", + "x86_64", ] [[package]] diff --git a/README.md b/README.md index 52e1f12da..f45609b82 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ [![verify (verus-lang/verus)](https://img.shields.io/github/actions/workflow/status/asterinas/vostd/ci-upstream-verus.yml?branch=main&label=verify%20(verus-lang%2Fverus))](https://github.com/asterinas/vostd/actions/workflows/ci-upstream-verus.yml) > [!NOTE] -> This repository is currently in a transitional state: the components under `ostd/src/sync` and `ostd/libs/id-alloc` already track the upcoming Asterinas release [v0.18.1](https://github.com/asterinas/asterinas/releases/tag/v0.18.1), while every other OSTD component is still based on [v0.16.0](https://github.com/asterinas/asterinas/releases/tag/v0.16.0). +> This repository is currently in a transitional state: the components under `ostd/src/sync`, `ostd/libs/id-alloc` and `ostd/src/io/io_port` already track the upcoming Asterinas release [v0.18.1](https://github.com/asterinas/asterinas/releases/tag/v0.18.1), while every other OSTD component is still based on [v0.16.0](https://github.com/asterinas/asterinas/releases/tag/v0.16.0). ## Overview diff --git a/ostd/src/arch/x86/device/io_port.rs b/ostd/src/arch/x86/device/io_port.rs index 74f7bbadf..c2d0399b6 100644 --- a/ostd/src/arch/x86/device/io_port.rs +++ b/ostd/src/arch/x86/device/io_port.rs @@ -1,5 +1,7 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port access. +pub use vstd_extra::external::{group_io_port_models, valid_io_port_access}; + pub use x86_64::{ instructions::port::{ PortReadAccess as IoPortReadAccess, PortWriteAccess as IoPortWriteAccess, ReadOnlyAccess, diff --git a/ostd/src/arch/x86/device/mod.rs b/ostd/src/arch/x86/device/mod.rs index 5d3b7fe3c..5e260d494 100644 --- a/ostd/src/arch/x86/device/mod.rs +++ b/ostd/src/arch/x86/device/mod.rs @@ -1,6 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 //! Device-related APIs. //! This module mainly contains the APIs that should exposed to the device driver like PCI, RTC -pub mod cmos; +/*pub mod cmos;*/ pub mod io_port; -pub mod serial; +/*pub mod serial;*/ diff --git a/ostd/src/arch/x86/io.rs b/ostd/src/arch/x86/io.rs index b78d04f26..36fe128a4 100644 --- a/ostd/src/arch/x86/io.rs +++ b/ostd/src/arch/x86/io.rs @@ -1,4 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 +use vstd::prelude::*; + use alloc::vec::Vec; use align_ext::AlignExt; @@ -55,6 +57,6 @@ pub(super) fn construct_io_mem_allocator_builder() -> IoMemAllocatorBuilder { // SAFETY: The range is guaranteed not to access physical memory. unsafe { IoMemAllocatorBuilder::new(ranges) } } - /// Port I/O definition reference: . +#[verus_verify] pub const MAX_IO_PORT: u16 = u16::MAX; diff --git a/ostd/src/arch/x86/mod.rs b/ostd/src/arch/x86/mod.rs index df7a81de1..db3d91a44 100644 --- a/ostd/src/arch/x86/mod.rs +++ b/ostd/src/arch/x86/mod.rs @@ -1,16 +1,16 @@ // SPDX-License-Identifier: MPL-2.0 //! Platform-specific code for the x86 platform. /*pub mod boot; -pub(crate) mod cpu; +pub(crate) mod cpu;*/ pub mod device; -pub(crate) mod ex_table; +/*pub(crate) mod ex_table;*/ pub(crate) mod io; -pub(crate) mod iommu;*/ +/*pub(crate) mod iommu;*/ pub(crate) mod irq; /* pub(crate) mod kernel; */ pub(crate) mod mm; -/*pub(crate) mod pci; -pub mod qemu; +pub(crate) mod pci; +/*pub mod qemu; pub(crate) mod serial; pub(crate) mod task; */ pub mod timer; @@ -212,7 +212,7 @@ pub(crate) fn enable_cpu_features() { *efer |= EferFlags::NO_EXECUTE_ENABLE; }); } -} +}*/ /// Inserts a TDX-specific code block. /// @@ -251,4 +251,3 @@ macro_rules! if_tdx_enabled { } pub use if_tdx_enabled; -*/ diff --git a/ostd/src/arch/x86/pci.rs b/ostd/src/arch/x86/pci.rs index e212be1f7..1a01d7f8e 100644 --- a/ostd/src/arch/x86/pci.rs +++ b/ostd/src/arch/x86/pci.rs @@ -1,30 +1,64 @@ // SPDX-License-Identifier: MPL-2.0 //! PCI bus access +use vstd::prelude::*; + use super::device::io_port::{ReadWriteAccess, WriteOnlyAccess}; use crate::{bus::pci::PciDeviceLocation, io::IoPort, prelude::*}; -static PCI_ADDRESS_PORT: IoPort = unsafe { IoPort::new(0x0CF8) }; -static PCI_DATA_PORT: IoPort = unsafe { IoPort::new(0x0CFC) }; +verus! { + +broadcast use super::device::io_port::group_io_port_models; +// Original Rust: static PCI_ADDRESS_PORT: IoPort = unsafe { IoPort::new(0x0CF8) }; + +exec static PCI_ADDRESS_PORT: IoPort + ensures + PCI_ADDRESS_PORT.well_formed(), +{ + unsafe { IoPort::new(0x0CF8) } +} + +// Original Rust: static PCI_DATA_PORT: IoPort = unsafe { IoPort::new(0x0CFC) }; +exec static PCI_DATA_PORT: IoPort + ensures + PCI_DATA_PORT.well_formed(), +{ + unsafe { IoPort::new(0x0CFC) } +} +} // verus! +#[verus_verify] const BIT32_ALIGN_MASK: u32 = 0xFFFC; +#[verus_verify] +#[verus_spec(result => ensures result is Ok)] pub(crate) fn write32(location: &PciDeviceLocation, offset: u32, value: u32) -> Result<()> { PCI_ADDRESS_PORT.write(encode_as_port(location) | (offset & BIT32_ALIGN_MASK)); PCI_DATA_PORT.write(value.to_le()); Ok(()) } +#[verus_verify] +#[verus_spec(result => ensures result is Ok)] pub(crate) fn read32(location: &PciDeviceLocation, offset: u32) -> Result { PCI_ADDRESS_PORT.write(encode_as_port(location) | (offset & BIT32_ALIGN_MASK)); Ok(PCI_DATA_PORT.read().to_le()) } +#[verus_verify] +#[verus_spec(returns true)] pub(crate) fn has_pci_bus() -> bool { true } +#[verus_verify] pub(crate) const MSIX_DEFAULT_MSG_ADDR: u32 = 0xFEE0_0000; +#[verus_verify] +#[verus_spec(returns + MSIX_DEFAULT_MSG_ADDR | 0b1_1000 + | ((remapping_index & 0x7FFF) << 5) + | ((remapping_index & 0x8000) >> 13), +)] pub(crate) fn construct_remappable_msix_address(remapping_index: u32) -> u32 { // Use remappable format. The bits[4:3] should be always set to 1 according to the manual. let mut address = MSIX_DEFAULT_MSG_ADDR | 0b1_1000; @@ -37,6 +71,13 @@ pub(crate) fn construct_remappable_msix_address(remapping_index: u32) -> u32 { } /// Encodes the bus, device, and function into a port address for use with the PCI I/O port. +#[verus_verify] +#[verus_spec(returns + (1u32 << 31) + | ((location.bus as u32) << 16) + | (((location.device as u32) & 0b11111) << 11) + | (((location.function as u32) & 0b111) << 8), +)] fn encode_as_port(location: &PciDeviceLocation) -> u32 { // 1 << 31: Configuration enable (1 << 31) diff --git a/ostd/src/boot/memory_region.rs b/ostd/src/boot/memory_region.rs index 8b36d1a02..9806d5972 100644 --- a/ostd/src/boot/memory_region.rs +++ b/ostd/src/boot/memory_region.rs @@ -261,14 +261,13 @@ impl Default for MemoryRegionArray { Self::new() } } -/* impl Deref for MemoryRegionArray { type Target = [MemoryRegion]; fn deref(&self) -> &Self::Target { &self.regions[..self.count] } -}*/ +} #[verus_verify] impl MemoryRegionArray { /// Constructs an empty set. diff --git a/ostd/src/boot/mod.rs b/ostd/src/boot/mod.rs index bdcffdb7f..8eb8cc4ce 100644 --- a/ostd/src/boot/mod.rs +++ b/ostd/src/boot/mod.rs @@ -12,10 +12,10 @@ use alloc::{ string::{String, ToString}, vec::Vec, }; - -use memory_region::{MemoryRegion, MemoryRegionArray}; +*/ +use memory_region::{/* MemoryRegion, */ MemoryRegionArray}; use spin::Once; - +/* /// The boot information provided by the bootloader. pub struct BootInfo { /// The name of the bootloader. @@ -38,6 +38,7 @@ pub fn boot_info() -> &'static BootInfo { } static INFO: Once = Once::new(); +*/ /// ACPI information from the bootloader. /// @@ -91,6 +92,7 @@ pub(crate) struct EarlyBootInfo { /// The boot-time information. pub(crate) static EARLY_INFO: Once = Once::new(); +/* /// Initializes the boot information. /// /// This function copies the boot-time accessible information to the heap to diff --git a/ostd/src/bus/mod.rs b/ostd/src/bus/mod.rs index 7b81924ce..b8898deb6 100644 --- a/ostd/src/bus/mod.rs +++ b/ostd/src/bus/mod.rs @@ -11,7 +11,7 @@ pub enum BusProbeError { ConfigurationSpaceError, } -/// Initializes the bus +/*/// Initializes the bus pub(crate) fn init() { pci::init(); -} +}*/ diff --git a/ostd/src/bus/pci/device_info.rs b/ostd/src/bus/pci/device_info.rs index 3d415c987..3bcc6c1a0 100644 --- a/ostd/src/bus/pci/device_info.rs +++ b/ostd/src/bus/pci/device_info.rs @@ -1,9 +1,12 @@ // SPDX-License-Identifier: MPL-2.0 //! PCI device Information +use vstd::prelude::*; + use core::iter; -use super::cfg_space::PciDeviceCommonCfgOffset; +/*use super::cfg_space::PciDeviceCommonCfgOffset;*/ +/* /// PCI device ID #[derive(Debug, Copy, Clone, PartialEq, Eq)] pub struct PciDeviceId { @@ -48,8 +51,10 @@ impl PciDeviceId { } } } +*/ /// PCI device Location +#[verus_verify] #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] pub struct PciDeviceLocation { /// Bus number diff --git a/ostd/src/bus/pci/mod.rs b/ostd/src/bus/pci/mod.rs index 0de48b517..261ab6202 100644 --- a/ostd/src/bus/pci/mod.rs +++ b/ostd/src/bus/pci/mod.rs @@ -48,14 +48,15 @@ //! PCI_BUS.lock().register_driver(driver_a); //! } //! ``` -pub mod bus; +/*pub mod bus; pub mod capability; pub mod cfg_space; -pub mod common_device; +pub mod common_device;*/ mod device_info; -pub use device_info::{PciDeviceId, PciDeviceLocation}; +pub use device_info::{/* PciDeviceId, */ PciDeviceLocation}; +/* use self::{bus::PciBus, common_device::PciCommonDevice}; use crate::{arch::pci::has_pci_bus, sync::Mutex}; @@ -74,4 +75,4 @@ pub(crate) fn init() { }; lock.register_common_device(device); } -} +}*/ diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index 0cd42a4e9..9e60f79c6 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -1,10 +1,16 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O Memory allocator. +use crate::specs::arch::PAGE_SIZE; +use vstd::{arithmetic::power2::is_pow2, prelude::*}; +use vstd_extra::{ + once::OnceImpl, resource::flags::OneShotSet, resource_invariant::TrivialResourceInvariant, +}; + use alloc::vec::Vec; use core::ops::Range; use log::{debug, info}; -use spin::Once; +/*use spin::Once;*/ use crate::{ io::io_mem::IoMem, @@ -13,23 +19,51 @@ use crate::{ }; /// I/O memory allocator that allocates memory I/O access to device drivers. +#[verus_verify] pub struct IoMemAllocator { allocators: Vec, } +#[verus_verify] impl IoMemAllocator { /// Acquires the I/O memory access for `range`. /// /// If the range is not available, then the return value will be `None`. + #[verus_spec(result => + requires + is_pow2(PAGE_SIZE as int), + range.start < range.end, + range.end <= usize::MAX - (PAGE_SIZE - 1), + io_mem_range_registered(range), + ensures + result matches Some(io_mem) ==> { + &&& io_mem.paddr() == range.start + &&& io_mem.length() == range.end - range.start + }, + )] pub fn acquire(&self, range: Range) -> Option { + /* Original Rust: find_allocator(&self.allocators, &range)? .alloc_specific(&range) .ok()?; + */ + let allocator = find_allocator(&self.allocators, &range)?; + proof! { + use_type_invariant(self); + lemma_found_window_contains(&self.allocators, &range, allocator); + } + proof_decl! { + let tracked initialized: OneShotSet; + } + let result = #[verus_spec(with => Tracked(initialized))] + allocator.alloc_specific(&range); + result.ok()?; - debug!("Acquiring MMIO range:{:x?}..{:x?}", range.start, range.end); + /* debug!("Acquiring MMIO range:{:x?}..{:x?}", range.start, range.end); */ // SAFETY: The created `IoMem` is guaranteed not to access physical memory or system device I/O. - unsafe { Some(IoMem::new(range, PageFlags::RW, CachePolicy::Uncacheable)) } + /* Original Rust: PageFlags::RW */ + unsafe { Some(IoMem::new(range, PageFlags::RW(), CachePolicy::Uncacheable)) } } /// Recycles an MMIO range. @@ -38,10 +72,11 @@ impl IoMemAllocator { /// /// The caller must have ownership of the MMIO region through the `IoMemAllocator::get` interface. #[expect(dead_code)] + #[verifier::external_body] pub(in crate::io) unsafe fn recycle(&self, range: Range) { let allocator = find_allocator(&self.allocators, &range).unwrap(); - debug!("Recycling MMIO range:{:x}..{:x}", range.start, range.end); + /* debug!("Recycling MMIO range:{:x}..{:x}", range.start, range.end); */ allocator.free(range); } @@ -51,6 +86,11 @@ impl IoMemAllocator { /// # Safety /// /// User must ensure the range doesn't belong to physical memory or system device I/O. + #[verus_spec(ret => + requires + windows_ordered(allocators@), + windows_match_registered(allocators@), + )] unsafe fn new(allocators: Vec) -> Self { Self { allocators } } @@ -60,24 +100,65 @@ impl IoMemAllocator { /// /// The builder must contains the memory I/O regions that don't belong to the physical memory. Also, OSTD /// must exclude the memory I/O regions of the system device before building the `IoMemAllocator`. +#[verus_verify] pub(crate) struct IoMemAllocatorBuilder { allocators: Vec, } +#[verus_verify] impl IoMemAllocatorBuilder { /// Initializes memory I/O region for devices. /// /// # Safety /// /// User must ensure the range doesn't belong to physical memory. + #[verus_spec(ret => + requires + usize_ranges_ordered(ranges@), + usize_ranges_match_registered(ranges@), + ensures + ret.type_inv(), + )] pub(crate) unsafe fn new(ranges: Vec>) -> Self { - info!( + /* info!( "Creating new I/O memory allocator builder, ranges: {:#x?}", ranges - ); - let mut allocators = Vec::with_capacity(ranges.len()); + ); */ + let mut allocators: Vec = Vec::with_capacity(ranges.len()); + #[verus_spec(it => + invariant + allocators@.len() == it.index(), + forall|j: int| #![trigger it.seq()[j]] 0 <= j < it.index() ==> { + &&& allocators@[j]@.start == it.seq()[j].start + &&& allocators@[j]@.end == it.seq()[j].end + }, + usize_ranges_ordered(it.seq()), + usize_ranges_match_registered(it.seq()), + forall|j: int| #![trigger registered_io_mem_windows()[j]] 0 <= j < it.index() ==> + allocators@[j]@ == registered_io_mem_windows()[j], + windows_ordered(allocators@), + )] for range in ranges { + proof! { + assert(range == it.seq()[it.index()]); + } allocators.push(RangeAllocator::new(range)); + proof! { + assert(allocators@[allocators@.len() - 1]@.start == range.start); + assert(range.start == registered_io_mem_windows()[it.index()].start); + assert(range.end == registered_io_mem_windows()[it.index()].end); + assert forall|i: int| #![trigger allocators@[i]] + 0 <= i < allocators@.len() - 1 + implies allocators@[i]@.end <= range.start by { + assert(allocators@[i]@.end == it.seq()[i].end); + assert(it.seq()[i].end <= it.seq()[i as int + 1].start); + } + assert(windows_ordered(allocators@)); + } + } + proof! { + assert(allocators@.len() == registered_io_mem_windows().len()); + assert(windows_match_registered(allocators@)); } Self { allocators } } @@ -85,7 +166,15 @@ impl IoMemAllocatorBuilder { /// Removes access to a specific memory I/O range. /// /// All drivers in OSTD must use this method to prevent peripheral drivers from accessing illegal memory I/O range. + #[verus_spec( + requires + range.start < range.end, + vstd_extra::panic::may_panic(), + io_mem_range_registered(range), + )] pub(crate) fn remove(&self, range: Range) { + /* Formatting machinery used by the original panic is not modeled by Verus. + Original Rust: let Some(allocator) = find_allocator(&self.allocators, &range) else { panic!( "Allocator for the system device's MMIO was not found. Range: {:x?}", @@ -99,34 +188,195 @@ impl IoMemAllocatorBuilder { range, err ); } + */ + let allocator = find_allocator(&self.allocators, &range); + vstd_extra::assert!(allocator.is_some()); + let allocator = allocator.unwrap(); + proof! { + use_type_invariant(self); + lemma_found_window_contains(&self.allocators, &range, allocator); + } + proof_decl! { + let tracked initialized: OneShotSet; + } + let result = #[verus_spec(with => Tracked(initialized))] + allocator.alloc_specific(&range); + vstd_extra::assert!(result.is_ok()); } } /// The I/O Memory allocator of the system. -pub static IO_MEM_ALLOCATOR: Once = Once::new(); +// Original Rust: pub static IO_MEM_ALLOCATOR: Once = Once::new(); +verus! { + +broadcast use vstd::std_specs::vec::group_vec_axioms; + +/// The registered MMIO windows are pairwise ordered: every window ends at or before the start +/// of the next one, so no window can partially cover a range that is contained in another one. +pub open spec fn windows_ordered(allocators: Seq) -> bool { + forall|i: int, j: int| + #![trigger allocators[i], allocators[j]] + 0 <= i < j < allocators.len() ==> allocators[i]@.end <= allocators[j]@.start +} + +/// The format of the windows handed to [`IoMemAllocatorBuilder::new`]. +pub open spec fn usize_ranges_ordered(ranges: Seq>) -> bool { + forall|i: int, j: int| + #![trigger ranges[i], ranges[j]] + 0 <= i < j < ranges.len() ==> ranges[i].end <= ranges[j].start +} + +/// The abstract MMIO windows registered by platform boot code. +pub uninterp spec fn registered_io_mem_windows() -> Seq>; + +/// The concrete range allocators represent the abstract boot-time windows exactly. +pub open spec fn windows_match_registered(allocators: Seq) -> bool { + &&& allocators.len() == registered_io_mem_windows().len() + &&& forall|i: int| + #![trigger registered_io_mem_windows()[i]] + 0 <= i < allocators.len() ==> allocators[i]@ == registered_io_mem_windows()[i] +} + +/// The ranges passed across the unsafe builder boundary represent the abstract windows. +pub open spec fn usize_ranges_match_registered(ranges: Seq>) -> bool { + &&& ranges.len() == registered_io_mem_windows().len() + &&& forall|i: int| + #![trigger ranges[i]] + 0 <= i < ranges.len() ==> { + &&& ranges[i].start == registered_io_mem_windows()[i].start + &&& ranges[i].end == registered_io_mem_windows()[i].end + } +} + +impl IoMemAllocatorBuilder { + /// The builder always holds the ordered windows handed to [`IoMemAllocatorBuilder::new`]. + #[verifier::type_invariant] + pub closed spec fn type_inv(self) -> bool { + windows_ordered(self.allocators@) && windows_match_registered(self.allocators@) + } +} + +impl IoMemAllocator { + /// The allocator inherits the ordered windows of the builder it was built from. + #[verifier::type_invariant] + pub closed spec fn type_inv(self) -> bool { + windows_ordered(self.allocators@) && windows_match_registered(self.allocators@) + } +} + +/// The trusted boot fact [`io_mem_range_registered`], made concrete: the index of the +/// registered window containing `range`. +pub proof fn lemma_registered_window(windows: &Vec, range: Range) -> (idx: + int) + requires + windows_ordered(windows@), + windows_match_registered(windows@), + io_mem_range_registered(range), + ensures + 0 <= idx < windows@.len(), + windows@[idx]@.start <= range.start && range.end <= windows@[idx]@.end, +{ + let idx = choose|m: int| + #![trigger registered_io_mem_windows()[m]] + 0 <= m < registered_io_mem_windows().len() && registered_io_mem_windows()[m].start + <= range.start && range.end <= registered_io_mem_windows()[m].end; + assert(windows@[idx]@ == registered_io_mem_windows()[idx]); + idx +} + +/// The window overlapping `range` found by [`find_allocator`] is exactly the registered +/// window containing it: ordered windows cannot partially cover a range contained in +/// another window. +pub proof fn lemma_found_window_contains( + windows: &Vec, + range: &Range, + found: &RangeAllocator, +) + requires + windows_ordered(windows@), + windows_match_registered(windows@), + io_mem_range_registered(*range), + found@.start < range.end && found@.end > range.start, + exists|k: int| #![trigger windows@[k]] 0 <= k < windows@.len() && windows@[k]@ == found@, + ensures + found@.start <= range.start && range.end <= found@.end, +{ + let container_idx = lemma_registered_window(windows, *range); + let found_idx = choose|k: int| + #![trigger windows@[k]] + 0 <= k < windows@.len() && windows@[k]@ == found@; + if found_idx < container_idx { + assert(windows@[found_idx]@.end <= windows@[container_idx]@.start); + assert(windows@[container_idx]@.start <= range.start); + assert(false); + } else if found_idx == container_idx { + assert(windows@[found_idx]@.start <= range.start && range.end <= windows@[found_idx]@.end); + } else { + assert(range.end <= windows@[container_idx]@.end); + assert(windows@[container_idx]@.end <= windows@[found_idx]@.start); + assert(false); + } +} + +/// A range is registered when one abstract boot-time MMIO window contains it. +pub open spec fn io_mem_range_registered(range: Range) -> bool { + exists|m: int| + #![trigger registered_io_mem_windows()[m]] + 0 <= m < registered_io_mem_windows().len() && registered_io_mem_windows()[m].start + <= range.start && range.end <= registered_io_mem_windows()[m].end +} +pub exec static IO_MEM_ALLOCATOR: OnceImpl + ensures + IO_MEM_ALLOCATOR.wf(), +{ + OnceImpl::new(Ghost(TrivialResourceInvariant)) +} + +} // verus! /// Initializes the static `IO_MEM_ALLOCATOR` based on builder. /// /// # Safety /// /// User must ensure all the memory I/O regions that belong to the system device have been removed by calling the /// `remove` function. +#[verus_verify] pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { + proof! { + use_type_invariant(&io_mem_builder); + } // SAFETY: The safety is upheld by the caller. - IO_MEM_ALLOCATOR.call_once(|| unsafe { IoMemAllocator::new(io_mem_builder.allocators) }); + // Original Rust: IO_MEM_ALLOCATOR.call_once(|| unsafe { IoMemAllocator::new(io_mem_builder.allocators) }); + IO_MEM_ALLOCATOR.init(unsafe { IoMemAllocator::new(io_mem_builder.allocators) }); } +#[verus_verify] +#[verus_spec(ret => + ensures + ret matches Some(res) ==> { + &&& res@.start < range.end + &&& res@.end > range.start + &&& exists|k: int| #![trigger allocators@[k]] + 0 <= k < allocators@.len() && allocators@[k]@ == res@ + } +)] fn find_allocator<'a>( allocators: &'a [RangeAllocator], range: &Range, ) -> Option<&'a RangeAllocator> { for allocator in allocators.iter() { let allocator_range = allocator.fullrange(); + /* Verus does not yet support `continue` in `for` loops. + Original Rust: if allocator_range.start >= range.end || allocator_range.end <= range.start { continue; } return Some(allocator); + */ + if allocator_range.start < range.end && allocator_range.end > range.start { + return Some(allocator); + } } None } diff --git a/ostd/src/io/io_mem/mod.rs b/ostd/src/io/io_mem/mod.rs index 3afa2d077..b546c7483 100644 --- a/ostd/src/io/io_mem/mod.rs +++ b/ostd/src/io/io_mem/mod.rs @@ -1,5 +1,13 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O memory and its allocator that allocates memory I/O (MMIO) to device drivers. +use crate::specs::{ + arch::PAGE_SIZE, + mm::{io::VmIoOwner, virt_mem::VirtPtr}, + task::AnyAtomicGuard, +}; +use vstd::{arithmetic::power2::is_pow2, prelude::*}; +use vstd_extra::panic::UnwrapOrPanic; + mod allocator; use core::ops::{Deref, Range}; @@ -11,8 +19,8 @@ pub(super) use self::allocator::init; use crate::{ Error, mm::{ - FallibleVmRead, FallibleVmWrite, HasPaddr, Infallible, PAGE_SIZE, Paddr, PodOnce, VmIo, - VmIoOnce, VmReader, VmWriter, + FallibleVmRead, FallibleVmWrite, HasPaddr, Infallible, /*PAGE_SIZE,*/ Paddr, PodOnce, + VmIo, VmIoOnce, VmReader, VmWriter, kspace::kvirt_area::KVirtArea, page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags}, }, @@ -21,6 +29,7 @@ use crate::{ /// I/O memory. #[derive(Debug, Clone)] +#[verus_verify] pub struct IoMem { kvirt_area: Arc, // The actually used range for MMIO is `kvirt_area.start + offset..kvirt_area.start + offset + limit` @@ -29,28 +38,58 @@ pub struct IoMem { pa: Paddr, } +verus! { + +#[verus_verify] +impl IoMem { + /// Logical offset into the page-aligned mapping. + pub closed spec fn offset_spec(&self) -> usize { + self.offset + } +} + +} // verus! +#[verus_verify] impl HasPaddr for IoMem { + #[verus_spec(returns IoMem::paddr(self))] fn paddr(&self) -> Paddr { self.pa } } +#[verus_verify] impl IoMem { /// Acquires an `IoMem` instance for the given range. + #[verus_spec(result => + requires + is_pow2(PAGE_SIZE as int), + range.start < range.end, + range.end <= usize::MAX - (PAGE_SIZE - 1), + allocator::io_mem_range_registered(range), + vstd_extra::panic::may_panic(), + ensures + result matches Ok(io_mem) ==> { + &&& io_mem.paddr() == range.start + &&& io_mem.length() == range.end - range.start + }, + )] pub fn acquire(range: Range) -> Result { allocator::IO_MEM_ALLOCATOR .get() - .unwrap() + /* .unwrap() */ + .unwrap_or_panic() .acquire(range) .ok_or(Error::AccessDenied) } /// Returns the physical address of the I/O memory. + #[verus_verify(dual_spec)] pub fn paddr(&self) -> Paddr { self.pa } /// Returns the length of the I/O memory region. + #[verus_verify(dual_spec)] pub fn length(&self) -> usize { self.limit } @@ -60,9 +99,23 @@ impl IoMem { /// # Panics /// /// This method will panic if the range is empty or out of bounds. + #[verus_verify] + #[verus_spec(result => + requires + range.start < range.end <= self.length(), + self.offset_spec() + range.start <= usize::MAX, + self.paddr() + range.start <= usize::MAX, + ensures + result.offset_spec() == self.offset_spec() + range.start, + result.length() == range.end - range.start, + result.paddr() == self.paddr() + range.start, + )] pub fn slice(&self, range: Range) -> Self { // This ensures `range.start < range.end` and `range.end <= limit`. + /* assert!(!range.is_empty() && range.end <= self.limit); + */ + vstd_extra::assert!(range.start < range.end && range.end <= self.limit); // We've checked the range is in bounds, so we can construct the new `IoMem` safely. Self { @@ -80,6 +133,17 @@ impl IoMem { /// - The given physical address range must be in the I/O memory region. /// - Reading from or writing to I/O memory regions may have side effects. Those side effects /// must not cause soundness problems (e.g., they must not corrupt the kernel memory). + #[verifier::external_body] + #[verus_spec(result => + requires + is_pow2(PAGE_SIZE as int), + range.start <= range.end, + range.end <= usize::MAX - (PAGE_SIZE - 1), + ensures + result.paddr() == range.start, + result.length() + == range.end - range.start, + )] pub(crate) unsafe fn new(range: Range, flags: PageFlags, cache: CachePolicy) -> Self { let first_page_start = range.start.align_down(PAGE_SIZE); let last_page_end = range.end.align_up(PAGE_SIZE); @@ -123,7 +187,11 @@ impl IoMem { // SAFETY: The caller of `IoMem::new()` ensures that the given // physical address range is I/O memory, so it is safe to map. - let kva = unsafe { KVirtArea::map_untracked_frames(area_size, 0, frames_range, prop) }; + // Original Rust: + // let kva = unsafe { KVirtArea::map_untracked_frames(area_size, 0, frames_range, prop) }; + let kva = unsafe { + KVirtArea::map_untracked_frames::(area_size, 0, frames_range, prop) + }; Self { kvirt_area: Arc::new(kva), @@ -147,7 +215,9 @@ impl IoMem { // safety of reading from the mapped physical address, and the mapping is valid. unsafe { VmReader::from_kernel_space( - (self.kvirt_area.deref().start() + self.offset) as *mut u8, + /* Original Rust: + (self.kvirt_area.deref().start() + self.offset) as *mut u8, */ + VirtPtr::from_vaddr(self.kvirt_area.deref().start() + self.offset, self.limit), self.limit, ) } @@ -158,47 +228,95 @@ impl IoMem { // safety of writing to the mapped physical address, and the mapping is valid. unsafe { VmWriter::from_kernel_space( - (self.kvirt_area.deref().start() + self.offset) as *mut u8, + /* Original Rust: + (self.kvirt_area.deref().start() + self.offset) as *mut u8, */ + VirtPtr::from_vaddr(self.kvirt_area.deref().start() + self.offset, self.limit), self.limit, ) } } } -impl VmIo for IoMem { - fn read(&self, offset: usize, writer: &mut VmWriter) -> Result<()> { +verus! { + +/* Original Rust: impl VmIo for IoMem { */ +impl VmIo<()> for IoMem { + closed spec fn obeys_vmio_spec() -> bool { + false + } + + closed spec fn obeys_vmio_read_spec() -> bool { + false + } + + closed spec fn obeys_vmio_write_spec() -> bool { + false + } + + open spec fn read_spec( + self, + offset: usize, + old_writer: VmWriter<'_>, + new_writer: VmWriter<'_>, + old_writer_own: VmIoOwner, + new_writer_own: VmIoOwner, + old_owner: (), + new_owner: (), + r: Result<()>, + ) -> bool { + false + } + + open spec fn write_spec( + self, + offset: usize, + old_reader: VmReader<'_>, + new_reader: VmReader<'_>, + old_reader_own: VmIoOwner, + new_reader_own: VmIoOwner, + old_owner: (), + new_owner: (), + r: Result<()>, + ) -> bool { + false + } + + /// Device reads are a trusted hardware boundary; the range checks and cursor updates remain + /// identical to the original implementation. + #[verifier::external_body] + /* Original Rust: fn read(&self, offset: usize, writer: &mut VmWriter) -> Result<()> { */ + fn read( + &self, + offset: usize, + writer: &mut VmWriter, + Tracked(_writer_own): Tracked<&mut VmIoOwner>, + Tracked(_owner): Tracked<&mut ()>, + ) -> Result<()> { let offset = offset + self.offset; - if self - .limit - .checked_sub(offset) - .is_none_or(|remain| remain < writer.avail()) - { + if self.limit.checked_sub(offset).is_none_or(|remain| remain < writer.avail()) { return Err(Error::InvalidArgs); } - - self.reader() - .skip(offset) - .read_fallible(writer) - .map_err(|(e, _)| e)?; + self.reader().skip(offset).read_fallible(writer).map_err(|(e, _)| e)?; debug_assert!(!writer.has_avail()); Ok(()) } - fn write(&self, offset: usize, reader: &mut VmReader) -> Result<()> { + /// Device writes are a trusted hardware boundary for the same reason as [`Self::read`]. + #[verifier::external_body] + /* Original Rust: fn write(&self, offset: usize, reader: &mut VmReader) -> Result<()> { */ + fn write( + &self, + offset: usize, + reader: &mut VmReader, + Tracked(_reader_own): Tracked<&mut VmIoOwner>, + Tracked(_owner): Tracked<&mut ()>, + ) -> Result<()> { let offset = offset + self.offset; - if self - .limit - .checked_sub(offset) - .is_none_or(|remain| remain < reader.remain()) - { + if self.limit.checked_sub(offset).is_none_or(|remain| remain < reader.remain()) { return Err(Error::InvalidArgs); } - - self.writer() - .skip(offset) - .write_fallible(reader) - .map_err(|(e, _)| e)?; + self.writer().skip(offset).write_fallible(reader).map_err(|(e, _)| e)?; debug_assert!(!reader.has_remain()); Ok(()) @@ -206,15 +324,34 @@ impl VmIo for IoMem { } impl VmIoOnce for IoMem { + closed spec fn obeys_vmio_once_read_requires() -> bool { + false + } + + closed spec fn obeys_vmio_once_write_requires() -> bool { + false + } + + closed spec fn obeys_vmio_once_read_ensures() -> bool { + false + } + + closed spec fn obeys_vmio_once_write_ensures() -> bool { + false + } + + #[verifier::external_body] fn read_once(&self, offset: usize) -> Result { self.reader().skip(offset).read_once() } + #[verifier::external_body] fn write_once(&self, offset: usize, new_val: &T) -> Result<()> { self.writer().skip(offset).write_once(new_val) } } +} // verus! impl Drop for IoMem { fn drop(&mut self) { // TODO: Multiple `IoMem` instances should not overlap, we should refactor the driver code and diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index 0e5b85e9a..f33c54ac2 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -1,41 +1,441 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port allocator. +use crate::arch::device::io_port::valid_io_port_access; +use vstd::{ + prelude::*, + resource::set::{GhostSetAuth, GhostSubset}, + tokens::InstanceId, +}; +use vstd_extra::{ownership::Inv, resource_invariant::ResourceInvariant}; + use core::ops::Range; use id_alloc::IdAlloc; use log::debug; use spin::Once; -use super::IoPort; +use super::{IoPort, lemma_port_id_set_contains, lemma_port_id_set_insert, port_id_set}; use crate::{ io::RawIoPortRange, sync::{LocalIrqDisabled, SpinLock}, }; +verus! { + +/// Identity assigned to the single global PIO allocator during trusted boot initialization. +pub uninterp spec fn io_port_allocator_instance_id() -> InstanceId; + +/// Allocated ids of a bitmap prefix `[0, end)`: `i` is in iff `s[i]`. +pub(crate) closed spec fn id_alloc_bits(s: Seq, end: int) -> Set + decreases end, +{ + if end <= 0 { + Set::empty() + } else { + let rest = id_alloc_bits(s, end - 1); + if s[end - 1] { + rest.insert((end - 1) as usize) + } else { + rest + } + } +} + +/// Set of ids currently allocated by `allocator`. +pub(crate) open spec fn id_alloc_view(allocator: &IdAlloc) -> Set { + id_alloc_bits(allocator@, allocator@.len() as int) +} + +/// Number of ids `allocator` can hold. +pub(crate) open spec fn id_alloc_capacity(allocator: &IdAlloc) -> usize { + allocator@.len() as usize +} + +/// Characterizes `id_alloc_bits`: `id_alloc_bits(s, end).contains(j)` holds exactly when +/// `0 <= j < end` and `s[j]` is `true`. +pub(crate) proof fn lemma_id_alloc_bits_char(s: Seq, end: int, j: usize) + requires + 0 <= end, + end <= usize::MAX as int, + s.len() >= end, + 0 <= (j as int), + ensures + id_alloc_bits(s, end).contains(j) == ((j as int) < end && s[j as int]), + decreases end, +{ + reveal(id_alloc_bits); + if end <= 0 { + assert(id_alloc_bits(s, end) =~= Set::empty()); + } else { + lemma_id_alloc_bits_char(s, end - 1, j); + if (j as int) == end - 1 { + assert(id_alloc_bits(s, end - 1).contains(j) == (((j as int) < end - 1) + && s[j as int])); + assert(id_alloc_bits(s, end).contains(j) == s[end - 1]); + assert(s[j as int] == s[end - 1]); + } else { + // j != end-1: the bit folded in at (end-1) is distinct from j. + assert(id_alloc_bits(s, end - 1).contains(j) == (((j as int) < end - 1) + && s[j as int])); + assert(((end - 1) as usize) as int == end - 1); + assert(j != (end - 1) as usize); + if s[end - 1] { + assert(id_alloc_bits(s, end - 1).insert((end - 1) as usize).contains(j) + == id_alloc_bits(s, end - 1).contains(j)); + } + assert(id_alloc_bits(s, end).contains(j) == id_alloc_bits(s, end - 1).contains(j)); + assert(((j as int) < end - 1 && s[j as int]) == ((j as int) < end && s[j as int])); + } + } +} + +/// For an in-bounds id, `id_alloc_view` membership coincides with the allocated bitmap bit. +pub(crate) proof fn lemma_id_alloc_view_contains(allocator: &IdAlloc, id: usize) + requires + allocator.inv(), + (id as int) < allocator@.len(), + allocator@.len() <= usize::MAX as int, + ensures + id_alloc_view(allocator).contains(id) == allocator@[id as int], +{ + lemma_id_alloc_bits_char(allocator@, allocator@.len() as int, id); +} + +pub(crate) open spec fn io_port_inner_inv_values( + allocated_instance_id: InstanceId, + allocated: Set, + allocator: &IdAlloc, +) -> bool { + &&& allocated_instance_id == io_port_allocator_instance_id() + &&& allocator.inv() + &&& allocator@.len() == crate::arch::io::MAX_IO_PORT as int + &&& allocated.subset_of(id_alloc_view(allocator)) + &&& id_alloc_capacity(allocator) == crate::arch::io::MAX_IO_PORT as usize +} + +/// Authority over the set of PIO ids currently allocated by the global allocator. +/// +/// The `Loc` of `auth` identifies the protocol instance and `auth@` is the set of allocated +/// ids. [`IoPortClaim`] fragments minted by [`IoPortAllocation::allocate`] transfer the +/// ownership of an acquired PIO range to the caller. +pub(super) tracked struct IoPortAllocation { + auth: GhostSetAuth, +} + +/// Fragment claiming ownership of a PIO id range handed out by [`IoPortAllocator::acquire`]. +/// +/// A claim asserts that its ids are allocated by the [`IoPortAllocation`] with the same +/// instance identity, and is consumed when the ids are released by +/// [`IoPortAllocator::recycle`]. +pub(super) tracked struct IoPortClaim { + subset: GhostSubset, +} + +impl IoPortAllocation { + /// Instance identity of the protocol. + pub closed spec fn instance_id(self) -> InstanceId { + self.auth.id() + } + + /// Ids currently allocated. + pub closed spec fn value(self) -> Set { + self.auth@ + } + + /// Creates a fresh protocol instance with an empty allocated set. + pub proof fn initialize() -> (tracked result: Self) { + let tracked (auth, _empty_claims) = GhostSetAuth::new(Set::empty()); + Self { auth } + } + + /// Allocates `ids`, requiring them to be currently free, and mints the matching claim + /// fragment. + pub proof fn allocate(tracked &mut self, ids: Set) -> (tracked claim: IoPortClaim) + requires + old(self).value().disjoint(ids), + ensures + final(self).instance_id() == old(self).instance_id(), + final(self).value() == old(self).value().union(ids), + claim.instance_id() == final(self).instance_id(), + claim.set() == ids, + { + let tracked subset = self.auth.insert_set(ids); + IoPortClaim { subset } + } + + /// Consumes `claim`, removing its ids from the allocated set. + pub proof fn release(tracked &mut self, tracked claim: IoPortClaim) + requires + claim.instance_id() == old(self).instance_id(), + ensures + final(self).instance_id() == old(self).instance_id(), + final(self).value() == old(self).value().difference(claim.set()), + { + self.auth.delete(claim.subset); + } + + /// Certifies `claim.set() <= self.value()` (the claim's ids are currently allocated). + pub proof fn claim_includes(tracked &self, tracked claim: &IoPortClaim) + requires + claim.instance_id() == self.instance_id(), + ensures + claim.set() <= self.value(), + { + claim.subset.agree(&self.auth); + } +} + +impl IoPortClaim { + /// Instance identity of the protocol that issued this claim. + pub closed spec fn instance_id(self) -> InstanceId { + self.subset.id() + } + + /// Ids claimed by this fragment. + pub closed spec fn set(self) -> Set { + self.subset@ + } +} + +ghost struct IoPortAllocInvariant; + +impl ResourceInvariant for IoPortAllocInvariant { + type Constant = (); + + type Resource = IoPortAllocation; + + closed spec fn inv(_constant: (), alloc: IdAlloc, r: IoPortAllocation) -> bool { + io_port_inner_inv_values(r.instance_id(), r.value(), &alloc) + } +} + +} // verus! /// I/O port allocator that allocates port I/O access to device drivers. -pub struct IoPortAllocator { +#[verus_verify] +pub(super) struct IoPortAllocator { /// Each ID indicates whether a Port I/O (1B) is allocated. /// /// Instead of using `RangeAllocator` like `IoMemAllocator` does, it is more reasonable to use `IdAlloc`, /// as PIO space includes only a small region; for example, x86 module in OSTD allows just 65536 I/O ports. - allocator: SpinLock, + allocator: SpinLock, } +#[verus_verify] impl IoPortAllocator { - /// Acquires the `IoPort`. Return None if any region in `port` cannot be allocated. - pub fn acquire(&self, port: u16) -> Option> { + /// Acquires an `IoPort`. Returns `None` if the PIO range is unavailable. + /// + /// `is_overlapping` indicates whether another `IoPort` can have a PIO range that overlaps with + /// this one. If it is true, only the first port in the PIO range will be marked as occupied; + /// otherwise, all ports in the PIO range will be marked as occupied. + #[verus_spec(result => + with + Tracked(claim_out): Tracked<&mut Tracked>>, + requires + size_of::() <= u16::MAX, + is_overlapping ==> port as usize + size_of::() <= u16::MAX, + valid_io_port_access::(port), + io_port_allocator_initialized(), + (*old(claim_out))@ is None, + ensures + result is Some <==> (*final(claim_out))@ is Some, + result matches Some(io_port) ==> { + &&& io_port@ == port + &&& io_port.is_overlapping() == is_overlapping + &&& io_port.well_formed() + &&& io_port.claim_matches_set((*final(claim_out))@->Some_0.set()) + &&& (*final(claim_out))@->Some_0.instance_id() == io_port_allocator_instance_id() + }, + )] + pub(super) fn acquire(&self, port: u16, is_overlapping: bool) -> Option> { + let range = if !is_overlapping { + port..port.checked_add(size_of::().try_into().ok()?)? + } else { + port..port.checked_add(1)? + }; + /* debug!("Try to acquire PIO range: {:#x?}", range); */ let mut allocator = self.allocator.lock(); - let mut range = port..(port + size_of::() as u16); - if range.any(|i| allocator.is_allocated(i as usize)) { + proof_decl! { + let ghost instance_id = allocator.resource().instance_id(); + let ghost preserved = allocator.resource().value(); + } + proof! { + assert(io_port_inner_inv_values(instance_id, preserved, &allocator.value())); + } + let allocator_inner = &mut *allocator; + // `Iterator::any` with a capturing closure is not supported by Verus. + // Original Rust: + // if range.any(|i| allocator.is_allocated(i as usize)) { return None; } + let mut already_allocated = false; + #[verus_spec(scan_iter => + invariant + allocator_inner.inv(), + allocator_inner@.len() + == crate::arch::io::MAX_IO_PORT as int, + !already_allocated ==> forall|id: usize| + range.start as usize <= id < + (range.start as int + scan_iter.index()) as usize ==> + !id_alloc_view(&allocator_inner).contains(id), + )] + for i in range.clone() { + proof! { + assert((i as usize) < allocator_inner@.len()) by { + assert((i as usize) < range.end as usize); + assert((range.end as usize) <= u16::MAX as usize); + assert((u16::MAX as usize) <= crate::arch::io::MAX_IO_PORT as usize); + assert(allocator_inner@.len() + == crate::arch::io::MAX_IO_PORT as int); + } + } + if allocator_inner.is_allocated(i as usize) { + already_allocated = true; + } + proof! { + lemma_id_alloc_view_contains(&allocator_inner, i as usize); + } + } + proof_decl! { + let tracked range_claim: IoPortClaim; + } + if already_allocated { + allocator.drop(); + proof! { + *claim_out = Tracked(None); + } return None; } + proof_decl! { + let ghost ids = port_id_set(range.start as usize, range.end as usize); + let ghost allocation_start_view = id_alloc_view(&allocator_inner); + } + proof! { + assert(ids.disjoint(id_alloc_view(&allocator_inner))) by { + assert forall|id: usize| #[trigger] ids.contains(id) implies + !id_alloc_view(&allocator_inner).contains(id) by { + lemma_port_id_set_contains( + range.start as usize, + range.end as usize, + id, + ); + } + } + assert forall|id: usize| ids.contains(id) implies + id < id_alloc_capacity(&allocator_inner) by { + lemma_port_id_set_contains( + range.start as usize, + range.end as usize, + id, + ); + } + assert forall|id: usize| + range.start as usize <= id < range.end as usize implies + !id_alloc_view(&allocator_inner).contains(id) by { + lemma_port_id_set_contains( + range.start as usize, + range.end as usize, + id, + ); + } + } + #[verus_spec(allocation_iter => + invariant + allocator_inner.inv(), + allocator_inner@.len() + == crate::arch::io::MAX_IO_PORT as int, + range.end as usize <= id_alloc_capacity(&allocator_inner), + instance_id == io_port_allocator_instance_id(), + preserved.subset_of(allocation_start_view), + preserved.subset_of(id_alloc_view(&allocator_inner)), + id_alloc_capacity(&allocator_inner) == + crate::arch::io::MAX_IO_PORT as usize, + id_alloc_view(&allocator_inner) == + allocation_start_view.union( + port_id_set( + range.start as usize, + (range.start as int + allocation_iter.index()) as usize, + ), + ), + forall|id: usize| + (range.start as int + allocation_iter.index()) as usize <= id < + range.end as usize ==> + !id_alloc_view(&allocator_inner).contains(id), + )] for i in range.clone() { - allocator.alloc_specific(i as usize); + proof_decl! { + let ghost old_view = id_alloc_view(&allocator_inner); + let ghost old_seq = allocator_inner@; + let ghost old_len = (allocator_inner@.len()) as int; + } + proof! { + assert((i as usize) == + (range.start as int + allocation_iter.index()) as usize); + assert((i as usize) < id_alloc_capacity(&allocator_inner)); + assert(allocator_inner.inv()); + assert(!id_alloc_view(&allocator_inner).contains(i as usize)); + assert(preserved.subset_of(old_view.insert(i as usize))) by { + assert forall|id: usize| + preserved.contains(id) implies + old_view.insert(i as usize).contains(id) by { + } + } + } + /* Original Rust: allocator.alloc_specific(i as usize); */ + let _res = allocator_inner.alloc_specific(i as usize); + proof! { + assert((allocator_inner@.len()) as int == old_len); + assert(id_alloc_view(&allocator_inner) == old_view.insert(i as usize)) by { + lemma_port_id_set_insert(range.start as usize, i as usize); + assert forall|j: usize| + #![trigger id_alloc_view(&allocator_inner).contains(j)] + id_alloc_view(&allocator_inner).contains(j) + == old_view.insert(i as usize).contains(j) by { + lemma_id_alloc_bits_char(old_seq, old_len, j); + lemma_id_alloc_bits_char(allocator_inner@, old_len, j); + if _res is Some { + assert(allocator_inner@ == old_seq.update(i as int, true)); + assert(allocator_inner@[j as int] == (if (j as int) == (i as int) { + true + } else { + old_seq[j as int] + })); + } else { + assert(old_seq[i as int]); + assert(allocator_inner@ == old_seq); + } + } + } + assert(preserved.subset_of(id_alloc_view(&allocator_inner))); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator_inner)); + } + } + proof! { + assert(ids.disjoint(preserved)) by { + assert forall|id: usize| #[trigger] ids.contains(id) implies + !preserved.contains(id) by { + } + } + assert(preserved.disjoint(ids)); + range_claim = allocator.tracked_borrow_mut_resource().allocate(ids); } - // SAFETY: The created IoPort is guaranteed not to access system device I/O - unsafe { Some(IoPort::new(port)) } + // SAFETY: The created `IoPort` is guaranteed not to access system device I/O. + /* Original Rust: unsafe { Some(IoPort::new_overlapping(port, is_overlapping)) } */ + let result = unsafe { Some(IoPort::new_overlapping(port, is_overlapping)) }; + proof! { + assert(id_alloc_view(&allocator.value()) == allocation_start_view.union(ids)); + assert(preserved.subset_of(allocation_start_view)); + assert(allocator.resource().value() == preserved.union(ids)); + assert(io_port_inner_inv_values( + allocator.resource().instance_id(), + allocator.resource().value(), + &allocator.value(), + )); + } + allocator.drop(); + proof! { + *claim_out = Tracked(Some(range_claim)); + } + result } /// Recycles an PIO range. @@ -43,15 +443,153 @@ impl IoPortAllocator { /// # Safety /// /// The caller must have ownership of the PIO region through the `IoPortAllocator::acquire` interface. - pub(in crate::io) unsafe fn recycle(&self, range: Range) { - debug!("Recycling MMIO range: {:#x?}", range); + #[verus_spec( + with + Tracked(claim): Tracked, + requires + claim.instance_id() == io_port_allocator_instance_id(), + claim.set() =~= port_id_set(range.start as usize, range.end as usize), + range.start <= range.end, + io_port_allocator_initialized(), + )] + pub(super) unsafe fn recycle(&self, range: Range) { + /* debug!("Recycling PIO range: {:#x?}", range); */ + /* Original Rust: + self.allocator + .lock() + .free_consecutive(range.start as usize..range.end as usize); + */ + let mut allocator = self.allocator.lock(); + proof_decl! { + let ghost instance_id: InstanceId; + let ghost preserved: Set; + let ghost bitmap_view: Set; + let ghost token_released: Set; + let ghost pre_seq: Seq; + let ghost pre_len: int; + } + proof! { + assert(range.start as usize <= range.end as usize); + instance_id = allocator.resource().instance_id(); + preserved = allocator.resource().value(); + pre_seq = allocator.value()@; + pre_len = allocator.value()@.len() as int; + bitmap_view = id_alloc_view(&allocator.value()); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator.value())); + assert(preserved.subset_of(bitmap_view)); + assert(bitmap_view == id_alloc_bits(pre_seq, pre_len)); + assert(pre_len == crate::arch::io::MAX_IO_PORT as int); + assert(crate::arch::io::MAX_IO_PORT as int <= usize::MAX as int); + assert(pre_len <= usize::MAX as int); + assert(claim.instance_id() == instance_id); + assert((range.end as usize) <= allocator.value()@.len()) by { + assert((range.end as usize) <= u16::MAX as usize); + assert((u16::MAX as usize) <= crate::arch::io::MAX_IO_PORT as usize); + assert(allocator.value()@.len() + == crate::arch::io::MAX_IO_PORT as int); + } + } + proof! { + let tracked r = allocator.tracked_borrow_mut_resource(); + r.claim_includes(&claim); + assert(port_id_set(range.start as usize, range.end as usize) <= r.value()); + assert(r.value() == preserved); + assert(port_id_set(range.start as usize, range.end as usize) <= preserved); + r.release(claim); + token_released = r.value(); + assert(token_released + == preserved.difference(port_id_set(range.start as usize, range.end as usize))); + assert forall|id: usize| + #![trigger token_released.contains(id)] + token_released.contains(id) implies { + &&& bitmap_view.contains(id) + &&& !(range.start as usize <= id < range.end as usize) + } by { + lemma_port_id_set_contains( + range.start as usize, + range.end as usize, + id, + ); + } + } + let allocator_inner = &mut *allocator; + /* Original Rust: self.allocator .lock() .free_consecutive(range.start as usize..range.end as usize); + */ + proof! { + assert(allocator_inner@.len() == crate::arch::io::MAX_IO_PORT as int); + assert(id_alloc_capacity(&allocator_inner) + == crate::arch::io::MAX_IO_PORT as usize); + assert(allocator_inner@ == pre_seq); + assert((range.end as usize) <= id_alloc_capacity(&allocator_inner)); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator_inner)); + assert(id_alloc_view(&allocator_inner) == bitmap_view); + assert forall|i: int| + range.start as usize <= i + && i < allocator_inner@.len() + && i < range.end as usize implies + allocator_inner@[i] + by { + assert(port_id_set(range.start as usize, range.end as usize) <= preserved); + assert(preserved.subset_of(bitmap_view)); + assert(bitmap_view == id_alloc_view(&allocator_inner)); + lemma_port_id_set_contains( + range.start as usize, + range.end as usize, + i as usize, + ); + lemma_id_alloc_view_contains(&allocator_inner, i as usize); + } + } + allocator_inner.free_consecutive(range.start as usize..range.end as usize); + proof! { + assert(allocator.value() == *allocator_inner); + let final_llen: int = allocator_inner@.len() as int; + assert(final_llen == pre_len); + assert(final_llen <= usize::MAX as int); + assert forall|id: usize| + #![trigger allocator.resource().value().contains(id)] + allocator.resource().value().contains(id) implies + id_alloc_view(&allocator_inner).contains(id) by { + lemma_port_id_set_contains(range.start as usize, range.end as usize, id); + lemma_id_alloc_bits_char(pre_seq, pre_len, id); + lemma_id_alloc_bits_char(allocator_inner@, final_llen, id); + assert(allocator.resource().value().contains(id) + == (preserved.contains(id) + && !port_id_set(range.start as usize, range.end as usize).contains(id))); + assert(port_id_set(range.start as usize, range.end as usize) <= preserved); + assert(preserved.subset_of(bitmap_view)); + assert(bitmap_view == id_alloc_bits(pre_seq, pre_len)); + assert(id_alloc_view(&allocator_inner) + == id_alloc_bits(allocator_inner@, final_llen)); + } + assert(allocator_inner.inv()); + assert(allocator_inner@.len() == crate::arch::io::MAX_IO_PORT as int); + assert(id_alloc_capacity(&allocator_inner) + == crate::arch::io::MAX_IO_PORT as usize); + assert(allocator.resource().instance_id() == instance_id); + assert(io_port_inner_inv_values( + allocator.resource().instance_id(), + allocator.resource().value(), + &allocator_inner, + )); + } + allocator.drop(); } } +verus! { + +/// Trusted boot-state fact required before accessing the global PIO allocator. +/// +/// Verus cannot currently mention an `exec static` in a specification, so this predicate is the +/// explicit specification boundary for the architecture's guarantee that [`init`] ran first. +pub uninterp spec fn io_port_allocator_initialized() -> bool; + +} // verus! pub(super) static IO_PORT_ALLOCATOR: Once = Once::new(); /// Initializes the static `IO_PORT_ALLOCATOR` and removes the system device I/O port regions. @@ -65,22 +603,24 @@ pub(super) static IO_PORT_ALLOCATOR: Once = Once::new(); /// /// 2. `MAX_IO_PORT` defined in `crate::arch::io` is guaranteed not to exceed the maximum /// value specified by architecture. -pub(crate) unsafe fn init() { +#[verifier::external_body] +pub(in crate::io) unsafe fn init() { // SAFETY: `MAX_IO_PORT` is guaranteed not to exceed the maximum value specified by architecture. let mut allocator = IdAlloc::with_capacity(crate::arch::io::MAX_IO_PORT as usize); - extern "C" { + unsafe extern "C" { fn __sensitive_io_ports_start(); fn __sensitive_io_ports_end(); } - let start = __sensitive_io_ports_start as usize; - let end = __sensitive_io_ports_end as usize; - assert!((end - start) % size_of::() == 0); + let start = __sensitive_io_ports_start as *const () as usize; + let end = __sensitive_io_ports_end as *const () as usize; + assert!((end - start).is_multiple_of(size_of::())); // Iterate through the sensitive I/O port ranges and remove them from the allocator. let io_port_range_count = (end - start) / size_of::(); for i in 0..io_port_range_count { - let range_base_addr = __sensitive_io_ports_start as usize + i * size_of::(); + let range_base_addr = + __sensitive_io_ports_start as *const () as usize + i * size_of::(); // SAFETY: The range is guaranteed to be valid as it is defined in the `.sensitive_io_ports` section. let port_range = unsafe { *(range_base_addr as *const RawIoPortRange) }; @@ -92,7 +632,15 @@ pub(crate) unsafe fn init() { } } + /* Original Rust: IO_PORT_ALLOCATOR.call_once(|| IoPortAllocator { allocator: SpinLock::new(allocator), + }); */ + IO_PORT_ALLOCATOR.call_once(|| IoPortAllocator { + allocator: SpinLock::new( + allocator, + Ghost::new(()), + Tracked::new(IoPortAllocation::initialize()), + ), }); } diff --git a/ostd/src/io/io_port/mod.rs b/ostd/src/io/io_port/mod.rs index 731ed3571..6f4c5671a 100644 --- a/ostd/src/io/io_port/mod.rs +++ b/ostd/src/io/io_port/mod.rs @@ -1,6 +1,10 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port and its allocator that allocates port I/O (PIO) to device drivers. -use crate::arch::device::io_port::{IoPortReadAccess, IoPortWriteAccess, PortRead, PortWrite}; +use vstd::prelude::*; + +use crate::arch::device::io_port::{ + IoPortReadAccess, IoPortWriteAccess, PortRead, PortWrite, valid_io_port_access, +}; mod allocator; use core::{marker::PhantomData, mem::size_of}; @@ -8,6 +12,11 @@ use core::{marker::PhantomData, mem::size_of}; pub(super) use self::allocator::init; use crate::{Error, prelude::*}; +verus! { + +broadcast use crate::arch::device::io_port::group_io_port_models; + +} // verus! /// An I/O port, representing a specific address in the I/O address of x86. /// /// The following code shows and example to read and write u32 value to an I/O port: @@ -20,23 +29,183 @@ use crate::{Error, prelude::*}; /// } /// ``` /// +#[derive(Debug)] +#[verus_verify] pub struct IoPort { port: u16, + is_overlapping: bool, value_marker: PhantomData, access_marker: PhantomData, } +verus! { + +impl View for IoPort { + type V = u16; + + closed spec fn view(&self) -> u16 { + self.port + } +} + +impl IoPort { + /// The complete byte range occupied by this typed port lies in the x86 PIO address space. + #[verifier::type_invariant] + pub open spec fn well_formed(&self) -> bool { + valid_io_port_access::(self@) + } + + /// Whether the port was acquired as overlapping: it occupies only its first port. + /// + /// Marks the occupied range of [`Self::claim_matches_set`] and the released range of + /// [`Self::drop`]. + pub closed spec fn is_overlapping(&self) -> bool { + self.is_overlapping + } + + /// Whether `claim` is the allocator-issued ownership token for this port's occupied range: + /// the complete typed range, or only the first port if the port was acquired as + /// overlapping. + pub open spec fn claim_matches_set(&self, claim: Set) -> bool { + claim == port_id_set( + self@ as usize, + if self.is_overlapping() { + (self@ as usize + 1) as usize + } else { + (self@ as usize + size_of::()) as usize + }, + ) + } +} + +/// Set of byte-sized PIO numbers in the half-open interval `[start, end)`. +pub open spec fn port_id_set(start: usize, end: usize) -> Set + decreases end - start, +{ + if start < end { + port_id_set(start, (end - 1) as usize).insert((end - 1) as usize) + } else { + Set::empty() + } +} + +/// Extending a PIO interval by one byte is equivalent to inserting its old endpoint. +pub proof fn lemma_port_id_set_insert(start: usize, end: usize) + requires + start <= end, + end < usize::MAX, + ensures + port_id_set(start, end).insert(end) == port_id_set(start, (end + 1) as usize), +{ +} + +/// Membership characterization for [`port_id_set`]. +pub proof fn lemma_port_id_set_contains(start: usize, end: usize, id: usize) + requires + start <= end, + ensures + port_id_set(start, end).contains(id) <==> start <= id < end, + decreases end - start, +{ + if start < end { + lemma_port_id_set_contains(start, (end - 1) as usize, id); + } +} + +} // verus! +/// Returns the initialized global PIO allocator. +/// +/// The executable body intentionally preserves the original `get().unwrap()` behavior. This +/// helper is trusted only because Verus cannot connect an `exec static` to a spec-level boot-state +/// predicate. +#[verifier::external_body] +#[verus_spec( + requires allocator::io_port_allocator_initialized(), +)] +fn initialized_allocator() -> &'static allocator::IoPortAllocator { + allocator::IO_PORT_ALLOCATOR.get().unwrap() +} + +#[verus_verify] impl IoPort { /// Acquires an `IoPort` instance for the given range. + /// + /// This method will mark all ports in the PIO range as occupied. + #[verus_spec(result => + with + -> claim: Tracked>, + requires + size_of::() <= u16::MAX, + port as usize + size_of::() <= u16::MAX, + valid_io_port_access::(port), + allocator::io_port_allocator_initialized(), + ensures + result is Ok <==> claim@ is Some, + result matches Ok(io_port) ==> { + &&& io_port@ == port + &&& !io_port.is_overlapping() + &&& io_port.well_formed() + &&& io_port.claim_matches_set(claim@->Some_0.set()) + &&& claim@->Some_0.instance_id() == allocator::io_port_allocator_instance_id() + }, + )] pub fn acquire(port: u16) -> Result> { - allocator::IO_PORT_ALLOCATOR - .get() - .unwrap() - .acquire(port) - .ok_or(Error::AccessDenied) + proof_decl! { + let tracked mut claim: Tracked> = Tracked(None); + } + let port = { + /* Original Rust: allocator::IO_PORT_ALLOCATOR.get().unwrap() */ + #[verus_spec(with Tracked(&mut claim))] + initialized_allocator().acquire(port, false) + }; + let result = port.ok_or(Error::AccessDenied); + proof_decl! { + let tracked claim_val: Option = claim.get(); + } + proof_with!(|= Tracked(claim_val)); + result + } + + /// Acquires an `IoPort` instance that may overlap with other `IoPort`s. + /// + /// This method will only mark the first port in the PIO range as occupied. + #[verus_spec(result => + with + -> claim: Tracked>, + requires + size_of::() <= u16::MAX, + port as usize + size_of::() <= u16::MAX, + valid_io_port_access::(port), + allocator::io_port_allocator_initialized(), + ensures + result is Ok <==> claim@ is Some, + result matches Ok(io_port) ==> { + &&& io_port@ == port + &&& io_port.is_overlapping() + &&& io_port.well_formed() + &&& io_port.claim_matches_set(claim@->Some_0.set()) + &&& claim@->Some_0.instance_id() == allocator::io_port_allocator_instance_id() + }, + )] + pub fn acquire_overlapping(port: u16) -> Result> { + proof_decl! { + let tracked mut claim: Tracked> = Tracked(None); + } + let port = { + /* Original Rust: allocator::IO_PORT_ALLOCATOR.get().unwrap() */ + #[verus_spec(with Tracked(&mut claim))] + initialized_allocator().acquire(port, true) + }; + let result = port.ok_or(Error::AccessDenied); + proof_decl! { + let tracked claim_val: Option = claim.get(); + } + proof_with!(|= Tracked(claim_val)); + result } /// Returns the port number. + #[verus_spec(returns self@)] pub const fn port(&self) -> u16 { self.port } @@ -46,48 +215,114 @@ impl IoPort { size_of::() as u16 } - /// Create an I/O port. + /// Creates an I/O port. + /// + /// # Safety + /// + /// Reading from or writing to the I/O port may have side effects. Those side effects must + /// not cause soundness problems (e.g., they must not corrupt the kernel memory). + #[verus_spec(ret => + requires + size_of::() <= u16::MAX, + port as usize + size_of::() <= u16::MAX, + valid_io_port_access::(port), + ensures + ret@ == port, + !ret.is_overlapping(), + ret.well_formed(), + )] + pub(crate) const unsafe fn new(port: u16) -> Self { + // SAFETY: The safety is upheld by the caller. + unsafe { Self::new_overlapping(port, false) } + } + + /// Creates an I/O port. + /// + /// See [`allocator::IoPortAllocator::acquire`] for an explanation of the `is_overlapping` + /// argument. /// /// # Safety /// - /// This function is marked unsafe as creating an I/O port is considered - /// a privileged operation. - pub const unsafe fn new(port: u16) -> Self { + /// Reading from or writing to the I/O port may have side effects. Those side effects must + /// not cause soundness problems (e.g., they must not corrupt the kernel memory). + #[verus_spec(ret => + requires + size_of::() <= u16::MAX, + port as usize + size_of::() <= u16::MAX, + valid_io_port_access::(port), + ensures + ret@ == port, + ret.is_overlapping() == is_overlapping, + ret.well_formed(), + )] + const unsafe fn new_overlapping(port: u16, is_overlapping: bool) -> Self { Self { port, + is_overlapping, value_marker: PhantomData, access_marker: PhantomData, } } + + /// Releases the allocator claim for this port. + /// + /// VERUS LIMITATION: this is called explicitly because Verus does not yet support proving + /// the standard `Drop` implementation below. + #[verus_spec( + with + Tracked(claim): Tracked, + requires + allocator::io_port_allocator_initialized(), + claim.instance_id() == allocator::io_port_allocator_instance_id(), + self.claim_matches_set(claim.set()), + self@ as usize + + (if self.is_overlapping() { 1 } else { size_of::() }) <= u16::MAX, + )] + pub fn drop(self) { + let range = if self.is_overlapping { + self.port..(self.port + 1) + } else { + self.port..(self.port + size_of::() as u16) + }; + unsafe { + #[verus_spec(with Tracked(claim))] + initialized_allocator().recycle(range); + } + } } +#[verus_verify] +#[verifier::allow(undeclared_external_trait)] impl IoPort { /// Reads from the I/O port - #[inline] + #[verus_spec(requires self.well_formed())] pub fn read(&self) -> T { unsafe { PortRead::read_from_port(self.port) } } } +#[verus_verify] +#[verifier::allow(undeclared_external_trait)] impl IoPort { /// Writes to the I/O port - #[inline] + #[verus_spec(requires self.well_formed())] pub fn write(&self, value: T) { unsafe { PortWrite::write_to_port(self.port, value) } } } -impl Drop for IoPort { +/* impl Drop for IoPort { fn drop(&mut self) { - // SAFETY: The caller have ownership of the PIO region. - unsafe { - allocator::IO_PORT_ALLOCATOR - .get() - .unwrap() - .recycle(self.port..(self.port + size_of::() as u16)); - } + let range = if !self.is_overlapping { + self.port..(self.port + size_of::() as u16) + } else { + self.port..(self.port + 1) + }; + + // SAFETY: We have ownership of the PIO region. + unsafe { allocator::IO_PORT_ALLOCATOR.get().unwrap().recycle(range) }; } -} +} */ /// Reserves an I/O port range which may refer to the port I/O range used by the /// system device driver. @@ -105,7 +340,8 @@ macro_rules! reserve_io_port_range { const _: () = { #[used] - #[link_section = ".sensitive_io_ports"] + // SAFETY: This is properly handled in the linker script. + #[unsafe(link_section = ".sensitive_io_ports")] static _RANGE: crate::io::RawIoPortRange = crate::io::RawIoPortRange { begin: $range.start, end: $range.end, @@ -142,15 +378,14 @@ macro_rules! sensitive_io_port { $(#[$meta])* $vis static $name: IoPort<$size, $access> = { #[used] - #[link_section = ".sensitive_io_ports"] + // SAFETY: This is properly handled in the linker script. + #[unsafe(link_section = ".sensitive_io_ports")] static _RESERVED_IO_PORT_RANGE: crate::io::RawIoPortRange = crate::io::RawIoPortRange { begin: $name.port(), end: $name.port() + $name.size(), }; - unsafe { - IoPort::new($port) - } + unsafe { IoPort::new($port) } }; )* }; @@ -160,8 +395,9 @@ pub(crate) use reserve_io_port_range; pub(crate) use sensitive_io_port; #[doc(hidden)] -#[derive(Debug, Clone, Copy)] #[repr(C)] +#[derive(Clone, Copy, Debug)] +#[verus_verify] pub(crate) struct RawIoPortRange { pub(crate) begin: u16, pub(crate) end: u16, diff --git a/ostd/src/io/mod.rs b/ostd/src/io/mod.rs index a87940453..e868aa4b3 100644 --- a/ostd/src/io/mod.rs +++ b/ostd/src/io/mod.rs @@ -5,7 +5,9 @@ //! through _allocators_. There are two types of device I/O: //! - `IoMem` for memory I/O (MMIO). //! - `IoPort` for port I/O (PIO). -mod io_mem; +use vstd::prelude::*; + +pub(crate) mod io_mem; use cfg_if::cfg_if; @@ -15,7 +17,8 @@ pub(crate) use self::io_mem::IoMemAllocatorBuilder; cfg_if!( if #[cfg(target_arch = "x86_64")] { mod io_port; - pub use io_port::IoPort; + + pub use self::io_port::IoPort; pub(crate) use self::io_port::{reserve_io_port_range, sensitive_io_port, RawIoPortRange}; } ); @@ -34,13 +37,14 @@ cfg_if!( /// /// 3. `MAX_IO_PORT` defined in `crate::arch::io` is guaranteed not to /// exceed the maximum value specified by architecture. +#[verus_verify] pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { // SAFETY: The safety is upheld by the caller. - unsafe { self::io_mem::init(io_mem_builder) }; + unsafe { io_mem::init(io_mem_builder) }; // SAFETY: The safety is upheld by the caller. #[cfg(target_arch = "x86_64")] unsafe { - self::io_port::init() + io_port::init() }; } diff --git a/ostd/src/lib.rs b/ostd/src/lib.rs index 8a90a3876..a4970bd77 100644 --- a/ostd/src/lib.rs +++ b/ostd/src/lib.rs @@ -38,16 +38,16 @@ pub mod arch; //#[path = "arch/riscv/mod.rs"] //pub mod arch; pub mod boot; -/*pub mod bus; -pub mod console; +pub mod bus; +/*pub mod console; pub mod cpu;*/ pub mod error; -/*pub mod io; -pub mod logger;*/ +pub mod io; +/*pub mod logger;*/ pub mod mm; -/*pub mod panic; +/*pub mod panic;*/ pub mod prelude; -pub mod smp;*/ +/*pub mod smp;*/ pub mod sync; pub mod task; pub mod timer; @@ -64,9 +64,9 @@ pub use ostd_macros::{ panic_handler, };*/ pub use ostd_pod::Pod; -/* -pub use self::{error::Error, prelude::Result}; +pub use self::{error::Error, prelude::Result}; +/* /// Initializes OSTD. /// /// This function represents the first phase booting up the system. It makes diff --git a/ostd/src/prelude.rs b/ostd/src/prelude.rs index f9ab829ef..bb1eeaf17 100644 --- a/ostd/src/prelude.rs +++ b/ostd/src/prelude.rs @@ -6,7 +6,7 @@ pub type Result = core::result::Result; pub(crate) use alloc::{boxed::Box, sync::Arc, vec::Vec}; - +/* #[cfg(ktest)] pub use ostd_macros::ktest; @@ -14,4 +14,4 @@ pub use crate::{ early_print as print, early_println as println, mm::{Paddr, UntypedMem, Vaddr}, panic::abort, -}; +}; */ diff --git a/verified_libs/vstd_extra/Cargo.toml b/verified_libs/vstd_extra/Cargo.toml index a4dd253d4..b95c61f43 100644 --- a/verified_libs/vstd_extra/Cargo.toml +++ b/verified_libs/vstd_extra/Cargo.toml @@ -16,3 +16,6 @@ std = ["vstd/std"] [dependencies] vstd = { workspace = true } bitvec.workspace = true + +[target.'cfg(target_arch = "x86_64")'.dependencies] +x86_64 = "0.14.13" diff --git a/verified_libs/vstd_extra/src/external/int_specs.rs b/verified_libs/vstd_extra/src/external/int_specs.rs index 1998925a5..239a7919a 100644 --- a/verified_libs/vstd_extra/src/external/int_specs.rs +++ b/verified_libs/vstd_extra/src/external/int_specs.rs @@ -27,6 +27,15 @@ pub assume_specification[ u32::is_power_of_two ](self_: u32) -> (r: bool) no_unwind ; +/// On a little-endian target, converting a native-endian `u32` to little endian is the identity. +#[cfg(target_endian = "little")] +pub assume_specification[ u32::to_le ](value: u32) -> u32 + returns + value, + opens_invariants none + no_unwind +; + pub assume_specification[ u64::is_power_of_two ](self_: u64) -> (r: bool) returns is_pow2(self_ as int), diff --git a/verified_libs/vstd_extra/src/external/io_port.rs b/verified_libs/vstd_extra/src/external/io_port.rs new file mode 100644 index 000000000..d4ce66be8 --- /dev/null +++ b/verified_libs/vstd_extra/src/external/io_port.rs @@ -0,0 +1,78 @@ +//! Specifications for x86 I/O-port access types and traits. +use core::mem::size_of; + +use vstd::prelude::*; +use x86_64::{ + instructions::port::{ReadWriteAccess, WriteOnlyAccess}, + structures::port::{PortRead, PortWrite}, +}; + +verus! { + +/// Whether a `T`-typed access at `port` fits in the PIO byte range `0..=u16::MAX`. +/// +/// Uninterpreted: `PortRead`/`PortWrite` are user-implementable, so meaning comes only from +/// the trusted widths in [`group_io_port_models`]. ISA-level fact only — no claim about +/// device decoding, access permission, or ownership. +pub uninterp spec fn valid_io_port_access(port: u16) -> bool; + +/// Trusted: `u8` ports are written and read via `outb`/`inb`. +pub broadcast axiom fn axiom_u8_pio_model(port: u16) + ensures + #[trigger] valid_io_port_access::(port) <==> port + size_of::() <= u16::MAX + 1, +; + +/// Trusted: `u16` ports are written and read via `outw`/`inw`. +pub broadcast axiom fn axiom_u16_pio_model(port: u16) + ensures + #[trigger] valid_io_port_access::(port) <==> port + size_of::() <= u16::MAX + 1, +; + +/// Trusted: `u32` ports are written and read via `outl`/`inl`. +pub broadcast axiom fn axiom_u32_pio_model(port: u16) + ensures + #[trigger] valid_io_port_access::(port) <==> port + size_of::() <= u16::MAX + 1, +; + +/// The trusted instances of the PIO model. +pub broadcast group group_io_port_models { + axiom_u8_pio_model, + axiom_u16_pio_model, + axiom_u32_pio_model, +} + +/// Opaque specification boundary for the third-party read/write access marker. +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExReadWriteAccess(ReadWriteAccess); + +/// Opaque specification boundary for the third-party write-only access marker. +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExWriteOnlyAccess(WriteOnlyAccess); + +/// Trusted specification boundary for values that can be read from an x86 I/O port. +#[verifier::external_trait_specification] +pub trait ExPortRead { + type ExternalTraitSpecificationFor: PortRead; + + /// A port read can produce any value supplied by the device. + unsafe fn read_from_port(port: u16) -> Self where Self: Sized + requires + valid_io_port_access::(port), + ; +} + +/// Trusted specification boundary for values that can be written to an x86 I/O port. +#[verifier::external_trait_specification] +pub trait ExPortWrite { + type ExternalTraitSpecificationFor: PortWrite; + + /// A port write has no modeled logical effect on kernel memory. + unsafe fn write_to_port(port: u16, value: Self) where Self: Sized + requires + valid_io_port_access::(port), + ; +} + +} // verus! diff --git a/verified_libs/vstd_extra/src/external/mod.rs b/verified_libs/vstd_extra/src/external/mod.rs index 868f67cd4..8414b33c1 100644 --- a/verified_libs/vstd_extra/src/external/mod.rs +++ b/verified_libs/vstd_extra/src/external/mod.rs @@ -8,6 +8,8 @@ pub mod convert; pub mod deref; pub mod ilog2; pub mod int_specs; +#[cfg(target_arch = "x86_64")] +pub mod io_port; pub mod iter; pub mod nonnull; pub mod ptr; @@ -20,6 +22,8 @@ pub use bitvec::*; pub use cmp::*; pub use ilog2::*; pub use int_specs::*; +#[cfg(target_arch = "x86_64")] +pub use io_port::*; pub use iter::*; pub use nonnull::*; pub use ptr::*;