From d5fda4fde03571e6dbc46729767924be7ac41920 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 25 Aug 2022 15:49:21 +0200 Subject: 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. --- aarch64/TargetPrinter.ml | 5 ----- backend/PrintAsm.ml | 28 ++++++++++++++++------------ backend/PrintAsmaux.ml | 1 - powerpc/TargetPrinter.ml | 5 ----- riscV/TargetPrinter.ml | 5 ----- x86/TargetPrinter.ml | 3 --- 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 = -- cgit