Change preference for new register in allocator

Currently, the register allocator picks caller-save registers in preference
to callee-save registers.

But for ARM in Thumb mode, more compact code is obtained if we prefer
integer registers R0...R3 rather than all integer caller-save registers.

This commit introduces an `allocatable_registers` function in
$ARCH/Conventions1.v that determines the preferred and remaining
registers to be used for register allocation.

1 files changed, 26 insertions, 0 deletions

diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index 0ddd882f..cd722402 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -18,6 +18,7 @@ Require Import Decidableplus.
 Require Import AST.
 Require Import Events.
 Require Import Locations.
+Require Import Compopts.
 Require Archi.
 
 (** * Classification of machine registers *)
@@ -71,6 +72,31 @@ Definition is_float_reg (r: mreg): bool :=
   | F8  | F9  | F10  | F11 | F12  | F13  | F14  | F15 => true
   end.
 
+(** How to use registers for register allocation.
+    In classic ARM mode, we favor the use of caller-save registers,
+    using callee-save registers only when no caller-save is available.
+    In Thumb mode, we additionally favor integer registers R0 to R3 over the other
+    integer registers, as they lead to more compact instruction encodings. *)
+
+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) :=
+  if thumb tt then
+  {| preferred_int_regs := R0 :: R1 :: R2 :: R3 :: nil;
+     remaining_int_regs := R4 :: R5 :: R6 :: R7 :: R12 :: R8 :: R9 :: R10 :: R11 :: nil;
+     preferred_float_regs := float_caller_save_regs;
+     remaining_float_regs := float_callee_save_regs |}
+  else
+  {| 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