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.

1 files changed, 9 insertions, 9 deletions

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.