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

6 files changed, 1554 insertions, 2566 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 5d815fd..27e801a 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -84,6 +84,11 @@ End PregEq.
 
 Module Pregmap := EMap(PregEq).
 
+(** Conventional names for stack pointer ([SP]) and return address ([RA]) *)
+
+Notation "'SP'" := GPR1 (only parsing).
+Notation "'RA'" := LR (only parsing).
+
 (** Symbolic constants.  Immediate operands to an arithmetic instruction
   or an indexed memory access can be either integer literals,
   or the low or high 16 bits of a symbolic reference (the address
@@ -291,7 +296,9 @@ lbl:    .long   table[0], table[1], ...
 *)
 
 Definition code := list instruction.
-Definition fundef := AST.fundef code.
+Definition function := code.
+Definition fn_code (f: function) : code := f.
+Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
 
 (** * Operational semantics *)
@@ -309,6 +316,14 @@ Definition genv := Genv.t fundef unit.
 Notation "a # b" := (a b) (at level 1, only parsing).
 Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level).
 
+(** Undefining some registers *)
+
+Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
+  match l with
+  | nil => rs
+  | r :: l' => undef_regs l' (rs#r <- Vundef)
+  end.
+
 Section RELSEM.
 
 (** Looking up instructions in a code sequence by position. *)
@@ -428,8 +443,8 @@ Definition const_high (c: constant) :=
   or [Error] if the processor is stuck. *)
 
 Inductive outcome: Type :=
-  | OK: regset -> mem -> outcome
-  | Error: outcome.
+  | Next: regset -> mem -> outcome
+  | Stuck: outcome.
 
 (** Manipulations over the [PC] register: continuing with the next
   instruction ([nextinstr]) or branching to a label ([goto_label]). *)
@@ -439,11 +454,11 @@ Definition nextinstr (rs: regset) :=
 
 Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) :=
   match label_pos lbl 0 c with
-  | None => Error
+  | None => Stuck
   | Some pos =>
       match rs#PC with
-      | Vptr b ofs => OK (rs#PC <- (Vptr b (Int.repr pos))) m
-      | _ => Error
+      | Vptr b ofs => Next (rs#PC <- (Vptr b (Int.repr pos))) m
+      | _ => Stuck
     end
   end.
 
@@ -453,29 +468,29 @@ Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) :=
 Definition load1 (chunk: memory_chunk) (rd: preg)
                  (cst: constant) (r1: ireg) (rs: regset) (m: mem) :=
   match Mem.loadv chunk m (Val.add (gpr_or_zero rs r1) (const_low cst)) with
-  | None => Error
-  | Some v => OK (nextinstr (rs#rd <- v)) m
+  | None => Stuck
+  | Some v => Next (nextinstr (rs#rd <- v)) m
   end.
 
 Definition load2 (chunk: memory_chunk) (rd: preg) (r1 r2: ireg)
                  (rs: regset) (m: mem) :=
   match Mem.loadv chunk m (Val.add rs#r1 rs#r2) with
-  | None => Error
-  | Some v => OK (nextinstr (rs#rd <- v)) m
+  | None => Stuck
+  | Some v => Next (nextinstr (rs#rd <- v)) m
   end.
 
 Definition store1 (chunk: memory_chunk) (r: preg)
                   (cst: constant) (r1: ireg) (rs: regset) (m: mem) :=
   match Mem.storev chunk m (Val.add (gpr_or_zero rs r1) (const_low cst)) (rs#r) with
-  | None => Error
-  | Some m' => OK (nextinstr rs) m'
+  | None => Stuck
+  | Some m' => Next (nextinstr rs) m'
   end.
 
 Definition store2 (chunk: memory_chunk) (r: preg) (r1 r2: ireg)
                   (rs: regset) (m: mem) :=
   match Mem.storev chunk m (Val.add rs#r1 rs#r2) (rs#r) with
-  | None => Error
-  | Some m' => OK (nextinstr rs) m'
+  | None => Stuck
+  | Some m' => Next (nextinstr rs) m'
   end.
 
 (** Operations over condition bits. *)
@@ -521,127 +536,124 @@ Definition compare_float (rs: regset) (v1 v2: val) :=
 Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome :=
   match i with
   | Padd rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m
   | Padde rd r1 r2 =>
-      OK (nextinstr (rs #rd <- (Val.add (Val.add rs#r1 rs#r2) rs#CARRY)
+      Next (nextinstr (rs #rd <- (Val.add (Val.add rs#r1 rs#r2) rs#CARRY)
                         #CARRY <- (Val.add_carry rs#r1 rs#r2 rs#CARRY))) m
   | Paddi rd r1 cst =>
-      OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)))) m
+      Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)))) m
   | Paddic rd r1 cst =>
-      OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst))
+      Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst))
                        #CARRY <- (Val.add_carry (gpr_or_zero rs r1) (const_low cst) Vzero))) m
   | Paddis rd r1 cst =>
-      OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m
+      Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m
   | Paddze rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY)
+      Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY)
                        #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m
   | Pallocframe sz ofs =>
       let (m1, stk) := Mem.alloc m 0 sz in
       let sp := Vptr stk Int.zero in
       match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with
-      | None => Error
-      | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)) m2
+      | None => Stuck
+      | Some m2 => Next (nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)) m2
       end
   | Pand_ rd r1 r2 =>
       let v := Val.and rs#r1 rs#r2 in
