From a14b9578ee5297d954103e05d7b2d322816ddd8f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:38:24 +0200 Subject: Support for 64-bit architectures: x86 in 64-bit mode This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model. To activate x86-64 bit support, configure with "x86_64-linux". Main steps: - Enrich Op.v and Asm.v with 64-bit operations - SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers - Conventions1: support x86-64 ABI in addition to the 32-bit ABI. - Add support for the new 64-bit operations everywhere. - runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode To do: - More optimizations are possible on 64-bit integer arithmetic operations. - Could add new chunks to load, say, an unsigned byte into a 64-bit long (currently we load as a 32-bit int then zero-extend). - Implements the wrong ABI for struct passing. --- ia32/TargetPrinter.ml | 508 ++++++++++++++++++++++++++++---------------------- 1 file changed, 282 insertions(+), 226 deletions(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 4ffb701b..c3e70042 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(* Printing IA32 assembly code in asm syntax *) +(* Printing x86-64 assembly code in asm syntax *) open Printf open !Datatypes @@ -25,30 +25,41 @@ module StringSet = Set.Make(String) (* Basic printing functions used in definition of the systems *) -let int_reg_name = function - | EAX -> "%eax" | EBX -> "%ebx" | ECX -> "%ecx" | EDX -> "%edx" - | ESI -> "%esi" | EDI -> "%edi" | EBP -> "%ebp" | ESP -> "%esp" +let int64_reg_name = function + | RAX -> "%rax" | RBX -> "%rbx" | RCX -> "%rcx" | RDX -> "%rdx" + | RSI -> "%rsi" | RDI -> "%rdi" | RBP -> "%rbp" | RSP -> "%rsp" + | R8 -> "%r8" | R9 -> "%r9" | R10 -> "%r10" | R11 -> "%r11" + | R12 -> "%r12" | R13 -> "%r13" | R14 -> "%r14" | R15 -> "%r15" -let int8_reg_name = function - | EAX -> "%al" | EBX -> "%bl" | ECX -> "%cl" | EDX -> "%dl" - | _ -> assert false +let int32_reg_name = function + | RAX -> "%eax" | RBX -> "%ebx" | RCX -> "%ecx" | RDX -> "%edx" + | RSI -> "%esi" | RDI -> "%edi" | RBP -> "%ebp" | RSP -> "%esp" + | R8 -> "%r8d" | R9 -> "%r9d" | R10 -> "%r10d" | R11 -> "%r11d" + | R12 -> "%r12d" | R13 -> "%r13d" | R14 -> "%r14d" | R15 -> "%r15d" -let high_int8_reg_name = function - | EAX -> "%ah" | EBX -> "%bh" | ECX -> "%ch" | EDX -> "%dh" - | _ -> assert false +let int8_reg_name = function + | RAX -> "%al" | RBX -> "%bl" | RCX -> "%cl" | RDX -> "%dl" + | RSI -> "%sil" | RDI -> "%dil" | RBP -> "%bpl" | RSP -> "%spl" + | R8 -> "%r8b" | R9 -> "%r9b" | R10 -> "%r10b" | R11 -> "%r11b" + | R12 -> "%r12b" | R13 -> "%r13b" | R14 -> "%r14b" | R15 -> "%r15b" let int16_reg_name = function - | EAX -> "%ax" | EBX -> "%bx" | ECX -> "%cx" | EDX -> "%dx" - | ESI -> "%si" | EDI -> "%di" | EBP -> "%bp" | ESP -> "%sp" + | RAX -> "%ax" | RBX -> "%bx" | RCX -> "%cx" | RDX -> "%dx" + | RSI -> "%si" | RDI -> "%di" | RBP -> "%bp" | RSP -> "%sp" + | R8 -> "%r8w" | R9 -> "%r9w" | R10 -> "%r10w" | R11 -> "%r11w" + | R12 -> "%r12w" | R13 -> "%r13w" | R14 -> "%r14w" | R15 -> "%r15w" let float_reg_name = function | XMM0 -> "%xmm0" | XMM1 -> "%xmm1" | XMM2 -> "%xmm2" | XMM3 -> "%xmm3" | XMM4 -> "%xmm4" | XMM5 -> "%xmm5" | XMM6 -> "%xmm6" | XMM7 -> "%xmm7" + | XMM8 -> "%xmm8" | XMM9 -> "%xmm9" | XMM10 -> "%xmm10" | XMM11 -> "%xmm11" + | XMM12 -> "%xmm12" | XMM13 -> "%xmm13" | XMM14 -> "%xmm14" | XMM15 -> "%xmm15" -let ireg oc r = output_string oc (int_reg_name r) let ireg8 oc r = output_string oc (int8_reg_name r) -let high_ireg8 oc r = output_string oc (high_int8_reg_name r) let ireg16 oc r = output_string oc (int16_reg_name r) +let ireg32 oc r = output_string oc (int32_reg_name r) +let ireg64 oc r = output_string oc (int64_reg_name r) +let ireg = if Archi.ptr64 then ireg64 else ireg32 let freg oc r = output_string oc (float_reg_name r) let preg oc = function @@ -56,6 +67,8 @@ let preg oc = function | FR r -> freg oc r | _ -> assert false +let z oc n = output_string oc (Z.to_string n) + (* The comment deliminiter *) let comment = "#" @@ -68,7 +81,7 @@ module type SYSTEM = val name_of_section: section_name -> string val stack_alignment: int val print_align: out_channel -> int -> unit - val print_mov_ra: out_channel -> ireg -> ident -> unit + val print_mov_rs: out_channel -> ireg -> ident -> unit val print_fun_info: out_channel -> P.t -> unit val print_var_info: out_channel -> P.t -> unit val print_epilogue: out_channel -> unit @@ -76,61 +89,6 @@ module type SYSTEM = val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit end -(* Printer functions for cygwin *) -module Cygwin_System : SYSTEM = - struct - - let raw_symbol oc s = - fprintf oc "_%s" s - - let symbol oc symb = - raw_symbol oc (extern_atom symb) - - 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 "COMM" - | Section_const i | Section_small_const i -> - if i 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 *) - - let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) - - let print_align oc n = - fprintf oc " .align %d\n" n - - let print_mov_ra oc rd id = - fprintf oc " movl $%a, %a\n" symbol id ireg rd - - let print_fun_info _ _ = () - - let print_var_info _ _ = () - - let print_epilogue _ = () - - let print_comm_decl oc name sz al = - fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al - - let print_lcomm_decl oc name sz al = - fprintf oc " .local %a\n" symbol name; - print_comm_decl oc name sz al - - end - (* Printer functions for ELF *) module ELF_System : SYSTEM = struct @@ -161,13 +119,13 @@ module ELF_System : SYSTEM = | Section_debug_ranges -> ".section .debug_ranges,\"\",@progbits" | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" - let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) + let stack_alignment = 16 let print_align oc n = fprintf oc " .align %d\n" n - let print_mov_ra oc rd id = - fprintf oc " movl $%a, %a\n" symbol id ireg rd + let print_mov_rs oc rd id = + fprintf oc " movq %a@GOTPCREL(%%rip), %a\n" symbol id ireg64 rd let print_fun_info = elf_print_fun_info @@ -228,26 +186,14 @@ module MacOS_System : SYSTEM = let print_align oc n = fprintf oc " .align %d\n" (log2 n) - let indirect_symbols : StringSet.t ref = ref StringSet.empty - - let print_mov_ra oc rd id = - let id = extern_atom id in - indirect_symbols := StringSet.add id !indirect_symbols; - fprintf oc " movl L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd + let print_mov_rs oc rd id = + fprintf oc " movq %a@GOTPCREL(%%rip), %a\n" symbol id ireg64 rd let print_fun_info _ _ = () let print_var_info _ _ = () - let print_epilogue oc = - fprintf oc " .section __IMPORT,__pointers,non_lazy_symbol_pointers\n"; - StringSet.iter - (fun s -> - fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s; - fprintf oc " .indirect_symbol %a\n" raw_symbol s; - fprintf oc " .long 0\n") - !indirect_symbols; - indirect_symbols := StringSet.empty + let print_epilogue oc = () let print_comm_decl oc name sz al = fprintf oc " .comm %a, %s, %d\n" @@ -269,27 +215,39 @@ module Target(System: SYSTEM):TARGET = let symbol_offset oc (symb, ofs) = symbol oc symb; - if ofs <> 0l then fprintf oc " + %ld" ofs + let ofs = Z.to_int64 ofs in + if ofs <> 0L then fprintf oc " + %Ld" ofs - - let addressing oc (Addrmode(base, shift, cst)) = + let addressing_gen ireg oc (Addrmode(base, shift, cst)) = begin match cst with | Coq_inl n -> - let n = camlint_of_coqint n in - fprintf oc "%ld" n + fprintf oc "%s" (Z.to_string n) | Coq_inr(id, ofs) -> - let ofs = camlint_of_coqint ofs in - if ofs = 0l - then symbol oc id - else fprintf oc "(%a + %ld)" symbol id ofs + if Archi.ptr64 then begin + (* RIP-relative addressing *) + let ofs' = Z.to_int64 ofs in + if ofs' = 0L + then fprintf oc "%a(%%rip)" symbol id + else fprintf oc "(%a + %Ld)(%%rip)" symbol id ofs' + end else begin + (* Absolute addressing *) + let ofs' = Z.to_int32 ofs in + if ofs' = 0l + then fprintf oc "%a" symbol id + else fprintf oc "(%a + %ld)" symbol id ofs' + end end; begin match base, shift with | None, None -> () | Some r1, None -> fprintf oc "(%a)" ireg r1 - | None, Some(r2,sc) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc - | Some r1, Some(r2,sc) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc + | None, Some(r2,sc) -> fprintf oc "(,%a,%a)" ireg r2 z sc + | Some r1, Some(r2,sc) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 z sc end + let addressing32 = addressing_gen ireg32 + let addressing64 = addressing_gen ireg64 + let addressing = addressing_gen ireg + let name_of_condition = function | Cond_e -> "e" | Cond_ne -> "ne" | Cond_b -> "b" | Cond_be -> "be" | Cond_ae -> "ae" | Cond_a -> "a" @@ -317,15 +275,28 @@ module Target(System: SYSTEM):TARGET = let print_file_line oc file line = print_file_line oc comment file line - - (* Built-in functions *) (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; - inlined by the compiler: take their arguments in arbitrary - registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *) + registers; preserve all registers except RCX, RDX, XMM6 and XMM7. *) + +(* Hack for large 64-bit immediates *) + + let intconst64 oc n = + let n1 = camlint64_of_coqint n in + let n2 = Int64.to_int32 n1 in + if n1 = Int64.of_int32 n2 then + (* fit in a 32-bit signed integer, can use as immediate *) + fprintf oc "$%ld" n2 + else begin + (* put the constant in memory and use a PC-relative memory operand *) + let lbl = new_label() in + float64_literals := (lbl, n1) :: !float64_literals; + fprintf oc "%a(%%rip)" label lbl + end (* Printing of instructions *) @@ -334,15 +305,36 @@ module Target(System: SYSTEM):TARGET = let print_instruction oc = function (* Moves *) | Pmov_rr(rd, r1) -> - fprintf oc " movl %a, %a\n" ireg r1 ireg rd - | Pmov_ri(rd, n) -> - fprintf oc " movl $%ld, %a\n" (camlint_of_coqint n) ireg rd - | Pmov_ra(rd, id) -> - print_mov_ra oc rd id - | Pmov_rm(rd, a) | Pmov_rm_a(rd, a) -> - fprintf oc " movl %a, %a\n" addressing a ireg rd - | Pmov_mr(a, r1) | Pmov_mr_a(a, r1) -> - fprintf oc " movl %a, %a\n" ireg r1 addressing a + if Archi.ptr64 + then fprintf oc " movq %a, %a\n" ireg64 r1 ireg64 rd + else fprintf oc " movl %a, %a\n" ireg32 r1 ireg32 rd + | Pmovl_ri(rd, n) -> + fprintf oc " movl $%ld, %a\n" (camlint_of_coqint n) ireg32 rd + | 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 + fprintf oc " movq $%ld, %a\n" n2 ireg64 rd + else + fprintf oc " movabsq $%Ld, %a\n" n1 ireg64 rd + | Pmov_rs(rd, id) -> + print_mov_rs oc rd id + | Pmovl_rm(rd, a) -> + fprintf oc " movl %a, %a\n" addressing a ireg32 rd + | Pmovq_rm(rd, a) -> + fprintf oc " movq %a, %a\n" addressing a ireg64 rd + | Pmov_rm_a(rd, a) -> + if Archi.ptr64 + then fprintf oc " movq %a, %a\n" addressing a ireg64 rd + else fprintf oc " movl %a, %a\n" addressing a ireg32 rd + | Pmovl_mr(a, r1) -> + fprintf oc " movl %a, %a\n" ireg32 r1 addressing a + | Pmovq_mr(a, r1) -> + fprintf oc " movq %a, %a\n" ireg64 r1 addressing a + | Pmov_mr_a(a, r1) -> + if Archi.ptr64 + then fprintf oc " movq %a, %a\n" ireg64 r1 addressing a + else fprintf oc " movl %a, %a\n" ireg32 r1 addressing a | Pmovsd_ff(rd, r1) -> fprintf oc " movapd %a, %a\n" freg r1 freg rd | Pmovsd_fi(rd, n) -> @@ -366,112 +358,183 @@ module Target(System: SYSTEM):TARGET = | Pfldl_m(a) -> fprintf oc " fldl %a\n" addressing a | Pfstpl_m(a) -> - fprintf oc " fstpl %a\n" addressing a + fprintf oc " fstpl %a\n" addressing a | Pflds_m(a) -> fprintf oc " flds %a\n" addressing a | Pfstps_m(a) -> fprintf oc " fstps %a\n" addressing a - | Pxchg_rr(r1, r2) -> - fprintf oc " xchgl %a, %a\n" ireg r1 ireg r2 (* Moves with conversion *) | Pmovb_mr(a, r1) -> fprintf oc " movb %a, %a\n" ireg8 r1 addressing a | Pmovw_mr(a, r1) -> fprintf oc " movw %a, %a\n" ireg16 r1 addressing a | Pmovzb_rr(rd, r1) -> - fprintf oc " movzbl %a, %a\n" ireg8 r1 ireg rd + fprintf oc " movzbl %a, %a\n" ireg8 r1 ireg32 rd | Pmovzb_rm(rd, a) -> - fprintf oc " movzbl %a, %a\n" addressing a ireg rd + fprintf oc " movzbl %a, %a\n" addressing a ireg32 rd | Pmovsb_rr(rd, r1) -> - fprintf oc " movsbl %a, %a\n" ireg8 r1 ireg rd + fprintf oc " movsbl %a, %a\n" ireg8 r1 ireg32 rd | Pmovsb_rm(rd, a) -> - fprintf oc " movsbl %a, %a\n" addressing a ireg rd + fprintf oc " movsbl %a, %a\n" addressing a ireg32 rd | Pmovzw_rr(rd, r1) -> - fprintf oc " movzwl %a, %a\n" ireg16 r1 ireg rd + fprintf oc " movzwl %a, %a\n" ireg16 r1 ireg32 rd | Pmovzw_rm(rd, a) -> - fprintf oc " movzwl %a, %a\n" addressing a ireg rd + fprintf oc " movzwl %a, %a\n" addressing a ireg32 rd | Pmovsw_rr(rd, r1) -> - fprintf oc " movswl %a, %a\n" ireg16 r1 ireg rd + fprintf oc " movswl %a, %a\n" ireg16 r1 ireg32 rd | Pmovsw_rm(rd, a) -> - fprintf oc " movswl %a, %a\n" addressing a ireg rd + fprintf oc " movswl %a, %a\n" addressing a ireg32 rd + | Pmovzl_rr(rd, r1) -> + fprintf oc " movl %a, %a\n" ireg32 r1 ireg32 rd + (* movl sets the high 32 bits of the destination to zero *) + | Pmovsl_rr(rd, r1) -> + fprintf oc " movslq %a, %a\n" ireg32 r1 ireg64 rd + | Pmovls_rr(rd) -> + () (* nothing to do *) | Pcvtsd2ss_ff(rd, r1) -> fprintf oc " cvtsd2ss %a, %a\n" freg r1 freg rd | Pcvtss2sd_ff(rd, r1) -> fprintf oc " cvtss2sd %a, %a\n" freg r1 freg rd | Pcvttsd2si_rf(rd, r1) -> - fprintf oc " cvttsd2si %a, %a\n" freg r1 ireg rd + fprintf oc " cvttsd2si %a, %a\n" freg r1 ireg32 rd | Pcvtsi2sd_fr(rd, r1) -> - fprintf oc " cvtsi2sd %a, %a\n" ireg r1 freg rd + fprintf oc " cvtsi2sd %a, %a\n" ireg32 r1 freg rd | Pcvttss2si_rf(rd, r1) -> - fprintf oc " cvttss2si %a, %a\n" freg r1 ireg rd + fprintf oc " cvttss2si %a, %a\n" freg r1 ireg32 rd | Pcvtsi2ss_fr(rd, r1) -> - fprintf oc " cvtsi2ss %a, %a\n" ireg r1 freg rd + fprintf oc " cvtsi2ss %a, %a\n" ireg32 r1 freg rd + | Pcvttsd2sl_rf(rd, r1) -> + fprintf oc " cvttsd2si %a, %a\n" freg r1 ireg64 rd + | Pcvtsl2sd_fr(rd, r1) -> + fprintf oc " cvtsi2sdq %a, %a\n" ireg64 r1 freg rd + | Pcvttss2sl_rf(rd, r1) -> + fprintf oc " cvttss2si %a, %a\n" freg r1 ireg64 rd + | Pcvtsl2ss_fr(rd, r1) -> + fprintf oc " cvtsi2ssq %a, %a\n" ireg64 r1 freg rd (* Arithmetic and logical operations over integers *) - | Plea(rd, a) -> - fprintf oc " leal %a, %a\n" addressing a ireg rd - | Pneg(rd) -> - fprintf oc " negl %a\n" ireg rd - | Psub_rr(rd, r1) -> - fprintf oc " subl %a, %a\n" ireg r1 ireg rd - | Pimul_rr(rd, r1) -> - fprintf oc " imull %a, %a\n" ireg r1 ireg rd - | Pimul_ri(rd, n) -> - fprintf oc " imull $%a, %a\n" coqint n ireg rd - | Pimul_r(r1) -> - fprintf oc " imull %a\n" ireg r1 - | Pmul_r(r1) -> - fprintf oc " mull %a\n" ireg r1 + | Pleal(rd, a) -> + fprintf oc " leal %a, %a\n" addressing32 a ireg32 rd + | Pleaq(rd, a) -> + fprintf oc " leaq %a, %a\n" addressing64 a ireg64 rd + | Pnegl(rd) -> + fprintf oc " negl %a\n" ireg32 rd + | Pnegq(rd) -> + fprintf oc " negq %a\n" ireg64 rd + | Paddl_ri (res,n) -> + fprintf oc " addl $%ld, %a\n" (camlint_of_coqint n) ireg32 res + | Paddq_ri (res,n) -> + fprintf oc " addq %a, %a\n" intconst64 n ireg64 res + | Psubl_rr(rd, r1) -> + fprintf oc " subl %a, %a\n" ireg32 r1 ireg32 rd + | Psubq_rr(rd, r1) -> + fprintf oc " subq %a, %a\n" ireg64 r1 ireg64 rd + | Pimull_rr(rd, r1) -> + fprintf oc " imull %a, %a\n" ireg32 r1 ireg32 rd + | Pimulq_rr(rd, r1) -> + fprintf oc " imulq %a, %a\n" ireg64 r1 ireg64 rd + | Pimull_ri(rd, n) -> + fprintf oc " imull $%a, %a\n" coqint n ireg32 rd + | Pimulq_ri(rd, n) -> + fprintf oc " imulq %a, %a\n" intconst64 n ireg64 rd + | Pimull_r(r1) -> + fprintf oc " imull %a\n" ireg32 r1 + | Pmull_r(r1) -> + fprintf oc " mull %a\n" ireg32 r1 | Pcltd -> fprintf oc " cltd\n" - | Pdiv(r1) -> - fprintf oc " divl %a\n" ireg r1 - | Pidiv(r1) -> - fprintf oc " idivl %a\n" ireg r1 - | Pand_rr(rd, r1) -> - fprintf oc " andl %a, %a\n" ireg r1 ireg rd - | Pand_ri(rd, n) -> - fprintf oc " andl $%a, %a\n" coqint n ireg rd - | Por_rr(rd, r1) -> - fprintf oc " orl %a, %a\n" ireg r1 ireg rd - | Por_ri(rd, n) -> - fprintf oc " orl $%a, %a\n" coqint n ireg rd - | Pxor_r(rd) -> - fprintf oc " xorl %a, %a\n" ireg rd ireg rd - | Pxor_rr(rd, r1) -> - fprintf oc " xorl %a, %a\n" ireg r1 ireg rd - | Pxor_ri(rd, n) -> - fprintf oc " xorl $%a, %a\n" coqint n ireg rd - | Pnot(rd) -> - fprintf oc " notl %a\n" ireg rd - | Psal_rcl(rd) -> - fprintf oc " sall %%cl, %a\n" ireg rd - | Psal_ri(rd, n) -> - fprintf oc " sall $%a, %a\n" coqint n ireg rd - | Pshr_rcl(rd) -> - fprintf oc " shrl %%cl, %a\n" ireg rd - | Pshr_ri(rd, n) -> - fprintf oc " shrl $%a, %a\n" coqint n ireg rd - | Psar_rcl(rd) -> - fprintf oc " sarl %%cl, %a\n" ireg rd - | Psar_ri(rd, n) -> - fprintf oc " sarl $%a, %a\n" coqint n ireg rd + | Pcqto -> + fprintf oc " cqto\n"; + | Pdivl(r1) -> + fprintf oc " divl %a\n" ireg32 r1 + | Pdivq(r1) -> + fprintf oc " divq %a\n" ireg64 r1 + | Pidivl(r1) -> + fprintf oc " idivl %a\n" ireg32 r1 + | Pidivq(r1) -> + fprintf oc " idivq %a\n" ireg64 r1 + | Pandl_rr(rd, r1) -> + fprintf oc " andl %a, %a\n" ireg32 r1 ireg32 rd + | Pandq_rr(rd, r1) -> + fprintf oc " andq %a, %a\n" ireg64 r1 ireg64 rd + | Pandl_ri(rd, n) -> + fprintf oc " andl $%a, %a\n" coqint n ireg32 rd + | Pandq_ri(rd, n) -> + fprintf oc " andq %a, %a\n" intconst64 n ireg64 rd + | Porl_rr(rd, r1) -> + fprintf oc " orl %a, %a\n" ireg32 r1 ireg32 rd + | Porq_rr(rd, r1) -> + fprintf oc " orq %a, %a\n" ireg64 r1 ireg64 rd + | Porl_ri(rd, n) -> + fprintf oc " orl $%a, %a\n" coqint n ireg32 rd + | Porq_ri(rd, n) -> + fprintf oc " orq %a, %a\n" intconst64 n ireg64 rd + | Pxorl_r(rd) -> + fprintf oc " xorl %a, %a\n" ireg32 rd ireg32 rd + | Pxorq_r(rd) -> + fprintf oc " xorq %a, %a\n" ireg64 rd ireg64 rd + | Pxorl_rr(rd, r1) -> + fprintf oc " xorl %a, %a\n" ireg32 r1 ireg32 rd + | Pxorq_rr(rd, r1) -> + fprintf oc " xorq %a, %a\n" ireg64 r1 ireg64 rd + | Pxorl_ri(rd, n) -> + fprintf oc " xorl $%a, %a\n" coqint n ireg32 rd + | Pxorq_ri(rd, n) -> + fprintf oc " xorq %a, %a\n" intconst64 n ireg64 rd + | Pnotl(rd) -> + fprintf oc " notl %a\n" ireg32 rd + | Pnotq(rd) -> + fprintf oc " notq %a\n" ireg64 rd + | Psall_rcl(rd) -> + fprintf oc " sall %%cl, %a\n" ireg32 rd + | Psalq_rcl(rd) -> + fprintf oc " salq %%cl, %a\n" ireg64 rd + | Psall_ri(rd, n) -> + fprintf oc " sall $%a, %a\n" coqint n ireg32 rd + | Psalq_ri(rd, n) -> + fprintf oc " salq $%a, %a\n" coqint n ireg64 rd + | Pshrl_rcl(rd) -> + fprintf oc " shrl %%cl, %a\n" ireg32 rd + | Pshrq_rcl(rd) -> + fprintf oc " shrq %%cl, %a\n" ireg64 rd + | Pshrl_ri(rd, n) -> + fprintf oc " shrl $%a, %a\n" coqint n ireg32 rd + | Pshrq_ri(rd, n) -> + fprintf oc " shrq $%a, %a\n" coqint n ireg64 rd + | Psarl_rcl(rd) -> + fprintf oc " sarl %%cl, %a\n" ireg32 rd + | Psarq_rcl(rd) -> + fprintf oc " sarq %%cl, %a\n" ireg64 rd + | Psarl_ri(rd, n) -> + fprintf oc " sarl $%a, %a\n" coqint n ireg32 rd + | Psarq_ri(rd, n) -> + fprintf oc " sarq $%a, %a\n" coqint n ireg64 rd | Pshld_ri(rd, r1, n) -> - fprintf oc " shldl $%a, %a, %a\n" coqint n ireg r1 ireg rd - | Pror_ri(rd, n) -> - fprintf oc " rorl $%a, %a\n" coqint n ireg rd - | Pcmp_rr(r1, r2) -> - fprintf oc " cmpl %a, %a\n" ireg r2 ireg r1 - | Pcmp_ri(r1, n) -> - fprintf oc " cmpl $%a, %a\n" coqint n ireg r1 - | Ptest_rr(r1, r2) -> - fprintf oc " testl %a, %a\n" ireg r2 ireg r1 - | Ptest_ri(r1, n) -> - fprintf oc " testl $%a, %a\n" coqint n ireg r1 + fprintf oc " shldl $%a, %a, %a\n" coqint n ireg32 r1 ireg32 rd + | Prorl_ri(rd, n) -> + fprintf oc " rorl $%a, %a\n" coqint n ireg32 rd + | Prorq_ri(rd, n) -> + fprintf oc " rorq $%a, %a\n" coqint n ireg64 rd + | Pcmpl_rr(r1, r2) -> + fprintf oc " cmpl %a, %a\n" ireg32 r2 ireg32 r1 + | Pcmpq_rr(r1, r2) -> + fprintf oc " cmpq %a, %a\n" ireg64 r2 ireg64 r1 + | Pcmpl_ri(r1, n) -> + fprintf oc " cmpl $%a, %a\n" coqint n ireg32 r1 + | Pcmpq_ri(r1, n) -> + fprintf oc " cmpq %a, %a\n" intconst64 n ireg64 r1 + | Ptestl_rr(r1, r2) -> + fprintf oc " testl %a, %a\n" ireg32 r2 ireg32 r1 + | Ptestq_rr(r1, r2) -> + fprintf oc " testq %a, %a\n" ireg64 r2 ireg64 r1 + | Ptestl_ri(r1, n) -> + fprintf oc " testl $%a, %a\n" coqint n ireg32 r1 + | Ptestq_ri(r1, n) -> + fprintf oc " testl %a, %a\n" intconst64 n ireg64 r1 | Pcmov(c, rd, r1) -> fprintf oc " cmov%s %a, %a\n" (name_of_condition c) ireg r1 ireg rd | Psetcc(c, rd) -> fprintf oc " set%s %a\n" (name_of_condition c) ireg8 rd; - fprintf oc " movzbl %a, %a\n" ireg8 rd ireg rd + fprintf oc " movzbl %a, %a\n" ireg8 rd ireg32 rd (* Arithmetic operations over floats *) | Paddd_ff(rd, r1) -> fprintf oc " addsd %a, %a\n" freg r1 freg rd @@ -513,10 +576,8 @@ module Target(System: SYSTEM):TARGET = | Pjmp_l(l) -> fprintf oc " jmp %a\n" label (transl_label l) | Pjmp_s(f, sg) -> - assert (not sg.sig_cc.cc_structret); fprintf oc " jmp %a\n" symbol f | Pjmp_r(r, sg) -> - assert (not sg.sig_cc.cc_structret); fprintf oc " jmp *%a\n" ireg r | Pjcc(c, l) -> let l = transl_label l in @@ -529,40 +590,35 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%a:\n" label l' | Pjmptbl(r, tbl) -> let l = new_label() in - fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r; + fprintf oc " jmp *%a(, %a, 8)\n" label l ireg64 r; jumptables := (l, tbl) :: !jumptables | Pcall_s(f, sg) -> - fprintf oc " call %a\n" symbol f; - if sg.sig_cc.cc_structret then - fprintf oc " pushl %%eax\n" + fprintf oc " call %a\n" symbol f | Pcall_r(r, sg) -> - fprintf oc " call *%a\n" ireg r; - if sg.sig_cc.cc_structret then - fprintf oc " pushl %%eax\n" + fprintf oc " call *%a\n" ireg r | Pret -> - if (!current_function_sig).sig_cc.cc_structret then begin - fprintf oc " movl 0(%%esp), %%eax\n"; - fprintf oc " ret $4\n" - end else begin - fprintf oc " ret\n" - end + fprintf oc " ret\n" (* Instructions produced by Asmexpand *) - | Padc_ri (res,n) -> - fprintf oc " adcl $%ld, %a\n" (camlint_of_coqint n) ireg res; - | Padc_rr (res,a1) -> - fprintf oc " adcl %a, %a\n" ireg a1 ireg res; - | Padd_ri (res,n) -> - fprintf oc " addl $%ld, %a\n" (camlint_of_coqint n) ireg res - | Padd_rr (res,a1) -> - fprintf oc " addl %a, %a\n" ireg a1 ireg res; - | Padd_mi (addr,n) -> + | Padcl_ri (res,n) -> + fprintf oc " adcl $%ld, %a\n" (camlint_of_coqint n) ireg32 res; + | Padcl_rr (res,a1) -> + fprintf oc " adcl %a, %a\n" ireg32 a1 ireg32 res; + | Paddl_rr (res,a1) -> + fprintf oc " addl %a, %a\n" ireg32 a1 ireg32 res; + | Paddl_mi (addr,n) -> fprintf oc " addl $%ld, %a\n" (camlint_of_coqint n) addressing addr - | Pbsf (res,a1) -> - fprintf oc " bsfl %a, %a\n" ireg a1 ireg res - | Pbsr (res,a1) -> - fprintf oc " bsrl %a, %a\n" ireg a1 ireg res - | Pbswap res -> - fprintf oc " bswap %a\n" ireg res + | Pbsfl (res,a1) -> + fprintf oc " bsfl %a, %a\n" ireg32 a1 ireg32 res + | Pbsfq (res,a1) -> + fprintf oc " bsfq %a, %a\n" ireg64 a1 ireg64 res + | Pbsrl (res,a1) -> + fprintf oc " bsrl %a, %a\n" ireg32 a1 ireg32 res + | Pbsrq (res,a1) -> + fprintf oc " bsrq %a, %a\n" ireg64 a1 ireg64 res + | Pbswap64 res -> + fprintf oc " bswap %a\n" ireg64 res + | Pbswap32 res -> + fprintf oc " bswap %a\n" ireg32 res | Pbswap16 res -> fprintf oc " rolw $8, %a\n" ireg16 res | Pcfi_adjust sz -> @@ -597,9 +653,9 @@ 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_mr(a, rs) -> + | Pmovsq_mr(a, rs) -> fprintf oc " movq %a, %a\n" freg rs addressing a - | Pmovq_rm(rd, a) -> + | Pmovsq_rm(rd, a) -> fprintf oc " movq %a, %a\n" addressing a freg rd | Pmovsb -> fprintf oc " movsb\n"; @@ -609,12 +665,14 @@ module Target(System: SYSTEM):TARGET = fprintf oc " movw %a, %a\n" addressing a ireg16 rd | Prep_movsl -> fprintf oc " rep movsl\n" - | Psbb_rr (res,a1) -> - fprintf oc " sbbl %a, %a\n" ireg a1 ireg res + | Psbbl_rr (res,a1) -> + fprintf oc " sbbl %a, %a\n" ireg32 a1 ireg32 res | Psqrtsd (res,a1) -> fprintf oc " sqrtsd %a, %a\n" freg a1 freg res - | Psub_ri (res,n) -> - fprintf oc " subl $%ld, %a\n" (camlint_of_coqint n) ireg res; + | Psubl_ri (res,n) -> + fprintf oc " subl $%ld, %a\n" (camlint_of_coqint n) ireg32 res; + | Psubq_ri (res,n) -> + fprintf oc " subq %a, %a\n" intconst64 n ireg64 res; (* Pseudo-instructions *) | Plabel(l) -> fprintf oc "%a:\n" label (transl_label l) @@ -646,11 +704,11 @@ module Target(System: SYSTEM):TARGET = let print_jumptable oc (lbl, tbl) = fprintf oc "%a:" label lbl; List.iter - (fun l -> fprintf oc " .long %a\n" label (transl_label l)) + (fun l -> fprintf oc " .quad %a\n" label (transl_label l)) tbl in if !jumptables <> [] then begin section oc jmptbl; - print_align oc 4; + print_align oc 8; List.iter (print_jumptable oc) !jumptables; jumptables := [] end @@ -674,10 +732,9 @@ module Target(System: SYSTEM):TARGET = comment (camlfloat_of_coqfloat n) | Init_space n -> if Z.gt n Z.zero then - fprintf oc " .space %s\n" (Z.to_string n) + fprintf oc " .space %a\n" z n | Init_addrof(symb, ofs) -> - fprintf oc " .long %a\n" - symbol_offset (symb, camlint_of_coqint ofs) + fprintf oc " .quad %a\n" symbol_offset (symb, ofs) let print_align = print_align @@ -760,6 +817,5 @@ let sel_target () = | "macosx" -> (module MacOS_System:SYSTEM) | "linux" | "bsd" -> (module ELF_System:SYSTEM) - | "cygwin" -> (module Cygwin_System:SYSTEM) | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") ):SYSTEM) in (module Target(S):TARGET) -- cgit