| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Tokstyle.Analysis.DataFlow
Description
This module provides a generic framework for forward data flow analysis
on C code, represented by the Ast. It includes tools
for building a control flow graph (CFG) from a function definition and
a fixpoint solver to compute data flow facts.
The core components are:
CFG: A control flow graph representation, where nodes contain basic blocks of statements.DataFlow: A type class that defines the specific analysis to be performed (e.g., reaching definitions, liveness analysis).buildCFG: A function to construct aCFGfrom aFunctionDefn.fixpoint: A generic solver that iteratively computes data flow facts until a stable state (fixpoint) is reached.
To use this module, you need to:
- Define a data type for your data flow facts.
- Create an instance of the
DataFlowtype class for your data type, implementingemptyFacts,transfer, andjoin. - Build the CFG for a function using
buildCFG. - Run the
fixpointsolver on the generated CFG. - Extract and use the computed
cfgInFactsandcfgOutFactsfrom the resulting CFG.
Synopsis
- data CFGNode l a = CFGNode {}
- type CFG l a = Map Int (CFGNode l a)
- class (Eq a, Show a, Monad m, Ord callCtx) => DataFlow m (c :: Type -> Type) l a callCtx | a -> l, a -> callCtx where
- fixpoint :: forall m c l a callCtx. (DataFlow m c l a callCtx, Show l, Ord l) => c l -> l -> CFG l a -> m (CFG l a, Set (l, callCtx))
- buildCFG :: forall m c l a callCtx. (DataFlow m c l a callCtx, Pretty l, Ord l, Show l, IsString l) => c l -> Node (Lexeme l) -> a -> m (CFG l a)
Documentation
A node in the control flow graph. Each node represents a basic block of statements.
Constructors
| CFGNode | |
Fields
| |
type CFG l a = Map Int (CFGNode l a) Source #
The Control Flow Graph is a map from node IDs to CFGNodes.
class (Eq a, Show a, Monad m, Ord callCtx) => DataFlow m (c :: Type -> Type) l a callCtx | a -> l, a -> callCtx where Source #
A type class for data flow analysis. Users of this framework must provide an instance of this class for their specific analysis.
Methods
emptyFacts :: c l -> m a Source #
The facts for an empty basic block.
transfer :: c l -> l -> Int -> a -> Node (Lexeme l) -> m (a, Set (l, callCtx)) Source #
The transfer function defines how a single statement affects the data flow facts. It takes the facts before the statement and returns the facts after the statement, plus any new work discovered.
join :: c l -> a -> a -> m a Source #
The join operator combines facts from multiple predecessor nodes. This is used at control flow merge points (e.g., after an if-statement or at the start of a loop).
Instances
| DataFlow PointsToAnalysis PointsToContext ScopedId PointsToFact RelevantInputState Source # | |
Defined in Tokstyle.Analysis.PointsTo Methods emptyFacts :: PointsToContext ScopedId -> PointsToAnalysis PointsToFact Source # transfer :: PointsToContext ScopedId -> ScopedId -> Int -> PointsToFact -> Node (Lexeme ScopedId) -> PointsToAnalysis (PointsToFact, Set (ScopedId, RelevantInputState)) Source # join :: PointsToContext ScopedId -> PointsToFact -> PointsToFact -> PointsToAnalysis PointsToFact Source # | |
fixpoint :: forall m c l a callCtx. (DataFlow m c l a callCtx, Show l, Ord l) => c l -> l -> CFG l a -> m (CFG l a, Set (l, callCtx)) Source #
A generic fixpoint solver for forward data flow analysis. This function iteratively applies the transfer function to each node in the CFG until the data flow facts no longer change. It uses a worklist algorithm for efficiency, and returns the final CFG along with any new work discovered.