From f0867a37e28a1f3670362e7935f9ef30988ddb92 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 17 Sep 2021 18:21:02 +0100 Subject: Fix compilation of verilog back end --- verilog/Asmexpand.ml | 99 +++++++++++++++++++++++++++++++++++------------- verilog/TargetPrinter.ml | 80 ++------------------------------------ 2 files changed, 77 insertions(+), 102 deletions(-) diff --git a/verilog/Asmexpand.ml b/verilog/Asmexpand.ml index caa9775a..1b3961e0 100644 --- a/verilog/Asmexpand.ml +++ b/verilog/Asmexpand.ml @@ -39,12 +39,7 @@ let _16z = Z.of_sint 16 let stack_alignment () = 16 -(* Pseudo instructions for 32/64 bit compatibility *) - -let _Plea (r, addr) = - if Archi.ptr64 then Pleaq (r, addr) else Pleal (r, addr) - -(* SP adjustment to allocate or free a stack frame *) +(* SP adjustment to allocate or free a stack frame. *) let align n a = if n >= 0 then (n + a - 1) land (-a) else n land (-a) @@ -56,7 +51,7 @@ let sp_adjustment_32 sz = (* The top 4 bytes have already been allocated by the "call" instruction. *) sz - 4 -let sp_adjustment_64 sz = +let sp_adjustment_elf64 sz = let sz = Z.to_int sz in if is_current_function_variadic() then begin (* If variadic, add room for register save area, which must be 16-aligned *) @@ -73,6 +68,13 @@ let sp_adjustment_64 sz = (sz - 8, -1) end +let sp_adjustment_win64 sz = + let sz = Z.to_int sz in + (* Preserve proper alignment of the stack *) + let sz = align sz 16 in + (* The top 8 bytes have already been allocated by the "call" instruction. *) + sz - 8 + (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; @@ -102,6 +104,21 @@ let offset_addressing (Addrmode(base, ofs, cst)) delta = let linear_addr reg ofs = Addrmode(Some reg, None, Coq_inl ofs) let global_addr id ofs = Addrmode(None, None, Coq_inr(id, ofs)) +(* A "leaq" instruction that does not overflow *) + +let emit_leaq r addr = + match Asmgen.normalize_addrmode_64 addr with + | (addr, None) -> + emit (Pleaq (r, addr)) + | (addr, Some delta) -> + emit (Pleaq (r, addr)); + emit (Paddq_ri (r, delta)) + +(* Pseudo "lea" instruction for 32/64 bit compatibility *) + +let emit_lea r addr = + if Archi.ptr64 then emit_leaq r addr else emit (Pleal (r, addr)) + (* Translate a builtin argument into an addressing mode *) let addressing_of_builtin_arg = function @@ -143,8 +160,8 @@ let expand_builtin_memcpy_small sz al src dst = copy (addressing_of_builtin_arg src) (addressing_of_builtin_arg dst) sz let expand_builtin_memcpy_big sz al src dst = - if src <> BA (IR RSI) then emit (_Plea (RSI, addressing_of_builtin_arg src)); - if dst <> BA (IR RDI) then emit (_Plea (RDI, addressing_of_builtin_arg dst)); + if src <> BA (IR RSI) then emit_lea RSI (addressing_of_builtin_arg src); + if dst <> BA (IR RDI) then emit_lea RDI (addressing_of_builtin_arg dst); (* TODO: movsq? *) emit (Pmovl_ri (RCX,coqint_of_camlint (Int32.of_int (sz / 4)))); emit Prep_movsl; @@ -256,7 +273,7 @@ let expand_builtin_va_start_32 r = emit (Pleal (RAX, linear_addr RSP (Z.of_uint32 ofs))); emit (Pmovl_mr (linear_addr r _0z, RAX)) -let expand_builtin_va_start_64 r = +let expand_builtin_va_start_elf64 r = if not (is_current_function_variadic ()) then invalid_arg "Fatal error: va_start used in non-vararg function"; let (ir, fr, ofs) = @@ -282,11 +299,22 @@ let expand_builtin_va_start_64 r = emit (Pmovl_mr (linear_addr r _0z, RAX)); emit (Pmovl_ri (RAX, coqint_of_camlint fp_offset)); emit (Pmovl_mr (linear_addr r _4z, RAX)); - emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 overflow_arg_area))); + emit_leaq RAX (linear_addr RSP (Z.of_uint64 overflow_arg_area)); emit (Pmovq_mr (linear_addr r _8z, RAX)); - emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 reg_save_area))); + emit_leaq RAX (linear_addr RSP (Z.of_uint64 reg_save_area)); emit (Pmovq_mr (linear_addr r _16z, RAX)) +let expand_builtin_va_start_win64 r = + if not (is_current_function_variadic ()) then + invalid_arg "Fatal error: va_start used in non-vararg function"; + let num_args = + List.length (get_current_function_args()) in + let ofs = + Int64.(add !current_function_stacksize + (mul 8L (of_int num_args))) in + emit_leaq RAX (linear_addr RSP (Z.of_uint64 ofs)); + emit (Pmovq_mr (linear_addr r _0z, RAX)) + (* FMA operations *) (* vfmadd r1, r2, r3 performs r1 := ri * rj + rk @@ -463,44 +491,63 @@ let expand_builtin_inline name args res = (* Vararg stuff *) | "__builtin_va_start", [BA(IR a)], _ -> assert (a = RDX); - if Archi.ptr64 - then expand_builtin_va_start_64 a + if Archi.ptr64 then expand_builtin_va_start_elf64 a else expand_builtin_va_start_32 a (* Synchronization *) | "__builtin_membar", [], _ -> () - (* no operation *) + (* No operation *) | "__builtin_nop", [], _ -> emit Pnop + (* Optimization hint *) + | "__builtin_unreachable", [], _ -> + () (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) -(* Calls to variadic functions for x86-64: register AL must contain +(* Calls to variadic functions for x86-64 ELF: register AL must contain the number of XMM registers used for parameter passing. To be on - the safe side. do the same if the called function is + the safe side, do the same if the called function is unprototyped. *) -let set_al sg = - if Archi.ptr64 && (sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto) then begin +let fixup_funcall_elf64 sg = + if sg.sig_cc.cc_vararg <> None || sg.sig_cc.cc_unproto then begin let (ir, fr, ofs) = next_arg_locations 0 0 0 sg.sig_args in emit (Pmovl_ri (RAX, coqint_of_camlint (Int32.of_int fr))) end +(* Calls to variadic functions for x86-64 Windows: + FP arguments passed in FP registers must also be passed in integer + registers. +*) + +let copy_fregs_to_iregs args fr ir = + () + +let fixup_funcall_win64 sg = + if sg.sig_cc.cc_vararg <> None then + copy_fregs_to_iregs sg.sig_args [XMM0; XMM1; XMM2; XMM3] [RCX; RDX; R8; R9] + +let fixup_funcall sg = + if Archi.ptr64 then + fixup_funcall_elf64 sg + else () + (* Expansion of instructions *) let expand_instruction instr = match instr with | Pallocframe (sz, ofs_ra, ofs_link) -> - if Archi.ptr64 then begin - let (sz, save_regs) = sp_adjustment_64 sz in + if Archi.ptr64 then begin + let (sz, save_regs) = sp_adjustment_elf64 sz in (* Allocate frame *) let sz' = Z.of_uint sz in emit (Psubq_ri (RSP, sz')); emit (Pcfi_adjust sz'); if save_regs >= 0 then begin (* Save the registers *) - emit (Pleaq (R10, linear_addr RSP (Z.of_uint save_regs))); + emit_leaq R10 (linear_addr RSP (Z.of_uint save_regs)); emit (Pcall_s (intern_string "__compcert_va_saveregs", {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})) end; @@ -508,7 +555,7 @@ let expand_instruction instr = let fullsz = sz + 8 in let addr1 = linear_addr RSP (Z.of_uint fullsz) in let addr2 = linear_addr RSP ofs_link in - emit (Pleaq (RAX, addr1)); + emit_leaq RAX addr1; emit (Pmovq_mr (addr2, RAX)); current_function_stacksize := Int64.of_int fullsz end else begin @@ -525,15 +572,15 @@ let expand_instruction instr = PrintAsmaux.current_function_stacksize := Int32.of_int sz end | Pfreeframe(sz, ofs_ra, ofs_link) -> - if Archi.ptr64 then begin - let (sz, _) = sp_adjustment_64 sz in + if Archi.ptr64 then begin + let (sz, _) = sp_adjustment_elf64 sz in emit (Paddq_ri (RSP, Z.of_uint sz)) end else begin let sz = sp_adjustment_32 sz in emit (Paddl_ri (RSP, Z.of_uint sz)) end | Pjmp_s(_, sg) | Pjmp_r(_, sg) | Pcall_s(_, sg) | Pcall_r(_, sg) -> - set_al sg; + fixup_funcall sg; emit instr | Pbuiltin (ef,args, res) -> begin diff --git a/verilog/TargetPrinter.ml b/verilog/TargetPrinter.ml index f0a54506..8950b8ca 100644 --- a/verilog/TargetPrinter.ml +++ b/verilog/TargetPrinter.ml @@ -131,25 +131,7 @@ module ELF_System : SYSTEM = let label = elf_label - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else common_section () - | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" - | Section_string -> ".section .rodata" - | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" - | 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 name_of_section = fun _ -> assert false let stack_alignment = 16 @@ -189,26 +171,7 @@ module MacOS_System : SYSTEM = let label oc lbl = fprintf oc "L%d" lbl - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i || (not !Clflags.option_fcommon) then ".data" else "COMM" - | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".const" else "COMM" - | Section_string -> ".const" - | Section_literal -> ".literal8" - | 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 name_of_section = fun _ -> assert false let stack_alignment = 16 (* mandatory *) @@ -248,25 +211,7 @@ module Cygwin_System : SYSTEM = let label oc lbl = fprintf oc "L%d" lbl - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else common_section () - | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rdata,\"dr\"" else "COMM" - | 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 name_of_section = fun _ -> assert false let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -887,24 +832,7 @@ module Target(System: SYSTEM):TARGET = end let print_epilogue oc = - if !need_masks then begin - section oc (Section_const true); - (* not Section_literal because not 8-bytes *) - 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 + assert false let comment = comment -- cgit