-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Analysis.Postdom
-- Description      : Populates postdominator entries in CFG blocks.
-- Copyright        : (c) Galois, Inc 2014
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module provides a method for populating the postdominator fields
-- in blocks of a Core SSA-form CFG.
------------------------------------------------------------------------
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
module Lang.Crucible.Analysis.Postdom
  ( postdomInfo
  , breakpointPostdomInfo
  , validatePostdom
  ) where

import           Control.Monad.State
import qualified Data.Bimap as Bimap
import           Data.Functor.Const
import qualified Data.Graph.Inductive as G
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.Maybe
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.TraversableFC
import qualified Data.Set as Set

import           Lang.Crucible.CFG.Core

-- | Convert a block ID to a node
toNode :: BlockID blocks ctx -> G.Node
toNode :: forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
BlockID blocks ctx -> Node
toNode (BlockID Index blocks ctx
b) = Node
1 Node -> Node -> Node
forall a. Num a => a -> a -> a
+ Index blocks ctx -> Node
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Node
Ctx.indexVal Index blocks ctx
b

-- | Create
reverseEdge :: Int -> Block ext blocks ret ctx -> G.LEdge ()
reverseEdge :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Node -> Block ext blocks ret ctx -> LEdge ()
reverseEdge Node
d Block ext blocks ret ctx
b = (Node
d, BlockID blocks ctx -> Node
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
BlockID blocks ctx -> Node
toNode (Block ext blocks ret ctx -> BlockID blocks ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret ctx
b), ())

-- | For a given block with out edges l, return edges from
-- each block in @l@ to @b@.
inEdges :: Block ext blocks ret ctx -> [G.LEdge ()]
inEdges :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> [LEdge ()]
inEdges Block ext blocks ret ctx
b =
  case Block ext blocks ret ctx
-> (forall (ctx :: Ctx CrucibleType).
    ProgramLoc
    -> TermStmt blocks ret ctx -> Maybe [Some (BlockID blocks)])
-> Maybe [Some (BlockID blocks)]
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) r.
Block ext blocks ret args
-> (forall (ctx :: Ctx CrucibleType).
    ProgramLoc -> TermStmt blocks ret ctx -> r)
-> r
withBlockTermStmt Block ext blocks ret ctx
b (\ProgramLoc
_ -> TermStmt blocks ret ctx -> Maybe [Some (BlockID blocks)]
forall (b :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TermStmt b ret ctx -> Maybe [Some (BlockID b)]
termStmtNextBlocks) of
    Maybe [Some (BlockID blocks)]
Nothing -> [Node -> Block ext blocks ret ctx -> LEdge ()
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Node -> Block ext blocks ret ctx -> LEdge ()
reverseEdge Node
0 Block ext blocks ret ctx
b]
    Just [Some (BlockID blocks)]
l -> (\(Some BlockID blocks x
n) -> BlockID blocks x -> Node
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
BlockID blocks ctx -> Node
toNode BlockID blocks x
n Node -> Block ext blocks ret ctx -> LEdge ()
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Node -> Block ext blocks ret ctx -> LEdge ()
`reverseEdge` Block ext blocks ret ctx
b) (Some (BlockID blocks) -> LEdge ())
-> [Some (BlockID blocks)] -> [LEdge ()]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Some (BlockID blocks)]
l

inEdgeGraph :: BlockMap ext blocks ret -> [Some (BlockID blocks)] -> G.UGr
inEdgeGraph :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret -> [Some (BlockID blocks)] -> UGr
inEdgeGraph BlockMap ext blocks ret
m [Some (BlockID blocks)]
breakpointIds = [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 = Node
0 Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: (forall (x :: Ctx CrucibleType). Block ext blocks ret x -> Node)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (Block ext blocks ret) x -> [Node]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: Ctx CrucibleType -> Type) a.
(forall (x :: Ctx CrucibleType). f x -> a)
-> forall (x :: Ctx (Ctx CrucibleType)). Assignment f x -> [a]
toListFC (BlockID blocks x -> Node
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
BlockID blocks ctx -> Node
toNode (BlockID blocks x -> Node)
-> (Block ext blocks ret x -> BlockID blocks x)
-> Block ext blocks ret x
-> Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block ext blocks ret x -> BlockID blocks x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID) BlockMap ext blocks ret
m
        cfgEdges :: [LEdge ()]
