From 800649c6a4146916f8dd18073c216e590afdadbf Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Thu, 16 Jul 2026 10:09:28 +1000 Subject: [PATCH 1/2] tool: fix assertion fail if system need rebuild In main.rs, we build the system in multiple iterations to make setvar region_paddr works. However there was a bug in allocation.rs that did not return an error when the tool picked a bad physical address. The code will continue simulating the capDL allocation algorithm with bad physical addresses and cause the assert: assert_eq!(u64::from(named_obj.object.paddr().unwrap()), cur_paddr); to fail. Since the invariant that all physical addresses are valid at this point have been violated. This commit fixed the error check to always return an error. Signed-off-by: Bill Nguyen --- tool/microkit/src/capdl/allocation.rs | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/tool/microkit/src/capdl/allocation.rs b/tool/microkit/src/capdl/allocation.rs index 19e8736c9..f316e54cc 100644 --- a/tool/microkit/src/capdl/allocation.rs +++ b/tool/microkit/src/capdl/allocation.rs @@ -106,21 +106,22 @@ pub fn simulate_capdl_object_alloc_algorithm( } } - if !phys_addrs_ok - && matches!( + if !phys_addrs_ok { + if matches!( error_reporting_level, CapDLAllocEmulationErrorLevel::PrintStderr - ) - { - eprintln!("Below are the valid ranges of memory to be allocated from:"); - eprintln!("Valid ranges outside of main memory:"); - for (_i, ut) in untypeds_by_paddr.iter().filter(|(_i, ut)| ut.is_device) { - eprintln!(" [0x{:0>12x}..0x{:0>12x})", ut.base(), ut.end()); - } - eprintln!("Valid ranges within main memory:"); - for (_i, ut) in untypeds_by_paddr.iter().filter(|(_i, ut)| !ut.is_device) { - eprintln!(" [0x{:0>12x}..0x{:0>12x})", ut.base(), ut.end()); + ) { + eprintln!("Below are the valid ranges of memory to be allocated from:"); + eprintln!("Valid ranges outside of main memory:"); + for (_i, ut) in untypeds_by_paddr.iter().filter(|(_i, ut)| ut.is_device) { + eprintln!(" [0x{:0>12x}..0x{:0>12x})", ut.base(), ut.end()); + } + eprintln!("Valid ranges within main memory:"); + for (_i, ut) in untypeds_by_paddr.iter().filter(|(_i, ut)| !ut.is_device) { + eprintln!(" [0x{:0>12x}..0x{:0>12x})", ut.base(), ut.end()); + } } + return false; } From 60043611ec3d57ca715369b5b3b83fe7270619b6 Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Thu, 16 Jul 2026 10:18:12 +1000 Subject: [PATCH 2/2] tool: Fix PD image load in multi-iteration build In the system build process, the capDL initialiser object is mutated to pack the spec and estimate the available memory to user space. This process is iterative to work out the exact amout of available memory. But the code recycles the mutated object, which causes the PDs' program images to not be loaded correctly. We need to keep a fresh copy of the initialiser and use that fresh copy every iteration. Signed-off-by: Bill Nguyen --- tool/microkit/src/capdl/initialiser.rs | 2 ++ tool/microkit/src/main.rs | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/tool/microkit/src/capdl/initialiser.rs b/tool/microkit/src/capdl/initialiser.rs index d944b823e..548ddd713 100644 --- a/tool/microkit/src/capdl/initialiser.rs +++ b/tool/microkit/src/capdl/initialiser.rs @@ -21,6 +21,7 @@ pub const INITIALISER_GRANULE_SIZE: PageSize = PageSize::Small; const PT_SEL4_CAPDL_SPEC: u32 = 0x64c3_4003; const PT_SEL4_CAPDL_FRAME_DATA: u32 = 0x64c3_4004; +#[derive(Clone)] pub struct CapDLInitialiserSpecMetadata { pub spec_size: u64, } @@ -35,6 +36,7 @@ pub enum LogLevel { Trace = 5, } +#[derive(Clone)] pub struct CapDLInitialiser { pub elf: ElfFile, pub phys_base: Option, diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index ec83dff1d..dd6934e64 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -410,7 +410,7 @@ fn main() -> Result<(), String> { // The monitor is just a special PD system_elfs.push(monitor_elf); - let mut capdl_initialiser = CapDLInitialiser::new(capdl_initialiser_elf); + let capdl_initialiser_orig = CapDLInitialiser::new(capdl_initialiser_elf); // Now build the capDL spec and final image. We may need to do this in >1 iterations on ARM and RISC-V // if there are Memory Regions without a paddr but subject to setvar region_paddr. @@ -418,6 +418,7 @@ fn main() -> Result<(), String> { let mut spec_need_refinement = true; let mut system_built = false; while spec_need_refinement && iteration < MAX_BUILD_ITERATION { + let mut capdl_initialiser = capdl_initialiser_orig.clone(); spec_need_refinement = false; // Patch all the required symbols in the Monitor and PDs according to the Microkit's requirements