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 ------------------------------------------------- 1 file changed, 175 deletions(-) (limited to 'backend/CSE3analysis.v') 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. -- cgit