seL4Config: remove duplicated constants

build_sdk.py

@@ -726,32 +726,35 @@ def build_sel4(
 
     # 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)
+    sel4_constants = ["object_sizes", "address_space_constants"]
+    for sel4_constant_type in sel4_constants:
+        header_src = tool_dir / f"{sel4_constant_type}.h"
+        json_dst = sdk_dir / "board" / board.name / config.name / f"{sel4_constant_type}.json"
+        preprocessor = "clang" if (llvm) else f"{target_triple}-cpp"
+        preprocess_cmd = [
+            preprocessor,
+            "-E",
+            "-P",
+            f"-I{include_dir}",
+            header_src,
+        ]
+        r = subprocess.run(preprocess_cmd, capture_output=True)
+        if r.returncode != 0:
+            raise Exception(f"Failed creating object_sizes.json: cmd={preprocess_cmd}")
+        sizes = []
+        for l in r.stdout.decode("utf-8").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(": ")
+                if "-" in size:
+                    lhs, rhs = size.strip("( )").split("-", 1)
+                    size = str(int(lhs.strip(), 0) - int(rhs.strip(), 0))
+                sizes.append((obj_name, int(size, 0)))
+
+        with open(json_dst, "w") as out_file:
+            json.dump(dict(sizes), out_file)
+            json_dst.chmod(0o744)
 
 
 def build_elf_component(

tool/microkit/address_space_constants.h

@@ -0,0 +1,21 @@
+/*
+ * Copyright 2026, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include <sel4/arch/constants.h>
+#include <sel4/constants.h>
+#include <sel4/plat/api/constants.h>
+#include <sel4/sel4_arch/constants.h>
+
+page_table_index_bits: seL4_PageTableIndexBits
+vspace_user_top: seL4_UserVSpaceTop
+
+#ifdef seL4_VSpaceIndexBits
+vspace_index_bits: seL4_VSpaceIndexBits
+#endif
+
+#ifdef seL4_IOPageTableIndexBits
+io_page_table_index_bits: seL4_IOPageTableIndexBits
+#endif

tool/microkit/src/main.rs

@@ -19,10 +19,10 @@ use microkit_tool::elf::ElfFile;
 use microkit_tool::loader::Loader;
 use microkit_tool::report::write_report;
 use microkit_tool::sdf::{parse, SysMemoryRegion, SysMemoryRegionPaddr};
-use microkit_tool::sdk::Sdk;
+use microkit_tool::sdk::{AvailableConfig, Sdk};
 use microkit_tool::sel4::{
-    emulate_kernel_boot, emulate_kernel_boot_partial, Arch, Config, PlatformConfig,
-    RiscvVirtualMemory,
+    emulate_kernel_boot, emulate_kernel_boot_partial, AddressSpaceConstants, Arch, Config,
+    ObjectSizes, PlatformConfig, RiscvVirtualMemory,
 };
 use microkit_tool::symbols::patch_symbols;
 use microkit_tool::util::{
@@ -95,6 +95,17 @@ fn bail_if_not_exists(description: &'static str, path: &Path) -> Result<(), Stri
     Ok(())
 }
 
+fn parse_json_file<T: serde::de::DeserializeOwned>(
+    file_name: &str,
+    file_description: &'static str,
+    current_config: &AvailableConfig,
+) -> Result<T, String> {
+    let path = current_config.config_dir.join(file_name);
+    bail_if_not_exists(file_description, &path)?;
+    serde_json::from_str(&fs::read_to_string(&path).expect("Error: Unable to read {path}"))
+        .map_err(|err| format!("Error: Unable to parse {file_name}: {err}"))
+}
+
 fn main() -> Result<(), String> {
     let sdk = match Sdk::discover() {
         Ok(discovered_info) => discovered_info,
@@ -197,12 +208,17 @@ fn main() -> Result<(), String> {
         }
     };
 
-    let object_sizes = {
-        let object_sizes_path = current_config.config_dir.join("object_sizes.json");
-        bail_if_not_exists("kernel object sizes file", &object_sizes_path)?;
+    let object_sizes: ObjectSizes = parse_json_file(
+        "object_sizes.json",
+        "kernel object sizes file",
+        current_config,
+    )?;
 
-        serde_json::from_str(&fs::read_to_string(object_sizes_path).unwrap()).unwrap()
-    };
+    let address_space_constants: AddressSpaceConstants = parse_json_file(
+        "address_space_constants.json",
+        "kernel address space constants file",
+        current_config,
+    )?;
 
     let hypervisor = match arch {
         Arch::Aarch64 => json_str_as_bool(&kernel_config_json, "ARM_HYPERVISOR_SUPPORT")?,
@@ -238,7 +254,7 @@ fn main() -> Result<(), String> {
     let kernel_config = Config {
         arch,
         word_size: json_str_as_u64(&kernel_config_json, "WORD_SIZE")?,
-        minimum_page_size: 4096,
+        minimum_page_size: 1 << object_sizes.small_page,
         paddr_user_device_top: json_str_as_u64(&kernel_config_json, "PADDR_USER_DEVICE_TOP")?,
         kernel_frame_size,
         init_cnode_bits: json_str_as_u64(&kernel_config_json, "ROOT_CNODE_SIZE_BITS")?,
@@ -265,6 +281,7 @@ fn main() -> Result<(), String> {
         device_regions,
         normal_regions,
         object_sizes,
+        address_space_constants,
     };
 
     if kernel_config.arch != Arch::X86_64 && !loader_elf_path.exists() {

tool/microkit/src/sel4.rs

@@ -261,9 +261,23 @@ pub struct PlatformConfig {
     pub memory: Vec<PlatformConfigRegion>,
 }
 
+/// Deserialised from a generated 'address_space_constants.json' file in the SDK.
+#[derive(Debug, Deserialize)]
+pub struct AddressSpaceConstants {
+    pub page_table_index_bits: u64,
+    #[serde(default)]
+    /// Only included for aarch64 builds
+    pub vspace_index_bits: Option<u64>,
+    #[serde(default)]
+    // Only included for x86 VT-D builds
+    pub io_page_table_index_bits: Option<u64>,
+    /// seL4_UserVSpaceTop.
+    pub vspace_user_top: u64,
+}
+
 /// 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)]
+#[derive(Debug, Deserialize)]
 pub struct ObjectSizes {
     pub tcb: u64,
     pub endpoint: u64,
@@ -303,30 +317,15 @@ pub struct Config {
     pub riscv_pt_levels: Option<RiscvVirtualMemory>,
     pub invocations_labels: serde_json::Value,
     /// Kernel object sizes, used for kernel boot emulation and untyped allocation.
-    pub object_sizes: Option<ObjectSizes>,
+    pub object_sizes: ObjectSizes,
+    /// Kernel address space constants
+    pub address_space_constants: AddressSpaceConstants,
     /// The two remaining fields are only valid on ARM and RISC-V
     pub device_regions: Option<Vec<PlatformConfigRegion>>,
     pub normal_regions: Option<Vec<PlatformConfigRegion>>,
 }
 
 impl Config {
-    /// Refers to 'seL4_UserVSpaceTop'. Is inclusive.
-    // TODO: We should auto-extract this from libsel4 headers.
-    pub fn user_vspace_top(&self) -> u64 {
-        match self.arch {
-            Arch::Aarch64 => match self.hypervisor {
-                true => match self.arm_pa_size_bits.unwrap() {
-                    40 => 0x00ffffffffff,
-                    44 => 0x0fffffffffff,
-                    _ => panic!("Unknown ARM physical address size bits"),
-                },
-                false => 0x7fffffffffff,
-            },
-            Arch::Riscv64 => 0x0000003fffffefff,
-            Arch::X86_64 => 0x7fffffffefff,
-        }
-    }
-
     /// Refers to the 'PPTR_BASE' define in kernel source
     pub fn virtual_base(&self) -> u64 {
         match self.arch {
@@ -350,7 +349,7 @@ impl Config {
     /// IPC Buffer is located at the highest possible virtual memory page
     pub fn pd_ipc_buffer(&self) -> u64 {
         // user_top is inclusive, so we mask off the bits inside the page.
-        self.user_vspace_top() & !(PageSize::Small as u64 - 1)
+        self.address_space_constants.vspace_user_top & !(PageSize::Small as u64 - 1)
     }
 
     /// The stack is located in the third highest possible virtual memory pages,
@@ -378,7 +377,7 @@ impl Config {
     /// Value is exclusive ..max)
     pub fn vm_map_max_vaddr(&self) -> u64 {
         // Add 1, because user_top is inclusive. Note this assumes no overflow.
-        self.user_vspace_top() + 1
+        self.address_space_constants.vspace_user_top + 1
     }
 
     pub fn paddr_to_kernel_vaddr(&self, paddr: u64) -> u64 {
@@ -404,6 +403,27 @@ impl Config {
             Arch::X86_64 => 4,
         }
     }
+
+    pub fn vspace_root_level(&self) -> usize {
+        if self.arch == Arch::Aarch64 && self.aarch64_vspace_s2_start_l1() {
+            1
+        } else {
+            0
+        }
+    }
+
+    pub fn vspace_level_index_bits(&self, level: usize) -> u64 {
+        assert!(level < self.num_page_table_levels());
+
+        if self.arch == Arch::Aarch64 && level == self.vspace_root_level() {
+            self.address_space_constants.vspace_index_bits.expect(
+                "Error: An Aarch64 build should have seL4_VSpaceIndexBits defined
+                    by seL4, captured in tool/microkit/address_space_constants.h",
+            )
+        } else {
+            self.address_space_constants.page_table_index_bits
+        }
+    }
 }
 
 #[derive(PartialEq, Clone, Copy, Eq)]
@@ -461,8 +481,7 @@ 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<u64> {
-        assert!(config.object_sizes.is_some());
-        let object_sizes = &config.object_sizes.as_ref().unwrap();
+        let object_sizes = &config.object_sizes;
         match self {
             ObjectType::Tcb => Some(object_sizes.tcb),
             ObjectType::Endpoint => Some(object_sizes.endpoint),

tool/microkit/tests/test.rs

@@ -11,6 +11,20 @@ use microkit_tool::{
 use serde_json::json;
 use std::path::Path;
 
+const DEFAULT_OBJECT_SIZES: sel4::ObjectSizes = sel4::ObjectSizes {
+    tcb: 0,
+    endpoint: 0,
+    notification: 0,
+    reply: 0,
+    vspace: 0,
+    page_table: 0,
+    huge_page: 0,
+    large_page: 0,
+    small_page: 0,
+    asid_pool: 0,
+    vcpu: None,
+};
+
 const DEFAULT_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config {
     arch: sel4::Arch::Aarch64,
     word_size: 64,
@@ -32,7 +46,13 @@ const DEFAULT_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config {
     invocations_labels: json!(null),
     device_regions: None,
     normal_regions: None,
-    object_sizes: None,
+    object_sizes: DEFAULT_OBJECT_SIZES,
+    address_space_constants: sel4::AddressSpaceConstants {
+        page_table_index_bits: 9,
+        vspace_index_bits: Some(10),
+        io_page_table_index_bits: None,
+        vspace_user_top: 0xffffffffff,
+    },
 };
 
 const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config {
@@ -56,7 +76,13 @@ const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config {
     invocations_labels: json!(null),
     device_regions: None,
     normal_regions: None,
-    object_sizes: None,
+    object_sizes: DEFAULT_OBJECT_SIZES,
+    address_space_constants: sel4::AddressSpaceConstants {
+        page_table_index_bits: 9,
+        vspace_index_bits: None,
+        io_page_table_index_bits: Some(9),
+        vspace_user_top: 0x7fffffffefff,
+    },
 };
 
 fn check_success(kernel_config: &sel4::Config, test_name: &str) {