The R13B03 release.OTP_R13B03

1 files changed, 1003 insertions, 0 deletions

diff --git a/lib/hipe/cerl/cerl_typean.erl b/lib/hipe/cerl/cerl_typean.erl
new file mode 100644
index 0000000000..ccd8903658
--- /dev/null
+++ b/lib/hipe/cerl/cerl_typean.erl
@@ -0,0 +1,1003 @@
+%% -*- erlang-indent-level: 4 -*-
+%%
+%% %CopyrightBegin%
+%% 
+%% Copyright Ericsson AB 2003-2009. All Rights Reserved.
+%% 
+%% The contents of this file are subject to the Erlang Public License,
+%% Version 1.1, (the "License"); you may not use this file except in
+%% compliance with the License. You should have received a copy of the
+%% Erlang Public License along with this software. If not, it can be
+%% retrieved online at http://www.erlang.org/.
+%% 
+%% Software distributed under the License is distributed on an "AS IS"
+%% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
+%% the License for the specific language governing rights and limitations
+%% under the License.
+%% 
+%% %CopyrightEnd%
+%%
+%% Type analysis of Core Erlang programs.
+%%
+%% Copyright (C) 2001-2002 Richard Carlsson
+%%
+%% Author contact: [email protected]
+%%
+%% @doc Type analysis of Core Erlang programs.
+
+%% TODO: filters must handle conjunctions for better precision!
+%% TODO: should get filters from patterns as well as guards.
+%% TODO: unused functions are being included in the analysis.
+
+-module(cerl_typean).
+
+-export([core_transform/2, analyze/1, pp_hook/0]).
+%%-export([analyze/2, analyze/5, annotate/1, annotate/2, annotate/5]).
+
+-import(erl_types, [t_any/0, t_atom/0, t_atom_vals/1, t_binary/0,
+		    t_cons/2, t_cons_hd/1, t_cons_tl/1, t_float/0,
+		    t_fun/0, t_fun/2, t_from_range/2, t_from_term/1,
+		    t_inf/2, t_integer/0,
+		    t_is_any/1, t_is_atom/1, t_is_cons/1, t_is_list/1,
+		    t_is_maybe_improper_list/1, t_is_none/1, t_is_tuple/1,
+		    t_limit/2, t_list_elements/1, t_maybe_improper_list/0,
+		    t_none/0, t_number/0, t_pid/0, t_port/0, t_product/1,
+		    t_reference/0, t_sup/2, t_to_tlist/1, t_tuple/0, t_tuple/1,
+		    t_tuple_args/1, t_tuple_size/1, t_tuple_subtypes/1]).
+
+-import(cerl, [ann_c_fun/3, ann_c_var/2, alias_pat/1, alias_var/1,
+	       apply_args/1, apply_op/1, atom_val/1, bitstr_size/1,
+	       bitstr_val/1, bitstr_type/1, bitstr_flags/1, binary_segments/1, 
+	       c_letrec/2, c_nil/0,
+	       c_values/1, call_args/1, call_module/1, call_name/1,
+	       case_arg/1, case_clauses/1, catch_body/1, clause_body/1,
+	       clause_guard/1, clause_pats/1, concrete/1, cons_hd/1,
+	       cons_tl/1, fun_body/1, fun_vars/1, get_ann/1, int_val/1,
+	       is_c_atom/1, is_c_int/1, let_arg/1, let_body/1, let_vars/1,
+	       letrec_body/1, letrec_defs/1, module_defs/1,
+	       module_defs/1, module_exports/1, pat_vars/1,
+	       primop_args/1, primop_name/1, receive_action/1,
+	       receive_clauses/1, receive_timeout/1, seq_arg/1,
+	       seq_body/1, set_ann/2, try_arg/1, try_body/1,
+	       try_evars/1, try_handler/1, try_vars/1, tuple_arity/1,
+	       tuple_es/1, type/1, values_es/1, var_name/1]).
+
+-import(cerl_trees, [get_label/1]).
+
+-ifdef(DEBUG).
+-define(ANNOTATE(X), case erl_types:t_to_string(X) of Q when length(Q) < 255 -> list_to_atom(Q); Q -> Q end).
+-else.
+-define(ANNOTATE(X), X).
+-endif.
+
+%% Limit for type representation depth.
+-define(DEF_LIMIT, 3).
+
+
+%% @spec core_transform(Module::cerl_records(), Options::[term()]) ->
+%%           cerl_records()
+%%
+%% @doc Annotates a module represented by records with type
+%% information. See <code>annotate/1</code> for details.
+%%
+%% <p>Use the compiler option <code>{core_transform, cerl_typean}</code>
+%% to insert this function as a compilation pass.</p>
+%%
+%% @see module/2
+
+-spec core_transform(cerl:cerl(), [term()]) -> cerl:cerl().
+
+core_transform(Code, _Opts) ->
+    {Code1, _} = cerl_trees:label(cerl:from_records(Code)),
+    %% io:fwrite("Running type analysis..."),
+    %% {T1,_} = statistics(runtime),
+    {Code2, _, _} = annotate(Code1),
+    %% {T2,_} = statistics(runtime),
+    %% io:fwrite("(~w ms).\n", [T2 - T1]),
+    cerl:to_records(Code2).
+
+
+%% =====================================================================
+%% annotate(Tree) -> {Tree1, Type, Vars}
+%%
+%%	    Tree = cerl:cerl()
+%%
+%%	Analyzes `Tree' (see `analyze') and appends terms `{type, Type}'
+%%	to the annotation list of each fun-expression node and
+%%	apply-expression node of `Tree', respectively, where `Labels' is
+%%	an ordered-set list of labels of fun-expressions in `Tree',
+%%	possibly also containing the atom `external', corresponding to
+%%	the dependency information derived by the analysis. Any previous
+%%	such annotations are removed from `Tree'. `Tree1' is the
+%%	modified tree; for details on `OutList', `Outputs' ,
+%%	`Dependencies' and `Escapes', see `analyze'.
+%%
+%%	Note: `Tree' must be annotated with labels in order to use this
+%%	function; see `analyze' for details.
+
+annotate(Tree) ->
+    annotate(Tree, ?DEF_LIMIT).
+
+annotate(Tree, Limit) ->
+    {_, _, Esc, Dep, Par} = cerl_closurean:analyze(Tree),
+    annotate(Tree, Limit, Esc, Dep, Par).
+
+annotate(Tree, Limit, Esc, Dep, Par) ->
+    {Type, Out, Vars} = analyze(Tree, Limit, Esc, Dep, Par),
+    DelAnn = fun (T) -> set_ann(T, delete_ann(type, get_ann(T))) end,
+    SetType = fun (T, Dict) ->
+		      case dict:find(get_label(T), Dict) of
+			  {ok, X} ->
+			      case t_is_any(X) of
+				  true ->
+				      DelAnn(T);
+				  false ->
+				      set_ann(T, append_ann(type,
+							    ?ANNOTATE(X),
+							    get_ann(T)))
+			      end;
+			  error ->
+			      DelAnn(T)
+		      end
+	      end,
+    F = fun (T) ->
+		case type(T) of
+		    var ->
+			SetType(T, Vars);
+		    apply ->
+			SetType(T, Out);
+		    call ->
+			SetType(T, Out);
+		    primop ->
+			SetType(T, Out);
+		    'fun' ->
+			SetType(T, Out);
+		    _ ->
+			DelAnn(T)
+		end
+	end,
+    {cerl_trees:map(F, Tree), Type, Vars}.
+
+append_ann(Tag, Val, [X | Xs]) ->
+    if tuple_size(X) >= 1, element(1, X) =:= Tag -> 
+	    append_ann(Tag, Val, Xs);
+       true ->
+	    [X | append_ann(Tag, Val, Xs)]
+    end;
+append_ann(Tag, Val, []) ->
+    [{Tag, Val}].
+
+delete_ann(Tag, [X | Xs]) ->
+    if tuple_size(X) >= 1, element(1, X) =:= Tag -> 
+	    delete_ann(Tag, Xs);
+       true ->
+	    [X | delete_ann(Tag, Xs)]
+    end;
+delete_ann(_, []) ->
+    [].
+
+
+%% =====================================================================
+%% analyze(Tree) -> {OutList, Outputs, Dependencies}
+%%
+%%	    Tree = cerl:cerl()
+%%	    OutList = [LabelSet] | none
+%%	    Outputs = dict(integer(), OutList)
+%%	    Dependencies = dict(integer(), LabelSet)
+%%	    LabelSet = ordset(Label)
+%%	    Label = integer() | external
+%%
+%%	Analyzes a module or an expression represented by `Tree'.
+%%
+%%	The returned `OutList' is a list of sets of labels of
+%%	fun-expressions which correspond to the possible closures in the
+%%	value list produced by `Tree' (viewed as an expression; the
+%%	"value" of a module contains its exported functions). The atom
+%%	`none' denotes missing or conflicting information.
+%%
+%%	The atom `external' in any label set denotes any possible
+%%	function outside `Tree', including those in `Escapes'.
+%%
+%%	`Outputs' is a mapping from the labels of fun-expressions in
+%%	`Tree' to corresponding lists of sets of labels of
+%%	fun-expressions (or the atom `none'), representing the possible
+%%	closures in the value lists returned by the respective
+%%	functions.
+%%
+%%	`Dependencies' is a similar mapping from the labels of
+%%	fun-expressions and apply-expressions in `Tree' to sets of
+%%	labels of corresponding fun-expressions which may contain call
+%%	sites of the functions or be called from the call sites,
+%%	respectively. Any such label not defined in `Dependencies'
+%%	represents an unreachable function or a dead or faulty
+%%	application.
+%%
+%%	`Escapes' is the set of labels of fun-expressions in `Tree' such
+%%	that corresponding closures may be accessed from outside `Tree'.
+%%
+%%	Note: `Tree' must be annotated with labels (as done by the
+%%	function `cerl_trees:label/1') in order to use this function.
+%%	The label annotation `{label, L}' (where L should be an integer)
+%%	must be the first element of the annotation list of each node in
+%%	the tree. Instances of variables bound in `Tree' which denote
+%%	the same variable must have the same label; apart from this,
+%%	labels should be unique. Constant literals do not need to be
+%%	labeled.
+
+-record(state, {k, vars, out, dep, work, funs, envs}).
+
+%% Note: In order to keep our domain simple, we assume that all remote
+%% calls and primops return a single value, if any.
+
+%% We wrap the given syntax tree T in a fun-expression labeled `top',
+%% which is initially in the set of escaped labels. `top' will be
+%% visited at least once.
+%%
+%% We create a separate function labeled `external', defined as:
+%% "External = fun () -> Any", which will represent any and all
+%% functions outside T, and whose return value has unknown type.
+
+-type label()    :: integer() | 'external' | 'top'.
+-type ordset(X)  :: [X].  % XXX: TAKE ME OUT
+-type labelset() :: ordset(label()).
+-type outlist()  :: [labelset()] | 'none'.
+
+-spec analyze(cerl:cerl()) -> {outlist(), dict(), dict()}.
+
+analyze(Tree) ->
+    analyze(Tree, ?DEF_LIMIT).
+
+analyze(Tree, Limit) ->
+    {_, _, Esc, Dep, Par} = cerl_closurean:analyze(Tree),
+    analyze(Tree, Limit, Esc, Dep, Par).
+
+analyze(Tree, Limit, Esc0, Dep0, Par) ->
+    %% Note that we use different name spaces for variable labels and
+    %% function/call site labels. We assume that the labeling of Tree
+    %% only uses integers, not atoms.
+    LabelExtL = [{label, external}],
+    External = ann_c_var(LabelExtL, {external, 1}),
+    ExtFun = ann_c_fun(LabelExtL, [], ann_c_var([{label, any}], 'Any')),
+%%%     io:fwrite("external fun:\n~s.\n",
+%%% 	      [cerl_prettypr:format(ExtFun, [noann, {paper, 80}])]),
+    LabelTopL = [{label, top}],
+    Top = ann_c_var(LabelTopL, {top, 0}),
+    TopFun = ann_c_fun(LabelTopL, [], Tree),
+
+    %% The "start fun" just makes the initialisation easier. It is not
+    %% itself in the call graph.
+    StartFun =  ann_c_fun([{label, start}], [],
+			  c_letrec([{External, ExtFun}, {Top, TopFun}],
+				   c_nil())),
+%%%     io:fwrite("start fun:\n~s.\n",
+%%% 	      [cerl_prettypr:format(StartFun, [{paper, 80}])]),
+
+    %% Gather a database of all fun-expressions in Tree and initialise
+    %% their outputs and parameter variables. All escaping functions can
+    %% receive any values as inputs. Also add an extra dependency edge
+    %% from each fun-expression label to its parent fun-expression.
+%%%     io:fwrite("Escape: ~p.\n",[Esc0]),
+    Esc = sets:from_list(Esc0),
+    Any = t_any(),
+    None = t_none(),
+    Funs0 = dict:new(),
+    Vars0 = dict:store(any, Any, dict:new()),
+    Out0 = dict:store(top, None,
+		      dict:store(external, None, dict:new())),
+    Envs0 = dict:store(top, dict:new(),
+		       dict:store(external, dict:new(), dict:new())),
+    F = fun (T, S = {Fs, Vs, Os, Es}) ->
+		case type(T) of
+		    'fun' ->
+			L = get_label(T),
+			As = fun_vars(T),
+			X = case sets:is_element(L, Esc) of
+				true -> Any;
+				false -> None
+			    end,
+			{dict:store(L, T, Fs),
+			 bind_vars_single(As, X, Vs),
+			 dict:store(L, None, Os),
+			 dict:store(L, dict:new(), Es)};
+		    _ ->
+			S
+		end
+	end,
+    {Funs, Vars, Out, Envs} = cerl_trees:fold(F, {Funs0, Vars0, Out0,
+						  Envs0}, StartFun),
+
+    %% Add dependencies from funs to their parent funs.
+    Dep = lists:foldl(fun ({L, L1}, D) -> add_dep(L, L1, D) end,
+		      Dep0, dict:to_list(Par)),
+
+    %% Enter the fixpoint iteration at the StartFun.
+    St = loop(TopFun, top, #state{vars = Vars,
+				  out = Out,
+				  dep = Dep,
+				  work = init_work(),
+				  funs = Funs,
+				  envs = Envs,
+				  k = Limit}),
+    {dict:fetch(top, St#state.out),
+     tidy_dict([top, external], St#state.out),
+     tidy_dict([any], St#state.vars)}.
+
+tidy_dict([X | Xs], D) ->
+    tidy_dict(Xs, dict:erase(X, D));
+tidy_dict([], D) ->
+    D.
+
+loop(T, L, St0) ->
+%%%     io:fwrite("analyzing: ~w.\n",[L]),
+%%%     io:fwrite("work: ~w.\n", [Queue0]),
+    Env = dict:fetch(L, St0#state.envs),
+    X0 = dict:fetch(L, St0#state.out),
+    {X1, St1} = visit(fun_body(T), Env, St0),
+    X = limit(X1, St1#state.k),
+    {W, M} = case equal(X0, X) of
+		 true ->
+		     {St1#state.work, St1#state.out};
+		 false ->
+%%%        		     io:fwrite("out (~w) changed: ~s <- ~s.\n",
+%%%        			       [L, erl_types:t_to_string(X),
+%%%    				erl_types:t_to_string(X0)]),
+		     M1 = dict:store(L, X, St1#state.out),
+		     case dict:find(L, St1#state.dep) of
+			 {ok, S} ->
+%%% 			     io:fwrite("adding work: ~w.\n", [S]),
+			     {add_work(S, St1#state.work), M1};
+			 error ->
+			     {St1#state.work, M1}
+		     end
+	     end,
+    St2 = St1#state{out = M},
+    case take_work(W) of
+	{ok, L1, W1} ->
+ 	    T1 = dict:fetch(L1, St2#state.funs),
+ 	    loop(T1, L1, St2#state{work = W1});
+	none ->
+	    St2
+    end.
+
+visit(T, Env, St) ->
+    case type(T) of
+	literal ->
+	    {t_from_term(concrete(T)), St};
+	var ->
+	    %% If a variable is not already in the store at this point,
+	    %% we initialize it to 'none()'.
+	    L = get_label(T),
+	    Vars = St#state.vars,
+	    case dict:find(L, Vars) of
+		{ok, X} ->
+		    case dict:find(var_name(T), Env) of
+			{ok, X1} ->
+%%%   			    io:fwrite("filtered variable reference: ~w:~s.\n",
+%%%   				      [var_name(T), erl_types:t_to_string(X1)]),
+			    {meet(X, X1), St};
+			error ->
+			    {X, St}
+		    end;
+		error ->
+		    X = t_none(),
+		    Vars1 = dict:store(L, X, Vars),
+		    St1 = St#state{vars = Vars1},
+		    {X, St1}
+	    end;
+	'fun' ->
+	    %% Must revisit the fun also, because its environment might
+	    %% have changed. (We don't keep track of such dependencies.)
+	    L = get_label(T),
+	    Xs = [dict:fetch(get_label(V), St#state.vars)
+		  || V <- fun_vars(T)],
+	    X = dict:fetch(L, St#state.out),
+	    St1 = St#state{work = add_work([L], St#state.work),
+			   envs = dict:store(L, Env, St#state.envs)},
+	    {t_fun(Xs, X), St1};
+	values ->
+	    {Xs, St1} = visit_list(values_es(T), Env, St),
+	    {t_product(Xs), St1};
+	cons ->
+	    {[X1, X2], St1} = visit_list([cons_hd(T), cons_tl(T)], Env, St),
+	    {t_cons(X1, X2), St1};
+	tuple ->
+	    {Xs, St1} = visit_list(tuple_es(T), Env, St),
+	    {t_tuple(Xs), St1};
+	'let' ->
+	    {X, St1} = visit(let_arg(T), Env, St),
+	    LetVars = let_vars(T),
+	    St1Vars = St1#state.vars,
+	    Vars = case t_is_any(X) orelse t_is_none(X) of
+		       true ->
+			   bind_vars_single(LetVars, X, St1Vars);
+		       false ->
+			   bind_vars(LetVars, t_to_tlist(X), St1Vars)
+		   end,
+	    visit(let_body(T), Env, St1#state{vars = Vars});
+	seq ->
+	    {_, St1} = visit(seq_arg(T), Env, St),
+	    visit(seq_body(T), Env, St1);
+	apply ->
+	    {_F, St1} = visit(apply_op(T), Env, St),
+	    {As, St2} = visit_list(apply_args(T), Env, St1),
+	    L = get_label(T),
+	    Ls = get_deps(L, St#state.dep),
+	    Out = St2#state.out,
+	    X = join_list([dict:fetch(L1, Out) || L1 <- Ls]),
+	    Out1 = dict:store(L, X, Out),
+	    {X, call_site(Ls, As, St2#state{out = Out1})};
+	call ->
+	    M = call_module(T),
+	    F = call_name(T),
+	    As = call_args(T),
+	    {[X1, X2], St1} = visit_list([M, F], Env, St),
+	    {Xs, St2} = visit_list(As, Env, St1),
+%%% 	    io:fwrite("call: ~w:~w(~w).\n",[X1,X2,Xs]),
+	    X = case {t_atom_vals(X1), t_atom_vals(X2)} of
+		    {[M1], [F1]} ->
+			A = length(As),
+%%% 			io:fwrite("known call: ~w:~w/~w.\n",
+%%% 				  [M1, F1, A]),
+			call_type(M1, F1, A, Xs);
+		    _ ->
+			t_any()
+		end,
+	    L = get_label(T),
+	    {X, St2#state{out = dict:store(L, X, St2#state.out)}};
+	primop ->
+	    As = primop_args(T),
+	    {Xs, St1} = visit_list(As, Env, St),
+	    F = atom_val(primop_name(T)),
+	    A = length(As),
+	    L = get_label(T),
+	    X = primop_type(F, A, Xs),
+	    {X, St1#state{out = dict:store(L, X, St1#state.out)}};
+	'case' ->
+	    {X, St1} = visit(case_arg(T), Env, St),
+	    Xs = case t_is_any(X) orelse t_is_none(X) of
+		     true ->
+			 [X || _ <- cerl:case_clauses(T)];
+		     false ->
+			 t_to_tlist(X)
+		 end,
+	    join_visit_clauses(Xs, case_clauses(T), Env, St1);
+	'receive' ->
+	    Any = t_any(),
+	    {X1, St1} = join_visit_clauses([Any], receive_clauses(T),
+					   Env, St),
+	    {X2, St2} = visit(receive_timeout(T), Env, St1),
+	    case t_is_atom(X2) andalso (t_atom_vals(X2) =:= [infinity]) of
+		true ->
+		    {X1, St2};
+		false ->
+		    {X3, St3} = visit(receive_action(T), Env, St2),
+		    {join(X1, X3), St3}
+	    end;
+	'try' ->
+	    {X, St1} = visit(try_arg(T), Env, St),
+	    Any = t_any(),
+	    Atom = t_atom(),
+	    TryVars = try_vars(T),
+	    St1Vars = St1#state.vars,
+	    Vars = case t_is_any(X) orelse t_is_none(X) of
+		       true ->
+			   bind_vars_single(TryVars, X, St1Vars);
+		       false ->
+			   bind_vars(TryVars, t_to_tlist(X), St1Vars)
+		   end,
+	    {X1, St2} = visit(try_body(T), Env, St1#state{vars = Vars}),
+	    EVars = bind_vars(try_evars(T), [Atom, Any, Any], St2#state.vars),
+	    {X2, St3} = visit(try_handler(T), Env, St2#state{vars = EVars}),
+	    {join(X1, X2), St3};
+	'catch' ->
+	    {_, St1} = visit(catch_body(T), Env, St),
+	    {t_any(), St1};
+	binary ->
+	    {_, St1} = visit_list(binary_segments(T), Env, St),
+	    {t_binary(), St1};
+	bitstr ->
+	    %% The other fields are constant literals.
+	    {_, St1} = visit(bitstr_val(T), Env, St),
+	    {_, St2} = visit(bitstr_size(T), Env, St1),
+	    {t_none(), St2};
+	letrec ->
+	    %% All the bound funs should be revisited, because the
+	    %% environment might have changed.
+	    Vars = bind_defs(letrec_defs(T), St#state.vars,
+			     St#state.out),
+	    Ls = [get_label(F) || {_, F} <- letrec_defs(T)],
+	    St1 = St#state{work = add_work(Ls, St#state.work),
+			   vars = Vars},
+	    visit(letrec_body(T), Env, St1);
+	module ->
+	    %% We handle a module as a sequence of function variables in
+	    %% the body of a `letrec'.
+	    {_, St1} = visit(c_letrec(module_defs(T),
+				      c_values(module_exports(T))),
+			     Env, St),
+	    {t_none(), St1}
+    end.
+
+visit_clause(T, Xs, Env, St) ->
+    Env1 = Env,
+    Vars = bind_pats(clause_pats(T), Xs, St#state.vars),
+    G = clause_guard(T),
+    {_, St1} = visit(G, Env1, St#state{vars = Vars}),
+    Env2 = guard_filters(G, Env1),
+    visit(clause_body(T), Env2, St1).
+
+%% We assume correct value-list typing.
+
+visit_list([T | Ts], Env, St) ->
+    {X, St1} = visit(T, Env, St),
+    {Xs, St2} = visit_list(Ts, Env, St1),
+    {[X | Xs], St2};
+visit_list([], _Env, St) ->
+    {[], St}.
+
+join_visit_clauses(Xs, [T | Ts], Env, St) ->
+    {X1, St1} = visit_clause(T, Xs, Env, St),
+    {X2, St2} = join_visit_clauses(Xs, Ts, Env, St1),
+    {join(X1, X2), St2};
+join_visit_clauses(_, [], _Env, St) ->
+    {t_none(), St}.
+
+bind_defs([{V, F} | Ds], Vars, Out) ->
+    Xs = [dict:fetch(get_label(V1), Vars) || V1 <- fun_vars(F)],
+    X = dict:fetch(get_label(F), Out),
+    bind_defs(Ds, dict:store(get_label(V), t_fun(Xs, X), Vars), Out);
+bind_defs([], Vars, _Out) ->
+    Vars.
+
+bind_pats(Ps, Xs, Vars) ->
+    if length(Xs) =:= length(Ps) ->
+	    bind_pats_list(Ps, Xs, Vars);
+       true ->
+	    bind_pats_single(Ps, t_none(), Vars)
+    end.
+
+bind_pats_list([P | Ps], [X | Xs], Vars) ->
+    Vars1 = bind_pat_vars(P, X, Vars),
+    bind_pats_list(Ps, Xs, Vars1);
+bind_pats_list([], [], Vars) ->
+    Vars.
+
+bind_pats_single([P | Ps], X, Vars) ->
+    bind_pats_single(Ps, X, bind_pat_vars(P, X, Vars));
+bind_pats_single([], _X, Vars) ->
+    Vars.
+
+bind_pat_vars(P, X, Vars) ->
+    case type(P) of
+	var ->
+	    dict:store(get_label(P), X, Vars);
+	literal ->
+	    Vars;
+	cons ->
+	    case t_is_cons(X) of
+		true ->
+		    %% If X is "nonempty proper list of X1", then the
+		    %% head has type X1 and the tail has type "proper
+		    %% list of X1". (If X is just "cons cell of X1",
+		    %% then both head and tail have type X1.)
+		    Vars1 = bind_pat_vars(cons_hd(P), t_cons_hd(X),
+					  Vars),
+		    bind_pat_vars(cons_tl(P), t_cons_tl(X), Vars1);
+		false ->
+		    case t_is_list(X) of
+			true ->
+			    %% If X is "proper list of X1", then the
+			    %% head has type X1 and the tail has type
+			    %% "proper list of X1", i.e., type X.
+			    Vars1 = bind_pat_vars(cons_hd(P),
+						  t_list_elements(X),
+						  Vars),
+			    bind_pat_vars(cons_tl(P), X, Vars1);
+			false ->
+			    case t_is_maybe_improper_list(X) of
+				true ->
+				    %% If X is "cons cell of X1", both
+				    %% the head and tail have type X1.
+				    X1 = t_list_elements(X),
+				    Vars1 = bind_pat_vars(cons_hd(P),
+							  X1, Vars),
+				    bind_pat_vars(cons_tl(P), X1,
+						  Vars1);
+				false ->
+				    bind_vars_single(pat_vars(P),
+						     top_or_bottom(X),
+						     Vars)
+			    end
+		    end
+	    end;
+	tuple ->
+	    case t_is_tuple(X) of
+		true ->
+		    case t_tuple_subtypes(X) of
+			unknown -> 
+			    bind_vars_single(pat_vars(P), top_or_bottom(X), 
+					     Vars);
+			[Tuple] ->
+			    case t_tuple_size(Tuple) =:= tuple_arity(P) of
+				true ->
+				    bind_pats_list(tuple_es(P), 
+						   t_tuple_args(Tuple), Vars);
+				
+				false ->
+				    bind_vars_single(pat_vars(P), 
+						     top_or_bottom(X), Vars)
+			    end;
+			List when is_list(List) ->
+			    bind_vars_single(pat_vars(P), top_or_bottom(X), 
+					     Vars)
+		    end;
+		false ->
+		    bind_vars_single(pat_vars(P), top_or_bottom(X), Vars)
+	    end;
+	binary ->
+	    bind_pats_single(binary_segments(P), t_none(), Vars);
+	bitstr ->
+	    %% Only the Value field is a new binding. Size is already
+	    %% bound, and the other fields are constant literals.
+	    %% We could create a filter for Size being an integer().
+	    Size = bitstr_size(P),
+	    ValType = 
+		case concrete(bitstr_type(P)) of
+		    float -> t_float();
+		    binary -> t_binary();
+		    integer ->
+			case is_c_int(Size) of
+			    false -> t_integer();
+			    true -> 
+				SizeVal = int_val(Size),
+				Flags = concrete(bitstr_flags(P)),
+				case lists:member(signed, Flags) of
+				    true -> 
+					t_from_range(-(1 bsl (SizeVal - 1)),
+						     1 bsl (SizeVal - 1) - 1);
+				    false -> 
+					t_from_range(0,1 bsl SizeVal - 1)
+				end
+			end
+		end,
+	    bind_pat_vars(bitstr_val(P), ValType, Vars);
+	alias ->
+	    P1 = alias_pat(P),
+	    Vars1 = bind_pat_vars(P1, X, Vars),
+	    dict:store(get_label(alias_var(P)), pat_type(P1, Vars1),
+		       Vars1)
+    end.
+
+pat_type(P, Vars) ->
+    case type(P) of
+	var ->
+	    dict:fetch(get_label(P), Vars);
+	literal ->
+	    t_from_term(concrete(P));
+	cons ->
+	    t_cons(pat_type(cons_hd(P), Vars), 
+		   pat_type(cons_tl(P), Vars));
+	tuple ->
+	    t_tuple([pat_type(E, Vars) || E <- tuple_es(P)]);
+	binary ->
+	    t_binary();
+	alias ->
+	    pat_type(alias_pat(P), Vars)
+    end.
+
+bind_vars(Vs, Xs, Vars) ->
+    if length(Vs) =:= length(Xs) ->
+	    bind_vars_list(Vs, Xs, Vars);
+       true ->
+	    bind_vars_single(Vs, t_none(), Vars)
+    end.
+
+bind_vars_list([V | Vs], [X | Xs], Vars) ->
+    bind_vars_list(Vs, Xs, dict:store(get_label(V), X, Vars));
+bind_vars_list([], [], Vars) ->
+    Vars.
+
+bind_vars_single([V | Vs], X, Vars) ->
+    bind_vars_single(Vs, X, dict:store(get_label(V), X, Vars));
+bind_vars_single([], _X, Vars) ->
+    Vars.
+
+add_dep(Source, Target, Deps) ->
+    case dict:find(Source, Deps) of
+	{ok, X} ->
+	    case set__is_member(Target, X) of
+		true ->
+		    Deps;
+		false ->
+%%%		    io:fwrite("new dep: ~w <- ~w.\n", [Target, Source]),
+		    dict:store(Source, set__add(Target, X), Deps)
+	    end;
+	error ->
+%%%	    io:fwrite("new dep: ~w <- ~w.\n", [Target, Source]),
+	    dict:store(Source, set__singleton(Target), Deps)
+    end.
+
+%% This handles a call site, updating parameter variables with respect
+%% to the actual parameters.
+
+call_site(Ls, Xs, St) ->
+%%     io:fwrite("call site: ~w ~s.\n",
+%% 	      [Ls, erl_types:t_to_string(erl_types:t_product(Xs))]),
+    {W, V} = call_site(Ls, Xs, St#state.work, St#state.vars,
+		       St#state.funs, St#state.k),
+    St#state{work = W, vars = V}.
+
+call_site([L | Ls], Xs, W, V, Fs, Limit) ->
+    Vs = fun_vars(dict:fetch(L, Fs)),
+    case bind_args(Vs, Xs, V, Limit) of
+	{V1, true} ->
+	    call_site(Ls, Xs, add_work([L], W), V1, Fs, Limit);
+	{V1, false} ->
+	    call_site(Ls, Xs, W, V1, Fs, Limit)
+    end;
+call_site([], _, W, V, _, _) ->
+    {W, V}.
+
+%% If the arity does not match the call, nothing is done here.
+
+bind_args(Vs, Xs, Vars, Limit) ->
+    if length(Vs) =:= length(Xs) ->
+	    bind_args(Vs, Xs, Vars, Limit, false);
+       true ->
+	    {Vars, false}
+    end.
+
+bind_args([V | Vs], [X | Xs], Vars, Limit, Ch) ->
+    L = get_label(V),
+    {Vars1, Ch1} = bind_arg(L, X, Vars, Limit, Ch),
+    bind_args(Vs, Xs, Vars1, Limit, Ch1);
+bind_args([], [], Vars, _Limit, Ch) ->
+    {Vars, Ch}.
+
+%% bind_arg(L, X, Vars, Limit) ->
+%%     bind_arg(L, X, Vars, Limit, false).
+
+bind_arg(L, X, Vars, Limit, Ch) ->
+    X0 = dict:fetch(L, Vars),
+    X1 = limit(join(X, X0), Limit),
+    case equal(X0, X1) of
+	true ->
+	    {Vars, Ch};
+	false ->
+%%%     	    io:fwrite("arg (~w) changed: ~s <- ~s + ~s.\n",
+%%%  		      [L, erl_types:t_to_string(X1),
+%%% 		       erl_types:t_to_string(X0),
+%%%  		       erl_types:t_to_string(X)]),
+	    {dict:store(L, X1, Vars), true}
+    end.
+
+%% Domain: type(), defined in module `erl_types'.
+
+meet(X, Y) -> t_inf(X, Y).
+
+join(X, Y) -> t_sup(X, Y).
+
+join_list([Xs | Xss]) ->
+    join(Xs, join_list(Xss));
+join_list([]) ->
+    t_none().
+
+equal(X, Y) -> X =:= Y.
+
+limit(X, K) -> t_limit(X, K).
+
+top_or_bottom(T) ->
+    case t_is_none(T) of
+	true ->
+	    T;
+	false ->
+	    t_any()
+    end.
+
+strict(Xs, T) ->
+    case erl_types:any_none(Xs) of
+	true ->
+	    t_none();
+	false ->
+	    T
+    end.
+
+%% Set abstraction for label sets.
+
+%% set__new() -> [].
+
+set__singleton(X) -> [X].
+
+%% set__to_list(S) -> S.
+
+%% set__from_list(S) -> ordsets:from_list(S).
+
+%% set__union(X, Y) -> ordsets:union(X, Y).
+
+set__add(X, S) -> ordsets:add_element(X, S).
+
+set__is_member(X, S) -> ordsets:is_element(X, S).    
+
+%% set__subtract(X, Y) -> ordsets:subtract(X, Y).
+
+%% set__equal(X, Y) -> X =:= Y.
+
+%% A simple but efficient functional queue.
+
+queue__new() -> {[], []}.
+
+queue__put(X, {In, Out}) -> {[X | In], Out}.
+
+queue__get({In, [X | Out]}) -> {ok, X, {In, Out}};
+queue__get({[], _}) -> empty;
+queue__get({In, _}) ->
+    [X | In1] = lists:reverse(In),
+    {ok, X, {[], In1}}.
+
+%% The work list - a queue without repeated elements.
+
+init_work() ->
+    {queue__put(external, queue__new()), sets:new()}.
+
+add_work(Ls, {Q, Set}) ->
+    add_work(Ls, Q, Set).
+
+%% Note that the elements are enqueued in order.
+
+add_work([L | Ls], Q, Set) ->
+    case sets:is_element(L, Set) of
+	true ->
+	    add_work(Ls, Q, Set);
+	false ->
+	    add_work(Ls, queue__put(L, Q), sets:add_element(L, Set))
+    end;
+add_work([], Q, Set) ->
+    {Q, Set}.
+
+take_work({Queue0, Set0}) ->
+    case queue__get(Queue0) of
+	{ok, L, Queue1} ->
+	    Set1 = sets:del_element(L, Set0),
+	    {ok, L, {Queue1, Set1}};
+	empty ->
+	    none
+    end.
+
+get_deps(L, Dep) ->
+    case dict:find(L, Dep) of
+	{ok, Ls} -> Ls;
+	error -> []
+    end.
+
+%% Type information for built-in functions. We do not check that the
+%% arguments have the correct type; if the call would actually fail,
+%% rather than return a value, this is a safe overapproximation.
+
+primop_type(match_fail, 1, _) -> t_none();
+primop_type(_, _, Xs) -> strict(Xs, t_any()).
+
+call_type(M, F, A, Xs) ->
+    erl_bif_types:type(M, F, A, Xs).
+
+guard_filters(T, Env) ->
+    guard_filters(T, Env, dict:new()).
+
+guard_filters(T, Env, Vars) ->
+    case type(T) of
+	call ->
+	    M = call_module(T),
+	    F = call_name(T),
+	    case is_c_atom(M) andalso is_c_atom(F) of
+		true ->
+		    As = call_args(T),
+		    case {atom_val(M), atom_val(F), length(As)} of
+			{erlang, 'and', 2} ->
+			    [A1, A2] = As,
+			    guard_filters(A1, guard_filters(A2, Env));
+			{erlang, is_atom, 1} ->
+			    filter(As, t_atom(), Env);
+			{erlang, is_binary, 1} ->
+			    filter(As, t_binary(), Env);
+			{erlang, is_float, 1} ->
+			    filter(As, t_float(), Env);
+			{erlang, is_function, 1} ->
+			    filter(As, t_fun(), Env);
+			{erlang, is_integer, 1} ->
+			    filter(As, t_integer(), Env);
+			{erlang, is_list, 1} ->
+			    filter(As, t_maybe_improper_list(), Env);
+			{erlang, is_number, 1} ->
+			    filter(As, t_number(), Env);
+			{erlang, is_pid, 1} ->
+			    filter(As, t_pid(), Env);
+			{erlang, is_port, 1} ->
+			    filter(As, t_port(), Env);
+			{erlang, is_reference, 1} ->
+			    filter(As, t_reference(), Env);
+			{erlang, is_tuple, 1} ->
+			    filter(As, t_tuple(), Env);
+			_ ->
+			    Env
+		    end;
+		false ->
+		    Env
+	    end;
+	var ->
+	    case dict:find(var_name(T), Vars) of
+		{ok, T1} ->
+		    guard_filters(T1, Env, Vars);
+		error ->
+		    Env
+	    end;
+	'let' ->
+	    case let_vars(T) of
+		[V] ->
+		    guard_filters(let_body(T), Env,
+				  dict:store(var_name(V), let_arg(T),
+					     Vars));
+		_ ->
+		    Env
+	    end;
+	values ->
+	    case values_es(T) of
+		[T1] ->
+		    guard_filters(T1, Env, Vars);
+		_ ->
+		    Env
+	    end;
+	_ ->
+	    Env
+    end.
+
+filter(As, X, Env) ->
+    [A] = As,
+    case type(A) of
+	var ->
+	    V = var_name(A),
+	    case dict:find(V, Env) of
+		{ok, X1} ->
+		    dict:store(V, meet(X, X1), Env);
+		error ->
+		    dict:store(V, X, Env)
+	    end;
+	_ ->
+	    Env
+    end.
+
+%% Callback hook for cerl_prettypr:
+
+-spec pp_hook() -> fun((cerl:cerl(), _, fun((_,_) -> any())) -> any()).
+
+pp_hook() ->
+    fun pp_hook/3.
+
+pp_hook(Node, Ctxt, Cont) ->
+    As = cerl:get_ann(Node),
+    As1 = proplists:delete(type, proplists:delete(label, As)),
+    As2 = proplists:delete(typesig, proplists:delete(file, As1)),
+    D = Cont(cerl:set_ann(Node, []), Ctxt),
+    T = case proplists:lookup(type, As) of
+	    {type, T0} -> T0;
+	    none ->
+		case proplists:lookup(typesig, As) of
+		    {typesig, T0} -> T0;
+		    none -> t_any()
+		end
+	end,
+    D1 = case erl_types:t_is_any(T) of
+	     true ->
+		 D;
+	     false ->
+		 case cerl:is_literal(Node) of
+		     true ->
+			 D;
+		     false ->
+			 S = erl_types:t_to_string(T),
+			 Q = prettypr:beside(prettypr:text("::"),
+					     prettypr:text(S)),
+			 prettypr:beside(D, Q)
+		 end
+	 end,
+    cerl_prettypr:annotate(D1, As2, Ctxt).
+
+%% =====================================================================