-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Utils.RegRewrite
-- Description      : Operations for manipulating registerized CFGs
-- Copyright        : (c) Galois, Inc 2014-2018
-- License          : BSD3
-- Maintainer       : Luke Maurer <lukemaurer@galois.com>
-- Stability        : provisional
--
-- A rewrite engine for registerized CFGs.
------------------------------------------------------------------------
{-# 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
  ( -- * Main interface
    annotateCFGStmts
    -- * Annotation monad
  , 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

------------------------------------------------------------------------
-- Public interface

-- | Add statements to each block in a CFG according to the given
-- instrumentation functions. See the 'Rewriter' monad for the
-- operations provided for adding code.
annotateCFGStmts :: TraverseExt ext
                 => u
                 -- ^ Initial user state
                 -> (forall s h. Posd (Stmt ext s) -> Rewriter ext h s ret u ())
                 -- ^ Action to run on each non-terminating statement;
                 -- must explicitly add the original statement back if
                 -- desired
                 -> (forall s h. Posd (TermStmt s ret) -> Rewriter ext h s ret u ())
                 -- ^ Action to run on each terminating statement
                 -> SomeCFG ext init ret
                 -- ^ Graph to rewrite
                 -> 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')

-- | Monad providing operations for modifying a basic block by adding
-- statements and/or splicing in conditional braches. Also provides a
-- 'MonadState' instance for storing user state.
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))
           )

-- | Add a new statement at the current position.
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))

-- | Add a new statement at the current position, marking it as
-- internally generated.
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

-- | Add a conditional at the current position. This will cause the
-- current block to end and new blocks to be generated for the two
-- branches and the remaining statements in the original block.
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)

-- | Create a new atom with a freshly allocated id. The id will not
-- have been used anywhere in the original CFG.
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 }

------------------------------------------------------------------------
-- Monad
--
-- For each block, rewriting occurs in two stages:
--
-- 1. Generate a sequence of "complex statements", each of which may
--    be an internal if-then-else.
-- 2. Rebuild the block from the complex statements, creating
--    additional blocks for internal control flow.
--
-- Step 1 occurs through a simple writer monad, leaving the nasty details
-- of block mangling to step 2.

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
    -- Have to do this pattern match *after* unpacking the Some from
    -- newSTNonceGenerator for obscure reasons involving Skolem
    -- functions
    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 }

-- | Return the output of a writer action without passing it onward.
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

------------------------------------------------------------------------
-- Implementation

-- Give fresh names to everything.  The only point of this is that the
-- new names come from a known nonce generator, so we can now generate
-- more names.  We do this in a separate pass up front so that we
-- don't have to juggle two namespaces afterward.
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 -- Step 1
     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
     -- Step 2
     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) -- Statements to process
       -> Seq (Posd (Stmt ext s)) -- Statements added to current block
       -> Seq (Block ext s ret)   -- Blocks created so far
       -> BlockID s               -- Id of current block
       -> ValueSet s              -- Extra inputs to current block
       -> Posd (TermStmt s ret)   -- Terminal statement of current block
       -> 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
           -- End the block, terminating with a branch statement
           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
           -- Make the branches into (sets of) blocks
           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
           -- Keep going with a new, currently empty block
           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