Cleaned up handling of composite conditions

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

6 files changed, 311 insertions, 99 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index ebb22a6..1870d69 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -85,9 +85,7 @@ Inductive testcond: Type :=
   | Cond_e | Cond_ne
   | Cond_b | Cond_be | Cond_ae | Cond_a
   | Cond_l | Cond_le | Cond_ge | Cond_g
-  | Cond_p | Cond_np
-  | Cond_nep                            (**r synthetic: P or (not Z) *)
-  | Cond_enp.                           (**r synthetic: (not P) and Z *)
+  | Cond_p | Cond_np.
 
 (** Instructions.  IA32 instructions accept many combinations of
   registers, memory references and immediate constants as arguments.
@@ -178,6 +176,7 @@ Inductive instruction: Type :=
   | Pjmp_s (symb: ident)
   | Pjmp_r (r: ireg)
   | Pjcc (c: testcond)(l: label)
+  | Pjcc2 (c1 c2: testcond)(l: label)
   | Pjmptbl (r: ireg) (tbl: list label) (**r pseudo *)
   | Pcall_s (symb: ident)
   | Pcall_r (r: ireg)
@@ -381,6 +380,7 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
       | Vint n => Some (Int.eq n Int.zero)
       | _ => None
       end
+(*
   | Cond_nep =>
       match rs PF, rs ZF with
       | Vint p, Vint z => Some (Int.eq p Int.one || Int.eq z Int.zero)
@@ -391,6 +391,7 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
       | Vint p, Vint z => Some (Int.eq p Int.zero && Int.eq z Int.one)
       | _, _ => None
       end
+*)
   end.
 
 (** The semantics is purely small-step and defined as a function
@@ -580,8 +581,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       end
   | Psetcc c rd =>
       match eval_testcond c rs with
-      | Some true => Next (nextinstr (rs#ECX <- Vundef #EDX <- Vundef #rd <- Vtrue)) m
-      | Some false => Next (nextinstr (rs#ECX <- Vundef #EDX <- Vundef #rd <- Vfalse)) m
+      | Some b => Next (nextinstr (rs#ECX <- Vundef #rd <- (Val.of_bool b))) m
       | None => Stuck
       end
   (** Arithmetic operations over floats *)
@@ -612,6 +612,12 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       | Some false => Next (nextinstr rs) m
       | None => Stuck
       end
+  | Pjcc2 cond1 cond2 lbl =>
+      match eval_testcond cond1 rs, eval_testcond cond2 rs with
+      | Some true, Some true => goto_label c lbl rs m
+      | Some _, Some _ => Next (nextinstr rs) m
+      | _, _ => Stuck
+      end
   | Pjmptbl r tbl =>
       match rs#r with
       | Vint n => 
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index c87167b..452f2e7 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -253,32 +253,59 @@ Definition testcond_for_unsigned_comparison (cmp: comparison) :=
   | Cge => Cond_ae
   end.
 
-Definition testcond_for_condition (cond: condition) : testcond :=
+Inductive extcond: Type :=
+  | Cond_base (c: testcond)
+  | Cond_or (c1 c2: testcond)
+  | Cond_and (c1 c2: testcond).
+
+Definition testcond_for_condition (cond: condition) : extcond :=
   match cond with
-  | Ccomp c => testcond_for_signed_comparison c
-  | Ccompu c => testcond_for_unsigned_comparison c
-  | Ccompimm c n => testcond_for_signed_comparison c
-  | Ccompuimm c n => testcond_for_unsigned_comparison c
+  | Ccomp c => Cond_base(testcond_for_signed_comparison c)
+  | Ccompu c => Cond_base(testcond_for_unsigned_comparison c)
+  | Ccompimm c n => Cond_base(testcond_for_signed_comparison c)
+  | Ccompuimm c n => Cond_base(testcond_for_unsigned_comparison c)
   | Ccompf c =>
       match c with
-      | Ceq => Cond_enp
-      | Cne => Cond_nep
-      | Clt => Cond_a
-      | Cle => Cond_ae
-      | Cgt => Cond_a
-      | Cge => Cond_ae
+      | Ceq => Cond_and Cond_np Cond_e
+      | Cne => Cond_or Cond_p Cond_ne
+      | Clt => Cond_base Cond_a
+      | Cle => Cond_base Cond_ae
+      | Cgt => Cond_base Cond_a
+      | Cge => Cond_base Cond_ae
       end
   | Cnotcompf c =>
       match c with
-      | Ceq => Cond_nep
-      | Cne => Cond_enp
-      | Clt => Cond_be
-      | Cle => Cond_b
-      | Cgt => Cond_be
-      | Cge => Cond_b
+      | Ceq => Cond_or Cond_p Cond_ne
+      | Cne => Cond_and Cond_np Cond_e
+      | Clt => Cond_base Cond_be
+      | Cle => Cond_base Cond_b
+      | Cgt => Cond_base Cond_be
+      | Cge => Cond_base Cond_b
       end
-  | Cmaskzero n => Cond_e
-  | Cmasknotzero n => Cond_ne
+  | Cmaskzero n => Cond_base Cond_e
+  | Cmasknotzero n => Cond_base Cond_ne
+  end.
+
+(** Acting upon extended conditions. *)
+
+Definition mk_setcc (cond: extcond) (rd: ireg) (k: code) :=
+  match cond with
+  | Cond_base c => Psetcc c rd :: k
+  | Cond_and c1 c2 =>
+      if ireg_eq rd EDX
+      then Psetcc c1 EDX :: Psetcc c2 ECX :: Pand_rr EDX ECX :: k
+      else Psetcc c1 EDX :: Psetcc c2 rd  :: Pand_rr rd EDX :: k
+  | Cond_or c1 c2 => 
+      if ireg_eq rd EDX
+      then Psetcc c1 EDX :: Psetcc c2 ECX :: Por_rr EDX ECX :: k
+      else Psetcc c1 EDX :: Psetcc c2 rd  :: Por_rr rd EDX :: k
+  end.
+
+Definition mk_jcc (cond: extcond) (lbl: label) (k: code) :=
+  match cond with
+  | Cond_base c => Pjcc c lbl :: k
+  | Cond_and c1 c2 => Pjcc2 c1 c2 lbl :: k
+  | Cond_or c1 c2 => Pjcc c1 lbl :: Pjcc c2 lbl :: k
   end.
 
 (** Translation of the arithmetic operation [r <- op(args)].
@@ -396,7 +423,7 @@ Definition transl_op
       do r <- freg_of res; do r1 <- ireg_of a1; OK (Pcvtsi2sd_fr r r1 :: k)
   | Ocmp c, args =>
       do r <- ireg_of res;
-      transl_cond c args (Psetcc (testcond_for_condition c) r :: k)
+      transl_cond c args (mk_setcc (testcond_for_condition c) r k)
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
@@ -486,7 +513,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
   | Mgoto lbl =>
       OK(Pjmp_l lbl :: k)
   | Mcond cond args lbl =>
-      transl_cond cond args (Pjcc (testcond_for_condition cond) lbl :: k)
+      transl_cond cond args (mk_jcc (testcond_for_condition cond) lbl k)
   | Mjumptable arg tbl =>
       do r <- ireg_of arg; OK (Pjmptbl r tbl :: k)
   | Mreturn =>
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index d049737..45ac48d 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -401,6 +401,20 @@ Proof.
   destruct (preg_of src); inv H; auto.
 Qed.
 
+Remark mk_setcc_label:
+  forall xc rd k,
+  find_label lbl (mk_setcc xc rd k) = find_label lbl k.
+Proof.
+  intros. destruct xc; simpl; auto; destruct (ireg_eq rd EDX); auto.
+Qed.
+
+Remark mk_jcc_label:
+  forall xc lbl' k,
+  find_label lbl (mk_jcc xc lbl' k) = find_label lbl k.
+Proof.
+  intros. destruct xc; auto.
+Qed.
+
 Ltac ArgsInv :=
   match goal with
   | [ H: Error _ = OK _ |- _ ] => discriminate
@@ -441,7 +455,7 @@ Proof.
   eapply mk_shift_label; eauto.
   eapply mk_shrximm_label; eauto.
   eapply mk_shift_label; eauto.
-  eapply trans_eq. eapply transl_cond_label; eauto. auto.
+  eapply trans_eq. eapply transl_cond_label; eauto. apply mk_setcc_label.
 Qed.
 
 Remark transl_load_label:
@@ -482,7 +496,7 @@ Opaque loadind.
   monadInv H; auto.
   inv H; simpl. destruct (peq lbl l). congruence. auto. 
   monadInv H; auto.
-  eapply trans_eq. eapply transl_cond_label; eauto. auto. 
+  eapply trans_eq. eapply transl_cond_label; eauto. apply mk_jcc_label.
   monadInv H; auto.
   monadInv H; auto.
 Qed.
@@ -624,6 +638,43 @@ Proof.
   econstructor; eauto. eapply exec_straight_at; eauto.
 Qed.
 
+Lemma exec_straight_steps_goto:
+  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
+  match_stack s ->
+  Mem.extends m2 m2' ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  Mach.find_label lbl f.(fn_code) = Some c' ->
+  transl_code_at_pc (rs1 PC) fb f (i :: c) ep tf tc ->
+  edx_preserved ep i = false ->
+  (forall k c, transl_instr f i ep k = OK c ->
+   exists jmp, exists k', exists rs2,
+       exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
+    /\ agree ms2 sp rs2
+    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->
+  exists st',
+  plus step tge (State rs1 m1') E0 st' /\
+  match_states (Machsem.State s fb sp c' ms2 m2) st'.
+Proof.
+  intros. inversion H3. subst. monadInv H9.
+  exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].
+  generalize (functions_transl _ _ _ H7 H8); intro FN.
+  generalize (transf_function_no_overflow _ _ H8); intro NOOV.
+  exploit exec_straight_steps_2; eauto. 
+  intros [ofs' [PC2 CT2]].
+  exploit find_label_goto_label; eauto. 
+  intros [tc' [rs3 [GOTO [AT' OTH]]]].
+  exists (State rs3 m2'); split.
+  eapply plus_right'.
+  eapply exec_straight_steps_1; eauto. 
+  econstructor; eauto.
+  eapply find_instr_tail. eauto. 
+  rewrite C. eexact GOTO.
+  traceEq.
+  econstructor; eauto.
+  apply agree_exten with rs2; auto with ppcgen.
+  congruence.
+Qed.
+
 Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
 Proof. induction 1; simpl. congruence. auto. Qed.
 
@@ -1053,22 +1104,40 @@ Lemma exec_Mcond_true_prop:
 Proof.
   intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0.
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  inv AT. monadInv H5.
+  left; eapply exec_straight_steps_goto; eauto.
+  intros. simpl in H2. 
   exploit transl_cond_correct; eauto. intros [rs' [A [B C]]].
-  generalize (functions_transl _ _ _ FIND H4); intro FN.
-  generalize (transf_function_no_overflow _ _ H4); intro NOOV.
-  exploit exec_straight_steps_2; eauto. 
-  intros [ofs' [PC2 CT2]].
-  exploit find_label_goto_label; eauto. 
-  intros [tc' [rs3 [GOTO [AT3 INV3]]]].
-  left; exists (State rs3 m'); split.
-  eapply plus_right'. 
-  eapply exec_straight_steps_1; eauto.
-  econstructor; eauto.
-  eapply find_instr_tail. eauto. simpl. rewrite B. eauto. traceEq.
-  econstructor; eauto. 
-  eapply agree_exten_temps; eauto. intros. rewrite INV3; auto with ppcgen.
-  congruence.
+  destruct (testcond_for_condition cond); simpl in *.
+(* simple jcc *)
+  exists (Pjcc c1 lbl); exists k; exists rs'.
+  split. eexact A.
+  split. eapply agree_exten_temps; eauto. 
+  simpl. rewrite B. auto.
+(* jcc; jcc *)
+  destruct (eval_testcond c1 rs') as [b1|]_eqn;
+  destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B.
+  destruct b1.   
+  (* first jcc jumps *)
+  exists (Pjcc c1 lbl); exists (Pjcc c2 lbl :: k); exists rs'.
+  split. eexact A.
+  split. eapply agree_exten_temps; eauto. 
+  simpl. rewrite Heqo. auto.
+  (* second jcc jumps *)
+  exists (Pjcc c2 lbl); exists k; exists (nextinstr rs').
+  split. eapply exec_straight_trans. eexact A. 
+  eapply exec_straight_one. simpl. rewrite Heqo. auto. auto.
+  split. eapply agree_exten_temps; eauto. 
+  intros. rewrite nextinstr_inv; auto with ppcgen.
+  simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0.
+  destruct b2; auto || discriminate.
+(* jcc2 *)
+  destruct (eval_testcond c1 rs') as [b1|]_eqn;
+  destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B.
+  destruct (andb_prop _ _ H4). subst. 
+  exists (Pjcc2 c1 c2 lbl); exists k; exists rs'.
+  split. eexact A.
+  split. eapply agree_exten_temps; eauto. 
+  simpl. rewrite Heqo; rewrite Heqo0; auto. 
 Qed.
 
 Lemma exec_Mcond_false_prop:
@@ -1083,11 +1152,34 @@ Proof.
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
   left; eapply exec_straight_steps; eauto. intros. simpl in H0. 
   exploit transl_cond_correct; eauto. intros [rs' [A [B C]]].
+  destruct (testcond_for_condition cond); simpl in *.
+(* simple jcc *)
   econstructor; split.
   eapply exec_straight_trans. eexact A. 
   apply exec_straight_one. simpl. rewrite B. eauto. auto. 
   split. apply agree_nextinstr. eapply agree_exten_temps; eauto.
   simpl; congruence.
+(* jcc ; jcc *)
+  destruct (eval_testcond c1 rs') as [b1|]_eqn;
+  destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B.
+  destruct (orb_false_elim _ _ H2); subst.
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. 
+  eapply exec_straight_two. simpl. rewrite Heqo. eauto. auto. 
+  simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0. eauto. auto. auto.
+  split. apply agree_nextinstr. apply agree_nextinstr. eapply agree_exten_temps; eauto.
+  simpl; congruence.
+(* jcc2 *)
+  destruct (eval_testcond c1 rs') as [b1|]_eqn;
+  destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B.
+  exists (nextinstr rs'); split.
+  eapply exec_straight_trans. eexact A. 
+  apply exec_straight_one. simpl. 
+  rewrite Heqo; rewrite Heqo0. 
+  destruct b1. simpl in *. subst b2. auto. auto.
+  auto.
+  split. apply agree_nextinstr. eapply agree_exten_temps; eauto.
+  rewrite H2; congruence.
 Qed.
 
 Lemma exec_Mjumptable_prop:
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index b3e7aaa..3a91ac5 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -1147,6 +1147,22 @@ Proof.
   intros. repeat SOther. 
 Qed.
 
+Definition eval_extcond (xc: extcond) (rs: regset) : option bool :=
+  match xc with
+  | Cond_base c =>
+      eval_testcond c rs
+  | Cond_and c1 c2 =>
+      match eval_testcond c1 rs, eval_testcond c2 rs with
+      | Some b1, Some b2 => Some (b1 && b2)
+      | _, _ => None
+      end
+  | Cond_or c1 c2 =>
+      match eval_testcond c1 rs, eval_testcond c2 rs with
+      | Some b1, Some b2 => Some (b1 || b2)
+      | _, _ => None
+      end
+  end.
+
 Definition swap_floats (c: comparison) (n1 n2: float) : float :=
   match c with
   | Clt | Cle => n2
@@ -1155,9 +1171,9 @@ Definition swap_floats (c: comparison) (n1 n2: float) : float :=
 
 Lemma testcond_for_float_comparison_correct:
   forall c n1 n2 rs,
-  eval_testcond (testcond_for_condition (Ccompf c))
-                (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
-                                           (Vfloat (swap_floats c n2 n1)) rs)) =
+  eval_extcond (testcond_for_condition (Ccompf c))
+               (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
+                                          (Vfloat (swap_floats c n2 n1)) rs)) =
   Some(Float.cmp c n1 n2).
 Proof.
   intros.
@@ -1165,7 +1181,7 @@ Proof.
   set (rs' := nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
                                         (Vfloat (swap_floats c n2 n1)) rs)).
   intros [A [B [C D]]].
-  unfold eval_testcond. rewrite A; rewrite B; rewrite C.
+  unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C.
   destruct c; simpl.
 (* eq *)
   rewrite Float.cmp_ne_eq.
@@ -1203,9 +1219,9 @@ Qed.
 
 Lemma testcond_for_neg_float_comparison_correct:
   forall c n1 n2 rs,
-  eval_testcond (testcond_for_condition (Cnotcompf c))
-                (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
-                                           (Vfloat (swap_floats c n2 n1)) rs)) =
+  eval_extcond (testcond_for_condition (Cnotcompf c))
+               (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
+                                          (Vfloat (swap_floats c n2 n1)) rs)) =
   Some(negb(Float.cmp c n1 n2)).
 Proof.
   intros.
@@ -1213,7 +1229,7 @@ Proof.
   set (rs' := nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
                                         (Vfloat (swap_floats c n2 n1)) rs)).
   intros [A [B [C D]]].
-  unfold eval_testcond. rewrite A; rewrite B; rewrite C.
+  unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C.
   destruct c; simpl.
 (* eq *)
   rewrite Float.cmp_ne_eq.
@@ -1255,7 +1271,7 @@ Lemma transl_cond_correct:
   eval_condition cond (map rs (map preg_of args)) m = Some b ->
   exists rs',
      exec_straight c rs m k rs' m
-  /\ eval_testcond (testcond_for_condition cond) rs' = Some b
+  /\ eval_extcond (testcond_for_condition cond) rs' = Some b
   /\ forall r, nontemp_preg r = true -> rs'#r = rs r.
 Proof.
   unfold transl_cond; intros. 
@@ -1264,17 +1280,17 @@ Proof.
   simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0. rewrite (ireg_of_eq _ _ EQ1) in H0.
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. simpl in H0. FuncInv.
-  subst b. apply testcond_for_signed_comparison_correct_ii. 
+  subst b. simpl. apply testcond_for_signed_comparison_correct_ii. 
   intros. unfold compare_ints. repeat SOther.
 (* compu *)
   simpl map in H0. 
   rewrite (ireg_of_eq _ _ EQ) in H0. rewrite (ireg_of_eq _ _ EQ1) in H0.
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. simpl in H0. FuncInv.
-  subst b. apply testcond_for_unsigned_comparison_correct_ii. 
-  apply testcond_for_unsigned_comparison_correct_ip; auto. 
-  apply testcond_for_unsigned_comparison_correct_pi; auto.
-  eapply testcond_for_unsigned_comparison_correct_pp; eauto.
+  subst b. simpl; apply testcond_for_unsigned_comparison_correct_ii. 
+  simpl; apply testcond_for_unsigned_comparison_correct_ip; auto. 
+  simpl; apply testcond_for_unsigned_comparison_correct_pi; auto.
+  simpl; eapply testcond_for_unsigned_comparison_correct_pp; eauto.
   intros. unfold compare_ints. repeat SOther.
 (* compimm *)
   simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0.
@@ -1284,14 +1300,14 @@ Proof.
   simpl in H0. FuncInv. simpl. rewrite Int.and_idem. auto. auto.
   apply exec_straight_one; auto.
   split. simpl in H0. FuncInv.
-  subst b. apply testcond_for_signed_comparison_correct_ii.
+  subst b. simpl; apply testcond_for_signed_comparison_correct_ii.
   intros. unfold compare_ints. repeat SOther.
 (* compuimm *)
   simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0.
   econstructor. split. apply exec_straight_one. simpl; eauto. auto.
   split. simpl in H0. FuncInv. 
-  subst b. apply testcond_for_unsigned_comparison_correct_ii. 
-  apply testcond_for_unsigned_comparison_correct_pi; auto.
+  subst b. simpl; apply testcond_for_unsigned_comparison_correct_ii. 
+  simpl; apply testcond_for_unsigned_comparison_correct_pi; auto.
   intros. unfold compare_ints. repeat SOther.
 (* compf *)
   simpl map in H0. rewrite (freg_of_eq _ _ EQ) in H0. rewrite (freg_of_eq _ _ EQ1) in H0.
@@ -1327,6 +1343,78 @@ Proof.
   intros. unfold compare_ints. repeat SOther.
 Qed.
 
+Remark eval_testcond_nextinstr:
+  forall c rs, eval_testcond c (nextinstr rs) = eval_testcond c rs.
+Proof.
+  intros. unfold eval_testcond. repeat rewrite nextinstr_inv; auto with ppcgen.
+Qed.
+
+Remark eval_testcond_set_ireg:
+  forall c rs r v, eval_testcond c (rs#(IR r) <- v) = eval_testcond c rs.
+Proof.
+  intros. unfold eval_testcond. repeat rewrite Pregmap.gso; auto with ppcgen.
+Qed.
+
+Lemma mk_setcc_correct:
+  forall cond rd k rs1 m b,
+  eval_extcond cond rs1 = Some b ->
+  exists rs2,
+  exec_straight (mk_setcc cond rd k) rs1 m k rs2 m
+  /\ rs2#rd = Val.of_bool b
+  /\ forall r, nontemp_preg r = true -> r <> rd -> rs2#r = rs1#r.
+Proof.
+  intros. destruct cond; simpl in *.
+(* base *)
+  econstructor; split.
+  apply exec_straight_one. simpl; rewrite H. eauto. auto.
+  split. repeat SRes. 
+  intros. repeat SOther. 
+(* or *)
+  destruct (eval_testcond c1 rs1) as [b1|]_eqn;
+  destruct (eval_testcond c2 rs1) as [b2|]_eqn; inv H.
+  assert (D: Val.or (Val.of_bool b1) (Val.of_bool b2) = Val.of_bool (b1 || b2)).
+    destruct b1; destruct b2; auto.
+  destruct (ireg_eq rd EDX).
+  subst rd. econstructor; split.
+  eapply exec_straight_three.
+  simpl; rewrite Heqo; eauto.
+  simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg.  rewrite Heqo0. eauto. 
+  simpl. eauto. 
+  auto. auto. auto.
+  split. SRes. 
+  intros. repeat SOther.
+  econstructor; split.
+  eapply exec_straight_three.
+  simpl; rewrite Heqo; eauto.
+  simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg.  rewrite Heqo0. eauto. 
+  simpl. eauto. 
+  auto. auto. auto.
+  split. repeat SRes. rewrite <- D. rewrite Val.or_commut. decEq; repeat SRes. 
+  intros. repeat SOther.
+(* and *)
+  destruct (eval_testcond c1 rs1) as [b1|]_eqn;
+  destruct (eval_testcond c2 rs1) as [b2|]_eqn; inv H.
+  assert (D: Val.and (Val.of_bool b1) (Val.of_bool b2) = Val.of_bool (b1 && b2)).
+    destruct b1; destruct b2; auto.
+  destruct (ireg_eq rd EDX).
+  subst rd. econstructor; split.
+  eapply exec_straight_three.
+  simpl; rewrite Heqo; eauto.
+  simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg.  rewrite Heqo0. eauto. 
+  simpl. eauto. 
+  auto. auto. auto.
+  split. SRes. 
+  intros. repeat SOther.
+  econstructor; split.
+  eapply exec_straight_three.
+  simpl; rewrite Heqo; eauto.
+  simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg.  rewrite Heqo0. eauto. 
+  simpl. eauto. 
+  auto. auto. auto.
+  split. repeat SRes. rewrite <- D. rewrite Val.and_commut. decEq; repeat SRes. 
+  intros. repeat SOther.
+Qed.
+
 (** Translation of arithmetic operations. *)
 
 (*
@@ -1367,8 +1455,6 @@ Ltac TranslOp :=
   [ apply exec_straight_one; [ simpl; eauto | auto ] 
   | split; [ repeat SRes | intros; repeat SOther ]].
 
-(* Move elsewhere *)
-
 Lemma transl_op_correct:
   forall op args res k c (rs: regset) m v,
   transl_op op args res k = OK c ->
@@ -1425,11 +1511,11 @@ Proof.
   remember (eval_condition c0 rs ## (preg_of ## args) m) as ob. destruct ob; inv EV. 
   rewrite (eval_condition_weaken _ _ _ (sym_equal Heqob)). 
   exploit transl_cond_correct; eauto. intros [rs2 [P [Q R]]].
-  exists (nextinstr (rs2#ECX <- Vundef #EDX <- Vundef #x <- v)).
-  split. eapply exec_straight_trans. eauto. 
-  apply exec_straight_one. simpl. rewrite Q. destruct b; inv H0; auto. auto.
-  split. repeat SRes. destruct b; inv H0; auto. 
-  intros. repeat SOther. 
+  exploit mk_setcc_correct; eauto. intros [rs3 [S [T U]]].
+  exists rs3.
+  split. eapply exec_straight_trans. eexact P. eexact S.
+  split. auto.
+  intros. transitivity (rs2 r); auto.
 Qed.
 
 (** Translation of memory loads. *)
diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v
index 674a73e..e0787d7 100644
--- a/ia32/Asmgenretaddr.v
+++ b/ia32/Asmgenretaddr.v
@@ -173,8 +173,24 @@ Proof.
   unfold storeind; intros. destruct ty; IsTail. destruct (preg_of src); IsTail.
 Qed.
 
+Lemma mk_setcc_tail:
+  forall cond rd k, is_tail k (mk_setcc cond rd k).
+Proof.
+  unfold mk_setcc; intros. destruct cond.
+  IsTail.
+  destruct (ireg_eq rd EDX); IsTail.
+  destruct (ireg_eq rd EDX); IsTail.
+Qed.
+
+Lemma mk_jcc_tail:
+  forall cond lbl k, is_tail k (mk_jcc cond lbl k).
+Proof.
+  unfold mk_jcc; intros. destruct cond; IsTail.
+Qed.
+
 Hint Resolve mk_mov_tail mk_shift_tail mk_div_tail mk_mod_tail mk_shrximm_tail
-             mk_intconv_tail mk_smallstore_tail loadind_tail storeind_tail : ppcretaddr.
+             mk_intconv_tail mk_smallstore_tail loadind_tail storeind_tail
+             mk_setcc_tail mk_jcc_tail : ppcretaddr.
 
 Lemma transl_cond_tail:
   forall cond args k c, transl_cond cond args k = OK c -> is_tail k c.
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 6f02a8a..a6369c4 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -132,7 +132,12 @@ let name_of_condition = function
   | Cond_b -> "b" | Cond_be -> "be" | Cond_ae -> "ae" | Cond_a -> "a"
   | Cond_l -> "l" | Cond_le -> "le" | Cond_ge -> "ge" | Cond_g -> "g"
   | Cond_p -> "p" | Cond_np -> "np" 
-  | Cond_nep | Cond_enp -> assert false (* treated specially *)
+
+let name_of_neg_condition = function
+  | Cond_e -> "ne" | Cond_ne -> "e"
+  | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be"
+  | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le"
+  | Cond_p -> "np" | Cond_np -> "p" 
 
 let section oc name =
   fprintf oc "	%s\n" name
@@ -218,14 +223,11 @@ let need_masks = ref false
 
 (* Built-in functions *)
 
-(* Built-ins.  They come in three flavors: 
+(* Built-ins.  They come in two flavors: 
    - annotation statements: take their arguments in registers or stack
      locations; generate no code;
    - inlined by the compiler: take their arguments in arbitrary
-     registers; preserve all registers except ECX, EDX, XMM6 and XMM7
-   - inlined while printing asm code; take their arguments in
-     locations dictated by the calling conventions; preserve
-     callee-save regs only. *)
+     registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *)
 
 (* Handling of annotations *)
 
@@ -588,21 +590,9 @@ let print_instruction oc = function
   | Ptest_ri(r1, n) ->
       fprintf oc "	testl	$%a, %a\n" coqint n ireg r1
   | Pcmov(c, rd, r1) ->
-      assert (c <> Cond_nep && c <> Cond_enp);
       fprintf oc "	cmov%s	%a, %a\n" (name_of_condition c) ireg r1 ireg rd
   | Psetcc(c, rd) ->
-      begin match c with
-      | Cond_nep ->
-          fprintf oc "	setne	%%cl\n";
-          fprintf oc "	setp	%%dl\n";
-          fprintf oc "	orb	%%dl, %%cl\n"
-      | Cond_enp ->
-          fprintf oc "	sete	%%cl\n";
-          fprintf oc "	setnp	%%dl\n";
-          fprintf oc "	andb	%%dl, %%cl\n"
-      | _ ->
-          fprintf oc "	set%s	%%cl\n" (name_of_condition c)
-      end;
+      fprintf oc "	set%s	%%cl\n" (name_of_condition c);
       fprintf oc "	movzbl	%%cl, %a\n" ireg rd
   (** Arithmetic operations over floats *)
   | Paddd_ff(rd, r1) ->
@@ -630,18 +620,13 @@ let print_instruction oc = function
       fprintf oc "	jmp	*%a\n" ireg r
   | Pjcc(c, l) ->
       let l = transl_label l in
-      begin match c with
-      | Cond_nep ->
-          fprintf oc "	jp	%a\n" label l;
-          fprintf oc "	jne	%a\n" label l
-      | Cond_enp ->
-          let l' = new_label() in
-          fprintf oc "	jp	%a\n" label l';
-          fprintf oc "	je	%a\n" label l;
-          fprintf oc "%a:\n" label l'
-      | _ ->
-          fprintf oc "	j%s	%a\n" (name_of_condition c) label l
-      end
+      fprintf oc "	j%s	%a\n" (name_of_condition c) label l
+  | Pjcc2(c1, c2, l) ->
+      let l = transl_label l in
+      let l' = new_label() in
+      fprintf oc "	j%s	%a\n" (name_of_neg_condition c1) label l';
+      fprintf oc "	j%s	%a\n" (name_of_condition c2) label l;
+      fprintf oc "%a:\n" label l'
   | Pjmptbl(r, tbl) ->
       let l = new_label() in
       fprintf oc "	jmp	*%a(, %a, 4)\n" label l ireg r;