Merge branch 'hb/dialyzer/guard_constr/OTP-11798'

* hb/dialyzer/guard_constr/OTP-11798:
  dialyzer: generalize guard constraints in a new way

5 files changed, 174 insertions, 33 deletions

diff --git a/lib/dialyzer/src/dialyzer_contracts.erl b/lib/dialyzer/src/dialyzer_contracts.erl
index 46eaeaa303..283031eb9a 100644
--- a/lib/dialyzer/src/dialyzer_contracts.erl
+++ b/lib/dialyzer/src/dialyzer_contracts.erl
@@ -20,6 +20,8 @@
 
 -module(dialyzer_contracts).
 
+-compile(export_all).
+
 -export([check_contract/2,
 	 check_contracts/4,
 	 contracts_without_fun/3,
@@ -439,7 +441,8 @@ contract_from_form([], _RecDict, _FileLine, TypeAcc, FormAcc) ->
   {lists:reverse(TypeAcc), lists:reverse(FormAcc)}.
 
 process_constraints(Constrs, RecDict, ExpTypes, AllRecords) ->
-  Init = initialize_constraints(Constrs, RecDict, ExpTypes, AllRecords),
+  Init0 = initialize_constraints(Constrs, RecDict, ExpTypes, AllRecords),
+  Init = remove_cycles(Init0),
   constraints_fixpoint(Init, RecDict, ExpTypes, AllRecords).
 
 initialize_constraints(Constrs, RecDict, ExpTypes, AllRecords) ->
@@ -479,12 +482,9 @@ constraints_fixpoint(OldVarDict, Constrs, RecDict, ExpTypes, AllRecords) ->
       constraints_fixpoint(NewVarDict, Constrs, RecDict, ExpTypes, AllRecords)
   end.
 
--define(TYPE_LIMIT, 4).
-
 final_form(Form, RecDict, ExpTypes, AllRecords, VarDict) ->
   T1 = erl_types:t_from_form(Form, RecDict, VarDict),
-  T2 = erl_types:t_solve_remote(T1, ExpTypes, AllRecords),
-  erl_types:t_limit(T2, ?TYPE_LIMIT).
+  erl_types:t_solve_remote(T1, ExpTypes, AllRecords).
 
 constraints_to_dict(Constrs, RecDict, ExpTypes, AllRecords, VarDict) ->
   Subtypes =
@@ -499,6 +499,74 @@ constraints_to_subs([C|Rest], RecDict, ExpTypes, AllRecords, VarDict, Acc) ->
   NewAcc = [{subtype, T1, T2}|Acc],
   constraints_to_subs(Rest, RecDict, ExpTypes, AllRecords, VarDict, NewAcc).
 
+%% Replaces variables with '_' when necessary to break up cycles among
+%% the constraints.
+
+remove_cycles(Constrs0) ->
+  Uses = find_uses(Constrs0),
+  G = digraph:new(),
+  Vs0 = [V || {V, _} <- Uses] ++ [V || {_, V} <- Uses],
+  Vs = lists:usort(Vs0),
+  lists:foreach(fun(V) -> _ = digraph:add_vertex(G, V) end, Vs),
+  lists:foreach(fun({From, To}) ->
+                    _ = digraph:add_edge(G, {From, To}, From, To, [])
+                end, Uses),
+  ok = remove_cycles(G, Vs),
+  ToRemove = ordsets:subtract(ordsets:from_list(Uses),
+                              ordsets:from_list(digraph:edges(G))),
+  Constrs = remove_uses(ToRemove, Constrs0),
+  digraph:delete(G),
+  Constrs.
+
+find_uses([{Var, Form}|Constrs]) ->
+  UsedVars = form_vars(Form, []),
+  VarName = erl_types:t_var_name(Var),
+  [{VarName, UsedVar} || UsedVar <- UsedVars] ++ find_uses(Constrs);
+find_uses([]) ->
+  [].
+
+form_vars({var, _, '_'}, Vs) -> Vs;
+form_vars({var, _, V}, Vs) -> [V|Vs];
+form_vars(T, Vs) when is_tuple(T) ->
+  form_vars(tuple_to_list(T), Vs);
+form_vars([E|Es], Vs) ->
+  form_vars(Es, form_vars(E, Vs));
+form_vars(_, Vs) -> Vs.
+
+remove_cycles(G, Vs) ->
+  NumberOfEdges = digraph:no_edges(G),
+  lists:foreach(fun(V) ->
+                        case digraph:get_cycle(G, V) of
+                          false -> true;
+                          [V] -> digraph:del_edge(G, {V, V});
+                          [V, V1|_] -> digraph:del_edge(G, {V, V1})
+                        end
+                    end, Vs),
+  case digraph:no_edges(G) =:= NumberOfEdges of
+    true -> ok;
+    false -> remove_cycles(G, Vs)
+  end.
+
+remove_uses([], Constrs) -> Constrs;
+remove_uses([{Var, Use}|ToRemove], Constrs0) ->
+  Constrs = remove_uses(Var, Use, Constrs0),
+  remove_uses(ToRemove, Constrs).
+
+remove_uses(_Var, _Use, []) -> [];
+remove_uses(Var, Use, [Constr|Constrs]) ->
+  {V, Form} = Constr,
+  case erl_types:t_var_name(V) =:= Var of
+    true -> [{V, remove_use(Form, Use)}|Constrs];
+    false -> [Constr|remove_uses(Var, Use, Constrs)]
+  end.
+
+remove_use({var, L, V}, V) -> {var, L, '_'};
+remove_use(T, V) when is_tuple(T) ->
+  list_to_tuple(remove_use(tuple_to_list(T), V));
+remove_use([E|Es], V) ->
+  [remove_use(E, V)|remove_use(Es, V)];
+remove_use(T, _V) -> T.
+
 %% Gets the most general domain of a list of domains of all
 %% the overloaded contracts
 
diff --git a/lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes b/lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes
index bfa33cd296..fbdd182358 100644
--- a/lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes
+++ b/lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes
@@ -1,27 +1,28 @@
 
 contracts_with_subtypes.erl:106: The call contracts_with_subtypes:rec_arg({'a','b'}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
 contracts_with_subtypes.erl:107: The call contracts_with_subtypes:rec_arg({'b','a'}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
-contracts_with_subtypes.erl:108: The call contracts_with_subtypes:rec_arg({'a',{'b','a'}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
 contracts_with_subtypes.erl:109: The call contracts_with_subtypes:rec_arg({'b',{'a','b'}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
-contracts_with_subtypes.erl:110: The call contracts_with_subtypes:rec_arg({'a',{'b',{'a','b'}}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
-contracts_with_subtypes.erl:111: The call contracts_with_subtypes:rec_arg({'b',{'a',{'b','a'}}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
-contracts_with_subtypes.erl:142: The pattern 1 can never match the type string()
-contracts_with_subtypes.erl:145: The pattern 'alpha' can never match the type {'ok',_} | {'ok',_,string()}
-contracts_with_subtypes.erl:147: The pattern 42 can never match the type {'ok',_} | {'ok',_,string()}
-contracts_with_subtypes.erl:163: The pattern 'alpha' can never match the type {'ok',_}
-contracts_with_subtypes.erl:165: The pattern 42 can never match the type {'ok',_}
-contracts_with_subtypes.erl:183: The pattern 'alpha' can never match the type {'ok',_}
-contracts_with_subtypes.erl:185: The pattern 42 can never match the type {'ok',_}
-contracts_with_subtypes.erl:202: The pattern 1 can never match the type string()
-contracts_with_subtypes.erl:205: The pattern {'ok', _} can never match the type {'ok',_,string()}
-contracts_with_subtypes.erl:206: The pattern 'alpha' can never match the type {'ok',_,string()}
-contracts_with_subtypes.erl:207: The pattern {'ok', 42} can never match the type {'ok',_,string()}
-contracts_with_subtypes.erl:208: The pattern 42 can never match the type {'ok',_,string()}
-contracts_with_subtypes.erl:234: Function flat_ets_new_t/0 has no local return
-contracts_with_subtypes.erl:235: The call contracts_with_subtypes:flat_ets_new(12,[]) breaks the contract (Name,Options) -> atom() when is_subtype(Name,atom()), is_subtype(Options,[Option]), is_subtype(Option,'set' | 'ordered_set' | 'bag' | 'duplicate_bag' | 'public' | 'protected' | 'private' | 'named_table' | {'keypos',integer()} | {'heir',pid(),term()} | {'heir','none'} | {'write_concurrency',boolean()} | {'read_concurrency',boolean()} | 'compressed')
+contracts_with_subtypes.erl:135: The call contracts_with_subtypes:rec2({'a','b'}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,ab())
+contracts_with_subtypes.erl:136: The call contracts_with_subtypes:rec2({'b','a'}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,ab())
+contracts_with_subtypes.erl:137: The call contracts_with_subtypes:rec2({'a',{'b','a'}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,ab())
+contracts_with_subtypes.erl:138: The call contracts_with_subtypes:rec2({'b',{'a','b'}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,ab())
+contracts_with_subtypes.erl:171: The pattern 1 can never match the type string()
+contracts_with_subtypes.erl:174: The pattern 'alpha' can never match the type {'ok',_} | {'ok',_,string()}
+contracts_with_subtypes.erl:176: The pattern 42 can never match the type {'ok',_} | {'ok',_,string()}
+contracts_with_subtypes.erl:192: The pattern 'alpha' can never match the type {'ok',_}
+contracts_with_subtypes.erl:194: The pattern 42 can never match the type {'ok',_}
+contracts_with_subtypes.erl:212: The pattern 'alpha' can never match the type {'ok',_}
+contracts_with_subtypes.erl:214: The pattern 42 can never match the type {'ok',_}
+contracts_with_subtypes.erl:231: The pattern 1 can never match the type string()
+contracts_with_subtypes.erl:234: The pattern {'ok', _} can never match the type {'ok',_,string()}
+contracts_with_subtypes.erl:235: The pattern 'alpha' can never match the type {'ok',_,string()}
+contracts_with_subtypes.erl:236: The pattern {'ok', 42} can never match the type {'ok',_,string()}
+contracts_with_subtypes.erl:237: The pattern 42 can never match the type {'ok',_,string()}
 contracts_with_subtypes.erl:23: Invalid type specification for function contracts_with_subtypes:extract2/0. The success typing is () -> 'something'
-contracts_with_subtypes.erl:261: Function factored_ets_new_t/0 has no local return
-contracts_with_subtypes.erl:262: The call contracts_with_subtypes:factored_ets_new(12,[]) breaks the contract (Name,Options) -> atom() when is_subtype(Name,atom()), is_subtype(Options,[Option]), is_subtype(Option,Type | Access | 'named_table' | {'keypos',Pos} | {'heir',Pid::pid(),HeirData} | {'heir','none'} | Tweaks), is_subtype(Type,type()), is_subtype(Access,access()), is_subtype(Tweaks,{'write_concurrency',boolean()} | {'read_concurrency',boolean()} | 'compressed'), is_subtype(Pos,pos_integer()), is_subtype(HeirData,term())
+contracts_with_subtypes.erl:263: Function flat_ets_new_t/0 has no local return
+contracts_with_subtypes.erl:264: The call contracts_with_subtypes:flat_ets_new(12,[]) breaks the contract (Name,Options) -> atom() when is_subtype(Name,atom()), is_subtype(Options,[Option]), is_subtype(Option,'set' | 'ordered_set' | 'bag' | 'duplicate_bag' | 'public' | 'protected' | 'private' | 'named_table' | {'keypos',integer()} | {'heir',pid(),term()} | {'heir','none'} | {'write_concurrency',boolean()} | {'read_concurrency',boolean()} | 'compressed')
+contracts_with_subtypes.erl:290: Function factored_ets_new_t/0 has no local return
+contracts_with_subtypes.erl:291: The call contracts_with_subtypes:factored_ets_new(12,[]) breaks the contract (Name,Options) -> atom() when is_subtype(Name,atom()), is_subtype(Options,[Option]), is_subtype(Option,Type | Access | 'named_table' | {'keypos',Pos} | {'heir',Pid::pid(),HeirData} | {'heir','none'} | Tweaks), is_subtype(Type,type()), is_subtype(Access,access()), is_subtype(Tweaks,{'write_concurrency',boolean()} | {'read_concurrency',boolean()} | 'compressed'), is_subtype(Pos,pos_integer()), is_subtype(HeirData,term())
 contracts_with_subtypes.erl:77: The call contracts_with_subtypes:foo1(5) breaks the contract (Arg1) -> Res when is_subtype(Arg1,atom()), is_subtype(Res,atom())
 contracts_with_subtypes.erl:78: The call contracts_with_subtypes:foo2(5) breaks the contract (Arg1) -> Res when is_subtype(Arg1,Arg2), is_subtype(Arg2,atom()), is_subtype(Res,atom())
 contracts_with_subtypes.erl:79: The call contracts_with_subtypes:foo3(5) breaks the contract (Arg1) -> Res when is_subtype(Arg2,atom()), is_subtype(Arg1,Arg2), is_subtype(Res,atom())
diff --git a/lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes2 b/lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes2
new file mode 100644
index 0000000000..9f5433a13d
--- /dev/null
+++ b/lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes2
@@ -0,0 +1,3 @@
+
+contracts_with_subtypes2.erl:18: Function t/0 has no local return
+contracts_with_subtypes2.erl:19: The call contracts_with_subtypes2:t({'a',{'b',{'c',{'d',{'e',{'g',3}}}}}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A}), is_subtype(A,{'b',B}), is_subtype(B,{'c',C}), is_subtype(C,{'d',D}), is_subtype(D,{'e',E}), is_subtype(E,{'f',_})
diff --git a/lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes.erl b/lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes.erl
index d72138d509..d7dfd9752e 100644
--- a/lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes.erl
+++ b/lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes.erl
@@ -103,15 +103,44 @@ c(babb) -> rec_arg({b, {a, {b, b}}});
 c(ababb) -> rec_arg({a, {b, {a, {b, b}}}});
 c(babaa) -> rec_arg({b, {a, {b, {a, a}}}}).
 
-w(ab) -> rec_arg({a, b});
-w(ba) -> rec_arg({b, a});
-w(aba) -> rec_arg({a, {b, a}});
-w(bab) -> rec_arg({b, {a, b}});
-w(abab) -> rec_arg({a, {b, {a, b}}});
-w(baba) -> rec_arg({b, {a, {b, a}}});
+w(ab) -> rec_arg({a, b}); % breaks the contract
+w(ba) -> rec_arg({b, a}); % breaks the contract
+w(aba) -> rec_arg({a, {b, a}}); % no longer breaks the contract
+w(bab) -> rec_arg({b, {a, b}}); % breaks the contract
+w(abab) -> rec_arg({a, {b, {a, b}}}); % no longer breaks the contract
+w(baba) -> rec_arg({b, {a, {b, a}}}); % no longer breaks the contract
 w(ababa) -> rec_arg({a, {b, {a, {b, a}}}});
 w(babab) -> rec_arg({b, {a, {b, {a, b}}}}).
 
+%% For comparison: the same thing with types
+
+-type ab() :: {a, a()} | {b, b()}.
+-type a() :: a | {b, b()}.
+-type b() :: b | {a, a()}.
+
+-spec rec2(Arg) -> ok when
+      Arg :: ab().
+
+rec2(X) -> get(X).
+
+d(aa) -> rec2({a, a});
+d(bb) -> rec2({b, b});
+d(abb) -> rec2({a, {b, b}});
+d(baa) -> rec2({b, {a, a}});
+d(abaa) -> rec2({a, {b, {a, a}}});
+d(babb) -> rec2({b, {a, {b, b}}});
+d(ababb) -> rec2({a, {b, {a, {b, b}}}});
+d(babaa) -> rec2({b, {a, {b, {a, a}}}}).
+
+q(ab) -> rec2({a, b}); % breaks the contract
+q(ba) -> rec2({b, a}); % breaks the contract
+q(aba) -> rec2({a, {b, a}}); % breaks the contract
+q(bab) -> rec2({b, {a, b}}); % breaks the contract
+q(abab) -> rec2({a, {b, {a, b}}});
+q(baba) -> rec2({b, {a, {b, a}}});
+q(ababa) -> rec2({a, {b, {a, {b, a}}}});
+q(babab) -> rec2({b, {a, {b, {a, b}}}}).
+
 %===============================================================================
 
 -type dublo(X) :: {X, X}.
@@ -143,7 +172,7 @@ st(X) when is_atom(X) ->
 		_Other -> ok
 	    end;
 	alpha -> bad;
-	{ok, 42} -> bad;
+	{ok, 42} -> ok;
 	42 -> bad
     end.
 
@@ -161,7 +190,7 @@ dt(X) when is_atom(X) ->
 	err2 -> ok;
 	{ok, X} -> ok;
 	alpha -> bad;
-	{ok, 42} -> bad;
+	{ok, 42} -> ok;
 	42 -> bad
     end.
 
@@ -181,7 +210,7 @@ dt2(X) when is_atom(X) ->
 	err2 -> ok;
 	{ok, X} -> ok;
 	alpha -> bad;
-	{ok, 42} -> bad;
+	{ok, 42} -> ok;
 	42 -> bad
     end.
 
diff --git a/lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes2.erl b/lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes2.erl
new file mode 100644
index 0000000000..d2f945b284
--- /dev/null
+++ b/lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes2.erl
@@ -0,0 +1,40 @@
+-module(contracts_with_subtypes2).
+
+-compile(export_all).
+
+-behaviour(supervisor).
+
+-spec t(Arg) -> ok when
+      Arg :: {a, A},
+      A :: {b, B},
+      B :: {c, C},
+      C :: {d, D},
+      D :: {e, E},
+      E :: {f, _}.
+
+t(X) ->
+    get(X).
+
+t() ->
+    t({a, {b, {c, {d, {e, {g, 3}}}}}}). % breaks the contract
+
+%% This one should possibly result in warnings about unused variables.
+-spec l() -> ok when
+      X :: Y,
+      Y :: X.
+
+l() ->
+    ok.
+
+%% This is the example from seq12547 (ticket OTP-11798).
+%% There used to be a warning.
+
+-spec init(term()) -> Result when
+      Result :: {ok, {{supervisor:strategy(),
+                       non_neg_integer(),
+                       pos_integer()},
+                      [supervisor:child_spec()]}}
+              | ignore.
+
+init(_) ->
+    foo:bar().