Skip to content

Commit 9cfa2d8

Browse files
vrindisbachervrindisbacher
committed
Checkin
1 parent e21c27c commit 9cfa2d8

2 files changed

Lines changed: 180 additions & 78 deletions

File tree

‎arch/rv32i/Cargo.toml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ authors.workspace = true
99
edition.workspace = true
1010

1111
[dependencies]
12+
flux-core = { git = "https://github.com/flux-rs/flux.git"}
1213
kernel = { path = "../../kernel" }
1314
flux_support = { path = "../../flux_support" }
1415
tock-registers = { path = "../../libraries/tock-register-interface" }

‎arch/rv32i/src/pmp.rs‎

Lines changed: 179 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
// Copyright Tock Contributors 2022.
44

5+
extern crate flux_core;
6+
57
use core::cell::Cell;
68
use core::fmt;
79
use core::num::NonZeroUsize;
@@ -95,9 +97,44 @@ flux_rs::defs! {
9597
extract(cfg.reg.val, 0b11000, 3) == 0
9698
}
9799

100+
fn region_configured_correctly(hardware_state: HardwareState, idx: int) -> bool {
101+
true
102+
}
98103

104+
// uninterpreted since we don't have forall:
105+
// forall i. i >= 0 && i < bound, region_configured_correctly(hardware_state, i)
106+
fn all_regions_configured_correctly_up_to(hardware_state: HardwareState, bound: int) -> bool;
99107
}
100108

109+
// Some axioms and verification state
110+
//
111+
// We want to prove that all regions up to a const generic are configured
112+
// correctly but we don't have a forall.
113+
//
114+
// So instead, we do the classic inductive evidence trick
115+
116+
#[flux_rs::opaque]
117+
#[flux_rs::refined_by(pmpcfg_registers: Map<int, bitvec<32>>, pmpaddr_registers: Map<int, bitvec<32>>)]
118+
pub struct HardwareState {}
119+
120+
#[flux_rs::trusted]
121+
impl HardwareState {
122+
pub fn new() -> Self {
123+
Self {}
124+
}
125+
}
126+
127+
#[flux_rs::trusted]
128+
#[flux_rs::sig(fn (&HardwareState[@hw]) ensures all_regions_configured_correctly_up_to(hw, 0))]
129+
fn all_regions_configured_correctly_base(hardware_state: &HardwareState) {}
130+
131+
#[flux_rs::trusted]
132+
#[flux_rs::sig(fn (&HardwareState[@hw], i: usize)
133+
requires all_regions_configured_correctly_up_to(hw, i) && region_configured_correctly(hw, i)
134+
ensures all_regions_configured_correctly_up_to(hw, i + 1)
135+
)]
136+
fn all_regions_configured_correctly_step(hardware_state: &HardwareState, i: usize) {}
137+
101138
register_bitfields_u8![u8,
102139
/// Generic `pmpcfg` octet.
103140
///
@@ -571,7 +608,10 @@ pub trait TORUserPMP<const MAX_REGIONS: usize> {
571608
/// To disable a region, set its configuration to [`TORUserPMPCFG::OFF`]. In
572609
/// this case, the start and end addresses are ignored and can be set to
573610
/// arbitrary values.
574-
fn configure_pmp(&self, regions: &[PMPUserRegion; MAX_REGIONS]) -> Result<(), ()>;
611+
#[flux_rs::sig(fn (&Self, &[PMPUserRegion; _], hw_state: &strg HardwareState) -> Result<(), ()>[#ok] ensures hw_state: HardwareState {hw:
612+
ok => all_regions_configured_correctly_up_to(hw, MAX_REGIONS)
613+
})]
614+
fn configure_pmp(&self, regions: &[PMPUserRegion; MAX_REGIONS], hardware_state: &mut HardwareState) -> Result<(), ()>;
575615

