diff options
Diffstat (limited to 'backend/InterfGraph.v')
| -rw-r--r-- | backend/InterfGraph.v | 302 |
1 files changed, 0 insertions, 302 deletions
diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v deleted file mode 100644 index 877c7c6..0000000 --- a/backend/InterfGraph.v +++ /dev/null @@ -1,302 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Representation of interference graphs for register allocation. *) - -Require Import Coqlib. -Require Import FSets. -Require Import FSetAVL. -Require Import Ordered. -Require Import Registers. -Require Import Locations. - -(** Interference graphs are undirected graphs with two kinds of nodes: -- RTL pseudo-registers; -- Machine registers. - -and four kind of edges: -- Conflict edges between two pseudo-registers. - (Meaning: these two pseudo-registers must not be assigned the same - location.) -- Conflict edges between a pseudo-register and a machine register - (Meaning: this pseudo-register must not be assigned this machine - register.) -- Preference edges between two pseudo-registers. - (Meaning: the generated code would be more efficient if those two - pseudo-registers were assigned the same location, but if this is not - possible, the generated code will still be correct.) -- Preference edges between a pseudo-register and a machine register - (Meaning: the generated code would be more efficient if this - pseudo-register was assigned this machine register, but if this is not - possible, the generated code will still be correct.) - -A graph is represented by four finite sets of edges (one of each kind -above). An edge is represented by a pair of two pseudo-registers or -a pair (pseudo-register, machine register). -In the case of two pseudo-registers ([r1], [r2]), we adopt the convention -that [r1] <= [r2], so as to reflect the undirected nature of the edge. -*) - -Module OrderedReg <: OrderedType with Definition t := reg := OrderedPositive. -Module OrderedRegReg := OrderedPair(OrderedReg)(OrderedReg). -Module OrderedMreg := OrderedIndexed(IndexedMreg). -Module OrderedRegMreg := OrderedPair(OrderedReg)(OrderedMreg). - -Module SetRegReg := FSetAVL.Make(OrderedRegReg). -Module SetRegMreg := FSetAVL.Make(OrderedRegMreg). - -Record graph: Type := mkgraph { - interf_reg_reg: SetRegReg.t; - interf_reg_mreg: SetRegMreg.t; - pref_reg_reg: SetRegReg.t; - pref_reg_mreg: SetRegMreg.t -}. - -Definition empty_graph := - mkgraph SetRegReg.empty SetRegMreg.empty - SetRegReg.empty SetRegMreg.empty. - -(** The following functions add a new edge (if not already present) - to the given graph. *) - -Definition ordered_pair (x y: reg) := - if plt x y then (x, y) else (y, x). - -Definition add_interf (x y: reg) (g: graph) := - mkgraph (SetRegReg.add (ordered_pair x y) g.(interf_reg_reg)) - g.(interf_reg_mreg) - g.(pref_reg_reg) - g.(pref_reg_mreg). - -Definition add_interf_mreg (x: reg) (y: mreg) (g: graph) := - mkgraph g.(interf_reg_reg) - (SetRegMreg.add (x, y) g.(interf_reg_mreg)) - g.(pref_reg_reg) - g.(pref_reg_mreg). - -Definition add_pref (x y: reg) (g: graph) := - mkgraph g.(interf_reg_reg) - g.(interf_reg_mreg) - (SetRegReg.add (ordered_pair x y) g.(pref_reg_reg)) - g.(pref_reg_mreg). - -Definition add_pref_mreg (x: reg) (y: mreg) (g: graph) := - mkgraph g.(interf_reg_reg) - g.(interf_reg_mreg) - g.(pref_reg_reg) - (SetRegMreg.add (x, y) g.(pref_reg_mreg)). - -(** [interfere x y g] holds iff there is a conflict edge in [g] - between the two pseudo-registers [x] and [y]. *) - -Definition interfere (x y: reg) (g: graph) : Prop := - SetRegReg.In (ordered_pair x y) g.(interf_reg_reg). - -(** [interfere_mreg x y g] holds iff there is a conflict edge in [g] - between the pseudo-register [x] and the machine register [y]. *) - -Definition interfere_mreg (x: reg) (y: mreg) (g: graph) : Prop := - SetRegMreg.In (x, y) g.(interf_reg_mreg). - -Lemma ordered_pair_charact: - forall x y, - ordered_pair x y = (x, y) \/ ordered_pair x y = (y, x). -Proof. - unfold ordered_pair; intros. - case (plt x y); intro; tauto. -Qed. - -Lemma ordered_pair_sym: - forall x y, ordered_pair y x = ordered_pair x y. -Proof. - unfold ordered_pair; intros. - destruct (plt y x); destruct (plt x y). - elim (Plt_strict x). eapply Plt_trans; eauto. - auto. - auto. - destruct (Pos.lt_total x y) as [A | [A | A]]. - elim n0; auto. - congruence. - elim n; auto. -Qed. - -Lemma interfere_sym: - forall x y g, interfere x y g -> interfere y x g. -Proof. - unfold interfere; intros. - rewrite ordered_pair_sym. auto. -Qed. - -(** [graph_incl g1 g2] holds if [g2] contains all the conflict edges of [g1] - and possibly more. *) - -Definition graph_incl (g1 g2: graph) : Prop := - (forall x y, interfere x y g1 -> interfere x y g2) /\ - (forall x y, interfere_mreg x y g1 -> interfere_mreg x y g2). - -Lemma graph_incl_trans: - forall g1 g2 g3, graph_incl g1 g2 -> graph_incl g2 g3 -> graph_incl g1 g3. -Proof. - unfold graph_incl; intros. - elim H0; elim H; intros. - split; eauto. -Qed. - -(** We show that the [add_] functions correctly record the desired - conflicts, and preserve whatever conflict edges were already present. *) - -Lemma add_interf_correct: - forall x y g, - interfere x y (add_interf x y g). -Proof. - intros. unfold interfere, add_interf; simpl. - apply SetRegReg.add_1. auto. -Qed. - -Lemma add_interf_incl: - forall a b g, graph_incl g (add_interf a b g). -Proof. - intros. split; intros. - unfold add_interf, interfere; simpl. - apply SetRegReg.add_2. exact H. - exact H. -Qed. - -Lemma add_interf_mreg_correct: - forall x y g, - interfere_mreg x y (add_interf_mreg x y g). -Proof. - intros. unfold interfere_mreg, add_interf_mreg; simpl. - apply SetRegMreg.add_1. auto. -Qed. - -Lemma add_interf_mreg_incl: - forall a b g, graph_incl g (add_interf_mreg a b g). -Proof. - intros. split; intros. - exact H. - unfold add_interf_mreg, interfere_mreg; simpl. - apply SetRegMreg.add_2. exact H. -Qed. - -Lemma add_pref_incl: - forall a b g, graph_incl g (add_pref a b g). -Proof. - intros. split; intros. - exact H. - exact H. -Qed. - -Lemma add_pref_mreg_incl: - forall a b g, graph_incl g (add_pref_mreg a b g). -Proof. - intros. split; intros. - exact H. - exact H. -Qed. - -(** [all_interf_regs g] returns the set of pseudo-registers that - are nodes of [g]. *) - -Definition add_intf2 (r1r2: reg * reg) (u: Regset.t) : Regset.t := - Regset.add (fst r1r2) (Regset.add (snd r1r2) u). -Definition add_intf1 (r1m2: reg * mreg) (u: Regset.t) : Regset.t := - Regset.add (fst r1m2) u. - -Definition all_interf_regs (g: graph) : Regset.t := - let s1 := SetRegMreg.fold add_intf1 g.(interf_reg_mreg) Regset.empty in - let s2 := SetRegMreg.fold add_intf1 g.(pref_reg_mreg) s1 in - let s3 := SetRegReg.fold add_intf2 g.(interf_reg_reg) s2 in - SetRegReg.fold add_intf2 g.(pref_reg_reg) s3. - -Lemma in_setregreg_fold: - forall g r1 r2 u, - SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u -> - Regset.In r1 (SetRegReg.fold add_intf2 g u) /\ - Regset.In r2 (SetRegReg.fold add_intf2 g u). -Proof. - set (add_intf2' := fun u r1r2 => add_intf2 r1r2 u). - assert (forall l r1 r2 u, - InA OrderedRegReg.eq (r1,r2) l \/ Regset.In r1 u /\ Regset.In r2 u -> - Regset.In r1 (List.fold_left add_intf2' l u) /\ - Regset.In r2 (List.fold_left add_intf2' l u)). - induction l; intros; simpl. - elim H; intro. inversion H0. auto. - apply IHl. destruct a as [a1 a2]. - elim H; intro. inversion H0; subst. - red in H2. simpl in H2. destruct H2. subst r1 r2. - right; unfold add_intf2', add_intf2; simpl; split. - apply Regset.add_1. auto. - apply Regset.add_2. apply Regset.add_1. auto. - tauto. - right; unfold add_intf2', add_intf2; simpl; split; - apply Regset.add_2; apply Regset.add_2; tauto. - - intros. rewrite SetRegReg.fold_1. apply H. - intuition. -Qed. - -Lemma in_setregreg_fold': - forall g r u, - Regset.In r u -> - Regset.In r (SetRegReg.fold add_intf2 g u). -Proof. - intros. exploit in_setregreg_fold. eauto. - intros [A B]. eauto. -Qed. - -Lemma in_setregmreg_fold: - forall g r1 mr2 u, - SetRegMreg.In (r1, mr2) g \/ Regset.In r1 u -> - Regset.In r1 (SetRegMreg.fold add_intf1 g u). -Proof. - set (add_intf1' := fun u r1mr2 => add_intf1 r1mr2 u). - assert (forall l r1 mr2 u, - InA OrderedRegMreg.eq (r1,mr2) l \/ Regset.In r1 u -> - Regset.In r1 (List.fold_left add_intf1' l u)). - induction l; intros; simpl. - elim H; intro. inversion H0. auto. - apply IHl with mr2. destruct a as [a1 a2]. - elim H; intro. inversion H0; subst. - red in H2. simpl in H2. destruct H2. subst r1 mr2. - right; unfold add_intf1', add_intf1; simpl. - apply Regset.add_1; auto. - tauto. - right; unfold add_intf1', add_intf1; simpl. - apply Regset.add_2; auto. - - intros. rewrite SetRegMreg.fold_1. apply H with mr2. - intuition. -Qed. - -Lemma all_interf_regs_correct_1: - forall r1 r2 g, - SetRegReg.In (r1, r2) g.(interf_reg_reg) -> - Regset.In r1 (all_interf_regs g) /\ - Regset.In r2 (all_interf_regs g). -Proof. - intros. unfold all_interf_regs. - apply in_setregreg_fold. right. - apply in_setregreg_fold. tauto. -Qed. - -Lemma all_interf_regs_correct_2: - forall r1 mr2 g, - SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) -> - Regset.In r1 (all_interf_regs g). -Proof. - intros. unfold all_interf_regs. - apply in_setregreg_fold'. apply in_setregreg_fold'. - apply in_setregmreg_fold with mr2. right. - apply in_setregmreg_fold with mr2. eauto. -Qed. - |