cfgEdges = (forall (x :: Ctx CrucibleType).
 Block ext blocks ret x -> [LEdge ()])
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (Block ext blocks ret) x -> [LEdge ()]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) m.
(FoldableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
forall (f :: Ctx CrucibleType -> Type) m.
Monoid m =>
(forall (x :: Ctx CrucibleType). f x -> m)
-> forall (x :: Ctx (Ctx CrucibleType)). Assignment f x -> m
foldMapFC Block ext blocks ret x -> [LEdge ()]
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> [LEdge ()]
forall (x :: Ctx CrucibleType).
Block ext blocks ret x -> [LEdge ()]
inEdges BlockMap ext blocks ret
m
        breakpointEdges :: [LEdge ()]
breakpointEdges = (Some (BlockID blocks) -> LEdge ())
-> [Some (BlockID blocks)] -> [LEdge ()]
forall a b. (a -> b) -> [a] -> [b]
map (\(Some BlockID blocks x
bid) -> Node -> Block ext blocks ret x -> LEdge ()
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Node -> Block ext blocks ret ctx -> LEdge ()
reverseEdge Node
0 (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
bid BlockMap ext blocks ret
m))
                              [Some (BlockID blocks)]
breakpointIds
        edges :: [LEdge ()]
edges = [LEdge ()]
cfgEdges [LEdge ()] -> [LEdge ()] -> [LEdge ()]
forall a. [a] -> [a] -> [a]
++ [LEdge ()]
breakpointEdges

-- | Return subgraph of nodes reachable from given node.
reachableSubgraph :: G.Node -> G.UGr -> G.UGr
reachableSubgraph :: Node -> UGr -> UGr
reachableSubgraph Node
initNode UGr
g = [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 [LNode ()]
nl [LEdge ()]
el
  where reachableNodes :: Set Node
reachableNodes = [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> Set Node) -> [Node] -> Set Node
forall a b. (a -> b) -> a -> b
$ Node -> UGr -> [Node]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
Node -> gr a b -> [Node]
G.bfs Node
initNode UGr
g
        keepNode :: Node -> Bool
keepNode = (Node -> Set Node -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Node
reachableNodes)
        nl :: [LNode ()]
nl = (LNode () -> Bool) -> [LNode ()] -> [LNode ()]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Node
n,()
_) -> Node -> Bool
keepNode Node
n) (UGr -> [LNode ()]
forall a b. Gr a b -> [LNode a]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
gr a b -> [LNode a]
G.labNodes UGr
g)

        keepEdge :: LEdge () -> Bool
keepEdge (Node
s,Node
e,()
_) = Node -> Bool
keepNode Node
s Bool -> Bool -> Bool
&& Node -> Bool
keepNode Node
e
        el :: [LEdge ()]
el = (LEdge () -> Bool) -> [LEdge ()] -> [LEdge ()]
forall a. (a -> Bool) -> [a] -> [a]
filter LEdge () -> Bool
keepEdge (UGr -> [LEdge ()]
forall a b. Gr a b -> [LEdge b]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
gr a b -> [LEdge b]
G.labEdges UGr
g)

nodeToBlockIDMap :: BlockMap ext blocks ret
                 -> Map G.Node (Some (BlockID blocks))
nodeToBlockIDMap :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret -> Map Node (Some (BlockID blocks))
nodeToBlockIDMap =
  (forall (x :: Ctx CrucibleType).
 Block ext blocks ret x
 -> Map Node (Some (BlockID blocks))
 -> Map Node (Some (BlockID blocks)))
-> forall (x :: Ctx (Ctx CrucibleType)).
   Map Node (Some (BlockID blocks))
   -> Assignment (Block ext blocks ret) x
   -> Map Node (Some (BlockID blocks))
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). f x -> b -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: Ctx CrucibleType -> Type) b.
(forall (x :: Ctx CrucibleType). f x -> b -> b)
-> forall (x :: Ctx (Ctx CrucibleType)). b -> Assignment f x -> b
foldrFC (\Block ext blocks ret x
b -> Node
-> Some (BlockID blocks)
-> Map Node (Some (BlockID blocks))
-> Map Node (Some (BlockID blocks))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (BlockID blocks x -> Node
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
BlockID blocks ctx -> Node
toNode (Block ext blocks ret x -> BlockID blocks x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret x
b)) (BlockID blocks x -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Block ext blocks ret x -> BlockID blocks x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret x
b)))
          Map Node (Some (BlockID blocks))
