From 548529d116033373cc8b44fb8cd3fa35242bc6c7 Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Mon, 23 Mar 2026 14:59:00 +1100 Subject: [PATCH 1/2] build_sdk.py: rename root_dir to sdk_dir Signed-off-by: Ivan Velickovic --- build_sdk.py | 72 +++++++++++++++++++++++++++------------------------- 1 file changed, 37 insertions(+), 35 deletions(-) diff --git a/build_sdk.py b/build_sdk.py index c631b7e43..19b9f7a42 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -568,7 +568,7 @@ def build_tool(tool_target: Path, target_triple: str) -> None: def build_sel4( sel4_dir: Path, - root_dir: Path, + sdk_dir: Path, build_dir: Path, board: BoardInfo, config: ConfigInfo, @@ -584,7 +584,7 @@ def build_sel4( sel4_install_dir.mkdir(exist_ok=True, parents=True) sel4_build_dir.mkdir(exist_ok=True, parents=True) - print(f"Building sel4: {sel4_dir=} {root_dir=} {build_dir=} {board=} {config=}") + print(f"Building sel4: {sel4_dir=} {sdk_dir=} {build_dir=} {board=} {config=}") config_args = [ *board.kernel_options.items(), @@ -637,7 +637,7 @@ def build_sel4( elf = sel4_install_dir / "bin" / "kernel.elf" elf64_dest = ( - root_dir / "board" / board.name / config.name / "elf" / "sel4.elf" + sdk_dir / "board" / board.name / config.name / "elf" / "sel4.elf" ) elf64_dest.unlink(missing_ok=True) shutil.copy(elf, elf64_dest) @@ -650,7 +650,7 @@ def build_sel4( # Otherwise, you get this "qemu-system-x86_64: Cannot load x86-64 image, give a 32bit one." if board.arch.is_x86(): elf32_dest = ( - root_dir / "board" / board.name / config.name / "elf" / "sel4_32.elf" + sdk_dir / "board" / board.name / config.name / "elf" / "sel4_32.elf" ) objcopy_arg = f"-O elf32-i386 {str(elf64_dest)} {str(elf32_dest)}" if llvm: @@ -663,12 +663,12 @@ def build_sel4( elf32_dest.chmod(0o744) invocations_all = sel4_build_dir / "generated" / "invocations_all.json" - dest = (root_dir / "board" / board.name / config.name / "invocations_all.json") + dest = (sdk_dir / "board" / board.name / config.name / "invocations_all.json") dest.unlink(missing_ok=True) shutil.copy(invocations_all, dest) dest.chmod(0o744) - include_dir = root_dir / "board" / board.name / config.name / "include" + include_dir = sdk_dir / "board" / board.name / config.name / "include" for source in ("kernel_Config", "libsel4", "libsel4/sel4_Config", "libsel4/autoconf"): source_dir = sel4_install_dir / source / "include" for p in source_dir.rglob("*"): @@ -684,15 +684,17 @@ def build_sel4( if not board.arch.is_x86(): # only non-x86 platforms have this file to describe memory regions platform_gen = sel4_build_dir / "gen_headers" / "plat" / "machine" / "platform_gen.json" - dest = root_dir / "board" / board.name / config.name / "platform_gen.json" + dest = sdk_dir / "board" / board.name / config.name / "platform_gen.json" dest.unlink(missing_ok=True) shutil.copy(platform_gen, dest) dest.chmod(0o744) + object_sizes_header = + def build_elf_component( component_name: str, - root_dir: Path, + sdk_dir: Path, build_dir: Path, board: BoardInfo, config: ConfigInfo, @@ -703,7 +705,7 @@ def build_elf_component( Right now this is either the loader or the monitor """ - sel4_dir = root_dir / "board" / board.name / config.name + sel4_dir = sdk_dir / "board" / board.name / config.name build_dir = build_dir / board.name / config.name / component_name build_dir.mkdir(exist_ok=True, parents=True) target_triple = f"{board.arch.target_triple()}" @@ -722,7 +724,7 @@ def build_elf_component( ) elf = build_dir / f"{component_name}.elf" dest = ( - root_dir / "board" / board.name / config.name / "elf" / f"{component_name}.elf" + sdk_dir / "board" / board.name / config.name / "elf" / f"{component_name}.elf" ) dest.unlink(missing_ok=True) shutil.copy(elf, dest) @@ -730,8 +732,8 @@ def build_elf_component( dest.chmod(0o744) -def build_doc(root_dir: Path): - output = root_dir / "doc" / "microkit_user_manual.pdf" +def build_doc(sdk_dir: Path): + output = sdk_dir / "doc" / "microkit_user_manual.pdf" environ["TEXINPUTS"] = "style:" r = system(f'cd docs && pandoc manual.md -o ../{output}') @@ -740,7 +742,7 @@ def build_doc(root_dir: Path): def build_lib_component( component_name: str, - root_dir: Path, + sdk_dir: Path, build_dir: Path, board: BoardInfo, config: ConfigInfo, @@ -750,7 +752,7 @@ def build_lib_component( Right now this is just libmicrokit.a """ - sel4_dir = root_dir / "board" / board.name / config.name + sel4_dir = sdk_dir / "board" / board.name / config.name build_dir = build_dir / board.name / config.name / component_name build_dir.mkdir(exist_ok=True, parents=True) @@ -768,7 +770,7 @@ def build_lib_component( f"Error building: {component_name} for board: {board.name} config: {config.name}" ) lib = build_dir / f"{component_name}.a" - lib_dir = root_dir / "board" / board.name / config.name / "lib" + lib_dir = sdk_dir / "board" / board.name / config.name / "lib" dest = lib_dir / f"{component_name}.a" dest.unlink(missing_ok=True) shutil.copy(lib, dest) @@ -782,7 +784,7 @@ def build_lib_component( # Make output read-only dest.chmod(0o744) - include_dir = root_dir / "board" / board.name / config.name / "include" + include_dir = sdk_dir / "board" / board.name / config.name / "include" source_dir = Path(component_name) / "include" for p in source_dir.rglob("*"): if not p.is_file(): @@ -797,7 +799,7 @@ def build_lib_component( def build_initialiser( component_name: str, - root_dir: Path, + sdk_dir: Path, build_dir: Path, board: BoardInfo, config: ConfigInfo, @@ -807,7 +809,7 @@ def build_initialiser( cargo_target = board.arch.rust_toolchain() dest = ( - root_dir / "board" / board.name / config.name / "elf" / f"{component_name}.elf" + sdk_dir / "board" / board.name / config.name / "elf" / f"{component_name}.elf" ) # To save on build times, we share a single 'build target' dir for the component, @@ -905,17 +907,17 @@ def main() -> None: if not sel4_dir.exists(): raise Exception(f"sel4_dir: {sel4_dir} does not exist") - root_dir = Path("release") / f"{NAME}-sdk-{version}" + sdk_dir = Path("release") / f"{NAME}-sdk-{version}" tar_file = Path("release") / f"{NAME}-sdk-{version}.tar.gz" source_tar_file = Path("release") / f"{NAME}-source-{version}.tar.gz" dir_structure = [ - root_dir / "bin", - root_dir / "board", + sdk_dir / "bin", + sdk_dir / "board", ] if not args.skip_docs: - dir_structure.append(root_dir / "doc") + dir_structure.append(sdk_dir / "doc") for (board, configs) in build_goals: - board_dir = root_dir / "board" / board.name + board_dir = sdk_dir / "board" / board.name dir_structure.append(board_dir) for config in configs: config_dir = board_dir / config.name @@ -929,12 +931,12 @@ def main() -> None: for dr in dir_structure: dr.mkdir(exist_ok=True, parents=True) - with open(root_dir / "VERSION", "w+") as f: + with open(sdk_dir / "VERSION", "w+") as f: f.write(version + "\n") - shutil.copy(Path("LICENSE.md"), root_dir) + shutil.copy(Path("LICENSE.md"), sdk_dir) licenses_dir = Path("LICENSES") - licenses_dest_dir = root_dir / "LICENSES" + licenses_dest_dir = sdk_dir / "LICENSES" for p in licenses_dir.rglob("*"): if not p.is_file(): continue @@ -946,33 +948,33 @@ def main() -> None: dest.chmod(0o744) if not args.skip_tool: - tool_target = root_dir / "bin" / "microkit" + tool_target = sdk_dir / "bin" / "microkit" test_tool() build_tool(tool_target, args.tool_target_triple) if not args.skip_docs: - build_doc(root_dir) + build_doc(sdk_dir) if not args.skip_run_time: build_dir = Path("build") for (board, configs) in build_goals: for config in configs: if not args.skip_sel4: - build_sel4(sel4_dir, root_dir, build_dir, board, config, args.llvm) + build_sel4(sel4_dir, sdk_dir, build_dir, board, config, args.llvm) loader_printing = 1 if config.name == "debug" else 0 loader_defines = [] if not board.arch.is_x86(): loader_defines.append(("LINK_ADDRESS", hex(board.loader_link_address))) - build_elf_component("loader", root_dir, build_dir, board, config, args.llvm, loader_defines) + build_elf_component("loader", sdk_dir, build_dir, board, config, args.llvm, loader_defines) - build_elf_component("monitor", root_dir, build_dir, board, config, args.llvm, []) - build_lib_component("libmicrokit", root_dir, build_dir, board, config, args.llvm) + build_elf_component("monitor", sdk_dir, build_dir, board, config, args.llvm, []) + build_lib_component("libmicrokit", sdk_dir, build_dir, board, config, args.llvm) if not args.skip_initialiser: - build_initialiser("initialiser", root_dir, build_dir, board, config) + build_initialiser("initialiser", sdk_dir, build_dir, board, config) # Setup the examples for example, example_path in EXAMPLES.items(): - include_dir = root_dir / "example" / example + include_dir = sdk_dir / "example" / example source_dir = example_path for p in source_dir.rglob("*"): if not p.is_file(): @@ -988,7 +990,7 @@ def main() -> None: print(f"Generating {tar_file}") # At this point we create a tar.gz file with tar_open(tar_file, "w:gz") as tar: - tar.add(root_dir, arcname=root_dir.name, filter=tar_filter) + tar.add(sdk_dir, arcname=sdk_dir.name, filter=tar_filter) # Build the source tar process = popen("git ls-files") From 113fc406306ebb7b71f4b53ed5759da0fcc3c579 Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Tue, 24 Mar 2026 12:28:22 +1100 Subject: [PATCH 2/2] tool: do not hard-code kernel object sizes Many of these constants are architecture-dependent, but also slightly differ depending on how the kernel is configured. Rather than reproducing all the special combinations of kernel configurations that affect object size in the tool itself, just read from the source of truth. This should prevent bugs such as 7323d0791b3406b26f075b79050c0eb0811c918f. Signed-off-by: Ivan Velickovic --- build_sdk.py | 34 +++++++++++++++- tool/microkit/object_sizes.h | 44 ++++++++++++++++++++ tool/microkit/src/main.rs | 25 +++++++++--- tool/microkit/src/sel4.rs | 79 +++++++++++++++--------------------- tool/microkit/tests/test.rs | 4 +- 5 files changed, 130 insertions(+), 56 deletions(-) create mode 100644 tool/microkit/object_sizes.h diff --git a/build_sdk.py b/build_sdk.py index 19b9f7a42..5ff324b1f 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -23,6 +23,7 @@ import platform as host_platform from enum import IntEnum import json +import subprocess from typing import Any, Dict, Union, List, Tuple, Optional @@ -568,6 +569,7 @@ def build_tool(tool_target: Path, target_triple: str) -> None: def build_sel4( sel4_dir: Path, + tool_dir: Path, sdk_dir: Path, build_dir: Path, board: BoardInfo, @@ -689,7 +691,34 @@ def build_sel4( shutil.copy(platform_gen, dest) dest.chmod(0o744) - object_sizes_header = + # Use the preprocessor to convert the seL4 object size constants to readable JSON + # for the tool. + object_sizes_header = tool_dir / "object_sizes.h" + dest = sdk_dir / "board" / board.name / config.name / "object_sizes.json" + preprocessor = "clang" if (llvm) else f"{target_triple}-cpp" + preprocess_cmd = [ + preprocessor, + "-E", + "-P", + f"-I{include_dir}", + object_sizes_header, + ] + r = subprocess.run(preprocess_cmd, capture_output=True) + if r.returncode != 0: + raise Exception(f"Failed creating object_sizes.json: cmd={preprocess_cmd}") + + preprocessor_out = r.stdout.decode("utf-8") + object_sizes = [] + for l in preprocessor_out.split("\n"): + # Preprocessor emits commented lines etc that we want to ignore + if ": " in l: + assert len(l.split(": ")) == 2 + obj_name, size = l.split(": ") + object_sizes.append((obj_name, int(size))) + + with open(dest, "w") as out_file: + json.dump(dict(object_sizes), out_file) + dest.chmod(0o744) def build_elf_component( @@ -907,6 +936,7 @@ def main() -> None: if not sel4_dir.exists(): raise Exception(f"sel4_dir: {sel4_dir} does not exist") + tool_dir = Path("tool/microkit") sdk_dir = Path("release") / f"{NAME}-sdk-{version}" tar_file = Path("release") / f"{NAME}-sdk-{version}.tar.gz" source_tar_file = Path("release") / f"{NAME}-source-{version}.tar.gz" @@ -960,7 +990,7 @@ def main() -> None: for (board, configs) in build_goals: for config in configs: if not args.skip_sel4: - build_sel4(sel4_dir, sdk_dir, build_dir, board, config, args.llvm) + build_sel4(sel4_dir, tool_dir, sdk_dir, build_dir, board, config, args.llvm) loader_printing = 1 if config.name == "debug" else 0 loader_defines = [] if not board.arch.is_x86(): diff --git a/tool/microkit/object_sizes.h b/tool/microkit/object_sizes.h new file mode 100644 index 000000000..d354f3cdd --- /dev/null +++ b/tool/microkit/object_sizes.h @@ -0,0 +1,44 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include + +/* + * The Microkit tool needs to know the sizes of kernel objects. + * seL4 exports these values through C header files, to make it + * easier for the tool to consume the object sizes, we preprocess + * this file to extract the sizes of objects and then build_sdk.py + * takes that output and mangles it into JSON. + */ + +tcb: seL4_TCBBits +endpoint: seL4_EndpointBits +notification: seL4_NotificationBits +small_page: seL4_PageBits +large_page: seL4_LargePageBits +asid_pool: seL4_ASIDPoolBits +asid_table: seL4_ASIDPoolIndexBits +slot: seL4_SlotBits +min_untyped_bits: seL4_MinUntypedBits +max_untyped_bits: seL4_MaxUntypedBits +vspace: seL4_VSpaceBits + +#ifdef seL4_ReplyBits +reply: seL4_ReplyBits +#endif + +#ifdef seL4_VCPUBits +vcpu: seL4_VCPUBits +#endif +#ifdef seL4_PageTableBits +page_table: seL4_PageTableBits +#endif +#ifdef seL4_HugePageBits +huge_page: seL4_HugePageBits +#endif +#ifdef seL4_IOPageTableBits +io_page_table: seL4_IOPageTableBits +#endif diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index ae6a188ef..d361eb9cf 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -472,6 +472,24 @@ fn main() -> Result<(), String> { } }; + let object_sizes = { + let object_sizes_path = sdk_dir + .join("board") + .join(args.board) + .join(args.config) + .join("object_sizes.json"); + + if !object_sizes_path.exists() { + eprintln!( + "Error: object sizes file '{}' does not exist", + object_sizes_path.display() + ); + std::process::exit(1); + } + + serde_json::from_str(&fs::read_to_string(object_sizes_path).unwrap()).unwrap() + }; + let hypervisor = match arch { Arch::Aarch64 => json_str_as_bool(&kernel_config_json, "ARM_HYPERVISOR_SUPPORT")?, Arch::X86_64 => json_str_as_bool(&kernel_config_json, "VTX")?, @@ -497,11 +515,6 @@ fn main() -> Result<(), String> { _ => None, }; - let x86_xsave_size = match arch { - Arch::X86_64 => Some(json_str_as_u64(&kernel_config_json, "XSAVE_SIZE")? as usize), - _ => None, - }; - let kernel_frame_size = match arch { Arch::Aarch64 => 1 << 12, Arch::Riscv64 => 1 << 21, @@ -534,10 +547,10 @@ fn main() -> Result<(), String> { arm_pa_size_bits, arm_smc, riscv_pt_levels: Some(RiscvVirtualMemory::Sv39), - x86_xsave_size, invocations_labels, device_regions, normal_regions, + object_sizes, }; if kernel_config.arch != Arch::X86_64 && !loader_elf_path.exists() { diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index 4c258e3c9..cca595fd0 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -261,6 +261,24 @@ pub struct PlatformConfig { pub memory: Vec, } +/// Deserialised from a generated 'object_sizes.json' file in the SDK +/// Maps a kernel object to the size of the object, specified in bits. +#[derive(Deserialize)] +pub struct ObjectSizes { + pub tcb: u64, + pub endpoint: u64, + pub notification: u64, + pub reply: u64, + pub vspace: u64, + pub page_table: u64, + pub huge_page: u64, + pub large_page: u64, + pub small_page: u64, + pub asid_pool: u64, + // Optional as vCPU is not supported on RISC-V. + pub vcpu: Option, +} + pub struct Config { pub arch: Arch, pub word_size: u64, @@ -283,9 +301,9 @@ pub struct Config { pub arm_smc: Option, /// RISC-V specific, what kind of virtual memory system (e.g Sv39) pub riscv_pt_levels: Option, - /// x86 specific, user context size - pub x86_xsave_size: Option, pub invocations_labels: serde_json::Value, + /// Kernel object sizes, used for kernel boot emulation and untyped allocation. + pub object_sizes: Option, /// The two remaining fields are only valid on ARM and RISC-V pub device_regions: Option>, pub normal_regions: Option>, @@ -432,54 +450,23 @@ impl ObjectType { /// Gets the number of bits to represent the size of a object. The /// size depends on architecture as well as kernel configuration. pub fn fixed_size_bits(self, config: &Config) -> Option { + assert!(config.object_sizes.is_some()); + let object_sizes = &config.object_sizes.as_ref().unwrap(); match self { - ObjectType::Tcb => match config.arch { - Arch::Aarch64 => { - if config.hypervisor && config.benchmark && config.num_cores > 1 { - Some(12) - } else { - Some(11) - } - } - Arch::Riscv64 => match config.fpu { - true => Some(11), - false => Some(10), - }, - Arch::X86_64 => { - // matches seL4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h - if config.x86_xsave_size.unwrap() >= 832 { - Some(12) - } else { - Some(11) - } - } - }, - ObjectType::Endpoint => Some(4), - ObjectType::Notification => Some(6), - ObjectType::Reply => Some(5), - ObjectType::VSpace => match config.arch { - Arch::Aarch64 => match config.hypervisor { - true => match config.arm_pa_size_bits.unwrap() { - 40 => Some(13), - 44 => Some(12), - _ => { - panic!("Unexpected ARM PA size bits when determining VSpace size bits") - } - }, - false => Some(12), - }, - _ => Some(12), - }, - ObjectType::PageTable => Some(12), - ObjectType::HugePage => Some(30), - ObjectType::LargePage => Some(21), - ObjectType::SmallPage => Some(12), + ObjectType::Tcb => Some(object_sizes.tcb), + ObjectType::Endpoint => Some(object_sizes.endpoint), + ObjectType::Notification => Some(object_sizes.notification), + ObjectType::Reply => Some(object_sizes.reply), + ObjectType::VSpace => Some(object_sizes.vspace), + ObjectType::PageTable => Some(object_sizes.page_table), + ObjectType::HugePage => Some(object_sizes.huge_page), + ObjectType::LargePage => Some(object_sizes.large_page), + ObjectType::SmallPage => Some(object_sizes.small_page), ObjectType::Vcpu => match config.arch { - Arch::Aarch64 => Some(12), - Arch::X86_64 => Some(14), + Arch::Aarch64 | Arch::X86_64 => Some(object_sizes.vcpu.unwrap()), _ => panic!("Unexpected architecture asking for vCPU size bits"), }, - ObjectType::AsidPool => Some(12), + ObjectType::AsidPool => Some(object_sizes.asid_pool), _ => None, } } diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 02263798c..7e4791f8a 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -27,11 +27,11 @@ const DEFAULT_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config { arm_pa_size_bits: Some(40), arm_smc: None, riscv_pt_levels: None, - x86_xsave_size: None, // Not necessary for SDF parsing invocations_labels: json!(null), device_regions: None, normal_regions: None, + object_sizes: None, }; const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config { @@ -51,11 +51,11 @@ const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config { arm_pa_size_bits: None, arm_smc: None, riscv_pt_levels: None, - x86_xsave_size: None, // Not necessary for SDF parsing invocations_labels: json!(null), device_regions: None, normal_regions: None, + object_sizes: None, }; fn check_success(kernel_config: &sel4::Config, test_name: &str) {