diff --git a/arch/cortex-m/src/mpu.rs b/arch/cortex-m/src/mpu.rs index 819b537732..b94319e876 100644 --- a/arch/cortex-m/src/mpu.rs +++ b/arch/cortex-m/src/mpu.rs @@ -6,6 +6,8 @@ //! Implementation of the memory protection unit for the Cortex-M0+, Cortex-M3, //! Cortex-M4, and Cortex-M7 +// TODO: verify configure_mpu with configure_for + use core::cell::Cell; use core::cmp; use core::fmt; @@ -43,13 +45,15 @@ flux_rs::defs! { fn srd(reg:bitvec<32>) -> int { extract(reg, 0x0000ff00, 8) } fn size(reg:bitvec<32>) -> int { extract(reg, 0x0000003e, 1) } + fn value(fv: FieldValueU32) -> bitvec<32> { fv.value} + - fn map_set(m: Map, k: int, v: int) -> Map { map_store(m, k, v) } - fn map_get(m: Map, k:int) -> int { map_select(m, k) } - fn map_def(v: int) -> Map { map_default(v) } + fn map_set(m: Map>, k: int, v: bitvec<32>) -> Map> { map_store(m, k, v) } + fn map_get(m: Map>, k:int) -> bitvec<32> { map_select(m, k) } + fn map_def(v: bitvec<32>) -> Map> { map_default(v) } - fn enabled(mpu: MPU) -> bool { enable(mpu.ctrl)} + // fn enabled(mpu: MPU) -> bool { enable(mpu.ctrl)} // VTOCK_TODO: simplify fn configured_for(mpu: MPU, config: CortexMConfig) -> bool { map_get(mpu.regions, 0) == map_get(config.regions, 0) && @@ -111,8 +115,14 @@ flux_rs::defs! { fn can_access(mpu: MPU, addr: int, sz: int, perms: mpu::Permissions) -> bool { true // TODO: + } + fn config_can_access(config: CortexMConfig, addr: int, sz: int, perms: mpu::Permissions) -> bool { + true // TODO: + } + fn config_cant_access(config: CortexMConfig, addr: int, sz: int) -> bool { + true // TODO: } } @@ -131,7 +141,7 @@ fn power_of_two(n: u32) -> usize { } #[flux_rs::opaque] -#[flux_rs::refined_by(regions: Map, attrs: Map)] +#[flux_rs::refined_by(regions: Map>, attrs: Map>)] pub struct HwGhostState {} impl HwGhostState { #[flux_rs::trusted] @@ -144,7 +154,7 @@ impl HwGhostState { /// Described in section 4.5 of /// #[repr(C)] -#[flux_rs::refined_by(ctrl: bitvec<32>, rnr: bitvec<32>, rbar: bitvec<32>, rasr: bitvec<32>, regions: Map, attrs: Map)] +#[flux_rs::refined_by(ctrl: bitvec<32>, rnr: bitvec<32>, rbar: bitvec<32>, rasr: bitvec<32>, regions: Map>, attrs: Map>)] pub struct MpuRegisters { /// Indicates whether the MPU is present and, if so, how many regions it /// supports. @@ -266,7 +276,7 @@ register_bitfields![u32, /// real hardware. /// #[flux_rs::invariant(MIN_REGION_SIZE > 0 && MIN_REGION_SIZE < 2147483648)] -#[flux_rs::refined_by(ctrl: bitvec<32>, rnr: bitvec<32>, rbar: bitvec<32>, rasr: bitvec<32>, regions: Map, attrs: Map)] +#[flux_rs::refined_by(ctrl: bitvec<32>, rnr: bitvec<32>, rbar: bitvec<32>, rasr: bitvec<32>, regions: Map>, attrs: Map>)] pub struct MPU { /// MMIO reference to MPU registers. #[field(MpuRegisters[ctrl, rnr, rbar, rasr, regions, attrs])] @@ -316,7 +326,10 @@ impl MPU { // VTOCK CODE #[flux_rs::trusted] - #[flux_rs::sig(fn(self: &strg Self[@mpu], &CortexMRegion[@addr, @attrs]) ensures self: Self[mpu.ctrl, mpu.rnr, addr.value, attrs.value, map_store(mpu.regions, region(mpu.rbar), bv_bv32_to_int(addr.value)), map_store(mpu.attrs, region(mpu.rbar), bv_bv32_to_int(attrs.value))])] + #[flux_rs::sig(fn(self: &strg Self[@mpu], &CortexMRegion[@addr, @attrs]) ensures + self: Self[mpu.ctrl, mpu.rnr, addr.value, attrs.value, + map_store(mpu.regions, region(addr.value), addr.value), + map_store(mpu.attrs, region(addr.value), attrs.value)])] fn commit_region(&mut self, region: &CortexMRegion) { self.registers.rbar.write(region.base_address()); self.registers.rasr.write(region.attributes()); @@ -331,8 +344,8 @@ impl MPU { const NUM_REGIONS: usize = 8; -#[flux_rs::opaque] -#[flux_rs::refined_by(dirty: bool, regions: Map, attrs: Map)] +// #[flux_rs::opaque] +#[flux_rs::refined_by(regions: Map>, attrs: Map>)] pub struct CortexMConfig { /// Unique ID for this configuration, assigned from a /// monotonically increasing counter in the MPU struct. @@ -342,6 +355,9 @@ pub struct CortexMConfig { /// Has the configuration changed since the last time the this process /// configuration was written to hardware? is_dirty: Cell, + + #[field(HwGhostState[regions, attrs])] + hw_state: HwGhostState, } /// Records the index of the last region used for application RAM memory. @@ -394,25 +410,26 @@ impl fmt::Display for CortexMConfig { } impl CortexMConfig { - #[flux_rs::trusted] fn id(&self) -> NonZeroUsize { self.id } - #[flux_rs::trusted] fn is_dirty(&self) -> bool { self.is_dirty.get() } - #[flux_rs::trusted] fn set_dirty(&self, b: bool) { self.is_dirty.set(b) } #[flux_rs::trusted] // #[flux_rs::sig(fn(self: &Self, idx: usize, region: CortexMRegion))] - // map_get - fn region_get(&self, idx: usize) -> &CortexMRegion { + #[flux_rs::sig(fn(&CortexMConfig[@self], {usize[@idx] | idx < 8}) -> &CortexMRegion{r: + region(value(r.rbar)) == idx && + value(r.rbar) == map_get(self.regions, idx) && + value(r.rasr) == map_get(self.attrs, idx) + })] + fn get_region(&self, idx: usize) -> &CortexMRegion { &self.regions[idx] } @@ -591,11 +608,16 @@ impl CortexMRegion { } } +#[flux_rs::assoc(fn enabled(self: Self) -> bool {enable(self.ctrl)} )] +// #[flux_rs::assoc(fn configured_for(self: Self, config: Self::MpuConfig) -> bool {false} )] +// #[flux_rs::assoc(fn can_access(self: Self, addr: int, sz: int, perms: Permissions) -> bool {false} )] impl mpu::MPU for MPU { type MpuConfig = CortexMConfig; - #[flux_rs::sig(fn(self: &strg Self) ensures self: Self)] + // #[flux_rs::sig(fn(self: &strg Self) ensures self: Self)] + #[flux_rs::sig(fn(self: &strg Self) ensures self: Self{mpu: enable(mpu.ctrl)})] fn enable_app_mpu(&mut self) { + // Enable the MPU, disable it during HardFault/NMI handlers, and allow // privileged code access to all unprotected memory. self.registers.ctrl.write( @@ -603,7 +625,8 @@ impl mpu::MPU for MPU { ); } - #[flux_rs::sig(fn(self: &strg Self) ensures self: Self{mpu: bv_and(mpu.ctrl, bv_int_to_bv32(0x00000001)) == bv_int_to_bv32(0) })] + // #[flux_rs::sig(fn(self: &strg Self) ensures self: Self{mpu: bv_and(mpu.ctrl, bv_int_to_bv32(0x00000001)) == bv_int_to_bv32(0) })] + #[flux_rs::sig(fn(self: &strg Self) ensures self: Self{mpu: !enable(mpu.ctrl)})] fn disable_app_mpu(&mut self) { // The MPU is not enabled for privileged mode, so we don't have to do // anything @@ -611,10 +634,10 @@ impl mpu::MPU for MPU { } fn number_total_regions(&self) -> usize { + self.registers.mpu_type.read(Type::DREGION()) as usize } - #[flux_rs::trusted] fn new_config(&self) -> Option { let id = self.config_count.get(); self.config_count.set(id.checked_add(1)?); @@ -625,6 +648,7 @@ impl mpu::MPU for MPU { id, regions: [CortexMRegion::empty(0); 8], is_dirty: Cell::new(true), + hw_state: HwGhostState::new(), // empty hw state }; self.reset_config(&mut ret); @@ -645,13 +669,23 @@ impl mpu::MPU for MPU { config.set_dirty(true); } + + // #[flux_rs::sig(fn( + // _, + // FluxPtrU8[@memstart], + // _, + // usize[@minsz], + // mpu::Permissions[@perms], + // config: &strg CortexMConfig[@c], + // ) -> Option{r: r => config_can_access(c, memstart, minsz, perms)} + // ensures config: CortexMConfig)] fn allocate_region( &self, unallocated_memory_start: FluxPtrU8, unallocated_memory_size: usize, min_region_size: usize, permissions: mpu::Permissions, - config: &mut Self::MpuConfig, + config: &mut CortexMConfig, ) -> Option { assume(min_region_size < 2147483648); @@ -777,10 +811,16 @@ impl mpu::MPU for MPU { Some(mpu::Region::new(start.as_fluxptr(), size)) } + // #[flux_rs::sig(fn( + // _, + // region: mpu::Region[@memstart, @memsz], + // config: &strg CortexMConfig[@c], + // ) -> Result<(), ()>{ r: r => !config_cant_access(c, memstart, memsz)} + // ensures config: CortexMConfig)] fn remove_memory_region( &self, region: mpu::Region, - config: &mut Self::MpuConfig, + config: &mut CortexMConfig, ) -> Result<(), ()> { let (idx, _r) = config .regions_iter() @@ -948,7 +988,7 @@ impl mpu::MPU for MPU { ) -> Result<(), ()> { // Get first region, or error if the process tried to update app memory // MPU region before it was created. - let (region_start_ptr, region_size) = config.region_get(0).location().ok_or(())?; + let (region_start_ptr, region_size) = config.get_region(0).location().ok_or(())?; let region_start = region_start_ptr.as_usize(); let app_memory_break = app_memory_break.as_usize(); @@ -1016,17 +1056,35 @@ impl mpu::MPU for MPU { Ok(()) } - #[flux_rs::sig(fn(self: &strg Self, &Self::MpuConfig) ensures self: Self)] - fn configure_mpu(&mut self, config: &Self::MpuConfig) { + // TODO: reimplement dirty tracking + // TODO: add for loop back in + #[flux_rs::sig(fn(self: &strg Self, &CortexMConfig[@config]) ensures self: Self{mpu: configured_for(mpu, config)})] + fn configure_mpu(&mut self, config: &CortexMConfig) { // If the hardware is already configured for this app and the app's MPU // configuration has not changed, then skip the hardware update. - if !self.hardware_is_configured_for.contains(&config.id()) || config.is_dirty() { + // if !self.hardware_is_configured_for.contains(&config.id()) || config.is_dirty() { // Set MPU regions - for region in config.regions_iter() { - self.commit_region(region); - } - self.hardware_is_configured_for.set(config.id()); - config.set_dirty(false); - } + self.commit_region(config.get_region(0)); + self.commit_region(config.get_region(1)); + self.commit_region(config.get_region(2)); + self.commit_region(config.get_region(3)); + self.commit_region(config.get_region(4)); + self.commit_region(config.get_region(5)); + self.commit_region(config.get_region(6)); + self.commit_region(config.get_region(7)); + // for region in config.regions_iter() { + // self.commit_region(region); + // } + // self.hardware_is_configured_for.set(config.id()); + // config.set_dirty(false); + // } } } + + +// TODO: simplify configured_for +// -- requires proving that beyond 8, everything is the same +// -- alternately, just requires a special macro +// TODO: better solution than trusted `get_region`? +// TODO: once there is support for double projections in specs, remove `value()` function +// -- alternately, dont refine CortexMRegion by FieldValue but just by bitvec? \ No newline at end of file diff --git a/flux.toml b/flux.toml new file mode 100644 index 0000000000..599e9fd8ae --- /dev/null +++ b/flux.toml @@ -0,0 +1 @@ +cache = true diff --git a/flux_support/src/extern_specs/mod.rs b/flux_support/src/extern_specs/mod.rs index dafb934425..74588505ba 100644 --- a/flux_support/src/extern_specs/mod.rs +++ b/flux_support/src/extern_specs/mod.rs @@ -4,3 +4,4 @@ mod non_null; mod num; mod option; mod slice; +mod result; diff --git a/flux_support/src/extern_specs/result.rs b/flux_support/src/extern_specs/result.rs new file mode 100644 index 0000000000..e688419629 --- /dev/null +++ b/flux_support/src/extern_specs/result.rs @@ -0,0 +1,19 @@ +/* +#[flux_rs::extern_spec] +#[flux_rs::refined_by(b: bool)] +enum Result { + #[variant({T} -> Result[true])] + Ok(T), + #[variant({E} -> Result[false])] + Err(E), +} + +#[flux_rs::extern_spec] +impl Result { + #[sig(fn(Self[@b]) -> bool[b])] + const fn is_ok(&self) -> bool; + + #[sig(fn(Self[@b]) -> bool[!b])] + const fn is_err(&self) -> bool; +} +*/ diff --git a/kernel/src/platform/mpu.rs b/kernel/src/platform/mpu.rs index b4b8310954..2ac0ec9641 100644 --- a/kernel/src/platform/mpu.rs +++ b/kernel/src/platform/mpu.rs @@ -4,7 +4,6 @@ //! Interface for configuring the Memory Protection Unit. -use core::cmp; use core::fmt::{self, Display}; #[allow(clippy::wildcard_imports)] use flux_support::*; @@ -29,15 +28,18 @@ pub enum Permissions { /// /// This is one contiguous address space protected by the MPU. #[derive(Copy, Clone, PartialEq, Eq)] +#[flux_rs::refined_by(ptr: int, sz: int)] pub struct Region { /// The memory address where the region starts. /// /// For maximum compatibility, we use a u8 pointer, however, note that many /// memory protection units have very strict alignment requirements for the /// memory regions protected by the MPU. + #[flux_rs::field(FluxPtrU8Mut[ptr])] start_address: FluxPtrU8Mut, /// The number of bytes of memory in the MPU region. + #[flux_rs::field(usize[sz])] size: usize, } @@ -86,13 +88,10 @@ impl Display for MpuConfigDefault { /// kernel when deciding where to place certain application memory regions so /// that the MPU can appropriately provide protection for those memory regions. -// VTOCK_TODO: can we hide `enabled`? // VTOCK-TODO: remove default associated refinements -// #[flux_rs::generics(Self as base)] #[flux_rs::assoc(fn enabled(self: Self) -> bool {false} )] -// VTOCK-TODO: add argument to `configured_for` for Self::MPUConfig once thats possible -#[flux_rs::assoc(fn configured_for(self: Self) -> bool {false} )] -#[flux_rs::assoc(fn can_access(self: Self, addr: int, sz: int, perms: Permissions) -> bool {false} )] +#[flux_rs::assoc(fn configured_for(self: Self, config: Self::MpuConfig) -> bool {false} )] +// #[flux_rs::assoc(fn can_access(self: Self, addr: int, sz: int, perms: Permissions) -> bool {false} )] pub trait MPU { /// MPU-specific state that defines a particular configuration for the MPU. /// That is, this should contain all of the required state such that the @@ -123,6 +122,7 @@ pub trait MPU { /// platforms the MPU rules apply to privileged code as well, and therefore /// some of the MPU configuration must be disabled for the kernel to effectively /// manage processes. + // #[flux_rs::sig(fn(self: &strg Self) ensures self: Self{r: !::enabled(r)})] fn disable_app_mpu(&mut self); /// Returns the maximum number of regions supported by the MPU. @@ -275,84 +275,85 @@ pub trait MPU { /// # Arguments /// /// - `config`: MPU region configuration + // #[flux_rs::sig(fn(self: &strg Self, &Self::MpuConfig[@config]) ensures self: Self{r: ::configured_for(r, config)})] fn configure_mpu(&mut self, config: &Self::MpuConfig); } -/// Implement default MPU trait for unit. -impl MPU for () { - type MpuConfig = MpuConfigDefault; - - fn enable_app_mpu(&mut self) {} - - fn disable_app_mpu(&mut self) {} - - fn number_total_regions(&self) -> usize { - 0 - } - - fn new_config(&self) -> Option { - Some(MpuConfigDefault) - } - - fn reset_config(&self, _config: &mut Self::MpuConfig) {} - - fn allocate_region( - &self, - unallocated_memory_start: FluxPtrU8Mut, - unallocated_memory_size: usize, - min_region_size: usize, - _permissions: Permissions, - _config: &mut Self::MpuConfig, - ) -> Option { - if min_region_size > unallocated_memory_size { - None - } else { - Some(Region::new(unallocated_memory_start, min_region_size)) - } - } - - fn remove_memory_region( - &self, - _region: Region, - _config: &mut Self::MpuConfig, - ) -> Result<(), ()> { - Ok(()) - } - - fn allocate_app_memory_region( - &self, - unallocated_memory_start: FluxPtrU8Mut, - unallocated_memory_size: usize, - min_memory_size: usize, - initial_app_memory_size: usize, - initial_kernel_memory_size: usize, - _permissions: Permissions, - _config: &mut Self::MpuConfig, - ) -> Option<(FluxPtrU8Mut, usize)> { - let memory_size = cmp::max( - min_memory_size, - initial_app_memory_size + initial_kernel_memory_size, - ); - if memory_size > unallocated_memory_size { - None - } else { - Some((unallocated_memory_start, memory_size)) - } - } - - fn update_app_memory_region( - &self, - app_memory_break: FluxPtrU8Mut, - kernel_memory_break: FluxPtrU8Mut, - _permissions: Permissions, - _config: &mut Self::MpuConfig, - ) -> Result<(), ()> { - if (app_memory_break.as_usize()) > (kernel_memory_break.as_usize()) { - Err(()) - } else { - Ok(()) - } - } - - fn configure_mpu(&mut self, _config: &Self::MpuConfig) {} -} +// /// Implement default MPU trait for unit. +// impl MPU for () { +// type MpuConfig = MpuConfigDefault; + +// fn enable_app_mpu(&mut self) {} + +// fn disable_app_mpu(&mut self) {} + +// fn number_total_regions(&self) -> usize { +// 0 +// } + +// fn new_config(&self) -> Option { +// Some(MpuConfigDefault) +// } + +// fn reset_config(&self, _config: &mut Self::MpuConfig) {} + +// fn allocate_region( +// &self, +// unallocated_memory_start: FluxPtrU8Mut, +// unallocated_memory_size: usize, +// min_region_size: usize, +// _permissions: Permissions, +// _config: &mut Self::MpuConfig, +// ) -> Option { +// if min_region_size > unallocated_memory_size { +// None +// } else { +// Some(Region::new(unallocated_memory_start, min_region_size)) +// } +// } + +// fn remove_memory_region( +// &self, +// _region: Region, +// _config: &mut Self::MpuConfig, +// ) -> Result<(), ()> { +// Ok(()) +// } + +// fn allocate_app_memory_region( +// &self, +// unallocated_memory_start: FluxPtrU8Mut, +// unallocated_memory_size: usize, +// min_memory_size: usize, +// initial_app_memory_size: usize, +// initial_kernel_memory_size: usize, +// _permissions: Permissions, +// _config: &mut Self::MpuConfig, +// ) -> Option<(FluxPtrU8Mut, usize)> { +// let memory_size = cmp::max( +// min_memory_size, +// initial_app_memory_size + initial_kernel_memory_size, +// ); +// if memory_size > unallocated_memory_size { +// None +// } else { +// Some((unallocated_memory_start, memory_size)) +// } +// } + +// fn update_app_memory_region( +// &self, +// app_memory_break: FluxPtrU8Mut, +// kernel_memory_break: FluxPtrU8Mut, +// _permissions: Permissions, +// _config: &mut Self::MpuConfig, +// ) -> Result<(), ()> { +// if (app_memory_break.as_usize()) > (kernel_memory_break.as_usize()) { +// Err(()) +// } else { +// Ok(()) +// } +// } + +// fn configure_mpu(&mut self, _config: &Self::MpuConfig) {} +// }