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

diff --git a/backend/Bounds.v b/backend/Bounds.v
index 8a383380..93a4b504 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -190,7 +190,7 @@ Remark fold_left_ensures:
   (forall a, P (f a b0)) ->
   forall l a, In b0 l -> P (fold_left f l a).
 Proof.
-  induction l; simpl; intros. contradiction. 
+  induction l; simpl; intros. contradiction.
   destruct H1. subst a. apply fold_left_preserves; auto. apply IHl; auto.
 Qed.
 
@@ -199,7 +199,7 @@ Definition only_callee_saves (u: RegSet.t) : Prop :=
 
 Lemma record_reg_only: forall u r, only_callee_saves u -> only_callee_saves (record_reg u r).
 Proof.
-  unfold only_callee_saves, record_reg; intros. 
+  unfold only_callee_saves, record_reg; intros.
   destruct (is_callee_save r) eqn:CS; auto.
   destruct (mreg_eq r r0). congruence. apply H; eapply RegSet.add_3; eauto.
 Qed.
@@ -214,11 +214,11 @@ Proof.
   intros. destruct i; simpl; auto using record_reg_only, record_regs_only.
 Qed.
 
-Lemma record_regs_of_function_only: 
+Lemma record_regs_of_function_only:
   only_callee_saves record_regs_of_function.
 Proof.
   intros. unfold record_regs_of_function.
-  apply fold_left_preserves. apply record_regs_of_instr_only. 
+  apply fold_left_preserves. apply record_regs_of_instr_only.
   red; intros. eelim RegSet.empty_1; eauto.
 Qed.
 
@@ -248,7 +248,7 @@ Next Obligation.
   apply record_regs_of_function_only. apply RegSet.elements_2.
   apply InA_alt. exists r; auto.
 Qed.
-  
+
 (** We now show the correctness of the inferred bounds. *)
 
 Lemma record_reg_incr: forall u r r', RegSet.In r' u -> RegSet.In r' (record_reg u r).
@@ -268,7 +268,7 @@ Qed.
 
 Lemma record_regs_ok: forall r rl u, In r rl -> is_callee_save r = true -> RegSet.In r (record_regs u rl).
 Proof.
-  intros. unfold record_regs. eapply fold_left_ensures; eauto using record_reg_incr, record_reg_ok. 
+  intros. unfold record_regs. eapply fold_left_ensures; eauto using record_reg_incr, record_reg_ok.
 Qed.
 
 Lemma record_regs_of_instr_incr: forall r' u i, RegSet.In r' u -> RegSet.In r' (record_regs_of_instr u i).
@@ -291,7 +291,7 @@ Proof.
   destruct H; auto using record_regs_incr, record_regs_ok.
 Qed.
 
-Lemma record_regs_of_function_ok: 
+Lemma record_regs_of_function_ok:
   forall r i, In i f.(fn_code) -> defined_by_instr r i -> is_callee_save r = true -> RegSet.In r record_regs_of_function.
 Proof.
   intros. unfold record_regs_of_function.
@@ -373,9 +373,9 @@ Lemma mreg_is_within_bounds:
   forall r, defined_by_instr r i ->
   mreg_within_bounds function_bounds r.
 Proof.
-  intros. unfold mreg_within_bounds. intros. 
+  intros. unfold mreg_within_bounds. intros.
   exploit record_regs_of_function_ok; eauto. intros.
-  apply RegSet.elements_1 in H2. rewrite InA_alt in H2. destruct H2 as (r' & A & B). 
+  apply RegSet.elements_1 in H2. rewrite InA_alt in H2. destruct H2 as (r' & A & B).
   subst r'; auto.
 Qed.
 
@@ -447,9 +447,9 @@ Proof.
 Local Opaque mreg_type.
   induction l as [ | r l]; intros; simpl.
 - omega.
-- eapply Zle_trans. 2: apply IHl. 
+- eapply Zle_trans. 2: apply IHl.
   generalize (AST.typesize_pos (mreg_type r)); intros.
-  apply Zle_trans with (align ofs (AST.typesize (mreg_type r))). 
+  apply Zle_trans with (align ofs (AST.typesize (mreg_type r))).
   apply align_le; auto.
   omega.
 Qed.