------------------------------------------------------------------------
-- |
-- Module      : Lang.Crucible.Analysis.DFS
-- Description : Depth-first search algorithm on Crucible CFGs
-- Copyright   : (c) Galois, Inc 2015
-- License     : BSD3
-- Maintainer  : Rob Dockins <rdockins@galois.com>
-- Stability   : provisional
--
-- This module defines a generic algorithm for depth-first search
-- traversal of a control flow graph.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Lang.Crucible.Analysis.DFS
( -- * Basic DFS types and algorithms
  DFSEdgeType(..)
, DFSNodeFunc
, DFSEdgeFunc
, dfs
, run_dfs

  -- * Some specific DFS traversals
, dfs_backedge_targets
, dfs_backedges
, dfs_list
, dfs_preorder
, dfs_postorder
) where

import Prelude hiding (foldr)
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Foldable

import Lang.Crucible.Types
import Lang.Crucible.CFG.Core

type SomeBlockID blocks = Some (BlockID blocks)

data DFSEdgeType
    = TreeEdge              -- ^ This edge is on the spanning forrest computed by this DFS
    | ForwardOrCrossEdge    -- ^ This edge is either a forward (to a direct decendent in the spanning tree)
                            --   or a cross edge (to a cousin node)
    | BackEdge              -- ^ This edge is a back edge (to an ancestor in the spanning tree).  Every cycle in
                            --   the graph must traverse at least one back edge.
  deriving (DFSEdgeType -> DFSEdgeType -> Bool
(DFSEdgeType -> DFSEdgeType -> Bool)
-> (DFSEdgeType -> DFSEdgeType -> Bool) -> Eq DFSEdgeType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DFSEdgeType -> DFSEdgeType -> Bool
== :: DFSEdgeType -> DFSEdgeType -> Bool
$c/= :: DFSEdgeType -> DFSEdgeType -> Bool
/= :: DFSEdgeType -> DFSEdgeType -> Bool
Eq, Eq DFSEdgeType
Eq DFSEdgeType =>
(DFSEdgeType -> DFSEdgeType -> Ordering)
-> (DFSEdgeType -> DFSEdgeType -> Bool)
-> (DFSEdgeType -> DFSEdgeType -> Bool)
-> (DFSEdgeType -> DFSEdgeType -> Bool)
-> (DFSEdgeType -> DFSEdgeType -> Bool)
-> (DFSEdgeType -> DFSEdgeType -> DFSEdgeType)
-> (DFSEdgeType -> DFSEdgeType -> DFSEdgeType)
-> Ord DFSEdgeType
DFSEdgeType -> DFSEdgeType -> Bool
DFSEdgeType -> DFSEdgeType -> Ordering
DFSEdgeType -> DFSEdgeType -> DFSEdgeType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DFSEdgeType -> DFSEdgeType -> Ordering
compare :: DFSEdgeType -> DFSEdgeType -> Ordering
$c< :: DFSEdgeType -> DFSEdgeType -> Bool
< :: DFSEdgeType -> DFSEdgeType -> Bool
$c<= :: DFSEdgeType -> DFSEdgeType -> Bool
<= :: DFSEdgeType -> DFSEdgeType -> Bool
$c> :: DFSEdgeType -> DFSEdgeType -> Bool
> :: DFSEdgeType -> DFSEdgeType -> Bool
$c>= :: DFSEdgeType -> DFSEdgeType -> Bool
>= :: DFSEdgeType -> DFSEdgeType -> Bool
$cmax :: DFSEdgeType -> DFSEdgeType -> DFSEdgeType
max :: DFSEdgeType -> DFSEdgeType -> DFSEdgeType
$cmin :: DFSEdgeType -> DFSEdgeType -> DFSEdgeType
min :: DFSEdgeType -> DFSEdgeType -> DFSEdgeType
Ord, Int -> DFSEdgeType -> ShowS
[DFSEdgeType] -> ShowS
DFSEdgeType -> String
(Int -> DFSEdgeType -> ShowS)
-> (DFSEdgeType -> String)
-> ([DFSEdgeType] -> ShowS)
-> Show DFSEdgeType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DFSEdgeType -> ShowS
showsPrec :: Int -> DFSEdgeType -> ShowS
$cshow :: DFSEdgeType -> String
show :: DFSEdgeType -> String
$cshowList :: [DFSEdgeType] -> ShowS
showList :: [DFSEdgeType] -> ShowS
Show)

