Revised Stacking and Asmgen passes and Mach semantics:

- no more prediction of return addresses (Asmgenretaddr is gone)
- instead, punch a hole for the retaddr in Mach stack frame and
  fill this hole with the return address in the Asmgen proof.



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

1 files changed, 294 insertions, 209 deletions

diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 8ef249d..0035dff 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -22,6 +22,23 @@ 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, mostly that argument and result registers are of the correct
+  types.  These properties are true by construction, but it's easier to
+  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.
+
 (** Decomposition of integer constants.  As noted in file [Asm],
   immediate arguments to PowerPC instructions must fit into 16 bits,
   and are interpreted after zero extension, sign extension, or
@@ -106,30 +123,36 @@ Definition rolm (r1 r2: ireg) (amount mask: int) (k: code) :=
 (** Accessing slots in the stack frame.  *)
 
 Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
-  if Int.eq (high_s ofs) Int.zero then
-    match ty with
-    | Tint => Plwz (ireg_of dst) (Cint ofs) base :: k
-    | Tfloat => Plfd (freg_of dst) (Cint ofs) base :: k
-    end
-  else
-    loadimm GPR0 ofs
-      (match ty with
-       | Tint => Plwzx (ireg_of dst) base GPR0 :: k
-       | Tfloat => Plfdx (freg_of dst) base GPR0 :: k
-       end).
+  match ty with
+  | Tint =>
+      do r <- ireg_of dst;
+      OK (if Int.eq (high_s ofs) Int.zero then
+            Plwz r (Cint ofs) base :: k
+          else
+            loadimm GPR0 ofs (Plwzx r base GPR0 :: k))
+  | Tfloat =>
+      do r <- freg_of dst;
+      OK (if Int.eq (high_s ofs) Int.zero then
+            Plfd r (Cint ofs) base :: k
+          else
+            loadimm GPR0 ofs (Plfdx r base GPR0 :: k))
+  end.
 
 Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
-  if Int.eq (high_s ofs) Int.zero then
-    match ty with
-    | Tint => Pstw (ireg_of src) (Cint ofs) base :: k
-    | Tfloat => Pstfd (freg_of src) (Cint ofs) base :: k
-    end
-  else
-    loadimm GPR0 ofs
-      (match ty with
-       | Tint => Pstwx (ireg_of src) base GPR0 :: k
-       | Tfloat => Pstfdx (freg_of src) base GPR0 :: k
-       end).
+  match ty with
+  | Tint =>
+      do r <- ireg_of src;
+      OK (if Int.eq (high_s ofs) Int.zero then
+            Pstw r (Cint ofs) base :: k
+          else
+            loadimm GPR0 ofs (Pstwx r base GPR0 :: k))
+  | Tfloat =>
+      do r <- freg_of src;
+      OK (if Int.eq (high_s ofs) Int.zero then
+            Pstfd r (Cint ofs) base :: k
+          else
+            loadimm GPR0 ofs (Pstfdx r base GPR0 :: k))
+  end.
 
 (** Constructor for a floating-point comparison.  The PowerPC has
   a single [fcmpu] instruction to compare floats, which sets
@@ -156,29 +179,31 @@ Definition transl_cond
               (cond: condition) (args: list mreg) (k: code) :=
   match cond, args with
   | Ccomp c, a1 :: a2 :: nil =>
-      Pcmpw (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmpw r1 r2 :: k)
   | Ccompu c, a1 :: a2 :: nil =>
-      Pcmplw (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmplw r1 r2 :: k)
   | Ccompimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
       if Int.eq (high_s n) Int.zero then
-        Pcmpwi (ireg_of a1) (Cint n) :: k
+        OK (Pcmpwi r1 (Cint n) :: k)
       else
-        loadimm GPR0 n (Pcmpw (ireg_of a1) GPR0 :: k)
+        OK (loadimm GPR0 n (Pcmpw r1 GPR0 :: k))
   | Ccompuimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
       if Int.eq (high_u n) Int.zero then
-        Pcmplwi (ireg_of a1) (Cint n) :: k
+        OK (Pcmplwi r1 (Cint n) :: k)
       else
-        loadimm GPR0 n (Pcmplw (ireg_of a1) GPR0 :: k)
+        OK (loadimm GPR0 n (Pcmplw r1 GPR0 :: k))
   | Ccompf cmp, a1 :: a2 :: nil =>
-      floatcomp cmp (freg_of a1) (freg_of a2) k
+      do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 k)
   | Cnotcompf cmp, a1 :: a2 :: nil =>
-      floatcomp cmp (freg_of a1) (freg_of a2) k
+      do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 k)
   | Cmaskzero n, a1 :: nil =>
