(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*         Xavier Leroy, Collège de France and INRIA Paris             *)
(*                                                                     *)
(*  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 AArch64 assembly code in asm syntax *)

open Printf
open Camlcoq
open Sections
open AST
open Asm
open AisAnnot
open PrintAsmaux
open Fileinfo

let intsz oc (sz, n) =
  match sz with X -> coqint64 oc n | W -> coqint oc n

let xreg_name = function
  | X0 -> "x0"   | X1 -> "x1"   | X2 -> "x2"   | X3 -> "x3"
  | X4 -> "x4"   | X5 -> "x5"   | X6 -> "x6"   | X7 -> "x7"
  | X8 -> "x8"   | X9 -> "x9"   | X10 -> "x10" | X11 -> "x11"
  | X12 -> "x12" | X13 -> "x13" | X14 -> "x14" | X15 -> "x15"
  | X16 -> "x16" | X17 -> "x17" | X18 -> "x18" | X19 -> "x19"
  | X20 -> "x20" | X21 -> "x21" | X22 -> "x22" | X23 -> "x23"
  | X24 -> "x24" | X25 -> "x25" | X26 -> "x26" | X27 -> "x27"
  | X28 -> "x28" | X29 -> "x29" | X30 -> "x30"

let wreg_name = function
  | X0 -> "w0"   | X1 -> "w1"   | X2 -> "w2"   | X3 -> "w3"
  | X4 -> "w4"   | X5 -> "w5"   | X6 -> "w6"   | X7 -> "w7"
  | X8 -> "w8"   | X9 -> "w9"   | X10 -> "w10" | X11 -> "w11"
  | X12 -> "w12" | X13 -> "w13" | X14 -> "w14" | X15 -> "w15"
  | X16 -> "w16" | X17 -> "w17" | X18 -> "w18" | X19 -> "w19"
  | X20 -> "w20" | X21 -> "w21" | X22 -> "w22" | X23 -> "w23"
  | X24 -> "w24" | X25 -> "w25" | X26 -> "w26" | X27 -> "w27"
  | X28 -> "w28" | X29 -> "w29" | X30 -> "w30"

let xreg0_name = function RR0 r -> xreg_name r | XZR -> "xzr"
let wreg0_name = function RR0 r -> wreg_name r | XZR -> "wzr"

let xregsp_name = function RR1 r -> xreg_name r | XSP -> "sp"
let wregsp_name = function RR1 r -> wreg_name r | XSP -> "wsp"

let dreg_name = function
| D0 -> "d0"   | D1 -> "d1"   | D2 -> "d2"   | D3 -> "d3"
| D4 -> "d4"   | D5 -> "d5"   | D6 -> "d6"   | D7 -> "d7"
| D8 -> "d8"   | D9 -> "d9"   | D10 -> "d10" | D11 -> "d11"
| D12 -> "d12" | D13 -> "d13" | D14 -> "d14" | D15 -> "d15"
| D16 -> "d16" | D17 -> "d17" | D18 -> "d18" | D19 -> "d19"
| D20 -> "d20" | D21 -> "d21" | D22 -> "d22" | D23 -> "d23"
| D24 -> "d24" | D25 -> "d25" | D26 -> "d26" | D27 -> "d27"
| D28 -> "d28" | D29 -> "d29" | D30 -> "d30" | D31 -> "d31"

let sreg_name = function
| D0 -> "s0"   | D1 -> "s1"   | D2 -> "s2"   | D3 -> "s3"
| D4 -> "s4"   | D5 -> "s5"   | D6 -> "s6"   | D7 -> "s7"
| D8 -> "s8"   | D9 -> "s9"   | D10 -> "s10" | D11 -> "s11"
| D12 -> "s12" | D13 -> "s13" | D14 -> "s14" | D15 -> "s15"
| D16 -> "s16" | D17 -> "s17" | D18 -> "s18" | D19 -> "s19"
| D20 -> "s20" | D21 -> "s21" | D22 -> "s22" | D23 -> "s23"
| D24 -> "s24" | D25 -> "s25" | D26 -> "s26" | D27 -> "s27"
| D28 -> "s28" | D29 -> "s29" | D30 -> "s30" | D31 -> "s31"

let xreg oc r = output_string oc (xreg_name r)
let wreg oc r = output_string oc (wreg_name r)
let ireg oc (sz, r) =
  output_string oc (match sz with X -> xreg_name r | W -> wreg_name r)

let xreg0 oc r = output_string oc (xreg0_name r)
let wreg0 oc r = output_string oc (wreg0_name r)
let ireg0 oc (sz, r) =
  output_string oc (match sz with X -> xreg0_name r | W -> wreg0_name r)

let xregsp oc r = output_string oc (xregsp_name r)
let iregsp oc (sz, r) =
  output_string oc (match sz with X -> xregsp_name r | W -> wregsp_name r)

let dreg oc r = output_string oc (dreg_name r)
let sreg oc r = output_string oc (sreg_name r)
let freg oc (sz, r) =
  output_string oc (match sz with D -> dreg_name r | S -> sreg_name r)

let preg_asm oc ty = function
    | DR (IR (RR1 r)) -> if ty = Tint then wreg oc r else xreg oc r
    | DR (FR r) -> if ty = Tsingle then sreg oc r else dreg oc r
| _    -> assert false

let preg_annot = function
    | DR (IR (RR1 r)) -> xreg_name r
    | DR (FR r) -> dreg_name r
    | _ -> assert false

(* Base-2 log of a Caml integer *)
let rec log2 n =
  assert (n > 0);
  if n = 1 then 0 else 1 + log2 (n lsr 1)

(* System dependent printer functions *)

module type SYSTEM =
  sig
    val comment: string
    val raw_symbol: out_channel -> string -> unit
    val symbol: out_channel -> P.t -> unit
    val symbol_offset_high: out_channel -> P.t * Z.t -> unit
    val symbol_offset_low: out_channel -> P.t * Z.t -> unit
    val label: out_channel -> int -> unit
    val label_high: out_channel -> int -> unit
    val label_low: out_channel -> int -> unit
    val load_symbol_address: out_channel -> ireg -> P.t -> unit
    val name_of_section: section_name -> string
    val print_fun_info:  out_channel -> P.t -> unit
    val print_var_info: out_channel -> P.t -> unit
    val print_comm_decl: out_channel -> P.t -> Z.t -> int -> unit
    val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit
  end

module ELF_System : SYSTEM =
  struct
    let comment = "//"
    let raw_symbol = output_string
    let symbol = elf_symbol
    let symbol_offset_high = elf_symbol_offset
    let symbol_offset_low oc id_ofs =
      fprintf oc "#:lo12:%a" elf_symbol_offset id_ofs

    let label = elf_label
    let label_high = elf_label
    let label_low oc lbl =
      fprintf oc "#:lo12:%a" elf_label lbl

    let load_symbol_address oc rd id =
        fprintf oc "	adrp	%a, :got:%a\n" xreg rd symbol id;
        fprintf oc "	ldr	%a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id

    (* Names of sections *)

    let name_of_section = function
      | Section_text         -> ".text"
      | Section_data(i, true) ->
         failwith "_Thread_local unsupported on this platform"
      | Section_data(i, false) | Section_small_data i ->
          variable_section ~sec:".data" ~bss:".bss" i
      | Section_const i | Section_small_const i ->
          variable_section ~sec:".section	.rodata" i
      | Section_string       -> ".section	.rodata"
      | Section_literal      -> ".section	.rodata"
      | Section_jumptable    -> ".section	.rodata"
      | Section_debug_info _ -> ".section	.debug_info,\"\",%progbits"
      | Section_debug_loc    -> ".section	.debug_loc,\"\",%progbits"
      | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",%progbits"
      | Section_debug_line _ -> ".section	.debug_line,\"\",%progbits"
      | Section_debug_ranges -> ".section	.debug_ranges,\"\",%progbits"
      | Section_debug_str    -> ".section	.debug_str,\"MS\",%progbits,1"
      | Section_user(s, wr, ex) ->
          sprintf ".section	\"%s\",\"a%s%s\",%%progbits"
            s (if wr then "w" else "") (if ex then "x" else "")
      | Section_ais_annotation -> sprintf ".section	\"__compcert_ais_annotations\",\"\",@note"

    let print_fun_info = elf_print_fun_info
    let print_var_info = elf_print_var_info

    let print_comm_decl oc name sz al =
      fprintf oc "	.comm	%a, %s, %d\n" symbol name (Z.to_string sz) al

    let print_lcomm_decl oc name sz al =
      fprintf oc "	.local	%a\n" symbol name;
      print_comm_decl oc name sz al
    
  end

