Graph view over IR.
This module implements a graph view on an intermediate representation of a subroutine. To create an instance of a graph, using existing subroutine use Sub.to_cfg. At any moment current sub term can be obtained using Sub.of_cfg function. This is a just a projection operation, so it doesn't take any computing time.
All Graph modification operations, like insert, remove and update in Node and Edge modules are mapped to corresponding Term operations. Also, for performance reasons, graph is augmented with auxiliary data structures, that performs most of the operations in O(log(N)) time.
Although this implements all operations of Graph interface it is recommended to use Term or Builder interfaces to build and modify underlying terms. The next few sections will clarify the behavior of a graph when it is modified using Graph interface. If you do not want to read the following sections, then better do not use this module to build your terms.
Inserting nodes
When node is inserted into a graph g all jumps of a node, that lead to blocks that are already in a graph will be represented as edges. Also, all jumps from other nodes to the inserted node, will be added as edges (assuming that this other nodes are also in the graph g). Thus inserting node can create an arbitrary number of edges, from zero to N. If jump target is not yet in the graph, then jump is not removed from a sequence of jumps of the inserted node, but just ignored.
Updating nodes
When node is updated with the same node (but possibly with different set of terms, see description of sameness) then all changes that affects control flow will be applied. For example, if jump is absent in a new version of a block, and this jump corresponds to an edge in the graph, then this edge will be removed.
Removing nodes
The node will be removed from the underlying sub term, and all edges incident to the removed node will be also removed. This will not affect jmp terms of blk terms.
Inserting edges
Edges in IR graph represents a transfer of a control flow between basic blocks. The basic block in IR is more reach, rather then a node in a graph. For example, in blk term the order of jumps matters. Jump n is taken, only if guard conditions of jumps 0 to n-1 evaluated to false (like switch statement in C language). The order of edges in a graph is unspecified. So, some precaution should be taken, to handle edge removing and inserting correctly. Each edge is labeled with abstract label, that represents the jump position in a graph.
When an edge is created it will look for corresponding jumps in source node. If there exists such jump, and it points to the destination, then it will be left untouched. If it points to a different node, then it will be fixed to point at the a given destination. If there is no position in a slot, represented by the a given label, then it will be inserted. Dummy jumps will be prepended before the inserted jump, if needed.
When an edge is inserted into the graph, then source and destination nodes are inserted or updated (depending on whether they were already present in the graph). As a result, the graph must contain at least nodes, incident to the edge, and the edge itself.
Updating edge
Updating an edge is basically the same, as updating incident nodes, a given that the edge exists in the graph.
Removing edge
Removing an edge is not symmetric with edge insertion. It doesn't remove the incident nodes, but instead removes jumps from the source node to destination. The jumps are removed accurately, so that the order (and semantics) is preserved. If the removed jump was in the middle of the sequence then it is substituted by a dummy jump with false guard.
module Edge : sig ... endsince in IR the order of edges defines semantics, we provide extra functions
module Node : sig ... endinclude Graphlib.Std.Graph
with type t := t
and type node := node
and type edge := edge
and type Node.label = blk term
and module Node := Node
and module Edge := Edge
nodes g returns all nodes of graph g in an unspecified order
edges g returns all edges of graph g in an unspecified order
is_directed is true if graph is a directed graph.
val number_of_edges : t -> intnumber_of_edges g returns the size of a graph g.
val number_of_nodes : t -> intnumber_of_nodes g returns the order of a graph g
All graphs provides a common interface for any opaque data structure
include Regular.Std.Opaque.S with type t := t
include Core_kernel.Comparable.S with type t := t
include Base.Comparable.S with type t := t
val ascending : t -> t -> intascending is identical to compare. descending x y = ascending y x. These are intended to be mnemonic when used like List.sort ~compare:ascending and List.sort
~cmp:descending, since they cause the list to be sorted in ascending or descending order, respectively.
val descending : t -> t -> intval between : t -> low:t -> high:t -> boolbetween t ~low ~high means low <= t <= high
val clamp_exn : t -> min:t -> max:t -> tclamp_exn t ~min ~max returns t', the closest value to t such that between t' ~low:min ~high:max is true.
Raises if not (min <= max).
All graphs are printable.
include Regular.Std.Printable.S with type t := t
val to_string : t -> stringto_string x returns a human-readable representation of x
val str : unit -> t -> stringstr () t is formatted output function that matches "%a" conversion format specifier in functions, that prints to string, e.g., sprintf, failwithf, errorf and, surprisingly all Lwt printing function, including Lwt_io.printf and logging (or any other function with type ('a,unit,string,...) formatN`. Example:
Or_error.errorf "type %a is not valid for %a"
Type.str ty Exp.str exp
val pps : unit -> t -> stringwill print to a standard output_channel, useful for using in printf, fprintf, etc.
prints a sequence of values of type t
this will include pp function from Core that has type t printer, and can be used in Format.printf family of functions
include Core_kernel.Pretty_printer.S with type t := t