try to be portable across archs

14 files changed, 43 insertions, 11 deletions

diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml
index ce5c67f6..14c75155 100644
--- a/arm/Machregsaux.ml
+++ b/arm/Machregsaux.ml
@@ -33,3 +33,8 @@ let register_by_name s =
 let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
+                                              
+let class_of_type = function
+  | AST.Tint | AST.Tlong -> 0
+  | AST.Tfloat | AST.Tsingle -> 1
+  | AST.Tany32 | AST.Tany64 -> assert false
diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli
index 9404568d..d7117c21 100644
--- a/arm/Machregsaux.mli
+++ b/arm/Machregsaux.mli
@@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
 val can_reserve_register: Machregs.mreg -> bool
+
+val class_of_type: AST.typ -> int
diff --git a/backend/IRC.ml b/backend/IRC.ml
index c7b1bf04..67da47da 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -15,6 +15,7 @@ open Camlcoq
 open AST
 open Registers
 open Machregs
+open Machregsaux
 open Locations
 open Conventions1
 open XTL
@@ -237,13 +238,9 @@ type graph = {
    according to their types.  A variable can be forced into class 2
    by giving it a negative spill cost. *)
 
-let class_of_type = function
-  | Tint | Tlong -> 0
-  | Tfloat | Tsingle -> 0 (* normal: 1 *)
-  | Tany32 | Tany64 -> assert false
 
-let class_of_reg r = 0
-  (* normal: if Conventions1.is_float_reg r then 1 else 0 *)
+let class_of_reg r =
+  if Conventions1.is_float_reg r then 1 else 0
 
 let class_of_loc = function
   | R r -> class_of_reg r
diff --git a/backend/IRC.mli b/backend/IRC.mli
index 30b6d5c1..f7bbf9c5 100644
--- a/backend/IRC.mli
+++ b/backend/IRC.mli
@@ -43,5 +43,4 @@ val coloring: graph -> (var -> loc)
 val reserved_registers: mreg list ref
 
 (* Auxiliaries to deal with register classes *)
-val class_of_type: AST.typ -> int
 val class_of_loc: loc -> int
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 19aba4f6..7db8a866 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -1067,7 +1067,7 @@ let make_parmove srcs dsts itmp ftmp k =
     | Locations.S(sl, ofs, ty), R rd ->
         code := LTL.Lgetstack(sl, ofs, ty, rd) :: !code
     | Locations.S(sls, ofss, tys), Locations.S(sld, ofsd, tyd) ->
-        let tmp = temp_for (class_of_type tys) in
+        let tmp = temp_for (Machregsaux.class_of_type tys) in
         (* code will be reversed at the end *)
         code := LTL.Lsetstack(tmp, sld, ofsd, tyd) ::
                 LTL.Lgetstack(sls, ofss, tys, tmp) :: !code
diff --git a/mppa_k1c/Machregsaux.ml b/mppa_k1c/Machregsaux.ml
index 473e0602..9c4175ed 100644
--- a/mppa_k1c/Machregsaux.ml
+++ b/mppa_k1c/Machregsaux.ml
@@ -31,3 +31,8 @@ let register_by_name s =
   Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
 
 let can_reserve_register r = Conventions1.is_callee_save r
+
+let class_of_type = function
+  | AST.Tint | AST.Tlong 
+  | AST.Tfloat | AST.Tsingle -> 0
+  | AST.Tany32 | AST.Tany64 -> assert false
diff --git a/mppa_k1c/Machregsaux.mli b/mppa_k1c/Machregsaux.mli
index 9404568d..d7117c21 100644
--- a/mppa_k1c/Machregsaux.mli
+++ b/mppa_k1c/Machregsaux.mli
@@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
 val can_reserve_register: Machregs.mreg -> bool
+
+val class_of_type: AST.typ -> int
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index 664f71a0..0b0d4548 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -33,3 +33,8 @@ let register_by_name s =
 let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
+                                              
+let class_of_type = function
+  | AST.Tint | AST.Tlong -> 0
+  | AST.Tfloat | AST.Tsingle -> 1
+  | AST.Tany32 | AST.Tany64 -> assert false
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index 9404568d..d7117c21 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/Machregsaux.mli
@@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
 val can_reserve_register: Machregs.mreg -> bool
+
+val class_of_type: AST.typ -> int
diff --git a/riscV/Machregsaux.ml b/riscV/Machregsaux.ml
index 473e0602..07097eaf 100644
--- a/riscV/Machregsaux.ml
+++ b/riscV/Machregsaux.ml
@@ -31,3 +31,8 @@ let register_by_name s =
   Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
 
 let can_reserve_register r = Conventions1.is_callee_save r
+                                              
+let class_of_type = function
+  | AST.Tint | AST.Tlong -> 0
+  | AST.Tfloat | AST.Tsingle -> 1
+  | AST.Tany32 | AST.Tany64 -> assert false
diff --git a/riscV/Machregsaux.mli b/riscV/Machregsaux.mli
index 9404568d..d7117c21 100644
--- a/riscV/Machregsaux.mli
+++ b/riscV/Machregsaux.mli
@@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
 val can_reserve_register: Machregs.mreg -> bool
+
+val class_of_type: AST.typ -> int
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index 646c4afb..35d555f9 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -15,6 +15,7 @@
 
 Require Import Coqlib Decidableplus.
 Require Import AST Machregs Locations.
+Require Import Errors.
 
 (** * Classification of machine registers *)
 
@@ -26,7 +27,7 @@ Require Import AST Machregs Locations.
   We follow the x86-32 and x86-64 application binary interfaces (ABI)
   in our choice of callee- and caller-save registers.
 *)
-
+  
 Definition is_callee_save (r: mreg) : bool :=
   match r with
   | AX | CX | DX => false
diff --git a/x86/Machregsaux.ml b/x86/Machregsaux.ml
index 473e0602..80066b00 100644
--- a/x86/Machregsaux.ml
+++ b/x86/Machregsaux.ml
@@ -14,9 +14,9 @@
 
 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))
@@ -31,3 +31,8 @@ let register_by_name s =
   Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
 
 let can_reserve_register r = Conventions1.is_callee_save r
+                                              
+let class_of_type = function
+  | AST.Tint | AST.Tlong -> 0
+  | AST.Tfloat | AST.Tsingle -> 1
+  | AST.Tany32 | AST.Tany64 -> assert false
diff --git a/x86/Machregsaux.mli b/x86/Machregsaux.mli
index 9404568d..d7117c21 100644
--- a/x86/Machregsaux.mli
+++ b/x86/Machregsaux.mli
@@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
 val can_reserve_register: Machregs.mreg -> bool
+
+val class_of_type: AST.typ -> int