Lang.Crucible.Analysis.Fixpoint.Components

Compute a weak topological ordering over a control flow graph using Bourdoncle's algorithm (See Note [Bourdoncle Components]).

Documentation

weakTopologicalOrdering :: Ord n => (n -> [n]) -> n -> [WTOComponent n]

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.

data WTOComponent n

Constructors

SCC (SCC n)

Vertex n

Instances

Foldable WTOComponent

Defined in Lang.Crucible.Analysis.Fixpoint.Components

Methods

fold :: Monoid m => WTOComponent m -> m

foldMap :: Monoid m => (a -> m) -> WTOComponent a -> m

foldMap' :: Monoid m => (a -> m) -> WTOComponent a -> m

foldr :: (a -> b -> b) -> b -> WTOComponent a -> b

foldr' :: (a -> b -> b) -> b -> WTOComponent a -> b

foldl :: (b -> a -> b) -> b -> WTOComponent a -> b

foldl' :: (b -> a -> b) -> b -> WTOComponent a -> b

foldr1 :: (a -> a -> a) -> WTOComponent a -> a

foldl1 :: (a -> a -> a) -> WTOComponent a -> a

toList :: WTOComponent a -> [a]

null :: WTOComponent a -> Bool

length :: WTOComponent a -> Int

elem :: Eq a => a -> WTOComponent a -> Bool

maximum :: Ord a => WTOComponent a -> a

minimum :: Ord a => WTOComponent a -> a

sum :: Num a => WTOComponent a -> a

product :: Num a => WTOComponent a -> a

Traversable WTOComponent

Defined in Lang.Crucible.Analysis.Fixpoint.Components

Methods

traverse :: Applicative f => (a -> f b) -> WTOComponent a -> f (WTOComponent b)

sequenceA :: Applicative f => WTOComponent (f a) -> f (WTOComponent a)

mapM :: Monad m => (a -> m b) -> WTOComponent a -> m (WTOComponent b)

sequence :: Monad m => WTOComponent (m a) -> m (WTOComponent a)

Functor WTOComponent

Defined in Lang.Crucible.Analysis.Fixpoint.Components

Methods

fmap :: (a -> b) -> WTOComponent a -> WTOComponent b

(<$) :: a -> WTOComponent b -> WTOComponent a

Show n => Show (WTOComponent n)

Defined in Lang.Crucible.Analysis.Fixpoint.Components

Methods

showsPrec :: Int -> WTOComponent n -> ShowS

show :: WTOComponent n -> String

showList :: [WTOComponent n] -> ShowS

data SCC n

Constructors

SCCData

Fields

• wtoHead :: n
• wtoComps :: [WTOComponent n]

Instances

Foldable SCC

Defined in Lang.Crucible.Analysis.Fixpoint.Components

Methods

fold :: Monoid m => SCC m -> m

foldMap :: Monoid m => (a -> m) -> SCC a -> m

foldMap' :: Monoid m => (a -> m) -> SCC a -> m

foldr :: (a -> b -> b) -> b -> SCC a -> b

foldr' :: (a -> b -> b) -> b -> SCC a -> b

foldl :: (b -> a -> b) -> b -> SCC a -> b

foldl' :: (b -> a -> b) -> b -> SCC a -> b

foldr1 :: (a -> a -> a) -> SCC a -> a

foldl1 :: (a -> a -> a) -> SCC a -> a

toList :: SCC a -> [a]

null :: SCC a -> Bool

length :: SCC a -> Int

elem :: Eq a => a -> SCC a -> Bool

maximum :: Ord a => SCC a -> a

minimum :: Ord a => SCC a -> a

sum :: Num a => SCC a -> a

product :: Num a => SCC a -> a

Traversable SCC

Defined in Lang.Crucible.Analysis.Fixpoint.Components

Methods

traverse :: Applicative f => (a -> f b) -> SCC a -> f (SCC b)

sequenceA :: Applicative f => SCC (f a) -> f (SCC a)

mapM :: Monad m => (a -> m b) -> SCC a -> m (SCC b)

sequence :: Monad m => SCC (m a) -> m (SCC a)

Functor SCC

Defined in Lang.Crucible.Analysis.Fixpoint.Components

Methods

fmap :: (a -> b) -> SCC a -> SCC b

(<$) :: a -> SCC b -> SCC a

Show n => Show (SCC n)

Defined in Lang.Crucible.Analysis.Fixpoint.Components

Methods

showsPrec :: Int -> SCC n -> ShowS

show :: SCC n -> String

showList :: [SCC n] -> ShowS

parentWTOComponent :: Ord n => [WTOComponent n] -> Map n n

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.

Special cases

cfgWeakTopologicalOrdering :: CFG ext blocks init ret -> [WTOComponent (Some (BlockID blocks))]

Compute a weak topological order for the CFG.

cfgSuccessors :: CFG ext blocks init ret -> Some (BlockID blocks) -> [Some (BlockID blocks)]

Useful for creating a first argument to weakTopologicalOrdering. See also cfgWeakTopologicalOrdering.

cfgStart :: CFG ext blocks init ret -> Some (BlockID blocks)

Useful for creating a second argument to weakTopologicalOrdering. See also cfgWeakTopologicalOrdering.