package graphlib

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

Generic Graph Library

module Make (Node : Regular.Std.Opaque.S) (Edge : Core_kernel.Std.T) : Graph with type node = Node.t and type Node.label = Node.t and type Edge.label = Edge.t

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

module Labeled (Node : Regular.Std.Opaque.S) (NL : Core_kernel.Std.T) (EL : Core_kernel.Std.T) : Graph with type node = (Node.t, NL.t) labeled and type Node.label = (Node.t, NL.t) labeled and type Edge.label = EL.t

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

val create : (module Graph with type t = 'c and type Edge.label = 'b and type Node.label = 'a) -> ?nodes:'a list -> ?edges:('a * 'a * 'b) list -> unit -> 'c

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] ()
val union : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> 'c -> 'c -> 'c

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).
val inter : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> 'c -> 'c -> 'c

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).
val to_dot : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> ?graph_attrs:('c -> graph_attr list) -> ?node_attrs:('n -> node_attr list) -> ?edge_attrs:('e -> edge_attr list) -> ?string_of_node:('n -> string) -> ?string_of_edge:('e -> string) -> ?channel:Core_kernel.Std.out_channel -> ?formatter:Format.formatter -> ?filename:string -> 'c -> unit

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.

val depth_first_visit : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> ?rev:bool -> ?start:'n -> 'c -> init:'s -> ('n, 'e, 's) dfs_visitor -> 's

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.

class ['n, 'e, 's] dfs_identity_visitor : ['n, 'e, 's] dfs_visitor

base class with all methods defaults to nothing.

val reverse_postorder_traverse : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> ?rev:bool -> ?start:'n -> 'c -> 'n Regular.Std.seq

returns a sequence of nodes in reverse post order.

val postorder_traverse : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> ?rev:bool -> ?start:'n -> 'c -> 'n Regular.Std.seq

returns a sequence of nodes in post order

val dominators : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> ?rev:bool -> 'c -> 'n -> 'n tree

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

val dom_frontier : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> ?rev:bool -> 'c -> 'n tree -> 'n frontier

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

val strong_components : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> 'c -> 'n partition

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.

val shortest_path : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> ?weight:('e -> int) -> ?rev:bool -> 'c -> 'n -> 'n -> 'e path option

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.

val is_reachable : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> ?rev:bool -> 'c -> 'n -> 'n -> bool

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.

val fold_reachable : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> ?rev:bool -> init:'a -> f:('a -> 'n -> 'a) -> 'c -> 'n -> 'a

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

val compare : (module Graph with type node = 'n and type t = 'a) -> (module Graph with type node = 'n and type t = 'b) -> 'a -> 'b -> int

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

val filtered : (module Graph with type edge = 'e and type node = 'n and type t = 'c) -> ?skip_node:('n -> bool) -> ?skip_edge:('e -> bool) -> unit -> (module Graph with type edge = 'e and type node = 'n and type t = 'c)

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 *)
val view : (module Graph with type edge = 'e and type node = 'n and type t = 'c and type Edge.label = 'b and type Node.label = 'a) -> node:(('n -> 'f) * ('f -> 'n)) -> edge:(('e -> 'd) * ('d -> 'e)) -> node_label:(('a -> 'p) * ('p -> 'a)) -> edge_label:(('b -> 'r) * ('r -> 'b)) -> (module Graph with type edge = 'd and type node = 'f and type t = 'c and type Edge.label = 'r and type Node.label = 'p)

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.

module To_ocamlgraph (G : Graph) : Graph.Sig.P with type t = G.t and type V.t = G.node and type E.t = G.edge and type V.label = G.Node.label and type E.label = G.Edge.label

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

module Of_ocamlgraph (G : Graph.Sig.P) : Graph with type t = G.t and type node = G.V.t and type edge = G.E.t and type Node.label = G.V.label and type Edge.label = G.E.label

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

module Filtered (G : Graph) (P : Predicate with type node = G.node and type edge = G.edge) : Graph with type t = G.t and type node = G.node and type edge = G.edge and module Node = G.Node and module Edge = G.Edge

functorized version of a filter function.

module Mapper (G : Graph) (N : Isomorphism with type s = G.node) (E : Isomorphism with type s = G.edge) (NL : Isomorphism with type s = G.Node.label) (EL : Isomorphism with type s = G.Edge.label) : Graph with type t = G.t and type node = N.t and type edge = E.t and type Node.label = NL.t and type Edge.label = EL.t

functorized version of Graphlib.view function.

type scheme

name generation scheme

type 'a symbolizer = 'a -> string

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

val create_scheme : next:(string -> string) -> string -> scheme

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

val symbols : scheme

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.

val numbers : scheme

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

empty string

val nothing : scheme

empty string

val by_given_order : scheme -> ('a -> 'a -> int) -> 'a Core_kernel.Std.Sequence.t -> 'a symbolizer
val by_natural_order : scheme -> ('a -> 'a -> int) -> 'a Core_kernel.Std.Sequence.t -> 'a symbolizer
module Dot : sig ... end

Generic dot printer.

OCaml

Innovation. Community. Security.