beam_ssa_type: Fix bugs relating to subtraction in type inference

Fixes #7488

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)

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),