Updated PR by removing whitespaces. Bug 17450.

1 files changed, 138 insertions, 138 deletions

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 70f9bfc7..07c7008d 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -100,9 +100,9 @@ Lemma numbering_holds_exten:
 Proof.
   intros. destruct H. constructor; intros.
 - auto.
-- apply equation_holds_exten. auto. 
-  eapply wf_equation_incr; eauto with cse. 
-- rewrite AGREE. eauto. eapply Plt_le_trans; eauto. eapply wf_num_reg; eauto. 
+- apply equation_holds_exten. auto.
+  eapply wf_equation_incr; eauto with cse.
+- rewrite AGREE. eauto. eapply Plt_le_trans; eauto. eapply wf_num_reg; eauto.
 Qed.
 
 End EXTEN.
@@ -136,16 +136,16 @@ Proof.
 + constructor; simpl; intros.
 * constructor; simpl; intros.
   apply wf_equation_incr with (num_next n). eauto with cse. xomega.
-  rewrite PTree.gsspec in H0. destruct (peq r0 r). 
+  rewrite PTree.gsspec in H0. destruct (peq r0 r).
   inv H0; xomega.
   apply Plt_trans_succ; eauto with cse.
   rewrite PMap.gsspec in H0. destruct (peq v (num_next n)).
   replace r0 with r by (simpl in H0; intuition). rewrite PTree.gss. subst; auto.
-  exploit wf_num_val; eauto with cse. intro. 
+  exploit wf_num_val; eauto with cse. intro.
   rewrite PTree.gso by congruence. auto.
 * eapply equation_holds_exten; eauto with cse.
 * unfold valu2. rewrite PTree.gsspec in H0. destruct (peq r0 r).
-  inv H0. rewrite peq_true; auto. 
+  inv H0. rewrite peq_true; auto.
   rewrite peq_false. eauto with cse. apply Plt_ne; eauto with cse.
 + unfold valu2. rewrite peq_true; auto.
 + auto.
@@ -169,9 +169,9 @@ Proof.
 - destruct (valnum_reg n a) as [n1 v1] eqn:V1.
   destruct (valnum_regs n1 rl) as [n2 vs] eqn:V2.
   inv H0.
-  exploit valnum_reg_holds; eauto. 
+  exploit valnum_reg_holds; eauto.
   intros (valu2 & A & B & C & D & E).
-  exploit (IHrl valu2); eauto. 
+  exploit (IHrl valu2); eauto.
   intros (valu3 & P & Q & R & S & T).
   exists valu3; splitall.
   + auto.
@@ -187,7 +187,7 @@ Lemma find_valnum_rhs_charact:
 Proof.
   induction eqs; simpl; intros.
 - inv H.
-- destruct a. destruct (strict && eq_rhs rh r) eqn:T. 
+- destruct a. destruct (strict && eq_rhs rh r) eqn:T.
   + InvBooleans. inv H. left; auto.
   + right; eauto.
 Qed.
@@ -198,9 +198,9 @@ Lemma find_valnum_rhs'_charact:
 Proof.
   induction eqs; simpl; intros.
 - inv H.
-- destruct a. destruct (eq_rhs rh r) eqn:T. 
+- destruct a. destruct (eq_rhs rh r) eqn:T.
   + inv H. exists strict; auto.
-  + exploit IHeqs; eauto. intros [s IN]. exists s; auto. 
+  + exploit IHeqs; eauto. intros [s IN]. exists s; auto.
 Qed.
 
 Lemma find_valnum_num_charact:
@@ -208,8 +208,8 @@ Lemma find_valnum_num_charact:
 Proof.
   induction eqs; simpl; intros.
 - inv H.
-- destruct a. destruct (strict && peq v v0) eqn:T. 
-  + InvBooleans. inv H. auto. 
+- destruct a. destruct (strict && peq v v0) eqn:T.
+  + InvBooleans. inv H. auto.
   + eauto.
 Qed.
 
@@ -220,7 +220,7 @@ Lemma reg_valnum_sound:
   rs#r = valu v.
 Proof.
   unfold reg_valnum; intros. destruct (num_val n)#v as [ | r1 rl] eqn:E; inv H.
-  eapply num_holds_reg; eauto. eapply wf_num_val; eauto with cse. 
+  eapply num_holds_reg; eauto. eapply wf_num_val; eauto with cse.
   rewrite E; auto with coqlib.
 Qed.
 
@@ -235,7 +235,7 @@ Proof.
 - inv H0; auto.
 - destruct (reg_valnum n a) as [r1|] eqn:RV1; try discriminate.
   destruct (regs_valnums n vl) as [rl1|] eqn:RVL; inv H0.
