{-# LANGUAGE Rank2Types, GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances, OverlappingInstances #-}
-- Handle-based IO with the assured open/close protocol, see README
-- This file contains the Security kernel. See SafeHandlesTest.hs for tests.
-- This is the final solution: lightweight monadic regions with
-- only type-level enforcement of region discipline
module SafeHandles
(IORT, -- constructors not exported
SIO,
SHandle,
SMonad1IO, -- for the sake of signatures
SMonadIO, -- for the sake of signatures
MonadRaise(..),
runSIO,
newRgn,
liftSIO,
newSHandle,
shDup,
IOMode(..), -- re-exported from System.IO
BufferMode(..), -- re-exported from System.IO
shGetLine,
shPutStrLn,
shPutStr,
shIsEOF,
shSetBuffering,
-- ByteString
shGetSome,
shPut,
shThrow,
shCatch,
shReport,
sNewIORef, -- IORef in SIO
sReadIORef,
sWriteIORef
) where
import System.IO
import Control.Exception
import Control.Monad.Reader
import Control.Monad.Trans
import Data.IORef
import Data.List (find)
import Prelude hiding (catch)
import qualified Data.ByteString as B -- for byte-string operations
-- The IO monad with safe handles and regions (SIO) is implemented as
-- the monad transformer IORT (recursively) applied to IO.
--
-- Each region maintains the state listing all open
-- handles assigned to the region.
-- Since we already have IO, it is easy to implement the state as a
-- mutable list (IORef of the list) and make this reference
-- a pervasive environment.
-- We could have used implicit parameters or implicit configurations to
-- pass that IORef around. Here, we use ReaderT.
-- Since we do IO with our handles, we may be tempted to make
-- the IORT transformer an instance of MonadIO. However, that would
-- give the user the ability to do any IO and so defeat the safety
-- guarantees. The purpose of IORT is to restrict permissible IO
-- operations to an assured set. Since we do need something like MonadIO,
-- we define our own private version here, RMonadIO. It is not exported.
-- Unlike MonadIO, our RMonadIO also supports catching and
-- handling of exceptions.
-- A region is identified by a label, a type eigenvariable (see 's'
-- in ST s).
newtype IORT s m v = IORT{ unIORT:: ReaderT (IORef [HandleR]) m v }
deriving (Monad)
type SIO s = IORT s IO
-- A simple abstract data type to track the duplication of handles
-- using reference counting
data HandleR = HandleR Handle (IORef Integer)
close_hr :: HandleR -> IO ()
close_hr (HandleR h refcount) = do
hPutStrLn stderr $ "Closing " ++ show h
rc <- readIORef refcount
assert (rc > 0) (return ())
writeIORef refcount (pred rc)
if rc > 1
then hPutStrLn stderr " Aliased handle wasn't closed"
else hClose h
new_hr :: Handle -> IO HandleR
new_hr h = newIORef 1 >>= return . HandleR h
eq_hr :: Handle -> HandleR -> Bool
eq_hr h1 (HandleR h2 _) = h1 == h2
-- Lift from one IORT to an IORT in a children region...
-- IORT should be opaque to the user: hence this is not the instance
-- of MonadTrans
liftSIO :: Monad m => IORT s m a -> IORT s1 (IORT s m) a
liftSIO = IORT . lift
-- Raise from one IORT to another: this class lets the user access
-- handles of an ancestor region
-- MonadRaise m1 m2 holds when either
-- - m2 is the same as m1, or
-- - m2 is the sequence of one or more IORT applied to m1.
-- In other words, MonadRaise m1 m2 holds if m1 is an improper
-- `suffix' of m2.
class (Monad m1, Monad m2) => MonadRaise m1 m2 where
lifts :: m1 a -> m2 a
-- The following is the general definition. It required the following extensions
-- {-# LANGUAGE EmptyDataDecls #-}
-- {-# LANGUAGE UndecidableInstances, OverlappingInstances #-}
-- to implement the disjunction present in the definition of MonadRaise.
-- In particular, OverlappingInstances are needed for TEQ.
-- We can actually eliminate overlapping if we write a type function
-- to reverse the order of IORT layers. We would search for a prefix
-- then, which is much easier.
{-
-- more complicated implementation
instance (TEQ m1 m2 eq, MonadRaise' m1 m2 eq) => MonadRaise m1 m2
class (Monad m1, Monad m2) => MonadRaise' m1 m2 eq
instance (Monad m1, Monad m2) => MonadRaise' m1 m2 HTrue
instance MonadRaise m1 m2 => MonadRaise' m1 (IORT s m2) HFalse
data HTrue
data HFalse
class TEQ (a :: * -> *) (b :: * -> *) eq | a b -> eq
instance TEQ a a HTrue
instance TypeCast eq HFalse => TEQ a b eq
-}
-- {-
-- A simpler implementation
instance Monad m => MonadRaise m m where
lifts = id
instance (Monad m2, m2 ~ (IORT s m2'), MonadRaise m1 m2')
=> MonadRaise m1 m2 where
lifts = IORT . lift . lifts
-- -}
-- In GHC 6.6 and earlier, we could only write the following specialized
-- definition. It handles only the fixed number of levels.
{-
instance Monad m => MonadRaise m m
instance Monad m => MonadRaise m (IORT s1 m)
instance Monad m => MonadRaise m (IORT s2 (IORT s1 m))
instance Monad m => MonadRaise m (IORT s3 (IORT s2 (IORT s1 m)))
-}
-- RMonadIO is an internal class, a version of MonadIO
class Monad m => RMonadIO m where
brace :: m a -> (a -> m b) -> (a -> m c) -> m c
snag :: Exception e => m a -> (e -> m a) -> m a
lIO :: IO a -> m a
instance RMonadIO IO where
brace = bracket
snag = catch
lIO = id
-- The following makes sure that a low-level handle (System.IO.Handle)
-- cannot escape in an IO exception. Whenever an IO exception is caught,
-- we remove the handle from the exception before passing it to the
-- exception handler.
-- With GHC 7.x, this sanitization is no longer needed: IOException is
-- opaque (the data constructors of IOError are not exported from
-- GHC.IO.Exceptions). So, the user cannot get hold of a handle
{-
catch':: Exception e => IO a -> (e -> IO a) -> IO a
catch' m f = catch m (f . sanitizeExc)
bracket' :: IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket' before after m =
bracket before after m `catch` (throwIO . sanitizeExc)
sanitizeExc :: IOException -> IOException
sanitizeExc e =
maybe e (\e -> IOException e{ioe_handle = Nothing}) $ ioErrors e
-}
instance RMonadIO m => RMonadIO (ReaderT r m) where
brace before after during = ReaderT (\r ->
let rr :: RMonadIO m => ReaderT r m a -> m a
rr m = runReaderT m r
in brace (rr before) (rr.after) (rr.during))
snag m f = ReaderT(\r ->
runReaderT m r `snag` \e -> runReaderT (f e) r)
lIO = lift . lIO
instance RMonadIO m => RMonadIO (IORT s m) where
brace before after during = IORT
(brace (unIORT before) (unIORT.after) (unIORT.during))
snag m f = IORT ( unIORT m `snag` (unIORT . f) )
lIO = IORT . lIO
-- A safe version of RMonadIO, which is exported
-- SMonadIO is useful in writing signatures
class RMonadIO m => SMonadIO m
instance RMonadIO m => SMonadIO (IORT s m)
-- A different version that enforces the fact the monad must be
-- of the form (IORT s m). It also _provides_ (rather than requires) that
-- m is a member of RMonadIO.
class RMonadIO (UnIORT m) => SMonad1IO m
instance RMonadIO m => SMonad1IO (IORT s m)
type family UnIORT (m :: * -> *) :: * -> *
type instance UnIORT (IORT s m) = m
-- There is no explicit close operation. A handle is automatically
-- closed when its region is finished (normally or abnormally).
newRgn :: RMonadIO m => (forall s. IORT s m v) -> m v
newRgn m = brace (lIO (newIORef [])) after (runReaderT (unIORT m))
where after handles = lIO (readIORef handles >>= mapM_ close)
close h = catch (close_hr h) (\(e::SomeException) -> return ())
runSIO :: (forall s. SIO s v) -> IO v
runSIO = newRgn
-- Our (safe) handle is labeled with the monad where it was created
newtype SHandle (m :: * -> *) = SHandle Handle -- data ctor not exported
-- Create a new handle and assign it to the current region
-- One can use liftIORT (newSHandle ...) to assign the handle to any parent
-- region.
newSHandle :: (m ~ (IORT s' m'), SMonad1IO m) =>
FilePath -> IOMode -> m (SHandle m)
newSHandle fname fmode = IORT r'
where r' = do
h <- lIO $ openFile fname fmode -- may raise exc
handles <- ask
hr <- lIO $ new_hr h
lIO $ modifyIORef handles (hr:)
return (SHandle h)
-- Safe-handle-based IO...
-- The handle is assigned to the current region or its ancestor.
-- So, we have to verify that the label of the handle is the prefix
-- (perhaps improper) of the label of the monad (label of the region).
shGetLine :: (MonadRaise m1 m2, SMonadIO m2) => SHandle m1 -> m2 String
shGetLine (SHandle h) = lIO (hGetLine h)
shPutStrLn :: (MonadRaise m1 m2, SMonadIO m2) => SHandle m1 -> String -> m2 ()
shPutStrLn (SHandle h) = lIO . hPutStrLn h
shPutStr :: (MonadRaise m1 m2, SMonadIO m2) => SHandle m1 -> String -> m2 ()
shPutStr (SHandle h) = lIO . hPutStr h
shIsEOF :: (MonadRaise m1 m2, SMonadIO m2) => SHandle m1 -> m2 Bool
shIsEOF (SHandle h) = lIO (hIsEOF h)
shSetBuffering :: (MonadRaise m1 m2, SMonadIO m2) =>
SHandle m1 -> BufferMode -> m2 ()
shSetBuffering (SHandle h) = lIO . hSetBuffering h
shGetSome :: (MonadRaise m1 m2, SMonadIO m2) =>
SHandle m1 -> Int -> m2 B.ByteString
shGetSome (SHandle h) = lIO . B.hGetSome h
shPut :: (MonadRaise m1 m2, SMonadIO m2) => SHandle m1 -> B.ByteString -> m2 ()
shPut (SHandle h) = lIO . B.hPut h
-- Duplicate a handle, returning a handle that can be used in the parent
-- region (and can be returned from the current region as the result).
-- This operation prolongs the life of a handle based on a
-- _dynamic_ condition. If we know the lifetime of a handle statically,
-- we can execute liftSIO (newSHandle ...) to place the handle in the
-- corresponding region. If we don't know the lifetime of a handle
-- statically, we place it in the inner region, and then extend its lifetime
-- by reassigning to the parent region based on the dynamic conditions.
shDup :: (m ~ (IORT s' m'), SMonad1IO m) =>
SHandle (IORT s1 m) -> IORT s1 m (SHandle m)
shDup (SHandle h) = IORT (do
handles <- ask >>= lIO . readIORef
let Just hr@(HandleR _ refcount) = find (eq_hr h) handles
lIO $ modifyIORef refcount succ
lift $ IORT (do -- in the parent monad
handles <- ask
lIO $ modifyIORef handles (hr:))
return (SHandle h))
-- It seems however that IOErrors don't invalidate the Handles.
-- For example, if EOF is reported, we may try to reposition the `file'
-- and read again. That's why in Posix, EOF and file errors can be cleared.
shThrow :: Exception e => SMonadIO m => e -> m a
shThrow = lIO . throwIO
shCatch :: Exception e => SMonadIO m => m a -> (e -> m a) -> m a
shCatch = snag
-- Useful for debugging
shReport :: SMonadIO m => String -> m ()
shReport = lIO . hPutStrLn stderr
-- make IORef available with SIO, so we may write tests that attempt
-- to leak handles and computations with handles via assignment
sNewIORef :: SMonadIO m => a -> m (IORef a)
sNewIORef = lIO . newIORef
sReadIORef :: SMonadIO m => IORef a -> m a
sReadIORef = lIO . readIORef
sWriteIORef :: SMonadIO m => IORef a -> a -> m ()
sWriteIORef r v = lIO $ writeIORef r v
{-
-- Standard HList stuff... No longer needed with GHC 7.x
class TypeCast a b | a -> b, b->a where typeCast :: a -> b
class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x = x
class TypeCast2 (a :: * -> *) (b :: * -> *) | a -> b, b->a
class TypeCast2' t (a :: * -> *) (b :: * -> *) | t a -> b, t b -> a
class TypeCast2'' t (a :: * -> *) (b :: * -> *) | t a -> b, t b -> a
instance TypeCast2' () a b => TypeCast2 a b
instance TypeCast2'' t a b => TypeCast2' t a b
instance TypeCast2'' () a a
-}