module MacOS_System : SYSTEM =
  struct
    let comment = ";"

    let raw_symbol oc s =
      fprintf oc "_%s" s

    let symbol oc symb =
      raw_symbol oc (extern_atom symb)

    let symbol_offset_gen kind oc (id, ofs) =
      fprintf oc "%a@%s" symbol id kind;
      let ofs = camlint64_of_ptrofs ofs in
      if ofs <> 0L then fprintf oc " + %Ld" ofs

    let symbol_offset_high = symbol_offset_gen "PAGE"
    let symbol_offset_low = symbol_offset_gen "PAGEOFF"

    let label oc lbl =
      fprintf oc "L%d" lbl

    let label_high oc lbl =
      fprintf oc "%a@PAGE" label lbl
    let label_low oc lbl =
      fprintf oc "%a@PAGEOFF" label lbl

    let load_symbol_address oc rd id =
      fprintf oc "	adrp	%a, %a@GOTPAGE\n" xreg rd symbol id;
      fprintf oc "	ldr	%a, [%a, %a@GOTPAGEOFF]\n" xreg rd xreg rd symbol id

    let name_of_section = function
      | Section_text -> ".text"
      | Section_data(i, true) ->
         failwith "_Thread_local unsupported on this platform"
      | Section_data(i, false) | Section_small_data i ->
          variable_section ~sec:".data" i
      | Section_const i  | Section_small_const i ->
          variable_section ~sec:".const" ~reloc:".const_data" i
      | Section_string -> ".const"
      | Section_literal -> ".const"
      | Section_jumptable -> ".text"
      | Section_user(s, wr, ex) ->
          sprintf ".section	\"%s\", %s, %s"
            (if wr then "__DATA" else "__TEXT") s
            (if ex then "regular, pure_instructions" else "regular")
      | Section_debug_info _ ->	".section	__DWARF,__debug_info,regular,debug"
      | Section_debug_loc  -> ".section	__DWARF,__debug_loc,regular,debug"
      | Section_debug_line _ -> ".section	__DWARF,__debug_line,regular,debug"
      | Section_debug_str -> ".section	__DWARF,__debug_str,regular,debug"
      | Section_debug_ranges -> ".section	__DWARF,__debug_ranges,regular,debug"
      | Section_debug_abbrev -> ".section	__DWARF,__debug_abbrev,regular,debug"
      | Section_ais_annotation -> assert false (* Not supported under MacOS *)

    let print_fun_info _ _ = ()
    let print_var_info _ _ = ()

    let print_comm_decl oc name sz al =
      fprintf oc "	.comm	%a, %s, %d\n"
                 symbol name (Z.to_string sz) (log2 al)

    let print_lcomm_decl oc name sz al =
      fprintf oc "	.lcomm	%a, %s, %d\n"
                 symbol name (Z.to_string sz) (log2 al)

  end

(* Module containing the printing functions *)

module Target(System: SYSTEM): TARGET =
  struct
    include System

(* Basic printing functions *)

    let print_label oc lbl = label oc (transl_label lbl)

(* Names of sections *)

    let section oc sec =
      fprintf oc "	%s\n" (name_of_section sec)

(* Associate labels to floating-point constants and to symbols. *)

    let emit_constants oc lit =
      if exists_constants () then begin
         section oc lit;
         if Hashtbl.length literal64_labels > 0 then
           begin
             fprintf oc "	.balign 8\n";
             Hashtbl.iter
               (fun bf lbl -> fprintf oc "%a:	.quad	0x%Lx\n" label lbl bf)
               literal64_labels
           end;
         if Hashtbl.length literal32_labels > 0 then
           begin
             fprintf oc "	.balign	4\n";
             Hashtbl.iter
               (fun bf lbl ->
                  fprintf oc "%a:	.long	0x%lx\n" label lbl bf)
               literal32_labels
           end;
         reset_literals ()
      end

(* Emit .file / .loc debugging directives *)

    let print_file_line oc file line =
      print_file_line oc comment file line

(* Name of testable condition *)

    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"

(* Print an addressing mode *)

    let addressing oc = function
    | ADimm(base, n) -> fprintf oc "[%a, #%a]" xregsp base coqint64 n
    | ADreg(base, r) -> fprintf oc "[%a, %a]" xregsp base xreg r
    | ADlsl(base, r, n) -> fprintf oc "[%a, %a, lsl #%a]" xregsp base xreg r coqint n
    | ADsxt(base, r, n) -> fprintf oc "[%a, %a, sxtw #%a]" xregsp base wreg r coqint n
    | ADuxt(base, r, n) -> fprintf oc "[%a, %a, uxtw #%a]" xregsp base wreg r coqint n
    | ADadr(base, id, ofs) -> fprintf oc "[%a, %a]" xregsp base symbol_offset_low (id, ofs)
    | ADpostincr(base, n) -> fprintf oc "[%a], #%a" xregsp base coqint64 n

(* Print a shifted operand *)
    let shiftop oc = function
    | SOnone -> ()
    | SOlsl n -> fprintf oc ", lsl #%a" coqint n
    | SOlsr n -> fprintf oc ", lsr #%a" coqint n
    | SOasr n -> fprintf oc ", asr #%a" coqint n
    | SOror n -> fprintf oc ", ror #%a" coqint n

(* Print a sign- or zero-extended register operand *)
    let regextend oc = function
    | (r, EOsxtb n) -> fprintf oc "%a, sxtb #%a" wreg r coqint n
    | (r, EOsxth n) -> fprintf oc "%a, sxth #%a" wreg r coqint n
    | (r, EOsxtw n) -> fprintf oc "%a, sxtw #%a" wreg r coqint n
    | (r, EOuxtb n) -> fprintf oc "%a, uxtb #%a" wreg r coqint n
    | (r, EOuxth n) -> fprintf oc "%a, uxth #%a" wreg r coqint n
    | (r, EOuxtw n) -> fprintf oc "%a, uxtw #%a" wreg r coqint n
    | (r, EOuxtx n) -> fprintf oc "%a, uxtx #%a" xreg r coqint n

    let next_profiling_label =
      let atomic_incr_counter = ref 0 in
      fun () ->
      let r = sprintf ".Lcompcert_atomic_incr%d" !atomic_incr_counter in
      incr atomic_incr_counter; r;;
                
    let print_profiling_logger oc id kind =
      assert (kind >= 0);
      assert (kind <= 1);
      fprintf oc "%s begin profiling %a %d: atomic increment\n" comment
        Profilingaux.pp_id id kind;
      let ofs = profiling_offset id kind and lbl = next_profiling_label () in
      fprintf oc "	adrp	x15, %s+%d\n" profiling_counter_table_name ofs;
      fprintf oc "	add	x15, x15, :lo12:(%s+%d)\n" profiling_counter_table_name ofs;
      fprintf oc "%s:\n" lbl;
      fprintf oc "	ldaxr	x17, [x15]\n";
      fprintf oc "	add	x17, x17, 1\n";
      fprintf oc "	stlxr	w29, x17, [x15]\n";
      fprintf oc "	cbnz	w29, %s\n" lbl;
      fprintf oc "%s end profiling %a %d\n" comment
        Profilingaux.pp_id id kind;;

(* Printing of instructions *)
    let print_instruction oc = function
    (* Branches *)
    | Pb lbl ->
        fprintf oc "	b	%a\n" print_label lbl
    | Pbc(c, lbl) ->
        fprintf oc "	b.%s	%a\n" (condition_name c) print_label lbl
    | Pbl(id, sg) ->
        fprintf oc "	bl	%a\n" symbol id
    | Pbs(id, sg) ->
        fprintf oc "	b	%a\n" symbol id
    | Pblr(r, sg) ->
        fprintf oc "	blr	%a\n" xreg r
    | Pbr(r, sg) ->
        fprintf oc "	br	%a\n" xreg r
    | Pret r ->
        fprintf oc "	ret	%a\n" xreg r
    | Pcbnz(sz, r, lbl) ->
        fprintf oc "	cbnz	%a, %a\n" ireg (sz, r) print_label lbl
    | Pcbz(sz, r, lbl) ->
        fprintf oc "	cbz	%a, %a\n" ireg (sz, r) print_label lbl
    | Ptbnz(sz, r, n, lbl) ->
        fprintf oc "	tbnz	%a, #%a, %a\n" ireg (sz, r) coqint n print_label lbl
    | Ptbz(sz, r, n, lbl) ->
        fprintf oc "	tbz	%a, #%a, %a\n" ireg (sz, r) coqint n print_label lbl
    (* Memory loads and stores *)
    | Pldrw(rd, a) | Pldrw_a(rd, a) ->
        fprintf oc "	ldr	%a, %a\n" wreg rd addressing a
    | Pldrx(rd, a) | Pldrx_a(rd, a) ->
        fprintf oc "	ldr	%a, %a\n" xreg rd addressing a
    | Pldrb(sz, rd, a) ->
        fprintf oc "	ldrb	%a, %a\n" wreg rd addressing a
    | Pldrsb(sz, rd, a) ->
        fprintf oc "	ldrsb	%a, %a\n" ireg (sz, rd) addressing a
    | Pldrh(sz, rd, a) ->
        fprintf oc "	ldrh	%a, %a\n" wreg rd addressing a
    | Pldrsh(sz, rd, a) ->
        fprintf oc "	ldrsh	%a, %a\n" ireg (sz, rd) addressing a
    | Pldrzw(rd, a) ->
        fprintf oc "	ldr	%a, %a\n" wreg rd addressing a
        (* the upper 32 bits of Xrd are set to 0, performing zero-extension *)
    | Pldrsw(rd, a) ->
        fprintf oc "	ldrsw	%a, %a\n" xreg rd addressing a
    | Pldpw(rd1, rd2, _, _, a) ->
        fprintf oc "	ldp	%a, %a, %a\n" wreg rd1 wreg rd2 addressing a
    | Pldpx(rd1, rd2, _, _, a) ->
        fprintf oc "	ldp	%a, %a, %a\n" xreg rd1 xreg rd2 addressing a
    | Pstrw(rs, a) | Pstrw_a(rs, a) ->
        fprintf oc "	str	%a, %a\n" wreg rs addressing a
    | Pstrx(rs, a) | Pstrx_a(rs, a) ->
        fprintf oc "	str	%a, %a\n" xreg rs addressing a
    | Pstrb(rs, a) ->
        fprintf oc "	strb	%a, %a\n" wreg rs addressing a
    | Pstrh(rs, a) ->
        fprintf oc "	strh	%a, %a\n" wreg rs addressing a
    | Pstpw(rs1, rs2, _, _, a) ->
        fprintf oc "	stp	%a, %a, %a\n" wreg rs1 wreg rs2 addressing a
    | Pstpx(rs1, rs2, _, _, a) ->
        fprintf oc "	stp	%a, %a, %a\n" xreg rs1 xreg rs2 addressing a
    (* Integer arithmetic, immediate *)
    | Paddimm(sz, rd, r1, n) ->
        fprintf oc "	add	%a, %a, #%a\n" iregsp (sz, rd) iregsp (sz, r1) intsz (sz, n)
    | Psubimm(sz, rd, r1, n) ->
        fprintf oc "	sub	%a, %a, #%a\n" iregsp (sz, rd) iregsp (sz, r1) intsz (sz, n)
    | Pcmpimm(sz, r1, n) ->
        fprintf oc "	cmp	%a, #%a\n" ireg (sz, r1) intsz (sz, n)
    | Pcmnimm(sz, r1, n) ->
        fprintf oc "	cmn	%a, #%a\n" ireg (sz, r1) intsz (sz, n)
    (* Move integer register *)
    | Pmov(rd, r1) ->
        fprintf oc "	mov	%a, %a\n" xregsp rd xregsp r1
    (* Logical, immediate *)
    | Pandimm(sz, rd, r1, n) ->
        fprintf oc "	and	%a, %a, #%a\n" ireg (sz, rd) ireg0 (sz, r1) intsz (sz, n)
    | Peorimm(sz, rd, r1, n) ->
        fprintf oc "	eor	%a, %a, #%a\n" ireg (sz, rd) ireg0 (sz, r1) intsz (sz, n)
    | Porrimm(sz, rd, r1, n) ->
        fprintf oc "	orr	%a, %a, #%a\n" ireg (sz, rd) ireg0 (sz, r1) intsz (sz, n)
    | Ptstimm(sz, r1, n) ->
        fprintf oc "	tst	%a, #%a\n" ireg (sz, r1) intsz (sz, n)
    (* Move wide immediate *)
    | Pmovz(sz, rd, n, pos) ->
        fprintf oc "	movz	%a, #%d, lsl #%d\n" ireg (sz, rd) (Z.to_int n) (Z.to_int pos)
    | Pmovn(sz, rd, n, pos) ->
        fprintf oc "	movn	%a, #%d, lsl #%d\n" ireg (sz, rd) (Z.to_int n) (Z.to_int pos)
    | Pmovk(sz, rd, n, pos) ->
        fprintf oc "	movk	%a, #%d, lsl #%d\n" ireg (sz, rd) (Z.to_int n) (Z.to_int pos)
    (* PC-relative addressing *)
    | Padrp(rd, id, ofs) ->
        fprintf oc "	adrp	%a, %a\n" xreg rd symbol_offset_high (id, ofs)
    | Paddadr(rd, r1, id, ofs) ->
        fprintf oc "	add	%a, %a, %a\n" xreg rd xreg r1 symbol_offset_low (id, ofs)
    (* Bit-field operations *)
    | Psbfiz(sz, rd, r1, r, s) ->
        fprintf oc "	sbfiz	%a, %a, %a, %d\n" ireg (sz, rd) ireg (sz, r1) coqint r (Z.to_int s)
    | Psbfx(sz, rd, r1, r, s) ->
        fprintf oc "	sbfx	%a, %a, %a, %d\n" ireg (sz, rd) ireg (sz, r1) coqint r (Z.to_int s)
    | Pubfiz(sz, rd, r1, r, s) ->
        fprintf oc "	ubfiz	%a, %a, %a, %d\n" ireg (sz, rd) ireg (sz, r1) coqint r (Z.to_int s)
    | Pubfx(sz, rd, r1, r, s) ->
        fprintf oc "	ubfx	%a, %a, %a, %d\n" ireg (sz, rd) ireg (sz, r1) coqint r (Z.to_int s)
    (* Integer arithmetic, shifted register *)
    | Padd(sz, rd, r1, r2, s) ->
        fprintf oc "	add	%a, %a, %a%a\n" ireg (sz, rd) ireg0 (sz, r1) ireg (sz, r2) shiftop s
    | Psub(sz, rd, r1, r2, s) ->
        fprintf oc "	sub	%a, %a, %a%a\n" ireg (sz, rd) ireg0 (sz, r1) ireg (sz, r2) shiftop s
    | Pcmp(sz, r1, r2, s) ->
        fprintf oc "	cmp	%a, %a%a\n" ireg0 (sz, r1) ireg (sz, r2) shiftop s
    | Pcmn(sz, r1, r2, s) ->
        fprintf oc "	cmn	%a, %a%a\n" ireg0 (sz, r1) ireg (sz, r2) shiftop s
    (* Integer arithmetic, extending register *)
    | Paddext(rd, r1, r2, x) ->
        fprintf oc "	add	%a, %a, %a\n" xregsp rd xregsp r1 regextend (r2, x)
    | Psubext(rd, r1, r2, x) ->
        fprintf oc "	sub	%a, %a, %a\n" xregsp rd xregsp r1 regextend (r2, x)
    | Pcmpext(r1, r2, x) ->
        fprintf oc "	cmp	%a, %a\n" xreg r1 regextend (r2, x)
    | Pcmnext(r1, r2, x) ->
        fprintf oc "	cmn	%a, %a\n" xreg r1 regextend (r2, x)
    (* Logical, shifted register *)
    | Pand(sz, rd, r1, r2, s) ->
        fprintf oc "	and	%a, %a, %a%a\n" ireg (sz, rd) ireg0 (sz, r1) ireg (sz, r2) shiftop s
    | Pbic(sz, rd, r1, r2, s) ->
        fprintf oc "	bic	%a, %a, %a%a\n" ireg (sz, rd) ireg0 (sz, r1) ireg (sz, r2) shiftop s
    | Peon(sz, rd, r1, r2, s) ->
        fprintf oc "	eon	%a, %a, %a%a\n" ireg (sz, rd) ireg0 (sz, r1) ireg (sz, r2) shiftop s
    | Peor(sz, rd, r1, r2, s) ->
        fprintf oc "	eor	%a, %a, %a%a\n" ireg (sz, rd) ireg0 (sz, r1) ireg (sz, r2) shiftop s
    | Porr(sz, rd, r1, r2, s) ->
        fprintf oc "	orr	%a, %a, %a%a\n" ireg (sz, rd) ireg0 (sz, r1) ireg (sz, r2) shiftop s
    | Porn(sz, rd, r1, r2, s) ->
        fprintf oc "	orn	%a, %a, %a%a\n" ireg (sz, rd) ireg0 (sz, r1) ireg (sz, r2) shiftop s
    | Ptst(sz, r1, r2, s) ->
        fprintf oc "	tst	%a, %a%a\n" ireg0 (sz, r1) ireg (sz, r2) shiftop s
    (* Variable shifts *)
    | Pasrv(sz, rd, r1, r2) ->
        fprintf oc "	asr	%a, %a, %a\n" ireg (sz, rd) ireg (sz, r1) ireg (sz, r2)
    | Plslv(sz, rd, r1, r2) ->
        fprintf oc "	lsl	%a, %a, %a\n" ireg (sz, rd) ireg (sz, r1) ireg (sz, r2)
    | Plsrv(sz, rd, r1, r2) ->
        fprintf oc "	lsr	%a, %a, %a\n" ireg (sz, rd) ireg (sz, r1) ireg (sz, r2)
    | Prorv(sz, rd, r1, r2) ->
        fprintf oc "	ror	%a, %a, %a\n" ireg (sz, rd) ireg (sz, r1) ireg (sz, r2)
    (* Bit operations *)
    | Pcls(sz, rd, r1) ->
        fprintf oc "	cls	%a, %a\n" ireg (sz, rd) ireg (sz, r1)
    | Pclz(sz, rd, r1) ->
        fprintf oc "	clz	%a, %a\n" ireg (sz, rd) ireg (sz, r1)
    | Prev(sz, rd, r1) ->
        fprintf oc "	rev	%a, %a\n" ireg (sz, rd) ireg (sz, r1)
    | Prev16(sz, rd, r1) ->
        fprintf oc "	rev16	%a, %a\n" ireg (sz, rd) ireg (sz, r1)
    | Prbit(sz, rd, r1) ->
        fprintf oc "	rbit	%a, %a\n" ireg (sz, rd) ireg (sz, r1)
    (* Conditional data processing *)
    | Pcsel(rd, r1, r2, c) ->
        fprintf oc "	csel	%a, %a, %a, %s\n" xreg rd xreg r1 xreg r2 (condition_name c)
    | Pcset(rd, c) ->
        fprintf oc "	cset	%a, %s\n" xreg rd (condition_name c)
    (* Integer multiply/divide *)
    | Pmadd(sz, rd, r1, r2, r3) ->
        fprintf oc "	madd	%a, %a, %a, %a\n" ireg (sz, rd) ireg (sz, r1) ireg (sz, r2) ireg0 (sz, r3)
    | Pmsub(sz, rd, r1, r2, r3) ->
        fprintf oc "	msub	%a, %a, %a, %a\n" ireg (sz, rd) ireg (sz, r1) ireg (sz, r2) ireg0 (sz, r3)
    | Psmulh(rd, r1, r2) ->
        fprintf oc "	smulh	%a, %a, %a\n" xreg rd xreg r1 xreg r2
    | Pumulh(rd, r1, r2) ->
        fprintf oc "	umulh	%a, %a, %a\n" xreg rd xreg r1 xreg r2
    | Psdiv(sz, rd, r1, r2) ->
        fprintf oc "	sdiv	%a, %a, %a\n" ireg (sz, rd) ireg (sz, r1) ireg (sz, r2)
    | Pudiv(sz, rd, r1, r2) ->
        fprintf oc "	udiv	%a, %a, %a\n" ireg (sz, rd) ireg (sz, r1) ireg (sz, r2)
    (* Floating-point loads and stores *)
    | Pldrs(rd, a) ->
        fprintf oc "	ldr	%a, %a\n" sreg rd addressing a
    | Pldrd(rd, a) | Pldrd_a(rd, a) ->
        fprintf oc "	ldr	%a, %a\n" dreg rd addressing a
    | Pstrs(rd, a) ->
        fprintf oc "	str	%a, %a\n" sreg rd addressing a
    | Pstrd(rd, a) | Pstrd_a(rd, a) ->
        fprintf oc "	str	%a, %a\n" dreg rd addressing a
    | Pldps(rd1, rd2, _, _, a) ->
        fprintf oc "	ldp	%a, %a, %a\n" sreg rd1 sreg rd2 addressing a
    | Pldpd(rd1, rd2, _, _, a) ->
        fprintf oc "	ldp	%a, %a, %a\n" dreg rd1 dreg rd2 addressing a
    | Pstps(rd1, rd2, _, _, a) ->
        fprintf oc "	stp	%a, %a, %a\n" sreg rd1 sreg rd2 addressing a
    | Pstpd(rd1, rd2, _, _, a) ->
        fprintf oc "	stp	%a, %a, %a\n" dreg rd1 dreg rd2 addressing a
    (* Floating-point move *)
    | Pfmov(rd, r1) ->
        fprintf oc "	fmov	%a, %a\n" dreg rd dreg r1
    | Pfmovimmd(rd, f) ->
        let d = camlint64_of_coqint (Floats.Float.to_bits f) in
        if is_immediate_float64 f then
          fprintf oc "	fmov	%a, #%.7f\n" dreg rd (Int64.float_of_bits d)
        else begin
          let lbl = label_literal64 d in
          fprintf oc "	adrp	x16, %a\n" label_high lbl;
          fprintf oc "	ldr	%a, [x16, %a] %s %.18g\n" dreg rd label_low lbl comment (Int64.float_of_bits d)
        end
    | Pfmovimms(rd, f) ->
        let d = camlint_of_coqint (Floats.Float32.to_bits f) in
        if is_immediate_float32 f then
          fprintf oc "	fmov	%a, #%.7f\n" sreg rd (Int32.float_of_bits d)
        else begin
          let lbl = label_literal32 d in
          fprintf oc "	adrp	x16, %a\n" label_high lbl;
          fprintf oc "	ldr	%a, [x16, %a] %s %.18g\n" sreg rd label_low lbl comment (Int32.float_of_bits d)
        end
    | Pfmovi(D, rd, r1) ->
        fprintf oc "	fmov	%a, %a\n" dreg rd xreg0 r1
    | Pfmovi(S, rd, r1) ->
        fprintf oc "	fmov	%a, %a\n" sreg rd wreg0 r1
    (* Floating-point conversions *)
    | Pfcvtds(rd, r1) ->
        fprintf oc "	fcvt	%a, %a\n" dreg rd sreg r1 
    | Pfcvtsd(rd, r1) ->
        fprintf oc "	fcvt	%a, %a\n" sreg rd dreg r1 
    | Pfcvtzs(isz, fsz, rd, r1) ->
        fprintf oc "	fcvtzs  %a, %a\n" ireg (isz, rd) freg (fsz, r1)
    | Pfcvtzu(isz, fsz, rd, r1) ->
        fprintf oc "	fcvtzu  %a, %a\n" ireg (isz, rd) freg (fsz, r1)
    | Pscvtf(fsz, isz, rd, r1) ->
        fprintf oc "	scvtf	%a, %a\n" freg (fsz, rd) ireg (isz, r1)
    | Pucvtf(fsz, isz, rd, r1) ->
        fprintf oc "	ucvtf	%a, %a\n" freg (fsz, rd) ireg (isz, r1)
    (* Floating-point arithmetic *)
    | Pfabs(sz, rd, r1) ->
        fprintf oc "	fabs	%a, %a\n" freg (sz, rd) freg (sz, r1)
    | Pfneg(sz, rd, r1) ->
        fprintf oc "	fneg	%a, %a\n" freg (sz, rd) freg (sz, r1)
    | Pfsqrt(sz, rd, r1) ->
        fprintf oc "	fsqrt	%a, %a\n" freg (sz, rd) freg (sz, r1)
    | Pfadd(sz, rd, r1, r2) ->
        fprintf oc "	fadd	%a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2)
    | Pfdiv(sz, rd, r1, r2) ->
        fprintf oc "	fdiv	%a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2)
    | Pfmul(sz, rd, r1, r2) ->
        fprintf oc "	fmul	%a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2)
    | Pfnmul(sz, rd, r1, r2) ->
        fprintf oc "	fnmul	%a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2)
    | Pfsub(sz, rd, r1, r2) ->
        fprintf oc "	fsub	%a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2)
    | Pfmadd(sz, rd, r1, r2, r3) ->
        fprintf oc "	fmadd	%a, %a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2) freg (sz, r3)
    | Pfmsub(sz, rd, r1, r2, r3) ->
        fprintf oc "	fmsub	%a, %a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2) freg (sz, r3)
    | Pfnmadd(sz, rd, r1, r2, r3) ->
        fprintf oc "	fnmadd	%a, %a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2) freg (sz, r3)
    | Pfnmsub(sz, rd, r1, r2, r3) ->
        fprintf oc "	fnmsub	%a, %a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2) freg (sz, r3)
    | Pfmax (sz, rd, r1, r2) ->
        fprintf oc "	fmax	%a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2)
    | Pfmin (sz, rd, r1, r2) ->
        fprintf oc "	fmin	%a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2)
    (* Floating-point comparison *)
    | Pfcmp(sz, r1, r2) ->
        fprintf oc "	fcmp	%a, %a\n" freg (sz, r1) freg (sz, r2)
    | Pfcmp0(sz, r1) ->
        fprintf oc "	fcmp	%a, #0.0\n" freg (sz, r1)
    (* Floating-point conditional select *)
    | Pfsel(rd, r1, r2, c) ->
        fprintf oc "	fcsel	%a, %a, %a, %s\n" dreg rd dreg r1 dreg r2 (condition_name c)
    (* No-op *)
    | Pnop -> ()
        (*fprintf oc "	nop\n"*)
    (* Pseudo-instructions expanded in Asmexpand *)
    | Pallocframe(sz, linkofs) -> assert false
    | Pfreeframe(sz, linkofs) -> assert false
    | Pcvtx2w rd -> assert false
    (* Pseudo-instructions not yet expanded *)
    | Plabel lbl ->
        fprintf oc "%a:\n" print_label lbl
    | Ploadsymbol(rd, id) ->
        load_symbol_address oc rd id
    | Pcvtsw2x(rd, r1) ->
        fprintf oc "	sxtw	%a, %a\n" xreg rd wreg r1
    | Pcvtuw2x(rd, r1) ->
        fprintf oc "	uxtw	%a, %a\n" xreg rd wreg r1
    | Pbtbl(r1, tbl) ->
        let lbl = new_label() in
        fprintf oc "	adr	x16, %a\n" label lbl;
        fprintf oc "	add	x16, x16, %a, uxtw #2\n" wreg r1;
        fprintf oc "	br	x16\n";
        fprintf oc "%a:" label lbl;
        List.iter (fun l -> fprintf oc "	b	%a\n" print_label l) tbl
    | Pcfi_adjust sz ->
        cfi_adjust oc (camlint_of_coqint sz)
    | Pcfi_rel_offset ofs ->
        cfi_rel_offset oc "lr" (camlint_of_coqint ofs)
    | Pbuiltin(ef, args, res) ->
        begin match ef with
          | EF_annot(kind,txt, targs) ->
            begin match (P.to_int kind) with
              | 1 -> let annot = annot_text preg_annot "sp" (camlstring_of_coqstring txt) args  in
                fprintf oc "%s annotation: %S\n" comment annot
              | 2 -> let lbl = new_label () in
                fprintf oc "%a:\n" label lbl;
                add_ais_annot lbl preg_annot "sp" (camlstring_of_coqstring txt) args
              | _ -> assert false
            end
         | EF_debug(kind, txt, targs) ->
             print_debug_info comment print_file_line preg_annot "sp" oc
                              (P.to_int kind) (extern_atom txt) args
         | EF_inline_asm(txt, sg, clob) ->
             fprintf oc "%s begin inline assembly\n\t" comment;
             print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
             fprintf oc "%s end inline assembly\n" comment
         | EF_profiling (id, coq_kind) ->
            print_profiling_logger oc id (Z.to_int coq_kind)
         | _ ->
             assert false
        end

    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 oc jmptbl =
      let print_tbl oc (lbl, tbl) =
        fprintf oc "%a:\n" label lbl;
        List.iter
          (fun l -> fprintf oc "	.long	%a - %a\n"
                               print_label l label lbl)
          tbl in
      if !jumptables <> [] then
        begin
          section oc jmptbl;
          fprintf oc "	.balign 4\n";
          List.iter (print_tbl oc) !jumptables;
          jumptables := []
        end

    let print_optional_fun_info _ = ()

    let print_comm_symb oc sz name align =
      if C2C.atom_is_static name
      then print_lcomm_decl oc name sz align
      else print_comm_decl oc name sz align

    let print_instructions oc fn =
      current_function_sig := fn.fn_sig;
      List.iter (print_instruction oc) fn.fn_code

