From b823343df80f1181b50d15f7660f36ab495bdb81 Mon Sep 17 00:00:00 2001 From: Callum Date: Mon, 6 Jul 2026 21:21:41 +1000 Subject: [PATCH 1/8] IOMMU: Minor modification to Map trait Minor adjustments to the prior sdf work to do with how permissions are handled. Previously I implemented read and write functions as part of the SysIOMapPerms enum, however the old SysMapPerms did not do this. Given these types are meant to exhibit similar behaviour extracting this common logic into the Map trait provides a streamlined interface to check if a permission is set. Signed-off-by: Callum --- tool/microkit/src/sdf.rs | 47 ++++++++++++++++++++++++++++++++-------- 1 file changed, 38 insertions(+), 9 deletions(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 2aa1ec84c..242d081c8 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -306,14 +306,6 @@ impl SysIOMapPerms { (false, false) => Err(()), } } - - pub fn read(self) -> bool { - matches!(self, SysIOMapPerms::Read | SysIOMapPerms::ReadWrite) - } - - pub fn write(self) -> bool { - matches!(self, SysIOMapPerms::Write | SysIOMapPerms::ReadWrite) - } } #[derive(Debug, PartialEq, Eq, Clone)] @@ -327,13 +319,17 @@ pub struct SysIOMap { pub text_pos: Option, } -trait Map { +pub trait Map { fn mr_name(&self) -> &str; fn addr(&self) -> u64; fn text_pos(&self) -> Option; fn element(&self) -> &'static str; fn addr_name(&self) -> &'static str; fn range_name(&self) -> &'static str; + fn read(&self) -> bool; + fn write(&self) -> bool; + fn execute(&self) -> bool; + fn cached(&self) -> bool; } impl Map for SysMap { @@ -360,6 +356,22 @@ impl Map for SysMap { fn range_name(&self) -> &'static str { "virtual address range" } + + fn read(&self) -> bool { + self.perms & SysMapPerms::Read as u8 != 0 + } + + fn write(&self) -> bool { + self.perms & SysMapPerms::Write as u8 != 0 + } + + fn execute(&self) -> bool { + self.perms & SysMapPerms::Execute as u8 != 0 + } + + fn cached(&self) -> bool { + self.cached + } } impl Map for SysIOMap { @@ -386,7 +398,24 @@ impl Map for SysIOMap { fn range_name(&self) -> &'static str { "io address range" } + + fn read(&self) -> bool { + matches!(self.perms, SysIOMapPerms::Read | SysIOMapPerms::ReadWrite) + } + + fn write(&self) -> bool { + matches!(self.perms, SysIOMapPerms::Write | SysIOMapPerms::ReadWrite) + } + + fn execute(&self) -> bool { + false + } + + fn cached(&self) -> bool { + false + } } + #[derive(Debug, PartialEq, Eq, Clone)] pub enum SysMemoryRegionKind { User, From 2b466614f48513f86d4578fa7499e2765cd3ac47 Mon Sep 17 00:00:00 2001 From: Callum Date: Mon, 29 Jun 2026 15:18:41 +1000 Subject: [PATCH 2/8] IOMMU: Refactor Address Space creation This commit is meant to preserve original functionality. The memory.rs file previously was a collection of functions that allowed the mapping of pages into vspaces. This commit refactors this logic into an AddressSpace type. This will allow us to simply support new variants of address spaces, including IO Address Spaces for devices. The majority of changes are made to allow the old functions to be reusued in a more generic way. The changes to the builder.rs reflect the changes to memory.rs or make use of the trait Map as trait bounds to handle both normal Mappings and IOMappings. Signed-off-by: Callum --- tool/microkit/src/capdl/builder.rs | 198 ++++++----- tool/microkit/src/capdl/memory.rs | 548 ++++++++++++++++------------- 2 files changed, 408 insertions(+), 338 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 4a66b7546..96cd71171 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -18,14 +18,14 @@ use sel4_capdl_initializer_types::{ use crate::{ capdl::{ irq::create_irq_handler_cap, - memory::{create_vspace, create_vspace_ept, map_page}, + memory::{create_vspace, create_vspace_ept, AddressSpace}, spec::{capdl_obj_physical_size_bits, BytesContent, ElfContent, FillContent}, util::*, }, elf::ElfFile, sdf::{ - CapMapType, CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, - MONITOR_PD_NAME, MONITOR_PRIORITY, + CapMapType, CpuCore, Map, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME, + MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, util::{ranges_overlap, round_down, round_up}, @@ -145,6 +145,11 @@ impl PDShadowCspace { } } +struct ElfSpecResult { + tcb: ObjectId, + address_space: AddressSpace, +} + pub struct CapDLSpecContainer { pub spec: Spec, /// Track allocations as we build the system for later use by the report. @@ -209,7 +214,7 @@ impl CapDLSpecContainer { /// as possible. These are the objects that will be created: /// -> TCB: Program counter set and VSpace capability bound. /// -> VSpace: all pages from the ELF mapped in. - /// Returns the object ID of the TCB + /// Returns ElfSpecResult containing the TCB object ID and the PDs address space. /// NOTE that all ELF frames will just be reference to the original ELF object rather than the actual data. /// So that symbols can be patched before the frames' data are filled in. fn add_elf_to_spec( @@ -219,9 +224,10 @@ impl CapDLSpecContainer { pd_cpu: CpuCore, elf_id: usize, elf: &ElfFile, - ) -> Result { + ) -> Result { // We assumes that ELFs and PDs have a one-to-one relationship. So for each ELF we create a VSpace. - let vspace_obj_id = create_vspace(self, sel4_config, pd_name); + let address_space = create_vspace(self, sel4_config, pd_name); + let vspace_obj_id = address_space.root(); let vspace_cap = capdl_util_make_page_table_cap(vspace_obj_id); // For each loadable segment in the ELF, map it into the address space of this PD. @@ -291,11 +297,9 @@ impl CapDLSpecContainer { true, ); - match map_page( + match address_space.map_page( self, sel4_config, - pd_name, - vspace_obj_id, frame_cap, page_size_bytes, cur_vaddr, @@ -309,7 +313,7 @@ impl CapDLSpecContainer { "add_elf_to_spec(): failed to map segment page to ELF because: {map_err_reason}" )) } - }; + } } } @@ -341,42 +345,47 @@ impl CapDLSpecContainer { object: Object::Tcb(tcb_inner_obj), }; - Ok(self.add_root_object(tcb_obj)) + Ok(ElfSpecResult { + tcb: self.add_root_object(tcb_obj), + address_space, + }) } } -/// Given a SysMap, page size, VSpace object ID, and a Vec of frame object ids, -/// map all frames into the given VSpace at the requested vaddr. -fn map_memory_region( +/// Given a map, page size, address space, and a Vec of frame object ids, map +/// all frames into the requested address space at the requested address. +fn map_memory_region( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, - pd_name: &str, - map: &SysMap, + map: &M, page_sz: u64, - target_vspace: ObjectId, + target_address_space: &AddressSpace, frames: &[ObjectId], -) { - let mut cur_vaddr = map.vaddr; - let read = map.perms & SysMapPerms::Read as u8 != 0; - let write = map.perms & SysMapPerms::Write as u8 != 0; - let execute = map.perms & SysMapPerms::Execute as u8 != 0; - let cached = map.cached; +) -> Result<(), String> { + let mut cur_vaddr = map.addr(); + let read = map.read(); + let write = map.write(); + let execute = map.execute(); for frame_obj_id in frames.iter() { // Make a cap for this frame. - let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, read, write, execute, cached); + let frame_cap = + capdl_util_make_frame_cap(*frame_obj_id, read, write, execute, map.cached()); // Map it into this PD address space. - map_page( - spec_container, - sel4_config, - pd_name, - target_vspace, - frame_cap, - page_sz, - cur_vaddr, - ) - .unwrap(); + target_address_space + .map_page(spec_container, sel4_config, frame_cap, page_sz, cur_vaddr) + .map_err(|err| { + format!( + "failed to map {} for MR '{}' into address-space '{}' at {} {:#x}: {err}", + map.element(), + map.mr_name(), + target_address_space.name(), + map.addr_name(), + cur_vaddr + ) + })?; cur_vaddr += page_sz; } + Ok(()) } /// Build a CapDL Spec according to the System Description File. @@ -394,18 +403,16 @@ pub fn build_capdl_spec( // We expect the PD ELFs to be first and the monitor ELF last in the list of ELFs. let mon_elf_id = elfs.len() - 1; assert!(elfs.len() == system.protection_domains.len() + 1); - let monitor_tcb_obj_id = { - let monitor_elf = &elfs[mon_elf_id]; - spec_container - .add_elf_to_spec( - kernel_config, - MONITOR_PD_NAME, - CpuCore(0), - mon_elf_id, - monitor_elf, - ) - .unwrap() - }; + let monitor_elf_spec = spec_container + .add_elf_to_spec( + kernel_config, + MONITOR_PD_NAME, + CpuCore(0), + mon_elf_id, + &elfs[mon_elf_id], + ) + .unwrap(); + let monitor_tcb_obj_id = monitor_elf_spec.tcb; // Create monitor fault endpoint object + cap let mon_fault_ep_obj_id = @@ -453,18 +460,16 @@ pub fn build_capdl_spec( ); let mon_stack_frame_cap = capdl_util_make_frame_cap(mon_stack_frame_obj_id, true, true, false, true); - let mon_vspace_obj_id = - capdl_util_get_vspace_id_from_tcb_id(&spec_container, monitor_tcb_obj_id); - map_page( - &mut spec_container, - kernel_config, - MONITOR_PD_NAME, - mon_vspace_obj_id, - mon_stack_frame_cap, - PageSize::Small as u64, - kernel_config.pd_stack_bottom(MON_STACK_SIZE), - ) - .unwrap(); + monitor_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + mon_stack_frame_cap, + PageSize::Small as u64, + kernel_config.pd_stack_bottom(MON_STACK_SIZE), + ) + .unwrap(); // Create monitor IPC Bufffer let mon_ipcbuf_frame_obj_id = capdl_util_make_frame_obj( @@ -476,16 +481,16 @@ pub fn build_capdl_spec( ); let mon_ipcbuf_frame_cap = capdl_util_make_frame_cap(mon_ipcbuf_frame_obj_id, true, true, false, true); - map_page( - &mut spec_container, - kernel_config, - MONITOR_PD_NAME, - mon_vspace_obj_id, - mon_ipcbuf_frame_cap.clone(), - PageSize::Small as u64, - kernel_config.pd_ipc_buffer(), - ) - .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); + monitor_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + mon_ipcbuf_frame_cap.clone(), + PageSize::Small as u64, + kernel_config.pd_ipc_buffer(), + ) + .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); // At this point, all of the required objects for the monitor have been created and its caps inserted into // the correct slot in the CSpace. We need to bind those objects into the TCB for the monitor to use them. @@ -628,9 +633,11 @@ 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_tcb_obj_id = spec_container + let pd_elf_spec = spec_container .add_elf_to_spec(kernel_config, &pd.name, pd.cpu, pd_global_idx, elf_obj) .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); // In the benchmark configuration, we allow PDs to access their own TCB. @@ -676,12 +683,11 @@ pub fn build_capdl_spec( map_memory_region( &mut spec_container, kernel_config, - &pd.name, map, page_size_bytes, - pd_vspace_obj_id, + &pd_elf_spec.address_space, frames, - ); + )?; } // Step 3-3a: Create and map in the IPC buffer @@ -694,16 +700,16 @@ pub fn build_capdl_spec( ); let ipcbuf_frame_cap = capdl_util_make_frame_cap(ipcbuf_frame_obj_id, true, true, false, true); - map_page( - &mut spec_container, - kernel_config, - &pd.name, - pd_vspace_obj_id, - ipcbuf_frame_cap.clone(), - PageSize::Small as u64, - kernel_config.pd_ipc_buffer(), - ) - .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); + pd_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + ipcbuf_frame_cap.clone(), + PageSize::Small as u64, + kernel_config.pd_ipc_buffer(), + ) + .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::IpcBuffer as u32, ipcbuf_frame_cap, @@ -725,16 +731,16 @@ pub fn build_capdl_spec( ); let stack_frame_cap = capdl_util_make_frame_cap(stack_frame_obj_id, true, true, false, true); - map_page( - &mut spec_container, - kernel_config, - &pd.name, - pd_vspace_obj_id, - stack_frame_cap, - PageSize::Small as u64, - cur_stack_vaddr, - ) - .unwrap(); + pd_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + stack_frame_cap, + PageSize::Small as u64, + cur_stack_vaddr, + ) + .unwrap(); cur_stack_vaddr += PageSize::Small as u64; } @@ -867,12 +873,13 @@ pub fn build_capdl_spec( // Create VM's Address Space and map in all memory regions. // This address space is shared across all vCPUs. The virtual address that we "map" the region is guest-physical. - let vm_vspace_obj_id = match kernel_config.arch { + let vm_address_space = match kernel_config.arch { Arch::X86_64 => { create_vspace_ept(&mut spec_container, kernel_config, &virtual_machine.name) } _ => create_vspace(&mut spec_container, kernel_config, &virtual_machine.name), }; + let vm_vspace_obj_id = vm_address_space.root(); let vm_vspace_cap = capdl_util_make_page_table_cap(vm_vspace_obj_id); for map in virtual_machine.maps.iter() { let frames = &mr_name_to_frames[&map.mr]; @@ -881,12 +888,11 @@ pub fn build_capdl_spec( map_memory_region( &mut spec_container, kernel_config, - &virtual_machine.name, map, page_size_bytes, - vm_vspace_obj_id, + &vm_address_space, frames, - ); + )?; } if kernel_config.arch == Arch::X86_64 { diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index d8b0c7bd1..d1b1fcd5a 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -4,7 +4,10 @@ // SPDX-License-Identifier: BSD-2-Clause // use crate::{ - capdl::{util::capdl_util_make_cte, CapDLNamedObject, CapDLSpecContainer}, + capdl::{ + spec::capdl_obj_human_name, util::capdl_util_make_cte, CapDLNamedObject, + CapDLSpecContainer, FrameFill, + }, sel4::{Arch, Config, PageSize}, }; use sel4_capdl_initializer_types::{cap, object, Cap, Object, ObjectId}; @@ -45,291 +48,352 @@ fn get_pt_level_name(sel4_config: &Config, level: usize) -> &str { } } -fn get_pt_level_index(sel4_config: &Config, level: usize, vaddr: u64) -> usize { - let levels = sel4_config.num_page_table_levels(); +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum AddressSpace { + VSpace { + name: String, + root: ObjectId, + x86_ept: bool, + }, +} - assert!(level < levels); +impl AddressSpace { + pub fn root(&self) -> ObjectId { + match self { + &Self::VSpace { root, .. } => root, + } + } + pub fn name(&self) -> &str { + match self { + Self::VSpace { name, .. } => name, + } + } - let index_bits = |level: usize| -> u64 { - if level == top_pt_level_number(sel4_config) - && sel4_config.arch == Arch::Aarch64 - && sel4_config.aarch64_vspace_s2_start_l1() - { - // Special case for first level on AArch64 platforms with hyp and 40 bits PA. - // It have 10 bits index for VSpace. - // match up with seL4_VSpaceBits in seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h - 10 - } else { - 9 + pub fn map_page( + &self, + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + frame_cap: Cap, + frame_size_bytes: u64, + addr: u64, + ) -> Result<(), String> { + self.map_recursive( + spec_container, + sel4_config, + self.root(), + Self::get_root_level(sel4_config), + frame_cap, + frame_size_bytes, + addr, + ) + } + + 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; + let levels = self.address_space_levels(sel4_config); + + match page_size_bytes { + SMALL_PAGE_BYTES => levels - 1, + LARGE_PAGE_BYTES => levels - 2, + _ => unreachable!( + "internal bug: get_pt_level_to_insert(): unknown page_size_bytes: {page_size_bytes}" + ), } - }; + } - let page_bits = 12; - let bits_from_higher_lvls: u64 = ((level + 1)..levels).map(index_bits).sum(); - let shift = page_bits + bits_from_higher_lvls; - let width = index_bits(level); - let mask = (1u64 << width) - 1; + fn get_level_name(&self, sel4_config: &Config, level: usize) -> String { + match self { + Self::VSpace { .. } => get_pt_level_name(sel4_config, level).to_string(), + } + } - ((vaddr >> shift) & mask) as usize -} + fn get_addr_label(&self) -> &'static str { + match self { + Self::VSpace { .. } => "vaddr", + } + } -fn get_pt_level_coverage(sel4_config: &Config, level: usize, vaddr: u64) -> Range { - let levels = sel4_config.num_page_table_levels() as u64; - let page_bits = 12; - let bits_from_higher_lvls: u64 = (levels - (level as u64)) * 9; + fn get_level_index(&self, sel4_config: &Config, level: usize, vaddr: u64) -> usize { + let levels = self.address_space_levels(sel4_config); - let coverage_bits = page_bits + bits_from_higher_lvls; + assert!(level < levels); - let low = (vaddr >> coverage_bits) << coverage_bits; - let high = vaddr | ((1 << coverage_bits) - 1); + let index_bits = |level: usize| -> u64 { + if matches!(self, AddressSpace::VSpace { .. }) + && level == Self::get_root_level(sel4_config) + && sel4_config.arch == Arch::Aarch64 + && sel4_config.aarch64_vspace_s2_start_l1() + { + // Special case for first level on AArch64 platforms with hyp and 40 bits PA. + // It have 10 bits index for VSpace. + // match up with seL4_VSpaceBits in seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h + 10 + } else { + 9 + } + }; - low..high -} + let page_bits = 12; + let bits_from_higher_lvls: u64 = ((level + 1)..levels).map(index_bits).sum(); + let shift = page_bits + bits_from_higher_lvls; + let width = index_bits(level); + let mask = (1u64 << width) - 1; -fn get_pt_level_to_insert(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; - match page_size_bytes { - SMALL_PAGE_BYTES => sel4_config.num_page_table_levels() - 1, - LARGE_PAGE_BYTES => sel4_config.num_page_table_levels() - 2, - _ => unreachable!( - "internal bug: get_pt_level_to_insert(): unknown page_size_bytes: {page_size_bytes}" - ), + ((vaddr >> shift) & mask) as usize } -} -fn top_pt_level_number(sel4_config: &Config) -> usize { - if sel4_config.arch == Arch::Aarch64 && sel4_config.aarch64_vspace_s2_start_l1() { - 1 - } else { - 0 + fn get_level_coverage(&self, sel4_config: &Config, level: usize, vaddr: u64) -> Range { + let levels = self.address_space_levels(sel4_config) as u64; + + let page_bits = 12; + let bits_from_higher_lvls: u64 = (levels - (level as u64)) * 9; + + let coverage_bits = page_bits + bits_from_higher_lvls; + + let low = (vaddr >> coverage_bits) << coverage_bits; + let high = vaddr | ((1 << coverage_bits) - 1); + + low..high } -} -fn insert_cap_into_page_table_level( - spec_container: &mut CapDLSpecContainer, - cur_level_obj_id: ObjectId, - cur_level: usize, - cur_level_slot: usize, - cap: Cap, -) -> Result<(), String> { - let page_table_level_obj_wrapper = spec_container - .get_root_object_mut(cur_level_obj_id) - .unwrap(); - if let Object::PageTable(page_table_object) = &mut page_table_level_obj_wrapper.object { - // Sanity check that this slot is free - match page_table_object - .slots + #[allow(clippy::too_many_arguments)] + fn map_recursive( + &self, + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + cur_level_obj_id: ObjectId, + cur_level: usize, + frame_cap: Cap, + frame_size_bytes: u64, + addr: u64, + ) -> 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); + + if cur_level == leaf_level { + self.insert_cap_into_level( + spec_container, + sel4_config, + cur_level_obj_id, + cur_level, + slot, + frame_cap, + ) + } else { + let next_obj_id = self.map_intermediary_level_helper( + spec_container, + sel4_config, + cur_level_obj_id, + cur_level, + slot, + addr, + )?; + self.map_recursive( + spec_container, + sel4_config, + next_obj_id, + cur_level + 1, + frame_cap, + frame_size_bytes, + addr, + ) + } + } + + fn map_intermediary_level_helper( + &self, + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + cur_level_obj_id: ObjectId, + cur_level: usize, + cur_level_slot: usize, + addr: u64, + ) -> Result { + 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 let Some(child_obj_id) = slots .iter() .find(|cte| usize::from(cte.slot) == cur_level_slot) + .map(|cte| cte.cap.obj()) { - Some(_) => Err(format!( - "insert_cap_into_page_table_level(): internal bug: slot {} at PT level {} with name '{}' already filled", - cur_level_slot, cur_level, spec_container.get_root_object(cur_level_obj_id).unwrap().name.as_ref().unwrap() - )), - None => { - page_table_object.slots.push(capdl_util_make_cte(cur_level_slot as u32, cap)); - Ok(()) - } + return Ok(child_obj_id); } - } else { - Err(format!( - "insert_cap_into_page_table_level(): internal bug: received a non-Page Table object id {} with name '{}'", - usize::from(cur_level_obj_id), spec_container.get_root_object(cur_level_obj_id).unwrap().name.as_ref().unwrap() - )) + + let next_level = cur_level + 1; + let next_level_coverage = self.get_level_coverage(sel4_config, next_level, addr); + let next_level_obj = CapDLNamedObject { + name: self + .object_name(sel4_config, next_level, next_level_coverage.start) + .into(), + object: self.make_intermediate_object(next_level), + }; + let next_obj_id = spec_container.add_root_object(next_level_obj); + let next_cap = self.make_intermediate_cap(next_obj_id); + + self.insert_cap_into_level( + spec_container, + sel4_config, + cur_level_obj_id, + cur_level, + cur_level_slot, + next_cap, + )?; + + Ok(next_obj_id) } -} -// Just this one time pinky promise -#[allow(clippy::too_many_arguments)] -fn map_intermediary_level_helper( - spec_container: &mut CapDLSpecContainer, - sel4_config: &Config, - pd_name: &str, - next_level_name_prefix: &str, - vspace_obj_id: ObjectId, - cur_level_obj_id: ObjectId, - cur_level: usize, - cur_level_slot: usize, - vaddr: u64, -) -> Result { - let page_table_level_obj_wrapper = spec_container.get_root_object(cur_level_obj_id).unwrap(); - if let Object::PageTable(page_table_object) = &page_table_level_obj_wrapper.object { - match page_table_object - .slots + fn insert_cap_into_level( + &self, + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + cur_level_obj_id: ObjectId, + cur_level: usize, + cur_level_slot: usize, + cap: Cap, + ) -> Result<(), String> { + let object = &mut spec_container + .get_root_object_mut(cur_level_obj_id) + .unwrap() + .object; + + self.valid_level_object(object, sel4_config, cur_level)?; + + let slots = object.slots_mut().unwrap(); + + if slots .iter() - .find(|cte| usize::from(cte.slot) == cur_level_slot) + .any(|cte| usize::from(cte.slot) == cur_level_slot) { - Some(cte_unwrapped) => { - // Next level object already created, nothing to do here - return Ok(cte_unwrapped.cap.obj()); - } - None => { - // We need to create the next level paging structure, get out of this scope for now - // so we don't get a double mutable borrow of spec when we need to insert the next level object - } + 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 { + slots.push(capdl_util_make_cte(cur_level_slot as u32, cap)); + Ok(()) } - } else { - return Err(format!("map_intermediary_level_helper(): internal bug: received a non-Page Table object id {} with name '{}', for mapping at level {}, to pd {}.", - usize::from(cur_level_obj_id), spec_container.get_root_object(cur_level_obj_id).unwrap().name.as_ref().unwrap(), cur_level, pd_name)); } - // Next level object not already created, create it. - let vspace_obj = match &spec_container.get_root_object(vspace_obj_id).unwrap().object { - Object::PageTable(o) => o, - _ => unreachable!( - "map_intermediary_level_helper(): internal bug: received a non VSpace object id {} with name '{}'", - usize::from(vspace_obj_id), spec_container.get_root_object(vspace_obj_id).unwrap().name.as_ref().unwrap() - ), - }; - let next_level_coverage = get_pt_level_coverage(sel4_config, cur_level + 1, vaddr); - let next_level_inner_obj = object::PageTable { - x86_ept: vspace_obj.x86_ept, - is_root: false, // because the VSpace has already been created separately - level: Some(cur_level as u8 + 1), - slots: [].to_vec(), - }; - // We create name with this PT level coverage so that every object names are unique - let next_level_object = CapDLNamedObject { - name: format!( - "{}_{}_vaddr_0x{:x}", - next_level_name_prefix, pd_name, next_level_coverage.start - ) - .into(), - object: Object::PageTable(next_level_inner_obj), - }; - let next_level_obj_id = spec_container.add_root_object(next_level_object); - let next_level_cap = Cap::PageTable(cap::PageTable { - object: next_level_obj_id, - }); + fn make_intermediate_object(&self, level: usize) -> Object { + match self { + &AddressSpace::VSpace { x86_ept, .. } => Object::PageTable(object::PageTable { + x86_ept, + is_root: false, + level: Some(level as u8), + slots: vec![], + }), + } + } - // Then insert into the correct slot at the current level, return and continue mapping - match insert_cap_into_page_table_level( - spec_container, - cur_level_obj_id, - cur_level, - cur_level_slot, - next_level_cap, - ) { - Ok(_) => Ok(next_level_obj_id), - Err(err_reason) => Err(err_reason), + fn make_intermediate_cap(&self, object: ObjectId) -> Cap { + match self { + AddressSpace::VSpace { .. } => Cap::PageTable(cap::PageTable { object }), + } } -} -pub fn create_vspace( - spec_container: &mut CapDLSpecContainer, - sel4_config: &Config, - pd_name: &str, -) -> ObjectId { - spec_container.add_root_object(CapDLNamedObject { - name: format!( - "{}_{}", - get_pt_level_name(sel4_config, top_pt_level_number(sel4_config)), - pd_name + fn object_name(&self, sel4_config: &Config, level: usize, coverage_start: u64) -> String { + format!( + "{}_{}_{}_{:#x}", + self.get_level_name(sel4_config, level), + self.name(), + self.get_addr_label(), + coverage_start ) - .into(), - object: Object::PageTable(object::PageTable { - x86_ept: false, - is_root: true, - level: Some(top_pt_level_number(sel4_config) as u8), - slots: [].to_vec(), - }), - }) + } + + fn valid_level_object( + &self, + object: &Object, + sel4_config: &Config, + cur_level: usize, + ) -> Result<(), String> { + let valid = match self { + AddressSpace::VSpace { .. } => matches!(object, Object::PageTable(_)), + }; + if valid { + Ok(()) + } else { + Err(format!( + "Error: found an invalid object {} at level {} in address-space {}!", + capdl_obj_human_name(object, sel4_config), + cur_level, + self.name() + )) + } + } + + fn address_space_levels(&self, sel4_config: &Config) -> usize { + match self { + AddressSpace::VSpace { .. } => sel4_config.num_page_table_levels(), + } + } + + fn get_root_level(sel4_config: &Config) -> usize { + if sel4_config.arch == Arch::Aarch64 && sel4_config.aarch64_vspace_s2_start_l1() { + 1 + } else { + 0 + } + } } -pub fn create_vspace_ept( +fn create_vspace_address_space( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, - vm_name: &str, -) -> ObjectId { - assert!(sel4_config.arch == Arch::X86_64); + name: &str, + x86_ept: bool, +) -> AddressSpace { + let root_level = AddressSpace::get_root_level(sel4_config); - spec_container.add_root_object(CapDLNamedObject { - name: format!("{}_{}", get_pt_level_name(sel4_config, 0), vm_name).into(), + let root = spec_container.add_root_object(CapDLNamedObject { + name: format!("{}_{}", get_pt_level_name(sel4_config, root_level), name).into(), object: Object::PageTable(object::PageTable { - x86_ept: true, + x86_ept, is_root: true, - level: Some(top_pt_level_number(sel4_config) as u8), - slots: [].to_vec(), + level: Some(root_level as u8), + slots: vec![], }), - }) + }); + + AddressSpace::VSpace { + name: name.to_string(), + root, + x86_ept, + } } -#[allow(clippy::too_many_arguments)] -fn map_recursive( +pub fn create_vspace( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, pd_name: &str, - vspace_obj_id: ObjectId, - pt_obj_id: ObjectId, - cur_level: usize, - frame_cap: Cap, - frame_size_bytes: u64, - vaddr: u64, -) -> Result<(), String> { - if cur_level >= sel4_config.num_page_table_levels() { - unreachable!("internal bug: we should have never recursed further!"); - } - - let this_level_index = get_pt_level_index(sel4_config, cur_level, vaddr); - - if cur_level == get_pt_level_to_insert(sel4_config, frame_size_bytes) { - // Base case: we got to the target level to insert the frame cap. - insert_cap_into_page_table_level( - spec_container, - pt_obj_id, - cur_level, - this_level_index, - frame_cap, - ) - } else { - // Recursive case: we have not gotten to the correct level, create the next level and recurse down. - let next_level_name_prefix = get_pt_level_name(sel4_config, cur_level + 1); - match map_intermediary_level_helper( - spec_container, - sel4_config, - pd_name, - next_level_name_prefix, - vspace_obj_id, - pt_obj_id, - cur_level, - this_level_index, - vaddr, - ) { - Ok(next_level_pt_obj_id) => map_recursive( - spec_container, - sel4_config, - pd_name, - vspace_obj_id, - next_level_pt_obj_id, - cur_level + 1, - frame_cap, - frame_size_bytes, - vaddr, - ), - Err(err_reason) => Err(err_reason), - } - } +) -> AddressSpace { + create_vspace_address_space(spec_container, sel4_config, pd_name, false) } -pub fn map_page( +pub fn create_vspace_ept( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, - pd_name: &str, - vspace_obj_id: ObjectId, - frame_cap: Cap, - frame_size_bytes: u64, - vaddr: u64, -) -> Result<(), String> { - map_recursive( - spec_container, - sel4_config, - pd_name, - vspace_obj_id, - vspace_obj_id, - top_pt_level_number(sel4_config), - frame_cap, - frame_size_bytes, - vaddr, - ) + vm_name: &str, +) -> AddressSpace { + assert!(sel4_config.arch == Arch::X86_64); + create_vspace_address_space(spec_container, sel4_config, vm_name, true) } From 770bf45c150fe5ef1b6eba9f4d96a895bb712df9 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 9 Jul 2026 13:06:29 +1000 Subject: [PATCH 3/8] Memory Refactor: Integrate the improved config This commit integrates the improved config to the memory module. This commit removes some of the duplicated constants definitions that seL4 already exports. Signed-off-by: Callum --- tool/microkit/src/capdl/memory.rs | 59 +++++++++++++++---------------- 1 file changed, 28 insertions(+), 31 deletions(-) diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index d1b1fcd5a..3061af1aa 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -8,7 +8,7 @@ use crate::{ spec::capdl_obj_human_name, util::capdl_util_make_cte, CapDLNamedObject, CapDLSpecContainer, FrameFill, }, - sel4::{Arch, Config, PageSize}, + sel4::{Arch, Config, ObjectType, PageSize}, }; use sel4_capdl_initializer_types::{cap, object, Cap, Object, ObjectId}; use std::ops::Range; @@ -81,7 +81,7 @@ impl AddressSpace { spec_container, sel4_config, self.root(), - Self::get_root_level(sel4_config), + self.get_root_level(sel4_config), frame_cap, frame_size_bytes, addr, @@ -114,40 +114,39 @@ impl AddressSpace { } } + fn get_leaf_bits(&self, sel4_config: &Config) -> u64 { + match self { + Self::VSpace { .. } => ObjectType::SmallPage.fixed_size_bits(sel4_config).unwrap(), + } + } + + fn level_index_bits(&self, sel4_config: &Config, level: usize) -> u64 { + match self { + Self::VSpace { .. } => sel4_config.vspace_level_index_bits(level), + } + } + fn get_level_index(&self, sel4_config: &Config, level: usize, vaddr: u64) -> usize { let levels = self.address_space_levels(sel4_config); - assert!(level < levels); - let index_bits = |level: usize| -> u64 { - if matches!(self, AddressSpace::VSpace { .. }) - && level == Self::get_root_level(sel4_config) - && sel4_config.arch == Arch::Aarch64 - && sel4_config.aarch64_vspace_s2_start_l1() - { - // Special case for first level on AArch64 platforms with hyp and 40 bits PA. - // It have 10 bits index for VSpace. - // match up with seL4_VSpaceBits in seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h - 10 - } else { - 9 - } - }; - - let page_bits = 12; - let bits_from_higher_lvls: u64 = ((level + 1)..levels).map(index_bits).sum(); + let page_bits = self.get_leaf_bits(sel4_config); + let bits_from_higher_lvls: u64 = ((level + 1)..levels) + .map(|level| self.level_index_bits(sel4_config, level)) + .sum(); let shift = page_bits + bits_from_higher_lvls; - let width = index_bits(level); + let width = self.level_index_bits(sel4_config, level); let mask = (1u64 << width) - 1; ((vaddr >> shift) & mask) as usize } fn get_level_coverage(&self, sel4_config: &Config, level: usize, vaddr: u64) -> Range { - let levels = self.address_space_levels(sel4_config) as u64; - - let page_bits = 12; - let bits_from_higher_lvls: u64 = (levels - (level as u64)) * 9; + let levels = self.address_space_levels(sel4_config); + let page_bits = self.get_leaf_bits(sel4_config); + let bits_from_higher_lvls: u64 = ((level + 1)..levels) + .map(|level| self.level_index_bits(sel4_config, level)) + .sum(); let coverage_bits = page_bits + bits_from_higher_lvls; @@ -347,11 +346,9 @@ impl AddressSpace { } } - fn get_root_level(sel4_config: &Config) -> usize { - if sel4_config.arch == Arch::Aarch64 && sel4_config.aarch64_vspace_s2_start_l1() { - 1 - } else { - 0 + fn get_root_level(&self, sel4_config: &Config) -> usize { + match self { + AddressSpace::VSpace { .. } => sel4_config.vspace_root_level(), } } } @@ -362,7 +359,7 @@ fn create_vspace_address_space( name: &str, x86_ept: bool, ) -> AddressSpace { - let root_level = AddressSpace::get_root_level(sel4_config); + let root_level = sel4_config.vspace_root_level(); let root = spec_container.add_root_object(CapDLNamedObject { name: format!("{}_{}", get_pt_level_name(sel4_config, root_level), name).into(), From 5f4f199d8bffcf0ff105081fecced46ecbcd30a8 Mon Sep 17 00:00:00 2001 From: Callum Date: Wed, 15 Jul 2026 15:25:09 +1000 Subject: [PATCH 4/8] IOMMU: Update Cargo rust-sel4 Update microkit to use rust-sel4 with the new x86 IOMMU capdl support. Signed-off-by: Callum --- Cargo.lock | 60 +++++++++++++++++++++++++++--------------------------- Cargo.toml | 4 ++-- 2 files changed, 32 insertions(+), 32 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 744b0db89..04ca34719 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -439,7 +439,7 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "sel4" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "cfg-if", "sel4-config", @@ -449,7 +449,7 @@ dependencies = [ [[package]] name = "sel4-alloca" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "cfg-if", ] @@ -457,7 +457,7 @@ dependencies = [ [[package]] name = "sel4-bitfield-ops" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "rustversion", ] @@ -465,12 +465,12 @@ dependencies = [ [[package]] name = "sel4-build-env" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" [[package]] name = "sel4-capdl-initializer" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "log", "rkyv", @@ -488,7 +488,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "miniz_oxide", "rkyv", @@ -500,7 +500,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types-derive" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "proc-macro2", "quote", @@ -510,7 +510,7 @@ dependencies = [ [[package]] name = "sel4-config" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "prettyplease", "proc-macro2", @@ -524,7 +524,7 @@ dependencies = [ [[package]] name = "sel4-config-data" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "sel4-build-env", "sel4-config-types", @@ -534,7 +534,7 @@ dependencies = [ [[package]] name = "sel4-config-macros" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "fallible-iterator", "proc-macro2", @@ -547,7 +547,7 @@ dependencies = [ [[package]] name = "sel4-config-types" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "serde", ] @@ -555,12 +555,12 @@ dependencies = [ [[package]] name = "sel4-ctors-dtors" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" [[package]] name = "sel4-dlmalloc" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "dlmalloc", "lock_api", @@ -569,17 +569,17 @@ dependencies = [ [[package]] name = "sel4-immediate-sync-once-cell" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" [[package]] name = "sel4-immutable-cell" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" [[package]] name = "sel4-initialize-tls" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "cfg-if", "sel4-alloca", @@ -588,7 +588,7 @@ dependencies = [ [[package]] name = "sel4-logging" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "lock_api", "log", @@ -597,12 +597,12 @@ dependencies = [ [[package]] name = "sel4-no-allocator" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" [[package]] name = "sel4-panicking" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "cfg-if", "sel4-immediate-sync-once-cell", @@ -613,12 +613,12 @@ dependencies = [ [[package]] name = "sel4-panicking-env" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" [[package]] name = "sel4-phdrs" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "sel4-phdrs-constants", ] @@ -626,12 +626,12 @@ dependencies = [ [[package]] name = "sel4-phdrs-constants" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" [[package]] name = "sel4-phdrs-patched" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "sel4-phdrs", "sel4-rodata-static", @@ -640,12 +640,12 @@ dependencies = [ [[package]] name = "sel4-rodata-static" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" [[package]] name = "sel4-root-task" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "sel4", "sel4-dlmalloc", @@ -660,7 +660,7 @@ dependencies = [ [[package]] name = "sel4-root-task-macros" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "proc-macro2", "quote", @@ -670,7 +670,7 @@ dependencies = [ [[package]] name = "sel4-runtime-common" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "cfg-if", "sel4", @@ -686,12 +686,12 @@ dependencies = [ [[package]] name = "sel4-stack" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" [[package]] name = "sel4-sync" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "lock_api", "sel4", @@ -701,7 +701,7 @@ dependencies = [ [[package]] name = "sel4-sys" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/seL4/rust-sel4?rev=21cca71072cda60bd8cc3f1b585818a21e0c6a77#21cca71072cda60bd8cc3f1b585818a21e0c6a77" dependencies = [ "bindgen", "glob", diff --git a/Cargo.toml b/Cargo.toml index b9d265064..6fee4e7c0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -13,11 +13,11 @@ members = [ [workspace.dependencies.sel4-capdl-initializer] git = "https://github.com/seL4/rust-sel4" -rev = "2541371f62dd097f7d47127125c44a0922145fa5" +rev = "21cca71072cda60bd8cc3f1b585818a21e0c6a77" [workspace.dependencies.sel4-capdl-initializer-types] git = "https://github.com/seL4/rust-sel4" -rev = "2541371f62dd097f7d47127125c44a0922145fa5" +rev = "21cca71072cda60bd8cc3f1b585818a21e0c6a77" [profile.release.package.microkit-tool] strip = true From 559c13946aa7ebd56c4f840cb4e582beb8dbdaf1 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 9 Jul 2026 13:06:29 +1000 Subject: [PATCH 5/8] IOMMU: Add IOMMU helper to config This commit adds a helper to extract the io page table index bits from the config. This currently only supports a IOMMU build on x86. Signed-off-by: Callum --- tool/microkit/src/sel4.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index 2868c2871..b2e4439ab 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -425,6 +425,19 @@ impl Config { self.address_space_constants.page_table_index_bits } } + + pub fn io_page_table_index_bits(&self) -> u64 { + match (self.arch, self.iommu) { + (Arch::X86_64, true) => self + .address_space_constants + .io_page_table_index_bits + .expect( + "Error: An x86 VT-D build should have seL4_IOPageTableIndexBits + defined by seL4, captured in tool/microkit/address_space_constants.h", + ), + _ => panic!("Error: currently not supported by Microkit."), + } + } } #[derive(PartialEq, Clone, Copy, Eq)] From f13594e65c83190948933e8d32d1754b03894947 Mon Sep 17 00:00:00 2001 From: Callum Date: Tue, 7 Jul 2026 10:22:32 +1000 Subject: [PATCH 6/8] IOMMU: Add backend support for IOMMU This commit implements support for the x86 IOMMU Capdl spec. The memory module is extended to allow for the construction of IOMMU address spaces. The Capdl spec refers to the IOSpace object as the IODevice object and the IO Page tables as IOPTs. Within microkit we use IOSpace to refer to the whole IO address space. It also provides an example using the qemu dma capable test device, demonstrating the use of the IOMMU. Note we did not need to provide physical memory addresses for any dma buffers, proving the IOMMU correctly translated our requests. Signed-off-by: Callum --- build_sdk.py | 3 +- example/x86_64_iommu_dma_test/Makefile | 72 ++++++ example/x86_64_iommu_dma_test/README.md | 25 ++ .../x86_64_iommu_dma_test.c | 234 ++++++++++++++++++ tool/microkit/src/capdl/builder.rs | 47 +++- tool/microkit/src/capdl/memory.rs | 127 +++++++++- tool/microkit/src/capdl/spec.rs | 5 + tool/microkit/src/sdf.rs | 20 +- tool/microkit/src/sel4.rs | 6 + tool/microkit/src/viper.rs | 2 + tool/microkit/tests/test.rs | 1 + 11 files changed, 517 insertions(+), 25 deletions(-) create mode 100644 example/x86_64_iommu_dma_test/Makefile create mode 100644 example/x86_64_iommu_dma_test/README.md create mode 100644 example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.c diff --git a/build_sdk.py b/build_sdk.py index e9c180f53..3019bd526 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -67,8 +67,7 @@ DEFAULT_KERNEL_OPTIONS_X86_64 = { "KernelPlatform": "pc99", "KernelX86MicroArch": "generic", - # See https://github.com/seL4/microkit/issues/418 for details. - "KernelIOMMU": False, + "KernelIOMMU": True, } | DEFAULT_KERNEL_OPTIONS diff --git a/example/x86_64_iommu_dma_test/Makefile b/example/x86_64_iommu_dma_test/Makefile new file mode 100644 index 000000000..ef104c251 --- /dev/null +++ b/example/x86_64_iommu_dma_test/Makefile @@ -0,0 +1,72 @@ +# +# Copyright 2026, UNSW +# +# SPDX-License-Identifier: BSD-2-Clause +# +ifeq ($(strip $(BUILD_DIR)),) +$(error BUILD_DIR must be specified) +endif + +ifeq ($(strip $(MICROKIT_SDK)),) +$(error MICROKIT_SDK must be specified) +endif + +ifeq ($(strip $(MICROKIT_BOARD)),) +$(error MICROKIT_BOARD must be specified) +endif + +ifeq ($(strip $(MICROKIT_CONFIG)),) +$(error MICROKIT_CONFIG must be specified) +endif + +BOARD_DIR := $(MICROKIT_SDK)/board/$(MICROKIT_BOARD)/$(MICROKIT_CONFIG) + +ARCH := ${shell grep 'CONFIG_SEL4_ARCH ' $(BOARD_DIR)/include/kernel/gen_config.h | cut -d' ' -f4} + +ifeq ($(ARCH),x86_64) + TOOLCHAIN := x86_64-linux-gnu + CFLAGS_ARCH := -march=x86-64 -mtune=generic +else +$(error Unsupported ARCH) +endif + +CC := $(TOOLCHAIN)-gcc +LD := $(TOOLCHAIN)-ld +AS := $(TOOLCHAIN)-as +OBJCOPY := $(TOOLCHAIN)-objcopy +MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit + +IMAGES := x86_64_iommu_dma_test.elf +CFLAGS := -nostdlib -ffreestanding -g3 -O3 -I$(BOARD_DIR)/include $(CFLAGS_ARCH) +LDFLAGS := -L$(BOARD_DIR)/lib -z noexecstack +LIBS := -lmicrokit -Tmicrokit.ld + +INITIAL_TASK = $(BUILD_DIR)/initialiser.elf +KERNEL = $(BUILD_DIR)/sel4.elf +KERNEL_32B = $(BUILD_DIR)/sel4_32.elf +REPORT = $(BUILD_DIR)/report.txt +SPEC = $(BUILD_DIR)/capdl_spec.json + +all: $(KERNEL) $(INITIAL_TASK) +qemu: $(KERNEL_32B) $(INITIAL_TASK) + +$(BUILD_DIR)/x86_64_iommu_dma_test.o: x86_64_iommu_dma_test.c Makefile + $(CC) -c $(CFLAGS) $< -o $@ + +$(BUILD_DIR)/x86_64_iommu_dma_test.elf: $(BUILD_DIR)/x86_64_iommu_dma_test.o + $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ + +$(KERNEL) $(KERNEL_32B) $(INITIAL_TASK): $(addprefix $(BUILD_DIR)/, $(IMAGES)) x86_64_iommu_dma_test.system + $(MICROKIT_TOOL) x86_64_iommu_dma_test.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(INITIAL_TASK) -r $(REPORT) --capdl-json $(SPEC) + +qemu: + qemu-system-x86_64 \ + -machine q35 \ + -cpu qemu64,+fsgsbase,+pdpe1gb,+xsaveopt,+xsave \ + -m "4G" \ + -display none \ + -serial mon:stdio \ + -device intel-iommu,intremap=off,aw-bits=39 \ + -device edu,dma_mask=0xffffffffffffffff,bus=pcie.0,addr=0x04.0 \ + -kernel $(KERNEL_32B) \ + -initrd $(INITIAL_TASK) diff --git a/example/x86_64_iommu_dma_test/README.md b/example/x86_64_iommu_dma_test/README.md new file mode 100644 index 000000000..d22406841 --- /dev/null +++ b/example/x86_64_iommu_dma_test/README.md @@ -0,0 +1,25 @@ + +# x86_64_iommu_dma_test + +This example checks x86 IOMMU mappings with QEMU's EDU PCI device. It maps one +RAM page into the EDU device's IOSpace, asks the device to DMA from that page +into its internal SRAM, then asks the device to DMA the SRAM contents back into +a second offset in the same RAM page and verifies the data. + +The QEMU command in the Makefile pins the EDU device at PCI BDF `00:04.0`, which +must match the `pcidev="0:4.0"` attribute in the system description. + +To build and run: + +```sh +mkdir build +make -C example/x86_64_iommu_dma_test \ + BUILD_DIR=build \ + MICROKIT_SDK=/path/to/microkit-sdk \ + MICROKIT_BOARD=x86_64_generic \ + MICROKIT_CONFIG=debug \ + qemu +``` diff --git a/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.c b/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.c new file mode 100644 index 000000000..fff25ad74 --- /dev/null +++ b/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.c @@ -0,0 +1,234 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include +#include + +#include + +#define PCI_CONFIG_ADDRESS 0xcf8u +#define PCI_CONFIG_DATA 0xcfcu +#define PCI_ENABLE 0x80000000u +#define PCI_COMMAND 0x04u +#define PCI_BAR0 0x10u +#define PCI_COMMAND_MEMORY 0x0002u +#define PCI_COMMAND_MASTER 0x0004u + +#define EDU_BUS 0u +#define EDU_DEV 4u +#define EDU_FUNC 0u +#define EDU_DEVICE_ID 0xedu +#define EDU_PCI_VENDOR_ID 0x1234u +#define EDU_PCI_DEVICE_ID 0x11e8u + +#define EDU_MMIO_PADDR 0xfe000000ull +#define EDU_MMIO_SIZE 0x00100000ull +#define EDU_BAR_SIZE 0x00100000ull +#define EDU_DMA_SRAM 0x40000ull +#define DMA_BUFFER_IOVA 0x00100000ull +#define DMA_TEST_BYTES 64u +#define DMA_RETURN_OFFSET 0x100u +#define DMA_TIMEOUT 10000000u + +#define EDU_REG_ID 0x00u +#define EDU_REG_ALIVE 0x04u +#define EDU_REG_DMA_SRC 0x80u +#define EDU_REG_DMA_DST 0x88u +#define EDU_REG_DMA_COUNT 0x90u +#define EDU_REG_DMA_CMD 0x98u + +#define EDU_DMA_START 0x1u +#define EDU_DMA_TO_RAM 0x2u + +uint64_t edu_mmio_window_vaddr; +uint64_t dma_buffer_vaddr; +uint64_t pci_config_ioport_id; + +static void put_hex64(uint64_t value) +{ + char buf[19] = "0x0000000000000000"; + for (size_t i = 0; i < 16; i++) { + unsigned int nibble = (value >> ((15 - i) * 4)) & 0xf; + buf[2 + i] = nibble < 10 ? '0' + nibble : 'a' + (nibble - 10); + } + microkit_dbg_puts(buf); +} + +static uint32_t pci_config_read32(uint8_t bus, uint8_t dev, uint8_t func, uint8_t offset) +{ + uint32_t address = + PCI_ENABLE | ((uint32_t)bus << 16) | ((uint32_t)dev << 11) | ((uint32_t)func << 8) | (offset & 0xfcu); + + microkit_x86_ioport_write_32(pci_config_ioport_id, PCI_CONFIG_ADDRESS, address); + return microkit_x86_ioport_read_32(pci_config_ioport_id, PCI_CONFIG_DATA); +} + +static uint16_t pci_config_read16(uint8_t bus, uint8_t dev, uint8_t func, uint8_t offset) +{ + uint32_t value = pci_config_read32(bus, dev, func, offset); + return (value >> ((offset & 2u) * 8)) & 0xffffu; +} + +static void pci_config_write16(uint8_t bus, uint8_t dev, uint8_t func, uint8_t offset, uint16_t value) +{ + uint32_t address = + PCI_ENABLE | ((uint32_t)bus << 16) | ((uint32_t)dev << 11) | ((uint32_t)func << 8) | (offset & 0xfcu); + + microkit_x86_ioport_write_32(pci_config_ioport_id, PCI_CONFIG_ADDRESS, address); + microkit_x86_ioport_write_16(pci_config_ioport_id, PCI_CONFIG_DATA + (offset & 2u), value); +} + +static void pci_config_write32(uint8_t bus, uint8_t dev, uint8_t func, uint8_t offset, uint32_t value) +{ + uint32_t address = + PCI_ENABLE | ((uint32_t)bus << 16) | ((uint32_t)dev << 11) | ((uint32_t)func << 8) | (offset & 0xfcu); + + microkit_x86_ioport_write_32(pci_config_ioport_id, PCI_CONFIG_ADDRESS, address); + microkit_x86_ioport_write_32(pci_config_ioport_id, PCI_CONFIG_DATA, value); +} + +static volatile uint32_t *edu_reg32(uintptr_t edu_base, uint32_t offset) +{ + return (volatile uint32_t *)(edu_base + offset); +} + +static volatile uint64_t *edu_reg64(uintptr_t edu_base, uint32_t offset) +{ + return (volatile uint64_t *)(edu_base + offset); +} + +static uint32_t edu_read32(uintptr_t edu_base, uint32_t offset) +{ + return *edu_reg32(edu_base, offset); +} + +static void edu_write32(uintptr_t edu_base, uint32_t offset, uint32_t value) +{ + *edu_reg32(edu_base, offset) = value; +} + +static void edu_write64(uintptr_t edu_base, uint32_t offset, uint64_t value) +{ + *edu_reg64(edu_base, offset) = value; +} + +static void wait_for_dma(uintptr_t edu_base) +{ + while ((edu_read32(edu_base, EDU_REG_DMA_CMD) & EDU_DMA_START)) + ; +} + +static void fill_dma_buffer(void) +{ + volatile uint32_t *buf = (volatile uint32_t *)(uintptr_t)dma_buffer_vaddr; + + for (size_t i = 0; i < DMA_TEST_BYTES / sizeof(uint32_t); i++) { + buf[i] = 0x5a000000u | (uint32_t)i; + buf[(DMA_RETURN_OFFSET / sizeof(uint32_t)) + i] = 0; + } +} + +static bool check_dma_return_buffer(void) +{ + volatile uint32_t *buf = (volatile uint32_t *)(uintptr_t)dma_buffer_vaddr; + + for (size_t i = 0; i < DMA_TEST_BYTES / sizeof(uint32_t); i++) { + uint32_t expected = 0x5a000000u | (uint32_t)i; + uint32_t actual = buf[(DMA_RETURN_OFFSET / sizeof(uint32_t)) + i]; + if (actual != expected) { + microkit_dbg_puts("DMA return buffer mismatch at word "); + put_hex64(i); + microkit_dbg_puts(": expected "); + put_hex64(expected); + microkit_dbg_puts(", got "); + put_hex64(actual); + microkit_dbg_puts("\n"); + return false; + } + } + return true; +} + +static bool check_edu_liveness(uintptr_t edu_base) +{ + const uint32_t probe = 0xa5a55a5au; + + edu_write32(edu_base, EDU_REG_ALIVE, probe); + return edu_read32(edu_base, EDU_REG_ALIVE) == ~probe; +} + +void init(void) +{ + microkit_dbg_puts("x86_64_iommu_dma_test: starting\n"); + + uint32_t id = pci_config_read32(EDU_BUS, EDU_DEV, EDU_FUNC, 0x00); + if ((id & 0xFFFFu) != EDU_PCI_VENDOR_ID || ((id >> 16) & 0xFFFFu) != EDU_PCI_DEVICE_ID) { + microkit_dbg_puts("x86_64_iommu_dma_test: EDU PCI device not found, id="); + put_hex64(id); + microkit_dbg_puts("\n"); + return; + } + + pci_config_write32(EDU_BUS, EDU_DEV, EDU_FUNC, PCI_BAR0, EDU_MMIO_PADDR); + + uint64_t bar0 = pci_config_read32(EDU_BUS, EDU_DEV, EDU_FUNC, PCI_BAR0) & ~0xfu; + if (bar0 < EDU_MMIO_PADDR || bar0 + EDU_BAR_SIZE > EDU_MMIO_PADDR + EDU_MMIO_SIZE) { + microkit_dbg_puts("x86_64_iommu_dma_test: EDU BAR outside mapped MMIO window, bar="); + put_hex64(bar0); + microkit_dbg_puts("\n"); + return; + } + + uint16_t command = pci_config_read16(EDU_BUS, EDU_DEV, EDU_FUNC, PCI_COMMAND); + command |= PCI_COMMAND_MEMORY | PCI_COMMAND_MASTER; + pci_config_write16(EDU_BUS, EDU_DEV, EDU_FUNC, PCI_COMMAND, command); + + uintptr_t edu_base = (uintptr_t)edu_mmio_window_vaddr + (uintptr_t)(bar0 - EDU_MMIO_PADDR); + microkit_dbg_puts("x86_64_iommu_dma_test: EDU BAR="); + put_hex64(bar0); + microkit_dbg_puts(", id_reg="); + uint32_t device_id = edu_read32(edu_base, EDU_REG_ID); + put_hex64(device_id); + if ((device_id & 0xFF) != EDU_DEVICE_ID) { + microkit_dbg_puts("x86_64_iommu_dma_test: Identification failed.\n"); + return; + } + microkit_dbg_puts("\n"); + + if (!check_edu_liveness(edu_base)) { + microkit_dbg_puts("x86_64_iommu_dma_test: EDU MMIO liveness check failed\n"); + return; + } + + /* The qemu education device works by copying from DRAM to an internal device buffer or vice-versa. */ + fill_dma_buffer(); + + edu_write64(edu_base, EDU_REG_DMA_SRC, DMA_BUFFER_IOVA); + edu_write64(edu_base, EDU_REG_DMA_DST, EDU_DMA_SRAM); + edu_write64(edu_base, EDU_REG_DMA_COUNT, DMA_TEST_BYTES); + edu_write32(edu_base, EDU_REG_DMA_CMD, EDU_DMA_START); + + wait_for_dma(edu_base); + + edu_write64(edu_base, EDU_REG_DMA_SRC, EDU_DMA_SRAM); + edu_write64(edu_base, EDU_REG_DMA_DST, DMA_BUFFER_IOVA + DMA_RETURN_OFFSET); + edu_write64(edu_base, EDU_REG_DMA_COUNT, DMA_TEST_BYTES); + edu_write32(edu_base, EDU_REG_DMA_CMD, EDU_DMA_START | EDU_DMA_TO_RAM); + + wait_for_dma(edu_base); + + if (!check_dma_return_buffer()) { + microkit_dbg_puts("x86_64_iommu_dma_test: DMA verification failed\n"); + return; + } + + microkit_dbg_puts("x86_64_iommu_dma_test: DMA verification passed\n"); +} + +void notified(microkit_channel ch) +{ + (void)ch; +} diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 96cd71171..9b928f767 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -18,14 +18,14 @@ use sel4_capdl_initializer_types::{ use crate::{ capdl::{ irq::create_irq_handler_cap, - memory::{create_vspace, create_vspace_ept, AddressSpace}, + memory::{create_iospace, create_vspace, create_vspace_ept, AddressSpace}, spec::{capdl_obj_physical_size_bits, BytesContent, ElfContent, FillContent}, util::*, }, elf::ElfFile, sdf::{ - CapMapType, CpuCore, Map, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME, - MONITOR_PRIORITY, + CapMapType, CpuCore, IommuDeviceIdentifier, Map, SystemDescription, BUDGET_DEFAULT, + MONITOR_PD_NAME, MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, util::{ranges_overlap, round_down, round_up}, @@ -1239,7 +1239,46 @@ pub fn build_capdl_spec( } // ********************************* - // Step 6. Sort the root objects + // Step 6. Create IOMMU Address Spaces + // ********************************* + let mut iospace_by_device: HashMap = HashMap::new(); + for iomap in system.iomaps.iter() { + let address_space = iospace_by_device + .entry(iomap.identifier) + .or_insert_with(|| { + create_iospace( + &mut spec_container, + kernel_config, + &iomap.device, + iomap.identifier, + iomap.domain_id, + ) + }); + let page_size_bytes = mr_name_to_frames + .get(&iomap.mr) + .ok_or(format!( + "Error: Memory region {} referenced by iomap not found.", + iomap.mr + ))? + .first() + .map(|&object_id| 1 << capdl_util_get_frame_size_bits(&spec_container, object_id)) + .ok_or(format!( + "Error: Memory region {} referenced by iomap has no frames.", + &iomap.mr + ))?; + + map_memory_region( + &mut spec_container, + kernel_config, + iomap, + page_size_bytes, + address_space, + &mr_name_to_frames[&iomap.mr], + )?; + } + + // ********************************* + // Step 7. Sort the root objects // ********************************* // The CapDL initialiser expects objects with paddr to come first, then sorted by size so that the // allocation algorithm at run-time can run more efficiently. diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index 3061af1aa..0294b3047 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -8,9 +8,12 @@ use crate::{ spec::capdl_obj_human_name, util::capdl_util_make_cte, CapDLNamedObject, CapDLSpecContainer, FrameFill, }, + sdf::IommuDeviceIdentifier, sel4::{Arch, Config, ObjectType, PageSize}, }; -use sel4_capdl_initializer_types::{cap, object, Cap, Object, ObjectId}; +use sel4_capdl_initializer_types::{ + cap, object, x86_io_address_space, Cap, Object, ObjectId, Word, +}; use std::ops::Range; /// For naming and debugging purposes only, no functional purpose. @@ -48,6 +51,14 @@ fn get_pt_level_name(sel4_config: &Config, level: usize) -> &str { } } +fn get_iopt_level_name(level: usize) -> String { + if level == 0 { + "iospace".to_string() + } else { + format!("iopt_level_{}", level - 1) + } +} + #[derive(Debug, Clone, PartialEq, Eq)] pub enum AddressSpace { VSpace { @@ -55,17 +66,22 @@ pub enum AddressSpace { root: ObjectId, x86_ept: bool, }, + IOSpace { + name: String, + root: ObjectId, + device: IommuDeviceIdentifier, + }, } impl AddressSpace { pub fn root(&self) -> ObjectId { match self { - &Self::VSpace { root, .. } => root, + &Self::VSpace { root, .. } | &Self::IOSpace { root, .. } => root, } } pub fn name(&self) -> &str { match self { - Self::VSpace { name, .. } => name, + Self::VSpace { name, .. } | Self::IOSpace { name, .. } => name, } } @@ -105,32 +121,42 @@ impl AddressSpace { fn get_level_name(&self, sel4_config: &Config, level: usize) -> String { match self { Self::VSpace { .. } => get_pt_level_name(sel4_config, level).to_string(), + Self::IOSpace { .. } => get_iopt_level_name(level), } } fn get_addr_label(&self) -> &'static str { match self { Self::VSpace { .. } => "vaddr", + Self::IOSpace { .. } => "ioaddr", } } - fn get_leaf_bits(&self, sel4_config: &Config) -> u64 { - match self { - Self::VSpace { .. } => ObjectType::SmallPage.fixed_size_bits(sel4_config).unwrap(), - } + fn get_leaf_bits(sel4_config: &Config) -> u64 { + ObjectType::SmallPage.fixed_size_bits(sel4_config).unwrap() } fn level_index_bits(&self, sel4_config: &Config, level: usize) -> u64 { match self { Self::VSpace { .. } => sel4_config.vspace_level_index_bits(level), + Self::IOSpace { .. } => { + if level > 0 { + sel4_config.io_page_table_index_bits() + } else { + panic!("IODevice root is not indexed by address bits"); + } + } } } fn get_level_index(&self, sel4_config: &Config, level: usize, vaddr: u64) -> usize { + if matches!(self, AddressSpace::IOSpace { .. }) && level == 0 { + return x86_io_address_space::IOSPACE_ROOT_IOPT_SLOT; + } let levels = self.address_space_levels(sel4_config); assert!(level < levels); - let page_bits = self.get_leaf_bits(sel4_config); + let page_bits = Self::get_leaf_bits(sel4_config); let bits_from_higher_lvls: u64 = ((level + 1)..levels) .map(|level| self.level_index_bits(sel4_config, level)) .sum(); @@ -143,7 +169,7 @@ impl AddressSpace { fn get_level_coverage(&self, sel4_config: &Config, level: usize, vaddr: u64) -> Range { let levels = self.address_space_levels(sel4_config); - let page_bits = self.get_leaf_bits(sel4_config); + let page_bits = Self::get_leaf_bits(sel4_config); let bits_from_higher_lvls: u64 = ((level + 1)..levels) .map(|level| self.level_index_bits(sel4_config, level)) .sum(); @@ -300,12 +326,22 @@ impl AddressSpace { level: Some(level as u8), slots: vec![], }), + AddressSpace::IOSpace { .. } => { + let iopt_level = level + .checked_sub(1) + .expect("Error: cannot create an intermediate IOPT for the root level."); + Object::IOPT(object::IOPT { + slots: vec![], + level: Word(iopt_level as u64), + }) + } } } fn make_intermediate_cap(&self, object: ObjectId) -> Cap { match self { AddressSpace::VSpace { .. } => Cap::PageTable(cap::PageTable { object }), + AddressSpace::IOSpace { .. } => Cap::IOPT(cap::IOPT { object }), } } @@ -327,6 +363,13 @@ impl AddressSpace { ) -> Result<(), String> { let valid = match self { AddressSpace::VSpace { .. } => matches!(object, Object::PageTable(_)), + AddressSpace::IOSpace { .. } => { + if cur_level == 0 { + matches!(object, Object::IODevice(_)) + } else { + matches!(object, Object::IOPT(_)) + } + } }; if valid { Ok(()) @@ -343,16 +386,82 @@ impl AddressSpace { fn address_space_levels(&self, sel4_config: &Config) -> usize { match self { AddressSpace::VSpace { .. } => sel4_config.num_page_table_levels(), + // IOSpace level 0 is the IODevice root. Slot 0 points to the + // normal IOPT tree root, and slots 1.. hold spare IOPTs for + // runtime prefix levels. + AddressSpace::IOSpace { .. } => x86_io_address_space::CAPDL_NUM_IOPT_LEVELS + 1, } } fn get_root_level(&self, sel4_config: &Config) -> usize { match self { AddressSpace::VSpace { .. } => sel4_config.vspace_root_level(), + AddressSpace::IOSpace { .. } => 0, } } } +// In future supporting SMMU can be done by matching on the IommuDeviceIdentifier or creating a new function. +pub fn create_iospace( + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + device_name: &str, + device_identifier: IommuDeviceIdentifier, + domain_id: Option, +) -> AddressSpace { + let IommuDeviceIdentifier::X86Pci(pci_device) = device_identifier; + + let root = spec_container.add_root_object(CapDLNamedObject { + name: format!("{}_{}", get_iopt_level_name(0), device_name).into(), + object: Object::IODevice(object::IODevice { + slots: vec![], + domain_id: domain_id.unwrap().into(), + pci_device: ( + Word(pci_device.bus.into()), + Word(pci_device.device.into()), + Word(pci_device.function.into()), + ), + }), + }); + + let address_space = AddressSpace::IOSpace { + name: device_name.to_string(), + root, + device: device_identifier, + }; + + // The IODevice root has two roles: slot 0 is reserved for the root of the + // normal 3-level IOPT tree, while slots 1.. hold spare IOPTs that the + // initialiser can use when seL4 reports a wider IOVA space at runtime. + for spare_idx in 0..x86_io_address_space::SPARE_NUM_LEVELS { + let slot = x86_io_address_space::IOSPACE_ROOT_IOPT_SLOT + 1 + spare_idx; + let next_obj_id = spec_container.add_root_object(CapDLNamedObject { + name: format!( + "{}_{}_spare_{}", + get_iopt_level_name(1), + address_space.name(), + slot + ) + .into(), + object: address_space.make_intermediate_object(1), + }); + let next_cap = address_space.make_intermediate_cap(next_obj_id); + + address_space + .insert_cap_into_level( + spec_container, + sel4_config, + address_space.root(), + address_space.get_root_level(sel4_config), + slot, + next_cap, + ) + .unwrap_or_else(|err| panic!("Error: create_iospace() failed allocating spare IOPT capabilities with error {err}")); + } + + address_space +} + fn create_vspace_address_space( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, diff --git a/tool/microkit/src/capdl/spec.rs b/tool/microkit/src/capdl/spec.rs index 980f4fef8..93a9b6704 100644 --- a/tool/microkit/src/capdl/spec.rs +++ b/tool/microkit/src/capdl/spec.rs @@ -51,6 +51,9 @@ pub fn capdl_obj_physical_size_bits(obj: &Object, sel4_config: &Confi } } Object::AsidPool(_) => ObjectType::AsidPool.fixed_size_bits(sel4_config).unwrap(), + Object::IOPT(_) => ObjectType::IOPageTable + .fixed_size_bits(sel4_config) + .unwrap(), Object::SchedContext(sched_context) => sched_context.size_bits as u64, Object::Reply => ObjectType::Reply.fixed_size_bits(sel4_config).unwrap(), _ => 0, @@ -75,6 +78,8 @@ pub fn capdl_obj_human_name(obj: &Object, sel4_config: &Config) -> &' } Object::PageTable(_) => "PageTable", Object::AsidPool(_) => "AsidPool", + Object::IODevice(_) => "x86 IODevice", + Object::IOPT(_) => "x86 IOPT", Object::ArmIrq(_) => "ARM IRQ", Object::IrqMsi(_) => "x86 MSI IRQ", Object::IrqIOApic(_) => "x86 IOAPIC IRQ", diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 242d081c8..db448bf87 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -22,7 +22,7 @@ use crate::sel4::{ use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool}; use crate::MAX_PDS; -use sel4_capdl_initializer_types::FillEntryContentBootInfoId; +use sel4_capdl_initializer_types::{x86_io_address_space, FillEntryContentBootInfoId}; use std::collections::{HashMap, HashSet}; use std::fmt; use std::fs; @@ -62,12 +62,6 @@ const PD_MAX_STACK_SIZE: u64 = 1024 * 1024 * 16; /// `src/arch/x86/object/interrupt.c` const X86_IRQ_VECTOR_MAX: i64 = 107; -// In reality the kernel dynamically determines this value. The tool assumes -// at least 512GiB of IO virtual address space. This handles all values reported -// to us by the kernel at runtime except for the 1GiB or no-iommu cases. -// This is currently applied to any iommu mapping independent of the architecture. -const IOMAP_MAX_VADDR: u64 = (1 << 39) - 1; - /// The purpose of this function is to parse an integer that could /// either be in decimal or hex format, unlike the normal parsing /// functionality that the Rust standard library provides. @@ -746,13 +740,13 @@ impl SysIOMap { let mr = checked_lookup(xml_sdf, node, "mr")?.to_string(); let iovaddr = sdf_parse_number(checked_lookup(xml_sdf, node, "iovaddr")?, node)?; - if iovaddr > IOMAP_MAX_VADDR { + if iovaddr > x86_io_address_space::CAPDL_MAX_IOVA { return Err(value_error( xml_sdf, node, format!( "iovaddr ({iovaddr:#x}) must be less than {:#x}", - IOMAP_MAX_VADDR + 1 + x86_io_address_space::CAPDL_MAX_IOVA + 1 ), )); } @@ -2212,7 +2206,13 @@ fn check_io_maps( for (identifier, maps) in by_device { let address_space = identifier.to_string(); - check_maps(xml_sdf, mrs, maps, &address_space, IOMAP_MAX_VADDR + 1)?; + check_maps( + xml_sdf, + mrs, + maps, + &address_space, + x86_io_address_space::CAPDL_MAX_IOVA + 1, + )?; } Ok(()) diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index b2e4439ab..83d66bac5 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -285,6 +285,7 @@ pub struct ObjectSizes { pub reply: u64, pub vspace: u64, pub page_table: u64, + pub io_page_table: Option, pub huge_page: u64, pub large_page: u64, pub small_page: u64, @@ -489,6 +490,7 @@ pub enum ObjectType { PageTable, Vcpu, AsidPool, + IOPageTable, } impl ObjectType { @@ -503,6 +505,10 @@ impl ObjectType { ObjectType::Reply => Some(object_sizes.reply), ObjectType::VSpace => Some(object_sizes.vspace), ObjectType::PageTable => Some(object_sizes.page_table), + ObjectType::IOPageTable => match (config.arch, config.iommu) { + (Arch::X86_64, true) => Some(object_sizes.io_page_table.unwrap()), + _ => panic!("Unexpected architecture or build asking for io_page_table_bits"), + }, ObjectType::HugePage => Some(object_sizes.huge_page), ObjectType::LargePage => Some(object_sizes.large_page), ObjectType::SmallPage => Some(object_sizes.small_page), diff --git a/tool/microkit/src/viper.rs b/tool/microkit/src/viper.rs index 3d459e1cd..0446c4f32 100644 --- a/tool/microkit/src/viper.rs +++ b/tool/microkit/src/viper.rs @@ -143,6 +143,8 @@ pub fn get_cap_view( | Cap::DomainSet(_) | Cap::Frame(_) | Cap::SchedContext(_) + | Cap::IOSpace(_) + | Cap::IOPT(_) | Cap::Untyped(_) => { /* ^ The caps above can occupy CSpace slots, but Viper * verification currently has no use for them, so we diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index c9f776bc7..0933da61a 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -21,6 +21,7 @@ const DEFAULT_OBJECT_SIZES: sel4::ObjectSizes = sel4::ObjectSizes { huge_page: 0, large_page: 0, small_page: 0, + io_page_table: None, asid_pool: 0, vcpu: None, }; From e63bdef4d3a38b63271df6c1e3ca578ca53375e5 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 9 Jul 2026 19:11:40 +1000 Subject: [PATCH 7/8] IOMMU: Add large page guard While seL4 does not support large pages to be used by the IOMMU, we will raise an error at the SDF parsing stage. Signed-off-by: Callum --- tool/microkit/src/sdf.rs | 11 ++++++++++- tool/microkit/tests/test.rs | 6 +++++- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index db448bf87..beb0fa4e6 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -2204,6 +2204,15 @@ fn check_io_maps( by_device.entry(iomap.identifier).or_default().push(iomap); } + if iomaps.iter().any(|iomap| { + mrs.iter() + .any(|mr| mr.page_size == PageSize::Large && mr.name == iomap.mr_name()) + }) { + return Err( + "Error: currently seL4 does not have large page support for the IOMMU".to_string(), + ); + } + for (identifier, maps) in by_device { let address_space = identifier.to_string(); check_maps( @@ -2828,7 +2837,7 @@ pub fn parse( // Optimise page size of MRs, if the page size is not specified for mr in &mut mrs { - if mr.page_size_specified_by_user { + if mr.page_size_specified_by_user || iomaps.iter().any(|iomap| iomap.mr_name() == mr.name) { continue; } diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 0933da61a..30f509452 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -909,12 +909,16 @@ mod iommu { ) } + // Currently this test fails with "Error: currently seL4 does not have large page support for the IOMMU" + // When seL4 supports large pages for the iommu it should fail with: + // Error: map for 'small_region' has io address range [0x1000..0x2000) which overlaps with map for + //'large_region' [0x0..0x200000) in PCI device 00:03.0 @ " #[test] fn test_overlap_mixed_page_sizes() { check_error( &DEFAULT_X86_64_KERNEL_CONFIG, "iommu_overlap_mixed_page_sizes.system", - "Error: map for 'small_region' has io address range [0x1000..0x2000) which overlaps with map for 'large_region' [0x0..0x200000) in PCI device 00:03.0 @", + "Error: currently seL4 does not have large page support for the IOMMU", ) } From ba6cf23194d475010b994fa040a82b7022cd7aa2 Mon Sep 17 00:00:00 2001 From: Callum Date: Tue, 14 Jul 2026 22:48:34 +1000 Subject: [PATCH 8/8] IOMMU: Integrate rust-sel4 capdl initialiser Integrate the new IOMMU support from the rust-sel4 capdl initialiser. Integrate the rust-sel4 PCI structure to avoid repeating definitions to improve code maintainability. The traits that we implement on the wrapper struct, make it easy to use the wrapper without having to worry about accessing the underyling type. Signed-off-by: Callum --- .../x86_64_iommu_dma_test.system | 2 +- tool/microkit/src/capdl/irq.rs | 6 +- tool/microkit/src/capdl/memory.rs | 30 +++--- tool/microkit/src/capdl/spec.rs | 6 +- tool/microkit/src/sdf.rs | 98 ++++++++++++------- tool/microkit/src/viper.rs | 2 +- 6 files changed, 86 insertions(+), 58 deletions(-) diff --git a/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.system b/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.system index eb35dd81d..d21c91906 100644 --- a/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.system +++ b/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.system @@ -7,7 +7,7 @@ - + diff --git a/tool/microkit/src/capdl/irq.rs b/tool/microkit/src/capdl/irq.rs index 99f32ad61..e826decb5 100644 --- a/tool/microkit/src/capdl/irq.rs +++ b/tool/microkit/src/capdl/irq.rs @@ -91,9 +91,9 @@ fn create_irq_obj( slots: [].to_vec(), extra: Box::new(object::IrqMsiExtraInfo { handle: Word(handle), - pci_bus: Word(pci_device.bus as u64), - pci_dev: Word(pci_device.device as u64), - pci_func: Word(pci_device.function as u64), + pci_bus: Word(pci_device.bus.into()), + pci_dev: Word(pci_device.device.into()), + pci_func: Word(pci_device.function.into()), }), }), }; diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index 0294b3047..1d089c80a 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -143,7 +143,7 @@ impl AddressSpace { if level > 0 { sel4_config.io_page_table_index_bits() } else { - panic!("IODevice root is not indexed by address bits"); + panic!("IOSpace root is not indexed by address bits"); } } } @@ -329,8 +329,8 @@ impl AddressSpace { AddressSpace::IOSpace { .. } => { let iopt_level = level .checked_sub(1) - .expect("Error: cannot create an intermediate IOPT for the root level."); - Object::IOPT(object::IOPT { + .expect("Error: cannot create an intermediate IOPageTable for the root level."); + Object::IOPageTable(object::IOPageTable { slots: vec![], level: Word(iopt_level as u64), }) @@ -341,7 +341,7 @@ impl AddressSpace { fn make_intermediate_cap(&self, object: ObjectId) -> Cap { match self { AddressSpace::VSpace { .. } => Cap::PageTable(cap::PageTable { object }), - AddressSpace::IOSpace { .. } => Cap::IOPT(cap::IOPT { object }), + AddressSpace::IOSpace { .. } => Cap::IOPageTable(cap::IOPageTable { object }), } } @@ -365,9 +365,9 @@ impl AddressSpace { AddressSpace::VSpace { .. } => matches!(object, Object::PageTable(_)), AddressSpace::IOSpace { .. } => { if cur_level == 0 { - matches!(object, Object::IODevice(_)) + matches!(object, Object::IOSpace(_)) } else { - matches!(object, Object::IOPT(_)) + matches!(object, Object::IOPageTable(_)) } } }; @@ -386,8 +386,8 @@ impl AddressSpace { fn address_space_levels(&self, sel4_config: &Config) -> usize { match self { AddressSpace::VSpace { .. } => sel4_config.num_page_table_levels(), - // IOSpace level 0 is the IODevice root. Slot 0 points to the - // normal IOPT tree root, and slots 1.. hold spare IOPTs for + // IOSpace level 0 is the IOSpace root. Slot 0 points to the + // normal IOPageTable tree root, and slots 1.. hold spare IOPTs for // runtime prefix levels. AddressSpace::IOSpace { .. } => x86_io_address_space::CAPDL_NUM_IOPT_LEVELS + 1, } @@ -413,14 +413,10 @@ pub fn create_iospace( let root = spec_container.add_root_object(CapDLNamedObject { name: format!("{}_{}", get_iopt_level_name(0), device_name).into(), - object: Object::IODevice(object::IODevice { + object: Object::IOSpace(object::IOSpace { slots: vec![], domain_id: domain_id.unwrap().into(), - pci_device: ( - Word(pci_device.bus.into()), - Word(pci_device.device.into()), - Word(pci_device.function.into()), - ), + pci_device: pci_device.into(), }), }); @@ -430,8 +426,8 @@ pub fn create_iospace( device: device_identifier, }; - // The IODevice root has two roles: slot 0 is reserved for the root of the - // normal 3-level IOPT tree, while slots 1.. hold spare IOPTs that the + // The IOSpace root has two roles: slot 0 is reserved for the root of the + // normal 3-level IOPageTable tree, while slots 1.. hold spare IOPageTable that the // initialiser can use when seL4 reports a wider IOVA space at runtime. for spare_idx in 0..x86_io_address_space::SPARE_NUM_LEVELS { let slot = x86_io_address_space::IOSPACE_ROOT_IOPT_SLOT + 1 + spare_idx; @@ -456,7 +452,7 @@ pub fn create_iospace( slot, next_cap, ) - .unwrap_or_else(|err| panic!("Error: create_iospace() failed allocating spare IOPT capabilities with error {err}")); + .unwrap_or_else(|err| panic!("Error: create_iospace() failed allocating spare IOPageTable capabilities with error {err}")); } address_space diff --git a/tool/microkit/src/capdl/spec.rs b/tool/microkit/src/capdl/spec.rs index 93a9b6704..eb1a086dd 100644 --- a/tool/microkit/src/capdl/spec.rs +++ b/tool/microkit/src/capdl/spec.rs @@ -51,7 +51,7 @@ pub fn capdl_obj_physical_size_bits(obj: &Object, sel4_config: &Confi } } Object::AsidPool(_) => ObjectType::AsidPool.fixed_size_bits(sel4_config).unwrap(), - Object::IOPT(_) => ObjectType::IOPageTable + Object::IOPageTable(_) => ObjectType::IOPageTable .fixed_size_bits(sel4_config) .unwrap(), Object::SchedContext(sched_context) => sched_context.size_bits as u64, @@ -78,8 +78,8 @@ pub fn capdl_obj_human_name(obj: &Object, sel4_config: &Config) -> &' } Object::PageTable(_) => "PageTable", Object::AsidPool(_) => "AsidPool", - Object::IODevice(_) => "x86 IODevice", - Object::IOPT(_) => "x86 IOPT", + Object::IOSpace(_) => "x86 IOSpace", + Object::IOPageTable(_) => "x86 IOPageTable", Object::ArmIrq(_) => "ARM IRQ", Object::IrqMsi(_) => "x86 MSI IRQ", Object::IrqIOApic(_) => "x86 IOAPIC IRQ", diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index beb0fa4e6..191b0da54 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -22,10 +22,12 @@ use crate::sel4::{ use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool}; use crate::MAX_PDS; -use sel4_capdl_initializer_types::{x86_io_address_space, FillEntryContentBootInfoId}; +use sel4_capdl_initializer_types::{object, x86_io_address_space, FillEntryContentBootInfoId}; use std::collections::{HashMap, HashSet}; use std::fmt; use std::fs; +use std::hash::{Hash, Hasher}; +use std::ops::Deref; use std::path::{Path, PathBuf}; use std::str::FromStr; @@ -91,18 +93,35 @@ fn loc_string(xml_sdf: &XmlSystemDescription, pos: roxmltree::TextPos) -> String format!("{}:{}:{}", xml_sdf.filename.display(), pos.row, pos.col) } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] -pub struct PciDevice { - pub bus: u8, - pub device: u8, - pub function: u8, +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct PciDevice(pub object::PCIDevice); + +impl Hash for PciDevice { + fn hash(&self, state: &mut H) { + self.0.bus.hash(state); + self.0.device.hash(state); + self.0.function.hash(state); + } +} + +impl Deref for PciDevice { + type Target = object::PCIDevice; + + fn deref(&self) -> &Self::Target { + &self.0 + } } -impl PciDevice { - /// Maximum values for PCI bus, device, function numbers. Inclusive. - const PCI_BUS_MAX: i64 = (1 << 8) - 1; - const PCI_DEV_MAX: i64 = (1 << 5) - 1; - const PCI_FUNC_MAX: i64 = (1 << 3) - 1; +impl From for object::PCIDevice { + fn from(device: PciDevice) -> Self { + device.0 + } +} + +impl From for PciDevice { + fn from(device: object::PCIDevice) -> Self { + PciDevice(device) + } } #[derive(Debug, Clone, Copy, PartialEq, Eq)] @@ -136,20 +155,24 @@ impl fmt::Display for PciDeviceParseError { PciDeviceParseError::DeviceParse => write!(f, "failed to parse PCI device"), PciDeviceParseError::FunctionParse => write!(f, "failed to parse PCI function"), PciDeviceParseError::BusOutOfRange => { - write!(f, "PCI bus must be within [0..{}]", PciDevice::PCI_BUS_MAX) + write!( + f, + "PCI bus must be within [0..{}]", + object::PCIDevice::PCI_BUS_MAX + ) } PciDeviceParseError::DeviceOutOfRange => { write!( f, "PCI device must be within [0..{}]", - PciDevice::PCI_DEV_MAX + object::PCIDevice::PCI_DEV_MAX ) } PciDeviceParseError::FunctionOutOfRange => { write!( f, "PCI function must be within [0..{}]", - PciDevice::PCI_FUNC_MAX + object::PCIDevice::PCI_FUNC_MAX ) } } @@ -166,28 +189,37 @@ impl FromStr for PciDevice { .split_once('.') .ok_or(PciDeviceParseError::Malformed)?; - let bus = - i64::from_str_radix(bus_str.trim(), 16).map_err(|_| PciDeviceParseError::BusParse)?; + let bus = i64::from_str_radix(bus_str.trim(), 16) + .map_err(|_| PciDeviceParseError::BusParse) + .and_then(|bus| { + match (0..=i64::from(object::PCIDevice::PCI_BUS_MAX)).contains(&bus) { + true => Ok(bus as u8), + false => Err(PciDeviceParseError::BusOutOfRange), + } + })?; let device = i64::from_str_radix(device_str.trim(), 16) - .map_err(|_| PciDeviceParseError::DeviceParse)?; + .map_err(|_| PciDeviceParseError::DeviceParse) + .and_then(|device| { + match (0..=i64::from(object::PCIDevice::PCI_DEV_MAX)).contains(&device) { + true => Ok(device as u8), + false => Err(PciDeviceParseError::DeviceOutOfRange), + } + })?; let function = i64::from_str_radix(function_str.trim(), 16) - .map_err(|_| PciDeviceParseError::FunctionParse)?; - - if !(0..=PciDevice::PCI_BUS_MAX).contains(&bus) { - return Err(PciDeviceParseError::BusOutOfRange); - } - if !(0..=PciDevice::PCI_DEV_MAX).contains(&device) { - return Err(PciDeviceParseError::DeviceOutOfRange); - } - if !(0..=PciDevice::PCI_FUNC_MAX).contains(&function) { - return Err(PciDeviceParseError::FunctionOutOfRange); - } + .map_err(|_| PciDeviceParseError::FunctionParse) + .and_then(|function| { + match (0..=i64::from(object::PCIDevice::PCI_FUNC_MAX)).contains(&function) { + true => Ok(function as u8), + false => Err(PciDeviceParseError::FunctionOutOfRange), + } + })?; - Ok(PciDevice { - bus: bus as u8, - device: device as u8, - function: function as u8, - }) + let result = object::PCIDevice { + bus, + device, + function, + }; + Ok(result.into()) } } diff --git a/tool/microkit/src/viper.rs b/tool/microkit/src/viper.rs index 0446c4f32..7a034aa23 100644 --- a/tool/microkit/src/viper.rs +++ b/tool/microkit/src/viper.rs @@ -144,7 +144,7 @@ pub fn get_cap_view( | Cap::Frame(_) | Cap::SchedContext(_) | Cap::IOSpace(_) - | Cap::IOPT(_) + | Cap::IOPageTable(_) | Cap::Untyped(_) => { /* ^ The caps above can occupy CSpace slots, but Viper * verification currently has no use for them, so we