diff options
author | Hans Bolinder <[email protected]> | 2013-03-21 15:49:01 +0100 |
---|---|---|
committer | Hans Bolinder <[email protected]> | 2014-01-21 09:28:19 +0100 |
commit | 7db0bb7ae867ea5de893914a89c51dc0369b5790 (patch) | |
tree | 842d2c4f9ae3dc008484e8a29c5fa90f0fc03737 /lib/dialyzer/src | |
parent | 9b92301dcae72faecdab9f5fe009a53f6d47b8a1 (diff) | |
download | otp-7db0bb7ae867ea5de893914a89c51dc0369b5790.tar.gz otp-7db0bb7ae867ea5de893914a89c51dc0369b5790.tar.bz2 otp-7db0bb7ae867ea5de893914a89c51dc0369b5790.zip |
[dialyzer] Re-work the handling of opaque types
It is now OK to inspect and modify the internals of opaque types within
the scope of the module.
The contracts are used for decorating types with opaqueness when it is
harmless to do so. The opaqueness is propagated by the typesig module
and also by the dataflow module.
A lot of details have been fixed or updated. In particular the modules
erl_types and erl_bif_types have been modified extensively.
The version in vsn.mk has been updated to 2.7. The reason is a
modification of #opaque{} in erl_types.
Dialyzer seems to be about five percent slower than it used to be.
Diffstat (limited to 'lib/dialyzer/src')
-rw-r--r-- | lib/dialyzer/src/dialyzer.erl | 15 | ||||
-rw-r--r-- | lib/dialyzer/src/dialyzer_cl.erl | 8 | ||||
-rw-r--r-- | lib/dialyzer/src/dialyzer_contracts.erl | 90 | ||||
-rw-r--r-- | lib/dialyzer/src/dialyzer_dataflow.erl | 1058 | ||||
-rw-r--r-- | lib/dialyzer/src/dialyzer_succ_typings.erl | 82 | ||||
-rw-r--r-- | lib/dialyzer/src/dialyzer_typesig.erl | 355 |
6 files changed, 846 insertions, 762 deletions
diff --git a/lib/dialyzer/src/dialyzer.erl b/lib/dialyzer/src/dialyzer.erl index 35156afff2..bb7e39dfda 100644 --- a/lib/dialyzer/src/dialyzer.erl +++ b/lib/dialyzer/src/dialyzer.erl @@ -423,6 +423,9 @@ message_to_string({call_without_opaque, [M, F, Args, ExpectedTriples]}) -> message_to_string({opaque_eq, [Type, _Op, OpaqueType]}) -> io_lib:format("Attempt to test for equality between a term of type ~s" " and a term of opaque type ~s\n", [Type, OpaqueType]); +message_to_string({opaque_guard, [Arg1, Infix, Arg2, ArgNs]}) -> + io_lib:format("Guard test ~s ~s ~s contains ~s\n", + [Arg1, Infix, Arg2, form_positions(ArgNs)]); message_to_string({opaque_guard, [Guard, Args]}) -> io_lib:format("Guard test ~w~s breaks the opaqueness of its argument\n", [Guard, Args]); @@ -435,8 +438,16 @@ message_to_string({opaque_match, [Pat, OpaqueType, OpaqueTerm]}) -> message_to_string({opaque_neq, [Type, _Op, OpaqueType]}) -> io_lib:format("Attempt to test for inequality between a term of type ~s" " and a term of opaque type ~s\n", [Type, OpaqueType]); -message_to_string({opaque_type_test, [Fun, Opaque]}) -> - io_lib:format("The type test ~s(~s) breaks the opaqueness of the term ~s\n", [Fun, Opaque, Opaque]); +message_to_string({opaque_type_test, [Fun, Args, Arg, ArgType]}) -> + io_lib:format("The type test ~s~s breaks the opaqueness of the term ~s~s\n", + [Fun, Args, Arg, ArgType]); +message_to_string({opaque_size, [SizeType, Size]}) -> + io_lib:format("The size ~s breaks the opaqueness of ~s\n", + [SizeType, Size]); +message_to_string({opaque_call, [M, F, Args, Culprit, OpaqueType]}) -> + io_lib:format("The call ~s:~s~s breaks the opaqueness of the term ~s :: ~s\n", + [M, F, Args, Culprit, OpaqueType]); + %%----- Warnings for concurrency errors -------------------- message_to_string({race_condition, [M, F, Args, Reason]}) -> io_lib:format("The call ~w:~w~s ~s\n", [M, F, Args, Reason]); diff --git a/lib/dialyzer/src/dialyzer_cl.erl b/lib/dialyzer/src/dialyzer_cl.erl index 365c0b36d4..a7be6e0d05 100644 --- a/lib/dialyzer/src/dialyzer_cl.erl +++ b/lib/dialyzer/src/dialyzer_cl.erl @@ -2,7 +2,7 @@ %%------------------------------------------------------------------- %% %CopyrightBegin% %% -%% Copyright Ericsson AB 2006-2013. All Rights Reserved. +%% Copyright Ericsson AB 2006-2014. 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 @@ -613,7 +613,7 @@ cl_loop(State, LogCache) -> -spec failed_anal_msg(string(), [_]) -> nonempty_string(). failed_anal_msg(Reason, LogCache) -> - Msg = "Analysis failed with error:\n" ++ Reason ++ "\n", + Msg = "Analysis failed with error:\n" ++ lists:flatten(Reason) ++ "\n", case LogCache =:= [] of true -> Msg; false -> @@ -640,7 +640,7 @@ store_unknown_behaviours(#cl_state{unknown_behaviours = Behs} = St, Beh) -> -spec cl_error(string()) -> no_return(). cl_error(Msg) -> - throw({dialyzer_error, Msg}). + throw({dialyzer_error, lists:flatten(Msg)}). -spec cl_error(#cl_state{}, string()) -> no_return(). @@ -650,7 +650,7 @@ cl_error(State, Msg) -> Outfile -> io:format(Outfile, "\n~s\n", [Msg]) end, maybe_close_output_file(State), - throw({dialyzer_error, Msg}). + throw({dialyzer_error, lists:flatten(Msg)}). return_value(State = #cl_state{erlang_mode = ErlangMode, mod_deps = ModDeps, diff --git a/lib/dialyzer/src/dialyzer_contracts.erl b/lib/dialyzer/src/dialyzer_contracts.erl index 332a326b0d..3467ab4e65 100644 --- a/lib/dialyzer/src/dialyzer_contracts.erl +++ b/lib/dialyzer/src/dialyzer_contracts.erl @@ -2,7 +2,7 @@ %%----------------------------------------------------------------------- %% %CopyrightBegin% %% -%% Copyright Ericsson AB 2007-2013. All Rights Reserved. +%% Copyright Ericsson AB 2007-2014. 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 @@ -21,10 +21,10 @@ -module(dialyzer_contracts). -export([check_contract/2, - check_contracts/3, + check_contracts/4, contracts_without_fun/3, contract_to_string/1, - get_invalid_contract_warnings/3, + get_invalid_contract_warnings/4, get_contract_args/1, get_contract_return/1, get_contract_return/2, @@ -160,17 +160,22 @@ process_contract_remote_types(CodeServer) -> dialyzer_codeserver:finalize_contracts(NewContractDict, NewCallbackDict, CodeServer). +-type opaques() :: [erl_types:erl_type()] | 'universe'. +-type opaques_fun() :: fun((module()) -> opaques()). + -spec check_contracts([{mfa(), file_contract()}], - dialyzer_callgraph:callgraph(), dict()) -> plt_contracts(). + dialyzer_callgraph:callgraph(), dict(), + opaques_fun()) -> plt_contracts(). -check_contracts(Contracts, Callgraph, FunTypes) -> +check_contracts(Contracts, Callgraph, FunTypes, FindOpaques) -> FoldFun = fun(Label, Type, NewContracts) -> case dialyzer_callgraph:lookup_name(Label, Callgraph) of {ok, {M,F,A} = MFA} -> case orddict:find(MFA, Contracts) of {ok, {_FileLine, Contract}} -> - case check_contract(Contract, Type) of + Opaques = FindOpaques(M), + case check_contract(Contract, Type, Opaques) of ok -> case erl_bif_types:is_known(M, F, A) of true -> @@ -192,7 +197,10 @@ check_contracts(Contracts, Callgraph, FunTypes) -> %% Checks all components of a contract -spec check_contract(#contract{}, erl_types:erl_type()) -> 'ok' | {'error', term()}. -check_contract(#contract{contracts = Contracts}, SuccType) -> +check_contract(Contract, SuccType) -> + check_contract(Contract, SuccType, 'universe'). + +check_contract(#contract{contracts = Contracts}, SuccType, Opaques) -> try Contracts1 = [{Contract, insert_constraints(Constraints, dict:new())} || {Contract, Constraints} <- Contracts], @@ -203,9 +211,9 @@ check_contract(#contract{contracts = Contracts}, SuccType) -> error -> {error, {overlapping_contract, []}}; ok -> - InfList = [erl_types:t_inf(Contract, SuccType, opaque) + InfList = [erl_types:t_inf(Contract, SuccType, Opaques) || Contract <- Contracts2], - case check_contract_inf_list(InfList, SuccType) of + case check_contract_inf_list(InfList, SuccType, Opaques) of {error, _} = Invalid -> Invalid; ok -> check_extraneous(Contracts2, SuccType) end @@ -217,7 +225,7 @@ check_contract(#contract{contracts = Contracts}, SuccType) -> check_domains([_]) -> ok; check_domains([Dom|Doms]) -> Fun = fun(D) -> - erl_types:any_none_or_unit(erl_types:t_inf_lists(Dom, D, opaque)) + erl_types:any_none_or_unit(erl_types:t_inf_lists(Dom, D)) end, case lists:all(Fun, Doms) of true -> check_domains(Doms); @@ -227,23 +235,23 @@ check_domains([Dom|Doms]) -> %% Allow a contract if one of the overloaded contracts is possible. %% We used to be more strict, e.g., all overloaded contracts had to be %% possible. -check_contract_inf_list([FunType|Left], SuccType) -> +check_contract_inf_list([FunType|Left], SuccType, Opaques) -> FunArgs = erl_types:t_fun_args(FunType), case lists:any(fun erl_types:t_is_none_or_unit/1, FunArgs) of - true -> check_contract_inf_list(Left, SuccType); + true -> check_contract_inf_list(Left, SuccType, Opaques); false -> STRange = erl_types:t_fun_range(SuccType), case erl_types:t_is_none_or_unit(STRange) of true -> ok; false -> Range = erl_types:t_fun_range(FunType), - case erl_types:t_is_none(erl_types:t_inf(STRange, Range, opaque)) of - true -> check_contract_inf_list(Left, SuccType); + case erl_types:t_is_none(erl_types:t_inf(STRange, Range)) of + true -> check_contract_inf_list(Left, SuccType, Opaques); false -> ok end end end; -check_contract_inf_list([], _SuccType) -> +check_contract_inf_list([], _SuccType, _Opaques) -> {error, invalid_contract}. check_extraneous([], _SuccType) -> ok; @@ -259,7 +267,7 @@ check_extraneous_1(Contract, SuccType) -> STRng = erl_types:t_fun_range(SuccType), ?debug("CR = ~p\nSR = ~p\n", [CRngs, STRng]), case [CR || CR <- CRngs, - erl_types:t_is_none(erl_types:t_inf(CR, STRng, opaque))] of + erl_types:t_is_none(erl_types:t_inf(CR, STRng))] of [] -> CRngList = list_part(CRng), STRngList = list_part(STRng), @@ -268,7 +276,7 @@ check_extraneous_1(Contract, SuccType) -> true -> CRngElements = erl_types:t_list_elements(CRngList), STRngElements = erl_types:t_list_elements(STRngList), - Inf = erl_types:t_inf(CRngElements, STRngElements, opaque), + Inf = erl_types:t_inf(CRngElements, STRngElements), case erl_types:t_is_none(Inf) of true -> {error, invalid_contract}; false -> ok @@ -278,7 +286,7 @@ check_extraneous_1(Contract, SuccType) -> end. list_part(Type) -> - erl_types:t_inf(erl_types:t_list(), Type, opaque). + erl_types:t_inf(erl_types:t_list(), Type). is_not_nil_list(Type) -> erl_types:t_is_list(Type) andalso not erl_types:t_is_nil(Type). @@ -374,7 +382,7 @@ insert_constraints([], Dict) -> Dict. store_tmp_contract(MFA, FileLine, TypeSpec, SpecDict, RecordsDict) -> %% io:format("contract from form: ~p\n", [TypeSpec]), TmpContract = contract_from_form(TypeSpec, RecordsDict, FileLine), - %% io:format("contract: ~p\n", [Contract]), + %% io:format("contract: ~p\n", [TmpContract]), dict:store(MFA, {FileLine, TmpContract}, SpecDict). contract_from_form(Forms, RecDict, FileLine) -> @@ -494,30 +502,35 @@ general_domain([], AccSig) -> AccSig1 = erl_types:subst_all_vars_to_any(AccSig), erl_types:t_fun_args(AccSig1). --spec get_invalid_contract_warnings([module()], dialyzer_codeserver:codeserver(), dialyzer_plt:plt()) -> [dial_warning()]. +-spec get_invalid_contract_warnings([module()], + dialyzer_codeserver:codeserver(), + dialyzer_plt:plt(), + opaques_fun()) -> [dial_warning()]. -get_invalid_contract_warnings(Modules, CodeServer, Plt) -> - get_invalid_contract_warnings_modules(Modules, CodeServer, Plt, []). +get_invalid_contract_warnings(Modules, CodeServer, Plt, FindOpaques) -> + get_invalid_contract_warnings_modules(Modules, CodeServer, Plt, FindOpaques, []). -get_invalid_contract_warnings_modules([Mod|Mods], CodeServer, Plt, Acc) -> +get_invalid_contract_warnings_modules([Mod|Mods], CodeServer, Plt, FindOpaques, Acc) -> Contracts1 = dialyzer_codeserver:lookup_mod_contracts(Mod, CodeServer), Contracts2 = dict:to_list(Contracts1), Records = dialyzer_codeserver:lookup_mod_records(Mod, CodeServer), - NewAcc = get_invalid_contract_warnings_funs(Contracts2, Plt, Records, Acc), - get_invalid_contract_warnings_modules(Mods, CodeServer, Plt, NewAcc); -get_invalid_contract_warnings_modules([], _CodeServer, _Plt, Acc) -> + NewAcc = get_invalid_contract_warnings_funs(Contracts2, Plt, Records, FindOpaques, Acc), + get_invalid_contract_warnings_modules(Mods, CodeServer, Plt, FindOpaques, NewAcc); +get_invalid_contract_warnings_modules([], _CodeServer, _Plt, _FindOpaques, Acc) -> Acc. get_invalid_contract_warnings_funs([{MFA, {FileLine, Contract}}|Left], - Plt, RecDict, Acc) -> + Plt, RecDict, FindOpaques, Acc) -> case dialyzer_plt:lookup(Plt, MFA) of none -> %% This must be a contract for a non-available function. Just accept it. - get_invalid_contract_warnings_funs(Left, Plt, RecDict, Acc); + get_invalid_contract_warnings_funs(Left, Plt, RecDict, FindOpaques, Acc); {value, {Ret, Args}} -> Sig = erl_types:t_fun(Args, Ret), + {M, _F, _A} = MFA, + Opaques = FindOpaques(M), NewAcc = - case check_contract(Contract, Sig) of + case check_contract(Contract, Sig, Opaques) of {error, invalid_contract} -> [invalid_contract_warning(MFA, FileLine, Sig, RecDict)|Acc]; {error, {overlapping_contract, []}} -> @@ -551,7 +564,7 @@ get_invalid_contract_warnings_funs([{MFA, {FileLine, Contract}}|Left], BifArgs = erl_bif_types:arg_types(M, F, A), BifRet = erl_bif_types:type(M, F, A), BifSig = erl_types:t_fun(BifArgs, BifRet), - case check_contract(Contract, BifSig) of + case check_contract(Contract, BifSig, Opaques) of {error, _} -> [invalid_contract_warning(MFA, FileLine, BifSig, RecDict) |Acc]; @@ -564,9 +577,9 @@ get_invalid_contract_warnings_funs([{MFA, {FileLine, Contract}}|Left], RecDict, Acc) end end, - get_invalid_contract_warnings_funs(Left, Plt, RecDict, NewAcc) + get_invalid_contract_warnings_funs(Left, Plt, RecDict, FindOpaques, NewAcc) end; -get_invalid_contract_warnings_funs([], _Plt, _RecDict, Acc) -> +get_invalid_contract_warnings_funs([], _Plt, _RecDict, _FindOpaques, Acc) -> Acc. invalid_contract_warning({M, F, A}, FileLine, SuccType, RecDict) -> @@ -601,16 +614,23 @@ picky_contract_check(CSig0, Sig0, MFA, FileLine, Contract, RecDict, Acc) -> end. extra_contract_warning({M, F, A}, FileLine, Contract, CSig, Sig, RecDict) -> - SigString = lists:flatten(dialyzer_utils:format_sig(Sig, RecDict)), - ContractString0 = lists:flatten(dialyzer_utils:format_sig(CSig, RecDict)), + %% We do not want to depend upon erl_types:t_to_string() possibly + %% hiding the contents of opaque types. + SigUnopaque = erl_types:t_unopaque(Sig), + CSigUnopaque = erl_types:t_unopaque(CSig), + SigString0 = + lists:flatten(dialyzer_utils:format_sig(SigUnopaque, RecDict)), + ContractString0 = + lists:flatten(dialyzer_utils:format_sig(CSigUnopaque, RecDict)), %% The only difference is in record fields containing 'undefined' or not. - IsUndefRecordFieldsRelated = SigString =:= ContractString0, + IsUndefRecordFieldsRelated = SigString0 =:= ContractString0, {IsRemoteTypesRelated, SubtypeRelation} = is_remote_types_related(Contract, CSig, Sig, RecDict), case IsUndefRecordFieldsRelated orelse IsRemoteTypesRelated of true -> no_warning; false -> + SigString = lists:flatten(dialyzer_utils:format_sig(Sig, RecDict)), ContractString = contract_to_string(Contract), {Tag, Msg} = case SubtypeRelation of diff --git a/lib/dialyzer/src/dialyzer_dataflow.erl b/lib/dialyzer/src/dialyzer_dataflow.erl index 922ccad599..3591d5be8e 100644 --- a/lib/dialyzer/src/dialyzer_dataflow.erl +++ b/lib/dialyzer/src/dialyzer_dataflow.erl @@ -2,7 +2,7 @@ %%-------------------------------------------------------------------- %% %CopyrightBegin% %% -%% Copyright Ericsson AB 2006-2012. All Rights Reserved. +%% Copyright Ericsson AB 2006-2014. 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 @@ -41,27 +41,33 @@ -include("dialyzer.hrl"). +%%-import(helper, %% 'helper' could be any module doing sanity checks... -import(erl_types, - [any_none/1, t_any/0, t_atom/0, t_atom/1, t_atom_vals/1, + [t_inf/2, t_inf/3, t_inf_lists/2, t_inf_lists/3, + t_inf_lists/3, t_is_equal/2, t_is_subtype/2, t_subtract/2, + t_sup/1, t_sup/2]). + +-import(erl_types, + [any_none/1, t_any/0, t_atom/0, t_atom/1, t_atom_vals/1, t_atom_vals/2, t_binary/0, t_boolean/0, t_bitstr/0, t_bitstr/2, t_bitstr_concat/1, t_bitstr_match/2, - t_cons/0, t_cons/2, t_cons_hd/1, t_cons_tl/1, t_contains_opaque/1, + t_cons/0, t_cons/2, t_cons_hd/2, t_cons_tl/2, + t_contains_opaque/2, t_find_opaque_mismatch/2, 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_inf/2, t_inf/3, t_inf_lists/2, t_inf_lists/3, t_inf_lists_masked/3, - t_integer/0, t_integers/1, - t_is_any/1, t_is_atom/1, t_is_atom/2, t_is_boolean/1, t_is_equal/2, - t_is_integer/1, t_is_nil/1, t_is_none/1, t_is_none_or_unit/1, - t_is_number/1, t_is_reference/1, t_is_pid/1, t_is_port/1, - t_is_subtype/2, t_is_unit/1, + t_fun/0, t_fun/2, t_fun_args/1, t_fun_args/2, t_fun_range/1, + t_fun_range/2, t_integer/0, t_integers/1, + t_is_any/1, t_is_atom/1, t_is_atom/2, t_is_any_atom/3, + t_is_boolean/2, + t_is_integer/2, t_is_nil/2, t_is_none/1, t_is_none_or_unit/1, + t_is_number/2, t_is_reference/2, t_is_pid/2, t_is_port/2, + t_is_unit/1, t_limit/2, t_list/0, t_maybe_improper_list/0, t_module/0, - t_none/0, t_non_neg_integer/0, t_number/0, t_number_vals/1, - t_opaque_match_atom/2, t_opaque_match_record/2, - t_opaque_matching_structure/2, + t_none/0, t_non_neg_integer/0, t_number/0, t_number_vals/2, t_pid/0, t_port/0, t_product/1, t_reference/0, - t_sup/1, t_sup/2, t_subtract/2, t_to_string/2, t_to_tlist/1, - t_tuple/0, t_tuple/1, t_tuple_args/1, t_tuple_subtypes/1, - t_unit/0, t_unopaque/1]). + t_to_string/2, t_to_tlist/1, + t_tuple/0, t_tuple/1, t_tuple_args/1, t_tuple_args/2, + t_tuple_subtypes/2, + t_unit/0, t_unopaque/2]). %%-define(DEBUG, true). %%-define(DEBUG_PP, true). @@ -204,7 +210,7 @@ analyze_loop(State) -> traverse(Tree, Map, State) -> ?debug("Handling ~p\n", [cerl:type(Tree)]), - %%debug_pp_map(Map), + %% debug_pp_map(Map), case cerl:type(Tree) of alias -> %% This only happens when checking for illegal record patterns @@ -256,12 +262,7 @@ traverse(Tree, Map, State) -> case cerl:unfold_literal(Tree) of Tree -> Type = literal_type(Tree), - NewType = - case erl_types:t_opaque_match_atom(Type, State#state.opaques) of - [Opaque] -> Opaque; - _ -> Type - end, - {State, Map, NewType}; + {State, Map, Type}; NewTree -> traverse(NewTree, Map, State) end; module -> @@ -286,8 +287,11 @@ traverse(Tree, Map, State) -> SMA; false -> State2 = - case (t_is_any(ArgType) orelse t_is_simple(ArgType) - orelse is_call_to_send(Arg)) of + case + t_is_any(ArgType) + orelse t_is_simple(ArgType, State) + orelse is_call_to_send(Arg) + of true -> % do not warn in these cases State1; false -> @@ -311,15 +315,7 @@ traverse(Tree, Map, State) -> case state__lookup_type_for_letrec(Tree, State) of error -> LType = lookup_type(Tree, Map), - Opaques = State#state.opaques, - case t_opaque_match_record(LType, Opaques) of - [Opaque] -> {State, Map, Opaque}; - _ -> - case t_opaque_match_atom(LType, Opaques) of - [Opaque] -> {State, Map, Opaque}; - _ -> {State, Map, LType} - end - end; + {State, Map, LType}; {ok, Type} -> {State, Map, Type} end; Other -> @@ -367,7 +363,8 @@ handle_apply(Tree, Map, State) -> Tree, Msg), {State3, Map2, t_none()}; false -> - NewArgs = t_inf_lists(ArgTypes, t_fun_args(OpType1)), + NewArgs = t_inf_lists(ArgTypes, + t_fun_args(OpType1, 'universe')), case any_none(NewArgs) of true -> Msg = {fun_app_args, @@ -378,7 +375,7 @@ handle_apply(Tree, Map, State) -> {State3, enter_type(Op, OpType1, Map2), t_none()}; false -> Map3 = enter_type_lists(Args, NewArgs, Map2), - Range0 = t_fun_range(OpType1), + Range0 = t_fun_range(OpType1, 'universe'), Range = case t_is_unit(Range0) of true -> t_none(); @@ -423,83 +420,55 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left], {M, F, A} = Fun, case erl_bif_types:is_known(M, F, A) of true -> - IsBIF = true, BArgs = erl_bif_types:arg_types(M, F, A), BRange = fun(FunArgs) -> - ArgPos = erl_bif_types:structure_inspecting_args(M, F, A), - NewFunArgs = - case ArgPos =:= [] of - true -> FunArgs; - false -> % some positions need to be un-opaqued - N = length(FunArgs), - PFs = lists:zip(lists:seq(1, N), FunArgs), - [case ordsets:is_element(P, ArgPos) of - true -> erl_types:t_unopaque(FArg, Opaques); - false -> FArg - end || {P, FArg} <- PFs] - end, - erl_bif_types:type(M, F, A, NewFunArgs) + erl_bif_types:type(M, F, A, FunArgs, Opaques) end, {BArgs, BRange}; - false -> IsBIF = false, GenSig + false -> + GenSig end; - local -> IsBIF = false, GenSig + local -> GenSig end, {SigArgs, SigRange} = - %% if there is hard-coded or contract information with opaque types, - %% the checking for possible type violations needs to take place w.r.t. - %% this information and not w.r.t. the structure-based success typing. - case prefer_opaque_types(CArgs, BifArgs) of - true -> {AnyArgs, t_any()}; % effectively forgets the success typing - false -> - case Sig of - {value, {SR, SA}} -> {SA, SR}; - none -> {AnyArgs, t_any()} - end - end, - ArgModeMask = [case lists:member(Arg, Opaques) of - true -> opaque; - false -> structured - end || Arg <- ArgTypes], - NewArgsSig = t_inf_lists_masked(SigArgs, ArgTypes, ArgModeMask), - NewArgsContract = t_inf_lists_masked(CArgs, ArgTypes, ArgModeMask), - NewArgsBif = t_inf_lists_masked(BifArgs, ArgTypes, ArgModeMask), - NewArgTypes0 = t_inf_lists_masked(NewArgsSig, NewArgsContract, ArgModeMask), - NewArgTypes = t_inf_lists_masked(NewArgTypes0, NewArgsBif, ArgModeMask), - BifRet = BifRange(NewArgTypes), - {TmpArgTypes, TmpArgsContract} = - case (TypeOfApply =:= remote) andalso (not IsBIF) of - true -> - List1 = lists:zip(CArgs, NewArgTypes), - List2 = lists:zip(CArgs, NewArgsContract), - {[erl_types:t_unopaque_on_mismatch(T1, T2, Opaques) - || {T1, T2} <- List1], - [erl_types:t_unopaque_on_mismatch(T1, T2, Opaques) - || {T1, T2} <- List2]}; - false -> {NewArgTypes, NewArgsContract} - end, - ContrRet = CRange(TmpArgTypes), - RetMode = - case t_contains_opaque(ContrRet) orelse t_contains_opaque(BifRet) of - true -> opaque; - false -> structured + case Sig of + {value, {SR, SA}} -> {SA, SR}; + none -> {AnyArgs, t_any()} end, - RetWithoutContr = t_inf(SigRange, BifRet, RetMode), - RetWithoutLocal = t_inf(ContrRet, RetWithoutContr, RetMode), + ?debug("--------------------------------------------------------\n", []), - ?debug("Fun: ~p\n", [Fun]), - ?debug("Args: ~s\n", [erl_types:t_to_string(t_product(ArgTypes))]), + ?debug("Fun: ~p\n", [state__lookup_name(Fun, State)]), + ?debug("Module ~p\n", [State#state.module]), + ?debug("CArgs ~s\n", [erl_types:t_to_string(t_product(CArgs))]), + ?debug("ArgTypes ~s\n", [erl_types:t_to_string(t_product(ArgTypes))]), + ?debug("BifArgs ~p\n", [erl_types:t_to_string(t_product(BifArgs))]), + + NewArgsSig = t_inf_lists(SigArgs, ArgTypes, Opaques), + ?debug("SigArgs ~s\n", [erl_types:t_to_string(t_product(SigArgs))]), ?debug("NewArgsSig: ~s\n", [erl_types:t_to_string(t_product(NewArgsSig))]), + NewArgsContract = t_inf_lists(CArgs, ArgTypes, Opaques), ?debug("NewArgsContract: ~s\n", [erl_types:t_to_string(t_product(NewArgsContract))]), + NewArgsBif = t_inf_lists(BifArgs, ArgTypes, Opaques), ?debug("NewArgsBif: ~s\n", [erl_types:t_to_string(t_product(NewArgsBif))]), - ?debug("NewArgTypes: ~s\n", [erl_types:t_to_string(t_product(NewArgTypes))]), + NewArgTypes0 = t_inf_lists(NewArgsSig, NewArgsContract), + NewArgTypes = t_inf_lists(NewArgTypes0, NewArgsBif, Opaques), + ?debug("NewArgTypes ~s\n", [erl_types:t_to_string(t_product(NewArgTypes))]), + ?debug("\n", []), + + BifRet = BifRange(NewArgTypes), + ContrRet = CRange(NewArgTypes), + RetWithoutContr = t_inf(SigRange, BifRet), + RetWithoutLocal = t_inf(ContrRet, RetWithoutContr), + ?debug("RetWithoutContr: ~s\n",[erl_types:t_to_string(RetWithoutContr)]), ?debug("RetWithoutLocal: ~s\n", [erl_types:t_to_string(RetWithoutLocal)]), ?debug("BifRet: ~s\n", [erl_types:t_to_string(BifRange(NewArgTypes))]), - ?debug("ContrRet: ~s\n", [erl_types:t_to_string(CRange(TmpArgTypes))]), - ?debug("SigRet: ~s\n", [erl_types:t_to_string(SigRange)]), + ?debug("SigRange: ~s\n", [erl_types:t_to_string(SigRange)]), + ?debug("ContrRet: ~s\n", [erl_types:t_to_string(CRange(NewArgTypes))]), + ?debug("LocalRet: ~s\n", [erl_types:t_to_string(LocalRet)]), + State1 = case is_race_analysis_enabled(State) of true -> @@ -513,6 +482,9 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left], FailedConj = any_none([RetWithoutLocal|NewArgTypes]), IsFailBif = t_is_none(BifRange(BifArgs)), IsFailSig = t_is_none(SigRange), + ?debug("FailedConj: ~p~n", [FailedConj]), + ?debug("IsFailBif: ~p~n", [IsFailBif]), + ?debug("IsFailSig: ~p~n", [IsFailSig]), State2 = case FailedConj andalso not (IsFailBif orelse IsFailSig) of true -> @@ -532,14 +504,14 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left], false -> FailedSig = any_none(NewArgsSig), FailedContract = - any_none([CRange(TmpArgsContract)|NewArgsContract]), + any_none([CRange(NewArgsContract)|NewArgsContract]), FailedBif = any_none([BifRange(NewArgsBif)|NewArgsBif]), InfSig = t_inf(t_fun(SigArgs, SigRange), - t_fun(BifArgs, BifRange(BifArgs))), + t_fun(BifArgs, BifRange(BifArgs))), FailReason = apply_fail_reason(FailedSig, FailedBif, FailedContract), Msg = get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes, InfSig, - Contr, CArgs, State1, FailReason), + Contr, CArgs, State1, FailReason, Opaques), WarnType = case Msg of {call, _} -> ?WARN_FAILING_CALL; {apply, _} -> ?WARN_FAILING_CALL; @@ -547,7 +519,8 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left], {call_without_opaque, _} -> ?WARN_OPAQUE; {opaque_type_test, _} -> ?WARN_OPAQUE end, - state__add_warning(State1, WarnType, Tree, Msg) + Frc = {erlang, is_record, 3} =:= state__lookup_name(Fun, State), + state__add_warning(State1, WarnType, Tree, Msg, Frc) end; false -> State1 end, @@ -571,7 +544,7 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left], TotalRet = case t_is_none(LocalRet) andalso t_is_unit(RetWithoutLocal) of true -> RetWithoutLocal; - false -> t_inf(RetWithoutLocal, LocalRet, opaque) + false -> t_inf(RetWithoutLocal, LocalRet) end, NewAccRet = t_sup(AccRet, TotalRet), ?debug("NewAccRet: ~s\n", [t_to_string(NewAccRet)]), @@ -590,7 +563,7 @@ apply_fail_reason(FailedSig, FailedBif, FailedContract) -> end. get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes, - Sig, Contract, ContrArgs, State, FailReason) -> + Sig, Contract, ContrArgs, State, FailReason, Opaques) -> ArgStrings = format_args(Args, ArgTypes, State), ContractInfo = case Contract of @@ -599,44 +572,52 @@ get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes, dialyzer_contracts:contract_to_string(C)}; none -> {false, none} end, - EnumArgTypes = - case NewArgTypes of - [] -> []; - _ -> lists:zip(lists:seq(1, length(NewArgTypes)), NewArgTypes) - end, + EnumArgTypes = lists:zip(lists:seq(1, length(NewArgTypes)), NewArgTypes), ArgNs = [Arg || {Arg, Type} <- EnumArgTypes, t_is_none(Type)], case state__lookup_name(Fun, State) of - {M, F, _A} -> - case is_opaque_type_test_problem(Fun, NewArgTypes, State) of - true -> - [Opaque] = NewArgTypes, - {opaque_type_test, [atom_to_list(F), erl_types:t_to_string(Opaque)]}; - false -> + {M, F, A} -> + case is_opaque_type_test_problem(Fun, Args, NewArgTypes, State) of + {yes, Arg, ArgType} -> + {opaque_type_test, [atom_to_list(F), ArgStrings, + format_arg(Arg), format_type(ArgType, State)]}; + no -> SigArgs = t_fun_args(Sig), - case is_opaque_related_problem(ArgNs, ArgTypes) of - true -> %% an opaque term is used where a structured term is expected - ExpectedArgs = - case FailReason of - only_sig -> SigArgs; - _ -> ContrArgs - end, - {call_with_opaque, [M, F, ArgStrings, ArgNs, ExpectedArgs]}; - false -> - case is_opaque_related_problem(ArgNs, SigArgs) orelse - is_opaque_related_problem(ArgNs, ContrArgs) of - true -> %% a structured term is used where an opaque is expected - ExpectedTriples = - case FailReason of - only_sig -> expected_arg_triples(ArgNs, SigArgs, State); - _ -> expected_arg_triples(ArgNs, ContrArgs, State) - end, - {call_without_opaque, [M, F, ArgStrings, ExpectedTriples]}; - false -> %% there is a structured term clash in some argument - {call, [M, F, ArgStrings, - ArgNs, FailReason, - format_sig_args(Sig, State), - format_type(t_fun_range(Sig), State), - ContractInfo]} + BadOpaque = + opaque_problems([SigArgs, ContrArgs], ArgTypes, Opaques, ArgNs), + %% In fact *both* 'call_with_opaque' and + %% 'call_without_opaque' are possible. + case lists:keyfind(decl, 1, BadOpaque) of + {decl, BadArgs} -> + %% a structured term is used where an opaque is expected + ExpectedTriples = + case FailReason of + only_sig -> expected_arg_triples(BadArgs, SigArgs, State); + _ -> expected_arg_triples(BadArgs, ContrArgs, State) + end, + {call_without_opaque, [M, F, ArgStrings, ExpectedTriples]}; + false -> + case lists:keyfind(use, 1, BadOpaque) of + {use, BadArgs} -> + %% an opaque term is used where a structured term is expected + ExpectedArgs = + case FailReason of + only_sig -> SigArgs; + _ -> ContrArgs + end, + {call_with_opaque, [M, F, ArgStrings, BadArgs, ExpectedArgs]}; + false -> + case + erl_bif_types:opaque_args(M, F, A, ArgTypes, Opaques) + of + [] -> %% there is a structured term clash in some argument + {call, [M, F, ArgStrings, + ArgNs, FailReason, + format_sig_args(Sig, State), + format_type(t_fun_range(Sig), State), + ContractInfo]}; + Ns -> + {call_with_opaque, [M, F, ArgStrings, Ns, ContrArgs]} + end end end end; @@ -648,20 +629,28 @@ get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes, ContractInfo]} end. -%% returns 'true' if we are running with opaque on (not checked yet), -%% and there is either a contract or hard-coded type information with -%% opaque types -%% TODO: check that we are running with opaque types -%% TODO: check the return type also -prefer_opaque_types(CArgs, BifArgs) -> - t_contains_opaque(t_product(CArgs)) - orelse t_contains_opaque(t_product(BifArgs)). - -is_opaque_related_problem(ArgNs, ArgTypes) -> - Fun = fun (N) -> erl_types:t_contains_opaque(lists:nth(N, ArgTypes)) end, - ArgNs =/= [] andalso lists:all(Fun, ArgNs). - -is_opaque_type_test_problem(Fun, ArgTypes, State) -> +%% -> [{ElementI, [ArgN]}] where [ArgN] is a non-empty list of +%% arguments containing unknown opaque types and Element is 1 or 2. +opaque_problems(ContractOrSigList, ArgTypes, Opaques, ArgNs) -> + ArgElementList = find_unknown(ContractOrSigList, ArgTypes, Opaques, ArgNs), + F = fun(1) -> decl; (2) -> use end, + [{F(ElementI), lists:usort([ArgN || {ArgN, EI} <- ArgElementList, + EI =:= ElementI])} || + ElementI <- lists:usort([EI || {_, EI} <- ArgElementList])]. + +%% -> [{ArgN, ElementI}] where ElementI = 1 means there is an unknown +%% opaque type in argument ArgN of the the contract/signature, +%% and ElementI = 2 means that there is an unknown opaque type in +%% argument ArgN of the the (current) argument types. +find_unknown(ContractOrSigList, ArgTypes, Opaques, NoneArgNs) -> + ArgNs = lists:seq(1, length(ArgTypes)), + [{ArgN, ElementI} || + ContractOrSig <- ContractOrSigList, + {E1, E2, ArgN} <- lists:zip3(ContractOrSig, ArgTypes, ArgNs), + lists:member(ArgN, NoneArgNs), + ElementI <- erl_types:t_find_unknown_opaque(E1, E2, Opaques)]. + +is_opaque_type_test_problem(Fun, Args, ArgTypes, State) -> case Fun of {erlang, FN, 1} when FN =:= is_atom; FN =:= is_boolean; FN =:= is_binary; FN =:= is_bitstring; @@ -669,10 +658,18 @@ is_opaque_type_test_problem(Fun, ArgTypes, State) -> FN =:= is_integer; FN =:= is_list; FN =:= is_number; FN =:= is_pid; FN =:= is_port; FN =:= is_reference; FN =:= is_tuple -> - [Type] = ArgTypes, - erl_types:t_is_opaque(Type) andalso - not lists:member(Type, State#state.opaques); - _ -> false + type_test_opaque_arg(Args, ArgTypes, State#state.opaques); + {erlang, FN, 2} when FN =:= is_function -> + type_test_opaque_arg(Args, ArgTypes, State#state.opaques); + _ -> no + end. + +type_test_opaque_arg([], [], _Opaques) -> + no; +type_test_opaque_arg([Arg|Args], [ArgType|ArgTypes], Opaques) -> + case erl_types:t_has_opaque_subtype(ArgType, Opaques) of + true -> {yes, Arg, ArgType}; + false -> type_test_opaque_arg(Args, ArgTypes, Opaques) end. expected_arg_triples(ArgNs, ArgTypes, State) -> @@ -683,47 +680,56 @@ expected_arg_triples(ArgNs, ArgTypes, State) -> add_bif_warnings({erlang, Op, 2}, [T1, T2] = Ts, Tree, State) when Op =:= '=:='; Op =:= '==' -> - Type1 = erl_types:t_unopaque(T1, State#state.opaques), - Type2 = erl_types:t_unopaque(T2, State#state.opaques), - Inf = t_inf(T1, T2), - Inf1 = t_inf(Type1, Type2), - case t_is_none(Inf) andalso t_is_none(Inf1) andalso(not any_none(Ts)) - andalso (not is_int_float_eq_comp(T1, Op, T2)) of + Opaques = State#state.opaques, + Inf = t_inf(T1, T2, Opaques), + case + t_is_none(Inf) andalso (not any_none(Ts)) + andalso (not is_int_float_eq_comp(T1, Op, T2, Opaques)) + of true -> - Args = case erl_types:t_is_opaque(T1) of - true -> [format_type(T2, State), Op, format_type(T1, State)]; - false -> [format_type(T1, State), Op, format_type(T2, State)] - end, - case any_opaque(Ts) of - true -> - state__add_warning(State, ?WARN_OPAQUE, Tree, {opaque_eq, Args}); - false -> - state__add_warning(State, ?WARN_MATCHING, Tree, {exact_eq, Args}) + %% Give priority to opaque warning (as usual). + case erl_types:t_find_unknown_opaque(T1, T2, Opaques) of + [] -> + Args = comp_format_args([], T1, Op, T2, State), + state__add_warning(State, ?WARN_MATCHING, Tree, {exact_eq, Args}); + Ns -> + Args = comp_format_args(Ns, T1, Op, T2, State), + state__add_warning(State, ?WARN_OPAQUE, Tree, {opaque_eq, Args}) end; false -> State end; add_bif_warnings({erlang, Op, 2}, [T1, T2] = Ts, Tree, State) when Op =:= '=/='; Op =:= '/=' -> - Inf = t_inf(T1, T2), - case t_is_none(Inf) andalso (not any_none(Ts)) - andalso (not is_int_float_eq_comp(T1, Op, T2)) andalso any_opaque(Ts) of + Opaques = State#state.opaques, + case + (not any_none(Ts)) + andalso (not is_int_float_eq_comp(T1, Op, T2, Opaques)) + of true -> - Args = case erl_types:t_is_opaque(T1) of - true -> [format_type(T2, State), Op, format_type(T1, State)]; - false -> [format_type(T1, State), Op, format_type(T2, State)] - end, - state__add_warning(State, ?WARN_OPAQUE, Tree, {opaque_neq, Args}); + case erl_types:t_find_unknown_opaque(T1, T2, Opaques) of + [] -> State; + Ns -> + Args = comp_format_args(Ns, T1, Op, T2, State), + state__add_warning(State, ?WARN_OPAQUE, Tree, {opaque_neq, Args}) + end; false -> State end; add_bif_warnings(_, _, _, State) -> State. -is_int_float_eq_comp(T1, Op, T2) -> +is_int_float_eq_comp(T1, Op, T2, Opaques) -> (Op =:= '==' orelse Op =:= '/=') andalso - ((erl_types:t_is_float(T1) andalso erl_types:t_is_integer(T2)) orelse - (erl_types:t_is_integer(T1) andalso erl_types:t_is_float(T2))). + ((erl_types:t_is_float(T1, Opaques) + andalso t_is_integer(T2, Opaques)) orelse + (t_is_integer(T1, Opaques) + andalso erl_types:t_is_float(T2, Opaques))). + +comp_format_args([1|_], T1, Op, T2, State) -> + [format_type(T2, State), Op, format_type(T1, State)]; +comp_format_args(_, T1, Op, T2, State) -> + [format_type(T1, State), Op, format_type(T2, State)]. %%---------------------------------------- @@ -784,16 +790,27 @@ handle_bitstr(Tree, Map, State) -> {State3, Map2, t_none()}; false -> UnitVal = cerl:concrete(cerl:bitstr_unit(Tree)), - Type = - case t_number_vals(SizeType) of - [OneSize] -> t_bitstr(0, OneSize * UnitVal); - _ -> - MinSize = erl_types:number_min(SizeType), - t_bitstr(UnitVal, UnitVal * MinSize) - end, + Opaques = State2#state.opaques, + NumberVals = t_number_vals(SizeType, Opaques), + {State3, Type} = + case t_contains_opaque(SizeType, Opaques) of + true -> + Msg = {opaque_size, [format_type(SizeType, State2), + format_cerl(Size)]}, + {state__add_warning(State2, ?WARN_OPAQUE, Size, Msg), + t_none()}; + false -> + case NumberVals of + [OneSize] -> {State2, t_bitstr(0, OneSize * UnitVal)}; + unknown -> {State2, t_bitstr()}; + _ -> + MinSize = erl_types:number_min(SizeType, Opaques), + {State2, t_bitstr(UnitVal, UnitVal * MinSize)} + end + end, Map3 = enter_type_lists([Val, Size, Tree], [ValType, SizeType, Type], Map2), - {State2, Map3, Type} + {State3, Map3, Type} end end. @@ -805,34 +822,47 @@ handle_call(Tree, Map, State) -> Args = cerl:call_args(Tree), MFAList = [M, F|Args], {State1, Map1, [MType0, FType0|As]} = traverse_list(MFAList, Map, State), - %% Module and function names should be treated as *structured terms* - %% even if they happen to be identical to an atom (or tuple) which - %% is also involved in the definition of an opaque data type. - MType = t_inf(t_module(), t_unopaque(MType0)), - FType = t_inf(t_atom(), t_unopaque(FType0)), + Opaques = State#state.opaques, + MType = t_inf(t_module(), MType0, Opaques), + FType = t_inf(t_atom(), FType0, Opaques), Map2 = enter_type_lists([M, F], [MType, FType], Map1), + MOpaque = t_is_none(MType) andalso (not t_is_none(MType0)), + FOpaque = t_is_none(FType) andalso (not t_is_none(FType0)), case any_none([MType, FType|As]) of true -> State2 = - case t_is_none(MType) andalso (not t_is_none(MType0)) of - true -> % This is a problem we just detected; not a known one - MS = format_cerl(M), - Msg = {app_call, [MS, format_cerl(F), - format_args(Args, As, State1), - MS, format_type(t_module(), State1), - format_type(MType0, State1)]}, - state__add_warning(State1, ?WARN_FAILING_CALL, Tree, Msg); - false -> - case t_is_none(FType) andalso (not t_is_none(FType0)) of - true -> - FS = format_cerl(F), - Msg = {app_call, [format_cerl(M), FS, - format_args(Args, As, State1), - FS, format_type(t_atom(), State1), - format_type(FType0, State1)]}, - state__add_warning(State1, ?WARN_FAILING_CALL, Tree, Msg); - false -> State1 - end + if + MOpaque -> % This is a problem we just detected; not a known one + MS = format_cerl(M), + case t_is_none(t_inf(t_module(), MType0)) of + true -> + Msg = {app_call, [MS, format_cerl(F), + format_args(Args, As, State1), + MS, format_type(t_module(), State1), + format_type(MType0, State1)]}, + state__add_warning(State1, ?WARN_FAILING_CALL, Tree, Msg); + false -> + Msg = {opaque_call, [MS, format_cerl(F), + format_args(Args, As, State1), + MS, format_type(MType0, State1)]}, + state__add_warning(State1, ?WARN_FAILING_CALL, Tree, Msg) + end; + FOpaque -> + FS = format_cerl(F), + case t_is_none(t_inf(t_atom(), FType0)) of + true -> + Msg = {app_call, [format_cerl(M), FS, + format_args(Args, As, State1), + FS, format_type(t_atom(), State1), + format_type(FType0, State1)]}, + state__add_warning(State1, ?WARN_FAILING_CALL, Tree, Msg); + false -> + Msg = {opaque_call, [format_cerl(M), FS, + format_args(Args, As, State1), + FS, format_type(FType0, State1)]}, + state__add_warning(State1, ?WARN_FAILING_CALL, Tree, Msg) + end; + true -> State1 end, {State2, Map2, t_none()}; false -> @@ -874,7 +904,7 @@ handle_case(Tree, Map, State) -> handle_clauses(Clauses, Arg, ArgType, ArgType, State2, [], Map2, [], []), Map3 = join_maps_end(MapList, Map2), - debug_pp_map(Map2), + debug_pp_map(Map3), {State3, Map3, Type} end. @@ -886,7 +916,7 @@ handle_cons(Tree, Map, State) -> {State1, Map1, HdType} = traverse(Hd, Map, State), {State2, Map2, TlType} = traverse(Tl, Map1, State1), State3 = - case t_is_none(t_inf(TlType, t_list())) of + case t_is_none(t_inf(TlType, t_list(), State2#state.opaques)) of true -> Msg = {improper_list_constr, [format_type(TlType, State2)]}, state__add_warning(State2, ?WARN_NON_PROPER_LIST, Tree, Msg); @@ -979,8 +1009,9 @@ handle_receive(Tree, Map, State) -> [], []), Map1 = join_maps(MapList, Map), {State3, Map2, TimeoutType} = traverse(Timeout, Map1, State2), - case (t_is_atom(TimeoutType) andalso - (t_atom_vals(TimeoutType) =:= ['infinity'])) of + Opaques = State3#state.opaques, + case (t_is_atom(TimeoutType, Opaques) andalso + (t_atom_vals(TimeoutType, Opaques) =:= ['infinity'])) of true -> {State3, Map2, ReceiveType}; false -> @@ -1031,55 +1062,46 @@ handle_tuple(Tree, Map, State) -> true -> {State1, Map1, t_none()}; false -> - %% Let's find out if this is a record or opaque construction. + %% Let's find out if this is a record case Elements of [Tag|Left] -> case cerl:is_c_atom(Tag) of true -> TagVal = cerl:atom_val(Tag), - case t_opaque_match_record(TupleType, State1#state.opaques) of - [Opaque] -> - RecStruct = t_opaque_matching_structure(TupleType, Opaque), - RecFields = t_tuple_args(RecStruct), - case bind_pat_vars(Elements, RecFields, [], Map1, State1) of - {error, _, ErrorPat, ErrorType, _} -> - Msg = {record_constr, - [TagVal, format_patterns(ErrorPat), - format_type(ErrorType, State1)]}, - State2 = state__add_warning(State1, ?WARN_MATCHING, - Tree, Msg), - {State2, Map1, t_none()}; - {Map2, _ETypes} -> - {State1, Map2, Opaque} - end; - _ -> - case state__lookup_record(TagVal, length(Left), State1) of - error -> {State1, Map1, TupleType}; - {ok, RecType} -> - InfTupleType = t_inf(RecType, TupleType), - case t_is_none(InfTupleType) of - true -> - RecC = format_type(TupleType, State1), - FieldDiffs = format_field_diffs(TupleType, State1), - Msg = {record_constr, [RecC, FieldDiffs]}, - State2 = state__add_warning(State1, ?WARN_MATCHING, - Tree, Msg), - {State2, Map1, t_none()}; - false -> - case bind_pat_vars(Elements, t_tuple_args(RecType), - [], Map1, State1) of - {error, bind, ErrorPat, ErrorType, _} -> - Msg = {record_constr, - [TagVal, format_patterns(ErrorPat), - format_type(ErrorType, State1)]}, - State2 = state__add_warning(State1, ?WARN_MATCHING, - Tree, Msg), - {State2, Map1, t_none()}; - {Map2, ETypes} -> - {State1, Map2, t_tuple(ETypes)} - end - end - end + case state__lookup_record(TagVal, length(Left), State1) of + error -> {State1, Map1, TupleType}; + {ok, RecType} -> + InfTupleType = t_inf(RecType, TupleType), + case t_is_none(InfTupleType) of + true -> + RecC = format_type(TupleType, State1), + FieldDiffs = format_field_diffs(TupleType, State1), + Msg = {record_constr, [RecC, FieldDiffs]}, + State2 = state__add_warning(State1, ?WARN_MATCHING, + Tree, Msg), + {State2, Map1, t_none()}; + false -> + case bind_pat_vars(Elements, t_tuple_args(RecType), + [], Map1, State1) of + {error, bind, ErrorPat, ErrorType, _} -> + Msg = {record_constr, + [TagVal, format_patterns(ErrorPat), + format_type(ErrorType, State1)]}, + State2 = state__add_warning(State1, ?WARN_MATCHING, + Tree, Msg), + {State2, Map1, t_none()}; + {error, opaque, ErrorPat, ErrorType, OpaqueType} -> + Msg = {opaque_match, + [format_patterns(ErrorPat), + format_type(ErrorType, State1), + format_type(OpaqueType, State1)]}, + State2 = state__add_warning(State1, ?WARN_OPAQUE, + Tree, Msg), + {State2, Map1, t_none()}; + {Map2, ETypes} -> + {State1, Map2, t_tuple(ETypes)} + end + end end; false -> {State1, Map1, t_tuple(EsType)} @@ -1356,7 +1378,9 @@ bind_pat_vars_reverse(Pats, Types, Acc, Map, State) -> end. bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) -> - ?debug("Binding pat: ~w to ~s\n", [cerl:type(Pat), format_type(Type, State)]), + ?debug("Binding pat: ~w to ~s\n", [cerl:type(Pat), format_type(Type, State)] +), + Opaques = State#state.opaques, {NewMap, TypeOut} = case cerl:type(Pat) of alias -> @@ -1372,9 +1396,15 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) -> case Rev of true -> {Map, t_bitstr()}; false -> - BinType = t_inf(t_bitstr(), Type), + BinType = t_inf(t_bitstr(), Type, Opaques), case t_is_none(BinType) of - true -> bind_error([Pat], Type, t_none(), bind); + true -> + case t_find_opaque_mismatch(t_bitstr(), Type) of + {ok, T1, T2} -> + bind_error([Pat], T1, T2, opaque); + error -> + bind_error([Pat], Type, t_none(), bind) + end; false -> Segs = cerl:binary_segments(Pat), {Map1, SegTypes} = bind_bin_segs(Segs, BinType, Map, State), @@ -1382,28 +1412,24 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) -> end end; cons -> - Cons = t_inf(Type, t_cons()), + Cons = t_inf(Type, t_cons(), Opaques), case t_is_none(Cons) of true -> bind_opaque_pats(t_cons(), Type, Pat, Map, State, Rev); false -> {Map1, [HdType, TlType]} = bind_pat_vars([cerl:cons_hd(Pat), cerl:cons_tl(Pat)], - [t_cons_hd(Cons), t_cons_tl(Cons)], + [t_cons_hd(Cons, Opaques), + t_cons_tl(Cons, Opaques)], [], Map, State, Rev), {Map1, t_cons(HdType, TlType)} end; literal -> Literal = literal_type(Pat), - LiteralOrOpaque = - case t_opaque_match_atom(Literal, State#state.opaques) of - [Opaque] -> Opaque; - _ -> Literal - end, - case t_is_none(t_inf(LiteralOrOpaque, Type)) of + case t_is_none(t_inf(Literal, Type, Opaques)) of true -> bind_opaque_pats(Literal, Type, Pat, Map, State, Rev); - false -> {Map, LiteralOrOpaque} + false -> {Map, Literal} end; tuple -> Es = cerl:tuple_es(Pat), @@ -1419,27 +1445,28 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) -> {ok, Record} -> [_Head|AnyTail] = [t_any() || _ <- Es], UntypedRecord = t_tuple([t_atom(TagAtom)|AnyTail]), - {not erl_types:t_is_equal(Record, UntypedRecord), Record} + {not t_is_equal(Record, UntypedRecord), Record} end; false -> {false, t_tuple(length(Es))} end end, - Tuple = t_inf(Prototype, Type), + Tuple = t_inf(Prototype, Type, Opaques), case t_is_none(Tuple) of true -> bind_opaque_pats(Prototype, Type, Pat, Map, State, Rev); false -> - SubTuples = t_tuple_subtypes(Tuple), + SubTuples = t_tuple_subtypes(Tuple, Opaques), %% Need to call the top function to get the try-catch wrapper MapJ = join_maps_begin(Map), Results = case Rev of true -> - [bind_pat_vars_reverse(Es, t_tuple_args(SubTuple), [], - MapJ, State) + [bind_pat_vars_reverse(Es, t_tuple_args(SubTuple, Opaques), + [], MapJ, State) || SubTuple <- SubTuples]; false -> - [bind_pat_vars(Es, t_tuple_args(SubTuple), [], MapJ, State) + [bind_pat_vars(Es, t_tuple_args(SubTuple, Opaques), [], + MapJ, State) || SubTuple <- SubTuples] end, case lists:keyfind(opaque, 2, Results) of @@ -1466,37 +1493,14 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) -> bind_pat_vars(Es, t_to_tlist(Type), [], Map, State, Rev), {Map1, t_product(EsTypes)}; var -> - Opaques = State#state.opaques, VarType1 = case state__lookup_type_for_letrec(Pat, State) of - error -> - LType = lookup_type(Pat, Map), - case t_opaque_match_record(LType, Opaques) of - [Opaque] -> Opaque; - _ -> - case t_opaque_match_atom(LType, Opaques) of - [Opaque] -> Opaque; - _ -> LType - end - end; + error -> lookup_type(Pat, Map); {ok, RecType} -> RecType end, %% Must do inf when binding args to pats. Vars in pats are fresh. - VarType2 = t_inf(VarType1, Type), - VarType3 = - case Opaques =/= [] of - true -> - case t_opaque_match_record(VarType2, Opaques) of - [OpaqueRec] -> OpaqueRec; - _ -> - case t_opaque_match_atom(VarType2, Opaques) of - [OpaqueAtom] -> OpaqueAtom; - _ -> VarType2 - end - end; - false -> VarType2 - end, - case t_is_none(VarType3) of + VarType2 = t_inf(VarType1, Type, Opaques), + case t_is_none(VarType2) of true -> case t_find_opaque_mismatch(VarType1, Type) of {ok, T1, T2} -> @@ -1505,8 +1509,8 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) -> bind_error([Pat], Type, t_none(), bind) end; false -> - Map1 = enter_type(Pat, VarType3, Map), - {Map1, VarType3} + Map1 = enter_type(Pat, VarType2, Map), + {Map1, VarType2} end; _Other -> %% Catch all is needed when binding args to pats @@ -1529,7 +1533,8 @@ bind_bin_segs([Seg|Segs], BinType, Acc, Map, State) -> binary = SegType, [] = Segs, %% just an assert T = t_inf(t_bitstr(UnitVal, 0), BinType), {Map1, [Type]} = bind_pat_vars([Val], [T], [], Map, State, false), - bind_bin_segs(Segs, t_bitstr(0, 0), [Type|Acc], Map1, State); + Type1 = remove_local_opaque_types(Type, State#state.opaques), + bind_bin_segs(Segs, t_bitstr(0, 0), [Type1|Acc], Map1, State); utf -> % XXX: possibly can be strengthened true = lists:member(SegType, [utf8, utf16, utf32]), {Map1, [_]} = bind_pat_vars([Val], [t_integer()], [], Map, State, false), @@ -1539,11 +1544,17 @@ bind_bin_segs([Seg|Segs], BinType, Acc, Map, State) -> Size = cerl:bitstr_size(Seg), {Map1, [SizeType]} = bind_pat_vars([Size], [t_non_neg_integer()], [], Map, State, false), + Opaques = State#state.opaques, + NumberVals = t_number_vals(SizeType, Opaques), + case t_contains_opaque(SizeType, Opaques) of + true -> bind_error([Seg], SizeType, t_none(), opaque); + false -> ok + end, Type = - case t_number_vals(SizeType) of + case NumberVals of [OneSize] -> t_bitstr(0, UnitVal * OneSize); - _ -> - MinSize = erl_types:number_min(SizeType), + _ -> % 'unknown' too + MinSize = erl_types:number_min(SizeType, Opaques), t_bitstr(UnitVal, UnitVal * MinSize) end, ValConstr = @@ -1551,7 +1562,7 @@ bind_bin_segs([Seg|Segs], BinType, Acc, Map, State) -> binary -> Type; %% The same constraints as for the whole bitstr float -> t_float(); integer -> - case t_number_vals(SizeType) of + case NumberVals of unknown -> t_integer(); List -> SizeVal = lists:max(List), @@ -1579,7 +1590,7 @@ bind_error(Pats, Type, OpaqueType, Error) -> bind_opaque_pats(GenType, Type, Pat, Map, State, Rev) -> case t_find_opaque_mismatch(GenType, Type) of {ok, T1, T2} -> - case lists:member(T2, State#state.opaques) of + case erl_types:is_opaque_type(T2, State#state.opaques) of true -> NewType = erl_types:t_struct_from_opaque(Type, [T2]), {Map1, _} = @@ -1700,19 +1711,9 @@ handle_guard_call(Guard, Map, Env, Eval, State) -> handle_guard_gen_fun({M, F, A}, Guard, Map, Env, Eval, State) -> Args = cerl:call_args(Guard), - {Map1, As0} = bind_guard_list(Args, Map, Env, dont_know, State), - MapFun = fun(Type) -> - case lists:member(Type, State#state.opaques) of - true -> erl_types:t_opaque_structure(Type); - false -> Type - end - end, - As = lists:map(MapFun, As0), - Mode = case As =:= As0 of - true -> structured; - false -> opaque - end, - BifRet = erl_bif_types:type(M, F, A, As), + {Map1, As} = bind_guard_list(Args, Map, Env, dont_know, State), + Opaques = State#state.opaques, + BifRet = erl_bif_types:type(M, F, A, As, Opaques), case t_is_none(BifRet) of true -> %% Is this an error-bif? @@ -1721,11 +1722,8 @@ handle_guard_gen_fun({M, F, A}, Guard, Map, Env, Eval, State) -> false -> signal_guard_fatal_fail(Eval, Guard, As, State) end; false -> - BifArgs = case erl_bif_types:arg_types(M, F, A) of - unknown -> lists:duplicate(A, t_any()); - List -> List - end, - Map2 = enter_type_lists(Args, t_inf_lists(BifArgs, As0, Mode), Map1), + BifArgs = bif_args(M, F, A), + Map2 = enter_type_lists(Args, t_inf_lists(BifArgs, As, Opaques), Map1), Ret = case Eval of pos -> t_inf(t_atom(true), BifRet); @@ -1771,29 +1769,19 @@ bind_type_test(Eval, TypeTest, ArgType, State) -> is_reference -> t_reference(); is_tuple -> t_tuple() end, - Mode = determine_mode(ArgType, State#state.opaques), case Eval of pos -> - Inf = t_inf(Type, ArgType, Mode), + Inf = t_inf(Type, ArgType, State#state.opaques), case t_is_none(Inf) of true -> error; false -> {ok, Inf, t_atom(true)} end; neg -> - case Mode of - opaque -> - Struct = erl_types:t_opaque_structure(ArgType), - case t_is_none(t_subtract(Struct, Type)) of - true -> error; - false -> {ok, ArgType, t_atom(false)} - end; - structured -> - Sub = t_subtract(ArgType, Type), - case t_is_none(Sub) of - true -> error; - false -> {ok, Sub, t_atom(false)} - end - end; + Sub = t_subtract(ArgType, Type), + case t_is_none(Sub) of + true -> error; + false -> {ok, Sub, t_atom(false)} + end; dont_know -> {ok, ArgType, t_boolean()} end. @@ -1802,9 +1790,10 @@ handle_guard_comp(Guard, Comp, Map, Env, Eval, State) -> Args = cerl:call_args(Guard), [Arg1, Arg2] = Args, {Map1, ArgTypes} = bind_guard_list(Args, Map, Env, dont_know, State), + Opaques = State#state.opaques, [Type1, Type2] = ArgTypes, - IsInt1 = t_is_integer(Type1), - IsInt2 = t_is_integer(Type2), + IsInt1 = t_is_integer(Type1, Opaques), + IsInt2 = t_is_integer(Type2, Opaques), case {cerl:type(Arg1), cerl:type(Arg2)} of {literal, literal} -> case erlang:Comp(cerl:concrete(Arg1), cerl:concrete(Arg2)) of @@ -1817,12 +1806,13 @@ handle_guard_comp(Guard, Comp, Map, Env, Eval, State) -> false when Eval =:= neg -> {Map, t_atom(false)} end; {literal, var} when IsInt1 andalso IsInt2 andalso (Eval =:= pos) -> - case bind_comp_literal_var(Arg1, Arg2, Type2, Comp, Map1) of + case bind_comp_literal_var(Arg1, Arg2, Type2, Comp, Map1, Opaques) of error -> signal_guard_fail(Eval, Guard, ArgTypes, State); {ok, NewMap} -> {NewMap, t_atom(true)} end; {var, literal} when IsInt1 andalso IsInt2 andalso (Eval =:= pos) -> - case bind_comp_literal_var(Arg2, Arg1, Type1, invert_comp(Comp), Map1) of + case bind_comp_literal_var(Arg2, Arg1, Type1, invert_comp(Comp), + Map1, Opaques) of error -> signal_guard_fail(Eval, Guard, ArgTypes, State); {ok, NewMap} -> {NewMap, t_atom(true)} end; @@ -1835,10 +1825,10 @@ invert_comp('<') -> '>'; invert_comp('>=') -> '=<'; invert_comp('>') -> '<'. -bind_comp_literal_var(Lit, Var, VarType, CompOp, Map) -> +bind_comp_literal_var(Lit, Var, VarType, CompOp, Map, Opaques) -> LitVal = cerl:concrete(Lit), NewVarType = - case t_number_vals(VarType) of + case t_number_vals(VarType, Opaques) of unknown -> Range = case CompOp of @@ -1847,7 +1837,7 @@ bind_comp_literal_var(Lit, Var, VarType, CompOp, Map) -> '>=' -> t_from_range(neg_inf, LitVal); '>' -> t_from_range(neg_inf, LitVal - 1) end, - t_inf(Range, VarType); + t_inf(Range, VarType, Opaques); NumberVals -> NewNumberVals = [X || X <- NumberVals, erlang:CompOp(LitVal, X)], t_integers(NewNumberVals) @@ -1861,17 +1851,18 @@ handle_guard_is_function(Guard, Map, Env, Eval, State) -> Args = cerl:call_args(Guard), {Map1, ArgTypes0} = bind_guard_list(Args, Map, Env, dont_know, State), [FunType0, ArityType0] = ArgTypes0, - ArityType = t_inf(ArityType0, t_integer()), + Opaques = State#state.opaques, + ArityType = t_inf(ArityType0, t_integer(), Opaques), case t_is_none(ArityType) of true -> signal_guard_fail(Eval, Guard, ArgTypes0, State); false -> FunTypeConstr = - case t_number_vals(ArityType) of + case t_number_vals(ArityType, State#state.opaques) of unknown -> t_fun(); Vals -> t_sup([t_fun(lists:duplicate(X, t_any()), t_any()) || X <- Vals]) end, - FunType = t_inf(FunType0, FunTypeConstr), + FunType = t_inf(FunType0, FunTypeConstr, Opaques), case t_is_none(FunType) of true -> case Eval of @@ -1896,33 +1887,45 @@ handle_guard_is_record(Guard, Map, Env, Eval, State) -> Arity = cerl:int_val(Arity0), {Map1, RecType} = bind_guard(Rec, Map, Env, dont_know, State), ArityMin1 = Arity - 1, - TupleType = - case state__lookup_record(Tag, ArityMin1, State) of - error -> t_tuple([t_atom(Tag)|lists:duplicate(ArityMin1, t_any())]); - {ok, Prototype} -> Prototype - end, - Mode = determine_mode(RecType, State#state.opaques), - NewTupleType = - case t_opaque_match_record(TupleType, State#state.opaques) of - [Opaque] -> Opaque; - _ -> TupleType - end, - Type = t_inf(NewTupleType, RecType, Mode), - case t_is_none(Type) of + Opaques = State#state.opaques, + Tuple = t_tuple([t_atom(Tag)|lists:duplicate(ArityMin1, t_any())]), + case t_is_none(t_inf(Tuple, RecType, Opaques)) of true -> - case Eval of - pos -> signal_guard_fail(Eval, Guard, - [RecType, t_from_term(Tag), - t_from_term(Arity)], - State); - neg -> {Map1, t_atom(false)}; - dont_know -> {Map1, t_atom(false)} + case erl_types:t_has_opaque_subtype(RecType, Opaques) of + true -> + signal_guard_fail(Eval, Guard, + [RecType, t_from_term(Tag), + t_from_term(Arity)], + State); + false -> + case Eval of + pos -> signal_guard_fail(Eval, Guard, + [RecType, t_from_term(Tag), + t_from_term(Arity)], + State); + neg -> {Map1, t_atom(false)}; + dont_know -> {Map1, t_atom(false)} + end end; false -> - case Eval of - pos -> {enter_type(Rec, Type, Map1), t_atom(true)}; - neg -> {Map1, t_atom(false)}; - dont_know -> {Map1, t_boolean()} + TupleType = + case state__lookup_record(Tag, ArityMin1, State) of + error -> Tuple; + {ok, Prototype} -> Prototype + end, + Type = t_inf(TupleType, RecType, State#state.opaques), + case t_is_none(Type) of + true -> + %% No special handling of opaque errors. + FArgs = "record " ++ format_type(RecType, State), + Msg = {record_matching, [FArgs, Tag]}, + throw({fail, {Guard, Msg}}); + false -> + case Eval of + pos -> {enter_type(Rec, Type, Map1), t_atom(true)}; + neg -> {Map1, t_atom(false)}; + dont_know -> {Map1, t_boolean()} + end end end. @@ -1975,14 +1978,24 @@ handle_guard_eq(Guard, Map, Env, Eval, State) -> bind_eq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State) -> {Map1, Type1} = bind_guard(Arg1, Map, Env, dont_know, State), {Map2, Type2} = bind_guard(Arg2, Map1, Env, dont_know, State), - case (t_is_nil(Type1) orelse t_is_nil(Type2) orelse - t_is_atom(Type1) orelse t_is_atom(Type2)) of + Opaques = State#state.opaques, + case + t_is_nil(Type1, Opaques) orelse t_is_nil(Type2, Opaques) + orelse t_is_atom(Type1, Opaques) orelse t_is_atom(Type2, Opaques) + of true -> bind_eqeq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State); false -> - case Eval of - pos -> {Map2, t_atom(true)}; - neg -> {Map2, t_atom(false)}; - dont_know -> {Map2, t_boolean()} + %% XXX. Is this test OK? + OpArgs = erl_types:t_find_unknown_opaque(Type1, Type2, Opaques), + case OpArgs =:= [] of + true -> + case Eval of + pos -> {Map2, t_atom(true)}; + neg -> {Map2, t_atom(false)}; + dont_know -> {Map2, t_boolean()} + end; + false -> + signal_guard_fail(Eval, Guard, [Type1, Type2], State) end end. @@ -2021,44 +2034,52 @@ bind_eqeq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State) -> {Map2, Type2} = bind_guard(Arg2, Map1, Env, dont_know, State), ?debug("Types are:~s =:= ~s\n", [t_to_string(Type1), t_to_string(Type2)]), - Inf = t_inf(Type1, Type2), + Opaques = State#state.opaques, + Inf = t_inf(Type1, Type2, Opaques), case t_is_none(Inf) of true -> - case Eval of - neg -> {Map2, t_atom(false)}; - dont_know -> {Map2, t_atom(false)}; - pos -> signal_guard_fail(Eval, Guard, [Type1, Type2], State) + OpArgs = erl_types:t_find_unknown_opaque(Type1, Type2, Opaques), + case OpArgs =:= [] of + true -> + case Eval of + neg -> {Map2, t_atom(false)}; + dont_know -> {Map2, t_atom(false)}; + pos -> signal_guard_fail(Eval, Guard, [Type1, Type2], State) + end; + false -> + signal_guard_fail(Eval, Guard, [Type1, Type2], State) end; false -> case Eval of - pos -> - case {cerl:type(Arg1), cerl:type(Arg2)} of - {var, var} -> - Map3 = enter_subst(Arg1, Arg2, Map2), - Map4 = enter_type(Arg2, Inf, Map3), - {Map4, t_atom(true)}; - {var, _} -> - Map3 = enter_type(Arg1, Inf, Map2), - {Map3, t_atom(true)}; - {_, var} -> - Map3 = enter_type(Arg2, Inf, Map2), - {Map3, t_atom(true)}; - {_, _} -> - {Map2, t_atom(true)} - end; - neg -> - {Map2, t_atom(false)}; - dont_know -> - {Map2, t_boolean()} + pos -> + case {cerl:type(Arg1), cerl:type(Arg2)} of + {var, var} -> + Map3 = enter_subst(Arg1, Arg2, Map2), + Map4 = enter_type(Arg2, Inf, Map3), + {Map4, t_atom(true)}; + {var, _} -> + Map3 = enter_type(Arg1, Inf, Map2), + {Map3, t_atom(true)}; + {_, var} -> + Map3 = enter_type(Arg2, Inf, Map2), + {Map3, t_atom(true)}; + {_, _} -> + {Map2, t_atom(true)} + end; + neg -> + {Map2, t_atom(false)}; + dont_know -> + {Map2, t_boolean()} end end. bind_eqeq_guard_lit_other(Guard, Arg1, Arg2, Map, Env, State) -> Eval = dont_know, + Opaques = State#state.opaques, case cerl:concrete(Arg1) of true -> {_, Type} = MT = bind_guard(Arg2, Map, Env, pos, State), - case t_is_atom(true, Type) of + case t_is_any_atom(true, Type, Opaques) of true -> MT; false -> {_, Type0} = bind_guard(Arg2, Map, Env, Eval, State), @@ -2066,7 +2087,7 @@ bind_eqeq_guard_lit_other(Guard, Arg1, Arg2, Map, Env, State) -> end; false -> {Map1, Type} = bind_guard(Arg2, Map, Env, neg, State), - case t_is_atom(false, Type) of + case t_is_any_atom(false, Type, Opaques) of true -> {Map1, t_atom(true)}; false -> {_, Type0} = bind_guard(Arg2, Map, Env, Eval, State), @@ -2087,14 +2108,15 @@ bind_eqeq_guard_lit_other(Guard, Arg1, Arg2, Map, Env, State) -> handle_guard_and(Guard, Map, Env, Eval, State) -> [Arg1, Arg2] = cerl:call_args(Guard), + Opaques = State#state.opaques, case Eval of pos -> {Map1, Type1} = bind_guard(Arg1, Map, Env, Eval, State), - case t_is_atom(true, Type1) of + case t_is_any_atom(true, Type1, Opaques) of false -> signal_guard_fail(Eval, Guard, [Type1, t_any()], State); true -> {Map2, Type2} = bind_guard(Arg2, Map1, Env, Eval, State), - case t_is_atom(true, Type2) of + case t_is_any_atom(true, Type2, Opaques) of false -> signal_guard_fail(Eval, Guard, [Type1, Type2], State); true -> {Map2, t_atom(true)} end @@ -2109,7 +2131,10 @@ handle_guard_and(Guard, Map, Env, Eval, State) -> try bind_guard(Arg2, MapJ, Env, neg, State) catch throw:{fail, _} -> bind_guard(Arg1, MapJ, Env, pos, State) end, - case t_is_atom(false, Type1) orelse t_is_atom(false, Type2) of + case + t_is_any_atom(false, Type1, Opaques) + orelse t_is_any_atom(false, Type2, Opaques) + of true -> {join_maps_end([Map1, Map2], MapJ), t_atom(false)}; false -> signal_guard_fail(Eval, Guard, [Type1, Type2], State) end; @@ -2124,11 +2149,16 @@ handle_guard_and(Guard, Map, Env, Eval, State) -> false -> NewMap = join_maps_end([Map1, Map2], MapJ), NewType = - case {t_atom_vals(Bool1), t_atom_vals(Bool2)} of + case {t_atom_vals(Bool1, Opaques), t_atom_vals(Bool2, Opaques)} of {['true'] , ['true'] } -> t_atom(true); {['false'], _ } -> t_atom(false); {_ , ['false']} -> t_atom(false); + {unknown , _ } -> + signal_guard_fail(Eval, Guard, [Type1, Type2], State); + {_ , unknown } -> + signal_guard_fail(Eval, Guard, [Type1, Type2], State); {_ , _ } -> t_boolean() + end, {NewMap, NewType} end @@ -2136,6 +2166,7 @@ handle_guard_and(Guard, Map, Env, Eval, State) -> handle_guard_or(Guard, Map, Env, Eval, State) -> [Arg1, Arg2] = cerl:call_args(Guard), + Opaques = State#state.opaques, case Eval of pos -> MapJ = join_maps_begin(Map), @@ -2149,19 +2180,23 @@ handle_guard_or(Guard, Map, Env, Eval, State) -> catch throw:{fail,_} -> bind_guard(Arg2, MapJ, Env, dont_know, State) end, - case ((t_is_atom(true, Bool1) andalso t_is_boolean(Bool2)) - orelse - (t_is_atom(true, Bool2) andalso t_is_boolean(Bool1))) of + case + ((t_is_any_atom(true, Bool1, Opaques) + andalso t_is_boolean(Bool2, Opaques)) + orelse + (t_is_any_atom(true, Bool2, Opaques) + andalso t_is_boolean(Bool1, Opaques))) + of true -> {join_maps_end([Map1, Map2], MapJ), t_atom(true)}; false -> signal_guard_fail(Eval, Guard, [Bool1, Bool2], State) end; neg -> {Map1, Type1} = bind_guard(Arg1, Map, Env, neg, State), - case t_is_atom(false, Type1) of + case t_is_any_atom(false, Type1, Opaques) of false -> signal_guard_fail(Eval, Guard, [Type1, t_any()], State); true -> {Map2, Type2} = bind_guard(Arg2, Map1, Env, neg, State), - case t_is_atom(false, Type2) of + case t_is_any_atom(false, Type2, Opaques) of false -> signal_guard_fail(Eval, Guard, [Type1, Type2], State); true -> {Map2, t_atom(false)} end @@ -2177,10 +2212,14 @@ handle_guard_or(Guard, Map, Env, Eval, State) -> false -> NewMap = join_maps_end([Map1, Map2], MapJ), NewType = - case {t_atom_vals(Bool1), t_atom_vals(Bool2)} of + case {t_atom_vals(Bool1, Opaques), t_atom_vals(Bool2, Opaques)} of {['false'], ['false']} -> t_atom(false); {['true'] , _ } -> t_atom(true); {_ , ['true'] } -> t_atom(true); + {unknown , _ } -> + signal_guard_fail(Eval, Guard, [Type1, Type2], State); + {_ , unknown } -> + signal_guard_fail(Eval, Guard, [Type1, Type2], State); {_ , _ } -> t_boolean() end, {NewMap, NewType} @@ -2189,10 +2228,11 @@ handle_guard_or(Guard, Map, Env, Eval, State) -> handle_guard_not(Guard, Map, Env, Eval, State) -> [Arg] = cerl:call_args(Guard), + Opaques = State#state.opaques, case Eval of neg -> {Map1, Type} = bind_guard(Arg, Map, Env, pos, State), - case t_is_atom(true, Type) of + case t_is_any_atom(true, Type, Opaques) of true -> {Map1, t_atom(false)}; false -> {_, Type0} = bind_guard(Arg, Map, Env, Eval, State), @@ -2200,7 +2240,7 @@ handle_guard_not(Guard, Map, Env, Eval, State) -> end; pos -> {Map1, Type} = bind_guard(Arg, Map, Env, neg, State), - case t_is_atom(false, Type) of + case t_is_any_atom(false, Type, Opaques) of true -> {Map1, t_atom(true)}; false -> {_, Type0} = bind_guard(Arg, Map, Env, Eval, State), @@ -2212,10 +2252,11 @@ handle_guard_not(Guard, Map, Env, Eval, State) -> case t_is_none(Bool) of true -> throw({fatal_fail, none}); false -> - case t_atom_vals(Bool) of + case t_atom_vals(Bool, Opaques) of ['true'] -> {Map1, t_atom(false)}; ['false'] -> {Map1, t_atom(true)}; - [_, _] -> {Map1, Bool} + [_, _] -> {Map1, Bool}; + unknown -> signal_guard_fail(Eval, Guard, [Type], State) end end end. @@ -2235,27 +2276,40 @@ bind_guard_list([], Map, _Env, _Eval, _State, Acc) -> state()) -> no_return(). signal_guard_fail(Eval, Guard, ArgTypes, State) -> + signal_guard_failure(Eval, Guard, ArgTypes, fail, State). + +signal_guard_fatal_fail(Eval, Guard, ArgTypes, State) -> + signal_guard_failure(Eval, Guard, ArgTypes, fatal_fail, State). + +signal_guard_failure(Eval, Guard, ArgTypes, Tag, State) -> Args = cerl:call_args(Guard), F = cerl:atom_val(cerl:call_name(Guard)), - MFA = {cerl:atom_val(cerl:call_module(Guard)), F, length(Args)}, - Msg = + {M, F, A} = MFA = {cerl:atom_val(cerl:call_module(Guard)), F, length(Args)}, + Opaques = State#state.opaques, + {Kind, XInfo} = + case erl_bif_types:opaque_args(M, F, A, ArgTypes, Opaques) of + [] -> + {case Eval of + neg -> neg_guard_fail; + pos -> guard_fail; + dont_know -> guard_fail + end, + []}; + Ns -> {opaque_guard, [Ns]} + end, + FArgs = case is_infix_op(MFA) of true -> [ArgType1, ArgType2] = ArgTypes, [Arg1, Arg2] = Args, - Kind = - case Eval of - neg -> neg_guard_fail; - pos -> guard_fail; - dont_know -> guard_fail - end, - {Kind, [format_args_1([Arg1], [ArgType1], State), - atom_to_list(F), - format_args_1([Arg2], [ArgType2], State)]}; + [format_args_1([Arg1], [ArgType1], State), + atom_to_list(F), + format_args_1([Arg2], [ArgType2], State)] ++ XInfo; false -> - mk_guard_msg(Eval, F, Args, ArgTypes, State) + [F, format_args(Args, ArgTypes, State)] end, - throw({fail, {Guard, Msg}}). + Msg = {Kind, FArgs}, + throw({Tag, {Guard, Msg}}). is_infix_op({erlang, '=:=', 2}) -> true; is_infix_op({erlang, '==', 2}) -> true; @@ -2268,25 +2322,10 @@ is_infix_op({erlang, '>=', 2}) -> true; is_infix_op({M, F, A}) when is_atom(M), is_atom(F), is_integer(A), 0 =< A, A =< 255 -> false. --spec signal_guard_fatal_fail(eval(), cerl:c_call(), [erl_types:erl_type()], - state()) -> no_return(). - -signal_guard_fatal_fail(Eval, Guard, ArgTypes, State) -> - Args = cerl:call_args(Guard), - F = cerl:atom_val(cerl:call_name(Guard)), - Msg = mk_guard_msg(Eval, F, Args, ArgTypes, State), - throw({fatal_fail, {Guard, Msg}}). - -mk_guard_msg(Eval, F, Args, ArgTypes, State) -> - FArgs = [F, format_args(Args, ArgTypes, State)], - case any_has_opaque_subtype(ArgTypes) of - true -> {opaque_guard, FArgs}; - false -> - case Eval of - neg -> {neg_guard_fail, FArgs}; - pos -> {guard_fail, FArgs}; - dont_know -> {guard_fail, FArgs} - end +bif_args(M, F, A) -> + case erl_bif_types:arg_types(M, F, A) of + unknown -> lists:duplicate(A, t_any()); + List -> List end. bind_guard_case_clauses(Arg, Clauses, Map0, Env, Eval, State) -> @@ -2366,14 +2405,15 @@ bind_guard_case_clauses(GenArgType, GenMap, ArgExpr, [Clause|Left], end, {NewMap3, CType} = bind_guard(cerl:clause_body(Clause), NewMap2, Env, Eval, State), + Opaques = State#state.opaques, case Eval of pos -> - case t_is_atom(true, CType) of + case t_is_any_atom(true, CType, Opaques) of true -> ok; false -> throw({fail, none}) end; neg -> - case t_is_atom(false, CType) of + case t_is_any_atom(false, CType, Opaques) of true -> ok; false -> throw({fail, none}) end; @@ -2501,8 +2541,11 @@ enter_type(Key, Val, MS) -> error -> ?debug("Entering ~p :: ~s\n", [KeyLabel, t_to_string(Val)]), case dict:find(KeyLabel, Dict) of - {ok, Val} -> MS; - {ok, _OldVal} -> store_map(KeyLabel, Val, MS); + {ok, Value} -> + case erl_types:t_is_equal(Val, Value) of + true -> MS; + false -> store_map(KeyLabel, Val, MS) + end; error -> store_map(KeyLabel, Val, MS) end end @@ -2611,10 +2654,15 @@ get_label(L) when is_integer(L) -> get_label(T) -> cerl_trees:get_label(T). -t_is_simple(ArgType) -> - t_is_atom(ArgType) orelse t_is_number(ArgType) orelse t_is_port(ArgType) - orelse t_is_pid(ArgType) orelse t_is_reference(ArgType) - orelse t_is_nil(ArgType). +t_is_simple(ArgType, State) -> + Opaques = State#state.opaques, + t_is_atom(ArgType, Opaques) orelse t_is_number(ArgType, Opaques) + orelse t_is_port(ArgType, Opaques) + orelse t_is_pid(ArgType, Opaques) orelse t_is_reference(ArgType, Opaques) + orelse t_is_nil(ArgType, Opaques). + +remove_local_opaque_types(Type, Opaques) -> + t_unopaque(Type, Opaques). %% t_is_structured(ArgType) -> %% case t_is_nil(ArgType) of @@ -2638,12 +2686,6 @@ is_call_to_send(Tree) -> andalso (Arity =:= 2) end. -any_opaque(Ts) -> - lists:any(fun erl_types:t_is_opaque/1, Ts). - -any_has_opaque_subtype(Ts) -> - lists:any(fun erl_types:t_has_opaque_subtype/1, Ts). - filter_match_fail([Clause] = Cls) -> Body = cerl:clause_body(Clause), case cerl:type(Body) of @@ -2662,12 +2704,6 @@ filter_match_fail([]) -> %% receive after 1 -> ok end []. -determine_mode(Type, Opaques) -> - case lists:member(Type, Opaques) of - true -> opaque; - false -> structured - end. - %%% =========================================================================== %%% %%% The State. @@ -2679,7 +2715,7 @@ state__new(Callgraph, Tree, Plt, Module, Records) -> erl_types:t_opaque_from_records(Records), TreeMap = build_tree_map(Tree), Funs = dict:fetch_keys(TreeMap), - FunTab = init_fun_tab(Funs, dict:new(), TreeMap, Callgraph, Plt, Opaques), + FunTab = init_fun_tab(Funs, dict:new(), TreeMap, Callgraph, Plt), ExportedFuns = [Fun || Fun <- Funs--[top], dialyzer_callgraph:is_escaping(Fun, Callgraph)], Work = init_work(ExportedFuns), @@ -2740,12 +2776,14 @@ state__add_warning(#state{warnings = Warnings, warning_mode = true} = State, case Force of true -> Warn = {Tag, {get_file(Ann), abs(get_line(Ann))}, Msg}, + ?debug("MSG ~s\n", [dialyzer:format_warning(Warn)]), State#state{warnings = [Warn|Warnings]}; false -> case is_compiler_generated(Ann) of true -> State; false -> Warn = {Tag, {get_file(Ann), get_line(Ann)}, Msg}, + ?debug("MSG ~s\n", [dialyzer:format_warning(Warn)]), State#state{warnings = [Warn|Warnings]} end end. @@ -2875,10 +2913,10 @@ build_tree_map(Tree) -> end, cerl_trees:fold(Fun, dict:new(), Tree). -init_fun_tab([top|Left], Dict, TreeMap, Callgraph, Plt, Opaques) -> +init_fun_tab([top|Left], Dict, TreeMap, Callgraph, Plt) -> NewDict = dict:store(top, {[], t_none()}, Dict), - init_fun_tab(Left, NewDict, TreeMap, Callgraph, Plt, Opaques); -init_fun_tab([Fun|Left], Dict, TreeMap, Callgraph, Plt, Opaques) -> + init_fun_tab(Left, NewDict, TreeMap, Callgraph, Plt); +init_fun_tab([Fun|Left], Dict, TreeMap, Callgraph, Plt) -> Arity = cerl:fun_arity(dict:fetch(Fun, TreeMap)), FunEntry = case dialyzer_callgraph:is_escaping(Fun, Callgraph) of @@ -2895,8 +2933,8 @@ init_fun_tab([Fun|Left], Dict, TreeMap, Callgraph, Plt, Opaques) -> false -> {not_handled, {lists:duplicate(Arity, t_none()), t_unit()}} end, NewDict = dict:store(Fun, FunEntry, Dict), - init_fun_tab(Left, NewDict, TreeMap, Callgraph, Plt, Opaques); -init_fun_tab([], Dict, _TreeMap, _Callgraph, _Plt, _Opaques) -> + init_fun_tab(Left, NewDict, TreeMap, Callgraph, Plt); +init_fun_tab([], Dict, _TreeMap, _Callgraph, _Plt) -> ?debug("DICT:~p\n",[dict:to_list(Dict)]), Dict. @@ -2945,34 +2983,27 @@ state__update_fun_entry(Tree, ArgTypes, Out0, if Fun =:= top -> Out0; true -> case lookup_fun_sig(Fun, CG, Plt) of - {value, {SigRet, _}} -> t_inf(SigRet, Out0, opaque); + {value, {SigRet, _}} -> t_inf(SigRet, Out0); none -> Out0 end end, Out = t_limit(Out1, ?TYPE_LIMIT), - case dict:find(Fun, FunTab) of - {ok, {ArgTypes, OldOut}} -> - case t_is_equal(OldOut, Out) of - true -> - ?debug("Fixpoint for ~w: ~s\n", - [state__lookup_name(Fun, State), - t_to_string(t_fun(ArgTypes, Out))]), - State; - false -> - NewEntry = {ArgTypes, Out}, - ?debug("New Entry for ~w: ~s\n", - [state__lookup_name(Fun, State), - t_to_string(t_fun(ArgTypes, Out))]), - NewFunTab = dict:store(Fun, NewEntry, FunTab), - State1 = State#state{fun_tab = NewFunTab}, - state__add_work_from_fun(Tree, State1) - end; - {ok, {NewArgTypes, _OldOut}} -> - %% Can only happen in self-recursive functions. Only update the out type. - NewEntry = {NewArgTypes, Out}, + {ok, {OldArgTypes, OldOut}} = dict:find(Fun, FunTab), + SameArgs = lists:all(fun({A, B}) -> erl_types:t_is_equal(A, B) + end, lists:zip(OldArgTypes, ArgTypes)), + SameOut = t_is_equal(OldOut, Out), + if + SameArgs, SameOut -> + ?debug("Fixpoint for ~w: ~s\n", + [state__lookup_name(Fun, State), + t_to_string(t_fun(ArgTypes, Out))]), + State; + true -> + %% Can only happen in self-recursive functions. + NewEntry = {OldArgTypes, Out}, ?debug("New Entry for ~w: ~s\n", [state__lookup_name(Fun, State), - t_to_string(t_fun(NewArgTypes, Out))]), + t_to_string(t_fun(OldArgTypes, Out))]), NewFunTab = dict:store(Fun, NewEntry, FunTab), State1 = State#state{fun_tab = NewFunTab}, state__add_work_from_fun(Tree, State1) @@ -2993,7 +3024,7 @@ state__add_work_from_fun(Tree, #state{callgraph = Callgraph, %% Must filter the result for results in this module. FilteredList = [L || {ok, L} <- LabelList, dict:is_key(L, TreeMap)], ?debug("~w: Will try to add:~w\n", - [state__lookup_name(get_label(Tree), State), MFAList]), + [state__lookup_name(Label, State), MFAList]), lists:foldl(fun(L, AccState) -> state__add_work(L, AccState) end, State, FilteredList) @@ -3054,7 +3085,8 @@ forward_args(Fun, ArgTypes, #state{work = Work, fun_tab = FunTab} = State) -> case Fixpoint of true -> State; false -> - NewArgTypes = [t_sup(X, Y) || {X, Y} <- lists:zip(ArgTypes, OldArgTypes)], + NewArgTypes = [t_sup(X, Y) || + {X, Y} <- lists:zip(ArgTypes, OldArgTypes)], NewWork = add_work(Fun, Work), ?debug("~w: forwarding args ~s\n", [state__lookup_name(Fun, State), @@ -3238,13 +3270,13 @@ format_field_diffs(RecConstruction, #state{records = R}) -> -spec format_sig_args(erl_types:erl_type(), state()) -> string(). -format_sig_args(Type, #state{records = R}) -> - SigArgs = t_fun_args(Type), +format_sig_args(Type, #state{opaques = Opaques} = State) -> + SigArgs = t_fun_args(Type, Opaques), case SigArgs of [] -> "()"; [SArg|SArgs] -> - lists:flatten("(" ++ t_to_string(SArg, R) - ++ ["," ++ t_to_string(T, R) || T <- SArgs] ++ ")") + lists:flatten("(" ++ format_type(SArg, State) + ++ ["," ++ format_type(T, State) || T <- SArgs] ++ ")") end. format_cerl(Tree) -> diff --git a/lib/dialyzer/src/dialyzer_succ_typings.erl b/lib/dialyzer/src/dialyzer_succ_typings.erl index 84379642bf..f0488b5ee3 100644 --- a/lib/dialyzer/src/dialyzer_succ_typings.erl +++ b/lib/dialyzer/src/dialyzer_succ_typings.erl @@ -2,7 +2,7 @@ %%----------------------------------------------------------------------- %% %CopyrightBegin% %% -%% Copyright Ericsson AB 2006-2012. All Rights Reserved. +%% Copyright Ericsson AB 2006-2014. 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 @@ -149,8 +149,10 @@ get_warnings(Callgraph, Plt, DocPlt, Codeserver, NewState = InitState#st{no_warn_unused = NoWarnUnused}, Mods = dialyzer_callgraph:modules(NewState#st.callgraph), MiniPlt = NewState#st.plt, + FindOpaques = lookup_and_find_opaques_fun(Codeserver), CWarns = - dialyzer_contracts:get_invalid_contract_warnings(Mods, Codeserver, MiniPlt), + dialyzer_contracts:get_invalid_contract_warnings(Mods, Codeserver, + MiniPlt, FindOpaques), MiniDocPlt = dialyzer_plt:get_mini_plt(DocPlt), ModWarns = ?timing(TimingServer, "warning", @@ -261,7 +263,16 @@ refine_one_module(M, {CodeServer, Callgraph, Plt, _Solvers}) -> FunTypes = get_fun_types_from_plt(AllFuns, Callgraph, Plt), NewFunTypes = dialyzer_dataflow:get_fun_types(ModCode, Plt, Callgraph, Records), - case reached_fixpoint(FunTypes, NewFunTypes) of + Contracts1 = dialyzer_codeserver:lookup_mod_contracts(M, CodeServer), + Contracts = orddict:from_list(dict:to_list(Contracts1)), + FindOpaques = find_opaques_fun(Records), + DecoratedFunTypes = + decorate_succ_typings(Contracts, Callgraph, NewFunTypes, FindOpaques), + %% ?debug("NewFunTypes ~p\n ~n", [dict:to_list(NewFunTypes)]), + %% ?debug("refine DecoratedFunTypes ~p\n ~n", [dict:to_list(DecoratedFunTypes)]), + debug_pp_functions("Refine", NewFunTypes, DecoratedFunTypes, Callgraph), + + case reached_fixpoint(FunTypes, DecoratedFunTypes) of true -> []; {false, NotFixpoint} -> ?debug("Not fixpoint\n", []), @@ -357,9 +368,16 @@ find_succ_types_for_scc(SCC, {Codeserver, Callgraph, Plt, Solvers}) -> AllFunSet = sets:from_list([X || {X, _} <- AllFuns]), FilteredFunTypes = dict:filter(fun(X, _) -> sets:is_element(X, AllFunSet) end, FunTypes), + FindOpaques = lookup_and_find_opaques_fun(Codeserver), + DecoratedFunTypes = + decorate_succ_typings(Contracts3, Callgraph, FilteredFunTypes, FindOpaques), %% Check contracts PltContracts = - dialyzer_contracts:check_contracts(Contracts3, Callgraph, FilteredFunTypes), + dialyzer_contracts:check_contracts(Contracts3, Callgraph, + DecoratedFunTypes, FindOpaques), + %% ?debug("FilteredFunTypes ~p\n ~n", [dict:to_list(FilteredFunTypes)]), + %% ?debug("SCC DecoratedFunTypes ~p\n ~n", [dict:to_list(DecoratedFunTypes)]), + debug_pp_functions("SCC", FilteredFunTypes, DecoratedFunTypes, Callgraph), ContractFixpoint = lists:all(fun({MFA, _C}) -> %% Check the non-deleted PLT @@ -368,16 +386,47 @@ find_succ_types_for_scc(SCC, {Codeserver, Callgraph, Plt, Solvers}) -> {value, _} -> true end end, PltContracts), - Plt = insert_into_plt(FilteredFunTypes, Callgraph, Plt), + Plt = insert_into_plt(DecoratedFunTypes, Callgraph, Plt), Plt = dialyzer_plt:insert_contract_list(Plt, PltContracts), case (ContractFixpoint andalso - reached_fixpoint_strict(PropTypes, FilteredFunTypes)) of + reached_fixpoint_strict(PropTypes, DecoratedFunTypes)) of true -> []; false -> ?debug("Not fixpoint for: ~w\n", [AllFuns]), [Fun || {Fun, _Arity} <- AllFuns] end. +decorate_succ_typings(Contracts, Callgraph, FunTypes, FindOpaques) -> + F = fun(Label, Type) -> + case dialyzer_callgraph:lookup_name(Label, Callgraph) of + {ok, MFA} -> + case orddict:find(MFA, Contracts) of + {ok, {_FileLine, Contract}} -> + Args = dialyzer_contracts:get_contract_args(Contract), + Ret = dialyzer_contracts:get_contract_return(Contract), + C = erl_types:t_fun(Args, Ret), + {M, _, _} = MFA, + Opaques = FindOpaques(M), + erl_types:t_decorate_with_opaque(Type, C, Opaques); + error -> Type + end; + error -> Type + end + end, + dict:map(F, FunTypes). + +lookup_and_find_opaques_fun(Codeserver) -> + fun(Module) -> + Records = dialyzer_codeserver:lookup_mod_records(Module, Codeserver), + (find_opaques_fun(Records))(Module) + end. + +find_opaques_fun(Records) -> + fun(Module) -> + erl_types:module_builtin_opaques(Module) ++ + erl_types:t_opaque_from_records(Records) + end. + get_fun_types_from_plt(FunList, Callgraph, Plt) -> get_fun_types_from_plt(FunList, Callgraph, Plt, dict:new()). @@ -443,9 +492,30 @@ debug_pp_succ_typings(SuccTypes) -> || {MFA, {contract, RetFun, ArgT}} <- SuccTypes], ?debug("\n", []), ok. + +debug_pp_functions(Header, FunTypes, DecoratedFunTypes, Callgraph) -> + ?debug("FunTypes (~s)\n", [Header]), + FTypes = lists:keysort(1, dict:to_list(FunTypes)), + DTypes = lists:keysort(1, dict:to_list(DecoratedFunTypes)), + Fun = fun({{Label, Type},{Label, DecoratedType}}) -> + Name = lookup_name(Label, Callgraph), + ?debug("~w (~w): ~s\n", + [Name, Label, erl_types:t_to_string(Type)]), + case erl_types:t_is_equal(Type, DecoratedType) of + true -> ok; + false -> + ?debug(" With opaque types: ~s\n", + [erl_types:t_to_string(DecoratedType)]) + end + end, + lists:foreach(Fun, lists:zip(FTypes, DTypes)), + ?debug("\n", []). -else. debug_pp_succ_typings(_) -> ok. + +debug_pp_functions(_, _, _, _) -> + ok. -endif. lookup_name(F, CG) -> diff --git a/lib/dialyzer/src/dialyzer_typesig.erl b/lib/dialyzer/src/dialyzer_typesig.erl index a418a11e65..db7875704a 100644 --- a/lib/dialyzer/src/dialyzer_typesig.erl +++ b/lib/dialyzer/src/dialyzer_typesig.erl @@ -2,7 +2,7 @@ %%----------------------------------------------------------------------- %% %CopyrightBegin% %% -%% Copyright Ericsson AB 2006-2013. All Rights Reserved. +%% Copyright Ericsson AB 2006-2014. 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 @@ -31,28 +31,30 @@ -export([analyze_scc/6]). -export([get_safe_underapprox/2]). +%%-import(helper, %% 'helper' could be any module doing sanity checks... +-import(erl_types, + [t_has_var/1, t_inf/2, t_is_equal/2, t_is_subtype/2, + t_subtract/2, t_subtract_list/2, t_sup/1, t_sup/2,t_unify/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_integer/0, + t_is_any/1, t_is_atom/1, t_is_any_atom/2, t_is_cons/1, 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_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_subst/2, t_timeout/0, t_tuple/0, t_tuple/1, - t_unify/3, t_var/1, t_var_name/1, + t_var/1, t_var_name/1, t_none/0, t_unit/0]). -include("dialyzer.hrl"). @@ -105,11 +107,10 @@ module :: module(), name_map = dict:new() :: dict(), next_label = 0 :: label(), - self_rec :: erl_types:erl_type(), + self_rec :: 'false' | 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()] @@ -192,11 +193,10 @@ solvers(Solvers) -> Solvers. %% %% ============================================================================ -traverse_scc([{MFA, Def, Rec}|Left], DefSet, AccState) -> +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), + {NewAccState, _} = traverse(DummyLetrec, DefSet, TmpState1), traverse_scc(Left, DefSet, NewAccState); traverse_scc([], _DefSet, AccState) -> AccState. @@ -386,12 +386,7 @@ traverse(Tree, DefinedVars, State) -> 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}; + {State, Type}; NewTree -> traverse(NewTree, DefinedVars, State) end; module -> @@ -462,25 +457,17 @@ traverse(Tree, DefinedVars, State) -> [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; + %% 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; false -> {State2, TupleType} - end; + end; [] -> {State2, TupleType} end; values -> @@ -591,9 +578,13 @@ handle_try(Tree, DefinedVars, State) -> case state__is_in_guard(State) of true -> Conj1 = mk_conj_constraint_list([ArgBodyCs, - mk_constraint(BodyVar, eq, TreeVar)]), + mk_constraint(BodyVar, + eq, + TreeVar)]), Disj = mk_disj_constraint_list([Conj1, - mk_constraint(HandlerVar, eq, TreeVar)]), + mk_constraint(HandlerVar, + eq, + TreeVar)]), NewState1 = state__new_constraint_context(HandlerState), Conj2 = mk_conj_constraint_list([OldCs, Disj]), NewState2 = state__store_conj(Conj2, NewState1), @@ -604,19 +595,27 @@ handle_try(Tree, DefinedVars, State) -> {false, false} -> Conj1 = mk_conj_constraint_list([ArgBodyCs, - mk_constraint(TreeVar, eq, BodyVar)]), + mk_constraint(TreeVar, + eq, + BodyVar)]), Conj2 = mk_conj_constraint_list([HandlerCs, - mk_constraint(TreeVar, eq, HandlerVar)]), + 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)]), + mk_constraint(TreeVar, + eq, + BodyVar)]), BodyVar}; {true, false} -> {mk_conj_constraint_list([HandlerCs, - mk_constraint(TreeVar, eq, HandlerVar)]), + mk_constraint(TreeVar, + eq, + HandlerVar)]), HandlerVar}; {true, true} -> ?debug("Throw failed\n", []), @@ -668,10 +667,7 @@ handle_call(Call, DefinedVars, State) -> 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; @@ -691,28 +687,24 @@ get_plt_constr(MFA, Dst, ArgVars, State) -> none -> {?mk_fun_var(fun(Map) -> ArgTypes = lookup_type_list(ArgVars, Map), - dialyzer_contracts:get_contract_return(C, ArgTypes) + 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) + ArgTypes = lookup_type_list(ArgVars, Map), + CRet = get_contract_return(C, ArgTypes), + t_inf(CRet, PltRetType) end, ArgVars), - [t_inf(X, Y, opaque) || {X, Y} <- lists:zip(GenArgs, PltArgTypes)]} + [t_inf(X, Y) || {X, Y} <- lists:zip(GenArgs, PltArgTypes)]} end, state__store_conj_lists([Dst|ArgVars], sub, [RetType|ArgCs], State) end. +get_contract_return(C, ArgTypes) -> + dialyzer_contracts:get_contract_return(C, ArgTypes). + filter_match_fail([Clause] = Cls) -> Body = cerl:clause_body(Clause), case cerl:type(Body) of @@ -1086,7 +1078,7 @@ 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) + bif_return(erlang, Op, 2, TmpArgTypes) end, Args), ArgFun = fun(A, Pos) -> @@ -1128,8 +1120,8 @@ get_bif_constr({erlang, Op, 2}, Dst, [Arg1, Arg2] = Args, _State) fun(LocalArg1, LocalArg2, LocalOp) -> fun(Map) -> DstType = lookup_type(Dst, Map), - IsTrue = t_is_atom(true, DstType), - IsFalse = t_is_atom(false, DstType), + IsTrue = t_is_any_atom(true, DstType), + IsFalse = t_is_any_atom(false, DstType), case IsTrue orelse IsFalse of true -> Arg1Type = lookup_type(LocalArg1, Map), @@ -1176,7 +1168,7 @@ get_bif_constr({erlang, Op, 2}, Dst, [Arg1, Arg2] = Args, _State) 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) + bif_return(erlang, Op, 2, TmpArgTypes) end, Args), mk_conj_constraint_list([mk_constraint(Dst, sub, DstVar), mk_constraint(Arg1, sub, Arg1Var), @@ -1218,7 +1210,7 @@ get_bif_constr({erlang, '++', 2}, Dst, [Hd, Tl] = Args, _State) -> 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) + bif_return(erlang, '++', 2, TmpArgTypes) end, Args), Cs = mk_constraints(Args, sub, ArgTypes), mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType), @@ -1240,7 +1232,7 @@ get_bif_constr({erlang, is_function, 1}, Dst, [Arg], 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 + case t_is_any_atom(true, DstType) of true -> ArityType = lookup_type(Arity, Map), case t_number_vals(ArityType) of @@ -1268,7 +1260,7 @@ 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 + case t_is_any_atom(true, lookup_type(Dst, Map)) of true -> t_tuple(); false -> t_any() end @@ -1276,7 +1268,7 @@ get_bif_constr({erlang, is_record, 2}, Dst, [Var, Tag] = Args, _State) -> ArgV = ?mk_fun_var(ArgFun, [Dst]), DstFun = fun(Map) -> TmpArgTypes = lookup_type_list(Args, Map), - erl_bif_types:type(erlang, is_record, 2, TmpArgTypes) + bif_return(erlang, is_record, 2, TmpArgTypes) end, DstV = ?mk_fun_var(DstFun, Args), mk_conj_constraint_list([mk_constraint(Dst, sub, DstV), @@ -1285,10 +1277,9 @@ get_bif_constr({erlang, is_record, 2}, Dst, [Var, Tag] = Args, _State) -> 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 + case t_is_any_atom(true, lookup_type(Dst, Map)) of true -> ArityType = lookup_type(Arity, Map), case t_is_integer(ArityType) of @@ -1304,10 +1295,7 @@ get_bif_constr({erlang, is_record, 3}, Dst, [Var, Tag, Arity] = Args, State) -> [TagVal] -> case lookup_record(Records, TagVal, ArityVal - 1) of {ok, Type} -> - case t_opaque_match_record(Type, AllOpaques) of - [Opaque] -> Opaque; - _ -> Type - end; + Type; error -> GenRecord end; _ -> GenRecord @@ -1323,38 +1311,9 @@ get_bif_constr({erlang, is_record, 3}, Dst, [Var, Tag, Arity] = Args, State) -> 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) + [TmpVar, TmpTag, TmpArity] = lookup_type_list(Args, Map), + TmpArgTypes = [TmpVar,TmpTag,TmpArity], + bif_return(erlang, is_record, 3, TmpArgTypes) end, DstV = ?mk_fun_var(DstFun, Args), mk_conj_constraint_list([mk_constraint(Dst, sub, DstV), @@ -1369,12 +1328,14 @@ get_bif_constr({erlang, 'and', 2}, Dst, [Arg1, Arg2] = Args, _State) -> ArgFun = fun(Var) -> fun(Map) -> DstType = lookup_type(Dst, Map), - case t_is_atom(true, DstType) of + case t_is_any_atom(true, DstType) of true -> True; false -> - case t_is_atom(false, DstType) of + case t_is_any_atom(false, DstType) of true -> - case t_is_atom(true, lookup_type(Var, Map)) of + case + t_is_any_atom(true, lookup_type(Var, Map)) + of true -> False; false -> t_boolean() end; @@ -1386,15 +1347,15 @@ get_bif_constr({erlang, 'and', 2}, Dst, [Arg1, Arg2] = Args, _State) -> end, DstFun = fun(Map) -> Arg1Type = lookup_type(Arg1, Map), - case t_is_atom(false, Arg1Type) of + case t_is_any_atom(false, Arg1Type) of true -> False; false -> Arg2Type = lookup_type(Arg2, Map), - case t_is_atom(false, Arg2Type) of + case t_is_any_atom(false, Arg2Type) of true -> False; false -> - case (t_is_atom(true, Arg1Type) - andalso t_is_atom(true, Arg2Type)) of + case (t_is_any_atom(true, Arg1Type) + andalso t_is_any_atom(true, Arg2Type)) of true -> True; false -> t_boolean() end @@ -1413,12 +1374,14 @@ get_bif_constr({erlang, 'or', 2}, Dst, [Arg1, Arg2] = Args, _State) -> ArgFun = fun(Var) -> fun(Map) -> DstType = lookup_type(Dst, Map), - case t_is_atom(false, DstType) of + case t_is_any_atom(false, DstType) of true -> False; false -> - case t_is_atom(true, DstType) of + case t_is_any_atom(true, DstType) of true -> - case t_is_atom(false, lookup_type(Var, Map)) of + case + t_is_any_atom(false, lookup_type(Var, Map)) + of true -> True; false -> t_boolean() end; @@ -1430,15 +1393,15 @@ get_bif_constr({erlang, 'or', 2}, Dst, [Arg1, Arg2] = Args, _State) -> end, DstFun = fun(Map) -> Arg1Type = lookup_type(Arg1, Map), - case t_is_atom(true, Arg1Type) of + case t_is_any_atom(true, Arg1Type) of true -> True; false -> Arg2Type = lookup_type(Arg2, Map), - case t_is_atom(true, Arg2Type) of + case t_is_any_atom(true, Arg2Type) of true -> True; false -> - case (t_is_atom(false, Arg1Type) - andalso t_is_atom(false, Arg2Type)) of + case (t_is_any_atom(false, Arg1Type) + andalso t_is_any_atom(false, Arg2Type)) of true -> False; false -> t_boolean() end @@ -1465,10 +1428,10 @@ get_bif_constr({erlang, 'not', 1}, Dst, [Arg] = Args, _State) -> Fun = fun(Var) -> fun(Map) -> Type = lookup_type(Var, Map), - case t_is_atom(true, Type) of + case t_is_any_atom(true, Type) of true -> False; false -> - case t_is_atom(false, Type) of + case t_is_any_atom(false, Type) of true -> True; false -> t_boolean() end @@ -1485,10 +1448,10 @@ get_bif_constr({erlang, '=:=', 2}, Dst, [Arg1, Arg2] = Args, _State) -> fun(Map) -> DstType = lookup_type(Dst, Map), OtherVarType = lookup_type(OtherVar, Map), - case t_is_atom(true, DstType) of + case t_is_any_atom(true, DstType) of true -> OtherVarType; false -> - case t_is_atom(false, DstType) of + case t_is_any_atom(false, DstType) of true -> case is_singleton_type(OtherVarType) of true -> t_subtract(lookup_type(Self, Map), OtherVarType); @@ -1518,7 +1481,7 @@ get_bif_constr({erlang, '=:=', 2}, Dst, [Arg1, Arg2] = Args, _State) -> 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) + bif_return(erlang, '==', 2, TmpArgTypes) end, ArgFun = fun(Var, Self) -> @@ -1527,16 +1490,16 @@ get_bif_constr({erlang, '==', 2}, Dst, [Arg1, Arg2] = Args, _State) -> DstType = lookup_type(Dst, Map), case is_singleton_non_number_type(VarType) of true -> - case t_is_atom(true, DstType) of + case t_is_any_atom(true, DstType) of true -> VarType; false -> - case t_is_atom(false, DstType) of + case t_is_any_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 + case t_is_any_atom(true, DstType) of true -> case t_is_number(VarType) of true -> t_number(); @@ -1560,18 +1523,14 @@ get_bif_constr({erlang, '==', 2}, Dst, [Arg1, Arg2] = Args, _State) -> mk_constraint(Arg1, sub, ArgV1), mk_constraint(Arg2, sub, ArgV2)]); get_bif_constr({erlang, element, 2} = _BIF, Dst, Args, - #state{cs = Constrs, opaques = Opaques}) -> + #state{cs = Constrs}) -> 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) + ATs2 = lookup_type_list(Args, Map), + bif_return(erlang, element, 2, ATs2) end, ReturnType = ?mk_fun_var(Fun, Args), ArgTypes = erl_bif_types:arg_types(erlang, element, 2), @@ -1583,22 +1542,14 @@ get_bif_constr({erlang, element, 2} = _BIF, Dst, Args, end, mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType)|NewCs]) end; -get_bif_constr({M, F, A} = _BIF, Dst, Args, State) -> +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) + TmpArgTypes = lookup_type_list(Args, Map), + bif_return(M, F, A, TmpArgTypes) end, Args), case erl_bif_types:is_known(M, F, A) of false -> @@ -1616,12 +1567,12 @@ get_bif_constr({M, F, A} = _BIF, Dst, Args, State) -> end. eval_inv_arith('+', _Pos, Dst, Arg) -> - erl_bif_types:type(erlang, '-', 2, [Dst, Arg]); + bif_return(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]), + TmpRet = bif_return(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 @@ -1630,9 +1581,9 @@ eval_inv_arith('*', _Pos, Dst, Arg) -> end end; eval_inv_arith('-', 1, Dst, Arg) -> - erl_bif_types:type(erlang, '-', 2, [Arg, Dst]); + bif_return(erlang, '-', 2, [Arg, Dst]); eval_inv_arith('-', 2, Dst, Arg) -> - erl_bif_types:type(erlang, '+', 2, [Arg, Dst]). + bif_return(erlang, '+', 2, [Arg, Dst]). range_inc(neg_inf) -> neg_inf; range_inc(pos_inf) -> pos_inf; @@ -1642,33 +1593,20 @@ 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) -> +get_bif_test_constr(Dst, Arg, Type, _State) -> ArgFun = fun(Map) -> DstType = lookup_type(Dst, Map), - case t_is_atom(true, DstType) of + case t_is_any_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; + t_from_term(false); false -> case t_is_subtype(ArgType, Type) of true -> t_from_term(true); @@ -1784,7 +1722,6 @@ minimize_state(#state{ fun_arities = FunArities, self_rec = SelfRec, prop_types = {d, PropTypes}, - opaques = Opaques, solvers = Solvers }) -> Opts = [{read_concurrency, true}], @@ -1798,7 +1735,6 @@ minimize_state(#state{ fun_arities = FunArities, self_rec = SelfRec, prop_types = {e, ETSPropTypes}, - opaques = Opaques, solvers = Solvers }. @@ -1956,8 +1892,7 @@ v2_solve_ref(Fun, Map, State) -> {ok, NewMap}. v2_solve(#constraint{}=C, Map, V2State) -> - State = V2State#v2_state.state, - case solve_one_c(C, Map, State#state.opaques) of + case solve_one_c(C, Map) of error -> report_failed_constraint(C, Map), {error, V2State}; @@ -2031,7 +1966,7 @@ v2_solve_self_recursive(Cs, Map, Id, RecType0, V2State0) -> {ok, NewMap, V2State, U} -> pp_map("recursive finished", NewMap), NewRecType = unsafe_lookup_type(Id, NewMap), - case t_is_equal(NewRecType, RecType0) of + case is_equal(NewRecType, RecType0) of true -> {NewMap2, U1} = enter_var_type(RecVar, NewRecType, NewMap), {ok, NewMap2, V2State, lists:umerge(U, U1)}; @@ -2397,7 +2332,7 @@ solve_self_recursive(Cs, Map, MapDict, Id, RecType0, State) -> {ok, NewMapDict, NewMap} -> pp_map("NewMap", NewMap), NewRecType = unsafe_lookup_type(Id, NewMap), - case t_is_equal(NewRecType, RecType0) of + case is_equal(NewRecType, RecType0) of true -> {ok, NewMapDict, enter_type(RecVar, NewRecType, NewMap)}; false -> @@ -2447,7 +2382,7 @@ solve_cs([#constraint_list{} = C|Tail], Map, MapDict, State) -> {error, _NewMapDict} = Error -> Error end; solve_cs([#constraint{} = C|Tail], Map, MapDict, State) -> - case solve_one_c(C, Map, State#state.opaques) of + case solve_one_c(C, Map) of error -> report_failed_constraint(C, Map), {error, MapDict}; @@ -2457,10 +2392,10 @@ solve_cs([#constraint{} = C|Tail], Map, MapDict, State) -> solve_cs([], Map, MapDict, _State) -> {ok, MapDict, Map}. -solve_one_c(#constraint{lhs = Lhs, rhs = Rhs, op = Op}, Map, Opaques) -> +solve_one_c(#constraint{lhs = Lhs, rhs = Rhs, op = Op}, Map) -> LhsType = lookup_type(Lhs, Map), RhsType = lookup_type(Rhs, Map), - Inf = t_inf(LhsType, RhsType, opaque), + Inf = t_inf(LhsType, RhsType), ?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)]), @@ -2468,12 +2403,12 @@ solve_one_c(#constraint{lhs = Lhs, rhs = Rhs, op = Op}, Map, Opaques) -> true -> error; false -> case Op of - sub -> solve_subtype(Lhs, Inf, Map, Opaques); + sub -> solve_subtype(Lhs, Inf, Map); eq -> - case solve_subtype(Lhs, Inf, Map, Opaques) of + case solve_subtype(Lhs, Inf, Map) of error -> error; {ok, {Map1, U1}} -> - case solve_subtype(Rhs, Inf, Map1, Opaques) of + case solve_subtype(Rhs, Inf, Map1) of error -> error; {ok, {Map2, U2}} -> {ok, {Map2, lists:umerge(U1, U2)}} end @@ -2481,7 +2416,7 @@ solve_one_c(#constraint{lhs = Lhs, rhs = Rhs, op = Op}, Map, Opaques) -> end end. -solve_subtype(Type, Inf, Map, Opaques) -> +solve_subtype(Type, Inf, Map) -> %% case cerl:is_literal(Type) of %% true -> %% case t_is_subtype(t_from_term(cerl:concrete(Type)), Inf) of @@ -2489,7 +2424,7 @@ solve_subtype(Type, Inf, Map, Opaques) -> %% false -> error %% end; %% false -> - try t_unify(Type, Inf, Opaques) of + try t_unify(Type, Inf) of {_, List} -> {ok, enter_type_list(List, Map)} catch throw:{mismatch, _T1, _T2} -> @@ -2540,7 +2475,7 @@ join_one_key(Key, [Map|Maps], Type) -> true -> Type; false -> NewType = lookup_type(Key, Map), - case t_is_equal(NewType, Type) of + case is_equal(NewType, Type) of true -> join_one_key(Key, Maps, Type); false -> join_one_key(Key, Maps, t_sup(NewType, Type)) end @@ -2555,7 +2490,7 @@ maps_are_equal(Map1, Map2, Deps) -> 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 + case 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)]), @@ -2587,14 +2522,20 @@ prune_keys(Map1, Map2, Deps) -> 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 + %% Keep any() in the map if it is opaque: + case is_equal(Val, t_any()) of true -> erase_type(Key, Map); false -> LimitedVal = t_limit(Val, ?INTERNAL_TYPE_LIMIT), + [?debug("LimitedVal ~s\n", [format_type(LimitedVal)]) || + not is_equal(LimitedVal, Val)], case dict:find(Key, Map) of - {ok, LimitedVal} -> Map; - {ok, _} -> map_store(Key, LimitedVal, Map); + {ok, Value} -> + case is_equal(Value, LimitedVal) of + true -> Map; + false -> map_store(Key, LimitedVal, Map) + end; error -> map_store(Key, LimitedVal, Map) end end; @@ -2681,7 +2622,10 @@ 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)). + is_equal(lookup_type(Key, Map1), lookup_type(Key, Map2)). + +is_equal(Type1, Type2) -> + t_is_equal(Type1, Type2). pp_map(_S, _Map) -> ?debug("\t~s: ~p\n", @@ -2716,11 +2660,6 @@ new_state(SCC0, NextLabel, CallGraph, Plt, PropTypes, 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}. @@ -2760,7 +2699,8 @@ state__lookup_undef_var(Tree, #state{callgraph = CG, plt = Plt}) -> {ok, MFA} -> case dialyzer_plt:lookup(Plt, MFA) of none -> error; - {value, {RetType, ArgTypes}} -> {ok, t_fun(ArgTypes, RetType)} + {value, {RetType, ArgTypes}} -> + {ok, t_fun(ArgTypes, RetType)} end end. @@ -2897,7 +2837,7 @@ state__get_cs(Var, #state{cmap = {d, Dict}}) -> dict:fetch(Var, Dict). state__is_self_rec(Fun, #state{self_rec = SelfRec}) -> - Fun =:= SelfRec. + not (SelfRec =:= 'false') andalso is_equal(Fun, SelfRec). state__store_funs(Vars0, Funs0, #state{fun_map = Map} = State) -> debug_make_name_map(Vars0, Funs0), @@ -2923,7 +2863,9 @@ state__finalize(State) -> %% %% ============================================================================ --spec mk_constraint(erl_types:erl_type(), constr_op(), fvar_or_type()) -> #constraint{}. +-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 @@ -2934,9 +2876,9 @@ mk_constraint(Lhs, Op, Rhs) -> case Deps =:= [] of true -> %% This constraint is constant. Solve it immediately. - case solve_one_c(C, map_new(), []) of + case solve_one_c(C, map_new()) of error -> throw(error); - _ -> + _R -> %% This is always true, keep it anyway for logistic reasons C end; @@ -2944,10 +2886,13 @@ mk_constraint(Lhs, Op, Rhs) -> C end; true -> - C = mk_constraint_1(t_any(), Op, t_any()), - C#constraint{deps = []} + mk_constraint_any(Op) end. +mk_constraint_any(Op) -> + C = mk_constraint_1(t_any(), Op, t_any()), + C#constraint{deps = []}. + %% 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(). @@ -3002,7 +2947,8 @@ 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_constraint(Lhs, Op, Rhs) | + mk_constraints(LhsTail, Op, RhsTail)]; mk_constraints([], _Op, []) -> []. @@ -3017,7 +2963,7 @@ mk_constraint_list(Type, List) -> Deps = calculate_deps(List2), case Deps =:= [] of true -> #constraint_list{type = conj, - list = [mk_constraint(t_any(), eq, t_any())], + list = [mk_constraint_any(eq)], deps = []}; false -> #constraint_list{type = Type, list = List2, deps = Deps} end. @@ -3236,6 +3182,9 @@ calculate_masks([], _I, L) -> %% %% ============================================================================ +bif_return(M, F, A, Xs) -> + erl_bif_types:type(M, F, A, Xs). + is_singleton_non_number_type(Type) -> case t_is_number(Type) of true -> false; @@ -3265,7 +3214,7 @@ is_singleton_type(Type) -> find_element(Args, Cs) -> [Pos, Tuple] = Args, - case erl_types:t_is_number(Pos) of + case t_is_number(Pos) of true -> case erl_types:t_number_vals(Pos) of 'unknown' -> 'unknown'; @@ -3301,8 +3250,10 @@ 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]])}; + RecType = + t_tuple([t_from_term(Tag)| + [FieldType || {_FieldName, FieldType} <- Fields]]), + {ok, RecType}; error -> error end. |