(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           Léo Gourdin        UGA, VERIMAG                   *)
(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Cyril Six          Kalray                         *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

(** * Translation from Machblock to AArch64 assembly block language (Asmblock) 
    Inspired from the Mach->Asm pass of original Leroy's backend, but adapted to the block structure like the KVX backend. *)

Require Import Recdef Coqlib Zwf Zbits.
Require Import Errors AST Integers Floats Op.
Require Import Locations Machblock Asm Asmblock.

Local Open Scope string_scope.
Local Open Scope list_scope.
Local Open Scope error_monad_scope.

(** Extracting integer or float registers. *)

Definition ireg_of (r: mreg) : res ireg :=
  match preg_of r with
  |  IR irs => match irs with
                | RR1 mr => OK mr
                | _ => Error(msg "Asmgenblock.ireg_of")
                end
  | _ => Error(msg "Asmgenblock.iregsp_of")
  end.

Definition freg_of (r: mreg) : res freg :=
  match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end.

(** Recognition of immediate arguments for logical integer operations.*)

(** Valid immediate arguments are repetitions of a bit pattern [B]
  of length [e] = 2, 4, 8, 16, 32 or 64.
  The bit pattern [B] must be of the form [0*1*0*] or [1*0*1*]
  but must not be all zeros or all ones. *)

(** The following automaton recognizes [0*1*0*|1*0*1*].
<<
               0          1          0
              / \        / \        / \
              \ /        \ /        \ /
        -0--> [B] --1--> [D] --0--> [F]
       /
     [A]
       \
        -1--> [C] --0--> [E] --1--> [G]
              / \        / \        / \
              \ /        \ /        \ /
               1          0          1
>>
*)

Module Automaton.

Inductive state : Type := SA | SB | SC | SD | SE | SF | SG | Sbad.

Definition start := SA.

Definition next (s: state) (b: bool) :=
  match s, b with
    | SA,false => SB      | SA,true => SC
    | SB,false => SB      | SB,true => SD
    | SC,false => SE      | SC,true => SC
    | SD,false => SF      | SD,true => SD
    | SE,false => SE      | SE,true => SG
    | SF,false => SF      | SF,true => Sbad
    | SG,false => Sbad    | SG,true => SG
    | Sbad,_ => Sbad
  end.

Definition accepting (s: state) :=
  match s with
  | SA | SB | SC | SD | SE | SF | SG => true
  | Sbad => false
  end.

Fixpoint run (len: nat) (s: state) (x: Z) : bool :=
  match len with
  | Datatypes.O => accepting s
  | Datatypes.S len => run len (next s (Z.odd x)) (Z.div2 x)
  end.

End Automaton.

(** The following function determines the candidate length [e],
    ensuring that [x] is a repetition [BB...B] 
    of a bit pattern [B] of length [e]. *)

Definition logical_imm_length (x: Z) (sixtyfour: bool) : nat :=
  (** [test n] checks that the low [2n] bits of [x] are of the
      form [BB], that is, two occurrences of the same [n] bits *)
  let test (n: Z) : bool :=
    Z.eqb (Zzero_ext n x) (Zzero_ext n (Z.shiftr x n)) in
  (** If [test n] fails, we know that the candidate length [e] is
      at least [2n].  Hence we test with decreasing values of [n]:
      32, 16, 8, 4, 2. *)
  if sixtyfour && negb (test 32) then 64%nat
  else if negb (test 16) then 32%nat
  else if negb (test 8) then 16%nat
  else if negb (test 4) then 8%nat
  else if negb (test 2) then 4%nat
  else 2%nat.

(** A valid logical immediate is 
- neither [0] nor [-1];
- composed of a repetition [BBBBB] of a bit-pattern [B] of length [e]
- the low [e] bits of the number, that is, [B], match [0*1*0*] or [1*0*1*].
*)

Definition is_logical_imm32 (x: int) : bool :=
  negb (Int.eq x Int.zero) && negb (Int.eq x Int.mone) &&
  Automaton.run (logical_imm_length (Int.unsigned x) false)
                Automaton.start (Int.unsigned x).

Definition is_logical_imm64 (x: int64) : bool :=
  negb (Int64.eq x Int64.zero) && negb (Int64.eq x Int64.mone) &&
  Automaton.run (logical_imm_length (Int64.unsigned x) true)
                Automaton.start (Int64.unsigned x).

(** Arithmetic immediates are 12-bit unsigned numbers, possibly shifted left 12 bits *)

Definition is_arith_imm32 (x: int) : bool :=
  Int.eq x (Int.zero_ext 12 x)
  || Int.eq x (Int.shl (Int.zero_ext 12 (Int.shru x (Int.repr 12))) (Int.repr 12)).

Definition is_arith_imm64 (x: int64) : bool :=
  Int64.eq x (Int64.zero_ext 12 x)
  || Int64.eq x (Int64.shl (Int64.zero_ext 12 (Int64.shru x (Int64.repr 12))) (Int64.repr 12)).

Definition bcode := list basic.

Program Definition single_basic (bi: basic): bblock :=
  {| header := nil; body:= bi::nil; exit := None |}.

(* insert [bi] at the head of [k] *)
Program Definition insert_basic (bi: basic) (k:bblocks): bblocks :=
  match k with
  | bb::k' =>
    match bb.(header) with
    | nil => {| header := nil; body := bi :: (body bb); exit := exit bb |}::k'
    | _ => (single_basic bi)::k
    end
  | _ => (single_basic bi)::k
  end.

Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity).

(* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *)
(** Alignment check for symbols *)
Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity).
Notation "a @@ b" := (app a b) (at level 49, right associativity).

(* The pop_bc and push_bc functions are used to adapt the output of some definitions
   in bblocks format and avoid some redefinitions. *)

