Haskell: arch-specific faults + split VMFault -> ArchFault + ReservedIRQ

Hypervisor extensions add extra fault types which are entirely
arch-specific. While the concept of a VM fault exists on all platforms,
these faults are also arch-specific.

This change adds an ArchFault datatype and constructor to the generic
Faults and Failures, and moves VMFault into ArchFault for the ARM
platform.

NOTE: fault indices have changed (generic goes before arch) as per
  the changes needed for SELFOUR-413, which is the seL4 C equivalent of
  this commit.

* add arch faults and failures to SEL4.cabal

* introduce and handle IRQReserved

  On ARM this does nothing, but on other platforms reserved IRQs are
  actually used.

* split TCB into ArchTCB (userContext)

* changing ArchFault to make haskell-translator to work

  tags: [VER-623][SELFOUR-413]

spec/haskell/SEL4.cabal

@@ -86,6 +86,8 @@ Library
                             SEL4.API.Types.ARM
                             SEL4.API.InvocationLabels.ARM
                             SEL4.API.Invocation.ARM
+                            SEL4.API.Faults.ARM
+                            SEL4.API.Failures.ARM
                             SEL4.Kernel.VSpace.ARM
                             SEL4.Kernel.Thread.ARM
                             SEL4.Object.ObjectType.ARM

spec/haskell/src/SEL4/API/Failures.lhs

@@ -10,6 +10,12 @@
 
 This module specifies the mechanisms used by the seL4 kernel to handle failures in kernel operations that must be communicated somehow to user-level code.
 
