File 2111-erts-Fix-term-equivalence-comparisons-on-f... of Package erlang

Overview Repositories Revisions Requests Users Attributes Meta

File 2111-erts-Fix-term-equivalence-comparisons-on-floating-po.patch of Package erlang (Revision 2f15b05a39d64e5cba90e927e8665465)

Currently displaying revision 2f15b05a39d64e5cba90e927e8665465 , Show latest

From e3e6efef0592047da583ec62205e9d1805c9a153 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?John=20H=C3=B6gberg?= <john@erlang.org>
Date: Fri, 13 Oct 2023 09:52:32 +0200
Subject: [PATCH] erts: Fix term equivalence comparisons on floating-point zero

+0.0 will now be considered distinct from -0.0
---
 erts/emulator/beam/erl_term.h              |   4 +-
 erts/emulator/beam/erl_term_hashing.c      |   5 -
 erts/emulator/beam/erl_utils.h             |  29 +++++-
 erts/emulator/beam/utils.c                 |  22 ++++-
 erts/emulator/test/bs_match_misc_SUITE.erl |   2 +-
 erts/emulator/test/float_SUITE.erl         |   8 +-
 erts/emulator/test/hash_SUITE.erl          |   7 +-
 erts/emulator/test/num_bif_SUITE.erl       |   2 +-
 erts/emulator/test/op_SUITE.erl            | 105 +++++++++++++++++++--
 lib/compiler/src/beam_ssa_type.erl         |   5 +-
 lib/compiler/test/float_SUITE.erl          |   2 +-
 lib/stdlib/test/io_SUITE.erl               |   2 +-
 lib/stdlib/test/math_SUITE.erl             |   2 +-
 13 files changed, 160 insertions(+), 35 deletions(-)

diff --git a/erts/emulator/beam/erl_term.h b/erts/emulator/beam/erl_term.h
index b2432b6806..fcbd70809d 100644
--- a/erts/emulator/beam/erl_term.h
+++ b/erts/emulator/beam/erl_term.h
@@ -472,9 +472,7 @@ typedef union float_def
     byte   fb[sizeof(ieee754_8)];
     Uint16 fs[sizeof(ieee754_8) / sizeof(Uint16)];
     Uint32 fw[sizeof(ieee754_8) / sizeof(Uint32)];
-#if defined(ARCH_64)
-    Uint   fdw;
-#endif
+    Uint64 fdw;
 } FloatDef;
 
 #if defined(ARCH_64)
diff --git a/erts/emulator/beam/erl_term_hashing.c b/erts/emulator/beam/erl_term_hashing.c
index 7aa10c9a85..ef1c2f85b8 100644
--- a/erts/emulator/beam/erl_term_hashing.c
+++ b/erts/emulator/beam/erl_term_hashing.c
@@ -2108,11 +2108,6 @@ make_internal_hash(Eterm term, erts_ihash_t salt)
 
                 GET_DOUBLE(term, ff);
 
-                if (ff.fd == 0.0f) {
-                    /* ensure positive 0.0 */
-                    ff.fd = erts_get_positive_zero_float();
-                }
-
                 IHASH_MIX_ALPHA(IHASH_TYPE_FLOAT);
                 IHASH_MIX_BETA_2F32(ff.fw[0], ff.fw[1]);
 
diff --git a/erts/emulator/beam/erl_utils.h b/erts/emulator/beam/erl_utils.h
index dce3665a8d..b9b1d524eb 100644
--- a/erts/emulator/beam/erl_utils.h
+++ b/erts/emulator/beam/erl_utils.h
@@ -184,6 +184,8 @@ Sint erts_cmp_compound(Eterm, Eterm, int, int);
 
 #define erts_float_comp(x,y) (((x)<(y)) ? -1 : (((x)==(y)) ? 0 : 1))
 
+ERTS_GLB_INLINE Uint64 erts_float_exact_sortable(const FloatDef *value);
+
 #if ERTS_GLB_INLINE_INCL_FUNC_DEF
 
 ERTS_GLB_INLINE int erts_cmp_atoms(Eterm a, Eterm b) {
@@ -215,6 +217,22 @@ ERTS_GLB_INLINE int erts_cmp_atoms(Eterm a, Eterm b) {
     return len_a - len_b;
 }
 
+/* Provides a sortable integer from the raw bits of a floating-point number.
+ *
+ * When these are compared, they return the exact same result as a floating-
+ * point comparison of the inputs aside from the fact that -0.0 < +0.0, making
+ * it suitable for use in term equivalence operators and map key order. */
+ERTS_GLB_INLINE Uint64 erts_float_exact_sortable(const FloatDef *value) {
+    static const Uint64 sign_bit = ((Uint64)1) << 63;
+    Uint64 float_bits = value->fdw;
+
+    if (float_bits & sign_bit) {
+        return ~float_bits;
+    }
+
+    return float_bits ^ sign_bit;
+}
+
 ERTS_GLB_INLINE Sint erts_cmp(Eterm a, Eterm b, int exact, int eq_only) {
     if (is_atom(a) && is_atom(b)) {
         return erts_cmp_atoms(a, b);
@@ -226,7 +244,16 @@ ERTS_GLB_INLINE Sint erts_cmp(Eterm a, Eterm b, int exact, int eq_only) {
         GET_DOUBLE(a, af);
         GET_DOUBLE(b, bf);
 
-        return erts_float_comp(af.fd, bf.fd);
+        if (exact) {
+            Uint64 sortable_a, sortable_b;
+
+            sortable_a = erts_float_exact_sortable(&af);
+            sortable_b = erts_float_exact_sortable(&bf);
+
+            return erts_float_comp(sortable_a, sortable_b);
+        } else {
+            return erts_float_comp(af.fd, bf.fd);
+        }
     }
 
     return erts_cmp_compound(a,b,exact,eq_only);
diff --git a/erts/emulator/beam/utils.c b/erts/emulator/beam/utils.c
index 208675f865..286093c957 100644
--- a/erts/emulator/beam/utils.c
+++ b/erts/emulator/beam/utils.c
@@ -1403,7 +1403,9 @@ tailrecur_ne:
 		    if (is_float(b)) {
 			GET_DOUBLE(a, af);
 			GET_DOUBLE(b, bf);
-			if (af.fd == bf.fd) goto pop_next;
+                        if (af.fdw == bf.fdw) {
+                            goto pop_next;
+                        }
 		    }
 		    break; /* not equal */
 		}
@@ -2016,11 +2018,21 @@ tailrecur_ne:
 		    goto mixed_types;
 		} else {
 		    FloatDef af;
-		    FloatDef bf; 
+		    FloatDef bf;
+
+                    GET_DOUBLE(a, af);
+                    GET_DOUBLE(b, bf);
 
-		    GET_DOUBLE(a, af);
-		    GET_DOUBLE(b, bf);
-		    ON_CMP_GOTO(erts_float_comp(af.fd, bf.fd));
+                    if (exact) {
+                        Uint64 sortable_a, sortable_b;
+
+                        sortable_a = erts_float_exact_sortable(&af);
+                        sortable_b = erts_float_exact_sortable(&bf);
+
+                        ON_CMP_GOTO(erts_float_comp(sortable_a, sortable_b));
+                    } else {
+                        ON_CMP_GOTO(erts_float_comp(af.fd, bf.fd));
+                    }
 		}
 	    case (_TAG_HEADER_POS_BIG >> _TAG_PRIMARY_SIZE):
 	    case (_TAG_HEADER_NEG_BIG >> _TAG_PRIMARY_SIZE):
diff --git a/erts/emulator/test/bs_match_misc_SUITE.erl b/erts/emulator/test/bs_match_misc_SUITE.erl
index 83f4873dbe..284da3c3f3 100644
--- a/erts/emulator/test/bs_match_misc_SUITE.erl
+++ b/erts/emulator/test/bs_match_misc_SUITE.erl
@@ -91,7 +91,7 @@ float_middle_endian(Config) when is_list(Config) ->
     ok.
 
 
-fcmp(0.0, 0.0) -> ok;
+fcmp(F1, F2) when F1 == 0.0, F2 == 0.0 -> ok;
 fcmp(F1, F2) when (F1 - F2) / F2 < 0.0000001 -> ok.
     
 match_float(Bin0, Fsz, I) ->
diff --git a/erts/emulator/test/float_SUITE.erl b/erts/emulator/test/float_SUITE.erl
index e62f63db6f..9c4b01e35d 100644
--- a/erts/emulator/test/float_SUITE.erl
+++ b/erts/emulator/test/float_SUITE.erl
@@ -378,7 +378,7 @@ op_add(A, B) ->
     R = unify(catch A + B, Info),
     R = unify(my_apply(erlang,'+',[A,B]), Info),
     case R of
-        _ when A + B =:= element(1,R) -> ok;
+        _ when A + B == element(1,R) -> ok;
         {{'EXIT',badarith}, Info} -> ok
     end.
 
@@ -387,7 +387,7 @@ op_sub(A, B) ->
     R = unify(catch A - B, Info),
     R = unify(my_apply(erlang,'-',[A,B]), Info),
     case R of
-        _ when A - B =:= element(1,R) -> ok;
+        _ when A - B == element(1,R) -> ok;
         {{'EXIT',badarith}, Info} -> ok
     end.
 
@@ -396,7 +396,7 @@ op_mul(A, B) ->
     R = unify(catch A * B, Info),
     R = unify(my_apply(erlang,'*',[A,B]), Info),
     case R of
-        _ when A * B =:= element(1,R) -> ok;
+        _ when A * B == element(1,R) -> ok;
         {{'EXIT',badarith}, Info} -> ok
     end.
 
@@ -405,7 +405,7 @@ op_div(A, B) ->
     R = unify(catch A / B, Info),
     R = unify(my_apply(erlang,'/',[A,B]), Info),
     case R of
-        _ when A / B =:= element(1,R) -> ok;
+        _ when A / B == element(1,R) -> ok;
         {{'EXIT',badarith}, Info} -> ok
     end.
 
diff --git a/erts/emulator/test/hash_SUITE.erl b/erts/emulator/test/hash_SUITE.erl
index 90b96f2f97..e594c3b3be 100644
--- a/erts/emulator/test/hash_SUITE.erl
+++ b/erts/emulator/test/hash_SUITE.erl
@@ -835,9 +835,10 @@ hash_zero_test() ->
 hash_zero_test([Z|Zs],F) ->
     hash_zero_test(Zs,Z,F(Z),F).
 hash_zero_test([Z|Zs],Z0,V,F) ->
-    true = Z0 =:= Z, %% assert exact equal
-    Z0   = Z,        %% assert matching
-    V    = F(Z),     %% assert hash
+    true = (0.0 == Z0) andalso (0.0 == Z),
+    %% assert that phash and phash2 yield the same hash for both -0.0 and +0.0,
+    %% even though they are different terms since OTP 27.
+    V    = F(Z),
     hash_zero_test(Zs,Z0,V,F);
 hash_zero_test([],_,_,_) ->
     ok.
diff --git a/erts/emulator/test/num_bif_SUITE.erl b/erts/emulator/test/num_bif_SUITE.erl
index c53b660bf5..b986eb25b8 100644
--- a/erts/emulator/test/num_bif_SUITE.erl
+++ b/erts/emulator/test/num_bif_SUITE.erl
@@ -354,7 +354,7 @@ max_diff_decimals(F, D) ->
 
 t_string_to_float_safe(Config) when is_list(Config) ->
     test_stf(0.0,"0.0"),
-    test_stf(0.0,"-0.0"),
+    test_stf(-0.0,"-0.0"),
     test_stf(0.5,"0.5"),
     test_stf(-0.5,"-0.5"),
     test_stf(100.0,"1.0e2"),
diff --git a/erts/emulator/test/op_SUITE.erl b/erts/emulator/test/op_SUITE.erl
index 358c2e0df6..ef5bbccc27 100644
--- a/erts/emulator/test/op_SUITE.erl
+++ b/erts/emulator/test/op_SUITE.erl
@@ -25,7 +25,8 @@
 -export([all/0, suite/0,
          bsl_bsr/1,logical/1,t_not/1,relop_simple/1,relop/1,
          complex_relop/1,unsafe_fusing/1,
-         range_tests/1,combined_relops/1,typed_relop/1]).
+         range_tests/1,combined_relops/1,typed_relop/1,
+         term_equivalence/1]).
 
 -import(lists, [foldl/3,flatmap/2]).
 
