-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Linear scan register allocator, formally verified in Coq
--   
--   The <tt>linearscan</tt> library is an implementation -- in Coq,
--   extracted to Haskell -- of a register allocation algorithm developed
--   by Christian Wimmer. It is described in detail in his Masters thesis,
--   which can be found at
--   <a>http://www.christianwimmer.at/Publications/Wimmer04a/Wimmer04a.pdf</a>.
--   A Java implementation of this same algorithm, by that author, is used
--   in Oracle's Graal project.
--   
--   This version of the algorithm was written and verified in Coq,
--   containing over 130 proved lemmas, at over 5K LOC. It was funded as a
--   research project by BAE Systems (<a>http://www.baesystems.com</a>), to
--   be used in an in-house compiler written in Haskell.
--   
--   In order for the Coq code to be usable from Haskell, it is first
--   extracted from Coq as a Haskell library, during which many of Coq's
--   fundamental types are mapped directly onto counterparts in the Haskell
--   Prelude. Thus, it should be within the performance range of an
--   equivalent implementation written directly in Haskell.
--   
--   Note that not every conceivable property of this library has been
--   proven. For some of the lower layers this is true, because the
--   algebraic constraints on these components could be exhaustively
--   described in the context of their use. However, higher-level
--   components represent a great variety of use cases, and not every one
--   of these cases has been proven correct. This represents an ongoing
--   effort, with the hope that proofs will entirely replace the necessity
--   for ad hoc unit testing, and that at some point we can know that any
--   allocation produced by this library must either fail, or be
--   mathematically sound.
--   
--   This library's sole entry point is the <a>LinearScan.allocate</a>
--   function, which takes a list of information about basic blocks to an
--   equivalent list, with annotations indicating allocation choices. In
--   order to use this function you must first convert from your own basic
--   block representation to that of the <tt>BlockInfo</tt>,
--   <tt>OpInfo</tt> and <tt>VarInfo</tt> structures used by this library.
--   For example of such a transformation from a Hoopl Graph, see the file
--   <tt>Tempest.hs</tt> in the tests directory.
@package linearscan
@version 0.1.0.0

module LinearScan

-- | Transform a list of basic blocks containing variable references, into
--   an equivalent list where each reference is associated with a register
--   allocation. Artificial save and restore instructions may also be
--   inserted into blocks to indicate spilling and reloading of variables.
--   
--   In order to call this function, the caller must transform their own
--   basic block representation into a linear series of <a>BlockInfo</a>
--   structures. Each of these structures may be associated with a unique
--   identifier, to assist with processing allocation info afterward.
--   
--   If allocation is found to be impossible -- for example if there are
--   simply not enough registers -- a <a>Left</a> value is returned, with a
--   string describing the error.
allocate :: [BlockInfo] -> Either String [BlockInfo]

-- | From the point of view of this library, a basic block is nothing more
--   than an ordered sequence of operations.
data BlockInfo
BlockInfo :: Int -> [OpInfo] -> BlockInfo
blockId :: BlockInfo -> Int
blockOps :: BlockInfo -> [OpInfo]
defaultBlockInfo :: BlockInfo

-- | Every operation may reference multiple variables and/or specific
--   physical registers. If a physical register is referenced, then that
--   register is considered unavailable for allocation over the range of
--   such references.
--   
--   Certain operations have special significance as to how basic blocks
--   are organized, and the lifetime of allocations. Thus, if an operation
--   begins or ends a loop, or represents a method call, it should be
--   indicated using the <a>OpKind</a> field. Indication of calls is
--   necessary in order to save and restore all registers around a call,
--   but indication of loops is optional, as it's merely avoids reloading
--   of spilled variables inside loop bodies.
data OpInfo
OpInfo :: Int -> Int -> OpKind -> [VarInfo] -> [PhysReg] -> OpInfo
opId :: OpInfo -> Int
opMeta :: OpInfo -> Int
opKind :: OpInfo -> OpKind
varRefs :: OpInfo -> [VarInfo]
regRefs :: OpInfo -> [PhysReg]
data OpKind
Normal :: OpKind
LoopBegin :: OpKind
LoopEnd :: OpKind
Call :: OpKind
defaultOpInfo :: OpInfo

-- | Each variable has associated allocation details, and a flag to
--   indicate whether it must be loaded into a register at its point of
--   use. Variables are also distinguished by their kind, which allows for
--   restricting the scope of their lifetime. For example, output variables
--   are not needed in a basic block until the first point of use, while
--   the lifetime of input variables extends until their final use.
data VarInfo
VarInfo :: Int -> VarKind -> Allocation -> Bool -> VarInfo
varId :: VarInfo -> Int
varKind :: VarInfo -> VarKind
varAlloc :: VarInfo -> Allocation
regRequired :: VarInfo -> Bool
data VarKind
Input :: VarKind
Temp :: VarKind
Output :: VarKind
data Allocation
Unallocated :: Allocation
Register :: PhysReg -> Allocation
Spill :: Allocation
type PhysReg = Int
defaultVarInfo :: VarInfo
instance Show OpKind
instance Eq OpKind
instance Show VarKind
instance Eq VarKind
instance Eq VarInfo
instance Show VarInfo
instance Eq OpInfo
instance Show OpInfo
instance Eq BlockInfo
instance Show BlockInfo