aarch64 haskell: validate InvocationLabels

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

spec/haskell/src/SEL4/API/Invocation/AARCH64.hs

@@ -5,15 +5,10 @@
 -- SPDX-License-Identifier: GPL-2.0-only
 --
 
--- This module defines the machine-specific invocations for RISC-V.
+-- This module defines the machine-specific invocations for AARCH64.
 
 {-# LANGUAGE EmptyDataDecls #-}
 
--- FIXME AARCH64: This file was copied *VERBATIM* from the RISCV64 version,
--- with minimal text substitution! Remove this comment after updating and
--- checking against C; update copyright as necessary.
--- Progress: add VCPU invocations
-
 module SEL4.API.Invocation.AARCH64 where
 
 import Prelude hiding (Word)
@@ -25,11 +20,9 @@ import SEL4.Object.Structures
 import Data.Word (Word8, Word16, Word32)
 import SEL4.Machine.RegisterSet.AARCH64 (Register(..), VCPUReg(..))
 
-{- RISC-V-Specific Objects -}
+{- AARCH64-Specific Objects -}
 
 -- This data type enumerates the object invocations that are possible.
--- These are invocations on the page table structures, on pages, and on
--- ASID pool structures.
 
 data Invocation
     = InvokeVSpaceRoot VSpaceRootInvocation
@@ -115,9 +108,6 @@ data VCPUInvocation
 
 {- Interrupt Control -}
 
--- The RISCV platform requires an interrupt control call to record whether
--- the interrupt was edge or level-triggered.
-
 data IRQControlInvocation
     = IssueIRQHandler {
         issueHandlerIRQ :: IRQ,

spec/haskell/src/SEL4/API/InvocationLabels/AARCH64.hs

@@ -16,9 +16,6 @@ data ArchInvocationLabel
         | ARMVSpaceInvalidate_Data
         | ARMVSpaceCleanInvalidate_Data
         | ARMVSpaceUnify_Instruction
-        -- FIXME AARCH64 C is undergoing review, currently having (for tables):
-        -- ARMPageUpperDirectoryMap, ...Unmap
-        -- ARMPageDirectoryMap, ...Unmap
         | ARMPageTableMap
         | ARMPageTableUnmap
         | ARMPageMap
@@ -35,8 +32,7 @@ data ArchInvocationLabel
         | ARMVCPUReadReg
         | ARMVCPUWriteReg
         | ARMVCPUAckVPPI
-        -- FIXME AARCH64: C has ARMIRQIssueIRQHandlerTrigger
-        | ARMIRQIssueIRQHandler
+        | ARMIRQIssueIRQHandlerTrigger
         -- FIXME AARCH64: SMMU invocation labels in C
         -- ARMSIDIssueSIDManager,
         -- | ARMSIDGetFault

spec/haskell/src/SEL4/Object/Interrupt/AARCH64.hs

@@ -33,7 +33,7 @@ decodeIRQControlInvocation :: Word -> [Word] -> PPtr CTE -> [Capability] ->
         KernelF SyscallError ArchInv.IRQControlInvocation
 decodeIRQControlInvocation label args srcSlot extraCaps =
     case (invocationType label, args, extraCaps) of
-        (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandler,
+        (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandlerTrigger,
             irqW:triggerW:index:depth:_, cnode:_) -> do
             checkIRQ irqW
             let irq = toEnum (fromIntegral irqW) :: IRQ
@@ -44,7 +44,7 @@ decodeIRQControlInvocation label args srcSlot extraCaps =
             ensureEmptySlot destSlot
             return $
                 ArchInv.IssueIRQHandler irq destSlot srcSlot (triggerW /= 0)
-        (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandler,_,_) ->
+        (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandlerTrigger,_,_) ->
             throw TruncatedMessage
         _ -> throw IllegalOperation
 

tools/haskell-translator/caseconvs

@@ -2009,6 +2009,13 @@ case \x of (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandler, irqW:triggerW:
     | (ArchInvocationLabel ARMIRQIssueIRQHandler, _, _) => ->2
     | _ => ->3
 
+case \x of (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandlerTrigger, irqW:triggerW:index:depth:_, cnode:_) -> (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandlerTrigger,_,_) -> _ ->  ---> let (label, args, extraCaps) = \x in
+    case (label, args, extraCaps) of
+      (ArchInvocationLabel ARMIRQIssueIRQHandlerTrigger,
+        irqW#triggerW#index#depth#_, cnode#_) => ->1
+    | (ArchInvocationLabel ARMIRQIssueIRQHandlerTrigger, _, _) => ->2
+    | _ => ->3
+
 case \x of (ArchInv.IssueIRQHandler (IRQ irq) destSlot srcSlot trigger) ->  ---> case \x of
   IssueIRQHandler irq destSlot srcSlot trigger => ->1