linearscan 0.3.1.0 → 0.4.0.0
raw patch · 25 files changed
+2561/−2761 lines, 25 filesdep −freedep −hoopldep −hspecdep ~basedep ~containersdep ~transformersPVP ok
version bump matches the API change (PVP)
Dependencies removed: free, hoopl, hspec, hspec-expectations, lens, linearscan
Dependency ranges changed: base, containers, transformers
API changes (from Hackage documentation)
- LinearScan: IsLoopBegin :: OpKind
- LinearScan: IsLoopEnd :: OpKind
+ LinearScan: instance Show (Details blk1 blk2 op1 op2 accType)
+ LinearScan: instance Show BlockLiveSets
+ LinearScan: instance Show FinalStage
+ LinearScan: instance Show IntervalDesc
+ LinearScan: instance Show LoopState
+ LinearScan: instance Show RangeDesc
+ LinearScan: instance Show SSError
+ LinearScan: instance Show ScanStateDesc
+ LinearScan: instance Show UsePos
+ LinearScan: instance Show VarKind
+ LinearScan: showOp1 :: OpInfo accType op1 op2 -> op1 -> String
- LinearScan: OpInfo :: (op1 -> OpKind) -> (op1 -> [VarInfo]) -> (PhysReg -> PhysReg -> State accType [op2]) -> (PhysReg -> PhysReg -> State accType [op2]) -> (PhysReg -> Maybe Int -> State accType [op2]) -> (Maybe Int -> PhysReg -> State accType [op2]) -> (op1 -> [(Int, PhysReg)] -> [op2]) -> OpInfo accType op1 op2
+ LinearScan: OpInfo :: (op1 -> OpKind) -> (op1 -> [VarInfo]) -> (PhysReg -> PhysReg -> State accType [op2]) -> (PhysReg -> PhysReg -> State accType [op2]) -> (PhysReg -> Maybe Int -> State accType [op2]) -> (Maybe Int -> PhysReg -> State accType [op2]) -> (op1 -> [(Int, PhysReg)] -> [op2]) -> (op1 -> String) -> OpInfo accType op1 op2
Files
- LinearScan.hs +320/−53
- LinearScan/Allocate.hs +129/−95
- LinearScan/Assign.hs +95/−204
- LinearScan/Blocks.hs +26/−98
- LinearScan/Build.hs +327/−208
- LinearScan/Eqtype.hs +0/−16
- LinearScan/IntMap.hs +29/−1
- LinearScan/Interval.hs +295/−326
- LinearScan/Lib.hs +17/−2
- LinearScan/LiveSets.hs +3/−2
- LinearScan/Loops.hs +412/−0
- LinearScan/Main.hs +54/−24
- LinearScan/Morph.hs +24/−14
- LinearScan/NonEmpty0.hs +15/−0
- LinearScan/Order.hs +0/−17
- LinearScan/Range.hs +47/−83
- LinearScan/Resolve.hs +186/−68
- LinearScan/ScanState.hs +3/−60
- LinearScan/Seq.hs +19/−0
- LinearScan/Split.hs +440/−440
- LinearScan/State.hs +20/−6
- LinearScan/UsePos.hs +97/−3
- linearscan.cabal +3/−21
- test/Main.hs +0/−445
- test/Tempest.hs +0/−575
LinearScan.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE ViewPatterns #-} @@ -9,27 +10,37 @@ ( -- * Main entry point allocate -- * Blocks- , BlockInfo(..)+ , LinearScan.BlockInfo(..) -- * Operations- , OpInfo(..)+ , LinearScan.OpInfo(..) , OpKind(..) -- * Variables , VarId- , VarInfo(..)- , VarKind(..)+ , LinearScan.VarInfo(..)+ , LS.VarKind(..) , PhysReg ) where -import Control.Monad.Trans.State+import Control.Monad.State+import Data.Functor.Identity+import Data.IntMap (IntMap)+import qualified Data.IntMap as M+import Data.IntSet (IntSet)+import qualified Data.IntSet as S+import qualified Data.List as L+-- import Debug.Trace import qualified LinearScan.Blocks as LS+import LinearScan.Blocks as LS+import qualified LinearScan.IntMap as LS+import qualified LinearScan.Interval as LS+import qualified LinearScan.LiveSets as LS+import qualified LinearScan.Loops as LS import qualified LinearScan.Main as LS import qualified LinearScan.Morph as LS-import LinearScan.Blocks- ( VarId- , VarKind(..)- , OpKind(..)- , PhysReg- )+import qualified LinearScan.Range as LS+import qualified LinearScan.ScanState as LS+import qualified LinearScan.UsePos as LS+import qualified LinearScan.Utils as LS -- | 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@@ -39,16 +50,19 @@ -- variables extends until their final use. data VarInfo = VarInfo { varId :: Either PhysReg VarId- , varKind :: VarKind+ , varKind :: LS.VarKind , regRequired :: Bool } -deriving instance Eq VarKind--- deriving instance Show VarKind+deriving instance Eq LS.VarKind+deriving instance Show LS.VarKind -fromVarInfo :: VarInfo -> LS.VarInfo+fromVarInfo :: LinearScan.VarInfo -> LS.VarInfo fromVarInfo (VarInfo a b c) = LS.Build_VarInfo a b c +toVarInfo :: LS.VarInfo -> LinearScan.VarInfo+toVarInfo (LS.Build_VarInfo a b c) = VarInfo a b c+ -- | 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.@@ -62,26 +76,55 @@ -- loop bodies. data OpInfo accType op1 op2 = OpInfo { opKind :: op1 -> OpKind- , opRefs :: op1 -> [VarInfo]+ , opRefs :: op1 -> [LinearScan.VarInfo] , moveOp :: PhysReg -> PhysReg -> State accType [op2] , swapOp :: PhysReg -> PhysReg -> State accType [op2] , saveOp :: PhysReg -> Maybe Int -> State accType [op2] , restoreOp :: Maybe Int -> PhysReg -> State accType [op2] , applyAllocs :: op1 -> [(Int, PhysReg)] -> [op2]+ , showOp1 :: op1 -> String } +showOp1' :: (op1 -> String)+ -> LS.OpId+ -- Interval Id, it's identity, and possible assigned reg+ -> [(Int, Either PhysReg LS.VarId, Maybe PhysReg)]+ -> [(Int, Either PhysReg LS.VarId, Maybe PhysReg)]+ -> op1+ -> String+showOp1' showop pos ins outs o =+ let showerv (Left r) = "r" ++ show r+ showerv (Right v) = "v" ++ show v in+ let render Nothing = ""+ render (Just r) = "=r" ++ show r in+ let marker label (i, erv, reg) =+ "<" ++ label ++ " " ++ showerv erv +++ (if i == either id id erv+ then ""+ else "[" ++ show i ++ "]") ++ render reg ++ ">\n" in+ concatMap (marker "End") outs +++ concatMap (marker "Beg") ins +++ show pos ++ ": " ++ showop o ++ "\n"+ deriving instance Eq OpKind deriving instance Show OpKind -fromOpInfo :: OpInfo accType op1 op2 -> LS.OpInfo accType op1 op2-fromOpInfo (OpInfo a b c d e f g) =- LS.Build_OpInfo a- (map fromVarInfo . b)+fromOpInfo :: LinearScan.OpInfo accType op1 op2 -> LS.OpInfo accType op1 op2+fromOpInfo (OpInfo a b c d e f g h) =+ LS.Build_OpInfo a (map fromVarInfo . b) ((runState .) . c) ((runState .) . d) ((runState .) . e)- ((runState .) . f) g+ ((runState .) . f) g h +toOpInfo :: LS.OpInfo accType op1 op2 -> LinearScan.OpInfo accType op1 op2+toOpInfo (LS.Build_OpInfo a b c d e f g h) =+ OpInfo a (map toVarInfo . b)+ ((StateT .) . fmap (fmap (fmap Identity)) c)+ ((StateT .) . fmap (fmap (fmap Identity)) d)+ ((StateT .) . fmap (fmap (fmap Identity)) e)+ ((StateT .) . fmap (fmap (fmap Identity)) f) g h+ -- | From the point of view of this library, a basic block is nothing more -- than an ordered sequence of operations. data BlockInfo blk1 blk2 op1 op2 = BlockInfo@@ -91,12 +134,225 @@ , setBlockOps :: blk1 -> [op2] -> [op2] -> [op2] -> blk2 } -fromBlockInfo :: BlockInfo blk1 blk2 op1 op2+type IntervalId = Int++data ScanStateDesc = ScanStateDesc+ { _nextInterval :: Int+ , intervals :: [LS.IntervalDesc]+ , fixedIntervals :: [Maybe LS.IntervalDesc]+ , unhandled :: [(IntervalId, Int)]+ , active :: [(IntervalId, PhysReg)]+ , inactive :: [(IntervalId, PhysReg)]+ , handled :: [(IntervalId, Maybe PhysReg)]+ , allocations :: IntMap PhysReg+ }++deriving instance Show LS.IntervalDesc+deriving instance Show LS.RangeDesc+deriving instance Show LS.UsePos++instance Show ScanStateDesc where+ show sd =+ "Unhandled:\n"+ ++ concatMap (\(i, _) -> " " ++ showInterval i ++ "\n")+ (unhandled sd) +++ "Active:\n"+ ++ concatMap (\(i, r) ->+ " r" ++ show r ++ showInterval i ++ "\n")+ (active sd) +++ "Inactive:\n"+ ++ concatMap (\(i, r) ->+ " r" ++ show r ++ showInterval i ++ "\n")+ (inactive sd) +++ "Handled:\n"+ ++ concatMap (\(i, r) ->+ " " ++ showReg r ++ showInterval i ++ "\n")+ (handled sd)+ where+ showInterval i = showIntervalDesc i (intervals sd !! i)++ showReg Nothing = "<stack>"+ showReg (Just r) = "r" ++ show r++showIntervalDesc :: Int -> LS.IntervalDesc -> String+showIntervalDesc i (LS.Build_IntervalDesc iv ib ie rs) =+ "[" ++ show i ++ "]: " ++ " v" ++ show iv ++ " "+ ++ show ib ++ "-" ++ show ie ++ " =>" ++ showRanges rs++showRanges :: [LS.RangeDesc] -> String+showRanges [] = ""+showRanges (LS.Build_RangeDesc rb re us:rs) =+ " " ++ show rb ++ "-" ++ show re+ ++ (case us of+ [] -> ""+ _ -> " [" ++ showUsePositions us ++ "]")+ ++ showRanges rs++showUsePositions :: [LS.UsePos] -> String+showUsePositions [] = ""+showUsePositions [u] = go u+ where+ go (LS.Build_UsePos n req _v) = show n ++ (if req then "" else "?")+showUsePositions (u:us) = go u ++ " " ++ showUsePositions us+ where+ go (LS.Build_UsePos n req _v) = show n ++ (if req then "" else "?")++toScanStateDesc :: LS.ScanStateDesc -> ScanStateDesc+toScanStateDesc (LS.Build_ScanStateDesc a b c d e f g) =+ let rs = L.foldl' (\m (k, mx) -> case mx of+ Nothing -> m+ Just r -> M.insert k r m)+ M.empty g in+ let xs = L.foldl' (\m (k, r) -> M.insert k r m) rs (e ++ f) in+ ScanStateDesc a b c d e f g xs++data LoopState = LoopState+ { activeBlocks :: IntSet+ , visitedBlocks :: IntSet+ , loopHeaderBlocks :: [BlockId]+ , loopEndBlocks :: IntSet+ , forwardBranches :: IntMap IntSet+ , backwardBranches :: IntMap IntSet+ , loopIndices :: IntMap IntSet+ , loopDepths :: IntMap (Int, Int)+ }++instance Show LoopState where+ show LoopState {..} = "LoopState = " +++ "\n activeBlocks = " ++ show (S.toList activeBlocks) +++ "\n visitedBlocks = " ++ show (S.toList visitedBlocks) +++ "\n loopHeaderBlocks = " ++ show loopHeaderBlocks +++ "\n loopEndBlocks = " ++ show (S.toList loopEndBlocks) +++ "\n forwardBranches = " ++ show (map (fmap S.toList) $+ M.toList forwardBranches) +++ "\n backwardBranches = " ++ show (map (fmap S.toList) $+ M.toList backwardBranches) +++ "\n loopIndices = " ++ show (map (fmap S.toList) $+ M.toList loopIndices) +++ "\n loopDepths = " ++ show (M.toList loopDepths)++toLoopState :: LS.LoopState -> LinearScan.LoopState+toLoopState (LS.Build_LoopState a b c d e f g h) =+ LoopState (S.fromList a) (S.fromList b) c (S.fromList d)+ (M.fromList (map (fmap S.fromList) e))+ (M.fromList (map (fmap S.fromList) f))+ (M.fromList (map (fmap S.fromList) g))+ (M.fromList h)++-- tracer :: String -> a -> a+-- tracer x = Debug.Trace.trace ("====================\n" ++ x)++showBlock1 :: (blk1 -> [op1])+ -> LS.BlockId+ -> LS.OpId+ -> [Int]+ -> [Int]+ -> (LS.OpId -> [op1] -> String)+ -> blk1+ -> String+showBlock1 getops bid pos liveIns liveOuts showops b =+ "\nBlock " ++ show bid +++ " => IN:" ++ show liveIns ++ " OUT:" ++ show liveOuts ++ "\n" +++ showops pos (getops b)++showOps1 :: LinearScan.OpInfo accType op1 op2 -> ScanStateDesc -> Int -> [op1]+ -> String+showOps1 _ _ _ [] = ""+showOps1 oinfo sd pos (o:os) =+ let here = pos*2+1 in+ let allocs = allocations sd in+ let k idx (bacc, eacc) i =+ let mreg = M.lookup idx allocs in+ (if LS.ibeg i == here+ then (idx, Right (LS.ivar i), mreg) : bacc+ else bacc,+ if LS.iend i == here+ then (idx, Right (LS.ivar i), mreg) : eacc+ else eacc) in+ let r _idx acc Nothing = acc+ r idx (bacc, eacc) (Just i) =+ let mreg = M.lookup idx allocs in+ (if LS.ibeg i == here+ then (idx, Left idx, mreg) : bacc+ else bacc,+ if LS.iend i == here+ then (idx, Left idx, mreg) : eacc+ else eacc) in+ let (begs, ends) =+ LS.vfoldl'_with_index (0 :: Int) k ([], []) (intervals sd) in+ let (begs', ends') =+ LS.vfoldl'_with_index (0 :: Int) r (begs, ends)+ (fixedIntervals sd) in+ showOp1' (showOp1 oinfo) (pos*2+1) begs' ends' o+ ++ showOps1 oinfo sd (pos+1) os++showBlocks1 :: LinearScan.BlockInfo blk1 blk2 op1 op2+ -> LinearScan.OpInfo accType op1 op2+ -> ScanStateDesc+ -> LS.IntMap LS.BlockLiveSets+ -> [blk1]+ -> String+showBlocks1 binfo oinfo sd ls = go 0+ where+ go _ [] = ""+ go pos (b:bs) =+ let bid = LinearScan.blockId binfo b in+ let (liveIn, liveOut) =+ case LS.coq_IntMap_lookup bid ls of+ Nothing -> (LS.emptyIntSet, LS.emptyIntSet)+ Just s -> (LS.blockLiveIn s, LS.blockLiveOut s) in+ let allops blk = let (x, y, z) = LinearScan.blockOps binfo blk in+ x ++ y ++ z in+ showBlock1 allops bid pos liveIn liveOut (showOps1 oinfo sd) b+ ++ go (pos + length (allops b)) bs++fromBlockInfo :: LinearScan.BlockInfo blk1 blk2 op1 op2 -> LS.BlockInfo blk1 blk2 op1 op2 fromBlockInfo (BlockInfo a b c d) =- LS.Build_BlockInfo a b- (\blk -> let (x, y, z) = c blk in ((x, y), z)) d+ LS.Build_BlockInfo a b (\blk -> let (x, y, z) = c blk in ((x, y), z)) d +toBlockInfo :: LS.BlockInfo blk1 blk2 op1 op2+ -> LinearScan.BlockInfo blk1 blk2 op1 op2+toBlockInfo (LS.Build_BlockInfo a b c d) =+ BlockInfo a b (\blk -> let ((x, y), z) = c blk in (x, y, z)) d++data Details blk1 blk2 op1 op2 accType = Details+ { reason :: Maybe (LS.SSError, LS.FinalStage)+ , liveSets :: [(Int, LS.BlockLiveSets)]+ , inputBlocks :: [blk1]+ , allocatedBlocks :: [blk2]+ , accumulator :: accType+ , scanStatePre :: Maybe ScanStateDesc+ , scanStatePost :: Maybe ScanStateDesc+ , blockInfo :: LinearScan.BlockInfo blk1 blk2 op1 op2+ , opInfo :: LinearScan.OpInfo accType op1 op2+ , loopState :: LoopState+ }++instance Show (Details blk1 blk2 op1 op2 accType) where+ show err = "Reason: " ++ show (reason err) ++ "\n\n"+ ++ ">>> ScanState before allocation:\n"+ ++ showScanStateDesc (scanStatePre err) ++ "\n"+ ++ ">>> ScanState after allocation:\n"+ ++ showScanStateDesc (scanStatePost err) ++ "\n"+ ++ ">>> " ++ show (loopState err) ++ "\n"+ where+ showScanStateDesc Nothing = ""+ showScanStateDesc (Just sd) =+ showBlocks1 (blockInfo err) (opInfo err) sd+ (liveSets err) (inputBlocks err)+ ++ "\n" ++ show sd++deriving instance Show LS.SSError+deriving instance Show LS.FinalStage+deriving instance Show LS.BlockLiveSets++toDetails :: LS.Details blk1 blk2 op1 op2 accType+ -> Details blk1 blk2 op1 op2 accType+toDetails (LS.Build_Details a b c d e f g h i j) =+ Details a b c d e (fmap toScanStateDesc f) (fmap toScanStateDesc g)+ (toBlockInfo h) (toOpInfo i) (toLoopState j)+ -- | 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@@ -109,37 +365,48 @@ -- simply not enough registers -- a 'Left' value is returned, with a string -- describing the error. allocate :: Int -- ^ Maximum number of registers to use- -> BlockInfo blk1 blk2 op1 op2- -> OpInfo accType op1 op2+ -> LinearScan.BlockInfo blk1 blk2 op1 op2+ -> LinearScan.OpInfo accType op1 op2 -> [blk1] -> State accType (Either String [blk2]) allocate 0 _ _ _ = return $ Left "Cannot allocate with no registers" allocate _ _ _ [] = return $ Left "No basic blocks were provided" allocate maxReg (fromBlockInfo -> binfo) (fromOpInfo -> oinfo) blocks = do- eres <- gets (LS.linearScan maxReg binfo oinfo blocks)- case eres of- Left x -> return $ Left $ case x of- LS.ECannotSplitSingleton1 n ->- "Current interval is a singleton (err#1) (" ++ show n ++ ")"- LS.ECannotSplitSingleton2 n ->- "Current interval is a singleton (err#2) (" ++ show n ++ ")"- LS.ECannotSplitSingleton3 n ->- "Current interval is a singleton (err#3) (" ++ show n ++ ")"- LS.ECannotSplitSingleton4 n ->- "Current interval is a singleton (err#4) (" ++ show n ++ ")"- LS.ECannotSplitSingleton5 n ->- "Current interval is a singleton (err#5) (" ++ show n ++ ")"- LS.ECannotSplitSingleton6 n ->- "Current interval is a singleton (err#6) (" ++ show n ++ ")"- LS.ECannotSplitSingleton7 n ->- "Current interval is a singleton (err#7) (" ++ show n ++ ")"- LS.ENoIntervalsToSplit ->- "There are no intervals to split"- LS.ERegisterAlreadyAssigned n ->- "Register is already assigned (" ++ show n ++ ")"- LS.ERegisterAssignmentsOverlap n ->- "Register assignments overlap (" ++ show n ++ ")"- LS.EFuelExhausted -> "Fuel was exhausted"- LS.EUnexpectedNoMoreUnhandled ->- "The unexpected happened: no more unhandled intervals"- Right (z, acc) -> put acc >> return (Right z)+ res <- gets (LS.linearScan maxReg binfo oinfo blocks)+ let res' = toDetails res+ put $ accumulator res'+ case reason res' of+ Just (err, _) -> reportError res' err+ Nothing ->+ -- tracer (show res') $+ return $ Right (allocatedBlocks res')+ where+ -- reportError res err =+ -- return $ Left $ tracer (show res) $ reasonToStr err+ reportError _res err =+ return $ Left $ reasonToStr err++ reasonToStr r = case r of+ LS.ERegistersExhausted _ ->+ "No registers available for allocation"+ LS.ENoValidSplitPositionUnh xid splitPos ->+ "No split position could be found for unhandled interval "+ ++ show xid ++ " @ " ++ show splitPos+ LS.ENoValidSplitPosition xid splitPos ->+ "No split position could be found for " ++ show xid+ ++ " @ " ++ show splitPos+ LS.ECannotSplitSingleton1 n ->+ "Current interval is a singleton (err#1) (" ++ show n ++ ")"+ LS.ECannotSplitSingleton2 n ->+ "Current interval is a singleton (err#2) (" ++ show n ++ ")"+ LS.ECannotSplitSingleton3 n ->+ "Current interval is a singleton (err#3) (" ++ show n ++ ")"+ LS.ENoIntervalsToSplit ->+ "There are no intervals to split"+ LS.ERegisterAlreadyAssigned n ->+ "Register is already assigned (" ++ show n ++ ")"+ LS.ERegisterAssignmentsOverlap n ->+ "Register assignments overlap (" ++ show n ++ ")"+ LS.EFuelExhausted -> "Fuel was exhausted"+ LS.EUnexpectedNoMoreUnhandled ->+ "The unexpected happened: no more unhandled intervals"
LinearScan/Allocate.hs view
@@ -52,12 +52,10 @@ Cursor.withCursor maxReg pre (\sd _ -> let {int = Cursor.curIntDetails maxReg sd} in Morph.return_- (LinearScan.Utils.vfoldl' maxReg (\mx v ->- Lib.option_choose mx- (case v of {- Prelude.Just i -> Interval.intervalIntersectionPoint ( int) ( i);- Prelude.Nothing -> Prelude.Nothing})) Prelude.Nothing- (ScanState.fixedIntervals maxReg sd)))+ (case LinearScan.Utils.nth maxReg (ScanState.fixedIntervals maxReg sd)+ reg of {+ Prelude.Just i -> Interval.intervalIntersectionPoint ( int) ( i);+ Prelude.Nothing -> Prelude.Nothing})) updateRegisterPos :: Prelude.Int -> ([] (Prelude.Maybe Lib.Coq_oddnum)) -> Prelude.Int -> (Prelude.Maybe Lib.Coq_oddnum) -> []@@ -78,6 +76,7 @@ () () (Prelude.Maybe (Morph.SState () () PhysReg)) tryAllocateFreeReg maxReg pre = Cursor.withCursor maxReg pre (\sd _ ->+ let {pos = Cursor.curPosition maxReg sd} in let { go = \f v p -> case p of {@@ -100,43 +99,47 @@ (ScanState.inactive maxReg sd)} in let {- freeUntilPos = Data.List.foldl'- (go (\i ->- Interval.intervalIntersectionPoint- (- (LinearScan.Utils.nth- (ScanState.nextInterval maxReg sd)- (ScanState.intervals maxReg sd) i))- ( (Cursor.curIntDetails maxReg sd)))) freeUntilPos'- intersectingIntervals}+ freeUntilPos'' = Data.List.foldl'+ (go (\i ->+ Interval.intervalIntersectionPoint+ (+ (LinearScan.Utils.nth+ (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) i))+ ( (Cursor.curIntDetails maxReg sd))))+ freeUntilPos' intersectingIntervals} in+ let {+ freeUntilPos = (LinearScan.Utils.vfoldl'_with_index) maxReg+ (\reg acc mint ->+ case mint of {+ Prelude.Just int ->+ updateRegisterPos maxReg acc reg+ (Interval.intervalIntersectionPoint ( int)+ ( (Cursor.curIntDetails maxReg sd)));+ Prelude.Nothing -> acc}) freeUntilPos''+ (ScanState.fixedIntervals maxReg sd)}+ in case ScanState.registerWithHighestPos maxReg freeUntilPos of { (,) reg mres -> let { success = Morph.stbind (\x -> Morph.return_ reg) (Morph.moveUnhandledToActive maxReg pre reg)} in- let {- maction = case mres of {- Prelude.Just n ->- case Eqtype.eq_op Ssrnat.nat_eqType ( (unsafeCoerce n))- (unsafeCoerce ((Prelude.succ) 0)) of {- Prelude.True -> Prelude.Nothing;- Prelude.False -> Prelude.Just- (case (Prelude.<=) ((Prelude.succ)- (Interval.intervalEnd- ( (Cursor.curIntDetails maxReg sd)))) - ( n) of {- Prelude.True -> success;- Prelude.False ->- Morph.stbind (\x ->- Morph.stbind (\x0 -> Morph.return_ reg)- (Morph.moveUnhandledToActive maxReg pre reg))- (Split.splitCurrentInterval maxReg pre- (Split.BeforePos n))})};- Prelude.Nothing -> Prelude.Just success}}- in- Morph.return_ maction})+ Morph.return_+ (case mres of {+ Prelude.Just n ->+ case (Prelude.<=) ( n) pos of {+ Prelude.True -> Prelude.Nothing;+ Prelude.False -> Prelude.Just+ (case (Prelude.<=) ((Prelude.succ)+ (Interval.intervalEnd+ ( (Cursor.curIntDetails maxReg sd)))) ( n) of {+ Prelude.True -> success;+ Prelude.False ->+ Morph.stbind (\x -> success)+ (Split.splitCurrentInterval maxReg pre (Split.BeforePos n))})};+ Prelude.Nothing -> Prelude.Just success})}) allocateBlockedReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState () () (Prelude.Maybe PhysReg)@@ -146,68 +149,78 @@ in let {pos = Cursor.curPosition maxReg sd} in let {- go = \v p ->+ go = \n v p -> case p of {- (,) i r ->+ (,) int r -> let { atPos = \u -> Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos) (unsafeCoerce (UsePos.uloc u))} in let {- pos' = case Interval.findIntervalUsePos- (Interval.getIntervalDesc- (- (LinearScan.Utils.nth- (ScanState.nextInterval maxReg sd)- (ScanState.intervals maxReg sd) i))) atPos of {+ pos' = case Interval.findIntervalUsePos ( int) atPos of { Prelude.Just s -> Prelude.Just Lib.odd1;- Prelude.Nothing ->- Interval.nextUseAfter- (Interval.getIntervalDesc- (- (LinearScan.Utils.nth- (ScanState.nextInterval maxReg sd)- (ScanState.intervals maxReg sd) i))) start}}+ Prelude.Nothing -> Interval.nextUseAfter ( int) start}} in- updateRegisterPos maxReg v r pos'}}+ updateRegisterPos n v r pos'}} in let {- nextUsePos' = Data.List.foldl' go+ resolve = \xs ->+ Prelude.map (\i -> (,)+ (Interval.packInterval+ (+ (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) (Prelude.fst i))))+ (Prelude.snd i)) xs}+ in+ let {+ nextUsePos' = Data.List.foldl' (go maxReg) (Data.List.replicate maxReg Prelude.Nothing)- (ScanState.active maxReg sd)}+ (resolve (ScanState.active maxReg sd))} in let {- intersectingIntervals = Prelude.filter (\x ->- Interval.intervalsIntersect- ( (Cursor.curIntDetails maxReg sd))- (- (LinearScan.Utils.nth- (ScanState.nextInterval maxReg sd)- (ScanState.intervals maxReg sd)- (Prelude.fst x))))- (ScanState.inactive maxReg sd)}+ intersectingIntervals = (Prelude.++)+ (Prelude.filter (\x ->+ Interval.intervalsIntersect+ ( (Cursor.curIntDetails maxReg sd))+ ( (Prelude.fst x)))+ (resolve (ScanState.inactive maxReg sd)))+ ((LinearScan.Utils.vfoldl'_with_index) maxReg+ (\reg acc mint ->+ case mint of {+ Prelude.Just int ->+ case Interval.intervalsIntersect+ ( (Cursor.curIntDetails maxReg sd))+ ( int) of {+ Prelude.True -> (:) ((,) int reg) acc;+ Prelude.False -> acc};+ Prelude.Nothing -> acc}) []+ (ScanState.fixedIntervals maxReg sd))} in- let {nextUsePos = Data.List.foldl' go nextUsePos' intersectingIntervals}+ let {+ nextUsePos = Data.List.foldl' (go maxReg) nextUsePos'+ intersectingIntervals} in case ScanState.registerWithHighestPos maxReg nextUsePos of { (,) reg mres -> case case mres of {- Prelude.Just n -> (Prelude.<=) ((Prelude.succ) ( n)) start;+ Prelude.Just n ->+ (Prelude.<=) ((Prelude.succ) ( n))+ (case Interval.lookupUsePos+ ( (Cursor.curIntDetails maxReg sd)) (\u ->+ (Prelude.<=) pos (UsePos.uloc u)) of {+ Prelude.Just s -> s;+ Prelude.Nothing ->+ Interval.intervalEnd ( (Cursor.curIntDetails maxReg sd))}); Prelude.Nothing -> Prelude.False} of { Prelude.True ->+ let {+ p = Interval.firstUseReqRegOrEnd ( (Cursor.curIntDetails maxReg sd))}+ in Morph.stbind (\x ->- Morph.stbind (\mloc ->- Morph.stbind (\x0 ->- Morph.stbind (\x1 -> Morph.return_ Prelude.Nothing)- (Morph.weakenHasLen_ maxReg pre))- (case mloc of {- Prelude.Just n ->- Split.splitCurrentInterval maxReg pre (Split.BeforePos n);- Prelude.Nothing -> Morph.return_ ()}))- (intersectsWithFixedInterval maxReg pre reg))- (Split.splitCurrentInterval maxReg pre- Split.BeforeFirstUsePosReqReg);+ Morph.stbind (\x0 -> Morph.return_ Prelude.Nothing)+ (Morph.moveUnhandledToHandled maxReg pre))+ (Split.splitCurrentInterval maxReg pre (Split.BeforePos p)); Prelude.False -> Morph.stbind (\x -> Morph.stbind (\x0 ->@@ -221,7 +234,7 @@ Prelude.Nothing -> Morph.return_ ()})) (intersectsWithFixedInterval maxReg pre reg)) (Split.splitActiveIntervalForReg maxReg pre reg pos))- (Split.splitAnyInactiveIntervalForReg maxReg pre reg)}})+ (Split.splitAnyInactiveIntervalForReg maxReg pre reg pos)}}) morphlen_transport :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.ScanStateDesc -> ScanState.IntervalId ->@@ -252,7 +265,7 @@ Prelude.True -> Morph.moveActiveToHandled maxReg z (unsafeCoerce x); Prelude.False -> case Prelude.not- (Interval.intervalCoversPos+ (Interval.posWithinInterval ( (LinearScan.Utils.nth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x))) pos) of {@@ -316,7 +329,7 @@ in f filtered_var; Prelude.False ->- case Interval.intervalCoversPos+ case Interval.posWithinInterval ( (LinearScan.Utils.nth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x))) pos of {@@ -352,24 +365,41 @@ handleInterval maxReg pre = Cursor.withCursor maxReg pre (\sd _ -> let {position = Cursor.curPosition maxReg sd} in- Morph.stbind (\x ->- Morph.stbind (\x0 ->- Morph.stbind (\mres ->- case mres of {- Prelude.Just x1 -> IState.imap (\x2 -> Prelude.Just x2) x1;- Prelude.Nothing -> allocateBlockedReg maxReg pre})- (tryAllocateFreeReg maxReg pre))+ case Interval.firstUsePos+ (Interval.getIntervalDesc ( (Cursor.curIntDetails maxReg sd))) of {+ Prelude.Just u ->+ Morph.stbind (\x ->+ Morph.stbind (\x0 ->+ Morph.stbind (\mres ->+ case mres of {+ Prelude.Just x1 -> IState.imap (\x2 -> Prelude.Just x2) x1;+ Prelude.Nothing -> allocateBlockedReg maxReg pre})+ (tryAllocateFreeReg maxReg pre))+ (Morph.liftLen maxReg pre (\sd0 ->+ checkInactiveIntervals maxReg sd0 position))) (Morph.liftLen maxReg pre (\sd0 ->- checkInactiveIntervals maxReg sd0 position)))- (Morph.liftLen maxReg pre (\sd0 ->- checkActiveIntervals maxReg sd0 position)))+ checkActiveIntervals maxReg sd0 position));+ Prelude.Nothing ->+ Morph.stbind (\x -> Morph.return_ Prelude.Nothing)+ (Morph.moveUnhandledToHandled maxReg pre)}) +finalizeScanState :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int ->+ ScanState.ScanStateDesc+finalizeScanState maxReg sd finalPos =+ case Morph.stbind (\x -> checkInactiveIntervals maxReg sd finalPos)+ (checkActiveIntervals maxReg sd finalPos) (Morph.Build_SSInfo sd __) of {+ Prelude.Left s -> sd;+ Prelude.Right p ->+ case p of {+ (,) u ss -> Morph.thisDesc maxReg sd ss}}+ walkIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int ->- Prelude.Either Morph.SSError ScanState.ScanStateSig+ Prelude.Either ((,) Morph.SSError ScanState.ScanStateSig)+ ScanState.ScanStateSig walkIntervals maxReg sd positions = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))- (\_ -> Prelude.Left- Morph.EFuelExhausted)+ (\_ -> Prelude.Left ((,) Morph.EFuelExhausted+ (ScanState.packScanState maxReg ScanState.InUse sd))) (\n -> let { go = let {@@ -380,7 +410,9 @@ __)) (\cnt -> case handleInterval maxReg sd ss of {- Prelude.Left err -> Prelude.Left err;+ Prelude.Left err -> Prelude.Left ((,) err+ (ScanState.packScanState maxReg ScanState.InUse+ (Morph.thisDesc maxReg sd ss))); Prelude.Right p -> case p of { (,) o ss' ->@@ -393,8 +425,10 @@ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> Prelude.Right ss')- (\n0 -> Prelude.Left- Morph.EUnexpectedNoMoreUnhandled)+ (\n0 -> Prelude.Left ((,)+ Morph.EUnexpectedNoMoreUnhandled+ (ScanState.packScanState maxReg ScanState.InUse+ (Morph.thisDesc maxReg sd ss')))) cnt}}}) count0} in go}
LinearScan/Assign.hs view
@@ -17,12 +17,14 @@ import qualified LinearScan.Graph as Graph import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Interval as Interval+import qualified LinearScan.Lib as Lib import qualified LinearScan.LiveSets as LiveSets import qualified LinearScan.Resolve as Resolve-import qualified LinearScan.ScanState as ScanState import qualified LinearScan.State as State+import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype+import qualified LinearScan.Seq as Seq import qualified LinearScan.Ssrnat as Ssrnat @@ -68,6 +70,16 @@ type AssnState accType a = State.State (AssnStateInfo accType) a +swapOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.PhysReg ->+ Blocks.PhysReg -> AssnState a3 ([] a2)+swapOpM maxReg oinfo sreg dreg =+ State.bind (\assn ->+ case Blocks.swapOp maxReg oinfo sreg dreg (assnAcc assn) of {+ (,) mop acc' ->+ State.bind (\x -> State.pure mop)+ (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn)+ (assnBlockEnd assn) acc'))}) State.get+ moveOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.PhysReg -> Blocks.PhysReg -> AssnState a3 ([] a2) moveOpM maxReg oinfo sreg dreg =@@ -98,190 +110,72 @@ (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn) (assnBlockEnd assn) acc'))}) State.get -pairM :: (AssnState a1 a2) -> (AssnState a1 a3) -> AssnState a1 ((,) a2 a3)-pairM x y =- State.bind (\x' -> State.bind (\y' -> State.pure ((,) x' y')) y) x--savesAndRestores :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.OpId ->- Blocks.VarInfo -> Blocks.PhysReg -> Interval.IntervalDesc- -> IntMap.IntSet -> AssnState a3 ((,) ([] a2) ([] a2))-savesAndRestores maxReg oinfo opid v reg int outs =- case Blocks.varId maxReg v of {- Prelude.Left p -> State.pure ((,) [] []);- Prelude.Right vid ->- State.bind (\assn ->- let {knd = Blocks.varKind maxReg v} in- let {- atBoundary = (Prelude.||)- ((Prelude.&&)- (Eqtype.eq_op Blocks.coq_VarKind_eqType- (unsafeCoerce knd) (unsafeCoerce Blocks.Input))- (Eqtype.eq_op Ssrnat.nat_eqType- (unsafeCoerce (assnBlockBeg assn))- (unsafeCoerce opid)))- ((Prelude.&&)- (Eqtype.eq_op Blocks.coq_VarKind_eqType- (unsafeCoerce knd) (unsafeCoerce Blocks.Output))- (Eqtype.eq_op Ssrnat.nat_eqType- (unsafeCoerce ((Prelude.succ) ((Prelude.succ)- opid))) (unsafeCoerce (assnBlockEnd assn))))}- in- let {- isFirst = Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)- (unsafeCoerce (Interval.firstUsePos int))- (unsafeCoerce (Prelude.Just opid))}- in- let {- isLast = Eqtype.eq_op- (Eqtype.option_eqType- (Eqtype.sig_eqType Ssrnat.nat_eqType- (unsafeCoerce Ssrnat.odd)))- (unsafeCoerce (Interval.nextUseAfter int opid))- (unsafeCoerce Prelude.Nothing)}- in- let {save = saveOpM maxReg oinfo reg (Prelude.Just vid)} in- let {- msave = case atBoundary of {- Prelude.True -> State.pure [];- Prelude.False -> save}}- in- let {restore = restoreOpM maxReg oinfo (Prelude.Just vid) reg} in- let {- mrestore = case atBoundary of {- Prelude.True -> State.pure [];- Prelude.False -> restore}}- in- case knd of {- Blocks.Input ->- case Interval.iknd int of {- Interval.Whole -> State.pure ((,) [] []);- Interval.LeftMost ->- case isLast of {- Prelude.True -> pairM (State.pure []) save;- Prelude.False -> State.pure ((,) [] [])};- Interval.Middle ->- case isFirst of {- Prelude.True ->- case isLast of {- Prelude.True -> pairM mrestore save;- Prelude.False -> pairM mrestore (State.pure [])};- Prelude.False ->- case isLast of {- Prelude.True -> pairM (State.pure []) save;- Prelude.False -> State.pure ((,) [] [])}};- Interval.RightMost ->- case isFirst of {- Prelude.True -> pairM mrestore (State.pure []);- Prelude.False -> State.pure ((,) [] [])}};- Blocks.Temp -> State.pure ((,) [] []);- Blocks.Output ->- case Interval.iknd int of {- Interval.LeftMost ->- case isLast of {- Prelude.True -> pairM (State.pure []) msave;- Prelude.False -> State.pure ((,) [] [])};- Interval.Middle ->- case isLast of {- Prelude.True -> pairM (State.pure []) msave;- Prelude.False -> State.pure ((,) [] [])};- _ -> State.pure ((,) [] [])}}) State.get}--collectAllocs :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Prelude.Int ->- IntMap.IntSet -> ([] ((,) Interval.IntervalDesc PhysReg)) ->- ((,) ((,) ([] ((,) Blocks.VarId PhysReg)) ([] a2)) ([] a2))- -> Blocks.VarInfo -> State.State (AssnStateInfo a3)- ((,) ((,) ([] ((,) Blocks.VarId PhysReg)) ([] a2)) ([] a2))-collectAllocs maxReg oinfo opid outs ints acc v =+varAllocs :: Prelude.Int -> Prelude.Int -> ([] Resolve.Allocation) ->+ Blocks.VarInfo -> [] ((,) Blocks.VarId PhysReg)+varAllocs maxReg opid allocs v = case Blocks.varId maxReg v of {- Prelude.Left p -> State.pure acc;+ Prelude.Left p -> []; Prelude.Right vid ->- let {- v_ints = Prelude.filter (\x ->- ScanState.isWithin (Prelude.fst x) vid opid) ints}- in- State.forFoldM acc v_ints (\acc' x ->- case x of {- (,) int reg ->- case acc' of {- (,) p saves' ->- case p of {- (,) allocs' restores' ->- State.bind (\res ->- case res of {- (,) rs ss ->- State.pure ((,) ((,) ((:) ((,) vid reg) allocs')- ((Prelude.++) rs restores')) ((Prelude.++) ss saves'))})- (savesAndRestores maxReg oinfo opid v reg int outs)}}})}--doAllocations :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]- ((,) Interval.IntervalDesc PhysReg)) -> IntMap.IntSet -> a1- -> AssnState a3 ([] a2)-doAllocations maxReg oinfo ints outs op =- State.bind (\assn ->- let {opid = assnOpId assn} in- let {vars = Blocks.opRefs maxReg oinfo op} in- State.bind (\res ->- case res of {- (,) y saves ->- case y of {- (,) allocs restores ->- let {op' = Blocks.applyAllocs maxReg oinfo op allocs} in- State.bind (\x ->- State.pure ((Prelude.++) restores ((Prelude.++) op' saves)))- (State.modify (\assn' -> Build_AssnStateInfo ((Prelude.succ)- ((Prelude.succ) opid)) (assnBlockBeg assn')- (assnBlockEnd assn') (assnAcc assn')))}})- (State.forFoldM ((,) ((,) [] []) []) vars- (collectAllocs maxReg oinfo opid outs ints))) State.get+ Prelude.map (\x -> (,) vid x)+ (Lib.catMaybes+ (Prelude.map (\i -> Resolve.intReg maxReg i)+ (Prelude.filter (\i ->+ let {int = Resolve.intVal maxReg i} in+ (Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce (Interval.ivar int)) (unsafeCoerce vid))+ ((Prelude.&&) ((Prelude.<=) (Interval.ibeg int) opid)+ (case Blocks.varKind maxReg v of {+ UsePos.Input -> (Prelude.<=) opid (Interval.iend int);+ _ -> (Prelude.<=) ((Prelude.succ) opid) (Interval.iend int)})))+ allocs)))} generateMoves :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]- ((,) (Prelude.Maybe (Prelude.Either PhysReg Prelude.Int))- (Prelude.Maybe (Prelude.Either PhysReg Prelude.Int)))) ->- AssnState a3 ([] a2)+ Resolve.ResolvingMove) -> AssnState a3 ([] a2) generateMoves maxReg oinfo moves =- State.forFoldM [] moves (\acc mv ->+ State.forFoldrM [] moves (\mv acc -> State.bind (\mops -> State.pure (case mops of { Prelude.Just ops -> (Prelude.++) ops acc; Prelude.Nothing -> acc})) (case mv of {- (,) o o0 ->- case o of {- Prelude.Just s ->- case s of {- Prelude.Left sreg ->- case o0 of {- Prelude.Just s0 ->- case s0 of {- Prelude.Left dreg ->- State.fmap (\x -> Prelude.Just x)- (moveOpM maxReg oinfo sreg dreg);- Prelude.Right vid ->- State.fmap (\x -> Prelude.Just x)- (saveOpM maxReg oinfo sreg (Prelude.Just vid))};- Prelude.Nothing ->- State.fmap (\x -> Prelude.Just x)- (saveOpM maxReg oinfo sreg Prelude.Nothing)};- Prelude.Right vid ->- case o0 of {- Prelude.Just s0 ->- case s0 of {- Prelude.Left dreg ->- State.fmap (\x -> Prelude.Just x)- (restoreOpM maxReg oinfo (Prelude.Just vid) dreg);- Prelude.Right n -> State.pure Prelude.Nothing};- Prelude.Nothing -> State.pure Prelude.Nothing}};- Prelude.Nothing ->- case o0 of {- Prelude.Just s ->- case s of {- Prelude.Left dreg ->- State.fmap (\x -> Prelude.Just x)- (restoreOpM maxReg oinfo Prelude.Nothing dreg);- Prelude.Right n -> State.pure Prelude.Nothing};- Prelude.Nothing -> State.pure Prelude.Nothing}}}))+ Resolve.Move sreg dreg ->+ State.fmap (\x -> Prelude.Just x) (moveOpM maxReg oinfo sreg dreg);+ Resolve.Swap sreg dreg ->+ State.fmap (\x -> Prelude.Just x) (swapOpM maxReg oinfo sreg dreg);+ Resolve.Spill sreg vid ->+ State.fmap (\x -> Prelude.Just x)+ (saveOpM maxReg oinfo sreg (Prelude.Just vid));+ Resolve.Restore vid dreg ->+ State.fmap (\x -> Prelude.Just x)+ (restoreOpM maxReg oinfo (Prelude.Just vid) dreg);+ Resolve.Nop -> State.pure Prelude.Nothing})) +doAllocations :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]+ Resolve.Allocation) -> a1 -> AssnState a3 ([] a2)+doAllocations maxReg oinfo allocs op =+ State.bind (\assn ->+ let {opid = assnOpId assn} in+ let {vars = Blocks.opRefs maxReg oinfo op} in+ let {+ regs = State.concat (Prelude.map (varAllocs maxReg opid allocs) vars)}+ in+ let {ops = Blocks.applyAllocs maxReg oinfo op regs} in+ State.bind (\transitions ->+ State.bind (\x -> State.pure ((Prelude.++) ops transitions))+ (State.modify (\assn' -> Build_AssnStateInfo ((Prelude.succ)+ ((Prelude.succ) opid)) (assnBlockBeg assn') (assnBlockEnd assn')+ (assnAcc assn'))))+ (case (Prelude.&&) ((Prelude.<=) (assnBlockBeg assn) opid)+ ((Prelude.<=) ((Prelude.succ) opid) (assnBlockEnd assn)) of {+ Prelude.True ->+ generateMoves maxReg oinfo+ (Resolve.determineMoves maxReg+ (Resolve.resolvingMoves maxReg allocs opid ((Prelude.succ)+ ((Prelude.succ) opid))));+ Prelude.False -> State.pure []})) State.get+ resolveMappings :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Prelude.Int -> ([] a2) -> (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) -> AssnState a3 ([] a2)@@ -295,31 +189,26 @@ State.bind (\emoves -> let {opsm'' = (Prelude.++) opsm' emoves} in State.pure opsm'') (generateMoves maxReg oinfo- (unsafeCoerce+ (Prelude.map (Resolve.moveFromGraph maxReg) (Graph.topsort (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType) gend)))) (generateMoves maxReg oinfo- (unsafeCoerce+ (Prelude.map (Resolve.moveFromGraph maxReg) (Graph.topsort (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType) gbeg)))}; Prelude.Nothing -> State.pure opsm} considerOps :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- (Blocks.OpInfo a5 a3 a4) -> (IntMap.IntSet -> a3 -> AssnState- a5 ([] a4)) -> (IntMap.IntMap LiveSets.BlockLiveSets) ->- (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) -> ([] a1) ->- State.State (AssnStateInfo a5) ([] a2)+ (Blocks.OpInfo a5 a3 a4) -> (a3 -> AssnState a5 ([] a4)) ->+ (IntMap.IntMap LiveSets.BlockLiveSets) -> (IntMap.IntMap+ ((,) Graph.Graph Graph.Graph)) -> ([] a1) -> State.State+ (AssnStateInfo a5) ([] a2) considerOps maxReg binfo oinfo f liveSets mappings = State.mapM (\blk -> let {ops = Blocks.blockOps binfo blk} in let {bid = Blocks.blockId binfo blk} in- let {- outs = case IntMap.coq_IntMap_lookup bid liveSets of {- Prelude.Just ls -> LiveSets.blockLiveOut ls;- Prelude.Nothing -> IntMap.emptyIntSet}}- in case ops of { (,) p opse -> case p of {@@ -329,12 +218,24 @@ State.bind (\opsm' -> State.bind (\opse' -> State.bind (\opsm'' ->- State.pure- (Blocks.setBlockOps binfo blk opsb' opsm'' opse'))+ case opsb' of {+ [] ->+ State.pure+ (Blocks.setBlockOps binfo blk opsb' opsm'' opse');+ (:) b bs ->+ case opse' of {+ [] ->+ State.pure+ (Blocks.setBlockOps binfo blk opsb' opsm'' opse');+ (:) e es ->+ State.pure+ (Blocks.setBlockOps binfo blk ((:) b [])+ ((Prelude.++) bs+ ((Prelude.++) opsm'' (Seq.belast e es))) ((:)+ (Seq.last e es) []))}}) (resolveMappings maxReg oinfo bid opsm' mappings))- (State.concatMapM (f outs) opse))- (State.concatMapM (f outs) opsm))- (State.concatMapM (f outs) opsb))+ (State.concatMapM f opse)) (State.concatMapM f opsm))+ (State.concatMapM f opsb)) (State.modify (\assn -> Build_AssnStateInfo (assnOpId assn) ((Prelude.+) (assnOpId assn) (Ssrnat.double (Data.List.length opsb)))@@ -344,22 +245,12 @@ (assnAcc assn)))}}) assignRegNum :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- (Blocks.OpInfo a5 a3 a4) -> ScanState.ScanStateDesc ->+ (Blocks.OpInfo a5 a3 a4) -> ([] Resolve.Allocation) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> (IntMap.IntMap Resolve.BlockMoves) -> ([] a1) -> a5 -> (,) ([] a2) a5-assignRegNum maxReg binfo oinfo sd liveSets mappings blocks acc =- case considerOps maxReg binfo oinfo- (doAllocations maxReg oinfo- (Prelude.map (\x -> (,)- (Interval.getIntervalDesc- (- (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)- (ScanState.intervals maxReg sd) (Prelude.fst x))))- (Prelude.snd x))- ((Prelude.++) (ScanState.handled maxReg sd)- ((Prelude.++) (ScanState.active maxReg sd)- (ScanState.inactive maxReg sd))))) liveSets mappings blocks- (Build_AssnStateInfo ((Prelude.succ) 0) ((Prelude.succ) 0)- ((Prelude.succ) 0) acc) of {+assignRegNum maxReg binfo oinfo allocs liveSets mappings blocks acc =+ case considerOps maxReg binfo oinfo (doAllocations maxReg oinfo allocs)+ liveSets mappings blocks (Build_AssnStateInfo ((Prelude.succ) 0)+ ((Prelude.succ) 0) ((Prelude.succ) 0) acc) of { (,) blocks' assn -> (,) blocks' (assnAcc assn)}
LinearScan/Blocks.hs view
@@ -1,6 +1,3 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}-{- For Hugs, use the option -F"cpp -P -traditional" -}- module LinearScan.Blocks where @@ -13,97 +10,22 @@ import qualified Data.Functor.Identity import qualified LinearScan.Utils -import qualified LinearScan.Eqtype as Eqtype-import qualified LinearScan.Ssrbool as Ssrbool-+import qualified LinearScan.UsePos as UsePos ---unsafeCoerce :: a -> b-#ifdef __GLASGOW_HASKELL__-import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#-#else--- HUGS-import qualified LinearScan.IOExts as IOExts-unsafeCoerce = IOExts.unsafeCoerce-#endif- type PhysReg = Prelude.Int -data VarKind =- Input- | Temp- | Output--eqVarKind :: VarKind -> VarKind -> Prelude.Bool-eqVarKind s1 s2 =- case s1 of {- Input ->- case s2 of {- Input -> Prelude.True;- _ -> Prelude.False};- Temp ->- case s2 of {- Temp -> Prelude.True;- _ -> Prelude.False};- Output ->- case s2 of {- Output -> Prelude.True;- _ -> Prelude.False}}--eqVarKindP :: Eqtype.Equality__Coq_axiom VarKind-eqVarKindP b1 b2 =- let {- _evar_0_ = let {_evar_0_ = Ssrbool.ReflectT} in- let {_evar_0_0 = Ssrbool.ReflectF} in- let {_evar_0_1 = Ssrbool.ReflectF} in- case b2 of {- Input -> _evar_0_;- Temp -> _evar_0_0;- Output -> _evar_0_1}}- in- let {- _evar_0_0 = let {_evar_0_0 = Ssrbool.ReflectF} in- let {_evar_0_1 = Ssrbool.ReflectT} in- let {_evar_0_2 = Ssrbool.ReflectF} in- case b2 of {- Input -> _evar_0_0;- Temp -> _evar_0_1;- Output -> _evar_0_2}}- in- let {- _evar_0_1 = let {_evar_0_1 = Ssrbool.ReflectF} in- let {_evar_0_2 = Ssrbool.ReflectF} in- let {_evar_0_3 = Ssrbool.ReflectT} in- case b2 of {- Input -> _evar_0_1;- Temp -> _evar_0_2;- Output -> _evar_0_3}}- in- case b1 of {- Input -> _evar_0_;- Temp -> _evar_0_0;- Output -> _evar_0_1}--coq_VarKind_eqMixin :: Eqtype.Equality__Coq_mixin_of VarKind-coq_VarKind_eqMixin =- Eqtype.Equality__Mixin eqVarKind eqVarKindP--coq_VarKind_eqType :: Eqtype.Equality__Coq_type-coq_VarKind_eqType =- unsafeCoerce coq_VarKind_eqMixin- type VarId = Prelude.Int data VarInfo =- Build_VarInfo (Prelude.Either PhysReg VarId) VarKind Prelude.Bool+ Build_VarInfo (Prelude.Either PhysReg VarId) UsePos.VarKind Prelude.Bool varId :: Prelude.Int -> VarInfo -> Prelude.Either PhysReg VarId varId maxReg v = case v of { Build_VarInfo varId0 varKind0 regRequired0 -> varId0} -varKind :: Prelude.Int -> VarInfo -> VarKind+varKind :: Prelude.Int -> VarInfo -> UsePos.VarKind varKind maxReg v = case v of { Build_VarInfo varId0 varKind0 regRequired0 -> varKind0}@@ -123,9 +45,9 @@ IsNormal | IsCall | IsBranch- | IsLoopBegin- | IsLoopEnd +type OpId = Prelude.Int+ data OpInfo accType opType1 opType2 = Build_OpInfo (opType1 -> OpKind) (opType1 -> [] VarInfo) (PhysReg -> PhysReg ->@@ -139,47 +61,55 @@ ([] opType2) accType) ((Prelude.Maybe VarId) -> PhysReg -> accType -> (,) ([] opType2) accType) - (opType1 -> ([] ((,) VarId PhysReg)) -> [] opType2)+ (opType1 -> ([] ((,) VarId PhysReg)) -> [] opType2) (opType1 ->+ Prelude.String) opKind :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> OpKind opKind maxReg o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0- applyAllocs0 -> opKind0}+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0+ applyAllocs0 showOp -> opKind0} opRefs :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> [] VarInfo opRefs maxReg o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0- applyAllocs0 -> opRefs0}+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0+ applyAllocs0 showOp -> opRefs0} moveOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> PhysReg -> a1 -> (,) ([] a3) a1 moveOp maxReg o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0- applyAllocs0 -> moveOp0}+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0+ applyAllocs0 showOp -> moveOp0} +swapOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> PhysReg -> a1 -> (,)+ ([] a3) a1+swapOp maxReg o =+ case o of {+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0+ applyAllocs0 showOp -> swapOp0}+ saveOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> (Prelude.Maybe VarId) -> a1 -> (,) ([] a3) a1 saveOp maxReg o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0- applyAllocs0 -> saveOp0}+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0+ applyAllocs0 showOp -> saveOp0} restoreOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> (Prelude.Maybe VarId) -> PhysReg -> a1 -> (,) ([] a3) a1 restoreOp maxReg o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0- applyAllocs0 -> restoreOp0}+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0+ applyAllocs0 showOp -> restoreOp0} applyAllocs :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> ([] ((,) VarId PhysReg)) -> [] a3 applyAllocs maxReg o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0- applyAllocs0 -> applyAllocs0}+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0+ applyAllocs0 showOp -> applyAllocs0} type BlockId = Prelude.Int @@ -230,8 +160,6 @@ blockSize :: (BlockInfo a1 a2 a3 a4) -> a1 -> Prelude.Int blockSize binfo block = Data.List.length (allBlockOps binfo block)--type OpId = Prelude.Int foldOps :: (BlockInfo a1 a2 a3 a4) -> (a5 -> a3 -> a5) -> a5 -> ([] a1) -> a5 foldOps binfo f z =
LinearScan/Build.hs view
@@ -19,10 +19,13 @@ import qualified LinearScan.Interval as Interval import qualified LinearScan.Lib as Lib import qualified LinearScan.LiveSets as LiveSets+import qualified LinearScan.Logic as Logic+import qualified LinearScan.Loops as Loops import qualified LinearScan.Morph as Morph import qualified LinearScan.NonEmpty0 as NonEmpty0 import qualified LinearScan.Range as Range import qualified LinearScan.ScanState as ScanState+import qualified LinearScan.Specif as Specif import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype@@ -52,206 +55,319 @@ newBuildState n = IntMap.emptyIntMap -data RangeCursor =- Build_RangeCursor Prelude.Int Range.BoundedRange Range.SortedRanges--emptyRangeCursor :: Prelude.Int -> Prelude.Int -> Prelude.Int -> RangeCursor-emptyRangeCursor b pos e =- (Prelude.flip (Prelude.$)) __ (\_ -> Build_RangeCursor pos- (Range.emptyBoundedRange ((Prelude.succ) (Ssrnat.double b))- ((Prelude.succ) (Ssrnat.double pos)))- (Range.emptySortedRanges ((Prelude.succ) (Ssrnat.double pos))))--transportRangeCursor :: Prelude.Int -> Prelude.Int -> Prelude.Int ->- Prelude.Int -> RangeCursor -> RangeCursor-transportRangeCursor b prev base e c =- let {_evar_0_ = \mid r rs -> Build_RangeCursor mid r rs} in- case c of {- Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}--type PendingRanges = (IntMap.IntMap RangeCursor)+type PendingRanges = [] Range.BoundedRange emptyPendingRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->- Prelude.Int -> IntMap.IntSet -> PendingRanges-emptyPendingRanges maxReg b pos e liveOuts =- (Prelude.flip (Prelude.$)) (emptyRangeCursor b pos e) (\empty ->- (Prelude.flip (Prelude.$)) (\xs vid ->- IntMap.coq_IntMap_insert ((Prelude.+) vid maxReg) empty xs) (\f ->- IntMap.coq_IntSet_foldl f IntMap.emptyIntMap liveOuts))+ IntMap.IntSet -> IntMap.IntMap PendingRanges+emptyPendingRanges maxReg b e liveOuts =+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$))+ (Range.emptyBoundedRange ((Prelude.succ) (Ssrnat.double b))+ ((Prelude.succ) (Ssrnat.double e))) (\empty ->+ (Prelude.flip (Prelude.$)) (\xs vid ->+ IntMap.coq_IntMap_insert ((Prelude.+) vid maxReg) ((:[]) empty) xs)+ (\f -> IntMap.coq_IntSet_foldl f IntMap.emptyIntMap liveOuts))) -mergeIntoSortedRanges :: Prelude.Int -> Prelude.Int -> PendingRanges ->- (IntMap.IntMap Range.SortedRanges) -> IntMap.IntMap- Range.SortedRanges-mergeIntoSortedRanges b pos pmap rmap =- IntMap.coq_IntMap_mergeWithKey (\_the_1st_wildcard_ _top_assumption_ ->- let {- _evar_0_ = \mid br ps rs ->+coq_BoundedRange_leq :: Prelude.Int -> Prelude.Int -> Range.BoundedRange ->+ Range.BoundedRange -> Prelude.Bool+coq_BoundedRange_leq b e x y =+ let {_evar_0_ = (Prelude.<=) (Range.rbeg x) (Range.rbeg y)} in+ let {_evar_0_0 = (Prelude.<=) (Range.rend x) (Range.rend y)} in+ case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Range.rend x))+ (unsafeCoerce (Range.rend y)) of {+ Prelude.True -> _evar_0_;+ Prelude.False -> _evar_0_0}++compilePendingRanges :: Prelude.Int -> Prelude.Int -> ([] Range.BoundedRange)+ -> Specif.Coq_sig2 Range.SortedRanges+compilePendingRanges b e ranges =+ let {_evar_0_ = \_ -> []} in+ let {+ _evar_0_0 = \r1 rs iHrs ->+ case rs of {+ [] -> (:) ( r1) [];+ (:) r2 rs2 -> (Prelude.flip (Prelude.$)) __ (\_ ->+ let {iHrs0 = iHrs __} in+ let {_evar_0_0 = \_ _ _ _ _ -> Logic.coq_False_rec} in let {- ps' = Range.prependRange ((Prelude.succ) (Ssrnat.double b))- ((Prelude.succ) (Ssrnat.double mid)) br ps ((Prelude.succ)- (Ssrnat.double b))}+ _evar_0_1 = \r2' rs2' ->+ let {_evar_0_1 = \_ -> (:) ( r1) ((:) r2' rs2')} in+ let {+ _evar_0_2 = \_ -> (:)+ (Range.packRange (Range.Build_RangeDesc+ (Prelude.min (Range.rbeg (Range.getRangeDesc r1))+ (Range.rbeg (Range.getRangeDesc r2')))+ (Prelude.max (Range.rend (Range.getRangeDesc r1))+ (Range.rend (Range.getRangeDesc r2')))+ (Lib.sortBy UsePos.upos_le+ ((Prelude.++) (Range.ups (Range.getRangeDesc r1))+ (Range.ups (Range.getRangeDesc r2')))))) rs2'}+ in+ case Range.range_ltn ( r1) r2' of {+ Prelude.True -> _evar_0_1 __;+ Prelude.False -> _evar_0_2 __}} in- Prelude.Just- (Range.coq_SortedRanges_cat ((Prelude.succ) (Ssrnat.double b)) ps'- ((Prelude.succ) (Ssrnat.double pos)) rs))}- in- (\rs ->- case _top_assumption_ of {- Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1 rs}))- (IntMap.coq_IntMap_map (\_top_assumption_ ->- let {- _evar_0_ = \_cursorMid_ br rs ->- (Prelude.flip (Prelude.$)) __ (\_ ->- - (Range.prependRange ((Prelude.succ) (Ssrnat.double b))- ((Prelude.succ) (Ssrnat.double _cursorMid_)) br rs- ((Prelude.succ) (Ssrnat.double b))))}- in- case _top_assumption_ of {- Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}))- (IntMap.coq_IntMap_map- (Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b))- ((Prelude.succ) (Ssrnat.double pos)))) ( pmap) rmap+ case iHrs0 of {+ [] -> _evar_0_0 __ __ __ __ __;+ (:) x x0 -> _evar_0_1 x x0})}}+ in+ Datatypes.list_rec _evar_0_ (\r1 rs iHrs _ -> _evar_0_0 r1 rs iHrs) ranges+ __ -varKindLtn :: Blocks.VarKind -> Blocks.VarKind -> Prelude.Bool-varKindLtn x y =- case x of {- Blocks.Input ->- case y of {- Blocks.Input -> Prelude.False;- _ -> Prelude.True};- Blocks.Temp ->- case y of {- Blocks.Output -> Prelude.True;- _ -> Prelude.False};- Blocks.Output -> Prelude.False}+rangesToBoundedRanges :: Prelude.Int -> Prelude.Int -> Range.RangeDesc -> ([]+ Range.RangeDesc) -> [] Range.BoundedRange+rangesToBoundedRanges b e y ys =+ case ys of {+ [] -> (:[]) ( y);+ (:) z zs -> (:) ( y) (rangesToBoundedRanges b e z zs)} -handleVars_combine :: Prelude.Int -> Prelude.Int -> Prelude.Int ->- Prelude.Int -> RangeCursor -> ((,) Prelude.Bool- ([] Blocks.VarKind)) -> Prelude.Maybe RangeCursor-handleVars_combine b pos e vid range vars =+compressPendingRanges :: Prelude.Int -> Prelude.Int -> PendingRanges ->+ PendingRanges+compressPendingRanges b e ranges =+ let {_evar_0_ = \r -> (:[]) r} in let {- _evar_0_ = \mid br srs ->+ _evar_0_0 = \r rs -> let {- _evar_0_ = \req kinds ->+ _evar_0_0 = \_ -> let {- upos = UsePos.Build_UsePos ((Prelude.succ) (Ssrnat.double pos)) req}+ _top_assumption_ = compilePendingRanges b e+ (Lib.insert (coq_BoundedRange_leq b e) r+ (Lib.sortBy (coq_BoundedRange_leq b e) ( rs)))} in- (Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ _evar_0_0 = \_ _ -> (Prelude.flip (Prelude.$)) __ (\_ ->- (Prelude.flip (Prelude.$)) __ (\_ ->- let {- _evar_0_ = \_ ->- (Prelude.flip (Prelude.$)) __ (\_ ->- let {- r2 = Range.coq_Range_cons upos (Range.Build_RangeDesc- ((Prelude.succ) (Ssrnat.double pos))- (Range.rend ( br)) (Range.ups ( br)))}- in- Prelude.Just (Build_RangeCursor mid r2 srs))}- in- let {- _evar_0_0 = \_ ->- let {- _evar_0_0 = \_ ->- (Prelude.flip (Prelude.$)) __ (\_ ->- let {r1 = Range.coq_Range_cons upos ( ( br))} in- Prelude.Just (Build_RangeCursor mid r1 srs))}- in- let {- _evar_0_1 = \_ ->- let {r1 = Range.newRange upos} in- let {- _evar_0_1 = \_ ->- (Prelude.flip (Prelude.$)) __ (\_ -> Prelude.Just- (Build_RangeCursor ((Prelude.succ) pos) r1- (- (Range.prependRange ((Prelude.succ) (Ssrnat.double b))- ((Prelude.succ) (Ssrnat.double mid)) br srs- ((Prelude.succ)- (Ssrnat.double ((Prelude.succ) pos)))))))}- in- _evar_0_1 __}- in- case (Prelude.<=) (Range.rbeg ( ( br))) (UsePos.uloc upos) of {- Prelude.True -> _evar_0_0 __;- Prelude.False -> _evar_0_1 __}}- in- case (Prelude.&&)- (Ssrbool.in_mem (unsafeCoerce Blocks.Output)- (Ssrbool.mem- (Seq.seq_predType Blocks.coq_VarKind_eqType) kinds))- (Prelude.not- (Ssrbool.in_mem (unsafeCoerce Blocks.Input)- (Ssrbool.mem- (Seq.seq_predType Blocks.coq_VarKind_eqType) kinds))) of {- Prelude.True -> _evar_0_ __;- Prelude.False -> _evar_0_0 __})))}+ let {_evar_0_0 = \_ -> rs} in _evar_0_0 __)}+ in+ let {+ _evar_0_1 = \x xs ->+ case _top_assumption_ of {+ [] -> Logic.coq_False_rec;+ (:) y ys -> rangesToBoundedRanges b e y ys}}+ in+ case Lib.insert (coq_BoundedRange_leq b e) r+ (Lib.sortBy (coq_BoundedRange_leq b e) ( rs)) of {+ [] -> _evar_0_0 __ __;+ (:) x x0 -> _evar_0_1 x x0}} in- case vars of {- (,) x x0 -> unsafeCoerce _evar_0_ x x0}}+ _evar_0_0 __} in+ (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+ (\x ->+ _evar_0_ x)+ (\x x0 ->+ _evar_0_0 x x0)+ ranges++mergeIntoSortedRanges :: Prelude.Int -> Prelude.Int -> (IntMap.IntMap+ PendingRanges) -> (IntMap.IntMap Range.SortedRanges)+ -> IntMap.IntMap Range.SortedRanges+mergeIntoSortedRanges b e pmap rmap =+ IntMap.coq_IntMap_mergeWithKey (\_the_1st_wildcard_ brs srs2 ->+ let {+ _top_assumption_ = compilePendingRanges b e+ (Lib.sortBy (coq_BoundedRange_leq b e) ( brs))}+ in+ Prelude.Just+ (Range.coq_SortedRanges_cat ((Prelude.succ) (Ssrnat.double b))+ _top_assumption_ ((Prelude.succ) (Ssrnat.double e)) srs2))+ (IntMap.coq_IntMap_map (\brs ->+ compilePendingRanges b e (Lib.sortBy (coq_BoundedRange_leq b e) ( brs))))+ (\sr ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ IntMap.coq_IntMap_map+ (Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b))+ ((Prelude.succ) (Ssrnat.double e))) sr)) pmap rmap++upos_before_rend :: Range.RangeDesc -> UsePos.UsePos -> Prelude.Bool+upos_before_rend rd upos =+ case Range.ups rd of {+ [] ->+ case UsePos.uvar upos of {+ UsePos.Input -> (Prelude.<=) (UsePos.uloc upos) (Range.rend rd);+ _ -> (Prelude.<=) ((Prelude.succ) (UsePos.uloc upos)) (Range.rend rd)};+ (:) u l ->+ case (Prelude.&&)+ (Prelude.not+ (Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (UsePos.uvar upos)) (unsafeCoerce UsePos.Input)))+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (UsePos.uloc u))+ (unsafeCoerce (Range.rend rd))) of {+ Prelude.True ->+ (Prelude.<=) ((Prelude.succ) (UsePos.uloc upos)) (UsePos.uloc u);+ Prelude.False -> (Prelude.<=) (UsePos.uloc upos) (UsePos.uloc u)}}++makeNewRange :: Prelude.Int -> Prelude.Int -> Prelude.Int -> UsePos.UsePos ->+ Range.BoundedRange+makeNewRange b pos e upos =+ Range.Build_RangeDesc+ (case UsePos.uvar upos of {+ UsePos.Input -> (Prelude.succ) (Ssrnat.double b);+ _ -> (Prelude.succ) (Ssrnat.double pos)})+ (case UsePos.uvar upos of {+ UsePos.Input -> (Prelude.succ) (Ssrnat.double pos);+ UsePos.Temp -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos));+ UsePos.Output -> (Prelude.succ) (Ssrnat.double e)}) ((:) upos [])++makeUsePos :: Prelude.Int -> Prelude.Int -> Blocks.VarInfo -> Specif.Coq_sig2+ UsePos.UsePos+makeUsePos maxReg pos var =+ let {+ upos = UsePos.Build_UsePos ((Prelude.succ) (Ssrnat.double pos))+ (Blocks.regRequired maxReg var) (Blocks.varKind maxReg var)}+ in+ (Prelude.flip (Prelude.$)) __ (\_ -> upos)++handleOutputVar :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int+ -> (Prelude.Maybe PendingRanges) -> Blocks.VarInfo ->+ Prelude.Maybe PendingRanges+handleOutputVar maxReg b pos e range var =+ let {_top_assumption_ = makeUsePos maxReg pos var} in+ let {+ _evar_0_ = \range0 ->+ (Prelude.flip (Prelude.$))+ (let {_top_assumption_0 = Prelude.head range0} in+ let {+ _evar_0_ = \_ ->+ let {+ r1 = Range.coq_Range_shift ( _top_assumption_0)+ (UsePos.uloc _top_assumption_)}+ in+ (Prelude.flip (Prelude.$)) __ (\_ -> r1)}+ in+ let {+ _evar_0_0 = \_ ->+ let {_evar_0_0 = \_ -> _top_assumption_0} in _evar_0_0 __}+ in+ case (Prelude.<=) ((Prelude.succ) (UsePos.uloc _top_assumption_))+ (Range.head_or_end ( _top_assumption_0)) of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}) (\res ->+ let {+ _evar_0_ = \_ ->+ (Prelude.flip (Prelude.$))+ (Range.coq_Range_cons _top_assumption_ ( res)) (\br ->+ let {_evar_0_ = \_the_1st_wildcard_ -> Prelude.Just ((:[]) br)} in+ let {+ _evar_0_0 = \_the_2nd_wildcard_ rs -> Prelude.Just+ (NonEmpty0.coq_NE_from_list br ( rs))}+ in+ (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+ (\x ->+ _evar_0_ x)+ (\x x0 ->+ _evar_0_0 x x0)+ range0)}+ in+ let {+ _evar_0_0 = \_ -> Prelude.Just+ (NonEmpty0.coq_NE_from_list (makeNewRange b pos e _top_assumption_)+ ( range0))}+ in+ case upos_before_rend ( res) _top_assumption_ of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __})}+ in+ let {+ _evar_0_0 = Prelude.Just ((:[]) (makeNewRange b pos e _top_assumption_))}+ in case range of {- Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}+ Prelude.Just x -> _evar_0_ x;+ Prelude.Nothing -> _evar_0_0} +handleVar :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int ->+ (Prelude.Maybe PendingRanges) -> Blocks.VarInfo -> Prelude.Maybe+ PendingRanges+handleVar maxReg b pos e range var =+ let {_top_assumption_ = makeUsePos maxReg pos var} in+ let {+ _evar_0_ = \range0 -> Prelude.Just+ (NonEmpty0.coq_NE_from_list (makeNewRange b pos e _top_assumption_)+ ( range0))}+ in+ let {+ _evar_0_0 = Prelude.Just ((:[]) (makeNewRange b pos e _top_assumption_))}+ in+ case range of {+ Prelude.Just x -> _evar_0_ x;+ Prelude.Nothing -> _evar_0_0}++handleVars_combine :: Prelude.Int -> Prelude.Int -> Prelude.Int ->+ Prelude.Int -> Prelude.Int -> ([] Blocks.VarInfo) ->+ PendingRanges -> Prelude.Maybe PendingRanges+handleVars_combine maxReg b pos e vid vars c1 =+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$)) (compressPendingRanges b e c1) (\c2 ->+ (Prelude.flip (Prelude.$))+ (Data.List.foldl' (handleOutputVar maxReg b pos e) (Prelude.Just c2)+ (Prelude.filter (\k ->+ Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (Blocks.varKind maxReg k))+ (unsafeCoerce UsePos.Output)) vars)) (\c3 ->+ (Prelude.flip (Prelude.$))+ (Data.List.foldl' (handleVar maxReg b pos e) c3+ (Prelude.filter (\k ->+ Prelude.not+ (Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (Blocks.varKind maxReg k))+ (unsafeCoerce UsePos.Output))) vars)) (\c4 -> c4))))+ handleVars_onlyRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->- (IntMap.IntMap RangeCursor) -> IntMap.IntMap- RangeCursor-handleVars_onlyRanges b pos e =- IntMap.coq_IntMap_map (transportRangeCursor b ((Prelude.succ) pos) pos e)+ (IntMap.IntMap PendingRanges) -> IntMap.IntMap+ PendingRanges+handleVars_onlyRanges b pos e h0 =+ h0 handleVars_onlyVars :: Prelude.Int -> Prelude.Int -> Prelude.Int ->- (IntMap.IntMap ((,) Prelude.Bool ([] Blocks.VarKind)))- -> IntMap.IntMap RangeCursor-handleVars_onlyVars b pos e =- IntMap.coq_IntMap_map (\_top_assumption_ ->- let {- _evar_0_ = \req kinds ->- let {- rd = Range.Build_RangeDesc- (case Ssrbool.in_mem (unsafeCoerce Blocks.Input)- (Ssrbool.mem (Seq.seq_predType Blocks.coq_VarKind_eqType)- kinds) of {- Prelude.True -> (Prelude.succ) (Ssrnat.double b);- Prelude.False -> (Prelude.succ) (Ssrnat.double pos)})- (case Ssrbool.in_mem (unsafeCoerce Blocks.Output)- (Ssrbool.mem (Seq.seq_predType Blocks.coq_VarKind_eqType)- kinds) of {- Prelude.True -> (Prelude.succ) (Ssrnat.double e);- Prelude.False -> (Prelude.succ) ((Prelude.succ)- (Ssrnat.double pos))}) ((:) (UsePos.Build_UsePos ((Prelude.succ)- (Ssrnat.double pos)) req) [])}- in- Build_RangeCursor e rd []}- in- case _top_assumption_ of {- (,) x x0 -> unsafeCoerce _evar_0_ x x0})+ Prelude.Int -> (IntMap.IntMap ([] Blocks.VarInfo)) ->+ IntMap.IntMap PendingRanges+handleVars_onlyVars maxReg b pos e =+ IntMap.coq_IntMap_foldlWithKey (\m vid vars ->+ (Prelude.flip (Prelude.$))+ (Data.List.foldl' (handleOutputVar maxReg b pos e) Prelude.Nothing+ (Prelude.filter (\k ->+ Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (Blocks.varKind maxReg k))+ (unsafeCoerce UsePos.Output)) vars)) (\c2 ->+ (Prelude.flip (Prelude.$))+ (Data.List.foldl' (handleVar maxReg b pos e) c2+ (Prelude.filter (\k ->+ Prelude.not+ (Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (Blocks.varKind maxReg k))+ (unsafeCoerce UsePos.Output))) vars)) (\c3 ->+ let {_evar_0_ = \c4 -> IntMap.coq_IntMap_insert vid c4 m} in+ case c3 of {+ Prelude.Just x -> _evar_0_ x;+ Prelude.Nothing -> m}))) IntMap.emptyIntMap -extractVarInfo :: Prelude.Int -> ([] Blocks.VarInfo) -> (,) Prelude.Bool- ([] Blocks.VarKind)+extractVarInfo :: Prelude.Int -> ([] Blocks.VarInfo) -> [] Blocks.VarInfo extractVarInfo maxReg xs =- (,)- (Prelude.not- (Eqtype.eq_op Ssrnat.nat_eqType- (unsafeCoerce (Seq.find (Blocks.regRequired maxReg) xs))- (unsafeCoerce (Data.List.length xs))))- (Lib.sortBy varKindLtn (Prelude.map (\v -> Blocks.varKind maxReg v) xs))+ let {_evar_0_ = \x -> (:) x []} in+ let {_evar_0_0 = \x xs0 -> (:) x ( xs0)} in+ (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+ (\x ->+ _evar_0_ x)+ (\x x0 ->+ _evar_0_0 x x0)+ xs handleVars :: Prelude.Int -> ([] Blocks.VarInfo) -> Prelude.Int ->- Prelude.Int -> Prelude.Int -> PendingRanges -> PendingRanges+ Prelude.Int -> Prelude.Int -> (IntMap.IntMap PendingRanges) ->+ IntMap.IntMap PendingRanges handleVars maxReg varRefs b pos e ranges = let { vars = IntMap.coq_IntMap_map (extractVarInfo maxReg) (IntMap.coq_IntMap_groupOn (Blocks.nat_of_varId maxReg) varRefs)} in- IntMap.coq_IntMap_mergeWithKey (handleVars_combine b pos e)- (handleVars_onlyRanges b pos e) (handleVars_onlyVars b pos e) ( ranges)- vars+ IntMap.coq_IntMap_mergeWithKey (handleVars_combine maxReg b pos e)+ (handleVars_onlyVars maxReg b pos e) (handleVars_onlyRanges b pos e) vars+ ranges reduceOp :: Prelude.Int -> (Blocks.OpInfo a4 a2 a3) -> Prelude.Int ->- Prelude.Int -> Prelude.Int -> a1 -> a2 -> PendingRanges ->- PendingRanges+ Prelude.Int -> Prelude.Int -> a1 -> a2 -> (IntMap.IntMap+ PendingRanges) -> IntMap.IntMap PendingRanges reduceOp maxReg oinfo b pos e block op ranges = let {refs = Blocks.opRefs maxReg oinfo op} in let {@@ -260,7 +376,7 @@ (Prelude.++) (Fintype.image_mem (Fintype.ordinal_finType maxReg) (\n -> Blocks.Build_VarInfo (Prelude.Left (unsafeCoerce n))- Blocks.Temp Prelude.True)+ UsePos.Temp Prelude.True) (Ssrbool.mem (Seq.seq_predType (Fintype.ordinal_eqType maxReg)) (unsafeCoerce (Fintype.ord_enum maxReg)))) refs;@@ -269,33 +385,31 @@ handleVars maxReg refs' b pos e ranges reduceBlock :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- (Blocks.OpInfo a5 a3 a4) -> Prelude.Int -> a1 -> PendingRanges- -> PendingRanges-reduceBlock maxReg binfo oinfo pos block =+ (Blocks.OpInfo a5 a3 a4) -> Prelude.Int -> Blocks.BlockId ->+ a1 -> Loops.LoopState -> (IntMap.IntMap IntMap.IntSet) ->+ (IntMap.IntMap PendingRanges) -> IntMap.IntMap PendingRanges+reduceBlock maxReg binfo oinfo pos bid block loops varUses = let {sz = Blocks.blockSize binfo block} in let {e = (Prelude.+) pos sz} in let {ops = Blocks.allBlockOps binfo block} in- let {- _evar_0_ = let {_evar_0_ = let {_evar_0_ = \h -> h} in _evar_0_} in- let {- _evar_0_0 = \o os iHos ->- let {- _evar_0_0 = \ranges ->- iHos- (reduceOp maxReg oinfo pos- ((Prelude.+) pos (Data.List.length os)) e block o- ranges)}- in- _evar_0_0}- in- Datatypes.list_rec _evar_0_ _evar_0_0 (Seq.rev ops)}- in- _evar_0_+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {_evar_0_ = \h0 -> h0} in+ let {+ _evar_0_0 = \os o iHos ranges ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$)) __ iHos+ (reduceOp maxReg oinfo pos+ ((Prelude.+) pos (Data.List.length os)) e block o ranges))}+ in+ Seq.last_ind (\_ h0 -> _evar_0_ h0) (\os o iHos _ ranges ->+ _evar_0_0 os o iHos ranges) ops __)) reduceBlocks :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (IntMap.IntMap+ (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> Loops.LoopState ->+ (IntMap.IntMap IntMap.IntSet) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Int -> BuildState-reduceBlocks maxReg binfo oinfo blocks liveSets pos =+reduceBlocks maxReg binfo oinfo blocks loops varUses liveSets pos = let {_evar_0_ = \pos0 -> newBuildState pos0} in let { _evar_0_0 = \b blocks0 iHbs pos0 ->@@ -307,14 +421,13 @@ let {sz = Blocks.blockSize binfo b} in let { _evar_0_0 = \_ ->- let {endpos = (Prelude.+) pos0 sz} in (Prelude.flip (Prelude.$)) __ (\_ ->- (Prelude.flip (Prelude.$)) __ (\_ ->- (Prelude.flip (Prelude.$))- (reduceBlock maxReg binfo oinfo pos0 b- (emptyPendingRanges maxReg pos0 endpos endpos outs))- (\pending ->- mergeIntoSortedRanges pos0 endpos pending (iHbs endpos))))}+ (Prelude.flip (Prelude.$))+ (reduceBlock maxReg binfo oinfo pos0 bid b loops varUses+ (emptyPendingRanges maxReg pos0 ((Prelude.+) pos0 sz) outs))+ (\pending ->+ mergeIntoSortedRanges pos0 ((Prelude.+) pos0 sz) pending+ (iHbs ((Prelude.+) pos0 sz))))} in let {_evar_0_1 = \_ -> iHbs pos0} in case (Prelude.<=) ((Prelude.succ) 0) sz of {@@ -341,7 +454,7 @@ ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_)))) (Range.rend ( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))- Interval.Whole (NonEmpty0.coq_NE_from_list _a_ _l_))))) vars}+ (NonEmpty0.coq_NE_from_list _a_ _l_))))) vars} in let { _evar_0_1 = \_ ->@@ -353,7 +466,7 @@ ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_)))) (Range.rend ( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))- Interval.Whole (NonEmpty0.coq_NE_from_list _a_ _l_))) vars))}+ (NonEmpty0.coq_NE_from_list _a_ _l_))) vars))} in case (Prelude.<=) ((Prelude.succ) vid) maxReg of { Prelude.True -> _evar_0_0 __;@@ -368,12 +481,12 @@ (Data.List.replicate maxReg Prelude.Nothing) IntMap.emptyIntMap) bs buildIntervals :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (IntMap.IntMap- LiveSets.BlockLiveSets) -> Prelude.Either Morph.SSError- ScanState.ScanStateSig-buildIntervals maxReg binfo oinfo blocks liveSets =+ (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> Loops.LoopState ->+ (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Either+ Morph.SSError ScanState.ScanStateSig+buildIntervals maxReg binfo oinfo blocks loops liveSets = let {- handleVar = \ss i ->+ add_unhandled_interval = \ss i -> ScanState.packScanState maxReg ScanState.Pending (ScanState.Build_ScanStateDesc ((Prelude.succ) (ScanState.nextInterval maxReg ( ss)))@@ -393,8 +506,14 @@ (ScanState.Build_ScanStateDesc 0 [] (Data.List.replicate maxReg Prelude.Nothing) [] [] [] [])); (:) b bs ->- let {bs0 = reduceBlocks maxReg binfo oinfo ((:) b bs) liveSets 0} in- case compileIntervals maxReg 0 bs0 of {+ let {+ varUses = Loops.computeVarReferences maxReg binfo oinfo ((:) b bs) loops}+ in+ let {+ reduced = reduceBlocks maxReg binfo oinfo ((:) b bs) loops varUses+ liveSets 0}+ in+ case compileIntervals maxReg 0 reduced of { (,) regs vars -> let { s2 = ScanState.packScanState maxReg ScanState.Pending@@ -413,6 +532,6 @@ (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0 [] (Data.List.replicate maxReg Prelude.Nothing) [] [] [] [])))} in- let {s3 = IntMap.coq_IntMap_foldl handleVar s2 vars} in+ let {s3 = IntMap.coq_IntMap_foldl add_unhandled_interval s2 vars} in Prelude.Right (ScanState.packScanState maxReg ScanState.InUse ( s3))}}
LinearScan/Eqtype.hs view
@@ -119,11 +119,6 @@ s2val u = u -sig_subType :: (Ssrbool.Coq_pred a1) -> Coq_subType a1-sig_subType p =- SubType (unsafeCoerce ) (unsafeCoerce (\x _ -> x)) (\_ k_S u ->- k_S (unsafeCoerce u) __)- inj_eqAxiom :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) -> Equality__Coq_axiom a1 inj_eqAxiom eT f x y =@@ -145,17 +140,6 @@ (Coq_sub_sort Equality__Coq_sort) val_eqP t p sT = inj_eqAxiom t (val p sT)--sig_eqMixin :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->- Equality__Coq_mixin_of Equality__Coq_sort-sig_eqMixin t p =- Equality__Mixin (\x y -> eq_op t ( x) ( y))- (unsafeCoerce (val_eqP t (\x -> p x) (sig_subType p)))--sig_eqType :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->- Equality__Coq_type-sig_eqType t p =- unsafeCoerce (sig_eqMixin t p) pair_eq :: Equality__Coq_type -> Equality__Coq_type -> Ssrbool.Coq_simpl_rel ((,) Equality__Coq_sort Equality__Coq_sort)
LinearScan/IntMap.hs view
@@ -42,6 +42,14 @@ emptyIntMap = [] +coq_IntMap_fromList :: ([] ((,) Prelude.Int a1)) -> IntMap a1+coq_IntMap_fromList x =+ x++coq_IntMap_size :: (IntMap a1) -> Prelude.Int+coq_IntMap_size m =+ Data.List.length m+ coq_IntMap_lookup :: Prelude.Int -> (IntMap a1) -> Prelude.Maybe a1 coq_IntMap_lookup k m = Lib.maybeLookup Ssrnat.nat_eqType (unsafeCoerce m) (unsafeCoerce k)@@ -91,6 +99,10 @@ coq_IntMap_foldlWithKey f z m = Data.List.foldl' (\acc x -> f acc (Prelude.fst x) (Prelude.snd x)) z m +coq_IntMap_toList :: (IntMap a1) -> [] ((,) Prelude.Int a1)+coq_IntMap_toList m =+ m+ eqIntMap :: Eqtype.Equality__Coq_type -> (IntMap Eqtype.Equality__Coq_sort) -> (IntMap Eqtype.Equality__Coq_sort) -> Prelude.Bool eqIntMap a s1 s2 =@@ -134,11 +146,19 @@ emptyIntSet = [] +coq_IntSet_singleton :: Prelude.Int -> IntSet+coq_IntSet_singleton x =+ (:) x []+ coq_IntSet_member :: Prelude.Int -> IntSet -> Prelude.Bool coq_IntSet_member k m = Ssrbool.in_mem (unsafeCoerce k) (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m)) +coq_IntSet_size :: IntSet -> Prelude.Int+coq_IntSet_size m =+ Data.List.length m+ coq_IntSet_insert :: Prelude.Int -> IntSet -> IntSet coq_IntSet_insert k m = case Ssrbool.in_mem (unsafeCoerce k)@@ -146,6 +166,10 @@ Prelude.True -> m; Prelude.False -> (:) k m} +coq_IntSet_delete :: Prelude.Int -> IntSet -> IntSet+coq_IntSet_delete k m =+ unsafeCoerce (Seq.rem Ssrnat.nat_eqType (unsafeCoerce k) (unsafeCoerce m))+ coq_IntSet_union :: IntSet -> IntSet -> IntSet coq_IntSet_union m1 m2 = unsafeCoerce@@ -168,6 +192,10 @@ coq_IntSet_forFold z m f = coq_IntSet_foldl f z m +coq_IntSet_toList :: IntSet -> [] Prelude.Int+coq_IntSet_toList m =+ m+ eqIntSet :: IntSet -> IntSet -> Prelude.Bool eqIntSet s1 s2 = Eqtype.eq_op (Seq.seq_eqType Ssrnat.nat_eqType) (unsafeCoerce s1)@@ -205,5 +233,5 @@ coq_IntMap_alter (\mxs -> case mxs of { Prelude.Just xs -> Prelude.Just ((:) x xs);- Prelude.Nothing -> Prelude.Just ((:) x [])}) n acc)+ Prelude.Nothing -> Prelude.Just ((:[]) x)}) n acc)
LinearScan/Interval.hs view
@@ -12,55 +12,40 @@ import qualified LinearScan.Lib as Lib import qualified LinearScan.Logic as Logic+import qualified LinearScan.NonEmpty0 as NonEmpty0 import qualified LinearScan.Range as Range+import qualified LinearScan.Specif as Specif import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrnat as Ssrnat __ :: any __ = Prelude.error "Logical or arity value used" -data IntervalKind =- Whole- | LeftMost- | Middle- | RightMost--splitKind :: IntervalKind -> (,) IntervalKind IntervalKind-splitKind k =- case k of {- Whole -> (,) LeftMost RightMost;- LeftMost -> (,) LeftMost Middle;- Middle -> (,) Middle Middle;- RightMost -> (,) Middle RightMost}- data IntervalDesc =- Build_IntervalDesc Prelude.Int Prelude.Int Prelude.Int IntervalKind - ([] Range.RangeDesc)+ Build_IntervalDesc Prelude.Int Prelude.Int Prelude.Int ([]+ Range.RangeDesc) ivar :: IntervalDesc -> Prelude.Int ivar i = case i of {- Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> ivar0}+ Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> ivar0} ibeg :: IntervalDesc -> Prelude.Int ibeg i = case i of {- Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> ibeg0}+ Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> ibeg0} iend :: IntervalDesc -> Prelude.Int iend i = case i of {- Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> iend0}--iknd :: IntervalDesc -> IntervalKind-iknd i =- case i of {- Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> iknd0}+ Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> iend0} rds :: IntervalDesc -> [] Range.RangeDesc rds i = case i of {- Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> rds0}+ Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> rds0} getIntervalDesc :: IntervalDesc -> IntervalDesc getIntervalDesc d =@@ -78,8 +63,8 @@ intervalEnd i = iend i -intervalCoversPos :: IntervalDesc -> Prelude.Int -> Prelude.Bool-intervalCoversPos d pos =+posWithinInterval :: IntervalDesc -> Prelude.Int -> Prelude.Bool+posWithinInterval d pos = (Prelude.&&) ((Prelude.<=) (intervalStart d) pos) ((Prelude.<=) ((Prelude.succ) pos) (intervalEnd d)) @@ -91,37 +76,53 @@ intervalIntersectionPoint :: IntervalDesc -> IntervalDesc -> Prelude.Maybe Lib.Coq_oddnum intervalIntersectionPoint i j =- Data.List.foldl' (\acc rd ->- case acc of {- Prelude.Just x -> Prelude.Just x;- Prelude.Nothing ->- Data.List.foldl' (\acc' rd' ->- case acc' of {- Prelude.Just x -> Prelude.Just x;- Prelude.Nothing -> Range.rangeIntersectionPoint ( rd) ( rd')})- Prelude.Nothing (rds j)}) Prelude.Nothing (rds i)+ Data.List.foldl' (\mx rd ->+ Lib.option_choose mx+ (Data.List.foldl' (\mx' rd' ->+ Lib.option_choose mx (Range.rangeIntersectionPoint ( rd) ( rd')))+ Prelude.Nothing (rds j))) Prelude.Nothing (rds i) searchInRange :: Range.RangeDesc -> (UsePos.UsePos -> Prelude.Bool) ->- Prelude.Maybe ((,) Range.RangeDesc UsePos.UsePos)+ Prelude.Maybe UsePos.UsePos searchInRange r f =- let {_evar_0_ = \x -> Prelude.Just ((,) r x)} in+ let {_evar_0_ = \x -> Prelude.Just x} in let {_evar_0_0 = Prelude.Nothing} in case Range.findRangeUsePos ( r) f of { Prelude.Just x -> _evar_0_ x; Prelude.Nothing -> _evar_0_0} findIntervalUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->- Prelude.Maybe ((,) Range.RangeDesc UsePos.UsePos)+ Prelude.Maybe+ ((,) Range.RangeDesc (Specif.Coq_sig2 UsePos.UsePos)) findIntervalUsePos d f =- let {- go rs =- (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)- (\r ->- searchInRange r f)- (\r rs' ->- Lib.option_choose (searchInRange r f) (go rs'))- rs}- in go (rds d)+ case d of {+ Build_IntervalDesc ivar0 ibeg0 iend0 rds0 ->+ let {+ _evar_0_ = \r ->+ let {_top_assumption_ = searchInRange r f} in+ let {+ _evar_0_ = \_top_assumption_0 -> Prelude.Just ((,) r+ _top_assumption_0)}+ in+ let {_evar_0_0 = Prelude.Nothing} in+ case _top_assumption_ of {+ Prelude.Just x -> _evar_0_ x;+ Prelude.Nothing -> _evar_0_0}}+ in+ let {+ _evar_0_0 = \r rs iHrs ->+ let {_top_assumption_ = searchInRange r f} in+ let {+ _evar_0_0 = \_top_assumption_0 -> Prelude.Just ((,) r+ _top_assumption_0)}+ in+ let {_evar_0_1 = iHrs __ __ __} in+ case _top_assumption_ of {+ Prelude.Just x -> _evar_0_0 x;+ Prelude.Nothing -> _evar_0_1}}+ in+ NonEmpty0.coq_NonEmpty_rec (\r _ _ _ -> _evar_0_ r) (\r rs iHrs _ _ _ ->+ _evar_0_0 r rs iHrs) rds0 __ __ __} lookupUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) -> Prelude.Maybe Lib.Coq_oddnum@@ -142,318 +143,286 @@ nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe Lib.Coq_oddnum nextUseAfter d pos =- lookupUsePos d (\u -> (Prelude.<=) ((Prelude.succ) pos) (UsePos.uloc u))+ case lookupUsePos d (\u ->+ (Prelude.<=) ((Prelude.succ) pos) (UsePos.uloc u)) of {+ Prelude.Just s -> Prelude.Just s;+ Prelude.Nothing -> Prelude.Nothing} -firstUsePos :: IntervalDesc -> Prelude.Maybe Prelude.Int-firstUsePos d =- case Range.ups ( (Prelude.head (rds d))) of {+rangeFirstUsePos :: Range.RangeDesc -> Prelude.Maybe UsePos.UsePos+rangeFirstUsePos rd =+ case Range.ups rd of { [] -> Prelude.Nothing;- (:) u l -> Prelude.Just (UsePos.uloc u)}+ (:) u l -> Prelude.Just u} +firstUsePos :: IntervalDesc -> Prelude.Maybe UsePos.UsePos+firstUsePos d =+ let {+ go xs =+ (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+ (\x ->+ rangeFirstUsePos ( x))+ (\x xs0 ->+ Lib.option_choose (rangeFirstUsePos ( x)) (go xs0))+ xs}+ in go (rds d)++lastUsePos :: IntervalDesc -> Prelude.Maybe UsePos.UsePos+lastUsePos d =+ let {+ go xs =+ (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+ (\x ->+ Lib.olast (Range.ups ( x)))+ (\x xs0 ->+ Lib.option_choose (go xs0) (Lib.olast (Range.ups ( x))))+ xs}+ in go (rds d)++afterLifetimeHole :: IntervalDesc -> Lib.Coq_oddnum -> Lib.Coq_oddnum+afterLifetimeHole d pos =+ let {+ f = \x k ->+ case (Prelude.<=) ((Prelude.succ) ( pos)) (Range.rbeg ( x)) of {+ Prelude.True -> Range.rbeg ( x);+ Prelude.False -> k}}+ in+ let {+ go xs =+ (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+ (\x ->+ f x pos)+ (\x xs0 ->+ f x (go xs0))+ xs}+ in go (rds d)+ firstUseReqReg :: IntervalDesc -> Prelude.Maybe Lib.Coq_oddnum firstUseReqReg d = lookupUsePos d UsePos.regReq -intervalSpan :: ([] Range.RangeDesc) -> Prelude.Int -> Prelude.Int ->- Prelude.Int -> Prelude.Int -> IntervalKind ->- ((,) (Prelude.Maybe IntervalDesc)- (Prelude.Maybe IntervalDesc))-intervalSpan rs before iv ib ie knd =+firstUseReqRegOrEnd :: IntervalDesc -> Lib.Coq_oddnum+firstUseReqRegOrEnd d =+ let {filtered_var = firstUseReqReg d} in+ case filtered_var of {+ Prelude.Just n -> n;+ Prelude.Nothing ->+ case Ssrnat.odd (iend d) of {+ Prelude.True -> iend d;+ Prelude.False -> Prelude.pred (iend d)}}++divideIntervalRanges :: IntervalDesc -> Prelude.Int ->+ ((,) Range.SortedRanges Range.SortedRanges)+divideIntervalRanges d before = let {- _evar_0_ = \lknd rknd ->- (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)- (\r ->- let {_top_assumption_ = Range.rangeSpan before ( r)} in+ _evar_0_ = \_top_assumption_ ->+ let {+ _evar_0_ = \_top_assumption_0 -> let {- _evar_0_ = \_top_assumption_0 ->+ _evar_0_ = \_ -> let {- _evar_0_ = \r0 _top_assumption_1 ->- let {- _evar_0_ = \r1 ->- let {- _evar_0_ = let {- _evar_0_ = \_ _ -> (,) (Prelude.Just- (packInterval (Build_IntervalDesc iv- (Range.rbeg ( r0)) (Range.rend ( r0)) lknd ((:[])- ( r0))))) (Prelude.Just- (packInterval (Build_IntervalDesc iv- (Range.rbeg ( r1)) (Range.rend ( r1)) rknd ((:[])- ( r1)))))}- in- _evar_0_}- in- _evar_0_ __ __}- in+ _evar_0_ = \_ _ -> let {- _evar_0_0 = let {- _evar_0_0 = let {- _evar_0_0 = \_ -> (,) (Prelude.Just- (packInterval (Build_IntervalDesc iv- (Range.rbeg ( r0)) (Range.rend ( r0))- knd ((:[]) ( r0))))) Prelude.Nothing}- in- _evar_0_0}- in- _evar_0_0}+ _evar_0_ = \_ ->+ let {_evar_0_ = let {_evar_0_ = \_ -> (,) [] []} in _evar_0_} in+ _evar_0_ __} in- case _top_assumption_1 of {- Prelude.Just x -> (\_ -> _evar_0_ x);- Prelude.Nothing -> _evar_0_0}}+ _evar_0_ __} in+ _evar_0_ __ __}+ in+ let {+ _evar_0_0 = \r2 rs2 -> let {- _evar_0_0 = \_top_assumption_1 ->+ _evar_0_0 = \_ -> let {- _evar_0_0 = \r1 ->+ _evar_0_0 = \_ _ -> let {- _evar_0_0 = let {- _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just- (packInterval (Build_IntervalDesc iv- (Range.rbeg ( r1)) (Range.rend ( r1)) knd ((:[])- ( r1)))))}- in- _evar_0_0}+ _evar_0_0 = \_ ->+ let {+ _evar_0_0 = let {+ _evar_0_0 = let {+ _evar_0_0 = \_ _ ->+ let {+ _evar_0_0 = let {+ _evar_0_0 = \_ -> (,)+ [] ((:) r2 rs2)}+ in+ _evar_0_0}+ in+ _evar_0_0 __}+ in+ _evar_0_0}+ in+ _evar_0_0}+ in+ _evar_0_0 __ __} in- _evar_0_0}+ _evar_0_0 __} in- let {_evar_0_1 = \_ -> Logic.coq_False_rec} in- case _top_assumption_1 of {- Prelude.Just x -> _evar_0_0 x;- Prelude.Nothing -> _evar_0_1}}+ _evar_0_0 __ __} in- case _top_assumption_0 of {- Prelude.Just x -> _evar_0_ x;- Prelude.Nothing -> _evar_0_0}}+ _evar_0_0 __} in- case _top_assumption_ of {- (,) x x0 -> _evar_0_ x x0 __})- (\r rs0 ->- let {_top_assumption_ = Range.rangeSpan before ( r)} in+ case _top_assumption_0 of {+ [] -> _evar_0_;+ (:) x x0 -> (\_ -> _evar_0_0 x x0)}}+ in+ let {+ _evar_0_0 = \r1 rs1 _top_assumption_0 -> let {- _evar_0_ = \_top_assumption_0 ->+ _evar_0_0 = \_ -> let {- _evar_0_ = \r0 _top_assumption_1 ->- let {- _evar_0_ = \r1 ->- let {- _evar_0_ = \_ ->- (Prelude.flip (Prelude.$)) __ (\_ ->- let {- _evar_0_ = \_ -> (,) (Prelude.Just- (packInterval (Build_IntervalDesc iv (Range.rbeg ( r0))- (Range.rend ( r0)) lknd ((:[]) ( r0))))) (Prelude.Just- (packInterval (Build_IntervalDesc iv (Range.rbeg ( r1))- (Range.rend ( (Prelude.last rs0))) rknd ((:) r1 rs0))))}- in- _evar_0_ __)}- in- _evar_0_ __}- in+ _evar_0_0 = \_ _ -> let { _evar_0_0 = \_ -> let {- _evar_0_0 = \_ ->- let {- _top_assumption_2 = intervalSpan rs0 before iv- (Range.rbeg ( (Prelude.head rs0)))- (Range.rend ( (Prelude.last rs0))) knd}- in- let {- _evar_0_0 = \_top_assumption_3 ->- let {- _evar_0_0 = \i1_1 _top_assumption_4 ->- let {- _evar_0_0 = \i1_2 ->- case i1_1 of {- Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 ->- let {- _evar_0_0 = let {- _evar_0_0 = \_ ->- let {- _evar_0_0 = \_ ->- let {- _evar_0_0 = \_ ->- (Prelude.flip (Prelude.$)) __ (\_ ->- let {- _evar_0_0 = let {- _evar_0_0 = \_ _ _ ->- (,) (Prelude.Just- (packInterval- (Build_IntervalDesc- ivar0- (Range.rbeg ( r))- iend0 lknd ((:) r- rds0))))- (Prelude.Just- (packInterval- (Build_IntervalDesc- (ivar ( i1_2))- (ibeg ( i1_2))- (iend ( i1_2))- rknd- (rds ( i1_2)))))}- in- _evar_0_0 __}- in- _evar_0_0)}- in- _evar_0_0 __}- in- _evar_0_0 __}- in- _evar_0_0}- in- _evar_0_0 __}}- in- let {- _evar_0_1 = \_ _ _ ->- case i1_1 of {- Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 ->- let {- _evar_0_1 = let {- _evar_0_1 = \_ ->- (Prelude.flip (Prelude.$)) __ (\_ ->- (Prelude.flip (Prelude.$)) __ (\_ ->- let {- _evar_0_1 = \_ ->- let {- _evar_0_1 = \_ -> (,)- (Prelude.Just- (packInterval- (Build_IntervalDesc ivar0- (Range.rbeg ( r)) iend0 lknd- ((:) r rds0))))- Prelude.Nothing}- in- _evar_0_1 __}- in- _evar_0_1 __))}- in- _evar_0_1}- in- _evar_0_1 __}}- in- case _top_assumption_4 of {- Prelude.Just x -> (\_ -> _evar_0_0 x);- Prelude.Nothing -> _evar_0_1}}- in- let {- _evar_0_1 = \_top_assumption_4 ->- let {- _evar_0_1 = \i1_2 ->- case i1_2 of {- Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 ->- let {- _evar_0_1 = let {- _evar_0_1 = \_ ->- let {- _evar_0_1 = \_ _ ->- let {- _evar_0_1 = \_ ->- let {- _evar_0_1 = \_ ->- let {- _evar_0_1 = \_ ->- (Prelude.flip (Prelude.$)) __- (\_ -> (,) (Prelude.Just- (packInterval- (Build_IntervalDesc iv- (Range.rbeg ( r0))- (Range.rend ( r0)) lknd- ((:[]) ( r0)))))- (Prelude.Just- (packInterval- (Build_IntervalDesc- (ivar (Build_IntervalDesc- ivar0- (Range.rbeg- ( (Prelude.head rds0)))- (Range.rend- ( (Prelude.last rds0)))- iknd0 rds0))- (ibeg (Build_IntervalDesc- ivar0- (Range.rbeg- ( (Prelude.head rds0)))- (Range.rend- ( (Prelude.last rds0)))- iknd0 rds0))- (iend (Build_IntervalDesc- ivar0- (Range.rbeg- ( (Prelude.head rds0)))- (Range.rend- ( (Prelude.last rds0)))- iknd0 rds0)) rknd- (rds (Build_IntervalDesc- ivar0- (Range.rbeg- ( (Prelude.head rds0)))- (Range.rend- ( (Prelude.last rds0)))- iknd0 rds0))))))}- in- _evar_0_1 __}- in- _evar_0_1 __}- in- _evar_0_1 __}- in- _evar_0_1 __ __}- in- _evar_0_1}- in- _evar_0_1 __}}- in- let {_evar_0_2 = \_ _ _ -> Logic.coq_False_rec} in- case _top_assumption_4 of {- Prelude.Just x -> (\_ _ _ -> _evar_0_1 x);- Prelude.Nothing -> _evar_0_2}}- in- case _top_assumption_3 of {- Prelude.Just x -> _evar_0_0 x;- Prelude.Nothing -> _evar_0_1}}- in- case _top_assumption_2 of {- (,) x x0 -> _evar_0_0 x x0 __ __ __}}+ _evar_0_0 = let {+ _evar_0_0 = let {+ _evar_0_0 = \_ _ ->+ let {+ _evar_0_0 = let {+ _evar_0_0 = \_ -> (,)+ ((:) r1 rs1) []}+ in+ _evar_0_0}+ in+ _evar_0_0 __}+ in+ _evar_0_0}+ in+ _evar_0_0} in- _evar_0_0 __}+ _evar_0_0 __ __} in- case _top_assumption_1 of {- Prelude.Just x -> (\_ -> _evar_0_ x);- Prelude.Nothing -> _evar_0_0}}+ _evar_0_0 __} in+ _evar_0_0 __ __}+ in+ let {+ _evar_0_1 = \r2 rs2 -> let {- _evar_0_0 = \_top_assumption_1 ->+ _evar_0_1 = \_ -> let {- _evar_0_0 = \r1 ->+ _evar_0_1 = \_ -> let {- _evar_0_0 = \_ ->- let {- _evar_0_0 = \_ ->- let {- _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just- (packInterval (Build_IntervalDesc iv (Range.rbeg ( r1))- (Range.rend ( (Prelude.last rs0))) knd ((:) r1 rs0))))}- in- _evar_0_0 __}- in- _evar_0_0 __}+ _evar_0_1 = let {+ _evar_0_1 = let {+ _evar_0_1 = \_ _ ->+ let {+ _evar_0_1 = let {+ _evar_0_1 = \_ -> (,)+ ((:) r1 rs1) ((:) r2+ rs2)}+ in+ _evar_0_1}+ in+ _evar_0_1 __}+ in+ _evar_0_1}+ in+ _evar_0_1} in- _evar_0_0 __}+ _evar_0_1 __ __} in- let {_evar_0_1 = \_ -> Logic.coq_False_rec} in- case _top_assumption_1 of {- Prelude.Just x -> (\_ -> _evar_0_0 x);- Prelude.Nothing -> _evar_0_1}}+ _evar_0_1 __} in- case _top_assumption_0 of {- Prelude.Just x -> _evar_0_ x;- Prelude.Nothing -> _evar_0_0}}+ _evar_0_1 __} in- case _top_assumption_ of {- (,) x x0 -> _evar_0_ x x0 __})- rs}+ case _top_assumption_0 of {+ [] -> _evar_0_0;+ (:) x x0 -> (\_ -> _evar_0_1 x x0)}}+ in+ case _top_assumption_ of {+ [] -> _evar_0_;+ (:) x x0 -> _evar_0_0 x x0}} in- case splitKind knd of {- (,) x x0 -> _evar_0_ x x0}+ case Lib.span (\rd ->+ (Prelude.<=) ((Prelude.succ) (Range.rend ( rd))) before) ( (rds d)) of {+ (,) x x0 -> _evar_0_ x x0 __}++splitIntervalRanges :: IntervalDesc -> Prelude.Int ->+ ((,) Range.SortedRanges Range.SortedRanges)+splitIntervalRanges d before =+ let {_top_assumption_ = divideIntervalRanges d before} in+ let {+ _evar_0_ = \_top_assumption_0 _top_assumption_1 ->+ let {+ _evar_0_ = \_ _ _ ->+ let {_evar_0_ = \_ -> Logic.coq_False_rec} in+ let {_evar_0_0 = \_a_ _l_ -> Logic.coq_False_rec} in+ case _top_assumption_0 of {+ [] -> _evar_0_ __;+ (:) x x0 -> _evar_0_0 x x0}}+ in+ let {+ _evar_0_0 = \r2 rs2 ->+ let {_evar_0_0 = \_ -> (,) _top_assumption_0 ((:) r2 rs2)} in+ let {+ _evar_0_1 = \_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {_top_assumption_2 = Range.rangeSpan ( r2) before} in+ let {+ _evar_0_1 = \r2a r2b -> (,) (Seq.rcons _top_assumption_0 r2a) ((:)+ r2b rs2)}+ in+ case _top_assumption_2 of {+ (,) x x0 -> _evar_0_1 x x0})}+ in+ case (Prelude.<=) before (Range.rbeg ( r2)) of {+ Prelude.True -> _evar_0_0 __;+ Prelude.False -> _evar_0_1 __}}+ in+ case _top_assumption_1 of {+ [] -> _evar_0_ __ __;+ (:) x x0 -> (\_ -> _evar_0_0 x x0)}}+ in+ case _top_assumption_ of {+ (,) x x0 -> _evar_0_ x x0 __}++type SubIntervalsOf = ((,) IntervalDesc IntervalDesc)++splitInterval :: IntervalDesc -> Prelude.Int -> SubIntervalsOf+splitInterval d before =+ let {_top_assumption_ = splitIntervalRanges d before} in+ let {+ _evar_0_ = \_top_assumption_0 ->+ let {+ _evar_0_ = \_top_assumption_1 ->+ let {_evar_0_ = \_ _ _ -> Logic.coq_False_rec} in+ let {_evar_0_0 = \r2 rs2 -> Logic.coq_False_rec} in+ case _top_assumption_1 of {+ [] -> _evar_0_ __ __;+ (:) x x0 -> (\_ -> _evar_0_0 x x0)}}+ in+ let {+ _evar_0_0 = \r1 rs1 _top_assumption_1 ->+ let {_evar_0_0 = \_ _ _ -> Logic.coq_False_rec} in+ let {+ _evar_0_1 = \r2 rs2 ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$)) __ (\_ -> (,)+ (packInterval (Build_IntervalDesc (ivar (getIntervalDesc d))+ (Range.rbeg+ ( (Prelude.head (NonEmpty0.coq_NE_from_list r1 rs1))))+ (Range.rend+ ( (Prelude.last (NonEmpty0.coq_NE_from_list r1 rs1))))+ (NonEmpty0.coq_NE_from_list r1 rs1)))+ (packInterval (Build_IntervalDesc (ivar (getIntervalDesc d))+ (Range.rbeg+ ( (Prelude.head (NonEmpty0.coq_NE_from_list r2 rs2))))+ (Range.rend+ ( (Prelude.last (NonEmpty0.coq_NE_from_list r2 rs2))))+ (NonEmpty0.coq_NE_from_list r2 rs2)))))}+ in+ case _top_assumption_1 of {+ [] -> _evar_0_0 __ __;+ (:) x x0 -> (\_ -> _evar_0_1 x x0)}}+ in+ (\_top_assumption_1 ->+ case _top_assumption_0 of {+ [] -> _evar_0_ _top_assumption_1;+ (:) x x0 -> _evar_0_0 x x0 _top_assumption_1})}+ in+ case _top_assumption_ of {+ (,) x x0 -> _evar_0_ x x0 __}
LinearScan/Lib.hs view
@@ -12,7 +12,6 @@ import qualified LinearScan.Specif as Specif import qualified LinearScan.Eqtype as Eqtype-import qualified LinearScan.Ssrbool as Ssrbool __ :: any@@ -24,6 +23,15 @@ Prelude.Just a -> x; Prelude.Nothing -> y} +olast :: ([] a1) -> Prelude.Maybe a1+olast l =+ let {+ go res xs =+ case xs of {+ [] -> res;+ (:) x xs0 -> go (Prelude.Just x) xs0}}+ in go Prelude.Nothing l+ maybeLookup :: Eqtype.Equality__Coq_type -> ([] ((,) Eqtype.Equality__Coq_sort a1)) -> Eqtype.Equality__Coq_sort -> Prelude.Maybe a1@@ -55,6 +63,13 @@ forFoldr b v f = Prelude.foldr f b v +catMaybes :: ([] (Prelude.Maybe a1)) -> [] a1+catMaybes l =+ forFoldr [] l (\mx rest ->+ case mx of {+ Prelude.Just x -> (:) x rest;+ Prelude.Nothing -> rest})+ span :: (a1 -> Prelude.Bool) -> ([] a1) -> (,) ([] a1) ([] a1) span p l = case l of {@@ -74,7 +89,7 @@ Prelude.False -> (,) (Prelude.fst acc) ((:) x (Prelude.snd acc))}) ((,) [] []) -insert :: (Ssrbool.Coq_rel a1) -> a1 -> ([] a1) -> [] a1+insert :: (a1 -> a1 -> Prelude.Bool) -> a1 -> ([] a1) -> [] a1 insert p z l = case l of { [] -> (:) z [];
LinearScan/LiveSets.hs view
@@ -16,6 +16,7 @@ import qualified LinearScan.Blocks as Blocks import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Lib as Lib+import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrnat as Ssrnat@@ -233,9 +234,9 @@ (,) lastIdx liveSet1 -> (,) ((Prelude.succ) ((Prelude.succ) lastIdx)) (case Lib.partition (\v ->- Eqtype.eq_op Blocks.coq_VarKind_eqType+ Eqtype.eq_op UsePos.coq_VarKind_eqType (unsafeCoerce (Blocks.varKind maxReg v))- (unsafeCoerce Blocks.Input))+ (unsafeCoerce UsePos.Input)) (Blocks.opRefs maxReg oinfo o) of { (,) inputs others -> let {
+ LinearScan/Loops.hs view
@@ -0,0 +1,412 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Loops where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Blocks as Blocks+import qualified LinearScan.IntMap as IntMap+import qualified LinearScan.Lib as Lib+import qualified LinearScan.State as State+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrnat as Ssrnat++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++data LoopState =+ Build_LoopState IntMap.IntSet IntMap.IntSet ([] Blocks.BlockId) IntMap.IntSet + (IntMap.IntMap IntMap.IntSet) (IntMap.IntMap IntMap.IntSet) (IntMap.IntMap+ IntMap.IntSet) + (IntMap.IntMap ((,) Prelude.Int Prelude.Int))++activeBlocks :: LoopState -> IntMap.IntSet+activeBlocks l =+ case l of {+ Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0+ loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0+ loopDepths0 -> activeBlocks0}++visitedBlocks :: LoopState -> IntMap.IntSet+visitedBlocks l =+ case l of {+ Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0+ loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0+ loopDepths0 -> visitedBlocks0}++loopHeaderBlocks :: LoopState -> [] Blocks.BlockId+loopHeaderBlocks l =+ case l of {+ Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0+ loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0+ loopDepths0 -> loopHeaderBlocks0}++loopEndBlocks :: LoopState -> IntMap.IntSet+loopEndBlocks l =+ case l of {+ Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0+ loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0+ loopDepths0 -> loopEndBlocks0}++forwardBranches :: LoopState -> IntMap.IntMap IntMap.IntSet+forwardBranches l =+ case l of {+ Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0+ loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0+ loopDepths0 -> forwardBranches0}++backwardBranches :: LoopState -> IntMap.IntMap IntMap.IntSet+backwardBranches l =+ case l of {+ Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0+ loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0+ loopDepths0 -> backwardBranches0}++loopIndices :: LoopState -> IntMap.IntMap IntMap.IntSet+loopIndices l =+ case l of {+ Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0+ loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0+ loopDepths0 -> loopIndices0}++loopDepths :: LoopState -> IntMap.IntMap ((,) Prelude.Int Prelude.Int)+loopDepths l =+ case l of {+ Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0+ loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0+ loopDepths0 -> loopDepths0}++emptyLoopState :: LoopState+emptyLoopState =+ Build_LoopState IntMap.emptyIntSet IntMap.emptyIntSet [] IntMap.emptyIntSet+ IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap+ IntMap.emptyIntMap++modifyActiveBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> State.State+ LoopState ()+modifyActiveBlocks f =+ State.modify (\st -> Build_LoopState (f (activeBlocks st))+ (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st)+ (forwardBranches st) (backwardBranches st) (loopIndices st)+ (loopDepths st))++modifyVisitedBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> State.State+ LoopState ()+modifyVisitedBlocks f =+ State.modify (\st -> Build_LoopState (activeBlocks st)+ (f (visitedBlocks st)) (loopHeaderBlocks st) (loopEndBlocks st)+ (forwardBranches st) (backwardBranches st) (loopIndices st)+ (loopDepths st))++modifyLoopHeaderBlocks :: (([] Blocks.BlockId) -> [] Blocks.BlockId) ->+ State.State LoopState ()+modifyLoopHeaderBlocks f =+ State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+ (f (loopHeaderBlocks st)) (loopEndBlocks st) (forwardBranches st)+ (backwardBranches st) (loopIndices st) (loopDepths st))++modifyLoopEndBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> State.State+ LoopState ()+modifyLoopEndBlocks f =+ State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+ (loopHeaderBlocks st) (f (loopEndBlocks st)) (forwardBranches st)+ (backwardBranches st) (loopIndices st) (loopDepths st))++modifyForwardBranches :: ((IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap+ IntMap.IntSet) -> State.State LoopState ()+modifyForwardBranches f =+ State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+ (loopHeaderBlocks st) (loopEndBlocks st) (f (forwardBranches st))+ (backwardBranches st) (loopIndices st) (loopDepths st))++modifyBackwardBranches :: ((IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap+ IntMap.IntSet) -> State.State LoopState ()+modifyBackwardBranches f =+ State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+ (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)+ (f (backwardBranches st)) (loopIndices st) (loopDepths st))++setLoopIndices :: (IntMap.IntMap IntMap.IntSet) -> State.State LoopState ()+setLoopIndices indices =+ State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+ (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)+ (backwardBranches st) indices (loopDepths st))++setLoopDepths :: (IntMap.IntMap ((,) Prelude.Int Prelude.Int)) -> State.State+ LoopState ()+setLoopDepths depths =+ State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+ (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)+ (backwardBranches st) (loopIndices st) depths)++addReference :: Prelude.Int -> Prelude.Int -> (IntMap.IntMap IntMap.IntSet)+ -> IntMap.IntMap IntMap.IntSet+addReference i x =+ IntMap.coq_IntMap_alter (\macc ->+ case macc of {+ Prelude.Just acc -> Prelude.Just (IntMap.coq_IntSet_insert x acc);+ Prelude.Nothing -> Prelude.Just (IntMap.coq_IntSet_singleton x)}) i++pathToLoopHeader :: Blocks.BlockId -> Prelude.Int -> LoopState ->+ Prelude.Maybe IntMap.IntSet+pathToLoopHeader b header st =+ let {+ go fuel visited b0 =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ Prelude.Nothing)+ (\n ->+ let {visited' = IntMap.coq_IntSet_insert b0 visited} in+ let {+ forwardPreds = case IntMap.coq_IntMap_lookup b0 (forwardBranches st) of {+ Prelude.Just preds -> IntMap.coq_IntSet_toList preds;+ Prelude.Nothing -> []}}+ in+ let {+ backwardPreds = case IntMap.coq_IntMap_lookup b0+ (backwardBranches st) of {+ Prelude.Just preds -> IntMap.coq_IntSet_toList preds;+ Prelude.Nothing -> []}}+ in+ let {preds = (Prelude.++) forwardPreds backwardPreds} in+ Lib.forFold (Prelude.Just (IntMap.coq_IntSet_singleton b0))+ (unsafeCoerce preds) (\mxs pred ->+ case mxs of {+ Prelude.Just xs ->+ case Eqtype.eq_op Ssrnat.nat_eqType pred (unsafeCoerce header) of {+ Prelude.True -> Prelude.Just+ (IntMap.coq_IntSet_union xs+ (IntMap.coq_IntSet_singleton (unsafeCoerce pred)));+ Prelude.False ->+ case IntMap.coq_IntSet_member (unsafeCoerce pred) visited' of {+ Prelude.True -> Prelude.Just xs;+ Prelude.False ->+ case unsafeCoerce go n visited' pred of {+ Prelude.Just ys -> Prelude.Just+ (IntMap.coq_IntSet_union xs ys);+ Prelude.Nothing -> Prelude.Nothing}}};+ Prelude.Nothing -> Prelude.Nothing}))+ fuel}+ in go (IntMap.coq_IntSet_size (visitedBlocks st)) IntMap.emptyIntSet b++computeLoopDepths :: (Blocks.BlockInfo a1 a2 a3 a4) -> (IntMap.IntMap + a1) -> State.State LoopState ()+computeLoopDepths binfo bs =+ State.bind (\st ->+ let {+ m = Lib.forFold IntMap.emptyIntMap+ (IntMap.coq_IntSet_toList (loopEndBlocks st)) (\m endBlock ->+ case IntMap.coq_IntMap_lookup endBlock bs of {+ Prelude.Just b ->+ Lib.forFold m (unsafeCoerce (Blocks.blockSuccessors binfo b))+ (\m' sux ->+ let {+ loopIndex = Seq.find (\x ->+ Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce x)+ sux) (loopHeaderBlocks st)}+ in+ case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce loopIndex)+ (unsafeCoerce (Data.List.length (loopHeaderBlocks st))) of {+ Prelude.True -> m';+ Prelude.False ->+ let {mres = pathToLoopHeader endBlock (unsafeCoerce sux) st}+ in+ case mres of {+ Prelude.Just path ->+ Lib.forFold m' (IntMap.coq_IntSet_toList path)+ (\m'' blk -> addReference loopIndex blk m'');+ Prelude.Nothing -> m'}});+ Prelude.Nothing -> m})}+ in+ let {+ f = \acc loopIndex refs ->+ IntMap.coq_IntSet_forFold acc refs (\m' blk ->+ let {+ f = \mx ->+ case mx of {+ Prelude.Just y ->+ case y of {+ (,) idx depth -> Prelude.Just ((,) (Prelude.min idx loopIndex)+ ((Prelude.succ) depth))};+ Prelude.Nothing -> Prelude.Just ((,) loopIndex ((Prelude.succ) 0))}}+ in+ IntMap.coq_IntMap_alter f blk m')}+ in+ State.bind (\x ->+ setLoopDepths (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m))+ (setLoopIndices m)) State.get++computeVarReferences :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->+ (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> LoopState ->+ IntMap.IntMap IntMap.IntSet+computeVarReferences maxReg binfo oinfo bs st =+ Lib.forFold IntMap.emptyIntMap bs (\acc b ->+ let {bid = Blocks.blockId binfo b} in+ let {+ g = \acc1 loopIndex blks ->+ case Prelude.not (IntMap.coq_IntSet_member bid blks) of {+ Prelude.True -> acc1;+ Prelude.False ->+ case Blocks.blockOps binfo b of {+ (,) p zs ->+ case p of {+ (,) xs ys ->+ Lib.forFold acc1 ((Prelude.++) xs ((Prelude.++) ys zs))+ (\acc2 op ->+ Lib.forFold acc2 (Blocks.opRefs maxReg oinfo op) (\acc3 v ->+ case Blocks.varId maxReg v of {+ Prelude.Left p0 -> acc3;+ Prelude.Right vid -> addReference loopIndex vid acc3}))}}}}+ in+ IntMap.coq_IntMap_foldlWithKey g acc (loopIndices st))++findLoopEnds :: (Blocks.BlockInfo a1 a2 a3 a4) -> (IntMap.IntMap a1) ->+ State.State LoopState ()+findLoopEnds binfo bs =+ let {+ go = let {+ go n b =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ State.pure ())+ (\n0 ->+ let {bid = Blocks.blockId binfo b} in+ State.bind (\x ->+ State.bind (\x0 ->+ State.bind (\x1 ->+ modifyActiveBlocks (IntMap.coq_IntSet_delete bid))+ (State.forM_ (Blocks.blockSuccessors binfo b) (\sux ->+ State.bind (\active ->+ State.bind (\x1 ->+ State.bind (\visited ->+ case IntMap.coq_IntSet_member sux visited of {+ Prelude.True -> State.pure ();+ Prelude.False ->+ case IntMap.coq_IntMap_lookup sux bs of {+ Prelude.Just x2 -> go n0 x2;+ Prelude.Nothing -> State.pure ()}})+ (State.gets visitedBlocks))+ (case IntMap.coq_IntSet_member sux active of {+ Prelude.True ->+ State.bind (\x1 ->+ State.bind (\x2 ->+ modifyBackwardBranches (addReference sux bid))+ (modifyLoopEndBlocks+ (IntMap.coq_IntSet_insert bid)))+ (modifyLoopHeaderBlocks (\l ->+ case Prelude.not+ (Ssrbool.in_mem (unsafeCoerce sux)+ (Ssrbool.mem+ (Seq.seq_predType+ Ssrnat.nat_eqType)+ (unsafeCoerce l))) of {+ Prelude.True -> (:) sux l;+ Prelude.False -> l}));+ Prelude.False ->+ modifyForwardBranches (addReference sux bid)}))+ (State.gets activeBlocks))))+ (modifyActiveBlocks (IntMap.coq_IntSet_insert bid)))+ (modifyVisitedBlocks (IntMap.coq_IntSet_insert bid)))+ n}+ in go}+ in+ case IntMap.coq_IntMap_toList bs of {+ [] -> State.pure ();+ (:) p l ->+ case p of {+ (,) n b ->+ State.bind (\x -> computeLoopDepths binfo bs)+ (go (IntMap.coq_IntMap_size bs) b)}}++computeBlockOrder :: (Blocks.BlockInfo a1 a2 a3 a4) -> ([] a1) -> (,)+ LoopState ([] a1)+computeBlockOrder binfo blocks =+ case blocks of {+ [] -> (,) emptyLoopState [];+ (:) b bs ->+ let {+ blockMap = IntMap.coq_IntMap_fromList+ (Prelude.map (\x -> (,) (Blocks.blockId binfo x) x) blocks)}+ in+ case findLoopEnds binfo blockMap emptyLoopState of {+ (,) u st ->+ let {+ isHeavier = \x y ->+ let {x_id = Blocks.blockId binfo x} in+ let {y_id = Blocks.blockId binfo y} in+ let {+ x_depth = case IntMap.coq_IntMap_lookup x_id (loopDepths st) of {+ Prelude.Just p ->+ case p of {+ (,) idx depth -> depth};+ Prelude.Nothing -> 0}}+ in+ let {+ y_depth = case IntMap.coq_IntMap_lookup y_id (loopDepths st) of {+ Prelude.Just p ->+ case p of {+ (,) idx depth -> depth};+ Prelude.Nothing -> 0}}+ in+ (Prelude.<=) ((Prelude.succ) y_depth) x_depth}+ in+ let {+ go = let {+ go n branches work_list =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ [])+ (\n0 ->+ case work_list of {+ [] -> [];+ (:) w ws ->+ case let {bid = Blocks.blockId binfo w} in+ let {suxs = Blocks.blockSuccessors binfo w} in+ Lib.forFoldr ((,) branches ws) suxs (\sux acc ->+ case acc of {+ (,) branches' ws' ->+ let {+ insertion = case IntMap.coq_IntMap_lookup sux+ blockMap of {+ Prelude.Just s ->+ Lib.insert isHeavier s ws';+ Prelude.Nothing -> ws'}}+ in+ case IntMap.coq_IntMap_lookup sux branches' of {+ Prelude.Just incs -> (,)+ (IntMap.coq_IntMap_insert sux+ (IntMap.coq_IntSet_delete bid incs)+ branches')+ (case Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce+ (IntMap.coq_IntSet_size incs))+ (unsafeCoerce ((Prelude.succ) 0)) of {+ Prelude.True -> insertion;+ Prelude.False -> ws'});+ Prelude.Nothing -> (,) branches' insertion}}) of {+ (,) branches' ws' -> (:) w (go n0 branches' ws')}})+ n}+ in go}+ in+ (,) st (go (Data.List.length blocks) (forwardBranches st) ((:) b []))}}+
LinearScan/Main.hs view
@@ -14,35 +14,65 @@ import qualified LinearScan.Assign as Assign import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Build as Build+import qualified LinearScan.IntMap as IntMap import qualified LinearScan.LiveSets as LiveSets+import qualified LinearScan.Loops as Loops import qualified LinearScan.Morph as Morph-import qualified LinearScan.Order as Order import qualified LinearScan.Resolve as Resolve+import qualified LinearScan.ScanState as ScanState+import qualified LinearScan.Ssrnat as Ssrnat +data FinalStage =+ BuildingIntervalsFailed+ | AllocatingRegistersFailed++data Details blockType1 blockType2 opType1 opType2 accType =+ Build_Details (Prelude.Maybe ((,) Morph.SSError FinalStage)) (IntMap.IntMap+ LiveSets.BlockLiveSets) + ([] blockType1) ([] blockType2) accType (Prelude.Maybe+ ScanState.ScanStateDesc) (Prelude.Maybe+ ScanState.ScanStateDesc) + (Blocks.BlockInfo blockType1 blockType2 opType1 opType2) (Blocks.OpInfo+ accType opType1+ opType2) Loops.LoopState+ linearScan :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) -> (Blocks.OpInfo- a5 a3 a4) -> ([] a1) -> a5 -> Prelude.Either Morph.SSError- ((,) ([] a2) a5)+ a5 a3 a4) -> ([] a1) -> a5 -> Details a1 a2 a3 a4 a5 linearScan maxReg binfo oinfo blocks accum =- let {blocks' = Order.computeBlockOrder blocks} in- let {liveSets = LiveSets.computeLocalLiveSets maxReg binfo oinfo blocks'}- in- let {- liveSets' = LiveSets.computeGlobalLiveSetsRecursively binfo blocks'- liveSets}- in- case Build.buildIntervals maxReg binfo oinfo blocks liveSets' of {- Prelude.Left err -> Prelude.Left err;- Prelude.Right ssig ->- case Allocate.walkIntervals maxReg ( ssig) ((Prelude.succ)- (Blocks.countOps binfo blocks)) of {- Prelude.Left err -> Prelude.Left err;- Prelude.Right ssig' ->- let {- mappings = Resolve.resolveDataFlow maxReg binfo ( ssig') blocks- liveSets'}- in- Prelude.Right- (Assign.assignRegNum maxReg binfo oinfo ( ssig') liveSets' mappings- blocks accum)}}+ case Loops.computeBlockOrder binfo blocks of {+ (,) loops blocks1 ->+ let {liveSets = LiveSets.computeLocalLiveSets maxReg binfo oinfo blocks1}+ in+ let {+ liveSets' = LiveSets.computeGlobalLiveSetsRecursively binfo blocks1+ liveSets}+ in+ case Build.buildIntervals maxReg binfo oinfo blocks1 loops liveSets' of {+ Prelude.Left err -> Build_Details (Prelude.Just ((,) err+ BuildingIntervalsFailed)) liveSets' blocks1 [] accum Prelude.Nothing+ Prelude.Nothing binfo oinfo loops;+ Prelude.Right ssig ->+ let {opCount = (Prelude.succ) (Blocks.countOps binfo blocks1)} in+ case Allocate.walkIntervals maxReg ( ssig) opCount of {+ Prelude.Left p ->+ case p of {+ (,) err ssig' -> Build_Details (Prelude.Just ((,) err+ AllocatingRegistersFailed)) liveSets' blocks1 [] accum+ (Prelude.Just ( ssig)) (Prelude.Just ( ssig')) binfo oinfo loops};+ Prelude.Right ssig' ->+ let {+ sd = Allocate.finalizeScanState maxReg ( ssig')+ (Ssrnat.double opCount)}+ in+ let {allocs = Resolve.determineAllocations maxReg sd} in+ let {+ mappings = Resolve.resolveDataFlow maxReg binfo allocs blocks1+ liveSets'}+ in+ case Assign.assignRegNum maxReg binfo oinfo allocs liveSets' mappings+ blocks1 accum of {+ (,) blocks2 accum' -> Build_Details Prelude.Nothing liveSets'+ blocks1 blocks2 accum' (Prelude.Just ( ssig)) (Prelude.Just sd)+ binfo oinfo loops}}}}
LinearScan/Morph.hs view
@@ -40,13 +40,12 @@ type PhysReg = Prelude.Int data SSError =- ECannotSplitSingleton1 Prelude.Int+ ERegistersExhausted Prelude.Int+ | ENoValidSplitPositionUnh Prelude.Int Prelude.Int+ | ENoValidSplitPosition Prelude.Int Prelude.Int+ | ECannotSplitSingleton1 Prelude.Int | ECannotSplitSingleton2 Prelude.Int | ECannotSplitSingleton3 Prelude.Int- | ECannotSplitSingleton4 Prelude.Int- | ECannotSplitSingleton5 Prelude.Int- | ECannotSplitSingleton6 Prelude.Int- | ECannotSplitSingleton7 Prelude.Int | ENoIntervalsToSplit | ERegisterAlreadyAssigned Prelude.Int | ERegisterAssignmentsOverlap Prelude.Int@@ -120,12 +119,6 @@ case _top_assumption_ of { Build_SSInfo x x0 -> _evar_0_ x} -weakenHasLen_ :: Prelude.Int -> ScanState.ScanStateDesc -> SState () () ()-weakenHasLen_ maxReg pre hS =- Prelude.Right ((,) ()- (case hS of {- Build_SSInfo thisDesc0 _ -> Build_SSInfo thisDesc0 __}))- strengthenHasLen :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.ScanStateDesc -> Prelude.Maybe () strengthenHasLen maxReg pre sd =@@ -135,6 +128,21 @@ [] -> _evar_0_ __; (:) x x0 -> _evar_0_0 x x0} +moveUnhandledToHandled :: Prelude.Int -> ScanState.ScanStateDesc -> SState + () () ()+moveUnhandledToHandled maxReg pre x =+ case x of {+ Build_SSInfo thisDesc0 _ ->+ case thisDesc0 of {+ ScanState.Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0+ unhandled0 active0 inactive0 handled0 ->+ case unhandled0 of {+ [] -> Logic.coq_False_rect;+ (:) p unhandled1 -> Prelude.Right ((,) () (Build_SSInfo+ (ScanState.Build_ScanStateDesc nextInterval0 intervals0+ fixedIntervals0 unhandled1 active0 inactive0 ((:) ((,)+ (Prelude.fst p) Prelude.Nothing) handled0)) __))}}}+ moveUnhandledToActive :: Prelude.Int -> ScanState.ScanStateDesc -> PhysReg -> SState () () () moveUnhandledToActive maxReg pre reg x =@@ -176,7 +184,8 @@ (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd)) (Fintype.ordinal_eqType maxReg)) x (unsafeCoerce (ScanState.active maxReg sd))))- (ScanState.inactive maxReg sd) ((:) (unsafeCoerce x)+ (ScanState.inactive maxReg sd) ((:) ((,) (Prelude.fst (unsafeCoerce x))+ (Prelude.Just (Prelude.snd (unsafeCoerce x)))) (ScanState.handled maxReg sd)) moveActiveToInactive :: Prelude.Int -> ScanState.ScanStateDesc ->@@ -222,6 +231,7 @@ (Eqtype.prod_eqType (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd)) (Fintype.ordinal_eqType maxReg)) x- (unsafeCoerce (ScanState.inactive maxReg sd)))) ((:) (unsafeCoerce x)- (ScanState.handled maxReg sd))+ (unsafeCoerce (ScanState.inactive maxReg sd)))) ((:) ((,)+ (Prelude.fst (unsafeCoerce x)) (Prelude.Just+ (Prelude.snd (unsafeCoerce x)))) (ScanState.handled maxReg sd))
LinearScan/NonEmpty0.hs view
@@ -11,6 +11,21 @@ import qualified LinearScan.Utils +coq_NonEmpty_rect :: (a1 -> a2) -> (a1 -> ([] a1) -> a2 -> a2) -> ([] + a1) -> a2+coq_NonEmpty_rect f f0 n =+ (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+ (\y ->+ f y)+ (\y n0 ->+ f0 y n0 (coq_NonEmpty_rect f f0 n0))+ n++coq_NonEmpty_rec :: (a1 -> a2) -> (a1 -> ([] a1) -> a2 -> a2) -> ([] + a1) -> a2+coq_NonEmpty_rec =+ coq_NonEmpty_rect+ coq_NE_from_list :: a1 -> ([] a1) -> [] a1 coq_NE_from_list x xs = case xs of {
− LinearScan/Order.hs
@@ -1,17 +0,0 @@-module LinearScan.Order where---import Debug.Trace (trace, traceShow)-import qualified Prelude-import qualified Data.IntMap-import qualified Data.IntSet-import qualified Data.List-import qualified Data.Ord-import qualified Data.Functor.Identity-import qualified LinearScan.Utils---computeBlockOrder :: ([] a1) -> [] a1-computeBlockOrder blocks =- blocks-
LinearScan/Range.hs view
@@ -54,6 +54,10 @@ case r of { Build_RangeDesc rbeg0 rend0 ups0 -> ups0} +head_or_end :: RangeDesc -> Prelude.Int+head_or_end rd =+ UsePos.head_or (rend rd) (ups rd)+ getRangeDesc :: RangeDesc -> RangeDesc getRangeDesc d = d@@ -62,53 +66,20 @@ packRange d = d -newRange :: UsePos.UsePos -> RangeDesc-newRange upos =- Build_RangeDesc (UsePos.uloc upos) ((Prelude.succ) (UsePos.uloc upos)) ((:)- upos [])+coq_Range_shift :: RangeDesc -> Prelude.Int -> RangeDesc+coq_Range_shift rd b =+ Build_RangeDesc b (rend rd) (ups rd) coq_Range_cons :: UsePos.UsePos -> RangeDesc -> RangeDesc coq_Range_cons upos rd = Build_RangeDesc (rbeg rd) (rend rd) ((:) upos (ups rd)) -type BoundedRange = RangeDesc--emptyBoundedRange :: Prelude.Int -> Prelude.Int -> BoundedRange-emptyBoundedRange b e =- Build_RangeDesc b e []+range_ltn :: RangeDesc -> RangeDesc -> Prelude.Bool+range_ltn x y =+ (Prelude.<=) ((Prelude.succ) (rend ( x))) (rbeg ( y)) type SortedRanges = Specif.Coq_sig2 ([] RangeDesc) -emptySortedRanges :: Prelude.Int -> SortedRanges-emptySortedRanges b =- []--prependRange :: Prelude.Int -> Prelude.Int -> BoundedRange -> SortedRanges ->- Prelude.Int -> SortedRanges-prependRange b e rp ranges pos =- let {_evar_0_ = \_ _ -> (:) rp []} in- let {- _evar_0_0 = \x xs ->- let {- _evar_0_0 = \_ _ ->- let {- r' = packRange (Build_RangeDesc (rbeg (getRangeDesc ( rp)))- (rend (getRangeDesc ( x)))- ((Prelude.++) (ups (getRangeDesc ( rp)))- (ups (getRangeDesc ( x)))))}- in- (:) r' xs}- in- let {_evar_0_1 = \_ _ -> (:) rp ((:) x xs)} in- case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend ( rp)))- (unsafeCoerce (rbeg ( x))) of {- Prelude.True -> _evar_0_0 __ __;- Prelude.False -> _evar_0_1 __ __}}- in- case ranges of {- [] -> _evar_0_ __ __;- (:) x x0 -> _evar_0_0 x x0}- coq_SortedRanges_cat :: Prelude.Int -> SortedRanges -> Prelude.Int -> SortedRanges -> SortedRanges coq_SortedRanges_cat b xs pos ys =@@ -156,9 +127,12 @@ rangesIntersect :: RangeDesc -> RangeDesc -> Prelude.Bool rangesIntersect x y =- case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {- Prelude.True -> (Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x);- Prelude.False -> (Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y)}+ (Prelude.||)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend x))+ (unsafeCoerce (rend y)))+ (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {+ Prelude.True -> (Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x);+ Prelude.False -> (Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y)}) rangeIntersectionPoint :: RangeDesc -> RangeDesc -> Prelude.Maybe Lib.Coq_oddnum@@ -166,8 +140,8 @@ case rangesIntersect x y of { Prelude.True -> Prelude.Just (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {- Prelude.True -> rbeg x;- Prelude.False -> rbeg y});+ Prelude.True -> rbeg y;+ Prelude.False -> rbeg x}); Prelude.False -> Prelude.Nothing} findRangeUsePos :: RangeDesc -> (UsePos.UsePos -> Prelude.Bool) ->@@ -193,54 +167,44 @@ in Datatypes.list_rec _evar_0_ _evar_0_0 (ups (getRangeDesc rd)) -rangeSpan :: Prelude.Int -> RangeDesc ->- ((,) (Prelude.Maybe RangeDesc) (Prelude.Maybe RangeDesc))-rangeSpan before rd =+type SubRangesOf = ((,) RangeDesc RangeDesc)++rangeSpan :: RangeDesc -> Prelude.Int -> SubRangesOf+rangeSpan rd before = (Prelude.flip (Prelude.$)) __ (\_ -> case rd of { Build_RangeDesc rbeg0 rend0 ups0 -> let { _evar_0_ = \l1 l2 -> let {- _evar_0_ = \_ ->- let {- _evar_0_ = \_ -> (,) Prelude.Nothing (Prelude.Just- (packRange (Build_RangeDesc rbeg0 rend0 ((Prelude.++) l1 l2))))}- in+ _evar_0_ = \_ _ -> let {- _evar_0_0 = \_ ->- let {- _evar_0_0 = \_ -> (,) (Prelude.Just- (packRange (Build_RangeDesc rbeg0 rend0 ((Prelude.++) l1 l2))))- Prelude.Nothing}- in- let {- _evar_0_1 = \_ ->- let {- _evar_0_1 = \_ ->- let {- _evar_0_1 = \_ ->- (Prelude.flip (Prelude.$)) __ (\_ ->- (Prelude.flip (Prelude.$)) __ (\_ -> (,) (Prelude.Just- (packRange (Build_RangeDesc rbeg0 before l1)))- (Prelude.Just- (packRange (Build_RangeDesc before rend0 l2)))))}- in- _evar_0_1 __}- in- _evar_0_1 __}- in- case (Prelude.<=) rend0 before of {- Prelude.True -> _evar_0_0 __;- Prelude.False -> _evar_0_1 __}}+ _evar_0_ = let {+ _evar_0_ = let {+ _evar_0_ = \_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (,)+ (packRange (Build_RangeDesc rbeg0+ before l1))+ (packRange (Build_RangeDesc before+ rend0 l2))))}+ in+ _evar_0_}+ in+ _evar_0_} in- case (Prelude.<=) before rbeg0 of {- Prelude.True -> _evar_0_ __;- Prelude.False -> _evar_0_0 __}}+ _evar_0_ __} in- _evar_0_ __}+ _evar_0_ __ __} in- case Lib.span (\x ->- (Prelude.<=) ((Prelude.succ) (UsePos.uloc x)) before) ups0 of {+ case Lib.span (\u ->+ (Prelude.<=) ((Prelude.succ) (UsePos.uloc u)) before) ups0 of { (,) x x0 -> _evar_0_ x x0}})++type BoundedRange = RangeDesc++emptyBoundedRange :: Prelude.Int -> Prelude.Int -> BoundedRange+emptyBoundedRange b e =+ Build_RangeDesc b e []
LinearScan/Resolve.hs view
@@ -16,9 +16,11 @@ import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Graph as Graph import qualified LinearScan.IntMap as IntMap+import qualified LinearScan.Interval as Interval import qualified LinearScan.Lib as Lib import qualified LinearScan.LiveSets as LiveSets import qualified LinearScan.ScanState as ScanState+import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Ssrnat as Ssrnat@@ -35,83 +37,199 @@ unsafeCoerce = IOExts.unsafeCoerce #endif -__ :: any-__ = Prelude.error "Logical or arity value used"+type PhysReg = Prelude.Int -checkIntervalBoundary :: Prelude.Int -> ScanState.ScanStateDesc ->- Prelude.Int -> Prelude.Bool ->- LiveSets.BlockLiveSets -> LiveSets.BlockLiveSets ->- (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) ->- Prelude.Int -> IntMap.IntMap- ((,) Graph.Graph Graph.Graph)-checkIntervalBoundary maxReg sd bid in_from from to mappings vid =+data Allocation =+ Build_Allocation Prelude.Int Interval.IntervalDesc (Prelude.Maybe PhysReg)++intVal :: Prelude.Int -> Allocation -> Interval.IntervalDesc+intVal maxReg a =+ case a of {+ Build_Allocation intId intVal0 intReg0 -> intVal0}++intReg :: Prelude.Int -> Allocation -> Prelude.Maybe PhysReg+intReg maxReg a =+ case a of {+ Build_Allocation intId intVal0 intReg0 -> intReg0}++determineAllocations :: Prelude.Int -> ScanState.ScanStateDesc -> []+ Allocation+determineAllocations maxReg sd =+ Prelude.map (\x -> Build_Allocation ( (Prelude.fst x))+ (Interval.getIntervalDesc+ (+ (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) (Prelude.fst x)))) (Prelude.snd x))+ (ScanState.handled maxReg sd)++type RawResolvingMove = (,) (Prelude.Maybe PhysReg) (Prelude.Maybe PhysReg)++data ResolvingMove =+ Move PhysReg PhysReg+ | Swap PhysReg PhysReg+ | Spill PhysReg Blocks.VarId+ | Restore Blocks.VarId PhysReg+ | Nop++prepareForGraph :: Prelude.Int -> Eqtype.Equality__Coq_sort ->+ RawResolvingMove -> (,)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+prepareForGraph maxReg vid x =+ case x of {+ (,) o o0 ->+ case o of {+ Prelude.Just x0 ->+ case o0 of {+ Prelude.Just y -> (,) (Prelude.Just (unsafeCoerce (Prelude.Left x0)))+ (Prelude.Just (unsafeCoerce (Prelude.Left y)));+ Prelude.Nothing -> (,) (Prelude.Just (unsafeCoerce (Prelude.Left x0)))+ (Prelude.Just (unsafeCoerce (Prelude.Right vid)))};+ Prelude.Nothing ->+ case o0 of {+ Prelude.Just y -> (,) (Prelude.Just+ (unsafeCoerce (Prelude.Right vid))) (Prelude.Just+ (unsafeCoerce (Prelude.Left y)));+ Prelude.Nothing -> (,) (Prelude.Just+ (unsafeCoerce (Prelude.Right vid))) (Prelude.Just+ (unsafeCoerce (Prelude.Right vid)))}}}++moveFromGraph :: Prelude.Int -> ((,)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> ResolvingMove+moveFromGraph maxReg mv =+ case mv of {+ (,) o o0 ->+ case o of {+ Prelude.Just s ->+ case unsafeCoerce s of {+ Prelude.Left x ->+ case o0 of {+ Prelude.Just s0 ->+ case unsafeCoerce s0 of {+ Prelude.Left y -> Move x y;+ Prelude.Right y -> Spill x y};+ Prelude.Nothing -> Nop};+ Prelude.Right x ->+ case o0 of {+ Prelude.Just s0 ->+ case unsafeCoerce s0 of {+ Prelude.Left y -> Restore x y;+ Prelude.Right s1 -> Nop};+ Prelude.Nothing -> Nop}};+ Prelude.Nothing -> Nop}}++determineMoves :: Prelude.Int -> (IntMap.IntMap RawResolvingMove) -> []+ ResolvingMove+determineMoves maxReg moves = let {- mfrom_int = ScanState.lookupInterval maxReg sd __ vid- (LiveSets.blockLastOpId from)}+ graph = Lib.forFold+ (Graph.emptyGraph+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType))+ (unsafeCoerce (IntMap.coq_IntMap_toList moves)) (\g mv ->+ Graph.addEdge+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType)+ (unsafeCoerce+ (prepareForGraph maxReg (Prelude.fst mv) (Prelude.snd mv)))+ g)} in+ Prelude.map (moveFromGraph maxReg)+ (Graph.topsort+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType)+ graph)++resolvingMoves :: Prelude.Int -> ([] Allocation) -> Prelude.Int ->+ Prelude.Int -> IntMap.IntMap RawResolvingMove+resolvingMoves maxReg allocs from to = let {- mto_int = ScanState.lookupInterval maxReg sd __ vid- (LiveSets.blockFirstOpId to)}+ liveAtFrom = IntMap.coq_IntMap_fromList+ (Prelude.map (\i -> (,) (Interval.ivar (intVal maxReg i))+ i)+ (Prelude.filter (\i ->+ (Prelude.&&)+ ((Prelude.<=) (Interval.ibeg (intVal maxReg i)) from)+ ((Prelude.<=) ((Prelude.succ) from)+ (Interval.iend (intVal maxReg i)))) allocs))} in- case Eqtype.eq_op- (Eqtype.option_eqType- (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd)))- (unsafeCoerce mfrom_int) (unsafeCoerce mto_int) of {- Prelude.True -> mappings;- Prelude.False ->+ let {+ liveAtTo = IntMap.coq_IntMap_fromList+ (Prelude.map (\i -> (,) (Interval.ivar (intVal maxReg i)) i)+ (Prelude.filter (\i ->+ let {int = intVal maxReg i} in+ (Prelude.&&) ((Prelude.<=) (Interval.ibeg int) to)+ (case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce to)+ (unsafeCoerce (Interval.iend int)) of {+ Prelude.True ->+ case Interval.lastUsePos int of {+ Prelude.Just u -> (Prelude.<=) to (UsePos.uloc u);+ Prelude.Nothing -> Prelude.False};+ Prelude.False ->+ (Prelude.<=) ((Prelude.succ) to) (Interval.iend int)}))+ allocs))}+ in+ IntMap.coq_IntMap_mergeWithKey (\vid x y ->+ case Eqtype.eq_op (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))+ (unsafeCoerce (intReg maxReg x)) (unsafeCoerce (intReg maxReg y)) of {+ Prelude.True -> Prelude.Nothing;+ Prelude.False -> Prelude.Just ((,) (intReg maxReg x) (intReg maxReg y))})+ (\x -> IntMap.emptyIntMap) (\x -> IntMap.emptyIntMap) liveAtFrom liveAtTo++checkBlockBoundary :: Prelude.Int -> ([] Allocation) -> Prelude.Int ->+ Prelude.Bool -> LiveSets.BlockLiveSets ->+ LiveSets.BlockLiveSets -> IntMap.IntSet ->+ (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) ->+ IntMap.IntMap ((,) Graph.Graph Graph.Graph)+checkBlockBoundary maxReg allocs bid in_from from to liveIn mappings =+ let {+ select = \acc vid x ->+ case IntMap.coq_IntSet_member vid liveIn of {+ Prelude.True -> (:) ((,) vid x) acc;+ Prelude.False -> acc}}+ in+ let {+ moves = IntMap.coq_IntMap_foldlWithKey select []+ (resolvingMoves maxReg allocs (LiveSets.blockLastOpId from)+ (LiveSets.blockFirstOpId to))}+ in+ Lib.forFold mappings (unsafeCoerce moves) (\ms mv -> let {- f = \mi ->- case mi of {- Prelude.Just i ->- case ScanState.lookupRegister maxReg sd __ i of {- Prelude.Just r -> Prelude.Left r;- Prelude.Nothing -> Prelude.Right vid};- Prelude.Nothing -> Prelude.Right vid}}+ addToGraphs = \e xs ->+ case xs of {+ (,) gbeg gend ->+ case in_from of {+ Prelude.True -> (,) gbeg+ (Graph.addEdge+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType) e gend);+ Prelude.False -> (,)+ (Graph.addEdge+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType) e gbeg) gend}}} in- let {sreg = unsafeCoerce f mfrom_int} in- let {dreg = unsafeCoerce f mto_int} in- case Eqtype.eq_op- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType) sreg dreg of {- Prelude.True -> mappings;- Prelude.False ->- let {- addToGraphs = \e xs ->- case xs of {- (,) gbeg gend ->- case in_from of {- Prelude.True -> (,) gbeg- (Graph.addEdge- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType) e gend);- Prelude.False -> (,)- (Graph.addEdge- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType) e gbeg) gend}}}- in- let {- f0 = \mxs ->- let {e = (,) (Prelude.Just sreg) (Prelude.Just dreg)} in- Prelude.Just- (unsafeCoerce addToGraphs e- (case mxs of {- Prelude.Just xs -> xs;- Prelude.Nothing -> (,)- (Graph.emptyGraph- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType))- (Graph.emptyGraph- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType))}))}- in- IntMap.coq_IntMap_alter f0 bid mappings}}+ let {+ f = \mxs ->+ unsafeCoerce addToGraphs+ (prepareForGraph maxReg (Prelude.fst mv) (Prelude.snd mv))+ (case mxs of {+ Prelude.Just xs -> xs;+ Prelude.Nothing -> (,)+ (Graph.emptyGraph+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType))+ (Graph.emptyGraph+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType))})}+ in+ IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms) type BlockMoves = (,) Graph.Graph Graph.Graph -resolveDataFlow :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- ScanState.ScanStateDesc -> ([] a1) -> (IntMap.IntMap+resolveDataFlow :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) -> ([]+ Allocation) -> ([] a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> IntMap.IntMap BlockMoves-resolveDataFlow maxReg binfo sd blocks liveSets =+resolveDataFlow maxReg binfo allocs blocks liveSets = Lib.forFold IntMap.emptyIntMap blocks (\mappings b -> let {bid = Blocks.blockId binfo b} in case IntMap.coq_IntMap_lookup bid liveSets of {@@ -129,8 +247,8 @@ Prelude.True -> bid; Prelude.False -> s_bid}} in- IntMap.coq_IntSet_forFold ms (LiveSets.blockLiveIn to)- (checkIntervalBoundary maxReg sd key in_from from to);+ checkBlockBoundary maxReg allocs key in_from from to+ (LiveSets.blockLiveIn to) ms; Prelude.Nothing -> ms}); Prelude.Nothing -> mappings})
LinearScan/ScanState.hs view
@@ -1,6 +1,3 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}-{- For Hugs, use the option -F"cpp -P -traditional" -}- module LinearScan.ScanState where @@ -15,22 +12,8 @@ import qualified LinearScan.Interval as Interval import qualified LinearScan.Lib as Lib-import qualified LinearScan.Eqtype as Eqtype-import qualified LinearScan.Fintype as Fintype-import qualified LinearScan.Ssrnat as Ssrnat ----unsafeCoerce :: a -> b-#ifdef __GLASGOW_HASKELL__-import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#-#else--- HUGS-import qualified LinearScan.IOExts as IOExts-unsafeCoerce = IOExts.unsafeCoerce-#endif- type PhysReg = Prelude.Int type FixedIntervalsType = [] (Prelude.Maybe Interval.IntervalDesc)@@ -41,7 +24,7 @@ ((,) Prelude.Int PhysReg)) - ([] ((,) Prelude.Int PhysReg))+ ([] ((,) Prelude.Int (Prelude.Maybe PhysReg))) nextInterval :: Prelude.Int -> ScanStateDesc -> Prelude.Int nextInterval maxReg s =@@ -81,7 +64,8 @@ Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0 active0 inactive0 handled0 -> inactive0} -handled :: Prelude.Int -> ScanStateDesc -> [] ((,) IntervalId PhysReg)+handled :: Prelude.Int -> ScanStateDesc -> []+ ((,) IntervalId (Prelude.Maybe PhysReg)) handled maxReg s = case s of { Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0@@ -103,47 +87,6 @@ Prelude.Nothing -> (,) reg Prelude.Nothing}; Prelude.Nothing -> (,) r Prelude.Nothing}}) ((,) ( 0) (Prelude.Just Lib.odd1))--isWithin :: Interval.IntervalDesc -> Prelude.Int -> Prelude.Int ->- Prelude.Bool-isWithin int vid opid =- (Prelude.&&)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Interval.ivar int))- (unsafeCoerce vid))- ((Prelude.&&) ((Prelude.<=) (Interval.ibeg int) opid)- ((Prelude.<=) ((Prelude.succ) opid) (Interval.iend int)))--lookupInterval :: Prelude.Int -> ScanStateDesc -> a1 -> Prelude.Int ->- Prelude.Int -> Prelude.Maybe IntervalId-lookupInterval maxReg sd st vid opid =- let {- f = \idx acc int ->- case acc of {- Prelude.Just x -> Prelude.Just x;- Prelude.Nothing ->- case isWithin ( int) vid opid of {- Prelude.True -> Prelude.Just idx;- Prelude.False -> Prelude.Nothing}}}- in- (LinearScan.Utils.vfoldl'_with_index) (nextInterval maxReg sd) f- Prelude.Nothing (intervals maxReg sd)--lookupRegister :: Prelude.Int -> ScanStateDesc -> a1 ->- Eqtype.Equality__Coq_sort -> Prelude.Maybe PhysReg-lookupRegister maxReg sd st intid =- Lib.forFold Prelude.Nothing- ((Prelude.++) (unsafeCoerce (handled maxReg sd))- ((Prelude.++) (unsafeCoerce (active maxReg sd))- (unsafeCoerce (inactive maxReg sd)))) (\acc x ->- case x of {- (,) xid reg ->- case acc of {- Prelude.Just r -> Prelude.Just r;- Prelude.Nothing ->- case Eqtype.eq_op (Fintype.ordinal_eqType (nextInterval maxReg sd))- xid intid of {- Prelude.True -> Prelude.Just reg;- Prelude.False -> Prelude.Nothing}}}) data ScanStateStatus = Pending
LinearScan/Seq.hs view
@@ -39,6 +39,12 @@ Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Data.List.length s)) (unsafeCoerce 0) +head :: a1 -> ([] a1) -> a1+head x0 s =+ case s of {+ [] -> x0;+ (:) x l -> x}+ rcons :: ([] a1) -> a1 -> [] a1 rcons s z = case s of {@@ -71,6 +77,19 @@ case s of { [] -> _evar_0_; (:) x x0 -> _evar_0_0 x x0}++last_ind :: a2 -> (([] a1) -> a1 -> a2 -> a2) -> ([] a1) -> a2+last_ind hnil hlast s =+ let {+ _evar_0_ = let {_evar_0_ = \s1 hs1 -> hs1} in+ let {+ _evar_0_0 = \x s2 iHs s1 hs1 ->+ let {_evar_0_0 = iHs (rcons s1 x) (hlast s1 x hs1)} in+ _evar_0_0}+ in+ Datatypes.list_rect _evar_0_ _evar_0_0 s [] hnil}+ in+ _evar_0_ find :: (Ssrbool.Coq_pred a1) -> ([] a1) -> Prelude.Int find a s =
LinearScan/Split.hs view
@@ -23,6 +23,7 @@ import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrnat as Ssrnat @@ -43,393 +44,140 @@ data SplitPosition = BeforePos Lib.Coq_oddnum- | BeforeFirstUsePosReqReg- | EndOfLifetimeHole+ | EndOfLifetimeHole Lib.Coq_oddnum -splitPosition :: Interval.IntervalDesc -> SplitPosition -> Prelude.Maybe- Lib.Coq_oddnum+splitPosition :: Interval.IntervalDesc -> SplitPosition -> Lib.Coq_oddnum splitPosition d pos = case pos of {- BeforePos x -> Prelude.Just x;- BeforeFirstUsePosReqReg ->- Interval.firstUseReqReg (Interval.getIntervalDesc d);- EndOfLifetimeHole -> Prelude.Nothing}+ BeforePos n -> n;+ EndOfLifetimeHole n ->+ Interval.afterLifetimeHole (Interval.getIntervalDesc d) n} -splitInterval :: Prelude.Int -> ScanState.ScanStateDesc ->- ScanState.IntervalId -> SplitPosition -> Prelude.Bool ->- Prelude.Either Morph.SSError- (Prelude.Maybe ScanState.ScanStateSig)-splitInterval maxReg sd uid pos forCurrent =+splitUnhandledInterval :: Prelude.Int -> ScanState.ScanStateDesc ->+ ScanState.IntervalId -> Prelude.Int -> ([]+ ((,) ScanState.IntervalId Prelude.Int)) ->+ SplitPosition -> Prelude.Either Morph.SSError+ (Prelude.Maybe ScanState.ScanStateSig)+splitUnhandledInterval maxReg sd uid beg us pos = let {- _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 ->- let {- _evar_0_ = \uid1 -> Prelude.Left (Morph.ECannotSplitSingleton1 ( uid1))}- in+ _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 ->+ let {int = LinearScan.Utils.nth _nextInterval_ ints uid0} in+ let {splitPos = splitPosition ( int) pos} in let {- _evar_0_0 = \_top_assumption_ ->+ _evar_0_ = \_ -> let {- _evar_0_0 = \u beg us uid1 ->- let {int = LinearScan.Utils.nth _nextInterval_ ints uid1} in+ _evar_0_ = \iv ib ie rds -> let {- _evar_0_0 = \_top_assumption_0 ->+ _top_assumption_ = Interval.splitInterval+ (Interval.Build_IntervalDesc iv ib ie rds)+ splitPos}+ in+ let {+ _evar_0_ = \i0 i1 -> let {- _evar_0_0 = \_ ->- (Prelude.flip (Prelude.$)) __ (\_ ->- let {- _evar_0_0 = \iv ib ie _iknd_ rds ->- let {- _top_assumption_1 = Interval.intervalSpan rds- _top_assumption_0 iv ib ie _iknd_}- in- let {- _evar_0_0 = \_top_assumption_2 ->- let {- _evar_0_0 = \_top_assumption_3 _top_assumption_4 ->- let {- _evar_0_0 = \_top_assumption_5 ->- let {- _evar_0_0 = \_ ->+ _evar_0_ = let {+ _evar_0_ = \_ _ -> let {- _evar_0_0 = \_ ->- let {- set_int_desc = ScanState.Build_ScanStateDesc- _nextInterval_- (LinearScan.Utils.set_nth _nextInterval_ ints- uid1 _top_assumption_3) _fixedIntervals_ ((:)- ((,) u beg) us) _active_ _inactive_ _handled_}- in- let {- _evar_0_0 = \_ ->- (Prelude.flip (Prelude.$)) __- (let {- new_unhandled = ScanState.Build_ScanStateDesc- ((Prelude.succ) _nextInterval_)- (LinearScan.Utils.snoc _nextInterval_- (LinearScan.Utils.set_nth _nextInterval_- ints uid1 _top_assumption_3)- _top_assumption_5) _fixedIntervals_- (Lib.insert (Lib.lebf Prelude.snd) ((,)- ( _nextInterval_)- (Interval.ibeg _top_assumption_5)) ((:)- (Prelude.id ((,) u beg))- (Prelude.map Prelude.id us)))- (Prelude.map Prelude.id _active_)- (Prelude.map Prelude.id _inactive_)- (Prelude.map Prelude.id _handled_)}- in- \_ -> Prelude.Right (Prelude.Just- (ScanState.packScanState maxReg- ScanState.InUse new_unhandled)))}- in- let {- _evar_0_1 = \_ ->- let {- _evar_0_1 = \_top_assumption_6 ->- let {- _evar_0_1 = \_ ->- let {- _evar_0_1 = \iv1 ib1 ie1 _iknd1_ rds1 ->- let {- _top_assumption_7 = Interval.intervalSpan- rds1- _top_assumption_6- iv1 ib1 ie1 _iknd1_}- in- let {- _evar_0_1 = \_top_assumption_8 ->- let {- _evar_0_1 = \_top_assumption_9 _top_assumption_10 ->- let {- _evar_0_1 = \_top_assumption_11 ->- (Prelude.flip (Prelude.$)) __- (let {- new_unhandled = ScanState.Build_ScanStateDesc- ((Prelude.succ) _nextInterval_)- (LinearScan.Utils.snoc- _nextInterval_- (LinearScan.Utils.set_nth- _nextInterval_ ints uid1- _top_assumption_3)- _top_assumption_11)- _fixedIntervals_- (Lib.insert- (Lib.lebf Prelude.snd) ((,)- ( _nextInterval_)- (Interval.ibeg- _top_assumption_11)) ((:)- (Prelude.id ((,) u beg))- (Prelude.map Prelude.id us)))- (Prelude.map Prelude.id- _active_)- (Prelude.map Prelude.id- _inactive_)- (Prelude.map Prelude.id- _handled_)}- in- let {- _evar_0_1 = \_ _ -> Prelude.Right- (Prelude.Just- (ScanState.packScanState maxReg- ScanState.InUse new_unhandled))}- in- let {- _evar_0_2 = \_ _ -> Prelude.Left- (Morph.ECannotSplitSingleton3- ( uid1))}- in- case (Prelude.<=) ((Prelude.succ)- beg)- (Interval.ibeg- _top_assumption_11) of {- Prelude.True -> _evar_0_1 __;- Prelude.False -> _evar_0_2 __})}- in- let {- _evar_0_2 = \_ -> Prelude.Right- (Prelude.Just- (ScanState.packScanState maxReg- ScanState.InUse set_int_desc))}- in- case _top_assumption_10 of {- Prelude.Just x -> (\_ -> _evar_0_1 x);- Prelude.Nothing -> _evar_0_2}}- in- let {- _evar_0_2 = \_top_assumption_9 ->- let {- _evar_0_2 = \_top_assumption_10 ->- (Prelude.flip (Prelude.$)) __- (let {- new_unhandled = ScanState.Build_ScanStateDesc- ((Prelude.succ) _nextInterval_)- (LinearScan.Utils.snoc- _nextInterval_- (LinearScan.Utils.set_nth- _nextInterval_ ints uid1- _top_assumption_3)- _top_assumption_10)- _fixedIntervals_- (Lib.insert- (Lib.lebf Prelude.snd) ((,)- ( _nextInterval_)- (Interval.ibeg- _top_assumption_10)) ((:)- (Prelude.id ((,) u beg))- (Prelude.map Prelude.id us)))- (Prelude.map Prelude.id- _active_)- (Prelude.map Prelude.id- _inactive_)- (Prelude.map Prelude.id- _handled_)}- in- let {- _evar_0_2 = \_ _ -> Prelude.Right- (Prelude.Just- (ScanState.packScanState maxReg- ScanState.InUse new_unhandled))}- in- let {- _evar_0_3 = \_ _ -> Prelude.Left- (Morph.ECannotSplitSingleton3- ( uid1))}- in- case (Prelude.<=) ((Prelude.succ)- beg)- (Interval.ibeg- _top_assumption_10) of {- Prelude.True -> _evar_0_2 __;- Prelude.False -> _evar_0_3 __})}- in- let {- _evar_0_3 = \_ ->- Logic.coq_False_rect}- in- case _top_assumption_9 of {- Prelude.Just x -> (\_ -> _evar_0_2 x);- Prelude.Nothing -> _evar_0_3}}- in- case _top_assumption_8 of {- Prelude.Just x -> _evar_0_1 x;- Prelude.Nothing -> _evar_0_2}}- in- case _top_assumption_7 of {- (,) x x0 -> _evar_0_1 x x0 __}}- in- case _top_assumption_5 of {- Interval.Build_IntervalDesc x x0 x1 x2 x3 ->- _evar_0_1 x x0 x1 x2 x3}}- in- let {- _evar_0_2 = \_ -> Prelude.Left- (Morph.ECannotSplitSingleton2 ( uid1))}- in- case (Prelude.&&)- ((Prelude.<=) ((Prelude.succ)- (Interval.ibeg _top_assumption_5))- _top_assumption_6)- ((Prelude.<=) ((Prelude.succ)- _top_assumption_6)- (Interval.iend _top_assumption_5)) of {- Prelude.True -> _evar_0_1 __;- Prelude.False -> _evar_0_2 __}}- in+ _evar_0_ = \_discharged_uid_ _discharged_us_ ->+ Logic.coq_False_rect}+ in+ let {+ _evar_0_0 = \x xs uid1 us1 ->+ (Prelude.flip (Prelude.$)) __ (\_ -> let {- _evar_0_2 = Prelude.Right (Prelude.Just- (ScanState.packScanState maxReg ScanState.InUse- set_int_desc))}+ _evar_0_0 = \_ ->+ (Prelude.flip (Prelude.$)) __+ (let {+ _evar_0_0 = let {+ _evar_0_0 = (Prelude.flip (Prelude.$))+ __ (\_ _ ->+ Prelude.Right+ (Prelude.Just+ (ScanState.packScanState+ maxReg+ ScanState.InUse+ (ScanState.Build_ScanStateDesc+ ((Prelude.succ)+ _nextInterval_)+ (LinearScan.Utils.snoc+ _nextInterval_+ (LinearScan.Utils.set_nth+ _nextInterval_+ ints uid1+ ( i0))+ ( i1))+ _fixedIntervals_+ (Lib.insert+ (Lib.lebf+ Prelude.snd)+ ((,)+ (+ _nextInterval_)+ (Interval.ibeg+ ( i1)))+ ((:)+ (Prelude.id+ ((,) uid1+ beg))+ (Prelude.map+ Prelude.id+ us1)))+ (Prelude.map+ Prelude.id+ _active_)+ (Prelude.map+ Prelude.id+ _inactive_)+ (Prelude.map+ Prelude.id+ _handled_)))))}+ in+ _evar_0_0}+ in+ _evar_0_0)} in- case splitPosition _top_assumption_5- BeforeFirstUsePosReqReg of {- Prelude.Just x -> _evar_0_1 x;- Prelude.Nothing -> _evar_0_2}}- in- case (Prelude.<=) ((Prelude.succ) beg)- (Interval.ibeg _top_assumption_5) of {- Prelude.True -> _evar_0_0 __;- Prelude.False -> _evar_0_1 __}}+ _evar_0_0 __)} in- _evar_0_0 __}- in- _evar_0_0 __}- in- let {- _evar_0_1 = \_ ->- let {- _evar_0_1 = Prelude.Left (Morph.ECannotSplitSingleton4- ( uid1))}- in- let {- _evar_0_2 = let {- _evar_0_2 = \_ ->- let {- _evar_0_2 = \_ ->- let {- set_int_desc = ScanState.Build_ScanStateDesc- _nextInterval_- (LinearScan.Utils.set_nth- _nextInterval_ ints uid1- _top_assumption_3)- _fixedIntervals_ ((:) ((,) u beg)- us) _active_ _inactive_ _handled_}- in- Prelude.Right (Prelude.Just- (ScanState.packScanState maxReg- ScanState.InUse set_int_desc))}- in- _evar_0_2 __}- in- _evar_0_2 __}- in- case forCurrent of {- Prelude.True -> _evar_0_1;- Prelude.False -> _evar_0_2}}- in- case _top_assumption_4 of {- Prelude.Just x -> (\_ -> _evar_0_0 x);- Prelude.Nothing -> _evar_0_1}}- in- let {- _evar_0_1 = \_top_assumption_3 ->- let {- _evar_0_1 = \_top_assumption_4 ->- let {- _evar_0_1 = \_ ->- (Prelude.flip (Prelude.$)) __- (let {- new_unhandled = ScanState.Build_ScanStateDesc- ((Prelude.succ) _nextInterval_)- (LinearScan.Utils.snoc _nextInterval_ ints- _top_assumption_4) _fixedIntervals_- (Lib.insert (Lib.lebf Prelude.snd) ((,)- ( _nextInterval_)- (Interval.ibeg _top_assumption_4)) ((:)- (Prelude.id ((,) u beg))- (Prelude.map Prelude.id us)))- (Prelude.map Prelude.id _active_)- (Prelude.map Prelude.id _inactive_)- (Prelude.map Prelude.id _handled_)}- in- \_ -> Prelude.Right (Prelude.Just- (ScanState.packScanState maxReg ScanState.InUse- new_unhandled)))}- in- let {- _evar_0_2 = \_ -> Prelude.Left- (Morph.ECannotSplitSingleton5 ( uid1))}+ case unh of {+ [] -> _evar_0_ uid0 us0;+ (:) x x0 -> _evar_0_0 x x0 uid0 us0}} in- case (Prelude.<=) ((Prelude.succ) beg)- (Interval.ibeg _top_assumption_4) of {- Prelude.True -> _evar_0_1 __;- Prelude.False -> _evar_0_2 __}}- in- let {_evar_0_2 = \_ -> Logic.coq_False_rect} in- case _top_assumption_3 of {- Prelude.Just x -> (\_ -> _evar_0_1 x);- Prelude.Nothing -> _evar_0_2}}- in- case _top_assumption_2 of {- Prelude.Just x -> _evar_0_0 x;- Prelude.Nothing -> _evar_0_1}}- in- case _top_assumption_1 of {- (,) x x0 -> _evar_0_0 x x0 __}}- in- case int of {- Interval.Build_IntervalDesc x x0 x1 x2 x3 ->- _evar_0_0 x x0 x1 x2 x3})}- in- let {- _evar_0_1 = \_ -> Prelude.Left (Morph.ECannotSplitSingleton2- ( uid1))}+ _evar_0_ __} in- case (Prelude.&&)- ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int)))- _top_assumption_0)- ((Prelude.<=) ((Prelude.succ) _top_assumption_0)- (Interval.iend ( int))) of {- Prelude.True -> _evar_0_0 __;- Prelude.False -> _evar_0_1 __}}+ _evar_0_ __} in- let {_evar_0_1 = Prelude.Right Prelude.Nothing} in- case splitPosition ( int) pos of {- Prelude.Just x -> _evar_0_0 x;- Prelude.Nothing -> _evar_0_1}}+ case _top_assumption_ of {+ (,) x x0 -> _evar_0_ x x0}} in- (\us _ uid1 ->- case _top_assumption_ of {- (,) x x0 -> _evar_0_0 x x0 us uid1})}+ case int of {+ Interval.Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}} in- case unh of {- [] -> _evar_0_ uid0;- (:) x x0 -> _evar_0_0 x x0 __ uid0}}+ let {+ _evar_0_0 = \_ -> Prelude.Left (Morph.ENoValidSplitPositionUnh ( uid0)+ splitPos)}+ in+ case (Prelude.&&)+ ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int))) splitPos)+ ((Prelude.<=) splitPos (Interval.iend ( int))) of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}} in case sd of { ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->- _evar_0_ x x0 x1 x2 x3 x4 x5 uid}+ _evar_0_ x x0 x1 x2 x3 x4 x5 uid us} splitCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc -> SplitPosition -> Morph.SState () () () splitCurrentInterval maxReg pre pos ssi = let { _evar_0_ = \desc ->+ let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in let {- _evar_0_ = \_nextInterval_ intervals0 _fixedIntervals_ unhandled0 _active_ _inactive_ _handled_ ->- let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in+ _evar_0_0 = \_top_assumption_ -> let {- _evar_0_0 = \_top_assumption_ ->+ _evar_0_0 = \uid beg us -> let {- _evar_0_0 = \uid beg us ->- let {- desc0 = ScanState.Build_ScanStateDesc _nextInterval_ intervals0- _fixedIntervals_ ((:) ((,) uid beg) us) _active_ _inactive_- _handled_}- in- (\_ _ _ _ ->- let {- _top_assumption_0 = splitInterval maxReg desc0 uid pos- Prelude.True}- in+ _evar_0_0 = \_nextInterval_ intervals0 _fixedIntervals_ unhandled0 _active_ _inactive_ _handled_ uid0 us0 _top_assumption_0 -> let {_evar_0_0 = \err -> Prelude.Left err} in let { _evar_0_1 = \_top_assumption_1 ->@@ -438,7 +186,7 @@ (Morph.Build_SSInfo _top_assumption_2 __))} in let {- _evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton6 ( uid))}+ _evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton1 ( uid0))} in case _top_assumption_1 of { Prelude.Just x -> _evar_0_1 x;@@ -446,23 +194,218 @@ in case _top_assumption_0 of { Prelude.Left x -> _evar_0_0 x;- Prelude.Right x -> _evar_0_1 x})}+ Prelude.Right x -> _evar_0_1 x}} in- (\us _ ->- case _top_assumption_ of {- (,) x x0 -> _evar_0_0 x x0 us})}+ case desc of {+ ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->+ _evar_0_0 x x0 x1 x2 x3 x4 x5 uid us+ (splitUnhandledInterval maxReg desc uid beg us pos)}} in- case unhandled0 of {- [] -> _evar_0_ __;- (:) x x0 -> _evar_0_0 x x0 __}}+ (\us _ _ _ _ _ ->+ case _top_assumption_ of {+ (,) x x0 -> _evar_0_0 x x0 us})} in- case desc of {- ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->- _evar_0_ x x0 x1 x2 x3 x4 x5 __ __ __}}+ case ScanState.unhandled maxReg desc of {+ [] -> _evar_0_ __ __ __ __;+ (:) x x0 -> _evar_0_0 x x0 __ __ __ __}} in case ssi of { Morph.Build_SSInfo x x0 -> _evar_0_ x __} +splitActiveOrInactiveInterval :: Prelude.Int -> ScanState.ScanStateDesc ->+ ScanState.IntervalId -> Prelude.Int -> ([]+ ((,) ScanState.IntervalId Prelude.Int)) ->+ ScanState.IntervalId -> SplitPosition ->+ Prelude.Either Morph.SSError+ (Prelude.Maybe ScanState.ScanStateSig)+splitActiveOrInactiveInterval maxReg sd uid beg us xid pos =+ let {+ _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 xid0 ->+ let {int = LinearScan.Utils.nth _nextInterval_ ints xid0} in+ let {splitPos = splitPosition ( int) pos} in+ let {+ _evar_0_ = \_ ->+ let {+ _evar_0_ = \iv ib ie rds ->+ let {+ _top_assumption_ = Interval.splitInterval+ (Interval.Build_IntervalDesc iv ib ie rds)+ splitPos}+ in+ let {+ _evar_0_ = \i0 i1 ->+ let {+ _evar_0_ = let {+ _evar_0_ = \_ _ ->+ let {+ _evar_0_ = \_top_assumption_0 ->+ let {+ _evar_0_ = \_ ->+ (Prelude.flip (Prelude.$)) __+ (let {+ _evar_0_ = let {+ _evar_0_ = \_ _ -> Prelude.Left+ (Morph.ENoValidSplitPosition+ ( xid0) _top_assumption_0)}+ in+ let {+ _evar_0_0 = \_ ->+ let {+ _evar_0_0 = \_ _ ->+ Prelude.Right (Prelude.Just+ (ScanState.packScanState+ maxReg ScanState.InUse+ (ScanState.Build_ScanStateDesc+ ((Prelude.succ)+ _nextInterval_)+ (LinearScan.Utils.snoc+ _nextInterval_+ (LinearScan.Utils.set_nth+ _nextInterval_ ints xid0+ ( i0)) ( i1))+ _fixedIntervals_+ (Lib.insert+ (Lib.lebf Prelude.snd)+ ((,) ( _nextInterval_)+ (Interval.ibeg ( i1)))+ ((:)+ (Prelude.id ((,) uid0+ beg))+ (Prelude.map Prelude.id+ us0)))+ (Prelude.map Prelude.id+ _active_)+ (Prelude.map Prelude.id+ _inactive_)+ (Prelude.map Prelude.id+ _handled_))))}+ in+ _evar_0_0 __}+ in+ case (Prelude.<=)+ (Interval.ibeg ( i1)) beg of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}}+ in+ _evar_0_)}+ in+ let {+ _evar_0_0 = \_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ _top_assumption_1 = Interval.splitInterval+ ( i1) _top_assumption_0}+ in+ let {+ _evar_0_0 = \i1_0 i1_1 ->+ (Prelude.flip (Prelude.$)) __+ (let {+ _evar_0_0 = (Prelude.flip (Prelude.$)) __+ (\_ _ -> Prelude.Right+ (Prelude.Just+ (ScanState.packScanState+ maxReg ScanState.InUse+ (ScanState.Build_ScanStateDesc+ ((Prelude.succ)+ ((Prelude.succ)+ _nextInterval_))+ (LinearScan.Utils.snoc+ ((Prelude.succ)+ _nextInterval_)+ (LinearScan.Utils.snoc+ _nextInterval_+ (LinearScan.Utils.set_nth+ _nextInterval_ ints+ xid0 ( i0))+ ( i1_1)) ( i1_0))+ _fixedIntervals_+ (Prelude.map Prelude.id+ (Lib.insert+ (Lib.lebf+ Prelude.snd) ((,)+ ( _nextInterval_)+ (Interval.ibeg+ ( i1_1))) ((:)+ (Prelude.id ((,) uid0+ beg))+ (Prelude.map+ Prelude.id us0))))+ (Prelude.map Prelude.id+ (Prelude.map Prelude.id+ _active_))+ (Prelude.map Prelude.id+ (Prelude.map Prelude.id+ _inactive_)) ((:)+ ((,)+ ( ((Prelude.succ)+ _nextInterval_))+ Prelude.Nothing)+ (Prelude.map Prelude.id+ (Prelude.map Prelude.id+ _handled_)))))))}+ in+ _evar_0_0)}+ in+ case _top_assumption_1 of {+ (,) x x0 -> _evar_0_0 x x0})}+ in+ case Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce (Interval.ibeg ( i1)))+ (unsafeCoerce _top_assumption_0) of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}}+ in+ let {+ _evar_0_0 = let {+ _evar_0_0 = \_ -> Prelude.Right+ (Prelude.Just+ (ScanState.packScanState maxReg+ ScanState.InUse+ (ScanState.Build_ScanStateDesc+ ((Prelude.succ) _nextInterval_)+ (LinearScan.Utils.snoc+ _nextInterval_+ (LinearScan.Utils.set_nth+ _nextInterval_ ints xid0 + ( i0)) ( i1)) _fixedIntervals_+ ((:) (Prelude.id ((,) uid0 beg))+ (Prelude.map Prelude.id us0))+ (Prelude.map Prelude.id _active_)+ (Prelude.map Prelude.id _inactive_)+ ((:) ((,) ( _nextInterval_)+ Prelude.Nothing)+ (Prelude.map Prelude.id _handled_)))))}+ in+ _evar_0_0 __}+ in+ case Interval.firstUseReqReg ( i1) of {+ Prelude.Just x -> _evar_0_ x;+ Prelude.Nothing -> _evar_0_0}}+ in+ _evar_0_ __}+ in+ _evar_0_ __}+ in+ case _top_assumption_ of {+ (,) x x0 -> _evar_0_ x x0}}+ in+ case int of {+ Interval.Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}}+ in+ let {+ _evar_0_0 = \_ -> Prelude.Left (Morph.ENoValidSplitPosition ( xid0)+ splitPos)}+ in+ case (Prelude.&&)+ ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int))) splitPos)+ ((Prelude.<=) splitPos (Interval.iend ( int))) of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}}+ in+ case sd of {+ ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->+ _evar_0_ x x0 x1 x2 x3 x4 x5 uid us xid}+ splitAssignedIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc -> PhysReg -> SplitPosition -> Prelude.Bool -> Morph.SState () () ()@@ -483,84 +426,140 @@ intlist)} in (Prelude.flip (Prelude.$)) __ (\_ ->+ let {_evar_0_ = \intlist0 intids0 -> Logic.coq_False_rect} in let {- _evar_0_ = \_nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ intlist0 intids0 ->- let {- desc0 = ScanState.Build_ScanStateDesc _nextInterval_ intervals0- _fixedIntervals_ _unhandled_ active0 inactive0 _handled_}- in- (\_ _ _ _ ->- let {_evar_0_ = \_ -> Prelude.Left Morph.ENoIntervalsToSplit} in+ _evar_0_0 = \_top_assumption_ -> let {- _evar_0_0 = \aid aids iHaids ->- let {- _top_assumption_ = splitInterval maxReg desc0 aid pos- Prelude.False}- in- let {_evar_0_0 = \err -> Prelude.Left err} in+ _evar_0_0 = \uid beg us -> let {- _evar_0_1 = \_top_assumption_0 ->+ _evar_0_0 = \_nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ uid0 us0 intlist0 intids0 -> let {- _evar_0_1 = \_top_assumption_1 -> Prelude.Right ((,) ()- (let {- _evar_0_1 = \_ ->- (Prelude.flip (Prelude.$)) __- (let {- act_to_inact = ScanState.Build_ScanStateDesc- (ScanState.nextInterval maxReg _top_assumption_1)- (ScanState.intervals maxReg _top_assumption_1)- (ScanState.fixedIntervals maxReg _top_assumption_1)- (ScanState.unhandled maxReg _top_assumption_1)- (unsafeCoerce- (Seq.rem- (Eqtype.prod_eqType- (Fintype.ordinal_eqType- (ScanState.nextInterval maxReg- _top_assumption_1))- (Fintype.ordinal_eqType maxReg))- (unsafeCoerce ((,) ( aid) reg))- (unsafeCoerce- (ScanState.active maxReg _top_assumption_1))))- ((:) ((,) ( aid) reg)- (ScanState.inactive maxReg _top_assumption_1))- (ScanState.handled maxReg _top_assumption_1)}- in- \_ -> Morph.Build_SSInfo act_to_inact __)}- in- let {- _evar_0_2 = \_ -> Morph.Build_SSInfo _top_assumption_1 __}- in- case Ssrbool.in_mem (unsafeCoerce ((,) ( aid) reg))- (Ssrbool.mem- (Seq.seq_predType- (Eqtype.prod_eqType- (Fintype.ordinal_eqType- (ScanState.nextInterval maxReg- _top_assumption_1))- (Fintype.ordinal_eqType maxReg)))- (unsafeCoerce- (ScanState.active maxReg _top_assumption_1))) of {- Prelude.True -> _evar_0_1 __;- Prelude.False -> _evar_0_2 __}))}+ _evar_0_0 = \_ -> Prelude.Right ((,) () (Morph.Build_SSInfo+ (ScanState.Build_ScanStateDesc _nextInterval_ intervals0+ _fixedIntervals_ _unhandled_ active0 inactive0 _handled_)+ __))} in let {- _evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton7- ( aid))}+ _evar_0_1 = \aid aids iHaids ->+ let {+ _evar_0_1 = \_ ->+ let {+ _top_assumption_0 = \x x0 x1 x2 x3 ->+ splitActiveOrInactiveInterval maxReg+ (ScanState.Build_ScanStateDesc _nextInterval_+ intervals0 _fixedIntervals_ _unhandled_ active0+ inactive0 _handled_) x x0 x1 x2 x3}+ in+ let {+ _top_assumption_1 = _top_assumption_0 uid0 beg us0 aid pos}+ in+ let {_evar_0_1 = \err -> Prelude.Left err} in+ let {+ _evar_0_2 = \_top_assumption_2 ->+ let {+ _evar_0_2 = \_top_assumption_3 -> Prelude.Right ((,) ()+ (let {+ _evar_0_2 = \_ ->+ (Prelude.flip (Prelude.$)) __+ (let {+ act_to_inact = ScanState.Build_ScanStateDesc+ (ScanState.nextInterval maxReg+ _top_assumption_3)+ (ScanState.intervals maxReg _top_assumption_3)+ (ScanState.fixedIntervals maxReg+ _top_assumption_3)+ (ScanState.unhandled maxReg _top_assumption_3)+ (unsafeCoerce+ (Seq.rem+ (Eqtype.prod_eqType+ (Fintype.ordinal_eqType+ (ScanState.nextInterval maxReg+ _top_assumption_3))+ (Fintype.ordinal_eqType maxReg))+ (unsafeCoerce ((,) ( aid) reg))+ (unsafeCoerce+ (ScanState.active maxReg+ _top_assumption_3)))) ((:) ((,) + ( aid) reg)+ (ScanState.inactive maxReg _top_assumption_3))+ (ScanState.handled maxReg _top_assumption_3)}+ in+ \_ ->+ let {+ _evar_0_2 = \_ -> Morph.Build_SSInfo+ act_to_inact __}+ in+ _evar_0_2 __)}+ in+ let {+ _evar_0_3 = \_ ->+ let {+ _evar_0_3 = \_ -> Morph.Build_SSInfo+ _top_assumption_3 __}+ in+ _evar_0_3 __}+ in+ case Ssrbool.in_mem (unsafeCoerce ((,) ( aid) reg))+ (Ssrbool.mem+ (Seq.seq_predType+ (Eqtype.prod_eqType+ (Fintype.ordinal_eqType+ (ScanState.nextInterval maxReg+ _top_assumption_3))+ (Fintype.ordinal_eqType maxReg)))+ (unsafeCoerce+ (ScanState.active maxReg _top_assumption_3))) of {+ Prelude.True -> _evar_0_2 __;+ Prelude.False -> _evar_0_3 __}))}+ in+ let {+ _evar_0_3 = Prelude.Left (Morph.ECannotSplitSingleton3+ ( aid))}+ in+ case _top_assumption_2 of {+ Prelude.Just x -> _evar_0_2 x;+ Prelude.Nothing -> _evar_0_3}}+ in+ case _top_assumption_1 of {+ Prelude.Left x -> _evar_0_1 x;+ Prelude.Right x -> _evar_0_2 x}}+ in+ let {+ _evar_0_2 = \_ -> Prelude.Left (Morph.ECannotSplitSingleton2+ ( aid))}+ in+ case (Prelude.<=) beg+ (+ (splitPosition+ (+ (LinearScan.Utils.nth+ (ScanState.nextInterval maxReg+ (ScanState.Build_ScanStateDesc+ _nextInterval_ intervals0 _fixedIntervals_+ _unhandled_ active0 inactive0 _handled_))+ (ScanState.intervals maxReg+ (ScanState.Build_ScanStateDesc+ _nextInterval_ intervals0 _fixedIntervals_+ _unhandled_ active0 inactive0 _handled_))+ aid)) pos)) of {+ Prelude.True -> _evar_0_1 __;+ Prelude.False -> _evar_0_2 __}} in- case _top_assumption_0 of {- Prelude.Just x -> _evar_0_1 x;- Prelude.Nothing -> _evar_0_2}}+ Datatypes.list_rect _evar_0_0 (\aid aids iHaids _ ->+ _evar_0_1 aid aids iHaids) intids0 __} in- case _top_assumption_ of {- Prelude.Left x -> _evar_0_0 x;- Prelude.Right x -> _evar_0_1 x}}+ (\intlist0 _ intids0 _ _ _ _ _ ->+ case desc of {+ ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->+ _evar_0_0 x x0 x1 x2 x3 x4 x5 uid us intlist0 intids0})} in- Datatypes.list_rect _evar_0_ (\aid aids iHaids _ ->- _evar_0_0 aid aids iHaids) intids0 __)}+ (\us _ ->+ case _top_assumption_ of {+ (,) x x0 -> _evar_0_0 x x0 us})} in- case desc of {- ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->- _evar_0_ x x0 x1 x2 x3 x4 x5 intlist intids})) __ __ __}+ case ScanState.unhandled maxReg desc of {+ [] -> (\_ _ _ _ -> _evar_0_ intlist intids);+ (:) x x0 -> _evar_0_0 x x0 __ intlist __ intids __})) __ __ __} in case ssi of { Morph.Build_SSInfo x x0 -> _evar_0_ x __}@@ -572,11 +571,12 @@ splitAssignedIntervalForReg maxReg pre reg (BeforePos pos) Prelude.True splitAnyInactiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->- PhysReg -> Morph.SState () () ()-splitAnyInactiveIntervalForReg maxReg pre reg ss =+ PhysReg -> Lib.Coq_oddnum -> Morph.SState+ () () ()+splitAnyInactiveIntervalForReg maxReg pre reg pos ss = (Prelude.flip (Prelude.$)) (\s ->- splitAssignedIntervalForReg maxReg s reg EndOfLifetimeHole Prelude.False)- (\_top_assumption_ ->+ splitAssignedIntervalForReg maxReg s reg (EndOfLifetimeHole pos)+ Prelude.False) (\_top_assumption_ -> let {_top_assumption_0 = _top_assumption_ pre ss} in let {_evar_0_ = \err -> Prelude.Right ((,) () ss)} in let {
LinearScan/State.hs view
@@ -17,6 +17,10 @@ get i = (,) i i +gets :: (a1 -> a2) -> State a1 a2+gets f s =+ (,) (f s) s+ put :: a1 -> State a1 () put x x0 = (,) () x@@ -60,15 +64,25 @@ [] -> pure []; (:) x xs -> liftA2 (\x0 x1 -> (:) x0 x1) (f x) (mapM f xs)} -foldM :: (a2 -> a3 -> State a1 a2) -> a2 -> ([] a3) -> State a1 a2-foldM f s l =+mapM_ :: (a2 -> State a1 a3) -> ([] a2) -> State a1 ()+mapM_ f l = case l of {+ [] -> pure ();+ (:) x xs -> bind (\x0 -> mapM_ f xs) (f x)}++forM_ :: ([] a2) -> (a2 -> State a1 a3) -> State a1 ()+forM_ l f =+ mapM_ f l++foldrM :: (a3 -> a2 -> State a1 a2) -> a2 -> ([] a3) -> State a1 a2+foldrM f s l =+ case l of { [] -> pure s;- (:) y ys -> bind (\x -> foldM f x ys) (f s y)}+ (:) y ys -> bind (f y) (foldrM f s ys)} -forFoldM :: a2 -> ([] a3) -> (a2 -> a3 -> State a1 a2) -> State a1 a2-forFoldM s l f =- foldM f s l+forFoldrM :: a2 -> ([] a3) -> (a3 -> a2 -> State a1 a2) -> State a1 a2+forFoldrM s l f =+ foldrM f s l concat :: ([] ([] a1)) -> [] a1 concat l =
LinearScan/UsePos.hs view
@@ -1,3 +1,6 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}+ module LinearScan.UsePos where @@ -10,17 +13,108 @@ import qualified Data.Functor.Identity import qualified LinearScan.Utils +import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrbool as Ssrbool +++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++data VarKind =+ Input+ | Temp+ | Output++eqVarKind :: VarKind -> VarKind -> Prelude.Bool+eqVarKind s1 s2 =+ case s1 of {+ Input ->+ case s2 of {+ Input -> Prelude.True;+ _ -> Prelude.False};+ Temp ->+ case s2 of {+ Temp -> Prelude.True;+ _ -> Prelude.False};+ Output ->+ case s2 of {+ Output -> Prelude.True;+ _ -> Prelude.False}}++eqVarKindP :: Eqtype.Equality__Coq_axiom VarKind+eqVarKindP b1 b2 =+ let {+ _evar_0_ = let {_evar_0_ = Ssrbool.ReflectT} in+ let {_evar_0_0 = Ssrbool.ReflectF} in+ let {_evar_0_1 = Ssrbool.ReflectF} in+ case b2 of {+ Input -> _evar_0_;+ Temp -> _evar_0_0;+ Output -> _evar_0_1}}+ in+ let {+ _evar_0_0 = let {_evar_0_0 = Ssrbool.ReflectF} in+ let {_evar_0_1 = Ssrbool.ReflectT} in+ let {_evar_0_2 = Ssrbool.ReflectF} in+ case b2 of {+ Input -> _evar_0_0;+ Temp -> _evar_0_1;+ Output -> _evar_0_2}}+ in+ let {+ _evar_0_1 = let {_evar_0_1 = Ssrbool.ReflectF} in+ let {_evar_0_2 = Ssrbool.ReflectF} in+ let {_evar_0_3 = Ssrbool.ReflectT} in+ case b2 of {+ Input -> _evar_0_1;+ Temp -> _evar_0_2;+ Output -> _evar_0_3}}+ in+ case b1 of {+ Input -> _evar_0_;+ Temp -> _evar_0_0;+ Output -> _evar_0_1}++coq_VarKind_eqMixin :: Eqtype.Equality__Coq_mixin_of VarKind+coq_VarKind_eqMixin =+ Eqtype.Equality__Mixin eqVarKind eqVarKindP++coq_VarKind_eqType :: Eqtype.Equality__Coq_type+coq_VarKind_eqType =+ unsafeCoerce coq_VarKind_eqMixin+ data UsePos =- Build_UsePos Prelude.Int Prelude.Bool+ Build_UsePos Prelude.Int Prelude.Bool VarKind uloc :: UsePos -> Prelude.Int uloc u = case u of {- Build_UsePos uloc0 regReq0 -> uloc0}+ Build_UsePos uloc0 regReq0 uvar0 -> uloc0} regReq :: UsePos -> Prelude.Bool regReq u = case u of {- Build_UsePos uloc0 regReq0 -> regReq0}+ Build_UsePos uloc0 regReq0 uvar0 -> regReq0}++uvar :: UsePos -> VarKind+uvar u =+ case u of {+ Build_UsePos uloc0 regReq0 uvar0 -> uvar0}++upos_le :: UsePos -> UsePos -> Prelude.Bool+upos_le x y =+ (Prelude.<=) (uloc x) (uloc y)++head_or :: Prelude.Int -> ([] UsePos) -> Prelude.Int+head_or x xs =+ Seq.head x (Prelude.map (\u -> uloc u) xs)
linearscan.cabal view
@@ -1,5 +1,5 @@ name: linearscan-version: 0.3.1.0+version: 0.4.0.0 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3@@ -65,10 +65,10 @@ LinearScan.List0 LinearScan.LiveSets LinearScan.Logic+ LinearScan.Loops LinearScan.Main LinearScan.Morph LinearScan.NonEmpty0- LinearScan.Order LinearScan.Range LinearScan.Resolve LinearScan.ScanState@@ -88,22 +88,4 @@ build-depends: base >=4.7 && <4.8 , containers , transformers--test-suite test- default-language: Haskell2010- type: exitcode-stdio-1.0- ghc-options: -fno-warn-deprecated-flags- hs-source-dirs: test- main-is: Main.hs- other-modules: Tempest- build-depends: - base >=3- , linearscan- , hspec >= 1.4.4- , hspec-expectations >= 0.3- , containers >= 0.5.5- , transformers >= 0.3.0.0- , hoopl >= 3.10.0.1- , lens >= 4.2- , mtl- , free+ , mtl
− test/Main.hs
@@ -1,445 +0,0 @@-{-# OPTIONS_GHC -Wall -Werror #-}--module Main where--{--The objective of these tests is to present a real world instruction stream to-the register allocator algorithm, and verify that for certain inputs we get-the expected outputs. I've extracted several of the types from the Tempest-compiler for which this algorithm was originally developed. We link from this-module to the Haskell interface code (LinearScan), which calls into the-Haskell code that was extracted from Coq.--}--import Tempest-import Test.Hspec--main :: IO ()-main = hspec $ do- describe "Sanity tests" sanityTests- describe "Block tests" blockTests--sanityTests :: SpecWith ()-sanityTests = do- it "Single instruction" $ asmTest 32- (label "entry"- (add v0 v1 v2)- return_) $-- label "entry"- (add r0 r1 r2)- return_-- it "Single, repeated instruction" $ asmTest 32- (label "entry"- (do add v0 v1 v2- add v0 v1 v2- add v0 v1 v2)- return_) $-- label "entry"- (do add r0 r1 r2- add r0 r1 r2- add r0 r1 r2)- return_-- it "Multiple instructions" $ asmTest 32- (label "entry"- (do add v0 v1 v2- add v0 v1 v3- add v0 v1 v2)- return_) $-- label "entry"- (do add r0 r1 r2- add r0 r1 r3- add r0 r1 r2)- return_-- it "More variables used than registers" $ asmTest 32- (label "entry"- (do add v0 v1 v2- add v3 v4 v5- add v6 v7 v8- add v9 v10 v11- add v12 v13 v14- add v15 v16 v17- add v18 v19 v20- add v21 v22 v23- add v24 v25 v26- add v27 v28 v29- add v30 v31 v32- add v33 v34 v35)- return_) $-- label "entry"- (do add r0 r1 r24- add r2 r3 r0- add r4 r5 r1- add r6 r7 r2- add r8 r9 r3- add r10 r11 r4- add r12 r13 r5- add r14 r15 r6- add r16 r17 r7- add r18 r19 r8- add r20 r21 r9- add r22 r23 r10)- return_-- it "Single long-lived variable" $ asmTest 32- (label "entry"- (do add v0 v1 v2- add v0 v4 v5- add v0 v7 v8- add v0 v10 v11)- return_) $-- label "entry"- (do add r0 r1 r5- add r0 r2 r1- add r0 r3 r2- add r0 r4 r3)- return_-- it "Two long-lived variables" $ asmTest 32- (label "entry"- (do add v0 v1 v2- add v0 v4 v5- add v0 v4 v8- add v0 v4 v11)- return_) $-- label "entry"- (do add r0 r1 r3- add r0 r2 r1- add r0 r2 r4- add r0 r2 r5)- return_-- it "One variable with a long interval" $ asmTest 32- (label "entry"- (do add v0 v1 v2- add v3 v4 v5- add v6 v7 v8- add v9 v10 v11- add v12 v13 v14- add v15 v16 v17- add v18 v19 v20- add v21 v22 v23- add v24 v25 v26- add v27 v28 v29- add v30 v31 v32- add v0 v34 v35)- return_) $-- label "entry"- (do add r0 r1 r23- add r2 r3 r1- add r4 r5 r2- add r6 r7 r3- add r8 r9 r4- add r10 r11 r5- add r12 r13 r6- add r14 r15 r7- add r16 r17 r8- add r18 r19 r9- add r20 r21 r10- add r0 r22 r11)- return_-- it "Many variables with long intervals" $ asmTest 32- (label "entry"- (do add v0 v1 v2- add v3 v4 v5- add v6 v7 v8- add v9 v10 v11- add v12 v13 v14- add v15 v16 v17- add v18 v19 v20- add v21 v22 v23- add v24 v25 v26- add v27 v28 v29- add v0 v1 v2- add v3 v4 v5- add v6 v7 v8- add v9 v10 v11- add v12 v13 v14- add v15 v16 v17- add v18 v19 v20- add v21 v22 v23- add v24 v25 v26- add v27 v28 v29)- return_) $-- label "entry"- (do add r0 r1 r20- add r2 r3 r21- add r4 r5 r22- add r6 r7 r23- add r8 r9 r24- add r10 r11 r25- add r12 r13 r26- add r14 r15 r27- add r16 r17 r28- add r18 r19 r29- add r0 r1 r20- add r2 r3 r21- add r4 r5 r22- add r6 r7 r23- add r8 r9 r24- add r10 r11 r25- add r12 r13 r26- add r14 r15 r27- add r16 r17 r28- add r18 r19 r29)- return_-- it "Spilling one variable" $ asmTest 32- (label "entry"- (do {- 1 -} add v0 v1 v2- {- 3 -} add v3 v4 v5- {- 5 -} add v6 v7 v8- {- 7 -} add v9 v10 v11- {- 9 -} add v12 v13 v14- {- 11 -} add v15 v16 v17- {- 13 -} add v18 v19 v20- {- 15 -} add v21 v22 v23- {- 17 -} add v24 v25 v26- {- 19 -} add v27 v28 v29- {- 21 -} add v30 v31 v32- {- 23 -} add v0 v1 v2- {- 25 -} add v3 v4 v5- {- 27 -} add v6 v7 v8- {- 29 -} add v9 v10 v11- {- 31 -} add v12 v13 v14- {- 33 -} add v15 v16 v17- {- 35 -} add v18 v19 v20- {- 37 -} add v21 v22 v23- {- 39 -} add v24 v25 v26- {- 41 -} add v27 v28 v29- {- 43 -} add v30 v31 v32)- return_) $-- label "entry"- (do {- 1 -} add r0 r1 r22- {- 3 -} add r2 r3 r23- {- 5 -} add r4 r5 r24- {- 7 -} add r6 r7 r25- {- 9 -} add r8 r9 r26- {- 11 -} add r10 r11 r27- {- 13 -} add r12 r13 r28- {- 15 -} add r14 r15 r29- {- 17 -} add r16 r17 r30- {- 19 -} add r18 r19 r31-- -- When we reach the 32nd variable considered (which happens- -- to be v30), we must spill a register because there are not 32- -- registers. So we pick the first register, counting from 0,- -- whose next use position is the furthest from this position.- -- That happens to be r18, which is next used at position 41.- save r18 0- {- 21 -} add r20 r21 r18- {- 23 -} add r0 r1 r22- {- 25 -} add r2 r3 r23- {- 27 -} add r4 r5 r24- {- 29 -} add r6 r7 r25- {- 31 -} add r8 r9 r26- {- 33 -} add r10 r11 r27- {- 35 -} add r12 r13 r28- {- 37 -} add r14 r15 r29- {- 39 -} add r16 r17 r30-- -- When it comes time to reload v29 (which had been allocated- -- to r18), we pick the first available register which happens- -- to be r0 in this case.- restore 0 r0- {- 41 -} add r0 r19 r31- {- 43 -} add r20 r21 r18)- return_-- it "Inserts only necessary saves and restores" $ asmTest 4- (label "entry"- (do {- 3 -} add v0 v1 v2- {- 5 -} add v2 v1 v3- {- 7 -} add v3 v2 v4- {- 9 -} add v4 v1 v0)- return_) $-- label "entry"- (do {- 3 -} add r1 r0 r2- {- 5 -} add r2 r0 r3- save r0 0- {- 7 -} add r3 r2 r0- restore 0 r2- {- 9 -} add r0 r2 r1)- return_--blockTests :: SpecWith ()-blockTests = do- it "Allocates across blocks" $ asmTest 32- (do label "entry"- (add v0 v1 v2)- (jump "skipped")- label "skipped"- (do add v2 v3 v4- add v2 v4 v5)- (jump "next")- label "next"- (do add v2 v5 v6- add v2 v6 v7- add v2 v7 v8)- return_)-- (do label "entry"- (add r0 r1 r3)- (jump "skipped")- label "skipped"- (do add r3 r2 r0- add r3 r0 r1)- (jump "next")- label "next"- (do add r3 r1 r0- add r3 r0 r1- add r3 r1 r0)- return_)-- it "Inserts resolving moves" $ asmTest 4- (do label "entry" -- 1- (add v0 v1 v2) -- 3- (branch Zero v2 "B3" "B2") -- 5- label "B2" -- 7- (do add v1 v2 v3 -- 9- add v0 v0 v4 -- 11- add v0 v0 v5 -- 13- add v0 v4 v6 -- 15- add v0 v5 v6) -- 17- (jump "B4") -- 19- label "B3" -- 21- (add v1 v2 v3) -- 23- (jump "B4") -- 25- label "B4" -- 27- (add v3 v3 v0) -- 29- return_) -- 31-- (do label "entry"- (add r0 r1 r2)- (branch Zero r2 "B2" "B3")- label "B2"- (add r1 r2 r3)- (jump "B4")- label "B3"- (do add r1 r2 r3- save r3 16- save r2 8- save r1 0- add r0 r0 r1- add r0 r0 r2- add r0 r1 r3- add r0 r2 r3- restore 16 r3)- (jump "B4")- label "B4"- (add r3 r3 r0)- return_)-- it "Inserts resolving moves another way" $ asmTest 4- (do label "entry" -- 1- (add v0 v1 v2) -- 3- (branch Zero v2 "B3" "B2") -- 5- label "B2" -- 7- (add v1 v2 v3) -- 9- (jump "B4") -- 11- label "B3" -- 13- (do add v1 v2 v3 -- 15- add v0 v0 v4 -- 17- add v0 v0 v5 -- 19- add v0 v4 v6 -- 21- add v0 v5 v6) -- 23- (jump "B4") -- 25- label "B4" -- 27- (add v3 v3 v0) -- 29- return_) -- 31-- (do label "entry"- (add r0 r1 r2)- (branch Zero r2 "B2" "B3")- label "B2"- (do add r1 r2 r3- save r3 0- add r0 r0 r1- add r0 r0 r2- add r0 r1 r3- add r0 r2 r3- restore 0 r1)- (jump "B4")- label "B3"- (do add r1 r2 r3- move r3 r1)- (jump "B4")- label "B4"- (add r1 r1 r0)- return_)-- it "Another resolution case" $ asmTest 4- (do label "entry" -- 1- (do lc v3 -- 3- lc v4 -- 5- lc v15 -- 7- lc v20) -- 9- (jump "L3") -- 11- label "L3" -- 13- (do move v3 v9 -- 15- move v9 v11 -- 17- move v11 v10 -- 19- move v10 v12 -- 21- move v12 v13 -- 23- lc v14 -- 25- move v15 v5) -- 27- (jump "L6") -- 29- label_ "L6" -- 31- (branch Zero v4 "L3" "L2") -- 33- label "L2" -- 35- (do lc v21 -- 37- move v21 v18 -- 39- move v5 v4 -- 41- lc v19 -- 43- move v20 v17) -- 45- (jump "L6")) -- 47-- (do label "entry" -- 1- (do lc r0 -- 3- lc r1 -- 5- lc r2 -- 7- lc r3 -- 9- save r3 0)- (jump "L3") -- 11- label "L3" -- 13- (do restore 8 r0- move r0 r3 -- 15- save r0 8- move r3 r0 -- 17- move r0 r3 -- 19- move r3 r0 -- 21- move r0 r3 -- 23- lc r0 -- 25- save r0 16- move r2 r0- save r2 24) -- 27- (jump "L6") -- 29- label_ "L6" -- 31- (branch Zero r1 "L3" "L2") -- 33- label "L2" -- 35- (do lc r3 -- 37- move r3 r2 -- 39- move r0 r1 -- 41- save r1 40- save r0 32- lc r3 -- 43- restore 0 r1- move r1 r0- restore 40 r1- restore 32 r0- restore 24 r2- save r1 0) -- 45- (jump "L6"))
− test/Tempest.hs
@@ -1,575 +0,0 @@-{-# LANGUAGE GADTs #-}-{-# LANGUAGE DeriveFoldable #-}-{-# LANGUAGE DeriveTraversable #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE ConstraintKinds #-}--{-# OPTIONS_GHC -Wall -Werror #-}-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}--module Tempest where--import Compiler.Hoopl as Hoopl hiding ((<*>))-import Control.Applicative-import Control.Exception-import Control.Lens-import Control.Monad.Free-import Control.Monad.State.Class-import Control.Monad.Trans.Class-import qualified Control.Monad.Trans.Free as TF-import Control.Monad.Trans.Free hiding (FreeF(..), Free)-import Control.Monad.Trans.State (StateT, evalStateT, evalState)-import Data.Foldable-import qualified Data.List-import qualified Data.Map as M-import Data.Maybe (fromMaybe)-import Data.Monoid--- import Debug.Trace-import LinearScan-import Test.Hspec----------------------------------------------------------------------------------- The input from the Tempest compiler has the following shape: 'Procedure a--- IRVar', which means that instructions ultimately refer to either physical--- registers, or virtual variables (by index).------ The output from the register allocator should be as close to the input as--- possible, with the difference that it has type 'Procedure a Reg', meaning--- that only physical registers are referenced.------ So the main allocation algorithm roughly has this type at present:------ regAlloc :: Procedure a IRVar -> Procedure a Reg---------------------------------------------------------------------------------data AtomicGroup = AtomicGroup deriving (Eq, Show)-type Name = String--newtype Linearity = Linearity { isLinear :: Bool }- deriving (Eq, Show)---- | Tests used for branching (correspond to branching instructions)-data Test- -- | beq- = Zero- -- | bne- | NonZero- -- | bgt- | Positive- -- | blt- | Negative- deriving (Eq, Show)--data CConv- = CConvC {- ccArgs :: [Reg],- ccResults :: [Reg],- ccIsBrack :: Bool- }- | InlineC- deriving (Eq, Show)--data Constant = Constant deriving (Eq, Show)--type Src a = a---- | Type synonym for indicating destination operands-type Dst a = a---- | Type synonym for indicating success or true branch-type Success a = a---- | Type synonym for indicating failure or false branch-type Failure a = a---- | Type synonym for indicating an external name-type Imported a = a--type Reg = Int--data Instruction reg- = Add reg reg reg- | Nop- deriving (Eq, Show, Functor, Foldable, Traversable)--data IRInstr v e x where- Label :: Label -> IRInstr v C O- Alloc :: AtomicGroup -> Maybe (Src v) -> Dst v -> IRInstr v O O- Reclaim :: Src v -> IRInstr v O O- Instr :: Instruction v -> IRInstr v O O- Call :: CConv -> Instruction v -> IRInstr v O O- LoadConst :: Constant -> Dst v -> IRInstr v O O- Move :: Src v -> Dst v -> IRInstr v O O- Copy :: Src v -> Dst v -> IRInstr v O O- Save :: Linearity -> Src v -> Dst Int -> IRInstr v O O- Restore :: Linearity -> Src Int -> Dst v -> IRInstr v O O- SaveOffset :: Linearity -> Int -> Src v -> Dst Int -> IRInstr v O O- RestoreOffset :: Linearity -> Int -> Src Int -> Dst v -> IRInstr v O O- Jump :: Label -> IRInstr v O C- Branch :: Test -> v -> Success Label -> Failure Label- -> IRInstr v O C- Stwb :: Linearity -> Src v -> Dst v- -> Success Label -> Failure Label -> IRInstr v O C- Strb :: Src v -> Dst v -> Success Label -> Failure Label- -> IRInstr v O C- ReturnInstr :: [Reg] -> Instruction v -> IRInstr v O C--deriving instance Eq v => Eq (IRInstr v e x)--instance Show v => Show (IRInstr v e x) where- show (Label l) = show l ++ ":"- show (Alloc g x1 x2) = "\t@alloc " ++ show g ++- (case x1 of Just v -> " " ++ show v ; _ -> " _")- ++ " " ++ show x2- show (Reclaim v) = "\t@reclaim " ++ show v- show (Instr i) = "\t" ++ show i- show (Call c i) = "\t@call " ++ show c ++ " " ++ show i- show (LoadConst c v) = "\t@lc " ++ show v ++ " " ++ show c- show (Move x1 x2) = "\t@mvrr " ++ show x1 ++ " " ++ show x2- show (Copy x1 x2) = "\t@cprr " ++ show x1 ++ " " ++ show x2- show (Save (Linearity l) src dst)- = "\t@save " ++ show l ++ " " ++ show src ++ " " ++ show dst- show (Restore (Linearity l) src dst)- = "\t@restore " ++ show l ++ " " ++ show src ++ " " ++ show dst- show (SaveOffset (Linearity l) off src dst)- = unwords ["\t@saveoff", show l, show off, show src, show dst]- show (RestoreOffset (Linearity l) off src dst)- = unwords ["\t@restoreoff", show l, show off, show src, show dst]- show (Jump l) = "\t@jmp " ++ show l- show (Branch tst v t f)- = "\t@b" ++ show tst ++ " " ++ show v- ++ " " ++ show t- ++ "; @jmp " ++ show f- show (Stwb lin x1 x2 t f)- = (if isLinear lin then "\t@stwlb " else "\t@stwb ")- ++ show x1 ++ " " ++ show x2- ++ " " ++ show f ++ "; @jmp " ++ show t- show (Strb x1 x2 t f) = "\t@strb " ++ show x1 ++ " " ++ show x2- ++ " " ++ show f ++ "; @jmp " ++ show t- show (ReturnInstr liveRegs i) = "\t@return " ++ show liveRegs ++ " " ++ show i--data Node a v e x = Node- { _nodeIRInstr :: IRInstr v e x- , _nodeMeta :: a- } deriving Eq--instance Show v => Show (Node a v e x) where- show (Node i _) = show i--instance NonLocal (Node a v) where- entryLabel (Node (Label l) _) = l- successors (Node (Jump l) _) = [l]- successors (Node (Branch _ _ t f) _) = [t, f]- successors (Node (Stwb _ _ _ s f) _) = [s, f]- successors (Node (Strb _ _ s f) _) = [s, f]- successors (Node (ReturnInstr _ _) _) = []--data AtomKind = Atom deriving (Eq, Show)-data Var = Var deriving (Eq, Show)--data IRVar' = PhysicalIV !PhysReg- | VirtualIV !Int !AtomKind- deriving Eq--instance Show IRVar' where- show (PhysicalIV r) = "r" ++ show r- show (VirtualIV n _) = "v" ++ show n---- | Virtual IR variable together with an optional AST variable-data IRVar =- IRVar- { _ivVar :: !IRVar' -- ^ The virtual or physical register- , _ivSrc :: !(Maybe Var) -- ^ An optional corresponding AST variable for- -- informational purposes.- }- deriving Eq--instance Show IRVar where- show (IRVar x _) = show x--type Engine m = (UniqueMonad m, MonadState Labels m)--instance UniqueMonad (StateT Labels SimpleUniqueMonad) where- freshUnique = lift freshUnique--asmTest :: (Engine m, m ~ StateT Labels SimpleUniqueMonad)- => Int -> Program IRVar m () -> Program Reg m ()- -> Expectation-asmTest regs (compile -> (prog, entry)) (compile -> (result, _)) =- go $ M.fromList $ zip (Prelude.map entryLabel blocks) [(1 :: Int)..]- where- GMany NothingO body NothingO = prog- blocks = postorder_dfs_from body entry-- go blockIds =- case evalState- (allocate regs (blockInfo getBlockId) opInfo blocks)- (newSpillStack 0) of- Left e -> error $ "Allocation failed: " ++ e- Right blks -> do- let graph' = newGraph blks- catch- (showGraph show graph' `shouldBe` showGraph show result)- (\e -> do- putStrLn "---- Expecting ----"- putStr $ showGraph show result- putStrLn "---- Compiled ----"- putStr $ showGraph show graph'- putStrLn "-------------------"- throwIO (e :: SomeException))- where- newBody = Data.Foldable.foldl' (flip addBlock) emptyBody- newGraph xs = GMany NothingO (newBody xs) NothingO-- getBlockId :: Hoopl.Label -> Int- getBlockId lbl =- fromMaybe (error "The impossible happened")- (M.lookup lbl blockIds)--variables :: Traversal (IRInstr v1 e x) (IRInstr v2 e x) v1 v2-variables f = go- where- go (Alloc ag msrc dst) = Alloc ag <$> traverse f msrc <*> f dst- go (Reclaim src) = Reclaim <$> f src- go (Instr i) = Instr <$> traverse f i- go (LoadConst c dst) = LoadConst c <$> f dst- go (Move src dst) = Move <$> f src <*> f dst- go (Copy src dst) = Copy <$> f src <*> f dst- go (Save lin src x) = Save lin <$> f src <*> pure x- go (Restore x1 x2 dst) = Restore x1 x2 <$> f dst- go (SaveOffset lin off src x) = SaveOffset lin off <$> f src <*> pure x- go (RestoreOffset lin off x dst) = RestoreOffset lin off x <$> f dst- go (Branch x1 cond x2 x3) = Branch x1 <$> f cond- <*> pure x2 <*> pure x3- go (Stwb x1 src dst x2 x3) = Stwb x1 <$> f src <*> f dst- <*> pure x2 <*> pure x3- go (Strb src dst x2 x3) = Strb <$> f src <*> f dst- <*> pure x2 <*> pure x3- go (Call cc i) = Call cc <$> traverse f i- go (ReturnInstr liveInRegs i) = ReturnInstr liveInRegs <$> traverse f i- go (Label x) = pure $ Label x- go (Jump x) = pure $ Jump x--metadata :: Lens (Node a1 v e x) (Node a2 v e x) a1 a2-metadata f (Node instr meta) = Node instr <$> f meta--irinstr :: Traversal (Node a v1 e x) (Node a v2 e x)- (IRInstr v1 e x) (IRInstr v2 e x)-irinstr f (Node instr meta) = Node <$> f instr <*> pure meta--data NodeV a v = NodeCO { getNodeCO :: Node a v C O }- | NodeOO { getNodeOO :: Node a v O O }- | NodeOC { getNodeOC :: Node a v O C }--instance Functor (NodeV v) where- fmap f (NodeCO n) = NodeCO (over (irinstr.variables) f n)- fmap f (NodeOO n) = NodeOO (over (irinstr.variables) f n)- fmap f (NodeOC n) = NodeOC (over (irinstr.variables) f n)--blockInfo :: (Hoopl.Label -> Int)- -> BlockInfo (Block (Node a IRVar) C C)- (Block (Node a Reg) C C)- (NodeV a IRVar)- (NodeV a Reg)-blockInfo getBlockId = BlockInfo- { blockId = getBlockId . entryLabel-- , blockSuccessors = Prelude.map getBlockId . successors-- , blockOps = \(BlockCC a b z) ->- ([NodeCO a], Prelude.map NodeOO (blockToList b), [NodeOC z])-- , setBlockOps = \_ [a] b [z] ->- BlockCC- (getNodeCO a)- (blockFromList (Prelude.map getNodeOO b))- (getNodeOC z)- }--data StackInfo = StackInfo- { stackPtr :: Int- , stackSlots :: M.Map (Maybe Int) Int- }- deriving (Eq, Show)--newSpillStack :: Int -> StackInfo-newSpillStack offset = StackInfo- { stackPtr = offset- , stackSlots = mempty- }--opInfo :: OpInfo StackInfo (NodeV a IRVar) (NodeV a Reg)-opInfo = OpInfo- { opKind = \n -> case n of- NodeOO (Node i _) -> case i of- Call {} -> IsCall- -- jww (2015-01-18): Identification of loop boundaries allows- -- the allocator to perform a block ordering optimization to- -- avoid excessive saves and restores, but it is optional.- -- ? -> LoopBegin- -- ? -> LoopEnd- _ -> IsNormal- NodeOC (Node i _) -> case i of- Jump {} -> IsBranch- Branch {} -> IsBranch- Strb {} -> IsBranch- Stwb {} -> IsBranch- _ -> IsNormal- _ -> IsNormal-- , opRefs = \n -> let f = getReferences in case n of- NodeCO o -> f o- NodeOO o -> f o- NodeOC o -> f o-- , moveOp = \sr dr -> do- let mv = Move sr dr- return [NodeOO (Node mv (error "no move meta"))]-- , swapOp = \sr dr ->- liftA2 (++) (mkRestoreOp Nothing dr)- (mkSaveOp sr Nothing)-- , saveOp = mkSaveOp- , restoreOp = mkRestoreOp-- -- Apply allocations, which changes IRVar's into Reg's.- , applyAllocs = \node m -> [fmap (setRegister m) node]- }- where- go :: Instruction IRVar -> [VarInfo]- go Nop = mempty- go (Add s1 s2 d1) =- mkv Input s1 <> mkv Input s2 <> mkv Output d1-- mkv :: VarKind -> IRVar -> [VarInfo]- mkv k (IRVar (PhysicalIV n) _) = [vinfo k (Left n)]- mkv k (IRVar (VirtualIV n _) _) = [vinfo k (Right n)]-- vinfo k en = VarInfo- { varId = en- , varKind = k- -- If there are variables which can be used directly from- -- memory, then this can be False, which relaxes some- -- requirements.- , regRequired = True- }-- getReferences :: Node a IRVar e x -> [VarInfo]- getReferences (Node (Label _) _) = mempty- getReferences (Node (Instr i) _) = go i- getReferences (Node (Jump _) _) = mempty- getReferences (Node (Move src dst) _) = mkv Input src <> mkv Output dst- getReferences (Node (LoadConst _ v) _) = mkv Output v- getReferences (Node (Branch _ v _ _) _) = mkv Input v- getReferences (Node (ReturnInstr _ i) _) = go i- getReferences n = error $ "getReferences: unhandled node: " ++ show n-- setRegister :: [(Int, PhysReg)] -> IRVar -> Reg- setRegister _ (IRVar (PhysicalIV r) _) = r- setRegister m (IRVar (VirtualIV n _) _) =- fromMaybe (error $ "Allocation failed for variable " ++ show n)- (Data.List.lookup n m)--getStackSlot vid = do- stack <- get- case M.lookup vid (stackSlots stack) of- Just off -> return off- Nothing -> do- let off = stackPtr stack- put StackInfo- { stackPtr = off + 8- , stackSlots =- M.insert vid off (stackSlots stack)- }- return off--mkSaveOp r vid = do- off <- getStackSlot vid- let sv = Save (Linearity False) r off- return [NodeOO (Node sv (error "no save meta"))]--mkRestoreOp vid r = do- off <- getStackSlot vid- let rs = Restore (Linearity False) off r- return [NodeOO (Node rs (error "no restore meta"))]--var :: Int -> IRVar-var i = IRVar { _ivVar = VirtualIV i Atom- , _ivSrc = Nothing- }--fixed :: Int -> IRVar-fixed i = IRVar { _ivVar = PhysicalIV i- , _ivSrc = Nothing- }--reg :: PhysReg -> PhysReg-reg r = r--v0 = var 0-v1 = var 1-v2 = var 2-v3 = var 3-v4 = var 4-v5 = var 5-v6 = var 6-v7 = var 7-v8 = var 8-v9 = var 9-v10 = var 10-v11 = var 11-v12 = var 12-v13 = var 13-v14 = var 14-v15 = var 15-v16 = var 16-v17 = var 17-v18 = var 18-v19 = var 19-v20 = var 20-v21 = var 21-v22 = var 22-v23 = var 23-v24 = var 24-v25 = var 25-v26 = var 26-v27 = var 27-v28 = var 28-v29 = var 29-v30 = var 30-v31 = var 31-v32 = var 32-v33 = var 33-v34 = var 34-v35 = var 35--r0 = reg 0-r1 = reg 1-r2 = reg 2-r3 = reg 3-r4 = reg 4-r5 = reg 5-r6 = reg 6-r7 = reg 7-r8 = reg 8-r9 = reg 9-r10 = reg 10-r11 = reg 11-r12 = reg 12-r13 = reg 13-r14 = reg 14-r15 = reg 15-r16 = reg 16-r17 = reg 17-r18 = reg 18-r19 = reg 19-r20 = reg 20-r21 = reg 21-r22 = reg 22-r23 = reg 23-r24 = reg 24-r25 = reg 25-r26 = reg 26-r27 = reg 27-r28 = reg 28-r29 = reg 29-r30 = reg 30-r31 = reg 31-r32 = reg 32-r33 = reg 33-r34 = reg 34-r35 = reg 35--type BodyF v = Free ((,) (Node () v O O)) ()--nodesToList :: BodyF v -> [Node () v O O]-nodesToList (Pure ()) = []-nodesToList (Free (Node n meta, xs)) = Node n meta : nodesToList xs--data ProgramF m v- = FreeLabel- { labelEntry :: Label- , labelBody :: BodyF v- , labelClose :: m (Node () v O C)- }--type Program v m a = FreeT ((,) (ProgramF m v)) m a--type Labels = M.Map String Label--getLabel :: Engine m => String -> m Label-getLabel str = do- l <- use (at str)- case l of- Just lbl -> return lbl- Nothing -> do- lbl <- freshLabel- at str .= Just lbl- return lbl--label :: Engine m => String -> BodyF v -> m (Node () v O C) -> Program v m ()-label str body close = do- lbl <- lift $ getLabel str- liftF (FreeLabel lbl body close, ())--label_ :: Engine m => String -> m (Node () v O C) -> Program v m ()-label_ str close = do- lbl <- lift $ getLabel str- liftF (FreeLabel lbl (Pure ()) close, ())--compile :: (Engine m, m ~ StateT Labels SimpleUniqueMonad, NonLocal (Node () v))- => Program v m () -> (Graph (Node () v) C C, Hoopl.Label)-compile prog = runSimpleUniqueMonad $- flip evalStateT (mempty :: M.Map String Label) $ do- body <- go prog- entry <- use (at "entry")- case entry of- Nothing -> error "Missing 'entry' label"- Just lbl -> return (bodyGraph body, lbl)- where- go m = do- p <- runFreeT m- case p of- TF.Pure () -> return emptyBody- TF.Free (blk, xs) -> addBlock <$> comp blk <*> go xs-- comp (FreeLabel lbl body close) = do- close' <- close- return $ BlockCC (Node (Label lbl) ())- (blockFromList (nodesToList body)) close'--add :: v -> v -> v -> BodyF v-add x0 x1 x2 = Free (Node (Instr (Add x0 x1 x2)) (), Pure ())--move :: v -> v -> BodyF v-move x0 x1 = Free (Node (Move x0 x1) (), Pure ())--lc :: v -> BodyF v-lc x0 = Free (Node (LoadConst Constant x0) (), Pure ())--return_ :: Monad m => m (Node () v O C)-return_ = return $ Node (ReturnInstr [] Nop) ()--branch :: Engine m => Test -> v -> String -> String -> m (Node () v O C)-branch tst v good bad = do- lblg <- getLabel good- lblb <- getLabel bad- return $ Node (Branch tst v lblg lblb) ()--jump :: Engine m => String -> m (Node () v O C)-jump dest = do- lbl <- getLabel dest- return $ Node (Jump lbl) ()--save :: PhysReg -> Dst Reg -> BodyF Reg-save r dst = Free (Node (Save (Linearity False) r dst) (), Pure ())--restore :: Src Reg -> PhysReg -> BodyF Reg-restore src r = Free (Node (Restore (Linearity False) src r) (), Pure ())