Module Asmblockgen

Require Import Coqlib.
Require Import Errors AST Integers Floats Op.
Require Import Locations Compopts.
Require Import Machblock Asm Asmblock.
Require Import MemcpyTypes.

Local Open Scope list_scope.
Local Open Scope error_monad_scope.


Definition bcode := list basic.

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

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).

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).


Definition pop_bc (k: bblocks): bcode :=
  match k with
  | bb :: k' =>
      match bb.(header) with
      | nil => (body bb)
      | _ => nil
      end
  | _ => nil
  end.

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.

Parameter symbol_is_aligned : ident -> Z -> bool.



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

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


Definition mk_immed_mem_word (x: int): int :=
  if Int.lt x Int.zero then
    Int.neg (Int.zero_ext (if thumb tt then 8 else 12) (Int.neg x))
  else
    Int.zero_ext 12 x.

Definition mk_immed_mem_small (x: int): int :=
  if Int.lt x Int.zero then
    Int.neg (Int.zero_ext 8 (Int.neg x))
  else
    Int.zero_ext 8 x.

Definition mk_immed_mem_float (x: int): int :=
  let x := Int.and x (Int.repr (-4)) in (* mask low 2 bits off *)
  if Int.lt x Int.zero then
    Int.neg (Int.zero_ext 10 (Int.neg x))
  else
    Int.zero_ext 10 x.

Definition iterate_op (op1 op2: shift_op -> basic) (l: list int) (k: bcode) :=
  match l with
  | nil =>
      op1 (SOimm Int.zero) ::bi k (* should never happen *)
  | i :: l' =>
      op1 (SOimm i) :: map (fun i => op2 (SOimm i)) l' ++ k
  end.



Definition loadimm_word (r: ireg) (n: int) (k: bcode) :=
  let hi := Int.shru n (Int.repr 16) in
  if Int.eq hi Int.zero
  then Pmovw n r ::bi k
  else Pmovw (Int.zero_ext 16 n) r ::bi Pmovt hi r r ::bi k.

Definition loadimm (r: ireg) (n: int) (k: bcode) :=
  let d1 := decompose_int CONST n in
  let d2 := decompose_int OTHER (Int.not n) in
  let l1 := List.length d1 in
  let l2 := List.length d2 in
  if Nat.leb l1 1%nat then
    Pmov r (SOimm n) ::bi k
  else if Nat.leb l2 1%nat then
    Pmvn r (SOimm (Int.not n)) ::bi k
  else if Archi.thumb2_support then
    loadimm_word r n k
  else if Nat.leb l1 l2 then
    iterate_op (Pmov r) (Porr r r) d1 k
  else
    iterate_op (Pmvn r) (Pbic r r) d2 k.

Definition addimm (r1 r2: ireg) (n: int) (k: bcode) :=
  if Int.ltu (Int.repr (-256)) n then
    Psub r1 r2 (SOimm (Int.neg n)) ::bi k
  else
   (let d1 := decompose_int ADDSUB n in
    let d2 := decompose_int ADDSUB (Int.neg n) in
    if Nat.leb (List.length d1) (List.length d2)
    then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k
    else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k).

Definition rsubimm (r1 r2: ireg) (n: int) (k: bcode) :=
  iterate_op (Prsb r1 r2) (Padd r1 r1) (decompose_int OTHER n) k.

Definition andimm (r1 r2: ireg) (n: int) (k: bcode) :=
  if is_immed_arith OTHER n
  then Pand r1 r2 (SOimm n) ::bi k
  else iterate_op (Pbic r1 r2) (Pbic r1 r1) (decompose_int OTHER (Int.not n)) k.

Definition orimm (r1 r2: ireg) (n: int) (k: bcode) :=
  iterate_op (Porr r1 r2) (Porr r1 r1) (decompose_int OTHER n) k.

Definition xorimm (r1 r2: ireg) (n: int) (k: bcode) :=
  iterate_op (Peor r1 r2) (Peor r1 r1) (decompose_int OTHER n) k.


Definition transl_shift (s: shift) (r: ireg) : shift_op :=
  match s with
 | Slsl n => SOlsl r (s_amount n)
  | Slsr n => SOlsr r (s_amount n)
  | Sasr n => SOasr r (s_amount n)
  | Sror n => SOror r (s_amount n)
  end.


