Skip to content

Commit 0da7716

Browse files
vrindisbachervrindisbacher
committed
convert kernel protection
1 parent d76e2a8 commit 0da7716

1 file changed

Lines changed: 157 additions & 76 deletions

File tree

‎arch/rv32i/src/pmp.rs‎

Lines changed: 157 additions & 76 deletions
Original file line numberDiff line numberDiff line change
@@ -148,8 +148,7 @@ flux_rs::defs! {
148148
fn region_configured_correctly(region: PMPUserRegion, hardware_state: HardwareState, idx: int) -> bool {
149149
let cfg_reg_idx = idx / 2;
150150
let cfg_reg = map_select(hardware_state.pmpcfg_registers, cfg_reg_idx);
151-
cfg_reg_configured_correctly(cfg_reg, region, idx)
152-
&& addr_reg_configured_correctly(hardware_state.pmpaddr_registers, region, idx)
151+
cfg_reg_configured_correctly(cfg_reg, region, idx) && addr_reg_configured_correctly(hardware_state.pmpaddr_registers, region, idx)
153152
}
154153

155154
// uninterpreted since we don't have forall:
@@ -1816,11 +1815,12 @@ pub mod simple {
18161815
pub mod kernel_protection {
18171816
use flux_support::LocalRegisterCopyU8;
18181817
use super::{
1819-
pmpcfg_octet, NAPOTRegionSpec, PMPUserRegion, TORRegionSpec, TORUserPMP, TORUserPMPCFG, HardwareState
1818+
pmpcfg_octet, NAPOTRegionSpec, PMPUserRegion, TORRegionSpec, TORUserPMP, TORUserPMPCFG, HardwareState,
1819+
all_regions_configured_correctly_base, all_regions_configured_correctly_step, u32_from_be_bytes
18201820
};
18211821
use crate::csr;
18221822
use core::fmt;
1823-
use flux_support::FluxPtrU8;
1823+
use flux_support::{FluxPtr, FieldValueU32};
18241824
use kernel::utilities::registers::FieldValue;
18251825

18261826
// ---------- Kernel memory-protection PMP memory region wrapper types -----
@@ -2095,90 +2095,171 @@ pub mod kernel_protection {
20952095
#[flux_rs::sig(fn (&Self, &[PMPUserRegion; _], hw_state: &strg HardwareState) -> Result<(), ()>[#ok] ensures hw_state: HardwareState {hw:
20962096
ok => all_regions_configured_correctly_up_to(MPU_REGIONS)
20972097
})]
2098-
#[flux_rs::trusted]
20992098
fn configure_pmp(&self, regions: &[PMPUserRegion; MPU_REGIONS], hardware_state: &mut HardwareState) -> Result<(), ()> {
2100-
// Could use `iter_array_chunks` once that's stable.
2101-
let mut regions_iter = regions.iter();
2102-
let mut i = 0;
2103-
2104-
while let Some(even_region) = regions_iter.next() {
2105-
let odd_region_opt = regions_iter.next();
2106-
let even_region_start = even_region.start.unwrap_or(FluxPtrU8::null());
2107-
let even_region_end = even_region.end.unwrap_or(FluxPtrU8::null());
2108-
2109-
if let Some(odd_region) = odd_region_opt {
2110-
let odd_region_start = odd_region.start.unwrap_or(FluxPtrU8::null());
2111-
let odd_region_end = odd_region.end.unwrap_or(FluxPtrU8::null());
2112-
// We can configure two regions at once which, given that we
2113-
// start at index 0 (an even offset), translates to a single
2114-
// CSR write for the pmpcfgX register:
2115-
csr::CSR.pmpconfig_set(
2116-
i / 2,
2117-
u32::from_be_bytes([
2118-
odd_region.tor.get(),
2119-
TORUserPMPCFG::OFF().get(),
2120-
even_region.tor.get(),
2121-
TORUserPMPCFG::OFF().get(),
2122-
]) as usize,
2099+
2100+
// configures region `i` and region `i + 1` correctly
2101+
#[flux_rs::sig(fn (i: usize, &PMPUserRegion[@er], &PMPUserRegion[@or], hw_state: &strg HardwareState[@og_hw])
2102+
// Note: these pre and post conditions (all_regions_configured) seem silly
2103+
// but we need them because otherwise Flux forgets
2104+
// all state after we return
2105+
requires
2106+
all_regions_configured_correctly_up_to(i) &&
2107+
i % 2 == 0
2108+
ensures hw_state: HardwareState{new_hw:
2109+
region_configured_correctly(er, new_hw, i) && region_configured_correctly(or, new_hw, i + 1)
2110+
&& all_regions_configured_correctly_up_to(i)
2111+
}
2112+
)]
2113+
fn configure_region_pair(i: usize, even_region: &PMPUserRegion, odd_region: &PMPUserRegion, hardware_state: &mut HardwareState) {
2114+
let even_region_start = match even_region.start {
2115+
Some(r) => r,
2116+
None => FluxPtr::null()
2117+
};
2118+
let even_region_end = match even_region.end {
2119+
Some(r) => r,
2120+
None => FluxPtr::null()
2121+
};
2122+
let odd_region_start = match odd_region.start {
2123+
Some(r) => r,
2124+
None => FluxPtr::null()
2125+
};
2126+
let odd_region_end = match odd_region.end {
2127+
Some(r) => r,
2128+
None => FluxPtr::null()
2129+
};
2130+
2131+
// We can configure two regions at once which, given that we
2132+
// start at index 0 (an even offset), translates to a single
2133+
// CSR write for the pmpcfgX register:
2134+
super::pmpconfig_set(i / 2,
2135+
u32_from_be_bytes(
2136+
odd_region.tor.get(),
2137+
TORUserPMPCFG::OFF().get(),
2138+
even_region.tor.get(),
2139+
TORUserPMPCFG::OFF().get(),
2140+
) as usize,
2141+
hardware_state
2142+
);
2143+
2144+
// Now, set the addresses of the respective regions, if they
2145+
// are enabled, respectively:
2146+
if even_region.tor != TORUserPMPCFG::OFF() {
2147+
super::pmpaddr_set(
2148+
i * 2 + 0,
2149+
super::overflowing_shr(even_region_start.as_usize(), 2),
2150+
hardware_state
21232151
);
21242152

2125-
// Now, set the addresses of the respective regions, if they
2126-
// are enabled, respectively:
2127-
if even_region.tor != TORUserPMPCFG::OFF() {
2128-
csr::CSR.pmpaddr_set(
2129-
i * 2 + 0,
2130-
(even_region_start.as_usize()).overflowing_shr(2).0,
2131-
);
2132-
csr::CSR.pmpaddr_set(
2133-
i * 2 + 1,
2134-
(even_region_start.as_usize()).overflowing_shr(2).0,
2135-
);
2136-
}
2153+
super::pmpaddr_set(
2154+
i * 2 + 1,
2155+
super::overflowing_shr(even_region_end.as_usize(), 2),
2156+
hardware_state
2157+
);
2158+
}
21372159

2138-
if odd_region.tor != TORUserPMPCFG::OFF() {
2139-
csr::CSR.pmpaddr_set(
2140-
i * 2 + 2,
2141-
(odd_region_start.as_usize()).overflowing_shr(2).0,
2142-
);
2143-
csr::CSR.pmpaddr_set(
2144-
i * 2 + 3,
2145-
(odd_region_end.as_usize()).overflowing_shr(2).0,
2146-
);
2147-
}
2160+
if odd_region.tor != TORUserPMPCFG::OFF() {
2161+
super::pmpaddr_set(
2162+
i * 2 + 2,
2163+
super::overflowing_shr(odd_region_start.as_usize(), 2),
2164+
hardware_state
2165+
);
2166+
super::pmpaddr_set(
2167+
i * 2 + 3,
2168+
super::overflowing_shr(odd_region_end.as_usize(), 2),
2169+
hardware_state
2170+
);
2171+
}
2172+
}
21482173

2149-
i += 2;
2150-
} else {
2151-
// Modify the first two pmpcfgX octets for this region:
2152-
csr::CSR.pmpconfig_modify(
2153-
i / 2,
2154-
FieldValue::<usize, csr::pmpconfig::pmpcfg::Register>::new(
2155-
0x0000FFFF,
2174+
// configures region `i` correctly
2175+
#[flux_rs::sig(fn (i: usize, &PMPUserRegion[@er], hw_state: &strg HardwareState[@og_hw])
2176+
// Note: these pre and post conditions (all_regions_configured) seem silly
2177+
// but we need them because otherwise Flux forgets
2178+
// all state after we return
2179+
requires all_regions_configured_correctly_up_to(i) && i % 2 == 0
2180+
ensures hw_state: HardwareState{new_hw:
2181+
region_configured_correctly(er, new_hw, i) && all_regions_configured_correctly_up_to(i)
2182+
}
2183+
)]
2184+
fn configure_region(i: usize, even_region: &PMPUserRegion, hardware_state: &mut HardwareState) {
2185+
let even_region_start = match even_region.start {
2186+
Some(r) => r,
2187+
None => FluxPtr::null()
2188+
};
2189+
let even_region_end = match even_region.end {
2190+
Some(r) => r,
2191+
None => FluxPtr::null()
2192+
};
2193+
2194+
// TODO: check overhead of code
2195+
// Modify the first two pmpcfgX octets for this region:
2196+
let bits = FieldValueU32::<csr::pmpconfig::pmpcfg::Register>::new(
2197+
0x0000FFFF,
2198+
0,
2199+
u32_from_be_bytes(
21562200
0,
2157-
u32::from_be_bytes([
2158-
0,
2159-
0,
2160-
even_region.tor.get(),
2161-
TORUserPMPCFG::OFF().get(),
2162-
]) as usize,
2163-
),
2201+
0,
2202+
even_region.tor.get(),
2203+
TORUserPMPCFG::OFF().get()
2204+
)
21642205
);
21652206

2166-
// Set the addresses if the region is enabled:
2167-
if even_region.tor != TORUserPMPCFG::OFF() {
2168-
csr::CSR.pmpaddr_set(
2169-
i * 2 + 0,
2170-
(even_region_start.as_usize()).overflowing_shr(2).0,
2171-
);
2172-
csr::CSR.pmpaddr_set(
2173-
i * 2 + 1,
2174-
(even_region_end.as_usize()).overflowing_shr(2).0,
2175-
);
2176-
}
2207+
super::pmpconfig_modify(i / 2, bits, hardware_state);
21772208

2178-
i += 1;
2209+
// Set the addresses if the region is enabled:
2210+
if even_region.tor != TORUserPMPCFG::OFF() {
2211+
super::pmpaddr_set(
2212+
i * 2 + 0,
2213+
super::overflowing_shr(even_region_start.as_usize(), 2),
2214+
hardware_state
2215+
);
2216+
super::pmpaddr_set(
2217+
i * 2 + 1,
2218+
super::overflowing_shr(even_region_end.as_usize(), 2),
2219+
hardware_state
2220+
);
21792221
}
21802222
}
21812223

2224+
#[flux_rs::sig(
2225+
fn (i: usize, core::slice::Iter<PMPUserRegion>[@idx, @len], max_regions: usize, hw_state: &strg HardwareState[@og_hw])
2226+
requires
2227+
all_regions_configured_correctly_up_to(i)
2228+
&& len == max_regions
2229+
&& (idx < len => i == idx && i % 2 == 0)
2230+
&& (idx >= len => all_regions_configured_correctly_up_to(max_regions))
2231+
2232+
ensures hw_state: HardwareState{new_hw: all_regions_configured_correctly_up_to(max_regions)}
2233+
)]
2234+
fn configure_all_regions_tail(i: usize, mut regions_iter: core::slice::Iter<'_, PMPUserRegion>, max_regions: usize, hardware_state: &mut HardwareState) {
2235+
if let Some(even_region) = regions_iter.next() {
2236+
let odd_region_opt = regions_iter.next();
2237+
2238+
match odd_region_opt {
2239+
None => {
2240+
configure_region(i, even_region, hardware_state);
2241+
all_regions_configured_correctly_step(even_region, hardware_state, i);
2242+
configure_all_regions_tail(i + 1, regions_iter, max_regions, hardware_state);
2243+
}
2244+
Some(odd_region) => {
2245+
configure_region_pair(i, even_region, odd_region, hardware_state);
2246+
all_regions_configured_correctly_step(even_region, hardware_state, i);
2247+
all_regions_configured_correctly_step(odd_region, hardware_state, i + 1);
2248+
configure_all_regions_tail(i + 2, regions_iter, max_regions, hardware_state);
2249+
}
2250+
}
2251+
}
2252+
}
2253+
2254+
// this should be an invariant but it's on a trait so things are weird
2255+
if regions.len() == 0 {
2256+
return Err(());
2257+
}
2258+
let regions_iter = regions.iter();
2259+
// call lemma to establish the original precondition
2260+
all_regions_configured_correctly_base(hardware_state);
2261+
configure_all_regions_tail(0, regions_iter, MPU_REGIONS, hardware_state);
2262+
21822263
Ok(())
21832264
}
21842265

0 commit comments

Comments
 (0)