Skip to content

Commit df69be5

Browse files
author
Evan Johnson
committed
some very messy hacking on cortexm mpu
1 parent e673dac commit df69be5

File tree

1 file changed

+106
-38
lines changed

1 file changed

+106
-38
lines changed

‎arch/cortex-m/src/mpu.rs‎

Lines changed: 106 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#![allow(unused)]
12
// Licensed under the Apache License, Version 2.0 or the MIT License.
23
// SPDX-License-Identifier: Apache-2.0 OR MIT
34
// Copyright Tock Contributors 2022.
@@ -29,12 +30,6 @@
2930

3031
// )]
3132

32-
// VTOCK_TODO: better solution for hardware register spooky-action-at-a-distance
33-
/* VTOCK TODOS
34-
1. Implement configured_for
35-
2. Implement can_service
36-
*/
37-
3833
use core::cell::Cell;
3934
use core::cmp;
4035
use core::fmt;
@@ -46,6 +41,8 @@ use kernel::platform::mpu;
4641
use kernel::utilities::cells::OptionalCell;
4742
use kernel::utilities::math;
4843

44+
// VTOCK-TODO: NUM_REGIONS currently fixed to 8. Need to also handle 16
45+
4946
flux_rs::defs! {
5047
fn bv32(x:int) -> bitvec<32> { bv_int_to_bv32(x) }
5148
fn bit(reg: bitvec<32>, power_of_two:int) -> bool { bv_bv32_to_int(bv_and(reg, bv32(power_of_two))) != 0}
@@ -86,8 +83,43 @@ flux_rs::defs! {
8683
// }
8784
// }
8885

86+
87+
fn enabled(mpu: MPU) -> bool { enable(mpu.ctrl)}
88+
// VTOCK_TODO: simplify
89+
fn configured_for(mpu: MPU, config: CortexMConfig) -> bool {
90+
map_get(mpu.regions, 0) == map_get(config.regions, 0) &&
91+
map_get(mpu.attrs, 0) == map_get(config.attrs, 0) &&
92+
map_get(mpu.regions, 1) == map_get(config.regions, 1) &&
93+
map_get(mpu.attrs, 1) == map_get(config.attrs, 1) &&
94+
map_get(mpu.regions, 2) == map_get(config.regions, 2) &&
95+
map_get(mpu.attrs, 2) == map_get(config.attrs, 2) &&
96+
map_get(mpu.regions, 3) == map_get(config.regions, 3) &&
97+
map_get(mpu.attrs, 3) == map_get(config.attrs, 3) &&
98+
map_get(mpu.regions, 4) == map_get(config.regions, 4) &&
99+
map_get(mpu.attrs, 4) == map_get(config.attrs, 4) &&
100+
map_get(mpu.regions, 5) == map_get(config.regions, 5) &&
101+
map_get(mpu.attrs, 5) == map_get(config.attrs, 5) &&
102+
map_get(mpu.regions, 6) == map_get(config.regions, 6) &&
103+
map_get(mpu.attrs, 6) == map_get(config.attrs, 6) &&
104+
map_get(mpu.regions, 7) == map_get(config.regions, 7) &&
105+
map_get(mpu.attrs, 7) == map_get(config.attrs, 7)
106+
}
107+
// fn user_can_access(mpu: Mpu, addr: int, sz: int, perms: mpu::Permissions) -> {
108+
// }
109+
// fn contains(raddr: int, rsize: int, addr: int, size: int) -> bool {
110+
// ((addr >= raddr) && (addr + size < raddr + rsize))
111+
// }
112+
113+
89114
}
90115

116+
// VTOCK_TODO: better solution for hardware register spooky-action-at-a-distance
117+
/* VTOCK TODOS
118+
1. enabled
119+
2. Implement configured_for
120+
3. Implement can_service
121+
*/
122+
91123
// VTOCK-TODO: supplementary proof?
92124
#[flux_rs::sig(fn(n: u32{n < 32}) -> usize {r: r > 0 })]
93125
#[flux_rs::trusted]
@@ -296,6 +328,8 @@ impl<const MIN_REGION_SIZE: usize> MPU<MIN_REGION_SIZE> {
296328
297329
const NUM_REGIONS: usize = 8;
298330

331+
#[flux_rs::opaque]
332+
#[flux_rs::refined_by(dirty: bool, regions: Map<int, int>, attrs: Map<int, int>)]
299333
pub struct CortexMConfig {
300334
/// Unique ID for this configuration, assigned from a
301335
/// monotonically increasing counter in the MPU struct.
@@ -316,7 +350,7 @@ const APP_MEMORY_REGION_MAX_NUM: usize = 1;
316350
impl fmt::Display for CortexMConfig {
317351
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
318352
write!(f, "\r\n Cortex-M MPU")?;
319-
for (i, region) in self.regions.iter().enumerate() {
353+
for (i, region) in self.regions_iter().enumerate() {
320354
if let Some(location) = region.location() {
321355
let access_bits = region.attributes().read(RegionAttributes::AP());
322356
let start = location.0.as_usize();
@@ -357,10 +391,44 @@ impl fmt::Display for CortexMConfig {
357391
}
358392

359393
impl CortexMConfig {
394+
#[flux_rs::trusted]
395+
fn id(&self) -> NonZeroUsize {
396+
self.id
397+
}
398+
399+
#[flux_rs::trusted]
400+
fn is_dirty(&self) -> bool {
401+
self.is_dirty.get()
402+
}
403+
404+
#[flux_rs::trusted]
405+
fn set_dirty(&self, b: bool) {
406+
self.is_dirty.set(b)
407+
}
408+
409+
#[flux_rs::trusted]
410+
// #[flux_rs::sig(fn(self: &Self, idx: usize, region: CortexMRegion))]
411+
// map_get
412+
fn region_get(&self, idx: usize) -> &CortexMRegion {
413+
&self.regions[idx]
414+
}
415+
416+
#[flux_rs::trusted]
417+
// map_set
418+
// #[flux_rs::sig(fn(self: &strg Self[@dirty, @regions, @attrs], idx: usize, region: CortexMRegion) ensures self: Self[dirty, map_set(regions, idx, region.addr), map_set(attrs, idx, region.attrs)])]
419+
fn region_set(&mut self, idx: usize, region: CortexMRegion) {
420+
self.regions[idx] = region
421+
}
422+
423+
#[flux_rs::trusted]
424+
fn regions_iter(&self) -> core::slice::Iter<'_, CortexMRegion> {
425+
self.regions.iter()
426+
}
427+
360428
#[flux_rs::trusted] // need spec for enumerate for this to work
361429
#[flux_rs::sig(fn(&CortexMConfig) -> Option<usize{r: r > 1 && r < 8}>)]
362430
fn unused_region_number(&self) -> Option<usize> {
363-
for (number, region) in self.regions.iter().enumerate() {
431+
for (number, region) in self.regions_iter().enumerate() {
364432
if number <= APP_MEMORY_REGION_MAX_NUM {
365433
continue;
366434
}
@@ -543,6 +611,7 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
543611
self.registers.mpu_type.read(Type::DREGION()) as usize
544612
}
545613

614+
#[flux_rs::trusted]
546615
fn new_config(&self) -> Option<Self::MpuConfig> {
547616
let id = self.config_count.get();
548617
self.config_count.set(id.checked_add(1)?);
@@ -551,7 +620,7 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
551620
// write the properly-indexed `CortexMRegion`s:
552621
let mut ret = CortexMConfig {
553622
id,
554-
regions: [CortexMRegion::empty(0); NUM_REGIONS],
623+
regions: [CortexMRegion::empty(0); 8],
555624
is_dirty: Cell::new(true),
556625
};
557626

@@ -561,16 +630,16 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
561630
}
562631

563632
fn reset_config(&self, config: &mut Self::MpuConfig) {
564-
config.regions[0] = CortexMRegion::empty(0);
565-
config.regions[1] = CortexMRegion::empty(1);
566-
config.regions[2] = CortexMRegion::empty(2);
567-
config.regions[3] = CortexMRegion::empty(3);
568-
config.regions[4] = CortexMRegion::empty(4);
569-
config.regions[5] = CortexMRegion::empty(5);
570-
config.regions[6] = CortexMRegion::empty(6);
571-
config.regions[7] = CortexMRegion::empty(7);
572-
573-
config.is_dirty.set(true);
633+
config.region_set(0, CortexMRegion::empty(0));
634+
config.region_set(1, CortexMRegion::empty(1));
635+
config.region_set(2, CortexMRegion::empty(2));
636+
config.region_set(3, CortexMRegion::empty(3));
637+
config.region_set(4, CortexMRegion::empty(4));
638+
config.region_set(5, CortexMRegion::empty(5));
639+
config.region_set(6, CortexMRegion::empty(6));
640+
config.region_set(7, CortexMRegion::empty(7));
641+
642+
config.set_dirty(true);
574643
}
575644

576645
fn allocate_region(
@@ -584,7 +653,7 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
584653
assume(min_region_size < 2147483648);
585654

586655
// Check that no previously allocated regions overlap the unallocated memory.
587-
for region in config.regions.iter() {
656+
for region in config.regions_iter() {
588657
if region.overlaps(unallocated_memory_start, unallocated_memory_size) {
589658
return None;
590659
}
@@ -699,8 +768,8 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
699768
permissions,
700769
);
701770

702-
config.regions[region_num] = region;
703-
config.is_dirty.set(true);
771+
config.region_set(region_num, region);
772+
config.set_dirty(true);
704773

705774
Some(mpu::Region::new(start.as_fluxptr(), size))
706775
}
@@ -711,8 +780,7 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
711780
config: &mut Self::MpuConfig,
712781
) -> Result<(), ()> {
713782
let (idx, _r) = config
714-
.regions
715-
.iter()
783+
.regions_iter()
716784
.enumerate()
717785
.find(|(_idx, r)| **r == region)
718786
.ok_or(())?;
@@ -722,8 +790,8 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
722790
}
723791
assume(idx < 8); // need spec for find
724792

725-
config.regions[idx] = CortexMRegion::empty(idx);
726-
config.is_dirty.set(true);
793+
config.region_set(idx, CortexMRegion::empty(idx));
794+
config.set_dirty(true);
727795

728796
Ok(())
729797
}
@@ -743,7 +811,7 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
743811
) -> Option<(FluxPtrU8, usize)> {
744812
// Check that no previously allocated regions overlap the unallocated
745813
// memory.
746-
for region in config.regions.iter() {
814+
for region in config.regions_iter() {
747815
if region.overlaps(unallocated_memory_start, unallocated_memory_size) {
748816
return None;
749817
}
@@ -861,9 +929,9 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
861929
)
862930
};
863931

864-
config.regions[0] = region0;
865-
config.regions[1] = region1;
866-
config.is_dirty.set(true);
932+
config.region_set(0, region0);
933+
config.region_set(1, region1);
934+
config.set_dirty(true);
867935

868936
Some((region_start.as_fluxptr(), memory_size_po2))
869937
}
@@ -877,7 +945,7 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
877945
) -> Result<(), ()> {
878946
// Get first region, or error if the process tried to update app memory
879947
// MPU region before it was created.
880-
let (region_start_ptr, region_size) = config.regions[0].location().ok_or(())?;
948+
let (region_start_ptr, region_size) = config.region_get(0).location().ok_or(())?;
881949
let region_start = region_start_ptr.as_usize();
882950

883951
let app_memory_break = app_memory_break.as_usize();
@@ -938,9 +1006,9 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
9381006
)
9391007
};
9401008

941-
config.regions[0] = region0;
942-
config.regions[1] = region1;
943-
config.is_dirty.set(true);
1009+
config.region_set(0, region0);
1010+
config.region_set(1, region1);
1011+
config.set_dirty(true);
9441012

9451013
Ok(())
9461014
}
@@ -949,13 +1017,13 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
9491017
fn configure_mpu(&mut self, config: &Self::MpuConfig) {
9501018
// If the hardware is already configured for this app and the app's MPU
9511019
// configuration has not changed, then skip the hardware update.
952-
if !self.hardware_is_configured_for.contains(&config.id) || config.is_dirty.get() {
1020+
if !self.hardware_is_configured_for.contains(&config.id()) || config.is_dirty() {
9531021
// Set MPU regions
954-
for region in config.regions.iter() {
1022+
for region in config.regions_iter() {
9551023
self.commit_region(region);
9561024
}
957-
self.hardware_is_configured_for.set(config.id);
958-
config.is_dirty.set(false);
1025+
self.hardware_is_configured_for.set(config.id());
1026+
config.set_dirty(false);
9591027
}
9601028
}
9611029
}

0 commit comments

Comments
 (0)