1% 2% Copyright 2014, General Dynamics C4 Systems 3% 4% This software may be distributed and modified according to the terms of 5% the GNU General Public License version 2. Note that NO WARRANTY is provided. 6% See "LICENSE_GPLv2.txt" for details. 7% 8% @TAG(GD_GPL) 9% 10 11This module defines the kernel's mechanisms for handling failures in kernel code. 12 13> module SEL4.Model.Failures where 14 15\begin{impdetails} 16 17> import SEL4.API.Failures 18> import SEL4.API.Types 19> import SEL4.Object.Structures 20> import SEL4.Model.StateData 21 22> import Control.Monad.Except 23 24\end{impdetails} 25 26\subsection{Data Types} 27 28\subsubsection{Monads} 29 30The "KernelF" monad is a transformation of the "Kernel" monad defined in \autoref{sec:model.statedata}. The "ExceptT" monad transformer is applied to "Kernel" to allow kernel functions to abort with a non-fatal error value. Depending on the type of error, which is indicated here by the type parameter "f", it may be either handled internally by the kernel or propagated to user level. 31 32> type KernelF f = ExceptT f Kernel 33 34Note that fatal errors, which are caused by kernel bugs or invalid states and should \emph{never} actually occur, are modelled by evaluating "undefined". This typically happens via a call to the Haskell function "error", or an implicit evaluation of "undefined" by the Haskell compiler on a pattern or guard match failure. 35 36\subsection{Failure Handling} 37 38\subsubsection{Allowing and Preventing Failure} 39 40The use of the "ExceptT" monad transformer to encapsulate code that can fail requires that transitions in and out of such code be explicitly marked. The following functions may be used to do so. Note that these are simply specialisations of existing functions defined on the "ExceptT" transformer or the "MonadTrans" class. 41 42> withoutFailure :: Kernel a -> KernelF f a 43> withoutFailure = lift 44 45> throw :: f -> KernelF f a 46> throw = throwError 47 48The "catchFailure" function is used to call code that may fail, given a function that can handle any failures. 49 50> catchFailure :: KernelF f a -> (f -> Kernel a) -> Kernel a 51> catchFailure f h = do 52> result <- runExceptT f 53> either h return result 54 55The "rethrowFailure" function converts one type of failure into another. This is used to convert a "LookupFailure" into the appropriate "Fault" or "SyscallError". 56 57> rethrowFailure :: 58> (f1 -> f2) -> KernelF f1 a -> KernelF f2 a 59> rethrowFailure t m = do 60> result <- lift $ runExceptT m 61> either (throw . t) return result 62 63\subsubsection{Lookup Failures} 64 65Lookup failures are handled by converting them to either faults or system call errors, depending on the type of lookup. The following functions perform this conversion. 66 67> capFaultOnFailure :: CPtr -> Bool -> KernelF LookupFailure a -> 68> KernelF Fault a 69> capFaultOnFailure cptr rp = rethrowFailure $ CapFault cptr rp 70 71> lookupErrorOnFailure :: Bool -> KernelF LookupFailure a -> 72> KernelF SyscallError a 73> lookupErrorOnFailure isSource = rethrowFailure $ FailedLookup isSource 74 75\subsubsection{Silent Failures} 76 77Some failures are silent; the kernel simply aborts the operation. 78 79> ignoreFailure :: KernelF f () -> Kernel () 80> ignoreFailure = (`catchFailure` const (return ())) 81 82If the expected result is a capability, silenced failures return null capabilities. 83 84> nullCapOnFailure :: KernelF f Capability -> Kernel Capability 85> nullCapOnFailure = flip catchFailure $ const $ return NullCap 86 87If the expected result is a list, silenced failures return the empty list. 88 89> emptyOnFailure :: KernelF f [a] -> Kernel [a] 90> emptyOnFailure m = m `catchFailure` (const $ return []) 91 92Returns the specified constant when execution fails. 93 94> constOnFailure :: a -> KernelF f a -> Kernel a 95> constOnFailure x m = m `catchFailure` (const $ return x) 96 97When silencing failures using either of the functions above, the type of failure is irrelevant; it only matters that a failure has or has not occurred. The "unifyFailure" function, along with an instance of "Error" for the unit type, allows failures of different types to be handled together. 98 99> unifyFailure :: KernelF f a -> KernelF () a 100> unifyFailure = rethrowFailure $ const () 101 102instance Error () 103 104\subsection{Detecting Failures} 105 106This trivial helper function is used to check that an argument is within an acceptable range. 107 108> rangeCheck :: (Integral a, Integral b) => 109> a -> b -> b -> KernelF SyscallError () 110> rangeCheck value minV maxV = 111> unless (value >= fromIntegral minV && value <= fromIntegral maxV) $ 112> throw $ RangeError (fromIntegral minV) (fromIntegral maxV) 113 114 115