Add ability to configure IRQ triggers

The Microkit tool and system description currently assume that
all interrupts are level triggered which is invalid.

This patch adds the ability for users to specify the trigger,
for example:
```
<irq irq="225" id="1" trigger="edge" />
```

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

docs/manual.md

@@ -479,6 +479,7 @@ The `irq` element has the following attributes:
 
 * `irq`: The hardware interrupt number.
 * `id`: The channel identifier. Must be at least 0 and less than 63.
+* `trigger`: (optional) Whether the IRQ is edge triggered ("edge") or level triggered ("level"). Defualts to "level".
 
 The `setvar` element has the following attributes:
 

tool/microkit/__main__.py

@@ -64,7 +64,7 @@
     Sel4CnodeMint,
     Sel4CnodeCopy,
     Sel4UntypedRetype,
-    Sel4IrqControlGet,
+    Sel4IrqControlGetTrigger,
     Sel4IrqHandlerSetNotification,
     Sel4SchedControlConfigureFlags,
     emulate_kernel_boot,
@@ -1173,9 +1173,10 @@ def build_system(
         for sysirq in pd.irqs:
             cap_address = system_cap_address_mask | cap_slot
             system_invocations.append(
-                Sel4IrqControlGet(
+                Sel4IrqControlGetTrigger(
                     IRQ_CONTROL_CAP_ADDRESS,
                     sysirq.irq,
+                    sysirq.trigger.value,
                     root_cnode_cap,
                     cap_address,
                     kernel_config.cap_address_bits

tool/microkit/sel4.py

@@ -158,6 +158,11 @@ def calculate_rootserver_size(initial_task_region: MemoryRegion) -> int:
     return size
 
 
+class Sel4ArmIrqTrigger(IntEnum):
+    Level = 0
+    Edge = 1
+
+
 class Sel4Aarch64Regs:
     """
 typedef struct seL4_UserContext_ {
@@ -528,13 +533,14 @@ class Sel4AsidPoolAssign(Sel4Invocation):
 
 
 @dataclass
-class Sel4IrqControlGet(Sel4Invocation):
+class Sel4IrqControlGetTrigger(Sel4Invocation):
     _object_type = "IRQ Control"
     _method_name = "Get"
     _extra_caps = ("dest_root", )
-    label = Sel4Label.IRQIssueIRQHandler
+    label = Sel4Label.ARMIRQIssueIRQHandlerTrigger
     irq_control: int
     irq: int
+    trigger: int
     dest_root: int
     dest_index: int
     dest_depth: int

tool/microkit/sysxml.py

@@ -4,6 +4,7 @@
 # SPDX-License-Identifier: BSD-2-Clause
 #
 from microkit.util import str_to_bool, UserError
+from microkit.sel4 import Sel4ArmIrqTrigger
 from typing import Dict, Iterable, Optional, Set, Tuple
 from dataclasses import dataclass
 from pathlib import Path
@@ -69,6 +70,7 @@ class SysMap:
 class SysIrq:
     irq: int
     id_: int
+    trigger: Sel4ArmIrqTrigger
 
 
 @dataclass(frozen=True, eq=True)
@@ -265,14 +267,22 @@ def xml2pd(pd_xml: ET.Element) -> ProtectionDomain:
                 if setvar_vaddr:
                     setvars.append(SysSetVar(setvar_vaddr, vaddr=vaddr))
             elif child.tag == "irq":
-                _check_attrs(child, ("irq", "id"))
+                _check_attrs(child, ("irq", "id", "trigger"))
                 irq = int(checked_lookup(child, "irq"), base=0)
                 id_ = int(checked_lookup(child, "id"), base=0)
                 if id_ >= 63:
                     raise ValueError("id must be < 63")
                 if id_ < 0:
                     raise ValueError("id must be >= 0")
-                irqs.append(SysIrq(irq, id_))
+
+                trigger_str = child.attrib.get("trigger", "level")
+                if trigger_str == "level":
+                    trigger = Sel4ArmIrqTrigger.Level
+                elif trigger_str == "edge":
+                    trigger = Sel4ArmIrqTrigger.Edge
+                else:
+                    raise ValueError(f"trigger must be either 'level' or 'edge'")
+                irqs.append(SysIrq(irq, id_, trigger))
             elif child.tag == "setvar":
                 _check_attrs(child, ("symbol", "region_paddr"))
                 symbol = checked_lookup(child, "symbol")

tool/test/__init__.py

@@ -101,6 +101,9 @@ def test_irq_less_than_0(self):
     def test_write_only_mr(self):
         self._check_error("pd_write_only_mr.xml", f"Error: perms must not be 'w', write-only mappings are not allowed on element 'map':")
 
+    def test_irq_invalid_trigger(self):
+        self._check_error("irq_invalid_trigger.xml", "Error: trigger must be either 'level' or 'edge' on element 'irq'")
+
 
 class ChannelParseTests(ExtendedTestCase):
     def test_missing_pd(self):

tool/test/irq_invalid_trigger.xml

@@ -0,0 +1,12 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2023, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="test1">
+        <program_image path="test" />
+        <irq irq="1" id="1" trigger="an_invalid_trigger" />
+    </protection_domain>
+</system>