examples: add mr_prefill

Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

Author: dreamliner787-9

.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
 

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/fill.bin

@@ -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.c

@@ -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>