-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.CFG.EarlyMergeLoops
-- Description      : Provides transformations on pre-SSA CFGs
-- Copyright        : (c) Galois, Inc 2020
-- License          : BSD3
-- Maintainer       : 
-- Stability        : experimental
--
-- This modules exposes a transformation that attempts to ensure that loop branches
-- are post-dominated by nodes in the loop.
--
-- The module is organized into 3 main components:
--   1. An analysis that computes the natural loops of a CFG;
--   2. An analysis that inserts postdominators into loops that have
--      "early exits" (and hence have postdominators outside the loop);
--   3. A "fixup" pass that ensures that, in the transformed CFG, all
--      values are well defined along all (new) paths.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

module Lang.Crucible.CFG.EarlyMergeLoops
  ( earlyMergeLoops
  ) where

import           Control.Monad (when, (>=>))
import           Control.Applicative ((<**>))
import qualified Data.Graph.Inductive as G
import qualified Data.Foldable as Fold
import           Data.Kind
import           Data.List (nub, minimumBy)
import qualified Data.Map.Strict as Map
import           Data.Maybe (fromMaybe)
import           Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq ((<|), fromList)
import           Data.String (fromString)

import           What4.ProgramLoc (Position(..), Posd(..))

import           Lang.Crucible.CFG.Expr
import           Lang.Crucible.CFG.Reg
import           Lang.Crucible.Panic
import           Lang.Crucible.Types

--------------------------
-- | Natural Loop Analysis
--------------------------

-- | This structure identifies natural loops. Natural loops are either
-- disjoint from each other, nested, or they share the same header.
data LoopInfo s = LoopInfo
  { forall s. LoopInfo s -> BlockID s
liFooter     :: !(BlockID s)
    -- ^ This is the block with a backedge (to the header)
  , forall s. LoopInfo s -> BlockID s
liHeader     :: !(BlockID s)
    -- ^ This is the destination of the backedge.
  , forall s. LoopInfo s -> Set (BlockID s)
liMembers    :: !(Set (BlockID s))
  -- ^ The loop members, which is the set of nodes that can reach the footer
  -- without going through the header.
  , forall s. LoopInfo s -> [CFGEdge s]
liEarlyExits :: ![CFGEdge s]
  -- ^ An exiting edge is an edge from a node in the loop to an edge
  -- not in the loop. An early exit is such an edge from a node that
  -- is not the footer node.
  , forall s. LoopInfo s -> [CFGEdge s]
liFooterIn   :: ![CFGEdge s]
  -- ^ All the edges to the footer
  , forall s. LoopInfo s -> [BlockID s]
liDominators :: ![BlockID s]
  -- ^ The dominators of the loop header.
  } deriving (LoopInfo s -> LoopInfo s -> Bool
(LoopInfo s -> LoopInfo s -> Bool)
-> (LoopInfo s -> LoopInfo s -> Bool) -> Eq (LoopInfo s)
forall s. LoopInfo s -> LoopInfo s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall s. LoopInfo s -> LoopInfo s -> Bool
== :: LoopInfo s -> LoopInfo s -> Bool
$c/= :: forall s. LoopInfo s -> LoopInfo s -> Bool
/= :: LoopInfo s -> LoopInfo s -> Bool
Eq, Node -> LoopInfo s -> ShowS
[LoopInfo s] -> ShowS
LoopInfo s -> String
(Node -> LoopInfo s -> ShowS)
-> (LoopInfo s -> String)
-> ([LoopInfo s] -> ShowS)
-> Show (LoopInfo s)
forall s. Node -> LoopInfo s -> ShowS
forall s. [LoopInfo s] -> ShowS
forall s. LoopInfo s -> String
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall s. Node -> LoopInfo s -> ShowS
showsPrec :: Node -> LoopInfo s -> ShowS
$cshow :: forall s. LoopInfo s -> String
show :: LoopInfo s -> String
$cshowList :: forall s. [LoopInfo s] -> ShowS
showList :: [LoopInfo s] -> ShowS
Show)
type CFGEdge s = (BlockID s, BlockID s)

-- | Detect all loops in a cfg.
-- The assumption is that two backedges in a cfg will have distinct destination blocks.
-- If this assumption does not hold, then return the empty list.
cfgLoops :: CFG ext s init ret -> [LoopInfo s]
cfgLoops :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [LoopInfo s]
cfgLoops CFG ext s init ret
cfg
  | Bool
distinct  = [LoopInfo s]
lis
  | Bool
otherwise = []
  where
    (Map Node (BlockID s)
nm, UGr
gr) = [Block ext s ret] -> (Map Node (BlockID s), UGr)
forall ext s (ret :: CrucibleType).
[Block ext s ret] -> (Map Node (BlockID s), UGr)
blocksGraph (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
cfg)
    root :: Node
root     = BlockID s -> Node
forall s. BlockID s -> Node
toNode (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID (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
cfgEntryBlock CFG ext s init ret
cfg))
    ls :: [(LEdge (), Set Node)]
ls       = Node -> UGr -> [(LEdge (), Set Node)]
loops Node
root UGr
gr
    lis :: [LoopInfo s]
lis      = (LEdge (), Set Node) -> LoopInfo s
mkLoopInfo ((LEdge (), Set Node) -> LoopInfo s)
-> [(LEdge (), Set Node)] -> [LoopInfo s]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LEdge (), Set Node)]
ls
    distinct :: Bool
distinct = [BlockID s] -> Node
forall a. [a] -> Node
forall (t :: Type -> Type) a. Foldable t => t a -> Node
length ([BlockID s] -> [BlockID s]
forall a. Eq a => [a] -> [a]
nub (LoopInfo s -> BlockID s
forall s. LoopInfo s -> BlockID s
liHeader (LoopInfo s -> BlockID s) -> [LoopInfo s] -> [BlockID s]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [LoopInfo s]
lis)) Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== [LoopInfo s] -> Node
forall a. [a] -> Node
forall (t :: Type -> Type) a. Foldable t => t a -> Node
length [LoopInfo s]
lis

    mkLoopInfo :: (LEdge (), Set Node) -> LoopInfo s
mkLoopInfo ((Node
footer, Node
header, ()
_), Set Node
members) =
      LoopInfo
      { liFooter :: BlockID s
liFooter     = Node -> BlockID s
toBlockID Node
footer
      , liHeader :: BlockID s
liHeader     = Node -> BlockID s
toBlockID Node
header
      , liMembers :: Set (BlockID s)
liMembers    = (Node -> BlockID s) -> Set Node -> Set (BlockID s)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Node -> BlockID s
toBlockID Set Node
members
      , liEarlyExits :: [CFGEdge s]
liEarlyExits = [ (Node -> BlockID s
toBlockID Node
i, Node -> BlockID s
toBlockID Node
j) | (Node
i,Node
j) <- Set Node -> [(Node, Node)]
exits Set Node
members, Node
i Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
footer ]
      , liFooterIn :: [CFGEdge s]
liFooterIn   = [ (Node -> BlockID s
toBlockID Node
j, Node -> BlockID s
toBlockID Node
footer) | Node
j <- UGr -> Node -> [Node]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
gr a b -> Node -> [Node]
G.pre UGr
gr Node
footer ]
      , liDominators :: [BlockID s]
liDominators = [BlockID s]
-> ([Node] -> [BlockID s]) -> Maybe [Node] -> [BlockID s]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((Node -> BlockID s) -> [Node] -> [BlockID s]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Node -> BlockID s
toBlockID) (Maybe [Node] -> [BlockID s]) -> Maybe [Node] -> [BlockID s]
forall a b. (a -> b) -> a -> b
$ Node -> [(Node, [Node])] -> Maybe [Node]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Node
header (UGr -> Node -> [(Node, [Node])]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
gr a b -> Node -> [(Node, [Node])]
G.dom UGr
gr Node
root)
      }

    toBlockID :: Node -> BlockID s
toBlockID Node
n = Map Node (BlockID s)
nm Map Node (BlockID s) -> Node -> BlockID s
forall k a. Ord k => Map k a -> k -> a
Map.! Node
n

    exits :: Set Node -> [(Node, Node)]
exits Set Node
bs = [ (Node
i, Node
j) | Node
i <- Set Node -> [Node]
forall a. Set a -> [a]
Set.toList Set Node
bs, Node
j <- UGr -> Node -> [Node]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
gr a b -> Node -> [Node]
G.suc UGr
gr Node
i, Node
j Node -> Set Node -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set Node
bs ]

-- | Is li1 nested in li2
isNested :: LoopInfo s -> LoopInfo s -> Ordering
isNested :: forall s. LoopInfo s -> LoopInfo s -> Ordering
isNested LoopInfo s
li1 LoopInfo s
li2
  | LoopInfo s -> BlockID s
forall s. LoopInfo s -> BlockID s
liHeader LoopInfo s
li2 BlockID s -> [BlockID s] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` LoopInfo s -> [BlockID s]
forall s. LoopInfo s -> [BlockID s]
liDominators LoopInfo s
li1 = Ordering
LT
  | Bool
otherwise = Ordering
EQ

-- | Return all loops in @g@, which are edges from a node in g to a
-- dominator of that node.
loops :: G.Node -- ^ entry node
      -> G.UGr -- ^ the graph
      -> [(G.LEdge (), Set G.Node)]
loops :: Node -> UGr -> [(LEdge (), Set Node)]
loops Node
root UGr
g = [ (LEdge ()
e, UGr -> Map Node [Node] -> Node -> Set Node
loopMembers UGr
g Map Node [Node]
dominators Node
header) | e :: LEdge ()
e@(Node
_,Node
header,()
_) <- [LEdge ()]
edges ]
  where
    edges :: [LEdge ()]
edges = Map Node [Node] -> UGr -> Node -> [LEdge ()]
loop Map Node [Node]
dominators UGr
g (Node -> [LEdge ()]) -> [Node] -> [LEdge ()]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< UGr -> [Node]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
gr a b -> [Node]
G.nodes UGr
g
    dominators :: Map Node [Node]
dominators = [(Node, [Node])] -> Map Node [Node]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Node, [Node])] -> Map Node [Node])
-> [(Node, [Node])] -> Map Node [Node]
forall a b. (a -> b) -> a -> b
$ UGr -> Node -> [(Node, [Node])]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
gr a b -> Node -> [(Node, [Node])]
G.dom UGr
g Node
root

-- | Return any edges from @n@ to a dominator of @n@, @n'@. The edge
-- @n@ to @n'@ is a loop.
loop :: Map.Map G.Node [G.Node] -- ^ Dominators
     -> G.UGr -- ^ The graph itself
     -> G.Node -- ^ The root node to inspect for backedges
     -> [G.LEdge ()] -- ^ A loop is an edge to a dominator
loop :: Map Node [Node] -> UGr -> Node -> [LEdge ()]
loop Map Node [Node]
domMap UGr
g Node
n =
  -- A back edge (loop) is an edge from n -> n' where n' dominates n
  [ (Node
n, Node
n', ()) | Node
n' <- UGr -> Node -> [Node]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
gr a b -> Node -> [Node]
G.suc UGr
g Node
n, Node
n Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
n', Node
n' Node -> [Node] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [Node] -> Node -> Map Node [Node] -> [Node]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Node
n Map Node [Node]
domMap ]

-- | The members of a loop are just those nodes dominated by the
-- header that can reach the header again
loopMembers :: G.UGr -> Map.Map G.Node [G.Node] -> G.Node -> Set G.Node
loopMembers :: UGr -> Map Node [Node] -> Node -> Set Node
loopMembers UGr
g Map Node [Node]
doms Node
header =
  [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList [Node]
members
  where
    fromHeader :: [Node]
fromHeader = Node -> UGr -> [Node]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
Node -> gr a b -> [Node]
G.reachable Node
header UGr
g
    members :: [Node]
members    = [ Node
x | Node
x <- [Node]
fromHeader, Node
header Node -> [Node] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` Node -> UGr -> [Node]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
Node -> gr a b -> [Node]
G.reachable Node
x UGr
g, Node -> Bool
headerDominates Node
x ]
    headerDominates :: Node -> Bool
headerDominates Node
n
      | Just [Node]
ds <- Node -> Map Node [Node] -> Maybe [Node]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Node
n Map Node [Node]
doms
      = Node
header Node -> [Node] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [Node]
ds
      | Bool
otherwise
      = Bool
False

-- | View a blockID as a node
toNode :: BlockID s -> G.Node
toNode :: forall s. BlockID s -> Node
toNode BlockID s
i =
  case BlockID s
i of
    LabelID Label s
l  -> Word64 -> Node
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Node) -> Word64 -> Node
forall a b. (a -> b) -> a -> b
$ Nonce s UnitType -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Nonce s UnitType -> Word64) -> Nonce s UnitType -> Word64
forall a b. (a -> b) -> a -> b
$ Label s -> Nonce s UnitType
forall s. Label s -> Nonce s UnitType
labelId Label s
l
    LambdaID LambdaLabel s tp
l -> Word64 -> Node
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Node) -> Word64 -> Node
forall a b. (a -> b) -> a -> b
$ Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Nonce s tp -> Word64) -> Nonce s tp -> Word64
forall a b. (a -> b) -> a -> b
$ LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s tp
l

-- | Compute the successor nodes of this block
blockSuccessors :: Block ext s ret -> [G.Node]
blockSuccessors :: forall ext s (ret :: CrucibleType). Block ext s ret -> [Node]
blockSuccessors Block ext s ret
b =
  [Node] -> ([BlockID s] -> [Node]) -> Maybe [BlockID s] -> [Node]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((BlockID s -> Node) -> [BlockID s] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map BlockID s -> Node
forall s. BlockID s -> Node
toNode) (Maybe [BlockID s] -> [Node]) -> Maybe [BlockID s] -> [Node]
forall a b. (a -> b) -> a -> b
$ TermStmt s ret -> Maybe [BlockID s]
forall s (ret :: CrucibleType). TermStmt s ret -> Maybe [BlockID s]
termNextLabels (Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val (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
b))

-- | Returns the edges from this block to its successors
blockEdges :: Block ext s ret -> [G.LEdge ()]
blockEdges :: forall ext s (ret :: CrucibleType). Block ext s ret -> [LEdge ()]
blockEdges Block ext s ret
b =
  Node -> Node -> LEdge ()
forall {a} {b}. a -> b -> (a, b, ())
mkEdge (BlockID s -> Node
forall s. BlockID s -> Node
toNode (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b)) (Node -> LEdge ()) -> [Node] -> [LEdge ()]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Block ext s ret -> [Node]
forall ext s (ret :: CrucibleType). Block ext s ret -> [Node]
blockSuccessors Block ext s ret
b
  where
    mkEdge :: a -> b -> (a, b, ())
mkEdge a
x b
y = (a
x, b
y, ())

blocksGraph :: [Block ext s ret] -> (Map.Map G.Node (BlockID s), G.UGr)
blocksGraph :: forall ext s (ret :: CrucibleType).
[Block ext s ret] -> (Map Node (BlockID s), UGr)
blocksGraph [Block ext s ret]
blocks = (Map Node (BlockID s)
m, [LNode ()] -> [LEdge ()] -> UGr
forall a b. [LNode a] -> [LEdge b] -> Gr a b
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
G.mkGraph ((,()) (Node -> LNode ()) -> [Node] -> [LNode ()]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Node]
nodes) [LEdge ()]
edges)
  where
    nodes :: [Node]
