Implement a `Osel` operation for x86

The operation compiles down to conditional moves.

1 files changed, 143 insertions, 21 deletions

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. *)