@@ -36,7 +37,7 @@ suite() ->
 all() ->
     [bsl_bsr, logical, t_not, relop_simple, relop,
      complex_relop, unsafe_fusing, range_tests,
-     combined_relops, typed_relop].
+     combined_relops, typed_relop, term_equivalence].
 
 %% Test the bsl and bsr operators.
 bsl_bsr(Config) when is_list(Config) ->
@@ -146,8 +147,8 @@ relop_simple(Config) when is_list(Config) ->
     F2 = float(Big2),
     T1 = erlang:make_tuple(3,87),
     T2 = erlang:make_tuple(3,87),
-    Terms = [-F2,Big2,-F1,-Big1,-33,-33.0,0,0.0,42,42.0,Big1,F1,Big2,F2,a,b,
-             {T1,a},{T2,b},[T1,Big1],[T2,Big2]],
+    Terms = [-F2,Big2,-F1,-Big1,-33,-33.0,0,0.0,-0.0,42,42.0,Big1,F1,Big2,F2,
+             a,b,{T1,a},{T2,b},[T1,Big1],[T2,Big2]],
 
     Combos = [{V1,V2} || V1 <- Terms, V2 <- Terms],
 
@@ -181,6 +182,8 @@ relop_simple_do(V1,V2) ->
     ID = not (V1 =/= V2),
     ID = not (V2 =/= V1),
 