nodes = BlockID s -> Node
forall s. BlockID s -> Node
toNode (BlockID s -> Node)
-> (Block ext s ret -> BlockID s) -> Block ext s ret -> Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID (Block ext s ret -> Node) -> [Block ext s ret] -> [Node]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Block ext s ret]
blocks
    m :: Map Node (BlockID s)
m     = [(Node, BlockID s)] -> Map Node (BlockID s)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Node] -> [BlockID s] -> [(Node, BlockID s)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Node]
nodes (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID (Block ext s ret -> BlockID s) -> [Block ext s ret] -> [BlockID s]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Block ext s ret]
blocks))
    edges :: [LEdge ()]
edges = Block ext s ret -> [LEdge ()]
forall ext s (ret :: CrucibleType). Block ext s ret -> [LEdge ()]
blockEdges       (Block ext s ret -> [LEdge ()]) -> [Block ext s ret] -> [LEdge ()]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Block ext s ret]
blocks

-----------------------------------------
-- | Undefined Value Fixup Transformation
-----------------------------------------

-- | A PartialValue of type @t@ closes over a register of type @Maybe t@
type ValueToPartialMap s  = MapF.MapF (Value s) (PartialValue s)
newtype PartialValue s tp = PartialValue { forall s (tp :: CrucibleType).
PartialValue s tp -> Reg s (MaybeType tp)
getPartial :: Reg s (MaybeType tp) }

type AtomSubst s = MapF.MapF (Atom s :: CrucibleType -> Type)
                              (Atom s :: CrucibleType -> Type)
type AtomPair s  = MapF.Pair (Atom s :: CrucibleType -> Type)
                              (Atom s :: CrucibleType -> Type)

-- | Undefined Value Fixup pass
-- The merge-block insertion process introduces infeasible paths along which
-- some registers may be undefined: this will later be interpreted as a block
-- input in the SSA transformation. To avoid this, we introduce a pass to
-- replace registers/atoms that may be undefined along some path with a partial
-- register (i.e. of type Maybe t).
--
-- Assuming that the input CFG has no paths along which a value is
-- read before being written, the paths along which the reference is
-- read but never written are a subset of the infeasible paths.
lowerUndefPass :: (Monad m, TraverseExt ext)
               => NonceGenerator m s
               -> Label s
               -> CFG ext s init ret
               -> m (CFG ext s init ret)
lowerUndefPass :: forall (m :: Type -> Type) ext s (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> Label s -> CFG ext s init ret -> m (CFG ext s init ret)
lowerUndefPass NonceGenerator m s
ng Label s
rootLabel CFG ext s init ret
cfg =
  do (ValueToPartialMap s
pvals, Seq (Posd (Stmt ext s))
refInits) <- NonceGenerator m s
-> CFG ext s init ret
-> m (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> CFG ext s init ret
-> m (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
mkPartialRegMap NonceGenerator m s
ng CFG ext s init ret
cfg

     let root' :: Block ext s ret
root' = 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 (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
root) (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockExtraInputs Block ext s ret
root) (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
root Seq (Posd (Stmt ext s))
-> Seq (Posd (Stmt ext s)) -> Seq (Posd (Stmt ext s))
forall a. Semigroup a => a -> a -> a
<> Seq (Posd (Stmt ext s))
refInits) (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
root)
     let lower :: Block ext s ret -> m (Block ext s ret)
lower Block ext s ret
blk
           | Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
blk BlockID s -> BlockID s -> Bool
forall a. Eq a => a -> a -> Bool
== Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
rootLabel
           = Block ext s ret -> m (Block ext s ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Block ext s ret
root'
           | Bool
otherwise
           = NonceGenerator m s
-> ValueToPartialMap s -> Block ext s ret -> m (Block ext s ret)
forall s (m :: Type -> Type) ext (ret :: CrucibleType).
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s -> Block ext s ret -> m (Block ext s ret)
lowerBlock NonceGenerator m s
ng ValueToPartialMap s
pvals Block ext s ret
blk

     [Block ext s ret]
blks' <- (Block ext s ret -> m (Block ext s ret))
-> [Block ext s ret] -> m [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 Block ext s ret -> m (Block ext s ret)
lower (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
cfg)
     let cfg' :: CFG ext s init ret
cfg' = CFG ext s init ret
cfg { cfgBlocks = blks' }
     CFG ext s init ret -> m (CFG ext s init ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return CFG ext s init ret
cfg'
  where
    root :: Block ext s ret
root = Block ext s ret -> Maybe (Block ext s ret) -> Block ext s ret
forall a. a -> Maybe a -> a
fromMaybe Block ext s ret
forall {a}. a
err (Maybe (Block ext s ret) -> Block ext s ret)
-> Maybe (Block ext s ret) -> Block ext s ret
forall a b. (a -> b) -> a -> b
$ CFG ext s init ret -> Label s -> Maybe (Block ext s ret)
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Label s -> Maybe (Block ext s ret)
findBlock CFG ext s init ret
cfg Label s
rootLabel
    err :: a
err  = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"EarlyMergeLoops.lowerUndefPass"
                 [ String
"Root block not found in cfg" ]

-- | Fixup the reads and writes in a block. This means, for each value in the domain
-- of the @ValueToPartialMap@ argument,
-- 1. If the value is read, then find the associated partial value register and read that instead
-- 2. Dually, if the value is written, then write that value to the associated partial value register.
lowerBlock :: forall s m ext ret
            . (Monad m, TraverseExt ext)
           => NonceGenerator m s
           -> ValueToPartialMap s
           -> Block ext s ret
           -> m (Block ext s ret)
lowerBlock :: forall s (m :: Type -> Type) ext (ret :: CrucibleType).
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s -> Block ext s ret -> m (Block ext s ret)
lowerBlock NonceGenerator m s
ng ValueToPartialMap s
pvals Block ext s ret
blk =
  do -- If this is a lambda block, treat the associated atom as a write to that atom.
     Seq (Posd (Stmt ext s))
initInputs               <- NonceGenerator m s
-> ValueToPartialMap s
-> Block ext s ret
-> m (Seq (Posd (Stmt ext s)))
forall s (m :: Type -> Type) ext (ret :: CrucibleType).
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> Block ext s ret
-> m (Seq (Posd (Stmt ext s)))
lowerBlockIDValues NonceGenerator m s
ng ValueToPartialMap s
pvals Block ext s ret
blk
     -- Dually, any values passed to a successor should be treated as reads
     (Seq (Posd (Stmt ext s))
preOutput, Posd (TermStmt s ret)
loweredTerm) <- NonceGenerator m s
-> ValueToPartialMap s
-> Block ext s ret
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall s (m :: Type -> Type) ext (ret :: CrucibleType).
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> Block ext s ret
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
lowerTermStmtValues NonceGenerator m s
ng ValueToPartialMap s
pvals Block ext s ret
blk
     -- Fix the reads and writes in the body of this block
     Seq (Posd (Stmt ext s))
lowered <- (Posd (Stmt ext s) -> m (Seq (Posd (Stmt ext s))))
-> Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a b. Monad m => (a -> m (Seq b)) -> Seq a -> m (Seq b)
concatMapSeqM (Posd (Stmt ext s) -> m (Seq (Posd (Stmt ext s)))
lowerReads (Posd (Stmt ext s) -> m (Seq (Posd (Stmt ext s))))
-> (Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s))))
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Posd (Stmt ext s) -> m (Seq (Posd (Stmt ext s))))
-> Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a b. Monad m => (a -> m (Seq b)) -> Seq a -> m (Seq b)
concatMapSeqM Posd (Stmt ext s) -> m (Seq (Posd (Stmt ext s)))
lowerWrites) (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
blk)
     Block ext s ret -> m (Block ext s ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Block ext s ret -> m (Block ext s ret))
-> Block ext s ret -> m (Block ext s ret)
forall a b. (a -> b) -> a -> b
$ 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 (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
blk) (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockExtraInputs Block ext s ret
blk) (Seq (Posd (Stmt ext s))
initInputs Seq (Posd (Stmt ext s))
-> Seq (Posd (Stmt ext s)) -> Seq (Posd (Stmt ext s))
forall a. Semigroup a => a -> a -> a
<> Seq (Posd (Stmt ext s))
lowered Seq (Posd (Stmt ext s))
-> Seq (Posd (Stmt ext s)) -> Seq (Posd (Stmt ext s))
forall a. Semigroup a => a -> a -> a
<> Seq (Posd (Stmt ext s))
preOutput) Posd (TermStmt s ret)
loweredTerm
  where
    lowerWrites :: Posd (Stmt ext s) -> m (Seq (Posd (Stmt ext s)))
lowerWrites = NonceGenerator m s
-> ValueToPartialMap s
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerValueWrites NonceGenerator m s
ng ValueToPartialMap s
pvals
    lowerReads :: Posd (Stmt ext s) -> m (Seq (Posd (Stmt ext s)))
lowerReads  = NonceGenerator m s
-> ValueToPartialMap s
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerValueReads NonceGenerator m s
ng ValueToPartialMap s
pvals

    concatMapSeqM :: Monad m => (a -> m (Seq b)) -> Seq a -> m (Seq b)
    concatMapSeqM :: forall a b. Monad m => (a -> m (Seq b)) -> Seq a -> m (Seq b)
concatMapSeqM a -> m (Seq b)
f Seq a
seq0 =
      (a -> Seq b -> m (Seq b)) -> Seq b -> Seq a -> m (Seq b)
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
Fold.foldrM (\a
s Seq b
ss -> a -> m (Seq b)
f a
s m (Seq b) -> m (Seq b -> Seq b) -> m (Seq b)
forall (f :: Type -> Type) a b.
Applicative f =>
f a -> f (a -> b) -> f b
<**> (Seq b -> Seq b) -> m (Seq b -> Seq b)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Seq b -> Seq b -> Seq b
forall a. Semigroup a => a -> a -> a
<> Seq b
ss)) Seq b
forall a. Monoid a => a
mempty Seq a
seq0

-- | The atom in a lambda ID is essentially an 'atom definition', so
-- we need to check if this lambda's atom needs to be 'lowered'.
lowerBlockIDValues :: forall s m ext ret
                     . (Monad m, TraverseExt ext)
                    => NonceGenerator m s
                    -> ValueToPartialMap s
                    -> Block ext s ret
                    -> m (Seq (Posd (Stmt ext s)))
lowerBlockIDValues :: forall s (m :: Type -> Type) ext (ret :: CrucibleType).
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> Block ext s ret
-> m (Seq (Posd (Stmt ext s)))
lowerBlockIDValues NonceGenerator m s
ng ValueToPartialMap s
pvals Block ext s ret
blk = 
  case Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
blk of
    LambdaID (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom -> Atom s tp
a)
      | Just (PartialValue s tp -> Reg s (MaybeType tp)
forall s (tp :: CrucibleType).
PartialValue s tp -> Reg s (MaybeType tp)
getPartial -> Reg s (MaybeType tp)
pr) <- Value s tp -> ValueToPartialMap s -> Maybe (PartialValue s tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) ValueToPartialMap s
pvals ->
        do Atom s (MaybeType tp)
pa <- NonceGenerator m s
-> Position -> TypeRepr (MaybeType tp) -> m (Atom s (MaybeType tp))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng (Atom s tp -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s tp
a) (TypeRepr tp -> TypeRepr (MaybeType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a))
           let setPa :: Posd (Stmt ext s)
setPa = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd (Atom s tp -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s tp
a) (Atom s (MaybeType tp)
-> AtomValue ext s (MaybeType tp) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s (MaybeType tp)
pa (App ext (Atom s) (MaybeType tp) -> AtomValue ext s (MaybeType tp)
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (TypeRepr tp -> Atom s tp -> App ext (Atom s) (MaybeType tp)
forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp1 -> f tp1 -> App ext f ('MaybeType tp1)
JustValue (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a) Atom s tp
a)))
               setPr :: Posd (Stmt ext s)
setPr = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd (Atom s tp -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s tp
a) (Reg s (MaybeType tp) -> Atom s (MaybeType tp) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Reg s tp -> Atom s tp -> Stmt ext s
SetReg Reg s (MaybeType tp)
pr Atom s (MaybeType tp)
pa)
           Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s))))
-> Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a b. (a -> b) -> a -> b
$ [Posd (Stmt ext s)] -> Seq (Posd (Stmt ext s))
forall a. [a] -> Seq a
Seq.fromList [ Posd (Stmt ext s)
setPa, Posd (Stmt ext s)
setPr ]
      | Bool
otherwise ->
        -- Not in our list of values to lower
        Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Seq (Posd (Stmt ext s))
forall a. Monoid a => a
mempty
    LabelID {} ->
      -- No atoms defined
      Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Seq (Posd (Stmt ext s))
forall a. Monoid a => a
mempty

-- | Jumping to a block with a value a la Output is akin to
-- 'reading' the atom, so if we already lifted the original value
-- of type T to a (Maybe T), we need to convert it back to a T
-- here.
lowerTermStmtValues :: forall s m ext ret
                     . (Monad m, TraverseExt ext)
                    => NonceGenerator m s
                    -> ValueToPartialMap s
                    -> Block ext s ret
                    -> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
lowerTermStmtValues :: forall s (m :: Type -> Type) ext (ret :: CrucibleType).
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> Block ext s ret
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
lowerTermStmtValues NonceGenerator m s
ng ValueToPartialMap s
pvals Block ext s ret
blk =
  case Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val (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
blk) of
    Output LambdaLabel s tp
ll Atom s tp
a          -> Atom s tp
-> (Atom s tp -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall (tp :: CrucibleType) (ty :: CrucibleType).
Atom s tp
-> (Atom s tp -> TermStmt s ty)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ty))
withLowered Atom s tp
a ((Atom s tp -> TermStmt s ret)
 -> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret)))
-> (Atom s tp -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall a b. (a -> b) -> a -> b
$ LambdaLabel s tp -> Atom s tp -> TermStmt s ret
forall s (tp :: CrucibleType) (ret :: CrucibleType).
LambdaLabel s tp -> Atom s tp -> TermStmt s ret
Output LambdaLabel s tp
ll
    MaybeBranch TypeRepr tp
t Atom s (MaybeType tp)
a LambdaLabel s tp
ll Label s
l -> Atom s (MaybeType tp)
-> (Atom s (MaybeType tp) -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall (tp :: CrucibleType) (ty :: CrucibleType).
Atom s tp
-> (Atom s tp -> TermStmt s ty)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ty))
withLowered Atom s (MaybeType tp)
a ((Atom s (MaybeType tp) -> TermStmt s ret)
 -> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret)))
-> (Atom s (MaybeType tp) -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall a b. (a -> b) -> a -> b
$ \Atom s (MaybeType tp)
a' -> TypeRepr tp
-> Atom s (MaybeType tp)
-> LambdaLabel s tp
-> Label s
-> TermStmt s ret
forall (tp :: CrucibleType) s (ret :: CrucibleType).
TypeRepr tp
-> Atom s (MaybeType tp)
-> LambdaLabel s tp
-> Label s
-> TermStmt s ret
MaybeBranch TypeRepr tp
t Atom s (MaybeType tp)
a' LambdaLabel s tp
ll Label s
l
    Return Atom s ret
a             -> Atom s ret
-> (Atom s ret -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall (tp :: CrucibleType) (ty :: CrucibleType).
Atom s tp
-> (Atom s tp -> TermStmt s ty)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ty))
withLowered Atom s ret
a ((Atom s ret -> TermStmt s ret)
 -> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret)))
