Revised Stacking and Asmgen passes and Mach semantics:

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



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

1 files changed, 391 insertions, 849 deletions

diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 658fc98..8fc8a7e 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -12,8 +12,9 @@
 
 (** Correctness proof for ARM code generation: auxiliary results. *)
 
-Require Import Axioms.
+(*Require Import Axioms.*)
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
@@ -24,455 +25,44 @@ Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
 Require Import Mach.
-Require Import Machsem.
-Require Import Machtyping.
 Require Import Asm.
 Require Import Asmgen.
 Require Import Conventions.
+Require Import Asmgenproof0.
 
-(** * Correspondence between Mach registers and PPC registers *)
+(** Useful properties of the R14 registers. *)
 
-Hint Extern 2 (_ <> _) => discriminate: ppcgen.
-
-(** Mapping from Mach registers to PPC registers. *)
-
-Lemma preg_of_injective:
-  forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
-Proof.
-  destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
-Qed.
-
-Lemma ireg_of_not_IR13:
-  forall r, ireg_of r <> IR13.
-Proof.
-  destruct r; simpl; congruence.
-Qed.
-
-Lemma ireg_of_not_IR14:
-  forall r, ireg_of r <> IR14.
-Proof.
-  destruct r; simpl; congruence.
-Qed.
-
-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_IR14:
-  forall r, preg_of r <> IR14.
-Proof.
-  unfold preg_of; intros. destruct (mreg_type r).
-  generalize (ireg_of_not_IR14 r); congruence.
-  congruence.
-Qed.
-
-Lemma preg_of_not_PC:
-  forall r, preg_of r <> PC.
-Proof.
-  intros. unfold preg_of. destruct (mreg_type r); congruence.
-Qed.
-
-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. *)
-
-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 -> 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.
-  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 ->
-  Val.lessdef (ms r) rs#(ireg_of r).
-Proof.
-  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 ->
-  Val.lessdef (ms r) rs#(freg_of r).
-Proof.
-  intros. generalize (preg_val _ _ _ r H). unfold preg_of. rewrite H0. auto.
-Qed.
-
-Lemma sp_val:
-  forall ms sp rs,
-  agree ms sp rs ->
-  sp = rs#IR13.
-Proof.
-  intros. destruct H; auto.
-Qed.
-
-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.
-  intros. destruct r; reflexivity.
-Qed.
-
-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, important_preg r = true -> rs'#r = rs#r) ->
-  agree ms sp rs'.
-Proof.
-  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 rs',
-  agree ms sp rs ->
-  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. 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.
-
-Lemma agree_set_other:
-  forall ms sp rs r v,
-  agree ms sp rs ->
-  important_preg r = false ->
-  agree ms sp (rs#r <- v).
-Proof.
-  intros. apply agree_exten with rs. auto.
-  intros. apply Pregmap.gso. congruence.
-Qed.
-
-Lemma agree_nextinstr:
-  forall ms sp rs,
-  agree ms sp rs -> agree ms sp (nextinstr rs).
+Lemma ireg_of_not_R14:
+  forall m r, ireg_of m = OK r -> IR r <> IR IR14.
 Proof.
-  intros. unfold nextinstr. apply agree_set_other. auto. auto.
+  intros. erewrite <- ireg_of_eq; eauto with asmgen.
 Qed.
+Hint Resolve ireg_of_not_R14: asmgen.
 
-Definition nontemp_preg (r: preg) : bool :=
-  match r with
-  | IR IR14 => false
-  | IR IR10 => false
-  | IR IR12 => false
-  | IR _ => true
-  | FR FR6 => false
-  | FR FR7 => 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.
-  congruence.
-Qed.
-
-Hint Resolve nontemp_diff: ppcgen.
-
-Lemma nontemp_important:
-  forall r, nontemp_preg r = true -> important_preg r = true.
+Lemma ireg_of_not_R14':
+  forall m r, ireg_of m = OK r -> r <> IR14.
 Proof.
-  unfold nontemp_preg, important_preg; destruct r; auto. destruct i; auto.
+  intros. generalize (ireg_of_not_R14 _ _ H). congruence.
 Qed.
+Hint Resolve ireg_of_not_R14': asmgen.
 
-Hint Resolve nontemp_important: ppcgen.
+(** Useful simplification tactic *)
 
-Remark undef_regs_1:
-  forall l ms r, ms r = Vundef -> Mach.undef_regs l ms r = Vundef.
-Proof.
-  induction l; simpl; intros. auto. apply IHl. unfold Regmap.set.
-  destruct (RegEq.eq r a); congruence.
-Qed.
+Ltac Simplif :=
+  ((rewrite nextinstr_inv by eauto with asmgen)
+  || (rewrite nextinstr_inv1 by eauto with asmgen)
+  || (rewrite Pregmap.gss)
+  || (rewrite nextinstr_pc)
+  || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen.
 
-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.
-  induction l; simpl; intros. auto.
-  rewrite IHl. apply Regmap.gso. intuition. intuition.
-Qed.
-
-Lemma agree_exten_temps:
-  forall ms sp rs rs',
-  agree ms sp rs ->
-  (forall r, nontemp_preg r = true -> rs'#r = rs#r) ->
-  agree (undef_temps ms) sp rs'.
-Proof.
-  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.
-
-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.
+Ltac Simpl := repeat Simplif.
 
-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.
-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. apply nextinstr_inv. red; intro; subst; discriminate.
-Qed.
-
-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. apply preg_of_not_PC. 
-Qed.
-
-(** Connection between Mach and Asm calling conventions for external
-    functions. *)
-
-Lemma extcall_arg_match:
-  forall ms sp rs m m' l v,
-  agree ms sp rs ->
-  Machsem.extcall_arg ms m sp l v ->
-  Mem.extends m m' ->
-  exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'.
-Proof.
-  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 m', agree ms sp rs -> Mem.extends m m' ->
-  forall ll vl,
-  list_forall2 (Machsem.extcall_arg ms m sp) ll vl ->
-  exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'.
-Proof.
-  induction 3; intros. 
-  exists (@nil val); split. constructor. constructor.
-  exploit extcall_arg_match; eauto. intros [v1' [A B]].
-  destruct IHlist_forall2 as [vl' [C D]].
-  exists (v1' :: vl'); split; constructor; auto.
-Qed.
-
-Lemma extcall_arguments_match:
-  forall ms m sp rs sg args m',
-  agree ms sp rs ->
-  Machsem.extcall_arguments ms m sp sg args ->
-  Mem.extends m m' ->
-  exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
-Proof.
-  unfold Machsem.extcall_arguments, Asm.extcall_arguments; intros.
-  eapply extcall_args_match; eauto.
-Qed.
-
-(** Translation of arguments to annotations. *)
-
-Lemma annot_arg_match:
-  forall ms sp rs m m' p v,
-  agree ms sp rs ->
-  Mem.extends m m' ->
-  Machsem.annot_arg ms m sp p v ->
-  exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'.
-Proof.
-  intros. inv H1; simpl.
-(* reg *)
-  exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto.
-(* stack *)
-  exploit Mem.load_extends; eauto. intros [v' [A B]].
-  exists v'; split; auto. 
-  inv H. econstructor; eauto. 
-Qed.
-
-Lemma annot_arguments_match:
-  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
-  forall pl vl,
-  Machsem.annot_arguments ms m sp pl vl ->
-  exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl'
-           /\ Val.lessdef_list vl vl'.
-Proof.
-  induction 3; intros. 
-  exists (@nil val); split. constructor. constructor.
-  exploit annot_arg_match; eauto. intros [v1' [A B]].
-  destruct IHlist_forall2 as [vl' [C D]].
-  exists (v1' :: vl'); split; constructor; auto.
-Qed.
-
-(** * Execution of straight-line code *)
+(** * Correctness of ARM constructor functions *)
 
-Section STRAIGHTLINE.
+Section CONSTRUCTORS.
 
 Variable ge: genv.
-Variable fn: code.
-
-(** Straight-line code is composed of PPC instructions that execute
-  in sequence (no branches, no function calls and returns).
-  The following inductive predicate relates the machine states
-  before and after executing a straight-line sequence of instructions.
-  Instructions are taken from the first list instead of being fetched
-  from memory. *)
-
-Inductive exec_straight: code -> regset -> mem -> 
-                         code -> regset -> mem -> Prop :=
-  | exec_straight_one:
-      forall i1 c rs1 m1 rs2 m2,
-      exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
-      rs2#PC = Val.add rs1#PC Vone ->
-      exec_straight (i1 :: c) rs1 m1 c rs2 m2
-  | exec_straight_step:
-      forall i c rs1 m1 rs2 m2 c' rs3 m3,
-      exec_instr ge fn i rs1 m1 = OK rs2 m2 ->
-      rs2#PC = Val.add rs1#PC Vone ->
-      exec_straight c rs2 m2 c' rs3 m3 ->
-      exec_straight (i :: c) rs1 m1 c' rs3 m3.
-
-Lemma exec_straight_trans:
-  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
-  exec_straight c1 rs1 m1 c2 rs2 m2 ->
-  exec_straight c2 rs2 m2 c3 rs3 m3 ->
-  exec_straight c1 rs1 m1 c3 rs3 m3.
-Proof.
-  induction 1; intros.
-  apply exec_straight_step with rs2 m2; auto.
-  apply exec_straight_step with rs2 m2; auto.
-Qed.
-
-Lemma exec_straight_two:
-  forall i1 i2 c rs1 m1 rs2 m2 rs3 m3,
-  exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
-  exec_instr ge fn i2 rs2 m2 = OK rs3 m3 ->
-  rs2#PC = Val.add rs1#PC Vone ->
-  rs3#PC = Val.add rs2#PC Vone ->
-  exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3.
-Proof.
-  intros. apply exec_straight_step with rs2 m2; auto.
-  apply exec_straight_one; auto.
-Qed.
-
-Lemma exec_straight_three:
-  forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4,
-  exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
-  exec_instr ge fn i2 rs2 m2 = OK rs3 m3 ->
-  exec_instr ge fn i3 rs3 m3 = OK rs4 m4 ->
-  rs2#PC = Val.add rs1#PC Vone ->
-  rs3#PC = Val.add rs2#PC Vone ->
-  rs4#PC = Val.add rs3#PC Vone ->
-  exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4.
-Proof.
-  intros. apply exec_straight_step with rs2 m2; auto.
-  eapply exec_straight_two; eauto.
-Qed.
-
-Lemma exec_straight_four:
-  forall i1 i2 i3 i4 c rs1 m1 rs2 m2 rs3 m3 rs4 m4 rs5 m5,
-  exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
-  exec_instr ge fn i2 rs2 m2 = OK rs3 m3 ->
-  exec_instr ge fn i3 rs3 m3 = OK rs4 m4 ->
-  exec_instr ge fn i4 rs4 m4 = OK rs5 m5 ->
-  rs2#PC = Val.add rs1#PC Vone ->
-  rs3#PC = Val.add rs2#PC Vone ->
-  rs4#PC = Val.add rs3#PC Vone ->
-  rs5#PC = Val.add rs4#PC Vone ->
-  exec_straight (i1 :: i2 :: i3 :: i4 :: c) rs1 m1 c rs5 m5.
-Proof.
-  intros. apply exec_straight_step with rs2 m2; auto.
-  eapply exec_straight_three; eauto.
-Qed.
-
-(** * Correctness of ARM constructor functions *)
+Variable fn: function.
 
 (** Decomposition of an integer constant *)
 
@@ -606,12 +196,12 @@ Lemma iterate_op_correct:
   forall op1 op2 (f: val -> int -> val) (rs: regset) (r: ireg) m v0 n k,
   (forall (rs:regset) n,
     exec_instr ge fn (op2 (SOimm n)) rs m =
-    OK (nextinstr (rs#r <- (f (rs#r) n))) m) ->
+    Next (nextinstr (rs#r <- (f (rs#r) n))) m) ->
   (forall n,
     exec_instr ge fn (op1 (SOimm n)) rs m =
-    OK (nextinstr (rs#r <- (f v0 n))) m) ->
+    Next (nextinstr (rs#r <- (f v0 n))) m) ->
   exists rs',
-     exec_straight (iterate_op op1 op2 (decompose_int n) k) rs m  k rs' m
+     exec_straight ge fn (iterate_op op1 op2 (decompose_int n) k) rs m  k rs' m
   /\ rs'#r = List.fold_left f (decompose_int n) v0
   /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
@@ -623,8 +213,7 @@ Proof.
   (* base case *)
   intros; simpl. econstructor.
   split. apply exec_straight_one. rewrite SEM1. reflexivity. reflexivity.
-  split. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. auto.
-  intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen.
+  intuition Simpl.
   (* inductive case *)
   intros. 
   rewrite List.map_app. simpl. rewrite app_ass. simpl. 
@@ -632,9 +221,8 @@ Proof.
   econstructor.
   split. eapply exec_straight_trans. eexact A. apply exec_straight_one.
   rewrite SEM2. reflexivity. reflexivity.
-  split. rewrite fold_left_app; simpl. rewrite nextinstr_inv; auto with ppcgen.
-  rewrite Pregmap.gss. rewrite B. auto.
-  intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen.
+  split. rewrite fold_left_app; simpl. Simpl. rewrite B. auto. 
+  intros; Simpl.
 Qed.
   
 (** Loading a constant. *)
@@ -642,7 +230,7 @@ Qed.
 Lemma loadimm_correct:
   forall r n k rs m,
   exists rs',
-     exec_straight (loadimm r n k) rs m  k rs' m
+     exec_straight ge fn (loadimm r n k) rs m  k rs' m
   /\ rs'#r = Vint n
   /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
@@ -667,7 +255,7 @@ Qed.
 Lemma addimm_correct:
   forall r1 r2 n k rs m,
   exists rs',
-     exec_straight (addimm r1 r2 n k) rs m  k rs' m
+     exec_straight ge fn (addimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = Val.add rs#r2 (Vint n)
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
@@ -693,9 +281,8 @@ Qed.
 
 Lemma andimm_correct:
   forall r1 r2 n k rs m,
-  r2 <> IR14 ->
   exists rs',
-     exec_straight (andimm r1 r2 n k) rs m  k rs' m
+     exec_straight ge fn (andimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = Val.and rs#r2 (Vint n)
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
@@ -704,7 +291,7 @@ Proof.
   case (is_immed_arith n).
   exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))).
   split. apply exec_straight_one; auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
+  split. rewrite nextinstr_inv; auto with asmgen. apply Pregmap.gss. 
   intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
   (* bic - bic* *)
   replace (Val.and (rs r2) (Vint n))
@@ -720,7 +307,7 @@ Qed.
 Lemma rsubimm_correct:
   forall r1 r2 n k rs m,
   exists rs',
-     exec_straight (rsubimm r1 r2 n k) rs m  k rs' m
+     exec_straight ge fn (rsubimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = Val.sub (Vint n) rs#r2
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
@@ -741,7 +328,7 @@ Qed.
 Lemma orimm_correct:
   forall r1 r2 n k rs m,
   exists rs',
-     exec_straight (orimm r1 r2 n k) rs m  k rs' m
+     exec_straight ge fn (orimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = Val.or rs#r2 (Vint n)
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
@@ -760,7 +347,7 @@ Qed.
 Lemma xorimm_correct:
   forall r1 r2 n k rs m,
   exists rs',
-     exec_straight (xorimm r1 r2 n k) rs m  k rs' m
+     exec_straight ge fn (xorimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = Val.xor rs#r2 (Vint n)
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
@@ -780,7 +367,7 @@ Lemma loadind_int_correct:
   forall (base: ireg) ofs dst (rs: regset) m v k,
   Mem.loadv Mint32 m (Val.add rs#base (Vint ofs)) = Some v ->
   exists rs',
-     exec_straight (loadind_int base ofs dst k) rs m k rs' m
+     exec_straight ge fn (loadind_int base ofs dst k) rs m k rs' m
   /\ rs'#dst = v
   /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r.
 Proof.
@@ -788,23 +375,21 @@ Proof.
   exists (nextinstr (rs#dst <- v)).
   split. apply exec_straight_one. simpl. 
     unfold exec_load. rewrite H. auto. auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  intuition Simpl.
   exploit addimm_correct. intros [rs' [A [B C]]].
   exists (nextinstr (rs'#dst <- v)).
   split. eapply exec_straight_trans. eauto. apply exec_straight_one.
     simpl. unfold exec_load. rewrite B.
     rewrite Val.add_assoc. simpl. rewrite Int.add_zero.
     rewrite H. auto. auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  intuition Simpl.
 Qed.
 
 Lemma loadind_float_correct:
   forall (base: ireg) ofs dst (rs: regset) m v k,
   Mem.loadv Mfloat64al32 m (Val.add rs#base (Vint ofs)) = Some v ->
   exists rs',
-     exec_straight (loadind_float base ofs dst k) rs m k rs' m
+     exec_straight ge fn (loadind_float base ofs dst k) rs m k rs' m
   /\ rs'#dst = v
   /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r.
 Proof.
@@ -812,33 +397,29 @@ Proof.
   exists (nextinstr (rs#dst <- v)).
   split. apply exec_straight_one. simpl. 
     unfold exec_load. rewrite H. auto. auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  intuition Simpl.
   exploit addimm_correct. eauto. intros [rs' [A [B C]]].
   exists (nextinstr (rs'#dst <- v)).
   split. eapply exec_straight_trans. eauto. apply exec_straight_one.
     simpl. unfold exec_load. rewrite B.
     rewrite Val.add_assoc. simpl. 
     rewrite Int.add_zero. rewrite H. auto. auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  intuition Simpl.
 Qed.
 
 Lemma loadind_correct:
-  forall (base: ireg) ofs ty dst k (rs: regset) m v,
+  forall (base: ireg) ofs ty dst k c (rs: regset) m v,
+  loadind base ofs ty dst k = OK c ->
   Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v ->
-  mreg_type dst = ty ->
   exists rs',
-     exec_straight (loadind base ofs ty dst k) rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of dst) = v
   /\ forall r, r <> PC -> r <> IR14 -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros. unfold loadind. 
-  assert (preg_of dst <> PC).
-    unfold preg_of. case (mreg_type dst); discriminate.
-  unfold preg_of. rewrite H0. destruct ty.
-  apply loadind_int_correct; auto.
-  apply loadind_float_correct; auto.
+  unfold loadind; intros.
+  destruct ty; monadInv H.
+  erewrite ireg_of_eq by eauto. apply loadind_int_correct; auto. 
+  erewrite freg_of_eq by eauto. apply loadind_float_correct; auto. 
 Qed.
 
 (** Indexed memory stores. *)
@@ -848,37 +429,36 @@ Lemma storeind_int_correct:
   Mem.storev Mint32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' ->
   src <> IR14 ->
   exists rs',
-     exec_straight (storeind_int src base ofs k) rs m k rs' m'
+     exec_straight ge fn (storeind_int src base ofs k) rs m k rs' m'
   /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r.
 Proof.
   intros; unfold storeind_int. destruct (is_immed_mem_word ofs).
   exists (nextinstr rs).
   split. apply exec_straight_one. simpl. 
     unfold exec_store. rewrite H. auto. auto.
-  intros. rewrite nextinstr_inv; auto.
+  intuition Simpl.
   exploit addimm_correct. eauto. intros [rs' [A [B C]]].
   exists (nextinstr rs').
   split. eapply exec_straight_trans. eauto. apply exec_straight_one.
     simpl. unfold exec_store. rewrite B.
     rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. 
     rewrite H. auto. 
-    congruence. auto with ppcgen. auto.
-  intros. rewrite nextinstr_inv; auto.
+    congruence. auto with asmgen. auto.
+  intuition Simpl.
 Qed.
 
 Lemma storeind_float_correct:
   forall (base: ireg) ofs (src: freg) (rs: regset) m m' k,
   Mem.storev Mfloat64al32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' ->
-  base <> IR14 ->
   exists rs',
-     exec_straight (storeind_float src base ofs k) rs m k rs' m'
+     exec_straight ge fn (storeind_float src base ofs k) rs m k rs' m'
   /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r.
 Proof.
   intros; unfold storeind_float. destruct (is_immed_mem_float ofs).
   exists (nextinstr rs).
   split. apply exec_straight_one. simpl. 
     unfold exec_store. rewrite H. auto. auto.
-  intros. rewrite nextinstr_inv; auto.
+  intuition Simpl.
   exploit addimm_correct. eauto. intros [rs' [A [B C]]].
   exists (nextinstr rs').
   split. eapply exec_straight_trans. eauto. apply exec_straight_one.
@@ -886,22 +466,23 @@ Proof.
     rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. 
     rewrite H. auto.
     congruence. congruence. 
-    auto with ppcgen. 
-  intros. rewrite nextinstr_inv; auto.
+    auto with asmgen.
+  intuition Simpl. 
 Qed.
 
 Lemma storeind_correct:
-  forall (base: ireg) ofs ty src k (rs: regset) m m',
+  forall (base: ireg) ofs ty src k c (rs: regset) m m',
+  storeind src base ofs ty k = OK c ->
   Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' ->
-  mreg_type src = ty ->
-  base <> IR14 ->
   exists rs',
-     exec_straight (storeind src base ofs ty k) rs m k rs' m'
+     exec_straight ge fn c rs m k rs' m'
   /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r.
 Proof.
-  intros. unfold storeind. unfold preg_of in H. rewrite H0 in H. destruct ty.
-  apply storeind_int_correct. auto. auto. auto with ppcgen.
-  apply storeind_float_correct. auto. auto.
+  unfold storeind; intros.
+  destruct ty; monadInv H.
+  erewrite ireg_of_eq  in H0 by eauto. apply storeind_int_correct; auto.
+  assert (IR x <> IR IR14) by eauto with asmgen. congruence.
+  erewrite freg_of_eq in H0 by eauto. apply storeind_float_correct; auto. 
 Qed.
 
 (** Translation of shift immediates *)
@@ -935,11 +516,10 @@ 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', important_preg r' = true -> rs1#r' = rs#r'.
+  /\ forall r', data_preg r' = true -> rs1#r' = rs#r'.
 Proof.
-  intros. unfold rs1. intuition; try reflexivity. 
-  rewrite nextinstr_inv; auto with ppcgen.
-  unfold compare_int. repeat rewrite Pregmap.gso; auto with ppcgen.
+  intros. unfold rs1. intuition; try reflexivity.
+  unfold compare_int. Simpl. 
 Qed.
 
 Lemma compare_float_spec:
@@ -955,43 +535,43 @@ 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', important_preg r' = true -> rs'#r' = rs#r'.
-Proof.
-  intros. unfold rs'. intuition; try reflexivity. 
-  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.
+  /\ forall r', data_preg r' = true -> rs'#r' = rs#r'.
+Proof.
+  intros. unfold rs'. intuition; try reflexivity.
+  unfold compare_float. Simpl. 
+Qed.
+
+Definition lock {A: Type} (x: A) := x.
+
+Ltac ArgsInv :=
+  repeat (match goal with
+  | [ H: Error _ = OK _ |- _ ] => discriminate
+  | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args
+  | [ H: bind _ _ = OK _ |- _ ] => monadInv H
+  | [ H: assertion _ = OK _ |- _ ] => monadInv H
+  end);
+  subst;
+  repeat (match goal with
+  | [ H: ireg_of ?x = OK ?y |- _ ] =>
+         simpl in *; rewrite (ireg_of_eq _ _ H) in *
+(*; change H with (lock (ireg_of x) = OK y)*)
+  | [ H: freg_of ?x = OK ?y |- _ ] =>
+         simpl in *; rewrite (freg_of_eq _ _ H) in *
+(*; change H with (lock (freg_of x) = OK y)*)
+  end).
 
 Lemma transl_cond_correct:
-  forall cond args k rs m,
-  map mreg_type args = type_of_condition cond ->
+  forall cond args k rs m c,
+  transl_cond cond args k = OK c ->
   exists rs',
-     exec_straight (transl_cond cond args k) rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ match eval_condition cond (map rs (map preg_of args)) m with
      | Some b => rs'#(CR (crbit_for_cond cond)) = Val.of_bool b
      | None => True
      end
-  /\ forall r, important_preg r = true -> rs'#r = rs r.
+  /\ forall r, data_preg r = true -> rs'#r = rs r.
 Proof.
-  intros until m; intros TY.
+  intros until c; intros TR. 
   assert (MATCH: forall v ob,
            v = Val.of_optbool ob ->
            match ob with Some b => v = Val.of_bool b | None => True end).
@@ -1006,268 +586,251 @@ Proof.
      intros. destruct v1; simpl; auto; destruct v2; simpl; auto.
      unfold Val.cmpu, Val.cmpu_bool in H. subst v. destruct H0; subst cmp; auto.
 
-   destruct cond; simpl in TY; TypeInv; simpl.
-  (* Ccomp *)
-  generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1)) m).
-  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  unfold transl_cond in TR; destruct cond; ArgsInv.
+- (* Ccomp *)
+  generalize (compare_int_spec rs (rs x) (rs x0) m).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto).
+  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
   auto.
-  (* Ccompu *)
-  generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1)) m).
-  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+- (* Ccompu *)
+  generalize (compare_int_spec rs (rs x) (rs x0) m).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct c; apply MATCH; assumption.
+  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
   auto.
-  (* Ccompshift *)
-  generalize (compare_int_spec rs (rs (ireg_of m0)) (eval_shift s (rs (ireg_of m1))) m).
-  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+- (* Ccompshift *)
+  generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. rewrite transl_shift_correct. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto).
-  rewrite transl_shift_correct. auto.
-  (* Ccompushift *)
-  generalize (compare_int_spec rs (rs (ireg_of m0)) (eval_shift s (rs (ireg_of m1))) m).
-  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  rewrite transl_shift_correct. 
+  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
+  auto.
+- (* Ccompushift *)
+  generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. rewrite transl_shift_correct. destruct c; apply MATCH; assumption.
-  rewrite transl_shift_correct. auto.
-  (* Ccompimm *)
+  rewrite transl_shift_correct. 
+  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
+  auto.
+- (* Ccompimm *)
   destruct (is_immed_arith i).
-  generalize (compare_int_spec rs (rs (ireg_of m0)) (Vint i) m).
-  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  generalize (compare_int_spec rs (rs x) (Vint i) m).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto. 
-  split. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto).
+  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
   auto.
   exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
-  generalize (compare_int_spec rs' (rs (ireg_of m0)) (Vint i) m).
-  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  generalize (compare_int_spec rs' (rs x) (Vint i) m).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
-  rewrite Q. rewrite R; eauto with ppcgen. auto.
-  split. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto).
-  intros. rewrite K; auto with ppcgen.
-  (* Ccompuimm *)
+  rewrite Q. rewrite R; eauto with asmgen. auto.
+  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
+  intros. rewrite C; auto with asmgen.
+- (* Ccompuimm *)
   destruct (is_immed_arith i).
-  generalize (compare_int_spec rs (rs (ireg_of m0)) (Vint i) m).
-  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  generalize (compare_int_spec rs (rs x) (Vint i) m).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto. 
-  split. destruct c; apply MATCH; assumption.
+  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
   auto.
   exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
-  generalize (compare_int_spec rs' (rs (ireg_of m0)) (Vint i) m).
-  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  generalize (compare_int_spec rs' (rs x) (Vint i) m).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
-  rewrite Q. rewrite R; eauto with ppcgen. auto.
-  split. destruct c; apply MATCH; assumption.
-  intros. rewrite K; auto with ppcgen.
-  (* Ccompf *)
-  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]]]]]]]]]].
+  rewrite Q. rewrite R; eauto with asmgen. auto.
+  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
+  intros. rewrite C; auto with asmgen.
+- (* Ccompf *)
+  generalize (compare_float_spec rs (rs x) (rs x0)).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. case c; apply MATCH; assumption.
+  split. case c0; apply MATCH; assumption.
   auto.
-  (* Cnotcompf *)
-  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]]]]]]]]]].
+- (* Cnotcompf *)
+  generalize (compare_float_spec rs (rs x) (rs x0)).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. rewrite <- Val.negate_cmpf_ne in B. rewrite <- Val.negate_cmpf_eq in A.  
-  destruct c; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
+  split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1.  
+  destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
   auto.
-  (* Ccompfzero *)
-  generalize (compare_float_spec rs (rs (freg_of m0)) (Vfloat Float.zero)).
-  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+- (* Ccompfzero *)
+  generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. case c; apply MATCH; assumption.
+  split. case c0; apply MATCH; assumption.
   auto.
-  (* Cnotcompf *)
-  generalize (compare_float_spec rs (rs (freg_of m0)) (Vfloat Float.zero)).
-  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+- (* Cnotcompf *)
+  generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)).
+  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. rewrite <- Val.negate_cmpf_ne in B. rewrite <- Val.negate_cmpf_eq in A.  
-  destruct c; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
+  split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1.  
+  destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
   auto.
 Qed.
 
 (** Translation of arithmetic operations. *)
 
-Ltac Simpl :=
-  match goal with
-  | [ |- context[nextinstr _ _] ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
-  | [ |- context[Pregmap.get ?x (Pregmap.set ?x _ _)] ] => rewrite Pregmap.gss; auto
-  | [ |- context[Pregmap.set ?x _ _ ?x] ] => rewrite Pregmap.gss; auto
-  | [ |- context[Pregmap.get _ (Pregmap.set _ _ _)] ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
-  | [ |- context[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_same:
-  forall op args res k (rs: regset) m v,
-  wt_instr (Mop op args res) ->
+  forall op args res k c (rs: regset) m v,
+  transl_op op args res k = OK c ->
   eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v ->
   match op with Ocmp _ => False | _ => True end ->
   exists rs',
-     exec_straight (transl_op op args res k) rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of res) = v
-  /\ forall r, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r.
+  /\ forall r, data_preg r = true -> r <> preg_of res -> rs'#r = rs#r.
 Proof.
-  intros. inv H. 
+  intros until v; intros TR EV NOCMP. 
+  unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; inv EV; try (TranslOpSimpl; fail).
   (* Omove *)
-  simpl in *. inv H0.
-  exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))).
-  split. unfold preg_of; rewrite <- H3.
-  destruct (mreg_type r1); apply exec_straight_one; auto.
-  split. Simpl. Simpl.
-  intros. Simpl. Simpl.
-  (* Other instructions *)
-  destruct op; simpl in H6; inv H6; TypeInv; simpl in H0; inv H0; try (TranslOpSimpl; fail).
+  exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of m0)))).
+  split.
+  destruct (preg_of res) eqn:RES; try discriminate;
+  destruct (preg_of m0) eqn:ARG; inv TR.
+  apply exec_straight_one; auto.
+  apply exec_straight_one; auto.
+  intuition Simpl.
   (* Ointconst *)
-  generalize (loadimm_correct (ireg_of res) i k rs m). intros [rs' [A [B C]]]. 
-  exists rs'. split. auto. split. rewrite B; auto. intros. auto with ppcgen.
+  generalize (loadimm_correct x i k rs m). intros [rs' [A [B C]]]. 
+  exists rs'; auto with asmgen. 
   (* Oaddrstack *)
-  generalize (addimm_correct (ireg_of res) IR13 i k rs m). 
+  generalize (addimm_correct x IR13 i k rs m). 
   intros [rs' [EX [RES OTH]]].
-  exists rs'. split. auto. split. auto. auto with ppcgen.
+  exists rs'; auto with asmgen. 
   (* Oaddimm *)
-  generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m).
+  generalize (addimm_correct x x0 i k rs m).
   intros [rs' [A [B C]]]. 
-  exists rs'. split. auto. split. auto. auto with ppcgen.
+  exists rs'; auto with asmgen.
   (* Orsbimm *)
-  generalize (rsubimm_correct (ireg_of res) (ireg_of m0) i k rs m).
+  generalize (rsubimm_correct x x0 i k rs m).
   intros [rs' [A [B C]]].
-  exists rs'.
-  split. eauto. split. rewrite B. auto. 
-  auto with ppcgen. 
+  exists rs'; auto with asmgen.
   (* Omul *)
-  destruct (ireg_eq (ireg_of res) (ireg_of m0) || ireg_eq (ireg_of res) (ireg_of m1)).
+  destruct (ireg_eq x x0 || ireg_eq x x1).
   econstructor; split.
   eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
-  split. repeat Simpl.
-  intros. repeat Simpl.
+  intuition Simpl.
   TranslOpSimpl.
   (* divs *)
-  econstructor. split. apply exec_straight_one. simpl. rewrite H2. reflexivity. auto. 
-  split. repeat Simpl. intros. repeat Simpl.
+  econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. 
+  intuition Simpl.
   (* divu *)
-  econstructor. split. apply exec_straight_one. simpl. rewrite H2. reflexivity. auto. 
-  split. repeat Simpl. intros. repeat Simpl.
+  econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto.
+  intuition Simpl.
   (* Oandimm *)
-  generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m
-                            (ireg_of_not_IR14 m0)).
+  generalize (andimm_correct x x0 i k rs m). 
   intros [rs' [A [B C]]]. 
-  exists rs'; auto with ppcgen.
+  exists rs'; auto with asmgen.
   (* Oorimm *)
-  generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m).
+  generalize (orimm_correct x x0 i k rs m).
   intros [rs' [A [B C]]]. 
-  exists rs'; auto with ppcgen.
+  exists rs'; auto with asmgen.
   (* Oxorimm *)
-  generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m).
+  generalize (xorimm_correct x x0 i k rs m).
   intros [rs' [A [B C]]]. 
-  exists rs'; auto with ppcgen.
+  exists rs'; auto with asmgen.
   (* Oshrximm *)
   exploit Val.shrx_shr; eauto. intros [n [i' [ARG1 [ARG2 RES]]]].
   injection ARG2; intro ARG2'; subst i'; clear ARG2.
   set (islt := Int.lt n Int.zero) in *.
   set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero) m)).
-  assert (OTH1: forall r', important_preg r' = true -> rs1#r' = rs#r').
+  assert (OTH1: forall r', data_preg r' = true -> rs1#r' = rs#r').
     generalize (compare_int_spec rs (Vint n) (Vint Int.zero) m).
     fold rs1. intros [A B]. intuition.
-  exploit (addimm_correct IR14 (ireg_of m0) (Int.sub (Int.shl Int.one i) Int.one)).
+  exploit (addimm_correct IR14 x0 (Int.sub (Int.shl Int.one i) Int.one)).
   intros [rs2 [EXEC2 [RES2 OTH2]]].
   set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))).
-  set (rs4 := nextinstr (rs3#(ireg_of res) <- (Val.shr rs3#IR14 (Vint i)))).
+  set (rs4 := nextinstr (rs3#x <- (Val.shr rs3#IR14 (Vint i)))).
   exists rs4; split.
   apply exec_straight_step with rs1 m.
   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)).
+  simpl. rewrite OTH2; eauto with asmgen.
+    change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)).
     unfold Val.cmp, Val.cmp_bool. change (Int.cmp Cge n Int.zero) with (negb islt).
-    rewrite OTH2. rewrite OTH1. rewrite ARG1. 
+    rewrite OTH2; eauto with asmgen. rewrite OTH1. rewrite ARG1. 
     unfold rs3. case islt; reflexivity.
-    destruct m0; reflexivity. auto with ppcgen. auto with ppcgen. discriminate. discriminate.
-  simpl. auto. 
-  auto. unfold rs3. case islt; auto. auto.
-  split. unfold rs4. repeat Simpl. unfold rs3. Simpl. destruct islt.
-  rewrite RES2. change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))). auto.
-  Simpl. rewrite <- ARG1; auto.
-  intros. unfold rs4; repeat Simpl. unfold rs3; repeat Simpl. 
-  transitivity (rs2 r). destruct islt; auto. Simpl. 
-  rewrite OTH2; auto with ppcgen.
+    rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen.
+    auto.
+    unfold rs3. destruct islt; auto. auto. 
+    split. unfold rs4; Simpl. unfold rs3. destruct islt. 
+    Simpl. rewrite RES2. unfold rs1. Simpl.
+    Simpl. congruence.
+    intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. 
   (* intoffloat *)
-  econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto.
-  split; intros; repeat Simpl.
+  econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
+  intuition Simpl.
   (* intuoffloat *)
-  econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto.
-  split; intros; repeat Simpl.
+  econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
+  intuition Simpl.
   (* floatofint *)
-  econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto.
-  split; intros; repeat Simpl.
+  econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
+  intuition Simpl.
   (* floatofintu *)
-  econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto.
-  split; intros; repeat Simpl.
+  econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
+  intuition Simpl.
   (* Ocmp *)
   contradiction.
 Qed.
 
 Lemma transl_op_correct:
-  forall op args res k (rs: regset) m v,
-  wt_instr (Mop op args res) ->
+  forall op args res k c (rs: regset) m v,
+  transl_op op args res k = OK c ->
   eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v ->
   exists rs',
-     exec_straight (transl_op op args res k) rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ Val.lessdef v rs'#(preg_of res)
-  /\ forall r, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r.
+  /\ forall r, data_preg r = true -> r <> preg_of res -> rs'#r = rs#r.
 Proof.
   intros. 
   assert (EITHER: match op with Ocmp _ => False | _ => True end \/ exists cmp, op = Ocmp cmp).
-    destruct op; auto. right; exists c; auto.
-  destruct EITHER as [A | [c A]]. 
+    destruct op; auto. right; exists c0; auto.
+  destruct EITHER as [A | [cmp A]]. 
   exploit transl_op_correct_same; eauto. intros [rs' [P [Q R]]].
   subst v. exists rs'; eauto. 
   (* Ocmp *)
-  subst op. inv H. simpl in H5. inv H5. simpl in H0. inv H0.
-  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 H1)
-  as [rs1 [A [B C]]].
-  set (rs2 := nextinstr (rs1#(ireg_of res) <- (Vint Int.zero))).
-  set (v := match rs2#(crbit_for_cond c) with
-             | Vint n => if Int.eq n Int.zero then Vint Int.zero else Vint Int.one
-             | _ => Vundef
-           end).
-  set (rs3 := nextinstr (rs2#(ireg_of res) <- v)).
+  subst op. simpl in H. monadInv H. simpl in H0. inv H0. 
+  rewrite (ireg_of_eq _ _ EQ).
+  exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]].
+  set (rs2 := nextinstr (rs1#x <- (Vint Int.zero))).
+  set (rs3 := nextinstr (match rs2#(crbit_for_cond cmp) with
+             | Vint n => if Int.eq n Int.zero then rs2 else rs2#x <- Vone
+             | _      => rs2#x <- Vundef
+             end)).
   exists rs3; split.
-  eapply exec_straight_trans. eauto. 
-  apply exec_straight_two with rs2 m; auto.
-  simpl. unfold rs3, v. 
-  destruct (rs2 (crbit_for_cond c)) eqn:?; auto.
-  destruct (Int.eq i Int.zero); auto. 
-  decEq. decEq. apply extensionality; intros. unfold Pregmap.set.
-  destruct (PregEq.eq x (ireg_of res)); auto. subst. 
-  unfold rs2. Simpl. Simpl.
-  replace (preg_of res) with (IR (ireg_of res)).
-  split. unfold rs3. Simpl. Simpl. 
-  destruct (eval_condition c rs ## (preg_of ## args) m); simpl; auto.
-  unfold v. unfold rs2. Simpl. Simpl. rewrite B. 
-  destruct b; simpl; auto.
-  intros. unfold rs3. repeat Simpl. unfold rs2. repeat Simpl.
-  unfold preg_of; rewrite H2; auto.
+  eapply exec_straight_trans. eexact A. apply exec_straight_two with rs2 m.
+  auto.
+  simpl. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto.
+  auto. unfold rs3.  destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto.
+  split. unfold rs3. Simpl. 
+  replace (rs2 (crbit_for_cond cmp)) with (rs1 (crbit_for_cond cmp)).
+  destruct (eval_condition cmp rs##(preg_of##args) m) as [[]|]; simpl in *.
+  rewrite B. simpl. Simpl. 
+  rewrite B. simpl. unfold rs2. Simpl.
+  auto.
+  destruct cmp; reflexivity. 
+  intros. transitivity (rs2 r). 
+  unfold rs3. destruct (rs2 (crbit_for_cond cmp)); Simpl. destruct (Int.eq i Int.zero); auto; Simpl.
+  unfold rs2. Simpl.
 Qed.
 
 Remark val_add_add_zero:
@@ -1276,43 +839,40 @@ 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)
+Lemma transl_memory_access_correct:
+  forall (P: regset -> Prop) (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',
+         addr args k c (rs: regset) a m m',
+  transl_memory_access mk_instr_imm mk_instr_gen is_immed addr args k = OK c ->
+  eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
   (forall (r1: ireg) (rs1: regset) n k,
-    eval_addressing ge sp addr (map rs (map preg_of args)) = Some(Val.add rs1#r1 (Vint n)) ->
+    Val.add rs1#r1 (Vint n) = a ->
     (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') ->
+    exec_straight ge fn (mk_instr_imm r1 n :: k) rs1 m k rs' m' /\ P rs') ->
   match mk_instr_gen with
   | None => True
   | Some mk =>
       (forall (r1: ireg) (sa: shift_addr) (rs1: regset) k,
-      eval_addressing ge sp addr (map rs (map preg_of args)) = Some(Val.add rs1#r1 (eval_shift_addr sa rs1)) ->
+      Val.add rs1#r1 (eval_shift_addr sa rs1) = a ->
       (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')
+      exec_straight ge fn (mk r1 sa :: k) rs1 m k rs' m' /\ P rs')
   end ->
-  agree ms sp rs ->
-  map mreg_type args = type_of_addressing addr ->
   exists rs',
-    exec_straight (transl_load_store mk_instr_imm mk_instr_gen is_immed addr args k) rs m
-                        k rs' m'
-  /\ agree ms' sp rs'.
+    exec_straight ge fn c rs m k rs' m' /\ P rs'.
 Proof.
-  intros. destruct addr; simpl in H2; TypeInv; simpl.
+  intros until m'; intros TR EA MK1 MK2.
+  unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in EA; inv EA.
   (* Aindexed *)
   case (is_immed i).
   (* Aindexed, small displacement *)
-  apply H; auto.
+  apply MK1; auto.
   (* Aindexed, large displacement *)
-  destruct (addimm_correct IR14 (ireg_of m0) i (mk_instr_imm IR14 Int.zero :: k) rs m)
+  destruct (addimm_correct IR14 x i (mk_instr_imm IR14 Int.zero :: k) rs m)
   as [rs' [A [B C]]].
-  exploit (H IR14 rs' Int.zero); eauto. 
+  exploit (MK1 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.
@@ -1320,13 +880,12 @@ Proof.
   (* Aindexed2 *)
   destruct mk_instr_gen as [mk | ]. 
   (* binary form available *)
-  apply H0; auto.
+  apply MK2; auto.
   (* binary form not available *)
-  set (rs' := nextinstr (rs#IR14 <- (Val.add (rs (ireg_of m0)) (rs (ireg_of m1))))).
-  exploit (H IR14 rs' Int.zero); eauto.
-  unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  decEq. apply val_add_add_zero. 
-  unfold rs'. intros. repeat Simpl. 
+  set (rs' := nextinstr (rs#IR14 <- (Val.add (rs x) (rs x0)))).
+  exploit (MK1 IR14 rs' Int.zero); eauto.
+  unfold rs'. Simpl. symmetry. apply val_add_add_zero. 
+  intros. unfold rs'. Simpl. 
   intros [rs'' [A B]].
   exists rs''; split.
   eapply exec_straight_step with (rs2 := rs'); eauto.
@@ -1334,189 +893,172 @@ Proof.
   (* Aindexed2shift *)
   destruct mk_instr_gen as [mk | ]. 
   (* binary form available *)
-  apply H0; auto. rewrite transl_shift_addr_correct. auto.
+  apply MK2; auto. rewrite transl_shift_addr_correct. auto.
   (* binary form not available *)
-  set (rs' := nextinstr (rs#IR14 <- (Val.add (rs (ireg_of m0)) (eval_shift s (rs (ireg_of m1)))))).
-  exploit (H IR14 rs' Int.zero); eauto.
-  unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  decEq. apply val_add_add_zero.
-  unfold rs'; intros; repeat Simpl.
+  set (rs' := nextinstr (rs#IR14 <- (Val.add (rs x) (eval_shift s (rs x0))))).
+  exploit (MK1 IR14 rs' Int.zero); eauto.
+  unfold rs'. Simpl. symmetry. apply val_add_add_zero. 
+  intros; unfold rs'; Simpl.
   intros [rs'' [A B]].
   exists rs''; split.
   eapply exec_straight_step with (rs2 := rs'); eauto.
   simpl. rewrite transl_shift_correct. auto. 
   auto.
   (* Ainstack *)
-  destruct (is_immed i).
+  destruct (is_immed i); inv TR.
   (* Ainstack, short displacement *)
-  apply H; auto. rewrite (sp_val _ _ _ H1). auto.
+  apply MK1; auto.
   (* Ainstack, large displacement *)
   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.
-  rewrite (sp_val _ _ _ H1). rewrite B. rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. auto.
+  exploit (MK1 IR14 rs' Int.zero); eauto.
+  rewrite B. rewrite Val.add_assoc. f_equal. simpl. rewrite Int.add_zero; auto. 
   intros [rs'' [D E]].
   exists rs''; split.
   eapply exec_straight_trans. eexact A. eexact D. auto.
 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 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') ->
-  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 ->
+  forall mk_instr is_immed dst addr args k c (rs: regset) a chunk m v,
+  transl_memory_access_int mk_instr is_immed dst addr args k = OK c ->
+  eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
-  Mem.extends m m' ->
+  (forall (r1 r2: ireg) (sa: shift_addr) (rs1: regset),
+    exec_instr ge fn (mk_instr r1 r2 sa) rs1 m =
+    exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 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 (undef_temps ms)) sp rs'.
+      exec_straight ge fn c rs m k rs' m
+   /\ rs'#(preg_of dst) = v
+   /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros. unfold transl_load_store_int.
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
-  unfold PregEq.t.
-  intros [a' [A B]].
-  exploit Mem.loadv_extends; eauto. intros [v' [C D]]. 
-  apply transl_load_store_correct with ms; auto.
-  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.
+  intros. monadInv H. erewrite ireg_of_eq by eauto.  
+  eapply transl_memory_access_correct; eauto.
+  intros; simpl. econstructor; split. apply exec_straight_one. 
+  rewrite H2. unfold exec_load. simpl eval_shift_addr. rewrite H. rewrite H1. eauto. auto.
+  split. Simpl. intros; Simpl. 
+  simpl; intros. 
+  econstructor; split. apply exec_straight_one. 
+  rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto.
+  split. Simpl. intros; Simpl.
 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 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') ->
-  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 ->
+  forall mk_instr is_immed dst addr args k c (rs: regset) a chunk m v,
+  transl_memory_access_float mk_instr is_immed dst addr args k = OK c ->
+  eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
-  Mem.extends m m' ->
+  (forall (r1: freg) (r2: ireg) (n: int) (rs1: regset),
+    exec_instr ge fn (mk_instr r1 r2 n) rs1 m =
+    exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 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 (undef_temps ms)) sp rs'.
+      exec_straight ge fn c rs m k rs' m
+   /\ rs'#(preg_of dst) = v
+   /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros. unfold transl_load_store_int.
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
-  unfold PregEq.t.
-  intros [a' [A B]].
-  exploit Mem.loadv_extends; eauto. intros [v' [C D]]. 
-  apply transl_load_store_correct with ms; auto.
-  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.
+  intros. monadInv H. erewrite freg_of_eq by eauto.  
+  eapply transl_memory_access_correct; eauto.
+  intros; simpl. econstructor; split. apply exec_straight_one. 
+  rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto.
+  split. Simpl. intros; Simpl.
+  simpl; auto.
 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 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 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 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_lessdef. eapply preg_vals; eauto. eauto.
-  unfold PregEq.t. 
-  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]].
-  exists m2'; split; auto.
-  apply transl_load_store_correct with ms; auto.
-  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.
+  forall mk_instr is_immed src addr args k c (rs: regset) a chunk m m',
+  transl_memory_access_int mk_instr is_immed src addr args k = OK c ->
+  eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
+  Mem.storev chunk m a rs#(preg_of src) = Some m' ->
+  (forall (r1 r2: ireg) (sa: shift_addr) (rs1: regset),
+    exec_instr ge fn (mk_instr r1 r2 sa) rs1 m =
+    exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) ->
+  exists rs',
+      exec_straight ge fn c rs m k rs' m'
+   /\ forall r, nontemp_preg r = true -> rs'#r = rs#r.
+Proof.
+  intros. monadInv H. erewrite ireg_of_eq in * by eauto.  
+  eapply transl_memory_access_correct; eauto.
+  intros; simpl. econstructor; split. apply exec_straight_one. 
+  rewrite H2. unfold exec_store. simpl eval_shift_addr. rewrite H. rewrite H3; eauto with asmgen. 
+  rewrite H1. eauto. auto.
+  intros; Simpl.
+  simpl; intros. 
+  econstructor; split. apply exec_straight_one. 
+  rewrite H2. unfold exec_store. rewrite H. rewrite H3; eauto with asmgen. 
+  rewrite H1. eauto. auto.
+  intros; Simpl.
 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 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 <> FR7 -> 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 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_lessdef. eapply preg_vals; eauto. eauto.
-  unfold PregEq.t. 
-  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]].
-  exists m2'; split; auto.
-  apply transl_load_store_correct with ms; auto.
-  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.
+  forall mk_instr is_immed src addr args k c (rs: regset) a chunk m m',
+  transl_memory_access_float mk_instr is_immed src addr args k = OK c ->
+  eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
+  Mem.storev chunk m a rs#(preg_of src) = Some m' ->
+  (forall (r1: freg) (r2: ireg) (n: int) (rs1: regset),
+    exec_instr ge fn (mk_instr r1 r2 n) rs1 m =
+    exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) ->
+  exists rs',
+      exec_straight ge fn c rs m k rs' m'
+   /\ forall r, nontemp_preg r = true -> rs'#r = rs#r.
+Proof.
+  intros. monadInv H. erewrite freg_of_eq in * by eauto.  
+  eapply transl_memory_access_correct; eauto.
+  intros; simpl. econstructor; split. apply exec_straight_one. 
+  rewrite H2. unfold exec_store. rewrite H. rewrite H3; eauto with asmgen. 
+  rewrite H1. eauto. auto.
+  intros; Simpl.
+  simpl; auto.
+Qed.
+
+Lemma transl_load_correct:
+  forall chunk addr args dst k c (rs: regset) a m v,
+  transl_load chunk addr args dst k = OK c ->
+  eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
+  Mem.loadv chunk m a = Some v ->
+  exists rs',
+      exec_straight ge fn c rs m k rs' m
+   /\ rs'#(preg_of dst) = v
+   /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
+Proof.
+  intros. destruct chunk; simpl in H.
+  eapply transl_load_int_correct; eauto.
+  eapply transl_load_int_correct; eauto.
+  eapply transl_load_int_correct; eauto.
+  eapply transl_load_int_correct; eauto.
+  eapply transl_load_int_correct; eauto.
+  eapply transl_load_float_correct; eauto.
+  apply Mem.loadv_float64al32 in H1. eapply transl_load_float_correct; eauto.
+  eapply transl_load_float_correct; eauto.
+Qed.
+
+Lemma transl_store_correct:
+  forall chunk addr args src k c (rs: regset) a m m',
+  transl_store chunk addr args src k = OK c ->
+  eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
+  Mem.storev chunk m a rs#(preg_of src) = Some m' ->
+  exists rs',
+      exec_straight ge fn c rs m k rs' m'
+   /\ forall r, nontemp_preg r = true -> rs'#r = rs#r.
+Proof.
+  intros. destruct chunk; simpl in H.
+- assert (Mem.storev Mint8unsigned m a (rs (preg_of src)) = Some m').
+    rewrite <- H1. destruct a; simpl; auto. symmetry. apply Mem.store_signed_unsigned_8.
+  clear H1. eapply transl_store_int_correct; eauto.
+- eapply transl_store_int_correct; eauto.
+- assert (Mem.storev Mint16unsigned m a (rs (preg_of src)) = Some m').
+    rewrite <- H1. destruct a; simpl; auto. symmetry. apply Mem.store_signed_unsigned_16.
+  clear H1. eapply transl_store_int_correct; eauto.
+- eapply transl_store_int_correct; eauto.
+- eapply transl_store_int_correct; eauto.
+- unfold transl_memory_access_float in H. monadInv H. rewrite (freg_of_eq _ _ EQ) in *. 
+  eapply transl_memory_access_correct; eauto. 
+  intros. econstructor; split. apply exec_straight_one.
+  simpl. unfold exec_store. rewrite H. rewrite H2; eauto with asmgen. 
+  rewrite H1. eauto. auto. intros. Simpl. 
+  simpl; auto.
+- apply Mem.storev_float64al32 in H1. eapply transl_store_float_correct; eauto.
+- eapply transl_store_float_correct; eauto.
+Qed.
+
+End CONSTRUCTORS.
 
-End STRAIGHTLINE.