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, 8 insertions, 8 deletions

diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index c89f8435..17a518cd 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1468,7 +1468,7 @@ End SOUNDNESS.
 
 (** ** Extension to separate compilation *)
 
-(** Following Kang et al, POPL 2016, we now extend the results above 
+(** Following Kang et al, POPL 2016, we now extend the results above
   to the case where only one compilation unit is analyzed, and not the
   whole program.  *)
 
@@ -1485,14 +1485,14 @@ Inductive sound_state: state -> Prop :=
 Theorem sound_step:
   forall st t st', RTL.step ge st t st' -> sound_state st -> sound_state st'.
 Proof.
-  intros. inv H0. constructor; intros. eapply sound_step_base; eauto. 
+  intros. inv H0. constructor; intros. eapply sound_step_base; eauto.
 Qed.
 
 Remark sound_state_inv:
   forall st cunit,
   sound_state st -> linkorder cunit prog -> sound_state_base cunit ge st.
 Proof.
-  intros. inv H. eauto. 
+  intros. inv H. eauto.
 Qed.
 
 End LINKING.
@@ -1700,7 +1700,7 @@ Proof.
   rewrite PTree.gsspec in H2. destruct (peq id id1).
   inv H2. rewrite PTree.gss in H3. discriminate.
   assert (Plt b (Genv.genv_next g)) by (eapply Genv.genv_symb_range; eauto).
-  rewrite PTree.gso in H3 by (apply Plt_ne; auto). 
+  rewrite PTree.gso in H3 by (apply Plt_ne; auto).
   assert (Mem.valid_block m b) by (red; rewrite <- H; auto).
   assert (b <> b1) by (apply Mem.valid_not_valid_diff with m; eauto with mem).
   apply bmatch_inv with m.
@@ -1729,7 +1729,7 @@ Proof.
   intros. eapply Mem.loadbytes_drop; eauto.
   right; right; right. unfold Genv.perm_globvar. rewrite H4, H5. constructor.
 + assert (Plt b (Genv.genv_next g)) by (eapply Genv.genv_symb_range; eauto).
-  rewrite PTree.gso in H3 by (apply Plt_ne; auto). 
+  rewrite PTree.gso in H3 by (apply Plt_ne; auto).
   assert (Mem.valid_block m b) by (red; rewrite <- H; auto).
   assert (b <> b1) by (apply Mem.valid_not_valid_diff with m; eauto with mem).
   apply bmatch_inv with m3.
@@ -1773,14 +1773,14 @@ Lemma alloc_global_consistent:
 Proof.
   intros; red; intros. destruct idg as [id1 [f1 | v1]]; simpl in *.
 - rewrite PTree.grspec in H0. destruct (PTree.elt_eq id id1); try discriminate.
-  rewrite PTree.gso by auto. apply H; auto. 
+  rewrite PTree.gso by auto. apply H; auto.
 - destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)) eqn:RO.
 + InvBooleans. rewrite negb_true_iff in H4.
   rewrite PTree.gsspec in *. destruct (peq id id1).
 * inv H0. exists v1; auto.
 * apply H; auto.
 + rewrite PTree.grspec in H0. destruct (PTree.elt_eq id id1); try discriminate.
-  rewrite PTree.gso by auto. apply H; auto. 
+  rewrite PTree.gso by auto. apply H; auto.
 Qed.
 
 Lemma romem_for_consistent:
@@ -1802,7 +1802,7 @@ Proof.
   exploit (romem_for_consistent cunit); eauto. intros (v & DM & RO & VO & DEFN & AB).
   destruct (prog_defmap_linkorder _ _ _ _ H DM) as (gd & P & Q).
   assert (gd = Gvar v).
-  { inv Q. inv H2. simpl in *. f_equal. f_equal. 
+  { inv Q. inv H2. simpl in *. f_equal. f_equal.
     destruct info1, info2; auto.
     inv H3; auto; discriminate. }
   subst gd. exists v; auto.