MPPA - Added ops for comparison operators

mppa_k1c/Asm.v

@@ -187,8 +187,10 @@ Inductive instruction : Type :=
   | Pmv     (rd: ireg) (rs: ireg)                   (**r integer move *)
 
 (** Comparisons *)
-  | Pcompw  (it: itest) (rd rs1 rs2: ireg)      (**r integer comparison *)
-  | Pcompd  (it: itest) (rd rs1 rs2: ireg)      (**r integer comparison *)
+  | Pcompw  (it: itest) (rd rs1 rs2: ireg)          (**r integer comparison *)
+  | Pcompiw (it: itest) (rd rs1: ireg) (imm: int)   (**r integer comparison imm *)
+  | Pcompd  (it: itest) (rd rs1 rs2: ireg)          (**r integer comparison double *)
+  | Pcompid (it: itest) (rd rs1: ireg) (imm: int64) (**r integer comparison double imm *)
 
 (** 32-bit integer register-immediate instructions *)
   | Paddiw  (rd: ireg) (rs: ireg) (imm: int)        (**r add immediate *)
@@ -756,8 +758,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 (** Comparisons *)
   | Pcompw c d s1 s2 => 
       Next (nextinstr (rs#d <- (compare_int c rs##s1 rs##s2 m))) m
+  | Pcompiw c d s i => 
+      Next (nextinstr (rs#d <- (compare_int c rs##s (Vint i) m))) m
   | Pcompd c d s1 s2 => 
       Next (nextinstr (rs#d <- (compare_long c rs###s1 rs###s2 m))) m
+  | Pcompid c d s i => 
+      Next (nextinstr (rs#d <- (compare_long c rs###s (Vlong i) m))) m
 
 (** 32-bit integer register-immediate instructions *)
   | Paddiw d s i =>

mppa_k1c/Asmgen.v

@@ -235,6 +235,81 @@ Definition transl_cbranch
       Error(msg "Asmgen.transl_cbranch")
   end.
 
+(** Translation of a condition operator.  The generated code sets the
+  [rd] target register to 0 or 1 depending on the truth value of the
+  condition. *)
+
+Definition transl_cond_int32s (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
+  Pcompw (itest_for_cmp cmp Signed) rd r1 r2 :: k.
+
+Definition transl_cond_int32u (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
+  Pcompw (itest_for_cmp cmp Unsigned) rd r1 r2 :: k.
+
+Definition transl_cond_int64s (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
+  Pcompd (itest_for_cmp cmp Signed) rd r1 r2 :: k.
+
+Definition transl_cond_int64u (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
+  Pcompd (itest_for_cmp cmp Unsigned) rd r1 r2 :: k.
+
+Definition transl_condimm_int32s (cmp: comparison) (rd r1: ireg) (n: int) (k: code) :=
+  Pcompiw (itest_for_cmp cmp Signed) rd r1 n :: k.
+
+Definition transl_condimm_int32u (cmp: comparison) (rd r1: ireg) (n: int) (k: code) :=
+  Pcompiw (itest_for_cmp cmp Unsigned) rd r1 n :: k.
+
+Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k: code) :=
+  Pcompid (itest_for_cmp cmp Signed) rd r1 n :: k.
+
+Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: code) :=
+  Pcompid (itest_for_cmp cmp Unsigned) rd r1 n :: k.
+
+Definition transl_cond_op
+           (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
+  match cond, args with
+  | Ccomp c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_int32s c rd r1 r2 k)
+  | Ccompu c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_int32u c rd r1 r2 k)
+  | Ccompimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (transl_condimm_int32s c rd r1 n k)
+  | Ccompuimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (transl_condimm_int32u c rd r1 n k)
+  | Ccompl c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_int64s c rd r1 r2 k)
+  | Ccomplu c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_int64u c rd r1 r2 k)
+  | Ccomplimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (transl_condimm_int64s c rd r1 n k)
+  | Ccompluimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (transl_condimm_int64u c rd r1 n k)
+(*| Ccompf c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_float c rd r1 r2 in
+      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
+  | Cnotcompf c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_float c rd r1 r2 in
+      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
+  | Ccompfs c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_single c rd r1 r2 in
+      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
+  | Cnotcompfs c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_single c rd r1 r2 in
+      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
+*)| _, _ =>
+      Error(msg "Asmgen.transl_cond_op")
+end.
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
@@ -537,10 +612,10 @@ Definition transl_op
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfcvtslu rd rs :: k)
 
-  | Ocmp cmp, _ =>
+*)| Ocmp cmp, _ =>
       do rd <- ireg_of res;
       transl_cond_op cmp rd args k
-*)
+  
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.

mppa_k1c/Asmgenproof.v

@@ -251,64 +251,22 @@ Qed.
   apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
   destruct normal; TailNoLabel.
 *)
-(*
+
 Remark transl_cond_op_label:
   forall cond args r k c,
   transl_cond_op cond r args k = OK c -> tail_nolabel k c.
 Proof.
   intros. unfold transl_cond_op in H; destruct cond; TailNoLabel.
-(*
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel. 
-- unfold transl_condimm_int32s.
-  destruct (Int.eq n Int.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl.
-* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel].
-* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel].
-* apply opimm32_label; intros; exact I.
-* destruct (Int.eq n (Int.repr Int.max_signed)). apply loadimm32_label. apply opimm32_label; intros; exact I.
-* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel.
-* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel.
-- unfold transl_condimm_int32u.
-  destruct (Int.eq n Int.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl; 
-  try (eapply tail_nolabel_trans; [apply loadimm32_label | TailNoLabel]).
-  apply opimm32_label; intros; exact I.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel. 
-- unfold transl_condimm_int64s.
-  destruct (Int64.eq n Int64.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl.
-* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel].
-* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel].
-* apply opimm64_label; intros; exact I.
-* destruct (Int64.eq n (Int64.repr Int64.max_signed)). apply loadimm32_label. apply opimm64_label; intros; exact I.
-* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel.
-* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel.
-- unfold transl_condimm_int64u.
-  destruct (Int64.eq n Int64.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl; 
-  try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]).
-  apply opimm64_label; intros; exact I.
-- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-*)
+- unfold transl_cond_int32s; destruct c0; simpl; TailNoLabel.
+- unfold transl_cond_int32u; destruct c0; simpl; TailNoLabel. 
+- unfold transl_condimm_int32s; destruct c0; simpl; TailNoLabel.
+- unfold transl_condimm_int32u; destruct c0; simpl; TailNoLabel.
+- unfold transl_cond_int64s; destruct c0; simpl; TailNoLabel.
+- unfold transl_cond_int64u; destruct c0; simpl; TailNoLabel. 
+- unfold transl_condimm_int64s; destruct c0; simpl; TailNoLabel.
+- unfold transl_condimm_int64u; destruct c0; simpl; TailNoLabel.
 Qed.
-*)
+
 Remark transl_op_label:
   forall op args r k c,
   transl_op op args r k = OK c -> tail_nolabel k c.
@@ -337,6 +295,8 @@ Opaque Int.eq.
 - apply opimm64_label; intros; exact I.
 (* Oxorimm64  *)
 - apply opimm64_label; intros; exact I.
+(* Ocmp *)
+- eapply transl_cond_op_label; eauto.
 Qed.
 
 (*

mppa_k1c/Asmgenproof1.v

@@ -737,7 +737,7 @@ Proof.
   split. eapply exec_straight_opt_right; eauto. apply exec_straight_one; auto.
   intros; Simpl. 
 Qed.
-(*
+
 (** Translation of condition operators *)
 
 Lemma transl_cond_int32s_correct:
@@ -747,24 +747,19 @@ Lemma transl_cond_int32s_correct:
   /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
 Proof.
-  intros. destruct cmp; simpl. 
+  intros. destruct cmp; simpl.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs##r1); auto.
+  split; intros; Simpl.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs##r1); auto.
+  split; intros; Simpl.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
   split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool.
-  simpl. rewrite (Val.negate_cmp_bool Clt). 
-  destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt). 
-  destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto.
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
 Qed.
 
 Lemma transl_cond_int32u_correct:
@@ -781,17 +776,12 @@ Proof.
   split; intros; Simpl.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
   split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool.
-  simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle). 
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt). 
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto.
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
 Qed.
 
 Lemma transl_cond_int64s_correct:
