Hybrid 64bit/32bit PowerPC port

This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.

The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.

In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.

9 files changed, 320 insertions, 271 deletions

diff --git a/common/AST.v b/common/AST.v
index 34f29bb3..8a46a153 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -111,7 +111,7 @@ Definition cc_default :=
 
 Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}.
 Proof.
-  decide equality; apply bool_dec. 
+  decide equality; apply bool_dec.
 Defined.
 Global Opaque calling_convention_eq.
 
@@ -301,7 +301,7 @@ Lemma prog_defmap_unique:
   ~In id (map fst defs2) ->
   (prog_defmap p)!id = Some g.
 Proof.
-  unfold prog_defmap; intros. rewrite H. apply PTree_Properties.of_list_unique; auto. 
+  unfold prog_defmap; intros. rewrite H. apply PTree_Properties.of_list_unique; auto.
 Qed.
 
 Lemma prog_defmap_norepet:
@@ -408,7 +408,7 @@ Proof.
               OK (List.map (transform_program_globdef transf_fun) l)).
   { induction l as [ | [id g] l]; simpl.
   - auto.
-  - destruct g; simpl; rewrite IHl; simpl. auto. destruct v; auto. 
+  - destruct g; simpl; rewrite IHl; simpl. auto. destruct v; auto.
   }
   rewrite EQ; simpl. auto.
 Qed.
@@ -563,7 +563,7 @@ End TRANSF_PARTIAL_FUNDEF.
 Set Contextual Implicit.
 
 (** In some intermediate languages (LTL, Mach), 64-bit integers can be
-  split into two 32-bit halves and held in a pair of registers.  
+  split into two 32-bit halves and held in a pair of registers.
   Syntactically, this is captured by the type [rpair] below. *)
 
 Inductive rpair (A: Type) : Type :=
@@ -589,7 +589,7 @@ Definition regs_of_rpair (A: Type) (p: rpair A): list A :=
   end.
 
 Fixpoint regs_of_rpairs (A: Type) (l: list (rpair A)): list A :=
-  match l with 
+  match l with
   | nil => nil
   | p :: l => regs_of_rpair p ++ regs_of_rpairs l
   end.
@@ -603,8 +603,8 @@ Qed.
 Lemma in_regs_of_rpairs_inv:
   forall (A: Type) (x: A) l, In x (regs_of_rpairs l) -> exists p, In p l /\ In x (regs_of_rpair p).
 Proof.
-  induction l; simpl; intros. contradiction. 
-  rewrite in_app_iff in H; destruct H. 
+  induction l; simpl; intros. contradiction.
+  rewrite in_app_iff in H; destruct H.
   exists a; auto.
   apply IHl in H. firstorder auto.
 Qed.
diff --git a/common/Events.v b/common/Events.v
index 97d4f072..14cd27c5 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -976,7 +976,7 @@ Proof.
   {
     intros.
     apply Mem.unchanged_on_implies with (fun b1 ofs1 => b1 <> b).
-    apply Mem.unchanged_on_trans with m'. 
+    apply Mem.unchanged_on_trans with m'.
     eapply Mem.alloc_unchanged_on; eauto.
     eapply Mem.store_unchanged_on; eauto.
     intros. eapply Mem.valid_not_valid_diff; eauto with mem.
@@ -997,7 +997,7 @@ Proof.
 (* mem extends *)
 - inv H. inv H1. inv H7.
   assert (SZ: v2 = Vptrofs sz).
-  { unfold Vptrofs in *. destruct Archi.ptr64; inv H5; auto. } 
+  { unfold Vptrofs in *. destruct Archi.ptr64; inv H5; auto. }
   subst v2.
   exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
   intros [m3' [A B]].
@@ -1009,7 +1009,7 @@ Proof.
 (* mem injects *)
 - inv H0. inv H2. inv H8.
   assert (SZ: v' = Vptrofs sz).
-  { unfold Vptrofs in *. destruct Archi.ptr64; inv H6; auto. } 
+  { unfold Vptrofs in *. destruct Archi.ptr64; inv H6; auto. }
   subst v'.
   exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl.
   intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]].
@@ -1036,7 +1036,7 @@ Proof.
     rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence.
     rewrite <- (Ptrofs.of_int_to_int SF sz0), <- (Ptrofs.of_int_to_int SF sz). congruence.
   }
-  subst. 
+  subst.
   split. constructor. intuition congruence.
 Qed.
 
@@ -1093,7 +1093,7 @@ Proof.
     eapply Mem.free_range_perm; eauto.
   exploit Mem.address_inject; eauto.
     apply Mem.perm_implies with Freeable; auto with mem.
-    apply P. instantiate (1 := lo). 
+    apply P. instantiate (1 := lo).
     generalize (size_chunk_pos Mptr); omega.
   intro EQ.
   exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D).
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 9affd634..dd8a1eb9 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -259,7 +259,7 @@ Lemma add_globals_app:
   forall gl2 gl1 ge,
   add_globals ge (gl1 ++ gl2) = add_globals (add_globals ge gl1) gl2.
 Proof.
-  intros. apply fold_left_app. 
+  intros. apply fold_left_app.
 Qed.
 
 Program Definition empty_genv (pub: list ident): t :=
@@ -429,17 +429,17 @@ Proof.
   { induction l as [ | [id1 g1] l]; intros; simpl.
   - auto.
   - apply IHl. unfold P, add_global, find_symbol, find_def; simpl.
-    rewrite ! PTree.gsspec. destruct (peq id id1). 
+    rewrite ! PTree.gsspec. destruct (peq id id1).
     + subst id1. split; intros.
       inv H0. exists (genv_next ge); split; auto. apply PTree.gss.
       destruct H0 as (b & A & B). inv A. rewrite PTree.gss in B. auto.
     + red in H; rewrite H. split.
-      intros (b & A & B). exists b; split; auto. rewrite PTree.gso; auto. 
-      apply Plt_ne. eapply genv_symb_range; eauto. 
-      intros (b & A & B). rewrite PTree.gso in B. exists b; auto. 
-      apply Plt_ne. eapply genv_symb_range; eauto. 
+      intros (b & A & B). exists b; split; auto. rewrite PTree.gso; auto.
+      apply Plt_ne. eapply genv_symb_range; eauto.
+      intros (b & A & B). rewrite PTree.gso in B. exists b; auto.
+      apply Plt_ne. eapply genv_symb_range; eauto.
   }
-  apply REC. unfold P, find_symbol, find_def; simpl. 
+  apply REC. unfold P, find_symbol, find_def; simpl.
   rewrite ! PTree.gempty. split.
   congruence.
   intros (b & A & B); congruence.
