example: add bootinfo example

This adds an example showing how to map a bootinfo-prefilled
MR to a PD. As the DTB is not passed through by Microkit loader,
it isn't obvious to demonstrate the feature on ARM and RISC-V.

For x86, this example reads the TSC frequency and prints it.

Signed-off-by: Terry Bai <tianyi.bai@unsw.edu.au>

Author: terryzbai

example/bootinfo/Makefile

@@ -0,0 +1,80 @@
+#
+# 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),x86_64)
+	TARGET_TRIPLE := x86_64-linux-gnu
+	CFLAGS_ARCH := -march=x86-64 -mtune=generic
+  KERNEL := $(BOARD_DIR)//elf/sel4.elf
+  KERNEL_32B := $(BOARD_DIR)//elf/sel4_32.elf
+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 := bootinfo.elf
+CFLAGS := -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):
+	mkdir -p $@
+
+$(BUILD_DIR)/%.o: %.c Makefile | $(BUILD_DIR)
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.elf: $(BUILD_DIR)/%.o
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) bootinfo.system
+	$(MICROKIT_TOOL) bootinfo.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
+
+qemu: $(IMAGE_FILE) $(KERNEL_32B)
+ifeq ($(ARCH),x86_64)
+	qemu-system-x86_64                      \
+			-cpu qemu64,+fsgsbase,+pdpe1gb,+xsaveopt,+xsave \
+			-m "1G"                         \
+			-display none                   \
+			-serial mon:stdio               \
+		-kernel $(KERNEL_32B)             \
+		-initrd $(IMAGE_FILE)
+else
+$(error Unsupported ARCH)
+endif

example/bootinfo/README.md

@@ -0,0 +1,30 @@
+<!--
+     Copyright 2026, UNSW
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+# Example - Hello World
+
+This is a basic example that demonstrates how one can define
+a MemoryRegion prefilled with BootInfo and map it to a PD, so 
+the PD can read the BootInfo in userland.
+
+Supported BootInfo includes:
+- x86_vbe
+- x86_mbmap
+- x86_acpi_rsdp
+- x86_framebuffer
+- x86_tsc_freq
+
+As Microkit loader does not pass the DTB through on ARM and RISC-V, 
+so only x86 is supported in this example for now.
+
+## Building
+
+```sh
+mkdir build
+make BUILD_DIR=build MICROKIT_BOARD=<board> MICROKIT_CONFIG=<debug/release/benchmark> MICROKIT_SDK=/path/to/sdk qemu
+```
+
+## Running
+
+See instructions for your board in the manual.

example/bootinfo/bootinfo.c

@@ -0,0 +1,37 @@
+/*
+ * Copyright 2026, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stdint.h>
+#include <microkit.h>
+
+#if defined(CONFIG_ARCH_X86_64)
+typedef struct {
+    seL4_BootInfoHeader header;
+    uint32_t value;
+} bootinfo_tsc_freq_t;
+bootinfo_tsc_freq_t *bootinfo_tsc_freq;
+#else
+#error "No example cases for this architecture"
+#endif
+
+void init(void)
+{
+    microkit_dbg_puts("====BootInfo====\n");
+#if defined(CONFIG_ARCH_X86_64)
+    if (bootinfo_tsc_freq->header.len) {
+        microkit_dbg_puts("TSC Frequency: ");
+        microkit_dbg_put32(bootinfo_tsc_freq->value);
+        microkit_dbg_puts("MHz\n");
+    } else {
+        microkit_dbg_puts("TSC Frequency is not found or prefilled properly.\n");
+    }
+#else
+#error "No example cases for this architecture"
+#endif
+}
+
+void notified(microkit_channel ch)
+{
+}

example/bootinfo/bootinfo.system

@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <memory_region name="bootinfo_x86_tsc_freq" prefill_bootinfo="x86_tsc_freq" />
+    <protection_domain name="bootinfo">
+        <program_image path="bootinfo.elf" />
+        <map mr="bootinfo_x86_tsc_freq" vaddr="0x2_000_000" perms="r" cached="true" setvar_vaddr="bootinfo_tsc_freq" />
+    </protection_domain>
+</system>