beam_validator: Improve type inference on inequality

Both sides need to be inferred, and we should infer as if we've
made an exact match when we know that LHS is single-valued. This
was done for select_val, but we failed to do so for is_ne_exact
et al.

2 files changed, 48 insertions, 25 deletions

diff --git a/lib/compiler/src/beam_validator.erl b/lib/compiler/src/beam_validator.erl
index a2e4707758..abc3aa3875 100644
--- a/lib/compiler/src/beam_validator.erl
+++ b/lib/compiler/src/beam_validator.erl
@@ -1531,21 +1531,8 @@ validate_select_val(Fail, [Val,{f,L}|T], Src, Vst0) ->
                          update_ne_types(Src, Val, FailVst)
                  end),
     validate_select_val(Fail, T, Src, Vst);
-validate_select_val(Fail, [], Src, Vst) ->
+validate_select_val(Fail, [], _Src, Vst) ->
     branch(Fail, Vst,
-           fun(FailVst) ->
-                    FailType = get_term_type(Src, FailVst),
-                    case beam_types:get_singleton_value(FailType) of
-                       {ok, Value} ->
-                           %% This is the only possible value at the fail
-                           %% label, so we can infer types as if we matched it
-                           %% directly.
-                           Lit = value_to_literal(Value),
-                           update_eq_types(Src, Lit, FailVst);
-                       error ->
-                           FailVst
-                   end
-           end,
            fun(SuccVst) ->
                    %% The next instruction is never executed.
                    kill_state(SuccVst)
@@ -1793,17 +1780,21 @@ update_type(Merge, With, Literal, Vst) ->
     end.
 
 update_eq_types(LHS, RHS, Vst0) ->
-    Vst1 = infer_types(eq_exact, LHS, RHS, Vst0),
+    LType = get_term_type(LHS, Vst0),
+    RType = get_term_type(RHS, Vst0),
 
-    T1 = get_term_type(LHS, Vst1),
-    T2 = get_term_type(RHS, Vst1),
+    Vst1 = update_type(fun meet/2, RType, LHS, Vst0),
+    Vst = update_type(fun meet/2, LType, RHS, Vst1),
 
-    Vst = update_type(fun meet/2, T2, LHS, Vst1),
-    update_type(fun meet/2, T1, RHS, Vst).
+    infer_types(eq_exact, LHS, RHS, Vst).
 
 update_ne_types(LHS, RHS, Vst0) ->
-    Vst = infer_types(ne_exact, LHS, RHS, Vst0),
+    Vst1 = update_ne_types_1(LHS, RHS, Vst0),
+    Vst = update_ne_types_1(RHS, LHS, Vst1),
+
+    infer_types(ne_exact, LHS, RHS, Vst).
 
+update_ne_types_1(LHS, RHS, Vst0) ->
     %% While updating types on equality is fairly straightforward, inequality
     %% is a bit trickier since all we know is that the *value* of LHS differs
     %% from RHS, so we can't blindly subtract their types.
@@ -1813,10 +1804,23 @@ update_ne_types(LHS, RHS, Vst0) ->
     %% #t_integer{} we would erroneously infer that the new type is float.
     %%
     %% Therefore, we only subtract when we know that RHS has a specific value.
-    RType = get_term_type(RHS, Vst),
+    RType = get_term_type(RHS, Vst0),
     case beam_types:is_singleton_type(RType) of
-        true -> update_type(fun subtract/2, RType, LHS, Vst);
-        false -> Vst
+        true ->
+            Vst = update_type(fun subtract/2, RType, LHS, Vst0),
+
+            %% If LHS has a specific value after subtraction we can infer types
+            %% as if we've made an exact match, which is much stronger than
+            %% ne_exact.
+            LType = get_term_type(LHS, Vst),
+            case beam_types:get_singleton_value(LType) of
+                {ok, Value} ->
+                    infer_types(eq_exact, LHS, value_to_literal(Value), Vst);
+                error ->
+                    Vst
+            end;
+        false ->
+            Vst0
     end.
 
 %% Helper functions for the above.
diff --git a/lib/compiler/test/beam_validator_SUITE.erl b/lib/compiler/test/beam_validator_SUITE.erl
index d49d5af9c3..326ad9042f 100644
--- a/lib/compiler/test/beam_validator_SUITE.erl
+++ b/lib/compiler/test/beam_validator_SUITE.erl
@@ -35,7 +35,7 @@
 	 map_field_lists/1,cover_bin_opt/1,
 	 val_dsetel/1,bad_tuples/1,bad_try_catch_nesting/1,
          receive_stacked/1,aliased_types/1,type_conflict/1,
-         infer_on_eq/1,infer_dead_value/1]).
+         infer_on_eq/1,infer_dead_value/1,infer_on_ne/1]).
 
 -include_lib("common_test/include/ct.hrl").
 
@@ -65,7 +65,7 @@ groups() ->
        map_field_lists,cover_bin_opt,val_dsetel,
        bad_tuples,bad_try_catch_nesting,
        receive_stacked,aliased_types,type_conflict,
-       infer_on_eq,infer_dead_value]}].
+       infer_on_eq,infer_dead_value,infer_on_ne]}].
 
 init_per_suite(Config) ->
     test_lib:recompile(?MODULE),
@@ -700,6 +700,25 @@ idv_1({_A, _B, _C, _D, _E, F, G},
 idv_1(_A, _B) ->
     error.
 
+%% ERL-998; type inference for select_val (#b_switch{}) was more clever than
+%% that for is_ne_exact (#b_br{}), sometimes failing validation when the type
+%% optimization pass acted on the former and the validator got the latter.
+
+-record(ion, {state}).
+
+infer_on_ne(Config) when is_list(Config) ->
+    #ion{state = closing} = ion_1(#ion{ state = id(open) }),
+    #ion{state = closing} = ion_close(#ion{ state = open }),
+    ok.
+
+ion_1(State = #ion{state = open}) -> ion_2(State);
+ion_1(State = #ion{state = closing}) -> ion_2(State).
+
+ion_2(State = #ion{state = open}) -> ion_close(State);
+ion_2(#ion{state = closing}) -> ok.
+
+ion_close(State = #ion{}) -> State#ion{state = closing}.
+
 %%%-------------------------------------------------------------------------
 
 transform_remove(Remove, Module) ->