linearscan 0.8.0 → 0.9.0
raw patch · 20 files changed
+787/−1181 lines, 20 files
Files
- LinearScan.hs +116/−78
- LinearScan/Allocate.hs +16/−34
- LinearScan/Assign.hs +245/−276
- LinearScan/Blocks.hs +5/−3
- LinearScan/Build.hs +28/−50
- LinearScan/Eqtype.hs +0/−30
- LinearScan/IntMap.hs +21/−7
- LinearScan/Interval.hs +9/−67
- LinearScan/List1.hs +0/−15
- LinearScan/Main.hs +22/−3
- LinearScan/Maybe.hs +39/−0
- LinearScan/Morph.hs +3/−5
- LinearScan/Prelude0.hs +0/−6
- LinearScan/Range.hs +1/−39
- LinearScan/Resolve.hs +111/−340
- LinearScan/Seq.hs +4/−0
- LinearScan/Spill.hs +4/−10
- LinearScan/UsePos.hs +0/−10
- LinearScan/Verify.hs +160/−207
- linearscan.cabal +3/−1
LinearScan.hs view
@@ -96,41 +96,10 @@ , moveOp :: PhysReg -> LS.VarId -> PhysReg -> m [op2] , saveOp :: PhysReg -> LS.VarId -> m [op2] , restoreOp :: LS.VarId -> PhysReg -> m [op2]- , applyAllocs :: op1 -> [(LS.VarId, PhysReg)] -> m [op2]+ , applyAllocs :: op1 -> [((LS.VarId, LS.VarKind), PhysReg)] -> m [op2] , showOp1 :: op1 -> String } -showOp1' :: (op1 -> String)- -> LS.OpId- -- Interval Id, it's identity, and possible assigned reg- -> [(Int, Either PhysReg LS.VarId, Maybe PhysReg)]- -> [(Int, Either PhysReg LS.VarId, Maybe PhysReg)]- -> [LS.ResolvingMoveSet]- -> Maybe (LS.RegStateDescSet, [LS.AllocError])- -> op1- -> String-showOp1' showop pos ins outs rms maerrs o =- let render Nothing = ""- render (Just r) = "=r" ++ show r in- let marker label (_i, Left r, _reg) =- " <" ++ label ++ " r" ++ show r ++ ">\n"- marker label (i, Right v, reg) =- " <" ++ label ++ " v" ++ show v ++- "[" ++ show i ++ "]" ++ render reg ++ ">\n" in- let leader = show pos ++ ": " in- let width = length leader in- concatMap (marker "End") outs ++- concatMap (marker "Beg") ins ++- leader ++ showop o ++ "\n" ++- (case maerrs of- Nothing -> ""- Just (regState, aerrs) ->- concatMap (\x -> replicate width ' ' ++ "!!! " ++- replicate 8 ' ' ++ show x ++ "\n") aerrs ++- (unlines . map (replicate (width + 12) ' ' ++) . lines . show- $ regState)) ++- concatMap (\x -> replicate (width + 8) ' ' ++ show x ++ "\n") rms- deriving instance Eq OpKind deriving instance Show OpKind @@ -267,21 +236,35 @@ -> IntSet -> IntSet -> LoopState+ -> Maybe LS.RegStateDescSet+ -> Maybe LS.RegStateDescSet -> (LS.OpId -> [op1] -> String) -> blk1 -> String-showBlock1 getops bid pos liveIns liveOuts loopInfo showops b =+showBlock1 getops bid pos liveIns liveOuts loopInfo initials finals showops b = "\n [ BLOCK " ++ show bid ++ " ]\n" ++ " Live In => " ++ show (S.toList liveIns) ++ "\n" ++ " Live Kill => " ++ show (S.toList liveKill) ++ "\n" ++ " Live Gen => " ++ show (S.toList liveGen) ++ "\n" ++ " Live Out => " ++ show (S.toList liveOuts) ++ "\n" ++ " Incoming =>" ++ (if null branches- then " Entry"- else branches) ++ "\n"+ then " Entry"+ else branches) ++ "\n" ++ (if null loops then "" else " Loops =>" ++ loops ++ "\n")+ ++ (case initials of+ Nothing -> ""+ Just xs ->+ " Inputs =>\n"+ ++ (unlines . map (replicate 12 ' ' ++)+ . lines . show $ xs))+ ++ (case finals of+ Nothing -> ""+ Just xs ->+ " Outputs =>\n"+ ++ (unlines . map (replicate 12 ' ' ++)+ . lines . show $ xs)) ++ showops pos (getops b) where liveGen = liveOuts `S.difference` liveIns@@ -315,6 +298,70 @@ Just (_, d') -> " Depth=" ++ show d' in hdr ++ e ++ idxs ++ d +opContext :: Int+ -> ScanStateDesc+ -> IntMap [LS.ResolvingMoveSet]+ -> IntMap (LS.RegStateDescSet, [LS.AllocError])+ -> Int+ -> String+opContext width sd rms aerrs here =+ concatMap (marker "End") outs +++ concatMap (marker "Beg") ins +++ (case M.lookup here aerrs of+ Nothing -> ""+ Just (regState, allocErrs) ->+ concatMap+ (\x -> replicate width ' ' ++ "!!! " +++ replicate 8 ' ' ++ show x ++ "\n") allocErrs +++ (unlines . map (replicate (width + 12) ' ' ++)+ . lines . show $ regState)) +++ concatMap (\x -> replicate (width + 8) ' ' ++ show x ++ "\n")+ (fromMaybe [] (M.lookup here rms))+ where+ render Nothing = ""+ render (Just r) = "=r" ++ show r++ marker label (_i, Left r, _reg) =+ " <" ++ label ++ " r" ++ show r ++ ">\n"+ marker label (i, Right v, reg) =+ " <" ++ label ++ " v" ++ show v +++ "[" ++ show i ++ "]" ++ render reg ++ ">\n"++ findInts p f z = foldr k z . zip [0..]+ where+ k (_idx, Nothing) rest = rest+ k (idx, Just i) (brest, erest) =+ let mreg = M.lookup idx (allocations sd) in+ (if LS.ibeg i == p+ then (idx, f idx i, mreg) : brest+ else brest,+ if LS.iend i == p+ then (idx, f idx i, mreg) : erest+ else erest)++ (ins, outs) =+ findInts here (\idx _ -> Left idx)+ (findInts here (\_ i -> Right (LS.ivar i)) ([], [])+ (map Just (intervals sd)))+ (fixedIntervals sd)++showOp1' :: (a -> String)+ -> ScanStateDesc+ -> Int+ -> IntMap [LS.ResolvingMoveSet]+ -> IntMap (LS.RegStateDescSet, [LS.AllocError])+ -> a+ -> String+showOp1' showop sd pos rms aerrs o =+ blank ++ "--------------------" ++ "\n" +++ opContext width sd rms aerrs pos +++ opContext width sd rms aerrs (pos+1) +++ leader ++ showop o ++ "\n"+ where+ leader = show pos ++ ": "+ width = length leader+ blank = replicate width ' '+ showOps1 :: LinearScan.OpInfo accType op1 op2 -> ScanStateDesc -> IntMap [LS.ResolvingMoveSet]@@ -324,30 +371,7 @@ -> String showOps1 _ _ _ _ _ [] = "" showOps1 oinfo sd rms aerrs pos (o:os) =- let here = pos*2+1 in- let allocs = allocations sd in- let k (idx, i) (brest, erest) =- let mreg = M.lookup idx allocs in- (if LS.ibeg i == here- then (idx, Right (LS.ivar i), mreg) : brest- else brest,- if LS.iend i == here- then (idx, Right (LS.ivar i), mreg) : erest- else erest) in- let r (_idx, Nothing) rest = rest- r (idx, Just i) (brest, erest) =- let mreg = M.lookup idx allocs in- (if LS.ibeg i == here- then (idx, Left idx, mreg) : brest- else brest,- if LS.iend i == here- then (idx, Left idx, mreg) : erest- else erest) in- let (begs, ends) = foldr k ([], []) (zip [0..] (intervals sd)) in- let entriesIn = fromMaybe [] . M.lookup (pos*2+1) in- let (begs', ends') = foldr r (begs, ends) (zip [0..] (fixedIntervals sd)) in- showOp1' (showOp1 oinfo) (pos*2+1) begs' ends'- (entriesIn rms) (M.lookup (pos*2+1) aerrs) o+ showOp1' (showOp1 oinfo) sd (pos*2+1) rms aerrs o ++ showOps1 oinfo sd rms aerrs (pos+1) os -- | From the point of view of this library, a basic block is nothing more@@ -367,10 +391,12 @@ -> IntMap LS.BlockLiveSets -> IntMap [LS.ResolvingMoveSet] -> IntMap (LS.RegStateDescSet, [LS.AllocError])+ -> IntMap LS.RegStateDescSet+ -> IntMap LS.RegStateDescSet -> LoopState -> [blk1] -> m String-showBlocks1 binfo oinfo sd ls rms aerrs loopInfo = go 0+showBlocks1 binfo oinfo sd ls rms aerrs initials finals loopInfo = go 0 where go _ [] = return "" go pos (b:bs) = do@@ -382,6 +408,7 @@ let allops blk = let (x, y, z) = LinearScan.blockOps binfo blk in x ++ y ++ z (showBlock1 allops bid pos liveIn liveOut loopInfo+ (M.lookup bid initials) (M.lookup bid finals) (showOps1 oinfo sd rms aerrs) b ++) `liftM` go (pos + length (allops b)) bs @@ -401,8 +428,9 @@ , resolvingMoves :: IntMap [LS.ResolvingMoveSet] , _inputBlocks :: [blk1] , orderedBlocks :: [blk1]- , allocatedBlocks :: Either (IntMap (LS.RegStateDescSet, [LS.AllocError]))- [blk2]+ , allocatedBlocks :: Either (IntMap (LS.RegStateDescSet, [LS.AllocError]),+ IntMap LS.RegStateDescSet,+ IntMap LS.RegStateDescSet) [blk2] , scanStatePre :: Maybe ScanStateDesc , scanStatePost :: Maybe ScanStateDesc , blockInfo :: LinearScan.BlockInfo m blk1 blk2 op1 op2@@ -451,8 +479,11 @@ showDetails :: Monad m => Details m blk1 blk2 op1 op2- -> IntMap (LS.RegStateDescSet, [LS.AllocError]) -> m String-showDetails err allocErrs = do+ -> IntMap (LS.RegStateDescSet, [LS.AllocError])+ -> IntMap LS.RegStateDescSet+ -> IntMap LS.RegStateDescSet+ -> m String+showDetails err allocErrs initials finals = do let preUnhandled Nothing = "" preUnhandled (Just sd) = "Original:\n" ++@@ -469,7 +500,8 @@ showScanStateDesc (Just sd) preUnhandled = liftM2 (++) (showBlocks1 (blockInfo err) (opInfo err) sd- (liveSets err) (resolvingMoves err) allocErrs+ (liveSets err) (resolvingMoves err)+ allocErrs initials finals (loopState err) (orderedBlocks err)) (return ("\n" ++ preUnhandled ++ show sd)) @@ -497,7 +529,9 @@ -> Details m blk1 blk2 op1 op2 toDetails (LS.Build_Details a b c d e f g h i) binfo oinfo = Details a (M.fromList b) (M.fromList c) d e- (either (Left . M.fromList) Right f)+ (either (\((x, y), z) ->+ Left (M.fromList x, M.fromList y, M.fromList z))+ Right f) (fmap toScanStateDesc g) (fmap toScanStateDesc h) binfo oinfo (toLoopState i) @@ -517,25 +551,29 @@ -> LinearScan.BlockInfo m blk1 blk2 op1 op2 -> LinearScan.OpInfo m op1 op2 -> LS.UseVerifier- -> [blk1] -> m (Either (String, [String]) [blk2])-allocate 0 _ _ _ _ = return $ Left ("", ["Cannot allocate with no registers"])-allocate _ _ _ _ [] = return $ Left ("", ["No basic blocks were provided"])+ -> [blk1] -> m (String, Either [String] [blk2])+allocate 0 _ _ _ _ = return ("", Left ["Cannot allocate with no registers"])+allocate _ _ _ _ [] = return ("", Left ["No basic blocks were provided"]) allocate maxReg binfo oinfo useVerifier blocks = do res <- U.unsafeCoerce $ LS.linearScan coqMonad maxReg (fromBlockInfo binfo) (fromOpInfo oinfo) useVerifier blocks let res' = toDetails res binfo oinfo case reason res' of Just (err, _) -> do- dets <- showDetails res' M.empty- return $ Left (dets, map reasonToStr err)+ dets <- showDetails res' M.empty M.empty M.empty+ return (dets, Left (map reasonToStr err)) Nothing -> case allocatedBlocks res' of- Left m -> do- dets <- showDetails res' m- return $ Left (dets,- concatMap (\(pos, (_, es)) ->- ("At position " ++ show pos) : map show es)- (M.toList m))- Right blks -> return $ Right blks+ Left (m, initials, finals) -> do+ dets <- showDetails res' m initials finals+ return (dets,+ Left (concatMap+ (\(pos, (_, es)) ->+ ("At position " ++ show pos)+ : map show es)+ (M.toList m)))+ Right blks -> do+ dets <- showDetails res' M.empty M.empty M.empty+ return (dets, Right blks) where reasonToStr r = case r of LS.EOverlapsWithFixedInterval pos reg ->
LinearScan/Allocate.hs view
@@ -15,12 +15,10 @@ import qualified LinearScan.Context as Context import qualified LinearScan.Cursor as Cursor-import qualified LinearScan.Functor as Functor import qualified LinearScan.Interval as Interval import qualified LinearScan.Lib as Lib import qualified LinearScan.Maybe as Maybe import qualified LinearScan.Morph as Morph-import qualified LinearScan.Prelude0 as Prelude0 import qualified LinearScan.ScanState as ScanState import qualified LinearScan.Specif as Specif import qualified LinearScan.Spill as Spill@@ -126,27 +124,17 @@ (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- let {- freeUntilPos = Data.List.foldl' (\v reg ->- case ScanState.verifyNewHandled maxReg sd- (Interval.getIntervalDesc- ( (Cursor.curIntDetails maxReg sd))) reg of {- Prelude.True -> v;- Prelude.False ->- updateRegisterPos maxReg v reg (Prelude.Just 0)})- freeUntilPos' (Fintype.ord_enum maxReg)}+ 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 {@@ -188,21 +176,15 @@ let { atPos = \u -> (Prelude.&&)- ((Prelude.||)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)- (unsafeCoerce (UsePos.uloc u)))- (Eqtype.eq_op Ssrnat.nat_eqType- (unsafeCoerce ((Prelude.succ) pos))- (unsafeCoerce (UsePos.uloc u)))) (UsePos.regReq u)}+ (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 Prelude0.odd1;+ Prelude.Just s -> Prelude.Just 0; Prelude.Nothing -> Interval.nextUseAfter ( int) pos}} in- updateRegisterPos maxReg v reg- (Functor.fmap (unsafeCoerce Maybe.coq_Maybe_Functor) (\x -> - x) (unsafeCoerce pos'))}}+ updateRegisterPos maxReg v reg pos'}} in let { resolve = \xs ->@@ -239,7 +221,7 @@ (case Interval.lookupUsePos ( (Cursor.curIntDetails maxReg sd)) (\u -> (Prelude.<=) pos (UsePos.uloc u)) of {- Prelude.Just s -> s;+ Prelude.Just s -> s; Prelude.Nothing -> Interval.intervalEnd ( (Cursor.curIntDetails maxReg sd))}); Prelude.Nothing -> Prelude.False} of {
LinearScan/Assign.hs view
@@ -18,7 +18,6 @@ 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@@ -26,6 +25,7 @@ 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@@ -128,10 +128,11 @@ 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)+ 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 ->@@ -139,19 +140,18 @@ (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)))+ ((Prelude.&&)+ ((Prelude.<=) ((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 PhysReg)-varInfoAllocs maxReg opid allocs v =+ 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 opid allocs (Blocks.varKind maxReg v) (unsafeCoerce vid)}+ Prelude.Right vid -> varAllocs maxReg pos allocs (unsafeCoerce vid) v} type Verified mType a = Verify.Verified mType AssnStateDesc a @@ -162,8 +162,8 @@ 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 =+ (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@@ -171,30 +171,42 @@ 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))+ 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) (\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);+ 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)) 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 @@ -216,256 +228,213 @@ Prelude.Just bls -> let {liveIns = LiveSets.blockLiveIn bls} in let {liveOuts = LiveSets.blockLiveOut bls} in- Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ case Maybe.fromMaybe ((,) [] [])+ (IntMap.coq_IntMap_lookup bid mappings) of {+ (,) begMoves endMoves -> let {- eg = Graph.emptyGraph- (Resolve.coq_ResGraphNode_eqType maxReg)- (Resolve.coq_ResGraphEdge_eqType maxReg)- (unsafeCoerce (Resolve.determineEdge maxReg))}+ k = setAllocations maxReg mDict oinfo useVerifier allocs} 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+ let {+ resolutions = \pos moves ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 ->+ 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))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y) (_assnOpId y)))+ mDict)}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> 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)+ (\bmoves -> Monad.bind (State0.coq_StateT_Monad mDict)- (\begMoves' ->+ (\opsm' -> Monad.bind (State0.coq_StateT_Monad mDict)- (\bmoves ->+ (\opse' -> 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))+ (\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 opid+ useVerifier bid liveOuts))+ (case opse of {+ [] ->+ Applicative.pure+ (State0.coq_StateT_Applicative mDict) [];+ (:) e es ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\xs ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\x2 ->+ Applicative.pure+ (State0.coq_StateT_Applicative mDict)+ ((Prelude.++) xs x2))+ (k (resolutions opid endMoves)+ (Seq.last e es)))+ (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 opid) begMoves)) (Monad.concatMapM- (State0.coq_StateT_Applicative mDict) k opsb)})- (Verify.verifyBlockBegin maxReg mDict opid useVerifier- bid liveIns loops);+ (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 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ case Maybe.fromMaybe ((,) [] [])+ (IntMap.coq_IntMap_lookup bid mappings) of {+ (,) begMoves endMoves -> let {- eg = Graph.emptyGraph- (Resolve.coq_ResGraphNode_eqType maxReg)- (Resolve.coq_ResGraphEdge_eqType maxReg)- (unsafeCoerce (Resolve.determineEdge maxReg))}+ k = setAllocations maxReg mDict oinfo useVerifier allocs} 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+ let {+ resolutions = \pos moves ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 ->+ 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))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y) (_assnOpId y)))+ mDict)}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> 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)+ (\bmoves -> Monad.bind (State0.coq_StateT_Monad mDict)- (\begMoves' ->+ (\opsm' -> Monad.bind (State0.coq_StateT_Monad mDict)- (\bmoves ->+ (\opse' -> 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))+ (\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 opid+ useVerifier bid IntSet.emptyIntSet))+ (case opse of {+ [] ->+ Applicative.pure+ (State0.coq_StateT_Applicative mDict) [];+ (:) e es ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\xs ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\x2 ->+ Applicative.pure+ (State0.coq_StateT_Applicative mDict)+ ((Prelude.++) xs x2))+ (k (resolutions opid endMoves)+ (Seq.last e es)))+ (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 opid) begMoves)) (Monad.concatMapM- (State0.coq_StateT_Applicative mDict) k opsb)})- (Verify.verifyBlockBegin maxReg mDict opid useVerifier- bid IntSet.emptyIntSet loops)})+ (State0.coq_StateT_Applicative mDict)+ (k+ (Applicative.pure+ (State0.coq_StateT_Applicative mDict) []))+ 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)))@@ -496,7 +465,7 @@ (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)}))})+ (:) p l -> Prelude.Left st}))}) (considerOps maxReg mDict binfo oinfo useVerifier allocs liveSets mappings loops blocks (Verify.newVerifiedSig maxReg newAssnStateDesc))
LinearScan/Blocks.hs view
@@ -55,8 +55,10 @@ Build_OpInfo (opType1 -> OpKind) (opType1 -> [] VarInfo) (PhysReg -> VarId -> PhysReg -> m) (PhysReg -> VarId -> m) (VarId -> PhysReg -> m) (opType1 -> ([]- ((,) VarId PhysReg)) -> m) - (opType1 -> Prelude.String)+ ((,)+ ((,) VarId UsePos.VarKind)+ PhysReg)) -> m) (opType1 ->+ Prelude.String) opKind :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> a2 -> OpKind@@ -94,7 +96,7 @@ showOp -> restoreOp0} applyAllocs :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> a2 ->- ([] ((,) VarId PhysReg)) -> a1+ ([] ((,) ((,) VarId UsePos.VarKind) PhysReg)) -> a1 applyAllocs maxReg h o = case o of { Build_OpInfo opKind0 opRefs0 moveOp0 saveOp0 restoreOp0 applyAllocs0
LinearScan/Build.hs view
@@ -196,20 +196,8 @@ upos_before_rend :: Range.RangeDesc -> UsePos.UsePos -> Prelude.Bool upos_before_rend rd upos = case Range.ups rd of {- [] ->- case UsePos.uvar upos of {- UsePos.Input -> (Prelude.<=) (UsePos.uloc upos) (Range.rend rd);- _ -> (Prelude.<=) ((Prelude.succ) (UsePos.uloc upos)) (Range.rend rd)};- (:) u l ->- case (Prelude.&&)- (Prelude.not- (Eqtype.eq_op UsePos.coq_VarKind_eqType- (unsafeCoerce (UsePos.uvar upos)) (unsafeCoerce UsePos.Input)))- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (UsePos.uloc u))- (unsafeCoerce (Range.rend rd))) of {- Prelude.True ->- (Prelude.<=) ((Prelude.succ) (UsePos.uloc upos)) (UsePos.uloc u);- Prelude.False -> (Prelude.<=) (UsePos.uloc upos) (UsePos.uloc u)}}+ [] -> (Prelude.<=) ((Prelude.succ) (UsePos.uloc upos)) (Range.rend rd);+ (:) u l -> (Prelude.<=) (UsePos.uloc upos) (UsePos.uloc u)} makeNewRange :: Prelude.Int -> Prelude.Int -> Prelude.Int -> UsePos.UsePos -> Range.BoundedRange@@ -217,20 +205,20 @@ Range.Build_RangeDesc (case UsePos.uvar upos of { UsePos.Input -> (Prelude.succ) (Ssrnat.double b);- _ -> (Prelude.succ) (Ssrnat.double pos)})+ _ -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos))}) (case UsePos.uvar upos of {- UsePos.Input -> (Prelude.succ) (Ssrnat.double pos);- UsePos.Temp -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos));+ UsePos.Input -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos));+ UsePos.Temp -> (Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ (Ssrnat.double pos))); UsePos.Output -> (Prelude.succ) (Ssrnat.double e)}) ((:) upos []) -makeUsePos :: Prelude.Int -> Prelude.Int -> Blocks.VarInfo -> Specif.Coq_sig2- UsePos.UsePos+makeUsePos :: Prelude.Int -> Prelude.Int -> Blocks.VarInfo -> UsePos.UsePos makeUsePos maxReg pos var =- let {- upos = UsePos.Build_UsePos ((Prelude.succ) (Ssrnat.double pos))- (Blocks.regRequired maxReg var) (Blocks.varKind maxReg var)}- in- (Prelude.flip (Prelude.$)) __ (\_ -> upos)+ UsePos.Build_UsePos+ (case Blocks.varKind maxReg var of {+ UsePos.Input -> (Prelude.succ) (Ssrnat.double pos);+ _ -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos))})+ (Blocks.regRequired maxReg var) (Blocks.varKind maxReg var) handleOutputVar :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int -> (Prelude.Maybe PendingRanges) -> Blocks.VarInfo ->@@ -296,11 +284,11 @@ _evar_0_ = \replaceFirst _top_assumption_0 -> let { _evar_0_ = \_ ->- (Prelude.flip (Prelude.$))- (Range.coq_Range_cons _top_assumption_ ( _top_assumption_0))- (\br ->- let {- _evar_0_ = let {+ let {+ _evar_0_ = (Prelude.flip (Prelude.$))+ (Range.coq_Range_cons _top_assumption_+ ( _top_assumption_0)) (\br ->+ let { _evar_0_ = \_the_1st_wildcard_ -> Prelude.Just ((:[]) br)} in@@ -313,15 +301,16 @@ _evar_0_ x) (\x x0 -> _evar_0_0 x x0)- range0}- in- let {- _evar_0_0 = Prelude.Just- (NonEmpty.coq_NE_from_list br ( range0))}- in- case replaceFirst of {- Prelude.True -> _evar_0_;- Prelude.False -> _evar_0_0})}+ range0)}+ in+ let {+ _evar_0_0 = (Prelude.flip (Prelude.$)) _top_assumption_0 (\br ->+ Prelude.Just+ (NonEmpty.coq_NE_from_list br ( range0)))}+ in+ case replaceFirst of {+ Prelude.True -> _evar_0_;+ Prelude.False -> _evar_0_0}} in let { _evar_0_0 = \_ -> Prelude.Just@@ -408,23 +397,12 @@ Prelude.Just x -> _evar_0_ x; Prelude.Nothing -> m}))) IntMap.emptyIntMap -extractVarInfo :: Prelude.Int -> ([] Blocks.VarInfo) -> [] Blocks.VarInfo-extractVarInfo maxReg xs =- let {_evar_0_ = \x -> (:) x []} in- let {_evar_0_0 = \x xs0 -> (:) x ( xs0)} in- (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)- (\x ->- _evar_0_ x)- (\x x0 ->- _evar_0_0 x x0)- xs- handleVars :: Prelude.Int -> ([] Blocks.VarInfo) -> Prelude.Int -> Prelude.Int -> Prelude.Int -> (IntMap.IntMap PendingRanges) -> IntMap.IntMap PendingRanges handleVars maxReg varRefs b pos e ranges = let {- vars = IntMap.coq_IntMap_map (extractVarInfo maxReg)+ vars = Prelude.id (IntMap.coq_IntMap_groupOn (Blocks.nat_of_varId maxReg) varRefs)} in IntMap.coq_IntMap_mergeWithKey (handleVars_combine maxReg b pos e)
LinearScan/Eqtype.hs view
@@ -78,36 +78,6 @@ case t of { Equality__Mixin x x0 -> _evar_0_ x x0} -eqbP :: Equality__Coq_axiom Prelude.Bool-eqbP _top_assumption_ =- let {- _evar_0_ = \_top_assumption_0 ->- let {_evar_0_ = Ssrbool.ReflectT} in- let {_evar_0_0 = Ssrbool.ReflectF} in- case _top_assumption_0 of {- Prelude.True -> _evar_0_;- Prelude.False -> _evar_0_0}}- in- let {- _evar_0_0 = \_top_assumption_0 ->- let {_evar_0_0 = Ssrbool.ReflectF} in- let {_evar_0_1 = Ssrbool.ReflectT} in- case _top_assumption_0 of {- Prelude.True -> _evar_0_0;- Prelude.False -> _evar_0_1}}- in- case _top_assumption_ of {- Prelude.True -> _evar_0_;- Prelude.False -> _evar_0_0}--bool_eqMixin :: Equality__Coq_mixin_of Prelude.Bool-bool_eqMixin =- Equality__Mixin (Prelude.==) eqbP--bool_eqType :: Equality__Coq_type-bool_eqType =- unsafeCoerce bool_eqMixin- data Coq_subType t = SubType (Any -> t) (t -> () -> Any) (() -> (t -> () -> Any) -> Any -> Any)
LinearScan/IntMap.hs view
@@ -111,17 +111,31 @@ coq_IntMap_foldlWithKey f z m = Data.List.foldl' (\acc x -> f acc (Prelude.fst x) (Prelude.snd x)) z m +coq_IntMap_foldrWithKey :: (a2 -> Prelude.Int -> a1 -> a1) -> a1 -> (IntMap+ a2) -> a1+coq_IntMap_foldrWithKey f z m =+ Prelude.foldr (\x -> f (Prelude.snd x) (Prelude.fst x)) z m+ coq_IntMap_toList :: (IntMap a1) -> [] ((,) Prelude.Int a1) coq_IntMap_toList m = m -coq_IntMap_addToList :: Prelude.Int -> a1 -> (IntMap ([] a1)) -> IntMap- ([] a1)-coq_IntMap_addToList k x m =- coq_IntMap_alter (\mxs -> Prelude.Just- (case mxs of {- Prelude.Just xs -> (:) x xs;- Prelude.Nothing -> (:) x []})) k m+coq_IntMap_combine :: (Prelude.Int -> (Prelude.Maybe a1) -> (Prelude.Maybe+ a2) -> Prelude.Maybe a3) -> (IntMap a1) -> (IntMap + a2) -> IntMap a3+coq_IntMap_combine f =+ coq_IntMap_mergeWithKey (\idx x y ->+ f idx (Prelude.Just x) (Prelude.Just y))+ (coq_IntMap_foldrWithKey (\x idx rest ->+ let {mres = f idx (Prelude.Just x) Prelude.Nothing} in+ case mres of {+ Prelude.Just res -> coq_IntMap_insert idx res rest;+ Prelude.Nothing -> rest}) emptyIntMap)+ (coq_IntMap_foldrWithKey (\y idx rest ->+ let {mres = f idx Prelude.Nothing (Prelude.Just y)} in+ case mres of {+ Prelude.Just res -> coq_IntMap_insert idx res rest;+ Prelude.Nothing -> rest}) emptyIntMap) eqIntMap :: Eqtype.Equality__Coq_type -> (IntMap Eqtype.Equality__Coq_sort) -> (IntMap Eqtype.Equality__Coq_sort) -> Prelude.Bool
LinearScan/Interval.hs view
@@ -1,6 +1,5 @@-{-# OPTIONS_GHC -cpp -XMagicHash #-}-{- For Hugs, use the option -F"cpp -P -traditional" -} + module LinearScan.Interval where @@ -17,34 +16,12 @@ import qualified LinearScan.Logic as Logic import qualified LinearScan.Maybe as Maybe import qualified LinearScan.NonEmpty as NonEmpty-import qualified LinearScan.Prelude0 as Prelude0 import qualified LinearScan.Range as Range import qualified LinearScan.Specif as Specif import qualified LinearScan.UsePos as UsePos-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- __ :: any __ = Prelude.error "Logical or arity value used" @@ -95,11 +72,10 @@ intervalsOverlap :: IntervalDesc -> IntervalDesc -> Prelude.Maybe Prelude.Int intervalsOverlap i j =- Data.List.foldl' (\acc xr ->- Data.List.foldl' (\acc' yr ->- Maybe.option_choose acc'- (Range.rangesIntersect (Range.getRangeDesc ( xr))- (Range.getRangeDesc ( yr)))) acc (rds j)) Prelude.Nothing (rds i)+ Seq.head Prelude.Nothing+ (Prelude.filter (\x -> Maybe.isJust x)+ (Seq.allpairs (\x y -> Range.rangesIntersect ( x) ( y)) ( (rds i))+ ( (rds j)))) findIntervalUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) -> Prelude.Maybe@@ -141,7 +117,7 @@ _evar_0_ __ lookupUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->- Prelude.Maybe Prelude0.Coq_oddnum+ Prelude.Maybe Prelude.Int lookupUsePos d f = let { _evar_0_ = \_top_assumption_ ->@@ -157,13 +133,7 @@ Prelude.Just x -> _evar_0_ x; Prelude.Nothing -> _evar_0_0} -intervalHasInputsAt :: IntervalDesc -> Prelude.Int -> Prelude.Bool-intervalHasInputsAt d pos =- Data.List.foldl' (\b r -> (Prelude.||) b (Range.hasInputsAt ( r) pos))- Prelude.False (rds d)--nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe- Prelude0.Coq_oddnum+nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe Prelude.Int nextUseAfter d pos = case lookupUsePos d (\u -> (Prelude.<=) ((Prelude.succ) pos) (UsePos.uloc u)) of {@@ -176,21 +146,6 @@ [] -> Prelude.Nothing; (:) u l -> Prelude.Just u} -posAtRangeEnd :: IntervalDesc -> Prelude.Int -> Prelude.Bool-posAtRangeEnd d pos =- let {- go xs =- (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)- (\x ->- Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Range.rend ( x)))- (unsafeCoerce pos))- (\x xs0 ->- (Prelude.||)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Range.rend ( x)))- (unsafeCoerce pos)) (go xs0))- xs}- in go (rds d)- firstUsePos :: IntervalDesc -> Prelude.Maybe UsePos.UsePos firstUsePos d = let {@@ -203,18 +158,6 @@ xs} in go (rds d) -lastUsePos :: IntervalDesc -> Prelude.Maybe UsePos.UsePos-lastUsePos d =- let {- go xs =- (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)- (\x ->- List1.olast (Range.ups ( x)))- (\x xs0 ->- Maybe.option_choose (go xs0) (List1.olast (Range.ups ( x))))- xs}- in go (rds d)- afterLifetimeHole :: IntervalDesc -> Prelude.Int -> Prelude.Int afterLifetimeHole d pos = let {@@ -233,7 +176,7 @@ xs} in go (rds d) -firstUseReqReg :: IntervalDesc -> Prelude.Maybe Prelude0.Coq_oddnum+firstUseReqReg :: IntervalDesc -> Prelude.Maybe Prelude.Int firstUseReqReg d = lookupUsePos d UsePos.regReq @@ -246,8 +189,7 @@ (case (Prelude.<=) ((Prelude.succ) (ibeg x)) (ibeg y) of { Prelude.True -> ibeg y; Prelude.False -> ibeg x});- Prelude.False ->- Range.rangesIntersect ( (Prelude.last (rds x))) ( (Prelude.head (rds y)))}+ Prelude.False -> Prelude.Nothing} divideIntervalRanges :: IntervalDesc -> Prelude.Int -> ((,) Range.SortedRanges Range.SortedRanges)
LinearScan/List1.hs view
@@ -37,21 +37,6 @@ Prelude.True -> Prelude.Just v0; Prelude.False -> maybeLookup a xs x}}} -listToMaybe :: ([] a1) -> Prelude.Maybe ([] a1)-listToMaybe xs =- case xs of {- [] -> Prelude.Nothing;- (:) a l -> Prelude.Just xs}--olast :: ([] a1) -> Prelude.Maybe a1-olast l =- let {- go res xs =- case xs of {- [] -> res;- (:) x xs0 -> go (Prelude.Just x) xs0}}- in go Prelude.Nothing l- forFold :: a2 -> ([] a1) -> (a2 -> a1 -> a2) -> a2 forFold b v f = Data.List.foldl' f b v
LinearScan/Main.hs view
@@ -71,10 +71,17 @@ (IntMap.IntMap LiveSets.BlockLiveSets) (IntMap.IntMap ([] Resolve.ResolvingMoveSet)) ([] blockType1) ([] blockType1) (Prelude.Either+ ((,)+ ((,) (IntMap.IntMap ((,) Verify.RegStateDescSet- ([] Verify.AllocError))) ([] blockType2)) - (Prelude.Maybe ScanStateDescSet) (Prelude.Maybe ScanStateDescSet) Loops.LoopState+ ([] Verify.AllocError)))+ (IntMap.IntMap Verify.RegStateDescSet))+ (IntMap.IntMap Verify.RegStateDescSet))+ ([] blockType2)) (Prelude.Maybe+ ScanStateDescSet) (Prelude.Maybe+ ScanStateDescSet) + Loops.LoopState linearScan :: (Monad.Monad a1) -> Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4 a5) -> (Blocks.OpInfo a1 a4 a5) -> Verify.UseVerifier@@ -114,9 +121,21 @@ Monad.bind dict (\res -> case res of { (,) moves blocks2 ->+ let {+ blockInfo = case blocks2 of {+ Prelude.Left vs -> Prelude.Left ((,) ((,)+ (Verify.verErrors maxReg vs)+ (IntMap.coq_IntMap_map (\x ->+ Verify.fromRegStateDesc maxReg ( x))+ (Verify.verInit maxReg vs)))+ (IntMap.coq_IntMap_map (\x ->+ Verify.fromRegStateDesc maxReg ( x))+ (Verify.verFinal maxReg vs)));+ Prelude.Right xs -> Prelude.Right xs}}+ in Applicative.pure (Monad.is_applicative dict) (Build_Details Prelude.Nothing liveSets' moves blocks- blocks1 blocks2 (Prelude.Just+ blocks1 blockInfo (Prelude.Just (toScanStateDescSet maxReg ( ssig))) (Prelude.Just (toScanStateDescSet maxReg s)) loops)}) (Assign.assignRegNum maxReg dict binfo oinfo useVerifier
+ LinearScan/Maybe.hs view
@@ -0,0 +1,39 @@+++module LinearScan.Maybe 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+++fromMaybe :: a1 -> (Prelude.Maybe a1) -> a1+fromMaybe x my =+ case my of {+ Prelude.Just z -> z;+ Prelude.Nothing -> x}++isJust :: (Prelude.Maybe a1) -> Prelude.Bool+isJust x =+ case x of {+ Prelude.Just a -> Prelude.True;+ Prelude.Nothing -> Prelude.False}++option_map :: (a1 -> a2) -> (Prelude.Maybe a1) -> Prelude.Maybe a2+option_map f x =+ case x of {+ Prelude.Just x0 -> Prelude.Just (f x0);+ Prelude.Nothing -> Prelude.Nothing}++option_choose :: (Prelude.Maybe a1) -> (Prelude.Maybe a1) -> Prelude.Maybe a1+option_choose x y =+ case x of {+ Prelude.Just a -> x;+ Prelude.Nothing -> y}+
LinearScan/Morph.hs view
@@ -144,15 +144,13 @@ in case Eqtype.eq_op (Eqtype.option_eqType- (Eqtype.sig_eqType- (Eqtype.sig_eqType Ssrnat.nat_eqType- (unsafeCoerce Ssrnat.odd)) (\u ->+ (Eqtype.sig_eqType Ssrnat.nat_eqType (\u -> (Prelude.&&) ((Prelude.<=) (Interval.ibeg ( (Vector0.vnth nextInterval0 intervals0 i)))- ( (unsafeCoerce u)))- ((Prelude.<=) ( (unsafeCoerce u))+ (unsafeCoerce u))+ ((Prelude.<=) ((Prelude.succ) (unsafeCoerce u)) (Interval.iend ( (Vector0.vnth nextInterval0 intervals0 i))))))) (unsafeCoerce
LinearScan/Prelude0.hs view
@@ -29,9 +29,3 @@ lebf f n m = (Prelude.<=) (f n) (f m) -type Coq_oddnum = Prelude.Int--odd1 :: Prelude.Int-odd1 =- (Prelude.succ) 0-
LinearScan/Range.hs view
@@ -133,34 +133,6 @@ transportSortedRanges b pos rp = rp -hasInputsAt :: RangeDesc -> Prelude.Int -> Prelude.Bool-hasInputsAt rd pos =- Data.List.foldl' (\b u ->- case (Prelude.||) b- ((Prelude.&&)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (UsePos.uloc u))- (unsafeCoerce pos))- (Eqtype.eq_op UsePos.coq_VarKind_eqType- (unsafeCoerce (UsePos.uvar u)) (unsafeCoerce UsePos.Input))) of {- Prelude.True -> Prelude.True;- Prelude.False -> b}) Prelude.False (ups rd)--hasOnlyOutputsAt :: RangeDesc -> Prelude.Int -> Prelude.Bool-hasOnlyOutputsAt rd pos =- let {- xs = Prelude.filter (\u ->- Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (UsePos.uloc u))- (unsafeCoerce pos)) (ups rd)}- in- (Prelude.&&) ((Prelude.<=) ((Prelude.succ) 0) (Data.List.length xs))- (Seq.all (\u ->- Eqtype.eq_op UsePos.coq_VarKind_eqType (unsafeCoerce (UsePos.uvar u))- (unsafeCoerce UsePos.Output)) xs)--rangesJoinedAt :: RangeDesc -> RangeDesc -> Prelude.Int -> Prelude.Bool-rangesJoinedAt x y pos =- (Prelude.&&) (hasInputsAt x pos) (Prelude.not (hasOnlyOutputsAt y pos))- rangesIntersect :: RangeDesc -> RangeDesc -> Prelude.Maybe Prelude.Int rangesIntersect x y = case (Prelude.&&) ((Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y))@@ -169,17 +141,7 @@ (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of { Prelude.True -> rbeg y; Prelude.False -> rbeg x});- Prelude.False ->- case (Prelude.&&)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend x))- (unsafeCoerce (rbeg y))) (rangesJoinedAt x y (rend x)) of {- Prelude.True -> Prelude.Just (rend x);- Prelude.False ->- case (Prelude.&&)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend y))- (unsafeCoerce (rbeg x))) (rangesJoinedAt y x (rend y)) of {- Prelude.True -> Prelude.Just (rend y);- Prelude.False -> Prelude.Nothing}}}+ Prelude.False -> Prelude.Nothing} findRangeUsePos :: RangeDesc -> (UsePos.UsePos -> Prelude.Bool) -> Prelude.Maybe UsePos.UsePos
LinearScan/Resolve.hs view
@@ -24,9 +24,6 @@ import qualified LinearScan.List1 as List1 import qualified LinearScan.LiveSets as LiveSets import qualified LinearScan.Monad as Monad-import qualified LinearScan.Prelude0 as Prelude0-import qualified LinearScan.Range as Range-import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Ssrbool as Ssrbool@@ -693,187 +690,45 @@ coq_ResGraphNode_eqType maxReg = unsafeCoerce (coq_ResGraphNode_eqMixin maxReg) -data ResGraphEdge =- Build_ResGraphEdge ResolvingMove Prelude.Bool--resMove :: Prelude.Int -> ResGraphEdge -> ResolvingMove-resMove maxReg r =- case r of {- Build_ResGraphEdge resMove0 resGhost0 -> resMove0}--resGhost :: Prelude.Int -> ResGraphEdge -> Prelude.Bool-resGhost maxReg r =- case r of {- Build_ResGraphEdge resMove0 resGhost0 -> resGhost0}--eqResGraphEdge :: Prelude.Int -> ResGraphEdge -> ResGraphEdge -> Prelude.Bool-eqResGraphEdge maxReg s1 s2 =- case s1 of {- Build_ResGraphEdge a1 b1 ->- case s2 of {- Build_ResGraphEdge a2 b2 ->- (Prelude.&&)- (Eqtype.eq_op (coq_ResolvingMove_eqType maxReg) (unsafeCoerce a1)- (unsafeCoerce a2))- (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1) (unsafeCoerce b2))}}--eqResGraphEdgeP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResGraphEdge-eqResGraphEdgeP maxReg _top_assumption_ =- let {- _evar_0_ = \a1 b1 _top_assumption_0 ->- let {- _evar_0_ = \a2 b2 ->- let {- _evar_0_ = \_ ->- let {- _evar_0_ = let {- _evar_0_ = \_ ->- let {_evar_0_ = Ssrbool.ReflectT} in _evar_0_}- in- let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in- case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {- Ssrbool.ReflectT -> _evar_0_ __;- Ssrbool.ReflectF -> _evar_0_0 __}}- in- _evar_0_}- in- let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in- case Eqtype.eqP (coq_ResolvingMove_eqType maxReg) a1 a2 of {- Ssrbool.ReflectT -> _evar_0_ __;- Ssrbool.ReflectF -> _evar_0_0 __}}- in- case _top_assumption_0 of {- Build_ResGraphEdge x x0 -> unsafeCoerce _evar_0_ x x0}}- in- case _top_assumption_ of {- Build_ResGraphEdge x x0 -> unsafeCoerce _evar_0_ x x0}--coq_ResGraphEdge_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of- ResGraphEdge-coq_ResGraphEdge_eqMixin maxReg =- Eqtype.Equality__Mixin (eqResGraphEdge maxReg) (eqResGraphEdgeP maxReg)--coq_ResGraphEdge_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type-coq_ResGraphEdge_eqType maxReg =- unsafeCoerce (coq_ResGraphEdge_eqMixin maxReg)--determineEdge :: Prelude.Int -> ResGraphEdge -> (,) ResGraphNode ResGraphNode-determineEdge maxReg x =- let {- go m =- case m of {- Move fr fv tr -> (,) (RegNode tr) (RegNode fr);- Transfer fr fv tr -> (,) (RegNode tr) (RegNode fr);- Spill fr tv -> (,) (VirtNode (VarNode tv)) (RegNode fr);- Restore fv tr -> (,) (RegNode tr) (VarNode fv);- AllocReg fv tr -> (,) (RegNode tr) (VarNode fv);- FreeReg fr tv -> (,) (VirtNode (VarNode tv)) (RegNode fr);- Looped x0 -> go x0}}- in go (resMove maxReg x)--compareEdges :: Prelude.Int -> ((,) Prelude.Int ResGraphEdge) -> ((,)- Prelude.Int ResGraphEdge) -> Prelude.Bool-compareEdges maxReg x y =- let {xe = determineEdge maxReg (Prelude.snd x)} in- let {ye = determineEdge maxReg (Prelude.snd y)} in- case (Prelude.&&)- (Eqtype.eq_op Ssrnat.nat_eqType (Prelude.fst (unsafeCoerce x))- (Prelude.fst (unsafeCoerce y)))- (Eqtype.eq_op (coq_ResGraphNode_eqType maxReg)- (Prelude.fst (unsafeCoerce xe)) (Prelude.fst (unsafeCoerce ye))) of {- Prelude.True ->- (Prelude.&&) (resGhost maxReg (Prelude.snd x))- (Prelude.not (resGhost maxReg (Prelude.snd y)));- Prelude.False -> Prelude.False}+determineNodes :: Prelude.Int -> ResolvingMove -> (,) ResGraphNode+ ResGraphNode+determineNodes maxReg x =+ case x of {+ Move fr fv tr -> (,) (RegNode tr) (RegNode fr);+ Transfer fr fv tr -> (,) (RegNode tr) (RegNode fr);+ Spill fr tv -> (,) (VirtNode (VarNode tv)) (RegNode fr);+ Restore fv tr -> (,) (RegNode tr) (VarNode fv);+ AllocReg fv tr -> (,) (RegNode tr) (VarNode fv);+ FreeReg fr tv -> (,) (VirtNode (VarNode tv)) (RegNode fr);+ Looped x0 -> determineNodes maxReg x0} -isEdgeSplittable :: Prelude.Int -> ResGraphEdge -> Prelude.Bool-isEdgeSplittable maxReg x =- case resMove maxReg x of {+isMoveSplittable :: Prelude.Int -> ResolvingMove -> Prelude.Bool+isMoveSplittable maxReg x =+ case x of { Move p v p0 -> Prelude.True; Transfer p v p0 -> Prelude.True; _ -> Prelude.False} -splitEdge :: Prelude.Int -> ResGraphEdge -> [] ResGraphEdge-splitEdge maxReg x =- case resMove maxReg x of {- Move fr fv tr -> (:) (Build_ResGraphEdge (Spill fr fv) Prelude.False) ((:)- (Build_ResGraphEdge (Restore fv tr) (resGhost maxReg x)) []);- Transfer fr fv tr -> (:) (Build_ResGraphEdge (FreeReg fr fv)- Prelude.False) ((:) (Build_ResGraphEdge (AllocReg fv tr)- (resGhost maxReg x)) []);+splitMove :: Prelude.Int -> ResolvingMove -> [] ResolvingMove+splitMove maxReg x =+ case x of {+ Move fr fv tr -> (:) (Spill fr fv) ((:) (Restore fv tr) []);+ Transfer fr fv tr -> (:) (FreeReg fr fv) ((:) (AllocReg fv tr) []); Looped r -> (:) x [];- _ -> (:) (Build_ResGraphEdge (Looped (resMove maxReg x))- (resGhost maxReg x)) []}--sortMoves :: Prelude.Int -> Graph.Graph -> [] ResGraphEdge-sortMoves maxReg x =- Prelude.map (\i -> Prelude.snd (unsafeCoerce i))- (List1.sortBy (unsafeCoerce (compareEdges maxReg))- (Prelude.snd- (Graph.topsort (coq_ResGraphNode_eqType maxReg)- (coq_ResGraphEdge_eqType maxReg) x- (unsafeCoerce (isEdgeSplittable maxReg))- (unsafeCoerce (splitEdge maxReg)))))--determineMoves :: Prelude.Int -> (IntMap.IntMap ([] ResGraphEdge)) -> []- ResGraphEdge-determineMoves maxReg moves =- sortMoves maxReg- (IntMap.coq_IntMap_foldr- (Prelude0.flip- (Prelude.foldr- (unsafeCoerce- (Graph.addEdge (coq_ResGraphNode_eqType maxReg)- (coq_ResGraphEdge_eqType maxReg)))))- (Graph.emptyGraph (coq_ResGraphNode_eqType maxReg)- (coq_ResGraphEdge_eqType maxReg)- (unsafeCoerce (determineEdge maxReg))) moves)+ _ -> (:) (Looped x) []} resolvingMoves :: Prelude.Int -> ([] Allocate.Allocation) -> (Prelude.Maybe IntSet.IntSet) -> Prelude.Int -> Prelude.Int ->- IntMap.IntMap ([] ResGraphEdge)+ IntMap.IntMap ResolvingMove resolvingMoves maxReg allocs liveIn from to = let {- collect = \p q i rest ->- let {int = Allocate.intVal maxReg i} in- case p int of {- Prelude.True -> IntMap.coq_IntMap_alter (q i) (Interval.ivar int) rest;- Prelude.False -> rest}}- in- let {- liveAtFrom = Prelude.foldr- (collect (\i ->- (Prelude.&&) ((Prelude.<=) (Interval.ibeg i) from)- ((Prelude.<=) ((Prelude.succ) from) (Interval.iend i)))- (\a x -> Prelude.Just a)) IntMap.emptyIntMap allocs}- in- let {- shouldKeep = \int pos ->- case (Prelude.<=) (Interval.ibeg int) pos of {- Prelude.True ->- case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)- (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.True;- Prelude.False -> (,)- ((Prelude.<=) ((Prelude.succ) to) (Interval.iend int)) Prelude.False};- Prelude.False -> (,) Prelude.False Prelude.False}}- in- let {- outputBegin = \int pos ->- Range.hasOnlyOutputsAt ( (Prelude.head (Interval.rds int))) pos}- in- let {- liveAtTo = Prelude.foldr- (collect (\i -> Prelude.fst (shouldKeep i to)) (\a rest ->- Prelude.Just ((:) ((,) ((,) a- (Prelude.snd (shouldKeep (Allocate.intVal maxReg a) to)))- (outputBegin (Allocate.intVal maxReg a) to))- (case rest of {- Prelude.Just xs -> xs;- Prelude.Nothing -> []})))) IntMap.emptyIntMap allocs}+ allocsAt = \pos ->+ Prelude.foldr (\a rest ->+ let {i = Allocate.intVal maxReg a} in+ case (Prelude.&&) ((Prelude.<=) (Interval.ibeg i) pos)+ ((Prelude.<=) ((Prelude.succ) pos) (Interval.iend i)) of {+ Prelude.True -> IntMap.coq_IntMap_insert (Interval.ivar i) a rest;+ Prelude.False -> rest}) IntMap.emptyIntMap allocs} in let { varNotLive = \vid ->@@ -881,174 +736,91 @@ Prelude.Just ins -> Prelude.not (IntSet.coq_IntSet_member vid ins); Prelude.Nothing -> Prelude.False}} in- let {- regsReferenced = IntMap.coq_IntMap_mergeWithKey (\vid x yps ->- let {- go = \acc yp ->- case yp of {- (,) y0 y1 ->- case y0 of {- (,) y y2 ->- case Prelude.not- (Eqtype.eq_op- (Eqtype.option_eqType- (Fintype.ordinal_eqType maxReg))- (unsafeCoerce- (Allocate.intReg maxReg x))- (unsafeCoerce- (Allocate.intReg maxReg y))) of {- Prelude.True ->- let {- next = case Allocate.intReg maxReg y of {- Prelude.Just yreg -> (:) yreg acc;- Prelude.Nothing -> acc}}- in- case Allocate.intReg maxReg x of {- Prelude.Just xreg -> (:) xreg next;- Prelude.Nothing -> next};- Prelude.False -> acc}}}}- in- Prelude.Just (Data.List.foldl' go [] yps))- (IntMap.coq_IntMap_foldlWithKey (\acc vid x ->- case Allocate.intReg maxReg x of {- Prelude.Just xreg ->- IntMap.coq_IntMap_addToList vid xreg acc;- Prelude.Nothing -> acc}) IntMap.emptyIntMap)- (IntMap.coq_IntMap_foldlWithKey (\acc vid yps ->- let {- go = \acc0 yp ->- case yp of {- (,) y0 y1 ->- case y0 of {- (,) y y2 ->- case Allocate.intReg maxReg y of {- Prelude.Just yreg ->- IntMap.coq_IntMap_addToList vid yreg acc0;- Prelude.Nothing -> acc0}}}}- in- Data.List.foldl' go acc yps) IntMap.emptyIntMap)- liveAtFrom liveAtTo}- in- let {- otherRegs = List1.concat- (Prelude.map (\x ->- (Prelude..) (Prelude.map Prelude.id) Prelude.snd x)- (IntMap.coq_IntMap_toList regsReferenced))}- in- IntMap.coq_IntMap_mergeWithKey (\vid x yps ->- let {- go = \yp ->- case yp of {- (,) y0 outb ->- case y0 of {- (,) y ghost ->- case Eqtype.eq_op- (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))- (unsafeCoerce (Allocate.intReg maxReg x))- (unsafeCoerce (Allocate.intReg maxReg y)) of {- Prelude.True ->+ IntMap.coq_IntMap_combine (\vid mx my ->+ case mx of {+ Prelude.Just x ->+ case my of {+ Prelude.Just y ->+ case Eqtype.eq_op+ (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))+ (unsafeCoerce (Allocate.intReg maxReg x))+ (unsafeCoerce (Allocate.intReg maxReg y)) of {+ Prelude.True -> Prelude.Nothing;+ Prelude.False ->+ case Allocate.intReg maxReg x of {+ Prelude.Just xr -> case Allocate.intReg maxReg y of {- Prelude.Just reg ->- case ghost of {- Prelude.True -> (:) (Build_ResGraphEdge (FreeReg reg vid)- Prelude.True) [];- Prelude.False ->- case IntSet.coq_IntSet_member ( reg) otherRegs of {- Prelude.True -> (:) (Build_ResGraphEdge (FreeReg reg vid)- Prelude.False) ((:) (Build_ResGraphEdge (AllocReg vid reg)- Prelude.False) []);- Prelude.False -> []}};- Prelude.Nothing -> []};- Prelude.False ->- let {- mmv = case Allocate.intReg maxReg x of {- Prelude.Just xr ->- case Allocate.intReg maxReg y of {- Prelude.Just yr -> Prelude.Just- (case (Prelude.||) outb (varNotLive vid) of {- Prelude.True -> Transfer xr vid yr;- Prelude.False -> Move xr vid yr});- Prelude.Nothing -> Prelude.Just (Spill xr vid)};- Prelude.Nothing ->- case Allocate.intReg maxReg y of {- Prelude.Just yr -> Prelude.Just- (case (Prelude.||) outb (varNotLive vid) of {- Prelude.True -> AllocReg vid yr;- Prelude.False -> Restore vid yr});- Prelude.Nothing -> Prelude.Nothing}}}- in- case mmv of {- Prelude.Just mv -> (:) (Build_ResGraphEdge mv ghost) [];- Prelude.Nothing -> []}}}}}- in- List1.listToMaybe- (Data.List.foldl' (\acc x0 -> (Prelude.++) acc (go x0)) [] yps))- (IntMap.coq_IntMap_foldlWithKey (\acc vid x ->- case Allocate.intReg maxReg x of {- Prelude.Just r ->- IntMap.coq_IntMap_addToList vid (Build_ResGraphEdge (FreeReg r vid)- Prelude.False) acc;- Prelude.Nothing -> acc}) IntMap.emptyIntMap)- (IntMap.coq_IntMap_foldlWithKey (\acc vid yps ->- let {- go = \acc0 yp ->- case yp of {- (,) y0 outb ->- case y0 of {- (,) y ghost ->+ Prelude.Just yr -> Prelude.Just+ (case (Prelude.||) (varNotLive vid)+ (Prelude.not (Ssrnat.odd to)) of {+ Prelude.True -> Transfer xr vid yr;+ Prelude.False -> Move xr vid yr});+ Prelude.Nothing -> Prelude.Just (Spill xr vid)};+ Prelude.Nothing -> case Allocate.intReg maxReg y of {- Prelude.Just r ->- IntMap.coq_IntMap_addToList vid (Build_ResGraphEdge (AllocReg- vid r) ghost) acc0;- Prelude.Nothing -> acc0}}}}- in- Data.List.foldl' go acc yps) IntMap.emptyIntMap) liveAtFrom liveAtTo--type BlockMoves = (,) Graph.Graph Graph.Graph+ Prelude.Just yr -> Prelude.Just+ (case (Prelude.||) (varNotLive vid)+ (Prelude.not (Ssrnat.odd to)) of {+ Prelude.True -> AllocReg vid yr;+ Prelude.False -> Restore vid yr});+ Prelude.Nothing -> Prelude.Nothing}}};+ Prelude.Nothing ->+ case Allocate.intReg maxReg x of {+ Prelude.Just r -> Prelude.Just (FreeReg r vid);+ Prelude.Nothing -> Prelude.Nothing}};+ Prelude.Nothing ->+ case my of {+ Prelude.Just y ->+ case Allocate.intReg maxReg y of {+ Prelude.Just r -> Prelude.Just (AllocReg vid r);+ Prelude.Nothing -> Prelude.Nothing};+ Prelude.Nothing -> Prelude.Nothing}}) (allocsAt from) (allocsAt to) -applyMappings :: Prelude.Int -> Blocks.BlockId -> (IntMap.IntMap BlockMoves)- -> Prelude.Bool -> (IntMap.IntMap ([] ResGraphEdge)) ->- IntMap.IntMap BlockMoves-applyMappings maxReg bid mappings in_from moves =+determineMoves :: Prelude.Int -> ([] Allocate.Allocation) -> (Prelude.Maybe+ IntSet.IntSet) -> Prelude.Int -> Prelude.Int -> []+ ResolvingMove+determineMoves maxReg allocs liveIn from to = let {- go = \ms mv ->- let {- addToGraphs = \e xs ->- case xs of {- (,) gbeg gend ->- case in_from of {- Prelude.True -> (,) gbeg- (Graph.addEdge (coq_ResGraphNode_eqType maxReg)- (coq_ResGraphEdge_eqType maxReg) e gend);- Prelude.False -> (,)- (Graph.addEdge (coq_ResGraphNode_eqType maxReg)- (coq_ResGraphEdge_eqType maxReg) e gbeg) gend}}}- in- let {- eg = Graph.emptyGraph (coq_ResGraphNode_eqType maxReg)- (coq_ResGraphEdge_eqType maxReg)- (unsafeCoerce (determineEdge maxReg))}- in- let {- f = \mxs ->- addToGraphs mv- (case mxs of {- Prelude.Just xs -> xs;- Prelude.Nothing -> (,) eg eg})}- in- IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms}+ sortMoves = \x ->+ Prelude.map (\i -> Prelude.snd i)+ (Prelude.snd+ (Graph.topsort (coq_ResGraphNode_eqType maxReg)+ (coq_ResolvingMove_eqType maxReg) x+ (unsafeCoerce (isMoveSplittable maxReg))+ (unsafeCoerce (splitMove maxReg))))} in- IntMap.coq_IntMap_foldl (Data.List.foldl' (unsafeCoerce go)) mappings moves+ unsafeCoerce sortMoves+ (IntMap.coq_IntMap_foldr+ (unsafeCoerce+ (Graph.addEdge (coq_ResGraphNode_eqType maxReg)+ (coq_ResolvingMove_eqType maxReg)))+ (Graph.emptyGraph (coq_ResGraphNode_eqType maxReg)+ (coq_ResolvingMove_eqType maxReg)+ (unsafeCoerce (determineNodes maxReg)))+ (resolvingMoves maxReg allocs liveIn from to)) +type BlockMoves = (,) ([] ResolvingMove) ([] ResolvingMove)+ checkBlockBoundary :: Prelude.Int -> ([] Allocate.Allocation) ->- Blocks.BlockId -> Prelude.Bool ->- LiveSets.BlockLiveSets -> LiveSets.BlockLiveSets ->- IntSet.IntSet -> (IntMap.IntMap BlockMoves) ->+ IntSet.IntSet -> Prelude.Int -> Prelude.Bool ->+ (Prelude.Maybe LiveSets.BlockLiveSets) ->+ LiveSets.BlockLiveSets -> (IntMap.IntMap BlockMoves) -> IntMap.IntMap BlockMoves-checkBlockBoundary maxReg allocs bid in_from from to liveIn mappings =- applyMappings maxReg bid mappings in_from- (resolvingMoves maxReg allocs (Prelude.Just liveIn)- (LiveSets.blockLastOpId from) (LiveSets.blockFirstOpId to))+checkBlockBoundary maxReg allocs liveIn bid in_from mfrom to mappings =+ let {+ moves = determineMoves maxReg allocs (Prelude.Just liveIn)+ (case mfrom of {+ Prelude.Just from -> LiveSets.blockLastOpId from;+ Prelude.Nothing -> 0}) (LiveSets.blockFirstOpId to)}+ in+ IntMap.coq_IntMap_alter (\mx ->+ case case mx of {+ Prelude.Just x -> x;+ Prelude.Nothing -> (,) [] []} of {+ (,) begs ends -> Prelude.Just+ (case in_from of {+ Prelude.True -> (,) begs moves;+ Prelude.False -> (,) moves ends})}) bid mappings resolveDataFlow :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] Allocate.Allocation) -> ([] @@ -1066,10 +838,9 @@ let { mappings' = case isFirst of { Prelude.True ->- applyMappings maxReg bid mappings Prelude.False- (resolvingMoves maxReg allocs Prelude.Nothing- ((Prelude.succ) 0)- (LiveSets.blockFirstOpId from));+ checkBlockBoundary maxReg allocs+ (LiveSets.blockLiveIn from) bid Prelude.False+ Prelude.Nothing from mappings; Prelude.False -> mappings}} in Monad.bind mDict (\suxs ->@@ -1091,9 +862,9 @@ Prelude.True -> bid; Prelude.False -> s_bid}} in- checkBlockBoundary maxReg allocs key- in_from from to (LiveSets.blockLiveIn to)- ms;+ checkBlockBoundary maxReg allocs+ (LiveSets.blockLiveIn to) key in_from+ (Prelude.Just from) to ms; Prelude.Nothing -> ms})}} in Applicative.pure (Monad.is_applicative mDict) ((,) mappings''
LinearScan/Seq.hs view
@@ -245,3 +245,7 @@ flatten = Prelude.foldr (Prelude.++) [] +allpairs :: (a1 -> a2 -> a3) -> ([] a1) -> ([] a2) -> [] a3+allpairs f s t =+ Prelude.foldr (\x -> (Prelude.++) (Prelude.map (f x) t)) [] s+
LinearScan/Spill.hs view
@@ -70,12 +70,7 @@ optimalSplitPosition :: Interval.IntervalDesc -> Prelude.Int -> Prelude.Int -> Prelude.Int optimalSplitPosition d lb ub =- case (Prelude.&&)- ((Prelude.||) (Interval.posAtRangeEnd d ub)- (Interval.intervalHasInputsAt (Interval.getIntervalDesc d) ub))- ((Prelude.<=) ((Prelude.succ) lb) ub) of {- Prelude.True -> Prelude.pred ub;- Prelude.False -> ub}+ ub spillInterval :: Prelude.Int -> ScanState.ScanStateDesc -> Interval.IntervalDesc -> ScanState.IntervalId -> Prelude.Int@@ -88,9 +83,8 @@ let { _evar_0_ = \_top_assumption_ -> (Prelude.flip (Prelude.$)) ((:) (Trace.EIntervalHasUsePosReqReg- ( _top_assumption_)) e2) (\e3 ->- let {- optSplitPos2 = optimalSplitPosition ( i1) beg ( _top_assumption_)}+ _top_assumption_) e2) (\e3 ->+ let {optSplitPos2 = optimalSplitPosition ( i1) beg _top_assumption_} in let { _evar_0_ = \_ ->@@ -136,7 +130,7 @@ let { _evar_0_0 = \_top_assumption_1 -> Prelude.Left ((:) (Trace.ECannotSpillIfRegisterRequiredBefore optSplitPos2- ( _top_assumption_1)) e3)}+ _top_assumption_1) e3)} in let { _evar_0_1 = \_ ->
LinearScan/UsePos.hs view
@@ -42,16 +42,6 @@ | Temp | Output -coq_VarKind_leq :: VarKind -> VarKind -> Prelude.Bool-coq_VarKind_leq x y =- case x of {- Input -> Prelude.True;- Temp ->- case y of {- Input -> Prelude.False;- _ -> Prelude.True};- Output -> Prelude.False}- eqVarKind :: VarKind -> VarKind -> Prelude.Bool eqVarKind s1 s2 = case s1 of {
LinearScan/Verify.hs view
@@ -15,7 +15,6 @@ import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Blocks as Blocks-import qualified LinearScan.Class as Class import qualified LinearScan.Contravariant as Contravariant import qualified LinearScan.Functor as Functor import qualified LinearScan.IntMap as IntMap@@ -128,46 +127,53 @@ data VerifiedSig a = Build_VerifiedSig RegStateDesc (IntMap.IntMap RegStateSig) (IntMap.IntMap- ([]- Resolve.ResolvingMoveSet)) - (IntMap.IntMap ((,) RegStateDescSet ([] AllocError))) a+ RegStateSig) + (IntMap.IntMap ([] Resolve.ResolvingMoveSet)) (IntMap.IntMap+ ((,) RegStateDescSet+ ([] AllocError))) a verDesc :: Prelude.Int -> (VerifiedSig a1) -> RegStateDesc verDesc maxReg v = case v of {- Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->- verDesc0}+ Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0+ verExt0 -> verDesc0} -verBlocks :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap RegStateSig-verBlocks maxReg v =+verInit :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap RegStateSig+verInit maxReg v = case v of {- Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->- verBlocks0}+ Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0+ verExt0 -> verInit0} +verFinal :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap RegStateSig+verFinal maxReg v =+ case v of {+ Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0+ verExt0 -> verFinal0}+ verMoves :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap ([] Resolve.ResolvingMoveSet) verMoves maxReg v = case v of {- Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->- verMoves0}+ Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0+ verExt0 -> verMoves0} verErrors :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap ((,) RegStateDescSet ([] AllocError)) verErrors maxReg v = case v of {- Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->- verErrors0}+ Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0+ verExt0 -> verErrors0} verExt :: Prelude.Int -> (VerifiedSig a1) -> a1 verExt maxReg v = case v of {- Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->- verExt0}+ Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0+ verExt0 -> verExt0} newVerifiedSig :: Prelude.Int -> a1 -> VerifiedSig a1 newVerifiedSig maxReg i = Build_VerifiedSig (newRegStateDesc maxReg) IntMap.emptyIntMap- IntMap.emptyIntMap IntMap.emptyIntMap i+ IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap i _verDesc :: Prelude.Int -> (Functor.Functor a2) -> (Contravariant.Contravariant a2) -> (RegStateDesc -> a2) ->@@ -178,38 +184,45 @@ _verState :: Prelude.Int -> (Functor.Functor a2) -> (RegStateDesc -> a2) -> (VerifiedSig a1) -> a2 _verState maxReg h f s =- Functor.fmap h (\x -> Build_VerifiedSig ( x) (verBlocks maxReg s)- (verMoves maxReg s) (verErrors maxReg s) (verExt maxReg s))- (f (verDesc maxReg s))+ Functor.fmap h (\x -> Build_VerifiedSig ( x) (verInit maxReg s)+ (verFinal maxReg s) (verMoves maxReg s) (verErrors maxReg s)+ (verExt maxReg s)) (f (verDesc maxReg s)) -_verBlocks :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap- RegStateSig) -> a2) -> (VerifiedSig a1) -> a2-_verBlocks maxReg h f s =+_verInit :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap+ RegStateSig) -> a2) -> (VerifiedSig a1) -> a2+_verInit maxReg h f s = Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s) x- (verMoves maxReg s) (verErrors maxReg s) (verExt maxReg s))- (f (verBlocks maxReg s))+ (verFinal maxReg s) (verMoves maxReg s) (verErrors maxReg s)+ (verExt maxReg s)) (f (verInit maxReg s)) +_verFinal :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap+ RegStateSig) -> a2) -> (VerifiedSig a1) -> a2+_verFinal maxReg h f s =+ Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)+ (verInit maxReg s) x (verMoves maxReg s) (verErrors maxReg s)+ (verExt maxReg s)) (f (verFinal maxReg s))+ _verMoves :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap ([] Resolve.ResolvingMoveSet)) -> a2) -> (VerifiedSig a1) -> a2 _verMoves maxReg h f s = Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)- (verBlocks maxReg s) x (verErrors maxReg s) (verExt maxReg s))- (f (verMoves maxReg s))+ (verInit maxReg s) (verFinal maxReg s) x (verErrors maxReg s)+ (verExt maxReg s)) (f (verMoves maxReg s)) _verErrors :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap ((,) RegStateDescSet ([] AllocError))) -> a2) -> (VerifiedSig a1) -> a2 _verErrors maxReg h f s = Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)- (verBlocks maxReg s) (verMoves maxReg s) x (verExt maxReg s))- (f (verErrors maxReg s))+ (verInit maxReg s) (verFinal maxReg s) (verMoves maxReg s) x+ (verExt maxReg s)) (f (verErrors maxReg s)) _verExt :: Prelude.Int -> (Functor.Functor a2) -> (a1 -> a2) -> (VerifiedSig a1) -> a2 _verExt maxReg h f s = Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)- (verBlocks maxReg s) (verMoves maxReg s) (verErrors maxReg s) x)- (f (verExt maxReg s))+ (verInit maxReg s) (verFinal maxReg s) (verMoves maxReg s)+ (verErrors maxReg s) x) (f (verExt maxReg s)) type Verified mType a a0 = State0.StateT (VerifiedSig a) mType a0 @@ -392,81 +405,34 @@ err = errorT maxReg mDict pc (VarNotResidentForReg var ( reg) res ((Prelude.succ) 0))} in- case res of {- Prelude.Just var' ->- Monad.unless (State0.coq_StateT_Monad mDict)- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce var)- (unsafeCoerce var')) err;- Prelude.Nothing ->- case useVerifier of {- VerifyEnabledStrict -> err;- _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})+ case useVerifier of {+ VerifyEnabledStrict ->+ case res of {+ Prelude.Just var' ->+ Monad.unless (State0.coq_StateT_Monad mDict)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce var)+ (unsafeCoerce var')) err;+ Prelude.Nothing -> err};+ _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}) (isResident maxReg mDict reg var)) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) -clearReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier ->- PhysReg -> Blocks.VarId -> Verified a1 a2 ()-clearReg maxReg mDict pc useVerifier reg var =- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- Monad.bind (State0.coq_StateT_Monad mDict) (\st ->- case Ssr.prop- (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)- (Lens.view (Lens.stepdownl' (unsafeCoerce (\_ -> residency)))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg))- (unsafeCoerce (Prelude.Just var))) of {- Prelude.Just _ ->- Lens.modifyStateT (\_ -> _verState maxReg)- (packRegState maxReg (Build_RegStateDesc- (Vector0.vmodify maxReg (rsAllocs maxReg st) reg- (Lens.set (\_ -> residency) Prelude.Nothing))- (rsStack maxReg st))) mDict;- Prelude.Nothing ->- let {- err = errorT maxReg mDict pc (VarNotResidentForReg var ( reg)- (Lens.view (Lens.stepdownl' (\_ -> residency))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg))- ((Prelude.succ) ((Prelude.succ) 0)))}- in- case useVerifier of {- VerifyEnabledStrict -> err;- _ ->- case Lens.view (Lens.stepdownl' (\_ -> residency))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {- Prelude.Just v -> err;- Prelude.Nothing ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})- (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))- (addMove maxReg mDict pc (Resolve.RSClearReg ( reg) var))- checkLiveness :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->- UseVerifier -> IntSet.IntSet -> Prelude.Bool -> Verified - a1 a2 ()-checkLiveness maxReg mDict pc useVerifier vars clearOut =+ UseVerifier -> IntSet.IntSet -> Verified a1 a2 ()+checkLiveness maxReg mDict pc useVerifier vars = case useVerifier of { VerifyEnabledStrict -> Monad.bind (State0.coq_StateT_Monad mDict) (\st ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- Monad.when (State0.coq_StateT_Monad mDict) clearOut- (Vector0.vfoldl_with_index maxReg (\reg act p ->- case Lens.view (Lens.stepdownl' (\_ -> residency)) p of {- Prelude.Just v ->- Monad.unless (State0.coq_StateT_Monad mDict)- (IntSet.coq_IntSet_member v vars)- (clearReg maxReg mDict pc useVerifier reg v);- Prelude.Nothing ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ()})- (Applicative.pure (State0.coq_StateT_Applicative mDict) ())- (rsAllocs maxReg st)))- (Monad.forM_ (State0.coq_StateT_Monad mDict)- (IntSet.coq_IntSet_toList vars) (\var ->- Monad.unless (State0.coq_StateT_Monad mDict)- (Vector0.vfoldl_with_index maxReg (\reg b p ->- (Prelude.||) b- (case Lens.view (Lens.stepdownl' (\_ -> residency)) p of {- Prelude.Just var0 -> Prelude.True;- Prelude.Nothing -> Prelude.False})) Prelude.False- (rsAllocs maxReg st))- (errorT maxReg mDict pc (VarNotResident var)))))+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ (IntSet.coq_IntSet_toList vars) (\var ->+ Monad.unless (State0.coq_StateT_Monad mDict)+ (Vector0.vfoldl_with_index maxReg (\reg b p ->+ (Prelude.||) b+ (case Lens.view (Lens.stepdownl' (\_ -> residency)) p of {+ Prelude.Just var0 -> Prelude.True;+ Prelude.Nothing -> Prelude.False})) Prelude.False+ (rsAllocs maxReg st))+ (errorT maxReg mDict pc (VarNotResident var)))) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict); _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()} @@ -479,7 +445,12 @@ Applicative.pure (State0.coq_StateT_Applicative mDict) (); VerifyEnabled -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- checkLiveness maxReg mDict pc useVerifier liveIns Prelude.True)+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\allocs ->+ Lens.applyStateT (\_ -> _verInit maxReg)+ (IntMap.coq_IntMap_insert bid allocs) mDict)+ (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict))+ (checkLiveness maxReg mDict pc useVerifier liveIns)) (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of { Prelude.Just fwds -> Monad.forM_ (State0.coq_StateT_Monad mDict)@@ -490,7 +461,7 @@ Lens.modifyStateT (\_ -> _verState maxReg) allocs mDict; Prelude.Nothing -> errorT maxReg mDict pc (UnknownPredecessorBlock bid pred)})- (Lens.use (Lens.stepdownl' (\_ -> _verBlocks maxReg)) mDict));+ (Lens.use (Lens.stepdownl' (\_ -> _verFinal maxReg)) mDict)); Prelude.Nothing -> case useVerifier of { VerifyEnabledStrict ->@@ -501,7 +472,12 @@ _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}); VerifyEnabledStrict -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- checkLiveness maxReg mDict pc useVerifier liveIns Prelude.True)+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\allocs ->+ Lens.applyStateT (\_ -> _verInit maxReg)+ (IntMap.coq_IntMap_insert bid allocs) mDict)+ (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict))+ (checkLiveness maxReg mDict pc useVerifier liveIns)) (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of { Prelude.Just fwds -> Monad.forM_ (State0.coq_StateT_Monad mDict)@@ -512,7 +488,7 @@ Lens.modifyStateT (\_ -> _verState maxReg) allocs mDict; Prelude.Nothing -> errorT maxReg mDict pc (UnknownPredecessorBlock bid pred)})- (Lens.use (Lens.stepdownl' (\_ -> _verBlocks maxReg)) mDict));+ (Lens.use (Lens.stepdownl' (\_ -> _verFinal maxReg)) mDict)); Prelude.Nothing -> case useVerifier of { VerifyEnabledStrict ->@@ -533,108 +509,97 @@ Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\allocs -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->- Lens.applyStateT (\_ -> _verBlocks maxReg)- (IntMap.coq_IntMap_insert bid allocs) mDict)- (Lens.modifyStateT (\_ -> _verState maxReg)- (packRegState maxReg (newRegStateDesc maxReg)) mDict))+ Lens.modifyStateT (\_ -> _verState maxReg)+ (packRegState maxReg (newRegStateDesc maxReg)) mDict)+ (Lens.applyStateT (\_ -> _verFinal maxReg)+ (IntMap.coq_IntMap_insert bid allocs) mDict)) (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict))- (checkLiveness maxReg mDict pc useVerifier liveOuts Prelude.False)}+ (checkLiveness maxReg mDict pc useVerifier liveOuts)} -verifyApplyAllocs :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo - a3 a1 a2) -> Blocks.OpId -> UseVerifier -> a1 -> ([]- ((,) Blocks.VarId PhysReg)) -> Verified a3 a4 ([] a2)-verifyApplyAllocs maxReg mDict oinfo pc useVerifier op allocs =- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict- (State0.coq_StateT_Monad mDict)- (Blocks.applyAllocs maxReg mDict oinfo op allocs))- (case useVerifier of {- VerifyDisabled ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ();- VerifyEnabled ->- Monad.forM_ (State0.coq_StateT_Monad mDict)- (List1.sortBy (\x y ->- UsePos.coq_VarKind_leq (Blocks.varKind maxReg x)- (Blocks.varKind maxReg y))- (Blocks.opRefs maxReg mDict oinfo op)) (\ref ->- case Blocks.varId maxReg ref of {- Prelude.Left reg ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ();- Prelude.Right var ->- case List1.maybeLookup Ssrnat.nat_eqType (unsafeCoerce allocs)- (unsafeCoerce var) of {- Prelude.Just reg ->- case Blocks.varKind maxReg ref of {- UsePos.Input ->- checkResidency maxReg mDict pc useVerifier reg var;- UsePos.Temp ->- checkReservation maxReg mDict pc useVerifier reg var;- UsePos.Output -> assignReg maxReg mDict pc useVerifier reg var};- Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}});- VerifyEnabledStrict ->- Monad.forM_ (State0.coq_StateT_Monad mDict)- (List1.sortBy (\x y ->- UsePos.coq_VarKind_leq (Blocks.varKind maxReg x)- (Blocks.varKind maxReg y))- (Blocks.opRefs maxReg mDict oinfo op)) (\ref ->- case Blocks.varId maxReg ref of {- Prelude.Left reg ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ();- Prelude.Right var ->- case List1.maybeLookup Ssrnat.nat_eqType (unsafeCoerce allocs)- (unsafeCoerce var) of {- Prelude.Just reg ->- case Blocks.varKind maxReg ref of {- UsePos.Input ->- checkResidency maxReg mDict pc useVerifier reg var;- UsePos.Temp ->- checkReservation maxReg mDict pc useVerifier reg var;- UsePos.Output -> assignReg maxReg mDict pc useVerifier reg var};- Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}})})+verifyAllocs :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 + a1 a2) -> Blocks.OpId -> UseVerifier -> a1 -> ([]+ ((,) ((,) Blocks.VarId UsePos.VarKind) PhysReg)) -> Verified+ a3 a4 ()+verifyAllocs maxReg mDict oinfo pc useVerifier op allocs =+ case useVerifier of {+ VerifyDisabled ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ VerifyEnabled ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ (Blocks.opRefs maxReg mDict oinfo op) (\ref ->+ case Blocks.varId maxReg ref of {+ Prelude.Left reg ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ Prelude.Right var ->+ case List1.maybeLookup+ (Eqtype.prod_eqType Ssrnat.nat_eqType+ UsePos.coq_VarKind_eqType) (unsafeCoerce allocs)+ (unsafeCoerce ((,) var (Blocks.varKind maxReg ref))) of {+ Prelude.Just reg ->+ case Blocks.varKind maxReg ref of {+ UsePos.Input -> checkResidency maxReg mDict pc useVerifier reg var;+ UsePos.Temp ->+ checkReservation maxReg mDict pc useVerifier reg var;+ UsePos.Output -> assignReg maxReg mDict pc useVerifier reg var};+ Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}});+ VerifyEnabledStrict ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ (Blocks.opRefs maxReg mDict oinfo op) (\ref ->+ case Blocks.varId maxReg ref of {+ Prelude.Left reg ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ Prelude.Right var ->+ case List1.maybeLookup+ (Eqtype.prod_eqType Ssrnat.nat_eqType+ UsePos.coq_VarKind_eqType) (unsafeCoerce allocs)+ (unsafeCoerce ((,) var (Blocks.varKind maxReg ref))) of {+ Prelude.Just reg ->+ case Blocks.varKind maxReg ref of {+ UsePos.Input -> checkResidency maxReg mDict pc useVerifier reg var;+ UsePos.Temp ->+ checkReservation maxReg mDict pc useVerifier reg var;+ UsePos.Output -> assignReg maxReg mDict pc useVerifier reg var};+ Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}})} verifyResolutions :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->- UseVerifier -> ([] Resolve.ResGraphEdge) -> Verified + UseVerifier -> ([] Resolve.ResolvingMove) -> Verified a1 a2 ([] Resolve.ResolvingMove) verifyResolutions maxReg mDict pc useVerifier moves = case useVerifier of { VerifyDisabled ->- Applicative.pure (State0.coq_StateT_Applicative mDict)- (Prelude.map (Resolve.resMove maxReg) moves);+ Applicative.pure (State0.coq_StateT_Applicative mDict) moves; _ -> Monad.forFoldM (State0.coq_StateT_Monad mDict) [] moves (\acc mv -> Monad.bind (State0.coq_StateT_Monad mDict) (\st ->- case Resolve.resMove maxReg mv of {+ case mv of { Resolve.Move fromReg fromVar toReg -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x3 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x4 ->- Applicative.pure (State0.coq_StateT_Applicative mDict)- (Seq.rcons acc (Resolve.resMove maxReg mv)))- (Monad.when (State0.coq_StateT_Monad mDict)- (Resolve.resGhost maxReg mv)- (releaseReg maxReg mDict pc useVerifier toReg- fromVar)))- (assignReg maxReg mDict pc useVerifier toReg fromVar))- (addMove maxReg mDict pc- (Resolve.weakenResolvingMove maxReg- (Resolve.resMove maxReg mv))))- (reserveReg maxReg mDict pc toReg fromVar))- (Monad.unless (State0.coq_StateT_Monad mDict)- (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)- (unsafeCoerce fromReg) (unsafeCoerce toReg))- (releaseReg maxReg mDict pc useVerifier fromReg fromVar)))- (checkResidency maxReg mDict pc useVerifier fromReg fromVar);+ Monad.bind (State0.coq_StateT_Monad mDict) (\check ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Seq.rcons acc mv))+ (case useVerifier of {+ VerifyEnabledStrict ->+ Monad.when (State0.coq_StateT_Monad mDict)+ (Maybe.isJust check)+ (assignReg maxReg mDict pc useVerifier toReg+ fromVar);+ _ ->+ assignReg maxReg mDict pc useVerifier toReg fromVar}))+ (isResident maxReg mDict fromReg fromVar))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg mv)))+ (reserveReg maxReg mDict pc toReg fromVar))+ (Monad.unless (State0.coq_StateT_Monad mDict)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)+ (unsafeCoerce fromReg) (unsafeCoerce toReg))+ (releaseReg maxReg mDict pc useVerifier fromReg fromVar)); Resolve.Transfer fromReg fromVar toReg -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->- Applicative.pure (State0.coq_StateT_Applicative mDict) acc)- (Monad.when (State0.coq_StateT_Monad mDict)- (Resolve.resGhost maxReg mv)- (releaseReg maxReg mDict pc useVerifier toReg fromVar)))+ Applicative.pure (State0.coq_StateT_Applicative mDict) acc) (reserveReg maxReg mDict pc toReg fromVar)) (Monad.unless (State0.coq_StateT_Monad mDict) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)@@ -647,10 +612,9 @@ Prelude.True -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> Applicative.pure (State0.coq_StateT_Applicative mDict)- (Seq.rcons acc (Resolve.resMove maxReg mv)))+ (Seq.rcons acc mv)) (addMove maxReg mDict pc- (Resolve.weakenResolvingMove maxReg- (Resolve.resMove maxReg mv)));+ (Resolve.weakenResolvingMove maxReg mv)); Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc}) (isResident maxReg mDict fromReg toSpillSlot))@@ -659,25 +623,15 @@ Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->- Applicative.pure (State0.coq_StateT_Applicative mDict)- (Seq.rcons acc (Resolve.resMove maxReg mv)))- (Monad.when (State0.coq_StateT_Monad mDict)- (Resolve.resGhost maxReg mv)- (releaseReg maxReg mDict pc useVerifier toReg- fromSpillSlot)))+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Seq.rcons acc mv)) (assignReg maxReg mDict pc useVerifier toReg fromSpillSlot)) (addMove maxReg mDict pc- (Resolve.weakenResolvingMove maxReg- (Resolve.resMove maxReg mv))))+ (Resolve.weakenResolvingMove maxReg mv))) (reserveReg maxReg mDict pc toReg fromSpillSlot); Resolve.AllocReg toVar toReg -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->- Applicative.pure (State0.coq_StateT_Applicative mDict) acc)- (Monad.when (State0.coq_StateT_Monad mDict)- (Resolve.resGhost maxReg mv)- (releaseReg maxReg mDict pc useVerifier toReg toVar)))+ Applicative.pure (State0.coq_StateT_Applicative mDict) acc) (reserveReg maxReg mDict pc toReg toVar); Resolve.FreeReg fromReg fromVar -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->@@ -687,10 +641,9 @@ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> Applicative.pure (State0.coq_StateT_Applicative mDict)- (Seq.rcons acc (Resolve.resMove maxReg mv)))+ (Seq.rcons acc mv)) (addMove maxReg mDict pc- (Resolve.weakenResolvingMove maxReg- (Resolve.resMove maxReg mv))))+ (Resolve.weakenResolvingMove maxReg mv))) (errorT maxReg mDict pc (LoopInResolvingMoves (Resolve.weakenResolvingMove maxReg x)))}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))}
linearscan.cabal view
@@ -1,5 +1,5 @@ name: linearscan-version: 0.8.0+version: 0.9.0 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3@@ -78,6 +78,7 @@ LinearScan.Logic LinearScan.Loops LinearScan.Main+ LinearScan.Maybe LinearScan.Monad LinearScan.Morph LinearScan.Nat@@ -106,6 +107,7 @@ Hask.Utils cpp-options: -DMAX_REG=4 -DREG_SIZE=8 ghc-options: -fno-warn-deprecated-flags+ other-extensions: Safe hs-source-dirs: . Hask/haskell build-depends: base >=4.7 && <5.0 , containers