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.

7 files changed, 129 insertions, 29 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
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
diff --git a/backend/IRC.ml b/backend/IRC.ml
index 1246a2d0..f9d7d770 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -195,8 +195,8 @@ module IntPairs = Hashtbl.Make(struct
 
 type graph = {
   (* Machine registers available for allocation *)
-  caller_save_registers: mreg array array;
-  callee_save_registers: mreg array array;
+  preferred_registers: mreg array array;
+  remaining_registers: mreg array array;
   num_available_registers: int array;
   start_points: int array;
   allocatable_registers: mreg list;
@@ -262,27 +262,28 @@ let rec remove_reserved = function
 (* Initialize and return an empty graph *)
 
 let init costs =
-  let int_caller_save = remove_reserved int_caller_save_regs
-  and float_caller_save = remove_reserved float_caller_save_regs
-  and int_callee_save = remove_reserved int_callee_save_regs
-  and float_callee_save = remove_reserved float_callee_save_regs in
+  let aregs = allocatable_registers () in
+  let int_preferred_regs = remove_reserved aregs.preferred_int_regs
+  and float_preferred_regs = remove_reserved aregs.preferred_float_regs
+  and int_remaining_regs = remove_reserved aregs.remaining_int_regs
+  and float_remaining_regs = remove_reserved aregs.remaining_float_regs in
   {
-    caller_save_registers =
-      [| Array.of_list int_caller_save;
-         Array.of_list float_caller_save;
+    preferred_registers =
+      [| Array.of_list int_preferred_regs;
+         Array.of_list float_preferred_regs;
          [||] |];
-    callee_save_registers =
-      [| Array.of_list int_callee_save;
-         Array.of_list float_callee_save;
+    remaining_registers =
+      [| Array.of_list int_remaining_regs;
+         Array.of_list float_remaining_regs;
          [||] |];
     num_available_registers =
-      [| List.length int_caller_save + List.length int_callee_save;
-         List.length float_caller_save + List.length float_callee_save;
+      [| List.length int_preferred_regs + List.length int_remaining_regs;
+         List.length float_preferred_regs + List.length float_remaining_regs;
          0 |];
     start_points =
       [| 0; 0; 0 |];
     allocatable_registers =
-      int_caller_save @ int_callee_save @ float_caller_save @ float_callee_save;
+      int_preferred_regs @ int_remaining_regs @ float_preferred_regs @ float_remaining_regs;
     stats_of_reg = costs;
     varTable = Hashtbl.create 253;
     nextIdent = 0;
@@ -773,13 +774,17 @@ let rec nodeOrder g stack =
 (* Assign a color (i.e. a hardware register or a stack location)
    to a node.  The color is chosen among the colors that are not
    assigned to nodes with which this node interferes.  The choice
-   is guided by the following heuristics: consider first caller-save
-   hardware register of the correct type; second, callee-save registers;
-   third, a stack location.  Callee-save registers and stack locations
-   are ``expensive'' resources, so we try to minimize their number
-   by picking the smallest available callee-save register or stack location.
-   In contrast, caller-save registers are ``free'', so we pick an
-   available one pseudo-randomly. *)
+   is guided by the following heuristics: consider first the preferred
+   hardware registers of the correct type; second the remaining
+   registers; third, a stack location.
+   For most architectures the preferred registers are the caller-save hardware
+   register and the rest are the callee-save hardware registers.
+   For some architectures these differ due other constraints.
+   Non-preferred registers (which always include callee-save registers)
+   and stack locations  are ``expensive'' resources,
+   so we try to minimize their number by picking the smallest available
+   callee-save register or stack location.  In contrast, preferred
+   registers are ``free'', so we pick an available one pseudo-randomly. *)
 
 module Regset =
   Set.Make(struct type t = mreg let compare = compare end)
@@ -792,22 +797,22 @@ let find_reg g conflicts regclass =
       then find avail (curr + 1) last
       else Some (R r)
     end in
-  let caller_save = g.caller_save_registers.(regclass)
-  and callee_save = g.callee_save_registers.(regclass)
+  let preferred_reg = g.preferred_registers.(regclass)
+  and remaining_reg = g.remaining_registers.(regclass)
   and start = g.start_points.(regclass) in
-  match find caller_save start (Array.length caller_save) with
+  match find preferred_reg start (Array.length preferred_reg) with
   | Some _ as res ->
       g.start_points.(regclass) <-
-        (if start + 1 < Array.length caller_save then start + 1 else 0);
+        (if start + 1 < Array.length preferred_reg then start + 1 else 0);
       res
   | None ->
-      match find caller_save 0 start with
+      match find preferred_reg 0 start with
       | Some _ as res ->
           g.start_points.(regclass) <-
-            (if start + 1 < Array.length caller_save then start + 1 else 0);
+            (if start + 1 < Array.length preferred_reg then start + 1 else 0);
           res
       | None ->
-          find callee_save 0 (Array.length callee_save)
+          find remaining_reg 0 (Array.length remaining_reg)
 
 (* Aggressive coalescing of stack slots.  When assigning a slot,
    try first the slots assigned to the pseudoregs for which we
diff --git a/extraction/extraction.v b/extraction/extraction.v
index e52a06ee..a714c831 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -167,6 +167,7 @@ Separate Extraction
    Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs
    Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs
    Conventions1.dummy_int_reg Conventions1.dummy_float_reg
+   Conventions1.allocatable_registers
    RTL.instr_defs RTL.instr_uses
    Machregs.mregs_for_operation Machregs.mregs_for_builtin
    Machregs.two_address_op Machregs.is_stack_reg
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index f05e77df..2b93e1d8 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -91,6 +91,23 @@ Definition float_callee_save_regs :=
 Definition dummy_int_reg := R3.     (**r Used in [Coloring]. *)
 Definition dummy_float_reg := F0.   (**r Used in [Coloring]. *)
 
+(** 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
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index eeaae3c4..2e2cedab 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -89,6 +89,23 @@ Definition is_float_reg (r: mreg) :=
   | 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
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index a4e3b970..abd22001 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -82,6 +82,23 @@ Definition dummy_float_reg := X0.   (**r Used in [Regalloc]. *)
 
 Definition callee_save_type := mreg_type.
 
+(** 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