Implement setvar region_paddr + setvar_addr and various fixes

build_sdk.py

@@ -774,7 +774,7 @@ def build_initialiser(
     else:
         capdl_init_elf = custom_rust_sel4_dir / "target" / cargo_target / "release" / "sel4-capdl-initializer.elf"
         cmd = f"""
-            cd {custom_rust_sel4_dir} && SEL4_PREFIX={sel4_src_dir.absolute()} {cargo_env} \
+            cd {custom_rust_sel4_dir} && SEL4_PREFIX={sel4_src_dir.absolute()} \
             cargo build {cargo_cross_options} --target {cargo_target} \
             --release -p sel4-capdl-initializer
         """

docs/manual.md

@@ -751,6 +751,7 @@ The `ioport` element has the following attributes:
 * `addr`: The base address of the I/O port.
 * `size`: The size in bytes of the I/O port region.
 * `setvar_id`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the I/O port identifier.
+* `setvar_addr`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the base address of the I/O port.
 
 The `setvar` element has the following attributes:
 

example/ethernet/ethernet.system

@@ -44,7 +44,7 @@
 
     <memory_region name="eth_clk" size="0x1_000" phys_addr="0x5b200000" />
 
-    <protection_domain name="gpt" priority="254">
+    <protection_domain name="gpt" priority="253">
         <program_image path="gpt.elf" />
         <map mr="lsio_gpt0" vaddr="0x2_000_000" perms="rw" cached="false" setvar_vaddr="gpt_regs" />
         <map mr="lsio_gpt0_clk" vaddr="0x2_200_000" perms="rw" cached="false" setvar_vaddr="gpt_regs_clk" />

example/hierarchy/hierarchy.system

@@ -5,9 +5,9 @@
  SPDX-License-Identifier: BSD-2-Clause
 -->
 <system>
-    <protection_domain name="restarter" priority="254">
+    <protection_domain name="restarter" priority="253">
         <program_image path="restarter.elf" />
-        <protection_domain name="crasher" priority="253" id="1">
+        <protection_domain name="crasher" priority="252" id="1">
             <program_image path="crasher.elf" />
         </protection_domain>
         <protection_domain name="hello" priority="1" id="2">

example/rust/rust.system

@@ -5,7 +5,7 @@
  SPDX-License-Identifier: BSD-2-Clause
 -->
 <system>
-    <protection_domain name="hello" priority="254">
+    <protection_domain name="hello" priority="253">
         <program_image path="hello.elf" />
     </protection_domain>
 </system>

example/setvar/Makefile

@@ -0,0 +1,58 @@
+#
+# Copyright 2025, UNSW.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+ifeq ($(strip $(BUILD_DIR)),)
+$(error BUILD_DIR must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_SDK)),)
+$(error MICROKIT_SDK must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_BOARD)),)
+$(error MICROKIT_BOARD must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_CONFIG)),)
+$(error MICROKIT_CONFIG must be specified)
+endif
+
+BOARD_DIR := $(MICROKIT_SDK)/board/$(MICROKIT_BOARD)/$(MICROKIT_CONFIG)
+
+ARCH := ${shell grep 'CONFIG_SEL4_ARCH  ' $(BOARD_DIR)/include/kernel/gen_config.h | cut -d' ' -f4}
+
+ifeq ($(ARCH),aarch64)
+	TOOLCHAIN := aarch64-none-elf
+	# No specific AArch64 flags
+	CFLAGS_ARCH :=
+else
+$(error Unsupported ARCH)
+endif
+
+CC := $(TOOLCHAIN)-gcc
+LD := $(TOOLCHAIN)-ld
+AS := $(TOOLCHAIN)-as
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
+
+SETVAR_OBJS := setvar.o
+
+IMAGES := setvar.elf
+CFLAGS := -mstrict-align -nostdlib -ffreestanding -g -O3 -Wall  -Wno-unused-function -Werror -I$(BOARD_DIR)/include $(CFLAGS_ARCH)
+LDFLAGS := -L$(BOARD_DIR)/lib
+LIBS := -lmicrokit -Tmicrokit.ld
+
+IMAGE_FILE = $(BUILD_DIR)/loader.img
+REPORT_FILE = $(BUILD_DIR)/report.txt
+
+all: $(IMAGE_FILE)
+
+$(BUILD_DIR)/%.o: %.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/setvar.elf: $(addprefix $(BUILD_DIR)/, $(SETVAR_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) setvar.system
+	$(MICROKIT_TOOL) setvar.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)

