From b1eda3907ceba76198ffd0a22f7f22931e74ebfc Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 23 Jul 2026 12:04:31 +1000 Subject: [PATCH 1/4] 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. From c53eaaa45d73af136431e435ac143cf02656735f Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 23 Jul 2026 14:31:58 +1000 Subject: [PATCH 2/4] MapPerms: Consistency between map and iomap This commit unifies the way VM rights are encoded in the sdf. Previously normal map perms were represented as a raw u8 while the iomap perms were represented as a proper type. Preserves existing behaviour. Signed-off-by: Callum --- tool/microkit/src/sdf.rs | 133 +++++++++++++++++++++++++------------ tool/microkit/src/viper.rs | 3 +- 2 files changed, 92 insertions(+), 44 deletions(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 1920f2fc0..79d659ebb 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -262,26 +262,45 @@ impl fmt::Display for IommuDeviceIdentifierParseError { } } -#[repr(u8)] -pub enum SysMapPerms { - Read = 1, - Write = 2, - Execute = 4, +#[derive(Debug, PartialEq, Eq, Clone, Copy)] +pub struct SysMapPerms { + rights: FrameRights, + execute: bool, +} + +pub enum SysMapPermsParseError { + InvalidChar, + WriteOnly, } impl SysMapPerms { - fn from_str(s: &str) -> Result { - let mut perms = 0; + fn from_str(s: &str) -> Result { + let mut read = false; + let mut write = false; + let mut execute = false; for c in s.chars() { match c { - 'r' => perms |= SysMapPerms::Read as u8, - 'w' => perms |= SysMapPerms::Write as u8, - 'x' => perms |= SysMapPerms::Execute as u8, - _ => return Err(()), + 'r' => read = true, + 'w' => write = true, + 'x' => execute = true, + _ => return Err(SysMapPermsParseError::InvalidChar), } } + let rights = match FrameRights::from_bools(read, write) { + FrameRights::Write => return Err(SysMapPermsParseError::WriteOnly), + frame_rights => frame_rights, + }; - Ok(perms) + Ok(Self { rights, execute }) + } + pub fn read(self) -> bool { + self.rights.read() + } + pub fn write(self) -> bool { + self.rights.write() + } + pub fn execute(self) -> bool { + self.execute } } @@ -289,22 +308,44 @@ impl SysMapPerms { pub struct SysMap { pub mr: String, pub vaddr: u64, - pub perms: u8, + pub perms: SysMapPerms, pub cached: bool, /// Location in the parsed SDF file. Because this struct is /// used in a non-XML context, we make the position optional. pub text_pos: Option, } +// We do not include attributes (execute/cached) here since seL4 does not treat them like vm_rights. #[derive(Debug, PartialEq, Eq, Clone, Copy)] -pub enum SysIOMapPerms { +pub enum FrameRights { Read, Write, ReadWrite, + None, } +impl FrameRights { + fn from_bools(read: bool, write: bool) -> Self { + match (read, write) { + (true, false) => Self::Read, + (false, true) => Self::Write, + (true, true) => Self::ReadWrite, + (false, false) => Self::None, + } + } + pub fn read(self) -> bool { + matches!(self, Self::Read | Self::ReadWrite) + } + pub fn write(self) -> bool { + matches!(self, Self::Write | Self::ReadWrite) + } +} + +#[derive(Debug, PartialEq, Eq, Clone, Copy)] +pub struct SysIOMapPerms(FrameRights); + impl SysIOMapPerms { - fn from_str(s: &str) -> Result { + fn from_str(s: &str) -> Result { let mut read = false; let mut write = false; @@ -312,16 +353,23 @@ impl SysIOMapPerms { match c { 'r' => read = true, 'w' => write = true, - _ => return Err(()), + _ => return Err(format!("Invalid character in string {s}")), } } - - match (read, write) { - (true, true) => Ok(SysIOMapPerms::ReadWrite), - (true, false) => Ok(SysIOMapPerms::Read), - (false, true) => Ok(SysIOMapPerms::Write), - (false, false) => Err(()), - } + let frame_rights = match FrameRights::from_bools(read, write) { + FrameRights::None => return Err("Invalid frame right for IOMap".into()), + frame_rights => frame_rights, + }; + Ok(SysIOMapPerms(frame_rights)) + } + pub fn read(self) -> bool { + self.0.read() + } + pub fn write(self) -> bool { + self.0.write() + } + pub fn execute(self) -> bool { + false } } @@ -375,15 +423,15 @@ impl Map for SysMap { } fn read(&self) -> bool { - self.perms & SysMapPerms::Read as u8 != 0 + self.perms.read() } fn write(&self) -> bool { - self.perms & SysMapPerms::Write as u8 != 0 + self.perms.write() } fn execute(&self) -> bool { - self.perms & SysMapPerms::Execute as u8 != 0 + self.perms.execute() } fn cached(&self) -> bool { @@ -417,15 +465,15 @@ impl Map for SysIOMap { } fn read(&self) -> bool { - matches!(self.perms, SysIOMapPerms::Read | SysIOMapPerms::ReadWrite) + self.perms.read() } fn write(&self) -> bool { - matches!(self.perms, SysIOMapPerms::Write | SysIOMapPerms::ReadWrite) + self.perms.write() } fn execute(&self) -> bool { - false + self.perms.execute() } fn cached(&self) -> bool { @@ -701,7 +749,14 @@ impl SysMap { let perms = if let Some(xml_perms) = node.attribute("perms") { match SysMapPerms::from_str(xml_perms) { Ok(parsed_perms) => parsed_perms, - Err(()) => { + Err(SysMapPermsParseError::WriteOnly) => { + return Err(value_error( + xml_sdf, + node, + "perms must not be 'w', write-only mappings are not allowed".to_string(), + )); + } + Err(_) => { return Err(value_error( xml_sdf, node, @@ -711,18 +766,12 @@ impl SysMap { } } else { // Default to read-write - SysMapPerms::Read as u8 | SysMapPerms::Write as u8 + SysMapPerms { + rights: FrameRights::ReadWrite, + execute: false, + } }; - // On all architectures, the kernel does not allow write-only mappings - if perms == SysMapPerms::Write as u8 { - return Err(value_error( - xml_sdf, - node, - "perms must not be 'w', write-only mappings are not allowed".to_string(), - )); - } - let cached = if let Some(xml_cached) = node.attribute("cached") { match str_to_bool(xml_cached) { Some(val) => val, @@ -779,7 +828,7 @@ impl SysIOMap { let perms = if let Some(xml_perms) = node.attribute("perms") { match SysIOMapPerms::from_str(xml_perms) { Ok(parsed_perms) => parsed_perms, - Err(()) => { + Err(_) => { return Err(value_error( xml_sdf, node, @@ -790,7 +839,7 @@ impl SysIOMap { } } else { // Default to read-write - SysIOMapPerms::ReadWrite + SysIOMapPerms(FrameRights::ReadWrite) }; Ok(SysIOMap { diff --git a/tool/microkit/src/viper.rs b/tool/microkit/src/viper.rs index 7a034aa23..78ce13ea6 100644 --- a/tool/microkit/src/viper.rs +++ b/tool/microkit/src/viper.rs @@ -6,7 +6,6 @@ use sel4_capdl_initializer_types::{Cap, Object}; use crate::capdl::CapDLSpecContainer; -use crate::sdf::SysMapPerms; use crate::sdf::SystemDescription; fn export_define_set(name: &'static str, vector: &[u64], target: &mut String) { @@ -312,7 +311,7 @@ pub fn get_mem_view(system: &SystemDescription, current_pd: usize) -> Option Date: Thu, 23 Jul 2026 23:38:35 +1000 Subject: [PATCH 3/4] WIP: Draft Memory Cap Impl --- docs/manual.md | 2 +- example/cap_sharing/Makefile | 3 + example/cap_sharing/cap_sharing.c | 199 ++++++++++++- example/cap_sharing/cap_sharing.system | 18 ++ libmicrokit/include/microkit.h | 141 ++++++++- libmicrokit/src/main.c | 3 + tool/microkit/src/capdl/builder.rs | 170 ++++++++++- tool/microkit/src/capdl/util.rs | 6 + tool/microkit/src/main.rs | 183 +++++++++++- tool/microkit/src/sdf.rs | 395 +++++++++++++++++++++---- tool/microkit/src/symbols.rs | 20 ++ 11 files changed, 1059 insertions(+), 81 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index b22813eea..46c5a37cd 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -959,7 +959,7 @@ 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 is not in the valid range of inputs (`0 < slot < microkit_root_cnode_size_bits`), it returns the value `seL4_CapNull`. +If the slot is not in the valid range of inputs (`0 < slot < (1 << microkit_max_user_caps_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/example/cap_sharing/Makefile b/example/cap_sharing/Makefile index 0901a34c9..d5fe648c7 100644 --- a/example/cap_sharing/Makefile +++ b/example/cap_sharing/Makefile @@ -75,9 +75,12 @@ $(IMAGE_FILE) $(KERNEL_32B) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES) ifeq ($(ARCH),x86_64) qemu: $(KERNEL_32B) $(IMAGE_FILE) qemu-system-x86_64 \ + -machine q35 \ -cpu qemu64,+fsgsbase,+pdpe1gb,+xsaveopt,+xsave \ -m "1G" \ -display none \ + -device intel-iommu,intremap=off,aw-bits=39 \ + -device edu,dma_mask=0xffffffffffffffff,bus=pcie.0,addr=0x04.0 \ -serial mon:stdio \ -kernel $(KERNEL_32B) \ -initrd $(IMAGE_FILE) diff --git a/example/cap_sharing/cap_sharing.c b/example/cap_sharing/cap_sharing.c index eefd16ffc..a6e6ced81 100644 --- a/example/cap_sharing/cap_sharing.c +++ b/example/cap_sharing/cap_sharing.c @@ -9,10 +9,36 @@ #define CH_SECONDARY ((microkit_channel)0) // As per cap_sharing.system -#define CAP_SECONDARY_SC (microkit_cspace_root_slot_to_cptr(1)) -#define CAP_SECONDARY_TCB (microkit_cspace_root_slot_to_cptr(2)) -#define CAP_MY_SC (microkit_cspace_root_slot_to_cptr(3)) -#define CAP_MY_TCB (microkit_cspace_root_slot_to_cptr(4)) +#define CAP_SECONDARY_SC (microkit_cspace_root_slot_to_cptr(1)) +#define CAP_SECONDARY_TCB (microkit_cspace_root_slot_to_cptr(2)) +#define CAP_MY_SC (microkit_cspace_root_slot_to_cptr(3)) +#define CAP_MY_TCB (microkit_cspace_root_slot_to_cptr(4)) +#define CAP_MY_VSPACE (microkit_cspace_root_slot_to_cptr(5)) +#define CAP_MR (microkit_cspace_root_slot_to_cptr(6)) +#define CAP_IOSPACE (microkit_cspace_root_slot_to_cptr(7)) +#define CAP_SECONDARY_STACK (microkit_cspace_root_slot_to_cptr(9)) +#define CAP_SECONDARY_IPCBUF (microkit_cspace_root_slot_to_cptr(10)) +#define CAP_SECONDARY_ELF (microkit_cspace_root_slot_to_cptr(11)) + +#define SLOT_SECONDARY_STACK 9 +#define SLOT_SECONDARY_IPCBUF 10 +#define SLOT_SECONDARY_ELF 11 + +#define MR_SIZE 0xa000 +#define MR_PAGE_SIZE 0x1000 +#define DMA_BUFFER_VADDR 0x10001000 +#define IOVA 0x100000 +#define RUNTIME_IOVA (IOVA + MR_SIZE) + +#if defined(CONFIG_ARCH_X86_64) +#define MICROKIT_EXAMPLE_DEFAULT_VM_ATTRIBUTES seL4_X86_Default_VMAttributes +#elif defined(CONFIG_ARCH_AARCH64) +#define MICROKIT_EXAMPLE_DEFAULT_VM_ATTRIBUTES seL4_ARM_Default_VMAttributes +#elif defined(CONFIG_ARCH_RISCV) +#define MICROKIT_EXAMPLE_DEFAULT_VM_ATTRIBUTES seL4_RISCV_Default_VMAttributes +#else +#error "Unsupported architecture" +#endif static void halt(void) { @@ -25,12 +51,177 @@ static void halt(void) while (1) { } } +static void put_hex64(seL4_Word value) +{ + static const char hex[] = "0123456789abcdef"; + + microkit_dbg_puts("0x"); + for (int i = 15; i >= 0; i--) { + microkit_dbg_putc(hex[(value >> (i * 4)) & 0xf]); + } +} + +static void check_cap(const char *name, seL4_CPtr cap) +{ + if (cap == seL4_CapNull) { + microkit_dbg_puts("|primary | missing cap: "); + microkit_dbg_puts(name); + microkit_dbg_puts("\n"); + halt(); + } +} + +static void print_frame_info(const char *name, seL4_CPtr cap, seL4_Word vaddr) +{ + seL4_Word paddr; + seL4_Error err = microkit_page_get_address(cap, &paddr); + if (err != seL4_NoError) { + microkit_dbg_puts("|primary | error retrieving physical address for "); + microkit_dbg_puts(name); + microkit_dbg_puts("\n"); + halt(); + } + + microkit_dbg_puts("|primary | "); + microkit_dbg_puts(name); + microkit_dbg_puts(" frame vaddr "); + put_hex64(vaddr); + microkit_dbg_puts(" paddr "); + put_hex64(paddr); + microkit_dbg_puts("\n"); +} + +static seL4_Bool root_slot_to_metadata_with_size(seL4_Word slot, seL4_Word *metadata, seL4_Word *size_bits) +{ + if (slot == 0 || slot >= MICROKIT_BIT(microkit_max_user_caps_bits) || microkit_root_cnode_metadata == 0) { + return seL4_False; + } + + seL4_Word *root_metadata = (seL4_Word *)microkit_root_cnode_metadata; + return microkit_metadata_unpack(root_metadata[slot], metadata, size_bits); +} + +static void validate_frame_metadata(void) +{ + seL4_Word secondary_stack_bottom; + if (!microkit_root_slot_to_metadata(SLOT_SECONDARY_STACK, &secondary_stack_bottom)) { + microkit_dbg_puts("|primary | error retrieving secondary stack metadata\n"); + halt(); + } + print_frame_info("secondary stack bottom", CAP_SECONDARY_STACK, secondary_stack_bottom); + + seL4_Word secondary_ipcbuf; + if (!microkit_root_slot_to_metadata(SLOT_SECONDARY_IPCBUF, &secondary_ipcbuf)) { + microkit_dbg_puts("|primary | error retrieving secondary IPC buffer metadata\n"); + halt(); + } + print_frame_info("secondary IPC buffer", CAP_SECONDARY_IPCBUF, secondary_ipcbuf); + + seL4_Word secondary_elf_metadata; + seL4_Word secondary_elf_metadata_size_bits; + if (!root_slot_to_metadata_with_size(SLOT_SECONDARY_ELF, &secondary_elf_metadata, &secondary_elf_metadata_size_bits)) { + microkit_dbg_puts("|primary | error retrieving secondary ELF metadata\n"); + halt(); + } + microkit_dbg_puts("|primary | secondary ELF metadata at "); + put_hex64(secondary_elf_metadata); + microkit_dbg_puts(" size bits "); + microkit_dbg_put32(secondary_elf_metadata_size_bits); + microkit_dbg_puts("\n"); + + seL4_Bool seen_empty_metadata_slot = seL4_False; + seL4_Word secondary_elf_frame_count = 0; + for (seL4_Word i = 0; i < MICROKIT_BIT(secondary_elf_metadata_size_bits); i++) { + seL4_Word secondary_elf_frame_vaddr; + seL4_Bool found = + microkit_root_slot_to_nested_metadata(SLOT_SECONDARY_ELF, i, &secondary_elf_frame_vaddr); + if (!found) { + seen_empty_metadata_slot = seL4_True; + continue; + } + if (seen_empty_metadata_slot) { + microkit_dbg_puts("|primary | error: secondary ELF metadata has a gap\n"); + halt(); + } + + print_frame_info("secondary ELF", CAP_SECONDARY_ELF | i, secondary_elf_frame_vaddr); + secondary_elf_frame_count++; + } + if (secondary_elf_frame_count == 0) { + microkit_dbg_puts("|primary | error: secondary ELF metadata has no frame entries\n"); + halt(); + } +} + +static void validate_mr_frame_caps(void) +{ + for (seL4_Word i = 0; i < MR_SIZE / MR_PAGE_SIZE; i++) { + seL4_CPtr frame = CAP_MR | i; + seL4_Word paddr; + seL4_Error err = microkit_page_get_address(frame, &paddr); + if (err != seL4_NoError) { + microkit_dbg_puts("|primary | error invoking MR frame capability\n"); + halt(); + } + + microkit_dbg_puts("|primary | dma_buffer frame "); + put_hex64(i); + microkit_dbg_puts(" paddr "); + put_hex64(paddr); + microkit_dbg_puts("\n"); + + err = microkit_page_map(frame, CAP_MY_VSPACE, DMA_BUFFER_VADDR + i * MR_PAGE_SIZE, seL4_ReadWrite, + MICROKIT_EXAMPLE_DEFAULT_VM_ATTRIBUTES); + if (err != seL4_NoError) { + microkit_dbg_puts("|primary | error mapping MR frame into VSpace\n"); + halt(); + } + + volatile uint8_t *buf = (volatile uint8_t *)(DMA_BUFFER_VADDR + i * MR_PAGE_SIZE); + *buf = (uint8_t)(i + 1); + + err = microkit_page_unmap(frame); + if (err != seL4_NoError) { + microkit_dbg_puts("|primary | error unmapping MR frame from VSpace\n"); + halt(); + } + +#if defined(CONFIG_ARCH_X86_64) && defined(CONFIG_IOMMU) + err = microkit_io_page_map(frame, CAP_IOSPACE, seL4_ReadWrite, RUNTIME_IOVA + i * MR_PAGE_SIZE); + if (err != seL4_NoError) { + microkit_dbg_puts("|primary | error mapping MR frame into IOSpace\n"); + halt(); + } + + err = microkit_page_unmap(frame); + if (err != seL4_NoError) { + microkit_dbg_puts("|primary | error unmapping MR frame from IOSpace\n"); + halt(); + } +#endif + } +} + void init(void) { seL4_Error err; microkit_dbg_puts("|primary | hello, world\n"); + check_cap("secondary SC", CAP_SECONDARY_SC); + check_cap("secondary TCB", CAP_SECONDARY_TCB); + check_cap("my SC", CAP_MY_SC); + check_cap("my TCB", CAP_MY_TCB); + check_cap("my VSpace", CAP_MY_VSPACE); + check_cap("dma_buffer frames", CAP_MR); + check_cap("QEMU EDU IOSpace", CAP_IOSPACE); + check_cap("secondary stack frames", CAP_SECONDARY_STACK); + check_cap("secondary IPC buffer frame", CAP_SECONDARY_IPCBUF); + check_cap("secondary ELF frames", CAP_SECONDARY_ELF); + + validate_frame_metadata(); + validate_mr_frame_caps(); + /* Notify the secondary. This will print output from secondary as it is higher priority. */ microkit_dbg_puts("|primary | notifying secondary\n"); diff --git a/example/cap_sharing/cap_sharing.system b/example/cap_sharing/cap_sharing.system index 3f18d6fa1..6a45e8d3f 100644 --- a/example/cap_sharing/cap_sharing.system +++ b/example/cap_sharing/cap_sharing.system @@ -5,8 +5,16 @@ SPDX-License-Identifier: BSD-2-Clause --> + + + + + + + + @@ -16,6 +24,16 @@ + + + + + + + + + + diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 259f271da..0b1b6d8a8 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -38,6 +38,8 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1) #define MICROKIT_MAX_IOPORT_ID MICROKIT_MAX_CHANNELS #define MICROKIT_PD_NAME_LENGTH 64 +#define MICROKIT_BIT(n) (((seL4_Word)1) << (n)) +#define MICROKIT_MASK(n) (MICROKIT_BIT(n) - 1) /* User provided functions */ void init(void); @@ -67,6 +69,10 @@ extern seL4_Word microkit_notifications; extern seL4_Word microkit_pps; extern seL4_Word microkit_ioports; extern seL4_Word microkit_root_cnode_size_bits; +extern seL4_Word microkit_max_user_caps_bits; + +/* Symbol for storing metadata about a pds root cnode */ +extern seL4_Word microkit_root_cnode_metadata; /* * Output a single character on the debug console. @@ -604,14 +610,143 @@ 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 is not in the valid range of inputs (0 < slot < microkit_root_cnode_size_bits), + * If the slot is not in the valid range of inputs + * (0 < slot < MICROKIT_BIT(microkit_max_user_caps_bits)), * it returns the value `seL4_CapNull`. **/ static inline seL4_CPtr microkit_cspace_root_slot_to_cptr(seL4_Word slot) { - if (slot == 0 || slot >= (1ULL << microkit_root_cnode_size_bits)) { + if (slot == 0 || slot >= MICROKIT_BIT(microkit_max_user_caps_bits)) { return seL4_CapNull; } - return slot << (seL4_WordBits - microkit_root_cnode_size_bits); + return slot << (seL4_WordBits - microkit_max_user_caps_bits); +} + +#define MICROKIT_METADATA_PRESENT_BITS 1 +#define MICROKIT_METADATA_NESTED_BITS 1 +#define MICROKIT_METADATA_SIZE_BITS 6 +#define MICROKIT_METADATA_PAYLOAD_BITS \ + (seL4_WordBits - MICROKIT_METADATA_PRESENT_BITS - MICROKIT_METADATA_NESTED_BITS - MICROKIT_METADATA_SIZE_BITS) + +#define MICROKIT_METADATA_PRESENT_MASK MICROKIT_BIT(seL4_WordBits - 1) +#define MICROKIT_METADATA_NESTED_MASK MICROKIT_BIT(MICROKIT_METADATA_PAYLOAD_BITS + MICROKIT_METADATA_SIZE_BITS) +#define MICROKIT_METADATA_SIZE_SHIFT MICROKIT_METADATA_PAYLOAD_BITS +#define MICROKIT_METADATA_SIZE_MASK MICROKIT_MASK(MICROKIT_METADATA_SIZE_BITS) +#define MICROKIT_METADATA_PAYLOAD_MASK MICROKIT_MASK(MICROKIT_METADATA_PAYLOAD_BITS) + +static inline seL4_Bool microkit_metadata_unpack_with_flags(seL4_Word word, seL4_Word *payload, seL4_Word *size_bits, + seL4_Bool *nested) +{ + if ((word & MICROKIT_METADATA_PRESENT_MASK) == 0) { + return seL4_False; + } + + *nested = (word & MICROKIT_METADATA_NESTED_MASK) != 0; + *size_bits = (word >> MICROKIT_METADATA_SIZE_SHIFT) & MICROKIT_METADATA_SIZE_MASK; + *payload = word & MICROKIT_METADATA_PAYLOAD_MASK; + return seL4_True; +} + +static inline seL4_Bool microkit_metadata_unpack(seL4_Word word, seL4_Word *payload, seL4_Word *size_bits) +{ + seL4_Bool ignored_nested; + return microkit_metadata_unpack_with_flags(word, payload, size_bits, &ignored_nested); +} + +static inline seL4_Bool microkit_root_slot_to_metadata(seL4_Word slot, seL4_Word *metadata) +{ + if (slot == 0 || slot >= MICROKIT_BIT(microkit_max_user_caps_bits) || microkit_root_cnode_metadata == 0) { + return seL4_False; + } + + seL4_Word *root_metadata = (seL4_Word *)microkit_root_cnode_metadata; + seL4_Word ignored_size_bits; + return microkit_metadata_unpack(root_metadata[slot], metadata, &ignored_size_bits); +} + +static inline seL4_Bool microkit_root_slot_to_nested_metadata(seL4_Word root_slot, seL4_Word nested_slot, + seL4_Word *metadata) +{ + if (root_slot == 0 || root_slot >= MICROKIT_BIT(microkit_max_user_caps_bits) || + microkit_root_cnode_metadata == 0) { + return seL4_False; + } + + seL4_Word *root_metadata = (seL4_Word *)microkit_root_cnode_metadata; + seL4_Word nested_size_bits; + seL4_Word nested_metadata_vaddr; + seL4_Bool nested; + if (!microkit_metadata_unpack_with_flags(root_metadata[root_slot], &nested_metadata_vaddr, &nested_size_bits, + &nested)) { + return seL4_False; + } + if (!nested || nested_slot >= MICROKIT_BIT(nested_size_bits)) { + return seL4_False; + } + + seL4_Word *nested_metadata = (seL4_Word *)nested_metadata_vaddr; + seL4_Word ignored_size_bits; + return microkit_metadata_unpack(nested_metadata[nested_slot], metadata, &ignored_size_bits); +} + +static inline seL4_Error microkit_page_get_address(seL4_CPtr frame, seL4_Word *paddr) +{ +#if defined(CONFIG_ARCH_X86_64) + seL4_X86_Page_GetAddress_t ret = seL4_X86_Page_GetAddress(frame); +#elif defined(CONFIG_ARCH_AARCH64) + seL4_ARM_Page_GetAddress_t ret = seL4_ARM_Page_GetAddress(frame); +#elif defined(CONFIG_ARCH_RISCV) + seL4_RISCV_Page_GetAddress_t ret = seL4_RISCV_Page_GetAddress(frame); +#else +#error "Unsupported architecture for 'microkit_page_get_address'" +#endif + + if (ret.error != seL4_NoError) { + return ret.error; + } + + *paddr = ret.paddr; + return seL4_NoError; +} + +static inline seL4_Error microkit_page_map(seL4_CPtr frame, seL4_CPtr vspace, seL4_Word vaddr, + seL4_CapRights_t rights, seL4_Word attributes) +{ +#if defined(CONFIG_ARCH_X86_64) + return seL4_X86_Page_Map(frame, vspace, vaddr, rights, attributes); +#elif defined(CONFIG_ARCH_AARCH64) + return seL4_ARM_Page_Map(frame, vspace, vaddr, rights, attributes); +#elif defined(CONFIG_ARCH_RISCV) + return seL4_RISCV_Page_Map(frame, vspace, vaddr, rights, attributes); +#else +#error "Unsupported architecture for 'microkit_page_map'" +#endif +} + +static inline seL4_Error microkit_io_page_map(seL4_CPtr frame, seL4_CPtr iospace, seL4_CapRights_t rights, + seL4_Word ioaddr) +{ +#if defined(CONFIG_ARCH_X86_64) && defined(CONFIG_IOMMU) + return seL4_X86_Page_MapIO(frame, iospace, rights, ioaddr); +#else + (void)frame; + (void)iospace; + (void)rights; + (void)ioaddr; + return seL4_InvalidArgument; +#endif +} + +static inline seL4_Error microkit_page_unmap(seL4_CPtr frame) +{ +#if defined(CONFIG_ARCH_X86_64) + return seL4_X86_Page_Unmap(frame); +#elif defined(CONFIG_ARCH_AARCH64) + return seL4_ARM_Page_Unmap(frame); +#elif defined(CONFIG_ARCH_RISCV) + return seL4_RISCV_Page_Unmap(frame); +#else +#error "Unsupported architecture for 'microkit_page_unmap'" +#endif } diff --git a/libmicrokit/src/main.c b/libmicrokit/src/main.c index bdb6e8147..1fc3be162 100644 --- a/libmicrokit/src/main.c +++ b/libmicrokit/src/main.c @@ -39,6 +39,9 @@ seL4_Word microkit_notifications; seL4_Word microkit_pps; seL4_Word microkit_ioports; seL4_Word microkit_root_cnode_size_bits; +seL4_Word microkit_max_user_caps_bits; + +seL4_Word microkit_root_cnode_metadata; #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 f878e73d0..6f886e650 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -24,11 +24,11 @@ use crate::{ }, elf::ElfFile, sdf::{ - CapMapType, CpuCore, Map, SystemDescription, BUDGET_DEFAULT, MONITOR_DOMAIN, + CapMap, CpuCore, FrameCapPerms, Map, SystemDescription, BUDGET_DEFAULT, MONITOR_DOMAIN, MONITOR_PD_NAME, MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, - util::{ranges_overlap, round_down, round_up}, + util::{calculate_size_bits, ranges_overlap, round_down, round_up}, }; const FAULT_BADGE: u64 = 1 << 62; @@ -145,6 +145,7 @@ impl PDShadowCspace { struct ElfSpecResult { tcb: ObjectId, address_space: AddressSpace, + frames: Vec, } pub struct CapDLSpecContainer { @@ -222,6 +223,7 @@ impl CapDLSpecContainer { elf_id: usize, elf: &ElfFile, ) -> Result { + let mut frame_obj_ids: Vec = Vec::new(); // We assumes that ELFs and PDs have a one-to-one relationship. So for each ELF we create a VSpace. let address_space = create_vspace(self, sel4_config, pd_name); let vspace_obj_id = address_space.root(); @@ -286,6 +288,7 @@ impl CapDLSpecContainer { None, PageSize::Small.fixed_size_bits(sel4_config) as u8, ); + frame_obj_ids.push(frame_obj_id); let frame_cap = capdl_util_make_frame_cap( frame_obj_id, segment.is_readable(), @@ -345,6 +348,7 @@ impl CapDLSpecContainer { Ok(ElfSpecResult { tcb: self.add_root_object(tcb_obj), address_space, + frames: frame_obj_ids, }) } } @@ -616,6 +620,9 @@ pub fn build_capdl_spec( // 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(); + let mut pd_stack_frames: HashMap> = HashMap::new(); + let mut pd_ipc_frame: HashMap = HashMap::new(); + let mut pd_elf_specs: 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. @@ -631,9 +638,13 @@ pub fn build_capdl_spec( 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. - let pd_elf_spec = spec_container - .add_elf_to_spec(kernel_config, &pd.name, pd.cpu, pd_global_idx, elf_obj) - .unwrap(); + pd_elf_specs.insert( + pd_global_idx, + spec_container + .add_elf_to_spec(kernel_config, &pd.name, pd.cpu, pd_global_idx, elf_obj) + .unwrap(), + ); + let pd_elf_spec = pd_elf_specs.get(&pd_global_idx).unwrap(); let pd_tcb_obj_id = pd_elf_spec.tcb; let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id); @@ -713,6 +724,13 @@ pub fn build_capdl_spec( ipcbuf_frame_cap, )); + if pd_ipc_frame + .insert(pd_global_idx, ipcbuf_frame_obj_id) + .is_some() + { + panic!("Error: there should only be one ipcbuff per pd"); + } + // Step 3-3b: 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); @@ -740,6 +758,10 @@ pub fn build_capdl_spec( ) .unwrap(); cur_stack_vaddr += PageSize::Small as u64; + pd_stack_frames + .entry(pd_global_idx) + .or_insert(vec![]) + .push(stack_frame_obj_id); } // Step 3-4 Create Scheduling Context @@ -1258,23 +1280,112 @@ pub fn build_capdl_spec( // ********************************* // Step 6. Handle extra cap mappings // ********************************* + for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() { 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()]; - - 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), + let cap_map_obj = match cap_map { + CapMap::IOSpace(map) => { + let addr_space_root = iospace_by_device + .get(map.name.as_str()) + .expect("Already validated in sdf.rs") + .root(); + capdl_util_make_iospace_cap(addr_space_root) + } + CapMap::Tcb(map) => { + let pd_src_shadow_cspace = + &pd_shadow_cspaces[&map.pd.expect("Already validated in sdf.rs")]; + capdl_util_make_tcb_cap(pd_src_shadow_cspace.tcb) + } + CapMap::Sc(map) => { + let pd_src_shadow_cspace = + &pd_shadow_cspaces[&map.pd.expect("Already validated in sdf.rs")]; + + capdl_util_make_sc_cap(pd_src_shadow_cspace.sched_context) + } + CapMap::VSpace(map) => { + let pd_src_shadow_cspace = + &pd_shadow_cspaces[&map.pd.expect("Already validated in sdf.rs")]; + capdl_util_make_page_table_cap(pd_src_shadow_cspace.vspace) + } + CapMap::MemoryRegionFrames(map) => { + let mr_frames = &mr_name_to_frames[&map.mr_name]; + let size_bits = calculate_size_bits(mr_frames.len() as u64).max(1); + + fill_cnode_with_frames( + &mut spec_container, + kernel_config, + mr_frames, + size_bits, + map.perms, + cspace.size_bits as u8, + &format!("pd_{}_slot_{}_mr_{}", pd.name, cap_map.slot(), map.mr_name), + ) + } + CapMap::ElfFrames(map) => { + let pd_src_frame_obj_ids = pd_elf_specs + .get(&map.pd_info().pd.expect("Already validated in sdf.rs")) + .expect("created above"); + + let size_bits = + calculate_size_bits(pd_src_frame_obj_ids.frames.len() as u64).max(1); + + fill_cnode_with_frames( + &mut spec_container, + kernel_config, + &pd_src_frame_obj_ids.frames, + size_bits, + map.perms, + cspace.size_bits as u8, + &format!( + "src_pd_{}_elf_frames_for_dst_{}_slot_{}", + map.pd_info.pd_name, + pd.name, + cap_map.slot() + ), + ) + } + CapMap::StackFrames(map) => { + let pd_src_frame_obj_ids = pd_stack_frames + .get(&map.pd_info().pd.expect("Already validated in sdf.rs")) + .expect("created above"); + + let size_bits = calculate_size_bits(pd_src_frame_obj_ids.len() as u64).max(1); + + fill_cnode_with_frames( + &mut spec_container, + kernel_config, + &pd_src_frame_obj_ids, + size_bits, + map.perms, + cspace.size_bits as u8, + &format!( + "src_pd_{}_stack_frames_for_dst_{}_slot_{}", + map.pd_info.pd_name, + pd.name, + cap_map.slot() + ), + ) + } + CapMap::IpcBufferFrame(map) => { + let pd_src_frame_obj_id = pd_ipc_frame + .get(&map.pd_info().pd.expect("Already validated in sdf.rs")) + .expect("created above"); + + capdl_util_make_frame_cap( + *pd_src_frame_obj_id, + map.perms.read(), + map.perms.write(), + false, + true, + ) + } }; // Map this into the destination pd's cspace and the specified slot. pd_shadow_cspaces[&pd_dest_idx].insert_cap_into_root_cnode( &mut spec_container, - cap_map.slot as u32, + cap_map.slot() as u32, cap_map_obj, ); } @@ -1393,3 +1504,34 @@ pub fn build_capdl_spec( Ok(spec_container) } + +fn fill_cnode_with_frames( + spec_container: &mut CapDLSpecContainer, + kernel_config: &Config, + frames: &[ObjectId], + size_bits: u8, + perms: FrameCapPerms, + root_cnode_bits: u8, + cnode_name: &str, +) -> Cap { + // The execute and cached fields are considered attributes by seL4 and from my understanding @cazb2 + // do not get masked when invoking the frame thus are redundant. Since they are not fixed at runtime. + let mut slot = 0; + let slots = frames + .iter() + .map(|&frame_obj_id| { + capdl_util_make_frame_cap(frame_obj_id, perms.read(), perms.write(), false, true) + }) + .map(|cap| { + let cte = capdl_util_make_cte(slot, cap); + slot += 1; + cte + }) + .collect(); + + let mr_cnode_obj = capdl_util_make_cnode_obj(spec_container, cnode_name, size_bits, slots); + + // Configure the CNode to simulate array indexing. + let mr_guard_size = kernel_config.cap_address_bits - root_cnode_bits as u64 - size_bits as u64; + capdl_util_make_cnode_cap(mr_cnode_obj, 0, mr_guard_size as u8) +} diff --git a/tool/microkit/src/capdl/util.rs b/tool/microkit/src/capdl/util.rs index a1c20e3ca..ae8ec54c5 100644 --- a/tool/microkit/src/capdl/util.rs +++ b/tool/microkit/src/capdl/util.rs @@ -70,6 +70,12 @@ pub fn capdl_util_make_tcb_cap(tcb_obj_id: ObjectId) -> Cap { Cap::Tcb(cap::Tcb { object: tcb_obj_id }) } +pub fn capdl_util_make_iospace_cap(iospace_obj_id: ObjectId) -> Cap { + Cap::IOSpace(cap::IOSpace { + object: iospace_obj_id, + }) +} + pub fn capdl_util_make_page_table_cap(pt_obj_id: ObjectId) -> Cap { Cap::PageTable(cap::PageTable { object: pt_obj_id }) } diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index daaaefeb3..fdb5a4525 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -18,21 +18,22 @@ use microkit_tool::capdl::packaging::pack_spec_into_initial_task; use microkit_tool::elf::ElfFile; use microkit_tool::loader::Loader; use microkit_tool::report::write_report; -use microkit_tool::sdf::{parse, SysMemoryRegion, SysMemoryRegionPaddr}; +use microkit_tool::sdf::{parse, Map, SysMap, SysMemoryRegion, SysMemoryRegionPaddr}; use microkit_tool::sdk::{AvailableConfig, Sdk}; use microkit_tool::sel4::{ emulate_kernel_boot, emulate_kernel_boot_partial, AddressSpaceConstants, Arch, Config, - ObjectSizes, PlatformConfig, RiscvVirtualMemory, + ObjectSizes, PageSize, PlatformConfig, RiscvVirtualMemory, }; use microkit_tool::symbols::patch_symbols; use microkit_tool::util::{ - get_full_path, human_size_strict, json_str, json_str_as_bool, json_str_as_u64, round_down, - round_up, + calculate_size_bits, get_full_path, human_size_strict, json_str, json_str_as_bool, + json_str_as_u64, round_down, round_up, }; use microkit_tool::viper; use microkit_tool::{DisjointMemoryRegion, MemoryRegion}; use std::collections::HashMap; use std::fs::{self, metadata}; +use std::ops::Range; use std::path::Path; const MAX_BUILD_ITERATION: usize = 3; @@ -414,6 +415,180 @@ fn main() -> Result<(), String> { // The monitor is just a special PD system_elfs.push(monitor_elf); + let get_mr_size = |mr_name: &str| { + system + .memory_regions + .iter() + .find(|mr| &mr.name == mr_name) + .expect("validated in sdf.rs") + .size + }; + let find_free_region = |regions: &mut [Range], size: u64, max_addr: u64| { + let page_size = PageSize::Small as u64; + let candidate_before = |possible_end| { + let end = round_down(possible_end, page_size); + let start = round_down( + end.checked_sub(size) + .expect("Error: no free region in address space"), + page_size, + ); + start..end + }; + + regions.sort_by_key(|range| range.start); + let mut possible_end = round_down(max_addr, page_size); + for region in regions.iter().rev() { + if possible_end <= region.start { + continue; + } + let candidate = candidate_before(possible_end); + if candidate.start >= region.end { + return candidate; + } + possible_end = round_down(region.start, page_size); + } + candidate_before(possible_end) + }; + let encode_metadata = |vaddr: u64, size_bits: u8, nested: bool| -> u64 { + const PRESENT_BITS: u64 = 1; + const NESTED_BITS: u64 = 1; + const SIZE_BITS: u64 = 6; + const PAYLOAD_BITS: u64 = u64::BITS as u64 - PRESENT_BITS - NESTED_BITS - SIZE_BITS; + const PRESENT_BIT: u64 = 1 << (u64::BITS - 1); + const NESTED_BIT: u64 = 1 << (PAYLOAD_BITS + SIZE_BITS); + if u64::from(size_bits) >= (1u64 << SIZE_BITS) { + panic!("Error: metadata size bits {size_bits} do not fit in {SIZE_BITS} bits"); + } + if vaddr >= (1 << PAYLOAD_BITS) { + panic!("Error: metadata vaddr {vaddr:#x} does not fit in {PAYLOAD_BITS} payload bits"); + } + PRESENT_BIT | (if nested { NESTED_BIT } else { 0 }) + | (u64::from(size_bits) << PAYLOAD_BITS) + | vaddr + }; + + let pd_elf_segments_by_idx: Vec>> = system_elfs + .iter() + .map(|seg| { + seg.loadable_segments() + .iter() + .map(|seg| { + let start = round_down(seg.virt_addr, PageSize::Small as u64); + let end = round_up(seg.virt_addr + seg.mem_size(), PageSize::Small as u64); + start..end + }) + .collect() + }) + .collect(); + + let mut pd_regions: Vec>> = system + .protection_domains + .iter() + .map(|pd| { + pd.maps + .iter() + .map(|map| map.vaddr..map.vaddr + get_mr_size(map.mr_name())) + .collect::>>() + }) + .collect(); + + for (idx, regions) in pd_regions.iter_mut().enumerate() { + regions.extend_from_slice(&pd_elf_segments_by_idx[idx]); + regions.sort_by_key(|range| range.start); + } + + let pd_stack_bases_by_idx = system + .protection_domains + .iter() + .map(|pd| kernel_config.pd_stack_bottom(pd.stack_size)) + .collect::>(); + + for (pd_idx, pd) in system.protection_domains.iter_mut().enumerate() { + let Some(cspace) = &mut pd.cspace else { + continue; + }; + + // create the MR with the bytes for the metadata + let mut root_metadata = vec![0u64; 1usize << cspace.size_bits]; + for cap_map in cspace.cap_maps.iter() { + match cap_map { + microkit_tool::sdf::CapMap::ElfFrames(map) => { + let other_pd_idx = map.pd_info().pd.expect("Filled in sdf.rs"); + let frame_vaddrs = system_elfs[other_pd_idx] + .loadable_segments() + .iter() + .flat_map(|seg| { + let start = round_down(seg.virt_addr, PageSize::Small as u64); + let end = + round_up(seg.virt_addr + seg.mem_size(), PageSize::Small as u64); + (start..end).step_by(PageSize::Small as usize) + }) + .collect::>(); + + let region_size_bytes = + round_up((frame_vaddrs.len() * 8) as u64, PageSize::Small as u64); + + let nested_cspace_region = find_free_region( + &mut pd_regions[pd_idx], + region_size_bytes, + kernel_config.pd_map_max_vaddr(pd.stack_size), + ); + pd_regions[pd_idx].push(nested_cspace_region.clone()); + + root_metadata[cap_map.slot() as usize] = encode_metadata( + nested_cspace_region.start, + calculate_size_bits(frame_vaddrs.len() as u64), + true, + ); + + let nested_metadata = frame_vaddrs + .into_iter() + .flat_map(|vaddr| encode_metadata(vaddr, 0, false).to_le_bytes()) + .collect::>(); + + let nested_mr_name = + format!("pd_{}_slot_{}_nested_metadata", pd.name, cap_map.slot()); + let nested_mr = + SysMemoryRegion::new_mr(nested_mr_name.clone(), nested_metadata); + system.memory_regions.push(nested_mr); + pd.maps + .push(SysMap::new_map(nested_mr_name, nested_cspace_region.start)); + } + microkit_tool::sdf::CapMap::StackFrames(map) => { + let other_pd_idx = map.pd_info().pd.expect("Filled in sdf.rs"); + root_metadata[cap_map.slot() as usize] = + encode_metadata(pd_stack_bases_by_idx[other_pd_idx], 0, false); + } + microkit_tool::sdf::CapMap::IpcBufferFrame(_) => { + root_metadata[cap_map.slot() as usize] = + encode_metadata(kernel_config.pd_ipc_buffer(), 0, false); + } + _ => (), + } + } + + let root_cspace_metadata_region = find_free_region( + &mut pd_regions[pd_idx], + round_up((1u64 << cspace.size_bits) * 8, PageSize::Small as u64), + kernel_config.pd_map_max_vaddr(pd.stack_size), + ); + + pd_regions[pd_idx].push(root_cspace_metadata_region.clone()); + let root_metadata_bytes = root_metadata + .iter() + .flat_map(|vaddr| vaddr.to_le_bytes()) + .collect::>(); + + cspace.metadata_vaddr = Some(root_cspace_metadata_region.start); + let root_mr_name = format!("pd_{}_slot_root_cspace_metadata", pd.name,); + let root_mr = SysMemoryRegion::new_mr(root_mr_name.clone(), root_metadata_bytes); + system.memory_regions.push(root_mr); + pd.maps.push(SysMap::new_map( + root_mr_name, + root_cspace_metadata_region.start, + )); + } + let capdl_initialiser_orig = CapDLInitialiser::new(capdl_initialiser_elf); // Now build the capDL spec and final image. We may need to do this in >1 iterations on ARM and RISC-V diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 79d659ebb..797b954ca 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -341,6 +341,35 @@ impl FrameRights { } } +#[derive(Debug, PartialEq, Eq, Clone, Copy)] +pub struct FrameCapPerms(FrameRights); + +impl FrameCapPerms { + fn from_str(s: &str) -> Result { + let mut read = false; + let mut write = false; + + for c in s.chars() { + match c { + 'r' => read = true, + 'w' => write = true, + _ => return Err(format!("Invalid character in string {s}")), + } + } + let frame_rights = match FrameRights::from_bools(read, write) { + FrameRights::None => return Err("Invalid frame right".into()), + frame_rights => frame_rights, + }; + Ok(FrameCapPerms(frame_rights)) + } + pub fn read(self) -> bool { + self.0.read() + } + pub fn write(self) -> bool { + self.0.write() + } +} + #[derive(Debug, PartialEq, Eq, Clone, Copy)] pub struct SysIOMapPerms(FrameRights); @@ -487,6 +516,7 @@ pub enum SysMemoryRegionKind { Elf, Stack, BootInfo, + GeneratedMetadata, } #[derive(Debug, PartialEq, Eq, Clone)] @@ -672,16 +702,19 @@ pub struct ProtectionDomain { text_pos: Option, } -#[derive(Debug, PartialEq, Eq, Copy, Clone, Hash)] -pub enum CapMapType { - Tcb, - Sc, - VSpace, +#[derive(Debug, PartialEq, Eq)] +pub struct CapMapCommon { + // 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, PartialEq, Eq)] -pub struct CapMap { - pub cap_type: CapMapType, +pub struct PdCapMap { + pub common: CapMapCommon, // 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 @@ -691,18 +724,129 @@ pub struct CapMap { // 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, +} + +/// The virtual address for the base of the MR in each PD that has it mapped is +/// specified in the SDF and can be retrieved external from the tool. +#[derive(Debug, PartialEq, Eq)] +pub struct MemoryRegionCapMap { + pub common: CapMapCommon, + pub mr_name: String, + pub perms: FrameCapPerms, +} + +impl MemoryRegionCapMap { + pub fn common(&self) -> &CapMapCommon { + &self.common + } +} + +#[derive(Debug, PartialEq, Eq)] +pub struct IOSpaceCapMap { + pub common: CapMapCommon, + pub name: String, +} + +impl IOSpaceCapMap { + pub fn common(&self) -> &CapMapCommon { + &self.common + } +} + +/// The virtual address for the base of the stack and the ipc buffer & page size is only +/// known internally to the tool. This requires the tool to expose this information. +#[derive(Debug, PartialEq, Eq)] +pub struct PdFrameCapMap { + pub pd_info: PdCapMap, + pub perms: FrameCapPerms, +} + +impl PdFrameCapMap { + pub fn common(&self) -> &CapMapCommon { + &self.pd_info.common + } + pub fn pd_info(&self) -> &PdCapMap { + &self.pd_info + } + pub fn pd_info_mut(&mut self) -> &mut PdCapMap { + &mut self.pd_info + } +} + +#[derive(Debug, PartialEq, Eq)] +pub enum CapMap { + Tcb(PdCapMap), + Sc(PdCapMap), + VSpace(PdCapMap), + IOSpace(IOSpaceCapMap), + MemoryRegionFrames(MemoryRegionCapMap), + ElfFrames(PdFrameCapMap), + StackFrames(PdFrameCapMap), + IpcBufferFrame(PdFrameCapMap), +} + +impl CapMap { + pub fn common(&self) -> &CapMapCommon { + match self { + CapMap::Tcb(map) | CapMap::Sc(map) | CapMap::VSpace(map) => &map.common, + CapMap::IOSpace(map) => &map.common, + CapMap::MemoryRegionFrames(map) => &map.common, + CapMap::ElfFrames(map) => map.common(), + CapMap::StackFrames(map) => map.common(), + CapMap::IpcBufferFrame(map) => map.common(), + } + } + pub fn pd_cap(&mut self) -> Option<&PdCapMap> { + match self { + CapMap::Tcb(map) | CapMap::Sc(map) | CapMap::VSpace(map) => Some(map), + CapMap::ElfFrames(map) => Some(map.pd_info()), + CapMap::StackFrames(map) | CapMap::IpcBufferFrame(map) => Some(map.pd_info()), + CapMap::IOSpace(_) | CapMap::MemoryRegionFrames(_) => None, + } + } + pub fn pd_cap_mut(&mut self) -> Option<&mut PdCapMap> { + match self { + CapMap::Tcb(map) | CapMap::Sc(map) | CapMap::VSpace(map) => Some(map), + CapMap::ElfFrames(map) => Some(map.pd_info_mut()), + CapMap::StackFrames(map) | CapMap::IpcBufferFrame(map) => Some(map.pd_info_mut()), + CapMap::IOSpace(_) | CapMap::MemoryRegionFrames(_) => None, + } + } + pub fn slot(&self) -> u64 { + self.common().slot + } + pub fn text_pos(&self) -> roxmltree::TextPos { + self.common().text_pos + } + pub fn cap_type(&self) -> &'static str { + match self { + CapMap::Tcb(_) => "Tcb", + CapMap::Sc(_) => "Sc", + CapMap::VSpace(_) => "VSpace", + CapMap::IOSpace(_) => "IOSpace", + CapMap::MemoryRegionFrames(_) => "MemoryRegion", + CapMap::ElfFrames(_) => "ElfFrames", + CapMap::StackFrames(_) => "StackFrames", + CapMap::IpcBufferFrame(_) => "IpcBufferFrame", + } + } + pub fn src_name(&self) -> &str { + match self { + CapMap::Tcb(map) | CapMap::Sc(map) | CapMap::VSpace(map) => &map.pd_name, + CapMap::IOSpace(map) => &map.name, + CapMap::MemoryRegionFrames(map) => &map.mr_name, + CapMap::ElfFrames(map) | CapMap::StackFrames(map) | CapMap::IpcBufferFrame(map) => { + &map.pd_info.pd_name + } + } + } } #[derive(Debug, PartialEq, Eq)] pub struct CSpace { pub cap_maps: Vec, pub size_bits: u64, + pub metadata_vaddr: Option, } #[derive(Debug, PartialEq, Eq)] @@ -796,6 +940,18 @@ impl SysMap { text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), }) } + pub fn new_map(mr: String, vaddr: u64) -> Self { + Self { + mr, + vaddr, + perms: SysMapPerms { + rights: FrameRights::Read, + execute: false, + }, + cached: true, + text_pos: None, + } + } } impl SysIOMap { @@ -1805,18 +1961,109 @@ impl VirtualMachine { } impl CapMap { - fn from_xml( - cap_type: CapMapType, + fn common_from_xml( + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + slot: u64, + ) -> CapMapCommon { + CapMapCommon { + slot, + text_pos: xml_sdf.doc.text_pos_at(node.range().start), + } + } + + fn handle_iospace( + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + slot: u64, + ) -> Result { + let name = checked_lookup(xml_sdf, node, "io_address_space")?; + + Ok(CapMap::IOSpace(IOSpaceCapMap { + common: Self::common_from_xml(xml_sdf, node, slot), + name: name.into(), + })) + } + + fn handle_pd_frame_source( + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + slot: u64, + cap_type: &str, + ) -> Result { + let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string(); + let perms = FrameCapPerms::from_str(checked_lookup(xml_sdf, node, "perms")?) + .map_err(|err| format! {"Error: {err} at location {}",loc_string(xml_sdf, xml_sdf.doc.text_pos_at(node.range().start))})?; + + let pd_info = PdCapMap { + common: Self::common_from_xml(xml_sdf, node, slot), + pd_name, + pd: None, + }; + + let pd_frame_cap = PdFrameCapMap { pd_info, perms }; + + match cap_type { + "cap_stack" => Ok(CapMap::StackFrames(pd_frame_cap)), + "cap_elf" => Ok(CapMap::ElfFrames(pd_frame_cap)), + "cap_ipcbuf" => Ok(CapMap::IpcBufferFrame(pd_frame_cap)), + _ => unreachable!("checked by caller"), + } + } + + fn handle_mr( xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, + slot: u64, ) -> 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 mr_name = checked_lookup(xml_sdf, node, "mr_name")?; + let perms = FrameCapPerms::from_str(checked_lookup(xml_sdf, node, "perms")?)?; + Ok(CapMap::MemoryRegionFrames(MemoryRegionCapMap { + common: Self::common_from_xml(xml_sdf, node, slot), + mr_name: mr_name.into(), + perms, + })) + } + + fn handle_pd_cap( + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + slot: u64, + ) -> Result { let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string(); + Ok(PdCapMap { + common: Self::common_from_xml(xml_sdf, node, slot), + pd_name, + // FIXME: Hack, filled out later. + pd: None, + }) + } + + fn from_xml( + cap_type: &str, + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + ) -> Result { + let allowed_attrs = match cap_type { + "cap_mr" => &["slot", "mr_name", "perms"].as_slice(), + "cap_iospace" => &["slot", "io_address_space"].as_slice(), + "cap_tcb" | "cap_sc" | "cap_vspace" => &["slot", "pd"].as_slice(), + "cap_stack" | "cap_elf" | "cap_ipcbuf" => &["slot", "pd", "perms"].as_slice(), + child_name => { + let location = loc_string(xml_sdf, xml_sdf.doc.text_pos_at(node.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}'")); + } + } + }; + check_attributes(xml_sdf, node, allowed_attrs)?; + let slot = sdf_parse_number(checked_lookup(xml_sdf, node, "slot")?, node)?; if slot == 0 { @@ -1826,15 +2073,17 @@ impl CapMap { ("The destination slot 0 has been reserved for Microkit CNode").to_string(), )); } - - 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), - }) + match cap_type { + "cap_mr" => Self::handle_mr(xml_sdf, node, slot), + "cap_iospace" => Self::handle_iospace(xml_sdf, node, slot), + "cap_tcb" => Self::handle_pd_cap(xml_sdf, node, slot).map(CapMap::Tcb), + "cap_sc" => Self::handle_pd_cap(xml_sdf, node, slot).map(CapMap::Sc), + "cap_vspace" => Self::handle_pd_cap(xml_sdf, node, slot).map(CapMap::VSpace), + "cap_stack" | "cap_elf" | "cap_ipcbuf" => { + Self::handle_pd_frame_source(xml_sdf, node, slot, cap_type) + } + _ => unreachable!("cap_type was validated above"), + } } } @@ -1845,31 +2094,20 @@ impl CSpace { 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)?, - 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}'")); - } - } - }) + cap_maps.push(CapMap::from_xml(child.tag_name().name(), xml_sdf, &child)?); } // 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)) + .map(|cap_map| calculate_size_bits(cap_map.common().slot + 1)) .max() .unwrap_or(1) as u64; Ok(CSpace { cap_maps, size_bits, + metadata_vaddr: None, }) } } @@ -2078,6 +2316,27 @@ impl SysMemoryRegion { prefill_bootinfo: prefill_bootinfo_maybe, }) } + + pub fn new_mr(name: String, bytes: Vec) -> Self { + let page_size = PageSize::Small as u64; + let size = round_up(bytes.len() as u64, page_size); + + if size == 0 { + panic!("Attempting to create a zero sized mr"); + } + Self { + name, + size, + page_size_specified_by_user: false, + page_size: PageSize::Small, + page_count: size / page_size, + phys_addr: SysMemoryRegionPaddr::Unspecified, + text_pos: None, + kind: SysMemoryRegionKind::GeneratedMetadata, + prefill_bytes: Some(bytes), + prefill_bootinfo: None, + } + } } impl ChannelEnd { @@ -2922,15 +3181,41 @@ pub fn parse( .collect(); 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 '{}': {}", - cap_map.pd_name, - loc_string(&xml_sdf, cap_map.text_pos) - )); - }; + match cap_map.pd_cap_mut() { + Some(pd_cap_map) => { + let Some(&pd) = pd_names_to_id.get(&pd_cap_map.pd_name) else { + return Err(format!( + "Error: unknown PD name '{}': {}", + pd_cap_map.pd_name, + loc_string(&xml_sdf, pd_cap_map.common.text_pos) + )); + }; - cap_map.pd = Some(pd); + pd_cap_map.pd = Some(pd) + } + None => (), + }; + match cap_map { + CapMap::MemoryRegionFrames(mr_cap_map) => { + if let None = mrs.iter().find(|mr| mr.name == mr_cap_map.mr_name) { + return Err(format!( + "Error: unknown MR name '{}': {}", + mr_cap_map.mr_name, + loc_string(&xml_sdf, mr_cap_map.common.text_pos) + )); + } + } + CapMap::IOSpace(iospace_cap_map) => { + if !io_address_space_names.contains(&iospace_cap_map.name) { + return Err(format!( + "Error: unknown IOSpace name '{}': {}", + iospace_cap_map.name, + loc_string(&xml_sdf, iospace_cap_map.common.text_pos) + )); + } + } + _ => (), + } } } @@ -3180,7 +3465,7 @@ pub fn parse( for cap_map in &cspace.cap_maps { user_cap_slots - .entry(cap_map.slot) + .entry(cap_map.slot()) .and_modify(|v| v.push(cap_map)) .or_insert(vec![cap_map]); } @@ -3190,10 +3475,10 @@ pub fn parse( 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) + "\n type {} from '{}' at '{}'", + mapping.cap_type(), + mapping.src_name(), + loc_string(&xml_sdf, mapping.text_pos()) )); } return Err(format!( diff --git a/tool/microkit/src/symbols.rs b/tool/microkit/src/symbols.rs index 03fd19a95..eb94bec46 100644 --- a/tool/microkit/src/symbols.rs +++ b/tool/microkit/src/symbols.rs @@ -144,6 +144,26 @@ pub fn patch_symbols( .to_le_bytes(), ) .unwrap(); + elf_obj + .write_symbol( + "microkit_max_user_caps_bits", + &pd.cspace + .as_ref() + .map_or(0u64, |cspace| cspace.size_bits) + .to_le_bytes(), + ) + .unwrap(); + elf_obj + .write_symbol( + "microkit_root_cnode_metadata", + &pd.cspace + .as_ref() + .map_or(0u64, |cspace| { + cspace.metadata_vaddr.expect("filled in main.rs") + }) + .to_le_bytes(), + ) + .unwrap(); let mut symbols_to_write: Vec<(&String, u64)> = Vec::new(); for setvar in pd.setvars.iter() { From 0f440e44219068361ea3f102d50cf7256176c7c7 Mon Sep 17 00:00:00 2001 From: Callum Date: Fri, 24 Jul 2026 08:37:31 +1000 Subject: [PATCH 4/4] WIP: Support PageTable This is required to map frames at runtime. --- example/cap_sharing/cap_sharing.c | 31 +- example/cap_sharing/cap_sharing.system | 7 +- libmicrokit/include/microkit.h | 70 ++--- libmicrokit/src/main.c | 5 +- tool/microkit/src/capdl/builder.rs | 69 ++++- tool/microkit/src/capdl/memory.rs | 111 +++++-- tool/microkit/src/main.rs | 42 ++- tool/microkit/src/sdf.rs | 408 +++++++++++++++++++++++-- tool/microkit/src/symbols.rs | 9 - 9 files changed, 612 insertions(+), 140 deletions(-) diff --git a/example/cap_sharing/cap_sharing.c b/example/cap_sharing/cap_sharing.c index a6e6ced81..6a70cba5f 100644 --- a/example/cap_sharing/cap_sharing.c +++ b/example/cap_sharing/cap_sharing.c @@ -26,6 +26,8 @@ #define MR_SIZE 0xa000 #define MR_PAGE_SIZE 0x1000 +#define STACK_SIZE 0x2000 + #define DMA_BUFFER_VADDR 0x10001000 #define IOVA 0x100000 #define RUNTIME_IOVA (IOVA + MR_SIZE) @@ -91,16 +93,6 @@ static void print_frame_info(const char *name, seL4_CPtr cap, seL4_Word vaddr) microkit_dbg_puts("\n"); } -static seL4_Bool root_slot_to_metadata_with_size(seL4_Word slot, seL4_Word *metadata, seL4_Word *size_bits) -{ - if (slot == 0 || slot >= MICROKIT_BIT(microkit_max_user_caps_bits) || microkit_root_cnode_metadata == 0) { - return seL4_False; - } - - seL4_Word *root_metadata = (seL4_Word *)microkit_root_cnode_metadata; - return microkit_metadata_unpack(root_metadata[slot], metadata, size_bits); -} - static void validate_frame_metadata(void) { seL4_Word secondary_stack_bottom; @@ -109,6 +101,10 @@ static void validate_frame_metadata(void) halt(); } print_frame_info("secondary stack bottom", CAP_SECONDARY_STACK, secondary_stack_bottom); + for (seL4_Word i = 1; i < STACK_SIZE / MICROKIT_BIT(seL4_PageBits); i++) { + print_frame_info("stack frame", CAP_SECONDARY_STACK | i, + secondary_stack_bottom + i * MICROKIT_BIT(seL4_PageBits)); + } seL4_Word secondary_ipcbuf; if (!microkit_root_slot_to_metadata(SLOT_SECONDARY_IPCBUF, &secondary_ipcbuf)) { @@ -118,30 +114,21 @@ static void validate_frame_metadata(void) print_frame_info("secondary IPC buffer", CAP_SECONDARY_IPCBUF, secondary_ipcbuf); seL4_Word secondary_elf_metadata; - seL4_Word secondary_elf_metadata_size_bits; - if (!root_slot_to_metadata_with_size(SLOT_SECONDARY_ELF, &secondary_elf_metadata, &secondary_elf_metadata_size_bits)) { + if (!microkit_root_slot_to_metadata(SLOT_SECONDARY_ELF, &secondary_elf_metadata)) { microkit_dbg_puts("|primary | error retrieving secondary ELF metadata\n"); halt(); } microkit_dbg_puts("|primary | secondary ELF metadata at "); put_hex64(secondary_elf_metadata); - microkit_dbg_puts(" size bits "); - microkit_dbg_put32(secondary_elf_metadata_size_bits); microkit_dbg_puts("\n"); - seL4_Bool seen_empty_metadata_slot = seL4_False; seL4_Word secondary_elf_frame_count = 0; - for (seL4_Word i = 0; i < MICROKIT_BIT(secondary_elf_metadata_size_bits); i++) { + for (seL4_Word i = 0;; i++) { seL4_Word secondary_elf_frame_vaddr; seL4_Bool found = microkit_root_slot_to_nested_metadata(SLOT_SECONDARY_ELF, i, &secondary_elf_frame_vaddr); if (!found) { - seen_empty_metadata_slot = seL4_True; - continue; - } - if (seen_empty_metadata_slot) { - microkit_dbg_puts("|primary | error: secondary ELF metadata has a gap\n"); - halt(); + break; } print_frame_info("secondary ELF", CAP_SECONDARY_ELF | i, secondary_elf_frame_vaddr); diff --git a/example/cap_sharing/cap_sharing.system b/example/cap_sharing/cap_sharing.system index 6a45e8d3f..199856ba0 100644 --- a/example/cap_sharing/cap_sharing.system +++ b/example/cap_sharing/cap_sharing.system @@ -6,15 +6,14 @@ --> - - + - + @@ -37,7 +36,7 @@ - + diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 0b1b6d8a8..25e9741fe 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -38,7 +38,7 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1) #define MICROKIT_MAX_IOPORT_ID MICROKIT_MAX_CHANNELS #define MICROKIT_PD_NAME_LENGTH 64 -#define MICROKIT_BIT(n) (((seL4_Word)1) << (n)) +#define MICROKIT_BIT(n) (((seL4_Uint64)1) << (n)) #define MICROKIT_MASK(n) (MICROKIT_BIT(n) - 1) /* User provided functions */ @@ -68,11 +68,10 @@ 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; -extern seL4_Word microkit_max_user_caps_bits; +extern seL4_Uint64 microkit_max_user_caps_bits; /* Symbol for storing metadata about a pds root cnode */ -extern seL4_Word microkit_root_cnode_metadata; +extern seL4_Uint64 microkit_root_cnode_metadata; /* * Output a single character on the debug console. @@ -623,46 +622,40 @@ static inline seL4_CPtr microkit_cspace_root_slot_to_cptr(seL4_Word slot) return slot << (seL4_WordBits - microkit_max_user_caps_bits); } +typedef seL4_Uint64 microkit_metadata_word_t; + +#define MICROKIT_METADATA_WORD_BITS 64 #define MICROKIT_METADATA_PRESENT_BITS 1 #define MICROKIT_METADATA_NESTED_BITS 1 -#define MICROKIT_METADATA_SIZE_BITS 6 #define MICROKIT_METADATA_PAYLOAD_BITS \ - (seL4_WordBits - MICROKIT_METADATA_PRESENT_BITS - MICROKIT_METADATA_NESTED_BITS - MICROKIT_METADATA_SIZE_BITS) + (MICROKIT_METADATA_WORD_BITS - MICROKIT_METADATA_PRESENT_BITS - MICROKIT_METADATA_NESTED_BITS) + +#define MICROKIT_METADATA_NESTED_MASK \ + (((microkit_metadata_word_t)1) << MICROKIT_METADATA_PAYLOAD_BITS) -#define MICROKIT_METADATA_PRESENT_MASK MICROKIT_BIT(seL4_WordBits - 1) -#define MICROKIT_METADATA_NESTED_MASK MICROKIT_BIT(MICROKIT_METADATA_PAYLOAD_BITS + MICROKIT_METADATA_SIZE_BITS) -#define MICROKIT_METADATA_SIZE_SHIFT MICROKIT_METADATA_PAYLOAD_BITS -#define MICROKIT_METADATA_SIZE_MASK MICROKIT_MASK(MICROKIT_METADATA_SIZE_BITS) -#define MICROKIT_METADATA_PAYLOAD_MASK MICROKIT_MASK(MICROKIT_METADATA_PAYLOAD_BITS) +#define MICROKIT_METADATA_PRESENT_MASK \ + (((microkit_metadata_word_t)1) << (MICROKIT_METADATA_PAYLOAD_BITS + MICROKIT_METADATA_NESTED_BITS)) -static inline seL4_Bool microkit_metadata_unpack_with_flags(seL4_Word word, seL4_Word *payload, seL4_Word *size_bits, - seL4_Bool *nested) +#define MICROKIT_METADATA_PAYLOAD_MASK (MICROKIT_MASK(MICROKIT_METADATA_PAYLOAD_BITS)) + +static inline seL4_Bool microkit_metadata_unpack(microkit_metadata_word_t word, seL4_Word *payload) { if ((word & MICROKIT_METADATA_PRESENT_MASK) == 0) { return seL4_False; } - *nested = (word & MICROKIT_METADATA_NESTED_MASK) != 0; - *size_bits = (word >> MICROKIT_METADATA_SIZE_SHIFT) & MICROKIT_METADATA_SIZE_MASK; - *payload = word & MICROKIT_METADATA_PAYLOAD_MASK; + *payload = (seL4_Word)(word & MICROKIT_METADATA_PAYLOAD_MASK); return seL4_True; } -static inline seL4_Bool microkit_metadata_unpack(seL4_Word word, seL4_Word *payload, seL4_Word *size_bits) -{ - seL4_Bool ignored_nested; - return microkit_metadata_unpack_with_flags(word, payload, size_bits, &ignored_nested); -} - static inline seL4_Bool microkit_root_slot_to_metadata(seL4_Word slot, seL4_Word *metadata) { if (slot == 0 || slot >= MICROKIT_BIT(microkit_max_user_caps_bits) || microkit_root_cnode_metadata == 0) { return seL4_False; } - seL4_Word *root_metadata = (seL4_Word *)microkit_root_cnode_metadata; - seL4_Word ignored_size_bits; - return microkit_metadata_unpack(root_metadata[slot], metadata, &ignored_size_bits); + microkit_metadata_word_t *root_metadata = (microkit_metadata_word_t *)microkit_root_cnode_metadata; + return microkit_metadata_unpack(root_metadata[slot], metadata); } static inline seL4_Bool microkit_root_slot_to_nested_metadata(seL4_Word root_slot, seL4_Word nested_slot, @@ -673,21 +666,28 @@ static inline seL4_Bool microkit_root_slot_to_nested_metadata(seL4_Word root_slo return seL4_False; } - seL4_Word *root_metadata = (seL4_Word *)microkit_root_cnode_metadata; - seL4_Word nested_size_bits; - seL4_Word nested_metadata_vaddr; - seL4_Bool nested; - if (!microkit_metadata_unpack_with_flags(root_metadata[root_slot], &nested_metadata_vaddr, &nested_size_bits, - &nested)) { + microkit_metadata_word_t *root_metadata = (microkit_metadata_word_t *)microkit_root_cnode_metadata; + microkit_metadata_word_t root_word = root_metadata[root_slot]; + + if ((root_word & MICROKIT_METADATA_NESTED_MASK) == 0) { return seL4_False; } - if (!nested || nested_slot >= MICROKIT_BIT(nested_size_bits)) { + + seL4_Word nested_metadata_vaddr; + if (!microkit_metadata_unpack(root_word, &nested_metadata_vaddr)) { return seL4_False; } - seL4_Word *nested_metadata = (seL4_Word *)nested_metadata_vaddr; - seL4_Word ignored_size_bits; - return microkit_metadata_unpack(nested_metadata[nested_slot], metadata, &ignored_size_bits); + microkit_metadata_word_t *nested_metadata = (microkit_metadata_word_t *)nested_metadata_vaddr; + for (seL4_Word i = 0;; i++) { + microkit_metadata_word_t nested_word = nested_metadata[i]; + if ((nested_word & MICROKIT_METADATA_PRESENT_MASK) == 0) { + return seL4_False; + } + if (i == nested_slot) { + return microkit_metadata_unpack(nested_word, metadata); + } + } } static inline seL4_Error microkit_page_get_address(seL4_CPtr frame, seL4_Word *paddr) diff --git a/libmicrokit/src/main.c b/libmicrokit/src/main.c index 1fc3be162..82a9412d9 100644 --- a/libmicrokit/src/main.c +++ b/libmicrokit/src/main.c @@ -38,10 +38,9 @@ seL4_Word microkit_irqs; seL4_Word microkit_notifications; seL4_Word microkit_pps; seL4_Word microkit_ioports; -seL4_Word microkit_root_cnode_size_bits; -seL4_Word microkit_max_user_caps_bits; +seL4_Uint64 microkit_max_user_caps_bits; -seL4_Word microkit_root_cnode_metadata; +seL4_Uint64 microkit_root_cnode_metadata; #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 6f886e650..3948b2ad1 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -94,7 +94,7 @@ 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; -const PD_CAP_BITS: u8 = PD_CAP_SIZE.ilog2() as u8; +pub 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; @@ -698,6 +698,24 @@ pub fn build_capdl_spec( frames, )?; } + for page_table in &pd.page_tables { + pd_elf_spec + .address_space + .map_page_tables_for_range( + &mut spec_container, + kernel_config, + page_table.page_size as u64, + page_table.vaddr..page_table.vaddr + page_table.size, + ) + .map_err(|err| { + format!( + "{err} while reserving page tables for PD '{}' range [{:#x}..{:#x})", + pd.name, + page_table.vaddr, + page_table.vaddr + page_table.size + ) + })?; + } // Step 3-3a: Create and map in the IPC buffer let ipcbuf_frame_obj_id = capdl_util_make_frame_obj( @@ -1276,6 +1294,34 @@ pub fn build_capdl_spec( &mr_name_to_frames[&iomap.mr], )?; } + for page_table in system.io_page_tables.iter() { + let address_space = iospace_by_device + .entry(&page_table.name) + .or_insert_with(|| { + create_iospace( + &mut spec_container, + kernel_config, + &page_table.name, + page_table.identifier, + page_table.domain_id, + ) + }); + address_space + .map_page_tables_for_range( + &mut spec_container, + kernel_config, + page_table.page_size as u64, + page_table.iovaddr..page_table.iovaddr + page_table.size, + ) + .map_err(|err| { + format!( + "{err} while reserving IO page tables for '{}' range [{:#x}..{:#x})", + page_table.name, + page_table.iovaddr, + page_table.iovaddr + page_table.size + ) + })?; + } // ********************************* // Step 6. Handle extra cap mappings @@ -1311,7 +1357,6 @@ pub fn build_capdl_spec( CapMap::MemoryRegionFrames(map) => { let mr_frames = &mr_name_to_frames[&map.mr_name]; let size_bits = calculate_size_bits(mr_frames.len() as u64).max(1); - fill_cnode_with_frames( &mut spec_container, kernel_config, @@ -1320,7 +1365,7 @@ pub fn build_capdl_spec( map.perms, cspace.size_bits as u8, &format!("pd_{}_slot_{}_mr_{}", pd.name, cap_map.slot(), map.mr_name), - ) + )? } CapMap::ElfFrames(map) => { let pd_src_frame_obj_ids = pd_elf_specs @@ -1343,7 +1388,7 @@ pub fn build_capdl_spec( pd.name, cap_map.slot() ), - ) + )? } CapMap::StackFrames(map) => { let pd_src_frame_obj_ids = pd_stack_frames @@ -1365,7 +1410,7 @@ pub fn build_capdl_spec( pd.name, cap_map.slot() ), - ) + )? } CapMap::IpcBufferFrame(map) => { let pd_src_frame_obj_id = pd_ipc_frame @@ -1513,7 +1558,13 @@ fn fill_cnode_with_frames( perms: FrameCapPerms, root_cnode_bits: u8, cnode_name: &str, -) -> Cap { +) -> Result { + if root_cnode_bits as u64 + size_bits as u64 > kernel_config.cap_address_bits { + return Err(format!( + "Attempting to create a nested cnode of size_bits {} below the root cnode of size_bits {}", + size_bits, root_cnode_bits + )); + } // The execute and cached fields are considered attributes by seL4 and from my understanding @cazb2 // do not get masked when invoking the frame thus are redundant. Since they are not fixed at runtime. let mut slot = 0; @@ -1533,5 +1584,9 @@ fn fill_cnode_with_frames( // Configure the CNode to simulate array indexing. let mr_guard_size = kernel_config.cap_address_bits - root_cnode_bits as u64 - size_bits as u64; - capdl_util_make_cnode_cap(mr_cnode_obj, 0, mr_guard_size as u8) + Ok(capdl_util_make_cnode_cap( + mr_cnode_obj, + 0, + mr_guard_size as u8, + )) } diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index 67a73626f..dbe9e4820 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -73,6 +73,11 @@ pub enum AddressSpace { }, } +enum LeafAction { + Insert(Cap), + Reserve, +} + impl AddressSpace { pub fn root(&self) -> ObjectId { match self { @@ -93,17 +98,43 @@ impl AddressSpace { frame_size_bytes: u64, addr: u64, ) -> Result<(), String> { - self.map_recursive( + self.map_or_reserve_recursive( spec_container, sel4_config, self.root(), self.get_root_level(sel4_config), - frame_cap, frame_size_bytes, addr, + LeafAction::Insert(frame_cap), ) } + pub fn map_page_tables_for_range( + &self, + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + page_size_bytes: u64, + range: Range, + ) -> Result<(), String> { + let mut addr = range.start; + while addr < range.end { + self.map_or_reserve_recursive( + spec_container, + sel4_config, + self.root(), + self.get_root_level(sel4_config), + page_size_bytes, + addr, + LeafAction::Reserve, + )?; + addr = addr + .checked_add(page_size_bytes) + .ok_or_else(|| "Error: page_table address range overflows".to_string())?; + } + + Ok(()) + } + fn get_leaf_level(&self, sel4_config: &Config, page_size_bytes: u64) -> usize { const SMALL_PAGE_BYTES: u64 = PageSize::Small as u64; const LARGE_PAGE_BYTES: u64 = PageSize::Large as u64; @@ -183,32 +214,41 @@ impl AddressSpace { } #[allow(clippy::too_many_arguments)] - fn map_recursive( + fn map_or_reserve_recursive( &self, spec_container: &mut CapDLSpecContainer, sel4_config: &Config, cur_level_obj_id: ObjectId, cur_level: usize, - frame_cap: Cap, - frame_size_bytes: u64, + page_size_bytes: u64, addr: u64, + leaf_action: LeafAction, ) -> Result<(), String> { if cur_level >= self.address_space_levels(sel4_config) { unreachable!("internal bug: recursed past the final address-space level"); } let slot = self.get_level_index(sel4_config, cur_level, addr); - let leaf_level = self.get_leaf_level(sel4_config, frame_size_bytes); + let leaf_level = self.get_leaf_level(sel4_config, page_size_bytes); if cur_level == leaf_level { - self.insert_cap_into_level( - spec_container, - sel4_config, - cur_level_obj_id, - cur_level, - slot, - frame_cap, - ) + match leaf_action { + LeafAction::Insert(frame_cap) => self.insert_cap_into_level( + spec_container, + sel4_config, + cur_level_obj_id, + cur_level, + slot, + frame_cap, + ), + LeafAction::Reserve => self.check_leaf_slot_empty( + spec_container, + sel4_config, + cur_level_obj_id, + cur_level, + slot, + ), + } } else { let next_obj_id = self.map_intermediary_level_helper( spec_container, @@ -218,18 +258,55 @@ impl AddressSpace { slot, addr, )?; - self.map_recursive( + self.map_or_reserve_recursive( spec_container, sel4_config, next_obj_id, cur_level + 1, - frame_cap, - frame_size_bytes, + page_size_bytes, addr, + leaf_action, ) } } + fn check_leaf_slot_empty( + &self, + spec_container: &CapDLSpecContainer, + sel4_config: &Config, + cur_level_obj_id: ObjectId, + cur_level: usize, + cur_level_slot: usize, + ) -> Result<(), String> { + let object = &spec_container + .get_root_object(cur_level_obj_id) + .unwrap() + .object; + + self.valid_level_object(object, sel4_config, cur_level)?; + let slots = object.slots().unwrap(); + + if slots + .iter() + .any(|cte| usize::from(cte.slot) == cur_level_slot) + { + Err(format!( + "address-space '{}': slot {} at level {} in object '{}' is already filled", + self.name(), + cur_level_slot, + cur_level, + spec_container + .get_root_object(cur_level_obj_id) + .unwrap() + .name + .as_ref() + .unwrap() + )) + } else { + Ok(()) + } + } + fn map_intermediary_level_helper( &self, spec_container: &mut CapDLSpecContainer, diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index fdb5a4525..1b7d77620 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -26,8 +26,8 @@ use microkit_tool::sel4::{ }; use microkit_tool::symbols::patch_symbols; use microkit_tool::util::{ - calculate_size_bits, get_full_path, human_size_strict, json_str, json_str_as_bool, - json_str_as_u64, round_down, round_up, + get_full_path, human_size_strict, json_str, json_str_as_bool, json_str_as_u64, round_down, + round_up, }; use microkit_tool::viper; use microkit_tool::{DisjointMemoryRegion, MemoryRegion}; @@ -449,22 +449,16 @@ fn main() -> Result<(), String> { } candidate_before(possible_end) }; - let encode_metadata = |vaddr: u64, size_bits: u8, nested: bool| -> u64 { + let encode_metadata = |vaddr: u64, nested: bool| -> u64 { const PRESENT_BITS: u64 = 1; const NESTED_BITS: u64 = 1; - const SIZE_BITS: u64 = 6; - const PAYLOAD_BITS: u64 = u64::BITS as u64 - PRESENT_BITS - NESTED_BITS - SIZE_BITS; - const PRESENT_BIT: u64 = 1 << (u64::BITS - 1); - const NESTED_BIT: u64 = 1 << (PAYLOAD_BITS + SIZE_BITS); - if u64::from(size_bits) >= (1u64 << SIZE_BITS) { - panic!("Error: metadata size bits {size_bits} do not fit in {SIZE_BITS} bits"); - } + const PAYLOAD_BITS: u64 = u64::BITS as u64 - PRESENT_BITS - NESTED_BITS; + const PRESENT_BIT: u64 = 1 << (PAYLOAD_BITS + 1); + const NESTED_BIT: u64 = 1 << PAYLOAD_BITS; if vaddr >= (1 << PAYLOAD_BITS) { panic!("Error: metadata vaddr {vaddr:#x} does not fit in {PAYLOAD_BITS} payload bits"); } - PRESENT_BIT | (if nested { NESTED_BIT } else { 0 }) - | (u64::from(size_bits) << PAYLOAD_BITS) - | vaddr + PRESENT_BIT | (if nested { NESTED_BIT } else { 0 }) | vaddr }; let pd_elf_segments_by_idx: Vec>> = system_elfs @@ -488,6 +482,7 @@ fn main() -> Result<(), String> { pd.maps .iter() .map(|map| map.vaddr..map.vaddr + get_mr_size(map.mr_name())) + .chain(pd.page_tables.iter().map(|pt| pt.vaddr..pt.vaddr + pt.size)) .collect::>>() }) .collect(); @@ -525,8 +520,11 @@ fn main() -> Result<(), String> { }) .collect::>(); - let region_size_bytes = - round_up((frame_vaddrs.len() * 8) as u64, PageSize::Small as u64); + // The last entry is a zero terminator. + let region_size_bytes = round_up( + ((frame_vaddrs.len() + 1) * 8) as u64, + PageSize::Small as u64, + ); let nested_cspace_region = find_free_region( &mut pd_regions[pd_idx], @@ -535,15 +533,13 @@ fn main() -> Result<(), String> { ); pd_regions[pd_idx].push(nested_cspace_region.clone()); - root_metadata[cap_map.slot() as usize] = encode_metadata( - nested_cspace_region.start, - calculate_size_bits(frame_vaddrs.len() as u64), - true, - ); + root_metadata[cap_map.slot() as usize] = + encode_metadata(nested_cspace_region.start, true); let nested_metadata = frame_vaddrs .into_iter() - .flat_map(|vaddr| encode_metadata(vaddr, 0, false).to_le_bytes()) + .flat_map(|vaddr| encode_metadata(vaddr, false).to_le_bytes()) + .chain(0u64.to_le_bytes()) .collect::>(); let nested_mr_name = @@ -557,11 +553,11 @@ fn main() -> Result<(), String> { microkit_tool::sdf::CapMap::StackFrames(map) => { let other_pd_idx = map.pd_info().pd.expect("Filled in sdf.rs"); root_metadata[cap_map.slot() as usize] = - encode_metadata(pd_stack_bases_by_idx[other_pd_idx], 0, false); + encode_metadata(pd_stack_bases_by_idx[other_pd_idx], false); } microkit_tool::sdf::CapMap::IpcBufferFrame(_) => { root_metadata[cap_map.slot() as usize] = - encode_metadata(kernel_config.pd_ipc_buffer(), 0, false); + encode_metadata(kernel_config.pd_ipc_buffer(), false); } _ => (), } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 797b954ca..06ed60f59 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -4,6 +4,7 @@ // SPDX-License-Identifier: BSD-2-Clause // +use crate::capdl::PD_CAP_BITS; /// This module is responsible for parsing the System Description Format (SDF) /// which is based on XML. /// We do not use any fancy XML, and instead keep things as minimal and simple @@ -29,7 +30,7 @@ use std::collections::{hash_map, HashMap, HashSet}; use std::fmt; use std::fs; use std::num::NonZero; -use std::ops::Deref; +use std::ops::{Deref, Range}; use std::path::{Path, PathBuf}; use std::str::FromStr; @@ -413,6 +414,68 @@ pub struct SysIOMap { pub text_pos: Option, } +#[derive(Debug, PartialEq, Eq)] +pub struct PageTable { + pub vaddr: u64, + pub size: u64, + pub page_size: PageSize, + pub text_pos: roxmltree::TextPos, +} + +#[derive(Debug, PartialEq, Eq)] +pub struct IOPageTable { + pub name: String, + pub identifier: IommuDeviceIdentifier, + pub domain_id: Option, + pub iovaddr: u64, + pub size: u64, + pub page_size: PageSize, + pub text_pos: roxmltree::TextPos, +} + +trait PageTableReservation { + fn element(&self) -> &'static str; + fn range_name(&self) -> &'static str; + fn range(&self) -> Range; + fn text_pos(&self) -> roxmltree::TextPos; +} + +impl PageTableReservation for PageTable { + fn element(&self) -> &'static str { + "page_table" + } + + fn range_name(&self) -> &'static str { + "virtual address range" + } + + fn range(&self) -> Range { + self.vaddr..self.vaddr + self.size + } + + fn text_pos(&self) -> roxmltree::TextPos { + self.text_pos + } +} + +impl PageTableReservation for IOPageTable { + fn element(&self) -> &'static str { + "io_page_table" + } + + fn range_name(&self) -> &'static str { + "address range" + } + + fn range(&self) -> Range { + self.iovaddr..self.iovaddr + self.size + } + + fn text_pos(&self) -> roxmltree::TextPos { + self.text_pos + } +} + pub trait Map { fn mr_name(&self) -> &str; fn addr(&self) -> u64; @@ -684,6 +747,7 @@ pub struct ProtectionDomain { /// Enable FPU for this PD. pub fpu: bool, pub maps: Vec, + pub page_tables: Vec, pub irqs: Vec, pub ioports: Vec, pub setvars: Vec, @@ -1010,11 +1074,154 @@ impl SysIOMap { } } +fn validate_page_table_region( + config: &Config, + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + addr: u64, + size: u64, + page_size: u64, + max_end: u64, + addr_name: &str, +) -> Result<(), String> { + if !config.page_sizes().contains(&page_size) { + return Err(value_error( + xml_sdf, + node, + format!("page size {page_size:#x} not supported"), + )); + } + + if size == 0 { + return Err(value_error( + xml_sdf, + node, + "size must be greater than 0".to_string(), + )); + } + + if !addr.is_multiple_of(page_size) { + return Err(value_error( + xml_sdf, + node, + format!("{addr_name} is not aligned to the page size"), + )); + } + + if !size.is_multiple_of(page_size) { + return Err(value_error( + xml_sdf, + node, + "size is not a multiple of the page size".to_string(), + )); + } + + let Some(end) = addr.checked_add(size) else { + return Err(value_error( + xml_sdf, + node, + "address range overflows".to_string(), + )); + }; + + if end > max_end { + return Err(value_error( + xml_sdf, + node, + format!("address range [{addr:#x}..{end:#x}) exceeds valid address space [0x0..{max_end:#x})"), + )); + } + + Ok(()) +} + +fn parse_page_table_region( + config: &Config, + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + addr_name: &'static str, + max_end: u64, +) -> Result<(u64, u64, PageSize, roxmltree::TextPos), String> { + check_attributes(xml_sdf, node, &[addr_name, "size", "page_size"])?; + + let addr = sdf_parse_number(checked_lookup(xml_sdf, node, addr_name)?, node)?; + let size = sdf_parse_number(checked_lookup(xml_sdf, node, "size")?, node)?; + let page_size = sdf_parse_number(checked_lookup(xml_sdf, node, "page_size")?, node)?; + + validate_page_table_region( + config, xml_sdf, node, addr, size, page_size, max_end, addr_name, + )?; + + Ok(( + addr, + size, + page_size.into(), + xml_sdf.doc.text_pos_at(node.range().start), + )) +} + +impl PageTable { + fn from_xml( + config: &Config, + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + max_vaddr: u64, + ) -> Result { + let (vaddr, size, page_size, text_pos) = + parse_page_table_region(config, xml_sdf, node, "vaddr", max_vaddr)?; + + Ok(PageTable { + vaddr, + size, + page_size, + text_pos, + }) + } +} + +impl IOPageTable { + fn from_xml( + config: &Config, + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + name: &str, + identifier: IommuDeviceIdentifier, + domain_id: Option, + ) -> Result { + let (iovaddr, size, page_size, text_pos) = parse_page_table_region( + config, + xml_sdf, + node, + "iovaddr", + x86_io_address_space::CAPDL_MAX_IOVA + 1, + )?; + + if page_size != PageSize::Small { + return Err(value_error( + xml_sdf, + node, + "currently seL4 does not have large page support for the IOMMU".to_string(), + )); + } + + Ok(IOPageTable { + name: name.to_string(), + identifier, + domain_id, + iovaddr, + size, + page_size, + text_pos, + }) + } +} + // This is implemented in such a way that each device will have its own address space. // If devices need to share physical memory, this can be done by mapping the same memory_region // into each address space. struct IOAddressSpace { iomaps: Vec, + io_page_tables: Vec, } impl IOAddressSpace { @@ -1087,6 +1294,7 @@ impl IOAddressSpace { iommu_device_identifiers.push(identifier); let mut iomaps = Vec::new(); + let mut io_page_tables = Vec::new(); for child in node.children().filter(|node| node.is_element()) { match child.tag_name().name() { @@ -1095,6 +1303,12 @@ impl IOAddressSpace { SysIOMap::from_xml(config, xml_sdf, &child, name, identifier, domain_id)?; iomaps.push(iomap); } + "io_page_table" => { + let io_page_table = IOPageTable::from_xml( + config, xml_sdf, &child, name, identifier, domain_id, + )?; + io_page_tables.push(io_page_table); + } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!( @@ -1106,7 +1320,10 @@ impl IOAddressSpace { } } - Ok(IOAddressSpace { iomaps }) + Ok(IOAddressSpace { + iomaps, + io_page_tables, + }) } } @@ -1314,6 +1531,7 @@ impl ProtectionDomain { } let mut maps = Vec::new(); + let mut page_tables = Vec::new(); let mut irqs = Vec::new(); let mut ioports = Vec::new(); let mut setvars: Vec = Vec::new(); @@ -1407,6 +1625,10 @@ impl ProtectionDomain { maps.push(map); } + "page_table" => { + let map_max_vaddr = config.pd_map_max_vaddr(stack_size); + page_tables.push(PageTable::from_xml(config, xml_sdf, &child, map_max_vaddr)?); + } "irq" => { let id = checked_lookup(xml_sdf, &child, "id")? .parse::() @@ -1763,7 +1985,7 @@ impl ProtectionDomain { )); } - cspace = Some(CSpace::from_xml(xml_sdf, &child)?); + cspace = Some(CSpace::from_xml(config, xml_sdf, &child)?); } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); @@ -1803,6 +2025,7 @@ impl ProtectionDomain { program_image_for_symbols, fpu, maps, + page_tables, irqs, ioports, setvars, @@ -2088,7 +2311,11 @@ impl CapMap { } impl CSpace { - fn from_xml(xml_sdf: &XmlSystemDescription, node: &roxmltree::Node) -> Result { + fn from_xml( + config: &Config, + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + ) -> Result { check_attributes(xml_sdf, node, &[])?; let mut cap_maps = vec![]; @@ -2098,11 +2325,25 @@ impl CSpace { } // Default to 1, the minimum allowed by the kernel. - let size_bits = cap_maps - .iter() - .map(|cap_map| calculate_size_bits(cap_map.common().slot + 1)) - .max() - .unwrap_or(1) as u64; + let mut size_bits = 1; + for cap_map in &cap_maps { + let slot_count = cap_map.common().slot.checked_add(1).ok_or_else(|| { + value_error( + xml_sdf, + node, + "overflow due to the large slot number in cspace".into(), + ) + })?; + size_bits = size_bits.max(calculate_size_bits(slot_count) as u64); + } + + if size_bits as u64 + PD_CAP_BITS as u64 > config.cap_address_bits { + return Err(value_error( + xml_sdf, + node, + format!("the CSpace has a slot that is too large, which stops us from indexing into the normal microkit cnode"), + )); + } Ok(CSpace { cap_maps, @@ -2763,6 +3004,7 @@ pub struct SystemDescription { pub protection_domains: Vec, pub memory_regions: Vec, pub iomaps: Vec, + pub io_page_tables: Vec, pub channels: Vec, pub domains: Domains, } @@ -2855,6 +3097,96 @@ where Ok(()) } +fn mapped_range(mrs: &[SysMemoryRegion], map: &M) -> Range { + let mr = mrs + .iter() + .find(|mr| mr.name == map.mr_name()) + .expect("map memory region already validated"); + let start = map.addr(); + start + ..start + .checked_add(mr.size) + .expect("map range already validated") +} + +fn check_page_table_reservation<'a, PT, M, I>( + xml_sdf: &XmlSystemDescription, + mrs: &[SysMemoryRegion], + page_table: &PT, + maps: I, + checked_page_tables: &[Range], + address_space: &str, +) -> Result<(), String> +where + PT: PageTableReservation, + M: Map + 'a, + I: IntoIterator, +{ + let page_table_range = page_table.range(); + + for map in maps { + let mapped_range = mapped_range(mrs, map); + if ranges_overlap(&page_table_range, &mapped_range) { + return Err(format!( + "Error: {} {} [{:#x}..{:#x}) overlaps with {} for '{}' [{:#x}..{:#x}) in {} {}", + page_table.element(), + page_table.range_name(), + page_table_range.start, + page_table_range.end, + map.element(), + map.mr_name(), + mapped_range.start, + mapped_range.end, + address_space, + location_suffix_format(xml_sdf, Some(page_table.text_pos())) + )); + } + } + + for checked_range in checked_page_tables { + if ranges_overlap(&page_table_range, checked_range) { + return Err(format!( + "Error: {} {} [{:#x}..{:#x}) overlaps with {} [{:#x}..{:#x}) in {} {}", + page_table.element(), + page_table.range_name(), + page_table_range.start, + page_table_range.end, + page_table.element(), + checked_range.start, + checked_range.end, + address_space, + location_suffix_format(xml_sdf, Some(page_table.text_pos())) + )); + } + } + + Ok(()) +} + +fn check_page_tables( + xml_sdf: &XmlSystemDescription, + mrs: &[SysMemoryRegion], + page_tables: &[PageTable], + maps: &[SysMap], + address_space: &str, +) -> Result<(), String> { + let mut checked_page_tables: Vec> = Vec::new(); + + for page_table in page_tables { + check_page_table_reservation( + xml_sdf, + mrs, + page_table, + maps, + &checked_page_tables, + address_space, + )?; + checked_page_tables.push(page_table.range()); + } + + Ok(()) +} + fn check_io_maps( xml_sdf: &XmlSystemDescription, mrs: &[SysMemoryRegion], @@ -2893,6 +3225,33 @@ fn check_io_maps( Ok(()) } +fn check_io_page_tables( + xml_sdf: &XmlSystemDescription, + mrs: &[SysMemoryRegion], + iomaps: &[SysIOMap], + io_page_tables: &[IOPageTable], +) -> Result<(), String> { + let mut checked_page_tables: HashMap<&str, Vec>> = HashMap::new(); + + for page_table in io_page_tables { + let checked_for_space = checked_page_tables + .entry(page_table.name.as_str()) + .or_default(); + check_page_table_reservation( + xml_sdf, + mrs, + page_table, + iomaps.iter().filter(|iomap| iomap.name == page_table.name), + checked_for_space, + &format!("io address space '{}'", page_table.name), + )?; + + checked_for_space.push(page_table.range()); + } + + Ok(()) +} + fn check_attributes( xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, @@ -3070,6 +3429,7 @@ pub fn parse( let mut root_pds = vec![]; let mut mrs = vec![]; let mut iomaps = vec![]; + let mut io_page_tables = vec![]; let mut io_address_space_names = HashSet::new(); let mut iommu_domain_ids = HashSet::new(); let mut iommu_device_identifiers = Vec::new(); @@ -3107,17 +3467,16 @@ pub fn parse( search_paths, )?), "io_address_space" => { - iomaps.extend( - IOAddressSpace::from_xml( - config, - &xml_sdf, - &child, - &mut io_address_space_names, - &mut iommu_domain_ids, - &mut iommu_device_identifiers, - )? - .iomaps, - ); + let io_address_space = IOAddressSpace::from_xml( + config, + &xml_sdf, + &child, + &mut io_address_space_names, + &mut iommu_domain_ids, + &mut iommu_device_identifiers, + )?; + iomaps.extend(io_address_space.iomaps); + io_page_tables.extend(io_address_space.io_page_tables); } "virtual_machine" => { let pos = xml_sdf.doc.text_pos_at(child.range().start); @@ -3444,6 +3803,13 @@ pub fn parse( &format!("protection domain '{}'", pd.name), config.pd_map_max_vaddr(pd.stack_size), )?; + check_page_tables( + &xml_sdf, + &mrs, + &pd.page_tables, + &pd.maps, + &format!("protection domain '{}'", pd.name), + )?; if let Some(vm) = &pd.virtual_machine { check_maps( &xml_sdf, @@ -3456,6 +3822,7 @@ pub fn parse( } check_io_maps(&xml_sdf, &mrs, &iomaps)?; + check_io_page_tables(&xml_sdf, &mrs, &iomaps, &io_page_tables)?; // 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 @@ -3636,6 +4003,7 @@ pub fn parse( protection_domains: pds, memory_regions: mrs, iomaps, + io_page_tables, channels, domains, }) diff --git a/tool/microkit/src/symbols.rs b/tool/microkit/src/symbols.rs index eb94bec46..e8209254f 100644 --- a/tool/microkit/src/symbols.rs +++ b/tool/microkit/src/symbols.rs @@ -135,15 +135,6 @@ 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(); elf_obj .write_symbol( "microkit_max_user_caps_bits",