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 @@ + + + + + + + +