ajout branche allocation de registres

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 205 insertions, 0 deletions

diff --git a/backend/Merge_Degree.v b/backend/Merge_Degree.v
new file mode 100755
index 00000000..15849794
--- /dev/null
+++ b/backend/Merge_Degree.v
@@ -0,0 +1,205 @@
+Require Import FSets.
+Require Import InterfGraphMapImp.
+Require Import Merge_Adjacency.
+Require Import ZArith.
+Require Import Edges.
+Require Import MyRegisters.
+Require Import Merge_Adjacency.
+Require Import Interference_adjacency.
+Require Import Remove_Vertex_Degree.
+
+Module Register := Regs.
+
+Import Edge Props RegFacts.
+
+(* If x interferes with both (fst_ext e) and (snd_ext e), then
+    its degree decreases of one when e is coalesced *)
+Lemma merge_degree_dec_inter : forall x e g Hin Haff,
+VertexSet.In x (interference_adj (fst_ext e) g) ->
+VertexSet.In x (interference_adj (snd_ext e) g) ->
+interf_degree g x = S (interf_degree (merge e g Hin Haff) x).
+
+Proof.
+intros. unfold interf_degree.
+rewrite (cardinal_m (merge_interf_adj_in_both _ _ _ Hin Haff H0 H)).
+rewrite remove_cardinal_1. reflexivity. apply interf_adj_comm. auto.
+Qed.
+
+(* If x does not interfere with both (fst_ext e) and (snd_ext e)
+    then its degree is unchanged when e is coalesced *)
+Lemma merge_dec_eq : forall x e g Hin Haff,
+~VertexSet.In x (interference_adj (fst_ext e) g) \/
+~VertexSet.In x (interference_adj (snd_ext e) g) ->
+~Register.eq x (fst_ext e) ->
+~Register.eq x (snd_ext e) ->
+interf_degree g x = interf_degree (merge e g Hin Haff) x.
+
+Proof.
+intros. unfold interf_degree. destruct H.
+destruct (In_dec x (interference_adj (snd_ext e) g)).
+rewrite (cardinal_m (merge_interf_adj_in_snd _ _ _ Hin Haff H0 H1 i)).
+rewrite add_cardinal_2. rewrite remove_cardinal_1. reflexivity.
+apply interf_adj_comm. auto.
+intro. elim H. apply interf_adj_comm. apply (VertexSet.remove_3 H2).
+rewrite (cardinal_m (merge_interf_adj_not_in _ _ _ Hin Haff H0 H1 n)). reflexivity.
+rewrite (cardinal_m (merge_interf_adj_not_in _ _ _ Hin Haff H0 H1 H)). reflexivity.
+Qed.
+
+(* The interference degree of any vertex which is not an endpoint
+    of e decreases when e is coalesced *)
+Lemma merge_degree_dec : forall x e g Hin Haff,
+~Register.eq x (fst_ext e) ->
+~Register.eq x (snd_ext e) ->
+interf_degree (merge e g Hin Haff) x <= interf_degree g x.
+
+Proof.
+intros. destruct (In_dec x (interference_adj (fst_ext e) g)).
+destruct (In_dec x (interference_adj (snd_ext e) g)).
+rewrite (merge_degree_dec_inter x e g Hin Haff i i0). auto.
+rewrite (merge_dec_eq x e g Hin Haff (or_intror _ n)); auto.
+rewrite (merge_dec_eq x e g Hin Haff (or_introl _ n)); auto.
+Qed.
+
+(* If x does not interfere with the first endpoint of e then
+    x is of low-degree in (merge e g Hin Haff) iff it is in g *)
+Lemma low_merge_low_fst : forall x e g K Hin Haff,
+~VertexSet.In x (interference_adj (fst_ext e) g) ->
+~Register.eq x (snd_ext e) ->
+~Register.eq x (fst_ext e) ->
+has_low_degree (merge e g Hin Haff) K x = has_low_degree g K x.
+
+Proof.
+intros x e g palette Hin Haff H H0 H1. unfold has_low_degree.
+rewrite (merge_dec_eq x e g Hin Haff); auto.
+Qed.
+
+(* If x does not interfere with the second endpoint of e then
+    x is of low-degree in (merge e g Hin Haff) iff it is in g *)
+Lemma low_merge_low_snd : forall x e g K Hin Haff,
+~VertexSet.In x (interference_adj (snd_ext e) g) ->
+~Register.eq x (snd_ext e) ->
+~Register.eq x (fst_ext e) ->
+has_low_degree (merge e g Hin Haff) K x = has_low_degree g K x.
+
+Proof.
+intros x e g palette Hin Haff H H0 H1. unfold has_low_degree.
+rewrite (merge_dec_eq x e g Hin Haff); auto.
+Qed.
+
+(* A high-degree vertex of (merge e g Hin Haff) is of high-degree in g *)
+Lemma merge_low_1 : forall g e x K Haff Hin,
+has_low_degree (merge e g Hin Haff) K x = false ->
+~Register.eq x (snd_ext e) ->
+~Register.eq x (fst_ext e) ->
+has_low_degree g K x = false.
+
+Proof.
+intros g e x K Haff Hin Hpre H0 H1. unfold has_low_degree in *.
+destruct (le_lt_dec K (interf_degree (merge e g Hin Haff) x));
+destruct (le_lt_dec K (interf_degree g x )); inversion Hpre.
+reflexivity.
+generalize (merge_degree_dec x e g Hin Haff H1 H0). intro.
+apply False_ind. intuition.
+Qed.
+
+(* A low-degree vertex of g is of low-degree in (merge e g Haff Hin) *)
+Lemma low_dec : forall x e g Hin Haff K,
+~Register.eq x (fst_ext e) ->
+~Register.eq x (snd_ext e) ->
+has_low_degree g K x = true ->
+has_low_degree (merge e g Hin Haff) K x = true.
+
+Proof.
+intros.
+case_eq (has_low_degree (merge e g Hin Haff) K x);[auto|intros].
+rewrite (merge_low_1 g e x K Haff Hin H2 H0 H) in H1. inversion H1.
+Qed.
+
+(* A vertex high-degree vertex of g (which is not an endpoint of e) 
+    which is of low-degree in (merge e g p q) belongs to the interference
+    neighborhood of the two endpoints of e in g *)
+Lemma merge_dec_interf : forall x e k g p q,
+has_low_degree g k x = false ->
+has_low_degree (merge e g p q) k x = true ->
+~Register.eq x (fst_ext e) ->
+~Register.eq x (snd_ext e) ->
+VertexSet.In x (interference_adj (fst_ext e) g) /\
+VertexSet.In x (interference_adj (snd_ext e) g).
+
+Proof.
+intros.
+destruct (In_dec x (interference_adj (fst_ext e) g)).
+split. assumption.
+destruct (In_dec x (interference_adj (snd_ext e) g)).
+assumption.
+rewrite (low_merge_low_snd _ _ _ _ p q n H2 H1) in H0. rewrite H0 in H. inversion H.
+rewrite (low_merge_low_fst _ _ _ _ p q n H2 H1) in H0. rewrite H0 in H. inversion H.
+Qed.
+
+(* A vertex high-degree vertex of g (which is not an endpoint of e) 
+    which is of low-degree in (merge e g p q) is of degree k in g *) 
+Lemma merge_dec_K : forall x e k g p q,
+~Register.eq x (fst_ext e) ->
+~Register.eq x (snd_ext e) ->
+has_low_degree g k x = false ->
+has_low_degree (merge e g p q) k x = true ->
+interf_degree g x = k.
+
+Proof.
+intros x e k g p q H0 H1 H2 H3. generalize I. intro H. unfold interf_degree.
+assert (VertexSet.In x (interference_adj (fst_ext e) g) /\
+        VertexSet.In x (interference_adj (snd_ext e) g)).
+apply (merge_dec_interf x e k g p q); auto.
+destruct H4.
+generalize (merge_degree_dec_inter x e g p q H4 H5). intro.
+unfold has_low_degree, interf_degree in *.
+destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x (merge e g p q)))).
+inversion H3.
+destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x g))).
+rewrite H6 in l0. rewrite (lt_le_S_eq _ _ l l0). assumption.
+inversion H2.
+Qed.
+
+(* Reciprocally, a vertex of degree k interfering with
+    the two endpoints of g is of low-degree in (merge e g p q) *)
+Lemma merge_dec_low : forall x e k g p q,
+interf_degree g x = k ->
+VertexSet.In x (interference_adj (fst_ext e) g) ->
+VertexSet.In x (interference_adj (snd_ext e) g) ->
+has_low_degree (merge e g p q) k x = true.
+
+Proof.
+unfold interf_degree. intros x e k g p q H0 H1 H2. generalize I. intro H.
+assert (~Register.eq x (fst_ext e)).
+intro. elim (not_in_interf_self (fst_ext e) g). rewrite H3 in H1. assumption.
+assert (~Register.eq x (snd_ext e)).
+intro. elim (not_in_interf_self (snd_ext e) g). rewrite H4 in H2. assumption.
+generalize (merge_degree_dec_inter x e g p q H1 H2). intro.
+unfold has_low_degree, interf_degree in *.
+destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x (merge e g p q)))).
+rewrite H5 in H0. rewrite <-H0 in l. elim (le_S_irrefl _ l).
+reflexivity.
+Qed.
+
+(* Again, unused but meaningful theorem, summarizing evolution of degree
+   when an edge e is coalesced *)
+
+Theorem merge_degree_evolution : forall x e k g p q,
+~Register.eq x (fst_ext e) ->
+~Register.eq x (snd_ext e) ->
+((has_low_degree g k x = false /\ has_low_degree (merge e g p q) k x = true)
+                                               <->
+(interf_degree g x = k /\
+ VertexSet.In x (interference_adj (fst_ext e) g) /\ 
+ VertexSet.In x (interference_adj (snd_ext e) g))).
+
+Proof.
+split; intros.
+destruct H1. 
+split. apply (merge_dec_K x e k g p q); auto.
+apply (merge_dec_interf x e k g p q); auto.
+destruct H1. destruct H2.
+split. unfold has_low_degree. rewrite H1. 
+destruct (le_lt_dec k k). reflexivity. elim (lt_irrefl _ l).
+apply merge_dec_low; auto.
+Qed.