From 0512188b869909df00bb32149e907b73daaabc59 Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Date: Tue, 14 Jul 2015 14:39:09 +1000
Subject: [PATCH] Fix up minor haskell issues.
Need to be careful about operations that are ambiguous in Haskell
but well-defined in the resulting Isabelle import.
---
haskell/src/SEL4/Kernel/VSpace/ARM.lhs | 8 +++-----
haskell/src/SEL4/Object/TCB.lhs | 2 +-
2 files changed, 4 insertions(+), 6 deletions(-)
diff --git a/haskell/src/SEL4/Kernel/VSpace/ARM.lhs b/haskell/src/SEL4/Kernel/VSpace/ARM.lhs
index 07b7b7062..61b8d5221 100644
--- a/haskell/src/SEL4/Kernel/VSpace/ARM.lhs
+++ b/haskell/src/SEL4/Kernel/VSpace/ARM.lhs
@@ -1093,9 +1093,7 @@ Capabilities for page directories --- the top level of the hardware-defined page
> -- Fail if there is nothing mapped here
> Nothing -> return $ InvokePageDirectory PageDirectoryNothing
> Just frameInfo -> do
-> withoutFailure $ stateAssert
-> (validMappingSize (fst frameInfo))
-> "mapping found in PD is of invalid size"
+> withoutFailure $ checkValidMappingSize (fst frameInfo)
> let baseStart = pageBase (VPtr start) (fst frameInfo)
> let baseEnd = pageBase (VPtr end - 1) (fst frameInfo)
> when (baseStart /= baseEnd) $
@@ -1313,8 +1311,8 @@ When we fetch a mapping in which to perform a page flush, we assert that its
size is valid. This check is ignored in Haskell, but the Isabelle model has a
notion of the largest permitted object size, and checks it appropriately.
-> validMappingSize :: VMPageSize -> KernelState -> Bool
-> validMappingSize _ = const True
+> checkValidMappingSize :: VMPageSize -> Kernel ()
+> checkValidMappingSize _ = return ()
\subsection{Invocation Implementations}
diff --git a/haskell/src/SEL4/Object/TCB.lhs b/haskell/src/SEL4/Object/TCB.lhs
index e551f4f0e..43ff275cc 100644
--- a/haskell/src/SEL4/Object/TCB.lhs
+++ b/haskell/src/SEL4/Object/TCB.lhs
@@ -587,7 +587,7 @@ When a new "Wait" operation begins, the caller slot in the waiting thread's TCB
> deleteCallerCap receiver = do
> callerSlot <- getThreadCallerSlot receiver
> callerCap <- getSlotCap callerSlot
-> assert (isReplyCap callerCap || callerCap == NullCap)
+> assert (isReplyCap callerCap || isNullCap callerCap)
> "Caller cap must be a reply cap"
> cteDeleteOne callerSlot
--
GitLab