Library Coloringproof

Correctness of graph coloring.





Require Import SetoidList.

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.

Require Import Coloring.

Correctness of the interference graph

We show that the interference graph built by interf_graph is correct in the sense that it contains all conflict edges that we need.

Many boring lemmas on the auxiliary functions used to construct the interference graph follow. The lemmas are of two kinds: the ``increasing'' lemmas show that the auxiliary functions only add edges to the interference graph, but do not remove existing edges; and the ``correct'' lemmas show that the auxiliary functions correctly add the edges that we'd like them to add.





Lemma graph_incl_refl:

  forall g, graph_incl g g.






Lemma add_interf_live_incl_aux:

  forall (filter: reg -> bool) res live g,

  graph_incl g

    (List.fold_left

      (fun g r => if filter r then add_interf r res g else g)

      live g).






Lemma add_interf_live_incl:

  forall (filter: reg -> bool) res live g,

  graph_incl g (add_interf_live filter res live g).






Lemma add_interf_live_correct_aux:

  forall filter res r live,

  InA Regset.E.eq r live -> filter r = true ->

  forall g,

  interfere r res

    (List.fold_left

      (fun g r => if filter r then add_interf r res g else g)

      live g).






Lemma add_interf_live_correct:

  forall filter res live g r,

  Regset.In r live ->

  filter r = true ->

  interfere r res (add_interf_live filter res live g).






Lemma add_interf_op_incl: 

  forall res live g,

  graph_incl g (add_interf_op res live g).






Lemma add_interf_op_correct:

  forall res live g r,

  Regset.In r live ->

  r <> res ->

  interfere r res (add_interf_op res live g).






Lemma add_interf_move_incl: 

  forall arg res live g,

  graph_incl g (add_interf_move arg res live g).






Lemma add_interf_move_correct:

  forall arg res live g r,

  Regset.In r live ->

  r <> arg -> r <> res ->

  interfere r res (add_interf_move arg res live g).






Lemma add_interf_destroyed_incl_aux_1:

  forall mr live g,

  graph_incl g

    (List.fold_left (fun g r => add_interf_mreg r mr g) live g).






Lemma add_interf_destroyed_incl_aux_2:

  forall mr live g,

  graph_incl g

    (Regset.fold (fun r g => add_interf_mreg r mr g) live g).






Lemma add_interf_destroyed_incl:

  forall live destroyed g,

  graph_incl g (add_interf_destroyed live destroyed g).






Lemma add_interfs_indirect_call_incl:

  forall rfun locs g,

  graph_incl g (add_interfs_indirect_call rfun locs g).






Lemma add_interfs_call_incl:

  forall ros locs g,

  graph_incl g (add_interf_call ros locs g).






Lemma interfere_incl:

  forall r1 r2 g1 g2,

  graph_incl g1 g2 ->

  interfere r1 r2 g1 ->

  interfere r1 r2 g2.






Lemma interfere_mreg_incl:

  forall r1 r2 g1 g2,

  graph_incl g1 g2 ->

  interfere_mreg r1 r2 g1 ->

  interfere_mreg r1 r2 g2.






Lemma add_interf_destroyed_correct_aux_1:

  forall mr r live,

  InA Regset.E.eq r live ->

  forall g,

  interfere_mreg r mr

    (List.fold_left (fun g r => add_interf_mreg r mr g) live g).






Lemma add_interf_destroyed_correct_aux_2:

  forall mr live g r,

  Regset.In r live ->

  interfere_mreg r mr

    (Regset.fold (fun r g => add_interf_mreg r mr g) live g).






Lemma add_interf_destroyed_correct:

  forall live destroyed g r mr,

  Regset.In r live ->

  In mr destroyed ->

  interfere_mreg r mr (add_interf_destroyed live destroyed g).






Lemma add_interfs_indirect_call_correct:

  forall rfun mr locs g,

  In (R mr) locs ->

  interfere_mreg rfun mr (add_interfs_indirect_call rfun locs g).






Lemma add_interfs_call_correct:

  forall rfun locs g mr,

  In (R mr) locs -> 

  interfere_mreg rfun mr (add_interf_call (inl _ rfun) locs g).






Lemma add_prefs_call_incl:

  forall args locs g,

  graph_incl g (add_prefs_call args locs g).






Lemma add_interf_entry_incl:

  forall params live g,

  graph_incl g (add_interf_entry params live g).






Lemma add_interf_entry_correct:

  forall params live g r1 r2,

  In r1 params ->

  Regset.In r2 live ->

  r1 <> r2 ->

  interfere r1 r2 (add_interf_entry params live g).






Lemma add_interf_params_incl_aux:

  forall p1 pl g,

  graph_incl g

   (List.fold_left

      (fun g r => if Reg.eq r p1 then g else add_interf r p1 g)

      pl g).






Lemma add_interf_params_incl:

  forall pl g,

  graph_incl g (add_interf_params pl g).






