diff options
Diffstat (limited to 'aarch64/Conventions1.v')
| -rw-r--r-- | aarch64/Conventions1.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v index 3e7159ac..c8d1d4dd 100644 --- a/aarch64/Conventions1.v +++ b/aarch64/Conventions1.v @@ -83,6 +83,23 @@ Definition is_float_reg (r: mreg): bool := | F24 | F25 | F26 | F27 | F28 | F29 | F30 | F31 => true end. +(** How to use registers for register allocation. + We favor the use of caller-save registers, using callee-save registers + only when no caller-save is available. *) + +Record alloc_regs := mk_alloc_regs { + preferred_int_regs: list mreg; + remaining_int_regs: list mreg; + preferred_float_regs: list mreg; + remaining_float_regs: list mreg +}. + +Definition allocatable_registers (_: unit) := + {| preferred_int_regs := int_caller_save_regs; + remaining_int_regs := int_callee_save_regs; + preferred_float_regs := float_caller_save_regs; + remaining_float_regs := float_callee_save_regs |}. + (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers |