Introduce and use the type fp_comparison for floating-point comparisons

With FP arithmetic, the negation of "x < y" is not "x >= y".  For this reason, the back-end intermediate languages of CompCert used to have both "Ccompf c" and "Cnotcompf c" comparison operators, where "c" is of type Integers.comparison and "Cnotcompf c" denotes the negation of FP comparison c.

There are some problems with this approach:
- Beyond Cnotcompf we also need Cnotcompfs (for single precision FP) and, in case of ARM, special forms for not-comparison against 0.0.  This duplication of comparison constructors inevitably causes some code and proof duplication.
- Cnotcompf Ceq is really Ccompf Cne, and likewise Cnotcompf Cne is really Ccompf Ceq, hence the representation of FP comparisons is not canonical, adding to the code and proof duplication mentioned above.
- Cnotcompf is introduced in CminorSel, but in Cminor we don't have it, making it impossible to express some transformations over comparisons at the machine-independent Cminor level.

This commit develops an alternate approach, whereas FP comparisons have their own type, defined as Floats.fp_comparison, and which includes constructors for "not <", "not <=", "not >" and "not >=".  Hence this type is closed under boolean negation, so to speak, and there is no longer a need for "Cnotcompf", given that "Ccompf" takes a fp_comparison and can therefore express all FP comparisons of interest.

1 files changed, 61 insertions, 58 deletions

diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v
index 904debdc..c638cdcf 100644
--- a/x86/Asmgenproof1.v
+++ b/x86/Asmgenproof1.v
@@ -700,8 +700,8 @@ 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 (Float.cmp Ceq n1 n2 || negb (Float.ordered n1 n2))
-  /\ rs'#CF = Val.of_bool (negb (Float.cmp Cge n1 n2))
+     rs'#ZF = Val.of_bool (Float.cmp FCeq n1 n2 || negb (Float.ordered n1 n2))
+  /\ rs'#CF = Val.of_bool (negb (Float.cmp FCge n1 n2))
   /\ rs'#PF = Val.of_bool (negb (Float.ordered n1 n2))
   /\ (forall r, data_preg r = true -> rs'#r = rs#r).
 Proof.
@@ -715,8 +715,8 @@ 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 (Float32.cmp Ceq n1 n2 || negb (Float32.ordered n1 n2))
-  /\ rs'#CF = Val.of_bool (negb (Float32.cmp Cge n1 n2))
+     rs'#ZF = Val.of_bool (Float32.cmp FCeq n1 n2 || negb (Float32.ordered n1 n2))
+  /\ rs'#CF = Val.of_bool (negb (Float32.cmp FCge n1 n2))
   /\ rs'#PF = Val.of_bool (negb (Float32.ordered n1 n2))
   /\ (forall r, data_preg r = true -> rs'#r = rs#r).
 Proof.
@@ -743,10 +743,10 @@ Definition eval_extcond (xc: extcond) (rs: regset) : option bool :=
       end
   end.
 
-Definition swap_floats {A: Type} (c: comparison) (n1 n2: A) : A :=
+Definition swap_floats {A: Type} (c: fp_comparison) (n1 n2: A) : A :=
   match c with
-  | Clt | Cle => n2
-  | Ceq | Cne | Cgt | Cge => n1
+  | FClt | FCle | FCnotlt | FCnotle => n2
+  | FCeq | FCne | FCgt | FCge | FCnotgt | FCnotge => n1
   end.
 
 Lemma testcond_for_float_comparison_correct:
@@ -778,38 +778,32 @@ Transparent Float.cmp Float.ordered.
  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:
-  forall c n1 n2 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.
-  generalize (compare_floats_spec rs (swap_floats c n1 n2) (swap_floats c n2 n1)).
-  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_extcond, eval_testcond. rewrite A; rewrite B; rewrite C.
-  destruct c; simpl.
-- (* 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.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.
+- (* notlt *)
+  replace (Float.cmp FCnotlt n1 n2) with (negb (Float.cmp FClt n1 n2)) by (symmetry; apply (Float.cmp_negate FClt)).
+  rewrite <- (Float.cmp_swap FCge n1 n2).
+  rewrite <- (Float.cmp_swap FCne n1 n2).
+  simpl.
+  rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq.
+  destruct (Float.cmp FClt n1 n2) eqn:LT; simpl.
+  destruct (Float.cmp FCeq n1 n2) eqn:EQ; simpl.
+  exfalso. eapply Float.cmp_lt_eq_false; eauto.
+  auto.
+  destruct (Float.cmp FCeq n1 n2); auto.
+- (* notle *)
+  replace (Float.cmp FCnotle n1 n2) with (negb (Float.cmp FCle n1 n2)) by (symmetry; apply (Float.cmp_negate FCle)).
+  rewrite <- (Float.cmp_swap FCge n1 n2). simpl.
+  destruct (Float.cmp FCle n1 n2); auto.
+- (* notgt *)
+  replace (Float.cmp FCnotgt n1 n2) with (negb (Float.cmp FCgt n1 n2)) by (symmetry; apply (Float.cmp_negate FCgt)).
+  rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq.
+  destruct (Float.cmp FCgt n1 n2) eqn:GT; simpl.
+  destruct (Float.cmp FCeq n1 n2) eqn:EQ; simpl.
+  exfalso. eapply Float.cmp_gt_eq_false; eauto.
+  auto.
+  destruct (Float.cmp FCeq n1 n2); auto.
+- (* notge *)
+  replace (Float.cmp FCnotge n1 n2) with (negb (Float.cmp FCge n1 n2)) by (symmetry; apply (Float.cmp_negate FCge)).
+  destruct (Float.cmp FCge n1 n2); auto.
 Opaque Float.cmp Float.ordered.
 Qed.
 
@@ -823,7 +817,7 @@ Proof.
   intros.
   generalize (compare_floats32_spec rs (swap_floats c n1 n2) (swap_floats c n2 n1)).
   set (rs' := nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2))
-                                        (Vsingle (swap_floats c n2 n1)) rs)).
+                                          (Vsingle (swap_floats c n2 n1)) rs)).
   intros [A [B [C D]]].
   unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C.
   destruct c; simpl.
