Add support for ARM SMC calls

Signed-off-by: Ivan Velickovic <[email protected]>

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:
 

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;

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),
     };
 

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<SysMap>,
     pub irqs: Vec<SysIrq>,
@@ -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,

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<usize>,
+    /// 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<bool>,
     /// RISC-V specific, what kind of virtual memory system (e.g Sv39)
     pub riscv_pt_levels: Option<RiscvVirtualMemory>,
 }

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,
 };