aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--aarch64/TargetPrinter.ml22
-rw-r--r--arm/TargetPrinter.ml9
-rw-r--r--backend/PrintAsm.ml15
-rw-r--r--backend/PrintAsmaux.ml2
-rw-r--r--powerpc/TargetPrinter.ml16
-rw-r--r--riscV/TargetPrinter.ml18
-rw-r--r--x86/TargetPrinter.ml15
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
generated by cgit (git 2.34.1) at 2024-05-20 05:38:01 +0000