Add support for prefilling memory regions from data files at compile time

.reuse/dep5

@@ -14,6 +14,7 @@ Files:
   VERSION
   docs/assets/microkit_flow.svg
   docs/assets/microkit_flow.pdf
+  example/mr_prefill/fill.bin
 Copyright: 2024, UNSW
 License: BSD-2-Clause
 

docs/manual.md

@@ -236,6 +236,16 @@ The mapping has a number of attributes, which include:
 **Note:** When a memory region is mapped into multiple protection
 domains, the attributes used for different mappings may vary.
 
+### Prefilling
+
+A *memory region* may be prefilled with data from a file at build time
+by specifying the file's name in the [System Description File]{#sysdesc}.
+
+In this case, specifying the memory region's size become optional. If
+a size isn't specified, the memory region will be sized by the length
+of the prefill file, rounded up to the smallest page size or the user
+specified page size.
+
 ## Channels {#channels}
 
 A *channel* enables two protection domains to interact using protected procedures or notifications.
@@ -1009,6 +1019,7 @@ The `map` element has the following attributes:
 * `cached`: (optional) Determines if mapped with caching enabled or disabled. Defaults to `true`.
 * `setvar_vaddr`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the virtual address of the memory region.
 * `setvar_size`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the size of the memory region.
+* `setvar_prefill_size`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the size of the prefilled data.
 
 The `irq` element has the following attributes on ARM and RISC-V:
 
@@ -1084,6 +1095,7 @@ It supports the following attributes:
 * `size`: Size of the memory region in bytes (must be a multiple of the page size)
 * `page_size`: (optional) Size of the pages used in the memory region; must be a supported page size if provided. Defaults to the largest page size for the target architecture that the memory region is aligned to.
 * `phys_addr`: (optional) The physical address for the start of the memory region (must be a multiple of the page size).
+* `prefill_path`: (optional) Path to a file containing data that the memory region will be filled with at boot.
 
 The `memory_region` element does not support any child elements.
 

example/mr_prefill/Makefile

@@ -0,0 +1,68 @@
+#
+# Copyright 2026, 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)
+  TARGET_TRIPLE := aarch64-none-elf
+  CFLAGS_ARCH := -mstrict-align
+else ifeq ($(ARCH),riscv64)
+  TARGET_TRIPLE := riscv64-unknown-elf
+  CFLAGS_ARCH := -march=rv64imafdc_zicsr_zifencei -mabi=lp64d
+else ifeq ($(ARCH),x86_64)
+	TARGET_TRIPLE := x86_64-linux-gnu
+	CFLAGS_ARCH := -march=x86-64 -mtune=generic
+else
+$(error Unsupported ARCH)
+endif
+
+ifeq ($(strip $(LLVM)),True)
+  CC := clang -target $(TARGET_TRIPLE)
+  AS := clang -target $(TARGET_TRIPLE)
+  LD := ld.lld
+else
+  CC := $(TARGET_TRIPLE)-gcc
+  LD := $(TARGET_TRIPLE)-ld
+  AS := $(TARGET_TRIPLE)-as
+endif
+
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
+
+IMAGES := mr_prefill.elf
+CFLAGS := -nostdlib -ffreestanding -g3 -O3 -I$(BOARD_DIR)/include $(CFLAGS_ARCH)
+LDFLAGS := -L$(BOARD_DIR)/lib -z noexecstack
+LIBS := -lmicrokit -Tmicrokit.ld
+
+IMAGE_FILE = $(BUILD_DIR)/loader.img
+REPORT = $(BUILD_DIR)/report.txt
+
+all: $(IMAGE_FILE)
+
+$(BUILD_DIR)/mr_prefill.o: mr_prefill.c Makefile
+	$(CC) -c $(CFLAGS) -Wall -Wno-unused-function -Werror $< -o $@
+
+$(BUILD_DIR)/mr_prefill.elf: $(BUILD_DIR)/mr_prefill.o
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) mr_prefill.system
+	$(MICROKIT_TOOL) mr_prefill.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT)

example/mr_prefill/README.md

@@ -0,0 +1,20 @@
+<!--
+     Copyright 2026, UNSW
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+# Example - Memory Region Prefill
+
+This is an example demostrating prefilling a memory region from a data file at compile time.
+
+All Microkit platforms are supported.
+
+## Building
+
+```sh
+mkdir build
+make BUILD_DIR=build MICROKIT_BOARD=<board> MICROKIT_CONFIG=<debug/release/benchmark> MICROKIT_SDK=/path/to/sdk
+```
+
+## Running
+
+See instructions for your board in the manual.

