Move shared code in new file.

The name_of_register and register_of_name function are shared between
all architectures and can be moved in a common file.

17 files changed, 46 insertions, 96 deletions

diff --git a/aarch64/Machregsaux.ml b/aarch64/Machregsaux.ml
index 7d233041..5f3c1a8d 100644
--- a/aarch64/Machregsaux.ml
+++ b/aarch64/Machregsaux.ml
@@ -12,22 +12,5 @@
 
 (** Auxiliary functions on machine registers *)
 
-open Camlcoq
-open Machregs
-
-let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
-
-let _ =
-  List.iter
-    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
-    Machregs.register_names
-
 let is_scratch_register s =
   s = "X16" || s = "x16" || s = "X30" || s = "x30"
-
-
-let name_of_register r =
-  Hashtbl.find_opt register_names r
-
-let register_by_name s =
-  Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml
index 7d278613..a4624a9d 100644
--- a/arm/Machregsaux.ml
+++ b/arm/Machregsaux.ml
@@ -12,20 +12,4 @@
 
 (** Auxiliary functions on machine registers *)
 
-open Camlcoq
-open Machregs
-
-let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
-
-let _ =
-  List.iter
-    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
-    Machregs.register_names
-
 let is_scratch_register s =  s = "R14"  || s = "r14"
-
-let name_of_register r =
-  Hashtbl.find_opt register_names r
-
-let register_by_name s =
-  Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli
index 884100bb..f3d52849 100644
--- a/arm/Machregsaux.mli
+++ b/arm/Machregsaux.mli
@@ -12,6 +12,4 @@
 
 (** Auxiliary functions on machine registers *)
 
-val name_of_register: Machregs.mreg -> string option
-val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
diff --git a/backend/IRC.ml b/backend/IRC.ml
index e94d6fbb..ed5ae186 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -101,7 +101,7 @@ after IRC elimination, when assigning a stack slot to a spilled variable. *)
 
 let name_of_loc = function
   | R r ->
-      begin match Machregsaux.name_of_register r with
+      begin match Machregsnames.name_of_register r with
                 | None -> "fixed-reg"
                 | Some s -> s
       end
diff --git a/backend/Machregsnames.ml b/backend/Machregsnames.ml
new file mode 100644
index 00000000..fdcbd0e5
--- /dev/null
+++ b/backend/Machregsnames.ml
@@ -0,0 +1,24 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+let register_names : (Machregs.mreg, string) Hashtbl.t = Hashtbl.create 31
+
+let _ =
+  List.iter
+    (fun (s, r) -> Hashtbl.add register_names r (Camlcoq.camlstring_of_coqstring s))
+    Machregs.register_names
+
+let name_of_register r =
+  Hashtbl.find_opt register_names r
+
+let register_by_name s =
+  Machregs.register_by_name (Camlcoq.coqstring_uppercase_ascii_of_camlstring s)
diff --git a/backend/Machregsnames.mli b/backend/Machregsnames.mli
new file mode 100644
index 00000000..1b600d35
--- /dev/null
+++ b/backend/Machregsnames.mli
@@ -0,0 +1,16 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Auxiliary functions on machine registers *)
+
+val name_of_register: Machregs.mreg -> string option
+val register_by_name: string -> Machregs.mreg option
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index 1c449e74..d75ba19c 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -22,7 +22,7 @@ open PrintAST
 open PrintOp
 
 let mreg pp r =
-  match Machregsaux.name_of_register r with
+  match Machregsnames.name_of_register r with
   | Some s -> fprintf pp "%s" s
   | None -> fprintf pp "<unknown machreg>"
 
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index 517f3037..8a5f9a7c 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -16,12 +16,11 @@ open Printf
 open Camlcoq
 open Datatypes
 open AST
-open Machregsaux
 open Mach
 open PrintAST
 
 let reg pp r =
