Merge of the reuse-temps branch:

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



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

15 files changed, 1080 insertions, 1267 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 9da5871..e49986f 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -159,17 +159,15 @@ Inductive instruction : Type :=
   | Pfadd: freg -> freg -> freg -> instruction                (**r float addition *)
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
   | Pfcti: ireg -> freg -> instruction                        (**r float-to-signed-int conversion *)
-  | Pfctiu: ireg -> freg -> instruction                       (**r float-to-unsigned-int conversion *)
   | Pfdiv: freg -> freg -> freg -> instruction                (**r float division *)
   | Pfmadd: freg -> freg -> freg -> freg -> instruction       (**r float multiply-add *)
+  | Pfmake: freg -> ireg -> ireg -> instruction               (**r build a float from 2 ints *)
   | Pfmr: freg -> freg -> instruction                         (**r float move *)
   | Pfmsub: freg -> freg -> freg -> freg -> instruction       (**r float multiply-sub *)
   | Pfmul: freg -> freg -> freg -> instruction                (**r float multiply *)
   | Pfneg: freg -> freg -> instruction                        (**r float negation *)
   | Pfrsp: freg -> freg -> instruction                        (**r float round to single precision *)
   | Pfsub: freg -> freg -> freg -> instruction                (**r float subtraction *)
-  | Pictf: freg -> ireg -> instruction                        (**r int-to-float conversion *)
-  | Piuctf: freg -> ireg -> instruction                       (**r unsigned int-to-float conversion *)
   | Plbz: ireg -> constant -> ireg -> instruction             (**r load 8-bit unsigned int *)
   | Plbzx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Plfd: freg -> constant -> ireg -> instruction             (**r load 64-bit float *)
@@ -235,72 +233,21 @@ lbl:    .double floatcst
   Initialized data in the constant data section are not modeled here,
   which is why we use a pseudo-instruction for this purpose.
 - [Pfcti]: convert a float to a signed integer.  This requires a transfer
-  via memory of a 32-bit integer from a float register to an int register,
-  which our memory model cannot express.  Expands to:
+  via memory of a 32-bit integer from a float register to an int register.
+  Expands to:
 <<
         fctiwz  f13, rsrc
         stfdu   f13, -8(r1)
         lwz     rdst, 4(r1)
         addi    r1, r1, 8
 >>
-- [Pfctiu]: convert a float to an unsigned integer.  The PowerPC way
-  to do this is to compare the argument against the floating-point
-  constant [2^31], subtract [2^31] if bigger, then convert to a signed
-  integer as above, then add back [2^31] if needed.  Expands to:
+- [Pfmake]: build a double float from two 32-bit integers.  This also
+  requires a transfer via memory.  Expands to:
 <<
-        addis   r12, 0, ha16(lbl1)
-        lfd     f13, lo16(lbl1)(r12)
-        fcmpu   cr7, rsrc, f13
-        cror    30, 29, 30
-        beq     cr7, lbl2
-        fctiwz  f13, rsrc
-        stfdu   f13, -8(r1)
-        lwz     rdst, 4(r1)
-        b       lbl3
-lbl2:   fsub    f13, rsrc, f13
-        fctiwz  f13, f13
-        stfdu   f13, -8(r1)
-        lwz     rdst, 4(r1)
-        addis   rdst, rdst, 0x8000
-lbl3:   addi    r1, r1, 8
-        .const_data
-lbl1:   .long   0x41e00000, 0x00000000    # 2^31 in double precision
-        .text
->>
-- [Pictf]: convert a signed integer to a float.  This requires complicated
-  bit-level manipulations of IEEE floats through mixed float and integer 
-  arithmetic over a memory word, which our memory model and axiomatization
-  of floats cannot express.  Expands to:
-<<
-        addis   r12, 0, 0x4330
-        stwu    r12, -8(r1)
-        addis   r12, rsrc, 0x8000
-        stw     r12, 4(r1)
-        addis   r12, 0, ha16(lbl)
-        lfd     f13, lo16(lbl)(r12)
+        stwu    rsrc1, -8(r1)
+        stw     rsrc2, 4(r1)
         lfd     rdst, 0(r1)
         addi    r1, r1, 8
-        fsub    rdst, rdst, f13
-        .const_data
-lbl:    .long   0x43300000, 0x80000000
-        .text
->>
-  (Don't worry if you do not understand this instruction sequence: intimate
-  knowledge of IEEE float arithmetic is necessary.)
-- [Piuctf]: convert an unsigned integer to a float.  The expansion is close
-  to that [Pictf], and equally obscure.
-<<
-        addis   r12, 0, 0x4330
-        stwu    r12, -8(r1)
-        stw     rsrc, 4(r1)
-        addis   r12, 0, ha16(lbl)
-        lfd     f13, lo16(lbl)(r12)
-        lfd     rdst, 0(r1)
-        addi    r1, r1, 8
-        fsub    rdst, rdst, f13
-        .const_data
-lbl:    .long   0x43300000, 0x00000000
-        .text
 >>
 - [Pallocframe lo hi ofs]: in the formal semantics, this pseudo-instruction
   allocates a memory block with bounds [lo] and [hi], stores the value
@@ -585,7 +532,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       let sp := Vptr stk (Int.repr lo) in
       match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with
       | None => Error
-      | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR12 <- Vundef)) m2
+      | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)) m2
       end
   | Pand_ rd r1 r2 =>
       let v := Val.and rs#r1 rs#r2 in
@@ -621,7 +568,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       | _ => Error
       end
   | Pbtbl r tbl =>
-      match rs#r with
+      match gpr_or_zero rs r with
       | Vint n => 
           let pos := Int.signed n in
           if zeq (Zmod pos 4) 0 then
