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

diff --git a/arm/Machregs.v b/arm/Machregs.v
index 317515c..4906eb0 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -13,6 +13,7 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
+Require Import Op.
 
 (** ** Machine registers *)
 
@@ -21,43 +22,36 @@ 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 ([ITx]).
-- Two float registers, not allocatable, reserved as temporaries for
-  spilling and reloading ([FTx]).
 
-  The type [mreg] does not include special-purpose machine registers
-  such as the stack pointer and the condition codes. *)
+  The type [mreg] does not include reserved machine registers
+  such as the stack pointer, the link register, and the condition codes. *)
 
 Inductive mreg: Type :=
   (** Allocatable integer regs *)
   | R0: mreg  | R1: mreg  | R2: mreg  | R3: mreg
   | R4: mreg  | R5: mreg  | R6: mreg  | R7: mreg
-  | R8: mreg  | R9: mreg  | R11: mreg
+  | R8: mreg  | R9: mreg  | R10: mreg | R11: mreg
+  | R12: mreg
   (** Allocatable double-precision float regs *)
   | F0: mreg  | F1: mreg  | F2: mreg  | F3: mreg
-  | F4: mreg  | F5: mreg
+  | F4: mreg  | F5: mreg  | F6: mreg  | F7: mreg
   | F8: mreg  | F9: mreg  | F10: mreg | F11: mreg
-  | F12: mreg | F13: mreg | F14: mreg | F15: mreg
-  (** Integer temporaries *)
-  | IT1: mreg (* R10 *) | IT2: mreg (* R12 *)
-  (** Float temporaries *)
-  | FT1: mreg (* F6 *) | FT2: mreg (* F7 *).
+  | F12: mreg | F13: mreg | F14: mreg | F15: 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
   | R0 => Tint  | R1 => Tint  | R2 => Tint  | R3 => Tint
   | R4 => Tint  | R5 => Tint  | R6 => Tint  | R7 => Tint
-  | R8 => Tint  | R9 => Tint  | R11 => Tint
+  | R8 => Tint  | R9 => Tint  | R10 => Tint | R11 => Tint
+  | R12 => Tint
   | F0 => Tfloat | F1 => Tfloat | F2 => Tfloat | F3 => Tfloat
-  | F4 => Tfloat| F5 => Tfloat
+  | F4 => Tfloat| F5 => Tfloat  | F6 => Tfloat | F7 => Tfloat
   | F8 => Tfloat | F9 => Tfloat | F10 => Tfloat | F11 => Tfloat
   | F12 => Tfloat | F13 => Tfloat | F14 => Tfloat | F15 => Tfloat
-  | IT1 => Tint | IT2 => Tint
-  | FT1 => Tfloat | FT2 => Tfloat
   end.
 
 Open Scope positive_scope.
@@ -69,13 +63,12 @@ Module IndexedMreg <: INDEXED_TYPE.
     match r with
     | R0 => 1  | R1 => 2  | R2 => 3  | R3 => 4
     | R4 => 5  | R5 => 6  | R6 => 7  | R7 => 8
-    | R8 => 9  | R9 => 10 | R11 => 11
-    | F0 => 12 | F1 => 13 | F2 => 14  | F3 => 15
-    | F4 => 16 | F5 => 17
-    | F8 => 18 | F9 => 19 | F10 => 20 | F11 => 21
-    | F12 => 22 | F13 => 23 | F14 => 24 | F15 => 25
-    | IT1 => 26 | IT2 => 27
-    | FT1 => 28 | FT2 => 29
+    | R8 => 9  | R9 => 10 | R10 => 11 | R11 => 12
+    | R12 => 13
+    | F0 => 14 | F1 => 15 | F2 => 16  | F3 => 17
+    | F4 => 18 | F5 => 19 | F6 => 20  | F7 => 21
+    | F8 => 22 | F9 => 23 | F10 => 24 | F11 => 25
+    | F12 => 26 | F13 => 27 | F14 => 28 | F15 => 29
     end.
   Lemma index_inj:
     forall r1 r2, index r1 = index r2 -> r1 = r2.
@@ -84,3 +77,67 @@ Module IndexedMreg <: INDEXED_TYPE.
   Qed.
 End IndexedMreg.
 
+(** ** Destroyed registers, preferred registers *)
+
+Definition destroyed_by_op (op: operation): list mreg :=
+  match op with
+  | Odiv | Odivu => R0 :: R1 :: R2 :: R3 :: R12 :: nil
+  | Ointoffloat | Ointuoffloat => F6 :: nil
+  | _ => nil
+  end.
+
+Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg :=
+  nil.
+
+Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg :=
+  match chunk with
+  | Mfloat32 => F6 :: nil
+  | _ => nil
+  end.
+
+Definition destroyed_by_cond (cond: condition): list mreg :=
+  nil.
+
+Definition destroyed_by_jumptable: list mreg :=
+  nil.
+
+Definition destroyed_by_builtin (ef: external_function): list mreg :=
+  match ef with
+  | EF_memcpy sz al => if zle sz 32 then nil else R2 :: R3 :: R12 :: nil
+  | _ => R12 :: F6 :: nil
+  end.
+
+Definition destroyed_at_function_entry: list mreg :=
+  R12 :: nil.
+
+Definition temp_for_parent_frame: mreg :=
+  R12.
+
+Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
+  match op with
+  | Odiv | Odivu => (Some R0 :: Some R1 :: nil, Some R0)
+  | _ => (nil, None)
+  end.
+
+Definition mregs_for_builtin (ef: external_function): list (option mreg) * list(option mreg) :=
+  match ef with
+  | EF_memcpy sz al =>
+      if zle sz 32 then (nil, nil) else (Some R3 :: Some R2 :: nil, nil)
+  | _ => (nil, nil)
+  end.
+
+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 are none for ARM. *)
+
+Definition two_address_op (op: operation) : bool :=
+  false.
+
+Global Opaque two_address_op.
+