Merge of branch seq-and-or. See Changelog for details.

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

3 files changed, 133 insertions, 119 deletions

diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 9664be8..a36adb1 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -399,8 +399,8 @@ let print_builtin_vstore_common oc chunk addr src tmp =
   | Mint32, IR src ->
       fprintf oc "	movl	%a, %a\n" ireg src addressing addr
   | Mfloat32, FR src ->
-      fprintf oc "      cvtsd2ss %a, %%xmm7\n" freg src;
-      fprintf oc "      movss   %%xmm7, %a\n" addressing addr
+      fprintf oc "	cvtsd2ss %a, %%xmm7\n" freg src;
+      fprintf oc "	movss	%%xmm7, %a\n" addressing addr
   | (Mfloat64 | Mfloat64al32), FR src ->
       fprintf oc "	movsd	%a, %a\n" freg src addressing addr
   | _ ->
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 6d44cf5..7bb2bee 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -74,36 +74,6 @@ Definition addrstack (ofs: int) :=
 
 Definition notint (e: expr) := Eop (Oxorimm Int.mone) (e ::: Enil).
 
-(** ** Boolean value and boolean negation *)
-
-Fixpoint boolval (e: expr) {struct e} : expr :=
-  let default := Eop (Ocmp (Ccompuimm Cne Int.zero)) (e ::: Enil) in
-  match e with 
-  | Eop (Ointconst n) Enil =>
-      Eop (Ointconst (if Int.eq n Int.zero then Int.zero else Int.one)) Enil
-  | Eop (Ocmp cond) args =>
-      Eop (Ocmp cond) args
-  | Econdition e1 e2 e3 =>
-      Econdition e1 (boolval e2) (boolval e3)
-  | _ =>
-      default
-  end.
-
-(** ** Boolean negation *)
-
-Fixpoint notbool (e: expr) {struct e} : expr :=
-  let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in
-  match e with 
-  | Eop (Ointconst n) Enil =>
-      Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil
-  | Eop (Ocmp cond) args =>
-      Eop (Ocmp (negate_condition cond)) args
-  | Econdition e1 e2 e3 =>
-      Econdition e1 (notbool e2) (notbool e3)
-  | _ =>
-      default
-  end.
-
 (** ** Integer addition and pointer addition *)
 
 Definition offset_addressing (a: addressing) (ofs: int) : addressing :=
@@ -368,12 +338,46 @@ Definition divf (e1 e2: expr) :=  Eop Odivf (e1 ::: e2 ::: Enil).
 
 (** ** Comparisons *)
 
+Nondetfunction compimm (default: comparison -> int -> condition)
+                       (sem: comparison -> int -> int -> bool)
+                       (c: comparison) (e1: expr) (n2: int) :=
+  match c, e1 with
+  | c, Eop (Ointconst n1) Enil =>
+      Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil
+  | Ceq, Eop (Ocmp c) el =>
+      if Int.eq_dec n2 Int.zero then
+        Eop (Ocmp (negate_condition c)) el
+      else if Int.eq_dec n2 Int.one then
+        Eop (Ocmp c) el
+      else 
+        Eop (Ointconst Int.zero) Enil
+  | Cne, Eop (Ocmp c) el =>
+      if Int.eq_dec n2 Int.zero then
+        Eop (Ocmp c) el
+      else if Int.eq_dec n2 Int.one then
+        Eop (Ocmp (negate_condition c)) el
+      else 
+        Eop (Ointconst Int.one) Enil
+  | Ceq, Eop (Oandimm n1) (t1 ::: Enil) =>
+      if Int.eq_dec n2 Int.zero then
+        Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil)
+      else
+        Eop (Ocmp (default c n2)) (e1 ::: Enil)
+  | Cne, Eop (Oandimm n1) (t1 ::: Enil) =>
+      if Int.eq_dec n2 Int.zero then
+        Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil)
+      else
+        Eop (Ocmp (default c n2)) (e1 ::: Enil)
+  | _, _ =>
+       Eop (Ocmp (default c n2)) (e1 ::: Enil)
+  end.
+
 Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 =>