forall k a. Map k a
Map.empty

postdomMap :: forall ext blocks ret
            . BlockMap ext blocks ret
           -> [Some (BlockID blocks)]
           -> Map (Some (BlockID blocks)) [Some (BlockID blocks)]
postdomMap :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret
-> [Some (BlockID blocks)]
-> Map (Some (BlockID blocks)) [Some (BlockID blocks)]
postdomMap BlockMap ext blocks ret
m [Some (BlockID blocks)]
breakpointIds = Map (Some (BlockID blocks)) [Some (BlockID blocks)]
r
  where g0 :: UGr
g0 = BlockMap ext blocks ret -> [Some (BlockID blocks)] -> UGr
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret -> [Some (BlockID blocks)] -> UGr
inEdgeGraph BlockMap ext blocks ret
m [Some (BlockID blocks)]
breakpointIds
        g :: UGr
g = Node -> UGr -> UGr
reachableSubgraph Node
0 UGr
g0

        idMap :: Map Node (Some (BlockID blocks))
idMap = BlockMap ext blocks ret -> Map Node (Some (BlockID blocks))
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret -> Map Node (Some (BlockID blocks))
nodeToBlockIDMap BlockMap ext blocks ret
m
        f :: Int -> Maybe (Some (BlockID blocks))
        f :: Node -> Maybe (Some (BlockID blocks))
f Node
0 = Maybe (Some (BlockID blocks))
forall a. Maybe a
Nothing
        f Node
i = Node
-> Map Node (Some (BlockID blocks))
-> Maybe (Some (BlockID blocks))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Node
i Map Node (Some (BlockID blocks))
idMap
        -- Map each block to the postdominator for the block.
        r :: Map (Some (BlockID blocks)) [Some (BlockID blocks)]
