aspec: arch split on invokeIRQHandler

The RISCV implementation of invokeIRQHandler calls plic_complete_claim
instead of maskInterrupt. plicCompleteClaim is added as a machine op
and invokeIRQHandler has been arch split for the ACKIrq case.

Signed-off-by: Victor Phan <Victor.Phan@data61.csiro.au>

spec/abstract/ARM/ArchInterrupt_A.thy

@@ -18,5 +18,10 @@ begin
 definition handle_reserved_irq :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad"
   where "handle_reserved_irq irq = return ()"
 
+fun arch_invoke_irq_handler :: "irq_handler_invocation \<Rightarrow> (unit,'z::state_ext) s_monad"
+  where
+  "arch_invoke_irq_handler (ACKIrq irq) = (do_machine_op $ maskInterrupt False irq)"
+| "arch_invoke_irq_handler _ = return ()"
+
 
 end

spec/abstract/ARM_HYP/ArchInterrupt_A.thy

@@ -87,6 +87,11 @@ where
      else if irq_vppi_event_index irq \<noteq> None then vppi_event irq
      else return ()"
 
+fun arch_invoke_irq_handler :: "irq_handler_invocation \<Rightarrow> (unit,'z::state_ext) s_monad"
+  where
+  "arch_invoke_irq_handler (ACKIrq irq) = (do_machine_op $ maskInterrupt False irq)"
+| "arch_invoke_irq_handler _ = return ()"
+
 end
 
 

spec/abstract/Interrupt_A.thy

@@ -42,7 +42,7 @@ slot. The IRQHandler operations load or clear those capabilities.\<close>
 fun
   invoke_irq_handler :: "irq_handler_invocation \<Rightarrow> (unit,'z::state_ext) s_monad"
 where
-  "invoke_irq_handler (ACKIrq irq) = (do_machine_op $ maskInterrupt False irq)"
+  "invoke_irq_handler (ACKIrq irq) = arch_invoke_irq_handler (ACKIrq irq)"
 | "invoke_irq_handler (SetIRQHandler irq cap slot) = (do
      irq_slot \<leftarrow> get_irq_slot irq;
      cap_delete_one irq_slot;

spec/abstract/RISCV64/ArchInterrupt_A.thy

@@ -10,8 +10,17 @@ theory ArchInterrupt_A
 imports "../Ipc_A"
 begin
 
+context begin interpretation Arch .
+
 definition handle_reserved_irq :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad"
   where
   "handle_reserved_irq irq = return ()"
 
-end
+fun arch_invoke_irq_handler :: "irq_handler_invocation \<Rightarrow> (unit,'z::state_ext) s_monad"
+  where
+  "arch_invoke_irq_handler (ACKIrq irq) = (do_machine_op $ plic_complete_claim irq)"
+| "arch_invoke_irq_handler _ = return ()"
+
+end
+
+end

spec/abstract/X64/ArchInterrupt_A.thy

@@ -18,5 +18,10 @@ begin
 definition handle_reserved_irq :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad"
   where "handle_reserved_irq irq = return ()"
 
+fun arch_invoke_irq_handler :: "irq_handler_invocation \<Rightarrow> (unit,'z::state_ext) s_monad"
+  where
+  "arch_invoke_irq_handler (ACKIrq irq) = (do_machine_op $ maskInterrupt False irq)"
+| "arch_invoke_irq_handler _ = return ()"
+
 
 end

spec/machine/RISCV64/MachineOps.thy

@@ -112,6 +112,13 @@ definition
 where
   "setIRQTrigger irq trigger \<equiv> machine_op_lift (setIRQTrigger_impl irq trigger)"
 
+consts'
+  plic_complete_claim_impl :: "irq \<Rightarrow> unit machine_rest_monad"
+
+definition
+  plic_complete_claim :: "irq \<Rightarrow> unit machine_monad"
+where
+  "plic_complete_claim irq \<equiv> machine_op_lift (plic_complete_claim_impl irq)"
 
 text \<open>Interrupts that cannot occur while the kernel is running (e.g. at preemption points), but
 that can occur from user mode. Empty on RISCV64.\<close>