compiler: Break out SSA/beam type definitions into a separate module

9 files changed, 605 insertions, 299 deletions

diff --git a/lib/compiler/src/Makefile b/lib/compiler/src/Makefile
index 0c1dc30f9c..89feb35bc2 100644
--- a/lib/compiler/src/Makefile
+++ b/lib/compiler/src/Makefile
@@ -71,6 +71,7 @@ MODULES =  \
 	beam_ssa_type \
 	beam_kernel_to_ssa \
 	beam_trim \
+	beam_types \
 	beam_utils \
 	beam_validator \
         beam_z \
@@ -103,6 +104,7 @@ HRL_FILES= \
 	beam_disasm.hrl \
 	beam_ssa_opt.hrl \
 	beam_ssa.hrl \
+	beam_types.hrl \
 	core_parse.hrl \
 	v3_kernel.hrl
 
@@ -203,7 +205,8 @@ $(EBIN)/beam_ssa_pp.beam: beam_ssa.hrl
 $(EBIN)/beam_ssa_pre_codegen.beam: beam_ssa.hrl
 $(EBIN)/beam_ssa_recv.beam: beam_ssa.hrl
 $(EBIN)/beam_ssa_share.beam: beam_ssa.hrl
-$(EBIN)/beam_ssa_type.beam: beam_ssa.hrl
+$(EBIN)/beam_ssa_type.beam: beam_ssa.hrl beam_types.hrl
+$(EBIN)/beam_types.beam: beam_types.hrl
 $(EBIN)/cerl.beam: core_parse.hrl
 $(EBIN)/compile.beam: core_parse.hrl ../../stdlib/include/erl_compile.hrl
 $(EBIN)/core_lib.beam: core_parse.hrl
diff --git a/lib/compiler/src/beam_ssa_type.erl b/lib/compiler/src/beam_ssa_type.erl
index f8fefa8936..6d697787c0 100644
--- a/lib/compiler/src/beam_ssa_type.erl
+++ b/lib/compiler/src/beam_ssa_type.erl
@@ -22,6 +22,8 @@
 -export([opt_start/4, opt_continue/4, opt_finish/3]).
 
 -include("beam_ssa_opt.hrl").
+-include("beam_types.hrl").
+
 -import(lists, [all/2,any/2,droplast/1,foldl/3,last/1,member/2,
                 keyfind/3,reverse/1,reverse/2,
                 sort/1,split/2]).
@@ -37,23 +39,6 @@
          sub = #{} :: #{beam_ssa:b_var():=beam_ssa:value()},
          ret_type = [] :: [type()]}).
 
