{-# 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
(
DFSEdgeType(..)
, DFSNodeFunc
, DFSEdgeFunc
, dfs
, run_dfs
, 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
| ForwardOrCrossEdge
| BackEdge
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)
type DFSNodeFunc ext blocks a = forall ret ctx. Block ext blocks ret ctx -> a -> a
type DFSEdgeFunc blocks a = DFSEdgeType -> SomeBlockID blocks -> SomeBlockID blocks -> a -> a
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
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_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
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
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 :: 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)
run_dfs :: forall ext blocks a ret cxt
. 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 :: 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
(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)
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 =
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
visit_edge :: Set (SomeBlockID blocks)
-> SomeBlockID blocks
-> SomeBlockID blocks
-> (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 =
(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 =
(DFSEdgeFunc blocks a
edge DFSEdgeType
ForwardOrCrossEdge SomeBlockID blocks
n SomeBlockID blocks
m a
x, Set (SomeBlockID blocks)
black)
| Bool
otherwise =
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)