+    implies(ID, V1 == V2),
+
     EQ = V1 == V2,
     EQ = V2 == V1,
     EQ = not (V1 /= V2),
@@ -193,6 +196,9 @@ relop_simple_do(V1,V2) ->
         {false, false, false, true,  +1} -> ok
     end.
 
+implies(false, _) -> ok;
+implies(true, true) -> ok.
+
 %% Emulate internal "cmp"
 cmp_emu(A,B) when is_tuple(A), is_tuple(B) ->
     SA = size(A),
@@ -297,7 +303,7 @@ relop(Config) when is_list(Config) ->
     Bin = <<"abc">>,
     BitString = <<0:7>>,
     Map = #{a => b},
-    Vs0 = [a,b,-33,-33.0,0,0.0,42,42.0,Big1,Big2,F1,F2,
+    Vs0 = [a,b,-33,-33.0,0,0.0,-0,0,42,42.0,Big1,Big2,F1,F2,
            Bin,BitString,Map],
     Vs = [unvalue(V) || V <- Vs0],
     Ops = ['==', '/=', '=:=', '=/=', '<', '=<', '>', '>='],
@@ -310,7 +316,7 @@ complex_relop(Config) when is_list(Config) ->
     Bin = <<"abc">>,
     BitString = <<0:7>>,
     Map = #{a => b},
-    Vs0 = [an_atom,42.0,42,Big,Float,Bin,BitString,Map],
+    Vs0 = [an_atom,42.0,42,0.0,-0.0,Big,Float,Bin,BitString,Map],
     Vs = flatmap(fun(X) -> [unvalue({X}),unvalue([X])] end, Vs0),
     Ops = ['==', '/=', '=:=', '=/=', '<', '=<', '>', '>='],
     binop(Ops, Vs).
@@ -985,6 +991,93 @@ classify_value(N) when is_integer(N), N < 0 ->
 classify_value(_N) ->
     other.
 
+term_equivalence(_Config) ->
+    %% Term equivalence has been tested before in this suite, but we need to
+    %% massage some edge cases that cannot easily be put into the other test
+    %% cases.
+    <<PosZero/float>> = id(<<0:1,0:63>>),
+    <<NegZero/float>> = id(<<1:1,0:63>>),
+
+    +0.0 = id(PosZero),
+    -0.0 = id(NegZero),
+
+    -1 = erts_internal:cmp_term(NegZero, PosZero),
+    1 = erts_internal:cmp_term(PosZero, NegZero),
+
+    -1 = cmp_float(NegZero, PosZero),
+    1 = cmp_float(PosZero, NegZero),
+
+    Floats = [0.0, -0.0, 4711.0, -4711.0, 12.0, 943.0],
+
+    [true = (cmp_float(A, B) =:= erts_internal:cmp_term(A, B)) ||
+     A <- Floats, B <- Floats],
+
+    ok.
+
+cmp_float(A0, B0) ->
+    A = float_comparable(A0),
+    B = float_comparable(B0),
+    if
+        A < B -> -1;
+        A > B -> +1;
+        A =:= B -> 0
+    end.
+
+%% Converts a float to a number which, when compared with other such converted
+%% floats, is ordered the same as '<' on the original inputs aside from the
+%% fact that -0.0 < +0.0 as required by the term equivalence order.
+%%
+%% This has been proven correct with the SMT-LIB model below:
+%%
+%% (define-const SignBit_bv (_ BitVec 64) #x8000000000000000)
+%% 
+%% ; Two finite floats X and Y of unknown value
+%% (declare-const X (_ FloatingPoint 11 53))
+%% (declare-const Y (_ FloatingPoint 11 53))
+%% (assert (= false (fp.isInfinite X) (fp.isInfinite Y)
+%%            (fp.isNaN X) (fp.isNaN Y)))
+%% 
+%% ; ... the bit representations of the aforementioned floats. The Z3 floating-
+%% ; point extension lacks a way to directly bit-cast a vector to a float, so
+%% ; we rely on equivalence here.
+%% (declare-const X_bv (_ BitVec 64))
+%% (declare-const Y_bv (_ BitVec 64))
+%% (assert (= ((_ to_fp 11 53) X_bv) X))
+%% (assert (= ((_ to_fp 11 53) Y_bv) Y))
+%% 
+%% ; The bit hack we're going to test
+%% (define-fun float_sortable ((value (_ BitVec 64))) (_ BitVec 64)
+%% (ite (distinct (bvand value SignBit_bv) SignBit_bv)
+%%  (bvxor value SignBit_bv)
+%%  (bvnot value)))
+%% 
+%% (define-fun float_bv_lt ((LHS (_ BitVec 64))
+%%                          (RHS (_ BitVec 64))) Bool
+%%  (bvult (float_sortable LHS) (float_sortable RHS)))
+%% 
+%% (push 1)
+%%   ; When either of X or Y are non-zero, (X < Y) = (bvX < bvY)
+%%   (assert (not (and (fp.isZero X) (fp.isZero Y))))
+%%   (assert (distinct (fp.lt X Y) (float_bv_lt X_bv Y_bv)))
+%%   (check-sat) ; unsat, proving by negation that the above always holds
+%% (pop 1)
+%% 
+%% (push 1)
+%%   ; Negative zero should sort lower than positive zero
+%%   (assert (and (fp.isNegative X) (fp.isPositive Y)
+%%                (fp.isZero X) (fp.isZero Y)))
+%%   (assert (not (float_bv_lt X_bv Y_bv)))
+%%   (check-sat) ; unsat
+%% (pop 1)
+float_comparable(V0) ->
+    Sign = 16#8000000000000000,
+    Mask = 16#FFFFFFFFFFFFFFFF,
+    <<V_bv:64/unsigned>> = <<V0/float>>,
+    case V_bv band Sign of
+        0 -> (V_bv bxor Sign) band Mask;
+        Sign -> (bnot V_bv) band Mask
+    end.
+
 %%%
 %%% Utilities.
 %%%
diff --git a/lib/compiler/src/beam_ssa_type.erl b/lib/compiler/src/beam_ssa_type.erl
index 3db712ac01..1a988d2b13 100644
--- a/lib/compiler/src/beam_ssa_type.erl
+++ b/lib/compiler/src/beam_ssa_type.erl
@@ -1180,10 +1180,9 @@ simplify(#b_set{op={bif,Op0},args=[A,B]}=I, Ts, Ds) when Op0 =:= '==';
                {#t_integer{},#t_integer{}} ->
                    %% Both side contain integers but no floats.
                    true;
-               {#t_float{},#t_float{}} ->
-                   %% Both side contain floats but no integers.
-                   true;
                {_,_} ->
+                   %% Either side can contain a number, substitution is unsafe
+                   %% even if both sides are floats as `-0.0 == +0.0`
                    false
            end,
     case EqEq of
diff --git a/lib/compiler/test/float_SUITE.erl b/lib/compiler/test/float_SUITE.erl
index 7a5aedcec6..da2128a560 100644
--- a/lib/compiler/test/float_SUITE.erl
+++ b/lib/compiler/test/float_SUITE.erl
@@ -55,7 +55,7 @@ float_zero(Config) when is_list(Config) ->
     <<16#8000000000000000:64>> = match_on_zero_and_to_binary(-1*0.0),
     ok.
 
-match_on_zero_and_to_binary(0.0 = X) -> <<X/float>>.
+match_on_zero_and_to_binary(X) when X == 0.0 -> <<X/float>>.
 
 %% Thanks to Tobias Lindahl <tobias.lindahl@it.uu.se>
 %% Shows the effect of pending exceptions on the x86.
diff --git a/lib/stdlib/test/io_SUITE.erl b/lib/stdlib/test/io_SUITE.erl
index f26d98cc18..877e4eec75 100644
--- a/lib/stdlib/test/io_SUITE.erl
+++ b/lib/stdlib/test/io_SUITE.erl
@@ -1562,7 +1562,7 @@ f2r({S,BE,M}) when 0 =< S, S =< 1,
     <<F:64/float>> = <<S:1, BE:11, M:52>>,
     case catch T/N of
         {'EXIT', _} -> ok;
-        TN -> true = F =:= TN
+        TN -> true = F == TN
     end,
     Vr.
 
diff --git a/lib/stdlib/test/math_SUITE.erl b/lib/stdlib/test/math_SUITE.erl
index 5e92debd69..ba95aa350b 100644
--- a/lib/stdlib/test/math_SUITE.erl
+++ b/lib/stdlib/test/math_SUITE.erl
@@ -69,7 +69,7 @@ floor_ceil(_Config) ->
     MinusZero = 0.0/(-1.0),
     -43.0 = do_floor_ceil(-42.1),
     -43.0 = do_floor_ceil(-42.7),
-    0.0 = do_floor_ceil(MinusZero),
+    true = (0.0 == do_floor_ceil(MinusZero)),
     10.0 = do_floor_ceil(10.1),
     10.0 = do_floor_ceil(10.9),
 
-- 
2.35.3

Places

File 2111-erts-Fix-term-equivalence-comparisons-on-floating-po.patch of Package erlang (Revision 2f15b05a39d64e5cba90e927e8665465)

Places