Updated PR by removing whitespaces. Bug 17450.

1 files changed, 65 insertions, 65 deletions

diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index aac37dc6..eb68f586 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -51,7 +51,7 @@ Lemma match_G:
   forall r id ofs,
   AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (Genv.symbol_address ge id ofs).
 Proof.
-  intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. 
+  intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH.
 Qed.
 
 Lemma match_S:
@@ -63,9 +63,9 @@ Qed.
 
 Ltac InvApproxRegs :=
   match goal with
-  | [ H: _ :: _ = _ :: _ |- _ ] => 
+  | [ H: _ :: _ = _ :: _ |- _ ] =>
         injection H; clear H; intros; InvApproxRegs
-  | [ H: ?v = AE.get ?r ae |- _ ] => 
+  | [ H: ?v = AE.get ?r ae |- _ ] =>
         generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs
   | _ => idtac
   end.
@@ -86,11 +86,11 @@ Ltac SimplVM :=
       rewrite E in *; clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
       let E := fresh in
-      assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
+      assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto);
       clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] =>
       let E := fresh in
-      assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto); 
+      assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto);
       clear H; SimplVM
   | _ => idtac
   end.
@@ -114,20 +114,20 @@ Lemma make_cmp_base_correct:
   forall c args vl,
   vl = map (fun r => AE.get r ae) args ->
   let (op', args') := make_cmp_base c args vl in
-  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
 Proof.
-  intros. unfold make_cmp_base. 
-  generalize (cond_strength_reduction_correct c args vl H). 
+  intros. unfold make_cmp_base.
+  generalize (cond_strength_reduction_correct c args vl H).
   destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ.
-  econstructor; split. simpl; eauto. rewrite EQ. auto. 
+  econstructor; split. simpl; eauto. rewrite EQ. auto.
 Qed.
 
 Lemma make_cmp_correct:
   forall c args vl,
   vl = map (fun r => AE.get r ae) args ->
   let (op', args') := make_cmp c args vl in
-  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
 Proof.
   intros c args vl.
