Skip to content

Commit 514cf01

Browse files
committed
tool: Support vspace and cnode extra cap maps
Signed-off-by: Krishnan Winter <krishnan.winter@unsw.edu.au>
1 parent b3f2a61 commit 514cf01

2 files changed

Lines changed: 30 additions & 1 deletion

File tree

tool/microkit/src/capdl/builder.rs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -580,11 +580,14 @@ pub fn build_capdl_spec(
580580
let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id);
581581

582582
let pd_tcb_obj = capdl_util_make_tcb_cap(pd_tcb_obj_id);
583+
let pd_vspace_obj = capdl_util_make_page_table_cap(pd_vspace_obj_id);
583584

584585
pd_shadow_cspace
585586
.entry(pd_global_idx)
586587
.or_insert_with(|| vec![None; CapMapType::__Len as usize])[CapMapType::Tcb as usize] =
587588
Some(pd_tcb_obj.clone());
589+
pd_shadow_cspace.get_mut(&pd_global_idx).unwrap()[CapMapType::Vspace as usize] =
590+
Some(pd_vspace_obj.clone());
588591

589592
// In the benchmark configuration, we allow PDs to access their own TCB.
590593
// This is necessary for accessing kernel's benchmark API.
@@ -596,7 +599,7 @@ pub fn build_capdl_spec(
596599
// Allow PD to access their own VSpace for ops such as cache cleaning on ARM.
597600
caps_to_insert_to_pd_cspace.push(capdl_util_make_cte(
598601
PD_VSPACE_CAP_IDX as u32,
599-
capdl_util_make_page_table_cap(pd_vspace_obj_id),
602+
pd_vspace_obj,
600603
));
601604

602605
// Step 3-2: Map in all Memory Regions
@@ -995,6 +998,8 @@ pub fn build_capdl_spec(
995998
);
996999
let pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64;
9971000
let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8);
1001+
pd_shadow_cspace.get_mut(&pd_global_idx).unwrap()[CapMapType::Cnode as usize] =
1002+
Some(pd_cnode_cap.clone());
9981003
caps_to_bind_to_tcb.push(capdl_util_make_cte(
9991004
TcbBoundSlot::CSpace as u32,
10001005
pd_cnode_cap,

tool/microkit/src/sdf.rs

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -280,6 +280,8 @@ pub struct ProtectionDomain {
280280
pub enum CapMapType {
281281
Tcb = 0,
282282
Sc,
283+
Vspace,
284+
Cnode,
283285
__Len,
284286
}
285287

@@ -1241,6 +1243,8 @@ impl CapMap {
12411243
let cap_type = match checked_lookup(xml_sdf, node, "type")? {
12421244
"tcb" => CapMapType::Tcb,
12431245
"sc" => CapMapType::Sc,
1246+
"vspace" => CapMapType::Vspace,
1247+
"cnode" => CapMapType::Cnode,
12441248
_ => {
12451249
return Err(value_error(
12461250
xml_sdf,
@@ -1952,6 +1956,8 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result<SystemDescrip
19521956
let mut user_cap_slots = Vec::new();
19531957
let mut user_tcb_names = Vec::new();
19541958
let mut user_sc_names = Vec::new();
1959+
let mut user_vspace_names = Vec::new();
1960+
let mut user_cnode_names = Vec::new();
19551961

19561962
for cap_map in pd.cap_maps.iter() {
19571963
if user_cap_slots.contains(&cap_map.dest_cspace_slot) {
@@ -1981,6 +1987,24 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result<SystemDescrip
19811987
} else {
19821988
user_sc_names.push(cap_map.pd_name.clone());
19831989
}
1990+
} else if cap_map.cap_type == CapMapType::Vspace {
1991+
if user_vspace_names.contains(&cap_map.pd_name) {
1992+
return Err(format!(
1993+
"Error: Duplicate vspace cap mapping. Src PD: '{}', dest PD: '{}'",
1994+
cap_map.pd_name, pd.name
1995+
));
1996+
} else {
1997+
user_vspace_names.push(cap_map.pd_name.clone());
1998+
}
1999+
} else if cap_map.cap_type == CapMapType::Cnode {
2000+
if user_cnode_names.contains(&cap_map.pd_name) {
2001+
return Err(format!(
2002+
"Error: Duplicate cnode cap mapping. Src PD: '{}', dest PD: '{}'",
2003+
cap_map.pd_name, pd.name
2004+
));
2005+
} else {
2006+
user_cnode_names.push(cap_map.pd_name.clone());
2007+
}
19842008
}
19852009
}
19862010
}

0 commit comments

Comments
 (0)