Safe Haskell | None |
---|

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 `Instruction`

s).

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`

.

- data DataflowAnalysis m f
- fwdDataflowAnalysis :: (Eq f, Monad m) => f -> (f -> f -> f) -> (f -> Instruction -> m f) -> DataflowAnalysis m f
- bwdDataflowAnalysis :: (Eq f, Monad m) => f -> (f -> f -> f) -> (f -> Instruction -> m f) -> DataflowAnalysis m f
- fwdDataflowEdgeAnalysis :: (Eq f, Monad m) => f -> (f -> f -> f) -> (f -> Instruction -> m f) -> (f -> Instruction -> m [(BasicBlock, f)]) -> DataflowAnalysis m f
- bwdDataflowEdgeAnalysis :: (Eq f, Monad m) => f -> (f -> f -> f) -> (f -> Instruction -> m f) -> ([(BasicBlock, f)] -> Instruction -> m f) -> DataflowAnalysis m f
- dataflow :: forall m f cfgLike. HasCFG cfgLike => cfgLike -> DataflowAnalysis m f -> f -> m (DataflowResult m f)
- data DataflowResult m f
- dataflowResult :: DataflowResult m f -> f
- dataflowResultAt :: DataflowResult m f -> Instruction -> m f

# Dataflow analysis

data DataflowAnalysis m f Source

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.

:: (Eq f, Monad m) | |

=> f | Top |

-> (f -> f -> f) | Meet |

-> (f -> Instruction -> m f) | Transfer |

-> DataflowAnalysis m f |

Define a basic `DataflowAnalysis`

:: (Eq f, Monad m) | |

=> f | Top |

-> (f -> f -> f) | Meet |

-> (f -> Instruction -> m f) | Transfer |

-> DataflowAnalysis m f |

A basic backward dataflow analysis

:: (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
`meet`

ed together. Missing values are taken from the result of the
normal transfer function.

:: (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 |

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

The opaque result of a dataflow analysis. Use the functions
`dataflowResult`

and `dataflowResultAt`

to extract results.

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.