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

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

3 files changed, 283 insertions, 409 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index dd434c02..2a120dd4 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -148,7 +148,6 @@ Inductive instruction : Type :=
   | Pmul: ireg -> ireg -> ireg -> instruction      (**r integer multiplication *)
   | Pmvn: ireg -> shift_op -> instruction          (**r integer complement *)
   | Porr: ireg -> ireg -> shift_op -> instruction  (**r bitwise or *)
-  | Ppush: list ireg -> instruction (** push registers on the stack instruction *)
   | Prsb: ireg -> ireg -> shift_op -> instruction  (**r integer reverse subtraction *)
   | Psbfx: ireg -> ireg -> int -> int -> instruction (**r signed bitfield extract *)
   | Pstr: ireg -> ireg -> shift_op -> instruction (**r int32 store *)
@@ -205,24 +204,7 @@ Inductive instruction : Type :=
   | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *)
   | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list preg -> list preg -> instruction  (**r built-in function *)
-  | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement *)
-  | Padc: ireg -> ireg -> shift_op -> instruction   (**r add with carry *)
-  | Pcfi_adjust: int -> instruction                 (**r .cfi_adjust debug directive *)
-  | Pclz: preg -> preg -> instruction               (**r count leading zeros. *)
-  | Pfsqrt: freg -> freg -> instruction             (**r floating-point square root. *)
-  | Prev: preg -> preg -> instruction               (**r reverse bytes and reverse bits. *)
-  | Prev16: preg -> preg -> instruction             (**r reverse bytes and reverse bits. *)
-  | Prsc: ireg -> ireg -> shift_op -> instruction (**r reverse subtract without carry. *)
-  | Psbc: ireg -> ireg -> shift_op -> instruction   (**r add with carry *)
-  (* Add, sub, rsb versions with s suffix *)
-  | Padds: ireg -> ireg -> shift_op -> instruction  (**r integer addition with update of condition flags *)
-  | Psubs: ireg -> ireg -> shift_op -> instruction  (**r integer subtraction with update of condition flags *)
-  | Prsbs: ireg -> ireg -> shift_op -> instruction  (**r integer reverse subtraction with update of condition flags *)
-  | Pdmb: instruction                               (**r data memory barrier *)
-  | Pdsb: instruction                               (**r data synchronization barrier *)
-  | Pisb: instruction                               (**r instruction synchronization barrier *)
-  | Pbne: label -> instruction.                     (**r branch if negative macro *)
-
+  | Pannot: external_function -> list (annot_arg preg) -> instruction. (**r annotation statement *)
 
 (** The pseudo-instructions are the following:
 
@@ -741,25 +723,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       end
   | 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. *)
-  | Ppush _
-  | Padc _ _ _
-  | Pcfi_adjust _
-  | Pclz _ _
-  | Prev _ _
-  | Prev16 _ _
-  | Pfsqrt _ _
-  | Prsc _ _ _
-  | Psbc _ _ _
-  | Padds _ _ _
-  | Psubs _ _ _
-  | Prsbs _ _ _
-  | Pdmb
-  | Pdsb
-  | Pisb
-  | Pbne _ =>
-    Stuck
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 95f35f37..4baaac3d 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -11,334 +11,8 @@
 (* *********************************************************************)
 
 (* Expanding built-ins and some pseudo-instructions by rewriting
-   of the ARM assembly code.  Currently not everything done, this
-   expansion is performed on the fly in PrintAsm. *)
+   of the ARM 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 Integers
+let expand_program p = p
 
