diff --git a/build_sdk.py b/build_sdk.py index c631b7e43..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,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,7 +753,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 +761,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 +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") 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) {