Refactor emitting of constants.

The function was the same for nearly all backends and also the way 32 bit
literals are printed so we moved it to PrintAsm. The 64 bit literals
however are still target specific.

7 files changed, 21 insertions, 76 deletions

diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index ce6c51fc..b2858e2e 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -274,24 +274,10 @@ module Target(System: SYSTEM): TARGET =
     let section oc sec =
       fprintf oc "	%s\n" (name_of_section sec)
 
-(* Associate labels to floating-point constants and to symbols. *)
-
-    let emit_constants oc lit =
-      if Hashtbl.length literal64_labels > 0 then begin
-        section oc (Sections.with_size 8 lit);
-        fprintf oc "	.balign 8\n";
-        Hashtbl.iter
-          (fun bf lbl -> fprintf oc "%a:	.quad	0x%Lx\n" label lbl bf)
-          literal64_labels
-      end;
-      if Hashtbl.length literal32_labels > 0 then begin
-        section oc (Sections.with_size 4 lit);
-        fprintf oc "	.balign 4\n";
-        Hashtbl.iter
-          (fun bf lbl -> fprintf oc "%a:	.long	0x%lx\n" label lbl bf)
-          literal32_labels
-      end;
-      reset_literals ()
+(* Printing floating-point constants. *)
+
+    let print_literal64 oc n lbl =
+      fprintf oc "%a:	.quad	0x%Lx\n" label lbl n
 
 (* Emit .file / .loc debugging directives *)
 
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 57359f11..20ca59d6 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -562,15 +562,6 @@ struct
     current_function_sig := fn.fn_sig;
     List.iter (print_instruction oc) fn.fn_code
 
-
-  let emit_constants oc lit =
-    if not !Constantexpand.literals_in_code && exists_constants () then begin
-      section oc (Sections.with_size 8 lit);
-      fprintf oc "	.balign 4\n";
-      Hashtbl.iter (print_literal64 oc) literal64_labels;
-    end;
-    reset_constants ()
-
   (* Data *)
 
   let print_prologue oc =
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 6d1fafd6..b267dfd8 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -37,6 +37,19 @@ module Printer(Target:TARGET) =
     let print_location oc loc =
       if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc)
 
+    let emit_constants oc lit =
+      if Hashtbl.length literal64_labels > 0 then begin
+        Target.section oc (Sections.with_size 8 lit);
+        Target.print_align oc 8;
+        iter_literal64 (Target.print_literal64 oc)
+      end;
+      if Hashtbl.length literal32_labels > 0 then begin
+        Target.section oc (Sections.with_size 4 lit);
+        Target.print_align oc 4;
+        iter_literal32 (fun n lbl -> fprintf oc "%a:	.long	0x%lx\n" Target.label lbl n);
+      end;
+      reset_literals ()
+
     let get_section_names name =
       match C2C.atom_sections name with
       | [t;l;j] -> (t, l, j)
@@ -65,7 +78,7 @@ module Printer(Target:TARGET) =
       Target.cfi_endproc oc;
       print_debug_label oc e;
       Target.print_fun_info oc name;
-      Target.emit_constants oc lit;
+      emit_constants oc lit;
       Target.print_jumptable oc jmptbl;
       if !Clflags.option_g then
         Hashtbl.iter (fun p i -> Debug.add_label name p i) current_function_labels
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index df2f72f2..2241edfd 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -33,7 +33,7 @@ module type TARGET =
       val cfi_startproc: out_channel -> unit
       val print_instructions: out_channel -> coq_function -> unit
       val cfi_endproc: out_channel -> unit
-      val emit_constants: out_channel -> section_name -> unit
+      val print_literal64 : out_channel -> int64 -> int -> unit
       val print_jumptable: out_channel -> section_name -> unit
       val section: out_channel -> section_name -> unit
       val name_of_section: section_name -> string
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 567b0598..5abf883d 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -915,24 +915,8 @@ module Target (System : SYSTEM):TARGET =
       and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in
       fprintf oc "%a:	.long	0x%lx, 0x%lx\n" label lbl nhi nlo
 
-    let print_literal32 oc n lbl =
-      fprintf oc "%a:	.long	0x%lx\n" label lbl n
-
     let print_fun_info = elf_print_fun_info
 
-    let emit_constants oc lit =
-      if Hashtbl.length literal64_labels > 0 then begin
-        section oc (Sections.with_size 8 lit);
-        fprintf oc "	.balign 8\n";
-        Hashtbl.iter (print_literal64 oc) literal64_labels
-      end;
-      if Hashtbl.length literal32_labels > 0 then begin
-        section oc (Sections.with_size 4 lit);
-        fprintf oc "	.balign 4\n";
-        Hashtbl.iter (print_literal32 oc) literal32_labels
-      end;
-      reset_literals ()
-
     let print_optional_fun_info _ = ()
 
     let print_var_info = elf_print_var_info
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index f86664e9..52a6853a 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -132,22 +132,8 @@ module Target : TARGET =
 
 (* Associate labels to floating-point constants and to symbols. *)
 
-    let emit_constants oc lit =
-      if Hashtbl.length literal64_labels > 0 then begin
-        section oc (Sections.with_size 8 lit);
-        fprintf oc "      .align 3\n";
-        Hashtbl.iter
-          (fun bf lbl -> fprintf oc "%a:	.quad	0x%Lx\n" label lbl bf)
-          literal64_labels
-      end;
-      if Hashtbl.length literal32_labels > 0 then begin
-        section oc (Sections.with_size 4 lit);
-        fprintf oc "      .align 2\n";
-        Hashtbl.iter
-          (fun bf lbl -> fprintf oc "%a:	.long	0x%lx\n" label lbl bf)
-          literal32_labels
-      end;
-      reset_literals ()
+    let print_literal64 oc n lbl =
+      fprintf oc "%a:	.quad	0x%Lx\n" label lbl n
 
 (* Generate code to load the address of id + ofs in register r *)
 
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 9b7490f7..50918bfc 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -860,8 +860,6 @@ module Target(System: SYSTEM):TARGET =
 
     let print_literal64 oc n lbl =
       fprintf oc "%a:	.quad	0x%Lx\n" label lbl n
-    let print_literal32 oc n lbl =
-      fprintf oc "%a:	.long	0x%lx\n" label lbl n
 
     let print_jumptable oc jmptbl =
       let print_jumptable (lbl, tbl) =
@@ -890,19 +888,6 @@ module Target(System: SYSTEM):TARGET =
 
     let name_of_section = name_of_section
 
-    let emit_constants oc lit =
-      if Hashtbl.length literal64_labels > 0 then begin
-        section oc (Sections.with_size 8 lit);
-        print_align oc 8;
-        Hashtbl.iter (print_literal64 oc) literal64_labels
-      end;
-      if Hashtbl.length literal32_labels > 0 then begin
-        section oc (Sections.with_size 4 lit);
-        print_align oc 4;
-        Hashtbl.iter (print_literal32 oc) literal32_labels
-      end;
-      reset_literals ()
-
     let cfi_startproc = cfi_startproc
     let cfi_endproc = cfi_endproc