diff --git a/libmicrokit/microkit.ld b/libmicrokit/microkit.ld index 8604370fe..8d246e477 100644 --- a/libmicrokit/microkit.ld +++ b/libmicrokit/microkit.ld @@ -66,9 +66,4 @@ SECTIONS . = ALIGN(4); _bss_end = .; } :data - - . = ALIGN(0x1000); - .ipc_buffer (NOLOAD): { - __sel4_ipc_buffer_obj = .; - } :NONE } diff --git a/libmicrokit/src/main.c b/libmicrokit/src/main.c index 8719d4950..d516fa19c 100644 --- a/libmicrokit/src/main.c +++ b/libmicrokit/src/main.c @@ -39,9 +39,20 @@ seL4_Word microkit_notifications; seL4_Word microkit_pps; seL4_Word microkit_ioports; -extern seL4_IPCBuffer __sel4_ipc_buffer_obj; +#define BIT(n) (1ULL << (n)) +#define MASK(n) (BIT(n) - 1ULL) -seL4_IPCBuffer *__sel4_ipc_buffer = &__sel4_ipc_buffer_obj; +// Workaround: https://github.com/seL4/seL4/issues/1693 +#if (seL4_UserTop & MASK(seL4_PageBits)) == 0 +#define user_top_inclusive (seL4_UserTop - 1) +#else +#define user_top_inclusive (seL4_UserTop) +#endif + +/* The tool assumes the IPC buffer in the top page of user memory */ +seL4_IPCBuffer *__sel4_ipc_buffer = (seL4_IPCBuffer *)(user_top_inclusive & ~MASK(seL4_PageBits)); +_Static_assert(sizeof(seL4_IPCBuffer) <= BIT(seL4_PageBits), + "IPC Buffer is expected to need less than one page in size"); extern const void (*const __init_array_start [])(void); extern const void (*const __init_array_end [])(void); diff --git a/monitor/src/main.c b/monitor/src/main.c index 028600477..e7e373a92 100644 --- a/monitor/src/main.c +++ b/monitor/src/main.c @@ -29,8 +29,20 @@ #define BASE_SCHED_CONTEXT_CAP 138 #define BASE_NOTIFICATION_CAP 202 -extern seL4_IPCBuffer __sel4_ipc_buffer_obj; -seL4_IPCBuffer *__sel4_ipc_buffer = &__sel4_ipc_buffer_obj; +#define BIT(n) (1ULL << (n)) +#define MASK(n) (BIT(n) - 1ULL) + +// Workaround: https://github.com/seL4/seL4/issues/1693 +#if (seL4_UserTop & MASK(seL4_PageBits)) == 0 +#define user_top_inclusive (seL4_UserTop - 1) +#else +#define user_top_inclusive (seL4_UserTop) +#endif + +/* The tool assumes the IPC buffer in the top page of user memory */ +seL4_IPCBuffer *__sel4_ipc_buffer = (seL4_IPCBuffer *)(user_top_inclusive & ~MASK(seL4_PageBits)); +_Static_assert(sizeof(seL4_IPCBuffer) <= BIT(seL4_PageBits), + "IPC Buffer is expected to need less than one page in size"); char pd_names[MAX_PDS][MAX_NAME_LEN]; seL4_Word pd_names_len; diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 5bb401be0..379487cfc 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -31,9 +31,6 @@ use crate::{ util::{ranges_overlap, round_down, round_up}, }; -// Corresponds to the IPC buffer symbol in libmicrokit and the monitor -const SYMBOL_IPC_BUFFER: &str = "__sel4_ipc_buffer_obj"; - const FAULT_BADGE: u64 = 1 << 62; const PPC_BADGE: u64 = 1 << 63; @@ -189,8 +186,8 @@ impl CapDLSpecContainer { /// Add the details of the given ELF into the given CapDL spec while inferring as much information /// as possible. These are the objects that will be created: - /// -> TCB: PC, SP and IPC buffer vaddr set. VSpace and IPC buffer frame caps bound. - /// -> VSpace: all ELF loadable pages and IPC buffer mapped in. + /// -> TCB: Program counter set and VSpace capability bound. + /// -> VSpace: all pages from the ELF mapped in. /// Returns the object ID of the TCB /// 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. @@ -295,47 +292,11 @@ impl CapDLSpecContainer { } } - // Create and map the IPC buffer for this ELF - let ipcbuf_frame_obj_id = capdl_util_make_frame_obj( - self, - Fill { - entries: [].to_vec(), - }, - &format!("ipcbuf_{pd_name}"), - None, - PageSize::Small.fixed_size_bits(sel4_config) as u8, - ); - let ipcbuf_frame_cap = - capdl_util_make_frame_cap(ipcbuf_frame_obj_id, true, true, false, true); - // We need to clone the IPC buf cap because in addition to mapping the frame into the VSpace, we need to bind - // this frame to the TCB as well. - let ipcbuf_frame_cap_for_tcb = ipcbuf_frame_cap.clone(); - let ipcbuf_vaddr = elf - .find_symbol(SYMBOL_IPC_BUFFER) - .unwrap_or_else(|_| panic!("Could not find {SYMBOL_IPC_BUFFER}")) - .0; - match map_page( - self, - sel4_config, - pd_name, - vspace_obj_id, - ipcbuf_frame_cap, - PageSize::Small as u64, - ipcbuf_vaddr, - ) { - Ok(_) => {} - Err(map_err_reason) => { - return Err(format!( - "build_capdl_spec(): failed to map ipc buffer frame to {pd_name} because: {map_err_reason}" - )) - } - }; - let tcb_name = format!("tcb_{pd_name}"); let entry_point = elf.entry; let tcb_extra_info = object::TcbExtraInfo { - ipc_buffer_addr: ipcbuf_vaddr.into(), + ipc_buffer_addr: 0.into(), affinity: Word(pd_cpu.0.into()), prio: 0, max_prio: 0, @@ -350,11 +311,7 @@ impl CapDLSpecContainer { let tcb_inner_obj = object::Tcb { // Bind the VSpace into the TCB - slots: [ - capdl_util_make_cte(TcbBoundSlot::VSpace as u32, vspace_cap), - capdl_util_make_cte(TcbBoundSlot::IpcBuffer as u32, ipcbuf_frame_cap_for_tcb), - ] - .to_vec(), + slots: vec![capdl_util_make_cte(TcbBoundSlot::VSpace as u32, vspace_cap)], extra: Box::new(tcb_extra_info), }; @@ -488,6 +445,27 @@ pub fn build_capdl_spec( ) .unwrap(); + // Create monitor IPC Bufffer + let mon_ipcbuf_frame_obj_id = capdl_util_make_frame_obj( + &mut spec_container, + Fill { entries: vec![] }, + &format!("ipcbuf_{MONITOR_PD_NAME}"), + None, + PageSize::Small.fixed_size_bits(kernel_config) as u8, + ); + 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"); + // 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. // In addition, `add_elf_to_spec()` doesn't fill most the details in the TCB. @@ -497,6 +475,7 @@ pub fn build_capdl_spec( .unwrap() .object { + monitor_tcb.extra.ipc_buffer_addr = Word(kernel_config.pd_ipc_buffer()); // Special case, monitor has its stack statically allocated. monitor_tcb.extra.sp = Word(kernel_config.pd_stack_top()); // While there is nothing stopping us from running the monitor at the highest priority alongside the @@ -505,6 +484,11 @@ pub fn build_capdl_spec( monitor_tcb.extra.max_prio = MONITOR_PRIORITY; monitor_tcb.extra.resume = true; + monitor_tcb.slots.push(capdl_util_make_cte( + TcbBoundSlot::IpcBuffer as u32, + mon_ipcbuf_frame_cap, + )); + monitor_tcb.slots.push(capdl_util_make_cte( TcbBoundSlot::CSpace as u32, mon_cnode_cap, @@ -634,21 +618,20 @@ pub fn build_capdl_spec( 1 << capdl_util_get_frame_size_bits(&spec_container, *frames.first().unwrap()); // sdf.rs sanity checks that the memory regions doesn't overlap with each others, etc. - // But it doesn't actually check for whether they overlap with a PD's stack or ELF segments. + // But it doesn't actually check for whether they overlap with a PD's ELF segments. // We perform this check here, otherwise the tool will panic with quite cryptic page-table related errors. let mr_vaddr_range = map.vaddr..(map.vaddr + (page_size_bytes * frames.len() as u64)); - let pd_stack_range = - kernel_config.pd_stack_bottom(pd.stack_size)..kernel_config.pd_stack_top(); - if ranges_overlap(&mr_vaddr_range, &pd_stack_range) { - return Err(format!("ERROR: mapping MR '{}' to PD '{}' with vaddr [0x{:x}..0x{:x}) will overlap with the stack at [0x{:x}..0x{:x})", map.mr, pd.name, mr_vaddr_range.start, mr_vaddr_range.end, pd_stack_range.start, pd_stack_range.end)); - } - for elf_seg in elf_obj.loadable_segments().iter() { let elf_seg_vaddr_range = elf_seg.virt_addr ..elf_seg.virt_addr + round_up(elf_seg.mem_size(), PageSize::Small as u64); if ranges_overlap(&mr_vaddr_range, &elf_seg_vaddr_range) { - return Err(format!("ERROR: mapping MR '{}' to PD '{}' with vaddr [0x{:x}..0x{:x}) will overlap with an ELF segment at [0x{:x}..0x{:x})", map.mr, pd.name, mr_vaddr_range.start, mr_vaddr_range.end, elf_seg_vaddr_range.start, elf_seg_vaddr_range.end)); + return Err( + format!( + "ERROR: mapping MR '{}' to PD '{}' with vaddr [0x{:x}..0x{:x}) will overlap with an ELF segment at [0x{:x}..0x{:x})", + map.mr, pd.name, mr_vaddr_range.start, mr_vaddr_range.end, elf_seg_vaddr_range.start, elf_seg_vaddr_range.end, + ) + ); } } @@ -663,7 +646,32 @@ pub fn build_capdl_spec( ); } - // Step 3-3: Create and map in the stack (bottom up) + // Step 3-3a: Create and map in the IPC buffer + let ipcbuf_frame_obj_id = capdl_util_make_frame_obj( + &mut spec_container, + Fill { entries: vec![] }, + &format!("ipcbuf_{}", pd.name), + None, + PageSize::Small.fixed_size_bits(kernel_config) as u8, + ); + 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"); + caps_to_bind_to_tcb.push(capdl_util_make_cte( + TcbBoundSlot::IpcBuffer as u32, + ipcbuf_frame_cap, + )); + + // Step 3-3b: Create and map in the stack (bottom up) let mut cur_stack_vaddr = kernel_config.pd_stack_bottom(pd.stack_size); pd_stack_bottoms.push(cur_stack_vaddr); let num_stack_frames = pd.stack_size / PageSize::Small as u64; @@ -1027,6 +1035,7 @@ pub fn build_capdl_spec( .unwrap() .object { + pd_tcb.extra.ipc_buffer_addr = Word(kernel_config.pd_ipc_buffer()); pd_tcb.extra.sp = Word(kernel_config.pd_stack_top()); pd_tcb.extra.master_fault_ep = None; // Not used on MCS kernel. pd_tcb.extra.prio = pd.priority; diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index 641fa63c6..bceb795a6 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -310,19 +310,21 @@ pub struct Config { } impl Config { - /// Refers to 'seL4_UserTop' + /// Refers to 'seL4_UserTop'. Is inclusive. + // TODO: Resolve https://github.com/seL4/seL4/issues/1693 (RISC-V/X86) + // TODO: We should auto-extract this from libsel4 headers. pub fn user_top(&self) -> u64 { match self.arch { Arch::Aarch64 => match self.hypervisor { true => match self.arm_pa_size_bits.unwrap() { - 40 => 0x10000000000, - 44 => 0x100000000000, + 40 => 0x00ffffffffff, + 44 => 0x0fffffffffff, _ => panic!("Unknown ARM physical address size bits"), }, - false => 0x800000000000, + false => 0x7fffffffffff, }, - Arch::Riscv64 => 0x0000003ffffff000, - Arch::X86_64 => 0x7ffffffff000, + Arch::Riscv64 => 0x0000003ffffff000 - 1, + Arch::X86_64 => 0x7ffffffff000 - 1, } } @@ -346,30 +348,39 @@ impl Config { } } + /// IPC Buffer is located at the highest possible virtual memory page + pub fn pd_ipc_buffer(&self) -> u64 { + // user_top is inclusive, so we mask off the bits inside the page. + // self.user_top() & !util::mask(PageSize::Small.fixed_size_bits(self)) + self.user_top() & !(PageSize::Small as u64 - 1) + } + + /// The stack is located in the third highest possible virtual memory pages, + /// as the IPC buffer lives in the top, and we add a guard page inbetween. pub fn pd_stack_top(&self) -> u64 { - self.user_top() + // Subtract off the guard page. + self.pd_ipc_buffer() - PageSize::Small as u64 } pub fn pd_stack_bottom(&self, stack_size: u64) -> u64 { self.pd_stack_top() - stack_size } - /// For simplicity and consistency, the stack of each PD occupies the highest - /// possible virtual memory region. That means that the highest possible address - /// for a user to be able to create a mapping at is below the stack region. + /// For simplicity and consistency, the stack & IPC buffers of each PD + /// occupy the highest memory regions near seL4_UserTop. + /// So the maximum vaddr allowed for mapping is the stack bottom. + /// Value is exclusive ..max) pub fn pd_map_max_vaddr(&self, stack_size: u64) -> u64 { - // This function depends on the invariant that the stack of a PD - // consumes the highest possible address of the virtual address space. - assert!(self.pd_stack_top() == self.user_top()); - self.pd_stack_bottom(stack_size) } - /// Unlike PDs, virtual machines do not have a stack and so the max virtual - /// address of a mapping is whatever seL4 chooses as the maximum virtual address - /// in a VSpace. + /// Unlike PDs, virtual machines do not have a stack or IPC buffer and so + /// the max virtual address of a mapping is whatever seL4 chooses as the + /// maximum virtual address in a VSpace. + /// Value is exclusive ..max) pub fn vm_map_max_vaddr(&self) -> u64 { - self.user_top() + // Add 1, because user_top is inclusive. Note this assumes no overflow. + self.user_top() + 1 } pub fn paddr_to_kernel_vaddr(&self, paddr: u64) -> u64 { diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 1c5046ebb..f7595c278 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -1007,7 +1007,7 @@ mod system { check_error( &DEFAULT_AARCH64_KERNEL_CONFIG, "sys_map_too_high.system", - "Error: vaddr (0x1000000000000000) must be less than 0xffffffe000 on element 'map'", + "Error: vaddr (0x1000000000000000) must be less than 0xffffffc000 on element 'map'", ) }