-(* Useful constants and helper functions *)
-
-let _0 = Integers.Int.zero
-let _1 = Integers.Int.one
-let _2 = coqint_of_camlint 2l
-let _4 = coqint_of_camlint 4l
-let _8 = coqint_of_camlint 8l
-let _16 = coqint_of_camlint 16l
-
-(* Emit instruction sequences that set or offset a register by a constant. *)
-(* No S suffix because they are applied to SP most of the time. *)
-
-let expand_movimm dst n =
-  match Asmgen.decompose_int n with
-  | [] -> assert false
-  | hd::tl->
-     emit (Pmov (dst,SOimm hd));
-     List.iter
-       (fun n -> emit (Porr (dst,dst, SOimm n))) tl
-
-let expand_subimm dst src n =
-  match Asmgen.decompose_int n with
-  | [] -> assert false
-  | hd::tl ->
-     emit (Psub(dst,src,SOimm hd));
-     List.iter (fun n -> emit (Psub (dst,dst,SOimm n))) tl
-
-let expand_addimm dst src n =
-  match Asmgen.decompose_int n with
-  | [] -> assert false
-  | hd::tl ->
-     emit (Padd (dst,src,SOimm hd));
-     List.iter (fun n -> emit (Padd (dst,dst,SOimm n))) tl
-
-let expand_int64_arith conflict rl fn =
-  if conflict then
-    begin
-      fn IR14;
-      emit (Pmov (rl,SOreg IR14))
-    end else
-    fn rl
-
-
-(* 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.
-*)
-
-(* 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 (dst,SOreg src))
-  | [FR src], [FR dst] ->
-     if dst <> src then emit (Pfcpyd (dst,src))
-  | _, _ -> assert false
-
-
-(* Handling of memcpy *)
-
-(* The ARM has strict alignment constraints for 2 and 4 byte accesses.
-   8-byte accesses must be 4-aligned. *)
-
-let expand_builtin_memcpy_small sz al src dst =
-  let rec copy ofs sz  =
-    if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
-	emit (Pfldd (FR7,src,ofs));
-	emit (Pfstd (FR7,dst,ofs));
-	copy (Int.add ofs _8) (sz - 8)
-      end else if sz >= 4 && al >= 4 then begin
-	emit (Pldr (IR14,src,SOimm ofs));
-	emit (Pstr (IR14,dst,SOimm ofs));
-	copy (Int.add ofs _4) (sz - 4)
-      end else if sz >= 2 && al >= 2 then begin
-	emit (Pldrh (IR14,src,SOimm ofs));
-	emit (Pstrh (IR14,dst,SOimm ofs));
-	copy (Int.add ofs _2) (sz - 2)
-      end else if sz >= 1 then begin
-	emit (Pldrb (IR14,src,SOimm ofs));
-	emit (Pstrb (IR14,dst,SOimm ofs));
-	copy (Int.add ofs _1) (sz - 1)
-      end else
-      () in
-  copy _0 sz
-
-let expand_builtin_memcpy_big sz al src dst =
-  assert (sz >= al);
-  assert (sz mod al = 0);
-  assert (src = IR2);
-  assert (dst = IR3);
-  let (load, store, chunksize) =
-    if al >= 4 then (Pldr (IR12,src,SOimm _4), Pstr (IR12,dst,SOimm _4) , 4)
-    else if al = 2 then (Pldrh (IR12,src,SOimm _2), Pstrh (IR12,dst,SOimm _2), 2)
-    else (Pldrb (IR12,src,SOimm _1), Pstrb (IR12,dst,SOimm _1), 1) in
-  expand_movimm IR14 (coqint_of_camlint (Int32.of_int (sz / chunksize)));
-  let lbl = new_label () in
-  emit (Plabel lbl);
-  emit load;
-  emit (Psubs (IR14,IR14,SOimm _1));
-  emit store;
-  emit (Pbne lbl)
-
-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 expand_builtin_vload_common chunk args res =
-  match chunk, args, res with
-  | Mint8unsigned, [IR addr], [IR res] ->
-     emit (Pldrb (res, addr,SOimm _0))
-  | Mint8signed, [IR addr], [IR res] ->
-     emit (Pldrsb (res, addr,SOimm _0))
-  | Mint16unsigned, [IR addr], [IR res] ->
-     emit (Pldrh (res, addr, SOimm _0))
-  | Mint16signed, [IR addr], [IR res] ->
-     emit (Pldrsh (res, addr, SOimm _0))
-  | Mint32, [IR addr], [IR res] ->
-     emit (Pldr (res,addr, SOimm _0))
-  | Mint64, [IR addr], [IR res1; IR res2] ->
-     if addr <> res2 then begin
-	 emit (Pldr (res2, addr, SOimm _0));
-	 emit (Pldr (res1, addr, SOimm _4))
-       end else begin
-	 emit (Pldr (res1,addr, SOimm _4));
-	 emit (Pldr (res2,addr, SOimm _0))
-       end
-  | Mfloat32, [IR addr], [FR res] ->
-     emit (Pflds (res, addr, _0))
-  | Mfloat64, [IR addr], [FR res] ->
-     emit (Pfldd (res,addr, _0))
-  | _ ->
-     assert false
-
-let expand_builtin_vload chunk args res =
-  expand_builtin_vload_common chunk args res
-
-let expand_builtin_vload_global chunk id ofs args res =
-  emit (Ploadsymbol (IR14,id,ofs));
-  expand_builtin_vload_common chunk args res
-
-let expand_builtin_vstore_common chunk args =
-  match chunk, args with
-  | (Mint8signed | Mint8unsigned), [IR  addr; IR src] ->
-     emit (Pstrb (src,addr, SOimm _0))
-  | (Mint16signed | Mint16unsigned), [IR  addr; IR src] ->
-     emit (Pstrh (src,addr, SOimm _0))
-  | Mint32, [IR  addr; IR src] ->
-     emit (Pstr (src,addr, SOimm _0))
-  | Mint64, [IR  addr; IR src1; IR src2] ->
-     emit (Pstr (src2,addr,SOimm _0));
-     emit (Pstr (src1,addr,SOimm _0))
-  | Mfloat32, [IR  addr; FR src] ->
-     emit (Pfstd (src,addr,_0))
-  | Mfloat64, [IR  addr; FR src] ->
-     emit (Pfsts (src,addr,_0));
-  | _ ->
-     assert false
-
-let expand_builtin_vstore chunk args =
-  expand_builtin_vstore_common chunk args
-
-let expand_builtin_vstore_global chunk id ofs args =
-  emit (Ploadsymbol (IR14,id,ofs));
-  expand_builtin_vstore_common chunk args
-
-(* Handling of varargs *)
-
-let align n a = (n + a - 1) land (-a)
-
-let rec next_arg_location ir ofs = function
-  | [] ->
-     Int32.of_int (ir * 4 + ofs)
-  | (Tint | Tsingle | Tany32) :: l ->
-     if ir < 4
-     then next_arg_location (ir + 1) ofs l
-     else next_arg_location ir (ofs + 4) l
-  | (Tfloat | Tlong | Tany64) :: l ->
-     if ir < 3
-     then next_arg_location (align ir 2 + 2) ofs l
-     else next_arg_location ir (align ofs 8 + 8) l
-
-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 =
-    Int32.add
-      (next_arg_location 0 0 !current_function.fn_sig.sig_args)
-      !PrintAsmaux.current_function_stacksize in
-  expand_addimm IR14 IR13 (coqint_of_camlint ofs);
-  emit (Pstr (IR14,r,SOimm _0))
-
-
-(* 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] ->
-     emit (Prev (IR res,IR a1))
-  | "__builtin_bswap16", [IR a1], [IR res] ->
-     emit (Prev16 (IR res,IR a1))
-  | "__builtin_clz", [IR a1], [IR res] ->
-     emit (Pclz (IR res, IR a1))
-  (* Float arithmetic *)
-  | "__builtin_fabs",  [FR a1], [FR res] ->
-     emit (Pfabsd (res,a1))
-  | "__builtin_fsqrt", [FR a1], [FR res] ->
-     emit (Pfsqrt (res,a1))
-  (* 64-bit integer arithmetic *)
-  | "__builtin_negl", [IR ah;IR al], [IR rh; IR rl] ->
-     emit (Prsbs (rl,al,SOimm _0));
-     if !Clflags.option_mthumb then begin
-	 emit (Pmvn (rh,SOreg ah));
-	 emit (Padc (rh,rh,SOimm _0))
-       end else
-       begin
-	 emit (Prsc (rh,ah,SOimm _0))
-       end
-  | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
-     expand_int64_arith (rl = ah || rl = bh) rl
-			(fun rl ->
-			 emit (Padds (rl,al,SOreg bl));
-			 emit (Padc (rh,ah,SOreg bh)))
-  | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
-     expand_int64_arith (rl = ah || rl = bh) rl
-		       (fun rl ->
-			emit (Psubs (rl,al,SOreg bl));
-			emit (Psbc (rh,ah,SOreg bh)))
-  | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
-     emit (Pumull (rl,rh,a,b))
-  (* Memory accesses *)
-  | "__builtin_read16_reversed", [IR a1], [IR res] ->
-     emit (Pldrh (res,a1,SOimm _0));
-     emit (Prev16 (IR res,IR res));
-  | "__builtin_read32_reversed", [IR a1], [IR res] ->
-     emit (Pldr (res,a1,SOimm _0));
-     emit (Prev (IR res,IR res));
-  | "__builtin_write16_reverse", [IR a1; IR a2], _ ->
-     emit (Prev16 (IR IR14, IR a2));
-     emit (Pstrh (IR14, a1, SOimm _0))
-  | "__builtin_write32_reverse", [IR a1; IR a2], _ ->
-     emit (Prev (IR IR14, IR a2));
-     emit (Pstr (IR14, a1, SOimm _0))
-  (* Synchronization *)
-  | "__builtin_membar",[], _ ->
-     ()
-  | "__builtin_dmb", [], _ ->
-     emit Pdmb
-  | "__builtin_dsb", [], _ ->
-     emit Pdsb
-  | "__builtin_isb", [], _ ->
-     emit Pisb
-  (* Vararg stuff *)
-  | "__builtin_va_start", [IR a], _ ->
-     expand_builtin_va_start a
-  (* Catch-all *)
-  | _ ->
-      invalid_arg ("unrecognized builtin " ^ name)
-
-let expand_instruction instr =
-  match instr with
-  | Pallocframe (sz, ofs) ->
-     emit (Pmov (IR12,SOreg IR13));
-     if (!current_function).fn_sig.sig_cc.cc_vararg then begin
-	 emit (Ppush [IR0;IR1;IR2;IR3]);
-	 emit (Pcfi_adjust _16);
-       end;
-     expand_subimm IR13 IR13 sz;
-     emit (Pcfi_adjust sz);
-     emit (Pstr (IR12,IR13,SOimm ofs))
-  | Pfreeframe (sz, ofs) ->
-     let sz =
-       if (!current_function).fn_sig.sig_cc.cc_vararg
-       then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz))
-       else sz in
-     if Asmgen.is_immed_arith sz
-     then emit (Padd (IR13,IR13,SOimm sz))
-     else emit (Pldr (IR13,IR13,SOimm 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_annot_val (txt,targ) ->
-	      expand_annot_val txt targ args res
-	   | EF_memcpy(sz, al) ->
-	      expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz))
-		(Int32.to_int (camlint_of_coqint al)) args
-	   | EF_inline_asm(txt, sg, clob) ->
-              emit instr
-	   | _ -> assert false
-     end
-  | _ ->
-     emit instr
-
-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/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 88261940..505c3265 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -304,6 +304,13 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
         
     let print_location oc loc =
       if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
