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
val nodes : t -> node Regular.Std.seqval edges : t -> edge Regular.Std.seqval number_of_edges : t -> intval number_of_nodes : t -> intval (>=) : t -> t -> boolval (<=) : t -> t -> boolval (<>) : t -> t -> boolval equal : t -> t -> boolval ascending : t -> t -> intval descending : t -> t -> intval between : t -> low:t -> high:t -> boolval clamp_exn : t -> min:t -> max:t -> tval clamp : t -> min:t -> max:t -> t Core_kernel.Or_error.tval validate_lbound :
min:t Core_kernel.Maybe_bound.t ->
t Core_kernel.Validate.checkval validate_ubound :
max:t Core_kernel.Maybe_bound.t ->
t Core_kernel.Validate.checkval validate_bound :
min:t Core_kernel.Maybe_bound.t ->
max:t Core_kernel.Maybe_bound.t ->
t Core_kernel.Validate.checkval compare : t -> t -> intval hashable : t Core_kernel.Std.Hashable.Hashtbl.Hashable.tmodule Table : sig ... endval to_string : t -> stringval str : unit -> t -> stringval pps : unit -> t -> stringval ppo : Core_kernel.Std.out_channel -> t -> unitval pp_seq : Format.formatter -> t Core_kernel.Std.Sequence.t -> unitval pp : Format.formatter -> t -> unit