Changed the ia32 backend to the new Printer.

5 files changed, 983 insertions, 1035 deletions

diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 381ef5df..8812d320 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -69,6 +69,11 @@ let float64_literals : (int * int64) list ref = ref []
 let float32_literals : (int * int32) list ref = ref []
 let jumptables : (int * label list) list ref = ref []
 
+let reset_constants () =
+  float64_literals := [];
+  float32_literals := [];
+  jumptables := []
+
 (* Variables used for the handling of varargs *)
 
 let current_function_stacksize = ref 0l
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
deleted file mode 100644
index 4c845b92..00000000
--- a/ia32/PrintAsm.ml
+++ /dev/null
@@ -1,1017 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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 IA32 assembly code in asm syntax *)
-
-open Printf
-open Datatypes
-open Camlcoq
-open Sections
-open AST
-open Memdata
-open Asm
-open PrintAsmaux
-
-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 int8_reg_name = function
-  | EAX -> "%al"  | EBX -> "%bl"  | ECX -> "%cl"  | EDX -> "%dl"
-  | _ -> assert false
-
-let high_int8_reg_name = function
-  | EAX -> "%ah"  | EBX -> "%bh"  | ECX -> "%ch"  | EDX -> "%dh"
-  | _ -> assert false
-
-let int16_reg_name = function
-  | EAX -> "%ax"  | EBX -> "%bx"  | ECX -> "%cx"  | EDX -> "%dx"
-  | ESI -> "%si"  | EDI -> "%di"  | EBP -> "%bp"  | ESP -> "%sp"
-
-let float_reg_name = function
-  | XMM0 -> "%xmm0"  | XMM1 -> "%xmm1"  | XMM2 -> "%xmm2"  | XMM3 -> "%xmm3"
-  | XMM4 -> "%xmm4"  | XMM5 -> "%xmm5"  | XMM6 -> "%xmm6"  | XMM7 -> "%xmm7"
-
-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 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
-
-
-(* 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_ra: 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 cygwin *)
-module Cygwin_System =
-  (struct
-
-    let raw_symbol oc s =
-       fprintf oc "_%s" s
-
-    let symbol = symbol
-
-    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")
-
-    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:SYSTEM)
-
-(* Printer functions for ELF *)
-module ELF_System =
-  (struct
-    
-    let raw_symbol oc s =
-      fprintf oc "%s" s
-  
-    let symbol = symbol
-
-    let label = 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 "")
-            
-    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 = print_fun_info
-      
-    let print_var_info = 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:SYSTEM)
-
-(* Printer functions for MacOS *)
-module MacOS_System =
-  (struct
-    
-    let raw_symbol oc s =
-     fprintf oc "_%s" s
-
-    let symbol oc symb =
-      fprintf oc "_%s" (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")
-    
-    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_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_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_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:SYSTEM)
-
-
-module AsmPrinter(Target: SYSTEM) =
-  (struct
-    open Target
-
-(*  Basic printing functions *)
-
-let symbol_offset oc (symb, ofs) =
-  symbol oc symb;
-  if ofs <> 0l then fprintf oc " + %ld" ofs
-
-
-let addressing oc (Addrmode(base, shift, cst)) =
-  begin match cst with
-  | Coq_inl n ->
-      let n = camlint_of_coqint n in
-      fprintf oc "%ld" 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
-  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
-  end
-
-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)
-
-(* SP adjustment to allocate or free a stack frame *)
-
-let int32_align n a =
-  if n >= 0l
-  then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a))
-  else Int32.logand n (Int32.of_int (-a))
-
-let sp_adjustment sz =
-  let sz = camlint_of_coqint sz in
-  (* Preserve proper alignment of the stack *)
-  let sz = int32_align sz stack_alignment in
-  (* The top 4 bytes have already been allocated by the "call" instruction. *)
-  let sz = Int32.sub sz 4l in
-  sz
-
-(* 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)
-
-(* Emit a align directive *)
-
-let need_masks = ref false
-
-(* Emit .file / .loc debugging directives *)
-
-let print_file_line oc file line =
-  PrintAnnot.print_file_line oc comment file line
-
-let print_location oc loc =
-  if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
-
-
-(* 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. *)
-
-(* Handling of annotations *)
-
-let print_annot_stmt oc txt targs args =
-  if Str.string_match re_file_line txt 0 then begin
-    print_file_line oc (Str.matched_group 1 txt)
-                       (int_of_string (Str.matched_group 2 txt))
-  end else begin
-    fprintf oc "%s annotation: " comment;
-    PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args
-  end
-
-let print_annot_val oc txt args res =
-  fprintf oc "%s annotation: " comment;
-  PrintAnnot.print_annot_val preg oc txt args;
-  match args, res with
-  | [IR src], [IR dst] ->
-      if dst <> src then fprintf oc "	movl	%a, %a\n" ireg src ireg dst
-  | [FR src], [FR dst] ->
-      if dst <> src then fprintf oc "	movapd	%a, %a\n" freg src freg dst
-  | _, _ -> assert false
-
-(* Handling of memcpy *)
-
-(* Unaligned memory accesses are quite fast on IA32, so use large
-   memory accesses regardless of alignment. *)
-
-let print_builtin_memcpy_small oc sz al src dst =
-  assert (src = EDX && dst = EAX);
-  let rec copy ofs sz =
-    if sz >= 8 && !Clflags.option_ffpu then begin
-      fprintf oc "	movq	%d(%a), %a\n" ofs ireg src freg XMM7;
-      fprintf oc "	movq	%a, %d(%a)\n" freg XMM7 ofs ireg dst;
-      copy (ofs + 8) (sz - 8)
-    end else if sz >= 4 then begin
-      fprintf oc "	movl	%d(%a), %a\n" ofs ireg src ireg ECX;
-      fprintf oc "	movl	%a, %d(%a)\n" ireg ECX ofs ireg dst;
-      copy (ofs + 4) (sz - 4)
-    end else if sz >= 2 then begin
-      fprintf oc "	movw	%d(%a), %a\n" ofs ireg src ireg16 ECX;
-      fprintf oc "	movw	%a, %d(%a)\n" ireg16 ECX ofs ireg dst;
-      copy (ofs + 2) (sz - 2)
-    end else if sz >= 1 then begin
-      fprintf oc "	movb	%d(%a), %a\n" ofs ireg src ireg8 ECX;
-      fprintf oc "	movb	%a, %d(%a)\n" ireg8 ECX ofs ireg dst;
-      copy (ofs + 1) (sz - 1)
-    end in
-  copy 0 sz
-
-let print_builtin_memcpy_big oc sz al src dst =
-  assert (src = ESI && dst = EDI);
-  fprintf oc "	movl	$%d, %a\n" (sz / 4) ireg ECX;
-  fprintf oc "	rep	movsl\n";
-  if sz mod 4 >= 2 then fprintf oc "	movsw\n";
-  if sz mod 2 >= 1 then fprintf oc "	movsb\n"
-
-let print_builtin_memcpy oc sz al args =
-  let (dst, src) =
-    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
-  fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n"
-          comment sz al;
-  if sz <= 32
-  then print_builtin_memcpy_small oc sz al src dst
-  else print_builtin_memcpy_big oc sz al src dst;
-  fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment
-
-(* Handling of volatile reads and writes *)
-
-let offset_addressing (Addrmode(base, ofs, cst)) delta =
-  Addrmode(base, ofs,
-           match cst with
-           | Coq_inl n -> Coq_inl(Integers.Int.add n delta)
-           | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta))
-
-let print_builtin_vload_common oc chunk addr res =
-  match chunk, res with
-  | Mint8unsigned, [IR res] ->
-      fprintf oc "	movzbl	%a, %a\n" addressing addr ireg res
-  | Mint8signed, [IR res] ->
-      fprintf oc "	movsbl	%a, %a\n" addressing addr ireg res
-  | Mint16unsigned, [IR res] ->
-      fprintf oc "	movzwl	%a, %a\n" addressing addr ireg res
-  | Mint16signed, [IR res] ->
-      fprintf oc "	movswl	%a, %a\n" addressing addr ireg res
-  | Mint32, [IR res] ->
-      fprintf oc "	movl	%a, %a\n" addressing addr ireg res
-  | Mint64, [IR res1; IR res2] ->
-      let addr' = offset_addressing addr (coqint_of_camlint 4l) in
-      if not (Asmgen.addressing_mentions addr res2) then begin
-        fprintf oc "	movl	%a, %a\n" addressing addr ireg res2;
-        fprintf oc "	movl	%a, %a\n" addressing addr' ireg res1
-      end else begin
-        fprintf oc "	movl	%a, %a\n" addressing addr' ireg res1;
-        fprintf oc "	movl	%a, %a\n" addressing addr ireg res2
-      end
-  | Mfloat32, [FR res] ->
-      fprintf oc "	movss	%a, %a\n" addressing addr freg res
-  | Mfloat64, [FR res] ->
-      fprintf oc "	movsd	%a, %a\n" addressing addr freg res
-  | _ ->
-      assert false
-
-let print_builtin_vload oc chunk args res =
-  fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
-  begin match args with
-  | [IR addr] ->
-      print_builtin_vload_common oc chunk
-                 (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) res
-  | _ ->
-      assert false
-  end;
-  fprintf oc "%s end builtin __builtin_volatile_read\n" comment
-
-let print_builtin_vload_global oc chunk id ofs args res =
-  fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
-  print_builtin_vload_common oc chunk
-                 (Addrmode(None, None, Coq_inr(id,ofs))) res;
-  fprintf oc "%s end builtin __builtin_volatile_read\n" comment
-
-let print_builtin_vstore_common oc chunk addr src tmp =
-  match chunk, src with
-  | (Mint8signed | Mint8unsigned), [IR src] ->
-      if Asmgen.low_ireg src then
-        fprintf oc "	movb	%a, %a\n" ireg8 src addressing addr
-      else begin
-        fprintf oc "	movl	%a, %a\n" ireg src ireg tmp;
-        fprintf oc "	movb	%a, %a\n" ireg8 tmp addressing addr
-      end
-  | (Mint16signed | Mint16unsigned), [IR src] ->
-      fprintf oc "	movw	%a, %a\n" ireg16 src addressing addr
-  | Mint32, [IR src] ->
-      fprintf oc "	movl	%a, %a\n" ireg src addressing addr
-  | Mint64, [IR src1; IR src2] ->
-      let addr' = offset_addressing addr (coqint_of_camlint 4l) in
-      fprintf oc "	movl	%a, %a\n" ireg src2 addressing addr;
-      fprintf oc "	movl	%a, %a\n" ireg src1 addressing addr'
-  | Mfloat32, [FR src] ->
-      fprintf oc "	movss	%a, %a\n" freg src addressing addr
-  | Mfloat64, [FR src] ->
-      fprintf oc "	movsd	%a, %a\n" freg src addressing addr
-  | _ ->
-      assert false
-
-let print_builtin_vstore oc chunk args =
-  fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
-  begin match args with
-  | IR addr :: src ->
-      print_builtin_vstore_common oc chunk
-                 (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src
-                 (if addr = EAX then ECX else EAX)
-  | _ ->
-      assert false
-  end;
-  fprintf oc "%s end builtin __builtin_volatile_write\n" comment
-
-let print_builtin_vstore_global oc chunk id ofs args =
-  fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
-  print_builtin_vstore_common oc chunk
-                 (Addrmode(None, None, Coq_inr(id,ofs))) args EAX;
-  fprintf oc "%s end builtin __builtin_volatile_write\n" comment
-
-(* Handling of varargs *)
-
-let print_builtin_va_start oc r =
-  if not (!current_function_sig).sig_cc.cc_vararg then
-    invalid_arg "Fatal error: va_start used in non-vararg function";
-  let ofs =
-    Int32.(add (add !current_function_stacksize 4l)
-               (mul 4l (Z.to_int32 (Conventions1.size_arguments
-                                           !current_function_sig)))) in
-  fprintf oc "	movl	%%esp, 0(%a)\n" ireg r;
-  fprintf oc "	addl	$%ld, 0(%a)\n" ofs ireg r
-
-(* Handling of compiler-inlined builtins *)
-
-let print_builtin_inline oc name args res =
-  fprintf oc "%s begin builtin %s\n" comment name;
-  begin match name, args, res with
-  (* Integer arithmetic *)
-  | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] ->
-      if a1 <> res then
-        fprintf oc "	movl	%a, %a\n" ireg a1 ireg res;
-      fprintf oc "	bswap	%a\n" ireg res
-  | "__builtin_bswap16", [IR a1], [IR res] ->
-      if a1 <> res then
-        fprintf oc "	movl	%a, %a\n" ireg a1 ireg res;
-      fprintf oc "	rolw	$8, %a\n" ireg16 res
-  | "__builtin_clz", [IR a1], [IR res] ->
-      fprintf oc "	bsrl	%a, %a\n" ireg a1 ireg res;
-      fprintf oc "	xorl	$31, %a\n" ireg res
-  | "__builtin_ctz", [IR a1], [IR res] ->
-      fprintf oc "	bsfl	%a, %a\n" ireg a1 ireg res
-  (* Float arithmetic *)
-  | "__builtin_fabs", [FR a1], [FR res] ->
-      need_masks := true;
-      if a1 <> res then
-        fprintf oc "	movapd	%a, %a\n" freg a1 freg res;
-      fprintf oc "	andpd	%a, %a\n" raw_symbol "__absd_mask" freg res
-  | "__builtin_fsqrt", [FR a1], [FR res] ->
-      fprintf oc "	sqrtsd	%a, %a\n" freg a1 freg res
-  | "__builtin_fmax", [FR a1; FR a2], [FR res] ->
-      if res = a1 then
-        fprintf oc "	maxsd	%a, %a\n" freg a2 freg res
-      else if res = a2 then
-        fprintf oc "	maxsd	%a, %a\n" freg a1 freg res
-      else begin
-        fprintf oc "	movapd	%a, %a\n" freg a1 freg res;
-        fprintf oc "	maxsd	%a, %a\n" freg a2 freg res
-      end
-  | "__builtin_fmin", [FR a1; FR a2], [FR res] ->
-      if res = a1 then
-        fprintf oc "	minsd	%a, %a\n" freg a2 freg res
-      else if res = a2 then
-        fprintf oc "	minsd	%a, %a\n" freg a1 freg res
-      else begin
-        fprintf oc "	movapd	%a, %a\n" freg a1 freg res;
-        fprintf oc "	minsd	%a, %a\n" freg a2 freg res
-      end
-  | ("__builtin_fmadd"|"__builtin_fmsub"|"__builtin_fnmadd"|"__builtin_fnmsub"),
-    [FR a1; FR a2; FR a3], [FR res] ->
-      let opcode =
-        match name with
-        | "__builtin_fmadd" -> "vfmadd"
-        | "__builtin_fmsub" -> "vfmsub"
-        | "__builtin_fnmadd" -> "vfnmadd"
-        | "__builtin_fnmsub" -> "vfnmsub"
-        | _ -> assert false in
-      if res = a1 then
-        fprintf oc "	%s132sd	%a, %a, %a\n" opcode freg a2 freg a3 freg res
-      else if res = a2 then
-        fprintf oc "	%s213sd	%a, %a, %a\n" opcode freg a3 freg a1 freg res
-      else if res = a3 then
-        fprintf oc "	%s231sd	%a, %a, %a\n" opcode freg a1 freg a2 freg res
-      else begin
-        fprintf oc "	movapd	%a, %a\n" freg a3 freg res;
-        fprintf oc "	%s231sd	%a, %a, %a\n" opcode freg a1 freg a2 freg res
-      end
-  (* 64-bit integer arithmetic *)
-  | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
-      assert (ah = EDX && al = EAX && rh = EDX && rl = EAX);
-      fprintf oc "	negl	%a\n" ireg EAX;
-      fprintf oc "	adcl	$0, %a\n" ireg EDX;
-      fprintf oc "	negl	%a\n" ireg EDX
-  | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
-      assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX);
-      fprintf oc "	addl	%a, %a\n" ireg EBX ireg EAX;
-      fprintf oc "	adcl	%a, %a\n" ireg ECX ireg EDX
-  | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
-      assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX);
-      fprintf oc "	subl	%a, %a\n" ireg EBX ireg EAX;
-      fprintf oc "	sbbl	%a, %a\n" ireg ECX ireg EDX
-  | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
-      assert (a = EAX && b = EDX && rh = EDX && rl = EAX);
-      fprintf oc "	mull    %a\n" ireg EDX
-  (* Memory accesses *)
-  | "__builtin_read16_reversed", [IR a1], [IR res] ->
-      fprintf oc "	movzwl	0(%a), %a\n" ireg a1 ireg res;
-      fprintf oc "	rolw	$8, %a\n" ireg16 res
-  | "__builtin_read32_reversed", [IR a1], [IR res] ->
-      fprintf oc "	movl	0(%a), %a\n" ireg a1 ireg res;
-      fprintf oc "	bswap	%a\n" ireg res
-  | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
-      let tmp = if a1 = ECX then EDX else ECX in
-      if a2 <> tmp then
-        fprintf oc "	movl	%a, %a\n" ireg a2 ireg tmp;
-      fprintf oc "	xchg	%a, %a\n" ireg8 tmp high_ireg8 tmp;
-      fprintf oc "	movw	%a, 0(%a)\n" ireg16 tmp ireg a1
-  | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
-      let tmp = if a1 = ECX then EDX else ECX in
-      if a2 <> tmp then
-        fprintf oc "	movl	%a, %a\n" ireg a2 ireg tmp;
-      fprintf oc "	bswap	%a\n" ireg tmp;
-      fprintf oc "	movl	%a, 0(%a)\n" ireg tmp ireg a1
-  (* Synchronization *)
-  | "__builtin_membar", [], _ ->
-      ()
-  (* Vararg stuff *)
-  | "__builtin_va_start", [IR a], _ ->
-      print_builtin_va_start oc a
-  (* Catch-all *)  
-  | _ ->
-      invalid_arg ("unrecognized builtin " ^ name)
-  end;
-  fprintf oc "%s end builtin %s\n" comment name
-
-(* Printing of instructions *)
-
-(* Reminder on AT&T syntax: op source, dest *)
-
-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
-  | 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, %a %s %.18g\n" label lbl 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, %a %s %.18g\n" label lbl 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
-  | 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
-  | Pmovzb_rm(rd, a) ->
-      fprintf oc "	movzbl	%a, %a\n" addressing a ireg rd
-  | Pmovsb_rr(rd, r1) ->
-      fprintf oc "	movsbl	%a, %a\n" ireg8 r1 ireg rd
-  | Pmovsb_rm(rd, a) ->
-      fprintf oc "	movsbl	%a, %a\n" addressing a ireg rd
-  | Pmovzw_rr(rd, r1) ->
-      fprintf oc "	movzwl	%a, %a\n" ireg16 r1 ireg rd
-  | Pmovzw_rm(rd, a) ->
-      fprintf oc "	movzwl	%a, %a\n" addressing a ireg rd
-  | Pmovsw_rr(rd, r1) ->
-      fprintf oc "	movswl	%a, %a\n" ireg16 r1 ireg rd
-  | Pmovsw_rm(rd, a) ->
-      fprintf oc "	movswl	%a, %a\n" addressing a ireg rd
-  | 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
-  | Pcvtsi2sd_fr(rd, r1) ->
-      fprintf oc "	cvtsi2sd %a, %a\n" ireg r1 freg rd
-  | Pcvttss2si_rf(rd, r1) ->
-      fprintf oc "	cvttss2si %a, %a\n" freg r1 ireg rd
-  | Pcvtsi2ss_fr(rd, r1) ->
-      fprintf oc "	cvtsi2ss %a, %a\n" ireg 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
-  | Pdiv(r1) ->
-      fprintf oc "	xorl	%%edx, %%edx\n";
-      fprintf oc "	divl	%a\n" ireg r1
-  | Pidiv(r1) ->
-      fprintf oc "	cltd\n";
-      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
-  | 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
-  | 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
-  (** 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, %a\n" raw_symbol "__negd_mask" freg rd
-  | Pabsd (rd) ->
-      need_masks := true;
-      fprintf oc "	andpd	%a, %a\n" raw_symbol "__absd_mask" 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, %a\n" raw_symbol "__negs_mask" freg rd
-  | Pabss (rd) ->
-      need_masks := true;
-      fprintf oc "	andpd	%a, %a\n" raw_symbol "__abss_mask" 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
-      fprintf oc "	jmp	*%a(, %a, 4)\n" label l ireg r;
-      jumptables := (l, tbl) :: !jumptables
-  | Pcall_s(f, sg) ->
-      fprintf oc "	call	%a\n" symbol f
-  | Pcall_r(r, sg) ->
-      fprintf oc "	call	*%a\n" ireg r
-  | Pret ->
-      fprintf oc "	ret\n"
-  (** Pseudo-instructions *)
-  | Plabel(l) ->
-      fprintf oc "%a:\n" label (transl_label l)
-  | Pallocframe(sz, ofs_ra, ofs_link) ->
-      let sz = sp_adjustment sz in
-      let ofs_link = camlint_of_coqint ofs_link in
-      fprintf oc "	subl	$%ld, %%esp\n" sz;
-      cfi_adjust oc sz;
-      fprintf oc "	leal	%ld(%%esp), %%edx\n" (Int32.add sz 4l);
-      fprintf oc "	movl	%%edx, %ld(%%esp)\n" ofs_link;
-      current_function_stacksize := sz
-  | Pfreeframe(sz, ofs_ra, ofs_link) ->
-      let sz = sp_adjustment sz in
-      fprintf oc "	addl	$%ld, %%esp\n" sz
-  | Pbuiltin(ef, args, res) ->
-      begin match ef with
-      | EF_builtin(name, sg) ->
-          print_builtin_inline oc (extern_atom name) args res
-      | EF_vload chunk ->
-          print_builtin_vload oc chunk args res
-      | EF_vstore chunk ->
-          print_builtin_vstore oc chunk args
-      | EF_vload_global(chunk, id, ofs) ->
-          print_builtin_vload_global oc chunk id ofs args res
-      | EF_vstore_global(chunk, id, ofs) ->
-          print_builtin_vstore_global oc chunk id ofs args
-      | EF_memcpy(sz, al) ->
-          print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz))
-                                  (Int32.to_int (camlint_of_coqint al)) args
-      | EF_annot_val(txt, targ) ->
-          print_annot_val oc (extern_atom txt) args res
-      | EF_inline_asm txt ->
-          fprintf oc "%s begin inline assembly\n" comment;
-          fprintf oc "	%s\n" (extern_atom txt);
-          fprintf oc "%s end inline assembly\n" comment
-      | _ ->
-          assert false
-      end
-  | Pannot(ef, args) ->
-      begin match ef with
-      | EF_annot(txt, targs) ->
-          print_annot_stmt oc (extern_atom txt) targs args
-      | _ ->
-          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 (lbl, tbl) =
-  fprintf oc "%a:" label lbl;
-  List.iter
-    (fun l -> fprintf oc "	.long	%a\n" label (transl_label l))
-    tbl
-
-let print_function oc name fn =
-  Hashtbl.clear current_function_labels;
-  float64_literals := []; float32_literals := [];
-  jumptables := [];
-  current_function_sig := fn.fn_sig;
-  let (text, lit, jmptbl) =
-    match C2C.atom_sections name with
-    | [t;l;j] -> (t, l, j)
-    |    _    -> (Section_text, Section_literal, Section_jumptable) in
-  section oc text;
-  let alignment =
-    match !Clflags.option_falignfunctions with Some n -> n | None -> 16 in
-  print_align oc alignment;
-  if not (C2C.atom_is_static name) then
-    fprintf oc "	.globl %a\n" symbol name;
-  fprintf oc "%a:\n" symbol name;
-  print_location oc (C2C.atom_location name);
-  cfi_startproc oc;
-  List.iter (print_instruction oc) fn.fn_code;
-  cfi_endproc oc;
-  print_fun_info oc name;
-  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;
-  if !jumptables <> [] then begin
-    section oc jmptbl;
-    print_align oc 4;
-    List.iter (print_jumptable oc) !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_coqfloat 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	%s\n" (Z.to_string n)
-  | Init_addrof(symb, ofs) ->
-      fprintf oc "	.long	%a\n" 
-                 symbol_offset (symb, camlint_of_coqint ofs)
-
-let print_init_data oc name id =
-  if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
-  && List.for_all (function Init_int8 _ -> true | _ -> false) id
-  then
-    fprintf oc "	.ascii	\"%s\"\n" (PrintCsyntax.string_of_init id)
-  else
-    List.iter (print_init oc) id
-
-let print_var oc name v =
-  match v.gvar_init with
-  | [] -> ()
-  | _  ->
-      let sec =
-        match C2C.atom_sections name with
-        | [s] -> s
-        |  _  -> Section_data true
-      and align =
-        match C2C.atom_alignof name with
-        | Some a -> a
-        | None -> 8 in (* 8-alignment is a safe default *)
-      let name_sec =
-        name_of_section sec in
-      if name_sec <> "COMM" then begin
-        fprintf oc "	%s\n" name_sec;
-        print_align oc align;
-        if not (C2C.atom_is_static name) then
-          fprintf oc "	.globl	%a\n" symbol name;
-        fprintf oc "%a:\n" symbol name;
-        print_init_data oc name v.gvar_init;
-        print_var_info oc name
-      end else begin
-        let sz =
-          match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
-        if C2C.atom_is_static name
-        then Target.print_lcomm_decl oc name sz align
-        else Target.print_comm_decl oc name sz align
-      end
-
-let print_globdef oc (name, gdef) =
-  match gdef with
-  | Gfun(Internal code) -> print_function oc name code
-  | Gfun(External ef) -> ()
-  | Gvar v -> print_var oc name v
-end)
-
-type target = ELF | MacOS | Cygwin
-
-let print_program oc p =
-  let target =   
-    match Configuration.system with
-    | "macosx" -> MacOS
-    | "linux"  -> ELF
-    | "bsd"    -> ELF
-    | "cygwin" -> Cygwin
-    | _        -> invalid_arg ("System " ^ Configuration.system ^ " not supported") in
-  let module Target = (val (match target with
-  | MacOS -> (module MacOS_System:SYSTEM)
-  | ELF -> (module ELF_System:SYSTEM)
-  | Cygwin -> (module Cygwin_System:SYSTEM)):SYSTEM) in
-  let module Printer = AsmPrinter(Target) in
-  PrintAnnot.print_version_and_options oc comment;
-  PrintAnnot.reset_filenames();
-  Printer.need_masks := false;
-  List.iter (Printer.print_globdef oc) p.prog_defs;
-  if !Printer.need_masks then begin
-    Printer.section oc (Section_const true);
-                        (* not Section_literal because not 8-bytes *)
-    Target.print_align oc 16;
-    fprintf oc "%a:	.quad   0x8000000000000000, 0\n"
-               Target.raw_symbol "__negd_mask";
-    fprintf oc "%a:	.quad   0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n"
-               Target.raw_symbol "__absd_mask";
-    fprintf oc "%a:	.long   0x80000000, 0, 0, 0\n"
-               Target.raw_symbol "__negs_mask";
-    fprintf oc "%a:	.long   0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n"
-               Target.raw_symbol "__abss_mask"
-  end;
-  Target.print_epilogue oc;
-  PrintAnnot.close_filenames()
diff --git a/ia32/PrintAsm.mli b/ia32/PrintAsm.mli
deleted file mode 100644
index aefe3a0a..00000000
--- a/ia32/PrintAsm.mli
+++ /dev/null
@@ -1,13 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-val print_program: out_channel -> Asm.program -> unit
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
new file mode 100644
index 00000000..5bb0eec4
--- /dev/null
+++ b/ia32/TargetPrinter.ml
@@ -0,0 +1,976 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 IA32 assembly code in asm syntax *)
+
+open Printf
+open Datatypes
+open Camlcoq
+open Sections
+open AST
+open Memdata
+open Asm
+open PrintAsmaux
+
+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 int8_reg_name = function
+  | EAX -> "%al"  | EBX -> "%bl"  | ECX -> "%cl"  | EDX -> "%dl"
+  | _ -> assert false
+
+let high_int8_reg_name = function
+  | EAX -> "%ah"  | EBX -> "%bh"  | ECX -> "%ch"  | EDX -> "%dh"
+  | _ -> assert false
+
+let int16_reg_name = function
+  | EAX -> "%ax"  | EBX -> "%bx"  | ECX -> "%cx"  | EDX -> "%dx"
+  | ESI -> "%si"  | EDI -> "%di"  | EBP -> "%bp"  | ESP -> "%sp"
+
+let float_reg_name = function
+  | XMM0 -> "%xmm0"  | XMM1 -> "%xmm1"  | XMM2 -> "%xmm2"  | XMM3 -> "%xmm3"
+  | XMM4 -> "%xmm4"  | XMM5 -> "%xmm5"  | XMM6 -> "%xmm6"  | XMM7 -> "%xmm7"
+
+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 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
+
+
+(* 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_ra: out_channel -> ireg -> ident -> unit
+      val print_fun_info: bool
+      val print_var_info: bool
+      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 cygwin *)
+module Cygwin_System =
+  (struct
+
+    let raw_symbol oc s =
+       fprintf oc "_%s" s
+
+    let symbol = symbol
+
+    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")
+
+    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 = false
+        
+    let print_var_info = false
+
+    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:SYSTEM)
+
+(* Printer functions for ELF *)
+module ELF_System =
+  (struct
+    
+    let raw_symbol oc s =
+      fprintf oc "%s" s
+  
+    let symbol = symbol
+
+    let label = 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 "")
+            
+    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 = true
+      
+    let print_var_info = true
+      
+    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:SYSTEM)
+
+(* Printer functions for MacOS *)
+module MacOS_System =
+  (struct
+    
+    let raw_symbol oc s =
+     fprintf oc "_%s" s
+
+    let symbol oc symb =
+      fprintf oc "_%s" (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")
+    
+    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_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_fun_info = false
+ 
+    let print_var_info = false
+    
+    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_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:SYSTEM)
+
+
+module Target(System: SYSTEM):TARGET =
+  (struct
+    open System
+
+(*  Basic printing functions *)
+
+    let symbol_offset oc (symb, ofs) =
+      symbol oc symb;
+      if ofs <> 0l then fprintf oc " + %ld" ofs
+
+
+    let addressing oc (Addrmode(base, shift, cst)) =
+      begin match cst with
+      | Coq_inl n ->
+          let n = camlint_of_coqint n in
+          fprintf oc "%ld" 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
+      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
+      end
+
+    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)
+
+(* SP adjustment to allocate or free a stack frame *)
+
+    let int32_align n a =
+      if n >= 0l
+      then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a))
+      else Int32.logand n (Int32.of_int (-a))
+
+    let sp_adjustment sz =
+      let sz = camlint_of_coqint sz in
+      (* Preserve proper alignment of the stack *)
+      let sz = int32_align sz stack_alignment in
+      (* The top 4 bytes have already been allocated by the "call" instruction. *)
+      let sz = Int32.sub sz 4l in
+      sz
+
+(* 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)
+
+(* Emit a align directive *)
+
+    let need_masks = ref false
+
+(* Emit .file / .loc debugging directives *)
+
+    let print_file_line oc file line =
+      PrintAnnot.print_file_line oc comment file line
+
+    let print_location oc loc =
+      if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
+
+
+(* 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. *)
+
+(* Handling of annotations *)
+
+    let print_annot_stmt oc txt targs args =
+      if Str.string_match re_file_line txt 0 then begin
+        print_file_line oc (Str.matched_group 1 txt)
+          (int_of_string (Str.matched_group 2 txt))
+      end else begin
+        fprintf oc "%s annotation: " comment;
+        PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args
+      end
+
+    let print_annot_val oc txt args res =
+      fprintf oc "%s annotation: " comment;
+      PrintAnnot.print_annot_val preg oc txt args;
+      match args, res with
+      | [IR src], [IR dst] ->
+          if dst <> src then fprintf oc "	movl	%a, %a\n" ireg src ireg dst
+      | [FR src], [FR dst] ->
+          if dst <> src then fprintf oc "	movapd	%a, %a\n" freg src freg dst
+      | _, _ -> assert false
+
+(* Handling of memcpy *)
+
+(* Unaligned memory accesses are quite fast on IA32, so use large
+   memory accesses regardless of alignment. *)
+
+    let print_builtin_memcpy_small oc sz al src dst =
+      assert (src = EDX && dst = EAX);
+      let rec copy ofs sz =
+        if sz >= 8 && !Clflags.option_ffpu then begin
+          fprintf oc "	movq	%d(%a), %a\n" ofs ireg src freg XMM7;
+          fprintf oc "	movq	%a, %d(%a)\n" freg XMM7 ofs ireg dst;
+          copy (ofs + 8) (sz - 8)
+        end else if sz >= 4 then begin
+          fprintf oc "	movl	%d(%a), %a\n" ofs ireg src ireg ECX;
+          fprintf oc "	movl	%a, %d(%a)\n" ireg ECX ofs ireg dst;
+          copy (ofs + 4) (sz - 4)
+        end else if sz >= 2 then begin
+          fprintf oc "	movw	%d(%a), %a\n" ofs ireg src ireg16 ECX;
+          fprintf oc "	movw	%a, %d(%a)\n" ireg16 ECX ofs ireg dst;
+          copy (ofs + 2) (sz - 2)
+        end else if sz >= 1 then begin
+          fprintf oc "	movb	%d(%a), %a\n" ofs ireg src ireg8 ECX;
+          fprintf oc "	movb	%a, %d(%a)\n" ireg8 ECX ofs ireg dst;
+          copy (ofs + 1) (sz - 1)
+        end in
+      copy 0 sz
+
+    let print_builtin_memcpy_big oc sz al src dst =
+      assert (src = ESI && dst = EDI);
+      fprintf oc "	movl	$%d, %a\n" (sz / 4) ireg ECX;
+      fprintf oc "	rep	movsl\n";
+      if sz mod 4 >= 2 then fprintf oc "	movsw\n";
+      if sz mod 2 >= 1 then fprintf oc "	movsb\n"
+
+    let print_builtin_memcpy oc sz al args =
+      let (dst, src) =
+        match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+      fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n"
+        comment sz al;
+      if sz <= 32
+      then print_builtin_memcpy_small oc sz al src dst
+      else print_builtin_memcpy_big oc sz al src dst;
+      fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment
+
+(* Handling of volatile reads and writes *)
+
+    let offset_addressing (Addrmode(base, ofs, cst)) delta =
+      Addrmode(base, ofs,
+               match cst with
+               | Coq_inl n -> Coq_inl(Integers.Int.add n delta)
+               | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta))
+
+    let print_builtin_vload_common oc chunk addr res =
+      match chunk, res with
+      | Mint8unsigned, [IR res] ->
+          fprintf oc "	movzbl	%a, %a\n" addressing addr ireg res
+      | Mint8signed, [IR res] ->
+          fprintf oc "	movsbl	%a, %a\n" addressing addr ireg res
+      | Mint16unsigned, [IR res] ->
+          fprintf oc "	movzwl	%a, %a\n" addressing addr ireg res
+      | Mint16signed, [IR res] ->
+          fprintf oc "	movswl	%a, %a\n" addressing addr ireg res
+      | Mint32, [IR res] ->
+          fprintf oc "	movl	%a, %a\n" addressing addr ireg res
+      | Mint64, [IR res1; IR res2] ->
+          let addr' = offset_addressing addr (coqint_of_camlint 4l) in
+          if not (Asmgen.addressing_mentions addr res2) then begin
+            fprintf oc "	movl	%a, %a\n" addressing addr ireg res2;
+            fprintf oc "	movl	%a, %a\n" addressing addr' ireg res1
+          end else begin
+            fprintf oc "	movl	%a, %a\n" addressing addr' ireg res1;
+            fprintf oc "	movl	%a, %a\n" addressing addr ireg res2
+          end
+      | Mfloat32, [FR res] ->
+          fprintf oc "	movss	%a, %a\n" addressing addr freg res
+      | Mfloat64, [FR res] ->
+          fprintf oc "	movsd	%a, %a\n" addressing addr freg res
+      | _ ->
+          assert false
+
+    let print_builtin_vload oc chunk args res =
+      fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+      begin match args with
+      | [IR addr] ->
+          print_builtin_vload_common oc chunk
+            (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) res
+      | _ ->
+          assert false
+      end;
+      fprintf oc "%s end builtin __builtin_volatile_read\n" comment
+
+    let print_builtin_vload_global oc chunk id ofs args res =
+      fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+      print_builtin_vload_common oc chunk
+        (Addrmode(None, None, Coq_inr(id,ofs))) res;
+      fprintf oc "%s end builtin __builtin_volatile_read\n" comment
+
+    let print_builtin_vstore_common oc chunk addr src tmp =
+      match chunk, src with
+      | (Mint8signed | Mint8unsigned), [IR src] ->
+          if Asmgen.low_ireg src then
+            fprintf oc "	movb	%a, %a\n" ireg8 src addressing addr
+          else begin
+            fprintf oc "	movl	%a, %a\n" ireg src ireg tmp;
+            fprintf oc "	movb	%a, %a\n" ireg8 tmp addressing addr
+          end
+      | (Mint16signed | Mint16unsigned), [IR src] ->
+          fprintf oc "	movw	%a, %a\n" ireg16 src addressing addr
+      | Mint32, [IR src] ->
+          fprintf oc "	movl	%a, %a\n" ireg src addressing addr
+      | Mint64, [IR src1; IR src2] ->
+          let addr' = offset_addressing addr (coqint_of_camlint 4l) in
+          fprintf oc "	movl	%a, %a\n" ireg src2 addressing addr;
+          fprintf oc "	movl	%a, %a\n" ireg src1 addressing addr'
+      | Mfloat32, [FR src] ->
+          fprintf oc "	movss	%a, %a\n" freg src addressing addr
+      | Mfloat64, [FR src] ->
+          fprintf oc "	movsd	%a, %a\n" freg src addressing addr
+      | _ ->
+          assert false
+
+    let print_builtin_vstore oc chunk args =
+      fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+      begin match args with
+      | IR addr :: src ->
+          print_builtin_vstore_common oc chunk
+            (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src
+            (if addr = EAX then ECX else EAX)
+      | _ ->
+          assert false
+      end;
+      fprintf oc "%s end builtin __builtin_volatile_write\n" comment
+
+    let print_builtin_vstore_global oc chunk id ofs args =
+      fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+      print_builtin_vstore_common oc chunk
+        (Addrmode(None, None, Coq_inr(id,ofs))) args EAX;
+      fprintf oc "%s end builtin __builtin_volatile_write\n" comment
+
+(* Handling of varargs *)
+
+    let print_builtin_va_start oc r =
+      if not (!current_function_sig).sig_cc.cc_vararg then
+        invalid_arg "Fatal error: va_start used in non-vararg function";
+      let ofs =
+        Int32.(add (add !current_function_stacksize 4l)
+                 (mul 4l (Z.to_int32 (Conventions1.size_arguments
+                                        !current_function_sig)))) in
+      fprintf oc "	movl	%%esp, 0(%a)\n" ireg r;
+      fprintf oc "	addl	$%ld, 0(%a)\n" ofs ireg r
+
+(* Handling of compiler-inlined builtins *)
+
+    let print_builtin_inline oc name args res =
+      fprintf oc "%s begin builtin %s\n" comment name;
+      begin match name, args, res with
+        (* Integer arithmetic *)
+      | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] ->
+          if a1 <> res then
+            fprintf oc "	movl	%a, %a\n" ireg a1 ireg res;
+          fprintf oc "	bswap	%a\n" ireg res
+      | "__builtin_bswap16", [IR a1], [IR res] ->
+          if a1 <> res then
+            fprintf oc "	movl	%a, %a\n" ireg a1 ireg res;
+          fprintf oc "	rolw	$8, %a\n" ireg16 res
+      | "__builtin_clz", [IR a1], [IR res] ->
+          fprintf oc "	bsrl	%a, %a\n" ireg a1 ireg res;
+          fprintf oc "	xorl	$31, %a\n" ireg res
+      | "__builtin_ctz", [IR a1], [IR res] ->
+          fprintf oc "	bsfl	%a, %a\n" ireg a1 ireg res
+            (* Float arithmetic *)
+      | "__builtin_fabs", [FR a1], [FR res] ->
+          need_masks := true;
+          if a1 <> res then
+            fprintf oc "	movapd	%a, %a\n" freg a1 freg res;
+          fprintf oc "	andpd	%a, %a\n" raw_symbol "__absd_mask" freg res
+      | "__builtin_fsqrt", [FR a1], [FR res] ->
+          fprintf oc "	sqrtsd	%a, %a\n" freg a1 freg res
+      | "__builtin_fmax", [FR a1; FR a2], [FR res] ->
+          if res = a1 then
+            fprintf oc "	maxsd	%a, %a\n" freg a2 freg res
+          else if res = a2 then
+            fprintf oc "	maxsd	%a, %a\n" freg a1 freg res
+          else begin
+            fprintf oc "	movapd	%a, %a\n" freg a1 freg res;
+            fprintf oc "	maxsd	%a, %a\n" freg a2 freg res
+          end
+      | "__builtin_fmin", [FR a1; FR a2], [FR res] ->
+          if res = a1 then
+            fprintf oc "	minsd	%a, %a\n" freg a2 freg res
+          else if res = a2 then
+            fprintf oc "	minsd	%a, %a\n" freg a1 freg res
+          else begin
+            fprintf oc "	movapd	%a, %a\n" freg a1 freg res;
+            fprintf oc "	minsd	%a, %a\n" freg a2 freg res
+          end
+      | ("__builtin_fmadd"|"__builtin_fmsub"|"__builtin_fnmadd"|"__builtin_fnmsub"),
+            [FR a1; FR a2; FR a3], [FR res] ->
+              let opcode =
+                match name with
+                | "__builtin_fmadd" -> "vfmadd"
+                | "__builtin_fmsub" -> "vfmsub"
+                | "__builtin_fnmadd" -> "vfnmadd"
+                | "__builtin_fnmsub" -> "vfnmsub"
+                | _ -> assert false in
+              if res = a1 then
+                fprintf oc "	%s132sd	%a, %a, %a\n" opcode freg a2 freg a3 freg res
+              else if res = a2 then
+                fprintf oc "	%s213sd	%a, %a, %a\n" opcode freg a3 freg a1 freg res
+              else if res = a3 then
+                fprintf oc "	%s231sd	%a, %a, %a\n" opcode freg a1 freg a2 freg res
+              else begin
+                fprintf oc "	movapd	%a, %a\n" freg a3 freg res;
+                fprintf oc "	%s231sd	%a, %a, %a\n" opcode freg a1 freg a2 freg res
+              end
+                  (* 64-bit integer arithmetic *)
+      | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
+          assert (ah = EDX && al = EAX && rh = EDX && rl = EAX);
+          fprintf oc "	negl	%a\n" ireg EAX;
+          fprintf oc "	adcl	$0, %a\n" ireg EDX;
+          fprintf oc "	negl	%a\n" ireg EDX
+      | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+          assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX);
+          fprintf oc "	addl	%a, %a\n" ireg EBX ireg EAX;
+          fprintf oc "	adcl	%a, %a\n" ireg ECX ireg EDX
+      | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+          assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX);
+          fprintf oc "	subl	%a, %a\n" ireg EBX ireg EAX;
+          fprintf oc "	sbbl	%a, %a\n" ireg ECX ireg EDX
+      | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
+          assert (a = EAX && b = EDX && rh = EDX && rl = EAX);
+          fprintf oc "	mull    %a\n" ireg EDX
+            (* Memory accesses *)
+      | "__builtin_read16_reversed", [IR a1], [IR res] ->
+          fprintf oc "	movzwl	0(%a), %a\n" ireg a1 ireg res;
+          fprintf oc "	rolw	$8, %a\n" ireg16 res
+      | "__builtin_read32_reversed", [IR a1], [IR res] ->
+          fprintf oc "	movl	0(%a), %a\n" ireg a1 ireg res;
+          fprintf oc "	bswap	%a\n" ireg res
+      | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
+          let tmp = if a1 = ECX then EDX else ECX in
+          if a2 <> tmp then
+            fprintf oc "	movl	%a, %a\n" ireg a2 ireg tmp;
+          fprintf oc "	xchg	%a, %a\n" ireg8 tmp high_ireg8 tmp;
+          fprintf oc "	movw	%a, 0(%a)\n" ireg16 tmp ireg a1
+      | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
+          let tmp = if a1 = ECX then EDX else ECX in
+          if a2 <> tmp then
+            fprintf oc "	movl	%a, %a\n" ireg a2 ireg tmp;
+          fprintf oc "	bswap	%a\n" ireg tmp;
+          fprintf oc "	movl	%a, 0(%a)\n" ireg tmp ireg a1
+            (* Synchronization *)
+      | "__builtin_membar", [], _ ->
+          ()
+            (* Vararg stuff *)
+      | "__builtin_va_start", [IR a], _ ->
+          print_builtin_va_start oc a
+            (* Catch-all *)  
+      | _ ->
+          invalid_arg ("unrecognized builtin " ^ name)
+      end;
+      fprintf oc "%s end builtin %s\n" comment name
+
+(* Printing of instructions *)
+
+(* Reminder on AT&T syntax: op source, dest *)
+
+    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
+      | 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, %a %s %.18g\n" label lbl 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, %a %s %.18g\n" label lbl 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
+      | 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
+      | Pmovzb_rm(rd, a) ->
+          fprintf oc "	movzbl	%a, %a\n" addressing a ireg rd
+      | Pmovsb_rr(rd, r1) ->
+          fprintf oc "	movsbl	%a, %a\n" ireg8 r1 ireg rd
+      | Pmovsb_rm(rd, a) ->
+          fprintf oc "	movsbl	%a, %a\n" addressing a ireg rd
+      | Pmovzw_rr(rd, r1) ->
+          fprintf oc "	movzwl	%a, %a\n" ireg16 r1 ireg rd
+      | Pmovzw_rm(rd, a) ->
+          fprintf oc "	movzwl	%a, %a\n" addressing a ireg rd
+      | Pmovsw_rr(rd, r1) ->
+          fprintf oc "	movswl	%a, %a\n" ireg16 r1 ireg rd
+      | Pmovsw_rm(rd, a) ->
+          fprintf oc "	movswl	%a, %a\n" addressing a ireg rd
+      | 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
+      | Pcvtsi2sd_fr(rd, r1) ->
+          fprintf oc "	cvtsi2sd %a, %a\n" ireg r1 freg rd
+      | Pcvttss2si_rf(rd, r1) ->
+          fprintf oc "	cvttss2si %a, %a\n" freg r1 ireg rd
+      | Pcvtsi2ss_fr(rd, r1) ->
+          fprintf oc "	cvtsi2ss %a, %a\n" ireg 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
+      | Pdiv(r1) ->
+          fprintf oc "	xorl	%%edx, %%edx\n";
+          fprintf oc "	divl	%a\n" ireg r1
+      | Pidiv(r1) ->
+          fprintf oc "	cltd\n";
+          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
+      | 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
+      | 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
+            (** 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, %a\n" raw_symbol "__negd_mask" freg rd
+      | Pabsd (rd) ->
+          need_masks := true;
+          fprintf oc "	andpd	%a, %a\n" raw_symbol "__absd_mask" 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, %a\n" raw_symbol "__negs_mask" freg rd
+      | Pabss (rd) ->
+          need_masks := true;
+          fprintf oc "	andpd	%a, %a\n" raw_symbol "__abss_mask" 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
+          fprintf oc "	jmp	*%a(, %a, 4)\n" label l ireg r;
+          jumptables := (l, tbl) :: !jumptables
+      | Pcall_s(f, sg) ->
+          fprintf oc "	call	%a\n" symbol f
+      | Pcall_r(r, sg) ->
+          fprintf oc "	call	*%a\n" ireg r
+      | Pret ->
+          fprintf oc "	ret\n"
+            (** Pseudo-instructions *)
+      | Plabel(l) ->
+          fprintf oc "%a:\n" label (transl_label l)
+      | Pallocframe(sz, ofs_ra, ofs_link) ->
+          let sz = sp_adjustment sz in
+          let ofs_link = camlint_of_coqint ofs_link in
+          fprintf oc "	subl	$%ld, %%esp\n" sz;
+          cfi_adjust oc sz;
+          fprintf oc "	leal	%ld(%%esp), %%edx\n" (Int32.add sz 4l);
+          fprintf oc "	movl	%%edx, %ld(%%esp)\n" ofs_link;
+          current_function_stacksize := sz
+      | Pfreeframe(sz, ofs_ra, ofs_link) ->
+          let sz = sp_adjustment sz in
+          fprintf oc "	addl	$%ld, %%esp\n" sz
+      | Pbuiltin(ef, args, res) ->
+          begin match ef with
+          | EF_builtin(name, sg) ->
+              print_builtin_inline oc (extern_atom name) args res
+          | EF_vload chunk ->
+              print_builtin_vload oc chunk args res
+          | EF_vstore chunk ->
+              print_builtin_vstore oc chunk args
+          | EF_vload_global(chunk, id, ofs) ->
+              print_builtin_vload_global oc chunk id ofs args res
+          | EF_vstore_global(chunk, id, ofs) ->
+              print_builtin_vstore_global oc chunk id ofs args
+          | EF_memcpy(sz, al) ->
+              print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz))
+                (Int32.to_int (camlint_of_coqint al)) args
+          | EF_annot_val(txt, targ) ->
+              print_annot_val oc (extern_atom txt) args res
+          | EF_inline_asm txt ->
+              fprintf oc "%s begin inline assembly\n" comment;
+              fprintf oc "	%s\n" (extern_atom txt);
+              fprintf oc "%s end inline assembly\n" comment
+          | _ ->
+              assert false
+          end
+      | Pannot(ef, args) ->
+          begin match ef with
+          | EF_annot(txt, targs) ->
+              print_annot_stmt oc (extern_atom txt) targs args
+          | _ ->
+              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 oc (lbl, tbl) =
+        fprintf oc "%a:" label lbl;
+        List.iter
+          (fun l -> fprintf oc "	.long	%a\n" label (transl_label l))
+          tbl in
+      if !jumptables <> [] then begin
+        section oc jmptbl;
+        print_align oc 4;
+        List.iter (print_jumptable oc) !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_coqfloat 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	%s\n" (Z.to_string n)
+      | Init_addrof(symb, ofs) ->
+          fprintf oc "	.long	%a\n" 
+            symbol_offset (symb, camlint_of_coqint 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 comment = comment
+
+    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 code =   List.iter (print_instruction oc) 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 _ = 
+      need_masks := false
+    
+    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;
+end)
+
+let sel_target () =
+ let module S = (val (match Configuration.system with
+  | "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)
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 97fa952d..d7249d17 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -701,11 +701,8 @@ module Target (System : SYSTEM):TARGET =
       | [t;l;j] -> (t, l, j)
       |    _    -> (Section_text, Section_literal, Section_jumptable)
             
-    let reset_constants () =
-      float64_literals := [];
-      float32_literals := [];
-      jumptables := []
-    
+    let reset_constants = reset_constants
+ 
     let print_var_info = true
 
     let print_comm_symb oc sz name align =