example/setvar/README.md

@@ -0,0 +1,21 @@
+<!--
+     Copyright 2025, UNSW
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+# Example - setvar
+
+This is a basic example that demonstrate how to use some `setvar` functionalities that the Microkit provides.
+
+Only QEMU virt (AArch64) is supported in this example. Although everything will work the same way on other
+platforms, but on x86-64 `<setvar region_paddr` won't be supported.
+
+## Building
+
+```sh
+mkdir build
+make BUILD_DIR=build MICROKIT_BOARD=qemu_virt_aarch64 MICROKIT_CONFIG=debug MICROKIT_SDK=/path/to/sdk
+```
+
+## Running
+
+See instructions for your board in the manual.

example/setvar/setvar.c

@@ -0,0 +1,40 @@
+/*
+ * Copyright 2025, UNSW.
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stdint.h>
+#include <microkit.h>
+
+uint64_t mr_with_paddr_vaddr;
+uint64_t mr_with_paddr_paddr;
+
+uint64_t small_mr_no_paddr_paddr;
+uint64_t large_mr_no_paddr_paddr;
+
+uint64_t pl011_paddr;
+
+void init(void)
+{
+    microkit_dbg_puts("Virtual address of 'mr_with_paddr': ");
+    microkit_dbg_put32(mr_with_paddr_vaddr);
+    microkit_dbg_puts("\n");
+    microkit_dbg_puts("Physical address of 'mr_with_paddr': ");
+    microkit_dbg_put32(mr_with_paddr_paddr);
+    microkit_dbg_puts("\n");
+
+    microkit_dbg_puts("Physical address of 'small_mr_no_paddr': ");
+    microkit_dbg_put32(small_mr_no_paddr_paddr);
+    microkit_dbg_puts("\n");
+    microkit_dbg_puts("Physical address of 'large_mr_no_paddr': ");
+    microkit_dbg_put32(large_mr_no_paddr_paddr);
+    microkit_dbg_puts("\n");
+
+    microkit_dbg_puts("Physical address of 'pl011_paddr': ");
+    microkit_dbg_put32(pl011_paddr);
+    microkit_dbg_puts("\n");
+}
+
+void notified(microkit_channel ch)
+{
+}

example/setvar/setvar.system

@@ -0,0 +1,27 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2025, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <!-- 0x900_0000 == 150994944 -->
+    <memory_region name="pl011" size="0x1000" phys_addr="0x900_0000" />
+
+    <!-- 0x8000_0000 == 2147483648 -->
+    <memory_region name="mr_with_paddr" size="0x1000" phys_addr="0x8000_0000" />
+
+    <memory_region name="small_mr_no_paddr" size="0x1000" />
+    <memory_region name="large_mr_no_paddr" size="0x200000" page_size="0x200000" />
+
+    <protection_domain name="setvar" priority="1">
+        <program_image path="setvar.elf" />
+
+        <!-- 0x2000_0000 == 536870912 -->
+        <map mr="mr_with_paddr" vaddr="0x2000_0000" setvar_vaddr="mr_with_paddr_vaddr" />
+        <setvar region_paddr="mr_with_paddr" symbol="mr_with_paddr_paddr" />
+        <setvar region_paddr="small_mr_no_paddr" symbol="small_mr_no_paddr_paddr" />
+        <setvar region_paddr="large_mr_no_paddr" symbol="large_mr_no_paddr_paddr" />
+        <setvar region_paddr="pl011" symbol="pl011_paddr" />
+    </protection_domain>
+</system>

example/x86_64_ioport/x86_64_ioport.c

@@ -6,13 +6,13 @@
 #include <stdint.h>
 #include <microkit.h>
 
-#define SERIAL_IOPORT_ID 0
-#define SERIAL_IOPORT_ADDRESS 0x3f8
+uint64_t com1_ioport_id;
+uint64_t com1_ioport_addr;
 
 static inline void serial_putc(char ch)
 {
     // Danger: may overflow hardware FIFO, but we are only writing a small message.
-    microkit_x86_ioport_write_8(SERIAL_IOPORT_ID, SERIAL_IOPORT_ADDRESS, ch);
+    microkit_x86_ioport_write_8(com1_ioport_id, com1_ioport_addr, ch);
 }
 
 static inline void serial_puts(const char *s)

example/x86_64_ioport/x86_64_ioport.system

@@ -7,6 +7,6 @@
 <system>
     <protection_domain name="x86_64_ioport" priority="100" >
         <program_image path="x86_64_ioport.elf" />
-        <ioport id="0" addr="0x3f8" size="8" />
+        <ioport id="0" addr="0x3f8" size="8" setvar_id="com1_ioport_id" setvar_addr="com1_ioport_addr"/>
     </protection_domain>
 </system>

tool/microkit/src/capdl/allocation.rs

@@ -13,6 +13,11 @@ use crate::{
     UntypedObject,
 };
 
+pub enum CapDLAllocEmulationErrorLevel {
+    Suppressed,
+    PrintStderr,
+}
+
 /// For the given spec and list of untypeds, simulate the CapDL initialiser's
 /// object allocation algorithm. Record each object's paddr and UT's index in
 /// its `expected_alloc` struct field. Assumes that the spec objects are sorted
@@ -23,6 +28,7 @@ pub fn simulate_capdl_object_alloc_algorithm(
     spec: &mut CapDLSpec,
     kernel_boot_info: &BootInfo,
     kernel_config: &Config,
+    error_reporting_level: CapDLAllocEmulationErrorLevel,
 ) -> bool {
     // Step 1: sort untypeds by paddr.
     // We don't want to mess with the original order in `kernel_boot_info` as we will patch
@@ -84,13 +90,23 @@ pub fn simulate_capdl_object_alloc_algorithm(
             if !(candidate_ut_range.start <= paddr_range.start
                 && candidate_ut_range.end >= paddr_range.end)
             {
-                eprintln!("ERROR: object '{}', with paddr 0x{:0>12x}..0x{:0>12x} is not in any valid memory region.", named_obj.name, paddr_range.start, paddr_range.end);
+                if matches!(
+                    error_reporting_level,
+                    CapDLAllocEmulationErrorLevel::PrintStderr
+                ) {
+                    eprintln!("ERROR: object '{}', with paddr 0x{:0>12x}..0x{:0>12x} is not in any valid memory region.", named_obj.name, paddr_range.start, paddr_range.end);
+                }
                 phys_addrs_ok = false;
             }
         }
     }
 
-    if !phys_addrs_ok {
+    if !phys_addrs_ok
+        && matches!(
+            error_reporting_level,
+            CapDLAllocEmulationErrorLevel::PrintStderr
+        )
+    {
         eprintln!("Below are the valid ranges of memory to be allocated from:");
         eprintln!("Valid ranges outside of main memory:");
         for (_i, ut) in untypeds_by_paddr.iter().filter(|(_i, ut)| ut.is_device) {
@@ -204,10 +220,15 @@ pub fn simulate_capdl_object_alloc_algorithm(
                 oom = true;
                 let shortfall = (obj_id_range.end - obj_id_range.start) as u64;
                 let individual_sz = (1 << size_bit) as u64;
-                eprintln!(
-                    "ERROR: ran out of untypeds for allocating objects of size {}, still need to create {} objects which requires {} of additional memory.",
-                    human_size_strict(individual_sz), shortfall, human_size_strict(individual_sz * shortfall)
-                );
+                if matches!(
+                    error_reporting_level,
+                    CapDLAllocEmulationErrorLevel::PrintStderr
+                ) {
+                    eprintln!(
+                        "ERROR: ran out of untypeds for allocating objects of size {}, still need to create {} objects which requires {} of additional memory.",
+                        human_size_strict(individual_sz), shortfall, human_size_strict(individual_sz * shortfall)
+                    );
+                }
             }
         }
     }

tool/microkit/src/capdl/builder.rs

@@ -488,7 +488,7 @@ pub fn build_capdl_spec(
 
         for frame_sequence in 0..mr.page_count {
             let paddr = mr
-                .phys_addr
+                .paddr()
                 .map(|base_paddr| (base_paddr + (frame_sequence * mr.page_size_bytes())) as usize);
             frame_ids.push(capdl_util_make_frame_obj(
                 &mut spec,

tool/microkit/src/capdl/initialiser.rs

@@ -18,20 +18,25 @@ const INITIALISER_HEAP_ADD_ON_CONSTANT: u64 = 16 * 4096;
 // Page size used for allocating the spec and heap segments.
 pub const INITIALISER_GRANULE_SIZE: PageSize = PageSize::Small;
 
+pub struct CapDLInitialiserSpecMetadata {
+    pub spec_size: u64,
+    pub heap_size: u64,
+}
+
 pub struct CapDLInitialiser {
     pub elf: ElfFile,
     pub heap_multiplier: f64,
-    pub spec_size: Option<u64>,
-    pub heap_size: Option<u64>,
+    pub phys_base: Option<u64>,
+    pub spec_metadata: Option<CapDLInitialiserSpecMetadata>,
 }
 
 impl CapDLInitialiser {
     pub fn new(elf: ElfFile, heap_multiplier: f64) -> CapDLInitialiser {
         CapDLInitialiser {
             elf,
             heap_multiplier,
-            spec_size: None,
-            heap_size: None,
+            phys_base: None,
+            spec_metadata: None,
         }
     }
 
@@ -40,7 +45,7 @@ impl CapDLInitialiser {
     }
 
     pub fn add_spec(&mut self, payload: Vec<u8>) {
-        if self.spec_size.is_some() || self.heap_size.is_some() {
+        if self.spec_metadata.is_some() {
             unreachable!("internal bug: CapDLInitialiser::add_spec() called more than once");
         }
 
@@ -104,17 +109,28 @@ impl CapDLInitialiser {
             )
             .unwrap();
 
-        self.spec_size = Some(spec_size);
-        self.heap_size = Some(heap_size);
+        self.spec_metadata = Some(CapDLInitialiserSpecMetadata {
+            spec_size,
+            heap_size,
+        });
+    }
+
+    pub fn spec_metadata(&self) -> &Option<CapDLInitialiserSpecMetadata> {
+        &self.spec_metadata
+    }
+
+    pub fn have_spec(&self) -> bool {
+        self.spec_metadata.is_some()
     }
 
     pub fn replace_spec(&mut self, new_payload: Vec<u8>) {
-        if self.spec_size.is_none() || self.heap_size.is_none() {
+        if self.spec_metadata.is_none() {
             unreachable!("internal bug: CapDLInitialiser::replace_spec() called when no spec have been added before");
         }
 
         self.elf.segments.pop();
         self.elf.segments.pop();
+        self.spec_metadata = None;
         self.add_spec(new_payload);
     }
 
@@ -134,4 +150,8 @@ impl CapDLInitialiser {
             .write_symbol("sel4_capdl_initializer_expected_untypeds_list", &uts_desc)
             .unwrap();
     }
+
+    pub fn set_phys_base(&mut self, phys_base: u64) {
+        self.phys_base = Some(phys_base);
+    }
 }

tool/microkit/src/capdl/mod.rs

@@ -9,9 +9,8 @@ pub mod builder;
 pub mod initialiser;
 mod irq;
 mod memory;
-pub mod reserialise_spec;
+pub mod packaging;
 pub mod spec;
 mod util;
 
 pub use self::builder::*;
-pub use self::reserialise_spec::*;