Skip to content

Commit d0f4fa6

Browse files
committed
tool: Change format of specifying cap maps for pds
Signed-off-by: Krishnan Winter <[email protected]>
1 parent 08af88d commit d0f4fa6

File tree

2 files changed

+76
-74
lines changed

2 files changed

+76
-74
lines changed

tool/microkit/src/capdl/builder.rs

Lines changed: 27 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -19,13 +19,12 @@ use crate::{
1919
capdl::{
2020
irq::create_irq_handler_cap,
2121
memory::{create_vspace, create_vspace_ept, map_page},
22-
spec::{capdl_obj_physical_size_bits, ElfContent},
22+
spec::{ElfContent, capdl_obj_physical_size_bits},
2323
util::*,
2424
},
2525
elf::ElfFile,
2626
sdf::{
27-
CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME,
28-
MONITOR_PRIORITY,
27+
BUDGET_DEFAULT, CapMapType, CpuCore, MONITOR_PD_NAME, MONITOR_PRIORITY, SysMap, SysMapPerms, SystemDescription
2928
},
3029
sel4::{Arch, Config, PageSize},
3130
util::{ranges_overlap, round_down, round_up},
@@ -1115,39 +1114,37 @@ pub fn build_capdl_spec(
11151114
for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() {
11161115
let pd_dest_cspace_id = *pd_id_to_cspace_id.get(&pd_dest_idx).unwrap();
11171116

1118-
for cap_map in pd.tcb_cap_maps.iter() {
1119-
// Get the TCB of the pd referenced in cap_map name
1117+
for cap_map in pd.cap_maps.iter() {
11201118
let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name)
11211119
.ok_or(format!("PD: '{}', does not exist when trying to map extra TCB cap into PD: '{}'", cap_map.pd_name, pd.name))?;
1122-
let pd_tcb_id = *pd_id_to_tcb_id.get(&pd_src_idx).unwrap();
11231120

1124-
// Map this into the destination pd's cspace and the specified slot.
1125-
let pd_tcb_cap = capdl_util_make_tcb_cap(pd_tcb_id);
1126-
capdl_util_insert_cap_into_cspace(
1127-
&mut spec_container,
1128-
pd_dest_cspace_id,
1129-
(PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32,
1130-
pd_tcb_cap,
1131-
);
1132-
}
1121+
if cap_map.cap_type == CapMapType::Tcb {
1122+
// Get the TCB of the pd referenced in cap_map name
1123+
let pd_tcb_id = *pd_id_to_tcb_id.get(&pd_src_idx).unwrap();
11331124

1134-
for cap_map in pd.sc_cap_maps.iter() {
1135-
let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name)
1136-
.ok_or(format!("PD: '{}', does not exist when trying to map extra SC cap into PD: '{}'", cap_map.pd_name, pd.name))?;
1137-
1138-
if system.protection_domains[*pd_src_idx].passive {
1139-
return Err(format!("Trying to map scheduling context of a passive PD: '{}' into PD: '{}'", cap_map.pd_name, pd.name));
1140-
}
1125+
// Map this into the destination pd's cspace and the specified slot.
1126+
let pd_tcb_cap = capdl_util_make_tcb_cap(pd_tcb_id);
1127+
capdl_util_insert_cap_into_cspace(
1128+
&mut spec_container,
1129+
pd_dest_cspace_id,
1130+
(PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32,
1131+
pd_tcb_cap,
1132+
);
1133+
} else if cap_map.cap_type == CapMapType::Sc {
1134+
if system.protection_domains[*pd_src_idx].passive {
1135+
return Err(format!("Trying to map scheduling context of a passive PD: '{}' into PD: '{}'", cap_map.pd_name, pd.name));
1136+
}
11411137

1142-
let pd_sc_id = *pd_id_to_sc_id.get(&pd_src_idx).unwrap();
1138+
let pd_sc_id = *pd_id_to_sc_id.get(&pd_src_idx).unwrap();
11431139

1144-
let pd_sc_cap = capdl_util_make_tcb_cap(pd_sc_id);
1145-
capdl_util_insert_cap_into_cspace(
1146-
&mut spec_container,
1147-
pd_dest_cspace_id,
1148-
(PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32,
1149-
pd_sc_cap,
1150-
);
1140+
let pd_sc_cap = capdl_util_make_tcb_cap(pd_sc_id);
1141+
capdl_util_insert_cap_into_cspace(
1142+
&mut spec_container,
1143+
pd_dest_cspace_id,
1144+
(PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32,
1145+
pd_sc_cap,
1146+
);
1147+
}
11511148
}
11521149
}
11531150

tool/microkit/src/sdf.rs

Lines changed: 49 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -261,8 +261,7 @@ pub struct ProtectionDomain {
261261
pub irqs: Vec<SysIrq>,
262262
pub ioports: Vec<IOPort>,
263263
pub setvars: Vec<SysSetVar>,
264-
pub tcb_cap_maps: Vec<CapMap>,
265-
pub sc_cap_maps: Vec<CapMap>,
264+
pub cap_maps: Vec<CapMap>,
266265
pub virtual_machine: Option<VirtualMachine>,
267266
/// Only used when parsing child PDs. All elements will be removed
268267
/// once we flatten each PD and its children into one list.
@@ -277,8 +276,15 @@ pub struct ProtectionDomain {
277276
text_pos: Option<roxmltree::TextPos>,
278277
}
279278

279+
#[derive(Debug, PartialEq, Eq)]
280+
pub enum CapMapType {
281+
Tcb = 1,
282+
Sc = 2,
283+
}
284+
280285
#[derive(Debug, PartialEq, Eq)]
281286
pub struct CapMap {
287+
pub cap_type: CapMapType,
282288
pub pd_name: String,
283289
pub dest_cspace_slot: u64,
284290
}
@@ -596,8 +602,7 @@ impl ProtectionDomain {
596602
let mut ioports = Vec::new();
597603
let mut setvars: Vec<SysSetVar> = Vec::new();
598604
let mut child_pds = Vec::new();
599-
let mut tcb_cap_maps = Vec::new();
600-
let mut sc_cap_maps = Vec::new();
605+
let mut cap_maps = Vec::new();
601606

602607
let mut program_image = None;
603608
let mut virtual_machine = None;
@@ -1052,11 +1057,8 @@ impl ProtectionDomain {
10521057

10531058
virtual_machine = Some(vm);
10541059
}
1055-
"tcb_cap_map" => {
1056-
tcb_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?);
1057-
}
1058-
"sc_cap_map" => {
1059-
sc_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?);
1060+
"cap" => {
1061+
cap_maps.push(CapMap::from_xml(xml_sdf, &child)?);
10601062
}
10611063
_ => {
10621064
let pos = xml_sdf.doc.text_pos_at(child.range().start);
@@ -1094,8 +1096,7 @@ impl ProtectionDomain {
10941096
irqs,
10951097
ioports,
10961098
setvars,
1097-
tcb_cap_maps,
1098-
sc_cap_maps,
1099+
cap_maps,
10991100
child_pds,
11001101
virtual_machine,
11011102
has_children,
@@ -1237,9 +1238,20 @@ impl CapMap {
12371238
xml_sdf: &XmlSystemDescription,
12381239
node: &roxmltree::Node,
12391240
) -> Result<CapMap, String> {
1240-
check_attributes(xml_sdf, node, &["src_pd_name", "dest_cspace_slot"])?;
1241+
check_attributes(xml_sdf, node, &["type", "pd", "dest_cspace_slot"])?;
12411242

1242-
let pd_name = checked_lookup(xml_sdf, node, "src_pd_name")?.to_string();
1243+
let cap_type =
1244+
match checked_lookup(xml_sdf, node, "type")? {
1245+
"tcb" => CapMapType::Tcb,
1246+
"sc" => CapMapType::Sc,
1247+
_ => return Err(value_error(
1248+
xml_sdf,
1249+
node,
1250+
"type must be 'tcb' or 'sc' ".to_string(),
1251+
))
1252+
};
1253+
1254+
let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string();
12431255
let dest_cspace_slot = sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?;
12441256

12451257
if dest_cspace_slot >= 128 {
@@ -1251,6 +1263,7 @@ impl CapMap {
12511263
}
12521264

12531265
Ok(CapMap {
1266+
cap_type,
12541267
pd_name,
12551268
dest_cspace_slot,
12561269
})
@@ -1933,48 +1946,40 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result<SystemDescrip
19331946
}
19341947

19351948
// Ensure that there are no overlapping extra cap maps in the user caps region
1949+
// and we are not mapping in the same tcb/sc
19361950
for pd in &pds {
19371951
let mut user_cap_slots = Vec::new();
19381952
let mut user_tcb_names = Vec::new();
19391953
let mut user_sc_names = Vec::new();
19401954

1941-
for tcb_cap_map in pd.tcb_cap_maps.iter() {
1942-
if user_cap_slots.contains(&tcb_cap_map.dest_cspace_slot) {
1943-
return Err(format!(
1944-
"Error: Overlapping cap slot: {} in protection domain: '{}'",
1945-
tcb_cap_map.dest_cspace_slot,
1946-
pd.name));
1947-
} else {
1948-
user_cap_slots.push(tcb_cap_map.dest_cspace_slot);
1949-
}
1950-
1951-
if user_tcb_names.contains(&tcb_cap_map.pd_name) {
1952-
return Err(format!(
1953-
"Error: Duplicate tcb cap mapping. Src PD: '{}', dest PD: '{}'",
1954-
tcb_cap_map.pd_name,
1955-
pd.name));
1956-
} else {
1957-
user_tcb_names.push(tcb_cap_map.pd_name.clone());
1958-
}
1959-
}
1960-
1961-
for sc_cap_map in pd.sc_cap_maps.iter() {
1962-
if user_cap_slots.contains(&sc_cap_map.dest_cspace_slot) {
1955+
for cap_map in pd.cap_maps.iter() {
1956+
if user_cap_slots.contains(&cap_map.dest_cspace_slot) {
19631957
return Err(format!(
19641958
"Error: Overlapping cap slot: {} in protection domain: '{}'",
1965-
sc_cap_map.dest_cspace_slot,
1959+
cap_map.dest_cspace_slot,
19661960
pd.name));
19671961
} else {
1968-
user_cap_slots.push(sc_cap_map.dest_cspace_slot);
1962+
user_cap_slots.push(cap_map.dest_cspace_slot);
19691963
}
19701964

1971-
if user_sc_names.contains(&sc_cap_map.pd_name) {
1972-
return Err(format!(
1973-
"Error: Duplicate sc cap mapping. Src PD: '{}', dest PD: '{}'",
1974-
sc_cap_map.pd_name,
1975-
pd.name));
1976-
} else {
1977-
user_sc_names.push(sc_cap_map.pd_name.clone());
1965+
if cap_map.cap_type == CapMapType::Tcb {
1966+
if user_tcb_names.contains(&cap_map.pd_name) {
1967+
return Err(format!(
1968+
"Error: Duplicate tcb cap mapping. Src PD: '{}', dest PD: '{}'",
1969+
cap_map.pd_name,
1970+
pd.name));
1971+
} else {
1972+
user_tcb_names.push(cap_map.pd_name.clone());
1973+
}
1974+
} else if cap_map.cap_type == CapMapType::Sc {
1975+
if user_sc_names.contains(&cap_map.pd_name) {
1976+
return Err(format!(
1977+
"Error: Duplicate sc cap mapping. Src PD: '{}', dest PD: '{}'",
1978+
cap_map.pd_name,
1979+
pd.name));
1980+
} else {
1981+
user_sc_names.push(cap_map.pd_name.clone());
1982+
}
19781983
}
19791984
}
19801985
}

0 commit comments

Comments
 (0)