-  simpl; f_equal. eapply reg_valnum_sound; eauto. eauto. 
+  simpl; f_equal. eapply reg_valnum_sound; eauto. eauto.
 Qed.
 
 Lemma find_rhs_sound:
@@ -256,10 +256,10 @@ Remark in_remove:
   forall (A: Type) (eq: forall (x y: A), {x=y}+{x<>y}) x y l,
   In y (List.remove eq x l) <-> x <> y /\ In y l.
 Proof.
-  induction l; simpl. 
+  induction l; simpl.
   tauto.
-  destruct (eq x a). 
-  subst a. rewrite IHl. tauto. 
+  destruct (eq x a).
+  subst a. rewrite IHl. tauto.
   simpl. rewrite IHl. intuition congruence.
 Qed.
 
@@ -274,7 +274,7 @@ Proof.
   + subst v. rewrite in_remove in H0. intuition.
   + split; auto. exploit wf_num_val; eauto. congruence.
 - split; auto. exploit wf_num_val; eauto. congruence.
-Qed.  
+Qed.
 
 Lemma update_reg_charact:
   forall n rd vd r v,
@@ -285,7 +285,7 @@ Proof.
   unfold update_reg; intros.
   rewrite PMap.gsspec in H0.
   destruct (peq v vd).
-- subst v. destruct H0. 
+- subst v. destruct H0.
 + subst r. apply PTree.gss.
 + exploit forget_reg_charact; eauto. intros [A B].
   rewrite PTree.gso by auto. eapply wf_num_val; eauto.
@@ -324,7 +324,7 @@ Proof.
     eauto with cse.
   * eapply update_reg_charact; eauto with cse.
 + eauto with cse.
-+ rewrite PTree.gsspec in H5. destruct (peq r rd). 
++ rewrite PTree.gsspec in H5. destruct (peq r rd).
   congruence.
   rewrite H2 by auto. eauto with cse.
 
@@ -334,17 +334,17 @@ Proof.
   { red; intros. unfold valu2. apply peq_false. apply Plt_ne; auto. }
   exists valu2; constructor; simpl; intros.
 + constructor; simpl; intros.
-  * destruct H3. inv H3. simpl; split. xomega. 
-    red; intros. apply Plt_trans_succ; eauto. 
-    apply wf_equation_incr with (num_next n). eauto with cse. xomega. 
+  * destruct H3. inv H3. simpl; split. xomega.
+    red; intros. apply Plt_trans_succ; eauto.
+    apply wf_equation_incr with (num_next n). eauto with cse. xomega.
   * rewrite PTree.gsspec in H3. destruct (peq r rd).
     inv H3. xomega.
     apply Plt_trans_succ; eauto with cse.
   * apply update_reg_charact; eauto with cse.
 + destruct H3. inv H3.
-  constructor. unfold valu2 at 2; rewrite peq_true. 
-  eapply rhs_eval_to_exten; eauto. 
-  eapply equation_holds_exten; eauto with cse. 
+  constructor. unfold valu2 at 2; rewrite peq_true.
+  eapply rhs_eval_to_exten; eauto.
+  eapply equation_holds_exten; eauto with cse.
 + rewrite PTree.gsspec in H3. unfold valu2. destruct (peq r rd).
   inv H3. rewrite peq_true; auto.
   rewrite peq_false. rewrite H2 by auto. eauto with cse.
@@ -363,7 +363,7 @@ Proof.
   exploit is_move_operation_correct; eauto. intros [A B]; subst op args.
   simpl in H0. inv H0.
   destruct (valnum_reg n src) as [n1 vsrc] eqn:VN.
-  exploit valnum_reg_holds; eauto. 
+  exploit valnum_reg_holds; eauto.
   intros (valu2 & A & B & C & D & E).
   exists valu2; constructor; simpl; intros.
 + constructor; simpl; intros; eauto with cse.
@@ -372,15 +372,15 @@ Proof.
     eauto with cse.
   * eapply update_reg_charact; eauto with cse.
 + eauto with cse.
-+ rewrite PTree.gsspec in H0. rewrite Regmap.gsspec. 
++ rewrite PTree.gsspec in H0. rewrite Regmap.gsspec.
   destruct (peq r dst). congruence. eauto with cse.
 
 - (* general case *)
   destruct (valnum_regs n args) as [n1 vl] eqn:VN.
-  exploit valnum_regs_holds; eauto. 
+  exploit valnum_regs_holds; eauto.
   intros (valu2 & A & B & C & D & E).