-      andimm_base GPR0 (ireg_of a1) n k
+      do r1 <- ireg_of a1; OK (andimm_base GPR0 r1 n k)
   | Cmasknotzero n, a1 :: nil =>
-      andimm_base GPR0 (ireg_of a1) n k
+      do r1 <- ireg_of a1; OK (andimm_base GPR0 r1 n k)
   | _, _ =>
-     k (**r never happens for well-typed code *)
+      Error(msg "Asmgen.transl_cond")
   end.
 
 (*  CRbit_0 = Less
@@ -264,180 +289,267 @@ Definition classify_condition (c: condition) (args: list mreg): condition_class
 
 Definition transl_cond_op
              (cond: condition) (args: list mreg) (r: mreg) (k: code) :=
+  do r' <- ireg_of r;
   match classify_condition cond args with
   | condition_eq0 _ a _ =>
-      Psubfic GPR0 (ireg_of a) (Cint Int.zero) ::
-      Padde (ireg_of r) GPR0 (ireg_of a) :: k
+      do a' <- ireg_of a;
+      OK (Psubfic GPR0 a' (Cint Int.zero) ::
+          Padde r' GPR0 a' :: k)
   | condition_ne0 _ a _ =>
-      Paddic GPR0 (ireg_of a) (Cint Int.mone) ::
-      Psubfe (ireg_of r) GPR0 (ireg_of a) :: k
+      do a' <- ireg_of a;
+      OK (Paddic GPR0 a' (Cint Int.mone) ::
+          Psubfe r' GPR0 a' :: k)
   | condition_ge0 _ a _ =>
-      Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one ::
-      Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k
+      do a' <- ireg_of a;
+      OK (Prlwinm r' a' Int.one Int.one ::
+          Pxori r' r' (Cint Int.one) :: k)
   | condition_lt0 _ a _ =>
-      Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: k
+      do a' <- ireg_of a;
+      OK (Prlwinm r' a' Int.one Int.one :: k)
   | condition_default _ _ =>
       let p := crbit_for_cond cond in
       transl_cond cond args
-        (Pmfcrbit (ireg_of r) (fst p) ::
+        (Pmfcrbit r' (fst p) ::
          if snd p
          then k
-         else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)
+         else Pxori r' r' (Cint Int.one) :: k)
   end.
 
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
 Definition transl_op
-              (op: operation) (args: list mreg) (r: mreg) (k: code) :=
+              (op: operation) (args: list mreg) (res: mreg) (k: code) :=
   match op, args with
   | Omove, a1 :: nil =>
-      match mreg_type a1 with
-      | Tint => Pmr (ireg_of r) (ireg_of a1) :: k
-      | Tfloat => Pfmr (freg_of r) (freg_of a1) :: k
+      match preg_of res, preg_of a1 with
+      | IR r, IR a => OK (Pmr r a :: k)
+      | FR r, FR a => OK (Pfmr r a :: k)
+      |  _   ,  _    => Error(msg "Asmgen.Omove")
       end
   | Ointconst n, nil =>
-      loadimm (ireg_of r) n k
+      do r <- ireg_of res; OK (loadimm r n k)
   | Ofloatconst f, nil =>
-      Plfi (freg_of r) f :: k
+      do r <- freg_of res; OK (Plfi r f :: k)
   | Oaddrsymbol s ofs, nil =>
-      if symbol_is_small_data s ofs then
-        Paddi (ireg_of r) GPR0 (Csymbol_sda s ofs) :: k
-      else
-        Paddis GPR12 GPR0 (Csymbol_high s ofs) ::
-        Paddi (ireg_of r) GPR12 (Csymbol_low s ofs) :: k
+      do r <- ireg_of res;
+      OK (if symbol_is_small_data s ofs then
+           Paddi r GPR0 (Csymbol_sda s ofs) :: k
+         else
+           Paddis GPR12 GPR0 (Csymbol_high s ofs) ::
+           Paddi r GPR12 (Csymbol_low s ofs) :: k)
   | Oaddrstack n, nil =>
-      addimm (ireg_of r) GPR1 n k
+      do r <- ireg_of res; OK (addimm r GPR1 n k)
   | Ocast8signed, a1 :: nil =>
-      Pextsb (ireg_of r) (ireg_of a1) :: k
+      do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pextsb r r1 :: k)
   | Ocast16signed, a1 :: nil =>