--define(ATOM_SET_SIZE, 5).
-
-%% Records that represent type information.
--record(t_atom, {elements=any :: 'any' | [atom()]}).
--record(t_bs_match, {type :: type()}).
--record(t_fun, {arity=any :: arity() | 'any'}).
--record(t_integer, {elements=any :: 'any' | {integer(),integer()}}).
--record(t_tuple, {size=0 :: integer(),
-                  exact=false :: boolean(),
-                  %% Known element types (1-based index), unknown elements are
-                  %% are assumed to be 'any'.
-                  elements=#{} :: #{ non_neg_integer() => type() }}).
-
--type type() :: 'any' | 'none' |
-                #t_atom{} | #t_bs_match{} | #t_fun{} | #t_integer{} | #t_tuple{} |
-                {'binary',pos_integer()} | 'cons' | 'float' |
-                'list' | 'map' | 'nil' | 'number'.
 -type type_db() :: #{beam_ssa:var_name():=type()}.
 
 -spec opt_start(Linear, Args, Anno, FuncDb) -> {Linear, FuncDb} when
@@ -100,7 +85,7 @@ join_arg_types(Args, ArgTypes, Anno) ->
               end, Ts0, ParamTypes).
 
 join_arg_types_1([Arg | Args], [TM | TMs], Ts) when map_size(TM) =/= 0 ->
-    join_arg_types_1(Args, TMs, Ts#{ Arg => join(maps:values(TM))});
+    join_arg_types_1(Args, TMs, Ts#{ Arg => beam_types:join(maps:values(TM))});
 join_arg_types_1([Arg | Args], [_TM | TMs], Ts) ->
     join_arg_types_1(Args, TMs, Ts#{ Arg => any });
 join_arg_types_1([], [], Ts) ->
@@ -159,7 +144,7 @@ opt_finish_1([Arg | Args], [TypeMap | TypeMaps], ParamInfo)
        map_size(TypeMap) =:= 0 ->
     opt_finish_1(Args, TypeMaps, ParamInfo);
 opt_finish_1([Arg | Args], [TypeMap | TypeMaps], ParamInfo0) ->
-    JoinedType0 = verified_type(join(maps:values(TypeMap))),
+    JoinedType0 = beam_types:join(maps:values(TypeMap)),
     case validator_anno(JoinedType0) of
         any ->
             opt_finish_1(Args, TypeMaps, ParamInfo0);
@@ -232,7 +217,7 @@ opt_1(L, #b_blk{is=Is0,last=Last0}=Blk0, Bs, Ts0,
             %% potentially narrow the type of the phi node
             %% in the former successor.
             Ls = maps:remove(L, D0#d.ls),
-            RetType = join([none|D0#d.ret_type]),
+            RetType = beam_types:join([none|D0#d.ret_type]),
             D = D0#d{ds=Ds,ls=Ls,sub=Sub,
                      func_db=Fdb,ret_type=[RetType]},
             Blk = Blk0#b_blk{is=Is,last=Ret},
@@ -553,14 +538,14 @@ simplify(#b_set{op={bif,is_function},args=[Fun,#b_literal{val=Arity}]}=I, Ts)
     end;
 simplify(#b_set{op={bif,Op0},args=Args}=I, Ts) when Op0 =:= '=='; Op0 =:= '/=' ->
     Types = get_types(Args, Ts),
-    EqEq0 = case {meet(Types),join(Types)} of
-                {none,any} -> true;
-                {#t_integer{},#t_integer{}} -> true;
-                {float,float} -> true;
-                {{binary,_},_} -> true;
-                {#t_atom{},_} -> true;
-                {_,_} -> false
-            end,
+    EqEq0 = case {beam_types:meet(Types),beam_types:join(Types)} of
+               {none,any} -> true;
+               {#t_integer{},#t_integer{}} -> true;
+               {float,float} -> true;
+               {{binary,_},_} -> true;
+               {#t_atom{},_} -> true;
+               {_,_} -> false
+           end,
     EqEq = EqEq0 orelse any_non_numeric_argument(Args, Ts),
     case EqEq of
         true ->
@@ -576,7 +561,7 @@ simplify(#b_set{op={bif,'=:='},args=[Same,Same]}, _Ts) ->
     #b_literal{val=true};
 simplify(#b_set{op={bif,'=:='},args=[A1,_A2]=Args}=I, Ts) ->
     [T1,T2] = get_types(Args, Ts),
-    case meet(T1, T2) of
+    case beam_types:meet(T1, T2) of
         none ->
             #b_literal{val=false};
         _ ->
@@ -813,7 +798,7 @@ opt_switch(#b_switch{fail=Fail,list=List0}=Sw0, Type, Ts, Ds) ->
 prune_switch_list([{_,Fail}|T], Fail, Type, Ts) ->
     prune_switch_list(T, Fail, Type, Ts);
 prune_switch_list([{Arg,_}=Pair|T], Fail, Type, Ts) ->
-    case meet(get_type(Arg, Ts), Type) of
+    case beam_types:meet(get_type(Arg, Ts), Type) of
         none ->
             %% Different types. This value can never match.
             prune_switch_list(T, Fail, Type, Ts);
@@ -873,7 +858,7 @@ update_successors(#b_ret{arg=Arg}, Ts, D) ->
             %% type.
             D;
         #{} ->
-            RetType = join([get_type(Arg, Ts) | D#d.ret_type]),
+            RetType = beam_types:join([get_type(Arg, Ts) | D#d.ret_type]),
             D#d{ret_type=[RetType]}
     end.
 
@@ -882,7 +867,7 @@ subtract_sw_list(V, List, Ts) ->
 
 sub_sw_list_1(Type, [{Val,_}|T], Ts) ->
     ValType = get_type(Val, Ts),
-    sub_sw_list_1(subtract(Type, ValType), T, Ts);
+    sub_sw_list_1(beam_types:subtract(Type, ValType), T, Ts);
 sub_sw_list_1(Type, [], _Ts) ->
     Type.
 
@@ -916,7 +901,7 @@ update_types(#b_set{op=Op,dst=Dst,args=Args}, Ts, Ds) ->
 
 type(phi, Args, Ts, _Ds) ->
     Types = [get_type(A, Ts) || {A,_} <- Args],
-    join(Types);
+    beam_types:join(Types);
 type({bif,'band'}, Args, Ts, _Ds) ->
     band_type(Args, Ts);
 type({bif,Bif}, Args, Ts, _Ds) ->
@@ -1158,8 +1143,8 @@ t_two_tuple(Type1, Type2) ->
 %%  Test whether TestOperation applied to an argument of type Type
 %%  will succeed.  Return yes, no, or maybe.
 %%
-%%  Type is a type as described in the comment for verified_type/1 at
-%%  the very end of this file, but it will *never* be 'any'.
+%%  Type can be any type as described in beam_types.hrl, but it must *never* be
+%%  any.
 
 will_succeed(is_atom, Type) ->
     case Type of
@@ -1351,7 +1336,7 @@ simplify_is_record(I, #t_tuple{exact=Exact,
                    #b_literal{} -> no;
                    none ->
                        %% Is it at all possible for the tag to match?
-                       case meet(get_type(RecTag, Ts), TagType) of
+                       case beam_types:meet(get_type(RecTag, Ts), TagType) of
                            none -> no;
                            _ -> maybe
                        end
@@ -1548,7 +1533,7 @@ infer_eq_type({bif,'=:='}, [#b_var{}=Arg0,#b_var{}=Arg1], Ts, _Ds) ->
     %% be inferred that L1 is 'cons' (the meet of 'cons' and 'list').
     Type0 = get_type(Arg0, Ts),
     Type1 = get_type(Arg1, Ts),
-    Type = meet(Type0, Type1),
+    Type = beam_types:meet(Type0, Type1),
     [{V,MeetType} ||
         {V,OrigType,MeetType} <-
             [{Arg0,Type0,Type},{Arg1,Type1,Type}],
@@ -1748,7 +1733,7 @@ join_types_1([V|Vs], Ts0, Ts1) ->
         {#{V:=Same},#{V:=Same}} ->
             join_types_1(Vs, Ts0, Ts1);
         {#{V:=T0},#{V:=T1}} ->
-            case join(T0, T1) of
+            case beam_types:join(T0, T1) of
                 T1 ->
                     join_types_1(Vs, Ts0, Ts1);
                 T ->
@@ -1760,10 +1745,6 @@ join_types_1([V|Vs], Ts0, Ts1) ->
 join_types_1([], Ts0, Ts1) ->
     maps:merge(Ts0, Ts1).
 
-join([T1,T2|Ts]) ->
-    join([join(T1, T2)|Ts]);
-join([T]) -> T.
-
 get_literal_from_type(#t_atom{elements=[Atom]}) ->
     #b_literal{val=Atom};
 get_literal_from_type(#t_integer{elements={Int,Int}}) ->
@@ -1825,271 +1806,18 @@ set_element_type(Key, any, Es) ->
 set_element_type(Key, Type, Es) ->
     Es#{ Key => Type }.
 
-%% join(Type1, Type2) -> Type
-%%  Return the "join" of Type1 and Type2. The join is a more general
-%%  type than Type1 and Type2. For example:
-%%
-%%     join(#t_integer{elements=any}, #t_integer=elements={0,3}}) ->
-%%          #t_integer{}
-%%
-%%  The join for two different types result in 'any', which is
-%%  the top element for our type lattice:
-%%
-%%     join(#t_integer{}, map) -> any
-
--spec join(type(), type()) -> type().
-
-join(T, T) ->
-    verified_type(T);
-join(none, T) ->
-    verified_type(T);
-join(T, none) ->
-    verified_type(T);
-join(any, _) -> any;
-join(_, any) -> any;
-join(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) ->
-    Set = ordsets:union(Set1, Set2),
-    case ordsets:size(Set) of
-        Size when Size =< ?ATOM_SET_SIZE ->
-            #t_atom{elements=Set};
-        _Size ->
-            #t_atom{elements=any}
-    end;
-join(#t_atom{elements=any}=T, #t_atom{elements=[_|_]}) -> T;
-join(#t_atom{elements=[_|_]}, #t_atom{elements=any}=T) -> T;
-join({binary,U1}, {binary,U2}) ->
-    {binary,gcd(U1, U2)};
-join(#t_fun{}, #t_fun{}) -> #t_fun{};
-join(#t_integer{elements={MinA,MaxA}},
-     #t_integer{elements={MinB,MaxB}}) ->
-    #t_integer{elements={min(MinA,MinB),max(MaxA,MaxB)}};
-join(#t_integer{}, #t_integer{}) -> t_integer();
-join(list, cons) -> list;
-join(cons, list) -> list;
-join(nil, cons) -> list;
-join(cons, nil) -> list;
-join(nil, list) -> list;
-join(list, nil) -> list;
-join(#t_integer{}, float) -> number;
-join(float, #t_integer{}) -> number;
-join(#t_integer{}, number) -> number;
-join(number, #t_integer{}) -> number;
-join(float, number) -> number;
-join(number, float) -> number;
-join(#t_tuple{size=Sz,exact=ExactA,elements=EsA},
-     #t_tuple{size=Sz,exact=ExactB,elements=EsB}) ->
-    Exact = ExactA and ExactB,
-    Es = join_tuple_elements(Sz, EsA, EsB),
-    #t_tuple{size=Sz,exact=Exact,elements=Es};
-join(#t_tuple{size=SzA,elements=EsA}, #t_tuple{size=SzB,elements=EsB}) ->
-    Sz = min(SzA, SzB),
-    Es = join_tuple_elements(Sz, EsA, EsB),
-    #t_tuple{size=Sz,elements=Es};
-join(_T1, _T2) ->
-    %%io:format("~p ~p\n", [_T1,_T2]),
-    any.
-
-join_tuple_elements(MinSize, EsA, EsB) ->
-    Es0 = join_elements(EsA, EsB),
-    maps:filter(fun(Index, _Type) -> Index =< MinSize end, Es0).
-
-join_elements(Es1, Es2) ->
-    Keys = if
-               map_size(Es1) =< map_size(Es2) -> maps:keys(Es1);
-               map_size(Es1) > map_size(Es2) -> maps:keys(Es2)
-           end,
-    join_elements_1(Keys, Es1, Es2, #{}).
-
-join_elements_1([Key | Keys], Es1, Es2, Acc0) ->
-    case {Es1, Es2} of
-        {#{ Key := Type1 }, #{ Key := Type2 }} ->
-            Acc = set_element_type(Key, join(Type1, Type2), Acc0),
-            join_elements_1(Keys, Es1, Es2, Acc);
-        {#{}, #{}} ->
-            join_elements_1(Keys, Es1, Es2, Acc0)
-    end;
-join_elements_1([], _Es1, _Es2, Acc) ->
-    Acc.
-
-gcd(A, B) ->
-    case A rem B of
-        0 -> B;
-        X -> gcd(B, X)
-    end.
-
 meet_types([{V,T0}|Vs], Ts) ->
     #{V:=T1} = Ts,
-    case meet(T0, T1) of
+    case beam_types:meet(T0, T1) of
         T1 -> meet_types(Vs, Ts);
         T -> meet_types(Vs, Ts#{V:=T})
     end;
 meet_types([], Ts) -> Ts.
 
-meet([T1,T2|Ts]) ->
-    meet([meet(T1, T2)|Ts]);
-meet([T]) -> T.
-
 subtract_types([{V,T0}|Vs], Ts) ->
     #{V:=T1} = Ts,
-    case subtract(T1, T0) of
+    case beam_types:subtract(T1, T0) of
         T1 -> subtract_types(Vs, Ts);
         T -> subtract_types(Vs, Ts#{V:=T})
     end;
 subtract_types([], Ts) -> Ts.
-
-%% subtract(Type1, Type2) -> Type.
-%%  Subtract Type2 from Type1. Example:
-%%
-%%     subtract(list, cons) -> nil
-
-subtract(#t_atom{elements=[_|_]=Set0}, #t_atom{elements=[_|_]=Set1}) ->
-    case ordsets:subtract(Set0, Set1) of
-        [] -> none;
-        [_|_]=Set -> #t_atom{elements=Set}
-    end;
-subtract(number, float) -> #t_integer{};
-subtract(number, #t_integer{elements=any}) -> float;
-subtract(list, cons) -> nil;
-subtract(list, nil) -> cons;
-subtract(T, _) -> T.
-
-%% meet(Type1, Type2) -> Type
-%%  Return the "meet" of Type1 and Type2. The meet is a narrower
-%%  type than Type1 and Type2. For example:
-%%
-%%     meet(#t_integer{elements=any}, #t_integer{elements={0,3}}) ->
-%%          #t_integer{elements={0,3}}
-%%
-%%  The meet for two different types result in 'none', which is
-%%  the bottom element for our type lattice:
-%%
-%%     meet(#t_integer{}, map) -> none
-
--spec meet(type(), type()) -> type().
-
-meet(T, T) ->
-    verified_type(T);
-meet(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) ->
-    case ordsets:intersection(Set1, Set2) of
-        [] ->
-            none;
-        [_|_]=Set ->
-            #t_atom{elements=Set}
-    end;
-meet(#t_atom{elements=[_|_]}=T, #t_atom{elements=any}) ->
-    T;
-meet(#t_atom{elements=any}, #t_atom{elements=[_|_]}=T) ->
-    T;
-meet(#t_fun{arity=any}, #t_fun{}=T) ->
-    T;
-meet(#t_fun{}=T, #t_fun{arity=any}) ->
-    T;
-meet(#t_integer{elements={_,_}}=T, #t_integer{elements=any}) ->
-    T;
-meet(#t_integer{elements=any}, #t_integer{elements={_,_}}=T) ->
-    T;
-meet(#t_integer{elements={MinA,MaxA}}, #t_integer{elements={MinB,MaxB}})
-  when MinA >= MinB, MaxA =< MaxB;
-       MinB >= MinA, MaxB =< MaxA ->
-    #t_integer{elements={max(MinA, MinB),min(MaxA, MaxB)}};
-meet(#t_integer{}=T, number) -> T;
-meet(float=T, number) -> T;
-meet(number, #t_integer{}=T) -> T;
-meet(number, float=T) -> T;
-meet(list, cons) -> cons;
-meet(list, nil) -> nil;
-meet(cons, list) -> cons;
-meet(nil, list) -> nil;
-meet(#t_tuple{}=T1, #t_tuple{}=T2) ->
-    meet_tuples(T1, T2);
-meet({binary,U1}, {binary,U2}) ->
-    {binary, U1 * U2 div gcd(U1, U2)};
-meet(any, T) ->
-    verified_type(T);
-meet(T, any) ->
-    verified_type(T);
-meet(_, _) ->
-    %% Inconsistent types. There will be an exception at runtime.
-    none.
-
-meet_tuples(#t_tuple{size=Sz1,exact=true},
-            #t_tuple{size=Sz2,exact=true}) when Sz1 =/= Sz2 ->
-    none;
-meet_tuples(#t_tuple{size=Sz1,exact=Ex1,elements=Es1},
-            #t_tuple{size=Sz2,exact=Ex2,elements=Es2}) ->
-    Size = max(Sz1, Sz2),
-    Exact = Ex1 or Ex2,
-    case meet_elements(Es1, Es2) of
-        none ->
-            none;
-        Es ->
-            #t_tuple{size=Size,exact=Exact,elements=Es}
-    end.
-
-meet_elements(Es1, Es2) ->
-    Keys = maps:keys(Es1) ++ maps:keys(Es2),
-    meet_elements_1(Keys, Es1, Es2, #{}).
-
-meet_elements_1([Key | Keys], Es1, Es2, Acc) ->
-    case {Es1, Es2} of
-        {#{ Key := Type1 }, #{ Key := Type2 }} ->
-            case meet(Type1, Type2) of
-                none -> none;
-                Type -> meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type })
-            end;
-        {#{ Key := Type1 }, _} ->
-            meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type1 });
-        {_, #{ Key := Type2 }} ->
-            meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type2 })
-    end;
-meet_elements_1([], _Es1, _Es2, Acc) ->
-    Acc.
-
-%% verified_type(Type) -> Type
-%%  Returns the passed in type if it is one of the defined types.
-%%  Crashes if there is anything wrong with the type.
-%%
-%%  Here are all possible types:
-%%
-%%  any                  Any Erlang term (top element for the type lattice).
-%%
-%%  #t_atom{}            Any atom or some specific atoms.
-%%  {binary,Unit}        Binary/bitstring aligned to unit Unit.
-%%  float                Floating point number.
-%%  #t_integer{}         Integer
-%%  list                 Empty or nonempty list.
-%%  map                  Map.
-%%  nil                  Empty list.
-%%  cons                 Cons (nonempty list).
-%%  number               A number (float or integer).
-%%  #t_tuple{}           Tuple.
-%%
-%%  none                 No type (bottom element for the type lattice).
-
--spec verified_type(T) -> T when
-      T :: type().
-
-verified_type(any=T) -> T;
-verified_type(none=T) -> T;
-verified_type(#t_atom{elements=any}=T) -> T;
-verified_type(#t_atom{elements=[_|_]}=T) -> T;
-verified_type({binary,U}=T) when is_integer(U) -> T;
-verified_type(#t_fun{arity=Arity}=T) when Arity =:= any; is_integer(Arity) -> T;
-verified_type(#t_integer{elements=any}=T) -> T;
-verified_type(#t_integer{elements={Min,Max}}=T)
-  when is_integer(Min), is_integer(Max), Min =< Max -> T;
-verified_type(list=T) -> T;
-verified_type(map=T) -> T;
-verified_type(nil=T) -> T;
-verified_type(cons=T) -> T;
-verified_type(number=T) -> T;
-verified_type(#t_tuple{size=Size,elements=Es}=T) ->
-    %% All known elements must have a valid index and type. 'any' is prohibited
-    %% since it's implicit and should never be present in the map.
-    maps:fold(fun(Index, Element, _) when is_integer(Index),
-                                          1 =< Index, Index =< Size,
-                                          Element =/= any, Element =/= none ->
-                      verified_type(Element)
-              end, [], Es),
-    T;
-verified_type(float=T) -> T.
diff --git a/lib/compiler/src/beam_types.erl b/lib/compiler/src/beam_types.erl
new file mode 100644
index 0000000000..6fcc70a4bd
--- /dev/null
+++ b/lib/compiler/src/beam_types.erl
@@ -0,0 +1,294 @@
+%%
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2019. All Rights Reserved.
+%%
+%% Licensed under the Apache License, Version 2.0 (the "License");
+%% you may not use this file except in compliance with the License.
+%% You may obtain a copy of the License at
+%%
+%%     http://www.apache.org/licenses/LICENSE-2.0
+%%
+%% Unless required by applicable law or agreed to in writing, software
+%% distributed under the License is distributed on an "AS IS" BASIS,
+%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+%% See the License for the specific language governing permissions and
+%% limitations under the License.
+%%
+%% %CopyrightEnd%
+%%
+
+-module(beam_types).
+
+-include("beam_types.hrl").
+
+-import(lists, [foldl/3, reverse/1]).
+
+-export([meet/1, meet/2, join/1, join/2, subtract/2, verified_type/1]).
+
+-export([call_types/3]).
+
+%%%
+%%% Type constructors
+%%%
+
+-spec t_boolean() -> type().
+t_boolean() -> #t_atom{elements=[false,true]}.
+
+%%%
+%%% Type operators
+%%%
+
+%% Return the "join" of Type1 and Type2. The join is a more general
+%% type than Type1 and Type2. For example:
+%%
+%%    join(#t_integer{elements=any}, #t_integer=elements={0,3}}) ->
+%%         #t_integer{}
+%%
+%% The join for two different types result in 'any', which is
+%% the top element for our type lattice:
+%%
+%%    join(#t_integer{}, map) -> any
+
+-spec join(type(), type()) -> type().
+
+join(T, T) ->
+    verified_type(T);
+join(none, T) ->
+    verified_type(T);
+join(T, none) ->
+    verified_type(T);
+join(any, _) -> any;
+join(_, any) -> any;
+join(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) ->
+    Set = ordsets:union(Set1, Set2),
+    case ordsets:size(Set) of
+        Size when Size =< ?ATOM_SET_SIZE ->
+            #t_atom{elements=Set};
+        _Size ->
+            #t_atom{elements=any}
+    end;
+join(#t_atom{elements=any}=T, #t_atom{elements=[_|_]}) -> T;
+join(#t_atom{elements=[_|_]}, #t_atom{elements=any}=T) -> T;
+join({binary,U1}, {binary,U2}) ->
+    {binary,gcd(U1, U2)};
+join(#t_fun{}, #t_fun{}) ->
+    #t_fun{};
+join(#t_integer{elements={MinA,MaxA}},
+     #t_integer{elements={MinB,MaxB}}) ->
+    #t_integer{elements={min(MinA,MinB),max(MaxA,MaxB)}};
+join(#t_integer{}, #t_integer{}) -> #t_integer{};
+join(list, cons) -> list;
+join(cons, list) -> list;
+join(nil, cons) -> list;
+join(cons, nil) -> list;
+join(nil, list) -> list;
+join(list, nil) -> list;
+join(#t_integer{}, float) -> number;
+join(float, #t_integer{}) -> number;
+join(#t_integer{}, number) -> number;
+join(number, #t_integer{}) -> number;
+join(float, number) -> number;
+join(number, float) -> number;
+join(#t_tuple{size=Sz,exact=ExactA,elements=EsA},
+     #t_tuple{size=Sz,exact=ExactB,elements=EsB}) ->
+    Exact = ExactA and ExactB,
+    Es = join_tuple_elements(Sz, EsA, EsB),
+    #t_tuple{size=Sz,exact=Exact,elements=Es};
+join(#t_tuple{size=SzA,elements=EsA}, #t_tuple{size=SzB,elements=EsB}) ->
+    Sz = min(SzA, SzB),
+    Es = join_tuple_elements(Sz, EsA, EsB),
+    #t_tuple{size=Sz,elements=Es};
+join(_T1, _T2) ->
+    %%io:format("~p ~p\n", [_T1,_T2]),
+    any.
+
+join_tuple_elements(MinSize, EsA, EsB) ->
+    Es0 = join_elements(EsA, EsB),
+    maps:filter(fun(Index, _Type) -> Index =< MinSize end, Es0).
+
+join_elements(Es1, Es2) ->
+    Keys = if
+               map_size(Es1) =< map_size(Es2) -> maps:keys(Es1);
+               map_size(Es1) > map_size(Es2) -> maps:keys(Es2)
+           end,
+    join_elements_1(Keys, Es1, Es2, #{}).
+
+join_elements_1([Key | Keys], Es1, Es2, Acc0) ->
+    case {Es1, Es2} of
+        {#{ Key := Type1 }, #{ Key := Type2 }} ->
+            Acc = set_element_type(Key, join(Type1, Type2), Acc0),
+            join_elements_1(Keys, Es1, Es2, Acc);
+        {#{}, #{}} ->
+            join_elements_1(Keys, Es1, Es2, Acc0)
+    end;
+join_elements_1([], _Es1, _Es2, Acc) ->
+    Acc.
+
+gcd(A, B) ->
+    case A rem B of
+        0 -> B;
+        X -> gcd(B, X)
+    end.
+
+set_element_type(_Key, none, Es) ->
+    Es;
+set_element_type(Key, any, Es) ->
+    maps:remove(Key, Es);
+set_element_type(Key, Type, Es) ->
+    Es#{ Key => Type }.
+
+%% Subtract Type2 from Type1. Example:
+%%    subtract(list, cons) -> nil
+
+-spec subtract(type(), type()) -> type().
+
+subtract(#t_atom{elements=[_|_]=Set0}, #t_atom{elements=[_|_]=Set1}) ->
+    case ordsets:subtract(Set0, Set1) of
+        [] -> none;
+        [_|_]=Set -> #t_atom{elements=Set}
+    end;
+subtract(number, float) -> #t_integer{};
+subtract(number, #t_integer{elements=any}) -> float;
+subtract(list, cons) -> nil;
+subtract(list, nil) -> cons;
+subtract(T, _) -> T.
+
+%% Return the "meet" of Type1 and Type2. The meet is a narrower
+%% type than Type1 and Type2. For example:
+%%
+%%    meet(#t_integer{elements=any}, #t_integer{elements={0,3}}) ->
+%%         #t_integer{elements={0,3}}
+%%
+%% The meet for two different types result in 'none', which is
+%% the bottom element for our type lattice:
+%%
+%%    meet(#t_integer{}, map) -> none
+
+-spec meet(type(), type()) -> type().
+
+meet(T, T) ->
+    verified_type(T);
+meet(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) ->
+    case ordsets:intersection(Set1, Set2) of
+        [] ->
+            none;
+        [_|_]=Set ->
+            #t_atom{elements=Set}
+    end;
+meet(#t_atom{elements=[_|_]}=T, #t_atom{elements=any}) ->
+    T;
+meet(#t_atom{elements=any}, #t_atom{elements=[_|_]}=T) ->
+    T;
+meet(#t_fun{arity=any}, #t_fun{}=T) ->
+    T;
+meet(#t_fun{}=T, #t_fun{arity=any}) ->
+    T;
+meet(#t_integer{elements={_,_}}=T, #t_integer{elements=any}) ->
+    T;
+meet(#t_integer{elements=any}, #t_integer{elements={_,_}}=T) ->
+    T;
+meet(#t_integer{elements={MinA,MaxA}}, #t_integer{elements={MinB,MaxB}})
+  when MinA >= MinB, MaxA =< MaxB;
+       MinB >= MinA, MaxB =< MaxA ->
+    #t_integer{elements={max(MinA, MinB),min(MaxA, MaxB)}};
+meet(#t_integer{}=T, number) -> T;
+meet(float=T, number) -> T;
+meet(number, #t_integer{}=T) -> T;
+meet(number, float=T) -> T;
+meet(list, cons) -> cons;
+meet(list, nil) -> nil;
+meet(cons, list) -> cons;
+meet(nil, list) -> nil;
+meet(#t_tuple{}=T1, #t_tuple{}=T2) ->
+    meet_tuples(T1, T2);
+meet({binary,U1}, {binary,U2}) ->
+    {binary, U1 * U2 div gcd(U1, U2)};
+meet(any, T) ->
+    verified_type(T);
+meet(T, any) ->
+    verified_type(T);
+meet(_, _) ->
+    %% Inconsistent types. There will be an exception at runtime.
+    none.
+
+meet_tuples(#t_tuple{size=Sz1,exact=true},
+            #t_tuple{size=Sz2,exact=true}) when Sz1 =/= Sz2 ->
+    none;
+meet_tuples(#t_tuple{size=Sz1,exact=Ex1,elements=Es1},
+            #t_tuple{size=Sz2,exact=Ex2,elements=Es2}) ->
+    Size = max(Sz1, Sz2),
+    Exact = Ex1 or Ex2,
+    case meet_elements(Es1, Es2) of
+        none ->
+            none;
+        Es ->
+            #t_tuple{size=Size,exact=Exact,elements=Es}
+    end.
+
+meet_elements(Es1, Es2) ->
+    Keys = maps:keys(Es1) ++ maps:keys(Es2),
+    meet_elements_1(Keys, Es1, Es2, #{}).
+
+meet_elements_1([Key | Keys], Es1, Es2, Acc) ->
+    case {Es1, Es2} of
+        {#{ Key := Type1 }, #{ Key := Type2 }} ->
+            case meet(Type1, Type2) of
+                none -> none;
+                Type -> meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type })
+            end;
+        {#{ Key := Type1 }, _} ->
+            meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type1 });
+        {_, #{ Key := Type2 }} ->
+            meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type2 })
+    end;
+meet_elements_1([], _Es1, _Es2, Acc) ->
+    Acc.
+
+%% Returns the passed in type if it is well-formed and safe to pass to
+%% arbitrary code, and crashes if there's anything wrong with it.
+%%
+%% Currently, all types described in beam_types.hrl except for #t_bs_match{}
+%% are considered safe.
+
+-spec verified_type(T) -> T when
+      T :: type().
+
+verified_type(any=T) -> T;
+verified_type(none=T) -> T;
+verified_type(#t_atom{elements=any}=T) -> T;
+verified_type(#t_atom{elements=[_|_]}=T) -> T;
+verified_type({binary,U}=T) when is_integer(U) -> T;
+verified_type(#t_fun{arity=Arity}=T) when Arity =:= any; is_integer(Arity) -> T;
+verified_type(#t_integer{elements=any}=T) -> T;
+verified_type(#t_integer{elements={Min,Max}}=T)
+  when is_integer(Min), is_integer(Max), Min =< Max -> T;
+verified_type(list=T) -> T;
+verified_type(map=T) -> T;
+verified_type(nil=T) -> T;
+verified_type(cons=T) -> T;
+verified_type(number=T) -> T;
+verified_type(#t_tuple{size=Size,elements=Es}=T) ->
+    %% All known elements must have a valid index and type. 'any' is prohibited
+    %% since it's implicit and should never be present in the map.
+    maps:fold(fun(Index, Element, _) when is_integer(Index),
+                                          1 =< Index, Index =< Size,
+                                          Element =/= any, Element =/= none ->
+                      verified_type(Element)
+              end, [], Es),
+    T;
+verified_type(float=T) -> T.
+
+%% Joins all the given types into a single type.
+-spec join([type()]) -> type().
+
+join([T1,T2|Ts]) ->
+    join([join(T1, T2)|Ts]);
+join([T]) -> T.
+
+%% Meets all the given types into a single type.
+-spec meet([type()]) -> type().
+
+meet([T1,T2|Ts]) ->
+    meet([meet(T1, T2)|Ts]);
+meet([T]) -> T.
diff --git a/lib/compiler/src/beam_types.hrl b/lib/compiler/src/beam_types.hrl
new file mode 100644
index 0000000000..dfbf104a2a
--- /dev/null
+++ b/lib/compiler/src/beam_types.hrl
@@ -0,0 +1,58 @@
+%%
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2019. All Rights Reserved.
+%%
+%% Licensed under the Apache License, Version 2.0 (the "License");
+%% you may not use this file except in compliance with the License.
+%% You may obtain a copy of the License at
+%%
+%%     http://www.apache.org/licenses/LICENSE-2.0
+%%
+%% Unless required by applicable law or agreed to in writing, software
+%% distributed under the License is distributed on an "AS IS" BASIS,
+%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+%% See the License for the specific language governing permissions and
+%% limitations under the License.
+%%
+%% %CopyrightEnd%
+%%
+
+%% Common term types for passes operating on beam SSA and assembly. Helper
+%% functions for wrangling these can be found in beam_types.erl
+%%
+%% The type lattice is as follows:
+%%
+%%  any                  Any Erlang term (top element).
+%%
+%%    - atom             An atom.
+%%    - {binary,Unit}    A bitstring aligned to unit Unit.
+%%    - #t_bs_match{}    A match context.
+%%    - #t_fun{}         A fun.
+%%    - map              A map.
+%%    - number           A number.
+%%       -- float        Floating point number.
+%%       -- integer      Integer.
+%%    - list             A list.
+%%       -- cons         Cons (nonempty list).
+%%       -- nil          The empty list.
+%%    - #t_tuple{}       Tuple.
+%%
+%%  none                 No type (bottom element).
+
+-define(ATOM_SET_SIZE, 5).
+
+-record(t_atom, {elements=any :: 'any' | [atom()]}).
+-record(t_fun, {arity=any :: arity() | 'any'}).
+-record(t_integer, {elements=any :: 'any' | {integer(),integer()}}).
+-record(t_bs_match, {type :: type()}).
+-record(t_tuple, {size=0 :: integer(),
+                  exact=false :: boolean(),
+                  %% Known element types (1-based index), unknown elements are
+                  %% are assumed to be 'any'.
+                  elements=#{} :: #{ non_neg_integer() => type() }}).
+
+-type type() :: 'any' | 'none' |
+                #t_atom{} | #t_bs_match{} | #t_fun{} | #t_integer{} |
+                #t_tuple{} | {'binary',pos_integer()} | 'cons' | 'float' |
+                'list' | 'map' | 'nil' | 'number'.
diff --git a/lib/compiler/src/compile.erl b/lib/compiler/src/compile.erl
index e5e63341b7..28ab8813ba 100644
--- a/lib/compiler/src/compile.erl
+++ b/lib/compiler/src/compile.erl
@@ -2111,6 +2111,7 @@ pre_load() ->
 	 beam_ssa_share,
 	 beam_ssa_type,
 	 beam_trim,
+	 beam_types,
 	 beam_utils,
 	 beam_validator,
 	 beam_z,
diff --git a/lib/compiler/src/compiler.app.src b/lib/compiler/src/compiler.app.src
index 9dc3b6e339..22ef67f357 100644
--- a/lib/compiler/src/compiler.app.src
+++ b/lib/compiler/src/compiler.app.src
@@ -46,6 +46,7 @@
              beam_ssa_share,
              beam_ssa_type,
 	     beam_trim,
+             beam_types,
 	     beam_utils,
 	     beam_validator,
 	     beam_z,
diff --git a/lib/compiler/test/Makefile b/lib/compiler/test/Makefile
index db8eb7e2e1..2c0767b17f 100644
--- a/lib/compiler/test/Makefile
+++ b/lib/compiler/test/Makefile
@@ -16,6 +16,7 @@ MODULES= \
 	beam_reorder_SUITE \
 	beam_ssa_SUITE \
 	beam_type_SUITE \
+	beam_types_SUITE \
 	beam_utils_SUITE \
 	bif_SUITE \
 	bs_bincomp_SUITE \
@@ -225,6 +226,6 @@ release_tests_spec: make_emakefile
 	$(INSTALL_DATA) $(ERL_DUMMY_FILES) "$(RELSYSDIR)"
 	rm $(ERL_DUMMY_FILES)
 	chmod -R u+w "$(RELSYSDIR)"
-	@tar cf - *_SUITE_data | (cd "$(RELSYSDIR)"; tar xf -)
+	@tar cf - *_SUITE_data property_test | (cd "$(RELSYSDIR)"; tar xf -)
 
 release_docs_spec:
diff --git a/lib/compiler/test/beam_types_SUITE.erl b/lib/compiler/test/beam_types_SUITE.erl
new file mode 100644
index 0000000000..66fd517ec0
--- /dev/null
+++ b/lib/compiler/test/beam_types_SUITE.erl
@@ -0,0 +1,80 @@
+%%
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2019. All Rights Reserved.
+%%
+%% Licensed under the Apache License, Version 2.0 (the "License");
+%% you may not use this file except in compliance with the License.
+%% You may obtain a copy of the License at
+%%
+%%     http://www.apache.org/licenses/LICENSE-2.0
+%%
+%% Unless required by applicable law or agreed to in writing, software
+%% distributed under the License is distributed on an "AS IS" BASIS,
+%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+%% See the License for the specific language governing permissions and
+%% limitations under the License.
+%%
+%% %CopyrightEnd%
+%%
+
+-module(beam_types_SUITE).
+
+-include_lib("compiler/src/beam_types.hrl").
+
+-export([all/0, suite/0, groups/0,
+         init_per_suite/1, end_per_suite/1]).
+
+-export([consistency/1, commutativity/1,
+         binary_consistency/1, integer_consistency/1]).
+
+suite() ->
+    [{ct_hooks,[ts_install_cth]}].
+
+all() ->
+    [{group,property_tests}].
+
+groups() ->
+    [{property_tests,[], [consistency, commutativity,
+                          binary_consistency, integer_consistency]}].
+
+init_per_suite(Config) ->
+    ct_property_test:init_per_suite(Config).
+
+end_per_suite(Config) ->
+    Config.
+
+consistency(Config) when is_list(Config) ->
+    %% manual test: proper:quickcheck(beam_types_prop:consistency()).
+    true = ct_property_test:quickcheck(beam_types_prop:consistency(), Config).
+
+commutativity(Config) when is_list(Config) ->
+    %% manual test: proper:quickcheck(beam_types_prop:commutativity()).
+    true = ct_property_test:quickcheck(beam_types_prop:commutativity(), Config).
+
+binary_consistency(Config) when is_list(Config) ->
+    %% These binaries should meet into {binary,12} as that's the best common
+    %% unit for both types.
+    A = {binary, 4},
+    B = {binary, 6},
+
+    {binary, 12} = beam_types:meet(A, B),
+    {binary, 2} = beam_types:join(A, B),
+
+    A = beam_types:meet(A, beam_types:join(A, B)),
+    A = beam_types:join(A, beam_types:meet(A, B)),
+
+    ok.
+
+integer_consistency(Config) when is_list(Config) ->
+    %% Integers that don't overlap fully should never meet.
+    A = #t_integer{elements={3,5}},
+    B = #t_integer{elements={4,6}},
+
+    none = beam_types:meet(A, B),
+    #t_integer{elements={3,6}} = beam_types:join(A, B),
+
+    A = beam_types:meet(A, beam_types:join(A, B)),
+    A = beam_types:join(A, beam_types:meet(A, B)),
+
+    ok.
diff --git a/lib/compiler/test/property_test/beam_types_prop.erl b/lib/compiler/test/property_test/beam_types_prop.erl
new file mode 100644
index 0000000000..815e353853
--- /dev/null
+++ b/lib/compiler/test/property_test/beam_types_prop.erl
@@ -0,0 +1,140 @@
+%%
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2019. All Rights Reserved.
+%%
+%% Licensed under the Apache License, Version 2.0 (the "License");
+%% you may not use this file except in compliance with the License.
+%% You may obtain a copy of the License at
+%%
+%%     http://www.apache.org/licenses/LICENSE-2.0
+%%
+%% Unless required by applicable law or agreed to in writing, software
+%% distributed under the License is distributed on an "AS IS" BASIS,
+%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+%% See the License for the specific language governing permissions and
+%% limitations under the License.
+%%
+%% %CopyrightEnd%
+%%
+
+-module(beam_types_prop).
+
+-compile([export_all, nowarn_export_all]).
+
+%% This module has only supports proper, as we don't have an eqc license to
+%% test with.
+
+-proptest([proper]).
+
+-ifdef(PROPER).
+
+-include_lib("compiler/src/beam_types.hrl").
+
+-include_lib("proper/include/proper.hrl").
+-define(MOD_eqc,proper).
+
+consistency() ->
+    ?FORALL({TypeA, TypeB},
+            ?LET(TypeA, type(),
+                 ?LET(TypeB, type(), {TypeA, TypeB})),
+            consistency_check(TypeA, TypeB)).
+
+consistency_check(A, B) ->
+    consistency_check_1(A, B),
+    consistency_check_1(B, A),
+    true.
+
+consistency_check_1(A, B) ->
+    A = beam_types:meet(A, beam_types:join(A, B)),
+    A = beam_types:join(A, beam_types:meet(A, B)),
+    ok.
+
+commutativity() ->
+    ?FORALL({TypeA, TypeB},
+            ?LET(TypeA, type(),
+                 ?LET(TypeB, type(), {TypeA, TypeB})),
+            commutativity_check(TypeA, TypeB)).
+
+commutativity_check(A, B) ->
+    true = beam_types:meet(A, B) =:= beam_types:meet(B, A),
+    true = beam_types:join(A, B) =:= beam_types:join(B, A),
+    true.
+
+%%%
+%%% Generators
+%%%
+
+type() ->
+    type(0).
+
+type(Depth) ->
+    oneof(nested_types(Depth) ++
+              numerical_types() ++
+              list_types() ++
+              other_types()).
+
+other_types() ->
+    [any, gen_atom(), gen_binary(), none].
+
+list_types() ->
+    [cons, list, nil].
+
+numerical_types() ->
+    [gen_integer(), float, number].
+
+nested_types(Depth) when Depth >= 3 -> [];
+nested_types(Depth) -> [map, gen_tuple(Depth + 1)].
+
+gen_atom() ->
+    ?LET(Size, range(0, ?ATOM_SET_SIZE),
+         case Size of
+             0 ->
+                 #t_atom{};
+             _ ->
+                 ?LET(Set, sized_list(Size, atom()),
+                      begin
+                          #t_atom{elements=ordsets:from_list(Set)}
+                      end)
+         end).
+
+gen_binary() ->
+    ?SHRINK({binary, range(1, 128)},
+            [{binary, [1, 2, 3, 5, 7, 8, 16, 32, 64]}]).
+
+gen_integer() ->
+    oneof([gen_integer_bounded(), #t_integer{}]).
+
+gen_integer_bounded() ->
+    ?LET(A, integer(),
+         ?LET(B, integer(),
+              begin
+                  #t_integer{elements={min(A,B), max(A,B)}}
+              end)).
+
+gen_tuple(Depth) ->
+    ?SIZED(Size,
+           ?LET(Exact, oneof([true, false]),
+                ?LET(Elements, gen_tuple_elements(Size, Depth),
+                     begin
+                         #t_tuple{exact=Exact,
+                                  size=Size,
+                                  elements=Elements}
+                     end))).
+
+gen_tuple_elements(Size, Depth) ->
+    ?LET(Types, sized_list(rand:uniform(Size div 4 + 1), gen_element(Depth)),
+         maps:from_list([{rand:uniform(Size), T} || T <- Types])).
+
+gen_element(Depth) ->
+    ?LAZY(?SUCHTHAT(Type, type(Depth),
+                    case Type of
+                        any -> false;
+                        none -> false;
+                        _ -> true
+                    end)).
+
+sized_list(0, _Gen) -> [];
+sized_list(N, Gen) -> [Gen | sized_list(N - 1, Gen)].
+
+-endif.