+\begin{impdetails}
+
+> {-# LANGUAGE CPP #-}
+
+\end{impdetails}
+
 > module SEL4.API.Failures where
 
 \begin{impdetails}
@@ -19,6 +25,8 @@ This module specifies the mechanisms used by the seL4 kernel to handle failures
 
 \end{impdetails}
 
+> import SEL4.API.Failures.TARGET
+
 \subsection{Types}
 
 \subsubsection{Faults}
@@ -31,15 +39,13 @@ The procedure for handling faults is defined in \autoref{sec:kernel.faulthandler
 >         = UserException {
 >             userExceptionNumber :: Word,
 >             userExceptionErrorCode :: Word }
->         | VMFault {
->             vmFaultAddress :: VPtr,
->             vmFaultArchData :: [Word] }
 >         | CapFault {
 >             capFaultAddress :: CPtr,
 >             capFaultInReceivePhase :: Bool,
 >             capFaultFailure :: LookupFailure }
 >         | UnknownSyscallException {
 >             unknownSyscallNumber :: Word }
+>         | ArchFault { archFault :: ArchFault }
 >         deriving Show
 
 \subsection{Kernel Init Failure}
@@ -124,7 +130,7 @@ There is a similar function used for the "Fault" type; it is defined in \autoref
 >
 > msgFromSyscallError (FailedLookup s lf) =
 >     (6, (fromIntegral $ fromEnum s):(msgFromLookupFailure lf))
->     
+>
 > msgFromSyscallError TruncatedMessage = (7, [])
 >
 > msgFromSyscallError DeleteFirst = (8, [])

spec/haskell/src/SEL4/API/Failures/ARM.lhs

@@ -0,0 +1,26 @@
+%
+% Copyright 2014, General Dynamics C4 Systems
+%
+% This software may be distributed and modified according to the terms of
+% the GNU General Public License version 2. Note that NO WARRANTY is provided.
+% See "LICENSE_GPLv2.txt" for details.
+%
+% @TAG(GD_GPL)
+%
+
+This module defines the encoding of arch-specific faults.
+
+> module SEL4.API.Failures.ARM where
+
+\begin{impdetails}
+
+> import SEL4.Machine
+
+\end{impdetails}
+
+> data ArchFault
+>     = VMFault {
+>             vmFaultAddress :: VPtr,
+>             vmFaultArchData :: [Word] }
+>     deriving Show
+

spec/haskell/src/SEL4/API/Faults.lhs

@@ -10,6 +10,12 @@
 
 This module specifies the mechanisms used by the seL4 kernel to handle faults and exceptions generated by user-level code.
 
+\begin{impdetails}
+
+> {-# LANGUAGE CPP #-}
+
+\end{impdetails}
+
 > module SEL4.API.Faults where
 
 \begin{impdetails}
@@ -22,6 +28,8 @@ This module specifies the mechanisms used by the seL4 kernel to handle faults an
 
 \end{impdetails}
 
+> import SEL4.API.Faults.TARGET
+
 \subsection{Sending Fault IPC}
 
 When a user-level task causes a fault or exception, represented in this model by the "Fault" type, the kernel performs a call to a user-level handler on the faulting thread's behalf. The following function defines the format and contents of the message that is sent by the kernel.
@@ -32,18 +40,16 @@ When a user-level task causes a fault or exception, represented in this model by
 >     pc <- asUser thread getRestartPC
 >     return (1,
 >         pc:fromCPtr cptr:fromIntegral (fromEnum rp):msgFromLookupFailure lf)
->
-> makeFaultMessage (VMFault vptr archData) thread = do
->     pc <- asUser thread getRestartPC
->     return (2, pc:fromVPtr vptr:archData)
->
+
 > makeFaultMessage (UnknownSyscallException n) thread = do
 >     msg <- asUser thread $ mapM getRegister syscallMessage
->     return (3, msg ++ [n])
+>     return (2, msg ++ [n])
 >
 > makeFaultMessage (UserException exception code) thread = do
 >     msg <- asUser thread $ mapM getRegister exceptionMessage
->     return (4, msg ++ [exception, code])
+>     return (3, msg ++ [exception, code])
+>
+> makeFaultMessage (ArchFault af) thread = makeArchFaultMessage af thread
 
 \subsection{Receiving Fault IPC Replies}
 
@@ -57,8 +63,6 @@ This function returns "True" if the faulting thread should be restarted after th
 > 
 > handleFaultReply (CapFault {}) _ _ _ = return True
 > 
-> handleFaultReply (VMFault {}) _ _ _ = return True
-> 
 > handleFaultReply (UnknownSyscallException _) thread label msg = do
 >     asUser thread $ zipWithM_
 >         (\r v -> setRegister r $ sanitiseRegister r v)
@@ -71,3 +75,6 @@ This function returns "True" if the faulting thread should be restarted after th
 >         exceptionMessage msg
 >     return (label == 0)
 
+> handleFaultReply (ArchFault af) thread label msg =
+>     handleArchFaultReply af thread label msg
+

spec/haskell/src/SEL4/API/Faults/ARM.lhs

@@ -0,0 +1,33 @@
+%
+% Copyright 2016, Data61, CSIRO
+%
+% This software may be distributed and modified according to the terms of
+% the GNU General Public License version 2. Note that NO WARRANTY is provided.
+% See "LICENSE_GPLv2.txt" for details.
+%
+% @TAG(DATA61_GPL)
+%
+
+This module defines the encoding of arch-specific faults.
+
+> module SEL4.API.Faults.ARM where
+
+\begin{impdetails}
+
+> import SEL4.Machine
+> import SEL4.Model
+> import SEL4.Object.Structures
+> import SEL4.Object.TCB(asUser)
+
+\end{impdetails}
+
+> import SEL4.API.Failures.ARM
+
+> makeArchFaultMessage :: ArchFault -> PPtr TCB -> Kernel (Word, [Word])
+> makeArchFaultMessage (VMFault vptr archData) thread = do
+>     pc <- asUser thread getRestartPC
+>     return (4, pc:fromVPtr vptr:archData)
+
+> handleArchFaultReply :: ArchFault -> PPtr TCB -> Word -> [Word] -> Kernel Bool
+> handleArchFaultReply (VMFault {}) _ _ _ = return True
+

spec/haskell/src/SEL4/Kernel/VSpace/ARM.lhs

@@ -16,6 +16,7 @@ This module defines the handling of the ARM hardware-defined page tables.
 
 > import SEL4.API.Types
 > import SEL4.API.Failures
+> import SEL4.API.Failures.ARM
 > import SEL4.Machine.RegisterSet
 > import SEL4.Machine.Hardware.ARM
 > import SEL4.Model
@@ -627,12 +628,12 @@ If the kernel receives a VM fault from the CPU, it must determine the address an
 > handleVMFault _ ARMDataAbort = do
 >     addr <- withoutFailure $ doMachineOp getFAR
 >     fault <- withoutFailure $ doMachineOp getDFSR
->     throw $ VMFault addr [0, fault .&. mask 14]
+>     throw $ ArchFault $ VMFault addr [0, fault .&. mask 14]
 >
 > handleVMFault thread ARMPrefetchAbort = do
 >     pc <- withoutFailure $ asUser thread $ getRestartPC
 >     fault <- withoutFailure $ doMachineOp getIFSR
->     throw $ VMFault (VPtr pc) [1, fault .&. mask 14]
+>     throw $ ArchFault $ VMFault (VPtr pc) [1, fault .&. mask 14]
 
 \subsection{Unmapping and Deletion}
 

spec/haskell/src/SEL4/Object/Instances.lhs

@@ -142,7 +142,7 @@ By default, new threads are unable to change the security domains of other threa
 >         tcbFaultHandler = CPtr 0,
 >         tcbIPCBuffer = VPtr 0,
 >         tcbBoundNotification = Nothing,
->         tcbContext = newContext }
+>         tcbArch = newArchTCB }
 >     injectKO   = KOTCB
 >     projectKO o = case o of
 >         KOTCB tcb -> return tcb

spec/haskell/src/SEL4/Object/Interrupt.lhs

@@ -154,6 +154,7 @@ This function is called during bootstrap to set up the initial state of the inte
 >         setInterruptState $ InterruptState (ptrFromPAddr frame) irqTable
 >         timerIRQ <- doMachineOp configureTimer
 >         setIRQState IRQTimer timerIRQ
+>         Arch.initInterruptController
 >         slot <- locateSlotCap rootCNCap biCapIRQC
 >         insertInitCap slot IRQControlCap
 >     return IRQControlCap
@@ -188,6 +189,7 @@ is set to an incorrect value.
 >           IRQTimer -> do
 >               timerTick
 >               doMachineOp resetTimer
+>           IRQReserved -> Arch.handleReservedIRQ irq
 >           IRQInactive -> fail $ "Received disabled IRQ " ++ show irq
 >       doMachineOp $ ackInterrupt irq
 

spec/haskell/src/SEL4/Object/Interrupt/ARM.lhs

@@ -33,3 +33,9 @@ Apparently ARM does not have any.
 > checkIRQ :: Word -> KernelF SyscallError ()
 > checkIRQ irq = rangeCheck irq (fromEnum minIRQ) (fromEnum maxIRQ)
 
+> handleReservedIRQ :: IRQ -> Kernel ()
+> handleReservedIRQ _irq = return () -- handleReservedIRQ does nothing on ARM
+
+> initInterruptController :: Kernel ()
+> initInterruptController = return ()
+

spec/haskell/src/SEL4/Object/Structures.lhs

@@ -267,9 +267,9 @@ The TCB is used to store various data about the thread's current state:
 
 >         tcbBoundNotification :: Maybe (PPtr Notification),
 
-\item and the saved user-level context of the thread.
+\item and any arch-specific TCB contents
 
->         tcbContext :: UserContext }
+>         tcbArch :: ArchTCB }
 >     deriving Show
 
 \end{itemize}
