Merge of the reuse-temps branch:

- Reload temporaries are marked as destroyed (set to Vundef) across
  operations in the semantics of LTL, LTLin, Linear and Mach, 
  allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 505 insertions, 0 deletions

diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
new file mode 100644
index 0000000..70929ff
--- /dev/null
+++ b/ia32/Asmgen.v
@@ -0,0 +1,505 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 IA32 Asm. *)
+
+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.
+
+Open Local Scope string_scope.
+Open Local Scope error_monad_scope.
+
+(** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the compiler:
+- Argument and result registers are of the correct type.
+- For two-address instructions, the result and the first argument
+  are in the same register.  (True by construction in [RTLgen], and preserved by [Reload].)
+- The first argument register is never [ECX] (a.k.a. [IT2]) nor [XMM7]
+  (a.k.a [FT2]).
+- The top of the floating-point stack ([ST0], a.k.a. [FP0]) can only
+  appear in [mov] instructions, but never in arithmetic instructions.
+
+All these properties are true by construction, but it is painful to track them statically.  Instead, we recheck them during code generation and fail if they do not hold.
+*)
+
+(** Extracting integer or float registers. *)
+
+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.
+
+(** Smart constructors for various operations. *)
+
+Definition mk_mov (rd rs: preg) (k: code) : res code :=
+  match rd, rs with
+  | IR rd, IR rs => OK (Pmov_rr rd rs :: k)
+  | FR rd, FR rs => OK (Pmovsd_ff rd rs :: k)
+  | ST0, FR rs => OK (Pfld_f rs :: k)
+  | FR rd, ST0 => OK (Pfstp_f rd :: k)
+  | _, _ => Error(msg "Asmgen.mk_mov")
+  end.
+
+Definition mk_shift (shift_instr: ireg -> instruction)
+                    (r1 r2: ireg) (k: code) : res code :=
+  if ireg_eq r2 ECX then
+    OK (shift_instr r1 :: k)
+  else
+    do x <- assertion (negb (ireg_eq r1 ECX));
+    OK (Pmov_rr ECX r2 :: shift_instr r1 :: k).
+
+Definition mk_div (div_instr: ireg -> instruction)
+                  (r1 r2: ireg) (k: code) : res code :=
+  if ireg_eq r1 EAX then
+    if ireg_eq r2 EDX then
+      OK (Pmov_rr ECX EDX :: div_instr ECX :: k)
+    else
+      OK (div_instr r2 :: k)
+  else
+    do x <- assertion (negb (ireg_eq r1 ECX));
+    if ireg_eq r2 EAX then
+      OK (Pmov_rr ECX EAX :: Pmov_rr EAX r1 ::
+          div_instr ECX ::
+          Pmov_rr r1 EAX :: Pmov_rr EAX ECX :: k)
+    else
+      OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX r2 :: Pmov_rr EAX r1 ::
+          div_instr ECX ::
+          Pmov_rr r2 ECX :: Pmov_rr r1 EAX :: Pmovd_rf EAX XMM7 :: k).
+
+Definition mk_mod (div_instr: ireg -> instruction)
+                  (r1 r2: ireg) (k: code) : res code :=
+  if ireg_eq r1 EAX then
+    if ireg_eq r2 EDX then
+      OK (Pmov_rr ECX EDX :: div_instr ECX :: Pmov_rr EAX EDX :: k)
+    else
+      OK (div_instr r2 :: Pmov_rr EAX EDX :: k)
+  else
+    do x <- assertion (negb (ireg_eq r1 ECX));
+    if ireg_eq r2 EDX then
+      OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX EDX :: Pmov_rr EAX r1 ::
+          div_instr ECX ::
+          Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k)
+    else
+      OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX r2 :: Pmov_rr EAX r1 ::
+          div_instr ECX ::
+          Pmov_rr r2 ECX :: Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k).
+
+Definition mk_shrximm (r: ireg) (n: int) (k: code) : res code :=
+  do x <- assertion (negb (ireg_eq r ECX));
+  let p := Int.sub (Int.shl Int.one n) Int.one in
+  OK (Ptest_rr r r ::
+      Plea ECX (Addrmode (Some r) None (inl _ p)) ::
+      Pcmov Cond_l r ECX ::
+      Psar_ri r n :: k).
+
+Definition low_ireg (r: ireg) : bool :=
+  match r with
+  | EAX | EBX | ECX | EDX => true
+  | ESI | EDI | EBP | ESP => false
+  end.
+
+Definition mk_intconv (mk: ireg -> ireg -> instruction) (rd rs: ireg) (k: code) :=
+  if low_ireg rs then
+    OK (mk rd rs :: k)
+  else
+    OK (Pmov_rr EDX rs :: mk rd EDX :: k).
+
+Definition mk_smallstore (sto: addrmode -> ireg ->instruction) 
+                         (addr: addrmode) (rs: ireg) (k: code) :=
+  if low_ireg rs then
+    OK (sto addr rs :: k)
+  else
+    OK (Plea ECX addr :: Pmov_rr EDX rs ::
+        sto (Addrmode (Some ECX) None (inl _ Int.zero)) EDX :: k).
+
+(** Accessing slots in the stack frame.  *)
+
+Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
+  match ty with
+  | Tint =>
+      do r <- ireg_of dst;
+      OK (Pmov_rm r (Addrmode (Some base) None (inl _ ofs)) :: k)
+  | Tfloat =>
+      match preg_of dst with
+      | FR r => OK (Pmovsd_fm r (Addrmode (Some base) None (inl _ ofs)) :: k)
+      | ST0  => OK (Pfld_m (Addrmode (Some base) None (inl _ ofs)) :: k)
+      | _ => Error (msg "Asmgen.loadind")
+      end
+  end.
+
+Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
+  match ty with
+  | Tint =>
+      do r <- ireg_of src;
+      OK (Pmov_mr (Addrmode (Some base) None (inl _ ofs)) r :: k)
+  | Tfloat =>
+      match preg_of src with
+      | FR r => OK (Pmovsd_mf (Addrmode (Some base) None (inl _ ofs)) r :: k)
+      | ST0  => OK (Pfstp_m (Addrmode (Some base) None (inl _ ofs)) :: k)
+      | _ => Error (msg "Asmgen.loadind")
+      end
+  end.
+
+(** Translation of addressing modes *)
+
+Definition transl_addressing (a: addressing) (args: list mreg): res addrmode :=
+  match a, args with
+  | Aindexed n, a1 :: nil =>
+      do r1 <- ireg_of a1; OK(Addrmode (Some r1) None (inl _ n))
+  | Aindexed2 n, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK(Addrmode (Some r1) (Some(r2, Int.one)) (inl _ n))
+  | Ascaled sc n, a1 :: nil =>
+      do r1 <- ireg_of a1; OK(Addrmode None (Some(r1, sc)) (inl _ n))
+  | Aindexed2scaled sc n, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK(Addrmode (Some r1) (Some(r2, sc)) (inl _ n))
+  | Aglobal id ofs, nil =>
+      OK(Addrmode None None (inr _ (id, ofs)))
+  | Abased id ofs, a1 :: nil =>
+      do r1 <- ireg_of a1; OK(Addrmode (Some r1) None (inr _ (id, ofs)))
+  | Abasedscaled sc id ofs, a1 :: nil =>
+      do r1 <- ireg_of a1; OK(Addrmode None (Some(r1, sc)) (inr _ (id, ofs)))
+  | Ainstack n, nil =>
+      OK(Addrmode (Some ESP) None (inl _ n))
+  | _, _ =>
+      Error(msg "Asmgen.transl_addressing")
+  end.
+
+(** Floating-point comparison.  We swap the operands in some cases
+   to simplify the handling of the unordered case. *)
+
+Definition floatcomp (cmp: comparison) (r1 r2: freg) : instruction :=
+  match cmp with
+  | Clt | Cle => Pcomisd_ff r2 r1
+  | Ceq | Cne | Cgt | Cge => Pcomisd_ff r1 r2
+  end.
+
+(** Translation of a condition.  Prepends to [k] the instructions
+  that evaluate the condition and leave its boolean result in bits
+  of the condition register. *)
+
+Definition transl_cond
+              (cond: condition) (args: list mreg) (k: code) : res code :=
+  match cond, args with
+  | Ccomp c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmp_rr r1 r2 :: k)
+  | Ccompu c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmp_rr r1 r2 :: k)
+  | Ccompimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1; OK (Pcmp_ri r1 n :: k)
+  | Ccompuimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if Int.eq_dec n Int.zero then Ptest_rr r1 r1 :: k else Pcmp_ri r1 n :: k)
+  | Ccompf cmp, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k)
+  | Cnotcompf cmp, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k)
+  | Cmaskzero n, a1 :: nil =>
+      do r1 <- ireg_of a1; OK (Ptest_ri r1 n :: k)
+  | Cmasknotzero n, a1 :: nil =>
+      do r1 <- ireg_of a1; OK (Ptest_ri r1 n :: k)
+  | _, _ =>
+     Error(msg "Asmgen.transl_cond")
+  end.
+
+(** What processor condition to test for a given Mach condition. *)
+
+Definition testcond_for_signed_comparison (cmp: comparison) :=
+  match cmp with
+  | Ceq => Cond_e
+  | Cne => Cond_ne
+  | Clt => Cond_l
+  | Cle => Cond_le
+  | Cgt => Cond_g
+  | Cge => Cond_ge
+  end.
+
+Definition testcond_for_unsigned_comparison (cmp: comparison) :=
+  match cmp with
+  | Ceq => Cond_e
+  | Cne => Cond_ne
+  | Clt => Cond_b
+  | Cle => Cond_be
+  | Cgt => Cond_a
+  | Cge => Cond_ae
+  end.
+
+Definition testcond_for_condition (cond: condition) : testcond :=
+  match cond with
+  | Ccomp c => testcond_for_signed_comparison c
+  | Ccompu c => testcond_for_unsigned_comparison c
+  | Ccompimm c n => testcond_for_signed_comparison c
+  | Ccompuimm c n => testcond_for_unsigned_comparison c
+  | Ccompf c =>
+      match c with
+      | Ceq => Cond_enp
+      | Cne => Cond_nep
+      | Clt => Cond_a
+      | Cle => Cond_ae
+      | Cgt => Cond_a
+      | Cge => Cond_ae
+      end
+  | Cnotcompf c =>
+      match c with
+      | Ceq => Cond_nep
+      | Cne => Cond_enp
+      | Clt => Cond_be
+      | Cle => Cond_b
+      | Cgt => Cond_be
+      | Cge => Cond_b
+      end
+  | Cmaskzero n => Cond_e
+  | Cmasknotzero n => Cond_ne
+  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: code) : Errors.res code :=
+  match op, args with
+  | Omove, a1 :: nil =>
+      mk_mov (preg_of res) (preg_of a1) k
+  | Ointconst n, nil =>
+      do r <- ireg_of res; OK (Pmov_ri r n :: k)
+  | Ofloatconst f, nil =>
+      do r <- freg_of res; OK (Pmovsd_fi r f :: k)
+  | Ocast8signed, a1 :: nil =>
+      do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsb_rr r r1 k
+  | Ocast8unsigned, a1 :: nil =>
+      do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovzb_rr r r1 k
+  | Ocast16signed, a1 :: nil =>
+      do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsw_rr r r1 k
+  | Ocast16unsigned, a1 :: nil =>
+      do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovzw_rr r r1 k
+  | Oneg, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; OK (Pneg r :: k)
+  | Osub, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; OK (Psub_rr r r2 :: k)
+  | Omul, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pimul_rr r r2 :: k)
+  | Omulimm n, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; OK (Pimul_ri r n :: k)
+  | Odiv, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; mk_div Pidiv r r2 k
+  | Odivu, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; mk_div Pdiv r r2 k
+  | Omod, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; mk_mod Pidiv r r2 k
+  | Omodu, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; mk_mod Pdiv r r2 k
+  | Oand, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pand_rr r r2 :: k)
+  | Oandimm n, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; OK (Pand_ri r n :: k)
+  | Oor, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; OK (Por_rr r r2 :: k)
+  | Oorimm n, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; OK (Por_ri r n :: k)
+  | Oxor, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pxor_rr r r2 :: k)
+  | Oxorimm n, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; OK (Pxor_ri r n :: k)
+  | Oshl, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; mk_shift Psal_rcl r r2 k
+  | Oshlimm n, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; OK (Psal_ri r n :: k)
+  | Oshr, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; mk_shift Psar_rcl r r2 k
+  | Oshrimm n, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; OK (Psar_ri r n :: k)
+  | Oshru, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2; mk_shift Pshr_rcl r r2 k
+  | Oshruimm n, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; OK (Pshr_ri r n :: k)
+  | Oshrximm n, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; mk_shrximm r n k
+  | Ororimm n, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- ireg_of res; OK (Pror_ri r n :: k)
+  | Olea addr, _ =>
+      do am <- transl_addressing addr args; do r <- ireg_of res;
+      OK (Plea r am :: k)
+  | Onegf, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- freg_of res; OK (Pnegd r :: k)
+  | Oabsf, a1 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- freg_of res; OK (Pabsd r :: k)
+  | Oaddf, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- freg_of res; do r2 <- freg_of a2; OK (Paddd_ff r r2 :: k)
+  | Osubf, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- freg_of res; do r2 <- freg_of a2; OK (Psubd_ff r r2 :: k)
+  | Omulf, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- freg_of res; do r2 <- freg_of a2; OK (Pmuld_ff r r2 :: k)
+  | Odivf, a1 :: a2 :: nil =>
+      do x <- assertion (mreg_eq a1 res);
+      do r <- freg_of res; do r2 <- freg_of a2; OK (Pdivd_ff r r2 :: k)
+  | Osingleoffloat, a1 :: nil =>
+      do r <- freg_of res; do r1 <- freg_of a1; OK (Pcvtsd2ss_ff r r1 :: k)
+  | Ointoffloat, a1 :: nil =>
+      do r <- ireg_of res; do r1 <- freg_of a1; OK (Pcvttsd2si_rf r r1 :: k)
+  | Ofloatofint, a1 :: nil =>
+      do r <- freg_of res; do r1 <- ireg_of a1; OK (Pcvtsi2sd_fr r r1 :: k)
+  | Ocmp c, args =>
+      do r <- ireg_of res;
+      transl_cond c args (Psetcc (testcond_for_condition c) r :: k)
+  | _, _ =>
+      Error(msg "Asmgen.transl_op")
+  end.
+
+(** Translation of memory loads and stores *)
+
+Definition transl_load (chunk: memory_chunk)
+                       (addr: addressing) (args: list mreg) (dest: mreg)
+                       (k: code) : res code :=
+  do am <- transl_addressing addr args;
+  match chunk with
+  | Mint8unsigned =>
+      do r <- ireg_of dest; OK(Pmovzb_rm r am :: k)
+  | Mint8signed =>
+      do r <- ireg_of dest; OK(Pmovsb_rm r am :: k)
+  | Mint16unsigned =>
+      do r <- ireg_of dest; OK(Pmovzw_rm r am :: k)
+  | Mint16signed =>
+      do r <- ireg_of dest; OK(Pmovsw_rm r am :: k)
+  | Mint32 =>
+      do r <- ireg_of dest; OK(Pmov_rm r am :: k)
+  | Mfloat32 =>
+      do r <- freg_of dest; OK(Pcvtss2sd_fm r am :: k)
+  | Mfloat64 =>
+      do r <- freg_of dest; OK(Pmovsd_fm r am :: k)
+  end.
+
+Definition transl_store (chunk: memory_chunk)
+                        (addr: addressing) (args: list mreg) (src: mreg)
+                        (k: code) : res code :=
+  do am <- transl_addressing addr args;
+  match chunk with
+  | Mint8unsigned | Mint8signed =>
+      do r <- ireg_of src; mk_smallstore Pmovb_mr am r k
+  | Mint16unsigned | Mint16signed =>
+      do r <- ireg_of src; mk_smallstore Pmovw_mr am r k
+  | Mint32 =>
+      do r <- ireg_of src; OK(Pmov_mr am r :: k)
+  | Mfloat32 =>
+      do r <- freg_of src; OK(Pcvtsd2ss_mf am r :: k)
+  | Mfloat64 =>
+      do r <- freg_of src; OK(Pmovsd_mf am r :: k)
+  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 ESP ofs ty dst k
+  | Msetstack src ofs ty =>
+      storeind src ESP ofs ty k
+  | Mgetparam ofs ty dst =>
+      do k1 <- loadind EDX ofs ty dst k;
+      loadind ESP f.(fn_link_ofs) Tint IT1 k1
+  | Mop op args res =>
+      transl_op op args res k
+  | Mload chunk addr args dst =>
+      transl_load chunk addr args dst k
+  | Mstore chunk addr args src =>
+      transl_store chunk addr args src k
+  | Mcall sig (inl reg) =>
+      do r <- ireg_of reg; OK (Pcall_r r :: k)
+  | Mcall sig (inr symb) =>
+      OK (Pcall_s symb :: k)
+  | Mtailcall sig (inl reg) =>
+      do r <- ireg_of reg; 
+      OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) 
+                     f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
+          Pjmp_r r :: k)
+  | Mtailcall sig (inr symb) =>
+      OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) 
+                     f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
+          Pjmp_s symb :: k)
+  | Mlabel lbl =>
+      OK(Plabel lbl :: k)
+  | Mgoto lbl =>
+      OK(Pjmp_l lbl :: k)
+  | Mcond cond args lbl =>
+      transl_cond cond args (Pjcc (testcond_for_condition cond) lbl :: k)
+  | Mjumptable arg tbl =>
+      do r <- ireg_of arg; OK (Pjmptbl r tbl :: k)
+  | Mreturn =>
+      OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) 
+                     f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
+          Pret :: k)
+  | Mbuiltin ef args res =>
+      OK (Pbuiltin ef (List.map preg_of args) (preg_of res) :: k)
+  end.
+
+Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) :=
+  match il with
+  | nil => OK nil
+  | i1 :: il' => do k <- transl_code f il'; transl_instr f i1 k
+  end.
+
+(** 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 transf_function (f: Mach.function) : res Asm.code :=
+  do c <- transl_code f f.(fn_code);
+  if zlt (list_length_z c) Int.max_unsigned 
+  then OK (Pallocframe (- f.(fn_framesize)) f.(fn_stacksize)
+                       f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c)
+  else Error (msg "code size exceeded").
+
+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.
+