(* pop_bc takes the body of the first bblock in the list if it does not have a header. *)
Definition pop_bc (k: bblocks): bcode :=
  match k with
  | bb :: k' => match bb.(header) with
                | nil => (body bb)
                | _ => nil
                end
  | _ => nil
  end.

(* push_bc tries to overwrite code in the first bblock if it does not have a header,
   otherwise, a new bblock is created and appended to the list. *)
Program Definition push_bc (bc: bcode) (k:bblocks): bblocks :=
  match bc with
  | bi :: bc' => match k with
                 | bb :: k' => match bb.(header) with
                               | nil => {| header := nil; body := bc; exit := exit bb |} :: k'
                               | _ => {| header := nil; body := bc; exit := None |} :: k
                               end
                 | _ => {| header := nil; body := bc; exit := None |} :: nil
                 end
  | nil => k
  end.
Next Obligation.
  simpl; auto.
Qed.
Next Obligation.
  simpl; auto.
Qed.
Next Obligation.
  simpl; auto.
Qed.

Parameter symbol_is_aligned : ident -> Z -> bool.
(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *)

(***************************************************************************************)

(** Decompose integer literals into 16-bit fragments *)

Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) :=
  match N with
  | Datatypes.O => nil
  | Datatypes.S N =>
    let frag := Zzero_ext 16 (Z.shiftr n p) in
    if Z.eqb frag 0 then
      decompose_int N n (p + 16)
    else
      (frag, p) :: decompose_int N (Z.ldiff n (Z.shiftl 65535 p)) (p + 16)
  end.

Definition negate_decomposition (l: list (Z * Z)) :=
  List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l.

Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode :=
    List.fold_right (fun np k => Pmovk sz (fst np) (snd np) rd rd ::bi k) k l.

Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z))  (k: bcode) : bcode :=
  match l with
  | nil => Pmovz sz 0 0 rd ::bi k
  | (n1, p1) :: l => (Pmovz sz n1 p1 rd) ::bi loadimm_k sz rd l k
  end.

Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode :=
  match l with
  | nil => Pmovn sz 0 0 rd ::bi k
  | (n1, p1) :: l => Pmovn sz n1 p1 rd ::bi loadimm_k sz rd (negate_decomposition l) k
  end.

Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: bcode) : bcode :=
  let N := match sz with W => 2%nat | X => 4%nat end in
  let dz := decompose_int N n 0 in
  let dn := decompose_int N (Z.lnot n) 0 in
  if Nat.leb (List.length dz) (List.length dn)
  then loadimm_z sz rd dz k
  else loadimm_n sz rd dn k.

Definition loadimm32 (rd: ireg) (n: int) (k: bcode) : bcode :=
  if is_logical_imm32 n
  then Porrimm W (Int.unsigned n) rd XZR ::bi k
  else loadimm W rd (Int.unsigned n) k.

Definition loadimm64 (rd: ireg) (n: int64) (k: bcode) : bcode :=
  if is_logical_imm64 n
  then Porrimm X (Int64.unsigned n) rd XZR ::bi k
  else loadimm X rd (Int64.unsigned n) k.

Definition offset_representable (sz: Z) (ofs: int64) : bool :=
  let isz := Int64.repr sz in
  (** either unscaled 9-bit signed *)
  Int64.eq ofs (Int64.sign_ext 9 ofs) ||
  (** or scaled 12-bit unsigned *)
  (Int64.eq (Int64.modu ofs isz) Int64.zero
   && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).

Definition indexed_memory_access_bc (insn: addressing -> basic)
                                 (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bcode) : bcode :=
  let ofs := Ptrofs.to_int64 ofs in
  if offset_representable sz ofs
  then insn (ADimm base ofs) :: k
  else loadimm64 X16 ofs (insn (ADreg base X16) :: k).

Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
  match ty, preg_of dst with
  | Tint,    IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrw rd) 4 base ofs k)
  | Tlong,   IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrx rd) 8 base ofs k)
  | Tsingle, FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrs rd) 4 base ofs k)
  | Tfloat,  FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrd rd) 8 base ofs k)
  | Tany32,  IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrw_a rd) 4 base ofs k)
  | Tany64,  IR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrx_a rd) 8 base ofs k)
  | Tany64,  FR rd => OK (indexed_memory_access_bc (PLd_rd_a Pldrd_a rd) 8 base ofs k)
  | _, _           => Error (msg "Asmgen.loadind")
  end.

Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode) :=
  match ty, preg_of src with
  | Tint,    IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrw rd) 4 base ofs k)
  | Tlong,   IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrx rd) 8 base ofs k)
  | Tsingle, FR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrs rd) 4 base ofs k)
  | Tfloat,  FR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrd rd) 8 base ofs k)
  | Tany32,  IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrw_a rd) 4 base ofs k)
  | Tany64,  IR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrx_a rd) 8 base ofs k)
  | Tany64,  FR rd => OK (indexed_memory_access_bc (PSt_rs_a Pstrd_a rd) 8 base ofs k)
  | _, _           => Error (msg "Asmgen.storeind")
  end.

Definition loadptr_bc (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bcode): bcode :=
  indexed_memory_access_bc (PLd_rd_a Pldrx dst) 8 base ofs k. 

Definition storeptr_bc (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bcode): bcode :=
  indexed_memory_access_bc (PSt_rs_a Pstrx src) 8 base ofs k.

(** Function epilogue *)

Definition make_epilogue (f: Machblock.function) : bcode :=
  loadptr_bc XSP f.(fn_retaddr_ofs) RA
  (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs)::nil).

(** Add immediate *)

Definition addimm_aux (insn: Z -> arith_pp)
                        (rd r1: iregsp) (n: Z) (k: bcode) :=
  let nlo := Zzero_ext 12 n in
  let nhi := n - nlo in
  if Z.eqb nhi 0 then
    insn nlo rd r1 ::bi k
  else if Z.eqb nlo 0 then
    insn nhi rd r1 ::bi k
  else
    insn nhi rd r1 ::bi insn nlo rd rd ::bi k.