Lemma add_interf_params_correct_aux:

  forall p1 pl g p2,

  In p2 pl ->

  p1 <> p2 ->

  interfere p1 p2

   (List.fold_left

      (fun g r => if Reg.eq r p1 then g else add_interf r p1 g)

      pl g).






Lemma add_interf_params_correct:

  forall pl g r1 r2,

  In r1 pl -> In r2 pl -> r1 <> r2 ->

  interfere r1 r2 (add_interf_params pl g).






Lemma add_edges_instr_incl:

  forall sig instr live g,

  graph_incl g (add_edges_instr sig instr live g).

The proposition below states that graph g contains all the conflict edges expected for instruction instr.





Definition correct_interf_instr

    (live: Regset.t) (instr: instruction) (g: graph) : Prop :=

  match instr with

  | Iop op args res s =>

      match is_move_operation op args with

      | Some arg =>

          forall r,

          Regset.In res live ->

          Regset.In r live ->

          r <> res -> r <> arg -> interfere r res g

      | None =>

          forall r,

          Regset.In res live ->

          Regset.In r live ->

          r <> res -> interfere r res g

      end

  | Iload chunk addr args res s =>

      forall r,

      Regset.In res live ->

      Regset.In r live ->

      r <> res -> interfere r res g

  | Icall sig ros args res s =>

      (forall r mr,

        Regset.In r live ->

        In mr destroyed_at_call_regs ->

        r <> res ->

        interfere_mreg r mr g)

   /\ (forall r,

        Regset.In r live ->

       r <> res -> interfere r res g)

   /\ (match ros with

       | inl rfun => forall mr, In (R mr) (loc_arguments sig) -> 

                                interfere_mreg rfun mr g

       | inr idfun => True

       end)

  | Itailcall sig ros args =>

      match ros with

        | inl rfun => forall mr, In (R mr) (loc_arguments sig) -> 

                                 interfere_mreg rfun mr g

        | inr idfun => True

      end

  | _ =>

      True

  end.




Lemma correct_interf_instr_incl:

  forall live instr g1 g2,

  graph_incl g1 g2 ->

  correct_interf_instr live instr g1 ->

  correct_interf_instr live instr g2.






Lemma add_edges_instr_correct:

  forall sig instr live g,

  correct_interf_instr live instr (add_edges_instr sig instr live g).






Lemma add_edges_instrs_incl_aux:

  forall sig live instrs g,

  graph_incl g

    (fold_left

       (fun (a : graph) (p : positive * instruction) =>

          add_edges_instr sig (snd p) live !! (fst p) a)

       instrs g).






Lemma add_edges_instrs_correct_aux:

  forall sig live instrs g pc i,

  In (pc, i) instrs ->

  correct_interf_instr live!!pc i

    (fold_left

       (fun (a : graph) (p : positive * instruction) =>

          add_edges_instr sig (snd p) live !! (fst p) a)

       instrs g).






Lemma add_edges_instrs_correct:

  forall f live pc i,

  f.(fn_code)!pc = Some i ->

  correct_interf_instr live!!pc i (add_edges_instrs f live).

Here are the three correctness properties of the generated inference graph. First, it contains the conflict edges needed by every instruction of the function.





Lemma interf_graph_correct_1:

  forall f live live0 pc i,

  f.(fn_code)!pc = Some i ->

  correct_interf_instr live!!pc i (interf_graph f live live0).

Second, function parameters conflict pairwise.





Lemma interf_graph_correct_2:

  forall f live live0 r1 r2,

  In r1 f.(fn_params) ->

  In r2 f.(fn_params) ->

  r1 <> r2 ->

  interfere r1 r2 (interf_graph f live live0).

Third, function parameters conflict pairwise with pseudo-registers live at function entry. If the function never uses a pseudo-register before it is defined, pseudo-registers live at function entry are a subset of the function parameters and therefore this condition is implied by interf_graph_correct_3. However, we prefer not to make this assumption.





Lemma interf_graph_correct_3:

  forall f live live0 r1 r2,

  In r1 f.(fn_params) ->

  Regset.In r2 live0 ->

  r1 <> r2 ->

  interfere r1 r2 (interf_graph f live live0).

Correctness of the a priori checks over the result of graph coloring

We now show that the checks performed over the candidate coloring returned by graph_coloring are correct: candidate colorings that pass these checks are indeed correct colorings.





Section CORRECT_COLORING.




Variable g: graph.

Variable env: regenv.

Variable allregs: Regset.t.

Variable coloring: reg -> loc.




Lemma check_coloring_1_correct:

  forall r1 r2,

  check_coloring_1 g coloring = true ->

  SetRegReg.In (r1, r2) g.(interf_reg_reg) ->

  coloring r1 <> coloring r2.






Lemma check_coloring_2_correct:

  forall r1 mr2,

  check_coloring_2 g coloring = true ->

  SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) ->

  coloring r1 <> R mr2.






Lemma same_typ_correct:

  forall t1 t2, same_typ t1 t2 = true -> t1 = t2.






Lemma loc_is_acceptable_correct:

  forall l, loc_is_acceptable l = true -> loc_acceptable l.






