linearscan 0.9.0 → 0.10.0
raw patch · 16 files changed
+1459/−552 lines, 16 files
Files
- LinearScan.hs +75/−54
- LinearScan/Allocate.hs +11/−12
- LinearScan/Assign.hs +380/−209
- LinearScan/Build.hs +9/−4
- LinearScan/Eqtype.hs +30/−0
- LinearScan/Interval.hs +18/−7
- LinearScan/Maybe.hs +6/−0
- LinearScan/Range.hs +0/−10
- LinearScan/Resolve.hs +446/−147
- LinearScan/ScanState.hs +2/−1
- LinearScan/Seq.hs +0/−4
- LinearScan/Trace.hs +1/−1
- LinearScan/UsePos.hs +32/−8
- LinearScan/Vector0.hs +20/−0
- LinearScan/Verify.hs +428/−94
- linearscan.cabal +1/−1
LinearScan.hs view
@@ -175,16 +175,19 @@ showUsePositions [u] = go u where go (LS.Build_UsePos n req v) =- (case v of LS.Input -> "i"- LS.Output -> "o"- LS.Temp -> "T")+ (case v of LS.Input -> "i"+ LS.InputOutput -> "I"+ LS.Output -> "o"+ LS.Temp -> "T") ++ show n ++ (if req then "" else "?") showUsePositions (u:us) = go u ++ " " ++ showUsePositions us where+ -- jww (2015-08-29): Remove this repetition. go (LS.Build_UsePos n req v) =- (case v of LS.Input -> "i"- LS.Output -> "o"- LS.Temp -> "T")+ (case v of LS.Input -> "i"+ LS.InputOutput -> "I"+ LS.Output -> "o"+ LS.Temp -> "T") ++ show n ++ (if req then "" else "?") toScanStateDesc :: LS.ScanStateDescSet -> ScanStateDesc@@ -241,7 +244,8 @@ -> (LS.OpId -> [op1] -> String) -> blk1 -> String-showBlock1 getops bid pos liveIns liveOuts loopInfo initials finals 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"@@ -265,20 +269,23 @@ " Outputs =>\n" ++ (unlines . map (replicate 12 ' ' ++) . lines . show $ xs))- ++ showops pos (getops b)+ ++ dotLayout ++ showops pos (getops b) where liveGen = liveOuts `S.difference` liveIns liveKill = liveIns `S.difference` liveOuts - branches =- let fwds = case M.lookup bid (forwardBranches loopInfo) of- Nothing -> ""- Just fwds' -> " Fwd" ++ show (S.toList fwds')- bwds = case M.lookup bid (backwardBranches loopInfo) of- Nothing -> ""- Just bwds' -> " Bkwd" ++ show (S.toList bwds')- in fwds ++ bwds+ fwds = maybe [] S.toList $ M.lookup bid (forwardBranches loopInfo)+ bwds = maybe [] S.toList $ M.lookup bid (backwardBranches loopInfo) + fwdsStr = case fwds of+ [] -> ""+ xs -> " Fwd" ++ show xs+ bwdsStr = case bwds of+ [] -> ""+ xs -> " Bkwd" ++ show xs++ branches = fwdsStr ++ bwdsStr+ loops = let hdr = if bid `elem` loopHeaderBlocks loopInfo then " Header"@@ -298,6 +305,18 @@ Just (_, d') -> " Depth=" ++ show d' in hdr ++ e ++ idxs ++ d + dotLayout =+ let leader = " DOT => " in+ (if null branches+ then leader ++ "L" ++ show bid ++ " [shape=box];\n"+ else "") +++ concatMap (\x -> leader ++ "L" ++ show x+ ++ " -> L" ++ show bid+ ++ " [color=green];\n") fwds +++ concatMap (\x -> leader ++ "L" ++ show x+ ++ " -> L" ++ show bid+ ++ " [color=red];\n") bwds+ opContext :: Int -> ScanStateDesc -> IntMap [LS.ResolvingMoveSet]@@ -345,34 +364,32 @@ (map Just (intervals sd))) (fixedIntervals sd) -showOp1' :: (a -> String)+showOps1 :: Bool+ -> LinearScan.OpInfo accType op1 op2 -> ScanStateDesc- -> Int -> IntMap [LS.ResolvingMoveSet] -> IntMap (LS.RegStateDescSet, [LS.AllocError])- -> a+ -> Int+ -> [op1] -> 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"+showOps1 _ _ _ _ _ _ [] = ""+showOps1 atBeg oinfo sd rms aerrs pos (o:os) =+ showOp1' ++ showOps1 False oinfo sd rms aerrs (pos+1) os where- leader = show pos ++ ": "+ showop = showOp1 oinfo+ here = pos*2+1+ leader = show here ++ ": " width = length leader- blank = replicate width ' ' -showOps1 :: LinearScan.OpInfo accType op1 op2- -> ScanStateDesc- -> IntMap [LS.ResolvingMoveSet]- -> IntMap (LS.RegStateDescSet, [LS.AllocError])- -> Int- -> [op1]- -> String-showOps1 _ _ _ _ _ [] = ""-showOps1 oinfo sd rms aerrs pos (o:os) =- showOp1' (showOp1 oinfo) sd (pos*2+1) rms aerrs o- ++ showOps1 oinfo sd rms aerrs (pos+1) os+ showOp1' =+ (if atBeg+ then leader ++ showop o ++ "\n"+ else "") +++ opContext width sd rms aerrs here +++ opContext width sd rms aerrs (here+1) +++ (if not atBeg+ then leader ++ showop o ++ "\n"+ else "") -- | From the point of view of this library, a basic block is nothing more -- than an ordered sequence of operations.@@ -400,7 +417,7 @@ where go _ [] = return "" go pos (b:bs) = do- bid <- LinearScan.blockId binfo b+ bid <- LinearScan.blockId binfo b let (liveIn, liveOut) = case M.lookup bid ls of Nothing -> (S.empty, S.empty) Just s -> (S.fromList (LS.blockLiveIn s),@@ -409,7 +426,7 @@ 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 ++)+ (showOps1 True oinfo sd rms aerrs) b ++) `liftM` go (pos + length (allops b)) bs fromBlockInfo :: Monad m@@ -454,28 +471,32 @@ else "r" ++ show reg ++ " -> " ++ info ++ "\n") ++ rest) "" (zip ([0..] :: [Int]) allocs) +showSplit :: Bool -> String+showSplit True = " {split}"+showSplit False = ""+ instance Show LS.ResolvingMoveSet where- show (LS.RSMove fr fv tr) =+ show (LS.RSMove fr fv tr) = "move (r" ++ show fr ++ " v" ++ show fv ++ ") " ++ "(r" ++ show tr ++ " v" ++ show fv ++ ")" show (LS.RSTransfer fr fv tr) = "<xfer> (r" ++ show fr ++ " v" ++ show fv ++ ") " ++ "(r" ++ show tr ++ " v" ++ show fv ++ ")"- show (LS.RSSpill fr tv) =- "spill (r" ++ show fr ++ " v" ++ show tv ++ ")"- show (LS.RSRestore fv tr) =- "restore (r" ++ show tr ++ " v" ++ show fv ++ ")"- show (LS.RSAllocReg fv tr) =- "<reserve> (r" ++ show tr ++ " v" ++ show fv ++ ")"- show (LS.RSFreeReg fr tv) =- "<release> (r" ++ show fr ++ " v" ++ show tv ++ ")"- show (LS.RSAssignReg fv tr) =+ show (LS.RSSpill fr tv b) =+ "spill (r" ++ show fr ++ " v" ++ show tv ++ ")" ++ showSplit b+ show (LS.RSRestore fv tr b) =+ "restore (r" ++ show tr ++ " v" ++ show fv ++ ")" ++ showSplit b+ show (LS.RSAllocReg fv tr b) =+ "<reserve> (r" ++ show tr ++ " v" ++ show fv ++ ")" ++ showSplit b+ show (LS.RSFreeReg fr tv b) =+ "<release> (r" ++ show fr ++ " v" ++ show tv ++ ")" ++ showSplit b+ show (LS.RSAssignReg fv tr) = "<assign> (r" ++ show tr ++ " v" ++ show fv ++ ")"- show (LS.RSClearReg fr tv) =+ show (LS.RSClearReg fr tv) = "<clear> (r" ++ show fr ++ " v" ++ show tv ++ ")"- show (LS.RSLooped x) = "!!!LOOPED! " ++ show x- -- show (LS.RSAllocStack tv) = "<AllocStack (v" ++ show tv ++ ")>"- -- show (LS.RSFreeStack fv) = "<FreeStack (v" ++ show fv ++ ")>"+ show (LS.RSLooped x) = "!!!LOOPED! " ++ show x+ show (LS.RSAllocStack tv) = "<alloc> (v" ++ show tv ++ ")"+ show (LS.RSFreeStack fv) = "<free> (v" ++ show fv ++ ")" showDetails :: Monad m => Details m blk1 blk2 op1 op2@@ -576,7 +597,7 @@ return (dets, Right blks) where reasonToStr r = case r of- LS.EOverlapsWithFixedInterval pos reg ->+ LS.EIntersectsWithFixedInterval pos reg -> "Current interval intersects with " ++ "fixed interval for register " ++ show reg ++ " at " ++ show pos LS.ESplitAssignedIntervalForReg xid reg pos ->
LinearScan/Allocate.hs view
@@ -58,17 +58,16 @@ type PhysReg = Prelude.Int -overlapsWithFixedInterval :: Prelude.Int -> ScanState.ScanStateDesc ->- PhysReg -> Morph.SState () ()- (Prelude.Maybe Prelude.Int)-overlapsWithFixedInterval maxReg pre reg =+intersectsWithFixedInterval :: Prelude.Int -> ScanState.ScanStateDesc ->+ PhysReg -> Morph.SState () ()+ (Prelude.Maybe Prelude.Int)+intersectsWithFixedInterval maxReg pre reg = Cursor.withCursor maxReg pre (\sd _ -> Context.ipure (case Vector0.vnth maxReg (ScanState.fixedIntervals maxReg sd) reg of { Prelude.Just i ->- Interval.intervalsOverlap- (Interval.getIntervalDesc ( (Cursor.curIntDetails maxReg sd)))- (Interval.getIntervalDesc ( i));+ Interval.intervalIntersectsWithSubrange+ ( (Cursor.curIntDetails maxReg sd)) ( i); Prelude.Nothing -> Prelude.Nothing})) updateRegisterPos :: Prelude.Int -> (Vector0.Vec (Prelude.Maybe Prelude.Int))@@ -97,9 +96,9 @@ case mint of { Prelude.Just int -> let {- op = Interval.intervalsOverlap- (Interval.getIntervalDesc ( int))- (Interval.getIntervalDesc d)}+ op = Interval.intervalIntersectsWithSubrange+ (Interval.getIntervalDesc d)+ (Interval.getIntervalDesc ( int))} in (,) (updateRegisterPos maxReg fup reg op) (Vector0.vreplace maxReg fai reg (Maybe.isJust op));@@ -237,12 +236,12 @@ (Morph.moveUnhandledToActive maxReg pre reg)) (case mloc of { Prelude.Just n ->- Context.context (Trace.EOverlapsWithFixedInterval n+ Context.context (Trace.EIntersectsWithFixedInterval n ( reg)) (Split.splitCurrentInterval maxReg pre (Split.BeforePos n)); Prelude.Nothing -> Context.ipure ()}))- (overlapsWithFixedInterval maxReg pre reg))+ (intersectsWithFixedInterval maxReg pre reg)) (Split.splitActiveIntervalForReg maxReg pre reg pos)) (Split.splitAnyInactiveIntervalForReg maxReg pre reg pos)})})
LinearScan/Assign.hs view
@@ -116,14 +116,18 @@ k (Blocks.moveOp maxReg mDict oinfo sreg svid dreg); Resolve.Transfer p v p0 -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing;- Resolve.Spill sreg svid ->+ Resolve.Spill sreg svid b -> k (Blocks.saveOp maxReg mDict oinfo sreg svid);- Resolve.Restore dvid dreg ->+ Resolve.Restore dvid dreg b -> k (Blocks.restoreOp maxReg mDict oinfo dvid dreg);- Resolve.AllocReg v p ->+ Resolve.AllocReg v p b -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing;- Resolve.FreeReg p v ->+ Resolve.FreeReg p v b -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing;+ Resolve.AllocStack v ->+ Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing;+ Resolve.FreeStack v ->+ Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.Looped r -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing})) @@ -140,10 +144,18 @@ (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Interval.ivar int)) vid)- ((Prelude.&&)- ((Prelude.<=) ((Prelude.succ) pos) (Interval.iend int))- ((Prelude.<=) ((Prelude.succ) (Interval.ibeg int))- ((Prelude.succ) ((Prelude.succ) pos))))) allocs)))+ (case Blocks.varKind maxReg v of {+ UsePos.Input ->+ (Prelude.&&)+ ((Prelude.<=) ((Prelude.succ) pos) (Interval.iend int))+ ((Prelude.<=) ((Prelude.succ) (Interval.ibeg int))+ ((Prelude.succ) pos));+ _ ->+ (Prelude.&&)+ ((Prelude.<=) ((Prelude.succ) ((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 -> []@@ -179,11 +191,14 @@ 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);+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ 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))+ (Verify.verifyTransitions maxReg mDict e allocs useVerifier moves b+ e); Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) []}} in@@ -204,7 +219,7 @@ (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)+ ((Prelude.succ) opid)) allocs useVerifier op regs)) injector) (transitions opid ((Prelude.succ) opid))) (transitions (Prelude.pred opid) opid)) (Lens.use (Lens.stepdownl' (\_ -> _verExt maxReg)) mDict)@@ -224,217 +239,373 @@ Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\bid ->- case IntMap.coq_IntMap_lookup bid liveSets of {- Prelude.Just bls ->- let {liveIns = LiveSets.blockLiveIn bls} in- let {liveOuts = LiveSets.blockLiveOut bls} in- case Maybe.fromMaybe ((,) [] [])- (IntMap.coq_IntMap_lookup bid mappings) of {- (,) begMoves endMoves ->- 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' ->- Monad.bind (State0.coq_StateT_Monad mDict)- (\bmoves ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\suxs ->+ case IntMap.coq_IntMap_lookup bid liveSets of {+ Prelude.Just bls ->+ let {liveIns = LiveSets.blockLiveIn bls} in+ let {liveOuts = LiveSets.blockLiveOut bls} in+ case let {+ fwds = Maybe.maybe [] IntSet.coq_IntSet_toList+ (IntMap.coq_IntMap_lookup bid+ (Loops.forwardBranches loops))}+ in+ let {+ bwds = Maybe.maybe [] IntSet.coq_IntSet_toList+ (IntMap.coq_IntMap_lookup bid+ (Loops.backwardBranches loops))}+ in+ (,)+ (List1.concat+ (Prelude.map (\b ->+ case IntMap.coq_IntMap_lookup b liveSets of {+ Prelude.Just x1 -> (:)+ (LiveSets.blockLastOpId x1) [];+ Prelude.Nothing -> []})+ ((Prelude.++) fwds bwds)))+ (List1.concat+ (Prelude.map (\b ->+ case IntMap.coq_IntMap_lookup b liveSets of {+ Prelude.Just x1 -> (:)+ (LiveSets.blockFirstOpId x1) [];+ Prelude.Nothing -> []}) suxs)) of {+ (,) froms tos ->+ case Maybe.fromMaybe ((,) [] [])+ (IntMap.coq_IntMap_lookup bid mappings) of {+ (,) begMoves endMoves ->+ let {+ k = setAllocations maxReg mDict oinfo useVerifier+ allocs}+ in+ let {+ resolutions = \pos toFroms moves ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ 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))+ (case toFroms of {+ Prelude.Left froms0 ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ froms0 (\b ->+ Verify.verifyTransitions maxReg mDict pos+ allocs useVerifier moves b ((Prelude.succ)+ pos));+ Prelude.Right tos0 ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ tos0 (\e ->+ Verify.verifyTransitions maxReg mDict pos+ allocs useVerifier moves pos e)})}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> Monad.bind (State0.coq_StateT_Monad mDict)- (\opsm' ->+ (\opsb' -> Monad.bind (State0.coq_StateT_Monad mDict)- (\opse' ->+ (\opid0 -> Monad.bind (State0.coq_StateT_Monad 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))}))+ (\bmoves ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\opsm' ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\z ->+ case z of {+ (,) opse' opid1 ->+ Monad.bind+ (State0.coq_StateT_Monad 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+ useVerifier bid liveOuts)})+ (case opse of {+ [] ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\opid1 ->+ Applicative.pure+ (State0.coq_StateT_Applicative+ mDict) ((,) [] opid1))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict);+ (:) e es ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\xs ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\opid1 ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\x2 ->+ Applicative.pure+ (State0.coq_StateT_Applicative+ mDict) ((,)+ ((Prelude.++) xs x2) opid1))+ (k+ (resolutions opid1+ (Prelude.Right tos)+ endMoves) (Seq.last e es)))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict))+ (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 opid0)+ (Prelude.Left froms) begMoves))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict)) (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- (Applicative.pure- (State0.coq_StateT_Applicative mDict) []))- opsb))- (Verify.verifyBlockBegin maxReg mDict opid useVerifier- bid liveIns loops)};- Prelude.Nothing ->- case Maybe.fromMaybe ((,) [] [])- (IntMap.coq_IntMap_lookup bid mappings) of {- (,) begMoves endMoves ->- 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' ->- Monad.bind (State0.coq_StateT_Monad mDict)- (\bmoves ->+ opsb))+ (Verify.verifyBlockBegin maxReg mDict opid+ useVerifier bid liveIns loops)}};+ Prelude.Nothing ->+ case let {+ fwds = Maybe.maybe [] IntSet.coq_IntSet_toList+ (IntMap.coq_IntMap_lookup bid+ (Loops.forwardBranches loops))}+ in+ let {+ bwds = Maybe.maybe [] IntSet.coq_IntSet_toList+ (IntMap.coq_IntMap_lookup bid+ (Loops.backwardBranches loops))}+ in+ (,)+ (List1.concat+ (Prelude.map (\b ->+ case IntMap.coq_IntMap_lookup b liveSets of {+ Prelude.Just x1 -> (:)+ (LiveSets.blockLastOpId x1) [];+ Prelude.Nothing -> []})+ ((Prelude.++) fwds bwds)))+ (List1.concat+ (Prelude.map (\b ->+ case IntMap.coq_IntMap_lookup b liveSets of {+ Prelude.Just x1 -> (:)+ (LiveSets.blockFirstOpId x1) [];+ Prelude.Nothing -> []}) suxs)) of {+ (,) froms tos ->+ case Maybe.fromMaybe ((,) [] [])+ (IntMap.coq_IntMap_lookup bid mappings) of {+ (,) begMoves endMoves ->+ let {+ k = setAllocations maxReg mDict oinfo useVerifier+ allocs}+ in+ let {+ resolutions = \pos toFroms moves ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ 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))+ (case toFroms of {+ Prelude.Left froms0 ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ froms0 (\b ->+ Verify.verifyTransitions maxReg mDict pos+ allocs useVerifier moves b ((Prelude.succ)+ pos));+ Prelude.Right tos0 ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ tos0 (\e ->+ Verify.verifyTransitions maxReg mDict pos+ allocs useVerifier moves pos e)})}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> Monad.bind (State0.coq_StateT_Monad mDict)- (\opsm' ->+ (\opsb' -> Monad.bind (State0.coq_StateT_Monad mDict)- (\opse' ->+ (\opid0 -> Monad.bind (State0.coq_StateT_Monad 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))}))+ (\bmoves ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\opsm' ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\z ->+ case z of {+ (,) opse' opid1 ->+ Monad.bind+ (State0.coq_StateT_Monad 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+ useVerifier bid IntSet.emptyIntSet)})+ (case opse of {+ [] ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\opid1 ->+ Applicative.pure+ (State0.coq_StateT_Applicative+ mDict) ((,) [] opid1))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict);+ (:) e es ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\xs ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\opid1 ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\x2 ->+ Applicative.pure+ (State0.coq_StateT_Applicative+ mDict) ((,)+ ((Prelude.++) xs x2) opid1))+ (k+ (resolutions opid1+ (Prelude.Right tos)+ endMoves) (Seq.last e es)))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict))+ (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 opid0)+ (Prelude.Left froms) begMoves))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict)) (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- (Applicative.pure- (State0.coq_StateT_Applicative mDict) []))- opsb))- (Verify.verifyBlockBegin maxReg mDict opid useVerifier- bid IntSet.emptyIntSet loops)}})+ 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.blockSuccessors mDict binfo blk))) (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict (State0.coq_StateT_Monad mDict) (Blocks.blockId mDict binfo blk)))
LinearScan/Build.hs view
@@ -203,14 +203,19 @@ Range.BoundedRange makeNewRange b pos e upos = Range.Build_RangeDesc- (case UsePos.uvar upos of {- UsePos.Input -> (Prelude.succ) (Ssrnat.double b);- _ -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos))})+ (case (Prelude.||)+ (Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (UsePos.uvar upos)) (unsafeCoerce UsePos.Input))+ (Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (UsePos.uvar upos))+ (unsafeCoerce UsePos.InputOutput)) of {+ Prelude.True -> (Prelude.succ) (Ssrnat.double b);+ Prelude.False -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos))}) (case UsePos.uvar upos of { 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 [])+ _ -> (Prelude.succ) (Ssrnat.double e)}) ((:) upos []) makeUsePos :: Prelude.Int -> Prelude.Int -> Blocks.VarInfo -> UsePos.UsePos makeUsePos maxReg pos var =
LinearScan/Eqtype.hs view
@@ -78,6 +78,36 @@ 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/Interval.hs view
@@ -70,13 +70,6 @@ (Prelude.&&) ((Prelude.<=) (intervalStart d) pos) ((Prelude.<=) ((Prelude.succ) pos) (intervalEnd d)) -intervalsOverlap :: IntervalDesc -> IntervalDesc -> Prelude.Maybe Prelude.Int-intervalsOverlap i j =- 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 ((,) Range.RangeDesc (Specif.Coq_sig2 UsePos.UsePos))@@ -190,6 +183,24 @@ Prelude.True -> ibeg y; Prelude.False -> ibeg x}); Prelude.False -> Prelude.Nothing}++intervalIntersectsWithSubrange :: IntervalDesc -> IntervalDesc ->+ Prelude.Maybe Prelude.Int+intervalIntersectsWithSubrange x y =+ let {+ go rs =+ case rs of {+ [] -> Prelude.Nothing;+ (:) r rs0 ->+ case (Prelude.&&)+ ((Prelude.<=) ((Prelude.succ) (ibeg x)) (Range.rend ( r)))+ ((Prelude.<=) ((Prelude.succ) (Range.rbeg ( r))) (iend x)) of {+ Prelude.True -> Prelude.Just+ (case (Prelude.<=) ((Prelude.succ) (ibeg x)) (Range.rbeg ( r)) of {+ Prelude.True -> Range.rbeg ( r);+ Prelude.False -> ibeg x});+ Prelude.False -> go rs0}}}+ in go ( (rds y)) divideIntervalRanges :: IntervalDesc -> Prelude.Int -> ((,) Range.SortedRanges Range.SortedRanges)
LinearScan/Maybe.hs view
@@ -19,6 +19,12 @@ Prelude.Just z -> z; Prelude.Nothing -> x} +maybe :: a1 -> (a2 -> a1) -> (Prelude.Maybe a2) -> a1+maybe x f my =+ case my of {+ Prelude.Just z -> f z;+ Prelude.Nothing -> x}+ isJust :: (Prelude.Maybe a1) -> Prelude.Bool isJust x = case x of {
LinearScan/Range.hs view
@@ -133,16 +133,6 @@ transportSortedRanges b pos rp = rp -rangesIntersect :: RangeDesc -> RangeDesc -> Prelude.Maybe Prelude.Int-rangesIntersect x y =- case (Prelude.&&) ((Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y))- ((Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x)) of {- Prelude.True -> Prelude.Just- (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {- Prelude.True -> rbeg y;- Prelude.False -> rbeg x});- Prelude.False -> Prelude.Nothing}- findRangeUsePos :: RangeDesc -> (UsePos.UsePos -> Prelude.Bool) -> Prelude.Maybe UsePos.UsePos findRangeUsePos rd f =
LinearScan/Resolve.hs view
@@ -57,38 +57,47 @@ data ResolvingMove = Move PhysReg Blocks.VarId PhysReg | Transfer PhysReg Blocks.VarId PhysReg- | Spill PhysReg Blocks.VarId- | Restore Blocks.VarId PhysReg- | AllocReg Blocks.VarId PhysReg- | FreeReg PhysReg Blocks.VarId+ | Spill PhysReg Blocks.VarId Prelude.Bool+ | Restore Blocks.VarId PhysReg Prelude.Bool+ | AllocReg Blocks.VarId PhysReg Prelude.Bool+ | FreeReg PhysReg Blocks.VarId Prelude.Bool+ | AllocStack Blocks.VarId+ | FreeStack Blocks.VarId | Looped ResolvingMove coq_ResolvingMove_rect :: Prelude.Int -> (PhysReg -> Blocks.VarId -> PhysReg -> a1) -> (PhysReg -> Blocks.VarId -> PhysReg ->- a1) -> (PhysReg -> Blocks.VarId -> a1) ->- (Blocks.VarId -> PhysReg -> a1) -> (Blocks.VarId ->- PhysReg -> a1) -> (PhysReg -> Blocks.VarId -> a1)+ a1) -> (PhysReg -> Blocks.VarId -> Prelude.Bool ->+ a1) -> (Blocks.VarId -> PhysReg -> Prelude.Bool ->+ a1) -> (Blocks.VarId -> PhysReg -> Prelude.Bool ->+ a1) -> (PhysReg -> Blocks.VarId -> Prelude.Bool ->+ a1) -> (Blocks.VarId -> a1) -> (Blocks.VarId -> a1) -> (ResolvingMove -> a1 -> a1) -> ResolvingMove -> a1-coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 r =+coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 f6 f7 r = case r of { Move p v p0 -> f p v p0; Transfer p v p0 -> f0 p v p0;- Spill p v -> f1 p v;- Restore v p -> f2 v p;- AllocReg v p -> f3 v p;- FreeReg p v -> f4 p v;- Looped r0 -> f5 r0 (coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 r0)}+ Spill p v b -> f1 p v b;+ Restore v p b -> f2 v p b;+ AllocReg v p b -> f3 v p b;+ FreeReg p v b -> f4 p v b;+ AllocStack v -> f5 v;+ FreeStack v -> f6 v;+ Looped r0 ->+ f7 r0 (coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 f6 f7 r0)} data ResolvingMoveSet = RSMove Prelude.Int Blocks.VarId Prelude.Int | RSTransfer Prelude.Int Blocks.VarId Prelude.Int- | RSSpill Prelude.Int Blocks.VarId- | RSRestore Blocks.VarId Prelude.Int- | RSAllocReg Blocks.VarId Prelude.Int- | RSFreeReg Prelude.Int Blocks.VarId+ | RSSpill Prelude.Int Blocks.VarId Prelude.Bool+ | RSRestore Blocks.VarId Prelude.Int Prelude.Bool+ | RSAllocReg Blocks.VarId Prelude.Int Prelude.Bool+ | RSFreeReg Prelude.Int Blocks.VarId Prelude.Bool | RSAssignReg Blocks.VarId Prelude.Int | RSClearReg Prelude.Int Blocks.VarId+ | RSAllocStack Blocks.VarId+ | RSFreeStack Blocks.VarId | RSLooped ResolvingMoveSet weakenResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMoveSet@@ -96,10 +105,12 @@ case x of { Move fr fv tr -> RSMove ( fr) fv ( tr); Transfer fr fv tr -> RSTransfer ( fr) fv ( tr);- Spill fr tv -> RSSpill ( fr) tv;- Restore fv tr -> RSRestore fv ( tr);- AllocReg fv tr -> RSAllocReg fv ( tr);- FreeReg fr tv -> RSFreeReg ( fr) tv;+ Spill fr tv b -> RSSpill ( fr) tv b;+ Restore fv tr b -> RSRestore fv ( tr) b;+ AllocReg fv tr b -> RSAllocReg fv ( tr) b;+ FreeReg fr tv b -> RSFreeReg ( fr) tv b;+ AllocStack tv -> RSAllocStack tv;+ FreeStack fv -> RSFreeStack fv; Looped x0 -> RSLooped (weakenResolvingMove maxReg x0)} eqResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMove ->@@ -130,42 +141,64 @@ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce tr2))); _ -> Prelude.False};- Spill fr1 fv1 ->+ Spill fr1 fv1 b1 -> case s2 of {- Spill fr2 fv2 ->+ Spill fr2 fv2 b2 -> (Prelude.&&) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce fr2))- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)- (unsafeCoerce fv2));+ ((Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)+ (unsafeCoerce fv2))+ (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1)+ (unsafeCoerce b2))); _ -> Prelude.False};- Restore tv1 tr1 ->+ Restore tv1 tr1 b1 -> case s2 of {- Restore tv2 tr2 ->+ Restore tv2 tr2 b2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce tv2))- (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)- (unsafeCoerce tr2));+ ((Prelude.&&)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)+ (unsafeCoerce tr2))+ (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1)+ (unsafeCoerce b2))); _ -> Prelude.False};- AllocReg fv1 tr1 ->+ AllocReg fv1 tr1 b1 -> case s2 of {- AllocReg fv2 tr2 ->+ AllocReg fv2 tr2 b2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce fv2))- (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)- (unsafeCoerce tr2));+ ((Prelude.&&)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)+ (unsafeCoerce tr2))+ (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1)+ (unsafeCoerce b2))); _ -> Prelude.False};- FreeReg fr1 tv1 ->+ FreeReg fr1 tv1 b1 -> case s2 of {- FreeReg fr2 tv2 ->+ FreeReg fr2 tv2 b2 -> (Prelude.&&) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce fr2))- (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)- (unsafeCoerce tv2));+ ((Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)+ (unsafeCoerce tv2))+ (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1)+ (unsafeCoerce b2))); _ -> Prelude.False};+ AllocStack tv1 ->+ case s2 of {+ AllocStack tv2 ->+ Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce tv2);+ _ -> Prelude.False};+ FreeStack fv1 ->+ case s2 of {+ FreeStack fv2 ->+ Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce fv2);+ _ -> Prelude.False}; Looped x -> case s2 of { Looped y -> eqResolvingMove maxReg x y;@@ -251,19 +284,23 @@ Ssrbool.ReflectF -> _evar_0_0 __}} in let {_evar_0_0 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_1 = \fr2 fv2 -> Ssrbool.ReflectF} in- let {_evar_0_2 = \tv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_3 = \fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_4 = \fr2 tv2 -> Ssrbool.ReflectF} in- let {_evar_0_5 = \y -> Ssrbool.ReflectF} in+ let {_evar_0_1 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_2 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_3 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> unsafeCoerce _evar_0_ x x0 x1; Transfer x x0 x1 -> _evar_0_0 x x0 x1;- Spill x x0 -> _evar_0_1 x x0;- Restore x x0 -> _evar_0_2 x x0;- AllocReg x x0 -> _evar_0_3 x x0;- FreeReg x x0 -> _evar_0_4 x x0;- Looped x -> _evar_0_5 x}}+ Spill x x0 x1 -> _evar_0_1 x x0 x1;+ Restore x x0 x1 -> _evar_0_2 x x0 x1;+ AllocReg x x0 x1 -> _evar_0_3 x x0 x1;+ FreeReg x x0 x1 -> _evar_0_4 x x0 x1;+ AllocStack x -> _evar_0_5 x;+ FreeStack x -> _evar_0_6 x;+ Looped x -> _evar_0_7 x}} in let { _evar_0_0 = \fr1 fv1 tr1 _top_assumption_0 ->@@ -345,34 +382,60 @@ Ssrbool.ReflectT -> _evar_0_1 __; Ssrbool.ReflectF -> _evar_0_2 __}} in- let {_evar_0_2 = \fr2 fv2 -> Ssrbool.ReflectF} in- let {_evar_0_3 = \tv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_4 = \fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in- let {_evar_0_6 = \y -> Ssrbool.ReflectF} in+ let {_evar_0_2 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_3 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_0 x x0 x1; Transfer x x0 x1 -> unsafeCoerce _evar_0_1 x x0 x1;- Spill x x0 -> _evar_0_2 x x0;- Restore x x0 -> _evar_0_3 x x0;- AllocReg x x0 -> _evar_0_4 x x0;- FreeReg x x0 -> _evar_0_5 x x0;- Looped x -> _evar_0_6 x}}+ Spill x x0 x1 -> _evar_0_2 x x0 x1;+ Restore x x0 x1 -> _evar_0_3 x x0 x1;+ AllocReg x x0 x1 -> _evar_0_4 x x0 x1;+ FreeReg x x0 x1 -> _evar_0_5 x x0 x1;+ AllocStack x -> _evar_0_6 x;+ FreeStack x -> _evar_0_7 x;+ Looped x -> _evar_0_8 x}} in let {- _evar_0_1 = \fr1 fv1 _top_assumption_0 ->+ _evar_0_1 = \fr1 fv1 b1 _top_assumption_0 -> let {_evar_0_1 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {- _evar_0_3 = \fr2 fv2 ->+ _evar_0_3 = \fr2 fv2 b2 -> let { _evar_0_3 = \_ -> let { _evar_0_3 = let { _evar_0_3 = \_ ->- let {_evar_0_3 = Ssrbool.ReflectT} in _evar_0_3}+ let {+ _evar_0_3 = let {+ _evar_0_3 = \_ ->+ let {_evar_0_3 = Ssrbool.ReflectT} in+ _evar_0_3}+ in+ let {_evar_0_4 = \_ -> Ssrbool.ReflectF}+ in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_3 __;+ Ssrbool.ReflectF -> _evar_0_4 __}}+ in+ _evar_0_3} in- let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in+ let {+ _evar_0_4 = \_ ->+ let {+ _evar_0_4 = \_ ->+ let {_evar_0_4 = Ssrbool.ReflectF} in _evar_0_4}+ in+ let {_evar_0_5 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_4 __;+ Ssrbool.ReflectF -> _evar_0_5 __}}+ in case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}}@@ -382,9 +445,30 @@ let { _evar_0_4 = \_ -> let {- _evar_0_4 = \_ -> let {_evar_0_4 = Ssrbool.ReflectF} in _evar_0_4}+ _evar_0_4 = \_ ->+ let {+ _evar_0_4 = let {+ _evar_0_4 = \_ ->+ let {_evar_0_4 = Ssrbool.ReflectF} in _evar_0_4}+ in+ let {_evar_0_5 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_4 __;+ Ssrbool.ReflectF -> _evar_0_5 __}}+ in+ _evar_0_4} in- let {_evar_0_5 = \_ -> Ssrbool.ReflectF} in+ let {+ _evar_0_5 = \_ ->+ let {+ _evar_0_5 = \_ ->+ let {_evar_0_5 = Ssrbool.ReflectF} in _evar_0_5}+ in+ let {_evar_0_6 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_5 __;+ Ssrbool.ReflectF -> _evar_0_6 __}}+ in case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { Ssrbool.ReflectT -> _evar_0_4 __; Ssrbool.ReflectF -> _evar_0_5 __}}@@ -393,34 +477,60 @@ Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}} in- let {_evar_0_4 = \tv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_5 = \fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in- let {_evar_0_7 = \y -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_9 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_1 x x0 x1; Transfer x x0 x1 -> _evar_0_2 x x0 x1;- Spill x x0 -> unsafeCoerce _evar_0_3 x x0;- Restore x x0 -> _evar_0_4 x x0;- AllocReg x x0 -> _evar_0_5 x x0;- FreeReg x x0 -> _evar_0_6 x x0;- Looped x -> _evar_0_7 x}}+ Spill x x0 x1 -> unsafeCoerce _evar_0_3 x x0 x1;+ Restore x x0 x1 -> _evar_0_4 x x0 x1;+ AllocReg x x0 x1 -> _evar_0_5 x x0 x1;+ FreeReg x x0 x1 -> _evar_0_6 x x0 x1;+ AllocStack x -> _evar_0_7 x;+ FreeStack x -> _evar_0_8 x;+ Looped x -> _evar_0_9 x}} in let {- _evar_0_2 = \tv1 tr1 _top_assumption_0 ->+ _evar_0_2 = \tv1 tr1 b1 _top_assumption_0 -> let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_4 = \fr2 fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {- _evar_0_5 = \tv2 tr2 ->+ _evar_0_5 = \tv2 tr2 b2 -> let { _evar_0_5 = \_ -> let { _evar_0_5 = let { _evar_0_5 = \_ ->- let {_evar_0_5 = Ssrbool.ReflectT} in _evar_0_5}+ let {+ _evar_0_5 = let {+ _evar_0_5 = \_ ->+ let {_evar_0_5 = Ssrbool.ReflectT} in+ _evar_0_5}+ in+ let {_evar_0_6 = \_ -> Ssrbool.ReflectF}+ in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_5 __;+ Ssrbool.ReflectF -> _evar_0_6 __}}+ in+ _evar_0_5} in- let {_evar_0_6 = \_ -> Ssrbool.ReflectF} in+ let {+ _evar_0_6 = \_ ->+ let {+ _evar_0_6 = \_ ->+ let {_evar_0_6 = Ssrbool.ReflectF} in _evar_0_6}+ in+ let {_evar_0_7 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_6 __;+ Ssrbool.ReflectF -> _evar_0_7 __}}+ in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_5 __; Ssrbool.ReflectF -> _evar_0_6 __}}@@ -430,9 +540,30 @@ let { _evar_0_6 = \_ -> let {- _evar_0_6 = \_ -> let {_evar_0_6 = Ssrbool.ReflectF} in _evar_0_6}+ _evar_0_6 = \_ ->+ let {+ _evar_0_6 = let {+ _evar_0_6 = \_ ->+ let {_evar_0_6 = Ssrbool.ReflectF} in _evar_0_6}+ in+ let {_evar_0_7 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_6 __;+ Ssrbool.ReflectF -> _evar_0_7 __}}+ in+ _evar_0_6} in- let {_evar_0_7 = \_ -> Ssrbool.ReflectF} in+ let {+ _evar_0_7 = \_ ->+ let {+ _evar_0_7 = \_ ->+ let {_evar_0_7 = Ssrbool.ReflectF} in _evar_0_7}+ in+ let {_evar_0_8 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_7 __;+ Ssrbool.ReflectF -> _evar_0_8 __}}+ in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_6 __; Ssrbool.ReflectF -> _evar_0_7 __}}@@ -441,34 +572,60 @@ Ssrbool.ReflectT -> _evar_0_5 __; Ssrbool.ReflectF -> _evar_0_6 __}} in- let {_evar_0_6 = \fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_7 = \fr2 tv2 -> Ssrbool.ReflectF} in- let {_evar_0_8 = \y -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_9 = \fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_10 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_2 x x0 x1; Transfer x x0 x1 -> _evar_0_3 x x0 x1;- Spill x x0 -> _evar_0_4 x x0;- Restore x x0 -> unsafeCoerce _evar_0_5 x x0;- AllocReg x x0 -> _evar_0_6 x x0;- FreeReg x x0 -> _evar_0_7 x x0;- Looped x -> _evar_0_8 x}}+ Spill x x0 x1 -> _evar_0_4 x x0 x1;+ Restore x x0 x1 -> unsafeCoerce _evar_0_5 x x0 x1;+ AllocReg x x0 x1 -> _evar_0_6 x x0 x1;+ FreeReg x x0 x1 -> _evar_0_7 x x0 x1;+ AllocStack x -> _evar_0_8 x;+ FreeStack x -> _evar_0_9 x;+ Looped x -> _evar_0_10 x}} in let {- _evar_0_3 = \fv1 tr1 _top_assumption_0 ->+ _evar_0_3 = \fv1 tr1 b1 _top_assumption_0 -> let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_5 = \fr2 fv2 -> Ssrbool.ReflectF} in- let {_evar_0_6 = \tv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let {- _evar_0_7 = \fv2 tr2 ->+ _evar_0_7 = \fv2 tr2 b2 -> let { _evar_0_7 = \_ -> let { _evar_0_7 = let { _evar_0_7 = \_ ->- let {_evar_0_7 = Ssrbool.ReflectT} in _evar_0_7}+ let {+ _evar_0_7 = let {+ _evar_0_7 = \_ ->+ let {_evar_0_7 = Ssrbool.ReflectT} in+ _evar_0_7}+ in+ let {_evar_0_8 = \_ -> Ssrbool.ReflectF}+ in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_7 __;+ Ssrbool.ReflectF -> _evar_0_8 __}}+ in+ _evar_0_7} in- let {_evar_0_8 = \_ -> Ssrbool.ReflectF} in+ let {+ _evar_0_8 = \_ ->+ let {+ _evar_0_8 = \_ ->+ let {_evar_0_8 = Ssrbool.ReflectF} in _evar_0_8}+ in+ let {_evar_0_9 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_8 __;+ Ssrbool.ReflectF -> _evar_0_9 __}}+ in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_7 __; Ssrbool.ReflectF -> _evar_0_8 __}}@@ -478,9 +635,30 @@ let { _evar_0_8 = \_ -> let {- _evar_0_8 = \_ -> let {_evar_0_8 = Ssrbool.ReflectF} in _evar_0_8}+ _evar_0_8 = \_ ->+ let {+ _evar_0_8 = let {+ _evar_0_8 = \_ ->+ let {_evar_0_8 = Ssrbool.ReflectF} in _evar_0_8}+ in+ let {_evar_0_9 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_8 __;+ Ssrbool.ReflectF -> _evar_0_9 __}}+ in+ _evar_0_8} in- let {_evar_0_9 = \_ -> Ssrbool.ReflectF} in+ let {+ _evar_0_9 = \_ ->+ let {+ _evar_0_9 = \_ ->+ let {_evar_0_9 = Ssrbool.ReflectF} in _evar_0_9}+ in+ let {_evar_0_10 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_9 __;+ Ssrbool.ReflectF -> _evar_0_10 __}}+ in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_8 __; Ssrbool.ReflectF -> _evar_0_9 __}}@@ -489,34 +667,60 @@ Ssrbool.ReflectT -> _evar_0_7 __; Ssrbool.ReflectF -> _evar_0_8 __}} in- let {_evar_0_8 = \fr2 tv2 -> Ssrbool.ReflectF} in- let {_evar_0_9 = \y -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_9 = \tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_10 = \fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_11 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_3 x x0 x1; Transfer x x0 x1 -> _evar_0_4 x x0 x1;- Spill x x0 -> _evar_0_5 x x0;- Restore x x0 -> _evar_0_6 x x0;- AllocReg x x0 -> unsafeCoerce _evar_0_7 x x0;- FreeReg x x0 -> _evar_0_8 x x0;- Looped x -> _evar_0_9 x}}+ Spill x x0 x1 -> _evar_0_5 x x0 x1;+ Restore x x0 x1 -> _evar_0_6 x x0 x1;+ AllocReg x x0 x1 -> unsafeCoerce _evar_0_7 x x0 x1;+ FreeReg x x0 x1 -> _evar_0_8 x x0 x1;+ AllocStack x -> _evar_0_9 x;+ FreeStack x -> _evar_0_10 x;+ Looped x -> _evar_0_11 x}} in let {- _evar_0_4 = \fr1 tv1 _top_assumption_0 ->+ _evar_0_4 = \fr1 tv1 b1 _top_assumption_0 -> let {_evar_0_4 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_6 = \fr2 fv2 -> Ssrbool.ReflectF} in- let {_evar_0_7 = \tv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_8 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in let {- _evar_0_9 = \fr2 tv2 ->+ _evar_0_9 = \fr2 tv2 b2 -> let { _evar_0_9 = \_ -> let { _evar_0_9 = let { _evar_0_9 = \_ ->- let {_evar_0_9 = Ssrbool.ReflectT} in _evar_0_9}+ let {+ _evar_0_9 = let {+ _evar_0_9 = \_ ->+ let {_evar_0_9 = Ssrbool.ReflectT} in+ _evar_0_9}+ in+ let {_evar_0_10 = \_ -> Ssrbool.ReflectF}+ in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_9 __;+ Ssrbool.ReflectF -> _evar_0_10 __}}+ in+ _evar_0_9} in- let {_evar_0_10 = \_ -> Ssrbool.ReflectF} in+ let {+ _evar_0_10 = \_ ->+ let {+ _evar_0_10 = \_ ->+ let {_evar_0_10 = Ssrbool.ReflectF} in _evar_0_10}+ in+ let {_evar_0_11 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_10 __;+ Ssrbool.ReflectF -> _evar_0_11 __}}+ in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_9 __; Ssrbool.ReflectF -> _evar_0_10 __}}@@ -527,9 +731,29 @@ _evar_0_10 = \_ -> let { _evar_0_10 = \_ ->- let {_evar_0_10 = Ssrbool.ReflectF} in _evar_0_10}+ let {+ _evar_0_10 = let {+ _evar_0_10 = \_ ->+ let {_evar_0_10 = Ssrbool.ReflectF} in _evar_0_10}+ in+ let {_evar_0_11 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_10 __;+ Ssrbool.ReflectF -> _evar_0_11 __}}+ in+ _evar_0_10} in- let {_evar_0_11 = \_ -> Ssrbool.ReflectF} in+ let {+ _evar_0_11 = \_ ->+ let {+ _evar_0_11 = \_ ->+ let {_evar_0_11 = Ssrbool.ReflectF} in _evar_0_11}+ in+ let {_evar_0_12 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_11 __;+ Ssrbool.ReflectF -> _evar_0_12 __}}+ in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_10 __; Ssrbool.ReflectF -> _evar_0_11 __}}@@ -538,46 +762,117 @@ Ssrbool.ReflectT -> _evar_0_9 __; Ssrbool.ReflectF -> _evar_0_10 __}} in- let {_evar_0_10 = \y -> Ssrbool.ReflectF} in+ let {_evar_0_10 = \tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_11 = \fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_12 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_4 x x0 x1; Transfer x x0 x1 -> _evar_0_5 x x0 x1;- Spill x x0 -> _evar_0_6 x x0;- Restore x x0 -> _evar_0_7 x x0;- AllocReg x x0 -> _evar_0_8 x x0;- FreeReg x x0 -> unsafeCoerce _evar_0_9 x x0;- Looped x -> _evar_0_10 x}}+ Spill x x0 x1 -> _evar_0_6 x x0 x1;+ Restore x x0 x1 -> _evar_0_7 x x0 x1;+ AllocReg x x0 x1 -> _evar_0_8 x x0 x1;+ FreeReg x x0 x1 -> unsafeCoerce _evar_0_9 x x0 x1;+ AllocStack x -> _evar_0_10 x;+ FreeStack x -> _evar_0_11 x;+ Looped x -> _evar_0_12 x}} in let {- _evar_0_5 = \x iHx _top_assumption_0 ->+ _evar_0_5 = \tv1 _top_assumption_0 -> let {_evar_0_5 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_7 = \fr2 fv2 -> Ssrbool.ReflectF} in- let {_evar_0_8 = \tv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_9 = \fv2 tr2 -> Ssrbool.ReflectF} in- let {_evar_0_10 = \fr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_9 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_10 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in let {- _evar_0_11 = \y ->- let {iHx0 = iHx y} in- let {_evar_0_11 = \_ -> Ssrbool.ReflectT} in+ _evar_0_11 = \tv2 ->+ let {+ _evar_0_11 = \_ -> let {_evar_0_11 = Ssrbool.ReflectT} in _evar_0_11}+ in let {_evar_0_12 = \_ -> Ssrbool.ReflectF} in- case iHx0 of {+ case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_11 __; Ssrbool.ReflectF -> _evar_0_12 __}} in+ let {_evar_0_12 = \fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_13 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of {- Move x0 x1 x2 -> _evar_0_5 x0 x1 x2;- Transfer x0 x1 x2 -> _evar_0_6 x0 x1 x2;- Spill x0 x1 -> _evar_0_7 x0 x1;- Restore x0 x1 -> _evar_0_8 x0 x1;- AllocReg x0 x1 -> _evar_0_9 x0 x1;- FreeReg x0 x1 -> _evar_0_10 x0 x1;- Looped x0 -> _evar_0_11 x0}}+ Move x x0 x1 -> _evar_0_5 x x0 x1;+ Transfer x x0 x1 -> _evar_0_6 x x0 x1;+ Spill x x0 x1 -> _evar_0_7 x x0 x1;+ Restore x x0 x1 -> _evar_0_8 x x0 x1;+ AllocReg x x0 x1 -> _evar_0_9 x x0 x1;+ FreeReg x x0 x1 -> _evar_0_10 x x0 x1;+ AllocStack x -> unsafeCoerce _evar_0_11 x;+ FreeStack x -> _evar_0_12 x;+ Looped x -> _evar_0_13 x}} in+ let {+ _evar_0_6 = \fv1 _top_assumption_0 ->+ let {_evar_0_6 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_9 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_10 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_11 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_12 = \tv2 -> Ssrbool.ReflectF} in+ let {+ _evar_0_13 = \fv2 ->+ let {+ _evar_0_13 = \_ -> let {_evar_0_13 = Ssrbool.ReflectT} in _evar_0_13}+ in+ let {_evar_0_14 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {+ Ssrbool.ReflectT -> _evar_0_13 __;+ Ssrbool.ReflectF -> _evar_0_14 __}}+ in+ let {_evar_0_14 = \y -> Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ Move x x0 x1 -> _evar_0_6 x x0 x1;+ Transfer x x0 x1 -> _evar_0_7 x x0 x1;+ Spill x x0 x1 -> _evar_0_8 x x0 x1;+ Restore x x0 x1 -> _evar_0_9 x x0 x1;+ AllocReg x x0 x1 -> _evar_0_10 x x0 x1;+ FreeReg x x0 x1 -> _evar_0_11 x x0 x1;+ AllocStack x -> _evar_0_12 x;+ FreeStack x -> unsafeCoerce _evar_0_13 x;+ Looped x -> _evar_0_14 x}}+ in+ let {+ _evar_0_7 = \x iHx _top_assumption_0 ->+ let {_evar_0_7 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_9 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_10 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_11 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_12 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in+ let {_evar_0_13 = \tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_14 = \fv2 -> Ssrbool.ReflectF} in+ let {+ _evar_0_15 = \y ->+ let {iHx0 = iHx y} in+ let {_evar_0_15 = \_ -> Ssrbool.ReflectT} in+ let {_evar_0_16 = \_ -> Ssrbool.ReflectF} in+ case iHx0 of {+ Ssrbool.ReflectT -> _evar_0_15 __;+ Ssrbool.ReflectF -> _evar_0_16 __}}+ in+ case _top_assumption_0 of {+ Move x0 x1 x2 -> _evar_0_7 x0 x1 x2;+ Transfer x0 x1 x2 -> _evar_0_8 x0 x1 x2;+ Spill x0 x1 x2 -> _evar_0_9 x0 x1 x2;+ Restore x0 x1 x2 -> _evar_0_10 x0 x1 x2;+ AllocReg x0 x1 x2 -> _evar_0_11 x0 x1 x2;+ FreeReg x0 x1 x2 -> _evar_0_12 x0 x1 x2;+ AllocStack x0 -> _evar_0_13 x0;+ FreeStack x0 -> _evar_0_14 x0;+ Looped x0 -> _evar_0_15 x0}}+ in coq_ResolvingMove_rect maxReg (unsafeCoerce _evar_0_) (unsafeCoerce _evar_0_0) (unsafeCoerce _evar_0_1) (unsafeCoerce _evar_0_2) (unsafeCoerce _evar_0_3)- (unsafeCoerce _evar_0_4) _evar_0_5 _top_assumption_+ (unsafeCoerce _evar_0_4) (unsafeCoerce _evar_0_5)+ (unsafeCoerce _evar_0_6) _evar_0_7 _top_assumption_ coq_ResolvingMove_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of ResolvingMove@@ -696,10 +991,12 @@ 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);+ Spill fr tv b -> (,) (VirtNode (VarNode tv)) (RegNode fr);+ Restore fv tr b -> (,) (RegNode tr) (VarNode fv);+ AllocReg fv tr b -> (,) (RegNode tr) (VarNode fv);+ FreeReg fr tv b -> (,) (VirtNode (VarNode tv)) (RegNode fr);+ AllocStack tv -> (,) (VarNode tv) (VirtNode (VarNode tv));+ FreeStack fv -> (,) (VirtNode (VarNode fv)) (VarNode fv); Looped x0 -> determineNodes maxReg x0} isMoveSplittable :: Prelude.Int -> ResolvingMove -> Prelude.Bool@@ -712,8 +1009,10 @@ 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) []);+ Move fr fv tr -> (:) (Spill fr fv Prelude.True) ((:) (Restore fv tr+ Prelude.True) []);+ Transfer fr fv tr -> (:) (FreeReg fr fv Prelude.True) ((:) (AllocReg fv tr+ Prelude.True) []); Looped r -> (:) x []; _ -> (:) (Looped x) []} @@ -755,25 +1054,25 @@ (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 -> Prelude.Just (Spill xr vid Prelude.False)}; Prelude.Nothing -> case Allocate.intReg maxReg y of { 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.True -> AllocReg vid yr Prelude.False;+ Prelude.False -> Restore vid yr Prelude.False}); 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.Just r -> Prelude.Just (FreeReg r vid Prelude.False);+ Prelude.Nothing -> Prelude.Just (FreeStack vid)}}; 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.Just r -> Prelude.Just (AllocReg vid r Prelude.False);+ Prelude.Nothing -> Prelude.Just (AllocStack vid)}; Prelude.Nothing -> Prelude.Nothing}}) (allocsAt from) (allocsAt to) determineMoves :: Prelude.Int -> ([] Allocate.Allocation) -> (Prelude.Maybe
LinearScan/ScanState.hs view
@@ -160,7 +160,8 @@ (Prelude.&&) (Seq.all check (handledIntervalDescsForReg maxReg sd reg)) (case Vector0.vnth maxReg (fixedIntervals maxReg sd) reg of { Prelude.Just i ->- Prelude.not (Ssrbool.isSome (Interval.intervalsOverlap int ( i)));+ Prelude.not+ (Ssrbool.isSome (Interval.intervalIntersectsWithSubrange int ( i))); Prelude.Nothing -> Prelude.True}) data ScanStateStatus =
LinearScan/Seq.hs view
@@ -245,7 +245,3 @@ 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/Trace.hs view
@@ -30,7 +30,7 @@ type TrueIfActiveT = Prelude.Bool data SSTrace =- EOverlapsWithFixedInterval Prelude.Int PhysRegT+ EIntersectsWithFixedInterval Prelude.Int PhysRegT | ESplitAssignedIntervalForReg IntervalIdT PhysRegT SplitPositionT | ESplitActiveOrInactiveInterval IntervalIdT TrueIfActiveT SplitPositionT | EIntervalHasUsePosReqReg Prelude.Int
LinearScan/UsePos.hs view
@@ -39,6 +39,7 @@ data VarKind = Input+ | InputOutput | Temp | Output @@ -49,6 +50,10 @@ case s2 of { Input -> Prelude.True; _ -> Prelude.False};+ InputOutput ->+ case s2 of {+ InputOutput -> Prelude.True;+ _ -> Prelude.False}; Temp -> case s2 of { Temp -> Prelude.True;@@ -65,35 +70,54 @@ let {_evar_0_ = Ssrbool.ReflectT} in let {_evar_0_0 = Ssrbool.ReflectF} in let {_evar_0_1 = Ssrbool.ReflectF} in+ let {_evar_0_2 = Ssrbool.ReflectF} in case _top_assumption_0 of { Input -> _evar_0_;- Temp -> _evar_0_0;- Output -> _evar_0_1}}+ InputOutput -> _evar_0_0;+ Temp -> _evar_0_1;+ Output -> _evar_0_2}} in let { _evar_0_0 = \_top_assumption_0 -> let {_evar_0_0 = Ssrbool.ReflectF} in let {_evar_0_1 = Ssrbool.ReflectT} in let {_evar_0_2 = Ssrbool.ReflectF} in+ let {_evar_0_3 = Ssrbool.ReflectF} in case _top_assumption_0 of { Input -> _evar_0_0;- Temp -> _evar_0_1;- Output -> _evar_0_2}}+ InputOutput -> _evar_0_1;+ Temp -> _evar_0_2;+ Output -> _evar_0_3}} in let { _evar_0_1 = \_top_assumption_0 -> let {_evar_0_1 = Ssrbool.ReflectF} in let {_evar_0_2 = Ssrbool.ReflectF} in let {_evar_0_3 = Ssrbool.ReflectT} in+ let {_evar_0_4 = Ssrbool.ReflectF} in case _top_assumption_0 of { Input -> _evar_0_1;- Temp -> _evar_0_2;- Output -> _evar_0_3}}+ InputOutput -> _evar_0_2;+ Temp -> _evar_0_3;+ Output -> _evar_0_4}} in+ let {+ _evar_0_2 = \_top_assumption_0 ->+ let {_evar_0_2 = Ssrbool.ReflectF} in+ let {_evar_0_3 = Ssrbool.ReflectF} in+ let {_evar_0_4 = Ssrbool.ReflectF} in+ let {_evar_0_5 = Ssrbool.ReflectT} in+ case _top_assumption_0 of {+ Input -> _evar_0_2;+ InputOutput -> _evar_0_3;+ Temp -> _evar_0_4;+ Output -> _evar_0_5}}+ in case _top_assumption_ of { Input -> _evar_0_;- Temp -> _evar_0_0;- Output -> _evar_0_1}+ InputOutput -> _evar_0_0;+ Temp -> _evar_0_1;+ Output -> _evar_0_2} coq_VarKind_eqMixin :: Eqtype.Equality__Coq_mixin_of VarKind coq_VarKind_eqMixin =
LinearScan/Vector0.hs view
@@ -135,6 +135,26 @@ unsafeCoerce _evar_0_0 x v) n +vfoldr_with_index :: Prelude.Int -> (Prelude.Int -> a1 -> a2 -> a2) -> a2 ->+ (Vec a1) -> a2+vfoldr_with_index n f b v =+ let {_evar_0_ = \_discharged_f_ _discharged_v_ -> b} in+ let {+ _evar_0_0 = \n0 f0 v0 ->+ let {_evar_0_0 = \x -> f0 (Fintype.inord n0 n0) x b} in+ let {+ _evar_0_1 = \sz x xs iHxs ->+ f0 (Fintype.inord n0 ((Prelude.-) n0 ((Prelude.succ) sz))) x iHxs}+ in+ vecn_rect _evar_0_0 _evar_0_1 n0 v0}+ in+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ _evar_0_ f v)+ (\x ->+ unsafeCoerce _evar_0_0 x f v)+ n+ vfoldl_with_index :: Prelude.Int -> (Prelude.Int -> a2 -> a1 -> a2) -> a2 -> (Vec a1) -> a2 vfoldl_with_index n f b v =
LinearScan/Verify.hs view
@@ -13,12 +13,14 @@ import qualified Data.Functor.Identity import qualified Hask.Utils +import qualified LinearScan.Allocate as Allocate import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Contravariant as Contravariant import qualified LinearScan.Functor as Functor import qualified LinearScan.IntMap as IntMap import qualified LinearScan.IntSet as IntSet+import qualified LinearScan.Interval as Interval import qualified LinearScan.Lens as Lens import qualified LinearScan.List1 as List1 import qualified LinearScan.Loops as Loops@@ -113,9 +115,16 @@ Prelude.Int | VarNotReservedForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId) Prelude.Int+ | StackNotAllocatedForVar Blocks.VarId+ | StackAlreadyAllocatedForVar Blocks.VarId | PhysRegAlreadyReservedForVar Prelude.Int Blocks.VarId | RegAlreadyReservedToVar Prelude.Int Blocks.VarId Blocks.VarId | BlockWithoutPredecessors Blocks.BlockId+ | AllocationDoesNotMatch Blocks.VarId (Prelude.Maybe+ (Prelude.Maybe Prelude.Int)) (Prelude.Maybe+ (Prelude.Maybe+ Prelude.Int)) + Prelude.Int Prelude.Int | UnknownPredecessorBlock Blocks.BlockId Blocks.BlockId | LoopInResolvingMoves Resolve.ResolvingMoveSet @@ -253,9 +262,48 @@ Prelude.Just xs -> Seq.rcons xs mv; Prelude.Nothing -> (:) mv []})) pc) mDict +allocationsAt :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int -> []+ Allocate.Allocation+allocationsAt maxReg intervals pos =+ Prelude.map (\i -> i)+ (Prelude.filter (\i ->+ let {int = Allocate.intVal maxReg i} in+ (Prelude.&&) ((Prelude.<=) (Interval.ibeg int) pos)+ ((Prelude.<=) ((Prelude.succ) pos) (Interval.iend int))) intervals)++allocationFor :: Prelude.Int -> ([] Allocate.Allocation) -> Blocks.VarId ->+ Prelude.Int -> Prelude.Maybe (Prelude.Maybe PhysReg)+allocationFor maxReg intervals var pos =+ case Prelude.filter (\i ->+ Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce (Interval.ivar (Allocate.intVal maxReg i)))+ (unsafeCoerce var)) (allocationsAt maxReg intervals pos) of {+ [] -> Prelude.Nothing;+ (:) a l ->+ case l of {+ [] -> Prelude.Just (Allocate.intReg maxReg a);+ (:) a0 l0 -> Prelude.Nothing}}++checkAllocation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> ([]+ Allocate.Allocation) -> (Prelude.Maybe+ (Prelude.Maybe PhysReg)) -> Blocks.VarId -> Prelude.Int ->+ Prelude.Int -> Verified a1 a2 ()+checkAllocation maxReg mDict pc intervals reg var pos idx =+ let {alloc = allocationFor maxReg intervals var pos} in+ case Prelude.not+ (Eqtype.eq_op+ (Eqtype.option_eqType+ (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg)))+ (unsafeCoerce alloc) (unsafeCoerce reg)) of {+ Prelude.True ->+ errorT maxReg mDict pc (AllocationDoesNotMatch var+ (reg)+ (alloc) pos idx);+ Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}+ reserveReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->- Blocks.VarId -> Verified a1 a2 ()-reserveReg maxReg mDict pc reg var =+ Blocks.VarId -> Prelude.Bool -> Verified a1 a2 ()+reserveReg maxReg mDict pc reg var fromSplit = Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\st -> case Ssr.prop@@ -282,11 +330,11 @@ Prelude.Nothing -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))- (addMove maxReg mDict pc (Resolve.RSAllocReg var ( reg)))+ (addMove maxReg mDict pc (Resolve.RSAllocReg var ( reg) fromSplit)) -isReserved :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Blocks.VarId ->- Verified a1 a2 (Prelude.Maybe Blocks.VarId)-isReserved maxReg mDict reg var =+isReserved :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Verified + a1 a2 (Prelude.Maybe Blocks.VarId)+isReserved maxReg mDict reg = Monad.bind (State0.coq_StateT_Monad mDict) (\st -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Lens.view (Lens.stepdownl' (\_ -> reservation))@@ -313,12 +361,13 @@ case useVerifier of { VerifyEnabledStrict -> err; _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})- (isReserved maxReg mDict reg var))+ (isReserved maxReg mDict reg)) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier- -> PhysReg -> Blocks.VarId -> Verified a1 a2 ()-releaseReg maxReg mDict pc useVerifier reg var =+ -> PhysReg -> Blocks.VarId -> Prelude.Bool -> Verified + a1 a2 ()+releaseReg maxReg mDict pc useVerifier reg var fromSplit = Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\st -> case Ssr.prop@@ -349,8 +398,42 @@ Prelude.Nothing -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))- (addMove maxReg mDict pc (Resolve.RSFreeReg ( reg) var))+ (addMove maxReg mDict pc (Resolve.RSFreeReg ( reg) var fromSplit)) +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))+ assignReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier -> PhysReg -> Blocks.VarId -> Verified a1 a2 () assignReg maxReg mDict pc useVerifier reg var =@@ -363,11 +446,21 @@ (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.Just var)))- (rsStack maxReg st))) mDict;+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Lens.modifyStateT (\_ -> _verState maxReg)+ (packRegState maxReg (Build_RegStateDesc+ (Vector0.vmodify maxReg (rsAllocs maxReg st) reg+ (Lens.set (\_ -> residency) (Prelude.Just var)))+ (rsStack maxReg st))) mDict)+ (Vector0.vfoldr_with_index maxReg (\reg0 x0 act ->+ case Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)+ (Prelude.fst x0) (unsafeCoerce (Prelude.Just var)) of {+ Prelude.True ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> act)+ (clearReg maxReg mDict pc useVerifier reg0 var);+ Prelude.False -> act})+ (Applicative.pure (State0.coq_StateT_Applicative mDict) ())+ (rsAllocs maxReg st)); Prelude.Nothing -> let { err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)@@ -386,9 +479,9 @@ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)) (addMove maxReg mDict pc (Resolve.RSAssignReg var ( reg))) -isResident :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Blocks.VarId ->- Verified a1 a2 (Prelude.Maybe Blocks.VarId)-isResident maxReg mDict reg var =+isResident :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Verified + a1 a2 (Prelude.Maybe Blocks.VarId)+isResident maxReg mDict reg = Monad.bind (State0.coq_StateT_Monad mDict) (\st -> Applicative.pure (State0.coq_StateT_Applicative mDict) (Lens.view (Lens.stepdownl' (\_ -> residency))@@ -414,28 +507,47 @@ (unsafeCoerce var')) err; Prelude.Nothing -> err}; _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()})- (isResident maxReg mDict reg var))+ (isResident maxReg mDict reg)) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) -checkLiveness :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->- UseVerifier -> IntSet.IntSet -> Verified a1 a2 ()-checkLiveness maxReg mDict pc useVerifier vars =- case useVerifier of {- VerifyEnabledStrict ->+allocStack :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier+ -> Blocks.VarId -> Verified a1 a2 ()+allocStack maxReg mDict pc useVerifier var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\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))))- (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict);- _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}+ case Ssr.prop+ (Prelude.not (IntSet.coq_IntSet_member var (rsStack maxReg st))) of {+ Prelude.Just _ ->+ Lens.modifyStateT (\_ -> _verState maxReg)+ (packRegState maxReg (Build_RegStateDesc (rsAllocs maxReg st)+ (IntSet.coq_IntSet_insert var (rsStack maxReg st)))) mDict;+ Prelude.Nothing ->+ let {err = errorT maxReg mDict pc (StackAlreadyAllocatedForVar var)}+ in+ case useVerifier of {+ VerifyEnabledStrict -> err;+ _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))+ (addMove maxReg mDict pc (Resolve.RSAllocStack var)) +freeStack :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier ->+ Blocks.VarId -> Verified a1 a2 ()+freeStack maxReg mDict pc useVerifier var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case Ssr.prop (IntSet.coq_IntSet_member var (rsStack maxReg st)) of {+ Prelude.Just _ ->+ Lens.modifyStateT (\_ -> _verState maxReg)+ (packRegState maxReg (Build_RegStateDesc (rsAllocs maxReg st)+ (IntSet.coq_IntSet_delete var (rsStack maxReg st)))) mDict;+ Prelude.Nothing ->+ let {err = errorT maxReg mDict pc (StackNotAllocatedForVar var)} in+ case useVerifier of {+ VerifyEnabledStrict -> err;+ _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))+ (addMove maxReg mDict pc (Resolve.RSFreeStack var))+ verifyBlockBegin :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier -> Prelude.Int -> IntSet.IntSet -> Loops.LoopState -> Verified a1 a2 ()@@ -445,12 +557,10 @@ Applicative.pure (State0.coq_StateT_Applicative mDict) (); VerifyEnabled -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- 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))+ 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)) (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of { Prelude.Just fwds -> Monad.forM_ (State0.coq_StateT_Monad mDict)@@ -472,12 +582,10 @@ _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}); VerifyEnabledStrict -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- 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))+ 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)) (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of { Prelude.Just fwds -> Monad.forM_ (State0.coq_StateT_Monad mDict)@@ -498,29 +606,27 @@ (errorT maxReg mDict pc (BlockWithoutPredecessors bid)); _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})} -verifyBlockEnd :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->- UseVerifier -> Prelude.Int -> IntSet.IntSet -> Verified - a1 a2 ()-verifyBlockEnd maxReg mDict pc useVerifier bid liveOuts =+verifyBlockEnd :: Prelude.Int -> (Monad.Monad a1) -> UseVerifier ->+ Prelude.Int -> IntSet.IntSet -> Verified a1 a2 ()+verifyBlockEnd maxReg mDict useVerifier bid liveOuts = case useVerifier of { VerifyDisabled -> Applicative.pure (State0.coq_StateT_Applicative mDict) (); _ ->- 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.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)}+ Monad.bind (State0.coq_StateT_Monad mDict) (\allocs ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ 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)} verifyAllocs :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 - a1 a2) -> Blocks.OpId -> UseVerifier -> a1 -> ([]+ a1 a2) -> Blocks.OpId -> ([] Allocate.Allocation) ->+ UseVerifier -> a1 -> ([] ((,) ((,) Blocks.VarId UsePos.VarKind) PhysReg)) -> Verified a3 a4 ()-verifyAllocs maxReg mDict oinfo pc useVerifier op allocs =+verifyAllocs maxReg mDict oinfo pc intervals useVerifier op allocs = case useVerifier of { VerifyDisabled -> Applicative.pure (State0.coq_StateT_Applicative mDict) ();@@ -529,7 +635,32 @@ (Blocks.opRefs maxReg mDict oinfo op) (\ref -> case Blocks.varId maxReg ref of { Prelude.Left reg ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ Monad.when (State0.coq_StateT_Monad mDict)+ (Prelude.not+ (Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (Blocks.varKind maxReg ref))+ (unsafeCoerce UsePos.Input)))+ (Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {+ Prelude.Just v ->+ errorT maxReg mDict pc (PhysRegAlreadyReservedForVar ( reg) v);+ Prelude.Nothing ->+ case Prelude.filter (\i ->+ Eqtype.eq_op+ (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))+ (unsafeCoerce (Allocate.intReg maxReg i))+ (unsafeCoerce (Prelude.Just reg)))+ (allocationsAt maxReg intervals (Prelude.pred pc)) of {+ [] ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ (:) x l ->+ errorT maxReg mDict pc (AllocationDoesNotMatch+ (Interval.ivar (Allocate.intVal maxReg x)) Prelude.Nothing+ (Prelude.Just+ ((Allocate.intReg maxReg x)))+ (Prelude.pred pc) 0)}})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)); Prelude.Right var -> case List1.maybeLookup (Eqtype.prod_eqType Ssrnat.nat_eqType@@ -538,16 +669,55 @@ Prelude.Just reg -> case Blocks.varKind maxReg ref of { UsePos.Input -> checkResidency maxReg mDict pc useVerifier reg var;+ UsePos.InputOutput ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ) 0))+ (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};+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkReservation maxReg mDict pc useVerifier reg var)+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)+ ((Prelude.succ) 0)));+ UsePos.Output ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ assignReg maxReg mDict pc useVerifier reg var)+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) 0))))}; 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) ();+ Monad.when (State0.coq_StateT_Monad mDict)+ (Prelude.not+ (Eqtype.eq_op UsePos.coq_VarKind_eqType+ (unsafeCoerce (Blocks.varKind maxReg ref))+ (unsafeCoerce UsePos.Input)))+ (Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {+ Prelude.Just v ->+ errorT maxReg mDict pc (PhysRegAlreadyReservedForVar ( reg) v);+ Prelude.Nothing ->+ case Prelude.filter (\i ->+ Eqtype.eq_op+ (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))+ (unsafeCoerce (Allocate.intReg maxReg i))+ (unsafeCoerce (Prelude.Just reg)))+ (allocationsAt maxReg intervals (Prelude.pred pc)) of {+ [] ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ (:) x l ->+ errorT maxReg mDict pc (AllocationDoesNotMatch+ (Interval.ivar (Allocate.intVal maxReg x)) Prelude.Nothing+ (Prelude.Just+ ((Allocate.intReg maxReg x)))+ (Prelude.pred pc) 0)}})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)); Prelude.Right var -> case List1.maybeLookup (Eqtype.prod_eqType Ssrnat.nat_eqType@@ -556,9 +726,23 @@ Prelude.Just reg -> case Blocks.varKind maxReg ref of { UsePos.Input -> checkResidency maxReg mDict pc useVerifier reg var;+ UsePos.InputOutput ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ) 0))+ (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};+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkReservation maxReg mDict pc useVerifier reg var)+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)+ ((Prelude.succ) 0)));+ UsePos.Output ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ assignReg maxReg mDict pc useVerifier reg var)+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) 0))))}; Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}})} verifyResolutions :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->@@ -582,61 +766,79 @@ (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);+ Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->+ assignReg maxReg mDict pc useVerifier toReg fromVar)+ (Monad.when (State0.coq_StateT_Monad mDict)+ (Maybe.isJust check)+ (checkResidency maxReg mDict pc useVerifier+ fromReg fromVar)); _ -> assignReg maxReg mDict pc useVerifier toReg fromVar}))- (isResident maxReg mDict fromReg fromVar))+ (isResident maxReg mDict fromReg)) (addMove maxReg mDict pc (Resolve.weakenResolvingMove maxReg mv)))- (reserveReg maxReg mDict pc toReg fromVar))+ (reserveReg maxReg mDict pc toReg fromVar Prelude.False)) (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));+ (releaseReg maxReg mDict pc useVerifier fromReg fromVar+ Prelude.False)); Resolve.Transfer fromReg fromVar 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)- (reserveReg maxReg mDict pc toReg fromVar))+ (reserveReg maxReg mDict pc toReg fromVar Prelude.False)) (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.Spill fromReg toSpillSlot ->+ (releaseReg maxReg mDict pc useVerifier fromReg fromVar+ Prelude.False));+ Resolve.Spill fromReg toSpillSlot fromSplit -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\check -> case Maybe.isJust check of { Prelude.True -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->- Applicative.pure (State0.coq_StateT_Applicative mDict)- (Seq.rcons acc mv))- (addMove maxReg mDict pc- (Resolve.weakenResolvingMove maxReg mv));+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Seq.rcons acc mv))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg mv)))+ (allocStack maxReg mDict pc useVerifier toSpillSlot); Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc})- (isResident maxReg mDict fromReg toSpillSlot))- (releaseReg maxReg mDict pc useVerifier fromReg toSpillSlot);- Resolve.Restore fromSpillSlot toReg ->+ (isResident maxReg mDict fromReg))+ (releaseReg maxReg mDict pc useVerifier fromReg toSpillSlot+ fromSplit);+ Resolve.Restore fromSpillSlot toReg fromSplit -> 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)- (Seq.rcons acc mv))- (assignReg maxReg mDict pc useVerifier toReg fromSpillSlot))+ Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Seq.rcons acc mv))+ (assignReg maxReg mDict pc useVerifier toReg fromSpillSlot))+ (freeStack maxReg mDict pc useVerifier fromSpillSlot)) (addMove maxReg mDict pc (Resolve.weakenResolvingMove maxReg mv)))- (reserveReg maxReg mDict pc toReg fromSpillSlot);- Resolve.AllocReg toVar toReg ->+ (reserveReg maxReg mDict pc toReg fromSpillSlot fromSplit);+ Resolve.AllocReg toVar toReg fromSplit -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc)- (reserveReg maxReg mDict pc toReg toVar);- Resolve.FreeReg fromReg fromVar ->+ (reserveReg maxReg mDict pc toReg toVar fromSplit);+ Resolve.FreeReg fromReg fromVar fromSplit -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc)- (releaseReg maxReg mDict pc useVerifier fromReg fromVar);+ (releaseReg maxReg mDict pc useVerifier fromReg fromVar+ fromSplit);+ Resolve.AllocStack toVar ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) acc)+ (allocStack maxReg mDict pc useVerifier toVar);+ Resolve.FreeStack fromVar ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) acc)+ (freeStack maxReg mDict pc useVerifier fromVar); Resolve.Looped x -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->@@ -646,5 +848,137 @@ (Resolve.weakenResolvingMove maxReg mv))) (errorT maxReg mDict pc (LoopInResolvingMoves (Resolve.weakenResolvingMove maxReg x)))})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))}++verifyTransitions :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> ([]+ Allocate.Allocation) -> UseVerifier -> ([]+ Resolve.ResolvingMove) -> Prelude.Int -> Prelude.Int ->+ Verified a1 a2 ()+verifyTransitions maxReg mDict pc intervals useVerifier moves from to =+ case useVerifier of {+ VerifyDisabled ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ _ ->+ Monad.forM_ (State0.coq_StateT_Monad mDict) moves (\mv ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case mv of {+ Resolve.Move fromReg fromVar toReg ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just toReg)) fromVar to ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ 0))))))+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just fromReg)) fromVar from ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0)))));+ Resolve.Transfer fromReg fromVar toReg ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just toReg)) fromVar to ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) 0))))))))+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just fromReg)) fromVar from ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) 0)))))));+ Resolve.Spill fromReg toSpillSlot fromSplit ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.unless (State0.coq_StateT_Monad mDict) fromSplit+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ Prelude.Nothing) toSpillSlot to ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) 0)))))))))))+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just fromReg)) toSpillSlot from ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0)))))))));+ Resolve.Restore fromSpillSlot toReg fromSplit ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just toReg)) fromSpillSlot to ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) 0))))))))))))+ (Monad.unless (State0.coq_StateT_Monad mDict) fromSplit+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ Prelude.Nothing) fromSpillSlot from ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))))))))));+ Resolve.AllocReg toVar toReg fromSplit ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just toReg)) toVar to ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))))))))))))+ (Monad.unless (State0.coq_StateT_Monad mDict) fromSplit+ (let {alloc = allocationFor maxReg intervals toVar from} in+ case alloc of {+ Prelude.Just o ->+ case o of {+ Prelude.Just p ->+ errorT maxReg mDict pc (AllocationDoesNotMatch toVar+ Prelude.Nothing+ (alloc) from+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ 0)))))))))))));+ Prelude.Nothing ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ()};+ Prelude.Nothing ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ()}));+ Resolve.FreeReg fromReg fromVar fromSplit ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.unless (State0.coq_StateT_Monad mDict) fromSplit+ (checkAllocation maxReg mDict pc intervals Prelude.Nothing+ fromVar to ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ 0)))))))))))))))))+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ (Prelude.Just fromReg)) fromVar from ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) 0)))))))))))))));+ Resolve.AllocStack toVar ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkAllocation maxReg mDict pc intervals (Prelude.Just+ Prelude.Nothing) toVar to ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ 0))))))))))))))))))+ (checkAllocation maxReg mDict pc intervals Prelude.Nothing toVar+ from ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) 0)))))))))))))))));+ Resolve.FreeStack fromVar ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkAllocation maxReg mDict pc intervals Prelude.Nothing fromVar+ to ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ 0))))))))))))))))))))+ (checkAllocation maxReg mDict pc intervals (Prelude.Just+ Prelude.Nothing) fromVar from ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)+ 0)))))))))))))))))));+ Resolve.Looped x ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ()}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))}
linearscan.cabal view
@@ -1,5 +1,5 @@ name: linearscan-version: 0.9.0+version: 0.10.0 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3