Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 93 insertions, 31 deletions

diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 632a55d..ce66e6a 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -13,6 +13,7 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
+Require Import Op.
 
 (** ** Machine registers *)
 
@@ -21,59 +22,55 @@ Require Import AST.
 - Integer registers that can be allocated to RTL pseudo-registers ([Rxx]).
 - Floating-point registers that can be allocated to RTL pseudo-registers 
   ([Fxx]).
-- Two integer registers, not allocatable, reserved as temporaries for
-  spilling and reloading ([IT1, IT2]).
-- Two float registers, not allocatable, reserved as temporaries for
-  spilling and reloading ([FT1, FT2]).
 
   The type [mreg] does not include special-purpose or reserved
-  machine registers such as the stack pointer and the condition codes. *)
+  machine registers such as the stack pointer (GPR1), the small data area
+  pointers (GPR2, GPR13), and the condition codes. *)
 
 Inductive mreg: Type :=
   (** Allocatable integer regs *)
   | R3: mreg  | R4: mreg  | R5: mreg  | R6: mreg
   | R7: mreg  | R8: mreg  | R9: mreg  | R10: mreg
+  | R11: mreg | R12: mreg
   | R14: mreg | R15: mreg | R16: mreg
   | R17: mreg | R18: mreg | R19: mreg | R20: mreg
   | R21: mreg | R22: mreg | R23: mreg | R24: mreg
   | R25: mreg | R26: mreg | R27: mreg | R28: mreg
   | R29: mreg | R30: mreg | R31: mreg
   (** Allocatable float regs *)
+  | F0: mreg
   | F1: mreg  | F2: mreg  | F3: mreg  | F4: mreg
   | F5: mreg  | F6: mreg  | F7: mreg  | F8: mreg
-  | F9: mreg  | F10: mreg | F11: mreg
-  | F14: mreg | F15: mreg
+  | F9: mreg  | F10: mreg | F11: mreg | F12: mreg
+  | F13: mreg | F14: mreg | F15: mreg
   | F16: mreg | F17: mreg | F18: mreg | F19: mreg
   | F20: mreg | F21: mreg | F22: mreg | F23: mreg
   | F24: mreg | F25: mreg | F26: mreg | F27: mreg
-  | F28: mreg | F29: mreg | F30: mreg | F31: mreg
-  (** Integer temporaries *)
-  | IT1: mreg (* R11 *) | IT2: mreg (* R12 *)
-  (** Float temporaries *)
-  | FT1: mreg (* F0 *) | FT2: mreg (* F12 *) | FT3: mreg (* F13 *).
+  | F28: mreg | F29: mreg | F30: mreg | F31: mreg.
 
 Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
 Proof. decide equality. Defined.
+Global Opaque mreg_eq.
 
 Definition mreg_type (r: mreg): typ :=
   match r with
   | R3 => Tint  | R4 => Tint  | R5 => Tint  | R6 => Tint
   | R7 => Tint  | R8 => Tint  | R9 => Tint  | R10 => Tint
+  | R11 => Tint | R12 => Tint
   | R14 => Tint | R15 => Tint | R16 => Tint
   | R17 => Tint | R18 => Tint | R19 => Tint | R20 => Tint
   | R21 => Tint | R22 => Tint | R23 => Tint | R24 => Tint
   | R25 => Tint | R26 => Tint | R27 => Tint | R28 => Tint
   | R29 => Tint | R30 => Tint | R31 => Tint
+  | F0 => Tfloat
   | F1 => Tfloat  | F2 => Tfloat  | F3 => Tfloat  | F4 => Tfloat
   | F5 => Tfloat  | F6 => Tfloat  | F7 => Tfloat  | F8 => Tfloat
-  | F9 => Tfloat  | F10 => Tfloat | F11 => Tfloat
-  | F14 => Tfloat | F15 => Tfloat
+  | F9 => Tfloat  | F10 => Tfloat | F11 => Tfloat | F12 => Tfloat
+  | F13 => Tfloat | F14 => Tfloat | F15 => Tfloat
   | F16 => Tfloat | F17 => Tfloat | F18 => Tfloat | F19 => Tfloat
   | F20 => Tfloat | F21 => Tfloat | F22 => Tfloat | F23 => Tfloat
   | F24 => Tfloat | F25 => Tfloat | F26 => Tfloat | F27 => Tfloat
   | F28 => Tfloat | F29 => Tfloat | F30 => Tfloat | F31 => Tfloat
-  | IT1 => Tint | IT2 => Tint
-  | FT1 => Tfloat | FT2 => Tfloat | FT3 => Tfloat
   end.
 
 Open Scope positive_scope.
