(* *********************************************************************)
(*                                                                     *)
(*              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 ARM assembly code in asm syntax *)

open Printf
open Datatypes
open Camlcoq
open Sections
open AST
open Memdata
open Asm
open PrintAsmaux

(* Type for the ABI versions *)
type float_abi_type =
  | Hard
  | Soft

(* Module type for the options *)
module type PRINTER_OPTIONS =
    sig
      val float_abi: float_abi_type
      val vfpv3: bool
      val hardware_idiv: bool
     end

(* Module containing the printing functions *)

module Target (Opt: PRINTER_OPTIONS) : TARGET =
  struct
(* Code generation options. *)
    
    let literals_in_code = ref true     (* to be turned into a proper option *)
    
(* Basic printing functions *)
        
    let print_label oc lbl = elf_label oc (transl_label lbl)
        
    let comment = "@"

    let symbol = elf_symbol

    let symbol_offset oc (symb, ofs) =
      symbol oc symb;
      let ofs = camlint_of_coqint ofs in
      if ofs <> 0l then fprintf oc " + %ld" ofs

    let int_reg_name = function
      | IR0 -> "r0" | IR1 -> "r1" | IR2 -> "r2" | IR3 -> "r3"
      | IR4 -> "r4" | IR5 -> "r5" | IR6 -> "r6" | IR7 -> "r7"
      | IR8 -> "r8" | IR9 -> "r9" | IR10 -> "r10" | IR11 -> "r11"
      | IR12 -> "r12" | IR13 -> "sp" | IR14 -> "lr"
            
    let float_reg_name = function
      | FR0 -> "d0"  | FR1 -> "d1"  | FR2 -> "d2"  | FR3 -> "d3"
      | FR4 -> "d4"  | FR5 -> "d5"  | FR6 -> "d6"  | FR7 -> "d7"
      | FR8 -> "d8"  | FR9 -> "d9"  | FR10 -> "d10"  | FR11 -> "d11"
      | FR12 -> "d12"  | FR13 -> "d13"  | FR14 -> "d14"  | FR15 -> "d15"
            
    let single_float_reg_index = function
      | FR0 -> 0  | FR1 -> 2  | FR2 -> 4  | FR3 -> 6
      | FR4 -> 8  | FR5 -> 10  | FR6 -> 12  | FR7 -> 14
      | FR8 -> 16  | FR9 -> 18  | FR10 -> 20  | FR11 -> 22
      | FR12 -> 24  | FR13 -> 26  | FR14 -> 28  | FR15 -> 30
            
    let single_float_reg_name = function
      | FR0 -> "s0"  | FR1 -> "s2"  | FR2 -> "s4"  | FR3 -> "s6"
      | FR4 -> "s8"  | FR5 -> "s10"  | FR6 -> "s12"  | FR7 -> "s14"
      | FR8 -> "s16"  | FR9 -> "s18"  | FR10 -> "s20"  | FR11 -> "s22"
      | FR12 -> "s24"  | FR13 -> "s26"  | FR14 -> "s28"  | FR15 -> "s30"
            
    let ireg oc r = output_string oc (int_reg_name r)
    let freg oc r = output_string oc (float_reg_name r)
    let freg_single oc r = output_string oc (single_float_reg_name r)
        
    let preg oc = function
      | IR r -> ireg oc r
      | FR r -> freg oc r
      | _    -> assert false
            
    let condition_name = function
      | TCeq -> "eq"
      | TCne -> "ne"
      | TChs -> "hs"
      | TClo -> "lo"
      | TCmi -> "mi"
      | TCpl -> "pl"
      | TChi -> "hi"
      | TCls -> "ls"
      | TCge -> "ge"
      | TClt -> "lt"
      | TCgt -> "gt"
      | TCle -> "le"
            
    let neg_condition_name = function
      | TCeq -> "ne"
      | TCne -> "eq"
      | TChs -> "lo"
      | TClo -> "hs"
      | TCmi -> "pl"
      | TCpl -> "mi"
      | TChi -> "ls"
      | TCls -> "hi"
      | TCge -> "lt"
      | TClt -> "ge"
      | TCgt -> "le"
      | TCle -> "gt"
            
