compiler: Fix some vestigial +0.0/-0.0 issues

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,
+    <<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.
 
 %%
 

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.
 %%%