@@ -85,21 +82,21 @@ Module IndexedMreg <: INDEXED_TYPE.
     match r with
     | R3 => 1  | R4 => 2  | R5 => 3  | R6 => 4
     | R7 => 5  | R8 => 6  | R9 => 7  | R10 => 8
-    | R14 => 9 | R15 => 10 | R16 => 11
-    | R17 => 12 | R18 => 13 | R19 => 14 | R20 => 15
-    | R21 => 16 | R22 => 17 | R23 => 18 | R24 => 19
-    | R25 => 20 | R26 => 21 | R27 => 22 | R28 => 23
-    | R29 => 24 | R30 => 25 | R31 => 26
-    | F1 => 28  | F2 => 29  | F3 => 30  | F4 => 31
-    | F5 => 32  | F6 => 33  | F7 => 34  | F8 => 35
-    | F9 => 36  | F10 => 37 | F11 => 38
-    | F14 => 39 | F15 => 40
-    | F16 => 41 | F17 => 42 | F18 => 43 | F19 => 44
-    | F20 => 45 | F21 => 46 | F22 => 47 | F23 => 48
-    | F24 => 49 | F25 => 50 | F26 => 51 | F27 => 52
-    | F28 => 53 | F29 => 54 | F30 => 55 | F31 => 56
-    | IT1 => 57 | IT2 => 58
-    | FT1 => 59 | FT2 => 60 | FT3 => 61
+    | R11 => 9 | R12 => 10
+    | R14 => 11 | R15 => 12 | R16 => 13
+    | R17 => 14 | R18 => 15 | R19 => 16 | R20 => 17
+    | R21 => 18 | R22 => 19 | R23 => 20 | R24 => 21
+    | R25 => 22 | R26 => 23 | R27 => 24 | R28 => 25
+    | R29 => 26 | R30 => 27 | R31 => 28
+    | F0 => 29
+    | F1 => 30  | F2 => 31  | F3 => 32  | F4 => 33
+    | F5 => 34  | F6 => 35  | F7 => 36  | F8 => 37
+    | F9 => 38  | F10 => 39 | F11 => 40 | F12 => 41
+    | F13 => 42 | F14 => 43 | F15 => 44
+    | F16 => 45 | F17 => 46 | F18 => 47 | F19 => 48
+    | F20 => 49 | F21 => 50 | F22 => 51 | F23 => 52
+    | F24 => 53 | F25 => 54 | F26 => 55 | F27 => 56
+    | F28 => 57 | F29 => 58 | F30 => 59 | F31 => 60
     end.
   Lemma index_inj:
     forall r1 r2, index r1 = index r2 -> r1 = r2.
@@ -108,3 +105,68 @@ Module IndexedMreg <: INDEXED_TYPE.
   Qed.
 End IndexedMreg.
 
+(** ** Destroyed registers, preferred registers *)
+
+Definition destroyed_by_op (op: operation): list mreg :=
+  match op with
+  | Ofloatconst _ => R12 :: nil
+  | Ointoffloat => F13 :: nil
+  | _ => nil
+  end.
+
+Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg :=
+  R12 :: nil.
+
+Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg :=
+  match chunk with
+  | Mfloat32 => R11 :: R12 :: F13 :: nil
+  | _ => R11 :: R12 :: nil
+  end.
+
+Definition destroyed_by_cond (cond: condition): list mreg :=
+  nil.
+
+Definition destroyed_by_jumptable: list mreg :=
+  R12 :: nil.
+
+Definition destroyed_by_builtin (ef: external_function): list mreg :=
+  match ef with
+  | EF_builtin _ _ => F13 :: nil
+  | EF_vload _ => nil
+  | EF_vstore Mfloat32 => F13 :: nil
+  | EF_vstore _ => nil
+  | EF_vload_global _ _ _ => R11 :: nil
+  | EF_vstore_global Mint64 _ _ => R10 :: R11 :: R12 :: nil
+  | EF_vstore_global Mfloat32 _ _ => R11 :: R12 :: F13 :: nil
+  | EF_vstore_global _ _ _ => R11 :: R12 :: nil
+  | EF_memcpy _ _ => R11 :: R12 :: F13 :: nil
+  | _ => nil
+  end.
+
+Definition destroyed_at_function_entry: list mreg :=
+  nil.
+
+Definition temp_for_parent_frame: mreg :=
+  R11.
+
+Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
+  (nil, None).
+
+Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (option mreg) :=
+  (nil, nil).
+
+Global Opaque
+    destroyed_by_op destroyed_by_load destroyed_by_store
+    destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin
+    destroyed_at_function_entry temp_for_parent_frame
+    mregs_for_operation mregs_for_builtin.
+
+(** 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. *)
+
+Definition two_address_op (op: operation) : bool :=
+  match op with
+  | Oroli _ _ => true
+  | _ => false
+  end.