diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-08-25 15:49:21 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-03 10:41:30 +0200 |
| commit | d5fda4fde03571e6dbc46729767924be7ac41920 (patch) | |
| tree | e69a0b4b4b6ee32b0fa8f655194f024739405cbd /backend | |
| parent | ad6467099ac7147040c59c022635e61370168568 (diff) | |
| download | compcert-d5fda4fde03571e6dbc46729767924be7ac41920.tar.gz compcert-d5fda4fde03571e6dbc46729767924be7ac41920.zip | |
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.
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/PrintAsm.ml | 28 | ||||
| -rw-r--r-- | backend/PrintAsmaux.ml | 1 |
2 files changed, 16 insertions, 13 deletions
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 |