From 0f16c5ebdb32b7ae50293768376b6d2714356a69 Mon Sep 17 00:00:00 2001
From: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Date: Wed, 22 Feb 2023 15:30:31 +1100
Subject: [PATCH] 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 <i.velickovic@unsw.edu.au>
---
 docs/manual.md                    |  1 +
 tool/microkit/__main__.py         |  5 +++--
 tool/microkit/sel4.py             | 10 ++++++++--
 tool/microkit/sysxml.py           | 14 ++++++++++++--
 tool/test/__init__.py             |  3 +++
 tool/test/irq_invalid_trigger.xml | 12 ++++++++++++
 6 files changed, 39 insertions(+), 6 deletions(-)
 create mode 100644 tool/test/irq_invalid_trigger.xml

diff --git a/docs/manual.md b/docs/manual.md
index 85325039e..76541ffdb 100644
--- a/docs/manual.md
+++ b/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:
 
diff --git a/tool/microkit/__main__.py b/tool/microkit/__main__.py
index b6bee8d63..a88c54b2f 100644
--- a/tool/microkit/__main__.py
+++ b/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
diff --git a/tool/microkit/sel4.py b/tool/microkit/sel4.py
index 87c16a7f8..777c6c104 100644
--- a/tool/microkit/sel4.py
+++ b/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
diff --git a/tool/microkit/sysxml.py b/tool/microkit/sysxml.py
index 9dc44476e..162173566 100644
--- a/tool/microkit/sysxml.py
+++ b/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")
diff --git a/tool/test/__init__.py b/tool/test/__init__.py
index 2a987ab36..a03a93ce9 100644
--- a/tool/test/__init__.py
+++ b/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):
diff --git a/tool/test/irq_invalid_trigger.xml b/tool/test/irq_invalid_trigger.xml
new file mode 100644
index 000000000..3b8b1cb4d
--- /dev/null
+++ b/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>