diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 4a66b7546..96cd71171 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -18,14 +18,14 @@ use sel4_capdl_initializer_types::{ use crate::{ capdl::{ irq::create_irq_handler_cap, - memory::{create_vspace, create_vspace_ept, map_page}, + memory::{create_vspace, create_vspace_ept, AddressSpace}, spec::{capdl_obj_physical_size_bits, BytesContent, ElfContent, FillContent}, util::*, }, elf::ElfFile, sdf::{ - CapMapType, CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, - MONITOR_PD_NAME, MONITOR_PRIORITY, + CapMapType, CpuCore, Map, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME, + MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, util::{ranges_overlap, round_down, round_up}, @@ -145,6 +145,11 @@ impl PDShadowCspace { } } +struct ElfSpecResult { + tcb: ObjectId, + address_space: AddressSpace, +} + pub struct CapDLSpecContainer { pub spec: Spec, /// Track allocations as we build the system for later use by the report. @@ -209,7 +214,7 @@ impl CapDLSpecContainer { /// as possible. These are the objects that will be created: /// -> TCB: Program counter set and VSpace capability bound. /// -> VSpace: all pages from the ELF mapped in. - /// Returns the object ID of the TCB + /// Returns ElfSpecResult containing the TCB object ID and the PDs address space. /// NOTE that all ELF frames will just be reference to the original ELF object rather than the actual data. /// So that symbols can be patched before the frames' data are filled in. fn add_elf_to_spec( @@ -219,9 +224,10 @@ impl CapDLSpecContainer { pd_cpu: CpuCore, elf_id: usize, elf: &ElfFile, - ) -> Result { + ) -> Result { // We assumes that ELFs and PDs have a one-to-one relationship. So for each ELF we create a VSpace. - let vspace_obj_id = create_vspace(self, sel4_config, pd_name); + let address_space = create_vspace(self, sel4_config, pd_name); + let vspace_obj_id = address_space.root(); let vspace_cap = capdl_util_make_page_table_cap(vspace_obj_id); // For each loadable segment in the ELF, map it into the address space of this PD. @@ -291,11 +297,9 @@ impl CapDLSpecContainer { true, ); - match map_page( + match address_space.map_page( self, sel4_config, - pd_name, - vspace_obj_id, frame_cap, page_size_bytes, cur_vaddr, @@ -309,7 +313,7 @@ impl CapDLSpecContainer { "add_elf_to_spec(): failed to map segment page to ELF because: {map_err_reason}" )) } - }; + } } } @@ -341,42 +345,47 @@ impl CapDLSpecContainer { object: Object::Tcb(tcb_inner_obj), }; - Ok(self.add_root_object(tcb_obj)) + Ok(ElfSpecResult { + tcb: self.add_root_object(tcb_obj), + address_space, + }) } } -/// Given a SysMap, page size, VSpace object ID, and a Vec of frame object ids, -/// map all frames into the given VSpace at the requested vaddr. -fn map_memory_region( +/// Given a map, page size, address space, and a Vec of frame object ids, map +/// all frames into the requested address space at the requested address. +fn map_memory_region( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, - pd_name: &str, - map: &SysMap, + map: &M, page_sz: u64, - target_vspace: ObjectId, + target_address_space: &AddressSpace, frames: &[ObjectId], -) { - let mut cur_vaddr = map.vaddr; - let read = map.perms & SysMapPerms::Read as u8 != 0; - let write = map.perms & SysMapPerms::Write as u8 != 0; - let execute = map.perms & SysMapPerms::Execute as u8 != 0; - let cached = map.cached; +) -> Result<(), String> { + let mut cur_vaddr = map.addr(); + let read = map.read(); + let write = map.write(); + let execute = map.execute(); for frame_obj_id in frames.iter() { // Make a cap for this frame. - let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, read, write, execute, cached); + let frame_cap = + capdl_util_make_frame_cap(*frame_obj_id, read, write, execute, map.cached()); // Map it into this PD address space. - map_page( - spec_container, - sel4_config, - pd_name, - target_vspace, - frame_cap, - page_sz, - cur_vaddr, - ) - .unwrap(); + target_address_space + .map_page(spec_container, sel4_config, frame_cap, page_sz, cur_vaddr) + .map_err(|err| { + format!( + "failed to map {} for MR '{}' into address-space '{}' at {} {:#x}: {err}", + map.element(), + map.mr_name(), + target_address_space.name(), + map.addr_name(), + cur_vaddr + ) + })?; cur_vaddr += page_sz; } + Ok(()) } /// Build a CapDL Spec according to the System Description File. @@ -394,18 +403,16 @@ pub fn build_capdl_spec( // We expect the PD ELFs to be first and the monitor ELF last in the list of ELFs. let mon_elf_id = elfs.len() - 1; assert!(elfs.len() == system.protection_domains.len() + 1); - let monitor_tcb_obj_id = { - let monitor_elf = &elfs[mon_elf_id]; - spec_container - .add_elf_to_spec( - kernel_config, - MONITOR_PD_NAME, - CpuCore(0), - mon_elf_id, - monitor_elf, - ) - .unwrap() - }; + let monitor_elf_spec = spec_container + .add_elf_to_spec( + kernel_config, + MONITOR_PD_NAME, + CpuCore(0), + mon_elf_id, + &elfs[mon_elf_id], + ) + .unwrap(); + let monitor_tcb_obj_id = monitor_elf_spec.tcb; // Create monitor fault endpoint object + cap let mon_fault_ep_obj_id = @@ -453,18 +460,16 @@ pub fn build_capdl_spec( ); let mon_stack_frame_cap = capdl_util_make_frame_cap(mon_stack_frame_obj_id, true, true, false, true); - let mon_vspace_obj_id = - capdl_util_get_vspace_id_from_tcb_id(&spec_container, monitor_tcb_obj_id); - map_page( - &mut spec_container, - kernel_config, - MONITOR_PD_NAME, - mon_vspace_obj_id, - mon_stack_frame_cap, - PageSize::Small as u64, - kernel_config.pd_stack_bottom(MON_STACK_SIZE), - ) - .unwrap(); + monitor_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + mon_stack_frame_cap, + PageSize::Small as u64, + kernel_config.pd_stack_bottom(MON_STACK_SIZE), + ) + .unwrap(); // Create monitor IPC Bufffer let mon_ipcbuf_frame_obj_id = capdl_util_make_frame_obj( @@ -476,16 +481,16 @@ pub fn build_capdl_spec( ); let mon_ipcbuf_frame_cap = capdl_util_make_frame_cap(mon_ipcbuf_frame_obj_id, true, true, false, true); - map_page( - &mut spec_container, - kernel_config, - MONITOR_PD_NAME, - mon_vspace_obj_id, - mon_ipcbuf_frame_cap.clone(), - PageSize::Small as u64, - kernel_config.pd_ipc_buffer(), - ) - .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); + monitor_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + mon_ipcbuf_frame_cap.clone(), + PageSize::Small as u64, + kernel_config.pd_ipc_buffer(), + ) + .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); // At this point, all of the required objects for the monitor have been created and its caps inserted into // the correct slot in the CSpace. We need to bind those objects into the TCB for the monitor to use them. @@ -628,9 +633,11 @@ pub fn build_capdl_spec( let mut caps_to_insert_to_pd_cspace: Vec = Vec::new(); // Step 3-1: Create TCB and VSpace with all ELF loadable frames mapped in. - let pd_tcb_obj_id = spec_container + let pd_elf_spec = spec_container .add_elf_to_spec(kernel_config, &pd.name, pd.cpu, pd_global_idx, elf_obj) .unwrap(); + + let pd_tcb_obj_id = pd_elf_spec.tcb; let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id); // In the benchmark configuration, we allow PDs to access their own TCB. @@ -676,12 +683,11 @@ pub fn build_capdl_spec( map_memory_region( &mut spec_container, kernel_config, - &pd.name, map, page_size_bytes, - pd_vspace_obj_id, + &pd_elf_spec.address_space, frames, - ); + )?; } // Step 3-3a: Create and map in the IPC buffer @@ -694,16 +700,16 @@ pub fn build_capdl_spec( ); let ipcbuf_frame_cap = capdl_util_make_frame_cap(ipcbuf_frame_obj_id, true, true, false, true); - map_page( - &mut spec_container, - kernel_config, - &pd.name, - pd_vspace_obj_id, - ipcbuf_frame_cap.clone(), - PageSize::Small as u64, - kernel_config.pd_ipc_buffer(), - ) - .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); + pd_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + ipcbuf_frame_cap.clone(), + PageSize::Small as u64, + kernel_config.pd_ipc_buffer(), + ) + .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::IpcBuffer as u32, ipcbuf_frame_cap, @@ -725,16 +731,16 @@ pub fn build_capdl_spec( ); let stack_frame_cap = capdl_util_make_frame_cap(stack_frame_obj_id, true, true, false, true); - map_page( - &mut spec_container, - kernel_config, - &pd.name, - pd_vspace_obj_id, - stack_frame_cap, - PageSize::Small as u64, - cur_stack_vaddr, - ) - .unwrap(); + pd_elf_spec + .address_space + .map_page( + &mut spec_container, + kernel_config, + stack_frame_cap, + PageSize::Small as u64, + cur_stack_vaddr, + ) + .unwrap(); cur_stack_vaddr += PageSize::Small as u64; } @@ -867,12 +873,13 @@ pub fn build_capdl_spec( // Create VM's Address Space and map in all memory regions. // This address space is shared across all vCPUs. The virtual address that we "map" the region is guest-physical. - let vm_vspace_obj_id = match kernel_config.arch { + let vm_address_space = match kernel_config.arch { Arch::X86_64 => { create_vspace_ept(&mut spec_container, kernel_config, &virtual_machine.name) } _ => create_vspace(&mut spec_container, kernel_config, &virtual_machine.name), }; + let vm_vspace_obj_id = vm_address_space.root(); let vm_vspace_cap = capdl_util_make_page_table_cap(vm_vspace_obj_id); for map in virtual_machine.maps.iter() { let frames = &mr_name_to_frames[&map.mr]; @@ -881,12 +888,11 @@ pub fn build_capdl_spec( map_memory_region( &mut spec_container, kernel_config, - &virtual_machine.name, map, page_size_bytes, - vm_vspace_obj_id, + &vm_address_space, frames, - ); + )?; } if kernel_config.arch == Arch::X86_64 { diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index d8b0c7bd1..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 2aa1ec84c..242d081c8 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -306,14 +306,6 @@ impl SysIOMapPerms { (false, false) => Err(()), } } - - pub fn read(self) -> bool { - matches!(self, SysIOMapPerms::Read | SysIOMapPerms::ReadWrite) - } - - pub fn write(self) -> bool { - matches!(self, SysIOMapPerms::Write | SysIOMapPerms::ReadWrite) - } } #[derive(Debug, PartialEq, Eq, Clone)] @@ -327,13 +319,17 @@ pub struct SysIOMap { pub text_pos: Option, } -trait Map { +pub trait Map { fn mr_name(&self) -> &str; fn addr(&self) -> u64; fn text_pos(&self) -> Option; fn element(&self) -> &'static str; fn addr_name(&self) -> &'static str; fn range_name(&self) -> &'static str; + fn read(&self) -> bool; + fn write(&self) -> bool; + fn execute(&self) -> bool; + fn cached(&self) -> bool; } impl Map for SysMap { @@ -360,6 +356,22 @@ impl Map for SysMap { fn range_name(&self) -> &'static str { "virtual address range" } + + fn read(&self) -> bool { + self.perms & SysMapPerms::Read as u8 != 0 + } + + fn write(&self) -> bool { + self.perms & SysMapPerms::Write as u8 != 0 + } + + fn execute(&self) -> bool { + self.perms & SysMapPerms::Execute as u8 != 0 + } + + fn cached(&self) -> bool { + self.cached + } } impl Map for SysIOMap { @@ -386,7 +398,24 @@ impl Map for SysIOMap { fn range_name(&self) -> &'static str { "io address range" } + + fn read(&self) -> bool { + matches!(self.perms, SysIOMapPerms::Read | SysIOMapPerms::ReadWrite) + } + + fn write(&self) -> bool { + matches!(self.perms, SysIOMapPerms::Write | SysIOMapPerms::ReadWrite) + } + + fn execute(&self) -> bool { + false + } + + fn cached(&self) -> bool { + false + } } + #[derive(Debug, PartialEq, Eq, Clone)] pub enum SysMemoryRegionKind { User,