diff --git a/Cargo.toml b/Cargo.toml index 225db1c11..d5facdda8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,12 +12,16 @@ members = [ ] [workspace.dependencies.sel4-capdl-initializer] -git = "https://github.com/seL4/rust-seL4" -rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4" +git = "https://github.com/au-ts/rust-seL4" +branch = "szymon/handoff-untypeds" +#git = "https://github.com/seL4/rust-seL4" +#rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4" [workspace.dependencies.sel4-capdl-initializer-types] -git = "https://github.com/seL4/rust-seL4" -rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4" +git = "https://github.com/au-ts/rust-seL4" +branch = "szymon/handoff-untypeds" +#git = "https://github.com/seL4/rust-seL4" +#rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4" [profile.release.package.microkit-tool] strip = true diff --git a/example/handoff_untypeds/Makefile b/example/handoff_untypeds/Makefile new file mode 100644 index 000000000..6b2703219 --- /dev/null +++ b/example/handoff_untypeds/Makefile @@ -0,0 +1,72 @@ +# +# Copyright 2026, UNSW +# Copyright 2021, Breakaway Consulting Pty. Ltd. +# +# 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) + TARGET_TRIPLE := aarch64-none-elf + CFLAGS_ARCH := -mstrict-align +else ifeq ($(ARCH),riscv64) + TARGET_TRIPLE := riscv64-unknown-elf + CFLAGS_ARCH := -march=rv64imafdc_zicsr_zifencei -mabi=lp64d +else ifeq ($(ARCH),x86_64) + TARGET_TRIPLE := x86_64-elf + CFLAGS_ARCH := -march=x86-64 -mtune=generic +else +$(error Unsupported ARCH) +endif + +ifeq ($(strip $(LLVM)),True) + CC := clang -target $(TARGET_TRIPLE) + AS := clang -target $(TARGET_TRIPLE) + LD := ld.lld +else + CC := $(TARGET_TRIPLE)-gcc + LD := $(TARGET_TRIPLE)-ld + AS := $(TARGET_TRIPLE)-as +endif + +MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit + +HELLO_OBJS := hello.o + +IMAGES := hello.elf +CFLAGS := -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 +SPEC = $(BUILD_DIR)/capdl_spec.json + +all: $(IMAGE_FILE) + +$(BUILD_DIR)/%.o: %.c Makefile + $(CC) -c $(CFLAGS) $< -o $@ + +$(BUILD_DIR)/hello.elf: $(addprefix $(BUILD_DIR)/, $(HELLO_OBJS)) + $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ + +$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) handoff_untypeds.system + $(MICROKIT_TOOL) handoff_untypeds.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) --capdl-json ${SPEC} diff --git a/example/handoff_untypeds/README.md b/example/handoff_untypeds/README.md new file mode 100644 index 000000000..1215cd8d9 --- /dev/null +++ b/example/handoff_untypeds/README.md @@ -0,0 +1,23 @@ + +# Example - Handoff untypeds + +This is a basic example that has a single protection domain +that receives capabilities to all remaining untyped memory, +prints information about the untypeds upon initialisation and +has an example of using these untypeds for creating new kernel objects. + +All supported platforms are supported in this example. + +## Building + +```sh +mkdir build +make BUILD_DIR=build MICROKIT_BOARD= MICROKIT_CONFIG= MICROKIT_SDK=/path/to/sdk +``` + +## Running + +See instructions for your board in the manual. diff --git a/example/handoff_untypeds/handoff_untypeds.system b/example/handoff_untypeds/handoff_untypeds.system new file mode 100644 index 000000000..0ddc140d3 --- /dev/null +++ b/example/handoff_untypeds/handoff_untypeds.system @@ -0,0 +1,13 @@ + + + + + + + + + diff --git a/example/handoff_untypeds/hello.c b/example/handoff_untypeds/hello.c new file mode 100644 index 000000000..2baafb919 --- /dev/null +++ b/example/handoff_untypeds/hello.c @@ -0,0 +1,68 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include +//#include +#include + +uintptr_t remaining_untypeds_vaddr; +typedef struct { + seL4_CNode untyped_cnode_cptr; + seL4_SlotRegion untypeds; + seL4_UntypedDesc untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; +} capDLBootInfo_t; + +capDLBootInfo_t *capDLBootInfo; + +void print_64(seL4_Word w) { + microkit_dbg_put32((seL4_Uint32) (w >> 32)); + microkit_dbg_put32((seL4_Uint32) w); +} +void init(void) +{ + capDLBootInfo = (capDLBootInfo_t*) remaining_untypeds_vaddr; + microkit_dbg_puts("hello, world\nuntyped_cnode_cptr: "); + microkit_dbg_put32((seL4_Uint32) (capDLBootInfo->untyped_cnode_cptr >> 32)); + microkit_dbg_putc(32); + microkit_dbg_put32((seL4_Uint32) capDLBootInfo->untyped_cnode_cptr); + microkit_dbg_puts("\nend\n"); + + microkit_dbg_puts("idx paddr sizeBits isDevice\n"); + for (uint32_t i = capDLBootInfo->untypeds.start; i < capDLBootInfo->untypeds.end; i++) { + microkit_dbg_put32(i); + microkit_dbg_puts(" "); + print_64(capDLBootInfo->untypedList[i].paddr); + microkit_dbg_puts(" "); + print_64(capDLBootInfo->untypedList[i].sizeBits); + microkit_dbg_puts(" "); + if(capDLBootInfo->untypedList[i].isDevice) { + microkit_dbg_puts("true\n"); + } else { + microkit_dbg_puts("false\n"); + } + } + + // Try retype untyped idx 39 + uint32_t untyped_idx = 40; + microkit_dbg_puts("Creating new untyped from Untyped Idx "); + microkit_dbg_put32(untyped_idx); + microkit_dbg_puts(" of size 4 at idx "); + microkit_dbg_put32(capDLBootInfo->untypeds.end); + seL4_Error err = seL4_Untyped_Retype(capDLBootInfo->untyped_cnode_cptr + untyped_idx, seL4_UntypedObject, 4, capDLBootInfo->untyped_cnode_cptr, 0, 0, capDLBootInfo->untypeds.end, 1); + // XXX: add Capability to the root CNode for Djawula (maybe?) + //seL4_Error err = seL4_Untyped_Retype(capDLBootInfo->untyped_cnode_cptr + 39, seL4_CNodeObject, 4, (uint64_t) 2 << (64-6), 0, 0, 68, 1); + + microkit_dbg_puts("\nseL4_NoError: "); + microkit_dbg_put32(seL4_NoError); + microkit_dbg_puts("\n"); + microkit_dbg_puts("err: "); + microkit_dbg_put32(err); + microkit_dbg_puts("\n"); +} + +void notified(microkit_channel ch) +{ +} diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index c40575871..b6e86c8f4 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -246,6 +246,7 @@ impl CapDLSpecContainer { &format!("elf_{pd_name}_{frame_sequence:09}"), None, PageSize::Small.fixed_size_bits(sel4_config) as u8, + false, ); let frame_cap = capdl_util_make_frame_cap( frame_obj_id, @@ -286,6 +287,7 @@ impl CapDLSpecContainer { &format!("ipcbuf_{pd_name}"), None, PageSize::Small.fixed_size_bits(sel4_config) as u8, + false, ); let ipcbuf_frame_cap = capdl_util_make_frame_cap(ipcbuf_frame_obj_id, true, true, false, true); @@ -439,6 +441,7 @@ pub fn build_capdl_spec( capdl_util_make_cte(MON_REPLY_CAP_IDX as u32, mon_reply_cap), ] .to_vec(), + false, ); let mon_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; let mon_cnode_cap = capdl_util_make_cnode_cap(mon_cnode_obj_id, 0, mon_guard_size as u8); @@ -452,6 +455,7 @@ pub fn build_capdl_spec( &format!("{MONITOR_PD_NAME}_stack"), None, PageSize::Small.fixed_size_bits(kernel_config) as u8, + false, ); let mon_stack_frame_cap = capdl_util_make_frame_cap(mon_stack_frame_obj_id, true, true, false, true); @@ -506,6 +510,8 @@ pub fn build_capdl_spec( let mut frame_ids = Vec::new(); let frame_size_bits = mr.page_size.fixed_size_bits(kernel_config); + // If this MR is supposed to receive untyped metadata, mark the first frame in the spec + let mut receive_all_untypeds = mr.receive_all_untypeds; for frame_sequence in 0..mr.page_count { let paddr = mr .paddr() @@ -518,7 +524,10 @@ pub fn build_capdl_spec( &format!("mr_{}_{:09}", mr.name, frame_sequence), paddr, frame_size_bits as u8, + receive_all_untypeds, )); + // Only mark the first frame in the Memory Region + receive_all_untypeds = false; } mr_name_to_frames.insert(&mr.name, frame_ids); @@ -629,6 +638,7 @@ pub fn build_capdl_spec( &format!("{}_stack_{:09}", pd.name, stack_frame_seq), None, PageSize::Small.fixed_size_bits(kernel_config) as u8, + false, ); let stack_frame_cap = capdl_util_make_frame_cap(stack_frame_obj_id, true, true, false, true); @@ -839,6 +849,7 @@ pub fn build_capdl_spec( &format!("{}_{}", virtual_machine.name, vcpu.id), PD_CAP_BITS, [].to_vec(), + false, ); let vm_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; let vm_cnode_cap = @@ -858,6 +869,7 @@ pub fn build_capdl_spec( None, // Must be consistent with the granule bits used in spec serialisation PageSize::Small.fixed_size_bits(kernel_config) as u8, + false, ); let vm_ipcbuf_frame_cap = capdl_util_make_frame_cap(vm_ipcbuf_frame_obj_id, true, true, false, true); @@ -955,19 +967,88 @@ pub fn build_capdl_spec( } // Step 3-13 Create CSpace and add all caps that the PD code and libmicrokit need to access. - let pd_cnode_obj_id = capdl_util_make_cnode_obj( - &mut spec_container, - &pd.name, - PD_CAP_BITS, - caps_to_insert_to_pd_cspace, - ); - let pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; - let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8); - caps_to_bind_to_tcb.push(capdl_util_make_cte( - TcbBoundSlot::CSpace as u32, - pd_cnode_cap, - )); - pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id); + // If this pd is supposed to receive all remaining untypeds, do what + // https://github.com/Neutrality-ch/microkit/commit/34d4b8d2e246dd77bcd538027277e37a5ba97764 + // proposed: create a new root CNode, and insert the Microkit CNode at index 0, (this means + // old CPtr's will still point to valid capabilities in the Microkit CNode), and create a + // placeholder CNode at index 1 of the new root CNode which will be receiving the untypeds. + // Mark the receiving CNode. + if pd.receive_all_untypeds { + let root_cnode_size_bits = 6; // XXX: for now 64 slots (2^{64}) + let receiving_untyped_cnode_size_bits = 8; // TODO: + // log2(MAX_NUM_BOOTINFO_UNTYPED_CAPS)?, + // some other precalculated value? + // Populate the below with pd_cnode_cap and pd_receiving_untyped_cnode_cap or use + // capdl_util_insert_cap_into_cspace instead? (whats the benefit of the first + // approach?) + //let mut caps_to_insert_to_pd_root_cspace: Vec = Vec::new(); + // TODO: slots: for pd_root_cnode_obj will need to contain the original Microkit CNode + // and the to-be-populated untyped receiving CNode + let pd_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &pd.name, + PD_CAP_BITS, + caps_to_insert_to_pd_cspace, + false, + ); + let mut pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64 - root_cnode_size_bits as u64; + println!("pd cnode guard size: {}", pd_guard_size); + let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8); + + let pd_receiving_untyped_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &(pd.name.clone() + "_receiving_untypeds"), + receiving_untyped_cnode_size_bits, + Vec::new(), + true, + ); + // OLD: pd_guard_size = kernel_config.cap_address_bits - receiving_untyped_cnode_size_bits as u64 - root_cnode_size_bits as u64; + pd_guard_size = kernel_config.cap_address_bits - receiving_untyped_cnode_size_bits as u64 - root_cnode_size_bits as u64; + // XXX: for the cap, do guard size up to the size_bits, so when addressing from the + // receiving_untypeds_cnode_cap, one can use max depth + println!("receivning untyped guard size: {}", pd_guard_size); + let pd_receiving_untyped_cnode_cap = capdl_util_make_cnode_cap(pd_receiving_untyped_cnode_obj_id, 0, pd_guard_size as u8); + let pd_receiving_untyped_cnode_cap_self_ref = capdl_util_make_cnode_cap(pd_receiving_untyped_cnode_obj_id, 0, pd_guard_size as u8); + capdl_util_insert_cap_into_cspace(&mut spec_container, pd_receiving_untyped_cnode_obj_id, 0, pd_receiving_untyped_cnode_cap_self_ref); + + let pd_root_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &(pd.name.clone() + "_root"), + root_cnode_size_bits, + Vec::new(), + false, + ); + pd_guard_size = 0; // so the old Microkit CNode indexes work as expected, but other + // CNode's (such as receiving untyped one) can be addressed at the + // root_cnode_size_bits most significant bits of the address. + println!("root cnode guard size: {}", pd_guard_size); + let pd_root_cnode_cap = capdl_util_make_cnode_cap(pd_root_cnode_obj_id, 0, pd_guard_size as u8); + capdl_util_insert_cap_into_cspace(&mut spec_container, pd_root_cnode_obj_id, 0, pd_cnode_cap); + capdl_util_insert_cap_into_cspace(&mut spec_container, pd_root_cnode_obj_id, 1, pd_receiving_untyped_cnode_cap); + + caps_to_bind_to_tcb.push(capdl_util_make_cte( + TcbBoundSlot::CSpace as u32, + pd_root_cnode_cap, + )); + // XXX: change this to root? or is this fine + pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id); + } else { + let pd_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &pd.name, + PD_CAP_BITS, + caps_to_insert_to_pd_cspace, + pd.receive_all_untypeds, + ); + let pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; + let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8); + caps_to_bind_to_tcb.push(capdl_util_make_cte( + TcbBoundSlot::CSpace as u32, + pd_cnode_cap, + )); + pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id); + } + // Step 3-14 Set the TCB parameters and all the various caps that we need to bind to this TCB. if let Object::Tcb(pd_tcb) = &mut spec_container diff --git a/tool/microkit/src/capdl/util.rs b/tool/microkit/src/capdl/util.rs index a1c20e3ca..8e6017d06 100644 --- a/tool/microkit/src/capdl/util.rs +++ b/tool/microkit/src/capdl/util.rs @@ -29,11 +29,13 @@ pub fn capdl_util_make_frame_obj( name: &str, paddr: Option, size_bits: u8, + receive_all_untypeds: bool, ) -> ObjectId { let frame_inner_obj = Object::Frame(object::Frame { size_bits, paddr, init: frame_init, + receive_all_untypeds, }); let frame_obj = CapDLNamedObject { name: format!("frame_{name}").into(), @@ -219,8 +221,9 @@ pub fn capdl_util_make_cnode_obj( pd_name: &str, size_bits: u8, slots: Vec, + receive_all_untypeds: bool, ) -> ObjectId { - let cnode_inner_obj = Object::CNode(object::CNode { size_bits, slots }); + let cnode_inner_obj = Object::CNode(object::CNode { size_bits, slots, receive_all_untypeds }); let cnode_obj = CapDLNamedObject { name: format!("cnode_{pd_name}").into(), object: cnode_inner_obj, diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 17b5adbae..a0cb8b7e3 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -125,6 +125,10 @@ pub struct SysMemoryRegion { /// due to the user's SDF or created by the tool for setting up the /// stack, ELF, etc. pub kind: SysMemoryRegionKind, + // Set to true means the PD which maps this memory region (only one allowed) + // will receive all untyped memory capabilities and this memory region will + // receive metadata on all of these untyped objects. + pub receive_all_untypeds: bool, } impl SysMemoryRegion { @@ -271,6 +275,9 @@ pub struct ProtectionDomain { pub parent: Option, /// Value of the setvar_id attribute, if a parent protection domain exists pub setvar_id: Option, + /// If true, CapDL initialiser will hand off all remaining untyped + /// capabilities to this PD. (Can only be set by one PD) + pub receive_all_untypeds: bool, /// Location in the parsed SDF file text_pos: Option, } @@ -544,6 +551,7 @@ impl ProtectionDomain { } } + let cpu = CpuCore( sdf_parse_number(node.attribute("cpu").unwrap_or("0"), node)? .try_into() @@ -1083,6 +1091,7 @@ impl ProtectionDomain { has_children, parent: None, setvar_id, + receive_all_untypeds: false, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), }) } @@ -1220,7 +1229,7 @@ impl SysMemoryRegion { xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, ) -> Result { - check_attributes(xml_sdf, node, &["name", "size", "page_size", "phys_addr"])?; + check_attributes(xml_sdf, node, &["name", "size", "page_size", "phys_addr", "receive_all_untypeds"])?; let name = checked_lookup(xml_sdf, node, "name")?; let size = sdf_parse_number(checked_lookup(xml_sdf, node, "size")?, node)?; @@ -1269,6 +1278,21 @@ impl SysMemoryRegion { let page_count = size / page_size; + let receive_all_untypeds = if let Some(xml_receive_all_untypeds) = node.attribute("receive_all_untypeds") { + match str_to_bool(xml_receive_all_untypeds) { + Some(val) => val, + None => { + return Err(value_error( + xml_sdf, + node, + "receive_all_untypeds must be 'true' or 'false'".to_string(), + )) + } + } + } else { + false + }; + Ok(SysMemoryRegion { name: name.to_string(), size, @@ -1278,6 +1302,7 @@ impl SysMemoryRegion { phys_addr, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), kind: SysMemoryRegionKind::User, + receive_all_untypeds: receive_all_untypeds, }) } } @@ -1713,8 +1738,9 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result 1 { return Err(format!( "Error: duplicate protection domain name '{}'.", @@ -1726,8 +1752,30 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result 1 { + return Err( + "Error: only one MR can receive the remaining untypeds".to_string() + ); + } for mr in &mrs { if mrs.iter().filter(|x| mr.name == x.name).count() > 1 { return Err(format!(