arm: verification tweaks for SGI API

- introduce arch interface for IRQControlCap dependencies as well as for
  isMDBParentOf (Arch_isIRQControlDescendant, Arch_isMDBParentOf). This
  mirrors the corresponding interface in the proofs and Haskell and
  avoids #ifdef proliferation in generic code.
- Arch_isIRQControlDescendant is currently only used for SGISignalCaps
- Arch_isMDBParentOf is used for SGISignalCaps and SMCCaps
- fix argument checking in Arch_decodeIRQControlInvocation (+ style
  tweak)
- Arch_sameObjectAs must return false for SGISignalCaps to align with
  finality definition of caps, i.e. SGISignalCaps are always final. This
  has no behaviour change, because finality doesn't matter for behaviour
  for SGISignalCaps, but we require for the proofs that the concept of
  finality aligns with the spec.
- simplify checks for IRQControlCap in sameObjectAs: sameObjectAs can
  never be true for IRQControlCap.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

include/arch/arm/arch/object/objecttype.h

@@ -29,3 +29,52 @@ word_t Arch_getObjectSize(word_t t);
 static inline void Arch_postCapDeletion(cap_t cap)
 {
 }
+
+/**
+ * Return true if the given arch cap can be a descendant of an IRQControlCap.
+ */
+static inline CONST bool_t Arch_isIRQControlDescendant(cap_t cap)
+{
+#if CONFIG_MAX_NUM_NODES == 1
+    return cap_get_capType(cap) == cap_sgi_signal_cap;
+#else
+    return false;
+#endif
+}
+
+/**
+ * isMDBParentOf for architecture caps. For most arch caps, this just returns
+ * true, but if there are badged versions of arch caps, this functions should
+ * perform the necessary checks.
+ *
+ * Called by the generic isMDBParentOf after the revocable bit has been checked
+ * and sameRegionAs has been established. This means we can assume both as true
+ * inside Arch_isMDBParentOf.
+ */
+static inline CONST bool_t Arch_isMDBParentOf(cap_t cap_a, cap_t cap_b, bool_t firstBadged)
+{
+    switch (cap_get_capType(cap_a)) {
+#if CONFIG_MAX_NUM_NODES == 1
+    case cap_sgi_signal_cap:
+        return !firstBadged;
+        break;
+#endif
+
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    case cap_smc_cap: {
+        word_t badge;
+
+        badge = cap_smc_cap_get_capSMCBadge(cap_a);
+        if (badge == 0) {
+            return true;
+        }
+        return (badge == cap_smc_cap_get_capSMCBadge(cap_b)) &&
+               !firstBadged;
+        break;
+    }
+#endif
+
+    default:
+        return true;
+    }
+}

include/arch/arm/arch/object/structures.h

@@ -12,17 +12,20 @@
 
 static inline bool_t CONST Arch_isCapRevocable(cap_t derivedCap, cap_t srcCap)
 {
-#ifdef CONFIG_ALLOW_SMC_CALLS
     switch (cap_get_capType(derivedCap)) {
+
+#if CONFIG_MAX_NUM_NODES == 1
+    case cap_sgi_signal_cap:
+        return cap_get_capType(srcCap) == cap_irq_control_cap;
+#endif
+
+#ifdef CONFIG_ALLOW_SMC_CALLS
     case cap_smc_cap:
         return (cap_smc_cap_get_capSMCBadge(derivedCap) !=
                 cap_smc_cap_get_capSMCBadge(srcCap));
+#endif
 
     default:
         return false;
     }
-#endif
-    return false;
 }
-
-

include/arch/riscv/arch/object/objecttype.h

@@ -30,3 +30,18 @@ static inline void Arch_postCapDeletion(cap_t cap)
 {
 }
 
+/**
+ * Return true if the given arch cap can be a descendant of an IRQControlCap.
+ */
+static inline CONST bool_t Arch_isIRQControlDescendant(cap_t cap)
+{
+    return false;
+}
+
+/**
+ * isMDBParentOf for architecture caps. See Arm version for more detailed docs.
+ */
+static inline CONST bool_t Arch_isMDBParentOf(cap_t cap_a, cap_t cap_b, bool_t firstBadged)
+{
+  return true;
+}

include/arch/x86/arch/object/objecttype.h

@@ -37,3 +37,18 @@ word_t Mode_getObjectSize(word_t t);
 
 void Arch_postCapDeletion(cap_t cap);
 
+/**
+ * Return true if the given arch cap can be a descendant of an IRQControlCap.
+ */
+static inline CONST bool_t Arch_isIRQControlDescendant(cap_t cap)
+{
+    return false;
+}
+
+/**
+ * isMDBParentOf for architecture caps. See Arm version for more detailed docs.
+ */
+static inline CONST bool_t Arch_isMDBParentOf(cap_t cap_a, cap_t cap_b, bool_t firstBadged)
+{
+  return true;
+}

