Updated PR by removing whitespaces. Bug 17450.

1 files changed, 314 insertions, 314 deletions

diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 22121075..979f8c0e 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -231,7 +231,7 @@ Definition definitive_initializer (init: list init_data) : bool :=
 
 Definition alloc_global (rm: romem) (idg: ident * globdef fundef unit): romem :=
   match idg with
-  | (id, Gfun f) => 
+  | (id, Gfun f) =>
       PTree.remove id rm
   | (id, Gvar v) =>
       if v.(gvar_readonly) && negb v.(gvar_volatile) && definitive_initializer v.(gvar_init)
@@ -255,26 +255,26 @@ Lemma analyze_entrypoint:
   /\ ematch bc (init_regs vl (fn_params f)) ae
   /\ mmatch bc m am.
 Proof.
-  intros. 
-  unfold analyze. 
+  intros.
+  unfold analyze.
   set (lu := Liveness.last_uses f).
   set (entry := VA.State (einit_regs f.(fn_params)) mfunction_entry).
   destruct (DS.fixpoint (fn_code f) successors_instr (transfer' f lu rm)
                         (fn_entrypoint f) entry) as [res|] eqn:FIX.
 - assert (A: VA.ge res!!(fn_entrypoint f) entry) by (eapply DS.fixpoint_entry; eauto).
   destruct (res!!(fn_entrypoint f)) as [ | ae am ]; simpl in A. contradiction.
-  destruct A as [A1 A2]. 
-  exists ae, am. 
-  split. auto. 
-  split. eapply ematch_ge; eauto. apply ematch_init; auto. 
+  destruct A as [A1 A2].
+  exists ae, am.
+  split. auto.
+  split. eapply ematch_ge; eauto. apply ematch_init; auto.
   auto.
 - exists AE.top, mtop.
-  split. apply PMap.gi. 
-  split. apply ematch_ge with (einit_regs (fn_params f)). 
-  apply ematch_init; auto. apply AE.ge_top. 
-  eapply mmatch_top'; eauto. 
+  split. apply PMap.gi.
+  split. apply ematch_ge with (einit_regs (fn_params f)).
+  apply ematch_init; auto. apply AE.ge_top.
+  eapply mmatch_top'; eauto.
 Qed.
-  
+
 Lemma analyze_successor:
   forall f n ae am instr s rm ae' am',
   (analyze rm f)!!n = VA.State ae am ->
@@ -291,9 +291,9 @@ Proof.
 - assert (A: VA.ge res!!s (transfer' f lu rm n res#n)).
   { eapply DS.fixpoint_solution; eauto with coqlib.
     intros. unfold transfer'. simpl. auto. }
-  rewrite H in A. unfold transfer' in A. rewrite H2 in A. rewrite H2.  
+  rewrite H in A. unfold transfer' in A. rewrite H2 in A. rewrite H2.
   destruct lu!n.
-  eapply VA.ge_trans. eauto. split; auto. apply eforget_ge. 
+  eapply VA.ge_trans. eauto. split; auto. apply eforget_ge.
   auto.
 - rewrite H2. rewrite PMap.gi. split; intros. apply AE.ge_top. eapply mmatch_top'; eauto.
 Qed.
@@ -311,11 +311,11 @@ Lemma analyze_succ:
   /\ ematch bc e ae''
   /\ mmatch bc m am''.
 Proof.
-  intros. exploit analyze_successor; eauto. rewrite H2. 
+  intros. exploit analyze_successor; eauto. rewrite H2.
   destruct (analyze rm f)#s as [ | ae'' am'']; simpl; try tauto. intros [A B].
   exists ae'', am''.
-  split. auto. 
-  split. eapply ematch_ge; eauto. eauto. 
+  split. auto.
+  split. eapply ematch_ge; eauto. eauto.
 Qed.
 
 (** ** Analysis of registers and builtin arguments *)
@@ -323,7 +323,7 @@ Qed.
 Lemma areg_sound:
   forall bc e ae r, ematch bc e ae -> vmatch bc (e#r) (areg ae r).
 Proof.
-  intros. apply H. 
+  intros. apply H.
 Qed.
 
 Lemma aregs_sound:
@@ -347,8 +347,8 @@ Lemma abuiltin_arg_sound:
 Proof.
   intros until am; intros EM RM MM GM SP.
   induction 1; simpl; eauto with va.
-- eapply loadv_sound; eauto. simpl. rewrite Int.add_zero_l. auto with va. 
-- simpl. rewrite Int.add_zero_l. auto with va. 
+- eapply loadv_sound; eauto. simpl. rewrite Int.add_zero_l. auto with va.
+- simpl. rewrite Int.add_zero_l. auto with va.
 - eapply loadv_sound; eauto. apply symbol_address_sound; auto.
 - apply symbol_address_sound; auto.
 Qed.
@@ -367,7 +367,7 @@ Proof.
   intros until am; intros EM RM MM GM SP.
   induction 1; simpl.
 - constructor.
-- constructor; auto. eapply abuiltin_arg_sound; eauto. 
+- constructor; auto. eapply abuiltin_arg_sound; eauto.
 Qed.
 
 Lemma set_builtin_res_sound:
@@ -376,7 +376,7 @@ Lemma set_builtin_res_sound:
   vmatch bc v av ->
   ematch bc (regmap_setres res v rs) (set_builtin_res res av ae).
 Proof.
-  intros. destruct res; simpl; auto. apply ematch_update; auto. 
+  intros. destruct res; simpl; auto. apply ematch_update; auto.
 Qed.
 
 (** ** Constructing block classifications *)
@@ -396,24 +396,24 @@ Qed.
 
 Lemma vmatch_no_stack: forall v x, vmatch bc v x -> vmatch bc v (Ifptr Nonstack).
 Proof.
-  induction 1; constructor; auto; eapply pmatch_no_stack; eauto. 
+  induction 1; constructor; auto; eapply pmatch_no_stack; eauto.
 Qed.
 
 Lemma smatch_no_stack: forall m b p, smatch bc m b p -> smatch bc m b Nonstack.
 Proof.
-  intros. destruct H as [A B]. split; intros. 
-  eapply vmatch_no_stack; eauto. 
-  eapply pmatch_no_stack; eauto. 
+  intros. destruct H as [A B]. split; intros.
+  eapply vmatch_no_stack; eauto.
+  eapply pmatch_no_stack; eauto.
 Qed.
 
 Lemma mmatch_no_stack: forall m am astk,
   mmatch bc m am -> mmatch bc m {| am_stack := astk; am_glob := PTree.empty _; am_nonstack := Nonstack; am_top := Nonstack |}.
 Proof.
   intros. destruct H. constructor; simpl; intros.
-- elim (NOSTACK b); auto. 
+- elim (NOSTACK b); auto.
 - rewrite PTree.gempty in H0; discriminate.
-- eapply smatch_no_stack; eauto. 
-- eapply smatch_no_stack; eauto. 
+- eapply smatch_no_stack; eauto.
+- eapply smatch_no_stack; eauto.
 - auto.
 Qed.
 
@@ -439,8 +439,8 @@ Theorem allocate_stack:
   /\ (forall b, Plt b sp -> bc' b = bc b)
   /\ (forall v x, vmatch bc v x -> vmatch bc' v (Ifptr Nonstack)).
 Proof.
-  intros until am; intros ALLOC GENV RO MM NOSTACK. 
-  exploit Mem.nextblock_alloc; eauto. intros NB. 
+  intros until am; intros ALLOC GENV RO MM NOSTACK.
+  exploit Mem.nextblock_alloc; eauto. intros NB.
   exploit Mem.alloc_result; eauto. intros SP.
   assert (SPINVALID: bc sp = BCinvalid).
   { rewrite SP. eapply bc_below_invalid. apply Plt_strict. eapply mmatch_below; eauto. }
@@ -450,13 +450,13 @@ Proof.
   {
     assert (forall b, f b = BCstack -> b = sp).
     { unfold f; intros. destruct (eq_block b sp); auto. eelim NOSTACK; eauto. }
-    intros. transitivity sp; auto. symmetry; auto. 
+    intros. transitivity sp; auto. symmetry; auto.
   }
   assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2).
   {
     assert (forall b id, f b = BCglob id -> bc b = BCglob id).
     { unfold f; intros. destruct (eq_block b sp). congruence. auto. }
-    intros. eapply (bc_glob bc); eauto. 
+    intros. eapply (bc_glob bc); eauto.
   }
   set (bc' := BC f F_stack F_glob). unfold f in bc'.
   assert (BC'EQ: forall b, bc b <> BCinvalid -> bc' b = bc b).
@@ -466,15 +466,15 @@ Proof.
 (* Part 2: invariance properties *)
   assert (SM: forall b p, bc b <> BCinvalid -> smatch bc m b p -> smatch bc' m' b Nonstack).
   {
-    intros. 
+    intros.
     apply smatch_incr with bc; auto.
-    apply smatch_inv with m. 
+    apply smatch_inv with m.
     apply smatch_no_stack with p; auto.
-    intros. eapply Mem.loadbytes_alloc_unchanged; eauto. eapply mmatch_below; eauto. 
+    intros. eapply Mem.loadbytes_alloc_unchanged; eauto. eapply mmatch_below; eauto.
   }
   assert (SMSTACK: smatch bc' m' sp Pbot).
   {
-    split; intros. 
+    split; intros.
     exploit Mem.load_alloc_same; eauto. intros EQ. subst v. constructor.
     exploit Mem.loadbytes_alloc_same; eauto with coqlib. congruence.
   }
@@ -483,15 +483,15 @@ Proof.
 - (* incr *)
   assumption.
 - (* sp is BCstack *)
-  simpl; apply dec_eq_true. 
+  simpl; apply dec_eq_true.
 - (* genv match *)
   eapply genv_match_exten; eauto.
   simpl; intros. destruct (eq_block b sp); intuition congruence.
-  simpl; intros. destruct (eq_block b sp); congruence. 
+  simpl; intros. destruct (eq_block b sp); congruence.
 - (* romatch *)
-  apply romatch_exten with bc. 
-  eapply romatch_alloc; eauto. eapply mmatch_below; eauto. 
-  simpl; intros. destruct (eq_block b sp); intuition. 
+  apply romatch_exten with bc.
+  eapply romatch_alloc; eauto. eapply mmatch_below; eauto.
+  simpl; intros. destruct (eq_block b sp); intuition.
 - (* mmatch *)
   constructor; simpl; intros.
   + (* stack *)
@@ -504,16 +504,16 @@ Proof.
     destruct (eq_block b sp). congruence. eapply SM; auto. eapply mmatch_nonstack; eauto.
   + (* top *)
     destruct (eq_block b sp).
-    subst b. apply smatch_ge with Pbot. apply SMSTACK. constructor.  
+    subst b. apply smatch_ge with Pbot. apply SMSTACK. constructor.
     eapply SM; auto. eapply mmatch_top; eauto.
   + (* below *)
-    red; simpl; intros. rewrite NB. destruct (eq_block b sp). 
-    subst b; rewrite SP; xomega. 
-    exploit mmatch_below; eauto. xomega. 
+    red; simpl; intros. rewrite NB. destruct (eq_block b sp).
+    subst b; rewrite SP; xomega.
+    exploit mmatch_below; eauto. xomega.
 - (* unchanged *)
   simpl; intros. apply dec_eq_false. apply Plt_ne. auto.
 - (* values *)
-  intros. apply vmatch_incr with bc; auto. eapply vmatch_no_stack; eauto. 
+  intros. apply vmatch_incr with bc; auto. eapply vmatch_no_stack; eauto.
 Qed.
 
 (** Construction 2: turn the stack into an "other" block, at public calls or function returns *)
@@ -540,15 +540,15 @@ Proof.
   {
     unfold f; intros.
     destruct (eq_block b1 sp); try discriminate.
-    destruct (eq_block b2 sp); try discriminate. 
-    eapply bc_stack; eauto. 
+    destruct (eq_block b2 sp); try discriminate.
+    eapply bc_stack; eauto.
   }
   assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2).
   {
     unfold f; intros.
     destruct (eq_block b1 sp); try discriminate.
-    destruct (eq_block b2 sp); try discriminate. 
-    eapply bc_glob; eauto. 
+    destruct (eq_block b2 sp); try discriminate.
+    eapply bc_glob; eauto.
   }
   set (bc' := BC f F_stack F_glob). unfold f in bc'.
 
@@ -556,7 +556,7 @@ Proof.
   assert (PM: forall b ofs p, pmatch bc b ofs p -> pmatch bc' b ofs Ptop).
   {
     intros. assert (pmatch bc b ofs Ptop) by (eapply pmatch_top'; eauto).
-    inv H0. constructor; simpl. destruct (eq_block b sp); congruence. 
+    inv H0. constructor; simpl. destruct (eq_block b sp); congruence.
   }
   assert (VM: forall v x, vmatch bc v x -> vmatch bc' v Vtop).
   {
@@ -571,32 +571,32 @@ Proof.
 (* Conclusions *)
   exists bc'; splitall.
 - (* nostack *)
-  red; simpl; intros. destruct (eq_block b sp). congruence. 
-  red; intros. elim n. eapply bc_stack; eauto. 
+  red; simpl; intros. destruct (eq_block b sp). congruence.
+  red; intros. elim n. eapply bc_stack; eauto.
 - (* bc' sp is BCother *)
-  simpl; apply dec_eq_true. 
+  simpl; apply dec_eq_true.
 - (* other blocks *)
-  intros; simpl; apply dec_eq_false; auto. 
+  intros; simpl; apply dec_eq_false; auto.
 - (* values *)
   auto.
 - (* genv *)
-  apply genv_match_exten with bc; auto. 
+  apply genv_match_exten with bc; auto.
   simpl; intros. destruct (eq_block b sp); intuition congruence.
   simpl; intros. destruct (eq_block b sp); auto.
 - (* romatch *)
-  apply romatch_exten with bc; auto. 
-  simpl; intros. destruct (eq_block b sp); intuition. 
+  apply romatch_exten with bc; auto.
+  simpl; intros. destruct (eq_block b sp); intuition.
 - (* mmatch top *)
-  constructor; simpl; intros. 
+  constructor; simpl; intros.
   + destruct (eq_block b sp). congruence. elim n. eapply bc_stack; eauto.
   + rewrite PTree.gempty in H0; discriminate.
   + destruct (eq_block b sp).
     subst b. eapply SM. eapply mmatch_stack; eauto.
-    eapply SM. eapply mmatch_nonstack; eauto. 
+    eapply SM. eapply mmatch_nonstack; eauto.
   + destruct (eq_block b sp).
     subst b. eapply SM. eapply mmatch_stack; eauto.
     eapply SM. eapply mmatch_top; eauto.
-  + red; simpl; intros. destruct (eq_block b sp). 
+  + red; simpl; intros. destruct (eq_block b sp).
     subst b. eapply mmatch_below; eauto. congruence.
     eapply mmatch_below; eauto.
 Qed.
@@ -626,15 +626,15 @@ Proof.
   {
     unfold f; intros.
     destruct (eq_block b1 sp); try discriminate.
-    destruct (eq_block b2 sp); try discriminate. 
-    eapply bc_stack; eauto. 
+    destruct (eq_block b2 sp); try discriminate.
+    eapply bc_stack; eauto.
   }
   assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2).
   {
     unfold f; intros.
     destruct (eq_block b1 sp); try discriminate.
-    destruct (eq_block b2 sp); try discriminate. 
-    eapply bc_glob; eauto. 
+    destruct (eq_block b2 sp); try discriminate.
+    eapply bc_glob; eauto.
   }
   set (bc' := BC f F_stack F_glob). unfold f in bc'.
 
@@ -642,11 +642,11 @@ Proof.
   assert (PM: forall b ofs p, pge Nonstack p -> pmatch bc b ofs p -> pmatch bc' b ofs Ptop).
   {
     intros. assert (pmatch bc b ofs Nonstack) by (eapply pmatch_ge; eauto).
-    inv H1. constructor; simpl; destruct (eq_block b sp); congruence. 
+    inv H1. constructor; simpl; destruct (eq_block b sp); congruence.
   }
   assert (VM: forall v x, vge (Ifptr Nonstack) x -> vmatch bc v x -> vmatch bc' v Vtop).
   {
-    intros. apply vmatch_ifptr; intros. subst v. 
+    intros. apply vmatch_ifptr; intros. subst v.
     inv H0; inv H; eapply PM; eauto.
   }
   assert (SM: forall b p, pge Nonstack p -> smatch bc m b p -> smatch bc' m b Ptop).
@@ -658,31 +658,31 @@ Proof.
 (* Conclusions *)
   exists bc'; splitall.
 - (* nostack *)
-  red; simpl; intros. destruct (eq_block b sp). congruence. 
-  red; intros. elim n. eapply bc_stack; eauto. 
+  red; simpl; intros. destruct (eq_block b sp). congruence.
+  red; intros. elim n. eapply bc_stack; eauto.
 - (* bc' sp is BCinvalid *)
-  simpl; apply dec_eq_true. 
+  simpl; apply dec_eq_true.
 - (* other blocks *)
-  intros; simpl; apply dec_eq_false; auto. 
+  intros; simpl; apply dec_eq_false; auto.
 - (* values *)
   auto.
 - (* genv *)
-  apply genv_match_exten with bc; auto. 
+  apply genv_match_exten with bc; auto.
   simpl; intros. destruct (eq_block b sp); intuition congruence.
   simpl; intros. destruct (eq_block b sp); congruence.
 - (* romatch *)
-  apply romatch_exten with bc; auto. 
-  simpl; intros. destruct (eq_block b sp); intuition. 
+  apply romatch_exten with bc; auto.
+  simpl; intros. destruct (eq_block b sp); intuition.
 - (* mmatch top *)
-  constructor; simpl; intros. 
+  constructor; simpl; intros.
   + destruct (eq_block b sp). congruence. elim n. eapply bc_stack; eauto.
   + rewrite PTree.gempty in H0; discriminate.
   + destruct (eq_block b sp). congruence.
-    eapply SM. eauto. eapply mmatch_nonstack; eauto. 
+    eapply SM. eauto. eapply mmatch_nonstack; eauto.
   + destruct (eq_block b sp). congruence.
-    eapply SM. eauto. eapply mmatch_nonstack; eauto. 
-    red; intros; elim n. eapply bc_stack; eauto. 
-  + red; simpl; intros. destruct (eq_block b sp). congruence. 
+    eapply SM. eauto. eapply mmatch_nonstack; eauto.
+    red; intros; elim n. eapply bc_stack; eauto.
+  + red; simpl; intros. destruct (eq_block b sp). congruence.
     eapply mmatch_below; eauto.
 Qed.
 
@@ -718,29 +718,29 @@ Proof.
   {
     assert (forall b, f b = BCstack -> b = sp).
     { unfold f; intros. destruct (eq_block b sp); auto. eelim NOSTACK; eauto. }
-    intros. transitivity sp; auto. symmetry; auto. 
+    intros. transitivity sp; auto. symmetry; auto.
   }
   assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2).
   {
     assert (forall b id, f b = BCglob id -> callee b = BCglob id).
     { unfold f; intros. destruct (eq_block b sp). congruence. auto. }
-    intros. eapply (bc_glob callee); eauto. 
+    intros. eapply (bc_glob callee); eauto.
   }
   set (bc := BC f F_stack F_glob). unfold f in bc.
   assert (INCR: bc_incr caller bc).
   {
-    red; simpl; intros. destruct (eq_block b sp). congruence. 
-    symmetry; apply SAME; auto. 
+    red; simpl; intros. destruct (eq_block b sp). congruence.
+    symmetry; apply SAME; auto.
   }
 (* Invariance properties *)
-  assert (PM: forall b ofs p, pmatch callee b ofs p -> pmatch bc b ofs Ptop).  
+  assert (PM: forall b ofs p, pmatch callee b ofs p -> pmatch bc b ofs Ptop).
   {
     intros. assert (pmatch callee b ofs Ptop) by (eapply pmatch_top'; eauto).
     inv H0. constructor; simpl. destruct (eq_block b sp); congruence.
   }
   assert (VM: forall v x, vmatch callee v x -> vmatch bc v Vtop).
   {
-    intros. assert (vmatch callee v0 Vtop) by (eapply vmatch_top; eauto). 
+    intros. assert (vmatch callee v0 Vtop) by (eapply vmatch_top; eauto).
     inv H0; constructor; eauto.
   }
   assert (SM: forall b p, smatch callee m b p -> smatch bc m b Ptop).
@@ -752,38 +752,38 @@ Proof.
 - (* result value *)
   eapply VM; eauto.
 - (* environment *)
-  eapply ematch_incr; eauto. 
+  eapply ematch_incr; eauto.
 - (* romem *)
   apply romatch_exten with callee; auto.
-  intros; simpl. destruct (eq_block b sp); intuition. 
+  intros; simpl. destruct (eq_block b sp); intuition.
 - (* mmatch *)
   constructor; simpl; intros.
   + (* stack *)
     apply ablock_init_sound. destruct (eq_block b sp).
-    subst b. eapply SM. eapply mmatch_nonstack; eauto. congruence. 
+    subst b. eapply SM. eapply mmatch_nonstack; eauto. congruence.
     elim (NOSTACK b); auto.
   + (* globals *)
     rewrite PTree.gempty in H0; discriminate.
   + (* nonstack *)
     destruct (eq_block b sp). congruence. eapply SM; auto. eapply mmatch_nonstack; eauto.
   + (* top *)
-    eapply SM. eapply mmatch_top; eauto. 
+    eapply SM. eapply mmatch_top; eauto.
     destruct (eq_block b sp); congruence.
   + (* below *)
-    red; simpl; intros. destruct (eq_block b sp). 
+    red; simpl; intros. destruct (eq_block b sp).
     subst b. eapply mmatch_below; eauto. congruence.
     eapply mmatch_below; eauto.
 - (* genv *)
   eapply genv_match_exten with caller; eauto.
-  simpl; intros. destruct (eq_block b sp). intuition congruence. 
+  simpl; intros. destruct (eq_block b sp). intuition congruence.
   split; intros. rewrite SAME in H by eauto with va. auto.
   apply <- (proj1 GE2) in H. apply (proj1 GE1) in H. auto.
-  simpl; intros. destruct (eq_block b sp). congruence. 
+  simpl; intros. destruct (eq_block b sp). congruence.
   rewrite <- SAME; eauto with va.
 - (* sp *)
   simpl. apply dec_eq_true.
 - (* unchanged *)
-  simpl; intros. destruct (eq_block b sp). congruence. 
+  simpl; intros. destruct (eq_block b sp). congruence.
   symmetry. apply SAME; auto. eapply Plt_trans. eauto. apply BELOW. congruence.
 Qed.
 
@@ -820,19 +820,19 @@ Proof.
   {
     assert (forall b, f b = BCstack -> b = sp).
     { unfold f; intros. destruct (eq_block b sp); auto. eelim NOSTACK; eauto. }
-    intros. transitivity sp; auto. symmetry; auto. 
+    intros. transitivity sp; auto. symmetry; auto.
   }
   assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2).
   {
     assert (forall b id, f b = BCglob id -> callee b = BCglob id).
     { unfold f; intros. destruct (eq_block b sp). congruence. auto. }
-    intros. eapply (bc_glob callee); eauto. 
+    intros. eapply (bc_glob callee); eauto.
   }
   set (bc := BC f F_stack F_glob). unfold f in bc.
   assert (INCR1: bc_incr caller bc).
   {
-    red; simpl; intros. destruct (eq_block b sp). congruence. 
-    symmetry; apply SAME; auto. 
+    red; simpl; intros. destruct (eq_block b sp). congruence.
+    symmetry; apply SAME; auto.
   }
   assert (INCR2: bc_incr callee bc).
   {
@@ -840,14 +840,14 @@ Proof.
   }
 
 (* Invariance properties *)
-  assert (PM: forall b ofs p, pmatch callee b ofs p -> pmatch bc b ofs Nonstack).  
+  assert (PM: forall b ofs p, pmatch callee b ofs p -> pmatch bc b ofs Nonstack).
   {
     intros. assert (pmatch callee b ofs Ptop) by (eapply pmatch_top'; eauto).
     inv H0. constructor; simpl; destruct (eq_block b sp); congruence.
   }
   assert (VM: forall v x, vmatch callee v x -> vmatch bc v (Ifptr Nonstack)).
   {
-    intros. assert (vmatch callee v0 Vtop) by (eapply vmatch_top; eauto). 
+    intros. assert (vmatch callee v0 Vtop) by (eapply vmatch_top; eauto).
     inv H0; constructor; eauto.
   }
   assert (SM: forall b p, smatch callee m b p -> smatch bc m b Nonstack).
@@ -856,21 +856,21 @@ Proof.
   }
   assert (BSTK: bmatch bc m sp (am_stack am)).
   {
-    apply bmatch_incr with caller; eauto. 
+    apply bmatch_incr with caller; eauto.
   }
 (* Conclusions *)
   exists bc; splitall.
 - (* result value *)
   eapply VM; eauto.
 - (* environment *)
-  eapply ematch_incr; eauto. 
+  eapply ematch_incr; eauto.
 - (* romem *)
   apply romatch_exten with callee; auto.
-  intros; simpl. destruct (eq_block b sp); intuition. 
+  intros; simpl. destruct (eq_block b sp); intuition.
 - (* mmatch *)
   constructor; simpl; intros.
   + (* stack *)
-    destruct (eq_block b sp). 
+    destruct (eq_block b sp).
     subst b. exact BSTK.
     elim (NOSTACK b); auto.
   + (* globals *)
@@ -878,12 +878,12 @@ Proof.
   + (* nonstack *)
     destruct (eq_block b sp). congruence. eapply SM; auto. eapply mmatch_nonstack; eauto.
   + (* top *)
-    destruct (eq_block b sp). 
-    subst. apply smatch_ge with (ab_summary (am_stack am)). apply BSTK. apply pge_lub_l. 
+    destruct (eq_block b sp).
+    subst. apply smatch_ge with (ab_summary (am_stack am)). apply BSTK. apply pge_lub_l.
     apply smatch_ge with Nonstack. eapply SM. eapply mmatch_top; eauto. apply pge_lub_r.
   + (* below *)
-    red; simpl; intros. destruct (eq_block b sp). 
-    subst b. apply Plt_le_trans with bound. apply BELOW. congruence. auto. 
+    red; simpl; intros. destruct (eq_block b sp).
+    subst b. apply Plt_le_trans with bound. apply BELOW. congruence. auto.
     eapply mmatch_below; eauto.
 - (* genv *)
   eapply genv_match_exten; eauto.
@@ -892,7 +892,7 @@ Proof.
 - (* sp *)
   simpl. apply dec_eq_true.
 - (* unchanged *)
-  simpl; intros. destruct (eq_block b sp). congruence. 
+  simpl; intros. destruct (eq_block b sp). congruence.
   symmetry. apply SAME; auto. eapply Plt_trans. eauto. apply BELOW. congruence.
 Qed.
 
@@ -919,19 +919,19 @@ Proof.
   intros until am; intros EC GENV ARGS RO MM NOSTACK.
   (* Part 1: using ec_mem_inject *)
   exploit (@external_call_mem_inject ef _ _ ge vargs m t vres m' (inj_of_bc bc) m vargs).
-  apply inj_of_bc_preserves_globals; auto. 
+  apply inj_of_bc_preserves_globals; auto.
   exact EC.
   eapply mmatch_inj; eauto. eapply mmatch_below; eauto.
-  revert ARGS. generalize vargs. 
+  revert ARGS. generalize vargs.
   induction vargs0; simpl; intros; constructor.
-  eapply vmatch_inj; eauto. auto. 
+  eapply vmatch_inj; eauto. auto.
   intros (j' & vres' & m'' & EC' & IRES & IMEM & UNCH1 & UNCH2 & IINCR & ISEP).
   assert (JBELOW: forall b, Plt b (Mem.nextblock m) -> j' b = inj_of_bc bc b).
   {
     intros. destruct (inj_of_bc bc b) as [[b' delta] | ] eqn:EQ.
-    eapply IINCR; eauto. 
+    eapply IINCR; eauto.
     destruct (j' b) as [[b'' delta'] | ] eqn:EQ'; auto.
-    exploit ISEP; eauto. tauto. 
+    exploit ISEP; eauto. tauto.
   }
   (* Part 2: constructing bc' from j' *)
   set (f := fun b => if plt b (Mem.nextblock m)
@@ -941,13 +941,13 @@ Proof.
   {
     assert (forall b, f b = BCstack -> bc b = BCstack).
     { unfold f; intros. destruct (plt b (Mem.nextblock m)); auto. destruct (j' b); discriminate. }
-    intros. apply (bc_stack bc); auto. 
+    intros. apply (bc_stack bc); auto.
   }
   assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2).
   {
     assert (forall b id, f b = BCglob id -> bc b = BCglob id).
     { unfold f; intros. destruct (plt b (Mem.nextblock m)); auto. destruct (j' b); discriminate. }
-    intros. eapply (bc_glob bc); eauto. 
+    intros. eapply (bc_glob bc); eauto.
   }
   set (bc' := BC f F_stack F_glob). unfold f in bc'.
   assert (INCR: bc_incr bc bc').
@@ -956,34 +956,34 @@ Proof.
   }
   assert (BC'INV: forall b, bc' b <> BCinvalid -> exists b' delta, j' b = Some(b', delta)).
   {
-    simpl; intros. destruct (plt b (Mem.nextblock m)). 
+    simpl; intros. destruct (plt b (Mem.nextblock m)).
     exists b, 0. rewrite JBELOW by auto. apply inj_of_bc_valid; auto.
-    destruct (j' b) as [[b' delta] | ]. 
-    exists b', delta; auto. 
+    destruct (j' b) as [[b' delta] | ].
+    exists b', delta; auto.
     congruence.
   }
 
   (* Part 3: injection wrt j' implies matching with top wrt bc' *)
   assert (PMTOP: forall b b' delta ofs, j' b = Some (b', delta) -> pmatch bc' b ofs Ptop).
   {
-    intros. constructor. simpl; unfold f. 
+    intros. constructor. simpl; unfold f.
     destruct (plt b (Mem.nextblock m)).
-    rewrite JBELOW in H by auto. eapply inj_of_bc_inv; eauto. 
+    rewrite JBELOW in H by auto. eapply inj_of_bc_inv; eauto.
     rewrite H; congruence.
   }
   assert (VMTOP: forall v v', Val.inject j' v v' -> vmatch bc' v Vtop).
   {
-    intros. inv H; constructor. eapply PMTOP; eauto. 
+    intros. inv H; constructor. eapply PMTOP; eauto.
   }
   assert (SMTOP: forall b, bc' b <> BCinvalid -> smatch bc' m' b Ptop).
   {
     intros; split; intros.
-  - exploit BC'INV; eauto. intros (b' & delta & J'). 
-    exploit Mem.load_inject. eexact IMEM. eauto. eauto. intros (v' & A & B). 
+  - exploit BC'INV; eauto. intros (b' & delta & J').
+    exploit Mem.load_inject. eexact IMEM. eauto. eauto. intros (v' & A & B).
     eapply VMTOP; eauto.
-  - exploit BC'INV; eauto. intros (b'' & delta & J'). 
+  - exploit BC'INV; eauto. intros (b'' & delta & J').
     exploit Mem.loadbytes_inject. eexact IMEM. eauto. eauto. intros (bytes & A & B).
-    inv B. inv H3. inv H7. eapply PMTOP; eauto. 
+    inv B. inv H3. inv H7. eapply PMTOP; eauto.
   }
   (* Conclusions *)
   exists bc'; splitall.
@@ -1004,29 +1004,29 @@ Proof.
   exploit RO; eauto. intros (R & P & Q).
   split; auto.
   split. apply bmatch_incr with bc; auto. apply bmatch_inv with m; auto.
-  intros. eapply Mem.loadbytes_unchanged_on_1. eapply external_call_readonly; eauto. 
-  auto. intros; red. apply Q. 
-  intros; red; intros; elim (Q ofs). 
+  intros. eapply Mem.loadbytes_unchanged_on_1. eapply external_call_readonly; eauto.
+  auto. intros; red. apply Q.
+  intros; red; intros; elim (Q ofs).
   eapply external_call_max_perm with (m2 := m'); eauto.
   destruct (j' b); congruence.
 - (* mmatch top *)
   constructor; simpl; intros.
-  + apply ablock_init_sound. apply SMTOP. simpl; congruence. 
+  + apply ablock_init_sound. apply SMTOP. simpl; congruence.
   + rewrite PTree.gempty in H0; discriminate.
   + apply SMTOP; auto.
-  + apply SMTOP; auto. 
-  + red; simpl; intros. destruct (plt b (Mem.nextblock m)). 
-    eapply Plt_le_trans. eauto. eapply external_call_nextblock; eauto. 
-    destruct (j' b) as [[bx deltax] | ] eqn:J'. 
-    eapply Mem.valid_block_inject_1; eauto. 
+  + apply SMTOP; auto.
+  + red; simpl; intros. destruct (plt b (Mem.nextblock m)).
+    eapply Plt_le_trans. eauto. eapply external_call_nextblock; eauto.
+    destruct (j' b) as [[bx deltax] | ] eqn:J'.
+    eapply Mem.valid_block_inject_1; eauto.
     congruence.
 - (* nostack *)
-  red; simpl; intros. destruct (plt b (Mem.nextblock m)). 
+  red; simpl; intros. destruct (plt b (Mem.nextblock m)).
   apply NOSTACK; auto.
   destruct (j' b); congruence.
 - (* unmapped blocks are invariant *)
   intros. eapply Mem.loadbytes_unchanged_on_1; auto.
-  apply UNCH1; auto. intros; red. unfold inj_of_bc; rewrite H0; auto. 
+  apply UNCH1; auto. intros; red. unfold inj_of_bc; rewrite H0; auto.
 Qed.
 
 Remark list_forall2_in_l:
@@ -1036,8 +1036,8 @@ Proof.
   induction 1; simpl; intros.
 - contradiction.
 - destruct H1.
-  + subst. exists b1; auto. 
-  + exploit IHlist_forall2; eauto. intros (x2 & U & V). exists x2; auto. 
+  + subst. exists b1; auto.
+  + exploit IHlist_forall2; eauto. intros (x2 & U & V). exists x2; auto.
 Qed.
 
 (** ** Semantic invariant *)
@@ -1122,10 +1122,10 @@ Lemma sound_stack_ext:
 Proof.
   induction 1; intros INV.
 - constructor.
-- assert (Plt sp bound') by eauto with va. 
+- assert (Plt sp bound') by eauto with va.
   eapply sound_stack_public_call; eauto. apply IHsound_stack; intros.
   apply INV. xomega. rewrite SAME; auto. xomega. auto. auto.
-- assert (Plt sp bound') by eauto with va. 
+- assert (Plt sp bound') by eauto with va.
   eapply sound_stack_private_call; eauto. apply IHsound_stack; intros.
   apply INV. xomega. rewrite SAME; auto. xomega. auto. auto.
   apply bmatch_ext with m; auto. intros. apply INV. xomega. auto. auto. auto.
@@ -1137,7 +1137,7 @@ Lemma sound_stack_inv:
   (forall b ofs n, Plt b bound -> bc b = BCinvalid -> n >= 0 -> Mem.loadbytes m' b ofs n = Mem.loadbytes m b ofs n) ->
   sound_stack bc stk m' bound.
 Proof.
-  intros. eapply sound_stack_ext; eauto. intros. rewrite <- H0; auto. 
+  intros. eapply sound_stack_ext; eauto. intros. rewrite <- H0; auto.
 Qed.
 
 Lemma sound_stack_storev:
@@ -1147,13 +1147,13 @@ Lemma sound_stack_storev:
   sound_stack bc stk m bound ->
   sound_stack bc stk m' bound.
 Proof.
-  intros. apply sound_stack_inv with m; auto. 
+  intros. apply sound_stack_inv with m; auto.
   destruct addr; simpl in H; try discriminate.
   assert (A: pmatch bc b i Ptop).
   { inv H0; eapply pmatch_top'; eauto. }
-  inv A. 
-  intros. eapply Mem.loadbytes_store_other; eauto. left; congruence. 
-Qed. 
+  inv A.
+  intros. eapply Mem.loadbytes_store_other; eauto. left; congruence.
+Qed.
 
 Lemma sound_stack_storebytes:
   forall m b ofs bytes m' bc aaddr stk bound,
@@ -1162,12 +1162,12 @@ Lemma sound_stack_storebytes:
   sound_stack bc stk m bound ->
   sound_stack bc stk m' bound.
 Proof.
-  intros. apply sound_stack_inv with m; auto. 
+  intros. apply sound_stack_inv with m; auto.
   assert (A: pmatch bc b ofs Ptop).
   { inv H0; eapply pmatch_top'; eauto. }
-  inv A. 
-  intros. eapply Mem.loadbytes_storebytes_other; eauto. left; congruence. 
-Qed. 
+  inv A.
+  intros. eapply Mem.loadbytes_storebytes_other; eauto. left; congruence.
+Qed.
 
 Lemma sound_stack_free:
   forall m b lo hi m' bc stk bound,
@@ -1185,10 +1185,10 @@ Lemma sound_stack_new_bound:
   Ple bound bound' ->
   sound_stack bc stk m bound'.
 Proof.
-  intros. inv H. 
+  intros. inv H.
 - constructor.
-- eapply sound_stack_public_call with (bound' := bound'0); eauto. xomega. 
-- eapply sound_stack_private_call with (bound' := bound'0); eauto. xomega. 
+- eapply sound_stack_public_call with (bound' := bound'0); eauto. xomega.
+- eapply sound_stack_private_call with (bound' := bound'0); eauto. xomega.
 Qed.
 
 Lemma sound_stack_exten:
@@ -1197,15 +1197,15 @@ Lemma sound_stack_exten:
   (forall b, Plt b bound -> bc1 b = bc b) ->
   sound_stack bc1 stk m bound.
 Proof.
-  intros. inv H. 
+  intros. inv H.
 - constructor.
-- assert (Plt sp bound') by eauto with va. 
+- assert (Plt sp bound') by eauto with va.
   eapply sound_stack_public_call; eauto.
-  rewrite H0; auto. xomega. 
+  rewrite H0; auto. xomega.
   intros. rewrite H0; auto. xomega.
-- assert (Plt sp bound') by eauto with va. 
+- assert (Plt sp bound') by eauto with va.
   eapply sound_stack_private_call; eauto.
-  rewrite H0; auto. xomega. 
+  rewrite H0; auto. xomega.
   intros. rewrite H0; auto. xomega.
 Qed.
 
@@ -1226,7 +1226,7 @@ Lemma sound_succ_state:
   sound_state (State s f (Vptr sp Int.zero) pc' e' m').
 Proof.
   intros. exploit analyze_succ; eauto. intros (ae'' & am'' & AN & EM & MM).
-  econstructor; eauto. 
+  econstructor; eauto.
 Qed.
 
 Theorem sound_step:
@@ -1235,72 +1235,72 @@ Proof.
   induction 1; intros SOUND; inv SOUND.
 
 - (* nop *)
-  eapply sound_succ_state; eauto. simpl; auto. 
+  eapply sound_succ_state; eauto. simpl; auto.
   unfold transfer; rewrite H. auto.
 
 - (* op *)
-  eapply sound_succ_state; eauto. simpl; auto. 
-  unfold transfer; rewrite H. eauto. 
+  eapply sound_succ_state; eauto. simpl; auto.
+  unfold transfer; rewrite H. eauto.
   apply ematch_update; auto. eapply eval_static_operation_sound; eauto with va.
 
 - (* load *)
-  eapply sound_succ_state; eauto. simpl; auto. 
-  unfold transfer; rewrite H. eauto. 
-  apply ematch_update; auto. eapply loadv_sound; eauto with va. 
+  eapply sound_succ_state; eauto. simpl; auto.
+  unfold transfer; rewrite H. eauto.
+  apply ematch_update; auto. eapply loadv_sound; eauto with va.
   eapply eval_static_addressing_sound; eauto with va.
 
 - (* store *)
   exploit eval_static_addressing_sound; eauto with va. intros VMADDR.
-  eapply sound_succ_state; eauto. simpl; auto. 
-  unfold transfer; rewrite H. eauto. 
-  eapply storev_sound; eauto. 
-  destruct a; simpl in H1; try discriminate. eapply romatch_store; eauto. 
-  eapply sound_stack_storev; eauto. 
+  eapply sound_succ_state; eauto. simpl; auto.
+  unfold transfer; rewrite H. eauto.
+  eapply storev_sound; eauto.
+  destruct a; simpl in H1; try discriminate. eapply romatch_store; eauto.
+  eapply sound_stack_storev; eauto.
 
 - (* call *)
   assert (TR: transfer f rm pc ae am = transfer_call ae am args res).
   { unfold transfer; rewrite H; auto. }
-  unfold transfer_call, analyze_call in TR. 
-  destruct (pincl (am_nonstack am) Nonstack && 
+  unfold transfer_call, analyze_call in TR.
+  destruct (pincl (am_nonstack am) Nonstack &&
             forallb (fun av => vpincl av Nonstack) (aregs ae args)) eqn:NOLEAK.
 + (* private call *)
   InvBooleans.
-  exploit analyze_successor; eauto. simpl; eauto. rewrite TR. intros SUCC. 
+  exploit analyze_successor; eauto. simpl; eauto. rewrite TR. intros SUCC.
   exploit hide_stack; eauto. apply pincl_ge; auto.
   intros (bc' & A & B & C & D & E & F & G).
   apply sound_call_state with bc'; auto.
   * eapply sound_stack_private_call with (bound' := Mem.nextblock m) (bc' := bc); eauto.
     apply Ple_refl.
     eapply mmatch_below; eauto.
-    eapply mmatch_stack; eauto. 
-  * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v. 
-    apply D with (areg ae r). 
+    eapply mmatch_stack; eauto.
+  * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v.
+    apply D with (areg ae r).
     rewrite forallb_forall in H2. apply vpincl_ge.
     apply H2. apply in_map; auto.
     auto with va.
 + (* public call *)
-  exploit analyze_successor; eauto. simpl; eauto. rewrite TR. intros SUCC. 
+  exploit analyze_successor; eauto. simpl; eauto. rewrite TR. intros SUCC.
   exploit anonymize_stack; eauto. intros (bc' & A & B & C & D & E & F & G).
   apply sound_call_state with bc'; auto.
   * eapply sound_stack_public_call with (bound' := Mem.nextblock m) (bc' := bc); eauto.
     apply Ple_refl.
     eapply mmatch_below; eauto.
-  * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v. 
+  * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v.
     apply D with (areg ae r). auto with va.
 
 - (* tailcall *)
   exploit anonymize_stack; eauto. intros (bc' & A & B & C & D & E & F & G).
   apply sound_call_state with bc'; auto.
-  erewrite Mem.nextblock_free by eauto. 
+  erewrite Mem.nextblock_free by eauto.
   apply sound_stack_new_bound with stk.
   apply sound_stack_exten with bc.
   eapply sound_stack_free; eauto.
   intros. apply C. apply Plt_ne; auto.
-  apply Plt_Ple. eapply mmatch_below; eauto. congruence. 
-  intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v. 
+  apply Plt_Ple. eapply mmatch_below; eauto. congruence.
+  intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v.
   apply D with (areg ae r). auto with va.
-  eapply romatch_free; eauto. 
-  eapply mmatch_free; eauto. 
+  eapply romatch_free; eauto.
+  eapply mmatch_free; eauto.
 
 - (* builtin *)
   assert (SPVALID: Plt sp0 (Mem.nextblock m)) by (eapply mmatch_below; eauto with va).
@@ -1314,72 +1314,72 @@ Proof.
   { unfold transfer_builtin_default, analyze_call; intros TR'.
   set (aargs := map (abuiltin_arg ae am rm) args) in *.
   assert (ARGS: list_forall2 (vmatch bc) vargs aargs) by (eapply abuiltin_args_sound; eauto).
-  destruct (pincl (am_nonstack am) Nonstack && 
+  destruct (pincl (am_nonstack am) Nonstack &&
             forallb (fun av => vpincl av Nonstack) aargs)
         eqn: NOLEAK.
 * (* private builtin call *)
   InvBooleans. rewrite forallb_forall in H3.
   exploit hide_stack; eauto. apply pincl_ge; auto.
   intros (bc1 & A & B & C & D & E & F & G).
-  exploit external_call_match; eauto. 
+  exploit external_call_match; eauto.
   intros. exploit list_forall2_in_l; eauto. intros (av & U & V).
-  eapply D; eauto with va. apply vpincl_ge. apply H3; auto. 
+  eapply D; eauto with va. apply vpincl_ge. apply H3; auto.
   intros (bc2 & J & K & L & M & N & O & P & Q).
   exploit (return_from_private_call bc bc2); eauto.
   eapply mmatch_below; eauto.
   rewrite K; auto.
   intros. rewrite K; auto. rewrite C; auto.
-  apply bmatch_inv with m. eapply mmatch_stack; eauto. 
+  apply bmatch_inv with m. eapply mmatch_stack; eauto.
   intros. apply Q; auto.
-  eapply external_call_nextblock; eauto. 
+  eapply external_call_nextblock; eauto.
   intros (bc3 & U & V & W & X & Y & Z & AA).
-  eapply sound_succ_state with (bc := bc3); eauto. simpl; auto. 
-  apply set_builtin_res_sound; auto. 
-  apply sound_stack_exten with bc. 
+  eapply sound_succ_state with (bc := bc3); eauto. simpl; auto.
+  apply set_builtin_res_sound; auto.
+  apply sound_stack_exten with bc.
   apply sound_stack_inv with m. auto.
   intros. apply Q. red. eapply Plt_trans; eauto.
   rewrite C; auto.
   exact AA.
 * (* public builtin call *)
-  exploit anonymize_stack; eauto. 
+  exploit anonymize_stack; eauto.
   intros (bc1 & A & B & C & D & E & F & G).
-  exploit external_call_match; eauto. 
+  exploit external_call_match; eauto.
   intros. exploit list_forall2_in_l; eauto. intros (av & U & V). eapply D; eauto with va.
   intros (bc2 & J & K & L & M & N & O & P & Q).
   exploit (return_from_public_call bc bc2); eauto.
   eapply mmatch_below; eauto.
   rewrite K; auto.
   intros. rewrite K; auto. rewrite C; auto.
-  eapply external_call_nextblock; eauto. 
+  eapply external_call_nextblock; eauto.
   intros (bc3 & U & V & W & X & Y & Z & AA).
-  eapply sound_succ_state with (bc := bc3); eauto. simpl; auto. 
-  apply set_builtin_res_sound; auto. 
-  apply sound_stack_exten with bc. 
+  eapply sound_succ_state with (bc := bc3); eauto. simpl; auto.
+  apply set_builtin_res_sound; auto.
+  apply sound_stack_exten with bc.
   apply sound_stack_inv with m. auto.
   intros. apply Q. red. eapply Plt_trans; eauto.
   rewrite C; auto.
   exact AA.
   }
-  unfold transfer_builtin in TR. 
+  unfold transfer_builtin in TR.
   destruct ef; auto.
 + (* volatile load *)
   inv H0; auto. inv H3; auto. inv H1.
   exploit abuiltin_arg_sound; eauto. intros VM1.
   eapply sound_succ_state; eauto. simpl; auto.
-  apply set_builtin_res_sound; auto. 
+  apply set_builtin_res_sound; auto.
   inv H3.
   * (* true volatile access *)
     assert (V: vmatch bc v (Ifptr Glob)).
     { inv H4; simpl in *; constructor. econstructor. eapply GE; eauto. }
-    destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto. 
+    destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto.
     apply vnormalize_sound. eapply vmatch_ge; eauto. constructor. constructor.
   * (* normal memory access *)
     exploit loadv_sound; eauto. simpl; eauto. intros V.
-    destruct (va_strict tt). 
+    destruct (va_strict tt).
     apply vmatch_lub_l. auto.
-    eapply vnormalize_cast; eauto. eapply vmatch_top; eauto. 
+    eapply vnormalize_cast; eauto. eapply vmatch_top; eauto.
 + (* volatile store *)
-  inv H0; auto. inv H3; auto. inv H4; auto. inv H1. 
+  inv H0; auto. inv H3; auto. inv H4; auto. inv H1.
   exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H0. intros VM1.
   exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H2. intros VM2.
   inv H9.
@@ -1394,84 +1394,84 @@ Proof.
     eapply romatch_store; eauto.
     eapply sound_stack_storev; eauto. simpl; eauto.
 + (* memcpy *)
-  inv H0; auto. inv H3; auto. inv H4; auto. inv H1. 
+  inv H0; auto. inv H3; auto. inv H4; auto. inv H1.
   exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H0. intros VM1.
   exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H2. intros VM2.
-  eapply sound_succ_state; eauto. simpl; auto. 
+  eapply sound_succ_state; eauto. simpl; auto.
   apply set_builtin_res_sound; auto. constructor.
-  eapply storebytes_sound; eauto. 
-  apply match_aptr_of_aval; auto. 
-  eapply Mem.loadbytes_length; eauto. 
-  intros. eapply loadbytes_sound; eauto. apply match_aptr_of_aval; auto. 
-  eapply romatch_storebytes; eauto. 
-  eapply sound_stack_storebytes; eauto. 
+  eapply storebytes_sound; eauto.
+  apply match_aptr_of_aval; auto.
+  eapply Mem.loadbytes_length; eauto.
+  intros. eapply loadbytes_sound; eauto. apply match_aptr_of_aval; auto.
+  eapply romatch_storebytes; eauto.
+  eapply sound_stack_storebytes; eauto.
 + (* annot *)
-  inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor. 
+  inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor.
 + (* annot val *)
   inv H0; auto. inv H3; auto. inv H1.
   eapply sound_succ_state; eauto. simpl; auto.
   apply set_builtin_res_sound; auto. eapply abuiltin_arg_sound; eauto.
 + (* debug *)
-  inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor. 
+  inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor.
 
 - (* cond *)
-  eapply sound_succ_state; eauto. 
-  simpl. destruct b; auto. 
-  unfold transfer; rewrite H; auto. 
+  eapply sound_succ_state; eauto.
+  simpl. destruct b; auto.
+  unfold transfer; rewrite H; auto.
 
 - (* jumptable *)
-  eapply sound_succ_state; eauto. 
-  simpl. eapply list_nth_z_in; eauto. 
+  eapply sound_succ_state; eauto.
+  simpl. eapply list_nth_z_in; eauto.
   unfold transfer; rewrite H; auto.
 
 - (* return *)
   exploit anonymize_stack; eauto. intros (bc' & A & B & C & D & E & F & G).
   apply sound_return_state with bc'; auto.
-  erewrite Mem.nextblock_free by eauto. 
+  erewrite Mem.nextblock_free by eauto.
   apply sound_stack_new_bound with stk.
   apply sound_stack_exten with bc.
   eapply sound_stack_free; eauto.
   intros. apply C. apply Plt_ne; auto.
   apply Plt_Ple. eapply mmatch_below; eauto with va.
-  destruct or; simpl. eapply D; eauto. constructor. 
-  eapply romatch_free; eauto. 
+  destruct or; simpl. eapply D; eauto. constructor.
+  eapply romatch_free; eauto.
   eapply mmatch_free; eauto.
 
 - (* internal function *)
-  exploit allocate_stack; eauto. 
+  exploit allocate_stack; eauto.
   intros (bc' & A & B & C & D & E & F & G).
-  exploit (analyze_entrypoint rm f args m' bc'); eauto. 
+  exploit (analyze_entrypoint rm f args m' bc'); eauto.
   intros (ae & am & AN & EM & MM').
-  econstructor; eauto. 
-  erewrite Mem.alloc_result by eauto. 
+  econstructor; eauto.
+  erewrite Mem.alloc_result by eauto.
   apply sound_stack_exten with bc; auto.
-  apply sound_stack_inv with m; auto. 
+  apply sound_stack_inv with m; auto.
   intros. eapply Mem.loadbytes_alloc_unchanged; eauto.
   intros. apply F. erewrite Mem.alloc_result by eauto. auto.
 
 - (* external function *)
   exploit external_call_match; eauto with va.
   intros (bc' & A & B & C & D & E & F & G & K).
-  econstructor; eauto. 
+  econstructor; eauto.
   apply sound_stack_new_bound with (Mem.nextblock m).
   apply sound_stack_exten with bc; auto.
-  apply sound_stack_inv with m; auto. 
+  apply sound_stack_inv with m; auto.
   eapply external_call_nextblock; eauto.
 
 - (* return *)
   inv STK.
   + (* from public call *)
-   exploit return_from_public_call; eauto. 
+   exploit return_from_public_call; eauto.
    intros; rewrite SAME; auto.
-   intros (bc1 & A & B & C & D & E & F & G). 
+   intros (bc1 & A & B & C & D & E & F & G).
    destruct (analyze rm f)#pc as [ |ae' am'] eqn:EQ; simpl in AN; try contradiction. destruct AN as [A1 A2].
    eapply sound_regular_state with (bc := bc1); eauto.
    apply sound_stack_exten with bc'; auto.
-   eapply ematch_ge; eauto. apply ematch_update. auto. auto. 
+   eapply ematch_ge; eauto. apply ematch_update. auto. auto.
   + (* from private call *)
-   exploit return_from_private_call; eauto. 
+   exploit return_from_private_call; eauto.
    intros; rewrite SAME; auto.
-   intros (bc1 & A & B & C & D & E & F & G). 
+   intros (bc1 & A & B & C & D & E & F & G).
    destruct (analyze rm f)#pc as [ |ae' am'] eqn:EQ; simpl in AN; try contradiction. destruct AN as [A1 A2].
    eapply sound_regular_state with (bc := bc1); eauto.
    apply sound_stack_exten with bc'; auto.
@@ -1498,8 +1498,8 @@ Lemma initial_block_classification:
   /\ (forall b id, bc b = BCglob id -> Genv.find_symbol ge id = Some b)
   /\ (forall b, Mem.valid_block m b -> bc b <> BCinvalid).
 Proof.
-  intros. 
-  set (f := fun b => 
+  intros.
+  set (f := fun b =>
               if plt b (Genv.genv_next ge) then
                 match Genv.invert_symbol ge b with None => BCother | Some id => BCglob id end
               else
@@ -1511,8 +1511,8 @@ Proof.
     destruct (Genv.invert_symbol ge b1) as [id1|] eqn:I1; inv H0.
     destruct (plt b2 (Genv.genv_next ge)); try discriminate.
     destruct (Genv.invert_symbol ge b2) as [id2|] eqn:I2; inv H1.
-    exploit Genv.invert_find_symbol. eexact I1. 
-    exploit Genv.invert_find_symbol. eexact I2. 
+    exploit Genv.invert_find_symbol. eexact I1.
+    exploit Genv.invert_find_symbol. eexact I2.
     congruence.
   }
   assert (F_stack: forall b1 b2, f b1 = BCstack -> f b2 = BCstack -> b1 = b2).
@@ -1523,19 +1523,19 @@ Proof.
   }
   set (bc := BC f F_stack F_glob). unfold f in bc.
   exists bc; splitall.
-- split; simpl; intros. 
+- split; simpl; intros.
   + split; intros.
     * rewrite pred_dec_true by (eapply Genv.genv_symb_range; eauto).
       erewrite Genv.find_invert_symbol; eauto.
-    * apply Genv.invert_find_symbol. 
+    * apply Genv.invert_find_symbol.
       destruct (plt b (Genv.genv_next ge)); try discriminate.
       destruct (Genv.invert_symbol ge b); congruence.
-  + rewrite ! pred_dec_true by assumption. 
+  + rewrite ! pred_dec_true by assumption.
     destruct (Genv.invert_symbol); split; congruence.
 - red; simpl; intros. destruct (plt b (Genv.genv_next ge)); try congruence.
-  erewrite <- Genv.init_mem_genv_next by eauto. auto. 
-- red; simpl; intros. 
-  destruct (plt b (Genv.genv_next ge)). 
+  erewrite <- Genv.init_mem_genv_next by eauto. auto.
+- red; simpl; intros.
+  destruct (plt b (Genv.genv_next ge)).
   destruct (Genv.invert_symbol ge b); congruence.
   congruence.
 - simpl; intros. destruct (plt b (Genv.genv_next ge)); try discriminate.
@@ -1561,13 +1561,13 @@ Proof.
                vge (Ifptr Glob) av ->
                pge Glob (ab_summary (ablock_store chunk ab p av))).
   {
-    intros. simpl. unfold vplub; destruct av; auto. 
+    intros. simpl. unfold vplub; destruct av; auto.
     inv H0. apply plub_least; auto.
     inv H0. apply plub_least; auto.
   }
   destruct id; auto.
-  simpl. destruct (propagate_float_constants tt); auto. 
-  simpl. destruct (propagate_float_constants tt); auto. 
+  simpl. destruct (propagate_float_constants tt); auto.
+  simpl. destruct (propagate_float_constants tt); auto.
   apply DFL. constructor. constructor.
 Qed.
 
@@ -1576,7 +1576,7 @@ Lemma store_init_data_list_summary:
   pge Glob (ab_summary ab) ->
   pge Glob (ab_summary (store_init_data_list ab p idl)).
 Proof.
-  induction idl; simpl; intros. auto. apply IHidl. apply store_init_data_summary; auto. 
+  induction idl; simpl; intros. auto. apply IHidl. apply store_init_data_summary; auto.
 Qed.
 
 Lemma store_init_data_sound:
@@ -1588,7 +1588,7 @@ Proof.
   intros. destruct id; try (eapply ablock_store_sound; eauto; constructor).
   simpl. destruct (propagate_float_constants tt); eapply ablock_store_sound; eauto; constructor.
   simpl. destruct (propagate_float_constants tt); eapply ablock_store_sound; eauto; constructor.
-  simpl in H. inv H. auto. 
+  simpl in H. inv H. auto.
   simpl in H. destruct (Genv.find_symbol ge i) as [b'|] eqn:FS; try discriminate.
   eapply ablock_store_sound; eauto. constructor. constructor. apply GMATCH; auto.
 Qed.
@@ -1602,7 +1602,7 @@ Proof.
   induction idl; simpl; intros.
 - inv H; auto.
 - destruct (Genv.store_init_data ge m b p a) as [m1|] eqn:SI; try discriminate.
-  eapply IHidl; eauto. eapply store_init_data_sound; eauto. 
+  eapply IHidl; eauto. eapply store_init_data_sound; eauto.
 Qed.
 
 Lemma store_init_data_other:
@@ -1614,7 +1614,7 @@ Lemma store_init_data_other:
 Proof.
   intros. eapply bmatch_inv; eauto.
   intros. destruct id; try (eapply Mem.loadbytes_store_other; eauto; fail); simpl in H.
-  inv H; auto. 
+  inv H; auto.
   destruct (Genv.find_symbol ge i); try discriminate.
   eapply Mem.loadbytes_store_other; eauto.
 Qed.
@@ -1626,10 +1626,10 @@ Lemma store_init_data_list_other:
   bmatch bc m b' ab ->
   bmatch bc m' b' ab.
 Proof.
-  induction idl; simpl; intros. 
+  induction idl; simpl; intros.
   inv H; auto.
   destruct (Genv.store_init_data ge m b p a) as [m1|] eqn:SI; try discriminate.
-  eapply IHidl; eauto. eapply store_init_data_other; eauto. 
+  eapply IHidl; eauto. eapply store_init_data_other; eauto.
 Qed.
 
 Lemma store_zeros_same:
@@ -1640,8 +1640,8 @@ Lemma store_zeros_same:
 Proof.
   intros until n. functional induction (store_zeros m b pos n); intros.
 - inv H. auto.
-- eapply IHo; eauto. change p with (vplub (I Int.zero) p). 
-  eapply smatch_store; eauto. constructor. 
+- eapply IHo; eauto. change p with (vplub (I Int.zero) p).
+  eapply smatch_store; eauto. constructor.
 - discriminate.
 Qed.
 
@@ -1654,8 +1654,8 @@ Lemma store_zeros_other:
 Proof.
   intros until n. functional induction (store_zeros m b p n); intros.
 - inv H. auto.
-- eapply IHo; eauto. eapply bmatch_inv; eauto. 
-  intros. eapply Mem.loadbytes_store_other; eauto. 
+- eapply IHo; eauto. eapply bmatch_inv; eauto.
+  intros. eapply Mem.loadbytes_store_other; eauto.
 - discriminate.
 Qed.
 
@@ -1673,16 +1673,16 @@ Lemma alloc_global_match:
   initial_mem_match bc m' (Genv.add_global g idg).
 Proof.
   intros; red; intros. destruct idg as [id [fd | gv]]; simpl in *.
-- destruct (Mem.alloc m 0 1) as [m1 b1] eqn:ALLOC. 
+- destruct (Mem.alloc m 0 1) as [m1 b1] eqn:ALLOC.
   unfold Genv.find_var_info, Genv.add_global in H2; simpl in H2.
-  assert (Plt b (Mem.nextblock m)). 
+  assert (Plt b (Mem.nextblock m)).
   { rewrite <- H. eapply Genv.genv_vars_range; eauto. }
-  assert (b <> b1). 
+  assert (b <> b1).
   { apply Plt_ne. erewrite Mem.alloc_result by eauto. auto. }
-  apply bmatch_inv with m. 
-  eapply H0; eauto. 
-  intros. transitivity (Mem.loadbytes m1 b ofs n). 
-  eapply Mem.loadbytes_drop; eauto. 
+  apply bmatch_inv with m.
+  eapply H0; eauto.
+  intros. transitivity (Mem.loadbytes m1 b ofs n).
+  eapply Mem.loadbytes_drop; eauto.
   eapply Mem.loadbytes_alloc_unchanged; eauto.
 - set (sz := Genv.init_data_list_size (gvar_init gv)) in *.
   destruct (Mem.alloc m 0 sz) as [m1 b1] eqn:ALLOC.
@@ -1690,28 +1690,28 @@ Proof.
   destruct (Genv.store_init_data_list ge m2 b1 0 (gvar_init gv)) as [m3 | ] eqn:SIDL; try discriminate.
   unfold Genv.find_var_info, Genv.add_global in H2; simpl in H2.
   rewrite PTree.gsspec in H2. destruct (peq b (Genv.genv_next g)).
-+ inversion H2; clear H2; subst v. 
++ inversion H2; clear H2; subst v.
   assert (b = b1). { erewrite Mem.alloc_result by eauto. congruence. }
-  clear e. subst b. 
-  apply bmatch_inv with m3. 
-  eapply store_init_data_list_sound; eauto. 
+  clear e. subst b.
+  apply bmatch_inv with m3.
+  eapply store_init_data_list_sound; eauto.
   apply ablock_init_sound.
-  eapply store_zeros_same; eauto. 
-  split; intros. 
-  exploit Mem.load_alloc_same; eauto. intros EQ; subst v; constructor. 
+  eapply store_zeros_same; eauto.
+  split; intros.
+  exploit Mem.load_alloc_same; eauto. intros EQ; subst v; constructor.
   exploit Mem.loadbytes_alloc_same; eauto with coqlib. congruence.
-  intros. eapply Mem.loadbytes_drop; eauto. 
-  right; right; right. unfold Genv.perm_globvar. rewrite H3, H4. constructor. 
-+ assert (Plt b (Mem.nextblock m)). 
+  intros. eapply Mem.loadbytes_drop; eauto.
+  right; right; right. unfold Genv.perm_globvar. rewrite H3, H4. constructor.
++ assert (Plt b (Mem.nextblock m)).
   { rewrite <- H. eapply Genv.genv_vars_range; eauto. }
-  assert (b <> b1). 
+  assert (b <> b1).
   { apply Plt_ne. erewrite Mem.alloc_result by eauto. auto. }
   apply bmatch_inv with m3.
-  eapply store_init_data_list_other; eauto. 
-  eapply store_zeros_other; eauto. 
-  apply bmatch_inv with m. 
-  eapply H0; eauto. 
-  intros. eapply Mem.loadbytes_alloc_unchanged; eauto. 
+  eapply store_init_data_list_other; eauto.
+  eapply store_zeros_other; eauto.
+  apply bmatch_inv with m.
+  eapply H0; eauto.
+  intros. eapply Mem.loadbytes_alloc_unchanged; eauto.
   intros. eapply Mem.loadbytes_drop; eauto.
 Qed.
 
@@ -1722,12 +1722,12 @@ Lemma alloc_globals_match:
   Genv.alloc_globals ge m gl = Some m' ->
   initial_mem_match bc m' (Genv.add_globals g gl).
 Proof.
-  induction gl; simpl; intros. 
-- inv H1; auto. 
+  induction gl; simpl; intros.
+- inv H1; auto.
 - destruct (Genv.alloc_global ge m a) as [m1|] eqn:AG; try discriminate.
-  eapply IHgl; eauto. 
-  erewrite Genv.alloc_global_nextblock; eauto. simpl. congruence. 
-  eapply alloc_global_match; eauto. 
+  eapply IHgl; eauto.
+  erewrite Genv.alloc_global_nextblock; eauto. simpl. congruence.
+  eapply alloc_global_match; eauto.
 Qed.
 
 Definition romem_consistent (g: genv) (rm: romem) :=
@@ -1747,19 +1747,19 @@ Proof.
   intros; red; intros. destruct idg as [id1 [fd1 | v1]];
   unfold Genv.add_global, Genv.find_symbol, Genv.find_var_info, alloc_global in *; simpl in *.
 - rewrite PTree.gsspec in H0. rewrite PTree.grspec in H1. unfold PTree.elt_eq in *.
-  destruct (peq id id1). congruence. eapply H; eauto. 
+  destruct (peq id id1). congruence. eapply H; eauto.
 - rewrite PTree.gsspec in H0. destruct (peq id id1).
-+ inv H0. rewrite PTree.gss. 
++ inv H0. rewrite PTree.gss.
   destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)) eqn:RO.
   InvBooleans. rewrite negb_true_iff in H4.
   rewrite PTree.gss in H1.
-  exists v1. intuition congruence. 
+  exists v1. intuition congruence.
   rewrite PTree.grs in H1. discriminate.
-+ rewrite PTree.gso. eapply H; eauto. 
++ rewrite PTree.gso. eapply H; eauto.
   destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)).
-  rewrite PTree.gso in H1; auto. 
-  rewrite PTree.gro in H1; auto. 
-  apply Plt_ne. eapply Genv.genv_symb_range; eauto. 
+  rewrite PTree.gso in H1; auto.
+  rewrite PTree.gro in H1; auto.
+  apply Plt_ne. eapply Genv.genv_symb_range; eauto.
 Qed.
 
 Lemma alloc_globals_consistent:
@@ -1767,14 +1767,14 @@ Lemma alloc_globals_consistent:
   romem_consistent g rm ->
   romem_consistent (Genv.add_globals g gl) (List.fold_left alloc_global gl rm).
 Proof.
-  induction gl; simpl; intros. auto. apply IHgl. apply alloc_global_consistent; auto. 
+  induction gl; simpl; intros. auto. apply IHgl. apply alloc_global_consistent; auto.
 Qed.
 
 End INIT.
 
 Theorem initial_mem_matches:
   forall m,
-  Genv.init_mem prog = Some m -> 
+  Genv.init_mem prog = Some m ->
   exists bc,
      genv_match bc ge
   /\ bc_below bc (Mem.nextblock m)
@@ -1783,7 +1783,7 @@ Theorem initial_mem_matches:
   /\ (forall b, Mem.valid_block m b -> bc b <> BCinvalid).
 Proof.
   intros.
-  exploit initial_block_classification; eauto. intros (bc & GE & BELOW & NOSTACK & INV & VALID). 
+  exploit initial_block_classification; eauto. intros (bc & GE & BELOW & NOSTACK & INV & VALID).
   exists bc; splitall; auto.
   assert (A: initial_mem_match bc m ge).
   {
@@ -1796,34 +1796,34 @@ Proof.
     red; intros. rewrite PTree.gempty in H1; discriminate.
   }
   red; intros.
-  exploit B; eauto. intros (v & FV & RO & NVOL & EQ). 
-  split. subst ab. apply store_init_data_list_summary. constructor. 
-  split. subst ab. eapply A; eauto. 
-  unfold ge in FV; exploit Genv.init_mem_characterization; eauto. 
-  intros (P & Q & R). 
-  intros; red; intros. exploit Q; eauto. intros [U V]. 
-  unfold Genv.perm_globvar in V; rewrite RO, NVOL in V. inv V. 
+  exploit B; eauto. intros (v & FV & RO & NVOL & EQ).
+  split. subst ab. apply store_init_data_list_summary. constructor.
+  split. subst ab. eapply A; eauto.
+  unfold ge in FV; exploit Genv.init_mem_characterization; eauto.
+  intros (P & Q & R).
+  intros; red; intros. exploit Q; eauto. intros [U V].
+  unfold Genv.perm_globvar in V; rewrite RO, NVOL in V. inv V.
 Qed.
 
-End INITIAL. 
+End INITIAL.
 
 Require Import Axioms.
 
 Theorem sound_initial:
   forall prog st, initial_state prog st -> sound_state prog st.
 Proof.
-  destruct 1. 
+  destruct 1.
   exploit initial_mem_matches; eauto. intros (bc & GE & BELOW & NOSTACK & RM & VALID).
-  apply sound_call_state with bc. 
-- constructor. 
-- simpl; tauto. 
+  apply sound_call_state with bc.
+- constructor.
+- simpl; tauto.
 - exact RM.
 - apply mmatch_inj_top with m0.
   replace (inj_of_bc bc) with (Mem.flat_inj (Mem.nextblock m0)).
   eapply Genv.initmem_inject; eauto.
   symmetry; apply extensionality; unfold Mem.flat_inj; intros x.
-  destruct (plt x (Mem.nextblock m0)). 
-  apply inj_of_bc_valid; auto. 
+  destruct (plt x (Mem.nextblock m0)).
+  apply inj_of_bc_valid; auto.
   unfold inj_of_bc. erewrite bc_below_invalid; eauto.
 - exact GE.
 - exact NOSTACK.
@@ -1848,7 +1848,7 @@ Lemma avalue_sound:
   /\ bc sp = BCstack.
 Proof.
   intros. inv H. exists bc; split; auto. rewrite AN. apply EM.
-Qed. 
+Qed.
 
 Definition aaddr (a: VA.t) (r: reg) : aptr :=
   match a with
@@ -1867,7 +1867,7 @@ Lemma aaddr_sound:
 Proof.
   intros. inv H. exists bc; split; auto.
   unfold aaddr; rewrite AN. apply match_aptr_of_aval. rewrite <- H0. apply EM.
-Qed. 
+Qed.
 
 Definition aaddressing (a: VA.t) (addr: addressing) (args: list reg) : aptr :=
   match a with
@@ -1884,8 +1884,8 @@ Lemma aaddressing_sound:
   /\ genv_match bc (Genv.globalenv prog)
   /\ bc sp = BCstack.
 Proof.
-  intros. inv H. exists bc; split; auto. 
-  unfold aaddressing. rewrite AN. apply match_aptr_of_aval. 
+  intros. inv H. exists bc; split; auto.
+  unfold aaddressing. rewrite AN. apply match_aptr_of_aval.
   eapply eval_static_addressing_sound; eauto with va.
 Qed.
 
@@ -1895,7 +1895,7 @@ Qed.
 Definition aaddr_arg (a: VA.t) (ba: builtin_arg reg) : aptr :=
   match a with
   | VA.Bot => Pbot
-  | VA.State ae am => 
+  | VA.State ae am =>
       match ba with
       | BA r => aptr_of_aval (AE.get r ae)
       | BA_addrstack ofs => Stk ofs
@@ -1914,7 +1914,7 @@ Lemma aaddr_arg_sound_1:
   eval_builtin_arg ge (fun r : positive => rs # r) (Vptr sp Int.zero) m a (Vptr b ofs) ->
   pmatch bc b ofs (aaddr_arg (VA.State ae am) a).
 Proof.
-  intros. 
+  intros.
   apply pmatch_ge with (aptr_of_aval (abuiltin_arg ae am rm a)).
   simpl. destruct a; try (apply pge_top); simpl; apply pge_refl.
   apply match_aptr_of_aval. eapply abuiltin_arg_sound; eauto.