r = [(Some (BlockID blocks), [Some (BlockID blocks)])]
-> Map (Some (BlockID blocks)) [Some (BlockID blocks)]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
          [ (Some (BlockID blocks)
pd_id, (Node -> Maybe (Some (BlockID blocks)))
-> [Node] -> [Some (BlockID blocks)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Node -> Maybe (Some (BlockID blocks))
f [Node]
l)
          | (Node
pd,Node
_:[Node]
l)  <- UGr -> Node -> [(Node, [Node])]
forall (gr :: Type -> Type -> Type) a b.
Graph gr =>
gr a b -> Node -> [(Node, [Node])]
G.dom UGr
g Node
0
          , Node
pd Node -> Node -> Bool
forall a. Ord a => a -> a -> Bool
> Node
0
          -- Get the post dominator blkID, using a total version of:
          --    let Just pd_id = Map.lookup pd idMap
          , Some (BlockID blocks)
pd_id <- [Maybe (Some (BlockID blocks))] -> [Some (BlockID blocks)]
forall a. [Maybe a] -> [a]
catMaybes [ Node
-> Map Node (Some (BlockID blocks))
-> Maybe (Some (BlockID blocks))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Node
pd Map Node (Some (BlockID blocks))
idMap ]
          ]

postdomAssignment :: forall ext blocks ret
                   . BlockMap ext blocks ret
                  -> [Some (BlockID blocks)]
                  -> CFGPostdom blocks
postdomAssignment :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret
-> [Some (BlockID blocks)] -> CFGPostdom blocks
postdomAssignment BlockMap ext blocks ret
m [Some (BlockID blocks)]
breakpointIds = (forall (x :: Ctx CrucibleType).
 Block ext blocks ret x -> Const [Some (BlockID blocks)] x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (Block ext blocks ret) x
   -> Assignment (Const [Some (BlockID blocks)]) 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 :: Ctx CrucibleType -> Type)
       (g :: Ctx CrucibleType -> Type).
(forall (x :: Ctx CrucibleType). f x -> g x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment f x -> Assignment g x
fmapFC Block ext blocks ret x -> Const [Some (BlockID blocks)] x
forall (x :: Ctx CrucibleType).
Block ext blocks ret x -> Const [Some (BlockID blocks)] x
go BlockMap ext blocks ret
m
  where pd :: Map (Some (BlockID blocks)) [Some (BlockID blocks)]
pd = BlockMap ext blocks ret
-> [Some (BlockID blocks)]
-> Map (Some (BlockID blocks)) [Some (BlockID blocks)]
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret
-> [Some (BlockID blocks)]
-> Map (Some (BlockID blocks)) [Some (BlockID blocks)]
postdomMap BlockMap ext blocks ret
m [Some (BlockID blocks)]
breakpointIds
        go :: Block ext blocks ret c -> Const [Some (BlockID blocks)] c
        go :: forall (x :: Ctx CrucibleType).
Block ext blocks ret x -> Const [Some (BlockID blocks)] x
go Block ext blocks ret c
b = [Some (BlockID blocks)] -> Const [Some (BlockID blocks)] c
forall {k} a (b :: k). a -> Const a b
Const ([Some (BlockID blocks)] -> Const [Some (BlockID blocks)] c)
-> [Some (BlockID blocks)] -> Const [Some (BlockID blocks)] c
forall a b. (a -> b) -> a -> b
$ [Some (BlockID blocks)]
-> Maybe [Some (BlockID blocks)] -> [Some (BlockID blocks)]
forall a. a -> Maybe a -> a
fromMaybe [] (Some (BlockID blocks)
-> Map (Some (BlockID blocks)) [Some (BlockID blocks)]
-> Maybe [Some (BlockID blocks)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (BlockID blocks c -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Block ext blocks ret c -> BlockID blocks c
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret c
b)) Map (Some (BlockID blocks)) [Some (BlockID blocks)]
pd)

-- | Compute posstdom information for CFG.
postdomInfo :: CFG ext b i r -> CFGPostdom b
postdomInfo :: forall ext (b :: Ctx (Ctx CrucibleType)) (i :: Ctx CrucibleType)
       (r :: CrucibleType).
CFG ext b i r -> CFGPostdom b
postdomInfo CFG ext b i r
g = BlockMap ext b r -> [Some (BlockID b)] -> CFGPostdom b
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret
-> [Some (BlockID blocks)] -> CFGPostdom blocks
postdomAssignment (CFG ext b i r -> BlockMap ext b r
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext b i r
g) []

breakpointPostdomInfo :: CFG ext b i r -> [BreakpointName] -> CFGPostdom b
breakpointPostdomInfo :: forall ext (b :: Ctx (Ctx CrucibleType)) (i :: Ctx CrucibleType)
       (r :: CrucibleType).
CFG ext b i r -> [BreakpointName] -> CFGPostdom b
breakpointPostdomInfo CFG ext b i r
g [BreakpointName]
breakpointNames = BlockMap ext b r -> [Some (BlockID b)] -> CFGPostdom b
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
BlockMap ext blocks ret
-> [Some (BlockID blocks)] -> CFGPostdom blocks
postdomAssignment (CFG ext b i r -> BlockMap ext b r
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext b i r
g) ([Some (BlockID b)] -> CFGPostdom b)
-> [Some (BlockID b)] -> CFGPostdom b
forall a b. (a -> b) -> a -> b
$
  (BreakpointName -> Maybe (Some (BlockID b)))
-> [BreakpointName] -> [Some (BlockID b)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\BreakpointName
nm -> BreakpointName
-> Bimap BreakpointName (Some (BlockID b))
-> Maybe (Some (BlockID b))
forall a b (m :: Type -> Type).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
Bimap.lookup BreakpointName
nm (CFG ext b i r -> Bimap BreakpointName (Some (BlockID b))
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Bimap BreakpointName (Some (BlockID blocks))
cfgBreakpoints CFG ext b i r
g)) [BreakpointName]
breakpointNames

blockEndsWithError :: Block ext blocks ret args -> Bool
blockEndsWithError :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (args :: Ctx CrucibleType).
Block ext blocks ret args -> Bool
blockEndsWithError Block ext blocks ret args
b =
  Block ext blocks ret args
-> (forall {ctx :: Ctx CrucibleType}.
    ProgramLoc -> TermStmt blocks ret ctx -> Bool)
-> Bool
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) r.
Block ext blocks ret args
-> (forall (ctx :: Ctx CrucibleType).
    ProgramLoc -> TermStmt blocks ret ctx -> r)
-> r
withBlockTermStmt Block ext blocks ret args
b ((forall {ctx :: Ctx CrucibleType}.
  ProgramLoc -> TermStmt blocks ret ctx -> Bool)
 -> Bool)
-> (forall {ctx :: Ctx CrucibleType}.
    ProgramLoc -> TermStmt blocks ret ctx -> Bool)
-> Bool
forall a b. (a -> b) -> a -> b
$ \ProgramLoc
_ TermStmt blocks ret ctx
ts ->
    case TermStmt blocks ret ctx
ts of
      ErrorStmt{} -> Bool
True
      TermStmt blocks ret ctx
_ -> Bool
False

addErrorIf :: Bool -> String -> State [String] ()
addErrorIf :: Bool -> String -> State [String] ()
addErrorIf Bool
True String
msg = ([String] -> [String]) -> State [String] ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (([String] -> [String]) -> State [String] ())
-> ([String] -> [String]) -> State [String] ()
forall a b. (a -> b) -> a -> b
$ (String
msgString -> [String] -> [String]
forall a. a -> [a] -> [a]
:)
addErrorIf Bool
False String
_ = () -> State [String] ()
forall a. a -> StateT [String] Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

validateTarget :: CFG ext blocks init ret
               -> CFGPostdom blocks
               -> String
               -- ^ Identifier for error.
               -> [Some (BlockID blocks)]
               -- ^ Postdoms for source block.
               -> Some (BlockID blocks)
               -- ^ Target
               -> State [String] ()
validateTarget :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
validateTarget CFG ext blocks init ret
_ CFGPostdom blocks
pdInfo String
src (Some BlockID blocks x
pd:[Some (BlockID blocks)]
src_postdoms) (Some BlockID blocks x
tgt)
  | Maybe (x :~: x) -> Bool
forall a. Maybe a -> Bool
isJust (BlockID blocks x -> BlockID blocks x -> Maybe (x :~: x)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
BlockID blocks a -> BlockID blocks b -> Maybe (a :~: b)
testEquality BlockID blocks x
pd BlockID blocks x
tgt) =
      Bool -> String -> State [String] ()
addErrorIf ([Some (BlockID blocks)]
src_postdoms [Some (BlockID blocks)] -> [Some (BlockID blocks)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Some (BlockID blocks)]
tgt_postdoms) (String -> State [String] ()) -> String -> State [String] ()
forall a b. (a -> b) -> a -> b
$
        String
"Unexpected postdominators from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
src String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BlockID blocks x -> String
forall a. Show a => a -> String
show BlockID blocks x
tgt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
  where Const [Some (BlockID blocks)]
tgt_postdoms = CFGPostdom blocks
pdInfo CFGPostdom blocks
-> Index blocks x -> Const [Some (BlockID blocks)] x
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! BlockID blocks x -> Index blocks x
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID blocks x
tgt
validateTarget CFG ext blocks init ret
g CFGPostdom blocks
pdInfo String
src [Some (BlockID blocks)]
src_postdoms (Some BlockID blocks x
tgt)
  | Block ext blocks ret x -> Bool
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (args :: Ctx CrucibleType).
Block ext blocks ret args -> Bool
blockEndsWithError Block ext blocks ret x
tgt_block =
    () -> State [String] ()
forall a. a -> StateT [String] Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
  | Bool
otherwise = do
      let tgt_len :: Node
tgt_len = [Some (BlockID blocks)] -> Node
forall a. [a] -> Node
forall (t :: Type -> Type) a. Foldable t => t a -> Node
length [Some (BlockID blocks)]
tgt_postdoms
      let src_len :: Node
src_len = [Some (BlockID blocks)] -> Node
forall a. [a] -> Node
forall (t :: Type -> Type) a. Foldable t => t a -> Node
length [Some (BlockID blocks)]
src_postdoms
      Bool -> String -> State [String] ()
addErrorIf (Node
tgt_len Node -> Node -> Bool
forall a. Ord a => a -> a -> Bool
< Node
src_len) (String -> State [String] ()) -> String -> State [String] ()
forall a b. (a -> b) -> a -> b
$
        String
"Unexpected postdominators from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
src String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BlockID blocks x -> String
forall a. Show a => a -> String
show BlockID blocks x
tgt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
      let tgt_prefix :: [Some (BlockID blocks)]
tgt_prefix = Node -> [Some (BlockID blocks)] -> [Some (BlockID blocks)]
forall a. Node -> [a] -> [a]
drop (Node
tgt_len Node -> Node -> Node
forall a. Num a => a -> a -> a
- Node
src_len) [Some (BlockID blocks)]
tgt_postdoms
      Bool -> String -> State [String] ()
addErrorIf ([Some (BlockID blocks)]
src_postdoms [Some (BlockID blocks)] -> [Some (BlockID blocks)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Some (BlockID blocks)]
tgt_prefix) (String -> State [String] ()) -> String -> State [String] ()
forall a b. (a -> b) -> a -> b
$
        String
"Unexpected postdominators from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
src String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BlockID blocks x -> String
forall a. Show a => a -> String
show BlockID blocks x
tgt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
  where tgt_block :: Block ext blocks ret x
tgt_block = 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
tgt (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)
        Const [Some (BlockID blocks)]
tgt_postdoms = CFGPostdom blocks
pdInfo CFGPostdom blocks
-> Index blocks x -> Const [Some (BlockID blocks)] x
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! BlockID blocks x -> Index blocks x
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID blocks x
tgt

validatePostdom :: CFG ext blocks init ret
                -> CFGPostdom blocks
                -> [String]
validatePostdom :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> CFGPostdom blocks -> [String]
validatePostdom CFG ext blocks init ret
g CFGPostdom blocks
pdInfo = (State [String] () -> [String] -> [String])
-> [String] -> State [String] () -> [String]
forall a b c. (a -> b -> c) -> b -> a -> c
flip State [String] () -> [String] -> [String]
forall s a. State s a -> s -> s
execState [] (State [String] () -> [String]) -> State [String] () -> [String]
forall a b. (a -> b) -> a -> b
$ do
  Assignment (Block ext blocks ret) blocks
-> (forall {x :: Ctx CrucibleType}.
    Block ext blocks ret x -> State [String] ())
-> State [String] ()
forall {k} {l} (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
       (f :: k -> Type) (c :: l) a.
(FoldableFC t, Applicative m) =>
t f c -> (forall (x :: k). f x -> m a) -> m ()
forFC_ (CFG ext blocks init ret -> Assignment (Block ext blocks ret) blocks
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) ((forall {x :: Ctx CrucibleType}.
  Block ext blocks ret x -> State [String] ())
 -> State [String] ())
-> (forall {x :: Ctx CrucibleType}.
    Block ext blocks ret x -> State [String] ())
-> State [String] ()
forall a b. (a -> b) -> a -> b
$ \Block ext blocks ret x
b -> do
    let Const [Some (BlockID blocks)]
b_pd = CFGPostdom blocks
pdInfo CFGPostdom blocks
-> Index blocks x -> Const [Some (BlockID blocks)] x
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! BlockID blocks x -> Index blocks x
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex (Block ext blocks ret x -> BlockID blocks x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret x
b)
    let loc :: String
loc = FnHandle init ret -> String
forall a. Show a => a -> String
show (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) String -> String -> String
forall a. [a] -> [a] -> [a]
++ BlockID blocks x -> String
forall a. Show a => a -> String
show (Block ext blocks ret x -> BlockID blocks x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret x
b)
    (Some (BlockID blocks) -> State [String] ())
-> [Some (BlockID blocks)] -> State [String] ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
validateTarget CFG ext blocks init ret
g CFGPostdom blocks
pdInfo String
loc [Some (BlockID blocks)]
b_pd) (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)

    Block ext blocks ret x
-> (forall {ctx :: Ctx CrucibleType}.
    ProgramLoc -> TermStmt blocks ret ctx -> State [String] ())
-> State [String] ()
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) r.
Block ext blocks ret args
-> (forall (ctx :: Ctx CrucibleType).
    ProgramLoc -> TermStmt blocks ret ctx -> r)
