linearscan-0.8.0: LinearScan/Assign.hs
{-# 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))