-- | Function to update the traversal state when we have finished visiting
--   all of a nodes's reachable children.
type DFSNodeFunc ext blocks a = forall ret ctx. Block ext blocks ret ctx -> a -> a

-- | Function to update the traversal state when traversing an edge.
type DFSEdgeFunc blocks a = DFSEdgeType -> SomeBlockID blocks -> SomeBlockID blocks -> a -> a


-- | Use depth-first search to calculate a set of all the block IDs that
--   are the target of some back-edge, i.e., a set of nodes through which
--   every loop passes.
dfs_backedge_targets :: CFG ext blocks init ret -> Set (SomeBlockID blocks)
dfs_backedge_targets :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> Set (SomeBlockID blocks)
dfs_backedge_targets =
  DFSNodeFunc ext blocks (Set (SomeBlockID blocks))
-> DFSEdgeFunc blocks (Set (SomeBlockID blocks))
-> Set (SomeBlockID blocks)
-> CFG ext blocks init ret
-> Set (SomeBlockID blocks)
forall ext (blocks :: Ctx (Ctx CrucibleType)) a
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
DFSNodeFunc ext blocks a
-> DFSEdgeFunc blocks a -> a -> CFG ext blocks init ret -> a
dfs (\Block ext blocks ret ctx
_ Set (SomeBlockID blocks)
x -> Set (SomeBlockID blocks)
x)
      (\DFSEdgeType
et SomeBlockID blocks
_ SomeBlockID blocks
m Set (SomeBlockID blocks)
x ->
        case DFSEdgeType
et of
          DFSEdgeType
BackEdge -> SomeBlockID blocks
-> Set (SomeBlockID blocks) -> Set (SomeBlockID blocks)
forall a. Ord a => a -> Set a -> Set a
Set.insert SomeBlockID blocks
m Set (SomeBlockID blocks)
x
          DFSEdgeType
_ -> Set (SomeBlockID blocks)
x)
      Set (SomeBlockID blocks)
forall a. Set a
Set.empty


-- | Compute a sequence of all the back edges found in a depth-first search of the given CFG.
dfs_backedges :: CFG ext blocks init ret -> Seq (SomeBlockID blocks, SomeBlockID blocks)
dfs_backedges :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Seq (SomeBlockID blocks, SomeBlockID blocks)
dfs_backedges =
  DFSNodeFunc
  ext blocks (Seq (SomeBlockID blocks, SomeBlockID blocks))
-> DFSEdgeFunc
     blocks (Seq (SomeBlockID blocks, SomeBlockID blocks))
-> Seq (SomeBlockID blocks, SomeBlockID blocks)
-> CFG ext blocks init ret
-> Seq (SomeBlockID blocks, SomeBlockID blocks)
forall ext (blocks :: Ctx (Ctx CrucibleType)) a
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
DFSNodeFunc ext blocks a
-> DFSEdgeFunc blocks a -> a -> CFG ext blocks init ret -> a
dfs (\Block ext blocks ret ctx
_ Seq (SomeBlockID blocks, SomeBlockID blocks)
x -> Seq (SomeBlockID blocks, SomeBlockID blocks)
x)
      (\DFSEdgeType
et SomeBlockID blocks
n SomeBlockID blocks
m Seq (SomeBlockID blocks, SomeBlockID blocks)
x ->
          case DFSEdgeType
et of
            DFSEdgeType
BackEdge -> Seq (SomeBlockID blocks, SomeBlockID blocks)
x Seq (SomeBlockID blocks, SomeBlockID blocks)
-> (SomeBlockID blocks, SomeBlockID blocks)
-> Seq (SomeBlockID blocks, SomeBlockID blocks)
forall a. Seq a -> a -> Seq a
Seq.|> (SomeBlockID blocks
n,SomeBlockID blocks
m)
            DFSEdgeType
_ -> Seq (SomeBlockID blocks, SomeBlockID blocks)
x)
      Seq (SomeBlockID blocks, SomeBlockID blocks)
forall a. Seq a
Seq.empty

{-
dfs_backedges_string :: CFG blocks init ret -> String
dfs_backedges_string = unlines . map showEdge . toList . dfs_backedges
  where showEdge :: (SomeBlockID blocks, SomeBlockID blocks) -> String
        showEdge (Some n, Some m) = show (n,m)
-}

