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, 33 insertions, 10 deletions

diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 0610b242..bf75d2e0 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -179,6 +179,14 @@ Proof.
 Qed.
 Hint Resolve rolm_label: labels.
 
+Remark loadimm64_label:
+  forall r n k, tail_nolabel k (loadimm64 r n k).
+Proof.
+  unfold loadimm64; intros.
+  destruct Int64.eq. TailNoLabel. destruct Int64.eq; TailNoLabel.
+Qed.
+Hint Resolve loadimm64_label: labels.
+
 Remark loadind_label:
   forall base ofs ty dst k c,
   loadind base ofs ty dst k = OK c -> tail_nolabel k c.
@@ -232,12 +240,27 @@ Remark transl_op_label:
 Proof.
 Opaque Int.eq.
   unfold transl_op; intros; destruct op; TailNoLabel.
-  destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
-  destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
-  destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
-  destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
-  destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
-  eapply transl_cond_op_label; eauto.
+- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
+- destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
+- destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
+- destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
+- destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
+- unfold addimm64, opimm64. destruct Int64.eq. TailNoLabel.
+  destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel.
+- unfold andimm64, andimm64_base, opimm64.
+  destruct (is_rldl_mask i || is_rldr_mask i). TailNoLabel.
+  destruct Int64.eq. TailNoLabel.
+  destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel.
+- unfold orimm64, opimm64. destruct Int64.eq. TailNoLabel.
+  destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel.
+- unfold xorimm64, opimm64. destruct Int64.eq. TailNoLabel.
+  destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel.
+- unfold rolm64, andimm64_base, opimm64.
+  destruct (is_rldl_mask i0 || is_rldr_mask i0 || is_rldl_mask (Int64.shru' i0 i)). TailNoLabel.
+  apply tail_nolabel_cons; unfold nolabel; auto.
+  destruct Int64.eq. TailNoLabel.
+  destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel.
+- eapply transl_cond_op_label; eauto.
 Qed.
 
 Remark transl_memory_access_label:
@@ -760,12 +783,12 @@ Opaque loadind.
   destruct (snd (crbit_for_cond cond)).
   (* Pbt, taken *)
   econstructor; econstructor; econstructor; split. eexact A.
-  split. eapply agree_exten; eauto with asmgen.
+  split. eapply agree_undef_regs; eauto with asmgen.
   split. simpl. rewrite B. reflexivity.
   auto with asmgen.
   (* Pbf, taken *)
   econstructor; econstructor; econstructor; split. eexact A.
-  split. eapply agree_exten; eauto with asmgen.
+  split. eapply agree_undef_regs; eauto with asmgen.
   split. simpl. rewrite B. reflexivity.
   auto with asmgen.
 
@@ -779,7 +802,7 @@ Opaque loadind.
   destruct (snd (crbit_for_cond cond)).
   apply exec_straight_one. simpl. rewrite B. reflexivity. auto.
   apply exec_straight_one. simpl. rewrite B. reflexivity. auto.
-  split. eapply agree_exten; eauto with asmgen.
+  split. eapply agree_undef_regs; eauto with asmgen.
   intros; Simpl.
   split. simpl. congruence.
   Simpl. 
@@ -865,7 +888,7 @@ Local Transparent destroyed_by_jumptable.
   apply exec_straight_two with rs4 m3'.
   simpl. unfold store1. rewrite gpr_or_zero_not_zero.
   change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR).
-  simpl const_low. rewrite ATLR. erewrite storev_offset_ptr by eexact P. auto. congruence.   
+  simpl const_low. rewrite ATLR. erewrite storev_offset_ptr by eexact P. auto. congruence.
   auto. auto. auto.
   left; exists (State rs5 m3'); split.
   eapply exec_straight_steps_1; eauto. omega. constructor.