Definition addimm32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
  let m := Int.neg n in
  if Int.eq n (Int.zero_ext 24 n) then
    addimm_aux (Paddimm W) rd r1 (Int.unsigned n) k
  else if Int.eq m (Int.zero_ext 24 m) then
    addimm_aux (Psubimm W) rd r1 (Int.unsigned m) k
  else if Int.lt n Int.zero then
    loadimm32 X16 m (Psub W SOnone rd r1 X16 ::bi k)
  else
    loadimm32 X16 n (Padd W SOnone rd r1 X16 ::bi k).

Definition addimm64 (rd r1: iregsp) (n: int64) (k: bcode) : bcode :=
  let m := Int64.neg n in
  if Int64.eq n (Int64.zero_ext 24 n) then
    addimm_aux (Paddimm X) rd r1 (Int64.unsigned n) k
  else if Int64.eq m (Int64.zero_ext 24 m) then
    addimm_aux (Psubimm X) rd r1 (Int64.unsigned m) k
  else if Int64.lt n Int64.zero then
    loadimm64 X16 m (Psubext (EOuxtx Int.zero) rd r1 X16 ::bi k)
  else
    loadimm64 X16 n (Paddext (EOuxtx Int.zero) rd r1 X16 ::bi k).

(** Logical immediate *)

Definition logicalimm32
              (insn1: Z -> arith_rr0)
              (insn2: shift_op -> arith_rr0r)
              (rd r1: ireg) (n: int) (k: bcode) : bcode :=
  if is_logical_imm32 n
  then insn1 (Int.unsigned n) rd r1 ::bi k
  else loadimm32 X16 n (insn2 SOnone rd r1 X16 ::bi k).

Definition logicalimm64
              (insn1: Z -> arith_rr0)
              (insn2: shift_op -> arith_rr0r)
              (rd r1: ireg) (n: int64) (k: bcode) : bcode :=
  if is_logical_imm64 n
  then insn1 (Int64.unsigned n) rd r1 ::bi k
  else loadimm64 X16 n (insn2 SOnone rd r1 X16 ::bi k).

(** Sign- or zero-extended arithmetic *)

Definition transl_extension (ex: extension) (a: int) : extend_op :=
  match ex with Xsgn32 => EOsxtw a | Xuns32 => EOuxtw a end.

Definition move_extended_base
              (rd: ireg) (r1: ireg) (ex: extension) (k: bcode) : bcode :=
  match ex with
  | Xsgn32 => Pcvtsw2x rd r1 ::bi k
  | Xuns32 => Pcvtuw2x rd r1 ::bi k
  end.

Definition move_extended
              (rd: ireg) (r1: ireg) (ex: extension) (a: int) (k: bcode) : bcode :=
  if Int.eq a Int.zero then
    move_extended_base rd r1 ex k
  else
    move_extended_base rd r1 ex (Padd X (SOlsl a) rd XZR rd ::bi k).

Definition arith_extended 
              (insnX: extend_op -> arith_ppp)
              (insnS: shift_op -> arith_rr0r)
              (rd r1 r2: ireg) (ex: extension) (a: int) (k: bcode) : bcode :=
  if Int.ltu a (Int.repr 5) then
    insnX (transl_extension ex a) rd r1 r2 ::bi k
  else
    move_extended_base X16 r2 ex (insnS (SOlsl a) rd r1 X16 ::bi k).

(** Extended right shift *)

Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
  if Int.eq n Int.zero then
    Pmov rd r1 ::bi k
  else
    Porr W (SOasr (Int.repr 31)) X16 XZR r1 ::bi
    Padd W (SOlsr (Int.sub Int.iwordsize n)) X16 r1 X16 ::bi
    Porr W (SOasr n) rd XZR X16 ::bi k.

