From c02a4682b51d2baa32182c6ed7f4adfb4644f07f Mon Sep 17 00:00:00 2001
From: Hans Bolinder <hasse@erlang.org>
Date: Tue, 12 Jun 2012 13:53:55 +0200
Subject: Add an alternative implmentation of the typesignature solver

An alternative implementation of the solver in dialyzer_typesig has
been introduced. It is faster than the original implementation.

Note: there is code for "loop detection". Where a loop occurs, the
evaluation is stopped and the current solution returned. This
behaviour is consistent with how the original implementation works.

There are a few known cases where the loop detection kicks in. They
are due to bugs which will hopefully be fixed in a near future.
---
 lib/dialyzer/src/dialyzer_typesig.erl | 568 +++++++++++++++++++++++++++++++---
 1 file changed, 527 insertions(+), 41 deletions(-)

(limited to 'lib/dialyzer')

diff --git a/lib/dialyzer/src/dialyzer_typesig.erl b/lib/dialyzer/src/dialyzer_typesig.erl
index e997eedf76..03ddeca229 100644
--- a/lib/dialyzer/src/dialyzer_typesig.erl
+++ b/lib/dialyzer/src/dialyzer_typesig.erl
@@ -78,6 +78,8 @@
 -record(constraint_list, {type :: 'conj' | 'disj',
 			  list :: [constr()],
 			  deps :: [dep()],
+                          masks :: [{dep(),[non_neg_integer()]}] |
+                                   {'d',dict()},
 			  id   :: {'list', dep()}}).
 
 -type constraint_list() :: #constraint_list{}.
@@ -109,7 +111,8 @@
 		records     = dict:new()        :: dict(),
 		opaques     = []                :: [erl_types:erl_type()],
 		scc         = []                :: [type_var()],
-		mfas                            :: [tuple()]
+		mfas                            :: [tuple()],
+                solvers     = [v2]              :: ['v1' | 'v2']
 	       }).
 
 %%-----------------------------------------------------------------------------
@@ -121,8 +124,10 @@
 %%-define(DEBUG_CONSTRAINTS, true).
 -ifdef(DEBUG).
 -define(DEBUG_NAME_MAP, true).
+-define(DEBUG_LOOP_DETECTION, true).
 -endif.
 %%-define(DEBUG_NAME_MAP, true).
+%%-define(DEBUG_LOOP_DETECTION, true).
 
 -ifdef(DEBUG).
 -define(debug(__String, __Args), io:format(__String, __Args)).
@@ -161,6 +166,7 @@
 		  dialyzer_plt:plt(), dict()) -> dict().
 
 analyze_scc(SCC, NextLabel, CallGraph, Plt, PropTypes) ->
+  %% FIXME. Solvers as an option and argument. Save in 'state.
   assert_format_of_scc(SCC),
   State1 = new_state(SCC, NextLabel, CallGraph, Plt, PropTypes),
   DefSet = add_def_list([Var || {_MFA, {Var, _Fun}, _Rec} <- SCC], sets:new()),
@@ -1663,7 +1669,7 @@ get_bif_test_constr(Dst, Arg, Type, State) ->
 solve([Fun], State) ->
   ?debug("============ Analyzing Fun: ~w ===========\n",
 	 [debug_lookup_name(Fun)]),
-  solve_fun(Fun, dict:new(), State);
+  solve_fun(Fun, map_new(), State);
 solve([_|_] = SCC, State) ->
   ?debug("============ Analyzing SCC: ~w ===========\n",
 	 [[debug_lookup_name(F) || F <- SCC]]),
@@ -1672,14 +1678,14 @@ solve([_|_] = SCC, State) ->
       false -> {false, State};
       SplitSCC -> {SplitSCC, minimize_state(State)}
     end,
-  solve_scc(SCC, Parallel, dict:new(), NewState, false).
+  solve_scc(SCC, Parallel, map_new(), NewState, false).
 
 solve_fun(Fun, FunMap, State) ->
   Cs = state__get_cs(Fun, State),
   Deps = get_deps(Cs),
   Ref = mk_constraint_ref(Fun, Deps),
   %% Note that functions are always considered to succeed.
-  {ok, _MapDict, NewMap} = solve_ref_or_list(Ref, FunMap, dict:new(), State),
+  NewMap = solve(Fun, Ref, FunMap, State),
   NewType = lookup_type(Fun, NewMap),
   NewFunMap1 = case state__get_rec_var(Fun, State) of
 		 error -> FunMap;
@@ -1694,7 +1700,7 @@ solve_scc(SCC, Parallel, Map, State, TryingUnit) ->
   Types = unsafe_lookup_type_list(Funs, Map),
   RecTypes = [t_limit(Type, ?TYPE_LIMIT) || Type <- Types],
   CleanMap = lists:foldl(fun(Fun, AccFunMap) ->
-			     dict:erase(t_var_name(Fun), AccFunMap)
+			     erase_type(t_var_name(Fun), AccFunMap)
 			 end, Map, SCC),
   Map1 = enter_type_lists(Vars, RecTypes, CleanMap),
   ?debug("Checking SCC: ~w\n", [[debug_lookup_name(F) || F <- SCC]]),
@@ -1842,7 +1848,7 @@ scc_fold_fun(F, FunMap, State) ->
   Deps = get_deps(state__get_cs(F, State)),
   Cs = mk_constraint_ref(F, Deps),
   %% Note that functions are always considered to succeed.
