Fixpoint computation implemented using the work list algorithm. This module makes writing data-flow analysis easy.
One of the simplest fixpoint analysis is that of reachability.
Given a directed graph module
G, its analysis can be implemented
module Reachability = Graph.Fixpoint.Make(G) (struct type vertex = G.E.vertex type edge = G.E.t type g = G.t type data = bool let direction = Graph.Fixpoint.Forward let equal = (=) let join = (||) let analyze _ = (fun x -> x) end)
The types for
g are those of the graph to be
data type is
bool: It will tell if the
vertex is reachable from the start vertex. The
bool is simply structural equality; the
join operation is
logical or. The
analyze function is very simple, too: If the
predecessor vertex is reachable, so is the successor vertex of the
To use the analysis, an instance of a graph
g is required. For
this analysis a predicate
is_root_vertex : G.E.vertex -> bool is
required to initialize the reachability of the root vertex to
true and of all other vertices to
let g = ... let result = Reachability.analyze is_root_vertex g
result is a map of type
G.E.vertex -> bool that can be
queried for every vertex to tell if the vertex is reachable from
the root vertex.
Minimal graph signature for work list algorithm
information stored at each vertex
type of edges of the underlying graph
type of vertices of the underlying graph
type of the underlying graph
analyze f g computes the fixpoint on the given graph using the
work list algorithm. Beware that a misconstructed Analysis will
f is used to create the initial analysis
data. The function returned is a map to see what data was computed
for which node.
Beware of applying function
analyze partially, to arguments
g only. The result is a function that is to be used to query
the result of the analysis.