-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Analysis.Fixpoint.Components
-- Description      : Compute weak topological ordering of CFG
-- Copyright        : (c) Galois, Inc 2015
-- License          : BSD3
-- Maintainer       : Tristan Ravitch <tristan@galois.com>
-- Stability        : provisional
--
-- Compute a weak topological ordering over a control flow graph using
-- Bourdoncle's algorithm (See Note [Bourdoncle Components]).
------------------------------------------------------------------------

{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}

module Lang.Crucible.Analysis.Fixpoint.Components (
  weakTopologicalOrdering,
  WTOComponent(..),
  SCC(..),
  parentWTOComponent,
  -- * Special cases
  cfgWeakTopologicalOrdering,
  cfgSuccessors,
  cfgStart
  ) where

import Control.Applicative
import Control.Monad ( when, void )
import qualified Control.Monad.State.Strict as St
import qualified Data.Foldable as F
import qualified Data.Map as M
import qualified Data.Traversable as T

import Prelude

import           Data.Parameterized.Some (Some(Some))
import           Lang.Crucible.CFG.Core (CFG, BlockID)
import qualified Lang.Crucible.CFG.Core as CFG

-- | Compute a weak topological ordering over a control flow graph.
--
-- Weak topological orderings provide an efficient iteration order for
-- chaotic iterations in abstract interpretation and dataflow analysis.
weakTopologicalOrdering :: (Ord n) => (n -> [n]) -> n -> [WTOComponent n]
weakTopologicalOrdering :: forall n. Ord n => (n -> [n]) -> n -> [WTOComponent n]
weakTopologicalOrdering n -> [n]
successors n
start =
  WTOState n -> [WTOComponent n]
forall n. WTOState n -> [WTOComponent n]
wtoPartition (State (WTOState n) Label -> WTOState n -> WTOState n
forall s a. State s a -> s -> s
St.execState (M n Label -> State (WTOState n) Label
forall n a. M n a -> State (WTOState n) a
runM (n -> M n Label
forall n. Ord n => n -> M n Label
visit n
start)) WTOState n
s0)
  where
    s0 :: WTOState n
s0 = WTOState { wtoSuccessors :: n -> [n]
wtoSuccessors = n -> [n]
successors
                  , wtoPartition :: [WTOComponent n]
wtoPartition = []
                  , wtoStack :: [n]
wtoStack = []
                  , wtoLabelSrc :: Label
wtoLabelSrc = Label
unlabeled
                  , wtoLabels :: Map n Label
wtoLabels = Map n Label
forall k a. Map k a
M.empty
                  }