-  {ok, _NewMapDict, Map} = solve_ref_or_list(Cs, FunMap, dict:new(), State),
+  Map = solve(F, Cs, FunMap, State),
   NewType0 = unsafe_lookup_type(F, Map),
   NewType = t_limit(NewType0, ?TYPE_LIMIT),
   NewFunMap = case state__get_rec_var(F, State) of
@@ -1855,15 +1861,438 @@ scc_fold_fun(F, FunMap, State) ->
 						  format_type(NewType)]),
   NewFunMap.
 
+solve(Fun, Cs, FunMap, State) ->
+  Solvers = State#state.solvers,
+  R = [solver(S, solve_fun(S, Fun, Cs, FunMap, State)) || S <- Solvers],
+  check_solutions(R, Fun, no_solver, no_map).
+
+solver(Solver, SolveFun) ->
+  ?debug("Start solver ~w\n", [Solver]),
+  try timer:tc(SolveFun) of
+    {Time, {ok, Map}} ->
+      ?debug("End solver ~w (~w microsecs)\n", [Solver, Time]),
+      {Solver, Map, Time};
+    {_, _R} ->
+      ?debug("Solver ~w returned unexpected result:\n  ~P\n",
+             [Solver, _R, 60]),
+      throw(error)
+  catch E:R ->
+      io:format("Solver ~w failed: ~w:~p\n ~p\n",
+                [Solver, E, R, erlang:get_stacktrace()]),
+      throw(error)
+  end.
+
+solve_fun(v1, _Fun, Cs, FunMap, State) ->
+  fun() ->
+      {ok, _MapDict, NewMap} = solve_ref_or_list(Cs, FunMap, dict:new(), State),
+      {ok, NewMap}
+  end;
+solve_fun(v2, Fun, _Cs, FunMap, State) ->
+  fun() -> v2_solve_ref(Fun, FunMap, State) end.
+
+check_solutions([], _Fun, _S, Map) ->
+  Map;
+check_solutions([{S1,Map1,_Time1}|Maps], Fun, S, Map) ->
+  ?debug("Solver ~w needed ~w microsecs\n", [S1, _Time1]),
+  case Map =:= no_map orelse sane_maps(Map, Map1, [Fun], S, S1) of
+    true ->
+      check_solutions(Maps, Fun, S1, Map1);
+    false ->
+      ?debug("Constraint solvers do not agree on ~w\n", [Fun]),
+      pp_map(atom_to_list(S), Map),
+      pp_map(atom_to_list(S1), Map1),
+      throw(error)
+  end.
+
+sane_maps(Map1, Map2, Keys, _S1, _S2) ->
+  lists:all(fun(Key) ->
+                V1 = unsafe_lookup_type(Key, Map1),
+                V2 = unsafe_lookup_type(Key, Map2),
+                case t_is_equal(V1, V2) of
+                  true -> true;
+                  false ->
+                    ?debug("Constraint solvers do not agree on ~w\n", [Key]),
+                    ?debug("~w: ~s\n",
+                           [_S1, format_type(unsafe_lookup_type(Key, Map1))]),
+                    ?debug("~w: ~s\n",
+                           [_S2, format_type(unsafe_lookup_type(Key, Map2))]),
+                    false
+                end
+            end, Keys).
+
+%% Solver v2
+
+-record(v2_state, {constr_data = dict:new() :: dict(),
+                   state :: #state{}}).
+
+v2_solve_ref(Fun, Map, State) ->
+  V2State = #v2_state{state = State},
+  {ok, NewMap, _, _} = v2_solve_reference(Fun, Map, V2State),
+  {ok, NewMap}.
+
+v2_solve(#constraint{}=C, Map, V2State) ->
+  State = V2State#v2_state.state,
+  case solve_one_c(C, Map, State#state.opaques) of
+    error ->
+      report_failed_constraint(C, Map),
+      {error, V2State};
+    {ok, {NewMap, U}} ->
+      {ok, NewMap, V2State, U}
+  end;
+v2_solve(#constraint_list{type = disj}=C, Map, V2State) ->
+  v2_solve_disjunct(C, Map, V2State);
+v2_solve(#constraint_list{type = conj}=C, Map, V2State) ->
+  v2_solve_conjunct(C, Map, V2State);
+v2_solve(#constraint_ref{id = Id}, Map, V2State) ->
+  v2_solve_reference(Id, Map, V2State).
+
+v2_solve_reference(Id, Map, V2State0) ->
+  ?debug("Checking ref to fun: ~w\n", [debug_lookup_name(Id)]),
+  pp_map("Map", Map),
+  pp_constr_data("solve_ref", V2State0),
+  Map1 = restore_local_map(V2State0, Id, Map),
+  State = V2State0#v2_state.state,
+  Cs = state__get_cs(Id, State),
+  Res =
+    case state__is_self_rec(Id, State) of
+      true -> v2_solve_self_recursive(Cs, Map1, Id, t_none(), V2State0);
+      false -> v2_solve(Cs, Map1, V2State0)
+    end,
+  {FunType, V2State} =
+    case Res of
+      {error, V2State1} ->
+        ?debug("Error solving for function ~p\n", [debug_lookup_name(Id)]),
+        Arity = state__fun_arity(Id, State),
+        FunType0 =
+          case state__prop_domain(t_var_name(Id), State) of
+            error -> t_fun(Arity, t_none());
+            {ok, Dom} -> t_fun(Dom, t_none())
+          end,
+        {FunType0, V2State1};
+      {ok, NewMap, V2State1, U} ->
+        ?debug("Done solving fun: ~p\n", [debug_lookup_name(Id)]),
+        FunType0 = lookup_type(Id, NewMap),
+        V2State2 = save_local_map(V2State1, Id, U, NewMap),
+        {FunType0, V2State2}
+    end,
+  ?debug("ref Id=~w Assigned ~s\n", [Id, format_type(FunType)]),
+  {NewMap1, U1} = enter_var_type(Id, FunType, Map),
+  {NewMap2, U2} =
+    case state__get_rec_var(Id, State) of
+      {ok, Var} -> enter_var_type(Var, FunType, NewMap1);
+      error -> {NewMap1, []}
+    end,
+  {ok, NewMap2, V2State, lists:umerge(U1, U2)}.
+
+v2_solve_self_recursive(Cs, Map, Id, RecType0, V2State0) ->
+  ?debug("Solving self recursive ~w\n", [debug_lookup_name(Id)]),
+  State = V2State0#v2_state.state,
+  {ok, RecVar} = state__get_rec_var(Id, State),
+  ?debug("OldRecType ~s\n", [format_type(RecType0)]),
+  RecType = t_limit(RecType0, ?TYPE_LIMIT),
+  {Map1, U0} = enter_var_type(RecVar, RecType, Map),
+  V2State1 = save_updated_vars1(V2State0, Cs, U0), % Probably not necessary
+  case v2_solve(Cs, Map1, V2State1) of
+    {error, _V2State}=Error ->
+      case t_is_none(RecType0) of
+	true ->
+	  %% Try again and assume that this is a non-terminating function.
+	  Arity = state__fun_arity(Id, State),
+	  NewRecType = t_fun(lists:duplicate(Arity, t_any()), t_unit()),
+	  v2_solve_self_recursive(Cs, Map, Id, NewRecType, V2State0);
+	false ->
+	  Error
+      end;
+    {ok, NewMap, V2State, U} ->
+      pp_map("recursive finished", NewMap),
+      NewRecType = unsafe_lookup_type(Id, NewMap),
+      case t_is_equal(NewRecType, RecType0) of
+	true ->
+          {NewMap2, U1} = enter_var_type(RecVar, NewRecType, NewMap),
+	  {ok, NewMap2, V2State, lists:umerge(U, U1)};
+	false ->
+	  v2_solve_self_recursive(Cs, Map, Id, NewRecType, V2State0)
+      end
+  end.
+
+enter_var_type(Var, Type, Map0) ->
+  {Map, Vs} = enter_type2(Var, Type, Map0),
+  {Map, [t_var_name(V) || V <- Vs]}.
+
+v2_solve_disjunct(Disj, Map, V2State0) ->
+  #constraint_list{type = disj, id = _Id, list = Cs, masks = Masks} = Disj,
+  ?debug("disjunct Id=~w~n", [_Id]),
+  pp_map("Map", Map),
+  pp_constr_data("disjunct", V2State0),
+  case get_flags(V2State0, Disj) of
+    {V2State1, failed_list} -> {error, V2State1}; % cannot happen
+    {V2State1, Flags} when Flags =/= [] ->
+      {ok, V2State, Eval, UL, MapL0, Uneval, Failed} =
+        v2_solve_disj(Flags, Cs, 1, Map, V2State1, [], [], [], [], false),
+      ?debug("disj ending _Id=~w Eval=~w, |Uneval|=~w |UL|=~w~n",
+             [_Id, Eval, length(Uneval), length(UL)]),
+      if Eval =:= [], Uneval =:= [] ->
+           {error, failed_list(Disj, V2State0)};
+         true ->
+           {Is0, UnIds} = lists:unzip(Uneval),
+           MapL = [restore_local_map(V2State, Id, Map) ||
+                    Id <- UnIds] ++ MapL0,
+           %% If some branch has just failed every variable of the
+           %% non-failed branches need to be checked, not just the
+           %% updated ones.
+           U0 = case Failed of
+                  false -> lists:umerge(UL);
+                  true -> constrained_keys(MapL)
+                end,
+           if U0 =:= [] -> {ok, Map, V2State, []};
+              true ->
+                NotFailed = lists:umerge(Is0, Eval),
+                U1 = [V || V <- U0,
+                           var_occurs_everywhere(V, Masks, NotFailed)],
+                NewMap = join_maps(U1, MapL, Map),
+                pp_map("NewMap", NewMap),
+                U = updated_vars_only(U1, Map, NewMap),
+                ?debug("disjunct finished _Id=~w\n", [_Id]),
+                {ok, NewMap, V2State, U}
+           end
+      end
+  end.
+
+var_occurs_everywhere(V, Masks, NotFailed) ->
+  ordsets:is_subset(NotFailed, get_mask(V, Masks)).
+
+v2_solve_disj([I|Is], [C|Cs], I, Map0, V2State0, UL, MapL, Eval, Uneval,
+              Failed0) ->
+  Id = C#constraint_list.id,
+  Map1 = restore_local_map(V2State0, Id, Map0),
+  case v2_solve(C, Map1, V2State0) of
+    {error, V2State} ->
+      ?debug("disj error I=~w~n", [I]),
+      Failed = Failed0 orelse not is_failed_list(C, V2State0),
+      v2_solve_disj(Is, Cs, I+1, Map0, V2State, UL, MapL, Eval, Uneval, Failed);
+    {ok, Map, V2State1, U} ->
+      ?debug("disj I=~w U=~w~n", [I, U]),
+      V2State = save_local_map(V2State1, Id, U, Map),
+      pp_map("DMap", Map),
+      v2_solve_disj(Is, Cs, I+1, Map0, V2State, [U|UL], [Map|MapL],
+                    [I|Eval], Uneval, Failed0)
+  end;
+v2_solve_disj([], [], _I, _Map, V2State, UL, MapL, Eval, Uneval, Failed) ->
+  {ok, V2State, lists:reverse(Eval), UL, MapL, lists:reverse(Uneval), Failed};
+v2_solve_disj(Is, [C|Cs], I, Map, V2State, UL, MapL, Eval, Uneval0, Failed) ->
+  Uneval = [{I,C#constraint_list.id} ||
+             not is_failed_list(C, V2State)] ++ Uneval0,
+  v2_solve_disj(Is, Cs, I+1, Map, V2State, UL, MapL, Eval, Uneval, Failed).
+
+save_local_map(#v2_state{constr_data = ConData}=V2State, Id, U, Map) ->
+  Part0 = [{V,dict:fetch(V, Map)} || V <- U],
+  Part1 =
+    case dict:find(Id, ConData) of
+      error -> []; % cannot happen
+      {ok, {Part2,[]}} -> Part2
+    end,
+  ?debug("save local map Id=~w:\n", [Id]),
+  Part = lists:ukeymerge(1, lists:keysort(1, Part0), Part1),
+  pp_map("New Part", dict:from_list(Part0)),
+  pp_map("Old Part", dict:from_list(Part1)),
+  pp_map(" => Part", dict:from_list(Part)),
+  V2State#v2_state{constr_data = dict:store(Id, {Part,[]}, ConData)}.
+
+restore_local_map(#v2_state{constr_data = ConData}, Id, Map0) ->
+  case dict:find(Id, ConData) of
+    error -> Map0;
+    {ok, failed} -> Map0;
+    {ok, {[],_}} -> Map0;
+    {ok, {Part0,U}} ->
+      Part = [{K,V} || {K,V} <- Part0, not lists:member(K, U)],
+      ?debug("restore local map Id=~w U=~w\n", [Id, U]),
+      pp_map("Part", dict:from_list(Part)),
+      pp_map("Map0", Map0),
+      Map = lists:foldl(fun({K,V}, D) -> dict:store(K, V, D)end, Map0, Part),
+      pp_map("Map", Map),
+      Map
+  end.
+
+v2_solve_conjunct(Conj, Map, V2State0) ->
+  #constraint_list{type = conj, list = Cs} = Conj,
+  ?debug("conjunct Id=~w~n", [Conj#constraint_list.id]),
+  IsFlat = case Cs of [#constraint{}|_] -> true; _ -> false end,
+  case get_flags(V2State0, Conj) of
+    {V2State, failed_list} -> {error, V2State};
+    {V2State, Flags} ->
+      v2_solve_conj(Flags, Cs, 1, Map, Conj, IsFlat, V2State, [], [], [],
+                    Map, Flags)
+  end.
+
+%% LastMap and LastFlags are used for loop detection.
+v2_solve_conj([I|Is], [Cs|Tail], I, Map0, Conj, IsFlat, V2State0,
+              UL, NewFs0, VarsUp, LastMap, LastFlags) ->
+  ?debug("conj Id=~w I=~w~n", [Conj#constraint_list.id, I]),
+  true = IsFlat =:= is_record(Cs, constraint),
+  pp_constr_data("conj", V2State0),
+  case v2_solve(Cs, Map0, V2State0) of
+    {error, V2State1} -> {error, failed_list(Conj, V2State1)};
+    {ok, Map, V2State1, []} ->
+      v2_solve_conj(Is, Tail, I+1, Map, Conj, IsFlat, V2State1,
+                    UL, NewFs0, VarsUp, LastMap, LastFlags);
+    {ok, Map, V2State1, U} when IsFlat -> % optimization
+      %% It is ensured by enumerate_constraints() that every
+      %% #constraint{} has a conjunct as parent, and that such a
+      %% parent has nothing but #constraint{}:s as children, a fact
+      %% which is used here to simplify the flag calculation.
+      Mask = lists:umerge([get_mask(V, Conj#constraint_list.masks) || V <- U]),
+      {Is1, NewF} = add_mask_to_flags(Is, Mask, I, []),
+      NewFs = [NewF|NewFs0],
+      v2_solve_conj(Is1, Tail, I+1, Map, Conj, IsFlat, V2State1,
+                    [U|UL], NewFs, VarsUp, LastMap, LastFlags);
+    {ok, Map, V2State1, U} ->
+      #constraint_list{masks = Masks, list = AllCs} = Conj,
+      M = lists:keydelete(I, 1, vars_per_child(U, Masks)),
+      {V2State2, NewF0} = save_updated_vars_list(AllCs, M, V2State1),
+      {NewF, F} = lists:splitwith(fun(J) -> J < I end, NewF0),
+      Is1 = lists:umerge(Is, F),
+      NewFs = [NewF|NewFs0],
+      v2_solve_conj(Is1, Tail, I+1, Map, Conj, IsFlat, V2State2,
+                    [U|UL], NewFs, VarsUp, LastMap, LastFlags)
+  end;
+v2_solve_conj([], _Cs, _I, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp,
+             LastMap, LastFlags) ->
+  U = lists:umerge(UL),
+  case lists:umerge(NewFs) of
+    [] ->
+      ?debug("conjunct finished Id=~w\n", [Conj#constraint_list.id]),
+      {ok, Map, V2State, lists:umerge([U|VarsUp])};
+    NewFlags when NewFlags =:= LastFlags, Map =:= LastMap ->
+      %% A loop was detected! The cause is some bug, possibly in erl_types.
+      %% The evaluation continues, but the results can be wrong.
+      report_detected_loop(Conj),
+      {ok, Map, V2State, lists:umerge([U|VarsUp])};
+    NewFlags ->
+      #constraint_list{type = conj, list = Cs} = Conj,
+      v2_solve_conj(NewFlags, Cs, 1, Map, Conj, IsFlat, V2State,
+                    [], [], [U|VarsUp], Map, NewFlags)
+  end;
+v2_solve_conj(Is, [_|Tail], I, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp,
+             LastMap, LastFlags) ->
+  v2_solve_conj(Is, Tail, I+1, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp,
+               LastMap, LastFlags).
+
+-ifdef(DEBUG_LOOP_DETECTION).
+report_detected_loop(Conj) ->
+  io:format("A loop was detected in ~w\n", [Conj#constraint_list.id]).
+-else.
+report_detected_loop(_) ->
+  ok.
+-endif.
+
+add_mask_to_flags(Flags, [Im|M], I, L) when I > Im ->
+  add_mask_to_flags(Flags, M, I, [Im|L]);
+add_mask_to_flags(Flags, [_|M], _I, L) ->
+  {lists:umerge(Flags, M), lists:reverse(L)}.
+
+get_mask(V, {d, Masks}) ->
+  case dict:find(V, Masks) of
+    error -> [];
+    {ok, M} -> M
+  end;
+get_mask(V, Masks) ->
+  case lists:keyfind(V, 1, Masks) of
+    false -> [];
+    {V, M} -> M
+  end.
+
+get_flags(#v2_state{constr_data = ConData}=V2State0, C) ->
+  #constraint_list{id = Id, list = Cs, masks = Masks} = C,
+  case dict:find(Id, ConData) of
+    error ->
+      ?debug("get_flags Id=~w Flags=all ~w\n", [Id, length(Cs)]),
+      V2State = V2State0#v2_state{constr_data = dict:store(Id, {[],[]}, ConData)},
+      {V2State, lists:seq(1, length(Cs))};
+    {ok, failed} ->
+      {V2State0, failed_list};
+    {ok, {Part,U}} when U =/= [] ->
+      ?debug("get_flags Id=~w U=~w\n", [Id, U]),
+      V2State = V2State0#v2_state{constr_data = dict:store(Id, {Part,[]}, ConData)},
+      save_updated_vars_list(Cs, vars_per_child(U, Masks), V2State)
+  end.
+
+vars_per_child(U, Masks) ->
+  family([{I, V} || V <- lists:usort(U), I <- get_mask(V, Masks)]).
+
+save_updated_vars_list(Cs, IU, V2State) ->
+  save_updated_vars_list1(Cs, IU, V2State, 1, []).
+
+save_updated_vars_list1([C|Cs], [{I,U}|IU], V2State0, I, Is) ->
+  V2State = save_updated_vars(C, U, V2State0),
+  save_updated_vars_list1(Cs, IU, V2State, I+1, [I|Is]);
+save_updated_vars_list1([], [], V2State, _I, Is) ->
+  {V2State, lists:reverse(Is)};
+save_updated_vars_list1([_|Cs], IU, V2State, I, Is) ->
+  save_updated_vars_list1(Cs, IU, V2State, I+1, Is).
+
+save_updated_vars(#constraint{}, _, V2State) ->
+  V2State;
+save_updated_vars(#constraint_list{}=C, U, V2State0) ->
+  save_updated_vars1(V2State0, C, U);
+save_updated_vars(#constraint_ref{id = Id}, U, V2State) ->
+  Cs = state__get_cs(Id, V2State#v2_state.state),
+  save_updated_vars(Cs, U, V2State).
+
+save_updated_vars1(V2State, C, U) ->
+  #v2_state{constr_data = ConData} = V2State,
+  #constraint_list{id = Id} = C,
+  case dict:find(Id, ConData) of
+    error -> V2State; % error means everything is flagged
+    {ok, failed} -> V2State;
+    {ok, {Part,U0}} ->
+      %% Duplicates are not so common; let masks/2 remove them.
+      U1 = U ++ U0,
+      V2State#v2_state{constr_data = dict:store(Id, {Part,U1}, ConData)}
+  end.
+
+-ifdef(DEBUG).
+pp_constr_data(_Tag, #v2_state{constr_data = D}) ->
+  io:format("Constr data at ~p\n", [_Tag]),
+  _ = [begin
+         case _PartU of
+           {_Part, _U} ->
+             io:format("Id: ~w Vars: ~w\n", [_Id, _U]),
+             [pp_map("Part", dict:from_list(_Part)) || _Part =/= []];
+           failed ->
+             io:format("Id: ~w failed list\n", [_Id])
+         end
+       end ||
+        {_Id, _PartU} <- lists:keysort(1, dict:to_list(D))],
+  ok.
+
+-else.
+pp_constr_data(_Tag, _V2State) ->
+  ok.
+-endif.
+
+failed_list(#constraint_list{id = Id}, #v2_state{constr_data = D}=V2State) ->
+  ?debug("error list ~w~n", [Id]),
+  V2State#v2_state{constr_data = dict:store(Id, failed, D)}.
+
+is_failed_list(#constraint_list{id = Id}, #v2_state{constr_data = D}) ->
+  dict:find(Id, D) =:= {ok, failed}.
+
+%% Solver v1
+
 solve_ref_or_list(#constraint_ref{id = Id, deps = Deps},
 		  Map, MapDict, State) ->
   {OldLocalMap, Check} =
     case dict:find(Id, MapDict) of
-      error -> {dict:new(), false};
+      error -> {map_new(), false};
       {ok, M} -> {M, true}
     end,
   ?debug("Checking ref to fun: ~w\n", [debug_lookup_name(Id)]),
+  %% Note: mk_constraint_ref() has already removed Id from Deps. The
+  %% reason for doing it there is that it makes it easy for
+  %% calculate_masks() to make the corresponding adjustment for
+  %% version v2.
   CheckDeps = ordsets:del_element(t_var_name(Id), Deps),
+  true = CheckDeps =:= Deps,
   case Check andalso maps_are_equal(OldLocalMap, Map, CheckDeps) of
     true ->
       ?debug("Equal\n", []),
@@ -1892,6 +2321,7 @@ solve_ref_or_list(#constraint_ref{id = Id, deps = Deps},
 	    FunType0 = lookup_type(Id, NewMap),
 	    {NewMapDict0, FunType0}
 	end,
+      ?debug("  Id=~w Assigned ~s\n", [Id, format_type(FunType)]),
       NewMap1 = enter_type(Id, FunType, Map),
       NewMap2 =
 	case state__get_rec_var(Id, State) of
@@ -1904,7 +2334,7 @@ solve_ref_or_list(#constraint_list{type=Type, list = Cs, deps = Deps, id = Id},
 		  Map, MapDict, State) ->
   {OldLocalMap, Check} =
     case dict:find(Id, MapDict) of
-      error -> {dict:new(), false};
+      error -> {map_new(), false};
       {ok, M} -> {M, true}
     end,
   ?debug("Checking ref to list: ~w\n", [Id]),
@@ -1926,7 +2356,7 @@ solve_self_recursive(Cs, Map, MapDict, Id, RecType0, State) ->
   {ok, RecVar} = state__get_rec_var(Id, State),
   ?debug("OldRecType ~s\n", [format_type(RecType0)]),
   RecType = t_limit(RecType0, ?TYPE_LIMIT),
-  Map1 = enter_type(RecVar, RecType, dict:erase(t_var_name(Id), Map)),
+  Map1 = enter_type(RecVar, RecType, erase_type(t_var_name(Id), Map)),
   pp_map("Map1", Map1),
   case solve_ref_or_list(Cs, Map1, MapDict, State) of
     {error, _} = Error ->
@@ -1994,14 +2424,9 @@ solve_cs([#constraint_list{} = C|Tail], Map, MapDict, State) ->
 solve_cs([#constraint{} = C|Tail], Map, MapDict, State) ->
   case solve_one_c(C, Map, State#state.opaques) of
     error ->
-      ?debug("+++++++++++\nFailed: ~s :: ~s ~w ~s :: ~s\n+++++++++++\n",
-	     [format_type(C#constraint.lhs),
-	      format_type(lookup_type(C#constraint.lhs, Map)),
-	      C#constraint.op,
-	      format_type(C#constraint.rhs),
-	      format_type(lookup_type(C#constraint.rhs, Map))]),
+      report_failed_constraint(C, Map),
       {error, MapDict};
-    {ok, NewMap} ->
+    {ok, {NewMap, _U}} ->
       solve_cs(Tail, NewMap, MapDict, State)
   end;
 solve_cs([], Map, MapDict, _State) ->
@@ -2022,7 +2447,11 @@ solve_one_c(#constraint{lhs = Lhs, rhs = Rhs, op = Op}, Map, Opaques) ->
 	eq ->
 	  case solve_subtype(Lhs, Inf, Map, Opaques) of
 	    error -> error;
-	    {ok, Map1} -> solve_subtype(Rhs, Inf, Map1, Opaques)
+	    {ok, {Map1, U1}} ->
+              case solve_subtype(Rhs, Inf, Map1, Opaques) of
+                error -> error;
+                {ok, {Map2, U2}} -> {ok, {Map2, lists:umerge(U1, U2)}}
+              end
 	  end
       end
   end.
@@ -2045,20 +2474,34 @@ solve_subtype(Type, Inf, Map, Opaques) ->
       end.
   %% end.
 
+report_failed_constraint(_C, _Map) ->
+  ?debug("+++++++++++\nFailed: ~s :: ~s ~w ~s :: ~s\n+++++++++++\n",
+         [format_type(_C#constraint.lhs),
+          format_type(lookup_type(_C#constraint.lhs, _Map)),
+          _C#constraint.op,
+          format_type(_C#constraint.rhs),
+          format_type(lookup_type(_C#constraint.rhs, _Map))]).
+
 %% ============================================================================
 %%
 %%  Maps and types.
 %%
 %% ============================================================================
 
+map_new() ->
+  dict:new().
+
 join_maps([Map]) ->
   Map;
 join_maps(Maps) ->
-  Keys = lists:foldl(fun(TmpMap, AccKeys) ->
-			 [Key || Key <- AccKeys, dict:is_key(Key, TmpMap)]
-		     end,
-		     dict:fetch_keys(hd(Maps)), tl(Maps)),
-  join_maps(Keys, Maps, dict:new()).
+  Keys = constrained_keys(Maps),
+  join_maps(Keys, Maps, map_new()).
+
+constrained_keys(Maps) ->
+  lists:foldl(fun(TmpMap, AccKeys) ->
+                  [Key || Key <- AccKeys, dict:is_key(Key, TmpMap)]
+              end,
+              dict:fetch_keys(hd(Maps)), tl(Maps)).
 
 join_maps([Key|Left], Maps = [Map|MapsLeft], AccMap) ->
   NewType = join_one_key(Key, MapsLeft, lookup_type(Key, Map)),
@@ -2121,13 +2564,13 @@ enter_type(Key, Val, Map) when is_integer(Key) ->
   ?debug("Entering ~s :: ~s\n", [format_type(t_var(Key)), format_type(Val)]),
   case t_is_any(Val) of
     true ->
-      dict:erase(Key, Map);
+      erase_type(Key, Map);
     false ->
       LimitedVal = t_limit(Val, ?INTERNAL_TYPE_LIMIT),
       case dict:find(Key, Map) of
 	{ok, LimitedVal} -> Map;
-	{ok, _} -> dict:store(Key, LimitedVal, Map);
-	error -> dict:store(Key, LimitedVal, Map)
+	{ok, _} -> map_store(Key, LimitedVal, Map);
+	error -> map_store(Key, LimitedVal, Map)
       end
   end;
 enter_type(Key, Val, Map) ->
@@ -2135,13 +2578,13 @@ enter_type(Key, Val, Map) ->
   KeyName = t_var_name(Key),
   case t_is_any(Val) of
     true ->
-      dict:erase(KeyName, Map);
+      erase_type(KeyName, Map);
     false ->
       LimitedVal = t_limit(Val, ?INTERNAL_TYPE_LIMIT),
       case dict:find(KeyName, Map) of
 	{ok, LimitedVal} -> Map;
-	{ok, _} -> dict:store(KeyName, LimitedVal, Map);
-	error -> dict:store(KeyName, LimitedVal, Map)
+	{ok, _} -> map_store(KeyName, LimitedVal, Map);
+	error -> map_store(KeyName, LimitedVal, Map)
       end
   end.
 
@@ -2151,11 +2594,25 @@ enter_type_lists([Key|KeyTail], [Val|ValTail], Map) ->
 enter_type_lists([], [], Map) ->
   Map.
 
-enter_type_list([{Key, Val}|Tail], Map) ->
+enter_type_list(KeyVals, Map) ->
+  enter_type_list(KeyVals, Map, []).
+
+enter_type_list([{Key, Val}|Tail], Map, U0) ->
+  {Map1,U1} = enter_type2(Key, Val, Map),
+  enter_type_list(Tail, Map1, U1++U0);
+enter_type_list([], Map, U) ->
+  {Map, ordsets:from_list(U)}.
+
+enter_type2(Key, Val, Map) ->
   Map1 = enter_type(Key, Val, Map),
-  enter_type_list(Tail, Map1);
-enter_type_list([], Map) ->
-  Map.
+  {Map1, [Key || not is_same(Key, Map, Map1)]}.
+
+map_store(Key, Val, Map) ->
+  ?debug("Storing ~w :: ~s\n", [Key, format_type(Val)]),
+  dict:store(Key, Val, Map).
+
+erase_type(Key, Map) ->
+  dict:erase(Key, Map).
 
 lookup_type_list(List, Map) ->
   [lookup_type(X, Map) || X <- List].
@@ -2206,12 +2663,17 @@ mk_var_no_lit(Var) ->
 mk_var_no_lit_list(List) ->
   [mk_var_no_lit(X) || X <- List].
 
+updated_vars_only(U, OldMap, NewMap) ->
+  [V || V <- U, not is_same(V, OldMap, NewMap)].
+
+is_same(Key, Map1, Map2) ->
+  t_is_equal(lookup_type(Key, Map1), lookup_type(Key, Map2)).
+
 pp_map(_S, _Map) ->
   ?debug("\t~s: ~p\n",
             [_S, [{X, lists:flatten(format_type(Y))} ||
                   {X, Y} <- lists:keysort(1, dict:to_list(_Map))]]).
 
-
 %% ============================================================================
 %%
 %%  The State.
@@ -2458,7 +2920,7 @@ mk_constraint(Lhs, Op, Rhs) ->
       case Deps =:= [] of
 	true ->
 	  %% This constraint is constant. Solve it immediately.
-	  case solve_one_c(C, dict:new(), []) of
+	  case solve_one_c(C, map_new(), []) of
 	    error -> throw(error);
 	    _ ->
 	      %% This is always true, keep it anyway for logistic reasons
@@ -2481,8 +2943,9 @@ constraint_opnd_is_any(Type) -> t_is_any(Type).
 
 -ifdef(DEBUG).
 
--spec mk_fun_var(fun((_) -> erl_types:erl_type()), [erl_types:erl_type()],
-		    integer()) -> #fun_var{}.
+-spec mk_fun_var(integer(),
+                 fun((_) -> erl_types:erl_type()),
+                 [erl_types:erl_type()]) -> #fun_var{}.
 
 mk_fun_var(Line, Fun, Types) ->
   Deps = [t_var_name(Var) || Var <- t_collect_vars(t_product(Types))],
@@ -2530,7 +2993,9 @@ mk_constraints([], _Op, []) ->
   [].
 
 mk_constraint_ref(Id, Deps) ->
-  #constraint_ref{id = Id, deps = Deps}.
+  %% See also solve_ref_or_list(), #constraint_ref{}.
+  Ds = ordsets:del_element(t_var_name(Id), Deps),
+  #constraint_ref{id = Id, deps = Ds}.
 
 mk_constraint_list(Type, List) ->
   List1 = ordsets:from_list(lift_lists(Type, List)),
@@ -2680,7 +3145,7 @@ enumerate_constraints([#constraint_list{type = conj, list = List} = C|Tail],
       NewDeep =:= [] -> {NewFlat, N2};
       true ->
         TmpCList = mk_conj_constraint_list(NewFlat),
-        {[TmpCList#constraint_list{id = {list, N2}} |  NewDeep],
+        {[TmpCList#constraint_list{id = {list, N2}}| NewDeep],
          N2 + 1}
     end,
   NewAcc = [C#constraint_list{list = NewList, id = {list, N3}}|Acc],
@@ -2725,7 +3190,9 @@ order_fun_constraints([#constraint_list{list = List, type = Type} = C|Tail],
 		  end,
 	lists:mapfoldl(FoldFun, State, List)
     end,
-  NewAcc = [update_constraint_list(C, NewList)|Acc],
+  C1 = update_constraint_list(C, NewList),
+  Masks = calculate_masks(NewList, 1, []),
+  NewAcc = [update_masks(C1, Masks)|Acc],
   order_fun_constraints(Tail, Funs, NewAcc, NewState);
 order_fun_constraints([#constraint{} = C|Tail], Funs, Acc, State) ->
   order_fun_constraints(Tail, Funs, [C|Acc], State);
@@ -2733,6 +3200,22 @@ order_fun_constraints([], Funs, Acc, State) ->
   NewState = order_fun_constraints(Funs, State),
   {lists:reverse(Acc)++Funs, NewState}.
 
+update_masks(C, Masks) ->
+  C#constraint_list{masks = Masks}.
+
+-define(VARS_LIMIT, 50).
+
+calculate_masks([C|Cs], I, L0) ->
+  calculate_masks(Cs, I+1, [{V, I} || V <- get_deps(C)] ++ L0);
+calculate_masks([], _I, L) ->
+  M = family(L),
+  case length(M) > ?VARS_LIMIT of
+    true ->
+      {d, dict:from_list(M)};
+    false ->
+      M
+  end.
+
 %% ============================================================================
 %%
 %%  Utilities.
@@ -2810,6 +3293,9 @@ lookup_record(Records, Tag, Arity) ->
       error
   end.
 
+family(L) ->
+    sofs:to_external(sofs:rel2fam(sofs:relation(L))).
+
 %% ============================================================================
 %%
 %%  Pretty printer and debug facilities.
@@ -2834,8 +3320,8 @@ format_type(Type) ->
 
 join_chars([], _Sep) ->
   [];
-join_chars([H | T], Sep) ->
-  [H | [[Sep,X] || X <- T]].
+join_chars([H|T], Sep) ->
+  [H|[[Sep,X] || X <- T]].
 
 debug_lookup_name(Var) ->
   case dict:find(t_var_name(Var), get(dialyzer_typesig_map)) of
-- 
cgit v1.2.3


From 1da86205f48d4572a9630c2727b452b459ac3387 Mon Sep 17 00:00:00 2001
From: Hans Bolinder <hasse@erlang.org>
Date: Wed, 13 Jun 2012 10:16:06 +0200
Subject: 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.
---
 lib/dialyzer/src/dialyzer.hrl                    |  9 +++--
 lib/dialyzer/src/dialyzer_analysis_callgraph.erl | 13 ++++---
 lib/dialyzer/src/dialyzer_cl.erl                 |  5 ++-
 lib/dialyzer/src/dialyzer_cl_parse.erl           |  9 ++++-
 lib/dialyzer/src/dialyzer_options.erl            | 14 ++++++-
 lib/dialyzer/src/dialyzer_succ_typings.erl       | 48 +++++++++++++-----------
 lib/dialyzer/src/dialyzer_typesig.erl            | 30 +++++++++------
 7 files changed, 82 insertions(+), 46 deletions(-)

(limited to 'lib/dialyzer')

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}.
-- 
cgit v1.2.3