Graph.Fixpoint
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 as follows:
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 vertex
, edge
and g
are those of the graph to be analyzed. The data
type is bool
: It will tell if the vertex is reachable from the start vertex. The equal
operation for 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 edge.
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 false
.
let g = ...
let result = Reachability.analyze is_root_vertex g
The 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.