-- 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. It has also been implemented in C++ by
--   Mozilla.
--   
--   This version of the algorithm was written and verified in Coq,
--   containing over 231 proved lemmas, at over 10K 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.
--   
--   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. In the absence of some complete coverage, this
--   version of the library provides an optional, runtime verifier to
--   confirm expectations of correctness, since it is easier to prove the
--   validity of generated data, than of how it was generated.
--   
--   This library's sole entry point is the function
--   <a>LinearScan.allocate</a>, which takes a list of basic blocks, and a
--   functional characterization of those blocks, and produces a new list,
--   with register allocations applied to their component operations.
@package linearscan
@version 1.0.0

module LinearScan

-- | Transform a list of basic blocks, containing variable references, into
--   an equivalent list where each reference has been associated with a
--   register allocation. Artificial save and restore instructions may be
--   inserted into those blocks to indicate spilling and reloading of
--   variables.
--   
--   In order to call this function, the caller must provide records that
--   functionally characterize these blocks and their operations according
--   to an abstract API. This is done so that any program graph conforming
--   to the API may be used, and no particular representation is required.
--   
--   A tuple is return where the first value is a textual dump that
--   describes the complete allocation state. If this value is never
--   forced, that data is not collected.
--   
--   The second value is the resulting list of allocated blocks. If
--   allocation is found to be impossible -- for example if there are not
--   enough registers -- a <a>Left</a> value is returned, with a list of
--   strings describing the error and its possible context. This is usually
--   when the textual dump should be provided, if one's user has selected
--   verbose error output, for example.
allocate :: forall m blk1 blk2 op1 op2. (Functor m, Applicative m, Monad m) => Int -> BlockInfo m blk1 blk2 op1 op2 -> OpInfo m op1 op2 -> UseVerifier -> [blk1] -> m (String, Either [String] [blk2])
data UseVerifier
VerifyDisabled :: UseVerifier
VerifyEnabled :: UseVerifier
VerifyEnabledStrict :: UseVerifier

-- | From the point of view of this library, a basic block is nothing more
--   than an ordered sequence of operations.
data BlockInfo m blk1 blk2 op1 op2
BlockInfo :: (blk1 -> Int) -> (blk1 -> [Int]) -> (blk1 -> blk1 -> m (blk1, blk1)) -> (blk1 -> ([op1], [op1], [op1])) -> (blk1 -> [op2] -> [op2] -> [op2] -> blk2) -> BlockInfo m blk1 blk2 op1 op2

-- | Identify the block with a unique number. The nature and ordering of
--   the number is not significant, only its uniqueness.
[blockId] :: BlockInfo m blk1 blk2 op1 op2 -> blk1 -> Int

-- | The immediate successors of a block.
[blockSuccessors] :: BlockInfo m blk1 blk2 op1 op2 -> blk1 -> [Int]

-- | Given two blocks, insert a new block between them to break up a
--   "critical edge" (where the first block has multiple destinations due
--   to a conditional branch, for example, while the second block has
--   multiple originations due to branches from other blocks). The result
--   is the new pair of blocks at that boundary. Typically, only one of the
--   two will be a newly created block.
[splitCriticalEdge] :: BlockInfo m blk1 blk2 op1 op2 -> blk1 -> blk1 -> m (blk1, blk1)

-- | Return the entry, body, and exit operation of a block. Typically, the
--   entry operation is a "label", and the exit operation is a branch, jump
--   or return.
[blockOps] :: BlockInfo m blk1 blk2 op1 op2 -> blk1 -> ([op1], [op1], [op1])

-- | Replace the set of operations for a block with a set of allocated
--   operations.
[setBlockOps] :: BlockInfo m blk1 blk2 op1 op2 -> blk1 -> [op2] -> [op2] -> [op2] -> blk2

-- | 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 its range of
--   use.
--   
--   Certain operations have special significance as to how basic blocks
--   are organized and lifetime of allocations. Thus, if an operation
--   begins or ends a loop, or represents a method call, this should be
--   indicated using the <a>OpKind</a> field. Indication of calls is
--   necessary for saving and restoring all registers around a call, while
--   indication of loops is optional, as it merely avoids reloading spilled
--   variables inside loop bodies.
data OpInfo m op1 op2
OpInfo :: (op1 -> OpKind) -> (op1 -> [VarInfo]) -> (PhysReg -> VarId -> PhysReg -> m [op2]) -> (PhysReg -> VarId -> m [op2]) -> (VarId -> PhysReg -> m [op2]) -> (op1 -> [((VarId, VarKind), PhysReg)] -> m [op2]) -> (op1 -> String) -> OpInfo m op1 op2

-- | Return the kind of operator prior to allocation.
[opKind] :: OpInfo m op1 op2 -> op1 -> OpKind

-- | Return all variable references for the operation.
[opRefs] :: OpInfo m op1 op2 -> op1 -> [VarInfo]

-- | Create move instruction(s) from one register to another, relating to
--   the given variable.
[moveOp] :: OpInfo m op1 op2 -> PhysReg -> VarId -> PhysReg -> m [op2]

-- | Create a spill instruction from the given restriction, to a stack slot
--   for the given variable.
[saveOp] :: OpInfo m op1 op2 -> PhysReg -> VarId -> m [op2]

-- | Create a load instruction from the stack slot for the given variable,
--   to the given register.
[restoreOp] :: OpInfo m op1 op2 -> VarId -> PhysReg -> m [op2]

-- | Given an operation, and a set of register allocations for each
--   variable used by the operation (differentiated by type of use), apply
--   the allocations to create one or more post-allocation operations.
[applyAllocs] :: OpInfo m op1 op2 -> op1 -> [((VarId, VarKind), PhysReg)] -> m [op2]

-- | Render the given pre-allocation operation as a string.
[showOp1] :: OpInfo m op1 op2 -> op1 -> String
data OpKind
IsNormal :: OpKind
IsCall :: OpKind
IsBranch :: OpKind

-- | Each "virtual variable" has details associated with it that affect the
--   allocation procedure.
data VarInfo
VarInfo :: Either PhysReg VarId -> VarKind -> Bool -> VarInfo

-- | Identify the variable, or if it is an explicit register reference.
[varId] :: VarInfo -> Either PhysReg VarId

-- | The kind of a variable determines the scope of its lifetime, and when
--   it is spilled or loaded to or from stack. 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.
[varKind] :: VarInfo -> VarKind

-- | If true, the variable's value must be loaded into a register at this
--   use position.
[regRequired] :: VarInfo -> Bool
data VarKind
Input :: VarKind
InputOutput :: VarKind
Temp :: VarKind
Output :: VarKind
type VarId = Int
type PhysReg = Int
instance GHC.Classes.Eq LinearScan.UsePos.VarKind
instance GHC.Classes.Eq LinearScan.Blocks.OpKind
instance GHC.Show.Show LinearScan.Blocks.OpKind
instance GHC.Show.Show LinearScan.Verify.AllocError
instance GHC.Show.Show LinearScan.Main.FinalStage
instance GHC.Show.Show LinearScan.LiveSets.BlockLiveSets
instance GHC.Show.Show LinearScan.Trace.SSTrace
instance GHC.Show.Show LinearScan.ScanStateDesc
instance GHC.Show.Show LinearScan.LoopState
instance GHC.Show.Show LinearScan.Verify.RegStateDescSet
instance GHC.Show.Show LinearScan.Resolve.ResolvingMoveSet
instance GHC.Show.Show LinearScan.Trace.SpillConditionT
instance GHC.Show.Show LinearScan.Trace.SplitPositionT