@@ -803,22 +793,17 @@ Lemma transl_cond_int64s_correct:
 Proof.
   intros. destruct cmp; simpl. 
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
+  split; intros; Simpl.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
+  split; intros; Simpl.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
   split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool.
-  simpl. rewrite (Val.negate_cmpl_bool Clt). 
-  destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt). 
-  destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto.
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
 Qed.
 
 Lemma transl_cond_int64u_correct:
@@ -835,17 +820,12 @@ Proof.
   split; intros; Simpl.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
   split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool.
-  simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle). 
-  destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt). 
-  destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto.
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
 Qed.
 
 Lemma transl_condimm_int32s_correct:
@@ -856,60 +836,19 @@ Lemma transl_condimm_int32s_correct:
   /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
   /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
-  intros. unfold transl_condimm_int32s.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C).
-  exists rs'; eauto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm32 GPR31 n (transl_cond_int32s cmp rd r1 GPR31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r).
-  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ unfold xorimm32. 
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ unfold xorimm32. 
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed).
-* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. 
-  unfold Int.lt. rewrite zlt_false. auto. 
-  change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed.
-  generalize (Int.signed_range i); omega.
-* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto.
-  unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
-  destruct (zlt (Int.signed n) (Int.signed i)).
-  rewrite zlt_false by omega. auto.
-  rewrite zlt_true by omega. auto.
-  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
-  assert (Int.signed n <> Int.max_signed).
-  { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. }
-  generalize (Int.signed_range n); omega.
-+ apply DFL.
-+ apply DFL.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
 Qed.
 
 Lemma transl_condimm_int32u_correct:
@@ -920,30 +859,19 @@ Lemma transl_condimm_int32u_correct:
   /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
   /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
-  intros. unfold transl_condimm_int32u.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split; auto. rewrite B; auto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm32 GPR31 n (transl_cond_int32u cmp rd r1 GPR31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r).
-  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ apply DFL.
-+ apply DFL.
-+ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto.
-  intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ apply DFL.
-+ apply DFL.
-+ apply DFL.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
 Qed.
 
 Lemma transl_condimm_int64s_correct:
@@ -954,60 +882,19 @@ Lemma transl_condimm_int64s_correct:
   /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
   /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
-  intros. unfold transl_condimm_int64s.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C).
-  exists rs'; eauto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm64 GPR31 n (transl_cond_int64s cmp rd r1 GPR31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r).
-  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ unfold xorimm64. 
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ unfold xorimm64. 
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed).
-* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. 
-  unfold Int64.lt. rewrite zlt_false. auto. 
-  change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed.
-  generalize (Int64.signed_range i); omega.
-* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto.
-  unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
-  destruct (zlt (Int64.signed n) (Int64.signed i)).
-  rewrite zlt_false by omega. auto.
-  rewrite zlt_true by omega. auto.
-  rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
-  assert (Int64.signed n <> Int64.max_signed).
-  { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
-  generalize (Int64.signed_range n); omega.
-+ apply DFL.
-+ apply DFL.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
 Qed.
 
 Lemma transl_condimm_int64u_correct:
@@ -1018,30 +905,19 @@ Lemma transl_condimm_int64u_correct:
   /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
   /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
-  intros. unfold transl_condimm_int64u.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split; auto. rewrite B; auto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm64 GPR31 n (transl_cond_int64u cmp rd r1 GPR31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r).
-  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ apply DFL.
-+ apply DFL.
-+ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto.
-  intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ apply DFL.
-+ apply DFL.
-+ apply DFL.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. app