x86: wrong modeling of ZF flag for FP comparisons

As written in the comment, ZF should be set if the two floats are
equal or unordered.  The "or unordered" case was missing in the
original modeling of FP comparisons.

- Set ZF flag correctly in the Asm.compare_floats and Asm.compare_floats32 functions.
- Update the proofs in Asmgenproof1 accordingly.

No change required to the code generated for FP comparisons: this code
already anticipated the "or unordered" case.

Problem reported by Alix Trieu.

2 files changed, 66 insertions, 130 deletions

diff --git a/x86/Asm.v b/x86/Asm.v
index dfa2a88a..32235c2d 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -442,8 +442,8 @@ Definition compare_longs (x y: val) (rs: regset) (m: mem): regset :=
      #PF  <- Vundef.
 
 (** Floating-point comparison between x and y:
--       ZF = 1 if x=y or unordered, 0 if x<>y
--       CF = 1 if x<y or unordered, 0 if x>=y
+-       ZF = 1 if x=y or unordered, 0 if x<>y and ordered
+-       CF = 1 if x<y or unordered, 0 if x>=y.
 -       PF = 1 if unordered, 0 if ordered.
 -       SF and 0F are undefined
 *)
@@ -451,9 +451,9 @@ Definition compare_longs (x y: val) (rs: regset) (m: mem): regset :=
 Definition compare_floats (vx vy: val) (rs: regset) : regset :=
   match vx, vy with
   | Vfloat x, Vfloat y =>
-      rs #ZF  <- (Val.of_bool (negb (Float.cmp Cne x y)))
+      rs #ZF  <- (Val.of_bool (Float.cmp Ceq x y || negb (Float.ordered x y)))
          #CF  <- (Val.of_bool (negb (Float.cmp Cge x y)))
-         #PF  <- (Val.of_bool (negb (Float.cmp Ceq x y || Float.cmp Clt x y || Float.cmp Cgt x y)))
+         #PF  <- (Val.of_bool (negb (Float.ordered x y)))
          #SF  <- Vundef
          #OF  <- Vundef
   | _, _ =>
@@ -463,9 +463,9 @@ Definition compare_floats (vx vy: val) (rs: regset) : regset :=
 Definition compare_floats32 (vx vy: val) (rs: regset) : regset :=
   match vx, vy with
   | Vsingle x, Vsingle y =>
-      rs #ZF  <- (Val.of_bool (negb (Float32.cmp Cne x y)))
+      rs #ZF  <- (Val.of_bool (Float32.cmp Ceq x y || negb (Float32.ordered x y)))
          #CF  <- (Val.of_bool (negb (Float32.cmp Cge x y)))
-         #PF  <- (Val.of_bool (negb (Float32.cmp Ceq x y || Float32.cmp Clt x y || Float32.cmp Cgt x y)))
+         #PF  <- (Val.of_bool (negb (Float32.ordered x y)))
          #SF  <- Vundef
          #OF  <- Vundef
   | _, _ =>
diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v
index c5b03426..904debdc 100644
--- a/x86/Asmgenproof1.v
+++ b/x86/Asmgenproof1.v
@@ -700,9 +700,9 @@ Qed.
 Lemma compare_floats_spec:
   forall rs n1 n2,
   let rs' := nextinstr (compare_floats (Vfloat n1) (Vfloat n2) rs) in
-     rs'#ZF = Val.of_bool (negb (Float.cmp Cne n1 n2))
+     rs'#ZF = Val.of_bool (Float.cmp Ceq n1 n2 || negb (Float.ordered n1 n2))
   /\ rs'#CF = Val.of_bool (negb (Float.cmp Cge n1 n2))
