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

diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 0a4b3ef6..2d9ae7a5 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -239,7 +239,7 @@ Definition mulhu (e1: expr) (e2: expr) := Eop Omulhu (e1 ::: e2 ::: Enil).
 
 (** ** Bitwise and, or, xor *)
 
-Nondetfunction andimm (n1: int) (e2: expr) := 
+Nondetfunction andimm (n1: int) (e2: expr) :=
   if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else
   if Int.eq n1 Int.mone then e2 else
   match e2 with
@@ -249,7 +249,7 @@ Nondetfunction andimm (n1: int) (e2: expr) :=
       let n := Int.and n1 n2 in
       if Int.eq (Int.shru (Int.shl n amount) amount) n
       && Int.ltu amount Int.iwordsize
-      then rolm t2 (Int.sub Int.iwordsize amount) 
+      then rolm t2 (Int.sub Int.iwordsize amount)
                    (Int.and (Int.shru Int.mone amount) n)
       else Eop (Oandimm n) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil)
   | Eop (Oandimm n2) (t2:::Enil) =>
@@ -259,7 +259,7 @@ Nondetfunction andimm (n1: int) (e2: expr) :=
   | Eop (Oshrimm amount) (t2:::Enil) =>
       if Int.eq (Int.shru (Int.shl n1 amount) amount) n1
       && Int.ltu amount Int.iwordsize
-      then rolm t2 (Int.sub Int.iwordsize amount) 
+      then rolm t2 (Int.sub Int.iwordsize amount)
                    (Int.and (Int.shru Int.mone amount) n1)
       else Eop (Oandimm n1) (e2:::Enil)
   | _ =>
@@ -396,14 +396,14 @@ Nondetfunction compimm (default: comparison -> int -> condition)
         Eop (Ocmp (negate_condition c)) el
       else if Int.eq_dec n2 Int.one then
         Eop (Ocmp c) el
-      else 
+      else
         Eop (Ointconst Int.zero) Enil
   | Cne, Eop (Ocmp c) el =>
       if Int.eq_dec n2 Int.zero then
         Eop (Ocmp c) el
       else if Int.eq_dec n2 Int.one then
         Eop (Ocmp (negate_condition c)) el
-      else 
+      else
         Eop (Ointconst Int.one) Enil
   | Ceq, Eop (Oandimm n1) (t1 ::: Enil) =>
       if Int.eq_dec n2 Int.zero then
@@ -483,7 +483,8 @@ Nondetfunction floatofintu (e: expr) :=
   | Eop (Ointconst n) Enil =>
       Eop (Ofloatconst (Float.of_intu n)) Enil
   | _ =>
-      if Archi.ppc64 then Eop Ofloatofintu (e ::: Enil) else
+      if Archi.ppc64 then
+        Eop Ofloatofintu (e ::: Enil)  else
         subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
              (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
   end.
@@ -493,7 +494,8 @@ Nondetfunction floatofint (e: expr) :=
   | Eop (Ointconst n) Enil =>
       Eop (Ofloatconst (Float.of_int n)) Enil
   | _ =>
-      if Archi.ppc64 then Eop Ofloatofint (e ::: Enil) else
+      if Archi.ppc64 then
+        Eop Ofloatofint (e ::: Enil) else
         subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
                                  ::: addimm Float.ox8000_0000 e ::: Enil))
              (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil)
@@ -517,7 +519,7 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 (** ** Recognition of addressing modes for load and store operations *)
 
 Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
-  match chunk with Mint64 => false | _ => true end.
+  match chunk with Mint64 => Archi.ppc64 | _ => true end.
 
 Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   match e with
@@ -539,6 +541,7 @@ Nondetfunction builtin_arg (e: expr) :=
   | Eop (Ointconst n) Enil => BA_int n
   | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs
   | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs
+  | Eop (Olongconst n) Enil => BA_long n
   | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
         BA_long (Int64.ofwords h l)
   | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)