-      Pextsh (ireg_of r) (ireg_of a1) :: k
+      do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pextsh r r1 :: k)
   | Oadd, a1 :: a2 :: nil =>
-      Padd (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Padd r r1 r2 :: k)
   | Oaddimm n, a1 :: nil =>
-      addimm (ireg_of r) (ireg_of a1) n k
+       do r1 <- ireg_of a1; do r <- ireg_of res; OK (addimm r r1 n k)
   | Osub, a1 :: a2 :: nil =>
-      Psubfc (ireg_of r) (ireg_of a2) (ireg_of a1) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Psubfc r r2 r1 :: k)
   | Osubimm n, a1 :: nil =>
-      if Int.eq (high_s n) Int.zero then
-        Psubfic (ireg_of r) (ireg_of a1) (Cint n) :: k
-      else
-        loadimm GPR0 n (Psubfc (ireg_of r) (ireg_of a1) GPR0 :: k)
+      do r1 <- ireg_of a1; do r <- ireg_of res;
+      OK (if Int.eq (high_s n) Int.zero then
+           Psubfic r r1 (Cint n) :: k
+         else
+          loadimm GPR0 n (Psubfc r r1 GPR0 :: k))
   | Omul, a1 :: a2 :: nil =>
-      Pmullw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pmullw r r1 r2 :: k)
   | Omulimm n, a1 :: nil =>
-      if Int.eq (high_s n) Int.zero then
-        Pmulli (ireg_of r) (ireg_of a1) (Cint n) :: k
-      else
-        loadimm GPR0 n (Pmullw (ireg_of r) (ireg_of a1) GPR0 :: k)
+      do r1 <- ireg_of a1; do r <- ireg_of res;
+      OK (if Int.eq (high_s n) Int.zero then
+           Pmulli r r1 (Cint n) :: k
+         else
+           loadimm GPR0 n (Pmullw r r1 GPR0 :: k))
   | Odiv, a1 :: a2 :: nil =>
-      Pdivw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pdivw r r1 r2 :: k)
   | Odivu, a1 :: a2 :: nil =>
-      Pdivwu (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pdivwu r r1 r2 :: k)
   | Oand, a1 :: a2 :: nil =>
-      Pand_ (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pand_ r r1 r2 :: k)
   | Oandimm n, a1 :: nil =>
-      andimm (ireg_of r) (ireg_of a1) n k
+      do r1 <- ireg_of a1; do r <- ireg_of res;
+      OK (andimm r r1 n k)
   | Oor, a1 :: a2 :: nil =>
-      Por (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Por r r1 r2 :: k)
   | Oorimm n, a1 :: nil =>
-      orimm (ireg_of r) (ireg_of a1) n k
+      do r1 <- ireg_of a1; do r <- ireg_of res;
+      OK (orimm r r1 n k)
   | Oxor, a1 :: a2 :: nil =>
-      Pxor (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pxor r r1 r2 :: k)
   | Oxorimm n, a1 :: nil =>
-      xorimm (ireg_of r) (ireg_of a1) n k
+      do r1 <- ireg_of a1; do r <- ireg_of res;
+      OK (xorimm r r1 n k)
   | Onot, a1 :: nil =>
-      Pnor (ireg_of r) (ireg_of a1) (ireg_of a1) :: k
+      do r1 <- ireg_of a1; do r <- ireg_of res;
+      OK (Pnor r r1 r1 :: k)
   | Onand, a1 :: a2 :: nil =>
