Module 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.

author
Markus W. Weissmann
see Introduction to Lattices and Order

B. A. Davey and H. A. Priestley, Cambridge University Press, 2002

see Fixed Point Theory

Andrzej Granas and James Dugundji, Springer, 2003

see Principles of Program Analysis

Flemming Nielson, Hanne Riis Nielson and Chris Hankin, Springer, 2005

see Ubersetzerbau 3: Analyse und Transformation

Reinhard Wilhelm and Helmut Seidl, Springer, 2010

module type G = sig ... end

Minimal graph signature for work list algorithm

type direction =
| Forward
| Backward

Type of an analysis

module type Analysis = sig ... end
module Make : functor (G : G) -> functor (A : Analysis with type g = G.t with type edge = G.E.t with type vertex = G.V.t) -> sig ... end