diff options
Diffstat (limited to 'backend/IRC_Graph_Functions.v')
| -rwxr-xr-x | backend/IRC_Graph_Functions.v | 548 |
1 files changed, 548 insertions, 0 deletions
diff --git a/backend/IRC_Graph_Functions.v b/backend/IRC_Graph_Functions.v new file mode 100755 index 00000000..fc691aa2 --- /dev/null +++ b/backend/IRC_Graph_Functions.v @@ -0,0 +1,548 @@ +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. |