Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"

This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing
changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.

3 files changed, 288 insertions, 520 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index b423b4fc..b67c3cc5 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -212,42 +212,7 @@ Inductive instruction: Type :=
   | Pallocframe(sz: Z)(ofs_ra ofs_link: int)
   | Pfreeframe(sz: Z)(ofs_ra ofs_link: int)
   | Pbuiltin(ef: external_function)(args: list preg)(res: list preg)
-  | Pannot(ef: external_function)(args: list (annot_arg preg))
-  | Padcl_ir (n: int) (r: ireg)
-  | Padcl_rr (r1: ireg) (r2: ireg)
-  | Paddl (r1: ireg) (r2: ireg)
-  | Paddl_mi (a: addrmode) (n: int)
-  | Paddl_ri (r1: ireg) (n: int)
-  | Pbsfl (r1: ireg) (r2: ireg)
-  | Pbslr (r1: ireg) (r2: ireg)
-  | Pbswap (r: ireg)
-  | Pcfi_adjust (n: int)
-  | Pfmadd132 (r1: freg) (r2: freg) (r3: freg)
-  | Pfmadd213 (r1: freg) (r2: freg) (r3: freg)
-  | Pfmadd231 (r1: freg) (r2: freg) (r3: freg)
-  | Pfmsub132 (r1: freg) (r2: freg) (r3: freg)
-  | Pfmsub213 (r1: freg) (r2: freg) (r3: freg)
-  | Pfmsub231 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmadd132 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmadd213 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmadd231 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmsub132 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmsub213 (r1: freg) (r2: freg) (r3: freg)
-  | Pfnmsub231 (r1: freg) (r2: freg) (r3: freg)
-  | Pmaxsd (r1: freg) (r2: freg)
-  | Pminsd (r1: freg) (r2: freg)
-  | Pmovb_rm (rs: ireg) (a: addrmode)
-  | Pmovq_rm (rs: freg) (a: addrmode)
-  | Pmovq_mr  (a: addrmode) (rs: freg)
-  | Pmovsb
-  | Pmovsw
-  | Pmovw_rm (rs: ireg) (ad: addrmode)
-  | Prep_movsl
-  | Prolw_8 (r: ireg)
-  | Psbbl (r1: ireg) (r2: ireg)
-  | Psqrtsd (r1: freg) (r2: freg)
-  | Psubl_ri (r1: ireg) (n: int)
-  | Pxchg (r1: ireg) (r2: ireg).
+  | Pannot(ef: external_function)(args: list (annot_arg preg)).
 
 Definition code := list instruction.
 Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
@@ -783,44 +748,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pbuiltin ef args res =>
       Stuck                             (**r treated specially below *)
   | Pannot ef args =>
-    Stuck                             (**r treated specially below *)
-  (** The following instructions and directives are not generated directly by Asmgen,
-      so we do not model them. *)
-  | Padcl_ir _ _
-  | Padcl_rr _ _
-  | Paddl _ _
-  | Paddl_mi _ _
-  | Paddl_ri _ _
-  | Pbswap _
-  | Pbsfl _ _
-  | Pbslr _ _
-  | Pcfi_adjust _
-  | Pfmadd132 _ _ _
-  | Pfmadd213 _ _ _
-  | Pfmadd231 _ _ _
-  | Pfmsub132 _ _ _
-  | Pfmsub213 _ _ _
-  | Pfmsub231 _ _ _
-  | Pfnmadd132 _ _ _
-  | Pfnmadd213 _ _ _
-  | Pfnmadd231 _ _ _
-  | Pfnmsub132 _ _ _
-  | Pfnmsub213 _ _ _
-  | Pfnmsub231 _ _ _
-  | Pmaxsd _ _
-  | Pminsd _ _
-  | Pmovb_rm _ _
-  | Pmovq_rm _ _
-  | Pmovq_mr _ _   
-  | Pmovsb
-  | Pmovsw
-  | Pmovw_rm _ _ 
-  | Prep_movsl
-  | Prolw_8 _
-  | Psbbl _ _
-  | Psqrtsd _ _
-  | Psubl_ri _ _
-  | Pxchg _ _ => Stuck 
+      Stuck                             (**r treated specially below *)
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index e07672a6..9a458c37 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -14,378 +14,5 @@
    of the IA32 assembly code.  Currently not done, this expansion
    is performed on the fly in PrintAsm. *)
 
