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

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.