-  eapply add_rhs_holds; eauto. 
-+ constructor. rewrite Regmap.gss. congruence. 
+  eapply add_rhs_holds; eauto.
++ constructor. rewrite Regmap.gss. congruence.
 + intros. apply Regmap.gso; auto.
 Qed.
 
@@ -393,10 +393,10 @@ Lemma add_load_holds:
 Proof.
   unfold add_load; intros.
   destruct (valnum_regs n args) as [n1 vl] eqn:VN.
-  exploit valnum_regs_holds; eauto. 
+  exploit valnum_regs_holds; eauto.
   intros (valu2 & A & B & C & D & E).
-  eapply add_rhs_holds; eauto. 
-+ econstructor. rewrite <- B; eauto. rewrite Regmap.gss; auto.  
+  eapply add_rhs_holds; eauto.
++ econstructor. rewrite <- B; eauto. rewrite Regmap.gss; auto.
 + intros. apply Regmap.gso; auto.
 Qed.
 
@@ -408,13 +408,13 @@ Proof.
   intros; constructor; simpl; intros.
 - constructor; simpl; intros.
   + eauto with cse.
-  + rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r). 
-    discriminate. 
+  + rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r).
+    discriminate.
     eauto with cse.
-  + exploit forget_reg_charact; eauto with cse. intros [A B]. 
+  + exploit forget_reg_charact; eauto with cse. intros [A B].
     rewrite PTree.gro; eauto with cse.
 - eauto with cse.
-- rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r). 
+- rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r).
   discriminate.
   rewrite Regmap.gso; eauto with cse.
 Qed.
@@ -429,7 +429,7 @@ Qed.
 
 Lemma kill_eqs_charact:
   forall pred l strict r eqs,
-  In (Eq l strict r) (kill_eqs pred eqs) -> 
+  In (Eq l strict r) (kill_eqs pred eqs) ->
   pred r = false /\ In (Eq l strict r) eqs.
 Proof.
   induction eqs; simpl; intros.
@@ -451,7 +451,7 @@ Proof.
   intros; constructor; simpl; intros.
 - constructor; simpl; intros; eauto with cse.
   destruct e. exploit kill_eqs_charact; eauto. intros [A B]. eauto with cse.
-- destruct eq. exploit kill_eqs_charact; eauto. intros [A B]. 
+- destruct eq. exploit kill_eqs_charact; eauto. intros [A B].
   exploit num_holds_eq; eauto. intro EH; inv EH; econstructor; eauto.
 - eauto with cse.
 Qed.
@@ -461,7 +461,7 @@ Lemma kill_all_loads_hold:
   numbering_holds valu ge sp rs m n ->
   numbering_holds valu ge sp rs m' (kill_all_loads n).
 Proof.
-  intros. eapply kill_equations_hold; eauto. 
+  intros. eapply kill_equations_hold; eauto.
   unfold filter_loads; intros. inv H1.
   constructor. rewrite <- H2. apply op_depends_on_memory_correct; auto.
   discriminate.
@@ -486,11 +486,11 @@ Proof.
   econstructor; eauto. rewrite <- H9.
   destruct a; simpl in H1; try discriminate.
   destruct a0; simpl in H9; try discriminate.
-  simpl. 
+  simpl.
   rewrite negb_false_iff in H6. unfold aaddressing in H6.
   eapply Mem.load_store_other. eauto.
-  eapply pdisjoint_sound. eauto. 
-  apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. 
+  eapply pdisjoint_sound. eauto.
+  apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
   apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va.
 Qed.
@@ -516,22 +516,22 @@ Lemma add_store_result_hold:
   approx = VA.State ae am ->
   exists valu2, numbering_holds valu2 ge sp rs m' (add_store_result approx n chunk addr args src).
 Proof.
-  unfold add_store_result; intros. 
-  unfold avalue; rewrite H3. 
+  unfold add_store_result; intros.
+  unfold avalue; rewrite H3.
   destruct (vincl (AE.get src ae) (store_normalized_range chunk)) eqn:INCL.
 - destruct (valnum_reg n src) as [n1 vsrc] eqn:VR1.
   destruct (valnum_regs n1 args) as [n2 vargs] eqn:VR2.
-  exploit valnum_reg_holds; eauto. intros (valu2 & A & B & C & D & E). 
+  exploit valnum_reg_holds; eauto. intros (valu2 & A & B & C & D & E).
   exploit valnum_regs_holds; eauto. intros (valu3 & P & Q & R & S & T).
   exists valu3. constructor; simpl; intros.
 + constructor; simpl; intros; eauto with cse.
