Up
# module Fixpoint

: 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 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