Definition transl_cond (cond: condition) (args: list mreg) (k: bcode) :=
  match cond, args with
  | Ccomp c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pcmp r1 (SOreg r2) ::bi k)
  | Ccompu c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pcmp r1 (SOreg r2) ::bi k)
  | Ccompshift c s, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pcmp r1 (transl_shift s r2) ::bi k)
  | Ccompushift c s, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pcmp r1 (transl_shift s r2) ::bi k)
  | Ccompimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (if is_immed_arith OTHER n then
            Pcmp r1 (SOimm n) ::bi k
          else if is_immed_arith OTHER (Int.neg n) then
            Pcmn r1 (SOimm (Int.neg n)) ::bi k
          else
            loadimm IR14 n (Pcmp r1 (SOreg IR14) ::bi k))
  | Ccompuimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (if is_immed_arith OTHER n then
            Pcmp r1 (SOimm n) ::bi k
          else if is_immed_arith OTHER (Int.neg n) then
            Pcmn r1 (SOimm (Int.neg n)) ::bi k
          else
            loadimm IR14 n (Pcmp r1 (SOreg IR14) ::bi k))
  | Ccompf cmp, a1 :: a2 :: nil =>
      do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfcmpd r1 r2 ::bi k)
  | Cnotcompf cmp, a1 :: a2 :: nil =>
      do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfcmpd r1 r2 ::bi k)
  | Ccompfzero cmp, a1 :: nil =>
      do r1 <- freg_of a1;
      OK (Pfcmpzd r1 ::bi k)
  | Cnotcompfzero cmp, a1 :: nil =>
      do r1 <- freg_of a1;
      OK (Pfcmpzd r1 ::bi k)
  | Ccompfs cmp, a1 :: a2 :: nil =>
      do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfcmps r1 r2 ::bi k)
  | Cnotcompfs cmp, a1 :: a2 :: nil =>
      do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfcmps r1 r2 ::bi k)
  | Ccompfszero cmp, a1 :: nil =>
      do r1 <- freg_of a1;
      OK (Pfcmpzs r1 ::bi k)
  | Cnotcompfszero cmp, a1 :: nil =>
      do r1 <- freg_of a1;
      OK (Pfcmpzs r1 ::bi k)
  | (Cmaskzero n | Cmasknotzero n), a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (if is_immed_arith OTHER n then
            Ptst r1 (SOimm n) ::bi k
          else
            loadimm IR14 n (Ptst r1 (SOreg IR14) ::bi k))
  | Ccompcarryu c, hi1 :: lo1 :: hi2 :: lo2 :: nil =>
      do rhi1 <- ireg_of hi1;
      do rlo1 <- ireg_of lo1;
      do rhi2 <- ireg_of hi2;
      do rlo2 <- ireg_of lo2;
      match c with
      | Cgt | Cle =>
          OK (Pcmp rlo2 (SOreg rlo1) ::bi
              Psbcs IR14 rhi2 (SOreg rhi1) ::bi k)
      | Clt | Cge =>
          OK (Pcmp rlo1 (SOreg rlo2) ::bi
              Psbcs IR14 rhi1 (SOreg rhi2) ::bi k)
      | Ceq | Cne =>
          Error (msg "Asmblockgen.Ccompcarryu: equality not supported")
      end
  | Ccompcarry c, hi1 :: lo1 :: hi2 :: lo2 :: nil =>
      do rhi1 <- ireg_of hi1;
      do rlo1 <- ireg_of lo1;
      do rhi2 <- ireg_of hi2;
      do rlo2 <- ireg_of lo2;
      match c with
      | Cgt | Cle =>
          OK (Pcmp rlo2 (SOreg rlo1) ::bi
              Psbcs IR14 rhi2 (SOreg rhi1) ::bi k)
      | Clt | Cge =>
          OK (Pcmp rlo1 (SOreg rlo2) ::bi
              Psbcs IR14 rhi1 (SOreg rhi2) ::bi k)
      | Ceq | Cne =>
          Error (msg "Asmblockgen.Ccompcarry: equality not supported")
      end
  | _, _ =>
      Error(msg "Asmgen.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 => cond_for_signed_cmp cmp
  | Ccompushift cmp s => cond_for_unsigned_cmp cmp
  | Ccompimm cmp n => cond_for_signed_cmp cmp
  | Ccompuimm cmp n => cond_for_unsigned_cmp cmp
  | 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
  | Ccompcarryu cmp =>
      match cmp with
      | Clt | Cge => cond_for_unsigned_cmp cmp
      | Cgt | Cle => cond_for_unsigned_cmp (swap_comparison cmp)
      | Ceq => TCeq | Cne => TCne
      end
  | Ccompcarry cmp =>
      match cmp with
      | Clt | Cge => cond_for_signed_cmp cmp
      | Cgt | Cle => cond_for_signed_cmp (swap_comparison cmp)
      | Ceq => TCeq | Cne => TCne
      end
  | Cmaskzero _ => TCeq
  | Cmasknotzero _ => TCne
  end.


Definition transl_op_cmp_cne (cmp: condition) (args: list mreg) (r: ireg) (k: bcode)
  : option (res bcode) :=
  match cmp, args with
  | Ccomp Cne, a1 :: a2 :: nil =>
      Some (do r1 <- ireg_of a1; do r2 <- ireg_of a2;
            OK (Psubs r r1 (SOreg r2) ::bi
                Pmovite TCeq r (SOreg r) (SOimm Int.one) ::bi k))
  | Ccompimm Cne i, a1 :: nil =>
      if is_immed_arith OTHER i then
        Some (do r1 <- ireg_of a1;
              OK (Psubs r r1 (SOimm i) ::bi
                  Pmovite TCeq r (SOreg r) (SOimm Int.one) ::bi k))
      else if is_immed_arith OTHER (Int.neg i) then
        Some (do r1 <- ireg_of a1;
              OK (Padds r r1 (SOimm (Int.neg i)) ::bi
                  Pmovite TCeq r (SOreg r) (SOimm Int.one) ::bi k))
      else
        None
  | _, _ =>
      None
  end.

Definition transl_op_cmp_ceq_clz (cmp: condition) (args: list mreg) (r: ireg) (k: bcode)
  : option (res bcode) :=
  match cmp, args with
  | Ccomp Ceq, a1 :: a2 :: nil =>
      Some (do r1 <- ireg_of a1; do r2 <- ireg_of a2;
            OK (Psub r r1 (SOreg r2) ::bi
                Pclz r r ::bi
                Pmov r (SOlsr r (Int.repr 5)) ::bi k))
  | Ccompshift Ceq s, a1 :: a2 :: nil =>
      Some (do r1 <- ireg_of a1; do r2 <- ireg_of a2;
            OK (Psub r r1 (transl_shift s r2) ::bi
                Pclz r r ::bi
                Pmov r (SOlsr r (Int.repr 5)) ::bi k))
  | Ccompimm Ceq n, a1 :: nil =>
      if Int.eq n Int.zero then
        Some (do r1 <- ireg_of a1;
              OK (Pclz r r1 ::bi
                  Pmov r (SOlsr r (Int.repr 5)) ::bi k))
      else if is_immed_arith OTHER n then
        Some (do r1 <- ireg_of a1;
              OK (Psub r r1 (SOimm n) ::bi
                  Pclz r r ::bi
                  Pmov r (SOlsr r (Int.repr 5)) ::bi k))
      else if is_immed_arith OTHER (Int.neg n) then
        Some (do r1 <- ireg_of a1;
              OK (Padd r r1 (SOimm (Int.neg n)) ::bi
                  Pclz r r ::bi
                  Pmov r (SOlsr r (Int.repr 5)) ::bi k))
      else
        None
  | _, _ =>
      None
  end.

Definition transl_op_cmp_default (cmp: condition) (args: list mreg) (r: ireg) (k: bcode) :=
  transl_cond cmp args
    (Pmovite (cond_for_cond cmp) r (SOimm Int.one) (SOimm Int.zero) ::bi k).

Definition transl_op_cmp (cmp: condition) (args: list mreg) (r: ireg) (k: bcode) :=
  match transl_op_cmp_cne cmp args r k with
  | Some res => res
  | None =>
      if Compopts.cmp_via_clz tt then
        match transl_op_cmp_ceq_clz cmp args r k with
        | Some res => res
        | None => transl_op_cmp_default cmp args r k
        end
      else
        transl_op_cmp_default cmp args r k
  end.

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 (SOreg a) ::bi k)
      | FR r, FR a => OK (Pfcpyd r a ::bi k)
      | _ , _ => Error(msg "Asmblockgen.Omove")
      end
  | Ocopy, a1 :: a2 :: nil =>
      assertion (mreg_eq res a1);
      OK (Pnop false ::bi k)
  | Ocopyimm _, a1 :: nil =>
      assertion (mreg_eq res a1);
      OK (Pnop false ::bi k)
  | Ointconst n, nil =>
      do r <- ireg_of res;
      OK (loadimm r n k)
  | Ofloatconst f, nil =>
      do r <- freg_of res;
      if Compopts.optim_double_zero_via_int tt then
        if Float.eq_dec f Float.zero
        then OK (loadimm IR14 Int.zero (Pdouble_of_iibits r IR14 IR14 ::bi k))
        else OK (Pflid r f ::bi k)
      else OK (Pflid r f ::bi k)
  | Osingleconst f, nil =>
      do r <- freg_of res;
      if Compopts.optim_single_zero_via_int tt then
        if Float32.eq_dec f Float32.zero
        then OK (loadimm IR14 Int.zero (Psingle_of_bits r IR14 ::bi k))
        else OK (Pflis f r ::bi k)
      else OK (Pflis f r ::bi k)
  | Oaddrsymbol s ofs, nil =>
      do r <- ireg_of res;
      OK (Ploadsymbol r s ofs ::bi k)
  | Oaddrstack n, nil =>
      do r <- ireg_of res;
      OK (addimm r IR13 (Ptrofs.to_int n) k)
  | Ocast8signed, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (if Archi.thumb2_support then
            Psxtb r r1 ::bi k
          else
            Pmov r (SOlsl r1 (Int.repr 24)) ::bi
            Pmov r (SOasr r (Int.repr 24)) ::bi k)
  | Ocast16signed, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (if Archi.thumb2_support then
            Psxth r r1 ::bi k
          else
            Pmov r (SOlsl r1 (Int.repr 16)) ::bi
            Pmov r (SOasr r (Int.repr 16)) ::bi k)
  | Oadd, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Padd r r1 (SOreg r2) ::bi k)
  | Oaddshift s, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Padd r r1 (transl_shift s r2) ::bi k)
  | Oaddimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (addimm r r1 n k)
  | Osub, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Psub r r1 (SOreg r2) ::bi k)
  | Osubshift s, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Psub r r1 (transl_shift s r2) ::bi k)
  | Orsubshift s, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Prsb r r1 (transl_shift s r2) ::bi k)
  | Orsubimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (rsubimm r r1 n k)
  | Omul, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pmul r r1 r2 ::bi k)
  | Omla, a1 :: a2 :: a3 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      do r2 <- ireg_of a2; do r3 <- ireg_of a3;
      OK (Pmla r r1 r2 r3 ::bi k)
  | Omls, a1 :: a2 :: a3 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      do r2 <- ireg_of a2; do r3 <- ireg_of a3;
      OK (Pmls r r1 r2 r3 ::bi k)
  | Omulhs, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Psmull IR14 r r1 r2 ::bi k)
  | Omulhu, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pumull IR14 r r1 r2 ::bi k)
  | Odiv, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      if Archi.hardware_idiv tt then
        OK (Psdiv r r1 r2 ::bi k)
      else
        assertion (mreg_eq res R0);
        assertion (mreg_eq a1 R0);
        assertion (mreg_eq a2 R1);
        OK (Psdiv r r1 r2 ::bi k)
  | Odivu, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      if Archi.hardware_idiv tt then
        OK (Pudiv r r1 r2 ::bi k)
      else
        assertion (mreg_eq res R0);
        assertion (mreg_eq a1 R0);
        assertion (mreg_eq a2 R1);
        OK (Pudiv r r1 r2 ::bi k)
  | Oand, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pand r r1 (SOreg r2) ::bi k)
  | Oandshift s, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pand r r1 (transl_shift s r2) ::bi k)
  | Oandimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (if Archi.thumb2_support && Int.eq n (Int.repr 255) then
            Puxtb r r1 ::bi k
          else if Archi.thumb2_support && Int.eq n (Int.repr 65535) then
            Puxth r r1 ::bi k
          else andimm r r1 n k)
  | Oor, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Porr r r1 (SOreg r2) ::bi k)
  | Oorshift s, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Porr r r1 (transl_shift s r2) ::bi k)
  | Oorimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (orimm r r1 n k)
  | Oxor, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Peor r r1 (SOreg r2) ::bi k)
  | Oxorshift s, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Peor r r1 (transl_shift s r2) ::bi k)
  | Oxorimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (xorimm r r1 n k)
  | Obic, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pbic r r1 (SOreg r2) ::bi k)
  | Obicshift s, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pbic r r1 (transl_shift s r2) ::bi k)
  | Onot, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (Pmvn r (SOreg r1) ::bi k)
  | Onotshift s, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (Pmvn r (transl_shift s r1) ::bi k)
  | Oshl, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Plsl r r1 r2 ::bi k)
  | Oshr, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pasr r r1 r2 ::bi k)
  | Oshru, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Plsr r r1 r2 ::bi k)
  | Oror, a1 :: a2 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK (Pror r r1 r2 ::bi k)
  | Oshift s, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (Pmov r (transl_shift s r1) ::bi k)
  | Oshrximm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      if Int.eq n Int.zero then
        OK (Pmov r (SOreg r1) ::bi k)
      else if Int.eq n Int.one then
        OK (Padd IR14 r1 (SOlsr r1 (Int.repr 31)) ::bi
            Pmov r (SOasr IR14 n) ::bi k)
      else
        OK (Pmov IR14 (SOasr r1 (Int.repr 31)) ::bi
            Padd IR14 r1 (SOlsr IR14 (Int.sub Int.iwordsize n)) ::bi
            Pmov r (SOasr IR14 n) ::bi k)
  | Onegf, a1 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1;
      OK (Pfnegd r r1 ::bi k)
  | Oabsf, a1 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1;
      OK (Pfabsd r r1 ::bi k)
  | Oaddf, a1 :: a2 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfaddd r r1 r2 ::bi k)
  | Osubf, a1 :: a2 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfsubd r r1 r2 ::bi k)
  | Omulf, a1 :: a2 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfmuld r r1 r2 ::bi k)
  | Omlaf, a1 :: a2 :: a3 :: nil =>
      assertion (mreg_eq a1 res);
      do r1 <- freg_of a1; do r2 <- freg_of a2; do r3 <- freg_of a3;
      OK (Pfmlad r1 r2 r3 ::bi k)
  | Omlsf, a1 :: a2 :: a3 :: nil =>
      assertion (mreg_eq a1 res);
      do r1 <- freg_of a1; do r2 <- freg_of a2; do r3 <- freg_of a3;
      OK (Pfmlsd r1 r2 r3 ::bi k)
  | Odivf, a1 :: a2 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfdivd r r1 r2 ::bi k)
  | Osqrtf, a1 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1;
      OK (Pfsqrtd r r1 ::bi k)
  | Onegfs, a1 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1;
      OK (Pfnegs r r1 ::bi k)
  | Oabsfs, a1 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1;
      OK (Pfabss r r1 ::bi k)
  | Oaddfs, a1 :: a2 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfadds r r1 r2 ::bi k)
  | Osubfs, a1 :: a2 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfsubs r r1 r2 ::bi k)
  | Omulfs, a1 :: a2 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfmuls r r1 r2 ::bi k)
  | Omlafs, a1 :: a2 :: a3 :: nil =>
      assertion (mreg_eq a1 res);
      do r1 <- freg_of a1; do r2 <- freg_of a2; do r3 <- freg_of a3;
      OK (Pfmlas r1 r2 r3 ::bi k)
  | Omlsfs, a1 :: a2 :: a3 :: nil =>
      assertion (mreg_eq a1 res);
      do r1 <- freg_of a1; do r2 <- freg_of a2; do r3 <- freg_of a3;
      OK (Pfmlss r1 r2 r3 ::bi k)
  | Odivfs, a1 :: a2 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2;
      OK (Pfdivs r r1 r2 ::bi k)
  | Osqrtfs, a1 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1;
      OK (Pfsqrts r r1 ::bi k)
  | Osingleoffloat, a1 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1;
      OK (Pfcvtsd r r1 ::bi k)
  | Ofloatofsingle, a1 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1;
      OK (Pfcvtds r r1 ::bi k)
  | Ointoffloat, a1 :: nil =>
      do r <- ireg_of res; do r1 <- freg_of a1;
      OK (Pftosizd r r1 ::bi k)
  | Ointuoffloat, a1 :: nil =>
      do r <- ireg_of res; do r1 <- freg_of a1;
      OK (Pftouizd r r1 ::bi k)
  | Ofloatofint, a1 :: nil =>
      do r <- freg_of res; do r1 <- ireg_of a1;
      OK (Pfsitod r r1 ::bi k)
  | Ofloatofintu, a1 :: nil =>
      do r <- freg_of res; do r1 <- ireg_of a1;
      OK (Pfuitod r r1 ::bi k)
  | Ointofsingle, a1 :: nil =>
      do r <- ireg_of res; do r1 <- freg_of a1;
      OK (Pftosizs r r1 ::bi k)
  | Ointuofsingle, a1 :: nil =>
      do r <- ireg_of res; do r1 <- freg_of a1;
      OK (Pftouizs r r1 ::bi k)
  | Osingleofint, a1 :: nil =>
      do r <- freg_of res; do r1 <- ireg_of a1;
      OK (Pfsitos r r1 ::bi k)
  | Osingleofintu, a1 :: nil =>
      do r <- freg_of res; do r1 <- ireg_of a1;
      OK (Pfuitos r r1 ::bi k)
  | Ocmp cmp, _ =>
      do r <- ireg_of res;
      transl_op_cmp cmp args r k
  | Osel cmp, a1 :: a2 :: args =>
      match preg_of res with
      | IR r =>
          do r1 <- ireg_of a1; do r2 <- ireg_of a2;
          if ireg_eq r1 r2 then
            OK (Pmov r (SOreg r1) ::bi k)
          else
            transl_cond cmp args
              (Pmovite (cond_for_cond cmp) r (SOreg r1) (SOreg r2) ::bi k)
      | FR r =>
          do r1 <- freg_of a1; do r2 <- freg_of a2;
          if freg_eq r1 r2 then
            OK (Pfcpyd r r1 ::bi k)
          else
            transl_cond cmp args
              (Pfmovite (cond_for_cond cmp) r r1 r2 ::bi k)
      | _ =>
          Error(msg "Asmgen.Osel")
      end
  | Oselimm cmp imm, a1 :: args =>
      do r <- ireg_of res;
      do r1 <- ireg_of a1;
      transl_cond cmp args
        (Pmovite (cond_for_cond cmp) r (SOreg r1) (SOimm imm) ::bi k)
  | Oselimm2 cmp imm1 imm2, args =>
      do r <- ireg_of res;
      transl_cond cmp args
        (Pmovite (cond_for_cond cmp) r (SOimm imm1) (SOimm imm2) ::bi k)
  | Oclz, a1 :: nil =>
      do r <- ireg_of res;
      do r1 <- ireg_of a1;
      OK (Pclz r r1 ::bi k)
  | Oreverse_bits, a1 :: nil =>
      do r <- ireg_of res;
      do r1 <- ireg_of a1;
      OK (Prbit r r1 ::bi k)
  | Obswap32, a1 :: nil =>
      do r <- ireg_of res;
      do r1 <- ireg_of a1;
      OK (Prev r r1 ::bi k)
  | Obits_of_single, a1 :: nil =>
      do r <- ireg_of res;
      do r1 <- freg_of a1;
      OK (Pbits_of_single r r1 ::bi k)
  | Ohibits_of_float, a1 :: nil =>
      do r <- ireg_of res;
      do r1 <- freg_of a1;
      OK (Phibits_of_float r r1 ::bi k)
  | Osingle_of_bits, a1 :: nil =>
      do r <- freg_of res;
      do r1 <- ireg_of a1;
      OK (Psingle_of_bits r r1 ::bi k)
  | (Osbfx lsb sz), a1 :: nil =>
      do r <- ireg_of res;
      do r1 <- ireg_of a1;
      OK (if Int.eq lsb Int.zero && Int.eq sz (Int.repr 8) then
            Psxtb r r1 ::bi k
          else if Int.eq lsb Int.zero && Int.eq sz (Int.repr 16) then
            Psxth r r1 ::bi k
          else Psbfx lsb sz r r1 ::bi k)
  | (Oubfx lsb sz), a1 :: nil =>
      do r <- ireg_of res;
      do r1 <- ireg_of a1;
      OK (if Int.eq lsb Int.zero && Int.eq sz (Int.repr 8) then
            Puxtb r r1 ::bi k
          else if Int.eq lsb Int.zero && Int.eq sz (Int.repr 16) then
            Puxth r r1 ::bi k
          else Pubfx lsb sz r r1 ::bi k)
  | (Obfc lsb sz), a1 :: nil =>
      assertion (mreg_eq a1 res);
      do r1 <- ireg_of a1;
      OK (if Archi.thumb2_support
             && Int.eq lsb (Int.repr 8) && Int.eq sz (Int.repr 24) then
            Puxtb r1 r1 ::bi k
          else if Archi.thumb2_support
             && Int.eq lsb (Int.repr 16) && Int.eq sz (Int.repr 16) then
            Puxth r1 r1 ::bi k
          else Pbfc lsb sz r1 r1 ::bi k)
  | (Obfi lsb sz), a1 :: a2 :: nil =>
      assertion (mreg_eq a1 res);
      do r1 <- ireg_of a1;
      do r2 <- ireg_of a2;
      OK (Pbfi lsb sz r1 r1 r2 ::bi k)
  | Ogetcanary, nil =>
      do r <- ireg_of res;
      OK (Pgetcanary r ::bi k)
  | Oaddimm_reg n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (addimm r r1 n k)
  | OEaddimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (Padd r r1 (SOimm n) ::bi k)
  | OEsubimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (Psub r r1 (SOimm n) ::bi k)
  | OErsbimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (Prsb r r1 (SOimm n) ::bi k)
  | OEandimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (if Archi.thumb2_support && Int.eq n (Int.repr 255) then
            Puxtb r r1 ::bi k
          else if Archi.thumb2_support && Int.eq n (Int.repr 65535) then
            Puxth r r1 ::bi k
          else Pand r r1 (SOimm n) ::bi k)
  | OEbicimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (Pbic r r1 (SOimm n) ::bi k)
  | OEorrimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (Porr r r1 (SOimm n) ::bi k)
  | OEeorimm n, a1 :: nil =>
      do r <- ireg_of res; do r1 <- ireg_of a1;
      OK (Peor r r1 (SOimm n) ::bi k)
  | OEmovimm n, nil =>
      do r <- ireg_of res;
      OK (Pmov r (SOimm n) ::bi k)
  | OEmvnimm n, nil =>
      do r <- ireg_of res;
      OK (Pmvn r (SOimm n) ::bi k)
  | Ocmpcarryu c, hi1 :: lo1 :: hi2 :: lo2 :: nil =>
      do r <- ireg_of res;
      do rhi1 <- ireg_of hi1;
      do rlo1 <- ireg_of lo1;
      do rhi2 <- ireg_of hi2;
      do rlo2 <- ireg_of lo2;
      match c with
      | Cgt | Cle =>
          OK (Pcmp rlo2 (SOreg rlo1) ::bi
              Psbcs r rhi2 (SOreg rhi1) ::bi
              Pmovite (cond_for_unsigned_cmp (swap_comparison c)) r
                      (SOimm Int.one) (SOimm Int.zero) ::bi k)
      | Clt | Cge =>
          OK (Pcmp rlo1 (SOreg rlo2) ::bi
              Psbcs r rhi1 (SOreg rhi2) ::bi
              Pmovite (cond_for_unsigned_cmp c) r
                      (SOimm Int.one) (SOimm Int.zero) ::bi k)
      | Ceq | Cne =>
          Error (msg "Asmblockgen.Ocmpcarryu: equality not supported")
      end
  | Ocmpcarry c, hi1 :: lo1 :: hi2 :: lo2 :: nil =>
      do r <- ireg_of res;
      do rhi1 <- ireg_of hi1;
      do rlo1 <- ireg_of lo1;
      do rhi2 <- ireg_of hi2;
      do rlo2 <- ireg_of lo2;
      match c with
      | Cgt | Cle =>
          OK (Pcmp rlo2 (SOreg rlo1) ::bi
              Psbcs r rhi2 (SOreg rhi1) ::bi
              Pmovite (cond_for_signed_cmp (swap_comparison c)) r
                      (SOimm Int.one) (SOimm Int.zero) ::bi k)
      | Clt | Cge =>
          OK (Pcmp rlo1 (SOreg rlo2) ::bi
              Psbcs r rhi1 (SOreg rhi2) ::bi
              Pmovite (cond_for_signed_cmp c) r
                      (SOimm Int.one) (SOimm Int.zero) ::bi k)
      | Ceq | Cne =>
          Error (msg "Asmblockgen.Ocmpcarry: equality not supported")
      end
  | _, _ => Error (msg "Asmblockgen.transl_op")
  end.


