From ab617cf8e6e60e8de3eb8de220f71dd05c18209f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 27 Apr 2023 16:32:13 +0100 Subject: Update verilog back end with new x86 changes --- verilog/TargetPrinter.ml | 158 ++++++++++++++++++++++++++++++++++++----------- 1 file changed, 123 insertions(+), 35 deletions(-) (limited to 'verilog/TargetPrinter.ml') 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) -- cgit