linearscan 0.3.0.1 → 0.3.1.0
raw patch · 14 files changed
+911/−203 lines, 14 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- LinearScan/Assign.hs +90/−74
- LinearScan/Build.hs +26/−27
- LinearScan/IntMap.hs +169/−8
- LinearScan/Lib.hs +25/−0
- LinearScan/LiveSets.hs +240/−48
- LinearScan/Main.hs +6/−2
- LinearScan/Range.hs +3/−15
- LinearScan/Resolve.hs +7/−7
- LinearScan/Seq.hs +67/−0
- LinearScan/Split.hs +175/−9
- LinearScan/Utils.hs +17/−4
- linearscan.cabal +1/−1
- test/Main.hs +67/−2
- test/Tempest.hs +18/−6
LinearScan/Assign.hs view
@@ -15,7 +15,9 @@ import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Graph as Graph+import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Interval as Interval+import qualified LinearScan.LiveSets as LiveSets import qualified LinearScan.Resolve as Resolve import qualified LinearScan.ScanState as ScanState import qualified LinearScan.State as State@@ -102,8 +104,8 @@ savesAndRestores :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.OpId -> Blocks.VarInfo -> Blocks.PhysReg -> Interval.IntervalDesc- -> AssnState a3 ((,) ([] a2) ([] a2))-savesAndRestores maxReg oinfo opid v reg int =+ -> IntMap.IntSet -> AssnState a3 ((,) ([] a2) ([] a2))+savesAndRestores maxReg oinfo opid v reg int outs = case Blocks.varId maxReg v of { Prelude.Left p -> State.pure ((,) [] []); Prelude.Right vid ->@@ -124,65 +126,72 @@ (unsafeCoerce ((Prelude.succ) ((Prelude.succ) opid))) (unsafeCoerce (assnBlockEnd assn))))} in- case atBoundary of {- Prelude.True -> State.pure ((,) [] []);- Prelude.False ->- let {- isFirst = Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)- (unsafeCoerce (Interval.firstUsePos int))- (unsafeCoerce (Prelude.Just opid))}- in- let {- isLast = Eqtype.eq_op- (Eqtype.option_eqType- (Eqtype.sig_eqType Ssrnat.nat_eqType- (unsafeCoerce Ssrnat.odd)))- (unsafeCoerce (Interval.nextUseAfter int opid))- (unsafeCoerce Prelude.Nothing)}- in- let {save = saveOpM maxReg oinfo reg (Prelude.Just vid)} in- let {restore = restoreOpM maxReg oinfo (Prelude.Just vid) reg} in- case knd of {- Blocks.Input ->- case Interval.iknd int of {- Interval.Whole -> State.pure ((,) [] []);- Interval.LeftMost ->- case isLast of {- Prelude.True -> pairM (State.pure []) save;- Prelude.False -> State.pure ((,) [] [])};- Interval.Middle ->- case isFirst of {- Prelude.True ->- case isLast of {- Prelude.True -> pairM restore save;- Prelude.False -> pairM restore (State.pure [])};- Prelude.False ->- case isLast of {- Prelude.True -> pairM (State.pure []) save;- Prelude.False -> State.pure ((,) [] [])}};- Interval.RightMost ->- case isFirst of {- Prelude.True -> pairM restore (State.pure []);- Prelude.False -> State.pure ((,) [] [])}};- Blocks.Temp -> State.pure ((,) [] []);- Blocks.Output ->- case Interval.iknd int of {- Interval.LeftMost ->+ let {+ isFirst = Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)+ (unsafeCoerce (Interval.firstUsePos int))+ (unsafeCoerce (Prelude.Just opid))}+ in+ let {+ isLast = Eqtype.eq_op+ (Eqtype.option_eqType+ (Eqtype.sig_eqType Ssrnat.nat_eqType+ (unsafeCoerce Ssrnat.odd)))+ (unsafeCoerce (Interval.nextUseAfter int opid))+ (unsafeCoerce Prelude.Nothing)}+ in+ let {save = saveOpM maxReg oinfo reg (Prelude.Just vid)} in+ let {+ msave = case atBoundary of {+ Prelude.True -> State.pure [];+ Prelude.False -> save}}+ in+ let {restore = restoreOpM maxReg oinfo (Prelude.Just vid) reg} in+ let {+ mrestore = case atBoundary of {+ Prelude.True -> State.pure [];+ Prelude.False -> restore}}+ in+ case knd of {+ Blocks.Input ->+ case Interval.iknd int of {+ Interval.Whole -> State.pure ((,) [] []);+ Interval.LeftMost ->+ case isLast of {+ Prelude.True -> pairM (State.pure []) save;+ Prelude.False -> State.pure ((,) [] [])};+ Interval.Middle ->+ case isFirst of {+ Prelude.True -> case isLast of {- Prelude.True -> pairM (State.pure []) save;- Prelude.False -> State.pure ((,) [] [])};- Interval.Middle ->+ Prelude.True -> pairM mrestore save;+ Prelude.False -> pairM mrestore (State.pure [])};+ Prelude.False -> case isLast of { Prelude.True -> pairM (State.pure []) save;- Prelude.False -> State.pure ((,) [] [])};- _ -> State.pure ((,) [] [])}}}) State.get}+ Prelude.False -> State.pure ((,) [] [])}};+ Interval.RightMost ->+ case isFirst of {+ Prelude.True -> pairM mrestore (State.pure []);+ Prelude.False -> State.pure ((,) [] [])}};+ Blocks.Temp -> State.pure ((,) [] []);+ Blocks.Output ->+ case Interval.iknd int of {+ Interval.LeftMost ->+ case isLast of {+ Prelude.True -> pairM (State.pure []) msave;+ Prelude.False -> State.pure ((,) [] [])};+ Interval.Middle ->+ case isLast of {+ Prelude.True -> pairM (State.pure []) msave;+ Prelude.False -> State.pure ((,) [] [])};+ _ -> State.pure ((,) [] [])}}) State.get} collectAllocs :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Prelude.Int ->- ([] ((,) Interval.IntervalDesc PhysReg)) -> ((,)- ((,) ([] ((,) Blocks.VarId PhysReg)) ([] a2)) ([] a2)) ->- Blocks.VarInfo -> State.State (AssnStateInfo a3)+ IntMap.IntSet -> ([] ((,) Interval.IntervalDesc PhysReg)) -> ((,) ((,) ([] ((,) Blocks.VarId PhysReg)) ([] a2)) ([] a2))-collectAllocs maxReg oinfo opid ints acc v =+ -> Blocks.VarInfo -> State.State (AssnStateInfo a3)+ ((,) ((,) ([] ((,) Blocks.VarId PhysReg)) ([] a2)) ([] a2))+collectAllocs maxReg oinfo opid outs ints acc v = case Blocks.varId maxReg v of { Prelude.Left p -> State.pure acc; Prelude.Right vid ->@@ -202,12 +211,12 @@ (,) rs ss -> State.pure ((,) ((,) ((:) ((,) vid reg) allocs') ((Prelude.++) rs restores')) ((Prelude.++) ss saves'))})- (savesAndRestores maxReg oinfo opid v reg int)}}})}+ (savesAndRestores maxReg oinfo opid v reg int outs)}}})} doAllocations :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]- ((,) Interval.IntervalDesc PhysReg)) -> a1 -> AssnState - a3 ([] a2)-doAllocations maxReg oinfo ints op =+ ((,) Interval.IntervalDesc PhysReg)) -> IntMap.IntSet -> a1+ -> AssnState a3 ([] a2)+doAllocations maxReg oinfo ints outs op = State.bind (\assn -> let {opid = assnOpId assn} in let {vars = Blocks.opRefs maxReg oinfo op} in@@ -223,7 +232,7 @@ ((Prelude.succ) opid)) (assnBlockBeg assn') (assnBlockEnd assn') (assnAcc assn')))}}) (State.forFoldM ((,) ((,) [] []) []) vars- (collectAllocs maxReg oinfo opid ints))) State.get+ (collectAllocs maxReg oinfo opid outs ints))) State.get generateMoves :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([] ((,) (Prelude.Maybe (Prelude.Either PhysReg Prelude.Int))@@ -274,10 +283,10 @@ Prelude.Nothing -> State.pure Prelude.Nothing}}})) resolveMappings :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Prelude.Int ->- ([] a2) -> (Data.IntMap.IntMap- ((,) Graph.Graph Graph.Graph)) -> AssnState a3 ([] a2)+ ([] a2) -> (IntMap.IntMap ((,) Graph.Graph Graph.Graph))+ -> AssnState a3 ([] a2) resolveMappings maxReg oinfo bid opsm mappings =- case Data.IntMap.lookup bid mappings of {+ case IntMap.coq_IntMap_lookup bid mappings of { Prelude.Just graphs -> case graphs of { (,) gbeg gend ->@@ -298,12 +307,19 @@ Prelude.Nothing -> State.pure opsm} considerOps :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- (Blocks.OpInfo a5 a3 a4) -> (a3 -> AssnState a5 ([] a4)) ->- (Data.IntMap.IntMap ((,) Graph.Graph Graph.Graph)) -> ([] - a1) -> State.State (AssnStateInfo a5) ([] a2)-considerOps maxReg binfo oinfo f mappings =+ (Blocks.OpInfo a5 a3 a4) -> (IntMap.IntSet -> a3 -> AssnState+ a5 ([] a4)) -> (IntMap.IntMap LiveSets.BlockLiveSets) ->+ (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) -> ([] a1) ->+ State.State (AssnStateInfo a5) ([] a2)+considerOps maxReg binfo oinfo f liveSets mappings = State.mapM (\blk -> let {ops = Blocks.blockOps binfo blk} in+ let {bid = Blocks.blockId binfo blk} in+ let {+ outs = case IntMap.coq_IntMap_lookup bid liveSets of {+ Prelude.Just ls -> LiveSets.blockLiveOut ls;+ Prelude.Nothing -> IntMap.emptyIntSet}}+ in case ops of { (,) p opse -> case p of {@@ -312,13 +328,13 @@ State.bind (\opsb' -> State.bind (\opsm' -> State.bind (\opse' ->- let {bid = Blocks.blockId binfo blk} in State.bind (\opsm'' -> State.pure (Blocks.setBlockOps binfo blk opsb' opsm'' opse')) (resolveMappings maxReg oinfo bid opsm' mappings))- (State.concatMapM f opse)) (State.concatMapM f opsm))- (State.concatMapM f opsb))+ (State.concatMapM (f outs) opse))+ (State.concatMapM (f outs) opsm))+ (State.concatMapM (f outs) opsb)) (State.modify (\assn -> Build_AssnStateInfo (assnOpId assn) ((Prelude.+) (assnOpId assn) (Ssrnat.double (Data.List.length opsb)))@@ -329,9 +345,9 @@ assignRegNum :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ScanState.ScanStateDesc ->- (Data.IntMap.IntMap Resolve.BlockMoves) -> ([] a1) -> a5 ->- (,) ([] a2) a5-assignRegNum maxReg binfo oinfo sd mappings blocks acc =+ (IntMap.IntMap LiveSets.BlockLiveSets) -> (IntMap.IntMap+ Resolve.BlockMoves) -> ([] a1) -> a5 -> (,) ([] a2) a5+assignRegNum maxReg binfo oinfo sd liveSets mappings blocks acc = case considerOps maxReg binfo oinfo (doAllocations maxReg oinfo (Prelude.map (\x -> (,)@@ -342,7 +358,7 @@ (Prelude.snd x)) ((Prelude.++) (ScanState.handled maxReg sd) ((Prelude.++) (ScanState.active maxReg sd)- (ScanState.inactive maxReg sd))))) mappings blocks+ (ScanState.inactive maxReg sd))))) liveSets mappings blocks (Build_AssnStateInfo ((Prelude.succ) 0) ((Prelude.succ) 0) ((Prelude.succ) 0) acc) of { (,) blocks' assn -> (,) blocks' (assnAcc assn)}
LinearScan/Build.hs view
@@ -46,7 +46,7 @@ __ :: any __ = Prelude.error "Logical or arity value used" -type BuildState = Data.IntMap.IntMap Range.SortedRanges+type BuildState = IntMap.IntMap Range.SortedRanges newBuildState :: Prelude.Int -> BuildState newBuildState n =@@ -69,21 +69,21 @@ case c of { Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1} -type PendingRanges = (Data.IntMap.IntMap RangeCursor)+type PendingRanges = (IntMap.IntMap RangeCursor) emptyPendingRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->- Prelude.Int -> Data.IntSet.IntSet -> PendingRanges+ Prelude.Int -> IntMap.IntSet -> PendingRanges emptyPendingRanges maxReg b pos e liveOuts = (Prelude.flip (Prelude.$)) (emptyRangeCursor b pos e) (\empty -> (Prelude.flip (Prelude.$)) (\xs vid ->- Data.IntMap.insert ((Prelude.+) vid maxReg) empty xs) (\f ->- Data.IntSet.foldl' f IntMap.emptyIntMap liveOuts))+ IntMap.coq_IntMap_insert ((Prelude.+) vid maxReg) empty xs) (\f ->+ IntMap.coq_IntSet_foldl f IntMap.emptyIntMap liveOuts)) mergeIntoSortedRanges :: Prelude.Int -> Prelude.Int -> PendingRanges ->- (Data.IntMap.IntMap Range.SortedRanges) ->- Data.IntMap.IntMap Range.SortedRanges+ (IntMap.IntMap Range.SortedRanges) -> IntMap.IntMap+ Range.SortedRanges mergeIntoSortedRanges b pos pmap rmap =- Data.IntMap.mergeWithKey (\_the_1st_wildcard_ _top_assumption_ ->+ IntMap.coq_IntMap_mergeWithKey (\_the_1st_wildcard_ _top_assumption_ -> let { _evar_0_ = \mid br ps rs -> (Prelude.flip (Prelude.$)) __ (\_ ->@@ -99,7 +99,7 @@ (\rs -> case _top_assumption_ of { Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1 rs}))- (Data.IntMap.map (\_top_assumption_ ->+ (IntMap.coq_IntMap_map (\_top_assumption_ -> let { _evar_0_ = \_cursorMid_ br rs -> (Prelude.flip (Prelude.$)) __ (\_ ->@@ -110,7 +110,7 @@ in case _top_assumption_ of { Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}))- (Data.IntMap.map+ (IntMap.coq_IntMap_map (Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b)) ((Prelude.succ) (Ssrnat.double pos)))) ( pmap) rmap @@ -196,17 +196,16 @@ Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1} handleVars_onlyRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->- (Data.IntMap.IntMap RangeCursor) ->- Data.IntMap.IntMap RangeCursor+ (IntMap.IntMap RangeCursor) -> IntMap.IntMap+ RangeCursor handleVars_onlyRanges b pos e =- Data.IntMap.map (transportRangeCursor b ((Prelude.succ) pos) pos e)+ IntMap.coq_IntMap_map (transportRangeCursor b ((Prelude.succ) pos) pos e) handleVars_onlyVars :: Prelude.Int -> Prelude.Int -> Prelude.Int ->- (Data.IntMap.IntMap- ((,) Prelude.Bool ([] Blocks.VarKind))) ->- Data.IntMap.IntMap RangeCursor+ (IntMap.IntMap ((,) Prelude.Bool ([] Blocks.VarKind)))+ -> IntMap.IntMap RangeCursor handleVars_onlyVars b pos e =- Data.IntMap.map (\_top_assumption_ ->+ IntMap.coq_IntMap_map (\_top_assumption_ -> let { _evar_0_ = \req kinds -> let {@@ -243,10 +242,10 @@ Prelude.Int -> Prelude.Int -> PendingRanges -> PendingRanges handleVars maxReg varRefs b pos e ranges = let {- vars = Data.IntMap.map (extractVarInfo maxReg)+ vars = IntMap.coq_IntMap_map (extractVarInfo maxReg) (IntMap.coq_IntMap_groupOn (Blocks.nat_of_varId maxReg) varRefs)} in- Data.IntMap.mergeWithKey (handleVars_combine b pos e)+ IntMap.coq_IntMap_mergeWithKey (handleVars_combine b pos e) (handleVars_onlyRanges b pos e) (handleVars_onlyVars b pos e) ( ranges) vars @@ -294,7 +293,7 @@ _evar_0_ reduceBlocks :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (Data.IntMap.IntMap+ (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Int -> BuildState reduceBlocks maxReg binfo oinfo blocks liveSets pos = let {_evar_0_ = \pos0 -> newBuildState pos0} in@@ -302,9 +301,9 @@ _evar_0_0 = \b blocks0 iHbs pos0 -> (Prelude.flip (Prelude.$)) (Blocks.blockId binfo b) (\bid -> (Prelude.flip (Prelude.$))- (case Data.IntMap.lookup bid liveSets of {+ (case IntMap.coq_IntMap_lookup bid liveSets of { Prelude.Just ls -> LiveSets.blockLiveOut ls;- Prelude.Nothing -> Data.IntSet.empty}) (\outs ->+ Prelude.Nothing -> IntMap.emptyIntSet}) (\outs -> let {sz = Blocks.blockSize binfo b} in let { _evar_0_0 = \_ ->@@ -326,9 +325,9 @@ compileIntervals :: Prelude.Int -> Prelude.Int -> BuildState -> (,) ScanState.FixedIntervalsType- (Data.IntMap.IntMap Interval.IntervalDesc)+ (IntMap.IntMap Interval.IntervalDesc) compileIntervals maxReg pos bs =- Data.IntMap.foldlWithKey (\_top_assumption_ ->+ IntMap.coq_IntMap_foldlWithKey (\_top_assumption_ -> let { _evar_0_ = \regs vars vid rs -> let {_evar_0_ = \_ -> (,) regs vars} in@@ -348,7 +347,7 @@ _evar_0_1 = \_ -> (Prelude.flip (Prelude.$)) ((Prelude.-) vid maxReg) (\vid' -> (,) regs- (Data.IntMap.insert vid'+ (IntMap.coq_IntMap_insert vid' (Interval.packInterval (Interval.Build_IntervalDesc vid' (Range.rbeg ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))@@ -369,7 +368,7 @@ (Data.List.replicate maxReg Prelude.Nothing) IntMap.emptyIntMap) bs buildIntervals :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (Data.IntMap.IntMap+ (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Either Morph.SSError ScanState.ScanStateSig buildIntervals maxReg binfo oinfo blocks liveSets =@@ -414,6 +413,6 @@ (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0 [] (Data.List.replicate maxReg Prelude.Nothing) [] [] [] [])))} in- let {s3 = Data.IntMap.foldl handleVar s2 vars} in+ let {s3 = IntMap.coq_IntMap_foldl handleVar s2 vars} in Prelude.Right (ScanState.packScanState maxReg ScanState.InUse ( s3))}}
LinearScan/IntMap.hs view
@@ -14,6 +14,10 @@ import qualified LinearScan.Utils import qualified LinearScan.Lib as Lib+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrnat as Ssrnat @@ -27,21 +31,178 @@ unsafeCoerce = IOExts.unsafeCoerce #endif -emptyIntMap :: Data.IntMap.IntMap a1+__ :: any+__ = Prelude.error "Logical or arity value used"++type IntMap a =+ [] ((,) Prelude.Int a)+ -- singleton inductive, whose constructor was getIntMap+ +emptyIntMap :: IntMap a1 emptyIntMap =- Data.IntMap.fromList []+ [] -coq_IntSet_forFold :: a1 -> Data.IntSet.IntSet -> (a1 -> Prelude.Int -> a1)- -> a1+coq_IntMap_lookup :: Prelude.Int -> (IntMap a1) -> Prelude.Maybe a1+coq_IntMap_lookup k m =+ Lib.maybeLookup Ssrnat.nat_eqType (unsafeCoerce m) (unsafeCoerce k)++coq_IntMap_alter :: ((Prelude.Maybe a1) -> Prelude.Maybe a1) -> Prelude.Int+ -> (IntMap a1) -> IntMap a1+coq_IntMap_alter f k m =+ case coq_IntMap_lookup k m of {+ Prelude.Just x ->+ Prelude.foldr (\z acc ->+ case z of {+ (,) a b ->+ case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce a) (unsafeCoerce k) of {+ Prelude.True ->+ case f (Prelude.Just x) of {+ Prelude.Just x' -> Seq.rcons acc ((,) k x');+ Prelude.Nothing -> acc};+ Prelude.False -> (:) z acc}}) [] m;+ Prelude.Nothing ->+ case f Prelude.Nothing of {+ Prelude.Just x -> Seq.rcons m ((,) k x);+ Prelude.Nothing -> m}}++coq_IntMap_insert :: Prelude.Int -> a1 -> (IntMap a1) -> IntMap a1+coq_IntMap_insert k x m =+ coq_IntMap_alter (\x0 -> Prelude.Just x) k m++coq_IntMap_map :: (a1 -> a2) -> (IntMap a1) -> IntMap a2+coq_IntMap_map f m =+ Prelude.map (\x -> (,) (Prelude.fst x) (f (Prelude.snd x))) m++coq_IntMap_mergeWithKey :: (Prelude.Int -> a1 -> a2 -> Prelude.Maybe + a3) -> ((IntMap a1) -> IntMap a3) -> ((IntMap + a2) -> IntMap a3) -> (IntMap a1) -> (IntMap + a2) -> IntMap a3+coq_IntMap_mergeWithKey combine only1 only2 m1 m2 =+ let {only1' = \xs -> only1 xs} in+ let {only2' = \xs -> only2 xs} in+ LinearScan.Utils.intMap_mergeWithKey' combine only1' only2' m1 m2++coq_IntMap_foldl :: (a1 -> a2 -> a1) -> a1 -> (IntMap a2) -> a1+coq_IntMap_foldl f z m =+ Data.List.foldl' (\acc x -> f acc (Prelude.snd x)) z m++coq_IntMap_foldlWithKey :: (a1 -> Prelude.Int -> a2 -> a1) -> a1 -> (IntMap+ a2) -> a1+coq_IntMap_foldlWithKey f z m =+ Data.List.foldl' (\acc x -> f acc (Prelude.fst x) (Prelude.snd x)) z m++eqIntMap :: Eqtype.Equality__Coq_type -> (IntMap Eqtype.Equality__Coq_sort)+ -> (IntMap Eqtype.Equality__Coq_sort) -> Prelude.Bool+eqIntMap a s1 s2 =+ Eqtype.eq_op (Seq.seq_eqType (Eqtype.prod_eqType Ssrnat.nat_eqType a))+ (unsafeCoerce s1) (unsafeCoerce s2)++eqIntMapP :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_axiom+ (IntMap Eqtype.Equality__Coq_sort)+eqIntMapP a _top_assumption_ =+ let {+ _evar_0_ = \s1 _top_assumption_0 ->+ let {+ _evar_0_ = \s2 ->+ let {_evar_0_ = \_ -> let {_evar_0_ = Ssrbool.ReflectT} in _evar_0_}+ in+ let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP+ (Seq.seq_eqType (Eqtype.prod_eqType Ssrnat.nat_eqType a)) s1 s2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ unsafeCoerce _evar_0_ _top_assumption_0}+ in+ unsafeCoerce _evar_0_ _top_assumption_++coq_IntMap_eqMixin :: Eqtype.Equality__Coq_type ->+ Eqtype.Equality__Coq_mixin_of+ (IntMap Eqtype.Equality__Coq_sort)+coq_IntMap_eqMixin a =+ Eqtype.Equality__Mixin (eqIntMap a) (eqIntMapP a)++coq_IntMap_eqType :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type+coq_IntMap_eqType a =+ unsafeCoerce (coq_IntMap_eqMixin a)++type IntSet =+ [] Prelude.Int+ -- singleton inductive, whose constructor was getIntSet+ +emptyIntSet :: IntSet+emptyIntSet =+ []++coq_IntSet_member :: Prelude.Int -> IntSet -> Prelude.Bool+coq_IntSet_member k m =+ Ssrbool.in_mem (unsafeCoerce k)+ (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m))++coq_IntSet_insert :: Prelude.Int -> IntSet -> IntSet+coq_IntSet_insert k m =+ case Ssrbool.in_mem (unsafeCoerce k)+ (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m)) of {+ Prelude.True -> m;+ Prelude.False -> (:) k m}++coq_IntSet_union :: IntSet -> IntSet -> IntSet+coq_IntSet_union m1 m2 =+ unsafeCoerce+ (Seq.undup Ssrnat.nat_eqType+ ((Prelude.++) (unsafeCoerce m1) (unsafeCoerce m2)))++coq_IntSet_difference :: IntSet -> IntSet -> IntSet+coq_IntSet_difference m1 m2 =+ Prelude.filter (\k ->+ Prelude.not+ (Ssrbool.in_mem (unsafeCoerce k)+ (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m2))))+ m1++coq_IntSet_foldl :: (a1 -> Prelude.Int -> a1) -> a1 -> IntSet -> a1+coq_IntSet_foldl f z m =+ Data.List.foldl' f z m++coq_IntSet_forFold :: a1 -> IntSet -> (a1 -> Prelude.Int -> a1) -> a1 coq_IntSet_forFold z m f =- Data.IntSet.foldl' f z m+ coq_IntSet_foldl f z m -coq_IntMap_groupOn :: (a1 -> Prelude.Int) -> ([] a1) -> Data.IntMap.IntMap- ([] a1)+eqIntSet :: IntSet -> IntSet -> Prelude.Bool+eqIntSet s1 s2 =+ Eqtype.eq_op (Seq.seq_eqType Ssrnat.nat_eqType) (unsafeCoerce s1)+ (unsafeCoerce s2)++eqIntSetP :: Eqtype.Equality__Coq_axiom IntSet+eqIntSetP _top_assumption_ =+ let {+ _evar_0_ = \s1 _top_assumption_0 ->+ let {+ _evar_0_ = \s2 ->+ let {_evar_0_ = \_ -> let {_evar_0_ = Ssrbool.ReflectT} in _evar_0_}+ in+ let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP (Seq.seq_eqType Ssrnat.nat_eqType) s1 s2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ unsafeCoerce _evar_0_ _top_assumption_0}+ in+ unsafeCoerce _evar_0_ _top_assumption_++coq_IntSet_eqMixin :: Eqtype.Equality__Coq_mixin_of IntSet+coq_IntSet_eqMixin =+ Eqtype.Equality__Mixin eqIntSet eqIntSetP++coq_IntSet_eqType :: Eqtype.Equality__Coq_type+coq_IntSet_eqType =+ unsafeCoerce coq_IntSet_eqMixin++coq_IntMap_groupOn :: (a1 -> Prelude.Int) -> ([] a1) -> IntMap ([] a1) coq_IntMap_groupOn p l = Lib.forFold emptyIntMap l (\acc x -> let {n = p x} in- Data.IntMap.alter (\mxs ->+ coq_IntMap_alter (\mxs -> case mxs of { Prelude.Just xs -> Prelude.Just ((:) x xs); Prelude.Nothing -> Prelude.Just ((:) x [])}) n acc)
LinearScan/Lib.hs view
@@ -24,6 +24,19 @@ Prelude.Just a -> x; Prelude.Nothing -> y} +maybeLookup :: Eqtype.Equality__Coq_type -> ([]+ ((,) Eqtype.Equality__Coq_sort a1)) ->+ Eqtype.Equality__Coq_sort -> Prelude.Maybe a1+maybeLookup a v x =+ case v of {+ [] -> Prelude.Nothing;+ (:) p xs ->+ case p of {+ (,) k v0 ->+ case Eqtype.eq_op a k x of {+ Prelude.True -> Prelude.Just v0;+ Prelude.False -> maybeLookup a xs x}}}+ lebf :: (a1 -> Prelude.Int) -> a1 -> a1 -> Prelude.Bool lebf f n m = (Prelude.<=) (f n) (f m)@@ -38,6 +51,10 @@ forFold b v f = Data.List.foldl' f b v +forFoldr :: a2 -> ([] a1) -> (a1 -> a2 -> a2) -> a2+forFoldr b v f =+ Prelude.foldr f b v+ span :: (a1 -> Prelude.Bool) -> ([] a1) -> (,) ([] a1) ([] a1) span p l = case l of {@@ -48,6 +65,14 @@ case span p xs of { (,) ys zs -> (,) ((:) x ys) zs}; Prelude.False -> (,) [] l}}++partition :: (a1 -> Prelude.Bool) -> ([] a1) -> (,) ([] a1) ([] a1)+partition p =+ Prelude.foldr (\x acc ->+ case p x of {+ Prelude.True -> (,) ((:) x (Prelude.fst acc)) (Prelude.snd acc);+ Prelude.False -> (,) (Prelude.fst acc) ((:) x (Prelude.snd acc))}) ((,)+ [] []) insert :: (Ssrbool.Coq_rel a1) -> a1 -> ([] a1) -> [] a1 insert p z l =
LinearScan/LiveSets.hs view
@@ -1,3 +1,6 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}+ module LinearScan.LiveSets where @@ -13,33 +16,48 @@ import qualified LinearScan.Blocks as Blocks import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Lib as Lib-import qualified LinearScan.Seq as Seq+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrnat as Ssrnat ++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"+ data BlockLiveSets =- Build_BlockLiveSets Data.IntSet.IntSet Data.IntSet.IntSet Data.IntSet.IntSet - Data.IntSet.IntSet Blocks.OpId Blocks.OpId+ Build_BlockLiveSets IntMap.IntSet IntMap.IntSet IntMap.IntSet IntMap.IntSet + Blocks.OpId Blocks.OpId -blockLiveGen :: BlockLiveSets -> Data.IntSet.IntSet+blockLiveGen :: BlockLiveSets -> IntMap.IntSet blockLiveGen b = case b of { Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0 blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveGen0} -blockLiveKill :: BlockLiveSets -> Data.IntSet.IntSet+blockLiveKill :: BlockLiveSets -> IntMap.IntSet blockLiveKill b = case b of { Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0 blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveKill0} -blockLiveIn :: BlockLiveSets -> Data.IntSet.IntSet+blockLiveIn :: BlockLiveSets -> IntMap.IntSet blockLiveIn b = case b of { Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0 blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveIn0} -blockLiveOut :: BlockLiveSets -> Data.IntSet.IntSet+blockLiveOut :: BlockLiveSets -> IntMap.IntSet blockLiveOut b = case b of { Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0@@ -57,9 +75,143 @@ Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0 blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLastOpId0} +eqBlockLiveSets :: BlockLiveSets -> BlockLiveSets -> Prelude.Bool+eqBlockLiveSets s1 s2 =+ case s1 of {+ Build_BlockLiveSets lg1 lk1 li1 lo1 fi1 la1 ->+ case s2 of {+ Build_BlockLiveSets lg2 lk2 li2 lo2 fi2 la2 ->+ (Prelude.&&)+ (Eqtype.eq_op IntMap.coq_IntSet_eqType (unsafeCoerce lg1)+ (unsafeCoerce lg2))+ ((Prelude.&&)+ (Eqtype.eq_op IntMap.coq_IntSet_eqType (unsafeCoerce lk1)+ (unsafeCoerce lk2))+ ((Prelude.&&)+ (Eqtype.eq_op IntMap.coq_IntSet_eqType (unsafeCoerce li1)+ (unsafeCoerce li2))+ ((Prelude.&&)+ (Eqtype.eq_op IntMap.coq_IntSet_eqType (unsafeCoerce lo1)+ (unsafeCoerce lo2))+ ((Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fi1)+ (unsafeCoerce fi2))+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce la1)+ (unsafeCoerce la2))))))}}++eqBlockLiveSetsP :: Eqtype.Equality__Coq_axiom BlockLiveSets+eqBlockLiveSetsP _top_assumption_ =+ let {+ _evar_0_ = \lg1 lk1 li1 lo1 fi1 la1 _top_assumption_0 ->+ let {+ _evar_0_ = \lg2 lk2 li2 lo2 fi2 la2 ->+ let {+ _evar_0_ = \_ ->+ let {+ _evar_0_ = let {+ _evar_0_ = \_ ->+ let {+ _evar_0_ = 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+ Ssrnat.nat_eqType+ la1 la2 of {+ Ssrbool.ReflectT ->+ _evar_0_+ __;+ Ssrbool.ReflectF ->+ _evar_0_0+ __}}+ in+ _evar_0_}+ in+ let {+ _evar_0_0 = \_ ->+ Ssrbool.ReflectF}+ in+ case Eqtype.eqP+ Ssrnat.nat_eqType+ fi1 fi2 of {+ Ssrbool.ReflectT ->+ _evar_0_ __;+ Ssrbool.ReflectF ->+ _evar_0_0 __}}+ in+ _evar_0_}+ in+ let {+ _evar_0_0 = \_ ->+ Ssrbool.ReflectF}+ in+ case Eqtype.eqP+ IntMap.coq_IntSet_eqType+ lo1 lo2 of {+ Ssrbool.ReflectT ->+ _evar_0_ __;+ Ssrbool.ReflectF ->+ _evar_0_0 __}}+ in+ _evar_0_}+ in+ let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP IntMap.coq_IntSet_eqType+ li1 li2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ _evar_0_}+ in+ let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP IntMap.coq_IntSet_eqType lk1 lk2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ _evar_0_}+ in+ let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP IntMap.coq_IntSet_eqType lg1 lg2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ case _top_assumption_0 of {+ Build_BlockLiveSets x x0 x1 x2 x3 x4 ->+ unsafeCoerce _evar_0_ x x0 x1 x2 x3 x4}}+ in+ case _top_assumption_ of {+ Build_BlockLiveSets x x0 x1 x2 x3 x4 ->+ unsafeCoerce _evar_0_ x x0 x1 x2 x3 x4}++coq_BlockLiveSets_eqMixin :: Eqtype.Equality__Coq_mixin_of BlockLiveSets+coq_BlockLiveSets_eqMixin =+ Eqtype.Equality__Mixin eqBlockLiveSets eqBlockLiveSetsP++coq_BlockLiveSets_eqType :: Eqtype.Equality__Coq_type+coq_BlockLiveSets_eqType =+ unsafeCoerce coq_BlockLiveSets_eqMixin+ computeLocalLiveSets :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- (Blocks.OpInfo a5 a3 a4) -> ([] a1) ->- Data.IntMap.IntMap BlockLiveSets+ (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> IntMap.IntMap+ BlockLiveSets computeLocalLiveSets maxReg binfo oinfo blocks = Prelude.snd (Lib.forFold ((,) ((Prelude.succ) 0) IntMap.emptyIntMap) blocks@@ -71,8 +223,8 @@ case p of { (,) opsb opsm -> let {- liveSet = Build_BlockLiveSets Data.IntSet.empty- Data.IntSet.empty Data.IntSet.empty Data.IntSet.empty+ liveSet = Build_BlockLiveSets IntMap.emptyIntSet+ IntMap.emptyIntSet IntMap.emptyIntSet IntMap.emptyIntSet ((Prelude.+) idx (Ssrnat.double (Data.List.length opsb))) idx} in case Lib.forFold ((,) idx liveSet)@@ -80,55 +232,95 @@ case acc0 of { (,) lastIdx liveSet1 -> (,) ((Prelude.succ) ((Prelude.succ) lastIdx))- (Lib.forFold liveSet1 (Blocks.opRefs maxReg oinfo o)- (\liveSet2 v ->- case Blocks.varId maxReg v of {- Prelude.Left p0 -> liveSet2;- Prelude.Right vid ->- case Blocks.varKind maxReg v of {- Blocks.Input ->- case Prelude.not- (Data.IntSet.member vid- (blockLiveKill liveSet2)) of {- Prelude.True -> Build_BlockLiveSets- (Data.IntSet.insert vid (blockLiveGen liveSet2))- (blockLiveKill liveSet2) (blockLiveIn liveSet2)- (blockLiveOut liveSet2)- (blockFirstOpId liveSet2) lastIdx;- Prelude.False -> liveSet2};- _ -> Build_BlockLiveSets (blockLiveGen liveSet2)- (Data.IntSet.insert vid (blockLiveKill liveSet2))- (blockLiveIn liveSet2) (blockLiveOut liveSet2)- (blockFirstOpId liveSet2) lastIdx}}))}) of {+ (case Lib.partition (\v ->+ Eqtype.eq_op Blocks.coq_VarKind_eqType+ (unsafeCoerce (Blocks.varKind maxReg v))+ (unsafeCoerce Blocks.Input))+ (Blocks.opRefs maxReg oinfo o) of {+ (,) inputs others ->+ let {+ liveSet2 = Lib.forFold liveSet1 inputs+ (\liveSet2 v ->+ case Blocks.varId maxReg v of {+ Prelude.Left p0 -> liveSet2;+ Prelude.Right vid ->+ case Prelude.not+ (IntMap.coq_IntSet_member vid+ (blockLiveKill liveSet2)) of {+ Prelude.True -> Build_BlockLiveSets+ (IntMap.coq_IntSet_insert vid+ (blockLiveGen liveSet2))+ (blockLiveKill liveSet2)+ (blockLiveIn liveSet2)+ (blockLiveOut liveSet2)+ (blockFirstOpId liveSet2) lastIdx;+ Prelude.False -> liveSet2}})}+ in+ let {+ liveSet3 = Lib.forFold liveSet2 others+ (\liveSet3 v ->+ case Blocks.varId maxReg v of {+ Prelude.Left p0 -> liveSet3;+ Prelude.Right vid ->+ Build_BlockLiveSets+ (blockLiveGen liveSet3)+ (IntMap.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 -> (,) lastIdx'- (Data.IntMap.insert (Blocks.blockId binfo b) liveSet3 m)}}}}))+ (IntMap.coq_IntMap_insert (Blocks.blockId binfo b) liveSet3 m)}}}})) computeGlobalLiveSets :: (Blocks.BlockInfo a1 a2 a3 a4) -> ([] a1) ->- (Data.IntMap.IntMap BlockLiveSets) ->- Data.IntMap.IntMap BlockLiveSets+ (IntMap.IntMap BlockLiveSets) -> IntMap.IntMap+ BlockLiveSets computeGlobalLiveSets binfo blocks liveSets =- Lib.forFold liveSets (Seq.rev blocks) (\liveSets1 b ->+ Lib.forFoldr liveSets blocks (\b liveSets1 -> let {bid = Blocks.blockId binfo b} in- case Data.IntMap.lookup bid liveSets1 of {+ case IntMap.coq_IntMap_lookup bid liveSets1 of { Prelude.Just liveSet -> let { liveSet2 = Lib.forFold liveSet (Blocks.blockSuccessors binfo b)- (\liveSet1 s_bid ->- case Data.IntMap.lookup s_bid liveSets1 of {+ (\liveSet2 s_bid ->+ case IntMap.coq_IntMap_lookup s_bid liveSets1 of { Prelude.Just sux -> Build_BlockLiveSets- (blockLiveGen liveSet1) (blockLiveKill liveSet1)- (blockLiveIn liveSet1)- (Data.IntSet.union (blockLiveOut liveSet1)- (blockLiveIn sux)) (blockFirstOpId liveSet1)- (blockLastOpId liveSet1);- Prelude.Nothing -> liveSet1})}+ (blockLiveGen liveSet2) (blockLiveKill liveSet2)+ (blockLiveIn liveSet2)+ (IntMap.coq_IntSet_union (blockLiveOut liveSet2)+ (blockLiveIn sux)) (blockFirstOpId liveSet2)+ (blockLastOpId liveSet2);+ Prelude.Nothing -> liveSet2})} in- Data.IntMap.insert bid (Build_BlockLiveSets (blockLiveGen liveSet2)- (blockLiveKill liveSet2)- (Data.IntSet.union- (Data.IntSet.difference (blockLiveOut liveSet2)+ IntMap.coq_IntMap_insert bid (Build_BlockLiveSets+ (blockLiveGen liveSet2) (blockLiveKill liveSet2)+ (IntMap.coq_IntSet_union+ (IntMap.coq_IntSet_difference (blockLiveOut liveSet2) (blockLiveKill liveSet2)) (blockLiveGen liveSet2)) (blockLiveOut liveSet2) (blockFirstOpId liveSet2) (blockLastOpId liveSet2)) liveSets1; Prelude.Nothing -> liveSets1})++computeGlobalLiveSetsRecursively :: (Blocks.BlockInfo a1 a2 a3 a4) -> ([] + a1) -> (IntMap.IntMap BlockLiveSets) ->+ IntMap.IntMap BlockLiveSets+computeGlobalLiveSetsRecursively binfo blocks liveSets =+ let {+ go n previous =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ previous)+ (\n0 ->+ let {computed = computeGlobalLiveSets binfo blocks previous} in+ case Eqtype.eq_op (IntMap.coq_IntMap_eqType coq_BlockLiveSets_eqType)+ (unsafeCoerce previous) (unsafeCoerce computed) of {+ Prelude.True -> computed;+ Prelude.False -> go n0 computed})+ n}+ in go (Data.List.length blocks) liveSets
LinearScan/Main.hs view
@@ -27,7 +27,10 @@ let {blocks' = Order.computeBlockOrder blocks} in let {liveSets = LiveSets.computeLocalLiveSets maxReg binfo oinfo blocks'} in- let {liveSets' = LiveSets.computeGlobalLiveSets binfo blocks' liveSets} in+ let {+ liveSets' = LiveSets.computeGlobalLiveSetsRecursively binfo blocks'+ liveSets}+ in case Build.buildIntervals maxReg binfo oinfo blocks liveSets' of { Prelude.Left err -> Prelude.Left err; Prelude.Right ssig ->@@ -40,5 +43,6 @@ liveSets'} in Prelude.Right- (Assign.assignRegNum maxReg binfo oinfo ( ssig') mappings blocks accum)}}+ (Assign.assignRegNum maxReg binfo oinfo ( ssig') liveSets' mappings+ blocks accum)}}
LinearScan/Range.hs view
@@ -221,22 +221,10 @@ let { _evar_0_1 = \_ -> (Prelude.flip (Prelude.$)) __ (\_ ->- let {- _evar_0_1 = \_ _ _ _ -> (,) (Prelude.Just+ (Prelude.flip (Prelude.$)) __ (\_ -> (,) (Prelude.Just (packRange (Build_RangeDesc rbeg0 before l1)))- Prelude.Nothing}- in- let {- _evar_0_2 = \u us ->- (Prelude.flip (Prelude.$)) __ (\_ -> (,) (Prelude.Just- (packRange (Build_RangeDesc rbeg0 before l1)))- (Prelude.Just- (packRange (Build_RangeDesc (UsePos.uloc u) rend0- ((:) u us)))))}- in- case l2 of {- [] -> _evar_0_1 __ __ __ __;- (:) x x0 -> _evar_0_2 x x0})}+ (Prelude.Just+ (packRange (Build_RangeDesc before rend0 l2)))))} in _evar_0_1 __} in
LinearScan/Resolve.hs view
@@ -41,8 +41,8 @@ checkIntervalBoundary :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int -> Prelude.Bool -> LiveSets.BlockLiveSets -> LiveSets.BlockLiveSets ->- (Data.IntMap.IntMap ((,) Graph.Graph Graph.Graph))- -> Prelude.Int -> Data.IntMap.IntMap+ (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) ->+ Prelude.Int -> IntMap.IntMap ((,) Graph.Graph Graph.Graph) checkIntervalBoundary maxReg sd bid in_from from to mappings vid = let {@@ -104,17 +104,17 @@ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType))}))} in- Data.IntMap.alter f0 bid mappings}}+ IntMap.coq_IntMap_alter f0 bid mappings}} type BlockMoves = (,) Graph.Graph Graph.Graph resolveDataFlow :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->- ScanState.ScanStateDesc -> ([] a1) -> (Data.IntMap.IntMap- LiveSets.BlockLiveSets) -> Data.IntMap.IntMap BlockMoves+ ScanState.ScanStateDesc -> ([] a1) -> (IntMap.IntMap+ LiveSets.BlockLiveSets) -> IntMap.IntMap BlockMoves resolveDataFlow maxReg binfo sd blocks liveSets = Lib.forFold IntMap.emptyIntMap blocks (\mappings b -> let {bid = Blocks.blockId binfo b} in- case Data.IntMap.lookup bid liveSets of {+ case IntMap.coq_IntMap_lookup bid liveSets of { Prelude.Just from -> let {successors = Blocks.blockSuccessors binfo b} in let {@@ -122,7 +122,7 @@ 0)} in Lib.forFold mappings successors (\ms s_bid ->- case Data.IntMap.lookup s_bid liveSets of {+ case IntMap.coq_IntMap_lookup s_bid liveSets of { Prelude.Just to -> let { key = case in_from of {
LinearScan/Seq.hs view
@@ -13,6 +13,7 @@ import qualified Data.Functor.Identity import qualified LinearScan.Utils +import qualified LinearScan.Datatypes as Datatypes import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrfun as Ssrfun@@ -30,6 +31,9 @@ unsafeCoerce = IOExts.unsafeCoerce #endif +__ :: any+__ = Prelude.error "Logical or arity value used"+ nilp :: ([] a1) -> Prelude.Bool nilp s = Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Data.List.length s))@@ -93,6 +97,59 @@ rev s = catrev s [] +eqseq :: Eqtype.Equality__Coq_type -> ([] Eqtype.Equality__Coq_sort) -> ([]+ Eqtype.Equality__Coq_sort) -> Prelude.Bool+eqseq t s1 s2 =+ case s1 of {+ [] ->+ case s2 of {+ [] -> Prelude.True;+ (:) s l -> Prelude.False};+ (:) x1 s1' ->+ case s2 of {+ [] -> Prelude.False;+ (:) x2 s2' -> (Prelude.&&) (Eqtype.eq_op t x1 x2) (eqseq t s1' s2')}}++eqseqP :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_axiom+ ([] Eqtype.Equality__Coq_sort)+eqseqP t _top_assumption_ =+ let {+ _evar_0_ = \_top_assumption_0 ->+ let {_evar_0_ = Ssrbool.ReflectT} in+ let {_evar_0_0 = \x2 s2 -> Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ [] -> _evar_0_;+ (:) x x0 -> _evar_0_0 x x0}}+ in+ let {+ _evar_0_0 = \x1 s1 iHs _top_assumption_0 ->+ let {_evar_0_0 = Ssrbool.ReflectF} in+ let {+ _evar_0_1 = \x2 s2 ->+ let {+ _evar_0_1 = \_ ->+ let {_evar_0_1 = Ssrbool.iffP (eqseq t s1 s2) (iHs s2)} in _evar_0_1}+ in+ let {_evar_0_2 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP t x1 x2 of {+ Ssrbool.ReflectT -> _evar_0_1 __;+ Ssrbool.ReflectF -> _evar_0_2 __}}+ in+ case _top_assumption_0 of {+ [] -> _evar_0_0;+ (:) x x0 -> _evar_0_1 x x0}}+ in+ Datatypes.list_rect _evar_0_ _evar_0_0 _top_assumption_++seq_eqMixin :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_mixin_of+ ([] Eqtype.Equality__Coq_sort)+seq_eqMixin t =+ Eqtype.Equality__Mixin (eqseq t) (eqseqP t)++seq_eqType :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type+seq_eqType t =+ unsafeCoerce (seq_eqMixin t)+ mem_seq :: Eqtype.Equality__Coq_type -> ([] Eqtype.Equality__Coq_sort) -> Eqtype.Equality__Coq_sort -> Prelude.Bool mem_seq t s =@@ -112,6 +169,16 @@ Eqtype.Equality__Coq_sort seq_predType t = Ssrbool.mkPredType (unsafeCoerce (pred_of_eq_seq t))++undup :: Eqtype.Equality__Coq_type -> ([] Eqtype.Equality__Coq_sort) -> []+ Eqtype.Equality__Coq_sort+undup t s =+ case s of {+ [] -> [];+ (:) x s' ->+ case Ssrbool.in_mem x (Ssrbool.mem (seq_predType t) (unsafeCoerce s')) of {+ Prelude.True -> undup t s';+ Prelude.False -> (:) x (undup t s')}} rem :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> ([] Eqtype.Equality__Coq_sort) -> [] Eqtype.Equality__Coq_sort
LinearScan/Split.hs view
@@ -92,6 +92,13 @@ let { _evar_0_0 = \_ -> let {+ set_int_desc = ScanState.Build_ScanStateDesc+ _nextInterval_+ (LinearScan.Utils.set_nth _nextInterval_ ints+ uid1 _top_assumption_3) _fixedIntervals_ ((:)+ ((,) u beg) us) _active_ _inactive_ _handled_}+ in+ let { _evar_0_0 = \_ -> (Prelude.flip (Prelude.$)) __ (let {@@ -114,18 +121,177 @@ (ScanState.packScanState maxReg ScanState.InUse new_unhandled)))} in- _evar_0_0 __}+ let {+ _evar_0_1 = \_ ->+ let {+ _evar_0_1 = \_top_assumption_6 ->+ let {+ _evar_0_1 = \_ ->+ let {+ _evar_0_1 = \iv1 ib1 ie1 _iknd1_ rds1 ->+ let {+ _top_assumption_7 = Interval.intervalSpan+ rds1+ _top_assumption_6+ iv1 ib1 ie1 _iknd1_}+ in+ let {+ _evar_0_1 = \_top_assumption_8 ->+ let {+ _evar_0_1 = \_top_assumption_9 _top_assumption_10 ->+ let {+ _evar_0_1 = \_top_assumption_11 ->+ (Prelude.flip (Prelude.$)) __+ (let {+ new_unhandled = ScanState.Build_ScanStateDesc+ ((Prelude.succ) _nextInterval_)+ (LinearScan.Utils.snoc+ _nextInterval_+ (LinearScan.Utils.set_nth+ _nextInterval_ ints uid1+ _top_assumption_3)+ _top_assumption_11)+ _fixedIntervals_+ (Lib.insert+ (Lib.lebf Prelude.snd) ((,)+ ( _nextInterval_)+ (Interval.ibeg+ _top_assumption_11)) ((:)+ (Prelude.id ((,) u beg))+ (Prelude.map Prelude.id us)))+ (Prelude.map Prelude.id+ _active_)+ (Prelude.map Prelude.id+ _inactive_)+ (Prelude.map Prelude.id+ _handled_)}+ in+ let {+ _evar_0_1 = \_ _ -> Prelude.Right+ (Prelude.Just+ (ScanState.packScanState maxReg+ ScanState.InUse new_unhandled))}+ in+ let {+ _evar_0_2 = \_ _ -> Prelude.Left+ (Morph.ECannotSplitSingleton3+ ( uid1))}+ in+ case (Prelude.<=) ((Prelude.succ)+ beg)+ (Interval.ibeg+ _top_assumption_11) of {+ Prelude.True -> _evar_0_1 __;+ Prelude.False -> _evar_0_2 __})}+ in+ let {+ _evar_0_2 = \_ -> Prelude.Right+ (Prelude.Just+ (ScanState.packScanState maxReg+ ScanState.InUse set_int_desc))}+ in+ case _top_assumption_10 of {+ Prelude.Just x -> (\_ -> _evar_0_1 x);+ Prelude.Nothing -> _evar_0_2}}+ in+ let {+ _evar_0_2 = \_top_assumption_9 ->+ let {+ _evar_0_2 = \_top_assumption_10 ->+ (Prelude.flip (Prelude.$)) __+ (let {+ new_unhandled = ScanState.Build_ScanStateDesc+ ((Prelude.succ) _nextInterval_)+ (LinearScan.Utils.snoc+ _nextInterval_+ (LinearScan.Utils.set_nth+ _nextInterval_ ints uid1+ _top_assumption_3)+ _top_assumption_10)+ _fixedIntervals_+ (Lib.insert+ (Lib.lebf Prelude.snd) ((,)+ ( _nextInterval_)+ (Interval.ibeg+ _top_assumption_10)) ((:)+ (Prelude.id ((,) u beg))+ (Prelude.map Prelude.id us)))+ (Prelude.map Prelude.id+ _active_)+ (Prelude.map Prelude.id+ _inactive_)+ (Prelude.map Prelude.id+ _handled_)}+ in+ let {+ _evar_0_2 = \_ _ -> Prelude.Right+ (Prelude.Just+ (ScanState.packScanState maxReg+ ScanState.InUse new_unhandled))}+ in+ let {+ _evar_0_3 = \_ _ -> Prelude.Left+ (Morph.ECannotSplitSingleton3+ ( uid1))}+ in+ case (Prelude.<=) ((Prelude.succ)+ beg)+ (Interval.ibeg+ _top_assumption_10) of {+ Prelude.True -> _evar_0_2 __;+ Prelude.False -> _evar_0_3 __})}+ in+ let {+ _evar_0_3 = \_ ->+ Logic.coq_False_rect}+ in+ case _top_assumption_9 of {+ Prelude.Just x -> (\_ -> _evar_0_2 x);+ Prelude.Nothing -> _evar_0_3}}+ in+ case _top_assumption_8 of {+ Prelude.Just x -> _evar_0_1 x;+ Prelude.Nothing -> _evar_0_2}}+ in+ case _top_assumption_7 of {+ (,) x x0 -> _evar_0_1 x x0 __}}+ in+ case _top_assumption_5 of {+ Interval.Build_IntervalDesc x x0 x1 x2 x3 ->+ _evar_0_1 x x0 x1 x2 x3}}+ in+ let {+ _evar_0_2 = \_ -> Prelude.Left+ (Morph.ECannotSplitSingleton2 ( uid1))}+ in+ case (Prelude.&&)+ ((Prelude.<=) ((Prelude.succ)+ (Interval.ibeg _top_assumption_5))+ _top_assumption_6)+ ((Prelude.<=) ((Prelude.succ)+ _top_assumption_6)+ (Interval.iend _top_assumption_5)) of {+ Prelude.True -> _evar_0_1 __;+ Prelude.False -> _evar_0_2 __}}+ in+ let {+ _evar_0_2 = Prelude.Right (Prelude.Just+ (ScanState.packScanState maxReg ScanState.InUse+ set_int_desc))}+ in+ case splitPosition _top_assumption_5+ BeforeFirstUsePosReqReg of {+ Prelude.Just x -> _evar_0_1 x;+ Prelude.Nothing -> _evar_0_2}}+ in+ case (Prelude.<=) ((Prelude.succ) beg)+ (Interval.ibeg _top_assumption_5) of {+ Prelude.True -> _evar_0_0 __;+ Prelude.False -> _evar_0_1 __}} in _evar_0_0 __} in- let {- _evar_0_1 = \_ -> Prelude.Left- (Morph.ECannotSplitSingleton3 ( uid1))}- in- case (Prelude.<=) ((Prelude.succ) beg)- (Interval.ibeg _top_assumption_5) of {- Prelude.True -> _evar_0_0 __;- Prelude.False -> _evar_0_1 __}}+ _evar_0_0 __} in let { _evar_0_1 = \_ ->
LinearScan/Utils.hs view
@@ -1,10 +1,11 @@ module LinearScan.Utils where import Data.Char-import Data.List+import Data.List as L+import Data.IntMap as M import Debug.Trace -trace = Debug.Trace.trace . map chr+trace = Debug.Trace.trace . L.map chr boundedTransport' pos n _top_assumption_ = _top_assumption_ @@ -12,9 +13,9 @@ set_nth _ xs n x = take n xs ++ x : drop (n+1) xs -vmap _ = Data.List.map+vmap _ = L.map -vfoldl' _ = Data.List.foldl'+vfoldl' _ = L.foldl' vfoldl'_with_index _ f = go 0 where@@ -34,3 +35,15 @@ uncons :: [a] -> Maybe (a, [a]) uncons [] = Nothing uncons (x:xs) = Just (x, xs)++intMap_mergeWithKey'+ :: (Int -> a -> b -> Maybe c)+ -> ([(Int, a)] -> [(Int, c)])+ -> ([(Int, b)] -> [(Int, c)])+ -> ([(Int, a)]) -> ([(Int, b)])+ -> [(Int, c)]+intMap_mergeWithKey' combine only1 only2 m1 m2 =+ M.toList $ M.mergeWithKey combine+ (M.fromList . only1 . M.toList)+ (M.fromList . only2 . M.toList)+ (M.fromList m1) (M.fromList m2)
linearscan.cabal view
@@ -1,5 +1,5 @@ name: linearscan-version: 0.3.0.1+version: 0.3.1.0 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3
test/Main.hs view
@@ -330,12 +330,14 @@ (jump "B4") label "B3" (do add r1 r2 r3- save r3 0+ save r3 16+ save r2 8+ save r1 0 add r0 r0 r1 add r0 r0 r2 add r0 r1 r3 add r0 r2 r3- restore 0 r3)+ restore 16 r3) (jump "B4") label "B4" (add r3 r3 r0)@@ -378,3 +380,66 @@ label "B4" (add r1 r1 r0) return_)++ it "Another resolution case" $ asmTest 4+ (do label "entry" -- 1+ (do lc v3 -- 3+ lc v4 -- 5+ lc v15 -- 7+ lc v20) -- 9+ (jump "L3") -- 11+ label "L3" -- 13+ (do move v3 v9 -- 15+ move v9 v11 -- 17+ move v11 v10 -- 19+ move v10 v12 -- 21+ move v12 v13 -- 23+ lc v14 -- 25+ move v15 v5) -- 27+ (jump "L6") -- 29+ label_ "L6" -- 31+ (branch Zero v4 "L3" "L2") -- 33+ label "L2" -- 35+ (do lc v21 -- 37+ move v21 v18 -- 39+ move v5 v4 -- 41+ lc v19 -- 43+ move v20 v17) -- 45+ (jump "L6")) -- 47++ (do label "entry" -- 1+ (do lc r0 -- 3+ lc r1 -- 5+ lc r2 -- 7+ lc r3 -- 9+ save r3 0)+ (jump "L3") -- 11+ label "L3" -- 13+ (do restore 8 r0+ move r0 r3 -- 15+ save r0 8+ move r3 r0 -- 17+ move r0 r3 -- 19+ move r3 r0 -- 21+ move r0 r3 -- 23+ lc r0 -- 25+ save r0 16+ move r2 r0+ save r2 24) -- 27+ (jump "L6") -- 29+ label_ "L6" -- 31+ (branch Zero r1 "L3" "L2") -- 33+ label "L2" -- 35+ (do lc r3 -- 37+ move r3 r2 -- 39+ move r0 r1 -- 41+ save r1 40+ save r0 32+ lc r3 -- 43+ restore 0 r1+ move r1 r0+ restore 40 r1+ restore 32 r0+ restore 24 r2+ save r1 0) -- 45+ (jump "L6"))
test/Tempest.hs view
@@ -365,6 +365,8 @@ getReferences (Node (Label _) _) = mempty getReferences (Node (Instr i) _) = go i getReferences (Node (Jump _) _) = mempty+ getReferences (Node (Move src dst) _) = mkv Input src <> mkv Output dst+ getReferences (Node (LoadConst _ v) _) = mkv Output v getReferences (Node (Branch _ v _ _) _) = mkv Input v getReferences (Node (ReturnInstr _ i) _) = go i getReferences n = error $ "getReferences: unhandled node: " ++ show n@@ -375,9 +377,9 @@ fromMaybe (error $ "Allocation failed for variable " ++ show n) (Data.List.lookup n m) -mkSaveOp r vid = do+getStackSlot vid = do stack <- get- off' <- case M.lookup vid (stackSlots stack) of+ case M.lookup vid (stackSlots stack) of Just off -> return off Nothing -> do let off = stackPtr stack@@ -387,13 +389,15 @@ M.insert vid off (stackSlots stack) } return off- let sv = Save (Linearity False) r off'++mkSaveOp r vid = do+ off <- getStackSlot vid+ let sv = Save (Linearity False) r off return [NodeOO (Node sv (error "no save meta"))] mkRestoreOp vid r = do- stack <- get- let off = fromMaybe (-1) (M.lookup vid (stackSlots stack))- rs = Restore (Linearity False) off r+ off <- getStackSlot vid+ let rs = Restore (Linearity False) off r return [NodeOO (Node rs (error "no restore meta"))] var :: Int -> IRVar@@ -515,6 +519,11 @@ lbl <- lift $ getLabel str liftF (FreeLabel lbl body close, ()) +label_ :: Engine m => String -> m (Node () v O C) -> Program v m ()+label_ str close = do+ lbl <- lift $ getLabel str+ liftF (FreeLabel lbl (Pure ()) close, ())+ compile :: (Engine m, m ~ StateT Labels SimpleUniqueMonad, NonLocal (Node () v)) => Program v m () -> (Graph (Node () v) C C, Hoopl.Label) compile prog = runSimpleUniqueMonad $@@ -541,6 +550,9 @@ move :: v -> v -> BodyF v move x0 x1 = Free (Node (Move x0 x1) (), Pure ())++lc :: v -> BodyF v+lc x0 = Free (Node (LoadConst Constant x0) (), Pure ()) return_ :: Monad m => m (Node () v O C) return_ = return $ Node (ReturnInstr [] Nop) ()