From 1fe68ad575178f7d8a775906947d2fed94d40976 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 30 Jul 2011 09:54:35 +0000 Subject: 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 --- arm/Machregs.v | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) (limited to 'arm/Machregs.v') 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. -- cgit