diff --git a/example/cap_sharing/Makefile b/example/cap_sharing/Makefile index 567863e8e..0901a34c9 100644 --- a/example/cap_sharing/Makefile +++ b/example/cap_sharing/Makefile @@ -55,6 +55,8 @@ LIBS := -lmicrokit -Tmicrokit.ld IMAGE_FILE = $(BUILD_DIR)/loader.img REPORT_FILE = $(BUILD_DIR)/report.txt +SPEC = $(BUILD_DIR)/capdl_spec.json +KERNEL_32B = $(BUILD_DIR)/sel4_32.elf all: $(IMAGE_FILE) @@ -67,5 +69,34 @@ $(BUILD_DIR)/%.o: %.c Makefile | $(BUILD_DIR) $(BUILD_DIR)/%.elf: $(BUILD_DIR)/%.o $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ -$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) cap_sharing.system - $(MICROKIT_TOOL) cap_sharing.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) +$(IMAGE_FILE) $(KERNEL_32B) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) cap_sharing.system + $(MICROKIT_TOOL) cap_sharing.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) --capdl-json $(SPEC) + +ifeq ($(ARCH),x86_64) +qemu: $(KERNEL_32B) $(IMAGE_FILE) + qemu-system-x86_64 \ + -cpu qemu64,+fsgsbase,+pdpe1gb,+xsaveopt,+xsave \ + -m "1G" \ + -display none \ + -serial mon:stdio \ + -kernel $(KERNEL_32B) \ + -initrd $(IMAGE_FILE) +else ifeq ($(ARCH),aarch64) +qemu: $(IMAGE_FILE) + qemu-system-aarch64 \ + -machine virt,virtualization=on -cpu cortex-a53 \ + -nographic \ + -m size=2G \ + -serial mon:stdio \ + -device loader,file=$(IMAGE_FILE),addr=0x70000000,cpu-num=0 +else ifeq ($(ARCH),riscv64) +qemu: $(IMAGE_FILE) + qemu-system-riscv64 \ + -machine virt \ + -kernel $(IMAGE_FILE) \ + -nographic \ + -m size=2G \ + -serial mon:stdio +else +$(error Unsupported ARCH) +endif diff --git a/example/cap_sharing/cap_sharing.system b/example/cap_sharing/cap_sharing.system index 3f18d6fa1..18247d2de 100644 --- a/example/cap_sharing/cap_sharing.system +++ b/example/cap_sharing/cap_sharing.system @@ -5,6 +5,8 @@ SPDX-License-Identifier: BSD-2-Clause --> + + @@ -16,6 +18,8 @@ + + diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 1b59319d2..79b612452 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -33,6 +33,10 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define BASE_IOPORT_CAP 394 #define BASE_USER_CAPS 458 +/* This should be kept in sync with `PD_ROOT_CAP_BITS` in capdl/builder.rs */ +#define PD_ROOT_CAP_BITS 6 +#define PD_ROOT_CAP_SIZE (1ULL << PD_ROOT_CAP_BITS) + #define MICROKIT_MAX_USER_CAPS 128 #define MICROKIT_MAX_CHANNELS 62 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1) @@ -594,9 +598,9 @@ static inline void microkit_deferred_irq_ack(microkit_channel ch) **/ static inline seL4_CPtr microkit_cspace_root_slot_to_cptr(seL4_Word slot) { - if (slot > MICROKIT_MAX_USER_CAPS) { + if (slot == 0 || slot >= PD_ROOT_CAP_SIZE) { return seL4_CapNull; } - return BASE_USER_CAPS + slot; + return slot << (seL4_WordBits - PD_ROOT_CAP_BITS); } diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 5bb401be0..1fc278684 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -95,14 +95,11 @@ 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_VCPU_CAP: u64 = PD_BASE_VM_TCB_CAP + 64; const PD_BASE_IOPORT_CAP: u64 = PD_BASE_VCPU_CAP + 64; -// 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; + +/* This should be kept in sync with `PD_ROOT_CAP_BITS` in libmicrokit/include/microkit.h */ +const PD_ROOT_CAP_SIZE: u32 = 64; +const PD_ROOT_CAP_BITS: u8 = PD_ROOT_CAP_SIZE.ilog2() as u8; +pub const PD_CAP_SIZE: u32 = 512; 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; @@ -120,6 +117,7 @@ pub struct ExpectedAllocation { struct PDShadowCspace { cspace: ObjectId, + microkit_cnode: ObjectId, notification: ObjectId, endpoint: Option, sched_context: ObjectId, @@ -573,7 +571,32 @@ pub fn build_capdl_spec( } // ********************************* - // Step 3. Create the PDs' spec + // Step 3. Create the CNodes' spec + // ********************************* + let mut user_cnodes: HashMap = HashMap::new(); + for (cnode_idx, cnode) in system.cnodes.iter().enumerate() { + let cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &(cnode.name.clone()), + cnode.size_bits, + Vec::new(), + ); + + // Have a cap at slot 0 pointing to itself + let pd_guard_size = kernel_config.cap_address_bits - cnode.size_bits as u64 - PD_ROOT_CAP_BITS as u64; + let cnode_cap_self_ref = capdl_util_make_cnode_cap(cnode_obj_id, 0, pd_guard_size.try_into().unwrap()); + capdl_util_insert_cap_into_cspace( + &mut spec_container, + cnode_obj_id, + 0, + cnode_cap_self_ref, + ); + + user_cnodes.insert(cnode_idx, (cnode_obj_id, cnode.size_bits)); + } + + // ********************************* + // Step 4. Create the PDs' spec // ********************************* // On ARM, check if we need to create the SMC object let arm_smc_obj_id = if kernel_config.arch == Arch::Aarch64 @@ -605,7 +628,7 @@ pub fn build_capdl_spec( let mut caps_to_bind_to_tcb: Vec = Vec::new(); let mut caps_to_insert_to_pd_cspace: Vec = Vec::new(); - // Step 3-1: Create TCB and VSpace with all ELF loadable frames mapped in. + // Step 4-1: Create TCB and VSpace with all ELF loadable frames mapped in. let pd_tcb_obj_id = spec_container .add_elf_to_spec(kernel_config, &pd.name, pd.cpu, pd_global_idx, elf_obj) .unwrap(); @@ -626,7 +649,7 @@ pub fn build_capdl_spec( capdl_util_make_page_table_cap(pd_vspace_obj_id), )); - // Step 3-2: Map in all Memory Regions + // Step 4-2: Map in all Memory Regions for map in pd.maps.iter() { let frames = &mr_name_to_frames[&map.mr]; // MRs have frames of equal size so just use the first frame's page size. @@ -663,7 +686,7 @@ pub fn build_capdl_spec( ); } - // Step 3-3: Create and map in the stack (bottom up) + // Step 4-3: Create and map in the stack (bottom up) let mut cur_stack_vaddr = kernel_config.pd_stack_bottom(pd.stack_size); pd_stack_bottoms.push(cur_stack_vaddr); let num_stack_frames = pd.stack_size / PageSize::Small as u64; @@ -692,7 +715,7 @@ pub fn build_capdl_spec( cur_stack_vaddr += PageSize::Small as u64; } - // Step 3-4 Create Scheduling Context + // Step 4-4 Create Scheduling Context let pd_sc_obj_id = capdl_util_make_sc_obj( &mut spec_container, &pd.name, @@ -707,7 +730,7 @@ pub fn build_capdl_spec( pd_sc_cap, )); - // Step 3-5 Create fault Endpoint cap to parent/monitor + // Step 4-5 Create fault Endpoint cap to parent/monitor let pd_fault_ep_cap = if let Some(pd_parent_id) = pd.parent { assert!(pd_global_idx > pd_parent_id); let badge: u64 = FAULT_BADGE | pd.id.unwrap(); @@ -742,7 +765,7 @@ pub fn build_capdl_spec( pd_fault_ep_cap.clone(), )); - // Step 3-6 Create cap to Monitor's endpoint for passive PDs. + // Step 4-6 Create cap to Monitor's endpoint for passive PDs. if pd.passive { let pd_monitor_ep_cap = capdl_util_make_endpoint_cap( mon_fault_ep_obj_id, @@ -757,7 +780,7 @@ pub fn build_capdl_spec( )); } - // Step 3-7 Create endpoint object for the PD if it has children or can receive PPCs, else it will be a notification + // Step 4-7 Create endpoint object for the PD if it has children or can receive PPCs, else it will be a notification let pd_ntfn_obj_id = capdl_util_make_ntfn_obj(&mut spec_container, &pd.name); let pd_ntfn_cap = capdl_util_make_ntfn_cap(pd_ntfn_obj_id, true, true, 0); let mut pd_ep_obj_id: Option = None; @@ -783,13 +806,13 @@ pub fn build_capdl_spec( pd_ntfn_cap, )); - // Step 3-8 Create Reply obj + cap and insert into CSpace + // Step 4-8 Create Reply obj + cap and insert into CSpace let pd_reply_obj_id = capdl_util_make_reply_obj(&mut spec_container, &pd.name); let pd_reply_cap = capdl_util_make_reply_cap(pd_reply_obj_id); caps_to_insert_to_pd_cspace .push(capdl_util_make_cte(PD_REPLY_CAP_IDX as u32, pd_reply_cap)); - // Step 3-9 Create spec and caps to IRQs + // Step 4-9 Create spec and caps to IRQs for irq in pd.irqs.iter() { // Create a IRQ handler cap and insert into the requested CSpace's slot. let irq_handle_cap = create_irq_handler_cap( @@ -805,7 +828,7 @@ pub fn build_capdl_spec( .push(capdl_util_make_cte(irq_cap_idx as u32, irq_handle_cap)); } - // Step 3-10 Create I/O port objects on x86 platform. + // Step 4-10 Create I/O port objects on x86 platform. for ioport in pd.ioports.iter() { let ioport_obj_id = capdl_util_make_ioport_obj(&mut spec_container, &pd.name, ioport.addr, ioport.size); @@ -816,7 +839,7 @@ pub fn build_capdl_spec( )); } - // Step 3-11 Create VM Spec. + // Step 4-11 Create VM Spec. if let Some(virtual_machine) = &pd.virtual_machine { // A VM really is just a collection of special threads, it has its own TCBs, Scheduling Contexts, etc... // The difference is that it have a vCPU for each TCB to store the virtual CPUs' states. @@ -999,7 +1022,7 @@ pub fn build_capdl_spec( } } - // Step 3-12 Create ARM SMC cap if requested. + // Step 4-12 Create ARM SMC cap if requested. if pd.smc { caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( PD_ARM_SMC_CAP_IDX as u32, @@ -1007,21 +1030,39 @@ pub fn build_capdl_spec( )); } - // Step 3-13 Create CSpace and add all caps that the PD code and libmicrokit need to access. + // Step 4-13 Create CSpace and add all caps that the PD code and libmicrokit need to access. let pd_cnode_obj_id = capdl_util_make_cnode_obj( &mut spec_container, &pd.name, PD_CAP_BITS, caps_to_insert_to_pd_cspace, ); - let pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; + let pd_guard_size = + kernel_config.cap_address_bits - PD_CAP_BITS as u64 - PD_ROOT_CAP_BITS as u64; let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8); + + let pd_root_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &(pd.name.clone() + "_root"), + PD_ROOT_CAP_BITS, + Vec::new(), + ); + // leave the guard size root cnode as 0 + let pd_root_cnode_cap = capdl_util_make_cnode_cap(pd_root_cnode_obj_id, 0, 0); + // place microkit managed cnode at slot 0 + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_root_cnode_obj_id, + 0, + pd_cnode_cap, + ); + caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::CSpace as u32, - pd_cnode_cap, + pd_root_cnode_cap, )); - // Step 3-14 Set the TCB parameters and all the various caps that we need to bind to this TCB. + // Step 4-14 Set the TCB parameters and all the various caps that we need to bind to this TCB. if let Object::Tcb(pd_tcb) = &mut spec_container .get_root_object_mut(pd_tcb_obj_id) .unwrap() @@ -1041,7 +1082,7 @@ pub fn build_capdl_spec( unreachable!("internal bug: build_capdl_spec() got a non TCB object ID when trying to set TCB parameters for the monitor."); } - // Step 3-15 bind this PD's TCB to the monitor, this accomplish two purposes: + // Step 4-15 bind this PD's TCB to the monitor, this accomplish two purposes: // 1. Allow PDs' TCBs to be named to their proper name in SDF in debug config. // 2. Allow passive PDs. capdl_util_insert_cap_into_cspace( @@ -1070,7 +1111,8 @@ pub fn build_capdl_spec( pd_shadow_cspaces.insert( pd_global_idx, PDShadowCspace { - cspace: pd_cnode_obj_id, + cspace: pd_root_cnode_obj_id, + microkit_cnode: pd_cnode_obj_id, endpoint: pd_ep_obj_id, notification: pd_ntfn_obj_id, sched_context: pd_sc_obj_id, @@ -1081,11 +1123,11 @@ pub fn build_capdl_spec( } // ********************************* - // Step 4. Create channels + // Step 5. Create channels // ********************************* for channel in system.channels.iter() { - let pd_a_cspace_id = pd_shadow_cspaces[&channel.end_a.pd].cspace; - let pd_b_cspace_id = pd_shadow_cspaces[&channel.end_b.pd].cspace; + let pd_a_cspace_id = pd_shadow_cspaces[&channel.end_a.pd].microkit_cnode; + let pd_b_cspace_id = pd_shadow_cspaces[&channel.end_b.pd].microkit_cnode; let pd_a_ntfn_id = pd_shadow_cspaces[&channel.end_a.pd].notification; let pd_b_ntfn_id = pd_shadow_cspaces[&channel.end_b.pd].notification; @@ -1148,7 +1190,7 @@ pub fn build_capdl_spec( } // ********************************* - // Step 5. Handle extra cap mappings + // Step 6. Handle extra cap mappings // ********************************* for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() { @@ -1157,27 +1199,63 @@ pub fn build_capdl_spec( for cap_map in pd.cap_maps.iter() { // TODO: Once we add more CapMap options, they might not all have // the pd_name. But for now, they do. - let pd_src_shadow_cspace = &pd_shadow_cspaces[&cap_map.pd.unwrap()]; + if let Some(src_pd) = cap_map.pd { + let pd_src_shadow_cspace = &pd_shadow_cspaces[&src_pd]; + + let cap_map_obj = match cap_map.cap_type { + CapMapType::Tcb => capdl_util_make_tcb_cap(pd_src_shadow_cspace.tcb), + CapMapType::Sc => capdl_util_make_sc_cap(pd_src_shadow_cspace.sched_context), + CapMapType::VSpace => capdl_util_make_page_table_cap(pd_src_shadow_cspace.vspace), + CapMapType::CSpace => { + let Some(named_object) = + spec_container.get_root_object(pd_src_shadow_cspace.cspace) + else { + unreachable!("internal bug: couldn't find cnode with given obj id."); + }; + let Object::CNode(ref cnode) = named_object.object else { + unreachable!( + "internal bug: got a non-CNode object id {} with name '{}'", + usize::from(pd_src_shadow_cspace.cspace), + named_object.name.as_ref().unwrap() + ); + }; + + let guard_size = + kernel_config.cap_address_bits as u8 - PD_ROOT_CAP_BITS - cnode.size_bits; + + capdl_util_make_cnode_cap(pd_src_shadow_cspace.cspace, 0, guard_size) + } + }; - let cap_map_obj = match cap_map.cap_type { - CapMapType::Tcb => capdl_util_make_tcb_cap(pd_src_shadow_cspace.tcb), - CapMapType::Sc => capdl_util_make_sc_cap(pd_src_shadow_cspace.sched_context), - CapMapType::VSpace => capdl_util_make_sc_cap(pd_src_shadow_cspace.vspace), - CapMapType::CSpace => capdl_util_make_sc_cap(pd_src_shadow_cspace.cspace), - }; + // Map this into the destination pd's cspace and the specified slot. + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_dest_cspace_id, + cap_map.slot as u32, + cap_map_obj, + ); - // Map this into the destination pd's cspace and the specified slot. - capdl_util_insert_cap_into_cspace( - &mut spec_container, - pd_dest_cspace_id, - (PD_BASE_USER_CAPS + cap_map.slot) as u32, - cap_map_obj, - ); + } else if let Some(src_cnode) = cap_map.cnode { + if let Some((cnode_obj_id, size_bits)) = user_cnodes.get(&src_cnode) { + let pd_guard_size = kernel_config.cap_address_bits - *size_bits as u64 - PD_ROOT_CAP_BITS as u64; + let cnode_cap = capdl_util_make_cnode_cap(*cnode_obj_id, 0, pd_guard_size.try_into().unwrap()); + + // Map this into the destination pd's cspace and the specified slot. + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_dest_cspace_id, + cap_map.slot as u32, + cnode_cap, + ); + } else { + unreachable!("internal bug: couldn't find cnode with given obj id."); + } + } } } // ********************************* - // Step 6. Sort the root objects + // Step 7. 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. @@ -1188,13 +1266,13 @@ pub fn build_capdl_spec( // 3. Record all of the root objects new index. // 4. Recurse through every cap, for any cap bearing the original object ID, write the new object ID. - // Step 6-1 + // Step 7-1 let mut obj_name_to_old_id: HashMap = HashMap::new(); for (id, obj) in spec_container.spec.objects.iter().enumerate() { obj_name_to_old_id.insert(obj.name.as_ref().unwrap().clone(), id.into()); } - // Step 6-2 + // Step 7-2 spec_container.spec.objects.sort_by(|a, b| { // Objects with paddrs always come first. if a.object.paddr().is_none() && b.object.paddr().is_some() { @@ -1233,7 +1311,7 @@ pub fn build_capdl_spec( } }); - // Step 6-3 + // Step 7-3 let mut obj_old_id_to_new_id: HashMap = HashMap::new(); for (new_id, obj) in spec_container.spec.objects.iter().enumerate() { obj_old_id_to_new_id.insert( @@ -1242,7 +1320,7 @@ pub fn build_capdl_spec( ); } - // Step 6-4 + // Step 7-4 for obj in spec_container.spec.objects.iter_mut() { match obj.object.slots_mut() { Some(caps) => { diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 55f40bf8e..c0abbab1f 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -170,6 +170,27 @@ impl SysMemoryRegion { } } + +#[derive(Debug, PartialEq, Eq)] +pub struct CNode { + pub name: String, + pub size_bits: u8, +} + +impl CNode { + fn from_xml(xml_sdf: &XmlSystemDescription, node: &roxmltree::Node) -> Result { + check_attributes(xml_sdf, node, &["name", "type", "size_bits"])?; + + let name = checked_lookup(xml_sdf, node, "name")?.to_string(); + let size_bits = sdf_parse_number(checked_lookup(xml_sdf, node, "size_bits")?, node)? as u8; + + Ok(CNode { + name, + size_bits, + }) + } +} + #[derive(Debug, PartialEq, Eq)] pub enum SysIrqKind { Conventional { @@ -314,8 +335,10 @@ pub struct CapMap { // opinion, making everything think in terms of PD names, and something // that was necessary to do for the multikernel changes); the pd idx will // be filled out later during SDF parse process. - pub pd_name: String, + pub pd_name: Option, + pub cnode_name: Option, pub pd: Option, + pub cnode: Option, // The destination "slot" in the CSpace: note that this is "opaque" and // can be shifted depending on the location in the CSpace to work as the CPtr, // but here it is given as the index into the CNode. @@ -1363,15 +1386,46 @@ impl CapMap { xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, ) -> Result { - // At the moment the four cap maps we support all have the 'pd' element, - // so we can include it here. When that stops being the case we will - // have to rework this a bit. - check_attributes(xml_sdf, node, &["slot", "pd"])?; + check_attributes(xml_sdf, node, &["slot", "pd", "cnode_name"])?; + + let pd_name_maybe = node.attribute("pd").map(|pd_name_str| pd_name_str.to_string()); - let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string(); + let cnode_name_maybe = node.attribute("cnode_name").map(|cnode_name_str| cnode_name_str.to_string()); + + if cap_type != CapMapType::CSpace && cnode_name_maybe.is_some() { + return Err(value_error( + xml_sdf, + node, + format!("invalid paramter 'cnode_name' for target CapMapType"), + )); + } + + if pd_name_maybe.is_some() && cnode_name_maybe.is_some() { + return Err(value_error( + xml_sdf, + node, + format!("'pd' and 'cnode_name' cannot be both specified"), + )); + } + + if pd_name_maybe.is_none() && cnode_name_maybe.is_none() { + return Err(value_error( + xml_sdf, + node, + format!("Either 'pd' and 'cnode_name' should be specified"), + )); + } let slot = sdf_parse_number(checked_lookup(xml_sdf, node, "slot")?, node)?; + if slot == 0 { + return Err(value_error( + xml_sdf, + node, + ("The destination slot 0 has been reserved for Microkit CNode").to_string(), + )); + } + // TODO: Rework this so that we don't have a fixed upper limit. if slot >= CAP_MAP_MAX_SLOT { return Err(value_error( @@ -1383,9 +1437,11 @@ impl CapMap { Ok(CapMap { cap_type, - pd_name, + pd_name: pd_name_maybe, + cnode_name: cnode_name_maybe, // FIXME: Hack, filled out later. pd: None, + cnode: None, slot, text_pos: xml_sdf.doc.text_pos_at(node.range().start), }) @@ -1694,6 +1750,7 @@ struct XmlSystemDescription<'a> { pub struct SystemDescription { pub protection_domains: Vec, pub memory_regions: Vec, + pub cnodes: Vec, pub channels: Vec, } @@ -1927,6 +1984,7 @@ pub fn parse( let mut root_pds = vec![]; let mut mrs = vec![]; + let mut cnodes = vec![]; let mut channels = vec![]; let system = doc .root() @@ -1966,6 +2024,7 @@ pub fn parse( loc_string(&xml_sdf, pos) )); } + "cnode" => cnodes.push(CNode::from_xml(&xml_sdf, &child)?), _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!( @@ -2008,17 +2067,35 @@ pub fn parse( .enumerate() .map(|(idx, pd)| (pd.name.clone(), idx)) .collect(); + let cnode_names_to_id: HashMap<_, _> = cnodes + .iter() + .enumerate() + .map(|(idx, cnode)| (cnode.name.clone(), idx)) + .collect(); for pd in pds.iter_mut() { for cap_map in pd.cap_maps.iter_mut() { - let Some(&pd) = pd_names_to_id.get(&cap_map.pd_name) else { - return Err(format!( - "Error: unknown PD name '{}': {}", - cap_map.pd_name, - loc_string(&xml_sdf, cap_map.text_pos) - )); - }; + if let Some(pd_name) = &cap_map.pd_name { + let Some(&pd) = pd_names_to_id.get(pd_name) else { + return Err(format!( + "Error: unknown PD name '{}': {}", + pd_name, + loc_string(&xml_sdf, cap_map.text_pos) + )); + }; + + cap_map.pd = Some(pd); + } + if let Some(cnode_name) = &cap_map.cnode_name { + let Some(&cnode) = cnode_names_to_id.get(cnode_name) else { + return Err(format!( + "Error: unknown CNode name '{}': {}", + cnode_name, + loc_string(&xml_sdf, cap_map.text_pos) + )); + }; - cap_map.pd = Some(pd); + cap_map.cnode = Some(cnode); + } } } @@ -2256,12 +2333,22 @@ pub fn parse( if cap_maps.len() > 1 { let mut lines = String::new(); for mapping in cap_maps { - lines.push_str(&format!( - "\n type {:?} from '{}' at '{}'", - mapping.cap_type, - mapping.pd_name, - loc_string(&xml_sdf, mapping.text_pos) - )); + if let Some(pd_name) = &mapping.pd_name { + lines.push_str(&format!( + "\n type {:?} from '{}' at '{}'", + mapping.cap_type, + pd_name, + loc_string(&xml_sdf, mapping.text_pos) + )); + } + if let Some(cnode_name) = &mapping.cnode_name { + lines.push_str(&format!( + "\n type {:?} from '{}' at '{}'", + mapping.cap_type, + cnode_name, + loc_string(&xml_sdf, mapping.text_pos) + )); + } } return Err(format!( "Error: overlapping user caps in slot {slot} of protection domain '{}':{}", @@ -2417,6 +2504,7 @@ pub fn parse( Ok(SystemDescription { protection_domains: pds, memory_regions: mrs, + cnodes, channels, }) } diff --git a/tool/microkit/tests/sdf/cap_mappings_slot_invalid.system b/tool/microkit/tests/sdf/cap_mappings_slot_invalid.system new file mode 100644 index 000000000..60cae4116 --- /dev/null +++ b/tool/microkit/tests/sdf/cap_mappings_slot_invalid.system @@ -0,0 +1,19 @@ + + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_invalid_cnode_ref.system b/tool/microkit/tests/sdf/pd_cap_mappings_invalid_cnode_ref.system new file mode 100644 index 000000000..0ce08fee0 --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_invalid_cnode_ref.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_invalid_parameter.system b/tool/microkit/tests/sdf/pd_cap_mappings_invalid_parameter.system new file mode 100644 index 000000000..8453b69e2 --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_invalid_parameter.system @@ -0,0 +1,21 @@ + + + + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_pd_cnode_both_specified.system b/tool/microkit/tests/sdf/pd_cap_mappings_pd_cnode_both_specified.system new file mode 100644 index 000000000..0e7fa16bd --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_pd_cnode_both_specified.system @@ -0,0 +1,17 @@ + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_src_not_specified.system b/tool/microkit/tests/sdf/pd_cap_mappings_src_not_specified.system new file mode 100644 index 000000000..aa5ffeed5 --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_src_not_specified.system @@ -0,0 +1,17 @@ + + + + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 1c5046ebb..924b9eac0 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -1040,6 +1040,42 @@ mod system { ) } + #[test] + fn test_cap_mappings_invalid_parameter() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_cap_mappings_invalid_parameter.system", + "Error: invalid attribute 'cnode' on element 'cap_sc'", + ) + } + + #[test] + fn test_cap_mappings_pd_cnode_both_specified() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_cap_mappings_pd_cnode_both_specified.system", + "Error: 'pd' and 'cnode_name' cannot be both specified on element 'cap_cspace'", + ) + } + + #[test] + fn test_cap_mappings_src_not_specified() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_cap_mappings_src_not_specified.system", + "Error: Either 'pd' and 'cnode_name' should be specified on element 'cap_cspace'" + ) + } + + #[test] + fn test_cap_mappings_slot_invalid() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "cap_mappings_slot_invalid.system", + "Error: The destination slot 0 has been reserved for Microkit CNode on element 'cap_sc'", + ) + } + #[test] fn test_cap_mappings_invalid() { check_error( @@ -1057,4 +1093,13 @@ mod system { "Error: unknown PD name 'invalid': pd_cap_mappings_invalid_pd_ref.system:12:13", ) } + + #[test] + fn test_cap_mappings_invalid_cnode_ref() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_cap_mappings_invalid_cnode_ref.system", + "Error: unknown CNode name 'invalid': pd_cap_mappings_invalid_cnode_ref.system:12:13" + ) + } }