From cf097d06f507e23374189c75c8961259dd033521 Mon Sep 17 00:00:00 2001 From: Evan Johnson Date: Wed, 17 Jul 2024 14:38:12 -0700 Subject: [PATCH] sort of verified. need update inside slice fix to work to continue --- arch/cortex-m/src/mpu.rs | 85 +++++++++++++++++++++++++++--------- kernel/src/utilities/math.rs | 36 +++++++++++++++ 2 files changed, 101 insertions(+), 20 deletions(-) diff --git a/arch/cortex-m/src/mpu.rs b/arch/cortex-m/src/mpu.rs index 17ca986ebc..0e8d6f401b 100644 --- a/arch/cortex-m/src/mpu.rs +++ b/arch/cortex-m/src/mpu.rs @@ -17,6 +17,23 @@ use kernel::utilities::registers::interfaces::{Readable, Writeable}; use kernel::utilities::registers::{register_bitfields, FieldValue, ReadOnly, ReadWrite}; use kernel::utilities::StaticRef; +#[flux::sig(fn(x: bool[true]))] +fn assert(_x: bool) {} + +#[flux::sig(fn(b:bool) ensures b)] +pub fn assume(b: bool) { + if !b { + panic!("assume fails") + } +} + +// VTOCK-TODO: supplementary proof? +#[flux::sig(fn(n: u32{n < 32}) -> usize {r: r > 0 })] +#[flux::trusted] +fn power_of_two(n: u32) -> usize { + 1_usize << n +} + /// MPU Registers for the Cortex-M3, Cortex-M4 and Cortex-M7 families /// Described in section 4.5 of /// @@ -132,11 +149,14 @@ const MPU_BASE_ADDRESS: StaticRef = /// /// There should only be one instantiation of this object as it represents /// real hardware. -pub struct MPU { +/// +#[flux::invariant(MIN_REGION_SIZE > 0 && MIN_REGION_SIZE < 2147483648)] +pub struct MPU { /// MMIO reference to MPU registers. registers: StaticRef, /// Monotonically increasing counter for allocated regions, used /// to assign unique IDs to `CortexMConfig` instances. + #[flux::field({Cell | MIN_REGION_SIZE > 0 && MIN_REGION_SIZE < 2147483648})] config_count: Cell, /// Optimization logic. This is used to indicate which application the MPU /// is currently configured for so that the MPU can skip updating when the @@ -144,7 +164,8 @@ pub struct MPU { hardware_is_configured_for: OptionalCell, } -impl MPU { +impl MPU { + #[flux::trusted] pub const unsafe fn new() -> Self { Self { registers: MPU_BASE_ADDRESS, @@ -165,12 +186,15 @@ impl MPU { + +const NUM_REGIONS: usize = 8; + +pub struct CortexMConfig { /// Unique ID for this configuration, assigned from a /// monotonically increasing counter in the MPU struct. id: NonZeroUsize, /// The computed region configuration for this process. - regions: [CortexMRegion; NUM_REGIONS], + regions: [CortexMRegion; 8], /// Has the configuration changed since the last time the this process /// configuration was written to hardware? is_dirty: Cell, @@ -182,7 +206,7 @@ pub struct CortexMConfig { /// needs. const APP_MEMORY_REGION_MAX_NUM: usize = 1; -impl fmt::Display for CortexMConfig { +impl fmt::Display for CortexMConfig { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "\r\n Cortex-M MPU")?; for (i, region) in self.regions.iter().enumerate() { @@ -236,7 +260,9 @@ impl fmt::Display for CortexMConfig { } } -impl CortexMConfig { +impl CortexMConfig { + #[flux::trusted] + #[flux::sig(fn(&CortexMConfig) -> Option)] fn unused_region_number(&self) -> Option { for (number, region) in self.regions.iter().enumerate() { if number <= APP_MEMORY_REGION_MAX_NUM { @@ -276,6 +302,8 @@ impl CortexMRegion { subregions: Option<(usize, usize)>, permissions: mpu::Permissions, ) -> CortexMRegion { + assume(region_size > 1 && region_size < (u32::MAX as usize)); + // Determine access and execute permissions let (access, execute) = match permissions { mpu::Permissions::ReadWriteExecute => ( @@ -305,7 +333,7 @@ impl CortexMRegion { + RegionBaseAddress::VALID::UseRBAR + RegionBaseAddress::REGION.val(region_num as u32); - let size_value = math::log_base_two(region_size as u32) - 1; + let size_value = math::log_base_two_u32_usize(region_size) - 1; // Attributes register let mut attributes = RegionAttributes::ENABLE::SET @@ -370,10 +398,8 @@ impl CortexMRegion { } } -impl mpu::MPU - for MPU -{ - type MpuConfig = CortexMConfig; +impl mpu::MPU for MPU { + type MpuConfig = CortexMConfig; fn enable_app_mpu(&self) { // Enable the MPU, disable it during HardFault/NMI handlers, and allow @@ -411,9 +437,14 @@ impl mpu::MPU } fn reset_config(&self, config: &mut Self::MpuConfig) { - for i in 0..NUM_REGIONS { - config.regions[i] = CortexMRegion::empty(i); - } + config.regions[0] = CortexMRegion::empty(0); + config.regions[1] = CortexMRegion::empty(1); + config.regions[2] = CortexMRegion::empty(2); + config.regions[3] = CortexMRegion::empty(3); + config.regions[4] = CortexMRegion::empty(4); + config.regions[5] = CortexMRegion::empty(5); + config.regions[6] = CortexMRegion::empty(6); + config.regions[7] = CortexMRegion::empty(7); config.is_dirty.set(true); } @@ -426,6 +457,8 @@ impl mpu::MPU permissions: mpu::Permissions, config: &mut Self::MpuConfig, ) -> Option { + assume(min_region_size < 2147483648); + // Check that no previously allocated regions overlap the unallocated memory. for region in config.regions.iter() { if region.overlaps(unallocated_memory_start, unallocated_memory_size) { @@ -453,7 +486,6 @@ impl mpu::MPU let mut region_start = start; let mut region_size = size; let mut subregions = None; - // We can only create an MPU region if the size is a power of two and it divides // the start address. If this is not the case, the first thing we try to do to // cover the memory region is to use a larger MPU region and expose certain subregions. @@ -469,7 +501,8 @@ impl mpu::MPU let tz = start.trailing_zeros(); if tz < 32 { // Find the largest power of two that divides `start` - 1_usize << tz + // 1_usize << tz + power_of_two(tz) } else { // This case means `start` is 0. let mut ceil = math::closest_power_of_two(size as u32) as usize; @@ -493,6 +526,8 @@ impl mpu::MPU size += subregion_size - (size % subregion_size); } + assume(size < 2147483648); + let end = start + size; let underlying_region_end = underlying_region_start + underlying_region_size; @@ -516,7 +551,8 @@ impl mpu::MPU // In this case, we can't use subregions to solve the alignment // problem. Instead, we round up `size` to a power of two and // shift `start` up in memory to make it align with `size`. - size = math::closest_power_of_two(size as u32) as usize; + + size = math::closest_power_of_two_usize(size); start += size - (start % size); region_start = start; @@ -545,6 +581,7 @@ impl mpu::MPU Some(mpu::Region::new(start as *const u8, size)) } + #[flux::trusted] fn remove_memory_region( &self, region: mpu::Region, @@ -593,10 +630,11 @@ impl mpu::MPU min_memory_size, initial_app_memory_size + initial_kernel_memory_size, ); + assume(memory_size > 1 && memory_size < 2147483648); // Size must be a power of two, so: // https://www.youtube.com/watch?v=ovo6zwv6DX4. - let mut memory_size_po2 = math::closest_power_of_two(memory_size as u32) as usize; + let mut memory_size_po2 = math::closest_power_of_two_usize(memory_size); let exponent = math::log_base_two(memory_size_po2 as u32); // Check for compliance with the constraints of the MPU. @@ -612,8 +650,10 @@ impl mpu::MPU // Region size is the actual size the MPU region will be set to, and is // half of the total power of two size we are allocating to the app. - let mut region_size = memory_size_po2 / 2; + //assume(memory_size_po2 > 1); + let mut region_size = memory_size_po2 / 2; + //assume(region_size > 0); // The region should start as close as possible to the start of the // unallocated memory. let mut region_start = unallocated_memory_start as usize; @@ -641,7 +681,10 @@ impl mpu::MPU // Calculates the end address of the enabled subregions and the initial // kernel memory break. let subregions_enabled_end = region_start + num_enabled_subregions * subregion_size; - let kernel_memory_break = region_start + memory_size_po2 - initial_kernel_memory_size; + //let kernel_memory_break = region_start + memory_size_po2 - initial_kernel_memory_size; + + let kernel_memory_break = + (region_start + memory_size_po2).checked_sub(initial_kernel_memory_size)?; // If the last subregion covering app-owned memory overlaps the start of // kernel-owned memory, we make the entire process memory block twice as @@ -668,6 +711,8 @@ impl mpu::MPU let num_enabled_subregions0 = cmp::min(num_enabled_subregions, 8); let num_enabled_subregions1 = num_enabled_subregions.saturating_sub(8); + assume(num_enabled_subregions0 > 0); + let region0 = CortexMRegion::new( region_start as *const u8, region_size, diff --git a/kernel/src/utilities/math.rs b/kernel/src/utilities/math.rs index 53d2752f93..32e5339a9a 100644 --- a/kernel/src/utilities/math.rs +++ b/kernel/src/utilities/math.rs @@ -6,8 +6,13 @@ use core::f32; + +// VTOCK-TODO: supplementary Z3 proofs for these two functions + /// Get closest power of two greater than the given number. #[flux::trusted] +// 2147483648 is half of u32::MAX. Anything higher than that causes overflow +#[flux::sig(fn(num: u32) -> u32{r: (num < 2147483648 => r > num)})] pub fn closest_power_of_two(mut num: u32) -> u32 { num -= 1; num |= num >> 1; @@ -19,6 +24,22 @@ pub fn closest_power_of_two(mut num: u32) -> u32 { num } +#[flux::trusted] +// 2147483648 is half of u32::MAX. Anything higher than that deviates from closest_power_of_two +// I added this function to avoid unnecessary downcasts, which can be dangerous. +#[flux::sig(fn(num: usize) -> usize{r: (num < 2147483648 => r > num)})] +pub fn closest_power_of_two_usize(mut num: usize) -> usize { + num -= 1; + num |= num >> 1; + num |= num >> 2; + num |= num >> 4; + num |= num >> 8; + num |= num >> 16; + num += 1; + num +} + + #[derive(Copy, Clone, Debug, PartialEq, PartialOrd, Eq, Ord)] pub struct PowerOfTwo(u32); @@ -58,6 +79,7 @@ impl PowerOfTwo { /// Note: this is the floor of the result. Also, an input of 0 results in an /// output of 0 #[flux::trusted] +#[flux::sig(fn(num: u32) -> u32{r: (r < 32) && (num > 1 => r > 0)})] pub fn log_base_two(num: u32) -> u32 { if num == 0 { 0 @@ -66,8 +88,22 @@ pub fn log_base_two(num: u32) -> u32 { } } +#[flux::trusted] +#[flux::sig(fn(num: usize{num < 4294967295}) -> u32{r: (r < 32) && (num > 1 => r > 0)})] +// Push cast into trusted function +// can only be used if downcast is not required +pub fn log_base_two_u32_usize(num: usize) -> u32 { + if num == 0 { + 0 + } else { + 31 - num.leading_zeros() + } +} + + /// Log base 2 of 64 bit unsigned integers. #[flux::trusted] +#[flux::sig(fn(num: u64) -> u32{r: r < 64 && (num > 1 => r > 0)})] pub fn log_base_two_u64(num: u64) -> u32 { if num == 0 { 0