diff --git a/LinearScan/Assign.hs b/LinearScan/Assign.hs --- a/LinearScan/Assign.hs +++ b/LinearScan/Assign.hs @@ -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)} diff --git a/LinearScan/Build.hs b/LinearScan/Build.hs --- a/LinearScan/Build.hs +++ b/LinearScan/Build.hs @@ -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))}} diff --git a/LinearScan/IntMap.hs b/LinearScan/IntMap.hs --- a/LinearScan/IntMap.hs +++ b/LinearScan/IntMap.hs @@ -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) diff --git a/LinearScan/Lib.hs b/LinearScan/Lib.hs --- a/LinearScan/Lib.hs +++ b/LinearScan/Lib.hs @@ -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 = diff --git a/LinearScan/LiveSets.hs b/LinearScan/LiveSets.hs --- a/LinearScan/LiveSets.hs +++ b/LinearScan/LiveSets.hs @@ -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 diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs --- a/LinearScan/Main.hs +++ b/LinearScan/Main.hs @@ -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)}} diff --git a/LinearScan/Range.hs b/LinearScan/Range.hs --- a/LinearScan/Range.hs +++ b/LinearScan/Range.hs @@ -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 diff --git a/LinearScan/Resolve.hs b/LinearScan/Resolve.hs --- a/LinearScan/Resolve.hs +++ b/LinearScan/Resolve.hs @@ -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 { diff --git a/LinearScan/Seq.hs b/LinearScan/Seq.hs --- a/LinearScan/Seq.hs +++ b/LinearScan/Seq.hs @@ -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 diff --git a/LinearScan/Split.hs b/LinearScan/Split.hs --- a/LinearScan/Split.hs +++ b/LinearScan/Split.hs @@ -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 = \_ -> diff --git a/LinearScan/Utils.hs b/LinearScan/Utils.hs --- a/LinearScan/Utils.hs +++ b/LinearScan/Utils.hs @@ -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) diff --git a/linearscan.cabal b/linearscan.cabal --- a/linearscan.cabal +++ b/linearscan.cabal @@ -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 diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -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")) diff --git a/test/Tempest.hs b/test/Tempest.hs --- a/test/Tempest.hs +++ b/test/Tempest.hs @@ -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) ()