Add an undocumented option [--solver [v1 | v2]]

The original implementation of the type signature solver is called 'v1'
and the newly introduced alternative implementation is called 'v2'.

It is possible to run just the one of the solvers (in case there is a
bug in for instance the v2 implementation) or both solvers
("--solver v1 --solver v2"). In the latter case an error is thrown if
the outcome differ.

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}.