diff --git a/docs/manual.md b/docs/manual.md index 86cf4aa2..65c1ec14 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -438,6 +438,7 @@ 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 init(void)` @@ -605,6 +606,16 @@ 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)` + +This API is available only on ARM and only when seL4 has been configured to enable the +`KernelAllowSMCCalls` option. + +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. + # System Description File {#sysdesc} This section describes the format of the System Description File (SDF). @@ -634,6 +645,7 @@ It supports the following attributes: * `passive`: (optional) Indicates that the protection domain will be passive and thus have its scheduling context removed after initialisation; defaults to false. * `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 4KiB. +* `smc`: (optional, only on ARM) Allow the PD to give an SMC call for the kernel to perform. Only available when the kernel has been configured with `KernelAllowSMCCalls`. Defaults to false. Additionally, it supports the following child elements: diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index a6c55559..39cff2f1 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -18,6 +18,8 @@ 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 @@ -206,6 +208,18 @@ static inline void microkit_vcpu_arm_write_reg(microkit_child vcpu, seL4_Word re } #endif +#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 + static inline void microkit_deferred_notify(microkit_channel ch) { microkit_have_signal = seL4_True; diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index cf86c382..6db07cb4 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -47,6 +47,7 @@ const VSPACE_CAP_IDX: u64 = 3; const REPLY_CAP_IDX: u64 = 4; const MONITOR_EP_CAP_IDX: u64 = 5; const TCB_CAP_IDX: u64 = 6; +const SMC_CAP_IDX: u64 = 7; const BASE_OUTPUT_NOTIFICATION_CAP: u64 = 10; const BASE_OUTPUT_ENDPOINT_CAP: u64 = BASE_OUTPUT_NOTIFICATION_CAP + 64; @@ -70,6 +71,7 @@ const INIT_CNODE_CAP_ADDRESS: u64 = 2; const INIT_VSPACE_CAP_ADDRESS: u64 = 3; const IRQ_CONTROL_CAP_ADDRESS: u64 = 4; // Singleton const INIT_ASID_POOL_CAP_ADDRESS: u64 = 6; +const SMC_CAP_ADDRESS: u64 = 15; // const ASID_CONTROL_CAP_ADDRESS: u64 = 5; // Singleton // const IO_PORT_CONTROL_CAP_ADDRESS: u64 = 7; // Null on this platform @@ -892,6 +894,7 @@ fn build_system( cap_address_names.insert(INIT_VSPACE_CAP_ADDRESS, "VSpace: init".to_string()); cap_address_names.insert(INIT_ASID_POOL_CAP_ADDRESS, "ASID Pool: init".to_string()); cap_address_names.insert(IRQ_CONTROL_CAP_ADDRESS, "IRQ Control".to_string()); + cap_address_names.insert(SMC_CAP_IDX, "SMC".to_string()); let system_cnode_bits = system_cnode_size.ilog2() as u64; @@ -2448,6 +2451,26 @@ fn build_system( } } + for (pd_idx, pd) in system.protection_domains.iter().enumerate() { + if pd.smc { + assert!(config.arm_smc.is_some() && config.arm_smc.unwrap()); + let cnode_obj = &cnode_objs[pd_idx]; + system_invocations.push(Invocation::new( + config, + InvocationArgs::CnodeMint { + cnode: cnode_obj.cap_addr, + dest_index: SMC_CAP_IDX, + dest_depth: PD_CAP_BITS, + src_root: root_cnode_cap, + src_obj: SMC_CAP_ADDRESS, + src_depth: config.cap_address_bits, + rights: Rights::All as u64, // FIXME: Check rights + badge: 0, + }, + )); + } + } + // All minting is complete at this point // Associate badges @@ -3297,6 +3320,11 @@ fn main() -> Result<(), String> { Arch::Riscv64 => None, }; + let arm_smc = match arch { + Arch::Aarch64 => Some(json_str_as_bool(&kernel_config_json, "ALLOW_SMC_CALLS")?), + _ => None, + }; + let kernel_frame_size = match arch { Arch::Aarch64 => 1 << 12, Arch::Riscv64 => 1 << 21, @@ -3315,6 +3343,7 @@ fn main() -> Result<(), String> { benchmark: args.config == "benchmark", fpu: json_str_as_bool(&kernel_config_json, "HAVE_FPU")?, arm_pa_size_bits, + arm_smc, riscv_pt_levels: Some(RiscvVirtualMemory::Sv39), }; diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 44cf1977..d8851cd8 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -144,6 +144,7 @@ pub struct ProtectionDomain { pub pp: bool, pub passive: bool, pub stack_size: u64, + pub smc: bool, pub program_image: PathBuf, pub maps: Vec, pub irqs: Vec, @@ -285,6 +286,9 @@ impl ProtectionDomain { "period", "passive", "stack_size", + // The SMC field is only available in certain configurations + // but we do the error-checking further down. + "smc", ]; if is_child { attrs.push("id"); @@ -360,6 +364,37 @@ impl ProtectionDomain { PD_DEFAULT_STACK_SIZE }; + let smc = if let Some(xml_smc) = node.attribute("smc") { + match str_to_bool(xml_smc) { + Some(val) => val, + None => { + return Err(value_error( + xml_sdf, + node, + "smc must be 'true' or 'false'".to_string(), + )) + } + } + } else { + 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 for this platform".to_string())); + } + } + None => { + return Err( + "ARM SMC forwarding support is not available for this architecture" + .to_string(), + ) + } + } + } + #[allow(clippy::manual_range_contains)] if stack_size < PD_MIN_STACK_SIZE || stack_size > PD_MAX_STACK_SIZE { return Err(value_error( @@ -559,6 +594,7 @@ impl ProtectionDomain { pp, passive, stack_size, + smc, program_image: program_image.unwrap(), maps, irqs, diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index 0e946a66..77ec7e6f 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -50,6 +50,10 @@ pub struct Config { pub fpu: bool, /// ARM-specific, number of physical address bits pub arm_pa_size_bits: Option, + /// ARM-specific, where or not SMC forwarding is allowed + /// False if the kernel config option has not been enabled. + /// None on any non-ARM architecture. + pub arm_smc: Option, /// RISC-V specific, what kind of virtual memory system (e.g Sv39) pub riscv_pt_levels: Option, } diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 29fed79f..8f3c0fcc 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -19,6 +19,7 @@ const DEFAULT_KERNEL_CONFIG: sel4::Config = sel4::Config { benchmark: false, fpu: true, arm_pa_size_bits: Some(40), + arm_smc: None, riscv_pt_levels: None, };