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/Graph_Facts.v | 191 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 191 insertions(+) create mode 100755 backend/Graph_Facts.v (limited to 'backend/Graph_Facts.v') diff --git a/backend/Graph_Facts.v b/backend/Graph_Facts.v new file mode 100755 index 00000000..3919b1f3 --- /dev/null +++ b/backend/Graph_Facts.v @@ -0,0 +1,191 @@ +Require Import FSets. +Require Import InterfGraphMapImp. +Require Import ZArith. +Require Import Edges. +Require Import MyRegisters. + +Import Edge OTFacts. +Module Import RegFacts := Facts VertexSet. +Module Import RegRegFacts := Facts EdgeSet. + +(* Definition of useful morphisms *) + +Add Morphism In_graph : In_graph_m. + +Proof. +unfold In_graph;intros x y H g. +split;intro H0;[rewrite <-H|rewrite H];assumption. +Qed. + +Add Morphism In_graph_edge : In_graph_edge_m. + +Proof. +unfold In_graph_edge; intros x y H g. fold (eq x y) in H. +split;intro H0;[rewrite <-H|rewrite H];assumption. +Qed. + +Add Morphism move_related : move_related_m. + +Proof. +unfold move_related. intros. rewrite (compat_preference_adj _ _ _ H). reflexivity. +Qed. + +Add Morphism get_weight : get_weight_m. + +Proof. +intros x y H. +rewrite (weight_ordered_weight x);rewrite (weight_ordered_weight y). +unfold get_weight;unfold E.eq in H. +destruct H as [_ H];inversion H;[|rewrite H2];reflexivity. +Qed. + +(* Useful rewriting lemmas *) + +Lemma rewrite_fst : forall x y z, +fst_ext (x,y,z) = x. + +Proof. +auto. +Qed. + +Lemma rewrite_snd : forall x y z, +snd_ext (x,y,z) = y. + +Proof. +auto. +Qed. + +Lemma rewrite_weight : forall x y z, +get_weight (x,y,z) = z. + +Proof. +auto. +Qed. + +(* A rewriting tactic *) + +Ltac change_rewrite := +repeat (try rewrite rewrite_fst in *; + try rewrite rewrite_snd in *; + try rewrite rewrite_weight in *). + +(* Two tactics for proving equality of edges *) +Ltac Eq_eq := +apply eq_ordered_eq;unfold E.eq; +split;[simpl;split;auto; intuition |try apply OptionN_as_OT.eq_refl; intuition]. + +Ltac Eq_comm_eq := rewrite edge_comm; Eq_eq. + +(* Extensionnality of redirect *) +Lemma redirect_ext : forall e e' x y, +eq e e' -> +eq (redirect x y e) (redirect x y e'). + +Proof. +intros e e' x y H. +destruct e as [xe we];destruct xe as [ex1 ex2]; +destruct e' as [xe' we'];destruct xe' as [e'x1 e'x2];simpl in *. +generalize (get_weight_m _ _ H);simpl;intro Heq;subst. +destruct (eq_charac _ _ H);destruct H0 as [H0 H1];unfold redirect;change_rewrite. +destruct (OTFacts.eq_dec ex1 x). +destruct (OTFacts.eq_dec e'x1 x). +Eq_eq. intuition. +elim (n (Regs.eq_trans (Regs.eq_sym H0) r)). +destruct (OTFacts.eq_dec e'x1 x). +elim (n (Regs.eq_trans H0 r)). +destruct (OTFacts.eq_dec ex2 x). +destruct (OTFacts.eq_dec e'x2 x). +Eq_eq. intuition. +elim (n1 (Regs.eq_trans (Regs.eq_sym H1) r)). +destruct (OTFacts.eq_dec e'x2 x). +elim (n1 (Regs.eq_trans H1 r)). +Eq_eq. +destruct (OTFacts.eq_dec ex1 x). +destruct (OTFacts.eq_dec e'x1 x). +Eq_eq. intuition. +apply (Regs.eq_trans H1 (Regs.eq_trans r0 (Regs.eq_trans (Regs.eq_sym r) H0))). +destruct (OTFacts.eq_dec e'x2 x). +Eq_comm_eq. intuition. +elim (n0 (Regs.eq_trans (Regs.eq_sym H0) r)). +destruct (OTFacts.eq_dec e'x2 x). +elim (n (Regs.eq_trans H0 r)). +destruct (OTFacts.eq_dec ex2 x). +destruct (OTFacts.eq_dec e'x1 x). +Eq_comm_eq. +elim (n1 (Regs.eq_trans (Regs.eq_sym H1) r)). +destruct (OTFacts.eq_dec e'x1 x). +elim (n1 (Regs.eq_trans H1 r)). +Eq_comm_eq. +Qed. + +(* The weight is left unchanged while applying redirect *) +Lemma redirect_weight_eq : forall e x y, +Edge.get_weight (redirect x y e) = Edge.get_weight e. + +Proof. +unfold redirect;intros e x y;destruct e as [e w];destruct e as [ex1 ex2];change_rewrite. +destruct (OTFacts.eq_dec ex1 x);destruct (OTFacts.eq_dec ex2 x);reflexivity. +Qed. + +(* Specification of redirect *) +Lemma redirect_charac : forall e x y, +(eq e (redirect x y e) /\ (~Regs.eq x (fst_ext e) /\ ~Regs.eq x (snd_ext e))) \/ +(eq (y, snd_ext e, get_weight e) (redirect x y e) /\ Regs.eq x (fst_ext e)) \/ +(eq (fst_ext e, y, get_weight e) (redirect x y e) /\ Regs.eq x (snd_ext e)). + +Proof. +intros e x y. +unfold redirect. change_rewrite. +destruct (OTFacts.eq_dec (fst_ext e) x). +right. left. split. apply eq_refl. auto. +destruct (OTFacts.eq_dec (snd_ext e) x). +right. right. split. apply eq_refl. auto. +left. split. apply eq_refl. split; intuition. +Qed. + +(* Weak equality implies equality for interference edges *) +Lemma weak_eq_interf_eq : forall x y, +weak_eq x y -> +interf_edge x -> +interf_edge y -> +eq x y. + +Proof. +unfold weak_eq, interf_edge, get_weight. intros. destruct H; destruct H. +Eq_eq. rewrite H0. rewrite H1. apply OptionN_as_OT.eq_refl. +rewrite (edge_eq x). rewrite (edge_eq y). +Eq_comm_eq. simpl. unfold get_weight. +rewrite H0. rewrite H1. apply OptionN_as_OT.eq_refl. +Qed. + +(* The second endpoint of e does not belongs to (merge e g H H0) *) +Lemma not_in_merge_snd : forall e g H H0, +~In_graph (snd_ext e) (merge e g H H0). + +Proof. +intros. intro. +rewrite In_merge_vertex in H1. destruct H1. +elim (H2 (Regs.eq_refl _)). +Qed. + +(* Extensionnality of the low-degree function *) +Lemma compat_bool_low : forall g K, +compat_bool Regs.eq (has_low_degree g K). + +Proof. +unfold compat_bool, has_low_degree, interf_degree. intros. +rewrite (compat_interference_adj _ _ _ H). reflexivity. +Qed. + +(* There cannot exist both an interference and + a preference between two vertices *) +Lemma interf_pref_conflict : forall x y g, +Prefere x y g /\ Interfere x y g -> False. + +Proof. +unfold Prefere, Interfere. intros. destruct H. destruct H. +assert (eq (x,y,Some x0) (x,y,None)). +apply is_simple_graph with (g:=g); auto. +unfold weak_eq. left. change_rewrite. split; auto. +generalize (get_weight_m _ _ H1). simpl. congruence. +Qed. -- cgit