path: root/arm/Asmgen.v

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Translation from Mach to ARM. *)

Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Import Mach.
Require Import Asm.

(** Recognition of integer immediate arguments.
- For arithmetic operations, immediates are
  8-bit quantities zero-extended and rotated right by 0, 2, 4, ... 30 bits.
- For memory accesses of type [Mint32], immediate offsets are
  12-bit quantities plus a sign bit.
- For other memory accesses, immediate offsets are
  8-bit quantities plus a sign bit. *)

Fixpoint is_immed_arith_aux (n: nat) (x msk: int) {struct n}: bool :=
  match n with
  | Datatypes.O => false
  | Datatypes.S n' =>
      Int.eq (Int.and x (Int.not msk)) Int.zero ||
      is_immed_arith_aux n' x (Int.ror msk (Int.repr 2))
  end.

Definition is_immed_arith (x: int) : bool :=
  is_immed_arith_aux 16%nat x (Int.repr 255).

Definition is_immed_mem_word (x: int) : bool :=
  Int.lt x (Int.repr 4096) && Int.lt (Int.repr (-4096)) x.
  
Definition is_immed_mem_small (x: int) : bool :=
  Int.lt x (Int.repr 256) && Int.lt (Int.repr (-256)) x.
  
Definition is_immed_mem_float (x: int) : bool :=
  Int.eq (Int.and x (Int.repr 3)) Int.zero
  && Int.lt x (Int.repr 1024) && Int.lt (Int.repr (-1024)) x.
  
(** Decomposition of a 32-bit integer into a list of immediate arguments,
    whose sum or "or" or "xor" equals the integer. *)

Fixpoint decompose_int_rec (N: nat) (n p: int) : list int :=
  match N with
  | Datatypes.O =>
      if Int.eq_dec n Int.zero then nil else n :: nil
  | Datatypes.S M =>
      if Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then
        decompose_int_rec M n (Int.add p (Int.repr 2))
      else
        let m := Int.shl (Int.repr 255) p in
        Int.and n m ::
        decompose_int_rec M (Int.and n (Int.not m)) (Int.add p (Int.repr 2))
  end.

Definition decompose_int (n: int) : list int :=
  match decompose_int_rec 12%nat n Int.zero with
  | nil => Int.zero :: nil
  | l   => l
  end.

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

(** Smart constructors for integer immediate arguments. *)