-> r
withBlockTermStmt Block ext blocks ret x
b ((forall {ctx :: Ctx CrucibleType}.
  ProgramLoc -> TermStmt blocks ret ctx -> State [String] ())
 -> State [String] ())
-> (forall {ctx :: Ctx CrucibleType}.
    ProgramLoc -> TermStmt blocks ret ctx -> State [String] ())
-> State [String] ()
forall a b. (a -> b) -> a -> b
$ \ProgramLoc
_ TermStmt blocks ret ctx
ts -> do
      case TermStmt blocks ret ctx
ts of
        Jump JumpTarget blocks ctx
tgt -> do
          CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
validateTarget CFG ext blocks init ret
g CFGPostdom blocks
pdInfo String
loc [Some (BlockID blocks)]
b_pd (JumpTarget blocks ctx -> Some (BlockID blocks)
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
JumpTarget blocks ctx -> Some (BlockID blocks)
jumpTargetID JumpTarget blocks ctx
tgt)
        Br Reg ctx BoolType
_ JumpTarget blocks ctx
tgt1 JumpTarget blocks ctx
tgt2  -> do
          CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
validateTarget CFG ext blocks init ret
g CFGPostdom blocks
pdInfo String
loc [Some (BlockID blocks)]
b_pd (JumpTarget blocks ctx -> Some (BlockID blocks)
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
JumpTarget blocks ctx -> Some (BlockID blocks)
jumpTargetID JumpTarget blocks ctx
tgt1)
          CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
