Add support for FPU flag for PDs

docs/manual.md

@@ -723,9 +723,7 @@ This will set the program counter of the vCPU to `entry_point`.
 
 Stop the execution of the VM's virtual CPU with ID `vcpu`.
 
-## `void microkit_vcpu_arm_inject_irq(microkit_child vcpu, seL4_Uint16 irq,
-seL4_Uint8 priority, seL4_Uint8 group,
-seL4_Uint8 index)`
+## `void microkit_vcpu_arm_inject_irq(microkit_child vcpu, seL4_Uint16 irq,seL4_Uint8 priority, seL4_Uint8 group, seL4_Uint8 index)`
 
 Inject a virtual ARM interrupt for a virtual CPU `vcpu` with IRQ number `irq`.
 The `priority` (0-31) determines what ARM GIC (generic interrupt controller)
@@ -1010,6 +1008,7 @@ It supports the following attributes:
   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.
 
 Additionally, it supports the following child elements:
 

tool/microkit/src/capdl/builder.rs

@@ -322,6 +322,7 @@ impl CapDLSpecContainer {
             prio: 0,
             max_prio: 0,
             resume: false,
+            fpu: true,
             ip: entry_point.into(),
             sp: 0.into(),
             gprs: Vec::new(),
@@ -468,7 +469,7 @@ pub fn build_capdl_spec(
     )
     .unwrap();
 
-    // At this point, all of the required objects for the monitor have been created and it caps inserted into
+    // At this point, all of the required objects for the monitor have been created and its caps inserted into
     // the correct slot in the CSpace. We need to bind those objects into the TCB for the monitor to use them.
     // In addition, `add_elf_to_spec()` doesn't fill most the details in the TCB.
     // Now fill them in: stack ptr, priority, ipc buf vaddr, etc.
@@ -939,6 +940,7 @@ pub fn build_capdl_spec(
                             affinity: Word(vcpu.cpu.0.into()),
                             prio: virtual_machine.priority,
                             max_prio: virtual_machine.priority,
+                            fpu: true,
                             resume: false,
                             // VMs do not have program images associated with them so these are always zero.
                             ip: Word(0),
@@ -1007,6 +1009,7 @@ pub fn build_capdl_spec(
             pd_tcb.extra.master_fault_ep = None; // Not used on MCS kernel.
             pd_tcb.extra.prio = pd.priority;
             pd_tcb.extra.max_prio = pd.priority;
+            pd_tcb.extra.fpu = pd.fpu;
             pd_tcb.extra.resume = true;
 
             pd_tcb.slots.extend(caps_to_bind_to_tcb);

tool/microkit/src/sdf.rs

@@ -261,6 +261,8 @@ pub struct ProtectionDomain {
     pub cpu: CpuCore,
     pub program_image: PathBuf,
     pub program_image_for_symbols: Option<PathBuf>,
+    /// Enable FPU for this PD.
+    pub fpu: bool,
     pub maps: Vec<SysMap>,
     pub irqs: Vec<SysIrq>,
     pub ioports: Vec<IOPort>,
@@ -461,6 +463,7 @@ impl ProtectionDomain {
             // but we do the error-checking further down.
             "smc",
             "cpu",
+            "fpu",
         ];
         if is_child {
             attrs.push("id");
@@ -613,6 +616,19 @@ impl ProtectionDomain {
             ));
         }
 
+        // FPU is enabled by default
+        let fpu = if let Some(xml_fpu) = node.attribute("fpu") {
+            match str_to_bool(xml_fpu) {
+                Some(val) => val,
+                None => {
+                    return Err(value_error(xml_sdf, node, "fpu must be 'true' or 'false'".to_string(),))
+                }
+            }
+        } else {
+            // Default to fpu enabled
+            true
+        };
+
         for child in node.children() {
             if !child.is_element() {
                 continue;
@@ -1081,6 +1097,7 @@ impl ProtectionDomain {
             cpu,
             program_image: program_image.unwrap(),
             program_image_for_symbols,
+            fpu,
             maps,
             irqs,
             ioports,

tool/microkit/tests/sdf/wrong_fpu_flag_value.system

@@ -0,0 +1,10 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2025, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="test" fpu="foo">
+    </protection_domain>
+</system>

tool/microkit/tests/test.rs

@@ -917,4 +917,13 @@ mod system {
             "Error: too many protection domains (64) defined. Maximum is 63.",
         )
     }
+
+    #[test]
+    fn test_fpu_flag_wrong_value() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "wrong_fpu_flag_value.system",
+            "Error: fpu must be 'true' or 'false'",
+        )
+    }
 }