576616
/// Enable the user-mode memory protection.
577617
///
@@ -1098,7 +1138,8 @@ impl<const MAX_REGIONS: usize, P: TORUserPMP<MAX_REGIONS> + 'static> kernel::pla
10981138
ac_config[i] = <Self::Region as mpu::RegionDescriptor>::default(i);
10991139
}
11001140
}
1101-
self.pmp.configure_pmp(&ac_config).unwrap();
1141+
let mut hw = HardwareState::new();
1142+
self.pmp.configure_pmp(&ac_config, &mut hw).unwrap();
11021143
}
11031144
}
11041145

@@ -1119,7 +1160,7 @@ pub mod test {
11191160
MPU_REGIONS
11201161
}
11211162

1122-
fn configure_pmp(&self, _regions: &[PMPUserRegion]) -> Result<(), ()> {
1163+
fn configure_pmp(&self, _regions: &[PMPUserRegion], hardware_state: &mut HardwareState) -> Result<(), ()> {
11231164
Ok(())
11241165
}
11251166

@@ -1348,8 +1389,8 @@ pub mod test {
13481389

13491390
pub mod simple {
13501391
use flux_support::LocalRegisterCopyU8;
1351-
use super::{pmpcfg_octet, PMPUserRegion, TORUserPMP, TORUserPMPCFG};
1352-
use crate::csr;
1392+
use super::{pmpcfg_octet, PMPUserRegion, TORUserPMP, TORUserPMPCFG, HardwareState};
1393+
use crate::{csr, pmp::{all_regions_configured_correctly_base, all_regions_configured_correctly_step}};
13531394
use core::fmt;
13541395
use flux_support::FluxPtr;
13551396
use kernel::utilities::registers::FieldValue;
@@ -1448,89 +1489,141 @@ pub mod simple {
14481489
// `u32::from_be_bytes` and then cast to usize, as it manages to compile
14491490
// on 64-bit systems as well. However, this implementation will not work
14501491
// on RV64I systems, due to the changed pmpcfgX CSR layout.
1451-
fn configure_pmp(&self, regions: &[PMPUserRegion; MPU_REGIONS]) -> Result<(), ()> {
1452-
// Could use `iter_array_chunks` once that's stable.
1453-
let mut regions_iter = regions.iter();
1454-
let mut i = 0;
1492+
#[flux_rs::sig(fn (&Self, &[PMPUserRegion; _], hw_state: &strg HardwareState) -> Result<(), ()>[#ok] ensures hw_state: HardwareState {hw:
1493+
ok => all_regions_configured_correctly_up_to(hw, MPU_REGIONS)
1494+
})]
1495+
fn configure_pmp(&self, regions: &[PMPUserRegion; MPU_REGIONS], hardware_state: &mut HardwareState) -> Result<(), ()> {
1496+
1497+
// configures region `i` and region `i + 1` correctly
1498+
#[flux_rs::trusted]
1499+
#[flux_rs::sig(fn (i: usize, &PMPUserRegion[@er], &PMPUserRegion[@or], hw_state: &strg HardwareState[@og_hw])
1500+
requires all_regions_configured_correctly_up_to(og_hw, i)
1501+
ensures hw_state: HardwareState{new_hw:
1502+
region_configured_correctly(new_hw, i) && region_configured_correctly(new_hw, i + 1) && all_regions_configured_correctly_up_to(new_hw, i)
1503+
}
1504+
)]
1505+
fn configure_region_pair(i: usize, even_region: &PMPUserRegion, odd_region: &PMPUserRegion, hardware_state: &mut HardwareState) {
1506+
let even_region_start = even_region.start.unwrap_or(FluxPtr::null());
1507+
let even_region_end = even_region.end.unwrap_or(FluxPtr::null());
1508+
let odd_region_start = odd_region.start.unwrap_or(FluxPtr::null());
1509+
let odd_region_end = odd_region.end.unwrap_or(FluxPtr::null());
1510+
1511+
// We can configure two regions at once which, given that we
1512+
// start at index 0 (an even offset), translates to a single
1513+
// CSR write for the pmpcfgX register:
1514+
csr::CSR.pmpconfig_set(
1515+
i / 2,
1516+
u32::from_be_bytes([
1517+
odd_region.tor.get(),
1518+
TORUserPMPCFG::OFF().get(),
1519+
even_region.tor.get(),
1520+
TORUserPMPCFG::OFF().get(),
1521+
]) as usize,
1522+
);
14551523

1456-
while let Some(even_region) = regions_iter.next() {
1457-
let odd_region_opt = regions_iter.next();
1524+
// Now, set the addresses of the respective regions, if they
1525+
// are enabled, respectively:
1526+
if even_region.tor != TORUserPMPCFG::OFF() {
1527+
csr::CSR.pmpaddr_set(
1528+
i * 2 + 0,
1529+
(even_region_start.as_usize()).overflowing_shr(2).0,
1530+
);
1531+
csr::CSR.pmpaddr_set(
1532+
i * 2 + 1,
1533+
(even_region_end.as_usize()).overflowing_shr(2).0,
1534+
);
1535+
}
1536+
1537+
if odd_region.tor != TORUserPMPCFG::OFF() {
1538+
csr::CSR.pmpaddr_set(
1539+
i * 2 + 2,
1540+
(odd_region_start.as_usize()).overflowing_shr(2).0,
1541+
);
1542+
csr::CSR.pmpaddr_set(
1543+
i * 2 + 3,
1544+
(odd_region_end.as_usize()).overflowing_shr(2).0,
1545+
);
1546+
}
1547+
}
1548+
1549+
// configures region `i` correctly
1550+
#[flux_rs::trusted]
1551+
#[flux_rs::sig(fn (i: usize, &PMPUserRegion[@er], hw_state: &strg HardwareState[@og_hw])
1552+
requires region_configured_correctly(og_hw, i)
1553+
ensures hw_state: HardwareState{new_hw:
1554+
region_configured_correctly(new_hw, i) && all_regions_configured_correctly_up_to(new_hw, i)
1555+
}
1556+
)]
1557+
fn configure_region(i: usize, even_region: &PMPUserRegion, hardware_state: &mut HardwareState) {
14581558
let even_region_start = even_region.start.unwrap_or(FluxPtr::null());
14591559
let even_region_end = even_region.end.unwrap_or(FluxPtr::null());
14601560

1461-
if let Some(odd_region) = odd_region_opt {
1462-
let odd_region_start = odd_region.start.unwrap_or(FluxPtr::null());
1463-
let odd_region_end = odd_region.end.unwrap_or(FluxPtr::null());
1464-
// We can configure two regions at once which, given that we
1465-
// start at index 0 (an even offset), translates to a single
1466-
// CSR write for the pmpcfgX register:
1467-
csr::CSR.pmpconfig_set(
1468-
i / 2,
1561+
// TODO: check overhead of code
1562+
// Modify the first two pmpcfgX octets for this region:
1563+
csr::CSR.pmpconfig_modify(
1564+
i / 2,
1565+
FieldValue::<usize, csr::pmpconfig::pmpcfg::Register>::new(
1566+
0x0000FFFF,
1567+
0,
14691568
u32::from_be_bytes([
1470-
odd_region.tor.get(),
1471-
TORUserPMPCFG::OFF().get(),
1569+
0,
1570+
0,
14721571
even_region.tor.get(),
14731572
TORUserPMPCFG::OFF().get(),
14741573
]) as usize,
1475-
);
1476-
1477-
// Now, set the addresses of the respective regions, if they
1478-
// are enabled, respectively:
1479-
if even_region.tor != TORUserPMPCFG::OFF() {
1480-
csr::CSR.pmpaddr_set(
1481-
i * 2 + 0,
1482-
(even_region_start.as_usize()).overflowing_shr(2).0,
1483-
);
1484-
csr::CSR.pmpaddr_set(
1485-
i * 2 + 1,
1486-
(even_region_end.as_usize()).overflowing_shr(2).0,
1487-
);
1488-
}
1489-
1490-
if odd_region.tor != TORUserPMPCFG::OFF() {
1491-
csr::CSR.pmpaddr_set(
1492-
i * 2 + 2,
1493-
(odd_region_start.as_usize()).overflowing_shr(2).0,
1494-
);
1495-
csr::CSR.pmpaddr_set(
1496-
i * 2 + 3,
1497-
(odd_region_end.as_usize()).overflowing_shr(2).0,
1498-
);
1499-
}
1574+
),
1575+
);
15001576

1501-
i += 2;
1502-
} else {
1503-
// TODO: check overhead of code
1504-
// Modify the first two pmpcfgX octets for this region:
1505-
csr::CSR.pmpconfig_modify(
1506-
i / 2,
1507-
FieldValue::<usize, csr::pmpconfig::pmpcfg::Register>::new(
1508-
0x0000FFFF,
1509-
0,
1510-
u32::from_be_bytes([
1511-
0,
1512-
0,
1513-
even_region.tor.get(),
1514-
TORUserPMPCFG::OFF().get(),
1515-
]) as usize,
1516-
),
1577+
// Set the addresses if the region is enabled:
1578+
if even_region.tor != TORUserPMPCFG::OFF() {
1579+
csr::CSR.pmpaddr_set(
1580+
i * 2 + 0,
1581+
(even_region_start.as_usize()).overflowing_shr(2).0,
15171582
);
1583+
csr::CSR.pmpaddr_set(
1584+
i * 2 + 1,
1585+
(even_region_end.as_usize()).overflowing_shr(2).0,
1586+
);
1587+
}
1588+
}
15181589

1519-
// Set the addresses if the region is enabled:
1520-
if even_region.tor != TORUserPMPCFG::OFF() {
1521-
csr::CSR.pmpaddr_set(
1522-
i * 2 + 0,
1523-
(even_region_start.as_usize()).overflowing_shr(2).0,
1524-
);
1525-
csr::CSR.pmpaddr_set(
1526-
i * 2 + 1,
1527-
(even_region_end.as_usize()).overflowing_shr(2).0,
1528-
);
1590+
#[flux_rs::sig(
1591+
fn (i: usize, core::slice::Iter<PMPUserRegion>[@idx, @len], max_regions: usize, hw_state: &strg HardwareState[@og_hw])
1592+
requires
1593+
all_regions_configured_correctly_up_to(og_hw, i)
1594+
&& len == max_regions
1595+
&& i == idx
1596+
&& idx <= len
1597+
ensures hw_state: HardwareState{new_hw: all_regions_configured_correctly_up_to(new_hw, max_regions)}
1598+
)]
1599+
fn configure_all_regions_tail(i: usize, mut regions_iter: core::slice::Iter<'_, PMPUserRegion>, max_regions: usize, hardware_state: &mut HardwareState) {
1600+
if let Some(even_region) = regions_iter.next() {
1601+
let odd_region_opt = regions_iter.next();
1602+
1603+
match odd_region_opt {
1604+
None => {
1605+
configure_region(i, even_region, hardware_state);
1606+
all_regions_configured_correctly_step(hardware_state, i);
1607+
configure_all_regions_tail(i + 1, regions_iter, max_regions, hardware_state);
1608+
}
1609+
Some(odd_region) => {
1610+
configure_region_pair(i, even_region, odd_region, hardware_state);
1611+
all_regions_configured_correctly_step(hardware_state, i);
1612+
all_regions_configured_correctly_step(hardware_state, i + 1);
1613+
configure_all_regions_tail(i + 2, regions_iter, max_regions, hardware_state);
1614+
}
15291615
}
1616+
}
1617+
}
15301618

1531-
i += 1;
1532-
}
1619+
// this should be an invariant but it's on a trait so things are weird
1620+
if regions.len() == 0 {
1621+
return Err(());
15331622
}
1623+
let regions_iter = regions.iter();
1624+
// call lemma to establish the original precondition
1625+
all_regions_configured_correctly_base(hardware_state);
1626+
configure_all_regions_tail(0, regions_iter, MPU_REGIONS, hardware_state);
15341627

