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

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 4b782286..f905ffa2 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -425,7 +425,7 @@ Proof.
             cmatch (Val.cmpu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2))
                    (Maybe (Ptrofs.cmpu c ofs1 ofs2))).
   {
-    intros. subst b2. simpl. destruct Archi.ptr64. 
+    intros. subst b2. simpl. destruct Archi.ptr64.
     constructor.
     rewrite dec_eq_true.
     destruct ((valid b1 (Ptrofs.unsigned ofs1) || valid b1 (Ptrofs.unsigned ofs1 - 1)) &&
@@ -1492,7 +1492,7 @@ Proof.
 - apply vmatch_uns. red; intros. rewrite Int.bits_rol by auto.
   generalize (Int.unsigned_range n); intros.
   rewrite Zmod_small by omega.
-  apply H1. omega. omega. 
+  apply H1. omega. omega.
 - destruct (zlt n0 Int.zwordsize); auto with va.
   apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by omega.
   generalize (Int.unsigned_range n); intros.
@@ -1732,7 +1732,7 @@ Proof.
     destruct (Int.ltu i0 Int64.iwordsize'); constructor. }
   unfold shift_long. destruct y; auto.
   destruct (Int.ltu n Int64.iwordsize') eqn:LT; auto.
-  destruct x; auto. 
+  destruct x; auto.
   inv H; inv H0. rewrite LT. constructor.
 Qed.
 
@@ -1966,6 +1966,19 @@ Proof.
   rewrite LTU; auto with va.
 Qed.
 
+Definition rolml (x: aval) (amount: int) (mask: int64) :=
+  andl (roll x (I amount)) (L mask).
+
+Lemma rolml_sound:
+  forall v x amount mask,
+  vmatch v x -> vmatch (Val.rolml v amount mask) (rolml x amount mask).
+Proof.
+  intros.
+  replace (Val.rolml v amount mask) with (Val.andl (Val.roll v (Vint amount)) (Vlong mask)).
+  apply andl_sound. apply roll_sound. auto. constructor. constructor.
+  destruct v; auto.
+Qed.
+
 (** Pointer operations *)
 
 Definition offset_ptr (v: aval) (n: ptrofs) :=
@@ -2101,7 +2114,7 @@ Proof.
   apply Z.min_case; auto with va.
 Qed.
 
-Definition longofint (v: aval) := 
+Definition longofint (v: aval) :=
   match v with
   | I i => L (Int64.repr (Int.signed i))
   | _ => ntop1 v
@@ -2113,7 +2126,7 @@ Proof.
   unfold Val.longofint, longofint; intros; inv H; auto with va.
 Qed.
 
-Definition longofintu (v: aval) := 
+Definition longofintu (v: aval) :=
   match v with
   | I i => L (Int64.repr (Int.unsigned i))
   | _ => ntop1 v
@@ -2637,7 +2650,7 @@ Proof.
   assert (IP: forall i b ofs,
     cmatch (Val.cmpu_bool valid c (Vint i) (Vptr b ofs)) (cmp_different_blocks c)).
   {
-    intros. simpl. destruct Archi.ptr64. 
+    intros. simpl. destruct Archi.ptr64.
     apply cmp_different_blocks_none.
     destruct (Int.eq i Int.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))).
     apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
@@ -2645,7 +2658,7 @@ Proof.
   assert (PI: forall i b ofs,
     cmatch (Val.cmpu_bool valid c (Vptr b ofs) (Vint i)) (cmp_different_blocks c)).
   {
-    intros. simpl. destruct Archi.ptr64. 
+    intros. simpl. destruct Archi.ptr64.
     apply cmp_different_blocks_none.
     destruct (Int.eq i Int.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))).
     apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
@@ -2942,7 +2955,7 @@ Proof with (auto using provenance_monotone with va).
 - destruct (zlt n2 16); constructor...
 - destruct ptr64...
 - destruct ptr64...
-- destruct ptr64... 
+- destruct ptr64...
 - destruct ptr64...
 - destruct ptr64...
 - destruct ptr64...
@@ -3511,7 +3524,7 @@ Proof.
 - unfold ablock_load_anywhere; intros; congruence.
 - assert (A: forall i, ZTree.get i (ab_contents ab1) = ZTree.get i (ab_contents ab2)).
   {
-    intros. exploit ZTree.beq_sound; eauto. instantiate (1 := i). 
+    intros. exploit ZTree.beq_sound; eauto. instantiate (1 := i).
     destruct (ab_contents ab1)##i, (ab_contents ab2)##i; intros; try contradiction.
     InvBooleans; subst; auto.
     auto. }
@@ -3569,7 +3582,7 @@ Proof.
   { exploit smatch_lub_l; eauto. instantiate (1 := ab_summary y).
     intros [SUMM _]. eapply vnormalize_cast; eauto. }
   exploit BM2; eauto.
-  unfold ablock_load; simpl. rewrite ZTree.gcombine by auto. 
+  unfold ablock_load; simpl. rewrite ZTree.gcombine by auto.
   unfold combine_acontents;
   destruct (ab_contents x)##ofs as [[chunkx avx]|], (ab_contents y)##ofs as [[chunky avy]|]; auto.
   destruct (chunk_eq chunkx chunky); auto. subst chunky.
@@ -3588,7 +3601,7 @@ Proof.
   { exploit smatch_lub_r; eauto. instantiate (1 := ab_summary x).
     intros [SUMM _]. eapply vnormalize_cast; eauto. }
   exploit BM2; eauto.
-  unfold ablock_load; simpl. rewrite ZTree.gcombine by auto. 
+  unfold ablock_load; simpl. rewrite ZTree.gcombine by auto.
   unfold combine_acontents;
   destruct (ab_contents x)##ofs as [[chunkx avx]|], (ab_contents y)##ofs as [[chunky avy]|]; auto.
   destruct (chunk_eq chunkx chunky); auto. subst chunky.