From 3c34c386912e904b432c53e1dbb2b3dda3f8501f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 9 Mar 2020 16:23:36 +0100 Subject: moved stuff around --- backend/CSE3analysis.v | 175 -------------------------------------------- backend/CSE3analysisproof.v | 157 ++++++++++++++++++++++++++++++++++++++- 2 files changed, 155 insertions(+), 177 deletions(-) diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 92d9202a..257149b5 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -93,57 +93,9 @@ Definition eq_id := positive. Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := Regmap.set i (PSet.add j (Regmap.get i m)) m. -Lemma add_i_j_adds : forall i j m, - PSet.contains (Regmap.get i (add_i_j i j m)) j = true. -Proof. - intros. - unfold add_i_j. - rewrite Regmap.gss. - auto with pset. -Qed. -Hint Resolve add_i_j_adds: cse3. - -Lemma add_i_j_monotone : forall i j i' j' m, - PSet.contains (Regmap.get i' m) j' = true -> - PSet.contains (Regmap.get i' (add_i_j i j m)) j' = true. -Proof. - intros. - unfold add_i_j. - destruct (peq i i'). - - subst i'. - rewrite Regmap.gss. - destruct (peq j j'). - + subst j'. - apply PSet.gadds. - + eauto with pset. - - rewrite Regmap.gso. - assumption. - congruence. -Qed. - -Hint Resolve add_i_j_monotone: cse3. - Definition add_ilist_j (ilist : list reg) (j : eq_id) (m : Regmap.t PSet.t) := List.fold_left (fun already i => add_i_j i j already) ilist m. -Lemma add_ilist_j_monotone : forall ilist j i' j' m, - PSet.contains (Regmap.get i' m) j' = true -> - PSet.contains (Regmap.get i' (add_ilist_j ilist j m)) j' = true. -Proof. - induction ilist; simpl; intros until m; intro CONTAINS; auto with cse3. -Qed. -Hint Resolve add_ilist_j_monotone: cse3. - -Lemma add_ilist_j_adds : forall ilist j m, - forall i, In i ilist -> - PSet.contains (Regmap.get i (add_ilist_j ilist j m)) j = true. -Proof. - induction ilist; simpl; intros until i; intro IN. - contradiction. - destruct IN as [HEAD | TAIL]; subst; auto with cse3. -Qed. -Hint Resolve add_ilist_j_adds: cse3. - Definition get_kills (eqs : PTree.t equation) : Regmap.t PSet.t := PTree.fold (fun already (eqno : eq_id) (eq : equation) => @@ -151,131 +103,4 @@ Definition get_kills (eqs : PTree.t equation) : (add_ilist_j (eq_args eq) eqno already)) eqs (PMap.init PSet.empty). -Definition xlget_kills (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) : - Regmap.t PSet.t := - List.fold_left (fun already (item : eq_id * equation) => - add_i_j (eq_lhs (snd item)) (fst item) - (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m. - -Lemma xlget_kills_monotone : - forall eqs m i j, - PSet.contains (Regmap.get i m) j = true -> - PSet.contains (Regmap.get i (xlget_kills eqs m)) j = true. -Proof. - induction eqs; simpl; trivial. - intros. - auto with cse3. -Qed. - -Hint Resolve xlget_kills_monotone : cse3. - -Lemma xlget_kills_has_lhs : - forall eqs m lhs sop args j, - In (j, {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |}) eqs -> - PSet.contains (Regmap.get lhs (xlget_kills eqs m)) j = true. -Proof. - induction eqs; simpl. - contradiction. - intros until j. - intro HEAD_TAIL. - destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl. - - auto with cse3. - - eapply IHeqs. eassumption. -Qed. -Hint Resolve xlget_kills_has_lhs : cse3. - -Lemma xlget_kills_has_arg : - forall eqs m lhs sop arg args j, - In (j, {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |}) eqs -> - In arg args -> - PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true. -Proof. - induction eqs; simpl. - contradiction. - intros until j. - intros HEAD_TAIL ARG. - destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl. - - auto with cse3. - - eapply IHeqs; eassumption. -Qed. - -Hint Resolve xlget_kills_has_arg : cse3. - - -Lemma get_kills_has_lhs : - forall eqs lhs sop args j, - PTree.get j eqs = Some {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> - PSet.contains (Regmap.get lhs (get_kills eqs)) j = true. -Proof. - unfold get_kills. - intros. - rewrite PTree.fold_spec. - change (fold_left - (fun (a : Regmap.t PSet.t) (p : positive * equation) => - add_i_j (eq_lhs (snd p)) (fst p) - (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. - eapply xlget_kills_has_lhs. - apply PTree.elements_correct. - eassumption. -Qed. - -Lemma get_kills_has_arg : - forall eqs lhs sop arg args j, - PTree.get j eqs = Some {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> - In arg args -> - PSet.contains (Regmap.get arg (get_kills eqs)) j = true. -Proof. - unfold get_kills. - intros. - rewrite PTree.fold_spec. - change (fold_left - (fun (a : Regmap.t PSet.t) (p : positive * equation) => - add_i_j (eq_lhs (snd p)) (fst p) - (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. - eapply xlget_kills_has_arg. - - apply PTree.elements_correct. - eassumption. - - assumption. -Qed. - -(* -Lemma xget_kills_monotone : - forall eqs m i j, - PSet.contains (Regmap.get i m) j = true -> - PSet.contains (Regmap.get i (xget_kills eqs m)) j = true. -Proof. - unfold xget_kills. - intros eqs m. - rewrite PTree.fold_spec. - generalize (PTree.elements eqs). - intro. - generalize m. - clear m. - induction l; simpl; trivial. - intros. - apply IHl. - apply add_i_j_monotone. - apply add_ilist_j_monotone. - assumption. -Qed. -*) -Lemma xget_kills_has_lhs : - forall eqs m lhs sop args j, - PTree.get j eqs = Some {| eq_lhs := lhs; - eq_op := sop; - eq_args:= args |} -> - PSet.contains (Regmap.get lhs (xget_kills eqs m)) j = true. - -Definition eq_involves (eq : equation) (i : reg) := - i = (eq_lhs eq) \/ In i (eq_args eq). - - Definition totoro := RELATION.lub. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index f864377e..af42a2e8 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -6,15 +6,162 @@ Require Import Memory Registers Op RTL Maps. Require Import Globalenvs Values. Require Import Linking Values Memory Globalenvs Events Smallstep. Require Import Registers Op RTL. -Require Import CSE3analysis CSE2deps CSE2depsproof. +Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet. Require Import Lia. +Lemma add_i_j_adds : forall i j m, + PSet.contains (Regmap.get i (add_i_j i j m)) j = true. +Proof. + intros. + unfold add_i_j. + rewrite Regmap.gss. + auto with pset. +Qed. +Hint Resolve add_i_j_adds: cse3. + +Lemma add_i_j_monotone : forall i j i' j' m, + PSet.contains (Regmap.get i' m) j' = true -> + PSet.contains (Regmap.get i' (add_i_j i j m)) j' = true. +Proof. + intros. + unfold add_i_j. + destruct (peq i i'). + - subst i'. + rewrite Regmap.gss. + destruct (peq j j'). + + subst j'. + apply PSet.gadds. + + eauto with pset. + - rewrite Regmap.gso. + assumption. + congruence. +Qed. + +Hint Resolve add_i_j_monotone: cse3. + +Lemma add_ilist_j_monotone : forall ilist j i' j' m, + PSet.contains (Regmap.get i' m) j' = true -> + PSet.contains (Regmap.get i' (add_ilist_j ilist j m)) j' = true. +Proof. + induction ilist; simpl; intros until m; intro CONTAINS; auto with cse3. +Qed. +Hint Resolve add_ilist_j_monotone: cse3. + +Lemma add_ilist_j_adds : forall ilist j m, + forall i, In i ilist -> + PSet.contains (Regmap.get i (add_ilist_j ilist j m)) j = true. +Proof. + induction ilist; simpl; intros until i; intro IN. + contradiction. + destruct IN as [HEAD | TAIL]; subst; auto with cse3. +Qed. +Hint Resolve add_ilist_j_adds: cse3. + +Definition xlget_kills (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) : + Regmap.t PSet.t := + List.fold_left (fun already (item : eq_id * equation) => + add_i_j (eq_lhs (snd item)) (fst item) + (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m. + +Lemma xlget_kills_monotone : + forall eqs m i j, + PSet.contains (Regmap.get i m) j = true -> + PSet.contains (Regmap.get i (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + auto with cse3. +Qed. + +Hint Resolve xlget_kills_monotone : cse3. + +Lemma xlget_kills_has_lhs : + forall eqs m lhs sop args j, + In (j, {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |}) eqs -> + PSet.contains (Regmap.get lhs (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros until j. + intro HEAD_TAIL. + destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl. + - auto with cse3. + - eapply IHeqs. eassumption. +Qed. +Hint Resolve xlget_kills_has_lhs : cse3. + +Lemma xlget_kills_has_arg : + forall eqs m lhs sop arg args j, + In (j, {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |}) eqs -> + In arg args -> + PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros until j. + intros HEAD_TAIL ARG. + destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl. + - auto with cse3. + - eapply IHeqs; eassumption. +Qed. + +Hint Resolve xlget_kills_has_arg : cse3. + +Lemma get_kills_has_lhs : + forall eqs lhs sop args j, + PTree.get j eqs = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + PSet.contains (Regmap.get lhs (get_kills eqs)) j = true. +Proof. + unfold get_kills. + intros. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : Regmap.t PSet.t) (p : positive * equation) => + add_i_j (eq_lhs (snd p)) (fst p) + (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. + eapply xlget_kills_has_lhs. + apply PTree.elements_correct. + eassumption. +Qed. + +Lemma get_kills_has_arg : + forall eqs lhs sop arg args j, + PTree.get j eqs = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + In arg args -> + PSet.contains (Regmap.get arg (get_kills eqs)) j = true. +Proof. + unfold get_kills. + intros. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : Regmap.t PSet.t) (p : positive * equation) => + add_i_j (eq_lhs (snd p)) (fst p) + (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills. + eapply xlget_kills_has_arg. + - apply PTree.elements_correct. + eassumption. + - assumption. +Qed. + +Definition eq_involves (eq : equation) (i : reg) := + i = (eq_lhs eq) \/ In i (eq_args eq). + Section SOUNDNESS. Variable F V : Type. Variable genv: Genv.t F V. Variable sp : val. - Definition eq_sem (eq : equation) (rs : regset) (m : mem) := + Variable eq_catalog : PTree.t equation. + + Definition sem_eq (eq : equation) (rs : regset) (m : mem) := match eq_op eq with | SOp op => match eval_operation genv sp op (rs ## (eq_args eq)) m with @@ -32,4 +179,10 @@ Section SOUNDNESS. | None => rs # (eq_lhs eq) = default_notrap_load_value chunk end end. + + Definition sem_rel (rel : RELATION.t) (rs : regset) (m : mem) := + forall i eq, + PSet.contains rel i = true -> + PTree.get i eq_catalog = Some eq -> + sem_eq eq rs m. End SOUNDNESS. -- cgit