(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  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.     *)
(*                                                                     *)
(* *********************************************************************)

(* Printing x86-64 assembly code in asm syntax *)

open Printf
open Camlcoq
open Sections
open AST
open Asm
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 =
  struct

    (* The comment delimiter *)
    let comment = "#"

    let raw_symbol oc s =
      fprintf oc "%s" s

    let symbol = elf_symbol

    let label = elf_label

    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	.rodata" i
      | 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 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 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

    let print_epilogue oc =
      if Archi.ptr64 then begin
        StringSet.iter (declare_indirect_symbol oc) !indirect_symbols;
        indirect_symbols := StringSet.empty
      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


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
      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 rip_rel =
      if Archi.ptr64 then "(%rip)" else ""

(* Large 64-bit immediates (bigger than a 32-bit signed integer) are
   not supported by the processor.  Turn them into memory operands. *)

    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 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
      | 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
      | 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
          | EF_debug(kind, txt, targs) ->
              print_debug_info comment print_file_line preg_annot "%esp" 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

    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 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 = print_align

    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 name_of_section = name_of_section

    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 cfi_startproc = cfi_startproc
    let cfi_endproc = cfi_endproc

    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

    let print_var_info = print_var_info

    let print_prologue oc =
      need_masks := false;
      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 label = label

    let address = if Archi.ptr64 then ".quad" else ".long"

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)