-      Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2 ::: Enil)
+      compimm Ccompimm Int.cmp (swap_comparison c) t2 n1
   | t1, Eop (Ointconst n2) Enil =>
-      Eop (Ocmp (Ccompimm c n2)) (t1 ::: Enil)
+      compimm Ccompimm Int.cmp c t1 n2
   | _, _ =>
       Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil)
   end.
@@ -381,9 +385,9 @@ Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
 Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 =>
-      Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2 ::: Enil)
+      compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1
   | t1, Eop (Ointconst n2) Enil =>
-      Eop (Ocmp (Ccompuimm c n2)) (t1 ::: Enil)
+      compimm Ccompuimm Int.cmpu c t1 n2
   | _, _ =>
       Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil)
   end.
@@ -420,17 +424,16 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
 Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil).
 
 Definition intuoffloat (e: expr) :=
-  let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in
   Elet e
     (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil)
-      (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
+      (Econdition (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)
         (intoffloat (Eletvar 1))
         (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
 
 Definition floatofintu (e: expr) :=
   let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in
   Elet e
-    (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
+    (Econdition (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)
       (floatofint (Eletvar O))
       (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)).
 
@@ -442,10 +445,3 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | _ => (Aindexed Int.zero, e:::Enil)
   end.
 
-(** ** Turning an expression into a condition *)
-
-Nondetfunction cond_of_expr (e: expr) :=
-  match e with
-  | Eop (Oandimm n) (t1:::Enil) => (Cmasknotzero n, t1:::Enil)
-  | _ => (Ccompuimm Cne Int.zero, e:::Enil)
-  end.
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 27d8574..f88f9c0 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -143,53 +143,6 @@ Proof.
   unfold notint; red; intros. TrivialExists. 
 Qed.
 
-Theorem eval_boolval: unary_constructor_sound boolval Val.boolval.
-Proof.
-  assert (DFL: 
-    forall le a x,
-    eval_expr ge sp e m le a x ->
-     exists v, eval_expr ge sp e m le (Eop (Ocmp (Ccompuimm Cne Int.zero)) (a ::: Enil)) v
-           /\ Val.lessdef (Val.boolval x) v).
-  intros. TrivialExists. simpl. destruct x; simpl; auto.
-
-  red. induction a; simpl; intros; eauto. destruct o; eauto.
-(* intconst *)
-  destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto.
-(* cmp *)
-  inv H. simpl in H5.
-  destruct (eval_condition c vl m) as []_eqn. 
-  TrivialExists. simpl. inv H5. rewrite Heqo. destruct b; auto.
-  simpl in H5. inv H5. 
-  exists Vundef; split; auto. EvalOp; simpl. rewrite Heqo; auto.
-
-(* condition *)
-  inv H. destruct v1.
-  exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
-  exploit IHa2; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
-Qed.
-
-Theorem eval_notbool: unary_constructor_sound notbool Val.notbool.
-Proof.
-  assert (DFL: 
-    forall le a x,
-    eval_expr ge sp e m le a x ->
-     exists v, eval_expr ge sp e m le (Eop (Ocmp (Ccompuimm Ceq Int.zero)) (a ::: Enil)) v
-           /\ Val.lessdef (Val.notbool x) v).
-  intros. TrivialExists. simpl. destruct x; simpl; auto.
-
-  red. induction a; simpl; intros; eauto. destruct o; eauto.
-(* intconst *)
-  destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto.
-(* cmp *)
-  inv H. simpl in H5. inv H5.
-  TrivialExists. simpl. rewrite eval_negate_condition. 
-  destruct (eval_condition c vl m); auto. destruct b; auto. 
-(* condition *)
-  inv H. destruct v1.
-  exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
-  exploit IHa2; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
-Qed.
-
 Lemma shift_symbol_address:
   forall id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n).
 Proof.
@@ -604,12 +557,94 @@ Proof.
   red; intros; TrivialExists.
 Qed.
 
+Section COMP_IMM.
+
+Variable default: comparison -> int -> condition.
+Variable intsem: comparison -> int -> int -> bool.
+Variable sem: comparison -> val -> val -> val.
+
+Hypothesis sem_int: forall c x y, sem c (Vint x) (Vint y) = Val.of_bool (intsem c x y).
+Hypothesis sem_undef: forall c v, sem c Vundef v = Vundef.
+Hypothesis sem_eq: forall x y, sem Ceq (Vint x) (Vint y) = Val.of_bool (Int.eq x y).
+Hypothesis sem_ne: forall x y, sem Cne (Vint x) (Vint y) = Val.of_bool (negb (Int.eq x y)).
+Hypothesis sem_default: forall c v n, sem c v (Vint n) = Val.of_optbool (eval_condition (default c n) (v :: nil) m).
+
+Lemma eval_compimm:
+  forall le c a n2 x,
+  eval_expr ge sp e m le a x ->
+  exists v, eval_expr ge sp e m le (compimm default intsem c a n2) v
+         /\ Val.lessdef (sem c x (Vint n2)) v.
+Proof.
+  intros until x.
+  unfold compimm; case (compimm_match c a); intros.
+(* constant *)
+  InvEval. rewrite sem_int. TrivialExists. simpl. destruct (intsem c0 n1 n2); auto.
+(* eq cmp *)
+  InvEval. inv H. simpl in H5. inv H5. 
+  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. 
+  simpl. rewrite eval_negate_condition.
+  destruct (eval_condition c0 vl m); simpl.
+  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
+  rewrite sem_undef; auto.
+  destruct (Int.eq_dec n2 Int.one). subst n2. TrivialExists.
+  simpl. destruct (eval_condition c0 vl m); simpl.
+  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
+  rewrite sem_undef; auto.
+  exists (Vint Int.zero); split. EvalOp. 
+  destruct (eval_condition c0 vl m); simpl.
+  unfold Vtrue, Vfalse. destruct b; rewrite sem_eq; rewrite Int.eq_false; auto.
+  rewrite sem_undef; auto.
+(* ne cmp *)
+  InvEval. inv H. simpl in H5. inv H5. 
+  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. 
+  simpl. destruct (eval_condition c0 vl m); simpl.
+  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
+  rewrite sem_undef; auto.
+  destruct (Int.eq_dec n2 Int.one). subst n2. TrivialExists.
+  simpl. rewrite eval_negate_condition. destruct (eval_condition c0 vl m); simpl.
+  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
+  rewrite sem_undef; auto.
+  exists (Vint Int.one); split. EvalOp. 
+  destruct (eval_condition c0 vl m); simpl.
+  unfold Vtrue, Vfalse. destruct b; rewrite sem_ne; rewrite Int.eq_false; auto.
+  rewrite sem_undef; auto.
+(* eq andimm *)
+  destruct (Int.eq_dec n2 Int.zero). InvEval; subst.
+  econstructor; split. EvalOp. simpl; eauto. 
+  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_eq. 
+  destruct (Int.eq (Int.and i n1) Int.zero); auto. 
+  TrivialExists. simpl. rewrite sem_default. auto.
+(* ne andimm *)
+  destruct (Int.eq_dec n2 Int.zero). InvEval; subst.
+  econstructor; split. EvalOp. simpl; eauto. 
+  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_ne. 
+  destruct (Int.eq (Int.and i n1) Int.zero); auto. 
+  TrivialExists. simpl. rewrite sem_default. auto.
+(* default *)
+  TrivialExists. simpl. rewrite sem_default. auto.
+Qed.
+
+Hypothesis sem_swap:
+  forall c x y, sem (swap_comparison c) x y = sem c y x.
+
+Lemma eval_compimm_swap:
+  forall le c a n2 x,
+  eval_expr ge sp e m le a x ->
+  exists v, eval_expr ge sp e m le (compimm default intsem (swap_comparison c) a n2) v
+         /\ Val.lessdef (sem c (Vint n2) x) v.
+Proof.
+  intros. rewrite <- sem_swap. eapply eval_compimm; eauto. 
+Qed.
+
+End COMP_IMM.
+
 Theorem eval_comp:
   forall c, binary_constructor_sound (comp c) (Val.cmp c).
 Proof.
   intros; red; intros until y. unfold comp; case (comp_match a b); intros; InvEval.
-  TrivialExists. simpl. rewrite Val.swap_cmp_bool. auto.
-  TrivialExists.
+  eapply eval_compimm_swap; eauto. 
+  intros. unfold Val.cmp. rewrite Val.swap_cmp_bool; auto.
+  eapply eval_compimm; eauto. 
   TrivialExists.
 Qed.
 
@@ -617,8 +652,9 @@ Theorem eval_compu:
   forall c, binary_constructor_sound (compu c) (Val.cmpu (Mem.valid_pointer m) c).
 Proof.
   intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval.
-  TrivialExists. simpl. rewrite Val.swap_cmpu_bool. auto.
-  TrivialExists.
+  eapply eval_compimm_swap; eauto. 
+  intros. unfold Val.cmpu. rewrite Val.swap_cmpu_bool; auto.
+  eapply eval_compimm; eauto. 
   TrivialExists.
 Qed.
 
@@ -628,7 +664,6 @@ Proof.
   intros; red; intros. unfold compf. TrivialExists.
 Qed.
 
-
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
 Proof.
   red; intros. unfold cast8signed. TrivialExists.
@@ -695,8 +730,8 @@ Proof.
     constructor. auto.
   econstructor. eauto.
   econstructor. instantiate (1 := Vfloat fm). EvalOp. 
-  apply eval_Econdition with (v1 := Float.cmp Clt f fm).
-  econstructor. eauto with evalexpr. auto.
+  eapply eval_Econdition with (vb := Float.cmp Clt f fm).
+  eauto with evalexpr. auto.
   destruct (Float.cmp Clt f fm) as []_eqn.
   exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ.
   EvalOp. simpl. rewrite EQ; auto.
@@ -728,8 +763,8 @@ Proof.
   set (fm := Float.floatofintu Float.ox8000_0000).
   assert (eval_expr ge sp e m (Vint i :: le) (Eletvar O) (Vint i)).
     constructor. auto. 
-  apply eval_Econdition with (v1 := Int.ltu i Float.ox8000_0000).
-  econstructor. constructor. eauto. constructor.
+  eapply eval_Econdition with (vb := Int.ltu i Float.ox8000_0000).
+  constructor. eauto. constructor.
   simpl. auto.
   destruct (Int.ltu i Float.ox8000_0000) as []_eqn.
   rewrite Float.floatofintu_floatofint_1; auto.
@@ -758,21 +793,4 @@ Proof.
   exists (v :: nil); split. constructor; auto. constructor. subst; simpl. rewrite Int.add_zero; auto. 
 Qed.
 
-Theorem eval_cond_of_expr:
-  forall le a v b,
-  eval_expr ge sp e m le a v ->
-  Val.bool_of_val v b ->
-  match cond_of_expr a with (cond, args) =>
-    exists vl,
-    eval_exprlist ge sp e m le args vl /\
-    eval_condition cond vl m = Some b
-  end.
-Proof.
-  intros until v. unfold cond_of_expr; case (cond_of_expr_match a); intros; InvEval.
-  subst v. exists (v1 :: nil); split; auto with evalexpr.
-  simpl. destruct v1; unfold Val.and in H0; inv H0; auto.
-  exists (v :: nil); split; auto with evalexpr.
-  simpl. inv H0; auto.
-Qed.
-
 End CMCONSTR.