+          
+(* 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.
+*)
 
 (* Handling of annotations *)
 
@@ -315,6 +322,167 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
         fprintf oc "%s annotation: " comment;
         print_annot_stmt preg "sp" oc txt targs args
       end
+          
+    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 0 else (fprintf oc "	mov	%a, %a\n" ireg dst ireg src; 1)
+      | [FR src], [FR dst] ->
+          if dst = src then 0 else (fprintf oc "	vmov.f64	%a, %a\n" freg dst freg src; 1)
+      | _, _ -> assert false
+            
+(* Handling of memcpy *)
+
+(* The ARM has strict alignment constraints for 2 and 4 byte accesses.
+   8-byte accesses must be 4-aligned. *)
+            
+    let print_builtin_memcpy_small oc sz al src dst =
+      let rec copy ofs sz ninstr =
+        if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
+          fprintf oc "	vldr	%a, [%a, #%d]\n" freg FR7 ireg src ofs;
+          fprintf oc "	vstr	%a, [%a, #%d]\n" freg FR7 ireg dst ofs;
+          copy (ofs + 8) (sz - 8) (ninstr + 2)
+        end else if sz >= 4 && al >= 4 then begin
+          fprintf oc "	ldr	%a, [%a, #%d]\n" ireg IR14 ireg src ofs;
+          fprintf oc "	str	%a, [%a, #%d]\n" ireg IR14 ireg dst ofs;
+          copy (ofs + 4) (sz - 4) (ninstr + 2)
+        end else if sz >= 2 && al >= 2 then begin
+          fprintf oc "	ldrh	%a, [%a, #%d]\n" ireg IR14 ireg src ofs;
+          fprintf oc "	strh	%a, [%a, #%d]\n" ireg IR14 ireg dst ofs;
+          copy (ofs + 2) (sz - 2) (ninstr + 2)
+        end else if sz >= 1 then begin
+          fprintf oc "	ldrb	%a, [%a, #%d]\n" ireg IR14 ireg src ofs;
+          fprintf oc "	strb	%a, [%a, #%d]\n" ireg IR14 ireg dst ofs;
+          copy (ofs + 1) (sz - 1) (ninstr + 2)
+        end else
+          ninstr in
+      copy 0 sz 0
+
+    let print_builtin_memcpy_big oc sz al src dst =
+      assert (sz >= al);
+      assert (sz mod al = 0);
+      assert (src = IR2);
+      assert (dst = IR3);
+      let (load, store, chunksize) =
+        if al >= 4 then ("ldr", "str", 4)
+        else if al = 2 then ("ldrh", "strh", 2)
+        else ("ldrb", "strb", 1) in
+      let n = movimm oc "r14" (coqint_of_camlint (Int32.of_int (sz / chunksize))) in
+      let lbl = new_label() in
+      fprintf oc ".L%d:	%s	%a, [%a], #%d\n" lbl load ireg IR12 ireg src chunksize;
+      fprintf oc "	subs	%a, %a, #1\n" ireg IR14 ireg IR14;
+      fprintf oc "	%s	%a, [%a], #%d\n" store ireg IR12 ireg dst chunksize;
+      fprintf oc "	bne	.L%d\n" lbl;
+      n + 4
+
+    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;
+      let n =
+        if sz <= 32
+        then print_builtin_memcpy_small oc sz al src dst
+        else print_builtin_memcpy_big oc sz al src dst in
+      fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment; n
+
+(* Handling of volatile reads and writes *)
+
+    let print_builtin_vload_common oc chunk args res =
+      match chunk, args, res with
+      | Mint8unsigned, [IR addr], [IR res] ->
+          fprintf oc "	ldrb	%a, [%a, #0]\n" ireg res ireg addr; 1
+      | Mint8signed, [IR addr], [IR res] ->
+          fprintf oc "	ldrsb	%a, [%a, #0]\n" ireg res ireg addr; 1
+      | Mint16unsigned, [IR addr], [IR res] ->
+          fprintf oc "	ldrh	%a, [%a, #0]\n" ireg res ireg addr; 1
+      | Mint16signed, [IR addr], [IR res] ->
+          fprintf oc "	ldrsh	%a, [%a, #0]\n" ireg res ireg addr; 1
+      | Mint32, [IR addr], [IR res] ->
+          fprintf oc "	ldr	%a, [%a, #0]\n" ireg res ireg addr; 1
+      | Mint64, [IR addr], [IR res1; IR res2] ->
+          if addr <> res2 then begin
+            fprintf oc "	ldr	%a, [%a, #0]\n" ireg res2 ireg addr;
+            fprintf oc "	ldr	%a, [%a, #4]\n" ireg res1 ireg addr
+          end else begin
+            fprintf oc "	ldr	%a, [%a, #4]\n" ireg res1 ireg addr;
+            fprintf oc "	ldr	%a, [%a, #0]\n" ireg res2 ireg addr
+          end; 2
+      | Mfloat32, [IR addr], [FR res] ->
+          fprintf oc "	vldr	%a, [%a, #0]\n" freg_single res ireg addr; 1
+      | Mfloat64, [IR addr], [FR res] ->
+          fprintf oc "	vldr	%a, [%a, #0]\n" freg res ireg addr; 1
+      | _ ->
+          assert false
+
+    let print_builtin_vload oc chunk args res =
+      fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+      let n = print_builtin_vload_common oc chunk args res in
+      fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n
+
+    let print_builtin_vload_global oc chunk id ofs args res =
+      fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+      let n1 = loadsymbol oc IR14 id ofs in
+      let n2 = print_builtin_vload_common oc chunk [IR IR14] res in
+      fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n1 + n2
+
+    let print_builtin_vstore_common oc chunk args =
+      match chunk, args with
+      | (Mint8signed | Mint8unsigned), [IR  addr; IR src] ->
+          fprintf oc "	strb	%a, [%a, #0]\n" ireg src ireg addr; 1
+      | (Mint16signed | Mint16unsigned), [IR  addr; IR src] ->
+          fprintf oc "	strh	%a, [%a, #0]\n" ireg src ireg addr; 1
+      | Mint32, [IR  addr; IR src] ->
+          fprintf oc "	str	%a, [%a, #0]\n" ireg src ireg addr; 1
+      | Mint64, [IR  addr; IR src1; IR src2] ->
+          fprintf oc "	str	%a, [%a, #0]\n" ireg src2 ireg addr;
+          fprintf oc "	str	%a, [%a, #4]\n" ireg src1 ireg addr; 2
+      | Mfloat32, [IR  addr; FR src] ->
+          fprintf oc "	vstr	%a, [%a, #0]\n" freg_single src ireg addr; 1
+      | Mfloat64, [IR  addr; FR src] ->
+          fprintf oc "	vstr	%a, [%a, #0]\n" freg src ireg addr; 1
+      | _ ->
+          assert false
+
+    let print_builtin_vstore oc chunk args =
+      fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+      let n = print_builtin_vstore_common oc chunk args in
+      fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n
+
+    let print_builtin_vstore_global oc chunk id ofs args =
+      fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+      let n1 = loadsymbol oc IR14 id ofs in
+      let n2 = print_builtin_vstore_common oc chunk (IR IR14 :: args) in
+      fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n1 + n2
+
+(* Handling of varargs *)
+
+    let align n a = (n + a - 1) land (-a)
+
+    let rec next_arg_location ir ofs = function
+      | [] ->
+          Int32.of_int (ir * 4 + ofs)
+      | (Tint | Tsingle | Tany32) :: l ->
+          if ir < 4
+          then next_arg_location (ir + 1) ofs l
+          else next_arg_location ir (ofs + 4) l
+      | (Tfloat | Tlong | Tany64) :: l ->
+          if ir < 3
+          then next_arg_location (align ir 2 + 2) ofs l
+          else next_arg_location ir (align ofs 8 + 8) l
+
+    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
+          (next_arg_location 0 0 (!current_function_sig).sig_args)
+          !current_function_stacksize in
+      let n = addimm oc "r14" "sp" (coqint_of_camlint ofs) in
+      fprintf oc "	str	r14, [%a, #0]\n" ireg r;
+      n + 1
 
 (* Auxiliary for 64-bit integer arithmetic built-ins.  They expand to
    two instructions, one computing the low 32 bits of the result,
@@ -331,6 +499,79 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       end else
         fn rl
 
+(* Handling of compiler-inlined builtins *)
+
+    let print_builtin_inline oc name args res =
+      fprintf oc "%s begin %s\n" comment name;
+      let n = match name, args, res with
+        (* Integer arithmetic *)
+      | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
+          fprintf oc "	rev	%a, %a\n" ireg res ireg a1; 1
+      | "__builtin_bswap16", [IR a1], [IR res] ->
+          fprintf oc "	rev16	%a, %a\n" ireg res ireg a1; 1
+      | "__builtin_clz", [IR a1], [IR res] ->
+          fprintf oc "	clz	%a, %a\n" ireg res ireg a1; 1
+            (* Float arithmetic *)
+      | "__builtin_fabs", [FR a1], [FR res] ->
+          fprintf oc "	vabs.f64 %a, %a\n" freg res freg a1; 1
+      | "__builtin_fsqrt", [FR a1], [FR res] ->
+          fprintf oc "	vsqrt.f64 %a, %a\n" freg res freg a1; 1
+            (* 64-bit integer arithmetic *)
+      | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
+          print_int64_arith oc (rl = ah) rl (fun rl ->
+            fprintf oc "	rsbs	%a, %a, #0\n" ireg rl ireg al;
+            (* No "rsc" instruction in Thumb2.  Emulate based on
+               rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry)
+               == mvn a, b; adc a, a, #0 *)
+            if !Clflags.option_mthumb then begin
+              fprintf oc "	mvn	%a, %a\n" ireg rh ireg ah;
+              fprintf oc "	adc	%a, %a, #0\n" ireg rh ireg rh; 3
+            end else begin
+              fprintf oc "	rsc	%a, %a, #0\n" ireg rh ireg ah; 2
+            end)
+      | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+          print_int64_arith oc (rl = ah || rl = bh) rl (fun rl ->
+            fprintf oc "	adds	%a, %a, %a\n" ireg rl ireg al ireg bl;
+            fprintf oc "	adc	%a, %a, %a\n" ireg rh ireg ah ireg bh; 2)
+      | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+          print_int64_arith oc (rl = ah || rl = bh) rl (fun rl ->
+            fprintf oc "	subs	%a, %a, %a\n" ireg rl ireg al ireg bl;
+            fprintf oc "	sbc	%a, %a, %a\n" ireg rh ireg ah ireg bh; 2)
+      | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
+          fprintf oc "	umull   %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1
+            (* Memory accesses *)
+      | "__builtin_read16_reversed", [IR a1], [IR res] ->
+          fprintf oc "	ldrh	%a, [%a, #0]\n" ireg res ireg a1;
+          fprintf oc "	rev16	%a, %a\n" ireg res ireg res; 2
+      | "__builtin_read32_reversed", [IR a1], [IR res] ->
+          fprintf oc "	ldr	%a, [%a, #0]\n" ireg res ireg a1;
+          fprintf oc "	rev	%a, %a\n" ireg res ireg res; 2
+      | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
+          fprintf oc "	rev16	%a, %a\n" ireg IR14 ireg a2;
+          fprintf oc "	strh	%a, [%a, #0]\n" ireg IR14 ireg a1; 2
+      | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
+          fprintf oc "	rev	%a, %a\n" ireg IR14 ireg a2;
+          fprintf oc "	str	%a, [%a, #0]\n" ireg IR14 ireg a1; 2
+            (* Synchronization *)
+      | "__builtin_membar", [], _ ->
+          0
+      | "__builtin_dmb", [], _ ->
+          fprintf oc "	dmb\n"; 1
+      | "__builtin_dsb", [], _ ->
+          fprintf oc "	dsb\n"; 1
+      | "__builtin_isb", [], _ ->
+          fprintf oc "	isb\n"; 1
+
+            (* Vararg stuff *)
+      | "__builtin_va_start", [IR a], _ ->
+          print_builtin_va_start oc a
+            (* Catch-all *)
+      | _ ->
+          invalid_arg ("unrecognized builtin " ^ name)
+      in
+      fprintf oc "%s end %s\n" comment name;
+      n
+
 (* Fixing up calling conventions *)
 
     type direction = Incoming | Outgoing
@@ -475,15 +716,11 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n
 
     let print_instruction oc = function
-      (* Core instructions *)
-      | Padc (r1,r2,so) ->
-	 fprintf oc "	adc	%a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
+        (* Core instructions *)
       | Padd(r1, r2, so) ->
           fprintf oc "	add%s	%a, %a, %a\n"
             (if !Clflags.option_mthumb && r2 <> IR14 then "s" else "")
             ireg r1 ireg r2 shift_op so; 1
-      | Padds (r1,r2,so) ->
-	 fprintf oc "	adds	%a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
       | Pand(r1, r2, so) ->
           fprintf oc "	and%t	%a, %a, %a\n"
             thumbS ireg r1 ireg r2 shift_op so; 1
@@ -494,8 +731,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           fprintf oc "	b	%a\n" print_label lbl; 1
       | Pbc(bit, lbl) ->
           fprintf oc "	b%s	%a\n" (condition_name bit) print_label lbl; 1
-      | Pbne lbl ->
-	 fprintf oc "	bne	%a\n" print_label lbl; 1
       | Pbsymb(id, sg) ->
           let n = fixup_arguments oc Outgoing sg in
           fprintf oc "	b	%a\n" symbol id;
@@ -520,19 +755,11 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Pbic(r1, r2, so) ->
           fprintf oc "	bic%t	%a, %a, %a\n"
             thumbS ireg r1 ireg r2 shift_op so; 1
-      | Pclz (r1,r2) ->
-	 fprintf oc "	clz	%a, %a\n" preg r1 preg r2; 1
       | Pcmp(r1, so) ->
           fprintf oc "	cmp	%a, %a\n" ireg r1 shift_op so; 1
-      | Pdmb ->
-	 fprintf oc "	dmb\n"; 1
-      | Pdsb ->
-	 fprintf oc "	dsb\n"; 1
-      |  Peor(r1, r2, so) ->
+      | Peor(r1, r2, so) ->
           fprintf oc "	eor%t	%a, %a, %a\n"
             thumbS ireg r1 ireg r2 shift_op so; 1
-      | Pisb ->
-	 fprintf oc "	isb\n"; 1
       | Pldr(r1, r2, sa) | Pldr_a(r1, r2, sa) ->
           fprintf oc "	ldr	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
       | Pldrb(r1, r2, sa) ->
@@ -564,22 +791,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Porr(r1, r2, so) ->
           fprintf oc "	orr%t	%a, %a, %a\n"
             thumbS ireg r1 ireg r2 shift_op so; 1
-      | Prev (r1,r2) ->
-	 fprintf oc "	rev	%a, %a\n" preg r1 preg r2; 1
-      | Prev16 (r1,r2) ->
-	 fprintf oc "	rev16	%a, %a\n" preg r1 preg r2; 1
       | Prsb(r1, r2, so) ->
-         fprintf oc "	rsb%t	%a, %a, %a\n"
-		 thumbS ireg r1 ireg r2 shift_op so; 1
-      | Prsbs(r1, r2, so) ->
-         fprintf oc "	rsbs	%a, %a, %a\n"
-		 ireg r1 ireg r2 shift_op so; 1
-      | Prsc (r1,r2,so) ->
-	 fprintf oc "	rsc	%a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
-      | Pfsqrt (f1,f2) ->
-	 fprintf oc "	vsqrt.f64 %a, %a\n" freg f1 freg f2; 1
-      | Psbc (r1,r2,sa) ->
-	 fprintf oc "	sbc	%a, %a, %a\n" ireg r1 ireg r2 shift_op sa; 1
+          fprintf oc "	rsb%t	%a, %a, %a\n"
+            thumbS ireg r1 ireg r2 shift_op so; 1
       | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) ->
           fprintf oc "	str	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa;
           begin match r1, r2, sa with