-> (Atom s ret -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall a b. (a -> b) -> a -> b
$ Atom s ret -> TermStmt s ret
forall s (ret :: CrucibleType). Atom s ret -> TermStmt s ret
Return
    TailCall Atom s (FunctionHandleType args ret)
f CtxRepr args
c Assignment (Atom s) args
a       -> Atom s (FunctionHandleType args ret)
-> (Atom s (FunctionHandleType args ret) -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall (tp :: CrucibleType) (ty :: CrucibleType).
Atom s tp
-> (Atom s tp -> TermStmt s ty)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ty))
withLowered Atom s (FunctionHandleType args ret)
f ((Atom s (FunctionHandleType args ret) -> TermStmt s ret)
 -> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret)))
-> (Atom s (FunctionHandleType args ret) -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall a b. (a -> b) -> a -> b
$ \Atom s (FunctionHandleType args ret)
f' -> Atom s (FunctionHandleType args ret)
-> CtxRepr args -> Assignment (Atom s) args -> TermStmt s ret
forall s (args :: Ctx CrucibleType) (ret :: CrucibleType).
Atom s (FunctionHandleType args ret)
-> CtxRepr args -> Assignment (Atom s) args -> TermStmt s ret
TailCall Atom s (FunctionHandleType args ret)
f' CtxRepr args
c Assignment (Atom s) args
a
    ErrorStmt Atom s (StringType Unicode)
msg        -> Atom s (StringType Unicode)
-> (Atom s (StringType Unicode) -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall (tp :: CrucibleType) (ty :: CrucibleType).
Atom s tp
-> (Atom s tp -> TermStmt s ty)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ty))
withLowered Atom s (StringType Unicode)
msg ((Atom s (StringType Unicode) -> TermStmt s ret)
 -> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret)))
-> (Atom s (StringType Unicode) -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall a b. (a -> b) -> a -> b
$ Atom s (StringType Unicode) -> TermStmt s ret
forall s (ret :: CrucibleType).
Atom s (StringType Unicode) -> TermStmt s ret
ErrorStmt
    VariantElim CtxRepr varctx
c Atom s (VariantType varctx)
a Assignment (LambdaLabel s) varctx
ls   -> Atom s (VariantType varctx)
-> (Atom s (VariantType varctx) -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall (tp :: CrucibleType) (ty :: CrucibleType).
Atom s tp
-> (Atom s tp -> TermStmt s ty)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ty))
withLowered Atom s (VariantType varctx)
a ((Atom s (VariantType varctx) -> TermStmt s ret)
 -> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret)))
-> (Atom s (VariantType varctx) -> TermStmt s ret)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall a b. (a -> b) -> a -> b
$ \Atom s (VariantType varctx)
a' -> CtxRepr varctx
-> Atom s (VariantType varctx)
-> Assignment (LambdaLabel s) varctx
-> TermStmt s ret
forall (varctx :: Ctx CrucibleType) s (ret :: CrucibleType).
CtxRepr varctx
-> Atom s (VariantType varctx)
-> Assignment (LambdaLabel s) varctx
-> TermStmt s ret
VariantElim CtxRepr varctx
c Atom s (VariantType varctx)
a' Assignment (LambdaLabel s) varctx
ls
    -- No atoms are output/read
    Jump {}              -> (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (Posd (Stmt ext s))
forall a. Monoid a => a
mempty, 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
blk)
    Br {}                -> (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ret))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (Posd (Stmt ext s))
forall a. Monoid a => a
mempty, 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
blk)

  where
    termPos :: Position
termPos = Posd (TermStmt s ret) -> Position
forall v. Posd v -> Position
pos (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
blk)
    withLowered :: forall (tp :: CrucibleType) ty.
                   Atom s tp
                -> (Atom s tp -> TermStmt s ty) -> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ty))
    withLowered :: forall (tp :: CrucibleType) (ty :: CrucibleType).
Atom s tp
-> (Atom s tp -> TermStmt s ty)
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ty))
withLowered Atom s tp
a Atom s tp -> TermStmt s ty
k =
      do (Seq (Posd (Stmt ext s))
setAtom, Atom s tp
a') <- Position -> Atom s tp -> m (Seq (Posd (Stmt ext s)), Atom s tp)
forall (tp :: CrucibleType).
Position -> Atom s tp -> m (Seq (Posd (Stmt ext s)), Atom s tp)
lowerAtomRead Position
termPos Atom s tp
a
         (Seq (Posd (Stmt ext s)), Posd (TermStmt s ty))
-> m (Seq (Posd (Stmt ext s)), Posd (TermStmt s ty))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (Posd (Stmt ext s))
setAtom, Position -> TermStmt s ty -> Posd (TermStmt s ty)
forall v. Position -> v -> Posd v
Posd Position
termPos (Atom s tp -> TermStmt s ty
k Atom s tp
a'))

    lowerAtomRead :: forall (tp :: CrucibleType). Position -> Atom s tp -> m (Seq (Posd (Stmt ext s)), Atom s tp)
    lowerAtomRead :: forall (tp :: CrucibleType).
Position -> Atom s tp -> m (Seq (Posd (Stmt ext s)), Atom s tp)
lowerAtomRead Position
p Atom s tp
a =
        do ([AtomPair s]
sub, [Stmt ext s]
setValue) <- NonceGenerator m s
-> ValueToPartialMap s
-> Some (Atom s)
-> m ([AtomPair s], [Stmt ext s])
forall (m :: Type -> Type) s ext.
Monad m =>
NonceGenerator m s
-> ValueToPartialMap s
-> Some (Atom s)
-> m ([AtomPair s], [Stmt ext s])
lowerAtom NonceGenerator m s
ng ValueToPartialMap s
pvals (Atom s tp -> Some (Atom s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Atom s tp
a)
           let a' :: Atom s tp
a' = AtomSubst s -> forall (tp :: CrucibleType). Atom s tp -> Atom s tp
forall s.
AtomSubst s -> forall (tp :: CrucibleType). Atom s tp -> Atom s tp
apSubst ([AtomPair s] -> AtomSubst s
forall s. [Pair (Atom s) (Atom s)] -> AtomSubst s
atomSubst [AtomPair s]
sub) Atom s tp
a
           (Seq (Posd (Stmt ext s)), Atom s tp)
-> m (Seq (Posd (Stmt ext s)), Atom s tp)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Seq (Posd (Stmt ext s)), Atom s tp)
 -> m (Seq (Posd (Stmt ext s)), Atom s tp))
-> (Seq (Posd (Stmt ext s)), Atom s tp)
-> m (Seq (Posd (Stmt ext s)), Atom s tp)
forall a b. (a -> b) -> a -> b
$ (Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd Position
p (Stmt ext s -> Posd (Stmt ext s))
-> Seq (Stmt ext s) -> Seq (Posd (Stmt ext s))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Stmt ext s] -> Seq (Stmt ext s)
forall a. [a] -> Seq a
Seq.fromList [Stmt ext s]
setValue, Atom s tp
a')
      

-- | Replace each write of a possibly-undef atom/register to a write of the
-- associated partial register by injecting it into a value of Maybe type.
lowerValueWrites :: forall m ext s. (Monad m, TraverseExt ext)
                 => NonceGenerator m s
                 -> ValueToPartialMap s
                 -> Posd (Stmt ext s)
                 -> m (Seq (Posd (Stmt ext s)))
lowerValueWrites :: forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerValueWrites NonceGenerator m s
ng ValueToPartialMap s
pvals Posd (Stmt ext s)
st =
  case Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
st of
   -- Replace r := a (morally) with pr := Just a,
   -- where pr is the partial register associated with r
   SetReg Reg s tp
r Atom s tp
a
     | Just (PartialValue s tp -> Reg s (MaybeType tp)
forall s (tp :: CrucibleType).
PartialValue s tp -> Reg s (MaybeType tp)
getPartial -> Reg s (MaybeType tp)
pr) <- Value s tp -> ValueToPartialMap s -> Maybe (PartialValue s tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup (Reg s tp -> Value s tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue Reg s tp
r) ValueToPartialMap s
pvals ->
         Reg s (MaybeType tp)
-> Atom s tp -> TypeRepr tp -> m (Seq (Posd (Stmt ext s)))
forall (tp :: CrucibleType).
Reg s (MaybeType tp)
-> Atom s tp -> TypeRepr tp -> m (Seq (Posd (Stmt ext s)))
setMaybeAtom Reg s (MaybeType tp)
pr Atom s tp
a (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a)
     | Bool
otherwise -> m (Seq (Posd (Stmt ext s)))
orig

   -- Given a := v, append pr := Just(a) where pr is the
   -- partial register associated with a
   DefineAtom Atom s tp
a AtomValue ext s tp
_
     | Just (PartialValue s tp -> Reg s (MaybeType tp)
forall s (tp :: CrucibleType).
PartialValue s tp -> Reg s (MaybeType tp)
getPartial -> Reg s (MaybeType tp)
pr) <- Value s tp -> ValueToPartialMap s -> Maybe (PartialValue s tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) ValueToPartialMap s
pvals ->
       do Seq (Posd (Stmt ext s))
setA' <- Reg s (MaybeType tp)
-> Atom s tp -> TypeRepr tp -> m (Seq (Posd (Stmt ext s)))
forall (tp :: CrucibleType).
Reg s (MaybeType tp)
-> Atom s tp -> TypeRepr tp -> m (Seq (Posd (Stmt ext s)))
setMaybeAtom Reg s (MaybeType tp)
pr Atom s tp
a (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a)
          Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Posd (Stmt ext s)
st Posd (Stmt ext s)
-> Seq (Posd (Stmt ext s)) -> Seq (Posd (Stmt ext s))
forall a. a -> Seq a -> Seq a
Seq.<| Seq (Posd (Stmt ext s))
setA')
     | Bool
otherwise -> m (Seq (Posd (Stmt ext s)))
orig

   -- No registers set or atoms defined:
   WriteGlobal {} -> m (Seq (Posd (Stmt ext s)))
orig
   WriteRef {}    -> m (Seq (Posd (Stmt ext s)))
orig
   DropRef {}     -> m (Seq (Posd (Stmt ext s)))
orig
   Print {}       -> m (Seq (Posd (Stmt ext s)))
orig
   Assert {}      -> m (Seq (Posd (Stmt ext s)))
orig
   Assume {}      -> m (Seq (Posd (Stmt ext s)))
orig
   Breakpoint {}  -> m (Seq (Posd (Stmt ext s)))
orig

  where
    orig :: m (Seq (Posd (Stmt ext s)))
orig = Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Posd (Stmt ext s)] -> Seq (Posd (Stmt ext s))
forall a. [a] -> Seq a
Seq.fromList [Posd (Stmt ext s)
st])

    -- Construct (pa := Just a; pr := pa) where pa is fresh
    setMaybeAtom :: forall (tp :: CrucibleType).
                    Reg s (MaybeType tp) -> Atom s tp -> TypeRepr tp -> m (Seq (Posd (Stmt ext s)))
    setMaybeAtom :: forall (tp :: CrucibleType).
Reg s (MaybeType tp)
-> Atom s tp -> TypeRepr tp -> m (Seq (Posd (Stmt ext s)))
setMaybeAtom Reg s (MaybeType tp)
pr Atom s tp
a TypeRepr tp
ty =
       do Atom s (MaybeType tp)
pa <- NonceGenerator m s
-> Position -> TypeRepr (MaybeType tp) -> m (Atom s (MaybeType tp))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng (Atom s tp -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s tp
a) (TypeRepr tp -> TypeRepr (MaybeType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr TypeRepr tp
ty)
          let setPa :: Posd (Stmt ext s)
setPa = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd (Posd (Stmt ext s) -> Position
forall v. Posd v -> Position
pos Posd (Stmt ext s)
st) (Atom s (MaybeType tp)
-> AtomValue ext s (MaybeType tp) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s (MaybeType tp)
pa (App ext (Atom s) (MaybeType tp) -> AtomValue ext s (MaybeType tp)
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (TypeRepr tp -> Atom s tp -> App ext (Atom s) (MaybeType tp)
forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp1 -> f tp1 -> App ext f ('MaybeType tp1)
JustValue TypeRepr tp
ty Atom s tp
a)))
              setPr :: Posd (Stmt ext s)
setPr = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd (Posd (Stmt ext s) -> Position
forall v. Posd v -> Position
pos Posd (Stmt ext s)
st) (Reg s (MaybeType tp) -> Atom s (MaybeType tp) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Reg s tp -> Atom s tp -> Stmt ext s
SetReg Reg s (MaybeType tp)
pr Atom s (MaybeType tp)
pa)
          Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s))))
-> Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a b. (a -> b) -> a -> b
$ [Posd (Stmt ext s)] -> Seq (Posd (Stmt ext s))
forall a. [a] -> Seq a
Seq.fromList [ Posd (Stmt ext s)
setPa, Posd (Stmt ext s)
setPr ]

-- | Replace each read of a lowered atom/register to a read of the
-- associated register + projection from Maybe
lowerValueReads :: forall m ext s
                . (Monad m, TraverseExt ext)
                => NonceGenerator m s
                -> ValueToPartialMap s
                -> Posd (Stmt ext s)
                -> m (Seq (Posd (Stmt ext s)))
lowerValueReads :: forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerValueReads NonceGenerator m s
ng ValueToPartialMap s
pvals Posd (Stmt ext s)
st =
  case Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
st of
    -- RegReads have only one form
    DefineAtom Atom s tp
a (ReadReg Reg s tp
r)
     | Just (PartialValue s tp -> Reg s (MaybeType tp)
forall s (tp :: CrucibleType).
PartialValue s tp -> Reg s (MaybeType tp)
getPartial -> Reg s (MaybeType tp)
pr) <- Value s tp -> ValueToPartialMap s -> Maybe (PartialValue s tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup (Reg s tp -> Value s tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue Reg s tp
r) ValueToPartialMap s
pvals ->
       NonceGenerator m s
-> Position
-> Atom s tp
-> Reg s (MaybeType tp)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) s (tp :: CrucibleType) ext.
Monad m =>
NonceGenerator m s
-> Position
-> Atom s tp
-> Reg s (MaybeType tp)
-> m (Seq (Posd (Stmt ext s)))
lowerRegRead NonceGenerator m s
ng (Posd (Stmt ext s) -> Position
forall v. Posd v -> Position
pos Posd (Stmt ext s)
st) Atom s tp
a Reg s (MaybeType tp)
pr
    -- For everything else, we need to check if any of the
    -- referenced atoms need to be lowered
    DefineAtom {}  -> NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerAtomReads NonceGenerator m s
ng ValueToPartialMap s
pvals [Some (Atom s)]
atomsToLower Posd (Stmt ext s)
st
    SetReg {}      -> NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerAtomReads NonceGenerator m s
ng ValueToPartialMap s
pvals [Some (Atom s)]
atomsToLower Posd (Stmt ext s)
st
    WriteGlobal {} -> NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerAtomReads NonceGenerator m s
ng ValueToPartialMap s
pvals [Some (Atom s)]
atomsToLower Posd (Stmt ext s)
st
    WriteRef {}    -> NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerAtomReads NonceGenerator m s
ng ValueToPartialMap s
pvals [Some (Atom s)]
atomsToLower Posd (Stmt ext s)
st
    DropRef {}     -> NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerAtomReads NonceGenerator m s
ng ValueToPartialMap s
pvals [Some (Atom s)]
atomsToLower Posd (Stmt ext s)
st
    Print {}       -> NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerAtomReads NonceGenerator m s
ng ValueToPartialMap s
pvals [Some (Atom s)]
atomsToLower Posd (Stmt ext s)
st
    Assert {}      -> NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerAtomReads NonceGenerator m s
