linearscan-0.5.0.0: Linear scan register allocator, formally verified in Coq

Safe HaskellNone
LanguageHaskell2010

LinearScan

Contents

Synopsis

Main entry point

allocate Source

Arguments

:: (Functor m, Applicative m, Monad m) 
=> Int

Maximum number of registers to use

-> BlockInfo m blk1 blk2 op1 op2 
-> OpInfo m op1 op2 
-> [blk1] 
-> m (Either String [blk2]) 

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 provide records that allow viewing and mutating of the original program graph.

If allocation is found to be impossible -- for example if there are simply not enough registers -- a Left value is returned, with a string describing the error.

Blocks

data BlockInfo m blk1 blk2 op1 op2 Source

From the point of view of this library, a basic block is nothing more than an ordered sequence of operations.

Constructors

BlockInfo 

Fields

blockId :: blk1 -> m Int
 
blockSuccessors :: blk1 -> m [Int]
 
splitCriticalEdge :: blk1 -> blk1 -> m (blk1, blk1)
 
blockOps :: blk1 -> ([op1], [op1], [op1])
 
setBlockOps :: blk1 -> [op2] -> [op2] -> [op2] -> blk2
 

Operations

data OpInfo m op1 op2 Source

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 OpKind 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.

Constructors

OpInfo 

Fields

opKind :: op1 -> OpKind
 
opRefs :: op1 -> [VarInfo]
 
moveOp :: PhysReg -> PhysReg -> m [op2]
 
swapOp :: PhysReg -> PhysReg -> m [op2]
 
saveOp :: PhysReg -> Maybe Int -> m [op2]
 
restoreOp :: Maybe Int -> PhysReg -> m [op2]
 
applyAllocs :: op1 -> [(Int, PhysReg)] -> m [op2]
 
showOp1 :: op1 -> String
 

data OpKind Source

Constructors

IsNormal 
IsCall 
IsBranch 

Instances

Variables

data VarInfo Source

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.

Constructors

VarInfo 

data VarKind Source

Constructors

Input 
Temp 
Output 

Instances