data WTOComponent n = SCC (SCC n)
                    | Vertex n
                    deriving ((forall a b. (a -> b) -> WTOComponent a -> WTOComponent b)
-> (forall a b. a -> WTOComponent b -> WTOComponent a)
-> Functor WTOComponent
forall a b. a -> WTOComponent b -> WTOComponent a
forall a b. (a -> b) -> WTOComponent a -> WTOComponent b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> WTOComponent a -> WTOComponent b
fmap :: forall a b. (a -> b) -> WTOComponent a -> WTOComponent b
$c<$ :: forall a b. a -> WTOComponent b -> WTOComponent a
<$ :: forall a b. a -> WTOComponent b -> WTOComponent a
Functor, (forall m. Monoid m => WTOComponent m -> m)
-> (forall m a. Monoid m => (a -> m) -> WTOComponent a -> m)
-> (forall m a. Monoid m => (a -> m) -> WTOComponent a -> m)
-> (forall a b. (a -> b -> b) -> b -> WTOComponent a -> b)
-> (forall a b. (a -> b -> b) -> b -> WTOComponent a -> b)
-> (forall b a. (b -> a -> b) -> b -> WTOComponent a -> b)
-> (forall b a. (b -> a -> b) -> b -> WTOComponent a -> b)
-> (forall a. (a -> a -> a) -> WTOComponent a -> a)
-> (forall a. (a -> a -> a) -> WTOComponent a -> a)
-> (forall a. WTOComponent a -> [a])
-> (forall a. WTOComponent a -> Bool)
-> (forall a. WTOComponent a -> Int)
-> (forall a. Eq a => a -> WTOComponent a -> Bool)
-> (forall a. Ord a => WTOComponent a -> a)
-> (forall a. Ord a => WTOComponent a -> a)
-> (forall a. Num a => WTOComponent a -> a)
-> (forall a. Num a => WTOComponent a -> a)
-> Foldable WTOComponent
forall a. Eq a => a -> WTOComponent a -> Bool
forall a. Num a => WTOComponent a -> a
forall a. Ord a => WTOComponent a -> a
forall m. Monoid m => WTOComponent m -> m
forall a. WTOComponent a -> Bool
forall a. WTOComponent a -> Int
forall a. WTOComponent a -> [a]
forall a. (a -> a -> a) -> WTOComponent a -> a
forall m a. Monoid m => (a -> m) -> WTOComponent a -> m
forall b a. (b -> a -> b) -> b -> WTOComponent a -> b
forall a b. (a -> b -> b) -> b -> WTOComponent a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => WTOComponent m -> m
fold :: forall m. Monoid m => WTOComponent m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> WTOComponent a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> WTOComponent a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> WTOComponent a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> WTOComponent a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> WTOComponent a -> b
foldr :: forall a b. (a -> b -> b) -> b -> WTOComponent a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> WTOComponent a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> WTOComponent a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> WTOComponent a -> b
foldl :: forall b a. (b -> a -> b) -> b -> WTOComponent a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> WTOComponent a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> WTOComponent a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> WTOComponent a -> a
foldr1 :: forall a. (a -> a -> a) -> WTOComponent a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> WTOComponent a -> a
foldl1 :: forall a. (a -> a -> a) -> WTOComponent a -> a
$ctoList :: forall a. WTOComponent a -> [a]
toList :: forall a. WTOComponent a -> [a]
$cnull :: forall a. WTOComponent a -> Bool
null :: forall a. WTOComponent a -> Bool
$clength :: forall a. WTOComponent a -> Int
length :: forall a. WTOComponent a -> Int
$celem :: forall a. Eq a => a -> WTOComponent a -> Bool
elem :: forall a. Eq a => a -> WTOComponent a -> Bool
$cmaximum :: forall a. Ord a => WTOComponent a -> a
maximum :: forall a. Ord a => WTOComponent a -> a
$cminimum :: forall a. Ord a => WTOComponent a -> a
minimum :: forall a. Ord a => WTOComponent a -> a
$csum :: forall a. Num a => WTOComponent a -> a
sum :: forall a. Num a => WTOComponent a -> a
$cproduct :: forall a. Num a => WTOComponent a -> a
product :: forall a. Num a => WTOComponent a -> a
F.Foldable, Functor WTOComponent
Foldable WTOComponent
(Functor WTOComponent, Foldable WTOComponent) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> WTOComponent a -> f (WTOComponent b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    WTOComponent (f a) -> f (WTOComponent a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> WTOComponent a -> m (WTOComponent b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    WTOComponent (m a) -> m (WTOComponent a))
-> Traversable WTOComponent
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
WTOComponent (m a) -> m (WTOComponent a)
forall (f :: Type -> Type) a.
Applicative f =>
WTOComponent (f a) -> f (WTOComponent a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> WTOComponent a -> m (WTOComponent b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> WTOComponent a -> f (WTOComponent b)
$ctraverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> WTOComponent a -> f (WTOComponent b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> WTOComponent a -> f (WTOComponent b)
$csequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
WTOComponent (f a) -> f (WTOComponent a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
WTOComponent (f a) -> f (WTOComponent a)
$cmapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> WTOComponent a -> m (WTOComponent b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> WTOComponent a -> m (WTOComponent b)
$csequence :: forall (m :: Type -> Type) a.
Monad m =>
WTOComponent (m a) -> m (WTOComponent a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
WTOComponent (m a) -> m (WTOComponent a)
T.Traversable, Int -> WTOComponent n -> ShowS
[WTOComponent n] -> ShowS
WTOComponent n -> String
(Int -> WTOComponent n -> ShowS)
-> (WTOComponent n -> String)
-> ([WTOComponent n] -> ShowS)
-> Show (WTOComponent n)
forall n. Show n => Int -> WTOComponent n -> ShowS
forall n. Show n => [WTOComponent n] -> ShowS
forall n. Show n => WTOComponent n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall n. Show n => Int -> WTOComponent n -> ShowS
showsPrec :: Int -> WTOComponent n -> ShowS
$cshow :: forall n. Show n => WTOComponent n -> String
show :: WTOComponent n -> String
$cshowList :: forall n. Show n => [WTOComponent n] -> ShowS
showList :: [WTOComponent n] -> ShowS
Show)

data SCC n = SCCData  { forall n. SCC n -> n
wtoHead :: n
                      , forall n. SCC n -> [WTOComponent n]
wtoComps :: [WTOComponent n]
                      }
             deriving ((forall a b. (a -> b) -> SCC a -> SCC b)
-> (forall a b. a -> SCC b -> SCC a) -> Functor SCC
forall a b. a -> SCC b -> SCC a
forall a b. (a -> b) -> SCC a -> SCC b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> SCC a -> SCC b
fmap :: forall a b. (a -> b) -> SCC a -> SCC b
$c<$ :: forall a b. a -> SCC b -> SCC a
<$ :: forall a b. a -> SCC b -> SCC a
Functor, (forall m. Monoid m => SCC m -> m)
-> (forall m a. Monoid m => (a -> m) -> SCC a -> m)
-> (forall m a. Monoid m => (a -> m) -> SCC a -> m)
-> (forall a b. (a -> b -> b) -> b -> SCC a -> b)
-> (forall a b. (a -> b -> b) -> b -> SCC a -> b)
-> (forall b a. (b -> a -> b) -> b -> SCC a -> b)
-> (forall b a. (b -> a -> b) -> b -> SCC a -> b)
-> (forall a. (a -> a -> a) -> SCC a -> a)
-> (forall a. (a -> a -> a) -> SCC a -> a)
-> (forall a. SCC a -> [a])
-> (forall a. SCC a -> Bool)
-> (forall a. SCC a -> Int)
-> (forall a. Eq a => a -> SCC a -> Bool)
-> (forall a. Ord a => SCC a -> a)
-> (forall a. Ord a => SCC a -> a)
-> (forall a. Num a => SCC a -> a)
-> (forall a. Num a => SCC a -> a)
-> Foldable SCC
forall a. Eq a => a -> SCC a -> Bool
forall a. Num a => SCC a -> a
forall a. Ord a => SCC a -> a
forall m. Monoid m => SCC m -> m
forall a. SCC a -> Bool
forall a. SCC a -> Int
forall a. SCC a -> [a]
forall a. (a -> a -> a) -> SCC a -> a
forall m a. Monoid m => (a -> m) -> SCC a -> m
forall b a. (b -> a -> b) -> b -> SCC a -> b
forall a b. (a -> b -> b) -> b -> SCC a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => SCC m -> m
fold :: forall m. Monoid m => SCC m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SCC a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> SCC a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SCC a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> SCC a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> SCC a -> b
foldr :: forall a b. (a -> b -> b) -> b -> SCC a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SCC a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> SCC a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SCC a -> b
foldl :: forall b a. (b -> a -> b) -> b -> SCC a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SCC a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> SCC a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> SCC a -> a
foldr1 :: forall a. (a -> a -> a) -> SCC a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SCC a -> a
foldl1 :: forall a. (a -> a -> a) -> SCC a -> a
$ctoList :: forall a. SCC a -> [a]
toList :: forall a. SCC a -> [a]
$cnull :: forall a. SCC a -> Bool
null :: forall a. SCC a -> Bool
$clength :: forall a. SCC a -> Int
length :: forall a. SCC a -> Int
$celem :: forall a. Eq a => a -> SCC a -> Bool
elem :: forall a. Eq a => a -> SCC a -> Bool
$cmaximum :: forall a. Ord a => SCC a -> a
maximum :: forall a. Ord a => SCC a -> a
$cminimum :: forall a. Ord a => SCC a -> a
minimum :: forall a. Ord a => SCC a -> a
$csum :: forall a. Num a => SCC a -> a
sum :: forall a. Num a => SCC a -> a
$cproduct :: forall a. Num a => SCC a -> a
product :: forall a. Num a => SCC a -> a
F.Foldable, Functor SCC
Foldable SCC
(Functor SCC, Foldable SCC) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> SCC a -> f (SCC b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    SCC (f a) -> f (SCC a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> SCC a -> m (SCC b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    SCC (m a) -> m (SCC a))
-> Traversable SCC
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a. Monad m => SCC (m a) -> m (SCC a)
forall (f :: Type -> Type) a.
Applicative f =>
SCC (f a) -> f (SCC a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> SCC a -> m (SCC b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> SCC a -> f (SCC b)
$ctraverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> SCC a -> f (SCC b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> SCC a -> f (SCC b)
$csequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
SCC (f a) -> f (SCC a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
SCC (f a) -> f (SCC a)
$cmapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> SCC a -> m (SCC b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> SCC a -> m (SCC b)
$csequence :: forall (m :: Type -> Type) a. Monad m => SCC (m a) -> m (SCC a)
sequence :: forall (m :: Type -> Type) a. Monad m => SCC (m a) -> m (SCC a)
T.Traversable, Int -> SCC n -> ShowS
[SCC n] -> ShowS
SCC n -> String
(Int -> SCC n -> ShowS)
-> (SCC n -> String) -> ([SCC n] -> ShowS) -> Show (SCC n)
forall n. Show n => Int -> SCC n -> ShowS
forall n. Show n => [SCC n] -> ShowS
forall n. Show n => SCC n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall n. Show n => Int -> SCC n -> ShowS
showsPrec :: Int -> SCC n -> ShowS
$cshow :: forall n. Show n => SCC n -> String
show :: SCC n -> String
$cshowList :: forall n. Show n => [SCC n] -> ShowS
showList :: [SCC n] -> ShowS
Show)

-- | Useful for creating a first argument to 'weakTopologicalOrdering'. See
-- also 'cfgWeakTopologicalOrdering'.
cfgSuccessors ::
  CFG ext blocks init ret ->
  Some (BlockID blocks) -> [Some (BlockID blocks)]
cfgSuccessors :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Some (BlockID blocks) -> [Some (BlockID blocks)]
cfgSuccessors CFG ext blocks init ret
cfg = \(Some BlockID blocks x
bid) -> 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)]
CFG.nextBlocks (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
CFG.getBlock BlockID blocks x
bid BlockMap ext blocks ret
bm) where
  bm :: BlockMap ext blocks ret
bm = 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
CFG.cfgBlockMap CFG ext blocks init ret
cfg

-- | Useful for creating a second argument to 'weakTopologicalOrdering'. See
-- also 'cfgWeakTopologicalOrdering'.
cfgStart :: CFG ext blocks init ret -> Some (BlockID blocks)
cfgStart :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> Some (BlockID blocks)
cfgStart CFG ext blocks init ret
cfg = BlockID blocks init -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (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
CFG.cfgEntryBlockID CFG ext blocks init ret
cfg)

-- | Compute a weak topological order for the CFG.
cfgWeakTopologicalOrdering ::
  CFG ext blocks init ret ->
  [WTOComponent (Some (BlockID blocks))]
cfgWeakTopologicalOrdering :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> [WTOComponent (Some (BlockID blocks))]
cfgWeakTopologicalOrdering CFG ext blocks init ret
cfg = (Some (BlockID blocks) -> [Some (BlockID blocks)])
-> Some (BlockID blocks) -> [WTOComponent (Some (BlockID blocks))]
forall n. Ord n => (n -> [n]) -> n -> [WTOComponent n]
weakTopologicalOrdering (CFG ext blocks init ret
-> Some (BlockID blocks) -> [Some (BlockID blocks)]
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Some (BlockID blocks) -> [Some (BlockID blocks)]
cfgSuccessors CFG ext blocks init ret
cfg) (CFG ext blocks init ret -> Some (BlockID blocks)
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> Some (BlockID blocks)
cfgStart CFG ext blocks init ret
cfg)

visit :: (Ord n) => n -> M n Label
visit :: forall n. Ord n => n -> M n Label
visit n
v = do
  n -> M n ()
forall n. n -> M n ()
push n
v
  Label
cn <- n -> M n Label
forall n. Ord n => n -> M n Label
labelVertex n
v
  (Label
leastLabel, Bool
isLoop) <- n -> Label -> M n (Label, Bool)
forall n. Ord n => n -> Label -> M n (Label, Bool)
visitSuccessors n
v Label
cn
  Label
cn' <- n -> M n Label
forall n. Ord n => n -> M n Label
lookupLabel n
v
  -- We only create a component if this vertex is the head of its
  -- strongly-connected component (i.e., its label is the same as the
  -- minimum label in its SCC, returned from visitSuccessors).  If so,
  -- we make a new component (which may be a singleton if the vertex
  -- is not in a loop).
  Bool -> M n () -> M n ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Label
cn' Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
leastLabel) (M n () -> M n ()) -> M n () -> M n ()
forall a b. (a -> b) -> a -> b
$ do
    n -> M n ()
forall n. Ord n => n -> M n ()
markDone n
v
    -- Note that we always have to pop, but we might only use the
    -- result if there was a loop
    M n (Maybe n)
forall n. M n (Maybe n)
pop M n (Maybe n) -> (Maybe n -> M n ()) -> M n ()
forall a b. M n a -> (a -> M n b) -> M n b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just n
elt ->
            case Bool
isLoop of
              Bool
False ->
                -- If there is no loop, add a singleton vertex to the partition
                WTOComponent n -> M n ()
forall n. WTOComponent n -> M n ()
addComponent (n -> WTOComponent n
forall n. n -> WTOComponent n
Vertex n
v)
              Bool
True -> do
                  -- Otherwise, unwind the stack and add a full component
                n -> n -> M n ()
forall n. Ord n => n -> n -> M n ()
unwindStack n
elt n
v
                n -> M n ()
forall n. Ord n => n -> M n ()
makeComponent n
v
        Maybe n
Nothing -> String -> M n ()
forall a. HasCallStack => String -> a
error String
"Pop attempted on empty stack (Components:visit)"
  -- We return the least label in the strongly-connected component
  -- containing this vertex, which is used if we have to unwind back
  -- to the SCC head vertex.
  Label -> M n Label
forall a. a -> M n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Label
leastLabel

-- | Unwind the stack until we reach the target node @v@
unwindStack :: (Ord n)
            => n -- ^ Current top of the stack
            -> n -- ^ Target element
            -> M n ()
unwindStack :: forall n. Ord n => n -> n -> M n ()
unwindStack n
elt n
v =
  case n
elt n -> n -> Bool
forall a. Eq a => a -> a -> Bool
/= n
v of
    Bool
False -> () -> M n ()
forall a. a -> M n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
    Bool
True -> do
      n -> M n ()
forall n. Ord n => n -> M n ()
resetLabel n
elt
      M n (Maybe n)
forall n. M n (Maybe n)
pop M n (Maybe n) -> (Maybe n -> M n ()) -> M n ()
forall a b. M n a -> (a -> M n b) -> M n b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Just n
elt' -> n -> n -> M n ()
forall n. Ord n => n -> n -> M n ()
unwindStack n
elt' n
v
          Maybe n
Nothing -> String -> M n ()
forall a. HasCallStack => String -> a
error (String -> M n ()) -> String -> M n ()
forall a b. (a -> b) -> a -> b
$ String
"Emptied stack without finding target element (Components:unwindStack)"

-- | Make a component with the given head element by visiting
-- everything in the SCC and recursively creating a new partition.
makeComponent :: (Ord n) => n -> M n ()
makeComponent :: forall n. Ord n => n -> M n ()
makeComponent n
v = do
  WTOState n
ctx <- M n (WTOState n)
forall s (m :: Type -> Type). MonadState s m => m s
St.get
  -- Do a recursive traversal with an empty partition
  let ctx' :: WTOState n
ctx' = State (WTOState n) () -> WTOState n -> WTOState n
forall s a. State s a -> s -> s
St.execState (M n () -> State (WTOState n) ()
forall n a. M n a -> State (WTOState n) a
runM ((n -> [n]) -> M n ()
forall {t :: Type -> Type} {n}.
(Foldable t, Ord n) =>
(n -> t n) -> M n ()
go (WTOState n -> n -> [n]
forall n. WTOState n -> n -> [n]
wtoSuccessors WTOState n
ctx))) (WTOState n
ctx { wtoPartition = [] })
  -- Restore the old partition but with the updated context
  WTOState n -> M n ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
St.put (WTOState n
ctx' { wtoPartition = wtoPartition ctx })
  let cmp :: WTOComponent n
cmp = SCC n -> WTOComponent n
forall n. SCC n -> WTOComponent n
SCC (SCC n -> WTOComponent n) -> SCC n -> WTOComponent n
forall a b. (a -> b) -> a -> b
$ SCCData { wtoHead :: n
wtoHead = n
v
                          , wtoComps :: [WTOComponent n]
wtoComps = WTOState n -> [WTOComponent n]
forall n. WTOState n -> [WTOComponent n]
wtoPartition WTOState n
ctx'
                          }
  WTOComponent n -> M n ()
forall n. WTOComponent n -> M n ()
addComponent WTOComponent n
cmp
  where
    go :: (n -> t n) -> M n ()
go n -> t n
successors = t n -> (n -> M n ()) -> M n ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
F.forM_ (n -> t n
successors n
v) ((n -> M n ()) -> M n ()) -> (n -> M n ()) -> M n ()
forall a b. (a -> b) -> a -> b
$ \n
s -> do
      Label
sl <- n -> M n Label
forall n. Ord n => n -> M n Label
lookupLabel n
s
      Bool -> M n () -> M n ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Label
sl Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
unlabeled) (M n () -> M n ()) -> M n () -> M n ()
forall a b. (a -> b) -> a -> b
$ do
        M n Label -> M n ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (n -> M n Label
forall n. Ord n => n -> M n Label
visit n
s)

-- | Visit successors of a node and find:
--
-- 1) The minimum label number of any reachable (indirect) successor
-- and 2) If the node is in a loop
visitSuccessors :: (Ord n) => n -> Label -> M n (Label, Bool)
visitSuccessors :: forall n. Ord n => n -> Label -> M n (Label, Bool)
visitSuccessors n
v Label
leastLabel0 = do
  n -> [n]
sucs <- (WTOState n -> n -> [n]) -> M n (n -> [n])
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
St.gets WTOState n -> n -> [n]
forall n. WTOState n -> n -> [n]
wtoSuccessors
  ((Label, Bool) -> n -> M n (Label, Bool))
-> (Label, Bool) -> [n] -> M n (Label, Bool)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
F.foldlM (Label, Bool) -> n -> M n (Label, Bool)
forall {n}. Ord n => (Label, Bool) -> n -> M n (Label, Bool)
go (Label
leastLabel0, Bool
False) (n -> [n]
sucs n
v)
  where
    go :: (Label, Bool) -> n -> M n (Label, Bool)
go acc :: (Label, Bool)
acc@(Label
leastLabel, Bool
_) n
successor = do
      Label
scn <- n -> M n Label
forall n. Ord n => n -> M n Label
lookupLabel n
successor
      Label
minScn <- case Label
scn Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
unlabeled of
        Bool
True -> n -> M n Label
forall n. Ord n => n -> M n Label
visit n
successor
        Bool
False -> Label -> M n Label
forall a. a -> M n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Label
scn
      case Label
minScn Label -> Label -> Bool
forall a. Ord a => a -> a -> Bool
<= Label
leastLabel of
        Bool
True -> (Label, Bool) -> M n (Label, Bool)
forall a. a -> M n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Label
minScn, Bool
True)
        Bool
False -> (Label, Bool) -> M n (Label, Bool)
forall a. a -> M n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Label, Bool)
acc

-- | Assign a label to a vertex.
--
-- This generates the next available label and assigns it to the
-- vertex.  Note that labels effectively start at 1, since 0 is used
-- to denote unassigned.  The actual labels are never exposed to
-- users, so that isn't a big deal.
labelVertex :: (Ord n) => n -> M n Label
labelVertex :: forall n. Ord n => n -> M n Label
labelVertex n
v = do
  Label
cn <- Label -> Label
nextLabel (Label -> Label) -> M n Label -> M n Label
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (WTOState n -> Label) -> M n Label
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
St.gets WTOState n -> Label
forall n. WTOState n -> Label
wtoLabelSrc
  (WTOState n -> WTOState n) -> M n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
St.modify' ((WTOState n -> WTOState n) -> M n ())
-> (WTOState n -> WTOState n) -> M n ()
forall a b. (a -> b) -> a -> b
$ \WTOState n
s -> WTOState n
s { wtoLabelSrc = cn
                       , wtoLabels = M.insert v cn (wtoLabels s)
                       }
  Label -> M n Label
forall a. a -> M n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Label
cn

-- | Look up the label of a vertex
lookupLabel :: (Ord n) => n -> M n Label
lookupLabel :: forall n. Ord n => n -> M n Label
lookupLabel n
v = do
  Map n Label
lbls <- (WTOState n -> Map n Label) -> M n (Map n Label)
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
St.gets WTOState n -> Map n Label
forall n. WTOState n -> Map n Label
wtoLabels
  case n -> Map n Label -> Maybe Label
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup n
v Map n Label
lbls of
    Maybe Label
Nothing -> Label -> M n Label
forall a. a -> M n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Label
unlabeled
    Just Label
l -> Label -> M n Label
forall a. a -> M n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Label
l

-- | Mark a vertex as processed by setting its Label to maxBound
markDone :: (Ord n) => n -> M n ()
markDone :: forall n. Ord n => n -> M n ()
markDone n
v =
  (WTOState n -> WTOState n) -> M n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
St.modify' ((WTOState n -> WTOState n) -> M n ())
-> (WTOState n -> WTOState n) -> M n ()
forall a b. (a -> b) -> a -> b
$ \WTOState n
s -> WTOState n
s { wtoLabels = M.insert v maxLabel (wtoLabels s) }

-- | Reset a label on a vertex to the unlabeled state
resetLabel :: (Ord n) => n -> M n ()
resetLabel :: forall n. Ord n => n -> M n ()
resetLabel n
v =
  (WTOState n -> WTOState n) -> M n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
St.modify' ((WTOState n -> WTOState n) -> M n ())
-> (WTOState n -> WTOState n) -> M n ()
forall a b. (a -> b) -> a -> b
$ \WTOState n
s -> WTOState n
s { wtoLabels = M.insert v unlabeled (wtoLabels s) }

-- | Add a component to the current partition
addComponent :: WTOComponent n -> M n ()
addComponent :: forall n. WTOComponent n -> M n ()
addComponent WTOComponent n
c =
  (WTOState n -> WTOState n) -> M n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
St.modify' ((WTOState n -> WTOState n) -> M n ())
-> (WTOState n -> WTOState n) -> M n ()
forall a b. (a -> b) -> a -> b
$ \WTOState n
s -> WTOState n
s { wtoPartition = c : wtoPartition s }

push :: n -> M n ()
push :: forall n. n -> M n ()
push n
n = (WTOState n -> WTOState n) -> M n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
St.modify' ((WTOState n -> WTOState n) -> M n ())
-> (WTOState n -> WTOState n) -> M n ()
forall a b. (a -> b) -> a -> b
$ \WTOState n
s -> WTOState n
s { wtoStack = n : wtoStack s }

pop :: M n (Maybe n)
pop :: forall n. M n (Maybe n)
pop = do
  [n]
stk <- (WTOState n -> [n]) -> M n [n]
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
St.gets WTOState n -> [n]
forall n. WTOState n -> [n]
wtoStack
  case [n]
stk of
    [] -> Maybe n -> M n (Maybe n)
forall a. a -> M n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe n
forall a. Maybe a
Nothing
    n
n : [n]
rest -> do
      (WTOState n -> WTOState n) -> M n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
St.modify' ((WTOState n -> WTOState n) -> M n ())
-> (WTOState n -> WTOState n) -> M n ()
forall a b. (a -> b) -> a -> b
$ \WTOState n
s -> WTOState n
s { wtoStack = rest }
      Maybe n -> M n (Maybe n)
forall a. a -> M n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (n -> Maybe n
forall a. a -> Maybe a
Just n
n)

data WTOState n = WTOState { forall n. WTOState n -> n -> [n]
wtoSuccessors :: n -> [n]
                           -- ^ The successor relation for the control flow graph
                           , forall n. WTOState n -> [WTOComponent n]
wtoPartition :: [WTOComponent n]
                           -- ^ The partition we are building up
                           , forall n. WTOState n -> [n]
wtoStack :: [n]
                           -- ^ A stack of visited nodes
                           , forall n. WTOState n -> Label
wtoLabelSrc :: Label
                           , forall n. WTOState n -> Map n Label
wtoLabels :: M.Map n Label
                           }

newtype M n a = M { forall n a. M n a -> State (WTOState n) a
runM :: St.State (WTOState n) a }
  deriving ((forall a b. (a -> b) -> M n a -> M n b)
-> (forall a b. a -> M n b -> M n a) -> Functor (M n)
forall a b. a -> M n b -> M n a
forall a b. (a -> b) -> M n a -> M n b
forall n a b. a -> M n b -> M n a
forall n a b. (a -> b) -> M n a -> M n b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall n a b. (a -> b) -> M n a -> M n b
fmap :: forall a b. (a -> b) -> M n a -> M n b
$c<$ :: forall n a b. a -> M n b -> M n a
<$ :: forall a b. a -> M n b -> M n a
Functor, Applicative (M n)
Applicative (M n) =>
(forall a b. M n a -> (a -> M n b) -> M n b)
-> (forall a b. M n a -> M n b -> M n b)
-> (forall a. a -> M n a)
-> Monad (M n)
forall n. Applicative (M n)
forall a. a -> M n a
forall n a. a -> M n a
forall a b. M n a -> M n b -> M n b
forall a b. M n a -> (a -> M n b) -> M n b
forall n a b. M n a -> M n b -> M n b
forall n a b. M n a -> (a -> M n b) -> M n b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall n a b. M n a -> (a -> M n b) -> M n b
>>= :: forall a b. M n a -> (a -> M n b) -> M n b
$c>> :: forall n a b. M n a -> M n b -> M n b
>> :: forall a b. M n a -> M n b -> M n b
$creturn :: forall n a. a -> M n a
return :: forall a. a -> M n a
Monad, St.MonadState (WTOState n), Functor (M n)
Functor (M n) =>
(forall a. a -> M n a)
-> (forall a b. M n (a -> b) -> M n a -> M n b)
-> (forall a b c. (a -> b -> c) -> M n a -> M n b -> M n c)
-> (forall a b. M n a -> M n b -> M n b)
-> (forall a b. M n a -> M n b -> M n a)
-> Applicative (M n)
forall n. Functor (M n)
forall a. a -> M n a
forall n a. a -> M n a
forall a b. M n a -> M n b -> M n a
forall a b. M n a -> M n b -> M n b
forall a b. M n (a -> b) -> M n a -> M n b
forall n a b. M n a -> M n b -> M n a
forall n a b. M n a -> M n b -> M n b
forall n a b. M n (a -> b) -> M n a -> M n b
forall a b c. (a -> b -> c) -> M n a -> M n b -> M n c
forall n a b c. (a -> b -> c) -> M n a -> M n b -> M n c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall n a. a -> M n a
pure :: forall a. a -> M n a
$c<*> :: forall n a b. M n (a -> b) -> M n a -> M n b
<*> :: forall a b. M n (a -> b) -> M n a -> M n b
$cliftA2 :: forall n a b c. (a -> b -> c) -> M n a -> M n b -> M n c
liftA2 :: forall a b c. (a -> b -> c) -> M n a -> M n b -> M n c
$c*> :: forall n a b. M n a -> M n b -> M n b
*> :: forall a b. M n a -> M n b -> M n b
$c<* :: forall n a b. M n a -> M n b -> M n a
<* :: forall a b. M n a -> M n b -> M n a
Applicative)

newtype Label = Label Int
  deriving (Label -> Label -> Bool
(Label -> Label -> Bool) -> (Label -> Label -> Bool) -> Eq Label
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Label -> Label -> Bool
== :: Label -> Label -> Bool
$c/= :: Label -> Label -> Bool
/= :: Label -> Label -> Bool
Eq, Eq Label
Eq Label =>
(Label -> Label -> Ordering)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Label)
-> (Label -> Label -> Label)
-> Ord Label
Label -> Label -> Bool
Label -> Label -> Ordering
Label -> Label -> Label
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 :: Label -> Label -> Ordering
compare :: Label -> Label -> Ordering
$c< :: Label -> Label -> Bool
< :: Label -> Label -> Bool
$c<= :: Label -> Label -> Bool
<= :: Label -> Label -> Bool
$c> :: Label -> Label -> Bool
> :: Label -> Label -> Bool
$c>= :: Label -> Label -> Bool
>= :: Label -> Label -> Bool
$cmax :: Label -> Label -> Label
max :: Label -> Label -> Label
$cmin :: Label -> Label -> Label
min :: Label -> Label -> Label
Ord, Int -> Label -> ShowS
[Label] -> ShowS
Label -> String
(Int -> Label -> ShowS)
-> (Label -> String) -> ([Label] -> ShowS) -> Show Label
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Label -> ShowS
showsPrec :: Int -> Label -> ShowS
$cshow :: Label -> String
show :: Label -> String
$cshowList :: [Label] -> ShowS
showList :: [Label] -> ShowS
Show)

nextLabel :: Label -> Label
nextLabel :: Label -> Label
nextLabel (Label Int
n) = Int -> Label
Label (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

unlabeled :: Label
unlabeled :: Label
unlabeled = Int -> Label
Label Int
0

maxLabel :: Label
maxLabel :: Label
maxLabel = Int -> Label
Label Int
forall a. Bounded a => a
maxBound

-- | Construct a map from each vertex to the head of its parent WTO component.
-- In particular, the head of a component is not in the map. The vertices that
-- are not in any component are not in the map.
parentWTOComponent :: (Ord n) => [WTOComponent n] -> M.Map n n
parentWTOComponent :: forall n. Ord n => [WTOComponent n] -> Map n n
parentWTOComponent = (WTOComponent n -> Map n n) -> [WTOComponent n] -> Map n n
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap' ((WTOComponent n -> Map n n) -> [WTOComponent n] -> Map n n)
-> (WTOComponent n -> Map n n) -> [WTOComponent n] -> Map n n
forall a b. (a -> b) -> a -> b
$ \case
  SCC SCC n
scc' -> SCC n -> Map n n
forall n. Ord n => SCC n -> Map n n
parentWTOComponent' SCC n
scc'
  Vertex{} -> Map n n
forall k a. Map k a
M.empty

parentWTOComponent' :: (Ord n) => SCC n -> M.Map n n
parentWTOComponent' :: forall n. Ord n => SCC n -> Map n n
parentWTOComponent' SCC n
scc =
  (WTOComponent n -> Map n n) -> [WTOComponent n] -> Map n n
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap'
    (\case
      SCC SCC n
scc' -> SCC n -> Map n n
forall n. Ord n => SCC n -> Map n n
parentWTOComponent' SCC n
scc'
      Vertex n
v -> n -> n -> Map n n
forall k a. k -> a -> Map k a
M.singleton n
v (n -> Map n n) -> n -> Map n n
forall a b. (a -> b) -> a -> b
$ SCC n -> n
forall n. SCC n -> n
wtoHead SCC n
scc)
    (SCC n -> [WTOComponent n]
forall n. SCC n -> [WTOComponent n]
wtoComps SCC n
scc)


{- Note [Bourdoncle Components]

Bourdoncle components are a weak topological ordering of graph
components that inform a good ordering for chaotic iteration.  The
components also provide a good set of locations to insert widening
operators for abstract interpretation.  The formulation was proposed
by Francois Bourdoncle in the paper "Efficient chaotic iteration
strategies with widenings" [1].

[1] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.89.8183&rep=rep1&type=pdf

The basic idea of Bourdoncle's algorithm is to compute the recursive
strongly-connected components of the control flow graph, sorted into
topological order.  It is based on Tarjan's SCC algorithm, except that
it recursively looks for strongly-connected components in each SCC it
finds.

-}