linearscan 0.10.0 → 0.10.1
raw patch · 2 files changed
+35/−49 lines, 2 files
Files
- LinearScan/Verify.hs +34/−48
- linearscan.cabal +1/−1
LinearScan/Verify.hs view
@@ -341,10 +341,9 @@ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) -checkReservation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->- UseVerifier -> PhysReg -> Blocks.VarId -> Verified - a1 a2 ()-checkReservation maxReg mDict pc useVerifier reg var =+checkReservation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg+ -> Blocks.VarId -> Verified a1 a2 ()+checkReservation maxReg mDict pc reg var = Monad.bind (State0.coq_StateT_Monad mDict) (\st -> let { err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)@@ -357,17 +356,12 @@ Prelude.Just var' -> Monad.unless (State0.coq_StateT_Monad mDict) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce var) var') err;- Prelude.Nothing ->- case useVerifier of {- VerifyEnabledStrict -> err;- _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})- (isReserved maxReg mDict reg))+ Prelude.Nothing -> err}) (isReserved maxReg mDict reg)) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) -releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier- -> PhysReg -> Blocks.VarId -> Prelude.Bool -> Verified - a1 a2 ()-releaseReg maxReg mDict pc useVerifier reg var fromSplit =+releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->+ Blocks.VarId -> Prelude.Bool -> Verified a1 a2 ()+releaseReg 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@@ -383,20 +377,10 @@ (Lens.set (\_ -> reservation) Prelude.Nothing)) (rsStack maxReg st))) mDict; Prelude.Nothing ->- let {- err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)- (Lens.view (Lens.stepdownl' (\_ -> reservation))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg))- ((Prelude.succ) ((Prelude.succ) 0)))}- in- case useVerifier of {- VerifyEnabledStrict -> err;- _ ->- case Lens.view (Lens.stepdownl' (\_ -> reservation))- (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {- Prelude.Just v -> err;- Prelude.Nothing ->- Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})+ errorT maxReg mDict pc (VarNotReservedForReg var ( reg)+ (Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg)) ((Prelude.succ)+ ((Prelude.succ) 0)))}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)) (addMove maxReg mDict pc (Resolve.RSFreeReg ( reg) var fromSplit)) @@ -676,7 +660,7 @@ (checkResidency maxReg mDict pc useVerifier reg var); UsePos.Temp -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- checkReservation maxReg mDict pc useVerifier reg var)+ checkReservation maxReg mDict pc reg var) (checkAllocation maxReg mDict pc intervals (Prelude.Just (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ) ((Prelude.succ) 0)));@@ -733,7 +717,7 @@ (checkResidency maxReg mDict pc useVerifier reg var); UsePos.Temp -> Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- checkReservation maxReg mDict pc useVerifier reg var)+ checkReservation maxReg mDict pc reg var) (checkAllocation maxReg mDict pc intervals (Prelude.Just (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ) ((Prelude.succ) 0)));@@ -781,8 +765,7 @@ (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- Prelude.False));+ (releaseReg maxReg mDict pc 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 ->@@ -791,8 +774,7 @@ (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- Prelude.False));+ (releaseReg maxReg mDict pc 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 ->@@ -808,20 +790,25 @@ Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc}) (isResident maxReg mDict fromReg))- (releaseReg maxReg mDict pc useVerifier fromReg toSpillSlot- fromSplit);+ (releaseReg maxReg mDict pc 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 ->- 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 fromSplit);+ Monad.bind (State0.coq_StateT_Monad mDict) (\check ->+ 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 mv))+ (assignReg maxReg mDict pc useVerifier toReg+ fromSpillSlot))+ (freeStack maxReg mDict pc useVerifier fromSpillSlot))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg mv)))+ (Monad.unless (State0.coq_StateT_Monad mDict)+ (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType) check+ (unsafeCoerce (Prelude.Just fromSpillSlot)))+ (reserveReg maxReg mDict pc toReg fromSpillSlot fromSplit)))+ (isReserved maxReg mDict toReg); Resolve.AllocReg toVar toReg fromSplit -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc)@@ -829,8 +816,7 @@ 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- fromSplit);+ (releaseReg maxReg mDict pc fromReg fromVar fromSplit); Resolve.AllocStack toVar -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
linearscan.cabal view
@@ -1,5 +1,5 @@ name: linearscan-version: 0.10.0+version: 0.10.1 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3