-  destruct H4; eauto with cse. subst e. split. 
-  eapply Plt_le_trans; eauto. 
+  destruct H4; eauto with cse. subst e. split.
+  eapply Plt_le_trans; eauto.
   red; simpl; intros. auto.
 + destruct H4; eauto with cse. subst eq. apply eq_holds_lessdef with (Val.load_result chunk rs#src).
   apply load_eval_to with a. rewrite <- Q; auto.
   destruct a; try discriminate. simpl. eapply Mem.load_store_same; eauto.
-  rewrite B. rewrite R by auto. apply store_normalized_range_sound with bc. 
+  rewrite B. rewrite R by auto. apply store_normalized_range_sound with bc.
   rewrite <- B. eapply vmatch_ge. apply vincl_ge; eauto. apply H2.
 + eauto with cse.
 
@@ -557,12 +557,12 @@ Proof.
 - destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate.
   econstructor; eauto. rewrite <- H11.
   destruct a; simpl in H10; try discriminate.
-  simpl. 
+  simpl.
   rewrite negb_false_iff in H8.
   eapply Mem.load_storebytes_other. eauto.
-  rewrite H6. rewrite nat_of_Z_eq by auto. 
-  eapply pdisjoint_sound. eauto. 
-  unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. 
+  rewrite H6. rewrite nat_of_Z_eq by auto.
+  eapply pdisjoint_sound. eauto.
+  unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
   auto.
 Qed.
@@ -576,14 +576,14 @@ Lemma load_memcpy:
   (align_chunk chunk | ofs2 - ofs1) ->
   Mem.load chunk m' b2 (i + (ofs2 - ofs1)) = Some v.
 Proof.
-  intros. 
+  intros.
   generalize (size_chunk_pos chunk); intros SPOS.
   set (n1 := i - ofs1).
   set (n2 := size_chunk chunk).
   set (n3 := sz - (n1 + n2)).
   replace sz with (n1 + (n2 + n3)) in H by (unfold n3, n2, n1; omega).
-  exploit Mem.loadbytes_split; eauto. 
-  unfold n1; omega. 
+  exploit Mem.loadbytes_split; eauto.
+  unfold n1; omega.
   unfold n3, n2, n1; omega.
   intros (bytes1 & bytes23 & LB1 & LB23 & EQ).
   clear H.
@@ -591,7 +591,7 @@ Proof.
   unfold n2; omega.
   unfold n3, n2, n1; omega.
   intros (bytes2 & bytes3 & LB2 & LB3 & EQ').
-  subst bytes23; subst bytes. 
+  subst bytes23; subst bytes.
   exploit Mem.load_loadbytes; eauto. intros (bytes2' & A & B).
   assert (bytes2' = bytes2).
   { replace (ofs1 + n1) with i in LB2 by (unfold n1; omega). unfold n2 in LB2. congruence.  }
@@ -604,17 +604,17 @@ Proof.
   { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n1; omega. }
   assert (L2: Z.of_nat (length bytes2) = n2).
   { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n2; omega. }
-  rewrite L1 in *. rewrite L2 in *. 
+  rewrite L1 in *. rewrite L2 in *.
   assert (LB': Mem.loadbytes m2 b2 (ofs2 + n1) n2 = Some bytes2).
   { rewrite <- L2. eapply Mem.loadbytes_storebytes_same; eauto. }
   assert (LB'': Mem.loadbytes m' b2 (ofs2 + n1) n2 = Some bytes2).
-  { rewrite <- LB'. eapply Mem.loadbytes_storebytes_other; eauto. 
-    unfold n2; omega. 
+  { rewrite <- LB'. eapply Mem.loadbytes_storebytes_other; eauto.
+    unfold n2; omega.
     right; left; omega. }
-  exploit Mem.load_valid_access; eauto. intros [P Q]. 
+  exploit Mem.load_valid_access; eauto. intros [P Q].
   rewrite B. apply Mem.loadbytes_load.
-  replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; omega). 
-  exact LB''. 
+  replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; omega).
+  exact LB''.
   apply Z.divide_add_r; auto.
 Qed.
 
@@ -625,7 +625,7 @@ Lemma shift_memcpy_eq_wf:
   wf_equation next e'.
 Proof with (try discriminate).
   unfold shift_memcpy_eq; intros.
-  destruct e. destruct r... destruct a... 
+  destruct e. destruct r... destruct a...
   destruct (zle src (Int.unsigned i) &&
         zle (Int.unsigned i + size_chunk m) (src + sz) &&
         zeq (delta mod align_chunk m) 0 && zle 0 (Int.unsigned i + delta) &&
@@ -642,7 +642,7 @@ Lemma shift_memcpy_eq_holds:
   equation_holds valu ge (Vptr sp Int.zero) m' e'.
 Proof with (try discriminate).
   intros. set (delta := dst - src) in *. unfold shift_memcpy_eq in H.
-  destruct e as [l strict rhs] eqn:E. 
+  destruct e as [l strict rhs] eqn:E.
   destruct rhs as [op vl | chunk addr vl]...
   destruct addr...
   set (i1 := Int.unsigned i) in *. set (j := i1 + delta) in *.
@@ -656,16 +656,16 @@ Proof with (try discriminate).
     Mem.loadv chunk m (Vptr sp i) = Some v ->
     Mem.loadv chunk m' (Vptr sp (Int.repr j)) = Some v).
   {
-    simpl; intros. rewrite Int.unsigned_repr by omega. 
-    unfold j, delta. eapply load_memcpy; eauto. 
+    simpl; intros. rewrite Int.unsigned_repr by omega.
+    unfold j, delta. eapply load_memcpy; eauto.
     apply Zmod_divide; auto. generalize (align_chunk_pos chunk); omega.
   }
   inv H2.
 + inv H3. destruct vl... simpl in H6. rewrite Int.add_zero_l in H6. inv H6.
-  apply eq_holds_strict. econstructor. simpl. rewrite Int.add_zero_l. eauto. 
+  apply eq_holds_strict. econstructor. simpl. rewrite Int.add_zero_l. eauto.
   apply LD; auto.
 + inv H4. destruct vl... simpl in H7. rewrite Int.add_zero_l in H7. inv H7.
-  apply eq_holds_lessdef with v; auto. 
+  apply eq_holds_lessdef with v; auto.
   econstructor. simpl. rewrite Int.add_zero_l. eauto. apply LD; auto.
 Qed.
 
@@ -677,7 +677,7 @@ Proof.
   induction eqs1; simpl; intros.
 - auto.
 - destruct (shift_memcpy_eq src sz delta a) as [e''|] eqn:SHIFT.
-  + destruct H. subst e''. right; exists a; auto. 
+  + destruct H. subst e''. right; exists a; auto.
     destruct IHeqs1 as [A | [e [A B]]]; auto. right; exists e; auto.
   + destruct IHeqs1 as [A | [e [A B]]]; auto. right; exists e; auto.
 Qed.
@@ -695,7 +695,7 @@ Lemma add_memcpy_holds:
   numbering_holds valu ge (Vptr sp Int.zero) rs m' (add_memcpy n1 n2 asrc adst sz).
 Proof.
   intros. unfold add_memcpy.
-  destruct asrc; auto; destruct adst; auto. 
+  destruct asrc; auto; destruct adst; auto.
   assert (A: forall b o i, pmatch bc b o (Stk i) -> b = sp /\ i = o).
   {
     intros. inv H7. split; auto. eapply bc_stack; eauto.
@@ -703,11 +703,11 @@ Proof.
   apply A in H3; destruct H3. subst bsrc ofs.
   apply A in H4; destruct H4. subst bdst ofs0.
   constructor; simpl; intros; eauto with cse.
-- constructor; simpl; eauto with cse. 
+- constructor; simpl; eauto with cse.
   intros. exploit add_memcpy_eqs_charact; eauto. intros [X | (e0 & X & Y)].
   eauto with cse.
-  apply wf_equation_incr with (num_next n1); auto. 
-  eapply shift_memcpy_eq_wf; eauto with cse. 
+  apply wf_equation_incr with (num_next n1); auto.
+  eapply shift_memcpy_eq_wf; eauto with cse.
 - exploit add_memcpy_eqs_charact; eauto. intros [X | (e0 & X & Y)].
   eauto with cse.
   eapply shift_memcpy_eq_holds; eauto with cse.
@@ -747,7 +747,7 @@ Proof.
   assert (sem op1 (map valu args1) = Some res).
     rewrite <- H0. eapply f_sound; eauto.
     simpl; intros.
-    exploit num_holds_eq; eauto. 
+    exploit num_holds_eq; eauto.
     eapply find_valnum_num_charact; eauto with cse.
     intros EH; inv EH; auto.
   destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ] eqn:?.
@@ -765,7 +765,7 @@ Lemma reduce_sound:
   sem op rs##rl = Some res ->
   sem op' rs##rl' = Some res.
 Proof.
-  unfold reduce; intros. 
+  unfold reduce; intros.
   destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ] eqn:?; inv H.
   eapply reduce_rec_sound; eauto. congruence.
   auto.
@@ -775,8 +775,8 @@ End REDUCE.
 
 (** The numberings associated to each instruction by the static analysis
   are inductively satisfiable, in the following sense: the numbering
-  at the function entry point is satisfiable, and for any RTL execution 
-  from [pc] to [pc'], satisfiability at [pc] implies 
+  at the function entry point is satisfiable, and for any RTL execution
+  from [pc] to [pc'], satisfiability at [pc] implies
   satisfiability at [pc']. *)
 
 Theorem analysis_correct_1:
@@ -797,7 +797,7 @@ Theorem analysis_correct_entry:
   analyze f vapprox = Some approx ->
   exists valu, numbering_holds valu ge sp rs m approx!!(f.(fn_entrypoint)).
 Proof.
-  intros. 
+  intros.
   replace (approx!!(f.(fn_entrypoint))) with Solver.L.top.
   exists (fun v => Vundef). apply empty_numbering_holds.
   symmetry. eapply Solver.fixpoint_entry; eauto.
@@ -843,7 +843,7 @@ Lemma sig_preserved:
 Proof.
   unfold transf_fundef; intros. destruct f; monadInv H; auto.
   unfold transf_function in EQ.
-  destruct (analyze f (vanalyze rm f)); try discriminate. inv EQ; auto. 
+  destruct (analyze f (vanalyze rm f)); try discriminate. inv EQ; auto.
 Qed.
 
 Definition transf_function' (f: function) (approxs: PMap.t numbering) : function :=
@@ -868,7 +868,7 @@ Lemma set_reg_lessdef:
   forall r v1 v2 rs1 rs2,
   Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> regs_lessdef (rs1#r <- v1) (rs2#r <- v2).
 Proof.
-  intros; red; intros. repeat rewrite Regmap.gsspec. 
+  intros; red; intros. repeat rewrite Regmap.gsspec.
   destruct (peq r0 r); auto.
 Qed.
 
@@ -958,7 +958,7 @@ Ltac TransfInstr :=
   | H1: (PTree.get ?pc ?c = Some ?instr), f: function, approx: PMap.t numbering |- _ =>
       cut ((transf_function' f approx).(fn_code)!pc = Some(transf_instr approx!!pc instr));
       [ simpl transf_instr
-      | unfold transf_function', transf_code; simpl; rewrite PTree.gmap; 
+      | unfold transf_function', transf_code; simpl; rewrite PTree.gmap;
         unfold option_map; rewrite H1; reflexivity ]
   end.
 
@@ -975,8 +975,8 @@ Proof.
   (* Inop *)
 - econstructor; split.
   eapply exec_Inop; eauto.
-  econstructor; eauto. 
-  eapply analysis_correct_1; eauto. simpl; auto. 
+  econstructor; eauto.
+  eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H; auto.
 
   (* Iop *)
@@ -987,9 +987,9 @@ Proof.
   econstructor; split.
   eapply exec_Iop with (v := v'); eauto.
   rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
-  econstructor; eauto. 
+  econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H. 
+  unfold transfer; rewrite H.
   destruct SAT as [valu NH]. eapply add_op_holds; eauto.
   apply set_reg_lessdef; auto.
 + (* possibly optimized *)
@@ -998,31 +998,31 @@ Proof.
   exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
   destruct (find_rhs n1 (Op op vl)) as [r|] eqn:?.
 * (* replaced by move *)
-  exploit find_rhs_sound; eauto. intros (v' & EV & LD). 
+  exploit find_rhs_sound; eauto. intros (v' & EV & LD).
   assert (v' = v) by (inv EV; congruence). subst v'.
   econstructor; split.
   eapply exec_Iop; eauto. simpl; eauto.
-  econstructor; eauto. 
+  econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H. 
-  eapply add_op_holds; eauto. 
+  unfold transfer; rewrite H.
+  eapply add_op_holds; eauto.
   apply set_reg_lessdef; auto.
   eapply Val.lessdef_trans; eauto.
 * (* possibly simplified *)
   destruct (reduce operation combine_op n1 op args vl) as [op' args'] eqn:?.
   assert (RES: eval_operation ge sp op' rs##args' m = Some v).
-    eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto. 
+    eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto.
     intros; eapply combine_op_sound; eauto.
   exploit eval_operation_lessdef. eapply regs_lessdef_regs; eauto. eauto. eauto.
   intros [v' [A B]].
   econstructor; split.
-  eapply exec_Iop with (v := v'); eauto.   
+  eapply exec_Iop with (v := v'); eauto.
   rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
   econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H. 
-  eapply add_op_holds; eauto. 
-  apply set_reg_lessdef; auto. 
+  unfold transfer; rewrite H.
+  eapply add_op_holds; eauto.
+  apply set_reg_lessdef; auto.
 
 - (* Iload *)
   destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
@@ -1030,31 +1030,31 @@ Proof.
   exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
   destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?.
 + (* replaced by move *)
-  exploit find_rhs_sound; eauto. intros (v' & EV & LD). 
+  exploit find_rhs_sound; eauto. intros (v' & EV & LD).
   assert (v' = v) by (inv EV; congruence). subst v'.
   econstructor; split.
   eapply exec_Iop; eauto. simpl; eauto.
-  econstructor; eauto. 
+  econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H. 
-  eapply add_load_holds; eauto. 
+  unfold transfer; rewrite H.
+  eapply add_load_holds; eauto.
   apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
 + (* load is preserved, but addressing is possibly simplified *)
   destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?.
   assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
-  { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. 
+  { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto.
     intros; eapply combine_addr_sound; eauto. }
   exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR.
   intros [a' [A B]].
   assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a').
   { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. }
-  exploit Mem.loadv_extends; eauto. 
+  exploit Mem.loadv_extends; eauto.
   intros [v' [X Y]].
   econstructor; split.
   eapply exec_Iload; eauto.
   econstructor; eauto.
-  eapply analysis_correct_1; eauto. simpl; auto. 
-  unfold transfer; rewrite H. 
+  eapply analysis_correct_1; eauto. simpl; auto.
+  unfold transfer; rewrite H.
   eapply add_load_holds; eauto.
   apply set_reg_lessdef; auto.
 
@@ -1064,7 +1064,7 @@ Proof.
   exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
   destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?.
   assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
-  { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. 
+  { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto.
     intros; eapply combine_addr_sound; eauto. }
   exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR.
   intros [a' [A B]].
@@ -1074,35 +1074,35 @@ Proof.
   econstructor; split.
   eapply exec_Istore; eauto.
   econstructor; eauto.
-  eapply analysis_correct_1; eauto. simpl; auto. 
+  eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H.
   inv SOUND.
-  eapply add_store_result_hold; eauto. 
+  eapply add_store_result_hold; eauto.
   eapply kill_loads_after_store_holds; eauto.
 
 - (* Icall *)
-  exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. 
+  exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']].
   econstructor; split.
   eapply exec_Icall; eauto.
   apply sig_preserved; auto.
-  econstructor; eauto. 
-  econstructor; eauto. 
-  intros. eapply analysis_correct_1; eauto. simpl; auto. 
-  unfold transfer; rewrite H. 
+  econstructor; eauto.
+  econstructor; eauto.
+  intros. eapply analysis_correct_1; eauto. simpl; auto.
+  unfold transfer; rewrite H.
   exists (fun _ => Vundef); apply empty_numbering_holds.
   apply regs_lessdef_regs; auto.
 
 - (* Itailcall *)
-  exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. 
+  exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']].
   exploit Mem.free_parallel_extends; eauto. intros [m'' [A B]].
   econstructor; split.
   eapply exec_Itailcall; eauto.
   apply sig_preserved; auto.
-  econstructor; eauto. 
+  econstructor; eauto.
   apply regs_lessdef_regs; auto.
 
 - (* Ibuiltin *)
-  exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. 
+  exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto.
   intros (vargs' & A & B).
   exploit external_call_mem_extends; eauto.
   intros (v' & m1' & P & Q & R & S).
@@ -1124,7 +1124,7 @@ Proof.
   { exists valu. apply set_res_unknown_holds. eapply kill_all_loads_hold; eauto. }
   destruct ef.
   + apply CASE1.
-  + apply CASE3. 
+  + apply CASE3.
   + apply CASE2; inv H1; auto.
   + apply CASE3.
   + apply CASE1.
@@ -1133,15 +1133,15 @@ Proof.
     simpl in H1. inv H1.
     exists valu.
     apply set_res_unknown_holds.
-    inv SOUND. unfold vanalyze, rm; rewrite AN. 
+    inv SOUND. unfold vanalyze, rm; rewrite AN.
     assert (pmatch bc bsrc osrc (aaddr_arg (VA.State ae am) a0))
-    by (eapply aaddr_arg_sound_1; eauto). 
+    by (eapply aaddr_arg_sound_1; eauto).
     assert (pmatch bc bdst odst (aaddr_arg (VA.State ae am) a1))
-    by (eapply aaddr_arg_sound_1; eauto). 
-    eapply add_memcpy_holds; eauto. 
-    eapply kill_loads_after_storebytes_holds; eauto. 
-    eapply Mem.loadbytes_length; eauto. 
-    simpl. apply Ple_refl. 
+    by (eapply aaddr_arg_sound_1; eauto).
+    eapply add_memcpy_holds; eauto.
+    eapply kill_loads_after_storebytes_holds; eauto.
+    eapply Mem.loadbytes_length; eauto.
+    simpl. apply Ple_refl.
   + apply CASE2; inv H1; auto.
   + apply CASE2; inv H1; auto.
   + apply CASE1.
@@ -1154,10 +1154,10 @@ Proof.
   exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
   destruct (reduce condition combine_cond n1 cond args vl) as [cond' args'] eqn:?.
   assert (RES: eval_condition cond' rs##args' m = Some b).
-  { eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto. 
+  { eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto.
     intros; eapply combine_cond_sound; eauto. }
   econstructor; split.
-  eapply exec_Icond; eauto. 
+  eapply exec_Icond; eauto.
   eapply eval_condition_lessdef; eauto. apply regs_lessdef_regs; auto.
   econstructor; eauto.
   destruct b; eapply analysis_correct_1; eauto; simpl; auto;
@@ -1166,7 +1166,7 @@ Proof.
 - (* Ijumptable *)
   generalize (RLD arg); rewrite H0; intro LD; inv LD.
   econstructor; split.
-  eapply exec_Ijumptable; eauto. 
+  eapply exec_Ijumptable; eauto.
   econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl. eapply list_nth_z_in; eauto.
   unfold transfer; rewrite H; auto.
@@ -1176,21 +1176,21 @@ Proof.
   econstructor; split.
   eapply exec_Ireturn; eauto.
   econstructor; eauto.
-  destruct or; simpl; auto. 
+  destruct or; simpl; auto.
 
 - (* internal function *)
-  monadInv H6. unfold transf_function in EQ. 
-  destruct (analyze f (vanalyze rm f)) as [approx|] eqn:?; inv EQ. 
-  exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. 
+  monadInv H6. unfold transf_function in EQ.
+  destruct (analyze f (vanalyze rm f)) as [approx|] eqn:?; inv EQ.
+  exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
   intros (m'' & A & B).
   econstructor; split.
-  eapply exec_function_internal; simpl; eauto. 
+  eapply exec_function_internal; simpl; eauto.
   simpl. econstructor; eauto.
   eapply analysis_correct_entry; eauto.
   apply init_regs_lessdef; auto.
 
 - (* external function *)
-  monadInv H6. 
+  monadInv H6.
   exploit external_call_mem_extends; eauto.
   intros (v' & m1' & P & Q & R & S).
   econstructor; split.
@@ -1211,7 +1211,7 @@ Lemma transf_initial_states:
   forall st1, initial_state prog st1 ->
   exists st2, initial_state tprog st2 /\ match_states st1 st2.
 Proof.
-  intros. inversion H. 
+  intros. inversion H.
   exploit funct_ptr_translated; eauto. intros [tf [A B]].
   exists (Callstate nil tf nil m0); split.
   econstructor; eauto.
@@ -1224,10 +1224,10 @@ Proof.
 Qed.
 
 Lemma transf_final_states:
-  forall st1 st2 r, 
+  forall st1 st2 r,
   match_states st1 st2 -> final_state st1 r -> final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H5. inv H3. constructor. 
+  intros. inv H0. inv H. inv H5. inv H3. constructor.
 Qed.
 
 Theorem transf_program_correct:
@@ -1236,10 +1236,10 @@ Proof.
   eapply forward_simulation_step with
     (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2).
 - eexact public_preserved.
-- intros. exploit transf_initial_states; eauto. intros [s2 [A B]]. 
+- intros. exploit transf_initial_states; eauto. intros [s2 [A B]].
   exists s2. split. auto. split. apply sound_initial; auto. auto.
 - intros. destruct H. eapply transf_final_states; eauto.
-- intros. destruct H0. exploit transf_step_correct; eauto. 
+- intros. destruct H0. exploit transf_step_correct; eauto.
   intros [s2' [A B]]. exists s2'; split. auto. split. eapply sound_step; eauto. auto.
 Qed.