diff options
| -rw-r--r-- | aarch64/TargetPrinter.ml | 5 | ||||
| -rw-r--r-- | backend/PrintAsm.ml | 28 | ||||
| -rw-r--r-- | backend/PrintAsmaux.ml | 1 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 5 | ||||
| -rw-r--r-- | riscV/TargetPrinter.ml | 5 | ||||
| -rw-r--r-- | 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 = |