validateTarget CFG ext blocks init ret
g CFGPostdom blocks
pdInfo String
loc [Some (BlockID blocks)]
b_pd (JumpTarget blocks ctx -> Some (BlockID blocks)
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
JumpTarget blocks ctx -> Some (BlockID blocks)
jumpTargetID JumpTarget blocks ctx
tgt2)
        MaybeBranch TypeRepr tp
_ Reg ctx (MaybeType tp)
_ SwitchTarget blocks ctx tp
x JumpTarget blocks ctx
y -> do
          CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
validateTarget CFG ext blocks init ret
g CFGPostdom blocks
pdInfo String
loc [Some (BlockID blocks)]
b_pd (SwitchTarget blocks ctx tp -> Some (BlockID blocks)
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
SwitchTarget blocks ctx tp -> Some (BlockID blocks)
switchTargetID SwitchTarget blocks ctx tp
x)
          CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
validateTarget CFG ext blocks init ret
g CFGPostdom blocks
pdInfo String
loc [Some (BlockID blocks)]
b_pd (JumpTarget blocks ctx -> Some (BlockID blocks)
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
JumpTarget blocks ctx -> Some (BlockID blocks)
jumpTargetID   JumpTarget blocks ctx
y)
        VariantElim CtxRepr varctx
_ Reg ctx (VariantType varctx)
_ Assignment (SwitchTarget blocks ctx) varctx
s -> do
          (forall (x :: CrucibleType).
 SwitchTarget blocks ctx x -> State [String] ())
