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

.github/workflows/sdk.yaml

@@ -19,7 +19,7 @@ on:
       - '*.*.*'
 
 env:
-  SEL4_VERSION: e912dff7341cf3b35475c3a7eee9a90c61b367a8
+  SEL4_VERSION: c8526a426f150bc11474ef21449efd87c5b8b6e3
 
 # To reduce the load we cancel any older runs of this workflow for the current
 # PR. For deployment to the main branch, the workflow will run on each push,

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

@@ -39,9 +39,13 @@ 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;
+/* The tool assumes the IPC buffer in the top page of user memory */
+seL4_IPCBuffer *__sel4_ipc_buffer = (seL4_IPCBuffer *)(seL4_UserVSpaceTop & ~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);

monitor/src/main.c

@@ -29,8 +29,13 @@
 #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)
+
+/* The tool assumes the IPC buffer in the top page of user memory */
+seL4_IPCBuffer *__sel4_ipc_buffer = (seL4_IPCBuffer *)(seL4_UserVSpaceTop & ~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;

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;
 
@@ -187,8 +184,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.
@@ -293,47 +290,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,
@@ -348,11 +309,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),
         };
 
@@ -486,6 +443,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.
@@ -495,6 +473,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
@@ -503,6 +482,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,
@@ -632,21 +616,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,
+                        )
+                    );
                 }
             }
 
@@ -661,7 +644,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;
@@ -1043,6 +1051,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,19 +310,20 @@ pub struct Config {
 }
 
 impl Config {
-    /// Refers to 'seL4_UserTop'
-    pub fn user_top(&self) -> u64 {
+    /// Refers to 'seL4_UserVSpaceTop'. Is inclusive.
+    // TODO: We should auto-extract this from libsel4 headers.
+    pub fn user_vspace_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 => 0x0000003fffffefff,
+            Arch::X86_64 => 0x7fffffffefff,
         }
     }
 
@@ -346,30 +347,38 @@ 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_vspace_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_UserVSpaceTop.
+    /// 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_vspace_top() + 1
     }
 
     pub fn paddr_to_kernel_vaddr(&self, paddr: u64) -> u64 {

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