linearscan 0.7.0 → 0.8.0
raw patch · 55 files changed
+2271/−1554 lines, 55 files
Files
- LinearScan.hs +207/−125
- LinearScan/Allocate.hs +222/−132
- LinearScan/Applicative.hs +1/−9
- LinearScan/Ascii.hs +1/−1
- LinearScan/Assign.hs +21/−43
- LinearScan/Blocks.hs +16/−24
- LinearScan/Build.hs +81/−28
- LinearScan/Choice.hs +1/−1
- LinearScan/Class.hs +1/−1
- LinearScan/Const.hs +1/−1
- LinearScan/Context.hs +1/−1
- LinearScan/Cursor.hs +1/−5
- LinearScan/Datatypes.hs +1/−1
- LinearScan/Eqtype.hs +1/−1
- LinearScan/Fintype.hs +1/−1
- LinearScan/Functor.hs +1/−1
- LinearScan/Graph.hs +62/−108
- LinearScan/Identity.hs +22/−1
- LinearScan/IntMap.hs +13/−1
- LinearScan/IntSet.hs +1/−1
- LinearScan/Interval.hs +43/−32
- LinearScan/Lens.hs +1/−1
- LinearScan/Lib.hs +1/−24
- LinearScan/List0.hs +1/−1
- LinearScan/List1.hs +7/−1
- LinearScan/LiveSets.hs +150/−81
- LinearScan/Logic.hs +1/−1
- LinearScan/Loops.hs +1/−1
- LinearScan/Main.hs +30/−25
- LinearScan/Monad.hs +1/−1
- LinearScan/Morph.hs +1/−1
- LinearScan/Nat.hs +1/−1
- LinearScan/NonEmpty.hs +1/−1
- LinearScan/Prelude0.hs +1/−1
- LinearScan/Range.hs +43/−14
- LinearScan/Resolve.hs +445/−330
- LinearScan/ScanState.hs +61/−9
- LinearScan/Seq.hs +11/−11
- LinearScan/Specif.hs +1/−1
- LinearScan/Spill.hs +230/−140
- LinearScan/Split.hs +199/−146
- LinearScan/Ssr.hs +1/−1
- LinearScan/Ssrbool.hs +1/−1
- LinearScan/Ssreflect.hs +1/−1
- LinearScan/Ssrfun.hs +1/−1
- LinearScan/Ssrnat.hs +1/−1
- LinearScan/State.hs +5/−1
- LinearScan/State0.hs +1/−1
- LinearScan/String0.hs +1/−1
- LinearScan/Trace.hs +18/−13
- LinearScan/Tuple.hs +1/−1
- LinearScan/UsePos.hs +28/−28
- LinearScan/Vector0.hs +1/−1
- LinearScan/Verify.hs +324/−193
- linearscan.cabal +1/−1
LinearScan.hs view
@@ -30,7 +30,6 @@ import qualified Data.IntSet as S import qualified Data.List as L import Data.Maybe (fromMaybe)-import qualified Hask.Utils as LS import qualified LinearScan.Applicative as Coq import LinearScan.Blocks import qualified LinearScan.Blocks as LS@@ -76,7 +75,6 @@ } deriving instance Eq LS.VarKind--- deriving instance Show LS.VarKind fromVarInfo :: LinearScan.VarInfo -> LS.VarInfo fromVarInfo (VarInfo a b c) = LS.Build_VarInfo a b c@@ -95,10 +93,9 @@ data OpInfo m op1 op2 = OpInfo { opKind :: op1 -> OpKind , opRefs :: op1 -> [LinearScan.VarInfo]- , moveOp :: PhysReg -> LS.VarId -> PhysReg -> m [op2]- , swapOp :: PhysReg -> LS.VarId -> PhysReg -> LS.VarId -> m [op2]+ , moveOp :: PhysReg -> LS.VarId -> PhysReg -> m [op2] , saveOp :: PhysReg -> LS.VarId -> m [op2]- , restoreOp :: LS.VarId -> PhysReg -> m [op2]+ , restoreOp :: LS.VarId -> PhysReg -> m [op2] , applyAllocs :: op1 -> [(LS.VarId, PhysReg)] -> m [op2] , showOp1 :: op1 -> String }@@ -109,38 +106,42 @@ -> [(Int, Either PhysReg LS.VarId, Maybe PhysReg)] -> [(Int, Either PhysReg LS.VarId, Maybe PhysReg)] -> [LS.ResolvingMoveSet]+ -> Maybe (LS.RegStateDescSet, [LS.AllocError]) -> op1 -> String-showOp1' showop pos ins outs rms o =- let showerv (Left r) = "r" ++ show r- showerv (Right v) = "v" ++ show v in+showOp1' showop pos ins outs rms maerrs o = 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+ let marker label (_i, Left r, _reg) =+ " <" ++ label ++ " r" ++ show r ++ ">\n"+ marker label (i, Right v, reg) =+ " <" ++ label ++ " v" ++ show v +++ "[" ++ show i ++ "]" ++ render reg ++ ">\n" in let leader = show pos ++ ": " in let width = length leader in concatMap (marker "End") outs ++ concatMap (marker "Beg") ins ++ leader ++ showop o ++ "\n" ++- concatMap (\x -> replicate width ' ' ++- replicate 8 ' ' ++ show x ++ "\n") rms+ (case maerrs of+ Nothing -> ""+ Just (regState, aerrs) ->+ concatMap (\x -> replicate width ' ' ++ "!!! " +++ replicate 8 ' ' ++ show x ++ "\n") aerrs +++ (unlines . map (replicate (width + 12) ' ' ++) . lines . show+ $ regState)) +++ concatMap (\x -> replicate (width + 8) ' ' ++ show x ++ "\n") rms deriving instance Eq OpKind deriving instance Show OpKind fromOpInfo :: Monad m => LinearScan.OpInfo m op1 op2 -> LS.OpInfo (m Any) op1 op2-fromOpInfo (OpInfo a b c d e f g h) =+fromOpInfo (OpInfo a b c d e f g) = LS.Build_OpInfo a (map fromVarInfo . b) (\r1 r2 -> U.unsafeCoerce (c r1 r2)) (\r1 r2 -> U.unsafeCoerce (d r1 r2)) (\r1 r2 -> U.unsafeCoerce (e r1 r2))- (\r1 r2 -> U.unsafeCoerce (f r1 r2))- (\r1 r2 -> U.unsafeCoerce (g r1 r2)) h+ (\r1 r2 -> U.unsafeCoerce (f r1 r2)) g data ScanStateDesc = ScanStateDesc { _nextInterval :: Int@@ -153,44 +154,44 @@ , 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")+ ++ concatMap (\(i, _) -> " " ++ showInterval sd i ++ "\n") (M.toList (unhandled sd)) ++ "Active:\n" ++ concatMap (\(i, r) ->- " r" ++ show r ++ showInterval i ++ "\n")+ " r" ++ show r ++ showInterval sd i ++ "\n") (M.toList (active sd)) ++ "Inactive:\n" ++ concatMap (\(i, r) ->- " r" ++ show r ++ showInterval i ++ "\n")+ " r" ++ show r ++ showInterval sd i ++ "\n") (M.toList (inactive sd)) ++ "Handled:\n" ++ concatMap (\(i, r) ->- " " ++ showReg r ++ showInterval i ++ "\n")+ " " ++ showReg r ++ showInterval sd i ++ "\n") (M.toList (handled sd)) ++ "Fixed:\n" ++ concatMap (\(reg, mi) -> case mi of Nothing -> ""- Just i -> " " ++ showIntervalDesc reg i ++ "\n")+ Just i ->+ " " ++ showIntervalDesc reg i True ++ "\n") (zip [0..] (fixedIntervals 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+showInterval :: ScanStateDesc -> Int -> String+showInterval sd i = showIntervalDesc i (intervals sd !! i) False +showIntervalDesc :: Int -> LS.IntervalDesc -> Bool -> String+showIntervalDesc i (LS.Build_IntervalDesc iv ib ie rs) isReg =+ (if isReg+ then "r" ++ show i ++ ": "+ else "[" ++ show i ++ "]: " ++ " v" ++ show iv) ++ " "+ ++ show ib ++ "-" ++ show ie ++ " =>" ++ showRanges rs+ showRanges :: [LS.RangeDesc] -> String showRanges [] = "" showRanges (LS.Build_RangeDesc rb re us:rs) =@@ -204,10 +205,18 @@ showUsePositions [] = "" showUsePositions [u] = go u where- go (LS.Build_UsePos n req _v) = show n ++ (if req then "" else "?")+ go (LS.Build_UsePos n req v) =+ (case v of LS.Input -> "i"+ LS.Output -> "o"+ LS.Temp -> "T")+ ++ 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 "?")+ go (LS.Build_UsePos n req v) =+ (case v of LS.Input -> "i"+ LS.Output -> "o"+ LS.Temp -> "T")+ ++ show n ++ (if req then "" else "?") toScanStateDesc :: LS.ScanStateDescSet -> ScanStateDesc toScanStateDesc (LS.Build_ScanStateDescSet a b c d e f g) =@@ -257,49 +266,89 @@ -> LS.OpId -> IntSet -> IntSet+ -> LoopState -> (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)+showBlock1 getops bid pos liveIns liveOuts loopInfo showops b =+ "\n [ BLOCK " ++ show bid ++ " ]\n"+ ++ " Live In => " ++ show (S.toList liveIns) ++ "\n"+ ++ " Live Kill => " ++ show (S.toList liveKill) ++ "\n"+ ++ " Live Gen => " ++ show (S.toList liveGen) ++ "\n"+ ++ " Live Out => " ++ show (S.toList liveOuts) ++ "\n"+ ++ " Incoming =>" ++ (if null branches+ then " Entry"+ else branches) ++ "\n"+ ++ (if null loops+ then ""+ else " Loops =>" ++ loops ++ "\n")+ ++ showops pos (getops b)+ where+ liveGen = liveOuts `S.difference` liveIns+ liveKill = liveIns `S.difference` liveOuts + branches =+ let fwds = case M.lookup bid (forwardBranches loopInfo) of+ Nothing -> ""+ Just fwds' -> " Fwd" ++ show (S.toList fwds')+ bwds = case M.lookup bid (backwardBranches loopInfo) of+ Nothing -> ""+ Just bwds' -> " Bkwd" ++ show (S.toList bwds')+ in fwds ++ bwds++ loops =+ let hdr = if bid `elem` loopHeaderBlocks loopInfo+ then " Header"+ else ""+ e = if S.member bid (loopEndBlocks loopInfo)+ then " End"+ else ""+ idxs = case foldr (\(idx, blks) rest ->+ if S.member bid blks+ then idx : rest+ else rest) []+ (M.toList (loopIndices loopInfo)) of+ [] -> ""+ xs -> " Idx" ++ show xs+ d = case M.lookup bid (loopDepths loopInfo) of+ Nothing -> ""+ Just (_, d') -> " Depth=" ++ show d'+ in hdr ++ e ++ idxs ++ d+ showOps1 :: LinearScan.OpInfo accType op1 op2 -> ScanStateDesc -> IntMap [LS.ResolvingMoveSet]+ -> IntMap (LS.RegStateDescSet, [LS.AllocError]) -> Int -> [op1] -> String-showOps1 _ _ _ _ [] = ""-showOps1 oinfo sd rms pos (o:os) =+showOps1 _ _ _ _ _ [] = ""+showOps1 oinfo sd rms aerrs pos (o:os) = let here = pos*2+1 in let allocs = allocations sd in- let k idx (bacc, eacc) i =+ let k (idx, i) (brest, erest) = let mreg = M.lookup idx allocs in (if LS.ibeg i == here- then (idx, Right (LS.ivar i), mreg) : bacc- else bacc,+ then (idx, Right (LS.ivar i), mreg) : brest+ else brest, 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 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- (fromMaybe [] (M.lookup (pos*2+1) rms)) o- ++ showOps1 oinfo sd rms (pos+1) os+ then (idx, Right (LS.ivar i), mreg) : erest+ else erest) in+ let r (_idx, Nothing) rest = rest+ r (idx, Just i) (brest, erest) =+ let mreg = M.lookup idx allocs in+ (if LS.ibeg i == here+ then (idx, Left idx, mreg) : brest+ else brest,+ if LS.iend i == here+ then (idx, Left idx, mreg) : erest+ else erest) in+ let (begs, ends) = foldr k ([], []) (zip [0..] (intervals sd)) in+ let entriesIn = fromMaybe [] . M.lookup (pos*2+1) in+ let (begs', ends') = foldr r (begs, ends) (zip [0..] (fixedIntervals sd)) in+ showOp1' (showOp1 oinfo) (pos*2+1) begs' ends'+ (entriesIn rms) (M.lookup (pos*2+1) aerrs) o+ ++ showOps1 oinfo sd rms aerrs (pos+1) os -- | From the point of view of this library, a basic block is nothing more -- than an ordered sequence of operations.@@ -317,22 +366,23 @@ -> ScanStateDesc -> IntMap LS.BlockLiveSets -> IntMap [LS.ResolvingMoveSet]+ -> IntMap (LS.RegStateDescSet, [LS.AllocError])+ -> LoopState -> [blk1] -> m String-showBlocks1 binfo oinfo sd ls rms = go 0+showBlocks1 binfo oinfo sd ls rms aerrs loopInfo = go 0 where go _ [] = return "" go pos (b:bs) = do bid <- LinearScan.blockId binfo b- let (liveIn, liveOut) =- case M.lookup bid ls of- Nothing -> (S.empty, S.empty)- Just s -> (S.fromList (LS.blockLiveIn s),- S.fromList (LS.blockLiveOut s))- let allops blk =- let (x, y, z) = LinearScan.blockOps binfo blk in- x ++ y ++ z- (showBlock1 allops bid pos liveIn liveOut (showOps1 oinfo sd rms) b ++)+ let (liveIn, liveOut) = case M.lookup bid ls of+ Nothing -> (S.empty, S.empty)+ Just s -> (S.fromList (LS.blockLiveIn s),+ S.fromList (LS.blockLiveOut s))+ let allops blk = let (x, y, z) = LinearScan.blockOps binfo blk+ in x ++ y ++ z+ (showBlock1 allops bid pos liveIn liveOut loopInfo+ (showOps1 oinfo sd rms aerrs) b ++) `liftM` go (pos + length (allops b)) bs fromBlockInfo :: Monad m@@ -351,8 +401,9 @@ , resolvingMoves :: IntMap [LS.ResolvingMoveSet] , _inputBlocks :: [blk1] , orderedBlocks :: [blk1]- , allocatedBlocks :: Either (IntMap [LS.AllocError]) [blk2]- , _scanStatePre :: Maybe ScanStateDesc+ , allocatedBlocks :: Either (IntMap (LS.RegStateDescSet, [LS.AllocError]))+ [blk2]+ , scanStatePre :: Maybe ScanStateDesc , scanStatePost :: Maybe ScanStateDesc , blockInfo :: LinearScan.BlockInfo m blk1 blk2 op1 op2 , opInfo :: LinearScan.OpInfo m op1 op2@@ -361,53 +412,66 @@ deriving instance Show LS.AllocError +instance Show LS.RegStateDescSet where+ show (LS.Build_RegStateDescSet allocs _stack) =+ foldr (\(reg, (residency, reservation)) rest ->+ let info = (case reservation of+ Nothing -> ""+ Just v -> "v" ++ show v) +++ (case residency of+ Nothing -> ""+ Just v -> "=v" ++ show v) in+ (if null info+ then ""+ else "r" ++ show reg ++ " -> " ++ info ++ "\n") ++ rest)+ "" (zip ([0..] :: [Int]) allocs)+ instance Show LS.ResolvingMoveSet where show (LS.RSMove fr fv tr) = "move (r" ++ show fr ++ " v" ++ show fv ++ ") " ++ "(r" ++ show tr ++ " v" ++ show fv ++ ")"- show (LS.RSSwap fr fv tr tv) =- "swap (r" ++ show fr ++ " v" ++ show fv ++ ") " ++- "(r" ++ show tr ++ " v" ++ show tv ++ ")"+ show (LS.RSTransfer fr fv tr) =+ "<xfer> (r" ++ show fr ++ " v" ++ show fv ++ ") " +++ "(r" ++ show tr ++ " v" ++ show fv ++ ")" show (LS.RSSpill fr tv) = "spill (r" ++ show fr ++ " v" ++ show tv ++ ")" show (LS.RSRestore fv tr) = "restore (r" ++ show tr ++ " v" ++ show fv ++ ")" show (LS.RSAllocReg fv tr) =- "reserve (r" ++ show tr ++ " v" ++ show fv ++ ")"+ "<reserve> (r" ++ show tr ++ " v" ++ show fv ++ ")" show (LS.RSFreeReg fr tv) =- "release (r" ++ show fr ++ " v" ++ show tv ++ ")"+ "<release> (r" ++ show fr ++ " v" ++ show tv ++ ")" show (LS.RSAssignReg fv tr) =- "assign (r" ++ show tr ++ " v" ++ show fv ++ ")"+ "<assign> (r" ++ show tr ++ " v" ++ show fv ++ ")" show (LS.RSClearReg fr tv) =- "clear (r" ++ show fr ++ " v" ++ show tv ++ ")"+ "<clear> (r" ++ show fr ++ " v" ++ show tv ++ ")"+ show (LS.RSLooped x) = "!!!LOOPED! " ++ show x -- show (LS.RSAllocStack tv) = "<AllocStack (v" ++ show tv ++ ")>" -- show (LS.RSFreeStack fv) = "<FreeStack (v" ++ show fv ++ ")>" --- showResolvingMoves :: IntMap [LS.ResolvingMoveSet] -> String--- showResolvingMoves =--- M.foldlWithKey' (\acc k mv ->--- acc ++ " " ++ show k ++ " => "--- ++ L.intercalate "\n " (map show mv) ++ "\n") ""--showDetails :: Monad m => Details m blk1 blk2 op1 op2 -> m String-showDetails err = do- -- pre <- showScanStateDesc (scanStatePre err)+showDetails :: Monad m+ => Details m blk1 blk2 op1 op2+ -> IntMap (LS.RegStateDescSet, [LS.AllocError]) -> m String+showDetails err allocErrs = do+ let preUnhandled Nothing = ""+ preUnhandled (Just sd) =+ "Original:\n" +++ concatMap (\(i, _) -> " " ++ showInterval sd i ++ "\n")+ (M.toList (unhandled sd)) post <- showScanStateDesc (scanStatePost err)+ (preUnhandled (scanStatePre err)) return $ "Reason: " ++ show (reason err) ++ "\n\n"- -- ++ ">>> ScanState before allocation:\n"- -- ++ pre ++ "\n" ++ ">>> ScanState after allocation:\n" ++ post ++ "\n"- -- ++ ">>> ResolvingMoves =\n"- -- ++ showResolvingMoves (resolvingMoves err) ++ "\n" ++ ">>> " ++ show (loopState err) ++ "\n" where- showScanStateDesc Nothing = return ""- showScanStateDesc (Just sd) =- liftM2 (++) (showBlocks1 (blockInfo err) (opInfo err) sd- (liveSets err) (resolvingMoves err)- (orderedBlocks err))- (return ("\n" ++ show sd))+ showScanStateDesc Nothing _ = return ""+ showScanStateDesc (Just sd) preUnhandled =+ liftM2 (++)+ (showBlocks1 (blockInfo err) (opInfo err) sd+ (liveSets err) (resolvingMoves err) allocErrs+ (loopState err) (orderedBlocks err))+ (return ("\n" ++ preUnhandled ++ show sd)) deriving instance Show LS.FinalStage deriving instance Show LS.BlockLiveSets@@ -462,44 +526,50 @@ let res' = toDetails res binfo oinfo case reason res' of Just (err, _) -> do- dets <- showDetails res'+ dets <- showDetails res' M.empty return $ Left (dets, map reasonToStr err) Nothing -> case allocatedBlocks res' of Left m -> do- dets <- showDetails res'+ dets <- showDetails res' m return $ Left (dets,- -- jww (2015-07-02): NYI- concatMap (\(pos, es) ->+ concatMap (\(pos, (_, es)) -> ("At position " ++ show pos) : map show es) (M.toList m)) Right blks -> return $ Right blks where reasonToStr r = case r of- LS.EIntersectsWithFixedInterval pos reg ->+ LS.EOverlapsWithFixedInterval pos reg -> "Current interval intersects with " ++ "fixed interval for register " ++ show reg ++ " at " ++ show pos- LS.ESplitAssignedIntervalForReg reg ->- "Splitting assigned interval for register " ++ show reg- LS.ESplitActiveOrInactiveInterval b ->- "Splitting " ++ (if b then "active" else "inactive") ++ " interval"+ LS.ESplitAssignedIntervalForReg xid reg pos ->+ "Splitting assigned interval " ++ show xid+ ++ " for register " ++ show reg ++ " at position "++ show pos+ LS.ESplitActiveOrInactiveInterval xid b pos ->+ "Splitting " ++ (if b then "active" else "inactive") ++ " interval "+ ++ show xid ++ " at position "++ show pos LS.ESpillInterval cond ->- "Spilling " ++ show cond- LS.ESplitUnhandledInterval ->- "Splitting unhandled interval"+ "Spilling due to " ++ show cond+ LS.ESplitUnhandledInterval uid pos ->+ "Splitting unhandled interval " ++ show uid+ ++ " at position" ++ show pos LS.EIntervalHasUsePosReqReg pos -> "Interval has use position requiring register at " ++ show pos LS.EIntervalBeginsAtSplitPosition -> "Interval begins at split position"- LS.EMoveUnhandledToActive reg ->- "Allocating unhandled interval at register " ++ show reg- LS.ESplitActiveIntervalForReg reg ->+ LS.EMoveUnhandledToActive uid reg ->+ "Allocating unhandled interval " ++ show uid+ ++ " at register " ++ show reg+ LS.ESplitActiveIntervalForReg reg pos -> "Splitting active interval for register " ++ show reg- LS.ESplitAnyInactiveIntervalForReg reg ->+ ++ " at position "++ show pos+ LS.ESplitAnyInactiveIntervalForReg reg pos -> "Splitting any inactive interval for register " ++ show reg+ ++ " at position "++ show pos LS.ESpillCurrentInterval -> "Spilling current interval"- LS.ESplitCurrentInterval pos ->- "Splitting current interval " ++ show pos+ LS.ESplitCurrentInterval uid pos ->+ "Splitting current interval " ++ show uid+ ++ " at position " ++ show pos LS.ETryAllocateFreeReg reg mpos xid -> "Trying to allocate register " ++ show reg ++ " at " ++ show mpos ++ " for interval " ++ show xid@@ -508,8 +578,10 @@ ++ " at " ++ show mpos ++ " for interval " ++ show xid LS.ERemoveUnhandledInterval xid -> "Removing unhandled interval " ++ show xid- LS.ECannotInsertUnhandled ->- "Cannot insert interval onto unhandled list"+ LS.ECannotInsertUnhandled beg ibeg splitPos iend ->+ "Cannot insert onto unhandled: beg " ++ show beg ++ " >= ibeg "+ ++ show ibeg ++ " && (ibeg == splitPos || iend " ++ show iend+ ++ " == splitPos " ++ show splitPos ++ ")" LS.EIntervalBeginsBeforeUnhandled xid -> "Cannot spill interval " ++ show xid ++ " (begins before current position)"@@ -519,12 +591,22 @@ "Interval " ++ show xid ++ " is a singleton" LS.ERegisterAlreadyAssigned reg -> "Register " ++ show reg ++ " already assigned"- LS.ERegisterAssignmentsOverlap reg ->+ LS.ERegisterAssignmentsOverlap reg i idx -> "Register assignments overlap at " ++ show reg+ ++ " for interval " ++ show i ++ " (index " ++ show idx ++ ")" LS.EUnexpectedNoMoreUnhandled -> "The unexpected happened: no more unhandled intervals"- LS.ECannotSpillIfRegisterRequired i ->- "Cannot spill interval " ++ show i- ++ " with use positions requiring registers"+ LS.ECannotSpillIfRegisterRequired xid ->+ "Cannot spill interval " ++ show xid+ ++ " at position requiring register"+ LS.ECannotSpillIfRegisterRequiredBefore splitPos pos ->+ "Cannot spill interval split at " ++ show splitPos+ ++ " requiring register at position " ++ show pos+ LS.ECannotModifyHandledInterval i ->+ "Attempt to modify handled interval " ++ show i LS.EFuelExhausted -> "Fuel was exhausted"+ LS.EUnhandledIntervalsRemain ->+ "There are unhandled intervals remaining"+ LS.EActiveIntervalsRemain -> "There are active intervals remaining"+ LS.EInactiveIntervalsRemain -> "There are inactive intervals remaining" LS.ENotYetImplemented n -> "Not Yet Implemented (#" ++ show n ++ ")"
LinearScan/Allocate.hs view
@@ -4,7 +4,7 @@ module LinearScan.Allocate where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -15,14 +15,17 @@ import qualified LinearScan.Context as Context import qualified LinearScan.Cursor as Cursor+import qualified LinearScan.Functor as Functor import qualified LinearScan.Interval as Interval import qualified LinearScan.Lib as Lib+import qualified LinearScan.Maybe as Maybe import qualified LinearScan.Morph as Morph import qualified LinearScan.Prelude0 as Prelude0 import qualified LinearScan.ScanState as ScanState import qualified LinearScan.Specif as Specif import qualified LinearScan.Spill as Spill import qualified LinearScan.Split as Split+import qualified LinearScan.Ssr as Ssr import qualified LinearScan.Trace as Trace import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Vector0 as Vector0@@ -57,60 +60,51 @@ type PhysReg = Prelude.Int -intersectsWithFixedInterval :: Prelude.Int -> ScanState.ScanStateDesc ->- PhysReg -> Morph.SState () ()- (Prelude.Maybe Prelude0.Coq_oddnum)-intersectsWithFixedInterval maxReg pre reg =+overlapsWithFixedInterval :: Prelude.Int -> ScanState.ScanStateDesc ->+ PhysReg -> Morph.SState () ()+ (Prelude.Maybe Prelude.Int)+overlapsWithFixedInterval maxReg pre reg = Cursor.withCursor maxReg pre (\sd _ ->- let {int = Cursor.curIntDetails maxReg sd} in Context.ipure (case Vector0.vnth maxReg (ScanState.fixedIntervals maxReg sd) reg of {- Prelude.Just i -> Interval.intervalOverlapPoint ( int) ( i);+ Prelude.Just i ->+ Interval.intervalsOverlap+ (Interval.getIntervalDesc ( (Cursor.curIntDetails maxReg sd)))+ (Interval.getIntervalDesc ( i)); Prelude.Nothing -> Prelude.Nothing})) -updateRegisterPos :: Prelude.Int -> (Vector0.Vec- (Prelude.Maybe Prelude0.Coq_oddnum)) -> Prelude.Int ->- (Prelude.Maybe Prelude0.Coq_oddnum) -> Vector0.Vec- (Prelude.Maybe Prelude0.Coq_oddnum)-updateRegisterPos n v r p =+updateRegisterPos :: Prelude.Int -> (Vector0.Vec (Prelude.Maybe Prelude.Int))+ -> PhysReg -> (Prelude.Maybe Prelude.Int) -> Vector0.Vec+ (Prelude.Maybe Prelude.Int)+updateRegisterPos maxReg v r p = case p of { Prelude.Just x ->- Vector0.vreplace n v r (Prelude.Just- (case Vector0.vnth n v r of {- Prelude.Just n0 ->- case (Prelude.<=) ((Prelude.succ) ( n0)) ( x) of {- Prelude.True -> n0;+ Vector0.vreplace maxReg v r (Prelude.Just+ (case Vector0.vnth maxReg v r of {+ Prelude.Just n ->+ case (Prelude.<=) ((Prelude.succ) n) x of {+ Prelude.True -> n; Prelude.False -> x}; Prelude.Nothing -> x})); Prelude.Nothing -> v} -convert_oddnum :: (Prelude.Maybe Prelude0.Coq_oddnum) -> Prelude.Maybe- Prelude.Int-convert_oddnum x =- case x of {- Prelude.Just x0 -> Prelude.Just ( x0);- Prelude.Nothing -> Prelude.Nothing}- findEligibleRegister :: Prelude.Int -> ScanState.ScanStateDesc -> Interval.IntervalDesc -> (Vector0.Vec- (Prelude.Maybe Prelude0.Coq_oddnum)) -> (,) PhysReg- (Prelude.Maybe Prelude0.Coq_oddnum)+ (Prelude.Maybe Prelude.Int)) -> (,) PhysReg+ (Prelude.Maybe Prelude.Int) findEligibleRegister maxReg sd d xs = case Vector0.vfoldl_with_index maxReg (\reg acc mint -> case acc of { (,) fup fai -> case mint of { Prelude.Just int ->- let {ip = Interval.intervalIntersectionPoint ( int) d} in let {- intersects = case ip of {- Prelude.Just o -> Prelude.True;- Prelude.Nothing -> Prelude.False}}+ op = Interval.intervalsOverlap+ (Interval.getIntervalDesc ( int))+ (Interval.getIntervalDesc d)} in- (,)- (updateRegisterPos maxReg fup reg- (Interval.intervalIntersectionPoint ( int) d))- (Vector0.vreplace maxReg fai reg intersects);+ (,) (updateRegisterPos maxReg fup reg op)+ (Vector0.vreplace maxReg fai reg (Maybe.isJust op)); Prelude.Nothing -> acc}}) ((,) xs (Vector0.vconst maxReg Prelude.False)) (ScanState.fixedIntervals maxReg sd) of {@@ -121,60 +115,60 @@ () () (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 { (,) i r -> updateRegisterPos maxReg v r (f i)}} in let {- freeUntilPos' = Data.List.foldl' (go (\x -> Prelude.Just Prelude0.odd1))- (Vector0.vconst maxReg Prelude.Nothing)- (ScanState.active maxReg sd)}+ actives = Data.List.foldl' (go (\x -> Prelude.Just 0))+ (Vector0.vconst maxReg Prelude.Nothing)+ (ScanState.active maxReg sd)} in let {- intersectingIntervals = Prelude.filter (\x ->- Interval.intervalsIntersect- (Interval.getIntervalDesc- ( (Cursor.curIntDetails maxReg sd)))- (Interval.getIntervalDesc- (- (Vector0.vnth- (ScanState.nextInterval maxReg sd)- (ScanState.intervals maxReg sd)- (Prelude.fst x)))))- (ScanState.inactive maxReg sd)}+ freeUntilPos' = Data.List.foldl'+ (go (\i ->+ Interval.intervalsIntersect+ (Interval.getIntervalDesc+ ( (Cursor.curIntDetails maxReg sd)))+ (Interval.getIntervalDesc+ (+ (Vector0.vnth+ (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) i)))))+ actives (ScanState.inactive maxReg sd)} in let {- freeUntilPos'' = Data.List.foldl'- (go (\i ->- Interval.intervalIntersectionPoint- (- (Vector0.vnth- (ScanState.nextInterval maxReg sd)- (ScanState.intervals maxReg sd) i))- ( (Cursor.curIntDetails maxReg sd))))- freeUntilPos' intersectingIntervals}+ freeUntilPos = Data.List.foldl' (\v reg ->+ case ScanState.verifyNewHandled maxReg sd+ (Interval.getIntervalDesc+ ( (Cursor.curIntDetails maxReg sd))) reg of {+ Prelude.True -> v;+ Prelude.False ->+ updateRegisterPos maxReg v reg (Prelude.Just 0)})+ freeUntilPos' (Fintype.ord_enum maxReg)} in case findEligibleRegister maxReg sd ( (Cursor.curIntDetails maxReg sd))- freeUntilPos'' of {+ freeUntilPos of { (,) reg mres -> let { success = Context.ibind (\x -> Context.ipure reg) (Morph.moveUnhandledToActive maxReg pre reg)} in let {cid = Cursor.curId maxReg sd} in- Context.context (Trace.ETryAllocateFreeReg ( reg) (convert_oddnum mres)+ Context.context (Trace.ETryAllocateFreeReg ( reg) mres ( (Prelude.fst cid))) (Context.ipure (case mres of { Prelude.Just n ->- case (Prelude.<=) ( n) pos of {+ case (Prelude.<=) n+ (Interval.intervalStart+ ( (Cursor.curIntDetails maxReg sd))) of { Prelude.True -> Prelude.Nothing; Prelude.False -> Prelude.Just (case (Prelude.<=) ((Prelude.succ) (Interval.intervalEnd- ( (Cursor.curIntDetails maxReg sd)))) ( n) of {+ ( (Cursor.curIntDetails maxReg sd)))) n of { Prelude.True -> success; Prelude.False -> Context.ibind (\x -> success)@@ -186,25 +180,29 @@ () () (Prelude.Maybe PhysReg) allocateBlockedReg maxReg pre = Cursor.withCursor maxReg pre (\sd _ ->- let {start = Interval.intervalStart ( (Cursor.curIntDetails maxReg sd))}- in- let {pos = Cursor.curPosition maxReg sd} in+ let {pos = Interval.intervalStart ( (Cursor.curIntDetails maxReg sd))} in let {- go = \n v p ->+ go = \v p -> case p of {- (,) int r ->+ (,) int reg -> let { atPos = \u -> (Prelude.&&)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)- (unsafeCoerce (UsePos.uloc u))) (UsePos.regReq u)}+ ((Prelude.||)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)+ (unsafeCoerce (UsePos.uloc u)))+ (Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce ((Prelude.succ) pos))+ (unsafeCoerce (UsePos.uloc u)))) (UsePos.regReq u)} in let { pos' = case Interval.findIntervalUsePos ( int) atPos of { Prelude.Just s -> Prelude.Just Prelude0.odd1;- Prelude.Nothing -> Interval.nextUseAfter ( int) start}}+ Prelude.Nothing -> Interval.nextUseAfter ( int) pos}} in- updateRegisterPos n v r pos'}}+ updateRegisterPos maxReg v reg+ (Functor.fmap (unsafeCoerce Maybe.coq_Maybe_Functor) (\x -> + x) (unsafeCoerce pos'))}} in let { resolve = \xs ->@@ -216,31 +214,28 @@ (Prelude.snd i)) xs} in let {- nextUsePos' = Data.List.foldl' (go maxReg)- (Vector0.vconst maxReg Prelude.Nothing)- (resolve (ScanState.active maxReg sd))}- in- let {- intersectingIntervals = Prelude.filter (\x ->- Interval.intervalsIntersect- (Interval.getIntervalDesc- ( (Cursor.curIntDetails maxReg sd)))- ( (Prelude.fst x)))- (resolve (ScanState.inactive maxReg sd))}+ actives = Data.List.foldl' go (Vector0.vconst maxReg Prelude.Nothing)+ (resolve (ScanState.active maxReg sd))} in let {- nextUsePos'' = Data.List.foldl' (go maxReg) nextUsePos'- intersectingIntervals}+ nextUsePos'' = Data.List.foldl' go actives+ (Prelude.filter (\x ->+ Ssrbool.isSome+ (Interval.intervalsIntersect+ (Interval.getIntervalDesc+ ( (Cursor.curIntDetails maxReg sd)))+ ( (Prelude.fst x))))+ (resolve (ScanState.inactive maxReg sd)))} in case findEligibleRegister maxReg sd ( (Cursor.curIntDetails maxReg sd)) nextUsePos'' of { (,) reg mres -> let {cid = Cursor.curId maxReg sd} in- Context.context (Trace.EAllocateBlockedReg ( reg) (convert_oddnum mres)+ Context.context (Trace.EAllocateBlockedReg ( reg) mres ( (Prelude.fst cid))) (case case mres of { Prelude.Just n ->- (Prelude.<=) ((Prelude.succ) ( n))+ (Prelude.<=) ((Prelude.succ) n) (case Interval.lookupUsePos ( (Cursor.curIntDetails maxReg sd)) (\u -> (Prelude.<=) pos (UsePos.uloc u)) of {@@ -260,12 +255,12 @@ (Morph.moveUnhandledToActive maxReg pre reg)) (case mloc of { Prelude.Just n ->- Context.context (Trace.EIntersectsWithFixedInterval- ( n) ( reg))+ Context.context (Trace.EOverlapsWithFixedInterval n+ ( reg)) (Split.splitCurrentInterval maxReg pre (Split.BeforePos n)); Prelude.Nothing -> Context.ipure ()}))- (intersectsWithFixedInterval maxReg pre reg))+ (overlapsWithFixedInterval maxReg pre reg)) (Split.splitActiveIntervalForReg maxReg pre reg pos)) (Split.splitAnyInactiveIntervalForReg maxReg pre reg pos)})}) @@ -286,42 +281,74 @@ type Coq_intermediate_result = Specif.Coq_sig2 ScanState.ScanStateDesc -goActive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc ->- ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg) ->- Coq_int_reg_seq -> Coq_intermediate_result-goActive maxReg pos sd z x xs =- case (Prelude.<=) ((Prelude.succ)- (Interval.intervalEnd- (- (Vector0.vnth (ScanState.nextInterval maxReg z)- (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of {- Prelude.True ->- Morph.moveActiveToHandled maxReg z Prelude.False (unsafeCoerce x);- Prelude.False ->- case Prelude.not- (Interval.posWithinInterval- (- (Vector0.vnth (ScanState.nextInterval maxReg z)- (ScanState.intervals maxReg z) (Prelude.fst x))) pos) of {- Prelude.True -> Morph.moveActiveToInactive maxReg z (unsafeCoerce x);- Prelude.False -> z}}+goActive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc -> ([]+ Trace.SSTrace) -> ScanState.ScanStateDesc -> ((,)+ ScanState.IntervalId PhysReg) -> Coq_int_reg_seq ->+ Prelude.Either ([] Trace.SSTrace) Coq_intermediate_result+goActive maxReg pos sd e z x xs =+ let {+ eres = case (Prelude.<=) ((Prelude.succ)+ (Interval.intervalEnd+ (+ (Vector0.vnth (ScanState.nextInterval maxReg z)+ (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of {+ Prelude.True ->+ let {+ filtered_var = Ssr.prop+ (ScanState.verifyNewHandled maxReg z+ (Interval.getIntervalDesc+ (+ (Vector0.vnth+ (ScanState.nextInterval maxReg z)+ (ScanState.intervals maxReg z)+ (Prelude.fst x)))) (Prelude.snd x))}+ in+ case filtered_var of {+ Prelude.Just _ ->+ let {+ filtered_var0 = Morph.moveActiveToHandled maxReg z+ Prelude.False (unsafeCoerce x)}+ in+ Prelude.Right filtered_var0;+ Prelude.Nothing -> Prelude.Left ((:)+ (Trace.ERegisterAssignmentsOverlap ( (Prelude.snd x))+ ( (Prelude.fst x)) ((Prelude.succ) 0)) e)};+ Prelude.False -> Prelude.Right+ (case Prelude.not+ (Interval.posWithinInterval+ (+ (Vector0.vnth (ScanState.nextInterval maxReg z)+ (ScanState.intervals maxReg z) (Prelude.fst x)))+ pos) of {+ Prelude.True ->+ Morph.moveActiveToInactive maxReg z (unsafeCoerce x);+ Prelude.False -> z})}}+ in+ case eres of {+ Prelude.Left err -> Prelude.Left err;+ Prelude.Right s -> Prelude.Right s} checkActiveIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int -> Morph.SState () () () checkActiveIntervals maxReg pre pos = Morph.withScanStatePO maxReg pre (\sd _ ->- let {- res = Lib.dep_foldl_inv (\s ->- Eqtype.prod_eqType- (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s))- (Fintype.ordinal_eqType maxReg)) sd- (unsafeCoerce (ScanState.active maxReg sd))- (Data.List.length (ScanState.active maxReg sd))- (unsafeCoerce (ScanState.active maxReg))- (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0))- (unsafeCoerce (\x _ x0 x1 _ -> goActive maxReg pos sd x x0 x1))}- in- Context.iput (Morph.Build_SSInfo res __))+ Context.ibind (\e ->+ let {+ eres = Lib.dep_foldl_invE (\s ->+ Eqtype.prod_eqType+ (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s))+ (Fintype.ordinal_eqType maxReg)) sd+ (unsafeCoerce (ScanState.active maxReg sd))+ (Data.List.length (ScanState.active maxReg sd))+ (unsafeCoerce (ScanState.active maxReg))+ (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0))+ (unsafeCoerce (\x _ x0 x1 _ ->+ goActive maxReg pos sd e x x0 x1))}+ in+ case eres of {+ Prelude.Left err -> Morph.error_ maxReg sd err;+ Prelude.Right s -> Context.iput (Morph.Build_SSInfo s __)})+ Context.iask) moveInactiveToActive' :: Prelude.Int -> ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg) -> Coq_int_reg_seq ->@@ -345,7 +372,8 @@ in Prelude.Right filtered_var0; Prelude.False -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap- ( (Prelude.snd x))) e)}+ ( (Prelude.snd x)) ( (Prelude.fst x)) ((Prelude.succ) ((Prelude.succ)+ 0))) e)} goInactive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc -> ([] Trace.SSTrace) -> ScanState.ScanStateDesc -> ((,)@@ -360,10 +388,24 @@ (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of { Prelude.True -> let {- filtered_var = Morph.moveInactiveToHandled maxReg z Prelude.False- (unsafeCoerce x)}+ filtered_var = Ssr.prop+ (ScanState.verifyNewHandled maxReg z+ (Interval.getIntervalDesc+ (+ (Vector0.vnth (ScanState.nextInterval maxReg z)+ (ScanState.intervals maxReg z) (Prelude.fst x))))+ (Prelude.snd x))} in- f filtered_var;+ case filtered_var of {+ Prelude.Just _ ->+ let {+ filtered_var0 = Morph.moveInactiveToHandled maxReg z Prelude.False+ (unsafeCoerce x)}+ in+ f filtered_var0;+ Prelude.Nothing -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap+ ( (Prelude.snd x)) ( (Prelude.fst x)) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) 0)))) e)}; Prelude.False -> case Interval.posWithinInterval (@@ -402,7 +444,7 @@ () () (Prelude.Maybe PhysReg) handleInterval maxReg pre = Cursor.withCursor maxReg pre (\sd _ ->- let {position = Cursor.curPosition maxReg sd} in+ let {pos = Interval.intervalStart ( (Cursor.curIntDetails maxReg sd))} in case Interval.firstUsePos (Interval.getIntervalDesc ( (Cursor.curIntDetails maxReg sd))) of { Prelude.Just u ->@@ -414,23 +456,71 @@ Prelude.Nothing -> allocateBlockedReg maxReg pre}) (tryAllocateFreeReg maxReg pre)) (Morph.liftLen maxReg pre (\sd0 ->- checkInactiveIntervals maxReg sd0 position)))+ checkInactiveIntervals maxReg sd0 pos))) (Morph.liftLen maxReg pre (\sd0 ->- checkActiveIntervals maxReg sd0 position));+ checkActiveIntervals maxReg sd0 pos)); Prelude.Nothing -> Context.ibind (\x -> Context.ipure Prelude.Nothing) (Morph.moveUnhandledToHandled maxReg pre)}) +finalizeScanState_obligation_1 :: Prelude.Int -> ScanState.ScanStateDesc ->+ Prelude.Int -> (Morph.SSInfo ()) ->+ Prelude.Either ([] Trace.SSTrace)+ ScanState.ScanStateDesc+finalizeScanState_obligation_1 maxReg sd finalPos ss =+ case ss of {+ Morph.Build_SSInfo thisDesc0 _ ->+ let {+ _evar_0_ = \_ ->+ let {+ _evar_0_ = \_ ->+ let {_evar_0_ = \_ -> Prelude.Right thisDesc0} in+ let {+ _evar_0_0 = \_ -> Prelude.Left ((:) Trace.EInactiveIntervalsRemain+ [])}+ in+ case Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce+ (Data.List.length (ScanState.inactive maxReg thisDesc0)))+ (unsafeCoerce 0) of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}}+ in+ let {+ _evar_0_0 = \_ -> Prelude.Left ((:) Trace.EActiveIntervalsRemain [])}+ in+ case Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce+ (Data.List.length (ScanState.active maxReg thisDesc0)))+ (unsafeCoerce 0) of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}}+ in+ let {+ _evar_0_0 = \_ -> Prelude.Left ((:) Trace.EUnhandledIntervalsRemain [])}+ in+ case Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce+ (Data.List.length (ScanState.unhandled maxReg thisDesc0)))+ (unsafeCoerce 0) of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}}+ finalizeScanState :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int ->+ Prelude.Either ([] Trace.SSTrace) ScanState.ScanStateDesc finalizeScanState maxReg sd finalPos =- case Context.ibind (\x -> checkInactiveIntervals maxReg sd finalPos)- (checkActiveIntervals maxReg sd finalPos) [] (Morph.Build_SSInfo sd- __) of {- Prelude.Left l -> sd;+ let {+ filtered_var = Context.ibind (\x ->+ checkInactiveIntervals maxReg sd finalPos)+ (checkActiveIntervals maxReg sd finalPos) []+ (Morph.Build_SSInfo sd __)}+ in+ case filtered_var of {+ Prelude.Left errs -> Prelude.Left errs; Prelude.Right p -> case p of {- (,) u ss -> Morph.thisDesc maxReg sd ss}}+ (,) u ss -> finalizeScanState_obligation_1 maxReg sd finalPos ss}} walkIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int -> Prelude.Either
LinearScan/Applicative.hs view
@@ -4,7 +4,7 @@ module LinearScan.Applicative where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -68,12 +68,4 @@ liftA2 :: (Applicative a1) -> (a2 -> a3 -> a4) -> a1 -> a1 -> a1 liftA2 h f x y = ap h (Functor.fmap (is_functor h) f x) y--data Alternative f =- Build_Alternative (Applicative f) (() -> f) (() -> f -> f -> f)--choose :: (Alternative a1) -> a1 -> a1 -> a1-choose alternative x x0 =- case alternative of {- Build_Alternative alt_is_applicative empty choose0 -> choose0 __ x x0}
LinearScan/Ascii.hs view
@@ -3,7 +3,7 @@ module LinearScan.Ascii where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Assign.hs view
@@ -4,7 +4,7 @@ module LinearScan.Assign where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -101,7 +101,7 @@ generateMoves :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 a1 a2) -> ([] Resolve.ResolvingMove) -> a3 generateMoves maxReg mDict oinfo moves =- Monad.forFoldrM mDict [] moves (\mv acc ->+ Monad.forFoldM mDict [] moves (\acc mv -> let { k = Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict)) (\x -> Prelude.Just x)}@@ -109,13 +109,13 @@ Monad.bind mDict (\mops -> Applicative.pure (Monad.is_applicative mDict) (case mops of {- Prelude.Just ops -> (Prelude.++) ops acc;+ Prelude.Just ops -> (Prelude.++) acc ops; Prelude.Nothing -> acc})) (case mv of { Resolve.Move sreg svid dreg -> k (Blocks.moveOp maxReg mDict oinfo sreg svid dreg);- Resolve.Swap sreg svid dreg dvid ->- k (Blocks.swapOp maxReg mDict oinfo sreg svid dreg dvid);+ Resolve.Transfer p v p0 ->+ Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.Spill sreg svid -> k (Blocks.saveOp maxReg mDict oinfo sreg svid); Resolve.Restore dvid dreg ->@@ -123,6 +123,8 @@ Resolve.AllocReg v p -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.FreeReg p v ->+ Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing;+ Resolve.Looped r -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing})) varAllocs :: Prelude.Int -> Prelude.Int -> ([] Allocate.Allocation) ->@@ -182,8 +184,8 @@ Prelude.True -> let { moves = Resolve.determineMoves maxReg- (Resolve.resolvingMoves maxReg allocs opid- ((Prelude.succ) ((Prelude.succ) opid)))}+ (Resolve.resolvingMoves maxReg allocs Prelude.Nothing+ opid ((Prelude.succ) ((Prelude.succ) opid)))} in Monad.bind (State0.coq_StateT_Monad mDict) (\moves' -> Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict@@ -216,7 +218,8 @@ let {liveOuts = LiveSets.blockLiveOut bls} in Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> let {- eg = Graph.emptyGraph (Resolve.coq_ResGraphNode maxReg)+ eg = Graph.emptyGraph+ (Resolve.coq_ResGraphNode_eqType maxReg) (Resolve.coq_ResGraphEdge_eqType maxReg) (unsafeCoerce (Resolve.determineEdge maxReg))} in@@ -229,14 +232,7 @@ allocs} in Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' ->- let {- begMoves = Graph.topsort- (Resolve.coq_ResGraphNode maxReg)- (Resolve.coq_ResGraphEdge_eqType- maxReg) gbeg- (unsafeCoerce- (Resolve.splitEdge maxReg))}- in+ let {begMoves = Resolve.sortMoves maxReg gbeg} in Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\begMoves' ->@@ -245,13 +241,7 @@ Monad.bind (State0.coq_StateT_Monad mDict) (\opsm' -> let {- endMoves = Graph.topsort- (Resolve.coq_ResGraphNode- maxReg)- (Resolve.coq_ResGraphEdge_eqType- maxReg) gend- (unsafeCoerce- (Resolve.splitEdge maxReg))}+ endMoves = Resolve.sortMoves maxReg gend} in Monad.bind (State0.coq_StateT_Monad mDict) (\opid1 ->@@ -327,7 +317,7 @@ endMoves'))) (Verify.verifyResolutions maxReg mDict (Prelude.pred (Prelude.pred opid1))- useVerifier (unsafeCoerce endMoves)))+ useVerifier endMoves)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y)@@ -341,7 +331,7 @@ (generateMoves maxReg mDict oinfo begMoves'))) (Verify.verifyResolutions maxReg mDict (Prelude.pred (Prelude.pred opid0)) useVerifier- (unsafeCoerce begMoves)))+ begMoves)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y)))@@ -353,7 +343,8 @@ Prelude.Nothing -> Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> let {- eg = Graph.emptyGraph (Resolve.coq_ResGraphNode maxReg)+ eg = Graph.emptyGraph+ (Resolve.coq_ResGraphNode_eqType maxReg) (Resolve.coq_ResGraphEdge_eqType maxReg) (unsafeCoerce (Resolve.determineEdge maxReg))} in@@ -366,14 +357,7 @@ allocs} in Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' ->- let {- begMoves = Graph.topsort- (Resolve.coq_ResGraphNode maxReg)- (Resolve.coq_ResGraphEdge_eqType- maxReg) gbeg- (unsafeCoerce- (Resolve.splitEdge maxReg))}- in+ let {begMoves = Resolve.sortMoves maxReg gbeg} in Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\begMoves' ->@@ -382,13 +366,7 @@ Monad.bind (State0.coq_StateT_Monad mDict) (\opsm' -> let {- endMoves = Graph.topsort- (Resolve.coq_ResGraphNode- maxReg)- (Resolve.coq_ResGraphEdge_eqType- maxReg) gend- (unsafeCoerce- (Resolve.splitEdge maxReg))}+ endMoves = Resolve.sortMoves maxReg gend} in Monad.bind (State0.coq_StateT_Monad mDict) (\opid1 ->@@ -465,7 +443,7 @@ endMoves'))) (Verify.verifyResolutions maxReg mDict (Prelude.pred (Prelude.pred opid1))- useVerifier (unsafeCoerce endMoves)))+ useVerifier endMoves)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y)@@ -479,7 +457,7 @@ (generateMoves maxReg mDict oinfo begMoves'))) (Verify.verifyResolutions maxReg mDict (Prelude.pred (Prelude.pred opid0)) useVerifier- (unsafeCoerce begMoves)))+ begMoves)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y)))
LinearScan/Blocks.hs view
@@ -3,7 +3,7 @@ module LinearScan.Blocks where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -54,59 +54,51 @@ data OpInfo m opType1 opType2 = Build_OpInfo (opType1 -> OpKind) (opType1 -> [] VarInfo) (PhysReg -> VarId -> PhysReg -> m) - (PhysReg -> VarId -> PhysReg -> VarId -> m) (PhysReg -> VarId -> m) - (VarId -> PhysReg -> m) (opType1 -> ([] ((,) VarId PhysReg)) -> m) (opType1- ->- Prelude.String)+ (PhysReg -> VarId -> m) (VarId -> PhysReg -> m) (opType1 -> ([]+ ((,) VarId PhysReg)) -> m) + (opType1 -> Prelude.String) opKind :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> a2 -> OpKind opKind maxReg h o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> opKind0}+ Build_OpInfo opKind0 opRefs0 moveOp0 saveOp0 restoreOp0 applyAllocs0+ showOp -> opKind0} opRefs :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> a2 -> [] VarInfo opRefs maxReg h o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> opRefs0}+ Build_OpInfo opKind0 opRefs0 moveOp0 saveOp0 restoreOp0 applyAllocs0+ showOp -> opRefs0} moveOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> PhysReg -> VarId -> PhysReg -> a1 moveOp maxReg h o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> moveOp0}--swapOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> PhysReg ->- VarId -> PhysReg -> VarId -> a1-swapOp maxReg h o =- case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> swapOp0}+ Build_OpInfo opKind0 opRefs0 moveOp0 saveOp0 restoreOp0 applyAllocs0+ showOp -> moveOp0} saveOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> PhysReg -> VarId -> a1 saveOp maxReg h o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> saveOp0}+ Build_OpInfo opKind0 opRefs0 moveOp0 saveOp0 restoreOp0 applyAllocs0+ showOp -> saveOp0} restoreOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> VarId -> PhysReg -> a1 restoreOp maxReg h o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> restoreOp0}+ Build_OpInfo opKind0 opRefs0 moveOp0 saveOp0 restoreOp0 applyAllocs0+ showOp -> restoreOp0} applyAllocs :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> a2 -> ([] ((,) VarId PhysReg)) -> a1 applyAllocs maxReg h o = case o of {- Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> applyAllocs0}+ Build_OpInfo opKind0 opRefs0 moveOp0 saveOp0 restoreOp0 applyAllocs0+ showOp -> applyAllocs0} type BlockId = Prelude.Int
LinearScan/Build.hs view
@@ -4,7 +4,7 @@ module LinearScan.Build where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -244,43 +244,96 @@ let { _evar_0_ = \_ -> let {- r1 = Range.coq_Range_shift ( _top_assumption_0)- (UsePos.uloc _top_assumption_)}+ _evar_0_ = (,) Prelude.True+ (let {+ r1 = Range.coq_Range_shift ( _top_assumption_0)+ (UsePos.uloc _top_assumption_)}+ in+ (Prelude.flip (Prelude.$)) __ (\_ -> r1))} in- (Prelude.flip (Prelude.$)) __ (\_ -> r1)}+ let {+ _evar_0_0 = \_top_assumption_1 ->+ let {+ _evar_0_0 = \loc req kind us ->+ let {+ _evar_0_0 = (,) Prelude.False+ ((Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ nR = makeNewRange b pos ((Prelude.succ) pos)+ _top_assumption_}+ in+ nR))}+ in+ let {+ _evar_0_1 = (,) Prelude.True+ (let {+ r1 = Range.coq_Range_shift ( _top_assumption_0)+ (UsePos.uloc _top_assumption_)}+ in+ (Prelude.flip (Prelude.$)) __ (\_ -> r1))}+ in+ case Eqtype.eq_op UsePos.coq_VarKind_eqType kind+ (unsafeCoerce UsePos.Output) of {+ Prelude.True -> _evar_0_0;+ Prelude.False -> _evar_0_1}}+ in+ case _top_assumption_1 of {+ UsePos.Build_UsePos x x0 x1 -> unsafeCoerce _evar_0_0 x x0 x1}}+ in+ case Range.ups ( _top_assumption_0) of {+ [] -> _evar_0_;+ (:) x x0 -> _evar_0_0 x x0}} in let {- _evar_0_0 = \_ ->- let {_evar_0_0 = \_ -> _top_assumption_0} in _evar_0_0 __}+ _evar_0_0 = \_ -> (,) Prelude.True+ (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- (NonEmpty.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- (NonEmpty.coq_NE_from_list (makeNewRange b pos e _top_assumption_)- ( range0))}+ _evar_0_ = \replaceFirst _top_assumption_0 ->+ let {+ _evar_0_ = \_ ->+ (Prelude.flip (Prelude.$))+ (Range.coq_Range_cons _top_assumption_ ( _top_assumption_0))+ (\br ->+ let {+ _evar_0_ = let {+ _evar_0_ = \_the_1st_wildcard_ -> Prelude.Just+ ((:[]) br)}+ in+ let {+ _evar_0_0 = \_the_2nd_wildcard_ rs -> Prelude.Just+ (NonEmpty.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+ (NonEmpty.coq_NE_from_list br ( range0))}+ in+ case replaceFirst of {+ Prelude.True -> _evar_0_;+ Prelude.False -> _evar_0_0})}+ in+ let {+ _evar_0_0 = \_ -> Prelude.Just+ (NonEmpty.coq_NE_from_list (makeNewRange b pos e _top_assumption_)+ ( range0))}+ in+ case upos_before_rend ( _top_assumption_0) _top_assumption_ of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}} in- case upos_before_rend ( res) _top_assumption_ of {- Prelude.True -> _evar_0_ __;- Prelude.False -> _evar_0_0 __})}+ case res of {+ (,) x x0 -> _evar_0_ x x0})} in let { _evar_0_0 = Prelude.Just ((:[]) (makeNewRange b pos e _top_assumption_))}
LinearScan/Choice.hs view
@@ -4,7 +4,7 @@ module LinearScan.Choice where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Class.hs view
@@ -4,7 +4,7 @@ module LinearScan.Class where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Const.hs view
@@ -4,7 +4,7 @@ module LinearScan.Const where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Context.hs view
@@ -3,7 +3,7 @@ module LinearScan.Context where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Cursor.hs view
@@ -3,7 +3,7 @@ module LinearScan.Cursor where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -31,10 +31,6 @@ curIntDetails maxReg sd = Vector0.vnth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) (Prelude.fst (curId maxReg sd))--curPosition :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int-curPosition maxReg sd =- Interval.intervalStart ( (curIntDetails maxReg sd)) withCursor :: Prelude.Int -> ScanState.ScanStateDesc -> (ScanState.ScanStateDesc -> () -> Morph.SState () a1 a2) ->
LinearScan/Datatypes.hs view
@@ -3,7 +3,7 @@ module LinearScan.Datatypes where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Eqtype.hs view
@@ -4,7 +4,7 @@ module LinearScan.Eqtype where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Fintype.hs view
@@ -4,7 +4,7 @@ module LinearScan.Fintype where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Functor.hs view
@@ -4,7 +4,7 @@ module LinearScan.Functor where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Graph.hs view
@@ -4,7 +4,7 @@ module LinearScan.Graph where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -16,6 +16,7 @@ import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Seq as Seq import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrnat as Ssrnat @@ -38,13 +39,12 @@ #endif data Graph =- Build_Graph ([] (Prelude.Maybe Eqtype.Equality__Coq_sort)) ([]- Eqtype.Equality__Coq_sort) - (Eqtype.Equality__Coq_sort -> (,) (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort))+ Build_Graph ([] Eqtype.Equality__Coq_sort) ([] Eqtype.Equality__Coq_sort) + (Eqtype.Equality__Coq_sort -> (,) Eqtype.Equality__Coq_sort+ Eqtype.Equality__Coq_sort) vertices :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph- -> [] (Prelude.Maybe Eqtype.Equality__Coq_sort)+ -> [] Eqtype.Equality__Coq_sort vertices a b g = case g of { Build_Graph vertices0 edges0 edge_f0 -> vertices0}@@ -56,17 +56,15 @@ Build_Graph vertices0 edges0 edge_f0 -> edges0} edge_f :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph ->- Eqtype.Equality__Coq_sort -> (,)- (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort)+ Eqtype.Equality__Coq_sort -> (,) Eqtype.Equality__Coq_sort+ Eqtype.Equality__Coq_sort edge_f a b g = case g of { Build_Graph vertices0 edges0 edge_f0 -> edge_f0} emptyGraph :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->- (Eqtype.Equality__Coq_sort -> (,)- (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Graph+ (Eqtype.Equality__Coq_sort -> (,) Eqtype.Equality__Coq_sort+ Eqtype.Equality__Coq_sort) -> Graph emptyGraph a b f = Build_Graph [] [] f @@ -75,11 +73,9 @@ addVertex a b v g = let {vg = vertices a b g} in Build_Graph- (case Ssrbool.in_mem v- (Ssrbool.mem (Seq.seq_predType (Eqtype.option_eqType a))- (unsafeCoerce vg)) of {+ (case Ssrbool.in_mem v (Ssrbool.mem (Seq.seq_predType a) (unsafeCoerce vg)) of { Prelude.True -> vg;- Prelude.False -> (:) (unsafeCoerce v) vg}) (edges a b g) (edge_f a b g)+ Prelude.False -> (:) v vg}) (edges a b g) (edge_f a b g) addEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph -> Graph@@ -93,117 +89,75 @@ Prelude.False -> (:) e eg}) (edge_f a b g)} in case edge_f a b g' e of {- (,) a0 z ->- addVertex a b (unsafeCoerce a0) (addVertex a b (unsafeCoerce z) g')}+ (,) a0 z -> addVertex a b a0 (addVertex a b z g')} removeEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph -> Graph removeEdge a b x g =- Build_Graph (vertices a b g)- (Prelude.filter (\y -> Prelude.not (Eqtype.eq_op b y x)) (edges a b g))- (edge_f a b g)+ Build_Graph (vertices a b g) (Seq.rem b x (edges a b g)) (edge_f a b g) connections :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->- (((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Prelude.Maybe- Eqtype.Equality__Coq_sort) -> (Prelude.Maybe- Eqtype.Equality__Coq_sort) -> Graph -> []- Eqtype.Equality__Coq_sort+ (((,) Eqtype.Equality__Coq_sort Eqtype.Equality__Coq_sort) ->+ Eqtype.Equality__Coq_sort) -> Eqtype.Equality__Coq_sort ->+ Graph -> [] Eqtype.Equality__Coq_sort connections a b f x g = Prelude.filter- ((Prelude..)- ((Prelude..) (\y ->- Eqtype.eq_op (Eqtype.option_eqType a) (unsafeCoerce y)- (unsafeCoerce x)) f) (edge_f a b g)) (edges a b g)+ ((Prelude..) ((Prelude..) (\y -> Eqtype.eq_op a y x) f) (edge_f a b g))+ (edges a b g) outbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->- (Prelude.Maybe Eqtype.Equality__Coq_sort) -> Graph -> []+ Eqtype.Equality__Coq_sort -> Graph -> [] Eqtype.Equality__Coq_sort outbound a b = connections a b Prelude.fst inbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->- (Prelude.Maybe Eqtype.Equality__Coq_sort) -> Graph -> []- Eqtype.Equality__Coq_sort+ Eqtype.Equality__Coq_sort -> Graph -> [] Eqtype.Equality__Coq_sort inbound a b = connections a b Prelude.snd -tsort' :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->- Prelude.Int -> ([] Eqtype.Equality__Coq_sort) -> ([]- (Prelude.Maybe Eqtype.Equality__Coq_sort)) ->- (Eqtype.Equality__Coq_sort -> [] Eqtype.Equality__Coq_sort) ->- Graph -> [] Eqtype.Equality__Coq_sort-tsort' a b fuel l roots k g =- (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))- (\_ ->- Seq.rev l)- (\fuel0 ->- case edges a b g of {- [] -> Seq.rev l;- (:) e es ->- case roots of {- [] ->- let {l0 = (:) (Prelude.snd (edge_f a b g e)) []} in- let {g' = Prelude.foldr (addEdge a b) (removeEdge a b e g) (k e)} in- case l0 of {- [] -> [];- (:) n s ->- let {outEdges = outbound a b n g'} in- case Data.List.foldl' (\acc e0 ->- case acc of {- (,) res g'' -> (,) ((:) e0 res) (removeEdge a b e0 g'')})- ((,) [] g') outEdges of {- (,) res g'' ->- let {- outNodes = Prelude.map ((Prelude..) Prelude.snd (edge_f a b g))- outEdges}- in- let {- s' = (Prelude.++) s- (Prelude.filter- ((Prelude..) Seq.nilp (\x -> inbound a b x g''))- outNodes)}- in- tsort' a b fuel0 ((Prelude.++) l res) s' k g''}};- (:) n s ->- let {l0 = (:) n s} in- case l0 of {- [] -> [];- (:) n0 s0 ->- let {outEdges = outbound a b n0 g} in- case Data.List.foldl' (\acc e0 ->- case acc of {- (,) res g'' -> (,) ((:) e0 res) (removeEdge a b e0 g'')})- ((,) [] g) outEdges of {- (,) res g'' ->- let {- outNodes = Prelude.map ((Prelude..) Prelude.snd (edge_f a b g))- outEdges}- in- let {- s' = (Prelude.++) s0- (Prelude.filter- ((Prelude..) Seq.nilp (\x -> inbound a b x g''))- outNodes)}- in- tsort' a b fuel0 ((Prelude.++) l res) s' k g''}}}})- fuel+removeVertex :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->+ Eqtype.Equality__Coq_sort -> Graph -> Graph+removeVertex a b v g =+ Prelude.foldr (removeEdge a b) (Build_Graph (Seq.rem a v (vertices a b g))+ (edges a b g) (edge_f a b g)) (outbound a b v g) topsort :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph ->- (Eqtype.Equality__Coq_sort -> [] Eqtype.Equality__Coq_sort) -> []- Eqtype.Equality__Coq_sort-topsort a b g k =+ (Eqtype.Equality__Coq_sort -> Prelude.Bool) ->+ (Eqtype.Equality__Coq_sort -> [] Eqtype.Equality__Coq_sort) -> (,)+ ([] Eqtype.Equality__Coq_sort)+ ([] ((,) Prelude.Int Eqtype.Equality__Coq_sort))+topsort a b g0 splittable split = let {- noInbound = let {- xs = Prelude.map ((Prelude..) Prelude.snd (edge_f a b g))- (edges a b g)}- in- Prelude.filter (\x ->- Prelude.not- (Ssrbool.in_mem (unsafeCoerce x)- (Ssrbool.mem (Seq.seq_predType (Eqtype.option_eqType a))- (unsafeCoerce xs)))) (vertices a b g)}- in- tsort' a b ((Prelude.succ) (Data.List.length (vertices a b g))) []- noInbound k g+ go fuel depth g =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ -> (,) (vertices a b g)+ (Prelude.map (\i -> (,) depth i) (edges a b g)))+ (\fuel0 ->+ let {+ noInbound = Prelude.filter (\v -> Seq.nilp (inbound a b v g))+ (vertices a b g)}+ in+ case noInbound of {+ [] ->+ case edges a b g of {+ [] -> (,) [] [];+ (:) e l ->+ let {+ x = case Prelude.filter (\e0 -> splittable e0) (edges a b g) of {+ [] -> e;+ (:) e' l0 -> e'}}+ in+ go fuel0 ((Prelude.succ) depth)+ (Prelude.foldr (addEdge a b) (removeEdge a b x g) (split x))};+ (:) s l ->+ case go fuel0 ((Prelude.succ) depth)+ (Prelude.foldr (removeVertex a b) g noInbound) of {+ (,) ns' es' -> (,) ((Prelude.++) noInbound ns')+ ((Prelude.++)+ (Prelude.map (\i -> (,) depth i)+ (Seq.flatten (Prelude.map (\n -> outbound a b n g) noInbound)))+ es')}})+ fuel}+ in go (Ssrnat.double (Data.List.length (vertices a b g0))) 0 g0
LinearScan/Identity.hs view
@@ -4,7 +4,7 @@ module LinearScan.Identity where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -13,7 +13,9 @@ import qualified Data.Functor.Identity import qualified Hask.Utils +import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Functor as Functor+import qualified LinearScan.Monad as Monad @@ -27,6 +29,16 @@ #ifdef __GLASGOW_HASKELL__+--unsafeCoerce :: a -> b+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+--unsafeCoerce :: a -> b+unsafeCoerce = IOExts.unsafeCoerce+#endif+++#ifdef __GLASGOW_HASKELL__ type Any = GHC.Prim.Any #else -- HUGS@@ -38,4 +50,13 @@ coq_Identity_Functor :: Functor.Functor (Identity Any) coq_Identity_Functor _ _ x = x++coq_Identity_Applicative :: Applicative.Applicative (Identity Any)+coq_Identity_Applicative =+ Applicative.Build_Applicative coq_Identity_Functor (\_ x -> x) (\_ _ x ->+ unsafeCoerce x)++coq_Identity_Monad :: Monad.Monad (Identity Any)+coq_Identity_Monad =+ Monad.Build_Monad coq_Identity_Applicative (\_ x -> x)
LinearScan/IntMap.hs view
@@ -4,7 +4,7 @@ module LinearScan.IntMap where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -102,6 +102,10 @@ coq_IntMap_foldl f z m = Data.List.foldl' (\acc x -> f acc (Prelude.snd x)) z m +coq_IntMap_foldr :: (a2 -> a1 -> a1) -> a1 -> (IntMap a2) -> a1+coq_IntMap_foldr f z m =+ Prelude.foldr (\x -> f (Prelude.snd x)) z m+ coq_IntMap_foldlWithKey :: (a1 -> Prelude.Int -> a2 -> a1) -> a1 -> (IntMap a2) -> a1 coq_IntMap_foldlWithKey f z m =@@ -110,6 +114,14 @@ coq_IntMap_toList :: (IntMap a1) -> [] ((,) Prelude.Int a1) coq_IntMap_toList m = m++coq_IntMap_addToList :: Prelude.Int -> a1 -> (IntMap ([] a1)) -> IntMap+ ([] a1)+coq_IntMap_addToList k x m =+ coq_IntMap_alter (\mxs -> Prelude.Just+ (case mxs of {+ Prelude.Just xs -> (:) x xs;+ Prelude.Nothing -> (:) x []})) k m eqIntMap :: Eqtype.Equality__Coq_type -> (IntMap Eqtype.Equality__Coq_sort) -> (IntMap Eqtype.Equality__Coq_sort) -> Prelude.Bool
LinearScan/IntSet.hs view
@@ -4,7 +4,7 @@ module LinearScan.IntSet where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Interval.hs view
@@ -4,7 +4,7 @@ module LinearScan.Interval where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -93,32 +93,13 @@ (Prelude.&&) ((Prelude.<=) (intervalStart d) pos) ((Prelude.<=) ((Prelude.succ) pos) (intervalEnd d)) -intervalOverlapPoint :: IntervalDesc -> IntervalDesc -> Prelude.Maybe- Prelude0.Coq_oddnum-intervalOverlapPoint x y =- Data.List.foldl' (\mx rd ->- Maybe.option_choose mx- (Data.List.foldl' (\mx' rd' ->- Maybe.option_choose mx (Range.rangeIntersectionPoint ( rd) ( rd')))- Prelude.Nothing (rds y))) Prelude.Nothing (rds x)--intervalsIntersect :: IntervalDesc -> IntervalDesc -> Prelude.Bool-intervalsIntersect x y =- (Prelude.||)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (iend x))- (unsafeCoerce (iend y)))- ((Prelude.&&) ((Prelude.<=) ((Prelude.succ) (ibeg x)) (iend y))- ((Prelude.<=) ((Prelude.succ) (ibeg y)) (iend x)))--intervalIntersectionPoint :: IntervalDesc -> IntervalDesc -> Prelude.Maybe- Prelude0.Coq_oddnum-intervalIntersectionPoint x y =- case intervalsIntersect (getIntervalDesc x) (getIntervalDesc y) of {- Prelude.True -> Prelude.Just- (case (Prelude.<=) ((Prelude.succ) (ibeg x)) (ibeg y) of {- Prelude.True -> ibeg y;- Prelude.False -> ibeg x});- Prelude.False -> Prelude.Nothing}+intervalsOverlap :: IntervalDesc -> IntervalDesc -> Prelude.Maybe Prelude.Int+intervalsOverlap i j =+ Data.List.foldl' (\acc xr ->+ Data.List.foldl' (\acc' yr ->+ Maybe.option_choose acc'+ (Range.rangesIntersect (Range.getRangeDesc ( xr))+ (Range.getRangeDesc ( yr)))) acc (rds j)) Prelude.Nothing (rds i) findIntervalUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) -> Prelude.Maybe@@ -176,6 +157,11 @@ Prelude.Just x -> _evar_0_ x; Prelude.Nothing -> _evar_0_0} +intervalHasInputsAt :: IntervalDesc -> Prelude.Int -> Prelude.Bool+intervalHasInputsAt d pos =+ Data.List.foldl' (\b r -> (Prelude.||) b (Range.hasInputsAt ( r) pos))+ Prelude.False (rds d)+ nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe Prelude0.Coq_oddnum nextUseAfter d pos =@@ -190,6 +176,21 @@ [] -> Prelude.Nothing; (:) u l -> Prelude.Just u} +posAtRangeEnd :: IntervalDesc -> Prelude.Int -> Prelude.Bool+posAtRangeEnd d pos =+ let {+ go xs =+ (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+ (\x ->+ Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Range.rend ( x)))+ (unsafeCoerce pos))+ (\x xs0 ->+ (Prelude.||)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Range.rend ( x)))+ (unsafeCoerce pos)) (go xs0))+ xs}+ in go (rds d)+ firstUsePos :: IntervalDesc -> Prelude.Maybe UsePos.UsePos firstUsePos d = let {@@ -214,12 +215,11 @@ xs} in go (rds d) -afterLifetimeHole :: IntervalDesc -> Prelude0.Coq_oddnum ->- Prelude0.Coq_oddnum+afterLifetimeHole :: IntervalDesc -> Prelude.Int -> Prelude.Int afterLifetimeHole d pos = let { f = \x k ->- case (Prelude.<=) ((Prelude.succ) ( pos)) (Range.rbeg ( x)) of {+ case (Prelude.<=) ((Prelude.succ) pos) (Range.rbeg ( x)) of { Prelude.True -> Range.rbeg ( x); Prelude.False -> k}} in@@ -237,6 +237,18 @@ firstUseReqReg d = lookupUsePos d UsePos.regReq +intervalsIntersect :: IntervalDesc -> IntervalDesc -> Prelude.Maybe+ Prelude.Int+intervalsIntersect x y =+ case (Prelude.&&) ((Prelude.<=) ((Prelude.succ) (ibeg x)) (iend y))+ ((Prelude.<=) ((Prelude.succ) (ibeg y)) (iend x)) of {+ Prelude.True -> Prelude.Just+ (case (Prelude.<=) ((Prelude.succ) (ibeg x)) (ibeg y) of {+ Prelude.True -> ibeg y;+ Prelude.False -> ibeg x});+ Prelude.False ->+ Range.rangesIntersect ( (Prelude.last (rds x))) ( (Prelude.head (rds y)))}+ divideIntervalRanges :: IntervalDesc -> Prelude.Int -> ((,) Range.SortedRanges Range.SortedRanges) divideIntervalRanges d before =@@ -363,8 +375,7 @@ [] -> _evar_0_; (:) x x0 -> _evar_0_0 x x0}} in- case List1.span (\rd ->- (Prelude.<=) ((Prelude.succ) (Range.rend ( rd))) before) ( (rds d)) of {+ case List1.span (\rd -> (Prelude.<=) (Range.rend ( rd)) before) ( (rds d)) of { (,) x x0 -> _evar_0_ x x0 __} splitIntervalRanges :: IntervalDesc -> Prelude.Int ->
LinearScan/Lens.hs view
@@ -4,7 +4,7 @@ module LinearScan.Lens where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Lib.hs view
@@ -3,7 +3,7 @@ module LinearScan.Lib where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -18,29 +18,6 @@ __ :: any __ = Prelude.error "Logical or arity value used"--dep_foldl_inv :: (a1 -> Eqtype.Equality__Coq_type) -> a1 -> ([]- Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a1 -> []- Eqtype.Equality__Coq_sort) -> (a1 -> a1 -> () ->- Eqtype.Equality__Coq_sort -> Eqtype.Equality__Coq_sort) ->- (a1 -> () -> Eqtype.Equality__Coq_sort -> ([]- Eqtype.Equality__Coq_sort) -> () -> Specif.Coq_sig2 - a1) -> a1-dep_foldl_inv e b v n q f f0 =- let {filtered_var = (,) v n} in- case filtered_var of {- (,) l n0 ->- case l of {- [] -> b;- (:) y ys ->- (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))- (\_ ->- b)- (\n' ->- let {filtered_var0 = f0 b __ y ys __} in- let {ys' = Prelude.map (f b filtered_var0 __) ys} in- dep_foldl_inv e filtered_var0 ys' n' q f f0)- n0}} dep_foldl_invE :: (a2 -> Eqtype.Equality__Coq_type) -> a2 -> ([] Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a2 -> []
LinearScan/List0.hs view
@@ -3,7 +3,7 @@ module LinearScan.List0 where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/List1.hs view
@@ -3,7 +3,7 @@ module LinearScan.List1 where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -36,6 +36,12 @@ case Eqtype.eq_op a k x of { Prelude.True -> Prelude.Just v0; Prelude.False -> maybeLookup a xs x}}}++listToMaybe :: ([] a1) -> Prelude.Maybe ([] a1)+listToMaybe xs =+ case xs of {+ [] -> Prelude.Nothing;+ (:) a l -> Prelude.Just xs} olast :: ([] a1) -> Prelude.Maybe a1 olast l =
LinearScan/LiveSets.hs view
@@ -4,7 +4,7 @@ module LinearScan.LiveSets where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -16,10 +16,15 @@ import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Functor as Functor+import qualified LinearScan.Identity as Identity import qualified LinearScan.IntMap as IntMap import qualified LinearScan.IntSet as IntSet+import qualified LinearScan.Lens as Lens import qualified LinearScan.List1 as List1 import qualified LinearScan.Monad as Monad+import qualified LinearScan.Prelude0 as Prelude0+import qualified LinearScan.State as State+import qualified LinearScan.State0 as State0 import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool@@ -88,6 +93,12 @@ Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0 blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLastOpId0} +emptyBlockLiveSets :: BlockLiveSets+emptyBlockLiveSets =+ Build_BlockLiveSets IntSet.emptyIntSet IntSet.emptyIntSet+ IntSet.emptyIntSet IntSet.emptyIntSet ((Prelude.succ) 0) ((Prelude.succ)+ 0)+ eqBlockLiveSets :: BlockLiveSets -> BlockLiveSets -> Prelude.Bool eqBlockLiveSets s1 s2 = case s1 of {@@ -222,6 +233,108 @@ coq_BlockLiveSets_eqType = unsafeCoerce coq_BlockLiveSets_eqMixin +_blockLiveGen :: (Functor.Functor a1) -> (IntSet.IntSet -> a1) ->+ BlockLiveSets -> a1+_blockLiveGen h f s =+ Functor.fmap h (\x -> Build_BlockLiveSets x (blockLiveKill s)+ (blockLiveIn s) (blockLiveOut s) (blockFirstOpId s) (blockLastOpId s))+ (f (blockLiveGen s))++_blockLiveKill :: (Functor.Functor a1) -> (IntSet.IntSet -> a1) ->+ BlockLiveSets -> a1+_blockLiveKill h f s =+ Functor.fmap h (\x -> Build_BlockLiveSets (blockLiveGen s) x+ (blockLiveIn s) (blockLiveOut s) (blockFirstOpId s) (blockLastOpId s))+ (f (blockLiveKill s))++_blockLiveIn :: (Functor.Functor a1) -> (IntSet.IntSet -> a1) ->+ BlockLiveSets -> a1+_blockLiveIn h f s =+ Functor.fmap h (\x -> Build_BlockLiveSets (blockLiveGen s)+ (blockLiveKill s) x (blockLiveOut s) (blockFirstOpId s)+ (blockLastOpId s)) (f (blockLiveIn s))++_blockLiveOut :: (Functor.Functor a1) -> (IntSet.IntSet -> a1) ->+ BlockLiveSets -> a1+_blockLiveOut h f s =+ Functor.fmap h (\x -> Build_BlockLiveSets (blockLiveGen s)+ (blockLiveKill s) (blockLiveIn s) x (blockFirstOpId s) (blockLastOpId s))+ (f (blockLiveOut s))++_blockFirstOpId :: (Functor.Functor a1) -> (Blocks.OpId -> a1) ->+ BlockLiveSets -> a1+_blockFirstOpId h f s =+ Functor.fmap h (\x -> Build_BlockLiveSets (blockLiveGen s)+ (blockLiveKill s) (blockLiveIn s) (blockLiveOut s) x (blockLastOpId s))+ (f (blockFirstOpId s))++_blockLastOpId :: (Functor.Functor a1) -> (Blocks.OpId -> a1) ->+ BlockLiveSets -> a1+_blockLastOpId h f s =+ Functor.fmap h (\x -> Build_BlockLiveSets (blockLiveGen s)+ (blockLiveKill s) (blockLiveIn s) (blockLiveOut s) (blockFirstOpId s) x)+ (f (blockLastOpId s))++computeLiveSets :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo + a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> a1 ->+ Prelude.Int -> State.State BlockLiveSets Prelude.Int+computeLiveSets maxReg mDict binfo oinfo b idx =+ case Blocks.blockOps mDict binfo b of {+ (,) p opse ->+ case p of {+ (,) opsb opsm ->+ Monad.bind+ (State0.coq_StateT_Monad (unsafeCoerce Identity.coq_Identity_Monad))+ (\x ->+ Monad.bind (unsafeCoerce State.coq_State_Monad) (\x0 ->+ Monad.forFoldM (unsafeCoerce State.coq_State_Monad) idx+ ((Prelude.++) opsb ((Prelude.++) opsm opse)) (\next o ->+ case List1.partition (\v ->+ Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (Blocks.varKind maxReg v))+ (unsafeCoerce UsePos.Input))+ (Blocks.opRefs maxReg mDict oinfo o) of {+ (,) inputs others ->+ Monad.bind (unsafeCoerce State.coq_State_Monad) (\x1 ->+ Monad.bind (unsafeCoerce State.coq_State_Monad) (\x2 ->+ Monad.bind (unsafeCoerce State.coq_State_Monad) (\x3 ->+ Applicative.pure+ (unsafeCoerce State.coq_State_Applicative)+ ((Prelude.succ) ((Prelude.succ) next)))+ (Lens.modifyStateT (\_ -> _blockLastOpId) next+ (unsafeCoerce Identity.coq_Identity_Monad)))+ (Monad.forM_ (unsafeCoerce State.coq_State_Monad) others+ (\v ->+ case Blocks.varId maxReg v of {+ Prelude.Left p0 ->+ Applicative.pure+ (unsafeCoerce State.coq_State_Applicative) ();+ Prelude.Right vid ->+ Lens.applyStateT (\_ -> _blockLiveKill)+ (IntSet.coq_IntSet_insert vid)+ (unsafeCoerce Identity.coq_Identity_Monad)})))+ (Monad.forM_ (unsafeCoerce State.coq_State_Monad) inputs+ (\v ->+ case Blocks.varId maxReg v of {+ Prelude.Left p0 ->+ Applicative.pure+ (unsafeCoerce State.coq_State_Applicative) ();+ Prelude.Right vid ->+ Monad.bind (unsafeCoerce State.coq_State_Monad)+ (\liveKill ->+ Monad.unless (unsafeCoerce State.coq_State_Monad)+ (IntSet.coq_IntSet_member vid liveKill)+ (Lens.applyStateT (\_ -> _blockLiveGen)+ (IntSet.coq_IntSet_insert vid)+ (unsafeCoerce Identity.coq_Identity_Monad)))+ (Lens.use (Lens.stepdownl' (\_ -> _blockLiveKill))+ (unsafeCoerce Identity.coq_Identity_Monad))}))}))+ (Lens.modifyStateT (\_ -> _blockLastOpId) idx+ (unsafeCoerce Identity.coq_Identity_Monad)))+ (Lens.modifyStateT (\_ -> _blockFirstOpId)+ ((Prelude.+) idx (Ssrnat.double (Data.List.length opsb)))+ (unsafeCoerce Identity.coq_Identity_Monad))}}+ computeLocalLiveSets :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> a5@@ -232,68 +345,39 @@ (\acc b -> case acc of { (,) idx m ->- case Blocks.blockOps mDict binfo b of {- (,) p opse ->- case p of {- (,) opsb opsm ->- let {- liveSet = Build_BlockLiveSets IntSet.emptyIntSet- IntSet.emptyIntSet IntSet.emptyIntSet IntSet.emptyIntSet- ((Prelude.+) idx (Ssrnat.double (Data.List.length opsb))) idx}- in- case List1.forFold ((,) idx liveSet)- ((Prelude.++) opsb ((Prelude.++) opsm opse)) (\acc0 o ->- case acc0 of {- (,) lastIdx liveSet1 -> (,) ((Prelude.succ)- ((Prelude.succ) lastIdx))- (case List1.partition (\v ->- Eqtype.eq_op UsePos.coq_VarKind_eqType- (unsafeCoerce (Blocks.varKind maxReg v))- (unsafeCoerce UsePos.Input))- (Blocks.opRefs maxReg mDict oinfo o) of {- (,) inputs others ->- let {- liveSet2 = List1.forFold liveSet1 inputs- (\liveSet2 v ->- case Blocks.varId maxReg v of {- Prelude.Left p0 -> liveSet2;- Prelude.Right vid ->- case Prelude.not- (IntSet.coq_IntSet_member vid- (blockLiveKill liveSet2)) of {- Prelude.True -> Build_BlockLiveSets- (IntSet.coq_IntSet_insert vid- (blockLiveGen liveSet2))- (blockLiveKill liveSet2)- (blockLiveIn liveSet2)- (blockLiveOut liveSet2)- (blockFirstOpId liveSet2) lastIdx;- Prelude.False -> liveSet2}})}- in- let {- liveSet3 = List1.forFold liveSet2 others- (\liveSet3 v ->- case Blocks.varId maxReg v of {- Prelude.Left p0 -> liveSet3;- Prelude.Right vid ->- Build_BlockLiveSets- (blockLiveGen liveSet3)- (IntSet.coq_IntSet_insert vid- (blockLiveKill liveSet3))- (blockLiveIn liveSet3)- (blockLiveOut liveSet3)- (blockFirstOpId liveSet3) lastIdx})}- in- Build_BlockLiveSets (blockLiveGen liveSet3)- (blockLiveKill liveSet3) (blockLiveIn liveSet3)- (blockLiveOut liveSet3) (blockFirstOpId liveSet3)- lastIdx})}) of {- (,) lastIdx' liveSet3 ->- Monad.bind mDict (\k ->- Applicative.pure (Monad.is_applicative mDict) ((,) lastIdx'- (IntMap.coq_IntMap_insert k liveSet3 m)))- (Blocks.blockId mDict binfo b)}}}}))+ case computeLiveSets maxReg mDict binfo oinfo b idx+ emptyBlockLiveSets of {+ (,) idx' liveSets ->+ Monad.bind mDict (\k ->+ Applicative.pure (Monad.is_applicative mDict) ((,) idx'+ (IntMap.coq_IntMap_insert k liveSets m)))+ (Blocks.blockId mDict binfo b)}})) +updateLiveSets :: (IntMap.IntMap BlockLiveSets) -> ([] Blocks.BlockId) ->+ State.State BlockLiveSets ()+updateLiveSets blockLiveSets suxs =+ Monad.bind+ (State0.coq_StateT_Monad (unsafeCoerce Identity.coq_Identity_Monad))+ (\x ->+ Monad.bind (unsafeCoerce State.coq_State_Monad) (\x0 ->+ Monad.bind (unsafeCoerce State.coq_State_Monad) (\ls ->+ Lens.modifyStateT (\_ -> _blockLiveIn)+ (IntSet.coq_IntSet_union+ (IntSet.coq_IntSet_difference (blockLiveOut ls)+ (blockLiveKill ls)) (blockLiveGen ls))+ (unsafeCoerce Identity.coq_Identity_Monad))+ (unsafeCoerce State.get))+ (Monad.forM_ (unsafeCoerce State.coq_State_Monad) suxs (\s_bid ->+ case IntMap.coq_IntMap_lookup s_bid blockLiveSets of {+ Prelude.Just sux ->+ Lens.applyStateT (\_ -> _blockLiveOut)+ (Prelude0.flip IntSet.coq_IntSet_union (blockLiveIn sux))+ (unsafeCoerce Identity.coq_Identity_Monad);+ Prelude.Nothing ->+ Applicative.pure (unsafeCoerce State.coq_State_Applicative) ()})))+ (Lens.modifyStateT (\_ -> _blockLiveOut) IntSet.emptyIntSet+ (unsafeCoerce Identity.coq_Identity_Monad))+ computeGlobalLiveSets :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] a1) -> (IntMap.IntMap BlockLiveSets) -> a5@@ -303,25 +387,10 @@ case IntMap.coq_IntMap_lookup bid liveSets1 of { Prelude.Just liveSet -> Monad.bind mDict (\suxs ->- let {- liveSet2 = List1.forFold liveSet suxs (\liveSet2 s_bid ->- case IntMap.coq_IntMap_lookup s_bid liveSets1 of {- Prelude.Just sux -> Build_BlockLiveSets- (blockLiveGen liveSet2) (blockLiveKill liveSet2)- (blockLiveIn liveSet2)- (IntSet.coq_IntSet_union (blockLiveOut liveSet2)- (blockLiveIn sux)) (blockFirstOpId liveSet2)- (blockLastOpId liveSet2);- Prelude.Nothing -> liveSet2})}- in- Applicative.pure (Monad.is_applicative mDict)- (IntMap.coq_IntMap_insert bid (Build_BlockLiveSets- (blockLiveGen liveSet2) (blockLiveKill liveSet2)- (IntSet.coq_IntSet_union- (IntSet.coq_IntSet_difference (blockLiveOut liveSet2)- (blockLiveKill liveSet2)) (blockLiveGen liveSet2))- (blockLiveOut liveSet2) (blockFirstOpId liveSet2)- (blockLastOpId liveSet2)) liveSets1))+ case updateLiveSets liveSets suxs liveSet of {+ (,) x liveSet' ->+ Applicative.pure (Monad.is_applicative mDict)+ (IntMap.coq_IntMap_insert bid liveSet' liveSets1)}) (Blocks.blockSuccessors mDict binfo b); Prelude.Nothing -> Applicative.pure (Monad.is_applicative mDict) liveSets1})
LinearScan/Logic.hs view
@@ -3,7 +3,7 @@ module LinearScan.Logic where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Loops.hs view
@@ -4,7 +4,7 @@ module LinearScan.Loops where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Main.hs view
@@ -3,7 +3,7 @@ module LinearScan.Main where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -71,11 +71,10 @@ (IntMap.IntMap LiveSets.BlockLiveSets) (IntMap.IntMap ([] Resolve.ResolvingMoveSet)) ([] blockType1) ([] blockType1) (Prelude.Either- (IntMap.IntMap ([] Verify.AllocError))- ([] blockType2)) (Prelude.Maybe- ScanStateDescSet) (Prelude.Maybe- ScanStateDescSet) - Loops.LoopState+ (IntMap.IntMap+ ((,) Verify.RegStateDescSet+ ([] Verify.AllocError))) ([] blockType2)) + (Prelude.Maybe ScanStateDescSet) (Prelude.Maybe ScanStateDescSet) Loops.LoopState linearScan :: (Monad.Monad a1) -> Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4 a5) -> (Blocks.OpInfo a1 a4 a5) -> Verify.UseVerifier@@ -90,7 +89,8 @@ let { opCount = (Prelude.succ) (Blocks.countOps dict binfo blocks1)} in- case Allocate.walkIntervals maxReg ( ssig) opCount of {+ case Allocate.walkIntervals maxReg ( ssig)+ (Ssrnat.double opCount) of { Prelude.Left p -> case p of { (,) err ssig' ->@@ -100,24 +100,29 @@ []) (Prelude.Just (toScanStateDescSet maxReg ( ssig))) (Prelude.Just (toScanStateDescSet maxReg ( ssig'))) loops)}; Prelude.Right ssig' ->- let {- sd = Allocate.finalizeScanState maxReg ( ssig')- (Ssrnat.double opCount)}- in- let {allocs = Allocate.determineAllocations maxReg sd} in- Monad.bind dict (\mappings ->- Monad.bind dict (\res ->- case res of {- (,) moves blocks2 ->- Applicative.pure (Monad.is_applicative dict)- (Build_Details Prelude.Nothing liveSets' moves blocks- blocks1 blocks2 (Prelude.Just- (toScanStateDescSet maxReg ( ssig))) (Prelude.Just- (toScanStateDescSet maxReg sd)) loops)})- (Assign.assignRegNum maxReg dict binfo oinfo useVerifier- allocs liveSets' mappings loops blocks1))- (Resolve.resolveDataFlow maxReg dict binfo allocs blocks1- liveSets')})+ case Allocate.finalizeScanState maxReg ( ssig')+ (Ssrnat.double opCount) of {+ Prelude.Left err ->+ Applicative.pure (Monad.is_applicative dict) (Build_Details+ (Prelude.Just ((,) err AllocatingRegistersFailed))+ liveSets' IntMap.emptyIntMap blocks blocks1 (Prelude.Right+ []) (Prelude.Just (toScanStateDescSet maxReg ( ssig)))+ (Prelude.Just (toScanStateDescSet maxReg ( ssig'))) loops);+ Prelude.Right s ->+ let {allocs = Allocate.determineAllocations maxReg s} in+ Monad.bind dict (\mappings ->+ Monad.bind dict (\res ->+ case res of {+ (,) moves blocks2 ->+ Applicative.pure (Monad.is_applicative dict)+ (Build_Details Prelude.Nothing liveSets' moves blocks+ blocks1 blocks2 (Prelude.Just+ (toScanStateDescSet maxReg ( ssig))) (Prelude.Just+ (toScanStateDescSet maxReg s)) loops)})+ (Assign.assignRegNum maxReg dict binfo oinfo useVerifier+ allocs liveSets' mappings loops blocks1))+ (Resolve.resolveDataFlow maxReg dict binfo allocs blocks1+ liveSets')}}) (Build.buildIntervals maxReg dict binfo oinfo blocks1 loops liveSets')) (LiveSets.computeGlobalLiveSetsRecursively dict binfo blocks1
LinearScan/Monad.hs view
@@ -3,7 +3,7 @@ module LinearScan.Monad where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Morph.hs view
@@ -4,7 +4,7 @@ module LinearScan.Morph where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Nat.hs view
@@ -3,7 +3,7 @@ module LinearScan.Nat where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/NonEmpty.hs view
@@ -3,7 +3,7 @@ module LinearScan.NonEmpty where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Prelude0.hs view
@@ -3,7 +3,7 @@ module LinearScan.Prelude0 where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Range.hs view
@@ -4,7 +4,7 @@ module LinearScan.Range where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -15,7 +15,6 @@ import qualified LinearScan.Datatypes as Datatypes import qualified LinearScan.List1 as List1-import qualified LinearScan.Prelude0 as Prelude0 import qualified LinearScan.Specif as Specif import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Eqtype as Eqtype@@ -134,23 +133,53 @@ transportSortedRanges b pos rp = rp -rangesIntersect :: RangeDesc -> RangeDesc -> Prelude.Bool-rangesIntersect x y =- (Prelude.||)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend x))- (unsafeCoerce (rend y)))- ((Prelude.&&) ((Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y))- ((Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x)))+hasInputsAt :: RangeDesc -> Prelude.Int -> Prelude.Bool+hasInputsAt rd pos =+ Data.List.foldl' (\b u ->+ case (Prelude.||) b+ ((Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (UsePos.uloc u))+ (unsafeCoerce pos))+ (Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (UsePos.uvar u)) (unsafeCoerce UsePos.Input))) of {+ Prelude.True -> Prelude.True;+ Prelude.False -> b}) Prelude.False (ups rd) -rangeIntersectionPoint :: RangeDesc -> RangeDesc -> Prelude.Maybe- Prelude0.Coq_oddnum-rangeIntersectionPoint x y =- case rangesIntersect (getRangeDesc x) (getRangeDesc y) of {+hasOnlyOutputsAt :: RangeDesc -> Prelude.Int -> Prelude.Bool+hasOnlyOutputsAt rd pos =+ let {+ xs = Prelude.filter (\u ->+ Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (UsePos.uloc u))+ (unsafeCoerce pos)) (ups rd)}+ in+ (Prelude.&&) ((Prelude.<=) ((Prelude.succ) 0) (Data.List.length xs))+ (Seq.all (\u ->+ Eqtype.eq_op UsePos.coq_VarKind_eqType (unsafeCoerce (UsePos.uvar u))+ (unsafeCoerce UsePos.Output)) xs)++rangesJoinedAt :: RangeDesc -> RangeDesc -> Prelude.Int -> Prelude.Bool+rangesJoinedAt x y pos =+ (Prelude.&&) (hasInputsAt x pos) (Prelude.not (hasOnlyOutputsAt y pos))++rangesIntersect :: RangeDesc -> RangeDesc -> Prelude.Maybe Prelude.Int+rangesIntersect x y =+ case (Prelude.&&) ((Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y))+ ((Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x)) of { Prelude.True -> Prelude.Just (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of { Prelude.True -> rbeg y; Prelude.False -> rbeg x});- Prelude.False -> Prelude.Nothing}+ Prelude.False ->+ case (Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend x))+ (unsafeCoerce (rbeg y))) (rangesJoinedAt x y (rend x)) of {+ Prelude.True -> Prelude.Just (rend x);+ Prelude.False ->+ case (Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend y))+ (unsafeCoerce (rbeg x))) (rangesJoinedAt y x (rend y)) of {+ Prelude.True -> Prelude.Just (rend y);+ Prelude.False -> Prelude.Nothing}}} findRangeUsePos :: RangeDesc -> (UsePos.UsePos -> Prelude.Bool) -> Prelude.Maybe UsePos.UsePos
LinearScan/Resolve.hs view
@@ -4,7 +4,7 @@ module LinearScan.Resolve where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -23,9 +23,9 @@ import qualified LinearScan.Interval as Interval import qualified LinearScan.List1 as List1 import qualified LinearScan.LiveSets as LiveSets-import qualified LinearScan.Maybe as Maybe import qualified LinearScan.Monad as Monad import qualified LinearScan.Prelude0 as Prelude0+import qualified LinearScan.Range as Range import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype@@ -59,31 +59,51 @@ data ResolvingMove = Move PhysReg Blocks.VarId PhysReg- | Swap PhysReg Blocks.VarId PhysReg Blocks.VarId+ | Transfer PhysReg Blocks.VarId PhysReg | Spill PhysReg Blocks.VarId | Restore Blocks.VarId PhysReg | AllocReg Blocks.VarId PhysReg | FreeReg PhysReg Blocks.VarId+ | Looped ResolvingMove +coq_ResolvingMove_rect :: Prelude.Int -> (PhysReg -> Blocks.VarId -> PhysReg+ -> a1) -> (PhysReg -> Blocks.VarId -> PhysReg ->+ a1) -> (PhysReg -> Blocks.VarId -> a1) ->+ (Blocks.VarId -> PhysReg -> a1) -> (Blocks.VarId ->+ PhysReg -> a1) -> (PhysReg -> Blocks.VarId -> a1)+ -> (ResolvingMove -> a1 -> a1) -> ResolvingMove ->+ a1+coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 r =+ case r of {+ Move p v p0 -> f p v p0;+ Transfer p v p0 -> f0 p v p0;+ Spill p v -> f1 p v;+ Restore v p -> f2 v p;+ AllocReg v p -> f3 v p;+ FreeReg p v -> f4 p v;+ Looped r0 -> f5 r0 (coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 r0)}+ data ResolvingMoveSet = RSMove Prelude.Int Blocks.VarId Prelude.Int- | RSSwap Prelude.Int Blocks.VarId Prelude.Int Blocks.VarId+ | RSTransfer Prelude.Int Blocks.VarId Prelude.Int | RSSpill Prelude.Int Blocks.VarId | RSRestore Blocks.VarId Prelude.Int | RSAllocReg Blocks.VarId Prelude.Int | RSFreeReg Prelude.Int Blocks.VarId- | RSAssignReg Prelude.Int Blocks.VarId+ | RSAssignReg Blocks.VarId Prelude.Int | RSClearReg Prelude.Int Blocks.VarId+ | RSLooped ResolvingMoveSet weakenResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMoveSet weakenResolvingMove maxReg x = case x of { Move fr fv tr -> RSMove ( fr) fv ( tr);- Swap fr fv tr tv -> RSSwap ( fr) fv ( tr) tv;+ Transfer fr fv tr -> RSTransfer ( fr) fv ( tr); Spill fr tv -> RSSpill ( fr) tv; Restore fv tr -> RSRestore fv ( tr); AllocReg fv tr -> RSAllocReg fv ( tr);- FreeReg fr tv -> RSFreeReg ( fr) tv}+ FreeReg fr tv -> RSFreeReg ( fr) tv;+ Looped x0 -> RSLooped (weakenResolvingMove maxReg x0)} eqResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMove -> Prelude.Bool@@ -101,20 +121,17 @@ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce tr2))); _ -> Prelude.False};- Swap fr1 fv1 tr1 tv1 ->+ Transfer fr1 fv1 tr1 -> case s2 of {- Swap fr2 fv2 tr2 tv2 ->+ Transfer fr2 fv2 tr2 -> (Prelude.&&) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce fr2)) ((Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce fv2))- ((Prelude.&&)- (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)- (unsafeCoerce tr2))- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)- (unsafeCoerce tv2))));+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)+ (unsafeCoerce tr2))); _ -> Prelude.False}; Spill fr1 fv1 -> case s2 of {@@ -151,6 +168,10 @@ (unsafeCoerce fr2)) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce tv2));+ _ -> Prelude.False};+ Looped x ->+ case s2 of {+ Looped y -> eqResolvingMove maxReg x y; _ -> Prelude.False}} eqResolvingMoveP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResolvingMove@@ -232,24 +253,26 @@ Ssrbool.ReflectT -> _evar_0_ __; Ssrbool.ReflectF -> _evar_0_0 __}} in- let {_evar_0_0 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_0 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_1 = \fr2 fv2 -> Ssrbool.ReflectF} in let {_evar_0_2 = \tv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_3 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \fr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> unsafeCoerce _evar_0_ x x0 x1;- Swap x x0 x1 x2 -> _evar_0_0 x x0 x1 x2;+ Transfer x x0 x1 -> _evar_0_0 x x0 x1; Spill x x0 -> _evar_0_1 x x0; Restore x x0 -> _evar_0_2 x x0; AllocReg x x0 -> _evar_0_3 x x0;- FreeReg x x0 -> _evar_0_4 x x0}}+ FreeReg x x0 -> _evar_0_4 x x0;+ Looped x -> _evar_0_5 x}} in let {- _evar_0_0 = \fr1 fv1 tr1 tv1 _top_assumption_0 ->+ _evar_0_0 = \fr1 fv1 tr1 _top_assumption_0 -> let {_evar_0_0 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {- _evar_0_1 = \fr2 fv2 tr2 tv2 ->+ _evar_0_1 = \fr2 fv2 tr2 -> let { _evar_0_1 = \_ -> let {@@ -258,42 +281,10 @@ let { _evar_0_1 = let { _evar_0_1 = \_ ->- let {- _evar_0_1 = let {- _evar_0_1 = \_ ->- let {- _evar_0_1 = Ssrbool.ReflectT}- in- _evar_0_1}- in- let {- _evar_0_2 = \_ ->- Ssrbool.ReflectF}- in- case Eqtype.eqP- Ssrnat.nat_eqType- tv1 tv2 of {- Ssrbool.ReflectT ->- _evar_0_1 __;- Ssrbool.ReflectF ->- _evar_0_2 __}}- in+ let {_evar_0_1 = Ssrbool.ReflectT} in _evar_0_1} in- let {- _evar_0_2 = \_ ->- let {- _evar_0_2 = \_ ->- let {_evar_0_2 = Ssrbool.ReflectF} in- _evar_0_2}- in- let {- _evar_0_3 = \_ -> Ssrbool.ReflectF}- in- case Eqtype.eqP Ssrnat.nat_eqType tv1- tv2 of {- Ssrbool.ReflectT -> _evar_0_2 __;- Ssrbool.ReflectF -> _evar_0_3 __}}+ let {_evar_0_2 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg)@@ -307,33 +298,9 @@ _evar_0_2 = \_ -> let { _evar_0_2 = \_ ->- let {- _evar_0_2 = let {- _evar_0_2 = \_ ->- let {_evar_0_2 = Ssrbool.ReflectF} in- _evar_0_2}- in- let {- _evar_0_3 = \_ -> Ssrbool.ReflectF}- in- case Eqtype.eqP Ssrnat.nat_eqType tv1- tv2 of {- Ssrbool.ReflectT -> _evar_0_2 __;- Ssrbool.ReflectF -> _evar_0_3 __}}- in- _evar_0_2}- in- let {- _evar_0_3 = \_ ->- let {- _evar_0_3 = \_ ->- let {_evar_0_3 = Ssrbool.ReflectF} in _evar_0_3}- in- let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in- case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {- Ssrbool.ReflectT -> _evar_0_3 __;- Ssrbool.ReflectF -> _evar_0_4 __}}+ let {_evar_0_2 = Ssrbool.ReflectF} in _evar_0_2} in+ let {_evar_0_3 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_2 __;@@ -352,33 +319,9 @@ let { _evar_0_2 = let { _evar_0_2 = \_ ->- let {- _evar_0_2 = let {- _evar_0_2 = \_ ->- let {_evar_0_2 = Ssrbool.ReflectF} in- _evar_0_2}- in- let {- _evar_0_3 = \_ -> Ssrbool.ReflectF}- in- case Eqtype.eqP Ssrnat.nat_eqType tv1- tv2 of {- Ssrbool.ReflectT -> _evar_0_2 __;- Ssrbool.ReflectF -> _evar_0_3 __}}- in- _evar_0_2}- in- let {- _evar_0_3 = \_ ->- let {- _evar_0_3 = \_ ->- let {_evar_0_3 = Ssrbool.ReflectF} in _evar_0_3}- in- let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in- case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {- Ssrbool.ReflectT -> _evar_0_3 __;- Ssrbool.ReflectF -> _evar_0_4 __}}+ let {_evar_0_2 = Ssrbool.ReflectF} in _evar_0_2} in+ let {_evar_0_3 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_2 __;@@ -390,29 +333,9 @@ _evar_0_3 = \_ -> let { _evar_0_3 = \_ ->- let {- _evar_0_3 = let {- _evar_0_3 = \_ ->- let {_evar_0_3 = Ssrbool.ReflectF} in _evar_0_3}- in- let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in- case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {- Ssrbool.ReflectT -> _evar_0_3 __;- Ssrbool.ReflectF -> _evar_0_4 __}}- in- _evar_0_3}- in- let {- _evar_0_4 = \_ ->- let {- _evar_0_4 = \_ ->- let {_evar_0_4 = Ssrbool.ReflectF} in _evar_0_4}- in- let {_evar_0_5 = \_ -> Ssrbool.ReflectF} in- case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {- Ssrbool.ReflectT -> _evar_0_4 __;- Ssrbool.ReflectF -> _evar_0_5 __}}+ let {_evar_0_3 = Ssrbool.ReflectF} in _evar_0_3} in+ let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}}@@ -429,18 +352,20 @@ let {_evar_0_3 = \tv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_0 x x0 x1;- Swap x x0 x1 x2 -> unsafeCoerce _evar_0_1 x x0 x1 x2;+ Transfer x x0 x1 -> unsafeCoerce _evar_0_1 x x0 x1; Spill x x0 -> _evar_0_2 x x0; Restore x x0 -> _evar_0_3 x x0; AllocReg x x0 -> _evar_0_4 x x0;- FreeReg x x0 -> _evar_0_5 x x0}}+ FreeReg x x0 -> _evar_0_5 x x0;+ Looped x -> _evar_0_6 x}} in let { _evar_0_1 = \fr1 fv1 _top_assumption_0 -> let {_evar_0_1 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_2 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let { _evar_0_3 = \fr2 fv2 -> let {@@ -474,18 +399,20 @@ let {_evar_0_4 = \tv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_1 x x0 x1;- Swap x x0 x1 x2 -> _evar_0_2 x x0 x1 x2;+ Transfer x x0 x1 -> _evar_0_2 x x0 x1; Spill x x0 -> unsafeCoerce _evar_0_3 x x0; Restore x x0 -> _evar_0_4 x x0; AllocReg x x0 -> _evar_0_5 x x0;- FreeReg x x0 -> _evar_0_6 x x0}}+ FreeReg x x0 -> _evar_0_6 x x0;+ Looped x -> _evar_0_7 x}} in let { _evar_0_2 = \tv1 tr1 _top_assumption_0 -> let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_3 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \fr2 fv2 -> Ssrbool.ReflectF} in let { _evar_0_5 = \tv2 tr2 ->@@ -519,18 +446,20 @@ in let {_evar_0_6 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \fr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_2 x x0 x1;- Swap x x0 x1 x2 -> _evar_0_3 x x0 x1 x2;+ Transfer x x0 x1 -> _evar_0_3 x x0 x1; Spill x x0 -> _evar_0_4 x x0; Restore x x0 -> unsafeCoerce _evar_0_5 x x0; AllocReg x x0 -> _evar_0_6 x x0;- FreeReg x x0 -> _evar_0_7 x x0}}+ FreeReg x x0 -> _evar_0_7 x x0;+ Looped x -> _evar_0_8 x}} in let { _evar_0_3 = \fv1 tr1 _top_assumption_0 -> let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_4 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fr2 fv2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \tv2 tr2 -> Ssrbool.ReflectF} in let {@@ -564,18 +493,20 @@ Ssrbool.ReflectF -> _evar_0_8 __}} in let {_evar_0_8 = \fr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_9 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_3 x x0 x1;- Swap x x0 x1 x2 -> _evar_0_4 x x0 x1 x2;+ Transfer x x0 x1 -> _evar_0_4 x x0 x1; Spill x x0 -> _evar_0_5 x x0; Restore x x0 -> _evar_0_6 x x0; AllocReg x x0 -> unsafeCoerce _evar_0_7 x x0;- FreeReg x x0 -> _evar_0_8 x x0}}+ FreeReg x x0 -> _evar_0_8 x x0;+ Looped x -> _evar_0_9 x}} in let { _evar_0_4 = \fr1 tv1 _top_assumption_0 -> let {_evar_0_4 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_5 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \fr2 fv2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \tv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \fv2 tr2 -> Ssrbool.ReflectF} in@@ -610,21 +541,46 @@ Ssrbool.ReflectT -> _evar_0_9 __; Ssrbool.ReflectF -> _evar_0_10 __}} in+ let {_evar_0_10 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_4 x x0 x1;- Swap x x0 x1 x2 -> _evar_0_5 x x0 x1 x2;+ Transfer x x0 x1 -> _evar_0_5 x x0 x1; Spill x x0 -> _evar_0_6 x x0; Restore x x0 -> _evar_0_7 x x0; AllocReg x x0 -> _evar_0_8 x x0;- FreeReg x x0 -> unsafeCoerce _evar_0_9 x x0}}+ FreeReg x x0 -> unsafeCoerce _evar_0_9 x x0;+ Looped x -> _evar_0_10 x}} in- case _top_assumption_ of {- Move x x0 x1 -> unsafeCoerce _evar_0_ x x0 x1;- Swap x x0 x1 x2 -> unsafeCoerce _evar_0_0 x x0 x1 x2;- Spill x x0 -> unsafeCoerce _evar_0_1 x x0;- Restore x x0 -> unsafeCoerce _evar_0_2 x x0;- AllocReg x x0 -> unsafeCoerce _evar_0_3 x x0;- FreeReg x x0 -> unsafeCoerce _evar_0_4 x x0}+ let {+ _evar_0_5 = \x iHx _top_assumption_0 ->+ let {_evar_0_5 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \fr2 fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \tv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_9 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_10 = \fr2 tv2 -> Ssrbool.ReflectF} in+ let {+ _evar_0_11 = \y ->+ let {iHx0 = iHx y} in+ let {_evar_0_11 = \_ -> Ssrbool.ReflectT} in+ let {_evar_0_12 = \_ -> Ssrbool.ReflectF} in+ case iHx0 of {+ Ssrbool.ReflectT -> _evar_0_11 __;+ Ssrbool.ReflectF -> _evar_0_12 __}}+ in+ case _top_assumption_0 of {+ Move x0 x1 x2 -> _evar_0_5 x0 x1 x2;+ Transfer x0 x1 x2 -> _evar_0_6 x0 x1 x2;+ Spill x0 x1 -> _evar_0_7 x0 x1;+ Restore x0 x1 -> _evar_0_8 x0 x1;+ AllocReg x0 x1 -> _evar_0_9 x0 x1;+ FreeReg x0 x1 -> _evar_0_10 x0 x1;+ Looped x0 -> _evar_0_11 x0}}+ in+ coq_ResolvingMove_rect maxReg (unsafeCoerce _evar_0_)+ (unsafeCoerce _evar_0_0) (unsafeCoerce _evar_0_1)+ (unsafeCoerce _evar_0_2) (unsafeCoerce _evar_0_3)+ (unsafeCoerce _evar_0_4) _evar_0_5 _top_assumption_ coq_ResolvingMove_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of ResolvingMove@@ -635,100 +591,144 @@ coq_ResolvingMove_eqType maxReg = unsafeCoerce (coq_ResolvingMove_eqMixin maxReg) -coq_ResGraphNode :: Prelude.Int -> Eqtype.Equality__Coq_type-coq_ResGraphNode maxReg =- Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType+data ResGraphNode =+ RegNode PhysReg+ | VarNode Blocks.VarId+ | VirtNode ResGraphNode +coq_ResGraphNode_rect :: Prelude.Int -> (PhysReg -> a1) -> (Blocks.VarId ->+ a1) -> (ResGraphNode -> a1 -> a1) -> ResGraphNode ->+ a1+coq_ResGraphNode_rect maxReg f f0 f1 r =+ case r of {+ RegNode p -> f p;+ VarNode v -> f0 v;+ VirtNode r0 -> f1 r0 (coq_ResGraphNode_rect maxReg f f0 f1 r0)}++eqResGraphNode :: Prelude.Int -> ResGraphNode -> ResGraphNode -> Prelude.Bool+eqResGraphNode maxReg s1 s2 =+ case s1 of {+ RegNode r1 ->+ case s2 of {+ RegNode r2 ->+ Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce r1)+ (unsafeCoerce r2);+ _ -> Prelude.False};+ VarNode v1 ->+ case s2 of {+ VarNode v2 ->+ Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce v1) (unsafeCoerce v2);+ _ -> Prelude.False};+ VirtNode n1 ->+ case s2 of {+ VirtNode n2 -> eqResGraphNode maxReg n1 n2;+ _ -> Prelude.False}}++eqResGraphNodeP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResGraphNode+eqResGraphNodeP maxReg _top_assumption_ =+ let {+ _evar_0_ = \r1 _top_assumption_0 ->+ let {+ _evar_0_ = \r2 ->+ let {_evar_0_ = \_ -> let {_evar_0_ = Ssrbool.ReflectT} in _evar_0_}+ in+ let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) r1 r2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ let {_evar_0_0 = \v2 -> Ssrbool.ReflectF} in+ let {_evar_0_1 = \n2 -> Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ RegNode x -> unsafeCoerce _evar_0_ x;+ VarNode x -> _evar_0_0 x;+ VirtNode x -> _evar_0_1 x}}+ in+ let {+ _evar_0_0 = \v1 _top_assumption_0 ->+ let {_evar_0_0 = \r2 -> Ssrbool.ReflectF} in+ let {+ _evar_0_1 = \v2 ->+ let {+ _evar_0_1 = \_ -> let {_evar_0_1 = Ssrbool.ReflectT} in _evar_0_1}+ in+ let {_evar_0_2 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Ssrnat.nat_eqType v1 v2 of {+ Ssrbool.ReflectT -> _evar_0_1 __;+ Ssrbool.ReflectF -> _evar_0_2 __}}+ in+ let {_evar_0_2 = \n2 -> Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ RegNode x -> _evar_0_0 x;+ VarNode x -> unsafeCoerce _evar_0_1 x;+ VirtNode x -> _evar_0_2 x}}+ in+ let {+ _evar_0_1 = \n1 iHn _top_assumption_0 ->+ let {_evar_0_1 = \r2 -> Ssrbool.ReflectF} in+ let {_evar_0_2 = \v2 -> Ssrbool.ReflectF} in+ let {+ _evar_0_3 = \n2 ->+ let {iHn0 = iHn n2} in+ let {_evar_0_3 = \_ -> Ssrbool.ReflectT} in+ let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in+ case iHn0 of {+ Ssrbool.ReflectT -> _evar_0_3 __;+ Ssrbool.ReflectF -> _evar_0_4 __}}+ in+ case _top_assumption_0 of {+ RegNode x -> _evar_0_1 x;+ VarNode x -> _evar_0_2 x;+ VirtNode x -> _evar_0_3 x}}+ in+ coq_ResGraphNode_rect maxReg (unsafeCoerce _evar_0_)+ (unsafeCoerce _evar_0_0) _evar_0_1 _top_assumption_++coq_ResGraphNode_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of+ ResGraphNode+coq_ResGraphNode_eqMixin maxReg =+ Eqtype.Equality__Mixin (eqResGraphNode maxReg) (eqResGraphNodeP maxReg)++coq_ResGraphNode_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type+coq_ResGraphNode_eqType maxReg =+ unsafeCoerce (coq_ResGraphNode_eqMixin maxReg)+ data ResGraphEdge =- Build_ResGraphEdge ResolvingMove Prelude.Bool (Prelude.Maybe- Eqtype.Equality__Coq_sort) - (Prelude.Maybe Eqtype.Equality__Coq_sort)+ Build_ResGraphEdge ResolvingMove Prelude.Bool resMove :: Prelude.Int -> ResGraphEdge -> ResolvingMove resMove maxReg r = case r of {- Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resMove0}+ Build_ResGraphEdge resMove0 resGhost0 -> resMove0} resGhost :: Prelude.Int -> ResGraphEdge -> Prelude.Bool resGhost maxReg r = case r of {- Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resGhost0}--resBeg :: Prelude.Int -> ResGraphEdge -> Prelude.Maybe- Eqtype.Equality__Coq_sort-resBeg maxReg r =- case r of {- Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resBeg0}--resEnd :: Prelude.Int -> ResGraphEdge -> Prelude.Maybe- Eqtype.Equality__Coq_sort-resEnd maxReg r =- case r of {- Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resEnd0}+ Build_ResGraphEdge resMove0 resGhost0 -> resGhost0} eqResGraphEdge :: Prelude.Int -> ResGraphEdge -> ResGraphEdge -> Prelude.Bool eqResGraphEdge maxReg s1 s2 = case s1 of {- Build_ResGraphEdge a1 b1 c1 d1 ->+ Build_ResGraphEdge a1 b1 -> case s2 of {- Build_ResGraphEdge a2 b2 c2 d2 ->+ Build_ResGraphEdge a2 b2 -> (Prelude.&&) (Eqtype.eq_op (coq_ResolvingMove_eqType maxReg) (unsafeCoerce a1) (unsafeCoerce a2))- ((Prelude.&&)- (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1)- (unsafeCoerce b2))- ((Prelude.&&)- (Eqtype.eq_op (Eqtype.option_eqType (coq_ResGraphNode maxReg))- (unsafeCoerce c1) (unsafeCoerce c2))- (Eqtype.eq_op (Eqtype.option_eqType (coq_ResGraphNode maxReg))- (unsafeCoerce d1) (unsafeCoerce d2))))}}+ (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1) (unsafeCoerce b2))}} eqResGraphEdgeP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResGraphEdge eqResGraphEdgeP maxReg _top_assumption_ = let {- _evar_0_ = \a1 b1 c1 d1 _top_assumption_0 ->+ _evar_0_ = \a1 b1 _top_assumption_0 -> let {- _evar_0_ = \a2 b2 c2 d2 ->+ _evar_0_ = \a2 b2 -> let { _evar_0_ = \_ -> let { _evar_0_ = let { _evar_0_ = \_ ->- let {- _evar_0_ = let {- _evar_0_ = \_ ->- let {- _evar_0_ = let {- _evar_0_ = \_ ->- let {- _evar_0_ = Ssrbool.ReflectT}- in- _evar_0_}- in- let {- _evar_0_0 = \_ ->- Ssrbool.ReflectF}- in- case Eqtype.eqP- (Eqtype.option_eqType- (coq_ResGraphNode- maxReg)) d1 d2 of {- Ssrbool.ReflectT ->- _evar_0_ __;- Ssrbool.ReflectF ->- _evar_0_0 __}}- in- _evar_0_}- in- let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in- case Eqtype.eqP- (Eqtype.option_eqType- (coq_ResGraphNode maxReg)) c1 c2 of {- Ssrbool.ReflectT -> _evar_0_ __;- Ssrbool.ReflectF -> _evar_0_0 __}}- in- _evar_0_}+ let {_evar_0_ = Ssrbool.ReflectT} in _evar_0_} in let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {@@ -743,10 +743,10 @@ Ssrbool.ReflectF -> _evar_0_0 __}} in case _top_assumption_0 of {- Build_ResGraphEdge x x0 x1 x2 -> unsafeCoerce _evar_0_ x x0 x1 x2}}+ Build_ResGraphEdge x x0 -> unsafeCoerce _evar_0_ x x0}} in case _top_assumption_ of {- Build_ResGraphEdge x x0 x1 x2 -> unsafeCoerce _evar_0_ x x0 x1 x2}+ Build_ResGraphEdge x x0 -> unsafeCoerce _evar_0_ x x0} coq_ResGraphEdge_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of ResGraphEdge@@ -757,53 +757,97 @@ coq_ResGraphEdge_eqType maxReg = unsafeCoerce (coq_ResGraphEdge_eqMixin maxReg) -determineEdge :: Prelude.Int -> ResGraphEdge -> (,)- (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort)+determineEdge :: Prelude.Int -> ResGraphEdge -> (,) ResGraphNode ResGraphNode determineEdge maxReg x =- (,) (resBeg maxReg x) (resEnd maxReg x)+ let {+ go m =+ case m of {+ Move fr fv tr -> (,) (RegNode tr) (RegNode fr);+ Transfer fr fv tr -> (,) (RegNode tr) (RegNode fr);+ Spill fr tv -> (,) (VirtNode (VarNode tv)) (RegNode fr);+ Restore fv tr -> (,) (RegNode tr) (VarNode fv);+ AllocReg fv tr -> (,) (RegNode tr) (VarNode fv);+ FreeReg fr tv -> (,) (VirtNode (VarNode tv)) (RegNode fr);+ Looped x0 -> go x0}}+ in go (resMove maxReg x) +compareEdges :: Prelude.Int -> ((,) Prelude.Int ResGraphEdge) -> ((,)+ Prelude.Int ResGraphEdge) -> Prelude.Bool+compareEdges maxReg x y =+ let {xe = determineEdge maxReg (Prelude.snd x)} in+ let {ye = determineEdge maxReg (Prelude.snd y)} in+ case (Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (Prelude.fst (unsafeCoerce x))+ (Prelude.fst (unsafeCoerce y)))+ (Eqtype.eq_op (coq_ResGraphNode_eqType maxReg)+ (Prelude.fst (unsafeCoerce xe)) (Prelude.fst (unsafeCoerce ye))) of {+ Prelude.True ->+ (Prelude.&&) (resGhost maxReg (Prelude.snd x))+ (Prelude.not (resGhost maxReg (Prelude.snd y)));+ Prelude.False -> Prelude.False}++isEdgeSplittable :: Prelude.Int -> ResGraphEdge -> Prelude.Bool+isEdgeSplittable maxReg x =+ case resMove maxReg x of {+ Move p v p0 -> Prelude.True;+ Transfer p v p0 -> Prelude.True;+ _ -> Prelude.False}+ splitEdge :: Prelude.Int -> ResGraphEdge -> [] ResGraphEdge splitEdge maxReg x = case resMove maxReg x of {- Move fr fv tr -> (:) (Build_ResGraphEdge (Spill fr fv) Prelude.False- (resBeg maxReg x) Prelude.Nothing) ((:) (Build_ResGraphEdge (Restore fv- tr) (resGhost maxReg x) Prelude.Nothing (resEnd maxReg x)) []);- Swap fr fv tr tv -> (:) (Build_ResGraphEdge (Swap tr tv fr fv)- (resGhost maxReg x) (resEnd maxReg x) (resBeg maxReg x)) [];- _ -> []}+ Move fr fv tr -> (:) (Build_ResGraphEdge (Spill fr fv) Prelude.False) ((:)+ (Build_ResGraphEdge (Restore fv tr) (resGhost maxReg x)) []);+ Transfer fr fv tr -> (:) (Build_ResGraphEdge (FreeReg fr fv)+ Prelude.False) ((:) (Build_ResGraphEdge (AllocReg fv tr)+ (resGhost maxReg x)) []);+ Looped r -> (:) x [];+ _ -> (:) (Build_ResGraphEdge (Looped (resMove maxReg x))+ (resGhost maxReg x)) []} -determineMoves :: Prelude.Int -> (IntMap.IntMap ResGraphEdge) -> []+sortMoves :: Prelude.Int -> Graph.Graph -> [] ResGraphEdge+sortMoves maxReg x =+ Prelude.map (\i -> Prelude.snd (unsafeCoerce i))+ (List1.sortBy (unsafeCoerce (compareEdges maxReg))+ (Prelude.snd+ (Graph.topsort (coq_ResGraphNode_eqType maxReg)+ (coq_ResGraphEdge_eqType maxReg) x+ (unsafeCoerce (isEdgeSplittable maxReg))+ (unsafeCoerce (splitEdge maxReg)))))++determineMoves :: Prelude.Int -> (IntMap.IntMap ([] ResGraphEdge)) -> [] ResGraphEdge determineMoves maxReg moves =- unsafeCoerce- (Graph.topsort (coq_ResGraphNode maxReg) (coq_ResGraphEdge_eqType maxReg)- (IntMap.coq_IntMap_foldl- (Prelude0.flip+ sortMoves maxReg+ (IntMap.coq_IntMap_foldr+ (Prelude0.flip+ (Prelude.foldr (unsafeCoerce- (Graph.addEdge (coq_ResGraphNode maxReg)- (coq_ResGraphEdge_eqType maxReg))))- (Graph.emptyGraph (coq_ResGraphNode maxReg)- (coq_ResGraphEdge_eqType maxReg)- (unsafeCoerce (determineEdge maxReg))) moves)- (unsafeCoerce (splitEdge maxReg)))+ (Graph.addEdge (coq_ResGraphNode_eqType maxReg)+ (coq_ResGraphEdge_eqType maxReg)))))+ (Graph.emptyGraph (coq_ResGraphNode_eqType maxReg)+ (coq_ResGraphEdge_eqType maxReg)+ (unsafeCoerce (determineEdge maxReg))) moves) -resolvingMoves :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int ->- Prelude.Int -> IntMap.IntMap ResGraphEdge-resolvingMoves maxReg allocs from to =+resolvingMoves :: Prelude.Int -> ([] Allocate.Allocation) -> (Prelude.Maybe+ IntSet.IntSet) -> Prelude.Int -> Prelude.Int ->+ IntMap.IntMap ([] ResGraphEdge)+resolvingMoves maxReg allocs liveIn from to = let {- liveAtFrom = IntMap.coq_IntMap_fromList- (Prelude.map (\i -> (,)- (Interval.ivar (Allocate.intVal maxReg i)) i)- (Prelude.filter (\i ->- (Prelude.&&)- ((Prelude.<=)- (Interval.ibeg (Allocate.intVal maxReg i)) from)- ((Prelude.<=) ((Prelude.succ) from)- (Interval.iend (Allocate.intVal maxReg i))))- allocs))}+ collect = \p q i rest ->+ let {int = Allocate.intVal maxReg i} in+ case p int of {+ Prelude.True -> IntMap.coq_IntMap_alter (q i) (Interval.ivar int) rest;+ Prelude.False -> rest}} in let {+ liveAtFrom = Prelude.foldr+ (collect (\i ->+ (Prelude.&&) ((Prelude.<=) (Interval.ibeg i) from)+ ((Prelude.<=) ((Prelude.succ) from) (Interval.iend i)))+ (\a x -> Prelude.Just a)) IntMap.emptyIntMap allocs}+ in+ let { shouldKeep = \int pos -> case (Prelude.<=) (Interval.ibeg int) pos of { Prelude.True ->@@ -818,97 +862,170 @@ Prelude.False -> (,) Prelude.False Prelude.False}} in let {- liveAtTo = IntMap.coq_IntMap_fromList- (Prelude.map (\i -> (,)- (Interval.ivar (Allocate.intVal maxReg i)) ((,) i- (Prelude.snd (shouldKeep (Allocate.intVal maxReg i) to))))- (Prelude.filter (\i ->- Prelude.fst (shouldKeep (Allocate.intVal maxReg i) to))- allocs))}+ outputBegin = \int pos ->+ Range.hasOnlyOutputsAt ( (Prelude.head (Interval.rds int))) pos} in- IntMap.coq_IntMap_mergeWithKey (\vid x yp ->- case yp of {- (,) y ghost ->- case Eqtype.eq_op- (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))- (unsafeCoerce (Allocate.intReg maxReg x))- (unsafeCoerce (Allocate.intReg maxReg y)) of {- Prelude.True ->- case Allocate.intReg maxReg y of {- Prelude.Just reg ->- case ghost of {- Prelude.True -> Prelude.Just (Build_ResGraphEdge (FreeReg reg vid)- Prelude.True (Prelude.Just (unsafeCoerce (Prelude.Left reg)))- (Prelude.Just (unsafeCoerce (Prelude.Right vid))));- Prelude.False -> Prelude.Nothing};- Prelude.Nothing -> Prelude.Nothing};- Prelude.False ->- let {- mmv = case Allocate.intReg maxReg x of {- Prelude.Just xr ->- case Allocate.intReg maxReg y of {- Prelude.Just yr -> Prelude.Just (Move xr vid yr);- Prelude.Nothing -> Prelude.Just (Spill xr vid)};- Prelude.Nothing ->- case Allocate.intReg maxReg y of {- Prelude.Just xr -> Prelude.Just (Restore vid xr);- Prelude.Nothing -> Prelude.Nothing}}}- in- let {- anchor = \x0 ->- Applicative.choose (unsafeCoerce Maybe.option_Alternative)- (Functor.fmap (unsafeCoerce Maybe.coq_Maybe_Functor) (\x1 ->- Prelude.Left x1) (unsafeCoerce (Allocate.intReg maxReg x0)))- (Prelude.Just (Prelude.Right vid))}- in- case mmv of {- Prelude.Just mv -> Prelude.Just (Build_ResGraphEdge mv ghost- (unsafeCoerce anchor x) (unsafeCoerce anchor y));- Prelude.Nothing -> Prelude.Nothing}}})+ let {+ liveAtTo = Prelude.foldr+ (collect (\i -> Prelude.fst (shouldKeep i to)) (\a rest ->+ Prelude.Just ((:) ((,) ((,) a+ (Prelude.snd (shouldKeep (Allocate.intVal maxReg a) to)))+ (outputBegin (Allocate.intVal maxReg a) to))+ (case rest of {+ Prelude.Just xs -> xs;+ Prelude.Nothing -> []})))) IntMap.emptyIntMap allocs}+ in+ let {+ varNotLive = \vid ->+ case liveIn of {+ Prelude.Just ins -> Prelude.not (IntSet.coq_IntSet_member vid ins);+ Prelude.Nothing -> Prelude.False}}+ in+ let {+ regsReferenced = IntMap.coq_IntMap_mergeWithKey (\vid x yps ->+ let {+ go = \acc yp ->+ case yp of {+ (,) y0 y1 ->+ case y0 of {+ (,) y y2 ->+ case Prelude.not+ (Eqtype.eq_op+ (Eqtype.option_eqType+ (Fintype.ordinal_eqType maxReg))+ (unsafeCoerce+ (Allocate.intReg maxReg x))+ (unsafeCoerce+ (Allocate.intReg maxReg y))) of {+ Prelude.True ->+ let {+ next = case Allocate.intReg maxReg y of {+ Prelude.Just yreg -> (:) yreg acc;+ Prelude.Nothing -> acc}}+ in+ case Allocate.intReg maxReg x of {+ Prelude.Just xreg -> (:) xreg next;+ Prelude.Nothing -> next};+ Prelude.False -> acc}}}}+ in+ Prelude.Just (Data.List.foldl' go [] yps))+ (IntMap.coq_IntMap_foldlWithKey (\acc vid x ->+ case Allocate.intReg maxReg x of {+ Prelude.Just xreg ->+ IntMap.coq_IntMap_addToList vid xreg acc;+ Prelude.Nothing -> acc}) IntMap.emptyIntMap)+ (IntMap.coq_IntMap_foldlWithKey (\acc vid yps ->+ let {+ go = \acc0 yp ->+ case yp of {+ (,) y0 y1 ->+ case y0 of {+ (,) y y2 ->+ case Allocate.intReg maxReg y of {+ Prelude.Just yreg ->+ IntMap.coq_IntMap_addToList vid yreg acc0;+ Prelude.Nothing -> acc0}}}}+ in+ Data.List.foldl' go acc yps) IntMap.emptyIntMap)+ liveAtFrom liveAtTo}+ in+ let {+ otherRegs = List1.concat+ (Prelude.map (\x ->+ (Prelude..) (Prelude.map Prelude.id) Prelude.snd x)+ (IntMap.coq_IntMap_toList regsReferenced))}+ in+ IntMap.coq_IntMap_mergeWithKey (\vid x yps ->+ let {+ go = \yp ->+ case yp of {+ (,) y0 outb ->+ case y0 of {+ (,) y ghost ->+ case Eqtype.eq_op+ (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))+ (unsafeCoerce (Allocate.intReg maxReg x))+ (unsafeCoerce (Allocate.intReg maxReg y)) of {+ Prelude.True ->+ case Allocate.intReg maxReg y of {+ Prelude.Just reg ->+ case ghost of {+ Prelude.True -> (:) (Build_ResGraphEdge (FreeReg reg vid)+ Prelude.True) [];+ Prelude.False ->+ case IntSet.coq_IntSet_member ( reg) otherRegs of {+ Prelude.True -> (:) (Build_ResGraphEdge (FreeReg reg vid)+ Prelude.False) ((:) (Build_ResGraphEdge (AllocReg vid reg)+ Prelude.False) []);+ Prelude.False -> []}};+ Prelude.Nothing -> []};+ Prelude.False ->+ let {+ mmv = case Allocate.intReg maxReg x of {+ Prelude.Just xr ->+ case Allocate.intReg maxReg y of {+ Prelude.Just yr -> Prelude.Just+ (case (Prelude.||) outb (varNotLive vid) of {+ Prelude.True -> Transfer xr vid yr;+ Prelude.False -> Move xr vid yr});+ Prelude.Nothing -> Prelude.Just (Spill xr vid)};+ Prelude.Nothing ->+ case Allocate.intReg maxReg y of {+ Prelude.Just yr -> Prelude.Just+ (case (Prelude.||) outb (varNotLive vid) of {+ Prelude.True -> AllocReg vid yr;+ Prelude.False -> Restore vid yr});+ Prelude.Nothing -> Prelude.Nothing}}}+ in+ case mmv of {+ Prelude.Just mv -> (:) (Build_ResGraphEdge mv ghost) [];+ Prelude.Nothing -> []}}}}}+ in+ List1.listToMaybe+ (Data.List.foldl' (\acc x0 -> (Prelude.++) acc (go x0)) [] yps)) (IntMap.coq_IntMap_foldlWithKey (\acc vid x -> case Allocate.intReg maxReg x of { Prelude.Just r ->- IntMap.coq_IntMap_insert vid (Build_ResGraphEdge (FreeReg r vid)- Prelude.False (Prelude.Just (unsafeCoerce (Prelude.Left r)))- (Prelude.Just (unsafeCoerce (Prelude.Right vid)))) acc;+ IntMap.coq_IntMap_addToList vid (Build_ResGraphEdge (FreeReg r vid)+ Prelude.False) acc; Prelude.Nothing -> acc}) IntMap.emptyIntMap)- (IntMap.coq_IntMap_foldlWithKey (\acc vid yp ->- case yp of {- (,) y ghost ->- case Allocate.intReg maxReg y of {- Prelude.Just r ->- IntMap.coq_IntMap_insert vid (Build_ResGraphEdge (AllocReg vid r)- ghost (Prelude.Just (unsafeCoerce (Prelude.Right vid)))- (Prelude.Just (unsafeCoerce (Prelude.Left r)))) acc;- Prelude.Nothing -> acc}}) IntMap.emptyIntMap) liveAtFrom liveAtTo+ (IntMap.coq_IntMap_foldlWithKey (\acc vid yps ->+ let {+ go = \acc0 yp ->+ case yp of {+ (,) y0 outb ->+ case y0 of {+ (,) y ghost ->+ case Allocate.intReg maxReg y of {+ Prelude.Just r ->+ IntMap.coq_IntMap_addToList vid (Build_ResGraphEdge (AllocReg+ vid r) ghost) acc0;+ Prelude.Nothing -> acc0}}}}+ in+ Data.List.foldl' go acc yps) IntMap.emptyIntMap) liveAtFrom liveAtTo type BlockMoves = (,) Graph.Graph Graph.Graph -movesBetween :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int ->- Prelude.Int -> [] ResGraphEdge-movesBetween maxReg allocs from to =- IntMap.coq_IntMap_foldl (Prelude0.flip (\x x0 -> (:) x x0)) []- (resolvingMoves maxReg allocs from to)- applyMappings :: Prelude.Int -> Blocks.BlockId -> (IntMap.IntMap BlockMoves)- -> Prelude.Bool -> ([] ResGraphEdge) -> IntMap.IntMap- BlockMoves+ -> Prelude.Bool -> (IntMap.IntMap ([] ResGraphEdge)) ->+ IntMap.IntMap BlockMoves applyMappings maxReg bid mappings in_from moves =- List1.forFold mappings (unsafeCoerce moves) (\ms mv ->+ let {+ go = \ms mv -> let { addToGraphs = \e xs -> case xs of { (,) gbeg gend -> case in_from of { Prelude.True -> (,) gbeg- (Graph.addEdge (coq_ResGraphNode maxReg)+ (Graph.addEdge (coq_ResGraphNode_eqType maxReg) (coq_ResGraphEdge_eqType maxReg) e gend); Prelude.False -> (,)- (Graph.addEdge (coq_ResGraphNode maxReg)+ (Graph.addEdge (coq_ResGraphNode_eqType maxReg) (coq_ResGraphEdge_eqType maxReg) e gbeg) gend}}} in let {- eg = Graph.emptyGraph (coq_ResGraphNode maxReg)+ eg = Graph.emptyGraph (coq_ResGraphNode_eqType maxReg) (coq_ResGraphEdge_eqType maxReg) (unsafeCoerce (determineEdge maxReg))} in@@ -919,7 +1036,9 @@ Prelude.Just xs -> xs; Prelude.Nothing -> (,) eg eg})} in- IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms)+ IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms}+ in+ IntMap.coq_IntMap_foldl (Data.List.foldl' (unsafeCoerce go)) mappings moves checkBlockBoundary :: Prelude.Int -> ([] Allocate.Allocation) -> Blocks.BlockId -> Prelude.Bool ->@@ -928,8 +1047,8 @@ IntMap.IntMap BlockMoves checkBlockBoundary maxReg allocs bid in_from from to liveIn mappings = applyMappings maxReg bid mappings in_from- (movesBetween maxReg allocs (LiveSets.blockLastOpId from)- (LiveSets.blockFirstOpId to))+ (resolvingMoves maxReg allocs (Prelude.Just liveIn)+ (LiveSets.blockLastOpId from) (LiveSets.blockFirstOpId to)) resolveDataFlow :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] Allocate.Allocation) -> ([] @@ -948,7 +1067,8 @@ mappings' = case isFirst of { Prelude.True -> applyMappings maxReg bid mappings Prelude.False- (movesBetween maxReg allocs ((Prelude.succ) 0)+ (resolvingMoves maxReg allocs Prelude.Nothing+ ((Prelude.succ) 0) (LiveSets.blockFirstOpId from)); Prelude.False -> mappings}} in@@ -961,12 +1081,7 @@ mappings'' = case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Data.List.length suxs)) (unsafeCoerce 0) of {- Prelude.True ->- applyMappings maxReg bid mappings' Prelude.True- (movesBetween maxReg allocs- (LiveSets.blockLastOpId from)- ((Prelude.succ) ((Prelude.succ)- (LiveSets.blockLastOpId from))));+ Prelude.True -> mappings'; Prelude.False -> List1.forFold mappings' suxs (\ms s_bid -> case IntMap.coq_IntMap_lookup s_bid liveSets of {
LinearScan/ScanState.hs view
@@ -1,9 +1,10 @@-+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -} module LinearScan.ScanState where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -14,11 +15,32 @@ import qualified LinearScan.Interval as Interval import qualified LinearScan.List1 as List1-import qualified LinearScan.Prelude0 as Prelude0 import qualified LinearScan.Vector0 as Vector0+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrbool as Ssrbool ++#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+import qualified GHC.Prim as GHC.Prim+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+#endif+++#ifdef __GLASGOW_HASKELL__+--unsafeCoerce :: a -> b+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+--unsafeCoerce :: a -> b+unsafeCoerce = IOExts.unsafeCoerce+#endif+ type PhysReg = Prelude.Int type FixedIntervalsType = Vector0.Vec (Prelude.Maybe Interval.IntervalDesc)@@ -79,9 +101,13 @@ Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0 active0 inactive0 handled0 -> handled0} +handledIds :: Prelude.Int -> ScanStateDesc -> [] IntervalId+handledIds maxReg s =+ Prelude.map (\i -> Prelude.fst i) (handled maxReg s)+ sortRegisterVector :: Prelude.Int -> (Vector0.Vec Prelude.Bool) ->- (Vector0.Vec (Prelude.Maybe Prelude0.Coq_oddnum)) -> []- ((,) PhysReg (Prelude.Maybe Prelude0.Coq_oddnum))+ (Vector0.Vec (Prelude.Maybe Prelude.Int)) -> []+ ((,) PhysReg (Prelude.Maybe Prelude.Int)) sortRegisterVector maxReg fixedAndIntersects = Vector0.vfoldl_with_index maxReg (\reg acc mpos -> let {@@ -98,18 +124,44 @@ case xmpos of { Prelude.Just xn -> case ympos of {- Prelude.Just yn -> (Prelude.<=) ((Prelude.succ) ( yn)) ( xn);+ Prelude.Just yn -> (Prelude.<=) ((Prelude.succ) yn) xn; Prelude.Nothing -> Prelude.False}; Prelude.Nothing -> Prelude.True}}}}} in List1.insert f ((,) reg mpos) acc) [] registerWithHighestPos :: Prelude.Int -> (Vector0.Vec Prelude.Bool) ->- (Vector0.Vec (Prelude.Maybe Prelude0.Coq_oddnum))- -> (,) PhysReg (Prelude.Maybe Prelude0.Coq_oddnum)+ (Vector0.Vec (Prelude.Maybe Prelude.Int)) -> (,)+ PhysReg (Prelude.Maybe Prelude.Int) registerWithHighestPos maxReg fixedAndIntersects =- (Prelude..) (Seq.head ((,) ( 0) (Prelude.Just Prelude0.odd1)))+ (Prelude..) (Seq.head ((,) ( 0) (Prelude.Just 0))) (sortRegisterVector maxReg fixedAndIntersects)++handledIntervalDescsForReg :: Prelude.Int -> ScanStateDesc -> PhysReg -> []+ Interval.IntervalDesc+handledIntervalDescsForReg maxReg sd reg =+ Prelude.map (\x ->+ Interval.getIntervalDesc+ (+ (Vector0.vnth (nextInterval maxReg sd) (intervals maxReg sd)+ (Prelude.fst x))))+ (Prelude.filter (\x ->+ Eqtype.eq_op (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))+ (Prelude.snd (unsafeCoerce x)) (unsafeCoerce (Prelude.Just reg)))+ (handled maxReg sd))++verifyNewHandled :: Prelude.Int -> ScanStateDesc -> Interval.IntervalDesc ->+ PhysReg -> Prelude.Bool+verifyNewHandled maxReg sd int reg =+ let {+ check = \y ->+ Prelude.not (Ssrbool.isSome (Interval.intervalsIntersect int y))}+ in+ (Prelude.&&) (Seq.all check (handledIntervalDescsForReg maxReg sd reg))+ (case Vector0.vnth maxReg (fixedIntervals maxReg sd) reg of {+ Prelude.Just i ->+ Prelude.not (Ssrbool.isSome (Interval.intervalsOverlap int ( i)));+ Prelude.Nothing -> Prelude.True}) data ScanStateStatus = Pending
LinearScan/Seq.hs view
@@ -4,7 +4,7 @@ module LinearScan.Seq where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -114,6 +114,12 @@ [] -> 0; (:) x s' -> (Prelude.+) (Ssrnat.nat_of_bool (a x)) (count a s')} +all :: (Ssrbool.Coq_pred a1) -> ([] a1) -> Prelude.Bool+all a s =+ case s of {+ [] -> Prelude.True;+ (:) x s' -> (Prelude.&&) (a x) (all a s')}+ drop :: Prelude.Int -> ([] a1) -> [] a1 drop n s = case s of {@@ -126,16 +132,6 @@ drop n' s') n} -catrev :: ([] a1) -> ([] a1) -> [] a1-catrev s1 s2 =- case s1 of {- [] -> s2;- (:) x s1' -> catrev s1' ((:) x s2)}--rev :: ([] a1) -> [] a1-rev s =- catrev s []- eqseq :: Eqtype.Equality__Coq_type -> ([] Eqtype.Equality__Coq_sort) -> ([] Eqtype.Equality__Coq_sort) -> Prelude.Bool eqseq t s1 s2 =@@ -244,4 +240,8 @@ (\n' -> (:) m (iota ((Prelude.succ) m) n')) n++flatten :: ([] ([] a1)) -> [] a1+flatten =+ Prelude.foldr (Prelude.++) []
LinearScan/Specif.hs view
@@ -3,7 +3,7 @@ module LinearScan.Specif where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Spill.hs view
@@ -4,7 +4,7 @@ module LinearScan.Spill where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -22,7 +22,9 @@ import qualified LinearScan.Trace as Trace import qualified LinearScan.Vector0 as Vector0 import qualified LinearScan.Eqtype as Eqtype-import qualified LinearScan.Ssrnat as Ssrnat+import qualified LinearScan.Fintype as Fintype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrbool as Ssrbool @@ -65,6 +67,16 @@ InactiveToHandled xid reg -> Trace.InactiveToHandledT ( xid) ( (unsafeCoerce reg))} +optimalSplitPosition :: Interval.IntervalDesc -> Prelude.Int -> Prelude.Int+ -> Prelude.Int+optimalSplitPosition d lb ub =+ case (Prelude.&&)+ ((Prelude.||) (Interval.posAtRangeEnd d ub)+ (Interval.intervalHasInputsAt (Interval.getIntervalDesc d) ub))+ ((Prelude.<=) ((Prelude.succ) lb) ub) of {+ Prelude.True -> Prelude.pred ub;+ Prelude.False -> ub}+ spillInterval :: Prelude.Int -> ScanState.ScanStateDesc -> Interval.IntervalDesc -> ScanState.IntervalId -> Prelude.Int -> ([] ((,) ScanState.IntervalId Prelude.Int)) ->@@ -76,8 +88,11 @@ let { _evar_0_ = \_top_assumption_ -> (Prelude.flip (Prelude.$)) ((:) (Trace.EIntervalHasUsePosReqReg- _top_assumption_) e2) (\e3 ->+ ( _top_assumption_)) e2) (\e3 -> let {+ optSplitPos2 = optimalSplitPosition ( i1) beg ( _top_assumption_)}+ in+ let { _evar_0_ = \_ -> let { _evar_0_ = \_ ->@@ -102,7 +117,8 @@ _evar_0_)} in let {- _evar_0_0 = \_ -> Prelude.Left ((:) Trace.ECannotInsertUnhandled+ _evar_0_0 = \_ -> Prelude.Left ((:) (Trace.ECannotInsertUnhandled+ beg (Interval.ibeg ( i1)) optSplitPos2 (Interval.iend ( i1))) ((:) Trace.EIntervalBeginsAtSplitPosition e3))} in case (Prelude.<=) ((Prelude.succ) beg) (Interval.ibeg ( i1)) of {@@ -113,15 +129,14 @@ _evar_0_0 = \_ -> (Prelude.flip (Prelude.$)) __ (\_ -> let {- _top_assumption_0 = Interval.splitInterval ( i1)- _top_assumption_}+ _top_assumption_0 = Interval.splitInterval ( i1) optSplitPos2} in let { _evar_0_0 = \i1_0 i1_1 -> let { _evar_0_0 = \_top_assumption_1 -> Prelude.Left ((:)- (Trace.ECannotSpillIfRegisterRequired ( _top_assumption_1))- e3)}+ (Trace.ECannotSpillIfRegisterRequiredBefore optSplitPos2+ ( _top_assumption_1)) e3)} in let { _evar_0_1 = \_ ->@@ -201,35 +216,103 @@ _evar_0_2 = \_ -> (Prelude.flip (Prelude.$)) __ (\_ -> (Prelude.flip (Prelude.$)) __- (\_ _ ->+ (\_ -> let {- _evar_0_2 = \_ _ _ ->- let {- b = Prelude0.lebf Prelude.snd- (Prelude.id ((,) uid- beg)) ((,)- (- (ScanState.nextInterval- maxReg sd))- (Interval.ibeg ( i1_1)))}- in+ _evar_0_2 = \_ _ -> let {- _evar_0_2 = \_ ->- Logic.coq_False_rect}+ _evar_0_2 = \_ _ _ ->+ let {+ b = Prelude0.lebf+ Prelude.snd+ (Prelude.id ((,) uid+ beg)) ((,)+ (+ (ScanState.nextInterval+ maxReg sd))+ (Interval.ibeg+ ( i1_1)))}+ in+ let {+ _evar_0_2 = \_ ->+ Logic.coq_False_rect}+ in+ let {+ _evar_0_3 = \_ ->+ Logic.coq_False_rect}+ in+ case b of {+ Prelude.True -> _evar_0_2 __;+ Prelude.False ->+ _evar_0_3 __}} in let {- _evar_0_3 = \_ ->- Logic.coq_False_rect}+ _evar_0_3 = \u' us' ->+ (Prelude.flip (Prelude.$)) __+ (\_ -> Prelude.Right+ (ScanState.Build_ScanStateDesc+ ((Prelude.succ)+ (ScanState.nextInterval+ maxReg sd))+ (Vector0.vreplace+ ((Prelude.succ)+ (ScanState.nextInterval+ maxReg sd))+ (unsafeCoerce+ (Vector0.vshiftin+ (ScanState.nextInterval+ maxReg sd)+ (ScanState.intervals+ maxReg sd) + ( i1_1))) ( uid)+ ( i1_0))+ (ScanState.fixedIntervals+ maxReg sd) us'+ (Prelude.map Prelude.id+ (ScanState.active maxReg+ sd))+ (Prelude.map Prelude.id+ (ScanState.inactive+ maxReg sd)) ((:) ((,)+ (Prelude.fst u')+ Prelude.Nothing)+ (Prelude.map Prelude.id+ (ScanState.handled maxReg+ sd)))))} in- case b of {- Prelude.True -> _evar_0_2 __;- Prelude.False -> _evar_0_3 __}}+ case unh' of {+ [] -> _evar_0_2 __ __ __;+ (:) x x0 -> _evar_0_3 x x0}} in let {- _evar_0_3 = \u' us' ->- (Prelude.flip (Prelude.$)) __- (\_ -> Prelude.Right- (ScanState.Build_ScanStateDesc+ _evar_0_3 = \_ _ -> Prelude.Left+ ((:)+ (Trace.ECannotModifyHandledInterval+ ( uid)) e3)}+ in+ case Prelude.not+ (Ssrbool.in_mem+ (unsafeCoerce ( uid))+ (Ssrbool.mem+ (Seq.seq_predType+ (Fintype.ordinal_eqType+ (ScanState.nextInterval+ maxReg sd')))+ (unsafeCoerce+ (ScanState.handledIds+ maxReg sd')))) of {+ Prelude.True -> _evar_0_2 __;+ Prelude.False -> _evar_0_3 __}))+ __}+ in+ let {+ _evar_0_3 = \xid reg ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$)) __+ (\_ ->+ let {+ _evar_0_3 = \_ _ ->+ let {+ sd'' = ScanState.Build_ScanStateDesc ((Prelude.succ) (ScanState.nextInterval maxReg sd))@@ -243,133 +326,142 @@ maxReg sd) (ScanState.intervals maxReg sd) ( i1_1)))- ( uid) ( i1_0))+ ( xid) ( i1_0)) (ScanState.fixedIntervals- maxReg sd) us'+ maxReg sd) unh' (Prelude.map Prelude.id (ScanState.active maxReg sd)) (Prelude.map Prelude.id (ScanState.inactive maxReg- sd)) ((:) ((,)- (Prelude.fst u')- Prelude.Nothing)+ sd)) (Prelude.map Prelude.id (ScanState.handled maxReg- sd)))))}- in- case unh' of {- [] -> _evar_0_2 __ __ __;- (:) x x0 -> _evar_0_3 x x0})) __}- in- let {- _evar_0_3 = \xid reg ->- (Prelude.flip (Prelude.$)) __ (\_ ->- (Prelude.flip (Prelude.$)) __- (\_ _ ->- let {- sd'' = ScanState.Build_ScanStateDesc- ((Prelude.succ)- (ScanState.nextInterval maxReg- sd))- (Vector0.vreplace- ((Prelude.succ)- (ScanState.nextInterval- maxReg sd))- (unsafeCoerce- (Vector0.vshiftin- (ScanState.nextInterval- maxReg sd)- (ScanState.intervals- maxReg sd) ( i1_1)))- ( xid) ( i1_0))- (ScanState.fixedIntervals- maxReg sd) unh'- (Prelude.map Prelude.id- (ScanState.active maxReg sd))- (Prelude.map Prelude.id- (ScanState.inactive maxReg- sd))- (Prelude.map Prelude.id- (ScanState.handled maxReg sd))}+ sd))}+ in+ let {+ elem = Prelude.id ((,) xid+ reg)}+ in+ (Prelude.flip (Prelude.$)) __+ (\_ ->+ let {+ _evar_0_3 = \a b ->+ (Prelude.flip (Prelude.$))+ __ (\_ ->+ let {+ _top_assumption_1 = + Morph.moveActiveToHandled+ maxReg sd''+ Prelude.True+ (unsafeCoerce ((,) a+ b))}+ in+ Prelude.Right+ _top_assumption_1)}+ in+ case elem of {+ (,) x x0 -> _evar_0_3 x x0})} in let {- elem = Prelude.id ((,) xid reg)}+ _evar_0_4 = \_ _ -> Prelude.Left+ ((:)+ (Trace.ECannotModifyHandledInterval+ ( xid)) e3)} in- (Prelude.flip (Prelude.$)) __- (\_ ->- let {- _evar_0_3 = \a b ->- (Prelude.flip (Prelude.$)) __- (\_ ->- let {- _top_assumption_1 = - Morph.moveActiveToHandled- maxReg sd''- Prelude.True- (unsafeCoerce ((,) a- b))}- in- Prelude.Right- _top_assumption_1)}- in- case elem of {- (,) x x0 -> _evar_0_3 x x0})))+ case Prelude.not+ (Ssrbool.in_mem+ (unsafeCoerce ( xid))+ (Ssrbool.mem+ (Seq.seq_predType+ (Fintype.ordinal_eqType+ (ScanState.nextInterval+ maxReg sd')))+ (unsafeCoerce+ (ScanState.handledIds+ maxReg sd')))) of {+ Prelude.True -> _evar_0_3 __;+ Prelude.False -> _evar_0_4 __})) __} in let { _evar_0_4 = \xid reg -> (Prelude.flip (Prelude.$)) __ (\_ -> (Prelude.flip (Prelude.$)) __- (\_ _ ->+ (\_ -> let {- sd'' = ScanState.Build_ScanStateDesc- ((Prelude.succ)- (ScanState.nextInterval maxReg- sd))- (Vector0.vreplace+ _evar_0_4 = \_ _ ->+ let {+ sd'' = ScanState.Build_ScanStateDesc ((Prelude.succ) (ScanState.nextInterval maxReg sd))- (unsafeCoerce- (Vector0.vshiftin- (ScanState.nextInterval- maxReg sd)- (ScanState.intervals- maxReg sd) ( i1_1)))- ( xid) ( i1_0))- (ScanState.fixedIntervals- maxReg sd) unh'- (Prelude.map Prelude.id- (ScanState.active maxReg sd))- (Prelude.map Prelude.id- (ScanState.inactive maxReg- sd))- (Prelude.map Prelude.id- (ScanState.handled maxReg sd))}+ (Vector0.vreplace+ ((Prelude.succ)+ (ScanState.nextInterval+ maxReg sd))+ (unsafeCoerce+ (Vector0.vshiftin+ (ScanState.nextInterval+ maxReg sd)+ (ScanState.intervals+ maxReg sd) ( i1_1)))+ ( xid) ( i1_0))+ (ScanState.fixedIntervals+ maxReg sd) unh'+ (Prelude.map Prelude.id+ (ScanState.active maxReg+ sd))+ (Prelude.map Prelude.id+ (ScanState.inactive maxReg+ sd))+ (Prelude.map Prelude.id+ (ScanState.handled maxReg+ sd))}+ in+ let {+ elem = Prelude.id ((,) xid+ reg)}+ in+ (Prelude.flip (Prelude.$)) __+ (\_ ->+ let {+ _evar_0_4 = \a b ->+ (Prelude.flip (Prelude.$))+ __ (\_ ->+ let {+ _top_assumption_1 = + Morph.moveInactiveToHandled+ maxReg sd''+ Prelude.True+ (unsafeCoerce ((,) a+ b))}+ in+ Prelude.Right+ _top_assumption_1)}+ in+ case elem of {+ (,) x x0 -> _evar_0_4 x x0})} in let {- elem = Prelude.id ((,) xid reg)}+ _evar_0_5 = \_ _ -> Prelude.Left+ ((:)+ (Trace.ECannotModifyHandledInterval+ ( xid)) e3)} in- (Prelude.flip (Prelude.$)) __- (\_ ->- let {- _evar_0_4 = \a b ->- (Prelude.flip (Prelude.$)) __- (\_ ->- let {- _top_assumption_1 = - Morph.moveInactiveToHandled- maxReg sd''- Prelude.True- (unsafeCoerce ((,) a- b))}- in- Prelude.Right- _top_assumption_1)}- in- case elem of {- (,) x x0 -> _evar_0_4 x x0})))+ case Prelude.not+ (Ssrbool.in_mem+ (unsafeCoerce ( xid))+ (Ssrbool.mem+ (Seq.seq_predType+ (Fintype.ordinal_eqType+ (ScanState.nextInterval+ maxReg sd')))+ (unsafeCoerce+ (ScanState.handledIds+ maxReg sd')))) of {+ Prelude.True -> _evar_0_4 __;+ Prelude.False -> _evar_0_5 __})) __} in case spill of {@@ -390,9 +482,7 @@ case _top_assumption_0 of { (,) x x0 -> _evar_0_0 x x0})} in- case Eqtype.eq_op Ssrnat.nat_eqType- (unsafeCoerce (Interval.ibeg ( i1)))- (unsafeCoerce _top_assumption_) of {+ case (Prelude.<=) optSplitPos2 (Interval.ibeg ( i1)) of { Prelude.True -> _evar_0_ __; Prelude.False -> _evar_0_0 __})} in@@ -430,20 +520,20 @@ _evar_0_1 __} in let {- _evar_0_2 = \xid _reg_ ->+ _evar_0_2 = \xid reg -> (Prelude.flip (Prelude.$)) __ (\_ -> let { _top_assumption_ = Morph.moveActiveToHandled maxReg sd- Prelude.True (unsafeCoerce ((,) xid _reg_))}+ Prelude.True (unsafeCoerce ((,) xid reg))} in Prelude.Right _top_assumption_)} in let {- _evar_0_3 = \xid _reg_ ->+ _evar_0_3 = \xid reg -> (Prelude.flip (Prelude.$)) __ (\_ -> let { _top_assumption_ = Morph.moveInactiveToHandled maxReg sd- Prelude.True (unsafeCoerce ((,) xid _reg_))}+ Prelude.True (unsafeCoerce ((,) xid reg))} in Prelude.Right _top_assumption_)} in
LinearScan/Split.hs view
@@ -4,7 +4,7 @@ module LinearScan.Split where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -55,17 +55,16 @@ type PhysReg = Prelude.Int data SplitPosition =- BeforePos Prelude0.Coq_oddnum- | EndOfLifetimeHole Prelude0.Coq_oddnum+ BeforePos Prelude.Int+ | EndOfLifetimeHole Prelude.Int coq_SplitPositionToT :: SplitPosition -> Trace.SplitPositionT coq_SplitPositionToT x = case x of {- BeforePos n -> Trace.BeforePosT ( n);- EndOfLifetimeHole n -> Trace.EndOfLifetimeHoleT ( n)}+ BeforePos n -> Trace.BeforePosT n;+ EndOfLifetimeHole n -> Trace.EndOfLifetimeHoleT n} -splitPosition :: Interval.IntervalDesc -> SplitPosition ->- Prelude0.Coq_oddnum+splitPosition :: Interval.IntervalDesc -> SplitPosition -> Prelude.Int splitPosition d pos = case pos of { BeforePos n -> n;@@ -79,11 +78,13 @@ Prelude.Either ([] Trace.SSTrace) ScanState.ScanStateSig splitUnhandledInterval maxReg sd uid beg us pos e =- (Prelude.flip (Prelude.$)) ((:) Trace.ESplitUnhandledInterval e) (\e2 ->+ (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitUnhandledInterval ( uid)+ (coq_SplitPositionToT pos)) e) (\e2 -> let { _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 -> let {int = Vector0.vnth _nextInterval_ ints uid0} in let {splitPos = splitPosition ( int) pos} in+ let {optSplitPos = Spill.optimalSplitPosition ( int) beg splitPos} in let { _evar_0_ = \_ -> let {@@ -91,36 +92,44 @@ let { _top_assumption_ = Interval.splitInterval (Interval.Build_IntervalDesc iv ib ie rds)- splitPos}+ optSplitPos} in let { _evar_0_ = \i0 i1 -> let { _evar_0_ = let { _evar_0_ = \_ _ ->- (Prelude.flip (Prelude.$)) __ (\_ _ ->+ (Prelude.flip (Prelude.$)) __ (\_ -> let {- _evar_0_ = \_discharged_uid_ _discharged_us_ ->- Logic.coq_False_rect}+ sd' = ScanState.Build_ScanStateDesc+ _nextInterval_ ints _fixedIntervals_ unh+ _active_ _inactive_ _handled_} in let {- _evar_0_0 = \x xs uid1 us1 ->- (Prelude.flip (Prelude.$)) __ (\_ ->- let {- _evar_0_0 = \_ ->- (Prelude.flip (Prelude.$)) __- (let {- _evar_0_0 = let {- _evar_0_0 = (Prelude.flip (Prelude.$))- __ (\_ _ ->- Prelude.Right- (ScanState.packScanState- maxReg- ScanState.InUse- (ScanState.Build_ScanStateDesc- ((Prelude.succ)- _nextInterval_)- (unsafeCoerce+ _evar_0_ = \_ _ ->+ let {+ _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_0 = \_ ->+ (Prelude.flip (Prelude.$)) __+ (let {+ _evar_0_0 = let {+ _evar_0_0 = (Prelude.flip (Prelude.$))+ __+ (\_ _ ->+ Prelude.Right+ (ScanState.packScanState+ maxReg+ ScanState.InUse+ (ScanState.Build_ScanStateDesc+ ((Prelude.succ)+ _nextInterval_)+ (unsafeCoerce (Vector0.vshiftin _nextInterval_ (Vector0.vreplace@@ -128,8 +137,8 @@ ints uid1 ( i0)) ( i1)))- _fixedIntervals_- (List1.insert+ _fixedIntervals_+ (List1.insert (Prelude0.lebf Prelude.snd) ((,)@@ -144,25 +153,42 @@ (Prelude.map Prelude.id us1)))- (Prelude.map+ (Prelude.map Prelude.id _active_)- (Prelude.map+ (Prelude.map Prelude.id _inactive_)- (Prelude.map+ (Prelude.map Prelude.id _handled_))))}- 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+ case unh of {+ [] -> _evar_0_ uid0 us0;+ (:) x x0 -> _evar_0_0 x x0 uid0 us0}} in- case unh of {- [] -> _evar_0_ uid0 us0;- (:) x x0 -> _evar_0_0 x x0 uid0 us0}) __}+ let {+ _evar_0_0 = \_ _ -> Prelude.Left ((:)+ (Trace.ECannotModifyHandledInterval ( uid0))+ e2)}+ in+ case Prelude.not+ (Ssrbool.in_mem (unsafeCoerce uid0)+ (Ssrbool.mem+ (Seq.seq_predType+ (Fintype.ordinal_eqType+ (ScanState.nextInterval maxReg+ sd')))+ (unsafeCoerce+ (ScanState.handledIds maxReg sd')))) of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}) __} in _evar_0_ __} in@@ -220,8 +246,10 @@ Prelude.False -> _evar_0_1 __}} in case (Prelude.&&)- ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int))) splitPos)- ((Prelude.<=) splitPos (Interval.iend ( int))) of {+ ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int)))+ optSplitPos)+ ((Prelude.<=) ((Prelude.succ) optSplitPos)+ (Interval.iend ( int))) of { Prelude.True -> _evar_0_ __; Prelude.False -> _evar_0_0 __}} in@@ -232,17 +260,17 @@ splitCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc -> SplitPosition -> Morph.SState () () () splitCurrentInterval maxReg pre pos e ssi =- (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitCurrentInterval- (coq_SplitPositionToT pos)) e) (\e2 ->+ let {+ _evar_0_ = \desc ->+ let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in let {- _evar_0_ = \desc ->- let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in+ _evar_0_0 = \_top_assumption_ -> let {- _evar_0_0 = \_top_assumption_ ->- let {- _evar_0_0 = \uid beg us ->+ _evar_0_0 = \uid beg us ->+ (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitCurrentInterval + ( uid) (coq_SplitPositionToT pos)) e) (\e2 _ _ _ _ -> let {- _evar_0_0 = \_nextInterval_ intervals0 _fixedIntervals_ unhandled0 _active_ _inactive_ _handled_ uid0 us0 _top_assumption_0 ->+ _evar_0_0 = \_nextInterval_ intervals0 fints 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 -> Prelude.Right ((,) ()@@ -255,18 +283,18 @@ 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 e2)}}- in- (\us _ _ _ _ _ ->- case _top_assumption_ of {- (,) x x0 -> _evar_0_0 x x0 us})}+ (splitUnhandledInterval maxReg desc uid beg us pos e2)})} in- case ScanState.unhandled maxReg desc 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 ssi of {- Morph.Build_SSInfo x x0 -> _evar_0_ x __})+ 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 -> ([]@@ -277,13 +305,16 @@ ([] Trace.SSTrace) ScanState.ScanStateSig splitActiveOrInactiveInterval maxReg sd uid beg us xid pos reg hin e = (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitActiveOrInactiveInterval+ ( xid) (case hin of { Prelude.Left _ -> Prelude.True;- Prelude.Right _ -> Prelude.False})) e) (\e2 ->+ Prelude.Right _ -> Prelude.False}) (coq_SplitPositionToT pos)) e)+ (\e2 -> let { _evar_0_ = \ni ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 xid0 hin0 -> let {int = Vector0.vnth ni ints xid0} in let {splitPos = splitPosition ( int) pos} in+ let {optSplitPos = Spill.optimalSplitPosition ( int) beg splitPos} in let { sd0 = ScanState.Build_ScanStateDesc ni ints _fixedIntervals_ unh _active_ _inactive_ _handled_}@@ -296,33 +327,54 @@ let { _top_assumption_ = Interval.splitInterval (Interval.Build_IntervalDesc iv ib ie rds)- splitPos}+ optSplitPos} in let { _evar_0_ = \i0 i1 -> let { _evar_0_ = let { _evar_0_ = \_ _ ->- (Prelude.flip (Prelude.$)) __ (\_ _ ->+ (Prelude.flip (Prelude.$)) __ (\_ -> let {- sd1 = ScanState.Build_ScanStateDesc ni- (Vector0.vreplace ni ints xid0 ( i0))- _fixedIntervals_ unh _active_ _inactive_- _handled_}- in- (Prelude.flip (Prelude.$)) __ (\_ ->+ _evar_0_ = \_ _ ->+ let {+ sd1 = ScanState.Build_ScanStateDesc ni+ (Vector0.vreplace ni ints xid0 ( i0))+ _fixedIntervals_ unh _active_ _inactive_+ _handled_}+ in (Prelude.flip (Prelude.$)) __ (\_ -> (Prelude.flip (Prelude.$)) __ (\_ ->- let {_evar_0_ = \err -> Prelude.Left err}- in- let {- _evar_0_0 = \_top_assumption_0 ->- Prelude.Right _top_assumption_0}- in- case Spill.spillInterval maxReg sd1 i1- uid0 beg us0 Spill.NewToHandled e2 of {- Prelude.Left x -> _evar_0_ x;- Prelude.Right x -> _evar_0_0 x})))) __}+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ _evar_0_ = \err -> Prelude.Left err}+ in+ let {+ _evar_0_0 = \_top_assumption_0 ->+ Prelude.Right _top_assumption_0}+ in+ case Spill.spillInterval maxReg sd1 i1+ uid0 beg us0 Spill.NewToHandled+ e2 of {+ Prelude.Left x -> _evar_0_ x;+ Prelude.Right x -> _evar_0_0 x})))}+ in+ let {+ _evar_0_0 = \_ _ -> Prelude.Left ((:)+ (Trace.ECannotModifyHandledInterval ( xid0))+ e2)}+ in+ case Prelude.not+ (Ssrbool.in_mem (unsafeCoerce xid0)+ (Ssrbool.mem+ (Seq.seq_predType+ (Fintype.ordinal_eqType+ (ScanState.nextInterval maxReg+ sd0)))+ (unsafeCoerce+ (ScanState.handledIds maxReg sd0)))) of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}) __} in _evar_0_ __} in@@ -376,7 +428,9 @@ in case (Prelude.&&) ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int)))- splitPos) ((Prelude.<=) splitPos (Interval.iend ( int))) of {+ optSplitPos)+ ((Prelude.<=) ((Prelude.succ) optSplitPos)+ (Interval.iend ( int))) of { Prelude.True -> _evar_0_ __; Prelude.False -> _evar_0_0 __})} in@@ -388,47 +442,47 @@ PhysReg -> SplitPosition -> Prelude.Bool -> Morph.SState () () () splitAssignedIntervalForReg maxReg pre reg pos trueForActives e ssi =- (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitAssignedIntervalForReg - ( reg)) e) (\e2 ->+ let {+ _evar_0_ = \desc -> let {- _evar_0_ = \desc ->+ intlist = case trueForActives of {+ Prelude.True -> ScanState.active maxReg desc;+ Prelude.False -> ScanState.inactive maxReg desc}}+ in+ (Prelude.flip (Prelude.$)) __ (\_ -> let {- intlist = case trueForActives of {- Prelude.True -> ScanState.active maxReg desc;- Prelude.False -> ScanState.inactive maxReg desc}}+ intids = Prelude.map (\i -> Prelude.fst i)+ (Prelude.filter (\i ->+ Eqtype.eq_op (Fintype.ordinal_eqType maxReg)+ (Prelude.snd (unsafeCoerce i)) (unsafeCoerce reg))+ intlist)} in (Prelude.flip (Prelude.$)) __ (\_ ->+ let {_evar_0_ = \intlist0 intids0 -> Logic.coq_False_rect} in let {- intids = Prelude.map (\i -> Prelude.fst i)- (Prelude.filter (\i ->- Eqtype.eq_op (Fintype.ordinal_eqType maxReg)- (Prelude.snd (unsafeCoerce i)) (unsafeCoerce reg))- intlist)}- in- (Prelude.flip (Prelude.$)) __ (\_ ->- let {_evar_0_ = \intlist0 intids0 -> 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 ->+ _evar_0_0 = \_nextInterval_ intervals0 fints _unhandled_ active0 inactive0 _handled_ uid0 us0 intlist0 intids0 -> let {- _evar_0_0 = \_nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ uid0 us0 intlist0 intids0 ->- let {- _evar_0_0 = \_ -> Prelude.Right ((,) () (Morph.Build_SSInfo- (ScanState.Build_ScanStateDesc _nextInterval_ intervals0- _fixedIntervals_ _unhandled_ active0 inactive0 _handled_)- __))}- in- let {- _evar_0_1 = \aid aids iHaids ->+ _evar_0_0 = \_ -> Prelude.Right ((,) () (Morph.Build_SSInfo+ (ScanState.Build_ScanStateDesc _nextInterval_ intervals0+ fints _unhandled_ active0 inactive0 _handled_) __))}+ in+ let {+ _evar_0_1 = \aid aids iHaids ->+ (Prelude.flip (Prelude.$)) ((:)+ (Trace.ESplitAssignedIntervalForReg ( aid) ( reg)+ (coq_SplitPositionToT pos)) e) (\e2 -> let { _evar_0_1 = \_ -> let { _top_assumption_0 = \x x0 x1 x2 x3 x4 -> splitActiveOrInactiveInterval maxReg (ScanState.Build_ScanStateDesc _nextInterval_- intervals0 _fixedIntervals_ _unhandled_ active0- inactive0 _handled_) x x0 x1 x2 x3 x4}+ intervals0 fints _unhandled_ active0 inactive0+ _handled_) x x0 x1 x2 x3 x4} in (Prelude.flip (Prelude.$)) (let {@@ -517,54 +571,53 @@ (Trace.ECannotSplitSingleton ( aid)) e2)} in case (Prelude.<=) beg- (- (splitPosition- (- (Vector0.vnth- (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 {+ (splitPosition+ (+ (Vector0.vnth+ (ScanState.nextInterval maxReg+ (ScanState.Build_ScanStateDesc+ _nextInterval_ intervals0 fints _unhandled_+ active0 inactive0 _handled_))+ (ScanState.intervals maxReg+ (ScanState.Build_ScanStateDesc+ _nextInterval_ intervals0 fints _unhandled_+ active0 inactive0 _handled_)) aid)) pos) of { Prelude.True -> _evar_0_1 __;- Prelude.False -> _evar_0_2 __}}- in- Datatypes.list_rect _evar_0_0 (\aid aids iHaids _ ->- _evar_0_1 aid aids iHaids) intids0 __}+ Prelude.False -> _evar_0_2 __})} in- (\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})}+ Datatypes.list_rect _evar_0_0 (\aid aids iHaids _ ->+ _evar_0_1 aid aids iHaids) intids0 __} in- (\us _ ->- case _top_assumption_ of {- (,) x x0 -> _evar_0_0 x x0 us})}+ (\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- 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 __})+ (\us _ ->+ case _top_assumption_ of {+ (,) x x0 -> _evar_0_0 x x0 us})}+ in+ 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 __} splitActiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->- PhysReg -> Prelude0.Coq_oddnum -> Morph.SState- () () ()+ PhysReg -> Prelude.Int -> Morph.SState () + () () splitActiveIntervalForReg maxReg pre reg pos =- Context.context (Trace.ESplitActiveIntervalForReg ( reg))+ Context.context (Trace.ESplitActiveIntervalForReg ( reg)+ (coq_SplitPositionToT (BeforePos pos))) (splitAssignedIntervalForReg maxReg pre reg (BeforePos pos) Prelude.True) splitAnyInactiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->- PhysReg -> Prelude0.Coq_oddnum ->- Morph.SState () () ()+ PhysReg -> Prelude.Int -> Morph.SState + () () () splitAnyInactiveIntervalForReg maxReg pre reg pos e ss = (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitAnyInactiveIntervalForReg- ( reg)) e) (\e2 ->+ ( reg) (coq_SplitPositionToT (EndOfLifetimeHole pos))) e) (\e2 -> (Prelude.flip (Prelude.$)) (\s -> splitAssignedIntervalForReg maxReg s reg (EndOfLifetimeHole pos) Prelude.False) (\_top_assumption_ ->
LinearScan/Ssr.hs view
@@ -3,7 +3,7 @@ module LinearScan.Ssr where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Ssrbool.hs view
@@ -4,7 +4,7 @@ module LinearScan.Ssrbool where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Ssreflect.hs view
@@ -3,7 +3,7 @@ module LinearScan.Ssreflect where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Ssrfun.hs view
@@ -3,7 +3,7 @@ module LinearScan.Ssrfun where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Ssrnat.hs view
@@ -4,7 +4,7 @@ module LinearScan.Ssrnat where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/State.hs view
@@ -4,7 +4,7 @@ module LinearScan.State where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -49,6 +49,10 @@ __ = Prelude.error "Logical or arity value used" type State s a = s -> (,) a s++get :: State a1 a1+get i =+ (,) i i modify :: (a1 -> a1) -> State a1 () modify f i =
LinearScan/State0.hs view
@@ -4,7 +4,7 @@ module LinearScan.State0 where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/String0.hs view
@@ -3,7 +3,7 @@ module LinearScan.String0 where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Trace.hs view
@@ -3,7 +3,7 @@ module LinearScan.Trace where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -30,29 +30,34 @@ type TrueIfActiveT = Prelude.Bool data SSTrace =- EIntersectsWithFixedInterval Prelude.Int PhysRegT- | ESplitAssignedIntervalForReg PhysRegT- | ESplitActiveOrInactiveInterval TrueIfActiveT- | EIntervalHasUsePosReqReg IntervalIdT+ EOverlapsWithFixedInterval Prelude.Int PhysRegT+ | ESplitAssignedIntervalForReg IntervalIdT PhysRegT SplitPositionT+ | ESplitActiveOrInactiveInterval IntervalIdT TrueIfActiveT SplitPositionT+ | EIntervalHasUsePosReqReg Prelude.Int | EIntervalBeginsAtSplitPosition- | EMoveUnhandledToActive PhysRegT- | ESplitActiveIntervalForReg PhysRegT- | ESplitAnyInactiveIntervalForReg PhysRegT+ | EMoveUnhandledToActive IntervalIdT PhysRegT+ | ESplitActiveIntervalForReg PhysRegT SplitPositionT+ | ESplitAnyInactiveIntervalForReg PhysRegT SplitPositionT | ESpillInterval SpillConditionT | ESpillCurrentInterval- | ESplitUnhandledInterval- | ESplitCurrentInterval SplitPositionT+ | ESplitUnhandledInterval IntervalIdT SplitPositionT+ | ESplitCurrentInterval IntervalIdT SplitPositionT | ETryAllocateFreeReg PhysRegT (Prelude.Maybe Prelude.Int) IntervalIdT | EAllocateBlockedReg PhysRegT (Prelude.Maybe Prelude.Int) IntervalIdT | ERemoveUnhandledInterval IntervalIdT- | ECannotInsertUnhandled+ | ECannotInsertUnhandled Prelude.Int Prelude.Int Prelude.Int Prelude.Int | EIntervalBeginsBeforeUnhandled IntervalIdT | ENoValidSplitPosition IntervalIdT | ECannotSplitSingleton IntervalIdT | ERegisterAlreadyAssigned PhysRegT- | ERegisterAssignmentsOverlap PhysRegT+ | ERegisterAssignmentsOverlap PhysRegT IntervalIdT Prelude.Int+ | ECannotModifyHandledInterval IntervalIdT | EUnexpectedNoMoreUnhandled- | ECannotSpillIfRegisterRequired PhysRegT+ | ECannotSpillIfRegisterRequired IntervalIdT+ | ECannotSpillIfRegisterRequiredBefore IntervalIdT Prelude.Int | EFuelExhausted+ | EUnhandledIntervalsRemain+ | EActiveIntervalsRemain+ | EInactiveIntervalsRemain | ENotYetImplemented Prelude.Int
LinearScan/Tuple.hs view
@@ -3,7 +3,7 @@ module LinearScan.Tuple where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/UsePos.hs view
@@ -4,7 +4,7 @@ module LinearScan.UsePos where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -50,10 +50,7 @@ case y of { Input -> Prelude.False; _ -> Prelude.True};- Output ->- case y of {- Output -> Prelude.True;- _ -> Prelude.False}}+ Output -> Prelude.False} eqVarKind :: VarKind -> VarKind -> Prelude.Bool eqVarKind s1 s2 =@@ -72,35 +69,38 @@ _ -> Prelude.False}} eqVarKindP :: Eqtype.Equality__Coq_axiom VarKind-eqVarKindP b1 b2 =+eqVarKindP _top_assumption_ = 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}}+ _evar_0_ = \_top_assumption_0 ->+ let {_evar_0_ = Ssrbool.ReflectT} in+ let {_evar_0_0 = Ssrbool.ReflectF} in+ let {_evar_0_1 = Ssrbool.ReflectF} in+ case _top_assumption_0 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}}+ _evar_0_0 = \_top_assumption_0 ->+ let {_evar_0_0 = Ssrbool.ReflectF} in+ let {_evar_0_1 = Ssrbool.ReflectT} in+ let {_evar_0_2 = Ssrbool.ReflectF} in+ case _top_assumption_0 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}}+ _evar_0_1 = \_top_assumption_0 ->+ let {_evar_0_1 = Ssrbool.ReflectF} in+ let {_evar_0_2 = Ssrbool.ReflectF} in+ let {_evar_0_3 = Ssrbool.ReflectT} in+ case _top_assumption_0 of {+ Input -> _evar_0_1;+ Temp -> _evar_0_2;+ Output -> _evar_0_3}} in- case b1 of {+ case _top_assumption_ of { Input -> _evar_0_; Temp -> _evar_0_0; Output -> _evar_0_1}
LinearScan/Vector0.hs view
@@ -4,7 +4,7 @@ module LinearScan.Vector0 where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet
LinearScan/Verify.hs view
@@ -4,7 +4,7 @@ module LinearScan.Verify where -import Debug.Trace (trace, traceShow)+import Debug.Trace (trace, traceShow, traceShowId) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet@@ -23,6 +23,7 @@ import qualified LinearScan.Lens as Lens import qualified LinearScan.List1 as List1 import qualified LinearScan.Loops as Loops+import qualified LinearScan.Maybe as Maybe import qualified LinearScan.Monad as Monad import qualified LinearScan.Prelude0 as Prelude0 import qualified LinearScan.Resolve as Resolve@@ -60,6 +61,7 @@ data UseVerifier = VerifyDisabled | VerifyEnabled+ | VerifyEnabledStrict type RegAllocations = Vector0.Vec ((,) (Prelude.Maybe Blocks.VarId) (Prelude.Maybe Blocks.VarId))@@ -77,6 +79,16 @@ case r of { Build_RegStateDesc rsAllocs0 rsStack0 -> rsStack0} +data RegStateDescSet =+ Build_RegStateDescSet ([]+ ((,) (Prelude.Maybe Blocks.VarId)+ (Prelude.Maybe Blocks.VarId))) IntSet.IntSet++fromRegStateDesc :: Prelude.Int -> RegStateDesc -> RegStateDescSet+fromRegStateDesc maxReg x =+ Build_RegStateDescSet (Vector0.vec_to_seq maxReg (rsAllocs maxReg x))+ (rsStack maxReg x)+ residency :: (Functor.Functor a1) -> ((Prelude.Maybe Blocks.VarId) -> a1) -> ((,) (Prelude.Maybe Blocks.VarId) (Prelude.Maybe Blocks.VarId)) -> a1@@ -98,14 +110,15 @@ data AllocError = VarNotAllocated Blocks.VarId | VarNotResident Blocks.VarId- | VarNotResidentForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId)- | VarNotReservedForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId)- | PhysRegAlreadyResidentForVar Prelude.Int Blocks.VarId+ | VarNotResidentForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId) + Prelude.Int+ | VarNotReservedForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId) + Prelude.Int | PhysRegAlreadyReservedForVar Prelude.Int Blocks.VarId | RegAlreadyReservedToVar Prelude.Int Blocks.VarId Blocks.VarId | BlockWithoutPredecessors Blocks.BlockId | UnknownPredecessorBlock Blocks.BlockId Blocks.BlockId- | ErrorAtBlockEnd Blocks.BlockId+ | LoopInResolvingMoves Resolve.ResolvingMoveSet type RegStateSig = RegStateDesc @@ -117,7 +130,7 @@ Build_VerifiedSig RegStateDesc (IntMap.IntMap RegStateSig) (IntMap.IntMap ([] Resolve.ResolvingMoveSet)) - (IntMap.IntMap ([] AllocError)) a+ (IntMap.IntMap ((,) RegStateDescSet ([] AllocError))) a verDesc :: Prelude.Int -> (VerifiedSig a1) -> RegStateDesc verDesc maxReg v =@@ -138,7 +151,8 @@ Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 -> verMoves0} -verErrors :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap ([] AllocError)+verErrors :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap+ ((,) RegStateDescSet ([] AllocError)) verErrors maxReg v = case v of { Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->@@ -183,7 +197,8 @@ (f (verMoves maxReg s)) _verErrors :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap- ([] AllocError)) -> a2) -> (VerifiedSig a1) -> a2+ ((,) RegStateDescSet ([] AllocError))) -> a2) -> (VerifiedSig+ a1) -> a2 _verErrors maxReg h f s = Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s) (verBlocks maxReg s) (verMoves maxReg s) x (verExt maxReg s))@@ -201,8 +216,15 @@ errorsT :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> ([] AllocError) -> Verified a1 a2 () errorsT maxReg mDict pc errs =- Lens.applyStateT (\_ -> _verErrors maxReg)- (IntMap.coq_IntMap_insert pc errs) mDict+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ Lens.applyStateT (\_ -> _verErrors maxReg) (\m ->+ Prelude0.flip (IntMap.coq_IntMap_insert pc) m+ (case IntMap.coq_IntMap_lookup pc m of {+ Prelude.Just p ->+ case p of {+ (,) d prevErrs -> (,) d ((Prelude.++) prevErrs errs)};+ Prelude.Nothing -> (,) (fromRegStateDesc maxReg st) errs})) mDict)+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) errorT :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> AllocError -> Verified a1 a2 ()@@ -250,31 +272,40 @@ (addMove maxReg mDict pc (Resolve.RSAllocReg var ( reg))) isReserved :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Blocks.VarId ->- Verified a1 a2 Prelude.Bool+ Verified a1 a2 (Prelude.Maybe Blocks.VarId) isReserved maxReg mDict reg var = Monad.bind (State0.coq_StateT_Monad mDict) (\st -> Applicative.pure (State0.coq_StateT_Applicative mDict)- (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)- (Lens.view (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg))- (unsafeCoerce (Prelude.Just var))))+ (Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) -checkReservation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg- -> Blocks.VarId -> Verified a1 a2 ()-checkReservation maxReg mDict pc reg var =- Monad.bind (State0.coq_StateT_Monad mDict) (\b ->- Monad.unless (State0.coq_StateT_Monad mDict) b- (Monad.bind (State0.coq_StateT_Monad mDict) (\st ->- errorT maxReg mDict pc (VarNotReservedForReg var ( reg)- (Lens.view (Lens.stepdownl' (\_ -> reservation))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg))))- (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)))- (isReserved maxReg mDict reg var)+checkReservation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->+ UseVerifier -> PhysReg -> Blocks.VarId -> Verified + a1 a2 ()+checkReservation maxReg mDict pc useVerifier reg var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ let {+ err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)+ (Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))+ ((Prelude.succ) 0))}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\res ->+ case res of {+ Prelude.Just var' ->+ Monad.unless (State0.coq_StateT_Monad mDict)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce var) var') err;+ Prelude.Nothing ->+ case useVerifier of {+ VerifyEnabledStrict -> err;+ _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})+ (isReserved maxReg mDict reg var))+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) -releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->- Blocks.VarId -> Verified a1 a2 ()-releaseReg maxReg mDict pc reg var =+releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier+ -> PhysReg -> Blocks.VarId -> Verified a1 a2 ()+releaseReg maxReg mDict pc useVerifier reg var = Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\st -> case Ssr.prop@@ -290,15 +321,26 @@ (Lens.set (\_ -> reservation) Prelude.Nothing)) (rsStack maxReg st))) mDict; Prelude.Nothing ->- errorT maxReg mDict pc (VarNotReservedForReg var ( reg)- (Lens.view (Lens.stepdownl' (\_ -> reservation))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg)))})+ let {+ err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)+ (Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))+ ((Prelude.succ) ((Prelude.succ) 0)))}+ in+ case useVerifier of {+ VerifyEnabledStrict -> err;+ _ ->+ case Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {+ Prelude.Just v -> err;+ Prelude.Nothing ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)) (addMove maxReg mDict pc (Resolve.RSFreeReg ( reg) var)) -assignReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->- Blocks.VarId -> Verified a1 a2 ()-assignReg maxReg mDict pc reg var =+assignReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier ->+ PhysReg -> Blocks.VarId -> Verified a1 a2 ()+assignReg maxReg mDict pc useVerifier reg var = Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\st -> case Ssr.prop@@ -314,50 +356,120 @@ (Lens.set (\_ -> residency) (Prelude.Just var))) (rsStack maxReg st))) mDict; Prelude.Nothing ->- errorT maxReg mDict pc (VarNotReservedForReg ( reg) var- (Lens.view (Lens.stepdownl' (\_ -> reservation))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg)))})+ let {+ err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)+ (Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))}+ in+ case useVerifier of {+ VerifyEnabledStrict -> err;+ _ ->+ case Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {+ Prelude.Just v -> err;+ Prelude.Nothing ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)) (addMove maxReg mDict pc (Resolve.RSAssignReg var ( reg))) isResident :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Blocks.VarId ->- Verified a1 a2 Prelude.Bool+ Verified a1 a2 (Prelude.Maybe Blocks.VarId) isResident maxReg mDict reg var = Monad.bind (State0.coq_StateT_Monad mDict) (\st -> Applicative.pure (State0.coq_StateT_Applicative mDict)- (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)- (Lens.view (Lens.stepdownl' (unsafeCoerce (\_ -> residency)))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg))- (unsafeCoerce (Prelude.Just var))))+ (Lens.view (Lens.stepdownl' (\_ -> residency))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) -checkResidency :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg- -> Blocks.VarId -> Verified a1 a2 ()-checkResidency maxReg mDict pc reg var =- Monad.bind (State0.coq_StateT_Monad mDict) (\b ->- Monad.unless (State0.coq_StateT_Monad mDict) b- (Monad.bind (State0.coq_StateT_Monad mDict) (\st ->- errorT maxReg mDict pc (VarNotResidentForReg var ( reg)- (Lens.view (Lens.stepdownl' (\_ -> residency))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg))))- (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)))- (isResident maxReg mDict reg var)--checkLiveness :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->- IntSet.IntSet -> Verified a1 a2 ()-checkLiveness maxReg mDict pc vars =+checkResidency :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->+ UseVerifier -> PhysReg -> Blocks.VarId -> Verified + a1 a2 ()+checkResidency maxReg mDict pc useVerifier reg var = Monad.bind (State0.coq_StateT_Monad mDict) (\st ->- Monad.forM_ (State0.coq_StateT_Monad mDict)- (IntSet.coq_IntSet_toList vars) (\var ->- Monad.unless (State0.coq_StateT_Monad mDict)- (Vector0.vfoldl_with_index maxReg (\reg b p ->- (Prelude.||) b- (case Lens.view (Lens.stepdownl' (\_ -> residency)) p of {- Prelude.Just var0 -> Prelude.True;- Prelude.Nothing -> Prelude.False})) Prelude.False- (rsAllocs maxReg st)) (errorT maxReg mDict pc (VarNotResident var))))+ Monad.bind (State0.coq_StateT_Monad mDict) (\res ->+ let {+ err = errorT maxReg mDict pc (VarNotResidentForReg var ( reg) res+ ((Prelude.succ) 0))}+ in+ case res of {+ Prelude.Just var' ->+ Monad.unless (State0.coq_StateT_Monad mDict)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce var)+ (unsafeCoerce var')) err;+ Prelude.Nothing ->+ case useVerifier of {+ VerifyEnabledStrict -> err;+ _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})+ (isResident maxReg mDict reg var)) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) +clearReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier ->+ PhysReg -> Blocks.VarId -> Verified a1 a2 ()+clearReg maxReg mDict pc useVerifier reg var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case Ssr.prop+ (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)+ (Lens.view (Lens.stepdownl' (unsafeCoerce (\_ -> residency)))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))+ (unsafeCoerce (Prelude.Just var))) of {+ Prelude.Just _ ->+ Lens.modifyStateT (\_ -> _verState maxReg)+ (packRegState maxReg (Build_RegStateDesc+ (Vector0.vmodify maxReg (rsAllocs maxReg st) reg+ (Lens.set (\_ -> residency) Prelude.Nothing))+ (rsStack maxReg st))) mDict;+ Prelude.Nothing ->+ let {+ err = errorT maxReg mDict pc (VarNotResidentForReg var ( reg)+ (Lens.view (Lens.stepdownl' (\_ -> residency))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))+ ((Prelude.succ) ((Prelude.succ) 0)))}+ in+ case useVerifier of {+ VerifyEnabledStrict -> err;+ _ ->+ case Lens.view (Lens.stepdownl' (\_ -> residency))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {+ Prelude.Just v -> err;+ Prelude.Nothing ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))+ (addMove maxReg mDict pc (Resolve.RSClearReg ( reg) var))++checkLiveness :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->+ UseVerifier -> IntSet.IntSet -> Prelude.Bool -> Verified + a1 a2 ()+checkLiveness maxReg mDict pc useVerifier vars clearOut =+ case useVerifier of {+ VerifyEnabledStrict ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.when (State0.coq_StateT_Monad mDict) clearOut+ (Vector0.vfoldl_with_index maxReg (\reg act p ->+ case Lens.view (Lens.stepdownl' (\_ -> residency)) p of {+ Prelude.Just v ->+ Monad.unless (State0.coq_StateT_Monad mDict)+ (IntSet.coq_IntSet_member v vars)+ (clearReg maxReg mDict pc useVerifier reg v);+ Prelude.Nothing ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ()})+ (Applicative.pure (State0.coq_StateT_Applicative mDict) ())+ (rsAllocs maxReg st)))+ (Monad.forM_ (State0.coq_StateT_Monad mDict)+ (IntSet.coq_IntSet_toList vars) (\var ->+ Monad.unless (State0.coq_StateT_Monad mDict)+ (Vector0.vfoldl_with_index maxReg (\reg b p ->+ (Prelude.||) b+ (case Lens.view (Lens.stepdownl' (\_ -> residency)) p of {+ Prelude.Just var0 -> Prelude.True;+ Prelude.Nothing -> Prelude.False})) Prelude.False+ (rsAllocs maxReg st))+ (errorT maxReg mDict pc (VarNotResident var)))))+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict);+ _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}+ verifyBlockBegin :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier -> Prelude.Int -> IntSet.IntSet -> Loops.LoopState -> Verified a1 a2 ()@@ -367,7 +479,7 @@ Applicative.pure (State0.coq_StateT_Applicative mDict) (); VerifyEnabled -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- checkLiveness maxReg mDict pc liveIns)+ checkLiveness maxReg mDict pc useVerifier liveIns Prelude.True) (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of { Prelude.Just fwds -> Monad.forM_ (State0.coq_StateT_Monad mDict)@@ -380,9 +492,35 @@ errorT maxReg mDict pc (UnknownPredecessorBlock bid pred)}) (Lens.use (Lens.stepdownl' (\_ -> _verBlocks maxReg)) mDict)); Prelude.Nothing ->- Monad.when (State0.coq_StateT_Monad mDict)- ((Prelude.<=) ((Prelude.succ) 0) (IntSet.coq_IntSet_size liveIns))- (errorT maxReg mDict pc (BlockWithoutPredecessors bid))})}+ case useVerifier of {+ VerifyEnabledStrict ->+ Monad.when (State0.coq_StateT_Monad mDict)+ ((Prelude.<=) ((Prelude.succ) 0)+ (IntSet.coq_IntSet_size liveIns))+ (errorT maxReg mDict pc (BlockWithoutPredecessors bid));+ _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}});+ VerifyEnabledStrict ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkLiveness maxReg mDict pc useVerifier liveIns Prelude.True)+ (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of {+ Prelude.Just fwds ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ (IntSet.coq_IntSet_toList fwds) (\pred ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\exits ->+ case IntMap.coq_IntMap_lookup pred exits of {+ Prelude.Just allocs ->+ Lens.modifyStateT (\_ -> _verState maxReg) allocs mDict;+ Prelude.Nothing ->+ errorT maxReg mDict pc (UnknownPredecessorBlock bid pred)})+ (Lens.use (Lens.stepdownl' (\_ -> _verBlocks maxReg)) mDict));+ Prelude.Nothing ->+ case useVerifier of {+ VerifyEnabledStrict ->+ Monad.when (State0.coq_StateT_Monad mDict)+ ((Prelude.<=) ((Prelude.succ) 0)+ (IntSet.coq_IntSet_size liveIns))+ (errorT maxReg mDict pc (BlockWithoutPredecessors bid));+ _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})} verifyBlockEnd :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier -> Prelude.Int -> IntSet.IntSet -> Verified @@ -391,7 +529,7 @@ case useVerifier of { VerifyDisabled -> Applicative.pure (State0.coq_StateT_Applicative mDict) ();- VerifyEnabled ->+ _ -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\allocs -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->@@ -400,7 +538,7 @@ (Lens.modifyStateT (\_ -> _verState maxReg) (packRegState maxReg (newRegStateDesc maxReg)) mDict)) (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict))- (checkLiveness maxReg mDict pc liveOuts)}+ (checkLiveness maxReg mDict pc useVerifier liveOuts Prelude.False)} verifyApplyAllocs :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 a1 a2) -> Blocks.OpId -> UseVerifier -> a1 -> ([]@@ -421,40 +559,37 @@ (Blocks.opRefs maxReg mDict oinfo op)) (\ref -> case Blocks.varId maxReg ref of { Prelude.Left reg ->- Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ Prelude.Right var ->+ case List1.maybeLookup Ssrnat.nat_eqType (unsafeCoerce allocs)+ (unsafeCoerce var) of {+ Prelude.Just reg -> case Blocks.varKind maxReg ref of { UsePos.Input ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ checkResidency maxReg mDict pc useVerifier reg var; UsePos.Temp ->- case Vector0.vnth maxReg (rsAllocs maxReg st) reg of {- (,) o o0 ->- case o0 of {- Prelude.Just v ->- errorT maxReg mDict pc (PhysRegAlreadyReservedForVar- ( reg) v);- Prelude.Nothing ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ()}};- UsePos.Output ->- case Vector0.vnth maxReg (rsAllocs maxReg st) reg of {- (,) o o0 ->- case o0 of {- Prelude.Just v ->- errorT maxReg mDict pc (PhysRegAlreadyReservedForVar- ( reg) v);- Prelude.Nothing ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})- (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict);+ checkReservation maxReg mDict pc useVerifier reg var;+ UsePos.Output -> assignReg maxReg mDict pc useVerifier reg var};+ Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}});+ VerifyEnabledStrict ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ (List1.sortBy (\x y ->+ UsePos.coq_VarKind_leq (Blocks.varKind maxReg x)+ (Blocks.varKind maxReg y))+ (Blocks.opRefs maxReg mDict oinfo op)) (\ref ->+ case Blocks.varId maxReg ref of {+ Prelude.Left reg ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) (); Prelude.Right var -> case List1.maybeLookup Ssrnat.nat_eqType (unsafeCoerce allocs) (unsafeCoerce var) of { Prelude.Just reg -> case Blocks.varKind maxReg ref of {- UsePos.Input -> checkResidency maxReg mDict pc reg var;- UsePos.Temp -> checkReservation maxReg mDict pc reg var;- UsePos.Output ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- assignReg maxReg mDict pc reg var)- (checkReservation maxReg mDict pc reg var)};+ UsePos.Input ->+ checkResidency maxReg mDict pc useVerifier reg var;+ UsePos.Temp ->+ checkReservation maxReg mDict pc useVerifier reg var;+ UsePos.Output -> assignReg maxReg mDict pc useVerifier reg var}; Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}})}) verifyResolutions :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->@@ -465,102 +600,98 @@ VerifyDisabled -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Prelude.map (Resolve.resMove maxReg) moves);- VerifyEnabled ->- Functor.fmap- (State0.coq_StateT_Functor- (Applicative.is_functor (Monad.is_applicative mDict))) Seq.rev- (Monad.forFoldM (State0.coq_StateT_Monad mDict) [] moves (\acc mv ->- Monad.bind (State0.coq_StateT_Monad mDict) (\st ->- case Resolve.resMove maxReg mv of {- Resolve.Move fromReg fromVar toReg ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x3 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x4 ->- Applicative.pure- (State0.coq_StateT_Applicative mDict) ((:)- (Resolve.resMove maxReg mv) acc))- (Monad.when (State0.coq_StateT_Monad mDict)- (Resolve.resGhost maxReg mv)- (releaseReg maxReg mDict pc toReg fromVar)))- (assignReg maxReg mDict pc toReg fromVar))- (addMove maxReg mDict pc- (Resolve.weakenResolvingMove maxReg- (Resolve.resMove maxReg mv))))- (reserveReg maxReg mDict pc toReg fromVar))- (Monad.unless (State0.coq_StateT_Monad mDict)- (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)- (unsafeCoerce fromReg) (unsafeCoerce toReg))- (releaseReg maxReg mDict pc fromReg fromVar)))- (checkResidency maxReg mDict pc fromReg fromVar);- Resolve.Swap fromReg fromVar toReg toVar ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x3 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x4 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x5 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x6 ->- Monad.bind (State0.coq_StateT_Monad mDict)- (\x7 ->- Applicative.pure- (State0.coq_StateT_Applicative mDict) ((:)- (Resolve.resMove maxReg mv) acc))- (assignReg maxReg mDict pc toReg fromVar))- (assignReg maxReg mDict pc fromReg toVar))- (reserveReg maxReg mDict pc toReg fromVar))- (reserveReg maxReg mDict pc fromReg toVar))- (addMove maxReg mDict pc- (Resolve.weakenResolvingMove maxReg- (Resolve.resMove maxReg mv))))- (releaseReg maxReg mDict pc toReg toVar))- (releaseReg maxReg mDict pc fromReg fromVar))- (checkResidency maxReg mDict pc toReg toVar))- (checkResidency maxReg mDict pc fromReg fromVar);- Resolve.Spill fromReg toSpillSlot ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- Monad.bind (State0.coq_StateT_Monad mDict) (\check ->- case check of {- Prelude.True ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->- Applicative.pure (State0.coq_StateT_Applicative mDict)- ((:) (Resolve.resMove maxReg mv) acc))- (addMove maxReg mDict pc- (Resolve.weakenResolvingMove maxReg- (Resolve.resMove maxReg mv)));- Prelude.False ->- Applicative.pure (State0.coq_StateT_Applicative mDict) acc})- (isResident maxReg mDict fromReg toSpillSlot))- (releaseReg maxReg mDict pc fromReg toSpillSlot);- Resolve.Restore fromSpillSlot toReg ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->- Applicative.pure (State0.coq_StateT_Applicative mDict)- ((:) (Resolve.resMove maxReg mv) acc))- (Monad.when (State0.coq_StateT_Monad mDict)- (Resolve.resGhost maxReg mv)- (releaseReg maxReg mDict pc toReg fromSpillSlot)))- (assignReg maxReg mDict pc toReg fromSpillSlot))- (addMove maxReg mDict pc- (Resolve.weakenResolvingMove maxReg- (Resolve.resMove maxReg mv))))- (reserveReg maxReg mDict pc toReg fromSpillSlot);- Resolve.AllocReg toVar toReg ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ _ ->+ Monad.forFoldM (State0.coq_StateT_Monad mDict) [] moves (\acc mv ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case Resolve.resMove maxReg mv of {+ Resolve.Move fromReg fromVar toReg ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x3 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x4 ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Seq.rcons acc (Resolve.resMove maxReg mv)))+ (Monad.when (State0.coq_StateT_Monad mDict)+ (Resolve.resGhost maxReg mv)+ (releaseReg maxReg mDict pc useVerifier toReg+ fromVar)))+ (assignReg maxReg mDict pc useVerifier toReg fromVar))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg+ (Resolve.resMove maxReg mv))))+ (reserveReg maxReg mDict pc toReg fromVar))+ (Monad.unless (State0.coq_StateT_Monad mDict)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)+ (unsafeCoerce fromReg) (unsafeCoerce toReg))+ (releaseReg maxReg mDict pc useVerifier fromReg fromVar)))+ (checkResidency maxReg mDict pc useVerifier fromReg fromVar);+ Resolve.Transfer fromReg fromVar toReg ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc) (Monad.when (State0.coq_StateT_Monad mDict) (Resolve.resGhost maxReg mv)- (releaseReg maxReg mDict pc toReg toVar)))- (reserveReg maxReg mDict pc toReg toVar);- Resolve.FreeReg fromReg fromVar ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ (releaseReg maxReg mDict pc useVerifier toReg fromVar)))+ (reserveReg maxReg mDict pc toReg fromVar))+ (Monad.unless (State0.coq_StateT_Monad mDict)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)+ (unsafeCoerce fromReg) (unsafeCoerce toReg))+ (releaseReg maxReg mDict pc useVerifier fromReg fromVar));+ Resolve.Spill fromReg toSpillSlot ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\check ->+ case Maybe.isJust check of {+ Prelude.True ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Seq.rcons acc (Resolve.resMove maxReg mv)))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg+ (Resolve.resMove maxReg mv)));+ Prelude.False ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) acc})+ (isResident maxReg mDict fromReg toSpillSlot))+ (releaseReg maxReg mDict pc useVerifier fromReg toSpillSlot);+ Resolve.Restore fromSpillSlot toReg ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Seq.rcons acc (Resolve.resMove maxReg mv)))+ (Monad.when (State0.coq_StateT_Monad mDict)+ (Resolve.resGhost maxReg mv)+ (releaseReg maxReg mDict pc useVerifier toReg+ fromSpillSlot)))+ (assignReg maxReg mDict pc useVerifier toReg fromSpillSlot))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg+ (Resolve.resMove maxReg mv))))+ (reserveReg maxReg mDict pc toReg fromSpillSlot);+ Resolve.AllocReg toVar toReg ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc)- (releaseReg maxReg mDict pc fromReg fromVar)})- (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)))}+ (Monad.when (State0.coq_StateT_Monad mDict)+ (Resolve.resGhost maxReg mv)+ (releaseReg maxReg mDict pc useVerifier toReg toVar)))+ (reserveReg maxReg mDict pc toReg toVar);+ Resolve.FreeReg fromReg fromVar ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) acc)+ (releaseReg maxReg mDict pc useVerifier fromReg fromVar);+ Resolve.Looped x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Seq.rcons acc (Resolve.resMove maxReg mv)))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg+ (Resolve.resMove maxReg mv))))+ (errorT maxReg mDict pc (LoopInResolvingMoves+ (Resolve.weakenResolvingMove maxReg x)))})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))}
linearscan.cabal view
@@ -1,5 +1,5 @@ name: linearscan-version: 0.7.0+version: 0.8.0 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3