Module Containers.GraphSig

A simple graph library to represent control-flow graphs.

We actually use an oriented hyper-graph structure: an edge connects a set of (source) nodes to a set of (destination) nodes. Equivalently, this can be seen as a bipartite graph where nodes and edges correspond to the two node partitions.

Nodes model program locations, where an invariant can be stored. Edges model transfer functions for basic blocks. An edge can have several source nodes, to model control-flow joins at the entry of basic blocks. It is also possible to model joins by having several edges incoming into the same node. An edge can have several destination nodes, to model conditionals with several outputs from a basic block. Alternatively, several edges outgoing from the same node can be used to model conditionals. We use "ports" to distinguish and classify between the different source and destination nodes of an edge. Ports carry tags. It is possible to have a node connected to the same edge several times, either on equal or different ports.

Nodes and edges have unique identifiers, ordered to serve as map keys. Each node and edge has a mutable data field of polymorphic type. However, data attached to nodes and edges can also be maintained outside of the graph structure, using hash-tables or maps from identifiers to the actual data.

Graphs are mutable to make it easier to construct them. It is expected that, after creation in the front-end, graphs remain unmodified (except maybe for the data fields).

Ordered, hashable data types

Nested lists

Nested lists of nodes are used to represent herarchical decompositions into strongly connected components.

Parameter signature

Graph signature