Definition shrx64 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
  if Int.eq n Int.zero then
    Pmov rd r1 ::bi k
  else
    Porr X (SOasr (Int.repr 63)) X16 XZR r1 ::bi
    Padd X (SOlsr (Int.sub Int64.iwordsize' n)) X16 r1 X16 ::bi
    Porr X (SOasr n) rd XZR X16 ::bi k.

(** Load the address [id + ofs] in [rd] *)

Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: bcode) : bcode :=
  if Archi.pic_code tt then
    if Ptrofs.eq ofs Ptrofs.zero then
      Ploadsymbol rd id ::bi k
    else
      Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k
  else
    Padrp id ofs rd ::bi Paddadr id ofs rd rd ::bi k.

(** Translate a shifted operand *)

Definition transl_shift (s: Op.shift) (a: int): Asm.shift_op :=
  match s with
  | Slsl => SOlsl a
  | Slsr => SOlsr a
  | Sasr => SOasr a
  | Sror => SOror a
  end.

(** Translation of a condition.  Prepends to [k] the instructions
  that evaluate the condition and leave its boolean result in one of
  the bits of the condition register.  The bit in question is
  determined by the [crbit_for_cond] function. *)

Definition transl_cond
              (cond: condition) (args: list mreg) (k: bcode) :=
  match cond, args with
  | (Ccomp c | Ccompu c), a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pcmp W SOnone r1 r2 ::bi k)
  | (Ccompshift c s a | Ccompushift c s a), a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pcmp W (transl_shift s a) r1 r2 ::bi k)
  | (Ccompimm c n | Ccompuimm c n), a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (if is_arith_imm32 n then
            Pcmpimm W (Int.unsigned n) r1 ::bi k
          else if is_arith_imm32 (Int.neg n) then
            Pcmnimm W (Int.unsigned (Int.neg n)) r1 ::bi k
          else
            loadimm32 X16 n (Pcmp W SOnone r1 X16 ::bi k))
  | (Cmaskzero n | Cmasknotzero n), a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (if is_logical_imm32 n then
            Ptstimm W (Int.unsigned n) r1 ::bi k
          else
            loadimm32 X16 n (Ptst W SOnone r1 X16 ::bi k))
  | (Ccompl c | Ccomplu c), a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pcmp X SOnone r1 r2 ::bi k)
  | (Ccomplshift c s a | Ccomplushift c s a), a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pcmp X (transl_shift s a) r1 r2 ::bi k)
  | (Ccomplimm c n | Ccompluimm c n), a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (if is_arith_imm64 n then
            Pcmpimm X (Int64.unsigned n) r1 ::bi k
          else if is_arith_imm64 (Int64.neg n) then
            Pcmnimm X (Int64.unsigned (Int64.neg n)) r1 ::bi k
          else
            loadimm64 X16 n (Pcmp X SOnone r1 X16 ::bi k))
  | (Cmasklzero n | Cmasklnotzero n), a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (if is_logical_imm64 n then
            Ptstimm X (Int64.unsigned n) r1 ::bi k
          else
            loadimm64 X16 n (Ptst X SOnone r1 X16 ::bi k))
  | Ccompf cmp, a1 :: a2 :: nil =>
      do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfcmp D r1 r2 ::bi k)
  | Cnotcompf cmp, a1 :: a2 :: nil =>
      do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfcmp D r1 r2 ::bi k)
  | Ccompfzero cmp, a1 :: nil =>
      do r1 <- freg_of a1;
      OK (Pfcmp0 D r1 ::bi k)
  | Cnotcompfzero cmp, a1 :: nil =>
      do r1 <- freg_of a1;
      OK (Pfcmp0 D r1 ::bi k)
  | Ccompfs cmp, a1 :: a2 :: nil =>
      do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfcmp S r1 r2 ::bi k)
  | Cnotcompfs cmp, a1 :: a2 :: nil =>
      do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfcmp S r1 r2 ::bi k)
  | Ccompfszero cmp, a1 :: nil =>
      do r1 <- freg_of a1;
      OK (Pfcmp0 S r1 ::bi k)
  | Cnotcompfszero cmp, a1 :: nil =>
      do r1 <- freg_of a1;
      OK (Pfcmp0 S r1 ::bi k)
  | _, _ =>
      Error(msg "Asmgenblock.transl_cond")
  end.

Definition cond_for_signed_cmp (cmp: comparison) :=
  match cmp with
  | Ceq => TCeq
  | Cne => TCne
  | Clt => TClt
  | Cle => TCle
  | Cgt => TCgt
  | Cge => TCge
  end.

Definition cond_for_unsigned_cmp (cmp: comparison) :=
  match cmp with
  | Ceq => TCeq
  | Cne => TCne
  | Clt => TClo
  | Cle => TCls
  | Cgt => TChi
  | Cge => TChs
  end.

Definition cond_for_float_cmp (cmp: comparison) :=
  match cmp with
  | Ceq => TCeq
  | Cne => TCne
  | Clt => TCmi
  | Cle => TCls
  | Cgt => TCgt
  | Cge => TCge
  end.

Definition cond_for_float_not_cmp (cmp: comparison) :=
  match cmp with
  | Ceq => TCne
  | Cne => TCeq
  | Clt => TCpl
  | Cle => TChi
  | Cgt => TCle
  | Cge => TClt
  end.

Definition cond_for_cond (cond: condition) :=
  match cond with
  | Ccomp cmp => cond_for_signed_cmp cmp
  | Ccompu cmp => cond_for_unsigned_cmp cmp
  | Ccompshift cmp s a => cond_for_signed_cmp cmp
  | Ccompushift cmp s a => cond_for_unsigned_cmp cmp
  | Ccompimm cmp n => cond_for_signed_cmp cmp
  | Ccompuimm cmp n => cond_for_unsigned_cmp cmp
  | Cmaskzero n => TCeq
  | Cmasknotzero n => TCne
  | Ccompl cmp => cond_for_signed_cmp cmp
  | Ccomplu cmp => cond_for_unsigned_cmp cmp
  | Ccomplshift cmp s a => cond_for_signed_cmp cmp
  | Ccomplushift cmp s a => cond_for_unsigned_cmp cmp
  | Ccomplimm cmp n => cond_for_signed_cmp cmp
  | Ccompluimm cmp n => cond_for_unsigned_cmp cmp
  | Cmasklzero n => TCeq
  | Cmasklnotzero n => TCne
  | Ccompf cmp => cond_for_float_cmp cmp
  | Cnotcompf cmp => cond_for_float_not_cmp cmp
  | Ccompfzero cmp => cond_for_float_cmp cmp
  | Cnotcompfzero cmp => cond_for_float_not_cmp cmp
  | Ccompfs cmp => cond_for_float_cmp cmp
  | Cnotcompfs cmp => cond_for_float_not_cmp cmp
  | Ccompfszero cmp => cond_for_float_cmp cmp
  | Cnotcompfszero cmp => cond_for_float_not_cmp cmp
  end.

(** Translation of a conditional branch.  Prepends to [k] the instructions
  that evaluate the condition and ranch to [lbl] if it holds.
  We recognize some conditional branches that can be implemented
  without setting then testing condition flags.  *)

Definition transl_cond_branch_default
  (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*cf_instruction) :=
  do ccode <- transl_cond c args k;
  OK(ccode, Pbc (cond_for_cond c) lbl).
 
