diff --git a/Cargo.lock b/Cargo.lock index 89b1b0de7..d26baff5b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -494,7 +494,7 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "sel4" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "cfg-if", "sel4-config", @@ -504,7 +504,7 @@ dependencies = [ [[package]] name = "sel4-alloca" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "cfg-if", ] @@ -512,7 +512,7 @@ dependencies = [ [[package]] name = "sel4-bitfield-ops" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "rustversion", ] @@ -520,12 +520,12 @@ dependencies = [ [[package]] name = "sel4-build-env" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" [[package]] name = "sel4-capdl-initializer" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "log", "rkyv", @@ -543,7 +543,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "miniz_oxide", "rkyv", @@ -555,7 +555,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types-derive" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "proc-macro2", "quote", @@ -565,7 +565,7 @@ dependencies = [ [[package]] name = "sel4-config" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "prettyplease", "proc-macro2", @@ -579,7 +579,7 @@ dependencies = [ [[package]] name = "sel4-config-data" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "sel4-build-env", "sel4-config-types", @@ -589,7 +589,7 @@ dependencies = [ [[package]] name = "sel4-config-macros" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "fallible-iterator", "proc-macro2", @@ -602,7 +602,7 @@ dependencies = [ [[package]] name = "sel4-config-types" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "serde", ] @@ -610,12 +610,12 @@ dependencies = [ [[package]] name = "sel4-ctors-dtors" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" [[package]] name = "sel4-dlmalloc" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "dlmalloc", "lock_api", @@ -624,17 +624,17 @@ dependencies = [ [[package]] name = "sel4-immediate-sync-once-cell" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" [[package]] name = "sel4-immutable-cell" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" [[package]] name = "sel4-initialize-tls" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "cfg-if", "sel4-alloca", @@ -643,7 +643,7 @@ dependencies = [ [[package]] name = "sel4-logging" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "lock_api", "log", @@ -652,12 +652,12 @@ dependencies = [ [[package]] name = "sel4-no-allocator" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" [[package]] name = "sel4-panicking" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "cfg-if", "sel4-immediate-sync-once-cell", @@ -668,12 +668,12 @@ dependencies = [ [[package]] name = "sel4-panicking-env" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" [[package]] name = "sel4-phdrs" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "sel4-phdrs-constants", ] @@ -681,12 +681,12 @@ dependencies = [ [[package]] name = "sel4-phdrs-constants" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" [[package]] name = "sel4-phdrs-patched" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "sel4-phdrs", "sel4-rodata-static", @@ -695,12 +695,12 @@ dependencies = [ [[package]] name = "sel4-rodata-static" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" [[package]] name = "sel4-root-task" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "sel4", "sel4-dlmalloc", @@ -715,7 +715,7 @@ dependencies = [ [[package]] name = "sel4-root-task-macros" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "proc-macro2", "quote", @@ -725,7 +725,7 @@ dependencies = [ [[package]] name = "sel4-runtime-common" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "cfg-if", "sel4", @@ -741,12 +741,12 @@ dependencies = [ [[package]] name = "sel4-stack" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" [[package]] name = "sel4-sync" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "lock_api", "sel4", @@ -756,7 +756,7 @@ dependencies = [ [[package]] name = "sel4-sys" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=413940c8058da32098c464f6cd09e550b230505c#413940c8058da32098c464f6cd09e550b230505c" +source = "git+https://github.com/au-ts/rust-sel4?rev=535c47d3044f1de7dd54b80d485b51f9e105c8be#535c47d3044f1de7dd54b80d485b51f9e105c8be" dependencies = [ "bindgen", "glob", diff --git a/Cargo.toml b/Cargo.toml index 1c02e1bd5..73f0bd130 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,12 +12,12 @@ members = [ ] [workspace.dependencies.sel4-capdl-initializer] -git = "https://github.com/seL4/rust-sel4" -rev = "413940c8058da32098c464f6cd09e550b230505c" +git = "https://github.com/au-ts/rust-sel4" +rev = "535c47d3044f1de7dd54b80d485b51f9e105c8be" [workspace.dependencies.sel4-capdl-initializer-types] -git = "https://github.com/seL4/rust-sel4" -rev = "413940c8058da32098c464f6cd09e550b230505c" +git = "https://github.com/au-ts/rust-sel4" +rev = "535c47d3044f1de7dd54b80d485b51f9e105c8be" [profile.release.package.microkit-tool] strip = true diff --git a/docs/manual.md b/docs/manual.md index 4c35fe059..b9714e77b 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -255,6 +255,16 @@ 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. +A *memory region* can also be prefilled with bootinfo by the capDL Initialiser +via the paramter `prefill_bootinfo` in the [System Description File](#sysdesc). +If a size isn't specified, the memory region defaults to a single smallest page. +The supported bootinfo types include: +* `x86_vbe` +* `x86_mbmap` +* `x86_acpi_rsdp` +* `x86_framebuffer` +* `x86_tsc_freq` + ## Channels {#channels} A *channel* enables two protection domains to interact using protected procedures or notifications. @@ -1037,6 +1047,7 @@ It supports the following attributes: * `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 initialisation. +* `prefill_bootinfo`: (optional) Bootinfo type that the memmory region will be filled with by the capDL initialiser. The `memory_region` element does not support any child elements. diff --git a/example/bootinfo/Makefile b/example/bootinfo/Makefile new file mode 100644 index 000000000..33fd5c854 --- /dev/null +++ b/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 diff --git a/example/bootinfo/README.md b/example/bootinfo/README.md new file mode 100644 index 000000000..7410869f1 --- /dev/null +++ b/example/bootinfo/README.md @@ -0,0 +1,30 @@ + +# 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= MICROKIT_CONFIG= MICROKIT_SDK=/path/to/sdk qemu +``` + +## Running + +See instructions for your board in the manual. diff --git a/example/bootinfo/bootinfo.c b/example/bootinfo/bootinfo.c new file mode 100644 index 000000000..f801dd201 --- /dev/null +++ b/example/bootinfo/bootinfo.c @@ -0,0 +1,37 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include + +#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) +{ +} diff --git a/example/bootinfo/bootinfo.system b/example/bootinfo/bootinfo.system new file mode 100644 index 000000000..a44e68e46 --- /dev/null +++ b/example/bootinfo/bootinfo.system @@ -0,0 +1,13 @@ + + + + + + + + + diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 5bb401be0..165c11ac5 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -11,8 +11,8 @@ use std::{ }; use sel4_capdl_initializer_types::{ - object, CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId, Spec, - Word, + object, CapTableEntry, Fill, FillEntry, FillEntryContent, FillEntryContentBootInfo, + NamedObject, Object, ObjectId, Spec, Word, }; use crate::{ @@ -531,8 +531,9 @@ pub fn build_capdl_spec( .paddr() .map(|base_paddr| Word(base_paddr + (frame_sequence * mr.page_size_bytes()))); + let starting_byte_idx = 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); @@ -554,6 +555,23 @@ pub fn build_capdl_spec( }] .to_vec(), } + } else if let Some(prefill_bootinfo) = mr.prefill_bootinfo { + let remaining_bytes_to_fill = mr.size - starting_byte_idx; + let num_bytes_to_fill = min(mr.page_size_bytes(), remaining_bytes_to_fill); + + FrameFill { + entries: [FillEntry { + range: Range { + start: 0, + end: num_bytes_to_fill, + }, + content: FillEntryContent::BootInfo(FillEntryContentBootInfo { + id: prefill_bootinfo, + offset: starting_byte_idx, + }), + }] + .to_vec(), + } } else { FrameFill { entries: [].to_vec(), diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 55f40bf8e..6960b333c 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -19,8 +19,10 @@ use crate::sel4::{ Arch, ArmRiscvIrqTrigger, Config, PageSize, X86IoapicIrqPolarity, X86IoapicIrqTrigger, }; + use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool}; use crate::MAX_PDS; +use sel4_capdl_initializer_types::FillEntryContentBootInfoId; use std::collections::{HashMap, HashSet}; use std::fmt::Display; use std::fs; @@ -116,6 +118,7 @@ pub enum SysMemoryRegionKind { User, Elf, Stack, + BootInfo, } #[derive(Debug, PartialEq, Eq, Clone)] @@ -141,6 +144,7 @@ pub struct SysMemoryRegion { /// stack, ELF, etc. pub kind: SysMemoryRegionKind, pub prefill_bytes: Option>, + pub prefill_bootinfo: Option, } impl SysMemoryRegion { @@ -1424,6 +1428,7 @@ impl SysMemoryRegion { xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, prefill_bytes_maybe: &Option>, + prefill_bootinfo_maybe: Option, page_size: u64, ) -> Result { match checked_lookup(xml_sdf, node, "size") { @@ -1460,15 +1465,19 @@ impl SysMemoryRegion { } Err(_) => { - // No size explicitly specified - match &prefill_bytes_maybe { - Some(bytes) => Ok(round_up(bytes.len() as u64, page_size)), + if prefill_bootinfo_maybe.is_some() { + Ok(page_size) + } else { + // No size explicitly specified + match &prefill_bytes_maybe { + Some(bytes) => Ok(round_up(bytes.len() as u64, page_size)), - None => Err(value_error( - xml_sdf, - node, - "size must be specified if memory region is not prefilled".to_string(), - )), + None => Err(value_error( + xml_sdf, + node, + "size must be specified if memory region is not prefilled".to_string(), + )), + } } } } @@ -1483,7 +1492,14 @@ impl SysMemoryRegion { check_attributes( xml_sdf, node, - &["name", "size", "page_size", "phys_addr", "prefill_path"], + &[ + "name", + "size", + "page_size", + "phys_addr", + "prefill_path", + "prefill_bootinfo", + ], )?; let name = checked_lookup(xml_sdf, node, "name")?; @@ -1540,7 +1556,44 @@ impl SysMemoryRegion { }) .transpose()?; - let size = Self::determine_size(xml_sdf, node, &prefill_bytes_maybe, page_size)?; + let prefill_bootinfo_maybe = node + .attribute("prefill_bootinfo") + .map(|xml_bi_type| match xml_bi_type { + "x86_vbe" => Ok(FillEntryContentBootInfoId::X86Vbe), + "x86_mbmmap" => Ok(FillEntryContentBootInfoId::X86Mbmmap), + "x86_acpi_rsdp" => Ok(FillEntryContentBootInfoId::X86AcpiRsdp), + "x86_framebuffer" => Ok(FillEntryContentBootInfoId::X86FrameBuffer), + "x86_tsc_freq" => Ok(FillEntryContentBootInfoId::X86TscFreq), + "fdt" => Ok(FillEntryContentBootInfoId::Fdt), + _ => Err(value_error( + xml_sdf, + node, + format!("BootInfoMap type: '{xml_bi_type}' is not supported"), + )), + }) + .transpose()?; + + if prefill_bytes_maybe.is_some() && prefill_bootinfo_maybe.is_some() { + return Err(value_error( + xml_sdf, + node, + "prefill_path and prefill_bootinfo cannot be both specified".to_string(), + )); + } + + let mr_kind = if prefill_bootinfo_maybe.is_none() { + SysMemoryRegionKind::User + } else { + SysMemoryRegionKind::BootInfo + }; + + let size = Self::determine_size( + xml_sdf, + node, + &prefill_bytes_maybe, + prefill_bootinfo_maybe, + page_size, + )?; let phys_addr = if let Some(xml_phys_addr) = node.attribute("phys_addr") { SysMemoryRegionPaddr::Specified(sdf_parse_number(xml_phys_addr, node)?) @@ -1569,8 +1622,9 @@ impl SysMemoryRegion { page_count, phys_addr, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), - kind: SysMemoryRegionKind::User, + kind: mr_kind, prefill_bytes: prefill_bytes_maybe, + prefill_bootinfo: prefill_bootinfo_maybe, }) } } diff --git a/tool/microkit/tests/sdf/mr_prefill_bootinfo_type_invalid.system b/tool/microkit/tests/sdf/mr_prefill_bootinfo_type_invalid.system new file mode 100644 index 000000000..5a542a43e --- /dev/null +++ b/tool/microkit/tests/sdf/mr_prefill_bootinfo_type_invalid.system @@ -0,0 +1,14 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/mr_prefill_bootinfo_valid.system b/tool/microkit/tests/sdf/mr_prefill_bootinfo_valid.system new file mode 100644 index 000000000..480c9ecfa --- /dev/null +++ b/tool/microkit/tests/sdf/mr_prefill_bootinfo_valid.system @@ -0,0 +1,14 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/mr_prefill_path_bootinfo_both_specified.system b/tool/microkit/tests/sdf/mr_prefill_path_bootinfo_both_specified.system new file mode 100644 index 000000000..9450d3f76 --- /dev/null +++ b/tool/microkit/tests/sdf/mr_prefill_path_bootinfo_both_specified.system @@ -0,0 +1,14 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 1c5046ebb..ea93dcee7 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -236,6 +236,32 @@ mod memory_region { "mr_prefill_sized_valid.system", ) } + + #[test] + fn test_mr_prefill_bootinfo_valid() { + check_success( + &DEFAULT_X86_64_KERNEL_CONFIG, + "mr_prefill_bootinfo_valid.system", + ) + } + + #[test] + fn test_mr_prefill_bootinfo_type_invalid() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "mr_prefill_bootinfo_type_invalid.system", + "Error: BootInfoMap type: 'x86_invalid_bootinfo' is not supported on element 'memory_region'", + ) + } + + #[test] + fn test_mr_prefill_path_bootinfo_both_specified() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "mr_prefill_path_bootinfo_both_specified.system", + "Error: prefill_path and prefill_bootinfo cannot be both specified on element 'memory_region'", + ) + } } #[cfg(test)]