aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/dialyzer/src/dialyzer.hrl9
-rw-r--r--lib/dialyzer/src/dialyzer_analysis_callgraph.erl13
-rw-r--r--lib/dialyzer/src/dialyzer_cl.erl5
-rw-r--r--lib/dialyzer/src/dialyzer_cl_parse.erl9
-rw-r--r--lib/dialyzer/src/dialyzer_options.erl14
-rw-r--r--lib/dialyzer/src/dialyzer_succ_typings.erl48
-rw-r--r--lib/dialyzer/src/dialyzer_typesig.erl30
7 files changed, 82 insertions, 46 deletions
diff --git a/lib/dialyzer/src/dialyzer.hrl b/lib/dialyzer/src/dialyzer.hrl
index 1b999a7b99..105a174e31 100644
--- a/lib/dialyzer/src/dialyzer.hrl
+++ b/lib/dialyzer/src/dialyzer.hrl
@@ -2,7 +2,7 @@
%%%
%%% %CopyrightBegin%
%%%
-%%% Copyright Ericsson AB 2006-2011. All Rights Reserved.
+%%% Copyright Ericsson AB 2006-2012. 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
@@ -111,6 +111,7 @@
-type rep_mode() :: 'quiet' | 'normal' | 'verbose'.
-type start_from() :: 'byte_code' | 'src_code'.
-type mfa_or_funlbl() :: label() | mfa().
+-type solver() :: 'v1' | 'v2'.
%%--------------------------------------------------------------------
%% Record declarations used by various files
@@ -129,7 +130,8 @@
behaviours_chk = false :: boolean(),
timing = false :: boolean() | 'debug',
timing_server :: dialyzer_timing:timing_server(),
- callgraph_file = "" :: file:filename()}).
+ callgraph_file = "" :: file:filename(),
+ solvers :: [solver()]}).
-record(options, {files = [] :: [file:filename()],
files_rec = [] :: [file:filename()],
@@ -149,7 +151,8 @@
output_format = formatted :: format(),
filename_opt = basename :: fopt(),
callgraph_file = "" :: file:filename(),
- check_plt = true :: boolean()}).
+ check_plt = true :: boolean(),
+ solvers = [] :: [solver()]}).
-record(contract, {contracts = [] :: [contract_pair()],
args = [] :: [erl_types:erl_type()],
diff --git a/lib/dialyzer/src/dialyzer_analysis_callgraph.erl b/lib/dialyzer/src/dialyzer_analysis_callgraph.erl
index 3bbde12481..496d317f8a 100644
--- a/lib/dialyzer/src/dialyzer_analysis_callgraph.erl
+++ b/lib/dialyzer/src/dialyzer_analysis_callgraph.erl
@@ -53,7 +53,8 @@
plt :: dialyzer_plt:plt(),
start_from = byte_code :: start_from(),
use_contracts = true :: boolean(),
- timing_server :: dialyzer_timing:timing_server()
+ timing_server :: dialyzer_timing:timing_server(),
+ solvers :: [solver()]
}).
-record(server_state, {parent :: pid(), legal_warnings :: [dial_warn_tag()]}).
@@ -136,7 +137,8 @@ analysis_start(Parent, Analysis) ->
parent = Parent,
start_from = Analysis#analysis.start_from,
use_contracts = Analysis#analysis.use_contracts,
- timing_server = Analysis#analysis.timing_server
+ timing_server = Analysis#analysis.timing_server,
+ solvers = Analysis#analysis.solvers
},
Files = ordsets:from_list(Analysis#analysis.files),
{Callgraph, NoWarn, TmpCServer0} = compile_and_store(Files, State),
@@ -192,20 +194,21 @@ analysis_start(Parent, Analysis) ->
analyze_callgraph(Callgraph, #analysis_state{codeserver = Codeserver,
doc_plt = DocPlt,
timing_server = TimingServer,
- parent = Parent} = State) ->
+ parent = Parent,
+ solvers = Solvers} = State) ->
Plt = dialyzer_plt:insert_callbacks(State#analysis_state.plt, Codeserver),
{NewPlt, NewDocPlt} =
case State#analysis_state.analysis_type of
plt_build ->
NewPlt0 =
dialyzer_succ_typings:analyze_callgraph(Callgraph, Plt, Codeserver,
- TimingServer, Parent),
+ TimingServer, Solvers, Parent),
{NewPlt0, DocPlt};
succ_typings ->
NoWarn = State#analysis_state.no_warn_unused,
{Warnings, NewPlt0, NewDocPlt0} =
dialyzer_succ_typings:get_warnings(Callgraph, Plt, DocPlt, Codeserver,
- NoWarn, TimingServer, Parent),
+ NoWarn, TimingServer, Solvers, Parent),
send_warnings(State#analysis_state.parent, Warnings),
{NewPlt0, NewDocPlt0}
end,
diff --git a/lib/dialyzer/src/dialyzer_cl.erl b/lib/dialyzer/src/dialyzer_cl.erl
index 5d253e77fa..6732d96b98 100644
--- a/lib/dialyzer/src/dialyzer_cl.erl
+++ b/lib/dialyzer/src/dialyzer_cl.erl
@@ -2,7 +2,7 @@
%%-------------------------------------------------------------------
%% %CopyrightBegin%
%%
-%% Copyright Ericsson AB 2006-2011. All Rights Reserved.
+%% Copyright Ericsson AB 2006-2012. 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
@@ -398,7 +398,8 @@ do_analysis(Files, Options, Plt, PltInfo) ->
timing = Options#options.timing,
plt = Plt,
use_contracts = Options#options.use_contracts,
- callgraph_file = Options#options.callgraph_file},
+ callgraph_file = Options#options.callgraph_file,
+ solvers = Options#options.solvers},
State3 = start_analysis(State2, InitAnalysis),
{T1, _} = statistics(wall_clock),
Return = cl_loop(State3),
diff --git a/lib/dialyzer/src/dialyzer_cl_parse.erl b/lib/dialyzer/src/dialyzer_cl_parse.erl
index 205b97ccf9..2ea3d3af5a 100644
--- a/lib/dialyzer/src/dialyzer_cl_parse.erl
+++ b/lib/dialyzer/src/dialyzer_cl_parse.erl
@@ -2,7 +2,7 @@
%%-----------------------------------------------------------------------
%% %CopyrightBegin%
%%
-%% Copyright Ericsson AB 2006-2011. All Rights Reserved.
+%% Copyright Ericsson AB 2006-2012. 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
@@ -198,6 +198,9 @@ cl(["--gui"|T]) ->
cl(["--wx"|T]) ->
put(dialyzer_options_mode, {gui, wx}),
cl(T);
+cl(["--solver",Solver|T]) -> % not documented
+ append_var(dialyzer_solvers, [list_to_atom(Solver)]),
+ cl(T);
cl([H|_] = L) ->
case filelib:is_file(H) orelse filelib:is_dir(H) of
true ->
@@ -258,6 +261,7 @@ init() ->
put(dialyzer_filename_opt, basename),
put(dialyzer_options_check_plt, DefaultOpts#options.check_plt),
put(dialyzer_timing, DefaultOpts#options.timing),
+ put(dialyzer_solvers, DefaultOpts#options.solvers),
ok.
append_defines([Def, Val]) ->
@@ -311,7 +315,8 @@ common_options() ->
{report_mode, get(dialyzer_options_report_mode)},
{use_spec, get(dialyzer_options_use_contracts)},
{warnings, get(dialyzer_warnings)},
- {check_plt, get(dialyzer_options_check_plt)}].
+ {check_plt, get(dialyzer_options_check_plt)},
+ {solvers, get(dialyzer_solvers)}].
%%-----------------------------------------------------------------------
diff --git a/lib/dialyzer/src/dialyzer_options.erl b/lib/dialyzer/src/dialyzer_options.erl
index a1e316d6cc..06672e595f 100644
--- a/lib/dialyzer/src/dialyzer_options.erl
+++ b/lib/dialyzer/src/dialyzer_options.erl
@@ -2,7 +2,7 @@
%%-----------------------------------------------------------------------
%% %CopyrightBegin%
%%
-%% Copyright Ericsson AB 2006-2011. All Rights Reserved.
+%% Copyright Ericsson AB 2006-2012. 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
@@ -196,6 +196,9 @@ build_options([{OptionName, Value} = Term|Rest], Options) ->
build_options(Rest, Options#options{callgraph_file = Value});
timing ->
build_options(Rest, Options#options{timing = Value});
+ solvers ->
+ assert_solvers(Value),
+ build_options(Rest, Options#options{solvers = Value});
_ ->
bad_option("Unknown dialyzer command line option", Term)
end;
@@ -257,6 +260,15 @@ is_plt_mode(plt_remove) -> true;
is_plt_mode(plt_check) -> true;
is_plt_mode(succ_typings) -> false.
+assert_solvers([]) ->
+ ok;
+assert_solvers([v1|Terms]) ->
+ assert_solvers(Terms);
+assert_solvers([v2|Terms]) ->
+ assert_solvers(Terms);
+assert_solvers([Term|_]) ->
+ bad_option("Illegal value for solver", Term).
+
-spec build_warnings([atom()], [dial_warning()]) -> [dial_warning()].
build_warnings([Opt|Opts], Warnings) ->
diff --git a/lib/dialyzer/src/dialyzer_succ_typings.erl b/lib/dialyzer/src/dialyzer_succ_typings.erl
index 9ca5a66dab..84379642bf 100644
--- a/lib/dialyzer/src/dialyzer_succ_typings.erl
+++ b/lib/dialyzer/src/dialyzer_succ_typings.erl
@@ -28,8 +28,8 @@
-module(dialyzer_succ_typings).
-export([analyze_callgraph/3,
- analyze_callgraph/5,
- get_warnings/7
+ analyze_callgraph/6,
+ get_warnings/8
]).
-export([
@@ -75,6 +75,7 @@
no_warn_unused :: set(),
parent = none :: parent(),
timing_server :: dialyzer_timing:timing_server(),
+ solvers :: [solver()],
plt :: dialyzer_plt:plt()}).
%%--------------------------------------------------------------------
@@ -84,28 +85,29 @@
dialyzer_plt:plt().
analyze_callgraph(Callgraph, Plt, Codeserver) ->
- analyze_callgraph(Callgraph, Plt, Codeserver, none, none).
+ analyze_callgraph(Callgraph, Plt, Codeserver, none, [], none).
-spec analyze_callgraph(dialyzer_callgraph:callgraph(), dialyzer_plt:plt(),
dialyzer_codeserver:codeserver(),
- dialyzer_timing:timing_server(), parent()) ->
+ dialyzer_timing:timing_server(),
+ [solver()], parent()) ->
dialyzer_plt:plt().
-analyze_callgraph(Callgraph, Plt, Codeserver, TimingServer, Parent) ->
+analyze_callgraph(Callgraph, Plt, Codeserver, TimingServer, Solvers, Parent) ->
NewState =
init_state_and_get_success_typings(Callgraph, Plt, Codeserver,
- TimingServer, Parent),
+ TimingServer, Solvers, Parent),
dialyzer_plt:restore_full_plt(NewState#st.plt, Plt).
%%--------------------------------------------------------------------
init_state_and_get_success_typings(Callgraph, Plt, Codeserver,
- TimingServer, Parent) ->
+ TimingServer, Solvers, Parent) ->
{SCCs, Callgraph1} =
?timing(TimingServer, "order", dialyzer_callgraph:finalize(Callgraph)),
State = #st{callgraph = Callgraph1, plt = dialyzer_plt:get_mini_plt(Plt),
codeserver = Codeserver, parent = Parent,
- timing_server = TimingServer},
+ timing_server = TimingServer, solvers = Solvers},
get_refined_success_typings(SCCs, State).
get_refined_success_typings(SCCs, #st{callgraph = Callgraph,
@@ -136,14 +138,14 @@ get_refined_success_typings(SCCs, #st{callgraph = Callgraph,
-type doc_plt() :: 'undefined' | dialyzer_plt:plt().
-spec get_warnings(dialyzer_callgraph:callgraph(), dialyzer_plt:plt(),
doc_plt(), dialyzer_codeserver:codeserver(), set(),
- dialyzer_timing:timing_server(), pid()) ->
+ dialyzer_timing:timing_server(), [solver()], pid()) ->
{[dial_warning()], dialyzer_plt:plt(), doc_plt()}.
get_warnings(Callgraph, Plt, DocPlt, Codeserver,
- NoWarnUnused, TimingServer, Parent) ->
+ NoWarnUnused, TimingServer, Solvers, Parent) ->
InitState =
init_state_and_get_success_typings(Callgraph, Plt, Codeserver,
- TimingServer, Parent),
+ TimingServer, Solvers, Parent),
NewState = InitState#st{no_warn_unused = NoWarnUnused},
Mods = dialyzer_callgraph:modules(NewState#st.callgraph),
MiniPlt = NewState#st.plt,
@@ -222,9 +224,10 @@ postprocess_dataflow_warns([{?WARN_CONTRACT_RANGE, {CallF, CallL}, Msg}|Rest],
refine_succ_typings(Modules, #st{codeserver = Codeserver,
callgraph = Callgraph,
plt = Plt,
- timing_server = Timing} = State) ->
+ timing_server = Timing,
+ solvers = Solvers} = State) ->
?debug("Module postorder: ~p\n", [Modules]),
- Init = {Codeserver, Callgraph, Plt},
+ Init = {Codeserver, Callgraph, Plt, Solvers},
NotFixpoint =
?timing(Timing, "refine",
dialyzer_coordinator:parallel_job(dataflow, Modules, Init, Timing)),
@@ -236,22 +239,22 @@ refine_succ_typings(Modules, #st{codeserver = Codeserver,
-spec find_depends_on(scc() | module(), fixpoint_init_data()) -> [scc()].
-find_depends_on(SCC, {_Codeserver, Callgraph, _Plt}) ->
+find_depends_on(SCC, {_Codeserver, Callgraph, _Plt, _Solvers}) ->
dialyzer_callgraph:get_depends_on(SCC, Callgraph).
-spec find_required_by(scc() | module(), fixpoint_init_data()) -> [scc()].
-find_required_by(SCC, {_Codeserver, Callgraph, _Plt}) ->
+find_required_by(SCC, {_Codeserver, Callgraph, _Plt, _Solvers}) ->
dialyzer_callgraph:get_required_by(SCC, Callgraph).
-spec lookup_names([label()], fixpoint_init_data()) -> [mfa_or_funlbl()].
-lookup_names(Labels, {_Codeserver, Callgraph, _Plt}) ->
+lookup_names(Labels, {_Codeserver, Callgraph, _Plt, _Solvers}) ->
[lookup_name(F, Callgraph) || F <- Labels].
-spec refine_one_module(module(), dataflow_init_data()) -> [label()]. % ordset
-refine_one_module(M, {CodeServer, Callgraph, Plt}) ->
+refine_one_module(M, {CodeServer, Callgraph, Plt, _Solvers}) ->
ModCode = dialyzer_codeserver:lookup_mod_code(M, CodeServer),
AllFuns = collect_fun_info([ModCode]),
Records = dialyzer_codeserver:lookup_mod_records(M, CodeServer),
@@ -322,8 +325,9 @@ compare_types_1([], [], _Strict, NotFixpoint) ->
end.
find_succ_typings(SCCs, #st{codeserver = Codeserver, callgraph = Callgraph,
- plt = Plt, timing_server = Timing} = State) ->
- Init = {Codeserver, Callgraph, Plt},
+ plt = Plt, timing_server = Timing,
+ solvers = Solvers} = State) ->
+ Init = {Codeserver, Callgraph, Plt, Solvers},
NotFixpoint =
?timing(Timing, "typesig",
dialyzer_coordinator:parallel_job(typesig, SCCs, Init, Timing)),
@@ -335,7 +339,7 @@ find_succ_typings(SCCs, #st{codeserver = Codeserver, callgraph = Callgraph,
-spec find_succ_types_for_scc(scc(), typesig_init_data()) -> [mfa_or_funlbl()].
-find_succ_types_for_scc(SCC, {Codeserver, Callgraph, Plt}) ->
+find_succ_types_for_scc(SCC, {Codeserver, Callgraph, Plt, Solvers}) ->
SCC_Info = [{MFA,
dialyzer_codeserver:lookup_mfa_code(MFA, Codeserver),
dialyzer_codeserver:lookup_mod_records(M, Codeserver)}
@@ -348,8 +352,8 @@ find_succ_types_for_scc(SCC, {Codeserver, Callgraph, Plt}) ->
AllFuns = collect_fun_info([Fun || {_MFA, {_Var, Fun}, _Rec} <- SCC_Info]),
PropTypes = get_fun_types_from_plt(AllFuns, Callgraph, Plt),
%% Assume that the PLT contains the current propagated types
- FunTypes =
- dialyzer_typesig:analyze_scc(SCC_Info, Label, Callgraph, Plt, PropTypes),
+ FunTypes = dialyzer_typesig:analyze_scc(SCC_Info, Label, Callgraph,
+ Plt, PropTypes, Solvers),
AllFunSet = sets:from_list([X || {X, _} <- AllFuns]),
FilteredFunTypes =
dict:filter(fun(X, _) -> sets:is_element(X, AllFunSet) end, FunTypes),
diff --git a/lib/dialyzer/src/dialyzer_typesig.erl b/lib/dialyzer/src/dialyzer_typesig.erl
index 03ddeca229..0df003a035 100644
--- a/lib/dialyzer/src/dialyzer_typesig.erl
+++ b/lib/dialyzer/src/dialyzer_typesig.erl
@@ -28,7 +28,7 @@
-module(dialyzer_typesig).
--export([analyze_scc/5]).
+-export([analyze_scc/6]).
-export([get_safe_underapprox/2]).
-import(erl_types,
@@ -112,7 +112,7 @@
opaques = [] :: [erl_types:erl_type()],
scc = [] :: [type_var()],
mfas :: [tuple()],
- solvers = [v2] :: ['v1' | 'v2']
+ solvers = [] :: [solver()]
}).
%%-----------------------------------------------------------------------------
@@ -146,7 +146,7 @@
%%-----------------------------------------------------------------------------
%% Analysis of strongly connected components.
%%
-%% analyze_scc(SCC, NextLabel, CallGraph, PLT, PropTypes) -> FunTypes
+%% analyze_scc(SCC, NextLabel, CallGraph, PLT, PropTypes, Solvers) -> FunTypes
%%
%% SCC - [{MFA, Def, Records}]
%% where Def = {Var, Fun} as in the Core Erlang module definitions.
@@ -159,16 +159,17 @@
%% about functions that can be called by this SCC.
%% PropTypes - A dictionary.
%% FunTypes - A dictionary.
+%% Solvers - User specified solvers.
%%-----------------------------------------------------------------------------
-spec analyze_scc(typesig_scc(), label(),
dialyzer_callgraph:callgraph(),
- dialyzer_plt:plt(), dict()) -> dict().
+ dialyzer_plt:plt(), dict(), [solver()]) -> dict().
-analyze_scc(SCC, NextLabel, CallGraph, Plt, PropTypes) ->
- %% FIXME. Solvers as an option and argument. Save in 'state.
+analyze_scc(SCC, NextLabel, CallGraph, Plt, PropTypes, Solvers0) ->
+ Solvers = solvers(Solvers0),
assert_format_of_scc(SCC),
- State1 = new_state(SCC, NextLabel, CallGraph, Plt, PropTypes),
+ State1 = new_state(SCC, NextLabel, CallGraph, Plt, PropTypes, Solvers),
DefSet = add_def_list([Var || {_MFA, {Var, _Fun}, _Rec} <- SCC], sets:new()),
State2 = traverse_scc(SCC, DefSet, State1),
State3 = state__finalize(State2),
@@ -182,6 +183,9 @@ assert_format_of_scc([{_MFA, {_Var, _Fun}, _Records}|Left]) ->
assert_format_of_scc([]) ->
ok.
+solvers([]) -> [v2];
+solvers(Solvers) -> Solvers.
+
%% ============================================================================
%%
%% Gets the constraints by traversing the code.
@@ -1764,7 +1768,8 @@ minimize_state(#state{
fun_arities = FunArities,
self_rec = SelfRec,
prop_types = {d, PropTypes},
- opaques = Opaques
+ opaques = Opaques,
+ solvers = Solvers
}) ->
ETSCMap = ets:new(cmap,[{read_concurrency, true}]),
ETSPropTypes = ets:new(prop_types,[{read_concurrency, true}]),
@@ -1776,7 +1781,8 @@ minimize_state(#state{
fun_arities = FunArities,
self_rec = SelfRec,
prop_types = {e, ETSPropTypes},
- opaques = Opaques
+ opaques = Opaques,
+ solvers = Solvers
}.
dispose_state(#state{cmap = {e, ETSCMap},
@@ -1901,6 +1907,8 @@ check_solutions([{S1,Map1,_Time1}|Maps], Fun, S, Map) ->
?debug("Constraint solvers do not agree on ~w\n", [Fun]),
pp_map(atom_to_list(S), Map),
pp_map(atom_to_list(S1), Map1),
+ io:format("A bug was found. Please report it, and use the option "
+ "`--solver v1' until the bug has been fixed.\n"),
throw(error)
end.
@@ -2680,7 +2688,7 @@ pp_map(_S, _Map) ->
%%
%% ============================================================================
-new_state(SCC0, NextLabel, CallGraph, Plt, PropTypes) ->
+new_state(SCC0, NextLabel, CallGraph, Plt, PropTypes, Solvers) ->
List = [{MFA, Var} || {MFA, {Var, _Fun}, _Rec} <- SCC0],
NameMap = dict:from_list(List),
MFAs = [MFA || {MFA, _Var} <- List],
@@ -2697,7 +2705,7 @@ new_state(SCC0, NextLabel, CallGraph, Plt, PropTypes) ->
end,
#state{callgraph = CallGraph, name_map = NameMap, next_label = NextLabel,
prop_types = {d, PropTypes}, plt = Plt, scc = ordsets:from_list(SCC),
- mfas = MFAs, self_rec = SelfRec}.
+ mfas = MFAs, self_rec = SelfRec, solvers = Solvers}.
state__set_rec_dict(State, RecDict) ->
State#state{records = RecDict}.
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 23:50:43 +0000