path: root/backend/Coloring.v

(** Construction and coloring of the interference graph. *)

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import RTLtyping.
Require Import Locations.
Require Import Conventions.
Require Import InterfGraph.

(** * Construction 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.
*)

Definition add_interf_live
    (filter: reg -> bool) (res: reg) (live: Regset.t) (g: graph): graph :=
  Regset.fold
    (fun g r => if filter r then add_interf r res g else g) live g.

Definition add_interf_op
    (res: reg) (live: Regset.t) (g: graph): graph :=
  add_interf_live
    (fun r => if Reg.eq r res then false else true)
    res live g.

Definition add_interf_move
    (arg res: reg) (live: Regset.t) (g: graph): graph :=
  add_interf_live
    (fun r =>
       if Reg.eq r res then false else
       if Reg.eq r arg then false else true)
    res live g.

Definition add_interf_call
    (live: Regset.t) (destroyed: list mreg) (g: graph): graph :=
  List.fold_left
    (fun g mr => Regset.fold (fun g r => add_interf_mreg r mr g) live g)
    destroyed g.

Fixpoint add_prefs_call
    (args: list reg) (locs: list loc) (g: graph) {struct args} : graph :=
  match args, locs with
  | a1 :: al, l1 :: ll =>
      add_prefs_call al ll
        (match l1 with R mr => add_pref_mreg a1 mr g | _ => g end)
  | _, _ => g
  end.

Definition add_interf_entry
    (params: list reg) (live: Regset.t) (g: graph): graph :=
  List.fold_left (fun g r => add_interf_op r live g) params g.

Fixpoint add_interf_params
    (params: list reg) (g: graph) {struct params}: graph :=
  match params with
  | nil => g
  | p1 :: pl =>
      add_interf_params pl
        (List.fold_left
          (fun g r => if Reg.eq r p1 then g else add_interf r p1 g)
          pl g)
  end.

Definition add_edges_instr
    (sig: signature) (i: instruction) (live: Regset.t) (g: graph) : graph :=
  match i with
  | Iop op args res s =>
      if Regset.mem res live then
        match is_move_operation op args with
        | Some arg =>
            add_pref arg res (add_interf_move arg res live g)
        | None =>
            add_interf_op res live g
        end
      else g
  | Iload chunk addr args dst s =>
      if Regset.mem dst live
      then add_interf_op dst live g
      else g
  | Icall sig ros args res s =>
      add_prefs_call args (loc_arguments sig)
        (add_pref_mreg res (loc_result sig)
          (add_interf_op res live
            (add_interf_call
              (Regset.remove res live) destroyed_at_call_regs g)))
  | Ialloc arg res s =>
      add_pref_mreg arg loc_alloc_argument
        (add_pref_mreg res loc_alloc_result
          (add_interf_op res live
            (add_interf_call
              (Regset.remove res live) destroyed_at_call_regs g)))
  | Ireturn (Some r) =>
      add_pref_mreg r (loc_result sig) g
  | _ => g
  end.

Definition add_edges_instrs (f: function) (live: PMap.t Regset.t) : graph :=
  PTree.fold
    (fun g pc i => add_edges_instr f.(fn_sig) i live!!pc g)
    f.(fn_code)
    empty_graph.

Definition interf_graph (f: function) (live: PMap.t Regset.t) (live0: Regset.t) :=
  add_prefs_call f.(fn_params) (loc_parameters f.(fn_sig))
    (add_interf_params f.(fn_params)
      (add_interf_entry f.(fn_params) live0
        (add_edges_instrs f live))).

(** * Graph coloring *)

(** 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. *)

Parameter graph_coloring: 
  function -> graph -> regenv -> Regset.t -> (reg -> loc).

(** 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].
*)

Definition check_coloring_1 (g: graph) (coloring: reg -> loc) :=
  SetRegReg.for_all 
    (fun r1r2 =>
      if Loc.eq (coloring (fst r1r2)) (coloring (snd r1r2)) then false else true)
    g.(interf_reg_reg).

Definition check_coloring_2 (g: graph) (coloring: reg -> loc) :=
  SetRegMreg.for_all 
    (fun r1mr2 =>
      if Loc.eq (coloring (fst r1mr2)) (R (snd r1mr2)) then false else true)
    g.(interf_reg_mreg).

Definition same_typ (t1 t2: typ) :=
  match t1, t2 with
  | Tint, Tint => true
  | Tfloat, Tfloat => true
  | _, _ => false
  end.

Definition loc_is_acceptable (l: loc) :=
  match l with
  | R r => 
     if In_dec Loc.eq l temporaries then false else true
  | S (Local ofs ty) =>
     if zlt ofs 0 then false else true
  | _ =>
     false
  end.

Definition check_coloring_3 (rs: Regset.t) (env: regenv) (coloring: reg -> loc) :=
  Regset.for_all
    (fun r =>
      let l := coloring r in
      andb (loc_is_acceptable l) (same_typ (env r) (Loc.type l)))
    rs.

Definition check_coloring
       (g: graph) (env: regenv) (rs: Regset.t) (coloring: reg -> loc) :=
  andb (check_coloring_1 g coloring)
       (andb (check_coloring_2 g coloring)
             (check_coloring_3 rs env coloring)).

(** 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. *)

Definition alloc_of_coloring (coloring: reg -> loc) (env: regenv) (rs: Regset.t) :=
  fun r =>
    if Regset.mem r rs
    then coloring r
    else match env r with Tint => R R3 | Tfloat => R F1 end.

(** * Coloring of the interference graph *)

(** 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. *)

Definition regalloc
    (f: function) (live: PMap.t Regset.t) (live0: Regset.t) (env: regenv) :=
  let g := interf_graph f live live0 in
  let rs := all_interf_regs g in
  let coloring := graph_coloring f g env rs in
  if check_coloring g env rs coloring
  then Some (alloc_of_coloring coloring env rs)
  else None.