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

11 files changed, 966 insertions, 977 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index d160be78..7ea1a8a3 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -152,9 +152,7 @@ Inductive instruction : Type :=
   | Pcmf: freg -> freg -> instruction              (**r float comparison *)
   | Pdvfd: freg -> freg -> freg -> instruction     (**r float division *)
   | Pfixz: ireg -> freg -> instruction             (**r float to signed int *)
-  | Pfixzu: ireg -> freg -> instruction            (**r float to unsigned int *)
   | Pfltd: freg -> ireg -> instruction             (**r signed int to float *)
-  | Pfltud: freg -> ireg -> instruction             (**r unsigned int to float *)
   | Pldfd: freg -> ireg -> int -> instruction      (**r float64 load *)
   | Pldfs: freg -> ireg -> int -> instruction      (**r float32 load *)
   | Plifd: freg -> float -> instruction            (**r load float constant *)
@@ -470,12 +468,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (rs#r1 <- (Val.divf rs#r2 rs#r3))) m
   | Pfixz r1 r2 =>
       OK (nextinstr (rs#r1 <- (Val.intoffloat rs#r2))) m
-  | Pfixzu r1 r2 =>
-      OK (nextinstr (rs#r1 <- (Val.intuoffloat rs#r2))) m
   | Pfltd r1 r2 =>
       OK (nextinstr (rs#r1 <- (Val.floatofint rs#r2))) m
-  | Pfltud r1 r2 =>
-      OK (nextinstr (rs#r1 <- (Val.floatofintu rs#r2))) m
   | Pldfd r1 r2 n =>
       exec_load Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m
   | Pldfs r1 r2 n =>
@@ -492,8 +486,11 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (rs#r1 <- (Val.mulf rs#r2 rs#r3))) m
   | Pstfd r1 r2 n =>      
       exec_store Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m
-  | Pstfs r1 r2 n =>      
-      exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m
+  | Pstfs r1 r2 n =>
+      match exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m with
+      | OK rs' m' => OK (rs'#FR3 <- Vundef) m'
+      | Error => Error
+      end
   | Psufd r1 r2 r3 =>     
       OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m
   (* Pseudo-instructions *)
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 775bb37f..b3412fbf 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -300,12 +300,8 @@ Definition transl_op
       Pmvfs (freg_of r) (freg_of a1) :: k
   | Ointoffloat, a1 :: nil =>
       Pfixz (ireg_of r) (freg_of a1) :: k
-  | Ointuoffloat, a1 :: nil =>
-      Pfixzu (ireg_of r) (freg_of a1) :: k
   | Ofloatofint, a1 :: nil =>
       Pfltd (freg_of r) (ireg_of a1) :: k
-  | Ofloatofintu, a1 :: nil =>
-      Pfltud (freg_of r) (ireg_of a1) :: k
   | Ocmp cmp, _ =>
       transl_cond cmp args
         (Pmov (ireg_of r) (SOimm Int.zero) ::
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index cc4d7ac5..d3e082f0 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -558,56 +558,84 @@ 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 f m'
         (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)
         (ATPC: rs PC = Vptr fb Int.zero)
-        (ATLR: rs IR14 = parent_ra s),
+        (ATLR: rs IR14 = parent_ra s)
+        (MEXT: Mem.extends m m'),
       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)
-        (ATPC: rs PC = parent_ra s),
+        (ATPC: rs PC = parent_ra s)
+        (MEXT: Mem.extends m m'),
       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 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 rs2,
-     exec_straight tge (transl_function f) (transl_code f c1) rs1 m1 (transl_code f c2) rs2 m2
+  Mem.extends m1 m1' ->
+  (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' /\
+  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.
+  intros. destruct H5 as [m2' [A [rs2 [B C]]]].
+  exists (State rs2 m2'); split.
   eapply exec_straight_exec; eauto.
   econstructor; eauto. eapply exec_straight_at; 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 ARM side.  Actually, all Mach transitions
@@ -642,6 +670,7 @@ Lemma exec_Mlabel_prop:
 Proof.
   intros; red; intros; inv MS.
   left; eapply exec_straight_steps; eauto with coqlib.
+  exists m'; split; auto.
   exists (nextinstr rs); split.
   simpl. apply exec_straight_one. reflexivity. reflexivity.
   apply agree_nextinstr; auto.
@@ -658,18 +687,15 @@ Proof.
   intros; red; intros; inv MS.
   unfold load_stack in H. 
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inversion WTI.
-  rewrite (sp_val _ _ _ AG) in H.
-  generalize (loadind_correct tge (transl_function f) IR13 ofs ty
-                dst (transl_code f c) rs m v H H1).
+  intro WTI. inv WTI.
+  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
+  rewrite (sp_val _ _ _ AG) in A.
+  exploit loadind_correct. eexact A. reflexivity. 
   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).
-  auto with ppcgen. 
-  intros. case (preg_eq r0 (preg_of dst)); intro.
-  subst r0. rewrite Pregmap.gss. auto. 
-  rewrite Pregmap.gso; auto.
+  exists m'; split; auto.
+  simpl. exists rs2; split. eauto. 
+  apply agree_set_mreg with rs; auto. congruence. auto with ppcgen. 
 Qed.
 
 Lemma exec_Msetstack_prop:
@@ -683,16 +709,16 @@ 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: IR13 <> IR14) by congruence.
-  generalize (storeind_correct tge (transl_function f) IR13 ofs ty
-                src (transl_code f c) rs m m' H H1 NOTE).
+  intro WTI. inv WTI.
+  exploit preg_val; eauto. instantiate (1 := src). intros A.
+  exploit Mem.storev_extends; eauto. intros [m2 [B C]].
+  rewrite (sp_val _ _ _ AG) in B.
+  exploit storeind_correct. eexact B. reflexivity. congruence.
   intros [rs2 [EX OTH]].
   left; eapply exec_straight_steps; eauto with coqlib.
-  exists rs2; split; auto.
-  apply agree_exten_2 with rs; auto.
+  exists m2; split; auto.
+  exists rs2; split; eauto.
+  apply agree_exten with rs; auto with ppcgen.
 Qed.
 
 Lemma exec_Mgetparam_prop:
@@ -703,29 +729,33 @@ 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.
+  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
+  intro WTI. inv WTI. auto.
+  unfold load_stack in *.
+  exploit Mem.loadv_extends. eauto. eexact H0. eauto. 
+  intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+  assert (parent' = parent). inv B. auto. simpl in H1; discriminate. subst parent'.
+  exploit Mem.loadv_extends. eauto. eexact H1. eauto. 
+  intros [v' [C D]]. 
   exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_link_ofs) IR14
-                 rs m parent (loadind IR14 ofs ty dst (transl_code f c))).
-  rewrite <- (sp_val ms sp rs); auto. 
+                 rs m' parent (loadind IR14 ofs (mreg_type dst) dst (transl_code f c))).
+  auto.
   intros [rs1 [EX1 [RES1 OTH1]]].
-  exploit (loadind_correct tge (transl_function f) IR14 ofs ty dst
-                (transl_code f c) rs1 m v).
-  rewrite RES1. auto. 
-  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
-  intro WTI. inversion WTI. auto.
+  exploit (loadind_correct tge (transl_function f) IR14 ofs (mreg_type dst) dst
+                (transl_code f c) rs1 m' v').
+  rewrite RES1. auto. auto. 
   intros [rs2 [EX2 [RES2 OTH2]]].
   left. eapply exec_straight_steps; eauto with coqlib.
+  exists m'; split; auto.
   exists rs2; split; simpl.
   eapply exec_straight_trans; eauto.
-  apply agree_exten_2 with (rs1#(preg_of dst) <- v).
-  apply agree_set_mreg. 
-  apply agree_exten_2 with rs; auto. 
-  intros. case (preg_eq r (preg_of dst)); intro.
-  subst r. rewrite Pregmap.gss. auto. 
-  rewrite Pregmap.gso; auto. 
+  apply agree_set_mreg with rs1. 
+  apply agree_set_mreg with rs. auto. auto. auto with ppcgen. 
+  congruence. auto with ppcgen.
 Qed.
 
 Lemma exec_Mop_prop:
@@ -734,14 +764,27 @@ 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 _ _))).
   intro WTI.
+  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. 
+  intros [v' [A B]]. 
+  assert (C: eval_operation tge sp op rs ## (preg_of ## args) = Some v').
+    rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
+  rewrite (sp_val _ _ _ AG) in C.
+  exploit transl_op_correct; eauto. intros [rs' [P [Q R]]].
   left; eapply exec_straight_steps; eauto with coqlib.
-  simpl. eapply transl_op_correct; auto.
-  rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
+  exists m'; split; auto.
+  exists rs'; split. simpl. eexact P. 
+  assert (agree (Regmap.set res v ms) sp rs').
+    apply agree_set_mreg with rs; auto. congruence. 
+    auto with ppcgen.
+  assert (agree (Regmap.set res v (undef_temps ms)) sp rs').
+    apply agree_set_undef_mreg with rs; auto. congruence. 
+    auto with ppcgen.
+  destruct op; assumption.
 Qed.
 
 Lemma exec_Mload_prop:
@@ -752,7 +795,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 _ _))).
@@ -760,12 +803,14 @@ Proof.
   assert (eval_addressing tge sp addr ms##args = Some a).
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
   left; eapply exec_straight_steps; eauto with coqlib.
+  exists m'; split; auto.
   destruct chunk; simpl; simpl in H6;
   (eapply transl_load_int_correct || eapply transl_load_float_correct);
   eauto; intros; reflexivity.
 Qed.
 
-Lemma storev_8_signed_unsigned:
  forall m a v,
  Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto.
  apply Mem.store_signed_unsigned_8.
Qed.

Lemma storev_16_signed_unsigned:
  forall m a v,
  Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto.
  apply Mem.store_signed_unsigned_16.
Qed.

+Lemma storev_8_signed_unsigned:
  forall m a v,
  Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto.
  apply Mem.store_signed_unsigned_8.
Qed.

Lemma storev_16_signed_unsigned:
  forall m a v,
  Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto.
  apply Mem.store_signed_unsigned_16.
Qed.
+

 Lemma exec_Mstore_prop:
   forall (s : list stackframe) (fb : block) (sp : val)
          (chunk : memory_chunk) (addr : addressing) (args : list mreg)
@@ -774,7 +819,7 @@ 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 _ _))).
@@ -788,6 +833,7 @@ Proof.
   simpl;
   (eapply transl_store_int_correct || eapply transl_store_float_correct);
   eauto; intros; simpl; auto.
+  econstructor; split. rewrite H2. eauto. intros. apply Pregmap.gso; auto.
 Qed.
 
 Lemma exec_Mcall_prop:
@@ -817,17 +863,20 @@ Proof.
     rewrite RA_EQ.
     change (rs2 IR14) with (Val.add (rs PC) Vone).
     rewrite <- H2. reflexivity. 
-  assert (AG3: agree ms sp rs2). 
-    unfold rs2; auto 8 with ppcgen.
-  left; exists (State rs2 m); split.
+  assert (AG3: agree ms sp rs2).
+    unfold rs2. apply agree_set_other; auto. apply agree_set_other; auto.
+  left; exists (State rs2 m'); split.
   apply plus_one.
     destruct ros; simpl in H5.
     econstructor. eauto. apply functions_transl. eexact H0. 
     eapply find_instr_tail. eauto.
-    simpl. rewrite <- (ireg_val ms sp rs); auto.
-    simpl in H. destruct (ms m0); try congruence. 
-    generalize H; predSpec Int.eq Int.eq_spec i Int.zero; intros; inv H7.
-    auto.
+    simpl.
+    assert (rs (ireg_of m0) = Vptr f' Int.zero).
+      generalize (ireg_val _ _ _ m0 AG H3). intro LD. simpl in H. inv LD. 
+      destruct (ms m0); try congruence.
+      generalize H. predSpec Int.eq Int.eq_spec i Int.zero; congruence.
+      rewrite <- H7 in H; congruence.
+    rewrite H6. auto.
     econstructor. eauto. apply functions_transl. eexact H0. 
     eapply find_instr_tail. eauto.
     simpl. unfold symbol_offset. rewrite symbols_preserved. 
@@ -835,8 +884,19 @@ Proof.
   econstructor; eauto.
   econstructor; eauto with coqlib.
   rewrite RA_EQ. econstructor; eauto.
+  eapply agree_sp_def; eauto. congruence.
 Qed.
 
+Lemma agree_change_sp:
+  forall ms sp rs sp',
+  agree ms sp rs -> sp' <> Vundef ->
+  agree ms sp' (rs#IR13 <- sp').
+Proof.
+  intros. inv H. split. apply Pregmap.gss. auto. 
+  intros. rewrite Pregmap.gso; auto with ppcgen.
+Qed.
+
+
 Lemma exec_Mtailcall_prop:
  forall (s : list stackframe) (fb stk : block) (soff : int)
         (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
         (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m',
  find_function_ptr ge ros ms = Some f' ->
  Genv.find_funct_ptr ge fb = Some (Internal f) ->
  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
  Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
  exec_instr_prop
          (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
          (Callstate s f' ms m').
Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -848,23 +908,31 @@ Lemma exec_Mtailcall_prop:
  forall (s : list stackframe) (fb stk : block) (soff
               loadind_int IR13 (fn_retaddr_ofs f) IR14
                 (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)).
   unfold call_instr; destruct ros; auto.
+  unfold load_stack in *.
+  exploit Mem.loadv_extends. eauto. eexact H1. auto. 
+  intros [parent' [A B]]. 
+  exploit lessdef_parent_sp; eauto. intros. subst parent'.
+  exploit Mem.loadv_extends. eauto. eexact H2. auto. 
+  intros [ra' [C D]].
+  exploit lessdef_parent_ra; eauto. intros. subst ra'.
+  exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
   destruct (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14
-                rs m (parent_ra s) 
+                rs m'0 (parent_ra s) 
                 (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c))
   as [rs1 [EXEC1 [RES1 OTH1]]].
   rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
   set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))).
   assert (EXEC2: exec_straight tge (transl_function f)
-                   (transl_code f (Mtailcall sig ros :: c)) rs m
-                   (call_instr :: transl_code f c) rs2 m').
+                   (transl_code f (Mtailcall sig ros :: c)) rs m'0
+                   (call_instr :: transl_code f c) rs2 m2').
   rewrite TR. eapply exec_straight_trans. eexact EXEC1.
   apply exec_straight_one. simpl.
   rewrite OTH1; auto with ppcgen. 
   rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
-  unfold load_stack in H1. simpl in H1. simpl. rewrite H1.
-  rewrite H3. auto. auto.
+  simpl chunk_of_type in A. rewrite A.
+  rewrite P. auto. auto. 
   set (rs3 := rs2#PC <- (Vptr f' Int.zero)).
-  left. exists (State rs3 m'); split.
+  left. exists (State rs3 m2'); split.
   (* Execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   inv AT. exploit exec_straight_steps_2; eauto. 
@@ -877,24 +945,19 @@ Lemma exec_Mtailcall_prop:
  forall (s : list stackframe) (fb stk : block) (soff
   replace (rs2 (ireg_of m0)) with (Vptr f' Int.zero). auto.
   unfold rs2. rewrite nextinstr_inv; auto with ppcgen. 
   rewrite Pregmap.gso. rewrite OTH1; auto with ppcgen.
-  rewrite <- (ireg_val ms (Vptr stk soff) rs); auto. 
-  destruct (ms m0); try discriminate.
-  generalize H. predSpec Int.eq Int.eq_spec i Int.zero; intros; inv H10.
-  auto.
-  decEq. auto with ppcgen. decEq. auto with ppcgen. decEq. auto with ppcgen.
-  replace (symbol_offset tge i Int.zero) with (Vptr f' Int.zero). auto.
-  unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto.
+  generalize (ireg_val _ _ _ m0 AG H7). intro LD. inv LD. 
+  destruct (ms m0); try congruence.
+  generalize H. predSpec Int.eq Int.eq_spec i Int.zero; congruence.
+  rewrite <- H10 in H; congruence.
+  auto with ppcgen.
+  unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. 
   traceEq.
   (* Match states *)
   constructor; auto.
-  assert (AG1: agree ms (Vptr stk soff) rs1).
-    eapply agree_exten_2; eauto.
-  assert (AG2: agree ms (parent_sp s) rs2).
-    inv AG1. constructor. auto. intros. unfold rs2. 
-    rewrite nextinstr_inv; auto with ppcgen.
-    rewrite Pregmap.gso. auto. auto with ppcgen. 
-  unfold rs3. apply agree_exten_2 with rs2; auto. 
-  intros. rewrite Pregmap.gso; auto.
+  unfold rs3. apply agree_set_other; auto. 
+  unfold rs2. apply agree_nextinstr. apply agree_change_sp with (Vptr stk soff).
+  apply agree_exten with rs; auto with ppcgen. 
+  apply parent_sp_def. auto.
 Qed.
 
 Lemma exec_Mbuiltin_prop:
@@ -904,28 +967,29 @@ 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 _ _))).
   intro WTI. inv WTI.
+  exploit external_call_mem_extends; eauto. eapply preg_vals; eauto.
+  intros [vres' [m2' [A [B [C D]]]]].
   inv AT. simpl in H3.
   generalize (functions_transl _ _ FIND); intro FN.
   generalize (functions_transl_no_overflow _ _ FIND); intro NOOV.
   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 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. 
+  eapply external_call_symbols_preserved; eauto. 
+  eexact symbols_preserved. eexact varinfo_preserved.
   econstructor; eauto with coqlib.
   unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso.
   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. eapply agree_set_undef_mreg; eauto. 
+  rewrite Pregmap.gss; auto. 
+  intros. rewrite Pregmap.gso; auto.
 Qed.
 
 Lemma exec_Mgoto_prop:
@@ -940,16 +1004,16 @@ 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.
   simpl; auto.
   econstructor; eauto.
   eapply Mach.find_label_incl; eauto.
-  apply agree_exten_2 with rs; auto. 
+  apply agree_exten with rs; auto with ppcgen.
 Qed.
 
 Lemma exec_Mcond_true_prop:
@@ -961,32 +1025,32 @@ 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 _ _))).
   intro WTI. inv WTI.
-  pose (k1 := Pbc (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).
-  simpl. intros [rs2 [EX [RES AG2]]].
+  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A.
+  exploit transl_cond_correct. eauto. eauto. 
+  intros [rs2 [EX [RES OTH]]].
   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.
   econstructor; eauto.
-  eapply find_instr_tail. unfold k1 in CT2. eauto.
+  eapply find_instr_tail. eauto.
   simpl. rewrite RES. simpl. auto.
   traceEq.
   econstructor; eauto. 
   eapply Mach.find_label_incl; eauto.
-  apply agree_exten_2 with rs2; auto. 
+  apply agree_exten_temps with rs; auto. intros. 
+  rewrite INV3; auto with ppcgen. 
 Qed.
 
 Lemma exec_Mcond_false_prop:
@@ -995,36 +1059,34 @@ 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 _ _))).
-  intro WTI. inversion WTI.
-  pose (k1 := Pbc (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).
-  simpl. intros [rs2 [EX [RES AG2]]].
+  intro WTI. inv WTI.
+  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A.
+  exploit transl_cond_correct. eauto. eauto. 
+  intros [rs2 [EX [RES OTH]]].
   left; eapply exec_straight_steps; eauto with coqlib.
+  exists m'; split; auto.
   exists (nextinstr rs2); split.
   simpl. eapply exec_straight_trans. eexact EX. 
-  unfold k1; apply exec_straight_one. 
-  simpl. rewrite RES. reflexivity.
-  reflexivity.
-  auto with ppcgen.
+  apply exec_straight_one. simpl. rewrite RES. reflexivity. reflexivity.
+  apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen.
 Qed.
 
 Lemma exec_Mjumptable_prop:
   forall (s : list stackframe) (fb : block) (f : function) (sp : val)
          (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction)
-         (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label)
+         (ms : mreg -> val) (m : mem) (n : int) (lbl : Mach.label)
          (c' : Mach.code),
-  rs arg = Vint n ->
+  ms arg = Vint n ->
   list_nth_z tbl (Int.signed n) = Some lbl ->
   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 (Mjumptable arg tbl :: c) rs m) E0
-    (Machconcr.State s fb sp c' rs m).
+    (Machconcr.State s fb sp (Mjumptable arg tbl :: c) ms m) E0
+    (Machconcr.State s fb sp c' (undef_temps ms) m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -1039,19 +1101,21 @@ Proof.
     omega.
   inv AT. simpl in H7. 
   set (k1 := Pbtbl IR14 tbl :: transl_code f c).
-  set (rs1 := nextinstr (rs0 # IR14 <- (Vint (Int.shl n (Int.repr 2))))).
+  set (rs1 := nextinstr (rs # IR14 <- (Vint (Int.shl n (Int.repr 2))))).
   generalize (functions_transl _ _ H4); intro FN.
   generalize (functions_transl_no_overflow _ _ H4); intro NOOV.
+  assert (rs (ireg_of arg) = Vint n).
+    exploit ireg_val; eauto. intros LD. inv LD. auto. congruence.
   assert (exec_straight tge (transl_function f)
-            (Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) :: k1) rs0 m
-            k1 rs1 m).
+            (Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) :: k1) rs m'
+            k1 rs1 m').
    apply exec_straight_one. 
-   simpl. rewrite <- (ireg_val _ _ _ _ AG H5). rewrite H. reflexivity. reflexivity. 
+   simpl. rewrite H8. reflexivity. reflexivity. 
   exploit exec_straight_steps_2; eauto. 
   intros [ofs' [PC1 CT1]].
-  generalize (find_label_goto_label f lbl rs1 m _ _ _ FIND PC1 H2).
+  generalize (find_label_goto_label f lbl rs1 m' _ _ _ FIND PC1 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. 
@@ -1064,15 +1128,25 @@ Opaque Zmod.  Opaque Zdiv.
   change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq.
   econstructor; eauto. 
   eapply Mach.find_label_incl; eauto.
-  apply agree_exten_2 with rs1; auto. 
+  apply agree_exten with rs1; auto with ppcgen.
   unfold rs1. apply agree_nextinstr. apply agree_set_other; auto with ppcgen.
+  apply agree_undef_temps; auto.
 Qed.
 
 Lemma exec_Mreturn_prop:
  forall (s : list stackframe) (fb stk : block) (soff : int)
         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m',
  Genv.find_funct_ptr ge fb = Some (Internal f) ->
  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
  Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
  exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
                  (Returnstate s ms m').
Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
+  unfold load_stack in *.
+  exploit Mem.loadv_extends. eauto. eexact H0. auto. 
+  intros [parent' [A B]]. 
+  exploit lessdef_parent_sp; eauto. intros. subst parent'.
+  exploit Mem.loadv_extends. eauto. eexact H1. auto. 
+  intros [ra' [C D]].
+  exploit lessdef_parent_ra; eauto. intros. subst ra'.
+  exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]].
+
   exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14
-                rs m (parent_ra s)
+                rs m'0 (parent_ra s)
                 (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)).
   rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
   intros [rs1 [EXEC1 [RES1 OTH1]]].
@@ -1080,14 +1154,13 @@ Lemma exec_Mreturn_prop:
  forall (s : list stackframe) (fb stk : block) (soff :
   assert (EXEC2: exec_straight tge (transl_function f)
           (loadind_int IR13 (fn_retaddr_ofs f) IR14
              (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize)  (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c))
-          rs m (Pbreg IR14 :: transl_code f c) rs2 m').
+          rs m'0 (Pbreg IR14 :: transl_code f c) rs2 m2').
   eapply exec_straight_trans. eexact EXEC1. 
   apply exec_straight_one. simpl. rewrite OTH1; try congruence.
-  rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
-  unfold load_stack in H0. simpl in H0; simpl; rewrite H0. rewrite H2. reflexivity.
-  reflexivity.
+  rewrite <- (sp_val ms (Vptr stk soff) rs); auto. 
+  simpl chunk_of_type in A. rewrite A. rewrite E. auto. auto.
   set (rs3 := rs2#PC <- (parent_ra s)).
-  left; exists (State rs3 m'); split.
+  left; exists (State rs3 m2'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   inv AT. exploit exec_straight_steps_2; eauto. 
@@ -1100,15 +1173,13 @@ Lemma exec_Mreturn_prop:
  forall (s : list stackframe) (fb stk : block) (soff :
   traceEq.
   (* match states *)
   constructor. auto.
-  assert (AG1: agree ms (Vptr stk soff) rs1).
-    apply agree_exten_2 with rs; auto. 
-  assert (AG2: agree ms (parent_sp s) rs2).
-    constructor. reflexivity. intros; unfold rs2.
-    rewrite nextinstr_inv; auto with ppcgen.
-    rewrite Pregmap.gso; auto with ppcgen.
-    inv AG1; auto.
-  unfold rs3. auto with ppcgen. 
-  reflexivity.
+  apply agree_exten with rs2.
+  unfold rs2. apply agree_nextinstr. apply agree_change_sp with (Vptr stk soff).
+  apply agree_exten with rs; auto with ppcgen.
+  apply parent_sp_def. auto.
+  intros. unfold rs3. apply Pregmap.gso; auto with ppcgen.
+  unfold rs3. apply Pregmap.gss.
+  auto.
 Qed.
 
 Hypothesis wt_prog: wt_program prog.
@@ -1132,21 +1203,26 @@ Proof.
   generalize (functions_transl_no_overflow _ _ H); intro NOOV.
   set (rs2 := nextinstr (rs#IR13 <- sp)).
   set (rs3 := nextinstr rs2).
+  exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
+  intros [m1' [A B]].
+  unfold store_stack in *; simpl chunk_of_type in *.
+  exploit Mem.storev_extends. eexact B. eauto. auto. auto. 
+  intros [m2' [C D]].
+  exploit Mem.storev_extends. eexact D. eauto. auto. auto. 
+  intros [m3' [E F]].
   (* Execution of function prologue *)
   assert (EXEC_PROLOGUE:
             exec_straight tge (transl_function f)
-              (transl_function f) rs m
-              (transl_code f f.(fn_code)) rs3 m3).
+              (transl_function f) rs m'
+              (transl_code f f.(fn_code)) rs3 m3').
   unfold transl_function at 2.
-  apply exec_straight_two with rs2 m2.
-  unfold exec_instr. rewrite H0. fold sp. 
-  rewrite <- (sp_val ms (parent_sp s) rs); auto. 
-  unfold store_stack in H1. change Mint32 with (chunk_of_type Tint). rewrite H1.
-  auto.
+  apply exec_straight_two with rs2 m2'.
+  unfold exec_instr. rewrite A. fold sp. 
+  rewrite <- (sp_val ms (parent_sp s) rs); auto. rewrite C. auto.
   unfold exec_instr. unfold eval_shift_addr. unfold exec_store.
   change (rs2 IR13) with sp. change (rs2 IR14) with (rs IR14). rewrite ATLR.
-  unfold store_stack in H2. change Mint32 with (chunk_of_type Tint). rewrite H2. 
-  auto. auto. auto.
+  rewrite E. auto. 
+  auto. auto. 
   (* Agreement at end of prologue *)
   assert (AT3: transl_code_at_pc rs3#PC fb f f.(fn_code)).
     change (rs3 PC) with (Val.add (Val.add (rs PC) Vone) Vone).
@@ -1155,14 +1231,12 @@ Proof.
     eapply code_tail_next_int; auto.
     change (Int.unsigned Int.zero) with 0. 
     unfold transl_function. constructor.
-  assert (AG2: agree ms sp rs2).
-    split. reflexivity. 
-    intros. unfold rs2. rewrite nextinstr_inv. 
-    repeat (rewrite Pregmap.gso). elim AG; auto.
-    auto with ppcgen. auto with ppcgen.
   assert (AG3: agree ms sp rs3).
-    unfold rs3; auto with ppcgen.
-  left; exists (State rs3 m3); split.
+    unfold rs3. apply agree_nextinstr.
+    unfold rs2. apply agree_nextinstr. 
+    apply agree_change_sp with (parent_sp s); auto. 
+    unfold sp. congruence.
+  left; exists (State rs3 m3'); split.
   (* execution *)
   eapply exec_straight_steps_1; eauto.
   change (Int.unsigned Int.zero) with 0. constructor.
@@ -1183,15 +1257,21 @@ Lemma exec_function_external_prop:
 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 IR14))
-                m'); split.
+  intros [tf [A B]]. simpl in B. inv B.
+  exploit extcall_arguments_match; eauto. 
+  intros [args' [C D]].
+  exploit external_call_mem_extends; eauto. 
+  intros [vres' [m2' [P [Q [R S]]]]].
+  left; exists (State (rs#(loc_external_result (ef_sig ef)) <- vres' #PC <- (rs IR14))
+                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.
+  unfold loc_external_result. 
+  eapply agree_set_mreg; eauto. 
+  rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gss. auto.
+  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
 Qed.
 
 Lemma exec_return_prop:
@@ -1241,6 +1321,8 @@ Proof.
      with (Vptr fb Int.zero).
   econstructor; eauto. constructor.
   split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen.
+  intros. unfold Regmap.init. auto. 
+  apply Mem.extends_refl.
   unfold symbol_offset. 
   rewrite (transform_partial_program_main _ _ TRANSF). 
   rewrite symbols_preserved. unfold ge; rewrite H1. auto.
@@ -1251,8 +1333,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 _ _ _ R0 AG) in H1. auto. auto.
+  compute in H1. exploit ireg_val; eauto. instantiate (1 := R0); auto. 
+  simpl. intros LD. inv LD; congruence. 
 Qed.
 
 Theorem transf_program_correct:
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index fc2ce7fa..c10c9dfc 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -27,7 +27,7 @@ Require Import Machconcr.
 Require Import Machtyping.
 Require Import Asm.
 Require Import Asmgen.
-Require Conventions.
+Require Import Conventions.
 
 (** * Correspondence between Mach registers and PPC registers *)
 
@@ -41,91 +41,86 @@ Proof.
   destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
 Qed.
 
-(** Characterization of PPC registers that correspond to Mach registers. *)
-
-Definition is_data_reg (r: preg) : Prop :=
-  match r with
-  | IR IR14 => False
-  | CR _ => False
-  | PC => False
-  | _ => True
-  end.
-
-Lemma ireg_of_is_data_reg:
-  forall (r: mreg), is_data_reg (ireg_of r).
-Proof.
-  destruct r; exact I.
-Qed.
-
-Lemma freg_of_is_data_reg:
-  forall (r: mreg), is_data_reg (ireg_of r).
-Proof.
-  destruct r; exact I.
-Qed.
-
-Lemma preg_of_is_data_reg:
-  forall (r: mreg), is_data_reg (preg_of r).
-Proof.
-  destruct r; exact I.
-Qed.
-
 Lemma ireg_of_not_IR13:
   forall r, ireg_of r <> IR13.
 Proof.
-  intro. case r; discriminate.
+  destruct r; simpl; congruence.
 Qed.
+
 Lemma ireg_of_not_IR14:
   forall r, ireg_of r <> IR14.
 Proof.
-  intro. case r; discriminate.
+  destruct r; simpl; congruence.
 Qed.
 
-Hint Resolve ireg_of_not_IR13 ireg_of_not_IR14: ppcgen.
+Lemma preg_of_not_IR13:
+  forall r, preg_of r <> IR13.
+Proof.
+  unfold preg_of; intros. destruct (mreg_type r).
+  generalize (ireg_of_not_IR13 r); congruence.
+  congruence.
+Qed.
 
-Lemma preg_of_not:
-  forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2.
+Lemma preg_of_not_IR14:
+  forall r, preg_of r <> IR14.
 Proof.
-  intros; red; intro. subst r2. elim H. apply preg_of_is_data_reg.
+  unfold preg_of; intros. destruct (mreg_type r).
+  generalize (ireg_of_not_IR14 r); congruence.
+  congruence.
 Qed.
-Hint Resolve preg_of_not: ppcgen.
 
-Lemma preg_of_not_IR13:
-  forall r, preg_of r <> IR13.
+Lemma preg_of_not_PC:
+  forall r, preg_of r <> PC.
 Proof.
-  intro. case r; discriminate.
+  intros. unfold preg_of. destruct (mreg_type r); congruence.
 Qed.
-Hint Resolve preg_of_not_IR13: ppcgen.
 
-(** Agreement between Mach register sets and PPC register sets. *)
+Lemma ireg_diff:
+  forall r1 r2, r1 <> r2 -> IR r1 <> IR r2.
+Proof. intros; congruence. Qed.
+
+Hint Resolve ireg_of_not_IR13 ireg_of_not_IR14
+             preg_of_not_IR13 preg_of_not_IR14
+             preg_of_not_PC ireg_diff: ppcgen.
+
+(** Agreement between Mach register sets and ARM register sets. *)
 
-Definition agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) :=
-  rs#IR13 = 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#IR13 = 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. destruct H. auto.
+Qed.
+
+Lemma preg_vals:
+  forall ms sp rs, agree ms sp rs ->
+  forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)).
 Proof.
-  intros. elim H. auto.
+  induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto.
 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. generalize (preg_val _ _ _ r H). 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. generalize (preg_val _ _ _ r H). unfold preg_of. rewrite H0. auto.
 Qed.
 
 Lemma sp_val:
@@ -133,76 +128,71 @@ Lemma sp_val:
   agree ms sp rs ->
   sp = rs#IR13.
 Proof.
-  intros. elim H; auto.
+  intros. destruct H; auto.
 Qed.
 
-Lemma agree_exten_1:
-  forall ms sp rs rs',
-  agree ms sp rs ->
-  (forall r, is_data_reg r -> rs'#r = rs#r) ->
-  agree ms sp rs'.
+Hint Resolve preg_val ireg_val freg_val sp_val: ppcgen.
+
+Definition important_preg (r: preg) : bool :=
+  match r with
+  | IR IR14 => false
+  | IR _ => true
+  | FR _ => true
+  | CR _ => false
+  | PC => false
+  end.
+
+Lemma preg_of_important:
+  forall r, important_preg (preg_of r) = true.
 Proof.
-  unfold agree; intros. elim H; intros.
-  split. rewrite H0. auto. exact I. 
-  intros. rewrite H0. auto. apply preg_of_is_data_reg.
+  intros. destruct r; reflexivity.
 Qed.
 
-Lemma agree_exten_2:
+Lemma important_diff:
+  forall r r',
+  important_preg r = true -> important_preg r' = false -> r <> r'.
+Proof.
+  congruence.
+Qed.
+Hint Resolve important_diff: ppcgen.
+
+Lemma agree_exten:
   forall ms sp rs rs',
   agree ms sp rs ->
-  (forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r) ->
+  (forall r, important_preg r = true -> rs'#r = rs#r) ->
   agree ms sp rs'.
 Proof.
-  intros. eapply agree_exten_1; eauto. 
-  intros. apply H0; red; intro; subst r; elim H1.
+  intros. destruct H. split. 
+  rewrite H0; auto. auto.
+  intros. rewrite H0; auto. apply preg_of_important.
 Qed.
 
 (** Preservation of register agreement under various assignments. *)
 
 Lemma agree_set_mreg:
-  forall ms sp rs r v,
+  forall ms sp rs r v rs',
   agree ms sp rs ->
-  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_IR13.
-  intros. unfold Regmap.set. case (RegEq.eq r0 r); intro.
-  subst r0. rewrite Pregmap.gss. auto.
-  rewrite Pregmap.gso. auto. red; intro. 
-  elim n. apply preg_of_injective; auto.
-Qed.
-Hint Resolve agree_set_mreg: ppcgen.
-
-Lemma agree_set_mireg:
-  forall ms sp rs r v,
-  agree ms sp (rs#(preg_of r) <- v) ->
-  mreg_type r = Tint ->
-  agree ms sp (rs#(ireg_of r) <- v).
-Proof.
-  intros. unfold preg_of in H. rewrite H0 in H. auto.
-Qed.
-Hint Resolve agree_set_mireg: ppcgen.
-
-Lemma agree_set_mfreg:
-  forall ms sp rs r v,
-  agree ms sp (rs#(preg_of r) <- v) ->
-  mreg_type r = Tfloat ->
-  agree ms sp (rs#(freg_of r) <- v).
+  Val.lessdef v (rs'#(preg_of r)) ->
+  (forall r', important_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
+  agree (Regmap.set r v ms) sp rs'.
 Proof.
-  intros. unfold preg_of in H. rewrite H0 in H. auto.
+  intros. destruct H. split.
+  rewrite H1; auto. apply sym_not_equal. apply preg_of_not_IR13.
+  auto.
+  intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. 
+  rewrite H1. auto. apply preg_of_important.
+  red; intros; elim n. eapply preg_of_injective; eauto.
 Qed.
-Hint Resolve agree_set_mfreg: ppcgen.
 
 Lemma agree_set_other:
   forall ms sp rs r v,
   agree ms sp rs ->
-  ~(is_data_reg r) ->
+  important_preg r = false ->
   agree ms sp (rs#r <- v).
 Proof.
-  intros. apply agree_exten_1 with rs.
-  auto. intros. apply Pregmap.gso. red; intro; subst r0; contradiction.
+  intros. apply agree_exten with rs. auto.
+  intros. apply Pregmap.gso. congruence.
 Qed.
-Hint Resolve agree_set_other: ppcgen.
 
 Lemma agree_nextinstr:
   forall ms sp rs,
@@ -210,139 +200,159 @@ Lemma agree_nextinstr:
 Proof.
   intros. unfold nextinstr. apply agree_set_other. auto. auto.
 Qed.
-Hint Resolve agree_nextinstr: ppcgen.
 
-Lemma agree_set_mireg_twice:
-  forall ms sp rs r v v',
-  agree ms sp rs ->
-  mreg_type r = Tint ->
-  agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v' #(ireg_of r) <- v).
+Definition nontemp_preg (r: preg) : bool :=
+  match r with
+  | IR IR14 => false
+  | IR IR10 => false
+  | IR IR12 => false
+  | IR _ => true
+  | FR FR2 => false
+  | FR FR3 => false
+  | FR _ => true
+  | CR _ => false
+  | PC => false
+  end.
+
+Lemma nontemp_diff:
+  forall r r',
+  nontemp_preg r = true -> nontemp_preg r' = false -> r <> r'.
 Proof.
-  intros. replace (IR (ireg_of r)) with (preg_of r). elim H; intros.
-  split. repeat (rewrite Pregmap.gso; auto with ppcgen).
-  intros. case (mreg_eq r r0); intro.
-  subst r0. rewrite Regmap.gss. rewrite Pregmap.gss. auto.
-  assert (preg_of r <> preg_of r0). 
-    red; intro. elim n. apply preg_of_injective. auto.
-  rewrite Regmap.gso; auto.
-  repeat (rewrite Pregmap.gso; auto).
-  unfold preg_of. rewrite H0. auto.
+  congruence.
 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 ->
-  mreg_type r = Tint ->
-  agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v).
+Hint Resolve nontemp_diff: ppcgen.
+
+Lemma nontemp_important:
+  forall r, nontemp_preg r = true -> important_preg r = true.
 Proof.
-  intros. elim H; intros.
-  split. rewrite Pregmap.gso. auto. 
-  generalize (ireg_of_not_IR13 r); congruence.
-  intros. generalize (H2 r0). 
-  case (mreg_eq r0 r); intro.
-  subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0.
-  rewrite Pregmap.gss. auto.
-  repeat rewrite Regmap.gso; auto.
-  rewrite Pregmap.gso. auto. 
-  replace (IR (ireg_of r)) with (preg_of r).
-  red; intros. elim n. apply preg_of_injective; auto.
-  unfold preg_of. rewrite H0. auto.
+  unfold nontemp_preg, important_preg; destruct r; auto. destruct i; auto.
 Qed.
-Hint Resolve agree_set_twice_mireg: ppcgen.
 
-Lemma agree_set_commut:
-  forall ms sp rs r1 r2 v1 v2,
-  r1 <> r2 ->
-  agree ms sp ((rs#r2 <- v2)#r1 <- v1) ->
-  agree ms sp ((rs#r1 <- v1)#r2 <- v2).
+Hint Resolve nontemp_important: ppcgen.
+
+Remark undef_regs_1:
+  forall l ms r, ms r = Vundef -> Mach.undef_regs l ms r = Vundef.
 Proof.
-  intros. apply agree_exten_1 with ((rs#r2 <- v2)#r1 <- v1). auto.
-  intros. 
-  case (preg_eq r r1); intro.
-  subst r1. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss.
-  auto. auto.
-  case (preg_eq r r2); intro.
-  subst r2. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss.
-  auto. auto.
-  repeat (rewrite Pregmap.gso; auto). 
-Qed. 
-Hint Resolve agree_set_commut: ppcgen.
-
-Lemma agree_nextinstr_commut:
-  forall ms sp rs r v,
-  agree ms sp (rs#r <- v) ->
-  r <> PC ->
-  agree ms sp ((nextinstr rs)#r <- v).
+  induction l; simpl; intros. auto. apply IHl. unfold Regmap.set.
+  destruct (RegEq.eq r a); congruence.
+Qed.
+
+Remark undef_regs_2:
+  forall l ms r, In r l -> Mach.undef_regs l ms r = Vundef.
+Proof.
+  induction l; simpl; intros. contradiction. 
+  destruct H. subst. apply undef_regs_1. apply Regmap.gss.
+  auto.
+Qed.
+
+Remark undef_regs_3:
+  forall l ms r, ~In r l -> Mach.undef_regs l ms r = ms r.
 Proof.
-  intros. unfold nextinstr. apply agree_set_commut. auto. 
-  apply agree_set_other. auto. auto. 
+  induction l; simpl; intros. auto.
+  rewrite IHl. apply Regmap.gso. intuition. intuition.
 Qed.
-Hint Resolve agree_nextinstr_commut: ppcgen.
 
-Lemma agree_set_mireg_exten:
-  forall ms sp rs r v (rs': regset),
+Lemma agree_exten_temps:
+  forall ms sp rs rs',
   agree ms sp rs ->
-  mreg_type r = Tint ->
-  rs'#(ireg_of r) = v ->
-  (forall r', r' <> PC -> r' <> ireg_of r -> r' <> IR14 -> rs'#r' = rs#r') ->
-  agree (Regmap.set r v ms) sp rs'.
+  (forall r, nontemp_preg r = true -> rs'#r = rs#r) ->
+  agree (undef_temps ms) sp rs'.
 Proof.
-  intros. 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.
+  intros. destruct H. split. 
+  rewrite H0; auto. auto. 
+  intros. unfold undef_temps. 
+  destruct (In_dec mreg_eq r (int_temporaries ++ float_temporaries)).
+  rewrite undef_regs_2; auto. 
+  rewrite undef_regs_3; auto. rewrite H0; auto.
+  simpl in n. destruct r; auto; intuition.
 Qed.
 
-(** Useful properties of the PC and GPR0 registers. *)
+Lemma agree_set_undef_mreg:
+  forall ms sp rs r v rs',
+  agree ms sp rs ->
+  Val.lessdef v (rs'#(preg_of r)) ->
+  (forall r', nontemp_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
+  agree (Regmap.set r v (undef_temps ms)) sp rs'.
+Proof.
+  intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto.
+  eapply agree_exten_temps; eauto. 
+  intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). 
+  congruence. auto. 
+  intros. rewrite Pregmap.gso; auto. 
+Qed.
+
+Lemma agree_undef_temps:
+  forall ms sp rs,
+  agree ms sp rs ->
+  agree (undef_temps ms) sp rs.
+Proof.
+  intros. eapply agree_exten_temps; eauto.
+Qed.
+
+(** Useful properties of the PC register. *)
 
 Lemma nextinstr_inv:
-  forall r rs, r <> PC -> (nextinstr rs)#r = rs#r.
+  forall r rs,
+  r <> PC ->
+  (nextinstr rs)#r = rs#r.
+Proof.
+  intros. unfold nextinstr. apply Pregmap.gso. red; intro; subst. auto.
+Qed.
+
+Lemma nextinstr_inv2:
+  forall r rs,
+  nontemp_preg r = true ->
+  (nextinstr rs)#r = rs#r.
 Proof.
-  intros. unfold nextinstr. apply Pregmap.gso. auto.
+  intros. apply nextinstr_inv. red; intro; subst; discriminate.
 Qed.
-Hint Resolve nextinstr_inv: ppcgen.
 
 Lemma nextinstr_set_preg:
   forall rs m v,
   (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone.
 Proof.
   intros. unfold nextinstr. rewrite Pregmap.gss. 
-  rewrite Pregmap.gso. auto. apply sym_not_eq. auto with ppcgen.
+  rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC. 
 Qed.
-Hint Resolve nextinstr_set_preg: ppcgen.
 
 (** Connection between Mach and Asm calling conventions for external
     functions. *)
 
 Lemma extcall_arg_match:
-  forall ms sp rs m l v,
+  forall ms sp rs m m' l v,
   agree ms sp rs ->
   Machconcr.extcall_arg ms m sp l v ->
-  Asm.extcall_arg rs m l v.
+  Mem.extends m m' ->
+  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 H0.
+  exists (rs#(preg_of r)); split. constructor. eauto with ppcgen.
+  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; eauto.
 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.
+  exists (@nil val); split; constructor.
+  exploit extcall_arg_match; eauto. intros [v1' [A B]].
+  exploit IHextcall_args; eauto. intros [vl' [C D]].
+  exists(v1' :: vl'); split. constructor; auto. constructor; auto.
 Qed.
 
 Lemma extcall_arguments_match:
-  forall ms m sp rs sg args,
+  forall ms m sp rs sg args m',
   agree ms sp rs ->
   Machconcr.extcall_arguments ms m sp sg args ->
-  Asm.extcall_arguments rs m sg args.
+  Mem.extends m m' ->
+  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.
@@ -564,7 +574,7 @@ Proof.
   exploit loadimm_correct. intros [rs' [A [B C]]].
   exists (nextinstr (rs'#r1 <- (Val.and rs#r2 (Vint n)))).
   split. eapply exec_straight_trans. eauto. apply exec_straight_one.
-  simpl. rewrite B. rewrite C; auto with ppcgen. congruence.
+  simpl. rewrite B. rewrite C; auto with ppcgen. 
   auto.
   split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
   intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
@@ -756,20 +766,6 @@ Qed.
 
 (** Translation of conditions *)
 
-Ltac TypeInv :=
-  match goal with
-  | H: (List.map ?f ?x = nil) |- _ =>
-      destruct x; [clear H | simpl in H; discriminate]
-  | H: (List.map ?f ?x = ?hd :: ?tl) |- _ =>
-      destruct x; simpl in H;
-      [ discriminate |
-        injection H; clear H; let T := fresh "T" in (
-          intros H T; TypeInv) ]
-  | _ => idtac
-  end.
-
-(** Translation of conditions. *)
-
 Lemma compare_int_spec:
   forall rs v1 v2,
   let rs1 := nextinstr (compare_int rs v1 v2) in
@@ -783,11 +779,11 @@ Lemma compare_int_spec:
   /\ rs1#CRlt = (Val.cmp Clt v1 v2)
   /\ rs1#CRgt = (Val.cmp Cgt v1 v2)
   /\ rs1#CRle = (Val.cmp Cle v1 v2)
-  /\ forall r', is_data_reg r' -> rs1#r' = rs#r'.
+  /\ forall r', important_preg r' = true -> rs1#r' = rs#r'.
 Proof.
   intros. unfold rs1. intuition; try reflexivity. 
-  rewrite nextinstr_inv; [unfold compare_int; repeat rewrite Pregmap.gso; auto | idtac];
-  red; intro; subst r'; elim H.
+  rewrite nextinstr_inv; auto with ppcgen.
+  unfold compare_int. repeat rewrite Pregmap.gso; auto with ppcgen.
 Qed.
 
 Lemma compare_float_spec:
@@ -803,302 +799,237 @@ Lemma compare_float_spec:
   /\ rs'#CRlt = (Val.notbool (Val.cmpf Cge v1 v2))
   /\ rs'#CRgt = (Val.cmpf Cgt v1 v2)               
   /\ rs'#CRle = (Val.notbool (Val.cmpf Cgt v1 v2))
-  /\ forall r', is_data_reg r' -> rs'#r' = rs#r'.
+  /\ forall r', important_preg r' = true -> rs'#r' = rs#r'.
 Proof.
   intros. unfold rs'. intuition; try reflexivity. 
-  rewrite nextinstr_inv; [unfold compare_float; repeat rewrite Pregmap.gso; auto | idtac];
-  red; intro; subst r'; elim H.
+  rewrite nextinstr_inv; auto with ppcgen.
+  unfold compare_float. repeat rewrite Pregmap.gso; auto with ppcgen.
 Qed.
 
+Ltac TypeInv1 :=
+  match goal with
+  | H: (List.map ?f ?x = nil) |- _ =>
+      destruct x; inv H; TypeInv1
+  | H: (List.map ?f ?x = ?hd :: ?tl) |- _ =>
+      destruct x; simpl in H; simplify_eq H; clear H; intros; TypeInv1
+  | _ => idtac
+  end.
+
+Ltac TypeInv2 :=
+  match goal with
+  | H: (mreg_type _ = Tint) |- _ => try (rewrite H in *); clear H; TypeInv2
+  | H: (mreg_type _ = Tfloat) |- _ => try (rewrite H in *); clear H; TypeInv2
+  | _ => idtac
+  end.
+
+Ltac TypeInv := TypeInv1; simpl in *; unfold preg_of in *; TypeInv2.
+
 Lemma transl_cond_correct:
-  forall cond args k ms sp rs m b,
+  forall cond args k rs m b,
   map mreg_type args = type_of_condition cond ->
-  agree ms sp rs ->
-  eval_condition cond (map ms args) = Some b ->
+  eval_condition cond (map rs (map preg_of args)) = Some b ->
   exists rs',
      exec_straight (transl_cond cond args k) rs m k rs' m
   /\ rs'#(CR (crbit_for_cond cond)) = Val.of_bool b
-  /\ agree ms sp rs'.
+  /\ forall r, important_preg r = true -> rs'#r = rs r.
 Proof.
-  intros.
-  rewrite <- (eval_condition_weaken _ _ H1). clear H1. 
-  destruct cond; simpl in H; TypeInv; simpl.
+  intros until b; intros TY EV. rewrite <- (eval_condition_weaken _ _ EV). clear EV.  
+  destruct cond; simpl in TY; TypeInv.
   (* Ccomp *)
-  generalize (compare_int_spec rs ms#m0 ms#m1).
+  generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))).
   intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
-  exists (nextinstr (compare_int rs ms#m0 ms#m1)).
-  split. apply exec_straight_one. simpl. 
-  repeat rewrite <- (ireg_val ms sp rs); trivial. 
-  reflexivity.
-  split. 
-  case c; simpl; auto.
-  apply agree_exten_1 with rs; auto.
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. case c; assumption.
+  auto.
   (* Ccompu *)
-  generalize (compare_int_spec rs ms#m0 ms#m1).
+  generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))).
   intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
-  exists (nextinstr (compare_int rs ms#m0 ms#m1)).
-  split. apply exec_straight_one. simpl. 
-  repeat rewrite <- (ireg_val ms sp rs); trivial. 
-  reflexivity.
-  split. 
-  case c; simpl; auto.
-  apply agree_exten_1 with rs; auto.
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. case c; assumption.
+  auto.
   (* Ccompshift *)
-  generalize (compare_int_spec rs ms#m0 (eval_shift_total s ms#m1)).
+  generalize (compare_int_spec rs (rs (ireg_of m0)) (eval_shift_total s (rs (ireg_of m1)))).
   intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
-  exists (nextinstr (compare_int rs ms#m0 (eval_shift_total s ms#m1))).
-  split. apply exec_straight_one. simpl.
-  rewrite transl_shift_correct. 
-  repeat rewrite <- (ireg_val ms sp rs); trivial.
-  reflexivity.
-  split. 
-  case c; simpl; auto.
-  apply agree_exten_1 with rs; auto.
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. rewrite transl_shift_correct. case c; assumption.
+  rewrite transl_shift_correct. auto.
   (* Ccompushift *)
-  generalize (compare_int_spec rs ms#m0 (eval_shift_total s ms#m1)).
+  generalize (compare_int_spec rs (rs (ireg_of m0)) (eval_shift_total s (rs (ireg_of m1)))).
   intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
-  exists (nextinstr (compare_int rs ms#m0 (eval_shift_total s ms#m1))).
-  split. apply exec_straight_one. simpl.
-  rewrite transl_shift_correct. 
-  repeat rewrite <- (ireg_val ms sp rs); trivial.
-  reflexivity.
-  split. 
-  case c; simpl; auto.
-  apply agree_exten_1 with rs; auto.
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. rewrite transl_shift_correct. case c; assumption.
+  rewrite transl_shift_correct. auto.
   (* Ccompimm *)
   destruct (is_immed_arith i).
-  generalize (compare_int_spec rs ms#m0 (Vint i)).
+  generalize (compare_int_spec rs (rs (ireg_of m0)) (Vint i)).
   intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
-  exists (nextinstr (compare_int rs ms#m0 (Vint i))).
-  split. apply exec_straight_one. simpl. 
-  rewrite <- (ireg_val ms sp rs); trivial. auto.
-  split. 
-  case c; simpl; auto.
-  apply agree_exten_1 with rs; auto.
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto. 
+  split. case c; assumption.
+  auto.
   exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
-  assert (AG: agree ms sp rs'). apply agree_exten_2 with rs; auto. 
-  generalize (compare_int_spec rs' ms#m0 (Vint i)).
+  generalize (compare_int_spec rs' (rs (ireg_of m0)) (Vint i)).
   intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
-  exists (nextinstr (compare_int rs' ms#m0 (Vint i))).
+  econstructor.
   split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
-  rewrite Q. rewrite <- (ireg_val ms sp rs'); trivial. auto.
-  split. 
-  case c; simpl; auto.
-  apply agree_exten_1 with rs'; auto.
+  rewrite Q. rewrite R; eauto with ppcgen. auto.
+  split. case c; assumption.
+  intros. rewrite K; auto with ppcgen.
   (* Ccompuimm *)
   destruct (is_immed_arith i).
-  generalize (compare_int_spec rs ms#m0 (Vint i)).
+  generalize (compare_int_spec rs (rs (ireg_of m0)) (Vint i)).
   intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
-  exists (nextinstr (compare_int rs ms#m0 (Vint i))).
-  split. apply exec_straight_one. simpl. 
-  rewrite <- (ireg_val ms sp rs); trivial. auto.
-  split. 
-  case c; simpl; auto.
-  apply agree_exten_1 with rs; auto.
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto. 
+  split. case c; assumption.
+  auto.
   exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
-  assert (AG: agree ms sp rs'). apply agree_exten_2 with rs; auto. 
-  generalize (compare_int_spec rs' ms#m0 (Vint i)).
+  generalize (compare_int_spec rs' (rs (ireg_of m0)) (Vint i)).
   intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
-  exists (nextinstr (compare_int rs' ms#m0 (Vint i))).
+  econstructor.
   split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
-  rewrite Q. rewrite <- (ireg_val ms sp rs'); trivial. auto.
-  split. 
-  case c; simpl; auto.
-  apply agree_exten_1 with rs'; auto.
+  rewrite Q. rewrite R; eauto with ppcgen. auto.
+  split. case c; assumption.
+  intros. rewrite K; auto with ppcgen.
   (* Ccompf *)
-  generalize (compare_float_spec rs ms#m0 ms#m1).
+  generalize (compare_float_spec rs (rs (freg_of m0)) (rs (freg_of m1))).
   intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
-  exists (nextinstr (compare_float rs ms#m0 ms#m1)).
-  split. apply exec_straight_one. simpl. 
-  repeat rewrite <- (freg_val ms sp rs); trivial. auto.
-  split. 
-  case c; simpl; auto.
-  apply agree_exten_1 with rs; auto.
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. case c; assumption.
+  auto.
   (* Cnotcompf *)
-  generalize (compare_float_spec rs ms#m0 ms#m1).
+  generalize (compare_float_spec rs (rs (freg_of m0)) (rs (freg_of m1))).
   intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
-  exists (nextinstr (compare_float rs ms#m0 ms#m1)).
-  split. apply exec_straight_one. simpl. 
-  repeat rewrite <- (freg_val ms sp rs); trivial. auto.
-  split. 
-  case c; simpl; auto.
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. case c; try assumption.
     rewrite Val.negate_cmpf_ne. auto.
     rewrite Val.negate_cmpf_eq. auto.
-  apply agree_exten_1 with rs; auto.
+  auto.
 Qed.
 
 (** Translation of arithmetic operations. *)
 
-Ltac TranslOpSimpl :=
+Ltac Simpl :=
   match goal with
-  | |- 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));
-     split; 
-     [ apply exec_straight_one;
-       [ repeat (rewrite (ireg_val ms sp rs); auto);
-         simpl; try rewrite transl_shift_correct; reflexivity
-       | reflexivity ]
-     | auto with ppcgen ])
-  ||
-    (exists (nextinstr (rs#(freg_of res) <- v));
-     split; 
-     [ apply exec_straight_one;
-       [ repeat (rewrite (freg_val ms sp rs); auto); reflexivity
-       | reflexivity ]
-     | auto with ppcgen ])
+  | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
+  | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto
+  | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto
+  | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
+  | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
   end.
 
+Ltac TranslOpSimpl :=
+  econstructor; split;
+  [ apply exec_straight_one; [simpl; eauto | reflexivity ]
+  | split; [try rewrite transl_shift_correct; repeat Simpl | intros; repeat Simpl] ].
+
 Lemma transl_op_correct:
-  forall op args res k ms sp rs m v,
+  forall op args res k (rs: regset) m v,
   wt_instr (Mop op args res) ->
-  agree ms sp rs ->
-  eval_operation ge sp op (map ms args) = Some v ->
+  eval_operation ge rs#IR13 op (map rs (map preg_of 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'.
+  /\ rs'#(preg_of res) = v
+  /\ forall r, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r.
 Proof.
-  intros. rewrite <- (eval_operation_weaken _ _ _ _ H1). (*clear H1; clear v.*)
-  inversion H.
+  intros. rewrite <- (eval_operation_weaken _ _ _ _ H0). 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 <- H3. rewrite H6. reflexivity.
-  auto with ppcgen.
-  apply exec_straight_one. simpl. rewrite (freg_val ms sp rs); auto.
-  simpl. unfold preg_of. rewrite <- H3. rewrite H6. reflexivity.
-  auto with ppcgen.
-  auto with ppcgen.
+  simpl.
+  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.
+  split. Simpl. Simpl.
+  intros. Simpl. Simpl.
   (* Other instructions *)
-  clear H2 H3 H5. 
-  destruct op; simpl in H6; injection H6; clear H6; intros;
-  TypeInv; simpl; try (TranslOpSimpl).
+  destruct op; simpl in H5; inv H5; TypeInv; try (TranslOpSimpl; fail).
   (* Omove again *)
   congruence.
   (* Ointconst *)
-  generalize (loadimm_correct (ireg_of res) i k rs m).
-  intros [rs' [A [B C]]]. 
-  exists rs'. split. auto. 
-  apply agree_set_mireg_exten with rs; auto. 
+  generalize (loadimm_correct (ireg_of res) i k rs m). intros [rs' [A [B C]]]. 
+  exists rs'. split. auto. split. auto. intros. auto with ppcgen.
   (* Oaddrstack *)
   generalize (addimm_correct (ireg_of res) IR13 i k rs m). 
   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.
+  exists rs'. split. auto. split. auto. auto with ppcgen.
   (* Ocast8signed *)
-  set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 24))))).
-  set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 24))))).
-  exists rs2. split.
-  apply exec_straight_two with rs1 m; auto.
-  simpl. rewrite <- (ireg_val ms sp rs); auto.
-  unfold rs2. 
-  replace (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 24))) with (Val.sign_ext 8 (ms m0)).
-  apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut.
-  apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. 
-  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  destruct (ms m0); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity.
-  vm_compute; auto. 
+  econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity.
+  compute; auto.
+  intros. repeat Simpl. 
   (* Ocast8unsigned *)
-  exists (nextinstr (rs#(ireg_of res) <- (Val.and (ms m0) (Vint (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.and (ms m0) (Vint (Int.repr 255))).
-  auto with ppcgen. 
-  destruct (ms m0); simpl; auto. rewrite Int.zero_ext_and. reflexivity. 
-  vm_compute; auto.
+  econstructor; split.
+  eapply exec_straight_one. simpl; eauto. auto. 
+  split. Simpl. Simpl.
+  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_and. reflexivity.
+  compute; auto.
+  intros. repeat Simpl.
   (* Ocast16signed *)
-  set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 16))))).
-  set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 16))))).
-  exists rs2. split.
-  apply exec_straight_two with rs1 m; auto.
-  simpl. rewrite <- (ireg_val ms sp rs); auto. 
-  unfold rs2. 
-  replace (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 16))) with (Val.sign_ext 16 (ms m0)).
-  apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut.
-  apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. 
-  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  destruct (ms m0); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity.
-  vm_compute; auto. 
+  econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity.
+  compute; auto.
+  intros. repeat Simpl. 
   (* Ocast16unsigned *)
-  set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 16))))).
-  set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shru (rs1 (ireg_of res)) (Vint (Int.repr 16))))).
-  exists rs2. split.
-  apply exec_straight_two with rs1 m; auto.
-  simpl. rewrite <- (ireg_val ms sp rs); auto. 
-  unfold rs2. 
-  replace (Val.shru (rs1 (ireg_of res)) (Vint (Int.repr 16))) with (Val.zero_ext 16 (ms m0)).
-  apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut.
-  apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. 
-  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  destruct (ms m0); simpl; auto. rewrite Int.zero_ext_shru_shl. reflexivity.
-  vm_compute; auto. 
+  econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_shru_shl. reflexivity.
+  compute; auto.
+  intros. repeat Simpl.
   (* Oaddimm *)
   generalize (addimm_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. split. auto. auto with ppcgen.
   (* Orsbimm *)
   exploit (makeimm_correct Prsb (fun v1 v2 => Val.sub v2 v1) (ireg_of res) (ireg_of m0));
   auto with ppcgen.
   intros [rs' [A [B C]]].
   exists rs'.
-  split. eauto.
-  apply agree_set_mireg_exten with rs; auto. rewrite B. 
-  rewrite <- (ireg_val ms sp rs); auto. 
+  split. eauto. split. rewrite B. auto. auto with ppcgen. 
   (* Omul *)
   destruct (ireg_eq (ireg_of res) (ireg_of m0) || ireg_eq (ireg_of res) (ireg_of m1)).
-  set (rs1 := nextinstr (rs#IR14 <- (Val.mul (ms m0) (ms m1)))).
-  set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#IR14))).
-  exists rs2; split.
-  apply exec_straight_two with rs1 m; auto.
-  simpl. repeat rewrite <- (ireg_val ms sp rs); auto.
-  unfold rs2. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. 
-  apply agree_nextinstr. apply agree_nextinstr_commut. 
-  apply agree_set_mireg; auto.  apply agree_set_mreg. apply agree_set_other. auto.
-  simpl; auto. auto with ppcgen. discriminate.
+  econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
+  split. repeat Simpl.
+  intros. repeat Simpl.
   TranslOpSimpl.
   (* Oandimm *)
   generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m
                             (ireg_of_not_IR14 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. 
+  exists rs'. split. auto. split. auto. auto with ppcgen.
   (* Oorimm *)
   exploit (makeimm_correct Porr Val.or (ireg_of res) (ireg_of m0));
   auto with ppcgen.
-  intros [rs' [A [B C]]].
-  exists rs'.
-  split. eauto.
-  apply agree_set_mireg_exten with rs; auto. rewrite B. 
-  rewrite <- (ireg_val ms sp rs); auto. 
+  intros [rs' [A [B C]]]. 
+  exists rs'. split. eauto. split. auto. auto with ppcgen.
   (* Oxorimm *)
   exploit (makeimm_correct Peor Val.xor (ireg_of res) (ireg_of m0));
   auto with ppcgen.
-  intros [rs' [A [B C]]].
-  exists rs'.
-  split. eauto.
-  apply agree_set_mireg_exten with rs; auto. rewrite B. 
-  rewrite <- (ireg_val ms sp rs); auto.
+  intros [rs' [A [B C]]]. 
+  exists rs'. split. eauto. split. auto. auto with ppcgen.
   (* Oshrximm *)
-  assert (exists n, ms m0 = Vint n /\ Int.ltu i (Int.repr 31) = true).
-    simpl in H1. destruct (ms m0); try discriminate.
+  assert (exists n, rs (ireg_of m0) = Vint n /\ Int.ltu i (Int.repr 31) = true).
+    destruct (rs (ireg_of m0)); try discriminate.
     exists i0; split; auto. destruct (Int.ltu i (Int.repr 31)); discriminate || auto.
-  destruct H3 as [n [ARG1 LTU]].
+  destruct H as [n [ARG1 LTU]]. clear H0.
   assert (LTU': Int.ltu i Int.iwordsize = true).
     exploit Int.ltu_inv. eexact LTU. intro.
     unfold Int.ltu. apply zlt_true.
-    assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto.
+    assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). compute; auto.
     omega.
-  assert (RSm0: rs (ireg_of m0) = Vint n).
-    rewrite <- ARG1. symmetry. eapply ireg_val; eauto. 
   set (islt := Int.lt n Int.zero).
   set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero))).
-  assert (OTH1: forall r', is_data_reg r' -> rs1#r' = rs#r').
+  assert (OTH1: forall r', important_preg r' = true -> rs1#r' = rs#r').
     generalize (compare_int_spec rs (Vint n) (Vint Int.zero)).
     fold rs1. intros [A B]. intuition.
   exploit (addimm_correct IR14 (ireg_of m0) (Int.sub (Int.shl Int.one i) Int.one)).
@@ -1107,83 +1038,47 @@ Proof.
   set (rs4 := nextinstr (rs3#(ireg_of res) <- (Val.shr rs3#IR14 (Vint i)))).
   exists rs4; split.
   apply exec_straight_step with rs1 m.
-  simpl. rewrite RSm0. auto. auto.
+  simpl. rewrite ARG1. auto. auto.
   eapply exec_straight_trans. eexact EXEC2.
   apply exec_straight_two with rs3 m.
   simpl. rewrite OTH2. change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)).
     unfold Val.cmp. change (Int.cmp Cge n Int.zero) with (negb islt).
-    rewrite OTH2. rewrite OTH1. rewrite RSm0. 
+    rewrite OTH2. rewrite OTH1. rewrite ARG1. 
     unfold rs3. case islt; reflexivity.
-    apply ireg_of_is_data_reg. decEq; auto with ppcgen. auto with ppcgen. congruence. congruence.
+    destruct m0; reflexivity. auto with ppcgen. auto with ppcgen. discriminate. discriminate.
   simpl. auto. 
   auto. unfold rs3. case islt; auto. auto.
-  (* agreement *)
-  assert (RES4: rs4#(ireg_of res) = Vint(Int.shrx n i)).
-    unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gss.
-    rewrite Int.shrx_shr. fold islt. unfold rs3.
-    repeat rewrite nextinstr_inv; auto. 
-    case islt. rewrite RES2. rewrite OTH1. rewrite RSm0. 
-    simpl. rewrite LTU'. auto.
-    apply ireg_of_is_data_reg. 
-    rewrite Pregmap.gss. simpl. rewrite LTU'. auto. congruence.
-    exact LTU. auto with ppcgen. 
-  assert (OTH4: forall r, is_data_reg r -> r <> ireg_of res -> rs4#r = rs#r).
-    intros. 
-    assert (r <> PC). red; intro; subst r; elim H3.
-    assert (r <> IR14). red; intro; subst r; elim H3.
-    unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-    unfold rs3. rewrite nextinstr_inv; auto.
-    transitivity (rs2 r).
-    case islt. auto. apply Pregmap.gso; auto.
-    rewrite OTH2; auto. 
-  apply agree_exten_1 with (rs#(ireg_of res) <- (Val.shrx (ms m0) (Vint i))).
-  auto with ppcgen.
-  intros. unfold Pregmap.set. destruct (PregEq.eq r (ireg_of res)).
-  subst r. rewrite ARG1. simpl. rewrite LTU'. auto.
-  auto.
-  (* Ointoffloat *)
-  exists (nextinstr (rs#(ireg_of res) <- (Val.intoffloat (ms m0)))).
-  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)))).
-  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)))).
-  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)))).
-  split. apply exec_straight_one. 
-  repeat (rewrite (ireg_val ms sp rs); auto).
-  reflexivity. auto 10 with ppcgen.
+  split. unfold rs4. repeat Simpl. rewrite ARG1. simpl. rewrite LTU'. rewrite Int.shrx_shr.
+  fold islt. unfold rs3. rewrite nextinstr_inv; auto with ppcgen. 
+  destruct islt. rewrite RES2. change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))). 
+  rewrite ARG1. simpl. rewrite LTU'. auto.
+  rewrite Pregmap.gss. simpl. rewrite LTU'. auto. 
+  assumption.
+  intros. unfold rs4; repeat Simpl. unfold rs3; repeat Simpl. 
+  transitivity (rs2 r). destruct islt; auto. Simpl. 
+  rewrite OTH2; auto with ppcgen.
   (* Ocmp *)
-  assert (exists b, eval_condition c ms##args = Some b /\ v = Val.of_bool b).
-    simpl in H1. destruct (eval_condition c ms##args). 
-    destruct b; inv H1. exists true; auto. exists false; auto.
-    discriminate.
-  destruct H5 as [b [EVC EQ]].
-  exploit transl_cond_correct; eauto. intros [rs' [A [B C]]].
-  rewrite (eval_condition_weaken _ _ EVC).
-  set (rs1 := nextinstr (rs'#(ireg_of res) <- (Vint Int.zero))).
-  set (rs2 := nextinstr (if b then (rs1#(ireg_of res) <- Vtrue) else rs1)).
-  exists rs2; split.
-  eapply exec_straight_trans. eauto. 
-  apply exec_straight_two with rs1 m; auto.
-  simpl. replace (rs1 (crbit_for_cond c)) with (Val.of_bool b).
-  unfold rs2. destruct b; auto. 
-  unfold rs2. destruct b; auto.
-  apply agree_set_mireg_exten with rs'; auto.
-  unfold rs2. rewrite nextinstr_inv; auto with ppcgen. 
-  destruct b. apply Pregmap.gss.
-  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. unfold rs2. rewrite nextinstr_inv; auto. 
-  transitivity (rs1 r'). destruct b; auto. rewrite Pregmap.gso; auto.
-  unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  fold preg_of in *.
+  assert (exists b, eval_condition c rs ## (preg_of ## args) = Some b /\ v = Val.of_bool b).
+    fold preg_of in H0. destruct (eval_condition c rs ## (preg_of ## args)).
+    exists b; split; auto. destruct b; inv H0; auto. congruence.
+  clear H0. destruct H as [b [EVC VBO]]. rewrite (eval_condition_weaken _ _ EVC).
+  destruct (transl_cond_correct c args 
+             (Pmov (ireg_of res) (SOimm Int.zero)
+              :: Pmovc (crbit_for_cond c) (ireg_of res) (SOimm Int.one) :: k)
+             rs m b H1 EVC)
+  as [rs1 [A [B C]]].
+  set (rs2 := nextinstr (rs1#(ireg_of res) <- (Vint Int.zero))).
+  set (rs3 := nextinstr (if b then (rs2#(ireg_of res) <- Vtrue) else rs2)).
+  exists rs3.
+  split. eapply exec_straight_trans. eauto. 
+  apply exec_straight_two with rs2 m; auto.
+  simpl. replace (rs2 (crbit_for_cond c)) with (Val.of_bool b).
+  unfold rs3. destruct b; auto.
+  unfold rs3. destruct b; auto.
+  split. unfold rs3. Simpl. destruct b. Simpl. unfold rs2. repeat Simpl.
+  intros. unfold rs3. Simpl. transitivity (rs2 r). 
+  destruct b; auto; Simpl. unfold rs2. repeat Simpl. 
 Qed.
 
 Remark val_add_add_zero:
@@ -1191,15 +1086,15 @@ Remark val_add_add_zero:
 Proof.
   intros. destruct v1; destruct v2; simpl; auto; rewrite Int.add_zero; auto.
 Qed.
- 
+
 Lemma transl_load_store_correct:
   forall (mk_instr_imm: ireg -> int -> instruction)
          (mk_instr_gen: option (ireg -> shift_addr -> instruction))
          (is_immed: int -> bool)
          addr args k ms sp rs m ms' m',
   (forall (r1: ireg) (rs1: regset) n k,
-    eval_addressing_total sp addr (map ms args) = Val.add rs1#r1 (Vint n) ->
-    agree ms sp rs1 ->
+    eval_addressing_total sp addr (map rs (map preg_of args)) = Val.add rs1#r1 (Vint n) ->
+    (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) ->
     exists rs',
     exec_straight (mk_instr_imm r1 n :: k) rs1 m k rs' m' /\
     agree ms' sp rs') ->
@@ -1207,8 +1102,8 @@ Lemma transl_load_store_correct:
   | None => True
   | Some mk =>
       (forall (r1: ireg) (sa: shift_addr) (rs1: regset) k,
-      eval_addressing_total sp addr (map ms args) = Val.add rs1#r1 (eval_shift_addr sa rs1) ->
-      agree ms sp rs1 ->
+      eval_addressing_total sp addr (map rs (map preg_of args)) = Val.add rs1#r1 (eval_shift_addr sa rs1) ->
+      (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) ->
       exists rs',
       exec_straight (mk r1 sa :: k) rs1 m k rs' m' /\
       agree ms' sp rs')
@@ -1224,62 +1119,53 @@ Proof.
   (* Aindexed *)
   case (is_immed i).
   (* Aindexed, small displacement *)
-  apply H; eauto. simpl. rewrite (ireg_val ms sp rs); auto.
+  apply H; auto.
   (* Aindexed, large displacement *)
-  exploit (addimm_correct IR14 (ireg_of t)); eauto with ppcgen. 
-  intros [rs' [A [B C]]].
-  exploit (H IR14 rs' Int.zero); eauto.
-  simpl. rewrite (ireg_val ms sp rs); auto. rewrite B.
-  rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity.
-  apply agree_exten_2 with rs; auto. 
+  destruct (addimm_correct IR14 (ireg_of m0) i (mk_instr_imm IR14 Int.zero :: k) rs m)
+  as [rs' [A [B C]]].
+  exploit (H IR14 rs' Int.zero); eauto. 
+  rewrite B. rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity.
   intros [rs'' [D E]].
   exists rs''; split.
   eapply exec_straight_trans. eexact A. eexact D. auto.
   (* Aindexed2 *)
   destruct mk_instr_gen as [mk | ]. 
   (* binary form available *)
-  apply H0; auto. simpl. repeat rewrite (ireg_val ms sp rs); auto. 
+  apply H0; auto.
   (* binary form not available *)
-  set (rs' := nextinstr (rs#IR14 <- (Val.add (ms t) (ms t0)))).
+  set (rs' := nextinstr (rs#IR14 <- (Val.add (rs (ireg_of m0)) (rs (ireg_of m1))))).
   exploit (H IR14 rs' Int.zero); eauto.
-  simpl. repeat rewrite (ireg_val ms sp rs); auto.
   unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  repeat rewrite (ireg_val ms sp rs); auto. apply val_add_add_zero. 
-  unfold rs'; auto with ppcgen.
+  apply val_add_add_zero. 
+  unfold rs'. intros. repeat Simpl. 
   intros [rs'' [A B]].
   exists rs''; split.
   eapply exec_straight_step with (rs2 := rs'); eauto.
-  simpl. repeat rewrite <- (ireg_val ms sp rs); auto.
-  auto.
+  simpl. auto. auto.
   (* Aindexed2shift *)
   destruct mk_instr_gen as [mk | ]. 
   (* binary form available *)
-  apply H0; auto. simpl. repeat rewrite (ireg_val ms sp rs); auto.
-  rewrite transl_shift_addr_correct. auto.
+  apply H0; auto. rewrite transl_shift_addr_correct. auto.
   (* binary form not available *)
-  set (rs' := nextinstr (rs#IR14 <- (Val.add (ms t) (eval_shift_total s (ms t0))))).
+  set (rs' := nextinstr (rs#IR14 <- (Val.add (rs (ireg_of m0)) (eval_shift_total s (rs (ireg_of m1)))))).
   exploit (H IR14 rs' Int.zero); eauto.
-  simpl. repeat rewrite (ireg_val ms sp rs); auto.
   unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  repeat rewrite (ireg_val ms sp rs); auto. apply val_add_add_zero. 
-  unfold rs'; auto with ppcgen.
+  apply val_add_add_zero.
+  unfold rs'; intros; repeat Simpl.
   intros [rs'' [A B]].
   exists rs''; split.
   eapply exec_straight_step with (rs2 := rs'); eauto.
-  simpl. rewrite transl_shift_correct. 
-  repeat rewrite <- (ireg_val ms sp rs); auto.
+  simpl. rewrite transl_shift_correct. auto. 
   auto.
   (* Ainstack *)
   destruct (is_immed i).
   (* Ainstack, short displacement *)
-  apply H. simpl.  rewrite (sp_val ms sp rs); auto. auto. 
+  apply H; auto. rewrite (sp_val _ _ _ H1). auto.
   (* Ainstack, large displacement *)
-  exploit (addimm_correct IR14 IR13); eauto with ppcgen. 
-  intros [rs' [A [B C]]].
+  destruct (addimm_correct IR14 IR13 i (mk_instr_imm IR14 Int.zero :: k) rs m)
+  as [rs' [A [B C]]].
   exploit (H IR14 rs' Int.zero); eauto.
-  simpl. rewrite (sp_val ms sp rs); auto. rewrite B.
-  rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity.
-  apply agree_exten_2 with rs; auto. 
+  rewrite (sp_val _ _ _ H1). rewrite B. rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. auto.
   intros [rs'' [D E]].
   exists rs''; split.
   eapply exec_straight_trans. eexact A. eexact D. auto.
@@ -1288,116 +1174,159 @@ Qed.
 Lemma transl_load_int_correct:
   forall (mk_instr: ireg -> ireg -> shift_addr -> instruction)
          (is_immed: int -> bool)
-         (rd: mreg) addr args k ms sp rs m chunk a v,
+         (rd: mreg) addr args k ms sp rs m m' chunk a v,
   (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset),
-    exec_instr ge c (mk_instr r1 r2 sa) rs1 m =
-    exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) ->
+    exec_instr ge c (mk_instr r1 r2 sa) rs1 m' =
+    exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m') ->
   agree ms sp rs ->
   map mreg_type args = type_of_addressing addr ->
   mreg_type rd = Tint ->
   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_int mk_instr is_immed rd addr args k) rs m
-                        k rs' m
-  /\ agree (Regmap.set rd v ms) sp rs'.
+    exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m'
+                        k rs' m'
+  /\ agree (Regmap.set rd v (undef_temps ms)) sp rs'.
 Proof.
   intros. unfold transl_load_store_int.
-  exploit eval_addressing_weaken. eauto. 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. intros E.
   apply transl_load_store_correct with ms; auto.
-  intros. exists (nextinstr (rs1#(ireg_of rd) <- v)); split.
-  apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. 
-  unfold exec_load. rewrite H4. auto. auto.
-  auto with ppcgen.
-  intros. exists (nextinstr (rs1#(ireg_of rd) <- v)); split.
-  apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. 
-  unfold exec_load. rewrite H4. auto. auto.
-  auto with ppcgen.
+  intros.
+  assert (Val.add (rs1 r1) (Vint n) = a') by congruence.
+  exists (nextinstr (rs1#(ireg_of rd) <- v')); split.
+  apply exec_straight_one. rewrite H. unfold exec_load. 
+  simpl. rewrite H8. rewrite C. auto. auto.
+  apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. 
+  unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. 
+  unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen.
+  intros.
+  assert (Val.add (rs1 r1) (eval_shift_addr sa rs1) = a') by congruence.
+  exists (nextinstr (rs1#(ireg_of rd) <- v')); split.
+  apply exec_straight_one. rewrite H. unfold exec_load. 
+  simpl. rewrite H8. rewrite C. auto. auto.
+  apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. 
+  unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. 
+  unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen.
 Qed.
 
 Lemma transl_load_float_correct:
   forall (mk_instr: freg -> ireg -> int -> instruction)
          (is_immed: int -> bool)
-         (rd: mreg) addr args k ms sp rs m chunk a v,
+         (rd: mreg) addr args k ms sp rs m m' chunk a v,
   (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset),
-    exec_instr ge c (mk_instr r1 r2 n) rs1 m =
-    exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) ->
+    exec_instr ge c (mk_instr r1 r2 n) rs1 m' =
+    exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m') ->
   agree ms sp rs ->
   map mreg_type args = type_of_addressing addr ->
   mreg_type rd = Tfloat ->
   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_float mk_instr is_immed rd addr args k) rs m
-                        k rs' m
-  /\ agree (Regmap.set rd v ms) sp rs'.
+    exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m'
+                        k rs' m'
+  /\ agree (Regmap.set rd v (undef_temps ms)) sp rs'.
 Proof.
-  intros. unfold transl_load_store_float.
-  exploit eval_addressing_weaken. eauto. intros. 
+  intros. unfold transl_load_store_int.
+  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. intros E.
   apply transl_load_store_correct with ms; auto.
-  intros. exists (nextinstr (rs1#(freg_of rd) <- v)); split.
-  apply exec_straight_one. rewrite H. rewrite <- H6. rewrite H5. 
-  unfold exec_load. rewrite H4. auto. auto.
-  auto with ppcgen.
+  intros.
+  assert (Val.add (rs1 r1) (Vint n) = a') by congruence.
+  exists (nextinstr (rs1#(freg_of rd) <- v')); split.
+  apply exec_straight_one. rewrite H. unfold exec_load. 
+  simpl. rewrite H8. rewrite C. auto. auto.
+  apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. 
+  unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. 
+  unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen.
 Qed.
 
 Lemma transl_store_int_correct:
   forall (mk_instr: ireg -> ireg -> shift_addr -> instruction)
          (is_immed: int -> bool)
-         (rd: mreg) addr args k ms sp rs m chunk a m',
+         (rd: mreg) addr args k ms sp rs m1 chunk a m2 m1',
   (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset),
-    exec_instr ge c (mk_instr r1 r2 sa) rs1 m =
-    exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) ->
+    exec_instr ge c (mk_instr r1 r2 sa) rs1 m1' =
+    exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m1') ->
   agree ms sp rs ->
   map mreg_type args = type_of_addressing addr ->
   mreg_type rd = Tint ->
   eval_addressing ge sp addr (map ms args) = Some a ->
-  Mem.storev chunk m a (ms rd) = Some m' ->
-  exists rs',
-    exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m
-                        k rs' m'
-  /\ agree ms sp rs'.
+  Mem.storev chunk m1 a (ms rd) = Some m2 ->
+  Mem.extends m1 m1' ->
+  exists m2',
+    Mem.extends m2 m2' /\
+    exists rs',
+    exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m1'
+                        k rs' m2'
+    /\ agree (undef_temps ms) sp rs'.
 Proof.
   intros. unfold transl_load_store_int.
-  exploit eval_addressing_weaken. eauto. intros. 
+  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
+  intros [a' [A B]].
+  exploit preg_val; eauto. instantiate (1 := rd). intros C.
+  exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]].
+  exploit eval_addressing_weaken. eexact A. intros F.
+  exists m2'; split; auto.
   apply transl_load_store_correct with ms; auto.
-  intros. exists (nextinstr rs1); split.
-  apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5.
-  unfold exec_store. rewrite <- (ireg_val ms sp rs1); auto.
-  rewrite H4. auto. auto.
-  auto with ppcgen.
-  intros. exists (nextinstr rs1); split.
-  apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5.
-  unfold exec_store. rewrite <- (ireg_val ms sp rs1); auto.
-  rewrite H4. auto. auto.
-  auto with ppcgen.
+  intros.
+  assert (Val.add (rs1 r1) (Vint n) = a') by congruence.
+  exists (nextinstr rs1); split.
+  apply exec_straight_one. rewrite H. simpl. rewrite H8. 
+  unfold exec_store. rewrite H7; auto with ppcgen. rewrite D. auto. auto.
+  apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen.
+  intros.
+  assert (Val.add (rs1 r1) (eval_shift_addr sa rs1) = a') by congruence.
+  exists (nextinstr rs1); split.
+  apply exec_straight_one. rewrite H. simpl. rewrite H8. 
+  unfold exec_store. rewrite H7; auto with ppcgen. rewrite D. auto. auto.
+  apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen.
 Qed.
 
 Lemma transl_store_float_correct:
   forall (mk_instr: freg -> ireg -> int -> instruction)
          (is_immed: int -> bool)
-         (rd: mreg) addr args k ms sp rs m chunk a m',
-  (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset),
-    exec_instr ge c (mk_instr r1 r2 n) rs1 m =
-    exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) ->
+         (rd: mreg) addr args k ms sp rs m1 chunk a m2 m1',
+  (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset) m2',
+   exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m1' = OK (nextinstr rs1) m2' ->
+   exists rs2,
+   exec_instr ge c (mk_instr r1 r2 n) rs1 m1' = OK rs2 m2'
+   /\ (forall (r: preg), r <> FR3 -> rs2 r = nextinstr rs1 r)) ->
   agree ms sp rs ->
   map mreg_type args = type_of_addressing addr ->
   mreg_type rd = Tfloat ->
   eval_addressing ge sp addr (map ms args) = Some a ->
-  Mem.storev chunk m a (ms rd) = Some m' ->
-  exists rs',
-    exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m
-                        k rs' m'
-  /\ agree ms sp rs'.
+  Mem.storev chunk m1 a (ms rd) = Some m2 ->
+  Mem.extends m1 m1' ->
+  exists m2',
+    Mem.extends m2 m2' /\
+    exists rs',
+    exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m1'
+                        k rs' m2'
+    /\ agree (undef_temps ms) sp rs'.
 Proof.
   intros. unfold transl_load_store_float.
-  exploit eval_addressing_weaken. eauto. intros. 
+  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
+  intros [a' [A B]].
+  exploit preg_val; eauto. instantiate (1 := rd). intros C.
+  exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]].
+  exploit eval_addressing_weaken. eexact A. intros F.
+  exists m2'; split; auto.
   apply transl_load_store_correct with ms; auto.
-  intros. exists (nextinstr rs1); split.
-  apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5.
-  unfold exec_store. rewrite <- (freg_val ms sp rs1); auto.
-  rewrite H4. auto. auto.
-  auto with ppcgen.
+  intros.
+  assert (Val.add (rs1 r1) (Vint n) = a') by congruence.
+  exploit (H fn (freg_of rd) r1 n rs1 m2').
+  unfold exec_store. rewrite H8. rewrite H7; auto with ppcgen. rewrite D. auto.
+  intros [rs2 [P Q]].
+  exists rs2; split. apply exec_straight_one. auto. rewrite Q; auto with ppcgen.
+  apply agree_exten_temps with rs; auto.
+  intros. rewrite Q; auto with ppcgen. Simpl. apply H7; auto with ppcgen.
 Qed.
 
 End STRAIGHTLINE.
diff --git a/arm/ConstpropOp.v b/arm/ConstpropOp.v
index e55c7f99..a56a5ef8 100644
--- a/arm/ConstpropOp.v
+++ b/arm/ConstpropOp.v
@@ -345,9 +345,6 @@ Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx),
   | eval_static_operation_case49:
       forall n1,
       eval_static_operation_cases (Ofloatofint) (I n1 :: nil)
-  | eval_static_operation_case50:
-      forall n1,
-      eval_static_operation_cases (Ofloatofintu) (I n1 :: nil)
   | eval_static_operation_case51:
       forall c vl,
       eval_static_operation_cases (Ocmp c) (vl)
@@ -458,8 +455,6 @@ Definition eval_static_operation_match (op: operation) (vl: list approx) :=
       eval_static_operation_case48 n1
   | Ofloatofint, I n1 :: nil =>
       eval_static_operation_case49 n1
-  | Ofloatofintu, I n1 :: nil =>
-      eval_static_operation_case50 n1
   | Ocmp c, vl =>
       eval_static_operation_case51 c vl
   | Oshrximm n, I n1 :: nil =>
@@ -568,8 +563,6 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
       I(Float.intoffloat n1)
   | eval_static_operation_case49 n1 =>
       F(Float.floatofint n1)
-  | eval_static_operation_case50 n1 =>
-      F(Float.floatofintu n1)
   | eval_static_operation_case51 c vl =>
       match eval_static_condition c vl with
       | None => Unknown
diff --git a/arm/Op.v b/arm/Op.v
index 1f26a728..606281dd 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -110,10 +110,8 @@ Inductive operation : Type :=
   | Odivf: operation                    (**r [rd = r1 / r2] *)
   | Osingleoffloat: operation           (**r [rd] is [r1] truncated to single-precision float *)
 (*c Conversions between int and float: *)
-  | Ointoffloat: operation              (**r [rd = int_of_float(r1)] *)
-  | Ointuoffloat: operation             (**r [rd = unsigned_int_of_float(r1)] *)
+  | Ointoffloat: operation              (**r [rd = signed_int_of_float(r1)] *)
   | Ofloatofint: operation              (**r [rd = float_of_signed_int(r1)] *)
-  | Ofloatofintu: operation             (**r [rd = float_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
   | Ocmp: condition -> operation.       (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
 
@@ -282,16 +280,9 @@ Definition eval_operation
   | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2))
   | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2))
   | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2))
-  | Osingleoffloat, v1 :: nil =>
-      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))
+  | Osingleoffloat, v1 :: nil => Some (Val.singleoffloat v1)
+  | Ointoffloat, Vfloat f1 :: nil => Some (Vint (Float.intoffloat f1))
+  | Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1))
   | Ocmp c, _ =>
       match eval_condition c vl with
       | None => None
@@ -493,9 +484,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Osingleoffloat => (Tfloat :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
-  | Ointuoffloat => (Tfloat :: nil, Tint)
   | Ofloatofint => (Tint :: nil, Tfloat)
-  | Ofloatofintu => (Tint :: nil, Tfloat)
   | Ocmp c => (type_of_condition c, Tint)
   end.
 
@@ -659,9 +648,7 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val :
   | Odivf, v1::v2::nil => Val.divf v1 v2
   | 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
   | Ocmp c, _ => eval_condition_total c vl
   | _, _ => Vundef
   end.
@@ -919,3 +906,70 @@ Lemma type_op_for_binary_addressing:
 Proof.
   intros. destruct addr; simpl in H; reflexivity || omegaContradiction.
 Qed.
+
+(** Two-address operations.  There are none in the ARM 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/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 9e1cae75..4f470cef 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -79,6 +79,11 @@ let float_reg_name = function
 let ireg oc r = output_string oc (int_reg_name r)
 let freg oc r = output_string oc (float_reg_name r)
 
+let preg oc = function
+  | IR r -> ireg oc r
+  | FR r -> freg oc r
+  | _    -> assert false
+
 let condition_name = function
   | CReq -> "eq"
   | CRne -> "ne"
@@ -417,30 +422,8 @@ let print_instruction oc labels = function
       fprintf oc "	dvfd	%a, %a, %a\n" freg r1 freg r2 freg r3; 1
   | Pfixz(r1, r2) ->
       fprintf oc "	fixz	%a, %a\n" ireg r1 freg r2; 1
-  | Pfixzu(r1, r2) ->
-      (* F3 = second float temporary is unused at this point,
-         but this should be reflected in the proof *)
-      let lbl = label_float 2147483648.0 in
-      let lbl2 = new_label() in
-      fprintf oc "	ldfd	f3, .L%d\n" lbl;
-      fprintf oc "	cmfe	%a, f3\n" freg r2;
-      fprintf oc "	fixltz	%a, %a\n" ireg r1 freg r2;
-      fprintf oc "	blt	.L%d\n" lbl2;
-      fprintf oc "	sufd	f3, %a, f3\n" freg r2;
-      fprintf oc "	fixz	%a, f3\n" ireg r1;
-      fprintf oc "	eor	%a, %a, #-2147483648\n" ireg r1 ireg r1;
-      fprintf oc ".L%d\n" lbl2;
-      7
   | Pfltd(r1, r2) ->
       fprintf oc "	fltd	%a, %a\n" freg r1 ireg r2; 1
-  | Pfltud(r1, r2) ->
-      fprintf oc "	fltd	%a, %a\n" freg r1 ireg r2;
-      fprintf oc "	cmp	%a, #0\n" ireg r2;
-      (* F3 = second float temporary is unused at this point,
-         but this should be reflected in the proof *)
-      let lbl = label_float 4294967296.0 in
-      fprintf oc "	ldfltd	f3, .L%d\n" lbl;
-      fprintf oc "	adfltd  %a, %a, f3\n" freg r1 freg r1; 4
   | Pldfd(r1, r2, n) ->
       fprintf oc "	ldfd	%a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1
   | Pldfs(r1, r2, n) ->
@@ -465,8 +448,6 @@ let print_instruction oc labels = function
   | Pstfd(r1, r2, n) ->
       fprintf oc "	stfd	%a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1
   | Pstfs(r1, r2, n) ->
-      (* F3 = second float temporary is unused at this point,
-         but this should be reflected in the proof *)
       fprintf oc "	mvfs	f3, %a\n" freg r1;
       fprintf oc "	stfs	f3, [%a, #%a]\n" ireg r2 coqint n; 2
   | Psufd(r1, r2, r3) ->
diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml
index 75d8593b..dff4e4f9 100644
--- a/arm/PrintOp.ml
+++ b/arm/PrintOp.ml
@@ -38,7 +38,7 @@ let print_condition reg pp = function
       fprintf pp "%a %su %a" reg r1 (comparison_name c) reg r2
   | (Ccompshift(c, s), [r1;r2]) ->
       fprintf pp "%a %ss %a %a" reg r1 (comparison_name c) reg r2 shift s
-  | (Ccompu(c, s), [r1;r2]) ->
+  | (Ccompushift(c, s), [r1;r2]) ->
       fprintf pp "%a %su %a %a" reg r1 (comparison_name c) reg r2 shift s
   | (Ccompimm(c, n), [r1]) ->
       fprintf pp "%a %ss %ld" reg r1 (comparison_name c) (camlint_of_coqint n)
@@ -68,7 +68,7 @@ let print_operation reg pp = function
   | Oaddimm n, [r1] -> fprintf pp "%a + %ld" reg r1 (camlint_of_coqint n)
   | Osub, [r1;r2] -> fprintf pp "%a - %a" reg r1 reg r2
   | Osubshift s, [r1;r2] -> fprintf pp "%a - %a %a" reg r1 reg r2 shift s
-  | Osubrshift s, [r1;r2] -> fprintf pp "%a %a - %a" reg r2 shift s reg r1
+  | Orsubshift s, [r1;r2] -> fprintf pp "%a %a - %a" reg r2 shift s reg r1
   | Orsubimm n, [r1] -> fprintf pp "%ld - %a" (camlint_of_coqint n) reg r1
   | Omul, [r1;r2] -> fprintf pp "%a * %a" reg r1 reg r2
   | Odiv, [r1;r2] -> fprintf pp "%a /s %a" reg r1 reg r2
@@ -99,9 +99,7 @@ let print_operation reg pp = function
   | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2
   | 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
   | Ocmp c, args -> print_condition reg pp (c, args)
   | _ -> fprintf pp "<bad operator>"
 
@@ -111,5 +109,3 @@ let print_addressing reg pp = function
   | Aindexed2shift s, [r1; r2] -> fprintf pp "%a + %a %a" reg r1 reg r2 shift s
   | Ainstack ofs, [] -> fprintf pp "stack(%ld)" (camlint_of_coqint ofs)
   | _ -> fprintf pp "<bad addressing>"
-
-
diff --git a/arm/SelectOp.v b/arm/SelectOp.v
index 66c12999..df2413a6 100644
--- a/arm/SelectOp.v
+++ b/arm/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
@@ -788,22 +796,24 @@ Definition same_expr_pure (e1 e2: expr) :=
 Definition or (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Oshift (Olsl n1) (t1:::Enil), Eop (Oshift (Olsr n2) (t2:::Enil)) => ...
+  | Eop (Oshift (Olsr n1) (t1:::Enil), Eop (Oshift (Olsl n2) (t2:::Enil)) => ...
   | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil)
   | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil)
   | _, _ => Eop Oor (e1:::e2:::Enil)
   end.
 *)
 
-(* TODO: symmetric of first case *)
-
 Inductive or_cases: forall (e1: expr) (e2: expr), Type :=
   | or_case1:
       forall n1 t1 n2 t2,
       or_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) (Eop (Oshift (Slsr n2)) (t2:::Enil))
   | or_case2:
+      forall n1 t1 n2 t2,
+      or_cases (Eop (Oshift (Slsr n1)) (t1:::Enil)) (Eop (Oshift (Slsl n2)) (t2:::Enil))
+  | or_case3:
       forall s t1 t2,
       or_cases (Eop (Oshift s) (t1:::Enil)) (t2)
-  | or_case3:
+  | or_case4:
       forall t1 s t2,
       or_cases (t1) (Eop (Oshift s) (t2:::Enil))
   | or_default:
@@ -814,10 +824,12 @@ Definition or_match (e1: expr) (e2: expr) :=
   match e1 as z1, e2 as z2 return or_cases z1 z2 with
   | Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) =>
       or_case1 n1 t1 n2 t2
+  | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) =>
+      or_case2 n1 t1 n2 t2
   | Eop (Oshift s) (t1:::Enil), t2 =>
-      or_case2 s t1 t2
+      or_case3 s t1 t2
   | t1, Eop (Oshift s) (t2:::Enil) =>
-      or_case3 t1 s t2
+      or_case4 t1 s t2
   | e1, e2 =>
       or_default e1 e2
   end.
@@ -829,9 +841,14 @@ Definition or (e1: expr) (e2: expr) :=
       && same_expr_pure t1 t2
       then Eop (Oshift (Sror n2)) (t1:::Enil)
       else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil)
-  | or_case2 s t1 t2 =>
+  | or_case2 n1 t1 n2 t2 =>
+      if Int.eq (Int.add (s_amount n2) (s_amount n1)) Int.iwordsize
+      && same_expr_pure t1 t2
+      then Eop (Oshift (Sror n1)) (t1:::Enil)
+      else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil)
+  | or_case3 s t1 t2 =>
       Eop (Oorshift s) (t2:::t1:::Enil)
-  | or_case3 t1 s t2 =>
+  | or_case4 t1 s t2 =>
       Eop (Oorshift s) (t1:::t2:::Enil)
   | or_default e1 e2 =>
       Eop Oor (e1:::e2:::Enil)
@@ -919,118 +936,6 @@ Definition shr (e1: expr) (e2: expr) :=
       Eop Oshr (e1:::e2:::Enil)
   end.
 
-(** ** Truncations and sign extensions *)
-
-Inductive cast8signed_cases: forall (e1: expr), Type :=
-  | cast8signed_case1:
-      forall (e2: expr),
-      cast8signed_cases (Eop Ocast8signed (e2 ::: Enil))
-  | 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
-  | e1 =>
-      cast8signed_default e1
-  end.
-
-Definition cast8signed (e: expr) := 
-  match cast8signed_match e with
-  | cast8signed_case1 e1 => 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_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
-  | e1 =>
-      cast8unsigned_default e1
-  end.
-
-Definition cast8unsigned (e: expr) := 
-  match cast8unsigned_match e with
-  | cast8unsigned_case1 e1 => 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_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
-  | e1 =>
-      cast16signed_default e1
-  end.
-
-Definition cast16signed (e: expr) := 
-  match cast16signed_match e with
-  | cast16signed_case1 e1 => 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_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
-  | e1 =>
-      cast16unsigned_default e1
-  end.
-
-Definition cast16unsigned (e: expr) := 
-  match cast16unsigned_match e with
-  | cast16unsigned_case1 e1 => 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_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
-  | e1 =>
-      singleoffloat_default e1
-  end.
-
-Definition singleoffloat (e: expr) := 
-  match singleoffloat_match e with
-  | singleoffloat_case1 e1 => e
-  | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil)
-  end.
-
 (** ** Comparisons *)
 
 (*
@@ -1106,20 +1011,39 @@ Definition compu (c: comparison) (e1: expr) (e2: expr) :=
 Definition compf (c: comparison) (e1: expr) (e2: expr) :=
   Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).
 
-(** ** Other operators, not optimized. *)
+(** ** Non-optimized operators. *)
 
+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 (Orsubimm 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 addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
 Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
 Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
 Definition divf (e1 e2: expr) :=  Eop Odivf (e1 ::: e2 ::: Enil).
 
+(** ** Conversions between unsigned ints and floats *)
+
+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) :=
+  let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in
+  Elet e
+    (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
+      (floatofint (Eletvar O))
+      (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)).
+
 (** ** Recognition of addressing modes for load and store operations *)
 
 (*
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index b2603466..c8f177b3 100644
--- a/arm/SelectOpproof.v
+++ b/arm/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) ->
@@ -644,7 +662,18 @@ Proof.
   destruct n1; auto. destruct n2; auto. auto. 
   EvalOp. econstructor. EvalOp. simpl. reflexivity.
   econstructor; eauto with evalexpr. 
-  simpl. congruence. 
+  simpl. congruence.
+  caseEq (Int.eq (Int.add (s_amount n2) (s_amount n1)) Int.iwordsize
+          && same_expr_pure t1 t2); intro.
+  destruct (andb_prop _ _ H1).
+  generalize (Int.eq_spec (Int.add (s_amount n2) (s_amount n1)) Int.iwordsize).
+  rewrite H4. intro. 
+  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. 
+  simpl. EvalOp. simpl. decEq. decEq. rewrite Int.or_commut. apply Int.or_ror.
+  destruct n2; auto. destruct n1; auto. auto. 
+  EvalOp. econstructor. EvalOp. simpl. reflexivity.
+  econstructor; eauto with evalexpr. 
+  simpl. congruence.
   EvalOp. simpl. rewrite Int.or_commut. congruence.
   EvalOp. simpl. congruence.
   EvalOp. 
@@ -702,55 +731,31 @@ 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. vm_compute; auto.
-  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. vm_compute; auto.
-  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. vm_compute; auto.
-  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. vm_compute; auto.
-  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.
-  EvalOp.
-Qed.
+Proof. TrivialOp singleoffloat. Qed. 
 
 Theorem eval_comp_int:
   forall le c a x b y,
@@ -894,30 +899,6 @@ Theorem eval_absf:
   eval_expr ge sp e m le (absf a) (Vfloat (Float.abs x)).
 Proof. intros; unfold absf; EvalOp. Qed.
 
-Theorem eval_intoffloat:
-  forall le a x,
-  eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)).
-Proof. intros; unfold intoffloat; EvalOp. Qed.
-
-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.
-
-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.
-
-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.
-
 Theorem eval_addf:
   forall le a x b y,
   eval_expr ge sp e m le a (Vfloat x) ->
@@ -946,6 +927,60 @@ Theorem eval_divf:
   eval_expr ge sp e m le (divf a b) (Vfloat (Float.div x y)).
 Proof. intros; unfold divf; EvalOp. Qed.
 
+Theorem eval_intoffloat:
+  forall le a x,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)).
+Proof. TrivialOp intoffloat. Qed.
+
+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. 
+  econstructor. eauto. 
+  set (f := 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 f).
+  econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
+  simpl. auto.
+  caseEq (Float.cmp Clt x f); 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.
+
+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. 
+  econstructor. eauto. 
+  set (f := Float.floatofintu Float.ox8000_0000).
+  assert (eval_expr ge sp e m (Vint x :: le) (Eletvar O) (Vint x)).
+    constructor. auto. 
+  apply eval_Econdition with (v1 := Int.ltu x Float.ox8000_0000).
+  econstructor. constructor. eauto. constructor.
+  simpl. auto.
+  caseEq (Int.ltu x Float.ox8000_0000); intros.
+  rewrite Float.floatofintu_floatofint_1; auto.
+  apply eval_floatofint; auto.
+  rewrite Float.floatofintu_floatofint_2; auto.
+  fold f. apply eval_addf. apply eval_floatofint. 
+  rewrite Int.sub_add_opp. apply eval_addimm; auto.
+  EvalOp.
+Qed.
+
 Lemma eval_addressing:
   forall le chunk a v b ofs,
   eval_expr ge sp e m le a v ->
diff --git a/arm/linux/Conventions1.v b/arm/linux/Conventions1.v
index 703dc12d..fdccf750 100644
--- a/arm/linux/Conventions1.v
+++ b/arm/linux/Conventions1.v
@@ -56,6 +56,9 @@ Definition float_temporaries := FT1 :: FT2 :: nil.
 Definition temporaries := 
   R IT1 :: R IT2 :: R FT1 :: R FT2 :: nil.
 
+Definition dummy_int_reg := R0.     (**r Used in [Coloring]. *)
+Definition dummy_float_reg := F0.   (**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
@@ -641,4 +644,3 @@ Proof.
   intro; simpl. ElimOrEq; reflexivity.
   intro; simpl. ElimOrEq; reflexivity.
 Qed.
-