From 25155caff36521819ddf51885f3c68043aa3343a Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Date: Wed, 15 Jul 2015 14:02:37 +1000
Subject: [PATCH] haskell: Add assertion about IRQ handler cap.
Once again, we know in the abstract invariants that these must be
async endpoint caps or null caps, but this is only knowable in
haskell by asserting it.
---
haskell/src/SEL4/Object/Interrupt.lhs | 3 +++
haskell/src/SEL4/Object/Structures.lhs | 4 ++++
2 files changed, 7 insertions(+)
diff --git a/haskell/src/SEL4/Object/Interrupt.lhs b/haskell/src/SEL4/Object/Interrupt.lhs
index a276ca09b..3a8f4e6c2 100644
--- a/haskell/src/SEL4/Object/Interrupt.lhs
+++ b/haskell/src/SEL4/Object/Interrupt.lhs
@@ -131,6 +131,9 @@ When the last IRQ handler capability for a given IRQ is deleted, the capability
> deletingIRQHandler :: IRQ -> Kernel ()
> deletingIRQHandler irq = do
> slot <- getIRQSlot irq
+> cap <- getSlotCap slot
+> assert (isAsyncEndpointCap cap || isNullCap cap)
+> "Cap in IRQ handler slot should be AsyncEP or Null."
> cteDeleteOne slot
> deletedIRQHandler :: IRQ -> Kernel ()
diff --git a/haskell/src/SEL4/Object/Structures.lhs b/haskell/src/SEL4/Object/Structures.lhs
index 4b543f43a..d467b7e6d 100644
--- a/haskell/src/SEL4/Object/Structures.lhs
+++ b/haskell/src/SEL4/Object/Structures.lhs
@@ -101,6 +101,10 @@ This is the type used to represent a capability.
> isUntypedCap (UntypedCap {}) = True
> isUntypedCap _ = False
+> isAsyncEndpointCap :: Capability -> Bool
+> isAsyncEndpointCap (AsyncEndpointCap {}) = True
+> isAsyncEndpointCap _ = False
+
\subsection{Kernel Objects}
When stored in the physical memory model (described in \autoref{sec:model.pspace}), kernel objects must be encapsulated in "KernelObject", so the stored type is independent of the real type of the object.
--
GitLab