More simplifications for literal printing

Use the same code to split 64 bit literals into two 32 bit halfs as is
used for 64 bit initialization data and print them in PrintAsm. This
removes the need for a target specific printing function for 64 bit
literals.

6 files changed, 16 insertions, 31 deletions

diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index b2858e2e..cde5668b 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -274,11 +274,6 @@ module Target(System: SYSTEM): TARGET =
     let section oc sec =
       fprintf oc "	%s\n" (name_of_section sec)
 
-(* 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 *)
 
     let print_file_line oc file line =
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index b267dfd8..2bbb5374 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -37,16 +37,27 @@ 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 splitlong b =
+      if Archi.big_endian then
+        (Int64.shift_right_logical b 32),
+        (Int64.logand b 0xFFFFFFFFL)
+      else
+        (Int64.logand b 0xFFFFFFFFL),
+        (Int64.shift_right_logical b 32)
+
     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)
+        iter_literal64 (fun n lbl ->
+            let (hi, lo) = splitlong n in
+            fprintf oc "%a:	.long	0x%Lx, 0x%Lx\n" Target.label lbl hi lo)
       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);
+        iter_literal32 (fun n lbl ->
+            fprintf oc "%a:	.long	0x%lx\n" Target.label lbl n);
       end;
       reset_literals ()
 
@@ -88,14 +99,6 @@ module Printer(Target:TARGET) =
         Target.symbol oc symb;
         let ofs = camlint64_of_ptrofs ofs in
         if ofs <> 0L then fprintf oc " + %Ld" ofs in
-      let splitlong b =
-        let b = camlint64_of_coqint b in
-        if Archi.big_endian then
-          (Int64.shift_right_logical b 32),
-          (Int64.logand b 0xFFFFFFFFL)
-        else
-          (Int64.logand b 0xFFFFFFFFL),
-          (Int64.shift_right_logical b 32) in
       match init with
       | Init_int8 n ->
           fprintf oc "	.byte	%ld\n" (camlint_of_coqint n)
@@ -104,14 +107,15 @@ module Printer(Target:TARGET) =
       | Init_int32 n ->
           fprintf oc "	.long	%ld\n" (camlint_of_coqint n)
       | Init_int64 n ->
-          let hi,lo = splitlong n in
+          let (hi, lo) = splitlong (camlint64_of_coqint n) in
           fprintf oc "	.long	0x%Lx, 0x%Lx\n" hi lo
       | Init_float32 n ->
           fprintf oc "	.long	0x%lx %s %.18g\n"
             (camlint_of_coqint (Floats.Float32.to_bits n))
             Target.comment (camlfloat_of_coqfloat32 n)
       | Init_float64 n ->
-          let hi,lo = splitlong (Floats.Float.to_bits n) in
+          let (hi, lo) =
+            splitlong (camlint64_of_coqint (Floats.Float.to_bits n)) in
           fprintf oc "	.long	0x%Lx, 0x%Lx %s %.18g\n" hi lo
             Target.comment (camlfloat_of_coqfloat n)
       | Init_space n ->
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 2241edfd..f5741113 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -33,7 +33,6 @@ module type TARGET =
       val cfi_startproc: out_channel -> unit
       val print_instructions: out_channel -> coq_function -> unit
       val cfi_endproc: out_channel -> 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 5abf883d..49209501 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -910,11 +910,6 @@ module Target (System : SYSTEM):TARGET =
 
     (* Print the code for a function *)
 
-    let print_literal64 oc n lbl =
-      let nlo = Int64.to_int32 n
-      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_fun_info = elf_print_fun_info
 
     let print_optional_fun_info _ = ()
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 52a6853a..373bd1a5 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -130,11 +130,6 @@ module Target : TARGET =
     let section oc sec =
       fprintf oc "	%s\n" (name_of_section sec)
 
-(* Associate labels to floating-point constants and to symbols. *)
-
-    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 *)
 
     let loadsymbol oc r id ofs =
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 50918bfc..dad8d15c 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -858,9 +858,6 @@ module Target(System: SYSTEM):TARGET =
               assert false
           end
 
-    let print_literal64 oc n lbl =
-      fprintf oc "%a:	.quad	0x%Lx\n" label lbl n
-
     let print_jumptable oc jmptbl =
       let print_jumptable (lbl, tbl) =
         let print_entry l =