@@ -770,12 +770,12 @@ Remark store_init_data_perm:
   store_init_data m b p i = Some m' ->
   (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
 Proof.
-  intros. 
+  intros.
   assert (forall chunk v,
           Mem.store chunk m b p v = Some m' ->
           (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm)).
     intros; split; eauto with mem.
-  destruct i; simpl in H; eauto. 
+  destruct i; simpl in H; eauto.
   inv H; tauto.
   destruct (find_symbol ge i); try discriminate. eauto.
 Qed.
@@ -788,7 +788,7 @@ Proof.
   induction idl as [ | i1 idl]; simpl; intros.
 - inv H; tauto.
 - destruct (store_init_data m b p i1) as [m1|] eqn:S1; try discriminate.
-  transitivity (Mem.perm m1 b' q k prm). 
+  transitivity (Mem.perm m1 b' q k prm).
   eapply store_init_data_perm; eauto.
   eapply IHidl; eauto.
 Qed.
@@ -849,8 +849,8 @@ Proof.
   intros until n. functional induction (store_zeros m b p n); intros.
 - inv H; apply Mem.unchanged_on_refl.
 - apply Mem.unchanged_on_trans with m'.
-+ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega. 
-+ apply IHo; auto. intros; apply H0; omega. 
++ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega.
++ apply IHo; auto. intros; apply H0; omega.
 - discriminate.
 Qed.
 
@@ -878,7 +878,7 @@ Proof.
 - inv H. apply Mem.unchanged_on_refl.
 - destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
   apply Mem.unchanged_on_trans with m1.
-  eapply store_init_data_unchanged; eauto. intros; apply H0; tauto. 
+  eapply store_init_data_unchanged; eauto. intros; apply H0; tauto.
   eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); omega.
 Qed.
 
@@ -947,8 +947,8 @@ Proof.
   intros; destruct i; simpl in H; try apply (Mem.loadbytes_store_same _ _ _ _ _ _ H).
 - inv H. simpl.
   assert (EQ: Z.of_nat (Z.to_nat z) = Z.max z 0).
-  { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } 
-  rewrite <- EQ. apply H0. omega. simpl. omega. 
+  { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. }
+  rewrite <- EQ. apply H0. omega. simpl. omega.
 - rewrite init_data_size_addrof. simpl.
   destruct (find_symbol ge i) as [b'|]; try discriminate.
   rewrite (Mem.loadbytes_store_same _ _ _ _ _ _ H).
@@ -976,14 +976,14 @@ Proof.
   eapply store_init_data_list_unchanged; eauto.
   intros; omega.
   intros; omega.
-  eapply store_init_data_loadbytes; eauto. 
+  eapply store_init_data_loadbytes; eauto.
   red; intros; apply H0. omega. omega.
   apply IHil with m1; auto.
-  red; intros. 
+  red; intros.
   eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => p + init_data_size i1 <= ofs1).
-  eapply store_init_data_unchanged; eauto. 
+  eapply store_init_data_unchanged; eauto.
+  intros; omega.
   intros; omega.
-  intros; omega. 
   apply H0. omega. omega.
   auto. auto.
 Qed.
@@ -1010,9 +1010,9 @@ Remark read_as_zero_unchanged:
   (forall i, ofs <= i < ofs + len -> P b i) ->
   read_as_zero m' b ofs len.
 Proof.
-  intros; red; intros. eapply Mem.load_unchanged_on; eauto. 
-  intros; apply H1. omega. 
-Qed. 
+  intros; red; intros. eapply Mem.load_unchanged_on; eauto.
+  intros; apply H1. omega.
+Qed.
 
 Lemma store_zeros_read_as_zero:
   forall m b p n m',
@@ -1078,7 +1078,7 @@ Proof.
   exploit IHil; eauto.
   set (P := fun (b': block) ofs' => p + init_data_size a <= ofs').
   apply read_as_zero_unchanged with (m := m) (P := P).
-  red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega. 
+  red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega.
   eapply store_init_data_unchanged with (P := P); eauto.
   intros; unfold P. omega.
   intros; unfold P. omega.
@@ -1094,7 +1094,7 @@ Proof.
   set (P := fun (b': block) ofs' => ofs' < p + init_data_size (Init_space z)).
   inv Heqo. apply read_as_zero_unchanged with (m := m1) (P := P).
   red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega.
-  eapply store_init_data_list_unchanged; eauto. 
+  eapply store_init_data_list_unchanged; eauto.
   intros; unfold P. omega.
   intros; unfold P. simpl; xomega.
 + rewrite init_data_size_addrof in *.
@@ -1118,7 +1118,7 @@ Proof.
   apply Mem.unchanged_on_implies with Q.
   apply Mem.unchanged_on_trans with m1.
   eapply Mem.alloc_unchanged_on; eauto.
-  eapply Mem.drop_perm_unchanged_on; eauto. 
+  eapply Mem.drop_perm_unchanged_on; eauto.
   intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem.
 - (* variable *)
   set (init := gvar_init v) in *.
@@ -1133,8 +1133,8 @@ Proof.
   apply Mem.unchanged_on_trans with m2.
   eapply store_zeros_unchanged; eauto.
   apply Mem.unchanged_on_trans with m3.
-  eapply store_init_data_list_unchanged; eauto. 
-  eapply Mem.drop_perm_unchanged_on; eauto. 
+  eapply store_init_data_list_unchanged; eauto.
+  eapply Mem.drop_perm_unchanged_on; eauto.
   intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem.
 Qed.
 
@@ -1147,7 +1147,7 @@ Proof.
 - inv H. apply Mem.unchanged_on_refl.
 - destruct (alloc_global m a) as [m''|] eqn:?; try discriminate.
   destruct a as [id g].
-  apply Mem.unchanged_on_trans with m''. 
+  apply Mem.unchanged_on_trans with m''.
   eapply alloc_global_unchanged; eauto.
   apply IHgl; auto.
 Qed.
@@ -1196,7 +1196,7 @@ Proof.
   exploit Mem.alloc_result; eauto. intros RES.
   rewrite H, <- RES. split.
   eapply Mem.perm_drop_1; eauto. omega.
-  intros. 
+  intros.
   assert (0 <= ofs < 1). { eapply Mem.perm_alloc_3; eauto. eapply Mem.perm_drop_4; eauto. }
   exploit Mem.perm_drop_2; eauto. intros ORD.
   split. omega. inv ORD; auto.
@@ -1210,35 +1210,35 @@ Proof.
   split. red; intros. eapply Mem.perm_drop_1; eauto.
   split. intros.
   assert (0 <= ofs < sz).
-  { eapply Mem.perm_alloc_3; eauto. 
+  { eapply Mem.perm_alloc_3; eauto.
     erewrite store_zeros_perm by eauto.
-    erewrite store_init_data_list_perm by eauto. 
+    erewrite store_init_data_list_perm by eauto.
     eapply Mem.perm_drop_4; eauto. }
   split; auto.
   eapply Mem.perm_drop_2; eauto.
   split. intros NOTVOL. apply load_store_init_data_invariant with m3.
-  intros. eapply Mem.load_drop; eauto. right; right; right. 
+  intros. eapply Mem.load_drop; eauto. right; right; right.
   unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem.
-  eapply store_init_data_list_charact; eauto. 
+  eapply store_init_data_list_charact; eauto.
   eapply store_zeros_read_as_zero; eauto.
-  intros NOTVOL. 
-  transitivity (Mem.loadbytes m3 b 0 sz). 
+  intros NOTVOL.
+  transitivity (Mem.loadbytes m3 b 0 sz).
   eapply Mem.loadbytes_drop; eauto. right; right; right.
   unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem.
   eapply store_init_data_list_loadbytes; eauto.
   eapply store_zeros_loadbytes; eauto.
 + assert (U: Mem.unchanged_on (fun _ _ => True) m m') by (eapply alloc_global_unchanged; eauto).
   assert (VALID: Mem.valid_block m b).
-  { red. rewrite <- H. eapply genv_defs_range; eauto. } 
+  { red. rewrite <- H. eapply genv_defs_range; eauto. }
   exploit H1; eauto.
   destruct gd0 as [f|v].
 * intros [A B]; split; intros.
   eapply Mem.perm_unchanged_on; eauto. exact I.
   eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I.
-* intros (A & B & C & D). split; [| split; [| split]]. 
+* intros (A & B & C & D). split; [| split; [| split]].
   red; intros. eapply Mem.perm_unchanged_on; eauto. exact I.
   intros. eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I.
-  intros. apply load_store_init_data_invariant with m; auto. 
+  intros. apply load_store_init_data_invariant with m; auto.
   intros. eapply Mem.load_unchanged_on_1; eauto. intros; exact I.
   intros. eapply Mem.loadbytes_unchanged_on; eauto. intros; exact I.
 - simpl. congruence.
@@ -1312,7 +1312,7 @@ Lemma init_mem_characterization_gen:
   init_mem p = Some m ->
   globals_initialized (globalenv p) (globalenv p) m.
 Proof.
-  intros. apply alloc_globals_initialized with Mem.empty. 
+  intros. apply alloc_globals_initialized with Mem.empty.
   auto.
   rewrite Mem.nextblock_empty. auto.
   red; intros. unfold find_def in H0; simpl in H0; rewrite PTree.gempty in H0; discriminate.
@@ -1499,7 +1499,7 @@ Proof.
   { intros. apply Mem.store_valid_access_3 in H0. destruct H0. congruence. }
   destruct i; simpl in H; eauto.
   simpl. apply Z.divide_1_l.
-  destruct (find_symbol ge i); try discriminate. eapply DFL. eassumption. 
+  destruct (find_symbol ge i); try discriminate. eapply DFL. eassumption.
   unfold Mptr, init_data_alignment; destruct Archi.ptr64; auto.
 Qed.
 
@@ -1537,14 +1537,14 @@ Theorem init_mem_inversion:
   init_data_list_aligned 0 v.(gvar_init)
   /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol (globalenv p) i = Some b.
 Proof.
-  intros until v. unfold init_mem. set (ge := globalenv p). 
-  revert m. generalize Mem.empty. generalize (prog_defs p). 
+  intros until v. unfold init_mem. set (ge := globalenv p).
+  revert m. generalize Mem.empty. generalize (prog_defs p).
   induction l as [ | idg1 defs ]; simpl; intros m m'; intros.
 - contradiction.
 - destruct (alloc_global ge m idg1) as [m''|] eqn:A; try discriminate.
   destruct H0.
-+ subst idg1; simpl in A. 
-  set (il := gvar_init v) in *. set (sz := init_data_list_size il) in *. 
++ subst idg1; simpl in A.
+  set (il := gvar_init v) in *. set (sz := init_data_list_size il) in *.
   destruct (Mem.alloc m 0 sz) as [m1 b].
   destruct (store_zeros m1 b 0 sz) as [m2|]; try discriminate.
   destruct (store_init_data_list ge m2 b 0 il) as [m3|] eqn:B; try discriminate.
@@ -1565,7 +1565,7 @@ Proof.
 - exists m; auto.
 - apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. omega.
 - destruct (Mem.valid_access_store m Mint8unsigned b p Vzero) as (m' & STORE).
-  split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega. 
+  split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega.
   simpl. apply Z.divide_1_l.
   congruence.
 Qed.
@@ -1577,17 +1577,17 @@ Lemma store_init_data_exists:
   (forall id ofs, i = Init_addrof id ofs -> exists b, find_symbol ge id = Some b) ->
   exists m', store_init_data ge m b p i = Some m'.
 Proof.
-  intros. 
+  intros.
   assert (DFL: forall chunk v,
           init_data_size i = size_chunk chunk ->
           init_data_alignment i = align_chunk chunk ->
           exists m', Mem.store chunk m b p v = Some m').
   { intros. destruct (Mem.valid_access_store m chunk b p v) as (m' & STORE).
-    split. rewrite <- H2; auto. rewrite <- H3; auto. 
+    split. rewrite <- H2; auto. rewrite <- H3; auto.
     exists m'; auto. }
   destruct i; eauto.
   simpl. exists m; auto.
-  simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eapply DFL. 
+  simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eapply DFL.
   unfold init_data_size, Mptr. destruct Archi.ptr64; auto.
   unfold init_data_alignment, Mptr. destruct Archi.ptr64; auto.
 Qed.
@@ -1601,11 +1601,11 @@ Lemma store_init_data_list_exists:
 Proof.
   induction il as [ | i1 il ]; simpl; intros.
 - exists m; auto.
-- destruct H0. 
+- destruct H0.
   destruct (@store_init_data_exists m b p i1) as (m1 & S1); eauto.
   red; intros. apply H. generalize (init_data_list_size_pos il); omega.
-  rewrite S1. 
-  apply IHil; eauto. 
+  rewrite S1.
+  apply IHil; eauto.
   red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); omega.
 Qed.
 
@@ -1622,7 +1622,7 @@ Proof.
   intros m [id [f|v]]; intros; simpl.
 - destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC.
   destruct (Mem.range_perm_drop_2 m1 b 0 1 Nonempty) as [m2 DROP].
-  red; intros; eapply Mem.perm_alloc_2; eauto. 
+  red; intros; eapply Mem.perm_alloc_2; eauto.
   exists m2; auto.
 - destruct H as [P Q].
   set (sz := init_data_list_size (gvar_init v)).
@@ -1651,14 +1651,14 @@ Theorem init_mem_exists:
      /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol (globalenv p) i = Some b) ->
   exists m, init_mem p = Some m.
 Proof.
-  intros. set (ge := globalenv p) in *. 
+  intros. set (ge := globalenv p) in *.
   unfold init_mem. revert H. generalize (prog_defs p) Mem.empty.
   induction l as [ | idg l]; simpl; intros.
 - exists m; auto.
 - destruct (@alloc_global_exists ge m idg) as [m1 A1].
   destruct idg as [id [f|v]]; eauto.
-  fold ge. rewrite A1. eapply IHl; eauto. 
-Qed. 
+  fold ge. rewrite A1. eapply IHl; eauto.
+Qed.
 
 End GENV.
 
@@ -1685,8 +1685,8 @@ Lemma add_global_match:
 Proof.
   intros. destruct H. constructor; simpl; intros.
 - congruence.
-- rewrite mge_next0, ! PTree.gsspec. destruct (peq id0 id); auto. 
-- rewrite mge_next0, ! PTree.gsspec. destruct (peq b (genv_next ge1)). 
+- rewrite mge_next0, ! PTree.gsspec. destruct (peq id0 id); auto.
+- rewrite mge_next0, ! PTree.gsspec. destruct (peq b (genv_next ge1)).
   constructor; auto.
   auto.
 Qed.
@@ -1718,7 +1718,7 @@ Hypothesis progmatch: match_program_gen match_fundef match_varinfo ctx p tp.
 Lemma globalenvs_match:
   match_genvs (match_globdef match_fundef match_varinfo ctx) (globalenv p) (globalenv tp).
 Proof.
-  intros. apply add_globals_match. apply progmatch. 
+  intros. apply add_globals_match. apply progmatch.
   constructor; simpl; intros; auto. rewrite ! PTree.gempty. constructor.
 Qed.
 
@@ -1734,7 +1734,7 @@ Theorem find_def_match:
   find_def (globalenv tp) b = Some tg /\ match_globdef match_fundef match_varinfo ctx g tg.
 Proof.
   intros. generalize (find_def_match_2 b). rewrite H; intros R; inv R.
-  exists y; auto. 
+  exists y; auto.
 Qed.
 
 Theorem find_funct_ptr_match:
@@ -1743,8 +1743,8 @@ Theorem find_funct_ptr_match:
   exists cunit tf,
   find_funct_ptr (globalenv tp) b = Some tf /\ match_fundef cunit f tf /\ linkorder cunit ctx.
 Proof.
-  intros. rewrite find_funct_ptr_iff in *. apply find_def_match in H. 
-  destruct H as (tg & P & Q). inv Q. 
+  intros. rewrite find_funct_ptr_iff in *. apply find_def_match in H.
+  destruct H as (tg & P & Q). inv Q.
   exists ctx', f2; intuition auto. apply find_funct_ptr_iff; auto.
 Qed.
 
@@ -1766,8 +1766,8 @@ Theorem find_var_info_match:
   exists tv,
   find_var_info (globalenv tp) b = Some tv /\ match_globvar match_varinfo v tv.
 Proof.
-  intros. rewrite find_var_info_iff in *. apply find_def_match in H. 
-  destruct H as (tg & P & Q). inv Q. 
+  intros. rewrite find_var_info_iff in *. apply find_def_match in H.
+  destruct H as (tg & P & Q). inv Q.
   exists v2; split; auto. apply find_var_info_iff; auto.
 Qed.
 
@@ -1783,10 +1783,10 @@ Theorem senv_match:
 Proof.
   red; simpl. repeat split.
 - apply find_symbol_match.
-- intros. unfold public_symbol. rewrite find_symbol_match. 
-  rewrite ! globalenv_public. 
+- intros. unfold public_symbol. rewrite find_symbol_match.
+  rewrite ! globalenv_public.
   destruct progmatch as (P & Q & R). rewrite R. auto.
-- intros. unfold block_is_volatile. 
+- intros. unfold block_is_volatile.
   destruct globalenvs_match as [P Q R]. specialize (R b).
   unfold find_var_info, find_def.
   inv R; auto.
@@ -1820,7 +1820,7 @@ Proof.
   { destruct a1 as [id1 g1]; destruct b1 as [id2 g2]; destruct H; simpl in *.
     subst id2. inv H2.
   - auto.
-  - inv H; simpl in *. 
+  - inv H; simpl in *.
     set (sz := init_data_list_size init) in *.
     destruct (Mem.alloc m 0 sz) as [m2 b] eqn:?.
     destruct (store_zeros m2 b 0 sz) as [m3|] eqn:?; try discriminate.
@@ -1853,7 +1853,7 @@ Theorem find_funct_ptr_transf_partial:
   exists tf,
   find_funct_ptr (globalenv tp) b = Some tf /\ transf f = OK tf.
 Proof.
-  intros. exploit (find_funct_ptr_match progmatch); eauto. 
+  intros. exploit (find_funct_ptr_match progmatch); eauto.
   intros (cu & tf & P & Q & R); exists tf; auto.
 Qed.
 
@@ -1863,7 +1863,7 @@ Theorem find_funct_transf_partial:
   exists tf,
   find_funct (globalenv tp) v = Some tf /\ transf f = OK tf.
 Proof.
-  intros. exploit (find_funct_match progmatch); eauto. 
+  intros. exploit (find_funct_match progmatch); eauto.
   intros (cu & tf & P & Q & R); exists tf; auto.
 Qed.
 
@@ -1871,7 +1871,7 @@ Theorem find_symbol_transf_partial:
   forall (s : ident),
   find_symbol (globalenv tp) s = find_symbol (globalenv p) s.
 Proof.
-  intros. eapply (find_symbol_match progmatch). 
+  intros. eapply (find_symbol_match progmatch).
 Qed.
 
 Theorem senv_transf_partial:
@@ -1901,7 +1901,7 @@ Theorem find_funct_ptr_transf:
   find_funct_ptr (globalenv p) b = Some f ->
   find_funct_ptr (globalenv tp) b = Some (transf f).
 Proof.
-  intros. exploit (find_funct_ptr_match progmatch); eauto. 
+  intros. exploit (find_funct_ptr_match progmatch); eauto.
   intros (cu & tf & P & Q & R). congruence.
 Qed.
 
@@ -1910,7 +1910,7 @@ Theorem find_funct_transf:
   find_funct (globalenv p) v = Some f ->
   find_funct (globalenv tp) v = Some (transf f).
 Proof.
-  intros. exploit (find_funct_match progmatch); eauto. 
+  intros. exploit (find_funct_match progmatch); eauto.
   intros (cu & tf & P & Q & R). congruence.
 Qed.
 
diff --git a/common/Linking.v b/common/Linking.v
index 52e774db..eaa95462 100644
--- a/common/Linking.v
+++ b/common/Linking.v
@@ -111,13 +111,13 @@ Inductive linkorder_varinit: list init_data -> list init_data -> Prop :=
 
 Instance Linker_varinit : Linker (list init_data) := {
   link := link_varinit;
-  linkorder := linkorder_varinit    
+  linkorder := linkorder_varinit
 }.
 Proof.
 - intros. constructor.
 - intros. inv H; inv H0; constructor; auto.
   congruence.
-  simpl. generalize (init_data_list_size_pos z). xomega. 
+  simpl. generalize (init_data_list_size_pos z). xomega.
 - unfold link_varinit; intros until z.
   destruct (classify_init x) eqn:Cx, (classify_init y) eqn:Cy; intros E; inv E; try (split; constructor; fail).
 + destruct (zeq sz (Z.max sz0 0 + 0)); inv H0.
@@ -159,7 +159,7 @@ Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := {
   linkorder := linkorder_vardef
 }.
 Proof.
-- intros. destruct x; constructor; apply linkorder_refl. 
+- intros. destruct x; constructor; apply linkorder_refl.
 - intros. inv H; inv H0. constructor; eapply linkorder_trans; eauto.
 - unfold link_vardef; intros until z.
   destruct x as [f1 i1 r1 v1], y as [f2 i2 r2 v2]; simpl.
@@ -214,7 +214,7 @@ Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F
 Proof.
 - intros. destruct x; constructor; apply linkorder_refl.
 - intros. inv H; inv H0; constructor; eapply linkorder_trans; eauto.
-- unfold link_def; intros.  
+- unfold link_def; intros.
   destruct x as [f1|v1], y as [f2|v2]; try discriminate.
 + destruct (link f1 f2) as [f|] eqn:L; inv H. apply link_linkorder in L.
   split; constructor; tauto.
@@ -229,7 +229,7 @@ Global Opaque Linker_def.
   a global definition in one unit but not in the other, this definition
   is left unchanged in the result of the link.  If a name has
   global definitions in both units, and is public (not static) in both,
-  the two definitions are linked as per [Linker_def] above.  
+  the two definitions are linked as per [Linker_def] above.
 
   If one or both definitions are static (not public), we should ideally
   rename it so that it can be kept unchanged in the result of the link.
@@ -284,8 +284,8 @@ Proof.
   unfold link_prog; intros p E.
   destruct (ident_eq (prog_main p1) (prog_main p2)); try discriminate.
   destruct (PTree_Properties.for_all dm1 link_prog_check) eqn:C; inv E.
-  rewrite PTree_Properties.for_all_correct in C. 
-  split; auto. split; auto. 
+  rewrite PTree_Properties.for_all_correct in C.
+  split; auto. split; auto.
   intros. exploit C; eauto. unfold link_prog_check. rewrite H0. intros.
   destruct (in_dec peq id (prog_public p1)); try discriminate.
   destruct (in_dec peq id (prog_public p2)); try discriminate.
@@ -303,7 +303,7 @@ Lemma link_prog_succeeds:
             prog_public := p1.(prog_public) ++ p2.(prog_public);
             prog_defs := PTree.elements (PTree.combine link_prog_merge dm1 dm2) |}.
 Proof.
-  intros. unfold link_prog. unfold proj_sumbool. rewrite H, dec_eq_true. simpl. 
+  intros. unfold link_prog. unfold proj_sumbool. rewrite H, dec_eq_true. simpl.
   replace (PTree_Properties.for_all dm1 link_prog_check) with true; auto.
   symmetry. apply PTree_Properties.for_all_correct; intros. rename a into gd1.
   unfold link_prog_check. destruct dm2!x as [gd2|] eqn:G2; auto.
@@ -334,29 +334,29 @@ Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program
 }.
 Proof.
 - intros; split; auto. split. apply incl_refl. intros.
-  exists gd1; split; auto. split; auto. apply linkorder_refl. 
+  exists gd1; split; auto. split; auto. apply linkorder_refl.
 
-- intros x y z (A1 & B1 & C1) (A2 & B2 & C2). 
-  split. congruence. split. red; eauto. 
-  intros. exploit C1; eauto. intros (gd2 & P & Q & R). 
-  exploit C2; eauto. intros (gd3 & U & X & Y). 
-  exists gd3. split; auto. split. eapply linkorder_trans; eauto. 
-  intros. transitivity gd2. apply Y. auto. apply R. red; intros; elim H0; auto. 
+- intros x y z (A1 & B1 & C1) (A2 & B2 & C2).
+  split. congruence. split. red; eauto.
+  intros. exploit C1; eauto. intros (gd2 & P & Q & R).
+  exploit C2; eauto. intros (gd3 & U & X & Y).
+  exists gd3. split; auto. split. eapply linkorder_trans; eauto.
+  intros. transitivity gd2. apply Y. auto. apply R. red; intros; elim H0; auto.
 
 - intros. apply link_prog_inv in H. destruct H as (L1 & L2 & L3).
   subst z; simpl. intuition auto.
 + red; intros; apply in_app_iff; auto.
-+ rewrite prog_defmap_elements, PTree.gcombine, H by auto. 
++ rewrite prog_defmap_elements, PTree.gcombine, H by auto.
   destruct (prog_defmap y)!id as [gd2|] eqn:GD2; simpl.
 * exploit L2; eauto. intros (P & Q & gd & R).
-  exists gd; split. auto. split. apply link_linkorder in R; tauto. 
+  exists gd; split. auto. split. apply link_linkorder in R; tauto.
   rewrite in_app_iff; tauto.
 * exists gd1; split; auto. split. apply linkorder_refl. auto.
 + red; intros; apply in_app_iff; auto.
-+ rewrite prog_defmap_elements, PTree.gcombine, H by auto. 
++ rewrite prog_defmap_elements, PTree.gcombine, H by auto.
   destruct (prog_defmap x)!id as [gd2|] eqn:GD2; simpl.
 * exploit L2; eauto. intros (P & Q & gd & R).
-  exists gd; split. auto. split. apply link_linkorder in R; tauto. 
+  exists gd; split. auto. split. apply link_linkorder in R; tauto.
   rewrite in_app_iff; tauto.
 * exists gd1; split; auto. split. apply linkorder_refl. auto.
 Defined.
@@ -417,24 +417,24 @@ Theorem match_program_defmap:
   forall ctx p1 p2, match_program_gen ctx p1 p2 ->
   forall id, option_rel (match_globdef ctx) (prog_defmap p1)!id (prog_defmap p2)!id.
 Proof.
-  intros. apply PTree_Properties.of_list_related. apply H. 
+  intros. apply PTree_Properties.of_list_related. apply H.
 Qed.
 
 Lemma match_program_gen_main:
   forall ctx p1 p2, match_program_gen ctx p1 p2 -> p2.(prog_main) = p1.(prog_main).
 Proof.
-  intros. apply H. 
+  intros. apply H.
 Qed.
 
 Lemma match_program_public:
   forall ctx p1 p2, match_program_gen ctx p1 p2 -> p2.(prog_public) = p1.(prog_public).
 Proof.
-  intros. apply H. 
+  intros. apply H.
 Qed.
 
 End MATCH_PROGRAM_GENERIC.
 
-(** In many cases, the context for [match_program_gen] is the source program or 
+(** In many cases, the context for [match_program_gen] is the source program or
   source compilation unit itself.  We provide a specialized definition for this case. *)
 
 Definition match_program {F1 V1 F2 V2: Type} {LF: Linker F1} {LV: Linker V1}
@@ -464,7 +464,7 @@ Lemma match_program_implies:
   (forall v w, match_varinfo1 v w -> match_varinfo2 v w) ->
   match_program match_fundef2 match_varinfo2 p p'.
 Proof.
-  intros. destruct H as [P Q]. split; auto. 
+  intros. destruct H as [P Q]. split; auto.
   eapply list_forall2_imply; eauto.
   intros. inv H3. split; auto. inv H5.
   econstructor; eauto.
@@ -488,12 +488,12 @@ Theorem match_transform_partial_program2:
   match_program_gen match_fundef match_varinfo ctx p tp.
 Proof.
   unfold transform_partial_program2; intros. monadInv H.
-  red; simpl; split; auto. 
-  revert x EQ. generalize (prog_defs p). 
+  red; simpl; split; auto.
+  revert x EQ. generalize (prog_defs p).
   induction l as [ | [i g] l]; simpl; intros.
 - monadInv EQ. constructor.
 - destruct g as [f|v].
-+ destruct (transf_fun i f) as [tf|?] eqn:TF; monadInv EQ. 
++ destruct (transf_fun i f) as [tf|?] eqn:TF; monadInv EQ.
   constructor; auto. split; simpl; auto. econstructor. apply linkorder_refl. eauto.
 + destruct (transf_globvar transf_var i v) as [tv|?] eqn:TV; monadInv EQ.
   constructor; auto. split; simpl; auto. constructor.
@@ -509,7 +509,7 @@ Theorem match_transform_partial_program_contextual:
   (forall f tf, transf_fun f = OK tf -> match_fundef p f tf) ->
   match_program match_fundef eq p tp.
 Proof.
-  intros. 
+  intros.
   eapply match_transform_partial_program2. eexact H.
   auto.
   simpl; intros. congruence.
@@ -523,8 +523,8 @@ Theorem match_transform_program_contextual:
   (forall f, match_fundef p f (transf_fun f)) ->
   match_program match_fundef eq p (transform_program transf_fun p).
 Proof.
-  intros. 
-  eapply match_transform_partial_program_contextual. 
+  intros.
+  eapply match_transform_partial_program_contextual.
   apply transform_program_partial_program with (transf_fun := transf_fun).
   simpl; intros. inv H0. auto.
 Qed.
@@ -582,11 +582,11 @@ Lemma link_match_globvar:
   match_globvar match_varinfo v1 tv1 -> match_globvar match_varinfo v2 tv2 ->
   exists tv, link tv1 tv2 = Some tv /\ match_globvar match_varinfo v tv.
 Proof.
-  simpl; intros. unfold link_vardef in *. inv H0; inv H1; simpl in *. 
+  simpl; intros. unfold link_vardef in *. inv H0; inv H1; simpl in *.
   destruct (link i1 i0) as [info'|] eqn:LINFO; try discriminate.
   destruct (link init init0) as [init'|] eqn:LINIT; try discriminate.
   destruct (eqb ro ro0 && eqb vo vo0); inv H.
-  exploit link_match_varinfo; eauto. intros (tinfo & P & Q). rewrite P. 
+  exploit link_match_varinfo; eauto. intros (tinfo & P & Q). rewrite P.
   econstructor; split. eauto. constructor. auto.
 Qed.
 
@@ -603,7 +603,7 @@ Proof.
   exploit link_match_fundef; eauto. intros (tf & P & Q).
   assert (X: exists ctx', linkorder ctx' ctx /\ match_fundef ctx' f tf).
   { destruct Q as [Q|Q]; econstructor; (split; [|eassumption]).
-    apply linkorder_trans with ctx1; auto. 
+    apply linkorder_trans with ctx1; auto.
     apply linkorder_trans with ctx2; auto. }
   destruct X as (cu & X & Y).
   exists (Gfun tf); split. rewrite P; auto. econstructor; eauto.
@@ -618,7 +618,7 @@ Lemma match_globdef_linkorder:
   linkorder ctx ctx' ->
   match_globdef match_fundef match_varinfo ctx' g tg.
 Proof.
-  intros. inv H. 
+  intros. inv H.
 - econstructor. eapply linkorder_trans; eauto. auto.
 - constructor; auto.
 Qed.
@@ -635,25 +635,25 @@ Proof.
   generalize H0; intros (A1 & B1 & C1).
   generalize H1; intros (A2 & B2 & C2).
   econstructor; split.
-- apply link_prog_succeeds. 
-+ congruence. 
-+ intros. 
+- apply link_prog_succeeds.
++ congruence.
++ intros.
   generalize (match_program_defmap _ _ _ _ _ H0 id) (match_program_defmap _ _ _ _ _ H1 id).
   rewrite H4, H5. intros R1 R2; inv R1; inv R2.
   exploit Q; eauto. intros (X & Y & gd & Z).
-  exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto. 
+  exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto.
   intros (tg & TL & _). intuition congruence.
 - split; [|split].
-+ rewrite R. apply PTree.elements_canonical_order'. intros id. 
++ rewrite R. apply PTree.elements_canonical_order'. intros id.
   rewrite ! PTree.gcombine by auto.
   generalize (match_program_defmap _ _ _ _ _ H0 id) (match_program_defmap _ _ _ _ _ H1 id).
   clear R. intros R1 R2; inv R1; inv R2; unfold link_prog_merge.
 * constructor.
-* constructor. apply match_globdef_linkorder with ctx2; auto. 
+* constructor. apply match_globdef_linkorder with ctx2; auto.
 * constructor. apply match_globdef_linkorder with ctx1; auto.
 * exploit Q; eauto. intros (X & Y & gd & Z).
-  exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto. 
-  intros (tg & TL & MG). rewrite Z, TL. constructor; auto. 
+  exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto.
+  intros (tg & TL & MG). rewrite Z, TL. constructor; auto.
 + rewrite R; simpl; auto.
 + rewrite R; simpl. congruence.
 Qed.
@@ -674,7 +674,7 @@ Remark link_transf_partial_fundef:
   link f1 f2 = Some f ->
   transf_partial_fundef tr1 f1 = OK tf1 ->
   transf_partial_fundef tr2 f2 = OK tf2 ->
-  exists tf, 
+  exists tf,
       link tf1 tf2 = Some tf
   /\ (transf_partial_fundef tr1 f = OK tf \/ transf_partial_fundef tr2 f = OK tf).
 Proof.
@@ -683,7 +683,7 @@ Local Transparent Linker_fundef.
 - discriminate.
 - destruct ef2; inv H. exists (Internal x); split; auto. left; simpl; rewrite EQ; auto.
 - destruct ef1; inv H. exists (Internal x); split; auto. right; simpl; rewrite EQ; auto.
-- destruct (external_function_eq ef1 ef2); inv H. exists (External ef2); split; auto. simpl. rewrite dec_eq_true; auto. 
+- destruct (external_function_eq ef1 ef2); inv H. exists (External ef2); split; auto. simpl. rewrite dec_eq_true; auto.
 Qed.
 
 Instance TransfPartialContextualLink
@@ -697,8 +697,8 @@ Instance TransfPartialContextualLink
 Proof.
   red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
   eapply link_match_program; eauto.
-- intros. eapply link_transf_partial_fundef; eauto. 
-- intros; subst. exists v; auto. 
+- intros. eapply link_transf_partial_fundef; eauto.
+- intros; subst. exists v; auto.
 Qed.
 
 Instance TransfPartialLink
@@ -711,8 +711,8 @@ Instance TransfPartialLink
 Proof.
   red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
   eapply link_match_program; eauto.
-- intros. eapply link_transf_partial_fundef; eauto. 
-- intros; subst. exists v; auto. 
+- intros. eapply link_transf_partial_fundef; eauto.
+- intros; subst. exists v; auto.
 Qed.
 
 Instance TransfTotallContextualLink
@@ -726,12 +726,12 @@ Instance TransfTotallContextualLink
 Proof.
   red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
   eapply link_match_program; eauto.
-- intros. subst. destruct f1, f2; simpl in *. 
+- intros. subst. destruct f1, f2; simpl in *.
 + discriminate.
-+ destruct e; inv H2. econstructor; eauto. 
-+ destruct e; inv H2. econstructor; eauto. 
-+ destruct (external_function_eq e e0); inv H2. econstructor; eauto. 
-- intros; subst. exists v; auto. 
++ destruct e; inv H2. econstructor; eauto.
++ destruct e; inv H2. econstructor; eauto.
++ destruct (external_function_eq e e0); inv H2. econstructor; eauto.
+- intros; subst. exists v; auto.
 Qed.
 
 Instance TransfTotalLink
@@ -744,12 +744,12 @@ Instance TransfTotalLink
 Proof.
   red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
   eapply link_match_program; eauto.
-- intros. subst. destruct f1, f2; simpl in *. 
+- intros. subst. destruct f1, f2; simpl in *.
 + discriminate.
-+ destruct e; inv H2. econstructor; eauto. 
-+ destruct e; inv H2. econstructor; eauto. 
-+ destruct (external_function_eq e e0); inv H2. econstructor; eauto. 
-- intros; subst. exists v; auto. 
++ destruct e; inv H2. econstructor; eauto.
++ destruct e; inv H2. econstructor; eauto.
++ destruct (external_function_eq e e0); inv H2. econstructor; eauto.
+- intros; subst. exists v; auto.
 Qed.
 
 (** * Linking a set of compilation units *)
@@ -794,7 +794,7 @@ Theorem link_list_match:
   exists b, link_list bl = Some b /\ prog_match a b.
 Proof.
   induction 1; simpl; intros a' L.
-- inv L. exists b; auto. 
+- inv L. exists b; auto.
 - destruct (link_list l) as [a1|] eqn:LL; try discriminate.
   exploit IHnlist_forall2; eauto. intros (b' & P & Q).
   red in TL. exploit TL; eauto. intros (b'' & U & V).
@@ -829,7 +829,7 @@ Program Definition pass_identity (l: Language): Pass l l :=
   {| pass_match := fun p1 p2 => p1 = p2;
      pass_match_link := _ |}.
 Next Obligation.
-  red; intros. subst. exists p; auto. 
+  red; intros. subst. exists p; auto.
 Defined.
 
 Program Definition pass_compose {l1 l2 l3: Language} (pass: Pass l1 l2) (pass': Pass l2 l3) : Pass l1 l3 :=
@@ -875,7 +875,7 @@ Lemma nlist_forall2_compose_inv:
   exists lb: nlist B, nlist_forall2 R1 la lb /\ nlist_forall2 R2 lb lc.
 Proof.
   induction 1.
-- rename b into c. destruct H as (b & P & Q). 
+- rename b into c. destruct H as (b & P & Q).
   exists (nbase b); split; constructor; auto.
 - rename b into c. destruct H as (b & P & Q). destruct IHnlist_forall2 as (lb & U & V).
   exists (ncons b lb); split; constructor; auto.
@@ -898,8 +898,8 @@ Proof.
 - apply nlist_forall2_compose_inv in F2. destruct F2 as (interm_units & P & Q).
   edestruct (@link_list_match _ _ (lang_link l1) (lang_link l2) (pass_match p))
   as (interm_prog & U & V).
-  apply pass_match_link. eauto. eauto.  
+  apply pass_match_link. eauto. eauto.
   exploit IHpasses; eauto. intros (tgt_prog & X & Y).
-  exists tgt_prog; split; auto. exists interm_prog; auto. 
+  exists tgt_prog; split; auto. exists interm_prog; auto.
 Qed.
 
diff --git a/common/Memdata.v b/common/Memdata.v
index 87547e1e..0aed4644 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -1062,7 +1062,7 @@ Lemma encode_val_int64:
      encode_val Mint32 (if Archi.big_endian then Val.hiword v else Val.loword v)
   ++ encode_val Mint32 (if Archi.big_endian then Val.loword v else Val.hiword v).
 Proof.
-  intros. unfold encode_val. rewrite H. 
+  intros. unfold encode_val. rewrite H.
   destruct v; destruct Archi.big_endian eqn:BI; try reflexivity;
   unfold Val.loword, Val.hiword, encode_val.
   unfold inj_bytes. rewrite <- map_app. f_equal.
diff --git a/common/Memory.v b/common/Memory.v
index 764fdc26..8bb69c02 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -912,7 +912,7 @@ Proof.
   rewrite Ptrofs.add_unsigned.
   replace (Ptrofs.unsigned (Ptrofs.of_int (Int.repr 4))) with (Int.unsigned (Int.repr 4))
     by (symmetry; apply Ptrofs.agree32_of_int; auto).
-  change (Int.unsigned (Int.repr 4)) with 4. 
+  change (Int.unsigned (Int.repr 4)) with 4.
   apply Ptrofs.unsigned_repr.
   exploit (Zdivide_interval (Ptrofs.unsigned i) Ptrofs.modulus 8).
   omega. apply Ptrofs.unsigned_range. auto.
@@ -934,7 +934,7 @@ Proof.
   exploit load_int64_split; eauto. intros (v1 & v2 & L1 & L2 & EQ).
   unfold Val.add; rewrite H0.
   assert (NV: Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4).
-  { apply addressing_int64_split; auto. 
+  { apply addressing_int64_split; auto.
     exploit load_valid_access. eexact H2. intros [P Q]. auto. }
   exists v1, v2.
 Opaque Ptrofs.repr.
@@ -1519,7 +1519,7 @@ Qed.
 Theorem loadbytes_storebytes_same:
   loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes.
 Proof.
-  intros. assert (STORE2:=STORE). unfold storebytes in STORE2. unfold loadbytes. 
+  intros. assert (STORE2:=STORE). unfold storebytes in STORE2. unfold loadbytes.
   destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
   try discriminate.
   rewrite pred_dec_true.
@@ -1829,7 +1829,7 @@ Proof.
   intros. exploit load_result; eauto. intro. rewrite H0.
   injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1.
   rewrite PMap.gss. destruct (size_chunk_nat_pos chunk) as [n E]. rewrite E. simpl.
-  rewrite ZMap.gi. apply decode_val_undef. 
+  rewrite ZMap.gi. apply decode_val_undef.
 Qed.
 
 Theorem load_alloc_same':
@@ -2930,7 +2930,7 @@ Proof.
   rewrite (nextblock_store _ _ _ _ _ _ H0). auto.
   eapply store_outside_inj; eauto.
   unfold inject_id; intros. inv H2. eapply H1; eauto. omega.
-  intros. eauto using perm_store_2. 
+  intros. eauto using perm_store_2.
 Qed.
 
 Theorem storev_extends:
@@ -2982,7 +2982,7 @@ Proof.
   rewrite (nextblock_storebytes _ _ _ _ _ H0). auto.
   eapply storebytes_outside_inj; eauto.
   unfold inject_id; intros. inv H2. eapply H1; eauto. omega.
-  intros. eauto using perm_storebytes_2. 
+  intros. eauto using perm_storebytes_2.
 Qed.
 
 Theorem alloc_extends:
@@ -3017,7 +3017,7 @@ Proof.
   intros. eapply perm_alloc_inv in H; eauto.
   generalize (perm_alloc_inv _ _ _ _ _ H0 b0 ofs Max Nonempty); intros PERM.
   destruct (eq_block b0 b).
-  subst b0. 
+  subst b0.
   assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by omega.
   destruct EITHER.
   left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto.
@@ -3034,7 +3034,7 @@ Proof.
   intros. inv H. constructor.
   rewrite (nextblock_free _ _ _ _ _ H0). auto.
   eapply free_left_inj; eauto.
-  intros. exploit mext_perm_inv0; eauto. intros [A|A]. 
+  intros. exploit mext_perm_inv0; eauto. intros [A|A].
   eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto.
   subst b0. right; eapply perm_free_2; eauto.
   intuition eauto using perm_free_3.
@@ -3051,7 +3051,7 @@ Proof.
   rewrite (nextblock_free _ _ _ _ _ H0). auto.
   eapply free_right_inj; eauto.
   unfold inject_id; intros. inv H. eapply H1; eauto. omega.
-  intros. eauto using perm_free_3. 
+  intros. eauto using perm_free_3.
 Qed.
 
 Theorem free_parallel_extends:
@@ -3498,7 +3498,7 @@ Proof.
   intros. eapply mi_representable; try eassumption.
   destruct H4; eauto with mem.
 (* perm inv *)
-  intros. exploit mi_perm_inv0; eauto using perm_store_2. 
+  intros. exploit mi_perm_inv0; eauto using perm_store_2.
   intuition eauto using perm_store_1, perm_store_2.
 Qed.
 
@@ -3523,7 +3523,7 @@ Proof.
   intros. eapply mi_representable; try eassumption.
   destruct H3; eauto with mem.
 (* perm inv *)
-  intros. exploit mi_perm_inv0; eauto using perm_store_2. 
+  intros. exploit mi_perm_inv0; eauto using perm_store_2.
   intuition eauto using perm_store_1, perm_store_2.
 Qed.
 
@@ -3594,7 +3594,7 @@ Proof.
   intros. eapply mi_representable0; eauto.
   destruct H4; eauto using perm_storebytes_2.
 (* perm inv *)
-  intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. 
+  intros. exploit mi_perm_inv0; eauto using perm_storebytes_2.
   intuition eauto using perm_storebytes_1, perm_storebytes_2.
 Qed.
 
@@ -3668,7 +3668,7 @@ Proof.
   intros. eapply mi_representable0; eauto.
   destruct H3; eauto using perm_storebytes_2.
 (* perm inv *)
-  intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. 
+  intros. exploit mi_perm_inv0; eauto using perm_storebytes_2.
   intuition eauto using perm_storebytes_1, perm_storebytes_2.
 Qed.
 
@@ -3694,7 +3694,7 @@ Proof.
   auto.
 (* perm inv *)
   intros. eapply perm_alloc_inv in H2; eauto. destruct (eq_block b0 b2).
-  subst b0. eelim fresh_block_alloc; eauto. 
+  subst b0. eelim fresh_block_alloc; eauto.
   eapply mi_perm_inv0; eauto.
 Qed.
 
@@ -3741,7 +3741,7 @@ Proof.
   destruct H4; eauto using perm_alloc_4.
 (* perm inv *)
   intros. unfold f' in H3; destruct (eq_block b0 b1); try discriminate.
-  exploit mi_perm_inv0; eauto. 
+  exploit mi_perm_inv0; eauto.
   intuition eauto using perm_alloc_1, perm_alloc_4.
 (* incr *)
   split. auto.
@@ -3892,7 +3892,7 @@ Proof.
 (* perm inv *)
   intros. exploit mi_perm_inv0; eauto. intuition eauto using perm_free_3.
   eapply perm_free_inv in H4; eauto. destruct H4 as [[A B] | A]; auto.
-  subst b1. right; eapply perm_free_2; eauto. 
+  subst b1. right; eapply perm_free_2; eauto.
 Qed.
 
 Lemma free_list_left_inject:
@@ -4080,7 +4080,7 @@ Proof.
   destruct H0; eauto using perm_inj.
   rewrite H. omega.
 (* perm inv *)
-  intros. 
+  intros.
   destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate.
   destruct (f' b') as [[b'' delta''] |] eqn:?; try discriminate.
   inversion H; clear H; subst b'' delta.
@@ -4163,7 +4163,7 @@ Proof.
   eapply mem_inj_compose; eauto.
   apply extensionality; intros. unfold compose_meminj, inject_id. auto.
   (* perm inv *)
-  exploit mext_perm_inv1; eauto. intros [A|A]. 
+  exploit mext_perm_inv1; eauto. intros [A|A].
   eapply mext_perm_inv0; eauto.
   right; red; intros; elim A. eapply perm_extends; eauto.
 Qed.
@@ -4305,7 +4305,7 @@ Lemma perm_unchanged_on:
   unchanged_on m m' -> P b ofs ->
   perm m b ofs k p -> perm m' b ofs k p.
 Proof.
-  intros. destruct H. apply unchanged_on_perm0; auto. eapply perm_valid_block; eauto. 
+  intros. destruct H. apply unchanged_on_perm0; auto. eapply perm_valid_block; eauto.
 Qed.
 
 Lemma perm_unchanged_on_2:
@@ -4324,7 +4324,7 @@ Proof.
 - intros. transitivity (perm m2 b ofs k p); apply unchanged_on_perm; auto.
   eapply valid_block_unchanged_on; eauto.
 - intros. transitivity (ZMap.get ofs (mem_contents m2)#b); apply unchanged_on_contents; auto.
-  eapply perm_unchanged_on; eauto. 
+  eapply perm_unchanged_on; eauto.
 Qed.
 
 Lemma loadbytes_unchanged_on_1:
@@ -4462,13 +4462,13 @@ Proof.
 - rewrite (nextblock_drop _ _ _ _ _ _ H). apply Ple_refl.
 - split; intros. eapply perm_drop_3; eauto.
   destruct (eq_block b0 b); auto.
-  subst b0. 
+  subst b0.
   assert (~ (lo <= ofs < hi)). { red; intros; eelim H0; eauto. }
   right; omega.
-  eapply perm_drop_4; eauto. 
-- unfold drop_perm in H. 
+  eapply perm_drop_4; eauto.
+- unfold drop_perm in H.
   destruct (range_perm_dec m b lo hi Cur Freeable); inv H; simpl. auto.
-Qed. 
+Qed.
 
 End UNCHANGED_ON.
 
@@ -4480,9 +4480,9 @@ Lemma unchanged_on_implies:
 Proof.
   intros. destruct H. constructor; intros.
 - auto.
-- apply unchanged_on_perm0; auto. 
-- apply unchanged_on_contents0; auto. 
-  apply H0; auto. eapply perm_valid_block; eauto. 
+- apply unchanged_on_perm0; auto.
+- apply unchanged_on_contents0; auto.
+  apply H0; auto. eapply perm_valid_block; eauto.
 Qed.
 
 End Mem.
diff --git a/common/Separation.v b/common/Separation.v
index c0a3c9cf..c27148aa 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -18,7 +18,7 @@
 (** This library defines a number of useful logical assertions about
   CompCert memory states, such as "block [b] at offset [ofs] contains
   value [v]".  Assertions can be grouped using a separating conjunction
-  operator in the style of separation logic.  
+  operator in the style of separation logic.
 
   Currently, this library is used only in module [Stackingproof]
   to reason about the shapes of stack frames generated during the
@@ -84,7 +84,7 @@ Qed.
 
 Remark massert_eqv_trans: forall p q r, massert_eqv p q -> massert_eqv q r -> massert_eqv p r.
 Proof.
-  unfold massert_eqv, massert_imp; intros. firstorder auto. 
+  unfold massert_eqv, massert_imp; intros. firstorder auto.
 Qed.
 
 (** Record [massert_eqv] and [massert_imp] as relations so that they can be used by rewriting tactics. *)
@@ -139,7 +139,7 @@ Add Morphism sepconj
 Proof.
   intros P1 P2 [A B] Q1 Q2 [C D].
   red; simpl; split; intros.
-- intuition auto. red; intros. apply (H2 b ofs); auto. 
+- intuition auto. red; intros. apply (H2 b ofs); auto.
 - intuition auto.
 Qed.
 
@@ -147,7 +147,7 @@ Add Morphism sepconj
   with signature massert_eqv ==> massert_eqv ==> massert_eqv
   as sepconj_morph_2.
 Proof.
-  intros. destruct H, H0. split; apply sepconj_morph_1; auto. 
+  intros. destruct H, H0. split; apply sepconj_morph_1; auto.
 Qed.
 
 Infix "**" := sepconj (at level 60, right associativity) : sep_scope.
@@ -155,7 +155,7 @@ Infix "**" := sepconj (at level 60, right associativity) : sep_scope.
 Local Open Scope sep_scope.
 
 Lemma sep_imp:
-  forall P P' Q Q' m, 
+  forall P P' Q Q' m,
   m |= P ** Q -> massert_imp P P' -> massert_imp Q Q' -> m |= P' ** Q'.
 Proof.
   intros. rewrite <- H0, <- H1; auto.
@@ -249,7 +249,7 @@ Lemma sep_drop2:
   forall P Q R m, m |= P ** Q ** R -> m |= P ** R.
 Proof.
   intros. rewrite sep_swap in H. eapply sep_drop; eauto.
-Qed. 
+Qed.
 
 Lemma sep_proj1:
   forall Q P m, m |= P ** Q -> m |= P.
@@ -263,25 +263,25 @@ Proof sep_drop.
 
 Definition sep_pick1 := sep_proj1.
 
-Lemma sep_pick2: 
+Lemma sep_pick2:
   forall P Q R m, m |= P ** Q ** R -> m |= Q.
 Proof.
   intros. eapply sep_proj1; eapply sep_proj2; eauto.
 Qed.
 
-Lemma sep_pick3: 
+Lemma sep_pick3:
   forall P Q R S m, m |= P ** Q ** R ** S -> m |= R.
 Proof.
   intros. eapply sep_pick2; eapply sep_proj2; eauto.
 Qed.
 
-Lemma sep_pick4: 
+Lemma sep_pick4:
   forall P Q R S T m, m |= P ** Q ** R ** S ** T -> m |= S.
 Proof.
   intros. eapply sep_pick3; eapply sep_proj2; eauto.
 Qed.
 
-Lemma sep_pick5: 
+Lemma sep_pick5:
   forall P Q R S T U m, m |= P ** Q ** R ** S ** T ** U -> m |= T.
 Proof.
   intros. eapply sep_pick4; eapply sep_proj2; eauto.
@@ -337,7 +337,7 @@ Lemma alloc_rule:
   m |= P ->
   m' |= range b lo hi ** P.
 Proof.
-  intros; simpl. split; [|split]. 
+  intros; simpl. split; [|split].
 - split; auto. split; auto. intros.
   apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.perm_alloc_2; eauto.
@@ -352,7 +352,7 @@ Lemma range_split:
   m |= range b lo hi ** P ->
   m |= range b lo mid ** range b mid hi ** P.
 Proof.
-  intros. rewrite <- sep_assoc. eapply sep_imp; eauto. 
+  intros. rewrite <- sep_assoc. eapply sep_imp; eauto.
   split; simpl; intros.
 - intuition auto.
 + omega.
@@ -425,8 +425,8 @@ Next Obligation.
 - exists v. split; auto. eapply Mem.load_unchanged_on; eauto. simpl; auto.
 Qed.
 Next Obligation.
-  eauto with mem. 
-Qed. 
+  eauto with mem.
+Qed.
 
 Lemma contains_no_overflow:
   forall spec m chunk b ofs,
@@ -466,10 +466,10 @@ Proof.
   destruct (Mem.valid_access_store _ _ _ _ v H) as [m' STORE].
   exists m'; split; auto. simpl. intuition auto.
 - eapply Mem.store_valid_access_1; eauto.
-- exists (Val.load_result chunk v); split; auto. eapply Mem.load_store_same; eauto. 
-- apply (m_invar P) with m; auto. 
-  eapply Mem.store_unchanged_on; eauto. 
-  intros; red; intros. apply (C b i); simpl; auto. 
+- exists (Val.load_result chunk v); split; auto. eapply Mem.load_store_same; eauto.
+- apply (m_invar P) with m; auto.
+  eapply Mem.store_unchanged_on; eauto.
+  intros; red; intros. apply (C b i); simpl; auto.
 Qed.
 
 Lemma storev_rule:
@@ -523,7 +523,7 @@ Lemma store_rule':
   exists m',
   Mem.store chunk m b ofs v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P.
 Proof.
-  intros. eapply store_rule; eauto. 
+  intros. eapply store_rule; eauto.
 Qed.
 
 Lemma storev_rule':
@@ -542,7 +542,7 @@ Program Definition mconj (P Q: massert) : massert := {|
   m_footprint := fun b ofs => m_footprint P b ofs \/ m_footprint Q b ofs
 |}.
 Next Obligation.
-  split. 
+  split.
   apply (m_invar P) with m; auto. eapply Mem.unchanged_on_implies; eauto. simpl; auto.
   apply (m_invar Q) with m; auto. eapply Mem.unchanged_on_implies; eauto. simpl; auto.
 Qed.
@@ -586,7 +586,7 @@ Lemma frame_mconj:
 Proof.
   intros. destruct H as (A & B & C); simpl in A.
   destruct H0 as (D & E & F).
-  simpl. intuition auto. 
+  simpl. intuition auto.
   red; simpl; intros. destruct H2. eapply F; eauto. eapply C; simpl; eauto.
 Qed.
 
@@ -602,7 +602,7 @@ Add Morphism mconj
   with signature massert_eqv ==> massert_eqv ==> massert_eqv
   as mconj_morph_2.
 Proof.
-  intros. destruct H, H0. split; apply mconj_morph_1; auto. 
+  intros. destruct H, H0. split; apply mconj_morph_1; auto.
 Qed.
 
 (** The image of a memory injection *)
@@ -615,8 +615,8 @@ Next Obligation.
   set (img := fun b' ofs => exists b delta, j b = Some(b', delta) /\ Mem.perm m0 b (ofs - delta) Max Nonempty) in *.
   assert (IMG: forall b1 b2 delta ofs k p,
            j b1 = Some (b2, delta) -> Mem.perm m0 b1 ofs k p -> img b2 (ofs + delta)).
-  { intros. red. exists b1, delta; split; auto. 
-    replace (ofs + delta - delta) with ofs by omega. 
+  { intros. red. exists b1, delta; split; auto.
+    replace (ofs + delta - delta) with ofs by omega.
     eauto with mem. }
   destruct H. constructor.
 - destruct mi_inj. constructor; intros.
@@ -624,11 +624,11 @@ Next Obligation.
 + eauto.
 + rewrite (Mem.unchanged_on_contents _ _ _ H0); eauto.
 - assumption.
-- intros. eapply Mem.valid_block_unchanged_on; eauto. 
+- intros. eapply Mem.valid_block_unchanged_on; eauto.
 - assumption.
 - assumption.
 - intros. destruct (Mem.perm_dec m0 b1 ofs Max Nonempty); auto.
-  eapply mi_perm_inv; eauto. 
+  eapply mi_perm_inv; eauto.
   eapply Mem.perm_unchanged_on_2; eauto.
 Qed.
 Next Obligation.
@@ -666,8 +666,8 @@ Proof.
 - apply (m_invar P) with m2; auto.
   eapply Mem.store_unchanged_on; eauto.
   intros; red; intros. eelim C; eauto. simpl.
-  exists b1, delta; split; auto. destruct VALID as [V1 V2]. 
-  apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. 
+  exists b1, delta; split; auto. destruct VALID as [V1 V2].
+  apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
   apply V1. omega.
 - red; simpl; intros. destruct H1 as (b0 & delta0 & U & V).
   eelim C; eauto. simpl. exists b0, delta0; eauto with mem.
@@ -695,41 +695,41 @@ Proof.
   assert (FRESH2: ~Mem.valid_block m2 b2) by (eapply Mem.fresh_block_alloc; eauto).
   destruct SEP as (INJ & SP & DISJ). simpl in INJ.
   exploit Mem.alloc_left_mapped_inject.
-- eapply Mem.alloc_right_inject; eauto. 
+- eapply Mem.alloc_right_inject; eauto.
 - eexact ALLOC1.
 - instantiate (1 := b2). eauto with mem.
 - instantiate (1 := delta). xomega.
 - intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). omega.
-- intros. apply Mem.perm_implies with Freeable; auto with mem. 
+- intros. apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.perm_alloc_2; eauto. xomega.
-- red; intros. apply Zdivides_trans with 8; auto. 
+- red; intros. apply Zdivides_trans with 8; auto.
   exists (8 / align_chunk chunk). destruct chunk; reflexivity.
-- intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. 
+- intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto.
 - intros (j' & INJ' & J1 & J2 & J3).
   exists j'; split; auto.
   rewrite <- ! sep_assoc.
   split; [|split].
 + simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; omega).
 * apply Mem.perm_implies with Freeable; auto with mem.
-  eapply Mem.perm_alloc_2; eauto. omega. 
+  eapply Mem.perm_alloc_2; eauto. omega.
 * apply Mem.perm_implies with Freeable; auto with mem.
-  eapply Mem.perm_alloc_2; eauto. omega. 
+  eapply Mem.perm_alloc_2; eauto. omega.
 * red; simpl; intros. destruct H1, H2. omega.
 * red; simpl; intros.
   assert (b = b2) by tauto. subst b.
   assert (0 <= ofs < lo \/ hi <= ofs < sz2) by tauto. clear H1.
   destruct H2 as (b0 & delta0 & D & E).
-  eapply Mem.perm_alloc_inv in E; eauto. 
+  eapply Mem.perm_alloc_inv in E; eauto.
   destruct (eq_block b0 b1).
   subst b0. rewrite J2 in D. inversion D; clear D; subst delta0. xomega.
-  rewrite J3 in D by auto. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. 
-+ apply (m_invar P) with m2; auto. eapply Mem.alloc_unchanged_on; eauto. 
+  rewrite J3 in D by auto. elim FRESH2. eapply Mem.valid_block_inject_2; eauto.
++ apply (m_invar P) with m2; auto. eapply Mem.alloc_unchanged_on; eauto.
 + red; simpl; intros.
   assert (VALID: Mem.valid_block m2 b) by (eapply (m_valid P); eauto).
   destruct H as [A | (b0 & delta0 & A & B)].
 * assert (b = b2) by tauto. subst b. contradiction.
-* eelim DISJ; eauto. simpl. 
-  eapply Mem.perm_alloc_inv in B; eauto. 
+* eelim DISJ; eauto. simpl.
+  eapply Mem.perm_alloc_inv in B; eauto.
   destruct (eq_block b0 b1).
   subst b0. rewrite J2 in A. inversion A; clear A; subst b delta0. contradiction.
   rewrite J3 in A by auto. exists b0, delta0; auto.
@@ -745,19 +745,19 @@ Lemma free_parallel_rule:
      Mem.free m2 b2 0 sz2 = Some m2'
   /\ m2' |= minjection j m1' ** P.
 Proof.
-  intros. rewrite <- ! sep_assoc in H. 
+  intros. rewrite <- ! sep_assoc in H.
   destruct H as (A & B & C).
   destruct A as (D & E & F).
   destruct D as (J & K & L).
   destruct J as (_ & _ & J). destruct K as (_ & _ & K).
   simpl in E.
   assert (PERM: Mem.range_perm m2 b2 0 sz2 Cur Freeable).
-  { red; intros. 
+  { red; intros.
     destruct (zlt ofs lo). apply J; omega.
     destruct (zle hi ofs). apply K; omega.
     replace ofs with ((ofs - delta) + delta) by omega.
-    eapply Mem.perm_inject; eauto. 
-    eapply Mem.free_range_perm; eauto. xomega. 
+    eapply Mem.perm_inject; eauto.
+    eapply Mem.free_range_perm; eauto. xomega.
   }
   destruct (Mem.range_perm_free _ _ _ _ PERM) as [m2' FREE].
   exists m2'; split; auto. split; [|split].
@@ -765,33 +765,33 @@ Proof.
   intros. apply (F b2 (ofs + delta0)).
 + simpl.
   destruct (zlt (ofs + delta0) lo). intuition auto.
-  destruct (zle hi (ofs + delta0)). intuition auto. 
+  destruct (zle hi (ofs + delta0)). intuition auto.
   destruct (eq_block b0 b1).
 * subst b0. rewrite H1 in H; inversion H; clear H; subst delta0.
   eelim (Mem.perm_free_2 m1); eauto. xomega.
-* exploit Mem.mi_no_overlap; eauto. 
-  apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. 
+* exploit Mem.mi_no_overlap; eauto.
+  apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem.
   eapply Mem.perm_free_3; eauto.
-  apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. 
-  eapply (Mem.free_range_perm m1); eauto. 
-  instantiate (1 := ofs + delta0 - delta). xomega. 
-  intros [X|X]. congruence. omega. 
-+ simpl. exists b0, delta0; split; auto. 
+  apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
+  eapply (Mem.free_range_perm m1); eauto.
+  instantiate (1 := ofs + delta0 - delta). xomega.
+  intros [X|X]. congruence. omega.
++ simpl. exists b0, delta0; split; auto.
   replace (ofs + delta0 - delta0) with ofs by omega.
-  apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. 
+  apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem.
   eapply Mem.perm_free_3; eauto.
-- apply (m_invar P) with m2; auto. 
-  eapply Mem.free_unchanged_on; eauto. 
-  intros; red; intros. eelim C; eauto. simpl. 
+- apply (m_invar P) with m2; auto.
+  eapply Mem.free_unchanged_on; eauto.
+  intros; red; intros. eelim C; eauto. simpl.
   destruct (zlt i lo). intuition auto.
   destruct (zle hi i). intuition auto.
-  right; exists b1, delta; split; auto. 
+  right; exists b1, delta; split; auto.
   apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-  eapply Mem.free_range_perm; eauto. xomega. 
-- red; simpl; intros. eelim C; eauto. 
-  simpl. right. destruct H as (b0 & delta0 & U & V). 
-  exists b0, delta0; split; auto. 
-  eapply Mem.perm_free_3; eauto. 
+  eapply Mem.free_range_perm; eauto. xomega.
+- red; simpl; intros. eelim C; eauto.
+  simpl. right. destruct H as (b0 & delta0 & U & V).
+  exists b0, delta0; split; auto.
+  eapply Mem.perm_free_3; eauto.
 Qed.
 
 (** Preservation of a global environment by a memory injection *)
@@ -836,7 +836,7 @@ Lemma globalenv_inject_incr:
 Proof.
   intros. destruct H1 as (A & B & C). destruct A as (bound & D & E).
   split; [|split]; auto.
-  exists bound; split; auto. 
+  exists bound; split; auto.
   inv E; constructor; intros.
 - eauto.
 - destruct (j b1) as [[b0 delta0]|] eqn:JB1.
@@ -860,7 +860,7 @@ Lemma external_call_parallel_rule:
   /\ inject_separated j j' m1 m2.
 Proof.
   intros until vargs2; intros CALL SEP ARGS.
-  destruct SEP as (A & B & C). simpl in A. 
+  destruct SEP as (A & B & C). simpl in A.
   exploit external_call_mem_inject; eauto.
   eapply globalenv_inject_preserves_globals. eapply sep_pick1; eauto.
   intros (j' & vres2 & m2' & CALL' & RES & INJ' & UNCH1 & UNCH2 & INCR & ISEP).
@@ -877,11 +877,11 @@ Proof.
   eelim C; eauto. simpl. exists b0, delta; auto.
 - red; intros. destruct H as (b0 & delta & J' & E).
   destruct (j b0) as [[b' delta'] | ] eqn:J.
-+ erewrite INCR in J' by eauto. inv J'. 
-  eelim C; eauto. simpl. exists b0, delta; split; auto. apply MAXPERMS; auto. 
++ erewrite INCR in J' by eauto. inv J'.
+  eelim C; eauto. simpl. exists b0, delta; split; auto. apply MAXPERMS; auto.
   eapply Mem.valid_block_inject_1; eauto.
 + exploit ISEP; eauto. intros (X & Y). elim Y. eapply m_valid; eauto.
-Qed.  
+Qed.
 
 Lemma alloc_parallel_rule_2:
   forall (F V: Type) (ge: Genv.t F V) m1 sz1 m1' b1 m2 sz2 m2' b2 P j lo hi delta,
@@ -898,19 +898,19 @@ Lemma alloc_parallel_rule_2:
   /\ inject_incr j j'
   /\ j' b1 = Some(b2, delta).
 Proof.
-  intros. 
+  intros.
   set (j1 := fun b => if eq_block b b1 then Some(b2, delta) else j b).
   assert (X: inject_incr j j1).
-  { unfold j1; red; intros. destruct (eq_block b b1); auto. 
-    subst b. eelim Mem.fresh_block_alloc. eexact H0. 
+  { unfold j1; red; intros. destruct (eq_block b b1); auto.
+    subst b. eelim Mem.fresh_block_alloc. eexact H0.
     eapply Mem.valid_block_inject_1. eauto. apply sep_proj1 in H. eexact H. }
   assert (Y: inject_separated j j1 m1 m2).
-  { unfold j1; red; intros. destruct (eq_block b0 b1). 
+  { unfold j1; red; intros. destruct (eq_block b0 b1).
   - inversion H9; clear H9; subst b3 delta0 b0. split; eapply Mem.fresh_block_alloc; eauto.
   - congruence. }
   rewrite sep_swap in H. eapply globalenv_inject_incr with (j' := j1) in H; eauto. rewrite sep_swap in H.
   clear X Y.
-  exploit alloc_parallel_rule; eauto. 
+  exploit alloc_parallel_rule; eauto.
   intros (j' & A & B & C & D).
   exists j'; split; auto.
   rewrite sep_swap4 in A. rewrite sep_swap4. apply globalenv_inject_incr with j1 m1; auto.
diff --git a/common/Smallstep.v b/common/Smallstep.v
index 9c91243a..c269013b 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -786,7 +786,7 @@ End SIMULATION_SEQUENCES.
 Lemma compose_forward_simulations:
   forall L1 L2 L3, forward_simulation L1 L2 -> forward_simulation L2 L3 -> forward_simulation L1 L3.
 Proof.
-  intros L1 L2 L3 S12 S23. 
+  intros L1 L2 L3 S12 S23.
   destruct S12 as [index order match_states props].
   destruct S23 as [index' order' match_states' props'].
 
@@ -1632,7 +1632,7 @@ Theorem factor_forward_simulation:
   forward_simulation L1 L2 -> single_events L2 ->
   forward_simulation (atomic L1) L2.
 Proof.
-  intros L1 L2 FS L2single. 
+  intros L1 L2 FS L2single.
   destruct FS as [index order match_states sim].
   apply Forward_simulation with order (ffs_match L1 L2 match_states); constructor.
 - (* wf *)
@@ -1727,7 +1727,7 @@ Theorem factor_backward_simulation:
   backward_simulation L1 L2 -> single_events L1 -> well_behaved_traces L2 ->
   backward_simulation L1 (atomic L2).
 Proof.
-  intros L1 L2 BS L1single L2wb. 
+  intros L1 L2 BS L1single L2wb.
   destruct BS as [index order match_states sim].
   apply Backward_simulation with order (fbs_match L1 L2 match_states); constructor.
 - (* wf *)
diff --git a/common/Values.v b/common/Values.v
index cfabb7a5..d086c69f 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -16,7 +16,6 @@
 (** This module defines the type of values that is used in the dynamic
   semantics of all our intermediate languages. *)
 
-Require Archi.
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
@@ -668,6 +667,12 @@ Definition modlu (v1 v2: val): option val :=
   | _, _ => None
   end.
 
+Definition addl_carry (v1 v2 cin: val): val :=
+  match v1, v2, cin with
+  | Vlong n1, Vlong n2, Vlong c => Vlong(Int64.add_carry n1 n2 c)
+  | _, _, _ => Vundef
+  end.
+
 Definition subl_overflow (v1 v2: val) : val :=
   match v1, v2 with
   | Vlong n1, Vlong n2 => Vint (Int.repr (Int64.unsigned (Int64.sub_overflow n1 n2 Int64.zero)))
@@ -734,6 +739,15 @@ Definition shrxl (v1 v2: val): option val :=
   | _, _ => None
   end.
 
+Definition shrl_carry (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vint n2 =>
+     if Int.ltu n2 Int64.iwordsize'
+     then Vlong(Int64.shr_carry' n1 n2)
+     else Vundef
+  | _, _ => Vundef
+  end.
+
 Definition roll (v1 v2: val): val :=
   match v1, v2 with
   | Vlong n1, Vint n2 => Vlong(Int64.rol n1 (Int64.repr (Int.unsigned n2)))
@@ -746,9 +760,9 @@ Definition rorl (v1 v2: val): val :=
   | _, _ => Vundef
   end.
 
-Definition rolml (v: val) (amount mask: int64): val :=
+Definition rolml (v: val) (amount: int) (mask: int64): val :=
   match v with
-  | Vlong n => Vlong(Int64.rolm n amount mask)
+  | Vlong n => Vlong(Int64.rolm n (Int64.repr (Int.unsigned amount)) mask)
   | _ => Vundef
   end.
 
@@ -1073,7 +1087,7 @@ Proof.
   symmetry. auto with ptrofs.
   symmetry. rewrite Int.add_commut. auto with ptrofs.
 - destruct (eq_block b b0); auto.
-  f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs. 
+  f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs.
 Qed.
 
 Theorem mul_commut: forall x y, mul x y = mul y x.
@@ -1133,6 +1147,28 @@ Proof.
   generalize (Int.eq_spec i0 Int.zero). rewrite Heqb; auto.
 Qed.
 
+Theorem modls_divls:
+  forall x y z,
+  modls x y = Some z -> exists v, divls x y = Some v /\ z = subl x (mull v y).
+Proof.
+  intros. destruct x; destruct y; simpl in *; try discriminate.
+  destruct (Int64.eq i0 Int64.zero
+        || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H.
+  exists (Vlong (Int64.divs i i0)); split; auto.
+  simpl. rewrite Int64.mods_divs. auto.
+Qed.
+
+Theorem modlu_divlu:
+  forall x y z,
+  modlu x y = Some z -> exists v, divlu x y = Some v /\ z = subl x (mull v y).
+Proof.
+  intros. destruct x; destruct y; simpl in *; try discriminate.
+  destruct (Int64.eq i0 Int64.zero) eqn:?; inv H.
+  exists (Vlong (Int64.divu i i0)); split; auto.
+  simpl. rewrite Int64.modu_divu. auto.
+  generalize (Int64.eq_spec i0 Int64.zero). rewrite Heqb; auto.
+Qed.
+
 Theorem divs_pow2:
   forall x n logn y,
   Int.is_power2 n = Some logn -> Int.ltu logn (Int.repr 31) = true ->
@@ -1282,7 +1318,7 @@ Proof.
   symmetry; apply zlt_true. change (Int.unsigned n < 32); omega.
   symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32.
   assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
-  rewrite Int.unsigned_repr. 
+  rewrite Int.unsigned_repr.
   change (Int.unsigned Int.iwordsize) with 32; omega.
   assert (32 < Int.max_unsigned) by reflexivity. omega.
 Qed.
@@ -1384,7 +1420,7 @@ Proof.
   symmetry. auto with ptrofs.
   symmetry. rewrite Int64.add_commut. auto with ptrofs.
 - destruct (eq_block b b0); auto.
-  simpl; f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs. 
+  simpl; f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs.
 - rewrite Int64.add_commut. rewrite Int64.sub_add_r. auto.
 Qed.
 
@@ -1462,7 +1498,7 @@ Proof.
          || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n Int64.mone); inv H3.
   simpl. rewrite H0. decEq. decEq.
   generalize (Int64.is_power2'_correct _ _ H); intro.
-  unfold Int64.shrx'. rewrite Int64.shl'_mul_two_p. rewrite <- H1. 
+  unfold Int64.shrx'. rewrite Int64.shl'_mul_two_p. rewrite <- H1.
   rewrite Int64.mul_commut. rewrite Int64.mul_one.
   rewrite Int64.repr_unsigned. auto.
 Qed.
@@ -1491,6 +1527,19 @@ Proof.
   simpl. decEq. symmetry. eapply Int64.modu_and; eauto.
 Qed.
 
+Theorem shrxl_carry:
+  forall x y z,
+  shrxl x y = Some z ->
+  addl (shrl x y) (shrl_carry x y) = z.
+Proof.
+  intros. destruct x; destruct y; simpl in H; inv H.
+  destruct (Int.ltu i0 (Int.repr 63)) eqn:?; inv H1.
+  exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63. intros.
+  assert (Int.ltu i0 Int64.iwordsize' = true).
+    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int64.iwordsize') with 64. omega.
+  simpl. rewrite H0. simpl. decEq. rewrite Int64.shrx'_carry; auto.
+Qed.
+
 Theorem shrxl_shrl_2:
   forall n x z,
   shrxl x (Vint n) = Some z ->
@@ -1511,7 +1560,7 @@ Proof.
   symmetry; apply zlt_true. change (Int.unsigned n < 64); omega.
   symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64.
   assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
-  rewrite Int.unsigned_repr. 
+  rewrite Int.unsigned_repr.
   change (Int.unsigned Int64.iwordsize') with 64; omega.
   assert (64 < Int.max_unsigned) by reflexivity. omega.
 Qed.
@@ -1603,7 +1652,7 @@ Theorem swap_cmpu_bool:
 Proof.
   assert (E: forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c).
   { destruct c; auto. }
-  intros; unfold cmpu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto.  
+  intros; unfold cmpu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto.
 - rewrite Int.swap_cmpu. auto.
 - rewrite Int.swap_cmpu. auto.
 - destruct (eq_block b b0); subst.
@@ -1630,7 +1679,7 @@ Theorem swap_cmplu_bool:
 Proof.
   assert (E: forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c).
   { destruct c; auto. }
-  intros; unfold cmplu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto.  
+  intros; unfold cmplu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto.
 - rewrite Int64.swap_cmpu. auto.
 - destruct (eq_block b b0); subst.
   rewrite dec_eq_true.
@@ -1937,7 +1986,7 @@ Qed.
 Lemma offset_ptr_assoc:
   forall v d1 d2, offset_ptr (offset_ptr v d1) d2 = offset_ptr v (Ptrofs.add d1 d2).
 Proof.
-  intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc. 
+  intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc.
 Qed.
 
 (** * Values and memory injections *)
@@ -1988,7 +2037,7 @@ Hint Resolve inject_list_nil inject_list_cons.
 Lemma inject_ptrofs:
   forall mi i, inject mi (Vptrofs i) (Vptrofs i).
 Proof.
-  unfold Vptrofs; intros. destruct Archi.ptr64; auto. 
+  unfold Vptrofs; intros. destruct Archi.ptr64; auto.
 Qed.
 
 Hint Resolve inject_ptrofs.
@@ -2002,7 +2051,7 @@ Lemma load_result_inject:
   inject f v1 v2 ->
   inject f (Val.load_result chunk v1) (Val.load_result chunk v2).
 Proof.
-  intros. inv H; destruct chunk; simpl; try constructor; destruct Archi.ptr64; econstructor; eauto. 
+  intros. inv H; destruct chunk; simpl; try constructor; destruct Archi.ptr64; econstructor; eauto.
 Qed.
 
 Remark add_inject:
@@ -2012,11 +2061,11 @@ Remark add_inject:
   inject f (Val.add v1 v2) (Val.add v1' v2').
 Proof.
   intros. unfold Val.add. destruct Archi.ptr64 eqn:SF.
-- inv H; inv H0; constructor. 
+- inv H; inv H0; constructor.
 - inv H; inv H0; simpl; auto.
-+ econstructor; eauto. 
++ econstructor; eauto.
   rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
-+ econstructor; eauto. 
++ econstructor; eauto.
   rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
 Qed.
 
@@ -2029,7 +2078,7 @@ Proof.
   intros. unfold Val.sub. destruct Archi.ptr64 eqn:SF.
 - inv H; inv H0; constructor.
 - inv H; inv H0; simpl; auto.
-+ econstructor; eauto. 
++ econstructor; eauto.
   rewrite Ptrofs.sub_add_l. auto.
 + destruct (eq_block b1 b0); auto.
   subst. rewrite H1 in H. inv H. rewrite dec_eq_true.
@@ -2044,11 +2093,11 @@ Remark addl_inject:
 Proof.
   intros. unfold Val.addl. destruct Archi.ptr64 eqn:SF.
 - inv H; inv H0; simpl; auto.
-+ econstructor; eauto. 
++ econstructor; eauto.
   rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
-+ econstructor; eauto. 
++ econstructor; eauto.
   rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
-- inv H; inv H0; constructor. 
+- inv H; inv H0; constructor.
 Qed.
 
 Remark subl_inject:
@@ -2059,7 +2108,7 @@ Remark subl_inject:
 Proof.
   intros. unfold Val.subl. destruct Archi.ptr64 eqn:SF.
 - inv H; inv H0; simpl; auto.
-+ econstructor; eauto. 
++ econstructor; eauto.
   rewrite Ptrofs.sub_add_l. auto.
 + destruct (eq_block b1 b0); auto.
   subst. rewrite H1 in H. inv H. rewrite dec_eq_true.
@@ -2126,7 +2175,7 @@ Lemma cmpu_bool_inject:
 Proof.
   Local Opaque Int.add Ptrofs.add.
   intros.
-  unfold cmpu_bool in *; destruct Archi.ptr64; 
+  unfold cmpu_bool in *; destruct Archi.ptr64;
   inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
 - fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1.
   fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))).