src/arch/arm/32/object/objecttype.c

@@ -370,6 +370,12 @@ bool_t CONST Arch_sameObjectAs(cap_t cap_a, cap_t cap_b)
             return false;
         }
     }
+#if CONFIG_MAX_NUM_NODES == 1
+    if (cap_get_capType(cap_a) == cap_sgi_signal_cap) {
+        return false;
+    }
+#endif
+
     return Arch_sameRegionAs(cap_a, cap_b);
 }
 

src/arch/arm/64/object/objecttype.c

@@ -333,6 +333,12 @@ bool_t CONST Arch_sameObjectAs(cap_t cap_a, cap_t cap_b)
         return false;
     }
 #endif
+#if CONFIG_MAX_NUM_NODES == 1
+    if (cap_get_capType(cap_a) == cap_sgi_signal_cap) {
+        return false;
+    }
+#endif
+
     return Arch_sameRegionAs(cap_a, cap_b);
 }
 

src/arch/arm/object/interrupt.c

@@ -92,7 +92,7 @@ exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,
         return Arch_invokeIRQControl(irq, destSlot, srcSlot, trigger);
 #if CONFIG_MAX_NUM_NODES == 1
     } else if (invLabel == ARMIRQIssueSGISignal) {
-        if (length < 3 || current_extra_caps.excaprefs[0] == NULL) {
+        if (length < 4 || current_extra_caps.excaprefs[0] == NULL) {
             userError("IRQControl: IssueSGISignal: Truncated message.");
             current_syscall_error.type = seL4_TruncatedMessage;
             return EXCEPTION_SYSCALL_ERROR;
@@ -107,7 +107,7 @@ exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,
         if (irq >= NUM_SGIS) {
             current_syscall_error.type = seL4_RangeError;
             current_syscall_error.rangeErrorMin = 0;
-            current_syscall_error.rangeErrorMax = NUM_SGIS -1;
+            current_syscall_error.rangeErrorMax = NUM_SGIS - 1;
             userError("IRQControl: IssueSGISignal: Invalid SGI IRQ 0x%lx.", irq);
             return EXCEPTION_SYSCALL_ERROR;
         }

src/object/cnode.c

@@ -780,6 +780,10 @@ bool_t PURE isMDBParentOf(cte_t *cte_a, cte_t *cte_b)
     if (!sameRegionAs(cte_a->cap, cte_b->cap)) {
         return false;
     }
+    if (!Arch_isMDBParentOf(cte_a->cap, cte_b->cap,
+                            mdb_node_get_mdbFirstBadged(cte_b->cteMDBNode))) {
+        return false;
+    }
     switch (cap_get_capType(cte_a->cap)) {
     case cap_endpoint_cap: {
         word_t badge;
@@ -805,20 +809,6 @@ bool_t PURE isMDBParentOf(cte_t *cte_a, cte_t *cte_b)
         break;
     }
 
-#ifdef CONFIG_ALLOW_SMC_CALLS
-    case cap_smc_cap: {
-        word_t badge;
-
-        badge = cap_smc_cap_get_capSMCBadge(cte_a->cap);
-        if (badge == 0) {
-            return true;
-        }
-        return (badge == cap_smc_cap_get_capSMCBadge(cte_b->cap)) &&
-               !mdb_node_get_mdbFirstBadged(cte_b->cteMDBNode);
-        break;
-    }
-#endif
-
     default:
         return true;
         break;

src/object/objecttype.c

@@ -342,10 +342,8 @@ bool_t CONST sameRegionAs(cap_t cap_a, cap_t cap_b)
 
     case cap_irq_control_cap:
         if (cap_get_capType(cap_b) == cap_irq_control_cap ||
-#if CONFIG_MAX_NUM_NODES == 1
-            cap_get_capType(cap_b) == cap_sgi_signal_cap ||
-#endif
-            cap_get_capType(cap_b) == cap_irq_handler_cap) {
+            cap_get_capType(cap_b) == cap_irq_handler_cap ||
+            Arch_isIRQControlDescendant(cap_b)) {
             return true;
         }
         break;
@@ -388,16 +386,9 @@ bool_t CONST sameObjectAs(cap_t cap_a, cap_t cap_b)
     if (cap_get_capType(cap_a) == cap_untyped_cap) {
         return false;
     }
-    if (cap_get_capType(cap_a) == cap_irq_control_cap &&
-        cap_get_capType(cap_b) == cap_irq_handler_cap) {
-        return false;
-    }
-#if CONFIG_MAX_NUM_NODES == 1
-    if (cap_get_capType(cap_a) == cap_irq_control_cap &&
-        cap_get_capType(cap_b) == cap_sgi_signal_cap) {
+    if (cap_get_capType(cap_a) == cap_irq_control_cap) {
         return false;
     }
-#endif
     if (isArchCap(cap_a) && isArchCap(cap_b)) {
         return Arch_sameObjectAs(cap_a, cap_b);
     }