1%% -*- erlang-indent-level: 2 -*-
2%%
3%% Licensed under the Apache License, Version 2.0 (the "License");
4%% you may not use this file except in compliance with the License.
5%% You may obtain a copy of the License at
6%%
7%%     http://www.apache.org/licenses/LICENSE-2.0
8%%
9%% Unless required by applicable law or agreed to in writing, software
10%% distributed under the License is distributed on an "AS IS" BASIS,
11%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12%% See the License for the specific language governing permissions and
13%% limitations under the License.
14
15%%%-------------------------------------------------------------------
16%%% File    : dialyzer_dataflow.erl
17%%% Author  : Tobias Lindahl <tobiasl@it.uu.se>
18%%% Description :
19%%%
20%%% Created : 19 Apr 2005 by Tobias Lindahl <tobiasl@it.uu.se>
21%%%-------------------------------------------------------------------
22
23-module(dialyzer_dataflow).
24
25-export([get_fun_types/5, get_warnings/5, format_args/3]).
26
27%% Data structure interfaces.
28-export([state__add_warning/2, state__cleanup/1,
29	 state__duplicate/1, dispose_state/1,
30         state__get_callgraph/1, state__get_races/1,
31         state__get_records/1, state__put_callgraph/2,
32         state__put_races/2, state__records_only/1,
33         state__find_function/2]).
34
35-export_type([state/0]).
36
37-include("dialyzer.hrl").
38
39-import(erl_types,
40        [t_inf/2, t_inf/3, t_inf_lists/2, t_inf_lists/3,
41         t_inf_lists/3, t_is_equal/2, t_is_subtype/2, t_subtract/2,
42         t_sup/1, t_sup/2]).
43
44-import(erl_types,
45	[any_none/1, t_any/0, t_atom/0, t_atom/1, t_atom_vals/1, t_atom_vals/2,
46	 t_binary/0, t_boolean/0,
47	 t_bitstr/0, t_bitstr/2, t_bitstr_concat/1, t_bitstr_match/2,
48	 t_cons/0, t_cons/2, t_cons_hd/2, t_cons_tl/2,
49         t_contains_opaque/2,
50	 t_find_opaque_mismatch/3, t_float/0, t_from_range/2, t_from_term/1,
51	 t_fun/0, t_fun/2, t_fun_args/1, t_fun_args/2, t_fun_range/1,
52	 t_fun_range/2, t_integer/0, t_integers/1,
53	 t_is_any/1, t_is_atom/1, t_is_atom/2, t_is_any_atom/3,
54         t_is_boolean/2,
55	 t_is_integer/2, t_is_list/1,
56	 t_is_nil/2, t_is_none/1, t_is_none_or_unit/1,
57	 t_is_number/2, t_is_reference/2, t_is_pid/2, t_is_port/2,
58         t_is_unit/1,
59	 t_limit/2, t_list/0, t_list_elements/2,
60	 t_maybe_improper_list/0, t_module/0,
61	 t_none/0, t_non_neg_integer/0, t_number/0, t_number_vals/2,
62	 t_pid/0, t_port/0, t_product/1, t_reference/0,
63         t_to_string/2, t_to_tlist/1,
64	 t_tuple/0, t_tuple/1, t_tuple_args/1, t_tuple_args/2,
65         t_tuple_subtypes/2,
66	 t_unit/0, t_unopaque/2,
67	 t_map/0, t_map/1, t_is_singleton/2
68     ]).
69
70%%-define(DEBUG, true).
71%%-define(DEBUG_PP, true).
72%%-define(DEBUG_TIME, true).
73
74-ifdef(DEBUG).
75-import(erl_types, [t_to_string/1]).
76-define(debug(S_, L_), io:format(S_, L_)).
77-else.
78-define(debug(S_, L_), ok).
79-endif.
80
81%%--------------------------------------------------------------------
82
83-type type()      :: erl_types:erl_type().
84-type types()     :: erl_types:type_table().
85
86-type curr_fun()  :: 'undefined' | 'top' | mfa_or_funlbl().
87
88-define(no_arg, no_arg).
89
90-define(TYPE_LIMIT, 3).
91
92-define(BITS, 128).
93
94%% Types with comment 'race' are due to dialyzer_races.erl.
95-record(state, {callgraph            :: dialyzer_callgraph:callgraph()
96                                      | 'undefined', % race
97                codeserver           :: dialyzer_codeserver:codeserver()
98                                      | 'undefined', % race
99		envs                 :: env_tab()
100                                      | 'undefined', % race
101		fun_tab		     :: fun_tab()
102                                      | 'undefined', % race
103                fun_homes            :: dict:dict(label(), mfa())
104                                      | 'undefined', % race
105		plt		     :: dialyzer_plt:plt()
106                                      | 'undefined', % race
107		opaques              :: [type()]
108                                      | 'undefined', % race
109		races = dialyzer_races:new() :: dialyzer_races:races(),
110		records = dict:new() :: types(),
111		tree_map	     :: dict:dict(label(), cerl:cerl())
112                                      | 'undefined', % race
113		warning_mode = false :: boolean(),
114		warnings = []        :: [raw_warning()],
115		work                 :: {[_], [_], sets:set()}
116                                      | 'undefined', % race
117		module               :: module(),
118                curr_fun             :: curr_fun()
119               }).
120
121-record(map, {map = maps:new()    :: type_tab(),
122              subst = maps:new()  :: subst_tab(),
123              modified = []       :: [Key :: term()],
124              modified_stack = [] :: [{[Key :: term()],reference()}],
125              ref = undefined     :: reference() | undefined}).
126
127-type env_tab()   :: dict:dict(label(), #map{}).
128-type fun_entry() :: {Args :: [type()], RetType :: type()}.
129-type fun_tab()   :: dict:dict('top' | label(),
130                               {'not_handled', fun_entry()} | fun_entry()).
131-type key()       :: label() | cerl:cerl().
132-type type_tab()  :: #{key() => type()}.
133-type subst_tab() :: #{key() => cerl:cerl()}.
134
135%% Exported Types
136
137-opaque state() :: #state{}.
138
139%%--------------------------------------------------------------------
140
141-type fun_types() :: dict:dict(label(), type()).
142
143-spec get_warnings(cerl:c_module(), dialyzer_plt:plt(),
144                   dialyzer_callgraph:callgraph(),
145                   dialyzer_codeserver:codeserver(),
146                   types()) ->
147	{[raw_warning()], fun_types()}.
148
149get_warnings(Tree, Plt, Callgraph, Codeserver, Records) ->
150  State1 = analyze_module(Tree, Plt, Callgraph, Codeserver, Records, true),
151  State2 = state__renew_warnings(state__get_warnings(State1), State1),
152  State3 = state__get_race_warnings(State2),
153  {State3#state.warnings, state__all_fun_types(State3)}.
154
155-spec get_fun_types(cerl:c_module(), dialyzer_plt:plt(),
156                    dialyzer_callgraph:callgraph(),
157                    dialyzer_codeserver:codeserver(),
158                    types()) -> fun_types().
159
160get_fun_types(Tree, Plt, Callgraph, Codeserver, Records) ->
161  State = analyze_module(Tree, Plt, Callgraph, Codeserver, Records, false),
162  state__all_fun_types(State).
163
164%%% ===========================================================================
165%%%
166%%%  The analysis.
167%%%
168%%% ===========================================================================
169
170analyze_module(Tree, Plt, Callgraph, Codeserver, Records, GetWarnings) ->
171  debug_pp(Tree, false),
172  Module = cerl:atom_val(cerl:module_name(Tree)),
173  TopFun = cerl:ann_c_fun([{label, top}], [], Tree),
174  State = state__new(Callgraph, Codeserver, TopFun, Plt, Module, Records),
175  State1 = state__race_analysis(not GetWarnings, State),
176  State2 = analyze_loop(State1),
177  case GetWarnings of
178    true ->
179      State3 = state__set_warning_mode(State2),
180      State4 = analyze_loop(State3),
181      dialyzer_races:race(State4);
182    false ->
183      State2
184  end.
185
186analyze_loop(State) ->
187  case state__get_work(State) of
188    none -> state__set_curr_fun(undefined, State);
189    {Fun, NewState0} ->
190      NewState1 = state__set_curr_fun(get_label(Fun), NewState0),
191      {ArgTypes, IsCalled} = state__get_args_and_status(Fun, NewState1),
192      case not IsCalled of
193	true ->
194	  ?debug("Not handling (not called) ~w: ~s\n",
195		 [NewState1#state.curr_fun,
196		  t_to_string(t_product(ArgTypes))]),
197	  analyze_loop(NewState1);
198	false ->
199	  case state__fun_env(Fun, NewState1) of
200	    none ->
201	      ?debug("Not handling (no env) ~w: ~s\n",
202		     [NewState1#state.curr_fun,
203		      t_to_string(t_product(ArgTypes))]),
204	      analyze_loop(NewState1);
205	    Map ->
206	      ?debug("Handling fun ~p: ~s\n",
207		     [NewState1#state.curr_fun,
208		      t_to_string(state__fun_type(Fun, NewState1))]),
209	      Vars = cerl:fun_vars(Fun),
210	      Map1 = enter_type_lists(Vars, ArgTypes, Map),
211	      Body = cerl:fun_body(Fun),
212              FunLabel = get_label(Fun),
213	      IsRaceAnalysisEnabled = is_race_analysis_enabled(State),
214              NewState3 =
215                case IsRaceAnalysisEnabled of
216                  true ->
217                    NewState2 = state__renew_curr_fun(
218                      state__lookup_name(FunLabel, NewState1), FunLabel,
219                      NewState1),
220                    state__renew_race_list([], 0, NewState2);
221		  false -> NewState1
222                end,
223	      {NewState4, _Map2, BodyType} =
224		traverse(Body, Map1, NewState3),
225	      ?debug("Done analyzing: ~w:~s\n",
226		     [NewState1#state.curr_fun,
227		      t_to_string(t_fun(ArgTypes, BodyType))]),
228              NewState5 =
229                case IsRaceAnalysisEnabled of
230                  true -> renew_race_code(NewState4);
231                  false -> NewState4
232                end,
233              NewState6 =
234                state__update_fun_entry(Fun, ArgTypes, BodyType, NewState5),
235              ?debug("done adding stuff for ~w\n",
236                     [state__lookup_name(get_label(Fun), State)]),
237              analyze_loop(NewState6)
238	  end
239      end
240  end.
241
242traverse(Tree, Map, State) ->
243  ?debug("Handling ~p\n", [cerl:type(Tree)]),
244  %% debug_pp_map(Map),
245  case cerl:type(Tree) of
246    alias ->
247      %% This only happens when checking for illegal record patterns
248      %% so the handling is a bit rudimentary.
249      traverse(cerl:alias_pat(Tree), Map, State);
250    apply ->
251      handle_apply(Tree, Map, State);
252    binary ->
253      Segs = cerl:binary_segments(Tree),
254      {State1, Map1, SegTypes} = traverse_list(Segs, Map, State),
255      {State1, Map1, t_bitstr_concat(SegTypes)};
256    bitstr ->
257      handle_bitstr(Tree, Map, State);
258    call ->
259      handle_call(Tree, Map, State);
260    'case' ->
261      handle_case(Tree, Map, State);
262    'catch' ->
263      {State1, _Map1, _} = traverse(cerl:catch_body(Tree), Map, State),
264      {State1, Map, t_any()};
265    cons ->
266      handle_cons(Tree, Map, State);
267    'fun' ->
268      Type = state__fun_type(Tree, State),
269      case state__warning_mode(State) of
270        true -> {State, Map, Type};
271        false ->
272          State2 = state__add_work(get_label(Tree), State),
273          State3 = state__update_fun_env(Tree, Map, State2),
274          {State3, Map, Type}
275      end;
276    'let' ->
277      handle_let(Tree, Map, State);
278    letrec ->
279      Defs = cerl:letrec_defs(Tree),
280      Body = cerl:letrec_body(Tree),
281      %% By not including the variables in scope we can assure that we
282      %% will get the current function type when using the variables.
283      FoldFun = fun({Var, Fun}, {AccState, AccMap}) ->
284		    {NewAccState, NewAccMap0, FunType} =
285		      traverse(Fun, AccMap, AccState),
286		    NewAccMap = enter_type(Var, FunType, NewAccMap0),
287		    {NewAccState, NewAccMap}
288		end,
289      {State1, Map1} = lists:foldl(FoldFun, {State, Map}, Defs),
290      traverse(Body, Map1, State1);
291    literal ->
292      Type = literal_type(Tree),
293      {State, Map, Type};
294    module ->
295      handle_module(Tree, Map, State);
296    primop ->
297      Type =
298	case cerl:atom_val(cerl:primop_name(Tree)) of
299	  match_fail -> t_none();
300	  raise -> t_none();
301	  bs_init_writable -> t_from_term(<<>>);
302	  Other -> erlang:error({'Unsupported primop', Other})
303	end,
304      {State, Map, Type};
305    'receive' ->
306      handle_receive(Tree, Map, State);
307    seq ->
308      Arg = cerl:seq_arg(Tree),
309      Body = cerl:seq_body(Tree),
310      {State1, Map1, ArgType} = SMA = traverse(Arg, Map, State),
311      case t_is_none_or_unit(ArgType) of
312	true ->
313	  SMA;
314	false ->
315	  State2 =
316	    case
317              t_is_any(ArgType)
318              orelse t_is_simple(ArgType, State)
319              orelse is_call_to_send(Arg)
320	      orelse is_lc_simple_list(Arg, ArgType, State)
321            of
322	      true -> % do not warn in these cases
323		State1;
324	      false ->
325		state__add_warning(State1, ?WARN_UNMATCHED_RETURN, Arg,
326				   {unmatched_return,
327				    [format_type(ArgType, State1)]})
328	    end,
329	  traverse(Body, Map1, State2)
330      end;
331    'try' ->
332      handle_try(Tree, Map, State);
333    tuple ->
334      handle_tuple(Tree, Map, State);
335    map ->
336      handle_map(Tree, Map, State);
337    values ->
338      Elements = cerl:values_es(Tree),
339      {State1, Map1, EsType} = traverse_list(Elements, Map, State),
340      Type = t_product(EsType),
341      {State1, Map1, Type};
342    var ->
343      ?debug("Looking up unknown variable: ~p\n", [Tree]),
344      case state__lookup_type_for_letrec(Tree, State) of
345	error ->
346	  LType = lookup_type(Tree, Map),
347          {State, Map, LType};
348	{ok, Type} -> {State, Map, Type}
349      end;
350    Other ->
351      erlang:error({'Unsupported type', Other})
352  end.
353
354traverse_list(Trees, Map, State) ->
355  traverse_list(Trees, Map, State, []).
356
357traverse_list([Tree|Tail], Map, State, Acc) ->
358  {State1, Map1, Type} = traverse(Tree, Map, State),
359  traverse_list(Tail, Map1, State1, [Type|Acc]);
360traverse_list([], Map, State, Acc) ->
361  {State, Map, lists:reverse(Acc)}.
362
363%%________________________________________
364%%
365%% Special instructions
366%%
367
368handle_apply(Tree, Map, State) ->
369  Args = cerl:apply_args(Tree),
370  Op = cerl:apply_op(Tree),
371  {State0, Map1, ArgTypes} = traverse_list(Args, Map, State),
372  {State1, Map2, OpType} = traverse(Op, Map1, State0),
373  case any_none(ArgTypes) of
374    true ->
375      {State1, Map2, t_none()};
376    false ->
377      FunList =
378	case state__lookup_call_site(Tree, State) of
379	  error -> [external]; %% so that we go directly in the fallback
380	  {ok, List} -> List
381	end,
382      FunInfoList = [{local, state__fun_info(Fun, State)} || Fun <- FunList],
383      case
384        handle_apply_or_call(FunInfoList, Args, ArgTypes, Map2, Tree, State1)
385      of
386	{had_external, State2} ->
387	  %% Fallback: use whatever info we collected from traversing the op
388	  %% instead of the result that has been generalized to t_any().
389	  Arity = length(Args),
390	  OpType1 = t_inf(OpType, t_fun(Arity, t_any())),
391	  case t_is_none(OpType1) of
392	    true ->
393	      Msg = {fun_app_no_fun,
394		     [format_cerl(Op), format_type(OpType, State2), Arity]},
395	      State3 = state__add_warning(State2, ?WARN_FAILING_CALL,
396					  Tree, Msg),
397	      {State3, Map2, t_none()};
398	    false ->
399	      NewArgs = t_inf_lists(ArgTypes,
400                                    t_fun_args(OpType1, 'universe')),
401	      case any_none(NewArgs) of
402		true ->
403		  Msg = {fun_app_args,
404			 [format_args(Args, ArgTypes, State),
405			  format_type(OpType, State)]},
406		  State3 = state__add_warning(State2, ?WARN_FAILING_CALL,
407					      Tree, Msg),
408		  {State3, enter_type(Op, OpType1, Map2), t_none()};
409		false ->
410		  Map3 = enter_type_lists(Args, NewArgs, Map2),
411		  Range0 = t_fun_range(OpType1, 'universe'),
412		  Range =
413		    case t_is_unit(Range0) of
414		      true  -> t_none();
415		      false -> Range0
416		    end,
417		  {State2, enter_type(Op, OpType1, Map3), Range}
418	      end
419	  end;
420	Normal -> Normal
421      end
422  end.
423
424handle_apply_or_call(FunInfoList, Args, ArgTypes, Map, Tree, State) ->
425  None = t_none(),
426  %% Call-site analysis may be inaccurate and consider more funs than those that
427  %% are actually possible. If all of them are incorrect, then warnings can be
428  %% emitted. If at least one fun is ok, however, then no warning is emitted,
429  %% just in case the bad ones are not really possible. The last argument is
430  %% used for this, with the following encoding:
431  %%   Initial value: {none, []}
432  %%   First fun checked: {one, <List of warns>}
433  %%   More funs checked: {many, <List of warns>}
434  %% A '{one, []}' can only become '{many, []}'.
435  %% If at any point an fun does not add warnings, then the list is also
436  %% replaced with an empty list.
437  handle_apply_or_call(FunInfoList, Args, ArgTypes, Map, Tree, State,
438		       [None || _ <- ArgTypes], None, false, {none, []}).
439
440handle_apply_or_call([{local, external}|Left], Args, ArgTypes, Map, Tree, State,
441		     _AccArgTypes, _AccRet, _HadExternal, Warns) ->
442  {HowMany, _} = Warns,
443  NewHowMany =
444    case HowMany of
445      none -> one;
446      _ -> many
447    end,
448  NewWarns = {NewHowMany, []},
449  handle_apply_or_call(Left, Args, ArgTypes, Map, Tree, State,
450		       ArgTypes, t_any(), true, NewWarns);
451handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left],
452		     Args, ArgTypes, Map, Tree,
453                     #state{opaques = Opaques} = State,
454                     AccArgTypes, AccRet, HadExternal, Warns) ->
455  Any = t_any(),
456  AnyArgs = [Any || _ <- Args],
457  GenSig = {AnyArgs, fun(_) -> t_any() end},
458  {CArgs, CRange} =
459    case Contr of
460      {value, #contract{args = As} = C} ->
461	{As, fun(FunArgs) ->
462		 dialyzer_contracts:get_contract_return(C, FunArgs)
463	     end};
464      none -> GenSig
465    end,
466  {BifArgs, BifRange} =
467    case TypeOfApply of
468      remote ->
469	{M, F, A} = Fun,
470	case erl_bif_types:is_known(M, F, A) of
471	  true ->
472	    BArgs = erl_bif_types:arg_types(M, F, A),
473	    BRange =
474	      fun(FunArgs) ->
475		  erl_bif_types:type(M, F, A, FunArgs, Opaques)
476	      end,
477	    {BArgs, BRange};
478          false ->
479            GenSig
480	end;
481      local -> GenSig
482    end,
483  {SigArgs, SigRange} =
484    case Sig of
485      {value, {SR, SA}} -> {SA, SR};
486      none -> {AnyArgs, t_any()}
487    end,
488
489  ?debug("--------------------------------------------------------\n", []),
490  ?debug("Fun: ~p\n", [state__lookup_name(Fun, State)]),
491  ?debug("Module ~p\n", [State#state.module]),
492  ?debug("CArgs ~s\n", [erl_types:t_to_string(t_product(CArgs))]),
493  ?debug("ArgTypes ~s\n", [erl_types:t_to_string(t_product(ArgTypes))]),
494  ?debug("BifArgs ~p\n", [erl_types:t_to_string(t_product(BifArgs))]),
495
496  NewArgsSig = t_inf_lists(SigArgs, ArgTypes, Opaques),
497  ?debug("SigArgs ~s\n", [erl_types:t_to_string(t_product(SigArgs))]),
498  ?debug("NewArgsSig: ~s\n", [erl_types:t_to_string(t_product(NewArgsSig))]),
499  NewArgsContract = t_inf_lists(CArgs, ArgTypes, Opaques),
500  ?debug("NewArgsContract: ~s\n",
501	 [erl_types:t_to_string(t_product(NewArgsContract))]),
502  NewArgsBif = t_inf_lists(BifArgs, ArgTypes, Opaques),
503  ?debug("NewArgsBif: ~s\n", [erl_types:t_to_string(t_product(NewArgsBif))]),
504  NewArgTypes0 = t_inf_lists(NewArgsSig, NewArgsContract),
505  NewArgTypes = t_inf_lists(NewArgTypes0, NewArgsBif, Opaques),
506  ?debug("NewArgTypes ~s\n", [erl_types:t_to_string(t_product(NewArgTypes))]),
507  ?debug("\n", []),
508
509  BifRet = BifRange(NewArgTypes),
510  ContrRet = CRange(NewArgTypes),
511  RetWithoutContr = t_inf(SigRange, BifRet),
512  RetWithoutLocal = t_inf(ContrRet, RetWithoutContr),
513
514  ?debug("RetWithoutContr: ~s\n",[erl_types:t_to_string(RetWithoutContr)]),
515  ?debug("RetWithoutLocal: ~s\n", [erl_types:t_to_string(RetWithoutLocal)]),
516  ?debug("BifRet: ~s\n", [erl_types:t_to_string(BifRange(NewArgTypes))]),
517  ?debug("SigRange: ~s\n", [erl_types:t_to_string(SigRange)]),
518  ?debug("ContrRet: ~s\n", [erl_types:t_to_string(ContrRet)]),
519  ?debug("LocalRet: ~s\n", [erl_types:t_to_string(LocalRet)]),
520
521  State1 =
522    case is_race_analysis_enabled(State) of
523      true ->
524        Ann = cerl:get_ann(Tree),
525        File = get_file(Ann),
526        Line = abs(get_line(Ann)),
527        dialyzer_races:store_race_call(Fun, ArgTypes, Args,
528                                       {File, Line}, State);
529      false -> State
530    end,
531  FailedConj = any_none([RetWithoutLocal|NewArgTypes]),
532  IsFailBif = t_is_none(BifRange(BifArgs)),
533  IsFailSig = t_is_none(SigRange),
534  ?debug("FailedConj: ~p~n", [FailedConj]),
535  ?debug("IsFailBif: ~p~n", [IsFailBif]),
536  ?debug("IsFailSig: ~p~n", [IsFailSig]),
537  State2 =
538    case FailedConj andalso not (IsFailBif orelse IsFailSig) of
539      true ->
540	case t_is_none(RetWithoutLocal) andalso
541	  not t_is_none(RetWithoutContr) andalso
542	  not any_none(NewArgTypes) of
543	  true ->
544	    {value, C1} = Contr,
545	    Contract = dialyzer_contracts:contract_to_string(C1),
546	    {M1, F1, A1} = state__lookup_name(Fun, State),
547	    ArgStrings = format_args(Args, ArgTypes, State),
548	    CRet = erl_types:t_to_string(RetWithoutContr),
549	    %% This Msg will be post_processed by dialyzer_succ_typings
550	    Msg =
551	      {contract_range, [Contract, M1, F1, A1, ArgStrings, CRet]},
552	    state__add_warning(State1, ?WARN_CONTRACT_RANGE, Tree, Msg);
553	  false ->
554	    FailedSig = any_none(NewArgsSig),
555	    FailedContract =
556	      any_none([CRange(NewArgsContract)|NewArgsContract]),
557	    FailedBif = any_none([BifRange(NewArgsBif)|NewArgsBif]),
558	    InfSig = t_inf(t_fun(SigArgs, SigRange),
559                           t_fun(BifArgs, BifRange(BifArgs))),
560	    FailReason =
561	      apply_fail_reason(FailedSig, FailedBif, FailedContract),
562	    Msg = get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes, InfSig,
563				     Contr, CArgs, State1, FailReason, Opaques),
564	    WarnType = case Msg of
565			 {call, _} -> ?WARN_FAILING_CALL;
566			 {apply, _} -> ?WARN_FAILING_CALL;
567			 {call_with_opaque, _} -> ?WARN_OPAQUE;
568			 {call_without_opaque, _} -> ?WARN_OPAQUE;
569			 {opaque_type_test, _} -> ?WARN_OPAQUE
570		       end,
571            Frc = {erlang, is_record, 3} =:= state__lookup_name(Fun, State),
572	    state__add_warning(State1, WarnType, Tree, Msg, Frc)
573	end;
574      false -> State1
575    end,
576  State3 =
577    case TypeOfApply of
578      local ->
579        case state__is_escaping(Fun, State2) of
580          true -> State2;
581          false ->
582            ForwardArgs = [t_limit(X, ?TYPE_LIMIT) || X <- ArgTypes],
583            forward_args(Fun, ForwardArgs, State2)
584        end;
585      remote ->
586        add_bif_warnings(Fun, NewArgTypes, Tree, State2)
587    end,
588  NewAccArgTypes =
589    case FailedConj of
590      true -> AccArgTypes;
591      false -> [t_sup(X, Y) || {X, Y} <- lists:zip(NewArgTypes, AccArgTypes)]
592    end,
593  TotalRet =
594    case t_is_none(LocalRet) andalso t_is_unit(RetWithoutLocal) of
595      true -> RetWithoutLocal;
596      false -> t_inf(RetWithoutLocal, LocalRet)
597    end,
598  NewAccRet = t_sup(AccRet, TotalRet),
599  ?debug("NewAccRet: ~s\n", [t_to_string(NewAccRet)]),
600  {NewWarnings, State4} = state__remove_added_warnings(State, State3),
601  {HowMany, OldWarnings} = Warns,
602  NewWarns =
603    case HowMany of
604      none -> {one, NewWarnings};
605      _ ->
606        case OldWarnings =:= [] of
607          true -> {many, []};
608          false ->
609            case NewWarnings =:= [] of
610              true -> {many, []};
611              false -> {many, NewWarnings ++ OldWarnings}
612            end
613        end
614    end,
615  handle_apply_or_call(Left, Args, ArgTypes, Map, Tree,
616		       State4, NewAccArgTypes, NewAccRet, HadExternal, NewWarns);
617handle_apply_or_call([], Args, _ArgTypes, Map, _Tree, State,
618		     AccArgTypes, AccRet, HadExternal, {_, Warnings}) ->
619  State1 = state__add_warnings(Warnings, State),
620  case HadExternal of
621    false ->
622      NewMap = enter_type_lists(Args, AccArgTypes, Map),
623      {State1, NewMap, AccRet};
624    true ->
625      {had_external, State1}
626  end.
627
628apply_fail_reason(FailedSig, FailedBif, FailedContract) ->
629  if
630    (FailedSig orelse FailedBif) andalso (not FailedContract) -> only_sig;
631    FailedContract andalso (not (FailedSig orelse FailedBif)) -> only_contract;
632    true                                                      -> both
633  end.
634
635get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes,
636		   Sig, Contract, ContrArgs, State, FailReason, Opaques) ->
637  ArgStrings = format_args(Args, ArgTypes, State),
638  ContractInfo =
639    case Contract of
640      {value, #contract{} = C} ->
641	{dialyzer_contracts:is_overloaded(C),
642	 dialyzer_contracts:contract_to_string(C)};
643      none -> {false, none}
644    end,
645  EnumArgTypes = lists:zip(lists:seq(1, length(NewArgTypes)), NewArgTypes),
646  ArgNs = [Arg || {Arg, Type} <- EnumArgTypes, t_is_none(Type)],
647  case state__lookup_name(Fun, State) of
648    {M, F, A} ->
649      case is_opaque_type_test_problem(Fun, Args, NewArgTypes, State) of
650	{yes, Arg, ArgType} ->
651	  {opaque_type_test, [atom_to_list(F), ArgStrings,
652                              format_arg(Arg), format_type(ArgType, State)]};
653	no ->
654	  SigArgs = t_fun_args(Sig),
655          BadOpaque =
656            opaque_problems([SigArgs, ContrArgs], ArgTypes, Opaques, ArgNs),
657          %% In fact *both* 'call_with_opaque' and
658          %% 'call_without_opaque' are possible.
659          case lists:keyfind(decl, 1, BadOpaque) of
660            {decl, BadArgs} ->
661              %% a structured term is used where an opaque is expected
662              ExpectedTriples =
663                case FailReason of
664                  only_sig -> expected_arg_triples(BadArgs, SigArgs, State);
665                  _ -> expected_arg_triples(BadArgs, ContrArgs, State)
666                end,
667              {call_without_opaque, [M, F, ArgStrings, ExpectedTriples]};
668            false ->
669              case lists:keyfind(use, 1, BadOpaque) of
670                {use, BadArgs} ->
671                  %% an opaque term is used where a structured term is expected
672                  ExpectedArgs =
673                    case FailReason of
674                      only_sig -> SigArgs;
675                      _ -> ContrArgs
676                    end,
677                  {call_with_opaque, [M, F, ArgStrings, BadArgs, ExpectedArgs]};
678                false ->
679                  case
680                    erl_bif_types:opaque_args(M, F, A, ArgTypes, Opaques)
681                  of
682                    [] ->  %% there is a structured term clash in some argument
683                      {call, [M, F, ArgStrings,
684                              ArgNs, FailReason,
685                              format_sig_args(Sig, State),
686                              format_type(t_fun_range(Sig), State),
687                              ContractInfo]};
688                    Ns ->
689                      {call_with_opaque, [M, F, ArgStrings, Ns, ContrArgs]}
690                  end
691	      end
692	  end
693      end;
694    Label when is_integer(Label) ->
695      {apply, [ArgStrings,
696	       ArgNs, FailReason,
697	       format_sig_args(Sig, State),
698	       format_type(t_fun_range(Sig), State),
699	       ContractInfo]}
700  end.
701
702%% -> [{ElementI, [ArgN]}] where [ArgN] is a non-empty list of
703%% arguments containing unknown opaque types and Element is 1 or 2.
704opaque_problems(ContractOrSigList, ArgTypes, Opaques, ArgNs) ->
705  ArgElementList = find_unknown(ContractOrSigList, ArgTypes, Opaques, ArgNs),
706  F = fun(1) -> decl; (2) -> use end,
707  [{F(ElementI), lists:usort([ArgN || {ArgN, EI} <- ArgElementList,
708                                      EI =:= ElementI])} ||
709    ElementI <- lists:usort([EI || {_, EI} <- ArgElementList])].
710
711%% -> [{ArgN, ElementI}] where ElementI = 1 means there is an unknown
712%% opaque type in argument ArgN of the the contract/signature,
713%% and ElementI = 2 means that there is an unknown opaque type in
714%% argument ArgN of the the (current) argument types.
715find_unknown(ContractOrSigList, ArgTypes, Opaques, NoneArgNs) ->
716  ArgNs = lists:seq(1, length(ArgTypes)),
717  [{ArgN, ElementI} ||
718    ContractOrSig <- ContractOrSigList,
719    {E1, E2, ArgN} <- lists:zip3(ContractOrSig, ArgTypes, ArgNs),
720    lists:member(ArgN, NoneArgNs),
721    ElementI <- erl_types:t_find_unknown_opaque(E1, E2, Opaques)].
722
723is_opaque_type_test_problem(Fun, Args, ArgTypes, State) ->
724  case Fun of
725    {erlang, FN, 1} when FN =:= is_atom;      FN =:= is_boolean;
726			 FN =:= is_binary;    FN =:= is_bitstring;
727			 FN =:= is_float;     FN =:= is_function;
728			 FN =:= is_integer;   FN =:= is_list;
729			 FN =:= is_number;    FN =:= is_pid; FN =:= is_port;
730			 FN =:= is_reference; FN =:= is_tuple;
731			 FN =:= is_map ->
732      type_test_opaque_arg(Args, ArgTypes, State#state.opaques);
733    {erlang, FN, 2} when FN =:= is_function ->
734      type_test_opaque_arg(Args, ArgTypes, State#state.opaques);
735    _ -> no
736  end.
737
738type_test_opaque_arg([], [], _Opaques) ->
739  no;
740type_test_opaque_arg([Arg|Args], [ArgType|ArgTypes], Opaques) ->
741  case erl_types:t_has_opaque_subtype(ArgType, Opaques) of
742    true -> {yes, Arg, ArgType};
743    false -> type_test_opaque_arg(Args, ArgTypes, Opaques)
744  end.
745
746expected_arg_triples(ArgNs, ArgTypes, State) ->
747  [begin
748     Arg = lists:nth(N, ArgTypes),
749     {N, Arg, format_type(Arg, State)}
750   end || N <- ArgNs].
751
752add_bif_warnings({erlang, Op, 2}, [T1, T2] = Ts, Tree, State)
753  when Op =:= '=:='; Op =:= '==' ->
754  Opaques = State#state.opaques,
755  Inf = t_inf(T1, T2, Opaques),
756  case
757    t_is_none(Inf) andalso (not any_none(Ts))
758    andalso (not is_int_float_eq_comp(T1, Op, T2, Opaques))
759  of
760    true ->
761      %% Give priority to opaque warning (as usual).
762      case erl_types:t_find_unknown_opaque(T1, T2, Opaques) of
763        [] ->
764          Args = comp_format_args([], T1, Op, T2, State),
765          state__add_warning(State, ?WARN_MATCHING, Tree, {exact_eq, Args});
766        Ns ->
767          Args = comp_format_args(Ns, T1, Op, T2, State),
768	  state__add_warning(State, ?WARN_OPAQUE, Tree, {opaque_eq, Args})
769      end;
770    false ->
771      State
772  end;
773add_bif_warnings({erlang, Op, 2}, [T1, T2] = Ts, Tree, State)
774  when Op =:= '=/='; Op =:= '/=' ->
775  Opaques = State#state.opaques,
776  case
777    (not any_none(Ts))
778    andalso (not is_int_float_eq_comp(T1, Op, T2, Opaques))
779  of
780    true ->
781      case erl_types:t_find_unknown_opaque(T1, T2, Opaques) of
782        [] -> State;
783        Ns ->
784          Args = comp_format_args(Ns, T1, Op, T2, State),
785	  state__add_warning(State, ?WARN_OPAQUE, Tree, {opaque_neq, Args})
786      end;
787    false ->
788      State
789  end;
790add_bif_warnings(_, _, _, State) ->
791  State.
792
793is_int_float_eq_comp(T1, Op, T2, Opaques) ->
794  (Op =:= '==' orelse Op =:= '/=') andalso
795    ((erl_types:t_is_float(T1, Opaques)
796      andalso t_is_integer(T2, Opaques)) orelse
797     (t_is_integer(T1, Opaques)
798      andalso erl_types:t_is_float(T2, Opaques))).
799
800comp_format_args([1|_], T1, Op, T2, State) ->
801  [format_type(T2, State), Op, format_type(T1, State)];
802comp_format_args(_, T1, Op, T2, State) ->
803  [format_type(T1, State), Op, format_type(T2, State)].
804
805%%----------------------------------------
806
807handle_bitstr(Tree, Map, State) ->
808  %% Construction of binaries.
809  Size = cerl:bitstr_size(Tree),
810  Val = cerl:bitstr_val(Tree),
811  BitstrType = cerl:concrete(cerl:bitstr_type(Tree)),
812  {State1, Map1, SizeType0} = traverse(Size, Map, State),
813  {State2, Map2, ValType0} = traverse(Val, Map1, State1),
814  case cerl:bitstr_bitsize(Tree) of
815    BitSz when BitSz =:= all orelse BitSz =:= utf ->
816      ValType =
817	case BitSz of
818	  all ->
819	    true = (BitstrType =:= binary),
820	    t_inf(ValType0, t_bitstr());
821	  utf ->
822	    true = lists:member(BitstrType, [utf8, utf16, utf32]),
823	    t_inf(ValType0, t_integer())
824	end,
825      Map3 = enter_type(Val, ValType, Map2),
826      case t_is_none(ValType) of
827	true ->
828	  Msg = {bin_construction, ["value",
829				    format_cerl(Val), format_cerl(Tree),
830				    format_type(ValType0, State2)]},
831	  State3 = state__add_warning(State2, ?WARN_BIN_CONSTRUCTION, Val, Msg),
832	  {State3, Map3, t_none()};
833	false ->
834	  {State2, Map3, t_bitstr()}
835      end;
836    BitSz when is_integer(BitSz) orelse BitSz =:= any ->
837      SizeType = t_inf(SizeType0, t_non_neg_integer()),
838      ValType =
839	case BitstrType of
840	  binary -> t_inf(ValType0, t_bitstr());
841	  float -> t_inf(ValType0, t_number());
842	  integer -> t_inf(ValType0, t_integer())
843	end,
844      case any_none([SizeType, ValType]) of
845	true ->
846	  {Msg, Offending} =
847	    case t_is_none(SizeType) of
848	      true ->
849		{{bin_construction,
850		  ["size", format_cerl(Size), format_cerl(Tree),
851		   format_type(SizeType0, State2)]},
852		 Size};
853	      false ->
854		{{bin_construction,
855		  ["value", format_cerl(Val), format_cerl(Tree),
856		   format_type(ValType0, State2)]},
857		 Val}
858	    end,
859	  State3 = state__add_warning(State2, ?WARN_BIN_CONSTRUCTION,
860				      Offending, Msg),
861	  {State3, Map2, t_none()};
862	false ->
863	  UnitVal = cerl:concrete(cerl:bitstr_unit(Tree)),
864          Opaques = State2#state.opaques,
865          NumberVals = t_number_vals(SizeType, Opaques),
866          {State3, Type} =
867            case t_contains_opaque(SizeType, Opaques) of
868              true ->
869                Msg = {opaque_size, [format_type(SizeType, State2),
870                                     format_cerl(Size)]},
871                {state__add_warning(State2, ?WARN_OPAQUE, Size, Msg),
872                 t_none()};
873              false ->
874                case NumberVals of
875                  [OneSize] -> {State2, t_bitstr(0, OneSize * UnitVal)};
876                  unknown -> {State2, t_bitstr()};
877                  _ ->
878                    MinSize = erl_types:number_min(SizeType, Opaques),
879                    {State2, t_bitstr(UnitVal, UnitVal * MinSize)}
880                end
881            end,
882	  Map3 = enter_type_lists([Val, Size, Tree],
883				  [ValType, SizeType, Type], Map2),
884	  {State3, Map3, Type}
885      end
886  end.
887
888%%----------------------------------------
889
890handle_call(Tree, Map, State) ->
891  M = cerl:call_module(Tree),
892  F = cerl:call_name(Tree),
893  Args = cerl:call_args(Tree),
894  MFAList = [M, F|Args],
895  {State1, Map1, [MType0, FType0|As]} = traverse_list(MFAList, Map, State),
896  Opaques = State#state.opaques,
897  MType = t_inf(t_module(), MType0, Opaques),
898  FType = t_inf(t_atom(), FType0, Opaques),
899  Map2 = enter_type_lists([M, F], [MType, FType], Map1),
900  MOpaque = t_is_none(MType) andalso (not t_is_none(MType0)),
901  FOpaque = t_is_none(FType) andalso (not t_is_none(FType0)),
902  case any_none([MType, FType|As]) of
903    true ->
904      State2 =
905        if
906          MOpaque -> % This is a problem we just detected; not a known one
907            MS = format_cerl(M),
908            case t_is_none(t_inf(t_module(), MType0)) of
909              true ->
910                Msg = {app_call, [MS, format_cerl(F),
911                                  format_args(Args, As, State1),
912                                  MS, format_type(t_module(), State1),
913                                  format_type(MType0, State1)]},
914                state__add_warning(State1, ?WARN_FAILING_CALL, Tree, Msg);
915              false ->
916                Msg = {opaque_call, [MS, format_cerl(F),
917                                     format_args(Args, As, State1),
918                                     MS, format_type(MType0, State1)]},
919                state__add_warning(State1, ?WARN_FAILING_CALL, Tree, Msg)
920            end;
921          FOpaque ->
922            FS = format_cerl(F),
923            case t_is_none(t_inf(t_atom(), FType0)) of
924              true ->
925                Msg = {app_call, [format_cerl(M), FS,
926                                  format_args(Args, As, State1),
927                                  FS, format_type(t_atom(), State1),
928                                  format_type(FType0, State1)]},
929                state__add_warning(State1, ?WARN_FAILING_CALL, Tree, Msg);
930              false ->
931                Msg = {opaque_call, [format_cerl(M), FS,
932                                     format_args(Args, As, State1),
933                                     FS, format_type(FType0, State1)]},
934                state__add_warning(State1, ?WARN_FAILING_CALL, Tree, Msg)
935            end;
936          true -> State1
937	end,
938      {State2, Map2, t_none()};
939    false ->
940      case t_is_atom(MType) of
941	true ->
942	  %% XXX: Consider doing this for all combinations of MF
943	  case {t_atom_vals(MType), t_atom_vals(FType)} of
944	    {[MAtom], [FAtom]} ->
945	      FunInfo = [{remote, state__fun_info({MAtom, FAtom, length(Args)},
946						  State1)}],
947	      handle_apply_or_call(FunInfo, Args, As, Map2, Tree, State1);
948	    {_MAtoms, _FAtoms} ->
949	      {State1, Map2, t_any()}
950	  end;
951	false ->
952	  {State1, Map2, t_any()}
953      end
954  end.
955
956%%----------------------------------------
957
958handle_case(Tree, Map, State) ->
959  Arg = cerl:case_arg(Tree),
960  Clauses = filter_match_fail(cerl:case_clauses(Tree)),
961  {State1, Map1, ArgType} = SMA = traverse(Arg, Map, State),
962  case t_is_none_or_unit(ArgType) of
963    true -> SMA;
964    false ->
965      State2 =
966        case is_race_analysis_enabled(State) of
967          true ->
968	    {RaceList, RaceListSize} = get_race_list_and_size(State1),
969            state__renew_race_list([beg_case|RaceList],
970                                   RaceListSize + 1, State1);
971          false -> State1
972        end,
973      Map2 = join_maps_begin(Map1),
974      {MapList, State3, Type} =
975	handle_clauses(Clauses, Arg, ArgType, ArgType, State2,
976		       [], Map2, [], []),
977      Map3 = join_maps_end(MapList, Map2),
978      debug_pp_map(Map3),
979      {State3, Map3, Type}
980  end.
981
982%%----------------------------------------
983
984handle_cons(Tree, Map, State) ->
985  Hd = cerl:cons_hd(Tree),
986  Tl = cerl:cons_tl(Tree),
987  {State1, Map1, HdType} = traverse(Hd, Map, State),
988  {State2, Map2, TlType} = traverse(Tl, Map1, State1),
989  State3 =
990    case t_is_none(t_inf(TlType, t_list(), State2#state.opaques)) of
991      true ->
992	Msg = {improper_list_constr, [format_type(TlType, State2)]},
993	state__add_warning(State2, ?WARN_NON_PROPER_LIST, Tree, Msg);
994      false ->
995	State2
996    end,
997  Type = t_cons(HdType, TlType),
998  {State3, Map2, Type}.
999
1000%%----------------------------------------
1001
1002handle_let(Tree, Map, State) ->
1003  IsRaceAnalysisEnabled = is_race_analysis_enabled(State),
1004  Arg = cerl:let_arg(Tree),
1005  Vars = cerl:let_vars(Tree),
1006  {Map0, State0} =
1007    case cerl:is_c_var(Arg) of
1008      true ->
1009	[Var] = Vars,
1010	{enter_subst(Var, Arg, Map),
1011         case IsRaceAnalysisEnabled of
1012           true ->
1013	    {RaceList, RaceListSize} = get_race_list_and_size(State),
1014             state__renew_race_list(
1015               [dialyzer_races:let_tag_new(Var, Arg)|RaceList],
1016               RaceListSize + 1, State);
1017           false -> State
1018         end};
1019      false -> {Map, State}
1020    end,
1021  Body = cerl:let_body(Tree),
1022  {State1, Map1, ArgTypes} = SMA = traverse(Arg, Map0, State0),
1023  State2 =
1024    case IsRaceAnalysisEnabled andalso cerl:is_c_call(Arg) of
1025      true ->
1026        Mod = cerl:call_module(Arg),
1027        Name = cerl:call_name(Arg),
1028        case cerl:is_literal(Mod) andalso
1029             cerl:concrete(Mod) =:= ets andalso
1030             cerl:is_literal(Name) andalso
1031             cerl:concrete(Name) =:= new of
1032          true -> renew_race_public_tables(Vars, State1);
1033          false -> State1
1034        end;
1035      false -> State1
1036    end,
1037  case t_is_none_or_unit(ArgTypes) of
1038    true -> SMA;
1039    false ->
1040      Map2 = enter_type_lists(Vars, t_to_tlist(ArgTypes), Map1),
1041      traverse(Body, Map2, State2)
1042  end.
1043
1044%%----------------------------------------
1045
1046handle_module(Tree, Map, State) ->
1047  %% By not including the variables in scope we can assure that we
1048  %% will get the current function type when using the variables.
1049  Defs = cerl:module_defs(Tree),
1050  PartFun = fun({_Var, Fun}) ->
1051		state__is_escaping(get_label(Fun), State)
1052	    end,
1053  {Defs1, Defs2} = lists:partition(PartFun, Defs),
1054  Letrec = cerl:c_letrec(Defs1, cerl:c_int(42)),
1055  {State1, Map1, _FunTypes} = traverse(Letrec, Map, State),
1056  %% Also add environments for the other top-level functions.
1057  VarTypes = [{Var, state__fun_type(Fun, State1)} || {Var, Fun} <- Defs],
1058  EnvMap = enter_type_list(VarTypes, Map),
1059  FoldFun = fun({_Var, Fun}, AccState) ->
1060		state__update_fun_env(Fun, EnvMap, AccState)
1061	    end,
1062  State2 = lists:foldl(FoldFun, State1, Defs2),
1063  {State2, Map1, t_any()}.
1064
1065%%----------------------------------------
1066
1067handle_receive(Tree, Map, State) ->
1068  Clauses = filter_match_fail(cerl:receive_clauses(Tree)),
1069  Timeout = cerl:receive_timeout(Tree),
1070  State1 =
1071    case is_race_analysis_enabled(State) of
1072      true ->
1073	{RaceList, RaceListSize} = get_race_list_and_size(State),
1074        state__renew_race_list([beg_case|RaceList],
1075                               RaceListSize + 1, State);
1076      false -> State
1077    end,
1078  {MapList, State2, ReceiveType} =
1079    handle_clauses(Clauses, ?no_arg, t_any(), t_any(), State1, [], Map,
1080                   [], []),
1081  Map1 = join_maps(MapList, Map),
1082  {State3, Map2, TimeoutType} = traverse(Timeout, Map1, State2),
1083  Opaques = State3#state.opaques,
1084  case (t_is_atom(TimeoutType, Opaques) andalso
1085	(t_atom_vals(TimeoutType, Opaques) =:= ['infinity'])) of
1086    true ->
1087      {State3, Map2, ReceiveType};
1088    false ->
1089      Action = cerl:receive_action(Tree),
1090      {State4, Map3, ActionType} = traverse(Action, Map, State3),
1091      Map4 = join_maps([Map3, Map1], Map),
1092      Type = t_sup(ReceiveType, ActionType),
1093      {State4, Map4, Type}
1094  end.
1095
1096%%----------------------------------------
1097
1098handle_try(Tree, Map, State) ->
1099  Arg = cerl:try_arg(Tree),
1100  EVars = cerl:try_evars(Tree),
1101  Vars = cerl:try_vars(Tree),
1102  Body = cerl:try_body(Tree),
1103  Handler = cerl:try_handler(Tree),
1104  {State1, Map1, ArgType} = traverse(Arg, Map, State),
1105  Map2 = mark_as_fresh(Vars, Map1),
1106  {SuccState, SuccMap, SuccType} =
1107    case bind_pat_vars(Vars, t_to_tlist(ArgType), [], Map2, State1) of
1108      {error, _, _, _, _} ->
1109	{State1, map__new(), t_none()};
1110      {SuccMap1, VarTypes} ->
1111	%% Try to bind the argument. Will only succeed if
1112	%% it is a simple structured term.
1113	SuccMap2 =
1114	  case bind_pat_vars_reverse([Arg], [t_product(VarTypes)], [],
1115				     SuccMap1, State1) of
1116	    {error, _, _, _, _} -> SuccMap1;
1117	    {SM, _} -> SM
1118	  end,
1119	traverse(Body, SuccMap2, State1)
1120    end,
1121  ExcMap1 = mark_as_fresh(EVars, Map),
1122  {State2, ExcMap2, HandlerType} = traverse(Handler, ExcMap1, SuccState),
1123  TryType = t_sup(SuccType, HandlerType),
1124  {State2, join_maps([ExcMap2, SuccMap], Map1), TryType}.
1125
1126%%----------------------------------------
1127
1128handle_map(Tree,Map,State) ->
1129  Pairs = cerl:map_es(Tree),
1130  Arg = cerl:map_arg(Tree),
1131  {State1, Map1, ArgType} = traverse(Arg, Map, State),
1132  ArgType1 = t_inf(t_map(), ArgType),
1133  case t_is_none_or_unit(ArgType1) of
1134    true ->
1135      {State1, Map1, ArgType1};
1136    false ->
1137      {State2, Map2, TypePairs, ExactKeys} =
1138	traverse_map_pairs(Pairs, Map1, State1, t_none(), [], []),
1139      InsertPair = fun({KV,assoc,_},Acc) -> erl_types:t_map_put(KV,Acc);
1140		      ({KV,exact,KVTree},Acc) ->
1141		       case t_is_none(T=erl_types:t_map_update(KV,Acc)) of
1142			 true -> throw({none, Acc, KV, KVTree});
1143			 false -> T
1144		       end
1145		   end,
1146      try lists:foldl(InsertPair, ArgType1, TypePairs)
1147      of ResT ->
1148	  BindT = t_map([{K, t_any()} || K <- ExactKeys]),
1149	  case bind_pat_vars_reverse([Arg], [BindT], [], Map2, State2) of
1150	    {error, _, _, _, _} -> {State2, Map2, ResT};
1151	    {Map3, _} ->           {State2, Map3, ResT}
1152	  end
1153      catch {none, MapType, {K,_}, KVTree} ->
1154	  Msg2 = {map_update, [format_type(MapType, State2),
1155			       format_type(K, State2)]},
1156	  {state__add_warning(State2, ?WARN_MAP_CONSTRUCTION, KVTree, Msg2),
1157	   Map2, t_none()}
1158      end
1159  end.
1160
1161traverse_map_pairs([], Map, State, _ShadowKeys, PairAcc, KeyAcc) ->
1162  {State, Map, lists:reverse(PairAcc), KeyAcc};
1163traverse_map_pairs([Pair|Pairs], Map, State, ShadowKeys, PairAcc, KeyAcc) ->
1164  Key = cerl:map_pair_key(Pair),
1165  Val = cerl:map_pair_val(Pair),
1166  Op = cerl:map_pair_op(Pair),
1167  {State1, Map1, [K,V]} = traverse_list([Key,Val],Map,State),
1168  KeyAcc1 =
1169    case cerl:is_literal(Op) andalso cerl:concrete(Op) =:= exact andalso
1170      t_is_singleton(K, State#state.opaques) andalso
1171      t_is_none(t_inf(ShadowKeys, K)) of
1172      true -> [K|KeyAcc];
1173      false -> KeyAcc
1174  end,
1175  traverse_map_pairs(Pairs, Map1, State1, t_sup(K, ShadowKeys),
1176		     [{{K,V},cerl:concrete(Op),Pair}|PairAcc], KeyAcc1).
1177
1178%%----------------------------------------
1179
1180handle_tuple(Tree, Map, State) ->
1181  Elements = cerl:tuple_es(Tree),
1182  {State1, Map1, EsType} = traverse_list(Elements, Map, State),
1183  TupleType = t_tuple(EsType),
1184  case t_is_none(TupleType) of
1185    true ->
1186      {State1, Map1, t_none()};
1187    false ->
1188      %% Let's find out if this is a record
1189      case Elements of
1190	[Tag|Left] ->
1191	  case cerl:is_c_atom(Tag) andalso is_literal_record(Tree) of
1192	    true ->
1193	      TagVal = cerl:atom_val(Tag),
1194              case state__lookup_record(TagVal, length(Left), State1) of
1195                error -> {State1, Map1, TupleType};
1196                {ok, RecType} ->
1197                  InfTupleType = t_inf(RecType, TupleType),
1198                  case t_is_none(InfTupleType) of
1199                    true ->
1200                      RecC = format_type(TupleType, State1),
1201                      FieldDiffs = format_field_diffs(TupleType, State1),
1202                      Msg = {record_constr, [RecC, FieldDiffs]},
1203                      State2 = state__add_warning(State1, ?WARN_MATCHING,
1204                                                  Tree, Msg),
1205                      {State2, Map1, t_none()};
1206                    false ->
1207                      case bind_pat_vars(Elements, t_tuple_args(RecType),
1208                                         [], Map1, State1) of
1209                        {error, bind, ErrorPat, ErrorType, _} ->
1210                          Msg = {record_constr,
1211                                 [TagVal, format_patterns(ErrorPat),
1212                                  format_type(ErrorType, State1)]},
1213                          State2 = state__add_warning(State1, ?WARN_MATCHING,
1214                                                      Tree, Msg),
1215                          {State2, Map1, t_none()};
1216                        {error, opaque, ErrorPat, ErrorType, OpaqueType} ->
1217                          Msg = {opaque_match,
1218                                 [format_patterns(ErrorPat),
1219                                  format_type(ErrorType, State1),
1220                                  format_type(OpaqueType, State1)]},
1221                          State2 = state__add_warning(State1, ?WARN_OPAQUE,
1222                                                      Tree, Msg),
1223                          {State2, Map1, t_none()};
1224                        {Map2, ETypes} ->
1225                          {State1, Map2, t_tuple(ETypes)}
1226                      end
1227                  end
1228	      end;
1229	    false ->
1230	      {State1, Map1, t_tuple(EsType)}
1231	  end;
1232	[] ->
1233	  {State1, Map1, t_tuple([])}
1234      end
1235  end.
1236
1237%%----------------------------------------
1238%% Clauses
1239%%
1240handle_clauses([C|Left], Arg, ArgType, OrigArgType, State, CaseTypes, MapIn,
1241	       Acc, ClauseAcc) ->
1242  IsRaceAnalysisEnabled = is_race_analysis_enabled(State),
1243  State1 =
1244    case IsRaceAnalysisEnabled of
1245      true ->
1246	{RaceList, RaceListSize} = get_race_list_and_size(State),
1247        state__renew_race_list(
1248          [dialyzer_races:beg_clause_new(Arg, cerl:clause_pats(C),
1249                                         cerl:clause_guard(C))|
1250           RaceList], RaceListSize + 1,
1251          State);
1252      false -> State
1253    end,
1254  {State2, ClauseMap, BodyType, NewArgType} =
1255    do_clause(C, Arg, ArgType, OrigArgType, MapIn, State1),
1256  {NewClauseAcc, State3} =
1257    case IsRaceAnalysisEnabled of
1258      true ->
1259	{RaceList1, RaceListSize1} = get_race_list_and_size(State2),
1260        EndClause = dialyzer_races:end_clause_new(Arg, cerl:clause_pats(C),
1261                                                  cerl:clause_guard(C)),
1262        {[EndClause|ClauseAcc],
1263         state__renew_race_list([EndClause|RaceList1],
1264                                RaceListSize1 + 1, State2)};
1265      false -> {ClauseAcc, State2}
1266    end,
1267  {NewCaseTypes, NewAcc} =
1268    case t_is_none(BodyType) of
1269      true -> {CaseTypes, Acc};
1270      false -> {[BodyType|CaseTypes], [ClauseMap|Acc]}
1271    end,
1272  handle_clauses(Left, Arg, NewArgType, OrigArgType, State3,
1273                 NewCaseTypes, MapIn, NewAcc, NewClauseAcc);
1274handle_clauses([], _Arg, _ArgType, _OrigArgType, State, CaseTypes, _MapIn, Acc,
1275	       ClauseAcc) ->
1276  State1 =
1277    case is_race_analysis_enabled(State) of
1278      true ->
1279	{RaceList, RaceListSize} = get_race_list_and_size(State),
1280        state__renew_race_list(
1281          [dialyzer_races:end_case_new(ClauseAcc)|RaceList],
1282	  RaceListSize + 1, State);
1283      false -> State
1284    end,
1285  {lists:reverse(Acc), State1, t_sup(CaseTypes)}.
1286
1287do_clause(C, Arg, ArgType0, OrigArgType, Map, State) ->
1288  Pats = cerl:clause_pats(C),
1289  Guard = cerl:clause_guard(C),
1290  Body = cerl:clause_body(C),
1291  State1 =
1292    case is_race_analysis_enabled(State) of
1293      true ->
1294        state__renew_fun_args(Pats, State);
1295      false -> State
1296    end,
1297  Map0 = mark_as_fresh(Pats, Map),
1298  Map1 = if Arg =:= ?no_arg -> Map0;
1299	    true -> bind_subst(Arg, Pats, Map0)
1300	 end,
1301  BindRes =
1302    case t_is_none(ArgType0) of
1303      true ->
1304	{error, bind, Pats, ArgType0, ArgType0};
1305      false ->
1306	ArgTypes =
1307	  case t_is_any(ArgType0) of
1308	    true -> [ArgType0 || _ <- Pats];
1309	    false -> t_to_tlist(ArgType0)
1310	  end,
1311	bind_pat_vars(Pats, ArgTypes, [], Map1, State1)
1312    end,
1313  case BindRes of
1314    {error, ErrorType, NewPats, Type, OpaqueTerm} ->
1315      ?debug("Failed binding pattern: ~s\nto ~s\n",
1316	     [cerl_prettypr:format(C), format_type(ArgType0, State1)]),
1317      case state__warning_mode(State1) of
1318        false ->
1319          {State1, Map, t_none(), ArgType0};
1320	true ->
1321	  {Msg, Force} =
1322	    case t_is_none(ArgType0) of
1323	      true ->
1324                PatString = format_patterns(Pats),
1325		PatTypes = [PatString, format_type(OrigArgType, State1)],
1326		%% See if this is covered by an earlier clause or if it
1327		%% simply cannot match
1328		OrigArgTypes =
1329		  case t_is_any(OrigArgType) of
1330		    true -> Any = t_any(), [Any || _ <- Pats];
1331		    false -> t_to_tlist(OrigArgType)
1332		  end,
1333		Tag =
1334		  case bind_pat_vars(Pats, OrigArgTypes, [], Map1, State1) of
1335		    {error,   bind, _, _, _} -> pattern_match;
1336		    {error, record, _, _, _} -> record_match;
1337		    {error, opaque, _, _, _} -> opaque_match;
1338		    {_, _} -> pattern_match_cov
1339		  end,
1340		{{Tag, PatTypes}, false};
1341	      false ->
1342		%% Try to find out if this is a default clause in a list
1343		%% comprehension and suppress this. A real Hack(tm)
1344		Force0 =
1345		  case is_compiler_generated(cerl:get_ann(C)) of
1346		    true ->
1347		      case Pats of
1348			[Pat] ->
1349			  case cerl:is_c_cons(Pat) of
1350			    true ->
1351			      not (cerl:is_c_var(cerl:cons_hd(Pat)) andalso
1352				   cerl:is_c_var(cerl:cons_tl(Pat)) andalso
1353				   cerl:is_literal(Guard) andalso
1354				   (cerl:concrete(Guard) =:= true));
1355			    false ->
1356			      true
1357			  end;
1358			[Pat0, Pat1] -> % binary comprehension
1359			  case cerl:is_c_cons(Pat0) of
1360			    true ->
1361			      not (cerl:is_c_var(cerl:cons_hd(Pat0)) andalso
1362				   cerl:is_c_var(cerl:cons_tl(Pat0)) andalso
1363                                   cerl:is_c_var(Pat1) andalso
1364				   cerl:is_literal(Guard) andalso
1365				   (cerl:concrete(Guard) =:= true));
1366			    false ->
1367			      true
1368			  end;
1369			_ -> true
1370		      end;
1371		    false ->
1372		      true
1373		  end,
1374                PatString =
1375                  case ErrorType of
1376                    bind   -> format_patterns(Pats);
1377                    record -> format_patterns(NewPats);
1378                    opaque -> format_patterns(NewPats)
1379                  end,
1380		PatTypes = case ErrorType of
1381			     bind -> [PatString, format_type(ArgType0, State1)];
1382			     record -> [PatString, format_type(Type, State1)];
1383			     opaque -> [PatString, format_type(Type, State1),
1384					format_type(OpaqueTerm, State1)]
1385			   end,
1386		FailedTag = case ErrorType of
1387			      bind  -> pattern_match;
1388			      record -> record_match;
1389			      opaque -> opaque_match
1390			    end,
1391		{{FailedTag, PatTypes}, Force0}
1392	    end,
1393	  WarnType = case Msg of
1394		       {opaque_match, _} -> ?WARN_OPAQUE;
1395		       {pattern_match, _} -> ?WARN_MATCHING;
1396		       {record_match, _} -> ?WARN_MATCHING;
1397		       {pattern_match_cov, _} -> ?WARN_MATCHING
1398		     end,
1399          {state__add_warning(State1, WarnType, C, Msg, Force),
1400           Map, t_none(), ArgType0}
1401      end;
1402    {Map2, PatTypes} ->
1403      Map3 =
1404	case Arg =:= ?no_arg of
1405	  true -> Map2;
1406	  false ->
1407	    %% Try to bind the argument. Will only succeed if
1408	    %% it is a simple structured term.
1409	    case bind_pat_vars_reverse([Arg], [t_product(PatTypes)],
1410				       [], Map2, State1) of
1411	      {error, _, _, _, _} -> Map2;
1412	      {NewMap, _} -> NewMap
1413	    end
1414	end,
1415      NewArgType =
1416	case Arg =:= ?no_arg of
1417	  true -> ArgType0;
1418	  false ->
1419	    GenType = dialyzer_typesig:get_safe_underapprox(Pats, Guard),
1420	    t_subtract(t_product(t_to_tlist(ArgType0)), GenType)
1421	end,
1422      case bind_guard(Guard, Map3, State1) of
1423	{error, Reason} ->
1424	  ?debug("Failed guard: ~s\n",
1425		 [cerl_prettypr:format(C, [{hook, cerl_typean:pp_hook()}])]),
1426	  PatString = format_patterns(Pats),
1427	  DefaultMsg =
1428	    case Pats =:= [] of
1429	      true -> {guard_fail, []};
1430	      false ->
1431		{guard_fail_pat, [PatString, format_type(ArgType0, State1)]}
1432	    end,
1433	  State2 =
1434	    case Reason of
1435	      none -> state__add_warning(State1, ?WARN_MATCHING, C, DefaultMsg);
1436	      {FailGuard, Msg} ->
1437		case is_compiler_generated(cerl:get_ann(FailGuard)) of
1438		  false ->
1439		    WarnType = case Msg of
1440				 {guard_fail, _} -> ?WARN_MATCHING;
1441				 {neg_guard_fail, _} -> ?WARN_MATCHING;
1442				 {opaque_guard, _} -> ?WARN_OPAQUE
1443			       end,
1444		    state__add_warning(State1, WarnType, FailGuard, Msg);
1445		  true ->
1446		    state__add_warning(State1, ?WARN_MATCHING, C, Msg)
1447		end
1448	    end,
1449          {State2, Map, t_none(), NewArgType};
1450        Map4 ->
1451          {RetState, RetMap, BodyType} = traverse(Body, Map4, State1),
1452          {RetState, RetMap, BodyType, NewArgType}
1453      end
1454  end.
1455
1456bind_subst(Arg, Pats, Map) ->
1457  case cerl:type(Arg) of
1458    values ->
1459      bind_subst_list(cerl:values_es(Arg), Pats, Map);
1460    var ->
1461      [Pat] = Pats,
1462      enter_subst(Arg, Pat, Map);
1463    _ ->
1464      Map
1465  end.
1466
1467bind_subst_list([Arg|ArgLeft], [Pat|PatLeft], Map) ->
1468  NewMap =
1469    case {cerl:type(Arg), cerl:type(Pat)} of
1470      {var, var} ->         enter_subst(Arg, Pat, Map);
1471      {var, alias} ->       enter_subst(Arg, cerl:alias_pat(Pat), Map);
1472      {literal, literal} -> Map;
1473      {T, T} ->             bind_subst_list(lists:flatten(cerl:subtrees(Arg)),
1474					    lists:flatten(cerl:subtrees(Pat)),
1475					    Map);
1476      _ ->                  Map
1477    end,
1478  bind_subst_list(ArgLeft, PatLeft, NewMap);
1479bind_subst_list([], [], Map) ->
1480  Map.
1481
1482%%----------------------------------------
1483%% Patterns
1484%%
1485
1486bind_pat_vars(Pats, Types, Acc, Map, State) ->
1487  try
1488    bind_pat_vars(Pats, Types, Acc, Map, State, false)
1489  catch
1490    throw:Error ->
1491      %% Error = {error, bind | opaque | record, ErrorPats, ErrorType}
1492      Error
1493  end.
1494
1495bind_pat_vars_reverse(Pats, Types, Acc, Map, State) ->
1496  try
1497    bind_pat_vars(Pats, Types, Acc, Map, State, true)
1498  catch
1499    throw:Error ->
1500      %% Error = {error, bind | opaque | record, ErrorPats, ErrorType}
1501      Error
1502  end.
1503
1504bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
1505  ?debug("Binding pat: ~w to ~s\n", [cerl:type(Pat), format_type(Type, State)]
1506),
1507  Opaques = State#state.opaques,
1508  {NewMap, TypeOut} =
1509    case cerl:type(Pat) of
1510      alias ->
1511	%% Map patterns are more allowing than the type of their literal. We
1512	%% must unfold AliasPat if it is a literal.
1513	AliasPat = dialyzer_utils:refold_pattern(cerl:alias_pat(Pat)),
1514	Var = cerl:alias_var(Pat),
1515	Map1 = enter_subst(Var, AliasPat, Map),
1516	{Map2, [PatType]} = bind_pat_vars([AliasPat], [Type], [],
1517					  Map1, State, Rev),
1518	{enter_type(Var, PatType, Map2), PatType};
1519      binary ->
1520	%% Cannot bind the binary if we are in reverse match since
1521	%% binary patterns and binary construction are not symmetric.
1522	case Rev of
1523	  true -> {Map, t_bitstr()};
1524	  false ->
1525	    BinType = t_inf(t_bitstr(), Type, Opaques),
1526	    case t_is_none(BinType) of
1527	      true ->
1528                case t_find_opaque_mismatch(t_bitstr(), Type, Opaques) of
1529                  {ok, T1, T2}  ->
1530                    bind_error([Pat], T1, T2, opaque);
1531                  error ->
1532                    bind_error([Pat], Type, t_none(), bind)
1533                end;
1534	      false ->
1535		Segs = cerl:binary_segments(Pat),
1536		{Map1, SegTypes} = bind_bin_segs(Segs, BinType, Map, State),
1537		{Map1, t_bitstr_concat(SegTypes)}
1538	    end
1539	end;
1540      cons ->
1541	Cons = t_inf(Type, t_cons(), Opaques),
1542	case t_is_none(Cons) of
1543	  true ->
1544	    bind_opaque_pats(t_cons(), Type, Pat, State);
1545	  false ->
1546	    {Map1, [HdType, TlType]} =
1547	      bind_pat_vars([cerl:cons_hd(Pat), cerl:cons_tl(Pat)],
1548			    [t_cons_hd(Cons, Opaques),
1549                             t_cons_tl(Cons, Opaques)],
1550			    [], Map, State, Rev),
1551	    {Map1, t_cons(HdType, TlType)}
1552	end;
1553      literal ->
1554	Pat0 = dialyzer_utils:refold_pattern(Pat),
1555	case cerl:is_literal(Pat0) of
1556	  true ->
1557	    Literal = literal_type(Pat),
1558	    case t_is_none(t_inf(Literal, Type, Opaques)) of
1559	      true ->
1560		bind_opaque_pats(Literal, Type, Pat, State);
1561	      false -> {Map, Literal}
1562	    end;
1563	  false ->
1564	    %% Retry with the unfolded pattern
1565	    {Map1, [PatType]}
1566	      = bind_pat_vars([Pat0], [Type], [], Map, State, Rev),
1567	    {Map1, PatType}
1568	end;
1569      map ->
1570	MapT = t_inf(Type, t_map(), Opaques),
1571	case t_is_none(MapT) of
1572	  true ->
1573	    bind_opaque_pats(t_map(), Type, Pat, State);
1574	  false ->
1575	    case Rev of
1576	      %% TODO: Reverse matching (propagating a matched subset back to a value)
1577	      true -> {Map, MapT};
1578	      false ->
1579		FoldFun =
1580		  fun(Pair, {MapAcc, ListAcc}) ->
1581		      %% Only exact (:=) can appear in patterns
1582		      exact = cerl:concrete(cerl:map_pair_op(Pair)),
1583		      Key = cerl:map_pair_key(Pair),
1584		      KeyType =
1585			case cerl:type(Key) of
1586			  var ->
1587			    case state__lookup_type_for_letrec(Key, State) of
1588			      error -> lookup_type(Key, MapAcc);
1589			      {ok, RecType} -> RecType
1590			    end;
1591			  literal ->
1592			    literal_type(Key)
1593			end,
1594		      Bind = erl_types:t_map_get(KeyType, MapT),
1595		      {MapAcc1, [ValType]} =
1596			bind_pat_vars([cerl:map_pair_val(Pair)],
1597				      [Bind], [], MapAcc, State, Rev),
1598		      case t_is_singleton(KeyType, Opaques) of
1599			true  -> {MapAcc1, [{KeyType, ValType}|ListAcc]};
1600			false -> {MapAcc1, ListAcc}
1601		      end
1602		  end,
1603		{Map1, Pairs} = lists:foldl(FoldFun, {Map, []}, cerl:map_es(Pat)),
1604		{Map1, t_inf(MapT, t_map(Pairs))}
1605	    end
1606	end;
1607      tuple ->
1608	Es = cerl:tuple_es(Pat),
1609	{TypedRecord, Prototype} =
1610	  case Es of
1611	    [] -> {false, t_tuple([])};
1612	    [Tag|Left] ->
1613	      case cerl:is_c_atom(Tag) andalso is_literal_record(Pat) of
1614		true ->
1615		  TagAtom = cerl:atom_val(Tag),
1616		  case state__lookup_record(TagAtom, length(Left), State) of
1617		    error -> {false, t_tuple(length(Es))};
1618		    {ok, Record} ->
1619		      [_Head|AnyTail] = [t_any() || _ <- Es],
1620		      UntypedRecord = t_tuple([t_atom(TagAtom)|AnyTail]),
1621		      {not t_is_equal(Record, UntypedRecord), Record}
1622		  end;
1623		false -> {false, t_tuple(length(Es))}
1624	      end
1625	  end,
1626	Tuple = t_inf(Prototype, Type, Opaques),
1627	case t_is_none(Tuple) of
1628	  true ->
1629	    bind_opaque_pats(Prototype, Type, Pat, State);
1630	  false ->
1631	    SubTuples = t_tuple_subtypes(Tuple, Opaques),
1632	    %% Need to call the top function to get the try-catch wrapper
1633            MapJ = join_maps_begin(Map),
1634	    Results =
1635	      case Rev of
1636		true ->
1637		  [bind_pat_vars_reverse(Es, t_tuple_args(SubTuple, Opaques),
1638                                         [], MapJ, State)
1639		   || SubTuple <- SubTuples];
1640		false ->
1641		  [bind_pat_vars(Es, t_tuple_args(SubTuple, Opaques), [],
1642                                 MapJ, State)
1643		   || SubTuple <- SubTuples]
1644	      end,
1645	    case lists:keyfind(opaque, 2, Results) of
1646	      {error, opaque, _PatList, _Type, Opaque} ->
1647		bind_error([Pat], Tuple, Opaque, opaque);
1648	      false ->
1649		case [M || {M, _} <- Results, M =/= error] of
1650		  [] ->
1651		    case TypedRecord of
1652		      true -> bind_error([Pat], Tuple, Prototype, record);
1653		      false -> bind_error([Pat], Tuple, t_none(), bind)
1654		    end;
1655		  Maps ->
1656		    Map1 = join_maps_end(Maps, MapJ),
1657		    TupleType = t_sup([t_tuple(EsTypes)
1658				       || {M, EsTypes} <- Results, M =/= error]),
1659		    {Map1, TupleType}
1660		end
1661	    end
1662	end;
1663      values ->
1664	Es = cerl:values_es(Pat),
1665	{Map1, EsTypes} =
1666	  bind_pat_vars(Es, t_to_tlist(Type), [], Map, State, Rev),
1667	{Map1, t_product(EsTypes)};
1668      var ->
1669	VarType1 =
1670	  case state__lookup_type_for_letrec(Pat, State) of
1671	    error -> lookup_type(Pat, Map);
1672	    {ok, RecType} -> RecType
1673	  end,
1674	%% Must do inf when binding args to pats. Vars in pats are fresh.
1675	VarType2 = t_inf(VarType1, Type, Opaques),
1676	case t_is_none(VarType2) of
1677	  true ->
1678	    case t_find_opaque_mismatch(VarType1, Type, Opaques) of
1679	      {ok, T1, T2}  ->
1680		bind_error([Pat], T1, T2, opaque);
1681	      error ->
1682		bind_error([Pat], Type, t_none(), bind)
1683	    end;
1684	  false ->
1685	    Map1 = enter_type(Pat, VarType2, Map),
1686	    {Map1, VarType2}
1687	end;
1688      _Other ->
1689	%% Catch all is needed when binding args to pats
1690	?debug("Failed match for ~p\n", [_Other]),
1691	bind_error([Pat], Type, t_none(), bind)
1692    end,
1693  bind_pat_vars(PatLeft, TypeLeft, [TypeOut|Acc], NewMap, State, Rev);
1694bind_pat_vars([], [], Acc, Map, _State, _Rev) ->
1695  {Map, lists:reverse(Acc)}.
1696
1697bind_bin_segs(BinSegs, BinType, Map, State) ->
1698  bind_bin_segs(BinSegs, BinType, [], Map, State).
1699
1700bind_bin_segs([Seg|Segs], BinType, Acc, Map, State) ->
1701  Val = cerl:bitstr_val(Seg),
1702  SegType = cerl:concrete(cerl:bitstr_type(Seg)),
1703  UnitVal = cerl:concrete(cerl:bitstr_unit(Seg)),
1704  case cerl:bitstr_bitsize(Seg) of
1705    all ->
1706      binary = SegType, [] = Segs, %% just an assert
1707      T = t_inf(t_bitstr(UnitVal, 0), BinType),
1708      {Map1, [Type]} = bind_pat_vars([Val], [T], [], Map, State, false),
1709      Type1 = remove_local_opaque_types(Type, State#state.opaques),
1710      bind_bin_segs(Segs, t_bitstr(0, 0), [Type1|Acc], Map1, State);
1711    utf -> % XXX: possibly can be strengthened
1712      true = lists:member(SegType, [utf8, utf16, utf32]),
1713      {Map1, [_]} = bind_pat_vars([Val], [t_integer()], [], Map, State, false),
1714      Type = t_binary(),
1715      bind_bin_segs(Segs, BinType, [Type|Acc], Map1, State);
1716    BitSz when is_integer(BitSz) orelse BitSz =:= any ->
1717      Size = cerl:bitstr_size(Seg),
1718      {Map1, [SizeType]} =
1719	bind_pat_vars([Size], [t_non_neg_integer()], [], Map, State, false),
1720      Opaques = State#state.opaques,
1721      NumberVals = t_number_vals(SizeType, Opaques),
1722      case t_contains_opaque(SizeType, Opaques) of
1723        true -> bind_error([Seg], SizeType, t_none(), opaque);
1724        false -> ok
1725      end,
1726      Type =
1727	case NumberVals of
1728	  [OneSize] -> t_bitstr(0, UnitVal * OneSize);
1729	  _ -> % 'unknown' too
1730	    MinSize = erl_types:number_min(SizeType, Opaques),
1731	    t_bitstr(UnitVal, UnitVal * MinSize)
1732	end,
1733      ValConstr =
1734	case SegType of
1735	  binary -> Type; %% The same constraints as for the whole bitstr
1736	  float -> t_float();
1737	  integer ->
1738	    case NumberVals of
1739	      unknown -> t_integer();
1740	      List ->
1741		SizeVal = lists:max(List),
1742		Flags = cerl:concrete(cerl:bitstr_flags(Seg)),
1743		N = SizeVal * UnitVal,
1744                case N >= ?BITS  of
1745                  true ->
1746                    case lists:member(signed, Flags) of
1747                      true -> t_from_range(neg_inf, pos_inf);
1748                      false -> t_from_range(0, pos_inf)
1749                    end;
1750                  false ->
1751                    case lists:member(signed, Flags) of
1752                      true -> t_from_range(-(1 bsl (N - 1)), 1 bsl (N - 1) - 1);
1753                      false -> t_from_range(0, 1 bsl N - 1)
1754                    end
1755                end
1756	    end
1757	end,
1758      {Map2, [_]} = bind_pat_vars([Val], [ValConstr], [], Map1, State, false),
1759      NewBinType = t_bitstr_match(Type, BinType),
1760      case t_is_none(NewBinType) of
1761	true -> bind_error([Seg], BinType, t_none(), bind);
1762	false -> bind_bin_segs(Segs, NewBinType, [Type|Acc], Map2, State)
1763      end
1764  end;
1765bind_bin_segs([], _BinType, Acc, Map, _State) ->
1766  {Map, lists:reverse(Acc)}.
1767
1768bind_error(Pats, Type, OpaqueType, Error0) ->
1769  Error = case {Error0, Pats} of
1770            {bind, [Pat]} ->
1771              case is_literal_record(Pat) of
1772                true -> record;
1773                false -> Error0
1774              end;
1775            _ -> Error0
1776          end,
1777  throw({error, Error, Pats, Type, OpaqueType}).
1778
1779-spec bind_opaque_pats(type(), type(), cerl:c_literal(), state()) ->
1780                          no_return().
1781
1782bind_opaque_pats(GenType, Type, Pat, State) ->
1783  case t_find_opaque_mismatch(GenType, Type, State#state.opaques) of
1784    {ok, T1, T2}  ->
1785	bind_error([Pat], T1, T2, opaque);
1786    error ->
1787      bind_error([Pat], Type, t_none(), bind)
1788  end.
1789
1790%%----------------------------------------
1791%% Guards
1792%%
1793
1794bind_guard(Guard, Map, State) ->
1795  try bind_guard(Guard, Map, maps:new(), pos, State) of
1796    {Map1, _Type} -> Map1
1797  catch
1798    throw:{fail, Warning} -> {error, Warning};
1799    throw:{fatal_fail, Warning} -> {error, Warning}
1800  end.
1801
1802bind_guard(Guard, Map, Env, Eval, State) ->
1803  ?debug("Handling ~w guard: ~s\n",
1804	 [Eval, cerl_prettypr:format(Guard, [{noann, true}])]),
1805  case cerl:type(Guard) of
1806    binary ->
1807      {Map, t_binary()};
1808    'case' ->
1809      Arg = cerl:case_arg(Guard),
1810      Clauses = cerl:case_clauses(Guard),
1811      bind_guard_case_clauses(Arg, Clauses, Map, Env, Eval, State);
1812    cons ->
1813      Hd = cerl:cons_hd(Guard),
1814      Tl = cerl:cons_tl(Guard),
1815      {Map1, HdType} = bind_guard(Hd, Map, Env, dont_know, State),
1816      {Map2, TlType} = bind_guard(Tl, Map1, Env, dont_know, State),
1817      {Map2, t_cons(HdType, TlType)};
1818    literal ->
1819      {Map, literal_type(Guard)};
1820    'try' ->
1821      Arg = cerl:try_arg(Guard),
1822      [Var] = cerl:try_vars(Guard),
1823      EVars = cerl:try_evars(Guard),
1824      %%?debug("Storing: ~w\n", [Var]),
1825      Map1 = join_maps_begin(Map),
1826      Map2 = mark_as_fresh(EVars, Map1),
1827      %% Visit handler first so we know if it should be ignored
1828      {{HandlerMap, HandlerType}, HandlerE} =
1829	try {bind_guard(cerl:try_handler(Guard), Map2, Env, Eval, State), none}
1830	catch throw:HE ->
1831	    {{Map2, t_none()}, HE}
1832	end,
1833      BodyEnv = maps:put(get_label(Var), Arg, Env),
1834      Wanted = case Eval of pos -> t_atom(true); neg -> t_atom(false);
1835		 dont_know -> t_any() end,
1836      case t_is_none(t_inf(HandlerType, Wanted)) of
1837	%% Handler won't save us; pretend it does not exist
1838	true -> bind_guard(cerl:try_body(Guard), Map, BodyEnv, Eval, State);
1839	false ->
1840	  {{BodyMap, BodyType}, BodyE} =
1841	    try {bind_guard(cerl:try_body(Guard), Map1, BodyEnv,
1842			    Eval, State), none}
1843	    catch throw:BE ->
1844		{{Map1, t_none()}, BE}
1845	    end,
1846	  Map3 = join_maps_end([BodyMap, HandlerMap], Map1),
1847	  case t_is_none(Sup = t_sup(BodyType, HandlerType)) of
1848	    true ->
1849	      %% Pick a reason. N.B. We assume that the handler is always
1850	      %% compiler-generated if the body is; that way, we won't need to
1851	      %% check.
1852	      Fatality = case {BodyE, HandlerE} of
1853			   {{fatal_fail, _}, _} -> fatal_fail;
1854			   {_, {fatal_fail, _}} -> fatal_fail;
1855			   _ -> fail
1856			 end,
1857	      throw({Fatality,
1858		     case {BodyE, HandlerE} of
1859		       {{_, Rsn}, _} when Rsn =/= none -> Rsn;
1860		       {_, {_,Rsn}} -> Rsn;
1861		       _ -> none
1862		     end});
1863	    false -> {Map3, Sup}
1864	  end
1865      end;
1866    tuple ->
1867      Es0 = cerl:tuple_es(Guard),
1868      {Map1, Es} = bind_guard_list(Es0, Map, Env, dont_know, State),
1869      {Map1, t_tuple(Es)};
1870    map ->
1871      case Eval of
1872	dont_know -> handle_guard_map(Guard, Map, Env, State);
1873	_PosOrNeg -> {Map, t_none()}  %% Map exprs do not produce bools
1874      end;
1875    'let' ->
1876      Arg = cerl:let_arg(Guard),
1877      [Var] = cerl:let_vars(Guard),
1878      %%?debug("Storing: ~w\n", [Var]),
1879      NewEnv = maps:put(get_label(Var), Arg, Env),
1880      bind_guard(cerl:let_body(Guard), Map, NewEnv, Eval, State);
1881    values ->
1882      Es = cerl:values_es(Guard),
1883      List = [bind_guard(V, Map, Env, dont_know, State) || V <- Es],
1884      Type = t_product([T || {_, T} <- List]),
1885      {Map, Type};
1886    var ->
1887      ?debug("Looking for var(~w)...", [cerl_trees:get_label(Guard)]),
1888      case maps:find(get_label(Guard), Env) of
1889	error ->
1890	  ?debug("Did not find it\n", []),
1891	  Type = lookup_type(Guard, Map),
1892	  Constr =
1893	    case Eval of
1894	      pos -> t_atom(true);
1895	      neg -> t_atom(false);
1896	      dont_know -> Type
1897	    end,
1898	  Inf = t_inf(Constr, Type),
1899	  {enter_type(Guard, Inf, Map), Inf};
1900	{ok, Tree} ->
1901	  ?debug("Found it\n", []),
1902	  {Map1, Type} = bind_guard(Tree, Map, Env, Eval, State),
1903	  {enter_type(Guard, Type, Map1), Type}
1904      end;
1905    call ->
1906      handle_guard_call(Guard, Map, Env, Eval, State)
1907  end.
1908
1909handle_guard_call(Guard, Map, Env, Eval, State) ->
1910  MFA = {cerl:atom_val(cerl:call_module(Guard)),
1911	 cerl:atom_val(cerl:call_name(Guard)),
1912	 cerl:call_arity(Guard)},
1913  case MFA of
1914    {erlang, F, 1} when F =:= is_atom; F =:= is_boolean;
1915			F =:= is_binary; F =:= is_bitstring;
1916			F =:= is_float; F =:= is_function;
1917			F =:= is_integer; F =:= is_list; F =:= is_map;
1918			F =:= is_number; F =:= is_pid; F =:= is_port;
1919			F =:= is_reference; F =:= is_tuple ->
1920      handle_guard_type_test(Guard, F, Map, Env, Eval, State);
1921    {erlang, is_function, 2} ->
1922      handle_guard_is_function(Guard, Map, Env, Eval, State);
1923    MFA when (MFA =:= {erlang, internal_is_record, 3}) or
1924	     (MFA =:= {erlang, is_record, 3}) ->
1925      handle_guard_is_record(Guard, Map, Env, Eval, State);
1926    {erlang, '=:=', 2} ->
1927      handle_guard_eqeq(Guard, Map, Env, Eval, State);
1928    {erlang, '==', 2} ->
1929      handle_guard_eq(Guard, Map, Env, Eval, State);
1930    {erlang, 'and', 2} ->
1931      handle_guard_and(Guard, Map, Env, Eval, State);
1932    {erlang, 'or', 2} ->
1933      handle_guard_or(Guard, Map, Env, Eval, State);
1934    {erlang, 'not', 1} ->
1935      handle_guard_not(Guard, Map, Env, Eval, State);
1936    {erlang, Comp, 2} when Comp =:= '<'; Comp =:= '=<';
1937                           Comp =:= '>'; Comp =:= '>=' ->
1938      handle_guard_comp(Guard, Comp, Map, Env, Eval, State);
1939    _ ->
1940      handle_guard_gen_fun(MFA, Guard, Map, Env, Eval, State)
1941  end.
1942
1943handle_guard_gen_fun({M, F, A}, Guard, Map, Env, Eval, State) ->
1944  Args = cerl:call_args(Guard),
1945  {Map1, As} = bind_guard_list(Args, Map, Env, dont_know, State),
1946  Opaques = State#state.opaques,
1947  BifRet = erl_bif_types:type(M, F, A, As, Opaques),
1948  case t_is_none(BifRet) of
1949    true ->
1950      %% Is this an error-bif?
1951      case t_is_none(erl_bif_types:type(M, F, A)) of
1952	true -> signal_guard_fail(Eval, Guard, As, State);
1953	false -> signal_guard_fatal_fail(Eval, Guard, As, State)
1954      end;
1955    false ->
1956      BifArgs = bif_args(M, F, A),
1957      Map2 = enter_type_lists(Args, t_inf_lists(BifArgs, As, Opaques), Map1),
1958      Ret =
1959	case Eval of
1960	  pos -> t_inf(t_atom(true), BifRet);
1961	  neg -> t_inf(t_atom(false), BifRet);
1962	  dont_know -> BifRet
1963	end,
1964      case t_is_none(Ret) of
1965	true ->
1966	  case Eval =:= pos of
1967	    true -> signal_guard_fail(Eval, Guard, As, State);
1968	    false -> throw({fail, none})
1969	  end;
1970	false -> {Map2, Ret}
1971      end
1972  end.
1973
1974handle_guard_type_test(Guard, F, Map, Env, Eval, State) ->
1975  [Arg] = cerl:call_args(Guard),
1976  {Map1, ArgType} = bind_guard(Arg, Map, Env, dont_know, State),
1977  case bind_type_test(Eval, F, ArgType, State) of
1978    error ->
1979      ?debug("Type test: ~w failed\n", [F]),
1980      signal_guard_fail(Eval, Guard, [ArgType], State);
1981    {ok, NewArgType, Ret} ->
1982      ?debug("Type test: ~w succeeded, NewType: ~s, Ret: ~s\n",
1983	     [F, t_to_string(NewArgType), t_to_string(Ret)]),
1984      {enter_type(Arg, NewArgType, Map1), Ret}
1985  end.
1986
1987bind_type_test(Eval, TypeTest, ArgType, State) ->
1988  Type = case TypeTest of
1989	   is_atom -> t_atom();
1990	   is_boolean -> t_boolean();
1991	   is_binary -> t_binary();
1992	   is_bitstring -> t_bitstr();
1993	   is_float -> t_float();
1994	   is_function -> t_fun();
1995	   is_integer -> t_integer();
1996	   is_list -> t_maybe_improper_list();
1997	   is_map -> t_map();
1998	   is_number -> t_number();
1999	   is_pid -> t_pid();
2000	   is_port -> t_port();
2001	   is_reference -> t_reference();
2002	   is_tuple -> t_tuple()
2003	 end,
2004  case Eval of
2005    pos ->
2006      Inf = t_inf(Type, ArgType, State#state.opaques),
2007      case t_is_none(Inf) of
2008	true -> error;
2009	false -> {ok, Inf, t_atom(true)}
2010      end;
2011    neg ->
2012      Sub = t_subtract(ArgType, Type),
2013      case t_is_none(Sub) of
2014        true -> error;
2015        false -> {ok, Sub, t_atom(false)}
2016      end;
2017    dont_know ->
2018      {ok, ArgType, t_boolean()}
2019  end.
2020
2021handle_guard_comp(Guard, Comp, Map, Env, Eval, State) ->
2022  Args = cerl:call_args(Guard),
2023  [Arg1, Arg2] = Args,
2024  {Map1, ArgTypes} = bind_guard_list(Args, Map, Env, dont_know, State),
2025  Opaques = State#state.opaques,
2026  [Type1, Type2] = ArgTypes,
2027  IsInt1 = t_is_integer(Type1, Opaques),
2028  IsInt2 = t_is_integer(Type2, Opaques),
2029  case {type(Arg1), type(Arg2)} of
2030    {{literal, Lit1}, {literal, Lit2}} ->
2031      case erlang:Comp(cerl:concrete(Lit1), cerl:concrete(Lit2)) of
2032	true  when Eval =:= pos ->       {Map, t_atom(true)};
2033	true  when Eval =:= dont_know -> {Map, t_atom(true)};
2034	true  when Eval =:= neg ->       {Map, t_atom(true)};
2035	false when Eval =:= pos ->
2036	  signal_guard_fail(Eval, Guard, ArgTypes, State);
2037	false when Eval =:= dont_know -> {Map, t_atom(false)};
2038	false when Eval =:= neg ->       {Map, t_atom(false)}
2039      end;
2040    {{literal, Lit1}, var} when IsInt1 andalso IsInt2 andalso (Eval =:= pos) ->
2041      case bind_comp_literal_var(Lit1, Arg2, Type2, Comp, Map1, Opaques) of
2042	error -> signal_guard_fail(Eval, Guard, ArgTypes, State);
2043	{ok, NewMap} -> {NewMap, t_atom(true)}
2044      end;
2045    {var, {literal, Lit2}} when IsInt1 andalso IsInt2 andalso (Eval =:= pos) ->
2046      case bind_comp_literal_var(Lit2, Arg1, Type1, invert_comp(Comp),
2047                                 Map1, Opaques) of
2048	error -> signal_guard_fail(Eval, Guard, ArgTypes, State);
2049	{ok, NewMap} -> {NewMap, t_atom(true)}
2050      end;
2051    {_, _} ->
2052      handle_guard_gen_fun({erlang, Comp, 2}, Guard, Map, Env, Eval, State)
2053  end.
2054
2055invert_comp('=<') -> '>=';
2056invert_comp('<')  -> '>';
2057invert_comp('>=') -> '=<';
2058invert_comp('>')  -> '<'.
2059
2060bind_comp_literal_var(Lit, Var, VarType, CompOp, Map, Opaques) ->
2061  LitVal = cerl:concrete(Lit),
2062  NewVarType =
2063    case t_number_vals(VarType, Opaques) of
2064      unknown ->
2065	Range =
2066	  case CompOp of
2067	    '=<' -> t_from_range(LitVal, pos_inf);
2068	    '<'  -> t_from_range(LitVal + 1, pos_inf);
2069	    '>=' -> t_from_range(neg_inf, LitVal);
2070	    '>'  -> t_from_range(neg_inf, LitVal - 1)
2071	  end,
2072	t_inf(Range, VarType, Opaques);
2073      NumberVals ->
2074	NewNumberVals = [X || X <- NumberVals, erlang:CompOp(LitVal, X)],
2075	t_integers(NewNumberVals)
2076    end,
2077  case t_is_none(NewVarType) of
2078    true -> error;
2079    false -> {ok, enter_type(Var, NewVarType, Map)}
2080  end.
2081
2082handle_guard_is_function(Guard, Map, Env, Eval, State) ->
2083  Args = cerl:call_args(Guard),
2084  {Map1, ArgTypes0} = bind_guard_list(Args, Map, Env, dont_know, State),
2085  [FunType0, ArityType0] = ArgTypes0,
2086  Opaques = State#state.opaques,
2087  ArityType = t_inf(ArityType0, t_integer(), Opaques),
2088  case t_is_none(ArityType) of
2089    true -> signal_guard_fail(Eval, Guard, ArgTypes0, State);
2090    false ->
2091      FunTypeConstr =
2092	case t_number_vals(ArityType, State#state.opaques) of
2093	  unknown -> t_fun();
2094	  Vals ->
2095	    t_sup([t_fun(lists:duplicate(X, t_any()), t_any()) || X <- Vals])
2096	end,
2097      FunType = t_inf(FunType0, FunTypeConstr, Opaques),
2098      case t_is_none(FunType) of
2099	true ->
2100	  case Eval of
2101	    pos -> signal_guard_fail(Eval, Guard, ArgTypes0, State);
2102	    neg -> {Map1, t_atom(false)};
2103	    dont_know -> {Map1, t_atom(false)}
2104	  end;
2105	false ->
2106	  case Eval of
2107	    pos -> {enter_type_lists(Args, [FunType, ArityType], Map1),
2108		    t_atom(true)};
2109	    neg -> {Map1, t_atom(false)};
2110	    dont_know -> {Map1, t_boolean()}
2111	  end
2112      end
2113  end.
2114
2115handle_guard_is_record(Guard, Map, Env, Eval, State) ->
2116  Args = cerl:call_args(Guard),
2117  [Rec, Tag0, Arity0] = Args,
2118  Tag = cerl:atom_val(Tag0),
2119  Arity = cerl:int_val(Arity0),
2120  {Map1, RecType} = bind_guard(Rec, Map, Env, dont_know, State),
2121  ArityMin1 = Arity - 1,
2122  Opaques = State#state.opaques,
2123  Tuple = t_tuple([t_atom(Tag)|lists:duplicate(ArityMin1, t_any())]),
2124  case t_is_none(t_inf(Tuple, RecType, Opaques)) of
2125    true ->
2126      case erl_types:t_has_opaque_subtype(RecType, Opaques) of
2127        true ->
2128          signal_guard_fail(Eval, Guard,
2129                            [RecType, t_from_term(Tag),
2130                             t_from_term(Arity)],
2131                            State);
2132        false ->
2133          case Eval of
2134            pos -> signal_guard_fail(Eval, Guard,
2135                                     [RecType, t_from_term(Tag),
2136                                      t_from_term(Arity)],
2137                                     State);
2138            neg -> {Map1, t_atom(false)};
2139            dont_know -> {Map1, t_atom(false)}
2140          end
2141      end;
2142    false ->
2143      TupleType =
2144        case state__lookup_record(Tag, ArityMin1, State) of
2145          error -> Tuple;
2146          {ok, Prototype} -> Prototype
2147        end,
2148      Type = t_inf(TupleType, RecType, State#state.opaques),
2149      case t_is_none(Type) of
2150        true ->
2151          %% No special handling of opaque errors.
2152          FArgs = "record " ++ format_type(RecType, State),
2153          Msg = {record_matching, [FArgs, Tag]},
2154          throw({fail, {Guard, Msg}});
2155        false ->
2156          case Eval of
2157            pos -> {enter_type(Rec, Type, Map1), t_atom(true)};
2158            neg -> {Map1, t_atom(false)};
2159            dont_know -> {Map1, t_boolean()}
2160          end
2161      end
2162  end.
2163
2164handle_guard_eq(Guard, Map, Env, Eval, State) ->
2165  [Arg1, Arg2] = cerl:call_args(Guard),
2166  case {type(Arg1), type(Arg2)} of
2167    {{literal, Lit1}, {literal, Lit2}} ->
2168      case cerl:concrete(Lit1) =:= cerl:concrete(Lit2) of
2169	true ->
2170	  if
2171	    Eval =:= pos -> {Map, t_atom(true)};
2172	    Eval =:= neg ->
2173	      ArgTypes = [t_from_term(cerl:concrete(Lit1)),
2174			  t_from_term(cerl:concrete(Lit2))],
2175	      signal_guard_fail(Eval, Guard, ArgTypes, State);
2176	    Eval =:= dont_know -> {Map, t_atom(true)}
2177	  end;
2178	false ->
2179	  if
2180	    Eval =:= neg -> {Map, t_atom(false)};
2181	    Eval =:= dont_know -> {Map, t_atom(false)};
2182	    Eval =:= pos ->
2183	      ArgTypes = [t_from_term(cerl:concrete(Lit1)),
2184			  t_from_term(cerl:concrete(Lit2))],
2185	      signal_guard_fail(Eval, Guard, ArgTypes, State)
2186	  end
2187      end;
2188    {{literal, Lit1}, _} when Eval =:= pos ->
2189      case cerl:concrete(Lit1) of
2190	Atom when is_atom(Atom) ->
2191	  bind_eqeq_guard_lit_other(Guard, Lit1, Arg2, Map, Env, State);
2192	[] ->
2193	  bind_eqeq_guard_lit_other(Guard, Lit1, Arg2, Map, Env, State);
2194	_ ->
2195	  bind_eq_guard(Guard, Lit1, Arg2, Map, Env, Eval, State)
2196      end;
2197    {_, {literal, Lit2}} when Eval =:= pos ->
2198      case cerl:concrete(Lit2) of
2199	Atom when is_atom(Atom) ->
2200	  bind_eqeq_guard_lit_other(Guard, Lit2, Arg1, Map, Env, State);
2201	[] ->
2202	  bind_eqeq_guard_lit_other(Guard, Lit2, Arg1, Map, Env, State);
2203	_ ->
2204	  bind_eq_guard(Guard, Arg1, Lit2, Map, Env, Eval, State)
2205      end;
2206    {_, _} ->
2207      bind_eq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State)
2208  end.
2209
2210bind_eq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State) ->
2211  {Map1, Type1} = bind_guard(Arg1, Map, Env, dont_know, State),
2212  {Map2, Type2} = bind_guard(Arg2, Map1, Env, dont_know, State),
2213  Opaques = State#state.opaques,
2214  case
2215    t_is_nil(Type1, Opaques) orelse t_is_nil(Type2, Opaques)
2216    orelse t_is_atom(Type1, Opaques) orelse t_is_atom(Type2, Opaques)
2217  of
2218    true -> bind_eqeq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State);
2219    false ->
2220      %% XXX. Is this test OK?
2221      OpArgs = erl_types:t_find_unknown_opaque(Type1, Type2, Opaques),
2222      case OpArgs =:= [] of
2223        true ->
2224          case Eval of
2225            pos -> {Map2, t_atom(true)};
2226            neg -> {Map2, t_atom(false)};
2227            dont_know -> {Map2, t_boolean()}
2228          end;
2229        false ->
2230          signal_guard_fail(Eval, Guard, [Type1, Type2], State)
2231      end
2232  end.
2233
2234handle_guard_eqeq(Guard, Map, Env, Eval, State) ->
2235  [Arg1, Arg2] = cerl:call_args(Guard),
2236  case {type(Arg1), type(Arg2)} of
2237    {{literal, Lit1}, {literal, Lit2}} ->
2238
2239      case cerl:concrete(Lit1) =:= cerl:concrete(Lit2) of
2240	true ->
2241	  if Eval =:= neg ->
2242	      ArgTypes = [t_from_term(cerl:concrete(Lit1)),
2243			  t_from_term(cerl:concrete(Lit2))],
2244	      signal_guard_fail(Eval, Guard, ArgTypes, State);
2245	     Eval =:= pos -> {Map, t_atom(true)};
2246	     Eval =:= dont_know -> {Map, t_atom(true)}
2247	  end;
2248	false ->
2249	  if Eval =:= neg -> {Map, t_atom(false)};
2250	     Eval =:= dont_know -> {Map, t_atom(false)};
2251	     Eval =:= pos ->
2252	      ArgTypes = [t_from_term(cerl:concrete(Lit1)),
2253			  t_from_term(cerl:concrete(Lit2))],
2254	      signal_guard_fail(Eval, Guard, ArgTypes, State)
2255	  end
2256      end;
2257    {{literal, Lit1}, _} when Eval =:= pos ->
2258      bind_eqeq_guard_lit_other(Guard, Lit1, Arg2, Map, Env, State);
2259    {_, {literal, Lit2}} when Eval =:= pos ->
2260      bind_eqeq_guard_lit_other(Guard, Lit2, Arg1, Map, Env, State);
2261    {_, _} ->
2262      bind_eqeq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State)
2263  end.
2264
2265bind_eqeq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State) ->
2266  {Map1, Type1} = bind_guard(Arg1, Map, Env, dont_know, State),
2267  {Map2, Type2} = bind_guard(Arg2, Map1, Env, dont_know, State),
2268  ?debug("Types are:~s =:= ~s\n", [t_to_string(Type1),
2269				   t_to_string(Type2)]),
2270  Opaques = State#state.opaques,
2271  Inf = t_inf(Type1, Type2, Opaques),
2272  case t_is_none(Inf) of
2273    true ->
2274      OpArgs = erl_types:t_find_unknown_opaque(Type1, Type2, Opaques),
2275      case OpArgs =:= [] of
2276        true ->
2277          case Eval of
2278            neg -> {Map2, t_atom(false)};
2279            dont_know -> {Map2, t_atom(false)};
2280            pos -> signal_guard_fail(Eval, Guard, [Type1, Type2], State)
2281          end;
2282        false ->
2283          signal_guard_fail(Eval, Guard, [Type1, Type2], State)
2284      end;
2285    false ->
2286      case Eval of
2287        pos ->
2288          case {cerl:type(Arg1), cerl:type(Arg2)} of
2289            {var, var} ->
2290              Map3 = enter_subst(Arg1, Arg2, Map2),
2291              Map4 = enter_type(Arg2, Inf, Map3),
2292              {Map4, t_atom(true)};
2293            {var, _} ->
2294              Map3 = enter_type(Arg1, Inf, Map2),
2295              {Map3, t_atom(true)};
2296            {_, var} ->
2297              Map3 = enter_type(Arg2, Inf, Map2),
2298              {Map3, t_atom(true)};
2299            {_, _} ->
2300              {Map2, t_atom(true)}
2301          end;
2302        neg ->
2303          {Map2, t_atom(false)};
2304        dont_know ->
2305          {Map2, t_boolean()}
2306      end
2307  end.
2308
2309bind_eqeq_guard_lit_other(Guard, Arg1, Arg2, Map, Env, State) ->
2310  Eval = dont_know,
2311  Opaques = State#state.opaques,
2312  case cerl:concrete(Arg1) of
2313    true ->
2314      {_, Type} = MT = bind_guard(Arg2, Map, Env, pos, State),
2315      case t_is_any_atom(true, Type, Opaques) of
2316	true -> MT;
2317	false ->
2318	  {_, Type0} = bind_guard(Arg2, Map, Env, Eval, State),
2319	  signal_guard_fail(Eval, Guard, [Type0, t_atom(true)], State)
2320      end;
2321    false ->
2322      {Map1, Type} = bind_guard(Arg2, Map, Env, neg, State),
2323      case t_is_any_atom(false, Type, Opaques) of
2324	true -> {Map1, t_atom(true)};
2325	false ->
2326	  {_, Type0} = bind_guard(Arg2, Map, Env, Eval, State),
2327	  signal_guard_fail(Eval, Guard, [Type0, t_atom(false)], State)
2328      end;
2329    Term ->
2330      LitType = t_from_term(Term),
2331      {Map1, Type} = bind_guard(Arg2, Map, Env, Eval, State),
2332      case t_is_subtype(LitType, Type) of
2333	false -> signal_guard_fail(Eval, Guard, [Type, LitType], State);
2334	true ->
2335	  case cerl:is_c_var(Arg2) of
2336	    true -> {enter_type(Arg2, LitType, Map1), t_atom(true)};
2337	    false -> {Map1, t_atom(true)}
2338	  end
2339      end
2340  end.
2341
2342handle_guard_and(Guard, Map, Env, Eval, State) ->
2343  [Arg1, Arg2] = cerl:call_args(Guard),
2344  Opaques = State#state.opaques,
2345  case Eval of
2346    pos ->
2347      {Map1, Type1} = bind_guard(Arg1, Map, Env, Eval, State),
2348      case t_is_any_atom(true, Type1, Opaques) of
2349	false -> signal_guard_fail(Eval, Guard, [Type1, t_any()], State);
2350	true ->
2351	  {Map2, Type2} = bind_guard(Arg2, Map1, Env, Eval, State),
2352	  case t_is_any_atom(true, Type2, Opaques) of
2353	    false -> signal_guard_fail(Eval, Guard, [Type1, Type2], State);
2354	    true -> {Map2, t_atom(true)}
2355	  end
2356      end;
2357    neg ->
2358      MapJ = join_maps_begin(Map),
2359      {Map1, Type1} =
2360	try bind_guard(Arg1, MapJ, Env, neg, State)
2361	catch throw:{fail, _} -> bind_guard(Arg2, MapJ, Env, pos, State)
2362	end,
2363      {Map2, Type2} =
2364	try bind_guard(Arg2, MapJ, Env, neg, State)
2365	catch throw:{fail, _} -> bind_guard(Arg1, MapJ, Env, pos, State)
2366	end,
2367      case
2368        t_is_any_atom(false, Type1, Opaques)
2369        orelse t_is_any_atom(false, Type2, Opaques)
2370      of
2371	true -> {join_maps_end([Map1, Map2], MapJ), t_atom(false)};
2372	false -> signal_guard_fail(Eval, Guard, [Type1, Type2], State)
2373      end;
2374    dont_know ->
2375      MapJ = join_maps_begin(Map),
2376      {Map1, Type1} = bind_guard(Arg1, MapJ, Env, dont_know, State),
2377      {Map2, Type2} = bind_guard(Arg2, MapJ, Env, dont_know, State),
2378      Bool1 = t_inf(Type1, t_boolean()),
2379      Bool2 = t_inf(Type2, t_boolean()),
2380      case t_is_none(Bool1) orelse t_is_none(Bool2) of
2381	true -> throw({fatal_fail, none});
2382	false ->
2383	  NewMap = join_maps_end([Map1, Map2], MapJ),
2384	  NewType =
2385	    case {t_atom_vals(Bool1, Opaques), t_atom_vals(Bool2, Opaques)} of
2386	      {['true'] , ['true'] } -> t_atom(true);
2387	      {['false'], _        } -> t_atom(false);
2388	      {_        , ['false']} -> t_atom(false);
2389              {unknown  , _        } ->
2390                signal_guard_fail(Eval, Guard, [Type1, Type2], State);
2391              {_        , unknown  } ->
2392                signal_guard_fail(Eval, Guard, [Type1, Type2], State);
2393	      {_        , _        } -> t_boolean()
2394
2395	    end,
2396	  {NewMap, NewType}
2397      end
2398  end.
2399
2400handle_guard_or(Guard, Map, Env, Eval, State) ->
2401  [Arg1, Arg2] = cerl:call_args(Guard),
2402  Opaques = State#state.opaques,
2403  case Eval of
2404    pos ->
2405      MapJ = join_maps_begin(Map),
2406      {Map1, Bool1} =
2407	try bind_guard(Arg1, MapJ, Env, pos, State)
2408	catch
2409	  throw:{fail,_} -> bind_guard(Arg1, MapJ, Env, dont_know, State)
2410	end,
2411      {Map2, Bool2} =
2412	try bind_guard(Arg2, MapJ, Env, pos, State)
2413	catch
2414	  throw:{fail,_} -> bind_guard(Arg2, MapJ, Env, dont_know, State)
2415	end,
2416      case
2417        ((t_is_any_atom(true, Bool1, Opaques)
2418          andalso t_is_boolean(Bool2, Opaques))
2419         orelse
2420           (t_is_any_atom(true, Bool2, Opaques)
2421            andalso t_is_boolean(Bool1, Opaques)))
2422      of
2423	true -> {join_maps_end([Map1, Map2], MapJ), t_atom(true)};
2424	false -> signal_guard_fail(Eval, Guard, [Bool1, Bool2], State)
2425      end;
2426    neg ->
2427      {Map1, Type1} = bind_guard(Arg1, Map, Env, neg, State),
2428      case t_is_any_atom(false, Type1, Opaques) of
2429	false -> signal_guard_fail(Eval, Guard, [Type1, t_any()], State);
2430	true ->
2431	  {Map2, Type2} = bind_guard(Arg2, Map1, Env, neg, State),
2432	  case t_is_any_atom(false, Type2, Opaques) of
2433	    false -> signal_guard_fail(Eval, Guard, [Type1, Type2], State);
2434	    true -> {Map2, t_atom(false)}
2435	  end
2436      end;
2437    dont_know ->
2438      MapJ = join_maps_begin(Map),
2439      {Map1, Type1} = bind_guard(Arg1, MapJ, Env, dont_know, State),
2440      {Map2, Type2} = bind_guard(Arg2, MapJ, Env, dont_know, State),
2441      Bool1 = t_inf(Type1, t_boolean()),
2442      Bool2 = t_inf(Type2, t_boolean()),
2443      case t_is_none(Bool1) orelse t_is_none(Bool2) of
2444	true -> throw({fatal_fail, none});
2445	false ->
2446	  NewMap = join_maps_end([Map1, Map2], MapJ),
2447	  NewType =
2448	    case {t_atom_vals(Bool1, Opaques), t_atom_vals(Bool2, Opaques)} of
2449	      {['false'], ['false']} -> t_atom(false);
2450	      {['true'] , _        } -> t_atom(true);
2451	      {_        , ['true'] } -> t_atom(true);
2452              {unknown  , _        } ->
2453                signal_guard_fail(Eval, Guard, [Type1, Type2], State);
2454              {_        , unknown  } ->
2455                signal_guard_fail(Eval, Guard, [Type1, Type2], State);
2456	      {_        , _        } -> t_boolean()
2457	    end,
2458	  {NewMap, NewType}
2459      end
2460  end.
2461
2462handle_guard_not(Guard, Map, Env, Eval, State) ->
2463  [Arg] = cerl:call_args(Guard),
2464  Opaques = State#state.opaques,
2465  case Eval of
2466    neg ->
2467      {Map1, Type} = bind_guard(Arg, Map, Env, pos, State),
2468      case t_is_any_atom(true, Type, Opaques) of
2469	true -> {Map1, t_atom(false)};
2470	false ->
2471	  {_, Type0} = bind_guard(Arg, Map, Env, Eval, State),
2472	  signal_guard_fail(Eval, Guard, [Type0], State)
2473      end;
2474    pos ->
2475      {Map1, Type} = bind_guard(Arg, Map, Env, neg, State),
2476      case t_is_any_atom(false, Type, Opaques) of
2477	true -> {Map1, t_atom(true)};
2478	false ->
2479	  {_, Type0} = bind_guard(Arg, Map, Env, Eval, State),
2480	  signal_guard_fail(Eval, Guard, [Type0], State)
2481      end;
2482    dont_know ->
2483      {Map1, Type} = bind_guard(Arg, Map, Env, dont_know, State),
2484      Bool = t_inf(Type, t_boolean()),
2485      case t_is_none(Bool) of
2486	true -> throw({fatal_fail, none});
2487	false ->
2488	  case t_atom_vals(Bool, Opaques) of
2489	    ['true'] -> {Map1, t_atom(false)};
2490	    ['false'] -> {Map1, t_atom(true)};
2491	    [_, _] -> {Map1, Bool};
2492            unknown -> signal_guard_fail(Eval, Guard, [Type], State)
2493	  end
2494      end
2495  end.
2496
2497bind_guard_list(Guards, Map, Env, Eval, State) ->
2498  bind_guard_list(Guards, Map, Env, Eval, State, []).
2499
2500bind_guard_list([G|Gs], Map, Env, Eval, State, Acc) ->
2501  {Map1, T} = bind_guard(G, Map, Env, Eval, State),
2502  bind_guard_list(Gs, Map1, Env, Eval, State, [T|Acc]);
2503bind_guard_list([], Map, _Env, _Eval, _State, Acc) ->
2504  {Map, lists:reverse(Acc)}.
2505
2506handle_guard_map(Guard, Map, Env, State) ->
2507  Pairs = cerl:map_es(Guard),
2508  Arg = cerl:map_arg(Guard),
2509  {Map1, ArgType0} = bind_guard(Arg, Map, Env, dont_know, State),
2510  ArgType1 = t_inf(t_map(), ArgType0),
2511  case t_is_none_or_unit(ArgType1) of
2512    true -> {Map1, t_none()};
2513    false ->
2514      {Map2, TypePairs} = bind_guard_map_pairs(Pairs, Map1, Env, State, []),
2515      {Map2, lists:foldl(fun({KV,assoc},Acc) -> erl_types:t_map_put(KV,Acc);
2516			    ({KV,exact},Acc) -> erl_types:t_map_update(KV,Acc)
2517			 end, ArgType1, TypePairs)}
2518  end.
2519
2520bind_guard_map_pairs([], Map, _Env, _State, PairAcc) ->
2521  {Map, lists:reverse(PairAcc)};
2522bind_guard_map_pairs([Pair|Pairs], Map, Env, State, PairAcc) ->
2523  Key = cerl:map_pair_key(Pair),
2524  Val = cerl:map_pair_val(Pair),
2525  Op = cerl:map_pair_op(Pair),
2526  {Map1, [K,V]} = bind_guard_list([Key,Val],Map,Env,dont_know,State),
2527  bind_guard_map_pairs(Pairs, Map1, Env, State,
2528		       [{{K,V},cerl:concrete(Op)}|PairAcc]).
2529
2530-type eval() :: 'pos' | 'neg' | 'dont_know'.
2531
2532-spec signal_guard_fail(eval(), cerl:c_call(), [type()],
2533			state()) -> no_return().
2534
2535signal_guard_fail(Eval, Guard, ArgTypes, State) ->
2536  signal_guard_failure(Eval, Guard, ArgTypes, fail, State).
2537
2538-spec signal_guard_fatal_fail(eval(), cerl:c_call(), [erl_types:erl_type()],
2539			      state()) -> no_return().
2540
2541signal_guard_fatal_fail(Eval, Guard, ArgTypes, State) ->
2542  signal_guard_failure(Eval, Guard, ArgTypes, fatal_fail, State).
2543
2544signal_guard_failure(Eval, Guard, ArgTypes, Tag, State) ->
2545  Args = cerl:call_args(Guard),
2546  F = cerl:atom_val(cerl:call_name(Guard)),
2547  {M, F, A} = MFA = {cerl:atom_val(cerl:call_module(Guard)), F, length(Args)},
2548  Opaques = State#state.opaques,
2549  {Kind, XInfo} =
2550    case erl_bif_types:opaque_args(M, F, A, ArgTypes, Opaques) of
2551      [] ->
2552        {case Eval of
2553           neg -> neg_guard_fail;
2554           pos -> guard_fail;
2555           dont_know -> guard_fail
2556         end,
2557         []};
2558      Ns -> {opaque_guard, [Ns]}
2559    end,
2560  FArgs =
2561    case is_infix_op(MFA) of
2562      true ->
2563	[ArgType1, ArgType2] = ArgTypes,
2564	[Arg1, Arg2] = Args,
2565	[format_args_1([Arg1], [ArgType1], State),
2566         atom_to_list(F),
2567         format_args_1([Arg2], [ArgType2], State)] ++ XInfo;
2568      false ->
2569        [F, format_args(Args, ArgTypes, State)]
2570    end,
2571  Msg = {Kind, FArgs},
2572  throw({Tag, {Guard, Msg}}).
2573
2574is_infix_op({erlang, '=:=', 2}) -> true;
2575is_infix_op({erlang, '==', 2}) -> true;
2576is_infix_op({erlang, '=/=', 2}) -> true;
2577is_infix_op({erlang, '=/', 2}) -> true;
2578is_infix_op({erlang, '<', 2}) -> true;
2579is_infix_op({erlang, '=<', 2}) -> true;
2580is_infix_op({erlang, '>', 2}) -> true;
2581is_infix_op({erlang, '>=', 2}) -> true;
2582is_infix_op({M, F, A}) when is_atom(M), is_atom(F),
2583			    is_integer(A), 0 =< A, A =< 255 -> false.
2584
2585bif_args(M, F, A) ->
2586  case erl_bif_types:arg_types(M, F, A) of
2587    unknown -> lists:duplicate(A, t_any());
2588    List -> List
2589  end.
2590
2591bind_guard_case_clauses(Arg, Clauses, Map0, Env, Eval, State) ->
2592  Clauses1 = filter_fail_clauses(Clauses),
2593  Map = join_maps_begin(Map0),
2594  {GenMap, GenArgType} = bind_guard(Arg, Map, Env, dont_know, State),
2595  bind_guard_case_clauses(GenArgType, GenMap, Arg, Clauses1, Map, Env, Eval,
2596			  t_none(), [], State).
2597
2598filter_fail_clauses([Clause|Left]) ->
2599  case (cerl:clause_pats(Clause) =:= []) of
2600    true ->
2601      Body = cerl:clause_body(Clause),
2602      case cerl:is_literal(Body) andalso (cerl:concrete(Body) =:= fail) orelse
2603	cerl:is_c_primop(Body) andalso
2604	(cerl:atom_val(cerl:primop_name(Body)) =:= match_fail) of
2605	true -> filter_fail_clauses(Left);
2606	false -> [Clause|filter_fail_clauses(Left)]
2607      end;
2608    false ->
2609      [Clause|filter_fail_clauses(Left)]
2610  end;
2611filter_fail_clauses([]) ->
2612  [].
2613
2614bind_guard_case_clauses(GenArgType, GenMap, ArgExpr, [Clause|Left],
2615			Map, Env, Eval, AccType, AccMaps, State) ->
2616  Pats = cerl:clause_pats(Clause),
2617  {NewMap0, ArgType} =
2618    case Pats of
2619      [Pat] ->
2620	case cerl:is_literal(Pat) of
2621	  true ->
2622	    try
2623	      case cerl:concrete(Pat) of
2624		true -> bind_guard(ArgExpr, Map, Env, pos, State);
2625		false -> bind_guard(ArgExpr, Map, Env, neg, State);
2626		_ -> {GenMap, GenArgType}
2627	      end
2628	    catch
2629	      throw:{fail, _} -> {none, GenArgType}
2630	    end;
2631	  false ->
2632	    {GenMap, GenArgType}
2633	end;
2634      _ -> {GenMap, GenArgType}
2635    end,
2636  NewMap1 =
2637    case Pats =:= [] of
2638      true -> NewMap0;
2639      false ->
2640	case t_is_none(ArgType) of
2641	  true -> none;
2642	  false ->
2643	    ArgTypes = case t_is_any(ArgType) of
2644			 true -> Any = t_any(), [Any || _ <- Pats];
2645			 false -> t_to_tlist(ArgType)
2646		       end,
2647	    case bind_pat_vars(Pats, ArgTypes, [], NewMap0, State) of
2648	      {error, _, _, _, _} -> none;
2649	      {PatMap, _PatTypes} -> PatMap
2650	    end
2651	end
2652    end,
2653  Guard = cerl:clause_guard(Clause),
2654  GenPatType = dialyzer_typesig:get_safe_underapprox(Pats, Guard),
2655  NewGenArgType = t_subtract(GenArgType, GenPatType),
2656  case (NewMap1 =:= none) orelse t_is_none(GenArgType) of
2657    true ->
2658      bind_guard_case_clauses(NewGenArgType, GenMap, ArgExpr, Left, Map, Env,
2659			      Eval, AccType, AccMaps, State);
2660    false ->
2661      {NewAccType, NewAccMaps} =
2662	try
2663	  {NewMap2, GuardType} = bind_guard(Guard, NewMap1, Env, pos, State),
2664	  case t_is_none(t_inf(t_atom(true), GuardType)) of
2665	    true -> throw({fail, none});
2666	    false -> ok
2667	  end,
2668	  {NewMap3, CType} = bind_guard(cerl:clause_body(Clause), NewMap2,
2669					Env, Eval, State),
2670          Opaques = State#state.opaques,
2671	  case Eval of
2672	    pos ->
2673	      case t_is_any_atom(true, CType, Opaques) of
2674		true -> ok;
2675		false -> throw({fail, none})
2676	      end;
2677	    neg ->
2678	      case t_is_any_atom(false, CType, Opaques) of
2679		true -> ok;
2680		false -> throw({fail, none})
2681	      end;
2682	    dont_know ->
2683	      ok
2684	  end,
2685	  {t_sup(AccType, CType), [NewMap3|AccMaps]}
2686	catch
2687	  throw:{fail, _What} -> {AccType, AccMaps}
2688	end,
2689      bind_guard_case_clauses(NewGenArgType, GenMap, ArgExpr, Left, Map, Env,
2690			      Eval, NewAccType, NewAccMaps, State)
2691  end;
2692bind_guard_case_clauses(_GenArgType, _GenMap, _ArgExpr, [], Map, _Env, _Eval,
2693			AccType, AccMaps, _State) ->
2694  case t_is_none(AccType) of
2695    true -> throw({fail, none});
2696    false -> {join_maps_end(AccMaps, Map), AccType}
2697  end.
2698
2699%%% ===========================================================================
2700%%%
2701%%%  Maps and types.
2702%%%
2703%%% ===========================================================================
2704
2705map__new() ->
2706  #map{}.
2707
2708%% join_maps_begin pushes 'modified' to the stack; join_maps pops
2709%% 'modified' from the stack.
2710
2711join_maps_begin(#map{modified = M, modified_stack = S, ref = Ref} = Map) ->
2712  Map#map{ref = make_ref(), modified = [], modified_stack = [{M,Ref} | S]}.
2713
2714join_maps_end(Maps, MapOut) ->
2715  #map{ref = Ref, modified_stack = [{M1,R1} | S]} = MapOut,
2716  true = lists:all(fun(M) -> M#map.ref =:= Ref end, Maps), % sanity
2717  Keys0 = lists:usort(lists:append([M#map.modified || M <- Maps])),
2718  #map{map = Map, subst = Subst} = MapOut,
2719  Keys = [Key ||
2720           Key <- Keys0,
2721           maps:is_key(Key, Map) orelse maps:is_key(Key, Subst)],
2722  Out = case Maps of
2723          [] -> join_maps(Maps, MapOut);
2724          _ -> join_maps(Keys, Maps, MapOut)
2725        end,
2726  debug_join_check(Maps, MapOut, Out),
2727  Out#map{ref = R1,
2728          modified = Out#map.modified ++ M1, % duplicates possible
2729          modified_stack = S}.
2730
2731join_maps(Maps, MapOut) ->
2732  #map{map = Map, subst = Subst} = MapOut,
2733  Keys = ordsets:from_list(maps:keys(Map) ++ maps:keys(Subst)),
2734  join_maps(Keys, Maps, MapOut).
2735
2736join_maps(Keys, Maps, MapOut) ->
2737  KTs = join_maps_collect(Keys, Maps, MapOut),
2738  lists:foldl(fun({K, T}, M) -> enter_type(K, T, M) end, MapOut, KTs).
2739
2740join_maps_collect([Key|Left], Maps, MapOut) ->
2741  Type = join_maps_one_key(Maps, Key, t_none()),
2742  case t_is_equal(lookup_type(Key, MapOut), Type) of
2743    true ->  join_maps_collect(Left, Maps, MapOut);
2744    false -> [{Key, Type} | join_maps_collect(Left, Maps, MapOut)]
2745  end;
2746join_maps_collect([], _Maps, _MapOut) ->
2747  [].
2748
2749join_maps_one_key([Map|Left], Key, AccType) ->
2750  case t_is_any(AccType) of
2751    true ->
2752      %% We can stop here
2753      AccType;
2754    false ->
2755      join_maps_one_key(Left, Key, t_sup(lookup_type(Key, Map), AccType))
2756  end;
2757join_maps_one_key([], _Key, AccType) ->
2758  AccType.
2759
2760-ifdef(DEBUG).
2761debug_join_check(Maps, MapOut, Out) ->
2762  #map{map = Map, subst = Subst} = Out,
2763  #map{map = Map2, subst = Subst2} = join_maps(Maps, MapOut),
2764  F = fun(D) -> lists:keysort(1, maps:to_list(D)) end,
2765  [throw({bug, join_maps}) ||
2766    F(Map) =/= F(Map2) orelse F(Subst) =/= F(Subst2)].
2767-else.
2768debug_join_check(_Maps, _MapOut, _Out) -> ok.
2769-endif.
2770
2771enter_type_lists([Key|KeyTail], [Val|ValTail], Map) ->
2772  Map1 = enter_type(Key, Val, Map),
2773  enter_type_lists(KeyTail, ValTail, Map1);
2774enter_type_lists([], [], Map) ->
2775  Map.
2776
2777enter_type_list([{Key, Val}|Left], Map) ->
2778  Map1 = enter_type(Key, Val, Map),
2779  enter_type_list(Left, Map1);
2780enter_type_list([], Map) ->
2781  Map.
2782
2783enter_type(Key, Val, MS) ->
2784  case cerl:is_literal(Key) of
2785    true -> MS;
2786    false ->
2787      case cerl:is_c_values(Key) of
2788	true ->
2789          Keys = cerl:values_es(Key),
2790	  case t_is_any(Val) orelse t_is_none(Val) of
2791	    true ->
2792	      enter_type_lists(Keys, [Val || _ <- Keys], MS);
2793	    false ->
2794	      enter_type_lists(Keys, t_to_tlist(Val), MS)
2795	  end;
2796	false ->
2797          #map{map = Map, subst = Subst} = MS,
2798	  KeyLabel = get_label(Key),
2799	  case maps:find(KeyLabel, Subst) of
2800	    {ok, NewKey} ->
2801	      ?debug("Binding ~p to ~p\n", [KeyLabel, NewKey]),
2802	      enter_type(NewKey, Val, MS);
2803	    error ->
2804	      ?debug("Entering ~p :: ~s\n", [KeyLabel, t_to_string(Val)]),
2805	      case maps:find(KeyLabel, Map) of
2806		{ok, Value} ->
2807                  case erl_types:t_is_equal(Val, Value) of
2808                    true -> MS;
2809                    false -> store_map(KeyLabel, Val, MS)
2810                  end;
2811		error -> store_map(KeyLabel, Val, MS)
2812	      end
2813	  end
2814      end
2815  end.
2816
2817store_map(Key, Val, #map{map = Map, ref = undefined} = MapRec) ->
2818  MapRec#map{map = maps:put(Key, Val, Map)};
2819store_map(Key, Val, #map{map = Map, modified = Mod} = MapRec) ->
2820  MapRec#map{map = maps:put(Key, Val, Map), modified = [Key | Mod]}.
2821
2822enter_subst(Key, Val0, #map{subst = Subst} = MS) ->
2823  KeyLabel = get_label(Key),
2824  Val = dialyzer_utils:refold_pattern(Val0),
2825  case cerl:is_literal(Val) of
2826    true ->
2827      store_map(KeyLabel, literal_type(Val), MS);
2828    false ->
2829      case cerl:is_c_var(Val) of
2830	false -> MS;
2831	true ->
2832	  ValLabel = get_label(Val),
2833	  case maps:find(ValLabel, Subst) of
2834	    {ok, NewVal} ->
2835	      enter_subst(Key, NewVal, MS);
2836	    error ->
2837	      if KeyLabel =:= ValLabel -> MS;
2838		 true ->
2839		  ?debug("Subst: storing ~p = ~p\n", [KeyLabel, ValLabel]),
2840                  store_subst(KeyLabel, ValLabel, MS)
2841	      end
2842	  end
2843      end
2844  end.
2845
2846store_subst(Key, Val, #map{subst = S, ref = undefined} = Map) ->
2847  Map#map{subst = maps:put(Key, Val, S)};
2848store_subst(Key, Val, #map{subst = S, modified = Mod} = Map) ->
2849  Map#map{subst = maps:put(Key, Val, S), modified = [Key | Mod]}.
2850
2851lookup_type(Key, #map{map = Map, subst = Subst}) ->
2852  lookup(Key, Map, Subst, t_none()).
2853
2854lookup(Key, Map, Subst, AnyNone) ->
2855  case cerl:is_literal(Key) of
2856    true -> literal_type(Key);
2857    false ->
2858      Label = get_label(Key),
2859      case maps:find(Label, Subst) of
2860	{ok, NewKey} -> lookup(NewKey, Map, Subst, AnyNone);
2861	error ->
2862	  case maps:find(Label, Map) of
2863	    {ok, Val} -> Val;
2864	    error -> AnyNone
2865	  end
2866      end
2867  end.
2868
2869lookup_fun_sig(Fun, Callgraph, Plt) ->
2870  MFAorLabel =
2871    case dialyzer_callgraph:lookup_name(Fun, Callgraph) of
2872      error -> Fun;
2873      {ok, MFA} -> MFA
2874    end,
2875  dialyzer_plt:lookup(Plt, MFAorLabel).
2876
2877literal_type(Lit) ->
2878  t_from_term(cerl:concrete(Lit)).
2879
2880mark_as_fresh([Tree|Left], Map) ->
2881  SubTrees1 = lists:append(cerl:subtrees(Tree)),
2882  {SubTrees2, Map1} =
2883    case cerl:type(Tree) of
2884      bitstr ->
2885	%% The Size field is not fresh.
2886	{SubTrees1 -- [cerl:bitstr_size(Tree)], Map};
2887      map_pair ->
2888	%% The keys are not fresh
2889	{SubTrees1 -- [cerl:map_pair_key(Tree)], Map};
2890      var ->
2891	{SubTrees1, enter_type(Tree, t_any(), Map)};
2892      _ ->
2893	{SubTrees1, Map}
2894    end,
2895  mark_as_fresh(SubTrees2 ++ Left, Map1);
2896mark_as_fresh([], Map) ->
2897  Map.
2898
2899-ifdef(DEBUG).
2900debug_pp_map(#map{map = Map}=MapRec) ->
2901  Keys = maps:keys(Map),
2902  io:format("Map:\n", []),
2903  lists:foreach(fun (Key) ->
2904		    io:format("\t~w :: ~s\n",
2905			      [Key, t_to_string(lookup_type(Key, MapRec))])
2906		end, Keys),
2907  ok.
2908-else.
2909debug_pp_map(_Map) -> ok.
2910-endif.
2911
2912%%% ===========================================================================
2913%%%
2914%%%  Utilities
2915%%%
2916%%% ===========================================================================
2917
2918get_label(L) when is_integer(L) ->
2919  L;
2920get_label(T) ->
2921  cerl_trees:get_label(T).
2922
2923t_is_simple(ArgType, State) ->
2924  Opaques = State#state.opaques,
2925  t_is_atom(ArgType, Opaques) orelse t_is_number(ArgType, Opaques)
2926    orelse t_is_port(ArgType, Opaques)
2927    orelse t_is_pid(ArgType, Opaques) orelse t_is_reference(ArgType, Opaques)
2928    orelse t_is_nil(ArgType, Opaques).
2929
2930remove_local_opaque_types(Type, Opaques) ->
2931  t_unopaque(Type, Opaques).
2932
2933%% t_is_structured(ArgType) ->
2934%%   case t_is_nil(ArgType) of
2935%%     true -> false;
2936%%     false ->
2937%%       SType = t_inf(t_sup([t_list(), t_tuple(), t_binary()]), ArgType),
2938%%       t_is_equal(ArgType, SType)
2939%%   end.
2940
2941is_call_to_send(Tree) ->
2942  case cerl:is_c_call(Tree) of
2943    false -> false;
2944    true ->
2945      Mod = cerl:call_module(Tree),
2946      Name = cerl:call_name(Tree),
2947      Arity = cerl:call_arity(Tree),
2948      cerl:is_c_atom(Mod)
2949	andalso cerl:is_c_atom(Name)
2950        andalso is_send(cerl:atom_val(Name))
2951	andalso (cerl:atom_val(Mod) =:= erlang)
2952	andalso (Arity =:= 2)
2953  end.
2954
2955is_send('!') -> true;
2956is_send(send) -> true;
2957is_send(_) -> false.
2958
2959is_lc_simple_list(Tree, TreeType, State) ->
2960  Opaques = State#state.opaques,
2961  Ann = cerl:get_ann(Tree),
2962  lists:member(list_comprehension, Ann)
2963    andalso t_is_list(TreeType)
2964    andalso t_is_simple(t_list_elements(TreeType, Opaques), State).
2965
2966filter_match_fail([Clause] = Cls) ->
2967  Body = cerl:clause_body(Clause),
2968  case cerl:type(Body) of
2969    primop ->
2970      case cerl:atom_val(cerl:primop_name(Body)) of
2971	match_fail -> [];
2972	raise -> [];
2973	_ -> Cls
2974      end;
2975    _ -> Cls
2976  end;
2977filter_match_fail([H|T]) ->
2978  [H|filter_match_fail(T)];
2979filter_match_fail([]) ->
2980  %% This can actually happen, for example in
2981  %%      receive after 1 -> ok end
2982  [].
2983
2984%%% ===========================================================================
2985%%%
2986%%%  The State.
2987%%%
2988%%% ===========================================================================
2989
2990state__new(Callgraph, Codeserver, Tree, Plt, Module, Records) ->
2991  Opaques = erl_types:t_opaque_from_records(Records),
2992  {TreeMap, FunHomes} = build_tree_map(Tree, Callgraph),
2993  Funs = dict:fetch_keys(TreeMap),
2994  FunTab = init_fun_tab(Funs, dict:new(), TreeMap, Callgraph, Plt),
2995  ExportedFuns =
2996    [Fun || Fun <- Funs--[top], dialyzer_callgraph:is_escaping(Fun, Callgraph)],
2997  Work = init_work(ExportedFuns),
2998  Env = lists:foldl(fun(Fun, Env) -> dict:store(Fun, map__new(), Env) end,
2999		    dict:new(), Funs),
3000  #state{callgraph = Callgraph, codeserver = Codeserver,
3001         envs = Env, fun_tab = FunTab, fun_homes = FunHomes, opaques = Opaques,
3002	 plt = Plt, races = dialyzer_races:new(), records = Records,
3003	 warning_mode = false, warnings = [], work = Work, tree_map = TreeMap,
3004	 module = Module}.
3005
3006state__warning_mode(#state{warning_mode = WM}) ->
3007  WM.
3008
3009state__set_warning_mode(#state{tree_map = TreeMap, fun_tab = FunTab,
3010                               races = Races} = State) ->
3011  ?debug("==========\nStarting warning pass\n==========\n", []),
3012  Funs = dict:fetch_keys(TreeMap),
3013  State#state{work = init_work([top|Funs--[top]]),
3014	      fun_tab = FunTab, warning_mode = true,
3015              races = dialyzer_races:put_race_analysis(true, Races)}.
3016
3017state__race_analysis(Analysis, #state{races = Races} = State) ->
3018  State#state{races = dialyzer_races:put_race_analysis(Analysis, Races)}.
3019
3020state__renew_curr_fun(CurrFun, CurrFunLabel,
3021                      #state{races = Races} = State) ->
3022  State#state{races = dialyzer_races:put_curr_fun(CurrFun, CurrFunLabel,
3023                                                  Races)}.
3024
3025state__renew_fun_args(Args, #state{races = Races} = State) ->
3026  case state__warning_mode(State) of
3027    true -> State;
3028    false ->
3029      State#state{races = dialyzer_races:put_fun_args(Args, Races)}
3030  end.
3031
3032state__renew_race_list(RaceList, RaceListSize,
3033                       #state{races = Races} = State) ->
3034  State#state{races = dialyzer_races:put_race_list(RaceList, RaceListSize,
3035                                                   Races)}.
3036
3037state__renew_warnings(Warnings, State) ->
3038  State#state{warnings = Warnings}.
3039
3040-spec state__add_warning(raw_warning(), state()) -> state().
3041
3042state__add_warning(Warn, #state{warnings = Warnings} = State) ->
3043  State#state{warnings = [Warn|Warnings]}.
3044
3045state__add_warning(State, Tag, Tree, Msg) ->
3046  state__add_warning(State, Tag, Tree, Msg, false).
3047
3048state__add_warning(#state{warning_mode = false} = State, _, _, _, _) ->
3049  State;
3050state__add_warning(#state{warnings = Warnings, warning_mode = true} = State,
3051		   Tag, Tree, Msg, Force) ->
3052  Ann = cerl:get_ann(Tree),
3053  case Force of
3054    true ->
3055      WarningInfo = {get_file(Ann),
3056                     abs(get_line(Ann)),
3057                     State#state.curr_fun},
3058      Warn = {Tag, WarningInfo, Msg},
3059      ?debug("MSG ~s\n", [dialyzer:format_warning(Warn)]),
3060      State#state{warnings = [Warn|Warnings]};
3061    false ->
3062      case is_compiler_generated(Ann) of
3063        true -> State;
3064        false ->
3065          WarningInfo = {get_file(Ann), get_line(Ann), State#state.curr_fun},
3066          Warn = {Tag, WarningInfo, Msg},
3067          case Tag of
3068            ?WARN_CONTRACT_RANGE -> ok;
3069            _ -> ?debug("MSG ~s\n", [dialyzer:format_warning(Warn)])
3070          end,
3071          State#state{warnings = [Warn|Warnings]}
3072      end
3073  end.
3074
3075state__remove_added_warnings(OldState, NewState) ->
3076  #state{warnings = OldWarnings} = OldState,
3077  #state{warnings = NewWarnings} = NewState,
3078  {NewWarnings -- OldWarnings, NewState#state{warnings = OldWarnings}}.
3079
3080state__add_warnings(Warns, #state{warnings = Warnings} = State) ->
3081  State#state{warnings = Warns ++ Warnings}.
3082
3083-spec state__set_curr_fun(curr_fun(), state()) -> state().
3084
3085state__set_curr_fun(undefined, State) ->
3086  State#state{curr_fun = undefined};
3087state__set_curr_fun(FunLbl, State) ->
3088  State#state{curr_fun = find_function(FunLbl, State)}.
3089
3090-spec state__find_function(mfa_or_funlbl(), state()) -> mfa_or_funlbl().
3091
3092state__find_function(FunLbl, State) ->
3093  find_function(FunLbl, State).
3094
3095state__get_race_warnings(#state{races = Races} = State) ->
3096  {Races1, State1} = dialyzer_races:get_race_warnings(Races, State),
3097  State1#state{races = Races1}.
3098
3099state__get_warnings(#state{tree_map = TreeMap, fun_tab = FunTab,
3100			   callgraph = Callgraph, plt = Plt} = State) ->
3101  FoldFun =
3102    fun({top, _}, AccState) -> AccState;
3103       ({FunLbl, Fun}, AccState) ->
3104        AccState1 = state__set_curr_fun(FunLbl, AccState),
3105	{NotCalled, Ret} =
3106	  case dict:fetch(get_label(Fun), FunTab) of
3107	    {not_handled, {_Args0, Ret0}} -> {true, Ret0};
3108	    {_Args0, Ret0} -> {false, Ret0}
3109	  end,
3110	case NotCalled of
3111	  true ->
3112            case dialyzer_callgraph:lookup_name(FunLbl, Callgraph) of
3113              error -> AccState1;
3114              {ok, {_M, F, A}} ->
3115                Msg = {unused_fun, [F, A]},
3116                state__add_warning(AccState1, ?WARN_NOT_CALLED, Fun, Msg)
3117            end;
3118	  false ->
3119	    {Name, Contract} =
3120	      case dialyzer_callgraph:lookup_name(FunLbl, Callgraph) of
3121		error -> {[], none};
3122		{ok, {_M, F, A} = MFA} ->
3123		  {[F, A], dialyzer_plt:lookup_contract(Plt, MFA)}
3124	      end,
3125	    case t_is_none(Ret) of
3126	      true ->
3127		%% Check if the function has a contract that allows this.
3128		Warn =
3129		  case Contract of
3130		    none -> not parent_allows_this(FunLbl, AccState1);
3131		    {value, C} ->
3132		      GenRet = dialyzer_contracts:get_contract_return(C),
3133		      not t_is_unit(GenRet)
3134		  end,
3135		case Warn of
3136		  true ->
3137		    case classify_returns(Fun) of
3138		      no_match ->
3139			Msg = {no_return, [no_match|Name]},
3140			state__add_warning(AccState1, ?WARN_RETURN_NO_RETURN,
3141					   Fun, Msg);
3142		      only_explicit ->
3143			Msg = {no_return, [only_explicit|Name]},
3144			state__add_warning(AccState1, ?WARN_RETURN_ONLY_EXIT,
3145					   Fun, Msg);
3146		      only_normal ->
3147			Msg = {no_return, [only_normal|Name]},
3148			state__add_warning(AccState1, ?WARN_RETURN_NO_RETURN,
3149					   Fun, Msg);
3150		      both ->
3151			Msg = {no_return, [both|Name]},
3152			state__add_warning(AccState1, ?WARN_RETURN_NO_RETURN,
3153					   Fun, Msg)
3154		    end;
3155		  false ->
3156		    AccState
3157		end;
3158	      false ->
3159		AccState
3160	    end
3161	end
3162    end,
3163  #state{warnings = Warn} = lists:foldl(FoldFun, State, dict:to_list(TreeMap)),
3164  Warn.
3165
3166state__is_escaping(Fun, #state{callgraph = Callgraph}) ->
3167  dialyzer_callgraph:is_escaping(Fun, Callgraph).
3168
3169state__lookup_type_for_letrec(Var, #state{callgraph = Callgraph} = State) ->
3170  Label = get_label(Var),
3171  case dialyzer_callgraph:lookup_letrec(Label, Callgraph) of
3172    error -> error;
3173    {ok, FunLabel} ->
3174      {ok, state__fun_type(FunLabel, State)}
3175  end.
3176
3177state__lookup_name({_, _, _} = MFA, #state{}) ->
3178  MFA;
3179state__lookup_name(top, #state{}) ->
3180  top;
3181state__lookup_name(Fun, #state{callgraph = Callgraph}) ->
3182  case dialyzer_callgraph:lookup_name(Fun, Callgraph) of
3183    {ok, MFA} -> MFA;
3184    error -> Fun
3185  end.
3186
3187state__lookup_record(Tag, Arity, #state{records = Records}) ->
3188  case erl_types:lookup_record(Tag, Arity, Records) of
3189    {ok, Fields} ->
3190      RecType =
3191        t_tuple([t_atom(Tag)|
3192                 [FieldType || {_FieldName, _Abstr, FieldType} <- Fields]]),
3193      {ok, RecType};
3194    error ->
3195      error
3196  end.
3197
3198state__get_args_and_status(Tree, #state{fun_tab = FunTab}) ->
3199  Fun = get_label(Tree),
3200  case dict:find(Fun, FunTab) of
3201    {ok, {not_handled, {ArgTypes, _}}} -> {ArgTypes, false};
3202    {ok, {ArgTypes, _}} -> {ArgTypes, true}
3203  end.
3204
3205build_tree_map(Tree, Callgraph) ->
3206  Fun =
3207    fun(T, {Dict, Homes, FunLbls} = Acc) ->
3208	case cerl:is_c_fun(T) of
3209	  true ->
3210            FunLbl = get_label(T),
3211	    Dict1 = dict:store(FunLbl, T, Dict),
3212            case catch dialyzer_callgraph:lookup_name(FunLbl, Callgraph) of
3213              {ok, MFA} ->
3214                F2 =
3215                  fun(Lbl, Dict0) ->
3216                      dict:store(Lbl, MFA, Dict0)
3217                  end,
3218                Homes1 = lists:foldl(F2, Homes, [FunLbl|FunLbls]),
3219                {Dict1, Homes1, []};
3220              _ ->
3221                {Dict1, Homes, [FunLbl|FunLbls]}
3222            end;
3223	  false ->
3224            Acc
3225	end
3226    end,
3227  Dict0 = dict:new(),
3228  {Dict, Homes, _} = cerl_trees:fold(Fun, {Dict0, Dict0, []}, Tree),
3229  {Dict, Homes}.
3230
3231init_fun_tab([top|Left], Dict, TreeMap, Callgraph, Plt) ->
3232  NewDict = dict:store(top, {[], t_none()}, Dict),
3233  init_fun_tab(Left, NewDict, TreeMap, Callgraph, Plt);
3234init_fun_tab([Fun|Left], Dict, TreeMap, Callgraph, Plt) ->
3235  Arity = cerl:fun_arity(dict:fetch(Fun, TreeMap)),
3236  FunEntry =
3237    case dialyzer_callgraph:is_escaping(Fun, Callgraph) of
3238      true ->
3239        Args = lists:duplicate(Arity, t_any()),
3240	case lookup_fun_sig(Fun, Callgraph, Plt) of
3241	  none -> {Args, t_unit()};
3242	  {value, {RetType, _}} ->
3243	    case t_is_none(RetType) of
3244	      true -> {Args, t_none()};
3245	      false -> {Args, t_unit()}
3246	    end
3247	end;
3248      false -> {not_handled, {lists:duplicate(Arity, t_none()), t_unit()}}
3249    end,
3250  NewDict = dict:store(Fun, FunEntry, Dict),
3251  init_fun_tab(Left, NewDict, TreeMap, Callgraph, Plt);
3252init_fun_tab([], Dict, _TreeMap, _Callgraph, _Plt) ->
3253  ?debug("DICT:~p\n",[dict:to_list(Dict)]),
3254  Dict.
3255
3256state__update_fun_env(Tree, Map, #state{envs = Envs} = State) ->
3257  NewEnvs = dict:store(get_label(Tree), Map, Envs),
3258  State#state{envs = NewEnvs}.
3259
3260state__fun_env(Tree, #state{envs = Envs}) ->
3261  Fun = get_label(Tree),
3262  case dict:find(Fun, Envs) of
3263    error -> none;
3264    {ok, Map} -> Map
3265  end.
3266
3267state__clean_not_called(#state{fun_tab = FunTab} = State) ->
3268  NewFunTab =
3269    dict:map(fun(top, Entry) -> Entry;
3270		(_Fun, {not_handled, {Args, _}}) -> {Args, t_none()};
3271		(_Fun, Entry) -> Entry
3272	     end, FunTab),
3273  State#state{fun_tab = NewFunTab}.
3274
3275state__all_fun_types(State) ->
3276  #state{fun_tab = FunTab} = state__clean_not_called(State),
3277  Tab1 = dict:erase(top, FunTab),
3278  dict:map(fun(_Fun, {Args, Ret}) -> t_fun(Args, Ret)end, Tab1).
3279
3280state__fun_type(Fun, #state{fun_tab = FunTab}) ->
3281  Label =
3282    if is_integer(Fun) -> Fun;
3283       true -> get_label(Fun)
3284    end,
3285  Entry = dict:find(Label, FunTab),
3286  ?debug("FunType ~p:~p\n",[Label, Entry]),
3287  case Entry of
3288    {ok, {not_handled, {A, R}}} ->
3289      t_fun(A, R);
3290    {ok, {A, R}} ->
3291      t_fun(A, R)
3292  end.
3293
3294state__update_fun_entry(Tree, ArgTypes, Out0,
3295			#state{fun_tab=FunTab, callgraph=CG, plt=Plt} = State)->
3296  Fun = get_label(Tree),
3297  Out1 =
3298    if Fun =:= top -> Out0;
3299       true ->
3300	case lookup_fun_sig(Fun, CG, Plt) of
3301	  {value, {SigRet, _}} -> t_inf(SigRet, Out0);
3302	  none -> Out0
3303	end
3304    end,
3305  Out = t_limit(Out1, ?TYPE_LIMIT),
3306  {ok, {OldArgTypes, OldOut}} = dict:find(Fun, FunTab),
3307  SameArgs = lists:all(fun({A, B}) -> erl_types:t_is_equal(A, B)
3308                       end, lists:zip(OldArgTypes, ArgTypes)),
3309  SameOut = t_is_equal(OldOut, Out),
3310  if
3311    SameArgs, SameOut ->
3312      ?debug("Fixpoint for ~w: ~s\n",
3313	     [state__lookup_name(Fun, State),
3314	      t_to_string(t_fun(ArgTypes, Out))]),
3315      State;
3316    true ->
3317      %% Can only happen in self-recursive functions.
3318      NewEntry = {OldArgTypes, Out},
3319      ?debug("New Entry for ~w: ~s\n",
3320	     [state__lookup_name(Fun, State),
3321	      t_to_string(t_fun(OldArgTypes, Out))]),
3322      NewFunTab = dict:store(Fun, NewEntry, FunTab),
3323      State1 = State#state{fun_tab = NewFunTab},
3324      state__add_work_from_fun(Tree, State1)
3325  end.
3326
3327state__add_work_from_fun(_Tree, #state{warning_mode = true} = State) ->
3328  State;
3329state__add_work_from_fun(Tree, #state{callgraph = Callgraph,
3330				      tree_map = TreeMap} = State) ->
3331  case get_label(Tree) of
3332    top -> State;
3333    Label when is_integer(Label) ->
3334      case dialyzer_callgraph:in_neighbours(Label, Callgraph) of
3335	none -> State;
3336	MFAList ->
3337	  LabelList = [dialyzer_callgraph:lookup_label(MFA, Callgraph)
3338		       || MFA <- MFAList],
3339	  %% Must filter the result for results in this module.
3340	  FilteredList = [L || {ok, L} <- LabelList, dict:is_key(L, TreeMap)],
3341	  ?debug("~w: Will try to add:~w\n",
3342		 [state__lookup_name(Label, State), MFAList]),
3343	  lists:foldl(fun(L, AccState) ->
3344			  state__add_work(L, AccState)
3345		      end, State, FilteredList)
3346      end
3347  end.
3348
3349state__add_work(external, State) ->
3350  State;
3351state__add_work(top, State) ->
3352  State;
3353state__add_work(Fun, #state{work = Work} = State) ->
3354  NewWork = add_work(Fun, Work),
3355  State#state{work = NewWork}.
3356
3357state__get_work(#state{work = Work, tree_map = TreeMap} = State) ->
3358  case get_work(Work) of
3359    none -> none;
3360    {Fun, NewWork} ->
3361      {dict:fetch(Fun, TreeMap), State#state{work = NewWork}}
3362  end.
3363
3364state__lookup_call_site(Tree, #state{callgraph = Callgraph}) ->
3365  Label = get_label(Tree),
3366  dialyzer_callgraph:lookup_call_site(Label, Callgraph).
3367
3368state__fun_info(external, #state{}) ->
3369  external;
3370state__fun_info({_, _, _} = MFA, #state{plt = PLT}) ->
3371  {MFA,
3372   dialyzer_plt:lookup(PLT, MFA),
3373   dialyzer_plt:lookup_contract(PLT, MFA),
3374   t_any()};
3375state__fun_info(Fun, #state{callgraph = CG, fun_tab = FunTab, plt = PLT}) ->
3376  {Sig, Contract} =
3377    case dialyzer_callgraph:lookup_name(Fun, CG) of
3378      error ->
3379	{dialyzer_plt:lookup(PLT, Fun), none};
3380      {ok, MFA} ->
3381	{dialyzer_plt:lookup(PLT, MFA), dialyzer_plt:lookup_contract(PLT, MFA)}
3382    end,
3383  LocalRet =
3384    case dict:fetch(Fun, FunTab) of
3385      {not_handled, {_Args, Ret}} -> Ret;
3386      {_Args, Ret} -> Ret
3387    end,
3388  ?debug("LocalRet: ~s\n", [t_to_string(LocalRet)]),
3389  {Fun, Sig, Contract, LocalRet}.
3390
3391forward_args(Fun, ArgTypes, #state{work = Work, fun_tab = FunTab} = State) ->
3392  {OldArgTypes, OldOut, Fixpoint} =
3393    case dict:find(Fun, FunTab) of
3394      {ok, {not_handled, {OldArgTypes0, OldOut0}}} ->
3395	{OldArgTypes0, OldOut0, false};
3396      {ok, {OldArgTypes0, OldOut0}} ->
3397	{OldArgTypes0, OldOut0,
3398	 t_is_subtype(t_product(ArgTypes), t_product(OldArgTypes0))}
3399    end,
3400  case Fixpoint of
3401    true -> State;
3402    false ->
3403      NewArgTypes = [t_sup(X, Y) ||
3404                      {X, Y} <- lists:zip(ArgTypes, OldArgTypes)],
3405      NewWork = add_work(Fun, Work),
3406      ?debug("~w: forwarding args ~s\n",
3407	     [state__lookup_name(Fun, State),
3408	      t_to_string(t_product(NewArgTypes))]),
3409      NewFunTab = dict:store(Fun, {NewArgTypes, OldOut}, FunTab),
3410      State#state{work = NewWork, fun_tab = NewFunTab}
3411  end.
3412
3413-spec state__cleanup(state()) -> state().
3414
3415state__cleanup(#state{callgraph = Callgraph,
3416                      races = Races,
3417                      records = Records}) ->
3418  #state{callgraph = dialyzer_callgraph:cleanup(Callgraph),
3419         races = dialyzer_races:cleanup(Races),
3420         records = Records}.
3421
3422-spec state__duplicate(state()) -> state().
3423
3424state__duplicate(#state{callgraph = Callgraph} = State) ->
3425  State#state{callgraph = dialyzer_callgraph:duplicate(Callgraph)}.
3426
3427-spec dispose_state(state()) -> ok.
3428
3429dispose_state(#state{callgraph = Callgraph}) ->
3430  dialyzer_callgraph:dispose_race_server(Callgraph).
3431
3432-spec state__get_callgraph(state()) -> dialyzer_callgraph:callgraph().
3433
3434state__get_callgraph(#state{callgraph = Callgraph}) ->
3435  Callgraph.
3436
3437-spec state__get_races(state()) -> dialyzer_races:races().
3438
3439state__get_races(#state{races = Races}) ->
3440  Races.
3441
3442-spec state__get_records(state()) -> types().
3443
3444state__get_records(#state{records = Records}) ->
3445  Records.
3446
3447-spec state__put_callgraph(dialyzer_callgraph:callgraph(), state()) ->
3448  state().
3449
3450state__put_callgraph(Callgraph, State) ->
3451  State#state{callgraph = Callgraph}.
3452
3453-spec state__put_races(dialyzer_races:races(), state()) -> state().
3454
3455state__put_races(Races, State) ->
3456  State#state{races = Races}.
3457
3458-spec state__records_only(state()) -> state().
3459
3460state__records_only(#state{records = Records}) ->
3461  #state{records = Records}.
3462
3463%%% ===========================================================================
3464%%%
3465%%%  Races
3466%%%
3467%%% ===========================================================================
3468
3469is_race_analysis_enabled(#state{races = Races, callgraph = Callgraph}) ->
3470  RaceDetection = dialyzer_callgraph:get_race_detection(Callgraph),
3471  RaceAnalysis = dialyzer_races:get_race_analysis(Races),
3472  RaceDetection andalso RaceAnalysis.
3473
3474get_race_list_and_size(#state{races = Races}) ->
3475  dialyzer_races:get_race_list_and_size(Races).
3476
3477renew_race_code(#state{races = Races, callgraph = Callgraph,
3478		       warning_mode = WarningMode} = State) ->
3479  case WarningMode of
3480    true -> State;
3481    false ->
3482      NewCallgraph = dialyzer_callgraph:renew_race_code(Races, Callgraph),
3483      State#state{callgraph = NewCallgraph}
3484  end.
3485
3486renew_race_public_tables([Var], #state{races = Races, callgraph = Callgraph,
3487				      warning_mode = WarningMode} = State) ->
3488  case WarningMode of
3489    true -> State;
3490    false ->
3491      Table = dialyzer_races:get_new_table(Races),
3492      case Table of
3493	no_t -> State;
3494	_Other ->
3495	  VarLabel = get_label(Var),
3496	  NewCallgraph =
3497	    dialyzer_callgraph:renew_race_public_tables(VarLabel, Callgraph),
3498	  State#state{callgraph = NewCallgraph}
3499      end
3500  end.
3501
3502%%% ===========================================================================
3503%%%
3504%%%  Worklist
3505%%%
3506%%% ===========================================================================
3507
3508init_work(List) ->
3509  {List, [], sets:from_list(List)}.
3510
3511get_work({[], [], _Set}) ->
3512  none;
3513get_work({[H|T], Rev, Set}) ->
3514  {H, {T, Rev, sets:del_element(H, Set)}};
3515get_work({[], Rev, Set}) ->
3516  get_work({lists:reverse(Rev), [], Set}).
3517
3518add_work(New, {List, Rev, Set} = Work) ->
3519  case sets:is_element(New, Set) of
3520    true -> Work;
3521    false -> {List, [New|Rev], sets:add_element(New, Set)}
3522  end.
3523
3524%%% ===========================================================================
3525%%%
3526%%%  Utilities.
3527%%%
3528%%% ===========================================================================
3529
3530get_line([Line|_]) when is_integer(Line) -> Line;
3531get_line([_|Tail]) -> get_line(Tail);
3532get_line([]) -> -1.
3533
3534get_file([]) -> [];
3535get_file([{file, File}|_]) -> File;
3536get_file([_|Tail]) -> get_file(Tail).
3537
3538is_compiler_generated(Ann) ->
3539  lists:member(compiler_generated, Ann) orelse (get_line(Ann) < 1).
3540
3541is_literal_record(Tree) ->
3542  Ann = cerl:get_ann(Tree),
3543  lists:member(record, Ann).
3544
3545-spec format_args([cerl:cerl()], [type()], state()) ->
3546  nonempty_string().
3547
3548format_args([], [], _State) ->
3549  "()";
3550format_args(ArgList0, TypeList, State) ->
3551  ArgList = fold_literals(ArgList0),
3552  "(" ++ format_args_1(ArgList, TypeList, State) ++ ")".
3553
3554format_args_1([Arg], [Type], State) ->
3555  format_arg(Arg) ++ format_type(Type, State);
3556format_args_1([Arg|Args], [Type|Types], State) ->
3557  String =
3558    case cerl:is_literal(Arg) of
3559      true -> format_cerl(Arg);
3560      false -> format_arg(Arg) ++ format_type(Type, State)
3561    end,
3562  String ++ "," ++ format_args_1(Args, Types, State).
3563
3564format_arg(Arg) ->
3565  Default = "",
3566  case cerl:is_c_var(Arg) of
3567    true ->
3568      case cerl:var_name(Arg) of
3569	Atom when is_atom(Atom) ->
3570	  case atom_to_list(Atom) of
3571	    "cor"++_ -> Default;
3572	    "rec"++_ -> Default;
3573	    Name -> Name ++ "::"
3574	  end;
3575	_What -> Default
3576      end;
3577    false ->
3578      Default
3579  end.
3580
3581-spec format_type(type(), state()) -> string().
3582
3583format_type(Type, #state{records = R}) ->
3584  t_to_string(Type, R).
3585
3586-spec format_field_diffs(type(), state()) -> string().
3587
3588format_field_diffs(RecConstruction, #state{records = R}) ->
3589  erl_types:record_field_diffs_to_string(RecConstruction, R).
3590
3591-spec format_sig_args(type(), state()) -> string().
3592
3593format_sig_args(Type, #state{opaques = Opaques} = State) ->
3594  SigArgs = t_fun_args(Type, Opaques),
3595  case SigArgs of
3596    [] -> "()";
3597    [SArg|SArgs] ->
3598      lists:flatten("(" ++ format_type(SArg, State)
3599		        ++ ["," ++ format_type(T, State) || T <- SArgs] ++ ")")
3600    end.
3601
3602format_cerl(Tree) ->
3603  cerl_prettypr:format(cerl:set_ann(Tree, []),
3604		       [{hook, dialyzer_utils:pp_hook()},
3605			{noann, true},
3606			{paper, 100000}, %% These guys strip
3607			{ribbon, 100000} %% newlines.
3608		       ]).
3609
3610format_patterns(Pats0) ->
3611  Pats = fold_literals(Pats0),
3612  NewPats = map_pats(cerl:c_values(Pats)),
3613  String = format_cerl(NewPats),
3614  case Pats of
3615    [PosVar] ->
3616      case cerl:is_c_var(PosVar) andalso (cerl:var_name(PosVar) =/= '') of
3617	true -> "variable "++String;
3618	false -> "pattern "++String
3619      end;
3620    _ ->
3621      "pattern "++String
3622  end.
3623
3624map_pats(Pats) ->
3625  Fun = fun(Tree) ->
3626	    case cerl:is_c_var(Tree) of
3627	      true ->
3628		case cerl:var_name(Tree) of
3629		  Atom when is_atom(Atom) ->
3630		    case atom_to_list(Atom) of
3631		      "cor"++_ -> cerl:c_var('');
3632		      "rec"++_ -> cerl:c_var('');
3633		      _ -> cerl:set_ann(Tree, [])
3634		    end;
3635		  _What -> cerl:c_var('')
3636		end;
3637	      false ->
3638		cerl:set_ann(Tree, [])
3639	    end
3640	end,
3641  cerl_trees:map(Fun, Pats).
3642
3643fold_literals(TreeList) ->
3644  [cerl:fold_literal(Tree) || Tree <- TreeList].
3645
3646type(Tree) ->
3647  Folded = cerl:fold_literal(Tree),
3648  case cerl:type(Folded) of
3649    literal -> {literal, Folded};
3650    Type -> Type
3651  end.
3652
3653is_literal(Tree) ->
3654  Folded = cerl:fold_literal(Tree),
3655  case cerl:is_literal(Folded) of
3656    true -> {yes, Folded};
3657    false -> no
3658  end.
3659
3660parent_allows_this(FunLbl, #state{callgraph = Callgraph, plt = Plt} =State) ->
3661  case state__is_escaping(FunLbl, State) of
3662    false -> false; % if it isn't escaping it can't be a return value
3663    true ->
3664      case state__lookup_name(FunLbl, State) of
3665	{_M, _F, _A} -> false; % if it has a name it is not a fun
3666	_ ->
3667	  case dialyzer_callgraph:in_neighbours(FunLbl, Callgraph) of
3668	    [Parent] ->
3669	      case state__lookup_name(Parent, State) of
3670		{_M, _F, _A} = PMFA ->
3671		  case dialyzer_plt:lookup_contract(Plt, PMFA) of
3672		    none -> false;
3673		    {value, C} ->
3674		      GenRet = dialyzer_contracts:get_contract_return(C),
3675		      case erl_types:t_is_fun(GenRet) of
3676			false -> false; % element of structure? far-fetched...
3677			true -> t_is_unit(t_fun_range(GenRet))
3678		      end
3679		  end;
3680		_ -> false % parent should have a name to have a contract
3681	      end;
3682	    _ -> false % called in other funs? far-fetched...
3683	  end
3684      end
3685  end.
3686
3687find_function({_, _, _} = MFA, _State) ->
3688  MFA;
3689find_function(top, _State) ->
3690  top;
3691find_function(FunLbl, #state{fun_homes = Homes}) ->
3692  dict:fetch(FunLbl, Homes).
3693
3694classify_returns(Tree) ->
3695  case find_terminals(cerl:fun_body(Tree)) of
3696    {false, false} -> no_match;
3697    {true, false} -> only_explicit;
3698    {false, true} -> only_normal;
3699    {true, true} -> both
3700  end.
3701
3702find_terminals(Tree) ->
3703  case cerl:type(Tree) of
3704    apply -> {false, true};
3705    binary -> {false, true};
3706    bitstr -> {false, true};
3707    call ->
3708      M0 = cerl:call_module(Tree),
3709      F0 = cerl:call_name(Tree),
3710      A = length(cerl:call_args(Tree)),
3711      case {is_literal(M0), is_literal(F0)} of
3712        {{yes, LitM}, {yes, LitF}} ->
3713	  M = cerl:concrete(LitM),
3714	  F = cerl:concrete(LitF),
3715	  case (erl_bif_types:is_known(M, F, A)
3716		andalso t_is_none(erl_bif_types:type(M, F, A))) of
3717	    true -> {true, false};
3718	    false -> {false, true}
3719	  end;
3720        _ ->
3721	  %% We cannot make assumptions. Say that both are true.
3722	  {true, true}
3723      end;
3724    'case' -> find_terminals_list(cerl:case_clauses(Tree));
3725    'catch' -> find_terminals(cerl:catch_body(Tree));
3726    clause -> find_terminals(cerl:clause_body(Tree));
3727    cons -> {false, true};
3728    'fun' -> {false, true};
3729    'let' -> find_terminals(cerl:let_body(Tree));
3730    letrec -> find_terminals(cerl:letrec_body(Tree));
3731    literal -> {false, true};
3732    map -> {false, true};
3733    primop -> {false, false}; %% match_fail, etc. are not explicit exits.
3734    'receive' ->
3735      Timeout = cerl:receive_timeout(Tree),
3736      Clauses = cerl:receive_clauses(Tree),
3737      case (cerl:is_literal(Timeout) andalso
3738	    (cerl:concrete(Timeout) =:= infinity)) of
3739	true ->
3740	  if Clauses =:= [] -> {false, true}; %% A never ending receive.
3741	     true -> find_terminals_list(Clauses)
3742	  end;
3743	false -> find_terminals_list([cerl:receive_action(Tree)|Clauses])
3744      end;
3745    seq -> find_terminals(cerl:seq_body(Tree));
3746    'try' ->
3747      find_terminals_list([cerl:try_handler(Tree), cerl:try_body(Tree)]);
3748    tuple -> {false, true};
3749    values -> {false, true};
3750    var -> {false, true}
3751  end.
3752
3753find_terminals_list(List) ->
3754  find_terminals_list(List, false, false).
3755
3756find_terminals_list([Tree|Left], Explicit1, Normal1) ->
3757  {Explicit2, Normal2} = find_terminals(Tree),
3758  case {Explicit1 or Explicit2, Normal1 or Normal2} of
3759    {true, true} = Ans -> Ans;
3760    {NewExplicit, NewNormal} ->
3761      find_terminals_list(Left, NewExplicit, NewNormal)
3762  end;
3763find_terminals_list([], Explicit, Normal) ->
3764  {Explicit, Normal}.
3765
3766%%----------------------------------------------------------------------------
3767
3768-ifdef(DEBUG_PP).
3769debug_pp(Tree, true) ->
3770  io:put_chars(cerl_prettypr:format(Tree, [{hook, cerl_typean:pp_hook()}])),
3771  io:nl(),
3772  ok;
3773debug_pp(Tree, false) ->
3774  io:put_chars(cerl_prettypr:format(strip_annotations(Tree))),
3775  io:nl(),
3776  ok.
3777
3778strip_annotations(Tree) ->
3779  Fun = fun(T) ->
3780	    case cerl:type(T) of
3781	      var ->
3782		cerl:set_ann(T, [{label, cerl_trees:get_label(T)}]);
3783	      'fun' ->
3784		cerl:set_ann(T, [{label, cerl_trees:get_label(T)}]);
3785	      _ ->
3786		cerl:set_ann(T, [])
3787	    end
3788	end,
3789  cerl_trees:map(Fun, Tree).
3790
3791-else.
3792
3793debug_pp(_Tree, _UseHook) ->
3794  ok.
3795-endif.
3796