summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-11-02 10:53:17 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-11-02 10:53:17 +0000
commite47dcb416c68da4e559d70e633276f7227659740 (patch)
treee0ffcfd7a6c291e77bcb083a646ea8b4fb20224a
parent5d84e6862562eb14fe489c297864e660ace12418 (diff)
Use callee-save regs starting with R31/F31 and going down, like Diab does
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1166 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--powerpc/eabi/Conventions.v28
1 files changed, 14 insertions, 14 deletions
diff --git a/powerpc/eabi/Conventions.v b/powerpc/eabi/Conventions.v
index acad012..fd3a4eb 100644
--- a/powerpc/eabi/Conventions.v
+++ b/powerpc/eabi/Conventions.v
@@ -38,12 +38,12 @@ Definition float_caller_save_regs :=
F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: nil.
Definition int_callee_save_regs :=
- R14 :: R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 ::
- R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: R31 :: nil.
+ R31 :: R30 :: R29 :: R28 :: R27 :: R26 :: R25 :: R24 :: R23 ::
+ R22 :: R21 :: R20 :: R19 :: R18 :: R17 :: R16 :: R15 :: R14 :: nil.
Definition float_callee_save_regs :=
- F14 :: F15 :: F16 :: F17 :: F18 :: F19 :: F20 :: F21 :: F22 ::
- F23 :: F24 :: F25 :: F26 :: F27 :: F28 :: F29 :: F30 :: F31 :: nil.
+ F31 :: F30 :: F29 :: F28 :: F27 :: F26 :: F25 :: F24 :: F23 ::
+ F22 :: F21 :: F20 :: F19 :: F18 :: F17 :: F16 :: F15 :: F14 :: nil.
Definition destroyed_at_call_regs :=
int_caller_save_regs ++ float_caller_save_regs.
@@ -65,20 +65,20 @@ Definition temporaries :=
Definition index_int_callee_save (r: mreg) :=
match r with
- | R14 => 0 | R15 => 1 | R16 => 2 | R17 => 3
- | R18 => 4 | R19 => 5 | R20 => 6 | R21 => 7
- | R22 => 8 | R23 => 9 | R24 => 10 | R25 => 11
- | R26 => 12 | R27 => 13 | R28 => 14 | R29 => 15
- | R30 => 16 | R31 => 17 | _ => -1
+ | R14 => 17 | R15 => 16 | R16 => 15 | R17 => 14
+ | R18 => 13 | R19 => 12 | R20 => 11 | R21 => 10
+ | R22 => 9 | R23 => 8 | R24 => 7 | R25 => 6
+ | R26 => 5 | R27 => 4 | R28 => 3 | R29 => 2
+ | R30 => 1 | R31 => 0 | _ => -1
end.
Definition index_float_callee_save (r: mreg) :=
match r with
- | F14 => 0 | F15 => 1 | F16 => 2 | F17 => 3
- | F18 => 4 | F19 => 5 | F20 => 6 | F21 => 7
- | F22 => 8 | F23 => 9 | F24 => 10 | F25 => 11
- | F26 => 12 | F27 => 13 | F28 => 14 | F29 => 15
- | F30 => 16 | F31 => 17 | _ => -1
+ | F14 => 17 | F15 => 16 | F16 => 15 | F17 => 14
+ | F18 => 13 | F19 => 12 | F20 => 11 | F21 => 10
+ | F22 => 9 | F23 => 8 | F24 => 7 | F25 => 6
+ | F26 => 5 | F27 => 4 | F28 => 3 | F29 => 2
+ | F30 => 1 | F31 => 0 | _ => -1
end.
Ltac ElimOrEq :=