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

1 files changed, 76 insertions, 6 deletions

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) ->