diff options
Diffstat (limited to 'verilog/TargetPrinter.ml')
| -rw-r--r-- | verilog/TargetPrinter.ml | 1496 |
1 files changed, 570 insertions, 926 deletions
diff --git a/verilog/TargetPrinter.ml b/verilog/TargetPrinter.ml index 00e70f65..aab6b9b8 100644 --- a/verilog/TargetPrinter.ml +++ b/verilog/TargetPrinter.ml @@ -3,14 +3,19 @@ (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Prashanth Mundkur, SRI International *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) +(* The contributions by Prashanth Mundkur are reused and adapted *) +(* under the terms of a Contributor License Agreement between *) +(* SRI International and INRIA. *) +(* *) (* *********************************************************************) -(* Printing x86-64 assembly code in asm syntax *) +(* Printing RISC-V assembly code in asm syntax *) open Printf open Camlcoq @@ -21,1003 +26,642 @@ open AisAnnot open PrintAsmaux open Fileinfo -module StringSet = Set.Make(String) - -(* Basic printing functions used in definition of the systems *) - -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 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 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 - | 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 ireg8 oc r = output_string oc (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_asm oc ty = function - | IR r -> if ty = Tlong then ireg64 oc r else ireg32 oc r - | FR r -> freg oc r - | _ -> assert false - -let preg_annot = function - | IR r -> if Archi.ptr64 then int64_reg_name r else int32_reg_name r - | FR r -> float_reg_name r - | _ -> assert false - -let ais_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 ais_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 preg_ais_annot = function - | IR r -> if Archi.ptr64 then ais_int64_reg_name r else ais_int32_reg_name r - | FR r -> float_reg_name r - | _ -> assert false - -let z oc n = output_string oc (Z.to_string n) - -(* 32/64 bit dependencies *) - -let data_pointer = if Archi.ptr64 then ".quad" else ".long" - -(* Base-2 log of a Caml integer *) -let rec log2 n = - assert (n > 0); - if n = 1 then 0 else 1 + log2 (n lsr 1) - -(* 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 - val name_of_section: section_name -> string - val stack_alignment: int - val print_align: out_channel -> int -> 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 - val print_comm_decl: out_channel -> P.t -> Z.t -> int -> unit - val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit - end - -(* Printer functions for ELF *) -module ELF_System : SYSTEM = +(* Module containing the printing functions *) + +module Target : TARGET = struct - (* The comment delimiter *) - let comment = "#" +(* Basic printing functions *) - let raw_symbol oc s = - fprintf oc "%s" s + let comment = "#" - let symbol = elf_symbol + let symbol = elf_symbol + let symbol_offset = elf_symbol_offset + let label = elf_label + + let print_label oc lbl = label oc (transl_label lbl) + + let use_abi_name = false + + let int_reg_num_name = function + | X1 -> "x1" | X2 -> "x2" | X3 -> "x3" + | X4 -> "x4" | X5 -> "x5" | X6 -> "x6" | X7 -> "x7" + | X8 -> "x8" | X9 -> "x9" | X10 -> "x10" | X11 -> "x11" + | X12 -> "x12" | X13 -> "x13" | X14 -> "x14" | X15 -> "x15" + | X16 -> "x16" | X17 -> "x17" | X18 -> "x18" | X19 -> "x19" + | X20 -> "x20" | X21 -> "x21" | X22 -> "x22" | X23 -> "x23" + | X24 -> "x24" | X25 -> "x25" | X26 -> "x26" | X27 -> "x27" + | X28 -> "x28" | X29 -> "x29" | X30 -> "x30" | X31 -> "x31" + + let int_reg_abi_name = function + | X1 -> "ra" | X2 -> "sp" | X3 -> "gp" + | X4 -> "tp" | X5 -> "t0" | X6 -> "t1" | X7 -> "t2" + | X8 -> "s0" | X9 -> "s1" | X10 -> "a0" | X11 -> "a1" + | X12 -> "a2" | X13 -> "a3" | X14 -> "a4" | X15 -> "a5" + | X16 -> "a6" | X17 -> "a7" | X18 -> "s2" | X19 -> "s3" + | X20 -> "s4" | X21 -> "s5" | X22 -> "s6" | X23 -> "s7" + | X24 -> "s8" | X25 -> "s9" | X26 -> "s10" | X27 -> "s11" + | X28 -> "t3" | X29 -> "t4" | X30 -> "t5" | X31 -> "t6" + + let float_reg_num_name = function + | F0 -> "f0" | F1 -> "f1" | F2 -> "f2" | F3 -> "f3" + | F4 -> "f4" | F5 -> "f5" | F6 -> "f6" | F7 -> "f7" + | F8 -> "f8" | F9 -> "f9" | F10 -> "f10" | F11 -> "f11" + | F12 -> "f12" | F13 -> "f13" | F14 -> "f14" | F15 -> "f15" + | F16 -> "f16" | F17 -> "f17" | F18 -> "f18" | F19 -> "f19" + | F20 -> "f20" | F21 -> "f21" | F22 -> "f22" | F23 -> "f23" + | F24 -> "f24" | F25 -> "f25" | F26 -> "f26" | F27 -> "f27" + | F28 -> "f28" | F29 -> "f29" | F30 -> "f30" | F31 -> "f31" + + let float_reg_abi_name = function + | F0 -> "ft0" | F1 -> "ft1" | F2 -> "ft2" | F3 -> "ft3" + | F4 -> "ft4" | F5 -> "ft5" | F6 -> "ft6" | F7 -> "ft7" + | F8 -> "fs0" | F9 -> "fs1" | F10 -> "fa0" | F11 -> "fa1" + | F12 -> "fa2" | F13 -> "fa3" | F14 -> "fa4" | F15 -> "fa5" + | F16 -> "fa6" | F17 -> "fa7" | F18 -> "fs2" | F19 -> "fs3" + | F20 -> "fs4" | F21 -> "fs5" | F22 -> "fs6" | F23 -> "fs7" + | F24 -> "fs8" | F25 -> "fs9" | F26 ->"fs10" | F27 -> "fs11" + | F28 -> "ft3" | F29 -> "ft4" | F30 -> "ft5" | F31 -> "ft6" + + let int_reg_name = if use_abi_name then int_reg_abi_name else int_reg_num_name + let float_reg_name = if use_abi_name then float_reg_abi_name else float_reg_num_name + + let ireg oc r = output_string oc (int_reg_name r) + let freg oc r = output_string oc (float_reg_name r) + + let ireg0 oc = function + | X0 -> output_string oc "x0" + | X r -> ireg oc r + + let preg_asm oc ty = function + | IR r -> ireg oc r + | FR r -> freg oc r + | _ -> assert false + + let preg_annot = function + | IR r -> int_reg_name r + | FR r -> float_reg_name r + | _ -> assert false - let label = elf_label +(* Names of sections *) let name_of_section = function - | Section_text -> ".text" + | Section_text -> ".text" | Section_data(i, true) -> failwith "_Thread_local unsupported on this platform" | Section_data(i, false) | Section_small_data i -> variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> variable_section ~sec:".section .rodata" i - | Section_string -> ".section .rodata" - | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" - | Section_jumptable -> ".text" + | Section_string -> ".section .rodata" + | Section_literal -> ".section .rodata" + | Section_jumptable -> ".section .rodata" + | Section_debug_info _ -> ".section .debug_info,\"\",%progbits" + | Section_debug_loc -> ".section .debug_loc,\"\",%progbits" + | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" + | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" + | Section_debug_ranges -> ".section .debug_ranges,\"\",%progbits" + | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",\"a%s%s\",@progbits" + 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 - - let print_align oc n = - fprintf oc " .align %d\n" n - - let print_mov_rs oc rd id = - if Archi.ptr64 - then fprintf oc " movq %a@GOTPCREL(%%rip), %a\n" symbol id ireg64 rd - else fprintf oc " movl $%a, %a\n" symbol id ireg32 rd - - let print_fun_info = elf_print_fun_info - - let print_var_info = elf_print_var_info - - let print_atexit oc to_be_called = - if Archi.ptr64 - then - begin - fprintf oc " leaq %s(%%rip), %%rdi\n" to_be_called; - fprintf oc " jmp atexit\n" - end - else - begin - fprintf oc " pushl $%s\n" to_be_called; - fprintf oc " call atexit\n"; - fprintf oc " addl $4, %%esp\n"; - fprintf oc " ret\n" - end - - let x86_profiling_stub oc nr_items - profiling_id_table_name - profiling_counter_table_name = - if Archi.ptr64 - then - begin - fprintf oc " leaq %s(%%rip), %%rdx\n" profiling_counter_table_name; - fprintf oc " leaq %s(%%rip), %%rsi\n" profiling_id_table_name; - fprintf oc " movl $%d, %%edi\n" nr_items; - fprintf oc " jmp %s\n" profiling_write_table_helper - end - else - begin - fprintf oc " pushl $%s\n" profiling_counter_table_name; - fprintf oc " pushl $%s\n" profiling_id_table_name; - fprintf oc " pushl $%d\n" nr_items; - fprintf oc " call %s\n" profiling_write_table_helper ; - fprintf oc " addl $12, %%esp\n"; - fprintf oc " ret\n" - end;; - - let print_epilogue oc = - print_profiling_epilogue elf_text_print_fun_info (Init_atexit print_atexit) x86_profiling_stub oc;; - - 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 MacOS *) -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 - - 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, true) -> - failwith "_Thread_local unsupported on this platform" - | Section_data(i, false) | 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 -> ".const" - | Section_literal -> ".const" - | 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 *) - - let print_align oc n = - fprintf oc " .align %d\n" (log2 n) - - 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 = () - - let print_comm_decl oc name sz al = - fprintf oc " .comm %a, %s, %d\n" - symbol name (Z.to_string sz) (log2 al) - - let print_lcomm_decl oc name sz al = - fprintf oc " .lcomm %a, %s, %d\n" - symbol name (Z.to_string sz) (log2 al) - - end - -(* Printer functions for Cygwin *) -module Cygwin_System : SYSTEM = - struct - - (* The comment delimiter *) - let comment = "#" - - let symbol_prefix = - if Archi.ptr64 then "" else "_" - - let raw_symbol oc s = - fprintf oc "%s%s" symbol_prefix 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, true) -> - failwith "_Thread_local unsupported on this platform" - | Section_data(i, false) | 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 - (* minimum is 4 for 32 bits, 8 for 64 bits; 8 is better for perfs *) - - 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 = - if Archi.ptr64 then begin - let s = extern_atom id in - indirect_symbols := StringSet.add s !indirect_symbols; - fprintf oc " movq .refptr.%s(%%rip), %a\n" s ireg rd - end else begin - fprintf oc " movl $%a, %a\n" symbol id ireg rd - end - - let print_fun_info _ _ = () - - let print_var_info _ _ = () + let section oc sec = + fprintf oc " %s\n" (name_of_section sec) - 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 +(* Associate labels to floating-point constants and to symbols. *) - let print_epilogue oc = - if Archi.ptr64 then begin - StringSet.iter (declare_indirect_symbol oc) !indirect_symbols; - indirect_symbols := StringSet.empty + let emit_constants oc lit = + if exists_constants () then begin + section oc lit; + if Hashtbl.length literal64_labels > 0 then + begin + fprintf oc " .align 3\n"; + Hashtbl.iter + (fun bf lbl -> fprintf oc "%a: .quad 0x%Lx\n" label lbl bf) + literal64_labels + end; + if Hashtbl.length literal32_labels > 0 then + begin + fprintf oc " .align 2\n"; + Hashtbl.iter + (fun bf lbl -> + fprintf oc "%a: .long 0x%lx\n" label lbl bf) + literal32_labels + end; + reset_literals () end - let print_comm_decl oc name sz al = - fprintf oc " .comm %a, %s, %d\n" - symbol name (Z.to_string sz) (log2 al) - - let print_lcomm_decl oc name sz al = - fprintf oc " .lcomm %a, %s, %d\n" - symbol name (Z.to_string sz) - (if Archi.ptr64 then al else log2 al) - - end - +(* Generate code to load the address of id + ofs in register r *) -module Target(System: SYSTEM):TARGET = - struct - open System - let symbol = symbol - -(* Basic printing functions *) - - let addressing_gen ireg oc (Addrmode(base, shift, cst)) = - begin match cst with - | Datatypes.Coq_inl n -> - fprintf oc "%s" (Z.to_string n) - | Datatypes.Coq_inr(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 z sc - | Some r1, Some(r2,sc) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 z sc + let loadsymbol oc r id ofs = + if Archi.pic_code () then begin + assert (ofs = Integers.Ptrofs.zero); + fprintf oc " la %a, %s\n" ireg r (extern_atom id) + end else begin + fprintf oc " lui %a, %%hi(%a)\n" + ireg r symbol_offset (id, ofs); + fprintf oc " addi %a, %a, %%lo(%a)\n" + ireg r ireg r symbol_offset (id, ofs) 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" - | Cond_l -> "l" | Cond_le -> "le" | Cond_ge -> "ge" | Cond_g -> "g" - | Cond_p -> "p" | Cond_np -> "np" - - let name_of_neg_condition = function - | Cond_e -> "ne" | Cond_ne -> "e" - | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be" - | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le" - | Cond_p -> "np" | Cond_np -> "p" - - -(* Names of sections *) - - let section oc sec = - fprintf oc " %s\n" (name_of_section sec) - -(* For "abs" and "neg" FP operations *) - - let need_masks = ref false - (* Emit .file / .loc debugging directives *) let print_file_line oc file line = print_file_line oc comment file line -(* In 64-bit mode use RIP-relative addressing to designate labels *) +(* + let print_location oc loc = + if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) +*) - let rip_rel = - if Archi.ptr64 then "(%rip)" else "" +(* Add "w" suffix to 32-bit instructions if we are in 64-bit mode *) + + let w oc = + if Archi.ptr64 then output_string oc "w" -(* Large 64-bit immediates (bigger than a 32-bit signed integer) are - not supported by the processor. Turn them into memory operands. *) +(* Offset part of a load or store *) - 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 = label_literal64 n1 in - fprintf oc "%a(%%rip)" label lbl - end + let offset oc = function + | Ofsimm n -> ptrofs oc n + | Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs) - let print_profiling_logger oc id kind = - assert (kind >= 0); - assert (kind <= 1); - let ofs = profiling_offset id kind in - if Archi.ptr64 - then - begin - fprintf oc "%s profiling %a %d: atomic increment\n" comment - Profilingaux.pp_id id kind; - fprintf oc " lock addq $1, %s+%d(%%rip)\n" - profiling_counter_table_name ofs - end - else - begin - fprintf oc "%s begin profiling %a %d: increment\n" comment - Profilingaux.pp_id id kind; - fprintf oc " addl $1, %s+%d\n" profiling_counter_table_name ofs; - fprintf oc " adcl $1, %s+%d\n" profiling_counter_table_name (ofs+4); - fprintf oc "%s end profiling %a %d: increment\n" comment - Profilingaux.pp_id id kind; - end - (* Printing of instructions *) - -(* Reminder on X86 assembly syntaxes: - AT&T syntax Intel syntax - (used by GNU as) (used in reference manuals) - dst <- op(src) op src, dst op dst, src - dst <- op(dst, src2) op src2, dst op dst, src2 - dst <- op(dst, src2, src3) op src3, src2, dst op dst, src2, src3 -*) - let print_instruction oc = function - (* Moves *) - | Pmov_rr(rd, r1) -> - 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) -> - let b = camlint64_of_coqint (Floats.Float.to_bits n) in - let lbl = label_literal64 b in - fprintf oc " movsd %a%s, %a %s %.18g\n" - label lbl rip_rel - freg rd comment (camlfloat_of_coqfloat n) - | Pmovsd_fm(rd, a) | Pmovsd_fm_a(rd, a) -> - fprintf oc " movsd %a, %a\n" addressing a freg rd - | Pmovsd_mf(a, r1) | Pmovsd_mf_a(a, r1) -> - fprintf oc " movsd %a, %a\n" freg r1 addressing a - | Pmovss_fi(rd, n) -> - let b = camlint_of_coqint (Floats.Float32.to_bits n) in - let lbl = label_literal32 b in - fprintf oc " movss %a%s, %a %s %.18g\n" - label lbl rip_rel - freg rd comment (camlfloat_of_coqfloat32 n) - | Pmovss_fm(rd, a) -> - fprintf oc " movss %a, %a\n" addressing a freg rd - | Pmovss_mf(a, r1) -> - fprintf oc " movss %a, %a\n" freg r1 addressing a - | Pfldl_m(a) -> - fprintf oc " fldl %a\n" addressing a - | Pfstpl_m(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 - (* 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 ireg32 rd - | Pmovzb_rm(rd, a) -> - fprintf oc " movzbl %a, %a\n" addressing a ireg32 rd - | Pmovsb_rr(rd, r1) -> - fprintf oc " movsbl %a, %a\n" ireg8 r1 ireg32 rd - | Pmovsb_rm(rd, a) -> - fprintf oc " movsbl %a, %a\n" addressing a ireg32 rd - | Pmovzw_rr(rd, r1) -> - fprintf oc " movzwl %a, %a\n" ireg16 r1 ireg32 rd - | Pmovzw_rm(rd, a) -> - fprintf oc " movzwl %a, %a\n" addressing a ireg32 rd - | Pmovsw_rr(rd, r1) -> - fprintf oc " movswl %a, %a\n" ireg16 r1 ireg32 rd - | Pmovsw_rm(rd, a) -> - 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 ireg32 rd - | Pcvtsi2sd_fr(rd, r1) -> - fprintf oc " cvtsi2sd %a, %a\n" ireg32 r1 freg rd - | Pcvttss2si_rf(rd, r1) -> - fprintf oc " cvttss2si %a, %a\n" freg r1 ireg32 rd - | Pcvtsi2ss_fr(rd, r1) -> - 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 *) - | 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 - | Pimulq_r(r1) -> - fprintf oc " imulq %a\n" ireg64 r1 - | Pmull_r(r1) -> - fprintf oc " mull %a\n" ireg32 r1 - | Pmulq_r(r1) -> - fprintf oc " mulq %a\n" ireg64 r1 - | Pcltd -> - fprintf oc " cltd\n" - | 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 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 ireg32 rd - (* Arithmetic operations over floats *) - | Paddd_ff(rd, r1) -> - fprintf oc " addsd %a, %a\n" freg r1 freg rd - | Psubd_ff(rd, r1) -> - fprintf oc " subsd %a, %a\n" freg r1 freg rd - | Pmuld_ff(rd, r1) -> - fprintf oc " mulsd %a, %a\n" freg r1 freg rd - | Pdivd_ff(rd, r1) -> - fprintf oc " divsd %a, %a\n" freg r1 freg rd - | Pnegd (rd) -> - need_masks := true; - fprintf oc " xorpd %a%s, %a\n" - raw_symbol "__negd_mask" rip_rel freg rd - | Pabsd (rd) -> - need_masks := true; - fprintf oc " andpd %a%s, %a\n" - raw_symbol "__absd_mask" rip_rel freg rd - | Pcomisd_ff(r1, r2) -> - fprintf oc " comisd %a, %a\n" freg r2 freg r1 - | Pxorpd_f (rd) -> - fprintf oc " xorpd %a, %a\n" freg rd freg rd - | Padds_ff(rd, r1) -> - fprintf oc " addss %a, %a\n" freg r1 freg rd - | Psubs_ff(rd, r1) -> - fprintf oc " subss %a, %a\n" freg r1 freg rd - | Pmuls_ff(rd, r1) -> - fprintf oc " mulss %a, %a\n" freg r1 freg rd - | Pdivs_ff(rd, r1) -> - fprintf oc " divss %a, %a\n" freg r1 freg rd - | Pnegs (rd) -> - need_masks := true; - fprintf oc " xorpd %a%s, %a\n" - raw_symbol "__negs_mask" rip_rel freg rd - | Pabss (rd) -> - need_masks := true; - fprintf oc " andpd %a%s, %a\n" - raw_symbol "__abss_mask" rip_rel freg rd - | Pcomiss_ff(r1, r2) -> - fprintf oc " comiss %a, %a\n" freg r2 freg r1 - | Pxorps_f (rd) -> - fprintf oc " xorpd %a, %a\n" freg rd freg rd - (* Branches and calls *) - | Pjmp_l(l) -> - fprintf oc " jmp %a\n" label (transl_label l) - | Pjmp_s(f, sg) -> - fprintf oc " jmp %a\n" symbol f - | Pjmp_r(r, sg) -> - fprintf oc " jmp *%a\n" ireg r - | Pjcc(c, l) -> - let l = transl_label l in - fprintf oc " j%s %a\n" (name_of_condition c) label l - | Pjcc2(c1, c2, l) -> - let l = transl_label l in - let l' = new_label() in - fprintf oc " j%s %a\n" (name_of_neg_condition c1) label l'; - fprintf oc " j%s %a\n" (name_of_condition c2) label l; - fprintf oc "%a:\n" label l' - | Pjmptbl(r, tbl) -> - let l = new_label() in - jumptables := (l, tbl) :: !jumptables; - if Archi.ptr64 then begin - let (tmp1, tmp2) = - if r = RAX then (RDX, RAX) else (RAX, RDX) in - fprintf oc " leaq %a(%%rip), %a\n" label l ireg tmp1; - fprintf oc " movslq (%a, %a, 4), %a\n" ireg tmp1 ireg r ireg tmp2; - fprintf oc " addq %a, %a\n" ireg tmp2 ireg tmp1; - fprintf oc " jmp *%a\n" ireg tmp1 - end else begin - fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r - end - | Pcall_s(f, sg) -> - fprintf oc " call %a\n" symbol f; - if (not Archi.ptr64) && sg.sig_cc.cc_structret then - fprintf oc " pushl %%eax\n" - | Pcall_r(r, sg) -> - fprintf oc " call *%a\n" ireg r; - if (not Archi.ptr64) && sg.sig_cc.cc_structret then - fprintf oc " pushl %%eax\n" - | Pret -> - if (not Archi.ptr64) - && (!current_function_sig).sig_cc.cc_structret then begin - fprintf oc " movl 4(%%esp), %%eax\n"; - fprintf oc " ret $4\n" - end else begin - fprintf oc " ret\n" - end - (* Instructions produced by Asmexpand *) - | 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 - | 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 -> - cfi_adjust oc (camlint_of_coqint sz) - | Pfmadd132 (res,a1,a2) -> - fprintf oc " vfmadd132sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfmadd213 (res,a1,a2) -> - fprintf oc " vfmadd213sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfmadd231 (res,a1,a2) -> - fprintf oc " vfmadd231sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfmsub132 (res,a1,a2) -> - fprintf oc " vfmsub132sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfmsub213 (res,a1,a2) -> - fprintf oc " vfmsub213sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfmsub231 (res,a1,a2) -> - fprintf oc " vfmsub231sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfnmadd132 (res,a1,a2) -> - fprintf oc " vfnmadd132sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfnmadd213 (res,a1,a2) -> - fprintf oc " vfnmadd213sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfnmadd231 (res,a1,a2) -> - fprintf oc " vfnmadd231sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfnmsub132 (res,a1,a2) -> - fprintf oc " vfnmsub132sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfnmsub213 (res,a1,a2) -> - fprintf oc " vfnmsub213sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pfnmsub231 (res,a1,a2) -> - fprintf oc " vfnmsub231sd %a, %a, %a\n" freg a2 freg a1 freg res - | Pmaxsd (res,a1) -> - fprintf oc " maxsd %a, %a\n" freg a1 freg res - | Pminsd (res,a1) -> - 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) -> - fprintf oc " movq %a, %a\n" addressing a freg rd - | Pmovsb -> - fprintf oc " movsb\n"; - | Pmovsw -> - fprintf oc " movsw\n"; - | Pmovw_rm (rd, a) -> - fprintf oc " movw %a, %a\n" addressing a ireg16 rd + | Pmv(rd, rs) -> + fprintf oc " mv %a, %a\n" ireg rd ireg rs + + (* 32-bit integer register-immediate instructions *) + | Paddiw (rd, rs, imm) -> + fprintf oc " addi%t %a, %a, %a\n" w ireg rd ireg0 rs coqint imm + | Psltiw (rd, rs, imm) -> + fprintf oc " slti %a, %a, %a\n" ireg rd ireg0 rs coqint imm + | Psltiuw (rd, rs, imm) -> + fprintf oc " sltiu %a, %a, %a\n" ireg rd ireg0 rs coqint imm + | Pandiw (rd, rs, imm) -> + fprintf oc " andi %a, %a, %a\n" ireg rd ireg0 rs coqint imm + | Poriw (rd, rs, imm) -> + fprintf oc " ori %a, %a, %a\n" ireg rd ireg0 rs coqint imm + | Pxoriw (rd, rs, imm) -> + fprintf oc " xori %a, %a, %a\n" ireg rd ireg0 rs coqint imm + | Pslliw (rd, rs, imm) -> + fprintf oc " slli%t %a, %a, %a\n" w ireg rd ireg0 rs coqint imm + | Psrliw (rd, rs, imm) -> + fprintf oc " srli%t %a, %a, %a\n" w ireg rd ireg0 rs coqint imm + | Psraiw (rd, rs, imm) -> + fprintf oc " srai%t %a, %a, %a\n" w ireg rd ireg0 rs coqint imm + | Pluiw (rd, imm) -> + fprintf oc " lui %a, %a\n" ireg rd coqint imm + + (* 32-bit integer register-register instructions *) + | Paddw(rd, rs1, rs2) -> + fprintf oc " add%t %a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2 + | Psubw(rd, rs1, rs2) -> + fprintf oc " sub%t %a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2 + + | Pmulw(rd, rs1, rs2) -> + fprintf oc " mul%t %a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2 + | Pmulhw(rd, rs1, rs2) -> assert (not Archi.ptr64); + fprintf oc " mulh %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Pmulhuw(rd, rs1, rs2) -> assert (not Archi.ptr64); + fprintf oc " mulhu %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + + | Pdivw(rd, rs1, rs2) -> + fprintf oc " div%t %a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2 + | Pdivuw(rd, rs1, rs2) -> + fprintf oc " divu%t %a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2 + | Premw(rd, rs1, rs2) -> + fprintf oc " rem%t %a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2 + | Premuw(rd, rs1, rs2) -> + fprintf oc " remu%t %a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2 + + | Psltw(rd, rs1, rs2) -> + fprintf oc " slt %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Psltuw(rd, rs1, rs2) -> + fprintf oc " sltu %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + + | Pandw(rd, rs1, rs2) -> + fprintf oc " and %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Porw(rd, rs1, rs2) -> + fprintf oc " or %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Pxorw(rd, rs1, rs2) -> + fprintf oc " xor %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Psllw(rd, rs1, rs2) -> + fprintf oc " sll%t %a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2 + | Psrlw(rd, rs1, rs2) -> + fprintf oc " srl%t %a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2 + | Psraw(rd, rs1, rs2) -> + fprintf oc " sra%t %a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2 + + (* 64-bit integer register-immediate instructions *) + | Paddil (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " addi %a, %a, %a\n" ireg rd ireg0 rs coqint64 imm + | Psltil (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " slti %a, %a, %a\n" ireg rd ireg0 rs coqint64 imm + | Psltiul (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " sltiu %a, %a, %a\n" ireg rd ireg0 rs coqint64 imm + | Pandil (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " andi %a, %a, %a\n" ireg rd ireg0 rs coqint64 imm + | Poril (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " ori %a, %a, %a\n" ireg rd ireg0 rs coqint64 imm + | Pxoril (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " xori %a, %a, %a\n" ireg rd ireg0 rs coqint64 imm + | Psllil (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " slli %a, %a, %a\n" ireg rd ireg0 rs coqint64 imm + | Psrlil (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " srli %a, %a, %a\n" ireg rd ireg0 rs coqint64 imm + | Psrail (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " srai %a, %a, %a\n" ireg rd ireg0 rs coqint64 imm + | Pluil (rd, imm) -> assert Archi.ptr64; + fprintf oc " lui %a, %a\n" ireg rd coqint64 imm + + (* 64-bit integer register-register instructions *) + | Paddl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " add %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Psubl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " sub %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + + | Pmull(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " mul %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Pmulhl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " mulh %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Pmulhul(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " mulhu %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + + | Pdivl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " div %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Pdivul(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " divu %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Preml(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " rem %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Premul(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " remu %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + + | Psltl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " slt %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Psltul(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " sltu %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + + | Pandl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " and %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Porl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " or %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Pxorl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " xor %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Pslll(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " sll %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Psrll(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " srl %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + | Psral(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " sra %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2 + + (* Unconditional jumps. Links are always to X1/RA. *) + (* TODO: fix up arguments for calls to variadics, to move *) + (* floating point arguments to integer registers. How? *) + | Pj_l(l) -> + fprintf oc " j %a\n" print_label l + | Pj_s(s, sg) -> + fprintf oc " j %a\n" symbol s + | Pj_r(r, sg) -> + fprintf oc " jr %a\n" ireg r + | Pjal_s(s, sg) -> + fprintf oc " call %a\n" symbol s + | Pjal_r(r, sg) -> + fprintf oc " jalr %a\n" ireg r + + (* Conditional branches, 32-bit comparisons *) + | Pbeqw(rs1, rs2, l) -> + fprintf oc " beq %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + | Pbnew(rs1, rs2, l) -> + fprintf oc " bne %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + | Pbltw(rs1, rs2, l) -> + fprintf oc " blt %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + | Pbltuw(rs1, rs2, l) -> + fprintf oc " bltu %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + | Pbgew(rs1, rs2, l) -> + fprintf oc " bge %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + | Pbgeuw(rs1, rs2, l) -> + fprintf oc " bgeu %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + + (* Conditional branches, 64-bit comparisons *) + | Pbeql(rs1, rs2, l) -> assert Archi.ptr64; + fprintf oc " beq %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + | Pbnel(rs1, rs2, l) -> assert Archi.ptr64; + fprintf oc " bne %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + | Pbltl(rs1, rs2, l) -> assert Archi.ptr64; + fprintf oc " blt %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + | Pbltul(rs1, rs2, l) -> assert Archi.ptr64; + fprintf oc " bltu %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + | Pbgel(rs1, rs2, l) -> assert Archi.ptr64; + fprintf oc " bge %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + | Pbgeul(rs1, rs2, l) -> assert Archi.ptr64; + fprintf oc " bgeu %a, %a, %a\n" ireg0 rs1 ireg0 rs2 print_label l + + (* Loads and stores *) + | Plb(rd, ra, ofs) -> + fprintf oc " lb %a, %a(%a)\n" ireg rd offset ofs ireg ra + | Plbu(rd, ra, ofs) -> + fprintf oc " lbu %a, %a(%a)\n" ireg rd offset ofs ireg ra + | Plh(rd, ra, ofs) -> + fprintf oc " lh %a, %a(%a)\n" ireg rd offset ofs ireg ra + | Plhu(rd, ra, ofs) -> + fprintf oc " lhu %a, %a(%a)\n" ireg rd offset ofs ireg ra + | Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) -> + fprintf oc " lw %a, %a(%a)\n" ireg rd offset ofs ireg ra + | Pld(rd, ra, ofs) | Pld_a(rd, ra, ofs) -> assert Archi.ptr64; + fprintf oc " ld %a, %a(%a)\n" ireg rd offset ofs ireg ra + + | Psb(rd, ra, ofs) -> + fprintf oc " sb %a, %a(%a)\n" ireg rd offset ofs ireg ra + | Psh(rd, ra, ofs) -> + fprintf oc " sh %a, %a(%a)\n" ireg rd offset ofs ireg ra + | Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) -> + fprintf oc " sw %a, %a(%a)\n" ireg rd offset ofs ireg ra + | Psd(rd, ra, ofs) | Psd_a(rd, ra, ofs) -> assert Archi.ptr64; + fprintf oc " sd %a, %a(%a)\n" ireg rd offset ofs ireg ra + + + (* Synchronization *) + | Pfence -> + fprintf oc " fence\n" + + (* floating point register move. + fmv.d preserves single-precision register contents, and hence + is applicable to both single- and double-precision moves. + *) + | Pfmv (fd,fs) -> + fprintf oc " fmv.d %a, %a\n" freg fd freg fs + | Pfmvxs (rd,fs) -> + fprintf oc " fmv.x.s %a, %a\n" ireg rd freg fs + | Pfmvsx (fd,rs) -> + fprintf oc " fmv.s.x %a, %a\n" freg fd ireg rs + | Pfmvxd (rd,fs) -> + fprintf oc " fmv.x.d %a, %a\n" ireg rd freg fs + | Pfmvdx (fd,rs) -> + fprintf oc " fmv.d.x %a, %a\n" freg fd ireg rs + + (* 32-bit (single-precision) floating point *) + | Pfls (fd, ra, ofs) -> + fprintf oc " flw %a, %a(%a)\n" freg fd offset ofs ireg ra + | Pfss (fs, ra, ofs) -> + fprintf oc " fsw %a, %a(%a)\n" freg fs offset ofs ireg ra + + | Pfnegs (fd, fs) -> + fprintf oc " fneg.s %a, %a\n" freg fd freg fs + | Pfabss (fd, fs) -> + fprintf oc " fabs.s %a, %a\n" freg fd freg fs + + | Pfadds (fd, fs1, fs2) -> + fprintf oc " fadd.s %a, %a, %a\n" freg fd freg fs1 freg fs2 + | Pfsubs (fd, fs1, fs2) -> + fprintf oc " fsub.s %a, %a, %a\n" freg fd freg fs1 freg fs2 + | Pfmuls (fd, fs1, fs2) -> + fprintf oc " fmul.s %a, %a, %a\n" freg fd freg fs1 freg fs2 + | Pfdivs (fd, fs1, fs2) -> + fprintf oc " fdiv.s %a, %a, %a\n" freg fd freg fs1 freg fs2 + | Pfmins (fd, fs1, fs2) -> + fprintf oc " fmin.s %a, %a, %a\n" freg fd freg fs1 freg fs2 + | Pfmaxs (fd, fs1, fs2) -> + fprintf oc " fmax.s %a, %a, %a\n" freg fd freg fs1 freg fs2 + + | Pfeqs (rd, fs1, fs2) -> + fprintf oc " feq.s %a, %a, %a\n" ireg rd freg fs1 freg fs2 + | Pflts (rd, fs1, fs2) -> + fprintf oc " flt.s %a, %a, %a\n" ireg rd freg fs1 freg fs2 + | Pfles (rd, fs1, fs2) -> + fprintf oc " fle.s %a, %a, %a\n" ireg rd freg fs1 freg fs2 + + | Pfsqrts (fd, fs) -> + fprintf oc " fsqrt.s %a, %a\n" freg fd freg fs + + | Pfmadds (fd, fs1, fs2, fs3) -> + fprintf oc " fmadd.s %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 + | Pfmsubs (fd, fs1, fs2, fs3) -> + fprintf oc " fmsub.s %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 + | Pfnmadds (fd, fs1, fs2, fs3) -> + fprintf oc " fnmadd.s %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 + | Pfnmsubs (fd, fs1, fs2, fs3) -> + fprintf oc " fnmsub.s %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 + + | Pfcvtws (rd, fs) -> + fprintf oc " fcvt.w.s %a, %a, rtz\n" ireg rd freg fs + | Pfcvtwus (rd, fs) -> + fprintf oc " fcvt.wu.s %a, %a, rtz\n" ireg rd freg fs + | Pfcvtsw (fd, rs) -> + fprintf oc " fcvt.s.w %a, %a\n" freg fd ireg0 rs + | Pfcvtswu (fd, rs) -> + fprintf oc " fcvt.s.wu %a, %a\n" freg fd ireg0 rs + + | Pfcvtls (rd, fs) -> assert Archi.ptr64; + fprintf oc " fcvt.l.s %a, %a, rtz\n" ireg rd freg fs + | Pfcvtlus (rd, fs) -> assert Archi.ptr64; + fprintf oc " fcvt.lu.s %a, %a, rtz\n" ireg rd freg fs + | Pfcvtsl (fd, rs) -> assert Archi.ptr64; + fprintf oc " fcvt.s.l %a, %a\n" freg fd ireg0 rs + | Pfcvtslu (fd, rs) -> assert Archi.ptr64; + fprintf oc " fcvt.s.lu %a, %a\n" freg fd ireg0 rs + + (* 64-bit (double-precision) floating point *) + | Pfld (fd, ra, ofs) | Pfld_a (fd, ra, ofs) -> + fprintf oc " fld %a, %a(%a)\n" freg fd offset ofs ireg ra + | Pfsd (fs, ra, ofs) | Pfsd_a (fs, ra, ofs) -> + fprintf oc " fsd %a, %a(%a)\n" freg fs offset ofs ireg ra + + | Pfnegd (fd, fs) -> + fprintf oc " fneg.d %a, %a\n" freg fd freg fs + | Pfabsd (fd, fs) -> + fprintf oc " fabs.d %a, %a\n" freg fd freg fs + + | Pfaddd (fd, fs1, fs2) -> + fprintf oc " fadd.d %a, %a, %a\n" freg fd freg fs1 freg fs2 + | Pfsubd (fd, fs1, fs2) -> + fprintf oc " fsub.d %a, %a, %a\n" freg fd freg fs1 freg fs2 + | Pfmuld (fd, fs1, fs2) -> + fprintf oc " fmul.d %a, %a, %a\n" freg fd freg fs1 freg fs2 + | Pfdivd (fd, fs1, fs2) -> + fprintf oc " fdiv.d %a, %a, %a\n" freg fd freg fs1 freg fs2 + | Pfmind (fd, fs1, fs2) -> + fprintf oc " fmin.d %a, %a, %a\n" freg fd freg fs1 freg fs2 + | Pfmaxd (fd, fs1, fs2) -> + fprintf oc " fmax.d %a, %a, %a\n" freg fd freg fs1 freg fs2 + + | Pfeqd (rd, fs1, fs2) -> + fprintf oc " feq.d %a, %a, %a\n" ireg rd freg fs1 freg fs2 + | Pfltd (rd, fs1, fs2) -> + fprintf oc " flt.d %a, %a, %a\n" ireg rd freg fs1 freg fs2 + | Pfled (rd, fs1, fs2) -> + fprintf oc " fle.d %a, %a, %a\n" ireg rd freg fs1 freg fs2 + + | Pfsqrtd (fd, fs) -> + fprintf oc " fsqrt.d %a, %a\n" freg fd freg fs + + | Pfmaddd (fd, fs1, fs2, fs3) -> + fprintf oc " fmadd.d %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 + | Pfmsubd (fd, fs1, fs2, fs3) -> + fprintf oc " fmsub.d %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 + | Pfnmaddd (fd, fs1, fs2, fs3) -> + fprintf oc " fnmadd.d %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 + | Pfnmsubd (fd, fs1, fs2, fs3) -> + fprintf oc " fnmsub.d %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 + + | Pfcvtwd (rd, fs) -> + fprintf oc " fcvt.w.d %a, %a, rtz\n" ireg rd freg fs + | Pfcvtwud (rd, fs) -> + fprintf oc " fcvt.wu.d %a, %a, rtz\n" ireg rd freg fs + | Pfcvtdw (fd, rs) -> + fprintf oc " fcvt.d.w %a, %a\n" freg fd ireg0 rs + | Pfcvtdwu (fd, rs) -> + fprintf oc " fcvt.d.wu %a, %a\n" freg fd ireg0 rs + + | Pfcvtld (rd, fs) -> assert Archi.ptr64; + fprintf oc " fcvt.l.d %a, %a, rtz\n" ireg rd freg fs + | Pfcvtlud (rd, fs) -> assert Archi.ptr64; + fprintf oc " fcvt.lu.d %a, %a, rtz\n" ireg rd freg fs + | Pfcvtdl (fd, rs) -> assert Archi.ptr64; + fprintf oc " fcvt.d.l %a, %a\n" freg fd ireg0 rs + | Pfcvtdlu (fd, rs) -> assert Archi.ptr64; + fprintf oc " fcvt.d.lu %a, %a\n" freg fd ireg0 rs + + | Pfcvtds (fd, fs) -> + fprintf oc " fcvt.d.s %a, %a\n" freg fd freg fs + | Pfcvtsd (fd, fs) -> + fprintf oc " fcvt.s.d %a, %a\n" freg fd freg fs + + (* Pseudo-instructions expanded in Asmexpand *) + | Pselectl(_, _, _, _) -> + assert false + | Pallocframe(sz, ofs) -> + assert false + | Pfreeframe(sz, ofs) -> + assert false + | Pseqw _ | Psnew _ | Pseql _ | Psnel _ | Pcvtl2w _ | Pcvtw2l _ -> + assert false + + (* Pseudo-instructions that remain *) + | Plabel lbl -> + fprintf oc "%a:\n" print_label lbl + | Ploadsymbol(rd, id, ofs) -> + loadsymbol oc rd id ofs + | Ploadsymbol_high(rd, id, ofs) -> + fprintf oc " lui %a, %%hi(%a)\n" ireg rd symbol_offset (id, ofs) + | Ploadli(rd, n) -> + let d = camlint64_of_coqint n in + let lbl = label_literal64 d in + fprintf oc " ld %a, %a %s %Lx\n" ireg rd label lbl comment d + | Ploadfi(rd, f) -> + let d = camlint64_of_coqint(Floats.Float.to_bits f) in + let lbl = label_literal64 d in + fprintf oc " fld %a, %a, x31 %s %.18g\n" + freg rd label lbl comment (camlfloat_of_coqfloat f) + | Ploadsi(rd, f) -> + let s = camlint_of_coqint(Floats.Float32.to_bits f) in + let lbl = label_literal32 s in + fprintf oc " flw %a, %a, x31 %s %.18g\n" + freg rd label lbl comment (camlfloat_of_coqfloat32 f) + | Pbtbl(r, tbl) -> + let lbl = new_label() in + fprintf oc "%s jumptable [ " comment; + List.iter (fun l -> fprintf oc "%a " print_label l) tbl; + fprintf oc "]\n"; + fprintf oc " sll x5, %a, 2\n" ireg r; + fprintf oc " la x31, %a\n" label lbl; + fprintf oc " add x5, x31, x5\n"; + fprintf oc " lw x5, 0(x5)\n"; + fprintf oc " add x5, x31, x5\n"; + fprintf oc " jr x5\n"; + jumptables := (lbl, tbl) :: !jumptables; + fprintf oc "%s end pseudoinstr btbl\n" comment | Pnop -> - fprintf oc " nop\n" - | Prep_movsl -> - fprintf oc " rep movsl\n" - | 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 - | 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) - | Pallocframe(sz, ofs_ra, ofs_link) - | Pfreeframe(sz, ofs_ra, ofs_link) -> - assert false + fprintf oc " nop\n" | Pbuiltin(ef, args, res) -> - begin match ef with - | EF_annot(kind,txt, targs) -> - begin match (P.to_int kind) with - | 1 -> let annot = annot_text preg_annot "esp" (camlstring_of_coqstring txt) args in - fprintf oc "%s annotation: %S\n" comment annot - | 2 -> let lbl = new_label () in - fprintf oc "%a:\n" label lbl; - let sp = if Archi.ptr64 then "rsp" else "esp" in - add_ais_annot lbl preg_ais_annot sp (camlstring_of_coqstring txt) args - | _ -> assert false - end + begin match ef with + | EF_annot(kind,txt, targs) -> + begin match (P.to_int kind) with + | 1 -> let annot = annot_text preg_annot "x2" (camlstring_of_coqstring txt) args in + fprintf oc "%s annotation: %S\n" comment annot + | 2 -> let lbl = new_label () in + fprintf oc "%a:\n" label lbl; + add_ais_annot lbl preg_annot "x2" (camlstring_of_coqstring txt) args + | _ -> assert false + end | EF_debug(kind, txt, targs) -> - print_debug_info comment print_file_line preg_annot "%esp" oc + print_debug_info comment print_file_line preg_annot "sp" oc (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment - | EF_profiling(id, coq_kind) -> - print_profiling_logger oc id (Z.to_int coq_kind) | _ -> assert false - end + 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 get_section_names name = + let (text, lit) = + match C2C.atom_sections name with + | t :: l :: _ -> (t, l) + | _ -> (Section_text, Section_literal) in + text,lit,Section_jumptable - let print_jumptable oc jmptbl = - let print_jumptable (lbl, tbl) = - let print_entry l = - if Archi.ptr64 then - fprintf oc " .long %a - %a\n" label (transl_label l) label lbl - else - fprintf oc " .long %a\n" label (transl_label l) - in - fprintf oc "%a:" label lbl; - List.iter print_entry tbl - in - if !jumptables <> [] then begin - section oc jmptbl; - print_align oc 4; - List.iter print_jumptable !jumptables; - jumptables := [] - end + let print_align oc alignment = + fprintf oc " .balign %d\n" alignment - let print_align = print_align + let print_jumptable oc jmptbl = + let print_tbl oc (lbl, tbl) = + fprintf oc "%a:\n" label lbl; + List.iter + (fun l -> fprintf oc " .long %a - %a\n" + print_label l label lbl) + tbl in + if !jumptables <> [] then + begin + section oc jmptbl; + fprintf oc " .balign 4\n"; + List.iter (print_tbl oc) !jumptables; + jumptables := [] + end - let print_comm_symb oc sz name align = - if C2C.atom_is_static name - then System.print_lcomm_decl oc name sz align - else System.print_comm_decl oc name sz align + let print_fun_info = elf_print_fun_info - let name_of_section = name_of_section + let print_optional_fun_info _ = () - 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 print_var_info = elf_print_var_info - let cfi_startproc = cfi_startproc - let cfi_endproc = cfi_endproc + let print_comm_symb oc sz name align = + if C2C.atom_is_static name then + fprintf oc " .local %a\n" symbol name; + fprintf oc " .comm %a, %s, %d\n" + symbol name + (Z.to_string sz) + align let print_instructions oc fn = current_function_sig := fn.fn_sig; List.iter (print_instruction oc) fn.fn_code - 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 +(* Data *) - let print_var_info = print_var_info + let address = if Archi.ptr64 then ".quad" else ".long" let print_prologue oc = - need_masks := false; + fprintf oc " .option %s\n" (if Archi.pic_code() then "pic" else "nopic"); if !Clflags.option_g then begin section oc Section_text; - if Configuration.system <> "bsd" then cfi_section oc end let print_epilogue oc = - if !need_masks then begin - section oc Section_literal; - 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 - - let default_falignment = 16 + let default_falignment = 2 - let label = label + let cfi_startproc oc = () + let cfi_endproc oc = () - let address = if Archi.ptr64 then ".quad" else ".long" - -end + end let sel_target () = - let module S = (val (match Configuration.system with - | "linux" | "bsd" -> (module ELF_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) + (module Target:TARGET) |