-      Pnand (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pnand r r1 r2 :: k)
   | Onor, a1 :: a2 :: nil =>
-      Pnor (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pnor r r1 r2 :: k)
   | Onxor, a1 :: a2 :: nil =>
-      Peqv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Peqv r r1 r2 :: k)
   | Oandc, a1 :: a2 :: nil =>
-      Pandc (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pandc r r1 r2 :: k)
   | Oorc, a1 :: a2 :: nil =>
-      Porc (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Porc r r1 r2 :: k)
   | Oshl, a1 :: a2 :: nil =>
-      Pslw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pslw r r1 r2 :: k)
   | Oshr, a1 :: a2 :: nil =>
-      Psraw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Psraw r r1 r2 :: k)
   | Oshrimm n, a1 :: nil =>
-      Psrawi (ireg_of r) (ireg_of a1) n :: k
+      do r1 <- ireg_of a1; do r <- ireg_of res;
+      OK (Psrawi r r1 n :: k)
   | Oshrximm n, a1 :: nil =>
-      Psrawi (ireg_of r) (ireg_of a1) n ::
-      Paddze (ireg_of r) (ireg_of r) :: k
+      do r1 <- ireg_of a1; do r <- ireg_of res;
+      OK (Psrawi r r1 n :: Paddze r r :: k)
   | Oshru, a1 :: a2 :: nil =>
-      Psrw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Psrw r r1 r2 :: k)
   | Orolm amount mask, a1 :: nil =>
-      rolm (ireg_of r) (ireg_of a1) amount mask k
+      do r1 <- ireg_of a1; do r <- ireg_of res;
+      OK (rolm r r1 amount mask k)
   | Oroli amount mask, a1 :: a2 :: nil =>
-      if mreg_eq a1 r  then (**r should always be true *)
-        Prlwimi (ireg_of r) (ireg_of a2) amount mask :: k
-      else
-        Pmr GPR0 (ireg_of a1) ::
-	Prlwimi GPR0 (ireg_of a2) amount mask ::
-	Pmr (ireg_of r) GPR0 :: k
+      do x <- assertion (mreg_eq a1 res);
+      do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Prlwimi r r2 amount mask :: k)
   | Onegf, a1 :: nil =>
-      Pfneg (freg_of r) (freg_of a1) :: k
+      do r1 <- freg_of a1; do r <- freg_of res;
+      OK (Pfneg r r1 :: k)
   | Oabsf, a1 :: nil =>
-      Pfabs (freg_of r) (freg_of a1) :: k
+      do r1 <- freg_of a1; do r <- freg_of res;
+      OK (Pfabs r r1 :: k)
   | Oaddf, a1 :: a2 :: nil =>
-      Pfadd (freg_of r) (freg_of a1) (freg_of a2) :: k
+      do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res;
+      OK (Pfadd r r1 r2 :: k)
   | Osubf, a1 :: a2 :: nil =>
-      Pfsub (freg_of r) (freg_of a1) (freg_of a2) :: k
+      do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res;
+      OK (Pfsub r r1 r2 :: k)
   | Omulf, a1 :: a2 :: nil =>
-      Pfmul (freg_of r) (freg_of a1) (freg_of a2) :: k
+      do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res;
+      OK (Pfmul r r1 r2 :: k)
   | Odivf, a1 :: a2 :: nil =>
-      Pfdiv (freg_of r) (freg_of a1) (freg_of a2) :: k
+      do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res;
+      OK (Pfdiv r r1 r2 :: k)
   | Osingleoffloat, a1 :: nil =>
-      Pfrsp (freg_of r) (freg_of a1) :: k
+      do r1 <- freg_of a1; do r <- freg_of res;
+      OK (Pfrsp r r1 :: k)
   | Ointoffloat, a1 :: nil =>
-      Pfcti (ireg_of r) (freg_of a1) :: k
+      do r1 <- freg_of a1; do r <- ireg_of res;
+      OK (Pfcti r r1 :: k)
   | Ofloatofwords, a1 :: a2 :: nil =>
