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, 14 insertions, 13 deletions

diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 8c296f0a..37bef464 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -213,11 +213,11 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) :
   synthesized by a [cror] instruction that computes the logical ``or''
   of the corresponding two conditions. *)
 
-Definition floatcomp (cmp: comparison) (r1 r2: freg) (k: code) :=
+Definition floatcomp (cmp: fp_comparison) (r1 r2: freg) (k: code) :=
   Pfcmpu r1 r2 ::
   match cmp with
-  | Cle => Pcror CRbit_3 CRbit_2 CRbit_0 :: k
-  | Cge => Pcror CRbit_3 CRbit_2 CRbit_1 :: k
+  | FCle | FCnotle => Pcror CRbit_3 CRbit_2 CRbit_0 :: k
+  | FCge | FCnotge => Pcror CRbit_3 CRbit_2 CRbit_1 :: k
   | _ => k
   end.
 
@@ -247,8 +247,6 @@ Definition transl_cond
         OK (loadimm GPR0 n (Pcmplw r1 GPR0 :: k))
   | Ccompf cmp, a1 :: a2 :: nil =>
       do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 k)
-  | Cnotcompf cmp, a1 :: a2 :: nil =>
-      do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 k)
   | Cmaskzero n, a1 :: nil =>
       do r1 <- ireg_of a1; OK (andimm_base GPR0 r1 n k)
   | Cmasknotzero n, a1 :: nil =>
@@ -292,14 +290,18 @@ Definition crbit_for_icmp (cmp: comparison) :=
   | Cge => (CRbit_0, false)
   end.
 
-Definition crbit_for_fcmp (cmp: comparison) :=
+Definition crbit_for_fcmp (cmp: fp_comparison) :=
   match cmp with
-  | Ceq => (CRbit_2, true)
-  | Cne => (CRbit_2, false)
-  | Clt => (CRbit_0, true)
-  | Cle => (CRbit_3, true)
-  | Cgt => (CRbit_1, true)
-  | Cge => (CRbit_3, true)
+  | FCeq => (CRbit_2, true)
+  | FCne => (CRbit_2, false)
+  | FClt => (CRbit_0, true)
+  | FCle => (CRbit_3, true)
+  | FCgt => (CRbit_1, true)
+  | FCge => (CRbit_3, true)
+  | FCnotlt => (CRbit_0, false)
+  | FCnotle => (CRbit_3, false)
+  | FCnotgt => (CRbit_1, false)
+  | FCnotge => (CRbit_3, false)
   end.
 
 Definition crbit_for_cond (cond: condition) :=
@@ -309,7 +311,6 @@ Definition crbit_for_cond (cond: condition) :=
   | Ccompimm cmp n => crbit_for_icmp cmp
   | Ccompuimm cmp n => crbit_for_icmp cmp
   | Ccompf cmp => crbit_for_fcmp cmp
-  | Cnotcompf cmp => let p := crbit_for_fcmp cmp in (fst p, negb (snd p))
   | Cmaskzero n => (CRbit_2, true)
   | Cmasknotzero n => (CRbit_2, false)
   | Ccompl cmp => crbit_for_icmp cmp