content: {-# LANGUAGE Trustworthy #-}
  {-# LANGUAGE DeriveDataTypeable #-}
  {-# LANGUAGE ExistentialQuantification #-}
  
  {- |
  
  This module exports exception types thrown in response to label
  failures.  In addition, it provides 'withContext', a function that
  annotates any exceptions in the 'AnyLabelError' hierarchy that are
  thrown within a given scope.  These annotations should be used to add
  function names to exceptions, so as to make it easier to pinpoint the
  cause of a label error.
  
  -}
  
  module LIO.Error (
      Annotatable(..), withContext
    , AnyLabelError(..), lerrToException, lerrFromException
    , GenericPrivDesc(..), LabelError(..),  labelError, labelErrorP
    , InsufficientPrivs(..), insufficientPrivs
    , ResultExceedsLabel(..)
    ) where
  
  import safe qualified Control.Exception as IO
  import safe Data.Typeable
  
  import safe LIO.Exception
  import safe LIO.Label
  import LIO.TCB
  
  -- | Class of error messages that can be annotated with context.
  class Annotatable e where
    annotate :: String -> e -> e
  
  -- | Parent of all label-related exceptions.
  data AnyLabelError = forall e. (Exception e, Annotatable e) =>
                       AnyLabelError e deriving Typeable
  
  instance Show AnyLabelError where
    showsPrec d (AnyLabelError e) = showsPrec d e
  
  instance Annotatable AnyLabelError where
    annotate s (AnyLabelError e) = AnyLabelError $ annotate s e
  
  instance Exception AnyLabelError
  
  -- | Executes an action with a context string, which will be added to
  -- any label exception thrown.
  -- 
  -- Note: this function wraps an action with a 'catch', and thus may
  -- incur a small runtime cost (though it is well under 100 ns on
  -- machines we benchmarked).
  withContext :: String -> LIO l a -> LIO l a
  withContext ctx (LIOTCB act) =
    LIOTCB $ \st -> act st `IO.catch` \e ->
    IO.throwIO $ annotate ctx (e :: AnyLabelError)
  
  -- | Definition of 'toException' for children of 'AnyLabelError' in
  -- the exception hierarchy.
  lerrToException :: (Exception e, Annotatable e) => e -> SomeException
  lerrToException = toException . AnyLabelError
  
  -- | Definition of 'fromException' for children of 'AnyLabelError' in
  -- the exception hierarchy.
  lerrFromException :: (Exception e) => SomeException -> Maybe e
  lerrFromException se = do
    AnyLabelError e <- fromException se
    cast e
  
  
  -- | A generic privilege description for recording relevant privileges
  -- in exceptions.
  data GenericPrivDesc l = forall p. (PrivDesc l p) => GenericPrivDesc p
  instance Show (GenericPrivDesc l) where
    showsPrec d (GenericPrivDesc p) = showsPrec d p
  
  
  -- | Main error type thrown by label failures in the 'LIO' monad.
  data LabelError l = LabelError {
      lerrContext :: [String] -- ^ Annotation of where the failure happened.
    , lerrFailure :: String   -- ^ Actual function that failed.
    , lerrCurLabel :: l       -- ^ Current label at time of error.
    , lerrCurClearance :: l   -- ^ Current clearance at time of error.
    , lerrPrivs :: [GenericPrivDesc l] -- ^ Any privileges involved in error.
    , lerrLabels :: [l]       -- ^ Any labels involved in error.
    } deriving (Show, Typeable)
  
  instance Annotatable (LabelError l) where
    annotate a e = e { lerrContext = a : lerrContext e }
  
  instance Label l => Exception (LabelError l) where
    toException = lerrToException
    fromException = lerrFromException
  
  -- | Throw a label-error exception.
  labelError :: (Label l) => String -- ^ Function that failed.
                          -> [l]    -- ^ Labels involved in error.
                          -> LIO l a
  labelError fl ls = do
    st <- getLIOStateTCB
    throwLIO LabelError {
        lerrContext = []
      , lerrFailure = fl
      , lerrCurLabel = lioLabel st
      , lerrCurClearance = lioClearance st
      , lerrPrivs = []
      , lerrLabels = ls
      }
  
  -- | Throw a label-error exception.
  labelErrorP :: (Label l, PrivDesc l p) => String  -- ^ Function that failed.
                                         -> Priv p  -- ^ Privileges involved.
                                         -> [l]     -- ^ Labels involved.
                                         -> LIO l a
  labelErrorP fl p ls = do
    st <- getLIOStateTCB
    throwLIO LabelError {
        lerrContext = []
      , lerrFailure = fl
      , lerrCurLabel = lioLabel st
      , lerrCurClearance = lioClearance st
      , lerrPrivs = [GenericPrivDesc $ privDesc p]
      , lerrLabels = ls
      }
  
  
  -- | Error indicating insufficient privileges (independent of the
  -- current label).  This exception is thrown by 'delegate', and
  -- should also be thrown by gates that receive insufficient privilege
  -- descriptions (see "LIO.Delegate").
  data InsufficientPrivs = forall p. (SpeaksFor p) => InsufficientPrivs {
      inspContext :: [String]
    , inspFailure :: String
    , inspSupplied :: p
    , inspNeeded :: p
    } deriving (Typeable)
  
  instance Show InsufficientPrivs where
    showsPrec _ (InsufficientPrivs c l s n) =
      ("InsufficientPrivs { inspContext = " ++) . shows c .
      (", inspLocation = " ++) . shows l .
      (", inspSupplied = " ++) . shows s .
      (", inspNeeded = " ++) . shows n .
      (" }" ++)
  
  instance Annotatable InsufficientPrivs where
    annotate a e = e { inspContext = a : inspContext e }
  
  instance Exception InsufficientPrivs where
    toException = lerrToException
    fromException = lerrFromException
  
  -- | Raise 'InsufficientPrivs' error.
  insufficientPrivs :: (SpeaksFor p) =>
                       String     -- ^ Function in which error occurs
                       -> p       -- ^ Description of privileges supplied
                       -> p       -- ^ Description of privileges needed
                       -> a
  insufficientPrivs fl supplied needed
    | isPriv supplied = error $ "insufficientPrivs: " ++ show fl ++
                        " supplied actual privileges instead of description"
    | otherwise = IO.throw $ InsufficientPrivs [] fl supplied needed
  
  -- | Error raised when a computation spawned by 'lFork' terminates
  -- with its current label above the label of the result.
  data ResultExceedsLabel l = ResultExceedsLabel {
      relContext :: [String]
    , relLocation :: String
    , relDeclaredLabel :: l
    , relActualLabel :: Maybe l
    } deriving (Show, Typeable)
  
  instance Annotatable (ResultExceedsLabel l) where
    annotate a e = e { relContext = a : relContext e }
  
  instance (Label l) => Exception (ResultExceedsLabel l) where
    toException = lerrToException
    fromException = lerrFromException
  