Definition indexed_memory_access
    (mk_instr: ireg -> int -> basic)
    (mk_immed: int -> int)
    (base: ireg) (n: int) (k: bcode) :=
  let n1 := mk_immed n in
  if Int.eq n n1
  then mk_instr base n ::bi k
  else addimm IR14 base (Int.sub n n1) (mk_instr IR14 n1 ::bi k).

Definition loadind_int (base: ireg) (ofs: ptrofs) (dst: ireg) (k: bcode) :=
  indexed_memory_access (fun base n => Pldr dst base (SOimm n)) mk_immed_mem_word base (Ptrofs.to_int ofs) k.

Definition storeind_int (base: ireg) (ofs: ptrofs) (dst: ireg) (k: bcode) :=
  indexed_memory_access (fun base n => Pstr dst base (SOimm n)) mk_immed_mem_word base (Ptrofs.to_int ofs) k.

Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
  let ofs := Ptrofs.to_int ofs in
  match ty, preg_of dst with
  | Tint, IR r =>
      OK (indexed_memory_access (fun base n => Pldr r base (SOimm n)) mk_immed_mem_word base ofs k)
  | Tany32, IR r =>
      OK (indexed_memory_access (fun base n => Pldr_a r base (SOimm n)) mk_immed_mem_word base ofs k)
  | Tsingle, FR r =>
      OK (indexed_memory_access (Pflds r) mk_immed_mem_float base ofs k)
  | Tfloat, FR r =>
      OK (indexed_memory_access (Pfldd r) mk_immed_mem_float base ofs k)
  | Tany64, FR r =>
      OK (indexed_memory_access (Pfldd_a r) mk_immed_mem_float base ofs k)
  | _, _ =>
      Error (msg "Asmgen.loadind")
  end.

Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: bcode) :=
  let ofs := Ptrofs.to_int ofs in
  match ty, preg_of src with
  | Tint, IR r =>
      OK (indexed_memory_access (fun base n => Pstr r base (SOimm n)) mk_immed_mem_word base ofs k)
  | Tany32, IR r =>
      OK (indexed_memory_access (fun base n => Pstr_a r base (SOimm n)) mk_immed_mem_word base ofs k)
  | Tsingle, FR r =>
      OK (indexed_memory_access (Pfsts r) mk_immed_mem_float base ofs k)
  | Tfloat, FR r =>
      OK (indexed_memory_access (Pfstd r) mk_immed_mem_float base ofs k)
  | Tany64, FR r =>
      OK (indexed_memory_access (Pfstd_a r) mk_immed_mem_float base ofs k)
  | _, _ =>
      Error (msg "Asmgen.storeind")
  end.


