From 3379f7c39aa92cec5481a308a01cd6f211fa5698 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?John=20H=C3=B6gberg?= Date: Tue, 11 Jul 2023 09:24:43 +0200 Subject: [PATCH] beam_ssa_type: Fix bugs relating to subtraction in type inference Fixes #7488 --- lib/compiler/src/beam_ssa_type.erl | 85 +++++++++++++++++++-------- lib/compiler/test/beam_type_SUITE.erl | 43 ++++++++++++++ 2 files changed, 104 insertions(+), 24 deletions(-) diff --git a/lib/compiler/src/beam_ssa_type.erl b/lib/compiler/src/beam_ssa_type.erl index 8fcb25273311..d492ed4b50a4 100644 --- a/lib/compiler/src/beam_ssa_type.erl +++ b/lib/compiler/src/beam_ssa_type.erl @@ -26,6 +26,7 @@ %% it goes. %% +-feature(maybe_expr, enable). -module(beam_ssa_type). -export([opt_start/2, opt_continue/4, opt_finish/3, opt_ranges/1]). @@ -2497,17 +2498,27 @@ infer_types_br_1(V, Ts, Ds) -> FailTs = subtract_types(NegTypes, Ts), {SuccTs, FailTs}; InvOp -> - %% This is an relational operator. + %% This is a relational operator. {bif,Op} = Op0, - %% Infer the types for both sides of operator succceding. + %% Infer the types for both sides of operator succeeding. Types = concrete_types(Args, Ts), - TrueTypes0 = infer_relop(Op, Args, Types, Ds), - TrueTypes = meet_types(TrueTypes0, Ts), + {TruePos, TrueNeg} = infer_relop(Op, Args, Types, Ds), + TrueTypes = maybe + TrueTypes0 = #{} ?= meet_types(TruePos, Ts), + subtract_types(TrueNeg, TrueTypes0) + else + none -> none + end, %% Infer the types for both sides of operator failing. - FalseTypes0 = infer_relop(InvOp, Args, Types, Ds), - FalseTypes = meet_types(FalseTypes0, Ts), + {FalsePos, FalseNeg} = infer_relop(InvOp, Args, Types, Ds), + FalseTypes = maybe + FalseTypes0 = #{} ?= meet_types(FalsePos, Ts), + subtract_types(FalseNeg, FalseTypes0) + else + none -> none + end, {TrueTypes, FalseTypes} end. @@ -2524,12 +2535,12 @@ infer_relop('=:=', [LHS,RHS], %% In order to avoid narrowing the types with regard to %% appendable-status, deduce the types for the case when neither %% LHS or RHS are appendable, then restore the appendable-status. - [{LHS,LType},{RHS,RType}|EqTypes] = + {[{LHS,LType},{RHS,RType} | EqTypes], []} = infer_relop('=:=', [LHS,RHS], [LType0#t_bitstring{appendable=false}, RType0#t_bitstring{appendable=false}], Ds), - [{LHS,LType#t_bitstring{appendable=LHSApp}}, - {RHS,RType#t_bitstring{appendable=RHSApp}}|EqTypes]; + {[{LHS,LType#t_bitstring{appendable=LHSApp}}, + {RHS,RType#t_bitstring{appendable=RHSApp}} | EqTypes], []}; infer_relop('=:=', [LHS,RHS], [LType,RType], Ds) -> EqTypes = infer_eq_type(map_get(LHS, Ds), RType), @@ -2538,11 +2549,10 @@ infer_relop('=:=', [LHS,RHS], [LType,RType], Ds) -> %% can be inferred that L1 is 'cons' (the meet of 'cons' and %% 'list'). Type = beam_types:meet(LType, RType), - [{LHS,Type},{RHS,Type}] ++ EqTypes; -infer_relop(Op, Args, Types, _Ds) -> - infer_relop(Op, Args, Types). + {[{LHS,Type},{RHS,Type}] ++ EqTypes, []}; +infer_relop('=/=', [LHS,RHS], [LType,RType], Ds) -> + NeTypes = infer_ne_type(map_get(LHS, Ds), RType), -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' @@ -2554,9 +2564,12 @@ infer_relop('=/=', [LHS,RHS], [LType,RType]) -> %% 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)} || - {V, ThisType, OtherType} <- [{RHS, RType, LType}, {LHS, LType, RType}], - beam_types:is_singleton_type(OtherType)]; + {[{V,beam_types:subtract(ThisType, OtherType)} || + {V, ThisType, OtherType} <- [{RHS, RType, LType}, {LHS, LType, RType}], + beam_types:is_singleton_type(OtherType)], NeTypes}; +infer_relop(Op, Args, Types, _Ds) -> + {infer_relop(Op, Args, Types), []}. + infer_relop(Op, [Arg1,Arg2], Types0) -> case infer_relop(Op, Types0) of any -> @@ -2659,8 +2672,13 @@ infer_br_value(V, Bool, NewTs) -> infer_types_switch(V, Lit, Ts0, IsTempVar, Ds) -> Args = [V,Lit], Types = concrete_types(Args, Ts0), - PosTypes = infer_relop('=:=', Args, Types, Ds), - Ts = meet_types(PosTypes, Ts0), + {PosTypes, NegTypes} = infer_relop('=:=', Args, Types, Ds), + Ts = maybe + Ts1 = #{} ?= meet_types(PosTypes, Ts0), + subtract_types(NegTypes, Ts1) + else + none -> none + end, case IsTempVar of true -> ts_remove_var(V, Ts); false -> Ts @@ -2744,15 +2762,15 @@ infer_type({bif,'and'}, [#b_var{}=LHS,#b_var{}=RHS], Ts, Ds) -> %% rewrite this BIF to plain control flow. %% %% Note that we can't do anything for the 'false' case as either (or both) - %% of the arguments could be false. + %% of the arguments could be false, so we must ignore the negations. #{ LHS := #b_set{op=LHSOp,args=LHSArgs}, RHS := #b_set{op=RHSOp,args=RHSArgs} } = Ds, - LHSTypes = infer_and_type(LHSOp, LHSArgs, Ts, Ds), - RHSTypes = infer_and_type(RHSOp, RHSArgs, Ts, Ds), + {LHSPos, _} = infer_and_type(LHSOp, LHSArgs, Ts, Ds), + {RHSPos, _} = infer_and_type(RHSOp, RHSArgs, Ts, Ds), True = beam_types:make_atom(true), - {[{LHS, True}, {RHS, True}] ++ LHSTypes ++ RHSTypes, []}; + {[{LHS, True}, {RHS, True}] ++ LHSPos ++ RHSPos, []}; infer_type(_Op, _Args, _Ts, _Ds) -> {[], []}. @@ -2801,11 +2819,30 @@ infer_eq_type(#b_set{op=get_tuple_element, infer_eq_type(_, _) -> []. +infer_ne_type(#b_set{op={bif,tuple_size},args=[#b_var{}=Tuple]}, + #t_integer{elements={Size,Size}}) -> + [{Tuple,#t_tuple{exact=true,size=Size}}]; +infer_ne_type(#b_set{op=get_tuple_element, + args=[#b_var{}=Tuple,#b_literal{val=N}]}, + ElementType) -> + Index = N + 1, + case {beam_types:is_singleton_type(ElementType), + beam_types:set_tuple_element(Index, ElementType, #{})} of + {true, #{ Index := _ }=Es} -> + [{Tuple,#t_tuple{size=Index,elements=Es}}]; + {_, #{}} -> + %% Subtraction is not safe: either we had a non-singleton element + %% type (see inference for `=/=`), or the element index was out of + %% range. + [] + end; +infer_ne_type(_, _) -> + []. + infer_and_type(Op, Args, Ts, Ds) -> case inv_relop(Op) of none -> - {LHSTypes0, _} = infer_type(Op, Args, Ts, Ds), - LHSTypes0; + infer_type(Op, Args, Ts, Ds); _InvOp -> {bif,RelOp} = Op, infer_relop(RelOp, Args, concrete_types(Args, Ts), Ds) diff --git a/lib/compiler/test/beam_type_SUITE.erl b/lib/compiler/test/beam_type_SUITE.erl index 94f1b8b0a6f6..97b396f2bbb8 100644 --- a/lib/compiler/test/beam_type_SUITE.erl +++ b/lib/compiler/test/beam_type_SUITE.erl @@ -1047,8 +1047,16 @@ sto_1(step_4_3) -> {b, [sto_1(case_3_3)]}. %% 3, so we must not subtract 2 on the failure path. type_subtraction(Config) when is_list(Config) -> true = type_subtraction_1(id(<<"A">>)), + + ok = type_subtraction_2(id(true)), + <<"aaaa">> = type_subtraction_2(id(false)), + {'EXIT', _} = catch type_subtraction_3(id(false)), + ok = catch type_subtraction_4(id(ok)), + {'EXIT', _} = catch type_subtraction_4(id(false)), + ok. + type_subtraction_1(_x@1) -> _a@1 = ts_12(_x@1), _b@1 = ts_23(_x@1), @@ -1073,6 +1081,41 @@ ts_23(_x@1) -> 2 end. +type_subtraction_2(X) -> + case ts_34(X) of + Tuple when element(1, Tuple) =:= ok -> + ok; + Tuple when element(1, Tuple) =:= error -> + element(2, Tuple) + end. + +ts_34(X) -> + case X of + true -> {ok}; + false -> {error, <<"aaaa">>} + end. + +type_subtraction_3(_V0) when is_boolean(_V0), is_binary(_V0), _V0 andalso _V0 -> + ok. + +type_subtraction_4(_V0) -> + try + _V0 = ok + catch + _ -> + << + 0 + || _V0 := _ <- ok, + (try ok of + _ when _V0, (_V0 andalso _V0) orelse trunc(ok) -> + ok + catch + _ -> + ok + end) + >> + end. + %% GH-4774: The validator didn't update container contents on type subtraction. container_subtraction(Config) when is_list(Config) -> A = id(baz),