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