-      Pfmake (freg_of r) (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res;
+      OK (Pfmake r r1 r2 :: k)
   | Ocmp cmp, _ =>
-      transl_cond_op cmp args r k
+      transl_cond_op cmp args res k
   | _, _ =>
-      k (**r never happens for well-typed code *)
+      Error(msg "Asmgen.transl_op")
   end.
 
-(** Common code to translate [Mload] and [Mstore] instructions. *)
+(** Translation of memory accesses: loads, and stores. *)
 
 Definition int_temp_for (r: mreg) :=
   if mreg_eq r IT2 then GPR11 else GPR12.
 
-Definition transl_load_store 
+Definition transl_memory_access
      (mk1: constant -> ireg -> instruction)
      (mk2: ireg -> ireg -> instruction)
      (addr: addressing) (args: list mreg) 
      (temp: ireg) (k: code) :=
   match addr, args with
   | Aindexed ofs, a1 :: nil =>
-      if Int.eq (high_s ofs) Int.zero then
-        mk1 (Cint ofs) (ireg_of a1) :: k
-      else
-        Paddis temp (ireg_of a1) (Cint (high_s ofs)) ::
-        mk1 (Cint (low_s ofs)) temp :: k
+      do r1 <- ireg_of a1;
+      OK (if Int.eq (high_s ofs) Int.zero then
+           mk1 (Cint ofs) r1 :: k
+         else
+           Paddis temp r1 (Cint (high_s ofs)) ::
+           mk1 (Cint (low_s ofs)) temp :: k)
   | Aindexed2, a1 :: a2 :: nil =>
-      mk2 (ireg_of a1) (ireg_of a2) :: k
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (mk2 r1 r2 :: k)
   | Aglobal symb ofs, nil =>
-      if symbol_is_small_data symb ofs then
-        mk1 (Csymbol_sda symb ofs) GPR0 :: k
-      else
-        Paddis temp GPR0 (Csymbol_high symb ofs) ::
-        mk1 (Csymbol_low symb ofs) temp :: k
+      OK (if symbol_is_small_data symb ofs then
+           mk1 (Csymbol_sda symb ofs) GPR0 :: k
+         else
+           Paddis temp GPR0 (Csymbol_high symb ofs) ::
+           mk1 (Csymbol_low symb ofs) temp :: k)
   | Abased symb ofs, a1 :: nil =>
-      Paddis temp (ireg_of a1) (Csymbol_high symb ofs) ::
-      mk1 (Csymbol_low symb ofs) temp :: k
+      do r1 <- ireg_of a1;
+      OK (Paddis temp r1 (Csymbol_high symb ofs) ::
+         mk1 (Csymbol_low symb ofs) temp :: k)
   | Ainstack ofs, nil =>
-      if Int.eq (high_s ofs) Int.zero then
-        mk1 (Cint ofs) GPR1 :: k
-      else
-        Paddis temp GPR1 (Cint (high_s ofs)) ::
-        mk1 (Cint (low_s ofs)) temp :: k
+      OK (if Int.eq (high_s ofs) Int.zero then
+           mk1 (Cint ofs) GPR1 :: k
+         else
+           Paddis temp GPR1 (Cint (high_s ofs)) ::
+           mk1 (Cint (low_s ofs)) temp :: k)
   | _, _ =>
-      (* should not happen *) k
+      Error(msg "Asmgen.transl_memory_access")
+  end.
+
+Definition transl_load (chunk: memory_chunk) (addr: addressing)
+                       (args: list mreg) (dst: mreg) (k: code) :=
+  match chunk with
+  | Mint8signed =>
+      do r <- ireg_of dst;
+      transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 (Pextsb r r :: k)
+  | Mint8unsigned =>
+      do r <- ireg_of dst;
+      transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 k
+  | Mint16signed =>
+      do r <- ireg_of dst;
+      transl_memory_access (Plha r) (Plhax r) addr args GPR12 k
+  | Mint16unsigned =>
+      do r <- ireg_of dst;
+      transl_memory_access (Plhz r) (Plhzx r) addr args GPR12 k
+  | Mint32 =>
+      do r <- ireg_of dst;
+      transl_memory_access (Plwz r) (Plwzx r) addr args GPR12 k
+  | Mfloat32 =>
+      do r <- freg_of dst;
+      transl_memory_access (Plfs r) (Plfsx r) addr args GPR12 k
+  | Mfloat64 | Mfloat64al32 =>
+      do r <- freg_of dst;
+      transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k
+  end.
+
+Definition transl_store (chunk: memory_chunk) (addr: addressing)
+                        (args: list mreg) (src: mreg) (k: code) :=
+  let temp := int_temp_for src in
+  match chunk with
+  | Mint8signed | Mint8unsigned =>
+      do r <- ireg_of src;
+      transl_memory_access (Pstb r) (Pstbx r) addr args temp k
+  | Mint16signed | Mint16unsigned =>
+      do r <- ireg_of src;
+      transl_memory_access (Psth r) (Psthx r) addr args temp k
+  | Mint32  =>
+      do r <- ireg_of src;
+      transl_memory_access (Pstw r) (Pstwx r) addr args temp k
+  | Mfloat32 =>
+      do r <- freg_of src;
+      transl_memory_access (Pstfs r) (Pstfsx r) addr args temp k
+  | Mfloat64 | Mfloat64al32 =>
+      do r <- freg_of src;
+      transl_memory_access (Pstfd r) (Pstfdx r) addr args temp k
   end.
 
 (** Translation of arguments to annotations *)
@@ -450,105 +562,80 @@ Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param :=
 
 (** Translation of a Mach instruction. *)
 
-Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
+Definition transl_instr (f: Mach.function) (i: Mach.instruction)
+                        (r11_is_parent: bool) (k: code) :=
   match i with
   | Mgetstack ofs ty dst =>
       loadind GPR1 ofs ty dst k
   | Msetstack src ofs ty =>
       storeind src GPR1 ofs ty k
   | Mgetparam ofs ty dst =>
-      Plwz GPR11 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR11 ofs ty dst k
+      if r11_is_parent then
+        loadind GPR11 ofs ty dst k
+      else
+        (do k1 <- loadind GPR11 ofs ty dst k;
+         loadind GPR1 f.(fn_link_ofs) Tint IT1 k1)
   | Mop op args res =>
       transl_op op args res k
   | Mload chunk addr args dst =>
-      match chunk with
-      | Mint8signed =>
-          transl_load_store
-            (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args GPR12
-            (Pextsb (ireg_of dst) (ireg_of dst) :: k)
-      | Mint8unsigned =>
-          transl_load_store
-            (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args GPR12 k
-      | Mint16signed =>
-          transl_load_store
-            (Plha (ireg_of dst)) (Plhax (ireg_of dst)) addr args GPR12 k
-      | Mint16unsigned =>
-          transl_load_store
-            (Plhz (ireg_of dst)) (Plhzx (ireg_of dst)) addr args GPR12 k
-      | Mint32 =>
-          transl_load_store
-            (Plwz (ireg_of dst)) (Plwzx (ireg_of dst)) addr args GPR12 k
-      | Mfloat32 =>
-          transl_load_store
-            (Plfs (freg_of dst)) (Plfsx (freg_of dst)) addr args GPR12 k
-      | Mfloat64 | Mfloat64al32 =>
-          transl_load_store
-            (Plfd (freg_of dst)) (Plfdx (freg_of dst)) addr args GPR12 k
-      end
+      transl_load chunk addr args dst k
   | Mstore chunk addr args src =>
-      let temp := int_temp_for src in
-      match chunk with
-      | Mint8signed =>
-          transl_load_store
-            (Pstb (ireg_of src)) (Pstbx (ireg_of src)) addr args temp k
-      | Mint8unsigned =>
-          transl_load_store
-            (Pstb (ireg_of src)) (Pstbx (ireg_of src)) addr args temp k
-      | Mint16signed =>
-          transl_load_store
-            (Psth (ireg_of src)) (Psthx (ireg_of src)) addr args temp k
-      | Mint16unsigned =>
-          transl_load_store
-            (Psth (ireg_of src)) (Psthx (ireg_of src)) addr args temp k
-      | Mint32 =>
-          transl_load_store
-            (Pstw (ireg_of src)) (Pstwx (ireg_of src)) addr args temp k
-      | Mfloat32 =>
-          transl_load_store
-            (Pstfs (freg_of src)) (Pstfsx (freg_of src)) addr args temp k
-      | Mfloat64 | Mfloat64al32 =>
-          transl_load_store
-            (Pstfd (freg_of src)) (Pstfdx (freg_of src)) addr args temp k
-      end
+      transl_store chunk addr args src k
   | Mcall sig (inl r) =>
-      Pmtctr (ireg_of r) :: Pbctrl :: k
+      do r1 <- ireg_of r; OK (Pmtctr r1 :: Pbctrl :: k)
   | Mcall sig (inr symb) =>
-      Pbl symb :: k
+      OK (Pbl symb :: k)
   | Mtailcall sig (inl r) =>
-      Pmtctr (ireg_of r) :: 
-      Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
-      Pmtlr GPR0 ::
-      Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: 
-      Pbctr :: k
+      do r1 <- ireg_of r;
+      OK (Pmtctr r1 ::
+          Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+          Pmtlr GPR0 ::
+          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: 
+          Pbctr :: k)
   | Mtailcall sig (inr symb) =>
-      Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
-      Pmtlr GPR0 ::
-      Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: 
-      Pbs symb :: k
+      OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+          Pmtlr GPR0 ::
+          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: 
+          Pbs symb :: k)
   | Mbuiltin ef args res =>
-      Pbuiltin ef (map preg_of args) (preg_of res) :: k
+      OK (Pbuiltin ef (map preg_of args) (preg_of res) :: k)
   | Mannot ef args =>
-      Pannot ef (map transl_annot_param args) :: k
+      OK (Pannot ef (map transl_annot_param args) :: k)
   | Mlabel lbl =>
-      Plabel lbl :: k
+      OK (Plabel lbl :: k)
   | Mgoto lbl =>
-      Pb lbl :: k
+      OK (Pb lbl :: k)
   | Mcond cond args lbl =>
       let p := crbit_for_cond cond in
       transl_cond cond args
         (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k)
   | Mjumptable arg tbl =>
-      Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) ::
-      Pbtbl GPR12 tbl :: k
+      do r <- ireg_of arg;
+      OK (Pbtbl r tbl :: k)
   | Mreturn =>
-      Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
-      Pmtlr GPR0 ::
-      Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
-      Pblr :: k
+      OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+          Pmtlr GPR0 ::
+          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
+          Pblr :: k)
+  end.
+
+(** Translation of a code sequence *)
+
+Definition r11_is_parent (before: bool) (i: Mach.instruction) : bool :=
+  match i with
+  | Msetstack src ofs ty => before
+  | Mgetparam ofs ty dst => negb (mreg_eq dst IT1)
+  | Mop Omove args res => before && negb (mreg_eq res IT1)
+  | _ => false
   end.
 
-Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
-  List.fold_right (transl_instr f) nil il.
+Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction)  (r11p: bool) :=
+  match il with
+  | nil => OK nil
+  | i1 :: il' =>
+      do k <- transl_code f il' (r11_is_parent r11p i1);
+      transl_instr f i1 r11p k
+  end.
 
 (** Translation of a whole function.  Note that we must check
   that the generated code contains less than [2^32] instructions,
@@ -556,18 +643,16 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
   around, leading to incorrect executions. *)
 
 Definition transl_function (f: Mach.function) :=
-  Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
-  Pmflr GPR0 ::
-  Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
-  transl_code f f.(fn_code).
-
-Open Local Scope string_scope.
+  do c <- transl_code f f.(Mach.fn_code) false;
+  OK (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
+      Pmflr GPR0 ::
+      Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: c).
 
 Definition transf_function (f: Mach.function) : res Asm.code :=
-  let c := transl_function f in
+  do c <- transl_function f;
   if zlt Int.max_unsigned (list_length_z c)
-  then Errors.Error (msg "code size exceeded")
-  else Errors.OK c.
+  then Error (msg "code size exceeded")
+  else OK c.
 
 Definition transf_fundef (f: Mach.fundef) : res Asm.fundef :=
   transf_partial_fundef transf_function f.