Definition transl_cond_branch
  (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*cf_instruction) :=
  match args, c with
  | a1 :: nil, (Ccompimm Cne n | Ccompuimm Cne n) =>
      if Int.eq n Int.zero
      then (do r1 <- ireg_of a1; OK (k, Pcbnz W r1 lbl))
      else transl_cond_branch_default c args lbl k
  | a1 :: nil, (Ccompimm Ceq n | Ccompuimm Ceq n) =>
      if Int.eq n Int.zero
      then (do r1 <- ireg_of a1; OK (k, Pcbz W r1 lbl))
      else transl_cond_branch_default c args lbl k
  | a1 :: nil, (Ccomplimm Cne n | Ccompluimm Cne n) =>
      if Int64.eq n Int64.zero
      then (do r1 <- ireg_of a1; OK (k, Pcbnz X r1 lbl))
      else transl_cond_branch_default c args lbl k
  | a1 :: nil, (Ccomplimm Ceq n | Ccompluimm Ceq n) =>
      if Int64.eq n Int64.zero
      then (do r1 <- ireg_of a1; OK (k, Pcbz X r1 lbl))
      else transl_cond_branch_default c args lbl k
  | a1 :: nil, Cmaskzero n =>
      match Int.is_power2 n with
      | Some bit => do r1 <- ireg_of a1; OK (k, Ptbz W r1 bit lbl)
      | None => transl_cond_branch_default c args lbl k
      end
  | a1 :: nil, Cmasknotzero n =>
      match Int.is_power2 n with
      | Some bit => do r1 <- ireg_of a1; OK (k, Ptbnz W r1 bit lbl)
      | None => transl_cond_branch_default c args lbl k
      end
  | a1 :: nil, Cmasklzero n =>
      match Int64.is_power2' n with
      | Some bit => do r1 <- ireg_of a1; OK (k, Ptbz X r1 bit lbl)
      | None => transl_cond_branch_default c args lbl k
      end
  | a1 :: nil, Cmasklnotzero n =>
      match Int64.is_power2' n with
      | Some bit => do r1 <- ireg_of a1; OK (k, Ptbnz X r1 bit lbl)
      | None => transl_cond_branch_default c args lbl k
      end
  | _, _ =>
      transl_cond_branch_default c args lbl k
  end.

(** Translation of the arithmetic operation [r <- op(args)].
  The corresponding instructions are prepended to [k]. *)