ng ValueToPartialMap s
pvals [Some (Atom s)]
atomsToLower Posd (Stmt ext s)
st
    Assume {}      -> NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerAtomReads NonceGenerator m s
ng ValueToPartialMap s
pvals [Some (Atom s)]
atomsToLower Posd (Stmt ext s)
st
    Breakpoint {}  -> NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerAtomReads NonceGenerator m s
ng ValueToPartialMap s
pvals [Some (Atom s)]
atomsToLower Posd (Stmt ext s)
st
  where
    atomsToLower :: [Some (Atom s)]
    atomsToLower :: [Some (Atom s)]
atomsToLower = Set (Some (Atom s)) -> [Some (Atom s)]
forall a. Set a -> [a]
Set.toList ((forall (x :: CrucibleType).
 Value s x -> Set (Some (Atom s)) -> Set (Some (Atom s)))
-> Stmt ext s -> Set (Some (Atom s)) -> Set (Some (Atom s))
forall ext s b.
TraverseExt ext =>
(forall (x :: CrucibleType). Value s x -> b -> b)
-> Stmt ext s -> b -> b
foldStmtInputs Value s x -> Set (Some (Atom s)) -> Set (Some (Atom s))
forall (x :: CrucibleType).
Value s x -> Set (Some (Atom s)) -> Set (Some (Atom s))
addIfLowered (Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
st) Set (Some (Atom s))
forall a. Monoid a => a
mempty)

    addIfLowered :: forall tp. Value s tp -> Set.Set (Some (Atom s)) -> Set.Set (Some (Atom s))
    addIfLowered :: forall (x :: CrucibleType).