Definition save_lr (ofs: ptrofs) (k: bcode) :=
  let n := Ptrofs.to_int ofs in
  let n1 := mk_immed_mem_word n in
  if Int.eq n n1
  then Pstr IR14 IR13 (SOimm n) ::bi k
  else addimm IR12 IR13 (Int.sub n n1) (Pstr IR14 IR12 (SOimm n1) ::bi k).

Definition save_lr_preserves_R12 (ofs: ptrofs) : bool :=
  let n := Ptrofs.to_int ofs in
  let n1 := mk_immed_mem_word n in
  Int.eq n n1.


Definition cond_preserves_IR14 (cond: condition) : bool :=
  match cond with
  | Ccompimm _ n | Ccompuimm _ n =>
      is_immed_arith OTHER n || is_immed_arith OTHER (Int.neg n)
  | Cmaskzero n | Cmasknotzero n =>
      is_immed_arith OTHER n
  | Ccompcarryu _ | Ccompcarry _ => false
  | _ => true
  end.

Definition addr_preserves_IR14 (mk_immed: int -> int) (addr: addressing) : bool :=
  match addr with
  | Aindexed n => Int.eq n (mk_immed n)
  | Ainstack n => let n' := Ptrofs.to_int n in Int.eq n' (mk_immed n')
  | Aindexed2 => true
  | Aindexed2shift _ => true
  end.

Definition preserves_IR14 (i: Machblock.basic_inst) : bool :=
  match i with
  | MBgetstack ofs ty _ | MBsetstack _ ofs ty =>
      let n := Ptrofs.to_int ofs in
      match ty with
      | Tint | Tany32 => Int.eq n (mk_immed_mem_word n)
      | Tsingle | Tfloat | Tany64 => Int.eq n (mk_immed_mem_float n)
      | _ => false
      end
  | MBgetparam _ _ _ => false
  | MBop op args res =>
      match op with
      | Omulhs | Omulhu | Ofloatconst _ => false
      | Oshrximm n => Int.eq n Int.zero
      | Ocmp cmp | Osel cmp | Oselimm cmp _ | Oselimm2 cmp _ _ => cond_preserves_IR14 cmp
      | Osingleconst f =>
          if Compopts.optim_single_zero_via_int tt
          then negb (Float32.eq_dec f Float32.zero)
          else true
      | _ => true
      end
  | MBload _ chunk addr _ _ =>
      addr_preserves_IR14
        (match chunk with
         | Mint8signed | Mint16signed | Mint16unsigned => mk_immed_mem_small
         | Mint8unsigned | Mint32 | Mint32al1 => mk_immed_mem_word
         | Mfloat32 | Mfloat64 => mk_immed_mem_float
         | _ => fun _ => Int.one
         end) addr
  | MBstore chunk addr _ _ =>
      addr_preserves_IR14
        (match chunk with
         | Mint8unsigned | Mint32 | Mint32al1 => mk_immed_mem_word
         | Mint16unsigned => mk_immed_mem_small
         | Mfloat32 | Mfloat64 => mk_immed_mem_float
         | _ => fun _ => Int.one
         end) addr
  | MBmemcpy sz _ =>
      match sz with
      | SZ8 => Archi.expanse_memcpy_fpu || negb (thumb tt)
      | _ => false
      end
  | MBsavecallee _ _ => false
  | MBrestorecallee _ _ => false
  end.


Definition exit_preserves_IR14 (oexit: option Machblock.control_flow_inst) : bool :=
  match oexit with
  | None => true
  | Some (MBcall _ _) => false
  | Some (MBtailcall _ _) => true
  | Some (MBbuiltin _ _ _) => false
  | Some (MBjumptable _ _) => false
  | Some (MBcond cond _ _) => cond_preserves_IR14 cond
  | Some MBreturn => true
  | Some (MBgoto _) => true
  end.

Definition bblock_preserves_IR14 (bb: Machblock.bblock) : bool :=
  forallb preserves_IR14 (Machblock.body bb) &&
  exit_preserves_IR14 (Machblock.exit bb).

Definition function_preserves_IR14 (f: Machblock.function) : bool :=
  forallb bblock_preserves_IR14 (Machblock.fn_code f).


Definition transl_memory_access
     (mk_instr_imm: ireg -> int -> basic)
     (mk_instr_gen: option (ireg -> shift_op -> basic))
     (mk_immed: int -> int)
     (addr: addressing) (args: list mreg) (k: bcode) :=
  match addr, args with
  | Aindexed n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (indexed_memory_access mk_instr_imm mk_immed r1 n k)
  | Aindexed2, a1 :: a2 :: nil =>
      match mk_instr_gen with
      | Some f =>
          do r1 <- ireg_of a1; do r2 <- ireg_of a2;
          OK (f r1 (SOreg r2) :: k)
      | None =>
          Error (msg "Asmgen.Aindexed2")
      end
  | Aindexed2shift s, a1 :: a2 :: nil =>
      match mk_instr_gen with
      | Some f =>
          do r1 <- ireg_of a1; do r2 <- ireg_of a2;
          OK (f r1 (transl_shift s r2) :: k)
      | None =>
          Error (msg "Asmgen.Aindexed2shift")
      end
  | Ainstack n, nil =>
      OK (indexed_memory_access mk_instr_imm mk_immed IR13 (Ptrofs.to_int n) k)
  | _, _ =>
      Error(msg "Asmgen.transl_memory_access")
  end.

Definition transl_memory_access_int
     (mk_instr: ireg -> ireg -> shift_op -> basic)
     (mk_immed: int -> int)
     (dst: mreg) (addr: addressing) (args: list mreg) (k: bcode) :=
  do rd <- ireg_of dst;
  transl_memory_access
    (fun r n => mk_instr rd r (SOimm n))
    (Some (mk_instr rd))
    mk_immed addr args k.

Definition transl_memory_access_float
     (mk_instr: freg -> ireg -> int -> basic)
     (mk_immed: int -> int)
     (dst: mreg) (addr: addressing) (args: list mreg) (k: bcode) :=
  do rd <- freg_of dst;
  transl_memory_access
    (mk_instr rd)
    None
    mk_immed addr args k.

Definition transl_load (trap : trapping_mode)
           (chunk: memory_chunk) (addr: addressing)
           (args: list mreg) (dst: mreg) (k: bcode) :=
  match trap with
  | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm")
  | TRAP =>
  match chunk with
  | Mint8signed =>
      transl_memory_access_int (fun r => Pldrsb r) mk_immed_mem_small dst addr args k
  | Mint8unsigned =>
      transl_memory_access_int (fun r => Pldrb r) mk_immed_mem_word dst addr args k
  | Mint16signed =>
      transl_memory_access_int (fun r => Pldrsh r) mk_immed_mem_small dst addr args k
  | Mint16unsigned =>
      transl_memory_access_int (fun r => Pldrh r) mk_immed_mem_small dst addr args k
  | Mint32 =>
      transl_memory_access_int (fun r => Pldr r) mk_immed_mem_word dst addr args k
  | Mint32al1 =>
      transl_memory_access_int (fun r => Pldr_u r) mk_immed_mem_word dst addr args k
  | Mfloat32 =>
      transl_memory_access_float (fun r => Pflds r) mk_immed_mem_float dst addr args k
  | Mfloat64 =>
      transl_memory_access_float (fun r => Pfldd r) mk_immed_mem_float dst addr args k
  | _ =>
      Error (msg "Asmgen.transl_load")
  end
  end.

Definition transl_store (chunk: memory_chunk) (addr: addressing)
                       (args: list mreg) (src: mreg) (k: bcode) :=
  match chunk with
  | Mint8unsigned =>
      transl_memory_access_int (fun r => Pstrb r) mk_immed_mem_word src addr args k
  | Mint16unsigned =>
      transl_memory_access_int (fun r => Pstrh r) mk_immed_mem_small src addr args k
  | Mint32 =>
      transl_memory_access_int (fun r => Pstr r) mk_immed_mem_word src addr args k
  | Mint32al1 =>
      transl_memory_access_int (fun r => Pstr_u r) mk_immed_mem_word src addr args k
  | Mfloat32 =>
      transl_memory_access_float (fun r => Pfsts r) mk_immed_mem_float src addr args k
  | Mfloat64 =>
      transl_memory_access_float (fun r => Pfstd r) mk_immed_mem_float src addr args k
  | _ =>
      Error (msg "Asmgen.transl_store")
  end.

Definition extract_memcpy_builtin_arg (barg: builtin_arg mreg) :=
  match barg with
  | BA r => do r' <- ireg_of r; OK (r', Int.zero)
  | BA_addptr (BA r) (BA_int n) => do r' <- ireg_of r; OK (r', n)
  | BA_addrstack ofs => OK (IR13, Ptrofs.to_int ofs)
  | _ => Error (msg "extract_memcpy_builtin_arg: invalid argument")
  end.

