diff options
Diffstat (limited to 'backend/IRC_Graph_Functions.v')
| -rwxr-xr-x | backend/IRC_Graph_Functions.v | 548 |
1 files changed, 0 insertions, 548 deletions
diff --git a/backend/IRC_Graph_Functions.v b/backend/IRC_Graph_Functions.v deleted file mode 100755 index fc691aa..0000000 --- a/backend/IRC_Graph_Functions.v +++ /dev/null @@ -1,548 +0,0 @@ -Require Import FSets. -Require Import InterfGraphMapImp. -Require Import Spill_WL. -Require Import ZArith. -Require Import Simplify_WL. -Require Import Spill_WL. -Require Import Merge_WL. -Require Import Freeze_WL. -Require Import IRC_graph. -Require Import Edges. -Require Import Conservative_criteria. -Require Import WS. - -Import RegFacts Props OTFacts. - -Definition any_vertex := VertexSet.choose. - -(* simplify *) - -Definition simplify_irc r ircg H := -Make_IRC_Graph (remove_vertex r (irc_g ircg)) - (simplify_wl r ircg (irc_k ircg)) - (pal ircg) - (irc_k ircg) - (WS_simplify r ircg H) - (Hk ircg). - -Definition simplify g : option (Register.t * irc_graph) := -let simplifyWL := get_simplifyWL (irc_wl g) in -match any_vertex simplifyWL as v return (any_vertex simplifyWL = v -> option (Register.t * irc_graph)) with -|Some r => fun H : any_vertex simplifyWL = Some r => - Some (r, simplify_irc r g (VertexSet.choose_1 H)) -|None => fun H : any_vertex simplifyWL = None => None -end (refl_equal (any_vertex simplifyWL)). - -Lemma simplify_inv_aux : - forall g P, - match simplify g with - | Some x => - forall ( H : (any_vertex (get_simplifyWL (irc_wl g)) = Some (fst x))), - (simplify_irc (fst x) g (VertexSet.choose_1 H) = snd x) -> P - | None => - (any_vertex (get_simplifyWL (irc_wl g)) = None -> P) - end -> P. -Proof. - intros g P. - unfold simplify. - - set (simplifyWL := get_simplifyWL (irc_wl g)) in *. - set (Z := any_vertex simplifyWL) in *. - - refine - (match Z as W - return forall (H : Z = W), - -match - match W as v return (Z = v -> option (Register.t * irc_graph)) with - | Some r => - fun H : Z = Some r => Some (r, simplify_irc r g (VertexSet.choose_1 H)) - | None => fun _ : Z = None => None - end H -with -| Some x => forall H : Z = Some (fst x), simplify_irc (fst x) g (VertexSet.choose_1 H) = snd x -> P -| None => Z = None -> P -end -> P - - with - | Some x => _ - | None => _ - end _). - -simpl. intros. apply X with (H0 := H). reflexivity. -auto. -Qed. - -Lemma simplify_inv : forall g res, -simplify g = Some res -> -any_vertex (get_simplifyWL (irc_wl g)) = Some (fst res). -Proof. - intros. - apply simplify_inv_aux with g. - rewrite H. - auto. -Qed. - -Lemma simplify_inv2 : forall g res, -simplify g = Some res -> -exists H, snd res = simplify_irc (fst res) g (VertexSet.choose_1 H). - -Proof. -intros. -apply (simplify_inv_aux g). rewrite H. -simpl. intros. rewrite <-H1. -exists H0. reflexivity. -Qed. - -(* merge *) - -Definition merge_irc e ircg pin paff := -let g' := merge e (irc_g ircg) pin paff in -Make_IRC_Graph g' - (merge_wl3 e ircg g' pin paff) - (pal ircg) - (irc_k ircg) - (WS_coalesce _ _ pin paff) - (Hk ircg). - -Definition coalesce g : option (Edge.t * irc_graph) := -let movesWL := get_movesWL (irc_wl g) in -let graph := irc_g g in -let HWS := HWS_irc g in -let k := irc_k g in -match any_coalescible_edge movesWL graph k as e -return (any_coalescible_edge movesWL graph k = e -> option (Edge.t * irc_graph)) with -|Some edge => fun H : any_coalescible_edge movesWL graph k = Some edge => - let Hin := any_coalescible_edge_11 _ _ _ _ H in - let Hing := proj2 (In_move_props _ _ _ _ _ _ _ _ Hin (refl_equal _) HWS) in - let Haff := proj1 (In_move_props _ _ _ _ _ _ _ _ Hin (refl_equal _) HWS) in - Some (edge,merge_irc edge g Hing Haff) -|None => fun H : any_coalescible_edge movesWL graph k = None => None -end (refl_equal (any_coalescible_edge movesWL graph k)). - -Lemma coalesce_inv_aux : - forall g P, - match coalesce g with - | Some x => - forall (H : (any_coalescible_edge (get_movesWL (irc_wl g)) (irc_g g) (irc_k g) = Some (fst x))), - (merge_irc (fst x) g - (proj2 (In_move_props _ _ _ _ _ _ _ _ (any_coalescible_edge_11 _ _ _ _ H) (refl_equal _) (HWS_irc g))) - (proj1 (In_move_props _ _ _ _ _ _ _ _ (any_coalescible_edge_11 _ _ _ _ H) (refl_equal _) (HWS_irc g)))) - = snd x -> P - | None => - (any_coalescible_edge (get_movesWL (irc_wl g)) (irc_g g) (irc_k g) = None -> P) - end -> P. -Proof. - intros g P. - unfold coalesce. - - set (movesWL := get_movesWL (irc_wl g)) in *. - set (Z := any_coalescible_edge movesWL (irc_g g) (irc_k g)) in *. - - refine - (match Z as W - return forall (H : Z = W), - -match - match W as e return (Z = e -> option (Edge.t * irc_graph)) with - | Some edge => - fun H : Z = Some edge => Some (edge, -merge_irc edge g - (proj2 - (In_move_props edge (irc_g g) - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), movesWL) movesWL - (get_spillWL (irc_wl g)) (get_freezeWL (irc_wl g)) - (get_simplifyWL (irc_wl g)) (irc_k g) - (any_coalescible_edge_11 edge (irc_g g) (irc_k g) movesWL H) - (refl_equal - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), movesWL)) (HWS_irc g))) - (proj1 - (In_move_props edge (irc_g g) - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), movesWL) movesWL - (get_spillWL (irc_wl g)) (get_freezeWL (irc_wl g)) - (get_simplifyWL (irc_wl g)) (irc_k g) - (any_coalescible_edge_11 edge (irc_g g) (irc_k g) movesWL H) - (refl_equal - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), movesWL)) (HWS_irc g)))) - | None => fun _ : Z = None => None - end H -with -| Some x => - forall H : Z = Some (fst x), - merge_irc (fst x) g - (proj2 - (In_move_props (fst x) (irc_g g) - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), movesWL) movesWL - (get_spillWL (irc_wl g)) (get_freezeWL (irc_wl g)) - (get_simplifyWL (irc_wl g)) (irc_k g) - (any_coalescible_edge_11 (fst x) (irc_g g) (irc_k g) movesWL H) - (refl_equal - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), movesWL)) (HWS_irc g))) - (proj1 - (In_move_props (fst x) (irc_g g) - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), movesWL) movesWL - (get_spillWL (irc_wl g)) (get_freezeWL (irc_wl g)) - (get_simplifyWL (irc_wl g)) (irc_k g) - (any_coalescible_edge_11 (fst x) (irc_g g) (irc_k g) movesWL H) - (refl_equal - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), movesWL)) (HWS_irc g))) = snd x -> - P -| None => Z = None -> P -end -> P - with - | Some x => _ - | None => _ - end _). - -simpl. intros. apply X with (H0 := H). reflexivity. -auto. -Qed. - -Lemma coalesce_inv : forall g res, -coalesce g = Some res -> -any_coalescible_edge (get_movesWL (irc_wl g)) (irc_g g) (irc_k g) = Some (fst res). -Proof. - intros. - apply (coalesce_inv_aux g). - rewrite H. - auto. -Qed. - -Lemma coalesce_inv_2 : forall g res, -coalesce g = Some res -> -exists H, exists H', snd res = merge_irc (fst res) g H H'. - -Proof. -intros. -apply (coalesce_inv_aux g). -rewrite H. -simpl. intros. -exists ((proj2 - (In_move_props (fst res) (irc_g g) - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), get_movesWL (irc_wl g)) - (get_movesWL (irc_wl g)) (get_spillWL (irc_wl g)) - (get_freezeWL (irc_wl g)) (get_simplifyWL (irc_wl g)) - (irc_k g) - (any_coalescible_edge_11 (fst res) (irc_g g) (irc_k g) - (get_movesWL (irc_wl g)) H0) - (refl_equal - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), get_movesWL (irc_wl g))) - (HWS_irc g)))). -exists ((proj1 - (In_move_props (fst res) (irc_g g) - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), get_movesWL (irc_wl g)) - (get_movesWL (irc_wl g)) (get_spillWL (irc_wl g)) - (get_freezeWL (irc_wl g)) (get_simplifyWL (irc_wl g)) - (irc_k g) - (any_coalescible_edge_11 (fst res) (irc_g g) (irc_k g) - (get_movesWL (irc_wl g)) H0) - (refl_equal - (get_spillWL (irc_wl g), get_freezeWL (irc_wl g), - get_simplifyWL (irc_wl g), get_movesWL (irc_wl g))) - (HWS_irc g)))). -auto. -Qed. - -(* freeze *) - -Definition delete_preference_edges_irc2 v ircg Hing Hdep := -let k := irc_k ircg in -let g' := delete_preference_edges v (irc_g ircg) Hing in -Make_IRC_Graph g' - (delete_preferences_wl2 v ircg k) - (pal ircg) - (irc_k ircg) - (WS_freeze v ircg Hing Hdep) - (Hk ircg). - -Definition freeze g : option (Register.t * irc_graph) := -let freezeWL := get_freezeWL (irc_wl g) in -let graph := irc_g g in -let HWS := HWS_irc g in -match any_vertex freezeWL as r -return (any_vertex freezeWL = r -> option (Register.t*irc_graph)) with -|Some x => fun H : any_vertex freezeWL = Some x => - let Hin := VertexSet.choose_1 H in - let Hing := proj1 (proj2 (proj2 (In_freeze_props _ _ _ _ _ _ _ _ Hin (refl_equal _) HWS)))in - Some (x,delete_preference_edges_irc2 x g Hing Hin) -|None => fun H : any_vertex freezeWL = None => None -end (refl_equal (any_vertex freezeWL)). - -Lemma freeze_inv_aux : - forall g P, - match freeze g with - | Some x => - forall ( H : (any_vertex (get_freezeWL (irc_wl g)) = Some (fst x))), - (delete_preference_edges_irc2 (fst x) g - (proj1 (proj2 (proj2 (In_freeze_props _ _ _ _ _ _ _ _ (VertexSet.choose_1 H) (refl_equal _) (HWS_irc g))))) - (VertexSet.choose_1 H) = snd x) -> P - | None => - (any_vertex (get_freezeWL (irc_wl g)) = None -> P) - end -> P. - -Proof. - intros g P. - unfold freeze. - - set (freezeWL := get_freezeWL (irc_wl g)) in *. - set (Z := any_vertex freezeWL) in *. - - refine - (match Z as W - return forall (H : Z = W), - -match - match W as v return (Z = v -> option (Register.t * irc_graph)) with - | Some x => - fun H : Z = Some x => Some - (x, - delete_preference_edges_irc2 x g - (proj1 - (proj2 - (proj2 - (In_freeze_props x (irc_g g) - (get_spillWL (irc_wl g), freezeWL, - get_simplifyWL (irc_wl g), get_movesWL (irc_wl g)) - freezeWL (get_spillWL (irc_wl g)) - (get_simplifyWL (irc_wl g)) (get_movesWL (irc_wl g)) - (irc_k g) (VertexSet.choose_1 H) - (refl_equal - (get_spillWL (irc_wl g), freezeWL, - get_simplifyWL (irc_wl g), get_movesWL (irc_wl g))) - (HWS_irc g))))) (VertexSet.choose_1 H)) - | None => fun _ : Z = None => None - end H -with -| Some x => - -forall H : Z = Some (fst x), - delete_preference_edges_irc2 (fst x) g - (proj1 - (proj2 - (proj2 - (In_freeze_props (fst x) (irc_g g) - (get_spillWL (irc_wl g), freezeWL, - get_simplifyWL (irc_wl g), get_movesWL (irc_wl g)) freezeWL - (get_spillWL (irc_wl g)) (get_simplifyWL (irc_wl g)) - (get_movesWL (irc_wl g)) (irc_k g) - (VertexSet.choose_1 H) - (refl_equal - (get_spillWL (irc_wl g), freezeWL, - get_simplifyWL (irc_wl g), get_movesWL (irc_wl g))) - (HWS_irc g))))) (VertexSet.choose_1 H) = snd x -> P -| None => Z = None -> P -end -> P - with - | Some x => _ - | None => _ - end _). - -simpl. intros. apply X with (H0 := H). reflexivity. -auto. -Qed. - -Lemma freeze_inv : forall g res, -freeze g = Some res -> -any_vertex (get_freezeWL (irc_wl g)) = Some (fst res). -Proof. - intros. - apply freeze_inv_aux with g. - rewrite H. - auto. -Qed. - -Lemma freeze_inv2 : forall g res, -freeze g = Some res -> -exists H', exists H, snd res = delete_preference_edges_irc2 (fst res) g H H'. - -Proof. -intros. -apply (freeze_inv_aux g). rewrite H. -simpl. intros. rewrite <-H1. -exists (VertexSet.choose_1 H0). -exists (proj1 (proj2 (proj2 (In_freeze_props _ _ _ _ _ _ _ _ (VertexSet.choose_1 H0) (refl_equal _) (HWS_irc g))))). reflexivity. -Qed. - -(* spill *) -Definition spill_irc r ircg H := -Make_IRC_Graph (remove_vertex r (irc_g ircg)) - (spill_wl r ircg (irc_k ircg)) - (pal ircg) - (irc_k ircg) - (WS_spill r ircg H) - (Hk ircg). - -Definition cost_order (opt : (Register.t*nat*nat)) y g := -let (tmp, pref_card) := opt in -let (x, int_card) := tmp in -let y_int := VertexSet.cardinal (interference_adj y g) in -match lt_eq_lt_dec y_int int_card with -|inleft (left _) => opt -|inleft (right _) => let y_pref := VertexSet.cardinal (preference_adj y g) in - match le_lt_dec pref_card y_pref with - |left _ => opt - |right _ => (y, y_int, y_pref) - end -|inright _ => (y, y_int, VertexSet.cardinal (preference_adj y g)) -end. - -Definition lowest_cost_aux s g o := -VertexSet.fold (fun v o => match o with - | Some opt => Some (cost_order opt v g) - | None => Some (v, VertexSet.cardinal (interference_adj v g), - VertexSet.cardinal (preference_adj v g)) - end) - s - o. - -Definition lowest_cost s g := -match lowest_cost_aux s g None with -| Some r => Some (fst (fst r)) -| None => None -end. - -Lemma lowest_cost_aux_in : forall x s g o, -lowest_cost_aux s g o = Some x-> -VertexSet.In (fst (fst x)) s \/ o = Some x. - -Proof. -intros. unfold lowest_cost_aux in H. -set (f := (fun (v : VertexSet.elt) (o : option (MyRegisters.Regs.t * nat * nat)) => - match o with - | Some opt => Some (cost_order opt v g) - | None => - Some - (v, VertexSet.cardinal (interference_adj v g), - VertexSet.cardinal (preference_adj v g)) - end )) in *. -unfold VertexSet.elt in *. -fold f in H. -rewrite VertexSet.fold_1 in H. -set (f' := fun a e => f e a) in *. -unfold VertexSet.elt in *. fold f' in H. -generalize VertexSet.elements_2. intro HH. -generalize (HH s). clear HH. intro HH. -generalize x o H. clear H. -induction (VertexSet.elements s). intros x0 o0 H. -simpl in H. right. auto. -simpl. intros. -assert (VertexSet.In (fst (fst x0)) s \/ (f' o0 a) = Some x0). -apply IHl. -intros. apply HH. right. auto. -auto. -destruct H0. -left. auto. -unfold f' in H0. unfold f in H0. -case_eq o0; intros. -rewrite H1 in *. -case_eq (cost_order p a g); intros. -rewrite H2 in H0. unfold cost_order in H2. -destruct p. simpl in *. destruct p. simpl in *. -destruct (lt_eq_lt_dec (VertexSet.cardinal (interference_adj a g)) n1). destruct s0. -right. rewrite H2. auto. -destruct (le_lt_dec n0 (VertexSet.cardinal (preference_adj a g))). -right. rewrite H2. auto. -left. apply HH. left. destruct p0. simpl in *. -destruct x0. destruct p. simpl in *. -inversion H0. inversion H2. subst. intuition. -left. apply HH. left. destruct p0. simpl in *. -destruct x0. destruct p. simpl in *. -inversion H0. inversion H2. subst. intuition. -rewrite H1 in H0. -unfold f' in H. rewrite H1 in H. simpl in H. rewrite H0 in H. -fold f' in H. -left. apply HH. inversion H0. simpl. left. intuition. -Qed. - -Lemma lowest_cost_in : forall x s g, -lowest_cost s g = Some x -> -VertexSet.In x s. - -Proof. -intros. unfold lowest_cost in H. -case_eq (lowest_cost_aux s g None); intros; rewrite H0 in H. -generalize (lowest_cost_aux_in p s g None H0). intro. -destruct H1. inversion H. subst. auto. -congruence. -congruence. -Qed. - -Definition spill g : option (Register.t * irc_graph) := -let spillWL := get_spillWL (irc_wl g) in -match lowest_cost spillWL (irc_g g) as v return (lowest_cost spillWL (irc_g g) = v -> option (Register.t * irc_graph)) with -|Some r => fun H : lowest_cost spillWL (irc_g g) = Some r => - Some (r, spill_irc r g (lowest_cost_in _ _ _ H)) -|None => fun H : lowest_cost spillWL (irc_g g) = None => None -end (refl_equal (lowest_cost spillWL (irc_g g))). - -Lemma spill_inv_aux : - forall g P, - match spill g with - | Some x => - forall ( H : (lowest_cost (get_spillWL (irc_wl g)) (irc_g g) = Some (fst x))), - (spill_irc (fst x) g (lowest_cost_in _ _ _ H) = snd x) -> P - | None => - (lowest_cost (get_spillWL (irc_wl g)) (irc_g g) = None -> P) - end -> P. -Proof. - intros g P. - unfold spill. - - set (spillWL := get_spillWL (irc_wl g)) in *. - set (Z := lowest_cost spillWL (irc_g g)) in *. - - refine - (match Z as W - return forall (H : Z = W), - -match - match W as v return (Z = v -> option (Register.t * irc_graph)) with - | Some r => - fun H : Z = Some r => Some (r, spill_irc r g (lowest_cost_in _ _ _ H)) - | None => fun _ : Z = None => None - end H -with -| Some x => forall H : Z = Some (fst x), spill_irc (fst x) g (lowest_cost_in _ _ _ H) = snd x -> P -| None => Z = None -> P -end -> P - - with - | Some x => _ - | None => _ - end _). - -simpl. intros. apply X with (H0 := H). reflexivity. -auto. -Qed. - -Lemma spill_inv : forall g res, -spill g = Some res -> -lowest_cost (get_spillWL (irc_wl g)) (irc_g g) = Some (fst res). -Proof. - intros. - apply spill_inv_aux with g. - rewrite H. - auto. -Qed. - -Lemma spill_inv2 : forall g res, -spill g = Some res -> -exists H, snd res = spill_irc (fst res) g (lowest_cost_in (fst res) (get_spillWL (irc_wl g)) (irc_g g) H). - -Proof. -intros. -apply (spill_inv_aux g). rewrite H. -simpl. intros. rewrite <-H1. -exists H0. reflexivity. -Qed. |