File 2111-erts-Fix-term-equivalence-comparisons-on-floating-po.patch of Package erlang
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