Definition indexed_memcpy_access
    (mk_instr: ireg -> ireg -> int -> int -> basic)
    (mk_immed: int -> int)
    (ras rad: ireg) (n1 n2: int) (k: bcode) :=
  let n1' := mk_immed n1 in
  let n2' := mk_immed n2 in
  let (ras', rad') :=
    if negb (PregEq.eq ras IR3) && negb (PregEq.eq rad IR2)
    then (IR2, IR3) else (IR3, IR2) in
  let eqr2 := PregEq.eq ras IR2 && PregEq.eq rad IR2 in
  let eqr3 := PregEq.eq ras IR3 && PregEq.eq rad IR3 in
  match Int.eq n1 n1', Int.eq n2 n2' with
  | true, true => mk_instr ras rad n1' n2' ::bi k
  | false, true =>
      let ras'' := if eqr3 then IR2 else ras' in
      addimm ras'' ras (Int.sub n1 n1') (mk_instr ras'' rad n1' n2' ::bi k)
  | true, false =>
      let rad'' := if eqr2 then IR3 else rad' in
      addimm rad'' rad (Int.sub n2 n2') (mk_instr ras rad'' n1' n2' ::bi k)
  | false, false =>
      if eqr3 then
        addimm rad' rad (Int.sub n2 n2')
        (addimm ras' ras (Int.sub n1 n1')
        (mk_instr ras' rad' n1' n2' ::bi k))
      else
        addimm ras' ras (Int.sub n1 n1')
        (addimm rad' rad (Int.sub n2 n2')
        (mk_instr ras' rad' n1' n2' ::bi k))
  end.