Lemma check_coloring_3_correct:

  forall r,

  check_coloring_3 allregs env coloring = true ->

  Regset.mem r allregs = true ->

  loc_acceptable (coloring r) /\ env r = Loc.type (coloring r).






End CORRECT_COLORING.

Correctness of clipping

We then show the correctness of the ``clipped'' coloring returned by alloc_of_coloring applied to a candidate coloring that passes the a posteriori checks.





Section ALLOC_OF_COLORING.




Variable g: graph.

Variable env: regenv.

Let allregs := all_interf_regs g.

Variable coloring: reg -> loc.

Let alloc := alloc_of_coloring coloring env allregs.




Lemma alloc_of_coloring_correct_1:

  forall r1 r2,

  check_coloring g env allregs coloring = true ->

  SetRegReg.In (r1, r2) g.(interf_reg_reg) ->

  alloc r1 <> alloc r2.






Lemma alloc_of_coloring_correct_2:

  forall r1 mr2,

  check_coloring g env allregs coloring = true ->

  SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) ->

  alloc r1 <> R mr2.






Lemma alloc_of_coloring_correct_3:

  forall r,

  check_coloring g env allregs coloring = true ->

  loc_acceptable (alloc r).






Lemma alloc_of_coloring_correct_4:

  forall r,

  check_coloring g env allregs coloring = true ->

  env r = Loc.type (alloc r).






End ALLOC_OF_COLORING.

Correctness of the whole graph coloring algorithm

Combining results from the previous sections, we now summarize the correctness properties of the assignment (of locations to registers) returned by regalloc.





Definition correct_alloc_instr

    (live: PMap.t Regset.t) (alloc: reg -> loc) 

    (pc: node) (instr: instruction) : Prop :=

  match instr with

  | Iop op args res s =>

      match is_move_operation op args with

      | Some arg =>

          forall r,

          Regset.In res live!!pc ->

          Regset.In r live!!pc ->

          r <> res -> r <> arg -> alloc r <> alloc res

      | None =>

          forall r,

          Regset.In res live!!pc ->

          Regset.In r live!!pc ->

          r <> res -> alloc r <> alloc res

      end

  | Iload chunk addr args res s =>

      forall r,

      Regset.In res live!!pc ->

      Regset.In r live!!pc ->

      r <> res -> alloc r <> alloc res

  | Icall sig ros args res s =>

      (forall r,

        Regset.In r live!!pc ->

        r <> res ->

        ~(In (alloc r) Conventions.destroyed_at_call))

   /\ (forall r,

        Regset.In r live!!pc ->

        r <> res -> alloc r <> alloc res)

   /\ (match ros with

        | inl rfun => ~(In (alloc rfun) (loc_arguments sig))

        | inr idfun => True

        end)

  | Itailcall sig ros args =>

      (match ros with

        | inl rfun => ~(In (alloc rfun) (loc_arguments sig))

        | inr idfun => True

        end)

  | _ =>

      True

  end.




Section REGALLOC_PROPERTIES.




Variable f: function.

Variable env: regenv.

Variable live: PMap.t Regset.t.

Variable live0: Regset.t.

Variable alloc: reg -> loc.




Let g := interf_graph f live live0.

Let allregs := all_interf_regs g.

Let coloring := graph_coloring f g env allregs.




Lemma regalloc_ok:

  regalloc f live live0 env = Some alloc ->

  check_coloring g env allregs coloring = true /\

  alloc = alloc_of_coloring coloring env allregs.






Lemma regalloc_acceptable:

  forall r,

  regalloc f live live0 env = Some alloc ->

  loc_acceptable (alloc r).






Lemma regsalloc_acceptable:

  forall rl,

  regalloc f live live0 env = Some alloc ->

  locs_acceptable (List.map alloc rl).






Lemma regalloc_preserves_types:

  forall r,

  regalloc f live live0 env = Some alloc ->

  Loc.type (alloc r) = env r.






Lemma correct_interf_alloc_instr:

  forall pc instr,

  (forall r1 r2, interfere r1 r2 g -> alloc r1 <> alloc r2) ->

  (forall r1 mr2, interfere_mreg r1 mr2 g -> alloc r1 <> R mr2) ->

  (forall r, loc_acceptable (alloc r)) ->

  correct_interf_instr live!!pc instr g ->

  correct_alloc_instr live alloc pc instr.






Lemma regalloc_correct_1:

  forall pc instr,

  regalloc f live live0 env = Some alloc ->

  f.(fn_code)!pc = Some instr ->

  correct_alloc_instr live alloc pc instr.






Lemma regalloc_correct_2:

  regalloc f live live0 env = Some alloc ->

  list_norepet f.(fn_params) ->

  list_norepet (List.map alloc f.(fn_params)).






Lemma regalloc_correct_3:

  forall r1 r2,

  regalloc f live live0 env = Some alloc ->

  In r1 f.(fn_params) ->

  Regset.In r2 live0 ->

  r1 <> r2 ->

  alloc r1 <> alloc r2.






End REGALLOC_PROPERTIES.