Definition loadimm (r: ireg) (n: int) (k: code) :=
  let d1 := decompose_int n in
  let d2 := decompose_int (Int.not n) in
  if le_dec (List.length d1) (List.length d2)
  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: code) :=
  let d1 := decompose_int n in
  let d2 := decompose_int (Int.neg n) in
  if le_dec (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 andimm (r1 r2: ireg) (n: int) (k: code) :=
  if is_immed_arith n 
  then Pand r1 r2 (SOimm n) :: k
  else iterate_op (Pbic r1 r2) (Pbic r1 r1) (decompose_int (Int.not n)) k.

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

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

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

(** Translation of a shift immediate operation (type [Op.shift]) *)

Definition transl_shift (s: shift) (r: ireg) : shift_op :=
  match s with
  | Slsl n => SOlslimm r (s_amount n)
  | Slsr n => SOlsrimm r (s_amount n)
  | Sasr n => SOasrimm r (s_amount n)
  | Sror n => SOrorimm r (s_amount n)
  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: code) :=
  match cond, args with
  | Ccomp c, a1 :: a2 :: nil =>
      Pcmp (ireg_of a1) (SOreg (ireg_of a2)) :: k
  | Ccompu c, a1 :: a2 :: nil =>
      Pcmp (ireg_of a1) (SOreg (ireg_of a2)) :: k
  | Ccompshift c s, a1 :: a2 :: nil =>
      Pcmp (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
  | Ccompushift c s, a1 :: a2 :: nil =>
      Pcmp (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
  | Ccompimm c n, a1 :: nil =>
      if is_immed_arith n then
        Pcmp (ireg_of a1) (SOimm n) :: k
      else
        loadimm IR14 n (Pcmp (ireg_of a1) (SOreg IR14) :: k)
  | Ccompuimm c n, a1 :: nil =>
      if is_immed_arith n then
        Pcmp (ireg_of a1) (SOimm n) :: k
      else
        loadimm IR14 n (Pcmp (ireg_of a1) (SOreg IR14) :: k)
  | Ccompf cmp, a1 :: a2 :: nil =>
      Pfcmpd (freg_of a1) (freg_of a2) :: k
  | Cnotcompf cmp, a1 :: a2 :: nil =>
      Pfcmpd (freg_of a1) (freg_of a2) :: k
  | _, _ =>
     k (**r never happens for well-typed code *)
  end.

Definition crbit_for_signed_cmp (cmp: comparison) :=
  match cmp with
  | Ceq => CReq
  | Cne => CRne
  | Clt => CRlt
  | Cle => CRle
  | Cgt => CRgt
  | Cge => CRge
  end.

Definition crbit_for_unsigned_cmp (cmp: comparison) :=
  match cmp with
  | Ceq => CReq
  | Cne => CRne
  | Clt => CRlo
  | Cle => CRls
  | Cgt => CRhi
  | Cge => CRhs
  end.

Definition crbit_for_float_cmp (cmp: comparison) :=
  match cmp with
  | Ceq => CReq
  | Cne => CRne
  | Clt => CRmi
  | Cle => CRls
  | Cgt => CRgt
  | Cge => CRge
  end.

Definition crbit_for_float_not_cmp (cmp: comparison) :=
  match cmp with
  | Ceq => CRne
  | Cne => CReq
  | Clt => CRpl
  | Cle => CRhi
  | Cgt => CRle
  | Cge => CRlt
  end.

Definition crbit_for_cond (cond: condition) :=
  match cond with
  | Ccomp cmp => crbit_for_signed_cmp cmp
  | Ccompu cmp => crbit_for_unsigned_cmp cmp
  | Ccompshift cmp s => crbit_for_signed_cmp cmp
  | Ccompushift cmp s => crbit_for_unsigned_cmp cmp
  | Ccompimm cmp n => crbit_for_signed_cmp cmp
  | Ccompuimm cmp n => crbit_for_unsigned_cmp cmp
  | Ccompf cmp => crbit_for_float_cmp cmp
  | Cnotcompf cmp => crbit_for_float_not_cmp cmp
  end.

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

Definition transl_op
              (op: operation) (args: list mreg) (r: mreg) (k: code) :=
  match op, args with
  | Omove, a1 :: nil =>
      match mreg_type a1 with
      | Tint => Pmov (ireg_of r) (SOreg (ireg_of a1)) :: k
      | Tfloat => Pfcpyd (freg_of r) (freg_of a1) :: k
      end
  | Ointconst n, nil =>
      loadimm (ireg_of r) n k
  | Ofloatconst f, nil =>
      Pflid (freg_of r) f :: k
  | Oaddrsymbol s ofs, nil =>
      Ploadsymbol (ireg_of r) s ofs :: k
  | Oaddrstack n, nil =>
      addimm (ireg_of r) IR13 n k
  | Ocast8signed, a1 :: nil =>
      Pmov (ireg_of r) (SOlslimm (ireg_of a1) (Int.repr 24)) ::
      Pmov (ireg_of r) (SOasrimm (ireg_of r) (Int.repr 24)) :: k
  | Ocast8unsigned, a1 :: nil =>
      Pand (ireg_of r) (ireg_of a1) (SOimm (Int.repr 255)) :: k
  | Ocast16signed, a1 :: nil =>
      Pmov (ireg_of r) (SOlslimm (ireg_of a1) (Int.repr 16)) ::
      Pmov (ireg_of r) (SOasrimm (ireg_of r) (Int.repr 16)) :: k
  | Ocast16unsigned, a1 :: nil =>
      Pmov (ireg_of r) (SOlslimm (ireg_of a1) (Int.repr 16)) ::
      Pmov (ireg_of r) (SOlsrimm (ireg_of r) (Int.repr 16)) :: k
  | Oadd, a1 :: a2 :: nil =>
      Padd (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
  | Oaddshift s, a1 :: a2 :: nil =>
      Padd (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
  | Oaddimm n, a1 :: nil =>
      addimm (ireg_of r) (ireg_of a1) n k
  | Osub, a1 :: a2 :: nil =>
      Psub (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
  | Osubshift s, a1 :: a2 :: nil =>
      Psub (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
  | Orsubshift s, a1 :: a2 :: nil =>
      Prsb (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
  | Orsubimm n, a1 :: nil =>
      rsubimm (ireg_of r) (ireg_of a1) n k
  | Omul, a1 :: a2 :: nil =>
      if ireg_eq (ireg_of r) (ireg_of a1)
      || ireg_eq (ireg_of r) (ireg_of a2)
      then Pmul IR14 (ireg_of a1) (ireg_of a2) :: Pmov (ireg_of r) (SOreg IR14) :: k
      else Pmul (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
  | Odiv, a1 :: a2 :: nil =>
      Psdiv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
  | Odivu, a1 :: a2 :: nil =>
      Pudiv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
  | Oand, a1 :: a2 :: nil =>
      Pand (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
  | Oandshift s, a1 :: a2 :: nil =>
      Pand (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
  | Oandimm n, a1 :: nil =>
      andimm (ireg_of r) (ireg_of a1) n k
  | Oor, a1 :: a2 :: nil =>
      Porr (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
  | Oorshift s, a1 :: a2 :: nil =>
      Porr (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
  | Oorimm n, a1 :: nil =>
      orimm (ireg_of r) (ireg_of a1) n k
  | Oxor, a1 :: a2 :: nil =>
      Peor (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
  | Oxorshift s, a1 :: a2 :: nil =>
      Peor (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
  | Oxorimm n, a1 :: nil =>
      xorimm (ireg_of r) (ireg_of a1) n k
  | Obic, a1 :: a2 :: nil =>
      Pbic (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
  | Obicshift s, a1 :: a2 :: nil =>
      Pbic (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
  | Onot, a1 :: nil =>
      Pmvn (ireg_of r) (SOreg (ireg_of a1)) :: k
  | Onotshift s, a1 :: nil =>
      Pmvn (ireg_of r) (transl_shift s (ireg_of a1)) :: k
  | Oshl, a1 :: a2 :: nil =>
      Pmov (ireg_of r) (SOlslreg (ireg_of a1) (ireg_of a2)) :: k
  | Oshr, a1 :: a2 :: nil =>
      Pmov (ireg_of r) (SOasrreg (ireg_of a1) (ireg_of a2)) :: k
  | Oshru, a1 :: a2 :: nil =>
      Pmov (ireg_of r) (SOlsrreg (ireg_of a1) (ireg_of a2)) :: k
  | Oshift s, a1 :: nil =>
      Pmov (ireg_of r) (transl_shift s (ireg_of a1)) :: k
  | Oshrximm n, a1 :: nil =>
      Pcmp (ireg_of a1) (SOimm Int.zero) ::
      addimm IR14 (ireg_of a1) (Int.sub (Int.shl Int.one n) Int.one)
         (Pmovc CRge IR14 (SOreg (ireg_of a1)) ::
          Pmov (ireg_of r) (SOasrimm IR14 n) :: k)
  | Onegf, a1 :: nil =>
      Pfnegd (freg_of r) (freg_of a1) :: k
  | Oabsf, a1 :: nil =>
      Pfabsd (freg_of r) (freg_of a1) :: k
  | Oaddf, a1 :: a2 :: nil =>
      Pfaddd (freg_of r) (freg_of a1) (freg_of a2) :: k
  | Osubf, a1 :: a2 :: nil =>
      Pfsubd (freg_of r) (freg_of a1) (freg_of a2) :: k
  | Omulf, a1 :: a2 :: nil =>
      Pfmuld (freg_of r) (freg_of a1) (freg_of a2) :: k
  | Odivf, a1 :: a2 :: nil =>
      Pfdivd (freg_of r) (freg_of a1) (freg_of a2) :: k
  | Osingleoffloat, a1 :: nil =>
      Pfcvtsd (freg_of r) (freg_of a1) :: k
  | Ointoffloat, a1 :: nil =>
      Pftosizd (ireg_of r) (freg_of a1) :: k
  | Ointuoffloat, a1 :: nil =>
      Pftouizd (ireg_of r) (freg_of a1) :: k
  | Ofloatofint, a1 :: nil =>
      Pfsitod (freg_of r) (ireg_of a1) :: k
  | Ofloatofintu, a1 :: nil =>
      Pfuitod (freg_of r) (ireg_of a1) :: k
  | Ocmp cmp, _ =>
      transl_cond cmp args
        (Pmov (ireg_of r) (SOimm Int.zero) ::
         Pmovc (crbit_for_cond cmp) (ireg_of r) (SOimm Int.one) ::
         k)
  | _, _ =>
      k (**r never happens for well-typed code *)
  end.

(** Common code to translate [Mload] and [Mstore] instructions. *)

Definition transl_shift_addr (s: shift) (r: ireg) : shift_addr :=
  match s with
  | Slsl n => SAlsl r (s_amount n)
  | Slsr n => SAlsr r (s_amount n)
  | Sasr n => SAasr r (s_amount n)
  | Sror n => SAror r (s_amount n)
  end.

Definition transl_load_store
     (mk_instr_imm: ireg -> int -> instruction)
     (mk_instr_gen: option (ireg -> shift_addr -> instruction))
     (is_immed: int -> bool)
     (addr: addressing) (args: list mreg) (k: code) : code :=
  match addr, args with
  | Aindexed n, a1 :: nil =>
      if is_immed n then
        mk_instr_imm (ireg_of a1) n :: k
      else
        addimm IR14 (ireg_of a1) n
          (mk_instr_imm IR14 Int.zero :: k)
  | Aindexed2, a1 :: a2 :: nil =>
      match mk_instr_gen with
      | Some f =>
          f (ireg_of a1) (SAreg (ireg_of a2)) :: k
      | None =>
          Padd IR14 (ireg_of a1) (SOreg (ireg_of a2)) ::
          mk_instr_imm IR14 Int.zero :: k
      end
  | Aindexed2shift s, a1 :: a2 :: nil =>
      match mk_instr_gen with
      | Some f =>
          f (ireg_of a1) (transl_shift_addr s (ireg_of a2)) :: k
      | None =>
          Padd IR14 (ireg_of a1) (transl_shift s (ireg_of a2)) ::
          mk_instr_imm IR14 Int.zero :: k
      end
  | Ainstack n, nil =>
      if is_immed n then
        mk_instr_imm IR13 n :: k
      else
        addimm IR14 IR13 n
          (mk_instr_imm IR14 Int.zero :: k)
  | _, _ =>
      (* should not happen *) k
  end.

Definition transl_load_store_int
     (mk_instr: ireg -> ireg -> shift_addr -> instruction)
     (is_immed: int -> bool)
     (rd: mreg) (addr: addressing) (args: list mreg) (k: code) :=
  transl_load_store
    (fun r n => mk_instr (ireg_of rd) r (SAimm n))
    (Some (mk_instr (ireg_of rd)))
    is_immed addr args k.

Definition transl_load_store_float
     (mk_instr: freg -> ireg -> int -> instruction)
     (is_immed: int -> bool)
     (rd: mreg) (addr: addressing) (args: list mreg) (k: code) :=
  transl_load_store
    (mk_instr (freg_of rd))
    None
    is_immed addr args k.

Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) :=
  if is_immed_mem_word ofs then
    Pldr dst base (SAimm ofs) :: k
  else
    addimm IR14 base ofs
      (Pldr dst IR14 (SAimm Int.zero) :: k).

Definition loadind_float (base: ireg) (ofs: int) (dst: freg) (k: code) :=
  if is_immed_mem_float ofs then
    Pfldd dst base ofs :: k
  else
    addimm IR14 base ofs
      (Pfldd dst IR14 Int.zero :: k).

Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
  match ty with
  | Tint => loadind_int base ofs (ireg_of dst) k
  | Tfloat => loadind_float base ofs (freg_of dst) k
  end.

Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) :=
  if is_immed_mem_word ofs then
    Pstr src base (SAimm ofs) :: k
  else
    addimm IR14 base ofs
      (Pstr src IR14 (SAimm Int.zero) :: k).

Definition storeind_float (src: freg) (base: ireg) (ofs: int) (k: code) :=
  if is_immed_mem_float ofs then
    Pfstd src base ofs :: k
  else
    addimm IR14 base ofs
      (Pfstd src IR14 Int.zero :: k).

Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
  match ty with
  | Tint => storeind_int (ireg_of src) base ofs k
  | Tfloat => storeind_float (freg_of src) base ofs k
  end.

(** Translation of arguments to annotations *)

Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param :=
  match p with
  | Mach.APreg r => APreg (preg_of r)
  | Mach.APstack chunk ofs => APstack chunk ofs
  end.

(** Translation of a Mach instruction. *)

Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
  match i with
  | Mgetstack ofs ty dst =>
      loadind IR13 ofs ty dst k
  | Msetstack src ofs ty =>
      storeind src IR13 ofs ty k
  | Mgetparam ofs ty dst =>
      loadind_int IR13 f.(fn_link_ofs) IR14 (loadind IR14 ofs ty dst k)
  | Mop op args res =>
      transl_op op args res k
  | Mload chunk addr args dst =>
      match chunk with
      | Mint8signed =>
          transl_load_store_int Pldrsb is_immed_mem_small dst addr args k
      | Mint8unsigned =>
          transl_load_store_int Pldrb is_immed_mem_word dst addr args k
      | Mint16signed =>
          transl_load_store_int Pldrsh is_immed_mem_small dst addr args k
      | Mint16unsigned =>
          transl_load_store_int Pldrh is_immed_mem_small dst addr args k
      | Mint32 =>
          transl_load_store_int Pldr is_immed_mem_word dst addr args k
      | Mfloat32 =>
          transl_load_store_float Pflds is_immed_mem_float dst addr args k
      | Mfloat64 =>
          transl_load_store_float Pfldd is_immed_mem_float dst addr args k
      end
  | Mstore chunk addr args src =>
      match chunk with
      | Mint8signed =>
          transl_load_store_int Pstrb is_immed_mem_small src addr args k
      | Mint8unsigned =>
          transl_load_store_int Pstrb is_immed_mem_word src addr args k
      | Mint16signed =>
          transl_load_store_int Pstrh is_immed_mem_small src addr args k
      | Mint16unsigned =>
          transl_load_store_int Pstrh is_immed_mem_small src addr args k
      | Mint32 =>
          transl_load_store_int Pstr is_immed_mem_word src addr args k
      | Mfloat32 =>
          transl_load_store_float Pfsts is_immed_mem_float src addr args k
      | Mfloat64 =>
          transl_load_store_float Pfstd is_immed_mem_float src addr args k
      end
  | Mcall sig (inl r) =>
      Pblreg (ireg_of r) sig :: k
  | Mcall sig (inr symb) =>
      Pblsymb symb sig :: k
  | Mtailcall sig (inl r) =>
      loadind_int IR13 f.(fn_retaddr_ofs) IR14
        (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg (ireg_of r) sig :: k)
  | Mtailcall sig (inr symb) =>
      loadind_int IR13 f.(fn_retaddr_ofs) IR14
        (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb sig :: k)
  | Mbuiltin ef args res =>
      Pbuiltin ef (map preg_of args) (preg_of res) :: k
  | Mannot ef args =>
      Pannot ef (map transl_annot_param args) :: k
  | Mlabel lbl =>
      Plabel lbl :: k
  | Mgoto lbl =>
      Pb lbl :: k
  | Mcond cond args lbl =>
      transl_cond cond args (Pbc (crbit_for_cond cond) lbl :: k)
  | Mjumptable arg tbl =>
      Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) ::
      Pbtbl IR14 tbl :: k
  | Mreturn =>
      loadind_int IR13 f.(fn_retaddr_ofs) IR14
        (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 f.(Mach.fn_sig) :: k)
  end.

Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
  List.fold_right (transl_instr f) nil il.

(** Translation of a whole function.  Note that we must check
  that the generated code contains less than [2^32] instructions,
  otherwise the offset part of the [PC] code pointer could wrap
  around, leading to incorrect executions. *)

Definition transl_function (f: Mach.function) :=
  mkfunction f.(Mach.fn_sig)
    (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
     Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) ::
     transl_code f f.(Mach.fn_code)).

Fixpoint code_size (c: code) : Z :=
  match c with
  | nil => 0
  | instr :: c' => code_size c' + 1
  end.

Open Local Scope string_scope.

Definition transf_function (f: Mach.function) : res Asm.function :=
  let tf := transl_function f in
  if zlt Int.max_unsigned (code_size tf.(fn_code))
  then Errors.Error (msg "code size exceeded")
  else Errors.OK tf.

Definition transf_fundef (f: Mach.fundef) : res Asm.fundef :=
  transf_partial_fundef transf_function f.

Definition transf_program (p: Mach.program) : res Asm.program :=
  transform_partial_program transf_fundef p.