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 contains utility functions used in system call implementations. 12 13> module SEL4.Model.Syscall where 14 15\begin{impdetails} 16 17> import SEL4.API.Failures 18> import SEL4.Model.StateData 19> import SEL4.Model.Failures 20> import SEL4.Model.Preemption 21> import Control.Monad.Except 22 23\end{impdetails} 24 25System calls in seL4 have three stages: one which may fault, one which may encounter system call errors, and one which cannot fail but may be interrupted. Generally the first is used to look up capabilities, the second to decode arguments and check for possible failures, and the third to perform the operation itself. If either of the first two stages fails, a failure handler runs instead of the following stages. 26 27The "syscall" function lifts code into the appropriate monads, and handles faults and errors. 28 29> syscall :: KernelF Fault a -> (Fault -> Kernel c) -> 30> (a -> KernelF SyscallError b) -> (SyscallError -> Kernel c) -> 31> (b -> KernelP c) -> KernelP c 32> syscall mFault hFault mError hError mFinalise = do 33> rFault <- withoutPreemption $ runExceptT mFault 34> case rFault of 35> Left f -> withoutPreemption $ hFault f 36> Right a -> do 37> rError <- withoutPreemption $ runExceptT $ mError a 38> case rError of 39> Left e -> withoutPreemption $ hError e 40> Right b -> mFinalise b 41 42 43