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