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