From 39a28221cccec655ac14eb258fab108a234845af Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Mon, 16 Mar 2026 14:16:52 +1100 Subject: [PATCH 1/8] tool: implement memory region data prefilling Signed-off-by: Bill Nguyen --- .reuse/dep5 | 1 + tool/microkit/src/capdl/builder.rs | 42 +++++- tool/microkit/src/capdl/packaging.rs | 19 ++- tool/microkit/src/capdl/spec.rs | 11 ++ tool/microkit/src/main.rs | 26 ++-- tool/microkit/src/sdf.rs | 136 ++++++++++++++++-- tool/microkit/src/symbols.rs | 8 ++ tool/microkit/src/util.rs | 15 +- tool/microkit/tests/prefills/empty.bin | 0 tool/microkit/tests/prefills/small.bin | 1 + .../sdf/mr_prefill_does_not_exists.system | 14 ++ .../tests/sdf/mr_prefill_empty_file.system | 14 ++ .../tests/sdf/mr_prefill_no_size_valid.system | 14 ++ .../sdf/mr_prefill_page_sized_valid.system | 14 ++ .../tests/sdf/mr_prefill_sized_valid.system | 14 ++ tool/microkit/tests/test.rs | 72 ++++++++-- 16 files changed, 346 insertions(+), 55 deletions(-) create mode 100644 tool/microkit/tests/prefills/empty.bin create mode 100644 tool/microkit/tests/prefills/small.bin create mode 100644 tool/microkit/tests/sdf/mr_prefill_does_not_exists.system create mode 100644 tool/microkit/tests/sdf/mr_prefill_empty_file.system create mode 100644 tool/microkit/tests/sdf/mr_prefill_no_size_valid.system create mode 100644 tool/microkit/tests/sdf/mr_prefill_page_sized_valid.system create mode 100644 tool/microkit/tests/sdf/mr_prefill_sized_valid.system diff --git a/.reuse/dep5 b/.reuse/dep5 index 7c857039d..b89873aa6 100644 --- a/.reuse/dep5 +++ b/.reuse/dep5 @@ -14,6 +14,7 @@ Files: VERSION docs/assets/microkit_flow.svg docs/assets/microkit_flow.pdf + tool/microkit/tests/prefills/small.bin Copyright: 2024, UNSW License: BSD-2-Clause diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 4173a2feb..44754e8e6 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/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; +pub type FrameFill = Fill; pub type CapDLNamedObject = NamedObject; 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, diff --git a/tool/microkit/src/capdl/packaging.rs b/tool/microkit/src/capdl/packaging.rs index 5a18ad248..1dbe897d0 100644 --- a/tool/microkit/src/capdl/packaging.rs +++ b/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 }, ); diff --git a/tool/microkit/src/capdl/spec.rs b/tool/microkit/src/capdl/spec.rs index 8d9bca61c..2486c837a 100644 --- a/tool/microkit/src/capdl/spec.rs +++ b/tool/microkit/src/capdl/spec.rs @@ -21,6 +21,17 @@ pub struct ElfContent { pub elf_seg_data_range: Range, } +#[derive(Clone, Serialize)] +pub struct BytesContent { + pub bytes: Vec, +} + +#[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, sel4_config: &Config) -> u64 { match obj { diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index 9fc628d34..600087272 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -23,7 +23,8 @@ use microkit_tool::sel4::{ }; use microkit_tool::symbols::patch_symbols; use microkit_tool::util::{ - human_size_strict, json_str, json_str_as_bool, json_str_as_u64, round_down, round_up, + get_full_path, human_size_strict, json_str, json_str_as_bool, json_str_as_u64, round_down, + round_up, }; use microkit_tool::{DisjointMemoryRegion, MemoryRegion}; use std::collections::HashMap; @@ -40,17 +41,6 @@ const KERNEL_COPY_FILENAME: &str = "sel4.elf"; // also copy the 32-bit version that was prepared by build_sdk.py for convenience. const KERNEL32_COPY_FILENAME: &str = "sel4_32.elf"; -fn get_full_path(path: &Path, search_paths: &Vec) -> Option { - for search_path in search_paths { - let full_path = search_path.join(path); - if full_path.exists() { - return Some(full_path.to_path_buf()); - } - } - - None -} - fn print_usage() { println!("usage: microkit [-h] [-o OUTPUT] [--image-type {{binary,elf,uimage}}] [-r REPORT] --board BOARD --config CONFIG [--capdl-json CAPDL_SPEC] --search-path [SEARCH_PATH ...] system") } @@ -573,7 +563,12 @@ fn main() -> Result<(), String> { "Microkit tool has various assumptions about the word size being 64-bits." ); - let mut system = match parse(args.system, &xml, &kernel_config) { + let mut search_paths = vec![std::env::current_dir().unwrap()]; + for path in args.search_paths { + search_paths.push(PathBuf::from(path)); + } + + let mut system = match parse(args.system, &xml, &kernel_config, &search_paths) { Ok(system) => system, Err(err) => { eprintln!("{err}"); @@ -630,11 +625,6 @@ fn main() -> Result<(), String> { std::process::exit(1); }); - let mut search_paths = vec![std::env::current_dir().unwrap()]; - for path in args.search_paths { - search_paths.push(PathBuf::from(path)); - } - // This list refers to all PD ELFs as well as the Monitor ELF. // The monitor is very similar to a PD so it is useful to pass around // a list like this. diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index ab5b6f3b3..48d3fd282 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -19,10 +19,11 @@ use crate::sel4::{ Arch, ArmRiscvIrqTrigger, Config, PageSize, X86IoapicIrqPolarity, X86IoapicIrqTrigger, }; -use crate::util::{ranges_overlap, str_to_bool}; +use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool}; use crate::MAX_PDS; use std::collections::HashSet; use std::fmt::Display; +use std::fs; use std::path::{Path, PathBuf}; /// Events that come through entry points (e.g notified or protected) are given an @@ -125,6 +126,7 @@ pub struct SysMemoryRegion { /// due to the user's SDF or created by the tool for setting up the /// stack, ELF, etc. pub kind: SysMemoryRegionKind, + pub prefill_bytes: Option>, } impl SysMemoryRegion { @@ -212,6 +214,7 @@ pub enum SysSetVarKind { Paddr { region: String }, Id { id: u64 }, X86IoPortAddr { address: u64 }, + PrefillSize { mr: String }, } #[derive(Debug, PartialEq, Eq)] @@ -347,6 +350,7 @@ impl SysMap { if allow_setvar { attrs.push("setvar_vaddr"); attrs.push("setvar_size"); + attrs.push("setvar_prefill_size"); } check_attributes(xml_sdf, node, &attrs)?; @@ -651,6 +655,14 @@ impl ProtectionDomain { checked_add_setvar(&mut setvars, setvar, xml_sdf, &child)?; } + if let Some(setvar_prefill_size) = child.attribute("setvar_prefill_size") { + let setvar = SysSetVar { + symbol: setvar_prefill_size.to_string(), + kind: SysSetVarKind::PrefillSize { mr: map.mr.clone() }, + }; + checked_add_setvar(&mut setvars, setvar, xml_sdf, &child)?; + } + maps.push(map); } "irq" => { @@ -1210,17 +1222,75 @@ impl VirtualMachine { } impl SysMemoryRegion { + fn determine_size( + xml_sdf: &XmlSystemDescription, + node: &roxmltree::Node, + prefill_bytes_maybe: &Option>, + page_size: u64, + ) -> Result { + match checked_lookup(xml_sdf, node, "size") { + Ok(size_str) => { + // Size explicitly specified + let size_parsed = sdf_parse_number(size_str, node)?; + + if !size_parsed.is_multiple_of(page_size) { + return Err(value_error( + xml_sdf, + node, + "size is not a multiple of the page size".to_string(), + )); + } + + match &prefill_bytes_maybe { + Some(bytes) => { + if bytes.len() > size_parsed as usize { + return Err(value_error( + xml_sdf, + node, + format!( + "size of prefill file exceeds memory region size: {:x} > {:x}", + bytes.len(), + size_parsed + ), + )); + } + + Ok(size_parsed) + } + None => Ok(size_parsed), + } + } + + Err(_) => { + // 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(), + )), + } + } + } + } + fn from_xml( config: &Config, xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, + search_paths: &Vec, ) -> Result { - check_attributes(xml_sdf, node, &["name", "size", "page_size", "phys_addr"])?; + check_attributes( + xml_sdf, + node, + &["name", "size", "page_size", "phys_addr", "prefill_path"], + )?; let name = checked_lookup(xml_sdf, node, "name")?; - let size = sdf_parse_number(checked_lookup(xml_sdf, node, "size")?, node)?; - let mut page_size_specified_by_user = false; + let mut page_size_specified_by_user = false; let page_size = if let Some(xml_page_size) = node.attribute("page_size") { page_size_specified_by_user = true; sdf_parse_number(xml_page_size, node)? @@ -1237,13 +1307,42 @@ impl SysMemoryRegion { )); } - if !size.is_multiple_of(page_size) { - return Err(value_error( - xml_sdf, - node, - "size is not a multiple of the page size".to_string(), - )); - } + let prefill_bytes_maybe = node + .attribute("prefill_path") + .map(|path_str| { + get_full_path(&PathBuf::from(path_str), search_paths) + .ok_or_else(|| { + value_error( + xml_sdf, + node, + format!("unable to find prefill file: '{path_str}'"), + ) + }) + .and_then(|prefill_path| { + fs::read(&prefill_path) + .map_err(|_| { + value_error( + xml_sdf, + node, + format!("failed to read file '{path_str}' at prefill_path"), + ) + }) + .and_then(|bytes| { + if bytes.is_empty() { + Err(value_error( + xml_sdf, + node, + format!("prefill file '{path_str}' is empty"), + )) + } else { + Ok(bytes) + } + }) + }) + }) + .transpose()?; + + let size = Self::determine_size(xml_sdf, node, &prefill_bytes_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)?) @@ -1273,6 +1372,7 @@ impl SysMemoryRegion { phys_addr, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), kind: SysMemoryRegionKind::User, + prefill_bytes: prefill_bytes_maybe, }) } } @@ -1611,7 +1711,12 @@ fn pd_flatten( Ok(all_pds) } -pub fn parse(filename: &str, xml: &str, config: &Config) -> Result { +pub fn parse( + filename: &str, + xml: &str, + config: &Config, + search_paths: &Vec, +) -> Result { let doc = match roxmltree::Document::parse(xml) { Ok(doc) => doc, Err(err) => return Err(format!("Could not parse '{filename}': {err}")), @@ -1651,7 +1756,12 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result channel_nodes.push(child), - "memory_region" => mrs.push(SysMemoryRegion::from_xml(config, &xml_sdf, &child)?), + "memory_region" => mrs.push(SysMemoryRegion::from_xml( + config, + &xml_sdf, + &child, + search_paths, + )?), "virtual_machine" => { let pos = xml_sdf.doc.text_pos_at(child.range().start); return Err(format!( diff --git a/tool/microkit/src/symbols.rs b/tool/microkit/src/symbols.rs index 6136cf145..0fc935da2 100644 --- a/tool/microkit/src/symbols.rs +++ b/tool/microkit/src/symbols.rs @@ -156,6 +156,14 @@ pub fn patch_symbols( } sdf::SysSetVarKind::Id { id } => *id, sdf::SysSetVarKind::X86IoPortAddr { address } => *address, + sdf::SysSetVarKind::PrefillSize { mr } => mr_name_to_desc + .get(mr) + .unwrap() + .prefill_bytes + .as_ref() + .unwrap() + .len() + as u64, }; symbols_to_write.push((&setvar.symbol, data)); } diff --git a/tool/microkit/src/util.rs b/tool/microkit/src/util.rs index 77420a172..6f2c0e275 100644 --- a/tool/microkit/src/util.rs +++ b/tool/microkit/src/util.rs @@ -4,9 +4,9 @@ // SPDX-License-Identifier: BSD-2-Clause // -use std::ops::Range; - use serde_json; +use std::ops::Range; +use std::path::{Path, PathBuf}; pub fn msb(x: u64) -> u64 { 64 - x.leading_zeros() as u64 - 1 @@ -203,6 +203,17 @@ pub fn monitor_serialise_names(names: &[String], max_len: usize, max_name_len: u names_bytes } +pub fn get_full_path(path: &Path, search_paths: &Vec) -> Option { + for search_path in search_paths { + let full_path = search_path.join(path); + if full_path.exists() { + return Some(full_path.to_path_buf()); + } + } + + None +} + #[cfg(test)] mod tests { // Note this useful idiom: importing names from outer (for mod tests) scope. diff --git a/tool/microkit/tests/prefills/empty.bin b/tool/microkit/tests/prefills/empty.bin new file mode 100644 index 000000000..e69de29bb diff --git a/tool/microkit/tests/prefills/small.bin b/tool/microkit/tests/prefills/small.bin new file mode 100644 index 000000000..30d74d258 --- /dev/null +++ b/tool/microkit/tests/prefills/small.bin @@ -0,0 +1 @@ +test \ No newline at end of file diff --git a/tool/microkit/tests/sdf/mr_prefill_does_not_exists.system b/tool/microkit/tests/sdf/mr_prefill_does_not_exists.system new file mode 100644 index 000000000..473840d01 --- /dev/null +++ b/tool/microkit/tests/sdf/mr_prefill_does_not_exists.system @@ -0,0 +1,14 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/mr_prefill_empty_file.system b/tool/microkit/tests/sdf/mr_prefill_empty_file.system new file mode 100644 index 000000000..609caacb1 --- /dev/null +++ b/tool/microkit/tests/sdf/mr_prefill_empty_file.system @@ -0,0 +1,14 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/mr_prefill_no_size_valid.system b/tool/microkit/tests/sdf/mr_prefill_no_size_valid.system new file mode 100644 index 000000000..1de5fb10c --- /dev/null +++ b/tool/microkit/tests/sdf/mr_prefill_no_size_valid.system @@ -0,0 +1,14 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/mr_prefill_page_sized_valid.system b/tool/microkit/tests/sdf/mr_prefill_page_sized_valid.system new file mode 100644 index 000000000..27388e4d7 --- /dev/null +++ b/tool/microkit/tests/sdf/mr_prefill_page_sized_valid.system @@ -0,0 +1,14 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/mr_prefill_sized_valid.system b/tool/microkit/tests/sdf/mr_prefill_sized_valid.system new file mode 100644 index 000000000..51de5c7de --- /dev/null +++ b/tool/microkit/tests/sdf/mr_prefill_sized_valid.system @@ -0,0 +1,14 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 7e4791f8a..006f3c80c 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -59,11 +59,16 @@ const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config { }; fn check_success(kernel_config: &sel4::Config, test_name: &str) { - let mut path = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let env_path = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")); + + let mut prefill_path = env_path.clone(); + prefill_path.push("tests/prefills"); + + let mut path = env_path.clone(); path.push("tests/sdf/"); path.push(test_name); let sdf = std::fs::read_to_string(path).unwrap(); - let parse = sdf::parse(test_name, &sdf, kernel_config); + let parse = sdf::parse(test_name, &sdf, kernel_config, &[prefill_path].to_vec()); if let Err(ref e) = parse { eprintln!("Expected no error, instead got:\n{e}") @@ -73,11 +78,17 @@ fn check_success(kernel_config: &sel4::Config, test_name: &str) { } fn check_error(kernel_config: &sel4::Config, test_name: &str, expected_err: &str) { - let mut path = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")); - path.push("tests/sdf/"); - path.push(test_name); - let sdf = std::fs::read_to_string(path).unwrap(); - let parse_err = sdf::parse(test_name, &sdf, kernel_config).unwrap_err(); + let env_path = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")); + + let mut prefill_path = env_path.clone(); + prefill_path.push("tests/prefills"); + + let mut sdf_path = env_path.clone(); + sdf_path.push("tests/sdf/"); + sdf_path.push(test_name); + let sdf = std::fs::read_to_string(sdf_path).unwrap(); + let parse_err = + sdf::parse(test_name, &sdf, kernel_config, &[prefill_path].to_vec()).unwrap_err(); if !parse_err.starts_with(expected_err) { eprintln!("Expected error:\n{expected_err}\nGot error:\n{parse_err}\n"); @@ -130,11 +141,10 @@ mod memory_region { #[test] fn test_missing_size() { - check_missing( + check_error( &DEFAULT_AARCH64_KERNEL_CONFIG, "mr_missing_size.system", - "size", - "memory_region", + "Error: size must be specified if memory region is not prefilled on element 'memory_region'", ) } @@ -164,6 +174,48 @@ mod memory_region { "Error: memory region 'mr2' physical address range [0x9001000..0x9002000) overlaps with another memory region 'mr1' [0x9000000..0x9002000) @ ", ) } + + #[test] + fn test_mr_prefill_empty_file() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "mr_prefill_empty_file.system", + "Error: prefill file 'empty.bin' is empty on element 'memory_region'", + ) + } + + #[test] + fn test_mr_prefill_does_not_exists() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "mr_prefill_does_not_exists.system", + "Error: unable to find prefill file: 'abcxyz.bin' on element 'memory_region'", + ) + } + + #[test] + fn test_mr_prefill_no_size_valid() { + check_success( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "mr_prefill_no_size_valid.system", + ) + } + + #[test] + fn test_mr_prefill_page_sized_valid() { + check_success( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "mr_prefill_page_sized_valid.system", + ) + } + + #[test] + fn test_mr_prefill_sized_valid() { + check_success( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "mr_prefill_sized_valid.system", + ) + } } #[cfg(test)] From 9ef256a5a2aaef61a7adae1d85646df3aa24f6a2 Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Tue, 10 Mar 2026 16:59:31 +1100 Subject: [PATCH 2/8] manual: document memory region data prefilling Signed-off-by: Bill Nguyen --- docs/manual.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/docs/manual.md b/docs/manual.md index 6a4434fdc..08a8eeafc 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -245,6 +245,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. @@ -1026,6 +1036,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: @@ -1101,6 +1112,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. From 946a9dda7f216ae37ed1e5a6bd8029e83f94e39c Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Tue, 10 Mar 2026 16:59:50 +1100 Subject: [PATCH 3/8] examples: add mr_prefill Signed-off-by: Bill Nguyen --- .reuse/dep5 | 1 + example/mr_prefill/Makefile | 68 +++++++++++++++++++++ example/mr_prefill/README.md | 20 +++++++ example/mr_prefill/fill.bin | Bin 0 -> 4112 bytes example/mr_prefill/mr_prefill.c | 85 +++++++++++++++++++++++++++ example/mr_prefill/mr_prefill.system | 15 +++++ 6 files changed, 189 insertions(+) create mode 100644 example/mr_prefill/Makefile create mode 100644 example/mr_prefill/README.md create mode 100644 example/mr_prefill/fill.bin create mode 100644 example/mr_prefill/mr_prefill.c create mode 100644 example/mr_prefill/mr_prefill.system diff --git a/.reuse/dep5 b/.reuse/dep5 index b89873aa6..7fec7a696 100644 --- a/.reuse/dep5 +++ b/.reuse/dep5 @@ -15,6 +15,7 @@ Files: docs/assets/microkit_flow.svg docs/assets/microkit_flow.pdf tool/microkit/tests/prefills/small.bin + example/mr_prefill/fill.bin Copyright: 2024, UNSW License: BSD-2-Clause diff --git a/example/mr_prefill/Makefile b/example/mr_prefill/Makefile new file mode 100644 index 000000000..56eb03e4b --- /dev/null +++ b/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) diff --git a/example/mr_prefill/README.md b/example/mr_prefill/README.md new file mode 100644 index 000000000..7cd387911 --- /dev/null +++ b/example/mr_prefill/README.md @@ -0,0 +1,20 @@ + +# 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= MICROKIT_CONFIG= MICROKIT_SDK=/path/to/sdk +``` + +## Running + +See instructions for your board in the manual. diff --git a/example/mr_prefill/fill.bin b/example/mr_prefill/fill.bin new file mode 100644 index 0000000000000000000000000000000000000000..4fe756a7670d710538b7a47b2c3b6467ab99b4db GIT binary patch literal 4112 zcmWd$770#wRc2%u1*0J_8UiCW1m2%r-8o`CKkD((5Eu=C(GVC7fzc2c4S~@R7!85Z L5Ey|WPznS9V3h`A literal 0 HcmV?d00001 diff --git a/example/mr_prefill/mr_prefill.c b/example/mr_prefill/mr_prefill.c new file mode 100644 index 000000000..5e34656f0 --- /dev/null +++ b/example/mr_prefill/mr_prefill.c @@ -0,0 +1,85 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include + +#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) +{ +} diff --git a/example/mr_prefill/mr_prefill.system b/example/mr_prefill/mr_prefill.system new file mode 100644 index 000000000..f1d69baf6 --- /dev/null +++ b/example/mr_prefill/mr_prefill.system @@ -0,0 +1,15 @@ + + + + + + + + + + + From 2d6cc0598cb33eb5eb00408d9e3cb565e61ff83c Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Mon, 30 Mar 2026 17:02:22 +1100 Subject: [PATCH 4/8] tool: clippy/fmt fix Signed-off-by: Ivan Velickovic --- tool/microkit/src/symbols.rs | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/tool/microkit/src/symbols.rs b/tool/microkit/src/symbols.rs index 0fc935da2..477ef5c7b 100644 --- a/tool/microkit/src/symbols.rs +++ b/tool/microkit/src/symbols.rs @@ -156,14 +156,9 @@ pub fn patch_symbols( } sdf::SysSetVarKind::Id { id } => *id, sdf::SysSetVarKind::X86IoPortAddr { address } => *address, - sdf::SysSetVarKind::PrefillSize { mr } => mr_name_to_desc - .get(mr) - .unwrap() - .prefill_bytes - .as_ref() - .unwrap() - .len() - as u64, + sdf::SysSetVarKind::PrefillSize { mr } => { + mr_name_to_desc[mr].prefill_bytes.as_ref().unwrap().len() as u64 + } }; symbols_to_write.push((&setvar.symbol, data)); } From e7c4c0bd54443d62f7b1441f5814d07edab1609b Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Tue, 31 Mar 2026 11:47:56 +1100 Subject: [PATCH 5/8] tool: check prefill used for prefill setvar Signed-off-by: Ivan Velickovic --- tool/microkit/src/sdf.rs | 11 +++++++++++ .../sdf/mr_prefill_size_without_prefill.system | 14 ++++++++++++++ tool/microkit/tests/test.rs | 9 +++++++++ 3 files changed, 34 insertions(+) create mode 100644 tool/microkit/tests/sdf/mr_prefill_size_without_prefill.system diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 48d3fd282..ceb582886 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -2105,6 +2105,17 @@ pub fn parse( if let SysSetVarKind::Paddr { region } = &setvar.kind { mr_names_with_setvar_paddr.insert(region); }; + if let SysSetVarKind::PrefillSize { mr } = &setvar.kind { + for matching_mr in &mrs { + if matching_mr.name == *mr && matching_mr.prefill_bytes.is_none() { + return Err(format!( + "Error: 'setvar_prefill_size' used for MR without a `prefill_path` @ '{}' {}", + matching_mr.name, + loc_string(&xml_sdf, matching_mr.text_pos.unwrap()), + )); + } + } + } } } for mr in mrs.iter_mut() { diff --git a/tool/microkit/tests/sdf/mr_prefill_size_without_prefill.system b/tool/microkit/tests/sdf/mr_prefill_size_without_prefill.system new file mode 100644 index 000000000..720c97bf7 --- /dev/null +++ b/tool/microkit/tests/sdf/mr_prefill_size_without_prefill.system @@ -0,0 +1,14 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 006f3c80c..997dbd304 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -193,6 +193,15 @@ mod memory_region { ) } + #[test] + fn test_mr_prefill_size_without_prefill() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "mr_prefill_size_without_prefill.system", + "Error: 'setvar_prefill_size' used for MR without a `prefill_path` @" + ) + } + #[test] fn test_mr_prefill_no_size_valid() { check_success( From d5bf68c63960d920d55ab17b8e6586c00821eee2 Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Tue, 31 Mar 2026 11:50:36 +1100 Subject: [PATCH 6/8] manual: fixes for prefill MR Signed-off-by: Ivan Velickovic --- docs/manual.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index 08a8eeafc..28135f991 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -1109,10 +1109,12 @@ The `memory_region` element describes a memory region. It supports the following attributes: * `name`: A unique name for the memory region -* `size`: Size of the memory region in bytes (must be a multiple of the page size) +* `size`: Size of the memory region in bytes (must be a multiple of the page size). This can + be omitted if the memory region is has `prefill_path`, the size will be determined by + the length of the file given. * `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. +* `prefill_path`: (optional) Path to a file containing data that the memory region will be filled with at initialisation. The `memory_region` element does not support any child elements. From effd370cce698164ec32105e1561f750a75134fe Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Tue, 31 Mar 2026 11:52:54 +1100 Subject: [PATCH 7/8] example: typo fix Signed-off-by: Ivan Velickovic --- example/mr_prefill/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/example/mr_prefill/README.md b/example/mr_prefill/README.md index 7cd387911..b29b8030a 100644 --- a/example/mr_prefill/README.md +++ b/example/mr_prefill/README.md @@ -4,7 +4,7 @@ --> # Example - Memory Region Prefill -This is an example demostrating prefilling a memory region from a data file at compile time. +This is an example demonstrating prefilling a memory region from a data file at compile time. All Microkit platforms are supported. From 33d1c1f43ebe503316d95452787118ee240512a2 Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Tue, 31 Mar 2026 11:53:15 +1100 Subject: [PATCH 8/8] tool: cargo fmt fix Signed-off-by: Ivan Velickovic --- tool/microkit/tests/test.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 997dbd304..d2becea69 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -198,7 +198,7 @@ mod memory_region { check_error( &DEFAULT_AARCH64_KERNEL_CONFIG, "mr_prefill_size_without_prefill.system", - "Error: 'setvar_prefill_size' used for MR without a `prefill_path` @" + "Error: 'setvar_prefill_size' used for MR without a `prefill_path` @", ) }