diff --git a/LinearScan.hs b/LinearScan.hs --- a/LinearScan.hs +++ b/LinearScan.hs @@ -324,7 +324,8 @@ data Details m blk1 blk2 op1 op2 = Details { reason :: Maybe (LS.SSError, LS.FinalStage) , liveSets :: [(Int, LS.BlockLiveSets)] - , inputBlocks :: [blk1] + , _inputBlocks :: [blk1] + , orderedBlocks :: [blk1] , allocatedBlocks :: [blk2] , scanStatePre :: Maybe ScanStateDesc , scanStatePost :: Maybe ScanStateDesc @@ -335,8 +336,8 @@ showDetails :: Monad m => Details m blk1 blk2 op1 op2 -> m String showDetails err = do - pre <- showScanStateDesc (scanStatePre err) - post <- showScanStateDesc (scanStatePost err) + pre <- showPreScanStateDesc (scanStatePre err) + post <- showPostScanStateDesc (scanStatePost err) return $ "Reason: " ++ show (reason err) ++ "\n\n" ++ ">>> ScanState before allocation:\n" ++ pre ++ "\n" @@ -344,13 +345,21 @@ ++ post ++ "\n" ++ ">>> " ++ show (loopState err) ++ "\n" where - showScanStateDesc Nothing = return "" - showScanStateDesc (Just sd) = + showPreScanStateDesc Nothing = return "" + showPreScanStateDesc (Just sd) = liftM2 (++) (showBlocks1 (blockInfo err) (opInfo err) sd - (liveSets err) (inputBlocks err)) + (liveSets err) (orderedBlocks err)) (return ("\n" ++ show sd)) + -- jww (2015-05-23): Show allocatedBlocks here? + showPostScanStateDesc Nothing = return "" + showPostScanStateDesc (Just sd) = + liftM2 (++) + (showBlocks1 (blockInfo err) (opInfo err) sd + (liveSets err) (orderedBlocks err)) + (return ("\n" ++ show sd)) + deriving instance Show LS.SSError deriving instance Show LS.FinalStage deriving instance Show LS.BlockLiveSets @@ -359,9 +368,9 @@ -> LinearScan.BlockInfo m blk1 blk2 op1 op2 -> LinearScan.OpInfo m op1 op2 -> Details m blk1 blk2 op1 op2 -toDetails (LS.Build_Details a b c d e f g) binfo oinfo = - Details a b c d (fmap toScanStateDesc e) (fmap toScanStateDesc f) - binfo oinfo (toLoopState g) +toDetails (LS.Build_Details a b c d e f g h) binfo oinfo = + Details a b c d e (fmap toScanStateDesc f) (fmap toScanStateDesc g) + binfo oinfo (toLoopState h) -- | Transform a list of basic blocks containing variable references, into an -- equivalent list where each reference is associated with a register diff --git a/LinearScan/Build.hs b/LinearScan/Build.hs --- a/LinearScan/Build.hs +++ b/LinearScan/Build.hs @@ -383,12 +383,21 @@ refs' = case Blocks.opKind maxReg mDict oinfo op of { Blocks.IsCall -> (Prelude.++) - (Fintype.image_mem (Fintype.ordinal_finType maxReg) (\n -> - Blocks.Build_VarInfo (Prelude.Left (unsafeCoerce n)) - UsePos.Temp Prelude.True) - (Ssrbool.mem - (Seq.seq_predType (Fintype.ordinal_eqType maxReg)) - (unsafeCoerce (Fintype.ord_enum maxReg)))) refs; + (Prelude.filter (\x -> + Prelude.not + (Ssrbool.in_mem (unsafeCoerce (Blocks.varId maxReg x)) + (Ssrbool.mem + (Seq.seq_predType + (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) + Ssrnat.nat_eqType)) + (unsafeCoerce + (Prelude.map (Blocks.varId maxReg) refs))))) + (Fintype.image_mem (Fintype.ordinal_finType maxReg) (\n -> + Blocks.Build_VarInfo (Prelude.Left (unsafeCoerce n)) + UsePos.Temp Prelude.True) + (Ssrbool.mem + (Seq.seq_predType (Fintype.ordinal_eqType maxReg)) + (unsafeCoerce (Fintype.ord_enum maxReg))))) refs; _ -> refs}} in handleVars maxReg refs' b pos e ranges diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs --- a/LinearScan/Main.hs +++ b/LinearScan/Main.hs @@ -65,8 +65,9 @@ data Details blockType1 blockType2 = Build_Details (Prelude.Maybe ((,) Morph.SSError FinalStage)) (IntMap.IntMap LiveSets.BlockLiveSets) - ([] blockType1) ([] blockType2) (Prelude.Maybe ScanStateDescSet) (Prelude.Maybe - ScanStateDescSet) + ([] blockType1) ([] blockType1) ([] blockType2) (Prelude.Maybe + ScanStateDescSet) (Prelude.Maybe + ScanStateDescSet) Loops.LoopState linearScan :: (Monad.Monad a1) -> Prelude.Int -> (Blocks.BlockInfo a1 @@ -83,7 +84,7 @@ Prelude.Left err -> Monad.pure (Monad.is_applicative dict) (k (Build_Details (Prelude.Just ((,) err - BuildingIntervalsFailed)) liveSets' blocks1 [] + BuildingIntervalsFailed)) liveSets' blocks blocks1 [] Prelude.Nothing Prelude.Nothing loops)); Prelude.Right ssig -> let { @@ -95,7 +96,7 @@ (,) err ssig' -> Monad.pure (Monad.is_applicative dict) (k (Build_Details (Prelude.Just ((,) err - AllocatingRegistersFailed)) liveSets' blocks1 [] + AllocatingRegistersFailed)) liveSets' blocks blocks1 [] (Prelude.Just (toScanStateDescSet maxReg ( ssig))) (Prelude.Just (toScanStateDescSet maxReg ( ssig'))) loops))}; @@ -108,8 +109,8 @@ Monad.bind dict (\mappings -> Monad.bind dict (\blocks2 -> Monad.pure (Monad.is_applicative dict) - (k (Build_Details Prelude.Nothing liveSets' blocks1 - blocks2 (Prelude.Just + (k (Build_Details Prelude.Nothing liveSets' blocks + blocks1 blocks2 (Prelude.Just (toScanStateDescSet maxReg ( ssig))) (Prelude.Just (toScanStateDescSet maxReg sd)) loops))) (Assign.assignRegNum maxReg dict binfo oinfo allocs diff --git a/LinearScan/Split.hs b/LinearScan/Split.hs --- a/LinearScan/Split.hs +++ b/LinearScan/Split.hs @@ -196,35 +196,70 @@ in let { _evar_0_2 = \_ -> - (Prelude.flip (Prelude.$)) __ (\_ _ -> - let { - _evar_0_2 = \_ _ _ -> + (Prelude.flip (Prelude.$)) __ (\_ -> + (Prelude.flip (Prelude.$)) __ (\_ _ -> let { - b = Lib.lebf Prelude.snd - (Prelude.id ((,) uid beg)) - ((,) - ( - (ScanState.nextInterval - maxReg sd)) - (Interval.ibeg ( i1_1)))} + _evar_0_2 = \_ _ _ -> + let { + b = Lib.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_2 = \_ -> - Logic.coq_False_rect} + _evar_0_3 = \u' us' -> + (Prelude.flip (Prelude.$)) __ + (\_ -> Prelude.Right + (ScanState.Build_ScanStateDesc + ((Prelude.succ) + (ScanState.nextInterval maxReg + sd)) + (LinearScan.Utils.set_nth + ((Prelude.succ) + (ScanState.nextInterval maxReg + sd)) + (LinearScan.Utils.snoc + (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 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 { - _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 = \u' us' -> - (Prelude.flip (Prelude.$)) __ (\_ -> - Prelude.Right - (ScanState.Build_ScanStateDesc + sd'' = ScanState.Build_ScanStateDesc ((Prelude.succ) (ScanState.nextInterval maxReg sd)) (LinearScan.Utils.set_nth @@ -235,111 +270,83 @@ (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) - ( i1_1)) ( uid) ( i1_0)) + ( i1_1)) ( xid) ( i1_0)) (ScanState.fixedIntervals maxReg - sd) us' + sd) unh' (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 unh' of { - [] -> _evar_0_2 __ __ __; - (:) x x0 -> _evar_0_3 x x0}) __} - in - let { - _evar_0_3 = \xid reg -> - (Prelude.flip (Prelude.$)) __ (\_ _ -> - let { - sd'' = ScanState.Build_ScanStateDesc - ((Prelude.succ) - (ScanState.nextInterval maxReg sd)) - (LinearScan.Utils.set_nth - ((Prelude.succ) - (ScanState.nextInterval maxReg sd)) - (LinearScan.Utils.snoc - (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_3 = \a b -> - (Prelude.flip (Prelude.$)) __ - (\_ -> - let { - _top_assumption_1 = Morph.moveActiveToHandled - maxReg - sd'' - Prelude.True - (unsafeCoerce + (ScanState.handled maxReg 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 + Prelude.Right _top_assumption_1)} + in + case elem of { + (,) x x0 -> _evar_0_3 x x0}))) __} in let { _evar_0_4 = \xid reg -> - (Prelude.flip (Prelude.$)) __ (\_ _ -> - let { - sd'' = ScanState.Build_ScanStateDesc - ((Prelude.succ) - (ScanState.nextInterval maxReg sd)) - (LinearScan.Utils.set_nth + (Prelude.flip (Prelude.$)) __ (\_ -> + (Prelude.flip (Prelude.$)) __ (\_ _ -> + let { + sd'' = ScanState.Build_ScanStateDesc ((Prelude.succ) (ScanState.nextInterval maxReg sd)) - (LinearScan.Utils.snoc + (LinearScan.Utils.set_nth + ((Prelude.succ) (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 + sd)) + (LinearScan.Utils.snoc + (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 + Prelude.Right _top_assumption_1)} + in + case elem of { + (,) x x0 -> _evar_0_4 x x0}))) __} in case spill of { NewToHandled -> _evar_0_1; @@ -497,69 +504,70 @@ let { _evar_0_ = let { _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_) - (LinearScan.Utils.snoc - _nextInterval_ - (LinearScan.Utils.set_nth + (Prelude.flip (Prelude.$)) __ (\_ _ -> + 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_) + (LinearScan.Utils.snoc _nextInterval_ - ints uid1 - ( i0)) - ( i1)) - _fixedIntervals_ - (Lib.insert - (Lib.lebf - Prelude.snd) - ((,) - ( - _nextInterval_) - (Interval.ibeg - ( i1))) - ((:) - (Prelude.id - ((,) uid1 - beg)) + (LinearScan.Utils.set_nth + _nextInterval_ + ints uid1 + ( i0)) + ( i1)) + _fixedIntervals_ + (Lib.insert + (Lib.lebf + Prelude.snd) + ((,) + ( + _nextInterval_) + (Interval.ibeg + ( i1))) + ((:) + (Prelude.id + ((,) uid1 + beg)) + (Prelude.map + Prelude.id + us1))) (Prelude.map Prelude.id - us1))) - (Prelude.map - Prelude.id - _active_) - (Prelude.map - Prelude.id - _inactive_) - (Prelude.map - Prelude.id - _handled_))))} - in - _evar_0_0} - in - _evar_0_0)} - in - _evar_0_0 __)} - in - case unh of { - [] -> _evar_0_ uid0 us0; - (:) x x0 -> _evar_0_0 x x0 uid0 us0}} + _active_) + (Prelude.map + Prelude.id + _inactive_) + (Prelude.map + Prelude.id + _handled_))))} + 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 _evar_0_ __} in @@ -653,24 +661,26 @@ let { _evar_0_ = let { _evar_0_ = \_ _ -> - let { - sd1 = ScanState.Build_ScanStateDesc ni - (LinearScan.Utils.set_nth ni ints xid0 ( i0)) - _fixedIntervals_ unh _active_ _inactive_ - _handled_} - in - (Prelude.flip (Prelude.$)) __ (\_ -> + (Prelude.flip (Prelude.$)) __ (\_ _ -> + let { + sd1 = ScanState.Build_ScanStateDesc ni + (LinearScan.Utils.set_nth 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 spillInterval maxReg sd1 i1 uid0 beg us0 - NewToHandled 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 spillInterval maxReg sd1 i1 uid0 beg + us0 NewToHandled of { + Prelude.Left x -> _evar_0_ x; + Prelude.Right x -> _evar_0_0 x})))) __} in _evar_0_ __} in diff --git a/linearscan.cabal b/linearscan.cabal --- a/linearscan.cabal +++ b/linearscan.cabal @@ -1,5 +1,5 @@ name: linearscan -version: 0.5.0.0 +version: 0.5.1.0 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3