example/mr_prefill/mr_prefill.c

@@ -0,0 +1,85 @@
+/*
+ * Copyright 2026, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stdint.h>
+#include <microkit.h>
+
+#define BEGIN_MAGIC 0x53145314
+#define VALUE_A     0x01234567
+#define VALUE_B     0x89ABCDEF
+#define END_MAGIC   0x75757575
+
+typedef struct __attribute__((packed)) fill_data {
+    uint32_t begin_magic;
+    uint32_t value_a;
+    uint8_t _padding1[0x400];
+    uint32_t value_b;
+    uint8_t _padding2[0xc00];
+    uint32_t end_magic;
+} fill_data_t;
+
+fill_data_t *filled_mr;
+uint64_t filled_mr_data_size;
+
+void init(void)
+{
+    microkit_dbg_puts("hello, world. my name is ");
+    microkit_dbg_puts(microkit_name);
+    microkit_dbg_puts("\n");
+
+    microkit_dbg_puts("checking prefilled memory region data length\n");
+    if (filled_mr_data_size != sizeof(fill_data_t)) {
+        microkit_dbg_puts("oh no prefilled data length doesn't match: ");
+        microkit_dbg_put32(filled_mr_data_size);
+        microkit_dbg_puts(" != ");
+        microkit_dbg_put32(sizeof(fill_data_t));
+        microkit_dbg_puts("\n");
+        return;
+    }
+
+    microkit_dbg_puts("checking prefilled memory region data\n");
+
+    if (filled_mr->begin_magic != BEGIN_MAGIC) {
+        microkit_dbg_puts("oh no begin magic doesn't match: ");
+        microkit_dbg_put32(filled_mr->begin_magic);
+        microkit_dbg_puts(" != ");
+        microkit_dbg_put32(BEGIN_MAGIC);
+        microkit_dbg_puts("\n");
+        return;
+    }
+
+    if (filled_mr->value_a != VALUE_A) {
+        microkit_dbg_puts("oh no value A doesn't match: ");
+        microkit_dbg_put32(filled_mr->value_a);
+        microkit_dbg_puts(" != ");
+        microkit_dbg_put32(VALUE_A);
+        microkit_dbg_puts("\n");
+        return;
+    }
+
+    if (filled_mr->value_b != VALUE_B) {
+        microkit_dbg_puts("oh no value B doesn't match: ");
+        microkit_dbg_put32(filled_mr->value_b);
+        microkit_dbg_puts(" != ");
+        microkit_dbg_put32(VALUE_B);
+        microkit_dbg_puts("\n");
+        return;
+    }
+
+    if (filled_mr->end_magic != END_MAGIC) {
+        microkit_dbg_puts("oh no end magic doesn't match: ");
+        microkit_dbg_put32(filled_mr->end_magic);
+        microkit_dbg_puts(" != ");
+        microkit_dbg_put32(END_MAGIC);
+        microkit_dbg_puts("\n");
+        return;
+    }
+
+    microkit_dbg_puts("prefilled data OK!\n");
+}
+
+void notified(microkit_channel ch)
+{
+}

example/mr_prefill/mr_prefill.system

@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <memory_region name="prefilled" prefill_path="fill.bin" />
+
+    <protection_domain name="mr_prefill" priority="100" >
+        <program_image path="mr_prefill.elf" />
+
+        <map mr="prefilled" vaddr="0x20000000" setvar_vaddr="filled_mr" setvar_prefill_size="filled_mr_data_size"/>
+    </protection_domain>
+</system>

tool/microkit/src/capdl/builder.rs

@@ -19,7 +19,7 @@ use crate::{
     capdl::{
         irq::create_irq_handler_cap,
         memory::{create_vspace, create_vspace_ept, map_page},
-        spec::{capdl_obj_physical_size_bits, ElfContent},
+        spec::{capdl_obj_physical_size_bits, BytesContent, ElfContent, FillContent},
         util::*,
     },
     elf::ElfFile,
@@ -104,7 +104,7 @@ const PD_SCHEDCONTEXT_EXTRA_SIZE_BITS: u64 = PD_SCHEDCONTEXT_EXTRA_SIZE.ilog2()
 pub const SLOT_BITS: u64 = 5;
 pub const SLOT_SIZE: u64 = 1 << SLOT_BITS;
 
-pub type FrameFill = Fill<ElfContent>;
+pub type FrameFill = Fill<FillContent>;
 pub type CapDLNamedObject = NamedObject<FrameFill>;
 
 pub struct ExpectedAllocation {
@@ -230,12 +230,12 @@ impl CapDLSpecContainer {
                             start: dest_offset,
                             end: dest_offset + len_to_cpy,
                         },
-                        content: FillEntryContent::Data(ElfContent {
+                        content: FillEntryContent::Data(FillContent::ElfContent(ElfContent {
                             elf_id,
                             elf_seg_idx: seg_idx,
                             elf_seg_data_range: (section_offset as usize
                                 ..((section_offset + len_to_cpy) as usize)),
-                        }),
+                        })),
                     });
                 }
 
@@ -510,11 +510,39 @@ pub fn build_capdl_spec(
             let paddr = mr
                 .paddr()
                 .map(|base_paddr| Word(base_paddr + (frame_sequence * mr.page_size_bytes())));
+
+            let frame_fill = if let Some(prefill_bytes) = &mr.prefill_bytes {
+                let starting_byte_idx = frame_sequence * mr.page_size_bytes();
+                let remaining_bytes_to_fill = prefill_bytes.len() as u64 - starting_byte_idx;
+                let num_bytes_to_fill = min(mr.page_size_bytes(), remaining_bytes_to_fill);
+
+                let mut frame_bytes = vec![];
+                frame_bytes.extend_from_slice(
+                    &prefill_bytes[starting_byte_idx as usize
+                        ..(starting_byte_idx + num_bytes_to_fill) as usize],
+                );
+
+                FrameFill {
+                    entries: [FillEntry {
+                        range: Range {
+                            start: 0,
+                            end: num_bytes_to_fill,
+                        },
+                        content: FillEntryContent::Data(FillContent::BytesContent(BytesContent {
+                            bytes: frame_bytes,
+                        })),
+                    }]
+                    .to_vec(),
+                }
+            } else {
+                FrameFill {
+                    entries: [].to_vec(),
+                }
+            };
+
             frame_ids.push(capdl_util_make_frame_obj(
                 &mut spec_container,
-                Fill {
-                    entries: [].to_vec(),
-                },
+                frame_fill,
                 &format!("mr_{}_{:09}", mr.name, frame_sequence),
                 paddr,
                 frame_size_bits as u8,

tool/microkit/src/capdl/packaging.rs

@@ -5,7 +5,7 @@
 //
 
 use crate::{
-    capdl::{initialiser::CapDLInitialiser, CapDLSpecContainer},
+    capdl::{initialiser::CapDLInitialiser, spec::FillContent, CapDLSpecContainer},
     elf::ElfFile,
     sel4::{Config, PageSize},
 };
@@ -23,10 +23,19 @@ pub fn pack_spec_into_initial_task(
     let (mut output_spec, embedded_frame_data_list) = spec_container.spec.embed_fill(
         PageSize::Small.fixed_size_bits(sel4_config) as u8,
         |_| embed_frames,
-        |d, buf| {
-            buf.copy_from_slice(
-                &system_elfs[d.elf_id].segments[d.elf_seg_idx].data()[d.elf_seg_data_range.clone()],
-            );
+        |d, buf: &mut [u8]| {
+            match d {
+                FillContent::ElfContent(elf_content) => {
+                    buf.copy_from_slice(
+                        &system_elfs[elf_content.elf_id].segments[elf_content.elf_seg_idx].data()
+                            [elf_content.elf_seg_data_range.clone()],
+                    );
+                }
+                FillContent::BytesContent(bytes_content) => {
+                    buf.copy_from_slice(&bytes_content.bytes);
+                }
+            }
+
             compress_frames
         },
     );

tool/microkit/src/capdl/spec.rs

@@ -21,6 +21,17 @@ pub struct ElfContent {
     pub elf_seg_data_range: Range<usize>,
 }
 
+#[derive(Clone, Serialize)]
+pub struct BytesContent {
+    pub bytes: Vec<u8>,
+}
+
+#[derive(Clone, Serialize)]
+pub enum FillContent {
+    ElfContent(ElfContent),
+    BytesContent(BytesContent),
+}
+
 /// CNode and SchedContext are quirky as they have variable size.
 pub fn capdl_obj_physical_size_bits(obj: &Object<FrameFill>, sel4_config: &Config) -> u64 {
     match obj {