package ocamlgraph

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 =
  1. | Forward
  2. | Backward
    (*

    Type of an analysis

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