8000 Eliminate internal consistency failure by bjorng · Pull Request #6189 · erlang/otp · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Eliminate internal consistency failure #6189

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Aug 3, 2022
Merged

Eliminate internal consistency failure #6189

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
113 changes: 55 additions & 58 deletions lib/compiler/src/beam_ssa_type.erl
View file
Open in desktop
10000
Original file line number Diff line number Diff line change
Expand Up @@ -2414,27 +2414,56 @@ infer_types_br_1(V, Ts, Ds) ->

case inv_relop(Op0) of
none ->
%% No a relation operator.
%% Not a relational operator.
{PosTypes, NegTypes} = infer_type(Op0, Args, Ts, Ds),
SuccTs = meet_types(PosTypes, Ts),
FailTs = subtract_types(NegTypes, Ts),
FailTs = infer_subtract_types(NegTypes, Ts),
{SuccTs, FailTs};
InvOp ->
%% This is an relational operator.
{bif,Op} = Op0,

%% Infer the types for both sides for operator succceding
%% Infer the types for both sides of operator succceding.
Types = concrete_types(Args, Ts),
TrueTypes0 = infer_relop(Op, Args, Types),
TrueTypes0 = infer_relop(Op, Args, Types, Ds),
TrueTypes = meet_types(TrueTypes0, Ts),

%% Infer the types for both sides operator failing.
FalseTypes0 = infer_relop(InvOp, Args, Types),
%% Infer the types for both sides of operator failing.
FalseTypes0 = infer_relop(InvOp, Args, Types, Ds),
FalseTypes = meet_types(FalseTypes0, Ts),

{TrueTypes, FalseTypes}
end.

infer_relop('=:=', [LHS,RHS], [LType,RType], Ds) ->
EqTypes = infer_eq_type(map_get(LHS, Ds), RType),