-> forall (x :: Ctx CrucibleType).
   Assignment (SwitchTarget blocks ctx) x -> State [String] ()
forall {k} {l} (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
       (f :: k -> Type) a.
(FoldableFC t, Applicative m) =>
(forall (x :: k). f x -> m a) -> forall (x :: l). t f x -> m ()
traverseFC_ (CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> CFGPostdom blocks
-> String
-> [Some (BlockID blocks)]
-> Some (BlockID blocks)
-> State [String] ()
validateTarget CFG ext blocks init ret
g CFGPostdom blocks
pdInfo String
loc [Some (BlockID blocks)]
b_pd (Some (BlockID blocks) -> State [String] ())
-> (SwitchTarget blocks ctx x -> Some (BlockID blocks))
-> SwitchTarget blocks ctx x
-> State [String] ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SwitchTarget blocks ctx x -> Some (BlockID blocks)
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
SwitchTarget blocks ctx tp -> Some (BlockID blocks)
switchTargetID) Assignment (SwitchTarget blocks ctx) varctx
s
        Return{} -> do
          Bool -> String -> State [String] ()
addErrorIf (Bool -> Bool
not ([Some (BlockID blocks)] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Some (BlockID blocks)]
b_pd)) (String -> State [String] ()) -> String -> State [String] ()
forall a b. (a -> b) -> a -> b
$
            String
"Expected empty postdom in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
loc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
        TailCall{} -> do
          Bool -> String -> State [String] ()
addErrorIf (Bool -> Bool
not ([Some (BlockID blocks)] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Some (BlockID blocks)]
b_pd)) (String -> State [String] ()) -> String -> State [String] ()
forall a b. (a -> b) -> a -> b
$
            String
"Expected empty postdom in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
loc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
        ErrorStmt{} -> do
          Bool -> String -> State [String] ()
addErrorIf (Bool -> Bool
not ([Some (BlockID blocks)] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Some (BlockID blocks)]
b_pd)) (String -> State [String] ()) -> String -> State [String] ()
forall a b. (a -> b) -> a -> b
$
            String
"Expected empty postdom in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
loc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."