{-# OPTIONS_GHC -cpp -fglasgow-exts #-} {- For Hugs, use the option -F"cpp -P -traditional" -} module LinearScan.Resolve where import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity import qualified LinearScan.Utils 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.Lib as Lib import qualified LinearScan.LiveSets as LiveSets import qualified LinearScan.ScanState as ScanState import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype 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 type PhysReg = Prelude.Int data Allocation = Build_Allocation Prelude.Int Interval.IntervalDesc (Prelude.Maybe PhysReg) intVal :: Prelude.Int -> Allocation -> Interval.IntervalDesc intVal maxReg a = case a of { Build_Allocation intId intVal0 intReg0 -> intVal0} intReg :: Prelude.Int -> Allocation -> Prelude.Maybe PhysReg intReg maxReg a = case a of { Build_Allocation intId intVal0 intReg0 -> intReg0} determineAllocations :: Prelude.Int -> ScanState.ScanStateDesc -> [] Allocation determineAllocations maxReg sd = Prelude.map (\x -> Build_Allocation ( (Prelude.fst x)) (Interval.getIntervalDesc ( (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) (Prelude.fst x)))) (Prelude.snd x)) (ScanState.handled maxReg sd) type RawResolvingMove = (,) (Prelude.Maybe PhysReg) (Prelude.Maybe PhysReg) data ResolvingMove = Move PhysReg PhysReg | Swap PhysReg PhysReg | Spill PhysReg Blocks.VarId | Restore Blocks.VarId PhysReg | Nop prepareForGraph :: Prelude.Int -> Eqtype.Equality__Coq_sort -> RawResolvingMove -> (,) (Prelude.Maybe Eqtype.Equality__Coq_sort) (Prelude.Maybe Eqtype.Equality__Coq_sort) prepareForGraph maxReg vid x = case x of { (,) o o0 -> case o of { Prelude.Just x0 -> case o0 of { Prelude.Just y -> (,) (Prelude.Just (unsafeCoerce (Prelude.Left x0))) (Prelude.Just (unsafeCoerce (Prelude.Left y))); Prelude.Nothing -> (,) (Prelude.Just (unsafeCoerce (Prelude.Left x0))) (Prelude.Just (unsafeCoerce (Prelude.Right vid)))}; Prelude.Nothing -> case o0 of { Prelude.Just y -> (,) (Prelude.Just (unsafeCoerce (Prelude.Right vid))) (Prelude.Just (unsafeCoerce (Prelude.Left y))); Prelude.Nothing -> (,) (Prelude.Just (unsafeCoerce (Prelude.Right vid))) (Prelude.Just (unsafeCoerce (Prelude.Right vid)))}}} moveFromGraph :: Prelude.Int -> ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort) (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> ResolvingMove moveFromGraph maxReg mv = case mv of { (,) o o0 -> case o of { Prelude.Just s -> case unsafeCoerce s of { Prelude.Left x -> case o0 of { Prelude.Just s0 -> case unsafeCoerce s0 of { Prelude.Left y -> Move x y; Prelude.Right y -> Spill x y}; Prelude.Nothing -> Nop}; Prelude.Right x -> case o0 of { Prelude.Just s0 -> case unsafeCoerce s0 of { Prelude.Left y -> Restore x y; Prelude.Right s1 -> Nop}; Prelude.Nothing -> Nop}}; Prelude.Nothing -> Nop}} determineMoves :: Prelude.Int -> (IntMap.IntMap RawResolvingMove) -> [] ResolvingMove determineMoves maxReg moves = let { graph = Lib.forFold (Graph.emptyGraph (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType)) (unsafeCoerce (IntMap.coq_IntMap_toList moves)) (\g mv -> Graph.addEdge (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType) (unsafeCoerce (prepareForGraph maxReg (Prelude.fst mv) (Prelude.snd mv))) g)} in Prelude.map (moveFromGraph maxReg) (Graph.topsort (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType) graph) resolvingMoves :: Prelude.Int -> ([] Allocation) -> Prelude.Int -> Prelude.Int -> IntMap.IntMap RawResolvingMove resolvingMoves maxReg allocs from to = let { liveAtFrom = IntMap.coq_IntMap_fromList (Prelude.map (\i -> (,) (Interval.ivar (intVal maxReg i)) i) (Prelude.filter (\i -> (Prelude.&&) ((Prelude.<=) (Interval.ibeg (intVal maxReg i)) from) ((Prelude.<=) ((Prelude.succ) from) (Interval.iend (intVal maxReg i)))) allocs))} in let { liveAtTo = IntMap.coq_IntMap_fromList (Prelude.map (\i -> (,) (Interval.ivar (intVal maxReg i)) i) (Prelude.filter (\i -> let {int = intVal maxReg i} in (Prelude.&&) ((Prelude.<=) (Interval.ibeg int) to) (case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce to) (unsafeCoerce (Interval.iend int)) of { Prelude.True -> case Interval.lastUsePos int of { Prelude.Just u -> (Prelude.<=) to (UsePos.uloc u); Prelude.Nothing -> Prelude.False}; Prelude.False -> (Prelude.<=) ((Prelude.succ) to) (Interval.iend int)})) allocs))} in IntMap.coq_IntMap_mergeWithKey (\vid x y -> case Eqtype.eq_op (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg)) (unsafeCoerce (intReg maxReg x)) (unsafeCoerce (intReg maxReg y)) of { Prelude.True -> Prelude.Nothing; Prelude.False -> Prelude.Just ((,) (intReg maxReg x) (intReg maxReg y))}) (\x -> IntMap.emptyIntMap) (\x -> IntMap.emptyIntMap) liveAtFrom liveAtTo checkBlockBoundary :: Prelude.Int -> ([] Allocation) -> Prelude.Int -> Prelude.Bool -> LiveSets.BlockLiveSets -> LiveSets.BlockLiveSets -> IntMap.IntSet -> (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) -> IntMap.IntMap ((,) Graph.Graph Graph.Graph) checkBlockBoundary maxReg allocs bid in_from from to liveIn mappings = let { select = \acc vid x -> case IntMap.coq_IntSet_member vid liveIn of { Prelude.True -> (:) ((,) vid x) acc; Prelude.False -> acc}} in let { moves = IntMap.coq_IntMap_foldlWithKey select [] (resolvingMoves maxReg allocs (LiveSets.blockLastOpId from) (LiveSets.blockFirstOpId to))} in Lib.forFold mappings (unsafeCoerce moves) (\ms mv -> let { addToGraphs = \e xs -> case xs of { (,) gbeg gend -> case in_from of { Prelude.True -> (,) gbeg (Graph.addEdge (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType) e gend); Prelude.False -> (,) (Graph.addEdge (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType) e gbeg) gend}}} in let { f = \mxs -> unsafeCoerce addToGraphs (prepareForGraph maxReg (Prelude.fst mv) (Prelude.snd mv)) (case mxs of { Prelude.Just xs -> xs; Prelude.Nothing -> (,) (Graph.emptyGraph (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType)) (Graph.emptyGraph (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType))})} in IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms) type BlockMoves = (,) Graph.Graph Graph.Graph resolveDataFlow :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) -> ([] Allocation) -> ([] a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> IntMap.IntMap BlockMoves resolveDataFlow maxReg binfo allocs blocks liveSets = Lib.forFold IntMap.emptyIntMap blocks (\mappings b -> let {bid = Blocks.blockId binfo b} in case IntMap.coq_IntMap_lookup bid liveSets of { Prelude.Just from -> let {successors = Blocks.blockSuccessors binfo b} in let { in_from = (Prelude.<=) (Data.List.length successors) ((Prelude.succ) 0)} in Lib.forFold mappings successors (\ms s_bid -> case IntMap.coq_IntMap_lookup s_bid liveSets of { Prelude.Just to -> let { key = case in_from of { Prelude.True -> bid; Prelude.False -> s_bid}} in checkBlockBoundary maxReg allocs key in_from from to (LiveSets.blockLiveIn to) ms; Prelude.Nothing -> ms}); Prelude.Nothing -> mappings})