@@ -136,20 +136,20 @@ Proof.
   { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
   unfold make_cmp. case (make_cmp_match c args vl); intros.
 - destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (rs#r1); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   apply make_cmp_base_correct; auto.
 - destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (rs#r1); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   apply make_cmp_base_correct; auto.
@@ -162,7 +162,7 @@ Lemma make_addimm_correct:
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v.
 Proof.
   intros. unfold make_addimm.
-  predSpec Int.eq Int.eq_spec n Int.zero; intros. 
+  predSpec Int.eq Int.eq_spec n Int.zero; intros.
   subst. exists (rs#r); split; auto. destruct (rs#r); simpl; auto; rewrite Int.add_zero; auto.
   exists (Val.add rs#r (Vint n)); auto.
 Qed.
@@ -177,7 +177,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shl_zero. auto.
   destruct (Int.ltu n Int.iwordsize) eqn:?; intros.
-  rewrite Val.shl_rolm; auto. econstructor; split; eauto. auto. 
+  rewrite Val.shl_rolm; auto. econstructor; split; eauto. auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
 
@@ -205,7 +205,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shru_zero. auto.
   destruct (Int.ltu n Int.iwordsize) eqn:?; intros.
-  rewrite Val.shru_rolm; auto. econstructor; split; eauto. auto. 
+  rewrite Val.shru_rolm; auto. econstructor; split; eauto. auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
 
@@ -221,10 +221,10 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.one; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_one; auto.
   destruct (Int.is_power2 n) eqn:?; intros.
-  rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). rewrite Val.shl_rolm. 
-  econstructor; split; eauto. auto. 
+  rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). rewrite Val.shl_rolm.
+  econstructor; split; eauto. auto.
   eapply Int.is_power2_range; eauto.
-  econstructor; split; eauto. auto. 
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_divimm_correct:
@@ -235,9 +235,9 @@ Lemma make_divimm_correct:
   exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divimm.
-  destruct (Int.is_power2 n) eqn:?. 
+  destruct (Int.is_power2 n) eqn:?.
   destruct (Int.ltu i (Int.repr 31)) eqn:?.
-  exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. 
+  exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence.
   exists v; auto.
   exists v; auto.
 Qed.
@@ -250,11 +250,11 @@ Lemma make_divuimm_correct:
   exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divuimm.
-  destruct (Int.is_power2 n) eqn:?. 
+  destruct (Int.is_power2 n) eqn:?.
   econstructor; split. simpl; eauto.
   exploit Int.is_power2_range; eauto. intros RANGE.
-  rewrite <- Val.shru_rolm; auto. rewrite H0 in H. 
-  destruct (rs#r1); simpl in *; inv H. 
+  rewrite <- Val.shru_rolm; auto. rewrite H0 in H.
+  destruct (rs#r1); simpl in *; inv H.
   destruct (Int.eq n Int.zero); inv H2.
   rewrite RANGE. rewrite (Int.divu_pow2 i0 _ _ Heqo). auto.
   exists v; auto.
@@ -273,17 +273,17 @@ Proof.
   subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto.
   destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero
                        | _ => false end) eqn:UNS.
-  destruct x; try congruence. 
+  destruct x; try congruence.
   exists (rs#r); split; auto.
   inv H; auto. simpl. replace (Int.and i n) with i; auto.
   generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ.
   Int.bit_solve. destruct (zlt i0 n0).
   replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
-  rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. 
-  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. 
-  rewrite Int.bits_not by auto. apply negb_involutive. 
-  rewrite H6 by auto. auto. 
-  econstructor; split; eauto. auto. 
+  rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
+  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
+  rewrite Int.bits_not by auto. apply negb_involutive.
+  rewrite H6 by auto. auto.
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_orimm_correct:
@@ -296,7 +296,7 @@ Proof.
   subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.or_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
   subst n. exists (Vint Int.mone); split; auto. destruct (rs#r); simpl; auto. rewrite Int.or_mone; auto.
-  econstructor; split; eauto. auto. 
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_xorimm_correct:
@@ -306,10 +306,10 @@ Lemma make_xorimm_correct:
 Proof.
   intros; unfold make_xorimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto. 
+  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
-  subst n. exists (Val.notint rs#r); split; auto. 
-  econstructor; split; eauto. auto. 
+  subst n. exists (Val.notint rs#r); split; auto.
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_mulfimm_correct:
@@ -318,11 +318,11 @@ Lemma make_mulfimm_correct:
   let (op, args) := make_mulfimm n r1 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfimm. 
-  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfimm.
+  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfimm_correct_2:
@@ -331,12 +331,12 @@ Lemma make_mulfimm_correct_2:
   let (op, args) := make_mulfimm n r2 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfimm. 
-  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfimm.
+  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto. 
-  rewrite Float.mul_commut; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto.
+  rewrite Float.mul_commut; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfsimm_correct:
@@ -345,11 +345,11 @@ Lemma make_mulfsimm_correct:
   let (op, args) := make_mulfsimm n r1 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfsimm. 
-  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfsimm.
+  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r1); simpl; auto. rewrite Float32.mul2_add; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r1); simpl; auto. rewrite Float32.mul2_add; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfsimm_correct_2:
@@ -358,12 +358,12 @@ Lemma make_mulfsimm_correct_2:
   let (op, args) := make_mulfsimm n r2 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfsimm. 
-  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfsimm.
+  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r2); simpl; auto. rewrite Float32.mul2_add; auto. 
-  rewrite Float32.mul_commut; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r2); simpl; auto. rewrite Float32.mul2_add; auto.
+  rewrite Float32.mul_commut; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_cast8signed_correct:
@@ -372,8 +372,8 @@ Lemma make_cast8signed_correct:
   let (op, args) := make_cast8signed r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v.
 Proof.
-  intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. 
-  exists rs#r; split; auto. 
+  intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL.
+  exists rs#r; split; auto.
   assert (V: vmatch bc rs#r (Sgn Ptop 8)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
   inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
@@ -386,8 +386,8 @@ Lemma make_cast16signed_correct:
   let (op, args) := make_cast16signed r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v.
 Proof.
-  intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. 
-  exists rs#r; split; auto. 
+  intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL.
+  exists rs#r; split; auto.
   assert (V: vmatch bc rs#r (Sgn Ptop 16)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
   inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
@@ -413,7 +413,7 @@ Proof.
   InvApproxRegs; SimplVM; inv H0. econstructor; split; eauto. apply Val.add_lessdef; auto.
   InvApproxRegs; SimplVM; inv H0. econstructor; split; eauto. rewrite Val.add_commut. apply Val.add_lessdef; auto.
 (* sub *)
-  InvApproxRegs; SimplVM; inv H0. fold (Val.sub (Vint n1) rs#r2). econstructor; split; eauto. 
+  InvApproxRegs; SimplVM; inv H0. fold (Val.sub (Vint n1) rs#r2). econstructor; split; eauto.
   InvApproxRegs; SimplVM; inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct.
 (* mul *)
   InvApproxRegs; SimplVM; inv H0. fold (Val.mul (Vint n1) rs#r2). rewrite Val.mul_commut. apply make_mulimm_correct; auto.
@@ -464,23 +464,23 @@ Proof.
   intros until res. unfold addr_strength_reduction.
   destruct (addr_strength_reduction_match addr args vl); simpl;
   intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
-- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. 
+- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto.
 - fold (Val.add (Vint n1) rs#r2). rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite Val.add_commut.
   econstructor; split; eauto. apply Val.add_lessdef; auto.
-- rewrite Int.add_zero_l. 
+- rewrite Int.add_zero_l.
   change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)).
   econstructor; split; eauto. apply Val.add_lessdef; auto.
 - fold (Val.add (Vint n1) rs#r2).  rewrite Int.add_zero_l. rewrite Int.add_commut.
   change (Vptr sp (Int.add n2 n1)) with (Val.add (Vptr sp n2) (Vint n1)).
   rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto.
-- econstructor; split; eauto. apply Val.add_lessdef; auto. 
-- rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. apply Val.add_lessdef; auto.
+- rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto.
 - fold (Val.add (Vint n1) rs#r2).
   rewrite Val.add_commut. econstructor; split; eauto.
 - econstructor; split; eauto.
-- rewrite Genv.shift_symbol_address. econstructor; split; eauto. 
-- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. 
-- rewrite Int.add_zero_l.  
+- rewrite Genv.shift_symbol_address. econstructor; split; eauto.
+- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto.
+- rewrite Int.add_zero_l.
   change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)).
   econstructor; split; eauto. apply Val.add_lessdef; auto.
 - exists res; auto.