From b1eda3907ceba76198ffd0a22f7f22931e74ebfc Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 23 Jul 2026 12:04:31 +1000 Subject: [PATCH] CapMap: Remove the root cnode upper bound This commit determines the size of the root cnode based upon the largest slot number that is specified in the sdf. Signed-off-by: Callum --- Cargo.lock | 4 +-- docs/manual.md | 3 ++- libmicrokit/include/microkit.h | 11 +++----- libmicrokit/src/main.c | 1 + tool/microkit/src/capdl/builder.rs | 16 ++++++----- tool/microkit/src/sdf.rs | 43 +++++++++++++++--------------- tool/microkit/src/symbols.rs | 10 +++++++ tool/microkit/src/util.rs | 10 +++++++ 8 files changed, 60 insertions(+), 38 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 05b6a61e9..67bd2d7ad 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -135,7 +135,7 @@ checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" [[package]] name = "initialiser" -version = "2.3.0" +version = "2.3.0-dev" dependencies = [ "sel4-capdl-initializer", ] @@ -194,7 +194,7 @@ checksum = "88904434abc2901f197fe8cc55f0445e7ded921dba5911dad2e2b39b48e663c4" [[package]] name = "microkit-tool" -version = "2.3.0" +version = "2.3.0-dev" dependencies = [ "rkyv", "roxmltree", diff --git a/docs/manual.md b/docs/manual.md index 4f757103c..b22813eea 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -959,7 +959,8 @@ Stop the PD from switching to guest execution mode when a Microkit entrypoint re 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`. +If the slot is not in the valid range of inputs (`0 < slot < microkit_root_cnode_size_bits`), it returns the value `seL4_CapNull`. +The value of `microkit_root_cnode_size_bits` is determined based on the largest slot specified in the ``. # System Description File {#sysdesc} diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index b31391aeb..259f271da 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -33,10 +33,6 @@ 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) @@ -70,6 +66,7 @@ extern seL4_Word microkit_irqs; extern seL4_Word microkit_notifications; extern seL4_Word microkit_pps; extern seL4_Word microkit_ioports; +extern seL4_Word microkit_root_cnode_size_bits; /* * Output a single character on the debug console. @@ -607,14 +604,14 @@ static inline void microkit_deferred_irq_ack(microkit_channel 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), + * If the slot is not in the valid range of inputs (0 < slot < microkit_root_cnode_size_bits), * it returns the value `seL4_CapNull`. **/ static inline seL4_CPtr microkit_cspace_root_slot_to_cptr(seL4_Word slot) { - if (slot == 0 || slot >= PD_ROOT_CAP_SIZE) { + if (slot == 0 || slot >= (1ULL << microkit_root_cnode_size_bits)) { return seL4_CapNull; } - return slot << (seL4_WordBits - PD_ROOT_CAP_BITS); + return slot << (seL4_WordBits - microkit_root_cnode_size_bits); } diff --git a/libmicrokit/src/main.c b/libmicrokit/src/main.c index f5d3bd02e..bdb6e8147 100644 --- a/libmicrokit/src/main.c +++ b/libmicrokit/src/main.c @@ -38,6 +38,7 @@ seL4_Word microkit_irqs; seL4_Word microkit_notifications; seL4_Word microkit_pps; seL4_Word microkit_ioports; +seL4_Word microkit_root_cnode_size_bits; #define BIT(n) (1ULL << (n)) #define MASK(n) (BIT(n) - 1ULL) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 612c1d499..f878e73d0 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -93,9 +93,6 @@ 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; -/* 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; @@ -1065,14 +1062,20 @@ pub fn build_capdl_spec( PD_CAP_BITS, caps_to_insert_to_pd_cspace, ); + + let root_cnode_size_bits = match &pd.cspace { + Some(cspace) => cspace.size_bits, + None => 1, + } as u8; + let pd_guard_size = - kernel_config.cap_address_bits - PD_CAP_BITS as u64 - PD_ROOT_CAP_BITS as u64; + kernel_config.cap_address_bits - PD_CAP_BITS as u64 - root_cnode_size_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, + root_cnode_size_bits, Vec::new(), ); // leave the guard size root cnode as 0 @@ -1256,7 +1259,8 @@ pub fn build_capdl_spec( // Step 6. Handle extra cap mappings // ********************************* for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() { - for cap_map in pd.cap_maps.iter() { + let Some(cspace) = &pd.cspace else { continue }; + for cap_map in cspace.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()]; diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index ca0e2dd1a..1920f2fc0 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -20,7 +20,7 @@ use crate::sel4::{ Arch, ArmRiscvIrqTrigger, Config, PageSize, X86IoapicIrqPolarity, X86IoapicIrqTrigger, }; -use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool}; +use crate::util::{calculate_size_bits, get_full_path, ranges_overlap, round_up, str_to_bool}; use crate::MAX_PDS; use sel4_capdl_initializer_types::{ object, x86_io_address_space, DomainSchedDuration, DomainSchedEntry, FillEntryContentBootInfoId, @@ -45,10 +45,6 @@ use std::str::FromStr; 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 @@ -613,7 +609,7 @@ pub struct ProtectionDomain { pub irqs: Vec, pub ioports: Vec, pub setvars: Vec, - pub cap_maps: Vec, + pub cspace: Option, 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. @@ -655,9 +651,10 @@ pub struct CapMap { text_pos: roxmltree::TextPos, } -#[derive(Debug)] +#[derive(Debug, PartialEq, Eq)] pub struct CSpace { - cap_maps: Vec, + pub cap_maps: Vec, + pub size_bits: u64, } #[derive(Debug, PartialEq, Eq)] @@ -1604,7 +1601,7 @@ impl ProtectionDomain { irqs, ioports, setvars, - cap_maps: cspace.map(|cspace| cspace.cap_maps).unwrap_or_default(), + cspace, child_pds, virtual_machine, has_children, @@ -1781,15 +1778,6 @@ impl CapMap { )); } - // 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, @@ -1823,7 +1811,17 @@ impl CSpace { }) } - Ok(CSpace { cap_maps }) + // Default to 1, the minimum allowed by the kernel. + let size_bits = cap_maps + .iter() + .map(|cap_map| calculate_size_bits(cap_map.slot + 1)) + .max() + .unwrap_or(1) as u64; + + Ok(CSpace { + cap_maps, + size_bits, + }) } } @@ -2873,8 +2871,8 @@ pub fn parse( .enumerate() .map(|(idx, pd)| (pd.name.clone(), idx)) .collect(); - for pd in pds.iter_mut() { - for cap_map in pd.cap_maps.iter_mut() { + for cspace in pds.iter_mut().filter_map(|pd| pd.cspace.as_mut()) { + for cap_map in cspace.cap_maps.iter_mut() { let Some(&pd) = pd_names_to_id.get(&cap_map.pd_name) else { return Err(format!( "Error: unknown PD name '{}': {}", @@ -3128,9 +3126,10 @@ 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 Some(cspace) = &pd.cspace else { continue }; let mut user_cap_slots = HashMap::>::new(); - for cap_map in &pd.cap_maps { + for cap_map in &cspace.cap_maps { user_cap_slots .entry(cap_map.slot) .and_modify(|v| v.push(cap_map)) diff --git a/tool/microkit/src/symbols.rs b/tool/microkit/src/symbols.rs index 477ef5c7b..03fd19a95 100644 --- a/tool/microkit/src/symbols.rs +++ b/tool/microkit/src/symbols.rs @@ -135,6 +135,16 @@ pub fn patch_symbols( .write_symbol("microkit_ioports", &pd.ioport_bits().to_le_bytes()) .unwrap(); + elf_obj + .write_symbol( + "microkit_root_cnode_size_bits", + &pd.cspace + .as_ref() + .map_or(0u64, |cspace| cspace.size_bits) + .to_le_bytes(), + ) + .unwrap(); + let mut symbols_to_write: Vec<(&String, u64)> = Vec::new(); for setvar in pd.setvars.iter() { // Check that the symbol exists in the ELF diff --git a/tool/microkit/src/util.rs b/tool/microkit/src/util.rs index 6f2c0e275..e35351313 100644 --- a/tool/microkit/src/util.rs +++ b/tool/microkit/src/util.rs @@ -73,6 +73,16 @@ pub fn ranges_overlap(left: &Range, right: &Range) -> bool !(left.end <= right.start || right.end <= left.start) } +/// Returns the number of bits required to repr the input +pub fn calculate_size_bits>(size: T) -> u8 { + let size: u64 = size.into(); + if size <= 1 { + 0 + } else { + (size - 1).ilog2() as u8 + 1 + } +} + /// Product a 'human readable' string for the size. /// /// 'strict' means that it must be simply represented.