{-# LANGUAGE Rank2Types, KindSignatures, GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances, OverlappingInstances #-} -- | -- <http://okmij.org/ftp/Haskell/regions.html#light-weight> -- -- Lightweight monadic regions -- -- [The Abstract of the paper] -- We present Haskell libraries that statically ensure the safe use of resources such as file -- handles. We statically prevent accessing an already closed handle or forgetting to close it. The -- libraries can be trivially extended to other resources such as database connections and graphic -- contexts. -- -- Because file handles and similar resources are scarce, we want to not just assure their safe use -- but further deallocate them soon after they are no longer needed. Relying on Fluet and -- Morrisett's calculus of nested regions, we contribute a novel, improved, and extended -- implementation of the calculus in Haskell, with file handles as resources. -- -- Our library supports region polymorphism and implicit region subtyping, along with higher-order -- functions, mutable state, recursion, and run-time exceptions. A program may allocate arbitrarily -- many resources and dispose of them in any order, not necessarily LIFO. Region annotations are -- part of an expression's inferred type. Our new Haskell encoding of monadic regions as monad -- transformers needs no witness terms. It assures timely deallocation even when resources have -- markedly different lifetimes and the identity of the longest-living resource is determined only -- dynamically. -- -- For contrast, we also implement a Haskell library for manual resource management, where -- deallocation is explicit and safety is assured by a form of linear types. We implement the linear -- typing in Haskell with the help of phantom types and a parameterized monad to statically track -- the type-state of resources. -- -- Joint work with Chung-chieh Shan. -- -- -- 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 System.SafeHandles (IORT, -- constructors not exported SIO, SHandle, runSIO, newRgn, liftSIO, newSHandle, shDup, IOMode(..), -- re-exported from System.IO shGetLine, shPutStrLn, shIsEOF, 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 GHC.IOBase (ioe_handle) -- | 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 -- | The following is the general definition. It required the following extensions -- -- > {-# LANGUAGE EmptyDataDecls, FunctionalDependencies #-} -- > {-# LANGUAGE UndecidableInstances, OverlappingInstances #-} -- -- to implement the disjunction present in the definition of MonadRaise. -- In particular, OverlappingInstances are needed for TEQ. {- -- 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 instance (Monad m2, TypeCast2 m2 (IORT s m2'), MonadRaise m1 m2') => MonadRaise m1 m2 -- -} -- 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 :: m a -> (Exception -> 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. catch':: IO a -> (Exception -> 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 :: Exception -> Exception 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 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 -- | 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 -> 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 :: RMonadIO m => FilePath -> IOMode -> IORT s m (SHandle (IORT s 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, RMonadIO m2) => SHandle m1 -> m2 String shGetLine (SHandle h) = lIO (hGetLine h) shPutStrLn :: (MonadRaise m1 m2, RMonadIO m2) => SHandle m1 -> String -> m2 () shPutStrLn (SHandle h) = lIO . hPutStrLn h shIsEOF :: (MonadRaise m1 m2, RMonadIO m2) => SHandle m1 -> m2 Bool shIsEOF (SHandle h) = lIO (hIsEOF 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 :: RMonadIO m => SHandle (IORT s1 (IORT s m)) -> IORT s1 (IORT s m) (SHandle (IORT s 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 :: RMonadIO m => Exception -> m a shThrow = lIO . throwIO shCatch :: RMonadIO m => m a -> (Exception -> m a) -> m a shCatch = snag -- | Useful for debugging shReport :: RMonadIO 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 :: RMonadIO m => a -> m (IORef a) sNewIORef = lIO . newIORef sReadIORef :: RMonadIO m => IORef a -> m a sReadIORef = lIO . readIORef sWriteIORef :: RMonadIO m => IORef a -> a -> m () sWriteIORef r v = lIO $ writeIORef r v -- | Standard HList stuff... -- 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