aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/TargetPrinter.ml8
-rw-r--r--backend/PrintAsm.ml8
-rw-r--r--backend/PrintAsmaux.ml24
-rw-r--r--ia32/TargetPrinter.ml23
-rw-r--r--powerpc/TargetPrinter.ml23
5 files changed, 50 insertions, 36 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 7eb01084..1d37d237 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -44,10 +44,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
(* Basic printing functions *)
- let print_label oc lbl = label oc (transl_label lbl)
+ let print_label oc lbl = elf_label oc (transl_label lbl)
let comment = "@"
+ let symbol = elf_symbol
+
let symbol_offset oc (symb, ofs) =
symbol oc symb;
let ofs = camlint_of_coqint ofs in
@@ -1058,9 +1060,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
if !Clflags.option_mthumb then
fprintf oc " .thumb_func\n"
- let print_fun_info = print_fun_info
+ let print_fun_info = elf_print_fun_info
- let print_var_info = print_var_info
+ let print_var_info = elf_print_var_info
let print_comm_symb oc sz name align =
if C2C.atom_is_static name then
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index fb03d96b..c356d7e5 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -37,9 +37,9 @@ module Printer(Target:TARGET) =
match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in
Target.print_align oc alignment;
if not (C2C.atom_is_static name) then
- fprintf oc " .globl %a\n" symbol name;
+ fprintf oc " .globl %a\n" Target.symbol name;
Target.print_optional_fun_info oc;
- fprintf oc "%a:\n" symbol name;
+ fprintf oc "%a:\n" Target.symbol name;
print_location oc (C2C.atom_location name);
Target.cfi_startproc oc;
Target.print_instructions oc fn;
@@ -74,8 +74,8 @@ module Printer(Target:TARGET) =
fprintf oc " %s\n" name_sec;
Target.print_align oc align;
if not (C2C.atom_is_static name) then
- fprintf oc " .global %a\n" symbol name;
- fprintf oc "%a:\n" symbol name;
+ fprintf oc " .global %a\n" Target.symbol name;
+ fprintf oc "%a:\n" Target.symbol name;
print_init_data oc name v.gvar_init;
Target.print_var_info oc name;
end else
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index f3d95f87..925add9e 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -41,6 +41,7 @@ module type TARGET =
val section: out_channel -> section_name -> unit
val name_of_section: section_name -> string
val comment: string
+ val symbol: out_channel -> P.t -> unit
end
(* On-the-fly label renaming *)
@@ -60,7 +61,7 @@ let transl_label lbl =
Hashtbl.add current_function_labels lbl lbl';
lbl'
-let label oc lbl =
+let elf_label oc lbl =
fprintf oc ".L%d" lbl
(* List of literals and jumptables used in the code *)
@@ -81,25 +82,22 @@ let current_function_sig =
ref { sig_args = []; sig_res = None; sig_cc = cc_default }
(* Functions for printing of symbol names *)
-let symbol oc symb =
+let elf_symbol oc symb =
fprintf oc "%s" (extern_atom symb)
-let symbol_offset oc (symb, ofs) =
- symbol oc symb;
+let elf_symbol_offset oc (symb, ofs) =
+ elf_symbol oc symb;
let ofs = camlint_of_coqint ofs in
if ofs <> 0l then fprintf oc " + %ld" ofs
-(* The comment deliminiter *)
-let comment = "#"
-
(* Functions for fun and var info *)
-let print_fun_info oc name =
- fprintf oc " .type %a, @function\n" symbol name;
- fprintf oc " .size %a, . - %a\n" symbol name symbol name
+let elf_print_fun_info oc name =
+ fprintf oc " .type %a, @function\n" elf_symbol name;
+ fprintf oc " .size %a, . - %a\n" elf_symbol name elf_symbol name
-let print_var_info oc name =
- fprintf oc " .type %a, @object\n" symbol name;
- fprintf oc " .size %a, . - %a\n" symbol name symbol name
+let elf_print_var_info oc name =
+ fprintf oc " .type %a, @object\n" elf_symbol name;
+ fprintf oc " .size %a, . - %a\n" elf_symbol name elf_symbol name
(* Emit .cfi directives *)
let cfi_startproc =
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 6de53025..55abe3b7 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -56,6 +56,8 @@ let preg oc = function
| FR r -> freg oc r
| _ -> assert false
+(* The comment deliminiter *)
+let comment = "#"
(* System dependend printer functions *)
module type SYSTEM =
@@ -81,7 +83,7 @@ module Cygwin_System : SYSTEM =
let raw_symbol oc s =
fprintf oc "_%s" s
- let symbol = symbol
+ let symbol = elf_symbol
let label oc lbl =
fprintf oc "L%d" lbl
@@ -129,9 +131,9 @@ module ELF_System : SYSTEM =
let raw_symbol oc s =
fprintf oc "%s" s
- let symbol = symbol
+ let symbol = elf_symbol
- let label = label
+ let label = elf_label
let name_of_section = function
| Section_text -> ".text"
@@ -154,9 +156,9 @@ module ELF_System : SYSTEM =
let print_mov_ra oc rd id =
fprintf oc " movl $%a, %a\n" symbol id ireg rd
- let print_fun_info = print_fun_info
+ let print_fun_info = elf_print_fun_info
- let print_var_info = print_var_info
+ let print_var_info = elf_print_var_info
let print_epilogue _ = ()
@@ -239,8 +241,9 @@ module MacOS_System : SYSTEM =
module Target(System: SYSTEM):TARGET =
- (struct
+ struct
open System
+ let symbol = symbol
(* Basic printing functions *)
@@ -914,8 +917,6 @@ module Target(System: SYSTEM):TARGET =
then System.print_lcomm_decl oc name sz align
else System.print_comm_decl oc name sz align
- let comment = comment
-
let name_of_section = name_of_section
let emit_constants oc lit =
@@ -963,8 +964,10 @@ module Target(System: SYSTEM):TARGET =
fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n"
raw_symbol "__abss_mask"
end;
- System.print_epilogue oc;
-end)
+ System.print_epilogue oc
+
+ let comment = comment
+end
let sel_target () =
let module S = (val (match Configuration.system with
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index e9c64ffc..964f75a7 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -26,6 +26,7 @@ open PrintAsmaux
module type SYSTEM =
sig
+ val comment: string
val constant: out_channel -> constant -> unit
val ireg: out_channel -> ireg -> unit
val freg: out_channel -> freg -> unit
@@ -39,6 +40,10 @@ module type SYSTEM =
val print_prologue: out_channel -> unit
end
+let symbol = elf_symbol
+
+let symbol_offset = elf_symbol_offset
+
let symbol_fragment oc s n op =
fprintf oc "(%a)%s" symbol_offset (s, n) op
@@ -66,6 +71,8 @@ let float_reg_name = function
module Linux_System : SYSTEM =
struct
+ let comment = "#"
+
let constant oc cst =
match cst with
| Cint n ->
@@ -129,7 +136,9 @@ module Linux_System : SYSTEM =
module Diab_System : SYSTEM =
struct
-
+
+ let comment = ";"
+
let constant oc cst =
match cst with
| Cint n ->
@@ -198,10 +207,13 @@ module Target (System : SYSTEM):TARGET =
include System
(* Basic printing functions *)
-
+ let symbol = symbol
+
let raw_symbol oc s =
fprintf oc "%s" s
+ let label = elf_label
+
let label_low oc lbl =
fprintf oc ".L%d@l" lbl
@@ -681,9 +693,8 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " .long %a\n"
symbol_offset (symb, ofs)
- let comment = comment
-
- let print_fun_info = print_fun_info
+
+ let print_fun_info = elf_print_fun_info
let emit_constants oc lit =
if !float64_literals <> [] || !float32_literals <> [] then begin
@@ -703,7 +714,7 @@ module Target (System : SYSTEM):TARGET =
let reset_constants = reset_constants
- let print_var_info = print_var_info
+ let print_var_info = elf_print_var_info
let print_comm_symb oc sz name align =
fprintf oc " %s %a, %s, %d\n"
generated by cgit (git 2.34.1) at 2024-06-02 22:01:13 +0000