Fix compilation of verilog back end

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<i><j><k> 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