aboutsummaryrefslogtreecommitdiffstats
path: root/verilog/TargetPrinter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'verilog/TargetPrinter.ml')
-rw-r--r--verilog/TargetPrinter.ml158
1 files changed, 123 insertions, 35 deletions
diff --git a/verilog/TargetPrinter.ml b/verilog/TargetPrinter.ml
index 8950b8ca..91e0b18e 100644
--- a/verilog/TargetPrinter.ml
+++ b/verilog/TargetPrinter.ml
@@ -95,9 +95,6 @@ let z oc n = output_string oc (Z.to_string n)
let data_pointer = if Archi.ptr64 then ".quad" else ".long"
-(* The comment deliminiter *)
-let comment = "#"
-
(* Base-2 log of a Caml integer *)
let rec log2 n =
assert (n > 0);
@@ -106,6 +103,7 @@ let rec log2 n =
(* System dependent printer functions *)
module type SYSTEM =
sig
+ val comment: string
val raw_symbol: out_channel -> string -> unit
val symbol: out_channel -> P.t -> unit
val label: out_channel -> int -> unit
@@ -124,6 +122,9 @@ module type SYSTEM =
module ELF_System : SYSTEM =
struct
+ (* The comment delimiter *)
+ let comment = "#"
+
let raw_symbol oc s =
fprintf oc "%s" s
@@ -131,7 +132,30 @@ module ELF_System : SYSTEM =
let label = elf_label
- let name_of_section = fun _ -> assert false
+ let name_of_section = function
+ | Section_text -> ".text"
+ | Section_data i | Section_small_data i ->
+ variable_section ~sec:".data" ~bss:".bss" i
+ | Section_const i | Section_small_const i ->
+ variable_section
+ ~sec:".section .rodata"
+ ~reloc:".section .data.rel.ro,\"aw\",@progbits"
+ i
+ | Section_string sz ->
+ elf_mergeable_string_section sz ".section .rodata"
+ | Section_literal sz ->
+ elf_mergeable_literal_section sz ".section .rodata"
+ | Section_jumptable -> ".text"
+ | Section_user(s, wr, ex) ->
+ sprintf ".section \"%s\",\"a%s%s\",@progbits"
+ s (if wr then "w" else "") (if ex then "x" else "")
+ | Section_debug_info _ -> ".section .debug_info,\"\",@progbits"
+ | Section_debug_loc -> ".section .debug_loc,\"\",@progbits"
+ | Section_debug_line _ -> ".section .debug_line,\"\",@progbits"
+ | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits"
+ | Section_debug_ranges -> ".section .debug_ranges,\"\",@progbits"
+ | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1"
+ | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note"
let stack_alignment = 16
@@ -162,6 +186,10 @@ module ELF_System : SYSTEM =
module MacOS_System : SYSTEM =
struct
+ (* The comment delimiter.
+ `##` instead of `#` to please the Clang assembler. *)
+ let comment = "##"
+
let raw_symbol oc s =
fprintf oc "_%s" s
@@ -171,7 +199,28 @@ module MacOS_System : SYSTEM =
let label oc lbl =
fprintf oc "L%d" lbl
- let name_of_section = fun _ -> assert false
+ let name_of_section = function
+ | Section_text -> ".text"
+ | Section_data i | Section_small_data i ->
+ variable_section ~sec:".data" i
+ | Section_const i | Section_small_const i ->
+ variable_section ~sec:".const" ~reloc:".const_data" i
+ | Section_string sz ->
+ macos_mergeable_string_section sz
+ | Section_literal sz ->
+ macos_mergeable_literal_section sz
+ | Section_jumptable -> ".text"
+ | Section_user(s, wr, ex) ->
+ sprintf ".section \"%s\", %s, %s"
+ (if wr then "__DATA" else "__TEXT") s
+ (if ex then "regular, pure_instructions" else "regular")
+ | Section_debug_info _ -> ".section __DWARF,__debug_info,regular,debug"
+ | Section_debug_loc -> ".section __DWARF,__debug_loc,regular,debug"
+ | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug"
+ | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug"
+ | Section_debug_ranges -> ".section __DWARF,__debug_ranges,regular,debug"
+ | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug"
+ | Section_ais_annotation -> assert false (* Not supported under MacOS *)
let stack_alignment = 16 (* mandatory *)
@@ -202,8 +251,13 @@ module MacOS_System : SYSTEM =
module Cygwin_System : SYSTEM =
struct
+ (* The comment delimiter *)
+ let comment = "#"
+
+ let symbol_prefix = ""
+
let raw_symbol oc s =
- fprintf oc "_%s" s
+ fprintf oc "%s%s" symbol_prefix s
let symbol oc symb =
raw_symbol oc (extern_atom symb)
@@ -211,21 +265,53 @@ module Cygwin_System : SYSTEM =
let label oc lbl =
fprintf oc "L%d" lbl
- let name_of_section = fun _ -> assert false
-
- let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
+ let name_of_section = function
+ | Section_text -> ".text"
+ | Section_data i | Section_small_data i ->
+ variable_section ~sec:".data" ~bss:".bss" i
+ | Section_const i | Section_small_const i ->
+ variable_section ~sec:".section .rdata,\"dr\"" i
+ | Section_string _ -> ".section .rdata,\"dr\""
+ | Section_literal _ -> ".section .rdata,\"dr\""
+ | Section_jumptable -> ".text"
+ | Section_user(s, wr, ex) ->
+ sprintf ".section %s, \"%s\"\n"
+ s (if ex then "xr" else if wr then "d" else "dr")
+ | Section_debug_info _ -> ".section .debug_info,\"dr\""
+ | Section_debug_loc -> ".section .debug_loc,\"dr\""
+ | Section_debug_line _ -> ".section .debug_line,\"dr\""
+ | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\""
+ | Section_debug_ranges -> ".section .debug_ranges,\"dr\""
+ | Section_debug_str-> assert false (* Should not be used *)
+ | Section_ais_annotation -> assert false (* Not supported for coff binaries *)
+
+ let stack_alignment = 8
let print_align oc n =
fprintf oc " .balign %d\n" n
+ let indirect_symbols : StringSet.t ref = ref StringSet.empty
+
let print_mov_rs oc rd id =
- fprintf oc " movl $%a, %a\n" symbol id ireg rd
+ assert Archi.ptr64;
+ let s = extern_atom id in
+ indirect_symbols := StringSet.add s !indirect_symbols;
+ fprintf oc " movq .refptr.%s(%%rip), %a\n" s ireg rd
let print_fun_info _ _ = ()
let print_var_info _ _ = ()
- let print_epilogue _ = ()
+ let declare_indirect_symbol oc s =
+ fprintf oc " .section .rdata$.refptr.%s, \"dr\"\n" s;
+ fprintf oc " .globl .refptr.%s\n" s;
+ fprintf oc " .linkonce discard\n";
+ fprintf oc ".refptr.%s:\n" s;
+ fprintf oc " .quad %s\n" s
+
+ let print_epilogue oc =
+ StringSet.iter (declare_indirect_symbol oc) !indirect_symbols;
+ indirect_symbols := StringSet.empty
let print_comm_decl oc name sz al =
fprintf oc " .comm %a, %s, %d\n"
@@ -233,7 +319,8 @@ module Cygwin_System : SYSTEM =
let print_lcomm_decl oc name sz al =
fprintf oc " .lcomm %a, %s, %d\n"
- symbol name (Z.to_string sz) (log2 al)
+ symbol name (Z.to_string sz)
+ (if Archi.ptr64 then al else log2 al)
end
@@ -345,7 +432,9 @@ module Target(System: SYSTEM):TARGET =
| Pmovq_ri(rd, n) ->
let n1 = camlint64_of_coqint n in
let n2 = Int64.to_int32 n1 in
- if n1 = Int64.of_int32 n2 then
+ if Int64.shift_right_logical n1 32 = Int64.zero then
+ fprintf oc " movl $%Ld, %a\n" n1 ireg32 rd
+ else if n1 = Int64.of_int32 n2 then
fprintf oc " movq $%ld, %a\n" n2 ireg64 rd
else
fprintf oc " movabsq $%Ld, %a\n" n1 ireg64 rd
@@ -654,7 +743,7 @@ module Target(System: SYSTEM):TARGET =
| Pret ->
if (not Archi.ptr64)
&& (!current_function_sig).sig_cc.cc_structret then begin
- fprintf oc " movl 0(%%esp), %%eax\n";
+ fprintf oc " movl 4(%%esp), %%eax\n";
fprintf oc " ret $4\n"
end else begin
fprintf oc " ret\n"
@@ -714,6 +803,8 @@ module Target(System: SYSTEM):TARGET =
fprintf oc " minsd %a, %a\n" freg a1 freg res
| Pmovb_rm (rd,a) ->
fprintf oc " movb %a, %a\n" addressing a ireg8 rd
+ | Pmovq_rf (rd, r1) ->
+ fprintf oc " movq %a, %a\n" freg r1 ireg64 rd
| Pmovsq_mr(a, rs) ->
fprintf oc " movq %a, %a\n" freg rs addressing a
| Pmovsq_rm(rd, a) ->
@@ -765,11 +856,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_literal32 oc n lbl =
- fprintf oc "%a: .long 0x%lx\n" label lbl n
-
let print_jumptable oc jmptbl =
let print_jumptable (lbl, tbl) =
let print_entry l =
@@ -797,15 +883,6 @@ module Target(System: SYSTEM):TARGET =
let name_of_section = name_of_section
- let emit_constants oc lit =
- if exists_constants () then begin
- section oc lit;
- print_align oc 8;
- Hashtbl.iter (print_literal64 oc) literal64_labels;
- Hashtbl.iter (print_literal32 oc) literal32_labels;
- reset_literals ()
- end
-
let cfi_startproc = cfi_startproc
let cfi_endproc = cfi_endproc
@@ -815,11 +892,6 @@ module Target(System: SYSTEM):TARGET =
let print_optional_fun_info _ = ()
- let get_section_names name =
- match C2C.atom_sections name with
- | [t;l;j] -> (t, l, j)
- | _ -> (Section_text, Section_literal, Section_jumptable)
-
let print_fun_info = print_fun_info
let print_var_info = print_var_info
@@ -832,7 +904,23 @@ module Target(System: SYSTEM):TARGET =
end
let print_epilogue oc =
- assert false
+ if !need_masks then begin
+ section oc (Section_literal 16);
+ print_align oc 16;
+ fprintf oc "%a: .quad 0x8000000000000000, 0\n"
+ raw_symbol "__negd_mask";
+ fprintf oc "%a: .quad 0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n"
+ raw_symbol "__absd_mask";
+ fprintf oc "%a: .long 0x80000000, 0, 0, 0\n"
+ raw_symbol "__negs_mask";
+ fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n"
+ raw_symbol "__abss_mask"
+ end;
+ System.print_epilogue oc;
+ if !Clflags.option_g then begin
+ Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
+ section oc Section_text;
+ end
let comment = comment
@@ -847,7 +935,7 @@ end
let sel_target () =
let module S = (val (match Configuration.system with
| "linux" | "bsd" -> (module ELF_System:SYSTEM)
- | "macosx" -> (module MacOS_System:SYSTEM)
+ | "macos" -> (module MacOS_System:SYSTEM)
| "cygwin" -> (module Cygwin_System:SYSTEM)
| _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") ):SYSTEM) in
(module Target(S):TARGET)
generated by cgit (git 2.34.1) at 2024-05-08 23:33:54 +0000