Definition transl_op
              (op: operation) (args: list mreg) (res: mreg) (k: bcode) :=
  match op, args with
  | Omove, a1 :: nil =>
      match preg_of res, preg_of a1 with
      | IR r, IR a => OK (Pmov r a ::bi k)
      | FR r, FR a => OK (Pfmov r a ::bi k)
      |  _  ,  _   => Error(msg "Asmgenblock.Omove")
      end
  | Ointconst n, nil =>
      do rd <- ireg_of res;
      OK (loadimm32 rd n k)
  | Olongconst n, nil =>
      do rd <- ireg_of res;
      OK (loadimm64 rd n k)
  | Ofloatconst f, nil =>
      do rd <- freg_of res;
      OK (if Float.eq_dec f Float.zero
          then Pfmovi D rd XZR ::bi k
          else Pfmovimmd f rd ::bi k)
  | Osingleconst f, nil =>
      do rd <- freg_of res;
      OK (if Float32.eq_dec f Float32.zero
          then Pfmovi S rd XZR ::bi k
          else Pfmovimms f rd ::bi k)
  | Oaddrsymbol id ofs, nil =>
      do rd <- ireg_of res;
      OK (loadsymbol rd id ofs k)
  | Oaddrstack ofs, nil =>
      do rd <- ireg_of res;
      OK (addimm64 rd XSP (Ptrofs.to_int64 ofs) k)
  (** 32-bit integer arithmetic *)
  | Oshift s a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Porr W (transl_shift s a) rd XZR r1 ::bi k)
  | Oadd, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Padd W SOnone rd r1 r2 ::bi k)
  | Oaddshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Padd W (transl_shift s a) rd r1 r2 ::bi k)
  | Oaddimm n, a1 :: nil =>
      do rd  <- ireg_of res; do rs <- ireg_of a1;
      OK (addimm32 rd rs n k)
  | Oneg, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psub W SOnone rd XZR r1 ::bi k)
  | Onegshift s a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psub W (transl_shift s a) rd XZR r1 ::bi k)
  | Osub, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Psub W SOnone rd r1 r2 ::bi k)
  | Osubshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Psub W (transl_shift s a) rd r1 r2 ::bi k)
  | Omul, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
      OK (Pmadd W rd rs1 rs2 XZR ::bi k)
  | Omuladd, a1 :: a2 :: a3 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
      OK (Pmadd W rd r2 r3 r1 ::bi k)
  | Omulsub, a1 :: a2 :: a3 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
      OK (Pmsub W rd r2 r3 r1 ::bi k)
  | Odiv, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Psdiv W rd r1 r2 ::bi k)
  | Odivu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pudiv W rd r1 r2 ::bi k)
  | Oand, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pand W SOnone rd r1 r2 ::bi k)
  | Oandshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pand W (transl_shift s a) rd r1 r2 ::bi k)
  | Oandimm n, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (logicalimm32 (Pandimm W) (Pand W) rd r1 n k)
  | Oor, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Porr W SOnone rd r1 r2 ::bi k)
  | Oorshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Porr W (transl_shift s a) rd r1 r2 ::bi k)
  | Oorimm n, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (logicalimm32 (Porrimm W) (Porr W) rd r1 n k)      
  | Oxor, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Peor W SOnone rd r1 r2 ::bi k)
  | Oxorshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Peor W (transl_shift s a) rd r1 r2 ::bi k)
  | Oxorimm n, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (logicalimm32 (Peorimm W) (Peor W) rd r1 n k)      
  | Onot, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Porn W SOnone rd XZR r1 ::bi k)
  | Onotshift s a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Porn W (transl_shift s a) rd XZR r1 ::bi k)
  | Obic, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pbic W SOnone rd r1 r2 ::bi k)
  | Obicshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pbic W (transl_shift s a) rd r1 r2 ::bi k)
  | Oorn, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Porn W SOnone rd r1 r2 ::bi k)
  | Oornshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Porn W (transl_shift s a) rd r1 r2 ::bi k)
  | Oeqv, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Peon W SOnone rd r1 r2 ::bi k)
  | Oeqvshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Peon W (transl_shift s a) rd r1 r2 ::bi k)
  | Oshl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Plslv W rd r1 r2 ::bi k)
  | Oshr, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pasrv W rd r1 r2 ::bi k)
  | Oshru, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Plsrv W rd r1 r2 ::bi k)
  | Oshrximm n, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (shrx32 rd r1 n k)
  | Ozext s, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Pubfiz W Int.zero s rd r1 ::bi k)
  | Osext s, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psbfiz W Int.zero s rd r1 ::bi k)
  | Oshlzext s a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Pubfiz W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k)
  | Oshlsext s a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psbfiz W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k)
  | Ozextshr a s, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Pubfx W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k)
  | Osextshr a s, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psbfx W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k)
  (** 64-bit integer arithmetic *)
  | Oshiftl s a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Porr X (transl_shift s a) rd XZR r1 ::bi k)
  | Oextend x a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (move_extended rd r1 x a k)
  (* [Omakelong] and [Ohighlong] should not occur *)
  | Olowlong, a1 :: nil => 
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      assertion (ireg_eq rd r1);
      OK (Pcvtx2w rd ::bi k)
  | Oaddl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Padd X SOnone rd r1 r2 ::bi k)
  | Oaddlshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Padd X (transl_shift s a) rd r1 r2 ::bi k)
  | Oaddlext x a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (arith_extended Paddext (Padd X) rd r1 r2 x a k)
  | Oaddlimm n, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (addimm64 rd r1 n k)
  | Onegl, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psub X SOnone rd XZR r1 ::bi k)
  | Oneglshift s a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psub X (transl_shift s a) rd XZR r1 ::bi k)
  | Osubl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Psub X SOnone rd r1 r2 ::bi k)
  | Osublshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Psub X (transl_shift s a) rd r1 r2 ::bi k)
  | Osublext x a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (arith_extended Psubext (Psub X) rd r1 r2 x a k)
  | Omull, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pmadd X rd r1 r2 XZR ::bi k)
  | Omulladd, a1 :: a2 :: a3 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
      OK (Pmadd X rd r2 r3 r1 ::bi k)
  | Omullsub, a1 :: a2 :: a3 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
      OK (Pmsub X rd r2 r3 r1 ::bi k)
  | Omullhs, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Psmulh rd r1 r2 ::bi k)
  | Omullhu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pumulh rd r1 r2 ::bi k)
  | Odivl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Psdiv X rd r1 r2 ::bi k)
  | Odivlu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pudiv X rd r1 r2 ::bi k)
  | Oandl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pand X SOnone rd r1 r2 ::bi k)
  | Oandlshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pand X (transl_shift s a) rd r1 r2 ::bi k)
  | Oandlimm n, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (logicalimm64 (Pandimm X) (Pand X) rd r1 n k)      
  | Oorl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Porr X SOnone rd r1 r2 ::bi k)
  | Oorlshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Porr X (transl_shift s a) rd r1 r2 ::bi k)
  | Oorlimm n, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (logicalimm64 (Porrimm X) (Porr X) rd r1 n k)      
  | Oxorl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Peor X SOnone rd r1 r2 ::bi k)
  | Oxorlshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Peor X (transl_shift s a) rd r1 r2 ::bi k)
  | Oxorlimm n, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (logicalimm64 (Peorimm X) (Peor X) rd r1 n k)      
  | Onotl, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Porn X SOnone rd XZR r1 ::bi k)
  | Onotlshift s a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Porn X (transl_shift s a) rd XZR r1 ::bi k)
  | Obicl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pbic X SOnone rd r1 r2 ::bi k)
  | Obiclshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pbic X (transl_shift s a) rd r1 r2 ::bi k)
  | Oornl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Porn X SOnone rd r1 r2 ::bi k)
  | Oornlshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Porn X (transl_shift s a) rd r1 r2 ::bi k)
  | Oeqvl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Peon X SOnone rd r1 r2 ::bi k)
  | Oeqvlshift s a, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Peon X (transl_shift s a) rd r1 r2 ::bi k)
  | Oshll, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Plslv X rd r1 r2 ::bi k)
  | Oshrl, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pasrv X rd r1 r2 ::bi k)
  | Oshrlu, a1 :: a2 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Plsrv X rd r1 r2 ::bi k)
  | Oshrlximm n, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (shrx64 rd r1 n k)
  | Ozextl s, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Pubfiz X Int.zero s rd r1 ::bi k)
  | Osextl s, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psbfiz X Int.zero s rd r1 ::bi k)
  | Oshllzext s a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Pubfiz X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k)
  | Oshllsext s a, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psbfiz X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k)
  | Ozextshrl a s, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Pubfx X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k)
  | Osextshrl a s, a1 :: nil =>
      do rd <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psbfx X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k)
  (** 64-bit floating-point arithmetic *)
  | Onegf, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfneg D rd rs ::bi k)
  | Oabsf, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfabs D rd rs ::bi k)
  | Oaddf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfadd D rd rs1 rs2 ::bi k)
  | Osubf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfsub D rd rs1 rs2 ::bi k)
  | Omulf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfmul D rd rs1 rs2 ::bi k)
  | Odivf, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfdiv D rd rs1 rs2 ::bi k)
  (** 32-bit floating-point arithmetic *)
  | Onegfs, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfneg S rd rs ::bi k)
  | Oabsfs, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfabs S rd rs ::bi k)
  | Oaddfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfadd S rd rs1 rs2 ::bi k)
  | Osubfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfsub S rd rs1 rs2 ::bi k)
  | Omulfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfmul S rd rs1 rs2 ::bi k)
  | Odivfs, a1 :: a2 :: nil =>
      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
      OK (Pfdiv S rd rs1 rs2 ::bi k)
  | Osingleoffloat, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfcvtsd rd rs ::bi k)
  | Ofloatofsingle, a1 :: nil =>
      do rd <- freg_of res; do rs <- freg_of a1;
      OK (Pfcvtds rd rs ::bi k)
  (** Conversions between int and float *)
  | Ointoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtzs W D rd rs ::bi k)
  | Ointuoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtzu W D rd rs ::bi k)
  | Ofloatofint, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pscvtf D W rd rs ::bi k)
  | Ofloatofintu, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pucvtf D W rd rs ::bi k)
  | Ointofsingle, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtzs W S rd rs ::bi k)
  | Ointuofsingle, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtzu W S rd rs ::bi k)
  | Osingleofint, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pscvtf S W rd rs ::bi k)
  | Osingleofintu, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pucvtf S W rd rs ::bi k)
  | Olongoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtzs X D rd rs ::bi k)
  | Olonguoffloat, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtzu X D rd rs ::bi k)
  | Ofloatoflong, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pscvtf D X rd rs ::bi k)
  | Ofloatoflongu, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pucvtf D X rd rs ::bi k)
  | Olongofsingle, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtzs X S rd rs ::bi k)
  | Olonguofsingle, a1 :: nil =>
      do rd <- ireg_of res; do rs <- freg_of a1;
      OK (Pfcvtzu X S rd rs ::bi k)
  | Osingleoflong, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pscvtf S X rd rs ::bi k)
  | Osingleoflongu, a1 :: nil =>
      do rd <- freg_of res; do rs <- ireg_of a1;
      OK (Pucvtf S X rd rs ::bi k)
  (** Boolean tests *)
  | Ocmp c, _ =>
      do rd <- ireg_of res;
      transl_cond c args (Pcset rd (cond_for_cond c) ::bi k)
  (** Conditional move *)
  | Osel cmp ty, a1 :: a2 :: args =>
      match preg_of res with
      | IR r => 
          do r1 <- ireg_of a1; do r2 <- ireg_of a2;
          transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) ::bi k)
      | FR r =>
          do r1 <- freg_of a1; do r2 <- freg_of a2;
          transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) ::bi k)
      | _ =>
          Error(msg "Asmgenblock.Osel")
      end
  | _, _ => Error(msg "Asmgenblock.transl_op")
  end.

