package graphlib

Make(Node)(Edge) creates a module that implements Graph interface and has unlabeled nodes of type Node.t and edges labeled with Edge.t

Labeled(Node)(Node_label)(Edge_label) creates a graph structure with both nodes and edges labeled with abitrary types.

create (module G) ~nodes ~edges () creates a graph using implementation provided by module G. Example:

module G = Graphlib.String.Bool;;
let g = Graphlib.create (module G) ~edges:[
    "entry", "loop", true;
    "loop", "exit", false;
    "loop", "loop", true] ()

union (module G) g1 g2 returns a graph g that is a union of graphs g1 and g2, i.e., contains all nodes and edges from this graphs.

Postcondition:

          - N(g) = N(g1) ∪ N(g2).
          - E(g) = E(g1) ∪ E(g2).

inter (module G) g1 g2 returns a graph g that is an intersection of graphs g1 and g2, i.e., it contain and edges from this graphs.

Postcondition:

          - N(g) = N(g1) ∩ N(g2).
          - E(g) = E(g1) ∩ E(g2).

to_dot (module G) ~filename:"graph.dot" g dumps graph g using dot format. This is a customizable version of printing function. For most cases it will be enough to use G.pp or G.to_string function. Use this function, if you really need to customize your output.

• parameter graph_attrs

  a list of global graph attributes;

• parameter node_attrs

  a list of node specific attributes;

• parameter edge_attrs

  a list of edge specific attributes;

• parameter string_of_node

  used to print nodes;

• parameter string_of_edge

  used to print edges;

• parameter channel

  where to output the graph;

• parameter formatter

  where to output the graph;

• parameter filename

  where to output the graph;

  Note: if no output parameter is provided, the graph will not be outputted. More than one output targets is OK. For example, to_dot (module G) ~filename:"graph.dot" ~channel:stdout g will output graph g into both file named "graph.dot" and standard output.

  Note: if string_of_node function is not provided, then graph nodes will be labeled with the reverse post order number.

depth_first_search (module G) ~init g. It is the most important algorithm of the Graphlib. It builds a forest of spanning trees of a graph, classifies graph edges and numbers nodes. It is a Swiss-army knife, that is very useful in implementing many other algorithms. You can think of this function as fold on steroids. But unlike fold, that accepts only one function, the depth_first_search accepts 5 different functions, that will be called on different situations, allowing you to «fill in the blanks» of your algorithm.

Although depth_first_search doesn't allow you to drive the walk itself, there're still ways to do this, using filtered function. That allows you to hide nodes or edges from the walker, thus effectively erasing them from a graph, without even touching it.

• parameter rev

  if true, then the graph g is traversed in a reverse direction. This is essentially the same, as reversing the graph, but make sure, that you've adjusted the start node.

• parameter start

  if specified, then the traverse will be started from the node that is equal to node start. Otherwise the traverse is started from the first node of a graph as returned by G.nodes, i.e., usually it is an arbitrary node.

• parameter start_tree

  node state is called on each new spanning tree started by the algorithm. If all nodes are reachable from the start node, then this function will be called only once. If all nodes of a graph are connected, then this function, will be called only once.

• parameter enter_node

  pre node state is called when a node is first discovered by the traversal. The number is a preorder number, also known as depth-first number or dfnum. All nodes are entered in a pre-order.

• parameter leave_node

  rpost node state is called when all successors of a node are left (finished). The provided number is a reverse post order number, that also defines a topological sorting order of a graph. All nodes, are left in a post order.

• parameter enter_edge

  kind edge state is called when and edge is first discovered. Edge kinds are described below. The destination of the edge may not be discovered (i.e., entered) yet. But the source is already entered (but not finished).

• parameter leave_edge

  kind edge state is called when the edge destination is at least started.

  Edges classification

  An edge in a spanning tree, produced by a depth first walk, can belong to one of the following category (kind):

  • Tree edges constitutes a spanning tree T of a graph;
  • Forward edges go from an ancestor to a descendants in a tree T;
  • Back edges go from descendants to ancestors in T, including node itself (they are also known as cycle edges).
  • Cross edges - all other edges, i.e., such edges for which doesn't go from ancestors to descendants or vice verse. They are possible since, tree defines only partial ordering.

  With respect to a pre-order and reverse post-ordering numbering the source x and a destination y of an edge with a given kind satisfy to the following inequalities:

              +---------+-----------------+---------------------+
              | Tree    | pre[x] < pre[y] | rpost[x] < rpost[y] |
              | Forward | pre[x] < pre[y] | rpost[x] < rpost[y] |
              | Back    | pre[x] ≥ pre[y] | rpost[x] ≥ rpost[y] |
              | Cross   | pre[x] > pre[y] | rpost[x] < rpost[y] |
              +---------+-----------------+---------------------+

  Note: since there can be more than one valid order of traversal of the same graph, (and thus more than one valid spanning tree), depending on a traversal the same edges can be classified differently. With the only exception, that a back edge will be always a back edge, disregarding the particular order.

  Complexity

  The algorithm is linear in time. It uses constant stack space. In fact, for small graphs it uses stack, but for large graphs dynamically switches to a heap storage. The space complexity is bounded by linear function of the graph depth.