(* In Thumb2 mode, some arithmetic instructions have shorter encodings
   if they carry the "S" flag (update condition flags):
       add   (but not sp + imm)
       and
       asr
       bic
       eor
       lsl
       lsr
       mov
       mvn
       orr
       rsb
       sub    (but not sp - imm)
   The proof of Asmgen shows that CompCert-generated code behaves the
   same whether flags are updated or not by those instructions.  The
   following printing function adds a "S" suffix if we are in Thumb2
   mode. *)

    let thumbS oc =
      if !Clflags.option_mthumb then output_char oc 's'

(* Names of sections *)

    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 -> ".text"
      | Section_jumptable -> ".text"
      | Section_user(s, wr, ex) ->
          sprintf ".section	\"%s\",\"a%s%s\",%%progbits"
            s (if wr then "w" else "") (if ex then "x" else "")
      | Section_debug_info
      | Section_debug_abbrev -> "" (* Dummy value *)
            
    let section oc sec =
      fprintf oc "	%s\n" (name_of_section sec)
        
(* Record current code position and latest position at which to
   emit float and symbol constants. *)
        
    let currpos = ref 0
    let size_constants = ref 0
    let max_pos_constants = ref max_int
        
    let distance_to_emit_constants () =
      if !literals_in_code
      then !max_pos_constants - (!currpos + !size_constants)
      else max_int
          
(* Associate labels to floating-point constants and to symbols *)
          
    let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t)
    let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t)
        
    let label_float bf =
      try
        Hashtbl.find float_labels bf
      with Not_found ->
        let lbl' = new_label() in
        Hashtbl.add float_labels bf lbl';
        size_constants := !size_constants + 8;
        max_pos_constants := min !max_pos_constants (!currpos + 1024);
        lbl'
          
    let label_float32 bf =
      try
        Hashtbl.find float32_labels bf
      with Not_found ->
        let lbl' = new_label() in
        Hashtbl.add float32_labels bf lbl';
        size_constants := !size_constants + 4;
        max_pos_constants := min !max_pos_constants (!currpos + 1024);
        lbl'
          
    let symbol_labels =
      (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t)
        
    let label_symbol id ofs =
      try
        Hashtbl.find symbol_labels (id, ofs)
      with Not_found ->
        let lbl' = new_label() in
        Hashtbl.add symbol_labels (id, ofs) lbl';
        size_constants := !size_constants + 4;
        max_pos_constants := min !max_pos_constants (!currpos + 4096);
        lbl'
          
    let reset_constants () =
      Hashtbl.clear float_labels;
      Hashtbl.clear float32_labels;
      Hashtbl.clear symbol_labels;
      size_constants := 0;
      max_pos_constants := max_int
          
    let emit_constants oc =
      fprintf oc "	.balign	4\n";
      Hashtbl.iter
        (fun bf lbl ->
          (* Little-endian floats *)
          let bfhi = Int64.shift_right_logical bf 32
          and bflo = Int64.logand bf 0xFFFF_FFFFL in
          fprintf oc ".L%d:	.word	0x%Lx, 0x%Lx\n" lbl bflo bfhi)
        float_labels;
      Hashtbl.iter
        (fun bf lbl ->
          fprintf oc ".L%d:	.word	0x%lx\n" lbl bf)
        float32_labels;
      Hashtbl.iter
        (fun (id, ofs) lbl ->
          fprintf oc ".L%d:	.word	%a\n"
            lbl symbol_offset (id, ofs))
        symbol_labels;
      reset_constants ()
        
(* Generate code to load the address of id + ofs in register r *)
        
    let loadsymbol oc r id ofs =
      if !Clflags.option_mthumb then begin
        fprintf oc "	movw	%a, #:lower16:%a\n"
          ireg r symbol_offset (id, ofs);
        fprintf oc "	movt	%a, #:upper16:%a\n"
          ireg r symbol_offset (id, ofs); 2
      end else begin
        let lbl = label_symbol id ofs in
        fprintf oc "	ldr	%a, .L%d @ %a\n" 
          ireg r lbl symbol_offset (id, ofs); 1
      end
          
