-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Analysis.Reachable
-- Description      : Compute the reachable subgraph of a CFG
-- Copyright        : (c) Galois, Inc 2015
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- Compute reachability on CFG blocks, reduce the CFG to include just
-- the reachable blocks, and remap block labels in the program to point
-- to the new, relabeled blocks.
------------------------------------------------------------------------

{-# LANGUAGE ScopedTypeVariables #-}
module Lang.Crucible.Analysis.Reachable
  ( reachableCFG
  ) where

import           Control.Monad.Identity
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.Maybe (fromMaybe)
import qualified Data.Bimap as Bimap
import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.TraversableFC
import qualified Data.Parameterized.Context as Ctx
import           Lang.Crucible.CFG.Core

remapBlockID :: MapF (BlockID b) (BlockID b') -> BlockID b a -> BlockID b' a
remapBlockID :: forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (a :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b') -> BlockID b a -> BlockID b' a
remapBlockID MapF (BlockID b) (BlockID b')
m BlockID b a
b =
  BlockID b' a -> Maybe (BlockID b' a) -> BlockID b' a
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> BlockID b' a
forall a. HasCallStack => [Char] -> a
error ([Char] -> BlockID b' a) -> [Char] -> BlockID b' a
forall a b. (a -> b) -> a -> b
$ [Char]
"Could not remap block " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BlockID b a -> [Char]
forall a. Show a => a -> [Char]
show BlockID b a
b)
            (BlockID b a
-> MapF (BlockID b) (BlockID b') -> Maybe (BlockID b' a)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup BlockID b a
b MapF (BlockID b) (BlockID b')
m)

remapJumpTarget :: MapF (BlockID b) (BlockID b')
                -> JumpTarget b c -> JumpTarget b' c
remapJumpTarget :: forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (c :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b') -> JumpTarget b c -> JumpTarget b' c
remapJumpTarget MapF (BlockID b) (BlockID b')
m (JumpTarget BlockID b args
x CtxRepr args
r Assignment (Reg c) args
a) = BlockID b' args
-> CtxRepr args -> Assignment (Reg c) args -> JumpTarget b' c
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) (ctx :: Ctx CrucibleType).
BlockID blocks args
-> CtxRepr args
-> Assignment (Reg ctx) args
-> JumpTarget blocks ctx
JumpTarget (MapF (BlockID b) (BlockID b') -> BlockID b args -> BlockID b' args
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (a :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b') -> BlockID b a -> BlockID b' a
remapBlockID MapF (BlockID b) (BlockID b')
m BlockID b args
x) CtxRepr args
r Assignment (Reg c) args
a

remapSwitchTarget :: MapF (BlockID b) (BlockID b')
                  -> SwitchTarget b c r -> SwitchTarget b' c r
remapSwitchTarget :: forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (c :: Ctx CrucibleType) (r :: CrucibleType).
MapF (BlockID b) (BlockID b')
-> SwitchTarget b c r -> SwitchTarget b' c r
remapSwitchTarget MapF (BlockID b) (BlockID b')
m (SwitchTarget BlockID b (args ::> r)
x CtxRepr args
r Assignment (Reg c) args
a) = BlockID b' (args ::> r)
-> CtxRepr args -> Assignment (Reg c) args -> SwitchTarget b' c r
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) (tp :: CrucibleType)
       (ctx :: Ctx CrucibleType).
BlockID blocks (args ::> tp)
-> CtxRepr args
-> Assignment (Reg ctx) args
-> SwitchTarget blocks ctx tp
SwitchTarget (MapF (BlockID b) (BlockID b')
-> BlockID b (args ::> r) -> BlockID b' (args ::> r)
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (a :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b') -> BlockID b a -> BlockID b' a
remapBlockID MapF (BlockID b) (BlockID b')
m BlockID b (args ::> r)
x) CtxRepr args
r Assignment (Reg c) args
a


remapTermStmt :: MapF (BlockID b) (BlockID b') -> TermStmt b ret c -> TermStmt b' ret c
remapTermStmt :: forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (c :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b')
-> TermStmt b ret c -> TermStmt b' ret c
remapTermStmt MapF (BlockID b) (BlockID b')
m TermStmt b ret c
ts =
  case TermStmt b ret c
ts of
    Jump JumpTarget b c
jmp -> JumpTarget b' c -> TermStmt b' ret c
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
Jump (MapF (BlockID b) (BlockID b') -> JumpTarget b c -> JumpTarget b' c
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (c :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b') -> JumpTarget b c -> JumpTarget b' c
remapJumpTarget MapF (BlockID b) (BlockID b')
m JumpTarget b c
jmp)
    Br Reg c BoolType
c JumpTarget b c
x JumpTarget b c
y -> Reg c BoolType
-> JumpTarget b' c -> JumpTarget b' c -> TermStmt b' ret c
forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
Reg ctx BoolType
-> JumpTarget blocks ctx
-> JumpTarget blocks ctx
-> TermStmt blocks ret ctx
Br Reg c BoolType
c (MapF (BlockID b) (BlockID b') -> JumpTarget b c -> JumpTarget b' c
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (c :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b') -> JumpTarget b c -> JumpTarget b' c
remapJumpTarget MapF (BlockID b) (BlockID b')
m JumpTarget b c
x) (MapF (BlockID b) (BlockID b') -> JumpTarget b c -> JumpTarget b' c
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (c :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b') -> JumpTarget b c -> JumpTarget b' c
remapJumpTarget MapF (BlockID b) (BlockID b')
m JumpTarget b c
y)
    MaybeBranch TypeRepr tp
tp Reg c (MaybeType tp)
r SwitchTarget b c tp
x JumpTarget b c
y -> TypeRepr tp
-> Reg c (MaybeType tp)
-> SwitchTarget b' c tp
-> JumpTarget b' c
-> TermStmt b' ret c
forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
TypeRepr tp
-> Reg ctx (MaybeType tp)
-> SwitchTarget blocks ctx tp
-> JumpTarget blocks ctx
-> TermStmt blocks ret ctx
MaybeBranch TypeRepr tp
tp Reg c (MaybeType tp)
r (MapF (BlockID b) (BlockID b')
-> SwitchTarget b c tp -> SwitchTarget b' c tp
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (c :: Ctx CrucibleType) (r :: CrucibleType).
MapF (BlockID b) (BlockID b')
-> SwitchTarget b c r -> SwitchTarget b' c r
remapSwitchTarget MapF (BlockID b) (BlockID b')
m SwitchTarget b c tp
x) (MapF (BlockID b) (BlockID b') -> JumpTarget b c -> JumpTarget b' c
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (c :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b') -> JumpTarget b c -> JumpTarget b' c
remapJumpTarget MapF (BlockID b) (BlockID b')
m JumpTarget b c
y)
    VariantElim CtxRepr varctx
c Reg c (VariantType varctx)
r Assignment (SwitchTarget b c) varctx
a -> CtxRepr varctx
-> Reg c (VariantType varctx)
-> Assignment (SwitchTarget b' c) varctx
-> TermStmt b' ret c
forall (varctx :: Ctx CrucibleType) (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
CtxRepr varctx
-> Reg ctx (VariantType varctx)
-> Assignment (SwitchTarget blocks ctx) varctx
-> TermStmt blocks ret ctx
VariantElim CtxRepr varctx
c Reg c (VariantType varctx)
r ((forall (x :: CrucibleType).
 SwitchTarget b c x -> SwitchTarget b' c x)
-> forall (x :: Ctx CrucibleType).
   Assignment (SwitchTarget b c) x -> Assignment (SwitchTarget b' c) 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 (MapF (BlockID b) (BlockID b')
-> SwitchTarget b c x -> SwitchTarget b' c x
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (c :: Ctx CrucibleType) (r :: CrucibleType).
MapF (BlockID b) (BlockID b')
-> SwitchTarget b c r -> SwitchTarget b' c r
remapSwitchTarget MapF (BlockID b) (BlockID b')
m) Assignment (SwitchTarget b c) varctx
a)
    Return Reg c ret
r          -> Reg c ret -> TermStmt b' ret c
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
Reg ctx ret -> TermStmt blocks ret ctx
Return Reg c ret
r
    TailCall Reg c (FunctionHandleType args ret)
f CtxRepr args
c Assignment (Reg c) args
a    -> Reg c (FunctionHandleType args ret)
-> CtxRepr args -> Assignment (Reg c) args -> TermStmt b' ret c
forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Reg ctx (FunctionHandleType args ret)
-> CtxRepr args
-> Assignment (Reg ctx) args
-> TermStmt blocks ret ctx
TailCall Reg c (FunctionHandleType args ret)
f CtxRepr args
c Assignment (Reg c) args
a
    ErrorStmt Reg c (StringType Unicode)
r       -> Reg c (StringType Unicode) -> TermStmt b' ret c
forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
Reg ctx (StringType Unicode) -> TermStmt blocks ret ctx
ErrorStmt Reg c (StringType Unicode)
r

remapBlock :: MapF (BlockID b) (BlockID b')
           -> BlockID b' ctx
           -> Block ext b r ctx
           -> Block ext b' r ctx
remapBlock :: forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) ext (r :: CrucibleType).
MapF (BlockID b) (BlockID b')
-> BlockID b' ctx -> Block ext b r ctx -> Block ext b' r ctx
remapBlock MapF (BlockID b) (BlockID b')
m BlockID b' ctx
nm Block ext b r ctx
b =
  Block { blockID :: BlockID b' ctx
blockID = BlockID b' ctx
nm
        , blockInputs :: CtxRepr ctx
blockInputs = Block ext b r ctx -> CtxRepr ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs Block ext b r ctx
b
        , _blockStmts :: StmtSeq ext b' r ctx
_blockStmts =
          Identity (StmtSeq ext b' r ctx) -> StmtSeq ext b' r ctx
forall a. Identity a -> a
runIdentity (Identity (StmtSeq ext b' r ctx) -> StmtSeq ext b' r ctx)
-> Identity (StmtSeq ext b' r ctx) -> StmtSeq ext b' r ctx
forall a b. (a -> b) -> a -> b
$
            (forall (ctx :: Ctx CrucibleType).
 (ProgramLoc, TermStmt b r ctx) -> Identity (StmtSeq ext b' r ctx))
-> StmtSeq ext b r ctx -> Identity (StmtSeq ext b' r ctx)
forall (f :: Type -> Type) (b :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) ext (b' :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
Functor f =>
(forall (ctx :: Ctx CrucibleType).
 (ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx))
-> StmtSeq ext b ret args -> f (StmtSeq ext b' ret args)
stmtSeqTermStmt
              (\(ProgramLoc
l,TermStmt b r ctx
s) -> StmtSeq ext b' r ctx -> Identity (StmtSeq ext b' r ctx)
forall a. a -> Identity a
Identity (ProgramLoc -> TermStmt b' r ctx -> StmtSeq ext b' r ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) ext.
ProgramLoc -> TermStmt blocks ret ctx -> StmtSeq ext blocks ret ctx
TermStmt ProgramLoc
l (MapF (BlockID b) (BlockID b')
-> TermStmt b r ctx -> TermStmt b' r ctx
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (c :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b')
-> TermStmt b ret c -> TermStmt b' ret c
remapTermStmt MapF (BlockID b) (BlockID b')
m TermStmt b r ctx
s)))
              (Block ext b r ctx -> StmtSeq ext b r ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> StmtSeq ext blocks ret ctx
_blockStmts Block ext b r ctx
b)
        }

mkOldMap :: forall ext b b' r
         .  Ctx.Assignment (Block ext b r) b'
         -> MapF (BlockID b) (BlockID b')
mkOldMap :: forall ext (b :: Ctx (Ctx CrucibleType))
       (b' :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Assignment (Block ext b r) b' -> MapF (BlockID b) (BlockID b')
mkOldMap Assignment (Block ext b r) b'
a = Size b'
-> (forall (tp :: Ctx CrucibleType).
    MapF (BlockID b) (BlockID b')
    -> Index b' tp -> MapF (BlockID b) (BlockID b'))
-> MapF (BlockID b) (BlockID b')
-> MapF (BlockID b) (BlockID b')
forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
Ctx.forIndex (Assignment (Block ext b r) b' -> Size b'
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment (Block ext b r) b'
a) MapF (BlockID b) (BlockID b')
-> Index b' tp -> MapF (BlockID b) (BlockID b')
forall (tp :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b')
-> Index b' tp -> MapF (BlockID b) (BlockID b')
f MapF (BlockID b) (BlockID b')
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
  where f :: MapF (BlockID b) (BlockID b')
          -> Ctx.Index b' c
          -> MapF (BlockID b) (BlockID b')
        f :: forall (tp :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b')
-> Index b' tp -> MapF (BlockID b) (BlockID b')
f MapF (BlockID b) (BlockID b')
m Index b' c
new_index = BlockID b c
-> BlockID b' c
-> MapF (BlockID b) (BlockID b')
-> MapF (BlockID b) (BlockID b')
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert (Block ext b r c -> BlockID b c
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext b r c
b) (Index b' c -> BlockID b' c
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID Index b' c
new_index) MapF (BlockID b) (BlockID b')
m
          where b :: Block ext b r c
b = Assignment (Block ext b r) b'
a Assignment (Block ext b r) b' -> Index b' c -> Block ext b r c
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index b' c
new_index

remapBlockMap :: forall ext b b' ret
               . MapF (BlockID b) (BlockID b')
              -> Ctx.Assignment (Block ext b ret) b'
                 -- ^ Map new blocks to old block IDs.
              -> BlockMap ext b' ret
remapBlockMap :: forall ext (b :: Ctx (Ctx CrucibleType))
       (b' :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
MapF (BlockID b) (BlockID b')
-> Assignment (Block ext b ret) b' -> BlockMap ext b' ret
remapBlockMap MapF (BlockID b) (BlockID b')
oldToNew Assignment (Block ext b ret) b'
newToOld = Size b'
-> (forall {tp :: Ctx CrucibleType}.
    Index b' tp -> Block ext b' ret tp)
-> Assignment (Block ext b' ret) b'
forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
Ctx.generate (Assignment (Block ext b ret) b' -> Size b'
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment (Block ext b ret) b'
newToOld) ((forall {tp :: Ctx CrucibleType}.
  Index b' tp -> Block ext b' ret tp)
 -> Assignment (Block ext b' ret) b')
-> (forall {tp :: Ctx CrucibleType}.
    Index b' tp -> Block ext b' ret tp)
-> Assignment (Block ext b' ret) b'
forall a b. (a -> b) -> a -> b
$ Index b' tp -> Block ext b' ret tp
forall {tp :: Ctx CrucibleType}. Index b' tp -> Block ext b' ret tp
f
  where f :: Ctx.Index b' ctx -> Block ext b' ret ctx
        f :: forall {tp :: Ctx CrucibleType}. Index b' tp -> Block ext b' ret tp
f Index b' ctx
i = MapF (BlockID b) (BlockID b')
-> BlockID b' ctx -> Block ext b ret ctx -> Block ext b' ret ctx
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) ext (r :: CrucibleType).
MapF (BlockID b) (BlockID b')
-> BlockID b' ctx -> Block ext b r ctx -> Block ext b' r ctx
remapBlock MapF (BlockID b) (BlockID b')
oldToNew (Index b' ctx -> BlockID b' ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID Index b' ctx
i) (Assignment (Block ext b ret) b'
newToOld Assignment (Block ext b ret) b'
-> Index b' ctx -> Block ext b ret ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index b' ctx
i)

exploreReachable :: BlockMap ext blocks ret
                 -> BlockID blocks init
                 -> Map (Some (BlockID blocks)) Int
exploreReachable :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (init :: Ctx CrucibleType).
BlockMap ext blocks ret
-> BlockID blocks init -> Map (Some (BlockID blocks)) Int
exploreReachable BlockMap ext blocks ret
m BlockID blocks init
d = BlockMap ext blocks ret
-> [Some (BlockID blocks)]
-> Map (Some (BlockID blocks)) Int
-> Map (Some (BlockID blocks)) Int
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret
-> [Some (BlockID blocks)]
-> Map (Some (BlockID blocks)) Int
-> Map (Some (BlockID blocks)) Int
exploreReachable' BlockMap ext blocks ret
m [BlockID blocks init -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks init
d] Map (Some (BlockID blocks)) Int
forall k a. Map k a
Map.empty

exploreReachable' :: BlockMap ext blocks ret
                  -> [Some (BlockID blocks)]
                  -> Map (Some (BlockID blocks)) Int
                  -> Map (Some (BlockID blocks)) Int
exploreReachable' :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret
-> [Some (BlockID blocks)]
-> Map (Some (BlockID blocks)) Int
-> Map (Some (BlockID blocks)) Int
exploreReachable' BlockMap ext blocks ret
_ [] Map (Some (BlockID blocks)) Int
r = Map (Some (BlockID blocks)) Int
r
exploreReachable' BlockMap ext blocks ret
m (Some BlockID blocks x
h:[Some (BlockID blocks)]
l) Map (Some (BlockID blocks)) Int
r =
  case Some (BlockID blocks)
-> Map (Some (BlockID blocks)) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (BlockID blocks x -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks x
h) Map (Some (BlockID blocks)) Int
r of
    Just Int
c -> BlockMap ext blocks ret
-> [Some (BlockID blocks)]
-> Map (Some (BlockID blocks)) Int
-> Map (Some (BlockID blocks)) Int
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret
-> [Some (BlockID blocks)]
-> Map (Some (BlockID blocks)) Int
-> Map (Some (BlockID blocks)) Int
exploreReachable' BlockMap ext blocks ret
m [Some (BlockID blocks)]
l (Some (BlockID blocks)
-> Int
-> Map (Some (BlockID blocks)) Int
-> Map (Some (BlockID blocks)) Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (BlockID blocks x -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks x
h) (Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Map (Some (BlockID blocks)) Int
r)
    Maybe Int
Nothing -> do
      let b :: Block ext blocks ret x
b = BlockID blocks x
-> BlockMap ext blocks ret -> Block ext blocks ret x
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock BlockID blocks x
h BlockMap ext blocks ret
m
      BlockMap ext blocks ret
-> [Some (BlockID blocks)]
-> Map (Some (BlockID blocks)) Int
-> Map (Some (BlockID blocks)) Int
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret
-> [Some (BlockID blocks)]
-> Map (Some (BlockID blocks)) Int
-> Map (Some (BlockID blocks)) Int
exploreReachable' BlockMap ext blocks ret
m (Block ext blocks ret x -> [Some (BlockID blocks)]
forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
       (a :: Ctx CrucibleType).
Block ext b r a -> [Some (BlockID b)]
nextBlocks Block ext blocks ret x
b [Some (BlockID blocks)]
-> [Some (BlockID blocks)] -> [Some (BlockID blocks)]
forall a. [a] -> [a] -> [a]
++ [Some (BlockID blocks)]
l) (Some (BlockID blocks)
-> Int
-> Map (Some (BlockID blocks)) Int
-> Map (Some (BlockID blocks)) Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (BlockID blocks x -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks x
h) Int
1 Map (Some (BlockID blocks)) Int
r)

insReachable :: BlockMap ext b r
             -> Some (Ctx.Assignment (Block ext b r))
             -> Some (BlockID b)
             -> Some (Ctx.Assignment (Block ext b r))
insReachable :: forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
BlockMap ext b r
-> Some (Assignment (Block ext b r))
-> Some (BlockID b)
-> Some (Assignment (Block ext b r))
insReachable BlockMap ext b r
m (Some Assignment (Block ext b r) x
a) (Some (BlockID Index b x
block_id)) = Assignment (Block ext b r) (x ::> x)
-> Some (Assignment (Block ext b r))
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Assignment (Block ext b r) (x ::> x)
 -> Some (Assignment (Block ext b r)))
-> Assignment (Block ext b r) (x ::> x)
-> Some (Assignment (Block ext b r))
forall a b. (a -> b) -> a -> b
$ Assignment (Block ext b r) x
a Assignment (Block ext b r) x
-> Block ext b r x -> Assignment (Block ext b r) (x ::> x)
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.:> (BlockMap ext b r
m BlockMap ext b r -> Index b x -> Block ext b r x
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index b x
block_id)



reachableCFG :: CFG ext blocks init ret -> SomeCFG ext init ret
reachableCFG :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> SomeCFG ext init ret
reachableCFG CFG ext blocks init ret
g =
    case (Some (Assignment (Block ext blocks ret))
 -> Some (BlockID blocks)
 -> Some (Assignment (Block ext blocks ret)))
-> Some (Assignment (Block ext blocks ret))
-> [Some (BlockID blocks)]
-> Some (Assignment (Block ext blocks 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
foldl (BlockMap ext blocks ret
-> Some (Assignment (Block ext blocks ret))
-> Some (BlockID blocks)
-> Some (Assignment (Block ext blocks ret))
forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
BlockMap ext b r
-> Some (Assignment (Block ext b r))
-> Some (BlockID b)
-> Some (Assignment (Block ext b r))
insReachable BlockMap ext blocks ret
old_map) (Assignment (Block ext blocks ret) EmptyCtx
-> Some (Assignment (Block ext blocks ret))
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Assignment (Block ext blocks ret) EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty) (Map (Some (BlockID blocks)) Int -> [Some (BlockID blocks)]
forall k a. Map k a -> [k]
Map.keys Map (Some (BlockID blocks)) Int
reachables) of
      Some Assignment (Block ext blocks ret) x
newToOld ->
--          trace ("Size change: " ++ show (Ctx.sizeInt (Ctx.size old_map) - Ctx.sizeInt (Ctx.size new_map))) $
                 CFG ext x init ret -> SomeCFG ext init ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> SomeCFG ext init ret
SomeCFG CFG ext x init ret
g'
        where oldToNew :: MapF (BlockID blocks) (BlockID x)
oldToNew = Assignment (Block ext blocks ret) x
-> MapF (BlockID blocks) (BlockID x)
forall ext (b :: Ctx (Ctx CrucibleType))
       (b' :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Assignment (Block ext b r) b' -> MapF (BlockID b) (BlockID b')
mkOldMap Assignment (Block ext blocks ret) x
newToOld
              new_map :: BlockMap ext x ret
new_map = MapF (BlockID blocks) (BlockID x)
-> Assignment (Block ext blocks ret) x -> BlockMap ext x ret
forall ext (b :: Ctx (Ctx CrucibleType))
       (b' :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
MapF (BlockID b) (BlockID b')
-> Assignment (Block ext b ret) b' -> BlockMap ext b' ret
remapBlockMap MapF (BlockID blocks) (BlockID x)
oldToNew Assignment (Block ext blocks ret) x
newToOld
              new_breakpoints :: Bimap BreakpointName (Some (BlockID x))
new_breakpoints = (Some (BlockID blocks) -> Some (BlockID x))
-> Bimap BreakpointName (Some (BlockID blocks))
-> Bimap BreakpointName (Some (BlockID x))
forall c b a. Ord c => (b -> c) -> Bimap a b -> Bimap a c
Bimap.mapR ((forall (tp :: Ctx CrucibleType).
 BlockID blocks tp -> BlockID x tp)
-> Some (BlockID blocks) -> Some (BlockID x)
forall {k} (f :: k -> Type) (g :: k -> Type).
(forall (tp :: k). f tp -> g tp) -> Some f -> Some g
mapSome ((forall (tp :: Ctx CrucibleType).
  BlockID blocks tp -> BlockID x tp)
 -> Some (BlockID blocks) -> Some (BlockID x))
-> (forall (tp :: Ctx CrucibleType).
    BlockID blocks tp -> BlockID x tp)
-> Some (BlockID blocks)
-> Some (BlockID x)
forall a b. (a -> b) -> a -> b
$ MapF (BlockID blocks) (BlockID x)
-> BlockID blocks tp -> BlockID x tp
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (a :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b') -> BlockID b a -> BlockID b' a
remapBlockID MapF (BlockID blocks) (BlockID x)
oldToNew) (CFG ext blocks init ret
-> Bimap BreakpointName (Some (BlockID blocks))
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Bimap BreakpointName (Some (BlockID blocks))
cfgBreakpoints CFG ext blocks init ret
g)
              g' :: CFG ext x init ret
g' = CFG { cfgHandle :: FnHandle init ret
cfgHandle = CFG ext blocks init ret -> FnHandle init ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle CFG ext blocks init ret
g
                       , cfgBlockMap :: BlockMap ext x ret
cfgBlockMap = BlockMap ext x ret
new_map
                       , cfgEntryBlockID :: BlockID x init
cfgEntryBlockID = MapF (BlockID blocks) (BlockID x)
-> BlockID blocks init -> BlockID x init
forall (b :: Ctx (Ctx CrucibleType)) (b' :: Ctx (Ctx CrucibleType))
       (a :: Ctx CrucibleType).
MapF (BlockID b) (BlockID b') -> BlockID b a -> BlockID b' a
remapBlockID MapF (BlockID blocks) (BlockID x)
oldToNew BlockID blocks init
entry_id
                       , cfgBreakpoints :: Bimap BreakpointName (Some (BlockID x))
cfgBreakpoints = Bimap BreakpointName (Some (BlockID x))
new_breakpoints
                       }
  where old_map :: BlockMap ext blocks ret
old_map = CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
g
        entry_id :: BlockID blocks init
entry_id = CFG ext blocks init ret -> BlockID blocks init
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgEntryBlockID CFG ext blocks init ret
g
        reachables :: Map (Some (BlockID blocks)) Int
reachables = BlockMap ext blocks ret
-> BlockID blocks init -> Map (Some (BlockID blocks)) Int
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (init :: Ctx CrucibleType).
BlockMap ext blocks ret
-> BlockID blocks init -> Map (Some (BlockID blocks)) Int
exploreReachable BlockMap ext blocks ret
old_map BlockID blocks init
entry_id