diff --git a/docs/manual.md b/docs/manual.md index e1369516c..a0666ab46 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -984,6 +984,13 @@ virtual CPU with ID `vcpu`. Write the registers of a given virtual CPU with ID `vcpu`. The `regs` argument is the pointer to the struct of registers `seL4_VCPUContext` that are written from. +## `seL4_CPtr microkit_cspace_slot_to_cptr(seL4_Word slot)` {#libmicrokit_cspace_slot_to_cptr} + +Converts the slot identifier of the ``'s capability element into an +`seL4_CPtr` value to be used in `libsel4` calls by the PD. + +If the slot exceeds the valid range of inputs (`0 <= slot < MICROKIT_MAX_USER_CAPS`), it returns the value `seL4_CapNull`. + # System Description File {#sysdesc} This section describes the format of the System Description File (SDF). @@ -1025,6 +1032,7 @@ Additionally, it supports the following child elements: * `protection_domain`: (zero or more) Describes a child protection domain. * `virtual_machine`: (zero or one) Describes a child virtual machine. * `ioport`: (zero or more) Describes an I/O port, x86-64 only. +* `cspace`: (zero or one) Describes ["extra" capabilities](#sdf-cspace) in the microkit-provided CSpace. The `program_image` element has the following attributes: @@ -1125,6 +1133,29 @@ It supports the following attributes: The `memory_region` element does not support any child elements. +## `cspace` {#sdf-cspace} + +The `cspace` element represents the *Capability Space* of each protection domain. +This is an advanced feature designed for users of Microkit who want more complex runtime behaviour than the system description file allows. +For more details on how CSpaces and capabilities work, please see the ['Capability Spaces' section of the seL4 reference manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf#chapter.3). + +It supports no attributes, but supports the following elements as children: + +* `cap_tcb`: A capability to a protection domain's Thread Control Block (TCB). +* `cap_sc`: A capability to a protection domain's Scheduling Context (SC). + If the protection domain is passive, this is a capability to the notification's scheduling context. +* `cap_vspace`: A capability to a protection domain's VSpace. +* `cap_cspace`: A capability to a protection domain's CSpace. + +All of the elements support the `slot` attribute, which is is an opaque identifier used to address the capability at runtime. +To convert the `slot` to an `seL4_CPtr`, use the [`seL4_CPtr microkit_cspace_slot_to_cptr(seL4_Word slot)`](#libmicrokit_cspace_slot_to_cptr) function. + +See the 'cap_sharing' example packaged in your SDK or [on GitHub](https://github.com/seL4/microkit/tree/main/example/cap_sharing). + +All capability elements (currently) all support the `pd` attribute, the name of the protection domain that the capability is from. +For instance, `` will place the TCB of PD 'alpha' in the CSpace of the current PD. + + ### Page sizes by architecture Below are the available page sizes for each architecture that Microkit supports. diff --git a/example/cap_sharing/Makefile b/example/cap_sharing/Makefile new file mode 100644 index 000000000..567863e8e --- /dev/null +++ b/example/cap_sharing/Makefile @@ -0,0 +1,71 @@ +# +# Copyright 2026, UNSW +# +# SPDX-License-Identifier: BSD-2-Clause +# +ifeq ($(strip $(BUILD_DIR)),) +$(error BUILD_DIR must be specified) +endif + +ifeq ($(strip $(MICROKIT_SDK)),) +$(error MICROKIT_SDK must be specified) +endif + +ifeq ($(strip $(MICROKIT_BOARD)),) +$(error MICROKIT_BOARD must be specified) +endif + +ifeq ($(strip $(MICROKIT_CONFIG)),) +$(error MICROKIT_CONFIG must be specified) +endif + +BOARD_DIR := $(MICROKIT_SDK)/board/$(MICROKIT_BOARD)/$(MICROKIT_CONFIG) + +ARCH := ${shell grep 'CONFIG_SEL4_ARCH ' $(BOARD_DIR)/include/kernel/gen_config.h | cut -d' ' -f4} + +ifeq ($(ARCH),aarch64) + TARGET_TRIPLE := aarch64-none-elf + CFLAGS_ARCH := -mstrict-align +else ifeq ($(ARCH),riscv64) + TARGET_TRIPLE := riscv64-unknown-elf + CFLAGS_ARCH := -march=rv64imafdc_zicsr_zifencei -mabi=lp64d +else ifeq ($(ARCH),x86_64) + TARGET_TRIPLE := x86_64-linux-gnu + CFLAGS_ARCH := -march=x86-64 -mtune=generic +else +$(error Unsupported ARCH) +endif + +ifeq ($(strip $(LLVM)),True) + CC := clang -target $(TARGET_TRIPLE) + AS := clang -target $(TARGET_TRIPLE) + LD := ld.lld +else + CC := $(TARGET_TRIPLE)-gcc + LD := $(TARGET_TRIPLE)-ld + AS := $(TARGET_TRIPLE)-as +endif + +MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit + +IMAGES := cap_sharing.elf secondary.elf +CFLAGS := -nostdlib -ffreestanding -g -O3 -Wall -Wno-unused-function -Werror -I$(BOARD_DIR)/include $(CFLAGS_ARCH) +LDFLAGS := -L$(BOARD_DIR)/lib +LIBS := -lmicrokit -Tmicrokit.ld + +IMAGE_FILE = $(BUILD_DIR)/loader.img +REPORT_FILE = $(BUILD_DIR)/report.txt + +all: $(IMAGE_FILE) + +$(BUILD_DIR): + mkdir -p $@ + +$(BUILD_DIR)/%.o: %.c Makefile | $(BUILD_DIR) + $(CC) -c $(CFLAGS) $< -o $@ + +$(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) diff --git a/example/cap_sharing/README.md b/example/cap_sharing/README.md new file mode 100644 index 000000000..e3251ee29 --- /dev/null +++ b/example/cap_sharing/README.md @@ -0,0 +1,44 @@ + +# Example - Cap Sharing + +This is a basic example that demonstrates how one can use the `` element +of a PD to give delegated access of specific capabilities associated with other +(or its own) protection domain. + +See `cap_sharing.system` for some comments on the internal setup of this system. +The idea behind this example is that we have two PDs, one of which has control +over the TCB and scheduling context of the other; this could be the basis of +(e.g.) a user space scheduler. + +All supported platforms are supported in this example. + +## Building + +```sh +mkdir build +make BUILD_DIR=build MICROKIT_BOARD= MICROKIT_CONFIG= MICROKIT_SDK=/path/to/sdk +``` + +## Running + +See instructions for your board in the manual. + +You should see the following output: + +``` +INFO [sel4_capdl_initializer::initialize] Starting CapDL initializer +INFO [sel4_capdl_initializer::initialize] Starting threads +MON|INFO: Microkit Monitor started! +|secondary| hello, world +|primary | hello, world +|primary | notifying secondary +|secondary| notified +|primary | suspending secondary +|primary | notifying secondary (it should not print) +|primary | resuming secondary (it should then print) +|secondary| notified +|primary | halting (success)... +``` diff --git a/example/cap_sharing/cap_sharing.c b/example/cap_sharing/cap_sharing.c new file mode 100644 index 000000000..b45bd43ba --- /dev/null +++ b/example/cap_sharing/cap_sharing.c @@ -0,0 +1,63 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include + +#define CH_SECONDARY ((microkit_channel)0) + +// As per cap_sharing.system +#define CAP_SECONDARY_SC (microkit_cspace_slot_to_cptr(1)) +#define CAP_SECONDARY_TCB (microkit_cspace_slot_to_cptr(2)) +#define CAP_MY_SC (microkit_cspace_slot_to_cptr(3)) +#define CAP_MY_TCB (microkit_cspace_slot_to_cptr(4)) + +static void halt(void) +{ + seL4_Error error = seL4_TCB_Suspend(CAP_MY_TCB); + if (error != seL4_NoError) { + microkit_dbg_puts("|primary | error suspending TCB\n"); + } + + microkit_dbg_puts("|primary | error: should not reach this point! we should have suspended ourself!\n"); + while (1) { } +} + +void init(void) +{ + seL4_Error err; + + microkit_dbg_puts("|primary | hello, world\n"); + + /* Notify the secondary. This will print output from secondary as it is + higher priority. */ + microkit_dbg_puts("|primary | notifying secondary\n"); + microkit_notify(CH_SECONDARY); + + microkit_dbg_puts("|primary | suspending secondary\n"); + err = seL4_TCB_Suspend(CAP_SECONDARY_TCB); + if (err != seL4_NoError) { + microkit_dbg_puts("|primary | error suspending TCB\n"); + halt(); + } + + /* Notify the secondary. It is suspended so it will not print. */ + microkit_dbg_puts("|primary | notifying secondary (it should not print)\n"); + microkit_notify(CH_SECONDARY); + + microkit_dbg_puts("|primary | resuming secondary (it should then print)\n"); + err = seL4_TCB_Resume(CAP_SECONDARY_TCB); + if (err != seL4_NoError) { + microkit_dbg_puts("|primary | error resuming TCB\n"); + halt(); + } + + microkit_dbg_puts("|primary | halting (success)...\n"); + halt(); +} + +void notified(microkit_channel ch) +{ +} diff --git a/example/cap_sharing/cap_sharing.system b/example/cap_sharing/cap_sharing.system new file mode 100644 index 000000000..3f18d6fa1 --- /dev/null +++ b/example/cap_sharing/cap_sharing.system @@ -0,0 +1,30 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/example/cap_sharing/secondary.c b/example/cap_sharing/secondary.c new file mode 100644 index 000000000..1eb341817 --- /dev/null +++ b/example/cap_sharing/secondary.c @@ -0,0 +1,18 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include + +void init(void) +{ + microkit_dbg_puts("|secondary| hello, world\n"); +} + +void notified(microkit_channel ch) +{ + microkit_dbg_puts("|secondary| notified\n"); + microkit_notify(ch); +} diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 90155d21e..ad9616105 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -28,7 +28,9 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define BASE_VM_TCB_CAP 266 #define BASE_VCPU_CAP 330 #define BASE_IOPORT_CAP 394 +#define BASE_USER_CAPS 458 +#define MICROKIT_MAX_USER_CAPS 128 #define MICROKIT_MAX_CHANNELS 62 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1) #define MICROKIT_MAX_IOPORT_ID MICROKIT_MAX_CHANNELS @@ -506,3 +508,19 @@ static inline void microkit_deferred_irq_ack(microkit_channel ch) microkit_signal_msg = seL4_MessageInfo_new(IRQAckIRQ, 0, 0, 0); microkit_signal_cap = (BASE_IRQ_CAP + ch); } + +/** + * Convert the "slot" identifier from the system file for the extra user caps + * element into the seL4_CPtr at runtime. + * + * If the slot exceeds the valid range of inputs (0 <= slot < MICROKIT_MAX_USER_CAPS), + * it returns the value `seL4_CapNull`. + **/ +static inline seL4_CPtr microkit_cspace_slot_to_cptr(seL4_Word slot) +{ + if (slot > MICROKIT_MAX_USER_CAPS) { + return seL4_CapNull; + } + + return BASE_USER_CAPS + slot; +} diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 8c6acd210..5bb401be0 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}, @@ -95,8 +95,14 @@ 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; - -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; @@ -112,6 +118,15 @@ pub struct ExpectedAllocation { pub paddr: u64, } +struct PDShadowCspace { + cspace: ObjectId, + notification: ObjectId, + endpoint: Option, + sched_context: ObjectId, + tcb: ObjectId, + vspace: ObjectId, +} + pub struct CapDLSpecContainer { pub spec: Spec, /// Track allocations as we build the system for later use by the report. @@ -573,10 +588,9 @@ pub fn build_capdl_spec( None }; - // 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(); + // This object keeps track of object IDs for various 'important' / nameable kernel objects for + // each PD so that we can make various references to them at later steps. + let mut pd_shadow_cspaces: 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. @@ -694,18 +708,21 @@ pub fn build_capdl_spec( )); // Step 3-5 Create fault Endpoint cap to parent/monitor - let pd_fault_ep_cap = if let Some(pd_parent) = pd.parent { - assert!(pd_global_idx > pd_parent); + 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(); - let parent_ep_obj_id = &pd_id_to_ep_id[&pd_parent]; + let parent_shadow_cspace = &pd_shadow_cspaces[&pd_parent_id]; + let parent_ep_obj_id = parent_shadow_cspace + .endpoint + .expect("parent should have EP due to needs_ep()"); let fault_ep_cap = - capdl_util_make_endpoint_cap(*parent_ep_obj_id, true, true, true, badge); + capdl_util_make_endpoint_cap(parent_ep_obj_id, true, true, true, badge); // Allow the parent PD to access the child's TCB: - let parent_cspace_obj_id = &pd_id_to_cspace_id[&pd_parent]; + let parent_cspace_obj_id = parent_shadow_cspace.cspace; capdl_util_insert_cap_into_cspace( &mut spec_container, - *parent_cspace_obj_id, + parent_cspace_obj_id, (PD_BASE_PD_TCB_CAP + pd.id.unwrap()) as u32, capdl_util_make_tcb_cap(pd_tcb_obj_id), ); @@ -744,7 +761,6 @@ pub fn build_capdl_spec( 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; - pd_id_to_ntfn_id.insert(pd_global_idx, pd_ntfn_obj_id); if pd.needs_ep(pd_global_idx, &system.channels) { pd_ep_obj_id = Some(capdl_util_make_endpoint_obj( &mut spec_container, @@ -753,7 +769,6 @@ pub fn build_capdl_spec( )); let pd_ep_cap = capdl_util_make_endpoint_cap(pd_ep_obj_id.unwrap(), true, true, true, 0); - pd_id_to_ep_id.insert(pd_global_idx, pd_ep_obj_id.unwrap()); caps_to_insert_to_pd_cspace .push(capdl_util_make_cte(PD_INPUT_CAP_IDX as u32, pd_ep_cap)); } else { @@ -1005,7 +1020,6 @@ pub fn build_capdl_spec( TcbBoundSlot::CSpace as u32, pd_cnode_cap, )); - pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id); // Step 3-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 @@ -1052,16 +1066,28 @@ pub fn build_capdl_spec( capdl_util_make_ntfn_cap(pd_ntfn_obj_id, true, true, 0), ); } + + pd_shadow_cspaces.insert( + pd_global_idx, + PDShadowCspace { + cspace: pd_cnode_obj_id, + endpoint: pd_ep_obj_id, + notification: pd_ntfn_obj_id, + sched_context: pd_sc_obj_id, + vspace: pd_vspace_obj_id, + tcb: pd_tcb_obj_id, + }, + ); } // ********************************* // Step 4. Create channels // ********************************* for channel in system.channels.iter() { - let pd_a_cspace_id = pd_id_to_cspace_id[&channel.end_a.pd]; - let pd_b_cspace_id = pd_id_to_cspace_id[&channel.end_b.pd]; - let pd_a_ntfn_id = pd_id_to_ntfn_id[&channel.end_a.pd]; - let pd_b_ntfn_id = pd_id_to_ntfn_id[&channel.end_b.pd]; + 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_ntfn_id = pd_shadow_cspaces[&channel.end_a.pd].notification; + let pd_b_ntfn_id = pd_shadow_cspaces[&channel.end_b.pd].notification; // We trust that the SDF parsing code have checked for duplicate IDs. if channel.end_a.notify { @@ -1091,7 +1117,9 @@ pub fn build_capdl_spec( if channel.end_a.pp { let pd_a_ep_cap_idx = PD_BASE_OUTPUT_ENDPOINT_CAP + channel.end_a.id; let pd_a_ep_badge = PPC_BADGE | channel.end_b.id; - let pd_b_ep_id = pd_id_to_ep_id[&channel.end_b.pd]; + let pd_b_ep_id = pd_shadow_cspaces[&channel.end_b.pd] + .endpoint + .expect("exists as needs_ep() is true"); let pd_a_ep_cap = capdl_util_make_endpoint_cap(pd_b_ep_id, true, true, true, pd_a_ep_badge); capdl_util_insert_cap_into_cspace( @@ -1105,7 +1133,9 @@ pub fn build_capdl_spec( if channel.end_b.pp { let pd_b_ep_cap_idx = PD_BASE_OUTPUT_ENDPOINT_CAP + channel.end_b.id; let pd_b_ep_badge = PPC_BADGE | channel.end_a.id; - let pd_a_ep_id = pd_id_to_ep_id[&channel.end_a.pd]; + let pd_a_ep_id = pd_shadow_cspaces[&channel.end_a.pd] + .endpoint + .expect("exists as needs_ep() is true"); let pd_b_ep_cap = capdl_util_make_endpoint_cap(pd_a_ep_id, true, true, true, pd_b_ep_badge); capdl_util_insert_cap_into_cspace( @@ -1118,7 +1148,36 @@ 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_shadow_cspaces[&pd_dest_idx].cspace; + + 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()]; + + 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, + (PD_BASE_USER_CAPS + cap_map.slot) as u32, + cap_map_obj, + ); + } + } + + // ********************************* + // 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 56901164a..365650100 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -21,7 +21,7 @@ use crate::sel4::{ }; use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool}; use crate::MAX_PDS; -use std::collections::HashSet; +use std::collections::{HashMap, HashSet}; use std::fmt::Display; use std::fs; use std::path::{Path, PathBuf}; @@ -38,6 +38,10 @@ use std::path::{Path, PathBuf}; const PD_MAX_ID: u64 = 61; const VCPU_MAX_ID: u64 = PD_MAX_ID; +/// This is the maximum slot allowed for cap maps. This can change if you wish, +/// but also update the MICROKIT_MAX_USER_CAPS define in `microkit.h`. +const CAP_MAP_MAX_SLOT: u64 = 128; + pub const MONITOR_PRIORITY: u8 = 255; const PD_MAX_PRIORITY: u8 = 254; /// In microseconds @@ -277,6 +281,7 @@ pub struct ProtectionDomain { pub irqs: Vec, pub ioports: Vec, pub setvars: 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. @@ -291,6 +296,39 @@ pub struct ProtectionDomain { text_pos: Option, } +#[derive(Debug, PartialEq, Eq, Copy, Clone, Hash)] +pub enum CapMapType { + Tcb, + Sc, + VSpace, + CSpace, +} + +#[derive(Debug, PartialEq, Eq)] +pub struct CapMap { + pub cap_type: CapMapType, + // FIXME: This is quite a hack. Basically, we need to be able to reference + // arbitrary PDs, but to gather the index, we need to know all the PDs. + // However, at the time of parsing the cap maps, we are in the process + // of parsing all the PDs. In lieu of something better (in my - @midnightveil's + // 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: 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. + pub slot: u64, + /// Location in the parsed SDF file + text_pos: roxmltree::TextPos, +} + +#[derive(Debug)] +pub struct CSpace { + cap_maps: Vec, +} + #[derive(Debug, PartialEq, Eq)] pub struct VirtualMachine { pub vcpus: Vec, @@ -610,6 +648,7 @@ impl ProtectionDomain { let mut program_image = None; let mut program_image_for_symbols = None; let mut virtual_machine = None; + let mut cspace = None; // Default to minimum priority let priority = if let Some(xml_priority) = node.attribute("priority") { @@ -1128,6 +1167,17 @@ impl ProtectionDomain { virtual_machine = Some(vm); } + "cspace" => { + if cspace.is_some() { + return Err(value_error( + xml_sdf, + node, + "cspace must only be specified once".to_string(), + )); + } + + cspace = Some(CSpace::from_xml(xml_sdf, &child)?); + } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!( @@ -1166,6 +1216,7 @@ impl ProtectionDomain { irqs, ioports, setvars, + cap_maps: cspace.map(|cspace| cspace.cap_maps).unwrap_or_default(), child_pds, virtual_machine, has_children, @@ -1306,6 +1357,68 @@ impl VirtualMachine { } } +impl CapMap { + fn from_xml( + cap_type: CapMapType, + 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"])?; + + let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string(); + + let slot = sdf_parse_number(checked_lookup(xml_sdf, node, "slot")?, node)?; + + // TODO: Rework this so that we don't have a fixed upper limit. + if slot >= CAP_MAP_MAX_SLOT { + return Err(value_error( + xml_sdf, + node, + format!("There are only {CAP_MAP_MAX_SLOT} destination cspace slots available."), + )); + } + + Ok(CapMap { + cap_type, + pd_name, + // FIXME: Hack, filled out later. + pd: None, + slot, + text_pos: xml_sdf.doc.text_pos_at(node.range().start), + }) + } +} + +impl CSpace { + fn from_xml(xml_sdf: &XmlSystemDescription, node: &roxmltree::Node) -> Result { + check_attributes(xml_sdf, node, &[])?; + + let mut cap_maps = vec![]; + + for child in node.children().filter(|c| c.is_element()) { + cap_maps.push(match child.tag_name().name() { + "cap_tcb" => CapMap::from_xml(CapMapType::Tcb, xml_sdf, &child)?, + "cap_sc" => CapMap::from_xml(CapMapType::Sc, xml_sdf, &child)?, + "cap_vspace" => CapMap::from_xml(CapMapType::VSpace, xml_sdf, &child)?, + "cap_cspace" => CapMap::from_xml(CapMapType::CSpace, xml_sdf, &child)?, + child_name => { + let location = loc_string(xml_sdf, xml_sdf.doc.text_pos_at(child.range().start)); + if let Some(type_name) = child_name.strip_prefix("cap_") { + return Err(format!("Cap type: '{type_name}' is not supported at '{location}'")); + } else { + return Err(format!("Element '{child_name}' is not supported in a element at '{location}'")); + } + } + }) + } + + Ok(CSpace { cap_maps }) + } +} + impl SysMemoryRegion { fn determine_size( xml_sdf: &XmlSystemDescription, @@ -1815,7 +1928,6 @@ pub fn parse( let mut root_pds = vec![]; let mut mrs = vec![]; let mut channels = vec![]; - let system = doc .root() .children() @@ -1889,6 +2001,27 @@ pub fn parse( channels.push(ch); } + // FIXME: Now we post-fill the PD ids in the capmap elements, which is + // ugly, and we should rework this to be less so. + let pd_names_to_id: HashMap<_, _> = pds + .iter() + .enumerate() + .map(|(idx, pd)| (pd.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) + )); + }; + + cap_map.pd = Some(pd); + } + } + // Now that we have parsed everything in the system description we can validate any // global properties (e.g no duplicate PD names etc). @@ -2080,6 +2213,37 @@ pub fn parse( } } + // Ensure that there are no overlapping extra cap maps in the user caps region + // and we are not mapping in the same cap from the same source more than once + for pd in &pds { + let mut user_cap_slots = HashMap::>::new(); + + for cap_map in &pd.cap_maps { + user_cap_slots + .entry(cap_map.slot) + .and_modify(|v| v.push(cap_map)) + .or_insert(vec![cap_map]); + } + + for (slot, cap_maps) in user_cap_slots.iter() { + 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) + )); + } + return Err(format!( + "Error: overlapping user caps in slot {slot} of protection domain '{}':{}", + pd.name, lines + )); + } + } + } + // Ensure MRs with physical addresses do not overlap let mut checked_mrs = Vec::with_capacity(mrs.len()); for mr in &mrs { diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_invalid.system b/tool/microkit/tests/sdf/pd_cap_mappings_invalid.system new file mode 100644 index 000000000..adbeda42c --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_invalid.system @@ -0,0 +1,19 @@ + + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_invalid_pd_ref.system b/tool/microkit/tests/sdf/pd_cap_mappings_invalid_pd_ref.system new file mode 100644 index 000000000..dfd085af6 --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_invalid_pd_ref.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_overlapping.system b/tool/microkit/tests/sdf/pd_cap_mappings_overlapping.system new file mode 100644 index 000000000..dc48b056b --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_overlapping.system @@ -0,0 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 056a32368..4a25465b3 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -996,4 +996,33 @@ mod system { "Error: fpu must be 'true' or 'false'", ) } + + #[test] + fn test_cap_mappings_overlapping() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_cap_mappings_overlapping.system", + r#"Error: overlapping user caps in slot 4 of protection domain 'pd_b': + type CSpace from 'pd_a' at 'pd_cap_mappings_overlapping.system:24:13' + type CSpace from 'pd_a' at 'pd_cap_mappings_overlapping.system:26:13'"#, + ) + } + + #[test] + fn test_cap_mappings_invalid() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_cap_mappings_invalid.system", + "Cap type: 'gerbils' is not supported at 'pd_cap_mappings_invalid.system:16:13'", + ) + } + + #[test] + fn test_cap_mappings_invalid_pd_ref() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_cap_mappings_invalid_pd_ref.system", + "Error: unknown PD name 'invalid': pd_cap_mappings_invalid_pd_ref.system:12:13", + ) + } }