aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorHans Bolinder <[email protected]>2014-03-17 09:53:32 +0100
committerHans Bolinder <[email protected]>2014-03-21 14:19:15 +0100
commitc777e4096a21f9734a1cec8d723137299b0f9193 (patch)
treeba035cb658a8e645b0c50aa3016ad8c7ba2ba5b2
parent4d614d868f90cfae31046038e6f178002a13c9ef (diff)
downloadotp-c777e4096a21f9734a1cec8d723137299b0f9193.tar.gz
otp-c777e4096a21f9734a1cec8d723137299b0f9193.tar.bz2
otp-c777e4096a21f9734a1cec8d723137299b0f9193.zip
dialyzer: generalize guard constraints in a new way
Guard constraints used to be limited to a certain depth, which handled mutually depending constraints safely, but also sometimes introduced unnecessary generalizations. This patch puts no explicit limit upon guard constraints (other than those that already exist in erl_types), but breaks cycles by replacing variables with the any() type. In some cases the old method resulted in more warnings, but since the limit was quite arbitrary and mutually depending guard constraints are (very) rare, the new method should been seen as an improvement since it handles cases that used to make Dialyzer loop or miss warnings.
-rw-r--r--lib/dialyzer/src/dialyzer_contracts.erl78
-rw-r--r--lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes39
-rw-r--r--lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes23
-rw-r--r--lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes.erl47
-rw-r--r--lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes2.erl40
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().