Value s x -> Set (Some (Atom s)) -> Set (Some (Atom s))
addIfLowered v :: Value s tp
v@(AtomValue Atom s tp
a) Set (Some (Atom s))
s
      | Value s tp -> ValueToPartialMap s -> Bool
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Bool
MapF.member Value s tp
v ValueToPartialMap s
pvals = Some (Atom s) -> Set (Some (Atom s)) -> Set (Some (Atom s))
forall a. Ord a => a -> Set a -> Set a
Set.insert (Atom s tp -> Some (Atom s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Atom s tp
a) Set (Some (Atom s))
s
    addIfLowered Value s tp
_ Set (Some (Atom s))
s = Set (Some (Atom s))
s

-- | Replace each read of a lowered atom to a read of the
-- associated register + projection from Maybe
lowerAtomReads :: forall m ext s.
                  (Monad m, TraverseExt ext)
               => NonceGenerator m s
               -> ValueToPartialMap s
               -> [Some (Atom s)]
               -> Posd (Stmt ext s)
               -> m (Seq (Posd (Stmt ext s)))
lowerAtomReads :: forall (m :: Type -> Type) ext s.
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> ValueToPartialMap s
-> [Some (Atom s)]
-> Posd (Stmt ext s)
-> m (Seq (Posd (Stmt ext s)))
lowerAtomReads NonceGenerator m s
ng ValueToPartialMap s
pvals [Some (Atom s)]
atomsToLower Posd (Stmt ext s)
st =
  do ([[AtomPair s]]
substs, [[Stmt ext s]]
readRegs) <- [([AtomPair s], [Stmt ext s])] -> ([[AtomPair s]], [[Stmt ext s]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([([AtomPair s], [Stmt ext s])]
 -> ([[AtomPair s]], [[Stmt ext s]]))
-> m [([AtomPair s], [Stmt ext s])]
-> m ([[AtomPair s]], [[Stmt ext s]])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Some (Atom s) -> m ([AtomPair s], [Stmt ext s]))
-> [Some (Atom s)] -> m [([AtomPair s], [Stmt ext s])]
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 (NonceGenerator m s
-> ValueToPartialMap s
-> Some (Atom s)
-> m ([AtomPair s], [Stmt ext s])
forall (m :: Type -> Type) s ext.
Monad m =>
NonceGenerator m s
-> ValueToPartialMap s
-> Some (Atom s)
-> m ([AtomPair s], [Stmt ext s])
lowerAtom NonceGenerator m s
ng ValueToPartialMap s
pvals) [Some (Atom s)]
atomsToLower
     let substMap :: AtomSubst s
substMap        = [AtomPair s] -> AtomSubst s
forall s. [Pair (Atom s) (Atom s)] -> AtomSubst s
atomSubst ([[AtomPair s]] -> [AtomPair s]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [[AtomPair s]]
substs)
     Stmt ext s
st'                <- (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Stmt ext s -> m (Stmt ext s)
forall (m :: Type -> Type) ext s.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Stmt ext s -> m (Stmt ext s)
mapStmtAtom (Atom s x -> m (Atom s x)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Atom s x -> m (Atom s x))
-> (Atom s x -> Atom s x) -> Atom s x -> m (Atom s x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomSubst s -> forall (tp :: CrucibleType). Atom s tp -> Atom s tp
forall s.
AtomSubst s -> forall (tp :: CrucibleType). Atom s tp -> Atom s tp
apSubst AtomSubst s
substMap) (Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
st)
     let stmts :: Seq (Posd (Stmt ext s))
stmts           = [Posd (Stmt ext s)] -> Seq (Posd (Stmt ext s))
forall a. [a] -> Seq a
Seq.fromList (Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd (Posd (Stmt ext s) -> Position
forall v. Posd v -> Position
pos Posd (Stmt ext s)
st) (Stmt ext s -> Posd (Stmt ext s))
-> [Stmt ext s] -> [Posd (Stmt ext s)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ([[Stmt ext s]] -> [Stmt ext s]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [[Stmt ext s]]
readRegs [Stmt ext s] -> [Stmt ext s] -> [Stmt ext s]
forall a. [a] -> [a] -> [a]
++ [Stmt ext s
st']))
     Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Seq (Posd (Stmt ext s))
stmts

apSubst :: AtomSubst s -> (forall (tp :: CrucibleType). Atom s tp -> Atom s tp)
apSubst :: forall s.
AtomSubst s -> forall (tp :: CrucibleType). Atom s tp -> Atom s tp
apSubst AtomSubst s
sub Atom s tp
n = Atom s tp -> Maybe (Atom s tp) -> Atom s tp
forall a. a -> Maybe a -> a
fromMaybe Atom s tp
n (Maybe (Atom s tp) -> Atom s tp) -> Maybe (Atom s tp) -> Atom s tp
forall a b. (a -> b) -> a -> b
$ Atom s tp -> AtomSubst s -> Maybe (Atom s tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup Atom s tp
n AtomSubst s
sub

atomSubst :: [MapF.Pair (Atom s :: CrucibleType -> Type) (Atom s)] -> AtomSubst s
atomSubst :: forall s. [Pair (Atom s) (Atom s)] -> AtomSubst s
atomSubst [Pair (Atom s) (Atom s)]
substs = [Pair (Atom s) (Atom s)] -> MapF (Atom s) (Atom s)
forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
[Pair k a] -> MapF k a
MapF.fromList [Pair (Atom s) (Atom s)]
substs

-- | Given an atom @a@ of type @t@ whose definition we've already
-- replaced with a register @r@ of type @Maybe t@, produce the
-- statements to
-- 1. read @r@ into a fresh @a'@
-- 2. set fresh @a''@ to @fromJust a'@
-- returns a mapping from @a@ to @a'@ and the above
lowerAtom :: forall m s ext.
             Monad m
          => NonceGenerator m s
          -> ValueToPartialMap s
          -> Some (Atom s)
          -> m ([AtomPair s], [Stmt ext s])
lowerAtom :: forall (m :: Type -> Type) s ext.
Monad m =>
NonceGenerator m s
-> ValueToPartialMap s
-> Some (Atom s)
-> m ([AtomPair s], [Stmt ext s])
lowerAtom NonceGenerator m s
ng ValueToPartialMap s
pvals (Some Atom s x
a)
  | Just (PartialValue s x -> Reg s (MaybeType x)
forall s (tp :: CrucibleType).
PartialValue s tp -> Reg s (MaybeType tp)
getPartial -> Reg s (MaybeType x)
r) <- Value s x -> ValueToPartialMap s -> Maybe (PartialValue s x)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup (Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s x
a) ValueToPartialMap s
pvals =
      do Atom s x
a'  <- (forall (x :: CrucibleType). Nonce s x -> m (Nonce s x))
-> Atom s x -> m (Atom s x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom (m (Nonce s x) -> Nonce s x -> m (Nonce s x)
forall a b. a -> b -> a
const (NonceGenerator m s -> m (Nonce s x)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng)) Atom s x
a
         Atom s (StringType Unicode)
str <- NonceGenerator m s
-> Position
-> TypeRepr (StringType Unicode)
-> m (Atom s (StringType Unicode))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng (Atom s x -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s x
a) TypeRepr (StringType Unicode)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
         Atom s (MaybeType x)
a'' <- NonceGenerator m s
-> Position -> TypeRepr (MaybeType x) -> m (Atom s (MaybeType x))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng (Atom s x -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s x
a) (TypeRepr x -> TypeRepr (MaybeType x)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (Atom s x -> TypeRepr x
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s x
a))
         let defs :: [Stmt ext s]
defs = [ Atom s (MaybeType x) -> AtomValue ext s (MaybeType x) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s (MaybeType x)
a'' (Reg s (MaybeType x) -> AtomValue ext s (MaybeType x)
forall s (tp :: CrucibleType) ext. Reg s tp -> AtomValue ext s tp
ReadReg Reg s (MaybeType x)
r)
                    , Atom s (StringType Unicode)
-> AtomValue ext s (StringType Unicode) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s (StringType Unicode)
str (App ext (Atom s) (StringType Unicode)
-> AtomValue ext s (StringType Unicode)
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (StringLiteral Unicode -> App ext (Atom s) (StringType Unicode)
forall (si :: StringInfo) ext (f :: CrucibleType -> Type).
StringLiteral si -> App ext f ('BaseToType (BaseStringType si))
StringLit (StringLiteral Unicode
"Lower Atom Pass: " StringLiteral Unicode
-> StringLiteral Unicode -> StringLiteral Unicode
forall a. Semigroup a => a -> a -> a
<> String -> StringLiteral Unicode
forall a. IsString a => String -> a
fromString (Nonce s x -> String
forall a. Show a => a -> String
show (Atom s x -> Nonce s x
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s x
a)))))
                    , Atom s x -> AtomValue ext s x -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s x
a'  (App ext (Atom s) x -> AtomValue ext s x
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (TypeRepr x
-> Atom s (MaybeType x)
-> Atom s (StringType Unicode)
-> App ext (Atom s) x
forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp
-> f (MaybeType tp) -> f (StringType Unicode) -> App ext f tp
FromJustValue (Atom s x -> TypeRepr x
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s x
a) Atom s (MaybeType x)
a'' Atom s (StringType Unicode)
str))
                    ]
         ([AtomPair s], [Stmt ext s]) -> m ([AtomPair s], [Stmt ext s])
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([Atom s x -> Atom s x -> AtomPair s
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
MapF.Pair Atom s x
a Atom s x
a'], [Stmt ext s]
defs)
  | Bool
otherwise =
      ([AtomPair s], [Stmt ext s]) -> m ([AtomPair s], [Stmt ext s])
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([], [])

-- | @lowerRegRead ng pos a pr@ constructs @a' := pr; a := fromJust a'@.
lowerRegRead :: Monad m
             => NonceGenerator m s
             -> Position
             -- ^ The position we should use for the new statements
             -> Atom s tp
             -- ^ The atom we're defininig
             -> Reg s (MaybeType tp)
             -- ^ The partial register to read from
             -> m (Seq (Posd (Stmt ext s)))
lowerRegRead :: forall (m :: Type -> Type) s (tp :: CrucibleType) ext.
Monad m =>
NonceGenerator m s
-> Position
-> Atom s tp
-> Reg s (MaybeType tp)
-> m (Seq (Posd (Stmt ext s)))
lowerRegRead NonceGenerator m s
ng Position
p Atom s tp
a Reg s (MaybeType tp)
pr =
  do Atom s (MaybeType tp)
a' <- NonceGenerator m s
-> Position -> TypeRepr (MaybeType tp) -> m (Atom s (MaybeType tp))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng (Atom s tp -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s tp
a) (TypeRepr tp -> TypeRepr (MaybeType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a))
     Atom s (StringType Unicode)
str <- NonceGenerator m s
-> Position
-> TypeRepr (StringType Unicode)
-> m (Atom s (StringType Unicode))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng (Atom s tp -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s tp
a) TypeRepr (StringType Unicode)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
     -- insert a new atom to read the reg, then replace with FromJustVal
     let stmts :: [Stmt ext s]
stmts = [ Atom s (StringType Unicode)
-> AtomValue ext s (StringType Unicode) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s (StringType Unicode)
str (App ext (Atom s) (StringType Unicode)
-> AtomValue ext s (StringType Unicode)
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (StringLiteral Unicode -> App ext (Atom s) (StringType Unicode)
forall (si :: StringInfo) ext (f :: CrucibleType -> Type).
StringLiteral si -> App ext f ('BaseToType (BaseStringType si))
StringLit StringLiteral Unicode
"Lower Register Pass"))
                 , Atom s (MaybeType tp)
-> AtomValue ext s (MaybeType tp) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s (MaybeType tp)
a'  (Reg s (MaybeType tp) -> AtomValue ext s (MaybeType tp)
forall s (tp :: CrucibleType) ext. Reg s tp -> AtomValue ext s tp
ReadReg Reg s (MaybeType tp)
pr)
                 , Atom s tp -> AtomValue ext s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s tp
a   (App ext (Atom s) tp -> AtomValue ext s tp
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (TypeRepr tp
-> Atom s (MaybeType tp)
-> Atom s (StringType Unicode)
-> App ext (Atom s) tp
forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp
-> f (MaybeType tp) -> f (StringType Unicode) -> App ext f tp
FromJustValue (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a) Atom s (MaybeType tp)
a' Atom s (StringType Unicode)
str))
                 ]
     Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s))))
-> Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s)))
forall a b. (a -> b) -> a -> b
$ [Posd (Stmt ext s)] -> Seq (Posd (Stmt ext s))
forall a. [a] -> Seq a
Seq.fromList (Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd Position
p (Stmt ext s -> Posd (Stmt ext s))
-> [Stmt ext s] -> [Posd (Stmt ext s)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Stmt ext s]
stmts)
  
-- | Traverse all dfs paths, avoiding backedges, to find values that may be read but not written.
-- Returns:
--  1. a mapping from values of type @t@ to corresponding registers of type @Maybe t@ 
--  2. statements to initialize the registers mentioned in said mapping.
mkPartialRegMap :: (Monad m, TraverseExt ext)
                => NonceGenerator m s
                -> CFG ext s init ret
                -> m ((ValueToPartialMap s, Seq (Posd (Stmt ext s))))
mkPartialRegMap :: forall (m :: Type -> Type) ext s (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> CFG ext s init ret
-> m (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
mkPartialRegMap NonceGenerator m s
ng CFG ext s init ret
cfg =
  ((ValueToPartialMap s, Seq (Posd (Stmt ext s)))
 -> ValueSet s
 -> Block ext s ret
 -> m ((ValueToPartialMap s, Seq (Posd (Stmt ext s))), ValueSet s))
-> (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
-> ValueSet s
-> Block ext s ret
-> CFG ext s init ret
-> m (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) ext genv penv s (ret :: CrucibleType)
       (init :: Ctx CrucibleType).
(Monad m, TraverseExt ext) =>
(genv -> penv -> Block ext s ret -> m (genv, penv))
-> genv -> penv -> Block ext s ret -> CFG ext s init ret -> m genv
traverseCFG (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
-> ValueSet s
-> Block ext s ret
-> m ((ValueToPartialMap s, Seq (Posd (Stmt ext s))), ValueSet s)
gatherPvals (ValueToPartialMap s
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty, Seq (Posd (Stmt ext s))
forall a. Monoid a => a
mempty) (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockExtraInputs Block ext s ret
entry) Block ext s ret
entry CFG ext s init ret
cfg
  where
    entry :: Block ext s ret
entry = 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
cfgEntryBlock CFG ext s init ret
cfg

    gatherPvals :: (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
-> ValueSet s
-> Block ext s ret
-> m ((ValueToPartialMap s, Seq (Posd (Stmt ext s))), ValueSet s)
gatherPvals (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
pvals ValueSet s
env Block ext s ret
blk =
      do (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
refs'   <- ((ValueToPartialMap s, Seq (Posd (Stmt ext s)))
 -> Some (Value s)
 -> m (ValueToPartialMap s, Seq (Posd (Stmt ext s))))
-> (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
-> ValueSet s
-> m (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
Fold.foldlM (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
-> Some (Value s)
-> m (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
addPval (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
pvals (ValueSet s -> Block ext s ret -> ValueSet s
forall s ext (ret :: CrucibleType).
ValueSet s -> Block ext s ret -> ValueSet s
blockUndefVals ValueSet s
env Block ext s ret
blk)
         ((ValueToPartialMap s, Seq (Posd (Stmt ext s))), ValueSet s)
-> m ((ValueToPartialMap s, Seq (Posd (Stmt ext s))), ValueSet s)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((ValueToPartialMap s, Seq (Posd (Stmt ext s)))
refs', ValueSet s
env ValueSet s -> ValueSet s -> ValueSet s
forall a. Semigroup a => a -> a -> a
<> Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockAssignedValues Block ext s ret
blk)
  
    addPval :: (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
-> Some (Value s)
-> m (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
addPval (ValueToPartialMap s
pvals, Seq (Posd (Stmt ext s))
inits) val :: Some (Value s)
val@(Some Value s x
v)  
      | Just PartialValue s x
_ <- Value s x -> ValueToPartialMap s -> Maybe (PartialValue s x)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup Value s x
v ValueToPartialMap s
pvals
      = (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
-> m (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ValueToPartialMap s
pvals, Seq (Posd (Stmt ext s))
inits)
      | Bool
otherwise
      = do (MapF.Pair Value s tp
vundef PartialValue s tp
pval, Seq (Posd (Stmt ext s))
is) <- NonceGenerator m s
-> Some (Value s)
-> m (Pair (Value s) (PartialValue s), Seq (Posd (Stmt ext s)))
forall (m :: Type -> Type) s ext.
Monad m =>
NonceGenerator m s
-> Some (Value s)
-> m (Pair (Value s) (PartialValue s), Seq (Posd (Stmt ext s)))
makePartialReg NonceGenerator m s
ng Some (Value s)
val
           (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
-> m (ValueToPartialMap s, Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Value s tp
-> PartialValue s tp -> ValueToPartialMap s -> ValueToPartialMap 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 Value s tp
vundef PartialValue s tp
pval ValueToPartialMap s
pvals, Seq (Posd (Stmt ext s))
inits Seq (Posd (Stmt ext s))
-> Seq (Posd (Stmt ext s)) -> Seq (Posd (Stmt ext s))
forall a. Semigroup a => a -> a -> a
<> Seq (Posd (Stmt ext s))
is)

-- | Given a value @v@ of type @t@, create a new register @r@ of type
--   @Maybe t@.  This function returns 1. the mapping from @v@ to such
--   an @r@, as well as the @stmts@ that will initialize @r@ to
--   @Nothing : Maybe t@.
makePartialReg :: Monad m
               => NonceGenerator m s
               -> Some (Value s)
               -> m (MapF.Pair (Value s) (PartialValue s), Seq (Posd (Stmt ext s)))
makePartialReg :: forall (m :: Type -> Type) s ext.
Monad m =>
NonceGenerator m s
-> Some (Value s)
-> m (Pair (Value s) (PartialValue s), Seq (Posd (Stmt ext s)))
makePartialReg NonceGenerator m s
ng (Some Value s x
val) =
  do Atom s ('MaybeType x)
a <- NonceGenerator m s
-> Position -> TypeRepr ('MaybeType x) -> m (Atom s ('MaybeType x))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng Position
p (TypeRepr x -> TypeRepr ('MaybeType x)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr TypeRepr x
ty)
     Reg s ('MaybeType x)
r <- NonceGenerator m s
-> Position -> TypeRepr ('MaybeType x) -> m (Reg s ('MaybeType x))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Reg s tp)
freshReg NonceGenerator m s
ng Position
p (TypeRepr x -> TypeRepr ('MaybeType x)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr TypeRepr x
ty)
     let v :: AtomValue ext s ('MaybeType x)
v = App ext (Atom s) ('MaybeType x) -> AtomValue ext s ('MaybeType x)
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (TypeRepr x -> App ext (Atom s) ('MaybeType x)
forall (tp1 :: CrucibleType) ext (f :: CrucibleType -> Type).
TypeRepr tp1 -> App ext f ('MaybeType tp1)
NothingValue TypeRepr x
ty)
         s :: Stmt ext s
s = Atom s ('MaybeType x)
-> AtomValue ext s ('MaybeType x) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s ('MaybeType x)
a AtomValue ext s ('MaybeType x)
v
         sr :: Stmt ext s
sr = Reg s ('MaybeType x) -> Atom s ('MaybeType x) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Reg s tp -> Atom s tp -> Stmt ext s
SetReg Reg s ('MaybeType x)
r Atom s ('MaybeType x)
a
         inits :: [Posd (Stmt ext s)]
inits = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd Position
p (Stmt ext s -> Posd (Stmt ext s))
-> [Stmt ext s] -> [Posd (Stmt ext s)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Stmt ext s
s, Stmt ext s
sr]
     (Pair (Value s) (PartialValue s), Seq (Posd (Stmt ext s)))
-> m (Pair (Value s) (PartialValue s), Seq (Posd (Stmt ext s)))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Value s x -> PartialValue s x -> Pair (Value s) (PartialValue s)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
MapF.Pair Value s x
val (Reg s ('MaybeType x) -> PartialValue s x
forall s (tp :: CrucibleType).
Reg s (MaybeType tp) -> PartialValue s tp
PartialValue Reg s ('MaybeType x)
r), [Posd (Stmt ext s)] -> Seq (Posd (Stmt ext s))
forall a. [a] -> Seq a
Seq.fromList [Posd (Stmt ext s)]
inits)
  where
    (TypeRepr x
ty, Position
p) = case Value s x
val of
                RegValue Reg s x
reg   -> (Reg s x -> TypeRepr x
forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg Reg s x
reg, Reg s x -> Position
forall s (tp :: CrucibleType). Reg s tp -> Position
regPosition Reg s x
reg)
                AtomValue Atom s x
atom -> (Atom s x -> TypeRepr x
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s x
atom, Atom s x -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s x
atom)

-------------------
-- | Merging Paths
-------------------

-- | This is a record used to construct/manage the variant type that the router block
-- will use to switch on. The important piece is the map that relates blockIDs to an index
-- into the variant type's ctx -- with this map we can associate a _value_ of the variant type
-- with a given blockID
data BlockSwitchInfo s ctx = BlockSwitchInfo
                             { forall s (ctx :: Ctx CrucibleType).
BlockSwitchInfo s ctx -> CtxRepr ctx
switchRepr :: CtxRepr ctx
                             , forall s (ctx :: Ctx CrucibleType).
BlockSwitchInfo s ctx -> Size ctx
switchSize :: Ctx.Size ctx
                             , forall s (ctx :: Ctx CrucibleType).
BlockSwitchInfo s ctx -> Map (BlockID s) (Index ctx UnitType)
switchMap  :: Map.Map (BlockID s) (Ctx.Index ctx UnitType)
                             }
                           deriving Node -> BlockSwitchInfo s ctx -> ShowS
[BlockSwitchInfo s ctx] -> ShowS
BlockSwitchInfo s ctx -> String
(Node -> BlockSwitchInfo s ctx -> ShowS)
-> (BlockSwitchInfo s ctx -> String)
-> ([BlockSwitchInfo s ctx] -> ShowS)
-> Show (BlockSwitchInfo s ctx)
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s (ctx :: Ctx CrucibleType).
Node -> BlockSwitchInfo s ctx -> ShowS
forall s (ctx :: Ctx CrucibleType).
[BlockSwitchInfo s ctx] -> ShowS
forall s (ctx :: Ctx CrucibleType). BlockSwitchInfo s ctx -> String
$cshowsPrec :: forall s (ctx :: Ctx CrucibleType).
Node -> BlockSwitchInfo s ctx -> ShowS
showsPrec :: Node -> BlockSwitchInfo s ctx -> ShowS
$cshow :: forall s (ctx :: Ctx CrucibleType). BlockSwitchInfo s ctx -> String
show :: BlockSwitchInfo s ctx -> String
$cshowList :: forall s (ctx :: Ctx CrucibleType).
[BlockSwitchInfo s ctx] -> ShowS
showList :: [BlockSwitchInfo s ctx] -> ShowS
Show

-- | Used as a substitution between labels.
-- Closes over the type of LambdaLabels
data BlockIDPair s where
   Labels       :: Label s -> Label s -> BlockIDPair s
   LambdaLabels :: LambdaLabel s tp -> LambdaLabel s tp -> BlockIDPair s

instance Show (BlockIDPair s) where
  show :: BlockIDPair s -> String
show (Labels Label s
l1 Label s
l2)       = Label s -> String
forall a. Show a => a -> String
show Label s
l1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" => " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Label s -> String
forall a. Show a => a -> String
show Label s
l2
  show (LambdaLabels LambdaLabel s tp
l1 LambdaLabel s tp
l2) = LambdaLabel s tp -> String
forall a. Show a => a -> String
show LambdaLabel s tp
l1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" =>{lambda} " String -> ShowS
forall a. [a] -> [a] -> [a]
++ LambdaLabel s tp -> String
forall a. Show a => a -> String
show LambdaLabel s tp
l2

-- | This is the main pass that attempts to optimize early exits in
-- the loops in a CFG.  In particular, this transformation ensures that the
-- postdominator of the loop header is a member of the loop.
--
-- Given a natural loop, its members are a set of blocks @bs@. Let the exit edges be 
-- the edges from some block @b@ in @bs@ to either the loop header or a block not in @bs@.
--
-- Let (i, j) be such an exit edge.This transofrmation inserts a new
-- block @r@ such that in the transformed cfg there is an edge (i, r)
-- and an edge (r, j). Moreover, the transformation ensures that [i,
-- r, j'] is not feasible for j' != j. This works by setting a
-- "destination" register @d := j@ in each block i for each exit edge
-- (i, j), and switching on the value of @d@ in the block @r@.
earlyMergeLoops :: ( TraverseExt ext, Monad m, Show (CFG ext s init ret) )
                => NonceGenerator m s
                -> CFG ext s init ret
                -> m (CFG ext s init ret)
earlyMergeLoops :: forall ext (m :: Type -> Type) s (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(TraverseExt ext, Monad m, Show (CFG ext s init ret)) =>
NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret)
earlyMergeLoops NonceGenerator m s
ng CFG ext s init ret
cfg0 =
  do CFG ext s init ret
cfg' <- NonceGenerator m s
-> Set (BlockID s)
-> [LoopInfo s]
-> CFG ext s init ret
-> m (CFG ext s init ret)
forall ext (m :: Type -> Type) s (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(TraverseExt ext, Monad m, Show (CFG ext s init ret)) =>
NonceGenerator m s
-> Set (BlockID s)
-> [LoopInfo s]
-> CFG ext s init ret
-> m (CFG ext s init ret)
earlyMergeLoops' NonceGenerator m s
ng Set (BlockID s)
forall a. Monoid a => a
mempty (CFG ext s init ret -> [LoopInfo s]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [LoopInfo s]
cfgLoops CFG ext s init ret
cfg0) CFG ext s init ret
cfg0
     NonceGenerator m s
-> Label s -> CFG ext s init ret -> m (CFG ext s init ret)
forall (m :: Type -> Type) ext s (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(Monad m, TraverseExt ext) =>
NonceGenerator m s
-> Label s -> CFG ext s init ret -> m (CFG ext s init ret)
lowerUndefPass NonceGenerator m s
ng (CFG ext s init ret -> Label s
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Label s
cfgEntryLabel CFG ext s init ret
cfg') CFG ext s init ret
cfg'
      
-- Merge a loop from loops in cfg.  The loops parameter is passed
-- to earlyMergeLoops (rather than calculated directly from cfg)
-- so that we can use see how the set of loops changes from
-- iteration to iteration: in particular, we want to make sure
-- that the number of loops does not increases
earlyMergeLoops' :: ( TraverseExt ext, Monad m, Show (CFG ext s init ret) )
                 => NonceGenerator m s
                 -> Set (BlockID s)
                 -> [LoopInfo s]
                 -> CFG ext s init ret
                 -> m (CFG ext s init ret)
earlyMergeLoops' :: forall ext (m :: Type -> Type) s (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(TraverseExt ext, Monad m, Show (CFG ext s init ret)) =>
NonceGenerator m s
-> Set (BlockID s)
-> [LoopInfo s]
-> CFG ext s init ret
-> m (CFG ext s init ret)
earlyMergeLoops' NonceGenerator m s
ng Set (BlockID s)
seen [LoopInfo s]
ls CFG ext s init ret
cfg
  | Just LoopInfo s
l <- Maybe (LoopInfo s)
nextLoop
  = do CFG ext s init ret
cfg' <- NonceGenerator m s
-> CFG ext s init ret -> LoopInfo s -> m (CFG ext s init ret)
forall ext (m :: Type -> Type) s (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(TraverseExt ext, Monad m) =>
NonceGenerator m s
-> CFG ext s init ret -> LoopInfo s -> m (CFG ext s init ret)
earlyMergeLoop NonceGenerator m s
ng CFG ext s init ret
cfg LoopInfo s
l

       -- Check if we should proceed: in particular, if the new CFG
       -- renamed or produced new loops, then we need to bail as we
       -- might not terminate in that case.
       let ls' :: [LoopInfo s]
ls'      = CFG ext s init ret -> [LoopInfo s]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [LoopInfo s]
cfgLoops CFG ext s init ret
cfg'
       let seen' :: Set (BlockID s)
seen'    = (BlockID s -> Set (BlockID s) -> Set (BlockID s)
forall a. Ord a => a -> Set a -> Set a
Set.insert (LoopInfo s -> BlockID s
forall s. LoopInfo s -> BlockID s
liHeader LoopInfo s
l) Set (BlockID s)
seen)
       let nextStep :: [LoopInfo s]
nextStep = Set (BlockID s) -> [LoopInfo s] -> [LoopInfo s]
forall {s}. Set (BlockID s) -> [LoopInfo s] -> [LoopInfo s]
candidates Set (BlockID s)
seen' [LoopInfo s]
ls'
       -- The termination transition invariant is that 
       Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when ([LoopInfo s] -> Node
forall a. [a] -> Node
forall (t :: Type -> Type) a. Foldable t => t a -> Node
length [LoopInfo s]
thisStep Node -> Node -> Bool
forall a. Ord a => a -> a -> Bool
<= [LoopInfo s] -> Node
forall a. [a] -> Node
forall (t :: Type -> Type) a. Foldable t => t a -> Node
length [LoopInfo s]
nextStep) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
         String -> [String] -> m ()
forall a. HasCallStack => String -> [String] -> a
panic String
"EarlyMergeLoops.earlyMergeLoops'"
               [String
"Non-decreasing number of loops in earlyMegeLoops'"]
       
       NonceGenerator m s
-> Set (BlockID s)
-> [LoopInfo s]
-> CFG ext s init ret
-> m (CFG ext s init ret)
forall ext (m :: Type -> Type) s (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(TraverseExt ext, Monad m, Show (CFG ext s init ret)) =>
NonceGenerator m s
-> Set (BlockID s)
-> [LoopInfo s]
-> CFG ext s init ret
-> m (CFG ext s init ret)
earlyMergeLoops' NonceGenerator m s
ng Set (BlockID s)
seen' [LoopInfo s]
ls' CFG ext s init ret
cfg'
  | Bool
otherwise
  = CFG ext s init ret -> m (CFG ext s init ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return CFG ext s init ret
cfg
  where
    thisStep :: [LoopInfo s]
thisStep =
      Set (BlockID s) -> [LoopInfo s] -> [LoopInfo s]
forall {s}. Set (BlockID s) -> [LoopInfo s] -> [LoopInfo s]
candidates Set (BlockID s)
seen [LoopInfo s]
ls

    nextLoop :: Maybe (LoopInfo s)
nextLoop 
      | [LoopInfo s] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [LoopInfo s]
thisStep  = Maybe (LoopInfo s)
forall a. Maybe a
Nothing
      | Bool
otherwise = LoopInfo s -> Maybe (LoopInfo s)
forall a. a -> Maybe a
Just ((LoopInfo s -> LoopInfo s -> Ordering)
-> [LoopInfo s] -> LoopInfo s
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy LoopInfo s -> LoopInfo s -> Ordering
forall s. LoopInfo s -> LoopInfo s -> Ordering
isNested [LoopInfo s]
thisStep)

    candidates :: Set (BlockID s) -> [LoopInfo s] -> [LoopInfo s]
candidates Set (BlockID s)
seenBlocks [LoopInfo s]
lis =
      (LoopInfo s -> Bool) -> [LoopInfo s] -> [LoopInfo s]
forall a. (a -> Bool) -> [a] -> [a]
filter (Set (BlockID s) -> LoopInfo s -> Bool
forall {s}. Set (BlockID s) -> LoopInfo s -> Bool
unseen Set (BlockID s)
seenBlocks) [LoopInfo s]
lis


    unseen :: Set (BlockID s) -> LoopInfo s -> Bool
unseen Set (BlockID s)
s LoopInfo s
li = LoopInfo s -> BlockID s
forall s. LoopInfo s -> BlockID s
liHeader LoopInfo s
li BlockID s -> Set (BlockID s) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set (BlockID s)
s

-- | Apply the transformation described in @earlyMergeLoops@ to a single loop.
earlyMergeLoop :: ( TraverseExt ext, Monad m )
               => NonceGenerator m s
               -> CFG ext s init ret
               -> LoopInfo s
               -> m (CFG ext s init ret)
earlyMergeLoop :: forall ext (m :: Type -> Type) s (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(TraverseExt ext, Monad m) =>
NonceGenerator m s
-> CFG ext s init ret -> LoopInfo s -> m (CFG ext s init ret)
earlyMergeLoop NonceGenerator m s
ng CFG ext s init ret
cfg LoopInfo s
li
  | Bool -> Bool
not ([CFGEdge s] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [CFGEdge s]
exits) =
      do Map (BlockID s) (Block ext s ret)
bmap' <- NonceGenerator m s
-> Map (BlockID s) (Block ext s ret)
-> [CFGEdge s]
-> m (Map (BlockID s) (Block ext s ret))
forall ext (m :: Type -> Type) s (ret :: CrucibleType).
(TraverseExt ext, Monad m) =>
NonceGenerator m s
-> Map (BlockID s) (Block ext s ret)
-> [(BlockID s, BlockID s)]
-> m (Map (BlockID s) (Block ext s ret))
funnelPaths NonceGenerator m s
ng Map (BlockID s) (Block ext s ret)
bmap [CFGEdge s]
exits
         CFG ext s init ret -> m (CFG ext s init ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return CFG ext s init ret
cfg { cfgBlocks = Map.elems bmap' }
  | Bool
otherwise =
      CFG ext s init ret -> m (CFG ext s init ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return CFG ext s init ret
cfg
  where
    exits :: [CFGEdge s]
exits         = [CFGEdge s] -> [CFGEdge s]
filterErrors (LoopInfo s -> [CFGEdge s]
forall s. LoopInfo s -> [CFGEdge s]
liEarlyExits LoopInfo s
li [CFGEdge s] -> [CFGEdge s] -> [CFGEdge s]
forall a. [a] -> [a] -> [a]
++ LoopInfo s -> [CFGEdge s]
forall s. LoopInfo s -> [CFGEdge s]
liFooterIn LoopInfo s
li)
    filterErrors :: [CFGEdge s] -> [CFGEdge s]
filterErrors  = (CFGEdge s -> Bool) -> [CFGEdge s] -> [CFGEdge s]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (CFGEdge s -> Bool) -> CFGEdge s -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (BlockID s) (Block ext s ret) -> CFGEdge s -> Bool
forall s ext (ret :: CrucibleType).
Map (BlockID s) (Block ext s ret) -> CFGEdge s -> Bool
errorPath Map (BlockID s) (Block ext s ret)
bmap)
    bmap :: Map (BlockID s) (Block ext s ret)
bmap          = CFG ext s init ret -> Map (BlockID s) (Block ext s ret)
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Map (BlockID s) (Block ext s ret)
blockMap CFG ext s init ret
cfg

-- | Given a set of edges (i, j) in E,
-- Create a single block that merges all paths before
-- continuing on to the respective j's
--
-- Create a unique block F and multiple blocks  i' j' such
-- that i -> i' -> F -> j' -> j.
-- This function defines a register 'r : () + () + ... + ()'
-- Each 'j' corresponds to one of these tags, so each
-- i' sets r to indicate which 'j' to jump to, and F
-- switches on r. Each j' is a lambda block that jumps to the
-- original j.
--
-- E.g. given i0 -> j0, i1 -> j0, i2 -> j1,
-- then i0' =  r := inj(0, ()); jump F
--      i1' =  r := inj(0, ()); jump F
--      i2' =  r := inj(1, ()); jump F
--      F   =  switch r { 0: j0', 1: j1' }
--      j0' = jump j0
--      j1' = jump j1
funnelPaths :: (TraverseExt ext, Monad m)
             => NonceGenerator m s
             -> Map.Map (BlockID s) (Block ext s ret)
             -> [(BlockID s, BlockID s)]
             -> m (Map.Map (BlockID s) (Block ext s ret))
funnelPaths :: forall ext (m :: Type -> Type) s (ret :: CrucibleType).
(TraverseExt ext, Monad m) =>
NonceGenerator m s
-> Map (BlockID s) (Block ext s ret)
-> [(BlockID s, BlockID s)]
-> m (Map (BlockID s) (Block ext s ret))
funnelPaths NonceGenerator m s
ng Map (BlockID s) (Block ext s ret)
bmap [(BlockID s, BlockID s)]
paths =
  case [BlockID s] -> Some (BlockSwitchInfo s)
forall s. [BlockID s] -> Some (BlockSwitchInfo s)
mkBlockSwitchInfo [BlockID s]
outBlocks of
    Some BlockSwitchInfo s x
p ->
      do ([BlockIDPair s]
rename, [Block ext s ret]
newBlocks) <- NonceGenerator m s
-> BlockSwitchInfo s x
-> [BlockID s]
-> m ([BlockIDPair s], [Block ext s ret])
forall (m :: Type -> Type) ext (ctx :: Ctx CrucibleType) s
       (ret :: CrucibleType).
(TraverseExt ext, Monad m) =>
NonceGenerator m s
-> BlockSwitchInfo s ctx
-> [BlockID s]
-> m ([BlockIDPair s], [Block ext s ret])
routePaths NonceGenerator m s
ng BlockSwitchInfo s x
p [BlockID s]
outBlocks
         let renamedMap :: Map (BlockID s) (Block ext s ret)
renamedMap       = (Map (BlockID s) (Block ext s ret)
 -> BlockID s -> Map (BlockID s) (Block ext s ret))
-> Map (BlockID s) (Block ext s ret)
-> [BlockID s]
-> Map (BlockID s) (Block ext s ret)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' ([BlockIDPair s]
-> Map (BlockID s) (Block ext s ret)
-> BlockID s
-> Map (BlockID s) (Block ext s ret)
forall {k} {ext} {t :: Type -> Type} {s} {ret :: CrucibleType}.
(Ord k, TraversableFC (ExprExtension ext),
 TraversableFC (StmtExtension ext), Foldable t) =>
t (BlockIDPair s)
-> Map k (Block ext s ret) -> k -> Map k (Block ext s ret)
updateBlock [BlockIDPair s]
rename) Map (BlockID s) (Block ext s ret)
bmap ((BlockID s, BlockID s) -> BlockID s
forall a b. (a, b) -> a
fst ((BlockID s, BlockID s) -> BlockID s)
-> [(BlockID s, BlockID s)] -> [BlockID s]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(BlockID s, BlockID s)]
paths)
             newMap :: Map (BlockID s) (Block ext s ret)
newMap           = (Map (BlockID s) (Block ext s ret)
 -> Block ext s ret -> Map (BlockID s) (Block ext s ret))
-> Map (BlockID s) (Block ext s ret)
-> [Block ext s ret]
-> Map (BlockID s) (Block ext s ret)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' Map (BlockID s) (Block ext s ret)
-> Block ext s ret -> Map (BlockID s) (Block ext s ret)
forall {s} {ext} {ret :: CrucibleType}.
Map (BlockID s) (Block ext s ret)
-> Block ext s ret -> Map (BlockID s) (Block ext s ret)
addNewBlock Map (BlockID s) (Block ext s ret)
renamedMap [Block ext s ret]
newBlocks

         Map (BlockID s) (Block ext s ret)
-> m (Map (BlockID s) (Block ext s ret))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Map (BlockID s) (Block ext s ret)
newMap
  where
    outBlocks :: [BlockID s]
outBlocks = [BlockID s] -> [BlockID s]
forall a. Eq a => [a] -> [a]
nub ((BlockID s, BlockID s) -> BlockID s
forall a b. (a, b) -> b
snd ((BlockID s, BlockID s) -> BlockID s)
-> [(BlockID s, BlockID s)] -> [BlockID s]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(BlockID s, BlockID s)]
paths)

    sub :: t (BlockIDPair s) -> TermStmt s ret -> TermStmt s ret
sub t (BlockIDPair s)
renaming TermStmt s ret
stmt = (TermStmt s ret -> BlockIDPair s -> TermStmt s ret)
-> TermStmt s ret -> t (BlockIDPair s) -> TermStmt s ret
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' TermStmt s ret -> BlockIDPair s -> TermStmt s ret
forall {s} {ret :: CrucibleType}.
TermStmt s ret -> BlockIDPair s -> TermStmt s ret
runRename TermStmt s ret
stmt t (BlockIDPair s)
renaming
    addNewBlock :: Map (BlockID s) (Block ext s ret)
-> Block ext s ret -> Map (BlockID s) (Block ext s ret)
addNewBlock Map (BlockID s) (Block ext s ret)
m Block ext s ret
b        = BlockID s
-> Block ext s ret
-> Map (BlockID s) (Block ext s ret)
-> Map (BlockID s) (Block ext s ret)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b) Block ext s ret
b Map (BlockID s) (Block ext s ret)
m
    updateBlock :: t (BlockIDPair s)
-> Map k (Block ext s ret) -> k -> Map k (Block ext s ret)
updateBlock t (BlockIDPair s)
ren Map k (Block ext s ret)
m k
bid  = (Block ext s ret -> Maybe (Block ext s ret))
-> k -> Map k (Block ext s ret) -> Map k (Block ext s ret)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (t (BlockIDPair s) -> Block ext s ret -> Maybe (Block ext s ret)
forall {ext} {t :: Type -> Type} {s} {ret :: CrucibleType}.
(TraversableFC (ExprExtension ext),
 TraversableFC (StmtExtension ext), Foldable t) =>
t (BlockIDPair s) -> Block ext s ret -> Maybe (Block ext s ret)
doUpdate t (BlockIDPair s)
ren) k
bid Map k (Block ext s ret)
m
    doUpdate :: t (BlockIDPair s) -> Block ext s ret -> Maybe (Block ext s ret)
doUpdate t (BlockIDPair s)
renaming Block ext s ret
blk  = Block ext s ret -> Maybe (Block ext s ret)
forall a. a -> Maybe a
Just (Block ext s ret -> Maybe (Block ext s ret))
-> Block ext s ret -> Maybe (Block ext s ret)
forall a b. (a -> b) -> a -> b
$ 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 (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
blk) (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockExtraInputs Block ext s ret
blk)
                                      (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
blk) (t (BlockIDPair s) -> TermStmt s ret -> TermStmt s ret
forall {t :: Type -> Type} {s} {ret :: CrucibleType}.
Foldable t =>
t (BlockIDPair s) -> TermStmt s ret -> TermStmt s ret
sub t (BlockIDPair s)
renaming (TermStmt s ret -> TermStmt s ret)
-> Posd (TermStmt s ret) -> Posd (TermStmt s ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
blk)

    -- Apply the label substitution in 'renaming'
    -- to the term stmt in tgt (no-op on stmts without labels)
    runRename :: TermStmt s ret -> BlockIDPair s -> TermStmt s ret
runRename TermStmt s ret
tgt BlockIDPair s
renaming =
      case (TermStmt s ret
tgt, BlockIDPair s
renaming) of
        (Jump Label s
t, Labels Label s
from Label s
to)
          | Label s
t Label s -> Label s -> Bool
forall a. Eq a => a -> a -> Bool
== Label s
from -> Label s -> TermStmt s ret
forall s (ret :: CrucibleType). Label s -> TermStmt s ret
Jump Label s
to
          | Bool
otherwise -> TermStmt s ret
tgt
        (Jump Label s
_, LambdaLabels {}) -> TermStmt s ret
tgt

        (Br Atom s BoolType
p Label s
t1 Label s
t2, Labels Label s
from Label s
to)
          | Label s
t1 Label s -> Label s -> Bool
forall a. Eq a => a -> a -> Bool
== Label s
from -> 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
p Label s
to Label s
t2
          | Label s
t2 Label s -> Label s -> Bool
forall a. Eq a => a -> a -> Bool
== Label s
from -> 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
p Label s
t1 Label s
to
          | Bool
otherwise  -> TermStmt s ret
tgt
        (Br {}, LambdaLabels {}) -> TermStmt s ret
tgt

        (Output LambdaLabel s tp
ll Atom s tp
a, LambdaLabels LambdaLabel s tp
from LambdaLabel s tp
to)
          | Just tp :~: tp
Refl <- LambdaLabel s tp -> LambdaLabel s tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b)
testEquality LambdaLabel s tp
ll LambdaLabel s tp
from -> LambdaLabel s tp -> Atom s tp -> TermStmt s ret
forall s (tp :: CrucibleType) (ret :: CrucibleType).
LambdaLabel s tp -> Atom s tp -> TermStmt s ret
Output LambdaLabel s tp
to Atom s tp
Atom s tp
a
          | Bool
otherwise -> TermStmt s ret
tgt
        (Output {}, Labels {}) -> TermStmt s ret
tgt

        (VariantElim CtxRepr varctx
ctx Atom s (VariantType varctx)
a Assignment (LambdaLabel s) varctx
assgn, r :: BlockIDPair s
r@(LambdaLabels {})) ->
          CtxRepr varctx
-> Atom s (VariantType varctx)
-> Assignment (LambdaLabel s) varctx
-> TermStmt s ret
forall (varctx :: Ctx CrucibleType) s (ret :: CrucibleType).
CtxRepr varctx
-> Atom s (VariantType varctx)
-> Assignment (LambdaLabel s) varctx
-> TermStmt s ret
VariantElim CtxRepr varctx
ctx Atom s (VariantType varctx)
a ((forall (x :: CrucibleType). LambdaLabel s x -> LambdaLabel s x)
-> forall (x :: Ctx CrucibleType).
   Assignment (LambdaLabel s) x -> Assignment (LambdaLabel s) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (BlockIDPair s -> LambdaLabel s x -> LambdaLabel s x
forall {s} {b :: CrucibleType}.
BlockIDPair s -> LambdaLabel s b -> LambdaLabel s b
renameLabel BlockIDPair s
r) Assignment (LambdaLabel s) varctx
assgn)
        (VariantElim {}, Labels {}) -> TermStmt s ret
tgt

        (MaybeBranch TypeRepr tp
t Atom s (MaybeType tp)
a LambdaLabel s tp
l1 Label s
l2, Labels Label s
from Label s
to)
          | Label s
l2 Label s -> Label s -> Bool
forall a. Eq a => a -> a -> Bool
== Label s
from -> TypeRepr tp
-> Atom s (MaybeType tp)
-> LambdaLabel s tp
-> Label s
-> TermStmt s ret
forall (tp :: CrucibleType) s (ret :: CrucibleType).
TypeRepr tp
-> Atom s (MaybeType tp)
-> LambdaLabel s tp
-> Label s
-> TermStmt s ret
MaybeBranch TypeRepr tp
t Atom s (MaybeType tp)
a LambdaLabel s tp
l1 Label s
to
          | Bool
otherwise  -> TermStmt s ret
tgt
        (MaybeBranch TypeRepr tp
t Atom s (MaybeType tp)
a LambdaLabel s tp
l1 Label s
l2, LambdaLabels LambdaLabel s tp
from LambdaLabel s tp
to)
          | Just tp :~: tp
Refl <- LambdaLabel s tp -> LambdaLabel s tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b)
testEquality LambdaLabel s tp
l1 LambdaLabel s tp
from ->
            TypeRepr tp
-> Atom s (MaybeType tp)
-> LambdaLabel s tp
-> Label s
-> TermStmt s ret
forall (tp :: CrucibleType) s (ret :: CrucibleType).
TypeRepr tp
-> Atom s (MaybeType tp)
-> LambdaLabel s tp
-> Label s
-> TermStmt s ret
MaybeBranch TypeRepr tp
t Atom s (MaybeType tp)
a LambdaLabel s tp
LambdaLabel s tp
to Label s
l2
          | Bool
otherwise  -> TermStmt s ret
tgt

        {- No labels to rename -}
        (Return Atom s ret
_, BlockIDPair s
_)     -> TermStmt s ret
tgt
        (TailCall {}, BlockIDPair s
_)  -> TermStmt s ret
tgt
        (ErrorStmt {}, BlockIDPair s
_) -> TermStmt s ret
tgt

    renameLabel :: BlockIDPair s -> LambdaLabel s b -> LambdaLabel s b
renameLabel (LambdaLabels LambdaLabel s tp
from LambdaLabel s tp
to) LambdaLabel s b
ll
      | Just tp :~: b
Refl <- LambdaLabel s tp -> LambdaLabel s b -> Maybe (tp :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b)
testEquality LambdaLabel s tp
from LambdaLabel s b
ll = LambdaLabel s tp
LambdaLabel s b
to
    renameLabel BlockIDPair s
_ LambdaLabel s b
l = LambdaLabel s b
l


-- | Given a list of blocks, build a record of a variant type such that each injection
-- is associated with a single block.
mkBlockSwitchInfo :: [BlockID s] -> Some (BlockSwitchInfo s)
mkBlockSwitchInfo :: forall s. [BlockID s] -> Some (BlockSwitchInfo s)
mkBlockSwitchInfo [BlockID s]
bs =
  case [BlockID s]
bs of
    []      ->
      BlockSwitchInfo s EmptyCtx -> Some (BlockSwitchInfo s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (CtxRepr EmptyCtx
-> Size EmptyCtx
-> Map (BlockID s) (Index EmptyCtx UnitType)
-> BlockSwitchInfo s EmptyCtx
forall s (ctx :: Ctx CrucibleType).
CtxRepr ctx
-> Size ctx
-> Map (BlockID s) (Index ctx UnitType)
-> BlockSwitchInfo s ctx
BlockSwitchInfo CtxRepr EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty Size EmptyCtx
forall {k}. Size 'EmptyCtx
Ctx.zeroSize Map (BlockID s) (Index EmptyCtx UnitType)
forall a. Monoid a => a
mempty)
    (BlockID s
b:[BlockID s]
bs') ->
      case [BlockID s] -> Some (BlockSwitchInfo s)
forall s. [BlockID s] -> Some (BlockSwitchInfo s)
mkBlockSwitchInfo [BlockID s]
bs' of
        Some (BlockSwitchInfo CtxRepr x
ctxRepr Size x
sz Map (BlockID s) (Index x UnitType)
indices) ->
          BlockSwitchInfo s (x '::> UnitType) -> Some (BlockSwitchInfo s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (BlockSwitchInfo s (x '::> UnitType) -> Some (BlockSwitchInfo s))
-> BlockSwitchInfo s (x '::> UnitType) -> Some (BlockSwitchInfo s)
forall a b. (a -> b) -> a -> b
$ BlockSwitchInfo { switchRepr :: CtxRepr (x '::> UnitType)
switchRepr = CtxRepr x
ctxRepr CtxRepr x -> TypeRepr UnitType -> CtxRepr (x '::> UnitType)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> TypeRepr UnitType
UnitRepr
                                 , switchSize :: Size (x '::> UnitType)
switchSize = Size x -> Size (x '::> UnitType)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
Ctx.incSize Size x
sz
                                 , switchMap :: Map (BlockID s) (Index (x '::> UnitType) UnitType)
switchMap  = BlockID s
-> Index (x '::> UnitType) UnitType
-> Map (BlockID s) (Index (x '::> UnitType) UnitType)
-> Map (BlockID s) (Index (x '::> UnitType) UnitType)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert BlockID s
b (Size x -> Index (x '::> UnitType) UnitType
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
Ctx.nextIndex Size x
sz) ((Index x UnitType -> Index (x '::> UnitType) UnitType)
-> Map (BlockID s) (Index x UnitType)
-> Map (BlockID s) (Index (x '::> UnitType) UnitType)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Index x UnitType -> Index (x '::> UnitType) UnitType
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
Ctx.skipIndex Map (BlockID s) (Index x UnitType)
indices)
                                 }

-- | This function does most of the work for @funnelPaths@.
-- In particular, given a list of blocks @b0...bn@,
-- it constructs a single @r@, a list @b_in0...b_inn@, and a list
-- @b_out0...@b_outn@ such that @b_in_i@ jump to @r@, and @r@
-- jumps to the corresponding @b_out_i@.
--
-- The return value is a pair of
-- (1) A list of BlockIDPairs, which should be understood as a substitution
-- on labels. This is necessary since we are introducing *new* blocks to replace
-- *old* jump targets. This substitution is used to update the old jump targets
-- (2) A list of newly created blocks
routePaths :: forall m ext ctx s ret
            . (TraverseExt ext, Monad m)
           => NonceGenerator m s
           -> BlockSwitchInfo s ctx
           -- ^ the variant info should map each element of @outs@ to an index into `ctx`
           -> [BlockID s]
           -- ^ the blocks that we want to join & then fan out from
           -> m ([BlockIDPair s], [Block ext s ret])
routePaths :: forall (m :: Type -> Type) ext (ctx :: Ctx CrucibleType) s
       (ret :: CrucibleType).
(TraverseExt ext, Monad m) =>
NonceGenerator m s
-> BlockSwitchInfo s ctx
-> [BlockID s]
-> m ([BlockIDPair s], [Block ext s ret])
routePaths NonceGenerator m s
ng (BlockSwitchInfo CtxRepr ctx
ctx Size ctx
sz Map (BlockID s) (Index ctx UnitType)
idxMap) [BlockID s]
outs =
  do -- 'bsi' has the information we need to associate each input block
     -- with an a particular *index* into a list of outputs. This means
     -- for each destination that we're routing to,
     -- we can set a register `r` to some value `v`
     -- and case split on `r` in a 'router block' to recover the intended destination

     -- this associates each such index with the new 'destination'
     Assignment (LambdaLabel s) ctx
mapping <- m (Assignment (LambdaLabel s) ctx)
mkMapping

     -- This is the block that switches on the destination block.
     -- l is its label, r is the register that we'll case split on,
     -- and 'router' is the actual block definition containing the switch
     (Label s
l, Reg s (VariantType ctx)
r, Block ext s ret
router) <- NonceGenerator m s
-> CtxRepr ctx
-> Assignment (LambdaLabel s) ctx
-> m (Label s, Reg s (VariantType ctx), Block ext s ret)
forall ext (m :: Type -> Type) s (routing :: Ctx CrucibleType)
       (ret :: CrucibleType).
(TraverseExt ext, Monad m) =>
NonceGenerator m s
-> CtxRepr routing
-> Assignment (LambdaLabel s) routing
-> m (Label s, Reg s (VariantType routing), Block ext s ret)
routerBlock NonceGenerator m s
ng CtxRepr ctx
ctx Assignment (LambdaLabel s) ctx
mapping
    
     -- construct the blocks feeding into the router. for each output block,
     -- set 'r' appropriately, by fetching the value from the index map in 'vi'
     ([BlockIDPair s]
rename, [Block ext s ret]
injBlocks) <- [(BlockIDPair s, Block ext s ret)]
-> ([BlockIDPair s], [Block ext s ret])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(BlockIDPair s, Block ext s ret)]
 -> ([BlockIDPair s], [Block ext s ret]))
-> m [(BlockIDPair s, Block ext s ret)]
-> m ([BlockIDPair s], [Block ext s ret])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BlockID s -> m (BlockIDPair s, Block ext s ret))
-> [BlockID s] -> m [(BlockIDPair s, Block ext s ret)]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Reg s (VariantType ctx)
-> Label s -> BlockID s -> m (BlockIDPair s, Block ext s ret)
mkInjBlock Reg s (VariantType ctx)
r Label s
l) [BlockID s]
outs

     -- Finally make the destination blocks that continue to the original
     -- targets
     let outputBlocks :: [Block ext s ret]
outputBlocks = (BlockID s
 -> Index ctx UnitType -> [Block ext s ret] -> [Block ext s ret])
-> [Block ext s ret]
-> Map (BlockID s) (Index ctx UnitType)
-> [Block ext s ret]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ([BlockIDPair s]
-> Assignment (LambdaLabel s) ctx
-> BlockID s
-> Index ctx UnitType
-> [Block ext s ret]
-> [Block ext s ret]
mkLambdaBlock [BlockIDPair s]
rename Assignment (LambdaLabel s) ctx
mapping) [] Map (BlockID s) (Index ctx UnitType)
idxMap

     ([BlockIDPair s], [Block ext s ret])
-> m ([BlockIDPair s], [Block ext s ret])
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([BlockIDPair s]
rename, Block ext s ret
router Block ext s ret -> [Block ext s ret] -> [Block ext s ret]
forall a. a -> [a] -> [a]
: [Block ext s ret]
outputBlocks [Block ext s ret] -> [Block ext s ret] -> [Block ext s ret]
forall a. [a] -> [a] -> [a]
++ [Block ext s ret]
injBlocks)
  where
    bidToTerm :: BlockID s -> [BlockIDPair s] -> TermStmt s ret
    bidToTerm :: BlockID s -> [BlockIDPair s] -> TermStmt s ret
bidToTerm BlockID s
origOut [BlockIDPair s]
rename =
      case (BlockID s
origOut, [BlockIDPair s]
rename) of
        (LabelID Label s
ll, [BlockIDPair s]
_ ) -> Label s -> TermStmt s ret
forall s (ret :: CrucibleType). Label s -> TermStmt s ret
Jump Label s
ll
        (LambdaID LambdaLabel s tp
ll, LambdaLabels LambdaLabel s tp
l1 LambdaLabel s tp
l2:[BlockIDPair s]
_)
          | Just tp :~: tp
Refl <- Nonce s tp -> Nonce s tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Nonce s a -> Nonce s b -> Maybe (a :~: b)
testEquality (LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s tp
ll) (LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s tp
l1) -> LambdaLabel s tp -> Atom s tp -> TermStmt s ret
forall s (tp :: CrucibleType) (ret :: CrucibleType).
LambdaLabel s tp -> Atom s tp -> TermStmt s ret
Output LambdaLabel s tp
l1 (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
l2)
        (BlockID s
_, BlockIDPair s
_:[BlockIDPair s]
rest) -> BlockID s -> [BlockIDPair s] -> TermStmt s ret
bidToTerm BlockID s
origOut [BlockIDPair s]
rest
        (BlockID s, [BlockIDPair s])
_ ->
          String -> TermStmt s ret
forall a. HasCallStack => String -> a
error String
"Output blocks mismatched in routePaths"
  
    mkMapping :: m (Assignment (LambdaLabel s) ctx)
mkMapping = Size ctx
-> (forall (tp :: CrucibleType).
    Index ctx tp -> m (LambdaLabel s tp))
-> m (Assignment (LambdaLabel s) ctx)
forall {k} (m :: Type -> Type) (ctx :: Ctx k) (f :: k -> Type).
Applicative m =>
Size ctx
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
Ctx.generateM Size ctx
sz ((forall (tp :: CrucibleType).
  Index ctx tp -> m (LambdaLabel s tp))
 -> m (Assignment (LambdaLabel s) ctx))
-> (forall (tp :: CrucibleType).
    Index ctx tp -> m (LambdaLabel s tp))
-> m (Assignment (LambdaLabel s) ctx)
forall a b. (a -> b) -> a -> b
$ \Index ctx tp
idx ->
      do Nonce s tp
n <- NonceGenerator m s -> m (Nonce s tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng
         Atom s tp
a <- NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng Position
internal (CtxRepr ctx
ctx CtxRepr ctx -> Index ctx tp -> TypeRepr tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
idx)
         LambdaLabel s tp -> m (LambdaLabel s tp)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Nonce s tp -> Atom s tp -> LambdaLabel s tp
forall s (tp :: CrucibleType).
Nonce s tp -> Atom s tp -> LambdaLabel s tp
LambdaLabel Nonce s tp
n Atom s tp
a)

    mkInjBlock :: Reg s (VariantType ctx)
-> Label s -> BlockID s -> m (BlockIDPair s, Block ext s ret)
mkInjBlock Reg s (VariantType ctx)
reg Label s
rlabel BlockID s
j =
      do let idx :: Index ctx UnitType
idx = Map (BlockID s) (Index ctx UnitType)
idxMap Map (BlockID s) (Index ctx UnitType)
-> BlockID s -> Index ctx UnitType
forall k a. Ord k => Map k a -> k -> a
Map.! BlockID s
j
         (BlockIDPair s
rename, Block ext s ret
injBlock) <- NonceGenerator m s
-> CtxRepr ctx
-> Reg s (VariantType ctx)
-> BlockID s
-> Index ctx UnitType
-> Label s
-> m (BlockIDPair s, Block ext s ret)
forall ext (m :: Type -> Type) s (routing :: Ctx CrucibleType)
       (ret :: CrucibleType).
(TraverseExt ext, Monad m) =>
NonceGenerator m s
-> CtxRepr routing
-> Reg s (VariantType routing)
-> BlockID s
-> Index routing UnitType
-> Label s
-> m (BlockIDPair s, Block ext s ret)
routerEntryBlock NonceGenerator m s
ng CtxRepr ctx
ctx Reg s (VariantType ctx)
reg BlockID s
j Index ctx UnitType
idx Label s
rlabel
         (BlockIDPair s, Block ext s ret)
-> m (BlockIDPair s, Block ext s ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BlockIDPair s
rename, Block ext s ret
injBlock)

    mkLambdaBlock :: [BlockIDPair s]
-> Assignment (LambdaLabel s) ctx
-> BlockID s
-> Index ctx UnitType
-> [Block ext s ret]
-> [Block ext s ret]
mkLambdaBlock [BlockIDPair s]
rename Assignment (LambdaLabel s) ctx
mapping BlockID s
blkId Index ctx UnitType
blkIdx [Block ext s ret]
blks =
      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 (LambdaLabel s UnitType -> BlockID s
forall s (tp :: CrucibleType). LambdaLabel s tp -> BlockID s
LambdaID (Assignment (LambdaLabel s) ctx
mapping Assignment (LambdaLabel s) ctx
-> Index ctx UnitType -> LambdaLabel s UnitType
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx UnitType
blkIdx))
              ValueSet s
forall a. Monoid a => a
mempty
              Seq (Posd (Stmt ext s))
forall a. Monoid a => a
mempty
              (Position -> TermStmt s ret -> Posd (TermStmt s ret)
forall v. Position -> v -> Posd v
Posd Position
internal (BlockID s -> [BlockIDPair s] -> TermStmt s ret
bidToTerm BlockID s
blkId [BlockIDPair s]
rename)) Block ext s ret -> [Block ext s ret] -> [Block ext s ret]
forall a. a -> [a] -> [a]
: [Block ext s ret]
blks

-- | Create a block that switches on a register. This does the work of
-- allocating the new label and discriminant register
routerBlock :: ( TraverseExt ext, Monad m )
            => NonceGenerator m s
            -> CtxRepr routing
            -> Ctx.Assignment (LambdaLabel s) routing
            -> m (Label s, Reg s (VariantType routing), Block ext s ret)
routerBlock :: forall ext (m :: Type -> Type) s (routing :: Ctx CrucibleType)
       (ret :: CrucibleType).
(TraverseExt ext, Monad m) =>
NonceGenerator m s
-> CtxRepr routing
-> Assignment (LambdaLabel s) routing
-> m (Label s, Reg s (VariantType routing), Block ext s ret)
routerBlock NonceGenerator m s
ng CtxRepr routing
ctx Assignment (LambdaLabel s) routing
mapping =
  do Label s
l        <- Nonce s UnitType -> Label s
forall s. Nonce s UnitType -> Label s
Label (Nonce s UnitType -> Label s)
-> m (Nonce s UnitType) -> m (Label s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NonceGenerator m s -> m (Nonce s UnitType)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng
     Reg s (VariantType routing)
destReg  <- NonceGenerator m s
-> Position
-> TypeRepr (VariantType routing)
-> m (Reg s (VariantType routing))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Reg s tp)
freshReg NonceGenerator m s
ng Position
internal (CtxRepr routing -> TypeRepr (VariantType routing)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('VariantType ctx)
VariantRepr CtxRepr routing
ctx)
     Atom s (VariantType routing)
readDest <- NonceGenerator m s
-> Position
-> TypeRepr (VariantType routing)
-> m (Atom s (VariantType routing))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng Position
internal (CtxRepr routing -> TypeRepr (VariantType routing)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('VariantType ctx)
VariantRepr CtxRepr routing
ctx)
     let elim :: TermStmt s ret
elim    = CtxRepr routing
-> Atom s (VariantType routing)
-> Assignment (LambdaLabel s) routing
-> TermStmt s ret
forall (varctx :: Ctx CrucibleType) s (ret :: CrucibleType).
CtxRepr varctx
-> Atom s (VariantType varctx)
-> Assignment (LambdaLabel s) varctx
-> TermStmt s ret
VariantElim CtxRepr routing
ctx Atom s (VariantType routing)
readDest Assignment (LambdaLabel s) routing
mapping
         readVar :: Posd (Stmt ext s)
readVar = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd Position
internal (Atom s (VariantType routing)
-> AtomValue ext s (VariantType routing) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s (VariantType routing)
readDest (Reg s (VariantType routing)
-> AtomValue ext s (VariantType routing)
forall s (tp :: CrucibleType) ext. Reg s tp -> AtomValue ext s tp
ReadReg Reg s (VariantType routing)
destReg))
         funnel :: Block ext s ret
funnel  = 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 (Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
l) ValueSet s
forall a. Monoid a => a
mempty (Posd (Stmt ext s) -> Seq (Posd (Stmt ext s))
forall a. a -> Seq a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Posd (Stmt ext s)
readVar) (Position -> TermStmt s ret -> Posd (TermStmt s ret)
forall v. Position -> v -> Posd v
Posd Position
internal TermStmt s ret
elim)
     (Label s, Reg s (VariantType routing), Block ext s ret)
-> m (Label s, Reg s (VariantType routing), Block ext s ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Label s
l, Reg s (VariantType routing)
destReg, Block ext s ret
funnel)

-- | This creates a block that to be substituted for @origID@.
-- This block will set the given register to the injection
-- given by @destIdx@, and then jump to a router block (described in @routePaths@)
-- that will `switch` on this register. 
routerEntryBlock :: ( TraverseExt ext, Monad m )
                 => NonceGenerator m s
                 -> CtxRepr routing
                 -> Reg s (VariantType routing)
                 -- ^ The register we will switch on
                 -> BlockID s
                 -- ^ The ID of the block we're substituting for
                 -> Ctx.Index routing UnitType
                 -- ^ Which injection in the variant type to use
                 -> Label s
                 -- ^ The label of the router block
                 -> m (BlockIDPair s, Block ext s ret)
routerEntryBlock :: forall ext (m :: Type -> Type) s (routing :: Ctx CrucibleType)
       (ret :: CrucibleType).
(TraverseExt ext, Monad m) =>
NonceGenerator m s
-> CtxRepr routing
-> Reg s (VariantType routing)
-> BlockID s
-> Index routing UnitType
-> Label s
-> m (BlockIDPair s, Block ext s ret)
routerEntryBlock NonceGenerator m s
ng CtxRepr routing
ctx Reg s (VariantType routing)
r BlockID s
origID Index routing UnitType
destIdx Label s
routerLabel =
  do Atom s UnitType
aUnit <- NonceGenerator m s
-> Position -> TypeRepr UnitType -> m (Atom s UnitType)
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng Position
internal TypeRepr UnitType
UnitRepr
     Atom s (VariantType routing)
aInj  <- NonceGenerator m s
-> Position
-> TypeRepr (VariantType routing)
-> m (Atom s (VariantType routing))
forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng Position
internal (CtxRepr routing -> TypeRepr (VariantType routing)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('VariantType ctx)
VariantRepr CtxRepr routing
ctx)
   
     (BlockID s
l, BlockIDPair s
rename) <-
       case BlockID s
origID of
         LabelID Label s
l1 ->
           do Label s
l2 <- (forall (x :: CrucibleType). Nonce s x -> m (Nonce s x))
-> Label s -> m (Label s)
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel (\Nonce s x
_ -> NonceGenerator m s -> m (Nonce s x)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng) Label s
l1
              (BlockID s, BlockIDPair s) -> m (BlockID s, BlockIDPair s)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
l2, Label s -> Label s -> BlockIDPair s
forall s. Label s -> Label s -> BlockIDPair s
Labels Label s
l1 Label s
l2)
         LambdaID l1 :: LambdaLabel s tp
l1@(LambdaLabel Nonce s tp
_ Atom s tp
a) ->
           do Nonce s tp
l' <- NonceGenerator m s -> m (Nonce s tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng
              Nonce s tp
a' <- NonceGenerator m s -> m (Nonce s tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng
              -- knot-tying in the LambdaLabel type results in an infinite loop
              let l2 :: LambdaLabel s tp
l2 = Nonce s tp -> Atom s tp -> LambdaLabel s tp
forall s (tp :: CrucibleType).
Nonce s tp -> Atom s tp -> LambdaLabel s tp
LambdaLabel Nonce s tp
l' Atom s tp
a { atomId = a' }
              (BlockID s, BlockIDPair s) -> m (BlockID s, BlockIDPair s)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LambdaLabel s tp -> BlockID s
forall s (tp :: CrucibleType). LambdaLabel s tp -> BlockID s
LambdaID LambdaLabel s tp
l2, LambdaLabel s tp -> LambdaLabel s tp -> BlockIDPair s
forall s (tp :: CrucibleType).
LambdaLabel s tp -> LambdaLabel s tp -> BlockIDPair s
LambdaLabels LambdaLabel s tp
l1 LambdaLabel s tp
l2)

     let defUnit :: Posd (Stmt ext s)
defUnit = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd Position
internal (Atom s UnitType -> AtomValue ext s UnitType -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s UnitType
aUnit (App ext (Atom s) UnitType -> AtomValue ext s UnitType
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp App ext (Atom s) UnitType
forall ext (f :: CrucibleType -> Type). App ext f UnitType
EmptyApp))
         defVar :: Posd (Stmt ext s)
defVar  = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd Position
internal (Atom s (VariantType routing)
-> AtomValue ext s (VariantType routing) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s (VariantType routing)
aInj (App ext (Atom s) (VariantType routing)
-> AtomValue ext s (VariantType routing)
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (CtxRepr routing
-> Index routing UnitType
-> Atom s UnitType
-> App ext (Atom s) (VariantType routing)
forall (ctx :: Ctx CrucibleType) (tp1 :: CrucibleType)
       (f :: CrucibleType -> Type) ext.
CtxRepr ctx
-> Index ctx tp1 -> f tp1 -> App ext f ('VariantType ctx)
InjectVariant CtxRepr routing
ctx Index routing UnitType
destIdx Atom s UnitType
aUnit)))
         setReg :: Posd (Stmt ext s)
setReg  = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd Position
internal (Reg s (VariantType routing)
-> Atom s (VariantType routing) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Reg s tp -> Atom s tp -> Stmt ext s
SetReg Reg s (VariantType routing)
r Atom s (VariantType routing)
aInj)
         stmts :: Seq (Posd (Stmt ext s))
stmts   = [Posd (Stmt ext s)] -> Seq (Posd (Stmt ext s))
forall a. [a] -> Seq a
Seq.fromList [Posd (Stmt ext s)
defUnit, Posd (Stmt ext s)
defVar, Posd (Stmt ext s)
setReg]
         blk :: Block ext s ret
blk     = 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
l ValueSet s
forall a. Monoid a => a
mempty Seq (Posd (Stmt ext s))
stmts (Position -> TermStmt s ret -> Posd (TermStmt s ret)
forall v. Position -> v -> Posd v
Posd Position
internal (Label s -> TermStmt s ret
forall s (ret :: CrucibleType). Label s -> TermStmt s ret
Jump Label s
routerLabel))

     (BlockIDPair s, Block ext s ret)
-> m (BlockIDPair s, Block ext s ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BlockIDPair s
rename, Block ext s ret
blk)

errorPath :: Map.Map (BlockID s) (Block ext s ret) -> CFGEdge s -> Bool
errorPath :: forall s ext (ret :: CrucibleType).
Map (BlockID s) (Block ext s ret) -> CFGEdge s -> Bool
errorPath Map (BlockID s) (Block ext s ret)
bmap (BlockID s
_, BlockID s
bid) =
  case BlockID s
-> Map (BlockID s) (Block ext s ret) -> Maybe (Block ext s ret)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BlockID s
bid Map (BlockID s) (Block ext s ret)
bmap of
    Just (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm -> Posd Position
_ (ErrorStmt Atom s (StringType Unicode)
_)) -> Bool
True
    Maybe (Block ext s ret)
_ -> Bool
False

-- | Generally useful helpers

freshAtom :: Monad m => NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom :: forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Atom s tp)
freshAtom NonceGenerator m s
ng Position
p TypeRepr tp
tp =
  do Nonce s tp
i <- NonceGenerator m s -> m (Nonce s tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng
     Atom s tp -> m (Atom s tp)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Atom s tp -> m (Atom s tp)) -> Atom s tp -> m (Atom s tp)
forall a b. (a -> b) -> a -> b
$ Atom { atomPosition :: Position
atomPosition = Position
p
                   , atomId :: Nonce s tp
atomId = Nonce s tp
i
                   , atomSource :: AtomSource s tp
atomSource = AtomSource s tp
forall s (tp :: CrucibleType). AtomSource s tp
Assigned
                   , typeOfAtom :: TypeRepr tp
typeOfAtom = TypeRepr tp
tp
                   }

freshReg :: Monad m => NonceGenerator m s -> Position -> TypeRepr tp -> m (Reg s tp)
freshReg :: forall (m :: Type -> Type) s (tp :: CrucibleType).
Monad m =>
NonceGenerator m s -> Position -> TypeRepr tp -> m (Reg s tp)
freshReg NonceGenerator m s
ng Position
p TypeRepr tp
tp =
  do Nonce s tp
i <- NonceGenerator m s -> m (Nonce s tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng
     Reg s tp -> m (Reg s tp)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Reg s tp -> m (Reg s tp)) -> Reg s tp -> m (Reg s tp)
forall a b. (a -> b) -> a -> b
$ Reg { regPosition :: Position
regPosition = Position
p
                  , regId :: Nonce s tp
regId = Nonce s tp
i
                  , typeOfReg :: TypeRepr tp
typeOfReg = TypeRepr tp
tp
                  }
      
findBlock :: CFG ext s init ret -> Label s -> Maybe (Block ext s ret)
findBlock :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Label s -> Maybe (Block ext s ret)
findBlock CFG ext s init ret
g Label s
l =
  (Block ext s ret -> Bool)
-> [Block ext s ret] -> Maybe (Block ext s ret)
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
Fold.find (\Block ext s ret
b -> Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b BlockID s -> BlockID s -> Bool
forall a. Eq a => a -> a -> Bool
== Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
l) (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
g)
  
blockUndefVals :: ValueSet s -> Block ext s ret -> ValueSet s
blockUndefVals :: forall s ext (ret :: CrucibleType).
ValueSet s -> Block ext s ret -> ValueSet s
blockUndefVals ValueSet s
def Block ext s ret
blk = Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockKnownInputs Block ext s ret
blk ValueSet s -> ValueSet s -> ValueSet s
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ ValueSet s
def

blockMap :: CFG ext s init ret -> Map.Map (BlockID s) (Block ext s ret)
blockMap :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Map (BlockID s) (Block ext s ret)
blockMap CFG ext s init ret
cfg = [(BlockID s, Block ext s ret)] -> Map (BlockID s) (Block ext s ret)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b, Block ext s ret
b) | Block ext s ret
b <- 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
cfg ]

internal :: Position
internal :: Position
internal = Position
InternalPos