Theory IRNodes
section ‹Graph Representation›
subsection ‹IR Graph Nodes›
theory IRNodes
imports
Values
begin
text ‹
The GraalVM IR is represented using a graph data structure.
Here we define the nodes that are contained within the graph.
Each node represents a Node subclass in the GraalVM compiler,
the node classes have annotated fields to indicate input and successor edges.
We represent these classes with each IRNode constructor explicitly labelling
a reference to the node IDs that it stores as inputs and successors.
The inputs\_of and successors\_of functions partition those labelled references
into input edges and successor edges of a node.
To identify each Node, we use a simple natural number index.
Zero is always the start node in a graph.
For human readability, within nodes we write
INPUT (or special case thereof) instead of ID for input edges, and
SUCC instead of ID for control-flow successor edges.
Optional edges are handled as "INPUT option" etc.
›