-  /\ rs'#PF = Val.of_bool (negb (Float.cmp Ceq n1 n2 || Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2))
+  /\ rs'#PF = Val.of_bool (negb (Float.ordered n1 n2))
   /\ (forall r, data_preg r = true -> rs'#r = rs#r).
 Proof.
   intros. unfold rs'; unfold compare_floats.
@@ -715,9 +715,9 @@ Qed.
 Lemma compare_floats32_spec:
   forall rs n1 n2,
   let rs' := nextinstr (compare_floats32 (Vsingle n1) (Vsingle n2) rs) in
-     rs'#ZF = Val.of_bool (negb (Float32.cmp Cne n1 n2))
+     rs'#ZF = Val.of_bool (Float32.cmp Ceq n1 n2 || negb (Float32.ordered n1 n2))
   /\ rs'#CF = Val.of_bool (negb (Float32.cmp Cge n1 n2))
-  /\ rs'#PF = Val.of_bool (negb (Float32.cmp Ceq n1 n2 || Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2))
+  /\ rs'#PF = Val.of_bool (negb (Float32.ordered n1 n2))
   /\ (forall r, data_preg r = true -> rs'#r = rs#r).
 Proof.
   intros. unfold rs'; unfold compare_floats32.
@@ -763,38 +763,22 @@ Proof.
   intros [A [B [C D]]].
   unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C.
   destruct c; simpl.
-(* eq *)
-  rewrite Float.cmp_ne_eq.
-  caseEq (Float.cmp Ceq n1 n2); intros.
-  auto.
-  simpl. destruct (Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2); auto.
-(* ne *)
-  rewrite Float.cmp_ne_eq.
-  caseEq (Float.cmp Ceq n1 n2); intros.
-  auto.
-  simpl. destruct (Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2); auto.
-(* lt *)
-  rewrite <- (Float.cmp_swap Cge n1 n2).
-  rewrite <- (Float.cmp_swap Cne n1 n2).
-  simpl.
-  rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq.
-  caseEq (Float.cmp Clt n1 n2); intros; simpl.
-  caseEq (Float.cmp Ceq n1 n2); intros; simpl.
-  elimtype False. eapply Float.cmp_lt_eq_false; eauto.
-  auto.
-  destruct (Float.cmp Ceq n1 n2); auto.
-(* le *)
+- (* eq *)
+Transparent Float.cmp Float.ordered.
+  unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
+- (* ne *)
+  unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
+- (* lt *)
+  rewrite <- (Float.cmp_swap Clt n2 n1). simpl. unfold Float.ordered. 
+  destruct (Float.compare n2 n1) as [[]|]; reflexivity.
+- (* le *)
   rewrite <- (Float.cmp_swap Cge n1 n2). simpl.
-  destruct (Float.cmp Cle n1 n2); auto.
-(* gt *)
-  rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq.
-  caseEq (Float.cmp Cgt n1 n2); intros; simpl.
-  caseEq (Float.cmp Ceq n1 n2); intros; simpl.
-  elimtype False. eapply Float.cmp_gt_eq_false; eauto.
-  auto.
-  destruct (Float.cmp Ceq n1 n2); auto.
-(* ge *)
+  destruct (Float.compare n1 n2) as [[]|]; auto.
+- (* gt *)
+ unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
+- (* ge *)
   destruct (Float.cmp Cge n1 n2); auto.
+Opaque Float.cmp Float.ordered.
 Qed.
 
 Lemma testcond_for_neg_float_comparison_correct:
@@ -811,38 +795,22 @@ Proof.
   intros [A [B [C D]]].
   unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C.
   destruct c; simpl.
-(* eq *)
-  rewrite Float.cmp_ne_eq.
-  caseEq (Float.cmp Ceq n1 n2); intros.
-  auto.
-  simpl. destruct (Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2); auto.
-(* ne *)
-  rewrite Float.cmp_ne_eq.
-  caseEq (Float.cmp Ceq n1 n2); intros.
-  auto.
-  simpl. destruct (Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2); auto.
-(* lt *)
-  rewrite <- (Float.cmp_swap Cge n1 n2).
-  rewrite <- (Float.cmp_swap Cne n1 n2).
-  simpl.
-  rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq.
-  caseEq (Float.cmp Clt n1 n2); intros; simpl.
-  caseEq (Float.cmp Ceq n1 n2); intros; simpl.
-  elimtype False. eapply Float.cmp_lt_eq_false; eauto.
-  auto.
-  destruct (Float.cmp Ceq n1 n2); auto.
-(* le *)
+- (* eq *)
+Transparent Float.cmp Float.ordered.
+  unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
+- (* ne *)
+  unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
+- (* lt *)
+  rewrite <- (Float.cmp_swap Clt n2 n1). simpl. unfold Float.ordered. 
+  destruct (Float.compare n2 n1) as [[]|]; reflexivity.
+- (* le *)
   rewrite <- (Float.cmp_swap Cge n1 n2). simpl.
-  destruct (Float.cmp Cle n1 n2); auto.
-(* gt *)
-  rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq.
-  caseEq (Float.cmp Cgt n1 n2); intros; simpl.
-  caseEq (Float.cmp Ceq n1 n2); intros; simpl.
-  elimtype False. eapply Float.cmp_gt_eq_false; eauto.
-  auto.
-  destruct (Float.cmp Ceq n1 n2); auto.
-(* ge *)
+  destruct (Float.compare n1 n2) as [[]|]; auto.
+- (* gt *)
+ unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
+- (* ge *)
   destruct (Float.cmp Cge n1 n2); auto.
+Opaque Float.cmp Float.ordered.
 Qed.
 
 Lemma testcond_for_float32_comparison_correct:
@@ -859,38 +827,22 @@ Proof.
   intros [A [B [C D]]].
   unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C.
   destruct c; simpl.
-(* eq *)
-  rewrite Float32.cmp_ne_eq.
-  caseEq (Float32.cmp Ceq n1 n2); intros.
-  auto.
-  simpl. destruct (Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2); auto.
-(* ne *)
-  rewrite Float32.cmp_ne_eq.
-  caseEq (Float32.cmp Ceq n1 n2); intros.
-  auto.
-  simpl. destruct (Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2); auto.
-(* lt *)
-  rewrite <- (Float32.cmp_swap Cge n1 n2).
-  rewrite <- (Float32.cmp_swap Cne n1 n2).
-  simpl.
-  rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq.
-  caseEq (Float32.cmp Clt n1 n2); intros; simpl.
-  caseEq (Float32.cmp Ceq n1 n2); intros; simpl.
-  elimtype False. eapply Float32.cmp_lt_eq_false; eauto.
-  auto.
-  destruct (Float32.cmp Ceq n1 n2); auto.
-(* le *)
+- (* eq *)
+Transparent Float32.cmp Float32.ordered.
+  unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
+- (* ne *)
+  unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
+- (* lt *)
+  rewrite <- (Float32.cmp_swap Clt n2 n1). simpl. unfold Float32.ordered. 
+  destruct (Float32.compare n2 n1) as [[]|]; reflexivity.
+- (* le *)
   rewrite <- (Float32.cmp_swap Cge n1 n2). simpl.
-  destruct (Float32.cmp Cle n1 n2); auto.
-(* gt *)
-  rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq.
-  caseEq (Float32.cmp Cgt n1 n2); intros; simpl.
-  caseEq (Float32.cmp Ceq n1 n2); intros; simpl.
-  elimtype False. eapply Float32.cmp_gt_eq_false; eauto.
-  auto.
-  destruct (Float32.cmp Ceq n1 n2); auto.
-(* ge *)
+  destruct (Float32.compare n1 n2) as [[]|]; auto.
+- (* gt *)
+ unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
+- (* ge *)
   destruct (Float32.cmp Cge n1 n2); auto.
+Opaque Float32.cmp Float32.ordered.
 Qed.
 
 Lemma testcond_for_neg_float32_comparison_correct:
@@ -907,38 +859,22 @@ Proof.
   intros [A [B [C D]]].
   unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C.
   destruct c; simpl.
-(* eq *)
-  rewrite Float32.cmp_ne_eq.
-  caseEq (Float32.cmp Ceq n1 n2); intros.
-  auto.
-  simpl. destruct (Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2); auto.
-(* ne *)
-  rewrite Float32.cmp_ne_eq.
-  caseEq (Float32.cmp Ceq n1 n2); intros.
-  auto.
-  simpl. destruct (Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2); auto.
-(* lt *)
-  rewrite <- (Float32.cmp_swap Cge n1 n2).
-  rewrite <- (Float32.cmp_swap Cne n1 n2).
-  simpl.
-  rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq.
-  caseEq (Float32.cmp Clt n1 n2); intros; simpl.
-  caseEq (Float32.cmp Ceq n1 n2); intros; simpl.
-  elimtype False. eapply Float32.cmp_lt_eq_false; eauto.
-  auto.
-  destruct (Float32.cmp Ceq n1 n2); auto.
-(* le *)
+- (* eq *)
+Transparent Float32.cmp Float32.ordered.
+  unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
+- (* ne *)
+  unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
+- (* lt *)
+  rewrite <- (Float32.cmp_swap Clt n2 n1). simpl. unfold Float32.ordered. 
+  destruct (Float32.compare n2 n1) as [[]|]; reflexivity.
+- (* le *)
   rewrite <- (Float32.cmp_swap Cge n1 n2). simpl.
-  destruct (Float32.cmp Cle n1 n2); auto.
-(* gt *)
-  rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq.
-  caseEq (Float32.cmp Cgt n1 n2); intros; simpl.
-  caseEq (Float32.cmp Ceq n1 n2); intros; simpl.
-  elimtype False. eapply Float32.cmp_gt_eq_false; eauto.
-  auto.
-  destruct (Float32.cmp Ceq n1 n2); auto.
-(* ge *)
+  destruct (Float32.compare n1 n2) as [[]|]; auto.
+- (* gt *)
+ unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
+- (* ge *)
   destruct (Float32.cmp Cge n1 n2); auto.
+Opaque Float32.cmp Float32.ordered.
 Qed.
 
 Remark swap_floats_commut: