Up

# moduleFixpoint

: sig

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.

See also DOC Introduction to Lattices and Order B. A. Davey and H. A. Priestley, Cambridge University Press, 2002
See also DOC Fixed Point Theory Andrzej Granas and James Dugundji, Springer, 2003
See also DOC Principles of Program Analysis Flemming Nielson, Hanne Riis Nielson and Chris Hankin, Springer, 2005
See also DOC Ubersetzerbau 3: Analyse und Transformation Reinhard Wilhelm and Helmut Seidl, Springer, 2010
#
module type G = sig

Minimal graph signature for work list algorithm

#
type t
#
module V : Sig.COMPARABLE
#
module E : sig
#
type t
#
val dst : t -> V.t
#
val src : t -> V.t
end
#
val fold_vertex : (V.t -> 'a -> 'a) -> t -> 'a -> 'a
#
val succ_e : t -> V.t -> E.t list
#
val pred_e : t -> V.t -> E.t list
#
val succ : t -> V.t -> V.t list
#
val pred : t -> V.t -> V.t list
end
#
type direction =
 # | Forward # | Backward (* Type of an analysis *)
#
module type Analysis = sig
#
type data

information stored at each vertex

#
type edge

type of edges of the underlying graph

#
type vertex

type of vertices of the underlying graph

#
type g

type of the underlying graph

#
val direction : direction

the direction of the analysis

#
val join : data -> data -> data

operation how to join data when paths meet

#
val equal : data -> data -> bool

predicate to determine the fixpoint

#
val analyze : edge -> data -> data

the actual analysis of one edge; provided the edge and the incoming data, it needs to compute the outgoing data

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

`analyze f g` computes the fixpoint on the given graph using the work list algorithm. Beware that a misconstructed Analysis will not terminate! `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 `f` and `g` only. The result is a function that is to be used to query the result of the analysis.

end
end