{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} module LinearScan.Assign where import Debug.Trace (trace, traceShow, traceShowId) 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 Hask.Utils import qualified LinearScan.Allocate as Allocate import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Class as Class import qualified LinearScan.Functor as Functor import qualified LinearScan.IntMap as IntMap import qualified LinearScan.IntSet as IntSet import qualified LinearScan.Interval as Interval import qualified LinearScan.Lens as Lens import qualified LinearScan.List1 as List1 import qualified LinearScan.LiveSets as LiveSets import qualified LinearScan.Loops as Loops import qualified LinearScan.Maybe as Maybe import qualified LinearScan.Monad as Monad import qualified LinearScan.Resolve as Resolve import qualified LinearScan.State0 as State0 import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Verify as Verify import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Seq as Seq import qualified LinearScan.Ssrnat as Ssrnat #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base import qualified GHC.Prim as GHC.Prim #else -- HUGS import qualified LinearScan.IOExts as IOExts #endif #ifdef __GLASGOW_HASKELL__ --unsafeCoerce :: a -> b unsafeCoerce = GHC.Base.unsafeCoerce# #else -- HUGS --unsafeCoerce :: a -> b unsafeCoerce = IOExts.unsafeCoerce #endif type PhysReg = Prelude.Int data AssnStateDesc = Build_AssnStateDesc Blocks.OpId Blocks.OpId Blocks.OpId assnOpId :: AssnStateDesc -> Blocks.OpId assnOpId a = case a of { Build_AssnStateDesc assnOpId0 assnBlockBeg0 assnBlockEnd0 -> assnOpId0} assnBlockBeg :: AssnStateDesc -> Blocks.OpId assnBlockBeg a = case a of { Build_AssnStateDesc assnOpId0 assnBlockBeg0 assnBlockEnd0 -> assnBlockBeg0} assnBlockEnd :: AssnStateDesc -> Blocks.OpId assnBlockEnd a = case a of { Build_AssnStateDesc assnOpId0 assnBlockBeg0 assnBlockEnd0 -> assnBlockEnd0} newAssnStateDesc :: AssnStateDesc newAssnStateDesc = Build_AssnStateDesc ((Prelude.succ) 0) ((Prelude.succ) 0) ((Prelude.succ) 0) _assnOpId :: (Functor.Functor a1) -> (Blocks.OpId -> a1) -> AssnStateDesc -> a1 _assnOpId h f s = Functor.fmap h (\x -> Build_AssnStateDesc x (assnBlockBeg s) (assnBlockEnd s)) (f (assnOpId s)) _assnBlockBeg :: (Functor.Functor a1) -> (Blocks.OpId -> a1) -> AssnStateDesc -> a1 _assnBlockBeg h f s = Functor.fmap h (\x -> Build_AssnStateDesc (assnOpId s) x (assnBlockEnd s)) (f (assnBlockBeg s)) _assnBlockEnd :: (Functor.Functor a1) -> (Blocks.OpId -> a1) -> AssnStateDesc -> a1 _assnBlockEnd h f s = Functor.fmap h (\x -> Build_AssnStateDesc (assnOpId s) (assnBlockBeg s) x) (f (assnBlockEnd s)) generateMoves :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 a1 a2) -> ([] Resolve.ResolvingMove) -> a3 generateMoves maxReg mDict oinfo moves = Monad.forFoldM mDict [] moves (\acc mv -> let { k = Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict)) (\x -> Prelude.Just x)} in Monad.bind mDict (\mops -> Applicative.pure (Monad.is_applicative mDict) (case mops of { Prelude.Just ops -> (Prelude.++) acc ops; Prelude.Nothing -> acc})) (case mv of { Resolve.Move sreg svid dreg -> k (Blocks.moveOp maxReg mDict oinfo sreg svid dreg); Resolve.Spill sreg svid b -> k (Blocks.saveOp maxReg mDict oinfo sreg svid); Resolve.Restore dvid dreg b -> k (Blocks.restoreOp maxReg mDict oinfo dvid dreg); Resolve.AllocReg v p -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.FreeReg p v -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.AssignReg v p -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.ClearReg p v -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.AllocStack v -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.FreeStack v -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.Looped r -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing})) varAllocs :: Prelude.Int -> Prelude.Int -> ([] Allocate.Allocation) -> Eqtype.Equality__Coq_sort -> Blocks.VarInfo -> [] ((,) ((,) Blocks.VarId UsePos.VarKind) PhysReg) varAllocs maxReg pos allocs vid v = Prelude.map (\x -> (,) ((,) (unsafeCoerce vid) (Blocks.varKind maxReg v)) x) (List1.catMaybes (Prelude.map (\i -> Allocate.intReg maxReg i) (Prelude.filter (\i -> let {int = Allocate.intVal maxReg i} in (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Interval.ivar int)) vid) (case Blocks.varKind maxReg v of { UsePos.Input -> (Prelude.&&) ((Prelude.<=) ((Prelude.succ) pos) (Interval.iend int)) ((Prelude.<=) ((Prelude.succ) (Interval.ibeg int)) ((Prelude.succ) pos)); _ -> (Prelude.&&) ((Prelude.<=) ((Prelude.succ) ((Prelude.succ) pos)) (Interval.iend int)) ((Prelude.<=) ((Prelude.succ) (Interval.ibeg int)) ((Prelude.succ) ((Prelude.succ) pos)))})) allocs))) varInfoAllocs :: Prelude.Int -> Prelude.Int -> ([] Allocate.Allocation) -> Blocks.VarInfo -> [] ((,) ((,) Blocks.VarId UsePos.VarKind) PhysReg) varInfoAllocs maxReg pos allocs v = case Blocks.varId maxReg v of { Prelude.Left p -> []; Prelude.Right vid -> varAllocs maxReg pos allocs (unsafeCoerce vid) v} type Verified mType a = Verify.Verified mType AssnStateDesc a _verExt :: Prelude.Int -> (Functor.Functor a1) -> (AssnStateDesc -> a1) -> (Verify.VerifiedSig AssnStateDesc) -> a1 _verExt maxReg h x x0 = Verify._verExt maxReg h x x0 setAllocations :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 a1 a2) -> Verify.UseVerifier -> ([] Allocate.Allocation) -> (Verified a3 ([] a2)) -> a1 -> Verified a3 ([] a2) setAllocations maxReg mDict oinfo useVerifier allocs injector op = Monad.bind (State0.coq_StateT_Monad mDict) (\assn -> let {opid = assnOpId assn} in let {vars = Blocks.opRefs maxReg mDict oinfo op} in let { regs = List1.concat (Prelude.map (varInfoAllocs maxReg opid allocs) vars)} in let { transitions = \b e -> case (Prelude.&&) ((Prelude.<=) (assnBlockBeg assn) b) ((Prelude.<=) ((Prelude.succ) b) (assnBlockEnd assn)) of { Prelude.True -> let { moves = Resolve.determineMoves maxReg allocs Prelude.Nothing b e} in Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\moves' -> Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict (State0.coq_StateT_Monad mDict) (generateMoves maxReg mDict oinfo moves')) (Verify.verifyResolutions maxReg mDict e useVerifier moves)) (Verify.verifyTransitions maxReg mDict e allocs useVerifier moves b e); Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) []}} in Monad.bind (State0.coq_StateT_Monad mDict) (\inputTransitions -> Monad.bind (State0.coq_StateT_Monad mDict) (\outputTransitions -> Monad.bind (State0.coq_StateT_Monad mDict) (\injected -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\ops -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> Applicative.pure (State0.coq_StateT_Applicative mDict) ((Prelude.++) inputTransitions ((Prelude.++) outputTransitions ((Prelude.++) injected ops)))) (Lens.plusStateT (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y)) ((Prelude.succ) ((Prelude.succ) 0)) mDict)) (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict (State0.coq_StateT_Monad mDict) (Blocks.applyAllocs maxReg mDict oinfo op regs))) (Verify.verifyAllocs maxReg mDict oinfo ((Prelude.succ) ((Prelude.succ) opid)) allocs useVerifier op regs)) injector) (transitions opid ((Prelude.succ) opid))) (transitions (Prelude.pred opid) opid)) (Lens.use (Lens.stepdownl' (\_ -> _verExt maxReg)) mDict) considerOps :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> Verify.UseVerifier -> ([] Allocate.Allocation) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> (IntMap.IntMap Resolve.BlockMoves) -> Loops.LoopState -> ([] a1) -> Verified a5 ([] a2) considerOps maxReg mDict binfo oinfo useVerifier allocs liveSets mappings loops = Monad.mapM (State0.coq_StateT_Applicative mDict) (\blk -> case Blocks.blockOps mDict binfo blk of { (,) p opse -> case p of { (,) opsb opsm -> Monad.bind (State0.coq_StateT_Monad mDict) (\opid -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> let {bid = Blocks.blockId mDict binfo blk} in let {suxs = Blocks.blockSuccessors mDict binfo blk} in case IntMap.coq_IntMap_lookup bid liveSets of { Prelude.Just bls -> let {liveIns = LiveSets.blockLiveIn bls} in let {liveOuts = LiveSets.blockLiveOut bls} in case let { fwds = Maybe.maybe [] IntSet.coq_IntSet_toList (IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops))} in let { bwds = Maybe.maybe [] IntSet.coq_IntSet_toList (IntMap.coq_IntMap_lookup bid (Loops.backwardBranches loops))} in (,) (List1.concat (Prelude.map (\b -> case IntMap.coq_IntMap_lookup b liveSets of { Prelude.Just x1 -> (:) (LiveSets.blockLastOpId x1) []; Prelude.Nothing -> []}) ((Prelude.++) fwds bwds))) (List1.concat (Prelude.map (\b -> case IntMap.coq_IntMap_lookup b liveSets of { Prelude.Just x1 -> (:) (LiveSets.blockFirstOpId x1) []; Prelude.Nothing -> []}) suxs)) of { (,) froms tos -> case Maybe.fromMaybe ((,) [] []) (IntMap.coq_IntMap_lookup bid mappings) of { (,) begMoves endMoves -> let { k = setAllocations maxReg mDict oinfo useVerifier allocs} in let { resolutions = \pos toFroms moves -> Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> Monad.bind (State0.coq_StateT_Monad mDict) (\moves' -> Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict (State0.coq_StateT_Monad mDict) (generateMoves maxReg mDict oinfo moves')) (Verify.verifyResolutions maxReg mDict pos useVerifier moves)) (case toFroms of { Prelude.Left froms0 -> Monad.forM_ (State0.coq_StateT_Monad mDict) froms0 (\b -> Verify.verifyTransitions maxReg mDict pos allocs useVerifier moves b ((Prelude.succ) pos)); Prelude.Right tos0 -> Monad.forM_ (State0.coq_StateT_Monad mDict) tos0 (\e -> Verify.verifyTransitions maxReg mDict pos allocs useVerifier moves pos e)})} in Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' -> Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\bmoves -> Monad.bind (State0.coq_StateT_Monad mDict) (\opsm' -> Monad.bind (State0.coq_StateT_Monad mDict) (\z -> case z of { (,) opse' opid1 -> Monad.bind (State0.coq_StateT_Monad mDict) (\x2 -> case opsb' of { [] -> let { opsm'' = (Prelude.++) bmoves opsm'} in case opse' of { [] -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Blocks.setBlockOps mDict binfo blk [] opsm'' []); (:) e es -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Blocks.setBlockOps mDict binfo blk [] ((Prelude.++) opsm'' (Seq.belast e es)) ((:) (Seq.last e es) []))}; (:) b bs -> let { opsm'' = (Prelude.++) bmoves opsm'} in case opse' of { [] -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Blocks.setBlockOps mDict binfo blk ((:) b []) ((Prelude.++) bs opsm'') []); (:) e es -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Blocks.setBlockOps mDict binfo blk ((:) b []) ((Prelude.++) bs ((Prelude.++) opsm'' (Seq.belast e es))) ((:) (Seq.last e es) []))}}) (Verify.verifyBlockEnd maxReg mDict useVerifier bid liveOuts)}) (case opse of { [] -> Monad.bind (State0.coq_StateT_Monad mDict) (\opid1 -> Applicative.pure (State0.coq_StateT_Applicative mDict) ((,) [] opid1)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict); (:) e es -> Monad.bind (State0.coq_StateT_Monad mDict) (\xs -> Monad.bind (State0.coq_StateT_Monad mDict) (\opid1 -> Monad.bind (State0.coq_StateT_Monad mDict) (\x2 -> Applicative.pure (State0.coq_StateT_Applicative mDict) ((,) ((Prelude.++) xs x2) opid1)) (k (resolutions opid1 (Prelude.Right tos) endMoves) (Seq.last e es))) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict)) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) (k (Applicative.pure (State0.coq_StateT_Applicative mDict) [])) (Seq.belast e es))})) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) (k (Applicative.pure (State0.coq_StateT_Applicative mDict) [])) opsm)) (resolutions (Prelude.pred opid0) (Prelude.Left froms) begMoves)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict)) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) (k (Applicative.pure (State0.coq_StateT_Applicative mDict) [])) opsb)) (Verify.verifyBlockBegin maxReg mDict opid useVerifier bid liveIns loops)}}; Prelude.Nothing -> case let { fwds = Maybe.maybe [] IntSet.coq_IntSet_toList (IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops))} in let { bwds = Maybe.maybe [] IntSet.coq_IntSet_toList (IntMap.coq_IntMap_lookup bid (Loops.backwardBranches loops))} in (,) (List1.concat (Prelude.map (\b -> case IntMap.coq_IntMap_lookup b liveSets of { Prelude.Just x1 -> (:) (LiveSets.blockLastOpId x1) []; Prelude.Nothing -> []}) ((Prelude.++) fwds bwds))) (List1.concat (Prelude.map (\b -> case IntMap.coq_IntMap_lookup b liveSets of { Prelude.Just x1 -> (:) (LiveSets.blockFirstOpId x1) []; Prelude.Nothing -> []}) suxs)) of { (,) froms tos -> case Maybe.fromMaybe ((,) [] []) (IntMap.coq_IntMap_lookup bid mappings) of { (,) begMoves endMoves -> let { k = setAllocations maxReg mDict oinfo useVerifier allocs} in let { resolutions = \pos toFroms moves -> Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> Monad.bind (State0.coq_StateT_Monad mDict) (\moves' -> Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict (State0.coq_StateT_Monad mDict) (generateMoves maxReg mDict oinfo moves')) (Verify.verifyResolutions maxReg mDict pos useVerifier moves)) (case toFroms of { Prelude.Left froms0 -> Monad.forM_ (State0.coq_StateT_Monad mDict) froms0 (\b -> Verify.verifyTransitions maxReg mDict pos allocs useVerifier moves b ((Prelude.succ) pos)); Prelude.Right tos0 -> Monad.forM_ (State0.coq_StateT_Monad mDict) tos0 (\e -> Verify.verifyTransitions maxReg mDict pos allocs useVerifier moves pos e)})} in Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' -> Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\bmoves -> Monad.bind (State0.coq_StateT_Monad mDict) (\opsm' -> Monad.bind (State0.coq_StateT_Monad mDict) (\z -> case z of { (,) opse' opid1 -> Monad.bind (State0.coq_StateT_Monad mDict) (\x2 -> case opsb' of { [] -> let { opsm'' = (Prelude.++) bmoves opsm'} in case opse' of { [] -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Blocks.setBlockOps mDict binfo blk [] opsm'' []); (:) e es -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Blocks.setBlockOps mDict binfo blk [] ((Prelude.++) opsm'' (Seq.belast e es)) ((:) (Seq.last e es) []))}; (:) b bs -> let { opsm'' = (Prelude.++) bmoves opsm'} in case opse' of { [] -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Blocks.setBlockOps mDict binfo blk ((:) b []) ((Prelude.++) bs opsm'') []); (:) e es -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Blocks.setBlockOps mDict binfo blk ((:) b []) ((Prelude.++) bs ((Prelude.++) opsm'' (Seq.belast e es))) ((:) (Seq.last e es) []))}}) (Verify.verifyBlockEnd maxReg mDict useVerifier bid IntSet.emptyIntSet)}) (case opse of { [] -> Monad.bind (State0.coq_StateT_Monad mDict) (\opid1 -> Applicative.pure (State0.coq_StateT_Applicative mDict) ((,) [] opid1)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict); (:) e es -> Monad.bind (State0.coq_StateT_Monad mDict) (\xs -> Monad.bind (State0.coq_StateT_Monad mDict) (\opid1 -> Monad.bind (State0.coq_StateT_Monad mDict) (\x2 -> Applicative.pure (State0.coq_StateT_Applicative mDict) ((,) ((Prelude.++) xs x2) opid1)) (k (resolutions opid1 (Prelude.Right tos) endMoves) (Seq.last e es))) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict)) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) (k (Applicative.pure (State0.coq_StateT_Applicative mDict) [])) (Seq.belast e es))})) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) (k (Applicative.pure (State0.coq_StateT_Applicative mDict) [])) opsm)) (resolutions (Prelude.pred opid0) (Prelude.Left froms) begMoves)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict)) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) (k (Applicative.pure (State0.coq_StateT_Applicative mDict) [])) opsb)) (Verify.verifyBlockBegin maxReg mDict opid useVerifier bid IntSet.emptyIntSet loops)}}}) (Lens.modifyStateT (\_ y -> (Prelude..) (_verExt maxReg y) (_assnBlockEnd y)) ((Prelude.+) opid (Ssrnat.double ((Prelude.+) (Data.List.length opsb) (Data.List.length opsm)))) mDict)) (Lens.modifyStateT (\_ y -> (Prelude..) (_verExt maxReg y) (_assnBlockBeg y)) ((Prelude.+) opid (Ssrnat.double (Data.List.length opsb))) mDict)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict)}}) assignRegNum :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> Verify.UseVerifier -> ([] Allocate.Allocation) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> (IntMap.IntMap Resolve.BlockMoves) -> Loops.LoopState -> ([] a1) -> a5 assignRegNum maxReg mDict binfo oinfo useVerifier allocs liveSets mappings loops blocks = Monad.bind mDict (\res -> case res of { (,) bs st -> Applicative.pure (Monad.is_applicative mDict) ((,) (Verify.verMoves maxReg st) (case IntMap.coq_IntMap_toList (Verify.verErrors maxReg st) of { [] -> Prelude.Right bs; (:) p l -> Prelude.Left st}))}) (considerOps maxReg mDict binfo oinfo useVerifier allocs liveSets mappings loops blocks (Verify.newVerifiedSig maxReg newAssnStateDesc))