Construction and coloring of the interference graph.

Two registers interfere if there exists a program point where they are both simultaneously live, and it is possible that they contain different values at this program point. Consequently, two registers that do not interfere can be merged into one register while preserving the program behavior: there is no program point where this merged register would have to hold two different values (for the two original registers), so to speak. The simplified algorithm for constructing the interference graph from the results of the liveness analysis is as follows:

     start with empty interference graph
     for each parameter p and register r live at the function entry point:
         add conflict edge p <-> r 
     for each instruction I in function:
         let L be the live registers "after" I
         if I is a "move" instruction  dst <- src, and dst is live:
            add conflict edges dst <-> r for each r in L \ {dst, src}
         else if I is an instruction with result dst, and dst is live:
            add conflict edges dst <-> r for each r in L \ {dst};
         if I is a "call" instruction dst <- f(args),
            add conflict edges between all pseudo-registers in L \ {dst}
            and all caller-save machine registers
     done

Notice that edges are added only when a register becomes live. A register becomes live either if it is the result of an operation (and is live afterwards), or if we are at the function entrance and the register is a function parameter. For two registers to be simultaneously live at some program point, it must be the case that one becomes live at a point where the other is already live. Hence, it suffices to add interference edges between registers that become live at some instruction and registers that are already live at this instruction. Notice also the special treatment of ``move'' instructions: since the destination register of the ``move'' is assigned the same value as the source register, it is semantically correct to assign the destination and the source registers to the same register, even if the source register remains live afterwards. (This is even desirable, since the ``move'' instruction can then be eliminated.) Thus, no interference is added between the source and the destination of a ``move'' instruction. Finally, for ``call'' instructions, we must make sure that pseudo-registers live across the instruction are allocated to callee-save machine register or to stack slots, but never to caller-save machine registers (these lose their values across the call). We therefore add the corresponding conflict edges between pseudo-registers live across and caller-save machine registers (pairwise). The full algorithm is similar to the simplified algorithm above, but records preference edges in addition to conflict edges. Preference edges guide the graph coloring algorithm by telling it that better code will be obtained eventually if it is possible to allocate certain pseudo-registers to the same location or to a given machine register. Preference edges are added:

• between the destination and source pseudo-registers of a ``move'' instruction;
• between the arguments of a ``call'' instruction and the locations of the arguments as dictated by the calling conventions;
• between the result of a ``call'' instruction and the location of the result as dictated by the calling conventions.

The actual coloring of the graph is performed by a function written directly in Caml, and not proved correct in any way. This function takes as argument the RTL function, the interference graph for this function, an assignment of types to RTL pseudo-registers, and the set of all RTL pseudo-registers mentioned in the interference graph. It returns the coloring as a function from pseudo-registers to locations.

To ensure that the result of graph_coloring is a correct coloring, we check a posteriori its result using the following Coq functions. Let coloring be the function reg -> loc returned by graph_coloring. The three properties checked are:

• coloring r1 <> coloring r2 if there is a conflict edge between r1 and r2 in the interference graph.
• coloring r1 <> R m2 if there is a conflict edge between pseudo-register r1 and machine register m2 in the interference graph.
• For all r mentioned in the interference graph, the location coloring r is acceptable and has the same type as r.

To preserve decidability of checking, the checks (especially the third one) are performed for the pseudo-registers mentioned in the interference graph. To facilitate the proofs, it is convenient to ensure that the properties hold for all pseudo-registers. To this end, we ``clip'' the candidate coloring returned by graph_coloring: the final coloring behave identically over pseudo-registers mentioned in the interference graph, but returns a dummy machine register of the correct type otherwise.

The following function combines the phases described above: construction of the interference graph, coloring by untrusted Caml code, checking of the candidate coloring returned, and adjustment of this coloring. If the coloring candidate is incorrect, None is returned, causing register allocation to fail.