-open Asm
-open Asmexpandaux
-open Asmgen
-open AST
-open Camlcoq
-open Datatypes
-open Integers
-       
-(* Useful constants and helper functions *)
-
-let _0 = Int.zero
-let _1 = Int.one
-let _2 = coqint_of_camlint 2l
-let _4 = coqint_of_camlint 4l
-let _8 = coqint_of_camlint 8l
-
-let stack_alignment () =
-  if Configuration.system = "macoxs" then 16
-  else 8
-	 
-(* 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
-			   
-			   
-(* 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 expand_annot_val txt targ args res =
-  emit (Pannot (EF_annot(txt,[targ]), List.map (fun r -> AA_base r) args));
-  match args, res with
-  | [IR src], [IR dst] ->
-     if dst <> src then emit (Pmov_rr (dst,src))
-  | [FR src], [FR dst] ->
-     if dst <> src then emit (Pmovsd_ff (dst,src))
-  | _, _ -> assert false
-
-			   
-(* Handling of memcpy *)
-
-(* Unaligned memory accesses are quite fast on IA32, so use large
-   memory accesses regardless of alignment. *)
-
-let expand_builtin_memcpy_small sz al src dst =
-  assert (src = EDX && dst = EAX);
-  let rec copy ofs sz =
-    if sz >= 8 && !Clflags.option_ffpu then begin
-	emit (Pmovq_rm (XMM7,Addrmode (Some src, None, Coq_inl ofs)));
-	emit (Pmovq_mr (Addrmode (Some src, None, Coq_inl ofs),XMM7));
-        copy (Int.add ofs _8) (sz - 8)
-      end else if sz >= 4 then begin
-	emit (Pmov_rm (ECX,Addrmode (Some src, None, Coq_inl ofs)));
-	emit (Pmov_mr (Addrmode (Some src, None, Coq_inl ofs),ECX));
-        copy (Int.add ofs _4) (sz - 4)
-      end else if sz >= 2 then begin
-	emit (Pmovw_rm (ECX,Addrmode (Some src, None, Coq_inl ofs)));
-	emit (Pmovw_mr (Addrmode (Some src, None, Coq_inl ofs),ECX));
-        copy (Int.add ofs _2) (sz - 2)
-      end else if sz >= 1 then begin
-	emit (Pmovb_rm (ECX,Addrmode (Some src, None, Coq_inl ofs)));
-	emit (Pmovb_mr (Addrmode (Some src, None, Coq_inl ofs),ECX));
-        copy (Int.add ofs _1) (sz - 1)
-      end in
-  copy _0 sz
-
-let expand_builtin_memcpy_big sz al src dst =
-  assert (src = ESI && dst = EDI);
-  emit (Pmov_ri (ECX,coqint_of_camlint (Int32.of_int (sz / 4))));
-  emit Prep_movsl;
-  if sz mod 4 >= 2 then emit Pmovsw;
-  if sz mod 2 >= 1 then emit Pmovsb
-
-let expand_builtin_memcpy sz al args =
-  let (dst, src) =
-    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
-  if sz <= 32
-  then expand_builtin_memcpy_small sz al src dst
-  else expand_builtin_memcpy_big sz al src dst
- 	   
-(* 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 expand_builtin_vload_common chunk addr res =
-  match chunk, res with
-  | Mint8unsigned, [IR res] ->
-     emit (Pmovzb_rm (res,addr))
-  | Mint8signed, [IR res] ->
-     emit (Pmovsb_rm (res,addr))
-  | Mint16unsigned, [IR res] ->
-     emit (Pmovzw_rm (res,addr))
-  | Mint16signed, [IR res] ->
-     emit (Pmovsw_rm (res,addr))
-  | Mint32, [IR res] ->
-     emit (Pmov_rm (res,addr))
-  | Mint64, [IR res1; IR res2] ->
-     let addr' = offset_addressing addr (coqint_of_camlint 4l) in
-     if not (Asmgen.addressing_mentions addr res2) then begin
-	 emit (Pmov_rm (res2,addr));
-	 emit (Pmov_rm (res1,addr'))
-       end else begin
-	 emit (Pmov_rm (res1,addr'));
-	 emit (Pmov_rm (res2,addr))
-       end
-  | Mfloat32, [FR res] ->
-     emit (Pmovss_fm (res,addr))
-  | Mfloat64, [FR res] ->
-     emit (Pmovsd_fm (res,addr))
-  | _ ->
-     assert false
-
-let expand_builtin_vload chunk args res =
-  match args with
-  | [IR addr] ->
-     expand_builtin_vload_common chunk (Addrmode (Some addr,None, Coq_inl _0)) res
-  | _ ->
-     assert false
-
-let expand_builtin_vload_global chunk id ofs args res =
-  expand_builtin_vload_common chunk (Addrmode(None, None, Coq_inr(id,ofs))) res
-			      
-let expand_builtin_vstore_common chunk addr src tmp =
-  match chunk, src with
-  | (Mint8signed | Mint8unsigned), [IR src] ->
-     if Asmgen.low_ireg src then
-       emit (Pmovb_mr (addr,src))
-     else begin
-	 emit (Pmov_rr (tmp,src));
-	 emit (Pmovb_mr (addr,tmp))
-       end
-  | (Mint16signed | Mint16unsigned), [IR src] ->
-     emit (Pmovw_mr (addr,src))
-  | Mint32, [IR src] ->
-     emit (Pmov_mr (addr,src))
-  | Mint64, [IR src1; IR src2] ->
-     let addr' = offset_addressing addr (coqint_of_camlint 4l) in
-     emit (Pmov_mr (addr,src2));
-     emit (Pmov_mr (addr',src1))
-  | Mfloat32, [FR src] ->
-     emit (Pmovss_mf (addr,src))
-  | Mfloat64, [FR src] ->
-     emit (Pmovsd_mf (addr,src))
-  | _ ->
-     assert false
-
-let expand_builtin_vstore chunk args =
-  match args with
-  | IR addr :: src ->
-     expand_builtin_vstore_common chunk
-       (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src
-       (if addr = EAX then ECX else EAX)
-  | _ -> assert false
-
-		
-let expand_builtin_vstore_global chunk id ofs args =
-  expand_builtin_vstore_common chunk
-    (Addrmode(None, None, Coq_inr(id,ofs))) args EAX
-
-		 
-(* Handling of varargs *)
-		 
-let expand_builtin_va_start r =
-  if not !current_function.fn_sig.sig_cc.cc_vararg then
-    invalid_arg "Fatal error: va_start used in non-vararg function";
-  let ofs = coqint_of_camlint
-    Int32.(add (add !PrintAsmaux.current_function_stacksize 4l)
-               (mul 4l (Z.to_int32 (Conventions1.size_arguments
-                                      !current_function.fn_sig)))) in
-  emit (Pmov_mr (Addrmode (Some r, None, Coq_inl _0),ESP));
-  emit (Paddl_mi (Addrmode (Some r,None,Coq_inl _0),ofs))
-	   
-(* Handling of compiler-inlined builtins *)
-
-let expand_builtin_inline name args res =
-  match name, args, res with
-  (* Integer arithmetic *)
-  | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] ->
-     if a1 <> res then
-       emit (Pmov_rr (res,a1));
-     emit (Pbswap res)
-  | "__builtin_bswap16", [IR a1], [IR res] ->
-     if a1 <> res then
-       emit (Pmov_rr (res,a1));
-     emit (Prolw_8 res)
-  | "__builtin_clz", [IR a1], [IR res] ->
-     emit (Pbslr (a1,res));
-     emit (Pxor_ri(res,coqint_of_camlint 31l))
-  | "__builtin_ctz", [IR a1], [IR res] ->
-     emit (Pbsfl (a1,res))
-  (* Float arithmetic *)
-  | "__builtin_fabs", [FR a1], [FR res] ->
-     if a1 <> res then
-       emit (Pmovsd_ff (a1,res));
-     emit (Pabsd res) (* This ensures that need_masks is set to true *)
-  | "__builtin_fsqrt", [FR a1], [FR res] ->
-     emit (Psqrtsd (a1,res))
-  | "__builtin_fmax", [FR a1; FR a2], [FR res] ->
-     if res = a1 then
-       emit (Pmaxsd (a2,res))
-     else if res = a2 then
-       emit (Pmaxsd (a1,res))
-     else begin
-	 emit (Pmovsd_ff (a1,res));
-	 emit (Pmaxsd (a2,res))
-       end
-  | "__builtin_fmin", [FR a1; FR a2], [FR res] ->
-     if res = a1 then
-       emit (Pminsd (a2,res))
-     else if res = a2 then
-       emit (Pminsd (a1,res))
-     else begin
-	 emit (Pmovsd_ff (a1,res));
-	 emit (Pminsd (a2,res))
-       end
-  | "__builtin_fmadd",  [FR a1; FR a2; FR a3], [FR res] ->
-     if res = a1 then
-       emit (Pfmadd132 (a2,a3,res))
-     else if res = a2 then
-       emit (Pfmadd213 (a2,a3,res))
-     else if res = a3 then
-       emit (Pfmadd231 (a2,a3,res))
-     else begin
-	 emit (Pmovsd_ff (a2,res));
-	 emit (Pfmadd231 (a1,a2,res))
-       end
-  |"__builtin_fmsub",  [FR a1; FR a2; FR a3], [FR res] ->
-     if res = a1 then
-       emit (Pfmsub132 (a2,a3,res))
-     else if res = a2 then
-       emit (Pfmsub213 (a2,a3,res))
-     else if res = a3 then
-       emit (Pfmsub231 (a2,a3,res))
-     else begin
-	 emit (Pmovsd_ff (a2,res));
-	 emit (Pfmsub231 (a1,a2,res))
-       end
-  | "__builtin_fnmadd",  [FR a1; FR a2; FR a3], [FR res] ->
-     if res = a1 then
-       emit (Pfnmadd132 (a2,a3,res))
-     else if res = a2 then
-       emit (Pfnmadd213 (a2,a3,res))
-     else if res = a3 then
-       emit (Pfnmadd231 (a2,a3,res))
-     else begin
-	 emit (Pmovsd_ff (a2,res));
-	 emit (Pfnmadd231 (a1,a2,res))
-       end
-  |"__builtin_fnmsub",  [FR a1; FR a2; FR a3], [FR res] ->
-     if res = a1 then
-       emit (Pfnmsub132 (a2,a3,res))
-     else if res = a2 then
-       emit (Pfnmsub213 (a2,a3,res))
-     else if res = a3 then
-       emit (Pfnmsub231 (a2,a3,res))
-     else begin
-	 emit (Pmovsd_ff (a2,res));
-	 emit (Pfnmsub231 (a1,a2,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);
-     emit (Pneg EAX);
-     emit (Padcl_ir (_0,EDX));
-     emit (Pneg 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);
-     emit (Paddl (EBX,EAX));
-     emit (Padcl_rr (ECX,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);
-     emit (Psub_rr (EBX,EAX));
-     emit (Psbbl (ECX,EDX))
-  | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
-     assert (a = EAX && b = EDX && rh = EDX && rl = EAX);
-     emit (Pmul_r EDX)
-  (* Memory accesses *)
-  | "__builtin_read16_reversed", [IR a1], [IR res] ->
-     let addr = Addrmode(Some a1,None,Coq_inl _0) in
-     emit (Pmovzw_rm (res,addr));
-     emit (Prolw_8 res)
-  | "__builtin_read32_reversed", [IR a1], [IR res] ->
-     let addr = Addrmode(Some a1,None,Coq_inl _0) in
-     emit (Pmov_rm (res,addr));
-     emit (Pbswap res)
-  | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
-     let tmp = if a1 = ECX then EDX else ECX in
-     let addr = Addrmode(Some a1,None,Coq_inl _0) in
-     if a2 <> tmp then
-       emit (Pmov_rr (a2,tmp));
-     emit (Pxchg (tmp,tmp));
-     emit (Pmovw_mr (addr,tmp))
-  (* Vararg stuff *)
-  | "__builtin_va_start", [IR a], _ ->
-     expand_builtin_va_start a
-  (* Synchronization *)
-  | "__builtin_membar", [], _ ->
-     ()
-  (* Catch-all *)
-  | _ ->
-     invalid_arg ("unrecognized builtin " ^ name)
-
-
-       
-let expand_instruction instr =
-  match instr with
-  | Pallocframe (sz, ofs_ra, ofs_link) ->
-     let sz = sp_adjustment sz in
-     let addr = Addrmode(Some ESP,None,Coq_inl (coqint_of_camlint (Int32.add sz 4l))) in
-     let addr' = Addrmode (Some ESP, None, Coq_inl ofs_link) in
-     let sz' = coqint_of_camlint sz in
-     emit (Psubl_ri (ESP,sz'));
-     emit (Pcfi_adjust sz');
-     emit (Plea (EDX,addr));
-     emit (Pmov_mr (addr',EDX));
-     PrintAsmaux.current_function_stacksize := sz
-  | Pfreeframe(sz, ofs_ra, ofs_link) ->
-     let sz = sp_adjustment sz in
-     emit (Paddl_ri (ESP,coqint_of_camlint sz))
-  | Pbuiltin (ef,args, res) ->
-     begin
-       match ef with
-       | EF_builtin(name, sg) ->
-	  expand_builtin_inline (extern_atom name) args res
-       | EF_vload chunk ->
-          expand_builtin_vload chunk args res
-       | EF_vstore chunk ->
-          expand_builtin_vstore chunk args
-       | EF_vload_global(chunk, id, ofs) ->
-          expand_builtin_vload_global chunk id ofs args res
-       | EF_vstore_global(chunk, id, ofs) ->
-          expand_builtin_vstore_global chunk id ofs args
-       | EF_memcpy(sz, al) ->
-          expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz))
-	    (Int32.to_int (camlint_of_coqint al)) args
-       | EF_annot_val(txt, targ) ->
-          expand_annot_val txt targ args res      
-       | EF_inline_asm(txt, sg, clob) ->
-          emit instr
-       | _ -> assert false
-     end
-  | _ -> emit instr
-       
 let expand_program p = p
 
-let expand_function fn =
-  set_current_function fn;
-  List.iter expand_instruction fn.fn_code;
-  get_current_function ()
-
-let expand_fundef = function
-  | Internal f -> Internal (expand_function f)
-  | External ef -> External ef
-
-let expand_program (p: Asm.program) : Asm.program =
-  AST.transform_program expand_fundef p
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 18aacebf..a53a8fbd 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -348,7 +348,156 @@ module Target(System: SYSTEM):TARGET =
         print_annot_stmt preg "%esp" oc txt targs args
       end
 
- (* Handling of varargs *)
+    let print_annot_val oc txt args res =
+      fprintf oc "%s annotation: " comment;
+      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
@@ -360,6 +509,117 @@ module Target(System: SYSTEM):TARGET =
       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 *)
 
@@ -581,83 +841,36 @@ module Target(System: SYSTEM):TARGET =
             fprintf oc "	ret\n"
           end
       (** Pseudo-instructions *)
-      | Padcl_ir (n,res) ->
-	 fprintf oc "  	adcl	$%ld, %a\n" (camlint_of_coqint n) ireg res;
-      | Padcl_rr (a1,res) ->
-	 fprintf oc "  	adcl	%a, %a\n" ireg a1 ireg res;
-      | Paddl (a1,res) ->
-	 fprintf oc "	addl	%a, %a\n" ireg a1 ireg res;
-      | Paddl_mi (addr,n) ->
-	 fprintf oc "	addl	$%ld, %a\n" (camlint_of_coqint n) addressing addr
-      | Paddl_ri (res,n) ->
-	  fprintf oc "	addl	$%ld, %a\n" (camlint_of_coqint n) ireg res
-      | Pbsfl (a1,res) ->
-	 fprintf oc "	bsfl	%a, %a\n" ireg a1 ireg res
-      | Pbslr (a1,res) ->
-	 fprintf oc "	bsrl	%a, %a\n" ireg a1 ireg res
-      | Pbswap res ->
-	 fprintf oc "	bswap	%a\n" ireg res
-      | Pcfi_adjust sz ->
-	 cfi_adjust oc (camlint_of_coqint sz)
-      | Pfmadd132 (a1,a2,res) ->
-	 fprintf oc "	vfmadd132sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfmadd213 (a1,a2,res) ->
-	 fprintf oc "	vfmadd213sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfmadd231 (a1,a2,res) ->
-	 fprintf oc "	vfmadd231sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfmsub132 (a1,a2,res) ->
-	 fprintf oc "	vfmsub132sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfmsub213 (a1,a2,res) ->
-	 fprintf oc "	vfmsub213sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfmsub231 (a1,a2,res) ->
-	 fprintf oc "	vfmsub231sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfnmadd132 (a1,a2,res) ->
-	 fprintf oc "	vfnmadd132sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfnmadd213 (a1,a2,res) ->
-	 fprintf oc "	vfnmadd213sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfnmadd231 (a1,a2,res) ->
-	 fprintf oc "	vfnmadd231sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfnmsub132 (a1,a2,res) ->
-	 fprintf oc "	vfnmsub132sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfnmsub213 (a1,a2,res) ->
-	 fprintf oc "	vfnmsub213sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pfnmsub231 (a1,a2,res) ->
-	 fprintf oc "	vfnmsub231sd	%a, %a, %a\n" freg a1 freg a2 freg res
-      | Pmaxsd (a1,res) ->
-	 fprintf oc "	maxsd	%a, %a\n" freg a1 freg res
-      | Pminsd (a1,res) ->
-	 fprintf oc "	minsd	%a, %a\n" freg a1 freg res
-      | Pmovb_rm (r1,a) ->
-	 fprintf oc "	movb	%a, %a\n" addressing a ireg8 r1
-      | Pmovq_rm(rd, a) ->
-          fprintf oc "	movq	%a, %a\n" addressing a freg rd
-      | Pmovq_mr(a, r1) ->
-          fprintf oc "	movq	%a, %a\n" freg r1 addressing a
-      | Pmovsb ->
-	 fprintf oc "	movsb\n";
-      | Pmovsw ->
-	 fprintf oc "	movsw\n";
-      | Pmovw_rm (r1, a) ->
-          fprintf oc "	movw	%a, %a\n" addressing a ireg16 r1
-      | Prep_movsl ->
-	 fprintf oc "	rep	movsl\n"
-      | Prolw_8 res ->
-	 fprintf oc "	rolw	$8, %a\n" ireg16 res
-      | Psbbl (a1,res) ->
-	 fprintf oc "	sbbl	%a, %a\n" ireg a1 ireg res
-      | Psqrtsd (a1,res) ->
-	 fprintf oc "	sqrtsd	%a, %a\n" freg a1 freg res
-      | Psubl_ri (res,n) ->
-	  fprintf oc "	subl	$%ld, %a\n" (camlint_of_coqint n) ireg res;
-      | Pxchg (a1,a2) ->
-	 fprintf oc "	xchg	%a, %a\n" ireg8 a1 high_ireg8 a2;
       | Plabel(l) ->
           fprintf oc "%a:\n" label (transl_label l)
-      | Pallocframe(sz, ofs_ra, ofs_link) 
+      | 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) ->
-	 assert false
+          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, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
               print_inline_asm preg oc (extern_atom txt) sg args res;