Implement a `Osel` operation for x86

The operation compiles down to conditional moves.

11 files changed, 298 insertions, 38 deletions

diff --git a/x86/Asm.v b/x86/Asm.v
index 32235c2d..58e28c40 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -851,11 +851,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Ptestq_ri r1 n =>
       Next (nextinstr (compare_longs (Val.andl (rs r1) (Vlong n)) (Vlong Int64.zero) rs m)) m
   | Pcmov c rd r1 =>
-      match eval_testcond c rs with
-      | Some true => Next (nextinstr (rs#rd <- (rs#r1))) m
-      | Some false => Next (nextinstr rs) m
-      | None => Next (nextinstr (rs#rd <- Vundef)) m
-      end
+      let v :=
+        match eval_testcond c rs with
+        | Some b => if b then rs#r1 else rs#rd
+        | None   => Vundef
+      end in
+      Next (nextinstr (rs#rd <- v)) m
   | Psetcc c rd =>
       Next (nextinstr (rs#rd <- (Val.of_optbool (eval_testcond c rs)))) m
   (** Arithmetic operations over double-precision floats *)
diff --git a/x86/Asmgen.v b/x86/Asmgen.v
index dedbfbe6..73e3263e 100644
--- a/x86/Asmgen.v
+++ b/x86/Asmgen.v
@@ -305,6 +305,35 @@ Definition mk_jcc (cond: extcond) (lbl: label) (k: code) :=
   | Cond_or c1 c2 => Pjcc c1 lbl :: Pjcc c2 lbl :: k
   end.
 
+Definition negate_testcond (c: testcond) : testcond :=
+  match c with
+  | Cond_e => Cond_ne  | Cond_ne => Cond_e
+  | Cond_b => Cond_ae  | Cond_be => Cond_a
+  | Cond_ae => Cond_b  | Cond_a => Cond_be
+  | Cond_l => Cond_ge  | Cond_le => Cond_g
+  | Cond_ge => Cond_l  | Cond_g => Cond_le
+  | Cond_p => Cond_np  | Cond_np => Cond_p
+  end.
+
+Definition mk_sel (cond: extcond) (rd r2: ireg) (k: code) :=
+  match cond with
+  | Cond_base c =>
+      OK (Pcmov (negate_testcond c) rd r2 :: k)
+  | Cond_and c1 c2 =>
+      OK (Pcmov (negate_testcond c1) rd r2 ::
+          Pcmov (negate_testcond c2) rd r2 :: k)
+  | Cond_or c1 c2 =>
+      Error (msg "Asmgen.mk_sel")    (**r should never happen, see [SelectOp.select] *)
+  end.
+
+Definition transl_sel
+      (cond: condition) (args: list mreg) (rd r2: ireg) (k: code) : res code :=
+  if ireg_eq rd r2 then
+    OK (Pmov_rr rd r2 :: k)    (* must generate one instruction... *)
+  else
+    do k1 <- mk_sel (testcond_for_condition cond) rd r2 k;
+    transl_cond cond args k1.
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
@@ -597,6 +626,10 @@ Definition transl_op
   | Ocmp c, args =>
       do r <- ireg_of res;
       transl_cond c args (mk_setcc (testcond_for_condition c) r k)
+  | Osel c ty, a1 :: a2 :: args =>
+      assertion (mreg_eq a1 res);
+      do r <- ireg_of res; do r2 <- ireg_of a2;
+      transl_sel c args r r2 k
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v
index 3aa87a4c..f1fd41e3 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -194,6 +194,14 @@ Proof.
   intros. destruct xc; simpl; TailNoLabel.
 Qed.
 
+Remark mk_sel_label:
+  forall xc rd r2 k c,
+  mk_sel xc rd r2 k = OK c ->
+  tail_nolabel k c.
+Proof.
+  unfold mk_sel; intros; destruct xc; inv H; TailNoLabel.
+Qed.
+
 Remark transl_cond_label:
   forall cond args k c,
   transl_cond cond args k = OK c ->
@@ -221,6 +229,9 @@ Proof.
   destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
   destruct (normalize_addrmode_64 x) as [am' [delta|]]; TailNoLabel.
   eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_setcc_label.
+  unfold transl_sel in EQ2. destruct (ireg_eq x x0); monadInv EQ2.
+  TailNoLabel.
+  eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_sel_label; eauto.
 Qed.
 
 Remark transl_load_label:
@@ -706,7 +717,7 @@ Opaque loadind.
   intros. simpl in TR.
   destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR)
   as [rs' [A [B C]]].
-  rewrite EC in B.
+  rewrite EC in B. destruct B as [B _].
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   exists (Pjcc c1 lbl); exists k; exists rs'.
@@ -744,7 +755,7 @@ Opaque loadind.
   left; eapply exec_straight_steps; eauto. intros. simpl in TR.
   destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR)
   as [rs' [A [B C]]].
-  rewrite EC in B.
+  rewrite EC in B. destruct B as [B _].
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   econstructor; split.
diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v
index 904debdc..fd88954e 100644
--- a/x86/Asmgenproof1.v
+++ b/x86/Asmgenproof1.v
@@ -208,7 +208,8 @@ Proof.
   set (x' := Int.add x tnm1).
   set (rs2 := nextinstr (compare_ints (Vint x) (Vint Int.zero) rs1 m)).
   set (rs3 := nextinstr (rs2#RCX <- (Vint x'))).
-  set (rs4 := nextinstr (if Int.lt x Int.zero then rs3#RAX <- (Vint x') else rs3)).
+  set (v' := if Int.lt x Int.zero then Vint x' else Vint x).
+  set (rs4 := nextinstr (rs3#RAX <- v')).
   set (rs5 := nextinstr_nf (rs4#RAX <- (Val.shr rs4#RAX (Vint n)))).
   assert (rs3#RAX = Vint x). unfold rs3. Simplifs.
   assert (rs3#RCX = Vint x'). unfold rs3. Simplifs.
@@ -218,13 +219,12 @@ Proof.
   change (rs2 RAX) with (rs1 RAX). rewrite A. simpl.
   rewrite Int.repr_unsigned. rewrite Int.add_zero_l. auto. auto.
   apply exec_straight_step with rs4 m. simpl.
-  rewrite Int.lt_sub_overflow. unfold rs4. destruct (Int.lt x Int.zero); simpl; auto.
-  unfold rs4. destruct (Int.lt x Int.zero); simpl; auto.
+  rewrite Int.lt_sub_overflow. unfold rs4, v'. rewrite H, H0. destruct (Int.lt x Int.zero); simpl; auto.
+  auto.
   apply exec_straight_one. auto. auto.
   split. unfold rs5. Simplifs. unfold rs4. rewrite nextinstr_inv; auto with asmgen.
-  destruct (Int.lt x Int.zero). rewrite Pregmap.gss. rewrite A; auto. rewrite A; rewrite H; auto.
+  rewrite Pregmap.gss. unfold v'. rewrite A. reflexivity.
   intros. unfold rs5. Simplifs. unfold rs4. Simplifs.
-  transitivity (rs3#r). destruct (Int.lt x Int.zero). Simplifs. auto.
   unfold rs3. Simplifs. unfold rs2. Simplifs.
   unfold compare_ints. Simplifs.
 Qed.
@@ -913,6 +913,7 @@ Lemma transl_cond_correct:
   /\ match eval_condition cond (map rs (map preg_of args)) m with
      | None => True
      | Some b => eval_extcond (testcond_for_condition cond) rs' = Some b
+              /\ eval_extcond (testcond_for_condition (negate_condition cond)) rs' = Some (negb b)
      end
   /\ forall r, data_preg r = true -> rs'#r = rs r.
 Proof.
@@ -921,58 +922,78 @@ Proof.
 - (* comp *)
   simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:?; auto.
+  split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:?; auto. split.
+  eapply testcond_for_signed_comparison_32_correct; eauto.
   eapply testcond_for_signed_comparison_32_correct; eauto.
+  rewrite Val.negate_cmp_bool, Heqo; auto.
   intros. unfold compare_ints. Simplifs.
 - (* compu *)
   simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto.
+  split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto. split.
   eapply testcond_for_unsigned_comparison_32_correct; eauto.
+  eapply testcond_for_unsigned_comparison_32_correct; eauto.
+  rewrite Val.negate_cmpu_bool, Heqo; auto.
   intros. unfold compare_ints. Simplifs.
 - (* compimm *)
   simpl. rewrite (ireg_of_eq _ _ EQ). destruct (Int.eq_dec n Int.zero).
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. destruct (rs x); simpl; auto. subst. rewrite Int.and_idem.
+  split. destruct (rs x); simpl; auto. subst. rewrite Int.and_idem. split.
+  eapply testcond_for_signed_comparison_32_correct; eauto.
   eapply testcond_for_signed_comparison_32_correct; eauto.
+  rewrite Val.negate_cmp_bool; auto.
   intros. unfold compare_ints. Simplifs.
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. destruct (Val.cmp_bool c0 (rs x) (Vint n)) eqn:?; auto.
+  split. destruct (Val.cmp_bool c0 (rs x) (Vint n)) eqn:?; auto. split.
   eapply testcond_for_signed_comparison_32_correct; eauto.
+  eapply testcond_for_signed_comparison_32_correct; eauto.
+  rewrite Val.negate_cmp_bool, Heqo; auto.
   intros. unfold compare_ints. Simplifs.
 - (* compuimm *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint n)) eqn:?; auto.
+  split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint n)) eqn:?; auto; split.
+  eapply testcond_for_unsigned_comparison_32_correct; eauto.
   eapply testcond_for_unsigned_comparison_32_correct; eauto.
+  rewrite Val.negate_cmpu_bool, Heqo; auto.
   intros. unfold compare_ints. Simplifs.
 - (* compl *)
   simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmpl_bool c0 (rs x) (rs x0)) eqn:?; auto.
+  split. destruct (Val.cmpl_bool c0 (rs x) (rs x0)) eqn:?; auto. split.
   eapply testcond_for_signed_comparison_64_correct; eauto.
+  eapply testcond_for_signed_comparison_64_correct; eauto.
+  rewrite Val.negate_cmpl_bool, Heqo; auto.
   intros. unfold compare_longs. Simplifs.
 - (* complu *)
   simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmplu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto.
+  split. destruct (Val.cmplu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto. split.
+  eapply testcond_for_unsigned_comparison_64_correct; eauto.
   eapply testcond_for_unsigned_comparison_64_correct; eauto.
+  rewrite Val.negate_cmplu_bool, Heqo; auto.
   intros. unfold compare_longs. Simplifs.
 - (* compimm *)
   simpl. rewrite (ireg_of_eq _ _ EQ). destruct (Int64.eq_dec n Int64.zero).
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. destruct (rs x); simpl; auto. subst. rewrite Int64.and_idem.
+  split. destruct (rs x); simpl; auto. subst. rewrite Int64.and_idem. split.
   eapply testcond_for_signed_comparison_64_correct; eauto.
+  eapply testcond_for_signed_comparison_64_correct; eauto.
+  rewrite Val.negate_cmpl_bool; auto.
   intros. unfold compare_longs. Simplifs.
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. destruct (Val.cmpl_bool c0 (rs x) (Vlong n)) eqn:?; auto.
+  split. destruct (Val.cmpl_bool c0 (rs x) (Vlong n)) eqn:?; auto. split.
+  eapply testcond_for_signed_comparison_64_correct; eauto.
   eapply testcond_for_signed_comparison_64_correct; eauto.
+  rewrite Val.negate_cmpl_bool, Heqo; auto.
   intros. unfold compare_longs. Simplifs.
 - (* compuimm *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmplu_bool (Mem.valid_pointer m) c0 (rs x) (Vlong n)) eqn:?; auto.
+  split. destruct (Val.cmplu_bool (Mem.valid_pointer m) c0 (rs x) (Vlong n)) eqn:?; auto. split.
   eapply testcond_for_unsigned_comparison_64_correct; eauto.
+  eapply testcond_for_unsigned_comparison_64_correct; eauto.
+  rewrite Val.negate_cmplu_bool, Heqo; auto.
   intros. unfold compare_longs. Simplifs.
 - (* compf *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
@@ -981,7 +1002,9 @@ Proof.
   destruct c0; simpl; auto.
   unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen.
   split. destruct (rs x); destruct (rs x0); simpl; auto.
-  repeat rewrite swap_floats_commut. apply testcond_for_float_comparison_correct.
+  repeat rewrite swap_floats_commut. split.
+  apply testcond_for_float_comparison_correct.
+  apply testcond_for_neg_float_comparison_correct.
   intros. Simplifs. apply compare_floats_inv; auto with asmgen.
 - (* notcompf *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
@@ -990,7 +1013,9 @@ Proof.
   destruct c0; simpl; auto.
   unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen.
   split. destruct (rs x); destruct (rs x0); simpl; auto.
-  repeat rewrite swap_floats_commut. apply testcond_for_neg_float_comparison_correct.
+  repeat rewrite swap_floats_commut. split.
+  apply testcond_for_neg_float_comparison_correct.
+  rewrite negb_involutive. apply testcond_for_float_comparison_correct.
   intros. Simplifs. apply compare_floats_inv; auto with asmgen.
 - (* compfs *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
@@ -999,7 +1024,9 @@ Proof.
   destruct c0; simpl; auto.
   unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen.
   split. destruct (rs x); destruct (rs x0); simpl; auto.
-  repeat rewrite swap_floats_commut. apply testcond_for_float32_comparison_correct.
+  repeat rewrite swap_floats_commut. split.
+  apply testcond_for_float32_comparison_correct.
+  apply testcond_for_neg_float32_comparison_correct.
   intros. Simplifs. apply compare_floats32_inv; auto with asmgen.
 - (* notcompfs *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
@@ -1008,7 +1035,9 @@ Proof.
   destruct c0; simpl; auto.
   unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen.
   split. destruct (rs x); destruct (rs x0); simpl; auto.
-  repeat rewrite swap_floats_commut. apply testcond_for_neg_float32_comparison_correct.
+  repeat rewrite swap_floats_commut. split.
+  apply testcond_for_neg_float32_comparison_correct.
+  rewrite negb_involutive. apply testcond_for_float32_comparison_correct.
   intros. Simplifs. apply compare_floats32_inv; auto with asmgen.
 - (* maskzero *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
@@ -1133,6 +1162,94 @@ Proof.
   intuition Simplifs.
 Qed.
 
+Definition negate_extcond (xc: extcond) : extcond :=
+  match xc with
+  | Cond_base c => Cond_base (negate_testcond c)
+  | Cond_and c1 c2 => Cond_or (negate_testcond c1) (negate_testcond c2)
+  | Cond_or c1 c2 => Cond_and (negate_testcond c1) (negate_testcond c2)
+  end.
+
+Remark negate_testcond_for_condition:
+  forall cond,
+  negate_extcond (testcond_for_condition cond) = testcond_for_condition (negate_condition cond).
+Proof.
+  intros. destruct cond; try destruct c; reflexivity.
+Qed.
+
+Lemma mk_sel_correct:
+  forall xc ty rd r2 k c ob rs m,
+  mk_sel xc rd r2 k = OK c ->
+  rd <> r2 ->
+  match ob with
+  | Some b => eval_extcond xc rs = Some b /\ eval_extcond (negate_extcond xc) rs = Some (negb b)
+  | None => True
+  end ->
+  exists rs',
+     exec_straight ge fn c rs m k rs' m
+  /\ Val.lessdef (Val.select ob rs#rd rs#r2 ty) rs'#rd
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs r.
+Proof.
+  intros. destruct xc; monadInv H; simpl in H1.
+- econstructor; split.
+  eapply exec_straight_one. reflexivity. reflexivity.
+  set (v :=  match eval_testcond (negate_testcond c0) rs with
+     | Some true => rs r2
+     | Some false => rs rd
+     | None => Vundef
+     end).
+  split. rewrite nextinstr_inv, Pregmap.gss by eauto with asmgen.
+  destruct ob; simpl; auto. destruct H1 as [_ B]; unfold v; rewrite B. 
+  destruct b; apply Val.lessdef_normalize.
+  intros; Simplifs.
+- econstructor; split.
+  eapply exec_straight_two. 
+  reflexivity. reflexivity. reflexivity. reflexivity.
+  set (v1 :=  match eval_testcond (negate_testcond c1) rs with
+     | Some true => rs r2
+     | Some false => rs rd
+     | None => Vundef
+     end).
+  rewrite eval_testcond_nextinstr, eval_testcond_set_ireg. 
+  set (v2 :=  match eval_testcond (negate_testcond c2) rs with
+     | Some true => nextinstr rs # rd <- v1 r2
+     | Some false => nextinstr rs # rd <- v1 rd
+     | None => Vundef
+     end).
+  split. rewrite nextinstr_inv, Pregmap.gss by eauto with asmgen.
+  destruct ob; simpl; auto.
+  destruct H1 as [_ B]. 
+  destruct (eval_testcond (negate_testcond c1) rs) as [b1|]; try discriminate.
+  destruct (eval_testcond (negate_testcond c2) rs) as [b2|]; try discriminate.
+  inv B. apply negb_sym in H1. subst b.
+  replace v2 with (if b2 then rs#r2 else v1).
+  unfold v1. destruct b1, b2; apply Val.lessdef_normalize.
+  unfold v2. destruct b2; symmetry; Simplifs.
+  intros; Simplifs.
+Qed.
+
+Lemma transl_sel_correct:
+  forall ty cond args rd r2 k c rs m,
+  transl_sel cond args rd r2 k = OK c ->
+  exists rs',
+     exec_straight ge fn c rs m k rs' m
+  /\ Val.lessdef (Val.select (eval_condition cond (map rs (map preg_of args)) m) rs#rd rs#r2 ty) rs'#rd
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs r.
+Proof.
+  unfold transl_sel; intros. destruct (ireg_eq rd r2); monadInv H. 
+- econstructor; split. 
+  apply exec_straight_one; reflexivity.
+  split. rewrite nextinstr_inv, Pregmap.gss by auto with asmgen. 
+  destruct eval_condition as [[]|]; simpl; auto using Val.lessdef_normalize.
+  intros; Simplifs.
+- destruct (transl_cond_correct _ _ _ _ rs m EQ0) as (rs1 & A & B & C).
+  rewrite <- negate_testcond_for_condition in B.
+  destruct (mk_sel_correct _ ty _ _ _ _ _ rs1 m EQ n B) as (rs2 & D & E & F).
+  exists rs2; split. 
+  eapply exec_straight_trans; eauto. 
+  split. rewrite ! C in E by auto with asmgen. exact E.
+  intros. rewrite F; auto.
+Qed.
+
 (** Translation of arithmetic operations. *)
 
 Ltac ArgsInv :=
@@ -1142,7 +1259,9 @@ Ltac ArgsInv :=
   | [ H: bind _ _ = OK _ |- _ ] => monadInv H; ArgsInv
   | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
   | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
-  | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *; clear H; ArgsInv
+  | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *; 
+                                    let X := fresh "EQ" in generalize (ireg_of_eq _ _ H); intros X;
+                                    clear H; ArgsInv
   | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *; clear H; ArgsInv
   | _ => idtac
   end.
@@ -1334,9 +1453,12 @@ Transparent destroyed_by_op.
   exists rs3.
   split. eapply exec_straight_trans. eexact P. eexact S.
   split. rewrite T. destruct (eval_condition cond rs ## (preg_of ## args) m).
-  rewrite Q. auto.
+  destruct Q as [Q _]. rewrite Q. auto.
   simpl; auto.
   intros. transitivity (rs2 r); auto.
+(* selection *)
+  rewrite EQ1. exploit transl_sel_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. eauto.
 Qed.
 
 (** Translation of memory loads. *)
diff --git a/x86/Machregs.v b/x86/Machregs.v
index bdf492ed..6f3064b8 100644
--- a/x86/Machregs.v
+++ b/x86/Machregs.v
@@ -351,6 +351,7 @@ Definition two_address_op (op: operation) : bool :=
   | Olongofsingle => false
   | Osingleoflong => false
   | Ocmp c => false
+  | Osel c op => true
   end.
 
 (* Constraints on constant propagation for builtins *)
diff --git a/x86/NeedOp.v b/x86/NeedOp.v
index 68ecc745..d9a58fbb 100644
--- a/x86/NeedOp.v
+++ b/x86/NeedOp.v
@@ -120,6 +120,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ointoffloat | Ofloatofint | Ointofsingle | Osingleofint => op1 (default nv)
   | Olongoffloat | Ofloatoflong | Olongofsingle | Osingleoflong => op1 (default nv)
   | Ocmp c => needs_of_condition c
+  | Osel c ty => nv :: nv :: needs_of_condition c
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
@@ -231,6 +232,10 @@ Proof.
   erewrite needs_of_condition_sound by eauto.
   subst v; simpl. auto with na.
   subst v; auto with na.
+- destruct (eval_condition c args m) as [b|] eqn:EC.
+  erewrite needs_of_condition_sound by eauto.
+  apply select_sound; auto.
+  simpl; auto with na.
 Qed.
 
 Lemma operation_is_redundant_sound:
diff --git a/x86/Op.v b/x86/Op.v
index 79c84ca2..16d75426 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -167,7 +167,9 @@ Inductive operation : Type :=
   | Olongofsingle            (**r [rd = signed_long_of_float32(r1)] *)
   | Osingleoflong            (**r [rd = float32_of_signed_long(r1)] *)
 (*c Boolean tests: *)
-  | Ocmp (cond: condition).  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Ocmp (cond: condition)  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Osel: condition -> typ -> operation.
+                             (**r [rd = rs1] if condition holds, [rd = rs2] otherwise. *)
 
 (** Comparison functions (used in modules [CSE] and [Allocation]). *)
 
@@ -186,7 +188,7 @@ Defined.
 
 Definition beq_operation: forall (x y: operation), bool.
 Proof.
-  generalize Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_addressing eq_condition; boolean_equality.
+  generalize Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec ident_eq typ_eq eq_addressing eq_condition; boolean_equality.
 Defined.
 
 Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}.
@@ -407,6 +409,7 @@ Definition eval_operation
   | Olongofsingle, v1::nil => Val.longofsingle v1
   | Osingleoflong, v1::nil => Val.singleoflong v1
   | Ocmp c, _ => Some(Val.of_optbool (eval_condition c vl m))
+  | Osel c ty, v1::v2::vl => Some(Val.select (eval_condition c vl m) v1 v2 ty)
   | _, _ => None
   end.
 
@@ -578,6 +581,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Olongofsingle => (Tsingle :: nil, Tlong)
   | Osingleoflong => (Tlong :: nil, Tsingle)
   | Ocmp c => (type_of_condition c, Tint)
+  | Osel c ty => (ty :: ty :: type_of_condition c, ty)
   end.
 
 (** Weak type soundness results for [eval_operation]:
@@ -735,6 +739,7 @@ Proof with (try exact I; try reflexivity).
   destruct v0; simpl in H0; inv H0. destruct (Float32.to_long f); inv H2...
   destruct v0; simpl in H0; inv H0...
   destruct (eval_condition cond vl m); simpl... destruct b...
+  unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I.
 Qed.
 
 End SOUNDNESS.
@@ -958,23 +963,42 @@ Definition is_trivial_op (op: operation) : bool :=
 
 (** Operations that depend on the memory state. *)
 
+Definition condition_depends_on_memory (c: condition) : bool :=
+  match c with
+  | Ccompu _ => negb Archi.ptr64
+  | Ccompuimm _ _ => negb Archi.ptr64
+  | Ccomplu _ => Archi.ptr64
+  | Ccompluimm _ _ => Archi.ptr64
+  | _ => false
+  end.
+
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp (Ccompu _) => negb Archi.ptr64
-  | Ocmp (Ccompuimm _ _) => negb Archi.ptr64
-  | Ocmp (Ccomplu _) => Archi.ptr64
-  | Ocmp (Ccompluimm _ _) => Archi.ptr64
+  | Ocmp c => condition_depends_on_memory c
+  | Osel c ty => condition_depends_on_memory c
   | _ => false
   end.
 
+Lemma condition_depends_on_memory_correct:
+  forall c args m1 m2,
+  condition_depends_on_memory c = false ->
+  eval_condition c args m1 = eval_condition c args m2.
+Proof.
+  intros until m2. 
+  destruct c; simpl; intros SF; auto; rewrite ? negb_false_iff in SF;
+  unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
+Qed.
+
 Lemma op_depends_on_memory_correct:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   op_depends_on_memory op = false ->
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
-  intros until m2. destruct op; simpl; try congruence.
-  destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF;
-  unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
+  intros until m2. destruct op; simpl; try congruence; intros C.
+- f_equal; f_equal; apply condition_depends_on_memory_correct; auto.
+- destruct args; auto. destruct args; auto.
+  rewrite (condition_depends_on_memory_correct c args m1 m2 C).
+  auto.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
@@ -1290,6 +1314,9 @@ Proof.
   exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
   destruct b; simpl; constructor.
   simpl; constructor.
+  apply Val.select_inject; auto.  
+  destruct (eval_condition c vl1 m1) eqn:?; auto.
+  right; symmetry; eapply eval_condition_inj; eauto.
 Qed.
 
 End EVAL_COMPAT.
diff --git a/x86/PrintOp.ml b/x86/PrintOp.ml
index faa5bb5f..6aa4d450 100644
--- a/x86/PrintOp.ml
+++ b/x86/PrintOp.ml
@@ -164,6 +164,10 @@ let print_operation reg pp = function
   | Olongofsingle, [r1] -> fprintf pp "longofsingle(%a)" reg r1
   | Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1
   | Ocmp c, args -> print_condition reg pp (c, args)
+  | Osel (c, ty), r1::r2::args ->
+      fprintf pp "%a ?%s %a : %a"
+         (print_condition reg) (c, args)
+         (PrintAST.name_of_type ty) reg r1 reg r2
   | _ -> fprintf pp "<bad operator>"
 
 
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index a1583600..cf0f37ec 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -456,7 +456,35 @@ Nondetfunction cast16signed (e: expr) :=
       Eop Ocast16signed (e ::: Enil)
   end.
 
-(** Floating-point conversions *)
+(** ** Selection *)
+
+Definition select_supported (ty: typ) : bool :=
+  match ty with
+  | Tint => true
+  | Tlong => Archi.ptr64
+  | _ => false
+  end.
+
+(** [Asmgen.mk_sel] cannot always handle the conditions that are
+    implemented as a "and" of two processor flags.  However it can
+    handle the negation of those conditions, which are implemented
+    as an "or".  So, for the risky conditions we just take their
+    negation and swap the two arguments of the [select]. *)
+
+Definition select_swap (cond: condition) :=
+  match cond with
+  | Ccompf Cne | Ccompfs Cne | Cnotcompf Ceq | Cnotcompfs Ceq => true
+  | _ => false
+  end.
+
+Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
+  if select_supported ty then
+    if select_swap cond
+    then Some (Eop (Osel (negate_condition cond) ty) (e2 ::: e1 ::: args))
+    else Some (Eop (Osel cond ty) (e1 ::: e2 ::: args))
+  else None.
+
+(** ** Floating-point conversions *)
 
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
 Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index fdbadaa8..b412ccf7 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -769,6 +769,32 @@ Proof.
   TrivialExists.
 Qed.
 
+Theorem eval_select: 
+  forall le ty cond al vl a1 v1 a2 v2 a b,
+  select ty cond al a1 a2 = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  eval_expr ge sp e m le a1 v1 ->
+  eval_expr ge sp e m le a2 v2 ->
+  eval_condition cond vl m = Some b ->
+  exists v, 
+     eval_expr ge sp e m le a v
+  /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
+Proof.
+  unfold select; intros. 
+  destruct (select_supported ty); try discriminate.
+  destruct (select_swap cond); inv H.
+- exists (Val.select (Some (negb b)) v2 v1 ty); split.
+  apply eval_Eop with (v2 :: v1 :: vl).
+  constructor; auto. constructor; auto.
+  simpl. rewrite eval_negate_condition, H3; auto.
+  destruct b; auto.
+- exists (Val.select (Some b) v1 v2 ty); split.
+  apply eval_Eop with (v1 :: v2 :: vl).
+  constructor; auto. constructor; auto.
+  simpl. rewrite H3; auto.
+  auto.
+Qed.
+
 Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
 Proof.
   red; intros. unfold singleoffloat. TrivialExists.
diff --git a/x86/ValueAOp.v b/x86/ValueAOp.v
index 1021a9c8..d0b8427a 100644
--- a/x86/ValueAOp.v
+++ b/x86/ValueAOp.v
@@ -160,6 +160,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Olongofsingle, v1::nil => longofsingle v1
   | Osingleoflong, v1::nil => singleoflong v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
+  | Osel c ty, v1::v2::vl => select (eval_static_condition c vl) v1 v2
   | _, _ => Vbot
   end.
 
@@ -258,6 +259,7 @@ Proof.
   eapply eval_static_addressing_32_sound; eauto.
   eapply eval_static_addressing_64_sound; eauto.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
+  apply select_sound; auto. eapply eval_static_condition_sound; eauto.
 Qed.
 
 End SOUNDNESS.