Sign Up
Log In
Log In
or
Sign Up
Places
All Projects
Status Monitor
Collapse sidebar
home:Ledest:erlang:26
erlang
2111-erts-Fix-term-equivalence-comparisons-on-f...
Overview
Repositories
Revisions
Requests
Users
Attributes
Meta
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
Locations
Projects
Search
Status Monitor
Help
OpenBuildService.org
Documentation
API Documentation
Code of Conduct
Contact
Support
@OBShq
Terms
openSUSE Build Service is sponsored by
The Open Build Service is an
openSUSE project
.
Sign Up
Log In
Places
Places
All Projects
Status Monitor
