LIO.Run

This module contains functions to launch LIO computations from within the IO monad. These functions are not useful from within LIO code (but not harmful either, since their types are in the IO monad).

This module is intended to be imported into your Main module, for use in invoking LIO code. The functions are also available via LIO and LIO.Core, but those modules will clutter your namespace with symbols you don't need in the IO monad.

Documentation

data LIOState l

Internal state of an LIO computation.

Constructors

LIOState

Fields

lioLabel :: !l

Current label.

lioClearance :: !l

Current clearance.

Instances

Eq l => Eq (LIOState l)

Read l => Read (LIOState l)

Show l => Show (LIOState l)

runLIO :: LIO l a -> LIOState l -> IO (a, LIOState l)

Execute an LIO action, returning its result and the final label state as a pair. Note that it returns a pair whether or not the LIO action throws an exception. Forcing the result value will re-throw the exception, but the label state will always be valid.

See also evalLIO.

evalLIO :: LIO l a -> LIOState l -> IO a

Given an LIO computation and some initial state, return an IO action which when executed will perform the IFC-safe LIO computation.

Because untrusted code cannot execute IO computations, this function should only be useful within trusted code. No harm is done from exposing the evalLIO symbol to untrusted code. (In general, untrusted code is free to produce IO computations, but it cannot execute them.)

Unlike runLIO, this function throws an exception if the underlying LIO action terminates with an exception.