Treat negated float comparisons more directly

Changes

@@ -98,6 +98,9 @@ Working version
   simpler IT blocks instead
   (Xavier Leroy, review by Mark Shinwell)
 
+- GPR#1487: Treat negated float comparisons more directly
+  (Leo White, review by Xavier Leroy)
+
 ### Runtime system:
 
 - MPR#6411, GPR#1535: don't compile everything with -static-libgcc on mingw32,

asmcomp/amd64/emit.mlp

@@ -385,7 +385,7 @@ let output_test_zero arg =
 
 (* Output a floating-point compare and branch *)
 
-let emit_float_test cmp neg i lbl =
+let emit_float_test cmp i lbl =
   (* Effect of comisd on flags and conditional branches:
                      ZF PF CF  cond. branches taken
         unordered     1  1  1  je, jb, jbe, jp
@@ -395,33 +395,41 @@ let emit_float_test cmp neg i lbl =
      If FP traps are on (they are off by default),
      comisd traps on QNaN and SNaN but ucomisd traps on SNaN only.
   *)
-  match (cmp, neg) with
-  | (Ceq, false) | (Cne, true) ->
+  match cmp with
+  | CFeq ->
       let next = new_label() in
       I.ucomisd (arg i 1) (arg i 0);
       I.jp (label next);          (* skip if unordered *)
       I.je lbl;                   (* branch taken if x=y *)
       def_label next
-  | (Cne, false) | (Ceq, true) ->
+  | CFneq ->
       I.ucomisd (arg i 1) (arg i 0);
       I.jp lbl;                   (* branch taken if unordered *)
       I.jne lbl                   (* branch taken if x<y or x>y *)
-  | (Clt, _) ->
+  | CFlt ->
       I.comisd (arg i 0) (arg i 1);
-      if not neg then I.ja lbl    (* branch taken if y>x i.e. x<y *)
-      else            I.jbe lbl   (* taken if unordered or y<=x i.e. !(x<y) *)
-  | (Cle, _) ->
+      I.ja lbl                    (* branch taken if y>x i.e. x<y *)
+  | CFnlt ->
+      I.comisd (arg i 0) (arg i 1);
+      I.jbe lbl                   (* taken if unordered or y<=x i.e. !(x<y) *)
+  | CFle ->
+      I.comisd (arg i 0) (arg i 1);(* swap compare *)
+      I.jae lbl                    (* branch taken if y>=x i.e. x<=y *)
+  | CFnle ->
       I.comisd (arg i 0) (arg i 1);(* swap compare *)
-      if not neg then I.jae lbl   (* branch taken if y>=x i.e. x<=y *)
-      else            I.jb lbl    (* taken if unordered or y<x i.e. !(x<=y) *)
-  | (Cgt, _) ->
+      I.jb lbl                     (* taken if unordered or y<x i.e. !(x<=y) *)
+  | CFgt ->
       I.comisd (arg i 1) (arg i 0);
-      if not neg then I.ja lbl    (* branch taken if x>y *)
-      else            I.jbe lbl   (* taken if unordered or x<=y i.e. !(x>y) *)
-  | (Cge, _) ->
+      I.ja lbl                     (* branch taken if x>y *)
+  | CFngt ->
+      I.comisd (arg i 1) (arg i 0);
+      I.jbe lbl                    (* taken if unordered or x<=y i.e. !(x>y) *)
+  | CFge ->
+      I.comisd (arg i 1) (arg i 0);(* swap compare *)
+      I.jae lbl                    (* branch taken if x>=y *)
+  | CFnge ->
       I.comisd (arg i 1) (arg i 0);(* swap compare *)
-      if not neg then I.jae lbl   (* branch taken if x>=y *)
-      else            I.jb lbl    (* taken if unordered or x<y i.e. !(x>=y) *)
+      I.jb lbl                     (* taken if unordered or x<y i.e. !(x>=y) *)
 
 (* Deallocate the stack frame before a return or tail call *)
 
@@ -770,8 +778,8 @@ let emit_instr fallthrough i =
       | Iinttest_imm(cmp, n) ->
           I.cmp (int n) (arg i 0);
           I.j (cond cmp) lbl
-      | Ifloattest(cmp, neg) ->
-          emit_float_test cmp neg i lbl
+      | Ifloattest cmp ->
+          emit_float_test cmp i lbl
       | Ioddtest ->
           I.test (int 1) (arg8 i 0);
           I.jne lbl

asmcomp/amd64/reload.ml