@@ -672,13 +619,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Pfcmpu r1 r2 =>
       OK (nextinstr (compare_float rs rs#r1 rs#r2)) m
   | Pfcti rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.intoffloat rs#r1) #FPR13 <- Vundef)) m
-  | Pfctiu rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.intuoffloat rs#r1) #FPR13 <- Vundef)) m
+      OK (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.intoffloat rs#r1))) m
   | Pfdiv rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m
   | Pfmadd rd r1 r2 r3 =>
       OK (nextinstr (rs#rd <- (Val.addf (Val.mulf rs#r1 rs#r2) rs#r3))) m
+  | Pfmake rd r1 r2 =>
+      OK (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m
   | Pfmr rd r1 =>
       OK (nextinstr (rs#rd <- (rs#r1))) m
   | Pfmsub rd r1 r2 r3 =>
@@ -691,10 +638,6 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m
   | Pfsub rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m
-  | Pictf rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.floatofint rs#r1) #GPR12 <- Vundef #FPR13 <- Vundef)) m
-  | Piuctf rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.floatofintu rs#r1) #GPR12 <- Vundef #FPR13 <- Vundef)) m
   | Plbz rd cst r1 =>
       load1 Mint8unsigned rd cst r1 rs m
   | Plbzx rd r1 r2 =>
@@ -716,7 +659,7 @@ 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#rd <- (Vfloat f) #GPR12 <- Vundef)) m
+      OK (nextinstr (rs #GPR12 <- Vundef #rd <- (Vfloat f))) m
   | Plwz rd cst r1 =>
       load1 Mint32 rd cst r1 rs m
   | Plwzx rd r1 r2 =>
@@ -766,9 +709,15 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Pstfdx rd r1 r2 =>
       store2 Mfloat64 rd r1 r2 rs m
   | Pstfs rd cst r1 =>
-      store1 Mfloat32 rd cst r1 (rs#FPR13 <- Vundef) m
+      match store1 Mfloat32 rd cst r1 rs m with
+      | OK rs' m' => OK (rs'#FPR13 <- Vundef) m'
+      | Error => Error
+      end
   | Pstfsx rd r1 r2 =>
-      store2 Mfloat32 rd r1 r2 (rs#FPR13 <- Vundef) m
+      match store2 Mfloat32 rd r1 r2 rs m with
+      | OK rs' m' => OK (rs'#FPR13 <- Vundef) m'
+      | Error => Error
+      end
   | Psth rd cst r1 =>
       store1 Mint16unsigned rd cst r1 rs m
   | Psthx rd r1 r2 =>
@@ -801,8 +750,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   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 [GPR12] nor [FPR13].
-  These two registers are reserved as temporaries, to be used
+  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 :=
@@ -814,20 +763,21 @@ Definition ireg_of (r: mreg) : ireg :=
   | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24
   | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28
   | R29 => GPR29 | R30 => GPR30 | R31 => GPR31
-  | IT1 => GPR11 | IT2 => GPR0
-  | _ => GPR0 (* should not happen *)
+  | 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 | F14 => FPR14 | F15 => FPR15
+  | F9 => FPR9  | F10 => FPR10 | F11 => FPR11
+  | F14 => FPR14 | F15 => FPR15
   | F16 => FPR16 | F17 => FPR17 | F18 => FPR18 | F19 => FPR19
   | F20 => FPR20 | F21 => FPR21 | F22 => FPR22 | F23 => FPR23
   | F24 => FPR24 | F25 => FPR25 | F26 => FPR26 | F27 => FPR27
   | F28 => FPR28 | F29 => FPR29 | F30 => FPR30 | F31 => FPR31
-  | FT1 => FPR0 | FT2 => FPR11 | FT3 => FPR12
+  | FT1 => FPR0 | FT2 => FPR12 | FT3 => FPR13
   | _ => FPR0 (* should not happen *)
   end.
 
@@ -886,7 +836,11 @@ Inductive step: state -> trace -> state -> Prop :=
       Genv.find_funct_ptr ge b = Some (Internal c) ->
       find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) ->
       external_call ef ge (map rs args) m t v m' ->
-      step (State rs m) t (State (nextinstr(rs # res <- v)) m')
+      step (State rs m) t
+           (State (nextinstr(rs #GPR11 <- Vundef #GPR12 <- Vundef
+                                #FPR12 <- Vundef #FPR13 <- Vundef
+                                #FPR0 <- Vundef #CTR <- Vundef
+                                #res <- v)) m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
       rs PC = Vptr b Int.zero ->
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index b1b1245..9c37c42 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -60,7 +60,7 @@ Definition loadimm (r: ireg) (n: int) (k: code) :=
     Paddis r GPR0 (Cint (high_u n)) ::
     Pori r r (Cint (low_u n)) :: k.
 
-Definition addimm_1 (r1 r2: ireg) (n: int) (k: code) :=
+Definition addimm (r1 r2: ireg) (n: int) (k: code) :=
   if Int.eq (high_s n) Int.zero then
     Paddi r1 r2 (Cint n) :: k
   else if Int.eq (low_s n) Int.zero then
@@ -69,24 +69,13 @@ Definition addimm_1 (r1 r2: ireg) (n: int) (k: code) :=
     Paddis r1 r2 (Cint (high_s n)) ::
     Paddi r1 r1 (Cint (low_s n)) :: k.
 
-Definition addimm_2 (r1 r2: ireg) (n: int) (k: code) :=
-  loadimm GPR12 n (Padd r1 r2 GPR12 :: k).
-
-Definition addimm (r1 r2: ireg) (n: int) (k: code) :=
-  if ireg_eq r1 GPR0 then
-    addimm_2 r1 r2 n k
-  else if ireg_eq r2 GPR0 then
-    addimm_2 r1 r2 n k
-  else
-    addimm_1 r1 r2 n k.
-
 Definition andimm (r1 r2: ireg) (n: int) (k: code) :=
   if Int.eq (high_u n) Int.zero then
     Pandi_ r1 r2 (Cint n) :: k
   else if Int.eq (low_u n) Int.zero then
     Pandis_ r1 r2 (Cint (high_u n)) :: k
   else
-    loadimm GPR12 n (Pand_ r1 r2 GPR12 :: k).
+    loadimm GPR0 n (Pand_ r1 r2 GPR0 :: k).
 
 Definition orimm (r1 r2: ireg) (n: int) (k: code) :=
   if Int.eq (high_u n) Int.zero then
@@ -106,36 +95,34 @@ Definition xorimm (r1 r2: ireg) (n: int) (k: code) :=
     Pxoris r1 r2 (Cint (high_u n)) ::
     Pxori r1 r1 (Cint (low_u n)) :: k.
 
-(** Smart constructors for indexed loads and stores,
-  where the address is the contents of a register plus
-  an integer literal. *)
-
-Definition loadind_aux (base: ireg) (ofs: int) (ty: typ) (dst: mreg) :=
-  match ty with
-  | Tint => Plwz (ireg_of dst) (Cint ofs) base
-  | Tfloat => Plfd (freg_of dst) (Cint ofs) base
-  end.
+(** 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
-    loadind_aux base ofs ty dst :: k
+    match ty with
+    | Tint => Plwz (ireg_of dst) (Cint ofs) base :: k
+    | Tfloat => Plfd (freg_of dst) (Cint ofs) base :: k
+    end
   else
-    Paddis GPR12 base (Cint (high_s ofs)) ::
-    loadind_aux GPR12 (low_s ofs) ty dst :: k.
-  
-Definition storeind_aux (src: mreg) (base: ireg) (ofs: int) (ty: typ) :=
-  match ty with
-  | Tint => Pstw (ireg_of src) (Cint ofs) base
-  | Tfloat => Pstfd (freg_of src) (Cint ofs) base
-  end.
+    loadimm GPR0 ofs
+      (match ty with
+       | Tint => Plwzx (ireg_of dst) base GPR0 :: k
+       | Tfloat => Plfdx (freg_of dst) 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
-    storeind_aux src base ofs ty :: k
+    match ty with
+    | Tint => Pstw (ireg_of src) (Cint ofs) base :: k
+    | Tfloat => Pstfd (freg_of src) (Cint ofs) base :: k
+    end
   else
-    Paddis GPR12 base (Cint (high_s ofs)) ::
-    storeind_aux src GPR12 (low_s ofs) ty :: k.
-  
+    loadimm GPR0 ofs
+      (match ty with
+       | Tint => Pstwx (ireg_of src) base GPR0 :: k
+       | Tfloat => Pstfdx (freg_of src) base GPR0 :: k
+       end).
+
 (** Constructor for a floating-point comparison.  The PowerPC has
   a single [fcmpu] instruction to compare floats, which sets
   bits 0, 1 and 2 of the condition register to reflect ``less'',
@@ -168,20 +155,20 @@ Definition transl_cond
       if Int.eq (high_s n) Int.zero then
         Pcmpwi (ireg_of a1) (Cint n) :: k
       else
-        loadimm GPR12 n (Pcmpw (ireg_of a1) GPR12 :: k)
+        loadimm GPR0 n (Pcmpw (ireg_of a1) GPR0 :: k)
   | Ccompuimm c n, a1 :: nil =>
       if Int.eq (high_u n) Int.zero then
         Pcmplwi (ireg_of a1) (Cint n) :: k
       else
-        loadimm GPR12 n (Pcmplw (ireg_of a1) GPR12 :: k)
+        loadimm GPR0 n (Pcmplw (ireg_of a1) GPR0 :: k)
   | Ccompf cmp, a1 :: a2 :: nil =>
       floatcomp cmp (freg_of a1) (freg_of a2) k
   | Cnotcompf cmp, a1 :: a2 :: nil =>
       floatcomp cmp (freg_of a1) (freg_of a2) k
   | Cmaskzero n, a1 :: nil =>
-      andimm GPR12 (ireg_of a1) n k
+      andimm GPR0 (ireg_of a1) n k
   | Cmasknotzero n, a1 :: nil =>
-      andimm GPR12 (ireg_of a1) n k
+      andimm GPR0 (ireg_of a1) n k
   | _, _ =>
      k (**r never happens for well-typed code *)
   end.
@@ -287,14 +274,14 @@ Definition transl_op
       if Int.eq (high_s n) Int.zero then
         Psubfic (ireg_of r) (ireg_of a1) (Cint n) :: k
       else
-        loadimm GPR12 n (Psubfc (ireg_of r) (ireg_of a1) GPR12 :: k)
+        loadimm GPR0 n (Psubfc (ireg_of r) (ireg_of a1) GPR0 :: k)
   | Omul, a1 :: a2 :: nil =>
       Pmullw (ireg_of r) (ireg_of a1) (ireg_of a2) :: 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 GPR12 n (Pmullw (ireg_of r) (ireg_of a1) GPR12 :: k)
+        loadimm GPR0 n (Pmullw (ireg_of r) (ireg_of a1) GPR0 :: k)
   | Odiv, a1 :: a2 :: nil =>
       Pdivw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
   | Odivu, a1 :: a2 :: nil =>
@@ -350,12 +337,8 @@ Definition transl_op
       Pfrsp (freg_of r) (freg_of a1) :: k
   | Ointoffloat, a1 :: nil =>
       Pfcti (ireg_of r) (freg_of a1) :: k
-  | Ointuoffloat, a1 :: nil =>
-      Pfctiu (ireg_of r) (freg_of a1) :: k
-  | Ofloatofint, a1 :: nil =>
-      Pictf (freg_of r) (ireg_of a1) :: k
-  | Ofloatofintu, a1 :: nil =>
-      Piuctf (freg_of r) (ireg_of a1) :: k
+  | Ofloatofwords, a1 :: a2 :: nil =>
+      Pfmake (freg_of r) (ireg_of a1) (ireg_of a2) :: k
   | Ocmp cmp, _ =>
       match classify_condition cmp args with
       | condition_ge0 _ a _ =>
@@ -377,43 +360,38 @@ Definition transl_op
 
 (** Common code to translate [Mload] and [Mstore] instructions. *)
 
+Definition int_temp_for (r: mreg) :=
+  if mreg_eq r IT2 then GPR11 else GPR12.
+
 Definition transl_load_store 
      (mk1: constant -> ireg -> instruction)
      (mk2: ireg -> ireg -> instruction)
-     (addr: addressing) (args: list mreg) (k: code) :=
+     (addr: addressing) (args: list mreg) 
+     (temp: ireg) (k: code) :=
   match addr, args with
   | Aindexed ofs, a1 :: nil =>
-      if ireg_eq (ireg_of a1) GPR0 then
-        Pmr GPR12 (ireg_of a1) ::
-        Paddis GPR12 GPR12 (Cint (high_s ofs)) ::
-        mk1 (Cint (low_s ofs)) GPR12 :: k
-      else if Int.eq (high_s ofs) Int.zero then
+      if Int.eq (high_s ofs) Int.zero then
         mk1 (Cint ofs) (ireg_of a1) :: k
       else
-        Paddis GPR12 (ireg_of a1) (Cint (high_s ofs)) ::
-        mk1 (Cint (low_s ofs)) GPR12 :: k
+        Paddis temp (ireg_of a1) (Cint (high_s ofs)) ::
+        mk1 (Cint (low_s ofs)) temp :: k
   | Aindexed2, a1 :: a2 :: nil =>
       mk2 (ireg_of a1) (ireg_of a2) :: k
   | Aglobal symb ofs, nil =>
       if symbol_is_small_data symb ofs then
         mk1 (Csymbol_sda symb ofs) GPR0 :: k
       else
-        Paddis GPR12 GPR0 (Csymbol_high symb ofs) ::
-        mk1 (Csymbol_low symb ofs) GPR12 :: k
+        Paddis temp GPR0 (Csymbol_high symb ofs) ::
+        mk1 (Csymbol_low symb ofs) temp :: k
   | Abased symb ofs, a1 :: nil =>
-      if ireg_eq (ireg_of a1) GPR0 then
-        Pmr GPR12 (ireg_of a1) ::
-        Paddis GPR12 GPR12 (Csymbol_high symb ofs) ::
-        mk1 (Csymbol_low symb ofs) GPR12 :: k
-      else
-        Paddis GPR12 (ireg_of a1) (Csymbol_high symb ofs) ::
-        mk1 (Csymbol_low symb ofs) GPR12 :: k
+      Paddis temp (ireg_of a1) (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 GPR12 GPR1 (Cint (high_s ofs)) ::
-        mk1 (Cint (low_s ofs)) GPR12 :: k
+        Paddis temp GPR1 (Cint (high_s ofs)) ::
+        mk1 (Cint (low_s ofs)) temp :: k
   | _, _ =>
       (* should not happen *) k
   end.
@@ -427,57 +405,58 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
   | Msetstack src ofs ty =>
       storeind src GPR1 ofs ty k
   | Mgetparam ofs ty dst =>
-      Plwz GPR12 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR12 ofs ty dst k
+      Plwz GPR11 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR11 ofs ty dst k
   | Mop op args res =>
       transl_op op args res k
   | Mload chunk addr args dst =>
       match chunk with
       | Mint8signed =>
           transl_load_store
-            (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args
+            (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 k
+            (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 k
+            (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 k
+            (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 k
+            (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 k
+            (Plfs (freg_of dst)) (Plfsx (freg_of dst)) addr args GPR12 k
       | Mfloat64 =>
           transl_load_store
-            (Plfd (freg_of dst)) (Plfdx (freg_of dst)) addr args k
+            (Plfd (freg_of dst)) (Plfdx (freg_of dst)) addr args GPR12 k
       end
   | 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 k
+            (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 k
+            (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 k
+            (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 k
+            (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 k
+            (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 k
+            (Pstfs (freg_of src)) (Pstfsx (freg_of src)) addr args temp k
       | Mfloat64 =>
           transl_load_store
-            (Pstfd (freg_of src)) (Pstfdx (freg_of src)) addr args k
+            (Pstfd (freg_of src)) (Pstfdx (freg_of src)) addr args temp k
       end
   | Mcall sig (inl r) =>
       Pmtctr (ireg_of r) :: Pbctrl :: k
@@ -485,13 +464,13 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pbl symb :: k
   | Mtailcall sig (inl r) =>
       Pmtctr (ireg_of r) :: 
-      Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
-      Pmtlr GPR12 ::
+      Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+      Pmtlr GPR0 ::
       Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: 
       Pbctr :: k
   | Mtailcall sig (inr symb) =>
-      Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
-      Pmtlr GPR12 ::
+      Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+      Pmtlr GPR0 ::
       Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: 
       Pbs symb :: k
   | Mbuiltin ef args res =>
@@ -508,8 +487,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) ::
       Pbtbl GPR12 tbl :: k
   | Mreturn =>
-      Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
-      Pmtlr GPR12 ::
+      Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+      Pmtlr GPR0 ::
       Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) ::
       Pblr :: k
   end.
@@ -524,8 +503,8 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
 
 Definition transl_function (f: Mach.function) :=
   Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) ::
-  Pmflr GPR12 ::
-  Pstw GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+  Pmflr GPR0 ::
+  Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
   transl_code f f.(fn_code).
 
 Open Local Scope string_scope.
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index fc14830..65c831e 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -342,25 +342,12 @@ Proof.
 Qed.
 Hint Rewrite loadimm_label: labels.
 
-Remark addimm_1_label:
-  forall r1 r2 n k, find_label lbl (addimm_1 r1 r2 n k) = find_label lbl k.
-Proof.
-  intros; unfold addimm_1. 
-  case (Int.eq (high_s n) Int.zero). reflexivity.
-  case (Int.eq (low_s n) Int.zero). reflexivity. reflexivity.
-Qed.
-Remark addimm_2_label:
-  forall r1 r2 n k, find_label lbl (addimm_2 r1 r2 n k) = find_label lbl k.
-Proof.
-  intros; unfold addimm_2. autorewrite with labels. reflexivity.
-Qed.
 Remark addimm_label:
   forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k.
 Proof.
   intros; unfold addimm. 
-  case (ireg_eq r1 GPR0); intro. apply addimm_2_label.
-  case (ireg_eq r2 GPR0); intro. apply addimm_2_label.
-  apply addimm_1_label.
+  case (Int.eq (high_s n) Int.zero). reflexivity.
+  case (Int.eq (low_s n) Int.zero). reflexivity. reflexivity.
 Qed.
 Hint Rewrite addimm_label: labels.
 
@@ -392,36 +379,22 @@ Proof.
 Qed.
 Hint Rewrite xorimm_label: labels.
 
-Remark loadind_aux_label:
-  forall base ofs ty dst k, find_label lbl (loadind_aux base ofs ty dst :: k) = find_label lbl k.
-Proof.
-  intros; unfold loadind_aux.
-  case ty; reflexivity.
-Qed.
 Remark loadind_label:
   forall base ofs ty dst k, find_label lbl (loadind base ofs ty dst k) = find_label lbl k.
 Proof.
   intros; unfold loadind. 
-  case (Int.eq (high_s ofs) Int.zero). apply loadind_aux_label.
-  transitivity (find_label lbl (loadind_aux GPR12 (low_s ofs) ty dst :: k)).
-  reflexivity. apply loadind_aux_label.
+  destruct (Int.eq (high_s ofs) Int.zero); destruct ty; autorewrite with labels; auto.
 Qed.
 Hint Rewrite loadind_label: labels.
-Remark storeind_aux_label:
-  forall base ofs ty dst k, find_label lbl (storeind_aux base ofs ty dst :: k) = find_label lbl k.
-Proof.
-  intros; unfold storeind_aux.
-  case dst; reflexivity.
-Qed.
+
 Remark storeind_label:
   forall base ofs ty src k, find_label lbl (storeind base src ofs ty k) = find_label lbl k.
 Proof.
-  intros; unfold storeind. 
-  case (Int.eq (high_s ofs) Int.zero). apply storeind_aux_label.
-  transitivity (find_label lbl (storeind_aux base GPR12 (low_s ofs) ty :: k)).
-  reflexivity. apply storeind_aux_label.
+  intros; unfold storeind.
+  destruct (Int.eq (high_s ofs) Int.zero); destruct ty; 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.
@@ -481,22 +454,19 @@ Hint Rewrite transl_op_label: labels.
 
 Remark transl_load_store_label:
   forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
-         addr args k,
+         addr args temp k,
   (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 k) = find_label lbl k.
+  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.
-  case (ireg_eq (ireg_of m) GPR0); intro.
-  simpl. rewrite H. auto. 
-  case (Int.eq (high_s i) Int.zero). simpl; rewrite H; auto.
-  simpl; rewrite H; auto.
+  destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto.
   simpl; rewrite H0; auto.
   destruct (symbol_is_small_data i i0); simpl; rewrite H; auto.
-  case (ireg_eq (ireg_of m) GPR0); intro; simpl; rewrite H; auto. 
-  case (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto.
+  simpl; rewrite H; auto.
+  destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto.
 Qed.
 Hint Rewrite transl_load_store_label: labels.
 
@@ -593,56 +563,102 @@ Inductive match_stack: list Machconcr.stackframe -> Prop :=
       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: Machconcr.state -> Asm.state -> Prop :=
   | match_states_intro:
-      forall s fb sp c ms m rs f
+      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),
+        (AG: agree ms sp rs)
+        (MEXT: Mem.extends m m'),
       match_states (Machconcr.State s fb sp c ms m)
-                   (Asm.State rs m)
+                   (Asm.State rs m')
   | match_states_call:
-      forall s fb ms m rs
+      forall s fb ms m rs m'
         (STACKS: match_stack s)
         (AG: agree ms (parent_sp s) rs)
+        (MEXT: Mem.extends m m')
         (ATPC: rs PC = Vptr fb Int.zero)
         (ATLR: rs LR = parent_ra s),
       match_states (Machconcr.Callstate s fb ms m)
-                   (Asm.State rs m)
+                   (Asm.State rs m')
   | match_states_return:
-      forall s ms m rs
+      forall s ms m rs m'
         (STACKS: match_stack s)
         (AG: agree ms (parent_sp s) rs)
+        (MEXT: Mem.extends m m')
         (ATPC: rs PC = parent_ra s),
       match_states (Machconcr.Returnstate s ms m)
-                   (Asm.State rs m).
+                   (Asm.State rs m').
 
 Lemma exec_straight_steps:
-  forall s fb sp m1 f c1 rs1 c2 m2 ms2,
+  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
+     exec_straight tge (transl_function f) (transl_code f c1) rs1 m1' (transl_code f c2) rs2 m2'
      /\ agree ms2 sp rs2) ->
+  Mem.extends m2 m2' ->
   exists st',
-  plus step tge (State rs1 m1) E0 st' /\
+  plus step tge (State rs1 m1') E0 st' /\
   match_states (Machconcr.State s fb sp c2 ms2 m2) st'.
 Proof.
   intros. destruct H4 as [rs2 [A B]].
-  exists (State rs2 m2); split.
+  exists (State rs2 m2'); split.
   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) ->
+  exists st',
+  plus step tge (State rs1 m1') E0 st' /\
+  match_states (Machconcr.State s fb sp c2 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.
+Qed.
+
 (** We need to show that, in the simulation diagram, we cannot
   take infinitely many Mach transitions that correspond to zero
   transitions on the PPC side.  Actually, all Mach transitions
@@ -694,18 +710,18 @@ Proof.
   unfold load_stack in H. 
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inversion WTI.
-  rewrite (sp_val _ _ _ AG) in H.
-  assert (NOTE: GPR1 <> GPR0). congruence.
-  generalize (loadind_correct tge (transl_function f) GPR1 ofs ty
-                dst (transl_code f c) rs m v H H1 NOTE).
+  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_exten_2 with (rs#(preg_of dst) <- v).
+  apply agree_exten_2 with (rs#(preg_of dst) <- v').
   auto with ppcgen. 
-  intros. case (preg_eq r0 (preg_of dst)); intro.
-  subst r0. rewrite Pregmap.gss. auto. 
-  rewrite Pregmap.gso; auto.
+  intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of dst)).
+  subst r0. auto.
+  apply OTH; auto.
 Qed.
 
 Lemma exec_Msetstack_prop:
@@ -719,12 +735,14 @@ Proof.
   intros; red; intros; inv MS.
   unfold store_stack in H. 
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inversion WTI.
-  rewrite (sp_val _ _ _ AG) in H.
-  rewrite (preg_val ms sp rs) in H; auto.
-  assert (NOTE: GPR1 <> GPR0). congruence.
-  generalize (storeind_correct tge (transl_function f) GPR1 ofs ty
-                src (transl_code f c) rs m m' H H1 NOTE).
+  intro WTI. inv WTI.
+  generalize (preg_val ms sp rs src AG). intro. 
+  exploit Mem.storev_extends; eauto.
+  intros [m2' [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.
@@ -739,34 +757,35 @@ Lemma exec_Mgetparam_prop:
   load_stack m sp Tint f.(fn_link_ofs) = Some parent ->
   load_stack m parent ty ofs = Some v ->
   exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set dst v ms) m).
+                  (Machconcr.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.
-  set (rs2 := nextinstr (rs#GPR12 <- parent)).
-  assert (EX1: exec_straight tge (transl_function f)
-                 (transl_code f (Mgetparam ofs ty dst :: c)) rs m
-                 (loadind GPR12 ofs ty dst (transl_code f c)) rs2 m).
-  simpl. apply exec_straight_one.
-  simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto with ppcgen.
-  unfold const_low. rewrite <- (sp_val ms sp rs); auto.
-  unfold load_stack in H0. simpl chunk_of_type in H0. 
-  rewrite H0. reflexivity. reflexivity.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inversion WTI.
-  unfold load_stack in H1. change parent with rs2#GPR12 in H1.
-  assert (NOTE: GPR12 <> GPR0). congruence.
-  generalize (loadind_correct tge (transl_function f) GPR12 ofs ty
-                dst (transl_code f c) rs2 m v H1 H3 NOTE).
-  intros [rs3 [EX2 [RES OTH]]].
-  left; eapply exec_straight_steps; eauto with coqlib.
-  exists rs3; split; simpl.
-  eapply exec_straight_trans; eauto.
-  apply agree_exten_2 with (rs2#(preg_of dst) <- v).
-  unfold rs2; auto with ppcgen.
-  intros. case (preg_eq r0 (preg_of dst)); intro.
-  subst r0. rewrite Pregmap.gss. auto. 
-  rewrite Pregmap.gso; auto. 
+  intro WTI. inv WTI.
+  unfold load_stack in *. simpl in H0. 
+  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.
+  assert (agree (Regmap.set IT1 Vundef ms) sp rs1).
+  unfold rs1. eauto with ppcgen.
+  apply agree_exten_2 with (rs1#(preg_of dst) <- v').
+  auto with ppcgen. 
+  intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of dst)). 
+  congruence. auto. 
 Qed.
 
 Lemma exec_Mop_prop:
@@ -775,7 +794,7 @@ Lemma exec_Mop_prop:
          (ms : mreg -> val) (m : mem) (v : val),
   eval_operation ge sp op ms ## args = Some v ->
   exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set res v ms) m).
+                  (Machconcr.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 _ _))).
@@ -805,7 +824,7 @@ Lemma exec_Mload_prop:
   eval_addressing ge sp addr ms ## args = Some a ->
   Mem.loadv chunk m a = Some v ->
   exec_instr_prop (Machconcr.State s fb sp (Mload chunk addr args dst :: c) ms m)
-               E0 (Machconcr.State s fb sp c (Regmap.set dst v ms) m).
+               E0 (Machconcr.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 _ _))).
@@ -820,26 +839,22 @@ Proof.
   (* 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).
+    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. 
-  generalize (transl_load_correct tge (transl_function f)
-                (Plbz (ireg_of dst)) (Plbzx (ireg_of dst))
-                Mint8unsigned addr args 
-                (Pextsb (ireg_of dst) (ireg_of dst) :: transl_code f c) 
-                ms sp rs m dst a v'
-                X1 X2 AG H3 H7 LOAD).
+    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]].
-  exists (nextinstr (rs2#(ireg_of dst) <- v)).
-  split. eapply exec_straight_trans. eexact EX1.
-  apply exec_straight_one. simpl. 
-  rewrite <- (ireg_val _ _ _ dst AG1);auto. rewrite Regmap.gss. 
-  rewrite EQ. reflexivity. reflexivity. 
-  eauto with ppcgen.
+  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.
 Qed.
 
 Lemma storev_8_signed_unsigned:
@@ -866,20 +881,20 @@ Lemma exec_Mstore_prop:
   eval_addressing ge sp addr ms ## args = Some a ->
   Mem.storev chunk m a (ms src) = Some m' ->
   exec_instr_prop (Machconcr.State s fb sp (Mstore chunk addr args src :: c) ms m) E0
-                  (Machconcr.State s fb sp c ms m').
+                  (Machconcr.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.
+  intro WTI; inv WTI.
   rewrite <- (eval_addressing_preserved _ _ symbols_preserved) in H.
-  left; eapply exec_straight_steps; eauto with coqlib. 
+  left; eapply exec_straight_steps_bis; eauto with coqlib.
   destruct chunk; simpl; simpl in H6;
   try (rewrite storev_8_signed_unsigned in H0);
   try (rewrite storev_16_signed_unsigned in H0);
   simpl; eapply transl_store_correct; eauto;
-  intros; (econstructor; split; [unfold preg_of; rewrite H6; reflexivity | auto]).
-  intros. apply Pregmap.gso; auto. 
-  intros. apply Pregmap.gso; auto.
+  (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.
 
 Lemma exec_Mcall_prop:
@@ -904,12 +919,15 @@ Proof.
   (* Indirect call *)
   generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1.
   generalize (code_tail_next_int _ _ _ _ NOOV CT1). intro CT2.
-  set (rs2 := nextinstr (rs#CTR <- (ms m0))).
-  set (rs3 := rs2 #LR <- (Val.add rs2#PC Vone) #PC <- (ms m0)).
-  assert (ATPC: rs3 PC = Vptr f' Int.zero).
-    change (rs3 PC) with (ms m0). 
-    destruct (ms m0); try discriminate.
+  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).
@@ -918,11 +936,11 @@ Proof.
     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. 
+  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 <- (ireg_val ms sp rs); auto. 
+    simpl. rewrite P2. auto.
   apply star_one. econstructor.
     change (rs2 PC) with (Val.add (rs PC) Vone). rewrite <- H5.
     simpl. auto.
@@ -933,6 +951,8 @@ Proof.
   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)).
@@ -947,7 +967,7 @@ Proof.
     rewrite <- H5. reflexivity. 
   assert (AG2: agree ms sp rs2). 
     unfold rs2; auto 8 with ppcgen.
-  left; exists (State rs2 m); split.
+  left; exists (State rs2 m'); split.
   apply plus_one. econstructor. 
     eauto.
     apply functions_transl. eexact H0. 
@@ -956,6 +976,7 @@ Proof.
   econstructor; eauto with coqlib.
   econstructor; eauto with coqlib.
   rewrite RA_EQ. econstructor; eauto.
+  eapply agree_sp_def; eauto. congruence.
 Qed.
 
 Lemma exec_Mtailcall_prop:
@@ -978,30 +999,43 @@ Proof.
   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 *)
-  set (rs2 := nextinstr (rs#CTR <- (ms m0))).
-  set (rs3 := nextinstr (rs2#GPR12 <- (parent_ra s))).
+  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))).
   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 
-            (Pbctr :: transl_code f c) rs5 m').
-  simpl. apply exec_straight_step with rs2 m. 
-  simpl. rewrite <- (ireg_val _ _ _ _ AG H7). reflexivity. reflexivity.
-  apply exec_straight_step with rs3 m.
+            (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.
+  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. unfold load_stack in H2. simpl in H2. rewrite H2.
-  reflexivity. discriminate. reflexivity.
-  apply exec_straight_step with rs4 m.
+  simpl. rewrite LOAD2. 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).
-  unfold load_stack in H1; simpl in H1. 
-  simpl. rewrite H1. rewrite H3. reflexivity. reflexivity.
-  left; exists (State rs6 m'); split.
+  simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity.
+  left; exists (State rs6 m2'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   econstructor.
@@ -1017,32 +1051,27 @@ Proof.
     unfold rs4, rs3, rs2; auto 10 with ppcgen.
   assert (AG5: agree ms (parent_sp s) rs5).
     unfold rs5. apply agree_nextinstr.
-    split. reflexivity. intros. inv AG4. rewrite H13. 
-    rewrite Pregmap.gso; auto with ppcgen.
+    split. reflexivity. apply parent_sp_def; auto. 
+    intros. inv AG4. rewrite Pregmap.gso; auto with ppcgen.
   unfold rs6; auto with ppcgen.
-  change (rs6 PC) with (ms m0). 
-  generalize H. destruct (ms m0); try congruence.
-  predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence.
   (* direct call *)
-  set (rs2 := nextinstr (rs#GPR12 <- (parent_ra s))).
+  set (rs2 := nextinstr (rs#GPR0 <- (parent_ra s))).
   set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
   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 
-            (Pbs i :: transl_code f c) rs4 m').
-  simpl. apply exec_straight_step with rs2 m. 
+            (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. 
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
   rewrite <- (sp_val _ _ _ AG). 
-  simpl. unfold load_stack in H2. simpl in H2. rewrite H2.
-  reflexivity. discriminate. reflexivity.
-  apply exec_straight_step with rs3 m.
+  simpl. rewrite LOAD2. auto. discriminate. 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).
-  unfold load_stack in H1; simpl in H1.
-  simpl. rewrite H1. rewrite H3. reflexivity. reflexivity.
-  left; exists (State rs5 m'); split.
+  simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity.
+  left; exists (State rs5 m2'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   econstructor.
@@ -1059,8 +1088,9 @@ Proof.
     unfold rs3, rs2; auto 10 with ppcgen.
   assert (AG4: agree ms (parent_sp s) rs4).
     unfold rs4. apply agree_nextinstr.
-    split. reflexivity. intros. inv AG3. rewrite H13. 
-    rewrite Pregmap.gso; auto with ppcgen.
+    split. reflexivity. 
+    apply parent_sp_def; auto.
+    intros. inv AG3. rewrite Pregmap.gso; auto with ppcgen.
   unfold rs5; auto with ppcgen.
 Qed.
 
@@ -1071,7 +1101,7 @@ Lemma exec_Mbuiltin_prop:
          (t : trace) (v : val) (m' : mem),
   external_call ef ge ms ## args m t v m' ->
   exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t
-                  (Machconcr.State s f sp b (Regmap.set res v ms) m').
+                  (Machconcr.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 _ _))).
@@ -1079,20 +1109,21 @@ Proof.
   inv AT. simpl in H3.
   generalize (functions_transl _ _ FIND); intro FN.
   generalize (functions_transl_no_overflow _ _ FIND); 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. 
   eapply exec_step_builtin. eauto. eauto.
-  eapply find_instr_tail; eauto. 
-  replace (rs##(preg_of##args)) with (ms##args).
+  eapply find_instr_tail; eauto.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
-  rewrite list_map_compose. apply list_map_exten. intros. 
-  symmetry. eapply preg_val; eauto. 
   econstructor; eauto with coqlib.
-  unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso.
+  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. 
-  auto with ppcgen.
+  apply sym_not_equal. auto with ppcgen.
+  apply agree_nextinstr. apply agree_set_mreg; auto. 
+  eapply agree_undef_temps; eauto. 
+  intros. repeat rewrite Pregmap.gso; auto. 
 Qed.
 
 Lemma exec_Mgoto_prop:
@@ -1107,9 +1138,9 @@ 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).
+  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.
+  left; exists (State rs2 m'); split.
   apply plus_one. econstructor; eauto.
   apply functions_transl; eauto.
   eapply find_instr_tail; eauto.
@@ -1128,7 +1159,7 @@ Lemma exec_Mcond_true_prop:
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
   exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c' ms m).
+                  (Machconcr.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 _ _))).
@@ -1138,16 +1169,16 @@ Proof.
          then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c
          else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c).
   generalize (transl_cond_correct tge (transl_function f)
-                cond args k1 ms sp rs m true H3 AG H).
+                cond args k1 ms sp rs m' true H3 AG H).
   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).
+  generalize (find_label_goto_label f lbl rs2 m' _ _ _ FIND PC2 H1).
   intros [rs3 [GOTO [AT3 INV3]]].
-  left; exists (State rs3 m); split.
+  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.
@@ -1160,7 +1191,7 @@ Proof.
   traceEq.
   econstructor; eauto. 
   eapply Mach.find_label_incl; eauto.
-  apply agree_exten_2 with rs2; auto. 
+  apply agree_exten_2 with rs2; auto with ppcgen. 
 Qed.
 
 Lemma exec_Mcond_false_prop:
@@ -1169,7 +1200,7 @@ Lemma exec_Mcond_false_prop:
          (c : list Mach.instruction) (ms : mreg -> val) (m : mem),
   eval_condition cond ms ## args = Some false ->
   exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c ms m).
+                  (Machconcr.State s fb sp c (undef_temps ms) m).
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -1179,7 +1210,7 @@ Proof.
          then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c
          else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c).
   generalize (transl_cond_correct tge (transl_function f)
-                cond args k1 ms sp rs m false H1 AG H).
+                cond args k1 ms sp rs m' false H1 AG H).
   simpl. intros [rs2 [EX [RES AG2]]].
   left; eapply exec_straight_steps; eauto with coqlib.
   exists (nextinstr rs2); split.
@@ -1205,7 +1236,7 @@ Lemma exec_Mjumptable_prop:
   Mach.find_label lbl (fn_code f) = Some c' ->
   exec_instr_prop
     (Machconcr.State s fb sp (Mjumptable arg tbl :: c) rs m) E0
-    (Machconcr.State s fb sp c' rs m).
+    (Machconcr.State s fb sp c' (undef_temps rs) m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -1227,17 +1258,18 @@ Proof.
   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).
+            (Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: k1) rs0 m'
+            k1 rs1 m').
    apply exec_straight_one. 
-   simpl. rewrite <- (ireg_val _ _ _ _ AG H5). rewrite H. reflexivity. reflexivity. 
+   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).
+  generalize (find_label_goto_label f lbl rs2 m' _ _ _ FIND PC2 H2).
   intros [rs3 [GOTO [AT3 INV3]]].
-  left; exists (State rs3 m); split.
+  left; exists (State rs3 m'); split.
   eapply plus_right'. 
   eapply exec_straight_steps_1; eauto.
   econstructor; eauto. 
@@ -1251,7 +1283,10 @@ Opaque Zmod.  Opaque Zdiv.
   econstructor; eauto. 
   eapply Mach.find_label_incl; eauto.
   apply agree_exten_2 with rs2; auto. 
-  unfold rs2, rs1. repeat apply agree_set_other; auto with ppcgen.
+  unfold rs2, rs1. apply agree_set_other; auto with ppcgen.
+  apply agree_undef_temps with rs0; auto.
+  intros. rewrite Pregmap.gso; auto. rewrite nextinstr_inv; auto.
+  rewrite Pregmap.gso; auto. 
 Qed.
 
 Lemma exec_Mreturn_prop:
@@ -1266,27 +1301,33 @@ Lemma exec_Mreturn_prop:
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
-  set (rs2 := nextinstr (rs#GPR12 <- (parent_ra s))).
+  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))).
   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 
-            (Pblr :: transl_code f c) rs4 m').
-  simpl. apply exec_straight_three with rs2 m rs3 m.
+            (transl_code f (Mreturn :: c)) rs m'0 
+            (Pblr :: transl_code f c) 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.
-  unfold load_stack in H1. simpl in H1. 
-  rewrite <- (sp_val _ _ _ AG). simpl. rewrite H1.
+  rewrite <- (sp_val _ _ _ AG). simpl. rewrite LOAD2. 
   reflexivity. discriminate.
-  unfold rs3. change (parent_ra s) with rs2#GPR12. reflexivity.
+  unfold rs3. reflexivity.
   simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
-  simpl. 
-  unfold load_stack in H0. simpl in H0.
-  rewrite H0. rewrite H2. reflexivity.
+  simpl. rewrite LOAD1. rewrite FREE'. reflexivity.
   reflexivity. reflexivity. reflexivity.
-  left; exists (State rs5 m'); split.
+  left; exists (State rs5 m2'); split.
   (* execution *)
-  apply plus_right' with E0 (State rs4 m') E0.
+  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). 
@@ -1303,7 +1344,7 @@ Proof.
   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. intros. unfold 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.
@@ -1328,23 +1369,29 @@ Proof.
     inversion TY; auto.
   exploit functions_transl; eauto. intro TFIND.
   generalize (functions_transl_no_overflow _ _ H); intro NOOV.
-  set (rs2 := nextinstr (rs#GPR1 <- sp #GPR12 <- Vundef)).
-  set (rs3 := nextinstr (rs2#GPR12 <- (parent_ra s))).
+  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).
   (* Execution of function prologue *)
   assert (EXEC_PROLOGUE:
             exec_straight tge (transl_function f)
-              (transl_function f) rs m
-              (transl_code f (fn_code f)) rs4 m3).
+              (transl_function f) rs m'
+              (transl_code f (fn_code f)) rs4 m3').
   unfold transl_function at 2. 
-  apply exec_straight_three with rs2 m2 rs3 m2.
-  unfold exec_instr. rewrite H0. fold sp.
-  unfold store_stack in H1. simpl chunk_of_type in H1. 
-  rewrite <- (sp_val _ _ _ AG). rewrite H1. reflexivity.
+  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.
   simpl. unfold store1. rewrite gpr_or_zero_not_zero. 
-  unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR12) with (parent_ra s).
-  unfold store_stack in H2. simpl chunk_of_type in H2. rewrite H2. reflexivity.
+  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)).
@@ -1356,13 +1403,13 @@ Proof.
     change (Int.unsigned Int.zero) with 0. 
     unfold transl_function. constructor.
   assert (AG2: agree ms sp rs2).
-    split. reflexivity. 
+    split. reflexivity. unfold sp. congruence. 
     intros. unfold rs2. rewrite nextinstr_inv. 
     repeat (rewrite Pregmap.gso). elim AG; auto.
     auto with ppcgen. auto with ppcgen. auto with ppcgen.
   assert (AG4: agree ms sp rs4).
     unfold rs4, rs3; auto with ppcgen.
-  left; exists (State rs4 m3); split.
+  left; exists (State rs4 m3'); split.
   (* execution *)
   eapply exec_straight_steps_1; eauto.
   change (Int.unsigned Int.zero) with 0. constructor.
@@ -1384,12 +1431,15 @@ Proof.
   intros; red; intros; inv MS.
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B. 
-  left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs LR))
-                m'); split.
+  exploit extcall_arguments_match; eauto. 
+  intros [args' [C D]].
+  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.
   apply plus_one. eapply exec_step_external; eauto. 
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
-  eapply extcall_arguments_match; eauto. 
   econstructor; eauto.
   unfold loc_external_result. auto with ppcgen.
 Qed.
@@ -1440,7 +1490,9 @@ Proof.
   replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero)
      with (Vptr fb Int.zero).
   econstructor; eauto. constructor.
-  split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen.
+  split. auto. simpl. congruence.
+  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
+  apply Mem.extends_refl.
   unfold symbol_offset. 
   rewrite (transform_partial_program_main _ _ TRANSF). 
   rewrite symbols_preserved. unfold ge; rewrite H1. auto.
@@ -1451,8 +1503,8 @@ Lemma transf_final_states:
   match_states st1 st2 -> Machconcr.final_state st1 r -> Asm.final_state st2 r.
 Proof.
   intros. inv H0. inv H. constructor. auto. 
-  compute in H1. 
-  rewrite (ireg_val _ _ _ R3 AG) in H1. auto. auto.
+  compute in H1.
+  exploit (ireg_val _ _ _ R3 AG). auto. rewrite H1; intro. inv H. auto.
 Qed.
 
 Theorem transf_program_correct:
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 0b146da..d428543 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -117,8 +117,7 @@ Qed.
 
 Definition is_data_reg (r: preg) : Prop :=
   match r with
-  | IR GPR12 => False
-  | FR FPR13 => False
+  | IR GPR0 => False
   | PC => False    | LR => False    | CTR => False
   | CR0_0 => False | CR0_1 => False | CR0_2 => False | CR0_3 => False
   | CARRY => False
@@ -148,17 +147,12 @@ Lemma ireg_of_not_GPR1:
 Proof.
   intro. case r; discriminate.
 Qed.
-Lemma ireg_of_not_GPR12:
-  forall r, ireg_of r <> GPR12.
+Lemma ireg_of_not_GPR0:
+  forall r, ireg_of r <> GPR0.
 Proof.
   intro. case r; discriminate.
 Qed.
-Lemma freg_of_not_FPR13:
-  forall r, freg_of r <> FPR13.
-Proof.
-  intro. case r; discriminate.
-Qed.
-Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR12 freg_of_not_FPR13: ppcgen.
+Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR0: ppcgen.
 
 Lemma preg_of_not:
   forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2.
@@ -174,36 +168,57 @@ Proof.
 Qed.
 Hint Resolve 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. *)
 
-Definition agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) :=
-  rs#GPR1 = sp /\ forall r: mreg, ms r = rs#(preg_of r).
+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 -> ms r = rs#(preg_of r).
+  agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r).
 Proof.
-  intros. elim H. auto.
+  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 ->
-  ms r = rs#(ireg_of r).
+  Val.lessdef (ms r) rs#(ireg_of r).
 Proof.
-  intros. elim H; intros.
-  generalize (H2 r). unfold preg_of. rewrite H0. auto.
+  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 ->
-  ms r = rs#(freg_of r).
+  Val.lessdef (ms r) rs#(freg_of r).
 Proof.
-  intros. elim H; intros.
-  generalize (H2 r). unfold preg_of. rewrite H0. auto.
+  intros. replace (FR (freg_of r)) with (preg_of r). eapply preg_val; eauto. 
+  unfold preg_of. rewrite H0. auto.
 Qed.
 
 Lemma sp_val:
@@ -220,8 +235,9 @@ Lemma agree_exten_1:
   (forall r, is_data_reg r -> rs'#r = rs#r) ->
   agree ms sp rs'.
 Proof.
-  unfold agree; intros. elim H; intros.
-  split. rewrite H0. auto. exact I. 
+  intros. inv H. constructor.
+  apply H0. exact I.
+  auto.
   intros. rewrite H0. auto. apply preg_of_is_data_reg.
 Qed.
 
@@ -229,7 +245,7 @@ Lemma agree_exten_2:
   forall ms sp rs rs',
   agree ms sp rs ->
   (forall r,
-     r <> IR GPR12 -> r <> FR FPR13 ->
+     r <> IR GPR0 ->
      r <> PC -> r <> LR -> r <> CTR ->
      r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 ->
      r <> CARRY ->
@@ -243,12 +259,14 @@ Qed.
 (** Preservation of register agreement under various assignments. *)
 
 Lemma agree_set_mreg:
-  forall ms sp rs r v,
+  forall ms sp rs r v v',
   agree ms sp rs ->
-  agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v).
+  Val.lessdef v v' ->
+  agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v').
 Proof.
-  unfold agree; intros. elim H; intros; clear H.
-  split. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR1.
+  intros. inv H. constructor.
+  rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR1.
+  auto.
   intros. unfold Regmap.set. case (RegEq.eq r0 r); intro.
   subst r0. rewrite Pregmap.gss. auto.
   rewrite Pregmap.gso. auto. red; intro. 
@@ -296,13 +314,14 @@ Qed.
 Hint Resolve agree_nextinstr: ppcgen.
 
 Lemma agree_set_mireg_twice:
-  forall ms sp rs r v v',
+  forall ms sp rs r v v' v1,
   agree ms sp rs ->
   mreg_type r = Tint ->
-  agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v' #(ireg_of r) <- v).
+  Val.lessdef v v' ->
+  agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v1 #(ireg_of r) <- v').
 Proof.
-  intros. replace (IR (ireg_of r)) with (preg_of r). elim H; intros.
-  split. repeat (rewrite Pregmap.gso; auto with ppcgen).
+  intros. replace (IR (ireg_of r)) with (preg_of r). inv H.
+  split. repeat (rewrite Pregmap.gso; auto with ppcgen). auto.
   intros. case (mreg_eq r r0); intro.
   subst r0. rewrite Regmap.gss. rewrite Pregmap.gss. auto.
   assert (preg_of r <> preg_of r0). 
@@ -314,15 +333,17 @@ Qed.
 Hint Resolve agree_set_mireg_twice: ppcgen.
 
 Lemma agree_set_twice_mireg:
-  forall ms sp rs r v v',
-  agree (Regmap.set r v' ms) sp rs ->
+  forall ms sp rs r v v1 v',
+  agree (Regmap.set r v1 ms) sp rs ->
   mreg_type r = Tint ->
-  agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v).
+  Val.lessdef v v' ->
+  agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v').
 Proof.
-  intros. elim H; intros.
+  intros. inv H. 
   split. rewrite Pregmap.gso. auto. 
   generalize (ireg_of_not_GPR1 r); congruence.
-  intros. generalize (H2 r0). 
+  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.
@@ -367,20 +388,66 @@ Lemma agree_set_mireg_exten:
   forall ms sp rs r v (rs': regset),
   agree ms sp rs ->
   mreg_type r = Tint ->
-  rs'#(ireg_of r) = v ->
+  Val.lessdef v rs'#(ireg_of r) ->
   (forall r', 
-     r' <> IR GPR12 -> r' <> FR FPR13 ->
+     r' <> IR GPR0 ->
      r' <> PC -> r' <> LR -> r' <> CTR ->
      r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 ->
      r' <> CARRY ->
      r' <> IR (ireg_of r) -> rs'#r' = rs#r') ->
   agree (Regmap.set r v ms) sp rs'.
 Proof.
-  intros. apply agree_exten_2 with (rs#(ireg_of r) <- v).
+  intros. set (v' := rs'#(ireg_of r)). 
+  apply agree_exten_2 with (rs#(ireg_of r) <- v').
   auto with ppcgen.
   intros. unfold Pregmap.set. case (PregEq.eq r0 (ireg_of r)); intro.
   subst r0. auto. apply H2; auto.
 Qed.
+Hint Resolve agree_set_mireg_exten: ppcgen.
+
+Lemma agree_undef_regs:
+  forall rl ms sp rs rs',
+  agree ms sp rs ->
+  (forall r, is_data_reg r -> ~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_1 with rs; auto.
+  apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))).
+  apply agree_set_mreg; 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, 
+     r <> IR GPR0 ->
+     r <> PC -> r <> LR -> r <> CTR ->
+     r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 ->
+     r <> CARRY ->
+     r <> IR GPR11 -> r <> IR GPR12 ->
+     r <> FR FPR0 -> r <> FR FPR12 -> r <> FR FPR13 ->
+     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. 
+  apply H0; (red; intro; subst; simpl in H1; intuition congruence).
+Qed.
+Hint Resolve agree_undef_temps: ppcgen.
+
+Lemma agree_undef_temps_2:
+  forall ms sp rs,
+  agree ms sp rs ->
+  agree (undef_temps ms) sp rs.
+Proof.
+  intros. apply agree_undef_temps with rs; auto. 
+Qed.
+Hint Resolve agree_undef_temps_2: ppcgen.
 
 (** Useful properties of the PC and GPR0 registers. *)
 
@@ -416,33 +483,41 @@ Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: ppcgen.
     functions. *)
 
 Lemma extcall_arg_match:
-  forall ms sp rs m l v,
+  forall ms sp rs m m' l v,
   agree ms sp rs ->
+  Mem.extends m m' ->
   Machconcr.extcall_arg ms m sp l v ->
-  Asm.extcall_arg rs m l v.
+  exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'.
 Proof.
-  intros. inv H0. 
-  rewrite (preg_val _ _ _ r H). constructor.
-  rewrite (sp_val _ _ _ H) in H1.
-  destruct ty; unfold load_stack in H1.
-  econstructor. reflexivity. assumption.
-  econstructor. reflexivity. assumption.
+  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.
 Qed.
 
 Lemma extcall_args_match:
-  forall ms sp rs m, agree ms sp rs ->
+  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
   forall ll vl,
   Machconcr.extcall_args ms m sp ll vl ->
-  Asm.extcall_args rs m ll vl.
+  exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'.
 Proof.
-  induction 2; constructor; auto. eapply extcall_arg_match; eauto.
+  induction 3; intros. 
+  exists (@nil val); split. constructor. constructor.
+  exploit extcall_arg_match; eauto. intros [v1' [A B]].
+  exploit IHextcall_args; eauto. intros [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto.
 Qed.
 
 Lemma extcall_arguments_match:
-  forall ms m sp rs sg args,
-  agree ms sp rs ->
+  forall ms m m' sp rs sg args,
+  agree ms sp rs -> Mem.extends m m' ->
   Machconcr.extcall_arguments ms m sp sg args ->
-  Asm.extcall_arguments rs m sg args.
+  exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
 Proof.
   unfold Machconcr.extcall_arguments, Asm.extcall_arguments; intros.
   eapply extcall_args_match; eauto.
@@ -611,16 +686,16 @@ Qed.
 
 (** Add integer immediate. *)
 
-Lemma addimm_1_correct:
+Lemma addimm_correct:
   forall r1 r2 n k rs m,
   r1 <> GPR0 ->
   r2 <> GPR0 ->
   exists rs',
-     exec_straight (addimm_1 r1 r2 n k) rs m  k rs' m
+     exec_straight (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_1.
+  intros. unfold addimm.
   (* addi *)
   case (Int.eq (high_s n) Int.zero).
   exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))).
@@ -653,55 +728,18 @@ Proof.
   unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
 Qed. 
 
-Lemma addimm_2_correct:
-  forall r1 r2 n k rs m,
-  r2 <> GPR12 ->
-  exists rs',
-     exec_straight (addimm_2 r1 r2 n k) rs m  k rs' m
-  /\ rs'#r1 = Val.add rs#r2 (Vint n)
-  /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'.
-Proof.
-  intros. unfold addimm_2.
-  generalize (loadimm_correct GPR12 n (Padd r1 r2 GPR12 :: k) rs m).
-  intros [rs1 [EX [RES OTHER]]].
-  exists (nextinstr (rs1#r1 <- (Val.add rs#r2 (Vint n)))).
-  split. eapply exec_straight_trans. eexact EX. 
-  apply exec_straight_one. simpl. rewrite RES. rewrite OTHER.
-  auto. congruence. discriminate.
-  reflexivity. 
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-Qed.
-
-Lemma addimm_correct:
-  forall r1 r2 n k rs m,
-  r2 <> GPR12 ->
-  exists rs',
-     exec_straight (addimm r1 r2 n k) rs m  k rs' m
-  /\ rs'#r1 = Val.add rs#r2 (Vint n)
-  /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'.
-Proof.
-  intros. unfold addimm.
-  case (ireg_eq r1 GPR0); intro.
-  apply addimm_2_correct; auto.
-  case (ireg_eq r2 GPR0); intro.
-  apply addimm_2_correct; auto.
-  generalize (addimm_1_correct r1 r2 n k rs m n0 n1).  
-  intros [rs' [EX [RES OTH]]]. exists rs'. intuition. 
-Qed.
-
 (** And integer immediate. *)
 
 Lemma andimm_correct:
   forall r1 r2 n k (rs : regset) m,
-  r2 <> GPR12 ->
+  r2 <> GPR0 ->
   let v := Val.and rs#r2 (Vint n) in
   exists rs',
      exec_straight (andimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = v
   /\ rs'#CR0_2 = Val.cmp Ceq v Vzero
   /\ forall r': preg,
-       r' <> r1 -> r' <> GPR12 -> r' <> PC ->
+       r' <> r1 -> r' <> GPR0 -> r' <> PC ->
        r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 ->
        rs'#r' = rs#r'.
 Proof.
@@ -728,7 +766,7 @@ Proof.
   split. auto.
   intros. rewrite D; auto. apply Pregmap.gso; auto.
   (* loadimm + and *)
-  generalize (loadimm_correct GPR12 n (Pand_ r1 r2 GPR12 :: k) rs m).
+  generalize (loadimm_correct GPR0 n (Pand_ r1 r2 GPR0 :: k) rs m).
   intros [rs1 [EX1 [RES1 OTHER1]]].
   exists (nextinstr (compare_sint (rs1#r1 <- v) v Vzero)).
   generalize (compare_sint_spec (rs1#r1 <- v) v Vzero).
@@ -823,21 +861,6 @@ Qed.
 
 (** Indexed memory loads. *)
 
-Lemma loadind_aux_correct:
-  forall (base: ireg) ofs ty dst (rs: regset) m v,
-  Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v ->
-  mreg_type dst = ty ->
-  base <> GPR0 ->
-  exec_instr ge fn (loadind_aux base ofs ty dst) rs m =
-    OK (nextinstr (rs#(preg_of dst) <- v)) m.
-Proof.
-  intros. unfold loadind_aux. unfold preg_of. rewrite H0. destruct ty.
-  simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto.
-  unfold const_low. simpl in H. rewrite H. auto.
-  simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto.
-  unfold const_low. simpl in H. rewrite H. auto.
-Qed.
-
 Lemma loadind_correct:
   forall (base: ireg) ofs ty dst k (rs: regset) m v,
   Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v ->
@@ -846,50 +869,33 @@ Lemma loadind_correct:
   exists rs',
      exec_straight (loadind base ofs ty dst k) rs m k rs' m
   /\ rs'#(preg_of dst) = v
-  /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> r <> preg_of dst -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
-  intros. unfold loadind.
-  assert (preg_of dst <> PC).
-    unfold preg_of. case (mreg_type dst); discriminate.
-  (* short offset *)
-  case (Int.eq (high_s ofs) Int.zero).
-  exists (nextinstr (rs#(preg_of dst) <- v)).
-  split. apply exec_straight_one. apply loadind_aux_correct; auto. 
-  unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. auto. auto.
-  split. rewrite nextinstr_inv; auto. apply Pregmap.gss.
+  intros. unfold loadind. destruct (Int.eq (high_s ofs) Int.zero).
+(* one load *)
+  exists (nextinstr (rs#(preg_of dst) <- v)); split.
+  destruct ty; apply exec_straight_one; auto with ppcgen; simpl.
+  unfold load1. rewrite gpr_or_zero_not_zero; auto.
+  simpl in *. rewrite H. unfold preg_of; rewrite H0. auto.
+  unfold load1. rewrite gpr_or_zero_not_zero; auto.
+  simpl in *. rewrite H. unfold preg_of; rewrite H0. auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
   intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  (* long offset *)
-  pose (rs1 := nextinstr (rs#GPR12 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
-  exists (nextinstr (rs1#(preg_of dst) <- v)).
-  split. apply exec_straight_two with rs1 m.
-  simpl. rewrite gpr_or_zero_not_zero; auto. 
-  apply loadind_aux_correct. 
-  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  rewrite Val.add_assoc. simpl. rewrite low_high_s. assumption.
-  auto. discriminate. reflexivity. 
-  unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. auto. auto.
-  split. rewrite nextinstr_inv; auto. apply Pregmap.gss.
+(* loadimm + one 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.
+  destruct ty; apply exec_straight_one; auto with ppcgen; simpl.
+  unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. 
+  unfold preg_of; rewrite H0. auto. congruence.
+  unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. 
+  unfold preg_of; rewrite H0. auto. congruence.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
   intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
 Qed.
 
 (** Indexed memory stores. *)
 
-Lemma storeind_aux_correct:
-  forall (base: ireg) ofs ty src (rs: regset) m m',
-  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 ->
-  exec_instr ge fn (storeind_aux src base ofs ty) rs m =
-    OK (nextinstr rs) m'.
-Proof.
-  intros. unfold storeind_aux. unfold preg_of in H. rewrite H0 in H. destruct ty.
-  simpl. unfold store1. rewrite gpr_or_zero_not_zero; auto.
-  unfold const_low. simpl in H. rewrite H. auto.
-  simpl. unfold store1. rewrite gpr_or_zero_not_zero; auto.
-  unfold const_low. simpl in H. rewrite H. auto.
-Qed.
-
 Lemma storeind_correct:
   forall (base: ireg) ofs ty src k (rs: regset) m m',
   Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' ->
@@ -897,28 +903,31 @@ Lemma storeind_correct:
   base <> GPR0 ->
   exists rs',
      exec_straight (storeind src base ofs ty k) rs m k rs' m'
-  /\ forall r, r <> PC -> r <> GPR12 -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
-  intros. unfold storeind.
-  (* short offset *)
-  case (Int.eq (high_s ofs) Int.zero).
-  exists (nextinstr rs).
-  split. apply exec_straight_one. apply storeind_aux_correct; auto. 
-  reflexivity. 
+  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 *)
+  exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
+  assert (rs' base = rs base). apply C; auto with ppcgen. congruence.
+  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. 
-  (* long offset *)
-  pose (rs1 := nextinstr (rs#GPR12 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
-  exists (nextinstr rs1).
-  split. apply exec_straight_two with rs1 m.
-  simpl. rewrite gpr_or_zero_not_zero; auto. 
-  apply storeind_aux_correct; auto with ppcgen.
-  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  rewrite nextinstr_inv; auto with ppcgen.
-  rewrite Pregmap.gso; auto with ppcgen.
-  rewrite Val.add_assoc. simpl. rewrite low_high_s. assumption.
-  reflexivity. reflexivity.
-  intros. rewrite nextinstr_inv; auto.
-  unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
 Qed.
 
 (** Float comparisons. *)
@@ -979,6 +988,19 @@ Ltac 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. *)
 
 Lemma transl_cond_correct_aux:
@@ -989,116 +1011,101 @@ Lemma transl_cond_correct_aux:
      exec_straight (transl_cond cond args k) rs m k rs' m
   /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
        (if snd (crbit_for_cond cond)
-        then eval_condition_total cond (map ms args)
-        else Val.notbool (eval_condition_total cond (map ms args)))
+        then eval_condition_total cond (map rs (map preg_of args))
+        else Val.notbool (eval_condition_total cond (map rs (map preg_of args))))
   /\ agree ms sp rs'.
 Proof.
-  intros.  destruct cond; simpl in H; TypeInv.
+  intros.
+  destruct cond; simpl in H; TypeInv; simpl; UseTypeInfo.
   (* Ccomp *)
-  simpl. 
-  generalize (compare_sint_spec rs ms#m0 ms#m1).
-  intros [A [B [C D]]].
-  exists (nextinstr (compare_sint rs ms#m0 ms#m1)).
-  split. apply exec_straight_one. simpl. 
-  repeat (rewrite <- (ireg_val ms sp rs); auto).
-  reflexivity.
+  destruct (compare_sint_spec rs (rs (ireg_of m0)) (rs (ireg_of m1)))
+  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.
   apply agree_exten_2 with rs; auto.
   (* Ccompu *)
-  simpl. 
-  generalize (compare_uint_spec rs ms#m0 ms#m1).
-  intros [A [B [C D]]].
-  exists (nextinstr (compare_uint rs ms#m0 ms#m1)).
-  split. apply exec_straight_one. simpl. 
-  repeat (rewrite <- (ireg_val ms sp rs); auto).
-  reflexivity.
+  destruct (compare_uint_spec rs (rs (ireg_of m0)) (rs (ireg_of m1)))
+  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.
   apply agree_exten_2 with rs; auto.
   (* Ccompimm *)
-  simpl.
   case (Int.eq (high_s i) Int.zero).
-  generalize (compare_sint_spec rs ms#m0 (Vint i)).
-  intros [A [B [C D]]].
-  exists (nextinstr (compare_sint rs ms#m0 (Vint i))).
-  split. apply exec_straight_one. simpl. 
-  repeat (rewrite <- (ireg_val ms sp rs); auto).
-  reflexivity.
+  destruct (compare_sint_spec rs (rs (ireg_of m0)) (Vint i))
+  as [A [B [C D]]].
+  econstructor; split.
+  apply exec_straight_one. simpl. eauto. reflexivity.
   split. 
   case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
   apply agree_exten_2 with rs; auto.
-  generalize (loadimm_correct GPR12 i (Pcmpw (ireg_of m0) GPR12 :: k) rs m).
+  generalize (loadimm_correct GPR0 i (Pcmpw (ireg_of m0) GPR0 :: k) rs m).
   intros [rs1 [EX1 [RES1 OTH1]]].
-  assert (agree ms sp rs1). apply agree_exten_2 with rs; auto.
-  generalize (compare_sint_spec rs1 ms#m0 (Vint i)).
-  intros [A [B [C D]]].
-  exists (nextinstr (compare_sint rs1 ms#m0 (Vint i))).
+  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. decEq. auto with ppcgen.
+  exists (nextinstr (compare_sint rs1 (rs1 (ireg_of m0)) (Vint i))).
   split. eapply exec_straight_trans. eexact EX1.
-  apply exec_straight_one. simpl. 
-  repeat (rewrite <- (ireg_val ms sp rs1); auto). rewrite RES1.
-  reflexivity. reflexivity.
-  split. 
+  apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto.
+  reflexivity. 
+  split. rewrite H. 
   case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
-  apply agree_exten_2 with rs1; auto.
+  apply agree_exten_2 with rs; auto.
+  intros. rewrite H; rewrite D; auto. 
   (* Ccompuimm *)
-  simpl.
   case (Int.eq (high_u i) Int.zero).
-  generalize (compare_uint_spec rs ms#m0 (Vint i)).
-  intros [A [B [C D]]].
-  exists (nextinstr (compare_uint rs ms#m0 (Vint i))).
-  split. apply exec_straight_one. simpl. 
-  repeat (rewrite <- (ireg_val ms sp rs); auto).
-  reflexivity.
+  destruct (compare_uint_spec rs (rs (ireg_of m0)) (Vint i))
+  as [A [B [C D]]].
+  econstructor; split.
+  apply exec_straight_one. simpl. eauto. reflexivity.
   split. 
   case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
   apply agree_exten_2 with rs; auto.
-  generalize (loadimm_correct GPR12 i (Pcmplw (ireg_of m0) GPR12 :: k) rs m).
+  generalize (loadimm_correct GPR0 i (Pcmplw (ireg_of m0) GPR0 :: k) rs m).
   intros [rs1 [EX1 [RES1 OTH1]]].
-  assert (agree ms sp rs1). apply agree_exten_2 with rs; auto.
-  generalize (compare_uint_spec rs1 ms#m0 (Vint i)).
-  intros [A [B [C D]]].
-  exists (nextinstr (compare_uint rs1 ms#m0 (Vint i))).
+  destruct (compare_uint_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. decEq. auto with ppcgen.
+  exists (nextinstr (compare_uint rs1 (rs1 (ireg_of m0)) (Vint i))).
   split. eapply exec_straight_trans. eexact EX1.
-  apply exec_straight_one. simpl. 
-  repeat (rewrite <- (ireg_val ms sp rs1); auto). rewrite RES1.
-  reflexivity. reflexivity.
-  split. 
+  apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto.
+  reflexivity. 
+  split. rewrite H. 
   case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
-  apply agree_exten_2 with rs1; auto.
+  apply agree_exten_2 with rs; auto.
+  intros. rewrite H; rewrite D; auto. 
   (* Ccompf *)
-  simpl.
-  generalize (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m).
-  intros [rs' [EX [RES OTH]]].
+  destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m)
+  as [rs' [EX [RES OTH]]].
   exists rs'. split. auto. 
-  split. rewrite RES. repeat (rewrite <- (freg_val ms sp rs); auto). 
+  split. apply RES. 
   apply agree_exten_2 with rs; auto.
   (* Cnotcompf *)
-  simpl. 
-  generalize (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m).
-  intros [rs' [EX [RES OTH]]].
+  destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m)
+  as [rs' [EX [RES OTH]]].
   exists rs'. split. auto. 
-  split. rewrite RES. repeat (rewrite <- (freg_val ms sp rs); auto).
+  split. rewrite RES.
   assert (forall v1 v2, Val.notbool (Val.notbool (Val.cmpf c v1 v2)) = Val.cmpf c v1 v2).
     intros v1 v2; unfold Val.cmpf; destruct v1; destruct v2; auto. 
     apply Val.notbool_idem2.
-  rewrite H.
-  generalize RES. case (snd (crbit_for_fcmp c)); simpl; auto.
+  rewrite H. case (snd (crbit_for_fcmp c)); simpl; auto.
   apply agree_exten_2 with rs; auto.
   (* Cmaskzero *)
-  simpl.
-  generalize (andimm_correct GPR12 (ireg_of m0) i k rs m (ireg_of_not_GPR12 m0)).
-  intros [rs' [A [B [C D]]]].
+  destruct (andimm_correct GPR0 (ireg_of m0) i k rs m (ireg_of_not_GPR0 m0))
+  as [rs' [A [B [C D]]]].
   exists rs'. split. assumption. 
-  split. rewrite C. rewrite <- (ireg_val ms sp rs); auto.
+  split. rewrite C. auto. 
   apply agree_exten_2 with rs; auto.
   (* Cmasknotzero *)
-  simpl.
-  generalize (andimm_correct GPR12 (ireg_of m0) i k rs m (ireg_of_not_GPR12 m0)).
-  intros [rs' [A [B [C D]]]].
+  destruct (andimm_correct GPR0 (ireg_of m0) i k rs m (ireg_of_not_GPR0 m0))
+  as [rs' [A [B [C D]]]].
   exists rs'. split. assumption. 
-  split. rewrite C. rewrite <- (ireg_val ms sp rs); auto.
-  rewrite Val.notbool_idem3. reflexivity. 
+  split. rewrite C. rewrite Val.notbool_idem3. reflexivity. 
   apply agree_exten_2 with rs; auto.
 Qed.
 
@@ -1115,31 +1122,37 @@ Lemma transl_cond_correct:
         else Val.notbool (Val.of_bool b))
   /\ agree ms sp rs'.
 Proof.
-  intros. rewrite <- (eval_condition_weaken _ _ H1). 
-  apply transl_cond_correct_aux; auto.
+  intros.
+  assert (eval_condition_total cond rs ## (preg_of ## args) = Val.of_bool b).
+    apply eval_condition_weaken. eapply eval_condition_lessdef; eauto. 
+    eapply preg_vals; eauto.
+  rewrite <- H2. eapply transl_cond_correct_aux; eauto.
 Qed.
 
 (** Translation of arithmetic operations. *)
 
 Ltac TranslOpSimpl :=
+  econstructor; split;
+  [ apply exec_straight_one; [simpl; eauto | reflexivity]
+  | auto 7 with ppcgen; fail ].
+(*
   match goal with
-  | |- exists rs' : regset,
+  | H: (Val.lessdef ?v ?v') |-
+         exists rs' : regset,
          exec_straight ?c ?rs ?m ?k rs' ?m /\
          agree (Regmap.set ?res ?v ?ms) ?sp rs'  =>
-    (exists (nextinstr (rs#(ireg_of res) <- v));
+
+    (exists (nextinstr (rs#(ireg_of res) <- v'));
      split; 
-     [ apply exec_straight_one;
-       [ repeat (rewrite (ireg_val ms sp rs); auto); reflexivity
-       | reflexivity ]
+     [ apply exec_straight_one; auto; fail
      | auto with ppcgen ])
   ||
-    (exists (nextinstr (rs#(freg_of res) <- v));
+    (exists (nextinstr (rs#(freg_of res) <- v'));
      split; 
-     [ apply exec_straight_one;
-       [ repeat (rewrite (freg_val ms sp rs); auto); reflexivity
-       | reflexivity ]
+     [ apply exec_straight_one; auto; fail
      | auto with ppcgen ])
   end.
+*)
 
 Lemma transl_op_correct:
   forall op args res k ms sp rs m v,
@@ -1147,41 +1160,44 @@ Lemma transl_op_correct:
   agree ms sp rs ->
   eval_operation ge sp op (map ms args) = Some v ->
   exists rs',
-     exec_straight (transl_op op args res k) rs m k rs' m
-  /\ agree (Regmap.set res v ms) sp 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'.
 Proof.
-  intros. rewrite <- (eval_operation_weaken _ _ _ _ H1). clear H1; clear v.
-  inversion H.
+  intros.
+  assert (exists v', Val.lessdef v v' /\
+          eval_operation_total ge sp op (map rs (map preg_of args)) = v').
+    exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. 
+    intros [v' [A B]]. exists v'; split; auto.
+    apply eval_operation_weaken; eauto. 
+  destruct H2 as [v' [LD EQ]]. clear H1.
+  inv H.
   (* Omove *)
-  simpl. exists (nextinstr (rs#(preg_of res) <- (ms r1))).
-  split. caseEq (mreg_type r1); intro.
-  apply exec_straight_one. simpl. rewrite (ireg_val ms sp rs); auto.
-  simpl. unfold preg_of. rewrite <- H2. rewrite H5. reflexivity.
-  auto with ppcgen.
-  apply exec_straight_one. simpl. rewrite (freg_val ms sp rs); auto.
-  simpl. unfold preg_of. rewrite <- H2. rewrite H5. reflexivity.
-  auto with ppcgen.
-  auto with ppcgen.
+  simpl in *. 
+  exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))).
+  split. unfold preg_of. rewrite <- H2.
+  destruct (mreg_type r1); apply exec_straight_one; auto.
+  auto with ppcgen. 
   (* Other instructions *)
-  clear H1; clear H2; clear H4.
-  destruct op; simpl in H5; injection H5; clear H5; intros;
-  TypeInv; simpl; try (TranslOpSimpl).
+  destruct op; simpl; simpl in H5; injection H5; clear H5; intros;
+  TypeInv; simpl in *; UseTypeInfo; try (TranslOpSimpl).
   (* Omove again *)
   congruence.
   (* Ointconst *)
-  generalize (loadimm_correct (ireg_of res) i k rs m).
-  intros [rs' [A [B C]]]. 
+  destruct (loadimm_correct (ireg_of res) i k rs m)
+  as [rs' [A [B C]]]. 
   exists rs'. split. auto. 
-  apply agree_set_mireg_exten with rs; auto. 
+  rewrite <- B in LD. eauto with ppcgen. 
   (* Ofloatconst *)
-  exists (nextinstr (rs#(freg_of res) <- (Vfloat f) #GPR12 <- Vundef)).
+  exists (nextinstr (rs #GPR12 <- Vundef #(freg_of res) <- (Vfloat f))).
   split. apply exec_straight_one. reflexivity. reflexivity.
-  auto with ppcgen.
+  apply agree_nextinstr. apply agree_set_mfreg; auto. apply agree_set_mreg; auto.
+  eapply agree_undef_temps; eauto. 
+  intros. apply Pregmap.gso; auto. 
   (* Oaddrsymbol *)
-  change (find_symbol_offset ge i i0) with (symbol_offset ge i i0).
-  set (v := symbol_offset ge i i0).
-  pose (rs1 := nextinstr (rs#GPR12 <- (high_half v))).
-  exists (nextinstr (rs1#(ireg_of res) <- v)).
+  change (find_symbol_offset ge i i0) with (symbol_offset ge i i0) in LD.
+  set (v' := symbol_offset ge i i0) in *.
+  pose (rs1 := nextinstr (rs#GPR12 <- (high_half v'))).
+  exists (nextinstr (rs1#(ireg_of res) <- v')).
   split. apply exec_straight_two with rs1 m.
   unfold exec_instr. rewrite gpr_or_zero_zero.
   unfold const_high. rewrite Val.add_commut. 
@@ -1189,173 +1205,127 @@ Proof.
   simpl. rewrite gpr_or_zero_not_zero. 2: congruence. 
   unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen.
   rewrite Pregmap.gss. 
-  fold v. rewrite Val.add_commut. unfold v. rewrite low_high_half.
+  fold v'. rewrite Val.add_commut. unfold v'. rewrite low_high_half.
   reflexivity. reflexivity. reflexivity. 
   unfold rs1. apply agree_nextinstr. apply agree_set_mireg; auto.
-  apply agree_set_mreg. apply agree_nextinstr.
-  apply agree_set_other. auto. simpl. tauto.
+  apply agree_set_mreg; auto. apply agree_nextinstr.
+  eapply agree_undef_temps; eauto.
+  intros. apply Pregmap.gso; auto.
   (* Oaddrstack *)
-  assert (GPR1 <> GPR12). discriminate.
-  generalize (addimm_correct (ireg_of res) GPR1 i k rs m H2). 
+  assert (GPR1 <> GPR0). discriminate.
+  generalize (addimm_correct (ireg_of res) GPR1 i k rs m (ireg_of_not_GPR0 res) H1). 
   intros [rs' [EX [RES OTH]]].
   exists rs'. split. auto. 
-  apply agree_set_mireg_exten with rs; auto.
-  rewrite (sp_val ms sp rs). auto. auto. 
+  apply agree_set_mireg_exten with rs; auto with ppcgen.
+  rewrite (sp_val ms sp rs) in LD; auto. rewrite RES; auto. 
   (* Ocast8unsigned *)
-  exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 255)))).
-  split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity.
-  replace (Val.zero_ext 8 (ms m0))
-      with (Val.rolm (ms m0) Int.zero (Int.repr 255)).
+  econstructor; split.
+  apply exec_straight_one. simpl; reflexivity. reflexivity. 
+  replace (Val.zero_ext 8 (rs (ireg_of m0)))
+      with (Val.rolm (rs (ireg_of m0)) Int.zero (Int.repr 255)) in LD.
   auto with ppcgen. 
-  unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto. 
+  unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto.
   rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
   (* Ocast16unsigned *)
-  exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 65535)))).
-  split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity.
-  replace (Val.zero_ext 16 (ms m0))
-      with (Val.rolm (ms m0) Int.zero (Int.repr 65535)).
+  econstructor; split.
+  apply exec_straight_one. simpl; reflexivity. reflexivity. 
+  replace (Val.zero_ext 16 (rs (ireg_of m0)))
+      with (Val.rolm (rs (ireg_of m0)) Int.zero (Int.repr 65535)) in LD.
   auto with ppcgen. 
-  unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto. 
+  unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto.
   rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
   (* Oaddimm *)
   generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m
-                            (ireg_of_not_GPR12 m0)).
+                            (ireg_of_not_GPR0 res) (ireg_of_not_GPR0 m0)).
   intros [rs' [A [B C]]]. 
   exists rs'. split. auto.
-  apply agree_set_mireg_exten with rs; auto.
-  rewrite (ireg_val ms sp rs); auto. 
-  (* Osub *)
-  exists (nextinstr (rs#(ireg_of res) <- (Val.sub (ms m0) (ms m1)) #CARRY <- Vundef)).
-  split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto).
-  simpl. reflexivity. auto with ppcgen.
+  rewrite <- B in LD. eauto with ppcgen.  
   (* Osubimm *)
   case (Int.eq (high_s i) Int.zero).
-  exists (nextinstr (rs#(ireg_of res) <- (Val.sub (Vint i) (ms m0)) #CARRY <- Vundef)).
-  split. apply exec_straight_one. rewrite (ireg_val ms sp rs); auto.
-  reflexivity. simpl. auto with ppcgen.
-  generalize (loadimm_correct GPR12 i (Psubfc (ireg_of res) (ireg_of m0) GPR12 :: k) rs m).
+  econstructor; split.
+  apply exec_straight_one. simpl; eauto. auto.
+  auto 7 with ppcgen.
+  generalize (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m).
   intros [rs1 [EX [RES OTH]]].
-  assert (agree ms sp rs1). apply agree_exten_2 with rs; auto.
-  exists (nextinstr (rs1#(ireg_of res) <- (Val.sub (Vint i) (ms m0)) #CARRY <- Vundef)).
-  split. eapply exec_straight_trans. eexact EX. 
-  apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto).
-  simpl. rewrite RES. rewrite OTH. reflexivity. 
-  generalize (ireg_of_not_GPR12 m0); congruence.
-  discriminate.
-  reflexivity. simpl; auto with ppcgen.
+  econstructor; split.
+  eapply exec_straight_trans. eexact EX. 
+  apply exec_straight_one. simpl; eauto. auto.
+  rewrite RES. rewrite OTH; auto with ppcgen.
+  assert (agree (undef_temps ms) sp rs1). eauto with ppcgen.  
+  auto with ppcgen. decEq; auto with ppcgen.
   (* Omulimm *)
   case (Int.eq (high_s i) Int.zero).
-  exists (nextinstr (rs#(ireg_of res) <- (Val.mul (ms m0) (Vint i)))).
-  split. apply exec_straight_one. rewrite (ireg_val ms sp rs); auto.
-  reflexivity. auto with ppcgen.
-  generalize (loadimm_correct GPR12 i (Pmullw (ireg_of res) (ireg_of m0) GPR12 :: k) rs m).
+  econstructor; split.
+  apply exec_straight_one. simpl; eauto. auto. 
+  auto with ppcgen.
+  generalize (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m).
   intros [rs1 [EX [RES OTH]]].
-  assert (agree ms sp rs1). apply agree_exten_2 with rs; auto.
-  exists (nextinstr (rs1#(ireg_of res) <- (Val.mul (ms m0) (Vint i)))).
-  split. eapply exec_straight_trans. eexact EX. 
-  apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto).
-  simpl. rewrite RES. rewrite OTH. reflexivity. 
-  generalize (ireg_of_not_GPR12 m0); congruence.
-  discriminate.
-  reflexivity. simpl; auto with ppcgen.
+  assert (agree (undef_temps ms) sp rs1). eauto with ppcgen.
+  econstructor; split.
+  eapply exec_straight_trans. eexact EX. 
+  apply exec_straight_one. simpl; eauto. auto.
+  rewrite RES. rewrite OTH; auto with ppcgen. decEq; auto with ppcgen.
   (* Oand *)
-  pose (v := Val.and (ms m0) (ms m1)).
-  pose (rs1 := rs#(ireg_of res) <- v).
-  generalize (compare_sint_spec rs1 v Vzero).
+  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]]].
-  exists (nextinstr (compare_sint rs1 v Vzero)).
-  split. apply exec_straight_one. 
-  unfold rs1, v. repeat (rewrite (ireg_val ms sp rs); auto). 
-  reflexivity.  
-  apply agree_exten_2 with rs1. unfold rs1, v; auto with ppcgen.
+  exists (nextinstr (compare_sint rs1 v' Vzero)).
+  split. apply exec_straight_one. auto. auto. 
+  apply agree_exten_2 with rs1. unfold rs1; auto with ppcgen.
   auto.
   (* Oandimm *)
   generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m
-                             (ireg_of_not_GPR12 m0)).
+                             (ireg_of_not_GPR0 m0)).
   intros [rs' [A [B [C D]]]]. 
-  exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto.
-  rewrite (ireg_val ms sp rs); auto.
+  exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen.
   (* Oorimm *)
   generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m).
   intros [rs' [A [B C]]]. 
-  exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto.
-  rewrite (ireg_val ms sp rs); auto.
+  exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. 
   (* Oxorimm *)
   generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m).
   intros [rs' [A [B C]]]. 
-  exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto.
-  rewrite (ireg_val ms sp rs); auto.
-  (* Oshr *)
-  exists (nextinstr (rs#(ireg_of res) <- (Val.shr (ms m0) (ms m1)) #CARRY <- (Val.shr_carry (ms m0) (ms m1)))).
-  split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto).
-  reflexivity. auto with ppcgen.
-  (* Oshrimm *)
-  exists (nextinstr (rs#(ireg_of res) <- (Val.shr (ms m0) (Vint i)) #CARRY <- (Val.shr_carry (ms m0) (Vint i)))).
-  split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto).
-  reflexivity. auto with ppcgen.
+  exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen.
   (* Oxhrximm *)
-  pose (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shr (ms m0) (Vint i)) #CARRY <- (Val.shr_carry (ms m0) (Vint i)))).
-  exists (nextinstr (rs1#(ireg_of res) <- (Val.shrx (ms m0) (Vint i)))).
+  pose (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shr (rs (ireg_of m0)) (Vint i)) #CARRY <- (Val.shr_carry (rs (ireg_of m0)) (Vint i)))).
+  exists (nextinstr (rs1#(ireg_of res) <- (Val.shrx (rs (ireg_of m0)) (Vint i)))).
   split. apply exec_straight_two with rs1 m.
-  unfold rs1; rewrite (ireg_val ms sp rs); auto.
-  simpl; unfold rs1; repeat rewrite <- (ireg_val ms sp rs); auto.
-  repeat (rewrite nextinstr_inv; try discriminate).
-  repeat rewrite Pregmap.gss. decEq. decEq. 
-  apply (f_equal3 (@Pregmap.set val)); auto.
-  rewrite Pregmap.gso. rewrite Pregmap.gss. apply Val.shrx_carry.
-  discriminate. reflexivity. reflexivity.
-  apply agree_exten_2 with (rs#(ireg_of res) <- (Val.shrx (ms m0) (Vint i))).
-  auto with ppcgen. 
-  intros. rewrite nextinstr_inv; auto. 
-  case (preg_eq (ireg_of res) r); intro.
-  subst r. repeat rewrite Pregmap.gss. auto.
-  repeat rewrite Pregmap.gso; auto.
-  unfold rs1. rewrite nextinstr_inv; auto.
-  repeat rewrite Pregmap.gso; auto.
+  auto. simpl. decEq. decEq. decEq. 
+  unfold rs1. repeat (rewrite nextinstr_inv; try discriminate).
+  rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. 
+  apply Val.shrx_carry. auto with ppcgen. auto. auto. 
+  apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. 
+  apply agree_set_commut. auto with ppcgen. 
+  apply agree_set_other. apply agree_set_mireg_twice; auto with ppcgen. 
+  compute; auto. auto with ppcgen. 
   (* Ointoffloat *)
-  exists (nextinstr (rs#(ireg_of res) <- (Val.intoffloat (ms m0)) #FPR13 <- Vundef)).
-  split. apply exec_straight_one. 
-  repeat (rewrite (freg_val ms sp rs); auto).
-  reflexivity. auto with ppcgen.
-  (* Ointuoffloat *)
-  exists (nextinstr (rs#(ireg_of res) <- (Val.intuoffloat (ms m0)) #FPR13 <- Vundef)).
-  split. apply exec_straight_one. 
-  repeat (rewrite (freg_val ms sp rs); auto).
-  reflexivity. auto with ppcgen.
-  (* Ofloatofint *)
-  exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)) #GPR12 <- Vundef #FPR13 <- Vundef)).
-  split. apply exec_straight_one. 
-  repeat (rewrite (ireg_val ms sp rs); auto).
-  reflexivity. auto 10 with ppcgen.
-  (* Ofloatofintu *)
-  exists (nextinstr (rs#(freg_of res) <- (Val.floatofintu (ms m0)) #GPR12 <- Vundef #FPR13 <- Vundef)).
-  split. apply exec_straight_one. 
-  repeat (rewrite (ireg_val ms sp rs); auto).
-  reflexivity. auto 10 with ppcgen.
+  econstructor; split.
+  apply exec_straight_one. simpl; eauto. auto.
+  apply agree_nextinstr. apply agree_set_mireg; auto. apply agree_set_mreg; auto.
+  apply agree_undef_temps with rs; auto. intros. 
+  repeat rewrite Pregmap.gso; auto. 
   (* Ocmp *)
-  generalize H2; case (classify_condition c args); intros.
+  revert H1 LD; case (classify_condition c args); intros.
   (* Optimization: compimm Cge 0 *)
-  subst n. simpl in H4. simpl. 
-  set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.rolm (ms r) Int.one Int.one))).
+  subst n. simpl in *. inv H1. UseTypeInfo. 
+  set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))).
   set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.xor (rs1#(ireg_of res)) (Vint Int.one)))).
   exists rs2.
-  split. apply exec_straight_two with rs1 m. 
-  simpl. unfold rs1. rewrite (ireg_val ms sp rs); auto. congruence.
-  auto. auto. auto.
-  rewrite <- Val.rolm_ge_zero. 
+  split. apply exec_straight_two with rs1 m; auto.
+  rewrite <- Val.rolm_ge_zero in LD.
   unfold rs2. apply agree_nextinstr.
   unfold rs1. apply agree_nextinstr_commut. fold rs1.
-  replace (rs1 (ireg_of res)) with (Val.rolm (ms r) Int.one Int.one).
-  apply agree_set_mireg_twice; auto.
+  replace (rs1 (ireg_of res)) with (Val.rolm (rs (ireg_of r)) Int.one Int.one).
+  apply agree_set_mireg_twice; auto with ppcgen.
   unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. auto. 
   auto with ppcgen. auto with ppcgen. 
   (* Optimization: compimm Clt 0 *)
-  subst n. simpl in H4. simpl. 
-  exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms r) Int.one Int.one))).
-  split. apply exec_straight_one. simpl. rewrite (ireg_val ms sp rs); auto. congruence.
-  auto. 
-  apply agree_nextinstr. apply agree_set_mireg.
-  rewrite Val.rolm_lt_zero. apply agree_set_mreg. auto. congruence. 
+  subst n. simpl in *. inv H1. UseTypeInfo. 
+  exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))).
+  split. apply exec_straight_one; auto. 
+  rewrite <- Val.rolm_lt_zero in LD.
+  auto with ppcgen. 
   (* General case *)
   set (bit := fst (crbit_for_cond c0)).
   set (isset := snd (crbit_for_cond c0)).
@@ -1364,7 +1334,7 @@ Proof.
         (if isset
          then k
          else Pxori (ireg_of res) (ireg_of res) (Cint Int.one) :: k)).
-  generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m H4 H0).
+  generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m H1 H0).
   fold bit; fold isset. 
   intros [rs1 [EX1 [RES1 AG1]]].
   set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#(reg_of_crbit bit)))).
@@ -1374,89 +1344,63 @@ Proof.
   unfold k1. apply exec_straight_one. 
   reflexivity. reflexivity. 
   unfold rs2. rewrite RES1. auto with ppcgen. 
-  exists (nextinstr (rs2#(ireg_of res) <- (eval_condition_total c0 ms##rl))).
+  econstructor. 
   split. apply exec_straight_trans with k1 rs1 m. assumption.
   unfold k1. apply exec_straight_two with rs2 m.
-  reflexivity. simpl. 
-  replace (Val.xor (rs2 (ireg_of res)) (Vint Int.one))
-     with (eval_condition_total c0 ms##rl).
-  reflexivity.
-  unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  rewrite RES1. apply Val.notbool_xor. apply eval_condition_total_is_bool.
-  reflexivity. reflexivity. 
-  unfold rs2. auto with ppcgen. 
+  reflexivity. simpl. eauto. auto. auto. 
+  apply agree_nextinstr. 
+  unfold rs2 at 1. rewrite nextinstr_inv. rewrite Pregmap.gss. 
+  rewrite RES1. rewrite <- Val.notbool_xor. 
+  unfold rs2. auto 7 with ppcgen. 
+  apply eval_condition_total_is_bool.
+  auto with ppcgen. 
 Qed.
 
 Lemma transl_load_store_correct:
   forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
-    addr args k ms sp rs m ms' m',
+    addr args (temp: ireg) k ms sp rs m ms' m',
   (forall cst (r1: ireg) (rs1: regset) k,
-    eval_addressing_total ge sp addr (map ms args) =
+    eval_addressing_total ge sp addr (map rs (map preg_of args)) =
                 Val.add (gpr_or_zero rs1 r1) (const_low ge cst) ->
-    agree ms sp rs1 ->
+    (forall (r: preg), 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) (rs1: regset) k,
-    eval_addressing_total ge sp addr (map ms args) = Val.add rs1#r1 rs1#r2 ->
-    agree ms sp rs1 ->
+  (forall (r1 r2: ireg) k,
+    eval_addressing_total ge sp addr (map rs (map preg_of args)) = Val.add rs#r1 rs#r2 ->
     exists rs',
-    exec_straight (mk2 r1 r2 :: k) rs1 m k rs' m' /\
+    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 ->
   exists rs',
-    exec_straight (transl_load_store mk1 mk2 addr args k) rs m
+    exec_straight (transl_load_store mk1 mk2 addr args temp k) rs m
                         k rs' m'
   /\ agree ms' sp rs'.
 Proof.
   intros. destruct addr; simpl in H2; TypeInv; simpl.
   (* Aindexed *)
-  case (ireg_eq (ireg_of t) GPR0); intro.
-  (* Aindexed from GPR0 *)
-  set (rs1 := nextinstr (rs#GPR12 <- (ms t))).
-  set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
-  assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) =
-                Val.add (gpr_or_zero rs2 GPR12) (const_low ge (Cint (low_s i)))).
-    simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
-    unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
-    rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
-    discriminate.
-  assert (AG: agree ms sp rs2). unfold rs2, rs1; auto 6 with ppcgen.
-  destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
-  exists rs'. split.
-  apply exec_straight_trans with (mk1 (Cint (low_s i)) GPR12 :: k) rs2 m.
-  apply exec_straight_two with rs1 m.
-  unfold rs1. rewrite (ireg_val ms sp rs); auto.
-  unfold rs2. replace (ms t) with (rs1#GPR12). auto.
-  unfold rs1. rewrite nextinstr_inv. apply Pregmap.gss. discriminate.
-  reflexivity. reflexivity.  
-  assumption. assumption.
-  (* Aindexed short *)
   case (Int.eq (high_s i) Int.zero).
-  assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) =
-                Val.add (gpr_or_zero rs (ireg_of t)) (const_low ge (Cint i))).
-    simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
-    rewrite (ireg_val ms sp rs); auto.
-  destruct (H _ _ _ k ADDR H1) as [rs' [EX' AG']].
-  exists rs'. split. auto. auto.
+  (* Aindexed short *)
+  apply H. 
+  simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+  auto.
   (* Aindexed long *)
-  set (rs1 := nextinstr (rs#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
-  assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) =
-                Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Cint (low_s i)))).
-    simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
-    unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+  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. rewrite nextinstr_inv. rewrite Pregmap.gss. 
     rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
     discriminate.
-  assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
-  destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
+  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.
-  simpl. rewrite gpr_or_zero_not_zero; auto. 
-  rewrite <- (ireg_val ms sp rs); auto. reflexivity.
-  assumption. assumption.
+  simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto. 
+  auto. auto.
   (* Aindexed2 *)
   apply H0. 
-  simpl. repeat (rewrite (ireg_val ms sp rs); auto). auto.
+  simpl. UseTypeInfo; auto.
   (* Aglobal *)
   case_eq (symbol_is_small_data i i0); intro SISD.
   (* Aglobal from small data *)
@@ -1466,17 +1410,16 @@ Proof.
   destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero. auto.
   auto.
   (* Aglobal general case *)
-  set (rs1 := nextinstr (rs#GPR12 <- (const_high ge (Csymbol_high i i0)))).
-  assert (ADDR: eval_addressing_total ge sp (Aglobal i i0) ms##nil =
-                Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Csymbol_low i i0))).
+  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. apply low_high_half. 
-    discriminate. discriminate.
-  assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
-  destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
+    discriminate.
+    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_zero. 
   rewrite Val.add_commut. unfold const_high. 
@@ -1484,153 +1427,142 @@ Proof.
   reflexivity. reflexivity.
   assumption. assumption.
   (* Abased *)
-  assert (COMMON:
-    forall (rs1: regset) r,
-    r <> GPR0 ->
-    ms t = rs1#r ->
-    agree ms sp rs1 ->
-    exists rs',
-      exec_straight
-        (Paddis GPR12 r (Csymbol_high i i0)
-         :: mk1 (Csymbol_low i i0) GPR12 :: k) rs1 m k rs' m'
-      /\ agree ms' sp rs').
-  intros. 
-  set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (const_high ge (Csymbol_high i i0))))).
-  assert (ADDR: eval_addressing_total ge sp (Abased i i0) ms##(t::nil) =
-                Val.add (gpr_or_zero rs2 GPR12) (const_low ge (Csymbol_low i i0))).
-    simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
-    unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
-    unfold const_high. 
-    set (v := symbol_offset ge i i0).
+  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.
     rewrite Val.add_assoc. 
-    rewrite (Val.add_commut (high_half v)).
-    unfold v. rewrite low_high_half. apply Val.add_commut.
-    discriminate.
-  assert (AG: agree ms sp rs2). unfold rs2; auto with ppcgen.
-  destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
-  exists rs'. split. apply exec_straight_step with rs2 m.
-  unfold exec_instr. rewrite gpr_or_zero_not_zero; auto.
-  rewrite <- H3. reflexivity. reflexivity. 
-  assumption. assumption.
-  case (ireg_eq (ireg_of t) GPR0); intro.
-  set (rs1 := nextinstr (rs#GPR12 <- (ms t))).
-  assert (R1: GPR12 <> GPR0). discriminate.
-  assert (R2: ms t = rs1 GPR12). 
-    unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss; auto.
-    discriminate.
-  assert (R3: agree ms sp rs1). unfold rs1; auto with ppcgen.
-  generalize (COMMON rs1 GPR12 R1 R2 R3). intros [rs' [EX' AG']].
-  exists rs'. split.
-  apply exec_straight_step with rs1 m.
-  unfold rs1. rewrite (ireg_val ms sp rs); auto. reflexivity.
+    unfold const_high, const_low. 
+    set (v := symbol_offset ge i i0).
+    symmetry. rewrite Val.add_commut. decEq.
+    unfold v. rewrite Val.add_commut. apply low_high_half. 
+    UseTypeInfo. auto. discriminate. 
+    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. auto.
   assumption. assumption.
-  apply COMMON; auto. eapply ireg_val; eauto.
   (* 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#GPR12 <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))).
-  assert (ADDR: eval_addressing_total ge sp (Ainstack i) ms##nil =
-                Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Cint (low_s i)))).
-    simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+  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).
+    simpl. rewrite gpr_or_zero_not_zero; auto. 
     unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
-    rewrite Val.add_assoc. decEq. simpl. rewrite low_high_s. auto.
-    discriminate.
-  assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
-  destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
+    rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
+    congruence.
+    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.
-  simpl. rewrite gpr_or_zero_not_zero. 
-  unfold rs1. rewrite (sp_val ms sp rs). reflexivity.
-  auto. discriminate. reflexivity. assumption. assumption.
+  unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+  rewrite <- (sp_val ms sp rs); auto. auto.
+  assumption. assumption.
 Qed.
 
 (** Translation of memory loads. *)
 
 Lemma transl_load_correct:
   forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
-    chunk addr args k ms sp rs m dst a v,
+    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) ->
+    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) ->
+    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 ->
   Mem.loadv chunk m a = Some v ->
+  Mem.extends m m' ->
   exists rs',
-    exec_straight (transl_load_store mk1 mk2 addr args k) rs m
-                        k rs' m
-  /\ agree (Regmap.set dst v ms) sp 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'.
 Proof.
-  intros. apply transl_load_store_correct with ms.
-  intros. exists (nextinstr (rs1#(preg_of dst) <- v)). 
-  split. apply exec_straight_one. rewrite H. 
-  unfold load1. rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
-  rewrite H5 in H4. rewrite H4. auto.
-  auto with ppcgen. auto with ppcgen. 
-  intros. exists (nextinstr (rs1#(preg_of dst) <- v)). 
+  intros.
+  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
+  intros [a' [A B]]. 
+  exploit Mem.loadv_extends; eauto. intros [v' [C D]].
+  exploit eval_addressing_weaken. eexact A. intro E. rewrite <- E in C.
+  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 <- H6. rewrite C. auto.
+  auto with ppcgen.
+  eauto with ppcgen.
+(* mk2 *)
+  intros. exists (nextinstr (rs#(preg_of dst) <- v')). 
   split. apply exec_straight_one. rewrite H0. 
-  unfold load2. 
-  rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
-  rewrite H5 in H4. rewrite H4. auto.
-  auto with ppcgen. auto with ppcgen. 
-  auto. auto.
+  unfold load2. rewrite <- H6. rewrite C. auto.
+  auto with ppcgen.
+  eauto with ppcgen.
+(* not GPR0 *)
+  congruence.
 Qed.
 
 (** Translation of memory 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',
-  (forall cst (r1: ireg) (rs1: regset),
-    exists rs2,
-    exec_instr ge fn (mk1 cst r1) rs1 m =
-    store1 ge chunk (preg_of src) cst r1 rs2 m
-    /\ (forall (r: preg), r <> FPR13 -> rs2 r = rs1 r)) ->
-  (forall (r1 r2: ireg) (rs1: regset),
-    exists rs2,
-    exec_instr ge fn (mk2 r1 r2) rs1 m =
-    store2 chunk (preg_of src) r1 r2 rs2 m
-    /\ (forall (r: preg), r <> FPR13 -> rs2 r = rs1 r)) ->
+    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' ->
-  exists rs',
-    exec_straight (transl_load_store mk1 mk2 addr args k) rs m
-                        k rs' m'
-  /\ agree ms sp rs'.
+  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'.
 Proof.
-  intros. apply transl_load_store_correct with ms.
-  intros. destruct (H cst r1 rs1) as [rs2 [A B]].
-  exists (nextinstr rs2). 
-  split. apply exec_straight_one. rewrite A. 
-  unfold store1. rewrite B. replace (gpr_or_zero rs2 r1) with (gpr_or_zero rs1 r1).
-  rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
-  rewrite H5 in H4. elim H6; intros. rewrite H8 in H4.
-  rewrite H4. auto.
-  unfold gpr_or_zero. destruct (ireg_eq r1 GPR0); auto. symmetry. apply B. discriminate.
-  apply preg_of_not. simpl. tauto.
-  rewrite <- B. auto. discriminate.
-  apply agree_nextinstr. eapply agree_exten_2; eauto.
-
-  intros. destruct (H0 r1 r2 rs1) as [rs2 [A B]].
-  exists (nextinstr rs2). 
-  split. apply exec_straight_one. rewrite A. 
-  unfold store2. repeat rewrite B. 
-  rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
-  rewrite H5 in H4. elim H6; intros. rewrite H8 in H4.
-  rewrite H4. auto.
-  apply preg_of_not. simpl. tauto.
-  discriminate. discriminate.
-  rewrite <- B. auto. discriminate.
-  apply agree_nextinstr. eapply agree_exten_2; eauto.
-
-  auto. auto.
+  intros.
+  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
+  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]].
+  exploit eval_addressing_weaken. eexact A. intro E. rewrite <- E in C.
+  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 <- 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. 
+  eapply agree_undef_temps; eauto. intros. 
+  rewrite V; auto. rewrite nextinstr_inv; auto. apply H7; auto. 
+  unfold int_temp_for. destruct (mreg_eq src IT2); auto.
+(* mk2 *)
+  intros.
+  exploit (H0 r1 r2 rs (nextinstr rs) m1').
+  unfold store2. rewrite <- 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. rewrite nextinstr_inv; auto.
+  unfold int_temp_for. destruct (mreg_eq src IT2); congruence.
 Qed.
 
-
 End STRAIGHTLINE.
 
diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v
index d55635b..ae3c2bd 100644
--- a/powerpc/Asmgenretaddr.v
+++ b/powerpc/Asmgenretaddr.v
@@ -109,7 +109,7 @@ Hint Resolve loadimm_tail: ppcretaddr.
 
 Lemma addimm_tail:
   forall r1 r2 n k, is_tail k (addimm r1 r2 n k).
-Proof. unfold addimm, addimm_1, addimm_2; intros; IsTail. Qed.
+Proof. unfold addimm; intros; IsTail. Qed.
 Hint Resolve addimm_tail: ppcretaddr.
 
 Lemma andimm_tail:
@@ -129,12 +129,12 @@ Hint Resolve xorimm_tail: ppcretaddr.
 
 Lemma loadind_tail:
   forall base ofs ty dst k, is_tail k (loadind base ofs ty dst k).
-Proof. unfold loadind; intros; IsTail. Qed.
+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; IsTail. Qed.
+Proof. unfold storeind; intros. destruct ty; IsTail. Qed.
 Hint Resolve storeind_tail: ppcretaddr.
 
 Lemma floatcomp_tail:
@@ -156,8 +156,8 @@ Qed.
 Hint Resolve transl_op_tail: ppcretaddr.
 
 Lemma transl_load_store_tail:
-  forall mk1 mk2 addr args k,
-  is_tail k (transl_load_store mk1 mk2 addr args k).
+  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.
 
diff --git a/powerpc/ConstpropOp.v b/powerpc/ConstpropOp.v
index ededce0..b6eecc7 100644
--- a/powerpc/ConstpropOp.v
+++ b/powerpc/ConstpropOp.v
@@ -182,9 +182,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Omulsubf, F n1 :: F n2 :: F n3 :: nil => F(Float.sub (Float.mul n1 n2) n3)
   | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
   | Ointoffloat, F n1 :: nil => I(Float.intoffloat n1)
-  | Ointuoffloat, F n1 :: nil => I(Float.intuoffloat n1)
-  | Ofloatofint, I n1 :: nil => F(Float.floatofint n1)
-  | Ofloatofintu, I n1 :: nil => F(Float.floatofintu n1)
+  | Ofloatofwords, I n1 :: I n2 :: nil => F(Float.from_words n1 n2)
   | Ocmp c, vl =>
       match eval_static_condition c vl with
       | None => Unknown
@@ -322,11 +320,8 @@ Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx),
       forall n1,
       eval_static_operation_cases (Ointoffloat) (F n1 :: nil)
   | eval_static_operation_case45:
-      forall n1,
-      eval_static_operation_cases (Ofloatofint) (I n1 :: nil)
-  | eval_static_operation_case46:
-      forall n1,
-      eval_static_operation_cases (Ofloatofintu) (I n1 :: nil)
+      forall n1 n2,
+      eval_static_operation_cases (Ofloatofwords) (I n1 :: I n2 :: nil)
   | eval_static_operation_case47:
       forall c vl,
       eval_static_operation_cases (Ocmp c) (vl)
@@ -336,9 +331,6 @@ Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx),
   | eval_static_operation_case49:
       forall n1,
       eval_static_operation_cases (Ocast16unsigned) (I n1 :: nil)
-  | eval_static_operation_case50:
-      forall n1,
-      eval_static_operation_cases (Ointuoffloat) (F n1 :: nil)
   | eval_static_operation_default:
       forall (op: operation) (vl: list approx),
       eval_static_operation_cases op vl.
@@ -429,18 +421,14 @@ Definition eval_static_operation_match (op: operation) (vl: list approx) :=
       eval_static_operation_case43 n1
   | Ointoffloat, F n1 :: nil =>
       eval_static_operation_case44 n1
-  | Ofloatofint, I n1 :: nil =>
-      eval_static_operation_case45 n1
-  | Ofloatofintu, I n1 :: nil =>
-      eval_static_operation_case46 n1
+  | Ofloatofwords, I n1 :: I n2 :: nil =>
+      eval_static_operation_case45 n1 n2
   | Ocmp c, vl =>
       eval_static_operation_case47 c vl
   | Ocast8unsigned, I n1 :: nil =>
       eval_static_operation_case48 n1
   | Ocast16unsigned, I n1 :: nil =>
       eval_static_operation_case49 n1
-  | Ointuoffloat, F n1 :: nil =>
-      eval_static_operation_case50 n1
   | op, vl =>
       eval_static_operation_default op vl
   end.
@@ -531,10 +519,8 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
       F(Float.singleoffloat n1)
   | eval_static_operation_case44 n1 =>
       I(Float.intoffloat n1)
-  | eval_static_operation_case45 n1 =>
-      F(Float.floatofint n1)
-  | eval_static_operation_case46 n1 =>
-      F(Float.floatofintu n1)
+  | eval_static_operation_case45 n1 n2 =>
+      F(Float.from_words n1 n2)
   | eval_static_operation_case47 c vl =>
       match eval_static_condition c vl with
       | None => Unknown
@@ -544,8 +530,6 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
       I(Int.zero_ext 8 n1)
   | eval_static_operation_case49 n1 =>
       I(Int.zero_ext 16 n1)
-  | eval_static_operation_case50 n1 =>
-      I(Float.intuoffloat n1)
   | eval_static_operation_default op vl =>
       Unknown
   end.
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 88b70c1..632a55d 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -41,18 +41,19 @@ Inductive mreg: Type :=
   (** Allocatable float regs *)
   | F1: mreg  | F2: mreg  | F3: mreg  | F4: mreg
   | F5: mreg  | F6: mreg  | F7: mreg  | F8: mreg
-  | F9: mreg  | F10: mreg | F14: mreg | F15: mreg
+  | F9: mreg  | F10: mreg | F11: mreg
+  | F14: mreg | F15: mreg
   | F16: mreg | F17: mreg | F18: mreg | F19: mreg
   | F20: mreg | F21: mreg | F22: mreg | F23: mreg
   | F24: mreg | F25: mreg | F26: mreg | F27: mreg
   | F28: mreg | F29: mreg | F30: mreg | F31: mreg
   (** Integer temporaries *)
-  | IT1: mreg (* R11 *) | IT2: mreg (* R0 *)
+  | IT1: mreg (* R11 *) | IT2: mreg (* R12 *)
   (** Float temporaries *)
-  | FT1: mreg (* F11 *) | FT2: mreg (* F12 *) | FT3: mreg (* F0 *).
+  | FT1: mreg (* F0 *) | FT2: mreg (* F12 *) | FT3: mreg (* F13 *).
 
 Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
-Proof. decide equality. Qed.
+Proof. decide equality. Defined.
 
 Definition mreg_type (r: mreg): typ :=
   match r with
@@ -65,7 +66,8 @@ Definition mreg_type (r: mreg): typ :=
   | R29 => Tint | R30 => Tint | R31 => Tint
   | F1 => Tfloat  | F2 => Tfloat  | F3 => Tfloat  | F4 => Tfloat
   | F5 => Tfloat  | F6 => Tfloat  | F7 => Tfloat  | F8 => Tfloat
-  | F9 => Tfloat  | F10 => Tfloat | F14 => Tfloat | F15 => Tfloat
+  | F9 => Tfloat  | F10 => Tfloat | F11 => Tfloat
+  | F14 => Tfloat | F15 => Tfloat
   | F16 => Tfloat | F17 => Tfloat | F18 => Tfloat | F19 => Tfloat
   | F20 => Tfloat | F21 => Tfloat | F22 => Tfloat | F23 => Tfloat
   | F24 => Tfloat | F25 => Tfloat | F26 => Tfloat | F27 => Tfloat
@@ -90,13 +92,14 @@ Module IndexedMreg <: INDEXED_TYPE.
     | R29 => 24 | R30 => 25 | R31 => 26
     | F1 => 28  | F2 => 29  | F3 => 30  | F4 => 31
     | F5 => 32  | F6 => 33  | F7 => 34  | F8 => 35
-    | F9 => 36  | F10 => 37 | F14 => 38 | F15 => 39
-    | F16 => 40 | F17 => 41 | F18 => 42 | F19 => 43
-    | F20 => 44 | F21 => 45 | F22 => 46 | F23 => 47
-    | F24 => 48 | F25 => 49 | F26 => 50 | F27 => 51
-    | F28 => 52 | F29 => 53 | F30 => 54 | F31 => 55
-    | IT1 => 56 | IT2 => 57
-    | FT1 => 58 | FT2 => 59 | FT3 => 60
+    | F9 => 36  | F10 => 37 | F11 => 38
+    | F14 => 39 | F15 => 40
+    | F16 => 41 | F17 => 42 | F18 => 43 | F19 => 44
+    | F20 => 45 | F21 => 46 | F22 => 47 | F23 => 48
+    | F24 => 49 | F25 => 50 | F26 => 51 | F27 => 52
+    | F28 => 53 | F29 => 54 | F30 => 55 | F31 => 56
+    | IT1 => 57 | IT2 => 58
+    | FT1 => 59 | FT2 => 60 | FT3 => 61
     end.
   Lemma index_inj:
     forall r1 r2, index r1 = index r2 -> r1 = r2.
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index 87800be..713e14d 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -24,13 +24,14 @@ let register_names = [
   ("R29", R29); ("R30", R30); ("R31", R31);
   ("F1", F1);  ("F2", F2);  ("F3", F3);  ("F4", F4);
   ("F5", F5);  ("F6", F6);  ("F7", F7);  ("F8", F8);
-  ("F9", F9);  ("F10", F10); ("F14", F14); ("F15", F15);
+  ("F9", F9);  ("F10", F10); ("F11", F11); 
+  ("F14", F14); ("F15", F15);
   ("F16", F16); ("F17", F17); ("F18", F18); ("F19", F19);
   ("F20", F20); ("F21", F21); ("F22", F22); ("F23", F23);
   ("F24", F24); ("F25", F25); ("F26", F26); ("F27", F27);
   ("F28", F28); ("F29", F29); ("F30", F30); ("F31", F31);
-  ("R11", IT1); ("R0", IT2);
-  ("F11", FT1); ("F12", FT2); ("F0", FT3)
+  ("R11", IT1); ("R12", IT2);
+  ("F0", FT1); ("F12", FT2); ("F13", FT3)
 ]
 
 let name_of_register r =
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 7a9aa50..902fc02 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -96,9 +96,7 @@ Inductive operation : Type :=
   | Osingleoffloat: operation           (**r [rd] is [r1] truncated to single-precision float *)
 (*c Conversions between int and float: *)
   | Ointoffloat: operation              (**r [rd = signed_int_of_float(r1)] *)
-  | Ointuoffloat: operation             (**r [rd = unsigned_int_of_float(r1)] *)
-  | Ofloatofint: operation              (**r [rd = float_of_signed_int(r1)] *)
-  | Ofloatofintu: operation             (**r [rd = float_of_unsigned_int(r1)] *)
+  | Ofloatofwords: operation            (**r [rd = float_of_words(r1,r2)] *)
 (*c Boolean tests: *)
   | Ocmp: condition -> operation.       (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
 
@@ -250,12 +248,8 @@ Definition eval_operation
       Some (Val.singleoffloat v1)
   | Ointoffloat, Vfloat f1 :: nil => 
       Some (Vint (Float.intoffloat f1))
-  | Ointuoffloat, Vfloat f1 :: nil => 
-      Some (Vint (Float.intuoffloat f1))
-  | Ofloatofint, Vint n1 :: nil => 
-      Some (Vfloat (Float.floatofint n1))
-  | Ofloatofintu, Vint n1 :: nil => 
-      Some (Vfloat (Float.floatofintu n1))
+  | Ofloatofwords, Vint i1 :: Vint i2 :: nil =>
+      Some (Vfloat (Float.from_words i1 i2))
   | Ocmp c, _ =>
       match eval_condition c vl with
       | None => None
@@ -466,9 +460,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Omulsubf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat)
   | Osingleoffloat => (Tfloat :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
-  | Ointuoffloat => (Tfloat :: nil, Tint)
-  | Ofloatofint => (Tint :: nil, Tfloat)
-  | Ofloatofintu => (Tint :: nil, Tfloat)
+  | Ofloatofwords => (Tint :: Tint :: nil, Tfloat)
   | Ocmp c => (type_of_condition c, Tint)
   end.
 
@@ -615,9 +607,7 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val :
   | Omulsubf, v1::v2::v3::nil => Val.subf (Val.mulf v1 v2) v3
   | Osingleoffloat, v1::nil => Val.singleoffloat v1
   | Ointoffloat, v1::nil => Val.intoffloat v1
-  | Ointuoffloat, v1::nil => Val.intuoffloat v1
-  | Ofloatofint, v1::nil => Val.floatofint v1
-  | Ofloatofintu, v1::nil => Val.floatofintu v1
+  | Ofloatofwords, v1::v2::nil => Val.floatofwords v1 v2
   | Ocmp c, _ => eval_condition_total c vl
   | _, _ => Vundef
   end.
@@ -840,3 +830,73 @@ Lemma type_op_for_binary_addressing:
 Proof.
   intros. destruct addr; simpl in H; reflexivity || omegaContradiction.
 Qed.
+
+(** Two-address operations.  There are none in the PowerPC architecture. *)
+
+Definition two_address_op (op: operation) : bool := false.
+
+(** Operations that are so cheap to recompute that CSE should not factor them out. *)
+
+Definition is_trivial_op (op: operation) : bool :=
+  match op with
+  | Omove => true
+  | Ointconst _ => true
+  | Oaddrsymbol _ _ => true
+  | Oaddrstack _ => true
+  | _ => false
+  end.
+
+(** Shifting stack-relative references.  This is used in [Stacking]. *)
+
+Definition shift_stack_addressing (delta: int) (addr: addressing) :=
+  match addr with
+  | Ainstack ofs => Ainstack (Int.add delta ofs)
+  | _ => addr
+  end.
+
+Definition shift_stack_operation (delta: int) (op: operation) :=
+  match op with
+  | Oaddrstack ofs => Oaddrstack (Int.add delta ofs)
+  | _ => op
+  end.
+
+Lemma shift_stack_eval_addressing:
+  forall (F V: Type) (ge: Genv.t F V) sp addr args delta,
+  eval_addressing ge (Val.sub sp (Vint delta)) (shift_stack_addressing delta addr) args =
+  eval_addressing ge sp addr args.
+Proof.
+  intros. destruct addr; simpl; auto. 
+  destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. 
+  decEq. decEq. rewrite <- Int.add_assoc. decEq. 
+  rewrite Int.sub_add_opp. rewrite Int.add_assoc.
+  rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. 
+  rewrite Int.sub_idem. apply Int.add_zero. 
+Qed.
+
+Lemma shift_stack_eval_operation:
+  forall (F V: Type) (ge: Genv.t F V) sp op args delta,
+  eval_operation ge (Val.sub sp (Vint delta)) (shift_stack_operation delta op) args =
+  eval_operation ge sp op args.
+Proof.
+  intros. destruct op; simpl; auto.
+  destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. 
+  decEq. decEq. rewrite <- Int.add_assoc. decEq. 
+  rewrite Int.sub_add_opp. rewrite Int.add_assoc.
+  rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. 
+  rewrite Int.sub_idem. apply Int.add_zero. 
+Qed.
+
+Lemma type_shift_stack_addressing:
+  forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.
+Proof.
+  intros. destruct addr; auto. 
+Qed.
+
+Lemma type_shift_stack_operation:
+  forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
+Proof.
+  intros. destruct op; auto.
+Qed.
+
+
+
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 9df9cc0..ef50795 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -263,14 +263,15 @@ let rec log2 n =
 
 (* Built-ins.  They come in two flavors: 
    - inlined by the compiler: take their arguments in arbitrary
-     registers; preserve all registers except GPR12 and FPR13
+     registers; preserve all registers except the temporaries
+     (GPR0, GPR11, GPR12,  FPR0, FPR12, FPR13);
    - inlined while printing asm code; take their arguments in
      locations dictated by the calling conventions; preserve
      callee-save regs only. *)
 
 let print_builtin_inlined oc name args res =
   fprintf oc "%s begin builtin %s\n" comment name;
-  (* Can use as temporaries: GPR12, FPR13 *)
+  (* Can use as temporaries: GPR0, GPR11, GPR12,  FPR0, FPR12, FPR13 *)
   begin match name, args, res with
   (* Volatile reads *)
   | "__builtin_volatile_read_int8unsigned", [IR addr], IR res ->
@@ -524,32 +525,18 @@ let print_instruction oc labels = function
       fprintf oc "	lwz	%a, 4(%a)\n" ireg r1 ireg GPR1;
       fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1;
       fprintf oc "%s end pseudoinstr fcti\n" comment
-  | Pfctiu(r1, r2) ->
-      let lbl1 = new_label() in
-      let lbl2 = new_label() in
-      let lbl3 = new_label() in
-      fprintf oc "%s begin pseudoinstr %a = fctiu(%a)\n" comment ireg r1 freg r2;
-      fprintf oc "	addis	%a, 0, %a\n" ireg GPR12  label_high lbl1;
-      fprintf oc "	lfd	%a, %a(%a)\n" freg FPR13  label_low lbl1  ireg GPR12;
-      fprintf oc "	fcmpu	%a, %a, %a\n" creg 7  freg r2  freg FPR13;
-      fprintf oc "	cror	30, 29, 30\n";
-      fprintf oc "	beq	%a, %a\n" creg 7  label lbl2;
-      fprintf oc "	fctiwz	%a, %a\n" freg FPR13  freg r2;
-      fprintf oc "	stfdu	%a, -8(%a)\n" freg FPR13  ireg GPR1;
-      fprintf oc "	lwz	%a, 4(%a)\n" ireg r1  ireg GPR1;
-      fprintf oc "	b	%a\n" label lbl3;
-      fprintf oc "%a:	fsub	%a, %a, %a\n" label lbl2  freg FPR13  freg r2  freg FPR13;
-      fprintf oc "	fctiwz	%a, %a\n" freg FPR13  freg FPR13;
-      fprintf oc "	stfdu	%a, -8(%a)\n" freg FPR13  ireg GPR1;
-      fprintf oc "	lwz	%a, 4(%a)\n" ireg r1  ireg GPR1;
-      fprintf oc "	addis	%a, %a, 0x8000\n" ireg r1 ireg r1;
-      fprintf oc "%a:	addi	%a, %a, 8\n" label lbl3  ireg GPR1  ireg GPR1;
-      float_literals := (lbl1, 0x41e0_0000_0000_0000L) :: !float_literals;
-      fprintf oc "%s end pseudoinstr fctiu\n" comment
   | Pfdiv(r1, r2, r3) ->
       fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
   | Pfmadd(r1, r2, r3, r4) ->
       fprintf oc "	fmadd	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
+  | Pfmake(rd, r1, r2) ->
+      fprintf oc "%s begin pseudoinstr %a = fmake(%a, %a)\n"
+              comment freg rd ireg r1 ireg r2;
+      fprintf oc "	stwu	%a, -8(%a)\n" ireg r1 ireg GPR1;
+      fprintf oc "	stw	%a, 4(%a)\n" ireg r2 ireg GPR1;
+      fprintf oc "	lfd	%a, 0(%a)\n" freg rd ireg GPR1;
+      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1;
+      fprintf oc "%s end pseudoinstr fmake\n" comment
   | Pfmr(r1, r2) ->
       fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
   | Pfmsub(r1, r2, r3, r4) ->
@@ -562,33 +549,6 @@ let print_instruction oc labels = function
       fprintf oc "	frsp	%a, %a\n" freg r1 freg r2
   | Pfsub(r1, r2, r3) ->
       fprintf oc "	fsub	%a, %a, %a\n" freg r1 freg r2 freg r3
-  | Pictf(r1, r2) ->
-      let lbl = new_label() in
-      fprintf oc "%s begin pseudoinstr %a = ictf(%a)\n" comment freg r1 ireg r2;
-      fprintf oc "	addis	%a, 0, 0x4330\n" ireg GPR12;
-      fprintf oc "	stwu	%a, -8(%a)\n" ireg GPR12  ireg GPR1;
-      fprintf oc "	addis	%a, %a, 0x8000\n" ireg GPR12  ireg r2;
-      fprintf oc "	stw	%a, 4(%a)\n" ireg GPR12  ireg GPR1;
-      fprintf oc "	addis	%a, 0, %a\n" ireg GPR12  label_high lbl;
-      fprintf oc "	lfd	%a, %a(%a)\n" freg FPR13  label_low lbl  ireg GPR12;
-      fprintf oc "	lfd	%a, 0(%a)\n" freg r1  ireg GPR1;
-      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1  ireg GPR1;
-      fprintf oc "	fsub	%a, %a, %a\n" freg r1  freg r1  freg FPR13;
-      float_literals := (lbl, 0x4330_0000_8000_0000L) :: !float_literals;
-      fprintf oc "%s end pseudoinstr ictf\n" comment
-  | Piuctf(r1, r2) ->
-      let lbl = new_label() in
-      fprintf oc "%s begin pseudoinstr %a = iuctf(%a)\n" comment freg r1 ireg r2;
-      fprintf oc "	addis	%a, 0, 0x4330\n" ireg GPR12;
-      fprintf oc "	stwu	%a, -8(%a)\n" ireg GPR12  ireg GPR1;
-      fprintf oc "	stw	%a, 4(%a)\n" ireg r2  ireg GPR1;
-      fprintf oc "	addis	%a, 0, %a\n" ireg GPR12  label_high lbl;
-      fprintf oc "	lfd	%a, %a(%a)\n" freg FPR13  label_low lbl  ireg GPR12;
-      fprintf oc "	lfd	%a, 0(%a)\n" freg r1  ireg GPR1;
-      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1  ireg GPR1;
-      fprintf oc "	fsub	%a, %a, %a\n" freg r1  freg r1  freg FPR13;
-      float_literals := (lbl, 0x4330_0000_0000_0000L) :: !float_literals;
-      fprintf oc "%s end pseudoinstr ictf\n" comment
   | Plbz(r1, c, r2) ->
       fprintf oc "	lbz	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Plbzx(r1, r2, r3) ->
diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml
index 31de8d1..4eb95bf 100644
--- a/powerpc/PrintOp.ml
+++ b/powerpc/PrintOp.ml
@@ -92,9 +92,7 @@ let print_operation reg pp = function
   | Omulsubf, [r1;r2;r3] -> fprintf pp "%a *f %a -f %a" reg r1 reg r2 reg r3
   | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1
   | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1
-  | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1
-  | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1
-  | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1
+  | Ofloatofwords, [r1;r2] -> fprintf pp "floatofwords(%a,%a)" reg r1 reg r2
   | Ocmp c, args -> print_condition reg pp (c, args)
   | _ -> fprintf pp "<bad operator>"
 
@@ -105,5 +103,3 @@ let print_addressing reg pp = function
   | Abased(id, ofs), [r1] -> fprintf pp "%s + %ld + %a" (extern_atom id) (camlint_of_coqint ofs) reg r1
   | Ainstack ofs, [] -> fprintf pp "stack(%ld)" (camlint_of_coqint ofs)
   | _ -> fprintf pp "<bad addressing>"
-
-
diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v
index e6a281b..c421cdc 100644
--- a/powerpc/SelectOp.v
+++ b/powerpc/SelectOp.v
@@ -50,6 +50,14 @@ Require Import CminorSel.
 
 Open Local Scope cminorsel_scope.
 
+(** ** Constants **)
+
+Definition addrsymbol (id: ident) (ofs: int) :=
+  Eop (Oaddrsymbol id ofs) Enil.
+
+Definition addrstack (ofs: int) :=
+  Eop (Oaddrstack ofs) Enil.
+
 (** ** Integer logical negation *)
 
 (** The natural way to write smart constructors is by pattern-matching
@@ -846,148 +854,6 @@ Definition subf (e1: expr) (e2: expr) :=
     end
   else Eop Osubf (e1:::e2:::Enil).
 
-(** ** Truncations and sign extensions *)
-
-Inductive cast8signed_cases: forall (e1: expr), Type :=
-  | cast8signed_case1:
-      forall (e2: expr),
-      cast8signed_cases (Eop Ocast8signed (e2 ::: Enil))
-  | cast8signed_case2:
-      forall mode args,
-      cast8signed_cases (Eload Mint8signed mode args)
-  | cast8signed_default:
-      forall (e1: expr),
-      cast8signed_cases e1.
-
-Definition cast8signed_match (e1: expr) :=
-  match e1 as z1 return cast8signed_cases z1 with
-  | Eop Ocast8signed (e2 ::: Enil) =>
-      cast8signed_case1 e2
-  | Eload Mint8signed mode args =>
-      cast8signed_case2 mode args
-  | e1 =>
-      cast8signed_default e1
-  end.
-
-Definition cast8signed (e: expr) := 
-  match cast8signed_match e with
-  | cast8signed_case1 e1 => e
-  | cast8signed_case2 mode args => e
-  | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil)
-  end.
-
-Inductive cast8unsigned_cases: forall (e1: expr), Type :=
-  | cast8unsigned_case1:
-      forall (e2: expr),
-      cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil))
-  | cast8unsigned_case2:
-      forall mode args,
-      cast8unsigned_cases (Eload Mint8unsigned mode args)
-  | cast8unsigned_default:
-      forall (e1: expr),
-      cast8unsigned_cases e1.
-
-Definition cast8unsigned_match (e1: expr) :=
-  match e1 as z1 return cast8unsigned_cases z1 with
-  | Eop Ocast8unsigned (e2 ::: Enil) =>
-      cast8unsigned_case1 e2
-  | Eload Mint8unsigned mode args =>
-      cast8unsigned_case2 mode args
-  | e1 =>
-      cast8unsigned_default e1
-  end.
-
-Definition cast8unsigned (e: expr) := 
-  match cast8unsigned_match e with
-  | cast8unsigned_case1 e1 => e
-  | cast8unsigned_case2 mode args => e
-  | cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil)
-  end.
-
-Inductive cast16signed_cases: forall (e1: expr), Type :=
-  | cast16signed_case1:
-      forall (e2: expr),
-      cast16signed_cases (Eop Ocast16signed (e2 ::: Enil))
-  | cast16signed_case2:
-      forall mode args,
-      cast16signed_cases (Eload Mint16signed mode args)
-  | cast16signed_default:
-      forall (e1: expr),
-      cast16signed_cases e1.
-
-Definition cast16signed_match (e1: expr) :=
-  match e1 as z1 return cast16signed_cases z1 with
-  | Eop Ocast16signed (e2 ::: Enil) =>
-      cast16signed_case1 e2
-  | Eload Mint16signed mode args =>
-      cast16signed_case2 mode args
-  | e1 =>
-      cast16signed_default e1
-  end.
-
-Definition cast16signed (e: expr) := 
-  match cast16signed_match e with
-  | cast16signed_case1 e1 => e
-  | cast16signed_case2 mode args => e
-  | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil)
-  end.
-
-Inductive cast16unsigned_cases: forall (e1: expr), Type :=
-  | cast16unsigned_case1:
-      forall (e2: expr),
-      cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil))
-  | cast16unsigned_case2:
-      forall mode args,
-      cast16unsigned_cases (Eload Mint16unsigned mode args)
-  | cast16unsigned_default:
-      forall (e1: expr),
-      cast16unsigned_cases e1.
-
-Definition cast16unsigned_match (e1: expr) :=
-  match e1 as z1 return cast16unsigned_cases z1 with
-  | Eop Ocast16unsigned (e2 ::: Enil) =>
-      cast16unsigned_case1 e2
-  | Eload Mint16unsigned mode args =>
-      cast16unsigned_case2 mode args
-  | e1 =>
-      cast16unsigned_default e1
-  end.
-
-Definition cast16unsigned (e: expr) := 
-  match cast16unsigned_match e with
-  | cast16unsigned_case1 e1 => e
-  | cast16unsigned_case2 mode args => e
-  | cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil)
-  end.
-
-Inductive singleoffloat_cases: forall (e1: expr), Type :=
-  | singleoffloat_case1:
-      forall (e2: expr),
-      singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil))
-  | singleoffloat_case2:
-      forall mode args,
-      singleoffloat_cases (Eload Mfloat32 mode args)
-  | singleoffloat_default:
-      forall (e1: expr),
-      singleoffloat_cases e1.
-
-Definition singleoffloat_match (e1: expr) :=
-  match e1 as z1 return singleoffloat_cases z1 with
-  | Eop Osingleoffloat (e2 ::: Enil) =>
-      singleoffloat_case1 e2
-  | Eload Mfloat32 mode args =>
-      singleoffloat_case2 mode args
-  | e1 =>
-      singleoffloat_default e1
-  end.
-
-Definition singleoffloat (e: expr) := 
-  match singleoffloat_match e with
-  | singleoffloat_case1 e1 => e
-  | singleoffloat_case2 mode args => e
-  | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil)
-  end.
-
 (** ** Comparisons *)
 
 Inductive comp_cases: forall (e1: expr) (e2: expr), Type :=
@@ -1034,15 +900,36 @@ Definition compu (c: comparison) (e1: expr) (e2: expr) :=
 Definition compf (c: comparison) (e1: expr) (e2: expr) :=
   Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).
 
+(** ** Floating-point conversions *)
+
+Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
+
+Definition intuoffloat (e: expr) :=
+  let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in
+  Elet e
+    (Econdition (CEcond (Ccompf Clt) (Eletvar O ::: f ::: Enil))
+      (intoffloat (Eletvar O))
+      (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar O) f)))).
+
+Definition floatofintu (e: expr) :=
+  subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
+       (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
+
+Definition floatofint (e: expr) :=
+  subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
+                           ::: addimm Float.ox8000_0000 e ::: Enil))
+       (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
+
 (** ** Other operators, not optimized. *)
 
+Definition cast8unsigned (e: expr) := Eop Ocast8unsigned (e ::: Enil).
+Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil).
+Definition cast16unsigned (e: expr) := Eop Ocast16unsigned (e ::: Enil).
+Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil).
+Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
 Definition negint (e: expr) := Eop (Osubimm Int.zero) (e ::: Enil).
 Definition negf (e: expr) :=  Eop Onegf (e ::: Enil).
 Definition absf (e: expr) :=  Eop Oabsf (e ::: Enil).
-Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
-Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil).
-Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil).
-Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil).
 Definition xor (e1 e2: expr) :=  Eop Oxor (e1 ::: e2 ::: Enil).
 Definition shr (e1 e2: expr) :=  Eop Oshr (e1 ::: e2 ::: Enil).
 Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 2fc1327..8a06433 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -100,6 +100,24 @@ Ltac InvEval := InvEval1; InvEval2; InvEval2.
   by the smart constructor.
 *)
 
+Theorem eval_addrsymbol:
+  forall le id ofs b,
+  Genv.find_symbol ge id = Some b ->
+  eval_expr ge sp e m le (addrsymbol id ofs) (Vptr b ofs).
+Proof.
+  intros. unfold addrsymbol. econstructor. constructor. 
+  simpl. rewrite H. auto.
+Qed.
+
+Theorem eval_addrstack:
+  forall le ofs b n,
+  sp = Vptr b n ->
+  eval_expr ge sp e m le (addrstack ofs) (Vptr b (Int.add n ofs)).
+Proof.
+  intros. unfold addrstack. econstructor. constructor. 
+  simpl. unfold offset_sp. rewrite H. auto.
+Qed.
+
 Theorem eval_notint:
   forall le a x,
   eval_expr ge sp e m le a (Vint x) ->
@@ -667,80 +685,35 @@ Proof.
   intros. EvalOp.
 Qed.
 
-Lemma loadv_cast:
-  forall chunk addr v,
-  Mem.loadv chunk m addr = Some v ->
-  match chunk with
-  | Mint8signed => v = Val.sign_ext 8 v
-  | Mint8unsigned => v = Val.zero_ext 8 v
-  | Mint16signed => v = Val.sign_ext 16 v
-  | Mint16unsigned => v = Val.zero_ext 16 v
-  | Mfloat32 => v = Val.singleoffloat v
-  | _ => True
-  end.
-Proof.
-  intros. destruct addr; simpl in H; try discriminate.
-  eapply Mem.load_cast. eauto.
-Qed.
-
 Theorem eval_cast8signed:
   forall le a v,
   eval_expr ge sp e m le a v ->
   eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v).
-Proof. 
-  intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto.
-  rewrite Int.sign_ext_idem. reflexivity. compute; auto.
-  inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). 
-  EvalOp.
-Qed.
+Proof. TrivialOp cast8signed. Qed.
 
 Theorem eval_cast8unsigned:
   forall le a v,
   eval_expr ge sp e m le a v ->
   eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v).
-Proof. 
-  intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto.
-  rewrite Int.zero_ext_idem. reflexivity. compute; auto.
-  inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). 
-  EvalOp.
-Qed.
+Proof. TrivialOp cast8unsigned. Qed.
 
 Theorem eval_cast16signed:
   forall le a v,
   eval_expr ge sp e m le a v ->
   eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v).
-Proof. 
-  intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto.
-  rewrite Int.sign_ext_idem. reflexivity. compute; auto.
-  inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). 
-  EvalOp.
-Qed.
+Proof. TrivialOp cast16signed. Qed.
 
 Theorem eval_cast16unsigned:
   forall le a v,
   eval_expr ge sp e m le a v ->
   eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v).
-Proof. 
-  intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto.
-  rewrite Int.zero_ext_idem. reflexivity. compute; auto.
-  inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). 
-  EvalOp.
-Qed.
+Proof. TrivialOp cast16unsigned. Qed.
 
 Theorem eval_singleoffloat:
   forall le a v,
   eval_expr ge sp e m le a v ->
   eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v).
-Proof. 
-  intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity.
-  inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). 
-  EvalOp.
-Qed.
+Proof. TrivialOp singleoffloat. Qed.
 
 Theorem eval_comp_int:
   forall le c a x b y,
@@ -883,19 +856,46 @@ Theorem eval_intuoffloat:
   forall le a x,
   eval_expr ge sp e m le a (Vfloat x) ->
   eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)).
-Proof. intros; unfold intuoffloat; EvalOp. Qed.
+Proof.
+  intros. unfold intuoffloat. 
+  econstructor. eauto. 
+  set (fm := Float.floatofintu Float.ox8000_0000).
+  assert (eval_expr ge sp e m (Vfloat x :: le) (Eletvar O) (Vfloat x)). constructor. auto. 
+  apply eval_Econdition with (v1 := Float.cmp Clt x fm).
+  econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
+  simpl. auto.
+  caseEq (Float.cmp Clt x fm); intros.
+  rewrite Float.intuoffloat_intoffloat_1; auto.
+  EvalOp.
+  rewrite Float.intuoffloat_intoffloat_2; auto.
+  apply eval_addimm. apply eval_intoffloat. apply eval_subf; auto. EvalOp.
+Qed.
 
 Theorem eval_floatofint:
   forall le a x,
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)).
-Proof. intros; unfold floatofint; EvalOp. Qed.
+Proof.
+  intros. unfold floatofint. rewrite Float.floatofint_from_words.
+  apply eval_subf.
+  EvalOp. constructor. EvalOp. simpl; eauto.
+  constructor. apply eval_addimm. eauto. constructor.
+  simpl. auto. 
+  EvalOp. 
+Qed.
 
 Theorem eval_floatofintu:
   forall le a x,
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)).
-Proof. intros; unfold floatofintu; EvalOp. Qed.
+Proof.
+  intros. unfold floatofintu. rewrite Float.floatofintu_from_words.
+  apply eval_subf.
+  EvalOp. constructor. EvalOp. simpl; eauto.
+  constructor. eauto. constructor.
+  simpl. auto. 
+  EvalOp. 
+Qed.
 
 Theorem eval_xor:
   forall le a x b y,
diff --git a/powerpc/eabi/Conventions1.v b/powerpc/eabi/Conventions1.v
index 60eaaa5..b25f2a5 100644
--- a/powerpc/eabi/Conventions1.v
+++ b/powerpc/eabi/Conventions1.v
@@ -35,7 +35,7 @@ Definition int_caller_save_regs :=
   R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: nil.
 
 Definition float_caller_save_regs :=
-  F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: nil.
+  F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: F11 :: nil.
 
 Definition int_callee_save_regs :=
   R31 :: R30 :: R29 :: R28 :: R27 :: R26 :: R25 :: R24 :: R23 ::
@@ -58,6 +58,9 @@ Definition float_temporaries := FT1 :: FT2 :: FT3 :: nil.
 Definition temporaries := 
   R IT1 :: R IT2 :: R FT1 :: R FT2 :: R FT3 :: nil.
 
+Definition dummy_int_reg := R3.     (**r Used in [Coloring]. *)
+Definition dummy_float_reg := F1.   (**r Used in [Coloring]. *)
+
 (** The [index_int_callee_save] and [index_float_callee_save] associate
   a unique positive integer to callee-save registers.  This integer is
   used in [Stacking] to determine where to save these registers in
diff --git a/powerpc/macosx/Conventions1.v b/powerpc/macosx/Conventions1.v
index a5741e1..2a0f233 100644
--- a/powerpc/macosx/Conventions1.v
+++ b/powerpc/macosx/Conventions1.v
@@ -35,7 +35,7 @@ Definition int_caller_save_regs :=
   R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: nil.
 
 Definition float_caller_save_regs :=
-  F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: nil.
+  F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: F11 :: nil.
 
 Definition int_callee_save_regs :=
   R14 :: R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 :: 
@@ -58,6 +58,9 @@ Definition float_temporaries := FT1 :: FT2 :: FT3 :: nil.
 Definition temporaries := 
   R IT1 :: R IT2 :: R FT1 :: R FT2 :: R FT3 :: nil.
 
+Definition dummy_int_reg := R3.     (**r Used in [Coloring]. *)
+Definition dummy_float_reg := F1.   (**r Used in [Coloring]. *)
+
 (** The [index_int_callee_save] and [index_float_callee_save] associate
   a unique positive integer to callee-save registers.  This integer is
   used in [Stacking] to determine where to save these registers in
@@ -291,7 +294,7 @@ Qed.
 (** The PowerPC ABI states the following convention for passing arguments
   to a function:
 - The first 8 integer arguments are passed in registers [R3] to [R10].
-- The first 10 float arguments are passed in registers [F1] to [F10].
+- The first 11 float arguments are passed in registers [F1] to [F11].
 - Each float argument passed in a float register ``consumes'' two
   integer arguments.
 - Extra arguments are passed on the stack, in [Outgoing] slots, consecutively
@@ -327,7 +330,7 @@ Fixpoint loc_arguments_rec
 Definition int_param_regs :=
   R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: nil.
 Definition float_param_regs :=
-  F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: nil.
+  F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: F11 :: nil.
 
 (** [loc_arguments s] returns the list of locations where to store arguments
   when calling a function with signature [s].  *)
@@ -589,4 +592,3 @@ Proof.
   intro; simpl. ElimOrEq; reflexivity.
   intro; simpl. ElimOrEq; reflexivity.
 Qed.
-