diff --git a/build_sdk.py b/build_sdk.py index 18adbc7e1..e9c180f53 100644 --- a/build_sdk.py +++ b/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( diff --git a/tool/microkit/address_space_constants.h b/tool/microkit/address_space_constants.h new file mode 100644 index 000000000..9e86078ee --- /dev/null +++ b/tool/microkit/address_space_constants.h @@ -0,0 +1,21 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ + +#include +#include +#include +#include + +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 diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index 0129c6810..909b39463 100644 --- a/tool/microkit/src/main.rs +++ b/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( + file_name: &str, + file_description: &'static str, + current_config: &AvailableConfig, +) -> Result { + 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() { diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index bbeddecee..e23084848 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -261,9 +261,23 @@ pub struct PlatformConfig { pub memory: Vec, } +/// 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, + #[serde(default)] + // Only included for x86 VT-D builds + pub io_page_table_index_bits: Option, + /// 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, pub invocations_labels: serde_json::Value, /// Kernel object sizes, used for kernel boot emulation and untyped allocation. - pub object_sizes: Option, + 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>, pub normal_regions: Option>, } 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 { - 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), diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 24cb81256..3328d23d9 100644 --- a/tool/microkit/tests/test.rs +++ b/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) {