From c4898cf2b9a8fc2020cdab6432e0d0e95db36bf2 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 18 Jun 2026 15:06:04 +1000 Subject: [PATCH 1/9] IOMMU: Clean up sdf.rs Hex formatting. Signed-off-by: Callum --- tool/microkit/src/sdf.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 588b380b6..6350428f9 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -415,7 +415,7 @@ impl SysMap { return Err(value_error( xml_sdf, node, - format!("vaddr (0x{vaddr:x}) must be less than 0x{max_vaddr:x}"), + format!("vaddr ({vaddr:#x}) must be less than {max_vaddr:#x}"), )); } @@ -627,7 +627,7 @@ impl ProtectionDomain { xml_sdf, node, format!( - "stack size must be between 0x{PD_MIN_STACK_SIZE:x} bytes and 0x{PD_MAX_STACK_SIZE:x} bytes" + "stack size must be between {PD_MIN_STACK_SIZE:#x} bytes and {PD_MAX_STACK_SIZE:#x} bytes" ), )); } @@ -1525,7 +1525,7 @@ impl SysMemoryRegion { return Err(value_error( xml_sdf, node, - format!("page size 0x{page_size:x} not supported"), + format!("page size {page_size:#x} not supported"), )); } @@ -1784,7 +1784,7 @@ fn check_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 virtual address range [{:#x}..{:#x}) which overlaps with map for '{}' [{:#x}..{:#x}) in {} '{}' @ {}", map.mr, map_start, map_end, @@ -2345,7 +2345,7 @@ pub fn parse( let pos = mr.text_pos.unwrap(); return Err( format!( - "Error: memory region '{}' physical address range [0x{:x}..0x{:x}) overlaps with another memory region '{}' [0x{:x}..0x{:x}) @ {}", + "Error: memory region '{}' physical address range [{:#x}..{:#x}) overlaps with another memory region '{}' [{:#x}..{:#x}) @ {}", mr.name, mr_start, mr_end, From f733526e1a5a02e7611dba5c8b39c61c0c40ebe9 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 18 Jun 2026 13:52:02 +1000 Subject: [PATCH 2/9] IOMMU: Refactor check_maps Replace ExecutionContext trait with a Map trait. The previous trait was primarily used in the check_maps function to handle memory regions in virtual machines and normal pds. This Map trait will allow the one check_maps function to handle both SysIOMaps and SysMaps uniformly. The additional information that was provided by the polymorhpic ExecutionContext is just passed as a string to be used in the respective error message. This is because outside of the check_maps function a protection_domain and a virtual_machine are handled as distinct types. Add error checking cases to check_maps. If the map_start + mr.size overflows alot of the pre-exisiting logic breaks so check for it. Also check that we don't overflow the top of user_virtual memory accouting for the differences between protection_domains, virtual_machines and io address spaces. Signed-off-by: Callum --- tool/microkit/src/sdf.rs | 199 +++++++++++++++++++++++---------------- 1 file changed, 120 insertions(+), 79 deletions(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 6350428f9..77e7ece38 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -113,6 +113,40 @@ pub struct SysMap { pub text_pos: Option, } +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; +} + +impl Map for SysMap { + fn mr_name(&self) -> &str { + &self.mr + } + + fn addr(&self) -> u64 { + self.vaddr + } + + fn text_pos(&self) -> Option { + self.text_pos + } + + fn element(&self) -> &'static str { + "map" + } + + fn addr_name(&self) -> &'static str { + "vaddr" + } + + fn range_name(&self) -> &'static str { + "virtual address range" + } +} #[derive(Debug, PartialEq, Eq, Clone)] pub enum SysMemoryRegionKind { User, @@ -350,49 +384,6 @@ pub struct VirtualCpu { pub cpu: Option, } -/// To avoid code duplication for handling protection domains -/// and virtual machines, which have a lot in common. -trait ExecutionContext { - fn name(&self) -> &String; - fn kind(&self) -> &'static str; -} - -impl ExecutionContext for ProtectionDomain { - fn name(&self) -> &String { - &self.name - } - - fn kind(&self) -> &'static str { - "protection domain" - } -} - -impl ExecutionContext for VirtualMachine { - fn name(&self) -> &String { - &self.name - } - - fn kind(&self) -> &'static str { - "virtual machine" - } -} - -impl SysMapPerms { - fn from_str(s: &str) -> Result { - let mut perms = 0; - for c in s.chars() { - match c { - 'r' => perms |= SysMapPerms::Read as u8, - 'w' => perms |= SysMapPerms::Write as u8, - 'x' => perms |= SysMapPerms::Execute as u8, - _ => return Err(()), - } - } - - Ok(perms) - } -} - impl SysMap { fn from_xml( xml_sdf: &XmlSystemDescription, @@ -1759,55 +1750,93 @@ pub struct SystemDescription { pub channels: Vec, } -fn check_maps( +fn location_suffix_format( + xml_sdf: &XmlSystemDescription, + text_pos: Option, +) -> String { + text_pos + .map(|pos| format!("@ {}", loc_string(xml_sdf, pos))) + .unwrap_or_default() +} + +// max_end is the first invalid virtual address +fn check_maps<'a, M, I>( xml_sdf: &XmlSystemDescription, mrs: &[SysMemoryRegion], - e: &dyn ExecutionContext, - maps: &[SysMap], -) -> Result<(), String> { - let mut checked_maps = Vec::with_capacity(maps.len()); + maps: I, + address_space: &str, + max_end: u64, +) -> Result<(), String> +where + M: Map + 'a, + I: IntoIterator, +{ + let mut checked_maps: Vec<(&str, u64, u64)> = Vec::new(); + for map in maps { - let maybe_mr = mrs.iter().find(|mr| mr.name == map.mr); - let pos = map.text_pos.unwrap(); - match maybe_mr { + let element = map.element(); + match mrs.iter().find(|mr| mr.name == map.mr_name()) { Some(mr) => { - if !map.vaddr.is_multiple_of(mr.page_size_bytes()) { + if !map.addr().is_multiple_of(mr.page_size_bytes()) { return Err(format!( - "Error: invalid vaddr alignment on 'map' @ {}", - loc_string(xml_sdf, pos) + "Error: invalid {} alignment on '{element}' {}", + map.addr_name(), + location_suffix_format(xml_sdf, map.text_pos()) + )); + } + + let map_start = map.addr(); + let Some(map_end) = map_start.checked_add(mr.size) else { + return Err(format!( + "Error: {element} for '{}' has address range that overflows {}", + map.mr_name(), + location_suffix_format(xml_sdf, map.text_pos()) + )); + }; + + if map_end > max_end { + return Err(format!( + "Error: {element} for '{}' has {} [{:#x}..{:#x}) which exceeds valid address space [{:#x}..{:#x}) {}", + map.mr_name(), + map.range_name(), + map_start, + map_end, + 0, + max_end, + location_suffix_format(xml_sdf, map.text_pos()) )); } - let map_start = map.vaddr; - let map_end = map.vaddr + mr.size; - for (name, start, end) in &checked_maps { + for (name, start, end) in checked_maps.iter() { if !(map_start >= *end || map_end <= *start) { - return Err( - format!( - "Error: map for '{}' has virtual address range [{:#x}..{:#x}) which overlaps with map for '{}' [{:#x}..{:#x}) in {} '{}' @ {}", - map.mr, - map_start, - map_end, - name, - start, - end, - e.kind(), - e.name(), - loc_string(xml_sdf, map.text_pos.unwrap()) - ) - ); + return Err(format!( + "Error: map for '{}' has {} [{:#x}..{:#x}) which overlaps with map for '{}' [{:#x}..{:#x}) in {} {}", + map.mr_name(), + map.range_name(), + map_start, + map_end, + name, + start, + end, + address_space, + location_suffix_format(xml_sdf, map.text_pos()) + )); } } - checked_maps.push((&map.mr, map_start, map_end)); + checked_maps.push((map.mr_name(), map_start, map_end)); } None => { return Err(format!( - "Error: invalid memory region name '{}' on 'map' @ {}", - map.mr, - loc_string(xml_sdf, pos) - )) + "Error: invalid memory region name '{}' on '{element}' {}", + map.mr_name(), + location_suffix_format(xml_sdf, map.text_pos()) + )); } - }; + } + } + + Ok(()) +} } Ok(()) @@ -2296,9 +2325,21 @@ pub fn parse( // Ensure that all maps are correct for pd in &pds { - check_maps(&xml_sdf, &mrs, pd, &pd.maps)?; + check_maps( + &xml_sdf, + &mrs, + pd.maps.iter(), + &format!("protection domain '{}'", pd.name), + config.pd_map_max_vaddr(pd.stack_size), + )?; if let Some(vm) = &pd.virtual_machine { - check_maps(&xml_sdf, &mrs, vm, &vm.maps)?; + check_maps( + &xml_sdf, + &mrs, + vm.maps.iter(), + &format!("virtual machine '{}'", vm.name), + config.vm_map_max_vaddr(), + )?; } } From 92225c7a9d29c4795ffd5ced04dd58cc3d78703e Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 18 Jun 2026 14:11:04 +1000 Subject: [PATCH 3/9] SDF: Add PCIDevice Type Add PciDevice struct and PCIDeviceParseError enum. This types allow us to implement the Display trait which gives a consistent way to output PCI information. The FromStr trait implemented for PCIDevice avoid duplicating logic required to parse the PCI identifier from the xml. When combined with the display trait on the PCIDeviceParseError, we get consistent error messages and avoid repeating code. Signed-off-by: Callum --- tool/microkit/src/capdl/irq.rs | 12 +- tool/microkit/src/sdf.rs | 207 +++++++++++++++++---------------- 2 files changed, 110 insertions(+), 109 deletions(-) diff --git a/tool/microkit/src/capdl/irq.rs b/tool/microkit/src/capdl/irq.rs index b2ddde9fe..99f32ad61 100644 --- a/tool/microkit/src/capdl/irq.rs +++ b/tool/microkit/src/capdl/irq.rs @@ -86,18 +86,14 @@ fn create_irq_obj( }), }), SysIrqKind::MSI { - pci_bus, - pci_dev, - pci_func, - handle, - .. + pci_device, handle, .. } => Object::IrqMsi(object::IrqMsi { slots: [].to_vec(), extra: Box::new(object::IrqMsiExtraInfo { handle: Word(handle), - pci_bus: Word(pci_bus), - pci_dev: Word(pci_dev), - pci_func: Word(pci_func), + pci_bus: Word(pci_device.bus as u64), + pci_dev: Word(pci_device.device as u64), + pci_func: Word(pci_device.function as u64), }), }), }; diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 77e7ece38..d37275ff7 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -24,9 +24,10 @@ use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool}; use crate::MAX_PDS; use sel4_capdl_initializer_types::FillEntryContentBootInfoId; use std::collections::{HashMap, HashSet}; -use std::fmt::Display; +use std::fmt; use std::fs; use std::path::{Path, PathBuf}; +use std::str::FromStr; /// Events that come through entry points (e.g notified or protected) are given an /// identifier that is used as the badge at runtime. @@ -56,11 +57,6 @@ pub const PD_DEFAULT_STACK_SIZE: u64 = 0x2000; const PD_MIN_STACK_SIZE: u64 = 0x1000; const PD_MAX_STACK_SIZE: u64 = 1024 * 1024 * 16; -/// 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; - /// Maximum x86 IRQ vector value. Inclusive. /// This value is calculated by the kernel as `irq_user_max - irq_user_min` in /// `src/arch/x86/object/interrupt.c` @@ -95,6 +91,105 @@ 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, +} + +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; +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum PciDeviceParseError { + Malformed, + BusParse, + DeviceParse, + FunctionParse, + BusOutOfRange, + DeviceOutOfRange, + FunctionOutOfRange, +} + +impl fmt::Display for PciDevice { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!( + f, + "{:02x}:{:02x}.{:x}", + self.bus, self.device, self.function + ) + } +} + +impl fmt::Display for PciDeviceParseError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + PciDeviceParseError::Malformed => { + write!(f, "expected PCI address in bus:device.function form") + } + PciDeviceParseError::BusParse => write!(f, "failed to parse PCI bus"), + 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) + } + PciDeviceParseError::DeviceOutOfRange => { + write!( + f, + "PCI device must be within [0..{}]", + PciDevice::PCI_DEV_MAX + ) + } + PciDeviceParseError::FunctionOutOfRange => { + write!( + f, + "PCI function must be within [0..{}]", + PciDevice::PCI_FUNC_MAX + ) + } + } + } +} + +impl FromStr for PciDevice { + type Err = PciDeviceParseError; + + fn from_str(s: &str) -> Result { + let (bus_str, device_function_str) = + s.split_once(':').ok_or(PciDeviceParseError::Malformed)?; + let (device_str, function_str) = device_function_str + .split_once('.') + .ok_or(PciDeviceParseError::Malformed)?; + + let bus = + i64::from_str_radix(bus_str.trim(), 16).map_err(|_| PciDeviceParseError::BusParse)?; + let device = i64::from_str_radix(device_str.trim(), 16) + .map_err(|_| PciDeviceParseError::DeviceParse)?; + 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); + } + + Ok(PciDevice { + bus: bus as u8, + device: device as u8, + function: function as u8, + }) + } +} #[repr(u8)] pub enum SysMapPerms { Read = 1, @@ -224,9 +319,7 @@ pub enum SysIrqKind { }, /// x86-64 specific MSI { - pci_bus: u64, - pci_dev: u64, - pci_func: u64, + pci_device: PciDevice, handle: u64, vector: u64, }, @@ -293,7 +386,7 @@ pub struct Channel { #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] pub struct CpuCore(pub u8); -impl Display for CpuCore { +impl fmt::Display for CpuCore { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { f.write_fmt(format_args!("cpu{:02}", self.0)) } @@ -901,94 +994,8 @@ impl ProtectionDomain { &["id", "setvar_id", "pcidev", "handle", "vector"], )?; - // A "pcidev" attribute is in a form of Bus:Dev.Func - // Split by the colon then the dot. - - // If the input is valid, index 0 contains "Bus", index 1 contains - // "Dev.Func" - let pci_parts_by_colon: Vec<_> = - pcidev_str.split(':').map(str::trim).collect(); - - if pci_parts_by_colon.len() != 2 { - return Err(format!( - "Error: failed to parse PCI address '{}' on element '{}'", - pcidev_str, - child.tag_name().name() - )); - } - - // If the input is valid, index 0 contains "Dev", index 1 contains - // "Func" - let pci_parts_by_dot: Vec<_> = - pci_parts_by_colon[1].split('.').map(str::trim).collect(); - if pci_parts_by_dot.len() != 2 { - return Err(format!( - "Error: failed to parse PCI address '{}' on element '{}'", - pcidev_str, - child.tag_name().name() - )); - } - - let pci_bus_maybe = i64::from_str_radix(pci_parts_by_colon[0], 16); - let pci_dev_maybe = i64::from_str_radix(pci_parts_by_dot[0], 16); - let pci_func_maybe = i64::from_str_radix(pci_parts_by_dot[1], 16); - - match pci_bus_maybe { - Ok(pci_bus_unchecked) => { - if !(0..=PCI_BUS_MAX).contains(&pci_bus_unchecked) { - return Err(value_error( - xml_sdf, - &child, - format!("PCI bus must be within [0..{PCI_BUS_MAX}]"), - )); - } - } - Err(_) => { - return Err(format!( - "Error: failed to parse PCI bus of '{}' on element '{}'", - pcidev_str, - child.tag_name().name() - )) - } - }; - - match pci_dev_maybe { - Ok(pci_dev_unchecked) => { - if !(0..=PCI_DEV_MAX).contains(&pci_dev_unchecked) { - return Err(value_error( - xml_sdf, - &child, - format!("PCI device must be within [0..{PCI_DEV_MAX}]"), - )); - } - } - Err(_) => { - return Err(format!( - "Error: failed to parse PCI device of '{}' on element '{}'", - pcidev_str, - child.tag_name().name() - )) - } - }; - - match pci_func_maybe { - Ok(pci_func_unchecked) => { - if !(0..=PCI_FUNC_MAX).contains(&pci_func_unchecked) { - return Err(value_error( - xml_sdf, - &child, - format!("PCI function must be within [0..{PCI_FUNC_MAX}]"), - )); - } - } - Err(_) => { - return Err(format!( - "Error: failed to parse PCI function of '{}' on element '{}'", - pcidev_str, - child.tag_name().name() - )) - } - }; + let pci_device = PciDevice::from_str(pcidev_str) + .map_err(|err| value_error(xml_sdf, &child, err.to_string()))?; let handle = checked_lookup(xml_sdf, &child, "handle")? .parse::() @@ -1015,9 +1022,7 @@ impl ProtectionDomain { let irq = SysIrq { id: id as u64, kind: SysIrqKind::MSI { - pci_bus: pci_bus_maybe.unwrap() as u64, - pci_dev: pci_dev_maybe.unwrap() as u64, - pci_func: pci_func_maybe.unwrap() as u64, + pci_device, handle: handle as u64, vector: vector as u64, }, From fbbe7262444acccd159b2f79efef6290385353c0 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 18 Jun 2026 14:16:23 +1000 Subject: [PATCH 4/9] IOMMU: Add SDF Support This commit adds iommu support to microkit sdfs. Define a constant to represent the a tool enforced limitation on the maximum virtual address suported for an IO address space. This is due to current x86 IOMMU behaviour in the kernel which dynamically detects the maximum virtual address for an IO address space. For more info read: BOOT_CODE bool_t vtd_init_num_iopts(uint32_t num_drhu) in seL4/src/plat/pc99/machine/intel-vtd.c. Add IOMMUDeviceIdentifier and IOMMUDeviceIdentifierParseError to support parsing the sdf based on the current architecture. This allows the sdf parsing to easily support ARM SMMU and RISCV IOMMU. The Display traits again remove repeated code when outputting IOMMUDeviceIdentifer or IOMMUDeviceIdentifierParseError, particularly useful for error messages. Add SysIOMapPerms. Representing the perms in an enum completely removes the existence of invalid IOMapPerms once we parse the sdf. Add SysIOMap. The dual to SysMap, used to represent a mapping in a devices IO virtual address space. Add check_io_maps adapter. Required because check_maps is designed to error check within one address space. Therefore we collect all the mappings that have been made on a per IO address space basis. Signed-off-by: Callum --- .../x86_64_iommu_dma_test.system | 20 ++ tool/microkit/src/sdf.rs | 311 +++++++++++++++++- .../tests/sdf/iommu_address_overflow.system | 15 + .../tests/sdf/iommu_duplicate_device.system | 18 + .../iommu_duplicate_device_identifier.system | 18 + .../tests/sdf/iommu_out_of_bound.system | 18 + .../iommu_overlap_different_devices.system | 19 ++ .../sdf/iommu_overlap_mixed_page_sizes.system | 17 + .../sdf/iommu_overlap_same_device.system | 17 + .../tests/sdf/iommu_pci_invalid.system | 15 + .../tests/sdf/iommu_pci_negative_bus.system | 15 + .../sdf/iommu_pci_negative_device.system | 15 + .../sdf/iommu_pci_negative_function.system | 15 + .../sdf/iommu_perms_execute_invalid.system | 15 + .../tests/sdf/iommu_perms_read_write.system | 15 + .../tests/sdf/iommu_perms_write_only.system | 15 + .../tests/sdf/iommu_range_out_of_bound.system | 15 + .../iommu_same_mr_different_devices.system | 18 + .../sdf/iommu_valid_perms_and_bound.system | 15 + .../pd_overlapping_mixed_page_sizes.system | 15 + .../tests/sdf/sys_map_range_too_high.system | 13 + tool/microkit/tests/test.rs | 172 +++++++++- 22 files changed, 804 insertions(+), 2 deletions(-) create mode 100644 example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.system create mode 100644 tool/microkit/tests/sdf/iommu_address_overflow.system create mode 100644 tool/microkit/tests/sdf/iommu_duplicate_device.system create mode 100644 tool/microkit/tests/sdf/iommu_duplicate_device_identifier.system create mode 100644 tool/microkit/tests/sdf/iommu_out_of_bound.system create mode 100644 tool/microkit/tests/sdf/iommu_overlap_different_devices.system create mode 100644 tool/microkit/tests/sdf/iommu_overlap_mixed_page_sizes.system create mode 100644 tool/microkit/tests/sdf/iommu_overlap_same_device.system create mode 100644 tool/microkit/tests/sdf/iommu_pci_invalid.system create mode 100644 tool/microkit/tests/sdf/iommu_pci_negative_bus.system create mode 100644 tool/microkit/tests/sdf/iommu_pci_negative_device.system create mode 100644 tool/microkit/tests/sdf/iommu_pci_negative_function.system create mode 100644 tool/microkit/tests/sdf/iommu_perms_execute_invalid.system create mode 100644 tool/microkit/tests/sdf/iommu_perms_read_write.system create mode 100644 tool/microkit/tests/sdf/iommu_perms_write_only.system create mode 100644 tool/microkit/tests/sdf/iommu_range_out_of_bound.system create mode 100644 tool/microkit/tests/sdf/iommu_same_mr_different_devices.system create mode 100644 tool/microkit/tests/sdf/iommu_valid_perms_and_bound.system create mode 100644 tool/microkit/tests/sdf/pd_overlapping_mixed_page_sizes.system create mode 100644 tool/microkit/tests/sdf/sys_map_range_too_high.system 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 new file mode 100644 index 000000000..eb35dd81d --- /dev/null +++ b/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.system @@ -0,0 +1,20 @@ + + + + + + + + + + + + + + + + diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index d37275ff7..34e0b253e 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -62,6 +62,12 @@ 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. @@ -190,6 +196,55 @@ impl FromStr for PciDevice { }) } } + +// This can be extended in future to support devices on an SMMU enabled Arm device +// or IOMMU enabled RISC-V device. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum IommuDeviceIdentifier { + X86Pci(PciDevice), +} + +#[derive(Clone, PartialEq, Eq)] +pub enum IommuDeviceIdentifierParseError { + UnsupportedArch(Arch), + Pci(PciDeviceParseError), +} + +impl IommuDeviceIdentifier { + fn from_str_for_arch( + config: &Config, + s: &str, + ) -> Result { + match config.arch { + Arch::X86_64 => PciDevice::from_str(s) + .map(IommuDeviceIdentifier::X86Pci) + .map_err(IommuDeviceIdentifierParseError::Pci), + Arch::Aarch64 | Arch::Riscv64 => Err(IommuDeviceIdentifierParseError::UnsupportedArch( + config.arch, + )), + } + } +} + +impl fmt::Display for IommuDeviceIdentifier { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + IommuDeviceIdentifier::X86Pci(pci_device) => write!(f, "PCI device {pci_device}"), + } + } +} + +impl fmt::Display for IommuDeviceIdentifierParseError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + IommuDeviceIdentifierParseError::UnsupportedArch(arch) => { + write!(f, "IOMMU device identifiers are not supported on {arch}") + } + IommuDeviceIdentifierParseError::Pci(err) => write!(f, "{err}"), + } + } +} + #[repr(u8)] pub enum SysMapPerms { Read = 1, @@ -197,6 +252,22 @@ pub enum SysMapPerms { Execute = 4, } +impl SysMapPerms { + fn from_str(s: &str) -> Result { + let mut perms = 0; + for c in s.chars() { + match c { + 'r' => perms |= SysMapPerms::Read as u8, + 'w' => perms |= SysMapPerms::Write as u8, + 'x' => perms |= SysMapPerms::Execute as u8, + _ => return Err(()), + } + } + + Ok(perms) + } +} + #[derive(Debug, Clone, PartialEq, Eq)] pub struct SysMap { pub mr: String, @@ -208,6 +279,53 @@ pub struct SysMap { pub text_pos: Option, } +#[derive(Debug, PartialEq, Eq, Clone, Copy)] +pub enum SysIOMapPerms { + Read, + Write, + ReadWrite, +} + +impl SysIOMapPerms { + fn from_str(s: &str) -> Result { + let mut read = false; + let mut write = false; + + for c in s.chars() { + match c { + 'r' => read = true, + 'w' => write = true, + _ => return Err(()), + } + } + + match (read, write) { + (true, true) => Ok(SysIOMapPerms::ReadWrite), + (true, false) => Ok(SysIOMapPerms::Read), + (false, true) => Ok(SysIOMapPerms::Write), + (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)] +pub struct SysIOMap { + pub device: String, + pub mr: String, + pub identifier: IommuDeviceIdentifier, + pub iovaddr: u64, + pub perms: SysIOMapPerms, + pub text_pos: Option, +} + trait Map { fn mr_name(&self) -> &str; fn addr(&self) -> u64; @@ -242,6 +360,32 @@ impl Map for SysMap { "virtual address range" } } + +impl Map for SysIOMap { + fn mr_name(&self) -> &str { + &self.mr + } + + fn addr(&self) -> u64 { + self.iovaddr + } + + fn text_pos(&self) -> Option { + self.text_pos + } + + fn element(&self) -> &'static str { + "iomap" + } + + fn addr_name(&self) -> &'static str { + "iovaddr" + } + + fn range_name(&self) -> &'static str { + "io address range" + } +} #[derive(Debug, PartialEq, Eq, Clone)] pub enum SysMemoryRegionKind { User, @@ -554,6 +698,137 @@ impl SysMap { } } +impl SysIOMap { + fn from_xml( + config: &Config, + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + device: &str, + identifier: IommuDeviceIdentifier, + ) -> Result { + if config.arch != Arch::X86_64 { + return Err(value_error( + xml_sdf, + node, + "IOMMU is not yet supported on ARM and RISC-V by Microkit".to_string(), + )); + } + + let attrs = vec!["mr", "iovaddr", "perms"]; + + check_attributes(xml_sdf, node, &attrs)?; + + 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 { + return Err(value_error( + xml_sdf, + node, + format!( + "iovaddr ({iovaddr:#x}) must be less than {:#x}", + IOMAP_MAX_VADDR + 1 + ), + )); + } + + let perms = if let Some(xml_perms) = node.attribute("perms") { + match SysIOMapPerms::from_str(xml_perms) { + Ok(parsed_perms) => parsed_perms, + Err(()) => { + return Err(value_error( + xml_sdf, + node, + "perms for io mapped memory must only be a combination of 'r' and 'w'" + .to_string(), + )) + } + } + } else { + // Default to read-write + SysIOMapPerms::ReadWrite + }; + + Ok(SysIOMap { + device: device.to_string(), + mr, + identifier, + iovaddr, + perms, + text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), + }) + } +} + +// This is implemented in such a way that each device will have its own address space. +// If devices need to share physical memory, this can be done by mapping the same memory_region +// into each address space. +struct IOAddressSpace { + iomaps: Vec, +} + +impl IOAddressSpace { + fn from_xml( + config: &Config, + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + device_names: &mut HashSet, + iommu_device_identifiers: &mut HashSet, + ) -> Result { + check_attributes(xml_sdf, node, &["name", "peripheral_id"])?; + let device_name = checked_lookup(xml_sdf, node, "name")?; + if !device_names.insert(device_name.to_string()) { + return Err(value_error( + xml_sdf, + node, + format!("duplicate device name '{device_name}'"), + )); + } + + // In the SDF we use peripheral_id as an architecture agnostic way to describe + // how a device is identified in a system. For example on x86 the IOMMU identifies + // devices by the PCI tuple (bus,dev,fn) + let identifier_str = checked_lookup(xml_sdf, node, "peripheral_id")?; + let identifier = + IommuDeviceIdentifier::from_str_for_arch(config, identifier_str).map_err(|err| { + value_error( + xml_sdf, + node, + format!("failed to parse device peripheral_id '{identifier_str}': {err}"), + ) + })?; + if !iommu_device_identifiers.insert(identifier) { + return Err(value_error( + xml_sdf, + node, + format!("duplicate device peripheral_id '{identifier}'"), + )); + } + + let mut iomaps = Vec::new(); + + for child in node.children().filter(|node| node.is_element()) { + match child.tag_name().name() { + "iomap" => { + let iomap = + SysIOMap::from_xml(config, xml_sdf, &child, device_name, identifier)?; + iomaps.push(iomap); + } + _ => { + let pos = xml_sdf.doc.text_pos_at(child.range().start); + return Err(format!( + "Error: invalid XML element '{}': {}", + child.tag_name().name(), + loc_string(xml_sdf, pos) + )); + } + } + } + + Ok(IOAddressSpace { iomaps }) + } +} + impl ProtectionDomain { pub fn needs_ep(&self, self_id: usize, channels: &[Channel]) -> bool { self.has_children @@ -1752,6 +2027,7 @@ struct XmlSystemDescription<'a> { pub struct SystemDescription { pub protection_domains: Vec, pub memory_regions: Vec, + pub iomaps: Vec, pub channels: Vec, } @@ -1842,6 +2118,21 @@ where Ok(()) } + +fn check_io_maps( + xml_sdf: &XmlSystemDescription, + mrs: &[SysMemoryRegion], + iomaps: &[SysIOMap], +) -> Result<(), String> { + let mut by_device: HashMap> = HashMap::new(); + + for iomap in iomaps { + by_device.entry(iomap.identifier).or_default().push(iomap); + } + + for (identifier, maps) in by_device { + let address_space = identifier.to_string(); + check_maps(xml_sdf, mrs, maps, &address_space, IOMAP_MAX_VADDR + 1)?; } Ok(()) @@ -2023,6 +2314,9 @@ pub fn parse( let mut root_pds = vec![]; let mut mrs = vec![]; + let mut iomaps = vec![]; + let mut device_names = HashSet::new(); + let mut iommu_device_identifiers = HashSet::new(); let mut channels = vec![]; let system = doc .root() @@ -2055,6 +2349,18 @@ pub fn parse( &child, search_paths, )?), + "io_address_space" => { + iomaps.extend( + IOAddressSpace::from_xml( + config, + &xml_sdf, + &child, + &mut device_names, + &mut iommu_device_identifiers, + )? + .iomaps, + ); + } "virtual_machine" => { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!( @@ -2176,7 +2482,7 @@ pub fn parse( // expose this footgun to users. return Err(format!( "Error: It is not possible for PD '{}' with a bound vCPU to have children on x86_64: {}", - pd.name(), + pd.name, loc_string(&xml_sdf, pd.text_pos.unwrap()))); } } @@ -2348,6 +2654,8 @@ pub fn parse( } } + check_io_maps(&xml_sdf, &mrs, &iomaps)?; + // Ensure that there are no overlapping extra cap maps in the user caps region // and we are not mapping in the same cap from the same source more than once for pd in &pds { @@ -2525,6 +2833,7 @@ pub fn parse( Ok(SystemDescription { protection_domains: pds, memory_regions: mrs, + iomaps, channels, }) } diff --git a/tool/microkit/tests/sdf/iommu_address_overflow.system b/tool/microkit/tests/sdf/iommu_address_overflow.system new file mode 100644 index 000000000..b6f06e890 --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_address_overflow.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_duplicate_device.system b/tool/microkit/tests/sdf/iommu_duplicate_device.system new file mode 100644 index 000000000..7641c3d01 --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_duplicate_device.system @@ -0,0 +1,18 @@ + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_duplicate_device_identifier.system b/tool/microkit/tests/sdf/iommu_duplicate_device_identifier.system new file mode 100644 index 000000000..5c0f09efc --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_duplicate_device_identifier.system @@ -0,0 +1,18 @@ + + + + + + + + + + + + + + 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..e57382d9d --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_out_of_bound.system @@ -0,0 +1,18 @@ + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_overlap_different_devices.system b/tool/microkit/tests/sdf/iommu_overlap_different_devices.system new file mode 100644 index 000000000..ec267eebf --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_overlap_different_devices.system @@ -0,0 +1,19 @@ + + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_overlap_mixed_page_sizes.system b/tool/microkit/tests/sdf/iommu_overlap_mixed_page_sizes.system new file mode 100644 index 000000000..cb62e8a06 --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_overlap_mixed_page_sizes.system @@ -0,0 +1,17 @@ + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_overlap_same_device.system b/tool/microkit/tests/sdf/iommu_overlap_same_device.system new file mode 100644 index 000000000..007be877c --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_overlap_same_device.system @@ -0,0 +1,17 @@ + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_pci_invalid.system b/tool/microkit/tests/sdf/iommu_pci_invalid.system new file mode 100644 index 000000000..fcd8e7885 --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_pci_invalid.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_pci_negative_bus.system b/tool/microkit/tests/sdf/iommu_pci_negative_bus.system new file mode 100644 index 000000000..f496e8b6c --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_pci_negative_bus.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_pci_negative_device.system b/tool/microkit/tests/sdf/iommu_pci_negative_device.system new file mode 100644 index 000000000..ff1366d20 --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_pci_negative_device.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_pci_negative_function.system b/tool/microkit/tests/sdf/iommu_pci_negative_function.system new file mode 100644 index 000000000..1324c3f8b --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_pci_negative_function.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_perms_execute_invalid.system b/tool/microkit/tests/sdf/iommu_perms_execute_invalid.system new file mode 100644 index 000000000..bffff94be --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_perms_execute_invalid.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_perms_read_write.system b/tool/microkit/tests/sdf/iommu_perms_read_write.system new file mode 100644 index 000000000..af489480d --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_perms_read_write.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_perms_write_only.system b/tool/microkit/tests/sdf/iommu_perms_write_only.system new file mode 100644 index 000000000..a2706700b --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_perms_write_only.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_range_out_of_bound.system b/tool/microkit/tests/sdf/iommu_range_out_of_bound.system new file mode 100644 index 000000000..d99627331 --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_range_out_of_bound.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_same_mr_different_devices.system b/tool/microkit/tests/sdf/iommu_same_mr_different_devices.system new file mode 100644 index 000000000..c31be4d1c --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_same_mr_different_devices.system @@ -0,0 +1,18 @@ + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_valid_perms_and_bound.system b/tool/microkit/tests/sdf/iommu_valid_perms_and_bound.system new file mode 100644 index 000000000..e7fd642e5 --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_valid_perms_and_bound.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_overlapping_mixed_page_sizes.system b/tool/microkit/tests/sdf/pd_overlapping_mixed_page_sizes.system new file mode 100644 index 000000000..2a604bb10 --- /dev/null +++ b/tool/microkit/tests/sdf/pd_overlapping_mixed_page_sizes.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/sys_map_range_too_high.system b/tool/microkit/tests/sdf/sys_map_range_too_high.system new file mode 100644 index 000000000..2dbffe5ea --- /dev/null +++ b/tool/microkit/tests/sdf/sys_map_range_too_high.system @@ -0,0 +1,13 @@ + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 3328d23d9..40b2081e6 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -641,7 +641,7 @@ mod protection_domain { check_error( &DEFAULT_X86_64_KERNEL_CONFIG, "irq_msi_pci_invalid.system", - "Error: failed to parse PCI address '0:0:0' on element 'irq'", + "Error: expected PCI address in bus:device.function form on element 'irq'", ) } @@ -712,6 +712,14 @@ mod protection_domain { ) } + #[test] + fn test_overlapping_mixed_page_size_maps() { + check_error(&DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_overlapping_mixed_page_sizes.system", + "Error: map for 'small_region' has virtual address range [0x201000..0x202000) which overlaps with map for 'large_region' [0x200000..0x400000) in protection domain 'test' @" + ) + } + #[test] fn test_overlapping_x86_io_ports_1() { check_error(&DEFAULT_X86_64_KERNEL_CONFIG, @@ -747,6 +755,159 @@ mod protection_domain { } } +#[cfg(test)] +mod iommu { + use super::*; + + #[test] + fn test_out_of_bound() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_out_of_bound.system", + "Error: iovaddr (0x8000000000) must be less than 0x8000000000 on element 'iomap': iommu_out_of_bound.system:10:9", + ) + } + + #[test] + fn test_range_out_of_bound() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_range_out_of_bound.system", + "Error: iomap for 'region' has io address range [0x7fff800000..0x8000200000) which exceeds valid address space [0x0..0x8000000000) @", + ) + } + + #[test] + fn test_address_overflow() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_address_overflow.system", + "Error: iomap for 'region' has address range that overflows @", + ) + } + + #[test] + fn test_valid_perms_and_bound() { + check_success( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_valid_perms_and_bound.system", + ) + } + + #[test] + fn test_perms_read_write() { + check_success( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_perms_read_write.system", + ) + } + + #[test] + fn test_perms_write_only() { + check_success( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_perms_write_only.system", + ) + } + + #[test] + fn test_perms_execute_invalid() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_perms_execute_invalid.system", + "Error: perms for io mapped memory must only be a combination of 'r' and 'w' on element 'iomap':", + ) + } + + #[test] + fn test_overlap_different_devices() { + check_success( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_overlap_different_devices.system", + ) + } + + #[test] + fn test_overlap_same_device() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_overlap_same_device.system", + "Error: map for 'region_b' has io address range [0x0..0x1000) which overlaps with map for 'region_a' [0x0..0x1000) in PCI device 00:03.0 @ iommu_overlap_same_device.system:12:9", + ) + } + + #[test] + fn test_same_mr_different_devices() { + check_success( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_same_mr_different_devices.system", + ) + } + + #[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 @", + ) + } + + #[test] + fn test_pci_invalid() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_pci_invalid.system", + "Error: failed to parse device peripheral_id '0:g.0': failed to parse PCI device on element 'io_address_space': iommu_pci_invalid.system:9:5", + ) + } + + #[test] + fn test_pci_negative_bus() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_pci_negative_bus.system", + "Error: failed to parse device peripheral_id '-1:0.0': PCI bus must be within [0..255] on element 'io_address_space':", + ) + } + + #[test] + fn test_pci_negative_device() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_pci_negative_device.system", + "Error: failed to parse device peripheral_id '0:-1.0': PCI device must be within [0..31] on element 'io_address_space':", + ) + } + + #[test] + fn test_pci_negative_function() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_pci_negative_function.system", + "Error: failed to parse device peripheral_id '0:0.-1': PCI function must be within [0..7] on element 'io_address_space':", + ) + } + + #[test] + fn test_duplicate_device() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_duplicate_device.system", + "Error: duplicate device name 'test_device' on element 'io_address_space':", + ) + } + + #[test] + fn test_duplicate_device_identifier() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_duplicate_device_identifier.system", + "Error: duplicate device peripheral_id 'PCI device 00:03.0' on element 'io_address_space':", + ) + } +} + #[cfg(test)] mod virtual_machine { use super::*; @@ -1063,6 +1224,15 @@ mod system { ) } + #[test] + fn test_map_range_too_high() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "sys_map_range_too_high.system", + "Error: map for 'foo' has virtual address range [0xffffffe000..0x10000000000) which exceeds valid address space [0x0..0xfffffff000) @", + ) + } + #[test] fn test_too_many_pds() { check_error( From 9a89a504c1a1599a901e683b2049b6188ca1f422 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 18 Jun 2026 14:58:34 +1000 Subject: [PATCH 5/9] IOMMU: Update manual Update the manual to include IOMMU information. Signed-off-by: Callum --- docs/manual.md | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/docs/manual.md b/docs/manual.md index 3bfef7a26..a66661b34 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -109,6 +109,7 @@ This document attempts to clearly describe all of these terms, however as the co * [interrupt](#irq) * [fault](#fault) * [ioport](#ioport) +* [io address space](#io_address_space) ## System {#system} @@ -242,6 +243,13 @@ The mapping has a number of attributes, which include: * caching attributes (mostly relevant for device memory) * permissions (read, write and execute) +*Note:* On x86 a memory region can also be *mapped* into one or more +io address spaces. This type of mapping is known as an *iomap*. It supports +a number of attributes, which include: + +* the io virtual address at which the region is mapped in the io address space +* permissions (read, write) + **Note:** When a memory region is mapped into multiple protection domains, the attributes used for different mappings may vary. @@ -367,6 +375,12 @@ delivered to another PD, the fault being handled depends on when the parent PD i I/O ports are x86 mechanisms to access certain physical devices (e.g. PC serial ports or PCI) using the `in` and `out` CPU instructions. The system description specifies if a protection domain have access to certain port address ranges. These accesses will be executed by seL4 and the result returned to protection domains. +## IO Address Spaces {#io_address_space} + +IO Address Spaces provide a way to isolate device memory accesses within a fixed virtual address space. The isolation provided by the address space is enforced by the underlying hardware IOMMU or SMMU. + +IO Address Spaces allow *memory regions* to be mapped to a provided base IO virtual address. These IO virtual addresses will be translated by the hardware IOMMU or SMMU to the underlying physical memory that backs the memory region. + # SDK {#sdk} Microkit is distributed as a software development kit (SDK). @@ -1074,6 +1088,23 @@ See the 'cap_sharing' example packaged in your SDK or [on GitHub](https://github All capability elements (currently) all support the `pd` attribute, the name of the protection domain that the capability is from. For instance, `` will place the TCB of PD 'alpha' in the CSpace of the current PD. +## `io_address_space` + +The `io_address_space` element describes an address space used to isolate a given device. + +It supports the following attributes: +* `name`: A unique name for the io address space +* `peripheral_id`: A unique identifier. This must match the identifier used by the hardware IOMMU or SMMU to identify devices. + +The `io_address_space` element supports the following elements as children: + +* `iomap`: This is used to map a *memory_region* into the io address space. + +The `iomap` element supports the following attributes: +* `mr`: Identifies the memory region to map. +* `iovaddr`: Identifies the io virtual address at which to map the memory region. +* `perms`: Identifies the permissions with which to map the memory region. Can be a combination of `r` (read), and `w` (write). + Defaults to read-write. ### Page sizes by architecture From 756674818b51618f91a660e1cc92ba7e8bfc1472 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 18 Jun 2026 15:57:39 +1000 Subject: [PATCH 6/9] IOMMU: Validate IOMMU Kernel Support Ensure that the sel4::Config struct has the iommu flag asserted, indicating the kernel was built with IOMMU support. If not we fail parsing any io address space elements encountered in the sdf. Signed-off-by: Callum --- tool/microkit/src/main.rs | 6 ++ tool/microkit/src/sdf.rs | 18 +++--- tool/microkit/src/sel4.rs | 1 + .../sdf/iommu_missing_from_config.system | 18 ++++++ tool/microkit/tests/test.rs | 64 +++++++++++++++++++ 5 files changed, 98 insertions(+), 9 deletions(-) create mode 100644 tool/microkit/tests/sdf/iommu_missing_from_config.system diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index 909b39463..ec83dff1d 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -227,6 +227,11 @@ fn main() -> Result<(), String> { _ => false, }; + 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")? { @@ -265,6 +270,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/sdf.rs b/tool/microkit/src/sdf.rs index 34e0b253e..b59783ade 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -700,20 +700,12 @@ impl SysMap { impl SysIOMap { fn from_xml( - config: &Config, + _config: &Config, xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, device: &str, identifier: IommuDeviceIdentifier, ) -> Result { - if config.arch != Arch::X86_64 { - return Err(value_error( - xml_sdf, - node, - "IOMMU is not yet supported on ARM and RISC-V by Microkit".to_string(), - )); - } - let attrs = vec!["mr", "iovaddr", "perms"]; check_attributes(xml_sdf, node, &attrs)?; @@ -775,6 +767,14 @@ impl IOAddressSpace { device_names: &mut HashSet, iommu_device_identifiers: &mut HashSet, ) -> Result { + let pos = xml_sdf.doc.text_pos_at(node.range().start); + if !config.iommu { + return Err(format!( + "Error: io address space requires seL4 to be built with IOMMU support: {}", + loc_string(xml_sdf, pos) + )); + } + check_attributes(xml_sdf, node, &["name", "peripheral_id"])?; let device_name = checked_lookup(xml_sdf, node, "name")?; if !device_names.insert(device_name.to_string()) { diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index e23084848..2868c2871 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -303,6 +303,7 @@ pub struct Config { pub cap_address_bits: u64, pub fan_out_limit: u64, pub max_num_bootinfo_untypeds: u64, + pub iommu: bool, pub hypervisor: bool, pub benchmark: bool, pub num_cores: u8, diff --git a/tool/microkit/tests/sdf/iommu_missing_from_config.system b/tool/microkit/tests/sdf/iommu_missing_from_config.system new file mode 100644 index 000000000..e57382d9d --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_missing_from_config.system @@ -0,0 +1,18 @@ + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 40b2081e6..e5fd82a52 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -36,6 +36,7 @@ const DEFAULT_AARCH64_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, @@ -66,6 +67,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, @@ -759,6 +761,68 @@ mod protection_domain { mod iommu { use super::*; + #[test] + fn test_iommu_missing_from_config() { + check_error( + &sel4::Config { + iommu: false, + ..DEFAULT_X86_64_KERNEL_CONFIG + }, + "iommu_missing_from_config.system", + "Error: io address space requires seL4 to be built with IOMMU support: ", + ); + } + + #[test] + fn test_iommu_missing_from_aarch64_config() { + check_error( + &sel4::Config { + iommu: false, + ..DEFAULT_AARCH64_KERNEL_CONFIG + }, + "iommu_missing_from_config.system", + "Error: io address space requires seL4 to be built with IOMMU support: ", + ); + } + + #[test] + fn test_iommu_missing_from_riscv64_config() { + check_error( + &sel4::Config { + arch: sel4::Arch::Riscv64, + iommu: false, + ..DEFAULT_AARCH64_KERNEL_CONFIG + }, + "iommu_missing_from_config.system", + "Error: io address space requires seL4 to be built with IOMMU support: ", + ); + } + + #[test] + fn test_iommu_unsupported_on_aarch64() { + check_error( + &sel4::Config { + iommu: true, + ..DEFAULT_AARCH64_KERNEL_CONFIG + }, + "iommu_missing_from_config.system", + "Error: failed to parse device peripheral_id '0:3.0': IOMMU device identifiers are not supported on AArch64 on element 'io_address_space':", + ); + } + + #[test] + fn test_iommu_unsupported_on_riscv64() { + check_error( + &sel4::Config { + arch: sel4::Arch::Riscv64, + iommu: true, + ..DEFAULT_AARCH64_KERNEL_CONFIG + }, + "iommu_missing_from_config.system", + "Error: failed to parse device peripheral_id '0:3.0': IOMMU device identifiers are not supported on RISC-V (64-bit) on element 'io_address_space':", + ); + } + #[test] fn test_out_of_bound() { check_error( From 2be5b9955c316845ff7268bb6bc3ed13a4487861 Mon Sep 17 00:00:00 2001 From: Callum Date: Tue, 7 Jul 2026 10:48:53 +1000 Subject: [PATCH 7/9] IOMMU: Capitalise io in manual Address Feedback from Bill. Signed-off-by: Callum --- docs/manual.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index a66661b34..4fa29d161 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -109,7 +109,7 @@ This document attempts to clearly describe all of these terms, however as the co * [interrupt](#irq) * [fault](#fault) * [ioport](#ioport) -* [io address space](#io_address_space) +* [IO address space](#io_address_space) ## System {#system} @@ -244,10 +244,10 @@ The mapping has a number of attributes, which include: * permissions (read, write and execute) *Note:* On x86 a memory region can also be *mapped* into one or more -io address spaces. This type of mapping is known as an *iomap*. It supports +IO address spaces. This type of mapping is known as an *iomap*. It supports a number of attributes, which include: -* the io virtual address at which the region is mapped in the io address space +* the io virtual address at which the region is mapped in the IO address space * permissions (read, write) **Note:** When a memory region is mapped into multiple protection @@ -1093,12 +1093,12 @@ For instance, `` will place the TCB of PD 'alpha' i The `io_address_space` element describes an address space used to isolate a given device. It supports the following attributes: -* `name`: A unique name for the io address space +* `name`: A unique name for the IO address space * `peripheral_id`: A unique identifier. This must match the identifier used by the hardware IOMMU or SMMU to identify devices. The `io_address_space` element supports the following elements as children: -* `iomap`: This is used to map a *memory_region* into the io address space. +* `iomap`: This is used to map a *memory_region* into the IO address space. The `iomap` element supports the following attributes: * `mr`: Identifies the memory region to map. From 52a45cb66db85baf5a75099407e9b3c7a3701b2f Mon Sep 17 00:00:00 2001 From: Callum Date: Tue, 7 Jul 2026 11:34:44 +1000 Subject: [PATCH 8/9] IOMMU: Fix an SDF parsing test Fix a test that was assuming a fixed max virtual address. Instead make the memory region large enough that it will be out of bounds on any realistic max virtual address reported by seL4 via user_top(). Signed-off-by: Callum --- tool/microkit/tests/sdf/sys_map_range_too_high.system | 4 ++-- tool/microkit/tests/test.rs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tool/microkit/tests/sdf/sys_map_range_too_high.system b/tool/microkit/tests/sdf/sys_map_range_too_high.system index 2dbffe5ea..1be99095e 100644 --- a/tool/microkit/tests/sdf/sys_map_range_too_high.system +++ b/tool/microkit/tests/sdf/sys_map_range_too_high.system @@ -5,9 +5,9 @@ SPDX-License-Identifier: BSD-2-Clause --> - + - + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index e5fd82a52..aa1377f20 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -1293,7 +1293,7 @@ mod system { check_error( &DEFAULT_AARCH64_KERNEL_CONFIG, "sys_map_range_too_high.system", - "Error: map for 'foo' has virtual address range [0xffffffe000..0x10000000000) which exceeds valid address space [0x0..0xfffffff000) @", + "Error: map for 'foo' has virtual address range [0xe000000000..0x200e000000000) which exceeds valid address space", ) } From ad35214d738c826b88ac775f6c4005400cc39a20 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 9 Jul 2026 17:49:49 +1000 Subject: [PATCH 9/9] IOMMU: Support domain ids Add domain ids to microkit system descriptions. Signed-off-by: Callum --- docs/manual.md | 4 ++ tool/microkit/src/sdf.rs | 39 +++++++++++++++++-- .../tests/sdf/iommu_address_overflow.system | 2 +- .../tests/sdf/iommu_duplicate_device.system | 4 +- .../iommu_duplicate_device_identifier.system | 4 +- .../iommu_duplicate_domain_identifier.system | 18 +++++++++ .../sdf/iommu_missing_from_config.system | 2 +- .../tests/sdf/iommu_out_of_bound.system | 2 +- .../iommu_overlap_different_devices.system | 4 +- .../sdf/iommu_overlap_mixed_page_sizes.system | 2 +- .../sdf/iommu_overlap_same_device.system | 2 +- .../tests/sdf/iommu_pci_invalid.system | 2 +- .../tests/sdf/iommu_pci_negative_bus.system | 2 +- .../sdf/iommu_pci_negative_device.system | 2 +- .../sdf/iommu_pci_negative_function.system | 2 +- .../sdf/iommu_perms_execute_invalid.system | 2 +- .../tests/sdf/iommu_perms_read_write.system | 2 +- .../tests/sdf/iommu_perms_write_only.system | 2 +- .../tests/sdf/iommu_range_out_of_bound.system | 2 +- .../iommu_same_mr_different_devices.system | 4 +- .../sdf/iommu_valid_perms_and_bound.system | 2 +- tool/microkit/tests/test.rs | 9 +++++ 22 files changed, 89 insertions(+), 25 deletions(-) create mode 100644 tool/microkit/tests/sdf/iommu_duplicate_domain_identifier.system diff --git a/docs/manual.md b/docs/manual.md index 4fa29d161..0dd0e9693 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -1093,14 +1093,18 @@ For instance, `` will place the TCB of PD 'alpha' i The `io_address_space` element describes an address space used to isolate a given device. It supports the following attributes: + * `name`: A unique name for the IO address space * `peripheral_id`: A unique identifier. This must match the identifier used by the hardware IOMMU or SMMU to identify devices. +* `domain_id`: A unique domain identifier, synonymous with an ASID. This is not optional due to current + constraints with x86 only providing certain information at runtime. The `io_address_space` element supports the following elements as children: * `iomap`: This is used to map a *memory_region* into the IO address space. The `iomap` element supports the following attributes: + * `mr`: Identifies the memory region to map. * `iovaddr`: Identifies the io virtual address at which to map the memory region. * `perms`: Identifies the permissions with which to map the memory region. Can be a combination of `r` (read), and `w` (write). diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index b59783ade..c948abf7f 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -321,6 +321,7 @@ pub struct SysIOMap { pub device: String, pub mr: String, pub identifier: IommuDeviceIdentifier, + pub domain_id: Option, pub iovaddr: u64, pub perms: SysIOMapPerms, pub text_pos: Option, @@ -705,6 +706,7 @@ impl SysIOMap { node: &roxmltree::Node, device: &str, identifier: IommuDeviceIdentifier, + domain_id: Option, ) -> Result { let attrs = vec!["mr", "iovaddr", "perms"]; @@ -745,6 +747,7 @@ impl SysIOMap { device: device.to_string(), mr, identifier, + domain_id, iovaddr, perms, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), @@ -765,6 +768,7 @@ impl IOAddressSpace { xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, device_names: &mut HashSet, + domain_ids: &mut HashSet, iommu_device_identifiers: &mut HashSet, ) -> Result { let pos = xml_sdf.doc.text_pos_at(node.range().start); @@ -775,7 +779,7 @@ impl IOAddressSpace { )); } - check_attributes(xml_sdf, node, &["name", "peripheral_id"])?; + check_attributes(xml_sdf, node, &["name", "peripheral_id", "domain_id"])?; let device_name = checked_lookup(xml_sdf, node, "name")?; if !device_names.insert(device_name.to_string()) { return Err(value_error( @@ -785,6 +789,27 @@ impl IOAddressSpace { )); } + // Currently we enforce unqiue domain ids. To support shared domain ids, we have to ensure + // each device has a duplicated copy of the whole page table structure due to how Intel + // implements IOMMU caching see section 6.2.1 in the Virtualization Technology (Intel® VT) for Directed I/O + // (Intel® VT-d) manual: + // http://www.intel.com/content/dam/www/public/us/en/documents/product-specifications/vt-directed-io-spec.pdf + let domain_id = match config.arch { + Arch::X86_64 => { + let domain_id = + sdf_parse_number(checked_lookup(xml_sdf, node, "domain_id")?, node)?; + if !domain_ids.insert(domain_id) { + return Err(value_error( + xml_sdf, + node, + "reusing a domain id is forbidden".into(), + )); + } + Some(domain_id) + } + _ => None, + }; + // In the SDF we use peripheral_id as an architecture agnostic way to describe // how a device is identified in a system. For example on x86 the IOMMU identifies // devices by the PCI tuple (bus,dev,fn) @@ -810,8 +835,14 @@ impl IOAddressSpace { for child in node.children().filter(|node| node.is_element()) { match child.tag_name().name() { "iomap" => { - let iomap = - SysIOMap::from_xml(config, xml_sdf, &child, device_name, identifier)?; + let iomap = SysIOMap::from_xml( + config, + xml_sdf, + &child, + device_name, + identifier, + domain_id, + )?; iomaps.push(iomap); } _ => { @@ -2316,6 +2347,7 @@ pub fn parse( let mut mrs = vec![]; let mut iomaps = vec![]; let mut device_names = HashSet::new(); + let mut domain_ids = HashSet::new(); let mut iommu_device_identifiers = HashSet::new(); let mut channels = vec![]; let system = doc @@ -2356,6 +2388,7 @@ pub fn parse( &xml_sdf, &child, &mut device_names, + &mut domain_ids, &mut iommu_device_identifiers, )? .iomaps, diff --git a/tool/microkit/tests/sdf/iommu_address_overflow.system b/tool/microkit/tests/sdf/iommu_address_overflow.system index b6f06e890..b9766dc79 100644 --- a/tool/microkit/tests/sdf/iommu_address_overflow.system +++ b/tool/microkit/tests/sdf/iommu_address_overflow.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_duplicate_device.system b/tool/microkit/tests/sdf/iommu_duplicate_device.system index 7641c3d01..4b4b84058 100644 --- a/tool/microkit/tests/sdf/iommu_duplicate_device.system +++ b/tool/microkit/tests/sdf/iommu_duplicate_device.system @@ -6,10 +6,10 @@ --> - + - + diff --git a/tool/microkit/tests/sdf/iommu_duplicate_device_identifier.system b/tool/microkit/tests/sdf/iommu_duplicate_device_identifier.system index 5c0f09efc..1d75c4d8e 100644 --- a/tool/microkit/tests/sdf/iommu_duplicate_device_identifier.system +++ b/tool/microkit/tests/sdf/iommu_duplicate_device_identifier.system @@ -6,10 +6,10 @@ --> - + - + diff --git a/tool/microkit/tests/sdf/iommu_duplicate_domain_identifier.system b/tool/microkit/tests/sdf/iommu_duplicate_domain_identifier.system new file mode 100644 index 000000000..fff94b753 --- /dev/null +++ b/tool/microkit/tests/sdf/iommu_duplicate_domain_identifier.system @@ -0,0 +1,18 @@ + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/iommu_missing_from_config.system b/tool/microkit/tests/sdf/iommu_missing_from_config.system index e57382d9d..e71224190 100644 --- a/tool/microkit/tests/sdf/iommu_missing_from_config.system +++ b/tool/microkit/tests/sdf/iommu_missing_from_config.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_out_of_bound.system b/tool/microkit/tests/sdf/iommu_out_of_bound.system index e57382d9d..e71224190 100644 --- a/tool/microkit/tests/sdf/iommu_out_of_bound.system +++ b/tool/microkit/tests/sdf/iommu_out_of_bound.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_overlap_different_devices.system b/tool/microkit/tests/sdf/iommu_overlap_different_devices.system index ec267eebf..5272ea36f 100644 --- a/tool/microkit/tests/sdf/iommu_overlap_different_devices.system +++ b/tool/microkit/tests/sdf/iommu_overlap_different_devices.system @@ -7,10 +7,10 @@ - + - + diff --git a/tool/microkit/tests/sdf/iommu_overlap_mixed_page_sizes.system b/tool/microkit/tests/sdf/iommu_overlap_mixed_page_sizes.system index cb62e8a06..69f70457d 100644 --- a/tool/microkit/tests/sdf/iommu_overlap_mixed_page_sizes.system +++ b/tool/microkit/tests/sdf/iommu_overlap_mixed_page_sizes.system @@ -7,7 +7,7 @@ - + diff --git a/tool/microkit/tests/sdf/iommu_overlap_same_device.system b/tool/microkit/tests/sdf/iommu_overlap_same_device.system index 007be877c..cae80eabb 100644 --- a/tool/microkit/tests/sdf/iommu_overlap_same_device.system +++ b/tool/microkit/tests/sdf/iommu_overlap_same_device.system @@ -7,7 +7,7 @@ - + diff --git a/tool/microkit/tests/sdf/iommu_pci_invalid.system b/tool/microkit/tests/sdf/iommu_pci_invalid.system index fcd8e7885..2fe62ca25 100644 --- a/tool/microkit/tests/sdf/iommu_pci_invalid.system +++ b/tool/microkit/tests/sdf/iommu_pci_invalid.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_pci_negative_bus.system b/tool/microkit/tests/sdf/iommu_pci_negative_bus.system index f496e8b6c..bfcd90377 100644 --- a/tool/microkit/tests/sdf/iommu_pci_negative_bus.system +++ b/tool/microkit/tests/sdf/iommu_pci_negative_bus.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_pci_negative_device.system b/tool/microkit/tests/sdf/iommu_pci_negative_device.system index ff1366d20..fde0ef76c 100644 --- a/tool/microkit/tests/sdf/iommu_pci_negative_device.system +++ b/tool/microkit/tests/sdf/iommu_pci_negative_device.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_pci_negative_function.system b/tool/microkit/tests/sdf/iommu_pci_negative_function.system index 1324c3f8b..d06d9e4d5 100644 --- a/tool/microkit/tests/sdf/iommu_pci_negative_function.system +++ b/tool/microkit/tests/sdf/iommu_pci_negative_function.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_perms_execute_invalid.system b/tool/microkit/tests/sdf/iommu_perms_execute_invalid.system index bffff94be..4a52c75cd 100644 --- a/tool/microkit/tests/sdf/iommu_perms_execute_invalid.system +++ b/tool/microkit/tests/sdf/iommu_perms_execute_invalid.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_perms_read_write.system b/tool/microkit/tests/sdf/iommu_perms_read_write.system index af489480d..169f3fab9 100644 --- a/tool/microkit/tests/sdf/iommu_perms_read_write.system +++ b/tool/microkit/tests/sdf/iommu_perms_read_write.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_perms_write_only.system b/tool/microkit/tests/sdf/iommu_perms_write_only.system index a2706700b..9adcd0af3 100644 --- a/tool/microkit/tests/sdf/iommu_perms_write_only.system +++ b/tool/microkit/tests/sdf/iommu_perms_write_only.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_range_out_of_bound.system b/tool/microkit/tests/sdf/iommu_range_out_of_bound.system index d99627331..b7df4bfc1 100644 --- a/tool/microkit/tests/sdf/iommu_range_out_of_bound.system +++ b/tool/microkit/tests/sdf/iommu_range_out_of_bound.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/sdf/iommu_same_mr_different_devices.system b/tool/microkit/tests/sdf/iommu_same_mr_different_devices.system index c31be4d1c..ec578c484 100644 --- a/tool/microkit/tests/sdf/iommu_same_mr_different_devices.system +++ b/tool/microkit/tests/sdf/iommu_same_mr_different_devices.system @@ -6,10 +6,10 @@ --> - + - + diff --git a/tool/microkit/tests/sdf/iommu_valid_perms_and_bound.system b/tool/microkit/tests/sdf/iommu_valid_perms_and_bound.system index e7fd642e5..e38a582f6 100644 --- a/tool/microkit/tests/sdf/iommu_valid_perms_and_bound.system +++ b/tool/microkit/tests/sdf/iommu_valid_perms_and_bound.system @@ -6,7 +6,7 @@ --> - + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index aa1377f20..642c3fa2d 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -970,6 +970,15 @@ mod iommu { "Error: duplicate device peripheral_id 'PCI device 00:03.0' on element 'io_address_space':", ) } + + #[test] + fn test_duplicate_domain_identifier() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "iommu_duplicate_domain_identifier.system", + "Error: reusing a domain id is forbidden on element 'io_address_space'", + ); + } } #[cfg(test)]