Extract kernel object sizes from headers

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,7 +569,8 @@ def build_tool(tool_target: Path, target_triple: str) -> None:
 
 def build_sel4(
     sel4_dir: Path,
-    root_dir: Path,
+    tool_dir: Path,
+    sdk_dir: Path,
     build_dir: Path,
     board: BoardInfo,
     config: ConfigInfo,
@@ -584,7 +586,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 +639,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 +652,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 +665,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 +686,44 @@ 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)
 
+    # 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(
     component_name: str,
-    root_dir: Path,
+    sdk_dir: Path,
     build_dir: Path,
     board: BoardInfo,
     config: ConfigInfo,
@@ -703,7 +734,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,16 +753,16 @@ 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)
     # Make output read-only
     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 +771,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 +781,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 +799,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 +813,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 +828,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 +838,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 +936,18 @@ 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}"
+    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"
     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 +961,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 +978,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, 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():
                     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 +1020,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")

tool/microkit/object_sizes.h

@@ -0,0 +1,44 @@
+/*
+ * Copyright 2026, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <sel4/constants.h>
+#include <sel4/sel4_arch/constants.h>
+
+/*
+ * 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

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() {