Definition select_memcpy_inst (sz: memcpy_typ) (ras rad: ireg) (ofss ofsd: int) (k: bcode) :=
  let mcpy_inst := fun cpy r1 r2 i1 i2 => PMemcpy cpy r1 r2 (Ofs i1) (Ofs i2) in
  let (mk_instr, mk_immed) :=
    match sz with
    | SZ1 => (mcpy_inst (Pmemcpy8 IR14), mk_immed_mem_word)
    | SZ2 => (mcpy_inst (Pmemcpy16 IR14), mk_immed_mem_small)
    | SZ4 => (mcpy_inst (Pmemcpy32 IR14), mk_immed_mem_word)
    | SZ8 =>
        match Archi.expanse_memcpy_fpu, thumb tt with
        | true, _ =>
            (fun r1 r2 i1 i2 => Pmemcpyf64 r1 r2 FR7 i1 i2, mk_immed_mem_float)
        | false, true =>
            if preg_eq rad IR11
            then (mcpy_inst (Pmemcpy64 IR10 IR14), mk_immed_mem_float)
            else (mcpy_inst (Pmemcpy64 IR11 IR14), mk_immed_mem_float)
        | _, _ =>
            if preg_eq rad IR8 || preg_eq rad IR9
            then (mcpy_inst (Pmemcpy64 IR10 IR11), mk_immed_mem_small)
            else (mcpy_inst (Pmemcpy64 IR8 IR9), mk_immed_mem_small)
        end
    end in
  indexed_memcpy_access mk_instr mk_immed ras rad ofss ofsd k.

Definition transl_memcpy (sz: memcpy_typ) (bargs: list (builtin_arg mreg)) (k: bcode) :=
  match bargs with
  | ba1 :: ba2 :: nil =>
      do (ras, ofss) <- extract_memcpy_builtin_arg ba2;
      do (rad, ofsd) <- extract_memcpy_builtin_arg ba1;
      OK (select_memcpy_inst sz ras rad ofss ofsd k)
  | _ => Error (msg "extract_memcpy_builtin_arg: invalid number of builtin arguments")
  end.


Fixpoint fregs_contiguous (fl: list freg) : bool :=
  match fl with
  | nil => true
  | f1 :: tl =>
      match tl with
      | nil => true
      | f2 :: _ =>
          Z.eqb (Asm.freg_index f2) (Asm.freg_index f1 + 1)
          && fregs_contiguous tl
      end
  end.

Fixpoint store_fp_per_reg (fl: list freg) (delta: Z) (k: bcode) : bcode :=
  match fl with
  | nil => k
  | fr :: tl =>
      Pcstf Pfstd_a fr IR14 (Int.repr delta)
      ::bi store_fp_per_reg tl (delta + 8) k
  end.

Fixpoint load_fp_per_reg (fl: list freg) (delta: Z) (k: bcode) : bcode :=
  match fl with
  | nil => k
  | fr :: tl =>
      Pcldf Pfldd_a fr IR14 (Int.repr delta)
      ::bi load_fp_per_reg tl (delta + 8) k
  end.

Definition transl_savecallee (f: Machblock.function) (ofs: Z) (l: list mreg)
                              (k: bcode) : res bcode :=
  match l with
  | nil => Error (msg "Asmblockgen: transl_savecallee empty list")
  | r :: _ =>
      match mreg_type r with
      | Tany32 =>
          do il <- mmap ireg_of l;
          OK (addimm IR14 IR13 (Int.repr (align ofs 4))
               (Pcstm IR14 (map (fun ir => (ir, AST.Many32)) il) ::bi k))
      | Tany64 =>
          do fl <- mmap freg_of l;
          if fregs_contiguous fl then
            OK (addimm IR14 IR13 (Int.repr (align ofs 8))
                 (Pcvstm IR14 (map (fun fr => (fr, AST.Many64)) fl) ::bi k))
          else
            OK (addimm IR14 IR13 (Int.repr (align ofs 8))
                 (store_fp_per_reg fl 0 k))
      | _ => Error (msg "Asmblockgen: transl_savecallee bad reg type")
      end
  end.

Definition transl_restorecallee (f: Machblock.function) (ofs: Z) (l: list mreg)
                                 (k: bcode) : res bcode :=
  match l with
  | nil => Error (msg "Asmblockgen: transl_restorecallee empty list")
  | r :: _ =>
      match mreg_type r with
      | Tany32 =>
          do il <- mmap ireg_of l;
          OK (addimm IR14 IR13 (Int.repr (align ofs 4))
               (Pcldm IR14 (map (fun ir => (ir, AST.Many32)) il) ::bi k))
      | Tany64 =>
          do fl <- mmap freg_of l;
          if fregs_contiguous fl then
            OK (addimm IR14 IR13 (Int.repr (align ofs 8))
                 (Pcvldm IR14 (map (fun fr => (fr, AST.Many64)) fl) ::bi k))
          else
            OK (addimm IR14 IR13 (Int.repr (align ofs 8))
                 (load_fp_per_reg fl 0 k))
      | _ => Error (msg "Asmblockgen: transl_restorecallee bad reg type")
      end
  end.


Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
                              (r12_is_parent: bool) (k: bcode) :=
  match i with
  | MBgetstack ofs ty dst =>
      loadind IR13 ofs ty dst k
  | MBsetstack src ofs ty =>
      storeind src IR13 ofs ty k
  | MBgetparam ofs ty dst =>
      do c <- loadind IR12 ofs ty dst k;
      OK (if r12_is_parent
          then c
          else loadind_int IR13 f.(fn_link_ofs) IR12 c)
  | MBop op args res =>
      transl_op op args res k
  | MBload trap chunk addr args dst =>
      transl_load trap chunk addr args dst k
  | MBstore chunk addr args src =>
      transl_store chunk addr args src k
  | MBmemcpy sz bargs =>
      transl_memcpy sz bargs k
  | MBsavecallee ofs l =>
      transl_savecallee f ofs l k
  | MBrestorecallee ofs l =>
      transl_restorecallee f ofs l k
  end.


Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
  match i with
  | MBsetstack src ofs ty => before
  | MBgetparam ofs ty dst => negb (mreg_eq dst R12)
  | MBop Omove args res => before && negb (mreg_eq res R12)
  | _ => 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 false ::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.

Definition make_epilogue (f: Machblock.function) : bcode :=
  let freeframe := Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::bi nil in
  if optim_leaf tt && function_preserves_IR14 f then
    freeframe
  else
    loadind_int SP f.(fn_retaddr_ofs) RA freeframe.

Definition is_low_ireg (r: ireg) : bool :=
  match r with
  | IR0 | IR1 | IR2 | IR3 | IR4 | IR5 | IR6 | IR7 => true
  | _ => false
  end.

