From a8c744000247af207b489d3cdd4e3d3cf60f72e1 Mon Sep 17 00:00:00 2001 From: blazy Date: Fri, 8 Jan 2010 07:53:02 +0000 Subject: ajout branche allocation de registres git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Merge_Adjacency.v | 347 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 347 insertions(+) create mode 100755 backend/Merge_Adjacency.v (limited to 'backend/Merge_Adjacency.v') diff --git a/backend/Merge_Adjacency.v b/backend/Merge_Adjacency.v new file mode 100755 index 00000000..d6d879ae --- /dev/null +++ b/backend/Merge_Adjacency.v @@ -0,0 +1,347 @@ +Require Import FSets. +Require Import InterfGraphMapImp. +Require Import Remove_Vertex_Degree. +Require Import Edges. +Require Import MyRegisters. +Require Import Interference_adjacency. +Require Import Graph_Facts. + +Module Register := Regs. + +Import Edge RegFacts Props. + +(* The following lemmas define the interference adjacency + of the first endpoint of e after the merge of e *) + +Lemma merge_interf_adj_fst_1 : forall e g H0 Haff, +VertexSet.Subset (interference_adj (fst_ext e) (merge e g H0 Haff)) + (VertexSet.union (interference_adj (fst_ext e) g) + (interference_adj (snd_ext e) g)). + +Proof. +unfold VertexSet.Subset. intros e g H Haff a H1. +rewrite in_interf in H1. generalize (In_merge_edge_inv _ _ _ H Haff H1); intro. +destruct H0 as [x H0]. destruct H0 as [H3 H4]. +destruct x as [ex wx]. destruct ex as [x1 x2]. +assert (interf_edge (x1,x2,wx)) as Hinterf. +destruct H4. unfold same_type in H2. destruct H2; destruct H2. +unfold aff_edge in H4. destruct H4. simpl in H4. congruence. +assumption. +destruct H4 as [H4 HH4]. +assert (eq (a, fst_ext e, None) (redirect (snd_ext e) (fst_ext e) (x1,x2,wx))). +apply weak_eq_interf_eq. assumption. unfold interf_edge. auto. +unfold interf_edge. rewrite redirect_weight_eq. auto. clear H4. +generalize (redirect_charac (x1,x2,wx) (snd_ext e) (fst_ext e)); intros. +destruct H2. destruct H2. destruct H4. rewrite <-H2 in H0. +apply VertexSet.union_2. rewrite in_interf. rewrite H0. assumption. +destruct H2. destruct H2. rewrite <-H2 in H0. change_rewrite. +apply VertexSet.union_3. rewrite in_interf. +destruct (eq_charac _ _ H0); destruct H5; change_rewrite. +assert (eq (a, snd_ext e, None) (x1, x2, wx)). +Eq_comm_eq. apply (Register.eq_trans _ _ _ H5 H6). +generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl. +rewrite H7. assumption. +assert (eq (a,snd_ext e, None) (x1,x2,wx)). +Eq_comm_eq. +generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl. +rewrite H7. assumption. +destruct H2; change_rewrite. rewrite <-H2 in H0. +destruct (eq_charac _ _ H0); destruct H5; change_rewrite. +apply VertexSet.union_3. rewrite in_interf. +assert (eq (a, snd_ext e, None) (x1,x2,wx)). +Eq_eq. +generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl. +rewrite H7. assumption. +apply VertexSet.union_3. rewrite in_interf. +assert (eq (a, snd_ext e, None) (x1,x2,wx)). +Eq_eq. +apply (Register.eq_trans _ _ _ H5 H6). +generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl. +rewrite H7. assumption. +Qed. + +Lemma merge_interf_adj_fst_2 : forall e g H0 Haff, +VertexSet.Subset (interference_adj (fst_ext e) g) + (interference_adj (fst_ext e) (merge e g H0 Haff)). + +Proof. +unfold VertexSet.Subset. intros. +rewrite in_interf in H. rewrite in_interf. +destruct (redirect_charac (a, fst_ext e, None) (snd_ext e) (fst_ext e)); intros. +change_rewrite. destruct H1. destruct H2. +rewrite H1. apply In_merge_interf_edge. assumption. +unfold interf_edge. auto. +change_rewrite. destruct H1. destruct H1. +elim (interf_pref_conflict (snd_ext e) (fst_ext e) g). +split. unfold Prefere. destruct Haff. exists x. +rewrite edge_comm. rewrite <-H3. rewrite (edge_eq e) in H0. assumption. +unfold Interfere. +assert (eq (snd_ext e, fst_ext e, None) (a, fst_ext e, None)) by Eq_eq. +rewrite H3. assumption. +destruct H1. rewrite H1. apply In_merge_interf_edge. assumption. +unfold interf_edge. auto. +Qed. + +Lemma merge_interf_adj_fst_3 : forall e g H0 Haff, +VertexSet.Subset (interference_adj (snd_ext e) g) + (interference_adj (fst_ext e) (merge e g H0 Haff)). + +Proof. +unfold VertexSet.Subset. intros. +rewrite in_interf in H. rewrite in_interf. +destruct (redirect_charac (a, snd_ext e, None) (snd_ext e) (fst_ext e)); intros. +change_rewrite. destruct H1. destruct H2. elim H3. auto. +change_rewrite. destruct H1. destruct H1. +elim (In_graph_edge_diff_ext _ _ H). change_rewrite. auto. +destruct H1. rewrite H1. apply In_merge_interf_edge. assumption. +unfold interf_edge. auto. +Qed. + +Lemma merge_interf_adj_fst : forall e g H0 Haff, +VertexSet.Equal (interference_adj (fst_ext e) (merge e g H0 Haff)) + (VertexSet.union (interference_adj (fst_ext e) g) + (interference_adj (snd_ext e) g)). + +Proof. +intros. split; intros. +apply (merge_interf_adj_fst_1 _ _ H0 Haff _ H). +destruct (VertexSet.union_1 H). + apply (merge_interf_adj_fst_2 _ _ H0 Haff _ H1). + apply (merge_interf_adj_fst_3 _ _ H0 Haff _ H1). +Qed. + +(* The following lemmas define the equality of the interference adjacency + of any vertex which is not an endpoint of e after the merge of e *) + +Lemma merge_interf_adj_1 : forall x e g Hin Haff, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +VertexSet.Subset (VertexSet.remove (snd_ext e) (interference_adj x g)) + (interference_adj x (merge e g Hin Haff)). + +Proof. +unfold VertexSet.Subset. intros. +rewrite in_interf. rewrite Dec.F.remove_iff in H1. destruct H1. +destruct (redirect_charac (a,x,None) (snd_ext e) (fst_ext e)); change_rewrite. +destruct H3. destruct H4. rewrite H3. +apply In_merge_interf_edge. rewrite <-in_interf. assumption. +unfold interf_edge. auto. +destruct H3. destruct H3. elim H2. auto. +destruct H3. elim H0. auto. +Qed. + +Lemma merge_interf_adj_2 : forall x e g Hin Haff, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +VertexSet.Subset (interference_adj x (merge e g Hin Haff)) + (VertexSet.add (fst_ext e) (interference_adj x g)). + +Proof. +unfold VertexSet.Subset. intros. +destruct (Register.eq_dec a (fst_ext e)); [apply VertexSet.add_1|apply VertexSet.add_2]; intuition. +rewrite in_interf in H1. generalize (In_merge_edge_inv _ _ _ Hin Haff H1). intro. +destruct H2. destruct H2. destruct H3. +assert (eq (a,x,None) (redirect (snd_ext e) (fst_ext e) x0)). +apply weak_eq_interf_eq. assumption. unfold interf_edge. auto. +unfold interf_edge. rewrite redirect_weight_eq. +unfold same_type in H4. destruct H4; destruct H4. +unfold aff_edge in H5. destruct H5. simpl in H5. congruence. +auto. intuition. +rewrite in_interf. rewrite H5. +destruct (redirect_charac x0 (snd_ext e) (fst_ext e)). +destruct H6. destruct H7. rewrite <-H6. assumption. +destruct H6. destruct H6. rewrite <-H6 in H5. +destruct (eq_charac _ _ H5); destruct H8; change_rewrite. +elim n. auto. elim H. auto. +destruct H6. rewrite <-H6 in H5. +destruct (eq_charac _ _ H5); destruct H8; change_rewrite. +elim H. auto. elim n. auto. +Qed. + +Lemma merge_interf_adj_not_in : forall x e g Hin Haff, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +~VertexSet.In x (interference_adj (snd_ext e) g) -> +VertexSet.Equal (interference_adj x (merge e g Hin Haff)) + (interference_adj x g). + +Proof. +intros. split; intros. +generalize (merge_interf_adj_2 x e g Hin Haff H H0 a H2). intro. +rewrite Dec.F.add_iff in H3. destruct H3. +rewrite <-H3 in H2. generalize (interf_adj_comm _ _ _ H2). intro. +rewrite merge_interf_adj_fst in H4. destruct (VertexSet.union_1 H4). +rewrite <-H3. apply interf_adj_comm. assumption. +elim H1. auto. +assumption. +apply merge_interf_adj_1; auto. +apply VertexSet.remove_2; auto. +intro. elim H1. apply interf_adj_comm. rewrite H3. assumption. +Qed. + +Lemma merge_interf_adj_in_snd : forall x e g Hin Haff, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +VertexSet.In x (interference_adj (snd_ext e) g) -> +VertexSet.Equal (interference_adj x (merge e g Hin Haff)) + (VertexSet.add (fst_ext e) (VertexSet.remove (snd_ext e) + (interference_adj x g))). + +Proof. +intros. split; intros. +generalize (merge_interf_adj_2 _ _ _ Hin Haff H H0 _ H2). intro. +rewrite Dec.F.add_iff in H3. destruct H3. +apply VertexSet.add_1. assumption. +apply VertexSet.add_2. apply VertexSet.remove_2. +intro. rewrite <-H4 in H2. rewrite in_interf in H2. +generalize (proj1 (In_graph_edge_in_ext _ _ H2)). change_rewrite. intro. +rewrite In_merge_vertex in H5. destruct H5. elim H6. auto. assumption. + +rewrite Dec.F.add_iff in H2. destruct H2. +rewrite <-H2. apply interf_adj_comm. rewrite merge_interf_adj_fst. +apply VertexSet.union_3. auto. +apply merge_interf_adj_1; auto. +Qed. + +Lemma merge_interf_adj_in_both : forall x e g Hin Haff, +VertexSet.In x (interference_adj (snd_ext e) g) -> +VertexSet.In x (interference_adj (fst_ext e) g) -> +VertexSet.Equal (interference_adj x (merge e g Hin Haff)) + (VertexSet.remove (snd_ext e) (interference_adj x g)). + +Proof. +intros. +assert (~Register.eq x (fst_ext e)). +intro. rewrite H1 in H0. elim (not_in_interf_self _ _ H0). +assert (~Register.eq x (snd_ext e)). +intro. rewrite H2 in H. elim (not_in_interf_self _ _ H). +rewrite merge_interf_adj_in_snd; auto. +split; intros. +rewrite Dec.F.add_iff in H3. destruct H3. +apply VertexSet.remove_2. intro. +elim (In_graph_edge_diff_ext _ _ Hin). rewrite H3. auto. +rewrite <-H3. apply interf_adj_comm. assumption. +assumption. +apply VertexSet.add_2. auto. +Qed. + +Lemma preference_adj_merge : forall x e g p q, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +VertexSet.Subset (preference_adj x (merge e g p q)) + (VertexSet.add (fst_ext e) + (VertexSet.remove (snd_ext e) (preference_adj x g))). + +Proof. +intros x e g p q H0 H1. generalize I. intro H. +unfold VertexSet.Subset; intros. +rewrite in_pref in H2. destruct H2. +generalize (In_merge_edge_inv e _ g p q H2). intro. +destruct H3. destruct H3. destruct H4 as [H4 HH4]. +unfold weak_eq in H4. change_rewrite. destruct H4. +unfold redirect in H4; change_rewrite. +destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite. +destruct H4. apply VertexSet.add_1. intuition. +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. +destruct H4. elim H0. intuition. +destruct H4. apply VertexSet.add_2. apply VertexSet.remove_2. +intro. elim n. rewrite H6. intuition. +rewrite in_pref. unfold same_type in HH4. +destruct HH4. destruct H6. +destruct H6. exists x2. +assert (eq (a,x,Some x2) x1). +apply eq_ordered_eq. split; try split; simpl; auto. +unfold get_weight in H6. rewrite H6. apply OptionN_as_OT.eq_refl. +rewrite H8. assumption. +destruct H6. unfold interf_edge in H7. simpl in H7. congruence. +unfold redirect in H4; change_rewrite. +destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite. +destruct H4. elim H0. auto. +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. +destruct H4. apply VertexSet.add_1. intuition. +destruct H4. apply VertexSet.add_2. apply VertexSet.remove_2. +intro. elim n0. rewrite H6. intuition. +rewrite in_pref. unfold same_type in HH4. +destruct HH4. destruct H6. +destruct H6. exists x2. +assert (eq (a,x,Some x2) x1). +rewrite edge_comm. apply eq_ordered_eq. split; try split; simpl; auto. +unfold get_weight in H6. rewrite H6. apply OptionN_as_OT.eq_refl. +rewrite H8. assumption. +destruct H6. unfold interf_edge in H7. simpl in H7. congruence. +Qed. + +Lemma preference_adj_merge_2 : forall x e g p q, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +VertexSet.Subset (VertexSet.remove (fst_ext e) (VertexSet.remove (snd_ext e) (preference_adj x g))) + (preference_adj x (merge e g p q)). + +Proof. +unfold VertexSet.Subset; intros x e g p q H0 H1 a H2. generalize I. intro H. +assert (~Register.eq a (fst_ext e)). intro. +rewrite H3 in H2. elim (VertexSet.remove_1 (Register.eq_refl _) H2). +generalize (VertexSet.remove_3 H2). clear H2. intro H2. +assert (~Register.eq a (snd_ext e)). intro. +rewrite H4 in H2. elim (VertexSet.remove_1 (Register.eq_refl _) H2). +generalize (VertexSet.remove_3 H2). clear H2. intro. +rewrite in_pref in H2. destruct H2. +assert (exists w, In_graph_edge (a,x,Some w) (merge e g p q)). +cut (Prefere (fst_ext (redirect (snd_ext e) (fst_ext e) (a,x,Some x0))) + (snd_ext (redirect (snd_ext e) (fst_ext e) (a,x,Some x0))) + (merge e g p q)). intro. +unfold redirect in H5; change_rewrite. +destruct (OTFacts.eq_dec a (snd_ext e)); change_rewrite. +elim (H4 r). +destruct (OTFacts.eq_dec x (snd_ext e)); change_rewrite. +elim (H1 r). +unfold Prefere in H5. assumption. +apply In_merge_pref_edge. assumption. +intro. destruct (eq_charac _ _ H5); change_rewrite; destruct H6. +elim H1. auto. +elim H0. auto. +unfold aff_edge. exists x0. auto. +intro. unfold redirect in H5;change_rewrite. +destruct (OTFacts.eq_dec a (snd_ext e)); change_rewrite. +elim (H4 r). +destruct (OTFacts.eq_dec x (snd_ext e)); change_rewrite. +elim (H1 r). +unfold Interfere in H5. generalize (In_merge_edge_inv e _ g p q H5). intro H8. +generalize I. intro H7. +destruct H8. destruct H6. destruct H8. +unfold weak_eq in H8. change_rewrite. destruct H8. +unfold redirect in H8; change_rewrite. +destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite; destruct H8. +elim (H3 H8). +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. +elim (H0 H10). +elim (interf_pref_conflict a x g). +split. +unfold Prefere. exists x0. assumption. +unfold Interfere. +assert (eq (a,x,None) x1). +apply weak_eq_interf_eq. unfold weak_eq. change_rewrite. +left. split; auto. unfold interf_edge. auto. +unfold same_type in H9. destruct H9. destruct H9. +unfold aff_edge in H11. destruct H11. simpl in H11. congruence. +destruct H9. assumption. +rewrite H11. assumption. + +unfold redirect in H8; change_rewrite. +destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite. +destruct H8. elim (H0 H10). +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. +destruct H8. elim (H3 H8). +elim (interf_pref_conflict a x g). +split. +unfold Prefere. exists x0. assumption. +unfold Interfere. destruct H8. +assert (eq (a,x,None) x1). +apply weak_eq_interf_eq. unfold weak_eq. change_rewrite. +right. split; auto. unfold interf_edge. auto. +unfold same_type in H9. destruct H9. destruct H9. +unfold aff_edge in H11. destruct H11. simpl in H11. congruence. +destruct H9. assumption. +rewrite H11. assumption. +rewrite in_pref. assumption. +Qed. -- cgit