Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 -> x86/x86_32/x86_64

Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq.

This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true).  Unlike previous approaches, no other file is duplicated between these two variants of x86.

While we are at it, I renamed "ia32" into "x86" everywhere.  "ia32" is Intel speak for the 32-bit architecture.  It is not a good name to describe both the 32 and 64 bit architectures.

Finally, .depend is no longer under version control and is regenerated when the target architecture changes.  That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).

1 files changed, 881 insertions, 0 deletions

diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
new file mode 100644
index 00000000..33d47830
--- /dev/null
+++ b/x86/TargetPrinter.ml
@@ -0,0 +1,881 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 !Datatypes
+open Camlcoq
+open Sections
+open AST
+open Asm
+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 oc = function
+  | IR r -> ireg oc r
+  | FR r -> freg oc 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"
+
+(* The comment deliminiter *)
+let comment = "#"
+
+(* System dependend printer functions *)
+module type SYSTEM =
+    sig
+      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
+
+    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 | Section_small_data i ->
+          if i then ".data" else "COMM"
+      | Section_const i | Section_small_const i ->
+          if i then ".section	.rodata" else "COMM"
+      | Section_string -> ".section	.rodata"
+      | Section_literal -> ".section	.rodata.cst8,\"aM\",@progbits,8"
+      | Section_jumptable -> ".text"
+      | Section_user(s, wr, ex) ->
+          sprintf ".section	\"%s\",\"a%s%s\",@progbits"
+            s (if wr then "w" else "") (if ex then "x" else "")
+      | Section_debug_info _ -> ".section	.debug_info,\"\",@progbits"
+      | Section_debug_loc -> ".section	.debug_loc,\"\",@progbits"
+      | Section_debug_line _ -> ".section	.debug_line,\"\",@progbits"
+      | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",@progbits"
+      | Section_debug_ranges -> ".section	.debug_ranges,\"\",@progbits"
+      | Section_debug_str -> ".section	.debug_str,\"MS\",@progbits,1"
+
+    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_epilogue _ = ()
+
+    let print_comm_decl oc name sz al =
+      fprintf oc "	.comm	%a, %s, %d\n" symbol name (Z.to_string sz) al
+
+    let print_lcomm_decl oc name sz al =
+      fprintf oc "	.local	%a\n" symbol name;
+      print_comm_decl oc name sz al
+
+  end
+
+(* Printer functions for MacOS *)
+module MacOS_System : SYSTEM =
+  struct
+
+    let raw_symbol oc s =
+     fprintf oc "_%s" s
+
+    let symbol oc symb =
+      raw_symbol oc (extern_atom symb)
+
+    let label oc lbl =
+      fprintf oc "L%d" lbl
+
+    let name_of_section = function
+      | Section_text -> ".text"
+      | Section_data i | Section_small_data i ->
+          if i then ".data" else "COMM"
+      | Section_const i  | Section_small_const i ->
+          if i then ".const" else "COMM"
+      | Section_string -> ".const"
+      | Section_literal -> ".literal8"
+      | Section_jumptable -> ".const"
+      | 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"
+
+
+    let stack_alignment =  16 (* mandatory *)
+
+    (* 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)
+
+    let print_align oc n =
+      fprintf oc "	.align	%d\n" (log2 n)
+
+    let indirect_symbols : StringSet.t ref = ref StringSet.empty
+
+    let print_mov_rs oc rd id =
+      if Archi.ptr64 then begin
+        fprintf oc "	movq    %a@GOTPCREL(%%rip), %a\n" symbol id ireg64 rd
+      end else begin
+        let id = extern_atom id in
+        indirect_symbols := StringSet.add id !indirect_symbols;
+        fprintf oc "	movl	L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd
+      end
+
+    let print_fun_info _ _ = ()
+
+    let print_var_info _ _ = ()
+
+    let print_epilogue oc =
+      if not Archi.ptr64 then begin
+        fprintf oc "	.section __IMPORT,__pointers,non_lazy_symbol_pointers\n";
+        StringSet.iter
+          (fun s ->
+            fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s;
+            fprintf oc "	.indirect_symbol %a\n" raw_symbol s;
+            fprintf oc "	.long	0\n")
+          !indirect_symbols;
+        indirect_symbols := StringSet.empty
+      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) (log2 al)
+
+  end
+
+
+module Target(System: SYSTEM):TARGET =
+  struct
+    open System
+    let symbol = symbol
+
+(*  Basic printing functions *)
+
+    let symbol_offset oc (symb, ofs) =
+      symbol oc symb;
+      let ofs = Z.to_int64 ofs in
+      if ofs <> 0L then fprintf oc " + %Ld" ofs
+
+    let addressing_gen ireg oc (Addrmode(base, shift, cst)) =
+      begin match cst with
+      | Coq_inl n ->
+          fprintf oc "%s" (Z.to_string n)
+      | 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 = new_label() in
+        float64_literals := (lbl, n1) :: !float64_literals;
+        fprintf oc "%a(%%rip)" label lbl
+      end
+
+
+
+(* Printing of instructions *)
+
+(* Reminder on AT&T syntax: op source, dest *)
+
+    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 = new_label() in
+          fprintf oc "	movsd	%a%s, %a %s %.18g\n"
+                     label lbl rip_rel
+                     freg rd comment (camlfloat_of_coqfloat n);
+          float64_literals := (lbl, b) :: !float64_literals
+      | 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 = new_label() in
+          fprintf oc "	movss	%a%s, %a %s %.18g\n"
+                     label lbl rip_rel
+                     freg rd comment (camlfloat_of_coqfloat32 n);
+          float32_literals := (lbl, b) :: !float32_literals
+      | 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	0(%%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 a1 freg a2 freg res
+      | Pfmadd213 (res,a1,a2) ->
+	 fprintf oc "	vfmadd213sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfmadd231 (res,a1,a2) ->
+	 fprintf oc "	vfmadd231sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfmsub132 (res,a1,a2) ->
+	 fprintf oc "	vfmsub132sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfmsub213 (res,a1,a2) ->
+	 fprintf oc "	vfmsub213sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfmsub231 (res,a1,a2) ->
+	 fprintf oc "	vfmsub231sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmadd132 (res,a1,a2) ->
+	 fprintf oc "	vfnmadd132sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmadd213 (res,a1,a2) ->
+	 fprintf oc "	vfnmadd213sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmadd231 (res,a1,a2) ->
+	 fprintf oc "	vfnmadd231sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmsub132 (res,a1,a2) ->
+	 fprintf oc "	vfnmsub132sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmsub213 (res,a1,a2) ->
+	 fprintf oc "	vfnmsub213sd	%a, %a, %a\n" freg a1 freg a2 freg res
+      | Pfnmsub231 (res,a1,a2) ->
+	 fprintf oc "	vfnmsub231sd	%a, %a, %a\n" freg a1 freg a2 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
+      | 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
+      | 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(txt, targs) ->
+              fprintf oc "%s annotation: " comment;
+              print_annot_text preg "%esp" oc (camlstring_of_coqstring txt) args
+          | EF_debug(kind, txt, targs) ->
+              print_debug_info comment print_file_line preg "%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 oc (camlstring_of_coqstring txt) sg args res;
+              fprintf oc "%s end inline assembly\n" comment
+          | _ ->
+              assert false
+          end
+
+    let print_literal64 oc (lbl, n) =
+      fprintf oc "%a:	.quad	0x%Lx\n" label lbl n
+    let print_literal32 oc (lbl, n) =
+      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_init oc = function
+      | Init_int8 n ->
+          fprintf oc "	.byte	%ld\n" (camlint_of_coqint n)
+      | Init_int16 n ->
+          fprintf oc "	.short	%ld\n" (camlint_of_coqint n)
+      | Init_int32 n ->
+          fprintf oc "	.long	%ld\n" (camlint_of_coqint n)
+      | Init_int64 n ->
+          fprintf oc "	.quad	%Ld\n" (camlint64_of_coqint n)
+      | Init_float32 n ->
+          fprintf oc "	.long	%ld %s %.18g\n"
+	    (camlint_of_coqint (Floats.Float32.to_bits n))
+	    comment (camlfloat_of_coqfloat32 n)
+      | Init_float64 n ->
+          fprintf oc "	.quad	%Ld %s %.18g\n"
+	    (camlint64_of_coqint (Floats.Float.to_bits n))
+	    comment (camlfloat_of_coqfloat n)
+      | Init_space n ->
+          if Z.gt n Z.zero then
+            fprintf oc "	.space	%a\n" z n
+      | Init_addrof(symb, ofs) ->
+          fprintf oc "	%s	%a\n" data_pointer symbol_offset (symb, ofs)
+
+    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 !float64_literals <> [] || !float32_literals <> [] then begin
+         section oc lit;
+         print_align oc 8;
+         List.iter (print_literal64 oc) !float64_literals;
+         float64_literals := [];
+         List.iter (print_literal32 oc) !float32_literals;
+         float32_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 reset_constants = reset_constants
+
+    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_const true);
+        (* not Section_literal because not 8-bytes *)
+        print_align oc 16;
+        fprintf oc "%a:	.quad   0x8000000000000000, 0\n"
+          raw_symbol "__negd_mask";
+        fprintf oc "%a:	.quad   0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n"
+          raw_symbol "__absd_mask";
+        fprintf oc "%a:	.long   0x80000000, 0, 0, 0\n"
+          raw_symbol "__negs_mask";
+        fprintf oc "%a:	.long   0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n"
+          raw_symbol "__abss_mask"
+      end;
+      System.print_epilogue oc;
+      if !Clflags.option_g then begin
+        Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
+        section oc Section_text;
+      end
+
+    let comment = comment
+
+    let default_falignment = 16
+
+    let label = label
+
+    let new_label = new_label
+
+end
+
+let sel_target () =
+ let module S = (val (match Configuration.system with
+  | "macosx" -> (module MacOS_System:SYSTEM)
+  | "linux"
+  | "bsd" -> (module ELF_System:SYSTEM)
+  | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")  ):SYSTEM) in
+ (module Target(S):TARGET)