-  match name_of_register r with
+  match Machregsnames.name_of_register r with
   | Some s -> fprintf pp "%s" s
   | None -> fprintf pp "<unknown reg>"
 
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index 6432682a..aeaef25e 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -22,7 +22,7 @@ open PrintOp
 open XTL
 
 let mreg pp r =
-  match Machregsaux.name_of_register r with
+  match Machregsnames.name_of_register r with
   | Some s -> fprintf pp "%s" s
   | None -> fprintf pp "<unknown machreg>"
 
diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index 92cf4cec..22ab2b5a 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -52,7 +52,7 @@ let process_use_section_pragma classname id =
 let reserved_registers = ref ([]: Machregs.mreg list)
 
 let process_reserve_register_pragma name =
-  match Machregsaux.register_by_name name with
+  match Machregsnames.register_by_name name with
   | None ->
       C2C.error "unknown register in `reserve_register' pragma"
   | Some r ->
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index 257e9cf7..df2da2a2 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -156,7 +156,7 @@ let transf_outputs loc env = function
 let check_clobbers loc clob =
   List.iter
     (fun c ->
-      if Machregsaux.register_by_name c <> None
+      if Machregsnames.register_by_name c <> None
       || Machregsaux.is_scratch_register c
       || c = "memory" || c = "cc" (* GCC does not accept MEMORY or CC *)
       then ()
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index 40c993fd..9d3a2243 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -12,20 +12,4 @@
 
 (** Auxiliary functions on machine registers *)
 
-open Camlcoq
-open Machregs
-
-let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
-
-let _ =
-  List.iter
-    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
-    Machregs.register_names
-
 let is_scratch_register s = s = "R0" || s = "r0"
-
-let name_of_register r =
-  Hashtbl.find_opt register_names r
-
-let register_by_name s =
-  Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index 884100bb..f3d52849 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/Machregsaux.mli
@@ -12,6 +12,4 @@
 
 (** Auxiliary functions on machine registers *)
 
-val name_of_register: Machregs.mreg -> string option
-val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
diff --git a/riscV/Machregsaux.ml b/riscV/Machregsaux.ml
index a273bb51..a48749a5 100644
--- a/riscV/Machregsaux.ml
+++ b/riscV/Machregsaux.ml
@@ -12,20 +12,4 @@
 
 (** Auxiliary functions on machine registers *)
 
-open Camlcoq
-open Machregs
-
-let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
-
-let _ =
-  List.iter
-    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
-    Machregs.register_names
-
 let is_scratch_register r = false
-
-let name_of_register r =
-  Hashtbl.find_opt register_names r
-
-let register_by_name s =
-  Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
diff --git a/riscV/Machregsaux.mli b/riscV/Machregsaux.mli
index 884100bb..f3d52849 100644
--- a/riscV/Machregsaux.mli
+++ b/riscV/Machregsaux.mli
@@ -12,6 +12,4 @@
 
 (** Auxiliary functions on machine registers *)
 
-val name_of_register: Machregs.mreg -> string option
-val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
diff --git a/x86/Machregsaux.ml b/x86/Machregsaux.ml
index a273bb51..a48749a5 100644
--- a/x86/Machregsaux.ml
+++ b/x86/Machregsaux.ml
@@ -12,20 +12,4 @@
 
 (** Auxiliary functions on machine registers *)
 
-open Camlcoq
-open Machregs
-
-let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
-
-let _ =
-  List.iter
-    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
-    Machregs.register_names
-
 let is_scratch_register r = false
-
-let name_of_register r =
-  Hashtbl.find_opt register_names r
-
-let register_by_name s =
-  Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
diff --git a/x86/Machregsaux.mli b/x86/Machregsaux.mli
index 884100bb..f3d52849 100644
--- a/x86/Machregsaux.mli
+++ b/x86/Machregsaux.mli
@@ -12,6 +12,4 @@
 
 (** Auxiliary functions on machine registers *)
 
-val name_of_register: Machregs.mreg -> string option
-val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool