diff options
Diffstat (limited to 'verilog/Asmexpand.ml')
| -rw-r--r-- | verilog/Asmexpand.ml | 77 |
1 files changed, 48 insertions, 29 deletions
diff --git a/verilog/Asmexpand.ml b/verilog/Asmexpand.ml index 1b3961e0..e2c556c7 100644 --- a/verilog/Asmexpand.ml +++ b/verilog/Asmexpand.ml @@ -39,6 +39,11 @@ 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. *) let align n a = @@ -104,21 +109,6 @@ 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 @@ -160,8 +150,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_lea RSI (addressing_of_builtin_arg src); - if dst <> BA (IR RDI) then emit_lea RDI (addressing_of_builtin_arg 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)); (* TODO: movsq? *) emit (Pmovl_ri (RCX,coqint_of_camlint (Int32.of_int (sz / 4)))); emit Prep_movsl; @@ -299,9 +289,9 @@ let expand_builtin_va_start_elf64 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_leaq RAX (linear_addr RSP (Z.of_uint64 overflow_arg_area)); + emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 overflow_arg_area))); emit (Pmovq_mr (linear_addr r _8z, RAX)); - emit_leaq RAX (linear_addr RSP (Z.of_uint64 reg_save_area)); + emit (Pleaq (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 = @@ -312,7 +302,7 @@ let expand_builtin_va_start_win64 r = 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 (Pleaq (RAX, linear_addr RSP (Z.of_uint64 ofs))); emit (Pmovq_mr (linear_addr r _0z, RAX)) (* FMA operations *) @@ -491,7 +481,8 @@ 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_elf64 a + if Archi.win64 then expand_builtin_va_start_win64 a + else if Archi.ptr64 then expand_builtin_va_start_elf64 a else expand_builtin_va_start_32 a (* Synchronization *) | "__builtin_membar", [], _ -> @@ -522,7 +513,14 @@ let fixup_funcall_elf64 sg = registers. *) -let copy_fregs_to_iregs args fr ir = +let rec copy_fregs_to_iregs args fr ir = + match (ir, fr, args) with + | (i1 :: ir, f1 :: fr, (Tfloat | Tsingle) :: args) -> + emit (Pmovq_rf (i1, f1)); + copy_fregs_to_iregs args fr ir + | (i1 :: ir, f1 :: fr, _ :: args) -> + copy_fregs_to_iregs args fr ir + | _ -> () let fixup_funcall_win64 sg = @@ -530,8 +528,10 @@ let fixup_funcall_win64 sg = 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 + if Archi.ptr64 + then if Archi.win64 + then fixup_funcall_win64 sg + else fixup_funcall_elf64 sg else () (* Expansion of instructions *) @@ -539,7 +539,23 @@ let fixup_funcall sg = let expand_instruction instr = match instr with | Pallocframe (sz, ofs_ra, ofs_link) -> - if Archi.ptr64 then begin + if Archi.win64 then begin + let sz = sp_adjustment_win64 sz in + if is_current_function_variadic() then + (* Save parameters passed in registers in reserved stack area *) + emit (Pcall_s (intern_string "__compcert_va_saveregs", + {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})); + (* Allocate frame *) + let sz' = Z.of_uint sz in + emit (Psubl_ri (RSP, sz')); + emit (Pcfi_adjust sz'); + (* Stack chaining *) + let addr1 = linear_addr RSP (Z.of_uint (sz + 8)) in + let addr2 = linear_addr RSP ofs_link in + emit (Pleaq (RAX,addr1)); + emit (Pmovq_mr (addr2, RAX)); + current_function_stacksize := Int64.of_int (sz + 8) + end else if Archi.ptr64 then begin let (sz, save_regs) = sp_adjustment_elf64 sz in (* Allocate frame *) let sz' = Z.of_uint sz in @@ -547,7 +563,7 @@ let expand_instruction instr = emit (Pcfi_adjust sz'); if save_regs >= 0 then begin (* Save the registers *) - emit_leaq R10 (linear_addr RSP (Z.of_uint save_regs)); + emit (Pleaq (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; @@ -555,7 +571,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_leaq RAX addr1; + emit (Pleaq (RAX, addr1)); emit (Pmovq_mr (addr2, RAX)); current_function_stacksize := Int64.of_int fullsz end else begin @@ -572,7 +588,10 @@ let expand_instruction instr = PrintAsmaux.current_function_stacksize := Int32.of_int sz end | Pfreeframe(sz, ofs_ra, ofs_link) -> - if Archi.ptr64 then begin + if Archi.win64 then begin + let sz = sp_adjustment_win64 sz in + emit (Paddq_ri (RSP, Z.of_uint sz)) + end else if Archi.ptr64 then begin let (sz, _) = sp_adjustment_elf64 sz in emit (Paddq_ri (RSP, Z.of_uint sz)) end else begin @@ -595,7 +614,7 @@ let expand_instruction instr = expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args | EF_annot_val(kind,txt, targ) -> expand_annot_val kind txt targ args res - | EF_annot _ | EF_debug _ | EF_inline_asm _ -> + | EF_annot _ | EF_debug _ | EF_inline_asm _ | EF_profiling _ -> emit instr | _ -> assert false |