Skip to content

Commit 78d76a3

Browse files
jhogbergjhogberg
committed
compiler: Fix some vestigial +0.0/-0.0 issues
1 parent a8bc077 commit 78d76a3

File tree

2 files changed

+127
-33
lines changed

2 files changed

+127
-33
lines changed

‎lib/compiler/src/beam_types.erl

Lines changed: 118 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,6 @@
4545
make_boolean/0,
4646
make_cons/2,
4747
make_float/1,
48-
make_float/2,
4948
make_integer/1,
5049
make_integer/2]).
5150

@@ -479,8 +478,7 @@ is_bs_matchable_type(Type) ->
479478
Result :: {ok, term()} | error.
480479
get_singleton_value(#t_atom{elements=[Atom]}) ->
481480
{ok, Atom};
482-
get_singleton_value(#t_float{elements={Float,Float}}) when Float /= 0 ->
483-
%% 0.0 is not actually a singleton as it has two encodings: 0.0 and -0.0
481+
get_singleton_value(#t_float{elements={Float,Float}}) ->
484482
{ok, Float};
485483
get_singleton_value(#t_integer{elements={Int,Int}}) ->
486484
{ok, Int};
@@ -697,11 +695,7 @@ make_cons(Head0, Tail) ->
697695

698696
-spec make_float(float()) -> type().
699697
make_float(Float) when is_float(Float) ->
700-
make_float(Float, Float).
701-
702-
-spec make_float(float(), float()) -> type().
703-
make_float(Min, Max) when is_float(Min), is_float(Max), Min =< Max ->
704-
#t_float{elements={Min, Max}}.
698+
#t_float{elements={Float,Float}}.
705699

706700
-spec make_integer(integer()) -> type().
707701
make_integer(Int) when is_integer(Int) ->
@@ -1053,9 +1047,9 @@ lub(#t_cons{type=Type,terminator=Term}, nil) ->
10531047
lub(#t_float{elements=R1}, #t_float{elements=R2}) ->
10541048
float_from_range(lub_ranges(R1, R2));
10551049
lub(#t_float{elements=R1}, #t_integer{elements=R2}) ->
1056-
number_from_range(lub_ranges(R1, R2));
1050+
number_from_range(widen_range(lub_ranges(R1, R2)));
10571051
lub(#t_float{elements=R1}, #t_number{elements=R2}) ->
1058-
number_from_range(lub_ranges(R1, R2));
1052+
number_from_range(widen_range(lub_ranges(R1, R2)));
10591053
lub(#t_fun{arity=SameArity,target=SameTarget,type=TypeA},
10601054
#t_fun{arity=SameArity,target=SameTarget,type=TypeB}) ->
10611055
#t_fun{arity=SameArity,target=SameTarget,type=join(TypeA, TypeB)};
@@ -1066,9 +1060,9 @@ lub(#t_fun{type=TypeA}, #t_fun{type=TypeB}) ->
10661060
lub(#t_integer{elements=R1}, #t_integer{elements=R2}) ->
10671061
integer_from_range(lub_ranges(R1, R2));
10681062
lub(#t_integer{elements=R1}, #t_float{elements=R2}) ->
1069-
number_from_range(lub_ranges(R1, R2));
1063+
number_from_range(widen_range(lub_ranges(R1, R2)));
10701064
lub(#t_integer{elements=R1}, #t_number{elements=R2}) ->
1071-
number_from_range(lub_ranges(R1, R2));
1065+
number_from_range(widen_range(lub_ranges(R1, R2)));
10721066
lub(#t_list{type=TypeA,terminator=TermA},
10731067
#t_list{type=TypeB,terminator=TermB}) ->
10741068
#t_list{type=join(TypeA, TypeB),terminator=join(TermA, TermB)};
@@ -1081,11 +1075,11 @@ lub(nil, #t_list{}=T) ->
10811075
lub(#t_list{}=T, nil) ->
10821076
T;
10831077
lub(#t_number{elements=R1}, #t_number{elements=R2}) ->
1084-
number_from_range(lub_ranges(R1, R2));
1078+
number_from_range(widen_range(lub_ranges(R1, R2)));
10851079
lub(#t_number{elements=R1}, #t_integer{elements=R2}) ->
1086-
number_from_range(lub_ranges(R1, R2));
1080+
number_from_range(widen_range(lub_ranges(R1, R2)));
10871081
lub(#t_number{elements=R1}, #t_float{elements=R2}) ->
1088-
number_from_range(lub_ranges(R1, R2));
1082+
number_from_range(widen_range(lub_ranges(R1, R2)));
10891083
lub(#t_map{super_key=SKeyA,super_value=SValueA},
10901084
#t_map{super_key=SKeyB,super_value=SValueB}) ->
10911085
%% Note the use of join/2; elements don't need to be normal types.
@@ -1132,6 +1126,14 @@ lub_ranges({MinA,MaxA}, {MinB,MaxB}) ->
11321126
lub_ranges(_, _) ->
11331127
any.
11341128

1129+
%% Expands integer 0 to `-0.0 .. +0.0`
1130+
widen_range({Min, 0}) ->
1131+
widen_range({Min, +0.0});
1132+
widen_range({0, Max}) ->
1133+
widen_range({-0.0, Max});
1134+
widen_range(Other) ->
1135+
Other.
1136+
11351137
lub_bs_matchable(UnitA, UnitB) ->
11361138
#t_bs_matchable{tail_unit=gcd(UnitA, UnitB)}.
11371139

@@ -1179,12 +1181,13 @@ float_from_range(none) ->
11791181
none;
11801182
float_from_range(any) ->
11811183
#t_float{};
1182-
float_from_range({Min0,Max0}) ->
1183-
case {safe_float(Min0),safe_float(Max0)} of
1184+
float_from_range({Min0, Max0}) ->
1185+
true = inf_le(Min0, Max0), %Assertion.
1186+
case {safe_float(Min0), safe_float(Max0)} of
11841187
{'-inf','+inf'} ->
11851188
#t_float{};
1186-
{Min,Max} ->
1187-
#t_float{elements={Min,Max}}
1189+
{Min, Max} ->
1190+
#t_float{elements={Min, Max}}
11881191
end.
11891192

11901193
safe_float(N) when is_number(N) ->
@@ -1218,21 +1221,104 @@ number_from_range(N) ->
12181221
none
12191222
end.
12201223

1221-
inf_le('-inf', _) -> true;
1222-
inf_le(A, B) -> A =< B.
1223-
1224-
inf_ge(_, '-inf') -> true;
1225-
inf_ge('-inf', _) -> false;
1226-
inf_ge(A, B) -> A >= B.
1224+
inf_le('-inf', _) ->
1225+
true;
1226+
inf_le(A, B) when is_float(A), is_float(B) ->
1227+
%% When float ranges are compared to float ranges, the total ordering
1228+
%% function must be used to preserve `-0.0 =/= +0.0`.
1229+
float_comparable(A) =< float_comparable(B);
1230+
inf_le(A, B) ->
1231+
A =< B.
1232+
1233+
inf_ge(_, '-inf') ->
1234+
true;
1235+
inf_ge('-inf', _) ->
1236+
false;
1237+
inf_ge(A, B) when is_float(A), is_float(B) ->
1238+
float_comparable(A) >= float_comparable(B);
1239+
inf_ge(A, B) ->
1240+
A >= B.
1241+
1242+
inf_min(A, B) when A =:= '-inf'; B =:= '-inf' ->
1243+
'-inf';
1244+
inf_min(A, B) when is_float(A), is_float(B) ->
1245+
case float_comparable(A) =< float_comparable(B) of
1246+
true -> A;
1247+
false -> B
1248+
end;
1249+
inf_min(A, B) when A =< B ->
1250+
A;
1251+
inf_min(A, B) when A > B ->
1252+
B.
12271253

1228-
inf_min(A, B) when A =:= '-inf'; B =:= '-inf' -> '-inf';
1229-
inf_min(A, B) when A =< B -> A;
1230-
inf_min(A, B) when A > B -> B.
1254+
inf_max('-inf', B) ->
1255+
B;
1256+
inf_max(A, '-inf') ->
1257+
A;
1258+
inf_max(A, B) when is_float(A), is_float(B) ->
1259+
case float_comparable(A) >= float_comparable(B) of
1260+
true -> A;
1261+
false -> B
1262+
end;
1263+
inf_max(A, B) when A >= B ->
1264+
A;
1265+
inf_max(A, B) when A < B ->
1266+
B.
12311267

1232-
inf_max('-inf', B) -> B;
1233-
inf_max(A, '-inf') -> A;
1234-
inf_max(A, B) when A >= B -> A;
1235-
inf_max(A, B) when A < B -> B.
1268+
%% Converts a float to a number which, when compared with other such converted
1269+
%% floats, is ordered the same as '<' on the original inputs aside from the
1270+
%% fact that -0.0 < +0.0 as required by the term equivalence order.
1271+
%%
1272+
%% This has been proven correct with the SMT-LIB model below:
1273+
%%
1274+
%% (define-const SignBit_bv (_ BitVec 64) #x8000000000000000)
1275+
%%
1276+
%% ; Two finite floats X and Y of unknown value
1277+
%% (declare-const X (_ FloatingPoint 11 53))
1278+
%% (declare-const Y (_ FloatingPoint 11 53))
1279+
%% (assert (= false (fp.isInfinite X) (fp.isInfinite Y)
1280+
%% (fp.isNaN X) (fp.isNaN Y)))
1281+
%%
1282+
%% ; ... the bit representations of the aforementioned floats. The Z3 floating-
1283+
%% ; point extension lacks a way to directly bit-cast a vector to a float, so
1284+
%% ; we rely on equivalence here.
1285+
%% (declare-const X_bv (_ BitVec 64))
1286+
%% (declare-const Y_bv (_ BitVec 64))
1287+
%% (assert (= ((_ to_fp 11 53) X_bv) X))
1288+
%% (assert (= ((_ to_fp 11 53) Y_bv) Y))
1289+
%%
1290+
%% ; The bit hack we're going to test
1291+
%% (define-fun float_sortable ((value (_ BitVec 64))) (_ BitVec 64)
1292+
%% (ite (distinct (bvand value SignBit_bv) SignBit_bv)
1293+
%% (bvxor value SignBit_bv)
1294+
%% (bvnot value)))
1295+
%%
1296+
%% (define-fun float_bv_lt ((LHS (_ BitVec 64))
1297+
%% (RHS (_ BitVec 64))) Bool
1298+
%% (bvult (float_sortable LHS) (float_sortable RHS)))
1299+
%%
1300+
%% (push 1)
1301+
%% ; When either of X or Y are non-zero, (X < Y) = (bvX < bvY)
1302+
%% (assert (not (and (fp.isZero X) (fp.isZero Y))))
1303+
%% (assert (distinct (fp.lt X Y) (float_bv_lt X_bv Y_bv)))
1304+
%% (check-sat) ; unsat, proving by negation that the above always holds
1305+
%% (pop 1)
1306+
%%
1307+
%% (push 1)
1308+
%% ; Negative zero should sort lower than positive zero
1309+
%% (assert (and (fp.isNegative X) (fp.isPositive Y)
1310+
%% (fp.isZero X) (fp.isZero Y)))
1311+
%% (assert (not (float_bv_lt X_bv Y_bv)))
1312+
%% (check-sat) ; unsat
1313+
%% (pop 1)
1314+
float_comparable(V0) when is_float(V0) ->
1315+
Sign = 16#8000000000000000,
1316+
Mask = 16#FFFFFFFFFFFFFFFF,
1317+
<<V_bv:64/unsigned>> = <<V0/float>>,
1318+
case V_bv band Sign of
1319+
0 -> (V_bv bxor Sign) band Mask;
1320+
Sign -> (bnot V_bv) band Mask
1321+
end.
12361322

12371323
%%
12381324

‎lib/compiler/test/beam_type_SUITE.erl

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@
3131
switch_fail_inference/1,failures/1,
3232
cover_maps_functions/1,min_max_mixed_types/1,
3333
not_equal/1,infer_relops/1,binary_unit/1,premature_concretization/1,
34-
funs/1,will_succeed/1]).
34+
funs/1,will_succeed/1,float_confusion/1]).
3535

3636
%% Force id/1 to return 'any'.
3737
-export([id/1]).
@@ -1505,6 +1505,14 @@ will_succeed_1(_V0, _V1)
15051505
will_succeed_1(_, _) ->
15061506
b.
15071507

1508+
%% GH-7901: Range operations did not honor the total order of floats.
1509+
float_confusion(_Config) ->
1510+
ok = float_confusion_1(catch (true = ok), -0.0),
1511+
ok = float_confusion_1(ok, 0.0).
1512+
1513+
float_confusion_1(_, _) ->
1514+
ok.
1515+
15081516
%%%
15091517
%%% Common utilities.
15101518
%%%

0 commit comments

Comments
 (0)