Copyright	(c) Galois Inc 2015
License	BSD3
Maintainer	Tristan Ravitch <tristan@galois.com>
Stability	provisional
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Analysis.Fixpoint.Components

Contents

Special cases

Description

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

Synopsis

weakTopologicalOrdering :: Ord n => (n -> [n]) -> n -> [WTOComponent n]
data WTOComponent n
- = SCC (SCC n)
- | Vertex n
data SCC n = SCCData {
- wtoHead :: n
- wtoComps :: [WTOComponent n]
}
cfgWeakTopologicalOrdering :: CFG ext blocks init ret -> [WTOComponent (Some (BlockID blocks))]
cfgSuccessors :: CFG ext blocks init ret -> Some (BlockID blocks) -> [Some (BlockID blocks)]
cfgStart :: CFG ext blocks init ret -> Some (BlockID blocks)

Documentation

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

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 Source #

Constructors

SCC (SCC n)
Vertex n

Instances

Instances details

Foldable WTOComponent Source #
Instance details 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 Source #
Instance details 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 Source #
Instance details 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) Source #
Instance details Defined in Lang.Crucible.Analysis.Fixpoint.Components Methods showsPrec :: Int -> WTOComponent n -> ShowS # show :: WTOComponent n -> String # showList :: [WTOComponent n] -> ShowS #

data SCC n Source #

Constructors

SCCData
Fields wtoHead :: n wtoComps :: [WTOComponent n]

Instances

Instances details

Foldable SCC Source #
Instance details 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 Source #
Instance details 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 Source #
Instance details 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) Source #
Instance details Defined in Lang.Crucible.Analysis.Fixpoint.Components Methods showsPrec :: Int -> SCC n -> ShowS # show :: SCC n -> String # showList :: [SCC n] -> ShowS #

Special cases

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

Compute a weak topological order for the CFG.

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

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

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

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