depth_first_visit (module G) ~init visitor g allows to specify visiting functions using object. That opens space for re-usability and using open recursion.

base class with all methods defaults to nothing.

returns a sequence of nodes in reverse post order.

returns a sequence of nodes in post order

dominators (module G) g entry builds a dominators tree for a given graph.

Definition: a walk is a sequence of alternating nodes and edges, where each edge's endpoints are the preceding and following nodes in the sequence.

Definition: a node v is reachable if there exists a walk starting from entry and ending with v.

Definition: node u dominates v if u = v or if all walks from entry to v contains u.

Definition: node u strictly dominates v if it dominates v and u <> v.

Definition: node u immediately dominates v if it strictly dominates v and there is no other node that strictly dominates v and is dominated by u.

Algorithm computes a dominator tree t that has the following properties:

1. Sets of graph nodes and tree nodes are equal;
2. if node u is a parent of node v, then node u immediately dominates node v;
3. if node u is an ancestors of node v, then node u strictly dominates node v;
4. if node v is a child of node u, then node u immediately dominates node v;
5. if node v is a descendant of node u, then node u strictly dominates node v.

If every node of graph g is reachable from a provided entry node, then properties (2) - (5) are reversible, i.e., an if statement can be read as iff, and the tree is unique.

Lemma: Everything dominates unreachable block.

Proof: (by contradiction) suppose there exists a node u that doesn't dominate unreachable block v. That means, that there exists a path from entry to v that doesn't contain u. But that means, at least, that v is reachable. This is a contradiction with the original statement that v is unreachable. Qed.

If some nodes of graph g are unreachable from the provided entry node, then they are dominated by all other nodes of a graph. It means that the provided system is under constrained and has more then one solution (i.e., there exists more than one tree, that satisfies properties (1) - (5). In a current implementation each unreachable node is immediately dominated by the entry, if the entry is in graph.

To get a post-dominator tree, reverse the graph by passing true to rev and pass exit node as a starting node.

Note: although it is not imposed by the algotihm, but it is a good idea to have an entry node, that doesn't have any predecessors. Usually, this is what is silently assumed in many program analysis textbooks, but is not true in general for control-flow graphs that are reconstructed from binaries

dom_frontier (module G) g dom_tree calculates dominance frontiers for all nodes in a graph g.

strong_components (module G) g partition graph into strongly connected components. The top of each component is a root node, i.e., a node that has the least pre-order number.

shortest_path (module G) ?weight ?rev g u v Find a shortest path from node u to node v.

• parameter weight

  defines a weight of each edge. It defaults to 1.

• parameter rev

  allows to reverse graph.

is_reachable (module G) ?rev g u v is true if node v is reachable from node u in graph g. If rev is true, then it will solve the same problem but on a reversed graph.

fold_reachable (module G) ?rev ~init ~f g n applies function f to all nodes reachable from node g in graph g. If rev is true, then the graph is reversed.

For example, the following will build a set of reachable nodes: fold_reachable (module G) ~init:G.Node.Set.empty ~f:Set.add

compare (module G1) (module G2) g1 g2 compares two graphs, with different implementation but the same node type.

let module G' = filtered (module G) ?skip_node ?skip_edge () creates a new module G' that can be used at any place instead of G, but that will hide nodes and edges, for which functions skip_node and skip_edge return true.

Example:

let killed_edges = G.Edge.Hash_set.create () in
let module G = Graphlib.filtered (module G)
    ~skip_edge:(Hash_set.mem killed_edges) () in
let rec loop g () =
  (* use (module G) as normal *)
  Hash_set.add killed_edges some_edge;
  (* all edges added to [killed_edges] will no be visible *)

view (module G) ~node ~edge ~node_label ~edge_label creates a proxy module, that will transform back and forward elements of graph, using corresponding functions.

To_ocamlgraph(G) returns a module that implements OCamlGraph interface for a persistent graph.

Of_ocamlgraph(O) creates an adapter module, that implements Graphlib interface on top of the module implementing OCamlGraph interface.

functorized version of a filter function.

functorized version of Graphlib.view function.

name generation scheme

a function that gives a name for a value of type 'a

create_scheme ~next init create a name generator, that will start with init and apply next on it infinitly.

lower case symbols, starting from 'a' and moving up to 'z'. As 'z' is reached, all foregoing symbols will have a form of 'node_N' where 'N' is an increasing natural number.

numbers from zero to inifinity (Sys.max_int in fact)

empty string

empty string

Generic dot printer.