@@ -604,9 +818,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Psub(r1, r2, so) ->
           fprintf oc "	sub%t	%a, %a, %a\n"
             thumbS ireg r1 ireg r2 shift_op so; 1
-      | Psubs(r1, r2, so) ->
-         fprintf oc "	subs	%a, %a, %a\n"
-		 ireg r1 ireg r2 shift_op so; 1
       | Pudiv ->
           if Opt.hardware_idiv then begin
             fprintf oc "	udiv	r0, r0, r1\n"; 1
@@ -675,11 +886,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Pfdivs(r1, r2, r3) ->
           fprintf oc "	vdiv.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
       | Pfmuls(r1, r2, r3) ->
-         fprintf oc "	vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
-      | Ppush rl ->
-	 let first = ref true in
-	 let sep () = if !first then first := false else output_string oc ", " in
-	 fprintf oc "	push	{%a}\n"  (fun oc rl -> List.iter (fun ir -> sep (); ireg oc ir) rl) rl; ;1
+          fprintf oc "	vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
       | Pfsubs(r1, r2, r3) ->
           fprintf oc "	vsub.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
       | Pflis(r1, f) ->
@@ -731,9 +938,25 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           fprintf oc "	vstr	%a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1
             (* Pseudo-instructions *)
       | Pallocframe(sz, ofs) ->
