{-# 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.Graph as Graph 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.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.Transfer p v p0 -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.Spill sreg svid -> k (Blocks.saveOp maxReg mDict oinfo sreg svid); Resolve.Restore dvid dreg -> 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.Looped r -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing})) varAllocs :: Prelude.Int -> Prelude.Int -> ([] Allocate.Allocation) -> UsePos.VarKind -> Eqtype.Equality__Coq_sort -> [] ((,) Blocks.VarId PhysReg) varAllocs maxReg opid allocs kind vid = Prelude.map (\x -> (,) (unsafeCoerce vid) 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) ((Prelude.&&) ((Prelude.<=) (Interval.ibeg int) opid) (case kind of { UsePos.Input -> (Prelude.<=) opid (Interval.iend int); _ -> (Prelude.<=) ((Prelude.succ) opid) (Interval.iend int)}))) allocs))) varInfoAllocs :: Prelude.Int -> Prelude.Int -> ([] Allocate.Allocation) -> Blocks.VarInfo -> [] ((,) Blocks.VarId PhysReg) varInfoAllocs maxReg opid allocs v = case Blocks.varId maxReg v of { Prelude.Left p -> []; Prelude.Right vid -> varAllocs maxReg opid allocs (Blocks.varKind maxReg v) (unsafeCoerce vid)} 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) -> a1 -> Verified a3 ([] a2) setAllocations maxReg mDict oinfo useVerifier allocs 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 Monad.bind (State0.coq_StateT_Monad mDict) (\ops -> Monad.bind (State0.coq_StateT_Monad mDict) (\transitions -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Applicative.pure (State0.coq_StateT_Applicative mDict) ((Prelude.++) ops transitions)) (Lens.plusStateT (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y)) ((Prelude.succ) ((Prelude.succ) 0)) mDict)) (case (Prelude.&&) ((Prelude.<=) (assnBlockBeg assn) opid) ((Prelude.<=) ((Prelude.succ) opid) (assnBlockEnd assn)) of { Prelude.True -> let { moves = Resolve.determineMoves maxReg (Resolve.resolvingMoves maxReg allocs Prelude.Nothing opid ((Prelude.succ) ((Prelude.succ) opid)))} in 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 opid useVerifier moves); Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) []})) (Verify.verifyApplyAllocs maxReg mDict oinfo opid useVerifier op regs)) (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 -> Monad.bind (State0.coq_StateT_Monad mDict) (\bid -> case IntMap.coq_IntMap_lookup bid liveSets of { Prelude.Just bls -> let {liveIns = LiveSets.blockLiveIn bls} in let {liveOuts = LiveSets.blockLiveOut bls} in Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> let { eg = Graph.emptyGraph (Resolve.coq_ResGraphNode_eqType maxReg) (Resolve.coq_ResGraphEdge_eqType maxReg) (unsafeCoerce (Resolve.determineEdge maxReg))} in case case IntMap.coq_IntMap_lookup bid mappings of { Prelude.Just graphs -> graphs; Prelude.Nothing -> (,) eg eg} of { (,) gbeg gend -> let { k = setAllocations maxReg mDict oinfo useVerifier allocs} in Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' -> let {begMoves = Resolve.sortMoves maxReg gbeg} in Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\begMoves' -> Monad.bind (State0.coq_StateT_Monad mDict) (\bmoves -> Monad.bind (State0.coq_StateT_Monad mDict) (\opsm' -> let { endMoves = Resolve.sortMoves maxReg gend} in Monad.bind (State0.coq_StateT_Monad mDict) (\opid1 -> Monad.bind (State0.coq_StateT_Monad mDict) (\endMoves' -> Monad.bind (State0.coq_StateT_Monad mDict) (\emoves -> Monad.bind (State0.coq_StateT_Monad mDict) (\opse' -> Monad.bind (State0.coq_StateT_Monad mDict) (\x2 -> case opsb' of { [] -> let { opsm'' = (Prelude.++) bmoves ((Prelude.++) opsm' emoves)} 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 ((Prelude.++) opsm' emoves)} 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 opid1 useVerifier bid liveOuts)) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) k opse)) (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict (State0.coq_StateT_Monad mDict) (generateMoves maxReg mDict oinfo endMoves'))) (Verify.verifyResolutions maxReg mDict (Prelude.pred (Prelude.pred opid1)) useVerifier endMoves)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict)) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) k opsm)) (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict (State0.coq_StateT_Monad mDict) (generateMoves maxReg mDict oinfo begMoves'))) (Verify.verifyResolutions maxReg mDict (Prelude.pred (Prelude.pred opid0)) useVerifier begMoves)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict)) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) k opsb)}) (Verify.verifyBlockBegin maxReg mDict opid useVerifier bid liveIns loops); Prelude.Nothing -> Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> let { eg = Graph.emptyGraph (Resolve.coq_ResGraphNode_eqType maxReg) (Resolve.coq_ResGraphEdge_eqType maxReg) (unsafeCoerce (Resolve.determineEdge maxReg))} in case case IntMap.coq_IntMap_lookup bid mappings of { Prelude.Just graphs -> graphs; Prelude.Nothing -> (,) eg eg} of { (,) gbeg gend -> let { k = setAllocations maxReg mDict oinfo useVerifier allocs} in Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' -> let {begMoves = Resolve.sortMoves maxReg gbeg} in Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\begMoves' -> Monad.bind (State0.coq_StateT_Monad mDict) (\bmoves -> Monad.bind (State0.coq_StateT_Monad mDict) (\opsm' -> let { endMoves = Resolve.sortMoves maxReg gend} in Monad.bind (State0.coq_StateT_Monad mDict) (\opid1 -> Monad.bind (State0.coq_StateT_Monad mDict) (\endMoves' -> Monad.bind (State0.coq_StateT_Monad mDict) (\emoves -> Monad.bind (State0.coq_StateT_Monad mDict) (\opse' -> Monad.bind (State0.coq_StateT_Monad mDict) (\x2 -> case opsb' of { [] -> let { opsm'' = (Prelude.++) bmoves ((Prelude.++) opsm' emoves)} 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 ((Prelude.++) opsm' emoves)} 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 opid1 useVerifier bid IntSet.emptyIntSet)) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) k opse)) (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict (State0.coq_StateT_Monad mDict) (generateMoves maxReg mDict oinfo endMoves'))) (Verify.verifyResolutions maxReg mDict (Prelude.pred (Prelude.pred opid1)) useVerifier endMoves)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict)) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) k opsm)) (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict (State0.coq_StateT_Monad mDict) (generateMoves maxReg mDict oinfo begMoves'))) (Verify.verifyResolutions maxReg mDict (Prelude.pred (Prelude.pred opid0)) useVerifier begMoves)) (Lens.use (Lens.stepdownl' (\_ y -> (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict)) (Monad.concatMapM (State0.coq_StateT_Applicative mDict) k opsb)}) (Verify.verifyBlockBegin maxReg mDict opid useVerifier bid IntSet.emptyIntSet loops)}) (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict (State0.coq_StateT_Monad mDict) (Blocks.blockId mDict binfo blk))) (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 (Verify.verErrors maxReg st)}))}) (considerOps maxReg mDict binfo oinfo useVerifier allocs liveSets mappings loops blocks (Verify.newVerifiedSig maxReg newAssnStateDesc))