(* 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 movimm oc dst n =
      match Asmgen.decompose_int n with
      | [] -> assert false
      | hd::tl as l ->
          fprintf oc "	mov	%s, #%a\n" dst coqint hd;
          List.iter
            (fun n -> fprintf oc "	orr	%s, %s, #%a\n" dst dst coqint n)
            tl;
          List.length l
            
    let addimm oc dst src n =
      match Asmgen.decompose_int n with
      | [] -> assert false
      | hd::tl as l ->
          fprintf oc "	add	%s, %s, #%a\n" dst src coqint hd;
          List.iter
            (fun n -> fprintf oc "	add	%s, %s, #%a\n" dst dst coqint n)
            tl;
          List.length l
            
    let subimm oc dst src n =
      match Asmgen.decompose_int n with
      | [] -> assert false
      | hd::tl as l ->
          fprintf oc "	sub	%s, %s, #%a\n" dst src coqint hd;
          List.iter
            (fun n -> fprintf oc "	sub	%s, %s, #%a\n" dst dst coqint n)
            tl;
          List.length l
            
(* Recognition of float constants appropriate for VMOV.
   a normalized binary floating point encoding with 1 sign bit, 4
   bits of fraction and a 3-bit exponent *)
   
    let is_immediate_float64 bits =
      let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in
      let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in
      exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant
        
   let is_immediate_float32 bits =
     let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in
     let mant = Int32.logand bits 0x7F_FFFFl in
     exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant
       

(* 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-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 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 "sp" 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 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,
   followed by another computing the high 32 bits.  In cases where
   the first instruction would overwrite arguments to the second
   instruction, we must go through IR14 to hold the low 32 bits of the result.
 *)

    let print_int64_arith oc conflict rl fn =
      if conflict then begin
        let n = fn IR14 in
        fprintf oc "	mov%t	%a, %a\n" thumbS ireg rl ireg IR14;
        n + 1
      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

    module FixupEABI = struct

      let ireg_param = function
        | 0 -> IR0 | 1 -> IR1 | 2 -> IR2 | 3 -> IR3 | _ -> assert false

      let freg_param = function
        | 0 -> FR0 | 1 -> FR1 | 2 -> FR2 | 3 -> FR3 | _ -> assert false

      let fixup_double oc dir f i1 i2 =
        match dir with
        | Incoming ->     (* f <- (i1, i2)  *)
            fprintf oc "	vmov	%a, %a, %a\n" freg f ireg i1 ireg i2
        | Outgoing ->     (* (i1, i2) <- f *)
            fprintf oc "	vmov	%a, %a, %a\n" ireg i1 ireg i2 freg f

      let fixup_single oc dir f i =
        match dir with
        | Incoming ->     (* f <- i *)
            fprintf oc "	vmov	%a, %a\n" freg_single f ireg i
        | Outgoing ->     (* i <- f *)
            fprintf oc "	vmov	%a, %a\n" ireg i freg_single f

      let fixup_conventions oc dir tyl =
        let rec fixup i tyl =
          if i >= 4 then 0 else
          match tyl with
          | [] -> 0
          | (Tint | Tany32) :: tyl' ->
              fixup (i+1) tyl'
          | Tlong :: tyl' ->
              fixup (((i + 1) land (-2)) + 2) tyl'
          | (Tfloat | Tany64) :: tyl' ->
              let i = (i + 1) land (-2) in
              if i >= 4 then 0 else begin
                fixup_double oc dir (freg_param i) (ireg_param i) (ireg_param (i+1));
                1 + fixup (i+2) tyl'
              end
          | Tsingle :: tyl' ->
              fixup_single oc dir (freg_param i) (ireg_param i);
              1 + fixup (i+1) tyl'
        in fixup 0 tyl

      let fixup_arguments oc dir sg =
        fixup_conventions oc dir sg.sig_args

      let fixup_result oc dir sg =
        fixup_conventions oc dir (proj_sig_res sg :: [])

    end

    module FixupHF = struct

      type fsize = Single | Double

      let rec find_single used pos =
        if pos >= Array.length used then pos
        else if used.(pos) then find_single used (pos + 1)
        else begin used.(pos) <- true; pos end

      let rec find_double used pos =
        if pos + 1 >= Array.length used then pos
        else if used.(pos) || used.(pos + 1) then find_double used (pos + 2)
        else begin used.(pos) <- true; used.(pos + 1) <- true; pos / 2 end

      let rec fixup_actions used fr tyl =
        match tyl with
        | [] -> []
        | (Tint | Tlong | Tany32) :: tyl' -> fixup_actions used fr tyl'
        | (Tfloat | Tany64) :: tyl' ->
            if fr >= 8 then [] else begin
              let dr = find_double used 0 in
              assert (dr < 8);
              (fr, Double, dr) :: fixup_actions used (fr + 1) tyl'
            end
        | Tsingle :: tyl' ->
            if fr >= 8 then [] else begin
              let sr = find_single used 0 in
              assert (sr < 16);
              (fr, Single, sr) :: fixup_actions used (fr + 1) tyl'
            end

      let rec fixup_outgoing oc = function
        | [] -> 0
        | (fr, Double, dr) :: act ->
            if fr = dr then fixup_outgoing oc act else begin
              fprintf oc "	vmov.f64 d%d, d%d\n" dr fr;
              1 + fixup_outgoing oc act
            end
        | (fr, Single, sr) :: act ->
            fprintf oc "	vmov.f32 s%d, s%d\n" sr (2*fr);
            1 + fixup_outgoing oc act

      let rec fixup_incoming oc = function
        | [] -> 0
        | (fr, Double, dr) :: act ->
            let n = fixup_incoming oc act in
            if fr = dr then n else begin
              fprintf oc "	vmov.f64 d%d, d%d\n" fr dr;
              1 + n
            end
        | (fr, Single, sr) :: act ->
            let n = fixup_incoming oc act in
            if fr = sr then n else begin
              fprintf oc "	vmov.f32 s%d, s%d\n" (2*fr) sr;
              1 + n
            end

      let fixup_arguments oc dir sg =
        if sg.sig_cc.cc_vararg then
          FixupEABI.fixup_arguments oc dir sg
        else begin
          let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in
          match dir with
          | Outgoing -> fixup_outgoing oc act
          | Incoming -> fixup_incoming oc act
        end

      let fixup_result oc dir sg =
        if sg.sig_cc.cc_vararg then
          FixupEABI.fixup_result oc dir sg
        else
          0
    end

    let (fixup_arguments, fixup_result) =
      match Opt.float_abi with
      | Soft -> (FixupEABI.fixup_arguments, FixupEABI.fixup_result)
      | Hard -> (FixupHF.fixup_arguments, FixupHF.fixup_result)
            
(* Printing of instructions *)

    let shift_op oc = function
      | SOimm n -> fprintf oc "#%a" coqint n
      | SOreg r -> ireg oc r
      | SOlsl(r, n) -> fprintf oc "%a, lsl #%a" ireg r coqint n
      | SOlsr(r, n) -> fprintf oc "%a, lsr #%a" ireg r coqint n
      | SOasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n
      | SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n

    let print_instruction oc = function
        (* 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
      | Pand(r1, r2, so) ->
          fprintf oc "	and%t	%a, %a, %a\n"
            thumbS ireg r1 ireg r2 shift_op so; 1
      | Pasr(r1, r2, r3) ->
          fprintf oc "	asr%t	%a, %a, %a\n"
            thumbS ireg r1 ireg r2 ireg r3; 1
      | Pb lbl ->
          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
      | Pbsymb(id, sg) ->
          let n = fixup_arguments oc Outgoing sg in
          fprintf oc "	b	%a\n" symbol id;
          n + 1
      | Pbreg(r, sg) ->
          let n = 
            if r = IR14
            then fixup_result oc Outgoing sg
            else fixup_arguments oc Outgoing sg in
          fprintf oc "	bx	%a\n" ireg r;
          n + 1
      | Pblsymb(id, sg) ->
          let n1 = fixup_arguments oc Outgoing sg in
          fprintf oc "	bl	%a\n" symbol id;
          let n2 = fixup_result oc Incoming sg in
          n1 + 1 + n2
      | Pblreg(r, sg) ->
          let n1 = fixup_arguments oc Outgoing sg in
          fprintf oc "	blx	%a\n" ireg r;
          let n2 = fixup_result oc Incoming sg in
          n1 + 1 + n2
      | Pbic(r1, r2, so) ->
          fprintf oc "	bic%t	%a, %a, %a\n"
            thumbS ireg r1 ireg r2 shift_op so; 1
      | Pcmp(r1, so) ->
          fprintf oc "	cmp	%a, %a\n" ireg r1 shift_op so; 1
      | Peor(r1, r2, so) ->
          fprintf oc "	eor%t	%a, %a, %a\n"
            thumbS ireg r1 ireg r2 shift_op so; 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) ->
          fprintf oc "	ldrb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
      | Pldrh(r1, r2, sa) ->
          fprintf oc "	ldrh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
      | Pldrsb(r1, r2, sa) ->
          fprintf oc "	ldrsb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
      | Pldrsh(r1, r2, sa) ->
          fprintf oc "	ldrsh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
      | Plsl(r1, r2, r3) ->
          fprintf oc "	lsl%t	%a, %a, %a\n"
            thumbS ireg r1 ireg r2 ireg r3; 1
      | Plsr(r1, r2, r3) ->
          fprintf oc "	lsr%t	%a, %a, %a\n"
            thumbS ireg r1 ireg r2 ireg r3; 1
      | Pmla(r1, r2, r3, r4) ->
          fprintf oc "	mla	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
      | Pmov(r1, so) ->
          fprintf oc "	mov%t	%a, %a\n" thumbS ireg r1 shift_op so; 1
      | Pmovw(r1, n) ->
          fprintf oc "	movw	%a, #%a\n" ireg r1 coqint n; 1
      | Pmovt(r1, n) ->
          fprintf oc "	movt	%a, #%a\n" ireg r1 coqint n; 1
      | Pmul(r1, r2, r3) ->
          fprintf oc "	mul	%a, %a, %a\n" ireg r1 ireg r2 ireg r3; 1
      | Pmvn(r1, so) ->
          fprintf oc "	mvn%t	%a, %a\n" thumbS ireg r1 shift_op so; 1
      | Porr(r1, r2, so) ->
          fprintf oc "	orr%t	%a, %a, %a\n"
            thumbS ireg r1 ireg r2 shift_op so; 1
      | Prsb(r1, r2, so) ->
          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
          | IR14, IR13, SOimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n)
          | _ -> ()
          end;
          1
      | Pstrb(r1, r2, sa) ->
          fprintf oc "	strb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
      | Pstrh(r1, r2, sa) ->
          fprintf oc "	strh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
      | Psdiv ->
          if Opt.hardware_idiv then begin
            fprintf oc "	sdiv	r0, r0, r1\n"; 1
          end else begin
            fprintf oc "	bl	__aeabi_idiv\n"; 1
          end
      | Psbfx(r1, r2, lsb, sz) ->
          fprintf oc "	sbfx	%a, %a, #%a, #%a\n" ireg r1 ireg r2 coqint lsb coqint sz; 1
      | Psmull(r1, r2, r3, r4) ->
          fprintf oc "	smull	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
      | Psub(r1, r2, so) ->
          fprintf oc "	sub%t	%a, %a, %a\n"
            thumbS ireg r1 ireg r2 shift_op so; 1
      | Pudiv ->
          if Opt.hardware_idiv then begin
            fprintf oc "	udiv	r0, r0, r1\n"; 1
          end else begin
            fprintf oc "	bl	__aeabi_uidiv\n"; 1
          end
      | Pumull(r1, r2, r3, r4) ->
          fprintf oc "	umull	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
            (* Floating-point VFD instructions *)
      | Pfcpyd(r1, r2) ->
          fprintf oc "	vmov.f64 %a, %a\n" freg r1 freg r2; 1
      | Pfabsd(r1, r2) ->
          fprintf oc "	vabs.f64 %a, %a\n" freg r1 freg r2; 1
      | Pfnegd(r1, r2) ->
          fprintf oc "	vneg.f64 %a, %a\n" freg r1 freg r2; 1
      | Pfaddd(r1, r2, r3) ->
          fprintf oc "	vadd.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
      | Pfdivd(r1, r2, r3) ->
          fprintf oc "	vdiv.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
      | Pfmuld(r1, r2, r3) ->
          fprintf oc "	vmul.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
      | Pfsubd(r1, r2, r3) ->
          fprintf oc "	vsub.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
      | Pflid(r1, f) ->
          let f = camlint64_of_coqint(Floats.Float.to_bits f) in
          if Opt.vfpv3 && is_immediate_float64 f then begin
            fprintf oc "	vmov.f64 %a, #%F\n"
              freg r1 (Int64.float_of_bits f); 1
              (* immediate floats have at most 4 bits of fraction, so they
                 should print exactly with OCaml's F decimal format. *)
          end else if !literals_in_code then begin
            let lbl = label_float f in
            fprintf oc "	vldr	%a, .L%d @ %.12g\n"
              freg r1 lbl (Int64.float_of_bits f); 1
          end else begin
            let lbl = label_float f in
            fprintf oc "	movw	r14, #:lower16:.L%d\n" lbl;
            fprintf oc "	movt	r14, #:upper16:.L%d\n" lbl;
            fprintf oc "	vldr	%a, [r14, #0] @ %.12g\n"
              freg r1 (Int64.float_of_bits f); 3
          end
      | Pfcmpd(r1, r2) ->
          fprintf oc "	vcmp.f64 %a, %a\n" freg r1 freg r2;
          fprintf oc "	vmrs APSR_nzcv, FPSCR\n"; 2
      | Pfcmpzd(r1) ->
          fprintf oc "	vcmp.f64 %a, #0\n" freg r1;
          fprintf oc "	vmrs APSR_nzcv, FPSCR\n"; 2
      | Pfsitod(r1, r2) ->
          fprintf oc "	vmov	%a, %a\n" freg_single r1 ireg r2;
          fprintf oc "	vcvt.f64.s32 %a, %a\n" freg r1 freg_single r1; 2
      | Pfuitod(r1, r2) ->
          fprintf oc "	vmov	%a, %a\n" freg_single r1 ireg r2;
          fprintf oc "	vcvt.f64.u32 %a, %a\n" freg r1 freg_single r1; 2
      | Pftosizd(r1, r2) ->
          fprintf oc "	vcvt.s32.f64 %a, %a\n" freg_single FR6 freg r2;
          fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6; 2
      | Pftouizd(r1, r2) ->
          fprintf oc "	vcvt.u32.f64 %a, %a\n" freg_single FR6 freg r2;
          fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6; 2
      | Pfabss(r1, r2) ->
          fprintf oc "	vabs.f32 %a, %a\n" freg_single r1 freg_single r2; 1
      | Pfnegs(r1, r2) ->
          fprintf oc "	vneg.f32 %a, %a\n" freg_single r1 freg_single r2; 1
      | Pfadds(r1, r2, r3) ->
          fprintf oc "	vadd.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
      | 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
      | 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) ->
          let f = camlint_of_coqint(Floats.Float32.to_bits f) in
          if Opt.vfpv3 && is_immediate_float32 f then begin
            fprintf oc "	vmov.f32 %a, #%F\n"
              freg_single r1 (Int32.float_of_bits f); 1
              (* immediate floats have at most 4 bits of fraction, so they
                 should print exactly with OCaml's F decimal format. *)
          end else if !literals_in_code then begin
            let lbl = label_float32 f in
            fprintf oc "	vldr	%a, .L%d @ %.12g\n"
              freg_single r1 lbl (Int32.float_of_bits f); 1
          end else begin
            fprintf oc "	movw	r14, #%ld\n" (Int32.logand f 0xFFFFl);
            fprintf oc "	movt	r14, #%ld\n" (Int32.shift_right_logical f 16);
            fprintf oc "	vmov	%a, r14 @ %.12g\n"
              freg_single r1 (Int32.float_of_bits f); 3
          end
      | Pfcmps(r1, r2) ->
          fprintf oc "	vcmp.f32 %a, %a\n" freg_single r1 freg_single r2;
          fprintf oc "	vmrs APSR_nzcv, FPSCR\n"; 2
      | Pfcmpzs(r1) ->
          fprintf oc "	vcmp.f32 %a, #0\n" freg_single r1;
          fprintf oc "	vmrs APSR_nzcv, FPSCR\n"; 2
      | Pfsitos(r1, r2) ->
          fprintf oc "	vmov	%a, %a\n" freg_single r1 ireg r2;
          fprintf oc "	vcvt.f32.s32 %a, %a\n" freg_single r1 freg_single r1; 2
      | Pfuitos(r1, r2) ->
          fprintf oc "	vmov	%a, %a\n" freg_single r1 ireg r2;
          fprintf oc "	vcvt.f32.u32 %a, %a\n" freg_single r1 freg_single r1; 2
      | Pftosizs(r1, r2) ->
          fprintf oc "	vcvt.s32.f32 %a, %a\n" freg_single FR6 freg_single r2;
          fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6; 2
      | Pftouizs(r1, r2) ->
          fprintf oc "	vcvt.u32.f32 %a, %a\n" freg_single FR6 freg_single r2;
          fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6; 2
      | Pfcvtsd(r1, r2) ->
          fprintf oc "	vcvt.f32.f64 %a, %a\n" freg_single r1 freg r2; 1
      | Pfcvtds(r1, r2) ->
          fprintf oc "	vcvt.f64.f32 %a, %a\n" freg r1 freg_single r2; 1
      | Pfldd(r1, r2, n) | Pfldd_a(r1, r2, n) ->
          fprintf oc "	vldr	%a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1
      | Pflds(r1, r2, n) ->
          fprintf oc "	vldr	%a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1
      | Pfstd(r1, r2, n) | Pfstd_a(r1, r2, n) ->
          fprintf oc "	vstr	%a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1
      | Pfsts(r1, r2, n) ->
          fprintf oc "	vstr	%a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1
            (* Pseudo-instructions *)
      | Pallocframe(sz, ofs) ->
          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) ->
          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) ->
          loadsymbol oc r1 id ofs
      | Pmovite(cond, r1, ifso, ifnot) ->
          fprintf oc "	ite	%s\n" (condition_name cond);
          fprintf oc "	mov%s	%a, %a\n"
            (condition_name cond) ireg r1 shift_op ifso;
          fprintf oc "	mov%s	%a, %a\n"
            (neg_condition_name cond) ireg r1 shift_op ifnot; 2
      | Pbtbl(r, tbl) ->
          if !Clflags.option_mthumb then begin
            let lbl = new_label() in
            fprintf oc "	adr	r14, .L%d\n" lbl;
            fprintf oc "	add	r14, r14, %a, lsl #2\n" ireg r;
            fprintf oc "	mov	pc, r14\n";
            fprintf oc ".L%d:\n" lbl;
            List.iter
              (fun l -> fprintf oc "	b.w	%a\n" print_label l)
              tbl;
            3 + List.length tbl
          end else begin
            fprintf oc "	add	pc, pc, %a, lsl #2\n" ireg r;
            fprintf oc "	nop\n";
            List.iter
              (fun l -> fprintf oc "	b	%a\n" print_label l)
              tbl;
            2 + List.length tbl
          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) ->
              fprintf oc "%s begin inline assembly\n" comment;
              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
              fprintf oc "%s end inline assembly\n" comment;
              5 (* hoping this is an upper bound...  *)
          | _ ->
              assert false
          end
      | Pannot(ef, args) ->
          begin match ef with
          | EF_annot(txt, targs) ->
              print_annot_stmt oc (extern_atom txt) targs args; 0
          | _ ->
              assert false
          end

    let no_fallthrough = function
      | Pb _ -> true
      | Pbsymb _ -> true
      | Pbreg _ -> true
      | _ -> false

    let rec print_instructions oc instrs =
      match instrs with
      | [] -> ()
      | i :: il ->
          let n = print_instruction oc i in
          currpos := !currpos + n * 4;
          let d = distance_to_emit_constants() in
          if d < 256 && no_fallthrough i then
            emit_constants oc
          else if d < 16 then begin
            let lbl = new_label() in
            fprintf oc "	b	.L%d\n" lbl;
            emit_constants oc;
            fprintf oc ".L%d:\n" lbl
          end;
          print_instructions oc il

    let get_section_names name =
      let (text, lit) =
        match C2C.atom_sections name with
        | t :: l :: _ -> (t, l)
        | _    -> (Section_text, Section_literal) in
      text,lit,Section_jumptable

    let print_align oc alignment =
      fprintf oc "	.balign %d\n" alignment

    let print_jumptable _ _ = ()

    let cfi_startproc = cfi_startproc

    let cfi_endproc = cfi_endproc

    let print_optional_fun_info oc =
      if !Clflags.option_mthumb then
        fprintf oc "	.thumb_func\n"

    let print_fun_info oc name =
      fprintf oc "	.type	%a, %%function\n" symbol name;
      fprintf oc "	.size	%a, . - %a\n" symbol name symbol name

    let print_var_info oc name =
      fprintf oc "	.type	%a, %%object\n" symbol name;
      fprintf oc "	.size	%a, . - %a\n" symbol name symbol name

    let print_comm_symb oc sz name align =
      if C2C.atom_is_static name then
        fprintf oc "	.local	%a\n" symbol name;
      fprintf oc "	.comm	%a, %s, %d\n"
        symbol name
        (Z.to_string sz)
        align

    let print_instructions oc fn =
      current_function_sig := fn.fn_sig;
      ignore (fixup_arguments oc Incoming fn.fn_sig);
      print_instructions oc fn.fn_code;
      if !literals_in_code then emit_constants oc

    let emit_constants oc lit =
      if not !literals_in_code && !size_constants > 0 then begin
        section oc lit;
        emit_constants oc
      end