@@ -874,9 +868,36 @@ Transparent Float32.cmp Float32.ordered.
  unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
 - (* ge *)
   destruct (Float32.cmp Cge n1 n2); auto.
+- (* notlt *)
+  replace (Float32.cmp FCnotlt n1 n2) with (negb (Float32.cmp FClt n1 n2)) by (symmetry; apply (Float32.cmp_negate FClt)).
+  rewrite <- (Float32.cmp_swap FCge n1 n2).
+  rewrite <- (Float32.cmp_swap FCne n1 n2).
+  simpl.
+  rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq.
+  destruct (Float32.cmp FClt n1 n2) eqn:LT; simpl.
+  destruct (Float32.cmp FCeq n1 n2) eqn:EQ; simpl.
+  exfalso. eapply Float32.cmp_lt_eq_false; eauto.
+  auto.
+  destruct (Float32.cmp FCeq n1 n2); auto.
+- (* notle *)
+  replace (Float32.cmp FCnotle n1 n2) with (negb (Float32.cmp FCle n1 n2)) by (symmetry; apply (Float32.cmp_negate FCle)).
+  rewrite <- (Float32.cmp_swap FCge n1 n2). simpl.
+  destruct (Float32.cmp FCle n1 n2); auto.
+- (* notgt *)
+  replace (Float32.cmp FCnotgt n1 n2) with (negb (Float32.cmp FCgt n1 n2)) by (symmetry; apply (Float32.cmp_negate FCgt)).
+  rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq.
+  destruct (Float32.cmp FCgt n1 n2) eqn:GT; simpl.
+  destruct (Float32.cmp FCeq n1 n2) eqn:EQ; simpl.
+  exfalso. eapply Float32.cmp_gt_eq_false; eauto.
+  auto.
+  destruct (Float32.cmp FCeq n1 n2); auto.
+- (* notge *)
+  replace (Float32.cmp FCnotge n1 n2) with (negb (Float32.cmp FCge n1 n2)) by (symmetry; apply (Float32.cmp_negate FCge)).
+  destruct (Float32.cmp FCge n1 n2); auto.
 Opaque Float32.cmp Float32.ordered.
 Qed.
 
+
 Remark swap_floats_commut:
   forall (A B: Type) c (f: A -> B) x y, swap_floats c (f x) (f y) = f (swap_floats c x y).
 Proof.
@@ -983,15 +1004,6 @@ Proof.
   split. destruct (rs x); destruct (rs x0); simpl; auto.
   repeat rewrite swap_floats_commut. apply testcond_for_float_comparison_correct.
   intros. Simplifs. apply compare_floats_inv; auto with asmgen.
-- (* notcompf *)
-  simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
-  exists (nextinstr (compare_floats (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)).
-  split. apply exec_straight_one.
-  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.
-  intros. Simplifs. apply compare_floats_inv; auto with asmgen.
 - (* compfs *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
   exists (nextinstr (compare_floats32 (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)).
@@ -1001,15 +1013,6 @@ Proof.
   split. destruct (rs x); destruct (rs x0); simpl; auto.
   repeat rewrite swap_floats_commut. apply testcond_for_float32_comparison_correct.
   intros. Simplifs. apply compare_floats32_inv; auto with asmgen.
-- (* notcompfs *)
-  simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
-  exists (nextinstr (compare_floats32 (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)).
-  split. apply exec_straight_one.
-  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.
-  intros. Simplifs. apply compare_floats32_inv; auto with asmgen.
 - (* maskzero *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
   econstructor. split. apply exec_straight_one. simpl; eauto. auto.