tool: create IPC buffer in the tool, not the ELF

This removes the need for the linker script to define the
IPC buffer.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

Author: midnightveil

libmicrokit/microkit.ld

@@ -66,9 +66,4 @@ SECTIONS
         . = ALIGN(4);
         _bss_end = .;
     } :data
-
-    . = ALIGN(0x1000);
-    .ipc_buffer (NOLOAD): {
-        __sel4_ipc_buffer_obj = .;
-    } :NONE
 }

libmicrokit/src/main.c

@@ -3,6 +3,7 @@
  *
  * SPDX-License-Identifier: BSD-2-Clause
  */
+#include <assert.h>
 #include <stdbool.h>
 #include <stddef.h>
 #include <stdint.h>
@@ -39,9 +40,19 @@ seL4_Word microkit_notifications;
 seL4_Word microkit_pps;
 seL4_Word microkit_ioports;
 
-extern seL4_IPCBuffer __sel4_ipc_buffer_obj;
+// Workaround: https://github.com/seL4/seL4/issues/1693
+#if seL4_UserTop == 0x00ffffffffff || seL4_UserTop == 0x0fffffffffff || seL4_UserTop == 0x7fffffffffff
+#define user_top_aligned (seL4_UserTop + 1)
+#elif (seL4_UserTop & ((1ULL << seL4_PageBits) - 1)) != 0
+#error "Expects seL4_UserTop to be aligned"
+#else
+#define user_top_aligned (seL4_UserTop)
+#endif
 
-seL4_IPCBuffer *__sel4_ipc_buffer = &__sel4_ipc_buffer_obj;
+/* The tool assumes the IPC buffer in the top page of user memory */
+seL4_IPCBuffer *__sel4_ipc_buffer = (seL4_IPCBuffer *)(user_top_aligned - (1ULL << seL4_PageBits));
+static_assert(sizeof(seL4_IPCBuffer) <= (1ULL << 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);

monitor/src/main.c

@@ -11,7 +11,7 @@
  *
  *   Acting as the fault handler for protection domains.
  */
-
+#include <assert.h>
 #include <stdbool.h>
 #include <stdint.h>
 #include <sel4/sel4.h>
@@ -29,8 +29,19 @@
 #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;
+// Workaround: https://github.com/seL4/seL4/issues/1693
+#if seL4_UserTop == 0x00ffffffffff || seL4_UserTop == 0x0fffffffffff || seL4_UserTop == 0x7fffffffffff
+#define user_top_aligned (seL4_UserTop + 1)
+#elif (seL4_UserTop & ((1ULL << seL4_PageBits) - 1)) != 0
+#error "Expects seL4_UserTop to be aligned"
+#else
+#define user_top_aligned (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_aligned - (1ULL << seL4_PageBits));
+static_assert(sizeof(seL4_IPCBuffer) <= (1ULL << 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;

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;
 
@@ -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");
+
     // 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,
@@ -638,17 +622,27 @@ pub fn build_capdl_spec(
             // 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));
+            let pd_reserved_range =
+                kernel_config.pd_map_max_vaddr(pd.stack_size)..kernel_config.user_top();
+            if ranges_overlap(&mr_vaddr_range, &pd_reserved_range) {
+                return Err(
+                    format!(
+                        "ERROR: mapping MR '{}' to PD '{}' with vaddr [0x{:x}..0x{:x}) will overlap with the PD reserved range at [0x{:x}..0x{:x})",
+                        map.mr, pd.name, mr_vaddr_range.start, mr_vaddr_range.end, pd_reserved_range.start, pd_reserved_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 +657,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");
+        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 +1046,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;

tool/microkit/src/sel4.rs

@@ -310,16 +310,18 @@ pub struct Config {
 }
 
 impl Config {
-    /// Refers to 'seL4_UserTop'
+    /// Refers to 'seL4_UserTop'. Is exclusive.
     pub fn user_top(&self) -> u64 {
         match self.arch {
+            // Almost the same as the true definition, but for an inconsistency
+            // TODO: Resolve https://github.com/seL4/seL4/issues/1693
             Arch::Aarch64 => match self.hypervisor {
                 true => match self.arm_pa_size_bits.unwrap() {
-                    40 => 0x10000000000,
-                    44 => 0x100000000000,
+                    40 => 0x00ffffffffff + 1,
+                    44 => 0x0fffffffffff + 1,
                     _ => panic!("Unknown ARM physical address size bits"),
                 },
-                false => 0x800000000000,
+                false => 0x7fffffffffff + 1,
             },
             Arch::Riscv64 => 0x0000003ffffff000,
             Arch::X86_64 => 0x7ffffffff000,
@@ -346,22 +348,26 @@ impl Config {
         }
     }
 
+    /// IPC Buffer is located at the highest possible virtual memory page
+    pub fn pd_ipc_buffer(&self) -> u64 {
+        self.user_top() - PageSize::Small as u64
+    }
+
+    /// 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.
     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)
     }
 

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'",
         )
     }