diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-02 12:42:19 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-02 12:42:19 +0000 |
commit | 265fa07b34a813ba9d8249ddad82d71e6002c10d (patch) | |
tree | 45831b1793c7920b10969fc7cf6316c202d78e91 /powerpc/macosx | |
parent | 94470fb6a652cb993982269fcb7a0e8319b54488 (diff) | |
download | compcert-265fa07b34a813ba9d8249ddad82d71e6002c10d.tar.gz compcert-265fa07b34a813ba9d8249ddad82d71e6002c10d.zip |
Merge of the reuse-temps branch:
- Reload temporaries are marked as destroyed (set to Vundef) across
operations in the semantics of LTL, LTLin, Linear and Mach,
allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/macosx')
-rw-r--r-- | powerpc/macosx/Conventions1.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/powerpc/macosx/Conventions1.v b/powerpc/macosx/Conventions1.v index a5741e1c..2a0f2336 100644 --- a/powerpc/macosx/Conventions1.v +++ b/powerpc/macosx/Conventions1.v @@ -35,7 +35,7 @@ Definition int_caller_save_regs := R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: nil. Definition float_caller_save_regs := - F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: nil. + F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: F11 :: nil. Definition int_callee_save_regs := R14 :: R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 :: @@ -58,6 +58,9 @@ Definition float_temporaries := FT1 :: FT2 :: FT3 :: nil. Definition temporaries := R IT1 :: R IT2 :: R FT1 :: R FT2 :: R FT3 :: nil. +Definition dummy_int_reg := R3. (**r Used in [Coloring]. *) +Definition dummy_float_reg := F1. (**r Used in [Coloring]. *) + (** The [index_int_callee_save] and [index_float_callee_save] associate a unique positive integer to callee-save registers. This integer is used in [Stacking] to determine where to save these registers in @@ -291,7 +294,7 @@ Qed. (** The PowerPC ABI states the following convention for passing arguments to a function: - The first 8 integer arguments are passed in registers [R3] to [R10]. -- The first 10 float arguments are passed in registers [F1] to [F10]. +- The first 11 float arguments are passed in registers [F1] to [F11]. - Each float argument passed in a float register ``consumes'' two integer arguments. - Extra arguments are passed on the stack, in [Outgoing] slots, consecutively @@ -327,7 +330,7 @@ Fixpoint loc_arguments_rec Definition int_param_regs := R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: nil. Definition float_param_regs := - F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: nil. + F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: F11 :: nil. (** [loc_arguments s] returns the list of locations where to store arguments when calling a function with signature [s]. *) @@ -589,4 +592,3 @@ Proof. intro; simpl. ElimOrEq; reflexivity. intro; simpl. ElimOrEq; reflexivity. Qed. - |