From d13bf6b3197af364054b664e065916dd79c2072d Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 9 Jul 2026 17:49:49 +1000 Subject: [PATCH 1/4] IOMMU: Support domain ids Add domain ids to microkit system descriptions. Signed-off-by: Callum --- docs/manual.md | 4 ++ tool/microkit/src/sdf.rs | 43 +++++++++++++++++-- .../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, 93 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..f349b4561 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,31 @@ impl IOAddressSpace { )); } + // In microkit enforcing uniqueness for domain ids is hugely simplifying and enforces better designs. + // If we were to allow shared domain ids, we would have to ensure that whenever two devices share a domain + // that they do not have any IOVA to physyical address mappings that conflict, and that they share the same + // IOPT objects, this because the source identifier aka the PCI BDF is not used in all caches. + // See section 6.2.1 and table 17 in the intel VT-D manual. + // https://www.google.com/url?sa=t&source=web&rct=j&opi=89978449&url=https://cdrdv2-public.intel.com/671081/vt-directed-io-spec.pdf&ved=2ahUKEwiN_YawksWVAxUDmFYBHfzzCEQQFnoECA0QAQ&usg=AOvVaw3fO9wnba58SqsP2HNKwdfu + // We make the user specify this information though since at runtime the selected domain_ids might be + // reserved by seL4 during its boot and therefore unavailable. This forces the user of microkit to select a new + // domain id. + 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 +839,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 +2351,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 +2392,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)] From c35471b010b75a821220c1cc774686aa5cf1623c Mon Sep 17 00:00:00 2001 From: Callum Date: Mon, 6 Jul 2026 21:21:41 +1000 Subject: [PATCH 2/4] IOMMU: Minor modification to Map trait Minor adjustments to the prior sdf work to do with how permissions are handled. Previously I implemented read and write functions as part of the SysIOMapPerms enum, however the old SysMapPerms did not do this. Given these types are meant to exhibit similar behaviour extracting this common logic into the Map trait provides a streamlined interface to check if a permission is set. Signed-off-by: Callum --- tool/microkit/src/sdf.rs | 47 ++++++++++++++++++++++++++++++++-------- 1 file changed, 38 insertions(+), 9 deletions(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index f349b4561..90af397ba 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -306,14 +306,6 @@ impl SysIOMapPerms { (false, false) => Err(()), } } - - pub fn read(self) -> bool { - matches!(self, SysIOMapPerms::Read | SysIOMapPerms::ReadWrite) - } - - pub fn write(self) -> bool { - matches!(self, SysIOMapPerms::Write | SysIOMapPerms::ReadWrite) - } } #[derive(Debug, PartialEq, Eq, Clone)] @@ -327,13 +319,17 @@ pub struct SysIOMap { pub text_pos: Option, } -trait Map { +pub trait Map { fn mr_name(&self) -> &str; fn addr(&self) -> u64; fn text_pos(&self) -> Option; fn element(&self) -> &'static str; fn addr_name(&self) -> &'static str; fn range_name(&self) -> &'static str; + fn read(&self) -> bool; + fn write(&self) -> bool; + fn execute(&self) -> bool; + fn cached(&self) -> bool; } impl Map for SysMap { @@ -360,6 +356,22 @@ impl Map for SysMap { fn range_name(&self) -> &'static str { "virtual address range" } + + fn read(&self) -> bool { + self.perms & SysMapPerms::Read as u8 != 0 + } + + fn write(&self) -> bool { + self.perms & SysMapPerms::Write as u8 != 0 + } + + fn execute(&self) -> bool { + self.perms & SysMapPerms::Execute as u8 != 0 + } + + fn cached(&self) -> bool { + self.cached + } } impl Map for SysIOMap { @@ -386,7 +398,24 @@ impl Map for SysIOMap { fn range_name(&self) -> &'static str { "io address range" } + + fn read(&self) -> bool { + matches!(self.perms, SysIOMapPerms::Read | SysIOMapPerms::ReadWrite) + } + + fn write(&self) -> bool { + matches!(self.perms, SysIOMapPerms::Write | SysIOMapPerms::ReadWrite) + } + + fn execute(&self) -> bool { + false + } + + fn cached(&self) -> bool { + false + } } + #[derive(Debug, PartialEq, Eq, Clone)] pub enum SysMemoryRegionKind { User, From d22e3333483f2acadb077e9b80daaa30baf2f130 Mon Sep 17 00:00:00 2001 From: Callum Date: Mon, 29 Jun 2026 15:18:41 +1000 Subject: [PATCH 3/4] IOMMU: Refactor Address Space creation This commit is meant to preserve original functionality. The memory.rs file previously was a collection of functions that allowed the mapping of pages into vspaces. This commit refactors this logic into an AddressSpace type. This will allow us to simply support new variants of address spaces, including IO Address Spaces for devices. The majority of changes are made to allow the old functions to be reusued in a more generic way. The changes to the builder.rs reflect the changes to memory.rs or make use of the trait Map as trait bounds to handle both normal Mappings and IOMappings. Signed-off-by: Callum --- tool/microkit/src/capdl/builder.rs | 198 ++++++----- tool/microkit/src/capdl/memory.rs | 548 ++++++++++++++++------------- 2 files changed, 408 insertions(+), 338 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index ab9863fb9..51c403a0b 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -18,14 +18,14 @@ use sel4_capdl_initializer_types::{ use crate::{ capdl::{ irq::create_irq_handler_cap, - memory::{create_vspace, create_vspace_ept, map_page}, + memory::{create_vspace, create_vspace_ept, AddressSpace}, spec::{capdl_obj_physical_size_bits, BytesContent, ElfContent, FillContent}, util::*, }, elf::ElfFile, sdf::{ - CapMapType, CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, - MONITOR_PD_NAME, MONITOR_PRIORITY, + CapMapType, CpuCore, Map, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME, + MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, util::{ranges_overlap, round_down, round_up}, @@ -122,6 +122,11 @@ struct PDShadowCspace { vspace: ObjectId, } +struct ElfSpecResult { + tcb: ObjectId, + address_space: AddressSpace, +} + pub struct CapDLSpecContainer { pub spec: Spec, /// Track allocations as we build the system for later use by the report. @@ -186,7 +191,7 @@ impl CapDLSpecContainer { /// as possible. These are the objects that will be created: /// -> TCB: Program counter set and VSpace capability bound. /// -> VSpace: all pages from the ELF mapped in. - /// Returns the object ID of the TCB + /// Returns ElfSpecResult containing the TCB object ID and the PDs address space. /// NOTE that all ELF frames will just be reference to the original ELF object rather than the actual data. /// So that symbols can be patched before the frames' data are filled in. fn add_elf_to_spec( @@ -196,9 +201,10 @@ impl CapDLSpecContainer { pd_cpu: CpuCore, elf_id: usize, elf: &ElfFile, - ) -> Result { + ) -> Result { // We assumes that ELFs and PDs have a one-to-one relationship. So for each ELF we create a VSpace. - let vspace_obj_id = create_vspace(self, sel4_config, pd_name); + let address_space = create_vspace(self, sel4_config, pd_name); + let vspace_obj_id = address_space.root(); let vspace_cap = capdl_util_make_page_table_cap(vspace_obj_id); // For each loadable segment in the ELF, map it into the address space of this PD. @@ -268,11 +274,9 @@ impl CapDLSpecContainer { true, ); - match map_page( + match address_space.map_page( self, sel4_config, - pd_name, - vspace_obj_id, frame_cap, page_size_bytes, cur_vaddr, @@ -286,7 +290,7 @@ impl CapDLSpecContainer { "add_elf_to_spec(): failed to map segment page to ELF because: {map_err_reason}" )) } - }; + } } } @@ -318,42 +322,47 @@ impl CapDLSpecContainer { object: Object::Tcb(tcb_inner_obj), }; - Ok(self.add_root_object(tcb_obj)) + Ok(ElfSpecResult { + tcb: self.add_root_object(tcb_obj), + address_space, + }) } } -/// Given a SysMap, page size, VSpace object ID, and a Vec of frame object ids, -/// map all frames into the given VSpace at the requested vaddr. -fn map_memory_region( +/// Given a map, page size, address space, and a Vec of frame object ids, map +/// all frames into the requested address space at the requested address. +fn map_memory_region( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, - pd_name: &str, - map: &SysMap, + map: &M, page_sz: u64, - target_vspace: ObjectId, + target_address_space: &AddressSpace, frames: &[ObjectId], -) { - let mut cur_vaddr = map.vaddr; - let read = map.perms & SysMapPerms::Read as u8 != 0; - let write = map.perms & SysMapPerms::Write as u8 != 0; - let execute = map.perms & SysMapPerms::Execute as u8 != 0; - let cached = map.cached; +) -> Result<(), String> { + let mut cur_vaddr = map.addr(); + let read = map.read(); + let write = map.write(); + let execute = map.execute(); for frame_obj_id in frames.iter() { // Make a cap for this frame. - let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, read, write, execute, cached); + let frame_cap = + capdl_util_make_frame_cap(*frame_obj_id, read, write, execute, map.cached()); // Map it into this PD address space. - map_page( - spec_container, - sel4_config, - pd_name, - target_vspace, - frame_cap, - page_sz, - cur_vaddr, - ) - .unwrap(); + target_address_space + .map_page(spec_container, sel4_config, frame_cap, page_sz, cur_vaddr) + .map_err(|err| { + format!( + "failed to map {} for MR '{}' into address-space '{}' at {} {:#x}: {err}", + map.element(), + map.mr_name(), + target_address_space.name(), + map.addr_name(), + cur_vaddr + ) + })?; cur_vaddr += page_sz; } + Ok(()) } /// Build a CapDL Spec according to the System Description File. @@ -371,18 +380,16 @@ pub fn build_capdl_spec( // We expect the PD ELFs to be first and the monitor ELF last in the list of ELFs. let mon_elf_id = elfs.len() - 1; assert!(elfs.len() == system.protection_domains.len() + 1); - let monitor_tcb_obj_id = { - let monitor_elf = &elfs[mon_elf_id]; - spec_container - .add_elf_to_spec( - kernel_config, - MONITOR_PD_NAME, - CpuCore(0), - mon_elf_id, - monitor_elf, - ) - .unwrap() - }; + let monitor_elf_spec = spec_container + .add_elf_to_spec( + kernel_config, + MONITOR_PD_NAME, + CpuCore(0), + mon_elf_id, + &elfs[mon_elf_id], + ) + .unwrap(); + let monitor_tcb_obj_id = monitor_elf_spec.tcb; // Create monitor fault endpoint object + cap let mon_fault_ep_obj_id = @@ -430,18 +437,16 @@ pub fn build_capdl_spec( ); let mon_stack_frame_cap = capdl_util_make_frame_cap(mon_stack_frame_obj_id, true, true, false, true); - let mon_vspace_obj_id = - capdl_util_get_vspace_id_from_tcb_id(&spec_container, monitor_tcb_obj_id); - map_page( - &mut spec_container, - kernel_config, - MONITOR_PD_NAME, - mon_vspace_obj_id, - mon_stack_frame_cap, - PageSize::Small as u64, - kernel_config.pd_stack_bottom(MON_STACK_SIZE), - ) - .unwrap(); + monitor_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + mon_stack_frame_cap, + PageSize::Small as u64, + kernel_config.pd_stack_bottom(MON_STACK_SIZE), + ) + .unwrap(); // Create monitor IPC Bufffer let mon_ipcbuf_frame_obj_id = capdl_util_make_frame_obj( @@ -453,16 +458,16 @@ pub fn build_capdl_spec( ); let mon_ipcbuf_frame_cap = capdl_util_make_frame_cap(mon_ipcbuf_frame_obj_id, true, true, false, true); - map_page( - &mut spec_container, - kernel_config, - MONITOR_PD_NAME, - mon_vspace_obj_id, - mon_ipcbuf_frame_cap.clone(), - PageSize::Small as u64, - kernel_config.pd_ipc_buffer(), - ) - .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); + monitor_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + mon_ipcbuf_frame_cap.clone(), + PageSize::Small as u64, + kernel_config.pd_ipc_buffer(), + ) + .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); // At this point, all of the required objects for the monitor have been created and its caps inserted into // the correct slot in the CSpace. We need to bind those objects into the TCB for the monitor to use them. @@ -605,9 +610,11 @@ pub fn build_capdl_spec( let mut caps_to_insert_to_pd_cspace: Vec = Vec::new(); // Step 3-1: Create TCB and VSpace with all ELF loadable frames mapped in. - let pd_tcb_obj_id = spec_container + let pd_elf_spec = spec_container .add_elf_to_spec(kernel_config, &pd.name, pd.cpu, pd_global_idx, elf_obj) .unwrap(); + + let pd_tcb_obj_id = pd_elf_spec.tcb; let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id); // In the benchmark configuration, we allow PDs to access their own TCB. @@ -653,12 +660,11 @@ pub fn build_capdl_spec( map_memory_region( &mut spec_container, kernel_config, - &pd.name, map, page_size_bytes, - pd_vspace_obj_id, + &pd_elf_spec.address_space, frames, - ); + )?; } // Step 3-3a: Create and map in the IPC buffer @@ -671,16 +677,16 @@ pub fn build_capdl_spec( ); let ipcbuf_frame_cap = capdl_util_make_frame_cap(ipcbuf_frame_obj_id, true, true, false, true); - map_page( - &mut spec_container, - kernel_config, - &pd.name, - pd_vspace_obj_id, - ipcbuf_frame_cap.clone(), - PageSize::Small as u64, - kernel_config.pd_ipc_buffer(), - ) - .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); + pd_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + ipcbuf_frame_cap.clone(), + PageSize::Small as u64, + kernel_config.pd_ipc_buffer(), + ) + .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::IpcBuffer as u32, ipcbuf_frame_cap, @@ -702,16 +708,16 @@ pub fn build_capdl_spec( ); let stack_frame_cap = capdl_util_make_frame_cap(stack_frame_obj_id, true, true, false, true); - map_page( - &mut spec_container, - kernel_config, - &pd.name, - pd_vspace_obj_id, - stack_frame_cap, - PageSize::Small as u64, - cur_stack_vaddr, - ) - .unwrap(); + pd_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + stack_frame_cap, + PageSize::Small as u64, + cur_stack_vaddr, + ) + .unwrap(); cur_stack_vaddr += PageSize::Small as u64; } @@ -846,12 +852,13 @@ pub fn build_capdl_spec( // Create VM's Address Space and map in all memory regions. // This address space is shared across all vCPUs. The virtual address that we "map" the region is guest-physical. - let vm_vspace_obj_id = match kernel_config.arch { + let vm_address_space = match kernel_config.arch { Arch::X86_64 => { create_vspace_ept(&mut spec_container, kernel_config, &virtual_machine.name) } _ => create_vspace(&mut spec_container, kernel_config, &virtual_machine.name), }; + let vm_vspace_obj_id = vm_address_space.root(); let vm_vspace_cap = capdl_util_make_page_table_cap(vm_vspace_obj_id); for map in virtual_machine.maps.iter() { let frames = &mr_name_to_frames[&map.mr]; @@ -860,12 +867,11 @@ pub fn build_capdl_spec( map_memory_region( &mut spec_container, kernel_config, - &virtual_machine.name, map, page_size_bytes, - vm_vspace_obj_id, + &vm_address_space, frames, - ); + )?; } if kernel_config.arch == Arch::X86_64 { diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index d8b0c7bd1..d1b1fcd5a 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -4,7 +4,10 @@ // SPDX-License-Identifier: BSD-2-Clause // use crate::{ - capdl::{util::capdl_util_make_cte, CapDLNamedObject, CapDLSpecContainer}, + capdl::{ + spec::capdl_obj_human_name, util::capdl_util_make_cte, CapDLNamedObject, + CapDLSpecContainer, FrameFill, + }, sel4::{Arch, Config, PageSize}, }; use sel4_capdl_initializer_types::{cap, object, Cap, Object, ObjectId}; @@ -45,291 +48,352 @@ fn get_pt_level_name(sel4_config: &Config, level: usize) -> &str { } } -fn get_pt_level_index(sel4_config: &Config, level: usize, vaddr: u64) -> usize { - let levels = sel4_config.num_page_table_levels(); +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum AddressSpace { + VSpace { + name: String, + root: ObjectId, + x86_ept: bool, + }, +} - assert!(level < levels); +impl AddressSpace { + pub fn root(&self) -> ObjectId { + match self { + &Self::VSpace { root, .. } => root, + } + } + pub fn name(&self) -> &str { + match self { + Self::VSpace { name, .. } => name, + } + } - let index_bits = |level: usize| -> u64 { - if level == top_pt_level_number(sel4_config) - && sel4_config.arch == Arch::Aarch64 - && sel4_config.aarch64_vspace_s2_start_l1() - { - // Special case for first level on AArch64 platforms with hyp and 40 bits PA. - // It have 10 bits index for VSpace. - // match up with seL4_VSpaceBits in seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h - 10 - } else { - 9 + pub fn map_page( + &self, + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + frame_cap: Cap, + frame_size_bytes: u64, + addr: u64, + ) -> Result<(), String> { + self.map_recursive( + spec_container, + sel4_config, + self.root(), + Self::get_root_level(sel4_config), + frame_cap, + frame_size_bytes, + addr, + ) + } + + fn get_leaf_level(&self, sel4_config: &Config, page_size_bytes: u64) -> usize { + const SMALL_PAGE_BYTES: u64 = PageSize::Small as u64; + const LARGE_PAGE_BYTES: u64 = PageSize::Large as u64; + let levels = self.address_space_levels(sel4_config); + + match page_size_bytes { + SMALL_PAGE_BYTES => levels - 1, + LARGE_PAGE_BYTES => levels - 2, + _ => unreachable!( + "internal bug: get_pt_level_to_insert(): unknown page_size_bytes: {page_size_bytes}" + ), } - }; + } - let page_bits = 12; - let bits_from_higher_lvls: u64 = ((level + 1)..levels).map(index_bits).sum(); - let shift = page_bits + bits_from_higher_lvls; - let width = index_bits(level); - let mask = (1u64 << width) - 1; + fn get_level_name(&self, sel4_config: &Config, level: usize) -> String { + match self { + Self::VSpace { .. } => get_pt_level_name(sel4_config, level).to_string(), + } + } - ((vaddr >> shift) & mask) as usize -} + fn get_addr_label(&self) -> &'static str { + match self { + Self::VSpace { .. } => "vaddr", + } + } -fn get_pt_level_coverage(sel4_config: &Config, level: usize, vaddr: u64) -> Range { - let levels = sel4_config.num_page_table_levels() as u64; - let page_bits = 12; - let bits_from_higher_lvls: u64 = (levels - (level as u64)) * 9; + fn get_level_index(&self, sel4_config: &Config, level: usize, vaddr: u64) -> usize { + let levels = self.address_space_levels(sel4_config); - let coverage_bits = page_bits + bits_from_higher_lvls; + assert!(level < levels); - let low = (vaddr >> coverage_bits) << coverage_bits; - let high = vaddr | ((1 << coverage_bits) - 1); + let index_bits = |level: usize| -> u64 { + if matches!(self, AddressSpace::VSpace { .. }) + && level == Self::get_root_level(sel4_config) + && sel4_config.arch == Arch::Aarch64 + && sel4_config.aarch64_vspace_s2_start_l1() + { + // Special case for first level on AArch64 platforms with hyp and 40 bits PA. + // It have 10 bits index for VSpace. + // match up with seL4_VSpaceBits in seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h + 10 + } else { + 9 + } + }; - low..high -} + let page_bits = 12; + let bits_from_higher_lvls: u64 = ((level + 1)..levels).map(index_bits).sum(); + let shift = page_bits + bits_from_higher_lvls; + let width = index_bits(level); + let mask = (1u64 << width) - 1; -fn get_pt_level_to_insert(sel4_config: &Config, page_size_bytes: u64) -> usize { - const SMALL_PAGE_BYTES: u64 = PageSize::Small as u64; - const LARGE_PAGE_BYTES: u64 = PageSize::Large as u64; - match page_size_bytes { - SMALL_PAGE_BYTES => sel4_config.num_page_table_levels() - 1, - LARGE_PAGE_BYTES => sel4_config.num_page_table_levels() - 2, - _ => unreachable!( - "internal bug: get_pt_level_to_insert(): unknown page_size_bytes: {page_size_bytes}" - ), + ((vaddr >> shift) & mask) as usize } -} -fn top_pt_level_number(sel4_config: &Config) -> usize { - if sel4_config.arch == Arch::Aarch64 && sel4_config.aarch64_vspace_s2_start_l1() { - 1 - } else { - 0 + fn get_level_coverage(&self, sel4_config: &Config, level: usize, vaddr: u64) -> Range { + let levels = self.address_space_levels(sel4_config) as u64; + + let page_bits = 12; + let bits_from_higher_lvls: u64 = (levels - (level as u64)) * 9; + + let coverage_bits = page_bits + bits_from_higher_lvls; + + let low = (vaddr >> coverage_bits) << coverage_bits; + let high = vaddr | ((1 << coverage_bits) - 1); + + low..high } -} -fn insert_cap_into_page_table_level( - spec_container: &mut CapDLSpecContainer, - cur_level_obj_id: ObjectId, - cur_level: usize, - cur_level_slot: usize, - cap: Cap, -) -> Result<(), String> { - let page_table_level_obj_wrapper = spec_container - .get_root_object_mut(cur_level_obj_id) - .unwrap(); - if let Object::PageTable(page_table_object) = &mut page_table_level_obj_wrapper.object { - // Sanity check that this slot is free - match page_table_object - .slots + #[allow(clippy::too_many_arguments)] + fn map_recursive( + &self, + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + cur_level_obj_id: ObjectId, + cur_level: usize, + frame_cap: Cap, + frame_size_bytes: u64, + addr: u64, + ) -> Result<(), String> { + if cur_level >= self.address_space_levels(sel4_config) { + unreachable!("internal bug: recursed past the final address-space level"); + } + + let slot = self.get_level_index(sel4_config, cur_level, addr); + let leaf_level = self.get_leaf_level(sel4_config, frame_size_bytes); + + if cur_level == leaf_level { + self.insert_cap_into_level( + spec_container, + sel4_config, + cur_level_obj_id, + cur_level, + slot, + frame_cap, + ) + } else { + let next_obj_id = self.map_intermediary_level_helper( + spec_container, + sel4_config, + cur_level_obj_id, + cur_level, + slot, + addr, + )?; + self.map_recursive( + spec_container, + sel4_config, + next_obj_id, + cur_level + 1, + frame_cap, + frame_size_bytes, + addr, + ) + } + } + + fn map_intermediary_level_helper( + &self, + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + cur_level_obj_id: ObjectId, + cur_level: usize, + cur_level_slot: usize, + addr: u64, + ) -> Result { + let object = &spec_container + .get_root_object(cur_level_obj_id) + .unwrap() + .object; + + self.valid_level_object(object, sel4_config, cur_level)?; + let slots = object.slots().unwrap(); + + if let Some(child_obj_id) = slots .iter() .find(|cte| usize::from(cte.slot) == cur_level_slot) + .map(|cte| cte.cap.obj()) { - Some(_) => Err(format!( - "insert_cap_into_page_table_level(): internal bug: slot {} at PT level {} with name '{}' already filled", - cur_level_slot, cur_level, spec_container.get_root_object(cur_level_obj_id).unwrap().name.as_ref().unwrap() - )), - None => { - page_table_object.slots.push(capdl_util_make_cte(cur_level_slot as u32, cap)); - Ok(()) - } + return Ok(child_obj_id); } - } else { - Err(format!( - "insert_cap_into_page_table_level(): internal bug: received a non-Page Table object id {} with name '{}'", - usize::from(cur_level_obj_id), spec_container.get_root_object(cur_level_obj_id).unwrap().name.as_ref().unwrap() - )) + + let next_level = cur_level + 1; + let next_level_coverage = self.get_level_coverage(sel4_config, next_level, addr); + let next_level_obj = CapDLNamedObject { + name: self + .object_name(sel4_config, next_level, next_level_coverage.start) + .into(), + object: self.make_intermediate_object(next_level), + }; + let next_obj_id = spec_container.add_root_object(next_level_obj); + let next_cap = self.make_intermediate_cap(next_obj_id); + + self.insert_cap_into_level( + spec_container, + sel4_config, + cur_level_obj_id, + cur_level, + cur_level_slot, + next_cap, + )?; + + Ok(next_obj_id) } -} -// Just this one time pinky promise -#[allow(clippy::too_many_arguments)] -fn map_intermediary_level_helper( - spec_container: &mut CapDLSpecContainer, - sel4_config: &Config, - pd_name: &str, - next_level_name_prefix: &str, - vspace_obj_id: ObjectId, - cur_level_obj_id: ObjectId, - cur_level: usize, - cur_level_slot: usize, - vaddr: u64, -) -> Result { - let page_table_level_obj_wrapper = spec_container.get_root_object(cur_level_obj_id).unwrap(); - if let Object::PageTable(page_table_object) = &page_table_level_obj_wrapper.object { - match page_table_object - .slots + fn insert_cap_into_level( + &self, + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + cur_level_obj_id: ObjectId, + cur_level: usize, + cur_level_slot: usize, + cap: Cap, + ) -> Result<(), String> { + let object = &mut spec_container + .get_root_object_mut(cur_level_obj_id) + .unwrap() + .object; + + self.valid_level_object(object, sel4_config, cur_level)?; + + let slots = object.slots_mut().unwrap(); + + if slots .iter() - .find(|cte| usize::from(cte.slot) == cur_level_slot) + .any(|cte| usize::from(cte.slot) == cur_level_slot) { - Some(cte_unwrapped) => { - // Next level object already created, nothing to do here - return Ok(cte_unwrapped.cap.obj()); - } - None => { - // We need to create the next level paging structure, get out of this scope for now - // so we don't get a double mutable borrow of spec when we need to insert the next level object - } + Err(format!( + "address-space '{}': slot {} at level {} in object '{}' is already filled", + self.name(), + cur_level_slot, + cur_level, + spec_container + .get_root_object(cur_level_obj_id) + .unwrap() + .name + .as_ref() + .unwrap() + )) + } else { + slots.push(capdl_util_make_cte(cur_level_slot as u32, cap)); + Ok(()) } - } else { - return Err(format!("map_intermediary_level_helper(): internal bug: received a non-Page Table object id {} with name '{}', for mapping at level {}, to pd {}.", - usize::from(cur_level_obj_id), spec_container.get_root_object(cur_level_obj_id).unwrap().name.as_ref().unwrap(), cur_level, pd_name)); } - // Next level object not already created, create it. - let vspace_obj = match &spec_container.get_root_object(vspace_obj_id).unwrap().object { - Object::PageTable(o) => o, - _ => unreachable!( - "map_intermediary_level_helper(): internal bug: received a non VSpace object id {} with name '{}'", - usize::from(vspace_obj_id), spec_container.get_root_object(vspace_obj_id).unwrap().name.as_ref().unwrap() - ), - }; - let next_level_coverage = get_pt_level_coverage(sel4_config, cur_level + 1, vaddr); - let next_level_inner_obj = object::PageTable { - x86_ept: vspace_obj.x86_ept, - is_root: false, // because the VSpace has already been created separately - level: Some(cur_level as u8 + 1), - slots: [].to_vec(), - }; - // We create name with this PT level coverage so that every object names are unique - let next_level_object = CapDLNamedObject { - name: format!( - "{}_{}_vaddr_0x{:x}", - next_level_name_prefix, pd_name, next_level_coverage.start - ) - .into(), - object: Object::PageTable(next_level_inner_obj), - }; - let next_level_obj_id = spec_container.add_root_object(next_level_object); - let next_level_cap = Cap::PageTable(cap::PageTable { - object: next_level_obj_id, - }); + fn make_intermediate_object(&self, level: usize) -> Object { + match self { + &AddressSpace::VSpace { x86_ept, .. } => Object::PageTable(object::PageTable { + x86_ept, + is_root: false, + level: Some(level as u8), + slots: vec![], + }), + } + } - // Then insert into the correct slot at the current level, return and continue mapping - match insert_cap_into_page_table_level( - spec_container, - cur_level_obj_id, - cur_level, - cur_level_slot, - next_level_cap, - ) { - Ok(_) => Ok(next_level_obj_id), - Err(err_reason) => Err(err_reason), + fn make_intermediate_cap(&self, object: ObjectId) -> Cap { + match self { + AddressSpace::VSpace { .. } => Cap::PageTable(cap::PageTable { object }), + } } -} -pub fn create_vspace( - spec_container: &mut CapDLSpecContainer, - sel4_config: &Config, - pd_name: &str, -) -> ObjectId { - spec_container.add_root_object(CapDLNamedObject { - name: format!( - "{}_{}", - get_pt_level_name(sel4_config, top_pt_level_number(sel4_config)), - pd_name + fn object_name(&self, sel4_config: &Config, level: usize, coverage_start: u64) -> String { + format!( + "{}_{}_{}_{:#x}", + self.get_level_name(sel4_config, level), + self.name(), + self.get_addr_label(), + coverage_start ) - .into(), - object: Object::PageTable(object::PageTable { - x86_ept: false, - is_root: true, - level: Some(top_pt_level_number(sel4_config) as u8), - slots: [].to_vec(), - }), - }) + } + + fn valid_level_object( + &self, + object: &Object, + sel4_config: &Config, + cur_level: usize, + ) -> Result<(), String> { + let valid = match self { + AddressSpace::VSpace { .. } => matches!(object, Object::PageTable(_)), + }; + if valid { + Ok(()) + } else { + Err(format!( + "Error: found an invalid object {} at level {} in address-space {}!", + capdl_obj_human_name(object, sel4_config), + cur_level, + self.name() + )) + } + } + + fn address_space_levels(&self, sel4_config: &Config) -> usize { + match self { + AddressSpace::VSpace { .. } => sel4_config.num_page_table_levels(), + } + } + + fn get_root_level(sel4_config: &Config) -> usize { + if sel4_config.arch == Arch::Aarch64 && sel4_config.aarch64_vspace_s2_start_l1() { + 1 + } else { + 0 + } + } } -pub fn create_vspace_ept( +fn create_vspace_address_space( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, - vm_name: &str, -) -> ObjectId { - assert!(sel4_config.arch == Arch::X86_64); + name: &str, + x86_ept: bool, +) -> AddressSpace { + let root_level = AddressSpace::get_root_level(sel4_config); - spec_container.add_root_object(CapDLNamedObject { - name: format!("{}_{}", get_pt_level_name(sel4_config, 0), vm_name).into(), + let root = spec_container.add_root_object(CapDLNamedObject { + name: format!("{}_{}", get_pt_level_name(sel4_config, root_level), name).into(), object: Object::PageTable(object::PageTable { - x86_ept: true, + x86_ept, is_root: true, - level: Some(top_pt_level_number(sel4_config) as u8), - slots: [].to_vec(), + level: Some(root_level as u8), + slots: vec![], }), - }) + }); + + AddressSpace::VSpace { + name: name.to_string(), + root, + x86_ept, + } } -#[allow(clippy::too_many_arguments)] -fn map_recursive( +pub fn create_vspace( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, pd_name: &str, - vspace_obj_id: ObjectId, - pt_obj_id: ObjectId, - cur_level: usize, - frame_cap: Cap, - frame_size_bytes: u64, - vaddr: u64, -) -> Result<(), String> { - if cur_level >= sel4_config.num_page_table_levels() { - unreachable!("internal bug: we should have never recursed further!"); - } - - let this_level_index = get_pt_level_index(sel4_config, cur_level, vaddr); - - if cur_level == get_pt_level_to_insert(sel4_config, frame_size_bytes) { - // Base case: we got to the target level to insert the frame cap. - insert_cap_into_page_table_level( - spec_container, - pt_obj_id, - cur_level, - this_level_index, - frame_cap, - ) - } else { - // Recursive case: we have not gotten to the correct level, create the next level and recurse down. - let next_level_name_prefix = get_pt_level_name(sel4_config, cur_level + 1); - match map_intermediary_level_helper( - spec_container, - sel4_config, - pd_name, - next_level_name_prefix, - vspace_obj_id, - pt_obj_id, - cur_level, - this_level_index, - vaddr, - ) { - Ok(next_level_pt_obj_id) => map_recursive( - spec_container, - sel4_config, - pd_name, - vspace_obj_id, - next_level_pt_obj_id, - cur_level + 1, - frame_cap, - frame_size_bytes, - vaddr, - ), - Err(err_reason) => Err(err_reason), - } - } +) -> AddressSpace { + create_vspace_address_space(spec_container, sel4_config, pd_name, false) } -pub fn map_page( +pub fn create_vspace_ept( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, - pd_name: &str, - vspace_obj_id: ObjectId, - frame_cap: Cap, - frame_size_bytes: u64, - vaddr: u64, -) -> Result<(), String> { - map_recursive( - spec_container, - sel4_config, - pd_name, - vspace_obj_id, - vspace_obj_id, - top_pt_level_number(sel4_config), - frame_cap, - frame_size_bytes, - vaddr, - ) + vm_name: &str, +) -> AddressSpace { + assert!(sel4_config.arch == Arch::X86_64); + create_vspace_address_space(spec_container, sel4_config, vm_name, true) } From 9ecdac4fce8fc542b750499b288085f486934141 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 9 Jul 2026 13:06:29 +1000 Subject: [PATCH 4/4] Memory Refactor: Integrate the improved config This commit integrates the improved config to the memory module. This commit removes some of the duplicated constants definitions that seL4 already exports. Signed-off-by: Callum --- tool/microkit/src/capdl/memory.rs | 59 +++++++++++++++---------------- 1 file changed, 28 insertions(+), 31 deletions(-) diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index d1b1fcd5a..3061af1aa 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -8,7 +8,7 @@ use crate::{ spec::capdl_obj_human_name, util::capdl_util_make_cte, CapDLNamedObject, CapDLSpecContainer, FrameFill, }, - sel4::{Arch, Config, PageSize}, + sel4::{Arch, Config, ObjectType, PageSize}, }; use sel4_capdl_initializer_types::{cap, object, Cap, Object, ObjectId}; use std::ops::Range; @@ -81,7 +81,7 @@ impl AddressSpace { spec_container, sel4_config, self.root(), - Self::get_root_level(sel4_config), + self.get_root_level(sel4_config), frame_cap, frame_size_bytes, addr, @@ -114,40 +114,39 @@ impl AddressSpace { } } + fn get_leaf_bits(&self, sel4_config: &Config) -> u64 { + match self { + Self::VSpace { .. } => ObjectType::SmallPage.fixed_size_bits(sel4_config).unwrap(), + } + } + + fn level_index_bits(&self, sel4_config: &Config, level: usize) -> u64 { + match self { + Self::VSpace { .. } => sel4_config.vspace_level_index_bits(level), + } + } + fn get_level_index(&self, sel4_config: &Config, level: usize, vaddr: u64) -> usize { let levels = self.address_space_levels(sel4_config); - assert!(level < levels); - let index_bits = |level: usize| -> u64 { - if matches!(self, AddressSpace::VSpace { .. }) - && level == Self::get_root_level(sel4_config) - && sel4_config.arch == Arch::Aarch64 - && sel4_config.aarch64_vspace_s2_start_l1() - { - // Special case for first level on AArch64 platforms with hyp and 40 bits PA. - // It have 10 bits index for VSpace. - // match up with seL4_VSpaceBits in seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h - 10 - } else { - 9 - } - }; - - let page_bits = 12; - let bits_from_higher_lvls: u64 = ((level + 1)..levels).map(index_bits).sum(); + let page_bits = self.get_leaf_bits(sel4_config); + let bits_from_higher_lvls: u64 = ((level + 1)..levels) + .map(|level| self.level_index_bits(sel4_config, level)) + .sum(); let shift = page_bits + bits_from_higher_lvls; - let width = index_bits(level); + let width = self.level_index_bits(sel4_config, level); let mask = (1u64 << width) - 1; ((vaddr >> shift) & mask) as usize } fn get_level_coverage(&self, sel4_config: &Config, level: usize, vaddr: u64) -> Range { - let levels = self.address_space_levels(sel4_config) as u64; - - let page_bits = 12; - let bits_from_higher_lvls: u64 = (levels - (level as u64)) * 9; + let levels = self.address_space_levels(sel4_config); + let page_bits = self.get_leaf_bits(sel4_config); + let bits_from_higher_lvls: u64 = ((level + 1)..levels) + .map(|level| self.level_index_bits(sel4_config, level)) + .sum(); let coverage_bits = page_bits + bits_from_higher_lvls; @@ -347,11 +346,9 @@ impl AddressSpace { } } - fn get_root_level(sel4_config: &Config) -> usize { - if sel4_config.arch == Arch::Aarch64 && sel4_config.aarch64_vspace_s2_start_l1() { - 1 - } else { - 0 + fn get_root_level(&self, sel4_config: &Config) -> usize { + match self { + AddressSpace::VSpace { .. } => sel4_config.vspace_root_level(), } } } @@ -362,7 +359,7 @@ fn create_vspace_address_space( name: &str, x86_ept: bool, ) -> AddressSpace { - let root_level = AddressSpace::get_root_level(sel4_config); + let root_level = sel4_config.vspace_root_level(); let root = spec_container.add_root_object(CapDLNamedObject { name: format!("{}_{}", get_pt_level_name(sel4_config, root_level), name).into(),