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 a CFG from a FunctionDefn.
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 DataFlow type class for your data type, implementing emptyFacts, transfer, and join.
Build the CFG for a function using buildCFG.
Run the fixpoint solver on the generated CFG.
Extract and use the computed cfgInFacts and cfgOutFacts from the resulting CFG.

Synopsis

data CFGNode l a = CFGNode {
- cfgNodeId :: Int
- cfgPreds :: [Int]
- cfgSuccs :: [Int]
- cfgStmts :: [Node (Lexeme l)]
- cfgInFacts :: a
- cfgOutFacts :: a
}
type CFG l a = Map Int (CFGNode l a)
class (Eq a, Show a) => DataFlow (c :: Type -> Type) l a where
- emptyFacts :: c l -> a
- transfer :: c l -> l -> a -> Node (Lexeme l) -> (a, Set (l, [Int]))
- join :: c l -> a -> a -> a
fixpoint :: forall c l a. (DataFlow c l a, Show l, Ord l) => c l -> l -> CFG l a -> (CFG l a, Set (l, [Int]))
buildCFG :: forall c l a. (DataFlow c l a, Pretty l, Ord l, Show l) => c l -> Node (Lexeme l) -> a -> CFG l a

Documentation

data CFGNode l a Source #

A node in the control flow graph. Each node represents a basic block of statements.

Constructors

CFGNode
Fields cfgNodeId :: Int A unique identifier for the node. cfgPreds :: [Int] A list of predecessor node IDs. cfgSuccs :: [Int] A list of successor node IDs. cfgStmts :: [Node (Lexeme l)] The statements in this basic block. cfgInFacts :: a The data flow facts at the entry of this node. cfgOutFacts :: a The data flow facts at the exit of this node.

Instances

Instances details

(Eq l, Eq a) => Eq (CFGNode l a) Source #
Instance details Defined in Tokstyle.Analysis.DataFlow Methods (==) :: CFGNode l a -> CFGNode l a -> Bool # (/=) :: CFGNode l a -> CFGNode l a -> Bool #
(Show l, Show a) => Show (CFGNode l a) Source #
Instance details Defined in Tokstyle.Analysis.DataFlow Methods showsPrec :: Int -> CFGNode l a -> ShowS # show :: CFGNode l a -> String # showList :: [CFGNode l a] -> ShowS #

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) => DataFlow (c :: Type -> Type) l a 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 -> a Source #

The facts for an empty basic block.

transfer :: c l -> l -> a -> Node (Lexeme l) -> (a, Set (l, [Int])) 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 -> 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

Instances details

DataFlow PointsToContext Text PointsToState Source #	The PointsTo analysis is an instance of the generic DataFlow framework.
Instance details Defined in Tokstyle.Analysis.PointsTo Methods emptyFacts :: PointsToContext Text -> PointsToState Source # transfer :: PointsToContext Text -> Text -> PointsToState -> Node (Lexeme Text) -> (PointsToState, Set (Text, [Int])) Source # join :: PointsToContext Text -> PointsToState -> PointsToState -> PointsToState Source #
DataFlow SecurityRankContext Text SecurityRankState Source #
Instance details Defined in Tokstyle.Analysis.SecurityRank Methods emptyFacts :: SecurityRankContext Text -> SecurityRankState Source # transfer :: SecurityRankContext Text -> Text -> SecurityRankState -> Node (Lexeme Text) -> (SecurityRankState, Set (Text, [Int])) Source # join :: SecurityRankContext Text -> SecurityRankState -> SecurityRankState -> SecurityRankState Source #

fixpoint :: forall c l a. (DataFlow c l a, Show l, Ord l) => c l -> l -> CFG l a -> (CFG l a, Set (l, [Int])) 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.

buildCFG :: forall c l a. (DataFlow c l a, Pretty l, Ord l, Show l) => c l -> Node (Lexeme l) -> a -> CFG l a Source #

Build a control flow graph for a function definition. This is the main entry point for constructing a CFG from a Cimple AST.