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/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..3061af1aa 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -4,8 +4,11 @@ // SPDX-License-Identifier: BSD-2-Clause // use crate::{ - capdl::{util::capdl_util_make_cte, CapDLNamedObject, CapDLSpecContainer}, - sel4::{Arch, Config, PageSize}, + capdl::{ + spec::capdl_obj_human_name, util::capdl_util_make_cte, CapDLNamedObject, + CapDLSpecContainer, FrameFill, + }, + sel4::{Arch, Config, ObjectType, PageSize}, }; use sel4_capdl_initializer_types::{cap, object, Cap, Object, ObjectId}; use std::ops::Range; @@ -45,291 +48,349 @@ 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_leaf_bits(&self, sel4_config: &Config) -> u64 { + match self { + Self::VSpace { .. } => ObjectType::SmallPage.fixed_size_bits(sel4_config).unwrap(), + } + } - let coverage_bits = page_bits + bits_from_higher_lvls; + fn level_index_bits(&self, sel4_config: &Config, level: usize) -> u64 { + match self { + Self::VSpace { .. } => sel4_config.vspace_level_index_bits(level), + } + } - let low = (vaddr >> coverage_bits) << coverage_bits; - let high = vaddr | ((1 << coverage_bits) - 1); + fn get_level_index(&self, sel4_config: &Config, level: usize, vaddr: u64) -> usize { + let levels = self.address_space_levels(sel4_config); + assert!(level < levels); - low..high -} + 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 = self.level_index_bits(sel4_config, 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); + 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; + + 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(&self, sel4_config: &Config) -> usize { + match self { + AddressSpace::VSpace { .. } => sel4_config.vspace_root_level(), + } + } } -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 = sel4_config.vspace_root_level(); - 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) } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index b59783ade..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)] @@ -321,18 +313,23 @@ 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, } -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 { @@ -359,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 { @@ -385,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, @@ -705,6 +735,7 @@ impl SysIOMap { node: &roxmltree::Node, device: &str, identifier: IommuDeviceIdentifier, + domain_id: Option, ) -> Result { let attrs = vec!["mr", "iovaddr", "perms"]; @@ -745,6 +776,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 +797,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 +808,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 +818,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 +868,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 +2380,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 +2421,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)]