%% As an example, assume that L1 is known to be 'list', and L2 is
%% known to be 'cons'. Then if 'L1 =:= L2' evaluates to 'true', it
%% can be inferred that L1 is 'cons' (the meet of 'cons' and
%% 'list').
Type = beam_types:meet(LType, RType),
Types = [{LHS,Type},{RHS,Type}],
[{V,T} || {#b_var{}=V,T} <- Types, T =/= any] ++ EqTypes;
infer_relop(Op, Args, Types, _Ds) ->
infer_relop(Op, Args, Types).

infer_relop('=/=', [LHS,RHS], [LType,RType]) ->
%% We must be careful with types inferred from '=/='.
%%
%% For example, if we have L =/= [a], we must not subtract 'cons'
%% from the type of L. In general, subtraction is only safe if
%% the type being subtracted is singled-valued, for example if it
%% is [] or the the atom 'true'.
%%
%% Note that we subtract the left-hand type from the right-hand
%% value and vice versa. We must not subtract the meet of the two
%% as it may be too specific. See beam_type_SUITE:type_subtraction/1
%% for details.
[{V,beam_types:subtract(ThisType, OtherType)} ||
{#b_var{}=V, ThisType, OtherType} <-
[{RHS, RType, LType}, {LHS, LType, RType}],
beam_types:is_singleton_type(OtherType)];
infer_relop(Op, [Arg1,Arg2], Types0) ->
case infer_relop(Op, Types0) of
any ->
Expand Down Expand Up @@ -2512,12 +2541,29 @@ inv_relop_1('<') -> '>=';
inv_relop_1('=<') -> '>';
inv_relop_1('>=') -> '<';
inv_relop_1('>') -> '=<';
inv_relop_1('=:=') -> '=/=';
inv_relop_1('=/=') -> '=:=';
inv_relop_1(_) -> none.

infer_get_range(#t_integer{elements=R}) -> R;
infer_get_range(#t_number{elements=R}) -> R;
infer_get_range(_) -> unknown.

infer_subtract_types([{V,T0}|Vs], Ts) ->
T1 = concrete_type(V, Ts),
case beam_types:subtract(T1, T0) of
T1 ->
infer_subtract_types(Vs, Ts);
T ->
%% We only do this subtraction for type tests whose
%% outcome is unknown. The outcome would have been known
%% (false) if type subtraction produced 'none'.
true = T =/= none, %Assertion.
infer_subtract_types(Vs, Ts#{V := T})
end;
infer_subtract_types([], Ts) ->
Ts.

infer_br_value(_V, _Bool, none) ->
none;
infer_br_value(V, Bool, NewTs) ->
Expand All @@ -2531,7 +2577,9 @@ infer_br_value(V, Bool, NewTs) ->
end.

infer_types_switch(V, Lit, Ts0, IsTempVar, Ds) ->
{PosTypes, _} = infer_type({bif,'=:='}, [V, Lit], Ts0, Ds),
Args = [V,Lit],
Types = concrete_types(Args, Ts0),
PosTypes = infer_relop('=:=', Args, Types, Ds),
Ts = meet_types(PosTypes, Ts0),
case IsTempVar of
true -> ts_remove_var(V, Ts);
Expand Down Expand Up @@ -2610,47 +2658,6 @@ infer_type({bif,is_reference}, [#b_var{}=Arg], _Ts, _Ds) ->
infer_type({bif,is_tuple}, [#b_var{}=Arg], _Ts, _Ds) ->
T = {Arg, #t_tuple{}},
{[T], [T]};
infer_type({bif,'=:='}, [#b_var{}=LHS,#b_var{}=RHS], Ts, _Ds) ->
%% As an example, assume that L1 is known to be 'list', and L2 is
%% known to be 'cons'. Then if 'L1 =:= L2' evaluates to 'true', it can
%% be inferred that L1 is 'cons' (the meet of 'cons' and 'list').
LType = concrete_type(LHS, Ts),
RType = concrete_type(RHS, Ts),
Type = beam_types:meet(LType, RType),

PosTypes = [{V,Type} || {V, OrigType} <- [{LHS, LType}, {RHS, RType}],
OrigType =/= Type],

%% We must be careful with types inferred from '=:='.
%%
%% If we have seen L =:= [a], we know that L is 'cons' if the
%% comparison succeeds. However, if the comparison fails, L could
%% still be 'cons'. Therefore, we must not subtract 'cons' from the
%% previous type of L.
%%
%% However, it is safe to subtract a type inferred from '=:=' if
%% it is single-valued, e.g. if it is [] or the atom 'true'.
%%
%% Note that we subtract the left-hand type from the right-hand
%% value and vice versa. We must not subtract the meet of the two
%% as it may be too specific. See beam_type_SUITE:type_subtraction/1
%% for details.
NegTypes = [T || {_, OtherType}=T <- [{RHS, LType}, {LHS, RType}],
beam_types:is_singleton_type(OtherType)],

{PosTypes, NegTypes};
infer_type({bif,'=:='}, [#b_var{}=Src,#b_literal{}=Lit], Ts, Ds) ->
Def = maps:get(Src, Ds),
LitType = concrete_type(Lit, Ts),
PosTypes = [{Src, LitType} | infer_eq_type(Def, LitType)],

%% Subtraction is only safe if LitType is single-valued.
NegTypes = case beam_types:is_singleton_type(LitType) of
true -> PosTypes;
false -> []
end,

{PosTypes, NegTypes};
infer_type(_Op, _Args, _Ts, _Ds) ->
{[], []}.

Expand Down Expand Up @@ -2742,16 +2749,6 @@ meet_types([{V,T0}|Vs], Ts) ->
meet_types([], Ts) ->
Ts.

subtract_types([{V,T0}|Vs], Ts) ->
T1 = concrete_type(V, Ts),
case beam_types:subtract(T1, T0) of
none -> none;
T1 -> subtract_types(Vs, Ts);
T -> subtract_types(Vs, Ts#{ V:= T })
end;
subtract_types([], Ts) ->
Ts.

parallel_join([A | As], [B | Bs]) ->
[beam_types:join(A, B) | parallel_join(As, Bs)];
parallel_join([], []) ->
Expand Down
33 changes: 33 additions & 0 deletions lib/compiler/src/beam_types.erl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -342,6 +342,39 @@ subtract(any, #t_number{elements={'-inf',Max}}) ->
number=#t_number{elements={Max,'+inf'}},
tuple_set=#t_tuple{},
other=other};
subtract(any, nil) ->
%%
%% We handle this subtraction mainly for correctness. Consider:
%%
%% foobar(L) when L =/= [], is_list(L), L =/= [], hd(L) -> ok.
%%
%% The type-based optimizations would rewrite the hd/1 BIF call to
%% a get_hd instruction:
%%
%% foobar(L) when L =/= [], is_list(L), L =/= [], get_hd(L) -> ok.
%%
%% The beam_ssa_dead pass would later remove the redundant second
%% test of `L =/= []`:
%%
%% foobar(L) when L =/= [], is_list(L), get_hd(L) -> ok.
%%
%% With that test removed, the type for L in the get_hd instruction
%% would be #t_list{} instead of the required #t_cons{} and that
%% would trigger an assertion. (If the assertion were to be removed,
%% beam_validator would complain instead.)
%%
%% By letting the type subtraction of `any` by `nil` return a
%% union, the optimized code above becomes legal. As an added bonus,
%% the is_list/1 guard test can be replaced with the cheaper
%% is_nonempty_list instruction:
%%
%% foobar(L) when L =/= [], is_nonempty_list(L), get_hd(L) -> ok.
%%
#t_union{atom=#t_atom{},
list=#t_cons{},
number=#t_number{},
tuple_set=#t_tuple{},
other=other};
subtract(#t_atom{elements=[_|_]=Set0}, #t_atom{elements=[_|_]=Set1}) ->
case ordsets:subtract(Set0, Set1) of
[] -> none;
Expand Down
24 changes: 22 additions & 2 deletions lib/compiler/test/beam_type_SUITE.erl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,8 @@
none_argument/1,success_type_oscillation/1,type_subtraction/1,
container_subtraction/1,is_list_opt/1,connected_tuple_elements/1,
switch_fail_inference/1,failures/1,
cover_maps_functions/1,min_max_mixed_types/1]).
cover_maps_functions/1,min_max_mixed_types/1,
not_equal/1]).

%% Force id/1 to return 'any'.
-export([id/1]).
Expand Down Expand Up @@ -66,7 +67,8 @@ groups() ->
switch_fail_inference,
failures,
cover_maps_functions,
min_max_mixed_types
min_max_mixed_types,
not_equal
]}].

init_per_suite(Config) ->
Expand Down Expand Up @@ -1138,5 +1140,23 @@ min_max_mixed_types(_Config) ->

ok.

%% GH-6183. beam_validator had a stronger type analysis for '=/=' and
%% is_ne_exact than the beam_ssa_type pass. It would figure out that
%% at the time the comparison 'a /= V' was evaluated, V must be equal
%% to 'true' and the comparison would therefore always return 'false'.
%% beam_validator would report that as a type conflict.

not_equal(_Config) ->
true = do_not_equal(true),
{'EXIT',{function_clause,_}} = catch do_not_equal(false),
{'EXIT',{function_clause,_}} = catch do_not_equal(0),
{'EXIT',{function_clause,_}} = catch do_not_equal(42),
{'EXIT',{function_clause,_}} = catch do_not_equal(self()),

ok.

do_not_equal(V) when (V / V < (V orelse true)); V; V ->
(V = (a /= V)) orelse 0.

id(I) ->
I.
0