llvm-analysis-0.3.0: A Haskell library for analyzing LLVM bitcode

Safe HaskellNone

LLVM.Analysis.CFG.Internal

Contents

Synopsis

CFG

data CFG Source

The type of function control flow graphs.

Constructors

CFG 

Fields

cfgFunction :: Function
 
cfgLabelMap :: Map BasicBlock Label
 
cfgBlockMap :: Map Label BasicBlock
 
cfgBody :: Graph Insn C C
 
cfgEntryLabel :: Label
 
cfgExitLabel :: Label
 
cfgPredecessors :: Map BasicBlock [BasicBlock]
 

Instances

Eq CFG

This instance does not compare the graphs directly - instead it compares just the function from which the graph is constructed. The construction is completely deterministic so this should be fine. It is also fast because function comparison just compares unique integer IDs.

HasFunction CFG 
ToGraphviz CFG 
FuncLike CFG 
HasCFG CFG 
HasPostdomTree CFG

Note that this instance constructs the postdominator tree from scratch.

HasDomTree CFG

Note, this instance constructs the dominator tree and could be expensive

class HasCFG a whereSource

A class for things from which a CFG can be obtained.

Methods

getCFG :: a -> CFGSource

controlFlowGraph :: Function -> CFGSource

Create a CFG for a function

basicBlockPredecessors :: HasCFG cfgLike => cfgLike -> BasicBlock -> [BasicBlock]Source

basicBlockSuccessors :: HasCFG cfgLike => cfgLike -> BasicBlock -> [BasicBlock]Source

Dataflow

data DataflowAnalysis m f whereSource

An opaque representation of a dataflow analysis. Analyses of this type are suitable for both forward and backward use.

For all dataflow analyses, the standard rules apply.

1) meet a top == a

2) Your lattice f must have finite height

The m type parameter is a Monad; this dataflow framework provides a monadic transfer function. This is intended to allow transfer functions to have monadic contexts that provide MonadReader and MonadWriter-like functionality. State is also useful for caching expensive sub-computations. Keep in mind that the analysis iterates to a fixedpoint and side effects in the monad will be repeated.

Constructors

FwdDataflowAnalysis :: (Eq f, Monad m) => f -> (f -> f -> f) -> (f -> Instruction -> m f) -> Maybe (f -> Instruction -> m [(BasicBlock, f)]) -> DataflowAnalysis m f 

Fields

analysisTop :: f
 
analysisMeet :: f -> f -> f
 
analysisTransfer :: f -> Instruction -> m f
 
analysisFwdEdgeTransfer :: Maybe (f -> Instruction -> m [(BasicBlock, f)])
 
BwdDataflowAnalysis :: (Eq f, Monad m) => f -> (f -> f -> f) -> (f -> Instruction -> m f) -> Maybe ([(BasicBlock, f)] -> Instruction -> m f) -> DataflowAnalysis m f 

Fields

analysisTop :: f
 
analysisMeet :: f -> f -> f
 
analysisTransfer :: f -> Instruction -> m f
 
analysisBwdEdgeTransfer :: Maybe ([(BasicBlock, f)] -> Instruction -> m f)
 

fwdDataflowAnalysisSource

Arguments

:: (Eq f, Monad m) 
=> f

Top

-> (f -> f -> f)

Meet

-> (f -> Instruction -> m f)

Transfer

-> DataflowAnalysis m f 

Define a basic DataflowAnalysis

bwdDataflowAnalysisSource

Arguments

:: (Eq f, Monad m) 
=> f

Top

-> (f -> f -> f)

Meet

-> (f -> Instruction -> m f)

Transfer

-> DataflowAnalysis m f 

A basic backward dataflow analysis

fwdDataflowEdgeAnalysisSource

Arguments

:: (Eq f, Monad m) 
=> f

Top

-> (f -> f -> f)

meet

-> (f -> Instruction -> m f)

Transfer

-> (f -> Instruction -> m [(BasicBlock, f)])

Edge Transfer

-> DataflowAnalysis m f 

A forward dataflow analysis that provides an addition /edge transfer function/. This function is run with each Terminator instruction (after the normal transfer function, whose results are fed to the edge transfer function). The edge transfer function allows you to let different information flow to each successor block of a terminator instruction.

If a BasicBlock in the edge transfer result is not a successor of the input instruction, that mapping is discarded. Multiples are meeted together. Missing values are taken from the result of the normal transfer function.

bwdDataflowEdgeAnalysisSource

Arguments

:: (Eq f, Monad m) 
=> f

Top

-> (f -> f -> f)

meet

-> (f -> Instruction -> m f)

Transfer

-> ([(BasicBlock, f)] -> Instruction -> m f)

Edge Transfer

-> DataflowAnalysis m f 

dataflowSource

Arguments

:: forall m f cfgLike . HasCFG cfgLike 
=> cfgLike

Something providing a CFG

-> DataflowAnalysis m f

The analysis to run

-> f

Initial fact for the entry node

-> m (DataflowResult m f) 

data DataflowResult m f whereSource

The opaque result of a dataflow analysis. Use the functions dataflowResult and dataflowResultAt to extract results.

Constructors

DataflowResult :: CFG -> DataflowAnalysis m f -> Fact C f -> Direction -> DataflowResult m f 

Instances

Eq f => Eq (DataflowResult m f) 
Show f => Show (DataflowResult m f) 
NFData f => NFData (DataflowResult m f) 

dataflowResult :: DataflowResult m f -> fSource

Look up the dataflow fact at the virtual exit note. This combines the results along all paths, including those ending in termination instructions like Unreachable and Resume.

If you want the result at only the return instruction(s), use dataflowResultAt and meets the results together.

dataflowResultAt :: DataflowResult m f -> Instruction -> m fSource

Look up the dataflow fact at a particular Instruction.

Internal types

data Insn e x whereSource

This is a wrapper GADT around the LLVM IR to mesh with Hoopl. It won't be exported or exposed to the user at all. We need this for two reasons:

1) Hoopl requires explicit Label instructions. In LLVM these are implicit in the function structure through BasicBlocks

2) Additionally, LLVM doens't have a unique exit instruction per function. resume, ret, and unreachable all terminate execution. c.f. UniqueExitLabel and ExitLabel (both seem to be needed because hoopl blocks need an entry and an exit).

Constructors

Lbl :: BasicBlock -> Label -> Insn C O 
Terminator :: Instruction -> [Label] -> Insn O C 
UniqueExitLabel :: Label -> Insn C O 
UniqueExit :: Insn O C 
Normal :: Instruction -> Insn O O 

Instances