ARM codegen ported to new ABI + VFD floats

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

1 files changed, 16 insertions, 10 deletions

diff --git a/arm/Machregs.v b/arm/Machregs.v
index 2e422d27..f5b53292 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -34,13 +34,15 @@ Inductive mreg: Type :=
   | R0: mreg  | R1: mreg  | R2: mreg  | R3: mreg
   | R4: mreg  | R5: mreg  | R6: mreg  | R7: mreg
   | R8: mreg  | R9: mreg  | R11: mreg
-  (** Allocatable float regs *)
-  | F0: mreg  | F1: mreg  | F4: mreg  | F5: mreg
-  | F6: mreg  | F7: mreg
+  (** Allocatable double-precision float regs *)
+  | F0: mreg  | F1: mreg  | F2: mreg  | F3: mreg
+  | F4: mreg  | F5: 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 (* F2 *) | FT2: mreg (* F3 *).
+  | FT1: mreg (* F6 *) | FT2: mreg (* F7 *).
 
 Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
 Proof. decide equality. Qed.
@@ -50,8 +52,10 @@ Definition mreg_type (r: mreg): typ :=
   | R0 => Tint  | R1 => Tint  | R2 => Tint  | R3 => Tint
   | R4 => Tint  | R5 => Tint  | R6 => Tint  | R7 => Tint
   | R8 => Tint  | R9 => Tint  | R11 => Tint
-  | F0 => Tfloat  | F1 => Tfloat  | F4 => Tfloat  | F5 => Tfloat
-  | F6 => Tfloat  | F7 => Tfloat
+  | F0 => Tfloat | F1 => Tfloat | F2 => Tfloat | F3 => Tfloat
+  | F4 => Tfloat| F5 => 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.
@@ -66,10 +70,12 @@ Module IndexedMreg <: INDEXED_TYPE.
     | 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 | F4 => 14  | F5 => 15
-    | F6 => 16 | F7 => 17
-    | IT1 => 18 | IT2 => 19
-    | FT1 => 20 | FT2 => 21
+    | 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
     end.
   Lemma index_inj:
     forall r1 r2, index r1 = index r2 -> r1 = r2.