(* Data *)

    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 "	.word	%ld\n" (camlint_of_coqint n)
      | Init_int64 n ->
          fprintf oc "	.quad	%Ld\n" (camlint64_of_coqint n)
      | Init_float32 n ->
          fprintf oc "	.word	0x%lx %s %.15g \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 "	.word	%a\n" symbol_offset (symb, ofs)
            
    let print_prologue oc =
      fprintf oc "	.syntax	unified\n";
      fprintf oc "	.arch	%s\n"
        (match Configuration.model with
        | "armv6" -> "armv6"
        | "armv7a" -> "armv7-a"
        | "armv7r" -> "armv7-r"
        | "armv7m" -> "armv7-m"
        | _ -> "armv7");
      fprintf oc "	.fpu	%s\n"
        (if Opt.vfpv3 then "vfpv3-d16" else "vfpv2");
      fprintf oc "	.%s\n" (if !Clflags.option_mthumb then "thumb" else "arm")

    let print_epilogue oc = ()

    let default_falignment = 4

    let get_start_addr () = -1 (* Dummy constant *)

    let get_end_addr () = -1 (* Dummy constant *)

    let get_stmt_list_addr () = -1 (* Dummy constant *)

    module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs (* Dummy Abbrev types *)
        
    let label = elf_label
       
    let new_label = new_label
        
    let print_file_loc _ _ = () (* Dummy function *)
  end

let sel_target () = 
  let module S : PRINTER_OPTIONS = struct
   
   let vfpv3 = Configuration.model >= "armv7"
   
   let float_abi = match Configuration.abi with
   | "eabi"      -> Soft
   | "hardfloat" -> Hard
   | _ -> assert false
   
   let hardware_idiv  =
   match  Configuration.model with
   | "armv7r" | "armv7m" -> !Clflags.option_mthumb
   | _ -> false

   end in
  (module Target(S):TARGET)