(** Translation of addressing modes *)
 
Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
                             (insn: Asm.addressing -> basic) (k: bcode) : res bcode :=
  match addr, args with
  | Aindexed ofs, a1 :: nil =>
      do r1 <- ireg_of a1;
       if offset_representable sz ofs then
        OK (insn (ADimm r1 ofs) ::bi k)
      else
        OK (loadimm64 X16 ofs (insn (ADreg r1 X16) ::bi k))
  | Aindexed2, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (insn (ADreg r1 r2) ::bi k)
  | Aindexed2shift a, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      if Int.eq a Int.zero then
        OK (insn (ADreg r1 r2) ::bi k)
      else if Int.eq (Int.shl Int.one a) (Int.repr sz) then
        OK (insn (ADlsl r1 r2 a) ::bi k)
      else
        OK (Padd X (SOlsl a) X16 r1 r2 ::bi insn (ADimm X16 Int64.zero) ::bi k)
  | Aindexed2ext x a, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      if Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz) then
        OK (insn (match x with Xsgn32 => ADsxt r1 r2 a
                             | Xuns32 => ADuxt r1 r2 a end) ::bi k)
      else
        OK (arith_extended Paddext (Padd X) X16 r1 r2 x a
                           (insn (ADimm X16 Int64.zero) ::bi k))
  | Aglobal id ofs, nil =>
      assertion (negb (Archi.pic_code tt));
      if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz
      then OK (Padrp id ofs X16 ::bi insn (ADadr X16 id ofs) ::bi k)
      else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) ::bi k))
  | Ainstack ofs, nil =>
      let ofs := Ptrofs.to_int64 ofs in
      if offset_representable sz ofs then
        OK (insn (ADimm XSP ofs) ::bi k)
      else
        OK (loadimm64 X16 ofs (insn (ADreg XSP X16) ::bi k))
  | _, _ =>
      Error(msg "Asmgen.transl_addressing")
  end.

(** Translation of loads and stores *)

Definition transl_load (chunk: memory_chunk) (addr: Op.addressing)
                       (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
  match chunk with
  | Mint8unsigned =>
      do rd <- ireg_of dst; transl_addressing 1 addr args (PLd_rd_a (Pldrb W) rd) k
  | Mint8signed =>
      do rd <- ireg_of dst; transl_addressing 1 addr args (PLd_rd_a (Pldrsb W) rd) k
  | Mint16unsigned =>
      do rd <- ireg_of dst; transl_addressing 2 addr args (PLd_rd_a (Pldrh W) rd) k
  | Mint16signed =>
      do rd <- ireg_of dst; transl_addressing 2 addr args (PLd_rd_a (Pldrsh W) rd) k
  | Mint32 =>
      do rd <- ireg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrw rd) k
  | Mint64 =>
      do rd <- ireg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrx rd) k
  | Mfloat32 =>
      do rd <- freg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrs rd) k
  | Mfloat64 =>
      do rd <- freg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrd rd) k
  | Many32 =>
      do rd <- ireg_of dst; transl_addressing 4 addr args (PLd_rd_a Pldrw_a rd) k
  | Many64 =>
      do rd <- ireg_of dst; transl_addressing 8 addr args (PLd_rd_a Pldrx_a rd) k
  end.

