diff --git a/build_sdk.py b/build_sdk.py
index f29131a59..59e82f65e 100644
--- a/build_sdk.py
+++ b/build_sdk.py
@@ -774,7 +774,7 @@ def build_initialiser(
else:
capdl_init_elf = custom_rust_sel4_dir / "target" / cargo_target / "release" / "sel4-capdl-initializer.elf"
cmd = f"""
- cd {custom_rust_sel4_dir} && SEL4_PREFIX={sel4_src_dir.absolute()} {cargo_env} \
+ cd {custom_rust_sel4_dir} && SEL4_PREFIX={sel4_src_dir.absolute()} \
cargo build {cargo_cross_options} --target {cargo_target} \
--release -p sel4-capdl-initializer
"""
diff --git a/docs/manual.md b/docs/manual.md
index b872c3fb2..f8ef925ac 100644
--- a/docs/manual.md
+++ b/docs/manual.md
@@ -751,6 +751,7 @@ The `ioport` element has the following attributes:
* `addr`: The base address of the I/O port.
* `size`: The size in bytes of the I/O port region.
* `setvar_id`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the I/O port identifier.
+* `setvar_addr`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the base address of the I/O port.
The `setvar` element has the following attributes:
diff --git a/example/ethernet/ethernet.system b/example/ethernet/ethernet.system
index 9857717af..3e1e3ed39 100644
--- a/example/ethernet/ethernet.system
+++ b/example/ethernet/ethernet.system
@@ -44,7 +44,7 @@
-
+
diff --git a/example/hierarchy/hierarchy.system b/example/hierarchy/hierarchy.system
index 55bddebb6..39d116949 100644
--- a/example/hierarchy/hierarchy.system
+++ b/example/hierarchy/hierarchy.system
@@ -5,9 +5,9 @@
SPDX-License-Identifier: BSD-2-Clause
-->
-
+
-
+
diff --git a/example/rust/rust.system b/example/rust/rust.system
index 146da4bab..4722a5f9f 100644
--- a/example/rust/rust.system
+++ b/example/rust/rust.system
@@ -5,7 +5,7 @@
SPDX-License-Identifier: BSD-2-Clause
-->
-
+
\ No newline at end of file
diff --git a/example/setvar/Makefile b/example/setvar/Makefile
new file mode 100644
index 000000000..36d178de8
--- /dev/null
+++ b/example/setvar/Makefile
@@ -0,0 +1,58 @@
+#
+# Copyright 2025, UNSW.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+ifeq ($(strip $(BUILD_DIR)),)
+$(error BUILD_DIR must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_SDK)),)
+$(error MICROKIT_SDK must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_BOARD)),)
+$(error MICROKIT_BOARD must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_CONFIG)),)
+$(error MICROKIT_CONFIG must be specified)
+endif
+
+BOARD_DIR := $(MICROKIT_SDK)/board/$(MICROKIT_BOARD)/$(MICROKIT_CONFIG)
+
+ARCH := ${shell grep 'CONFIG_SEL4_ARCH ' $(BOARD_DIR)/include/kernel/gen_config.h | cut -d' ' -f4}
+
+ifeq ($(ARCH),aarch64)
+ TOOLCHAIN := aarch64-none-elf
+ # No specific AArch64 flags
+ CFLAGS_ARCH :=
+else
+$(error Unsupported ARCH)
+endif
+
+CC := $(TOOLCHAIN)-gcc
+LD := $(TOOLCHAIN)-ld
+AS := $(TOOLCHAIN)-as
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
+
+SETVAR_OBJS := setvar.o
+
+IMAGES := setvar.elf
+CFLAGS := -mstrict-align -nostdlib -ffreestanding -g -O3 -Wall -Wno-unused-function -Werror -I$(BOARD_DIR)/include $(CFLAGS_ARCH)
+LDFLAGS := -L$(BOARD_DIR)/lib
+LIBS := -lmicrokit -Tmicrokit.ld
+
+IMAGE_FILE = $(BUILD_DIR)/loader.img
+REPORT_FILE = $(BUILD_DIR)/report.txt
+
+all: $(IMAGE_FILE)
+
+$(BUILD_DIR)/%.o: %.c Makefile
+ $(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/setvar.elf: $(addprefix $(BUILD_DIR)/, $(SETVAR_OBJS))
+ $(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) setvar.system
+ $(MICROKIT_TOOL) setvar.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
diff --git a/example/setvar/README.md b/example/setvar/README.md
new file mode 100644
index 000000000..5315c45ac
--- /dev/null
+++ b/example/setvar/README.md
@@ -0,0 +1,21 @@
+
+# Example - setvar
+
+This is a basic example that demonstrate how to use some `setvar` functionalities that the Microkit provides.
+
+Only QEMU virt (AArch64) is supported in this example. Although everything will work the same way on other
+platforms, but on x86-64 `
+#include
+
+uint64_t mr_with_paddr_vaddr;
+uint64_t mr_with_paddr_paddr;
+
+uint64_t small_mr_no_paddr_paddr;
+uint64_t large_mr_no_paddr_paddr;
+
+uint64_t pl011_paddr;
+
+void init(void)
+{
+ microkit_dbg_puts("Virtual address of 'mr_with_paddr': ");
+ microkit_dbg_put32(mr_with_paddr_vaddr);
+ microkit_dbg_puts("\n");
+ microkit_dbg_puts("Physical address of 'mr_with_paddr': ");
+ microkit_dbg_put32(mr_with_paddr_paddr);
+ microkit_dbg_puts("\n");
+
+ microkit_dbg_puts("Physical address of 'small_mr_no_paddr': ");
+ microkit_dbg_put32(small_mr_no_paddr_paddr);
+ microkit_dbg_puts("\n");
+ microkit_dbg_puts("Physical address of 'large_mr_no_paddr': ");
+ microkit_dbg_put32(large_mr_no_paddr_paddr);
+ microkit_dbg_puts("\n");
+
+ microkit_dbg_puts("Physical address of 'pl011_paddr': ");
+ microkit_dbg_put32(pl011_paddr);
+ microkit_dbg_puts("\n");
+}
+
+void notified(microkit_channel ch)
+{
+}
diff --git a/example/setvar/setvar.system b/example/setvar/setvar.system
new file mode 100644
index 000000000..f5ef8cd19
--- /dev/null
+++ b/example/setvar/setvar.system
@@ -0,0 +1,27 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/example/x86_64_ioport/x86_64_ioport.c b/example/x86_64_ioport/x86_64_ioport.c
index 83a853a6e..65a2b8bef 100644
--- a/example/x86_64_ioport/x86_64_ioport.c
+++ b/example/x86_64_ioport/x86_64_ioport.c
@@ -6,13 +6,13 @@
#include
#include
-#define SERIAL_IOPORT_ID 0
-#define SERIAL_IOPORT_ADDRESS 0x3f8
+uint64_t com1_ioport_id;
+uint64_t com1_ioport_addr;
static inline void serial_putc(char ch)
{
// Danger: may overflow hardware FIFO, but we are only writing a small message.
- microkit_x86_ioport_write_8(SERIAL_IOPORT_ID, SERIAL_IOPORT_ADDRESS, ch);
+ microkit_x86_ioport_write_8(com1_ioport_id, com1_ioport_addr, ch);
}
static inline void serial_puts(const char *s)
diff --git a/example/x86_64_ioport/x86_64_ioport.system b/example/x86_64_ioport/x86_64_ioport.system
index 02fb63e38..2b0a1b21c 100644
--- a/example/x86_64_ioport/x86_64_ioport.system
+++ b/example/x86_64_ioport/x86_64_ioport.system
@@ -7,6 +7,6 @@
-
+
diff --git a/tool/microkit/src/capdl/allocation.rs b/tool/microkit/src/capdl/allocation.rs
index 69bf35562..a82808767 100644
--- a/tool/microkit/src/capdl/allocation.rs
+++ b/tool/microkit/src/capdl/allocation.rs
@@ -13,6 +13,11 @@ use crate::{
UntypedObject,
};
+pub enum CapDLAllocEmulationErrorLevel {
+ Suppressed,
+ PrintStderr,
+}
+
/// For the given spec and list of untypeds, simulate the CapDL initialiser's
/// object allocation algorithm. Record each object's paddr and UT's index in
/// its `expected_alloc` struct field. Assumes that the spec objects are sorted
@@ -23,6 +28,7 @@ pub fn simulate_capdl_object_alloc_algorithm(
spec: &mut CapDLSpec,
kernel_boot_info: &BootInfo,
kernel_config: &Config,
+ error_reporting_level: CapDLAllocEmulationErrorLevel,
) -> bool {
// Step 1: sort untypeds by paddr.
// We don't want to mess with the original order in `kernel_boot_info` as we will patch
@@ -84,13 +90,23 @@ pub fn simulate_capdl_object_alloc_algorithm(
if !(candidate_ut_range.start <= paddr_range.start
&& candidate_ut_range.end >= paddr_range.end)
{
- eprintln!("ERROR: object '{}', with paddr 0x{:0>12x}..0x{:0>12x} is not in any valid memory region.", named_obj.name, paddr_range.start, paddr_range.end);
+ if matches!(
+ error_reporting_level,
+ CapDLAllocEmulationErrorLevel::PrintStderr
+ ) {
+ eprintln!("ERROR: object '{}', with paddr 0x{:0>12x}..0x{:0>12x} is not in any valid memory region.", named_obj.name, paddr_range.start, paddr_range.end);
+ }
phys_addrs_ok = false;
}
}
}
- if !phys_addrs_ok {
+ if !phys_addrs_ok
+ && 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) {
@@ -204,10 +220,15 @@ pub fn simulate_capdl_object_alloc_algorithm(
oom = true;
let shortfall = (obj_id_range.end - obj_id_range.start) as u64;
let individual_sz = (1 << size_bit) as u64;
- eprintln!(
- "ERROR: ran out of untypeds for allocating objects of size {}, still need to create {} objects which requires {} of additional memory.",
- human_size_strict(individual_sz), shortfall, human_size_strict(individual_sz * shortfall)
- );
+ if matches!(
+ error_reporting_level,
+ CapDLAllocEmulationErrorLevel::PrintStderr
+ ) {
+ eprintln!(
+ "ERROR: ran out of untypeds for allocating objects of size {}, still need to create {} objects which requires {} of additional memory.",
+ human_size_strict(individual_sz), shortfall, human_size_strict(individual_sz * shortfall)
+ );
+ }
}
}
}
diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs
index 67476cc9f..be19db732 100644
--- a/tool/microkit/src/capdl/builder.rs
+++ b/tool/microkit/src/capdl/builder.rs
@@ -488,7 +488,7 @@ pub fn build_capdl_spec(
for frame_sequence in 0..mr.page_count {
let paddr = mr
- .phys_addr
+ .paddr()
.map(|base_paddr| (base_paddr + (frame_sequence * mr.page_size_bytes())) as usize);
frame_ids.push(capdl_util_make_frame_obj(
&mut spec,
diff --git a/tool/microkit/src/capdl/initialiser.rs b/tool/microkit/src/capdl/initialiser.rs
index 6ce7d3682..b5574dc9c 100644
--- a/tool/microkit/src/capdl/initialiser.rs
+++ b/tool/microkit/src/capdl/initialiser.rs
@@ -18,11 +18,16 @@ const INITIALISER_HEAP_ADD_ON_CONSTANT: u64 = 16 * 4096;
// Page size used for allocating the spec and heap segments.
pub const INITIALISER_GRANULE_SIZE: PageSize = PageSize::Small;
+pub struct CapDLInitialiserSpecMetadata {
+ pub spec_size: u64,
+ pub heap_size: u64,
+}
+
pub struct CapDLInitialiser {
pub elf: ElfFile,
pub heap_multiplier: f64,
- pub spec_size: Option,
- pub heap_size: Option,
+ pub phys_base: Option,
+ pub spec_metadata: Option,
}
impl CapDLInitialiser {
@@ -30,8 +35,8 @@ impl CapDLInitialiser {
CapDLInitialiser {
elf,
heap_multiplier,
- spec_size: None,
- heap_size: None,
+ phys_base: None,
+ spec_metadata: None,
}
}
@@ -40,7 +45,7 @@ impl CapDLInitialiser {
}
pub fn add_spec(&mut self, payload: Vec) {
- if self.spec_size.is_some() || self.heap_size.is_some() {
+ if self.spec_metadata.is_some() {
unreachable!("internal bug: CapDLInitialiser::add_spec() called more than once");
}
@@ -104,17 +109,28 @@ impl CapDLInitialiser {
)
.unwrap();
- self.spec_size = Some(spec_size);
- self.heap_size = Some(heap_size);
+ self.spec_metadata = Some(CapDLInitialiserSpecMetadata {
+ spec_size,
+ heap_size,
+ });
+ }
+
+ pub fn spec_metadata(&self) -> &Option {
+ &self.spec_metadata
+ }
+
+ pub fn have_spec(&self) -> bool {
+ self.spec_metadata.is_some()
}
pub fn replace_spec(&mut self, new_payload: Vec) {
- if self.spec_size.is_none() || self.heap_size.is_none() {
+ if self.spec_metadata.is_none() {
unreachable!("internal bug: CapDLInitialiser::replace_spec() called when no spec have been added before");
}
self.elf.segments.pop();
self.elf.segments.pop();
+ self.spec_metadata = None;
self.add_spec(new_payload);
}
@@ -134,4 +150,8 @@ impl CapDLInitialiser {
.write_symbol("sel4_capdl_initializer_expected_untypeds_list", &uts_desc)
.unwrap();
}
+
+ pub fn set_phys_base(&mut self, phys_base: u64) {
+ self.phys_base = Some(phys_base);
+ }
}
diff --git a/tool/microkit/src/capdl/mod.rs b/tool/microkit/src/capdl/mod.rs
index e6f2d48f4..88a8d7339 100644
--- a/tool/microkit/src/capdl/mod.rs
+++ b/tool/microkit/src/capdl/mod.rs
@@ -9,9 +9,8 @@ pub mod builder;
pub mod initialiser;
mod irq;
mod memory;
-pub mod reserialise_spec;
+pub mod packaging;
pub mod spec;
mod util;
pub use self::builder::*;
-pub use self::reserialise_spec::*;
diff --git a/tool/microkit/src/capdl/reserialise_spec.rs b/tool/microkit/src/capdl/packaging.rs
similarity index 63%
rename from tool/microkit/src/capdl/reserialise_spec.rs
rename to tool/microkit/src/capdl/packaging.rs
index b6d09e82a..e0b90ef3d 100644
--- a/tool/microkit/src/capdl/reserialise_spec.rs
+++ b/tool/microkit/src/capdl/packaging.rs
@@ -1,22 +1,26 @@
//
-// Copyright 2023, Colias Group, LLC
// Copyright 2025, UNSW
//
// SPDX-License-Identifier: BSD-2-Clause
//
+use std::ops::Range;
+
+use sel4_capdl_initializer_types::{
+ DeflatedBytesContent, IndirectDeflatedBytesContent, IndirectObjectName, ObjectNamesLevel, Spec,
+};
+
+use crate::{
+ capdl::{initialiser::CapDLInitialiser, spec::ElfContent, CapDLSpec},
+ elf::ElfFile,
+};
+
// A simple reimplementation of
// https://github.com/seL4/rust-sel4/blob/6f8d1baaad3aaca6f20966a2acb40e4651546519/crates/sel4-capdl-initializer/add-spec/src/reserialize_spec.rs
// We can't reuse the original code because it assumes that we are loading ELF frames from files.
// Which isn't suitable for Microkit as we want to embed the frames' data directly into the spec for
// easily patching ELF symbols.
-use std::ops::Range;
-
-use sel4_capdl_initializer_types::*;
-
-use crate::{capdl::spec::ElfContent, elf::ElfFile};
-
// @billn TODO: instead of doing this serialise our type -> deserialise into their type -> serialise business
// we can directly insert IndirectObjectName and IndirectDeflatedBytesContent into our spec type
// and one shot serialise at the cost of more complicated type definitions in spec.rs.
@@ -24,7 +28,7 @@ use crate::{capdl::spec::ElfContent, elf::ElfFile};
// Given a `Spec` data structure from sel4_capdl_initializer_types, "flatten" it into a vector of bytes
// for encapsulating it into the CapDL initialiser ELF.
-pub fn reserialise_spec(
+fn reserialise_spec(
elfs: &[ElfFile],
input_spec: &Spec<'static, String, ElfContent, ()>,
object_names_level: &ObjectNamesLevel,
@@ -81,3 +85,39 @@ impl SourcesBuilder {
start..end
}
}
+
+pub fn pack_spec_into_initial_task(
+ build_config: &str,
+ spec: &CapDLSpec,
+ system_elfs: &[ElfFile],
+ capdl_initialiser: &mut CapDLInitialiser,
+) {
+ // Reserialise the spec into a type that can be understood by rust-sel4.
+ let spec_reserialised = {
+ let spec_as_json = serde_json::to_string(&spec).unwrap();
+
+ // The full type definition is `Spec<'a, N, D, M>` where:
+ // N = object name type
+ // D = frame fill data type
+ // M = embedded frame data type
+ // Only N and D is useful for Microkit.
+ serde_json::from_str::>(&spec_as_json).unwrap()
+ };
+
+ // Now embed the built spec into the CapDL initialiser.
+ let name_level = match build_config {
+ "debug" => ObjectNamesLevel::All,
+ // We don't copy over the object names as there is no debug printing in these configuration to save memory.
+ "release" | "benchmark" => ObjectNamesLevel::None,
+ _ => panic!("unknown configuration {build_config}"),
+ };
+
+ let capdl_spec_as_binary = reserialise_spec(system_elfs, &spec_reserialised, &name_level);
+
+ // Patch the spec and heap into the ELF image.
+ if capdl_initialiser.have_spec() {
+ capdl_initialiser.replace_spec(capdl_spec_as_binary);
+ } else {
+ capdl_initialiser.add_spec(capdl_spec_as_binary);
+ }
+}
diff --git a/tool/microkit/src/lib.rs b/tool/microkit/src/lib.rs
index f0a33764a..10ba1f258 100644
--- a/tool/microkit/src/lib.rs
+++ b/tool/microkit/src/lib.rs
@@ -6,7 +6,10 @@
use std::{cmp::min, fmt};
-use crate::{sel4::Config, util::struct_to_bytes};
+use crate::{
+ sel4::{Config, PageSize},
+ util::struct_to_bytes,
+};
pub mod capdl;
pub mod elf;
@@ -187,7 +190,7 @@ impl MemoryRegion {
}
}
-#[derive(Default, Debug)]
+#[derive(Default, Debug, Clone)]
pub struct DisjointMemoryRegion {
pub regions: Vec,
}
@@ -205,6 +208,13 @@ impl DisjointMemoryRegion {
}
pub fn insert_region(&mut self, base: u64, end: u64) {
+ assert!(base < end);
+
+ if self.regions.is_empty() {
+ self.regions.push(MemoryRegion::new(base, end));
+ return;
+ }
+
let mut insert_idx = self.regions.len();
for (idx, region) in self.regions.iter().enumerate() {
if end <= region.base {
@@ -212,10 +222,19 @@ impl DisjointMemoryRegion {
break;
}
}
- // FIXME: Should extend here if adjacent rather than
- // inserting now
- self.regions
- .insert(insert_idx, MemoryRegion::new(base, end));
+ // Merge if contiguous
+ if insert_idx == 0 && self.regions.first().unwrap().base == end {
+ self.regions.first_mut().unwrap().base = base;
+ } else if insert_idx == self.regions.len() && self.regions.last().unwrap().end == base {
+ self.regions.last_mut().unwrap().end = end;
+ } else if insert_idx < self.regions.len() && end == self.regions[insert_idx].base {
+ self.regions[insert_idx].base = base;
+ } else if insert_idx < self.regions.len() && base == self.regions[insert_idx].end {
+ self.regions[insert_idx].end = end;
+ } else {
+ self.regions
+ .insert(insert_idx, MemoryRegion::new(base, end));
+ }
self.check();
}
@@ -269,29 +288,34 @@ impl DisjointMemoryRegion {
/// Allocate region of 'size' bytes, returning the base address.
/// The allocated region is removed from the disjoint memory region.
- /// Allocation policy is simple first fit.
+ /// Allocation policy is simple first fit in bottom up direction.
/// Possibly a 'best fit' policy would be better.
/// 'best' may be something that best matches a power-of-two
/// allocation
- pub fn allocate(&mut self, size: u64) -> u64 {
+ pub fn allocate(&mut self, size: u64, align_page_sz: PageSize) -> Option {
let mut region_to_remove: Option = None;
- for region in &self.regions {
- if size <= region.size() {
+
+ for region in self.regions.iter() {
+ if size <= region.size()
+ && region.base.next_multiple_of(align_page_sz as u64) + size <= region.end
+ {
region_to_remove = Some(*region);
break;
}
}
+ // Got a region that fits, block out the target area, split up the remaining region if necessary.
match region_to_remove {
Some(region) => {
- self.remove_region(region.base, region.base + size);
- region.base
+ let base = region.base.next_multiple_of(align_page_sz as u64);
+ self.remove_region(base, base + size);
+ Some(base)
}
- None => panic!("Unable to allocate {size} bytes"),
+ None => None,
}
}
- pub fn allocate_from(&mut self, size: u64, lower_bound: u64) -> u64 {
+ pub fn allocate_from(&mut self, size: u64, lower_bound: u64) -> Option {
let mut region_to_remove = None;
for region in &self.regions {
if size <= region.size() && region.base >= lower_bound {
@@ -303,9 +327,9 @@ impl DisjointMemoryRegion {
match region_to_remove {
Some(region) => {
self.remove_region(region.base, region.base + size);
- region.base
+ Some(region.base)
}
- None => panic!("Unable to allocate {size} bytes from lower_bound 0x{lower_bound:x}"),
+ None => None,
}
}
}
diff --git a/tool/microkit/src/loader.rs b/tool/microkit/src/loader.rs
index 453bc1b64..08e81cdf8 100644
--- a/tool/microkit/src/loader.rs
+++ b/tool/microkit/src/loader.rs
@@ -129,7 +129,7 @@ impl<'a> Loader<'a> {
kernel_elf: &'a ElfFile,
initial_task_elf: &'a ElfFile,
initial_task_phy_base: u64,
- initial_task_vaddr_range: Range,
+ initial_task_vaddr_range: &Range,
) -> Loader<'a> {
if config.arch == Arch::X86_64 {
unreachable!("internal error: x86_64 does not support creating a loader image");
diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs
index 4ee3b37ff..adda0ad4e 100644
--- a/tool/microkit/src/main.rs
+++ b/tool/microkit/src/main.rs
@@ -7,25 +7,30 @@
// we want our asserts, even if the compiler figures out they hold true already during compile-time
#![allow(clippy::assertions_on_constants)]
-use microkit_tool::capdl::allocation::simulate_capdl_object_alloc_algorithm;
+use microkit_tool::capdl::allocation::{
+ simulate_capdl_object_alloc_algorithm, CapDLAllocEmulationErrorLevel,
+};
+use microkit_tool::capdl::build_capdl_spec;
use microkit_tool::capdl::initialiser::{CapDLInitialiser, DEFAULT_INITIALISER_HEAP_MULTIPLIER};
-use microkit_tool::capdl::spec::ElfContent;
-use microkit_tool::capdl::{build_capdl_spec, reserialise_spec};
+use microkit_tool::capdl::packaging::pack_spec_into_initial_task;
use microkit_tool::elf::ElfFile;
use microkit_tool::loader::Loader;
use microkit_tool::report::write_report;
-use microkit_tool::sdf::parse;
+use microkit_tool::sdf::{parse, SysMemoryRegion, SysMemoryRegionPaddr};
use microkit_tool::sel4::{
emulate_kernel_boot, emulate_kernel_boot_partial, Arch, Config, PlatformConfig,
RiscvVirtualMemory,
};
use microkit_tool::symbols::patch_symbols;
-use microkit_tool::util::{human_size_strict, json_str, json_str_as_bool, json_str_as_u64};
-use microkit_tool::MemoryRegion;
-use sel4_capdl_initializer_types::{ObjectNamesLevel, Spec};
+use microkit_tool::util::{
+ human_size_strict, json_str, json_str_as_bool, json_str_as_u64, round_down, round_up,
+};
+use microkit_tool::{DisjointMemoryRegion, MemoryRegion};
use std::fs::{self, metadata};
use std::path::{Path, PathBuf};
+const MAX_BUILD_ITERATION: usize = 3;
+
fn get_full_path(path: &Path, search_paths: &Vec) -> Option {
for search_path in search_paths {
let full_path = search_path.join(path);
@@ -495,7 +500,7 @@ fn main() -> Result<(), String> {
"Microkit tool has various assumptions about the word size being 64-bits."
);
- let system = match parse(args.system, &xml, &kernel_config) {
+ let mut system = match parse(args.system, &xml, &kernel_config) {
Ok(system) => system,
Err(err) => {
eprintln!("{err}");
@@ -503,7 +508,33 @@ fn main() -> Result<(), String> {
}
};
- let mut monitor_elf = ElfFile::from_path(&monitor_elf_path)?;
+ let capdl_initialiser_elf = ElfFile::from_path(&capdl_init_elf_path).unwrap();
+
+ // Only relevant for ARM and RISC-V.
+ // Determine how much physical memory is available to the kernel after it boots but before dropping
+ // to userspace by partially emulating the kernel boot process. This is useful for two purposes:
+ // 1. To implement setvar region_paddr for memory regions that doesn't specify a phys address, where
+ // we must automatically select a suitable address inside the Microkit tool.
+ // 2. Post-spec generation sanity checks at a later point to ensure that there are sufficient memory
+ // to allocate all kernel objects.
+ let (kernel_elf_maybe, available_memory_maybe, kernel_boot_region_maybe) =
+ match kernel_config.arch {
+ Arch::X86_64 => (None, None, None),
+ Arch::Aarch64 | Arch::Riscv64 => {
+ let kernel_elf = ElfFile::from_path(&kernel_elf_path).unwrap();
+
+ // Now determine how much memory we have after the kernel boots.
+ let (available_memory, kernel_boot_region) =
+ emulate_kernel_boot_partial(&kernel_config, &kernel_elf);
+ (
+ Some(kernel_elf),
+ Some(available_memory),
+ Some(kernel_boot_region),
+ )
+ }
+ };
+
+ let monitor_elf = ElfFile::from_path(&monitor_elf_path)?;
let mut search_paths = vec![std::env::current_dir().unwrap()];
for path in args.search_paths {
@@ -528,159 +559,294 @@ fn main() -> Result<(), String> {
}
}
}
- // Patch all the required symbols in the Monitor and PDs according to the Microkit's requirements
- if let Err(err) = patch_symbols(&kernel_config, &mut system_elfs, &mut monitor_elf, &system) {
- eprintln!("ERROR: {err}");
- std::process::exit(1);
- }
// The monitor is just a special PD
system_elfs.push(monitor_elf);
- // We have parsed the XML and all ELF files, create the CapDL spec of the system described in the XML.
- let mut spec = build_capdl_spec(&kernel_config, &mut system_elfs, &system)?;
-
- // Reserialise the spec into a type that can be understood by rust-sel4.
- let spec_reserialised = {
- // Eagerly write out the spec so we can debug in case something crash later.
- let spec_as_json = if args.capdl_spec.is_some() {
- let serialised = serde_json::to_string_pretty(&spec).unwrap();
- fs::write(args.capdl_spec.unwrap(), &serialised).unwrap();
- serialised
- } else {
- serde_json::to_string(&spec).unwrap()
- };
- // The full type definition is `Spec<'a, N, D, M>` where:
- // N = object name type
- // D = frame fill data type
- // M = embedded frame data type
- // Only N and D is useful for Microkit.
- serde_json::from_str::>(&spec_as_json).unwrap()
- };
+ let mut capdl_initialiser =
+ CapDLInitialiser::new(capdl_initialiser_elf, args.initialiser_heap_size_multiplier);
- // Now embed the built spec into the CapDL initialiser.
- let name_level = match args.config {
- "debug" => ObjectNamesLevel::All,
- // We don't copy over the object names as there is no printing in these configuration to save memory.
- "release" | "benchmark" => ObjectNamesLevel::None,
- _ => panic!("unknown configuration {}", args.config),
- };
+ // 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.
+ let mut iteration = 0;
+ let mut spec_need_refinement = true;
+ let mut system_built = false;
+ while spec_need_refinement && iteration < MAX_BUILD_ITERATION {
+ spec_need_refinement = false;
- let num_objects = spec.objects.len();
- let capdl_spec_as_binary =
- reserialise_spec::reserialise_spec(&system_elfs, &spec_reserialised, &name_level);
+ // Patch all the required symbols in the Monitor and PDs according to the Microkit's requirements
+ if let Err(err) = patch_symbols(&kernel_config, &mut system_elfs, &system) {
+ eprintln!("ERROR: {err}");
+ std::process::exit(1);
+ }
- // Patch the spec and heap into the ELF image.
- let mut capdl_initialiser = CapDLInitialiser::new(
- ElfFile::from_path(&capdl_init_elf_path)?,
- args.initialiser_heap_size_multiplier,
- );
- capdl_initialiser.add_spec(capdl_spec_as_binary);
+ let mut spec = build_capdl_spec(&kernel_config, &mut system_elfs, &system)?;
+ pack_spec_into_initial_task(args.config, &spec, &system_elfs, &mut capdl_initialiser);
- println!(
- "MICROKIT|CAPDL SPEC: number of root objects = {}, spec footprint = {}, initialiser heap size = {}",
- num_objects,
- human_size_strict(capdl_initialiser.spec_size.unwrap()),
- human_size_strict(capdl_initialiser.heap_size.unwrap())
- );
- let initialiser_vaddr_range = capdl_initialiser.image_bound();
- println!(
- "MICROKIT|INITIAL TASK: memory size = {}",
- human_size_strict(initialiser_vaddr_range.end - initialiser_vaddr_range.start),
- );
+ match kernel_config.arch {
+ Arch::X86_64 => {
+ // setvar region_paddr not supported on this architecture nor can we emulate the
+ // kernel boot process to statically check for issues due to unknown memory map, so nothing to do.
+ // Write out the capDL initialiser as an ELF boot module and we are done.
+ }
+ Arch::Aarch64 | Arch::Riscv64 => {
+ // Now that we have the CapDL initialiser ELF with embedded spec,
+ // we can determine exactly how much memory will be available statically when the kernel
+ // drops to userspace on ARM and RISC-V. This allow us to sanity check that:
+ // 1. There are enough memory to allocate all the objects required in the spec.
+ // 2. All frames with a physical attached reside in legal memory (device or normal).
+ // 3. Objects can be allocated from the free untyped list. For example, we detect
+ // situations where you might have a few frames with size bit 12 to allocate but
+ // only have untyped with size bit <12 remaining.
+ // This also allow the tool to automatically pick physical address of Memory Regions with out
+ // an explicit paddr in SDF but are subject to setvar region_paddr.
+
+ // Determine how much memory the CapDL initialiser needs.
+ let initialiser_vaddr_range = capdl_initialiser.image_bound();
+ let initial_task_size = initialiser_vaddr_range.end - initialiser_vaddr_range.start;
+
+ // Reuse data from the partial kernel boot emulation previously done.
+ // .clone() as we need to mutate this for every iteration.
+ let mut available_memory = available_memory_maybe.clone().unwrap();
+ let kernel_boot_region = kernel_boot_region_maybe.unwrap();
+
+ // The kernel relies on the initial task region being allocated above the kernel
+ // boot/ELF region, so we have the end of the kernel boot region as the lower
+ // bound for allocating the reserved region.
+ let initial_task_phys_base_maybe =
+ available_memory.allocate_from(initial_task_size, kernel_boot_region.end);
+ if initial_task_phys_base_maybe.is_none() {
+ // Unlikely to happen on Microkit-supported platforms with multi gigabytes memory.
+ // But printing a helpful error in case we do run into this problem.
+ eprintln!(
+ "ERROR: cannot allocate memory for the initialiser, contiguous physical memory region of size {} not found", human_size_strict(initial_task_size)
+ );
+ eprintln!("ERROR: physical memory regions the initialiser can be placed at:");
+ for region in available_memory.regions {
+ eprintln!(
+ " [0x{:0>12x}..0x{:0>12x}), size: {}",
+ region.base,
+ region.end,
+ human_size_strict(region.size())
+ );
+ }
+ std::process::exit(1);
+ }
- // For x86 we write out the initialiser ELF as is, but on ARM and RISC-V we build the bootloader image.
- if kernel_config.arch == Arch::X86_64 {
- match capdl_initialiser.elf.reserialise(Path::new(args.output)) {
- Ok(size) => {
- println!(
- "MICROKIT|BOOT MODULE: image file size = {}",
- human_size_strict(size)
+ let initial_task_phys_base = initial_task_phys_base_maybe.unwrap();
+ capdl_initialiser.set_phys_base(initial_task_phys_base);
+ let initial_task_phys_region = MemoryRegion::new(
+ initial_task_phys_base,
+ initial_task_phys_base + initial_task_size,
+ );
+ let initial_task_virt_region = MemoryRegion::new(
+ capdl_initialiser.elf.lowest_vaddr(),
+ initialiser_vaddr_range.end,
);
- }
- Err(err) => {
- eprintln!("Error: couldn't write the boot module to filesystem: {err}");
- }
- }
- } else {
- // Now that we have the entire spec and CapDL initialiser ELF with embedded spec,
- // we can determine exactly how much memory will be available statically when the kernel
- // drops to userspace on ARM and RISC-V. This allow us to sanity check that:
- // 1. There are enough memory to allocate all the objects required in the spec.
- // 2. All frames with a physical attached reside in legal memory (device or normal).
- // 3. Objects can be allocated from the free untyped list. For example, we detect
- // situations where you might have a few frames with size bit 12 to allocate but
- // only have untyped with size bit <12 remaining.
-
- // We achieve this by emulating the kernel's boot process in the tool:
-
- // Determine how much memory the CapDL initialiser needs.
- let initial_task_size = initialiser_vaddr_range.end - initialiser_vaddr_range.start;
-
- // Parse the kernel's ELF to determine the kernel's window.
- let kernel_elf = ElfFile::from_path(&kernel_elf_path).unwrap();
-
- // Now determine how much memory we have after the kernel boots.
- let (mut available_memory, kernel_boot_region) =
- emulate_kernel_boot_partial(&kernel_config, &kernel_elf);
-
- // The kernel relies on the initial task region being allocated above the kernel
- // boot/ELF region, so we have the end of the kernel boot region as the lower
- // bound for allocating the reserved region.
- let initial_task_phys_base =
- available_memory.allocate_from(initial_task_size, kernel_boot_region.end);
-
- let initial_task_phys_region = MemoryRegion::new(
- initial_task_phys_base,
- initial_task_phys_base + initial_task_size,
- );
- let initial_task_virt_region = MemoryRegion::new(
- capdl_initialiser.elf.lowest_vaddr(),
- initialiser_vaddr_range.end,
- );
- // With the initial task region determined the kernel boot can be emulated. This provides
- // the boot info information which is needed for the next steps
- let kernel_boot_info = emulate_kernel_boot(
- &kernel_config,
- &kernel_elf,
- initial_task_phys_region,
- initial_task_virt_region,
- );
+ // With the initial task region determined the kernel boot can be emulated in full. This provides
+ // the boot info information (containing untyped objects) which is needed for the next steps
+ let kernel_boot_info = emulate_kernel_boot(
+ &kernel_config,
+ kernel_elf_maybe.as_ref().unwrap(),
+ initial_task_phys_region,
+ initial_task_virt_region,
+ );
- let alloc_ok =
- simulate_capdl_object_alloc_algorithm(&mut spec, &kernel_boot_info, &kernel_config);
- write_report(&spec, &kernel_config, args.report);
- if !alloc_ok {
- eprintln!("ERROR: could not allocate all required kernel objects. Please see report for more details.");
- std::process::exit(1);
- }
+ if iteration == 0 {
+ // On the first iteration where the spec have not been refined, simulate the capDL allocation algorithm
+ // to double check that all kernel objects of the system as described by SDF can be successfully allocated.
+ if !simulate_capdl_object_alloc_algorithm(
+ &mut spec,
+ &kernel_boot_info,
+ &kernel_config,
+ CapDLAllocEmulationErrorLevel::PrintStderr,
+ ) {
+ eprintln!("ERROR: could not allocate all required kernel objects. Please see report for more details.");
+ std::process::exit(1);
+ }
+ } else {
+ // Do the same thing for further iterations, at this point the simulation won't fail *except* for when we have picked a
+ // bad address for Memory Regions subject to setvar region_paddr. This can happen because after we have
+ // picked the address, we will update spec and patch it into the program's frame. Which will causes the
+ // spec to increase in size as the frames' data are compressed. So if the simulation fail, we need to
+ // pick another address as we now have a better idea of how large the spec is.
+
+ // This is highly unlikely to happen unless the spec size increase causes the initial task size to cross
+ // a 4K page boundary.
+ if !simulate_capdl_object_alloc_algorithm(
+ &mut spec,
+ &kernel_boot_info,
+ &kernel_config,
+ CapDLAllocEmulationErrorLevel::Suppressed,
+ ) {
+ // Encountered a problem, pick a better address.
+ for tool_allocate_mr in system.memory_regions.iter_mut().filter(|mr| {
+ matches!(mr.phys_addr, SysMemoryRegionPaddr::ToolAllocated(_))
+ }) {
+ tool_allocate_mr.phys_addr = SysMemoryRegionPaddr::ToolAllocated(None);
+ }
+ }
+ }
- // Everything checks out, patch the list of untypeds we used to simulate object allocation into the initialiser.
- // At runtime the intialiser will validate what we simulated against what the kernel gives it. If they deviate
- // we will have problems! For example, if we simulated with more memory than what's actually available, the initialiser
- // can crash.
- capdl_initialiser.add_expected_untypeds(&kernel_boot_info.untyped_objects);
-
- // Everything checks out, now build the bootloader!
- let loader = Loader::new(
- &kernel_config,
- Path::new(&loader_elf_path),
- &kernel_elf,
- &capdl_initialiser.elf,
- initial_task_phys_base,
- initialiser_vaddr_range,
- );
+ // Now pick a physical address for any memory regions that are subject to setvar region_paddr.
+ // Doing something a bit unconventional here: converting the list of untypeds back to a DisjointMemoryRegion
+ // to give us a view of physical memory available after the kernel drops to user space.
+ // I.e. available memory after the initial task have been created.
+ {
+ let mut available_user_memory = DisjointMemoryRegion::default();
+ for ut in kernel_boot_info
+ .untyped_objects
+ .iter()
+ .filter(|ut| !ut.is_device)
+ {
+ // Only take untypeds that can at least fit a page because some have been used to back the initial task's
+ // kernel object such as TCB, endpoint etc.
+ let start = round_up(ut.base(), kernel_config.minimum_page_size);
+ let end = round_down(ut.end(), kernel_config.minimum_page_size);
+ if end > start {
+ // will be automatically merged
+ available_user_memory.insert_region(ut.base(), ut.end());
+ }
+ }
+
+ // Then take away any memory ranges occupied by Memory Regions with a paddr specified in SDF.
+ for mr in system.memory_regions.iter() {
+ if let SysMemoryRegionPaddr::Specified(sdf_paddr) = mr.phys_addr {
+ let mr_end = sdf_paddr + mr.size;
+
+ // MR may be device memory, which isn't covered in available_user_memory.
+ let is_normal_mem =
+ available_user_memory.regions.iter().any(|region| {
+ sdf_paddr >= region.base
+ && sdf_paddr < region.end
+ && mr_end <= region.end
+ });
+ if is_normal_mem {
+ available_user_memory.remove_region(sdf_paddr, sdf_paddr + mr.size);
+ }
+ }
+ }
- loader.write_image(Path::new(args.output));
+ let mut tool_allocated_mrs = Vec::new();
+ for (mr_id, tool_allocate_mr) in system
+ .memory_regions
+ .iter_mut()
+ .enumerate()
+ .filter(|(_, mr)| {
+ matches!(mr.phys_addr, SysMemoryRegionPaddr::ToolAllocated(None))
+ })
+ {
+ spec_need_refinement = true;
+
+ let target_paddr = available_user_memory
+ .allocate(tool_allocate_mr.size, tool_allocate_mr.page_size);
+ if target_paddr.is_none() {
+ eprintln!("ERROR: cannot auto-select a physical address for MR {} because there are no contiguous memory region of sufficient size.", tool_allocate_mr.name);
+ eprintln!("ERROR: MR {} needs to be physically contiguous as it is a subject of a setvar region_paddr.", tool_allocate_mr.name);
+ if !tool_allocated_mrs.is_empty() {
+ eprintln!("Previously auto-allocated memory regions:");
+ for allocated_mr_id in tool_allocated_mrs {
+ let allocated_mr: &SysMemoryRegion =
+ &system.memory_regions[allocated_mr_id];
+ eprintln!(
+ "name = '{}', paddr = 0x{:0>12x}, size = 0x{:0>12x}",
+ allocated_mr.name,
+ allocated_mr.paddr().unwrap(),
+ allocated_mr.size
+ );
+ }
+ }
+ eprintln!("available physical memory regions:");
+ for region in available_user_memory.regions {
+ eprintln!(
+ "[0x{:0>12x}..0x{:0>12x}), size: {}",
+ region.base,
+ region.end,
+ human_size_strict(region.size())
+ );
+ }
+ std::process::exit(1);
+ }
+ tool_allocated_mrs.push(mr_id);
+ tool_allocate_mr.phys_addr =
+ SysMemoryRegionPaddr::ToolAllocated(target_paddr);
+ }
+ }
- println!(
- "MICROKIT|LOADER: image file size = {}",
- human_size_strict(metadata(args.output).unwrap().len())
- );
+ // Patch the list of untypeds we used to simulate object allocation into the initialiser.
+ // At runtime the intialiser will validate what we simulated against what the kernel gives it. If they deviate
+ // we will have problems! For example, if we simulated with more memory than what's actually available, the initialiser
+ // can crash.
+ capdl_initialiser.add_expected_untypeds(&kernel_boot_info.untyped_objects);
+ }
+ };
+
+ if !spec_need_refinement {
+ // All is well in the universe, write the image out.
+ println!(
+ "MICROKIT|CAPDL SPEC: number of root objects = {}, spec footprint = {}, initialiser heap size = {}",
+ spec.objects.len(),
+ human_size_strict(capdl_initialiser.spec_metadata().as_ref().unwrap().spec_size),
+ human_size_strict(capdl_initialiser.spec_metadata().as_ref().unwrap().heap_size)
+ );
+ let initialiser_vaddr_range = capdl_initialiser.image_bound();
+ println!(
+ "MICROKIT|INITIAL TASK: memory size = {}",
+ human_size_strict(initialiser_vaddr_range.end - initialiser_vaddr_range.start),
+ );
+
+ match kernel_config.arch {
+ Arch::X86_64 => match capdl_initialiser.elf.reserialise(Path::new(args.output)) {
+ Ok(size) => {
+ println!(
+ "MICROKIT|BOOT MODULE: image file size = {}",
+ human_size_strict(size)
+ );
+ }
+ Err(err) => {
+ eprintln!("ERROR: couldn't write the boot module to filesystem: {err}");
+ std::process::exit(1);
+ }
+ },
+ Arch::Aarch64 | Arch::Riscv64 => {
+ let loader = Loader::new(
+ &kernel_config,
+ Path::new(&loader_elf_path),
+ kernel_elf_maybe.as_ref().unwrap(),
+ &capdl_initialiser.elf,
+ capdl_initialiser.phys_base.unwrap(),
+ &initialiser_vaddr_range,
+ );
+
+ loader.write_image(Path::new(args.output));
+
+ println!(
+ "MICROKIT|LOADER: image file size = {}",
+ human_size_strict(metadata(args.output).unwrap().len())
+ );
+ }
+ };
+
+ if args.capdl_spec.is_some() {
+ let serialised = serde_json::to_string_pretty(&spec).unwrap();
+ fs::write(args.capdl_spec.unwrap(), &serialised).unwrap();
+ };
+
+ write_report(&spec, &kernel_config, args.report);
+ system_built = true;
+ break;
+ } else {
+ // Some memory regions have had their physical address updated, rebuild the spec.
+ iteration += 1;
+ }
}
- write_report(&spec, &kernel_config, args.report);
+ if !system_built {
+ // Cannot build a reasonable spec, absurd.
+ // Only reachable when there are setvar region_paddr that we keep selecting the wrong address.
+ panic!("ERROR: fatal, failed to build system in {iteration} iterations");
+ }
Ok(())
}
diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs
index 4971b2fb8..9803c913a 100644
--- a/tool/microkit/src/sdf.rs
+++ b/tool/microkit/src/sdf.rs
@@ -21,6 +21,7 @@ use crate::sel4::{
};
use crate::util::{ranges_overlap, str_to_bool};
use crate::MAX_PDS;
+use std::collections::HashSet;
use std::path::{Path, PathBuf};
/// Events that come through entry points (e.g notified or protected) are given an
@@ -101,6 +102,15 @@ pub enum SysMemoryRegionKind {
Stack,
}
+#[derive(Debug, PartialEq, Eq, Clone)]
+pub enum SysMemoryRegionPaddr {
+ Unspecified,
+ // ToolAllocated means that the MR doesn't have an explicit paddr in SDF, but
+ // is a subject of a setvar region_paddr.
+ ToolAllocated(Option),
+ Specified(u64),
+}
+
#[derive(Debug, PartialEq, Eq, Clone)]
pub struct SysMemoryRegion {
pub name: String,
@@ -108,7 +118,7 @@ pub struct SysMemoryRegion {
page_size_specified_by_user: bool,
pub page_size: PageSize,
pub page_count: u64,
- pub phys_addr: Option,
+ pub phys_addr: SysMemoryRegionPaddr,
pub text_pos: Option,
/// For error reporting is useful to know whether the MR was created
/// due to the user's SDF or created by the tool for setting up the
@@ -133,6 +143,14 @@ impl SysMemoryRegion {
pub fn page_size_bytes(&self) -> u64 {
self.page_size as u64
}
+
+ pub fn paddr(&self) -> Option {
+ match self.phys_addr {
+ SysMemoryRegionPaddr::Unspecified => None,
+ SysMemoryRegionPaddr::ToolAllocated(paddr_maybe) => paddr_maybe,
+ SysMemoryRegionPaddr::Specified(sdf_paddr) => Some(sdf_paddr),
+ }
+ }
}
#[derive(Debug, PartialEq, Eq)]
@@ -192,6 +210,7 @@ pub enum SysSetVarKind {
Vaddr { address: u64 },
Paddr { region: String },
Id { id: u64 },
+ X86IoPortAddr { address: u64 },
}
#[derive(Debug, PartialEq, Eq)]
@@ -859,7 +878,11 @@ impl ProtectionDomain {
}
"ioport" => {
if let Arch::X86_64 = config.arch {
- check_attributes(xml_sdf, &child, &["id", "setvar_id", "addr", "size"])?;
+ check_attributes(
+ xml_sdf,
+ &child,
+ &["id", "setvar_id", "setvar_addr", "addr", "size"],
+ )?;
let id = checked_lookup(xml_sdf, &child, "id")?
.parse::()
@@ -890,6 +913,14 @@ impl ProtectionDomain {
let addr =
sdf_parse_number(checked_lookup(xml_sdf, &child, "addr")?, &child)?;
+ if let Some(setvar_addr) = child.attribute("setvar_addr") {
+ let setvar = SysSetVar {
+ symbol: setvar_addr.to_string(),
+ kind: SysSetVarKind::X86IoPortAddr { address: addr },
+ };
+ checked_add_setvar(&mut setvars, setvar, xml_sdf, &child)?;
+ }
+
let size = checked_lookup(xml_sdf, &child, "size")?
.parse::()
.unwrap();
@@ -916,6 +947,17 @@ impl ProtectionDomain {
}
}
"setvar" => {
+ match config.arch {
+ Arch::Aarch64 | Arch::Riscv64 => {}
+ Arch::X86_64 => {
+ return Err(value_error(
+ xml_sdf,
+ node,
+ "setvar with 'region_paddr' for MR without a specified paddr is unsupported on x86_64".to_string(),
+ ));
+ }
+ };
+
check_attributes(xml_sdf, &child, &["symbol", "region_paddr"])?;
let symbol = checked_lookup(xml_sdf, &child, "symbol")?.to_string();
let region = checked_lookup(xml_sdf, &child, "region_paddr")?.to_string();
@@ -1161,17 +1203,20 @@ impl SysMemoryRegion {
}
let phys_addr = if let Some(xml_phys_addr) = node.attribute("phys_addr") {
- Some(sdf_parse_number(xml_phys_addr, node)?)
+ SysMemoryRegionPaddr::Specified(sdf_parse_number(xml_phys_addr, node)?)
} else {
- None
+ // At this point it is unsure whether this MR is a subject of a setvar region_paddr.
+ SysMemoryRegionPaddr::Unspecified
};
- if phys_addr.is_some() && !phys_addr.unwrap().is_multiple_of(page_size) {
- return Err(value_error(
- xml_sdf,
- node,
- "phys_addr is not aligned to the page size".to_string(),
- ));
+ if let SysMemoryRegionPaddr::Specified(sdf_paddr) = phys_addr {
+ if !sdf_paddr.is_multiple_of(page_size) {
+ return Err(value_error(
+ xml_sdf,
+ node,
+ "phys_addr is not aligned to the page size".to_string(),
+ ));
+ }
}
let page_count = size / page_size;
@@ -1800,9 +1845,9 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result= *end || mr_end <= *start) {
@@ -1872,8 +1917,8 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Result Result<(), String> {
// *********************************
// Step 1. Write ELF symbols in the monitor.
// *********************************
+ let monitor_elf = pd_elf_files.last_mut().unwrap();
+
let pd_names: Vec = system
.protection_domains
.iter()
@@ -150,22 +151,13 @@ pub fn patch_symbols(
let data = match &setvar.kind {
sdf::SysSetVarKind::Size { mr } => mr_name_to_desc.get(mr).unwrap().size,
sdf::SysSetVarKind::Vaddr { address } => *address,
- sdf::SysSetVarKind::Paddr { region } => {
- match mr_name_to_desc.get(region).unwrap().phys_addr {
- Some(specified_paddr) => specified_paddr,
- None => {
- if kernel_config.arch == Arch::X86_64 {
- return Err(
- "setvar with 'region_paddr' for MR without a specified paddr is unsupported on x86_64."
- .to_string(),
- );
- } else {
- panic!("setvar with 'region_paddr' for MR without a specified paddr is currently unimplemented!");
- }
- }
- }
- }
+ sdf::SysSetVarKind::Paddr { region } => mr_name_to_desc
+ .get(region)
+ .unwrap()
+ .paddr()
+ .unwrap_or_default(),
sdf::SysSetVarKind::Id { id } => *id,
+ sdf::SysSetVarKind::X86IoPortAddr { address } => *address,
};
symbols_to_write.push((&setvar.symbol, data));
}