@@ -107,13 +107,13 @@ method! reload_test tst arg =
       if stackp arg.(0) && stackp arg.(1)
       then [| self#makereg arg.(0); arg.(1) |]
       else arg
-  | Ifloattest((Clt|Cle), _) ->
+  | Ifloattest (CFlt | CFnlt | CFle | CFnle) ->
       (* Cf. emit.mlp: we swap arguments in this case *)
       (* First argument can be on stack, second must be in register *)
       if stackp arg.(1)
       then [| arg.(0); self#makereg arg.(1) |]
       else arg
-  | Ifloattest((Ceq|Cne|Cgt|Cge), _) ->
+  | Ifloattest (CFeq | CFneq | CFgt | CFngt | CFge | CFnge) ->
       (* Second argument can be on stack, first must be in register *)
       if stackp arg.(0)
       then [| self#makereg arg.(0); arg.(1) |]

asmcomp/arm/emit.mlp

@@ -165,8 +165,8 @@ let emit_call_bound_error bd =
 (* Negate a comparison *)
 
 let negate_integer_comparison = function
-    Isigned cmp   -> Isigned(negate_comparison cmp)
-  | Iunsigned cmp -> Iunsigned(negate_comparison cmp)
+  | Isigned cmp   -> Isigned(negate_integer_comparison cmp)
+  | Iunsigned cmp -> Iunsigned(negate_integer_comparison cmp)
 
 (* Names of various instructions *)
 
@@ -726,18 +726,20 @@ let emit_instr i =
             `	cmp	{emit_reg i.arg.(0)}, #{emit_int n}\n`;
             let comp = name_for_comparison cmp in
             `	b{emit_string comp}	{emit_label lbl}\n`; 2
-        | Ifloattest(cmp, neg) ->
-            let comp = (match (cmp, neg) with
-                          (Ceq, false) | (Cne, true) -> "eq"
-                        | (Cne, false) | (Ceq, true) -> "ne"
-                        | (Clt, false) -> "cc"
-                        | (Clt, true)  -> "cs"
-                        | (Cle, false) -> "ls"
-                        | (Cle, true)  -> "hi"
-                        | (Cgt, false) -> "gt"
-                        | (Cgt, true)  -> "le"
-                        | (Cge, false) -> "ge"
-                        | (Cge, true)  -> "lt") in
+        | Ifloattest cmp ->
+            let comp =
+              match cmp with
+              | CFeq -> "eq"
+              | CFneq -> "ne"
+              | CFlt -> "cc"
+              | CFnlt -> "cs"
+              | CFle -> "ls"
+              | CFnle -> "hi"
+              | CFgt -> "gt"
+              | CFngt -> "le"
+              | CFge -> "ge"
+              | CFnge -> "lt"
+            in
             `	fcmpd	{emit_reg i.arg.(0)}, {emit_reg i.arg.(1)}\n`;
             `	fmstat\n`;
             `	b{emit_string comp}	{emit_label lbl}\n`; 3

asmcomp/arm/selection.ml

@@ -240,16 +240,19 @@ method private select_operation_softfp op args dbg =
   | (Cfloatofint, args) -> (self#iextcall("__aeabi_i2d", false), args)
   | (Cintoffloat, args) -> (self#iextcall("__aeabi_d2iz", false), args)
   | (Ccmpf comp, args) ->
-      let func = (match comp with
-                    Cne    (* there's no __aeabi_dcmpne *)
-                  | Ceq -> "__aeabi_dcmpeq"
-                  | Clt -> "__aeabi_dcmplt"
-                  | Cle -> "__aeabi_dcmple"
-                  | Cgt -> "__aeabi_dcmpgt"
-                  | Cge -> "__aeabi_dcmpge") in
-      let comp = (match comp with
-                    Cne -> Ceq (* eq 0 => false *)
-                  | _   -> Cne (* ne 0 => true *)) in
+      let comp, func =
+        match comp with
+        | CFeq -> Cne, "__aeabi_dcmpeq"
+        | CFneq -> Ceq, "__aeabi_dcmpeq"
+        | CFlt -> Cne, "__aeabi_dcmplt"
+        | CFnlt -> Ceq, "__aeabi_dcmplt"
+        | CFle -> Cne, "__aeabi_dcmple"
+        | CFnle -> Ceq, "__aeabi_dcmple"
+        | CFgt -> Cne, "__aeabi_dcmpgt"
+        | CFngt -> Ceq, "__aeabi_dcmpgt"
+        | CFge -> Cne, "__aeabi_dcmpge"
+        | CFnge -> Ceq, "__aeabi_dcmpge"
+      in
       (Iintop_imm(Icomp(Iunsigned comp), 0),
        [Cop(Cextcall(func, typ_int, false, None), args, dbg)])
   (* Add coercions around loads and stores of 32-bit floats *)

asmcomp/arm64/emit.mlp

@@ -792,18 +792,20 @@ let emit_instr i =
             `	cmp	{emit_reg i.arg.(0)}, #{emit_int n}\n`;
             let comp = name_for_comparison cmp in
             `	b.{emit_string comp}	{emit_label lbl}\n`
-        | Ifloattest(cmp, neg) ->
-            let comp = (match (cmp, neg) with
-                        | (Ceq, false) | (Cne, true) -> "eq"
-                        | (Cne, false) | (Ceq, true) -> "ne"
-                        | (Clt, false) -> "cc"
-                        | (Clt, true)  -> "cs"
-                        | (Cle, false) -> "ls"
-                        | (Cle, true)  -> "hi"
-                        | (Cgt, false) -> "gt"
-                        | (Cgt, true)  -> "le"
-                        | (Cge, false) -> "ge"
-                        | (Cge, true)  -> "lt") in
+        | Ifloattest cmp ->
+            let comp =
+              match cmp with
+              | CFeq -> "eq"
+              | CFneq -> "ne"
+              | CFlt -> "cc"
+              | CFnlt -> "cs"
+              | CFle -> "ls"
+              | CFnle -> "hi"
+              | CFgt -> "gt"
+              | CFngt -> "le"
+              | CFge -> "ge"
+              | CFnge -> "lt"
+            in
             `	fcmp	{emit_reg i.arg.(0)}, {emit_reg i.arg.(1)}\n`;
             `	b.{emit_string comp}	{emit_label lbl}\n`
         | Ioddtest ->

asmcomp/closure.ml

@@ -226,15 +226,31 @@ let make_const_ref c =
 let make_const_int n = make_const (Uconst_int n)
 let make_const_ptr n = make_const (Uconst_ptr n)
 let make_const_bool b = make_const_ptr(if b then 1 else 0)
-let make_comparison cmp x y =
+
+let make_integer_comparison cmp x y =
   make_const_bool
     (match cmp with
        Ceq -> x = y
-     | Cneq -> x <> y
+     | Cne -> x <> y
      | Clt -> x < y
      | Cgt -> x > y
      | Cle -> x <= y
      | Cge -> x >= y)
+
+let make_float_comparison cmp x y =
+  make_const_bool
+    (match cmp with
+     | CFeq -> x = y
+     | CFneq -> not (x = y)
+     | CFlt -> x < y
+     | CFnlt -> not (x < y)
+     | CFgt -> x > y
+     | CFngt -> not (x > y)
+     | CFle -> x <= y
+     | CFnle -> not (x <= y)
+     | CFge -> x >= y
+     | CFnge -> not (x >= y))
+
 let make_const_float n = make_const_ref (Uconst_float n)
 let make_const_natint n = make_const_ref (Uconst_nativeint n)
 let make_const_int32 n = make_const_ref (Uconst_int32 n)
@@ -280,7 +296,7 @@ let simplif_arith_prim_pure fpc p (args, approxs) dbg =
           make_const_int (n1 lsr n2)
       | Pasrint when 0 <= n2 && n2 < 8 * Arch.size_int ->
           make_const_int (n1 asr n2)
-      | Pintcomp c -> make_comparison c n1 n2
+      | Pintcomp c -> make_integer_comparison c n1 n2
       | _ -> default
       end
   (* float *)
@@ -299,7 +315,7 @@ let simplif_arith_prim_pure fpc p (args, approxs) dbg =
       | Psubfloat -> make_const_float (n1 -. n2)
       | Pmulfloat -> make_const_float (n1 *. n2)
       | Pdivfloat -> make_const_float (n1 /. n2)
-      | Pfloatcomp c  -> make_comparison c n1 n2
+      | Pfloatcomp c  -> make_float_comparison c n1 n2
       | _ -> default
       end
   (* nativeint *)
@@ -325,7 +341,7 @@ let simplif_arith_prim_pure fpc p (args, approxs) dbg =
       | Pandbint Pnativeint -> make_const_natint (Nativeint.logand n1 n2)
       | Porbint Pnativeint ->  make_const_natint (Nativeint.logor n1 n2)
       | Pxorbint Pnativeint -> make_const_natint (Nativeint.logxor n1 n2)
-      | Pbintcomp(Pnativeint, c)  -> make_comparison c n1 n2
+      | Pbintcomp(Pnativeint, c)  -> make_integer_comparison c n1 n2
       | _ -> default
       end
   (* nativeint, int *)
@@ -363,7 +379,7 @@ let simplif_arith_prim_pure fpc p (args, approxs) dbg =
       | Pandbint Pint32 -> make_const_int32 (Int32.logand n1 n2)
       | Porbint Pint32 -> make_const_int32 (Int32.logor n1 n2)
       | Pxorbint Pint32 -> make_const_int32 (Int32.logxor n1 n2)
-      | Pbintcomp(Pint32, c) -> make_comparison c n1 n2
+      | Pbintcomp(Pint32, c) -> make_integer_comparison c n1 n2
       | _ -> default
       end
   (* int32, int *)
@@ -401,7 +417,7 @@ let simplif_arith_prim_pure fpc p (args, approxs) dbg =
       | Pandbint Pint64 -> make_const_int64 (Int64.logand n1 n2)
       | Porbint Pint64 -> make_const_int64 (Int64.logor n1 n2)
       | Pxorbint Pint64 -> make_const_int64 (Int64.logxor n1 n2)
-      | Pbintcomp(Pint64, c) -> make_comparison c n1 n2
+      | Pbintcomp(Pint64, c) -> make_integer_comparison c n1 n2
       | _ -> default
       end
   (* int64, int *)

asmcomp/cmm.ml

@@ -89,24 +89,21 @@ let size_machtype mty =
   done;
   !size
 
-type comparison =
-    Ceq
-  | Cne
-  | Clt
-  | Cle
-  | Cgt
-  | Cge
-
-let negate_comparison = function
-    Ceq -> Cne | Cne -> Ceq
-  | Clt -> Cge | Cle -> Cgt
-  | Cgt -> Cle | Cge -> Clt
-
-let swap_comparison = function
-    Ceq -> Ceq | Cne -> Cne
-  | Clt -> Cgt | Cle -> Cge
-  | Cgt -> Clt | Cge -> Cle
+type integer_comparison = Lambda.integer_comparison =
+  | Ceq | Cne | Clt | Cgt | Cle | Cge
 
+let negate_integer_comparison = Lambda.negate_integer_comparison
+
+let swap_integer_comparison = Lambda.swap_integer_comparison
+
+(* With floats [not (x < y)] is not the same as [x >= y] due to NaNs,
+   so we provide additional comparisons to represent the negations.*)
+type float_comparison = Lambda.float_comparison =
+  | CFeq | CFneq | CFlt | CFnlt | CFgt | CFngt | CFle | CFnle | CFge | CFnge
+
+let negate_float_comparison = Lambda.negate_float_comparison
+
+let swap_float_comparison = Lambda.swap_float_comparison
 type label = int
 
 let label_counter = ref 99
@@ -142,13 +139,13 @@ and operation =
   | Cstore of memory_chunk * Lambda.initialization_or_assignment
   | Caddi | Csubi | Cmuli | Cmulhi | Cdivi | Cmodi
   | Cand | Cor | Cxor | Clsl | Clsr | Casr
-  | Ccmpi of comparison
+  | Ccmpi of integer_comparison
   | Caddv | Cadda
-  | Ccmpa of comparison
+  | Ccmpa of integer_comparison
   | Cnegf | Cabsf
   | Caddf | Csubf | Cmulf | Cdivf
   | Cfloatofint | Cintoffloat
-  | Ccmpf of comparison
+  | Ccmpf of float_comparison
   | Craise of raise_kind
   | Ccheckbound
 

asmcomp/cmm.mli

@@ -72,16 +72,17 @@ val ge_component
 
 val size_machtype: machtype -> int
 
-type comparison =
-    Ceq
-  | Cne
-  | Clt
-  | Cle
-  | Cgt
-  | Cge
+type integer_comparison = Lambda.integer_comparison =
+  | Ceq | Cne | Clt | Cgt | Cle | Cge
 
-val negate_comparison: comparison -> comparison
-val swap_comparison: comparison -> comparison
+val negate_integer_comparison: integer_comparison -> integer_comparison
+val swap_integer_comparison: integer_comparison -> integer_comparison
+
+type float_comparison = Lambda.float_comparison =
+  | CFeq | CFneq | CFlt | CFnlt | CFgt | CFngt | CFle | CFnle | CFge | CFnge
+
+val negate_float_comparison: float_comparison -> float_comparison
+val swap_float_comparison: float_comparison -> float_comparison
 
 type label = int
 val new_label: unit -> label
@@ -113,14 +114,14 @@ and operation =
   | Cstore of memory_chunk * Lambda.initialization_or_assignment
   | Caddi | Csubi | Cmuli | Cmulhi | Cdivi | Cmodi
   | Cand | Cor | Cxor | Clsl | Clsr | Casr
-  | Ccmpi of comparison
+  | Ccmpi of integer_comparison
   | Caddv (* pointer addition that produces a [Val] (well-formed Caml value) *)
   | Cadda (* pointer addition that produces a [Addr] (derived heap pointer) *)
-  | Ccmpa of comparison
+  | Ccmpa of integer_comparison
   | Cnegf | Cabsf
   | Caddf | Csubf | Cmulf | Cdivf
   | Cfloatofint | Cintoffloat
-  | Ccmpf of comparison
+  | Ccmpf of float_comparison
   | Craise of raise_kind
   | Ccheckbound