Definition transl_store (chunk: memory_chunk) (addr: Op.addressing)
                        (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
  match chunk with
  | Mint8unsigned | Mint8signed =>
      do r1 <- ireg_of src; transl_addressing 1 addr args (PSt_rs_a Pstrb r1) k
  | Mint16unsigned | Mint16signed =>
      do r1 <- ireg_of src; transl_addressing 2 addr args (PSt_rs_a Pstrh r1) k
  | Mint32 =>
      do r1 <- ireg_of src; transl_addressing 4 addr args (PSt_rs_a Pstrw r1) k
  | Mint64 =>
      do r1 <- ireg_of src; transl_addressing 8 addr args (PSt_rs_a Pstrx r1) k
  | Mfloat32 =>
      do r1 <- freg_of src; transl_addressing 4 addr args (PSt_rs_a Pstrs r1) k
  | Mfloat64 =>
      do r1 <- freg_of src; transl_addressing 8 addr args (PSt_rs_a Pstrd r1) k
  | Many32 =>
      do r1 <- ireg_of src; transl_addressing 4 addr args (PSt_rs_a Pstrw_a r1) k
  | Many64 =>
      do r1 <- ireg_of src; transl_addressing 8 addr args (PSt_rs_a Pstrx_a r1) k
  end.

(** Translation of a Machblock instruction. *)

Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
                              (ep: bool) (k: bcode) :=
  match i with
  | MBgetstack ofs ty dst =>
      loadind XSP ofs ty dst k
  | MBsetstack src ofs ty =>
      storeind src XSP ofs ty k
  | MBgetparam ofs ty dst =>
      do c <- loadind X29 ofs ty dst k;
      OK (if ep then c else loadptr_bc XSP f.(fn_link_ofs) X29 c)
  | MBop op args res =>
      transl_op op args res k
  | MBload t chunk addr args dst =>
      match t with
      | TRAP => transl_load chunk addr args dst k
      | NOTRAP => Error(msg "Asmgenblock.transl_instr_basic: NOTRAP load not supported in aarch64.")
      end
  | MBstore chunk addr args src =>
      transl_store chunk addr args src k
  end.

(** Translation of a code sequence *)

Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
  match i with
  (*| MBgetstack ofs ty dst => before && negb (mreg_eq dst R29)*)
  | MBsetstack src ofs ty => before
  | MBgetparam ofs ty dst => negb (mreg_eq dst R29)
  | MBop op args res => before && negb (mreg_eq res R29)
  (*| MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst R29)*)
  | _ => false
  end.

Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
  match il with
  | nil => OK (nil)
  | i1 :: il' =>
      do k1 <- transl_basic_code f il' (it1_is_parent it1p i1);
      transl_instr_basic f i1 it1p k1
  end.

Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks :=
  match ex with
  | None =>
    match bdy with
    | nil => {| header := ll; body:= Pnop::nil; exit := None |} :: nil
    | _ => {| header := ll; body:= bdy; exit := None |} :: nil
    end
  | _ =>
    match bdy with
    | nil => {| header := ll; body:= nil; exit := ex |} :: nil
    | _ => {| header := ll; body:= bdy; exit := ex |} :: nil
    end
  end.
Next Obligation.
  induction bdy. congruence.
  simpl. auto.
Qed.
Next Obligation.
  destruct ex. simpl. auto.
  congruence.
Qed.
Next Obligation.
  induction bdy. congruence.
  simpl. auto.
Qed.

Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res (bcode*control) :=
  match ctl with
  | MBcall sig (inl r) => do r1 <- ireg_of r;
      OK (nil, PCtlFlow (Pblr r1 sig))
  | MBcall sig (inr symb) => OK (nil, PCtlFlow (Pbl symb sig))
  | MBtailcall sig (inr symb) => OK(make_epilogue f, PCtlFlow (Pbs symb sig))
  | MBtailcall sig (inl r) => do r1 <- ireg_of r;
      OK (make_epilogue f, PCtlFlow (Pbr r1 sig))
  | MBbuiltin ef args res => OK (nil, Pbuiltin ef (List.map (map_builtin_arg dreg_of) args) (map_builtin_res dreg_of res))
  | MBgoto lbl => OK (nil, PCtlFlow (Pb lbl))
  | MBcond cond args lbl => do (bc, c) <- transl_cond_branch cond args lbl nil; OK (bc, PCtlFlow c)
  | MBreturn => OK (make_epilogue f, PCtlFlow (Pret RA))
  | MBjumptable arg tbl => do r <- ireg_of arg;
      OK (nil, PCtlFlow (Pbtbl r tbl))
  end.

Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) : res (bcode*option control) :=
  match ext with
    Some ctl => do (b,c) <- transl_control f ctl; OK (b, Some c)
  | None => OK (nil, None)
  end.

Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
  do (bdy2, ex) <- transl_exit f fb.(Machblock.exit);
  do bdy1 <- transl_basic_code f fb.(Machblock.body) ep;
  OK (cons_bblocks fb.(Machblock.header) (bdy1 @@ bdy2) ex) 
  .

Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) :=
  match lmb with
  | nil => OK nil
  | mb :: lmb => 
      do lb <- transl_block f mb (if Machblock.header mb then ep else false);
      do lb' <- transl_blocks f lmb false;
      OK (lb @@ lb')
  end
.

Program Definition make_prologue (f:  Machblock.function) (k:bblocks) :=
  {| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::bi
      ((PSt_rs_a Pstrx RA) (ADimm XSP (Ptrofs.to_int64 (f.(fn_retaddr_ofs))))) ::bi nil;
      exit := None |} :: k.
  
Definition transl_function (f: Machblock.function) : res Asmblock.function :=
  do lb <- transl_blocks f f.(Machblock.fn_code) true;
  OK (mkfunction f.(Machblock.fn_sig)
        (make_prologue f lb)).

Definition transf_function (f: Machblock.function) : res Asmblock.function :=
  do tf <- transl_function f;
  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
  then Error (msg "code size exceeded")
  else OK tf.

Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
  transf_partial_fundef transf_function f.

Definition transf_program (p: Machblock.program) : res Asmblock.program :=
  transform_partial_program transf_fundef p.