@@ -411,6 +411,7 @@ The interrupt controller state consists of an array with one entry for each of t
 >     = IRQInactive
 >     | IRQSignal
 >     | IRQTimer
+>     | IRQReserved
 >     deriving (Show, Eq)
 
 Each entry in the domain schedule specifies a domain and a length (a number of time slices).

spec/haskell/src/SEL4/Object/Structures/ARM.lhs

@@ -69,6 +69,19 @@ The ARM kernel stores one ARM-specific type of object in the PSpace: ASID pools,
 >                 KOPTE _ -> 2 
 >                 KOPDE _ -> 2
 
+\subsection{Threads}
+
+TCBs contain state that is arch-specific. ``ArchTCB'' represents a wrapper for
+this state. The thread's saved user-level context, which is expected to be
+present on all platforms is stored here.
+
+> data ArchTCB = ArchThread {
+>         atcbContext :: UserContext }
+>     deriving Show
+
+> newArchTCB = ArchThread {
+>     atcbContext = newContext }
+
 \subsection{ASID Pools}
 
 An ASID pool is an array of pointers to page directories. This is used to implement virtual ASIDs on ARM; it is not accessed by the hardware.

spec/haskell/src/SEL4/Object/TCB.lhs

@@ -726,6 +726,16 @@ TCB, using a pointer to the TCB.
 >         tcb <- getObject tptr
 >         setObject tptr $ f tcb
 
+For convenience, we create analogous functions for a TCBs arch component.
+
+> archThreadGet :: (ArchTCB -> a) -> PPtr TCB -> Kernel a
+> archThreadGet f tptr = liftM (f . tcbArch) $ getObject tptr
+
+> archThreadSet :: (ArchTCB -> ArchTCB) -> PPtr TCB -> Kernel ()
+> archThreadSet f tptr = do
+>         tcb <- getObject tptr
+>         setObject tptr $ tcb { tcbArch = f (tcbArch tcb) }
+
 \subsection{User-level Context}
 
 Actions performed by user-level code, or by the kernel when modifying
@@ -736,15 +746,14 @@ The following function performs an operation in the user-level context of a spec
 thread. The operation is represented by a function in the
 "State" monad operating on the thread's "UserContext" structure.
 
-A typical use of this function is "asUser tcbPtr $ setRegister R0 1",
+A typical use of this function is "asUser tcbPtr \$ setRegister R0 1",
 which stores the value "1" in the register "R0" of to the thread
 identified by "tcbPtr".
 
 > asUser :: PPtr TCB -> UserMonad a -> Kernel a
 > asUser tptr f = do
->         uc <- threadGet tcbContext tptr
->         let (a, uc') = runState f uc
->         threadSet (\tcb -> tcb { tcbContext = uc' }) tptr
+>         atcb <- threadGet tcbArch tptr
+>         let (a, uc') = runState f $ atcbContext atcb
+>         threadSet (\tcb -> tcb { tcbArch = atcb { atcbContext = uc' } }) tptr
 >         return a
 
-