diff --git a/LinearScan.hs b/LinearScan.hs --- a/LinearScan.hs +++ b/LinearScan.hs @@ -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 -> diff --git a/LinearScan/Allocate.hs b/LinearScan/Allocate.hs --- a/LinearScan/Allocate.hs +++ b/LinearScan/Allocate.hs @@ -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 { diff --git a/LinearScan/Assign.hs b/LinearScan/Assign.hs --- a/LinearScan/Assign.hs +++ b/LinearScan/Assign.hs @@ -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)) diff --git a/LinearScan/Blocks.hs b/LinearScan/Blocks.hs --- a/LinearScan/Blocks.hs +++ b/LinearScan/Blocks.hs @@ -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 diff --git a/LinearScan/Build.hs b/LinearScan/Build.hs --- a/LinearScan/Build.hs +++ b/LinearScan/Build.hs @@ -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) diff --git a/LinearScan/Eqtype.hs b/LinearScan/Eqtype.hs --- a/LinearScan/Eqtype.hs +++ b/LinearScan/Eqtype.hs @@ -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) diff --git a/LinearScan/IntMap.hs b/LinearScan/IntMap.hs --- a/LinearScan/IntMap.hs +++ b/LinearScan/IntMap.hs @@ -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 diff --git a/LinearScan/Interval.hs b/LinearScan/Interval.hs --- a/LinearScan/Interval.hs +++ b/LinearScan/Interval.hs @@ -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) diff --git a/LinearScan/List1.hs b/LinearScan/List1.hs --- a/LinearScan/List1.hs +++ b/LinearScan/List1.hs @@ -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 diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs --- a/LinearScan/Main.hs +++ b/LinearScan/Main.hs @@ -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 diff --git a/LinearScan/Maybe.hs b/LinearScan/Maybe.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Maybe.hs @@ -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} + diff --git a/LinearScan/Morph.hs b/LinearScan/Morph.hs --- a/LinearScan/Morph.hs +++ b/LinearScan/Morph.hs @@ -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 diff --git a/LinearScan/Prelude0.hs b/LinearScan/Prelude0.hs --- a/LinearScan/Prelude0.hs +++ b/LinearScan/Prelude0.hs @@ -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 - diff --git a/LinearScan/Range.hs b/LinearScan/Range.hs --- a/LinearScan/Range.hs +++ b/LinearScan/Range.hs @@ -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 diff --git a/LinearScan/Resolve.hs b/LinearScan/Resolve.hs --- a/LinearScan/Resolve.hs +++ b/LinearScan/Resolve.hs @@ -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'' diff --git a/LinearScan/Seq.hs b/LinearScan/Seq.hs --- a/LinearScan/Seq.hs +++ b/LinearScan/Seq.hs @@ -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 + diff --git a/LinearScan/Spill.hs b/LinearScan/Spill.hs --- a/LinearScan/Spill.hs +++ b/LinearScan/Spill.hs @@ -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 = \_ -> diff --git a/LinearScan/UsePos.hs b/LinearScan/UsePos.hs --- a/LinearScan/UsePos.hs +++ b/LinearScan/UsePos.hs @@ -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 { diff --git a/LinearScan/Verify.hs b/LinearScan/Verify.hs --- a/LinearScan/Verify.hs +++ b/LinearScan/Verify.hs @@ -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))} diff --git a/linearscan.cabal b/linearscan.cabal --- a/linearscan.cabal +++ b/linearscan.cabal @@ -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