From 0e3dc58c8a422c9149f68713a4a3767299dee75b Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Wed, 25 Feb 2026 16:40:06 +1100 Subject: [PATCH 01/13] Incomplete support for VTD in microkit tool. Signed-off-by: Cheng Li --- tool/microkit/src/capdl/builder.rs | 80 +++++- tool/microkit/src/capdl/iomem.rs | 240 ++++++++++++++++++ tool/microkit/src/capdl/memory.rs | 6 +- tool/microkit/src/capdl/mod.rs | 1 + tool/microkit/src/capdl/spec.rs | 2 + tool/microkit/src/sdf.rs | 106 ++++++++ tool/microkit/src/sel4.rs | 8 + .../tests/sdf/iommu_out_of_bound.system | 15 ++ tool/microkit/tests/test.rs | 9 + 9 files changed, 452 insertions(+), 15 deletions(-) create mode 100644 tool/microkit/src/capdl/iomem.rs create mode 100644 tool/microkit/tests/sdf/iommu_out_of_bound.system diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 44754e8e6..70ebb114d 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -17,6 +17,7 @@ use sel4_capdl_initializer_types::{ use crate::{ capdl::{ + iomem::create_iospace, irq::create_irq_handler_cap, memory::{create_vspace, create_vspace_ept, map_page}, spec::{capdl_obj_physical_size_bits, BytesContent, ElfContent, FillContent}, @@ -381,6 +382,38 @@ fn map_memory_region( } } +/// Map frames to the IOSpace +fn map_io_memory_region( + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + pd_name: &str, + map: &SysMap, + target_iospace: ObjectId, + 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; + // 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); + // // Map it into this PD address space. + // map_page( + // spec_container, + // sel4_config, + // pd_name, + // target_vspace, + // frame_cap, + // page_sz, + // cur_vaddr, + // ) + // .unwrap(); + // cur_vaddr += page_sz; + // } +} + /// Build a CapDL Spec according to the System Description File. pub fn build_capdl_spec( kernel_config: &Config, @@ -673,7 +706,30 @@ pub fn build_capdl_spec( cur_stack_vaddr += PageSize::Small as u64; } - // Step 3-4 Create Scheduling Context + // Step 3-4 Create and Map IO Page Table Structure + for iomap in &pd.iomaps { + let iospace_id = create_iospace( + &mut spec_container, + kernel_config, + &pd.name, + iomap.pci_bus, + iomap.pci_dev, + iomap.dev_func, + pd.id.unwrap(), + ); + + // map_io_memory_region( + // &mut spec_container, + // kernel_config, + // &pd.name, + // map, + // page_size_bytes, + // pd_vspace_obj_id, + // frames, + // ); + } + + // Step 3-5 Create Scheduling Context let pd_sc_obj_id = capdl_util_make_sc_obj( &mut spec_container, &pd.name, @@ -688,7 +744,7 @@ pub fn build_capdl_spec( pd_sc_cap, )); - // Step 3-5 Create fault Endpoint cap to parent/monitor + // Step 3-6 Create fault Endpoint cap to parent/monitor let pd_fault_ep_cap = if let Some(pd_parent) = pd.parent { assert!(pd_global_idx > pd_parent); let badge: u64 = FAULT_BADGE | pd.id.unwrap(); @@ -720,7 +776,7 @@ pub fn build_capdl_spec( pd_fault_ep_cap.clone(), )); - // Step 3-6 Create cap to Monitor's endpoint for passive PDs. + // Step 3-7 Create cap to Monitor's endpoint for passive PDs. if pd.passive { let pd_monitor_ep_cap = capdl_util_make_endpoint_cap( mon_fault_ep_obj_id, @@ -735,7 +791,7 @@ pub fn build_capdl_spec( )); } - // Step 3-7 Create endpoint object for the PD if it has children or can receive PPCs, else it will be a notification + // Step 3-8 Create endpoint object for the PD if it has children or can receive PPCs, else it will be a notification let pd_ntfn_obj_id = capdl_util_make_ntfn_obj(&mut spec_container, &pd.name); let pd_ntfn_cap = capdl_util_make_ntfn_cap(pd_ntfn_obj_id, true, true, 0); let mut pd_ep_obj_id: Option = None; @@ -763,13 +819,13 @@ pub fn build_capdl_spec( pd_ntfn_cap, )); - // Step 3-8 Create Reply obj + cap and insert into CSpace + // Step 3-9 Create Reply obj + cap and insert into CSpace let pd_reply_obj_id = capdl_util_make_reply_obj(&mut spec_container, &pd.name); let pd_reply_cap = capdl_util_make_reply_cap(pd_reply_obj_id); caps_to_insert_to_pd_cspace .push(capdl_util_make_cte(PD_REPLY_CAP_IDX as u32, pd_reply_cap)); - // Step 3-9 Create spec and caps to IRQs + // Step 3-10 Create spec and caps to IRQs for irq in pd.irqs.iter() { // Create a IRQ handler cap and insert into the requested CSpace's slot. let irq_handle_cap = create_irq_handler_cap( @@ -785,7 +841,7 @@ pub fn build_capdl_spec( .push(capdl_util_make_cte(irq_cap_idx as u32, irq_handle_cap)); } - // Step 3-10 Create I/O port objects on x86 platform. + // Step 3-11 Create I/O port objects on x86 platform. for ioport in pd.ioports.iter() { let ioport_obj_id = capdl_util_make_ioport_obj(&mut spec_container, &pd.name, ioport.addr, ioport.size); @@ -796,7 +852,7 @@ pub fn build_capdl_spec( )); } - // Step 3-11 Create VM Spec. + // Step 3-12 Create VM Spec. if let Some(virtual_machine) = &pd.virtual_machine { // A VM really is just a collection of special threads, it has its own TCBs, Scheduling Contexts, etc... // The difference is that it have a vCPU for each TCB to store the virtual CPUs' states. @@ -974,7 +1030,7 @@ pub fn build_capdl_spec( } } - // Step 3-12 Create ARM SMC cap if requested. + // Step 3-13 Create ARM SMC cap if requested. if pd.smc { caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( PD_ARM_SMC_CAP_IDX as u32, @@ -982,7 +1038,7 @@ pub fn build_capdl_spec( )); } - // Step 3-13 Create CSpace and add all caps that the PD code and libmicrokit need to access. + // Step 3-14 Create CSpace and add all caps that the PD code and libmicrokit need to access. let pd_cnode_obj_id = capdl_util_make_cnode_obj( &mut spec_container, &pd.name, @@ -997,7 +1053,7 @@ pub fn build_capdl_spec( )); pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id); - // Step 3-14 Set the TCB parameters and all the various caps that we need to bind to this TCB. + // Step 3-15 Set the TCB parameters and all the various caps that we need to bind to this TCB. if let Object::Tcb(pd_tcb) = &mut spec_container .get_root_object_mut(pd_tcb_obj_id) .unwrap() @@ -1016,7 +1072,7 @@ pub fn build_capdl_spec( unreachable!("internal bug: build_capdl_spec() got a non TCB object ID when trying to set TCB parameters for the monitor."); } - // Step 3-15 bind this PD's TCB to the monitor, this accomplish two purposes: + // Step 3-16 bind this PD's TCB to the monitor, this accomplish two purposes: // 1. Allow PDs' TCBs to be named to their proper name in SDF in debug config. // 2. Allow passive PDs. capdl_util_insert_cap_into_cspace( diff --git a/tool/microkit/src/capdl/iomem.rs b/tool/microkit/src/capdl/iomem.rs new file mode 100644 index 000000000..d8766e800 --- /dev/null +++ b/tool/microkit/src/capdl/iomem.rs @@ -0,0 +1,240 @@ +use sel4_capdl_initializer_types::{cap, object, Cap, Object, ObjectId}; + +use crate::{ + capdl::{ + memory::{get_pt_level_coverage, get_pt_level_index, get_pt_level_to_insert}, + util::capdl_util_make_cte, + CapDLNamedObject, CapDLSpecContainer, + }, + sel4::{Config, PageSize}, +}; + +const VTD_PML4_LEVEL: u8 = 0; +const VTD_ENTRY_LEVEL: u8 = 4; + +pub fn create_iospace( + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + pd_name: &str, + pci_bus: u8, + pci_device: u8, + dev_func: u8, + pd_id: u64, +) -> ObjectId { + let id = spec_container.add_root_object(CapDLNamedObject { + name: format!( + "{}_{}", + get_iopt_level_name(sel4_config, VTD_PML4_LEVEL as usize), + pd_name, + ) + .into(), + object: Object::IOPageTable(object::IOPageTable { + is_root: true, + level: Some(VTD_PML4_LEVEL), + slots: [].to_vec(), + }), + }); + + spec_container.add_root_object(CapDLNamedObject { + name: format!("IOSpace_{}", pd_name,).into(), + object: Object::IOSpace(object::IOSpace { + pci_bus, + pci_device, + dev_func, + pd_id, + root_pt_id: id, + }), + }); + + id +} + +fn get_iopt_level_name(sel4_config: &Config, level: usize) -> &str { + match sel4_config.arch { + crate::sel4::Arch::X86_64 => match level { + 0 => "VTD_pml4", + 1 => "VTD_pdpt", + 2 => "VTD_pd", + 3 => "VTD_pt", + _ => unreachable!(), + }, + _ => unreachable!("get_iopt_level_name(): Internal bug: Only x86 support iommu!"), + } +} + +// 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, + 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::IOPageTable(page_table_object) = &page_table_level_obj_wrapper.object { + match page_table_object + .slots + .iter() + .find(|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 + } + } + } 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)); + } + + // get_pt_level_coverage works the same for io memory as well + let next_level_coverage = get_pt_level_coverage(sel4_config, cur_level + 1, vaddr); + let next_level_inner_obj = object::IOPageTable { + is_root: false, // IOSpace is always created seperately + 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!( + "{}_{}_ioaddr_0x{:x}", + next_level_name_prefix, pd_name, next_level_coverage.start + ) + .into(), + object: Object::IOPageTable(next_level_inner_obj), + }; + let next_level_obj_id = spec_container.add_root_object(next_level_object); + let next_level_cap = Cap::IOPageTable(cap::IOPageTable { + object: next_level_obj_id, + }); + + // Then insert into the correct slot at the current level, return and continue mapping + match insert_cap_into_io_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 insert_cap_into_io_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::IOPageTable(page_table_object) = &mut page_table_level_obj_wrapper.object { + // Sanity check that this slot is free + match page_table_object + .slots + .iter() + .find(|cte| usize::from(cte.slot) == cur_level_slot) + { + Some(_) => Err(format!( + "insert_cap_into_io_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(()) + } + } + } else { + Err(format!( + "insert_cap_into_io_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() + )) + } +} + +#[allow(clippy::too_many_arguments)] +fn map_recursive( + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + pd_name: &str, + pt_obj_id: ObjectId, + cur_level: usize, + frame_cap: Cap, + ioaddr: u64, +) -> Result<(), String> { + assert!( + VTD_ENTRY_LEVEL as usize == sel4_config.num_page_table_levels(), + "internal bug: The maximum page table level does not match!" + ); + + 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, ioaddr); + + if cur_level == get_pt_level_to_insert(sel4_config, PageSize::Small as u64) { + // Base case: we got to the target level to insert the frame cap. + insert_cap_into_io_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_iopt_level_name(sel4_config, cur_level + 1); + match map_intermediary_level_helper( + spec_container, + sel4_config, + pd_name, + next_level_name_prefix, + pt_obj_id, + cur_level, + this_level_index, + ioaddr, + ) { + Ok(next_level_pt_obj_id) => map_recursive( + spec_container, + sel4_config, + pd_name, + next_level_pt_obj_id, + cur_level + 1, + frame_cap, + ioaddr, + ), + Err(err_reason) => Err(err_reason), + } + } +} + +pub fn map_io_page( + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + pd_name: &str, + iospace_obj_id: ObjectId, + frame_cap: Cap, + ioaddr: u64, +) -> Result<(), String> { + map_recursive( + spec_container, + sel4_config, + pd_name, + iospace_obj_id, + VTD_PML4_LEVEL as usize, + frame_cap, + ioaddr, + ) +} diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index d8b0c7bd1..6985dcb0f 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -45,7 +45,7 @@ fn get_pt_level_name(sel4_config: &Config, level: usize) -> &str { } } -fn get_pt_level_index(sel4_config: &Config, level: usize, vaddr: u64) -> usize { +pub(crate) fn get_pt_level_index(sel4_config: &Config, level: usize, vaddr: u64) -> usize { let levels = sel4_config.num_page_table_levels(); assert!(level < levels); @@ -73,7 +73,7 @@ fn get_pt_level_index(sel4_config: &Config, level: usize, vaddr: u64) -> usize { ((vaddr >> shift) & mask) as usize } -fn get_pt_level_coverage(sel4_config: &Config, level: usize, vaddr: u64) -> Range { +pub(crate) 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; @@ -86,7 +86,7 @@ fn get_pt_level_coverage(sel4_config: &Config, level: usize, vaddr: u64) -> Rang low..high } -fn get_pt_level_to_insert(sel4_config: &Config, page_size_bytes: u64) -> usize { +pub(crate) 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 { diff --git a/tool/microkit/src/capdl/mod.rs b/tool/microkit/src/capdl/mod.rs index 88a8d7339..2df7192d9 100644 --- a/tool/microkit/src/capdl/mod.rs +++ b/tool/microkit/src/capdl/mod.rs @@ -7,6 +7,7 @@ pub mod allocation; pub mod builder; pub mod initialiser; +mod iomem; mod irq; mod memory; pub mod packaging; diff --git a/tool/microkit/src/capdl/spec.rs b/tool/microkit/src/capdl/spec.rs index 2486c837a..046b91fe4 100644 --- a/tool/microkit/src/capdl/spec.rs +++ b/tool/microkit/src/capdl/spec.rs @@ -74,6 +74,8 @@ pub fn capdl_obj_human_name(obj: &Object, sel4_config: &Config) -> &' } } Object::PageTable(_) => "PageTable", + Object::IOPageTable(_) => "IOPageTable", + Object::IOSpace(_) => "IOSpace", Object::AsidPool(_) => "AsidPool", Object::ArmIrq(_) => "ARM IRQ", Object::IrqMsi(_) => "x86 MSI IRQ", diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index ceb582886..132f2719b 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -156,6 +156,15 @@ impl SysMemoryRegion { } } +#[derive(Debug, PartialEq, Eq, Clone)] +pub struct IOMemMap { + pub name: String, + pub pci_bus: u8, + pub pci_dev: u8, + pub dev_func: u8, + pub ioaddr: u64, +} + #[derive(Debug, PartialEq, Eq)] pub enum SysIrqKind { Conventional { @@ -264,6 +273,7 @@ pub struct ProtectionDomain { pub maps: Vec, pub irqs: Vec, pub ioports: Vec, + pub iomaps: Vec, pub setvars: Vec, pub virtual_machine: Option, /// Only used when parsing child PDs. All elements will be removed @@ -416,6 +426,95 @@ impl SysMap { } } +impl IOMemMap { + fn from_xml( + config: &Config, + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + ) -> Result { + const PCI_DEV_MAX: u8 = 0x1F; + const DEV_FUNC_MAX: u8 = 0b111; + if config.arch != Arch::X86_64 { + return Err(value_error( + xml_sdf, + &node, + "IOMMU isn't supported on ARM and RISC-V".to_string(), + )); + } + + check_attributes(xml_sdf, &node, &["mr", "pcidev", "addr"])?; + + let mr = checked_lookup(xml_sdf, node, "mr")?.to_string(); + let pcidev_str = checked_lookup(xml_sdf, node, "pcidev")?.to_string(); + let ioaddr = sdf_parse_number(checked_lookup(xml_sdf, node, "addr")?, node)?; + + let max_ioaddr = config.iommu_top(); + + if ioaddr >= max_ioaddr { + return Err(value_error( + xml_sdf, + node, + format!("ioaddr (0x{ioaddr:x}) must be less than 0x{max_ioaddr:x}"), + )); + } + + let pci_parts: Vec = pcidev_str + .split([':', '.']) + .map(str::trim) + .map(|x| { + i64::from_str_radix(x, 16) + .expect("Error: Failed to parse parts of the PCI device address") + }) + .collect(); + + if pci_parts.len() != 3 { + return Err(format!( + "Error: failed to parse PCI address '{}' on element '{}'", + pcidev_str, + node.tag_name().name() + )); + } + + let pci_bus: u8 = pci_parts[0] as u8; + + if pci_parts[0] != pci_bus as i64 { + return Err(value_error( + xml_sdf, + &node, + "Invalid value for PCI bus".to_string(), + )); + } + + let pci_dev: u8 = pci_parts[1] as u8; + + if pci_parts[1] != pci_dev as i64 || pci_dev > PCI_DEV_MAX { + return Err(value_error( + xml_sdf, + &node, + "Invalid value for PCI Device".to_string(), + )); + } + + let dev_func: u8 = pci_parts[2] as u8; + + if pci_parts[2] != dev_func as i64 || dev_func > DEV_FUNC_MAX { + return Err(value_error( + xml_sdf, + &node, + "Invalid value for PCI Device Function".to_string(), + )); + } + + Ok(IOMemMap { + name: mr, + pci_bus: u8::try_from(pci_parts[0]).unwrap(), + pci_dev: u8::try_from(pci_parts[1]).unwrap(), + dev_func: u8::try_from(pci_parts[2]).unwrap(), + ioaddr, + }) + } +} + impl ProtectionDomain { pub fn needs_ep(&self, self_id: usize, channels: &[Channel]) -> bool { self.has_children @@ -591,6 +690,7 @@ impl ProtectionDomain { let mut maps = Vec::new(); let mut irqs = Vec::new(); let mut ioports = Vec::new(); + let mut iomaps = Vec::new(); let mut setvars: Vec = Vec::new(); let mut child_pds = Vec::new(); @@ -993,6 +1093,11 @@ impl ProtectionDomain { )); } } + "iomap" => { + let iomap = IOMemMap::from_xml(config, xml_sdf, &child)?; + + iomaps.push(iomap); + } "setvar" => { check_attributes(xml_sdf, &child, &["symbol", "region_paddr"])?; let symbol = checked_lookup(xml_sdf, &child, "symbol")?.to_string(); @@ -1084,6 +1189,7 @@ impl ProtectionDomain { maps, irqs, ioports, + iomaps, setvars, child_pds, virtual_machine, diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index cca595fd0..17ee864d1 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -325,6 +325,14 @@ impl Config { } } + pub fn iommu_top(&self) -> u64 { + match self.arch { + Arch::Aarch64 => unreachable!("Internal bug: Aarch64 doesn't support IOMMU"), + Arch::Riscv64 => unreachable!("Internal bug: Risv64 doesn't support IOMMU"), + Arch::X86_64 => 1 << (12 + 9 + 9 + 9), + } + } + pub fn virtual_base(&self) -> u64 { match self.arch { Arch::Aarch64 => match self.hypervisor { diff --git a/tool/microkit/tests/sdf/iommu_out_of_bound.system b/tool/microkit/tests/sdf/iommu_out_of_bound.system new file mode 100644 index 000000000..1d65146aa --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_out_of_bound.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index d2becea69..62137bf5c 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -623,6 +623,15 @@ mod protection_domain { "Error: cpu core must be less than 1, got 10 on element 'protection_domain':", ) } + + #[test] + fn test_iommu_valid_on_x86() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_out_of_bound.system", + "Error: ioaddr (0x8000000000) must be less than 0x8000000000 on element 'iomap':", + ) + } } #[cfg(test)] From 48b37e0375e97c554bca47afc02a386acc31e568 Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Wed, 25 Feb 2026 16:53:25 +1100 Subject: [PATCH 02/13] Finish the first iteration of the implementation. Signed-off-by: Cheng Li --- tool/microkit/src/capdl/builder.rs | 62 ++++++++++++++---------------- 1 file changed, 29 insertions(+), 33 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 70ebb114d..f56bbccaf 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -17,7 +17,7 @@ use sel4_capdl_initializer_types::{ use crate::{ capdl::{ - iomem::create_iospace, + iomem::{create_iospace, map_io_page}, irq::create_irq_handler_cap, memory::{create_vspace, create_vspace_ept, map_page}, spec::{capdl_obj_physical_size_bits, BytesContent, ElfContent, FillContent}, @@ -25,7 +25,7 @@ use crate::{ }, elf::ElfFile, sdf::{ - CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME, + CpuCore, IOMemMap, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME, MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, @@ -387,31 +387,26 @@ fn map_io_memory_region( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, pd_name: &str, - map: &SysMap, + map: &IOMemMap, target_iospace: ObjectId, 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; - // 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); - // // Map it into this PD address space. - // map_page( - // spec_container, - // sel4_config, - // pd_name, - // target_vspace, - // frame_cap, - // page_sz, - // cur_vaddr, - // ) - // .unwrap(); - // cur_vaddr += page_sz; - // } + let mut cur_vaddr = map.ioaddr; + for frame_obj_id in frames.iter() { + // Make a cap for this frame. The perms should not matter in IOMMU + let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, true, true, false, false); + // Map it into this PD IOSpace. + map_io_page( + spec_container, + sel4_config, + pd_name, + target_iospace, + frame_cap, + cur_vaddr, + ) + .unwrap(); + cur_vaddr += PageSize::Small as u64; + } } /// Build a CapDL Spec according to the System Description File. @@ -718,15 +713,16 @@ pub fn build_capdl_spec( pd.id.unwrap(), ); - // map_io_memory_region( - // &mut spec_container, - // kernel_config, - // &pd.name, - // map, - // page_size_bytes, - // pd_vspace_obj_id, - // frames, - // ); + let frames = mr_name_to_frames.get(&iomap.name).unwrap(); + + map_io_memory_region( + &mut spec_container, + kernel_config, + &pd.name, + iomap, + iospace_id, + frames, + ); } // Step 3-5 Create Scheduling Context From 726cb26db9d75023097b318da0d045546379d470 Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Thu, 26 Feb 2026 15:59:36 +1100 Subject: [PATCH 03/13] Tool can output correct specs in tried (limited) tests. Signed-off-by: Cheng Li --- tool/microkit/src/capdl/builder.rs | 55 ++++++++++++++++++------------ tool/microkit/src/capdl/iomem.rs | 7 ++-- tool/microkit/src/capdl/spec.rs | 3 ++ tool/microkit/src/sdf.rs | 1 + tool/microkit/src/sel4.rs | 3 ++ 5 files changed, 46 insertions(+), 23 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index f56bbccaf..e72c4ecd9 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -11,8 +11,8 @@ use std::{ }; use sel4_capdl_initializer_types::{ - object, CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId, Spec, - Word, + object::{self}, + CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId, Spec, Word, }; use crate::{ @@ -702,27 +702,40 @@ pub fn build_capdl_spec( } // Step 3-4 Create and Map IO Page Table Structure - for iomap in &pd.iomaps { - let iospace_id = create_iospace( - &mut spec_container, - kernel_config, - &pd.name, - iomap.pci_bus, - iomap.pci_dev, - iomap.dev_func, - pd.id.unwrap(), - ); + { + let mut pci_to_iospace: HashMap<(u8, u8, u8), ObjectId> = HashMap::new(); + for iomap in &pd.iomaps { + let iospace_id = + match pci_to_iospace.get(&(iomap.pci_bus, iomap.pci_dev, iomap.dev_func)) { + Some(iospace_id) => iospace_id.clone(), + None => { + let iospace_id = create_iospace( + &mut spec_container, + kernel_config, + &pd.name, + iomap.pci_bus, + iomap.pci_dev, + iomap.dev_func, + pd_global_idx, + ); + + pci_to_iospace + .insert((iomap.pci_bus, iomap.pci_dev, iomap.dev_func), iospace_id); + iospace_id + } + }; - let frames = mr_name_to_frames.get(&iomap.name).unwrap(); + let frames = mr_name_to_frames.get(&iomap.name).unwrap(); - map_io_memory_region( - &mut spec_container, - kernel_config, - &pd.name, - iomap, - iospace_id, - frames, - ); + map_io_memory_region( + &mut spec_container, + kernel_config, + &pd.name, + iomap, + iospace_id, + frames, + ); + } } // Step 3-5 Create Scheduling Context diff --git a/tool/microkit/src/capdl/iomem.rs b/tool/microkit/src/capdl/iomem.rs index d8766e800..b059b8612 100644 --- a/tool/microkit/src/capdl/iomem.rs +++ b/tool/microkit/src/capdl/iomem.rs @@ -19,7 +19,7 @@ pub fn create_iospace( pci_bus: u8, pci_device: u8, dev_func: u8, - pd_id: u64, + pd_id: usize, ) -> ObjectId { let id = spec_container.add_root_object(CapDLNamedObject { name: format!( @@ -42,7 +42,10 @@ pub fn create_iospace( pci_device, dev_func, pd_id, - root_pt_id: id, + slots: vec![capdl_util_make_cte( + 0, + Cap::IOPageTable(cap::IOPageTable { object: id }), + )], }), }); diff --git a/tool/microkit/src/capdl/spec.rs b/tool/microkit/src/capdl/spec.rs index 046b91fe4..03335541e 100644 --- a/tool/microkit/src/capdl/spec.rs +++ b/tool/microkit/src/capdl/spec.rs @@ -53,6 +53,9 @@ pub fn capdl_obj_physical_size_bits(obj: &Object, sel4_config: &Confi Object::AsidPool(_) => ObjectType::AsidPool.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(), + Object::IOPageTable(_) => ObjectType::IOPageTable + .fixed_size_bits(sel4_config) + .unwrap(), _ => 0, } } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 132f2719b..249c3e3dd 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -426,6 +426,7 @@ impl SysMap { } } +// Things to check, make sure that there are no overlapping mappings per PCI device impl IOMemMap { fn from_xml( config: &Config, diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index 17ee864d1..fe2154661 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -450,6 +450,7 @@ pub enum ObjectType { SmallPage, LargePage, PageTable, + IOPageTable, Vcpu, AsidPool, } @@ -475,6 +476,8 @@ impl ObjectType { _ => panic!("Unexpected architecture asking for vCPU size bits"), }, ObjectType::AsidPool => Some(object_sizes.asid_pool), + ObjectType::IOPageTable => Some(12), + // It would be best to avoid such catch all case so people might forget to add the size of new object type here. _ => None, } } From 704a36153cccd53d0cbb2d684d4cc027e462c2ca Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Thu, 5 Mar 2026 14:38:29 +1100 Subject: [PATCH 04/13] iommu works for blk exampl on x86 qemu. Signed-off-by: Cheng Li --- Cargo.toml | 6 +- example/iommu/blk/blk.system | 84 ++++++++++++++++++++++++++ example/iommu/build.sh | 14 +++++ tool/microkit/src/capdl/initialiser.rs | 2 +- tool/microkit/src/capdl/iomem.rs | 5 +- 5 files changed, 105 insertions(+), 6 deletions(-) create mode 100644 example/iommu/blk/blk.system create mode 100644 example/iommu/build.sh diff --git a/Cargo.toml b/Cargo.toml index f9e7a481f..f23c88b8c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,12 +12,10 @@ members = [ ] [workspace.dependencies.sel4-capdl-initializer] -git = "https://github.com/seL4/rust-sel4" -rev = "cf43f5d0a97854e9916cc999fdd97ff3b5fbea7b" +path = "/home/cheng/system/rust-sel4/crates/sel4-capdl-initializer" [workspace.dependencies.sel4-capdl-initializer-types] -git = "https://github.com/seL4/rust-sel4" -rev = "cf43f5d0a97854e9916cc999fdd97ff3b5fbea7b" +path = "/home/cheng/system/rust-sel4/crates/sel4-capdl-initializer/types" [profile.release.package.microkit-tool] strip = true diff --git a/example/iommu/blk/blk.system b/example/iommu/blk/blk.system new file mode 100644 index 000000000..a1adc00e7 --- /dev/null +++ b/example/iommu/blk/blk.system @@ -0,0 +1,84 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/example/iommu/build.sh b/example/iommu/build.sh new file mode 100644 index 000000000..ebde05574 --- /dev/null +++ b/example/iommu/build.sh @@ -0,0 +1,14 @@ +source ~/system/myvenv/bin/activate +BOARDS=x86_64_generic +python build_sdk.py --skip-docs --skip-tar --configs=debug --boards=$BOARDS --sel4=/home/cheng/work/seL4 +cd ./example/hello +make MICROKIT_SDK=/home/cheng/work/microkit/release/microkit-sdk-2.1.0-dev MICROKIT_CONFIG=debug BUILD_DIR=build MICROKIT_BOARD=x86_64_generic + +qemu-system-x86_64 -machine q35 -kernel /home/cheng/work/microkit/release/microkit-sdk-2.1.0-dev/board/x86_64_generic/debug/elf/sel4_32.elf -m size=2G -serial mon:stdio -cpu qemu64,+fsgsbase,+pdpe1gb,+pcid,+invpcid,+xsave,+xsaves,+xsaveopt -initrd loader.img -device intel-iommu,intremap=on,caching-mode=on -device virtio-blk-pci,drive=hd,addr=0x3.0,iommu_platform=on,disable-legacy=on \ +-nographic \ +-d guest_errors \ +-drive file=disk,if=none,format=raw,id=hd + +/home/cheng/work/microkit/release/microkit-sdk-2.1.0-dev/bin/microkit blk.system --search-path /home/cheng/work/sddf/examples/blk/build --board x86_64_generic --config debug -o loader.img -r report.txt + +qemu-system-x86_64 -machine q35 -kernel /home/cheng/work/microkit/release/microkit-sdk-2.1.0-dev/board/x86_64_generic/debug/elf/sel4_32.elf -m size=2G -serial mon:stdio -cpu qemu64,+fsgsbase,+pdpe1gb,+pcid,+invpcid,+xsave,+xsaves,+xsaveopt -initrd loader.img -device intel-iommu,intremap=on,caching-mode=on -device virtio-blk-pci,drive=hd,addr=0x3.0,iommu_platform=on,disable-legacy=on -nographic -d guest_errors -drive file=disk,if=none,format=raw,id=hd \ No newline at end of file diff --git a/tool/microkit/src/capdl/initialiser.rs b/tool/microkit/src/capdl/initialiser.rs index 250203b55..4be001d52 100644 --- a/tool/microkit/src/capdl/initialiser.rs +++ b/tool/microkit/src/capdl/initialiser.rs @@ -44,7 +44,7 @@ impl CapDLInitialiser { elf, phys_base: None, spec_metadata: None, - log_level: LogLevel::Info, + log_level: LogLevel::Debug, } } diff --git a/tool/microkit/src/capdl/iomem.rs b/tool/microkit/src/capdl/iomem.rs index b059b8612..ed0b482a3 100644 --- a/tool/microkit/src/capdl/iomem.rs +++ b/tool/microkit/src/capdl/iomem.rs @@ -35,13 +35,16 @@ pub fn create_iospace( }), }); + const PD_TO_DOMAIN_ID_OFFSET: u16 = 1; + spec_container.add_root_object(CapDLNamedObject { name: format!("IOSpace_{}", pd_name,).into(), object: Object::IOSpace(object::IOSpace { pci_bus, pci_device, dev_func, - pd_id, + domain_id: u16::try_from(pd_id).expect(&format!("The pd id {} is too large!", pd_id)) + + PD_TO_DOMAIN_ID_OFFSET, slots: vec![capdl_util_make_cte( 0, Cap::IOPageTable(cap::IOPageTable { object: id }), From 2dc4f59224e0a885cc50f0d14ced5301f977afd0 Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Mon, 16 Mar 2026 16:23:40 +1100 Subject: [PATCH 05/13] Check whether IOMMU is enabled in Kernel Config. Signed-off-by: Cheng Li --- tool/microkit/src/capdl/builder.rs | 4 +++- tool/microkit/src/main.rs | 7 +++++++ tool/microkit/src/sel4.rs | 1 + 3 files changed, 11 insertions(+), 1 deletion(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index e72c4ecd9..b24ceff58 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -702,7 +702,7 @@ pub fn build_capdl_spec( } // Step 3-4 Create and Map IO Page Table Structure - { + if kernel_config.iommu { let mut pci_to_iospace: HashMap<(u8, u8, u8), ObjectId> = HashMap::new(); for iomap in &pd.iomaps { let iospace_id = @@ -736,6 +736,8 @@ pub fn build_capdl_spec( frames, ); } + } else if pd.iomaps.len() != 0 { + return Err(format!("ERROR: System description file contains iomap elements despite IOMMU is not supported!")); } // Step 3-5 Create Scheduling Context diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index 600087272..5e0616b7b 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -487,6 +487,12 @@ fn main() -> Result<(), String> { _ => false, }; + // Add check to make sure IOMMU is enabled and the platform is x86 in kernel_config_json. + let iommu = match arch { + Arch::X86_64 => json_str_as_bool(&kernel_config_json, "IOMMU")?, + _ => false, + }; + let arm_pa_size_bits = match arch { Arch::Aarch64 => { if json_str_as_bool(&kernel_config_json, "ARM_PA_SIZE_BITS_40")? { @@ -525,6 +531,7 @@ fn main() -> Result<(), String> { "MAX_NUM_BOOTINFO_UNTYPED_CAPS", )?, hypervisor, + iommu, benchmark: args.config == "benchmark", num_cores: if json_str_as_bool(&kernel_config_json, "ENABLE_SMP_SUPPORT")? { json_str_as_u64(&kernel_config_json, "MAX_NUM_NODES")? diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index fe2154661..0d663af2d 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -290,6 +290,7 @@ pub struct Config { pub fan_out_limit: u64, pub max_num_bootinfo_untypeds: u64, pub hypervisor: bool, + pub iommu: bool, pub benchmark: bool, pub num_cores: u8, pub fpu: bool, From cac9f93aadaf9f3494de6edefbbd5f4c7f174e37 Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Wed, 18 Mar 2026 12:53:40 +1100 Subject: [PATCH 06/13] Add config and memory region sanity checks. Signed-off-by: Cheng Li --- tool/microkit/src/sdf.rs | 68 +++++++++++++++++++++++++++++++++++++ tool/microkit/tests/test.rs | 2 ++ 2 files changed, 70 insertions(+) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 249c3e3dd..b2ecad414 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -163,6 +163,7 @@ pub struct IOMemMap { pub pci_dev: u8, pub dev_func: u8, pub ioaddr: u64, + pub text_pos: Option, } #[derive(Debug, PartialEq, Eq)] @@ -512,6 +513,7 @@ impl IOMemMap { pci_dev: u8::try_from(pci_parts[1]).unwrap(), dev_func: u8::try_from(pci_parts[2]).unwrap(), ioaddr, + text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), }) } } @@ -1606,6 +1608,69 @@ pub struct SystemDescription { pub channels: Vec, } +fn io_check_maps( + xml_sdf: &XmlSystemDescription, + mrs: &[SysMemoryRegion], + e: &dyn ExecutionContext, + io_maps: &[IOMemMap], +) -> Result<(), String> { + let mut checked_maps = Vec::with_capacity(io_maps.len()); + for io_map in io_maps { + let maybe_mr = mrs.iter().find(|mr| mr.name == io_map.name); + let pos = io_map.text_pos.unwrap(); + match maybe_mr { + Some(mr) => { + // Page size check + if mr.page_size_bytes() != PageSize::Small as u64 { + return Err(format!( + "Error: invalid page size specified on 'iomap' @ {}, only 4 KB page size is supported for x86 IOMMU", + loc_string(xml_sdf, pos) + )); + } + // Alignment check + if !io_map.ioaddr.is_multiple_of(mr.page_size_bytes()) { + return Err(format!( + "Error: invalid ioaddr alignment on 'iomap' @ {}", + loc_string(xml_sdf, pos) + )); + } + + // Overlap check + let map_start = io_map.ioaddr; + let map_end = map_start + mr.size; + for (name, start, end) in &checked_maps { + if !(map_start >= *end || map_end <= *start) { + return Err( + format!( + "Error: map for '{}' has virtual address range [0x{:x}..0x{:x}) which overlaps with map for '{}' [0x{:x}..0x{:x}) in {} '{}' @ {}", + io_map.name, + map_start, + map_end, + name, + start, + end, + e.kind(), + e.name(), + loc_string(xml_sdf, pos) + ) + ); + } + } + checked_maps.push((&io_map.name, map_start, map_end)); + } + None => { + return Err(format!( + "Error: invalid memory region name '{}' on 'map' @ {}", + io_map.name, + loc_string(xml_sdf, pos) + )) + } + } + } + + Ok(()) +} + fn check_maps( xml_sdf: &XmlSystemDescription, mrs: &[SysMemoryRegion], @@ -2097,6 +2162,9 @@ pub fn parse( // Ensure that all maps are correct for pd in &pds { check_maps(&xml_sdf, &mrs, pd, &pd.maps)?; + if pd.iomaps.len() != 0 { + io_check_maps(&xml_sdf, &mrs, pd, &pd.iomaps)? + } if let Some(vm) = &pd.virtual_machine { check_maps(&xml_sdf, &mrs, vm, &vm.maps)?; } diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 62137bf5c..82bdca1a6 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -21,6 +21,7 @@ const DEFAULT_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config { max_num_bootinfo_untypeds: 230, fan_out_limit: 256, hypervisor: true, + iommu: false, benchmark: false, num_cores: 1, fpu: true, @@ -45,6 +46,7 @@ const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config { max_num_bootinfo_untypeds: 230, fan_out_limit: 256, hypervisor: true, + iommu: true, benchmark: false, num_cores: 1, fpu: true, From bdf848f6b19fc97e8fcd33166172d9eac5eaf7ff Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Thu, 19 Mar 2026 15:02:56 +1100 Subject: [PATCH 07/13] Use the three-level VTD PD structure instead of the four-level structure for generating spec in microkit tool. Signed-off-by: Cheng Li --- tool/microkit/src/capdl/iomem.rs | 110 +++++++++++++++++++------------ 1 file changed, 69 insertions(+), 41 deletions(-) diff --git a/tool/microkit/src/capdl/iomem.rs b/tool/microkit/src/capdl/iomem.rs index ed0b482a3..1e657dd67 100644 --- a/tool/microkit/src/capdl/iomem.rs +++ b/tool/microkit/src/capdl/iomem.rs @@ -1,16 +1,23 @@ +use std::ops::Range; + use sel4_capdl_initializer_types::{cap, object, Cap, Object, ObjectId}; use crate::{ capdl::{ - memory::{get_pt_level_coverage, get_pt_level_index, get_pt_level_to_insert}, util::capdl_util_make_cte, CapDLNamedObject, CapDLSpecContainer, }, - sel4::{Config, PageSize}, + sel4::Config, }; -const VTD_PML4_LEVEL: u8 = 0; -const VTD_ENTRY_LEVEL: u8 = 4; +// VTD Page table level is defaulted to the three-level structure even if the hardware supports four level. +// Sel4 will only attempt to use the four-level structure if the hardware does not supports three level. +// https://github.com/seL4/seL4/blob/c406015c389decc4559fd44cb69604ddd24a0ddb/src/plat/pc99/machine/intel-vtd.c#L498 +const VTD_PDPT_LEVEL: u8 = 0; +const VTD_PAGE_TABLE_LEVEL: u8 = 3; +const VTD_BITS_PER_LEVEL: u8 = 9; +const VTD_ENTRY_BITS: u8 = 12; +pub(crate) const VTD_THREE_LEVEL_BITS: u8 = VTD_BITS_PER_LEVEL * VTD_PAGE_TABLE_LEVEL + VTD_ENTRY_BITS; pub fn create_iospace( spec_container: &mut CapDLSpecContainer, @@ -24,13 +31,13 @@ pub fn create_iospace( let id = spec_container.add_root_object(CapDLNamedObject { name: format!( "{}_{}", - get_iopt_level_name(sel4_config, VTD_PML4_LEVEL as usize), + get_iopt_level_name(sel4_config, VTD_PDPT_LEVEL), pd_name, ) .into(), object: Object::IOPageTable(object::IOPageTable { is_root: true, - level: Some(VTD_PML4_LEVEL), + level: Some(VTD_PDPT_LEVEL), slots: [].to_vec(), }), }); @@ -55,13 +62,31 @@ pub fn create_iospace( id } -fn get_iopt_level_name(sel4_config: &Config, level: usize) -> &str { +pub fn map_io_page( + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + pd_name: &str, + iospace_obj_id: ObjectId, + frame_cap: Cap, + ioaddr: u64, +) -> Result<(), String> { + map_recursive( + spec_container, + sel4_config, + pd_name, + iospace_obj_id, + VTD_PDPT_LEVEL, + frame_cap, + ioaddr, + ) +} + +fn get_iopt_level_name(sel4_config: &Config, level: u8) -> &str { match sel4_config.arch { crate::sel4::Arch::X86_64 => match level { - 0 => "VTD_pml4", - 1 => "VTD_pdpt", - 2 => "VTD_pd", - 3 => "VTD_pt", + 0 => "VTD_pdpt", + 1 => "VTD_pd", + 2 => "VTD_pt", _ => unreachable!(), }, _ => unreachable!("get_iopt_level_name(): Internal bug: Only x86 support iommu!"), @@ -76,9 +101,9 @@ fn map_intermediary_level_helper( pd_name: &str, next_level_name_prefix: &str, cur_level_obj_id: ObjectId, - cur_level: usize, + cur_level: u8, cur_level_slot: usize, - vaddr: u64, + ioaddr: u64, ) -> Result { let page_table_level_obj_wrapper = spec_container.get_root_object(cur_level_obj_id).unwrap(); if let Object::IOPageTable(page_table_object) = &page_table_level_obj_wrapper.object { @@ -102,7 +127,7 @@ fn map_intermediary_level_helper( } // get_pt_level_coverage works the same for io memory as well - let next_level_coverage = get_pt_level_coverage(sel4_config, cur_level + 1, vaddr); + let next_level_coverage = get_io_pt_level_coverage(sel4_config, cur_level + 1, ioaddr); let next_level_inner_obj = object::IOPageTable { is_root: false, // IOSpace is always created seperately level: Some(cur_level as u8 + 1), @@ -138,7 +163,7 @@ fn map_intermediary_level_helper( fn insert_cap_into_io_page_table_level( spec_container: &mut CapDLSpecContainer, cur_level_obj_id: ObjectId, - cur_level: usize, + cur_level: u8, cur_level_slot: usize, cap: Cap, ) -> Result<(), String> { @@ -175,22 +200,17 @@ fn map_recursive( sel4_config: &Config, pd_name: &str, pt_obj_id: ObjectId, - cur_level: usize, + cur_level: u8, frame_cap: Cap, ioaddr: u64, ) -> Result<(), String> { - assert!( - VTD_ENTRY_LEVEL as usize == sel4_config.num_page_table_levels(), - "internal bug: The maximum page table level does not match!" - ); - - if cur_level >= sel4_config.num_page_table_levels() { + if cur_level >= VTD_PAGE_TABLE_LEVEL { unreachable!("internal bug: we should have never recursed further!"); } - let this_level_index = get_pt_level_index(sel4_config, cur_level, ioaddr); + let this_level_index = get_io_pt_level_index(sel4_config, cur_level, ioaddr); - if cur_level == get_pt_level_to_insert(sel4_config, PageSize::Small as u64) { + if cur_level == VTD_PAGE_TABLE_LEVEL - 1 { // Base case: we got to the target level to insert the frame cap. insert_cap_into_io_page_table_level( spec_container, @@ -226,21 +246,29 @@ fn map_recursive( } } -pub fn map_io_page( - spec_container: &mut CapDLSpecContainer, - sel4_config: &Config, - pd_name: &str, - iospace_obj_id: ObjectId, - frame_cap: Cap, - ioaddr: u64, -) -> Result<(), String> { - map_recursive( - spec_container, - sel4_config, - pd_name, - iospace_obj_id, - VTD_PML4_LEVEL as usize, - frame_cap, - ioaddr, - ) +fn get_io_pt_level_index(sel4_config: &Config, level: u8, ioaddr: u64) -> usize { + match sel4_config.arch { + crate::sel4::Arch::X86_64 => { + assert!(level < VTD_PAGE_TABLE_LEVEL); + + let shift = VTD_BITS_PER_LEVEL * (VTD_PAGE_TABLE_LEVEL - level) - VTD_BITS_PER_LEVEL + VTD_ENTRY_BITS; + + ((ioaddr >> shift) & ((1u64 << VTD_BITS_PER_LEVEL) - 1)) as usize + }, + crate::sel4::Arch::Aarch64 => unreachable!("Internal bug: Aarch64 is not supported for IOMMU"), + crate::sel4::Arch::Riscv64 => unreachable!("Internal bug: Riscv64 is not supported for IOMMU"), + } } + +fn get_io_pt_level_coverage(sel4_config: &Config, level: u8, ioaddr: u64) -> Range { + match sel4_config.arch { + crate::sel4::Arch::X86_64 => { + let bits_from_higher_lvls: u64 = (VTD_PAGE_TABLE_LEVEL as u64 - (level as u64)) * VTD_BITS_PER_LEVEL as u64; + let coverage_bits = VTD_BITS_PER_LEVEL as u64 + bits_from_higher_lvls; + let low = (ioaddr >> coverage_bits) << coverage_bits; + let high = ioaddr | ((1 << coverage_bits) - 1); + low..high + }, + _ => unreachable!("get_io_pt_level_coverage(): Internal bug: IOMMU is only supported for x86!"), + } +} \ No newline at end of file From e63fbac77f3b746b59b667c9b4f898eb4e89e859 Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Mon, 23 Mar 2026 14:08:32 +1100 Subject: [PATCH 08/13] Change the code back to default for four level VTD page table. Signed-off-by: Cheng Li --- tool/microkit/src/capdl/iomem.rs | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/tool/microkit/src/capdl/iomem.rs b/tool/microkit/src/capdl/iomem.rs index 1e657dd67..d49c3ac54 100644 --- a/tool/microkit/src/capdl/iomem.rs +++ b/tool/microkit/src/capdl/iomem.rs @@ -13,11 +13,11 @@ use crate::{ // VTD Page table level is defaulted to the three-level structure even if the hardware supports four level. // Sel4 will only attempt to use the four-level structure if the hardware does not supports three level. // https://github.com/seL4/seL4/blob/c406015c389decc4559fd44cb69604ddd24a0ddb/src/plat/pc99/machine/intel-vtd.c#L498 -const VTD_PDPT_LEVEL: u8 = 0; -const VTD_PAGE_TABLE_LEVEL: u8 = 3; +const VTD_PML4_LEVEL: u8 = 0; +const VTD_PAGE_TABLE_LEVEL: u8 = 4; const VTD_BITS_PER_LEVEL: u8 = 9; const VTD_ENTRY_BITS: u8 = 12; -pub(crate) const VTD_THREE_LEVEL_BITS: u8 = VTD_BITS_PER_LEVEL * VTD_PAGE_TABLE_LEVEL + VTD_ENTRY_BITS; +// pub(crate) const VTD_WHOLE_BITS: u8 = VTD_BITS_PER_LEVEL * VTD_PAGE_TABLE_LEVEL + VTD_ENTRY_BITS; pub fn create_iospace( spec_container: &mut CapDLSpecContainer, @@ -31,13 +31,13 @@ pub fn create_iospace( let id = spec_container.add_root_object(CapDLNamedObject { name: format!( "{}_{}", - get_iopt_level_name(sel4_config, VTD_PDPT_LEVEL), + get_iopt_level_name(sel4_config, VTD_PML4_LEVEL), pd_name, ) .into(), object: Object::IOPageTable(object::IOPageTable { is_root: true, - level: Some(VTD_PDPT_LEVEL), + level: Some(VTD_PML4_LEVEL), slots: [].to_vec(), }), }); @@ -75,7 +75,7 @@ pub fn map_io_page( sel4_config, pd_name, iospace_obj_id, - VTD_PDPT_LEVEL, + VTD_PML4_LEVEL, frame_cap, ioaddr, ) @@ -84,9 +84,10 @@ pub fn map_io_page( fn get_iopt_level_name(sel4_config: &Config, level: u8) -> &str { match sel4_config.arch { crate::sel4::Arch::X86_64 => match level { - 0 => "VTD_pdpt", - 1 => "VTD_pd", - 2 => "VTD_pt", + 0 => "VTD_pml4", + 1 => "VTD_pdpt", + 2 => "VTD_pd", + 3 => "VTD_pt", _ => unreachable!(), }, _ => unreachable!("get_iopt_level_name(): Internal bug: Only x86 support iommu!"), From 72abe7930cb65e6c63e667373e77f6ca824a7983 Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Wed, 25 Mar 2026 15:45:05 +1100 Subject: [PATCH 09/13] Add check to make sure the io addresses are in valid range. Refine the check unused mr and mr page size optimization logic for iomaps support. Signed-off-by: Cheng Li --- tool/microkit/src/capdl/iomem.rs | 35 +++++++++++++++++++------------- tool/microkit/src/capdl/mod.rs | 2 +- tool/microkit/src/sdf.rs | 32 ++++++++++++++++++++++++++--- 3 files changed, 51 insertions(+), 18 deletions(-) diff --git a/tool/microkit/src/capdl/iomem.rs b/tool/microkit/src/capdl/iomem.rs index d49c3ac54..522fdee88 100644 --- a/tool/microkit/src/capdl/iomem.rs +++ b/tool/microkit/src/capdl/iomem.rs @@ -3,10 +3,7 @@ use std::ops::Range; use sel4_capdl_initializer_types::{cap, object, Cap, Object, ObjectId}; use crate::{ - capdl::{ - util::capdl_util_make_cte, - CapDLNamedObject, CapDLSpecContainer, - }, + capdl::{util::capdl_util_make_cte, CapDLNamedObject, CapDLSpecContainer}, sel4::Config, }; @@ -15,9 +12,11 @@ use crate::{ // https://github.com/seL4/seL4/blob/c406015c389decc4559fd44cb69604ddd24a0ddb/src/plat/pc99/machine/intel-vtd.c#L498 const VTD_PML4_LEVEL: u8 = 0; const VTD_PAGE_TABLE_LEVEL: u8 = 4; +const VTD_SEL4_DEFAULT_PT_LEVEL: u8 = 3; const VTD_BITS_PER_LEVEL: u8 = 9; const VTD_ENTRY_BITS: u8 = 12; -// pub(crate) const VTD_WHOLE_BITS: u8 = VTD_BITS_PER_LEVEL * VTD_PAGE_TABLE_LEVEL + VTD_ENTRY_BITS; +pub(crate) const VTD_MAX_ADDR: u64 = + (1 << (VTD_BITS_PER_LEVEL * VTD_SEL4_DEFAULT_PT_LEVEL + VTD_ENTRY_BITS)) - 1; pub fn create_iospace( spec_container: &mut CapDLSpecContainer, @@ -251,25 +250,33 @@ fn get_io_pt_level_index(sel4_config: &Config, level: u8, ioaddr: u64) -> usize match sel4_config.arch { crate::sel4::Arch::X86_64 => { assert!(level < VTD_PAGE_TABLE_LEVEL); - - let shift = VTD_BITS_PER_LEVEL * (VTD_PAGE_TABLE_LEVEL - level) - VTD_BITS_PER_LEVEL + VTD_ENTRY_BITS; + + let shift = VTD_BITS_PER_LEVEL * (VTD_PAGE_TABLE_LEVEL - level) - VTD_BITS_PER_LEVEL + + VTD_ENTRY_BITS; ((ioaddr >> shift) & ((1u64 << VTD_BITS_PER_LEVEL) - 1)) as usize - }, - crate::sel4::Arch::Aarch64 => unreachable!("Internal bug: Aarch64 is not supported for IOMMU"), - crate::sel4::Arch::Riscv64 => unreachable!("Internal bug: Riscv64 is not supported for IOMMU"), + } + crate::sel4::Arch::Aarch64 => { + unreachable!("Internal bug: Aarch64 is not supported for IOMMU") + } + crate::sel4::Arch::Riscv64 => { + unreachable!("Internal bug: Riscv64 is not supported for IOMMU") + } } } fn get_io_pt_level_coverage(sel4_config: &Config, level: u8, ioaddr: u64) -> Range { match sel4_config.arch { crate::sel4::Arch::X86_64 => { - let bits_from_higher_lvls: u64 = (VTD_PAGE_TABLE_LEVEL as u64 - (level as u64)) * VTD_BITS_PER_LEVEL as u64; + let bits_from_higher_lvls: u64 = + (VTD_PAGE_TABLE_LEVEL as u64 - (level as u64)) * VTD_BITS_PER_LEVEL as u64; let coverage_bits = VTD_BITS_PER_LEVEL as u64 + bits_from_higher_lvls; let low = (ioaddr >> coverage_bits) << coverage_bits; let high = ioaddr | ((1 << coverage_bits) - 1); low..high - }, - _ => unreachable!("get_io_pt_level_coverage(): Internal bug: IOMMU is only supported for x86!"), + } + _ => unreachable!( + "get_io_pt_level_coverage(): Internal bug: IOMMU is only supported for x86!" + ), } -} \ No newline at end of file +} diff --git a/tool/microkit/src/capdl/mod.rs b/tool/microkit/src/capdl/mod.rs index 2df7192d9..72fafaf84 100644 --- a/tool/microkit/src/capdl/mod.rs +++ b/tool/microkit/src/capdl/mod.rs @@ -7,7 +7,7 @@ pub mod allocation; pub mod builder; pub mod initialiser; -mod iomem; +pub mod iomem; mod irq; mod memory; pub mod packaging; diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index b2ecad414..8684fe0b7 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -1635,14 +1635,26 @@ fn io_check_maps( )); } - // Overlap check + // Addr and Overlap check let map_start = io_map.ioaddr; let map_end = map_start + mr.size; + if map_end > crate::capdl::iomem::VTD_MAX_ADDR { + return Err( + format!( + "Error: map for '{}' has io address 0x{:x} which exceeds the upper limits of VTD in {} '{}' @ {}", + io_map.name, + map_end, + e.kind(), + e.name(), + loc_string(xml_sdf, pos) + ) + ); + } for (name, start, end) in &checked_maps { if !(map_start >= *end || map_end <= *start) { return Err( format!( - "Error: map for '{}' has virtual address range [0x{:x}..0x{:x}) which overlaps with map for '{}' [0x{:x}..0x{:x}) in {} '{}' @ {}", + "Error: map for '{}' has io address range [0x{:x}..0x{:x}) which overlaps with map for '{}' [0x{:x}..0x{:x}) in {} '{}' @ {}", io_map.name, map_start, map_end, @@ -2201,8 +2213,10 @@ pub fn parse( // Check that all MRs are used let mut all_maps = vec![]; + let mut all_iomaps = vec![]; for pd in &pds { all_maps.extend(&pd.maps); + all_iomaps.extend(&pd.iomaps); if let Some(vm) = &pd.virtual_machine { all_maps.extend(&vm.maps); } @@ -2215,7 +2229,12 @@ pub fn parse( break; } } - + for iomap in &all_iomaps { + if iomap.name == mr.name { + found = true; + break; + } + } if !found { println!("WARNING: unused memory region '{}'", mr.name); } @@ -2234,6 +2253,13 @@ pub fn parse( continue; } + // Check if this MR is mapped as io memory + for iomap in &all_iomaps { + if iomap.name == mr.name { + continue; + } + } + // Get all the addresses that this MR will be mapped into let mut addrs: Vec<_> = all_maps .iter() From 17d437453bc8d0443b8a5fd2509f10fccfe25037 Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Fri, 27 Mar 2026 17:07:21 +1100 Subject: [PATCH 10/13] Add perms and setvar for iomap. Signed-off-by: Cheng Li --- tool/microkit/src/capdl/builder.rs | 7 ++- tool/microkit/src/sdf.rs | 72 +++++++++++++++++++++++++----- tool/microkit/src/sel4.rs | 8 ---- tool/microkit/src/symbols.rs | 1 + tool/microkit/tests/test.rs | 2 +- 5 files changed, 67 insertions(+), 23 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index b24ceff58..d3d6d6c63 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -392,9 +392,12 @@ fn map_io_memory_region( frames: &[ObjectId], ) { let mut cur_vaddr = map.ioaddr; + let read = map.perms & SysMapPerms::Read as u8 != 0; + let write = map.perms & SysMapPerms::Write as u8 != 0; + for frame_obj_id in frames.iter() { - // Make a cap for this frame. The perms should not matter in IOMMU - let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, true, true, false, false); + // Make a cap for this frame. + let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, read, write, false, false); // Map it into this PD IOSpace. map_io_page( spec_container, diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 8684fe0b7..5f21eceec 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -163,6 +163,7 @@ pub struct IOMemMap { pub pci_dev: u8, pub dev_func: u8, pub ioaddr: u64, + pub perms: u8, pub text_pos: Option, } @@ -225,6 +226,7 @@ pub enum SysSetVarKind { Id { id: u64 }, X86IoPortAddr { address: u64 }, PrefillSize { mr: String }, + IoAddr { address: u64 }, } #[derive(Debug, PartialEq, Eq)] @@ -433,6 +435,7 @@ impl IOMemMap { config: &Config, xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, + allow_setvar: bool, ) -> Result { const PCI_DEV_MAX: u8 = 0x1F; const DEV_FUNC_MAX: u8 = 0b111; @@ -444,21 +447,44 @@ impl IOMemMap { )); } - check_attributes(xml_sdf, &node, &["mr", "pcidev", "addr"])?; + let mut attrs = vec!["mr", "pcidev", "addr"]; + if allow_setvar { + attrs.push("setvar_vaddr"); + attrs.push("setvar_size"); + } + + check_attributes(xml_sdf, &node, &attrs)?; let mr = checked_lookup(xml_sdf, node, "mr")?.to_string(); let pcidev_str = checked_lookup(xml_sdf, node, "pcidev")?.to_string(); let ioaddr = sdf_parse_number(checked_lookup(xml_sdf, node, "addr")?, node)?; - let max_ioaddr = config.iommu_top(); - - if ioaddr >= max_ioaddr { - return Err(value_error( - xml_sdf, - node, - format!("ioaddr (0x{ioaddr:x}) must be less than 0x{max_ioaddr:x}"), - )); - } + let perms = if let Some(xml_perms) = node.attribute("perms") { + match SysMapPerms::from_str(xml_perms) { + Ok(parsed_perms) => { + if parsed_perms != SysMapPerms::Read as u8 | SysMapPerms::Write as u8 + || parsed_perms != SysMapPerms::Read as u8 + { + return Err(value_error( + xml_sdf, + node, + "perms for io mapped memory can only be 'r' or 'rw'".to_string(), + )); + } + parsed_perms + } + Err(()) => { + return Err(value_error( + xml_sdf, + node, + "perms for io mapped memory can only be 'r' or 'rw'".to_string(), + )) + } + } + } else { + // Default to read-write + SysMapPerms::Read as u8 | SysMapPerms::Write as u8 + }; let pci_parts: Vec = pcidev_str .split([':', '.']) @@ -513,6 +539,7 @@ impl IOMemMap { pci_dev: u8::try_from(pci_parts[1]).unwrap(), dev_func: u8::try_from(pci_parts[2]).unwrap(), ioaddr, + perms, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), }) } @@ -1097,7 +1124,27 @@ impl ProtectionDomain { } } "iomap" => { - let iomap = IOMemMap::from_xml(config, xml_sdf, &child)?; + let iomap = IOMemMap::from_xml(config, xml_sdf, &child, true)?; + + if let Some(setvar_vaddr) = child.attribute("setvar_vaddr") { + let setvar = SysSetVar { + symbol: setvar_vaddr.to_string(), + kind: SysSetVarKind::IoAddr { + address: iomap.ioaddr, + }, + }; + checked_add_setvar(&mut setvars, setvar, xml_sdf, &child)?; + } + + if let Some(setvar_size) = child.attribute("setvar_size") { + let setvar = SysSetVar { + symbol: setvar_size.to_string(), + kind: SysSetVarKind::Size { + mr: iomap.name.clone(), + }, + }; + checked_add_setvar(&mut setvars, setvar, xml_sdf, &child)?; + } iomaps.push(iomap); } @@ -1641,9 +1688,10 @@ fn io_check_maps( if map_end > crate::capdl::iomem::VTD_MAX_ADDR { return Err( format!( - "Error: map for '{}' has io address 0x{:x} which exceeds the upper limits of VTD in {} '{}' @ {}", + "Error: iomap for '{}' has address 0x{:x} which exceeds the upper limits of {} in {} '{}' @ {}", io_map.name, map_end, + crate::capdl::iomem::VTD_MAX_ADDR, e.kind(), e.name(), loc_string(xml_sdf, pos) diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index 0d663af2d..16f969c2b 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -326,14 +326,6 @@ impl Config { } } - pub fn iommu_top(&self) -> u64 { - match self.arch { - Arch::Aarch64 => unreachable!("Internal bug: Aarch64 doesn't support IOMMU"), - Arch::Riscv64 => unreachable!("Internal bug: Risv64 doesn't support IOMMU"), - Arch::X86_64 => 1 << (12 + 9 + 9 + 9), - } - } - pub fn virtual_base(&self) -> u64 { match self.arch { Arch::Aarch64 => match self.hypervisor { diff --git a/tool/microkit/src/symbols.rs b/tool/microkit/src/symbols.rs index 477ef5c7b..fb5c09627 100644 --- a/tool/microkit/src/symbols.rs +++ b/tool/microkit/src/symbols.rs @@ -159,6 +159,7 @@ pub fn patch_symbols( sdf::SysSetVarKind::PrefillSize { mr } => { mr_name_to_desc[mr].prefill_bytes.as_ref().unwrap().len() as u64 } + sdf::SysSetVarKind::IoAddr { address } => *address, }; symbols_to_write.push((&setvar.symbol, data)); } diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 82bdca1a6..dcdf700c7 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -631,7 +631,7 @@ mod protection_domain { check_error( &DEFAULT_X86_64_KERNEL_CONFIG, "iommu_out_of_bound.system", - "Error: ioaddr (0x8000000000) must be less than 0x8000000000 on element 'iomap':", + "Error: iomap for 'region' has address 0x8000001000 which exceeds the upper limits of 549755813887 in protection domain 'test' @ iommu_out_of_bound.system:13:9", ) } } From 62eb4cc22e8cb905a8b309248235109aade539d4 Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Fri, 10 Apr 2026 17:19:55 +1000 Subject: [PATCH 11/13] Remove unused code. Signed-off-by: Cheng Li --- example/iommu/blk/blk.system | 84 ------------------------------------ example/iommu/build.sh | 14 ------ 2 files changed, 98 deletions(-) delete mode 100644 example/iommu/blk/blk.system delete mode 100644 example/iommu/build.sh diff --git a/example/iommu/blk/blk.system b/example/iommu/blk/blk.system deleted file mode 100644 index a1adc00e7..000000000 --- a/example/iommu/blk/blk.system +++ /dev/null @@ -1,84 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file diff --git a/example/iommu/build.sh b/example/iommu/build.sh deleted file mode 100644 index ebde05574..000000000 --- a/example/iommu/build.sh +++ /dev/null @@ -1,14 +0,0 @@ -source ~/system/myvenv/bin/activate -BOARDS=x86_64_generic -python build_sdk.py --skip-docs --skip-tar --configs=debug --boards=$BOARDS --sel4=/home/cheng/work/seL4 -cd ./example/hello -make MICROKIT_SDK=/home/cheng/work/microkit/release/microkit-sdk-2.1.0-dev MICROKIT_CONFIG=debug BUILD_DIR=build MICROKIT_BOARD=x86_64_generic - -qemu-system-x86_64 -machine q35 -kernel /home/cheng/work/microkit/release/microkit-sdk-2.1.0-dev/board/x86_64_generic/debug/elf/sel4_32.elf -m size=2G -serial mon:stdio -cpu qemu64,+fsgsbase,+pdpe1gb,+pcid,+invpcid,+xsave,+xsaves,+xsaveopt -initrd loader.img -device intel-iommu,intremap=on,caching-mode=on -device virtio-blk-pci,drive=hd,addr=0x3.0,iommu_platform=on,disable-legacy=on \ --nographic \ --d guest_errors \ --drive file=disk,if=none,format=raw,id=hd - -/home/cheng/work/microkit/release/microkit-sdk-2.1.0-dev/bin/microkit blk.system --search-path /home/cheng/work/sddf/examples/blk/build --board x86_64_generic --config debug -o loader.img -r report.txt - -qemu-system-x86_64 -machine q35 -kernel /home/cheng/work/microkit/release/microkit-sdk-2.1.0-dev/board/x86_64_generic/debug/elf/sel4_32.elf -m size=2G -serial mon:stdio -cpu qemu64,+fsgsbase,+pdpe1gb,+pcid,+invpcid,+xsave,+xsaves,+xsaveopt -initrd loader.img -device intel-iommu,intremap=on,caching-mode=on -device virtio-blk-pci,drive=hd,addr=0x3.0,iommu_platform=on,disable-legacy=on -nographic -d guest_errors -drive file=disk,if=none,format=raw,id=hd \ No newline at end of file From 6d880c90f3ab05ca1bc90f8f7736e84d90871055 Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Wed, 15 Apr 2026 15:34:54 +1000 Subject: [PATCH 12/13] Enable x86 iommu in build_sdk.py. Signed-off-by: Cheng Li --- build_sdk.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build_sdk.py b/build_sdk.py index 5ff324b1f..1f6050a3b 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -68,7 +68,7 @@ "KernelPlatform": "pc99", "KernelX86MicroArch": "generic", # See https://github.com/seL4/microkit/issues/418 for details. - "KernelIOMMU": False, + "KernelIOMMU": True, } | DEFAULT_KERNEL_OPTIONS From bd75a2f76b2fdf240ec565870372ab1b70d112f4 Mon Sep 17 00:00:00 2001 From: Cheng Li Date: Mon, 20 Apr 2026 15:07:47 +1000 Subject: [PATCH 13/13] Improve code. Signed-off-by: Cheng Li --- Cargo.toml | 6 ++++-- tool/microkit/src/capdl/builder.rs | 6 +++--- tool/microkit/src/capdl/iomem.rs | 6 +++--- tool/microkit/src/sdf.rs | 12 ++++++------ 4 files changed, 16 insertions(+), 14 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index f23c88b8c..c5f0d0e0e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,10 +12,12 @@ members = [ ] [workspace.dependencies.sel4-capdl-initializer] -path = "/home/cheng/system/rust-sel4/crates/sel4-capdl-initializer" +git = "https://github.com/au-ts/rust-sel4" +branch = "cheng/iommu_support" [workspace.dependencies.sel4-capdl-initializer-types] -path = "/home/cheng/system/rust-sel4/crates/sel4-capdl-initializer/types" +git = "https://github.com/au-ts/rust-sel4" +branch = "cheng/iommu_support" [profile.release.package.microkit-tool] strip = true diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index d3d6d6c63..a801ee847 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -710,7 +710,7 @@ pub fn build_capdl_spec( for iomap in &pd.iomaps { let iospace_id = match pci_to_iospace.get(&(iomap.pci_bus, iomap.pci_dev, iomap.dev_func)) { - Some(iospace_id) => iospace_id.clone(), + Some(iospace_id) => *iospace_id, None => { let iospace_id = create_iospace( &mut spec_container, @@ -739,8 +739,8 @@ pub fn build_capdl_spec( frames, ); } - } else if pd.iomaps.len() != 0 { - return Err(format!("ERROR: System description file contains iomap elements despite IOMMU is not supported!")); + } else if !pd.iomaps.is_empty() { + return Err("ERROR: System description file contains iomap elements despite IOMMU is not supported!".to_string()); } // Step 3-5 Create Scheduling Context diff --git a/tool/microkit/src/capdl/iomem.rs b/tool/microkit/src/capdl/iomem.rs index 522fdee88..4ce89616d 100644 --- a/tool/microkit/src/capdl/iomem.rs +++ b/tool/microkit/src/capdl/iomem.rs @@ -49,7 +49,8 @@ pub fn create_iospace( pci_bus, pci_device, dev_func, - domain_id: u16::try_from(pd_id).expect(&format!("The pd id {} is too large!", pd_id)) + domain_id: u16::try_from(pd_id) + .unwrap_or_else(|_| panic!("The pd id {} is too large!", pd_id)) + PD_TO_DOMAIN_ID_OFFSET, slots: vec![capdl_util_make_cte( 0, @@ -93,7 +94,6 @@ fn get_iopt_level_name(sel4_config: &Config, level: u8) -> &str { } } -// Just this one time pinky promise #[allow(clippy::too_many_arguments)] fn map_intermediary_level_helper( spec_container: &mut CapDLSpecContainer, @@ -130,7 +130,7 @@ fn map_intermediary_level_helper( let next_level_coverage = get_io_pt_level_coverage(sel4_config, cur_level + 1, ioaddr); let next_level_inner_obj = object::IOPageTable { is_root: false, // IOSpace is always created seperately - level: Some(cur_level as u8 + 1), + level: Some(cur_level + 1), slots: [].to_vec(), }; // We create name with this PT level coverage so that every object names are unique diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 5f21eceec..f27e21192 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -442,7 +442,7 @@ impl IOMemMap { if config.arch != Arch::X86_64 { return Err(value_error( xml_sdf, - &node, + node, "IOMMU isn't supported on ARM and RISC-V".to_string(), )); } @@ -453,7 +453,7 @@ impl IOMemMap { attrs.push("setvar_size"); } - check_attributes(xml_sdf, &node, &attrs)?; + check_attributes(xml_sdf, node, &attrs)?; let mr = checked_lookup(xml_sdf, node, "mr")?.to_string(); let pcidev_str = checked_lookup(xml_sdf, node, "pcidev")?.to_string(); @@ -508,7 +508,7 @@ impl IOMemMap { if pci_parts[0] != pci_bus as i64 { return Err(value_error( xml_sdf, - &node, + node, "Invalid value for PCI bus".to_string(), )); } @@ -518,7 +518,7 @@ impl IOMemMap { if pci_parts[1] != pci_dev as i64 || pci_dev > PCI_DEV_MAX { return Err(value_error( xml_sdf, - &node, + node, "Invalid value for PCI Device".to_string(), )); } @@ -528,7 +528,7 @@ impl IOMemMap { if pci_parts[2] != dev_func as i64 || dev_func > DEV_FUNC_MAX { return Err(value_error( xml_sdf, - &node, + node, "Invalid value for PCI Device Function".to_string(), )); } @@ -2222,7 +2222,7 @@ pub fn parse( // Ensure that all maps are correct for pd in &pds { check_maps(&xml_sdf, &mrs, pd, &pd.maps)?; - if pd.iomaps.len() != 0 { + if !pd.iomaps.is_empty() { io_check_maps(&xml_sdf, &mrs, pd, &pd.iomaps)? } if let Some(vm) = &pd.virtual_machine {