{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Lang.Crucible.Utils.RegRewrite
(
annotateCFGStmts
, Rewriter
, addStmt
, addInternalStmt
, ifte
, freshAtom
) where
import Control.Monad.RWS.Strict
import Control.Monad.State.Strict ( StateT, evalStateT )
import Control.Monad.ST ( ST, runST )
import Data.Foldable ( toList )
import Data.Parameterized.Map ( MapF )
import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.Nonce ( Nonce, NonceGenerator, freshNonce
, newSTNonceGenerator )
import Data.Parameterized.Some ( Some(Some) )
import Data.Sequence ( Seq )
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import What4.ProgramLoc
import Lang.Crucible.CFG.Extension
import Lang.Crucible.CFG.Reg
import Lang.Crucible.Types
annotateCFGStmts :: TraverseExt ext
=> u
-> (forall s h. Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (forall s h. Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
-> SomeCFG ext init ret
-> SomeCFG ext init ret
annotateCFGStmts :: forall ext u (ret :: CrucibleType) (init :: Ctx CrucibleType).
TraverseExt ext =>
u
-> (forall s h. Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (forall s h. Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
-> SomeCFG ext init ret
-> SomeCFG ext init ret
annotateCFGStmts u
u forall s h. Posd (Stmt ext s) -> Rewriter ext h s ret u ()
fS forall s h. Posd (TermStmt s ret) -> Rewriter ext h s ret u ()
fT (SomeCFG CFG ext s init ret
cfg) =
u
-> (forall {h} {s}. Rewriter ext h s ret u (SomeCFG ext init ret))
-> SomeCFG ext init ret
forall u ext (ret :: CrucibleType) a.
u -> (forall h s. Rewriter ext h s ret u a) -> a
runRewriter u
u ((forall {h} {s}. Rewriter ext h s ret u (SomeCFG ext init ret))
-> SomeCFG ext init ret)
-> (forall {h} {s}. Rewriter ext h s ret u (SomeCFG ext init ret))
-> SomeCFG ext init ret
forall a b. (a -> b) -> a -> b
$
do CFG ext s init ret
cfg1 <- CFG ext s init ret -> Rewriter ext h s ret u (CFG ext s init ret)
forall s0 s ext (init :: Ctx CrucibleType) (ret :: CrucibleType) h
u.
TraverseExt ext =>
CFG ext s0 init ret -> Rewriter ext h s ret u (CFG ext s init ret)
renameAll CFG ext s init ret
cfg
[[Block ext s ret]]
blocks' <- (Block ext s ret -> Rewriter ext h s ret u [Block ext s ret])
-> [Block ext s ret] -> Rewriter ext h s ret u [[Block ext s ret]]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM ((Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
-> Block ext s ret
-> Rewriter ext h s ret u [Block ext s ret]
forall ext s h (ret :: CrucibleType) u.
TraverseExt ext =>
(Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
-> Block ext s ret
-> Rewriter ext h s ret u [Block ext s ret]
annotateBlockStmts Posd (Stmt ext s) -> Rewriter ext h s ret u ()
forall s h. Posd (Stmt ext s) -> Rewriter ext h s ret u ()
fS Posd (TermStmt s ret) -> Rewriter ext h s ret u ()
forall s h. Posd (TermStmt s ret) -> Rewriter ext h s ret u ()
fT) (CFG ext s init ret -> [Block ext s ret]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks CFG ext s init ret
cfg1)
CFG ext s init ret -> SomeCFG ext init ret
forall ext (init :: Ctx CrucibleType) (ret :: CrucibleType) s.
CFG ext s init ret -> SomeCFG ext init ret
SomeCFG (CFG ext s init ret -> SomeCFG ext init ret)
-> Rewriter ext h s ret u (CFG ext s init ret)
-> Rewriter ext h s ret u (SomeCFG ext init ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> CFG ext s init ret
-> [Block ext s ret] -> Rewriter ext h s ret u (CFG ext s init ret)
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType) h u.
CFG ext s init ret
-> [Block ext s ret] -> Rewriter ext h s ret u (CFG ext s init ret)
newCFG CFG ext s init ret
cfg1 ([[Block ext s ret]] -> [Block ext s ret]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [[Block ext s ret]]
blocks')
newtype Rewriter ext h s (ret :: CrucibleType) u a =
Rewriter (RWST (NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u (ST h) a)
deriving ( (forall a b.
(a -> b) -> Rewriter ext h s ret u a -> Rewriter ext h s ret u b)
-> (forall a b.
a -> Rewriter ext h s ret u b -> Rewriter ext h s ret u a)
-> Functor (Rewriter ext h s ret u)
forall a b.
a -> Rewriter ext h s ret u b -> Rewriter ext h s ret u a
forall a b.
(a -> b) -> Rewriter ext h s ret u a -> Rewriter ext h s ret u b
forall ext h s (ret :: CrucibleType) u a b.
a -> Rewriter ext h s ret u b -> Rewriter ext h s ret u a
forall ext h s (ret :: CrucibleType) u a b.
(a -> b) -> Rewriter ext h s ret u a -> Rewriter ext h s ret u b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall ext h s (ret :: CrucibleType) u a b.
(a -> b) -> Rewriter ext h s ret u a -> Rewriter ext h s ret u b
fmap :: forall a b.
(a -> b) -> Rewriter ext h s ret u a -> Rewriter ext h s ret u b
$c<$ :: forall ext h s (ret :: CrucibleType) u a b.
a -> Rewriter ext h s ret u b -> Rewriter ext h s ret u a
<$ :: forall a b.
a -> Rewriter ext h s ret u b -> Rewriter ext h s ret u a
Functor, Functor (Rewriter ext h s ret u)
Functor (Rewriter ext h s ret u) =>
(forall a. a -> Rewriter ext h s ret u a)
-> (forall a b.
Rewriter ext h s ret u (a -> b)
-> Rewriter ext h s ret u a -> Rewriter ext h s ret u b)
-> (forall a b c.
(a -> b -> c)
-> Rewriter ext h s ret u a
-> Rewriter ext h s ret u b
-> Rewriter ext h s ret u c)
-> (forall a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u b)
-> (forall a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u a)
-> Applicative (Rewriter ext h s ret u)
forall a. a -> Rewriter ext h s ret u a
forall a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u a
forall a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u b
forall a b.
Rewriter ext h s ret u (a -> b)
-> Rewriter ext h s ret u a -> Rewriter ext h s ret u b
forall a b c.
(a -> b -> c)
-> Rewriter ext h s ret u a
-> Rewriter ext h s ret u b
-> Rewriter ext h s ret u c
forall ext h s (ret :: CrucibleType) u.
Functor (Rewriter ext h s ret u)
forall ext h s (ret :: CrucibleType) u a.
a -> Rewriter ext h s ret u a
forall ext h s (ret :: CrucibleType) u a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u a
forall ext h s (ret :: CrucibleType) u a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u b
forall ext h s (ret :: CrucibleType) u a b.
Rewriter ext h s ret u (a -> b)
-> Rewriter ext h s ret u a -> Rewriter ext h s ret u b
forall ext h s (ret :: CrucibleType) u a b c.
(a -> b -> c)
-> Rewriter ext h s ret u a
-> Rewriter ext h s ret u b
-> Rewriter ext h s ret u c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall ext h s (ret :: CrucibleType) u a.
a -> Rewriter ext h s ret u a
pure :: forall a. a -> Rewriter ext h s ret u a
$c<*> :: forall ext h s (ret :: CrucibleType) u a b.
Rewriter ext h s ret u (a -> b)
-> Rewriter ext h s ret u a -> Rewriter ext h s ret u b
<*> :: forall a b.
Rewriter ext h s ret u (a -> b)
-> Rewriter ext h s ret u a -> Rewriter ext h s ret u b
$cliftA2 :: forall ext h s (ret :: CrucibleType) u a b c.
(a -> b -> c)
-> Rewriter ext h s ret u a
-> Rewriter ext h s ret u b
-> Rewriter ext h s ret u c
liftA2 :: forall a b c.
(a -> b -> c)
-> Rewriter ext h s ret u a
-> Rewriter ext h s ret u b
-> Rewriter ext h s ret u c
$c*> :: forall ext h s (ret :: CrucibleType) u a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u b
*> :: forall a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u b
$c<* :: forall ext h s (ret :: CrucibleType) u a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u a
<* :: forall a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u a
Applicative, Applicative (Rewriter ext h s ret u)
Applicative (Rewriter ext h s ret u) =>
(forall a b.
Rewriter ext h s ret u a
-> (a -> Rewriter ext h s ret u b) -> Rewriter ext h s ret u b)
-> (forall a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u b)
-> (forall a. a -> Rewriter ext h s ret u a)
-> Monad (Rewriter ext h s ret u)
forall a. a -> Rewriter ext h s ret u a
forall a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u b
forall a b.
Rewriter ext h s ret u a
-> (a -> Rewriter ext h s ret u b) -> Rewriter ext h s ret u b
forall ext h s (ret :: CrucibleType) u.
Applicative (Rewriter ext h s ret u)
forall ext h s (ret :: CrucibleType) u a.
a -> Rewriter ext h s ret u a
forall ext h s (ret :: CrucibleType) u a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u b
forall ext h s (ret :: CrucibleType) u a b.
Rewriter ext h s ret u a
-> (a -> Rewriter ext h s ret u b) -> Rewriter ext h s ret u b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall ext h s (ret :: CrucibleType) u a b.
Rewriter ext h s ret u a
-> (a -> Rewriter ext h s ret u b) -> Rewriter ext h s ret u b
>>= :: forall a b.
Rewriter ext h s ret u a
-> (a -> Rewriter ext h s ret u b) -> Rewriter ext h s ret u b
$c>> :: forall ext h s (ret :: CrucibleType) u a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u b
>> :: forall a b.
Rewriter ext h s ret u a
-> Rewriter ext h s ret u b -> Rewriter ext h s ret u b
$creturn :: forall ext h s (ret :: CrucibleType) u a.
a -> Rewriter ext h s ret u a
return :: forall a. a -> Rewriter ext h s ret u a
Monad, MonadState u
, MonadWriter (Seq (ComplexStmt ext s))
)
addStmt :: Posd (Stmt ext s) -> Rewriter ext h s ret u ()
addStmt :: forall ext s h (ret :: CrucibleType) u.
Posd (Stmt ext s) -> Rewriter ext h s ret u ()
addStmt Posd (Stmt ext s)
stmt = Seq (ComplexStmt ext s) -> Rewriter ext h s ret u ()
forall w (m :: Type -> Type). MonadWriter w m => w -> m ()
tell (ComplexStmt ext s -> Seq (ComplexStmt ext s)
forall a. a -> Seq a
Seq.singleton (Posd (Stmt ext s) -> ComplexStmt ext s
forall ext s. Posd (Stmt ext s) -> ComplexStmt ext s
Stmt Posd (Stmt ext s)
stmt))
addInternalStmt :: Stmt ext s -> Rewriter ext h s ret u ()
addInternalStmt :: forall ext s h (ret :: CrucibleType) u.
Stmt ext s -> Rewriter ext h s ret u ()
addInternalStmt = Posd (Stmt ext s) -> Rewriter ext h s ret u ()
forall ext s h (ret :: CrucibleType) u.
Posd (Stmt ext s) -> Rewriter ext h s ret u ()
addStmt (Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (Stmt ext s -> Posd (Stmt ext s))
-> Stmt ext s
-> Rewriter ext h s ret u ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd Position
InternalPos
ifte :: Atom s BoolType
-> Rewriter ext h s ret u ()
-> Rewriter ext h s ret u ()
-> Rewriter ext h s ret u ()
ifte :: forall s ext h (ret :: CrucibleType) u.
Atom s BoolType
-> Rewriter ext h s ret u ()
-> Rewriter ext h s ret u ()
-> Rewriter ext h s ret u ()
ifte Atom s BoolType
atom Rewriter ext h s ret u ()
thn Rewriter ext h s ret u ()
els =
do (~(), Seq (ComplexStmt ext s)
thnSeq) <- Rewriter ext h s ret u ()
-> Rewriter ext h s ret u ((), Seq (ComplexStmt ext s))
forall w (m :: Type -> Type) a. MonadWriter w m => m a -> m (a, w)
gather Rewriter ext h s ret u ()
thn
(~(), Seq (ComplexStmt ext s)
elsSeq) <- Rewriter ext h s ret u ()
-> Rewriter ext h s ret u ((), Seq (ComplexStmt ext s))
forall w (m :: Type -> Type) a. MonadWriter w m => m a -> m (a, w)
gather Rewriter ext h s ret u ()
els
Seq (ComplexStmt ext s) -> Rewriter ext h s ret u ()
forall w (m :: Type -> Type). MonadWriter w m => w -> m ()
tell (Seq (ComplexStmt ext s) -> Rewriter ext h s ret u ())
-> Seq (ComplexStmt ext s) -> Rewriter ext h s ret u ()
forall a b. (a -> b) -> a -> b
$ ComplexStmt ext s -> Seq (ComplexStmt ext s)
forall a. a -> Seq a
Seq.singleton (Atom s BoolType
-> Seq (ComplexStmt ext s)
-> Seq (ComplexStmt ext s)
-> ComplexStmt ext s
forall ext s.
Atom s BoolType
-> Seq (ComplexStmt ext s)
-> Seq (ComplexStmt ext s)
-> ComplexStmt ext s
IfThenElse Atom s BoolType
atom Seq (ComplexStmt ext s)
thnSeq Seq (ComplexStmt ext s)
elsSeq)
freshAtom :: TypeRepr tp -> Rewriter ext h s ret u (Atom s tp)
freshAtom :: forall (tp :: CrucibleType) ext h s (ret :: CrucibleType) u.
TypeRepr tp -> Rewriter ext h s ret u (Atom s tp)
freshAtom TypeRepr tp
tp =
do NonceGenerator (ST h) s
ng <- RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
-> Rewriter ext h s ret u (NonceGenerator (ST h) s)
forall ext h s (ret :: CrucibleType) u a.
RWST (NonceGenerator (ST h) s) (Seq (ComplexStmt ext s)) u (ST h) a
-> Rewriter ext h s ret u a
Rewriter (RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
-> Rewriter ext h s ret u (NonceGenerator (ST h) s))
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
-> Rewriter ext h s ret u (NonceGenerator (ST h) s)
forall a b. (a -> b) -> a -> b
$ RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
forall r (m :: Type -> Type). MonadReader r m => m r
ask
Nonce s tp
n <- RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s tp)
-> Rewriter ext h s ret u (Nonce s tp)
forall ext h s (ret :: CrucibleType) u a.
RWST (NonceGenerator (ST h) s) (Seq (ComplexStmt ext s)) u (ST h) a
-> Rewriter ext h s ret u a
Rewriter (RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s tp)
-> Rewriter ext h s ret u (Nonce s tp))
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s tp)
-> Rewriter ext h s ret u (Nonce s tp)
forall a b. (a -> b) -> a -> b
$ ST h (Nonce s tp)
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s tp)
forall (m :: Type -> Type) a.
Monad m =>
m a
-> RWST (NonceGenerator (ST h) s) (Seq (ComplexStmt ext s)) u m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ST h (Nonce s tp)
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s tp))
-> ST h (Nonce s tp)
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s tp)
forall a b. (a -> b) -> a -> b
$ NonceGenerator (ST h) s -> ST h (Nonce s tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator (ST h) s
ng
Atom s tp -> Rewriter ext h s ret u (Atom s tp)
forall a. a -> Rewriter ext h s ret u a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Atom s tp -> Rewriter ext h s ret u (Atom s tp))
-> Atom s tp -> Rewriter ext h s ret u (Atom s tp)
forall a b. (a -> b) -> a -> b
$ Atom { atomPosition :: Position
atomPosition = Position
InternalPos
, atomId :: Nonce s tp
atomId = Nonce s tp
n
, atomSource :: AtomSource s tp
atomSource = AtomSource s tp
forall s (tp :: CrucibleType). AtomSource s tp
Assigned
, typeOfAtom :: TypeRepr tp
typeOfAtom = TypeRepr tp
tp }
data ComplexStmt ext s
= Stmt (Posd (Stmt ext s))
| IfThenElse (Atom s BoolType)
(Seq (ComplexStmt ext s))
(Seq (ComplexStmt ext s))
runRewriter :: forall u ext ret a
. u -> (forall h s. Rewriter ext h s ret u a) -> a
runRewriter :: forall u ext (ret :: CrucibleType) a.
u -> (forall h s. Rewriter ext h s ret u a) -> a
runRewriter u
u forall h s. Rewriter ext h s ret u a
m = (forall s. ST s a) -> a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s a) -> a) -> (forall s. ST s a) -> a
forall a b. (a -> b) -> a -> b
$ do
Some NonceGenerator (ST s) x
ng <- ST s (Some (NonceGenerator (ST s)))
forall t. ST t (Some (NonceGenerator (ST t)))
newSTNonceGenerator
case Rewriter ext s x ret u a
forall h s. Rewriter ext h s ret u a
m of
Rewriter RWST (NonceGenerator (ST s) x) (Seq (ComplexStmt ext x)) u (ST s) a
f -> do
(a
a, u
_, Seq (ComplexStmt ext x)
_) <- RWST (NonceGenerator (ST s) x) (Seq (ComplexStmt ext x)) u (ST s) a
-> NonceGenerator (ST s) x
-> u
-> ST s (a, u, Seq (ComplexStmt ext x))
forall r w s (m :: Type -> Type) a.
RWST r w s m a -> r -> s -> m (a, s, w)
runRWST RWST (NonceGenerator (ST s) x) (Seq (ComplexStmt ext x)) u (ST s) a
f NonceGenerator (ST s) x
ng u
u
a -> ST s a
forall a. a -> ST s a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
a
freshLabel :: forall ext h s ret u. Rewriter ext h s ret u (Label s)
freshLabel :: forall ext h s (ret :: CrucibleType) u.
Rewriter ext h s ret u (Label s)
freshLabel =
do NonceGenerator (ST h) s
ng <- RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
-> Rewriter ext h s ret u (NonceGenerator (ST h) s)
forall ext h s (ret :: CrucibleType) u a.
RWST (NonceGenerator (ST h) s) (Seq (ComplexStmt ext s)) u (ST h) a
-> Rewriter ext h s ret u a
Rewriter (RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
-> Rewriter ext h s ret u (NonceGenerator (ST h) s))
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
-> Rewriter ext h s ret u (NonceGenerator (ST h) s)
forall a b. (a -> b) -> a -> b
$ RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
forall r (m :: Type -> Type). MonadReader r m => m r
ask
Nonce s UnitType
n <- RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s UnitType)
-> Rewriter ext h s ret u (Nonce s UnitType)
forall ext h s (ret :: CrucibleType) u a.
RWST (NonceGenerator (ST h) s) (Seq (ComplexStmt ext s)) u (ST h) a
-> Rewriter ext h s ret u a
Rewriter (RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s UnitType)
-> Rewriter ext h s ret u (Nonce s UnitType))
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s UnitType)
-> Rewriter ext h s ret u (Nonce s UnitType)
forall a b. (a -> b) -> a -> b
$ ST h (Nonce s UnitType)
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s UnitType)
forall (m :: Type -> Type) a.
Monad m =>
m a
-> RWST (NonceGenerator (ST h) s) (Seq (ComplexStmt ext s)) u m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ST h (Nonce s UnitType)
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s UnitType))
-> ST h (Nonce s UnitType)
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(Nonce s UnitType)
forall a b. (a -> b) -> a -> b
$ NonceGenerator (ST h) s -> ST h (Nonce s UnitType)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator (ST h) s
ng
Label s -> Rewriter ext h s ret u (Label s)
forall a. a -> Rewriter ext h s ret u a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Label s -> Rewriter ext h s ret u (Label s))
-> Label s -> Rewriter ext h s ret u (Label s)
forall a b. (a -> b) -> a -> b
$ Label { labelId :: Nonce s UnitType
labelId = Nonce s UnitType
n }
gather :: MonadWriter w m => m a -> m (a, w)
gather :: forall w (m :: Type -> Type) a. MonadWriter w m => m a -> m (a, w)
gather m a
m = (w -> w) -> m (a, w) -> m (a, w)
forall w (m :: Type -> Type) a.
MonadWriter w m =>
(w -> w) -> m a -> m a
censor (w -> w -> w
forall a b. a -> b -> a
const w
forall a. Monoid a => a
mempty) (m (a, w) -> m (a, w)) -> m (a, w) -> m (a, w)
forall a b. (a -> b) -> a -> b
$ m a -> m (a, w)
forall a. m a -> m (a, w)
forall w (m :: Type -> Type) a. MonadWriter w m => m a -> m (a, w)
listen m a
m
renameAll :: forall s0 s ext init ret h u
. ( TraverseExt ext )
=> CFG ext s0 init ret
-> Rewriter ext h s ret u (CFG ext s init ret)
renameAll :: forall s0 s ext (init :: Ctx CrucibleType) (ret :: CrucibleType) h
u.
TraverseExt ext =>
CFG ext s0 init ret -> Rewriter ext h s ret u (CFG ext s init ret)
renameAll CFG ext s0 init ret
cfg = do
NonceGenerator (ST h) s
ng <- RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
-> Rewriter ext h s ret u (NonceGenerator (ST h) s)
forall ext h s (ret :: CrucibleType) u a.
RWST (NonceGenerator (ST h) s) (Seq (ComplexStmt ext s)) u (ST h) a
-> Rewriter ext h s ret u a
Rewriter (RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
-> Rewriter ext h s ret u (NonceGenerator (ST h) s))
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
-> Rewriter ext h s ret u (NonceGenerator (ST h) s)
forall a b. (a -> b) -> a -> b
$ RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(NonceGenerator (ST h) s)
forall r (m :: Type -> Type). MonadReader r m => m r
ask
RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(CFG ext s init ret)
-> Rewriter ext h s ret u (CFG ext s init ret)
forall ext h s (ret :: CrucibleType) u a.
RWST (NonceGenerator (ST h) s) (Seq (ComplexStmt ext s)) u (ST h) a
-> Rewriter ext h s ret u a
Rewriter (RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(CFG ext s init ret)
-> Rewriter ext h s ret u (CFG ext s init ret))
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(CFG ext s init ret)
-> Rewriter ext h s ret u (CFG ext s init ret)
forall a b. (a -> b) -> a -> b
$ ST h (CFG ext s init ret)
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(CFG ext s init ret)
forall (m :: Type -> Type) a.
Monad m =>
m a
-> RWST (NonceGenerator (ST h) s) (Seq (ComplexStmt ext s)) u m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ST h (CFG ext s init ret)
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(CFG ext s init ret))
-> ST h (CFG ext s init ret)
-> RWST
(NonceGenerator (ST h) s)
(Seq (ComplexStmt ext s))
u
(ST h)
(CFG ext s init ret)
forall a b. (a -> b) -> a -> b
$ StateT (MapF (Nonce s0) (Nonce s)) (ST h) (CFG ext s init ret)
-> MapF (Nonce s0) (Nonce s) -> ST h (CFG ext s init ret)
forall (m :: Type -> Type) s a. Monad m => StateT s m a -> s -> m a
evalStateT ((forall (x :: CrucibleType).
Nonce s0 x
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) (Nonce s x))
-> CFG ext s0 init ret
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) (CFG ext s init ret)
forall (m :: Type -> Type) ext s s' (init :: Ctx CrucibleType)
(ret :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> CFG ext s init ret -> m (CFG ext s' init ret)
substCFG (NonceGenerator (ST h) s
-> Nonce s0 x
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) (Nonce s x)
forall (tp :: CrucibleType).
NonceGenerator (ST h) s
-> Nonce s0 tp
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) (Nonce s tp)
rename NonceGenerator (ST h) s
ng) CFG ext s0 init ret
cfg) MapF (Nonce s0) (Nonce s)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
where
rename :: NonceGenerator (ST h) s
-> Nonce s0 (tp :: CrucibleType)
-> StateT (MapF @CrucibleType (Nonce s0) (Nonce s)) (ST h) (Nonce s tp)
rename :: forall (tp :: CrucibleType).
NonceGenerator (ST h) s
-> Nonce s0 tp
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) (Nonce s tp)
rename NonceGenerator (ST h) s
ng Nonce s0 tp
n = do
MapF (Nonce s0) (Nonce s)
mapping <- StateT
(MapF (Nonce s0) (Nonce s)) (ST h) (MapF (Nonce s0) (Nonce s))
forall s (m :: Type -> Type). MonadState s m => m s
get
case Nonce s0 tp -> MapF (Nonce s0) (Nonce s) -> Maybe (Nonce s tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup Nonce s0 tp
n MapF (Nonce s0) (Nonce s)
mapping of
Just Nonce s tp
n' ->
Nonce s tp
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) (Nonce s tp)
forall a. a -> StateT (MapF (Nonce s0) (Nonce s)) (ST h) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Nonce s tp
n'
Maybe (Nonce s tp)
Nothing -> do
Nonce s tp
n' <- ST h (Nonce s tp)
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) (Nonce s tp)
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MapF (Nonce s0) (Nonce s)) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ST h (Nonce s tp)
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) (Nonce s tp))
-> ST h (Nonce s tp)
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) (Nonce s tp)
forall a b. (a -> b) -> a -> b
$ NonceGenerator (ST h) s -> ST h (Nonce s tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator (ST h) s
ng
(MapF (Nonce s0) (Nonce s) -> MapF (Nonce s0) (Nonce s))
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (Nonce s0 tp
-> Nonce s tp
-> MapF (Nonce s0) (Nonce s)
-> MapF (Nonce s0) (Nonce s)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert Nonce s0 tp
n Nonce s tp
n')
Nonce s tp
-> StateT (MapF (Nonce s0) (Nonce s)) (ST h) (Nonce s tp)
forall a. a -> StateT (MapF (Nonce s0) (Nonce s)) (ST h) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Nonce s tp
n'
newCFG :: CFG ext s init ret
-> [Block ext s ret]
-> Rewriter ext h s ret u (CFG ext s init ret)
newCFG :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType) h u.
CFG ext s init ret
-> [Block ext s ret] -> Rewriter ext h s ret u (CFG ext s init ret)
newCFG CFG ext s init ret
cfg [Block ext s ret]
blocks = do
CFG ext s init ret -> Rewriter ext h s ret u (CFG ext s init ret)
forall a. a -> Rewriter ext h s ret u a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (CFG ext s init ret -> Rewriter ext h s ret u (CFG ext s init ret))
-> CFG ext s init ret
-> Rewriter ext h s ret u (CFG ext s init ret)
forall a b. (a -> b) -> a -> b
$ CFG ext s init ret
cfg { cfgBlocks = blocks }
annotateBlockStmts :: TraverseExt ext
=> (Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
-> Block ext s ret
-> Rewriter ext h s ret u [Block ext s ret]
annotateBlockStmts :: forall ext s h (ret :: CrucibleType) u.
TraverseExt ext =>
(Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
-> Block ext s ret
-> Rewriter ext h s ret u [Block ext s ret]
annotateBlockStmts Posd (Stmt ext s) -> Rewriter ext h s ret u ()
fS Posd (TermStmt s ret) -> Rewriter ext h s ret u ()
fT Block ext s ret
block =
do
Seq (ComplexStmt ext s)
stmts <- (Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
-> Block ext s ret
-> Rewriter ext h s ret u (Seq (ComplexStmt ext s))
forall ext s h (ret :: CrucibleType) u.
(Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
-> Block ext s ret
-> Rewriter ext h s ret u (Seq (ComplexStmt ext s))
annotateAsComplexStmts Posd (Stmt ext s) -> Rewriter ext h s ret u ()
fS Posd (TermStmt s ret) -> Rewriter ext h s ret u ()
fT Block ext s ret
block
Seq (ComplexStmt ext s)
-> Block ext s ret -> Rewriter ext h s ret u [Block ext s ret]
forall ext s (ret :: CrucibleType) h u.
TraverseExt ext =>
Seq (ComplexStmt ext s)
-> Block ext s ret -> Rewriter ext h s ret u [Block ext s ret]
rebuildBlock Seq (ComplexStmt ext s)
stmts Block ext s ret
block
annotateAsComplexStmts :: (Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
-> Block ext s ret
-> Rewriter ext h s ret u (Seq (ComplexStmt ext s))
annotateAsComplexStmts :: forall ext s h (ret :: CrucibleType) u.
(Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> (Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
-> Block ext s ret
-> Rewriter ext h s ret u (Seq (ComplexStmt ext s))
annotateAsComplexStmts Posd (Stmt ext s) -> Rewriter ext h s ret u ()
fS Posd (TermStmt s ret) -> Rewriter ext h s ret u ()
fT Block ext s ret
block =
do (~(), Seq (ComplexStmt ext s)
stmts) <- Rewriter ext h s ret u ()
-> Rewriter ext h s ret u ((), Seq (ComplexStmt ext s))
forall w (m :: Type -> Type) a. MonadWriter w m => m a -> m (a, w)
gather (Rewriter ext h s ret u ()
-> Rewriter ext h s ret u ((), Seq (ComplexStmt ext s)))
-> Rewriter ext h s ret u ()
-> Rewriter ext h s ret u ((), Seq (ComplexStmt ext s))
forall a b. (a -> b) -> a -> b
$
do (Posd (Stmt ext s) -> Rewriter ext h s ret u ())
-> Seq (Posd (Stmt ext s)) -> Rewriter ext h s ret u ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Posd (Stmt ext s) -> Rewriter ext h s ret u ()
fS (Block ext s ret -> Seq (Posd (Stmt ext s))
forall ext s (ret :: CrucibleType).
Block ext s ret -> Seq (Posd (Stmt ext s))
blockStmts Block ext s ret
block)
Posd (TermStmt s ret) -> Rewriter ext h s ret u ()
fT (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
block)
Seq (ComplexStmt ext s)
-> Rewriter ext h s ret u (Seq (ComplexStmt ext s))
forall a. a -> Rewriter ext h s ret u a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Seq (ComplexStmt ext s)
stmts
rebuildBlock :: TraverseExt ext
=> Seq (ComplexStmt ext s)
-> Block ext s ret
-> Rewriter ext h s ret u [Block ext s ret]
rebuildBlock :: forall ext s (ret :: CrucibleType) h u.
TraverseExt ext =>
Seq (ComplexStmt ext s)
-> Block ext s ret -> Rewriter ext h s ret u [Block ext s ret]
rebuildBlock Seq (ComplexStmt ext s)
stmts Block ext s ret
block =
Seq (Block ext s ret) -> [Block ext s ret]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (Seq (Block ext s ret) -> [Block ext s ret])
-> Rewriter ext h s ret u (Seq (Block ext s ret))
-> Rewriter ext h s ret u [Block ext s ret]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
forall ext s (ret :: CrucibleType) h u.
TraverseExt ext =>
Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
go Seq (ComplexStmt ext s)
stmts Seq (Posd (Stmt ext s))
forall a. Seq a
Seq.empty Seq (Block ext s ret)
forall a. Seq a
Seq.empty
(Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
block) (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockExtraInputs Block ext s ret
block) (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
block)
where
go :: TraverseExt ext
=> Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
go :: forall ext s (ret :: CrucibleType) h u.
TraverseExt ext =>
Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
go Seq (ComplexStmt ext s)
s Seq (Posd (Stmt ext s))
accStmts Seq (Block ext s ret)
accBlocks BlockID s
bid ValueSet s
ext Posd (TermStmt s ret)
term = case Seq (ComplexStmt ext s)
s of
Seq (ComplexStmt ext s)
Seq.Empty ->
Seq (Block ext s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
forall a. a -> Rewriter ext h s ret u a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (Block ext s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret)))
-> Seq (Block ext s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
forall a b. (a -> b) -> a -> b
$ Seq (Block ext s ret)
accBlocks Seq (Block ext s ret) -> Block ext s ret -> Seq (Block ext s ret)
forall a. Seq a -> a -> Seq a
Seq.|> BlockID s
-> ValueSet s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret
forall ext s (ret :: CrucibleType).
TraverseExt ext =>
BlockID s
-> ValueSet s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret
mkBlock BlockID s
bid ValueSet s
ext Seq (Posd (Stmt ext s))
accStmts Posd (TermStmt s ret)
term
(Stmt Posd (Stmt ext s)
stmt Seq.:<| Seq (ComplexStmt ext s)
s') ->
Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
forall ext s (ret :: CrucibleType) h u.
TraverseExt ext =>
Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
go Seq (ComplexStmt ext s)
s' (Seq (Posd (Stmt ext s))
accStmts Seq (Posd (Stmt ext s))
-> Posd (Stmt ext s) -> Seq (Posd (Stmt ext s))
forall a. Seq a -> a -> Seq a
Seq.|> Posd (Stmt ext s)
stmt) Seq (Block ext s ret)
accBlocks BlockID s
bid ValueSet s
ext Posd (TermStmt s ret)
term
(IfThenElse Atom s BoolType
a Seq (ComplexStmt ext s)
thn Seq (ComplexStmt ext s)
els Seq.:<| Seq (ComplexStmt ext s)
s') ->
do Label s
thnLab <- Rewriter ext h s ret u (Label s)
forall ext h s (ret :: CrucibleType) u.
Rewriter ext h s ret u (Label s)
freshLabel
Label s
elsLab <- Rewriter ext h s ret u (Label s)
forall ext h s (ret :: CrucibleType) u.
Rewriter ext h s ret u (Label s)
freshLabel
Label s
newLab <- Rewriter ext h s ret u (Label s)
forall ext h s (ret :: CrucibleType) u.
Rewriter ext h s ret u (Label s)
freshLabel
let branch :: Posd (TermStmt s ret)
branch = Position -> TermStmt s ret -> Posd (TermStmt s ret)
forall v. Position -> v -> Posd v
Posd Position
InternalPos (Atom s BoolType -> Label s -> Label s -> TermStmt s ret
forall s (ret :: CrucibleType).
Atom s BoolType -> Label s -> Label s -> TermStmt s ret
Br Atom s BoolType
a Label s
thnLab Label s
elsLab)
thisBlock :: Block ext s ret
thisBlock = BlockID s
-> ValueSet s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret
forall ext s (ret :: CrucibleType).
TraverseExt ext =>
BlockID s
-> ValueSet s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret
mkBlock BlockID s
bid ValueSet s
ext Seq (Posd (Stmt ext s))
accStmts Posd (TermStmt s ret)
branch
let jump :: Posd (TermStmt s ret)
jump = Position -> TermStmt s ret -> Posd (TermStmt s ret)
forall v. Position -> v -> Posd v
Posd Position
InternalPos (Label s -> TermStmt s ret
forall s (ret :: CrucibleType). Label s -> TermStmt s ret
Jump Label s
newLab)
Seq (Block ext s ret)
thnBlocks <-
Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
forall ext s (ret :: CrucibleType) h u.
TraverseExt ext =>
Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
go Seq (ComplexStmt ext s)
thn Seq (Posd (Stmt ext s))
forall a. Seq a
Seq.empty Seq (Block ext s ret)
forall a. Seq a
Seq.empty (Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
thnLab) ValueSet s
forall a. Set a
Set.empty Posd (TermStmt s ret)
jump
Seq (Block ext s ret)
elsBlocks <-
Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
forall ext s (ret :: CrucibleType) h u.
TraverseExt ext =>
Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
go Seq (ComplexStmt ext s)
els Seq (Posd (Stmt ext s))
forall a. Seq a
Seq.empty Seq (Block ext s ret)
forall a. Seq a
Seq.empty (Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
elsLab) ValueSet s
forall a. Set a
Set.empty Posd (TermStmt s ret)
jump
let accBlocks' :: Seq (Block ext s ret)
accBlocks' = (Seq (Block ext s ret)
accBlocks Seq (Block ext s ret) -> Block ext s ret -> Seq (Block ext s ret)
forall a. Seq a -> a -> Seq a
Seq.|> Block ext s ret
thisBlock) Seq (Block ext s ret)
-> Seq (Block ext s ret) -> Seq (Block ext s ret)
forall a. Seq a -> Seq a -> Seq a
Seq.><
Seq (Block ext s ret)
thnBlocks Seq (Block ext s ret)
-> Seq (Block ext s ret) -> Seq (Block ext s ret)
forall a. Seq a -> Seq a -> Seq a
Seq.>< Seq (Block ext s ret)
elsBlocks
Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
forall ext s (ret :: CrucibleType) h u.
TraverseExt ext =>
Seq (ComplexStmt ext s)
-> Seq (Posd (Stmt ext s))
-> Seq (Block ext s ret)
-> BlockID s
-> ValueSet s
-> Posd (TermStmt s ret)
-> Rewriter ext h s ret u (Seq (Block ext s ret))
go Seq (ComplexStmt ext s)
s' Seq (Posd (Stmt ext s))
forall a. Seq a
Seq.empty Seq (Block ext s ret)
accBlocks' (Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
newLab) ValueSet s
forall a. Set a
Set.empty Posd (TermStmt s ret)
term