-         assert false
+          fprintf oc "	mov	r12, sp\n";
+          if (!current_function_sig).sig_cc.cc_vararg then begin
+            fprintf oc "	push	{r0, r1, r2, r3}\n";
+            cfi_adjust oc 16l
+          end;
+          let sz' = camlint_of_coqint sz in
+          let ninstr = subimm oc "sp" "sp" sz in
+          cfi_adjust oc sz';
+          fprintf oc "	str	r12, [sp, #%a]\n" coqint ofs;
+          current_function_stacksize := sz';
+          ninstr + (if (!current_function_sig).sig_cc.cc_vararg then 3 else 2)
       | Pfreeframe(sz, ofs) ->
-	 assert false
+          let sz =
+            if (!current_function_sig).sig_cc.cc_vararg
+            then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz))
+            else sz in
+          if Asmgen.is_immed_arith sz
+          then fprintf oc "	add	sp, sp, #%a\n" coqint sz
+          else fprintf oc "	ldr	sp, [sp, #%a]\n" coqint ofs; 1
       | Plabel lbl ->
           fprintf oc "%a:\n" print_label lbl; 0
       | Ploadsymbol(r1, id, ofs) ->
@@ -765,6 +988,21 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           end
       | 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;
@@ -780,7 +1018,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           | _ ->
               assert false
           end
-      | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0
 
     let no_fallthrough = function
       | Pb _ -> true