LObj.hs

{-# LANGUAGE Unsafe #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE CPP #-}

-- | This module provides routines for safely exposing IO functions in
-- the 'LIO' monad.  At a high level, certain IO objects such as
-- handles can be associated with a label via 'LObj', while certain
-- operations can then be blessed (via 'blessTCB') to operate on such
-- 'LObj' objects.
--
-- For example, trusted code might define the following:
--
-- > import qualified System.IO as IO
-- > 
-- > type Handle = LObj DCLabel IO.Handle
-- > 
-- > hPutStrLn :: LObj DCLabel IO.Handle -> String -> LIO DCLabel ()
-- > hPutStrLn h = blessTCB "hPutStrLn" IO.hPutStrLn h
-- >
-- > hPutStrLnP :: DCPriv -> LObj DCLabel IO.Handle -> String -> LIO DCLabel ()
-- > hPutStrLnP h = blessPTCB "hPutStrLnP" IO.hPutStrLn h
-- > 
-- > hGetLine :: LObj DCLabel IO.Handle -> LIO DCLabel String
-- > hGetLine h = blessTCB "hGetLine" IO.hGetLine h
--
-- Then application-specific trusted code can wrap a specific label
-- around each 'Handle' using the 'LObjTCB' constructor.
module LIO.TCB.LObj (LObj(..), blessTCB, blessPTCB, GuardIO(..)) where

import safe Data.Typeable

import safe LIO.Core
import safe LIO.Error
import safe LIO.Label
import LIO.TCB

-- | A \"@LObj label object@\" is a wrapper around an IO abstraction
-- of type @object@ (such as a file handle or socket) on which it is
-- safe to do @IO@ operations in the 'LIO' monad when the caller can
-- read and write a the label @label@.  It is the job of the trusted
-- code constructing such a @LObj@ object to ensure both that the same
-- IO object is only ever associated with a single label, and that the
-- abstraction combined with its blessed IO operations (see
-- 'blessTCB') cannot be used to communicate with code running at
-- different labels.
data LObj label object = LObjTCB !label !object deriving (Typeable)

instance LabelOf LObj where
  {-# INLINE labelOf #-}
  labelOf (LObjTCB l _) = l

instance (Label l, Show t) => ShowTCB (LObj l t) where
  showTCB (LObjTCB l t) = show t ++ " {" ++ show l ++ "}"

#include "TypeVals.hs"

-- | Class for lifting 'IO' actions.
class GuardIO l io lio | l io -> lio where
  -- | Lifts an 'IO' action in the 'LIO' monad, executing a guard
  -- before calling the function.
  guardIOTCB :: (LIO l ()) -> io -> lio
instance GuardIO l (IO r) (LIO l r) where
  {-# INLINE guardIOTCB #-}
  guardIOTCB guard io = guard >> ioTCB io
#define GUARDIO(types, vals) \
instance GuardIO l (types -> IO r) (types -> LIO l r) where { \
  {-# INLINE guardIOTCB #-}; \
  guardIOTCB guard io vals = guard >> ioTCB (io vals); \
}
TypesVals (GUARDIO)

-- | This function can be used to turn an 'IO' function into an 'LIO'
-- one.  The 'LIO' version expects a 'LObj' argument, and before
-- performing any IO uses 'guardWrite' to check that the current label
-- can write the label in the 'LObj' object.
-- 
-- The first argument should be the name of the function being defined
-- with @blessTCB@.  Its purpose is to enhance error reporting.
--
-- Note that @io@ and @lio@ are function types (of up to nine
-- arguments), which must be the same in all types except the monad.
-- For example, if @io@ is @Int -> String -> IO ()@, then @lio@ must
-- be @Int -> String -> LIO l ()@.
blessTCB :: (GuardIO l io lio, Label l) =>
            String -> (a -> io) -> (LObj l a) -> lio
{-# INLINE blessTCB #-}
blessTCB name io (LObjTCB l a) =
  guardIOTCB (withContext name $ guardWrite l) (io a)

-- | A variant of 'blessTCB' that produces an 'LIO' function taking a
-- privilege argument.
blessPTCB :: (GuardIO l io lio, PrivDesc l p) =>
             String -> (a -> io) -> Priv p -> (LObj l a) -> lio
{-# INLINE blessPTCB #-}
blessPTCB name io p (LObjTCB l a) =
  guardIOTCB (withContext name $ guardWriteP p l) (io a)