From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/Allocation.v | 92 ++++++++++++++++++++++++++-------------------------- 1 file changed, 46 insertions(+), 46 deletions(-) (limited to 'backend/Allocation.v') diff --git a/backend/Allocation.v b/backend/Allocation.v index 196a4075..7534e23f 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -34,7 +34,7 @@ Require Import RTLtyping. Require Import LTL. (** The validation algorithm used here is described in - "Validating register allocation and spilling", + "Validating register allocation and spilling", by Silvain Rideau and Xavier Leroy, in Compiler Construction (CC 2010), LNCS 6011, Springer, 2010. *) @@ -157,7 +157,7 @@ Definition classify_operation (op: operation) (args: list reg) : operation_kind | op, args => operation_other op args end. -(** Check RTL instruction [i] against LTL basic block [b]. +(** Check RTL instruction [i] against LTL basic block [b]. On success, return [Some] with a [block_shape] describing the correspondence. On error, return [None]. *) @@ -372,7 +372,7 @@ Module OrderedEquation <: OrderedType. (OrderedLoc.lt (eloc x) (eloc y) \/ (eloc x = eloc y /\ OrderedEqKind.lt (ekind x) (ekind y)))). Lemma eq_refl : forall x : t, eq x x. - Proof (@refl_equal t). + Proof (@refl_equal t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. Proof (@sym_equal t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. @@ -380,13 +380,13 @@ Module OrderedEquation <: OrderedType. Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. - destruct H. + destruct H. destruct H0. left; eapply Plt_trans; eauto. destruct H0. rewrite <- H0. auto. - destruct H. rewrite H. - destruct H0. auto. + destruct H. rewrite H. + destruct H0. auto. destruct H0. right; split; auto. - intuition. + intuition. left; eapply OrderedLoc.lt_trans; eauto. left; congruence. left; congruence. @@ -405,10 +405,10 @@ Module OrderedEquation <: OrderedType. destruct (OrderedPositive.compare (ereg x) (ereg y)). - apply LT. red; auto. - destruct (OrderedLoc.compare (eloc x) (eloc y)). - + apply LT. red; auto. + + apply LT. red; auto. + destruct (OrderedEqKind.compare (ekind x) (ekind y)). * apply LT. red; auto. - * apply EQ. red in e; red in e0; red in e1; red. + * apply EQ. red in e; red in e0; red in e1; red. destruct x; destruct y; simpl in *; congruence. * apply GT. red; auto. + apply GT. red; auto. @@ -416,7 +416,7 @@ Module OrderedEquation <: OrderedType. Defined. Definition eq_dec (x y: t) : {x = y} + {x <> y}. Proof. - intros. decide equality. + intros. decide equality. apply Loc.eq. apply peq. apply IndexedEqKind.eq. @@ -434,7 +434,7 @@ Module OrderedEquation' <: OrderedType. (Plt (ereg x) (ereg y) \/ (ereg x = ereg y /\ OrderedEqKind.lt (ekind x) (ekind y)))). Lemma eq_refl : forall x : t, eq x x. - Proof (@refl_equal t). + Proof (@refl_equal t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. Proof (@sym_equal t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. @@ -442,14 +442,14 @@ Module OrderedEquation' <: OrderedType. Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. - destruct H. - destruct H0. left; eapply OrderedLoc.lt_trans; eauto. + destruct H. + destruct H0. left; eapply OrderedLoc.lt_trans; eauto. destruct H0. rewrite <- H0. auto. - destruct H. rewrite H. - destruct H0. auto. + destruct H. rewrite H. + destruct H0. auto. destruct H0. right; split; auto. - intuition. - left; eapply Plt_trans; eauto. + intuition. + left; eapply Plt_trans; eauto. left; congruence. left; congruence. right; split. congruence. eapply OrderedEqKind.lt_trans; eauto. @@ -467,10 +467,10 @@ Module OrderedEquation' <: OrderedType. destruct (OrderedLoc.compare (eloc x) (eloc y)). - apply LT. red; auto. - destruct (OrderedPositive.compare (ereg x) (ereg y)). - + apply LT. red; auto. + + apply LT. red; auto. + destruct (OrderedEqKind.compare (ekind x) (ekind y)). * apply LT. red; auto. - * apply EQ. red in e; red in e0; red in e1; red. + * apply EQ. red in e; red in e0; red in e1; red. destruct x; destruct y; simpl in *; congruence. * apply GT. red; auto. + apply GT. red; auto. @@ -510,10 +510,10 @@ Program Definition add_equation (q: equation) (e: eqs) := mkeqs (EqSet.add q (eqs1 e)) (EqSet2.add q (eqs2 e)) _. Next Obligation. split; intros. - destruct (OrderedEquation'.eq_dec q q0). + destruct (OrderedEquation'.eq_dec q q0). apply EqSet.add_1; auto. apply EqSet.add_2. apply (eqs_same e). apply EqSet2.add_3 with q; auto. - destruct (OrderedEquation.eq_dec q q0). + destruct (OrderedEquation.eq_dec q q0). apply EqSet2.add_1; auto. apply EqSet2.add_2. apply (eqs_same e). apply EqSet.add_3 with q; auto. Qed. @@ -522,10 +522,10 @@ Program Definition remove_equation (q: equation) (e: eqs) := mkeqs (EqSet.remove q (eqs1 e)) (EqSet2.remove q (eqs2 e)) _. Next Obligation. split; intros. - destruct (OrderedEquation'.eq_dec q q0). + destruct (OrderedEquation'.eq_dec q q0). eelim EqSet2.remove_1; eauto. apply EqSet.remove_2; auto. apply (eqs_same e). apply EqSet2.remove_3 with q; auto. - destruct (OrderedEquation.eq_dec q q0). + destruct (OrderedEquation.eq_dec q q0). eelim EqSet.remove_1; eauto. apply EqSet2.remove_2; auto. apply (eqs_same e). apply EqSet.remove_3 with q; auto. Qed. @@ -585,7 +585,7 @@ Definition subst_reg_kind (r1: reg) (k1: equation_kind) (r2: reg) (k2: equation_ (** [subst_loc l1 l2 e] simulates the effect of assigning [l2] to [l1] on [e]. All equations of the form [r = l1 [kind]] are replaced by [r = l2 [kind]]. Return [None] if [e] contains an equation of the form [r = l] with [l] - partially overlapping [l1]. + partially overlapping [l1]. *) Definition subst_loc (l1 l2: loc) (e: eqs) : option eqs := @@ -784,7 +784,7 @@ Fixpoint can_undef (ml: list mreg) (e: eqs) : bool := Fixpoint can_undef_except (l: loc) (ml: list mreg) (e: eqs) : bool := match ml with | nil => true - | m1 :: ml => + | m1 :: ml => (Loc.eq l (R m1) || loc_unconstrained (R m1) e) && can_undef_except l ml e end. @@ -967,11 +967,11 @@ Definition transfer_aux (f: RTL.function) (env: regenv) track_moves env mv e1 | BSstore2 addr addr' args src mv1 args1' src1' mv2 args2' src2' s => assertion (can_undef (destroyed_by_store Mint32 addr') e); - do e1 <- add_equations args args2' + do e1 <- add_equations args args2' (add_equation (Eq kind_second_word src (R src2')) e); do e2 <- track_moves env mv2 e1; assertion (can_undef (destroyed_by_store Mint32 addr) e2); - do e3 <- add_equations args args1' + do e3 <- add_equations args args1' (add_equation (Eq kind_first_word src (R src1')) e2); track_moves env mv1 e3 | BScall sg ros args res mv1 ros' mv2 s => @@ -1059,22 +1059,22 @@ Module LEq <: SEMILATTICE. Lemma eq_refl: forall x, eq x x. Proof. - intros; destruct x; simpl; auto. red; tauto. + intros; destruct x; simpl; auto. red; tauto. Qed. Lemma eq_sym: forall x y, eq x y -> eq y x. Proof. - unfold eq; intros; destruct x; destruct y; auto. + unfold eq; intros; destruct x; destruct y; auto. red in H; red; intros. rewrite H; tauto. - Qed. + Qed. Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. Proof. unfold eq; intros. destruct x; destruct y; try contradiction; destruct z; auto. - red in H; red in H0; red; intros. rewrite H. auto. + red in H; red in H0; red; intros. rewrite H. auto. Qed. - Definition beq (x y: t) := + Definition beq (x y: t) := match x, y with | OK a, OK b => EqSet.equal a b | Error _, Error _ => true @@ -1083,14 +1083,14 @@ Module LEq <: SEMILATTICE. Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. - unfold beq, eq; intros. destruct x; destruct y. + unfold beq, eq; intros. destruct x; destruct y. apply EqSet.equal_2. auto. discriminate. discriminate. auto. Qed. - Definition ge (x y: t) := + Definition ge (x y: t) := match x, y with | OK a, OK b => EqSet.Subset b a | Error _, _ => True @@ -1099,18 +1099,18 @@ Module LEq <: SEMILATTICE. Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. - unfold eq, ge, EqSet.Equal, EqSet.Subset; intros. + unfold eq, ge, EqSet.Equal, EqSet.Subset; intros. destruct x; destruct y; auto. intros; rewrite H; auto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. Proof. unfold ge, EqSet.Subset; intros. destruct x; auto; destruct y; try contradiction. - destruct z; eauto. + destruct z; eauto. Qed. Definition bot: t := OK empty_eqs. - + Lemma ge_bot: forall x, ge x bot. Proof. unfold ge, bot, EqSet.Subset; simpl; intros. @@ -1126,25 +1126,25 @@ Module LEq <: SEMILATTICE. | Error _, _ => x end. Next Obligation. - split; intros. - apply EqSet2.union_1 in H. destruct H; rewrite eqs_same in H. + split; intros. + apply EqSet2.union_1 in H. destruct H; rewrite eqs_same in H. apply EqSet.union_2; auto. apply EqSet.union_3; auto. - apply EqSet.union_1 in H. destruct H; rewrite <- eqs_same in H. + apply EqSet.union_1 in H. destruct H; rewrite <- eqs_same in H. apply EqSet2.union_2; auto. apply EqSet2.union_3; auto. Qed. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. - unfold lub, ge, EqSet.Subset; intros. - destruct x; destruct y; auto. - intros; apply EqSet.union_2; auto. + unfold lub, ge, EqSet.Subset; intros. + destruct x; destruct y; auto. + intros; apply EqSet.union_2; auto. Qed. Lemma ge_lub_right: forall x y, ge (lub x y) y. Proof. - unfold lub, ge, EqSet.Subset; intros. - destruct x; destruct y; auto. - intros; apply EqSet.union_3; auto. + unfold lub, ge, EqSet.Subset; intros. + destruct x; destruct y; auto. + intros; apply EqSet.union_3; auto. Qed. End LEq. -- cgit