From a33639f167aa83e35053dc0ba85ab83ef9e9dc18 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Wed, 5 Nov 2025 16:17:36 +1100 Subject: [PATCH 1/5] tool: Map sc of children into parent cspace Signed-off-by: Krishnan Winter --- libmicrokit/include/microkit.h | 7 ++++--- tool/microkit/src/capdl/builder.rs | 11 ++++++++++- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index db43ff99a..c4e27c4a7 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -26,9 +26,10 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define BASE_ENDPOINT_CAP 74 #define BASE_IRQ_CAP 138 #define BASE_TCB_CAP 202 -#define BASE_VM_TCB_CAP 266 -#define BASE_VCPU_CAP 330 -#define BASE_IOPORT_CAP 394 +#define BASE_SC_CAP 266 +#define BASE_VM_TCB_CAP 330 +#define BASE_VCPU_CAP 394 +#define BASE_IOPORT_CAP 458 #define MICROKIT_MAX_CHANNELS 62 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index c40575871..6322d16a3 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -92,7 +92,8 @@ const PD_BASE_OUTPUT_NOTIFICATION_CAP: u64 = 10; const PD_BASE_OUTPUT_ENDPOINT_CAP: u64 = PD_BASE_OUTPUT_NOTIFICATION_CAP + 64; const PD_BASE_IRQ_CAP: u64 = PD_BASE_OUTPUT_ENDPOINT_CAP + 64; const PD_BASE_PD_TCB_CAP: u64 = PD_BASE_IRQ_CAP + 64; -const PD_BASE_VM_TCB_CAP: u64 = PD_BASE_PD_TCB_CAP + 64; +const PD_BASE_PD_SC_CAP: u64 = PD_BASE_PD_TCB_CAP + 64; +const PD_BASE_VM_TCB_CAP: u64 = PD_BASE_PD_SC_CAP + 64; const PD_BASE_VCPU_CAP: u64 = PD_BASE_VM_TCB_CAP + 64; const PD_BASE_IOPORT_CAP: u64 = PD_BASE_VCPU_CAP + 64; @@ -681,6 +682,14 @@ pub fn build_capdl_spec( capdl_util_make_tcb_cap(pd_tcb_obj_id), ); + // Allow the parent PD to access the child's SC: + capdl_util_insert_cap_into_cspace( + &mut spec, + *parent_cspace_obj_id, + (PD_BASE_PD_SC_CAP + pd.id.unwrap()) as usize, + capdl_util_make_sc_cap(pd_sc_obj_id), + ); + fault_ep_cap }; caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( From af25c663cfac48a969e6da3b50a7242276196faa Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Thu, 4 Dec 2025 15:12:00 +1100 Subject: [PATCH 2/5] tool: Add mapping a pd's tcb cap into another pd Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 41 +++++++++++++++++++++++++++--- tool/microkit/src/sdf.rs | 38 ++++++++++++++++++++++++++- 2 files changed, 75 insertions(+), 4 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 6322d16a3..8d1641de1 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -541,11 +541,17 @@ pub fn build_capdl_spec( None }; + // Mapping between pd name and id for faster lookups + let mut pd_name_to_id: HashMap = HashMap::new(); + // Keep tabs on each PD's CSpace, Notification and Endpoint objects so we can create channels between them at a later step. let mut pd_id_to_cspace_id: HashMap = HashMap::new(); let mut pd_id_to_ntfn_id: HashMap = HashMap::new(); let mut pd_id_to_ep_id: HashMap = HashMap::new(); + // Keep tabs on caps such as TCB so that we can create additional mappings for the cap into other PD's cspaces. + let mut pd_id_to_tcb_id: HashMap = HashMap::new(); + // Keep track of the global count of vCPU objects so we can bind them to the monitor for setting TCB name in debug config. // Only used on ARM and RISC-V as on x86-64 VMs share the same TCB as PD's which will have their TCB name set separately. let mut monitor_vcpu_idx = 0; @@ -556,6 +562,8 @@ pub fn build_capdl_spec( for (pd_global_idx, pd) in system.protection_domains.iter().enumerate() { let elf_obj = &elfs[pd_global_idx]; + pd_name_to_id.insert(pd.name.clone(), pd_global_idx); + let mut caps_to_bind_to_tcb: Vec = Vec::new(); let mut caps_to_insert_to_pd_cspace: Vec = Vec::new(); @@ -565,6 +573,9 @@ pub fn build_capdl_spec( .unwrap(); let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id); + pd_id_to_tcb_id.insert(pd_global_idx, pd_tcb_obj_id); + + // In the benchmark configuration, we allow PDs to access their own TCB. // This is necessary for accessing kernel's benchmark API. if kernel_config.benchmark { @@ -684,9 +695,9 @@ pub fn build_capdl_spec( // Allow the parent PD to access the child's SC: capdl_util_insert_cap_into_cspace( - &mut spec, + &mut spec_container, *parent_cspace_obj_id, - (PD_BASE_PD_SC_CAP + pd.id.unwrap()) as usize, + (PD_BASE_PD_SC_CAP + pd.id.unwrap()) as u32, capdl_util_make_sc_cap(pd_sc_obj_id), ); @@ -1088,7 +1099,31 @@ pub fn build_capdl_spec( } // ********************************* - // Step 5. Sort the root objects + // Step 5. Handle extra cap mappings + // ********************************* + + for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() { + let pd_dest_cspace_id = *pd_id_to_cspace_id.get(&pd_dest_idx).unwrap(); + + for cap_map in pd.tcb_cap_maps.iter() { + // Get the TCB of the pd referenced in cap_map name + let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name) + .ok_or(format!("PD: {}, does not exist when trying to map extra TCB cap into PD: {}", cap_map.pd_name, pd.name))?; + let pd_tcb_id = *pd_id_to_tcb_id.get(&pd_src_idx).unwrap(); + + // Map this into the destination pd's cspace and the specified slot. + let pd_tcb_cap = capdl_util_make_tcb_cap(pd_tcb_id); + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_dest_cspace_id, + (PD_BASE_PD_TCB_CAP + cap_map.dest_cspace_slot) as u32, + pd_tcb_cap, + ); + } + } + + // ********************************* + // Step 6. Sort the root objects // ********************************* // The CapDL initialiser expects objects with paddr to come first, then sorted by size so that the // allocation algorithm at run-time can run more efficiently. diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 17b5adbae..50a1c8214 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -261,6 +261,7 @@ pub struct ProtectionDomain { pub irqs: Vec, pub ioports: Vec, pub setvars: Vec, + pub tcb_cap_maps: Vec, pub virtual_machine: Option, /// Only used when parsing child PDs. All elements will be removed /// once we flatten each PD and its children into one list. @@ -275,6 +276,12 @@ pub struct ProtectionDomain { text_pos: Option, } +#[derive(Debug, PartialEq, Eq)] +pub struct TcbCapMap { + pub pd_name: String, + pub dest_cspace_slot: u64, +} + #[derive(Debug, PartialEq, Eq)] pub struct VirtualMachine { pub vcpus: Vec, @@ -588,6 +595,7 @@ impl ProtectionDomain { let mut ioports = Vec::new(); let mut setvars: Vec = Vec::new(); let mut child_pds = Vec::new(); + let mut tcb_cap_maps = Vec::new(); let mut program_image = None; let mut virtual_machine = None; @@ -1042,6 +1050,9 @@ impl ProtectionDomain { virtual_machine = Some(vm); } + "tcb_cap_map" => { + tcb_cap_maps.push(TcbCapMap::from_xml(xml_sdf, &child)?); + } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!( @@ -1078,6 +1089,7 @@ impl ProtectionDomain { irqs, ioports, setvars, + tcb_cap_maps, child_pds, virtual_machine, has_children, @@ -1214,6 +1226,31 @@ impl VirtualMachine { } } +impl TcbCapMap { + fn from_xml( + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + ) -> Result { + check_attributes(xml_sdf, node, &["src_pd_name", "dest_cspace_slot"])?; + + let pd_name = checked_lookup(xml_sdf, node, "src_pd_name")?.to_string(); + let dest_cspace_slot = sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?; + + if dest_cspace_slot >= 64 { + return Err(value_error( + xml_sdf, + node, + "There are only 64 destination cspace slots available. Max slot allowed is 63".to_string(), + )); + } + + Ok(TcbCapMap { + pd_name, + dest_cspace_slot, + }) + } +} + impl SysMemoryRegion { fn from_xml( config: &Config, @@ -1630,7 +1667,6 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Date: Thu, 4 Dec 2025 17:51:40 +1100 Subject: [PATCH 3/5] tool: Error checking for cap maps. User cap region Signed-off-by: Krishnan Winter --- libmicrokit/include/microkit.h | 3 +++ tool/microkit/src/capdl/builder.rs | 14 +++++++--- tool/microkit/src/sdf.rs | 41 ++++++++++++++++++++++++------ 3 files changed, 46 insertions(+), 12 deletions(-) diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index c4e27c4a7..b0e3710fb 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -31,6 +31,9 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define BASE_VCPU_CAP 394 #define BASE_IOPORT_CAP 458 +// @kwinter: Bounding user caps to 128. Is this restriction ok for now? +#define BASE_USER_CAPS 522 + #define MICROKIT_MAX_CHANNELS 62 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1) #define MICROKIT_MAX_IOPORT_ID MICROKIT_MAX_CHANNELS diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 8d1641de1..7e2a88904 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -96,8 +96,14 @@ const PD_BASE_PD_SC_CAP: u64 = PD_BASE_PD_TCB_CAP + 64; const PD_BASE_VM_TCB_CAP: u64 = PD_BASE_PD_SC_CAP + 64; const PD_BASE_VCPU_CAP: u64 = PD_BASE_VM_TCB_CAP + 64; const PD_BASE_IOPORT_CAP: u64 = PD_BASE_VCPU_CAP + 64; - -pub const PD_CAP_SIZE: u32 = 512; +// The following region can be used for whatever the user wants to map into their +// cspace. We restrict them to use this region so that they don't accidently +// overwrite other parts of the cspace. The cspace slot that the users provide +// for mapping in extra caps such as TCBs and SCs will be as an offset to this +// index. We are bounding this to 128 slots for now. +const PD_BASE_USER_CAPS: u64 = PD_BASE_IOPORT_CAP + 64; + +pub const PD_CAP_SIZE: u32 = 1024; const PD_CAP_BITS: u8 = PD_CAP_SIZE.ilog2() as u8; const PD_SCHEDCONTEXT_EXTRA_SIZE: u64 = 256; const PD_SCHEDCONTEXT_EXTRA_SIZE_BITS: u64 = PD_SCHEDCONTEXT_EXTRA_SIZE.ilog2() as u64; @@ -1108,7 +1114,7 @@ pub fn build_capdl_spec( for cap_map in pd.tcb_cap_maps.iter() { // Get the TCB of the pd referenced in cap_map name let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name) - .ok_or(format!("PD: {}, does not exist when trying to map extra TCB cap into PD: {}", cap_map.pd_name, pd.name))?; + .ok_or(format!("PD: '{}', does not exist when trying to map extra TCB cap into PD: '{}'", cap_map.pd_name, pd.name))?; let pd_tcb_id = *pd_id_to_tcb_id.get(&pd_src_idx).unwrap(); // Map this into the destination pd's cspace and the specified slot. @@ -1116,7 +1122,7 @@ pub fn build_capdl_spec( capdl_util_insert_cap_into_cspace( &mut spec_container, pd_dest_cspace_id, - (PD_BASE_PD_TCB_CAP + cap_map.dest_cspace_slot) as u32, + (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, pd_tcb_cap, ); } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 50a1c8214..20c069547 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -261,7 +261,7 @@ pub struct ProtectionDomain { pub irqs: Vec, pub ioports: Vec, pub setvars: Vec, - pub tcb_cap_maps: Vec, + pub tcb_cap_maps: Vec, pub virtual_machine: Option, /// Only used when parsing child PDs. All elements will be removed /// once we flatten each PD and its children into one list. @@ -277,7 +277,7 @@ pub struct ProtectionDomain { } #[derive(Debug, PartialEq, Eq)] -pub struct TcbCapMap { +pub struct CapMap { pub pd_name: String, pub dest_cspace_slot: u64, } @@ -1051,7 +1051,7 @@ impl ProtectionDomain { virtual_machine = Some(vm); } "tcb_cap_map" => { - tcb_cap_maps.push(TcbCapMap::from_xml(xml_sdf, &child)?); + tcb_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); @@ -1226,25 +1226,25 @@ impl VirtualMachine { } } -impl TcbCapMap { +impl CapMap { fn from_xml( xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, - ) -> Result { + ) -> Result { check_attributes(xml_sdf, node, &["src_pd_name", "dest_cspace_slot"])?; let pd_name = checked_lookup(xml_sdf, node, "src_pd_name")?.to_string(); let dest_cspace_slot = sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?; - if dest_cspace_slot >= 64 { + if dest_cspace_slot >= 128 { return Err(value_error( xml_sdf, node, - "There are only 64 destination cspace slots available. Max slot allowed is 63".to_string(), + "There are only 128 destination cspace slots available. Max slot allowed is 63".to_string(), )); } - Ok(TcbCapMap { + Ok(CapMap { pd_name, dest_cspace_slot, }) @@ -1926,6 +1926,31 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Date: Fri, 5 Dec 2025 11:24:05 +1100 Subject: [PATCH 4/5] tool: Add mapping a pd's sc cap into another pd Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 25 ++++++++++++++++++++++++- tool/microkit/src/sdf.rs | 28 ++++++++++++++++++++++++++++ 2 files changed, 52 insertions(+), 1 deletion(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 7e2a88904..70ced9d18 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -555,8 +555,9 @@ pub fn build_capdl_spec( let mut pd_id_to_ntfn_id: HashMap = HashMap::new(); let mut pd_id_to_ep_id: HashMap = HashMap::new(); - // Keep tabs on caps such as TCB so that we can create additional mappings for the cap into other PD's cspaces. + // Keep tabs on caps such as TCB and SC so that we can create additional mappings for the cap into other PD's cspaces. let mut pd_id_to_tcb_id: HashMap = HashMap::new(); + let mut pd_id_to_sc_id: HashMap = HashMap::new(); // Keep track of the global count of vCPU objects so we can bind them to the monitor for setting TCB name in debug config. // Only used on ARM and RISC-V as on x86-64 VMs share the same TCB as PD's which will have their TCB name set separately. @@ -672,6 +673,9 @@ pub fn build_capdl_spec( pd.budget, 0x100 + pd_global_idx as u64, ); + + pd_id_to_sc_id.insert(pd_global_idx, pd_sc_obj_id); + let pd_sc_cap = capdl_util_make_sc_cap(pd_sc_obj_id); caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::SchedContext as u32, @@ -1126,6 +1130,25 @@ pub fn build_capdl_spec( pd_tcb_cap, ); } + + for cap_map in pd.sc_cap_maps.iter() { + let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name) + .ok_or(format!("PD: '{}', does not exist when trying to map extra SC cap into PD: '{}'", cap_map.pd_name, pd.name))?; + + if system.protection_domains[*pd_src_idx].passive { + return Err(format!("Trying to map scheduling context of a passive PD: '{}' into PD: '{}'", cap_map.pd_name, pd.name)); + } + + let pd_sc_id = *pd_id_to_sc_id.get(&pd_src_idx).unwrap(); + + let pd_sc_cap = capdl_util_make_tcb_cap(pd_sc_id); + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_dest_cspace_id, + (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, + pd_sc_cap, + ); + } } // ********************************* diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 20c069547..4c5000fba 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -262,6 +262,7 @@ pub struct ProtectionDomain { pub ioports: Vec, pub setvars: Vec, pub tcb_cap_maps: Vec, + pub sc_cap_maps: Vec, pub virtual_machine: Option, /// Only used when parsing child PDs. All elements will be removed /// once we flatten each PD and its children into one list. @@ -596,6 +597,7 @@ impl ProtectionDomain { let mut setvars: Vec = Vec::new(); let mut child_pds = Vec::new(); let mut tcb_cap_maps = Vec::new(); + let mut sc_cap_maps = Vec::new(); let mut program_image = None; let mut virtual_machine = None; @@ -1053,6 +1055,9 @@ impl ProtectionDomain { "tcb_cap_map" => { tcb_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); } + "sc_cap_map" => { + sc_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); + } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!( @@ -1090,6 +1095,7 @@ impl ProtectionDomain { ioports, setvars, tcb_cap_maps, + sc_cap_maps, child_pds, virtual_machine, has_children, @@ -1930,6 +1936,8 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Result Date: Mon, 5 Jan 2026 13:52:26 +1100 Subject: [PATCH 5/5] tool: Change format of specifying cap maps for pds Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 66 +++++++++--------- tool/microkit/src/sdf.rs | 107 +++++++++++++++-------------- 2 files changed, 90 insertions(+), 83 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 70ced9d18..c92025cb7 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -24,8 +24,8 @@ use crate::{ }, elf::ElfFile, sdf::{ - CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME, - MONITOR_PRIORITY, + CapMapType, CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, + MONITOR_PD_NAME, MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, util::{ranges_overlap, round_down, round_up}, @@ -582,7 +582,6 @@ pub fn build_capdl_spec( pd_id_to_tcb_id.insert(pd_global_idx, pd_tcb_obj_id); - // In the benchmark configuration, we allow PDs to access their own TCB. // This is necessary for accessing kernel's benchmark API. if kernel_config.benchmark { @@ -1115,39 +1114,42 @@ pub fn build_capdl_spec( for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() { let pd_dest_cspace_id = *pd_id_to_cspace_id.get(&pd_dest_idx).unwrap(); - for cap_map in pd.tcb_cap_maps.iter() { - // Get the TCB of the pd referenced in cap_map name - let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name) - .ok_or(format!("PD: '{}', does not exist when trying to map extra TCB cap into PD: '{}'", cap_map.pd_name, pd.name))?; - let pd_tcb_id = *pd_id_to_tcb_id.get(&pd_src_idx).unwrap(); + for cap_map in pd.cap_maps.iter() { + let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name).ok_or(format!( + "PD: '{}', does not exist when trying to map extra TCB cap into PD: '{}'", + cap_map.pd_name, pd.name + ))?; - // Map this into the destination pd's cspace and the specified slot. - let pd_tcb_cap = capdl_util_make_tcb_cap(pd_tcb_id); - capdl_util_insert_cap_into_cspace( - &mut spec_container, - pd_dest_cspace_id, - (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, - pd_tcb_cap, - ); - } + if cap_map.cap_type == CapMapType::Tcb { + // Get the TCB of the pd referenced in cap_map name + let pd_tcb_id = *pd_id_to_tcb_id.get(pd_src_idx).unwrap(); - for cap_map in pd.sc_cap_maps.iter() { - let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name) - .ok_or(format!("PD: '{}', does not exist when trying to map extra SC cap into PD: '{}'", cap_map.pd_name, pd.name))?; - - if system.protection_domains[*pd_src_idx].passive { - return Err(format!("Trying to map scheduling context of a passive PD: '{}' into PD: '{}'", cap_map.pd_name, pd.name)); - } + // Map this into the destination pd's cspace and the specified slot. + let pd_tcb_cap = capdl_util_make_tcb_cap(pd_tcb_id); + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_dest_cspace_id, + (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, + pd_tcb_cap, + ); + } else if cap_map.cap_type == CapMapType::Sc { + if system.protection_domains[*pd_src_idx].passive { + return Err(format!( + "Trying to map scheduling context of a passive PD: '{}' into PD: '{}'", + cap_map.pd_name, pd.name + )); + } - let pd_sc_id = *pd_id_to_sc_id.get(&pd_src_idx).unwrap(); + let pd_sc_id = *pd_id_to_sc_id.get(pd_src_idx).unwrap(); - let pd_sc_cap = capdl_util_make_tcb_cap(pd_sc_id); - capdl_util_insert_cap_into_cspace( - &mut spec_container, - pd_dest_cspace_id, - (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, - pd_sc_cap, - ); + let pd_sc_cap = capdl_util_make_tcb_cap(pd_sc_id); + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_dest_cspace_id, + (PD_BASE_USER_CAPS + cap_map.dest_cspace_slot) as u32, + pd_sc_cap, + ); + } } } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 4c5000fba..2540ebd2c 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -261,8 +261,7 @@ pub struct ProtectionDomain { pub irqs: Vec, pub ioports: Vec, pub setvars: Vec, - pub tcb_cap_maps: Vec, - pub sc_cap_maps: Vec, + pub cap_maps: Vec, pub virtual_machine: Option, /// Only used when parsing child PDs. All elements will be removed /// once we flatten each PD and its children into one list. @@ -277,8 +276,15 @@ pub struct ProtectionDomain { text_pos: Option, } +#[derive(Debug, PartialEq, Eq)] +pub enum CapMapType { + Tcb = 1, + Sc = 2, +} + #[derive(Debug, PartialEq, Eq)] pub struct CapMap { + pub cap_type: CapMapType, pub pd_name: String, pub dest_cspace_slot: u64, } @@ -596,8 +602,7 @@ impl ProtectionDomain { let mut ioports = Vec::new(); let mut setvars: Vec = Vec::new(); let mut child_pds = Vec::new(); - let mut tcb_cap_maps = Vec::new(); - let mut sc_cap_maps = Vec::new(); + let mut cap_maps = Vec::new(); let mut program_image = None; let mut virtual_machine = None; @@ -1052,11 +1057,8 @@ impl ProtectionDomain { virtual_machine = Some(vm); } - "tcb_cap_map" => { - tcb_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); - } - "sc_cap_map" => { - sc_cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); + "cap" => { + cap_maps.push(CapMap::from_xml(xml_sdf, &child)?); } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); @@ -1094,8 +1096,7 @@ impl ProtectionDomain { irqs, ioports, setvars, - tcb_cap_maps, - sc_cap_maps, + cap_maps, child_pds, virtual_machine, has_children, @@ -1233,24 +1234,36 @@ impl VirtualMachine { } impl CapMap { - fn from_xml( - xml_sdf: &XmlSystemDescription, - node: &roxmltree::Node, - ) -> Result { - check_attributes(xml_sdf, node, &["src_pd_name", "dest_cspace_slot"])?; + fn from_xml(xml_sdf: &XmlSystemDescription, node: &roxmltree::Node) -> Result { + check_attributes(xml_sdf, node, &["type", "pd", "dest_cspace_slot"])?; + + let cap_type = match checked_lookup(xml_sdf, node, "type")? { + "tcb" => CapMapType::Tcb, + "sc" => CapMapType::Sc, + _ => { + return Err(value_error( + xml_sdf, + node, + "type must be 'tcb' or 'sc' ".to_string(), + )) + } + }; - let pd_name = checked_lookup(xml_sdf, node, "src_pd_name")?.to_string(); - let dest_cspace_slot = sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?; + let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string(); + let dest_cspace_slot = + sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?; if dest_cspace_slot >= 128 { return Err(value_error( xml_sdf, node, - "There are only 128 destination cspace slots available. Max slot allowed is 63".to_string(), + "There are only 128 destination cspace slots available. Max slot allowed is 63" + .to_string(), )); } Ok(CapMap { + cap_type, pd_name, dest_cspace_slot, }) @@ -1933,48 +1946,40 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result