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/Spill_WL.v | 141 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 141 insertions(+) create mode 100755 backend/Spill_WL.v (limited to 'backend/Spill_WL.v') diff --git a/backend/Spill_WL.v b/backend/Spill_WL.v new file mode 100755 index 00000000..1ed1c2d9 --- /dev/null +++ b/backend/Spill_WL.v @@ -0,0 +1,141 @@ +Require Import FSets. +Require Import InterfGraphMapImp. +Require Import Freeze_WL. +Require Import Edges. +Require Import WS. +Require Import Interference_adjacency. +Require Import Affinity_relation. +Require Import Remove_Vertex_WL. +Require Import IRC_graph. + +Import RegFacts Props OTFacts. + +Definition spill_wl r ircg K := + let g := irc_g ircg in + let wl := irc_wl ircg in + let simplify := get_simplifyWL wl in + let freeze := get_freezeWL wl in + let spillWL := get_spillWL wl in + let movesWL := get_movesWL wl in + let pre := precolored g in + let int_adj := interference_adj r g in + let not_pre_int_adj := VertexSet.diff int_adj pre in + let pre_adj := preference_adj r g in + let not_pre_pre_adj := VertexSet.diff pre_adj pre in + let newlow := VertexSet.filter (fun x => eq_K K (VertexSet.cardinal (interference_adj x g))) not_pre_int_adj in + let (free, simp) := VertexSet.partition (move_related g) newlow in + let newnmr := VertexSet.filter (fun x => eq_K 1 (VertexSet.cardinal (preference_adj x g)) && has_low_degree g K x) not_pre_pre_adj in + let simplifyWL__ := VertexSet.union simplify simp in + let simplifyWL' := VertexSet.union simplifyWL__ newnmr in + let freezeWL__ := VertexSet.diff freeze newnmr in + let freezeWL' := VertexSet.union freezeWL__ free in + let spillWL_ := VertexSet.diff spillWL newlow in + let spillWL' := VertexSet.remove r spillWL_ in + let movesWL' := not_incident_edges r movesWL g in + (spillWL', freezeWL', simplifyWL', movesWL'). + + +Lemma WS_spill_aux : forall r ircg, +VertexSet.In r (get_spillWL (irc_wl ircg)) -> +WS_properties (remove_vertex r (irc_g ircg)) (VertexSet.cardinal (pal ircg)) + (spill_wl r ircg (VertexSet.cardinal (pal ircg))). + +Proof. +intros. +generalize (WS_props_equal (remove_vertex r (irc_g ircg)) (VertexSet.cardinal (pal ircg)) + (remove_wl_2 r ircg (VertexSet.cardinal (pal ircg))) + (spill_wl r ircg (VertexSet.cardinal (pal ircg)))). +generalize (WS_remove_wl_2 r ircg). +unfold remove_wl_2, spill_wl, get_simplifyWL, + get_freezeWL, get_spillWL, get_movesWL. +set (g' := remove_vertex r (irc_g ircg)) in *. +set (k := VertexSet.cardinal (pal ircg)) in *. +set (g := irc_g ircg) in *. +set (wl := irc_wl ircg) in *. +set ( simplify := get_simplifyWL wl ) in *. +set ( freeze := get_freezeWL wl ) in *. +set ( spillWL := get_spillWL wl ) in *. +set ( int_adj := interference_adj r g ) in *. +set ( not_pre_int_adj := VertexSet.diff int_adj (precolored g) ) in *. +set ( pre_adj := preference_adj r g ) in *. +set ( not_pre_pre_adj := VertexSet.diff pre_adj (precolored g) ) in *. +set ( low := VertexSet.filter (fun x => eq_K k (VertexSet.cardinal (interference_adj x g))) not_pre_int_adj ) in *. +set ( simpfree := VertexSet.partition (move_related g) low ) in *. +case_eq simpfree. intros free simp Hsf. +unfold simpfree in Hsf. +set ( nmr := VertexSet.filter (fun x => eq_K 1 (VertexSet.cardinal (preference_adj x g)) && has_low_degree g k x) not_pre_pre_adj) in *. +set ( simplifyWL__ := VertexSet.union simplify simp ) in *. +set ( simplifyWL_ := VertexSet.union simplifyWL__ nmr) in *. +set ( simplifyWL' := VertexSet.remove r simplifyWL_ ) in *. +set ( freezeWL__ := VertexSet.diff freeze nmr ) in *. +set ( freezeWL_ := VertexSet.union freezeWL__ free ) in *. +set ( freezeWL' := VertexSet.remove r freezeWL_ ) in *. +set ( spillWL_ := VertexSet.diff spillWL low ) in *. +set ( spillWL' := VertexSet.remove r spillWL_ ) in *. +set ( movesWL' := not_incident_edges r (get_movesWL wl) g) in *. simpl. +generalize (In_spill_props _ _ _ _ _ _ _ _ H (refl_equal _) (HWS_irc ircg)). intro Hr. + +intros HWS H0. apply H0. + +(* r is not removed from simplify *) +split; intros. +apply (VertexSet.remove_3 H1). + +apply VertexSet.remove_2. intro. rewrite <-H2 in H1. clear H2. +destruct (VertexSet.union_1 H1). +destruct (VertexSet.union_1 H2). +generalize (In_simplify_props _ _ _ _ _ _ _ _ H3 (refl_equal _) (HWS_irc ircg)). intro. +destruct H4. destruct Hr. rewrite H4 in H6. inversion H6. + +assert (simp = snd (VertexSet.partition (move_related g) low)) as Hsimp. +rewrite Hsf. auto. rewrite Hsimp in H3. +rewrite VertexSet.partition_2 in H3. +generalize (VertexSet.filter_1 (compat_not_compat (compat_bool_move _)) H3). intro. +unfold low in H4. generalize (VertexSet.filter_1 (eq_K_compat _ _) H4). intro. +elim (not_in_interf_self r g). apply (VertexSet.diff_1 H5). +apply compat_bool_move. + +unfold nmr in H2. generalize (VertexSet.filter_1 (compat_move_up _ _) H2). intro. +elim (not_in_pref_self r g (VertexSet.diff_1 H3)). +assumption. + +(* r is not deleted from freezewl, since it is not move-related and + no vertex is removed from freeze, since free is empty, because + preference adj r g is empty *) + +set (s := VertexSet.union (VertexSet.diff (snd (fst (fst wl))) nmr) free). +split; intros. +apply (VertexSet.remove_3 H1). + +apply VertexSet.remove_2. intro. rewrite <-H2 in H1. clear H2. +unfold s in H1. +destruct (VertexSet.union_1 H1). +generalize (In_freeze_props _ _ _ _ _ _ _ _ (VertexSet.diff_1 H2) (refl_equal _) (HWS_irc ircg)). intro. +destruct H3. destruct Hr. rewrite H5 in H3. inversion H3. + +assert (free = fst (VertexSet.partition (move_related g) low)). +rewrite Hsf. auto. +rewrite H3 in H2. rewrite VertexSet.partition_1 in H2. +generalize (VertexSet.filter_1 (compat_bool_move _ ) H2). intro. +unfold low in H4. generalize (VertexSet.filter_1 (eq_K_compat _ _) H4). intro. +elim (not_in_interf_self r g). apply (VertexSet.diff_1 H5). +apply compat_bool_move. assumption. + +(* spill worklist is unchanged *) +apply VertexSet.eq_refl. + +(* moves worklst is unchanged *) +apply EdgeSet.eq_refl. + +(* WS_remove_wl respects the invariant *) +assumption. +Qed. + +Lemma WS_spill : forall r ircg, +VertexSet.In r (get_spillWL (irc_wl ircg)) -> +WS_properties (remove_vertex r (irc_g ircg)) (irc_k ircg) + (spill_wl r ircg (irc_k ircg)). + +Proof. +intros. rewrite <-(Hk ircg). apply WS_spill_aux. auto. +Qed. -- cgit