diff options
Diffstat (limited to 'backend/WS.v')
| -rwxr-xr-x | backend/WS.v | 231 |
1 files changed, 231 insertions, 0 deletions
diff --git a/backend/WS.v b/backend/WS.v new file mode 100755 index 00000000..2f433272 --- /dev/null +++ b/backend/WS.v @@ -0,0 +1,231 @@ +Require Import FSets. +Require Import InterfGraphMapImp. +Require Import Conservative_criteria. +Require Import Edges. +Require Import MyRegisters. +Require Import Affinity_relation. + +Import Edge RegFacts Props OTFacts. + +(* Intersections of vertices sets of the worklists are empty *) +Lemma WS_empty_inter_1 : forall g palette WL, +WS_properties g palette WL -> +VertexSet.Empty (VertexSet.inter (get_spillWL WL) (get_freezeWL WL)). + +Proof. +intros g palette WL H. +unfold VertexSet.Empty. +intros a H0. +generalize (VertexSet.inter_1 H0);intro H1. +generalize (VertexSet.inter_2 H0);intro H2. +unfold WS_properties in H. +destruct H as [H H3];destruct H3 as [H3 H4];destruct H4 as [H4 H5]. +generalize (proj1 (H a) H1);intro H6. +destruct H6 as [H6 _]. +generalize (proj1 (H3 a) H2);intro H7. +destruct H7 as [H7 _]. +rewrite H6 in H7; inversion H7. +Qed. + +Lemma WS_empty_inter_2 : forall g palette WL, +WS_properties g palette WL -> +VertexSet.Empty (VertexSet.inter (get_spillWL WL) (get_simplifyWL WL)). + +Proof. +intros g palette WL H. +unfold VertexSet.Empty. +intros a H0. +generalize (VertexSet.inter_1 H0);intro H1. +generalize (VertexSet.inter_2 H0);intro H2. +unfold WS_properties in H. +destruct H as [H H3];destruct H3 as [H3 H4];destruct H4 as [H4 H5]. +generalize (proj1 (H a) H1);intro H6. +destruct H6 as [H6 _]. +generalize (proj1 (H4 a) H2);intro H7. +destruct H7 as [H7 _]. +rewrite H6 in H7; inversion H7. +Qed. + +Lemma WS_empty_inter_3 : forall g palette WL, +WS_properties g palette WL -> +VertexSet.Empty (VertexSet.inter (get_freezeWL WL) (get_simplifyWL WL)). + +Proof. +intros g palette WL H. +unfold VertexSet.Empty. +intros a H0. +generalize (VertexSet.inter_1 H0);intro H1. +generalize (VertexSet.inter_2 H0);intro H2. +unfold WS_properties in H. +destruct H as [H H3];destruct H3 as [H3 H4];destruct H4 as [H4 H5]. +generalize (proj1 (H3 a) H1);intro H6. +destruct H6 as [_ H6]. +destruct H6 as [H6 _]. +generalize (proj1 (H4 a) H2);intro H7. +destruct H7 as [_ H7]. +destruct H7 as [H7 _]. +rewrite H6 in H7; inversion H7. +Qed. + +(* A tactic for simplifying proofs of belonging of a vertex to a worklist *) +Ltac WS_apply H := generalize H;intro HWS_; +match goal with +| |- (VertexSet.In ?A _) => destruct HWS_ as [HWS_ HWS__]; + try (apply (proj2 (HWS_ A))); + destruct HWS__ as [HWS__ HWS___]; + try (apply (proj2 (HWS__ A))); + destruct HWS___ as [HWS___ HWS____]; + try (apply (proj2 (HWS___ A))); + clear HWS_ HWS__ HWS___ HWS____ +| |- (EdgeSet.In ?A _) => do 3 destruct HWS_ as [_ HWS_]; + apply (proj2 (HWS_ A)); + clear HWS_ +end. + +(* Lemmas for generalizing properties of a vertex belonging to a given worklist *) +Lemma In_spill_props : forall x g WL s a b c palette, +VertexSet.In x s -> +WL = (s,a,b,c) -> +WS_properties g palette WL -> +has_low_degree g palette x = false /\ In_graph x g /\ ~VertexSet.In x (precolored g). + +Proof. +intros x g WL s a b c palette H H0 H1. +unfold WS_properties in H1;rewrite H0 in H1. +destruct H1 as [H1 _]. +unfold get_spillWL in H1;simpl in H1. +apply (proj1 (H1 x) H). +Qed. + +Lemma In_freeze_props : forall x g WL s a b c palette, +VertexSet.In x s -> +WL = (a,s,b,c) -> +WS_properties g palette WL -> +has_low_degree g palette x = true /\ move_related g x = true /\ In_graph x g /\ ~VertexSet.In x (precolored g). + +Proof. +intros x g WL s a b c palette H H0 H1. +unfold WS_properties in H1;rewrite H0 in H1. +destruct H1 as [_ H1]. +destruct H1 as [H1 _]. +unfold get_freezeWL in H1;simpl in H1. +generalize (proj1 (H1 x) H);intro. +intuition. +apply move_related_in_graph;intuition. +Qed. + +Lemma In_simplify_props : forall x g WL s a b c palette, +VertexSet.In x s -> +WL = (a,b,s,c) -> +WS_properties g palette WL -> +has_low_degree g palette x = true /\ move_related g x = false /\ In_graph x g /\ ~VertexSet.In x (precolored g). + +Proof. +intros x g WL s a b c palette H H0 H1. +unfold WS_properties in H1;rewrite H0 in H1. +do 2 destruct H1 as [_ H1]. +destruct H1 as [H1 _]. +unfold get_spillWL in H1;simpl in H1. +apply (proj1 (H1 x) H). +Qed. + +Lemma In_move_props : forall e g WL s a b c palette, +EdgeSet.In e s -> +WL = (a,b,c,s) -> +WS_properties g palette WL -> +aff_edge e /\ In_graph_edge e g. + +Proof. +intros e g WL s a b c palette H H0 H1. +unfold WS_properties in H1;rewrite H0 in H1. +do 3 destruct H1 as [_ H1]. +unfold get_movesWL in H1;simpl in H1. +apply (proj1 (H1 e) H). +Qed. + +Lemma WS_props_equal : +forall g palette ws ws', +VertexSet.Equal (get_simplifyWL ws) (get_simplifyWL ws') -> +VertexSet.Equal (get_freezeWL ws) (get_freezeWL ws') -> +VertexSet.Equal (get_spillWL ws) (get_spillWL ws') -> +EdgeSet.Equal (get_movesWL ws) (get_movesWL ws') -> +WS_properties g palette ws -> +WS_properties g palette ws'. + +Proof. +unfold WS_properties;unfold get_spillWL;unfold get_freezeWL; +unfold get_simplifyWL;unfold get_movesWL;simpl;unfold VertexSet.Equal; +unfold EdgeSet.Equal;intros g palette ws ws' H H0 H1 H2 H3. +destruct ws as [ws d]; destruct ws as [ws c]; destruct ws as [a b]. +destruct ws' as [ws' p]; destruct ws' as [ws' o]; destruct ws' as [m n]. simpl in *. +generalize (VertexSet.eq_sym H);generalize (VertexSet.eq_sym H0); +generalize (VertexSet.eq_sym H1);generalize (EdgeSet.eq_sym H2); +clear H;clear H0;clear H1;clear H2;intros H2 H1 H0 H. + +destruct H3 as [Hsp H3];destruct H3 as [Hf H3]; +destruct H3 as [Hsi Hm]. +do 2 split. +intro H4;apply (proj1 (Hsp x) (proj1 (H1 x) H4)). +intro H4;apply (proj2 (H1 x) (proj2 (Hsp x) H4)). +split;intro H4. +apply (proj1 (Hf x) (proj1 (H0 x) H4)). +apply (proj2 (H0 x) (proj2 (Hf x) H4)). +split. +split;intro H4. +apply (proj1 (Hsi x) (proj1 (H x) H4)). +apply (proj2 (H x) (proj2 (Hsi x) H4)). +split;intro H4. +apply (proj1 (Hm e) (proj1 (H2 e) H4)). +apply (proj2 (H2 e) (proj2 (Hm e) H4)). +Qed. + +(* Definition of the nonprecolored vertices of a graph *) +Definition not_precolored g := VertexSet.diff (V g) (precolored g). + +(* The union of vertices worklists forms the nonprecolored vertices set of g *) +Lemma not_precolored_union_ws : forall g palette ws, +WS_properties g palette ws -> +VertexSet.Equal +(VertexSet.union (VertexSet.union (get_spillWL ws) (get_freezeWL ws)) (get_simplifyWL ws)) +(not_precolored g). + +Proof. +intros g palette ws HWS. +split. intro H. +unfold not_precolored. apply VertexSet.diff_3. +destruct (VertexSet.union_1 H). +destruct (VertexSet.union_1 H0). +apply (proj1(proj2 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). +apply (proj2(proj2 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). +apply (proj2(proj2 (In_simplify_props _ _ _ _ _ _ _ _ H0 (refl_equal _) HWS))). +destruct (VertexSet.union_1 H). +destruct (VertexSet.union_1 H0). +apply (proj2(proj2 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). +apply (proj2(proj2 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). +apply (proj2(proj2 (In_simplify_props _ _ _ _ _ _ _ _ H0 (refl_equal _) HWS))). +intro H. +unfold not_precolored in H. +generalize (VertexSet.diff_1 H). intro H0. +generalize (VertexSet.diff_2 H). clear H. intro H. +case_eq (has_low_degree g palette a); intro Hlow. +case_eq (move_related g a); intro Haff. +apply VertexSet.union_2. apply VertexSet.union_3. +WS_apply HWS. intuition. +apply VertexSet.union_3. +WS_apply HWS. intuition. +apply VertexSet.union_2. apply VertexSet.union_2. +WS_apply HWS. intuition. +Qed. + +(* The moves worklists is equal to the set of affinity edges *) +Lemma moves_AE : forall g palette ws, +WS_properties g palette ws -> +EdgeSet.Equal (AE g) (get_movesWL ws). + +Proof. +split; intros. +destruct ws. destruct p. destruct p. +simpl. WS_apply H. apply (proj1 (In_graph_aff_edge_in_AE _ _) H0). +generalize (In_move_props _ _ _ _ _ _ _ _ H0 (refl_equal _) H). intro H1. +apply (proj2 (In_graph_aff_edge_in_AE _ _) H1). +Qed. |