LLVM.Analysis.Dataflow

This module defines an interface for intra-procedural dataflow analysis (forward and backward).

The user defines an analysis with the dataflowAnalysis function, which can be constructed from a top value, a meet operator, and a transfer function (which is run as needed for Instructions).

To use this dataflow analysis framework, pass it an initial analysis state (which may be top or a different value) and something providing a control flow graph, along with the opaque analysis object. The analysis then returns an abstract result that represents dataflow facts at each Instruction in the Function. For example,

 let initialState = ...
     a = dataflowAnalysis top meet transfer
     results = forwardDataflow initialState analysis cfg
 in dataflowResult results

gives the dataflow value for the virtual exit node (to which all other function termination instructions flow). To get results at other instructions, see dataflowResultAt.

Dataflow analysis

data DataflowAnalysis m f

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.

fwdDataflowAnalysis

Arguments

:: (Eq f, Monad m)

=> f

Top

-> (f -> f -> f)

Meet

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

Transfer

-> DataflowAnalysis m f

Define a basic DataflowAnalysis

bwdDataflowAnalysis

Arguments

:: (Eq f, Monad m)

=> f

Top

-> (f -> f -> f)

Meet

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

Transfer

-> DataflowAnalysis m f

A basic backward dataflow analysis

fwdDataflowEdgeAnalysis

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.

bwdDataflowEdgeAnalysis

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

dataflow

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

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

Instances

Eq f => Eq (DataflowResult m f)

Show f => Show (DataflowResult m f)

NFData f => NFData (DataflowResult m f)

dataflowResult :: DataflowResult m f -> f

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 f

Look up the dataflow fact at a particular Instruction.