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 <c.berry@student.unsw.edu.au>

Author: cazb2

Cargo.lock

@@ -959,7 +959,8 @@ Stop the PD from switching to guest execution mode when a Microkit entrypoint re
 Converts the slot identifier of the `<cspace>`'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 `<cspace>`.
 
 # System Description File {#sysdesc}
 

docs/manual.md

@@ -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
  * <cspace> 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);
 }

libmicrokit/include/microkit.h

@@ -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)

libmicrokit/src/main.c

@@ -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()];

tool/microkit/src/capdl/builder.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<SysIrq>,
     pub ioports: Vec<IOPort>,
     pub setvars: Vec<SysSetVar>,
-    pub cap_maps: Vec<CapMap>,
+    pub cspace: Option<CSpace>,
     pub virtual_machine: Option<VirtualMachine>,
     /// 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<CapMap>,
+    pub cap_maps: Vec<CapMap>,
+    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::<u64, Vec<_>>::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))

tool/microkit/src/sdf.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

tool/microkit/src/symbols.rs

@@ -73,6 +73,16 @@ pub fn ranges_overlap<T: PartialOrd>(left: &Range<T>, right: &Range<T>) -> bool
     !(left.end <= right.start || right.end <= left.start)
 }
 
+/// Returns the number of bits required to repr the input
+pub fn calculate_size_bits<T: Into<u64>>(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.