diff --git a/lib/compiler/src/beam_types.erl b/lib/compiler/src/beam_types.erl index 3fc2476898e1..68be4fe5add0 100644 --- a/lib/compiler/src/beam_types.erl +++ b/lib/compiler/src/beam_types.erl @@ -45,7 +45,6 @@ make_boolean/0, make_cons/2, make_float/1, - make_float/2, make_integer/1, make_integer/2]). @@ -479,8 +478,7 @@ is_bs_matchable_type(Type) -> Result :: {ok, term()} | error. get_singleton_value(#t_atom{elements=[Atom]}) -> {ok, Atom}; -get_singleton_value(#t_float{elements={Float,Float}}) when Float /= 0 -> - %% 0.0 is not actually a singleton as it has two encodings: 0.0 and -0.0 +get_singleton_value(#t_float{elements={Float,Float}}) -> {ok, Float}; get_singleton_value(#t_integer{elements={Int,Int}}) -> {ok, Int}; @@ -697,11 +695,7 @@ make_cons(Head0, Tail) -> -spec make_float(float()) -> type(). make_float(Float) when is_float(Float) -> - make_float(Float, Float). - --spec make_float(float(), float()) -> type(). -make_float(Min, Max) when is_float(Min), is_float(Max), Min =< Max -> - #t_float{elements={Min, Max}}. + #t_float{elements={Float,Float}}. -spec make_integer(integer()) -> type(). make_integer(Int) when is_integer(Int) -> @@ -1128,10 +1122,18 @@ is_identifier(reference) -> true; is_identifier(_) -> false. lub_ranges({MinA,MaxA}, {MinB,MaxB}) -> - {inf_min(MinA, MinB), inf_max(MaxA, MaxB)}; + widen_range({inf_min(MinA, MinB), inf_max(MaxA, MaxB)}); lub_ranges(_, _) -> any. +%% Expands integer 0 to `-0.0 .. +0.0` +widen_range({Min, 0}) -> + widen_range({Min, +0.0}); +widen_range({0, Max}) -> + widen_range({-0.0, Max}); +widen_range({Min, Max}) -> + {Min, Max}. + lub_bs_matchable(UnitA, UnitB) -> #t_bs_matchable{tail_unit=gcd(UnitA, UnitB)}. @@ -1179,12 +1181,13 @@ float_from_range(none) -> none; float_from_range(any) -> #t_float{}; -float_from_range({Min0,Max0}) -> - case {safe_float(Min0),safe_float(Max0)} of +float_from_range({Min0, Max0}) -> + true = inf_le(Min0, Max0), %Assertion. + case {safe_float(Min0), safe_float(Max0)} of {'-inf','+inf'} -> #t_float{}; - {Min,Max} -> - #t_float{elements={Min,Max}} + {Min, Max} -> + #t_float{elements={Min, Max}} end. safe_float(N) when is_number(N) -> @@ -1218,21 +1221,104 @@ number_from_range(N) -> none end. -inf_le('-inf', _) -> true; -inf_le(A, B) -> A =< B. - -inf_ge(_, '-inf') -> true; -inf_ge('-inf', _) -> false; -inf_ge(A, B) -> A >= B. +inf_le('-inf', _) -> + true; +inf_le(A, B) when is_float(A), is_float(B) -> + %% When floats are compared to floats, the total ordering function must be + %% used to preserve `-0.0 =/= +0.0`. + float_comparable(A) =< float_comparable(B); +inf_le(A, B) -> + A =< B. + +inf_ge(_, '-inf') -> + true; +inf_ge('-inf', _) -> + false; +inf_ge(A, B) when is_float(A), is_float(B) -> + float_comparable(A) >= float_comparable(B); +inf_ge(A, B) -> + A >= B. + +inf_min(A, B) when A =:= '-inf'; B =:= '-inf' -> + '-inf'; +inf_min(A, B) when is_float(A), is_float(B) -> + case float_comparable(A) =< float_comparable(B) of + true -> A; + false -> B + end; +inf_min(A, B) when A =< B -> + A; +inf_min(A, B) when A > B -> + B. -inf_min(A, B) when A =:= '-inf'; B =:= '-inf' -> '-inf'; -inf_min(A, B) when A =< B -> A; -inf_min(A, B) when A > B -> B. +inf_max('-inf', B) -> + B; +inf_max(A, '-inf') -> + A; +inf_max(A, B) when is_float(A), is_float(B) -> + case float_comparable(A) >= float_comparable(B) of + true -> A; + false -> B + end; +inf_max(A, B) when A >= B -> + A; +inf_max(A, B) when A < B -> + B. -inf_max('-inf', B) -> B; -inf_max(A, '-inf') -> A; -inf_max(A, B) when A >= B -> A; -inf_max(A, B) when A < B -> B. +%% 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) when is_float(V0) -> + Sign = 16#8000000000000000, + Mask = 16#FFFFFFFFFFFFFFFF, + <> = <>, + case V_bv band Sign of + 0 -> (V_bv bxor Sign) band Mask; + Sign -> (bnot V_bv) band Mask + end. %% diff --git a/lib/compiler/test/beam_type_SUITE.erl b/lib/compiler/test/beam_type_SUITE.erl index 49b5cb6e745c..69670448f421 100644 --- a/lib/compiler/test/beam_type_SUITE.erl +++ b/lib/compiler/test/beam_type_SUITE.erl @@ -31,7 +31,7 @@ switch_fail_inference/1,failures/1, cover_maps_functions/1,min_max_mixed_types/1, not_equal/1,infer_relops/1,binary_unit/1,premature_concretization/1, - funs/1,will_succeed/1]). + funs/1,will_succeed/1,float_confusion/1]). %% Force id/1 to return 'any'. -export([id/1]). @@ -1505,6 +1505,14 @@ will_succeed_1(_V0, _V1) will_succeed_1(_, _) -> b. +%% GH-7901: Range operations did not honor the total order of floats. +float_confusion(_Config) -> + ok = float_confusion_1(catch (true = ok), -0.0), + ok = float_confusion_1(ok, 0.0). + +float_confusion_1(_, _) -> + ok. + %%% %%% Common utilities. %%%