-- | Compute a sequence of all the edges visited in a depth-first search of the given CFG.
dfs_list :: CFG ext blocks init ret -> Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
dfs_list :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
dfs_list =
  DFSNodeFunc
  ext
  blocks
  (Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks))
-> DFSEdgeFunc
     blocks (Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks))
-> Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
-> CFG ext blocks init ret
-> Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
forall ext (blocks :: Ctx (Ctx CrucibleType)) a
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
DFSNodeFunc ext blocks a
-> DFSEdgeFunc blocks a -> a -> CFG ext blocks init ret -> a
dfs (\Block ext blocks ret ctx
_ Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
x -> Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
x)
      (\DFSEdgeType
et SomeBlockID blocks
n SomeBlockID blocks
m Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
x -> Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
x Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
-> (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
-> Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
forall a. Seq a -> a -> Seq a
Seq.|> (DFSEdgeType
et,SomeBlockID blocks
n,SomeBlockID blocks
m))
      Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
forall a. Seq a
Seq.empty

-- | Compute a postorder traversal of all the reachable nodes in the CFG
dfs_postorder :: CFG ext blocks init ret -> Seq (SomeBlockID blocks)
dfs_postorder :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> Seq (SomeBlockID blocks)
dfs_postorder =
  DFSNodeFunc ext blocks (Seq (SomeBlockID blocks))
-> DFSEdgeFunc blocks (Seq (SomeBlockID blocks))
-> Seq (SomeBlockID blocks)
-> CFG ext blocks init ret
-> Seq (SomeBlockID blocks)
forall ext (blocks :: Ctx (Ctx CrucibleType)) a
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
DFSNodeFunc ext blocks a
-> DFSEdgeFunc blocks a -> a -> CFG ext blocks init ret -> a
dfs (\Block ext blocks ret ctx
blk Seq (SomeBlockID blocks)
x -> Seq (SomeBlockID blocks)
x Seq (SomeBlockID blocks)
-> SomeBlockID blocks -> Seq (SomeBlockID blocks)
forall a. Seq a -> a -> Seq a
Seq.|> (BlockID blocks ctx -> SomeBlockID blocks
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (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
blk)))
      (\DFSEdgeType
_ SomeBlockID blocks
_ SomeBlockID blocks
_ Seq (SomeBlockID blocks)
x -> Seq (SomeBlockID blocks)
x)
      Seq (SomeBlockID blocks)
forall a. Seq a
Seq.empty

-- | Compute a preorder traversal of all the reachable nodes in the CFG
dfs_preorder :: CFG ext blocks init ret -> Seq (SomeBlockID blocks)
dfs_preorder :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> Seq (SomeBlockID blocks)
dfs_preorder =
  DFSNodeFunc ext blocks (Seq (SomeBlockID blocks))
-> DFSEdgeFunc blocks (Seq (SomeBlockID blocks))
-> Seq (SomeBlockID blocks)
-> CFG ext blocks init ret
-> Seq (SomeBlockID blocks)
forall ext (blocks :: Ctx (Ctx CrucibleType)) a
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
DFSNodeFunc ext blocks a
-> DFSEdgeFunc blocks a -> a -> CFG ext blocks init ret -> a
dfs (\Block ext blocks ret ctx
_ Seq (SomeBlockID blocks)
x -> Seq (SomeBlockID blocks)
x)
      (\DFSEdgeType
et SomeBlockID blocks
_n SomeBlockID blocks
m Seq (SomeBlockID blocks)
x ->
          case DFSEdgeType
et of
            DFSEdgeType
TreeEdge -> Seq (SomeBlockID blocks)
x Seq (SomeBlockID blocks)
-> SomeBlockID blocks -> Seq (SomeBlockID blocks)
forall a. Seq a -> a -> Seq a
Seq.|> SomeBlockID blocks
m
            DFSEdgeType
_ -> Seq (SomeBlockID blocks)
x)
      Seq (SomeBlockID blocks)
forall a. Seq a
Seq.empty

{-
dfs_list_string :: CFG blocks init ret -> String
dfs_list_string = unlines . map showEdge . toList . dfs_list
  where showEdge :: (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks) -> String
        showEdge (et, Some n, Some m) = show (et,n,m)
-}

-- | A depth-first search algorithm on a block map.
--
--   The DFSNodeFunc and DFSEdgeFunc define what we are computing. The DFSEdgeFunc is called
--   on each edge.  The edges are classified according to standard depth-first search
--   terminology.  A tree edge is an edge in the discovered spanning tree.  A back edge
--   goes from a child to an ancestor in the spanning tree.  A ForwardOrCross edge travels
--   either from an ancestor to a child (but not a tree edge), or between two unrelated nodes.
--   The forward/cross case can be distinguished, if desired, by tracking the order in which
--   nodes are found.  A forward edge goes from a low numbered node to a high numbered node,
--   but a cross edge goes from a high node to a low node.
--
--   The DFSNodeFunc is called on each block _after_ the DFS has processed all its fresh reachable
--   children; that is, as the search is leaving the given node.  In particular, using the DFSNodeFunc
--   to put the blocks in a queue will give a postorder traversal of the discovered nodes.
--   Contrarywise, using the DFSEdgeFunc to place blocks in a queue when they occur in a TreeEdge
--   will give a preorder traversal of the discovered nodes.
--
--   We track the lifecycle of nodes by using two sets; an ancestor set and a black set.
--   Nodes are added to the ancestor set as we pass down into recursive calls, and changes
--   to this set are discarded upon return.  The black set records black nodes (those whose
--   visit is completed), and changes are threaded through the search.
--
--   In the standard parlance, a node is white if it has not yet been discovered; it is
--   in neither the ancestor nor black set.  A node is grey if it has been discovered, but
--   not yet completed; such a node is in the ancestor set, but not the black set.  A node
--   is black if its visit has been completed; it is in the black set and not in the ancestor
--   set.  INVARIANT: at all times, the ancestor set and black set are disjoint.
--   After a DFS is completed, all visited nodes will be in the black set; any nodes not in the
--   black set are unreachable from the initial node.

dfs :: DFSNodeFunc ext blocks a
    -> DFSEdgeFunc blocks a
    -> a
    -> CFG ext blocks init ret
    -> a
dfs :: forall ext (blocks :: Ctx (Ctx CrucibleType)) a
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
DFSNodeFunc ext blocks a
-> DFSEdgeFunc blocks a -> a -> CFG ext blocks init ret -> a
dfs DFSNodeFunc ext blocks a
visit DFSEdgeFunc blocks a
edge a
x CFG ext blocks init ret
cfg =
   (a, Set (SomeBlockID blocks)) -> a
forall a b. (a, b) -> a
fst ((a, Set (SomeBlockID blocks)) -> a)
-> (a, Set (SomeBlockID blocks)) -> a
forall a b. (a -> b) -> a -> b
$ DFSNodeFunc ext blocks a
-> DFSEdgeFunc blocks a
-> BlockMap ext blocks ret
-> Set (SomeBlockID blocks)
-> BlockID blocks init
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
forall ext (blocks :: Ctx (Ctx CrucibleType)) a
       (ret :: CrucibleType) (cxt :: Ctx CrucibleType).
DFSNodeFunc ext blocks a
-> DFSEdgeFunc blocks a
-> BlockMap ext blocks ret
-> Set (SomeBlockID blocks)
-> BlockID blocks cxt
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
run_dfs
             Block ext blocks ret ctx -> a -> a
DFSNodeFunc ext blocks a
visit
             DFSEdgeFunc blocks a
edge
             (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
cfg)
             Set (SomeBlockID blocks)
forall a. Set a
Set.empty
             (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
cfg)
             (a
x, Set (SomeBlockID blocks)
forall a. Set a
Set.empty)


-- | Low-level depth-first search function.  This exposes more of the moving parts
--   than `dfs` for algorithms that need more access to the guts.
run_dfs :: forall ext blocks a ret cxt
         . DFSNodeFunc ext blocks a      -- ^ action to take after a visit is finished
        -> DFSEdgeFunc blocks a      -- ^ action to take for each edge
        -> BlockMap ext blocks ret       -- ^ CFG blocks to search
        -> Set (SomeBlockID blocks)  -- ^ ancestor nodes
        -> BlockID blocks cxt        -- ^ a white node to visit
        -> (a, Set (SomeBlockID blocks)) -- ^ Partially-computed value and initial black set
        -> (a, Set (SomeBlockID blocks)) -- ^ Computed value and modified black set
run_dfs :: forall ext (blocks :: Ctx (Ctx CrucibleType)) a
       (ret :: CrucibleType) (cxt :: Ctx CrucibleType).
DFSNodeFunc ext blocks a
-> DFSEdgeFunc blocks a
-> BlockMap ext blocks ret
-> Set (SomeBlockID blocks)
-> BlockID blocks cxt
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
run_dfs DFSNodeFunc ext blocks a
visit DFSEdgeFunc blocks a
edge BlockMap ext blocks ret
bm = Set (SomeBlockID blocks)
-> BlockID blocks cxt
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
forall (cxt' :: Ctx CrucibleType).
Set (SomeBlockID blocks)
-> BlockID blocks cxt'
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
visit_id

 where visit_id :: forall cxt'
                 . Set (SomeBlockID blocks)
                -> BlockID blocks cxt'
                -> (a, Set (SomeBlockID blocks))
                -> (a, Set (SomeBlockID blocks))
       visit_id :: forall (cxt' :: Ctx CrucibleType).
Set (SomeBlockID blocks)
-> BlockID blocks cxt'
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
visit_id Set (SomeBlockID blocks)
an BlockID blocks cxt'
i (a
x,Set (SomeBlockID blocks)
black) =
          let block :: Block ext blocks ret cxt'
block = BlockID blocks cxt'
-> BlockMap ext blocks ret -> Block ext blocks ret cxt'
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 cxt'
i BlockMap ext blocks ret
bm
              -- Insert index 'i' into the ancestor set before the recursive call
              (a
x',Set (SomeBlockID blocks)
black') = Set (SomeBlockID blocks)
-> Block ext blocks ret cxt'
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
forall (ctx :: Ctx CrucibleType).
Set (SomeBlockID blocks)
-> Block ext blocks ret ctx
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
visit_block (SomeBlockID blocks
-> Set (SomeBlockID blocks) -> Set (SomeBlockID blocks)
forall a. Ord a => a -> Set a -> Set a
Set.insert (BlockID blocks cxt' -> SomeBlockID blocks
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks cxt'
i) Set (SomeBlockID blocks)
an) Block ext blocks ret cxt'
block (a
x, Set (SomeBlockID blocks)
black)

              -- After the recursive call has completed, add 'i' to the black set
              -- and call the node visit function
           in (Block ext blocks ret cxt' -> a -> a
DFSNodeFunc ext blocks a
visit Block ext blocks ret cxt'
block a
x', SomeBlockID blocks
-> Set (SomeBlockID blocks) -> Set (SomeBlockID blocks)
forall a. Ord a => a -> Set a -> Set a
Set.insert (BlockID blocks cxt' -> SomeBlockID blocks
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks cxt'
i) Set (SomeBlockID blocks)
black')

       visit_block :: Set (SomeBlockID blocks)
                   -> Block ext blocks ret ctx
                   -> (a, Set (SomeBlockID blocks))
                   -> (a, Set (SomeBlockID blocks))
       visit_block :: forall (ctx :: Ctx CrucibleType).
Set (SomeBlockID blocks)
-> Block ext blocks ret ctx
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
visit_block Set (SomeBlockID blocks)
an Block ext blocks ret ctx
block =
           -- Get a list of all the next block ids we might jump to next, and visit them one by one,
           -- composting together their effects on the partial computation and black set.
           Block ext blocks ret ctx
-> (forall {ctx :: Ctx CrucibleType}.
    ProgramLoc
    -> TermStmt blocks ret ctx
    -> (a, Set (SomeBlockID blocks))
    -> (a, Set (SomeBlockID blocks)))
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID 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
block ((forall {ctx :: Ctx CrucibleType}.
  ProgramLoc
  -> TermStmt blocks ret ctx
  -> (a, Set (SomeBlockID blocks))
  -> (a, Set (SomeBlockID blocks)))
 -> (a, Set (SomeBlockID blocks)) -> (a, Set (SomeBlockID blocks)))
-> (forall {ctx :: Ctx CrucibleType}.
    ProgramLoc
    -> TermStmt blocks ret ctx
    -> (a, Set (SomeBlockID blocks))
    -> (a, Set (SomeBlockID blocks)))
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
forall a b. (a -> b) -> a -> b
$ \ProgramLoc
_loc TermStmt blocks ret ctx
t ->
              (SomeBlockID blocks
 -> ((a, Set (SomeBlockID blocks)) -> (a, Set (SomeBlockID blocks)))
 -> (a, Set (SomeBlockID blocks))
 -> (a, Set (SomeBlockID blocks)))
-> ((a, Set (SomeBlockID blocks)) -> (a, Set (SomeBlockID blocks)))
-> [SomeBlockID blocks]
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\SomeBlockID blocks
m (a, Set (SomeBlockID blocks)) -> (a, Set (SomeBlockID blocks))
f -> (a, Set (SomeBlockID blocks)) -> (a, Set (SomeBlockID blocks))
f ((a, Set (SomeBlockID blocks)) -> (a, Set (SomeBlockID blocks)))
-> ((a, Set (SomeBlockID blocks)) -> (a, Set (SomeBlockID blocks)))
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (SomeBlockID blocks)
-> SomeBlockID blocks
-> SomeBlockID blocks
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
visit_edge Set (SomeBlockID blocks)
an (BlockID blocks ctx -> SomeBlockID blocks
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (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
block)) SomeBlockID blocks
m) (a, Set (SomeBlockID blocks)) -> (a, Set (SomeBlockID blocks))
forall a. a -> a
id
                 ([SomeBlockID blocks]
 -> (a, Set (SomeBlockID blocks)) -> (a, Set (SomeBlockID blocks)))
-> [SomeBlockID blocks]
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
forall a b. (a -> b) -> a -> b
$ [SomeBlockID blocks]
-> Maybe [SomeBlockID blocks] -> [SomeBlockID blocks]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [SomeBlockID blocks] -> [SomeBlockID blocks])
-> Maybe [SomeBlockID blocks] -> [SomeBlockID blocks]
forall a b. (a -> b) -> a -> b
$ TermStmt blocks ret ctx -> Maybe [SomeBlockID blocks]
forall (b :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TermStmt b ret ctx -> Maybe [Some (BlockID b)]
termStmtNextBlocks TermStmt blocks ret ctx
t

       -- Given source and target block ids, examine the ancestor and black sets
       -- to discover if the node we are about to visit is a white, grey or black node
       -- and classify the edge accordingly.  Recursively visit the target node if it is white.
       visit_edge :: Set (SomeBlockID blocks) -- ^ ancestor set
                  -> SomeBlockID blocks       -- ^ source block id
                  -> SomeBlockID blocks       -- ^ target block id
                  -> (a, Set (SomeBlockID blocks))
                  -> (a, Set (SomeBlockID blocks))
       visit_edge :: Set (SomeBlockID blocks)
-> SomeBlockID blocks
-> SomeBlockID blocks
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
visit_edge Set (SomeBlockID blocks)
an SomeBlockID blocks
n m :: SomeBlockID blocks
m@(Some BlockID blocks x
m') (a
x, Set (SomeBlockID blocks)
black)
           | SomeBlockID blocks -> Set (SomeBlockID blocks) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SomeBlockID blocks
m Set (SomeBlockID blocks)
an =    -- grey node, back edge
                (DFSEdgeFunc blocks a
edge DFSEdgeType
BackEdge SomeBlockID blocks
n SomeBlockID blocks
m a
x, Set (SomeBlockID blocks)
black)

           | SomeBlockID blocks -> Set (SomeBlockID blocks) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SomeBlockID blocks
m Set (SomeBlockID blocks)
black = -- black node, forward/cross edge
                (DFSEdgeFunc blocks a
edge DFSEdgeType
ForwardOrCrossEdge SomeBlockID blocks
n SomeBlockID blocks
m a
x, Set (SomeBlockID blocks)
black)

           | Bool
otherwise =          -- white node, tree edge; recusively visit
                Set (SomeBlockID blocks)
-> BlockID blocks x
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
forall (cxt' :: Ctx CrucibleType).
Set (SomeBlockID blocks)
-> BlockID blocks cxt'
-> (a, Set (SomeBlockID blocks))
-> (a, Set (SomeBlockID blocks))
visit_id Set (SomeBlockID blocks)
an BlockID blocks x
m' (DFSEdgeFunc blocks a
edge DFSEdgeType
TreeEdge SomeBlockID blocks
n SomeBlockID blocks
m a
x, Set (SomeBlockID blocks)
black)