Safe Haskell	None

LLVM.Analysis.Dataflow

Contents

Dataflow analysis
Dataflow results

Description

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

The user simply defines a type to represent the state of their dataflow analysis as an instance of DataflowAnalysis. This class adds one function, transfer, to the semilattices defined in the lattices package.

To use this dataflow analysis framework, pass it an initial analysis state and either a control flow graph or a function. The analysis then returns a function that maps instructions to the dataflow value at that instruction. For example,

 let initialState = ...
     cfg = mkCFG f
     results = forwardDataflow initialState cfg
 in results (cfgFinalValue cfg)

gives the dataflow value for the return instruction in function f. Any instruction in f can be used as an argument to the result function.

Synopsis

Dataflow analysis

class (BoundedMeetSemiLattice a, Monad m) => DataflowAnalysis m a whereSource

A class defining the interface to a dataflow analysis. The analysis object itself that is passed to one of the dataflow functions acts as the initial state.

Note that the second type parameter, c, can be used to pass information that is global and constant for the analysis of a function. This can save space by not requiring the information to be stored redundantly in every dataflow fact. If this parameter is not needed, it can safely be instantiated as () (and subsequently ignored).

Methods

transfer Source

Arguments

:: a	The incoming analysis state
-> Instruction	The instruction being analyzed
-> m a

The transfer function of this analysis. It is given any global constant data, the current set of facts, the current instruction, and a list of incoming edges.

phiTransfer Source

Arguments

:: [Instruction]	The instruction being analyzed
-> [(BasicBlock, a, CFGEdge)]	Incoming CFG edges
-> m a

edgeTransfer :: a -> CFGEdge -> m aSource

This is a hook to perform some analysis on an _edge_ before the normal transfer functions run on the next instruction.

This is a convenient separation of edge and instruction processing, but it also improves precision in cases like:

 define void @f(i8* %p) nounwind uwtable {
   %1 = icmp ne i8* %p, null
   br i1 %1, label %2, label %3

 ; <label>:2                                       ; preds = %0
   call void @free(i8* %p) nounwind
   br label %3

 ; <label>:3                                       ; preds = %2, %0
   ret void
 }

Without separate edge processing, the join at the return statement executes before we can use information about %p being NULL on one edge of the branch.

NOTE: This transfer function is only appleid to edges between basic blocks. Within a basic block, the edge is always an unconditional edge and there is no merging anyway.

Instances

(BoundedMeetSemiLattice ScalarInfo, Monad m) => DataflowAnalysis m ScalarInfo
(BoundedMeetSemiLattice ReturnInfo, Monad (AnalysisMonad m), Monad m) => DataflowAnalysis (AnalysisMonad m) ReturnInfo

class MeetSemiLattice a where

Methods

meet :: a -> a -> a

Instances

MeetSemiLattice Bool
MeetSemiLattice ReturnInfo
MeetSemiLattice ScalarInfo
(Ord a, Enumerable a) => MeetSemiLattice (Set (Enumerated a))
MeetSemiLattice v => MeetSemiLattice (k -> v)
(MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b)
(Ord k, Enumerable k, MeetSemiLattice v) => MeetSemiLattice (Map (Enumerated k) v)

class MeetSemiLattice a => BoundedMeetSemiLattice a where

Methods

top :: a

Instances

BoundedMeetSemiLattice Bool
BoundedMeetSemiLattice ReturnInfo
BoundedMeetSemiLattice ScalarInfo
(MeetSemiLattice (Set (Enumerated a)), Ord a, Enumerable a) => BoundedMeetSemiLattice (Set (Enumerated a))
(MeetSemiLattice (k -> v), BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (k -> v)
(MeetSemiLattice (a, b), BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b)
(MeetSemiLattice (Map (Enumerated k) v), Ord k, Enumerable k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Map (Enumerated k) v)

meets :: BoundedMeetSemiLattice a => [a] -> a

forwardDataflow :: (Eq a, HasCFG b, DataflowAnalysis m a) => a -> b -> m (DataflowResult a)Source

backwardDataflow :: (Eq a, HasCFG b, DataflowAnalysis m a) => a -> b -> m (DataflowResult a)Source

FIXME: This is currently broken. When should the phi instructions be processed in parallel? Before or after the instructions in the block? It also needs to look up the output fact of the *first* instruction of the block instead of the last

Dataflow results

data DataflowResult a Source

The opaque result of a dataflow analysis

Instances

Eq a => Eq (DataflowResult a)
NFData a => NFData (DataflowResult a)

dataflowResult :: DataflowResult a -> Instruction -> aSource

Get the result of a dataflow analysis at the given instruction. Will throw an error if the instruction is not in the function for which this analysis was run.

FIXME: The block result here needs to be able to reverse the instruction list if doing a backwards analysis