(* Data *)

    let address = ".quad"

    let print_prologue oc =
      if !Clflags.option_g then begin
        section oc Section_text;
      end

    let aarch64_profiling_stub oc nr_items
          profiling_id_table_name
          profiling_counter_table_name =
	fprintf oc "	adrp	x2, %s\n" profiling_counter_table_name;
	fprintf oc "	adrp	x1, %s\n" profiling_id_table_name;
	fprintf oc "	add	x2, x2, :lo12:%s\n" profiling_counter_table_name;
	fprintf oc "	add	x1, x1, :lo12:%s\n" profiling_id_table_name;
	fprintf oc "	mov	w0, %d\n" nr_items;
        fprintf oc "	b	%s\n" profiling_write_table_helper ;;

    let print_atexit oc to_be_called =
      	fprintf oc "	adrp	x0, %s\n" to_be_called;
	fprintf oc "	add	x0, x0, :lo12:%s\n" to_be_called;
	fprintf oc "	b	atexit\n";;
        

    let print_epilogue oc =
      print_profiling_epilogue elf_text_print_fun_info (Init_atexit print_atexit) aarch64_profiling_stub oc;
      if !Clflags.option_g then begin
        Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
        section oc Section_text;
      end

    let default_falignment = 4

    let cfi_startproc oc = ()
    let cfi_endproc oc = ()

  end

let sel_target () =
  let module S =
    (val (match Configuration.system with
          | "linux" -> (module ELF_System : SYSTEM)
          | "macos" -> (module MacOS_System : SYSTEM)
          | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported"))
     : SYSTEM) in
  (module Target(S) : TARGET)