15351628
Ok(())
15361629
}
@@ -1556,7 +1649,7 @@ pub mod simple {
15561649
pub mod kernel_protection {
15571650
use flux_support::LocalRegisterCopyU8;
15581651
use super::{
1559-
pmpcfg_octet, NAPOTRegionSpec, PMPUserRegion, TORRegionSpec, TORUserPMP, TORUserPMPCFG,
1652+
pmpcfg_octet, NAPOTRegionSpec, PMPUserRegion, TORRegionSpec, TORUserPMP, TORUserPMPCFG, HardwareState
15601653
};
15611654
use crate::csr;
15621655
use core::fmt;
@@ -1832,7 +1925,11 @@ pub mod kernel_protection {
18321925
// `u32::from_be_bytes` and then cast to usize, as it manages to compile
18331926
// on 64-bit systems as well. However, this implementation will not work
18341927
// on RV64I systems, due to the changed pmpcfgX CSR layout.
1835-
fn configure_pmp(&self, regions: &[PMPUserRegion; MPU_REGIONS]) -> Result<(), ()> {
1928+
#[flux_rs::sig(fn (&Self, &[PMPUserRegion; _], hw_state: &strg HardwareState) -> Result<(), ()>[#ok] ensures hw_state: HardwareState {hw:
1929+
ok => all_regions_configured_correctly_up_to(hw, MPU_REGIONS)
1930+
})]
1931+
#[flux_rs::trusted]
1932+
fn configure_pmp(&self, regions: &[PMPUserRegion; MPU_REGIONS], hardware_state: &mut HardwareState) -> Result<(), ()> {
18361933
// Could use `iter_array_chunks` once that's stable.
18371934
let mut regions_iter = regions.iter();
18381935
let mut i = 0;
@@ -1943,7 +2040,7 @@ pub mod kernel_protection {
19432040
pub mod kernel_protection_mml_epmp {
19442041
use flux_support::LocalRegisterCopyU8;
19452042
use super::{
1946-
pmpcfg_octet, NAPOTRegionSpec, PMPUserRegion, TORRegionSpec, TORUserPMP, TORUserPMPCFG,
2043+
pmpcfg_octet, NAPOTRegionSpec, PMPUserRegion, TORRegionSpec, TORUserPMP, TORUserPMPCFG, HardwareState
19472044
};
19482045
use crate::csr;
19492046
use crate::pmp::permissions_to_pmpcfg;
@@ -2225,7 +2322,11 @@ pub mod kernel_protection_mml_epmp {
22252322
// `u32::from_be_bytes` and then cast to usize, as it manages to compile
22262323
// on 64-bit systems as well. However, this implementation will not work
22272324
// on RV64I systems, due to the changed pmpcfgX CSR layout.
2228-
fn configure_pmp(&self, regions: &[PMPUserRegion; MPU_REGIONS]) -> Result<(), ()> {
2325+
#[flux_rs::sig(fn (&Self, &[PMPUserRegion; _], hw_state: &strg HardwareState) -> Result<(), ()>[#ok] ensures hw_state: HardwareState {hw:
2326+
ok => all_regions_configured_correctly_up_to(hw, MPU_REGIONS)
2327+
})]
2328+
#[flux_rs::trusted]
2329+
fn configure_pmp(&self, regions: &[PMPUserRegion; MPU_REGIONS], hardware_state: &mut HardwareState) -> Result<(), ()> {
22292330
// Configure all of the regions' addresses and store their pmpcfg octets
22302331
// in our shadow storage. If the user PMP is already enabled, we further
22312332
// apply this configuration (set the pmpcfgX CSRs) by running

0 commit comments

Comments
 (0)