{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} module LinearScan.Allocate 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.Context as Context import qualified LinearScan.Cursor as Cursor import qualified LinearScan.Interval as Interval import qualified LinearScan.Maybe as Maybe import qualified LinearScan.Morph as Morph import qualified LinearScan.ScanState as ScanState import qualified LinearScan.Specif as Specif import qualified LinearScan.Spill as Spill import qualified LinearScan.Split as Split import qualified LinearScan.Ssr as Ssr import qualified LinearScan.Trace as Trace import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Vector0 as Vector0 import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq import qualified LinearScan.Ssrbool as Ssrbool 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 __ :: any __ = Prelude.error "Logical or arity value used" type PhysReg = Prelude.Int intersectsWithFixedInterval :: Prelude.Int -> ScanState.ScanStateDesc -> PhysReg -> Morph.SState () () (Prelude.Maybe Prelude.Int) intersectsWithFixedInterval maxReg pre reg = Cursor.withCursor maxReg pre (\sd _ -> Context.ipure (case Vector0.vnth maxReg (ScanState.fixedIntervals maxReg sd) reg of { Prelude.Just i -> Interval.intervalIntersectsWithSubrange ( (Cursor.curIntDetails maxReg sd)) ( i); Prelude.Nothing -> Prelude.Nothing})) updateRegisterPos :: Prelude.Int -> (Vector0.Vec (Prelude.Maybe Prelude.Int)) -> PhysReg -> (Prelude.Maybe Prelude.Int) -> Vector0.Vec (Prelude.Maybe Prelude.Int) updateRegisterPos maxReg v r p = case p of { Prelude.Just x -> Vector0.vreplace maxReg v r (Prelude.Just (case Vector0.vnth maxReg v r of { Prelude.Just n -> case (Prelude.<=) ((Prelude.succ) n) x of { Prelude.True -> n; Prelude.False -> x}; Prelude.Nothing -> x})); Prelude.Nothing -> v} findEligibleRegister :: Prelude.Int -> ScanState.ScanStateDesc -> Interval.IntervalDesc -> (Vector0.Vec (Prelude.Maybe Prelude.Int)) -> (,) PhysReg (Prelude.Maybe Prelude.Int) findEligibleRegister maxReg sd d xs = case Vector0.vfoldl_with_index maxReg (\reg acc mint -> case acc of { (,) fup fai -> case mint of { Prelude.Just int -> let { op = Interval.intervalIntersectsWithSubrange (Interval.getIntervalDesc d) (Interval.getIntervalDesc ( int))} in (,) (updateRegisterPos maxReg fup reg op) (Vector0.vreplace maxReg fai reg (Maybe.isJust op)); Prelude.Nothing -> acc}}) ((,) xs (Vector0.vconst maxReg Prelude.False)) (ScanState.fixedIntervals maxReg sd) of { (,) xs0 fixedAndIntersects -> ScanState.registerWithHighestPos maxReg fixedAndIntersects xs0} tryAllocateFreeReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState () () (Prelude.Maybe (Morph.SState () () PhysReg)) tryAllocateFreeReg maxReg pre = Cursor.withCursor maxReg pre (\sd _ -> let { go = \f v p -> case p of { (,) i r -> updateRegisterPos maxReg v r (f i)}} in let { actives = Data.List.foldl' (go (\x -> Prelude.Just 0)) (Vector0.vconst maxReg Prelude.Nothing) (ScanState.active maxReg sd)} in let { freeUntilPos = Data.List.foldl' (go (\i -> Interval.intervalsIntersect (Interval.getIntervalDesc ( (Cursor.curIntDetails maxReg sd))) (Interval.getIntervalDesc ( (Vector0.vnth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) i))))) actives (ScanState.inactive maxReg sd)} in case findEligibleRegister maxReg sd ( (Cursor.curIntDetails maxReg sd)) freeUntilPos of { (,) reg mres -> let { success = Context.ibind (\x -> Context.ipure reg) (Morph.moveUnhandledToActive maxReg pre reg)} in let {cid = Cursor.curId maxReg sd} in Context.context (Trace.ETryAllocateFreeReg (Prelude.id reg) mres (Prelude.id (Prelude.fst cid))) (Context.ipure (case mres of { Prelude.Just n -> case (Prelude.<=) n (Interval.intervalStart ( (Cursor.curIntDetails maxReg sd))) of { Prelude.True -> Prelude.Nothing; Prelude.False -> Prelude.Just (case (Prelude.<=) ((Prelude.succ) (Interval.intervalEnd ( (Cursor.curIntDetails maxReg sd)))) n of { Prelude.True -> success; Prelude.False -> Context.ibind (\x -> success) (Split.splitCurrentInterval maxReg pre (Split.BeforePos n))})}; Prelude.Nothing -> Prelude.Just success}))}) allocateBlockedReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState () () (Prelude.Maybe PhysReg) allocateBlockedReg maxReg pre = Cursor.withCursor maxReg pre (\sd _ -> let {pos = Interval.intervalStart ( (Cursor.curIntDetails maxReg sd))} in let { go = \v p -> case p of { (,) int reg -> let { atPos = \u -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos) (unsafeCoerce (UsePos.uloc u))) (UsePos.regReq u)} in let { pos' = case Interval.findIntervalUsePos ( int) atPos of { Prelude.Just s -> Prelude.Just 0; Prelude.Nothing -> Interval.nextUseAfter ( int) pos}} in updateRegisterPos maxReg v reg pos'}} in let { resolve = \xs -> Prelude.map (\i -> (,) (Interval.packInterval ( (Vector0.vnth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) (Prelude.fst i)))) (Prelude.snd i)) xs} in let { actives = Data.List.foldl' go (Vector0.vconst maxReg Prelude.Nothing) (resolve (ScanState.active maxReg sd))} in let { nextUsePos'' = Data.List.foldl' go actives (Prelude.filter (\x -> Ssrbool.isSome (Interval.intervalsIntersect (Interval.getIntervalDesc ( (Cursor.curIntDetails maxReg sd))) ( (Prelude.fst x)))) (resolve (ScanState.inactive maxReg sd)))} in case findEligibleRegister maxReg sd ( (Cursor.curIntDetails maxReg sd)) nextUsePos'' of { (,) reg mres -> let {cid = Cursor.curId maxReg sd} in Context.context (Trace.EAllocateBlockedReg (Prelude.id reg) mres (Prelude.id (Prelude.fst cid))) (case case mres of { Prelude.Just n -> (Prelude.<=) ((Prelude.succ) n) (case Interval.lookupUsePos ( (Cursor.curIntDetails maxReg sd)) (\u -> (Prelude.<=) pos (UsePos.uloc u)) of { Prelude.Just s -> s; Prelude.Nothing -> Interval.intervalEnd ( (Cursor.curIntDetails maxReg sd))}); Prelude.Nothing -> Prelude.False} of { Prelude.True -> Context.ibind (\x -> Context.ipure Prelude.Nothing) (Spill.spillCurrentInterval maxReg pre); Prelude.False -> Context.ibind (\x -> Context.ibind (\x0 -> Context.ibind (\mloc -> Context.ibind (\x1 -> Context.ibind (\x2 -> Context.ipure (Prelude.Just reg)) (Morph.moveUnhandledToActive maxReg pre reg)) (case mloc of { Prelude.Just n -> Context.context (Trace.EIntersectsWithFixedInterval n (Prelude.id reg)) (Split.splitCurrentInterval maxReg pre (Split.BeforePos n)); Prelude.Nothing -> Context.ipure ()})) (intersectsWithFixedInterval maxReg pre reg)) (Split.splitActiveIntervalForReg maxReg pre reg pos)) (Split.splitAnyInactiveIntervalForReg maxReg pre reg pos)})}) morphlen_transport :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.ScanStateDesc -> ScanState.IntervalId -> ScanState.IntervalId morphlen_transport maxReg b b' = Prelude.id mt_fst :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg) -> (,) ScanState.IntervalId PhysReg mt_fst maxReg b b' x = case x of { (,) xid reg -> (,) (morphlen_transport maxReg b b' xid) reg} type Coq_int_reg_seq = [] ((,) ScanState.IntervalId PhysReg) type Coq_intermediate_result = Specif.Coq_sig2 ScanState.ScanStateDesc goActive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc -> ([] Trace.SSTrace) -> ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg) -> Coq_int_reg_seq -> Prelude.Either ([] Trace.SSTrace) Coq_intermediate_result goActive maxReg pos sd e z x xs = let { eres = case (Prelude.<=) ((Prelude.succ) (Interval.intervalEnd ( (Vector0.vnth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of { Prelude.True -> let { filtered_var = Ssr.prop (ScanState.verifyNewHandled maxReg z (Interval.getIntervalDesc ( (Vector0.vnth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x)))) (Prelude.snd x))} in case filtered_var of { Prelude.Just _ -> let { filtered_var0 = Morph.moveActiveToHandled maxReg z Prelude.False (unsafeCoerce x)} in Prelude.Right filtered_var0; Prelude.Nothing -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap (Prelude.id (Prelude.snd x)) (Prelude.id (Prelude.fst x)) ((Prelude.succ) 0)) e)}; Prelude.False -> Prelude.Right (case Prelude.not (Interval.posWithinInterval ( (Vector0.vnth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x))) pos) of { Prelude.True -> Morph.moveActiveToInactive maxReg z (unsafeCoerce x); Prelude.False -> z})}} in case eres of { Prelude.Left err -> Prelude.Left err; Prelude.Right s -> Prelude.Right s} dep_foldl_invE :: (a2 -> Eqtype.Equality__Coq_type) -> a2 -> ([] Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a2 -> [] Eqtype.Equality__Coq_sort) -> (a2 -> a2 -> () -> Eqtype.Equality__Coq_sort -> Eqtype.Equality__Coq_sort) -> (a2 -> () -> Eqtype.Equality__Coq_sort -> ([] Eqtype.Equality__Coq_sort) -> () -> Prelude.Either a1 (Specif.Coq_sig2 a2)) -> Prelude.Either a1 a2 dep_foldl_invE e b v n q f f0 = let {filtered_var = (,) v n} in case filtered_var of { (,) l n0 -> case l of { [] -> Prelude.Right b; (:) y ys -> (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> Prelude.Right b) (\n' -> let {filtered_var0 = f0 b __ y ys __} in case filtered_var0 of { Prelude.Left err -> Prelude.Left err; Prelude.Right s -> let {ys' = Prelude.map (f b s __) ys} in dep_foldl_invE e s ys' n' q f f0}) n0}} checkActiveIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int -> Morph.SState () () () checkActiveIntervals maxReg pre pos = Morph.withScanStatePO maxReg pre (\sd _ -> Context.ibind (\e -> let { eres = dep_foldl_invE (\s -> Eqtype.prod_eqType (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s)) (Fintype.ordinal_eqType maxReg)) sd (unsafeCoerce (ScanState.active maxReg sd)) (Data.List.length (ScanState.active maxReg sd)) (unsafeCoerce (ScanState.active maxReg)) (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0)) (unsafeCoerce (\x _ x0 x1 _ -> goActive maxReg pos sd e x x0 x1))} in case eres of { Prelude.Left err -> Morph.error_ maxReg sd err; Prelude.Right s -> Context.iput (Morph.Build_SSInfo s __)}) Context.iask) moveInactiveToActive' :: Prelude.Int -> ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg) -> Coq_int_reg_seq -> ([] Trace.SSTrace) -> Prelude.Either ([] Trace.SSTrace) (Specif.Coq_sig2 ScanState.ScanStateDesc) moveInactiveToActive' maxReg z x xs e = let { filtered_var = Prelude.not (Ssrbool.in_mem (Prelude.snd (unsafeCoerce x)) (Ssrbool.mem (Seq.seq_predType (Fintype.ordinal_eqType maxReg)) (unsafeCoerce (Prelude.map (\i -> Prelude.snd i) (ScanState.active maxReg z)))))} in case filtered_var of { Prelude.True -> let { filtered_var0 = Morph.moveInactiveToActive maxReg z (unsafeCoerce x)} in Prelude.Right filtered_var0; Prelude.False -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap (Prelude.id (Prelude.snd x)) (Prelude.id (Prelude.fst x)) ((Prelude.succ) ((Prelude.succ) 0))) e)} goInactive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc -> ([] Trace.SSTrace) -> ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg) -> Coq_int_reg_seq -> Prelude.Either ([] Trace.SSTrace) Coq_intermediate_result goInactive maxReg pos sd e z x xs = let {f = \sd' -> Prelude.Right sd'} in case (Prelude.<=) ((Prelude.succ) (Interval.intervalEnd ( (Vector0.vnth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of { Prelude.True -> let { filtered_var = Ssr.prop (ScanState.verifyNewHandled maxReg z (Interval.getIntervalDesc ( (Vector0.vnth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x)))) (Prelude.snd x))} in case filtered_var of { Prelude.Just _ -> let { filtered_var0 = Morph.moveInactiveToHandled maxReg z Prelude.False (unsafeCoerce x)} in f filtered_var0; Prelude.Nothing -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap (Prelude.id (Prelude.snd x)) (Prelude.id (Prelude.fst x)) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0)))) e)}; Prelude.False -> case Interval.posWithinInterval ( (Vector0.vnth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x))) pos of { Prelude.True -> let {filtered_var = moveInactiveToActive' maxReg z x xs e} in case filtered_var of { Prelude.Left err -> Prelude.Left err; Prelude.Right s -> f s}; Prelude.False -> f z}} checkInactiveIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int -> Morph.SState () () () checkInactiveIntervals maxReg pre pos = Morph.withScanStatePO maxReg pre (\sd _ -> Context.ibind (\e -> let { eres = dep_foldl_invE (\s -> Eqtype.prod_eqType (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s)) (Fintype.ordinal_eqType maxReg)) sd (unsafeCoerce (ScanState.inactive maxReg sd)) (Data.List.length (ScanState.inactive maxReg sd)) (unsafeCoerce (ScanState.inactive maxReg)) (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0)) (unsafeCoerce (\x _ x0 x1 _ -> goInactive maxReg pos sd e x x0 x1))} in case eres of { Prelude.Left err -> Morph.error_ maxReg sd err; Prelude.Right s -> Context.iput (Morph.Build_SSInfo s __)}) Context.iask) handleInterval :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState () () (Prelude.Maybe PhysReg) handleInterval maxReg pre = Cursor.withCursor maxReg pre (\sd _ -> let {pos = Interval.intervalStart ( (Cursor.curIntDetails maxReg sd))} in case Interval.firstUsePos (Interval.getIntervalDesc ( (Cursor.curIntDetails maxReg sd))) of { Prelude.Just u -> Context.ibind (\x -> Context.ibind (\x0 -> Context.ibind (\mres -> case mres of { Prelude.Just x1 -> Context.imap (\x2 -> Prelude.Just x2) x1; Prelude.Nothing -> allocateBlockedReg maxReg pre}) (tryAllocateFreeReg maxReg pre)) (Morph.liftLen maxReg pre (\sd0 -> checkInactiveIntervals maxReg sd0 pos))) (Morph.liftLen maxReg pre (\sd0 -> checkActiveIntervals maxReg sd0 pos)); Prelude.Nothing -> Context.ibind (\x -> Context.ipure Prelude.Nothing) (Morph.moveUnhandledToHandled maxReg pre)}) finalizeScanState_obligation_1 :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int -> (Morph.SSInfo ()) -> Prelude.Either ([] Trace.SSTrace) ScanState.ScanStateDesc finalizeScanState_obligation_1 maxReg sd finalPos ss = case ss of { Morph.Build_SSInfo thisDesc0 _ -> let { _evar_0_ = \_ -> let { _evar_0_ = \_ -> let {_evar_0_ = \_ -> Prelude.Right thisDesc0} in let { _evar_0_0 = \_ -> Prelude.Left ((:) Trace.EInactiveIntervalsRemain [])} in case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Data.List.length (ScanState.inactive maxReg thisDesc0))) (unsafeCoerce 0) of { Prelude.True -> _evar_0_ __; Prelude.False -> _evar_0_0 __}} in let { _evar_0_0 = \_ -> Prelude.Left ((:) Trace.EActiveIntervalsRemain [])} in case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Data.List.length (ScanState.active maxReg thisDesc0))) (unsafeCoerce 0) of { Prelude.True -> _evar_0_ __; Prelude.False -> _evar_0_0 __}} in let { _evar_0_0 = \_ -> Prelude.Left ((:) Trace.EUnhandledIntervalsRemain [])} in case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Data.List.length (ScanState.unhandled maxReg thisDesc0))) (unsafeCoerce 0) of { Prelude.True -> _evar_0_ __; Prelude.False -> _evar_0_0 __}} finalizeScanState :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int -> Prelude.Either ([] Trace.SSTrace) ScanState.ScanStateDesc finalizeScanState maxReg sd finalPos = let { filtered_var = Context.ibind (\x -> checkInactiveIntervals maxReg sd finalPos) (checkActiveIntervals maxReg sd finalPos) [] (Morph.Build_SSInfo sd __)} in case filtered_var of { Prelude.Left errs -> Prelude.Left errs; Prelude.Right p -> case p of { (,) u ss -> finalizeScanState_obligation_1 maxReg sd finalPos ss}} walkIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int -> Prelude.Either ((,) ([] Trace.SSTrace) ScanState.ScanStateSig) ScanState.ScanStateSig walkIntervals maxReg sd positions = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> Prelude.Left ((,) ((:) Trace.EFuelExhausted []) (ScanState.packScanState maxReg ScanState.InUse sd))) (\n -> let { go = let { go count0 ss = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> Prelude.Right (Morph.Build_SSInfo (Morph.thisDesc maxReg ss) __)) (\cnt -> case handleInterval maxReg sd [] ss of { Prelude.Left err -> Prelude.Left ((,) err (ScanState.packScanState maxReg ScanState.InUse (Morph.thisDesc maxReg ss))); Prelude.Right p -> case p of { (,) o ss' -> case Morph.strengthenHasLen maxReg sd (Morph.thisDesc maxReg ss') of { Prelude.Just _ -> go cnt (Morph.Build_SSInfo (Morph.thisDesc maxReg ss') __); Prelude.Nothing -> Prelude.Right ss'}}}) count0} in go} in case Hask.Utils.uncons (ScanState.unhandled maxReg sd) of { Prelude.Just s -> case s of { (,) x s0 -> case x of { (,) i pos -> case go (Seq.count (\x0 -> Eqtype.eq_op Ssrnat.nat_eqType (Prelude.snd (unsafeCoerce x0)) (unsafeCoerce pos)) (ScanState.unhandled maxReg sd)) (Morph.Build_SSInfo sd __) of { Prelude.Left err -> Prelude.Left err; Prelude.Right ss -> walkIntervals maxReg (Morph.thisDesc maxReg ss) n}}}; Prelude.Nothing -> Prelude.Right (ScanState.packScanState maxReg ScanState.InUse sd)}) positions 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.id (Prelude.fst x)) (Interval.getIntervalDesc ( (Vector0.vnth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) (Prelude.fst x)))) (Prelude.snd x)) (ScanState.handled maxReg sd)