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.

15 files changed, 92 insertions, 90 deletions

diff --git a/x86/Asm.v b/x86/Asm.v
index 1c204b02..8b873e48 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -209,7 +209,7 @@ Inductive instruction: Type :=
   | Pcmpl_ri (r1: ireg) (n: int)
   | Pcmpq_ri (r1: ireg) (n: int64)
   | Ptestl_rr (r1 r2: ireg)
-  | Ptestq_rr (r1 r2: ireg) 
+  | Ptestq_rr (r1 r2: ireg)
   | Ptestl_ri (r1: ireg) (n: int)
   | Ptestq_ri (r1: ireg) (n: int64)
   | Pcmov (c: testcond) (rd: ireg) (r1: ireg)
@@ -792,7 +792,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pxorl_rr rd r1 =>
       Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd rs#r1))) m
   | Pxorq_rr rd r1 =>
-      Next (nextinstr_nf (rs#rd <- (Val.xorl rs#rd rs#r1))) m 
+      Next (nextinstr_nf (rs#rd <- (Val.xorl rs#rd rs#r1))) m
   | Pxorl_ri rd n =>
       Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd (Vint n)))) m
   | Pxorq_ri rd n =>
@@ -1145,7 +1145,7 @@ Proof.
   { intros. inv H; inv H0; congruence. }
   assert (B: forall p v1 v2,
              extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
-  { intros. inv H; inv H0. 
+  { intros. inv H; inv H0.
     eapply A; eauto.
     f_equal; eapply A; eauto. }
   assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 90dc0e69..8e69061e 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -29,7 +29,7 @@ let _1 = Integers.Int.one
 let _2 = coqint_of_camlint 2l
 let _4 = coqint_of_camlint 4l
 let _8 = coqint_of_camlint 8l
-  
+
 let _0z = Z.zero
 let _1z = Z.one
 let _2z = Z.of_sint 2
@@ -49,7 +49,7 @@ let _Plea (r, addr) =
 let align n a =
   if n >= 0 then (n + a - 1) land (-a) else n land (-a)
 
-let sp_adjustment_32 sz =  
+let sp_adjustment_32 sz =
   let sz = Z.to_int sz in
   (* Preserve proper alignment of the stack *)
   let sz = align sz (stack_alignment ()) in
@@ -72,7 +72,7 @@ let sp_adjustment_64 sz =
     (* The top 8 bytes have already been allocated by the "call" instruction. *)
     (sz - 8, -1)
   end
-  
+
 (* Built-ins.  They come in two flavors:
    - annotation statements: take their arguments in registers or stack
    locations; generate no code;
@@ -500,7 +500,7 @@ let expand_instruction instr =
        emit (Pleaq (RAX, addr1));
        emit (Pmovq_mr (addr2, RAX));
        current_function_stacksize := Int64.of_int fullsz
-     end else begin     
+     end else begin
        let sz = sp_adjustment_32 sz in
        (* Allocate frame *)
        let sz' = Z.of_uint sz in
@@ -512,7 +512,7 @@ let expand_instruction instr =
        emit (Pleal (RAX,addr1));
        emit (Pmovl_mr (addr2,RAX));
        PrintAsmaux.current_function_stacksize := Int32.of_int sz
-     end  
+     end
   | Pfreeframe(sz, ofs_ra, ofs_link) ->
      if Archi.ptr64 then begin
        let (sz, _) = sp_adjustment_64 sz in
diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v
index e56dc429..6caf4531 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -780,7 +780,7 @@ Opaque loadind.
   exploit functions_transl; eauto. intro FN.
   generalize (transf_function_no_overflow _ _ H5); intro NOOV.
   set (rs1 := rs0 #RAX <- Vundef #RDX <- Vundef).
-  exploit (find_label_goto_label f tf lbl rs1); eauto. 
+  exploit (find_label_goto_label f tf lbl rs1); eauto.
   intros [tc' [rs' [A [B C]]]].
   exploit ireg_val; eauto. rewrite H. intros LD; inv LD.
   left; econstructor; split.
@@ -789,7 +789,7 @@ Opaque loadind.
   simpl. rewrite <- H9.  unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
   econstructor; eauto.
 Transparent destroyed_by_jumptable.
-  apply agree_undef_regs with rs0; auto. 
+  apply agree_undef_regs with rs0; auto.
   simpl; intros. destruct H8. rewrite C by auto with asmgen. unfold rs1; Simplifs.
   congruence.
 
@@ -834,7 +834,7 @@ Transparent destroyed_by_jumptable.
   left; econstructor; split.
   apply plus_one. econstructor; eauto.
   simpl. rewrite Ptrofs.unsigned_zero. simpl. eauto.
-  simpl. rewrite C. simpl in F, P. 
+  simpl. rewrite C. simpl in F, P.
   replace (chunk_of_type Tptr) with Mptr in F, P by (unfold Tptr, Mptr; destruct Archi.ptr64; auto).
   rewrite (sp_val _ _ _ AG) in F. rewrite F.
   rewrite ATLR. rewrite P. eauto.
@@ -883,7 +883,7 @@ Proof.
   econstructor; eauto.
   constructor.
   apply Mem.extends_refl.
-  split. reflexivity. simpl. 
+  split. reflexivity. simpl.
   unfold Vnullptr; destruct Archi.ptr64; congruence.
   intros. rewrite Regmap.gi. auto.
   unfold Genv.symbol_address.
diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v
index 6191ea39..aade95d2 100644
--- a/x86/Asmgenproof1.v
+++ b/x86/Asmgenproof1.v
@@ -254,7 +254,7 @@ Proof.
   set (rs5 := nextinstr_nf (rs4#RAX <- v4)).
   assert (X: forall v1 v2,
              Val.addl v1 (Val.addl v2 (Vlong Int64.zero)) = Val.addl v1 v2).
-  { intros. unfold Val.addl; destruct Archi.ptr64 eqn:SF, v0; auto; destruct v5; auto. 
+  { intros. unfold Val.addl; destruct Archi.ptr64 eqn:SF, v0; auto; destruct v5; auto.
     rewrite Int64.add_zero; auto.
     rewrite Ptrofs.add_zero; auto.
     rewrite Int64.add_zero; auto.
diff --git a/x86/CombineOpproof.v b/x86/CombineOpproof.v
index f59e582b..a7024501 100644
--- a/x86/CombineOpproof.v
+++ b/x86/CombineOpproof.v
@@ -125,7 +125,7 @@ Theorem combine_addr_32_sound:
 Proof.
   intros. functional inversion H; subst.
   (* indexed - lea *)
-  UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. 
+  UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7.
   eapply eval_offset_addressing_total_32; eauto.
 Qed.
 
@@ -136,7 +136,7 @@ Theorem combine_addr_64_sound:
 Proof.
   intros. functional inversion H; subst.
   (* indexed - leal *)
-  UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. 
+  UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7.
   eapply eval_offset_addressing_total_64; eauto.
 Qed.
 
diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp
index 0bf143d2..759d7c16 100644
--- a/x86/ConstpropOp.vp
+++ b/x86/ConstpropOp.vp
@@ -46,7 +46,7 @@ Definition const_for_result (a: aval) : option operation :=
   one if some of its arguments are statically known.  These are again
   large pattern-matchings expressed in indirect style. *)
 
-Nondetfunction cond_strength_reduction 
+Nondetfunction cond_strength_reduction
               (cond: condition) (args: list reg) (vl: list aval) :=
   match cond, args, vl with
   | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
@@ -65,7 +65,7 @@ Nondetfunction cond_strength_reduction
       (Ccompluimm (swap_comparison c) n1, r2 :: nil)
   | Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil =>
       (Ccompluimm c n2, r1 :: nil)
-  | _, _, _ => 
+  | _, _, _ =>
       (cond, args)
   end.
 
@@ -350,7 +350,7 @@ Definition make_cast16signed (r: reg) (a: aval) :=
 Definition make_cast16unsigned (r: reg) (a: aval) :=
   if vincl a (Uns Ptop 16) then (Omove, r :: nil) else (Ocast16unsigned, r :: nil).
 
-Nondetfunction op_strength_reduction 
+Nondetfunction op_strength_reduction
               (op: operation) (args: list reg) (vl: list aval) :=
   match op, args, vl with
   | Ocast8signed, r1 :: nil, v1 :: nil => make_cast8signed r1 v1
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index 4f582f86..5eb46e34 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -85,7 +85,7 @@ Lemma eval_Olea_ptr:
   forall a el,
   eval_operation ge (Vptr sp Ptrofs.zero) (Olea_ptr a) el m = eval_addressing ge (Vptr sp Ptrofs.zero) a el.
 Proof.
-  unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto. 
+  unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto.
 Qed.
 
 Lemma const_for_result_correct:
@@ -112,12 +112,12 @@ Proof.
     exists (Genv.symbol_address ge id Ptrofs.zero); auto.
   * inv H2. exists (Genv.symbol_address ge id ofs); split.
     rewrite eval_Olea_ptr. apply eval_addressing_Aglobal.
-    auto.  
+    auto.
   + (* stack *)
     inv H2. exists (Vptr sp ofs); split.
-    rewrite eval_Olea_ptr. rewrite eval_addressing_Ainstack.  
+    rewrite eval_Olea_ptr. rewrite eval_addressing_Ainstack.
     simpl. rewrite Ptrofs.add_zero_l; auto.
-    auto.  
+    auto.
 Qed.
 
 Lemma cond_strength_reduction_correct:
@@ -152,8 +152,8 @@ Local Opaque Val.add.
   assert (B: forall x y z, Int.repr (Int.signed x * y + z) = Int.add (Int.mul x (Int.repr y)) (Int.repr z)).
   { intros; apply Int.eqm_samerepr; apply Int.eqm_add; auto with ints.
     unfold Int.mul; auto using Int.eqm_signed_unsigned with ints. }
-  intros until res; intros VL EA. 
-  unfold addr_strength_reduction_32_generic; destruct (addr_strength_reduction_32_generic_match addr args vl); 
+  intros until res; intros VL EA.
+  unfold addr_strength_reduction_32_generic; destruct (addr_strength_reduction_32_generic_match addr args vl);
   simpl in *; InvApproxRegs; SimplVM; try (inv EA).
 - econstructor; split; eauto. rewrite A, Val.add_assoc, Val.add_permut. auto.
 - econstructor; split; eauto. rewrite A, Val.add_assoc. auto.
@@ -178,19 +178,19 @@ Proof.
              Val.add (Genv.symbol_address ge symb ofs) (Vint (Int.repr n))).
   { intros. rewrite <- A. apply Genv.shift_symbol_address_32; auto. }
 Local Opaque Val.add.
-  destruct (addr_strength_reduction_32_match addr args vl); 
+  destruct (addr_strength_reduction_32_match addr args vl);
   simpl in *; InvApproxRegs; SimplVM; FuncInv; subst; rewrite ?SF.
 - econstructor; split; eauto. rewrite B. apply Val.add_lessdef; auto.
 - econstructor; split; eauto. rewrite Ptrofs.add_zero_l.
 Local Transparent Val.add.
   inv H0; auto. rewrite H2. simpl; rewrite SF, A. auto.
-- econstructor; split; eauto. 
-  unfold Ptrofs.add at 2. rewrite B. 
+- econstructor; split; eauto.
+  unfold Ptrofs.add at 2. rewrite B.
   fold (Ptrofs.add n1 (Ptrofs.of_int n2)).
   rewrite Genv.shift_symbol_address_32 by auto.
   rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
 - econstructor; split; eauto.
-  unfold Ptrofs.add at 2. rewrite B. 
+  unfold Ptrofs.add at 2. rewrite B.
   fold (Ptrofs.add n2 (Ptrofs.of_int n1)).
   rewrite Genv.shift_symbol_address_32 by auto.
   rewrite ! Val.add_assoc. rewrite Val.add_permut. apply Val.add_lessdef; auto.
@@ -203,7 +203,7 @@ Local Transparent Val.add.
   apply Val.lessdef_same; do 3 f_equal. auto with ptrofs.
 - econstructor; split; eauto. rewrite B. rewrite ! Val.add_assoc. rewrite (Val.add_commut (Vint (Int.repr ofs))).
   apply Val.add_lessdef; auto.
-- econstructor; split; eauto. rewrite B. rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc. 
+- econstructor; split; eauto. rewrite B. rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc.
   rewrite (Val.add_commut (Vint (Int.repr ofs))). apply Val.add_lessdef; auto.
 - econstructor; split; eauto. rewrite B. rewrite Genv.shift_symbol_address_32 by auto.
   rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
@@ -229,8 +229,8 @@ Local Opaque Val.addl.
   assert (B: forall x y z, Int64.repr (Int64.signed x * y + z) = Int64.add (Int64.mul x (Int64.repr y)) (Int64.repr z)).
   { intros; apply Int64.eqm_samerepr; apply Int64.eqm_add; auto with ints.
     unfold Int64.mul; auto using Int64.eqm_signed_unsigned with ints. }
-  intros until res; intros VL EA. 
-  unfold addr_strength_reduction_64_generic; destruct (addr_strength_reduction_64_generic_match addr args vl); 
+  intros until res; intros VL EA.
+  unfold addr_strength_reduction_64_generic; destruct (addr_strength_reduction_64_generic_match addr args vl);
   simpl in *; InvApproxRegs; SimplVM; try (inv EA).
 - econstructor; split; eauto. rewrite A, Val.addl_assoc, Val.addl_permut. auto.
 - econstructor; split; eauto. rewrite A, Val.addl_assoc. auto.
@@ -256,19 +256,19 @@ Proof.
              Val.addl (Genv.symbol_address ge symb ofs) (Vlong (Int64.repr n))).
   { intros. rewrite <- A. apply Genv.shift_symbol_address_64; auto. }
 Local Opaque Val.addl.
-  destruct (addr_strength_reduction_64_match addr args vl); 
+  destruct (addr_strength_reduction_64_match addr args vl);
   simpl in *; InvApproxRegs; SimplVM; FuncInv; subst; rewrite ?SF.
 - econstructor; split; eauto. rewrite B. apply Val.addl_lessdef; auto.
 - econstructor; split; eauto. rewrite Ptrofs.add_zero_l.
 Local Transparent Val.addl.
   inv H0; auto. rewrite H2. simpl; rewrite SF, A. auto.
-- econstructor; split; eauto. 
-  unfold Ptrofs.add at 2. rewrite B. 
+- econstructor; split; eauto.
+  unfold Ptrofs.add at 2. rewrite B.
   fold (Ptrofs.add n1 (Ptrofs.of_int64 n2)).
   rewrite Genv.shift_symbol_address_64 by auto.
   rewrite ! Val.addl_assoc. apply Val.addl_lessdef; auto.
 - econstructor; split; eauto.
-  unfold Ptrofs.add at 2. rewrite B. 
+  unfold Ptrofs.add at 2. rewrite B.
   fold (Ptrofs.add n2 (Ptrofs.of_int64 n1)).
   rewrite Genv.shift_symbol_address_64 by auto.
   rewrite ! Val.addl_assoc. rewrite Val.addl_permut. apply Val.addl_lessdef; auto.
@@ -350,8 +350,8 @@ Proof.
   intros. unfold make_addimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
   subst. exists (e#r); split; auto.
-  destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. 
-  exists (Val.add e#r (Vint n)); split; auto. simpl. rewrite Int.repr_signed; auto. 
+  destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto.
+  exists (Val.add e#r (Vint n)); split; auto. simpl. rewrite Int.repr_signed; auto.
 Qed.
 
 Lemma make_shlimm_correct:
@@ -514,7 +514,7 @@ Proof.
   predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
   subst. exists (e#r); split; auto.
   destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto.
-  exists (Val.addl e#r (Vlong n)); split; auto. simpl. rewrite Int64.repr_signed; auto. 
+  exists (Val.addl e#r (Vlong n)); split; auto. simpl. rewrite Int64.repr_signed; auto.
 Qed.
 
 Lemma make_shllimm_correct:
@@ -606,8 +606,8 @@ Proof.
   econstructor; split. simpl; eauto.
   rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2.
   simpl.
-  erewrite Int64.is_power2'_range by eauto.    
-  erewrite Int64.divu_pow2' by eauto.  auto. 
+  erewrite Int64.is_power2'_range by eauto.
+  erewrite Int64.divu_pow2' by eauto.  auto.
   exists v; auto.
 Qed.
 
@@ -621,7 +621,7 @@ Proof.
   intros; unfold make_modluimm.
   destruct (Int64.is_power2 n) eqn:?.
   exists v; split; auto. simpl. decEq.
-  rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. 
+  rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2.
   simpl. erewrite Int64.modu_and by eauto. auto.
   exists v; auto.
 Qed.
@@ -830,7 +830,7 @@ Proof.
   InvApproxRegs; SimplVM; inv H0.
   replace (Val.subl e#r1 (Vlong n2)) with (Val.addl e#r1 (Vlong (Int64.neg n2))).
   apply make_addlimm_correct; auto.
-  unfold Val.addl, Val.subl. destruct Archi.ptr64 eqn:SF, e#r1; auto. 
+  unfold Val.addl, Val.subl. destruct Archi.ptr64 eqn:SF, e#r1; auto.
   rewrite Int64.sub_add_opp; auto.
   rewrite Ptrofs.sub_add_opp. do 2 f_equal. auto with ptrofs.
   rewrite Int64.sub_add_opp; auto.
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index dbc8b064..ecfb85bf 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -63,6 +63,8 @@ Definition destroyed_at_call :=
 Definition dummy_int_reg := AX.     (**r Used in [Regalloc]. *)
 Definition dummy_float_reg := X0.   (**r Used in [Regalloc]. *)
 
+Definition callee_save_type := mreg_type.
+  
 Definition is_float_reg (r: mreg) :=
   match r with
   | AX | BX | CX | DX | SI | DI | BP
@@ -146,11 +148,11 @@ Lemma loc_result_pair:
   | One _ => True
   | Twolong r1 r2 =>
        r1 <> r2 /\ sg.(sig_res) = Some Tlong
-    /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true 
-    /\ Archi.splitlong = true
+    /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
+    /\ Archi.ptr64 = false
   end.
 Proof.
-  intros. change Archi.splitlong with (negb Archi.ptr64).
+  intros. 
   unfold loc_result, loc_result_32, loc_result_64, mreg_type;
   destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; auto.
   split; auto. congruence.
@@ -162,7 +164,7 @@ Lemma loc_result_exten:
   forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
 Proof.
   intros. unfold loc_result, loc_result_32, loc_result_64.
-  destruct Archi.ptr64; rewrite H; auto.  
+  destruct Archi.ptr64; rewrite H; auto.
 Qed.
 
 (** ** Location of function arguments *)
@@ -310,7 +312,7 @@ Opaque list_nth_z.
   { intros. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H1.
     subst. left. eapply list_nth_z_in; eauto.
     eapply IHtyl; eauto.
-    subst. split. omega. assumption. 
+    subst. split. omega. assumption.
     eapply Y; eauto. omega. }
   assert (B: forall ty, In p
       match list_nth_z float_param_regs fr with
@@ -321,7 +323,7 @@ Opaque list_nth_z.
   { intros. destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H1.
     subst. right. eapply list_nth_z_in; eauto.
     eapply IHtyl; eauto.
-    subst. split. omega. assumption. 
+    subst. split. omega. assumption.
     eapply Y; eauto. omega. }
   destruct a; eauto.
 Qed.
@@ -337,15 +339,15 @@ Proof.
   assert (X: forall l, loc_argument_64_charact 0 l -> loc_argument_acceptable l).
   { unfold loc_argument_64_charact, loc_argument_acceptable.
     destruct l as [r | [] ofs ty]; auto.  intros [C|C]; auto.
-    intros [C D]. split; auto. apply Zdivide_trans with 2; auto. 
+    intros [C D]. split; auto. apply Zdivide_trans with 2; auto.
     exists (2 / typealign ty); destruct ty; reflexivity.
   }
-  exploit loc_arguments_64_charact; eauto using Zdivide_0. 
+  exploit loc_arguments_64_charact; eauto using Zdivide_0.
   unfold forall_rpair; destruct p; intuition auto.
 - (* 32 bits *)
   assert (X: forall l, loc_argument_32_charact 0 l -> loc_argument_acceptable l).
   { destruct l as [r | [] ofs ty]; simpl; intuition auto. rewrite H2; apply Z.divide_1_l. }
-  exploit loc_arguments_32_charact; eauto. 
+  exploit loc_arguments_32_charact; eauto.
   unfold forall_rpair; destruct p; intuition auto.
 Qed.
 
@@ -373,14 +375,14 @@ Proof.
     | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0
     | None => size_arguments_64 tyl ir fr (ofs0 + 2)
     end).
-  { destruct (list_nth_z int_param_regs ir); eauto. 
+  { destruct (list_nth_z int_param_regs ir); eauto.
     apply Zle_trans with (ofs0 + 2); auto. omega. }
   assert (B: ofs0 <=
     match list_nth_z float_param_regs fr with
     | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0
     | None => size_arguments_64 tyl ir fr (ofs0 + 2)
     end).
-  { destruct (list_nth_z float_param_regs fr); eauto. 
+  { destruct (list_nth_z float_param_regs fr); eauto.
     apply Zle_trans with (ofs0 + 2); auto. omega. }
   destruct a; auto.
 Qed.
@@ -420,7 +422,7 @@ Proof.
   contradiction.
   assert (T: forall ty0, typesize ty0 <= 2).
   { destruct ty0; simpl; omega. }
-  assert (A: forall ty0, 
+  assert (A: forall ty0,
              In (S Outgoing ofs ty) (regs_of_rpairs
               match list_nth_z int_param_regs ir with
               | Some ireg =>
@@ -435,9 +437,9 @@ Proof.
   { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0.
   - discriminate.
   - eapply IHtyl; eauto.
-  - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.  
+  - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
   - eapply IHtyl; eauto. }
-  assert (B: forall ty0, 
+  assert (B: forall ty0,
              In (S Outgoing ofs ty) (regs_of_rpairs
               match list_nth_z float_param_regs fr with
               | Some ireg =>
@@ -452,7 +454,7 @@ Proof.
   { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0.
   - discriminate.
   - eapply IHtyl; eauto.
-  - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.  
+  - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
   - eapply IHtyl; eauto. }
   destruct a; eauto.
 Qed.
diff --git a/x86/Machregs.v b/x86/Machregs.v
index 04be0cd6..ffaf2531 100644
--- a/x86/Machregs.v
+++ b/x86/Machregs.v
@@ -58,7 +58,7 @@ Proof.
 Qed.
 
 Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
-  
+
 Instance Finite_mreg : Finite mreg := {
   Finite_elements := all_mregs;
   Finite_elements_spec := all_mregs_complete
@@ -151,7 +151,7 @@ Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mre
   match chunk with
   | Mint8signed | Mint8unsigned => if Archi.ptr64 then nil else AX :: CX :: nil
   | _ => nil
-  end. 
+  end.
 
 Definition destroyed_by_cond (cond: condition): list mreg :=
   nil.
diff --git a/x86/NeedOp.v b/x86/NeedOp.v
index 09013cdd..68ecc745 100644
--- a/x86/NeedOp.v
+++ b/x86/NeedOp.v
@@ -225,7 +225,7 @@ Proof.
 - eapply needs_of_addressing_32_sound; eauto.
 - change (eval_addressing64 ge (Vptr sp Ptrofs.zero) a args')
     with (eval_operation ge (Vptr sp Ptrofs.zero) (Oleal a) args' m').
-  eapply default_needs_of_operation_sound; eauto. 
+  eapply default_needs_of_operation_sound; eauto.
   destruct a; simpl in H0; auto.
 - destruct (eval_condition cond args m) as [b|] eqn:EC; simpl in H2.
   erewrite needs_of_condition_sound by eauto.
diff --git a/x86/Op.v b/x86/Op.v
index 43133cfa..18f9e092 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -393,14 +393,14 @@ Remark eval_addressing_Aglobal:
   forall (F V: Type) (genv: Genv.t F V) sp id ofs,
   eval_addressing genv sp (Aglobal id ofs) nil = Some (Genv.symbol_address genv id ofs).
 Proof.
-  intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto. 
+  intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto.
 Qed.
 
 Remark eval_addressing_Ainstack:
   forall (F V: Type) (genv: Genv.t F V) sp ofs,
   eval_addressing genv sp (Ainstack ofs) nil = Some (Val.offset_ptr sp ofs).
 Proof.
-  intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto. 
+  intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto.
 Qed.
 
 Remark eval_addressing_Ainstack_inv:
@@ -605,7 +605,7 @@ Corollary type_of_addressing_sound:
   eval_addressing genv sp addr vl = Some v ->
   Val.has_type v Tptr.
 Proof.
-  unfold eval_addressing, Tptr; intros. 
+  unfold eval_addressing, Tptr; intros.
   destruct Archi.ptr64; eauto using type_of_addressing64_sound, type_of_addressing32_sound.
 Qed.
 
@@ -815,7 +815,7 @@ Lemma eval_shift_stack_addressing32:
   eval_addressing32 ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl =
   eval_addressing32 ge (Vptr sp (Ptrofs.repr delta)) addr vl.
 Proof.
-  intros. 
+  intros.
   assert (A: forall i, Ptrofs.add Ptrofs.zero (Ptrofs.add i (Ptrofs.repr delta)) = Ptrofs.add (Ptrofs.repr delta) i).
   { intros. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut. }
   destruct addr; simpl; rewrite ?A; reflexivity.
@@ -826,7 +826,7 @@ Lemma eval_shift_stack_addressing64:
   eval_addressing64 ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl =
   eval_addressing64 ge (Vptr sp (Ptrofs.repr delta)) addr vl.
 Proof.
-  intros. 
+  intros.
   assert (A: forall i, Ptrofs.add Ptrofs.zero (Ptrofs.add i (Ptrofs.repr delta)) = Ptrofs.add (Ptrofs.repr delta) i).
   { intros. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut. }
   destruct addr; simpl; rewrite ?A; reflexivity.
@@ -837,7 +837,7 @@ Lemma eval_shift_stack_addressing:
   eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl =
   eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl.
 Proof.
-  intros. unfold eval_addressing. 
+  intros. unfold eval_addressing.
   destruct Archi.ptr64; auto using eval_shift_stack_addressing32, eval_shift_stack_addressing64.
 Qed.
 
@@ -1234,7 +1234,7 @@ Proof.
   inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
   inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
   inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
-  inv H4; simpl in H1; try discriminate. simpl. destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists. 
+  inv H4; simpl in H1; try discriminate. simpl. destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists.
   inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
   inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
   inv H4; simpl; auto.
@@ -1426,7 +1426,7 @@ Proof.
   rewrite eval_shift_stack_addressing.
   eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
   intros. apply symbol_address_inject.
-  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 Lemma eval_operation_inject:
@@ -1446,7 +1446,7 @@ Proof.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
   intros. apply symbol_address_inject.
-  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 End EVAL_INJECT.
diff --git a/x86/SelectLongproof.v b/x86/SelectLongproof.v
index 2262a70b..3bef632d 100644
--- a/x86/SelectLongproof.v
+++ b/x86/SelectLongproof.v
@@ -399,7 +399,7 @@ Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Va
 Proof.
   unfold mullimm. intros; red; intros.
   destruct Archi.splitlong eqn:SL.
-  eapply SplitLongproof.eval_mullimm; eauto.  
+  eapply SplitLongproof.eval_mullimm; eauto.
   predSpec Int64.eq Int64.eq_spec n Int64.zero.
   exists (Vlong Int64.zero); split. apply eval_longconst.
   destruct x; simpl; auto. subst n; rewrite Int64.mul_zero; auto.
@@ -426,14 +426,14 @@ Proof.
 - TrivialExists.
 Qed.
 
-Theorem eval_mullhu: 
+Theorem eval_mullhu:
   forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)).
 Proof.
   unfold mullhu; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhu; auto.
   red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto.
 Qed.
 
-Theorem eval_mullhs: 
+Theorem eval_mullhs:
   forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)).
 Proof.
   unfold mullhs; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhs; auto.
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index 2037760f..1200c3d7 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -369,14 +369,14 @@ Nondetfunction compimm (default: comparison -> int -> condition)
         Eop (Ocmp (negate_condition c)) el
       else if Int.eq_dec n2 Int.one then
         Eop (Ocmp c) el
-      else 
+      else
         Eop (Ointconst Int.zero) Enil
   | Cne, Eop (Ocmp c) el =>
       if Int.eq_dec n2 Int.zero then
         Eop (Ocmp c) el
       else if Int.eq_dec n2 Int.one then
         Eop (Ocmp (negate_condition c)) el
-      else 
+      else
         Eop (Ointconst Int.one) Enil
   | Ceq, Eop (Oandimm n1) (t1 ::: Enil) =>
       if Int.eq_dec n2 Int.zero then
@@ -420,7 +420,7 @@ Definition compfs (c: comparison) (e1: expr) (e2: expr) :=
 
 (** ** Integer conversions *)
 
-Nondetfunction cast8unsigned (e: expr) := 
+Nondetfunction cast8unsigned (e: expr) :=
   match e with
   | Eop (Ointconst n) Enil =>
       Eop (Ointconst (Int.zero_ext 8 n)) Enil
@@ -438,7 +438,7 @@ Nondetfunction cast8signed (e: expr) :=
       Eop Ocast8signed (e ::: Enil)
   end.
 
-Nondetfunction cast16unsigned (e: expr) := 
+Nondetfunction cast16unsigned (e: expr) :=
   match e with
   | Eop (Ointconst n) Enil =>
       Eop (Ointconst (Int.zero_ext 16 n)) Enil
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index 1728c39d..e2e0b830 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -115,7 +115,7 @@ Lemma eval_Olea_ptr:
   forall a el m,
   eval_operation ge sp (Olea_ptr a) el m = eval_addressing ge sp a el.
 Proof.
-  unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto. 
+  unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto.
 Qed.
 
 Theorem eval_addrsymbol:
@@ -162,7 +162,7 @@ Proof.
 + TrivialExists; simpl. rewrite Int.add_commut. auto.
 + inv H0. simpl in H6. TrivialExists. simpl.
   erewrite eval_offset_addressing_total_32 by eauto. rewrite Int.repr_signed; auto.
-+ TrivialExists. simpl. rewrite Int.repr_signed; auto. 
++ TrivialExists. simpl. rewrite Int.repr_signed; auto.
 Qed.
 
 Theorem eval_add: binary_constructor_sound add Val.add.
@@ -172,7 +172,7 @@ Proof.
   assert (B: forall id ofs n, Archi.ptr64 = false ->
              Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.repr n)) =
              Val.add (Genv.symbol_address ge id ofs) (Vint (Int.repr n))).
-  { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int (Int.repr n)) by auto with ptrofs. 
+  { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int (Int.repr n)) by auto with ptrofs.
     apply Genv.shift_symbol_address_32; auto. }
   red; intros until y.
   unfold add; case (add_match a b); intros; InvEval.
@@ -193,7 +193,7 @@ Proof.
 - TrivialExists.
 - TrivialExists. simpl. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
 - TrivialExists. simpl. rewrite Val.add_assoc; auto.
-- TrivialExists. simpl. 
+- TrivialExists. simpl.
   unfold Val.add; destruct Archi.ptr64, x, y; auto.
   + rewrite Int.add_zero; auto.
   + rewrite Int.add_zero; auto.
@@ -324,7 +324,7 @@ Proof.
   exploit (eval_shlimm j (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]].
   exploit eval_add. eexact A1. eexact A2. intros [v3 [A3 B3]].
   exists v3; split. econstructor; eauto.
-  rewrite D; simpl; rewrite Int.add_zero. 
+  rewrite D; simpl; rewrite Int.add_zero.
   replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one j)))
      with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint j))).
   rewrite Val.mul_add_distr_r.
@@ -936,12 +936,12 @@ Proof.
                      /\ eval_addressing ge sp (Aindexed 0) vl = Some v).
   { intros. exists (v :: nil); split. constructor; auto. constructor. auto. }
   unfold addressing; case (addressing_match a); intros.
-- destruct (negb Archi.ptr64 && addressing_valid addr) eqn:E. 
-+ inv H. InvBooleans. apply negb_true_iff in H. unfold eval_addressing; rewrite H. 
+- destruct (negb Archi.ptr64 && addressing_valid addr) eqn:E.
++ inv H. InvBooleans. apply negb_true_iff in H. unfold eval_addressing; rewrite H.
   exists vl; auto.
 + apply D; auto.
-- destruct (Archi.ptr64 && addressing_valid addr) eqn:E. 
-+ inv H. InvBooleans. unfold eval_addressing; rewrite H. 
+- destruct (Archi.ptr64 && addressing_valid addr) eqn:E.
++ inv H. InvBooleans. unfold eval_addressing; rewrite H.
   exists vl; auto.
 + apply D; auto.
 - apply D; auto.
diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v
index 44fd43b2..22c68099 100644
--- a/x86/Stacklayout.v
+++ b/x86/Stacklayout.v
@@ -72,7 +72,7 @@ Local Opaque Z.add Z.mul sepconj range.
   assert (0 <= 4 * b.(bound_outgoing)) by omega.
   assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
   assert (olink + w <= ocs) by (unfold ocs; omega).
-  assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
+  assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr).
   assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
   assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
   assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega).
@@ -88,13 +88,13 @@ Local Opaque Z.add Z.mul sepconj range.
   rewrite sep_swap34.
 (* Apply range_split and range_split2 repeatedly *)
   unfold fe_ofs_arg.
-  apply range_split_2. fold olink. omega. omega. 
+  apply range_split_2. fold olink. omega. omega.
   apply range_split. omega.
   apply range_split_2. fold ol. omega. omega.
   apply range_drop_right with ostkdata. omega.
   rewrite sep_swap.
   apply range_drop_left with (ostkdata + bound_stack_data b). omega.
-  rewrite sep_swap. 
+  rewrite sep_swap.
   exact H.
 Qed.
 
@@ -115,11 +115,11 @@ Proof.
   assert (0 <= 4 * b.(bound_outgoing)) by omega.
   assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
   assert (olink + w <= ocs) by (unfold ocs; omega).
-  assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
+  assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr).
   assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
   assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
   assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega).
-  split. omega. omega. 
+  split. omega. omega.
 Qed.
 
 Lemma frame_env_aligned: