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, 18 insertions, 5 deletions

diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index ce9c3542..6f2c6a03 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -86,7 +86,7 @@ Definition mreg_type (r: mreg): typ :=
   match r with
   | R3  | R4  | R5  | R6  | R7  | R8  | R9  | R10  | R11 | R12
   | R14 | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24
-  | R25 | R26 | R27 | R28 | R29 | R30 | R31 => Tany32
+  | R25 | R26 | R27 | R28 | R29 | R30 | R31 => if Archi.ppc64 then Tany64 else Tany32
   | F0  | F1  | F2  | F3  | F4  | F5  | F6  | F7
   | F8  | F9  | F10 | F11 | F12 | F13 | F14 | F15
   | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23
@@ -159,11 +159,25 @@ Definition register_by_name (s: string) : option mreg :=
 
 (** ** Destroyed registers, preferred registers *)
 
+Definition destroyed_by_cond (cond: condition): list mreg :=
+  match cond with
+  | Ccomplimm _ _ | Ccompluimm _ _ => R12 :: nil
+  | _ => nil
+  end.
+
 Definition destroyed_by_op (op: operation): list mreg :=
   match op with
   | Ofloatconst _ => R12 :: nil
   | Osingleconst _ => R12 :: nil
+  | Olongconst _ => R12 :: nil
   | Ointoffloat | Ointuoffloat => F13 :: nil
+  | Olongoffloat => F13 :: nil
+  | Oaddlimm _ => R12 :: nil
+  | Oandlimm _ => R12 :: nil
+  | Oorlimm _ => R12 :: nil
+  | Oxorlimm _ => R12 :: nil
+  | Orolml _ _ => R12 :: nil
+  | Ocmp c => destroyed_by_cond c
   | _ => nil
   end.
 
@@ -173,9 +187,6 @@ Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg
 Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg :=
   R11 :: R12 :: nil.
 
-Definition destroyed_by_cond (cond: condition): list mreg :=
-  nil.
-
 Definition destroyed_by_jumptable: list mreg :=
   R12 :: nil.
 
@@ -239,11 +250,13 @@ Global Opaque
 
 (** Two-address operations.  Return [true] if the first argument and
   the result must be in the same location *and* are unconstrained
-  by [mregs_for_operation]. There is only one: rotate-mask-insert. *)
+  by [mregs_for_operation]. *)
 
 Definition two_address_op (op: operation) : bool :=
   match op with
   | Oroli _ _ => true
+  | Olowlong => true
+  | Ofloatofsingle => true
   | _ => false
   end.