linearscan 0.5.0.0 → 0.5.1.0
raw patch · 5 files changed
+240/−211 lines, 5 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- LinearScan.hs +18/−9
- LinearScan/Build.hs +15/−6
- LinearScan/Main.hs +7/−6
- LinearScan/Split.hs +199/−189
- linearscan.cabal +1/−1
LinearScan.hs view
@@ -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
LinearScan/Build.hs view
@@ -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
LinearScan/Main.hs view
@@ -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
LinearScan/Split.hs view
@@ -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
linearscan.cabal view
@@ -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