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/Delete_Preference_Edges_Move.v | 138 +++++++++++++++++++++++++++++++++ 1 file changed, 138 insertions(+) create mode 100755 backend/Delete_Preference_Edges_Move.v (limited to 'backend/Delete_Preference_Edges_Move.v') diff --git a/backend/Delete_Preference_Edges_Move.v b/backend/Delete_Preference_Edges_Move.v new file mode 100755 index 00000000..66f9ab6a --- /dev/null +++ b/backend/Delete_Preference_Edges_Move.v @@ -0,0 +1,138 @@ +Require Import FSets. +Require Import InterfGraphMapImp. +Require Import Merge_Move. +Require Import Edges. +Require Import MyRegisters. +Require Import Affinity_relation. +Require Import Interference_adjacency. +Require Import Delete_Preference_Edges_Adjacency. +Require Import Remove_Vertex_Move. + +Import Edge Props RegFacts. + +(* The frozen vertex is nonmove-related in the resulting graph *) +Lemma not_aff_related_delete_preference_edges : forall r g p, +move_related (delete_preference_edges r g p) r = false. + +Proof. +intros. apply move_related_false_charac2. +intros. +rewrite In_delete_preference_edges_edge in H0. destruct H0. +intro. elim H1. split; assumption. +Qed. + +(* A vertex which is move-related after a freeze is move-related before it *) +Lemma move_related_delete_move_related : forall x r g p, +move_related (delete_preference_edges r g p) x = true -> +move_related g x = true. + +Proof. +intros x r g p H. +generalize (move_related_charac _ _ H);intro H0. +destruct H0 as [y H0]. +destruct H0 as [H0 H1];destruct H1 as [H1 H2]. +rewrite In_delete_preference_edges_edge in H1. destruct H1. +apply (move_related_charac2 _ _ _ H0 H1 H2). +Qed. + +(* A vertex which is move-related in g and not in (delete_preference_edges r g H) + is a preference neighbor of r in g *) +Lemma delete_preference_edges_move_1 : forall x r g H, +~Register.eq r x -> +move_related g x = true -> +move_related (delete_preference_edges r g H) x = false -> +VertexSet.In x (preference_adj r g). + +Proof. +intros. generalize (not_move_related_empty_pref _ _ H2). intro. +rewrite delete_preference_preference_adj in H3. +destruct (In_dec r (preference_adj x g)). +apply pref_adj_comm. assumption. +assert (VertexSet.Equal (preference_adj x g) VertexSet.empty). +split; intros. +rewrite <-H3. apply VertexSet.remove_2. +intro. rewrite <-H5 in H4. elim n. auto. +assumption. +elim (VertexSet.empty_1 H4). +elim (move_related_not_empty_pref _ _ H1 H4). +auto. +Qed. + +(* A vertex which is move-related in g and nonmove-related in + (delete_preference_edges r g H) has a preference degree of 1 *) +Lemma delete_preference_edges_move_2 : forall x r g H, +~Register.eq r x -> +move_related g x = true -> +move_related (delete_preference_edges r g H) x = false -> +VertexSet.cardinal (preference_adj x g) = 1. + +Proof. +intros. generalize (not_move_related_empty_pref _ _ H2). intro. +rewrite delete_preference_preference_adj in H3. +destruct (In_dec r (preference_adj x g)). +cut (VertexSet.Equal (preference_adj x g) (VertexSet.singleton r)). intros. +rewrite H4. apply singleton_cardinal. +split; intros. +destruct (Register.eq_dec a r). +apply VertexSet.singleton_2. intuition. +assert (VertexSet.In a VertexSet.empty). +rewrite <-H3. apply VertexSet.remove_2; auto. +elim (VertexSet.empty_1 H5). +generalize (VertexSet.singleton_1 H4). intro. +rewrite <-H5. auto. +elim (move_related_not_empty_pref _ _ H1). +rewrite <-H3. + +split; intros. +rewrite Dec.F.remove_neq_iff. +assumption. +intro. rewrite <-H5 in H4. elim n. auto. +apply (VertexSet.remove_3 H4). +auto. +Qed. + +(* Reciprocally, a vertex which is move-related in g, + has a preference degree of 1 and is a preference neighbor of r + is nonmove-related in (delete_preference_edges r g H) *) +Lemma delete_preference_edges_move_inv : forall x r g H, +~Register.eq r x -> +move_related g x = true -> +VertexSet.In x (preference_adj r g) -> +VertexSet.cardinal (preference_adj x g) = 1 -> +move_related (delete_preference_edges r g H) x = false. + +Proof. +intros. +apply move_related_false_charac2. intros. +rewrite In_delete_preference_edges_edge in H5. +destruct H5. +intro. elim H6. +split. assumption. +cut (VertexSet.Equal (preference_adj x g) (VertexSet.singleton r)). intros. +destruct H7;[right|left]. +rewrite (edge_eq e) in H5. +assert (eq (x, snd_ext e, get_weight e) (fst_ext e, snd_ext e, get_weight e)). +Eq_eq. rewrite <-H9 in H5. +destruct H4. rewrite H4 in H5. +apply VertexSet.singleton_1. rewrite <-H8. +rewrite in_pref. exists x0. rewrite edge_comm. auto. +rewrite (edge_eq e) in H5. +assert (eq (fst_ext e, x, get_weight e) (fst_ext e, snd_ext e, get_weight e)). +Eq_eq. rewrite <-H9 in H5. +destruct H4. rewrite H4 in H5. +apply VertexSet.singleton_1. rewrite <-H8. +rewrite in_pref. exists x0. rewrite edge_comm. auto. +rewrite edge_comm. assumption. +apply cardinal_1_singleton. apply pref_adj_comm. assumption. assumption. +Qed. + +Lemma delete_preference_edges_move_false_false : forall x r g H, +move_related g x = false -> +move_related (delete_preference_edges r g H) x = false. + +Proof. +intros. +case_eq (move_related (delete_preference_edges r g H) x); intros. +rewrite (move_related_delete_move_related _ _ _ _ H1) in H0. inversion H0. +reflexivity. +Qed. -- cgit