diff --git a/Cargo.lock b/Cargo.lock index 67bd2d7ad..eba3fa7b9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -439,7 +439,7 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "sel4" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "cfg-if", "sel4-config", @@ -449,7 +449,7 @@ dependencies = [ [[package]] name = "sel4-alloca" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "cfg-if", ] @@ -457,7 +457,7 @@ dependencies = [ [[package]] name = "sel4-bitfield-ops" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "rustversion", ] @@ -465,12 +465,12 @@ dependencies = [ [[package]] name = "sel4-build-env" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [[package]] name = "sel4-capdl-initializer" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "log", "rkyv", @@ -488,7 +488,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "miniz_oxide", "rkyv", @@ -500,7 +500,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types-derive" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "proc-macro2", "quote", @@ -510,7 +510,7 @@ dependencies = [ [[package]] name = "sel4-config" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "prettyplease", "proc-macro2", @@ -524,7 +524,7 @@ dependencies = [ [[package]] name = "sel4-config-data" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "sel4-build-env", "sel4-config-types", @@ -534,7 +534,7 @@ dependencies = [ [[package]] name = "sel4-config-macros" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "fallible-iterator", "proc-macro2", @@ -547,7 +547,7 @@ dependencies = [ [[package]] name = "sel4-config-types" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "serde", ] @@ -555,12 +555,12 @@ dependencies = [ [[package]] name = "sel4-ctors-dtors" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [[package]] name = "sel4-dlmalloc" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "dlmalloc", "lock_api", @@ -569,17 +569,17 @@ dependencies = [ [[package]] name = "sel4-immediate-sync-once-cell" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [[package]] name = "sel4-immutable-cell" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [[package]] name = "sel4-initialize-tls" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "cfg-if", "sel4-alloca", @@ -588,7 +588,7 @@ dependencies = [ [[package]] name = "sel4-logging" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "lock_api", "log", @@ -597,12 +597,12 @@ dependencies = [ [[package]] name = "sel4-no-allocator" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [[package]] name = "sel4-panicking" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "cfg-if", "sel4-immediate-sync-once-cell", @@ -613,12 +613,12 @@ dependencies = [ [[package]] name = "sel4-panicking-env" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [[package]] name = "sel4-phdrs" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "sel4-phdrs-constants", ] @@ -626,12 +626,12 @@ dependencies = [ [[package]] name = "sel4-phdrs-constants" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [[package]] name = "sel4-phdrs-patched" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "sel4-phdrs", "sel4-rodata-static", @@ -640,12 +640,12 @@ dependencies = [ [[package]] name = "sel4-rodata-static" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [[package]] name = "sel4-root-task" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "sel4", "sel4-dlmalloc", @@ -660,7 +660,7 @@ dependencies = [ [[package]] name = "sel4-root-task-macros" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "proc-macro2", "quote", @@ -670,7 +670,7 @@ dependencies = [ [[package]] name = "sel4-runtime-common" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "cfg-if", "sel4", @@ -686,12 +686,12 @@ dependencies = [ [[package]] name = "sel4-stack" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [[package]] name = "sel4-sync" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "lock_api", "sel4", @@ -701,7 +701,7 @@ dependencies = [ [[package]] name = "sel4-sys" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=dbe6445d56059ed9a757e53c7137892aece1d179#dbe6445d56059ed9a757e53c7137892aece1d179" +source = "git+https://github.com/seL4/rust-sel4?rev=7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb#7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" dependencies = [ "bindgen", "glob", diff --git a/Cargo.toml b/Cargo.toml index 87718a1be..f48722417 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -13,11 +13,11 @@ members = [ [workspace.dependencies.sel4-capdl-initializer] git = "https://github.com/seL4/rust-sel4" -rev = "dbe6445d56059ed9a757e53c7137892aece1d179" +rev = "7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [workspace.dependencies.sel4-capdl-initializer-types] git = "https://github.com/seL4/rust-sel4" -rev = "dbe6445d56059ed9a757e53c7137892aece1d179" +rev = "7a56b4f1ee9084e2b5930b19afa47c080cd0e6cb" [profile.release.package.microkit-tool] strip = true diff --git a/docs/manual.md b/docs/manual.md index e3d21aa1c..d701c11e3 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -638,7 +638,6 @@ If the protection domain has children it must also implement: void microkit_vcpu_arm_ack_vppi(microkit_child vcpu, seL4_Word irq); seL4_Word microkit_vcpu_arm_read_reg(microkit_child vcpu, seL4_Word reg); void microkit_vcpu_arm_write_reg(microkit_child vcpu, seL4_Word reg, seL4_Word value); - void microkit_arm_smc_call(seL4_ARM_SMCContext *args, seL4_ARM_SMCContext *response); void microkit_x86_ioport_write_8(microkit_ioport ioport_id, seL4_Word port_addr, seL4_Word data); void microkit_x86_ioport_write_16(microkit_ioport ioport_id, @@ -866,17 +865,6 @@ Write to a register for a given virtual CPU with ID `vcpu`. The `reg` argument i register that is written to. The `value` argument is what the register will be set to. The list of registers is defined by the enum `seL4_VCPUReg` in the seL4 source code. -## `void microkit_arm_smc_call(seL4_ARM_SMCContext *args, seL4_ARM_SMCContext *response)` - -The API takes in arguments for a Secure Monitor Call which will be performed by seL4. Any -response values will be placed into the `response` structure. - -The `seL4_ARM_SMCContext` structure contains fields for registers x0 to x7. - -Note that this API is only available when the PD making the call has been configured to -have SMC enabled in the SDF. Note that when the kernel makes the actual SMC, it cannot -pre-empt the Secure Monitor and therefore any kernel WCET properties are no longer guaranteed. - ## `void microkit_x86_ioport_write_(8|16|32)(microkit_ioport ioport_id, seL4_Word port_addr, seL4_Word data)` Write an 8, 16, or 32 bits value at port address `port_addr` to I/O Port with ID `ioport_id`. @@ -991,7 +979,6 @@ It supports the following attributes: * `stack_size`: (optional) Number of bytes that will be used for the PD's stack. Must be be between 4KiB and 16MiB and be 4K page-aligned. Defaults to 8KiB. * `cpu`: (optional) set the physical CPU core this PD will run on. Defaults to zero. -* `smc`: (optional, only on ARM) Allow the PD to give an SMC call for the kernel to perform.. Defaults to false. * `fpu`: (optional) whether this PD can access the FPU. Defaults to true. * `domain`: (conditionally required) the name of the domain that this PD belongs to. If a domain schedule is specified, this is mandatory, else it is disallowed. @@ -1126,15 +1113,23 @@ It supports no attributes, but supports the following elements as children: * `cap_sc`: A capability to a protection domain's Scheduling Context (SC). If the protection domain is passive, this is a capability to the notification's scheduling context. * `cap_vspace`: A capability to a protection domain's VSpace. +* `cap_smc`: (only on ARM) A badged capability for performing specific SMC calls. All of the elements support the `slot` attribute, which is is an opaque identifier used to address the capability at runtime. To convert the `slot` to an `seL4_CPtr`, use the [`seL4_CPtr microkit_cspace_root_slot_to_cptr(seL4_Word slot)`](#libmicrokit_cspace_root_slot_to_cptr) function. See the 'cap_sharing' example packaged in your SDK or [on GitHub](https://github.com/seL4/microkit/tree/main/example/cap_sharing). -All capability elements (currently) all support the `pd` attribute, the name of the protection domain that the capability is from. +The 'tcb', 'sc' and 'vspace' elements support `pd` attribute, the name of the protection domain that the capability is from. For instance, `` will place the TCB of PD 'alpha' in the CSpace of the current PD. +The `cap_smc` elements supports the `function_id` attribute. This is an allowlisted function ID permitted +for an invocation on the SMC capability. If you want to support multiple SMC function invocations, create +multiple `cap_smc` for each function ID. For example; to permit calls to the `PSCI_VERSION` (0x84000000) +function, add ``. If you do not care about isolation, +or are experimenting, specifying a `function_id="0"` grants an unbadged SMC capability that allows +any SMC function invocations. + ## `io_address_space` The `io_address_space` element describes an address space used to isolate a given device. diff --git a/example/arm_smc/Makefile b/example/arm_smc/Makefile index 0a535a469..9b8546113 100644 --- a/example/arm_smc/Makefile +++ b/example/arm_smc/Makefile @@ -45,6 +45,7 @@ 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) @@ -55,4 +56,4 @@ $(BUILD_DIR)/arm_smc.elf: $(addprefix $(BUILD_DIR)/, $(ARM_SMC_OBJS)) $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ $(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) arm_smc.system - $(MICROKIT_TOOL) arm_smc.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) + $(MICROKIT_TOOL) arm_smc.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) --capdl-json $(SPEC) diff --git a/example/arm_smc/arm_smc.c b/example/arm_smc/arm_smc.c index ae319e921..65137ad87 100644 --- a/example/arm_smc/arm_smc.c +++ b/example/arm_smc/arm_smc.c @@ -6,23 +6,42 @@ #include #include +#define CAP_SMC (microkit_cspace_root_slot_to_cptr(1)) #define PSCI_VERSION_FID 0x84000000 +#define PSCI_FUNCTION_CPU_ON 0x84000001 void init(void) { - microkit_dbg_puts("Getting SMC version via microkit_arm_smc_call()\n"); + microkit_dbg_puts("Getting SMC version via seL4_ARM_SMC_Call()\n"); - seL4_ARM_SMCContext args = {0}; - seL4_ARM_SMCContext resp = {0}; + seL4_ARM_SMCContext args = { .x0 = PSCI_VERSION_FID, 0 }; + seL4_ARM_SMCContext resp = { 0 }; - args.x0 = PSCI_VERSION_FID; - microkit_arm_smc_call(&args, &resp); + seL4_Error err; + err = seL4_ARM_SMC_Call(CAP_SMC, &args, &resp); + if (err != seL4_NoError) { + // Possible if you invoke with the wrong function IDs, amongst others + microkit_dbg_puts("internal error: failed to make SMC call\n"); + return; + } microkit_dbg_puts("PSCI version: "); microkit_dbg_put32(((uint32_t) resp.x0 >> 16) & 0xFFFF); microkit_dbg_puts("."); microkit_dbg_put32((uint32_t) resp.x0 & 0xFFFF); microkit_dbg_puts("\n"); + + // This is not allowed! + args.x0 = PSCI_FUNCTION_CPU_ON; + + microkit_dbg_puts("Trying to power a CPU ON (which should not work)\n"); + err = seL4_ARM_SMC_Call(CAP_SMC, &args, &resp); + if (err == seL4_NoError) { + microkit_dbg_puts("internal error: this succeeded\n"); + return; + } + + microkit_dbg_puts("Failed successfully to call CPU_ON\n"); } void notified(microkit_channel ch) diff --git a/example/arm_smc/arm_smc.system b/example/arm_smc/arm_smc.system index b448d5043..525dae3ba 100644 --- a/example/arm_smc/arm_smc.system +++ b/example/arm_smc/arm_smc.system @@ -5,7 +5,12 @@ SPDX-License-Identifier: BSD-2-Clause --> - + + + + + + - \ No newline at end of file + diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index b31391aeb..bacad2bd8 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -22,8 +22,7 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define MONITOR_EP 5 /* Only valid in the 'benchmark' configuration */ #define TCB_CAP 6 -/* Only valid when the PD has been configured to make SMC calls */ -#define ARM_SMC_CAP 7 + #define BASE_OUTPUT_NOTIFICATION_CAP 10 #define BASE_ENDPOINT_CAP 74 #define BASE_IRQ_CAP 138 @@ -290,18 +289,6 @@ static inline void microkit_vcpu_arm_write_reg(microkit_child vcpu, seL4_Word re } #endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ -#if defined(CONFIG_ALLOW_SMC_CALLS) -static inline void microkit_arm_smc_call(seL4_ARM_SMCContext *args, seL4_ARM_SMCContext *response) -{ - seL4_Error err; - err = seL4_ARM_SMC_Call(ARM_SMC_CAP, args, response); - if (err != seL4_NoError) { - microkit_dbg_puts("microkit_arm_smc_call: error making SMC call\n"); - microkit_internal_crash(err); - } -} -#endif /* CONFIG_ALLOW_SMC_CALLS */ - #if defined(CONFIG_ARCH_X86_64) static inline void microkit_x86_ioport_write_8(microkit_ioport ioport_id, seL4_Word port_addr, seL4_Word data) { diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 1520022dc..715bb325f 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -8,6 +8,7 @@ use core::ops::Range; use std::{ cmp::{min, Ordering}, collections::{BTreeMap, HashMap}, + num::NonZeroU64, rc::Rc, }; @@ -25,8 +26,8 @@ use crate::{ }, elf::ElfFile, sdf::{ - CapMapType, CpuCore, Map, SystemDescription, BUDGET_DEFAULT, MONITOR_DOMAIN, - MONITOR_PD_NAME, MONITOR_PRIORITY, + CapMapRefData, CapMapRefDataPdKind, CpuCore, Map, SystemDescription, BUDGET_DEFAULT, + MONITOR_DOMAIN, MONITOR_PD_NAME, MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, util::{ranges_overlap, round_down, round_up}, @@ -84,7 +85,6 @@ const PD_REPLY_CAP_IDX: u64 = 4; const PD_MONITOR_EP_CAP_IDX: u64 = 5; // Valid only in benchmark configuration. const PD_TCB_CAP_IDX: u64 = 6; -const PD_ARM_SMC_CAP_IDX: u64 = 7; const PD_BASE_OUTPUT_NOTIFICATION_CAP: u64 = 10; const PD_BASE_OUTPUT_ENDPOINT_CAP: u64 = PD_BASE_OUTPUT_NOTIFICATION_CAP + 64; @@ -604,18 +604,16 @@ pub fn build_capdl_spec( // ********************************* // Step 3. Create the PDs' spec // ********************************* - // On ARM, check if we need to create the SMC object - let arm_smc_obj_id = if kernel_config.arch == Arch::Aarch64 - && kernel_config.arm_smc.unwrap_or(false) - && system.protection_domains.values().any(|pd| pd.smc) - { - Some(spec_container.add_root_object(NamedObject { - name: "arm_smc".to_owned().into(), - object: Object::ArmSmc, - })) - } else { - None - }; + // On ARM (only), get the SMC root cap object ID. + let arm_smc_obj_id = + if kernel_config.arch == Arch::Aarch64 && kernel_config.arm_smc.unwrap_or(false) { + Some(spec_container.add_root_object(NamedObject { + name: "arm_smc".to_owned().into(), + object: Object::ArmSmc, + })) + } else { + None + }; // This object keeps track of object IDs for various 'important' / nameable kernel objects for // each PD so that we can make various references to them at later steps. @@ -1050,14 +1048,6 @@ pub fn build_capdl_spec( } } - // Step 3-12 Create ARM SMC cap if requested. - if pd.smc { - caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( - PD_ARM_SMC_CAP_IDX as u32, - capdl_util_make_arm_smc_cap(arm_smc_obj_id.unwrap()), - )); - } - // 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, @@ -1257,14 +1247,25 @@ pub fn build_capdl_spec( // ********************************* for pd in system.protection_domains.values() { for cap_map in pd.cap_maps.iter() { - // TODO: Once we add more CapMap options, they might not all have - // the pd_name. But for now, they do. - let pd_src_shadow_cspace = &pd_shadow_cspaces[&cap_map.pd]; - - let cap_map_obj = match cap_map.cap_type { - CapMapType::Tcb => capdl_util_make_tcb_cap(pd_src_shadow_cspace.tcb), - CapMapType::Sc => capdl_util_make_sc_cap(pd_src_shadow_cspace.sched_context), - CapMapType::VSpace => capdl_util_make_page_table_cap(pd_src_shadow_cspace.vspace), + let cap_map_obj = match &cap_map.ref_data { + CapMapRefData::Pd { pd, kind, .. } => { + let pd_src_shadow_cspace = &pd_shadow_cspaces[pd]; + match kind { + CapMapRefDataPdKind::Tcb => { + capdl_util_make_tcb_cap(pd_src_shadow_cspace.tcb) + } + CapMapRefDataPdKind::Sc => { + capdl_util_make_sc_cap(pd_src_shadow_cspace.sched_context) + } + CapMapRefDataPdKind::VSpace => { + capdl_util_make_page_table_cap(pd_src_shadow_cspace.vspace) + } + } + } + CapMapRefData::ArmSmcFunction { function_id } => capdl_util_make_arm_smc_cap( + arm_smc_obj_id.unwrap(), + function_id.map(NonZeroU64::get).unwrap_or(0).into(), + ), }; // Map this into the destination pd's cspace and the specified slot. diff --git a/tool/microkit/src/capdl/spec.rs b/tool/microkit/src/capdl/spec.rs index eb1a086dd..a2ef6125a 100644 --- a/tool/microkit/src/capdl/spec.rs +++ b/tool/microkit/src/capdl/spec.rs @@ -98,6 +98,7 @@ pub fn capdl_cap_badge(cap: &Cap) -> Option { match cap { Cap::Endpoint(endpoint) => Some(endpoint.badge), Cap::Notification(notification) => Some(notification.badge), + Cap::ArmSmc(smc) => Some(smc.badge), _ => None, } } diff --git a/tool/microkit/src/capdl/util.rs b/tool/microkit/src/capdl/util.rs index 46f283107..ea11e2076 100644 --- a/tool/microkit/src/capdl/util.rs +++ b/tool/microkit/src/capdl/util.rs @@ -290,8 +290,9 @@ pub fn capdl_util_make_vcpu_cap(vcpu_obj_id: ObjectId) -> Cap { }) } -pub fn capdl_util_make_arm_smc_cap(arm_smc_obj_id: ObjectId) -> Cap { +pub fn capdl_util_make_arm_smc_cap(arm_smc_obj_id: ObjectId, function_id: Word) -> Cap { Cap::ArmSmc(cap::ArmSmc { object: arm_smc_obj_id, + badge: function_id, }) } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index bb5c5b189..b9197b957 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -47,7 +47,7 @@ use util::*; // Internal re-exports pub(crate) use consts::*; -pub(crate) use cspace::CapMapType; +pub(crate) use cspace::{CapMapRefData, CapMapRefDataPdKind}; pub(crate) use iommu::IommuDeviceIdentifier; pub(crate) use irq::{SysIrq, SysIrqKind}; pub(crate) use memory_region::{Map, SysMapPerms}; @@ -310,10 +310,14 @@ pub fn parse( for pd in pds.values() { for cap_map in pd.cap_maps.iter() { - if !pds.contains_key(&cap_map.pd) { + let CapMapRefData::Pd { pd, .. } = &cap_map.ref_data else { + continue; + }; + + if !pds.contains_key(pd) { return Err(format!( "Error: unknown PD name '{}': {}", - cap_map.pd, + pd, loc_string(&xml_sdf, cap_map.text_pos) )); }; @@ -549,12 +553,10 @@ pub fn parse( for (slot, cap_maps) in user_cap_slots.iter() { if cap_maps.len() > 1 { let mut lines = String::new(); - for mapping in cap_maps { + for &mapping in cap_maps { lines.push_str(&format!( - "\n type {:?} from '{}' at '{}'", - mapping.cap_type, - mapping.pd, - loc_string(&xml_sdf, mapping.text_pos) + "\n {}", + mapping.format_for_slot_collision(&xml_sdf) )); } return Err(format!( diff --git a/tool/microkit/src/sdf/cspace.rs b/tool/microkit/src/sdf/cspace.rs index 50f096520..477a78295 100644 --- a/tool/microkit/src/sdf/cspace.rs +++ b/tool/microkit/src/sdf/cspace.rs @@ -4,6 +4,7 @@ // SPDX-License-Identifier: BSD-2-Clause // +use std::num::NonZeroU64; use std::rc::Rc; use super::consts::*; @@ -12,17 +13,48 @@ use super::util::{ }; use super::{SdfLocation, SdfNode, SystemDescriptionFile}; +use crate::{sel4::Arch, Config}; + #[derive(Debug, PartialEq, Eq, Copy, Clone)] pub enum CapMapType { Tcb, Sc, VSpace, + ArmSmc, +} + +#[derive(Debug, PartialEq, Eq)] +pub enum CapMapRefDataPdKind { + Tcb, + Sc, + VSpace, +} + +impl From for CapMapRefDataPdKind { + fn from(value: CapMapType) -> Self { + match value { + CapMapType::Tcb => CapMapRefDataPdKind::Tcb, + CapMapType::Sc => CapMapRefDataPdKind::Sc, + CapMapType::VSpace => CapMapRefDataPdKind::VSpace, + CapMapType::ArmSmc => unreachable!(), + } + } +} + +#[derive(Debug, PartialEq, Eq)] +pub enum CapMapRefData { + Pd { + pd: Rc, + kind: CapMapRefDataPdKind, + }, + ArmSmcFunction { + function_id: Option, + }, } #[derive(Debug, PartialEq, Eq)] pub struct CapMap { - pub cap_type: CapMapType, - pub pd: Rc, + pub ref_data: CapMapRefData, // The destination "slot" in the CSpace: note that this is "opaque" and // can be shifted depending on the location in the CSpace to work as the CPtr, // but here it is given as the index into the CNode. @@ -39,15 +71,38 @@ pub struct CSpace { impl CapMap { fn from_xml( cap_type: CapMapType, + config: &Config, xml_sdf: &SystemDescriptionFile, node: &dyn SdfNode, ) -> Result { - // At the moment the four cap maps we support all have the 'pd' element, - // so we can include it here. When that stops being the case we will - // have to rework this a bit. - check_attributes(xml_sdf, node, &["slot", "pd"])?; + let ref_data = match cap_type { + CapMapType::Tcb | CapMapType::Sc | CapMapType::VSpace => { + check_attributes(xml_sdf, node, &["slot", "pd"])?; + + let pd = Rc::from(checked_lookup(xml_sdf, node, "pd")?); + + CapMapRefData::Pd { + pd, + kind: cap_type.into(), + } + } + CapMapType::ArmSmc => { + check_attributes(xml_sdf, node, &["slot", "function_id"])?; + + if config.arch != Arch::Aarch64 { + return Err(value_error( + xml_sdf, + node, + "cap_smc is only supported on AArch64".to_string(), + )); + } + + let function_id: u64 = sdf_parse_required_attribute(xml_sdf, node, "function_id")?; + let function_id = NonZeroU64::new(function_id); - let pd = Rc::from(checked_lookup(xml_sdf, node, "pd")?); + CapMapRefData::ArmSmcFunction { function_id } + } + }; let slot: u64 = sdf_parse_required_attribute(xml_sdf, node, "slot")?; @@ -69,16 +124,33 @@ impl CapMap { } Ok(CapMap { - cap_type, - pd, + ref_data, slot, text_pos: node.range().start, }) } + + pub(crate) fn format_for_slot_collision(&self, xml_sdf: &SystemDescriptionFile) -> String { + let loc = loc_string(xml_sdf, self.text_pos); + + match &self.ref_data { + CapMapRefData::Pd { pd, kind, .. } => { + format!("pd '{pd}'s {kind:?} at '{loc}'") + } + CapMapRefData::ArmSmcFunction { function_id } => { + format!( + "smc cap for function '{} at '{}'", + function_id.map(NonZeroU64::get).unwrap_or(0), + loc + ) + } + } + } } impl CSpace { pub(super) fn from_xml( + config: &Config, xml_sdf: &SystemDescriptionFile, node: &dyn SdfNode, ) -> Result { @@ -88,9 +160,10 @@ impl CSpace { for child in node.children() { cap_maps.push(match child.tag_name() { - "cap_tcb" => CapMap::from_xml(CapMapType::Tcb, xml_sdf, &*child)?, - "cap_sc" => CapMap::from_xml(CapMapType::Sc, xml_sdf, &*child)?, - "cap_vspace" => CapMap::from_xml(CapMapType::VSpace, xml_sdf, &*child)?, + "cap_tcb" => CapMap::from_xml(CapMapType::Tcb, config, xml_sdf, &*child)?, + "cap_sc" => CapMap::from_xml(CapMapType::Sc, config, xml_sdf, &*child)?, + "cap_vspace" => CapMap::from_xml(CapMapType::VSpace, config, xml_sdf, &*child)?, + "cap_smc" => CapMap::from_xml(CapMapType::ArmSmc, config, xml_sdf, &*child)?, child_name => { let location = loc_string(xml_sdf, child.range().start); if let Some(type_name) = child_name.strip_prefix("cap_") { diff --git a/tool/microkit/src/sdf/pd_vm.rs b/tool/microkit/src/sdf/pd_vm.rs index 91fd1d6f8..a14a0a282 100644 --- a/tool/microkit/src/sdf/pd_vm.rs +++ b/tool/microkit/src/sdf/pd_vm.rs @@ -74,7 +74,6 @@ pub struct ProtectionDomain { pub sched_params: SchedulingParams, pub passive: bool, pub stack_size: u64, - pub smc: bool, pub cpu: CpuCore, pub domain: Option, pub program_image: PathBuf, @@ -186,24 +185,6 @@ impl ProtectionDomain { let stack_size: u64 = sdf_parse_attribute(xml_sdf, node, "stack_size")?.unwrap_or(PD_DEFAULT_STACK_SIZE); - let smc = sdf_parse_attribute(xml_sdf, node, "smc")?.unwrap_or(false); - - if smc { - match config.arm_smc { - Some(smc_allowed) => { - if !smc_allowed { - return Err(value_error(xml_sdf, node, "Using SMC support without ARM SMC forwarding support enabled in the kernel for this platform".to_string())); - } - } - None => { - return Err( - "ARM SMC forwarding support is not available for this architecture" - .to_string(), - ) - } - } - } - let cpu = CpuCore(sdf_parse_attribute(xml_sdf, node, "cpu")?.unwrap_or(0u8)); if cpu.0 >= config.num_cores { @@ -680,7 +661,7 @@ impl ProtectionDomain { )); } - cspace = Some(CSpace::from_xml(xml_sdf, &*child)?); + cspace = Some(CSpace::from_xml(config, xml_sdf, &*child)?); } _ => { let pos = child.range().start; @@ -713,7 +694,6 @@ impl ProtectionDomain { }, passive, stack_size, - smc, cpu, domain, program_image: program_image.unwrap(), diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_smc_function_id_0.system b/tool/microkit/tests/sdf/pd_cap_mappings_smc_function_id_0.system new file mode 100644 index 000000000..cee55c1bc --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_smc_function_id_0.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_cap_mappings_smc_on_x86.system b/tool/microkit/tests/sdf/pd_cap_mappings_smc_on_x86.system new file mode 100644 index 000000000..99ad69ba5 --- /dev/null +++ b/tool/microkit/tests/sdf/pd_cap_mappings_smc_on_x86.system @@ -0,0 +1,15 @@ + + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 8f9a2fbb4..08947b8c6 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -1488,8 +1488,8 @@ mod system { &DEFAULT_AARCH64_KERNEL_CONFIG, "pd_cap_mappings_overlapping.system", r#"Error: overlapping user caps in slot 3 of protection domain 'pd_b': - type VSpace from 'pd_a' at 'pd_cap_mappings_overlapping.system:23:13' - type VSpace from 'pd_a' at 'pd_cap_mappings_overlapping.system:25:13'"#, + pd 'pd_a's VSpace at 'pd_cap_mappings_overlapping.system:23:13' + pd 'pd_a's VSpace at 'pd_cap_mappings_overlapping.system:25:13'"#, ) } @@ -1519,4 +1519,21 @@ mod system { "Error: unknown PD name 'invalid': pd_cap_mappings_invalid_pd_ref.system:12:13", ) } + + #[test] + fn test_cap_mappings_smc_on_x86() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "pd_cap_mappings_smc_on_x86.system", + "Error: cap_smc is only supported on AArch64 on element 'cap_smc': pd_cap_mappings_smc_on_x86.system:12:13", + ); + } + + #[test] + fn test_cap_mappings_smc_function_id_0() { + check_success( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_cap_mappings_smc_function_id_0.system", + ); + } }