-      OK (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m
+      Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m
   | Pandc rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.and rs#r1 (Val.notint rs#r2)))) m
+      Next (nextinstr (rs#rd <- (Val.and rs#r1 (Val.notint rs#r2)))) m
   | Pandi_ rd r1 cst =>
       let v := Val.and rs#r1 (const_low cst) in
-      OK (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m
+      Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m
   | Pandis_ rd r1 cst =>
       let v := Val.and rs#r1 (const_high cst) in
-      OK (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m
+      Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m
   | Pb lbl =>
       goto_label c lbl rs m
   | Pbctr =>
-      OK (rs#PC <- (rs#CTR)) m
+      Next (rs#PC <- (rs#CTR)) m
   | Pbctrl =>
-      OK (rs#LR <- (Val.add rs#PC Vone) #PC <- (rs#CTR)) m
+      Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (rs#CTR)) m
   | Pbf bit lbl =>
       match rs#(reg_of_crbit bit) with
-      | Vint n => if Int.eq n Int.zero then goto_label c lbl rs m else OK (nextinstr rs) m
-      | _ => Error
+      | Vint n => if Int.eq n Int.zero then goto_label c lbl rs m else Next (nextinstr rs) m
+      | _ => Stuck
       end
   | Pbl ident =>
-      OK (rs#LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset ident Int.zero)) m
+      Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset ident Int.zero)) m
   | Pbs ident =>
-      OK (rs#PC <- (symbol_offset ident Int.zero)) m
+      Next (rs#PC <- (symbol_offset ident Int.zero)) m
   | Pblr =>
-      OK (rs#PC <- (rs#LR)) m
+      Next (rs#PC <- (rs#LR)) m
   | Pbt bit lbl =>
       match rs#(reg_of_crbit bit) with
-      | Vint n => if Int.eq n Int.zero then OK (nextinstr rs) m else goto_label c lbl rs m
-      | _ => Error
+      | Vint n => if Int.eq n Int.zero then Next (nextinstr rs) m else goto_label c lbl rs m
+      | _ => Stuck
       end
   | Pbtbl r tbl =>
-      match gpr_or_zero rs r with
+      match rs r with
       | Vint n => 
-          let pos := Int.unsigned n in
-          if zeq (Zmod pos 4) 0 then
-            match list_nth_z tbl (pos / 4) with
-            | None => Error
-            | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
-            end
-          else Error
-      | _ => Error
+          match list_nth_z tbl (Int.unsigned n) with
+          | None => Stuck
+          | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
+          end
+      | _ => Stuck
       end
   | Pcmplw r1 r2 =>
-      OK (nextinstr (compare_uint rs m rs#r1 rs#r2)) m
+      Next (nextinstr (compare_uint rs m rs#r1 rs#r2)) m
   | Pcmplwi r1 cst =>
-      OK (nextinstr (compare_uint rs m rs#r1 (const_low cst))) m
+      Next (nextinstr (compare_uint rs m rs#r1 (const_low cst))) m
   | Pcmpw r1 r2 =>
-      OK (nextinstr (compare_sint rs rs#r1 rs#r2)) m
+      Next (nextinstr (compare_sint rs rs#r1 rs#r2)) m
   | Pcmpwi r1 cst =>
-      OK (nextinstr (compare_sint rs rs#r1 (const_low cst))) m
+      Next (nextinstr (compare_sint rs rs#r1 (const_low cst))) m
   | Pcror bd b1 b2 =>
-      OK (nextinstr (rs#(reg_of_crbit bd) <- (Val.or rs#(reg_of_crbit b1) rs#(reg_of_crbit b2)))) m
+      Next (nextinstr (rs#(reg_of_crbit bd) <- (Val.or rs#(reg_of_crbit b1) rs#(reg_of_crbit b2)))) m
   | Pdivw rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.maketotal (Val.divs rs#r1 rs#r2)))) m
+      Next (nextinstr (rs#rd <- (Val.maketotal (Val.divs rs#r1 rs#r2)))) m
   | Pdivwu rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.maketotal (Val.divu rs#r1 rs#r2)))) m
+      Next (nextinstr (rs#rd <- (Val.maketotal (Val.divu rs#r1 rs#r2)))) m
   | Peqv rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.notint (Val.xor rs#r1 rs#r2)))) m
+      Next (nextinstr (rs#rd <- (Val.notint (Val.xor rs#r1 rs#r2)))) m
   | Pextsb rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m
+      Next (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m
   | Pextsh rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m
+      Next (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m
   | Pfreeframe sz ofs =>
       match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with
-      | None => Error
+      | None => Stuck
       | Some v =>
           match rs#GPR1 with
           | Vptr stk ofs =>
               match Mem.free m stk 0 sz with
-              | None => Error
-              | Some m' => OK (nextinstr (rs#GPR1 <- v)) m'
+              | None => Stuck
+              | Some m' => Next (nextinstr (rs#GPR1 <- v)) m'
               end
-          | _ => Error
+          | _ => Stuck
           end
       end
   | Pfabs rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.absf rs#r1))) m
+      Next (nextinstr (rs#rd <- (Val.absf rs#r1))) m
   | Pfadd rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m
   | Pfcmpu r1 r2 =>
-      OK (nextinstr (compare_float rs rs#r1 rs#r2)) m
+      Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
   | Pfcti rd r1 =>
-      OK (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m
+      Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m
   | Pfdiv rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m
   | Pfmake rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m
   | Pfmr rd r1 =>
-      OK (nextinstr (rs#rd <- (rs#r1))) m
+      Next (nextinstr (rs#rd <- (rs#r1))) m
   | Pfmul rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m
   | Pfneg rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.negf rs#r1))) m
+      Next (nextinstr (rs#rd <- (Val.negf rs#r1))) m
   | Pfrsp rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m
+      Next (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m
   | Pfsub rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m
   | Plbz rd cst r1 =>
       load1 Mint8unsigned rd cst r1 rs m
   | Plbzx rd r1 r2 =>
@@ -663,50 +675,50 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Plhzx rd r1 r2 =>
       load2 Mint16unsigned rd r1 r2 rs m
   | Plfi rd f =>
-      OK (nextinstr (rs #GPR12 <- Vundef #rd <- (Vfloat f))) m
+      Next (nextinstr (rs #GPR12 <- Vundef #rd <- (Vfloat f))) m
   | Plwz rd cst r1 =>
       load1 Mint32 rd cst r1 rs m
   | Plwzx rd r1 r2 =>
       load2 Mint32 rd r1 r2 rs m
   | Pmfcrbit rd bit =>
-      OK (nextinstr (rs#rd <- (rs#(reg_of_crbit bit)))) m
+      Next (nextinstr (rs#rd <- (rs#(reg_of_crbit bit)))) m
   | Pmflr rd =>
-      OK (nextinstr (rs#rd <- (rs#LR))) m
+      Next (nextinstr (rs#rd <- (rs#LR))) m
   | Pmr rd r1 =>
-      OK (nextinstr (rs#rd <- (rs#r1))) m
+      Next (nextinstr (rs#rd <- (rs#r1))) m
   | Pmtctr r1 =>
-      OK (nextinstr (rs#CTR <- (rs#r1))) m
+      Next (nextinstr (rs#CTR <- (rs#r1))) m
   | Pmtlr r1 =>
-      OK (nextinstr (rs#LR <- (rs#r1))) m
+      Next (nextinstr (rs#LR <- (rs#r1))) m
   | Pmulli rd r1 cst =>
-      OK (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m
+      Next (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m
   | Pmullw rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.mul rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.mul rs#r1 rs#r2))) m
   | Pnand rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.notint (Val.and rs#r1 rs#r2)))) m
+      Next (nextinstr (rs#rd <- (Val.notint (Val.and rs#r1 rs#r2)))) m
   | Pnor rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.notint (Val.or rs#r1 rs#r2)))) m
+      Next (nextinstr (rs#rd <- (Val.notint (Val.or rs#r1 rs#r2)))) m
   | Por rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.or rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.or rs#r1 rs#r2))) m
   | Porc rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.or rs#r1 (Val.notint rs#r2)))) m
+      Next (nextinstr (rs#rd <- (Val.or rs#r1 (Val.notint rs#r2)))) m
   | Pori rd r1 cst =>
-      OK (nextinstr (rs#rd <- (Val.or rs#r1 (const_low cst)))) m
+      Next (nextinstr (rs#rd <- (Val.or rs#r1 (const_low cst)))) m
   | Poris rd r1 cst =>
-      OK (nextinstr (rs#rd <- (Val.or rs#r1 (const_high cst)))) m
+      Next (nextinstr (rs#rd <- (Val.or rs#r1 (const_high cst)))) m
   | Prlwinm rd r1 amount mask =>
-      OK (nextinstr (rs#rd <- (Val.rolm rs#r1 amount mask))) m
+      Next (nextinstr (rs#rd <- (Val.rolm rs#r1 amount mask))) m
   | Prlwimi rd r1 amount mask =>
-      OK (nextinstr (rs#rd <- (Val.or (Val.and rs#rd (Vint (Int.not mask)))
+      Next (nextinstr (rs#rd <- (Val.or (Val.and rs#rd (Vint (Int.not mask)))
                                      (Val.rolm rs#r1 amount mask)))) m
   | Pslw rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m
   | Psraw rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2) #CARRY <- (Val.shr_carry rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2) #CARRY <- (Val.shr_carry rs#r1 rs#r2))) m
   | Psrawi rd r1 n =>
-      OK (nextinstr (rs#rd <- (Val.shr rs#r1 (Vint n)) #CARRY <- (Val.shr_carry rs#r1 (Vint n)))) m
+      Next (nextinstr (rs#rd <- (Val.shr rs#r1 (Vint n)) #CARRY <- (Val.shr_carry rs#r1 (Vint n)))) m
   | Psrw rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.shru rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.shru rs#r1 rs#r2))) m
   | Pstb rd cst r1 =>
       store1 Mint8unsigned rd cst r1 rs m
   | Pstbx rd r1 r2 =>
@@ -717,13 +729,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       store2 Mfloat64al32 rd r1 r2 rs m
   | Pstfs rd cst r1 =>
       match store1 Mfloat32 rd cst r1 rs m with
-      | OK rs' m' => OK (rs'#FPR13 <- Vundef) m'
-      | Error => Error
+      | Next rs' m' => Next (rs'#FPR13 <- Vundef) m'
+      | Stuck => Stuck
       end
   | Pstfsx rd r1 r2 =>
       match store2 Mfloat32 rd r1 r2 rs m with
-      | OK rs' m' => OK (rs'#FPR13 <- Vundef) m'
-      | Error => Error
+      | Next rs' m' => Next (rs'#FPR13 <- Vundef) m'
+      | Stuck => Stuck
       end
   | Psth rd cst r1 =>
       store1 Mint16unsigned rd cst r1 rs m
@@ -734,41 +746,34 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Pstwx rd r1 r2 =>
       store2 Mint32 rd r1 r2 rs m
   | Psubfc rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1)
+      Next (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1)
                        #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) Vone))) m
   | Psubfe rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.add (Val.add rs#r2 (Val.notint rs#r1)) rs#CARRY)
+      Next (nextinstr (rs#rd <- (Val.add (Val.add rs#r2 (Val.notint rs#r1)) rs#CARRY)
                        #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) rs#CARRY))) m
   | Psubfic rd r1 cst =>
-      OK (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1)
+      Next (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1)
                        #CARRY <- (Val.add_carry (const_low cst) (Val.notint rs#r1) Vone))) m
   | Pxor rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.xor rs#r1 rs#r2))) m
+      Next (nextinstr (rs#rd <- (Val.xor rs#r1 rs#r2))) m
   | Pxori rd r1 cst =>
-      OK (nextinstr (rs#rd <- (Val.xor rs#r1 (const_low cst)))) m
+      Next (nextinstr (rs#rd <- (Val.xor rs#r1 (const_low cst)))) m
   | Pxoris rd r1 cst =>
-      OK (nextinstr (rs#rd <- (Val.xor rs#r1 (const_high cst)))) m
+      Next (nextinstr (rs#rd <- (Val.xor rs#r1 (const_high cst)))) m
   | Plabel lbl =>
-      OK (nextinstr rs) m
+      Next (nextinstr rs) m
   | Pbuiltin ef args res =>
-      Error    (**r treated specially below *)
+      Stuck    (**r treated specially below *)
   | Pannot ef args =>
-      Error    (**r treated specially below *)
+      Stuck    (**r treated specially below *)
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
-  to the PPC view.  PPC has two different types for registers
-  (integer and float) while LTL et al have only one.  The
-  [ireg_of] and [freg_of] are therefore partial in principle.
-  To keep things simpler, we make them return nonsensical
-  results when applied to a LTL register of the wrong type.
-  The proof in [Asmgenproof] will show that this never happens.
-
-  Note that no LTL register maps to [GPR0].
+  to the PPC view.  Note that no LTL register maps to [GPR0].
   This register is reserved as a temporary to be used
   by the generated PPC code.  *)
 
-Definition ireg_of (r: mreg) : ireg :=
+Definition preg_of (r: mreg) : preg :=
   match r with
   | R3 => GPR3  | R4 => GPR4  | R5 => GPR5  | R6 => GPR6
   | R7 => GPR7  | R8 => GPR8  | R9 => GPR9  | R10 => GPR10
@@ -778,11 +783,6 @@ Definition ireg_of (r: mreg) : ireg :=
   | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28
   | R29 => GPR29 | R30 => GPR30 | R31 => GPR31
   | IT1 => GPR11 | IT2 => GPR12
-  | _ => GPR12 (* should not happen *)
-  end.
-
-Definition freg_of (r: mreg) : freg :=
-  match r with
   | F1 => FPR1  | F2 => FPR2  | F3 => FPR3  | F4 => FPR4
   | F5 => FPR5  | F6 => FPR6  | F7 => FPR7  | F8 => FPR8
   | F9 => FPR9  | F10 => FPR10 | F11 => FPR11
@@ -792,13 +792,6 @@ Definition freg_of (r: mreg) : freg :=
   | F24 => FPR24 | F25 => FPR25 | F26 => FPR26 | F27 => FPR27
   | F28 => FPR28 | F29 => FPR29 | F30 => FPR30 | F31 => FPR31
   | FT1 => FPR0 | FT2 => FPR12 | FT3 => FPR13
-  | _ => FPR0 (* should not happen *)
-  end.
-
-Definition preg_of (r: mreg) :=
-  match mreg_type r with
-  | Tint => IR (ireg_of r)
-  | Tfloat => FR (freg_of r)
   end.
 
 (** Extract the values of the arguments of an external call.
@@ -849,7 +842,7 @@ Inductive step: state -> trace -> state -> Prop :=
       rs PC = Vptr b ofs ->
       Genv.find_funct_ptr ge b = Some (Internal c) ->
       find_instr (Int.unsigned ofs) c = Some i ->
-      exec_instr c i rs m = OK rs' m' ->
+      exec_instr c i rs m = Next rs' m' ->
       step (State rs m) E0 (State rs' m')
   | exec_step_builtin:
       forall b ofs c ef args res rs m t v m',
@@ -968,3 +961,25 @@ Ltac Equalities :=
 (* final states *)
   inv H; inv H0. congruence.
 Qed.
+
+(** Classification functions for processor registers (used in Asmgenproof). *)
+
+Definition data_preg (r: preg) : bool :=
+  match r with
+  | IR GPR0 => false
+  | PC => false    | LR => false    | CTR => false
+  | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false
+  | CARRY => false
+  | _ => true
+  end.
+
+Definition nontemp_preg (r: preg) : bool :=
+  match r with
+  | IR GPR0 => false | IR GPR11 => false | IR GPR12 => false
+  | FR FPR0 => false | FR FPR12 => false | FR FPR13 => false
+  | PC => false      | LR => false       | CTR => false
+  | CR0_0 => false   | CR0_1 => false    | CR0_2 => false    | CR0_3 => false
+  | CARRY => false
+  | _ => true
+  end.
+
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.
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index de9decb..6c95744 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -27,11 +27,9 @@ Require Import Op.
 Require Import Locations.
 Require Import Conventions.
 Require Import Mach.
-Require Import Machsem.
-Require Import Machtyping.
 Require Import Asm.
 Require Import Asmgen.
-Require Import Asmgenretaddr.
+Require Import Asmgenproof0.
 Require Import Asmgenproof1.
 
 Section PRESERVATION.
@@ -67,210 +65,53 @@ Proof
   (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
 
 Lemma functions_transl:
-  forall f b,
+  forall f b tf,
   Genv.find_funct_ptr ge b = Some (Internal f) ->
-  Genv.find_funct_ptr tge b = Some (Internal (transl_function f)).
+  transf_function f = OK tf ->
+  Genv.find_funct_ptr tge b = Some (Internal tf).
 Proof.
   intros. 
-  destruct (functions_translated _ _ H) as [tf [A B]].
-  rewrite A. generalize B. unfold transf_fundef, transf_partial_fundef, transf_function.
-  case (zlt Int.max_unsigned (list_length_z (transl_function f))); simpl; intro.
-  congruence. intro. inv B0. auto.
-Qed.
-
-Lemma functions_transl_no_overflow:
-  forall b f,
-  Genv.find_funct_ptr ge b = Some (Internal f) ->
-  list_length_z (transl_function f) <= Int.max_unsigned.
-Proof.
-  intros. 
-  destruct (functions_translated _ _ H) as [tf [A B]].
-  generalize B. unfold transf_fundef, transf_partial_fundef, transf_function.
-  case (zlt Int.max_unsigned (list_length_z (transl_function f))); simpl; intro.
-  congruence. intro; omega.
+  destruct (functions_translated _ _ H) as [tf' [A B]].
+  rewrite A. monadInv B. f_equal. congruence.
 Qed.
 
 (** * Properties of control flow *)
 
-Lemma find_instr_in:
-  forall c pos i,
-  find_instr pos c = Some i -> In i c.
-Proof.
-  induction c; simpl. intros; discriminate.
-  intros until i. case (zeq pos 0); intros.
-  left; congruence. right; eauto.
-Qed.
-
-Lemma find_instr_tail:
-  forall c1 i c2 pos,
-  code_tail pos c1 (i :: c2) ->
-  find_instr pos c1 = Some i.
-Proof.
-  induction c1; simpl; intros.
-  inv H.
-  destruct (zeq pos 0). subst pos.
-  inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction.
-  inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega.
-  eauto.
-Qed.
-
-Remark code_tail_bounds:
-  forall fn ofs i c,
-  code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn.
+Lemma transf_function_no_overflow:
+  forall f tf,
+  transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned.
 Proof.
-  assert (forall ofs fn c, code_tail ofs fn c ->
-          forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn).
-  induction 1; intros; simpl. 
-  rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega.
-  rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega.
-  eauto.
-Qed.
-
-Lemma code_tail_next:
-  forall fn ofs i c,
-  code_tail ofs fn (i :: c) ->
-  code_tail (ofs + 1) fn c.
-Proof.
-  assert (forall ofs fn c, code_tail ofs fn c ->
-          forall i c', c = i :: c' -> code_tail (ofs + 1) fn c').
-  induction 1; intros.
-  subst c. constructor. constructor.
-  constructor. eauto.
-  eauto.
-Qed.
-
-Lemma code_tail_next_int:
-  forall fn ofs i c,
-  list_length_z fn <= Int.max_unsigned ->
-  code_tail (Int.unsigned ofs) fn (i :: c) ->
-  code_tail (Int.unsigned (Int.add ofs Int.one)) fn c.
-Proof.
-  intros. rewrite Int.add_unsigned.
-  change (Int.unsigned Int.one) with 1.
-  rewrite Int.unsigned_repr. apply code_tail_next with i; auto.
-  generalize (code_tail_bounds _ _ _ _ H0). omega. 
-Qed.
-
-(** [transl_code_at_pc pc fn c] holds if the code pointer [pc] points
-  within the PPC code generated by translating Mach function [fn],
-  and [c] is the tail of the generated code at the position corresponding
-  to the code pointer [pc]. *)
-
-Inductive transl_code_at_pc: val -> block -> Mach.function -> Mach.code -> Prop :=
-  transl_code_at_pc_intro:
-    forall b ofs f c,
-    Genv.find_funct_ptr ge b = Some (Internal f) ->
-    code_tail (Int.unsigned ofs) (transl_function f) (transl_code f c) ->
-    transl_code_at_pc (Vptr b ofs) b f c.
-
-(** The following lemmas show that straight-line executions
-  (predicate [exec_straight]) correspond to correct PPC executions
-  (predicate [exec_steps]) under adequate [transl_code_at_pc] hypotheses. *)
-
-Lemma exec_straight_steps_1:
-  forall fn c rs m c' rs' m',
-  exec_straight tge fn c rs m c' rs' m' ->
-  list_length_z fn <= Int.max_unsigned ->
-  forall b ofs,
-  rs#PC = Vptr b ofs ->
-  Genv.find_funct_ptr tge b = Some (Internal fn) ->
-  code_tail (Int.unsigned ofs) fn c ->
-  plus step tge (State rs m) E0 (State rs' m').
-Proof.
-  induction 1; intros.
-  apply plus_one.
-  econstructor; eauto. 
-  eapply find_instr_tail. eauto.
-  eapply plus_left'.
-  econstructor; eauto. 
-  eapply find_instr_tail. eauto.
-  apply IHexec_straight with b (Int.add ofs Int.one). 
-  auto. rewrite H0. rewrite H3. reflexivity.
-  auto. 
-  apply code_tail_next_int with i; auto.
-  traceEq.
-Qed.
-    
-Lemma exec_straight_steps_2:
-  forall fn c rs m c' rs' m',
-  exec_straight tge fn c rs m c' rs' m' ->
-  list_length_z fn <= Int.max_unsigned ->
-  forall b ofs,
-  rs#PC = Vptr b ofs ->
-  Genv.find_funct_ptr tge b = Some (Internal fn) ->
-  code_tail (Int.unsigned ofs) fn c ->
-  exists ofs',
-     rs'#PC = Vptr b ofs'
-  /\ code_tail (Int.unsigned ofs') fn c'.
-Proof.
-  induction 1; intros.
-  exists (Int.add ofs Int.one). split.
-  rewrite H0. rewrite H2. auto.
-  apply code_tail_next_int with i1; auto.
-  apply IHexec_straight with (Int.add ofs Int.one).
-  auto. rewrite H0. rewrite H3. reflexivity. auto. 
-  apply code_tail_next_int with i; auto.
+  intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. 
+  omega.
 Qed.
 
 Lemma exec_straight_exec:
-  forall fb f c c' rs m rs' m',
-  transl_code_at_pc (rs PC) fb f c ->
-  exec_straight tge (transl_function f)
-                (transl_code f c) rs m c' rs' m' ->
+  forall f c ep tf tc c' rs m rs' m',
+  transl_code_at_pc ge (rs PC) f c ep tf tc ->
+  exec_straight tge tf tc rs m c' rs' m' ->
   plus step tge (State rs m) E0 (State rs' m').
 Proof.
-  intros. inversion H. subst.
+  intros. inv H.
   eapply exec_straight_steps_1; eauto.
-  eapply functions_transl_no_overflow; eauto. 
-  eapply functions_transl; eauto.
+  eapply transf_function_no_overflow; eauto.
+  eapply functions_transl; eauto. 
 Qed.
 
 Lemma exec_straight_at:
-  forall fb f c c' rs m rs' m',
-  transl_code_at_pc (rs PC) fb f c ->
-  exec_straight tge (transl_function f)
-                (transl_code f c) rs m (transl_code f c') rs' m' ->
-  transl_code_at_pc (rs' PC) fb f c'.
+  forall f c ep tf tc c' ep' tc' rs m rs' m',
+  transl_code_at_pc ge (rs PC) f c ep tf tc ->
+  transl_code f c' ep' = OK tc' ->
+  exec_straight tge tf tc rs m tc' rs' m' ->
+  transl_code_at_pc ge (rs' PC) f c' ep' tf tc'.
 Proof.
-  intros. inversion H. subst. 
-  generalize (functions_transl_no_overflow _ _ H2). intro.
-  generalize (functions_transl _ _ H2). intro.
-  generalize (exec_straight_steps_2 _ _ _ _ _ _ _
-                H0 H4 _ _ (sym_equal H1) H5 H3).
+  intros. inv H. 
+  exploit exec_straight_steps_2; eauto. 
+  eapply transf_function_no_overflow; eauto.
+  eapply functions_transl; eauto.
   intros [ofs' [PC' CT']].
   rewrite PC'. constructor; auto.
 Qed.
 
-(** Correctness of the return addresses predicted by
-    [PPCgen.return_address_offset]. *)
-
-Remark code_tail_no_bigger:
-  forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
-Proof.
-  induction 1; simpl; omega.
-Qed.
-
-Remark code_tail_unique:
-  forall fn c pos pos',
-  code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
-Proof.
-  induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  f_equal. eauto.
-Qed.
-
-Lemma return_address_offset_correct:
-  forall b ofs fb f c ofs',
-  transl_code_at_pc (Vptr b ofs) fb f c ->
-  return_address_offset f c ofs' ->
-  ofs' = ofs.
-Proof.
-  intros. inv H0. inv H. 
-  generalize (code_tail_unique _ _ _ _ H1 H7). intro. rewrite H. 
-  apply Int.repr_unsigned.
-Qed.
-
 (** The [find_label] function returns the code tail starting at the
   given label.  A connection with [code_tail] is then established. *)
 
@@ -391,119 +232,137 @@ Qed.
 Hint Rewrite rolm_label: labels.
 
 Remark loadind_label:
-  forall base ofs ty dst k, find_label lbl (loadind base ofs ty dst k) = find_label lbl k.
+  forall base ofs ty dst k c,
+  loadind base ofs ty dst k = OK c ->
+  find_label lbl c = find_label lbl k.
 Proof.
-  intros; unfold loadind. 
-  destruct (Int.eq (high_s ofs) Int.zero); destruct ty; autorewrite with labels; auto.
+  unfold loadind; intros.
+  destruct ty; destruct (Int.eq (high_s ofs) Int.zero); monadInv H;
+  autorewrite with labels; auto.
 Qed.
-Hint Rewrite loadind_label: labels.
 
 Remark storeind_label:
-  forall base ofs ty src k, find_label lbl (storeind base src ofs ty k) = find_label lbl k.
+  forall base ofs ty src k c,
+  storeind base src ofs ty k = OK c ->
+  find_label lbl c = find_label lbl k.
 Proof.
-  intros; unfold storeind.
-  destruct (Int.eq (high_s ofs) Int.zero); destruct ty; autorewrite with labels; auto.
+  unfold storeind; intros.
+  destruct ty; destruct (Int.eq (high_s ofs) Int.zero); monadInv H;
+  autorewrite with labels; auto.
 Qed.
-Hint Rewrite storeind_label: labels.
 
 Remark floatcomp_label:
   forall cmp r1 r2 k, find_label lbl (floatcomp cmp r1 r2 k) = find_label lbl k.
 Proof.
   intros; unfold floatcomp. destruct cmp; reflexivity.
 Qed.
+Hint Rewrite floatcomp_label: labels.
 
 Remark transl_cond_label:
-  forall cond args k, find_label lbl (transl_cond cond args k) = find_label lbl k.
+  forall cond args k c,
+  transl_cond cond args k = OK c -> find_label lbl c = find_label lbl k.
 Proof.
-  intros; unfold transl_cond.
-  destruct cond; (destruct args; 
-  [try reflexivity | destruct args;
-  [try reflexivity | destruct args; try reflexivity]]).
-  case (Int.eq (high_s i) Int.zero). reflexivity. 
-  autorewrite with labels; reflexivity.
-  case (Int.eq (high_u i) Int.zero). reflexivity. 
-  autorewrite with labels; reflexivity.
-  apply floatcomp_label. apply floatcomp_label.
-  apply andimm_base_label. apply andimm_base_label.
+  unfold transl_cond; intros; destruct cond; 
+  (destruct args; 
+  [try discriminate | destruct args;
+  [try discriminate | destruct args; try discriminate]]);
+  monadInv H; autorewrite with labels; auto.
+  destruct (Int.eq (high_s i) Int.zero); inv EQ0; autorewrite with labels; auto.
+  destruct (Int.eq (high_u i) Int.zero); inv EQ0; autorewrite with labels; auto.
 Qed.
-Hint Rewrite transl_cond_label: labels.
 
 Remark transl_cond_op_label:
-  forall c args r k,
-  find_label lbl (transl_cond_op c args r k) = find_label lbl k.
+  forall cond args r k c,
+  transl_cond_op cond args r k = OK c -> find_label lbl c = find_label lbl k.
 Proof.
-  intros c args.
-  unfold transl_cond_op. destruct (classify_condition c args); intros; auto.
-  autorewrite with labels. destruct (snd (crbit_for_cond c)); auto. 
+  unfold transl_cond_op; intros; destruct (classify_condition cond args);
+  monadInv H; auto.
+  erewrite transl_cond_label. 2: eauto. 
+  destruct (snd (crbit_for_cond c0)); auto.
 Qed.
-Hint Rewrite transl_cond_op_label: labels.
 
 Remark transl_op_label:
-  forall op args r k, find_label lbl (transl_op op args r k) = find_label lbl k.
+  forall op args r k c,
+  transl_op op args r k = OK c -> find_label lbl c = find_label lbl k.
 Proof.
-  intros; unfold transl_op;
-  destruct op; destruct args; try (destruct args); try (destruct args); try (destruct args);
-  try reflexivity; autorewrite with labels; try reflexivity.
-  case (mreg_type m); reflexivity.
-  case (symbol_is_small_data i i0); reflexivity.
-  case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity.
-  case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity.
-  destruct (mreg_eq m r); reflexivity.
+  unfold transl_op; intros; destruct op; try (eapply transl_cond_op_label; eauto; fail);
+  (destruct args; 
+  [try discriminate | destruct args;
+  [try discriminate | destruct args; try discriminate]]);
+  try (monadInv H); autorewrite with labels; auto.
+  destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; auto.
+  destruct (symbol_is_small_data i i0); auto.
+  destruct (Int.eq (high_s i) Int.zero); autorewrite with labels; auto.
+  destruct (Int.eq (high_s i) Int.zero); autorewrite with labels; auto.
 Qed.
-Hint Rewrite transl_op_label: labels.
 
-Remark transl_load_store_label:
+Remark transl_memory_access_label:
   forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
-         addr args temp k,
+         addr args temp k c,
+  transl_memory_access mk1 mk2 addr args temp k = OK c ->
   (forall c r, is_label lbl (mk1 c r) = false) ->
   (forall r1 r2, is_label lbl (mk2 r1 r2) = false) ->
-  find_label lbl (transl_load_store mk1 mk2 addr args temp k) = find_label lbl k.
-Proof.
-  intros; unfold transl_load_store.
-  destruct addr; destruct args; try (destruct args); try (destruct args);
-  try reflexivity.
-  destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto.
+  find_label lbl c = find_label lbl k.
+Proof.
+  unfold transl_memory_access; intros; destruct addr; 
+  (destruct args; 
+  [try discriminate | destruct args;
+  [try discriminate | destruct args; try discriminate]]);
+  monadInv H; autorewrite with labels; auto.
+  destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H0; auto.
+  simpl; rewrite H1; auto.
+  destruct (symbol_is_small_data i i0); simpl; rewrite H0; auto.
   simpl; rewrite H0; auto.
-  destruct (symbol_is_small_data i i0); simpl; rewrite H; auto.
-  simpl; rewrite H; auto.
-  destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto.
+  destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H0; auto.
 Qed.
-Hint Rewrite transl_load_store_label: labels.
 
 Lemma transl_instr_label:
-  forall f i k,
-  find_label lbl (transl_instr f i k) = 
-    if Mach.is_label lbl i then Some k else find_label lbl k.
-Proof.
-  intros. generalize (Mach.is_label_correct lbl i). 
-  case (Mach.is_label lbl i); intro.
-  subst i. simpl. rewrite peq_true. auto.
-  destruct i; simpl; autorewrite with labels; try reflexivity.
-  destruct m; rewrite transl_load_store_label; intros; reflexivity. 
-  destruct m; rewrite transl_load_store_label; intros; reflexivity. 
-  destruct s0; reflexivity.
-  destruct s0; reflexivity.
-  rewrite peq_false. auto. congruence.
-  case (snd (crbit_for_cond c)); reflexivity.
+  forall f i ep k c,
+  transl_instr f i ep k = OK c ->
+  find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k.
+Proof.
+  unfold transl_instr, Mach.is_label; intros; destruct i; try (monadInv H);
+  autorewrite with labels; auto.
+  eapply loadind_label; eauto.
+  eapply storeind_label; eauto.
+  destruct ep. eapply loadind_label; eauto.
+  monadInv H. transitivity (find_label lbl x); eapply loadind_label; eauto. 
+  eapply transl_op_label; eauto.
+  destruct m; monadInv H; rewrite (transl_memory_access_label _ _ _ _ _ _ _ EQ0); auto.
+  destruct m; monadInv H; rewrite (transl_memory_access_label _ _ _ _ _ _ _ EQ0); auto.
+  destruct s0; monadInv H; auto.
+  destruct s0; monadInv H; auto.
+  erewrite transl_cond_label. 2: eauto. destruct (snd (crbit_for_cond c0)); auto.
 Qed.
 
 Lemma transl_code_label:
-  forall f c,
-  find_label lbl (transl_code f c) = 
-    option_map (transl_code f) (Mach.find_label lbl c).
+  forall f c ep tc,
+  transl_code f c ep = OK tc ->
+  match Mach.find_label lbl c with
+  | None => find_label lbl tc = None
+  | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc'
+  end.
 Proof.
   induction c; simpl; intros.
-  auto. rewrite transl_instr_label.
-  case (Mach.is_label lbl a). reflexivity.
-  auto.
+  inv H. auto.
+  monadInv H. rewrite (transl_instr_label _ _ _ _ _ EQ0).
+  generalize (Mach.is_label_correct lbl a). 
+  destruct (Mach.is_label lbl a); intros.
+  subst a. simpl in EQ. exists x; auto.
+  eapply IHc; eauto.
 Qed.
 
 Lemma transl_find_label:
-  forall f,
-  find_label lbl (transl_function f) = 
-    option_map (transl_code f) (Mach.find_label lbl f.(fn_code)).
+  forall f tf,
+  transf_function f = OK tf ->
+  match Mach.find_label lbl f.(Mach.fn_code) with
+  | None => find_label lbl tf = None
+  | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc
+  end.
 Proof.
-  intros. unfold transl_function. simpl. apply transl_code_label.
+  intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0.
+  monadInv EQ. simpl.
+  eapply transl_code_label; eauto. 
 Qed.
 
 End TRANSL_LABEL.
@@ -512,28 +371,26 @@ End TRANSL_LABEL.
   transition in the generated PPC code. *)
 
 Lemma find_label_goto_label:
-  forall f lbl rs m c' b ofs,
+  forall f tf lbl rs m c' b ofs,
   Genv.find_funct_ptr ge b = Some (Internal f) ->
+  transf_function f = OK tf ->
   rs PC = Vptr b ofs ->
-  Mach.find_label lbl f.(fn_code) = Some c' ->
-  exists rs',
-    goto_label (transl_function f) lbl rs m = OK rs' m  
-  /\ transl_code_at_pc (rs' PC) b f c'
+  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
+  exists tc', exists rs',
+    goto_label tf lbl rs m = Next rs' m  
+  /\ transl_code_at_pc ge (rs' PC) f c' false tf tc'
   /\ forall r, r <> PC -> rs'#r = rs#r.
 Proof.
-  intros. 
-  generalize (transl_find_label lbl f).
-  rewrite H1; simpl. intro.
-  generalize (label_pos_code_tail lbl (transl_function f) 0 
-                 (transl_code f c') H2).
-  intros [pos' [A [B C]]].
-  exists (rs#PC <- (Vptr b (Int.repr pos'))).
-  split. unfold goto_label. rewrite A. rewrite H0. auto.
+  intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. 
+  intros [tc [A B]].
+  exploit label_pos_code_tail; eauto. instantiate (1 := 0).
+  intros [pos' [P [Q R]]].
+  exists tc; exists (rs#PC <- (Vptr b (Int.repr pos'))).
+  split. unfold goto_label. rewrite P. rewrite H1. auto.
   split. rewrite Pregmap.gss. constructor; auto. 
-  rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in B.
-  auto. omega. 
-  generalize (functions_transl_no_overflow _ _ H). 
-  omega.
+  rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in Q.
+  auto. omega.
+  generalize (transf_function_no_overflow _ _ H0). omega.
   intros. apply Pregmap.gso; auto.
 Qed.
 
@@ -555,108 +412,92 @@ Qed.
 - Mach register values and PPC register values agree.
 *)
 
-Inductive match_stack: list Machsem.stackframe -> Prop :=
-  | match_stack_nil:
-      match_stack nil
-  | match_stack_cons: forall fb sp ra c s f,
-      Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      wt_function f ->
-      incl c f.(fn_code) ->
-      transl_code_at_pc ra fb f c ->
-      sp <> Vundef ->
-      ra <> Vundef ->
-      match_stack s ->
-      match_stack (Stackframe fb sp ra c :: s).
-
-Inductive match_states: Machsem.state -> Asm.state -> Prop :=
+Inductive match_states: Mach.state -> Asm.state -> Prop :=
   | match_states_intro:
-      forall s fb sp c ms m rs m' f
-        (STACKS: match_stack s)
-        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
-        (WTF: wt_function f)
-        (INCL: incl c f.(fn_code))
-        (AT: transl_code_at_pc (rs PC) fb f c)
-        (AG: agree ms sp rs)
-        (MEXT: Mem.extends m m'),
-      match_states (Machsem.State s fb sp c ms m)
+      forall s f sp c ep ms m m' rs tf tc ra
+        (STACKS: match_stack ge s m m' ra sp)
+        (MEXT: Mem.extends m m')
+        (AT: transl_code_at_pc ge (rs PC) f c ep tf tc)
+        (AG: agree ms (Vptr sp Int.zero) rs)
+        (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra)
+        (DXP: ep = true -> rs#GPR11 = parent_sp s),
+      match_states (Mach.State s f (Vptr sp Int.zero) c ms m)
                    (Asm.State rs m')
   | match_states_call:
-      forall s fb ms m rs m'
-        (STACKS: match_stack s)
-        (AG: agree ms (parent_sp s) rs)
+      forall s fd ms m m' rs fb
+        (STACKS: match_stack ge s m m' (rs LR) (Mem.nextblock m))
         (MEXT: Mem.extends m m')
+        (AG: agree ms (parent_sp s) rs)
         (ATPC: rs PC = Vptr fb Int.zero)
-        (ATLR: rs LR = parent_ra s),
-      match_states (Machsem.Callstate s fb ms m)
+        (FUNCT: Genv.find_funct_ptr ge fb = Some fd)
+        (WTRA: Val.has_type (rs LR) Tint),
+      match_states (Mach.Callstate s fd ms m)
                    (Asm.State rs m')
   | match_states_return:
-      forall s ms m rs m'
-        (STACKS: match_stack s)
-        (AG: agree ms (parent_sp s) rs)
+      forall s ms m m' rs
+        (STACKS: match_stack ge s m m' (rs PC) (Mem.nextblock m))
         (MEXT: Mem.extends m m')
-        (ATPC: rs PC = parent_ra s),
-      match_states (Machsem.Returnstate s ms m)
+        (AG: agree ms (parent_sp s) rs),
+      match_states (Mach.Returnstate s ms m)
                    (Asm.State rs m').
 
 Lemma exec_straight_steps:
-  forall s fb sp m1' f c1 rs1 c2 m2 m2' ms2,
-  match_stack s ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  wt_function f ->
-  incl c2 f.(fn_code) ->
-  transl_code_at_pc (rs1 PC) fb f c1 ->
-  (exists rs2,
-     exec_straight tge (transl_function f) (transl_code f c1) rs1 m1' (transl_code f c2) rs2 m2'
-     /\ agree ms2 sp rs2) ->
+  forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 ra,
+  match_stack ge s m2 m2' ra sp ->
   Mem.extends m2 m2' ->
+  retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra ->
+  transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc ->
+  (forall k c (TR: transl_instr f i ep k = OK c),
+   exists rs2,
+       exec_straight tge tf c rs1 m1' k rs2 m2'
+    /\ agree ms2 (Vptr sp Int.zero) rs2
+    /\ (r11_is_parent ep i = true -> rs2#GPR11 = parent_sp s)) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Machsem.State s fb sp c2 ms2 m2) st'.
+  match_states (Mach.State s f (Vptr sp Int.zero) c ms2 m2) st'.
 Proof.
-  intros. destruct H4 as [rs2 [A B]].
+  intros. inversion H2; subst. monadInv H7. 
+  exploit H3; eauto. intros [rs2 [A [B C]]]. 
   exists (State rs2 m2'); split.
-  eapply exec_straight_exec; eauto.
+  eapply exec_straight_exec; eauto. 
   econstructor; eauto. eapply exec_straight_at; eauto.
 Qed.
 
-Lemma exec_straight_steps_bis:
-  forall s fb sp m1' f c1 rs1 c2 m2 ms2,
-  match_stack s ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  wt_function f ->
-  incl c2 f.(fn_code) ->
-  transl_code_at_pc (rs1 PC) fb f c1 ->
-  (exists m2',
-      Mem.extends m2 m2'
-   /\ exists rs2,
-        exec_straight tge (transl_function f) (transl_code f c1) rs1 m1' (transl_code f c2) rs2 m2'
-        /\ agree ms2 sp rs2) ->
+Lemma exec_straight_steps_goto:
+  forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c' ra,
+  match_stack ge s m2 m2' ra sp ->
+  Mem.extends m2 m2' ->
+  retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra ->
+  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
+  transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc ->
+  r11_is_parent ep i = false ->
+  (forall k c (TR: transl_instr f i ep k = OK c),
+   exists jmp, exists k', exists rs2,
+       exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
+    /\ agree ms2 (Vptr sp Int.zero) rs2
+    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Machsem.State s fb sp c2 ms2 m2) st'.
+  match_states (Mach.State s f (Vptr sp Int.zero) c' ms2 m2) st'.
 Proof.
-  intros. destruct H4 as [m2' [A B]]. 
-  eapply exec_straight_steps; eauto.
-Qed.
-
-Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
-Proof. induction 1; simpl. congruence. auto. Qed.
-
-Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef.
-Proof. induction 1; simpl. unfold Vzero. congruence. auto. Qed.
-
-Lemma lessdef_parent_sp:
-  forall s v,
-  match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
-Proof.
-  intros. inv H0. auto. exploit parent_sp_def; eauto. tauto.
-Qed.
-
-Lemma lessdef_parent_ra:
-  forall s v,
-  match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s.
-Proof.
-  intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
+  intros. inversion H3; subst. monadInv H9.
+  exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].
+  generalize (functions_transl _ _ _ H7 H8); intro FN.
+  generalize (transf_function_no_overflow _ _ H8); intro NOOV.
+  exploit exec_straight_steps_2; eauto. 
+  intros [ofs' [PC2 CT2]].
+  exploit find_label_goto_label; eauto. 
+  intros [tc' [rs3 [GOTO [AT' OTH]]]].
+  exists (State rs3 m2'); split.
+  eapply plus_right'.
+  eapply exec_straight_steps_1; eauto. 
+  econstructor; eauto.
+  eapply find_instr_tail. eauto. 
+  rewrite C. eexact GOTO.
+  traceEq.
+  econstructor; eauto.
+  apply agree_exten with rs2; auto with asmgen.
+  congruence.
 Qed.
 
 (** We need to show that, in the simulation diagram, we cannot
@@ -667,448 +508,285 @@ Qed.
   So, the following integer measure will suffice to rule out
   the unwanted behaviour. *)
 
-Definition measure (s: Machsem.state) : nat :=
+Definition measure (s: Mach.state) : nat :=
   match s with
-  | Machsem.State _ _ _ _ _ _ => 0%nat
-  | Machsem.Callstate _ _ _ _ => 0%nat
-  | Machsem.Returnstate _ _ _ => 1%nat
+  | Mach.State _ _ _ _ _ _ => 0%nat
+  | Mach.Callstate _ _ _ _ => 0%nat
+  | Mach.Returnstate _ _ _ => 1%nat
   end.
 
-(** We show the simulation diagram by case analysis on the Mach transition
-  on the left.  Since the proof is large, we break it into one lemma
-  per transition. *)
-
-Definition exec_instr_prop (s1: Machsem.state) (t: trace) (s2: Machsem.state) : Prop :=
-  forall s1' (MS: match_states s1 s1'),
-  (exists s2', plus step tge s1' t s2' /\ match_states s2 s2')
-  \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat.
-
-
-Lemma exec_Mlabel_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
-         (m : mem),
-  exec_instr_prop (Machsem.State s fb sp (Mlabel lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c ms m).
+Remark preg_of_not_GPR11: forall r, negb (mreg_eq r IT1) = true -> IR GPR11 <> preg_of r.
 Proof.
-  intros; red; intros; inv MS.
-  left; eapply exec_straight_steps; eauto with coqlib.
-  exists (nextinstr rs); split.
-  simpl. apply exec_straight_one. reflexivity. reflexivity.
-  apply agree_nextinstr; auto.
+  intros. change (IR GPR11) with (preg_of IT1). red; intros. 
+  exploit preg_of_injective; eauto. intros; subst r; discriminate.
 Qed.
 
-Lemma exec_Mgetstack_prop:
-  forall (s : list stackframe) (fb : block) (sp : val) (ofs : int)
-         (ty : typ) (dst : mreg) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (v : val),
-  load_stack m sp ty ofs = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0
-                  (Machsem.State s fb sp c (Regmap.set dst v ms) m).
-Proof.
-  intros; red; intros; inv MS.
-  unfold load_stack in H. 
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inversion WTI.
-  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
-  rewrite (sp_val _ _ _ AG) in A.
-  exploit (loadind_correct tge (transl_function f) GPR1 ofs ty dst (transl_code f c) rs m' v').
-  auto. auto. congruence. 
-  intros [rs2 [EX [RES OTH]]].
-  left; eapply exec_straight_steps; eauto with coqlib.
-  simpl. exists rs2; split. auto. 
-  apply agree_set_mreg with rs; auto with ppcgen. congruence. 
-Qed.
+(** This is the simulation diagram.  We prove it by case analysis on the Mach transition. *)
 
-Lemma exec_Msetstack_prop:
-  forall (s : list stackframe) (fb : block) (sp : val) (src : mreg)
-         (ofs : int) (ty : typ) (c : list Mach.instruction)
-         (ms : mreg -> val) (m m' : mem),
-  store_stack m sp ty ofs (ms src) = Some m' ->
-  exec_instr_prop (Machsem.State s fb sp (Msetstack src ofs ty :: c) ms m) E0
-                  (Machsem.State s fb sp c ms m').
+Theorem step_simulation:
+  forall S1 t S2, Mach.step ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1'),
+  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
+  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
 Proof.
-  intros; red; intros; inv MS.
-  unfold store_stack in H. 
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inv WTI.
-  generalize (preg_val ms sp rs src AG). intro. 
-  exploit Mem.storev_extends; eauto.
-  intros [m2' [A B]].
+  induction 1; intros; inv MS.
+
+- (* Mlabel *)
+  left; eapply exec_straight_steps; eauto; intros. 
+  monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
+  split. apply agree_nextinstr; auto. simpl; congruence.
+
+- (* Mgetstack *)
+  unfold load_stack in H.
+  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
   rewrite (sp_val _ _ _ AG) in A.
-  exploit (storeind_correct tge (transl_function f) GPR1 ofs (mreg_type src)
-                src (transl_code f c) rs).
-  eauto. auto. congruence.
-  intros [rs2 [EX OTH]].
-  left; eapply exec_straight_steps; eauto with coqlib.
-  exists rs2; split; auto.
-  apply agree_exten with rs; auto with ppcgen.
-Qed.
+  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
+  exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
+  exists rs'; split. eauto.
+  split. eapply agree_set_mreg; eauto with asmgen. congruence.
+  simpl; congruence.
 
-Lemma exec_Mgetparam_prop:
-  forall (s : list stackframe) (fb : block) (f: Mach.function) (sp : val)
-         (ofs : int) (ty : typ) (dst : mreg) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (v : val),
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (parent_sp s) ty ofs = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
-                  (Machsem.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inv WTI.
-  unfold load_stack in *. simpl in H0. 
+- (* Msetstack *)
+  unfold store_stack in H.
+  assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
+  exploit Mem.storev_extends; eauto. intros [m2' [A B]]. 
+  left; eapply exec_straight_steps; eauto.
+  eapply match_stack_storev; eauto. 
+  eapply retaddr_stored_at_storev; eauto. 
+  rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
+  exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
+  exists rs'; split. eauto.
+  split. change (undef_setstack rs) with rs. apply agree_exten with rs0; auto with asmgen.
+  simpl; intros. rewrite Q; auto with asmgen.
+
+- (* Mgetparam *)
+  unfold load_stack in *. 
+  exploit Mem.loadv_extends. eauto. eexact H. auto. 
+  intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+  exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'.
   exploit Mem.loadv_extends. eauto. eexact H0. auto. 
-  intros [parent' [A B]].
-  exploit Mem.loadv_extends. eauto. eexact H1. 
-  instantiate (1 := (Val.add parent' (Vint ofs))). 
-  inv B. auto. simpl; auto.
   intros [v' [C D]].
-  left; eapply exec_straight_steps; eauto with coqlib. simpl. 
-  set (rs1 := nextinstr (rs#GPR11 <- parent')).
-  exploit (loadind_correct tge (transl_function f) GPR11 ofs (mreg_type dst) dst (transl_code f c) rs1 m' v').
-  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. auto. congruence.
-  intros [rs2 [U [V W]]].
-  exists rs2; split.
-  apply exec_straight_step with rs1 m'.
-  simpl. unfold load1. simpl. rewrite gpr_or_zero_not_zero.
-  rewrite <- (sp_val _ _ _ AG). rewrite A. auto. congruence. auto. 
-  auto.
-  apply agree_set_mreg with rs1; auto with ppcgen. 
-  unfold rs1. change (IR GPR11) with (preg_of IT1). 
-  apply agree_nextinstr. apply agree_set_mreg with rs; auto with ppcgen.
-  intros. apply Pregmap.gso; auto with ppcgen.
-  congruence.
-Qed.
-
-Lemma exec_Mop_prop:
-  forall (s : list stackframe) (fb : block) (sp : val) (op : operation)
-         (args : list mreg) (res : mreg) (c : list Mach.instruction)
-         (ms : mreg -> val) (m : mem) (v : val),
-  eval_operation ge sp op ms ## args m = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mop op args res :: c) ms m) E0
-                  (Machsem.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
-Proof.
-  intros; red; intros; inv MS.
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI.
-  left; eapply exec_straight_steps; eauto with coqlib.
-  simpl. eapply transl_op_correct; eauto.
-  rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
-Qed.
-
-Remark loadv_8_signed_unsigned:
-  forall m a v,
-  Mem.loadv Mint8signed m a = Some v ->
-  exists v', Mem.loadv Mint8unsigned m a = Some v' /\ v = Val.sign_ext 8 v'.
-Proof.
-  unfold Mem.loadv; intros. destruct a; try congruence.
-  generalize (Mem.load_int8_signed_unsigned m b (Int.unsigned i)).
-  rewrite H. destruct (Mem.load Mint8unsigned m b (Int.unsigned i)).
-  simpl; intros. exists v0; split; congruence.
+Opaque loadind.
+  left; eapply exec_straight_steps; eauto; intros.
+  destruct ep; simpl in TR. 
+(* GPR11 contains parent *)
+  exploit loadind_correct. eexact TR.
+  instantiate (2 := rs0). rewrite DXP; eauto.  congruence.
+  intros [rs1 [P [Q R]]].
+  exists rs1; split. eauto. 
+  split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
+  simpl; intros. rewrite R; auto with asmgen. 
+  apply preg_of_not_GPR11; auto.
+(* GPR11 does not contain parent *)
+  monadInv TR.  
+  exploit loadind_correct. eexact EQ0. eauto. congruence. intros [rs1 [P [Q R]]]. simpl in Q.
+  exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. congruence.
+  intros [rs2 [S [T U]]]. 
+  exists rs2; split. eapply exec_straight_trans; eauto.
+  split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
+  instantiate (1 := rs1#GPR11 <- (rs2#GPR11)). intros.
+  rewrite Pregmap.gso; auto with asmgen.
+  congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' GPR11). congruence. auto with asmgen. 
+  simpl; intros. rewrite U; auto with asmgen. 
+  apply preg_of_not_GPR11; auto.
+
+- (* Mop *)
+  assert (eval_operation tge (Vptr sp0 Int.zero) op rs##args m = Some v). 
+    rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
+  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0.
+  intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. 
+  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
+  exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].
+  exists rs2; split. eauto. split. auto. 
+  simpl. destruct op; try congruence. destruct ep; simpl; try congruence. intros. 
+  rewrite R; auto. apply preg_of_not_GPR11; auto.
+
+- (* Mload *)
+  assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). 
+    rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
+  intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+  exploit Mem.loadv_extends; eauto. intros [v' [C D]].
+  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
+  exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. 
+  exists rs2; split. eauto.
+  split. eapply agree_set_undef_mreg; eauto. congruence.
+  intros; auto with asmgen. 
   simpl; congruence.
-Qed.
 
-Lemma exec_Mload_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (chunk : memory_chunk) (addr : addressing) (args : list mreg)
-         (dst : mreg) (c : list Mach.instruction) (ms : mreg -> val)
-         (m : mem) (a v : val),
-  eval_addressing ge sp addr ms ## args = Some a ->
-  Mem.loadv chunk m a = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mload chunk addr args dst :: c) ms m)
-               E0 (Machsem.State s fb sp c (Regmap.set dst v (undef_temps ms)) m).
-Proof.
-  intros; red; intros; inv MS.
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI; inversion WTI.
-  assert (eval_addressing tge sp addr ms##args = Some a).
+- (* Mstore *)
+  assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). 
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
-  left; eapply exec_straight_steps; eauto with coqlib;
-  destruct chunk; simpl; simpl in H6;
-  (* all cases but Mint8signed and Mfloat64 *)
-  try (eapply transl_load_correct; eauto;
-       intros; simpl; unfold preg_of; rewrite H6; auto; fail).
-  (* Mint8signed *)
-  exploit loadv_8_signed_unsigned; eauto. intros [v' [LOAD EQ]].
-  assert (X1: forall (cst : constant) (r1 : ireg) (rs1 : regset),
-    exec_instr tge (transl_function f) (Plbz (ireg_of dst) cst r1) rs1 m' =
-    load1 tge Mint8unsigned (preg_of dst) cst r1 rs1 m').
-    intros. unfold preg_of; rewrite H6. reflexivity. 
-  assert (X2: forall (r1 r2 : ireg) (rs1 : regset),
-    exec_instr tge (transl_function f) (Plbzx (ireg_of dst) r1 r2) rs1 m' =
-    load2 Mint8unsigned (preg_of dst) r1 r2 rs1 m').
-    intros. unfold preg_of; rewrite H6. reflexivity.
-  exploit transl_load_correct; eauto. 
-  intros [rs2 [EX1 AG1]].
-  econstructor; split. 
-  eapply exec_straight_trans. eexact EX1.
-  apply exec_straight_one. simpl. eauto. auto.
-  apply agree_nextinstr.
-  eapply agree_set_twice_mireg; eauto.
-  rewrite EQ. apply Val.sign_ext_lessdef. 
-  generalize (ireg_val _ _ _ dst AG1 H6). rewrite Regmap.gss. auto.
-  (* Mfloat64 *)
-  exploit Mem.loadv_float64al32; eauto. intros. clear H0.
-  eapply transl_load_correct; eauto;
-  intros; simpl; unfold preg_of; rewrite H6; auto.
-Qed.
-
-Lemma storev_8_signed_unsigned:
-  forall m a v,
-  Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
-Proof.
-  intros. unfold Mem.storev. destruct a; auto.
-  apply Mem.store_signed_unsigned_8.
-Qed.
-
-Lemma storev_16_signed_unsigned:
-  forall m a v,
-  Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
-Proof.
-  intros. unfold Mem.storev. destruct a; auto.
-  apply Mem.store_signed_unsigned_16.
-Qed.
-
-Lemma exec_Mstore_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (chunk : memory_chunk) (addr : addressing) (args : list mreg)
-         (src : mreg) (c : list Mach.instruction) (ms : mreg -> val)
-         (m m' : mem) (a : val),
-  eval_addressing ge sp addr ms ## args = Some a ->
-  Mem.storev chunk m a (ms src) = Some m' ->
-  exec_instr_prop (Machsem.State s fb sp (Mstore chunk addr args src :: c) ms m) E0
-                  (Machsem.State s fb sp c (undef_temps ms) m').
-Proof.
-  intros; red; intros; inv MS.
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI; inv WTI.
-  rewrite <- (eval_addressing_preserved _ _ symbols_preserved) in H.
-  left; eapply exec_straight_steps_bis; eauto with coqlib.
-  destruct chunk; simpl; simpl in H6;
-  try (generalize (Mem.storev_float64al32 _ _ _ _ H0); intros);
-  try (rewrite storev_8_signed_unsigned in H0);
-  try (rewrite storev_16_signed_unsigned in H0);
-  simpl; eapply transl_store_correct; eauto;
-  (unfold preg_of; rewrite H6; intros; econstructor; eauto).
-  split. simpl. rewrite H1. eauto. intros; apply Pregmap.gso; auto.
-  split. simpl. rewrite H1. eauto. intros; apply Pregmap.gso; auto.
-Qed.
+  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
+  intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+  assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
+  exploit Mem.storev_extends; eauto. intros [m2' [C D]].
+  left; eapply exec_straight_steps; eauto.
+  eapply match_stack_storev; eauto.
+  eapply retaddr_stored_at_storev; eauto.
+  intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. 
+  exists rs2; split. eauto.
+  split. eapply agree_exten_temps; eauto. intros; auto with asmgen. 
+  simpl; congruence.
 
-Lemma exec_Mcall_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (sig : signature) (ros : mreg + ident) (c : Mach.code)
-         (ms : Mach.regset) (m : mem) (f : function) (f' : block)
-         (ra : int),
-  find_function_ptr ge ros ms = Some f' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  return_address_offset f c ra ->
-  exec_instr_prop (Machsem.State s fb sp (Mcall sig ros :: c) ms m) E0
-                  (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' ms m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inversion WTI.
+- (* Mcall *)
   inv AT. 
-  assert (NOOV: list_length_z (transl_function f) <= Int.max_unsigned).
-    eapply functions_transl_no_overflow; eauto.
-  destruct ros; simpl in H; simpl transl_code in H7.
-  (* Indirect call *)
-  generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1.
+  assert (NOOV: list_length_z tf <= Int.max_unsigned).
+    eapply transf_function_no_overflow; eauto.
+  destruct ros as [rf|fid]; simpl in H; monadInv H3.
++ (* Indirect call *)
+  exploit Genv.find_funct_inv; eauto. intros [bf EQ2].
+  rewrite EQ2 in H; rewrite  Genv.find_funct_find_funct_ptr in H. 
+  assert (rs0 x0 = Vptr bf Int.zero).
+    exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto.
+  generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1.
   generalize (code_tail_next_int _ _ _ _ NOOV CT1). intro CT2.
-  assert (P1: ms m0 = Vptr f' Int.zero).
-    destruct (ms m0); try congruence. 
-    generalize H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence.
-  assert (P2: rs (ireg_of m0) = Vptr f' Int.zero).
-    generalize (ireg_val _ _ _ m0 AG H3).
-    rewrite P1. intro. inv H2. auto.
-  set (rs2 := nextinstr (rs#CTR <- (Vptr f' Int.zero))).
-  set (rs3 := rs2 #LR <- (Val.add rs2#PC Vone) #PC <- (Vptr f' Int.zero)).
-  assert (ATPC: rs3 PC = Vptr f' Int.zero). reflexivity.
-  exploit return_address_offset_correct; eauto. constructor; eauto. 
-  intro RA_EQ.
-  assert (ATLR: rs3 LR = Vptr fb ra).
-    rewrite RA_EQ.
-    change (rs3 LR) with (Val.add (Val.add (rs PC) Vone) Vone).
-    rewrite <- H5. reflexivity. 
-  assert (AG3: agree ms sp rs3). 
-    unfold rs3, rs2; auto 8 with ppcgen.
-  left; exists (State rs3 m'); split.
-  apply plus_left with E0 (State rs2 m') E0. 
-    econstructor. eauto. apply functions_transl. eexact H0. 
-    eapply find_instr_tail. eauto.
-    simpl. rewrite P2. auto.
-  apply star_one. econstructor.
-    change (rs2 PC) with (Val.add (rs PC) Vone). rewrite <- H5.
-    simpl. auto.
-    apply functions_transl. eexact H0.
-    eapply find_instr_tail. eauto.
-    simpl. reflexivity.
+  assert (TCA: transl_code_at_pc ge (Vptr b (Int.add (Int.add ofs Int.one) Int.one)) f c false tf x).
+    econstructor; eauto. 
+  left; econstructor; split.
+  eapply plus_left. eapply exec_step_internal. eauto.
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
+  simpl. eauto.
+  apply star_one. eapply exec_step_internal. Simpl. rewrite <- H0; simpl; eauto.
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
+  simpl. eauto.
   traceEq.
+  econstructor; eauto. 
   econstructor; eauto.
-  econstructor; eauto with coqlib.
-  rewrite RA_EQ. econstructor; eauto.
-  eapply agree_sp_def; eauto. congruence.
-
-  (* Direct call *)
-  generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1.
-  set (rs2 := rs #LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset tge i Int.zero)).
-  assert (ATPC: rs2 PC = Vptr f' Int.zero).
-    change (rs2 PC) with (symbol_offset tge i Int.zero).
-    unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto.
-  exploit return_address_offset_correct; eauto. constructor; eauto. 
-  intro RA_EQ.
-  assert (ATLR: rs2 LR = Vptr fb ra).
-    rewrite RA_EQ.
-    change (rs2 LR) with (Val.add (rs PC) Vone).
-    rewrite <- H5. reflexivity. 
-  assert (AG2: agree ms sp rs2). 
-    unfold rs2; auto 8 with ppcgen.
-  left; exists (State rs2 m'); split.
-  apply plus_one. econstructor. 
-    eauto.
-    apply functions_transl. eexact H0. 
-    eapply find_instr_tail. eauto.
-    simpl. reflexivity.
-  econstructor; eauto with coqlib.
-  econstructor; eauto with coqlib.
-  rewrite RA_EQ. econstructor; eauto.
-  eapply agree_sp_def; eauto. congruence.
-Qed.
-
-Lemma exec_Mtailcall_prop:
-  forall (s : list stackframe) (fb stk : block) (soff : int)
-         (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m',
-  find_function_ptr ge ros ms = Some f' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
-  Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-  exec_instr_prop
-          (Machsem.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
-          (Callstate s f' ms m').
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inversion WTI.
-  inversion AT. subst b f0 c0.
-  assert (NOOV: list_length_z (transl_function f) <= Int.max_unsigned).
-    eapply functions_transl_no_overflow; eauto.
-  exploit Mem.free_parallel_extends; eauto.
-  intros [m2' [FREE' EXT']].
-  unfold load_stack in *. simpl in H1; simpl in H2.
-  exploit Mem.load_extends. eexact MEXT. eexact H1.
-  intros [parent' [LOAD1 LD1]].
-  rewrite (lessdef_parent_sp s parent' STACKS LD1) in LOAD1.
-  exploit Mem.load_extends. eexact MEXT. eexact H2.
-  intros [ra' [LOAD2 LD2]].
-  rewrite (lessdef_parent_ra s ra' STACKS LD2) in LOAD2.
-  destruct ros; simpl in H; simpl in H9.
-  (* Indirect call *)
-  assert (P1: ms m0 = Vptr f' Int.zero).
-    destruct (ms m0); try congruence. 
-    generalize H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence.
-  assert (P2: rs (ireg_of m0) = Vptr f' Int.zero).
-    generalize (ireg_val _ _ _ m0 AG H7).
-    rewrite P1. intro. inv H11. auto.
-  set (rs2 := nextinstr (rs#CTR <- (Vptr f' Int.zero))).
-  set (rs3 := nextinstr (rs2#GPR0 <- (parent_ra s))).
-  set (rs4 := nextinstr (rs3#LR <- (parent_ra s))).
+  Simpl. rewrite <- H0; eexact TCA.
+  change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. 
+  simpl. eapply agree_exten; eauto. intros. Simpl. 
+  Simpl. rewrite <- H0. exact I.
++ (* Direct call *)
+  destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate.
+  generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1.
+  assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x).
+    econstructor; eauto. 
+  left; econstructor; split.
+  apply plus_one. eapply exec_step_internal. eauto.
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
+  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. eauto.
+  econstructor; eauto. 
+  econstructor; eauto.
+  rewrite <- H0. eexact TCA.
+  change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. 
+  simpl. eapply agree_exten; eauto. intros. Simpl.
+  auto.
+  rewrite <- H0. exact I.
+
+- (* Mtailcall *)
+  inversion AT; subst.
+  assert (NOOV: list_length_z tf <= Int.max_unsigned).
+    eapply transf_function_no_overflow; eauto.
+  rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
+  exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. 
+  exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
+  assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 GPR1) (Vint (fn_retaddr_ofs f))) = Some ra).
+Opaque Int.repr.
+    erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l.
+    eapply rsa_contains; eauto.
+  exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]].
+  assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')).
+    apply match_stack_change_bound with stk.
+    eapply match_stack_free_left; eauto. 
+    eapply match_stack_free_left; eauto. 
+    eapply match_stack_free_right; eauto.
+    omega.
+    apply Z.lt_le_incl. change (Mem.valid_block m'' stk).
+    eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. 
+    eapply retaddr_stored_at_valid; eauto.
+  destruct ros as [rf|fid]; simpl in H; monadInv H6.
++ (* Indirect call *)
+  exploit Genv.find_funct_inv; eauto. intros [bf EQ2].
+  rewrite EQ2 in H; rewrite  Genv.find_funct_find_funct_ptr in H. 
+  assert (rs0 x0 = Vptr bf Int.zero).
+    exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto.
+  set (rs2 := nextinstr (rs0#CTR <- (Vptr bf Int.zero))).
+  set (rs3 := nextinstr (rs2#GPR0 <- ra)).
+  set (rs4 := nextinstr (rs3#LR <- ra)).
   set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))).
   set (rs6 := rs5#PC <- (rs5 CTR)).
-  assert (exec_straight tge (transl_function f)
-            (transl_code f (Mtailcall sig (inl ident m0) :: c)) rs m'0 
-            (Pbctr :: transl_code f c) rs5 m2').
-  simpl. apply exec_straight_step with rs2 m'0. 
-  simpl. rewrite P2. auto. auto.
+  assert (exec_straight tge tf
+            (Pmtctr x0 :: Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0
+              :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbctr :: x)
+            rs0 m'0
+            (Pbctr :: x) rs5 m2').
+  apply exec_straight_step with rs2 m'0. 
+  simpl. rewrite H6. auto. auto.
   apply exec_straight_step with rs3 m'0.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  change (rs2 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). 
-  simpl. rewrite LOAD2. auto. congruence. auto. 
+  change (rs2 GPR1) with (rs0 GPR1). rewrite C. auto. congruence. auto.
   apply exec_straight_step with rs4 m'0.
   simpl. reflexivity. reflexivity.
   apply exec_straight_one. 
-  simpl. change (rs4 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
-  simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity.
+  simpl. change (rs4 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG).
+  rewrite E. reflexivity. reflexivity.
   left; exists (State rs6 m2'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   econstructor.
-  change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone) Vone).
-  rewrite <- H8; simpl. eauto.
+  change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone).
+  rewrite <- H3; simpl. eauto.
   eapply functions_transl; eauto. 
   eapply find_instr_tail.
   repeat (eapply code_tail_next_int; auto). eauto. 
   simpl. reflexivity. traceEq.
   (* match states *)
   econstructor; eauto.
-  assert (AG4: agree ms (Vptr stk soff) rs4).
-    unfold rs4, rs3, rs2; auto 10 with ppcgen.
-  assert (AG5: agree ms (parent_sp s) rs5).
-    unfold rs5. apply agree_nextinstr.
-    split. reflexivity. apply parent_sp_def; auto. 
-    intros. inv AG4. rewrite Pregmap.gso; auto with ppcgen.
-  unfold rs6; auto with ppcgen.
-  (* direct call *)
-  set (rs2 := nextinstr (rs#GPR0 <- (parent_ra s))).
-  set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
+Hint Resolve agree_nextinstr agree_set_other: asmgen.
+  assert (AG4: agree rs (Vptr stk Int.zero) rs4).
+    unfold rs4, rs3, rs2; auto 10 with asmgen.
+  assert (AG5: agree rs (parent_sp s) rs5).
+    unfold rs5. apply agree_nextinstr. eapply agree_change_sp. eauto. 
+    eapply parent_sp_def; eauto. 
+  unfold rs6, rs5; auto 10 with asmgen.
+  reflexivity.
+  change (rs6 LR) with ra. eapply retaddr_stored_at_type; eauto. 
++ (* Direct call *)
+  destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate.
+  set (rs2 := nextinstr (rs0#GPR0 <- ra)).
+  set (rs3 := nextinstr (rs2#LR <- ra)).
   set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
-  set (rs5 := rs4#PC <- (Vptr f' Int.zero)).
-  assert (exec_straight tge (transl_function f)
-            (transl_code f (Mtailcall sig (inr mreg i) :: c)) rs m'0 
-            (Pbs i :: transl_code f c) rs4 m2').
-  simpl. apply exec_straight_step with rs2 m'0. 
+  set (rs5 := rs4#PC <- (Vptr bf Int.zero)).
+  assert (exec_straight tge tf
+            (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0
+             :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid :: x)
+            rs0 m'0
+            (Pbs fid :: x) rs4 m2').
+  apply exec_straight_step with rs2 m'0. 
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  rewrite <- (sp_val _ _ _ AG). 
-  simpl. rewrite LOAD2. auto. discriminate. auto. 
+  rewrite C. auto. congruence. auto.
   apply exec_straight_step with rs3 m'0.
   simpl. reflexivity. reflexivity.
   apply exec_straight_one. 
-  simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
-  simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity.
+  simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG).
+  rewrite E. reflexivity. reflexivity.
   left; exists (State rs5 m2'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   econstructor.
-  change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone).
-  rewrite <- H8; simpl. eauto.
+  change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone).
+  rewrite <- H3; simpl. eauto.
   eapply functions_transl; eauto. 
   eapply find_instr_tail.
   repeat (eapply code_tail_next_int; auto). eauto. 
-  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. 
-  reflexivity. traceEq.
+  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. auto. traceEq.
   (* match states *)
   econstructor; eauto.
-  assert (AG3: agree ms (Vptr stk soff) rs3).
-    unfold rs3, rs2; auto 10 with ppcgen.
-  assert (AG4: agree ms (parent_sp s) rs4).
-    unfold rs4. apply agree_nextinstr.
-    split. reflexivity. 
-    apply parent_sp_def; auto.
-    intros. inv AG3. rewrite Pregmap.gso; auto with ppcgen.
-  unfold rs5; auto with ppcgen.
-Qed.
+Hint Resolve agree_nextinstr agree_set_other: asmgen.
+  assert (AG3: agree rs (Vptr stk Int.zero) rs3).
+    unfold rs3, rs2; auto 10 with asmgen.
+  assert (AG4: agree rs (parent_sp s) rs4).
+    unfold rs4. apply agree_nextinstr. eapply agree_change_sp. eauto. 
+    eapply parent_sp_def; eauto. 
+  unfold rs5; auto 10 with asmgen.
+  reflexivity.
+  change (rs5 LR) with ra. eapply retaddr_stored_at_type; eauto.
 
-Lemma exec_Mbuiltin_prop:
-  forall (s : list stackframe) (f : block) (sp : val)
-         (ms : Mach.regset) (m : mem) (ef : external_function)
-         (args : list mreg) (res : mreg) (b : list Mach.instruction)
-         (t : trace) (v : val) (m' : mem),
-  external_call ef ge ms ## args m t v m' ->
-  exec_instr_prop (Machsem.State s f sp (Mbuiltin ef args res :: b) ms m) t
-                  (Machsem.State s f sp b (Regmap.set res v (undef_temps ms)) m').
-Proof.
-  intros; red; intros; inv MS.
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inv WTI.
-  inv AT. simpl in H3.
-  generalize (functions_transl _ _ FIND); intro FN.
-  generalize (functions_transl_no_overflow _ _ FIND); intro NOOV.
+- (* Mbuiltin *)
+  inv AT. monadInv H3. 
+  exploit functions_transl; eauto. intro FN.
+  generalize (transf_function_no_overflow _ _ H2); intro NOOV.
   exploit external_call_mem_extends; eauto. eapply preg_vals; eauto.
   intros [vres' [m2' [A [B [C D]]]]].
   left. econstructor; split. apply plus_one. 
@@ -1116,30 +794,23 @@ Proof.
   eapply find_instr_tail; eauto.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
-  econstructor; eauto with coqlib.
-  unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with ppcgen.
-  rewrite <- H0. simpl. constructor; auto.
-  eapply code_tail_next_int; eauto. 
-  apply sym_not_equal. auto with ppcgen.
-  apply agree_nextinstr. apply agree_set_mreg_undef_temps with rs; auto. 
-  rewrite Pregmap.gss. auto.
-  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
-Qed.
+  econstructor; eauto.
+  eapply match_stack_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
+  instantiate (2 := tf); instantiate (1 := x).
+  Simpl. rewrite <- H0. simpl. econstructor; eauto.
+  eapply code_tail_next_int; eauto.
+  apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. 
+  rewrite Pregmap.gss. auto. 
+  intros. Simpl. 
+  eapply retaddr_stored_at_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
+  congruence.
 
-Lemma exec_Mannot_prop:
-  forall (s : list stackframe) (f : block) (sp : val)
-         (ms : Mach.regset) (m : mem) (ef : external_function)
-         (args : list Mach.annot_param) (b : list Mach.instruction)
-         (vargs: list val) (t : trace) (v : val) (m' : mem),
-  Machsem.annot_arguments ms m sp args vargs ->
-  external_call ef ge vargs m t v m' ->
-  exec_instr_prop (Machsem.State s f sp (Mannot ef args :: b) ms m) t
-                  (Machsem.State s f sp b ms m').
-Proof.
-  intros; red; intros; inv MS.
-  inv AT. simpl in H3.
-  generalize (functions_transl _ _ FIND); intro FN.
-  generalize (functions_transl_no_overflow _ _ FIND); intro NOOV.
+- (* Mannot *)
+  inv AT. monadInv H4. 
+  exploit functions_transl; eauto. intro FN.
+  generalize (transf_function_no_overflow _ _ H3); intro NOOV.
   exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. 
   exploit external_call_mem_extends; eauto.
   intros [vres' [m2' [A [B [C D]]]]].
@@ -1148,373 +819,238 @@ Proof.
   eapply find_instr_tail; eauto. eauto.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
-  econstructor; eauto with coqlib.
+  eapply match_states_intro with (ep := false); eauto with coqlib.
+  eapply match_stack_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
   unfold nextinstr. rewrite Pregmap.gss. 
-  rewrite <- H1; simpl. econstructor; auto.
+  rewrite <- H1; simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto. 
   apply agree_nextinstr. auto.
-Qed.
+  eapply retaddr_stored_at_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
+  congruence.
 
-Lemma exec_Mgoto_prop:
-  forall (s : list stackframe) (fb : block) (f : function) (sp : val)
-         (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
-         (m : mem) (c' : Mach.code),
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machsem.State s fb sp (Mgoto lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c' ms m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. simpl in H3.
-  generalize (find_label_goto_label f lbl rs m' _ _ _ FIND (sym_equal H1) H0).
-  intros [rs2 [GOTO [AT2 INV]]].
-  left; exists (State rs2 m'); split.
+- (* Mgoto *)
+  inv AT. monadInv H3. 
+  exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
+  left; exists (State rs' m'); split.
   apply plus_one. econstructor; eauto.
-  apply functions_transl; eauto.
+  eapply functions_transl; eauto.
   eapply find_instr_tail; eauto.
-  simpl; auto.
-  econstructor; eauto.
-  eapply Mach.find_label_incl; eauto.
-  apply agree_exten with rs; auto with ppcgen.
-Qed.
-
-Lemma exec_Mcond_true_prop:
-  forall (s : list stackframe) (fb : block) (f : function) (sp : val)
-         (cond : condition) (args : list mreg) (lbl : Mach.label)
-         (c : list Mach.instruction) (ms : mreg -> val) (m : mem)
-         (c' : Mach.code),
-  eval_condition cond ms ## args m = Some true ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c' (undef_temps ms) m).
-Proof.
-  intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0.
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inv WTI.
-  pose (k1 := 
-         if snd (crbit_for_cond cond)
-         then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c
-         else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c).
-  exploit transl_cond_correct; eauto. 
-  simpl. intros [rs2 [EX [RES AG2]]].
-  inv AT. simpl in H5.
-  generalize (functions_transl _ _ H4); intro FN.
-  generalize (functions_transl_no_overflow _ _ H4); intro NOOV.
-  exploit exec_straight_steps_2; eauto. 
-  intros [ofs' [PC2 CT2]].
-  generalize (find_label_goto_label f lbl rs2 m' _ _ _ FIND PC2 H1).
-  intros [rs3 [GOTO [AT3 INV3]]].
-  left; exists (State rs3 m'); split.
-  eapply plus_right'. 
-  eapply exec_straight_steps_1; eauto.
-  caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES.
-  econstructor; eauto.
-  eapply find_instr_tail. unfold k1 in CT2; rewrite ISSET in CT2. eauto.
-  simpl. rewrite RES. simpl. auto.
+  simpl; eauto.
   econstructor; eauto.
-  eapply find_instr_tail. unfold k1 in CT2; rewrite ISSET in CT2. eauto.
-  simpl. rewrite RES. simpl. auto.
-  traceEq.
-  econstructor; eauto. 
-  eapply Mach.find_label_incl; eauto.
-  apply agree_undef_temps with rs2; auto with ppcgen.
-Qed.
-
-Lemma exec_Mcond_false_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (cond : condition) (args : list mreg) (lbl : Mach.label)
-         (c : list Mach.instruction) (ms : mreg -> val) (m : mem),
-  eval_condition cond ms ## args m = Some false ->
-  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c (undef_temps ms) m).
-Proof.
-  intros; red; intros; inv MS.
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inversion WTI.
-  exploit transl_cond_correct; eauto.
-  simpl. intros [rs2 [EX [RES AG2]]].
-  left; eapply exec_straight_steps; eauto with coqlib.
-  exists (nextinstr rs2); split.
-  simpl. eapply exec_straight_trans. eexact EX. 
-  caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES.
-  apply exec_straight_one. simpl. rewrite RES. reflexivity.
-  reflexivity.
-  apply exec_straight_one. simpl. rewrite RES. reflexivity.
-  reflexivity.
-  apply agree_nextinstr. apply agree_undef_temps with rs2; auto.
-Qed.
+  eapply agree_exten; eauto with asmgen.
+  congruence.
 
-Lemma exec_Mjumptable_prop:
-  forall (s : list stackframe) (fb : block) (f : function) (sp : val)
-         (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction)
-         (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label)
-         (c' : Mach.code),
-  rs arg = Vint n ->
-  list_nth_z tbl (Int.unsigned n) = Some lbl ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop
-    (Machsem.State s fb sp (Mjumptable arg tbl :: c) rs m) E0
-    (Machsem.State s fb sp c' (undef_temps rs) m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inv WTI.
-  exploit list_nth_z_range; eauto. intro RANGE.
-  assert (SHIFT: Int.unsigned (Int.rolm n (Int.repr 2) (Int.repr (-4))) = Int.unsigned n * 4).
-    replace (Int.repr (-4)) with (Int.shl Int.mone (Int.repr 2)).
-    rewrite <- Int.shl_rolm. rewrite Int.shl_mul.
-    unfold Int.mul. apply Int.unsigned_repr. omega.
-    compute. reflexivity.
-    apply Int.mkint_eq. compute. reflexivity.
-  inv AT. simpl in H7. 
-  set (k1 := Pbtbl GPR12 tbl :: transl_code f c).
-  set (rs1 := nextinstr (rs0 # GPR12 <- (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))))).
-  generalize (functions_transl _ _ H4); intro FN.
-  generalize (functions_transl_no_overflow _ _ H4); intro NOOV.
-  assert (exec_straight tge (transl_function f)
-            (Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: k1) rs0 m'
-            k1 rs1 m').
-   apply exec_straight_one. 
-   simpl. generalize (ireg_val _ _ _ arg AG H5). rewrite H. intro. inv H8. 
-   reflexivity. reflexivity. 
-  exploit exec_straight_steps_2; eauto. 
-  intros [ofs' [PC1 CT1]].
-  set (rs2 := rs1 # GPR12 <- Vundef # CTR <- Vundef).
-  assert (PC2: rs2 PC = Vptr fb ofs'). rewrite <- PC1. reflexivity.
-  generalize (find_label_goto_label f lbl rs2 m' _ _ _ FIND PC2 H2).
-  intros [rs3 [GOTO [AT3 INV3]]].
-  left; exists (State rs3 m'); split.
-  eapply plus_right'. 
-  eapply exec_straight_steps_1; eauto.
-  econstructor; eauto. 
-  eapply find_instr_tail. unfold k1 in CT1. eauto.
-  unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen.  
-  change (rs1 GPR12) with (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))).
-  lazy iota beta.   rewrite SHIFT.  rewrite Z_mod_mult. rewrite zeq_true.
-  rewrite Z_div_mult.
-  change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq.
+- (* Mcond true *)
+  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
+  left; eapply exec_straight_steps_goto; eauto.
+  intros. simpl in TR.
+  destruct (transl_cond_correct_1 tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]].
+  rewrite EC in B.
+  destruct (snd (crbit_for_cond cond)).
+  (* Pbt, taken *)
+  econstructor; econstructor; econstructor; split. eexact A. 
+  split. eapply agree_exten_temps; eauto with asmgen.
+  simpl. rewrite B. reflexivity. 
+  (* Pbf, taken *)
+  econstructor; econstructor; econstructor; split. eexact A. 
+  split. eapply agree_exten_temps; eauto with asmgen.
+  simpl. rewrite B. reflexivity. 
+
+- (* Mcond false *)
+  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
+  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
+  destruct (transl_cond_correct_1 tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]].
+  rewrite EC in B.
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. 
+  destruct (snd (crbit_for_cond cond)).
+  apply exec_straight_one. simpl. rewrite B. reflexivity. auto.
+  apply exec_straight_one. simpl. rewrite B. reflexivity. auto.
+  split. eapply agree_exten_temps; eauto with asmgen.
+  intros; Simpl.
+  simpl. congruence.
+
+- (* Mjumptable *)
+  inv AT. monadInv H5. 
+  exploit functions_transl; eauto. intro FN.
+  generalize (transf_function_no_overflow _ _ H4); intro NOOV.
+  exploit find_label_goto_label. eauto. eauto.
+  instantiate (2 := rs0#GPR12 <- Vundef #CTR <- Vundef). 
+  Simpl. eauto.
+  eauto. 
+  intros [tc' [rs' [A [B C]]]].
+  exploit ireg_val; eauto. rewrite H. intros LD; inv LD.
+  left; econstructor; split.
+  apply plus_one. econstructor; eauto. 
+  eapply find_instr_tail; eauto. 
+  simpl. rewrite <- H8. unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
   econstructor; eauto. 
-  eapply Mach.find_label_incl; eauto.
-  apply agree_undef_temps with rs0; auto.
-  intros. rewrite INV3; auto with ppcgen.
-  unfold rs2. repeat rewrite Pregmap.gso; auto with ppcgen.
-  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. 
-  apply Pregmap.gso; auto with ppcgen.
-Qed.
+  eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simpl. 
+  congruence.
 
-Lemma exec_Mreturn_prop:
-  forall (s : list stackframe) (fb stk : block) (soff : int)
-         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m',
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
-  Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-  exec_instr_prop (Machsem.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
-                  (Returnstate s ms m').
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
-  exploit Mem.free_parallel_extends; eauto.
-  intros [m2' [FREE' EXT']].
-  unfold load_stack in *. simpl in H0; simpl in H1.
-  exploit Mem.load_extends. eexact MEXT. eexact H0.
-  intros [parent' [LOAD1 LD1]].
-  rewrite (lessdef_parent_sp s parent' STACKS LD1) in LOAD1.
-  exploit Mem.load_extends. eexact MEXT. eexact H1.
-  intros [ra' [LOAD2 LD2]].
-  rewrite (lessdef_parent_ra s ra' STACKS LD2) in LOAD2.
-  set (rs2 := nextinstr (rs#GPR0 <- (parent_ra s))).
-  set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
+- (* Mreturn *)
+  inversion AT; subst. 
+  assert (NOOV: list_length_z tf <= Int.max_unsigned).
+    eapply transf_function_no_overflow; eauto.
+  rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
+  exploit Mem.loadv_extends. eauto. eexact H. auto. simpl. intros [parent' [A B]]. 
+  exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
+  assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 GPR1) (Vint (fn_retaddr_ofs f))) = Some ra).
+Opaque Int.repr.
+    erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l.
+    eapply rsa_contains; eauto.
+  exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]].
+  assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')).
+    apply match_stack_change_bound with stk.
+    eapply match_stack_free_left; eauto.
+    eapply match_stack_free_left; eauto.
+    eapply match_stack_free_right; eauto. omega.
+    apply Z.lt_le_incl. change (Mem.valid_block m'' stk).
+    eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. 
+    eapply retaddr_stored_at_valid; eauto.
+  monadInv H5.
+  set (rs2 := nextinstr (rs0#GPR0 <- ra)).
+  set (rs3 := nextinstr (rs2#LR <- ra)).
   set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
-  set (rs5 := rs4#PC <- (parent_ra s)).
-  assert (exec_straight tge (transl_function f)
-            (transl_code f (Mreturn :: c)) rs m'0 
-            (Pblr :: transl_code f c) rs4 m2').
+  set (rs5 := rs4#PC <- ra).
+  assert (exec_straight tge tf
+           (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1
+           :: Pmtlr GPR0
+           :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pblr :: x) rs0 m'0
+           (Pblr :: x) rs4 m2').
   simpl. apply exec_straight_three with rs2 m'0 rs3 m'0.
-  simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  rewrite <- (sp_val _ _ _ AG). simpl. rewrite LOAD2. 
-  reflexivity. discriminate.
-  unfold rs3. reflexivity.
-  simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
-  simpl. rewrite LOAD1. rewrite FREE'. reflexivity.
-  reflexivity. reflexivity. reflexivity.
+  simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. rewrite C. auto. congruence.
+  simpl. auto. 
+  simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A. 
+  rewrite <- (sp_val _ _ _ AG). rewrite E. auto. 
+  auto. auto. auto. 
   left; exists (State rs5 m2'); split.
   (* execution *)
   apply plus_right' with E0 (State rs4 m2') E0.
   eapply exec_straight_exec; eauto.
-  inv AT. econstructor.
-  change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). 
-  rewrite <- H4. simpl. eauto.
-  apply functions_transl; eauto.
-  generalize (functions_transl_no_overflow _ _ H5); intro NOOV.
-  simpl in H6. eapply find_instr_tail. 
+  econstructor.
+  change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). 
+  rewrite <- H2. simpl. eauto.
+  eapply functions_transl; eauto.
+  eapply find_instr_tail. 
   eapply code_tail_next_int; auto.
   eapply code_tail_next_int; auto.
   eapply code_tail_next_int; eauto.
   reflexivity. traceEq.
   (* match states *)
   econstructor; eauto. 
-  assert (AG3: agree ms (Vptr stk soff) rs3). 
-    unfold rs3, rs2; auto 10 with ppcgen.
-  assert (AG4: agree ms (parent_sp s) rs4).
-    split. reflexivity. apply parent_sp_def; auto. intros. unfold rs4. 
-    rewrite nextinstr_inv. rewrite Pregmap.gso.
-    elim AG3; auto. auto with ppcgen. auto with ppcgen.
-  unfold rs5; auto with ppcgen.
-Qed.
-
-Hypothesis wt_prog: wt_program prog.
-
-Lemma exec_function_internal_prop:
-  forall (s : list stackframe) (fb : block) (ms : Mach.regset)
-         (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block),
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mem.alloc m 0 (fn_stacksize f) = (m1, stk) ->
-  let sp := Vptr stk Int.zero in
-  store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
-  store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
-  exec_instr_prop (Machsem.Callstate s fb ms m) E0
-                  (Machsem.State s fb sp (fn_code f) (undef_temps ms) m3).
-Proof.
-  intros; red; intros; inv MS.
-  assert (WTF: wt_function f).
-    generalize (Genv.find_funct_ptr_prop wt_fundef _ _ wt_prog H); intro TY.
-    inversion TY; auto.
-  exploit functions_transl; eauto. intro TFIND.
-  generalize (functions_transl_no_overflow _ _ H); intro NOOV.
-  unfold store_stack in *; simpl in *.
-  exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. 
-  intros [m1' [ALLOC' MEXT1]].
-  exploit Mem.store_within_extends. eexact MEXT1. eexact H1. auto.
-  intros [m2' [STORE2 MEXT2]].
-  exploit Mem.store_within_extends. eexact MEXT2. eexact H2. auto.
-  intros [m3' [STORE3 MEXT3]].
-  set (rs2 := nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)).
-  set (rs3 := nextinstr (rs2#GPR0 <- (parent_ra s))).
-  set (rs4 := nextinstr rs3).
+  assert (AG3: agree rs (Vptr stk Int.zero) rs3). 
+    unfold rs3, rs2; auto 10 with asmgen.
+  assert (AG4: agree rs (parent_sp s) rs4).
+    unfold rs4. apply agree_nextinstr. eapply agree_change_sp; eauto. 
+    eapply parent_sp_def; eauto.
+  unfold rs5; auto with asmgen.
+
+- (* internal function *)
+  exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
+  generalize EQ; intros EQ'. monadInv EQ'. 
+  destruct (zlt Int.max_unsigned (list_length_z x0)); inversion EQ1. clear EQ1.
+  unfold store_stack in *. 
+  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
+  intros [m1' [C D]].
+  assert (E: Mem.extends m2 m1') by (eapply Mem.free_left_extends; eauto).
+  exploit Mem.storev_extends. eexact E. eexact H1. eauto. eauto. 
+  intros [m2' [F G]].
+  exploit retaddr_stored_at_can_alloc. eexact H. eauto. eauto. eauto. eauto. 
+  auto. auto. auto. auto. eauto. 
+  intros [m3' [P [Q R]]].
   (* Execution of function prologue *)
+  monadInv EQ0.
+  set (rs2 := nextinstr (rs0#GPR1 <- sp #GPR0 <- Vundef)).
+  set (rs3 := nextinstr (rs2#GPR0 <- (rs0#LR))).
+  set (rs4 := nextinstr rs3).
   assert (EXEC_PROLOGUE:
-            exec_straight tge (transl_function f)
-              (transl_function f) rs m'
-              (transl_code f (fn_code f)) rs4 m3').
-  unfold transl_function at 2. 
+            exec_straight tge x
+              x rs0 m'
+              x1 rs4 m3').
+  rewrite <- H5 at 2. 
   apply exec_straight_three with rs2 m2' rs3 m2'.
-  unfold exec_instr. rewrite ALLOC'. fold sp.
-  rewrite <- (sp_val _ _ _ AG). unfold sp; simpl; rewrite STORE2. reflexivity.
-  simpl. change (rs2 LR) with (rs LR). rewrite ATLR. reflexivity.
+  unfold exec_instr. rewrite C. fold sp.
+  rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. 
+  simpl. auto.
   simpl. unfold store1. rewrite gpr_or_zero_not_zero. 
-  unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR0) with (parent_ra s).
-  simpl. rewrite STORE3. reflexivity. 
-  discriminate. reflexivity. reflexivity. reflexivity.
-  (* Agreement at end of prologue *)
-  assert (AT4: transl_code_at_pc rs4#PC fb f f.(fn_code)).
-    change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone).
-    rewrite ATPC. simpl. constructor. auto.
-    eapply code_tail_next_int; auto.
-    eapply code_tail_next_int; auto.
-    eapply code_tail_next_int; auto.
-    change (Int.unsigned Int.zero) with 0. 
-    unfold transl_function. constructor.
-  assert (AG2: agree ms sp rs2).
-    split. reflexivity. unfold sp. congruence. 
-    intros. unfold rs2. rewrite nextinstr_inv. 
-    repeat (rewrite Pregmap.gso). inv AG; auto.
-    auto with ppcgen. auto with ppcgen. auto with ppcgen.
-  assert (AG4: agree ms sp rs4).
-    unfold rs4, rs3; auto with ppcgen.
+  change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). simpl. 
+  rewrite Int.add_zero_l. rewrite P. auto. congruence.
+  auto. auto. auto.
   left; exists (State rs4 m3'); split.
-  (* execution *)
-  eapply exec_straight_steps_1; eauto.
-  change (Int.unsigned Int.zero) with 0. constructor.
-  (* match states *)
-  econstructor; eauto with coqlib. apply agree_undef_temps with rs4; auto.
-Qed.
+  eapply exec_straight_steps_1; eauto. unfold fn_code; omega. constructor. 
+  econstructor; eauto. 
+  assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto).
+  rewrite <- STK in STACKS. simpl in F. simpl in H1.
+  eapply match_stack_invariant; eauto.
+  intros. eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_free_3; eauto. 
+  eapply Mem.perm_store_2; eauto. unfold block; omega.
+  intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. 
+  eapply Mem.perm_alloc_1; eauto. 
+  intros. erewrite Mem.load_store_other. 2: eauto.
+  erewrite Mem.load_store_other. 2: eauto. 
+  eapply Mem.load_alloc_other; eauto.
+  left; unfold block; omega.
+  left; unfold block; omega.
+  change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). 
+  rewrite ATPC. simpl. constructor; eauto.
+  subst x. unfold fn_code. eapply code_tail_next_int. omega. 
+  eapply code_tail_next_int. omega. 
+  eapply code_tail_next_int. omega. 
+  constructor.
+  unfold rs4, rs3, rs2.
+  apply agree_nextinstr. apply agree_set_other; auto. apply agree_set_other; auto. 
+  apply agree_nextinstr. apply agree_set_other; auto.
+  eapply agree_change_sp; eauto. apply agree_exten_temps with rs0; eauto.
+  unfold sp; congruence.
+  congruence.
 
-Lemma exec_function_external_prop:
-  forall (s : list stackframe) (fb : block) (ms : Mach.regset)
-         (m : mem) (t0 : trace) (ms' : RegEq.t -> val)
-         (ef : external_function) (args : list val) (res : val) (m': mem),
-  Genv.find_funct_ptr ge fb = Some (External ef) ->
-  external_call ef ge args m t0 res m' ->
-  Machsem.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
-  ms' = Regmap.set (loc_result (ef_sig ef)) res ms ->
-  exec_instr_prop (Machsem.Callstate s fb ms m)
-               t0 (Machsem.Returnstate s ms' m').
-Proof.
-  intros; red; intros; inv MS.
+- (* external function *)
   exploit functions_translated; eauto.
-  intros [tf [A B]]. simpl in B. inv B. 
+  intros [tf [A B]]. simpl in B. inv B.
   exploit extcall_arguments_match; eauto. 
   intros [args' [C D]].
-  exploit external_call_mem_extends; eauto. 
+  exploit external_call_mem_extends; eauto.
   intros [res' [m2' [P [Q [R S]]]]].
-  left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res' #PC <- (rs LR))
-                m2'); split.
+  left; econstructor; split.
   apply plus_one. eapply exec_step_external; eauto. 
-  eapply external_call_symbols_preserved; eauto.
+  eapply external_call_symbols_preserved; eauto. 
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
-  unfold loc_external_result. 
-  apply agree_set_other; auto with ppcgen.
-  apply agree_set_mreg with rs; auto. 
-  rewrite Pregmap.gss; auto. 
-  intros; apply Pregmap.gso; auto.
-Qed.
-
-Lemma exec_return_prop:
-  forall (s : list stackframe) (fb : block) (sp ra : val)
-         (c : Mach.code) (ms : Mach.regset) (m : mem),
-  exec_instr_prop (Machsem.Returnstate (Stackframe fb sp ra c :: s) ms m) E0
-                  (Machsem.State s fb sp c ms m).
-Proof.
-  intros; red; intros; inv MS. inv STACKS. simpl in *.
+  rewrite Pregmap.gss. apply match_stack_change_bound with (Mem.nextblock m). 
+  eapply match_stack_extcall; eauto.
+  intros. eapply external_call_max_perm; eauto.
+  eapply external_call_nextblock; eauto.
+  unfold loc_external_result.
+  eapply agree_set_mreg; eauto. 
+  rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. 
+  intros; Simpl.
+
+- (* return *)
+  inv STACKS. simpl in *.
   right. split. omega. split. auto. 
-  econstructor; eauto. rewrite ATPC; auto.  
+  econstructor; eauto. congruence.
 Qed.
 
-Theorem transf_instr_correct:
-  forall s1 t s2, Machsem.step ge s1 t s2 ->
-  exec_instr_prop s1 t s2.
-Proof
-  (Machsem.step_ind ge exec_instr_prop
-           exec_Mlabel_prop
-           exec_Mgetstack_prop
-           exec_Msetstack_prop
-           exec_Mgetparam_prop
-           exec_Mop_prop
-           exec_Mload_prop
-           exec_Mstore_prop
-           exec_Mcall_prop
-           exec_Mtailcall_prop
-           exec_Mbuiltin_prop
-           exec_Mannot_prop
-           exec_Mgoto_prop
-           exec_Mcond_true_prop
-           exec_Mcond_false_prop
-           exec_Mjumptable_prop
-           exec_Mreturn_prop
-           exec_function_internal_prop
-           exec_function_external_prop
-           exec_return_prop).
-
 Lemma transf_initial_states:
-  forall st1, Machsem.initial_state prog st1 ->
+  forall st1, Mach.initial_state prog st1 ->
   exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. unfold ge0 in *.
+  exploit functions_translated; eauto. intros [tf [A B]]. 
   econstructor; split.
   econstructor.
   eapply Genv.init_mem_transf_partial; eauto.
   replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero)
-     with (Vptr fb Int.zero).
-  econstructor; eauto. constructor.
-  split. auto. simpl. congruence.
-  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
+     with (Vptr b Int.zero).
+  econstructor; eauto.
+  constructor.
   apply Mem.extends_refl.
+  split. auto. intros. rewrite Regmap.gi. auto. 
+  reflexivity. 
+  exact I.
   unfold symbol_offset. 
   rewrite (transform_partial_program_main _ _ TRANSF). 
   rewrite symbols_preserved. unfold ge; rewrite H1. auto.
@@ -1522,21 +1058,22 @@ Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r, 
-  match_states st1 st2 -> Machsem.final_state st1 r -> Asm.final_state st2 r.
+  match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r.
 Proof.
-  intros. inv H0. inv H. constructor. auto. 
-  compute in H1.
-  exploit (ireg_val _ _ _ R3 AG). auto. rewrite H1; intro. inv H. auto.
+  intros. inv H0. inv H. inv STACKS. constructor.
+  auto. 
+  compute in H1. 
+  generalize (preg_val _ _ _ R3 AG). rewrite H1. intros LD; inv LD. auto.
 Qed.
 
 Theorem transf_program_correct:
-  forward_simulation (Machsem.semantics prog) (Asm.semantics tprog).
+  forward_simulation (Mach.semantics prog) (Asm.semantics tprog).
 Proof.
   eapply forward_simulation_star with (measure := measure).
   eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
-  exact transf_instr_correct. 
+  exact step_simulation.
 Qed.
 
 End PRESERVATION.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 56cb224..1e16a0d 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -13,6 +13,7 @@
 (** Correctness proof for PPC generation: auxiliary results. *)
 
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
@@ -23,11 +24,10 @@ Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
 Require Import Mach.
-Require Import Machsem.
-Require Import Machtyping.
 Require Import Asm.
 Require Import Asmgen.
 Require Import Conventions.
+Require Import Asmgenproof0.
 
 (** * Properties of low half/high half decomposition *)
 
@@ -103,308 +103,7 @@ Proof.
   rewrite Int.sub_idem. apply Int.add_zero.
 Qed.
 
-(** * Correspondence between Mach registers and PPC registers *)
-
-Hint Extern 2 (_ <> _) => discriminate: ppcgen.
-
-(** Mapping from Mach registers to PPC registers. *)
-
-Lemma preg_of_injective:
-  forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
-Proof.
-  destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
-Qed.
-
-(** Characterization of PPC registers that correspond to Mach registers. *)
-
-Definition is_data_reg (r: preg) : bool :=
-  match r with
-  | IR GPR0 => false
-  | PC => false    | LR => false    | CTR => false
-  | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false
-  | CARRY => false
-  | _ => true
-  end.
-
-Lemma ireg_of_is_data_reg:
-  forall (r: mreg), is_data_reg (ireg_of r) = true.
-Proof.
-  destruct r; reflexivity.
-Qed.
-
-Lemma freg_of_is_data_reg:
-  forall (r: mreg), is_data_reg (ireg_of r) = true.
-Proof.
-  destruct r; reflexivity.
-Qed.
-
-Lemma preg_of_is_data_reg:
-  forall (r: mreg), is_data_reg (preg_of r) = true.
-Proof.
-  destruct r; reflexivity.
-Qed.
-
-Lemma data_reg_diff:
-  forall r r', is_data_reg r = true -> is_data_reg r' = false -> r <> r'.
-Proof.
-  intros. congruence.
-Qed.
-
-Lemma ireg_diff:
-  forall r r', r <> r' -> IR r <> IR r'.
-Proof.
-  intros. congruence.
-Qed.
-
-Lemma diff_ireg:
-  forall r r', IR r <> IR r' -> r <> r'.
-Proof.
-  intros. congruence.
-Qed.
-
-Hint Resolve ireg_of_is_data_reg freg_of_is_data_reg preg_of_is_data_reg
-             data_reg_diff ireg_diff diff_ireg: ppcgen.
-
-Definition is_nontemp_reg (r: preg) : bool :=
-  match r with
-  | IR GPR0 => false | IR GPR11 => false | IR GPR12 => false
-  | FR FPR0 => false | FR FPR12 => false | FR FPR13 => false
-  | PC => false      | LR => false       | CTR => false
-  | CR0_0 => false   | CR0_1 => false    | CR0_2 => false    | CR0_3 => false
-  | CARRY => false
-  | _ => true
-  end.
-
-Remark is_nontemp_is_data:
-  forall r, is_nontemp_reg r = true -> is_data_reg r = true.
-Proof.
-  destruct r; simpl; try congruence. destruct i; congruence.
-Qed.
-
-Lemma nontemp_reg_diff:
-  forall r r', is_nontemp_reg r = true -> is_nontemp_reg r' = false -> r <> r'.
-Proof.
-  intros. congruence.
-Qed.
-
-Hint Resolve is_nontemp_is_data nontemp_reg_diff: ppcgen.
-
-Lemma ireg_of_not_GPR1:
-  forall r, ireg_of r <> GPR1.
-Proof.
-  intro. case r; discriminate.
-Qed.
-
-Lemma preg_of_not_GPR1:
-  forall r, preg_of r <> GPR1.
-Proof.
-  intro. case r; discriminate.
-Qed.
-Hint Resolve ireg_of_not_GPR1 preg_of_not_GPR1: ppcgen.
-
-Lemma int_temp_for_diff:
-  forall r, IR(int_temp_for r) <> preg_of r.
-Proof.
-  intros. unfold int_temp_for. destruct (mreg_eq r IT2).
-  subst r. compute. congruence. 
-  change (IR GPR12) with (preg_of IT2). red; intros; elim n.
-  apply preg_of_injective; auto.
-Qed.
-
-(** Agreement between Mach register sets and PPC register sets. *)
-
-Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree {
-  agree_sp: rs#GPR1 = sp;
-  agree_sp_def: sp <> Vundef;
-  agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r))
-}.
-
-Lemma preg_val:
-  forall ms sp rs r,
-  agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r).
-Proof.
-  intros. eapply agree_mregs; eauto. 
-Qed.
-
-Lemma preg_vals:
-  forall ms sp rs rl,
-  agree ms sp rs -> Val.lessdef_list (List.map ms rl) (List.map rs (List.map preg_of rl)).
-Proof.
-  induction rl; intros; simpl.
-  constructor.
-  constructor. eapply preg_val; eauto. eauto.
-Qed.
-
-Lemma ireg_val:
-  forall ms sp rs r,
-  agree ms sp rs ->
-  mreg_type r = Tint ->
-  Val.lessdef (ms r) rs#(ireg_of r).
-Proof.
-  intros. replace (IR (ireg_of r)) with (preg_of r). eapply preg_val; eauto. 
-  unfold preg_of. rewrite H0. auto.
-Qed.
-
-Lemma freg_val:
-  forall ms sp rs r,
-  agree ms sp rs ->
-  mreg_type r = Tfloat ->
-  Val.lessdef (ms r) rs#(freg_of r).
-Proof.
-  intros. replace (FR (freg_of r)) with (preg_of r). eapply preg_val; eauto. 
-  unfold preg_of. rewrite H0. auto.
-Qed.
-
-Lemma sp_val:
-  forall ms sp rs,
-  agree ms sp rs ->
-  sp = rs#GPR1.
-Proof.
-  intros. elim H; auto.
-Qed.
-
-Lemma agree_exten:
-  forall ms sp rs rs',
-  agree ms sp rs ->
-  (forall r, is_data_reg r = true -> rs'#r = rs#r) ->
-  agree ms sp rs'.
-Proof.
-  intros. inv H. constructor; auto. 
-  intros. rewrite H0; auto with ppcgen.
-Qed.
-
-(** Preservation of register agreement under various assignments. *)
-
-Lemma agree_set_mreg:
-  forall ms sp rs r v rs',
-  agree ms sp rs ->
-  Val.lessdef v (rs'#(preg_of r)) ->
-  (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
-  agree (Regmap.set r v ms) sp rs'.
-Proof.
-  intros. inv H. constructor; auto with ppcgen.
-  intros. unfold Regmap.set. destruct (RegEq.eq r0 r).
-  subst r0. auto.
-  rewrite H1; auto with ppcgen. red; intros; elim n; apply preg_of_injective; auto.
-Qed.
-Hint Resolve agree_set_mreg: ppcgen.
-
-Lemma agree_set_mireg:
-  forall ms sp rs r v (rs': regset),
-  agree ms sp rs ->
-  Val.lessdef v (rs'#(ireg_of r)) ->
-  mreg_type r = Tint ->
-  (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
-  agree (Regmap.set r v ms) sp rs'.
-Proof.
-  intros. eapply agree_set_mreg; eauto.  unfold preg_of; rewrite H1; auto.
-Qed.
-Hint Resolve agree_set_mireg: ppcgen.
-
-Lemma agree_set_mfreg:
-  forall ms sp rs r v (rs': regset),
-  agree ms sp rs ->
-  Val.lessdef v (rs'#(freg_of r)) ->
-  mreg_type r = Tfloat ->
-  (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
-  agree (Regmap.set r v ms) sp rs'.
-Proof.
-  intros. eapply agree_set_mreg; eauto.  unfold preg_of; rewrite H1; auto.
-Qed.
-
-Lemma agree_set_other:
-  forall ms sp rs r v,
-  agree ms sp rs ->
-  is_data_reg r = false ->
-  agree ms sp (rs#r <- v).
-Proof.
-  intros. apply agree_exten with rs.
-  auto. intros. apply Pregmap.gso. congruence.
-Qed.
-Hint Resolve agree_set_other: ppcgen.
-
-Lemma agree_nextinstr:
-  forall ms sp rs,
-  agree ms sp rs -> agree ms sp (nextinstr rs).
-Proof.
-  intros. unfold nextinstr. apply agree_set_other. auto. auto.
-Qed.
-Hint Resolve agree_nextinstr: ppcgen.
-
-Lemma agree_undef_regs:
-  forall rl ms sp rs rs',
-  agree ms sp rs ->
-  (forall r, is_data_reg r = true -> ~In r (List.map preg_of rl) -> rs'#r = rs#r) ->
-  agree (undef_regs rl ms) sp rs'.
-Proof.
-  induction rl; simpl; intros.
-  apply agree_exten with rs; auto.
-  apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))).
-  apply agree_set_mreg with rs; auto with ppcgen. 
-  intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of a)).
-  congruence. auto.
-  intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of a)).
-  congruence. apply H0; auto. intuition congruence.
-Qed.
-
-Lemma agree_undef_temps:
-  forall ms sp rs rs',
-  agree ms sp rs ->
-  (forall r, is_nontemp_reg r = true -> rs'#r = rs#r) ->
-  agree (undef_temps ms) sp rs'.
-Proof.
-  unfold undef_temps. intros. apply agree_undef_regs with rs; auto.
-  simpl. unfold preg_of; simpl. intros. intuition.
-  apply H0. destruct r; simpl in *; auto.
-  destruct i; intuition. destruct f; intuition.
-Qed.
-Hint Resolve agree_undef_temps: ppcgen.
-
-Lemma agree_set_mreg_undef_temps:
-  forall ms sp rs r v rs',
-  agree ms sp rs ->
-  Val.lessdef v (rs'#(preg_of r)) ->
-  (forall r', is_nontemp_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
-  agree (Regmap.set r v (undef_temps ms)) sp rs'.
-Proof.
-  intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))).
-  apply agree_undef_temps with rs; auto.
-  intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). 
-  congruence. apply H1; auto. 
-  auto.
-  intros. rewrite Pregmap.gso; auto. 
-Qed.
-
-Lemma agree_set_twice_mireg:
-  forall ms sp rs r v v1 v',
-  agree (Regmap.set r v1 ms) sp rs ->
-  mreg_type r = Tint ->
-  Val.lessdef v v' ->
-  agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v').
-Proof.
-  intros. inv H. 
-  split. rewrite Pregmap.gso. auto. 
-  generalize (ireg_of_not_GPR1 r); congruence.
-  auto.
-  intros. generalize (agree_mregs0 r0). 
-  case (mreg_eq r0 r); intro.
-  subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0.
-  rewrite Pregmap.gss. auto.
-  repeat rewrite Regmap.gso; auto.
-  rewrite Pregmap.gso. auto. 
-  replace (IR (ireg_of r)) with (preg_of r).
-  red; intros. elim n. apply preg_of_injective; auto.
-  unfold preg_of. rewrite H0. auto.
-Qed.
-
-(** Useful properties of the PC and GPR0 registers. *)
-
-Lemma nextinstr_inv:
-  forall r rs, r <> PC -> (nextinstr rs)#r = rs#r.
-Proof.
-  intros. unfold nextinstr. apply Pregmap.gso. auto.
-Qed.
-Hint Resolve nextinstr_inv: ppcgen.
+(** Useful properties of the GPR0 registers. *)
 
 Lemma gpr_or_zero_not_zero:
   forall rs r, r <> GPR0 -> gpr_or_zero rs r = rs#r.
@@ -416,154 +115,40 @@ Lemma gpr_or_zero_zero:
 Proof.
   intros. reflexivity.
 Qed.
-Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: ppcgen.
-
-(** Connection between Mach and Asm calling conventions for external
-    functions. *)
+Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: asmgen.
 
-Lemma extcall_arg_match:
-  forall ms sp rs m m' l v,
-  agree ms sp rs ->
-  Mem.extends m m' ->
-  Machsem.extcall_arg ms m sp l v ->
-  exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'.
+Lemma ireg_of_not_GPR0:
+  forall m r, ireg_of m = OK r -> IR r <> IR GPR0.
 Proof.
-  intros. inv H1.
-  exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto.
-  unfold load_stack in H2.
-  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
-  rewrite (sp_val _ _ _ H) in A.
-  exists v'; split; auto.
-  destruct ty; econstructor.
-  reflexivity. assumption.
-  reflexivity. assumption.
+  intros. erewrite <- ireg_of_eq; eauto with asmgen.
 Qed.
+Hint Resolve ireg_of_not_GPR0: asmgen.
 
-Lemma extcall_args_match:
-  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
-  forall ll vl,
-  list_forall2 (Machsem.extcall_arg ms m sp) ll vl ->
-  exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'.
+Lemma ireg_of_not_GPR0':
+  forall m r, ireg_of m = OK r -> r <> GPR0.
 Proof.
-  induction 3; intros. 
-  exists (@nil val); split. constructor. constructor.
-  exploit extcall_arg_match; eauto. intros [v1' [A B]].
-  destruct IHlist_forall2 as [vl' [C D]].
-  exists (v1' :: vl'); split; constructor; auto.
+  intros. generalize (ireg_of_not_GPR0 _ _ H). congruence.
 Qed.
+Hint Resolve ireg_of_not_GPR0': asmgen.
 
-Lemma extcall_arguments_match:
-  forall ms m m' sp rs sg args,
-  agree ms sp rs -> Mem.extends m m' ->
-  Machsem.extcall_arguments ms m sp sg args ->
-  exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
-Proof.
-  unfold Machsem.extcall_arguments, Asm.extcall_arguments; intros.
-  eapply extcall_args_match; eauto.
-Qed.
+(** Useful simplification tactic *)
 
-(** Translation of arguments to annotations. *)
+Ltac Simplif :=
+  ((rewrite nextinstr_inv by eauto with asmgen)
+  || (rewrite nextinstr_inv1 by eauto with asmgen)
+  || (rewrite Pregmap.gss)
+  || (rewrite nextinstr_pc)
+  || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen.
 
-Lemma annot_arg_match:
-  forall ms sp rs m m' p v,
-  agree ms sp rs ->
-  Mem.extends m m' ->
-  Machsem.annot_arg ms m sp p v ->
-  exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'.
-Proof.
-  intros. inv H1; simpl.
-(* reg *)
-  exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto.
-(* stack *)
-  exploit Mem.load_extends; eauto. intros [v' [A B]].
-  exists v'; split; auto. 
-  inv H. econstructor; eauto. 
-Qed.
+Ltac Simpl := repeat Simplif.
 
-Lemma annot_arguments_match:
-  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
-  forall pl vl,
-  Machsem.annot_arguments ms m sp pl vl ->
-  exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl'
-           /\ Val.lessdef_list vl vl'.
-Proof.
-  induction 3; intros. 
-  exists (@nil val); split. constructor. constructor.
-  exploit annot_arg_match; eauto. intros [v1' [A B]].
-  destruct IHlist_forall2 as [vl' [C D]].
-  exists (v1' :: vl'); split; constructor; auto.
-Qed.
-
-(** * Execution of straight-line code *)
+(** * Correctness of PowerPC constructor functions *)
 
-Section STRAIGHTLINE.
+Section CONSTRUCTORS.
 
 Variable ge: genv.
 Variable fn: code.
 
-(** Straight-line code is composed of PPC instructions that execute
-  in sequence (no branches, no function calls and returns).
-  The following inductive predicate relates the machine states
-  before and after executing a straight-line sequence of instructions.
-  Instructions are taken from the first list instead of being fetched
-  from memory. *)
-
-Inductive exec_straight: code -> regset -> mem -> 
-                         code -> regset -> mem -> Prop :=
-  | exec_straight_one:
-      forall i1 c rs1 m1 rs2 m2,
-      exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
-      rs2#PC = Val.add rs1#PC Vone ->
-      exec_straight (i1 :: c) rs1 m1 c rs2 m2
-  | exec_straight_step:
-      forall i c rs1 m1 rs2 m2 c' rs3 m3,
-      exec_instr ge fn i rs1 m1 = OK rs2 m2 ->
-      rs2#PC = Val.add rs1#PC Vone ->
-      exec_straight c rs2 m2 c' rs3 m3 ->
-      exec_straight (i :: c) rs1 m1 c' rs3 m3.
-
-Lemma exec_straight_trans:
-  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
-  exec_straight c1 rs1 m1 c2 rs2 m2 ->
-  exec_straight c2 rs2 m2 c3 rs3 m3 ->
-  exec_straight c1 rs1 m1 c3 rs3 m3.
-Proof.
-  induction 1; intros.
-  apply exec_straight_step with rs2 m2; auto.
-  apply exec_straight_step with rs2 m2; auto.
-Qed.
-
-Lemma exec_straight_two:
-  forall i1 i2 c rs1 m1 rs2 m2 rs3 m3,
-  exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
-  exec_instr ge fn i2 rs2 m2 = OK rs3 m3 ->
-  rs2#PC = Val.add rs1#PC Vone ->
-  rs3#PC = Val.add rs2#PC Vone ->
-  exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3.
-Proof.
-  intros. apply exec_straight_step with rs2 m2; auto.
-  apply exec_straight_one; auto.
-Qed.
-
-Lemma exec_straight_three:
-  forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4,
-  exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
-  exec_instr ge fn i2 rs2 m2 = OK rs3 m3 ->
-  exec_instr ge fn i3 rs3 m3 = OK rs4 m4 ->
-  rs2#PC = Val.add rs1#PC Vone ->
-  rs3#PC = Val.add rs2#PC Vone ->
-  rs4#PC = Val.add rs3#PC Vone ->
-  exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4.
-Proof.
-  intros. apply exec_straight_step with rs2 m2; auto.
-  eapply exec_straight_two; eauto.
-Qed.
-
-(** * Correctness of PowerPC constructor functions *)
-
-Ltac SIMP :=
-  (rewrite nextinstr_inv || rewrite Pregmap.gss || rewrite Pregmap.gso); auto with ppcgen.
-
 (** Properties of comparisons. *)
 
 Lemma compare_float_spec:
@@ -578,7 +163,7 @@ Proof.
   split. reflexivity.
   split. reflexivity.
   split. reflexivity.
-  intros. unfold compare_float. repeat SIMP.
+  intros. unfold compare_float. Simpl.
 Qed.
 
 Lemma compare_sint_spec:
@@ -593,7 +178,7 @@ Proof.
   split. reflexivity.
   split. reflexivity.
   split. reflexivity.
-  intros. unfold compare_sint. repeat SIMP.
+  intros. unfold compare_sint. Simpl.
 Qed.
 
 Lemma compare_uint_spec:
@@ -608,7 +193,7 @@ Proof.
   split. reflexivity.
   split. reflexivity.
   split. reflexivity.
-  intros. unfold compare_uint. repeat SIMP.
+  intros. unfold compare_uint. Simpl.
 Qed.
 
 (** Loading a constant. *)
@@ -616,35 +201,25 @@ Qed.
 Lemma loadimm_correct:
   forall r n k rs m,
   exists rs',
-     exec_straight (loadimm r n k) rs m  k rs' m
+     exec_straight ge fn (loadimm r n k) rs m  k rs' m
   /\ rs'#r = Vint n
   /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
   intros. unfold loadimm.
   case (Int.eq (high_s n) Int.zero).
   (* addi *)
-  exists (nextinstr (rs#r <- (Vint n))).
-  split. apply exec_straight_one. 
-  simpl. rewrite Int.add_zero_l. auto.
-  reflexivity. 
-  split. repeat SIMP. intros; repeat SIMP. 
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
+  rewrite Int.add_zero_l. intuition Simpl.
   (* addis *)
   generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro.
-  exists (nextinstr (rs#r <- (Vint n))).
-  split. apply exec_straight_one. 
-  simpl. rewrite Int.add_commut. 
-  rewrite <- H. rewrite low_high_s. reflexivity.
-  reflexivity. 
-  split. repeat SIMP. intros; repeat SIMP. 
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
+  rewrite <- H. rewrite Int.add_commut. rewrite low_high_s. 
+  intuition Simpl.
   (* addis + ori *)
-  pose (rs1 := nextinstr (rs#r <- (Vint (Int.shl (high_u n) (Int.repr 16))))).
-  exists (nextinstr (rs1#r <- (Vint n))).
-  split. eapply exec_straight_two. 
-  simpl. rewrite Int.add_zero_l. reflexivity.
-  simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  unfold Val.or. rewrite low_high_u. reflexivity.
-  reflexivity. reflexivity.
-  unfold rs1. split. repeat SIMP. intros; repeat SIMP. 
+  econstructor; split. eapply exec_straight_two. 
+  simpl; eauto. simpl; eauto. auto. auto.
+  split. Simpl. rewrite Int.add_zero_l. unfold Val.or. rewrite low_high_u. auto.
+  intros; Simpl.
 Qed.
 
 (** Add integer immediate. *)
@@ -654,37 +229,31 @@ Lemma addimm_correct:
   r1 <> GPR0 ->
   r2 <> GPR0 ->
   exists rs',
-     exec_straight (addimm r1 r2 n k) rs m  k rs' m
+     exec_straight ge fn (addimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = Val.add rs#r2 (Vint n)
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
   intros. unfold addimm.
   (* addi *)
   case (Int.eq (high_s n) Int.zero).
-  exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))).
-  split. apply exec_straight_one. 
-  simpl. rewrite gpr_or_zero_not_zero; auto.
-  reflexivity. 
-  split. repeat SIMP. intros. repeat SIMP.
+  econstructor; split. apply exec_straight_one. 
+  simpl. rewrite gpr_or_zero_not_zero; eauto.
+  reflexivity.
+  intuition Simpl.
   (* addis *)
   generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro.
-  exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))).
-  split. apply exec_straight_one.
-  simpl. rewrite gpr_or_zero_not_zero; auto.
-  generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. intro.
-  rewrite H2. auto.
-  reflexivity.
-  split. repeat SIMP. intros; repeat SIMP.
+  econstructor; split. apply exec_straight_one.
+  simpl. rewrite gpr_or_zero_not_zero; auto. auto. 
+  split. Simpl. 
+  generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. congruence. 
+  intros; Simpl.
   (* addis + addi *)
-  pose (rs1 := nextinstr (rs#r1 <- (Val.add rs#r2 (Vint (Int.shl (high_s n) (Int.repr 16)))))).
-  exists (nextinstr (rs1#r1 <- (Val.add rs#r2 (Vint n)))).
-  split. apply exec_straight_two with rs1 m.
-  simpl. rewrite gpr_or_zero_not_zero; auto. 
-  simpl. rewrite gpr_or_zero_not_zero; auto.
-  unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
-  rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
-  reflexivity. reflexivity. 
-  unfold rs1; split. repeat SIMP. intros; repeat SIMP.
+  econstructor; split. eapply exec_straight_two.
+  simpl. rewrite gpr_or_zero_not_zero; eauto. 
+  simpl. rewrite gpr_or_zero_not_zero; eauto.
+  auto. auto. 
+  split. Simpl. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
+  intros; Simpl.
 Qed. 
 
 (** And integer immediate. *)
@@ -694,10 +263,10 @@ Lemma andimm_base_correct:
   r2 <> GPR0 ->
   let v := Val.and rs#r2 (Vint n) in
   exists rs',
-     exec_straight (andimm_base r1 r2 n k) rs m  k rs' m
+     exec_straight ge fn (andimm_base r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = v
   /\ rs'#CR0_2 = Val.cmp Ceq v Vzero
-  /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
+  /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
 Proof.
   intros. unfold andimm_base.
   case (Int.eq (high_u n) Int.zero).
@@ -706,9 +275,9 @@ Proof.
   generalize (compare_sint_spec (rs#r1 <- v) v Vzero).
   intros [A [B [C D]]].
   split. apply exec_straight_one. reflexivity. reflexivity.
-  split. rewrite D; auto with ppcgen. SIMP. 
+  split. rewrite D; auto with asmgen. Simpl.
   split. auto.
-  intros. rewrite D; auto with ppcgen. SIMP.
+  intros. rewrite D; auto with asmgen. Simpl.
   (* andis *)
   generalize (Int.eq_spec (low_u n) Int.zero);
   case (Int.eq (low_u n) Int.zero); intro.
@@ -718,9 +287,9 @@ Proof.
   split. apply exec_straight_one. simpl.
   generalize (low_high_u n). rewrite H0. rewrite Int.or_zero. 
   intro. rewrite H1. reflexivity. reflexivity.
-  split. rewrite D; auto with ppcgen. SIMP. 
+  split. rewrite D; auto with asmgen. Simpl.
   split. auto.
-  intros. rewrite D; auto with ppcgen. SIMP.
+  intros. rewrite D; auto with asmgen. Simpl.
   (* loadimm + and *)
   generalize (loadimm_correct GPR0 n (Pand_ r1 r2 GPR0 :: k) rs m).
   intros [rs1 [EX1 [RES1 OTHER1]]].
@@ -731,25 +300,24 @@ Proof.
   apply exec_straight_one. simpl. rewrite RES1. 
   rewrite (OTHER1 r2). reflexivity. congruence. congruence.
   reflexivity. 
-  split. rewrite D; auto with ppcgen. SIMP. 
+  split. rewrite D; auto with asmgen. Simpl.
   split. auto.
-  intros. rewrite D; auto with ppcgen. SIMP.
+  intros. rewrite D; auto with asmgen. Simpl.
 Qed.
 
 Lemma andimm_correct:
   forall r1 r2 n k (rs : regset) m,
   r2 <> GPR0 ->
   exists rs',
-     exec_straight (andimm r1 r2 n k) rs m  k rs' m
+     exec_straight ge fn (andimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = Val.and rs#r2 (Vint n)
-  /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
+  /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
 Proof.
   intros. unfold andimm. destruct (is_rlw_mask n).
   (* turned into rlw *)
-  exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))).
-  split. apply exec_straight_one. simpl. rewrite Val.rolm_zero. auto. reflexivity.
-  split. SIMP. apply Pregmap.gss. 
-  intros. SIMP. apply Pregmap.gso; auto with ppcgen.
+  econstructor; split. eapply exec_straight_one.
+  simpl. rewrite Val.rolm_zero. eauto. auto. 
+  intuition Simpl.
   (* andimm_base *)
   destruct (andimm_base_correct r1 r2 n k rs m) as [rs' [A [B [C D]]]]; auto.
   exists rs'; auto.
@@ -761,7 +329,7 @@ Lemma orimm_correct:
   forall r1 (r2: ireg) n k (rs : regset) m,
   let v := Val.or rs#r2 (Vint n) in
   exists rs',
-     exec_straight (orimm r1 r2 n k) rs m  k rs' m
+     exec_straight ge fn (orimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = v
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
@@ -770,8 +338,7 @@ Proof.
   (* ori *)
   exists (nextinstr (rs#r1 <- v)).
   split. apply exec_straight_one. reflexivity. reflexivity.
-  split. repeat SIMP.
-  intros. repeat SIMP.
+  intuition Simpl.
   (* oris *)
   generalize (Int.eq_spec (low_u n) Int.zero);
   case (Int.eq (low_u n) Int.zero); intro.
@@ -779,12 +346,11 @@ Proof.
   split. apply exec_straight_one. simpl.
   generalize (low_high_u n). rewrite H. rewrite Int.or_zero. 
   intro. rewrite H0. reflexivity. reflexivity.
-  split. repeat SIMP.
-  intros. repeat SIMP.
+  intuition Simpl.
   (* oris + ori *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
-  split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss.   rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. 
-  intros. repeat SIMP.
+  intuition Simpl. 
+  rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. 
 Qed.
 
 (** Xor integer immediate. *)
@@ -793,7 +359,7 @@ Lemma xorimm_correct:
   forall r1 (r2: ireg) n k (rs : regset) m,
   let v := Val.xor rs#r2 (Vint n) in
   exists rs',
-     exec_straight (xorimm r1 r2 n k) rs m  k rs' m
+     exec_straight ge fn (xorimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = v
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
@@ -802,20 +368,19 @@ Proof.
   (* xori *)
   exists (nextinstr (rs#r1 <- v)).
   split. apply exec_straight_one. reflexivity. reflexivity.
-  split. repeat SIMP. intros. repeat SIMP.
+  intuition Simpl.
   (* xoris *)
   generalize (Int.eq_spec (low_u n) Int.zero);
   case (Int.eq (low_u n) Int.zero); intro.
   exists (nextinstr (rs#r1 <- v)).
   split. apply exec_straight_one. simpl.
-  generalize (low_high_u_xor n). rewrite H. rewrite Int.xor_zero. 
+  generalize (low_high_u n). rewrite H. rewrite Int.or_zero. 
   intro. rewrite H0. reflexivity. reflexivity.
-  split. repeat SIMP. intros. repeat SIMP.
+  intuition Simpl.
   (* xoris + xori *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
-  split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss.
+  intuition Simpl. 
   rewrite Val.xor_assoc. simpl. rewrite low_high_u_xor. reflexivity. 
-  intros. repeat SIMP.
 Qed.
 
 (** Rotate and mask. *)
@@ -824,95 +389,108 @@ Lemma rolm_correct:
   forall r1 r2 amount mask k (rs : regset) m,
   r1 <> GPR0 ->
   exists rs',
-     exec_straight (rolm r1 r2 amount mask k) rs m  k rs' m
+     exec_straight ge fn (rolm r1 r2 amount mask k) rs m  k rs' m
   /\ rs'#r1 = Val.rolm rs#r2 amount mask
-  /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
+  /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
 Proof.
   intros. unfold rolm. destruct (is_rlw_mask mask).
   (* rlwinm *)
-  exists (nextinstr (rs#r1 <- (Val.rolm rs#r2 amount mask))).
-  split. apply exec_straight_one; auto.
-  split. SIMP. apply Pregmap.gss.
-  intros. SIMP. apply Pregmap.gso; auto.
+  econstructor; split. eapply exec_straight_one; simpl; eauto.
+  intuition Simpl.
   (* rlwinm ; andimm *)
   set (rs1 := nextinstr (rs#r1 <- (Val.rolm rs#r2 amount Int.mone))).
   destruct (andimm_base_correct r1 r1 mask k rs1 m) as [rs' [A [B [C D]]]]; auto.
   exists rs'.
   split. eapply exec_straight_step; eauto. auto. auto. 
-  split. rewrite B. unfold rs1. SIMP. rewrite Pregmap.gss. 
-  destruct (rs r2); simpl; auto. unfold Int.rolm. rewrite Int.and_assoc. 
+  split. rewrite B. unfold rs1. rewrite nextinstr_inv; auto with asmgen. 
+  rewrite Pregmap.gss. destruct (rs r2); simpl; auto. 
+  unfold Int.rolm. rewrite Int.and_assoc. 
   decEq; decEq; decEq. rewrite Int.and_commut. apply Int.and_mone.
-  intros. rewrite D; auto. unfold rs1; SIMP. apply Pregmap.gso; auto.
+  intros. rewrite D; auto. unfold rs1; Simpl. 
 Qed.
 
 (** Indexed memory loads. *)
 
 Lemma loadind_correct:
-  forall (base: ireg) ofs ty dst k (rs: regset) m v,
+  forall (base: ireg) ofs ty dst k (rs: regset) m v c,
+  loadind base ofs ty dst k = OK c ->
   Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v ->
-  mreg_type dst = ty ->
   base <> GPR0 ->
   exists rs',
-     exec_straight (loadind base ofs ty dst k) rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of dst) = v
   /\ forall r, r <> PC -> r <> preg_of dst -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
-  intros. unfold loadind. destruct (Int.eq (high_s ofs) Int.zero).
-(* one load *)
-  exists (nextinstr (rs#(preg_of dst) <- v)); split.
-  unfold preg_of. rewrite H0.
-  destruct ty; apply exec_straight_one; auto with ppcgen; simpl.
-  unfold load1. rewrite gpr_or_zero_not_zero; auto.
-  simpl in *. rewrite H. auto.
-  unfold load1. rewrite gpr_or_zero_not_zero; auto.
-  simpl in *. rewrite H. auto.
-  split. repeat SIMP. intros. repeat SIMP.
-(* loadimm + one load *)
+Opaque Int.eq.
+  unfold loadind; intros. destruct ty; monadInv H; simpl in H0.
+(* integer *)
+  rewrite (ireg_of_eq _ _ EQ).
+  destruct (Int.eq (high_s ofs) Int.zero).
+  (* one load *)
+  econstructor; split. apply exec_straight_one. simpl.
+  unfold load1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto.
+  intuition Simpl.
+  (* loadimm + load *)
+  exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
+  exists (nextinstr (rs'#x <- v)); split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. 
+  simpl. unfold load2. rewrite C; auto with asmgen. rewrite B. rewrite H0. auto. 
+  intuition Simpl. 
+(* float *)
+  rewrite (freg_of_eq _ _ EQ).
+  destruct (Int.eq (high_s ofs) Int.zero).
+  (* one load *)
+  econstructor; split. apply exec_straight_one. simpl.
+  unfold load1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto.
+  intuition Simpl.
+  (* loadimm + load *)
   exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
-  exists (nextinstr (rs'#(preg_of dst) <- v)); split.
-  eapply exec_straight_trans. eexact A.
-  unfold preg_of. rewrite H0.
-  destruct ty; apply exec_straight_one; auto with ppcgen; simpl.
-  unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto.
-  unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto.
-  split. repeat SIMP.
-  intros. repeat SIMP. 
+  exists (nextinstr (rs'#x <- v)); split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. 
+  simpl. unfold load2. rewrite C; auto with asmgen. rewrite B. rewrite H0. auto. 
+  intuition Simpl. 
 Qed.
 
 (** Indexed memory stores. *)
 
 Lemma storeind_correct:
-  forall (base: ireg) ofs ty src k (rs: regset) m m',
+  forall (base: ireg) ofs ty src k (rs: regset) m m' c,
+  storeind src base ofs ty k = OK c ->
   Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' ->
-  mreg_type src = ty ->
   base <> GPR0 ->
   exists rs',
-     exec_straight (storeind src base ofs ty k) rs m k rs' m'
+     exec_straight ge fn c rs m k rs' m'
   /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
-  intros. unfold storeind. destruct (Int.eq (high_s ofs) Int.zero).
-(* one store *)
-  exists (nextinstr rs); split.
-  destruct ty; apply exec_straight_one; auto with ppcgen; simpl.
-  unfold store1. rewrite gpr_or_zero_not_zero; auto.
-  simpl in *. unfold preg_of in H; rewrite H0 in H. rewrite H. auto.
-  unfold store1. rewrite gpr_or_zero_not_zero; auto.
-  simpl in *. unfold preg_of in H; rewrite H0 in H. rewrite H. auto.
-  intros. apply nextinstr_inv; auto.
-(* loadimm + one store *)
+  unfold storeind; intros.
+  assert (preg_of src <> GPR0) by auto with asmgen.
+  destruct ty; monadInv H; simpl in H0.
+(* integer *)
+  rewrite (ireg_of_eq _ _ EQ) in *.
+  destruct (Int.eq (high_s ofs) Int.zero).
+  (* one store *)
+  econstructor; split. apply exec_straight_one. simpl.
+  unfold store1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto.
+  intros; Simpl.
+  (* loadimm + store *)
+  exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
+  exists (nextinstr rs'); split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. 
+  simpl. unfold store2. rewrite B. rewrite ! C; auto with asmgen. rewrite H0. auto. 
+  intuition Simpl. 
+(* float *)
+  rewrite (freg_of_eq _ _ EQ) in *.
+  destruct (Int.eq (high_s ofs) Int.zero).
+  (* one store *)
+  econstructor; split. apply exec_straight_one. simpl.
+  unfold store1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto.
+  intuition Simpl.
+  (* loadimm + store *)
   exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
-  assert (rs' base = rs base). apply C; auto with ppcgen. 
-  assert (rs' (preg_of src) = rs (preg_of src)). apply C; auto with ppcgen. 
-  exists (nextinstr rs').
-  split. eapply exec_straight_trans. eexact A. 
-  destruct ty; apply exec_straight_one; auto with ppcgen; simpl.
-  unfold store2. replace (IR (ireg_of src)) with (preg_of src). 
-  rewrite H2; rewrite H3. rewrite B. simpl in H. rewrite H. auto.
-  unfold preg_of; rewrite H0; auto.
-  unfold store2. replace (FR (freg_of src)) with (preg_of src). 
-  rewrite H2; rewrite H3. rewrite B. simpl in H. rewrite H. auto.
-  unfold preg_of; rewrite H0; auto.
-  intros. rewrite nextinstr_inv; auto. 
+  exists (nextinstr rs'); split. 
+  eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. 
+  simpl. unfold store2. rewrite B. rewrite ! C; auto with asmgen. rewrite H0. auto. 
+  intuition Simpl. 
 Qed.
 
 (** Float comparisons. *)
@@ -920,7 +498,7 @@ Qed.
 Lemma floatcomp_correct:
   forall cmp (r1 r2: freg) k rs m,
   exists rs',
-     exec_straight (floatcomp cmp r1 r2 k) rs m k rs' m
+     exec_straight ge fn (floatcomp cmp r1 r2 k) rs m k rs' m
   /\ rs'#(reg_of_crbit (fst (crbit_for_fcmp cmp))) = 
        (if snd (crbit_for_fcmp cmp)
         then Val.cmpf cmp rs#r1 rs#r2
@@ -938,10 +516,10 @@ Proof.
     case cmp; tauto.
   unfold floatcomp.  elim H; intro; clear H.
   exists rs1.
-  split. generalize H0; intros [EQ|[EQ|[EQ|EQ]]]; subst cmp;
+  split. destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp;
   apply exec_straight_one; reflexivity.
   split. 
-  generalize H0; intros [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. 
+  destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. 
   rewrite Val.negate_cmpf_eq. auto.
   auto.
   (* two instrs *)
@@ -958,155 +536,132 @@ Proof.
   split. elim H0; intro; subst cmp; simpl.
   reflexivity.
   reflexivity.
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  intros. Simpl. 
 Qed.
 
-Ltac TypeInv :=
-  match goal with
-  | H: (List.map ?f ?x = nil) |- _ =>
-      destruct x; [clear H | simpl in H; discriminate]
-  | H: (List.map ?f ?x = ?hd :: ?tl) |- _ =>
-      destruct x; simpl in H;
-      [ discriminate |
-        injection H; clear H; let T := fresh "T" in (
-          intros H T; TypeInv) ]
-  | _ => idtac
-  end.
-
-Ltac UseTypeInfo :=
-  match goal with
-  | T: (mreg_type ?r = ?t), H: context[preg_of ?r] |- _ =>
-      unfold preg_of in H; UseTypeInfo
-  | T: (mreg_type ?r = ?t), H: context[mreg_type ?r] |- _ =>
-      rewrite T in H; UseTypeInfo
-  | T: (mreg_type ?r = ?t) |- context[preg_of ?r] =>
-      unfold preg_of; UseTypeInfo
-  | T: (mreg_type ?r = ?t) |- context[mreg_type ?r] =>
-      rewrite T; UseTypeInfo
-  | _ => idtac
-  end.
-
 (** Translation of conditions. *)
 
+Ltac ArgsInv :=
+  repeat (match goal with
+  | [ H: Error _ = OK _ |- _ ] => discriminate
+  | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args
+  | [ H: bind _ _ = OK _ |- _ ] => monadInv H
+  | [ H: assertion _ = OK _ |- _ ] => monadInv H
+  end);
+  subst;
+  repeat (match goal with
+  | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *
+  | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *
+  end).
+
 Lemma transl_cond_correct_1:
-  forall cond args k rs m,
-  map mreg_type args = type_of_condition cond ->
+  forall cond args k rs m c,
+  transl_cond cond args k = OK c ->
   exists rs',
-     exec_straight (transl_cond cond args k) rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
        (if snd (crbit_for_cond cond)
         then Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)
         else Val.notbool (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)))
-  /\ forall r, is_data_reg r = true -> rs'#r = rs#r.
+  /\ forall r, data_preg r = true -> rs'#r = rs#r.
 Proof.
   intros.
 Opaque Int.eq.
-  destruct cond; simpl in H; TypeInv; simpl; UseTypeInfo.
+  unfold transl_cond in H; destruct cond; ArgsInv; simpl.
   (* Ccomp *)
-  fold (Val.cmp c (rs (ireg_of m0)) (rs (ireg_of m1))).
-  destruct (compare_sint_spec rs (rs (ireg_of m0)) (rs (ireg_of m1)))
-  as [A [B [C D]]].
+  fold (Val.cmp c0 (rs x) (rs x0)).
+  destruct (compare_sint_spec rs (rs x) (rs x0)) as [A [B [C D]]].
   econstructor; split.
   apply exec_straight_one. simpl; reflexivity. reflexivity.
   split. 
-  case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
-  auto with ppcgen.
+  case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
+  auto with asmgen.
   (* Ccompu *)
-  fold (Val.cmpu (Mem.valid_pointer m) c (rs (ireg_of m0)) (rs (ireg_of m1))).
-  destruct (compare_uint_spec rs m (rs (ireg_of m0)) (rs (ireg_of m1)))
-  as [A [B [C D]]].
+  fold (Val.cmpu (Mem.valid_pointer m) c0 (rs x) (rs x0)).
+  destruct (compare_uint_spec rs m (rs x) (rs x0)) as [A [B [C D]]].
   econstructor; split.
   apply exec_straight_one. simpl; reflexivity. reflexivity.
   split. 
-  case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
-  auto with ppcgen.
+  case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
+  auto with asmgen.
   (* Ccompimm *)
-  fold (Val.cmp c (rs (ireg_of m0)) (Vint i)).
-  case (Int.eq (high_s i) Int.zero).
-  destruct (compare_sint_spec rs (rs (ireg_of m0)) (Vint i))
-  as [A [B [C D]]].
+  fold (Val.cmp c0 (rs x) (Vint i)).
+  destruct (Int.eq (high_s i) Int.zero); inv EQ0.
+  destruct (compare_sint_spec rs (rs x) (Vint i)) as [A [B [C D]]].
   econstructor; split.
-  apply exec_straight_one. simpl. eauto. reflexivity.
+  apply exec_straight_one. simpl; reflexivity. reflexivity.
   split. 
-  case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
-  auto with ppcgen.
-  generalize (loadimm_correct GPR0 i (Pcmpw (ireg_of m0) GPR0 :: k) rs m).
-  intros [rs1 [EX1 [RES1 OTH1]]].
-  destruct (compare_sint_spec rs1 (rs (ireg_of m0)) (Vint i))
-  as [A [B [C D]]].
-  assert (rs1 (ireg_of m0) = rs (ireg_of m0)).
-    apply OTH1; auto with ppcgen. 
-  exists (nextinstr (compare_sint rs1 (rs1 (ireg_of m0)) (Vint i))).
+  case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
+  auto with asmgen.
+  destruct (loadimm_correct GPR0 i (Pcmpw x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]].
+  destruct (compare_sint_spec rs1 (rs x) (Vint i)) as [A [B [C D]]].
+  assert (SAME: rs1 x = rs x) by (apply OTH1; eauto with asmgen).
+  exists (nextinstr (compare_sint rs1 (rs1 x) (Vint i))).
   split. eapply exec_straight_trans. eexact EX1.
-  apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto.
+  apply exec_straight_one. simpl. rewrite RES1; rewrite SAME; auto.
   reflexivity. 
-  split. rewrite H. 
-  case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
-  intros. rewrite H; rewrite D; auto with ppcgen.
+  split. rewrite SAME. 
+  case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
+  intros. rewrite SAME; rewrite D; auto with asmgen.
   (* Ccompuimm *)
-  fold (Val.cmpu (Mem.valid_pointer m) c (rs (ireg_of m0)) (Vint i)).
-  case (Int.eq (high_u i) Int.zero).
-  destruct (compare_uint_spec rs m (rs (ireg_of m0)) (Vint i))
-  as [A [B [C D]]].
+  fold (Val.cmpu (Mem.valid_pointer m) c0 (rs x) (Vint i)).
+  destruct (Int.eq (high_u i) Int.zero); inv EQ0.
+  destruct (compare_uint_spec rs m (rs x) (Vint i)) as [A [B [C D]]].
   econstructor; split.
-  apply exec_straight_one. simpl. eauto. reflexivity.
+  apply exec_straight_one. simpl; reflexivity. reflexivity.
   split. 
-  case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
-  auto with ppcgen.
-  generalize (loadimm_correct GPR0 i (Pcmplw (ireg_of m0) GPR0 :: k) rs m).
-  intros [rs1 [EX1 [RES1 OTH1]]].
-  destruct (compare_uint_spec rs1 m (rs (ireg_of m0)) (Vint i))
-  as [A [B [C D]]].
-  assert (rs1 (ireg_of m0) = rs (ireg_of m0)). apply OTH1; auto with ppcgen.
-  exists (nextinstr (compare_uint rs1 m (rs1 (ireg_of m0)) (Vint i))).
+  case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
+  auto with asmgen.
+  destruct (loadimm_correct GPR0 i (Pcmplw x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]].
+  destruct (compare_uint_spec rs1 m (rs x) (Vint i)) as [A [B [C D]]].
+  assert (SAME: rs1 x = rs x) by (apply OTH1; eauto with asmgen).
+  exists (nextinstr (compare_uint rs1 m (rs1 x) (Vint i))).
   split. eapply exec_straight_trans. eexact EX1.
-  apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto.
+  apply exec_straight_one. simpl. rewrite RES1; rewrite SAME; auto.
   reflexivity. 
-  split. rewrite H. 
-  case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
-  intros. rewrite H; rewrite D; auto with ppcgen.
+  split. rewrite SAME. 
+  case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
+  intros. rewrite SAME; rewrite D; auto with asmgen.
   (* Ccompf *)
-  fold (Val.cmpf c (rs (freg_of m0)) (rs (freg_of m1))).
-  destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m)
-  as [rs' [EX [RES OTH]]].
+  fold (Val.cmpf c0 (rs x) (rs x0)).
+  destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]].
   exists rs'. split. auto. 
   split. apply RES. 
-  auto with ppcgen.
+  auto with asmgen.
   (* Cnotcompf *)
   rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4.
-  fold (Val.cmpf c (rs (freg_of m0)) (rs (freg_of m1))).
-  destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m)
-  as [rs' [EX [RES OTH]]].
+  fold (Val.cmpf c0 (rs x) (rs x0)).
+  destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]].
   exists rs'. split. auto. 
-  split. rewrite RES. destruct (snd (crbit_for_fcmp c)); auto. 
-  auto with ppcgen.
+  split. rewrite RES. destruct (snd (crbit_for_fcmp c0)); auto. 
+  auto with asmgen.
   (* Cmaskzero *)
-  destruct (andimm_base_correct GPR0 (ireg_of m0) i k rs m)
-  as [rs' [A [B [C D]]]]. auto with ppcgen.
+  destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]].
+  eauto with asmgen.
   exists rs'. split. assumption. 
-  split. rewrite C. destruct (rs (ireg_of m0)); auto. 
-  auto with ppcgen.
+  split. rewrite C. destruct (rs x); auto. 
+  auto with asmgen.
   (* Cmasknotzero *)
-  destruct (andimm_base_correct GPR0 (ireg_of m0) i k rs m)
-  as [rs' [A [B [C D]]]]. auto with ppcgen.
+  destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]].
+  eauto with asmgen.
   exists rs'. split. assumption. 
-  split. rewrite C. destruct (rs (ireg_of m0)); auto.
+  split. rewrite C. destruct (rs x); auto.
   fold (option_map negb (Some (Int.eq (Int.and i0 i) Int.zero))).
   rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. auto. 
-  auto with ppcgen.
+  auto with asmgen.
 Qed.
 
 Lemma transl_cond_correct_2:
-  forall cond args k rs m b,
-  map mreg_type args = type_of_condition cond ->
+  forall cond args k rs m b c,
+  transl_cond cond args k = OK c ->
   eval_condition cond (map rs (map preg_of args)) m = Some b ->
   exists rs',
-     exec_straight (transl_cond cond args k) rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
        (if snd (crbit_for_cond cond)
         then Val.of_bool b
         else Val.notbool (Val.of_bool b))
-  /\ forall r, is_data_reg r = true -> rs'#r = rs#r.
+  /\ forall r, data_preg r = true -> rs'#r = rs#r.
 Proof.
   intros.
   replace (Val.of_bool b)
@@ -1115,14 +670,14 @@ Proof.
   rewrite H0; auto.
 Qed.
 
-Lemma transl_cond_correct:
-  forall cond args k ms sp rs m b m',
-  map mreg_type args = type_of_condition cond ->
+Lemma transl_cond_correct_3:
+  forall cond args k ms sp rs m b m' c,
+  transl_cond cond args k = OK c ->
   agree ms sp rs ->
   eval_condition cond (map ms args) m = Some b ->
   Mem.extends m m' ->
   exists rs',
-     exec_straight (transl_cond cond args k) rs m' k rs' m'
+     exec_straight ge fn c rs m' k rs' m'
   /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
        (if snd (crbit_for_cond cond)
         then Val.of_bool b
@@ -1184,66 +739,60 @@ Transparent Int.eq.
 Qed.
 
 Lemma transl_cond_op_correct:
-  forall cond args r k rs m,
-  mreg_type r = Tint ->
-  map mreg_type args = type_of_condition cond ->
+  forall cond args r k rs m c,
+  transl_cond_op cond args r k = OK c ->
   exists rs',
-     exec_straight (transl_cond_op cond args r k) rs m k rs' m
-  /\ rs'#(ireg_of r) = Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)
-  /\ forall r', is_data_reg r' = true -> r' <> ireg_of r -> rs'#r' = rs#r'.
+     exec_straight ge fn c rs m k rs' m
+  /\ rs'#(preg_of r) = Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)
+  /\ forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r'.
 Proof.
   intros until args. unfold transl_cond_op.
-  destruct (classify_condition cond args);
-  intros until m; intros TY1 TY2; simpl in TY2.
+  destruct (classify_condition cond args); intros; monadInv H; simpl;
+  erewrite ! ireg_of_eq; eauto.
 (* eq 0 *)
-  inv TY2. simpl. unfold preg_of; rewrite H0. 
   econstructor; split.
   eapply exec_straight_two; simpl; reflexivity.
-  split. repeat SIMP. destruct (rs (ireg_of r)); simpl; auto. 
+  split. Simpl. destruct (rs x0); simpl; auto.  
   apply add_carry_eq0.
-  intros; repeat SIMP.
+  intros; Simpl.
 (* ne 0 *)
-  inv TY2. simpl. unfold preg_of; rewrite H0.
   econstructor; split.
   eapply exec_straight_two; simpl; reflexivity.
-  split. repeat SIMP. rewrite gpr_or_zero_not_zero; auto with ppcgen.
-  destruct (rs (ireg_of r)); simpl; auto.
+  rewrite gpr_or_zero_not_zero; eauto with asmgen.
+  split. Simpl. destruct (rs x0); simpl; auto.  
   apply add_carry_ne0.
-  intros; repeat SIMP.
+  intros; Simpl.
 (* ge 0 *)
-  inv TY2. simpl. unfold preg_of; rewrite H0.
   econstructor; split.
   eapply exec_straight_two; simpl; reflexivity.
-  split. repeat SIMP. rewrite Val.rolm_ge_zero. auto.  
-  intros; repeat SIMP.
+  split. Simpl. rewrite Val.rolm_ge_zero. auto.  
+  intros; Simpl.
 (* lt 0 *)
-  inv TY2. simpl. unfold preg_of; rewrite H0.
   econstructor; split.
   apply exec_straight_one; simpl; reflexivity.
-  split. repeat SIMP. rewrite Val.rolm_lt_zero. auto. 
-  intros; repeat SIMP.
+  split. Simpl. rewrite Val.rolm_lt_zero. auto. 
+  intros; Simpl.
 (* default *)
-  set (bit := fst (crbit_for_cond c)).
-  set (isset := snd (crbit_for_cond c)).
+  set (bit := fst (crbit_for_cond c)) in *.
+  set (isset := snd (crbit_for_cond c)) in *.
   set (k1 :=
-        Pmfcrbit (ireg_of r) bit ::
+        Pmfcrbit x bit ::
         (if isset
          then k
-         else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)).
-  generalize (transl_cond_correct_1 c rl k1 rs m TY2).
+         else Pxori x x (Cint Int.one) :: k)).
+  generalize (transl_cond_correct_1 c rl k1 rs m c0 EQ0).
   fold bit; fold isset. 
   intros [rs1 [EX1 [RES1 AG1]]].
   destruct isset.
   (* bit set *)
   econstructor; split.  eapply exec_straight_trans. eexact EX1. 
-  unfold k1. apply exec_straight_one; simpl; reflexivity. 
-  split. repeat SIMP. intros; repeat SIMP.
+  unfold k1. apply exec_straight_one; simpl; reflexivity.
+  intuition Simpl.
   (* bit clear *)
   econstructor; split.  eapply exec_straight_trans. eexact EX1. 
-  unfold k1. eapply exec_straight_two; simpl; reflexivity. 
-  split. repeat SIMP. rewrite RES1. 
-  destruct (eval_condition c rs ## (preg_of ## rl) m). destruct b; auto. auto.
-  intros; repeat SIMP.
+  unfold k1. eapply exec_straight_two; simpl; reflexivity.
+  intuition Simpl.
+  rewrite RES1. destruct (eval_condition c rs ## (preg_of ## rl) m). destruct b; auto. auto.
 Qed.
 
 (** Translation of arithmetic operations. *)
@@ -1251,137 +800,123 @@ Qed.
 Ltac TranslOpSimpl :=
   econstructor; split;
   [ apply exec_straight_one; [simpl; eauto | reflexivity]
-  | split; intros; (repeat SIMP; fail) ].
+  | split; intros; Simpl; fail ].
 
 Lemma transl_op_correct_aux:
-  forall op args res k (rs: regset) m v,
-  wt_instr (Mop op args res) ->
+  forall op args res k (rs: regset) m v c,
+  transl_op op args res k = OK c ->
   eval_operation ge (rs#GPR1) op (map rs (map preg_of args)) m = Some v ->
   exists rs',
-     exec_straight (transl_op op args res k) rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of res) = v
   /\ forall r,
-     match op with Omove => is_data_reg r = true | _ => is_nontemp_reg r = true end ->
+     match op with Omove => data_preg r = true | _ => nontemp_preg r = true end ->
      r <> preg_of res -> rs'#r = rs#r.
 Proof.
-  intros until v; intros WT EV.
-  inv WT.
+Opaque Int.eq. Opaque Int.repr.
+  intros. unfold transl_op in H; destruct op; ArgsInv; simpl in H0; try (inv H0); try TranslOpSimpl.
   (* Omove *)
-  simpl in *. inv EV. 
-  exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))).
-  split. unfold preg_of. rewrite <- H0.
-  destruct (mreg_type r1); apply exec_straight_one; auto.
-  split. repeat SIMP. intros; repeat SIMP.
-  (* Other instructions *)
-Opaque Int.eq.
-  destruct op; simpl; simpl in H3; injection H3; clear H3; intros;
-  TypeInv; simpl in *; UseTypeInfo; inv EV; try (TranslOpSimpl).
+  destruct (preg_of res) eqn:RES; destruct (preg_of m0) eqn:ARG; inv H.
+  TranslOpSimpl.
+  TranslOpSimpl.
   (* Ointconst *)
-  destruct (loadimm_correct (ireg_of res) i k rs m) as [rs' [A [B C]]]. 
-  exists rs'. split. auto. split. auto. auto with ppcgen.
+  destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]]. 
+  exists rs'. auto with asmgen. 
   (* Oaddrsymbol *)
   change (symbol_address ge i i0) with (symbol_offset ge i i0).
   set (v' := symbol_offset ge i i0).
-  caseEq (symbol_is_small_data i i0); intro SD.
+  destruct (symbol_is_small_data i i0) eqn:SD.
   (* small data *)
   econstructor; split. apply exec_straight_one; simpl; reflexivity.
-  split. repeat SIMP.
-  rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. 
+  split. Simpl. rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. 
   destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero; auto. 
-  intros; repeat SIMP.
+  intros; Simpl.
   (* not small data *)
 Opaque Val.add.
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
-  split. repeat SIMP. rewrite gpr_or_zero_zero.
-  rewrite gpr_or_zero_not_zero; auto with ppcgen. repeat SIMP. 
+  split. Simpl. rewrite gpr_or_zero_zero.
+  rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl.  
   rewrite (Val.add_commut Vzero). rewrite high_half_zero. 
   rewrite Val.add_commut. rewrite low_high_half. auto.
-  intros; repeat SIMP.
+  intros; Simpl.
   (* Oaddrstack *)
-  destruct (addimm_correct (ireg_of res) GPR1 i k rs m) as [rs' [EX [RES OTH]]].
-    auto with ppcgen. congruence.
-  exists rs'; auto with ppcgen.
+  destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen.
+  exists rs'; auto with asmgen.
   (* Oaddimm *)
-  destruct (addimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]; auto with ppcgen.
-  exists rs'; auto with ppcgen.
+  destruct (addimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen.
+  exists rs'; auto with asmgen.
   (* Osubimm *)
   case (Int.eq (high_s i) Int.zero).
   TranslOpSimpl.
-  destruct (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]].
+  destruct (loadimm_correct GPR0 i (Psubfc x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]].
   econstructor; split.
   eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity.
-  split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. 
-  intros; repeat SIMP. 
+  split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. 
+  intros; Simpl.
   (* Omulimm *)
   case (Int.eq (high_s i) Int.zero).
   TranslOpSimpl.
-  destruct (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]].
+  destruct (loadimm_correct GPR0 i (Pmullw x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]].
   econstructor; split.
   eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity.
-  split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. 
-  intros; repeat SIMP.
+  split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. 
+  intros; Simpl.
   (* Odivs *)
-  replace v with (Val.maketotal (Val.divs (rs (ireg_of m0)) (rs (ireg_of m1)))).
+  replace v with (Val.maketotal (Val.divs (rs x) (rs x0))).
   TranslOpSimpl. 
-  rewrite H2; auto.
+  rewrite H1; auto.
   (* Odivu *)
-  replace v with (Val.maketotal (Val.divu (rs (ireg_of m0)) (rs (ireg_of m1)))).
+  replace v with (Val.maketotal (Val.divu (rs x) (rs x0))).
   TranslOpSimpl. 
-  rewrite H2; auto.
+  rewrite H1; auto.
   (* Oand *)
-  set (v' := Val.and (rs (ireg_of m0)) (rs (ireg_of m1))) in *.
-  pose (rs1 := rs#(ireg_of res) <- v').
-  generalize (compare_sint_spec rs1 v' Vzero).
-  intros [A [B [C D]]].
+  set (v' := Val.and (rs x) (rs x0)) in *.
+  pose (rs1 := rs#x1 <- v').
+  destruct (compare_sint_spec rs1 v' Vzero) as [A [B [C D]]].
   econstructor; split. apply exec_straight_one; simpl; reflexivity.
-  split. rewrite D; auto with ppcgen. unfold rs1. SIMP. 
-  intros. rewrite D; auto with ppcgen. unfold rs1. SIMP.
+  split. rewrite D; auto with asmgen. unfold rs1; Simpl.
+  intros. rewrite D; auto with asmgen. unfold rs1; Simpl.
   (* Oandimm *)
-  destruct (andimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]; auto with ppcgen.
-  exists rs'; auto with ppcgen.
+  destruct (andimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen.
+  exists rs'; auto with asmgen.
   (* Oorimm *)
-  destruct (orimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. 
-  exists rs'; auto with ppcgen.
+  destruct (orimm_correct x0 x i k rs m) as [rs' [A [B C]]]. 
+  exists rs'; auto with asmgen.
   (* Oxorimm *)
-  destruct (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. 
-  exists rs'; auto with ppcgen.
+  destruct (xorimm_correct x0 x i k rs m) as [rs' [A [B C]]]. 
+  exists rs'; auto with asmgen.
   (* Onor *)
-  replace (Val.notint (rs (ireg_of m0)))
-     with (Val.notint (Val.or (rs (ireg_of m0)) (rs (ireg_of m0)))).
+  replace (Val.notint (rs x))
+     with (Val.notint (Val.or (rs x) (rs x))).
   TranslOpSimpl.
-  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.or_idem. auto.
+  destruct (rs x); simpl; auto. rewrite Int.or_idem. auto.
   (* Oshrximm *)
   econstructor; split.
   eapply exec_straight_two; simpl; reflexivity. 
-  split. repeat SIMP. apply Val.shrx_carry. auto. 
-  intros; repeat SIMP. 
+  split. Simpl. apply Val.shrx_carry. auto. 
+  intros; Simpl.
   (* Orolm *)
-  destruct (rolm_correct (ireg_of res) (ireg_of m0) i i0 k rs m) as [rs' [A [B C]]]; auto with ppcgen.
-  exists rs'; auto with ppcgen.
-  (* Oroli *)
-  destruct (mreg_eq m0 res). subst m0.
-  TranslOpSimpl.
-  econstructor; split.
-  eapply exec_straight_three; simpl; reflexivity. 
-  split. repeat SIMP. intros; repeat SIMP.
+  destruct (rolm_correct x0 x i i0 k rs m) as [rs' [A [B C]]]; eauto with asmgen.
+  exists rs'; auto with asmgen.
   (* Ointoffloat *)
-  replace v with (Val.maketotal (Val.intoffloat (rs (freg_of m0)))).
+  replace v with (Val.maketotal (Val.intoffloat (rs x))).
   TranslOpSimpl.
-  rewrite H2; auto.
+  rewrite H1; auto.
   (* Ocmp *)
-  destruct (transl_cond_op_correct c args res k rs m) as [rs' [A [B C]]]; auto.
-  exists rs'; auto with ppcgen.
+  destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto.
+  exists rs'; auto with asmgen.
 Qed.
 
 Lemma transl_op_correct:
-  forall op args res k ms sp rs m v m',
-  wt_instr (Mop op args res) ->
+  forall op args res k ms sp rs m v m' c,
+  transl_op op args res k = OK c ->
   agree ms sp rs ->
   eval_operation ge sp op (map ms args) m = Some v ->
   Mem.extends m m' ->
   exists rs',
-     exec_straight (transl_op op args res k) rs m' k rs' m'
-  /\ agree (Regmap.set res v (undef_op op ms)) sp rs'.
+     exec_straight ge fn c rs m' k rs' m'
+  /\ agree (Regmap.set res v (undef_op op ms)) sp rs'
+  /\ forall r, op = Omove -> data_preg r = true -> r <> preg_of res -> rs'#r = rs#r.
 Proof.
   intros. 
   exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. 
@@ -1389,74 +924,67 @@ Proof.
   exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]].
   rewrite <- Q in B.
   exists rs'; split. eexact P. 
-  unfold undef_op. destruct op;
-  (apply agree_set_mreg_undef_temps with rs || apply agree_set_mreg with rs);
+  split. unfold undef_op. destruct op;
+  (apply agree_set_undef_mreg with rs || apply agree_set_mreg with rs);
   auto.
+  intros. subst op. auto.
 Qed.
 
-Lemma transl_load_store_correct:
-  forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
-    addr args (temp: ireg) k ms sp rs m ms' m',
+(** Translation of memory accesses *)
+
+Lemma transl_memory_access_correct:
+  forall (P: regset -> Prop) mk1 mk2 addr args temp k c (rs: regset) a m m',
+  transl_memory_access mk1 mk2 addr args temp k = OK c ->
+  eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a ->
+  temp <> GPR0 ->
   (forall cst (r1: ireg) (rs1: regset) k,
-    eval_addressing ge sp addr (map rs (map preg_of args)) =
-                Some(Val.add (gpr_or_zero rs1 r1) (const_low ge cst)) ->
-    (forall (r: preg), r <> PC -> r <> temp -> rs1 r = rs r) ->
+    Val.add (gpr_or_zero rs1 r1) (const_low ge cst) = a ->
+    (forall r, r <> PC -> r <> temp -> rs1 r = rs r) ->
     exists rs',
-    exec_straight (mk1 cst r1 :: k) rs1 m k rs' m' /\
-    agree ms' sp rs') ->
-  (forall (r1 r2: ireg) k,
-    eval_addressing ge sp addr (map rs (map preg_of args)) = Some(Val.add rs#r1 rs#r2) ->
+        exec_straight ge fn (mk1 cst r1 :: k) rs1 m k rs' m' /\ P rs') ->
+  (forall (r1 r2: ireg) (rs1: regset) k,
+    Val.add rs1#r1 rs1#r2 = a ->
+    (forall r, r <> PC -> r <> temp -> rs1 r = rs r) ->
     exists rs',
-    exec_straight (mk2 r1 r2 :: k) rs m k rs' m' /\
-    agree ms' sp rs') ->
-  agree ms sp rs ->
-  map mreg_type args = type_of_addressing addr ->
-  temp <> GPR0 ->
+        exec_straight ge fn (mk2 r1 r2 :: k) rs1 m k rs' m' /\ P rs') ->
   exists rs',
-    exec_straight (transl_load_store mk1 mk2 addr args temp k) rs m
-                        k rs' m'
-  /\ agree ms' sp rs'.
+      exec_straight ge fn c rs m k rs' m' /\ P rs'.
 Proof.
-  intros. destruct addr; simpl in H2; TypeInv; simpl.
+  intros until m'; intros TR ADDR TEMP MK1 MK2. 
+  unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in ADDR; inv ADDR.
   (* Aindexed *)
   case (Int.eq (high_s i) Int.zero).
   (* Aindexed short *)
-  apply H. 
-  simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto with ppcgen.
-  auto.
+  apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
   (* Aindexed long *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add (rs (ireg_of m0)) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
-  exploit (H (Cint (low_s i)) temp rs1 k).
-    simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto. 
-    unfold rs1; repeat SIMP. rewrite Val.add_assoc.
+  set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
+  exploit (MK1 (Cint (low_s i)) temp rs1 k).
+    simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
+    unfold rs1; Simpl. rewrite Val.add_assoc.
 Transparent Val.add.
     simpl. rewrite low_high_s. auto.
-    intros; unfold rs1; repeat SIMP.
+    intros; unfold rs1; Simpl.
   intros [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
-  simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto. 
+  simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. 
   auto. auto.
   (* Aindexed2 *)
-  apply H0. 
-  simpl. UseTypeInfo; auto.
+  apply MK2; auto.
   (* Aglobal *)
-  case_eq (symbol_is_small_data i i0); intro SISD.
+  destruct (symbol_is_small_data i i0) eqn:SISD; inv TR.
   (* Aglobal from small data *)
-  apply H. rewrite gpr_or_zero_zero. simpl const_low. 
-  rewrite small_data_area_addressing; auto. simpl. 
+  apply MK1. simpl. rewrite small_data_area_addressing; auto.
   unfold symbol_address, symbol_offset. 
   destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero. auto.
   auto.
   (* Aglobal general case *)
   set (rs1 := nextinstr (rs#temp <- (const_high ge (Csymbol_high i i0)))).
-  exploit (H (Csymbol_low i i0) temp rs1 k).
-    simpl. rewrite gpr_or_zero_not_zero; auto. 
-    unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
-    unfold const_high, const_low. 
-    set (v := symbol_offset ge i i0).
-    symmetry. rewrite Val.add_commut. unfold v. rewrite low_high_half. auto. 
-    discriminate.
-    intros; unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  exploit (MK1 (Csymbol_low i i0) temp rs1 k).
+    simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
+    unfold rs1. Simpl. 
+    unfold const_high, const_low.
+    rewrite Val.add_commut. rewrite low_high_half. auto.
+    intros; unfold rs1; Simpl.
   intros [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
   unfold exec_instr. rewrite gpr_or_zero_zero. 
@@ -1465,27 +993,24 @@ Transparent Val.add.
   reflexivity. reflexivity.
   assumption. assumption.
   (* Abased *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add (rs (ireg_of m0)) (const_high ge (Csymbol_high i i0))))).
-  exploit (H (Csymbol_low i i0) temp rs1 k).
-    simpl. rewrite gpr_or_zero_not_zero; auto. 
-    unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+  set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (const_high ge (Csymbol_high i i0))))).
+  exploit (MK1 (Csymbol_low i i0) temp rs1 k).
+    simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
+    unfold rs1. Simpl. 
     rewrite Val.add_assoc. 
     unfold const_high, const_low. 
-    set (v := symbol_offset ge i i0).
-    symmetry. rewrite Val.add_commut. decEq. decEq. 
-    unfold v. rewrite Val.add_commut. rewrite low_high_half. auto. 
-    UseTypeInfo. auto. discriminate. 
-    intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+    symmetry. rewrite Val.add_commut. f_equal. f_equal. 
+    rewrite Val.add_commut. rewrite low_high_half. auto.
+    intros; unfold rs1; Simpl.
   intros [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto.
+  unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
   assumption. assumption.
   (* Ainstack *)
-  case (Int.eq (high_s i) Int.zero).
-  apply H. simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. 
-  rewrite (sp_val ms sp rs); auto. auto.
-  set (rs1 := nextinstr (rs#temp <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))).
-  exploit (H (Cint (low_s i)) temp rs1 k).
+  destruct (Int.eq (high_s i) Int.zero); inv TR.
+  apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. 
+  set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s i) (Int.repr 16)))))).
+  exploit (MK1 (Cint (low_s i)) temp rs1 k).
     simpl. rewrite gpr_or_zero_not_zero; auto. 
     unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
     rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
@@ -1493,120 +1018,149 @@ Transparent Val.add.
     intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
   intros [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen.
-  rewrite <- (sp_val ms sp rs); auto. auto.
+  unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
   assumption. assumption.
 Qed.
 
-(** Translation of memory loads. *)
+(** Translation of loads *)
 
 Lemma transl_load_correct:
-  forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
-    chunk addr args k ms sp rs m m' dst a v,
-  (forall cst (r1: ireg) (rs1: regset),
-    exec_instr ge fn (mk1 cst r1) rs1 m' =
-    load1 ge chunk (preg_of dst) cst r1 rs1 m') ->
-  (forall (r1 r2: ireg) (rs1: regset),
-    exec_instr ge fn (mk2 r1 r2) rs1 m' =
-    load2 chunk (preg_of dst) r1 r2 rs1 m') ->
-  agree ms sp rs ->
-  map mreg_type args = type_of_addressing addr ->
-  eval_addressing ge sp addr (map ms args) = Some a ->
+  forall chunk addr args dst k c (rs: regset) m a v,
+  transl_load chunk addr args dst k = OK c ->
+  eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
-  Mem.extends m m' ->
   exists rs',
-    exec_straight (transl_load_store mk1 mk2 addr args GPR12 k) rs m'
-                        k rs' m'
-  /\ agree (Regmap.set dst v (undef_temps ms)) sp rs'.
+     exec_straight ge fn c rs m k rs' m
+  /\ rs'#(preg_of dst) = v
+  /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs' r = rs r.
 Proof.
   intros.
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
-  unfold PregEq.t.
-  intros [a' [A B]]. 
-  exploit Mem.loadv_extends; eauto. intros [v' [C D]].
-  apply transl_load_store_correct with ms; auto.
-(* mk1 *)
-  intros. exists (nextinstr (rs1#(preg_of dst) <- v')). 
-  split. apply exec_straight_one. rewrite H.
-  unfold load1. rewrite A in H6. inv H6. rewrite C. auto. 
-  unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen.
-  apply agree_set_mreg with rs1. 
-  apply agree_undef_temps with rs; auto with ppcgen.
-  repeat SIMP. 
-  intros; repeat SIMP.
-(* mk2 *)
-  intros. exists (nextinstr (rs#(preg_of dst) <- v')). 
-  split. apply exec_straight_one. rewrite H0. 
-  unfold load2. rewrite A in H6. inv H6. rewrite C. auto.
-  unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen.
-  apply agree_set_mreg with rs.
-  apply agree_undef_temps with rs; auto with ppcgen.
-  repeat SIMP. 
-  intros; repeat SIMP.
-(* not GPR0 *)
-  congruence.
-Qed.
-
-(** Translation of memory stores. *)
+  assert (BASE: forall mk1 mk2 k' chunk' v',
+  transl_memory_access mk1 mk2 addr args GPR12 k' = OK c ->
+  Mem.loadv chunk' m a = Some v' ->
+  (forall cst (r1: ireg) (rs1: regset),
+    exec_instr ge fn (mk1 cst r1) rs1 m =
+    load1 ge chunk' (preg_of dst) cst r1 rs1 m) ->
+  (forall (r1 r2: ireg) (rs1: regset),
+    exec_instr ge fn (mk2 r1 r2) rs1 m =
+    load2 chunk' (preg_of dst) r1 r2 rs1 m) ->
+  exists rs',
+     exec_straight ge fn c rs m k' rs' m
+  /\ rs'#(preg_of dst) = v'
+  /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs' r = rs r).
+  {
+  intros. eapply transl_memory_access_correct; eauto. congruence.
+  intros. econstructor; split. apply exec_straight_one. 
+  rewrite H4. unfold load1. rewrite H6. rewrite H3. eauto. 
+  unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen.
+  intuition Simpl.
+  intros. econstructor; split. apply exec_straight_one. 
+  rewrite H5. unfold load2. rewrite H6. rewrite H3. eauto. 
+  unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen.
+  intuition Simpl.
+  }
+  destruct chunk; monadInv H.
+- (* Mint8signed *)
+  assert (exists v1, Mem.loadv Mint8unsigned m a = Some v1 /\ v = Val.sign_ext 8 v1).
+  {
+    destruct a; simpl in *; try discriminate. 
+    rewrite Mem.load_int8_signed_unsigned in H1. 
+    destruct (Mem.load Mint8unsigned m b (Int.unsigned i)); simpl in H1; inv H1.
+    exists v0; auto.
+  }
+  destruct H as [v1 [LD SG]]. clear H1. 
+  exploit BASE; eauto; erewrite ireg_of_eq by eauto; auto.
+  intros [rs1 [A [B C]]].
+  econstructor; split. 
+  eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. 
+  split. Simpl. congruence. intros. Simpl. 
+- (* Mint8unsigned *)
+  eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
+- (* Mint816signed *)
+  eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
+- (* Mint16unsigned *)
+  eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
+- (* Mint32 *)
+  eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
+- (* Mfloat32 *)
+  eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
+- (* Mfloat64 *)
+  apply Mem.loadv_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
+- (* Mfloat64al32 *)
+  eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
+Qed.
+
+(** Translation of stores *)
 
 Lemma transl_store_correct:
-  forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
-    chunk addr args k ms sp rs m src a m' m1,
-  (forall cst (r1: ireg) (rs1 rs2: regset) (m2: mem),
-    store1 ge chunk (preg_of src) cst r1 rs1 m1 = OK rs2 m2 ->
-    exists rs3,
-    exec_instr ge fn (mk1 cst r1) rs1 m1 = OK rs3 m2
-    /\ (forall (r: preg), r <> FPR13 -> rs3 r = rs2 r)) ->
-  (forall (r1 r2: ireg) (rs1 rs2: regset) (m2: mem),
-    store2 chunk (preg_of src) r1 r2 rs1 m1 = OK rs2 m2 ->
-    exists rs3,
-    exec_instr ge fn (mk2 r1 r2) rs1 m1 = OK rs3 m2
-    /\ (forall (r: preg), r <> FPR13 -> rs3 r = rs2 r)) ->
-  agree ms sp rs ->
-  map mreg_type args = type_of_addressing addr ->
-  eval_addressing ge sp addr (map ms args) = Some a ->
-  Mem.storev chunk m a (ms src) = Some m' ->
-  Mem.extends m m1 ->
-  exists m1',
-     Mem.extends m' m1'
-  /\ exists rs',
-       exec_straight (transl_load_store mk1 mk2 addr args (int_temp_for src) k) rs m1
-                     k rs' m1'
-       /\ agree (undef_temps ms) sp rs'.
+  forall chunk addr args src k c (rs: regset) m a m',
+  transl_store chunk addr args src k = OK c ->
+  eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a ->
+  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
+  exists rs',
+     exec_straight ge fn c rs m k rs' m'
+  /\ forall r, r <> PC -> r <> GPR11 -> r <> GPR12 -> r <> FPR13 -> rs' r = rs r.
 Proof.
   intros.
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
-  unfold PregEq.t.
-  intros [a' [A B]].
-  assert (Z: Val.lessdef (ms src) (rs (preg_of src))). eapply preg_val; eauto.
-  exploit Mem.storev_extends; eauto. intros [m1' [C D]].
-  exists m1'; split; auto.
-  apply transl_load_store_correct with ms; auto.
-(* mk1 *)
-  intros.
-  exploit (H cst r1 rs1 (nextinstr rs1) m1').
-  unfold store1. rewrite A in H6. inv H6. 
-  replace (rs1 (preg_of src)) with (rs (preg_of src)).
-  rewrite C. auto.
-  symmetry. apply H7. auto with ppcgen. 
-  apply sym_not_equal. apply int_temp_for_diff.
-  intros [rs3 [U V]].
-  exists rs3; split.
-  apply exec_straight_one. auto. rewrite V; auto with ppcgen. 
-  apply agree_undef_temps with rs. auto. 
-  intros. rewrite V; auto with ppcgen. SIMP. apply H7; auto with ppcgen.
-  unfold int_temp_for. destruct (mreg_eq src IT2); auto with ppcgen.
-(* mk2 *)
-  intros.
-  exploit (H0 r1 r2 rs (nextinstr rs) m1').
-  unfold store2. rewrite A in H6. inv H6. rewrite C. auto. 
-  intros [rs3 [U V]].
-  exists rs3; split.
-  apply exec_straight_one. auto. rewrite V; auto with ppcgen. 
-  eapply agree_undef_temps; eauto. intros. 
-  rewrite V; auto with ppcgen. 
-  unfold int_temp_for. destruct (mreg_eq src IT2); congruence.
-Qed.
-
-End STRAIGHTLINE.
+  assert (TEMP0: int_temp_for src = GPR11 \/ int_temp_for src = GPR12).
+    unfold int_temp_for. destruct (mreg_eq src IT2); auto.
+  assert (TEMP1: int_temp_for src <> GPR0).
+    destruct TEMP0; congruence.
+  assert (TEMP2: IR (int_temp_for src) <> preg_of src).
+    unfold int_temp_for. destruct (mreg_eq src IT2). 
+    subst src; simpl; congruence.
+    change (IR GPR12) with (preg_of IT2). red; intros; elim n. 
+    eapply preg_of_injective; eauto.
+  assert (BASE: forall mk1 mk2 chunk',
+  transl_memory_access mk1 mk2 addr args (int_temp_for src) k = OK c ->
+  Mem.storev chunk' m a (rs (preg_of src)) = Some m' ->
+  (forall cst (r1: ireg) (rs1: regset),
+    exec_instr ge fn (mk1 cst r1) rs1 m =
+    store1 ge chunk' (preg_of src) cst r1 rs1 m) ->
+  (forall (r1 r2: ireg) (rs1: regset),
+    exec_instr ge fn (mk2 r1 r2) rs1 m =
+    store2 chunk' (preg_of src) r1 r2 rs1 m) ->
+  exists rs',
+     exec_straight ge fn c rs m k rs' m'
+  /\ forall r, r <> PC -> r <> GPR11 -> r <> GPR12 -> r <> FPR13 -> rs' r = rs r).
+  {
+  intros. eapply transl_memory_access_correct; eauto.
+  intros. econstructor; split. apply exec_straight_one. 
+  rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. 
+  intros; Simpl. apply H7; auto. destruct TEMP0; congruence. 
+  intros. econstructor; split. apply exec_straight_one. 
+  rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. 
+  intros; Simpl. apply H7; auto. destruct TEMP0; congruence. 
+  }
+  destruct chunk; monadInv H.
+- (* Mint8signed *)
+  assert (Mem.storev Mint8unsigned m a (rs (preg_of src)) = Some m').
+    rewrite <- H1. destruct a; simpl; auto. symmetry. apply Mem.store_signed_unsigned_8.
+  clear H1. eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
+- (* Mint8unsigned *)
+  eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
+- (* Mint16signed *)
+  assert (Mem.storev Mint16unsigned m a (rs (preg_of src)) = Some m').
+    rewrite <- H1. destruct a; simpl; auto. symmetry. apply Mem.store_signed_unsigned_16.
+  clear H1. eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
+- (* Mint16unsigned *)
+  eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
+- (* Mint32 *)
+  eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
+- (* Mfloat32 *)
+  rewrite (freg_of_eq _ _ EQ) in H1.
+  eapply transl_memory_access_correct. eauto. eauto. eauto. 
+  intros. econstructor; split. apply exec_straight_one. 
+  simpl. unfold store1. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. 
+  intros. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence.
+  intros. econstructor; split. apply exec_straight_one. 
+  simpl. unfold store2. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. 
+  intros. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence.
+- (* Mfloat64 *)
+  apply Mem.storev_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
+- (* Mfloat64al32 *)
+  eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
+Qed.
+
+End CONSTRUCTORS.
 
diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v
deleted file mode 100644
index ddbfda6..0000000
--- a/powerpc/Asmgenretaddr.v
+++ /dev/null
@@ -1,204 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Predictor for return addresses in generated PPC code.
-
-    The [return_address_offset] predicate defined here is used in the
-    semantics for Mach (module [Machsem]) to determine the
-    return addresses that are stored in activation records. *)
-
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Op.
-Require Import Locations.
-Require Import Mach.
-Require Import Asm.
-Require Import Asmgen.
-
-(** The ``code tail'' of an instruction list [c] is the list of instructions
-  starting at PC [pos]. *)
-
-Inductive code_tail: Z -> code -> code -> Prop :=
-  | code_tail_0: forall c,
-      code_tail 0 c c
-  | code_tail_S: forall pos i c1 c2,
-      code_tail pos c1 c2 ->
-      code_tail (pos + 1) (i :: c1) c2.
-
-Lemma code_tail_pos:
-  forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
-Proof.
-  induction 1. omega. omega.
-Qed.
-
-(** Consider a Mach function [f] and a sequence [c] of Mach instructions
-  representing the Mach code that remains to be executed after a
-  function call returns.  The predicate [return_address_offset f c ofs]
-  holds if [ofs] is the integer offset of the PPC instruction
-  following the call in the PPC code obtained by translating the
-  code of [f]. Graphically:
-<<
-     Mach function f    |--------- Mcall ---------|
-         Mach code c    |                |--------|
-                        |                 \        \
-                        |                  \        \
-                        |                   \        \
-     PPC code           |                    |--------|
-     PPC function       |--------------- Pbl ---------|
-
-                        <-------- ofs ------->
->>
-*)
-
-Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop :=
-  | return_address_offset_intro:
-      forall c f ofs,
-      code_tail ofs (transl_function f) (transl_code f c) ->
-      return_address_offset f c (Int.repr ofs).
-
-(** We now show that such an offset always exists if the Mach code [c]
-  is a suffix of [f.(fn_code)].  This holds because the translation
-  from Mach to PPC is compositional: each Mach instruction becomes
-  zero, one or several PPC instructions, but the order of instructions
-  is preserved. *)
-
-Lemma is_tail_code_tail:
-  forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1.
-Proof.
-  induction 1. exists 0; constructor.
-  destruct IHis_tail as [ofs CT]. exists (ofs + 1); constructor; auto.
-Qed.
-
-Hint Resolve is_tail_refl: ppcretaddr.
-
-Ltac IsTail :=
-  auto with ppcretaddr;
-  match goal with
-  | [ |- is_tail _ (_ :: _) ] => constructor; IsTail
-  | [ |- is_tail _ (match ?x with true => _ | false => _ end) ] => destruct x; IsTail
-  | [ |- is_tail _ (match ?x with left _ => _ | right _ => _ end) ] => destruct x; IsTail
-  | [ |- is_tail _ (match ?x with nil => _ | _ :: _ => _ end) ] => destruct x; IsTail
-  | [ |- is_tail _ (match ?x with Tint => _ | Tfloat => _ end) ] => destruct x; IsTail
-  | [ |- is_tail _ (?f _ _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
-  | [ |- is_tail _ (?f _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
-  | [ |- is_tail _ (?f _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
-  | [ |- is_tail _ (?f _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
-  | [ |- is_tail _ (?f _ _ ?k) ] => apply is_tail_trans with k; IsTail
-  | _ => idtac
-  end.
-
-Lemma loadimm_tail:
-  forall r n k, is_tail k (loadimm r n k).
-Proof. unfold loadimm; intros; IsTail. Qed.
-Hint Resolve loadimm_tail: ppcretaddr.
-
-Lemma addimm_tail:
-  forall r1 r2 n k, is_tail k (addimm r1 r2 n k).
-Proof. unfold addimm; intros; IsTail. Qed.
-Hint Resolve addimm_tail: ppcretaddr.
-
-Lemma andimm_base_tail:
-  forall r1 r2 n k, is_tail k (andimm_base r1 r2 n k).
-Proof. unfold andimm_base; intros; IsTail. Qed.
-Hint Resolve andimm_base_tail: ppcretaddr.
-
-Lemma andimm_tail:
-  forall r1 r2 n k, is_tail k (andimm r1 r2 n k).
-Proof. unfold andimm; intros; IsTail. Qed.
-Hint Resolve andimm_tail: ppcretaddr.
-
-Lemma orimm_tail:
-  forall r1 r2 n k, is_tail k (orimm r1 r2 n k).
-Proof. unfold orimm; intros; IsTail. Qed.
-Hint Resolve orimm_tail: ppcretaddr.
-
-Lemma xorimm_tail:
-  forall r1 r2 n k, is_tail k (xorimm r1 r2 n k).
-Proof. unfold xorimm; intros; IsTail. Qed.
-Hint Resolve xorimm_tail: ppcretaddr.
-
-Lemma rolm_tail:
-  forall r1 r2 amount mask k, is_tail k (rolm r1 r2 amount mask k).
-Proof. unfold rolm; intros; IsTail. Qed.
-Hint Resolve rolm_tail: ppcretaddr.
-
-Lemma loadind_tail:
-  forall base ofs ty dst k, is_tail k (loadind base ofs ty dst k).
-Proof. unfold loadind; intros. destruct ty; IsTail. Qed.
-Hint Resolve loadind_tail: ppcretaddr.
-
-Lemma storeind_tail:
-  forall src base ofs ty k, is_tail k (storeind src base ofs ty k).
-Proof. unfold storeind; intros. destruct ty; IsTail. Qed.
-Hint Resolve storeind_tail: ppcretaddr.
-
-Lemma floatcomp_tail:
-  forall cmp r1 r2 k, is_tail k (floatcomp cmp r1 r2 k).
-Proof. unfold floatcomp; intros; destruct cmp; IsTail. Qed.
-Hint Resolve floatcomp_tail: ppcretaddr.
-
-Lemma transl_cond_tail:
-  forall cond args k, is_tail k (transl_cond cond args k).
-Proof. unfold transl_cond; intros; destruct cond; IsTail. Qed.
-Hint Resolve transl_cond_tail: ppcretaddr.
-
-Lemma transl_cond_op_tail:
-  forall cond args r k, is_tail k (transl_cond_op cond args r k).
-Proof.
-  unfold transl_cond_op; intros.
-  destruct (classify_condition cond args); IsTail.
-Qed.
-Hint Resolve transl_cond_op_tail: ppcretaddr.
-
-Lemma transl_op_tail:
-  forall op args r k, is_tail k (transl_op op args r k).
-Proof.
-  unfold transl_op; intros; destruct op; IsTail. 
-Qed.
-Hint Resolve transl_op_tail: ppcretaddr.
-
-Lemma transl_load_store_tail:
-  forall mk1 mk2 addr args temp k,
-  is_tail k (transl_load_store mk1 mk2 addr args temp k).
-Proof. unfold transl_load_store; intros; destruct addr; IsTail. Qed.
-Hint Resolve transl_load_store_tail: ppcretaddr.
-
-Lemma transl_instr_tail:
-  forall f i k, is_tail k (transl_instr f i k).
-Proof.
-  unfold transl_instr; intros; destruct i; IsTail.
-  destruct m; IsTail.
-  destruct m; IsTail.
-  destruct s0; IsTail.
-  destruct s0; IsTail.
-Qed.
-Hint Resolve transl_instr_tail: ppcretaddr.
-
-Lemma transl_code_tail: 
-  forall f c1 c2, is_tail c1 c2 -> is_tail (transl_code f c1) (transl_code f c2).
-Proof.
-  induction 1; simpl. constructor. eapply is_tail_trans; eauto with ppcretaddr.
-Qed.
-
-Lemma return_address_exists:
-  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(fn_code) ->
-  exists ra, return_address_offset f c ra.
-Proof.
-  intros. assert (is_tail (transl_code f c) (transl_function f)).
-  unfold transl_function. IsTail. apply transl_code_tail; eauto with coqlib.
-  destruct (is_tail_code_tail _ _ H0) as [ofs A].
-  exists (Int.repr ofs). constructor. auto.
-Qed.
-
- 
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index c9203ec..152a4f7 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -536,7 +536,8 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "%s jumptable [ " comment;
       List.iter (fun l -> fprintf oc "%a " label (transl_label l)) tbl;
       fprintf oc "]\n";
-      fprintf oc "	addis	%a, %a, %a\n" ireg GPR12 ireg r label_high lbl;
+      fprintf oc "	slwi    %a, %a, 2\n" ireg GPR12 ireg r;
+      fprintf oc "	addis	%a, %a, %a\n" ireg GPR12 ireg GPR12 label_high lbl;
       fprintf oc "	lwz	%a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12;
       fprintf oc "	mtctr	%a\n" ireg GPR12;
       fprintf oc "	bctr\n";