%% -*- erlang-indent-level: 2 -*-
%%-----------------------------------------------------------------------
%% %CopyrightBegin%
%%
%% Copyright Ericsson AB 2006-2013. All Rights Reserved.
%%
%% The contents of this file are subject to the Erlang Public License,
%% Version 1.1, (the "License"); you may not use this file except in
%% compliance with the License. You should have received a copy of the
%% Erlang Public License along with this software. If not, it can be
%% retrieved online at http://www.erlang.org/.
%%
%% Software distributed under the License is distributed on an "AS IS"
%% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
%% the License for the specific language governing rights and limitations
%% under the License.
%%
%% %CopyrightEnd%
%%
%%%-------------------------------------------------------------------
%%% File : dialyzer_typesig.erl
%%% Author : Tobias Lindahl <[email protected]>
%%% Description :
%%%
%%% Created : 25 Apr 2005 by Tobias Lindahl <[email protected]>
%%%-------------------------------------------------------------------
-module(dialyzer_typesig).
-export([analyze_scc/6]).
-export([get_safe_underapprox/2]).
-import(erl_types,
[t_any/0, t_atom/0, t_atom_vals/1,
t_binary/0, t_bitstr/0, t_bitstr/2, t_bitstr_concat/1, t_boolean/0,
t_collect_vars/1, t_cons/2, t_cons_hd/1, t_cons_tl/1,
t_float/0, t_from_range/2, t_from_term/1,
t_fun/0, t_fun/2, t_fun_args/1, t_fun_range/1,
t_has_var/1,
t_inf/2, t_inf/3, t_integer/0,
t_is_any/1, t_is_atom/1, t_is_atom/2, t_is_cons/1, t_is_equal/2,
t_is_float/1, t_is_fun/1,
t_is_integer/1, t_non_neg_integer/0,
t_is_list/1, t_is_nil/1, t_is_none/1, t_is_number/1,
t_is_subtype/2, t_limit/2, t_list/0, t_list/1,
t_list_elements/1, t_nonempty_list/1, t_maybe_improper_list/0,
t_module/0, t_number/0, t_number_vals/1,
t_opaque_match_record/2, t_opaque_matching_structure/2,
t_opaque_from_records/1,
t_pid/0, t_port/0, t_product/1, t_reference/0,
t_subst/2, t_subtract/2, t_subtract_list/2, t_sup/1, t_sup/2,
t_timeout/0, t_tuple/0, t_tuple/1,
t_unify/3, t_var/1, t_var_name/1,
t_none/0, t_unit/0]).
-include("dialyzer.hrl").
%%-----------------------------------------------------------------------------
-type dep() :: integer(). %% type variable names used as constraint ids
-type type_var() :: erl_types:erl_type(). %% actually: {'c','var',_,_}
-record(fun_var, {'fun' :: fun((_) -> erl_types:erl_type()), deps :: [dep()],
origin :: integer()}).
-type constr_op() :: 'eq' | 'sub'.
-type fvar_or_type() :: #fun_var{} | erl_types:erl_type().
-record(constraint, {lhs :: erl_types:erl_type(),
op :: constr_op(),
rhs :: fvar_or_type(),
deps :: [dep()]}).
-type constraint() :: #constraint{}.
-record(constraint_list, {type :: 'conj' | 'disj',
list :: [constr()],
deps :: [dep()],
masks :: [{dep(),[non_neg_integer()]}] |
{'d',dict()},
id :: {'list', dep()}}).
-type constraint_list() :: #constraint_list{}.
-record(constraint_ref, {id :: type_var(), deps :: [dep()]}).
-type constraint_ref() :: #constraint_ref{}.
-type constr() :: constraint() | constraint_list() | constraint_ref().
-type typesig_scc() :: [{mfa(), {cerl:c_var(), cerl:c_fun()}, dict()}].
-type typesig_funmap() :: [{type_var(), type_var()}]. %% Orddict
-type dict_or_ets() :: {'d', dict()} | {'e', ets:tid()}.
-record(state, {callgraph :: dialyzer_callgraph:callgraph(),
cs = [] :: [constr()],
cmap = {'d', dict:new()} :: dict_or_ets(),
fun_map = [] :: typesig_funmap(),
fun_arities = dict:new() :: dict(),
in_match = false :: boolean(),
in_guard = false :: boolean(),
module :: module(),
name_map = dict:new() :: dict(),
next_label = 0 :: label(),
self_rec :: erl_types:erl_type(),
plt :: dialyzer_plt:plt(),
prop_types = {'d', dict:new()} :: dict_or_ets(),
records = dict:new() :: dict(),
opaques = [] :: [erl_types:erl_type()],
scc = [] :: [type_var()],
mfas :: [tuple()],
solvers = [] :: [solver()]
}).
%%-----------------------------------------------------------------------------
-define(TYPE_LIMIT, 4).
-define(INTERNAL_TYPE_LIMIT, 5).
%%-define(DEBUG, true).
%%-define(DEBUG_CONSTRAINTS, true).
-ifdef(DEBUG).
-define(DEBUG_NAME_MAP, true).
-define(DEBUG_LOOP_DETECTION, true).
-endif.
%%-define(DEBUG_NAME_MAP, true).
%%-define(DEBUG_LOOP_DETECTION, true).
-ifdef(DEBUG).
-define(debug(__String, __Args), io:format(__String, __Args)).
-define(mk_fun_var(Fun, Vars), mk_fun_var(?LINE, Fun, Vars)).
-else.
-define(debug(__String, __Args), ok).
-define(mk_fun_var(Fun, Vars), mk_fun_var(Fun, Vars)).
-endif.
%% ============================================================================
%%
%% The analysis.
%%
%% ============================================================================
%%-----------------------------------------------------------------------------
%% Analysis of strongly connected components.
%%
%% analyze_scc(SCC, NextLabel, CallGraph, PLT, PropTypes, Solvers) -> FunTypes
%%
%% SCC - [{MFA, Def, Records}]
%% where Def = {Var, Fun} as in the Core Erlang module definitions.
%% Records = dict(RecName, {Arity, [{FieldName, FieldType}]})
%% NextLabel - An integer that is higher than any label in the code.
%% CallGraph - A callgraph as produced by dialyzer_callgraph.erl
%% Note: The callgraph must have been built with all the
%% code that the SCC is a part of.
%% PLT - A dialyzer PLT. This PLT should contain available information
%% about functions that can be called by this SCC.
%% PropTypes - A dictionary.
%% FunTypes - A dictionary.
%% Solvers - User specified solvers.
%%-----------------------------------------------------------------------------
-spec analyze_scc(typesig_scc(), label(),
dialyzer_callgraph:callgraph(),
dialyzer_plt:plt(), dict(), [solver()]) -> dict().
analyze_scc(SCC, NextLabel, CallGraph, Plt, PropTypes, Solvers0) ->
Solvers = solvers(Solvers0),
assert_format_of_scc(SCC),
State1 = new_state(SCC, NextLabel, CallGraph, Plt, PropTypes, Solvers),
DefSet = add_def_list([Var || {_MFA, {Var, _Fun}, _Rec} <- SCC], sets:new()),
State2 = traverse_scc(SCC, DefSet, State1),
State3 = state__finalize(State2),
Funs = state__scc(State3),
pp_constrs_scc(Funs, State3),
constraints_to_dot_scc(Funs, State3),
solve(Funs, State3).
assert_format_of_scc([{_MFA, {_Var, _Fun}, _Records}|Left]) ->
assert_format_of_scc(Left);
assert_format_of_scc([]) ->
ok.
solvers([]) -> [v2];
solvers(Solvers) -> Solvers.
%% ============================================================================
%%
%% Gets the constraints by traversing the code.
%%
%% ============================================================================
traverse_scc([{MFA, Def, Rec}|Left], DefSet, AccState) ->
TmpState1 = state__set_rec_dict(AccState, Rec),
TmpState2 = state__set_opaques(TmpState1, MFA),
DummyLetrec = cerl:c_letrec([Def], cerl:c_atom(foo)),
{NewAccState, _} = traverse(DummyLetrec, DefSet, TmpState2),
traverse_scc(Left, DefSet, NewAccState);
traverse_scc([], _DefSet, AccState) ->
AccState.
traverse(Tree, DefinedVars, State) ->
?debug("Handling ~p\n", [cerl:type(Tree)]),
case cerl:type(Tree) of
alias ->
Var = cerl:alias_var(Tree),
Pat = cerl:alias_pat(Tree),
DefinedVars1 = add_def(Var, DefinedVars),
{State1, PatVar} = traverse(Pat, DefinedVars1, State),
State2 = state__store_conj(mk_var(Var), eq, PatVar, State1),
{State2, PatVar};
apply ->
Args = cerl:apply_args(Tree),
Arity = length(Args),
Op = cerl:apply_op(Tree),
{State0, ArgTypes} = traverse_list(Args, DefinedVars, State),
{State1, OpType} = traverse(Op, DefinedVars, State0),
{State2, FunType} = state__get_fun_prototype(OpType, Arity, State1),
State3 = state__store_conj(FunType, eq, OpType, State2),
State4 = state__store_conj(mk_var(Tree), sub, t_fun_range(FunType),
State3),
State5 = state__store_conj_lists(ArgTypes, sub, t_fun_args(FunType),
State4),
case state__lookup_apply(Tree, State) of
unknown ->
{State5, mk_var(Tree)};
FunLabels ->
case get_apply_constr(FunLabels, mk_var(Tree), ArgTypes, State5) of
error -> {State5, mk_var(Tree)};
{ok, State6} -> {State6, mk_var(Tree)}
end
end;
binary ->
{State1, SegTypes} = traverse_list(cerl:binary_segments(Tree),
DefinedVars, State),
Type = ?mk_fun_var(fun(Map) ->
TmpSegTypes = lookup_type_list(SegTypes, Map),
t_bitstr_concat(TmpSegTypes)
end, SegTypes),
{state__store_conj(mk_var(Tree), sub, Type, State1), mk_var(Tree)};
bitstr ->
Size = cerl:bitstr_size(Tree),
UnitVal = cerl:int_val(cerl:bitstr_unit(Tree)),
Val = cerl:bitstr_val(Tree),
{State1, [SizeType, ValType]} =
traverse_list([Size, Val], DefinedVars, State),
{State2, TypeConstr} =
case cerl:bitstr_bitsize(Tree) of
all -> {State1, t_bitstr(UnitVal, 0)};
utf -> {State1, t_binary()}; % contains an integer number of bytes
N when is_integer(N) -> {State1, t_bitstr(0, N)};
any -> % Size is not a literal
{state__store_conj(SizeType, sub, t_non_neg_integer(), State1),
?mk_fun_var(bitstr_constr(SizeType, UnitVal), [SizeType])}
end,
ValTypeConstr =
case cerl:concrete(cerl:bitstr_type(Tree)) of
binary -> TypeConstr;
float ->
case state__is_in_match(State1) of
true -> t_float();
false -> t_number()
end;
integer ->
case state__is_in_match(State1) of
true ->
Flags = cerl:concrete(cerl:bitstr_flags(Tree)),
?mk_fun_var(bitstr_val_constr(SizeType, UnitVal, Flags),
[SizeType]);
false -> t_integer()
end;
utf8 -> t_integer();
utf16 -> t_integer();
utf32 -> t_integer()
end,
State3 = state__store_conj(ValType, sub, ValTypeConstr, State2),
State4 = state__store_conj(mk_var(Tree), sub, TypeConstr, State3),
{State4, mk_var(Tree)};
'case' ->
Arg = cerl:case_arg(Tree),
Clauses = filter_match_fail(cerl:case_clauses(Tree)),
{State1, ArgVar} = traverse(Arg, DefinedVars, State),
handle_clauses(Clauses, mk_var(Tree), ArgVar, DefinedVars, State1);
call ->
handle_call(Tree, DefinedVars, State);
'catch' ->
%% XXX: Perhaps there is something to say about this.
{State, mk_var(Tree)};
cons ->
Hd = cerl:cons_hd(Tree),
Tl = cerl:cons_tl(Tree),
{State1, [HdVar, TlVar]} = traverse_list([Hd, Tl], DefinedVars, State),
case cerl:is_literal(cerl:fold_literal(Tree)) of
true ->
%% We do not need to do anything more here.
{State, t_cons(HdVar, TlVar)};
false ->
ConsVar = mk_var(Tree),
ConsType = ?mk_fun_var(fun(Map) ->
t_cons(lookup_type(HdVar, Map),
lookup_type(TlVar, Map))
end, [HdVar, TlVar]),
HdType = ?mk_fun_var(fun(Map) ->
Cons = lookup_type(ConsVar, Map),
case t_is_cons(Cons) of
false -> t_any();
true -> t_cons_hd(Cons)
end
end, [ConsVar]),
TlType = ?mk_fun_var(fun(Map) ->
Cons = lookup_type(ConsVar, Map),
case t_is_cons(Cons) of
false -> t_any();
true -> t_cons_tl(Cons)
end
end, [ConsVar]),
State2 = state__store_conj_lists([HdVar, TlVar, ConsVar], sub,
[HdType, TlType, ConsType],
State1),
{State2, ConsVar}
end;
'fun' ->
Body = cerl:fun_body(Tree),
Vars = cerl:fun_vars(Tree),
DefinedVars1 = add_def_list(Vars, DefinedVars),
State0 = state__new_constraint_context(State),
FunFailType =
case state__prop_domain(cerl_trees:get_label(Tree), State0) of
error -> t_fun(length(Vars), t_none());
{ok, Dom} -> t_fun(Dom, t_none())
end,
TreeVar = mk_var(Tree),
State2 =
try
State1 = case state__add_prop_constrs(Tree, State0) of
not_called -> State0;
PropState -> PropState
end,
{BodyState, BodyVar} = traverse(Body, DefinedVars1, State1),
state__store_conj(TreeVar, eq,
t_fun(mk_var_list(Vars), BodyVar), BodyState)
catch
throw:error ->
state__store_conj(TreeVar, eq, FunFailType, State0)
end,
Cs = state__cs(State2),
State3 = state__store_constrs(TreeVar, Cs, State2),
Ref = mk_constraint_ref(TreeVar, get_deps(Cs)),
OldCs = state__cs(State),
State4 = state__new_constraint_context(State3),
State5 = state__store_conj_list([OldCs, Ref], State4),
State6 = state__store_fun_arity(Tree, State5),
State7 = state__add_fun_to_scc(TreeVar, State6),
{State7, TreeVar};
'let' ->
Vars = cerl:let_vars(Tree),
Arg = cerl:let_arg(Tree),
Body = cerl:let_body(Tree),
{State1, ArgVars} = traverse(Arg, DefinedVars, State),
State2 = state__store_conj(t_product(mk_var_list(Vars)), eq,
ArgVars, State1),
DefinedVars1 = add_def_list(Vars, DefinedVars),
traverse(Body, DefinedVars1, State2);
letrec ->
Defs = cerl:letrec_defs(Tree),
Body = cerl:letrec_body(Tree),
Funs = [Fun || {_Var, Fun} <- Defs],
Vars = [Var || {Var, _Fun} <- Defs],
State1 = state__store_funs(Vars, Funs, State),
DefinedVars1 = add_def_list(Vars, DefinedVars),
{State2, _} = traverse_list(Funs, DefinedVars1, State1),
traverse(Body, DefinedVars1, State2);
literal ->
%% This is needed for finding records
case cerl:unfold_literal(Tree) of
Tree ->
Type = t_from_term(cerl:concrete(Tree)),
NewType =
case erl_types:t_opaque_match_atom(Type, State#state.opaques) of
[Opaque] -> Opaque;
_ -> Type
end,
{State, NewType};
NewTree -> traverse(NewTree, DefinedVars, State)
end;
module ->
Defs = cerl:module_defs(Tree),
Funs = [Fun || {_Var, Fun} <- Defs],
Vars = [Var || {Var, _Fun} <- Defs],
DefinedVars1 = add_def_list(Vars, DefinedVars),
State1 = state__store_funs(Vars, Funs, State),
FoldFun = fun(Fun, AccState) ->
{S, _} = traverse(Fun, DefinedVars1,
state__new_constraint_context(AccState)),
S
end,
lists:foldl(FoldFun, State1, Funs);
primop ->
case cerl:atom_val(cerl:primop_name(Tree)) of
match_fail -> throw(error);
raise -> throw(error);
bs_init_writable -> {State, t_from_term(<<>>)};
Other -> erlang:error({'Unsupported primop', Other})
end;
'receive' ->
Clauses = filter_match_fail(cerl:receive_clauses(Tree)),
Timeout = cerl:receive_timeout(Tree),
case (cerl:is_c_atom(Timeout) andalso
(cerl:atom_val(Timeout) =:= infinity)) of
true ->
handle_clauses(Clauses, mk_var(Tree), [], DefinedVars, State);
false ->
Action = cerl:receive_action(Tree),
{State1, TimeoutVar} = traverse(Timeout, DefinedVars, State),
State2 = state__store_conj(TimeoutVar, sub, t_timeout(), State1),
handle_clauses(Clauses, mk_var(Tree), [], Action, DefinedVars, State2)
end;
seq ->
Body = cerl:seq_body(Tree),
Arg = cerl:seq_arg(Tree),
{State1, _} = traverse(Arg, DefinedVars, State),
traverse(Body, DefinedVars, State1);
'try' ->
handle_try(Tree, DefinedVars, State);
tuple ->
Elements = cerl:tuple_es(Tree),
{State1, EVars} = traverse_list(Elements, DefinedVars, State),
{State2, TupleType} =
case cerl:is_literal(cerl:fold_literal(Tree)) of
true ->
%% We do not need to do anything more here.
{State, t_tuple(EVars)};
false ->
%% We have the same basic problem as in products, but we want to
%% make sure that everything that can be used as tags for the
%% disjoint unions stays in the tuple.
Fun = fun(Var, AccState) ->
case t_has_var(Var) of
true ->
{AccState1, NewVar} = state__mk_var(AccState),
{NewVar,
state__store_conj(Var, eq, NewVar, AccState1)};
false ->
{Var, AccState}
end
end,
{NewEvars, TmpState} = lists:mapfoldl(Fun, State1, EVars),
{TmpState, t_tuple(NewEvars)}
end,
case Elements of
[Tag|Fields] ->
case cerl:is_c_atom(Tag) of
true ->
%% Check if an opaque term is constructed.
case t_opaque_match_record(TupleType, State#state.opaques) of
[Opaque] ->
OpStruct = t_opaque_matching_structure(TupleType, Opaque),
State3 = state__store_conj(TupleType, sub, OpStruct, State2),
{State3, Opaque};
%% Check if a record is constructed.
_ ->
Arity = length(Fields),
Records = State2#state.records,
case lookup_record(Records, cerl:atom_val(Tag), Arity) of
error -> {State2, TupleType};
{ok, RecType} ->
State3 = state__store_conj(TupleType, sub, RecType, State2),
{State3, TupleType}
end
end;
false -> {State2, TupleType}
end;
[] -> {State2, TupleType}
end;
values ->
%% We can get into trouble when unifying products that have the
%% same element appearing several times. Handle these cases by
%% introducing fresh variables and constraining them to be equal
%% to the original ones. This is similar to what happens in
%% pattern matching where the matching is done on fresh
%% variables and guards assert that the matching is correct.
Elements = cerl:values_es(Tree),
{State1, EVars} = traverse_list(Elements, DefinedVars, State),
Arity = length(EVars),
Unique = length(ordsets:from_list(EVars)),
case Arity =:= Unique of
true -> {State1, t_product(EVars)};
false ->
{State2, Vars} = state__mk_vars(Arity, State1),
State3 = state__store_conj_lists(Vars, eq, EVars, State2),
{State3, t_product(Vars)}
end;
var ->
case is_def(Tree, DefinedVars) of
true -> {State, mk_var(Tree)};
false ->
%% If we are analyzing SCCs this can be a function variable.
case state__lookup_undef_var(Tree, State) of
error -> erlang:error({'Undefined variable', Tree});
{ok, Type} ->
{State1, NewVar} = state__mk_var(State),
{state__store_conj(NewVar, sub, Type, State1), NewVar}
end
end;
Other ->
erlang:error({'Unsupported type', Other})
end.
traverse_list(Trees, DefinedVars, State) ->
traverse_list(Trees, DefinedVars, State, []).
traverse_list([Tree|Tail], DefinedVars, State, Acc) ->
{State1, Var} = traverse(Tree, DefinedVars, State),
traverse_list(Tail, DefinedVars, State1, [Var|Acc]);
traverse_list([], _DefinedVars, State, Acc) ->
{State, lists:reverse(Acc)}.
add_def(Var, Set) ->
sets:add_element(cerl_trees:get_label(Var), Set).
add_def_list([H|T], Set) ->
add_def_list(T, add_def(H, Set));
add_def_list([], Set) ->
Set.
add_def_from_tree(T, DefinedVars) ->
Vars = cerl_trees:fold(fun(X, Acc) ->
case cerl:is_c_var(X) of
true -> [X|Acc];
false -> Acc
end
end, [], T),
add_def_list(Vars, DefinedVars).
add_def_from_tree_list([H|T], DefinedVars) ->
add_def_from_tree_list(T, add_def_from_tree(H, DefinedVars));
add_def_from_tree_list([], DefinedVars) ->
DefinedVars.
is_def(Var, Set) ->
sets:is_element(cerl_trees:get_label(Var), Set).
%%----------------------------------------
%% Try
%%
handle_try(Tree, DefinedVars, State) ->
Arg = cerl:try_arg(Tree),
Vars = cerl:try_vars(Tree),
EVars = cerl:try_evars(Tree),
Body = cerl:try_body(Tree),
Handler = cerl:try_handler(Tree),
State1 = state__new_constraint_context(State),
{ArgBodyState, BodyVar} =
try
{State2, ArgVar} = traverse(Arg, DefinedVars, State1),
DefinedVars1 = add_def_list(Vars, DefinedVars),
{State3, BodyVar1} = traverse(Body, DefinedVars1, State2),
State4 = state__store_conj(t_product(mk_var_list(Vars)), eq, ArgVar,
State3),
{State4, BodyVar1}
catch
throw:error ->
{State1, t_none()}
end,
State6 = state__new_constraint_context(ArgBodyState),
{HandlerState, HandlerVar} =
try
DefinedVars2 = add_def_list([X || X <- EVars, cerl:is_c_var(X)],
DefinedVars),
traverse(Handler, DefinedVars2, State6)
catch
throw:error ->
{State6, t_none()}
end,
ArgBodyCs = state__cs(ArgBodyState),
HandlerCs = state__cs(HandlerState),
TreeVar = mk_var(Tree),
OldCs = state__cs(State),
case state__is_in_guard(State) of
true ->
Conj1 = mk_conj_constraint_list([ArgBodyCs,
mk_constraint(BodyVar, eq, TreeVar)]),
Disj = mk_disj_constraint_list([Conj1,
mk_constraint(HandlerVar, eq, TreeVar)]),
NewState1 = state__new_constraint_context(HandlerState),
Conj2 = mk_conj_constraint_list([OldCs, Disj]),
NewState2 = state__store_conj(Conj2, NewState1),
{NewState2, TreeVar};
false ->
{NewCs, ReturnVar} =
case {t_is_none(BodyVar), t_is_none(HandlerVar)} of
{false, false} ->
Conj1 =
mk_conj_constraint_list([ArgBodyCs,
mk_constraint(TreeVar, eq, BodyVar)]),
Conj2 =
mk_conj_constraint_list([HandlerCs,
mk_constraint(TreeVar, eq, HandlerVar)]),
Disj = mk_disj_constraint_list([Conj1, Conj2]),
{Disj, TreeVar};
{false, true} ->
{mk_conj_constraint_list([ArgBodyCs,
mk_constraint(TreeVar, eq, BodyVar)]),
BodyVar};
{true, false} ->
{mk_conj_constraint_list([HandlerCs,
mk_constraint(TreeVar, eq, HandlerVar)]),
HandlerVar};
{true, true} ->
?debug("Throw failed\n", []),
throw(error)
end,
Conj = mk_conj_constraint_list([OldCs, NewCs]),
NewState1 = state__new_constraint_context(HandlerState),
NewState2 = state__store_conj(Conj, NewState1),
{NewState2, ReturnVar}
end.
%%----------------------------------------
%% Call
%%
handle_call(Call, DefinedVars, State) ->
Args = cerl:call_args(Call),
Mod = cerl:call_module(Call),
Fun = cerl:call_name(Call),
Dst = mk_var(Call),
case cerl:is_c_atom(Mod) andalso cerl:is_c_atom(Fun) of
true ->
M = cerl:atom_val(Mod),
F = cerl:atom_val(Fun),
A = length(Args),
MFA = {M, F, A},
{State1, ArgVars} = traverse_list(Args, DefinedVars, State),
case state__lookup_rec_var_in_scope(MFA, State) of
error ->
case get_bif_constr(MFA, Dst, ArgVars, State1) of
none ->
{get_plt_constr(MFA, Dst, ArgVars, State1), Dst};
C ->
{state__store_conj(C, State1), Dst}
end;
{ok, Var} ->
%% This is part of the SCC currently analyzed.
%% Intercept and change this to an apply instead.
?debug("Found the call to ~w\n", [MFA]),
Label = cerl_trees:get_label(Call),
Apply = cerl:ann_c_apply([{label, Label}], Var, Args),
traverse(Apply, DefinedVars, State)
end;
false ->
{State1, MF} = traverse_list([Mod, Fun], DefinedVars, State),
{state__store_conj_lists(MF, sub, [t_module(), t_atom()], State1), Dst}
end.
get_plt_constr(MFA, Dst, ArgVars, State) ->
Plt = state__plt(State),
PltRes = dialyzer_plt:lookup(Plt, MFA),
Opaques = State#state.opaques,
Module = State#state.module,
SCCMFAs = State#state.mfas,
{FunModule, _, _} = MFA,
Contract =
case lists:member(MFA, SCCMFAs) of
true -> none;
false -> dialyzer_plt:lookup_contract(Plt, MFA)
end,
case Contract of
none ->
case PltRes of
none -> State;
{value, {PltRetType, PltArgTypes}} ->
state__store_conj_lists([Dst|ArgVars], sub,
[PltRetType|PltArgTypes], State)
end;
{value, #contract{args = GenArgs} = C} ->
{RetType, ArgCs} =
case PltRes of
none ->
{?mk_fun_var(fun(Map) ->
ArgTypes = lookup_type_list(ArgVars, Map),
dialyzer_contracts:get_contract_return(C, ArgTypes)
end, ArgVars), GenArgs};
{value, {PltRetType, PltArgTypes}} ->
%% Need to combine the contract with the success typing.
{?mk_fun_var(
fun(Map) ->
ArgTypes0 = lookup_type_list(ArgVars, Map),
ArgTypes = case FunModule =:= Module of
false ->
List = lists:zip(PltArgTypes, ArgTypes0),
[erl_types:t_unopaque_on_mismatch(T1, T2, Opaques)
|| {T1, T2} <- List];
true -> ArgTypes0
end,
CRet = dialyzer_contracts:get_contract_return(C, ArgTypes),
t_inf(CRet, PltRetType, opaque)
end, ArgVars),
[t_inf(X, Y, opaque) || {X, Y} <- lists:zip(GenArgs, PltArgTypes)]}
end,
state__store_conj_lists([Dst|ArgVars], sub, [RetType|ArgCs], State)
end.
filter_match_fail([Clause] = Cls) ->
Body = cerl:clause_body(Clause),
case cerl:type(Body) of
primop ->
case cerl:atom_val(cerl:primop_name(Body)) of
match_fail -> [];
raise -> [];
_ -> Cls
end;
_ -> Cls
end;
filter_match_fail([H|T]) ->
[H|filter_match_fail(T)];
filter_match_fail([]) ->
%% This can actually happen, for example in
%% receive after 1 -> ok end
[].
%% If there is a significant number of clauses, we cannot apply the
%% list subtraction scheme since it causes the analysis to be too
%% slow. Typically, this only affects automatically generated files.
%% The dataflow analysis doesn't suffer from this, so we will get some
%% information anyway.
-define(MAX_NOF_CLAUSES, 15).
handle_clauses(Clauses, TopVar, Arg, DefinedVars, State) ->
handle_clauses(Clauses, TopVar, Arg, none, DefinedVars, State).
handle_clauses([], _, _, Action, DefinedVars, State) when Action =/= none ->
%% Can happen when a receive has no clauses, see filter_match_fail.
traverse(Action, DefinedVars, State);
handle_clauses(Clauses, TopVar, Arg, Action, DefinedVars, State) ->
SubtrTypeList =
if length(Clauses) > ?MAX_NOF_CLAUSES -> overflow;
true -> []
end,
{State1, CList} = handle_clauses_1(Clauses, TopVar, Arg, DefinedVars,
State, SubtrTypeList, []),
{NewCs, NewState} =
case Action of
none ->
if CList =:= [] -> throw(error);
true -> {CList, State1}
end;
_ ->
try
{State2, ActionVar} = traverse(Action, DefinedVars, State1),
TmpC = mk_constraint(TopVar, eq, ActionVar),
ActionCs = mk_conj_constraint_list([state__cs(State2),TmpC]),
{[ActionCs|CList], State2}
catch
throw:error ->
if CList =:= [] -> throw(error);
true -> {CList, State1}
end
end
end,
OldCs = state__cs(State),
NewCList = mk_disj_constraint_list(NewCs),
FinalState = state__new_constraint_context(NewState),
{state__store_conj_list([OldCs, NewCList], FinalState), TopVar}.
handle_clauses_1([Clause|Tail], TopVar, Arg, DefinedVars,
State, SubtrTypes, Acc) ->
State0 = state__new_constraint_context(State),
Pats = cerl:clause_pats(Clause),
Guard = cerl:clause_guard(Clause),
Body = cerl:clause_body(Clause),
NewSubtrTypes =
case SubtrTypes =:= overflow of
true -> overflow;
false ->
ordsets:add_element(get_safe_underapprox(Pats, Guard), SubtrTypes)
end,
try
DefinedVars1 = add_def_from_tree_list(Pats, DefinedVars),
State1 = state__set_in_match(State0, true),
{State2, PatVars} = traverse_list(Pats, DefinedVars1, State1),
State3 =
case Arg =:= [] of
true -> State2;
false ->
S = state__store_conj(Arg, eq, t_product(PatVars), State2),
case SubtrTypes =:= overflow of
true -> S;
false ->
SubtrPatVar = ?mk_fun_var(fun(Map) ->
TmpType = lookup_type(Arg, Map),
t_subtract_list(TmpType, SubtrTypes)
end, [Arg]),
state__store_conj(Arg, sub, SubtrPatVar, S)
end
end,
State4 = handle_guard(Guard, DefinedVars1, State3),
{State5, BodyVar} = traverse(Body, DefinedVars1,
state__set_in_match(State4, false)),
State6 = state__store_conj(TopVar, eq, BodyVar, State5),
Cs = state__cs(State6),
handle_clauses_1(Tail, TopVar, Arg, DefinedVars, State6,
NewSubtrTypes, [Cs|Acc])
catch
throw:error ->
handle_clauses_1(Tail, TopVar, Arg, DefinedVars,
State, NewSubtrTypes, Acc)
end;
handle_clauses_1([], _TopVar, _Arg, _DefinedVars, State, _SubtrType, Acc) ->
{state__new_constraint_context(State), Acc}.
-spec get_safe_underapprox([cerl:c_values()], cerl:cerl()) -> erl_types:erl_type().
get_safe_underapprox(Pats, Guard) ->
try
Map1 = cerl_trees:fold(fun(X, Acc) ->
case cerl:is_c_var(X) of
true ->
dict:store(cerl_trees:get_label(X), t_any(),
Acc);
false -> Acc
end
end, dict:new(), cerl:c_values(Pats)),
{Type, Map2} = get_underapprox_from_guard(Guard, Map1),
Map3 = case t_is_none(t_inf(t_from_term(true), Type)) of
true -> throw(dont_know);
false ->
case cerl:is_c_var(Guard) of
false -> Map2;
true ->
dict:store(cerl_trees:get_label(Guard),
t_from_term(true), Map2)
end
end,
{Ts, _Map4} = get_safe_underapprox_1(Pats, [], Map3),
t_product(Ts)
catch
throw:dont_know -> t_none()
end.
get_underapprox_from_guard(Tree, Map) ->
True = t_from_term(true),
case cerl:type(Tree) of
call ->
case {cerl:concrete(cerl:call_module(Tree)),
cerl:concrete(cerl:call_name(Tree)),
length(cerl:call_args(Tree))} of
{erlang, is_function, 2} ->
[Fun, Arity] = cerl:call_args(Tree),
case cerl:is_c_int(Arity) of
false -> throw(dont_know);
true ->
{FunType, Map1} = get_underapprox_from_guard(Fun, Map),
Inf = t_inf(FunType, t_fun(cerl:int_val(Arity), t_any())),
case t_is_none(Inf) of
true -> throw(dont_know);
false ->
{True, dict:store(cerl_trees:get_label(Fun), Inf, Map1)}
end
end;
MFA ->
case get_type_test(MFA) of
{ok, Type} ->
[Arg] = cerl:call_args(Tree),
{ArgType, Map1} = get_underapprox_from_guard(Arg, Map),
Inf = t_inf(Type, ArgType),
case t_is_none(Inf) of
true -> throw(dont_know);
false ->
case cerl:is_literal(Arg) of
true -> {True, Map1};
false ->
{True, dict:store(cerl_trees:get_label(Arg), Inf, Map1)}
end
end;
error ->
case MFA of
{erlang, '=:=', 2} -> throw(dont_know);
{erlang, '==', 2} -> throw(dont_know);
{erlang, 'and', 2} ->
[Arg1, Arg2] = cerl:call_args(Tree),
case ((cerl:is_c_var(Arg1) orelse cerl:is_literal(Arg1))
andalso
(cerl:is_c_var(Arg2) orelse cerl:is_literal(Arg2))) of
true ->
{Arg1Type, _} = get_underapprox_from_guard(Arg1, Map),
{Arg2Type, _} = get_underapprox_from_guard(Arg2, Map),
case (t_is_equal(True, Arg1Type) andalso
t_is_equal(True, Arg2Type)) of
true -> {True, Map};
false -> throw(dont_know)
end;
false ->
throw(dont_know)
end;
{erlang, 'or', 2} -> throw(dont_know);
_ -> throw(dont_know)
end
end
end;
var ->
Type =
case dict:find(cerl_trees:get_label(Tree), Map) of
error -> throw(dont_know);
{ok, T} -> T
end,
{Type, Map};
literal ->
case cerl:unfold_literal(Tree) of
Tree ->
Type =
case cerl:concrete(Tree) of
Int when is_integer(Int) -> t_from_term(Int);
Atom when is_atom(Atom) -> t_from_term(Atom);
_Other -> throw(dont_know)
end,
{Type, Map};
OtherTree ->
get_underapprox_from_guard(OtherTree, Map)
end;
_ ->
throw(dont_know)
end.
%%
%% The guard test {erlang, is_function, 2} is handled specially by the
%% function get_underapprox_from_guard/2
%%
get_type_test({erlang, is_atom, 1}) -> {ok, t_atom()};
get_type_test({erlang, is_boolean, 1}) -> {ok, t_boolean()};
get_type_test({erlang, is_binary, 1}) -> {ok, t_binary()};
get_type_test({erlang, is_bitstring, 1}) -> {ok, t_bitstr()};
get_type_test({erlang, is_float, 1}) -> {ok, t_float()};
get_type_test({erlang, is_function, 1}) -> {ok, t_fun()};
get_type_test({erlang, is_integer, 1}) -> {ok, t_integer()};
get_type_test({erlang, is_list, 1}) -> {ok, t_list()};
get_type_test({erlang, is_number, 1}) -> {ok, t_number()};
get_type_test({erlang, is_pid, 1}) -> {ok, t_pid()};
get_type_test({erlang, is_port, 1}) -> {ok, t_port()};
%% get_type_test({erlang, is_record, 2}) -> {ok, t_tuple()};
%% get_type_test({erlang, is_record, 3}) -> {ok, t_tuple()};
get_type_test({erlang, is_reference, 1}) -> {ok, t_reference()};
get_type_test({erlang, is_tuple, 1}) -> {ok, t_tuple()};
get_type_test({M, F, A}) when is_atom(M), is_atom(F), is_integer(A) -> error.
bitstr_constr(SizeType, UnitVal) ->
fun(Map) ->
TmpSizeType = lookup_type(SizeType, Map),
case t_is_subtype(TmpSizeType, t_non_neg_integer()) of
true ->
case t_number_vals(TmpSizeType) of
[OneSize] -> t_bitstr(0, OneSize * UnitVal);
_ ->
MinSize = erl_types:number_min(TmpSizeType),
t_bitstr(UnitVal, MinSize * UnitVal)
end;
false ->
t_bitstr(UnitVal, 0)
end
end.
bitstr_val_constr(SizeType, UnitVal, Flags) ->
fun(Map) ->
TmpSizeType = lookup_type(SizeType, Map),
case t_is_subtype(TmpSizeType, t_non_neg_integer()) of
true ->
case erl_types:number_max(TmpSizeType) of
N when is_integer(N), N < 128 -> %% Avoid illegal arithmetic
TotalSizeVal = N * UnitVal,
{RangeMin, RangeMax} =
case lists:member(signed, Flags) of
true -> {-(1 bsl (TotalSizeVal - 1)),
1 bsl (TotalSizeVal - 1) - 1};
false -> {0, 1 bsl TotalSizeVal - 1}
end,
t_from_range(RangeMin, RangeMax);
_ ->
t_integer()
end;
false ->
t_integer()
end
end.
get_safe_underapprox_1([Pat|Left], Acc, Map) ->
case cerl:type(Pat) of
alias ->
APat = cerl:alias_pat(Pat),
AVar = cerl:alias_var(Pat),
{[VarType], Map1} = get_safe_underapprox_1([AVar], [], Map),
{[PatType], Map2} = get_safe_underapprox_1([APat], [], Map1),
Inf = t_inf(VarType, PatType),
case t_is_none(Inf) of
true -> throw(dont_know);
false ->
Map3 = dict:store(cerl_trees:get_label(AVar), Inf, Map2),
get_safe_underapprox_1(Left, [Inf|Acc], Map3)
end;
binary ->
%% TODO: Can maybe do something here
throw(dont_know);
cons ->
{[Hd, Tl], Map1} =
get_safe_underapprox_1([cerl:cons_hd(Pat), cerl:cons_tl(Pat)], [], Map),
case t_is_any(Tl) of
true -> get_safe_underapprox_1(Left, [t_nonempty_list(Hd)|Acc], Map1);
false -> throw(dont_know)
end;
literal ->
case cerl:unfold_literal(Pat) of
Pat ->
Type =
case cerl:concrete(Pat) of
Int when is_integer(Int) -> t_from_term(Int);
Atom when is_atom(Atom) -> t_from_term(Atom);
[] -> t_from_term([]);
_Other -> throw(dont_know)
end,
get_safe_underapprox_1(Left, [Type|Acc], Map);
OtherPat ->
get_safe_underapprox_1([OtherPat|Left], Acc, Map)
end;
tuple ->
Es = cerl:tuple_es(Pat),
{Ts, Map1} = get_safe_underapprox_1(Es, [], Map),
Type = t_tuple(Ts),
get_safe_underapprox_1(Left, [Type|Acc], Map1);
values ->
Es = cerl:values_es(Pat),
{Ts, Map1} = get_safe_underapprox_1(Es, [], Map),
Type = t_product(Ts),
get_safe_underapprox_1(Left, [Type|Acc], Map1);
var ->
case dict:find(cerl_trees:get_label(Pat), Map) of
error -> throw(dont_know);
{ok, VarType} -> get_safe_underapprox_1(Left, [VarType|Acc], Map)
end
end;
get_safe_underapprox_1([], Acc, Map) ->
{lists:reverse(Acc), Map}.
%%----------------------------------------
%% Guards
%%
handle_guard(Guard, DefinedVars, State) ->
True = t_from_term(true),
State1 = state__set_in_guard(State, true),
State2 = state__new_constraint_context(State1),
{State3, Return} = traverse(Guard, DefinedVars, State2),
State4 = state__store_conj(Return, eq, True, State3),
Cs = state__cs(State4),
NewCs = mk_disj_norm_form(Cs),
OldCs = state__cs(State),
State5 = state__set_in_guard(State4, state__is_in_guard(State)),
State6 = state__new_constraint_context(State5),
state__store_conj(mk_conj_constraint_list([OldCs, NewCs]), State6).
%%=============================================================================
%%
%% BIF constraints
%%
%%=============================================================================
get_bif_constr({erlang, Op, 2}, Dst, Args = [Arg1, Arg2], _State)
when Op =:= '+'; Op =:= '-'; Op =:= '*' ->
ReturnType = ?mk_fun_var(fun(Map) ->
TmpArgTypes = lookup_type_list(Args, Map),
erl_bif_types:type(erlang, Op, 2, TmpArgTypes)
end, Args),
ArgFun =
fun(A, Pos) ->
F =
fun(Map) ->
DstType = lookup_type(Dst, Map),
AType = lookup_type(A, Map),
case t_is_integer(DstType) of
true ->
case t_is_integer(AType) of
true ->
eval_inv_arith(Op, Pos, DstType, AType);
false ->
%% This must be temporary.
t_integer()
end;
false ->
case t_is_float(DstType) of
true ->
case t_is_integer(AType) of
true -> t_float();
false -> t_number()
end;
false ->
t_number()
end
end
end,
?mk_fun_var(F, [Dst, A])
end,
Arg1FunVar = ArgFun(Arg2, 2),
Arg2FunVar = ArgFun(Arg1, 1),
mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType),
mk_constraint(Arg1, sub, Arg1FunVar),
mk_constraint(Arg2, sub, Arg2FunVar)]);
get_bif_constr({erlang, Op, 2}, Dst, [Arg1, Arg2] = Args, _State)
when Op =:= '<'; Op =:= '=<'; Op =:= '>'; Op =:= '>=' ->
ArgFun =
fun(LocalArg1, LocalArg2, LocalOp) ->
fun(Map) ->
DstType = lookup_type(Dst, Map),
IsTrue = t_is_atom(true, DstType),
IsFalse = t_is_atom(false, DstType),
case IsTrue orelse IsFalse of
true ->
Arg1Type = lookup_type(LocalArg1, Map),
Arg2Type = lookup_type(LocalArg2, Map),
case t_is_integer(Arg1Type) andalso t_is_integer(Arg2Type) of
true ->
Max1 = erl_types:number_max(Arg1Type),
Min1 = erl_types:number_min(Arg1Type),
Max2 = erl_types:number_max(Arg2Type),
Min2 = erl_types:number_min(Arg2Type),
case LocalOp of
'=<' ->
if IsTrue -> t_from_range(Min1, Max2);
IsFalse -> t_from_range(range_inc(Min2), Max1)
end;
'<' ->
if IsTrue -> t_from_range(Min1, range_dec(Max2));
IsFalse -> t_from_range(Min2, Max1)
end;
'>=' ->
if IsTrue -> t_from_range(Min2, Max1);
IsFalse -> t_from_range(Min1, range_dec(Max2))
end;
'>' ->
if IsTrue -> t_from_range(range_inc(Min2), Max1);
IsFalse -> t_from_range(Min1, Max2)
end
end;
false -> t_any()
end;
false -> t_any()
end
end
end,
{Arg1Fun, Arg2Fun} =
case Op of
'<' -> {ArgFun(Arg1, Arg2, '<'), ArgFun(Arg2, Arg1, '>=')};
'=<' -> {ArgFun(Arg1, Arg2, '=<'), ArgFun(Arg2, Arg1, '>=')};
'>' -> {ArgFun(Arg1, Arg2, '>'), ArgFun(Arg2, Arg1, '<')};
'>=' -> {ArgFun(Arg1, Arg2, '>='), ArgFun(Arg2, Arg1, '=<')}
end,
DstArgs = [Dst, Arg1, Arg2],
Arg1Var = ?mk_fun_var(Arg1Fun, DstArgs),
Arg2Var = ?mk_fun_var(Arg2Fun, DstArgs),
DstVar = ?mk_fun_var(fun(Map) ->
TmpArgTypes = lookup_type_list(Args, Map),
erl_bif_types:type(erlang, Op, 2, TmpArgTypes)
end, Args),
mk_conj_constraint_list([mk_constraint(Dst, sub, DstVar),
mk_constraint(Arg1, sub, Arg1Var),
mk_constraint(Arg2, sub, Arg2Var)]);
get_bif_constr({erlang, '++', 2}, Dst, [Hd, Tl] = Args, _State) ->
HdFun = fun(Map) ->
DstType = lookup_type(Dst, Map),
case t_is_cons(DstType) of
true -> t_list(t_cons_hd(DstType));
false ->
case t_is_list(DstType) of
true ->
case t_is_nil(DstType) of
true -> DstType;
false -> t_list(t_list_elements(DstType))
end;
false -> t_list()
end
end
end,
TlFun = fun(Map) ->
DstType = lookup_type(Dst, Map),
case t_is_cons(DstType) of
true -> t_sup(t_cons_tl(DstType), DstType);
false ->
case t_is_list(DstType) of
true ->
case t_is_nil(DstType) of
true -> DstType;
false -> t_list(t_list_elements(DstType))
end;
false -> t_any()
end
end
end,
DstL = [Dst],
HdVar = ?mk_fun_var(HdFun, DstL),
TlVar = ?mk_fun_var(TlFun, DstL),
ArgTypes = erl_bif_types:arg_types(erlang, '++', 2),
ReturnType = ?mk_fun_var(fun(Map) ->
TmpArgTypes = lookup_type_list(Args, Map),
erl_bif_types:type(erlang, '++', 2, TmpArgTypes)
end, Args),
Cs = mk_constraints(Args, sub, ArgTypes),
mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType),
mk_constraint(Hd, sub, HdVar),
mk_constraint(Tl, sub, TlVar)
|Cs]);
get_bif_constr({erlang, is_atom, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_atom(), State);
get_bif_constr({erlang, is_binary, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_binary(), State);
get_bif_constr({erlang, is_bitstring, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_bitstr(), State);
get_bif_constr({erlang, is_boolean, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_boolean(), State);
get_bif_constr({erlang, is_float, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_float(), State);
get_bif_constr({erlang, is_function, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_fun(), State);
get_bif_constr({erlang, is_function, 2}, Dst, [Fun, Arity], _State) ->
ArgFun = fun(Map) ->
DstType = lookup_type(Dst, Map),
case t_is_atom(true, DstType) of
true ->
ArityType = lookup_type(Arity, Map),
case t_number_vals(ArityType) of
unknown -> t_fun();
Vals -> t_sup([t_fun(X, t_any()) || X <- Vals])
end;
false -> t_any()
end
end,
ArgV = ?mk_fun_var(ArgFun, [Dst, Arity]),
mk_conj_constraint_list([mk_constraint(Dst, sub, t_boolean()),
mk_constraint(Arity, sub, t_integer()),
mk_constraint(Fun, sub, ArgV)]);
get_bif_constr({erlang, is_integer, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_integer(), State);
get_bif_constr({erlang, is_list, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_maybe_improper_list(), State);
get_bif_constr({erlang, is_number, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_number(), State);
get_bif_constr({erlang, is_pid, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_pid(), State);
get_bif_constr({erlang, is_port, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_port(), State);
get_bif_constr({erlang, is_reference, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_reference(), State);
get_bif_constr({erlang, is_record, 2}, Dst, [Var, Tag] = Args, _State) ->
ArgFun = fun(Map) ->
case t_is_atom(true, lookup_type(Dst, Map)) of
true -> t_tuple();
false -> t_any()
end
end,
ArgV = ?mk_fun_var(ArgFun, [Dst]),
DstFun = fun(Map) ->
TmpArgTypes = lookup_type_list(Args, Map),
erl_bif_types:type(erlang, is_record, 2, TmpArgTypes)
end,
DstV = ?mk_fun_var(DstFun, Args),
mk_conj_constraint_list([mk_constraint(Dst, sub, DstV),
mk_constraint(Tag, sub, t_atom()),
mk_constraint(Var, sub, ArgV)]);
get_bif_constr({erlang, is_record, 3}, Dst, [Var, Tag, Arity] = Args, State) ->
%% TODO: Revise this to make it precise for Tag and Arity.
Records = State#state.records,
AllOpaques = State#state.opaques,
ArgFun =
fun(Map) ->
case t_is_atom(true, lookup_type(Dst, Map)) of
true ->
ArityType = lookup_type(Arity, Map),
case t_is_integer(ArityType) of
true ->
case t_number_vals(ArityType) of
[ArityVal] ->
TagType = lookup_type(Tag, Map),
case t_is_atom(TagType) of
true ->
AnyElems = lists:duplicate(ArityVal-1, t_any()),
GenRecord = t_tuple([TagType|AnyElems]),
case t_atom_vals(TagType) of
[TagVal] ->
case lookup_record(Records, TagVal, ArityVal - 1) of
{ok, Type} ->
case t_opaque_match_record(Type, AllOpaques) of
[Opaque] -> Opaque;
_ -> Type
end;
error -> GenRecord
end;
_ -> GenRecord
end;
false -> t_tuple(ArityVal)
end;
_ -> t_tuple()
end;
false -> t_tuple()
end;
false -> t_any()
end
end,
ArgV = ?mk_fun_var(ArgFun, [Tag, Arity, Dst]),
DstFun = fun(Map) ->
[TmpVar, TmpTag, TmpArity] = TmpArgTypes = lookup_type_list(Args, Map),
TmpArgTypes2 =
case lists:member(TmpVar, AllOpaques) of
true ->
case t_is_integer(TmpArity) of
true ->
case t_number_vals(TmpArity) of
[TmpArityVal] ->
case t_is_atom(TmpTag) of
true ->
case t_atom_vals(TmpTag) of
[TmpTagVal] ->
case lookup_record(Records, TmpTagVal,
TmpArityVal - 1) of
{ok, TmpType} ->
case t_is_none(t_inf(TmpType, TmpVar, opaque)) of
true -> TmpArgTypes;
false -> [TmpType, TmpTag, TmpArity]
end;
error -> TmpArgTypes
end;
_ -> TmpArgTypes
end;
false -> TmpArgTypes
end;
_ -> TmpArgTypes
end;
false -> TmpArgTypes
end;
false -> TmpArgTypes
end,
erl_bif_types:type(erlang, is_record, 3, TmpArgTypes2)
end,
DstV = ?mk_fun_var(DstFun, Args),
mk_conj_constraint_list([mk_constraint(Dst, sub, DstV),
mk_constraint(Arity, sub, t_integer()),
mk_constraint(Tag, sub, t_atom()),
mk_constraint(Var, sub, ArgV)]);
get_bif_constr({erlang, is_tuple, 1}, Dst, [Arg], State) ->
get_bif_test_constr(Dst, Arg, t_tuple(), State);
get_bif_constr({erlang, 'and', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
True = t_from_term(true),
False = t_from_term(false),
ArgFun = fun(Var) ->
fun(Map) ->
DstType = lookup_type(Dst, Map),
case t_is_atom(true, DstType) of
true -> True;
false ->
case t_is_atom(false, DstType) of
true ->
case t_is_atom(true, lookup_type(Var, Map)) of
true -> False;
false -> t_boolean()
end;
false ->
t_boolean()
end
end
end
end,
DstFun = fun(Map) ->
Arg1Type = lookup_type(Arg1, Map),
case t_is_atom(false, Arg1Type) of
true -> False;
false ->
Arg2Type = lookup_type(Arg2, Map),
case t_is_atom(false, Arg2Type) of
true -> False;
false ->
case (t_is_atom(true, Arg1Type)
andalso t_is_atom(true, Arg2Type)) of
true -> True;
false -> t_boolean()
end
end
end
end,
ArgV1 = ?mk_fun_var(ArgFun(Arg2), [Arg2, Dst]),
ArgV2 = ?mk_fun_var(ArgFun(Arg1), [Arg1, Dst]),
DstV = ?mk_fun_var(DstFun, Args),
mk_conj_constraint_list([mk_constraint(Dst, sub, DstV),
mk_constraint(Arg1, sub, ArgV1),
mk_constraint(Arg2, sub, ArgV2)]);
get_bif_constr({erlang, 'or', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
True = t_from_term(true),
False = t_from_term(false),
ArgFun = fun(Var) ->
fun(Map) ->
DstType = lookup_type(Dst, Map),
case t_is_atom(false, DstType) of
true -> False;
false ->
case t_is_atom(true, DstType) of
true ->
case t_is_atom(false, lookup_type(Var, Map)) of
true -> True;
false -> t_boolean()
end;
false ->
t_boolean()
end
end
end
end,
DstFun = fun(Map) ->
Arg1Type = lookup_type(Arg1, Map),
case t_is_atom(true, Arg1Type) of
true -> True;
false ->
Arg2Type = lookup_type(Arg2, Map),
case t_is_atom(true, Arg2Type) of
true -> True;
false ->
case (t_is_atom(false, Arg1Type)
andalso t_is_atom(false, Arg2Type)) of
true -> False;
false -> t_boolean()
end
end
end
end,
ArgV1 = ?mk_fun_var(ArgFun(Arg2), [Arg2, Dst]),
ArgV2 = ?mk_fun_var(ArgFun(Arg1), [Arg1, Dst]),
DstV = ?mk_fun_var(DstFun, Args),
F = fun(A) ->
try [mk_constraint(A, sub, True)]
catch throw:error -> []
end
end,
Constrs = F(Arg1) ++ F(Arg2),
Disj = mk_disj_constraint_list([mk_constraint(Dst, sub, False)|Constrs]),
mk_conj_constraint_list([mk_constraint(Dst, sub, DstV),
mk_constraint(Arg1, sub, ArgV1),
mk_constraint(Arg2, sub, ArgV2),
Disj]);
get_bif_constr({erlang, 'not', 1}, Dst, [Arg] = Args, _State) ->
True = t_from_term(true),
False = t_from_term(false),
Fun = fun(Var) ->
fun(Map) ->
Type = lookup_type(Var, Map),
case t_is_atom(true, Type) of
true -> False;
false ->
case t_is_atom(false, Type) of
true -> True;
false -> t_boolean()
end
end
end
end,
ArgV = ?mk_fun_var(Fun(Dst), [Dst]),
DstV = ?mk_fun_var(Fun(Arg), Args),
mk_conj_constraint_list([mk_constraint(Arg, sub, ArgV),
mk_constraint(Dst, sub, DstV)]);
get_bif_constr({erlang, '=:=', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
ArgFun =
fun(Self, OtherVar) ->
fun(Map) ->
DstType = lookup_type(Dst, Map),
OtherVarType = lookup_type(OtherVar, Map),
case t_is_atom(true, DstType) of
true -> OtherVarType;
false ->
case t_is_atom(false, DstType) of
true ->
case is_singleton_type(OtherVarType) of
true -> t_subtract(lookup_type(Self, Map), OtherVarType);
false -> t_any()
end;
false ->
t_any()
end
end
end
end,
DstFun = fun(Map) ->
ArgType1 = lookup_type(Arg1, Map),
ArgType2 = lookup_type(Arg2, Map),
case t_is_none(t_inf(ArgType1, ArgType2)) of
true -> t_from_term(false);
false -> t_boolean()
end
end,
DstArgs = [Dst, Arg1, Arg2],
ArgV1 = ?mk_fun_var(ArgFun(Arg1, Arg2), DstArgs),
ArgV2 = ?mk_fun_var(ArgFun(Arg2, Arg1), DstArgs),
DstV = ?mk_fun_var(DstFun, Args),
mk_conj_constraint_list([mk_constraint(Dst, sub, DstV),
mk_constraint(Arg1, sub, ArgV1),
mk_constraint(Arg2, sub, ArgV2)]);
get_bif_constr({erlang, '==', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
DstFun = fun(Map) ->
TmpArgTypes = lookup_type_list(Args, Map),
erl_bif_types:type(erlang, '==', 2, TmpArgTypes)
end,
ArgFun =
fun(Var, Self) ->
fun(Map) ->
VarType = lookup_type(Var, Map),
DstType = lookup_type(Dst, Map),
case is_singleton_non_number_type(VarType) of
true ->
case t_is_atom(true, DstType) of
true -> VarType;
false ->
case t_is_atom(false, DstType) of
true -> t_subtract(lookup_type(Self, Map), VarType);
false -> t_any()
end
end;
false ->
case t_is_atom(true, DstType) of
true ->
case t_is_number(VarType) of
true -> t_number();
false ->
case t_is_atom(VarType) of
true -> VarType;
false -> t_any()
end
end;
false ->
t_any()
end
end
end
end,
DstV = ?mk_fun_var(DstFun, Args),
ArgL = [Arg1, Arg2, Dst],
ArgV1 = ?mk_fun_var(ArgFun(Arg2, Arg1), ArgL),
ArgV2 = ?mk_fun_var(ArgFun(Arg1, Arg2), ArgL),
mk_conj_constraint_list([mk_constraint(Dst, sub, DstV),
mk_constraint(Arg1, sub, ArgV1),
mk_constraint(Arg2, sub, ArgV2)]);
get_bif_constr({erlang, element, 2} = _BIF, Dst, Args,
#state{cs = Constrs, opaques = Opaques}) ->
GenType = erl_bif_types:type(erlang, element, 2),
case t_is_none(GenType) of
true -> ?debug("Bif: ~w failed\n", [_BIF]), throw(error);
false ->
Fun = fun(Map) ->
[I, T] = ATs = lookup_type_list(Args, Map),
ATs2 = case lists:member(T, Opaques) of
true -> [I, erl_types:t_opaque_structure(T)];
false -> ATs
end,
erl_bif_types:type(erlang, element, 2, ATs2)
end,
ReturnType = ?mk_fun_var(Fun, Args),
ArgTypes = erl_bif_types:arg_types(erlang, element, 2),
Cs = mk_constraints(Args, sub, ArgTypes),
NewCs =
case find_element(Args, Constrs) of
'unknown' -> Cs;
Elem -> [mk_constraint(Dst, eq, Elem)|Cs]
end,
mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType)|NewCs])
end;
get_bif_constr({M, F, A} = _BIF, Dst, Args, State) ->
GenType = erl_bif_types:type(M, F, A),
Opaques = State#state.opaques,
case t_is_none(GenType) of
true -> ?debug("Bif: ~w failed\n", [_BIF]), throw(error);
false ->
UnopaqueFun =
fun(T) -> case lists:member(T, Opaques) of
true -> erl_types:t_unopaque(T, [T]);
false -> T
end
end,
ReturnType = ?mk_fun_var(fun(Map) ->
TmpArgTypes0 = lookup_type_list(Args, Map),
TmpArgTypes = [UnopaqueFun(T) || T<- TmpArgTypes0],
erl_bif_types:type(M, F, A, TmpArgTypes)
end, Args),
case erl_bif_types:is_known(M, F, A) of
false ->
case t_is_any(GenType) of
true ->
none;
false ->
mk_constraint(Dst, sub, ReturnType)
end;
true ->
ArgTypes = erl_bif_types:arg_types(M, F, A),
Cs = mk_constraints(Args, sub, ArgTypes),
mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType)|Cs])
end
end.
eval_inv_arith('+', _Pos, Dst, Arg) ->
erl_bif_types:type(erlang, '-', 2, [Dst, Arg]);
eval_inv_arith('*', _Pos, Dst, Arg) ->
case t_number_vals(Arg) of
[0] -> t_integer();
_ ->
TmpRet = erl_bif_types:type(erlang, 'div', 2, [Dst, Arg]),
Zero = t_from_term(0),
%% If 0 is not part of the result, it cannot be part of the argument.
case t_is_subtype(Zero, Dst) of
false -> t_subtract(TmpRet, Zero);
true -> TmpRet
end
end;
eval_inv_arith('-', 1, Dst, Arg) ->
erl_bif_types:type(erlang, '-', 2, [Arg, Dst]);
eval_inv_arith('-', 2, Dst, Arg) ->
erl_bif_types:type(erlang, '+', 2, [Arg, Dst]).
range_inc(neg_inf) -> neg_inf;
range_inc(pos_inf) -> pos_inf;
range_inc(Int) when is_integer(Int) -> Int + 1.
range_dec(neg_inf) -> neg_inf;
range_dec(pos_inf) -> pos_inf;
range_dec(Int) when is_integer(Int) -> Int - 1.
get_bif_test_constr(Dst, Arg, Type, State) ->
ArgFun = fun(Map) ->
DstType = lookup_type(Dst, Map),
case t_is_atom(true, DstType) of
true -> Type;
false -> t_any()
end
end,
ArgV = ?mk_fun_var(ArgFun, [Dst]),
Opaques = State#state.opaques,
DstFun = fun(Map) ->
ArgType = lookup_type(Arg, Map),
case t_is_none(t_inf(ArgType, Type)) of
true ->
case lists:member(ArgType, Opaques) of
true ->
OpaqueStruct = erl_types:t_opaque_structure(ArgType),
case t_is_none(t_inf(OpaqueStruct, Type)) of
true -> t_from_term(false);
false ->
case t_is_subtype(ArgType, Type) of
true -> t_from_term(true);
false -> t_boolean()
end
end;
false -> t_from_term(false)
end;
false ->
case t_is_subtype(ArgType, Type) of
true -> t_from_term(true);
false -> t_boolean()
end
end
end,
DstV = ?mk_fun_var(DstFun, [Arg]),
mk_conj_constraint_list([mk_constraint(Dst, sub, DstV),
mk_constraint(Arg, sub, ArgV)]).
%%=============================================================================
%%
%% Constraint solver.
%%
%%=============================================================================
solve([Fun], State) ->
?debug("============ Analyzing Fun: ~w ===========\n",
[debug_lookup_name(Fun)]),
solve_fun(Fun, map_new(), State);
solve([_|_] = SCC, State) ->
?debug("============ Analyzing SCC: ~w ===========\n",
[[debug_lookup_name(F) || F <- SCC]]),
{Parallel, NewState} =
case parallel_split(SCC) of
false -> {false, State};
SplitSCC -> {SplitSCC, minimize_state(State)}
end,
solve_scc(SCC, Parallel, map_new(), NewState, false).
solve_fun(Fun, FunMap, State) ->
Cs = state__get_cs(Fun, State),
Deps = get_deps(Cs),
Ref = mk_constraint_ref(Fun, Deps),
%% Note that functions are always considered to succeed.
NewMap = solve(Fun, Ref, FunMap, State),
NewType = lookup_type(Fun, NewMap),
NewFunMap1 = case state__get_rec_var(Fun, State) of
error -> FunMap;
{ok, Var} -> enter_type(Var, NewType, FunMap)
end,
enter_type(Fun, NewType, NewFunMap1).
solve_scc(SCC, Parallel, Map, State, TryingUnit) ->
Vars0 = [{Fun, state__get_rec_var(Fun, State)} || Fun <- SCC],
Vars = [Var || {_, {ok, Var}} <- Vars0],
Funs = [Fun || {Fun, {ok, _}} <- Vars0],
Types = unsafe_lookup_type_list(Funs, Map),
RecTypes = [t_limit(Type, ?TYPE_LIMIT) || Type <- Types],
CleanMap = lists:foldl(fun(Fun, AccFunMap) ->
erase_type(t_var_name(Fun), AccFunMap)
end, Map, SCC),
Map1 = enter_type_lists(Vars, RecTypes, CleanMap),
?debug("Checking SCC: ~w\n", [[debug_lookup_name(F) || F <- SCC]]),
FunSet = ordsets:from_list([t_var_name(F) || F <- SCC]),
Map2 =
case Parallel of
false -> solve_whole_scc(SCC, Map1, State);
SplitSCC -> solve_whole_scc_parallel(SplitSCC, Map1, State)
end,
case maps_are_equal(Map2, Map, FunSet) of
true ->
?debug("SCC ~w reached fixpoint\n", [SCC]),
NewTypes = unsafe_lookup_type_list(Funs, Map2),
case erl_types:any_none([t_fun_range(T) || T <- NewTypes])
andalso TryingUnit =:= false of
true ->
UnitTypes =
[case t_is_none(t_fun_range(T)) of
false -> T;
true -> t_fun(t_fun_args(T), t_unit())
end || T <- NewTypes],
Map3 = enter_type_lists(Funs, UnitTypes, Map2),
solve_scc(SCC, Parallel, Map3, State, true);
false ->
case Parallel of
false -> true;
_ -> dispose_state(State)
end,
Map2
end;
false ->
?debug("SCC ~w did not reach fixpoint\n", [SCC]),
solve_scc(SCC, Parallel, Map2, State, TryingUnit)
end.
solve_whole_scc(SCC, Map, State) ->
SolveFun = fun(X, Y) -> scc_fold_fun(X, Y, State) end,
lists:foldl(SolveFun, Map, SCC).
%%------------------------------------------------------------------------------
-define(worth_it, 42).
parallel_split(SCC) ->
Length = length(SCC),
case Length > 2*?worth_it of
false -> false;
true ->
case min(dialyzer_utils:parallelism(), 8) of
1 -> false;
CPUs ->
FullShare = Length div CPUs + 1,
Unit = max(FullShare, ?worth_it),
split(SCC, Unit, [])
end
end.
minimize_state(#state{
cmap = {d, CMap},
fun_map = FunMap,
fun_arities = FunArities,
self_rec = SelfRec,
prop_types = {d, PropTypes},
opaques = Opaques,
solvers = Solvers
}) ->
ETSCMap = ets:new(cmap,[{read_concurrency, true}]),
ETSPropTypes = ets:new(prop_types,[{read_concurrency, true}]),
true = ets:insert(ETSCMap, dict:to_list(CMap)),
true = ets:insert(ETSPropTypes, dict:to_list(PropTypes)),
#state
{cmap = {e, ETSCMap},
fun_map = FunMap,
fun_arities = FunArities,
self_rec = SelfRec,
prop_types = {e, ETSPropTypes},
opaques = Opaques,
solvers = Solvers
}.
dispose_state(#state{cmap = {e, ETSCMap},
prop_types = {e, ETSPropTypes}}) ->
true = ets:delete(ETSCMap),
true = ets:delete(ETSPropTypes).
solve_whole_scc_parallel(SplitSCC, Map, State) ->
Workers = spawn_workers(SplitSCC, Map, State),
wait_results(Workers, Map, fold_res_fun(State)).
spawn_workers(SplitSCC, Map, State) ->
Spawner = solve_scc_spawner(self(), Map, State),
lists:foreach(Spawner, SplitSCC),
length(SplitSCC).
wait_results(0, Map, _FoldResFun) ->
Map;
wait_results(Pending, Map, FoldResFun) ->
Res = receive_scc_result(),
NewMap = lists:foldl(FoldResFun, Map, Res),
wait_results(Pending-1, NewMap, FoldResFun).
solve_scc_spawner(Parent, Map, State) ->
fun(SCCPart) ->
spawn_link(fun() -> solve_scc_worker(Parent, SCCPart, Map, State) end)
end.
split([], _Unit, Acc) ->
Acc;
split(List, Unit, Acc) ->
{Taken, Rest} =
try
lists:split(Unit, List)
catch
_:_ -> {List, []}
end,
split(Rest, Unit, [Taken|Acc]).
solve_scc_worker(Parent, SCCPart, Map, State) ->
SolveFun = fun(X, Y) -> scc_fold_fun(X, Y, State) end,
FinalMap = lists:foldl(SolveFun, Map, SCCPart),
Res =
[{F, t_limit(unsafe_lookup_type(F, FinalMap), ?TYPE_LIMIT)} ||
F <- SCCPart],
send_scc_result(Parent, Res).
fold_res_fun(State) ->
fun({F, Type}, Map) ->
case state__get_rec_var(F, State) of
{ok, R} ->
enter_type(R, Type, enter_type(F, Type, Map));
error ->
enter_type(F, Type, Map)
end
end.
receive_scc_result() ->
receive
{scc_fun, Res} -> Res
end.
send_scc_result(Parent, Res) ->
Parent ! {scc_fun, Res}.
%%------------------------------------------------------------------------------
scc_fold_fun(F, FunMap, State) ->
Deps = get_deps(state__get_cs(F, State)),
Cs = mk_constraint_ref(F, Deps),
%% Note that functions are always considered to succeed.
Map = solve(F, Cs, FunMap, State),
NewType0 = unsafe_lookup_type(F, Map),
NewType = t_limit(NewType0, ?TYPE_LIMIT),
NewFunMap = case state__get_rec_var(F, State) of
{ok, R} ->
enter_type(R, NewType, enter_type(F, NewType, FunMap));
error ->
enter_type(F, NewType, FunMap)
end,
?debug("Done solving for function ~w :: ~s\n", [debug_lookup_name(F),
format_type(NewType)]),
NewFunMap.
solve(Fun, Cs, FunMap, State) ->
Solvers = State#state.solvers,
R = [solver(S, solve_fun(S, Fun, Cs, FunMap, State)) || S <- Solvers],
check_solutions(R, Fun, no_solver, no_map).
solver(Solver, SolveFun) ->
?debug("Start solver ~w\n", [Solver]),
try timer:tc(SolveFun) of
{Time, {ok, Map}} ->
?debug("End solver ~w (~w microsecs)\n", [Solver, Time]),
{Solver, Map, Time};
{_, _R} ->
?debug("Solver ~w returned unexpected result:\n ~P\n",
[Solver, _R, 60]),
throw(error)
catch E:R ->
io:format("Solver ~w failed: ~w:~p\n ~p\n",
[Solver, E, R, erlang:get_stacktrace()]),
throw(error)
end.
solve_fun(v1, _Fun, Cs, FunMap, State) ->
fun() ->
{ok, _MapDict, NewMap} = solve_ref_or_list(Cs, FunMap, dict:new(), State),
{ok, NewMap}
end;
solve_fun(v2, Fun, _Cs, FunMap, State) ->
fun() -> v2_solve_ref(Fun, FunMap, State) end.
check_solutions([], _Fun, _S, Map) ->
Map;
check_solutions([{S1,Map1,_Time1}|Maps], Fun, S, Map) ->
?debug("Solver ~w needed ~w microsecs\n", [S1, _Time1]),
case Map =:= no_map orelse sane_maps(Map, Map1, [Fun], S, S1) of
true ->
check_solutions(Maps, Fun, S1, Map1);
false ->
?debug("Constraint solvers do not agree on ~w\n", [Fun]),
pp_map(atom_to_list(S), Map),
pp_map(atom_to_list(S1), Map1),
io:format("A bug was found. Please report it, and use the option "
"`--solver v1' until the bug has been fixed.\n"),
throw(error)
end.
sane_maps(Map1, Map2, Keys, _S1, _S2) ->
lists:all(fun(Key) ->
V1 = unsafe_lookup_type(Key, Map1),
V2 = unsafe_lookup_type(Key, Map2),
case t_is_equal(V1, V2) of
true -> true;
false ->
?debug("Constraint solvers do not agree on ~w\n", [Key]),
?debug("~w: ~s\n",
[_S1, format_type(unsafe_lookup_type(Key, Map1))]),
?debug("~w: ~s\n",
[_S2, format_type(unsafe_lookup_type(Key, Map2))]),
false
end
end, Keys).
%% Solver v2
-record(v2_state, {constr_data = dict:new() :: dict(),
state :: #state{}}).
v2_solve_ref(Fun, Map, State) ->
V2State = #v2_state{state = State},
{ok, NewMap, _, _} = v2_solve_reference(Fun, Map, V2State),
{ok, NewMap}.
v2_solve(#constraint{}=C, Map, V2State) ->
State = V2State#v2_state.state,
case solve_one_c(C, Map, State#state.opaques) of
error ->
report_failed_constraint(C, Map),
{error, V2State};
{ok, {NewMap, U}} ->
{ok, NewMap, V2State, U}
end;
v2_solve(#constraint_list{type = disj}=C, Map, V2State) ->
v2_solve_disjunct(C, Map, V2State);
v2_solve(#constraint_list{type = conj}=C, Map, V2State) ->
v2_solve_conjunct(C, Map, V2State);
v2_solve(#constraint_ref{id = Id}, Map, V2State) ->
v2_solve_reference(Id, Map, V2State).
v2_solve_reference(Id, Map, V2State0) ->
?debug("Checking ref to fun: ~w\n", [debug_lookup_name(Id)]),
pp_map("Map", Map),
pp_constr_data("solve_ref", V2State0),
Map1 = restore_local_map(V2State0, Id, Map),
State = V2State0#v2_state.state,
Cs = state__get_cs(Id, State),
Res =
case state__is_self_rec(Id, State) of
true -> v2_solve_self_recursive(Cs, Map1, Id, t_none(), V2State0);
false -> v2_solve(Cs, Map1, V2State0)
end,
{FunType, V2State} =
case Res of
{error, V2State1} ->
?debug("Error solving for function ~p\n", [debug_lookup_name(Id)]),
Arity = state__fun_arity(Id, State),
FunType0 =
case state__prop_domain(t_var_name(Id), State) of
error -> t_fun(Arity, t_none());
{ok, Dom} -> t_fun(Dom, t_none())
end,
{FunType0, V2State1};
{ok, NewMap, V2State1, U} ->
?debug("Done solving fun: ~p\n", [debug_lookup_name(Id)]),
FunType0 = lookup_type(Id, NewMap),
V2State2 = save_local_map(V2State1, Id, U, NewMap),
{FunType0, V2State2}
end,
?debug("ref Id=~w Assigned ~s\n", [Id, format_type(FunType)]),
{NewMap1, U1} = enter_var_type(Id, FunType, Map),
{NewMap2, U2} =
case state__get_rec_var(Id, State) of
{ok, Var} -> enter_var_type(Var, FunType, NewMap1);
error -> {NewMap1, []}
end,
{ok, NewMap2, V2State, lists:umerge(U1, U2)}.
v2_solve_self_recursive(Cs, Map, Id, RecType0, V2State0) ->
?debug("Solving self recursive ~w\n", [debug_lookup_name(Id)]),
State = V2State0#v2_state.state,
{ok, RecVar} = state__get_rec_var(Id, State),
?debug("OldRecType ~s\n", [format_type(RecType0)]),
RecType = t_limit(RecType0, ?TYPE_LIMIT),
{Map1, U0} = enter_var_type(RecVar, RecType, Map),
V2State1 = save_updated_vars1(V2State0, Cs, U0), % Probably not necessary
case v2_solve(Cs, Map1, V2State1) of
{error, _V2State}=Error ->
case t_is_none(RecType0) of
true ->
%% Try again and assume that this is a non-terminating function.
Arity = state__fun_arity(Id, State),
NewRecType = t_fun(lists:duplicate(Arity, t_any()), t_unit()),
v2_solve_self_recursive(Cs, Map, Id, NewRecType, V2State0);
false ->
Error
end;
{ok, NewMap, V2State, U} ->
pp_map("recursive finished", NewMap),
NewRecType = unsafe_lookup_type(Id, NewMap),
case t_is_equal(NewRecType, RecType0) of
true ->
{NewMap2, U1} = enter_var_type(RecVar, NewRecType, NewMap),
{ok, NewMap2, V2State, lists:umerge(U, U1)};
false ->
v2_solve_self_recursive(Cs, Map, Id, NewRecType, V2State0)
end
end.
enter_var_type(Var, Type, Map0) ->
{Map, Vs} = enter_type2(Var, Type, Map0),
{Map, [t_var_name(V) || V <- Vs]}.
v2_solve_disjunct(Disj, Map, V2State0) ->
#constraint_list{type = disj, id = _Id, list = Cs, masks = Masks} = Disj,
?debug("disjunct Id=~w~n", [_Id]),
pp_map("Map", Map),
pp_constr_data("disjunct", V2State0),
case get_flags(V2State0, Disj) of
{V2State1, failed_list} -> {error, V2State1}; % cannot happen
{V2State1, Flags} when Flags =/= [] ->
{ok, V2State, Eval, UL, MapL0, Uneval, Failed} =
v2_solve_disj(Flags, Cs, 1, Map, V2State1, [], [], [], [], false),
?debug("disj ending _Id=~w Eval=~w, |Uneval|=~w |UL|=~w~n",
[_Id, Eval, length(Uneval), length(UL)]),
if Eval =:= [], Uneval =:= [] ->
{error, failed_list(Disj, V2State0)};
true ->
{Is0, UnIds} = lists:unzip(Uneval),
MapL = [restore_local_map(V2State, Id, Map) ||
Id <- UnIds] ++ MapL0,
%% If some branch has just failed every variable of the
%% non-failed branches need to be checked, not just the
%% updated ones.
U0 = case Failed of
false -> lists:umerge(UL);
true -> constrained_keys(MapL)
end,
if U0 =:= [] -> {ok, Map, V2State, []};
true ->
NotFailed = lists:umerge(Is0, Eval),
U1 = [V || V <- U0,
var_occurs_everywhere(V, Masks, NotFailed)],
NewMap = join_maps(U1, MapL, Map),
pp_map("NewMap", NewMap),
U = updated_vars_only(U1, Map, NewMap),
?debug("disjunct finished _Id=~w\n", [_Id]),
{ok, NewMap, V2State, U}
end
end
end.
var_occurs_everywhere(V, Masks, NotFailed) ->
ordsets:is_subset(NotFailed, get_mask(V, Masks)).
v2_solve_disj([I|Is], [C|Cs], I, Map0, V2State0, UL, MapL, Eval, Uneval,
Failed0) ->
Id = C#constraint_list.id,
Map1 = restore_local_map(V2State0, Id, Map0),
case v2_solve(C, Map1, V2State0) of
{error, V2State} ->
?debug("disj error I=~w~n", [I]),
Failed = Failed0 orelse not is_failed_list(C, V2State0),
v2_solve_disj(Is, Cs, I+1, Map0, V2State, UL, MapL, Eval, Uneval, Failed);
{ok, Map, V2State1, U} ->
?debug("disj I=~w U=~w~n", [I, U]),
V2State = save_local_map(V2State1, Id, U, Map),
pp_map("DMap", Map),
v2_solve_disj(Is, Cs, I+1, Map0, V2State, [U|UL], [Map|MapL],
[I|Eval], Uneval, Failed0)
end;
v2_solve_disj([], [], _I, _Map, V2State, UL, MapL, Eval, Uneval, Failed) ->
{ok, V2State, lists:reverse(Eval), UL, MapL, lists:reverse(Uneval), Failed};
v2_solve_disj(Is, [C|Cs], I, Map, V2State, UL, MapL, Eval, Uneval0, Failed) ->
Uneval = [{I,C#constraint_list.id} ||
not is_failed_list(C, V2State)] ++ Uneval0,
v2_solve_disj(Is, Cs, I+1, Map, V2State, UL, MapL, Eval, Uneval, Failed).
save_local_map(#v2_state{constr_data = ConData}=V2State, Id, U, Map) ->
Part0 = [{V,dict:fetch(V, Map)} || V <- U],
Part1 =
case dict:find(Id, ConData) of
error -> []; % cannot happen
{ok, {Part2,[]}} -> Part2
end,
?debug("save local map Id=~w:\n", [Id]),
Part = lists:ukeymerge(1, lists:keysort(1, Part0), Part1),
pp_map("New Part", dict:from_list(Part0)),
pp_map("Old Part", dict:from_list(Part1)),
pp_map(" => Part", dict:from_list(Part)),
V2State#v2_state{constr_data = dict:store(Id, {Part,[]}, ConData)}.
restore_local_map(#v2_state{constr_data = ConData}, Id, Map0) ->
case dict:find(Id, ConData) of
error -> Map0;
{ok, failed} -> Map0;
{ok, {[],_}} -> Map0;
{ok, {Part0,U}} ->
Part = [{K,V} || {K,V} <- Part0, not lists:member(K, U)],
?debug("restore local map Id=~w U=~w\n", [Id, U]),
pp_map("Part", dict:from_list(Part)),
pp_map("Map0", Map0),
Map = lists:foldl(fun({K,V}, D) -> dict:store(K, V, D)end, Map0, Part),
pp_map("Map", Map),
Map
end.
v2_solve_conjunct(Conj, Map, V2State0) ->
#constraint_list{type = conj, list = Cs} = Conj,
?debug("conjunct Id=~w~n", [Conj#constraint_list.id]),
IsFlat = case Cs of [#constraint{}|_] -> true; _ -> false end,
case get_flags(V2State0, Conj) of
{V2State, failed_list} -> {error, V2State};
{V2State, Flags} ->
v2_solve_conj(Flags, Cs, 1, Map, Conj, IsFlat, V2State, [], [], [],
Map, Flags)
end.
%% LastMap and LastFlags are used for loop detection.
v2_solve_conj([I|Is], [Cs|Tail], I, Map0, Conj, IsFlat, V2State0,
UL, NewFs0, VarsUp, LastMap, LastFlags) ->
?debug("conj Id=~w I=~w~n", [Conj#constraint_list.id, I]),
true = IsFlat =:= is_record(Cs, constraint),
pp_constr_data("conj", V2State0),
case v2_solve(Cs, Map0, V2State0) of
{error, V2State1} -> {error, failed_list(Conj, V2State1)};
{ok, Map, V2State1, []} ->
v2_solve_conj(Is, Tail, I+1, Map, Conj, IsFlat, V2State1,
UL, NewFs0, VarsUp, LastMap, LastFlags);
{ok, Map, V2State1, U} when IsFlat -> % optimization
%% It is ensured by enumerate_constraints() that every
%% #constraint{} has a conjunct as parent, and that such a
%% parent has nothing but #constraint{}:s as children, a fact
%% which is used here to simplify the flag calculation.
Mask = lists:umerge([get_mask(V, Conj#constraint_list.masks) || V <- U]),
{Is1, NewF} = add_mask_to_flags(Is, Mask, I, []),
NewFs = [NewF|NewFs0],
v2_solve_conj(Is1, Tail, I+1, Map, Conj, IsFlat, V2State1,
[U|UL], NewFs, VarsUp, LastMap, LastFlags);
{ok, Map, V2State1, U} ->
#constraint_list{masks = Masks, list = AllCs} = Conj,
M = lists:keydelete(I, 1, vars_per_child(U, Masks)),
{V2State2, NewF0} = save_updated_vars_list(AllCs, M, V2State1),
{NewF, F} = lists:splitwith(fun(J) -> J < I end, NewF0),
Is1 = lists:umerge(Is, F),
NewFs = [NewF|NewFs0],
v2_solve_conj(Is1, Tail, I+1, Map, Conj, IsFlat, V2State2,
[U|UL], NewFs, VarsUp, LastMap, LastFlags)
end;
v2_solve_conj([], _Cs, _I, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp,
LastMap, LastFlags) ->
U = lists:umerge(UL),
case lists:umerge(NewFs) of
[] ->
?debug("conjunct finished Id=~w\n", [Conj#constraint_list.id]),
{ok, Map, V2State, lists:umerge([U|VarsUp])};
NewFlags when NewFlags =:= LastFlags, Map =:= LastMap ->
%% A loop was detected! The cause is some bug, possibly in erl_types.
%% The evaluation continues, but the results can be wrong.
report_detected_loop(Conj),
{ok, Map, V2State, lists:umerge([U|VarsUp])};
NewFlags ->
#constraint_list{type = conj, list = Cs} = Conj,
v2_solve_conj(NewFlags, Cs, 1, Map, Conj, IsFlat, V2State,
[], [], [U|VarsUp], Map, NewFlags)
end;
v2_solve_conj(Is, [_|Tail], I, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp,
LastMap, LastFlags) ->
v2_solve_conj(Is, Tail, I+1, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp,
LastMap, LastFlags).
-ifdef(DEBUG_LOOP_DETECTION).
report_detected_loop(Conj) ->
io:format("A loop was detected in ~w\n", [Conj#constraint_list.id]).
-else.
report_detected_loop(_) ->
ok.
-endif.
add_mask_to_flags(Flags, [Im|M], I, L) when I > Im ->
add_mask_to_flags(Flags, M, I, [Im|L]);
add_mask_to_flags(Flags, [_|M], _I, L) ->
{lists:umerge(Flags, M), lists:reverse(L)}.
get_mask(V, {d, Masks}) ->
case dict:find(V, Masks) of
error -> [];
{ok, M} -> M
end;
get_mask(V, Masks) ->
case lists:keyfind(V, 1, Masks) of
false -> [];
{V, M} -> M
end.
get_flags(#v2_state{constr_data = ConData}=V2State0, C) ->
#constraint_list{id = Id, list = Cs, masks = Masks} = C,
case dict:find(Id, ConData) of
error ->
?debug("get_flags Id=~w Flags=all ~w\n", [Id, length(Cs)]),
V2State = V2State0#v2_state{constr_data = dict:store(Id, {[],[]}, ConData)},
{V2State, lists:seq(1, length(Cs))};
{ok, failed} ->
{V2State0, failed_list};
{ok, {Part,U}} when U =/= [] ->
?debug("get_flags Id=~w U=~w\n", [Id, U]),
V2State = V2State0#v2_state{constr_data = dict:store(Id, {Part,[]}, ConData)},
save_updated_vars_list(Cs, vars_per_child(U, Masks), V2State)
end.
vars_per_child(U, Masks) ->
family([{I, V} || V <- lists:usort(U), I <- get_mask(V, Masks)]).
save_updated_vars_list(Cs, IU, V2State) ->
save_updated_vars_list1(Cs, IU, V2State, 1, []).
save_updated_vars_list1([C|Cs], [{I,U}|IU], V2State0, I, Is) ->
V2State = save_updated_vars(C, U, V2State0),
save_updated_vars_list1(Cs, IU, V2State, I+1, [I|Is]);
save_updated_vars_list1([], [], V2State, _I, Is) ->
{V2State, lists:reverse(Is)};
save_updated_vars_list1([_|Cs], IU, V2State, I, Is) ->
save_updated_vars_list1(Cs, IU, V2State, I+1, Is).
save_updated_vars(#constraint{}, _, V2State) ->
V2State;
save_updated_vars(#constraint_list{}=C, U, V2State0) ->
save_updated_vars1(V2State0, C, U);
save_updated_vars(#constraint_ref{id = Id}, U, V2State) ->
Cs = state__get_cs(Id, V2State#v2_state.state),
save_updated_vars(Cs, U, V2State).
save_updated_vars1(V2State, C, U) ->
#v2_state{constr_data = ConData} = V2State,
#constraint_list{id = Id} = C,
case dict:find(Id, ConData) of
error -> V2State; % error means everything is flagged
{ok, failed} -> V2State;
{ok, {Part,U0}} ->
%% Duplicates are not so common; let masks/2 remove them.
U1 = U ++ U0,
V2State#v2_state{constr_data = dict:store(Id, {Part,U1}, ConData)}
end.
-ifdef(DEBUG).
pp_constr_data(_Tag, #v2_state{constr_data = D}) ->
io:format("Constr data at ~p\n", [_Tag]),
_ = [begin
case _PartU of
{_Part, _U} ->
io:format("Id: ~w Vars: ~w\n", [_Id, _U]),
[pp_map("Part", dict:from_list(_Part)) || _Part =/= []];
failed ->
io:format("Id: ~w failed list\n", [_Id])
end
end ||
{_Id, _PartU} <- lists:keysort(1, dict:to_list(D))],
ok.
-else.
pp_constr_data(_Tag, _V2State) ->
ok.
-endif.
failed_list(#constraint_list{id = Id}, #v2_state{constr_data = D}=V2State) ->
?debug("error list ~w~n", [Id]),
V2State#v2_state{constr_data = dict:store(Id, failed, D)}.
is_failed_list(#constraint_list{id = Id}, #v2_state{constr_data = D}) ->
dict:find(Id, D) =:= {ok, failed}.
%% Solver v1
solve_ref_or_list(#constraint_ref{id = Id, deps = Deps},
Map, MapDict, State) ->
{OldLocalMap, Check} =
case dict:find(Id, MapDict) of
error -> {map_new(), false};
{ok, M} -> {M, true}
end,
?debug("Checking ref to fun: ~w\n", [debug_lookup_name(Id)]),
%% Note: mk_constraint_ref() has already removed Id from Deps. The
%% reason for doing it there is that it makes it easy for
%% calculate_masks() to make the corresponding adjustment for
%% version v2.
CheckDeps = ordsets:del_element(t_var_name(Id), Deps),
true = CheckDeps =:= Deps,
case Check andalso maps_are_equal(OldLocalMap, Map, CheckDeps) of
true ->
?debug("Equal\n", []),
{ok, MapDict, Map};
false ->
?debug("Not equal. Solving\n", []),
Cs = state__get_cs(Id, State),
Res =
case state__is_self_rec(Id, State) of
true -> solve_self_recursive(Cs, Map, MapDict, Id, t_none(), State);
false -> solve_ref_or_list(Cs, Map, MapDict, State)
end,
{NewMapDict, FunType} =
case Res of
{error, NewMapDict0} ->
?debug("Error solving for function ~p\n", [debug_lookup_name(Id)]),
Arity = state__fun_arity(Id, State),
FunType0 =
case state__prop_domain(t_var_name(Id), State) of
error -> t_fun(Arity, t_none());
{ok, Dom} -> t_fun(Dom, t_none())
end,
{NewMapDict0, FunType0};
{ok, NewMapDict0, NewMap} ->
?debug("Done solving fun: ~p\n", [debug_lookup_name(Id)]),
FunType0 = lookup_type(Id, NewMap),
{NewMapDict0, FunType0}
end,
?debug(" Id=~w Assigned ~s\n", [Id, format_type(FunType)]),
NewMap1 = enter_type(Id, FunType, Map),
NewMap2 =
case state__get_rec_var(Id, State) of
{ok, Var} -> enter_type(Var, FunType, NewMap1);
error -> NewMap1
end,
{ok, dict:store(Id, NewMap2, NewMapDict), NewMap2}
end;
solve_ref_or_list(#constraint_list{type=Type, list = Cs, deps = Deps, id = Id},
Map, MapDict, State) ->
{OldLocalMap, Check} =
case dict:find(Id, MapDict) of
error -> {map_new(), false};
{ok, M} -> {M, true}
end,
?debug("Checking ref to list: ~w\n", [Id]),
if
OldLocalMap =:= error -> {error, MapDict};
true ->
case Check andalso maps_are_equal(OldLocalMap, Map, Deps) of
true ->
?debug("~w equal ~w\n", [Type, Id]),
{ok, MapDict, Map};
false ->
?debug("~w not equal: ~w. Solving\n", [Type, Id]),
solve_clist(Cs, Type, Id, Deps, MapDict, Map, State)
end
end.
solve_self_recursive(Cs, Map, MapDict, Id, RecType0, State) ->
?debug("Solving self recursive ~w\n", [debug_lookup_name(Id)]),
{ok, RecVar} = state__get_rec_var(Id, State),
?debug("OldRecType ~s\n", [format_type(RecType0)]),
RecType = t_limit(RecType0, ?TYPE_LIMIT),
Map1 = enter_type(RecVar, RecType, erase_type(t_var_name(Id), Map)),
pp_map("Map1", Map1),
case solve_ref_or_list(Cs, Map1, MapDict, State) of
{error, _} = Error ->
case t_is_none(RecType0) of
true ->
%% Try again and assume that this is a non-terminating function.
Arity = state__fun_arity(Id, State),
NewRecType = t_fun(lists:duplicate(Arity, t_any()), t_unit()),
solve_self_recursive(Cs, Map, MapDict, Id, NewRecType, State);
false ->
Error
end;
{ok, NewMapDict, NewMap} ->
pp_map("NewMap", NewMap),
NewRecType = unsafe_lookup_type(Id, NewMap),
case t_is_equal(NewRecType, RecType0) of
true ->
{ok, NewMapDict, enter_type(RecVar, NewRecType, NewMap)};
false ->
solve_self_recursive(Cs, Map, MapDict, Id, NewRecType, State)
end
end.
solve_clist(Cs, conj, Id, Deps, MapDict, Map, State) ->
case solve_cs(Cs, Map, MapDict, State) of
{error, NewMapDict} ->
{error, dict:store(Id, error, NewMapDict)};
{ok, NewMapDict, NewMap} = Ret ->
case Cs of
[_] ->
%% Just a special case for one conjunctive constraint.
Ret;
_ ->
case maps_are_equal(Map, NewMap, Deps) of
true -> {ok, dict:store(Id, NewMap, NewMapDict), NewMap};
false -> solve_clist(Cs, conj, Id, Deps, NewMapDict, NewMap, State)
end
end
end;
solve_clist(Cs, disj, Id, _Deps, MapDict, Map, State) ->
Fun = fun(C, Dict) ->
case solve_ref_or_list(C, Map, Dict, State) of
{ok, NewDict, NewMap} -> {{ok, NewMap}, NewDict};
{error, _NewDict} = Error -> Error
end
end,
{Maps, NewMapDict} = lists:mapfoldl(Fun, MapDict, Cs),
case [X || {ok, X} <- Maps] of
[] -> {error, dict:store(Id, error, NewMapDict)};
MapList ->
NewMap = join_maps(MapList),
{ok, dict:store(Id, NewMap, NewMapDict), NewMap}
end.
solve_cs([#constraint_ref{} = C|Tail], Map, MapDict, State) ->
case solve_ref_or_list(C, Map, MapDict, State) of
{ok, NewMapDict, Map1} -> solve_cs(Tail, Map1, NewMapDict, State);
{error, _NewMapDict} = Error -> Error
end;
solve_cs([#constraint_list{} = C|Tail], Map, MapDict, State) ->
case solve_ref_or_list(C, Map, MapDict, State) of
{ok, NewMapDict, Map1} -> solve_cs(Tail, Map1, NewMapDict, State);
{error, _NewMapDict} = Error -> Error
end;
solve_cs([#constraint{} = C|Tail], Map, MapDict, State) ->
case solve_one_c(C, Map, State#state.opaques) of
error ->
report_failed_constraint(C, Map),
{error, MapDict};
{ok, {NewMap, _U}} ->
solve_cs(Tail, NewMap, MapDict, State)
end;
solve_cs([], Map, MapDict, _State) ->
{ok, MapDict, Map}.
solve_one_c(#constraint{lhs = Lhs, rhs = Rhs, op = Op}, Map, Opaques) ->
LhsType = lookup_type(Lhs, Map),
RhsType = lookup_type(Rhs, Map),
Inf = t_inf(LhsType, RhsType, opaque),
?debug("Solving: ~s :: ~s ~w ~s :: ~s\n\tInf: ~s\n",
[format_type(Lhs), format_type(LhsType), Op,
format_type(Rhs), format_type(RhsType), format_type(Inf)]),
case t_is_none(Inf) of
true -> error;
false ->
case Op of
sub -> solve_subtype(Lhs, Inf, Map, Opaques);
eq ->
case solve_subtype(Lhs, Inf, Map, Opaques) of
error -> error;
{ok, {Map1, U1}} ->
case solve_subtype(Rhs, Inf, Map1, Opaques) of
error -> error;
{ok, {Map2, U2}} -> {ok, {Map2, lists:umerge(U1, U2)}}
end
end
end
end.
solve_subtype(Type, Inf, Map, Opaques) ->
%% case cerl:is_literal(Type) of
%% true ->
%% case t_is_subtype(t_from_term(cerl:concrete(Type)), Inf) of
%% true -> {ok, Map};
%% false -> error
%% end;
%% false ->
try t_unify(Type, Inf, Opaques) of
{_, List} -> {ok, enter_type_list(List, Map)}
catch
throw:{mismatch, _T1, _T2} ->
?debug("Mismatch between ~s and ~s\n",
[format_type(_T1), format_type(_T2)]),
error
end.
%% end.
report_failed_constraint(_C, _Map) ->
?debug("+++++++++++\nFailed: ~s :: ~s ~w ~s :: ~s\n+++++++++++\n",
[format_type(_C#constraint.lhs),
format_type(lookup_type(_C#constraint.lhs, _Map)),
_C#constraint.op,
format_type(_C#constraint.rhs),
format_type(lookup_type(_C#constraint.rhs, _Map))]).
%% ============================================================================
%%
%% Maps and types.
%%
%% ============================================================================
map_new() ->
dict:new().
join_maps([Map]) ->
Map;
join_maps(Maps) ->
Keys = constrained_keys(Maps),
join_maps(Keys, Maps, map_new()).
constrained_keys(Maps) ->
lists:foldl(fun(TmpMap, AccKeys) ->
[Key || Key <- AccKeys, dict:is_key(Key, TmpMap)]
end,
dict:fetch_keys(hd(Maps)), tl(Maps)).
join_maps([Key|Left], Maps = [Map|MapsLeft], AccMap) ->
NewType = join_one_key(Key, MapsLeft, lookup_type(Key, Map)),
NewAccMap = enter_type(Key, NewType, AccMap),
join_maps(Left, Maps, NewAccMap);
join_maps([], _Maps, AccMap) ->
AccMap.
join_one_key(Key, [Map|Maps], Type) ->
case t_is_any(Type) of
true -> Type;
false ->
NewType = lookup_type(Key, Map),
case t_is_equal(NewType, Type) of
true -> join_one_key(Key, Maps, Type);
false -> join_one_key(Key, Maps, t_sup(NewType, Type))
end
end;
join_one_key(_Key, [], Type) ->
Type.
maps_are_equal(Map1, Map2, Deps) ->
NewDeps = prune_keys(Map1, Map2, Deps),
maps_are_equal_1(Map1, Map2, NewDeps).
maps_are_equal_1(Map1, Map2, [H|Tail]) ->
T1 = lookup_type(H, Map1),
T2 = lookup_type(H, Map2),
case t_is_equal(T1, T2) of
true -> maps_are_equal_1(Map1, Map2, Tail);
false ->
?debug("~w: ~s =/= ~s\n", [H, format_type(T1), format_type(T2)]),
false
end;
maps_are_equal_1(_Map1, _Map2, []) ->
true.
-define(PRUNE_LIMIT, 100).
prune_keys(Map1, Map2, Deps) ->
%% This is only worthwhile if the number of deps is reasonably large,
%% and also bigger than the number of elements in the maps.
NofDeps = length(Deps),
case NofDeps > ?PRUNE_LIMIT of
true ->
Keys1 = dict:fetch_keys(Map1),
case length(Keys1) > NofDeps of
true ->
Set1 = lists:sort(Keys1),
Set2 = lists:sort(dict:fetch_keys(Map2)),
ordsets:intersection(ordsets:union(Set1, Set2), Deps);
false ->
Deps
end;
false ->
Deps
end.
enter_type(Key, Val, Map) when is_integer(Key) ->
?debug("Entering ~s :: ~s\n", [format_type(t_var(Key)), format_type(Val)]),
case t_is_any(Val) of
true ->
erase_type(Key, Map);
false ->
LimitedVal = t_limit(Val, ?INTERNAL_TYPE_LIMIT),
case dict:find(Key, Map) of
{ok, LimitedVal} -> Map;
{ok, _} -> map_store(Key, LimitedVal, Map);
error -> map_store(Key, LimitedVal, Map)
end
end;
enter_type(Key, Val, Map) ->
KeyName = t_var_name(Key),
enter_type(KeyName, Val, Map).
enter_type_lists([Key|KeyTail], [Val|ValTail], Map) ->
Map1 = enter_type(Key, Val, Map),
enter_type_lists(KeyTail, ValTail, Map1);
enter_type_lists([], [], Map) ->
Map.
enter_type_list(KeyVals, Map) ->
enter_type_list(KeyVals, Map, []).
enter_type_list([{Key, Val}|Tail], Map, U0) ->
{Map1,U1} = enter_type2(Key, Val, Map),
enter_type_list(Tail, Map1, U1++U0);
enter_type_list([], Map, U) ->
{Map, ordsets:from_list(U)}.
enter_type2(Key, Val, Map) ->
Map1 = enter_type(Key, Val, Map),
{Map1, [Key || not is_same(Key, Map, Map1)]}.
map_store(Key, Val, Map) ->
?debug("Storing ~w :: ~s\n", [Key, format_type(Val)]),
dict:store(Key, Val, Map).
erase_type(Key, Map) ->
dict:erase(Key, Map).
lookup_type_list(List, Map) ->
[lookup_type(X, Map) || X <- List].
unsafe_lookup_type(Key, Map) ->
case dict:find(t_var_name(Key), Map) of
{ok, Type} -> Type;
error -> t_none()
end.
unsafe_lookup_type_list(List, Map) ->
[unsafe_lookup_type(X, Map) || X <- List].
lookup_type(Key, Map) when is_integer(Key) ->
case dict:find(Key, Map) of
error -> t_any();
{ok, Val} -> Val
end;
lookup_type(#fun_var{'fun' = Fun}, Map) ->
Fun(Map);
lookup_type(Key, Map) ->
%% Seems unused and dialyzer complains about it -- commented out.
%% case cerl:is_literal(Key) of
%% true -> t_from_term(cerl:concrete(Key));
%% false ->
t_subst(Key, Map).
%% end.
mk_var(Var) ->
case cerl:is_literal(Var) of
true -> Var;
false ->
case cerl:is_c_values(Var) of
true -> t_product(mk_var_no_lit_list(cerl:values_es(Var)));
false -> t_var(cerl_trees:get_label(Var))
end
end.
mk_var_list(List) ->
[mk_var(X) || X <- List].
mk_var_no_lit(Var) ->
case cerl:is_literal(Var) of
true -> t_from_term(cerl:concrete(Var));
false -> mk_var(Var)
end.
mk_var_no_lit_list(List) ->
[mk_var_no_lit(X) || X <- List].
updated_vars_only(U, OldMap, NewMap) ->
[V || V <- U, not is_same(V, OldMap, NewMap)].
is_same(Key, Map1, Map2) ->
t_is_equal(lookup_type(Key, Map1), lookup_type(Key, Map2)).
pp_map(_S, _Map) ->
?debug("\t~s: ~p\n",
[_S, [{X, lists:flatten(format_type(Y))} ||
{X, Y} <- lists:keysort(1, dict:to_list(_Map))]]).
%% ============================================================================
%%
%% The State.
%%
%% ============================================================================
new_state(SCC0, NextLabel, CallGraph, Plt, PropTypes, Solvers) ->
List = [{MFA, Var} || {MFA, {Var, _Fun}, _Rec} <- SCC0],
NameMap = dict:from_list(List),
MFAs = [MFA || {MFA, _Var} <- List],
SCC = [mk_var(Fun) || {_MFA, {_Var, Fun}, _Rec} <- SCC0],
SelfRec =
case SCC of
[OneF] ->
Label = t_var_name(OneF),
case dialyzer_callgraph:is_self_rec(Label, CallGraph) of
true -> OneF;
false -> false
end;
_Many -> false
end,
#state{callgraph = CallGraph, name_map = NameMap, next_label = NextLabel,
prop_types = {d, PropTypes}, plt = Plt, scc = ordsets:from_list(SCC),
mfas = MFAs, self_rec = SelfRec, solvers = Solvers}.
state__set_rec_dict(State, RecDict) ->
State#state{records = RecDict}.
state__set_opaques(#state{records = RecDict} = State, {M, _F, _A}) ->
Opaques =
erl_types:module_builtin_opaques(M) ++ t_opaque_from_records(RecDict),
State#state{opaques = Opaques, module = M}.
state__set_in_match(State, Bool) ->
State#state{in_match = Bool}.
state__is_in_match(#state{in_match = Bool}) ->
Bool.
state__set_in_guard(State, Bool) ->
State#state{in_guard = Bool}.
state__is_in_guard(#state{in_guard = Bool}) ->
Bool.
state__get_fun_prototype(Op, Arity, State) ->
case t_is_fun(Op) of
true -> {State, Op};
false ->
{State1, [Ret|Args]} = state__mk_vars(Arity+1, State),
Fun = t_fun(Args, Ret),
{State1, Fun}
end.
state__lookup_rec_var_in_scope(MFA, #state{name_map = NameMap}) ->
dict:find(MFA, NameMap).
state__store_fun_arity(Tree, #state{fun_arities = Map} = State) ->
Arity = length(cerl:fun_vars(Tree)),
Id = mk_var(Tree),
State#state{fun_arities = dict:store(Id, Arity, Map)}.
state__fun_arity(Id, #state{fun_arities = Map}) ->
dict:fetch(Id, Map).
state__lookup_undef_var(Tree, #state{callgraph = CG, plt = Plt}) ->
Label = cerl_trees:get_label(Tree),
case dialyzer_callgraph:lookup_rec_var(Label, CG) of
error -> error;
{ok, MFA} ->
case dialyzer_plt:lookup(Plt, MFA) of
none -> error;
{value, {RetType, ArgTypes}} -> {ok, t_fun(ArgTypes, RetType)}
end
end.
state__lookup_apply(Tree, #state{callgraph = Callgraph}) ->
Apply = cerl_trees:get_label(Tree),
case dialyzer_callgraph:lookup_call_site(Apply, Callgraph) of
error ->
unknown;
{ok, List} ->
case lists:member(external, List) of
true -> unknown;
false -> List
end
end.
get_apply_constr(FunLabels, Dst, ArgTypes, #state{callgraph = CG} = State) ->
MFAs = [dialyzer_callgraph:lookup_name(Label, CG) || Label <- FunLabels],
case lists:member(error, MFAs) of
true -> error;
false ->
Constrs0 =
[begin
State1 = state__new_constraint_context(State),
try get_plt_constr(MFA, Dst, ArgTypes, State1) of
State2 -> state__cs(State2)
catch
throw:error -> error
end
end || {ok, MFA} <- MFAs],
case [C || C <- Constrs0, C =/= error] of
[] -> throw(error);
Constrs ->
ApplyConstr = mk_disj_constraint_list(Constrs),
{ok, state__store_conj(ApplyConstr, State)}
end
end.
state__scc(#state{scc = SCC}) ->
SCC.
state__add_fun_to_scc(Fun, #state{scc = SCC} = State) ->
State#state{scc = ordsets:add_element(Fun, SCC)}.
state__plt(#state{plt = PLT}) ->
PLT.
state__new_constraint_context(State) ->
State#state{cs = []}.
state__prop_domain(FunLabel, #state{prop_types = {e, ETSPropTypes}}) ->
try ets:lookup_element(ETSPropTypes, FunLabel, 2) of
{_Range_Fun, Dom} -> {ok, Dom};
FunType -> {ok, t_fun_args(FunType)}
catch
_:_ -> error
end;
state__prop_domain(FunLabel, #state{prop_types = {d, PropTypes}}) ->
case dict:find(FunLabel, PropTypes) of
error -> error;
{ok, {_Range_Fun, Dom}} -> {ok, Dom};
{ok, FunType} -> {ok, t_fun_args(FunType)}
end.
state__add_prop_constrs(Tree, #state{prop_types = {d, PropTypes}} = State) ->
Label = cerl_trees:get_label(Tree),
case dict:find(Label, PropTypes) of
error -> State;
{ok, FunType} ->
case t_fun_args(FunType) of
unknown -> State;
ArgTypes ->
case erl_types:any_none(ArgTypes) of
true -> not_called;
false ->
?debug("Adding propagated constr: ~s for function ~w\n",
[format_type(FunType), debug_lookup_name(mk_var(Tree))]),
FunVar = mk_var(Tree),
state__store_conj(FunVar, sub, FunType, State)
end
end
end.
state__cs(#state{cs = Cs}) ->
mk_conj_constraint_list(Cs).
state__store_conj(C, #state{cs = Cs} = State) ->
State#state{cs = [C|Cs]}.
state__store_conj_list([H|T], State) ->
State1 = state__store_conj(H, State),
state__store_conj_list(T, State1);
state__store_conj_list([], State) ->
State.
state__store_conj(Lhs, Op, Rhs, #state{cs = Cs} = State) ->
State#state{cs = [mk_constraint(Lhs, Op, Rhs)|Cs]}.
state__store_conj_lists(List1, Op, List2, State) ->
{NewList1, NewList2} = strip_of_any_constrs(List1, List2),
state__store_conj_lists_1(NewList1, Op, NewList2, State).
strip_of_any_constrs(List1, List2) ->
strip_of_any_constrs(List1, List2, [], []).
strip_of_any_constrs([T1|Left1], [T2|Left2], Acc1, Acc2) ->
case t_is_any(T1) orelse constraint_opnd_is_any(T2) of
true -> strip_of_any_constrs(Left1, Left2, Acc1, Acc2);
false -> strip_of_any_constrs(Left1, Left2, [T1|Acc1], [T2|Acc2])
end;
strip_of_any_constrs([], [], Acc1, Acc2) ->
{Acc1, Acc2}.
state__store_conj_lists_1([Arg1|Arg1Tail], Op, [Arg2|Arg2Tail], State) ->
State1 = state__store_conj(Arg1, Op, Arg2, State),
state__store_conj_lists_1(Arg1Tail, Op, Arg2Tail, State1);
state__store_conj_lists_1([], _Op, [], State) ->
State.
state__mk_var(#state{next_label = NL} = State) ->
{State#state{next_label = NL+1}, t_var(NL)}.
state__mk_vars(N, #state{next_label = NL} = State) ->
NewLabel = NL + N,
Vars = [t_var(X) || X <- lists:seq(NL, NewLabel-1)],
{State#state{next_label = NewLabel}, Vars}.
state__store_constrs(Id, Cs, #state{cmap = {d, Dict}} = State) ->
NewDict = dict:store(Id, Cs, Dict),
State#state{cmap = {d, NewDict}}.
state__get_cs(Var, #state{cmap = {e, ETSDict}}) ->
ets:lookup_element(ETSDict, Var, 2);
state__get_cs(Var, #state{cmap = {d, Dict}}) ->
dict:fetch(Var, Dict).
state__is_self_rec(Fun, #state{self_rec = SelfRec}) ->
Fun =:= SelfRec.
state__store_funs(Vars0, Funs0, #state{fun_map = Map} = State) ->
debug_make_name_map(Vars0, Funs0),
Vars = mk_var_list(Vars0),
Funs = mk_var_list(Funs0),
NewMap = lists:foldl(fun({Var, Fun}, MP) -> orddict:store(Var, Fun, MP) end,
Map, lists:zip(Vars, Funs)),
State#state{fun_map = NewMap}.
state__get_rec_var(Fun, #state{fun_map = Map}) ->
case [V || {V, FV} <- Map, FV =:= Fun] of
[Var] -> {ok, Var};
[] -> error
end.
state__finalize(State) ->
State1 = enumerate_constraints(State),
order_fun_constraints(State1).
%% ============================================================================
%%
%% Constraints
%%
%% ============================================================================
-spec mk_constraint(erl_types:erl_type(), constr_op(), fvar_or_type()) -> #constraint{}.
mk_constraint(Lhs, Op, Rhs) ->
case t_is_any(Lhs) orelse constraint_opnd_is_any(Rhs) of
false ->
Deps = find_constraint_deps([Lhs, Rhs]),
C0 = mk_constraint_1(Lhs, Op, Rhs),
C = C0#constraint{deps = Deps},
case Deps =:= [] of
true ->
%% This constraint is constant. Solve it immediately.
case solve_one_c(C, map_new(), []) of
error -> throw(error);
_ ->
%% This is always true, keep it anyway for logistic reasons
C
end;
false ->
C
end;
true ->
C = mk_constraint_1(t_any(), Op, t_any()),
C#constraint{deps = []}
end.
%% the following function is used so that we do not call
%% erl_types:t_is_any/1 with a term other than an erl_type()
-spec constraint_opnd_is_any(fvar_or_type()) -> boolean().
constraint_opnd_is_any(#fun_var{}) -> false;
constraint_opnd_is_any(Type) -> t_is_any(Type).
-ifdef(DEBUG).
-spec mk_fun_var(integer(),
fun((_) -> erl_types:erl_type()),
[erl_types:erl_type()]) -> #fun_var{}.
mk_fun_var(Line, Fun, Types) ->
Deps = [t_var_name(Var) || Var <- t_collect_vars(t_product(Types))],
#fun_var{'fun' = Fun, deps = ordsets:from_list(Deps), origin = Line}.
-else.
-spec mk_fun_var(fun((_) -> erl_types:erl_type()), [erl_types:erl_type()]) -> #fun_var{}.
mk_fun_var(Fun, Types) ->
Deps = [t_var_name(Var) || Var <- t_collect_vars(t_product(Types))],
#fun_var{'fun' = Fun, deps = ordsets:from_list(Deps)}.
-endif.
-spec get_deps(constr()) -> [dep()].
get_deps(#constraint{deps = D}) -> D;
get_deps(#constraint_list{deps = D}) -> D;
get_deps(#constraint_ref{deps = D}) -> D.
-spec find_constraint_deps([fvar_or_type()]) -> [dep()].
find_constraint_deps(List) ->
ordsets:from_list(find_constraint_deps(List, [])).
find_constraint_deps([#fun_var{deps = Deps}|Tail], Acc) ->
find_constraint_deps(Tail, [Deps|Acc]);
find_constraint_deps([Type|Tail], Acc) ->
NewAcc = [[t_var_name(D) || D <- t_collect_vars(Type)]|Acc],
find_constraint_deps(Tail, NewAcc);
find_constraint_deps([], Acc) ->
lists:flatten(Acc).
mk_constraint_1(Lhs, eq, Rhs) when Lhs < Rhs ->
#constraint{lhs = Lhs, op = eq, rhs = Rhs};
mk_constraint_1(Lhs, eq, Rhs) ->
#constraint{lhs = Rhs, op = eq, rhs = Lhs};
mk_constraint_1(Lhs, Op, Rhs) ->
#constraint{lhs = Lhs, op = Op, rhs = Rhs}.
mk_constraints([Lhs|LhsTail], Op, [Rhs|RhsTail]) ->
[mk_constraint(Lhs, Op, Rhs)|mk_constraints(LhsTail, Op, RhsTail)];
mk_constraints([], _Op, []) ->
[].
mk_constraint_ref(Id, Deps) ->
%% See also solve_ref_or_list(), #constraint_ref{}.
Ds = ordsets:del_element(t_var_name(Id), Deps),
#constraint_ref{id = Id, deps = Ds}.
mk_constraint_list(Type, List) ->
List1 = ordsets:from_list(lift_lists(Type, List)),
List2 = ordsets:filter(fun(X) -> get_deps(X) =/= [] end, List1),
Deps = calculate_deps(List2),
case Deps =:= [] of
true -> #constraint_list{type = conj,
list = [mk_constraint(t_any(), eq, t_any())],
deps = []};
false -> #constraint_list{type = Type, list = List2, deps = Deps}
end.
lift_lists(Type, List) ->
lift_lists(Type, List, []).
lift_lists(Type, [#constraint_list{type = Type, list = List}|Tail], Acc) ->
lift_lists(Type, Tail, List++Acc);
lift_lists(Type, [C|Tail], Acc) ->
lift_lists(Type, Tail, [C|Acc]);
lift_lists(_Type, [], Acc) ->
Acc.
update_constraint_list(CL, List) ->
CL#constraint_list{list = List}.
%% We expand guard constraints into dijunctive normal form to gain
%% precision in simple guards. However, because of the exponential
%% growth of this expansion in the presens of disjunctions we can even
%% get into trouble while expanding.
%%
%% To limit this we only expand when the number of disjunctions are
%% below a certain limit. This limit is currently set based on the
%% behaviour of boolean 'or'.
%%
%% V1 = V2 or V3
%%
%% Gives us in simplified form the constraints
%%
%% <Some cs> * ((V1 = true) + (V2 = true) + (V1 = false))
%%
%% and thus a three-parted disjunction. If want to allow for two
%% levels of disjunction we need to have 3^2 = 9 disjunctions. If we
%% want three levels we need 3^3 = 27 disjunctions. More than that
%% seems unnecessary and tends to blow up.
%%
%% Note that by not expanding we lose some precision, but we get a
%% safe over approximation.
-define(DISJ_NORM_FORM_LIMIT, 28).
mk_disj_norm_form(#constraint_list{} = CL) ->
try
List1 = expand_to_conjunctions(CL),
mk_disj_constraint_list(List1)
catch
throw:too_many_disj -> CL
end.
expand_to_conjunctions(#constraint_list{type = conj, list = List}) ->
List1 = [C || C <- List, is_simple_constraint(C)],
List2 = [expand_to_conjunctions(C) || #constraint_list{} = C <- List],
case List2 =:= [] of
true -> [mk_conj_constraint_list(List1)];
false ->
case List2 of
[JustOneList] ->
[mk_conj_constraint_list([L|List1]) || L <- JustOneList];
_ ->
combine_conj_lists(List2, List1)
end
end;
expand_to_conjunctions(#constraint_list{type = disj, list = List}) ->
if length(List) > ?DISJ_NORM_FORM_LIMIT -> throw(too_many_disj);
true -> ok
end,
List1 = [C || C <- List, is_simple_constraint(C)],
%% Just an assert.
[] = [C || #constraint{} = C <- List1],
Expanded = lists:flatten([expand_to_conjunctions(C)
|| #constraint_list{} = C <- List]),
ReturnList = Expanded ++ List1,
if length(ReturnList) > ?DISJ_NORM_FORM_LIMIT -> throw(too_many_disj);
true -> ReturnList
end.
is_simple_constraint(#constraint{}) -> true;
is_simple_constraint(#constraint_ref{}) -> true;
is_simple_constraint(#constraint_list{}) -> false.
combine_conj_lists([List1, List2|Left], Prefix) ->
NewList = [mk_conj_constraint_list([L1, L2]) || L1 <- List1, L2 <- List2],
if length(NewList) > ?DISJ_NORM_FORM_LIMIT -> throw(too_many_disj);
true -> ok
end,
combine_conj_lists([NewList|Left], Prefix);
combine_conj_lists([List], Prefix) ->
[mk_conj_constraint_list([mk_conj_constraint_list(Prefix), L]) || L <- List].
calculate_deps(List) ->
calculate_deps(List, []).
calculate_deps([H|Tail], Acc) ->
Deps = get_deps(H),
calculate_deps(Tail, [Deps|Acc]);
calculate_deps([], Acc) ->
ordsets:from_list(lists:flatten(Acc)).
mk_conj_constraint_list(List) ->
mk_constraint_list(conj, List).
mk_disj_constraint_list([NotReallyAList]) ->
NotReallyAList;
mk_disj_constraint_list(List) ->
%% Make sure each element in the list is either a conjunction or a
%% ref. Wrap single constraints into conjunctions.
List1 = [wrap_simple_constr(C) || C <- List],
mk_constraint_list(disj, List1).
wrap_simple_constr(#constraint{} = C) -> mk_conj_constraint_list([C]);
wrap_simple_constr(#constraint_list{} = C) -> C;
wrap_simple_constr(#constraint_ref{} = C) -> C.
enumerate_constraints(State) ->
Cs = [mk_constraint_ref(Id, get_deps(state__get_cs(Id, State)))
|| Id <- state__scc(State)],
{_, _, NewState} = enumerate_constraints(Cs, 0, [], State),
NewState.
enumerate_constraints([#constraint_ref{id = Id} = C|Tail], N, Acc, State) ->
Cs = state__get_cs(Id, State),
{[NewCs], NewN, NewState1} = enumerate_constraints([Cs], N, [], State),
NewState2 = state__store_constrs(Id, NewCs, NewState1),
enumerate_constraints(Tail, NewN+1, [C|Acc], NewState2);
enumerate_constraints([#constraint_list{type = conj, list = List} = C|Tail],
N, Acc, State) ->
%% Separate the flat constraints from the deep ones to make a
%% separate fixpoint iteration over the flat ones for speed.
{Flat, Deep} = lists:partition(fun(#constraint{}) -> true;
(#constraint_list{}) -> false;
(#constraint_ref{}) -> false
end, List),
{NewFlat, N1, State1} = enumerate_constraints(Flat, N, [], State),
{NewDeep, N2, State2} = enumerate_constraints(Deep, N1, [], State1),
{NewList, N3} =
if
NewFlat =:= [] -> {NewDeep, N2};
NewDeep =:= [] -> {NewFlat, N2};
true ->
TmpCList = mk_conj_constraint_list(NewFlat),
{[TmpCList#constraint_list{id = {list, N2}}| NewDeep],
N2 + 1}
end,
NewAcc = [C#constraint_list{list = NewList, id = {list, N3}}|Acc],
enumerate_constraints(Tail, N3+1, NewAcc, State2);
enumerate_constraints([#constraint_list{list = List, type = disj} = C|Tail],
N, Acc, State) ->
{NewList, NewN, NewState} = enumerate_constraints(List, N, [], State),
NewAcc = [C#constraint_list{list = NewList, id = {list, NewN}}|Acc],
enumerate_constraints(Tail, NewN+1, NewAcc, NewState);
enumerate_constraints([#constraint{} = C|Tail], N, Acc, State) ->
enumerate_constraints(Tail, N, [C|Acc], State);
enumerate_constraints([], N, Acc, State) ->
{lists:reverse(Acc), N, State}.
%% Put the fun ref constraints last in any conjunction since we need
%% to separate the environment from the interior of the function.
order_fun_constraints(State) ->
Cs = [mk_constraint_ref(Id, get_deps(state__get_cs(Id, State)))
|| Id <- state__scc(State)],
order_fun_constraints(Cs, State).
order_fun_constraints([#constraint_ref{id = Id}|Tail], State) ->
Cs = state__get_cs(Id, State),
{[NewCs], State1} = order_fun_constraints([Cs], [], [], State),
NewState = state__store_constrs(Id, NewCs, State1),
order_fun_constraints(Tail, NewState);
order_fun_constraints([], State) ->
State.
order_fun_constraints([#constraint_ref{} = C|Tail], Funs, Acc, State) ->
order_fun_constraints(Tail, [C|Funs], Acc, State);
order_fun_constraints([#constraint_list{list = List, type = Type} = C|Tail],
Funs, Acc, State) ->
{NewList, NewState} =
case Type of
conj -> order_fun_constraints(List, [], [], State);
disj ->
FoldFun = fun(X, AccState) ->
{[NewX], NewAccState} =
order_fun_constraints([X], [], [], AccState),
{NewX, NewAccState}
end,
lists:mapfoldl(FoldFun, State, List)
end,
C1 = update_constraint_list(C, NewList),
Masks = calculate_masks(NewList, 1, []),
NewAcc = [update_masks(C1, Masks)|Acc],
order_fun_constraints(Tail, Funs, NewAcc, NewState);
order_fun_constraints([#constraint{} = C|Tail], Funs, Acc, State) ->
order_fun_constraints(Tail, Funs, [C|Acc], State);
order_fun_constraints([], Funs, Acc, State) ->
NewState = order_fun_constraints(Funs, State),
{lists:reverse(Acc)++Funs, NewState}.
update_masks(C, Masks) ->
C#constraint_list{masks = Masks}.
-define(VARS_LIMIT, 50).
calculate_masks([C|Cs], I, L0) ->
calculate_masks(Cs, I+1, [{V, I} || V <- get_deps(C)] ++ L0);
calculate_masks([], _I, L) ->
M = family(L),
case length(M) > ?VARS_LIMIT of
true ->
{d, dict:from_list(M)};
false ->
M
end.
%% ============================================================================
%%
%% Utilities.
%%
%% ============================================================================
is_singleton_non_number_type(Type) ->
case t_is_number(Type) of
true -> false;
false -> is_singleton_type(Type)
end.
is_singleton_type(Type) ->
case t_is_atom(Type) of
true ->
case t_atom_vals(Type) of
unknown -> false;
[_] -> true;
[_|_] -> false
end;
false ->
case t_is_integer(Type) of
true ->
case t_number_vals(Type) of
unknown -> false;
[_] -> true;
[_|_] -> false
end;
false ->
t_is_nil(Type)
end
end.
find_element(Args, Cs) ->
[Pos, Tuple] = Args,
case erl_types:t_is_number(Pos) of
true ->
case erl_types:t_number_vals(Pos) of
'unknown' -> 'unknown';
[I] ->
case find_constraint(Tuple, Cs) of
'unknown' -> 'unknown';
#constraint{lhs = ExTuple} ->
case erl_types:t_is_tuple(ExTuple) of
true ->
Elems = erl_types:t_tuple_args(ExTuple),
Elem = lists:nth(I, Elems),
case erl_types:t_is_var(Elem) of
true -> Elem;
false -> 'unknown'
end;
false -> 'unknown'
end
end;
_ -> 'unknown'
end;
false -> 'unknown'
end.
find_constraint(_Tuple, []) ->
'unknown';
find_constraint(Tuple, [#constraint{op = 'eq', rhs = Tuple} = C|_]) ->
C;
find_constraint(Tuple, [#constraint_list{list = List}|Cs]) ->
find_constraint(Tuple, List ++ Cs);
find_constraint(Tuple, [_|Cs]) ->
find_constraint(Tuple, Cs).
lookup_record(Records, Tag, Arity) ->
case erl_types:lookup_record(Tag, Arity, Records) of
{ok, Fields} ->
{ok, t_tuple([t_from_term(Tag)|
[FieldType || {_FieldName, FieldType} <- Fields]])};
error ->
error
end.
family(L) ->
sofs:to_external(sofs:rel2fam(sofs:relation(L))).
%% ============================================================================
%%
%% Pretty printer and debug facilities.
%%
%% ============================================================================
-ifdef(DEBUG_CONSTRAINTS).
-ifndef(DEBUG).
-define(DEBUG, true).
-endif.
-endif.
-ifdef(DEBUG).
format_type(#fun_var{deps = Deps, origin = Origin}) ->
L = [format_type(t_var(X)) || X <- Deps],
io_lib:format("Fun@L~p(~s)", [Origin, join_chars(L, ",")]);
format_type(Type) ->
case cerl:is_literal(Type) of
true -> io_lib:format("~w", [cerl:concrete(Type)]);
false -> erl_types:t_to_string(Type)
end.
join_chars([], _Sep) ->
[];
join_chars([H|T], Sep) ->
[H|[[Sep,X] || X <- T]].
debug_lookup_name(Var) ->
case dict:find(t_var_name(Var), get(dialyzer_typesig_map)) of
error -> Var;
{ok, Name} -> Name
end.
-endif.
-ifdef(DEBUG_NAME_MAP).
debug_make_name_map(Vars, Funs) ->
Map = get(dialyzer_typesig_map),
NewMap =
if Map =:= undefined -> debug_make_name_map(Vars, Funs, dict:new());
true -> debug_make_name_map(Vars, Funs, Map)
end,
put(dialyzer_typesig_map, NewMap).
debug_make_name_map([Var|VarLeft], [Fun|FunLeft], Map) ->
Name = {cerl:fname_id(Var), cerl:fname_arity(Var)},
FunLabel = cerl_trees:get_label(Fun),
debug_make_name_map(VarLeft, FunLeft, dict:store(FunLabel, Name, Map));
debug_make_name_map([], [], Map) ->
Map.
-else.
debug_make_name_map(_Vars, _Funs) ->
ok.
-endif.
-ifdef(DEBUG_CONSTRAINTS).
pp_constrs_scc(SCC, State) ->
[pp_constrs(Fun, state__get_cs(Fun, State), State) || Fun <- SCC].
pp_constrs(Fun, Cs, State) ->
io:format("Constraints for fun: ~w", [debug_lookup_name(Fun)]),
MaxDepth = pp_constraints(Cs, State),
io:format("Depth: ~w\n", [MaxDepth]).
pp_constraints(Cs, State) ->
Res = pp_constraints([Cs], 0, 0, State),
io:nl(),
Res.
pp_constraints([List|Tail], Level, MaxDepth, State) when is_list(List) ->
pp_constraints(List++Tail, Level, MaxDepth, State);
pp_constraints([#constraint_ref{id = Id}|Left], Level, MaxDepth, State) ->
Cs = state__get_cs(Id, State),
pp_indent(Level),
io:format("%Ref ~w%", [t_var_name(Id)]),
pp_constraints([Cs|Left], Level, MaxDepth, State);
pp_constraints([#constraint{}=C], Level, MaxDepth, _State) ->
pp_op(C, Level),
erlang:max(Level, MaxDepth);
pp_constraints([#constraint{}=C|Tail], Level, MaxDepth, State) ->
pp_op(C, Level),
pp_constraints(Tail, Level, MaxDepth, State);
pp_constraints([#constraint_list{type = Type, list = List, id = Id}],
Level, MaxDepth, State) ->
pp_indent(Level),
case Type of
conj -> io:format("Conj ~w (", [Id]);
disj -> io:format("Disj ~w (", [Id])
end,
NewMaxDepth = pp_constraints(List, Level + 1, MaxDepth, State),
io:format(")", []),
NewMaxDepth;
pp_constraints([#constraint_list{type = Type, list = List, id = Id}|Tail],
Level, MaxDepth, State) ->
pp_indent(Level),
case Type of
conj -> io:format("Conj ~w (", [Id]);
disj -> io:format("Disj ~w (", [Id])
end,
NewMaxDepth = pp_constraints(List, Level+1, MaxDepth, State),
io:format(")", []),
pp_constraints(Tail, Level, NewMaxDepth, State).
pp_op(#constraint{lhs = Lhs, op = Op, rhs = Rhs}, Level) ->
pp_indent(Level),
io:format("~s ~w ~s", [format_type(Lhs), Op, format_type(Rhs)]).
pp_indent(Level) ->
io:format("\n~*s", [Level*2, ""]).
-else.
pp_constrs_scc(_SCC, _State) ->
ok.
-endif.
-ifdef(TO_DOT).
constraints_to_dot_scc(SCC, State) ->
io:format("SCC: ~p\n", [SCC]),
Name = lists:flatten([io_lib:format("'~w'", [debug_lookup_name(Fun)])
|| Fun <- SCC]),
Cs = [state__get_cs(Fun, State) || Fun <- SCC],
constraints_to_dot(Cs, Name, State).
constraints_to_dot(Cs0, Name, State) ->
NofCs = length(Cs0),
Cs = lists:zip(lists:seq(1, NofCs), Cs0),
{Graph, Opts, _N} = constraints_to_nodes(Cs, NofCs + 1, 1, [], [], State),
hipe_dot:translate_list(Graph, "/tmp/cs.dot", "foo", Opts),
Res = os:cmd("dot -o /tmp/"++ Name ++ ".ps -T ps /tmp/cs.dot"),
io:format("Res: ~p~n", [Res]),
ok.
constraints_to_nodes([{Name, #constraint_list{type = Type, list = List, id=Id}}
|Left], N, Level, Graph, Opts, State) ->
N1 = N + length(List),
NewList = lists:zip(lists:seq(N, N1 - 1), List),
Names = [SubName || {SubName, _C} <- NewList],
Edges = [{Name, SubName} || SubName <- Names],
ThisNode = [{Name, Opt} || Opt <- [{label,
lists:flatten(io_lib:format("~w", [Id]))},
{shape, get_shape(Type)},
{level, Level}]],
{NewGraph, NewOpts, N2} = constraints_to_nodes(NewList, N1, Level+1,
[Edges|Graph],
[ThisNode|Opts], State),
constraints_to_nodes(Left, N2, Level, NewGraph, NewOpts, State);
constraints_to_nodes([{Name, #constraint{lhs = Lhs, op = Op, rhs = Rhs}}|Left],
N, Level, Graph, Opts, State) ->
Label = lists:flatten(io_lib:format("~s ~w ~s",
[format_type(Lhs), Op,
format_type(Rhs)])),
ThisNode = [{Name, Opt} || Opt <- [{label, Label}, {level, Level}]],
NewOpts = [ThisNode|Opts],
constraints_to_nodes(Left, N, Level, Graph, NewOpts, State);
constraints_to_nodes([{Name, #constraint_ref{id = Id0}}|Left],
N, Level, Graph, Opts, State) ->
Id = debug_lookup_name(Id0),
CList = state__get_cs(Id0, State),
ThisNode = [{Name, Opt} || Opt <- [{label,
lists:flatten(io_lib:format("~w", [Id]))},
{shape, ellipse},
{level, Level}]],
NewList = [{N, CList}],
{NewGraph, NewOpts, N1} = constraints_to_nodes(NewList, N + 1, Level + 1,
[{Name, N}|Graph],
[ThisNode|Opts], State),
constraints_to_nodes(Left, N1, Level, NewGraph, NewOpts, State);
constraints_to_nodes([], N, _Level, Graph, Opts, _State) ->
{lists:flatten(Graph), lists:flatten(Opts), N}.
get_shape(conj) -> box;
get_shape(disj) -> diamond.
-else.
constraints_to_dot_scc(_SCC, _State) ->
ok.
-endif.
