Support for 64-bit architectures: x86 in 64-bit mode

This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model.

To activate x86-64 bit support, configure with "x86_64-linux".

Main steps:
- Enrich Op.v and Asm.v with 64-bit operations
- SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers
- Conventions1: support x86-64 ABI in addition to the 32-bit ABI.
- Add support for the new 64-bit operations everywhere.
- runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode

To do:
- More optimizations are possible on 64-bit integer arithmetic operations.
- Could add new chunks to load, say, an unsigned byte into a 64-bit long
  (currently we load as a 32-bit int then zero-extend).
- Implements the wrong ABI for struct passing.

1 files changed, 282 insertions, 226 deletions

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