Definition is_near_label (lbl : label) (near_labels : list (label * Z)) :=
  existsb (fun (x : label * Z) => let (l, _) := x in peq lbl l) near_labels.

Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (near_labels : list (label * Z)) : res (bcode * control) :=
  match cond, args with
  | Ccompimm Ceq n, a1 :: nil | Ccompuimm Ceq n, a1 :: nil =>
      if Compopts.thumb tt && Compopts.short_branches tt
      && Int.eq n Int.zero && is_near_label lbl near_labels
      then do r1 <- ireg_of a1;
           if is_low_ireg r1
           then OK (Pnop false :: nil, PCtlFlow (Pcbz r1 lbl))
           else do ccode <- transl_cond cond args nil;
                OK (ccode, PCtlFlow (Pbc (cond_for_cond cond) lbl))
      else do ccode <- transl_cond cond args nil;
           OK (ccode, PCtlFlow (Pbc (cond_for_cond cond) lbl))
  | Ccompimm Cne n, a1 :: nil | Ccompuimm Cne n, a1 :: nil =>
      if Compopts.thumb tt && Compopts.short_branches tt
      && Int.eq n Int.zero && is_near_label lbl near_labels
      then do r1 <- ireg_of a1;
           if is_low_ireg r1
           then OK (Pnop false :: nil, PCtlFlow (Pcbnz r1 lbl))
           else do ccode <- transl_cond cond args nil;
                OK (ccode, PCtlFlow (Pbc (cond_for_cond cond) lbl))
      else do ccode <- transl_cond cond args nil;
           OK (ccode, PCtlFlow (Pbc (cond_for_cond cond) lbl))
  | _, _ =>
      do ccode <- transl_cond cond args nil;
      OK (ccode, PCtlFlow (Pbc (cond_for_cond cond) lbl))
  end.

Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (near_labels : list (label * Z)) : res (bcode * control) :=
  match ctl with
  | MBcall sig (inl arg) =>
      do r <- ireg_of arg;
      OK (nil, PCtlFlow (Pblreg r sig))
  | MBcall sig (inr symb) =>
      OK (nil, PCtlFlow (Pblsymb symb sig))
  | MBtailcall sig (inl arg) =>
      do r <- ireg_of arg;
      OK (make_epilogue f, PCtlFlow (Pbreg r sig))
  | MBtailcall sig (inr symb) =>
      OK (make_epilogue f, PCtlFlow (Pbsymb symb 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 <- transl_cbranch cond args lbl near_labels;
      OK bc
  | MBreturn =>
      OK (make_epilogue f, PCtlFlow (Pbreg RA f.(Machblock.fn_sig)))
  | 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) (near_labels : list (label * Z)) : res (bcode*option control) :=
  match ext with
    Some ctl => do (b,c) <- transl_control f ctl near_labels; OK (b, Some c)
  | None => OK (nil, None)
  end.

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

Definition near_label_thresh := 126.

Fixpoint bump_near_labels bump (l : list (label * Z)) :=
  match l with
  | nil => nil
  | (hl, hdist)::t => let hdist' := bump + hdist in
            if hdist' >=? near_label_thresh
            then nil
            else (hl,hdist') :: bump_near_labels bump t
  end.

Definition is_low_dreg (r: dreg) : bool :=
  match r with
  | IR ir => is_low_ireg ir
  | FR _ => false
  end.

Definition thumb_size_mov (rd: ireg) (so: shift_op) : Z :=
  match so with
  | SOreg _ => 2
  | SOimm n => if is_low_ireg rd && Int.ltu n (Int.repr 256) then 2 else 4
  | _ => 4
  end.

Definition thumb_size_arith (i: ar_instruction) : Z :=
  match i with
  | PArithRO Pmov rd (SOreg rs) => 2
  | PArithRO Pmvn rd (SOreg rs) =>
      if is_low_ireg rd && is_low_ireg rs then 2 else 4
  | PArithRRO Padd rd rn (SOreg rm) =>
      if is_low_ireg rd && is_low_ireg rn && is_low_ireg rm then 2
      else if ireg_eq rd rn then 2
      else 4
  | PArithRRO Psub rd rn (SOreg rm) =>
      if is_low_ireg rd && is_low_ireg rn && is_low_ireg rm then 2 else 4
  | PArithRRO Padd rd rn (SOimm n) =>
      if is_low_ireg rd && is_low_ireg rn && Int.ltu n (Int.repr 256) then 2 else 4
  | PArithRRO Psub rd rn (SOimm n) =>
      if is_low_ireg rd && is_low_ireg rn && Int.ltu n (Int.repr 256) then 2 else 4
  | PArithRRO Pand rd _ (SOreg rm) =>
      if is_low_ireg rd && is_low_ireg rm then 2 else 4
  | PArithRRO Peor rd _ (SOreg rm) =>
      if is_low_ireg rd && is_low_ireg rm then 2 else 4
  | PArithRRO Porr rd _ (SOreg rm) =>
      if is_low_ireg rd && is_low_ireg rm then 2 else 4
  | PArithRRO Pbic rd _ (SOreg rm) =>
      if is_low_ireg rd && is_low_ireg rm then 2 else 4
  | PArithRRO Prsb rd rn (SOimm n) =>
      if is_low_ireg rd && is_low_ireg rn && Int.eq n Int.zero then 2 else 4
  | PArithComparisonRO Pcmp rn (SOreg rm) => 2
  | PArithComparisonRO Pcmn rn (SOreg rm) =>
      if is_low_ireg rn && is_low_ireg rm then 2 else 4
  | PArithComparisonRO Pcmp rn (SOimm n) =>
      if is_low_ireg rn && Int.ltu n (Int.repr 256) then 2 else 4
  | PArithPPP Plsl rd r1 r2 => if is_low_dreg rd && is_low_dreg r1 then 2 else 4
  | PArithPPP Plsr rd r1 r2 => if is_low_dreg rd && is_low_dreg r1 then 2 else 4
  | PArithPPP Pasr rd r1 r2 => if is_low_dreg rd && is_low_dreg r1 then 2 else 4
  | PArithPPP Pror rd r1 r2 => if is_low_dreg rd && is_low_dreg r1 then 2 else 4
  | PArithPP Puxtb rd rs => if is_low_dreg rd && is_low_dreg rs then 2 else 4
  | PArithPP Psxtb rd rs => if is_low_dreg rd && is_low_dreg rs then 2 else 4
  | PArithPP Puxth rd rs => if is_low_dreg rd && is_low_dreg rs then 2 else 4
  | PArithPP Psxth rd rs => if is_low_dreg rd && is_low_dreg rs then 2 else 4
  | PArithPPP Pmul rd r1 r2 => if is_low_dreg rd && is_low_dreg r1 && is_low_dreg r2 then 2 else 4
  | PArithComparisonFF _ _ _ => 8
  | PArithComparisonF _ _ => 8
  | PArithPP Pfsitod _ _ => 8
  | PArithPP Pfuitod _ _ => 8
  | PArithPP Pfsitos _ _ => 8
  | PArithPP Pfuitos _ _ => 8
  | Pftosizd _ _ => 8
  | Pftouizd _ _ => 8
  | Pftosizs _ _ => 8
  | Pftouizs _ _ => 8
  | Pmovite _ rd o1 o2 =>
      if shift_op_eq (SOreg rd) o1 then 2 + thumb_size_mov rd o2
      else 2 + thumb_size_mov rd o1 + thumb_size_mov rd o2
  | Pfmovite _ rd r1 _ =>
      if freg_eq rd r1 then 6 else 10
  | _ => 4
  end.

Definition thumb_size_load (ld: ld_instruction) : Z :=
  match ld with
  | Pcldi _ rd ra (SOreg rm) =>
      if is_low_ireg rd && is_low_ireg ra && is_low_ireg rm then 2 else 4
  | Pcldi (Pldr | Pldr_a) rd IR13 (SOimm n) =>
      if is_low_ireg rd && Int.eq (Int.and n (Int.repr 3)) Int.zero
         && Int.ltu n (Int.repr 1024) then 2 else 4
  | Pcldi (Pldr | Pldr_a) rd ra (SOimm n) =>
      if is_low_ireg rd && is_low_ireg ra && Int.ltu n (Int.repr 128) then 2 else 4
  | Pcldi Pldrb rd ra (SOimm n) =>
      if is_low_ireg rd && is_low_ireg ra && Int.ltu n (Int.repr 32) then 2 else 4
  | Pcldi Pldrh rd ra (SOimm n) =>
      if is_low_ireg rd && is_low_ireg ra && Int.ltu n (Int.repr 64) then 2 else 4
  | _ => 4
  end.

Definition thumb_size_store (st: st_instruction) : Z :=
  match st with
  | Pcsti _ rs ra (SOreg rm) =>
      if is_low_ireg rs && is_low_ireg ra && is_low_ireg rm then 2 else 4
  | Pcsti (Pstr | Pstr_a) rs IR13 (SOimm n) =>
      if is_low_ireg rs && Int.eq (Int.and n (Int.repr 3)) Int.zero
         && Int.ltu n (Int.repr 1024) then 2 else 4
  | Pcsti (Pstr | Pstr_a) rs ra (SOimm n) =>
      if is_low_ireg rs && is_low_ireg ra && Int.ltu n (Int.repr 128) then 2 else 4
  | Pcsti Pstrb rs ra (SOimm n) =>
      if is_low_ireg rs && is_low_ireg ra && Int.ltu n (Int.repr 32) then 2 else 4
  | Pcsti Pstrh rs ra (SOimm n) =>
      if is_low_ireg rs && is_low_ireg ra && Int.ltu n (Int.repr 64) then 2 else 4
  | _ => 4
  end.

Definition thumb_size_basic (x : basic) : Z :=
  match x with
  | Pnop false => 0
  | Pnop true => 2
  | Pcfi_rel_offset _ => 0
  | PArith i => thumb_size_arith i
  | PLoad ld => thumb_size_load ld
  | PStore st => thumb_size_store st
  | PMemcpy _ _ _ _ _ => 8
  | Pmemcpyf64 _ _ _ _ _ => 8
  | Pallocframe _ _ => 24
  | Pfreeframe _ _ => 16
  | Ploadsymbol _ _ _ => 8
  | Psdiv _ _ _ => 4
  | Pudiv _ _ _ => 4
  end.

Fixpoint count_fp_xtypes (xtl : list xtype) : Z :=
  match xtl with
  | nil => 0
  | x :: rest =>
      match x with
      | Xfloat | Xsingle | Xany64 => 1 + count_fp_xtypes rest
      | _ => count_fp_xtypes rest
      end
  end.

Definition fixup_args_size (sg : signature) : Z :=
  4 * count_fp_xtypes sg.(sig_args).

Definition fixup_result_size (sg : signature) : Z :=
  match sg.(sig_res) with
  | Xfloat | Xsingle | Xany64 => 4
  | _ => 0
  end.

Definition thumb_size_exit (x : control) : Z :=
  match x with
  | PCtlFlow (Pcbz _ _) => 2
  | PCtlFlow (Pcbnz _ _) => 2
  | PCtlFlow (Pb _) => 4
  | PCtlFlow (Pbc _ _) => 4
  | PCtlFlow (Pbtbl _ tbl) => 4 + 2 * Z.of_nat (List.length tbl)
  | PCtlFlow (Pbreg _ sg) => 2 + Z.max (fixup_args_size sg) (fixup_result_size sg)
  | PCtlFlow (Pblreg _ sg) => 4 + fixup_args_size sg + fixup_result_size sg
  | PCtlFlow (Pbsymb _ sg) => 4 + fixup_args_size sg
  | PCtlFlow (Pblsymb _ sg) => 4 + fixup_args_size sg + fixup_result_size sg
  | Pbuiltin _ _ _ => 64
  end.

Definition thumb_size_block (lb : bblock) :=
  (List.fold_left (fun x y => x + thumb_size_basic y) (body lb) 0) +
    (match exit lb with
     | None => 0
     | Some x => thumb_size_exit x
    end).

Definition thumb_size_blocks (lbs : list bblock) :=
  List.fold_left (fun x y => x + thumb_size_block y) lbs 0.

Definition pool_size_basic (x : basic) : Z :=
  match x with
  | PArith (Pflid _ _) => 8
  | PArith (PArithP (Pflis _) _) => 4
  | Ploadsymbol _ _ _ => 4
  | _ => 0
  end.

Definition pool_size_exit (cap : Z) (x : control) : Z :=
  match x with
  | Pbuiltin _ _ _ => 4
  | PCtlFlow (Pb _) => cap
  | PCtlFlow (Pbsymb _ _) => cap
  | PCtlFlow (Pbreg _ _) => cap
  | _ => 0
  end.

Definition pool_size_block (cap : Z) (lb : bblock) : Z :=
  (List.fold_left (fun x y => x + pool_size_basic y) (body lb) 0) +
    (match exit lb with
     | None => 0
     | Some x => pool_size_exit cap x
    end).

Definition pool_size_blocks (cap : Z) (lbs : list bblock) : Z :=
  List.fold_left (fun x y => x + pool_size_block cap y) lbs 0.



Definition oaddrsymbol_uses_pool (ofs : ptrofs) : bool :=
  if andb Archi.thumb2_support (negb (Compopts.optim_for_size tt)) then
    let o := Ptrofs.signed ofs in
    negb (andb (Z.leb (-32768) o) (Z.leb o 32767))
  else true.

Definition ofloatconst_uses_pool (f : float) : bool :=
  if andb (Compopts.optim_double_zero_via_int tt) (Float.eq_dec f Float.zero)
  then false
  else if andb Archi.vfpv3 (is_immediate_float64 f)
  then false
  else true.

Definition osingleconst_uses_pool (f : float32) : bool :=
  if andb (Compopts.optim_single_zero_via_int tt) (Float32.eq_dec f Float32.zero)
  then false
  else if andb Archi.vfpv3 (is_immediate_float32 f)
  then false
  else true.

Definition pool_size_mach_basic (b : Machblock.basic_inst) : Z :=
  match b with
  | MBop op _ _ =>
      match op with
      | Ofloatconst f => if ofloatconst_uses_pool f then 8 else 0
      | Osingleconst f => if osingleconst_uses_pool f then 4 else 0
      | Oaddrsymbol _ ofs => if oaddrsymbol_uses_pool ofs then 4 else 0
      | _ => 0
      end
  | _ => 0
  end.

Definition pool_size_mach_exit (e : option Machblock.control_flow_inst) : Z :=
  match e with
  | Some (MBbuiltin _ _ _) => 4
  | _ => 0
  end.

Definition pool_size_machblock (b : Machblock.bblock) : Z :=
  List.fold_left (fun a bi => a + pool_size_mach_basic bi) (Machblock.body b) 0
    + pool_size_mach_exit (Machblock.exit b).

Definition pool_size_machblocks (lb : list Machblock.bblock) : Z :=
  List.fold_left (fun a b => a + pool_size_machblock b) lb 0.

Definition pool_cap (f : Machblock.function) : Z :=
  Z.min 1024 (pool_size_machblocks f.(Machblock.fn_code)).

Fixpoint transl_blocks0 (f: Machblock.function) (cap: Z) (lmb: list Machblock.bblock) (ep: bool) (near_labels: list (label * Z.t)) : res ((list bblock) * list (label * Z.t)):=
  match lmb with
  | nil => OK (nil, near_labels)
  | mb :: lmb =>
      do lbx' <- transl_blocks0 f cap lmb false near_labels;
      let (lb', near_labels') := lbx' in
      do lb <- transl_block f mb (if Machblock.header mb then ep else false) near_labels';
      let near_labels'' :=
        bump_near_labels
          (thumb_size_blocks lb + pool_size_blocks cap lb) near_labels' in
      OK ((lb @@ lb'),
          ((List.map (fun x => (x, 0)) (Machblock.header mb)) @@ near_labels''))
  end.

Definition transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) : res (list bblock) :=
  do lbx' <- transl_blocks0 f (pool_cap f) lmb ep nil;
  let (lb', near_labels') := lbx' in OK lb'.

Program Definition make_prologue (f: Machblock.function) (lb: bblocks) :=
  {| header := nil; body :=
      Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::bi
      save_lr f.(fn_retaddr_ofs)
        (Pcfi_rel_offset (Ptrofs.to_int f.(fn_retaddr_ofs)) ::bi nil);
        exit := None |} :: lb.

Definition transl_function (f: Machblock.function): res Asmblock.function :=
  do lb <- transl_blocks f f.(Machblock.fn_code) (save_lr_preserves_R12 f.(fn_retaddr_ofs));
  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.