diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/compiler/src/beam_call_types.erl | 2 | ||||
| -rw-r--r-- | lib/compiler/src/beam_ssa_type.erl | 142 | ||||
| -rw-r--r-- | lib/compiler/src/beam_types.erl | 850 | ||||
| -rw-r--r-- | lib/compiler/src/beam_types.hrl | 29 | ||||
| -rw-r--r-- | lib/compiler/src/beam_validator.erl | 12 | ||||
| -rw-r--r-- | lib/compiler/test/property_test/beam_types_prop.erl | 56 |
6 files changed, 751 insertions, 340 deletions
diff --git a/lib/compiler/src/beam_call_types.erl b/lib/compiler/src/beam_call_types.erl index 2aba6f7961..a94a7caa74 100644 --- a/lib/compiler/src/beam_call_types.erl +++ b/lib/compiler/src/beam_call_types.erl @@ -37,7 +37,7 @@ -spec types(Mod, Func, ArgTypes) -> {RetType, ArgTypes, CanSubtract} when Mod :: atom(), Func :: atom(), - ArgTypes :: [type()], + ArgTypes :: [normal_type()], RetType :: type(), CanSubtract :: boolean(). diff --git a/lib/compiler/src/beam_ssa_type.erl b/lib/compiler/src/beam_ssa_type.erl index 5e7b54a064..f4fc33bf4f 100644 --- a/lib/compiler/src/beam_ssa_type.erl +++ b/lib/compiler/src/beam_ssa_type.erl @@ -84,7 +84,8 @@ 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 => beam_types:join(maps:values(TM))}); + Type = beam_types:join(maps:values(TM)), + join_arg_types_1(Args, TMs, Ts#{ Arg => Type }); join_arg_types_1([Arg | Args], [_TM | TMs], Ts) -> join_arg_types_1(Args, TMs, Ts#{ Arg => any }); join_arg_types_1([], [], Ts) -> @@ -388,9 +389,9 @@ opt_call(#b_set{dst=Dst,args=[#b_local{}=Callee|Args]}=I0, D, Ts0, Ds0, Fdb0) -> %% Match contexts are treated as bitstrings when optimizing %% arguments, as we don't yet support removing the %% "bs_start_match3" instruction. - Types = [case get_type(Arg, Ts) of - #t_bs_context{} -> #t_bitstring{}; - Type -> Type + Types = [case raw_type(Arg, Ts) of + #t_bs_context{} -> #t_bitstring{}; + Type -> Type end || Arg <- Args], %% Update the argument types of *this exact call*, the types @@ -443,7 +444,7 @@ opt_make_fun(#b_set{op=make_fun, #{ Callee := #func_info{exported=false,arg_types=ArgTypes0}=Info } -> ArgCount = Callee#b_local.arity - length(FreeVars), - FVTypes = [get_type(FreeVar, Ts) || FreeVar <- FreeVars], + FVTypes = [raw_type(FreeVar, Ts) || FreeVar <- FreeVars], Types = duplicate(ArgCount, any) ++ FVTypes, CallId = {D#d.func_id, Dst}, @@ -486,8 +487,10 @@ simplify(#b_set{op={bif,'or'},args=Args}=I, Ts) -> I end; simplify(#b_set{op={bif,element},args=[#b_literal{val=Index},Tuple]}=I0, Ts) -> - case beam_types:get_tuple_size(get_type(Tuple, Ts)) of - {_,Size} when is_integer(Index), 1 =< Index, Index =< Size -> + case normalized_type(Tuple, Ts) of + #t_tuple{size=Size} when is_integer(Index), + 1 =< Index, + Index =< Size -> I = I0#b_set{op=get_tuple_element, args=[Tuple,#b_literal{val=Index-1}]}, simplify(I, Ts); @@ -495,28 +498,28 @@ simplify(#b_set{op={bif,element},args=[#b_literal{val=Index},Tuple]}=I0, Ts) -> eval_bif(I0, Ts) end; simplify(#b_set{op={bif,hd},args=[List]}=I, Ts) -> - case get_type(List, Ts) of + case normalized_type(List, Ts) of cons -> I#b_set{op=get_hd}; _ -> eval_bif(I, Ts) end; simplify(#b_set{op={bif,tl},args=[List]}=I, Ts) -> - case get_type(List, Ts) of + case normalized_type(List, Ts) of cons -> I#b_set{op=get_tl}; _ -> eval_bif(I, Ts) end; simplify(#b_set{op={bif,size},args=[Term]}=I, Ts) -> - case get_type(Term, Ts) of + case normalized_type(Term, Ts) of #t_tuple{} -> simplify(I#b_set{op={bif,tuple_size}}, Ts); _ -> eval_bif(I, Ts) end; simplify(#b_set{op={bif,tuple_size},args=[Term]}=I, Ts) -> - case get_type(Term, Ts) of + case normalized_type(Term, Ts) of #t_tuple{size=Size,exact=true} -> #b_literal{val=Size}; _ -> @@ -524,7 +527,7 @@ simplify(#b_set{op={bif,tuple_size},args=[Term]}=I, Ts) -> end; simplify(#b_set{op={bif,is_function},args=[Fun,#b_literal{val=Arity}]}=I, Ts) when is_integer(Arity), Arity >= 0 -> - case get_type(Fun, Ts) of + case normalized_type(Fun, Ts) of #t_fun{arity=any} -> I; #t_fun{arity=Arity} -> @@ -535,15 +538,15 @@ simplify(#b_set{op={bif,is_function},args=[Fun,#b_literal{val=Arity}]}=I, Ts) #b_literal{val=false} end; simplify(#b_set{op={bif,Op0},args=Args}=I, Ts) when Op0 =:= '=='; Op0 =:= '/=' -> - Types = get_types(Args, Ts), + Types = normalized_types(Args, Ts), EqEq0 = case {beam_types:meet(Types),beam_types:join(Types)} of - {none,any} -> true; - {#t_integer{},#t_integer{}} -> true; - {float,float} -> true; - {#t_bitstring{},_} -> true; - {#t_atom{},_} -> true; - {_,_} -> false - end, + {none,any} -> true; + {#t_integer{},#t_integer{}} -> true; + {float,float} -> true; + {#t_bitstring{},_} -> true; + {#t_atom{},_} -> true; + {_,_} -> false + end, EqEq = EqEq0 orelse any_non_numeric_argument(Args, Ts), case EqEq of true -> @@ -557,33 +560,35 @@ simplify(#b_set{op={bif,Op0},args=Args}=I, Ts) when Op0 =:= '=='; Op0 =:= '/=' - end; 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 beam_types:meet(T1, T2) of +simplify(#b_set{op={bif,'=:='},args=[LHS,RHS]}=I, Ts) -> + LType = raw_type(LHS, Ts), + RType = raw_type(RHS, Ts), + case beam_types:meet(LType, RType) of none -> #b_literal{val=false}; _ -> - case {beam_types:is_boolean_type(T1),T2} of + case {beam_types:is_boolean_type(LType), + beam_types:normalize(RType)} of {true,#t_atom{elements=[true]}} -> %% Bool =:= true ==> Bool - A1; + LHS; {true,#t_atom{elements=[false]}} -> %% Bool =:= false ==> not Bool %% %% This will be further optimized to eliminate the %% 'not', swapping the success and failure - %% branches in the br instruction. If A1 comes + %% branches in the br instruction. If LHS comes %% from a type test (such as is_atom/1) or a %% comparison operator (such as >=) that can be %% translated to test instruction, this %% optimization will eliminate one instruction. - simplify(I#b_set{op={bif,'not'},args=[A1]}, Ts); + simplify(I#b_set{op={bif,'not'},args=[LHS]}, Ts); {_,_} -> eval_bif(I, Ts) end end; simplify(#b_set{op={bif,Op},args=Args}=I, Ts) -> - Types = get_types(Args, Ts), + Types = normalized_types(Args, Ts), case is_float_op(Op, Types) of false -> eval_bif(I, Ts); @@ -592,7 +597,7 @@ simplify(#b_set{op={bif,Op},args=Args}=I, Ts) -> eval_bif(beam_ssa:add_anno(float_op, AnnoArgs, I), Ts) end; simplify(#b_set{op=get_tuple_element,args=[Tuple,#b_literal{val=N}]}=I, Ts) -> - case get_type(Tuple, Ts) of + case normalized_type(Tuple, Ts) of #t_tuple{size=Size,elements=Es} when Size > N -> ElemType = beam_types:get_element_type(N + 1, Es), case beam_types:get_singleton_value(ElemType) of @@ -605,7 +610,7 @@ simplify(#b_set{op=get_tuple_element,args=[Tuple,#b_literal{val=N}]}=I, Ts) -> I end; simplify(#b_set{op=is_nonempty_list,args=[Src]}=I, Ts) -> - case get_type(Src, Ts) of + case normalized_type(Src, Ts) of any -> I; list -> I; cons -> #b_literal{val=true}; @@ -613,7 +618,7 @@ simplify(#b_set{op=is_nonempty_list,args=[Src]}=I, Ts) -> end; simplify(#b_set{op=is_tagged_tuple, args=[Src,#b_literal{val=Size},#b_literal{}=Tag]}=I, Ts) -> - simplify_is_record(I, get_type(Src, Ts), Size, Tag, Ts); + simplify_is_record(I, normalized_type(Src, Ts), Size, Tag, Ts); simplify(#b_set{op=put_list,args=[#b_literal{val=H}, #b_literal{val=T}]}, _Ts) -> #b_literal{val=[H|T]}; @@ -631,7 +636,7 @@ simplify(I, _Ts) -> I. any_non_numeric_argument([#b_literal{val=Lit}|_], _Ts) -> is_non_numeric(Lit); any_non_numeric_argument([#b_var{}=V|T], Ts) -> - is_non_numeric_type(get_type(V, Ts)) orelse any_non_numeric_argument(T, Ts); + is_non_numeric_type(raw_type(V, Ts)) orelse any_non_numeric_argument(T, Ts); any_non_numeric_argument([], _Ts) -> false. is_non_numeric([H|T]) -> @@ -649,7 +654,7 @@ is_non_numeric(_) -> true. is_non_numeric_tuple(Tuple, El) when El >= 1 -> is_non_numeric(element(El, Tuple)) andalso - is_non_numeric_tuple(Tuple, El-1); + is_non_numeric_tuple(Tuple, El-1); is_non_numeric_tuple(_Tuple, 0) -> true. is_non_numeric_type(#t_atom{}) -> true; @@ -676,9 +681,11 @@ make_literal_list([_|_], _) -> make_literal_list([], Acc) -> reverse(Acc). -is_safe_bool_op(Args, Ts) -> - [T1,T2] = get_types(Args, Ts), - beam_types:is_boolean_type(T1) andalso beam_types:is_boolean_type(T2). +is_safe_bool_op([LHS, RHS], Ts) -> + LType = raw_type(LHS, Ts), + RType = raw_type(RHS, Ts), + beam_types:is_boolean_type(LType) andalso + beam_types:is_boolean_type(RType). all_same([{H,_}|T]) -> all(fun({E,_}) -> E =:= H end, T). @@ -691,7 +698,7 @@ eval_bif(#b_set{op={bif,Bif},args=Args}=I, Ts) -> true -> case make_literal_list(Args) of none -> - case get_types(Args, Ts) of + case normalized_types(Args, Ts) of [any] -> I; [Type] -> @@ -724,8 +731,7 @@ simplify_arg(#b_var{}=Arg0, Sub, Ts) -> #b_literal{}=LitArg -> LitArg; #b_var{}=Arg -> - Type = get_type(Arg, Ts), - case beam_types:get_singleton_value(Type) of + case beam_types:get_singleton_value(raw_type(Arg, Ts)) of {ok, Val} -> #b_literal{val=Val}; error -> Arg end @@ -766,7 +772,7 @@ opt_terminator(#b_br{bool=#b_var{}}=Br, Ts, Ds) -> opt_terminator(#b_switch{arg=#b_literal{}}=Sw, _Ts, _Ds) -> beam_ssa:normalize(Sw); opt_terminator(#b_switch{arg=#b_var{}=V}=Sw, Ts, Ds) -> - case get_type(V, Ts) of + case normalized_type(V, Ts) of any -> beam_ssa:normalize(Sw); Type -> @@ -796,7 +802,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 beam_types:meet(get_type(Arg, Ts), Type) of + case beam_types:meet(raw_type(Arg, Ts), Type) of none -> %% Different types. This value can never match. prune_switch_list(T, Fail, Type, Ts); @@ -860,7 +866,7 @@ update_successors(#b_ret{arg=Arg}=Last, Ts, D0) -> %% type. D0; #{} -> - RetType = beam_types:join([get_type(Arg, Ts) | D0#d.ret_type]), + RetType = beam_types:join([raw_type(Arg, Ts) | D0#d.ret_type]), D0#d{ret_type=[RetType]} end, {Last, D}. @@ -881,13 +887,13 @@ update_switch([], _V, _UsedOnce, _Ts, Acc, D) -> {Acc, D}. subtract_sw_list(V, List, Ts) -> - case sub_sw_list_1(get_type(V, Ts), List, Ts) of + case sub_sw_list_1(raw_type(V, Ts), List, Ts) of none -> none; Type -> Ts#{ V := Type } end. sub_sw_list_1(Type, [{Val,_}|T], Ts) -> - ValType = get_type(Val, Ts), + ValType = raw_type(Val, Ts), sub_sw_list_1(beam_types:subtract(Type, ValType), T, Ts); sub_sw_list_1(Type, [], _Ts) -> Type. @@ -911,10 +917,11 @@ update_types(#b_set{op=Op,dst=Dst,args=Args}, Ts, Ds) -> Ts#{Dst=>T}. type(phi, Args, Ts, _Ds) -> - Types = [get_type(A, Ts) || {A,_} <- Args], + Types = [raw_type(A, Ts) || {A,_} <- Args], beam_types:join(Types); type({bif,Bif}, Args, Ts, _Ds) -> - {RetType, _, _} = beam_call_types:types(erlang, Bif, get_types(Args, Ts)), + ArgTypes = normalized_types(Args, Ts), + {RetType, _, _} = beam_call_types:types(erlang, Bif, ArgTypes), RetType; type(bs_init, _Args, _Ts, _Ds) -> #t_bitstring{}; @@ -927,10 +934,11 @@ type(bs_get_tail, _Args, _Ts, _Ds) -> #t_bitstring{}; type(call, [#b_remote{mod=#b_literal{val=Mod}, name=#b_literal{val=Name}}|Args], Ts, _Ds) -> - {RetType, _, _} = beam_call_types:types(Mod, Name, get_types(Args, Ts)), + ArgTypes = normalized_types(Args, Ts), + {RetType, _, _} = beam_call_types:types(Mod, Name, ArgTypes), RetType; type(get_tuple_element, [Tuple, Offset], Ts, _Ds) -> - #t_tuple{size=Size,elements=Es} = get_type(Tuple, Ts), + #t_tuple{size=Size,elements=Es} = normalized_type(Tuple, Ts), #b_literal{val=N} = Offset, true = Size > N, %Assertion. beam_types:get_element_type(N + 1, Es); @@ -946,7 +954,7 @@ type(put_list, _Args, _Ts, _Ds) -> cons; type(put_tuple, Args, Ts, _Ds) -> {Es, _} = foldl(fun(Arg, {Es0, Index}) -> - Type = get_type(Arg, Ts), + Type = raw_type(Arg, Ts), Es = beam_types:set_element_type(Index, Type, Es0), {Es, Index + 1} end, {#{}, 1}, Args), @@ -954,7 +962,7 @@ type(put_tuple, Args, Ts, _Ds) -> type(succeeded, [#b_var{}=Src], Ts, Ds) -> case maps:get(Src, Ds) of #b_set{op={bif,Bif},args=BifArgs} -> - Types = get_types(BifArgs, Ts), + Types = normalized_types(BifArgs, Ts), case {Bif,Types} of {BoolOp,[T1,T2]} when BoolOp =:= 'and'; BoolOp =:= 'or' -> BothBool = beam_types:is_boolean_type(T1) andalso @@ -1151,7 +1159,7 @@ simplify_is_record(I, #t_tuple{exact=Exact, {ok, _} -> no; error -> %% Is it at all possible for the tag to match? - case beam_types:meet(get_type(RecTag, Ts), TagType) of + case beam_types:meet(raw_type(RecTag, Ts), TagType) of none -> no; _ -> maybe end @@ -1181,7 +1189,7 @@ simplify_switch_bool(#b_switch{arg=B,fail=Fail,list=List0}, Ts, Ds) -> simplify_not(#b_br{bool=#b_var{}=V,succ=Succ,fail=Fail}=Br0, Ts, Ds) -> case Ds of #{V:=#b_set{op={bif,'not'},args=[Bool]}} -> - case beam_types:is_boolean_type(get_type(Bool, Ts)) of + case beam_types:is_boolean_type(raw_type(Bool, Ts)) of true -> Br = Br0#b_br{bool=Bool,succ=Fail,fail=Succ}, beam_ssa:normalize(Br); @@ -1249,16 +1257,18 @@ used_once_last_uses([V|Vs], L, Uses) -> end; used_once_last_uses([], _, Uses) -> Uses. +normalized_types(Values, Ts) -> + [normalized_type(Val, Ts) || Val <- Values]. + +normalized_type(V, Ts) -> + beam_types:normalize(raw_type(V, Ts)). -get_types(Values, Ts) -> - [get_type(Val, Ts) || Val <- Values]. --spec get_type(beam_ssa:value(), type_db()) -> type(). +-spec raw_type(beam_ssa:value(), type_db()) -> type(). -get_type(#b_var{}=V, Ts) -> - #{V:=T} = Ts, - T; -get_type(#b_literal{val=Val}, _Ts) -> - beam_types:make_type_from_value(Val). +raw_type(#b_literal{val=Value}, _Ts) -> + beam_types:make_type_from_value(Value); +raw_type(V, Ts) -> + map_get(V, Ts). %% infer_types(Var, Types, #d{}) -> {SuccTypes,FailTypes} %% Looking at the expression that defines the variable Var, infer @@ -1332,14 +1342,14 @@ infer_types_switch(V, Lit, Ts, #d{ds=Ds}) -> infer_eq_type({bif,'=:='}, [#b_var{}=Src,#b_literal{}=Lit], Ts, Ds) -> Def = maps:get(Src, Ds), - Type = get_type(Lit, Ts), + Type = raw_type(Lit, Ts), [{Src,Type} | infer_eq_lit(Def, Lit)]; infer_eq_type({bif,'=:='}, [#b_var{}=Arg0,#b_var{}=Arg1], Ts, _Ds) -> %% As an example, assume that L1 is known to be 'list', and L2 is %% known to be 'cons'. Then if 'L1 =:= L2' evaluates to 'true', it can %% be inferred that L1 is 'cons' (the meet of 'cons' and 'list'). - Type0 = get_type(Arg0, Ts), - Type1 = get_type(Arg1, Ts), + Type0 = raw_type(Arg0, Ts), + Type1 = raw_type(Arg1, Ts), Type = beam_types:meet(Type0, Type1), [{V,MeetType} || {V,OrigType,MeetType} <- @@ -1355,7 +1365,7 @@ infer_eq_lit(#b_set{op=get_tuple_element, args=[#b_var{}=Tuple,#b_literal{val=N}]}, #b_literal{}=Lit) -> Index = N + 1, - Es = beam_types:set_element_type(Index, get_type(Lit, #{}), #{}), + Es = beam_types:set_element_type(Index, raw_type(Lit, #{}), #{}), [{Tuple,#t_tuple{size=Index,elements=Es}}]; infer_eq_lit(_, _) -> []. @@ -1368,7 +1378,7 @@ infer_type(succeeded, [#b_var{}=Src], Ts, Ds) -> %% not branching on 'succeeded'. infer_type(is_tagged_tuple, [#b_var{}=Src,#b_literal{val=Size}, #b_literal{}=Tag], _Ts, _Ds) -> - Es = beam_types:set_element_type(1, get_type(Tag, #{}), #{}), + Es = beam_types:set_element_type(1, raw_type(Tag, #{}), #{}), T = {Src,#t_tuple{exact=true,size=Size,elements=Es}}, {[T], [T]}; infer_type(is_nonempty_list, [#b_var{}=Src], _Ts, _Ds) -> @@ -1408,7 +1418,7 @@ infer_type(_Op, _Args, _Ts, _Ds) -> {[], []}. infer_success_type({bif,Op}, Args, Ts, _Ds) -> - ArgTypes = get_types(Args, Ts), + ArgTypes = normalized_types(Args, Ts), {_, PosTypes0, CanSubtract} = beam_call_types:types(erlang, Op, ArgTypes), PosTypes = [T || {#b_var{},_}=T <- zip(Args, PosTypes0)], diff --git a/lib/compiler/src/beam_types.erl b/lib/compiler/src/beam_types.erl index 4f8ba0ada5..821ccd31bb 100644 --- a/lib/compiler/src/beam_types.erl +++ b/lib/compiler/src/beam_types.erl @@ -22,14 +22,14 @@ -include("beam_types.hrl"). --import(lists, [foldl/3]). +-import(lists, [foldl/3, reverse/1, reverse/2]). -export([meet/1, meet/2, join/1, join/2, subtract/2]). -export([get_singleton_value/1, - get_tuple_size/1, is_singleton_type/1, - is_boolean_type/1]). + is_boolean_type/1, + normalize/1]). -export([get_element_type/2, set_element_type/3]). @@ -38,223 +38,276 @@ -export([make_atom/1, make_boolean/0, make_integer/1, - make_integer/2, - make_tuple/2, - make_tuple/3]). + make_integer/2]). -%% Return the "join" of Type1 and Type2. The join is a more general -%% type than Type1 and Type2. For example: +-define(IS_LIST_TYPE(N), + N =:= list orelse + N =:= cons orelse + N =:= nil). + +-define(IS_NUMBER_TYPE(N), + N =:= number orelse + N =:= float orelse + is_record(N, t_integer)). + +-define(TUPLE_SET_LIMIT, 20). + +%% Folds meet/2 over a list. + +-spec meet([type()]) -> type(). + +meet([T1, T2 | Ts]) -> + meet([meet(T1, T2) | Ts]); +meet([T]) -> T. + +%% Return the "meet" of Type1 and Type2, which is more general than Type1 and +%% Type2. This is identical to glb/2 but can operate on and produce unions. %% -%% join(#t_integer{elements=any}, #t_integer=elements={0,3}}) -> -%% #t_integer{} +%% A = #t_union{list=nil, number=[number], other=[#t_map{}]} +%% B = #t_union{number=[#t_integer{}], other=[#t_map{}]} %% -%% The join for two different types result in 'any', which is -%% the top element for our type lattice: +%% meet(A, B) -> +%% #t_union{number=[#t_integer{}], other=[#t_map{}]} %% -%% join(#t_integer{}, #t_map{}) -> any +%% The meet of two different types result in 'none', which is the bottom +%% element for our type lattice: +%% +%% meet(#t_integer{}, #t_map{}) -> none --spec join(type(), type()) -> type(). +-spec meet(type(), type()) -> type(). -join(T, T) -> +meet(T, T) -> verified_type(T); -join(none, T) -> +meet(any, T) -> verified_type(T); -join(T, none) -> +meet(T, any) -> 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} +meet(#t_union{}=A, B) -> + meet_unions(A, B); +meet(A, #t_union{}=B) -> + meet_unions(B, A); +meet(A, B) -> + glb(A, B). + +meet_unions(#t_union{atom=AtomA,list=ListA,number=NumberA, + tuple_set=TSetA,other=OtherA}, + #t_union{atom=AtomB,list=ListB,number=NumberB, + tuple_set=TSetB,other=OtherB}) -> + Union = #t_union{atom=glb(AtomA, AtomB), + list=glb(ListA, ListB), + number=glb(NumberA, NumberB), + tuple_set=meet_tuple_sets(TSetA, TSetB), + other=glb(OtherA, OtherB)}, + shrink_union(Union); +meet_unions(#t_union{atom=AtomA}, #t_atom{}=B) -> + case glb(AtomA, B) of + none -> none; + Atom -> Atom end; -join(#t_atom{elements=any}=T, #t_atom{elements=[_|_]}) -> T; -join(#t_atom{elements=[_|_]}, #t_atom{elements=any}=T) -> T; -join(#t_bitstring{unit=U1}, #t_bitstring{unit=U2}) -> - #t_bitstring{unit=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_bs_context{slots=SlotsA,valid=ValidA}, - #t_bs_context{slots=SlotsB,valid=ValidB}) -> - #t_bs_context{slots=min(SlotsA, SlotsB), - valid=ValidA band ValidB}; -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. +meet_unions(#t_union{number=NumberA}, B) when ?IS_NUMBER_TYPE(B) -> + case glb(NumberA, B) of + none -> none; + Number -> Number + end; +meet_unions(#t_union{list=ListA}, B) when ?IS_LIST_TYPE(B) -> + case glb(ListA, B) of + none -> none; + List -> List + end; +meet_unions(#t_union{tuple_set=Tuples}, #t_tuple{}=B) -> + Set = meet_tuple_sets(Tuples, new_tuple_set(B)), + shrink_union(#t_union{tuple_set=Set}); +meet_unions(#t_union{other=OtherA}, OtherB) -> + case glb(OtherA, OtherB) of + none -> none; + Other -> Other + end. -join_tuple_elements(MinSize, EsA, EsB) -> - Es0 = join_elements(EsA, EsB), - maps:filter(fun(Index, _Type) -> Index =< MinSize end, Es0). +meet_tuple_sets(none, _) -> + none; +meet_tuple_sets(_, none) -> + none; +meet_tuple_sets(#t_tuple{}=A, #t_tuple{}=B) -> + new_tuple_set(glb(A, B)); +meet_tuple_sets(#t_tuple{}=Tuple, Records) -> + mts_tuple(Records, Tuple, []); +meet_tuple_sets(Records, #t_tuple{}=Tuple) -> + meet_tuple_sets(Tuple, Records); +meet_tuple_sets(RecordsA, RecordsB) -> + mts_records(RecordsA, RecordsB). + +mts_tuple([{Key, Type} | Records], Tuple, Acc) -> + case glb(Type, Tuple) of + none -> mts_tuple(Records, Tuple, Acc); + T -> mts_tuple(Records, Tuple, [{Key, T} | Acc]) + end; +mts_tuple([], _Tuple, [_|_]=Acc) -> + reverse(Acc); +mts_tuple([], _Tuple, []) -> + none. -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, #{}). +mts_records(RecordsA, RecordsB) -> + mts_records(RecordsA, RecordsB, []). -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) +mts_records([{Key, A} | RsA], [{Key, B} | RsB], Acc) -> + case glb(A, B) of + none -> mts_records(RsA, RsB, Acc); + T -> mts_records(RsA, RsB, [{Key, T} | Acc]) end; -join_elements_1([], _Es1, _Es2, Acc) -> - Acc. +mts_records([{KeyA, _} | _ ]=RsA, [{KeyB, _} | RsB], Acc) when KeyA > KeyB -> + mts_records(RsA, RsB, Acc); +mts_records([{KeyA, _} | RsA], [{KeyB, _} | _] = RsB, Acc) when KeyA < KeyB -> + mts_records(RsA, RsB, Acc); +mts_records(_RsA, [], [_|_]=Acc) -> + reverse(Acc); +mts_records([], _RsB, [_|_]=Acc) -> + reverse(Acc); +mts_records(_RsA, _RsB, []) -> + none. -gcd(A, B) -> - case A rem B of - 0 -> B; - X -> gcd(B, X) - end. +%% Folds join/2 over a list. -%% Joins all the given types into a single type. -spec join([type()]) -> type(). -join([T1,T2|Ts]) -> - join([join(T1, T2)|Ts]); +join([T1, T2| Ts]) -> + join([join(T1, T2) | Ts]); join([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: +%% Return the "join" of Type1 and Type2, which is more general than Type1 and +%% Type2. This is identical to lub/2 but can operate on and produce unions. %% -%% meet(#t_integer{}, #t_map{}) -> none +%% join(#t_integer{}, #t_map{}) -> #t_union{number=[#t_integer{}], +%% other=[#t_map{}]} --spec meet(type(), type()) -> type(). +-spec join(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} +join(T, T) -> T; +join(_T, any) -> any; +join(any, _T) -> any; +join(T, none) -> T; +join(none, T) -> T; + +join(#t_union{}=A, B) -> + join_unions(A, B); +join(A, #t_union{}=B) -> + join_unions(B, A); + +%% Union creation... +join(#t_atom{}=A, #t_atom{}=B) -> + lub(A, B); +join(#t_atom{}=A, B) when ?IS_LIST_TYPE(B) -> + #t_union{atom=A,list=B}; +join(#t_atom{}=A, B) when ?IS_NUMBER_TYPE(B) -> + #t_union{atom=A,number=B}; +join(#t_atom{}=A, #t_tuple{}=B) -> + #t_union{atom=A,tuple_set=new_tuple_set(B)}; +join(#t_atom{}=A, B) -> + #t_union{atom=A,other=B}; +join(A, #t_atom{}=B) -> + join(B, A); + +join(A, B) when ?IS_LIST_TYPE(A), ?IS_LIST_TYPE(B) -> + lub(A, B); +join(A, B) when ?IS_LIST_TYPE(A), ?IS_NUMBER_TYPE(B) -> + #t_union{list=A,number=B}; +join(A, #t_tuple{}=B) when ?IS_LIST_TYPE(A) -> + #t_union{list=A,tuple_set=new_tuple_set(B)}; +join(A, B) when ?IS_LIST_TYPE(A) -> + #t_union{list=A,other=B}; +join(A, B) when ?IS_LIST_TYPE(B) -> + join(B, A); + +join(A, B) when ?IS_NUMBER_TYPE(A), ?IS_NUMBER_TYPE(B) -> + lub(A, B); +join(A, #t_tuple{}=B) when ?IS_NUMBER_TYPE(A) -> + #t_union{number=A,tuple_set=new_tuple_set(B)}; +join(A, B) when ?IS_NUMBER_TYPE(A) -> + #t_union{number=A,other=B}; +join(A, B) when ?IS_NUMBER_TYPE(B) -> + join(B, A); + +join(#t_tuple{}=A, #t_tuple{}=B) -> + case {record_key(A), record_key(B)} of + {Same, Same} -> + lub(A, B); + {none, _Key} -> + lub(A, B); + {_Key, none} -> + lub(A, B); + {KeyA, KeyB} when KeyA < KeyB -> + #t_union{tuple_set=[{KeyA, A}, {KeyB, B}]}; + {KeyA, KeyB} when KeyA > KeyB -> + #t_union{tuple_set=[{KeyB, B}, {KeyA, A}]} end; -meet(#t_atom{elements=[_|_]}=T, #t_atom{elements=any}) -> - T; -meet(#t_atom{elements=any}, #t_atom{elements=[_|_]}=T) -> - T; -meet(#t_bs_context{slots=SlotCountA,valid=ValidSlotsA}, - #t_bs_context{slots=SlotCountB,valid=ValidSlotsB}) -> - CommonSlotMask = (1 bsl min(SlotCountA, SlotCountB)) - 1, - CommonSlotsA = ValidSlotsA band CommonSlotMask, - CommonSlotsB = ValidSlotsB band CommonSlotMask, - if - CommonSlotsA =:= CommonSlotsB -> - #t_bs_context{slots=max(SlotCountA, SlotCountB), - valid=ValidSlotsA bor ValidSlotsB}; - CommonSlotsA =/= CommonSlotsB -> - none - end; -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, MinA =< MaxB; - MinB >= MinA, MinB =< MaxA -> - true = MinA =< MaxA andalso MinB =< MaxB, %Assertion. - #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(#t_bitstring{unit=U1}, #t_bitstring{unit=U2}) -> - #t_bitstring{unit=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} +join(#t_tuple{}=A, B) -> + %% All other combinations have been tried already, so B must be 'other' + #t_union{tuple_set=new_tuple_set(A),other=B}; +join(A, #t_tuple{}=B) -> + join(B, A); + +join(A, B) -> + lub(A, B). + +join_unions(#t_union{atom=AtomA,list=ListA,number=NumberA, + tuple_set=TSetA,other=OtherA}, + #t_union{atom=AtomB,list=ListB,number=NumberB, + tuple_set=TSetB,other=OtherB}) -> + Union = #t_union{atom=lub(AtomA, AtomB), + list=lub(ListA, ListB), + number=lub(NumberA, NumberB), + tuple_set=join_tuple_sets(TSetA, TSetB), + other=lub(OtherA, OtherB)}, + shrink_union(Union); +join_unions(#t_union{atom=AtomA}=A, #t_atom{}=B) -> + A#t_union{atom=lub(AtomA, B)}; +join_unions(#t_union{list=ListA}=A, B) when ?IS_LIST_TYPE(B) -> + A#t_union{list=lub(ListA, B)}; +join_unions(#t_union{number=NumberA}=A, B) when ?IS_NUMBER_TYPE(B) -> + A#t_union{number=lub(NumberA, B)}; +join_unions(#t_union{tuple_set=TSetA}=A, #t_tuple{}=B) -> + Set = join_tuple_sets(TSetA, new_tuple_set(B)), + shrink_union(A#t_union{tuple_set=Set}); +join_unions(#t_union{other=OtherA}=A, B) -> + case lub(OtherA, B) of + any -> any; + T -> A#t_union{other=T} 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) -> +join_tuple_sets(A, none) -> + A; +join_tuple_sets(none, B) -> + B; +join_tuple_sets(#t_tuple{}=A, #t_tuple{}=B) -> + lub(A, B); +join_tuple_sets(#t_tuple{}=Tuple, Records) -> + jts_tuple(Records, Tuple); +join_tuple_sets(Records, #t_tuple{}=Tuple) -> + join_tuple_sets(Tuple, Records); +join_tuple_sets(RecordsA, RecordsB) -> + jts_records(RecordsA, RecordsB). + +jts_tuple([{_Key, Tuple} | Records], Acc) -> + jts_tuple(Records, lub(Tuple, Acc)); +jts_tuple([], Acc) -> Acc. -%% 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. +jts_records(RsA, RsB) -> + jts_records(RsA, RsB, 0, []). + +jts_records(RsA, RsB, N, Acc) when N > ?TUPLE_SET_LIMIT -> + A = normalize_tuple_set(RsA, none), + B = normalize_tuple_set(RsB, A), + #t_tuple{} = normalize_tuple_set(Acc, B); +jts_records([{Key, A} | RsA], [{Key, B} | RsB], N, Acc) -> + jts_records(RsA, RsB, N + 1, [{Key, lub(A, B)} | Acc]); +jts_records([{KeyA, _} | _]=RsA, [{KeyB, B} | RsB], N, Acc) when KeyA > KeyB -> + jts_records(RsA, RsB, N + 1, [{KeyB, B} | Acc]); +jts_records([{KeyA, A} | RsA], [{KeyB, _} | _] = RsB, N, Acc) when KeyA < KeyB -> + jts_records(RsA, RsB, N + 1, [{KeyA, A} | Acc]); +jts_records([], RsB, _N, Acc) -> + reverse(Acc, RsB); +jts_records(RsA, [], _N, Acc) -> + reverse(Acc, RsA). %% Subtract Type2 from Type1. Example: %% subtract(list, cons) -> nil @@ -270,38 +323,28 @@ subtract(number, float) -> #t_integer{}; subtract(number, #t_integer{elements=any}) -> float; subtract(list, cons) -> nil; subtract(list, nil) -> cons; -subtract(T, _) -> T. -%% Verifies that the given type is well-formed. - --spec verified_type(T) -> T when - T :: type(). +subtract(#t_union{atom=Atom}=A, #t_atom{}=B)-> + shrink_union(A#t_union{atom=subtract(Atom, B)}); +subtract(#t_union{number=Number}=A, B) when ?IS_NUMBER_TYPE(B) -> + shrink_union(A#t_union{number=subtract(Number, B)}); +subtract(#t_union{list=List}=A, B) when ?IS_LIST_TYPE(B) -> + shrink_union(A#t_union{list=subtract(List, B)}); +subtract(#t_union{tuple_set=[_|_]=Records0}=A, #t_tuple{}=B) -> + %% Filter out all records that are strictly more specific than B. + NewSet = case [{Key, T} || {Key, T} <- Records0, meet(T, B) =/= T] of + [_|_]=Records -> Records; + [] -> none + end, + shrink_union(A#t_union{tuple_set=NewSet}); +subtract(#t_union{tuple_set=#t_tuple{}=Tuple}=A, #t_tuple{}=B) -> + %% Exclude Tuple if it's strictly more specific than B. + case meet(Tuple, B) of + Tuple -> shrink_union(A#t_union{tuple_set=none}); + _ -> A + end; -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(#t_bitstring{unit=U}=T) when is_integer(U), U >= 1 -> T; -verified_type(#t_bs_context{}=T) -> 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(#t_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. +subtract(T, _) -> T. %%% %%% Type operators @@ -319,23 +362,15 @@ get_singleton_value(nil) -> get_singleton_value(_) -> error. --spec get_tuple_size(Type) -> Result when - Type :: type(), - Result :: none | {at_least, Size} | {exact, Size}, - Size :: non_neg_integer(). -get_tuple_size(#t_tuple{size=Size,exact=false}) -> - {at_least,Size}; -get_tuple_size(#t_tuple{size=Size,exact=true}) -> - {exact,Size}; -get_tuple_size(_) -> - none. - -spec is_boolean_type(type()) -> boolean(). is_boolean_type(#t_atom{elements=[F,T]}) -> F =:= false andalso T =:= true; is_boolean_type(#t_atom{elements=[B]}) -> is_boolean(B); -is_boolean_type(_) -> false. +is_boolean_type(#t_union{}=T) -> + is_boolean_type(normalize(T)); +is_boolean_type(_) -> + false. -spec is_singleton_type(type()) -> boolean(). is_singleton_type(Type) -> @@ -361,6 +396,23 @@ get_element_type(Index, Es) -> #{} -> any end. +-spec normalize(type()) -> normal_type(). +normalize(#t_union{atom=Atom,list=List,number=Number, + tuple_set=Tuples,other=Other}) -> + A = lub(Atom, List), + B = lub(A, Number), + C = lub(B, Other), + normalize_tuple_set(Tuples, C); +normalize(T) -> + verified_normal_type(T). + +normalize_tuple_set([{_, A} | Records], B) -> + normalize_tuple_set(Records, lub(A, B)); +normalize_tuple_set([], B) -> + B; +normalize_tuple_set(A, B) -> + lub(A, B). + %%% %%% Type constructors %%% @@ -408,17 +460,319 @@ make_integer(Int) when is_integer(Int) -> make_integer(Min, Max) when is_integer(Min), is_integer(Max), Min =< Max -> #t_integer{elements={Min,Max}}. --spec make_tuple(Size, Exact) -> type() when - Size :: non_neg_integer(), - Exact :: boolean(). -make_tuple(Size, Exact) -> - make_tuple(Size, Exact, #{}). - --spec make_tuple(Size, Exact, Elements) -> type() when - Size :: non_neg_integer(), - Exact :: boolean(), - Elements :: #{ non_neg_integer() => type() }. -make_tuple(Size, Exact, Elements) -> - #t_tuple{size=Size, - exact=Exact, - elements=Elements}. +%%% +%%% Helpers +%%% + +%% Return the greatest lower bound of the types Type1 and Type2. The GLB is a +%% more specific type than Type1 and Type2, and is always a normal type. +%% +%% glb(#t_integer{elements=any}, #t_integer{elements={0,3}}) -> +%% #t_integer{elements={0,3}} +%% +%% The GLB of two different types result in 'none', which is the bottom +%% element for our type lattice: +%% +%% glb(#t_integer{}, #t_map{}) -> none + +-spec glb(normal_type(), normal_type()) -> normal_type(). + +glb(T, T) -> + verified_normal_type(T); +glb(any, T) -> + verified_normal_type(T); +glb(T, any) -> + verified_normal_type(T); +glb(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) -> + case ordsets:intersection(Set1, Set2) of + [] -> + none; + [_|_]=Set -> + #t_atom{elements=Set} + end; +glb(#t_atom{elements=[_|_]}=T, #t_atom{elements=any}) -> + T; +glb(#t_atom{elements=any}, #t_atom{elements=[_|_]}=T) -> + T; +glb(#t_bs_context{slots=SlotCountA,valid=ValidSlotsA}, + #t_bs_context{slots=SlotCountB,valid=ValidSlotsB}) -> + CommonSlotMask = (1 bsl min(SlotCountA, SlotCountB)) - 1, + CommonSlotsA = ValidSlotsA band CommonSlotMask, + CommonSlotsB = ValidSlotsB band CommonSlotMask, + if + CommonSlotsA =:= CommonSlotsB -> + #t_bs_context{slots=max(SlotCountA, SlotCountB), + valid=ValidSlotsA bor ValidSlotsB}; + CommonSlotsA =/= CommonSlotsB -> + none + end; +glb(#t_fun{arity=any}, #t_fun{}=T) -> + T; +glb(#t_fun{}=T, #t_fun{arity=any}) -> + T; +glb(#t_integer{elements={_,_}}=T, #t_integer{elements=any}) -> + T; +glb(#t_integer{elements=any}, #t_integer{elements={_,_}}=T) -> + T; +glb(#t_integer{elements={MinA,MaxA}}, #t_integer{elements={MinB,MaxB}}) + when MinA >= MinB, MinA =< MaxB; + MinB >= MinA, MinB =< MaxA -> + true = MinA =< MaxA andalso MinB =< MaxB, %Assertion. + #t_integer{elements={max(MinA, MinB),min(MaxA, MaxB)}}; +glb(#t_integer{}=T, number) -> T; +glb(float=T, number) -> T; +glb(number, #t_integer{}=T) -> T; +glb(number, float=T) -> T; +glb(list, cons) -> cons; +glb(list, nil) -> nil; +glb(cons, list) -> cons; +glb(nil, list) -> nil; +glb(#t_tuple{}=T1, #t_tuple{}=T2) -> + glb_tuples(T1, T2); +glb(#t_bitstring{unit=U1}, #t_bitstring{unit=U2}) -> + #t_bitstring{unit=U1 * U2 div gcd(U1, U2)}; +glb(_, _) -> + %% Inconsistent types. There will be an exception at runtime. + none. + +glb_tuples(#t_tuple{size=Sz1,exact=true}, + #t_tuple{size=Sz2,exact=true}) when Sz1 =/= Sz2 -> + none; +glb_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 glb_elements(Es1, Es2) of + none -> + none; + Es -> + #t_tuple{size=Size,exact=Exact,elements=Es} + end. + +glb_elements(Es1, Es2) -> + Keys = maps:keys(Es1) ++ maps:keys(Es2), + glb_elements_1(Keys, Es1, Es2, #{}). + +glb_elements_1([Key | Keys], Es1, Es2, Acc) -> + case {Es1, Es2} of + {#{ Key := Type1 }, #{ Key := Type2 }} -> + %% Note the use of meet/2; elements don't need to be normal types. + case meet(Type1, Type2) of + none -> none; + Type -> glb_elements_1(Keys, Es1, Es2, Acc#{ Key => Type }) + end; + {#{ Key := Type1 }, _} -> + glb_elements_1(Keys, Es1, Es2, Acc#{ Key => Type1 }); + {_, #{ Key := Type2 }} -> + glb_elements_1(Keys, Es1, Es2, Acc#{ Key => Type2 }) + end; +glb_elements_1([], _Es1, _Es2, Acc) -> + Acc. + +%% Return the least upper bound of the types Type1 and Type2. The LUB is a more +%% general type than Type1 and Type2, and is always a normal type. +%% +%% For example: +%% +%% lub(#t_integer{elements=any}, #t_integer=elements={0,3}}) -> +%% #t_integer{} +%% +%% The LUB for two different types result in 'any' (not a union type!), which +%% is the top element for our type lattice: +%% +%% lub(#t_integer{}, #t_map{}) -> any + +-spec lub(normal_type(), normal_type()) -> normal_type(). + +lub(T, T) -> + verified_normal_type(T); +lub(none, T) -> + verified_normal_type(T); +lub(T, none) -> + verified_normal_type(T); +lub(any, _) -> + any; +lub(_, any) -> + any; +lub(#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; +lub(#t_atom{elements=any}=T, #t_atom{elements=[_|_]}) -> T; +lub(#t_atom{elements=[_|_]}, #t_atom{elements=any}=T) -> T; +lub(#t_bitstring{unit=U1}, #t_bitstring{unit=U2}) -> + #t_bitstring{unit=gcd(U1, U2)}; +lub(#t_fun{}, #t_fun{}) -> + #t_fun{}; +lub(#t_integer{elements={MinA,MaxA}}, + #t_integer{elements={MinB,MaxB}}) -> + #t_integer{elements={min(MinA,MinB),max(MaxA,MaxB)}}; +lub(#t_bs_context{slots=SlotsA,valid=ValidA}, + #t_bs_context{slots=SlotsB,valid=ValidB}) -> + #t_bs_context{slots=min(SlotsA, SlotsB), + valid=ValidA band ValidB}; +lub(#t_integer{}, #t_integer{}) -> #t_integer{}; +lub(list, cons) -> list; +lub(cons, list) -> list; +lub(nil, cons) -> list; +lub(cons, nil) -> list; +lub(nil, list) -> list; +lub(list, nil) -> list; +lub(#t_integer{}, float) -> number; +lub(float, #t_integer{}) -> number; +lub(#t_integer{}, number) -> number; +lub(number, #t_integer{}) -> number; +lub(float, number) -> number; +lub(number, float) -> number; +lub(#t_tuple{size=Sz,exact=ExactA,elements=EsA}, + #t_tuple{size=Sz,exact=ExactB,elements=EsB}) -> + Exact = ExactA and ExactB, + Es = lub_tuple_elements(Sz, EsA, EsB), + #t_tuple{size=Sz,exact=Exact,elements=Es}; +lub(#t_tuple{size=SzA,elements=EsA}, #t_tuple{size=SzB,elements=EsB}) -> + Sz = min(SzA, SzB), + Es = lub_tuple_elements(Sz, EsA, EsB), + #t_tuple{size=Sz,elements=Es}; +lub(_T1, _T2) -> + %%io:format("~p ~p\n", [_T1,_T2]), + any. + +lub_tuple_elements(MinSize, EsA, EsB) -> + Es0 = lub_elements(EsA, EsB), + maps:filter(fun(Index, _Type) -> Index =< MinSize end, Es0). + +lub_elements(Es1, Es2) -> + Keys = if + map_size(Es1) =< map_size(Es2) -> maps:keys(Es1); + map_size(Es1) > map_size(Es2) -> maps:keys(Es2) + end, + lub_elements_1(Keys, Es1, Es2, #{}). + +lub_elements_1([Key | Keys], Es1, Es2, Acc0) -> + case {Es1, Es2} of + {#{ Key := Type1 }, #{ Key := Type2 }} -> + %% Note the use of join/2; elements don't need to be normal types. + Acc = set_element_type(Key, join(Type1, Type2), Acc0), + lub_elements_1(Keys, Es1, Es2, Acc); + {#{}, #{}} -> + lub_elements_1(Keys, Es1, Es2, Acc0) + end; +lub_elements_1([], _Es1, _Es2, Acc) -> + Acc. + +%% + +gcd(A, B) -> + case A rem B of + 0 -> B; + X -> gcd(B, X) + end. + +%% + +record_key(#t_tuple{exact=true,size=Size,elements=#{ 1 := Tag }}) -> + case is_singleton_type(Tag) of + true -> {Size, Tag}; + false -> none + end; +record_key(_) -> + none. + +new_tuple_set(T) -> + case record_key(T) of + none -> T; + Key -> [{Key, T}] + end. + +%% + +shrink_union(#t_union{other=any}) -> + any; +shrink_union(#t_union{atom=Atom,list=none,number=none, + tuple_set=none,other=none}) -> + Atom; +shrink_union(#t_union{atom=none,list=List,number=none, + tuple_set=none,other=none}) -> + List; +shrink_union(#t_union{atom=none,list=none,number=Number, + tuple_set=none,other=none}) -> + Number; +shrink_union(#t_union{atom=none,list=none,number=none, + tuple_set=#t_tuple{}=Tuple,other=none}) -> + Tuple; +shrink_union(#t_union{atom=none,list=none,number=none, + tuple_set=[{_Key, Record}],other=none}) -> + #t_tuple{} = Record; %Assertion. +shrink_union(#t_union{atom=none,list=none,number=none, + tuple_set=none,other=Other}) -> + Other; +shrink_union(#t_union{}=T) -> + T. + +%% Verifies that the given type is well-formed. + +-spec verified_type(T) -> T when + T :: type(). + +verified_type(#t_union{atom=Atom, + list=List, + number=Number, + tuple_set=TSet, + other=Other}=T) -> + _ = verified_normal_type(Atom), + _ = verified_normal_type(List), + _ = verified_normal_type(Number), + _ = verify_tuple_set(TSet), + _ = verified_normal_type(Other), + T; +verified_type(T) -> + verified_normal_type(T). + +verify_tuple_set([_|_]=T) -> + _ = [verified_normal_type(Rec) || {_, Rec} <- T], + T; +verify_tuple_set(#t_tuple{}=T) -> + none = record_key(T), %Assertion. + T; +verify_tuple_set(none=T) -> + T. + +-spec verified_normal_type(T) -> T when + T :: normal_type(). + +verified_normal_type(any=T) -> T; +verified_normal_type(none=T) -> T; +verified_normal_type(#t_atom{elements=any}=T) -> T; +verified_normal_type(#t_atom{elements=[_|_]}=T) -> T; +verified_normal_type(#t_bitstring{unit=U}=T) + when is_integer(U), U >= 1 -> + T; +verified_normal_type(#t_bs_context{}=T) -> T; +verified_normal_type(#t_fun{arity=Arity}=T) + when Arity =:= any; is_integer(Arity) -> + T; +verified_normal_type(float=T) -> T; +verified_normal_type(#t_integer{elements=any}=T) -> T; +verified_normal_type(#t_integer{elements={Min,Max}}=T) + when is_integer(Min), is_integer(Max), Min =< Max -> + T; +verified_normal_type(list=T) -> T; +verified_normal_type(#t_map{}=T) -> T; +verified_normal_type(nil=T) -> T; +verified_normal_type(cons=T) -> T; +verified_normal_type(number=T) -> T; +verified_normal_type(#t_tuple{size=Size,elements=Es}=T) -> + %% All known elements must have a valid index and type (which may be a + %% union). 'any' is prohibited since it's implicit and should never be + %% present in the map, and a 'none' element ought to have reduced the + %% entire tuple to 'none'. + maps:fold(fun(Index, Element, _) when is_integer(Index), + 1 =< Index, Index =< Size, + Element =/= any, Element =/= none -> + verified_type(Element) + end, [], Es), + T. diff --git a/lib/compiler/src/beam_types.hrl b/lib/compiler/src/beam_types.hrl index 212fe62063..09f87d61ba 100644 --- a/lib/compiler/src/beam_types.hrl +++ b/lib/compiler/src/beam_types.hrl @@ -39,6 +39,13 @@ %% - #t_tuple{} Tuple. %% %% none No type (bottom element). +%% +%% We also use #t_union{} to represent conflicting types produced by certain +%% expressions, e.g. the "#t_atom{} or #t_tuple{}" of lists:keyfind/3, which is +%% very useful for preserving type information when we would otherwise have +%% reduced it to 'any'. Since few operations can make direct use of this extra +%% type information, types should generally be normalized to one of the above +%% before use. -define(ATOM_SET_SIZE, 5). @@ -62,8 +69,20 @@ -type elements() :: tuple_elements() | map_elements(). --type type() :: any | none | - list | number | - #t_atom{} | #t_bitstring{} | #t_bs_context{} | - #t_fun{} | #t_integer{} | #t_map{} | #t_tuple{} | - 'cons' | 'float' | 'nil'. +-type normal_type() :: any | none | + list | number | + #t_atom{} | #t_bitstring{} | #t_bs_context{} | + #t_fun{} | #t_integer{} | #t_map{} | #t_tuple{} | + 'cons' | 'float' | 'nil'. + +-type record_key() :: {Arity :: integer(), Tag :: normal_type() }. +-type record_set() :: ordsets:ordset({record_key(), #t_tuple{}}). +-type tuple_set() :: #t_tuple{} | record_set(). + +-record(t_union, {atom=none :: none | #t_atom{}, + list=none :: none | list | cons | nil, + number=none :: none | number | float | #t_integer{}, + tuple_set=none :: none | tuple_set(), + other=none :: normal_type()}). + +-type type() :: #t_union{} | normal_type(). diff --git a/lib/compiler/src/beam_validator.erl b/lib/compiler/src/beam_validator.erl index d959700b88..923a0b4a4e 100644 --- a/lib/compiler/src/beam_validator.erl +++ b/lib/compiler/src/beam_validator.erl @@ -570,7 +570,7 @@ valfun_1({get_tuple_element,Src,N,Dst}, Vst) -> Index = N+1, assert_not_literal(Src), assert_type(#t_tuple{size=Index}, Src, Vst), - #t_tuple{elements=Es} = get_term_type(Src, Vst), + #t_tuple{elements=Es} = normalize(get_term_type(Src, Vst)), Type = beam_types:get_element_type(Index, Es), extract_term(Type, {bif,element}, [{integer,Index}, Src], Dst, Vst); valfun_1({jump,{f,Lbl}}, Vst) -> @@ -762,7 +762,7 @@ valfun_4({set_tuple_element,Src,Tuple,N}, Vst) -> %% helpers as we must support overwriting (rather than just widening or %% narrowing) known elements, and we can't use extract_term either since %% the source tuple may be aliased. - #t_tuple{elements=Es0}=Type = get_term_type(Tuple, Vst), + #t_tuple{elements=Es0}=Type = normalize(get_term_type(Tuple, Vst)), Es = beam_types:set_element_type(I, get_term_type(Src, Vst), Es0), override_type(Type#t_tuple{elements=Es}, Tuple, Vst); %% Match instructions. @@ -1927,6 +1927,9 @@ is_literal(_) -> false. %% The funny-looking abstract types produced here are intended to provoke %% errors on actual use; they do no harm just lying around. +normalize(#t_abstract{}=A) -> error({abstract_type, A}); +normalize(T) -> beam_types:normalize(T). + join(Same, Same) -> Same; join(#t_abstract{}=A, B) -> #t_abstract{kind={join, A, B}}; join(A, #t_abstract{}=B) -> #t_abstract{kind={join, A, B}}; @@ -2369,7 +2372,7 @@ assert_not_fragile(Lit, #vst{}) -> %%% bif_types(Op, Ss, Vst) -> - Args = [get_term_type(Arg, Vst) || Arg <- Ss], + Args = [normalize(get_term_type(Arg, Vst)) || Arg <- Ss], beam_call_types:types(erlang, Op, Args). call_types({extfunc,M,F,A}, A, Vst) -> @@ -2384,7 +2387,8 @@ get_call_args(Arity, Vst) -> get_call_args_1(Arity, Arity, _) -> []; get_call_args_1(N, Arity, Vst) when N < Arity -> - [get_movable_term_type({x,N}, Vst) | get_call_args_1(N + 1, Arity, Vst)]. + ArgType = normalize(get_movable_term_type({x,N}, Vst)), + [ArgType | get_call_args_1(N + 1, Arity, Vst)]. check_limit({x,X}=Src) when is_integer(X) -> if diff --git a/lib/compiler/test/property_test/beam_types_prop.erl b/lib/compiler/test/property_test/beam_types_prop.erl index e797440ba5..8199d1bd5a 100644 --- a/lib/compiler/test/property_test/beam_types_prop.erl +++ b/lib/compiler/test/property_test/beam_types_prop.erl @@ -49,10 +49,10 @@ absorption_1() -> absorption_check(A, B) -> %% a ∨ (a ∧ b) = a, - A = beam_types:join(A, beam_types:meet(A, B)), + A = join(A, meet(A, B)), %% a ∧ (a ∨ b) = a. - A = beam_types:meet(A, beam_types:join(A, B)), + A = meet(A, join(A, B)), true. @@ -68,13 +68,13 @@ associativity_1() -> associativity_check(A, B, C) -> %% a ∨ (b ∨ c) = (a ∨ b) ∨ c, - LHS_Join = beam_types:join(A, beam_types:join(B, C)), - RHS_Join = beam_types:join(beam_types:join(A, B), C), + LHS_Join = join(A, join(B, C)), + RHS_Join = join(join(A, B), C), LHS_Join = RHS_Join, %% a ∧ (b ∧ c) = (a ∧ b) ∧ c. - LHS_Meet = beam_types:meet(A, beam_types:meet(B, C)), - RHS_Meet = beam_types:meet(beam_types:meet(A, B), C), + LHS_Meet = meet(A, meet(B, C)), + RHS_Meet = meet(meet(A, B), C), LHS_Meet = RHS_Meet, true. @@ -90,10 +90,10 @@ commutativity_1() -> commutativity_check(A, B) -> %% a ∨ b = b ∨ a, - true = beam_types:join(A, B) =:= beam_types:join(B, A), + true = join(A, B) =:= join(B, A), %% a ∧ b = b ∧ a. - true = beam_types:meet(A, B) =:= beam_types:meet(B, A), + true = meet(A, B) =:= meet(B, A), true. @@ -105,10 +105,10 @@ idempotence_1() -> idempotence_check(Type) -> %% a ∨ a = a, - Type = beam_types:join(Type, Type), + Type = join(Type, Type), %% a ∧ a = a. - Type = beam_types:meet(Type, Type), + Type = meet(Type, Type), true. @@ -117,13 +117,16 @@ identity() -> identity_check(Type) -> %% a ∨ [bottom element] = a, - Type = beam_types:join(Type, none), + Type = join(Type, none), %% a ∧ [top element] = a. - Type = beam_types:meet(Type, any), + Type = meet(Type, any), true. +meet(A, B) -> beam_types:meet(A, B). +join(A, B) -> beam_types:join(A, B). + %%% %%% Generators %%% @@ -149,8 +152,8 @@ list_types() -> numerical_types() -> [gen_integer(), float, number]. -nested_types(Depth) when Depth >= 3 -> []; -nested_types(Depth) -> [#t_map{}, gen_tuple(Depth + 1)]. +nested_types(Depth) when Depth >= 3 -> [none]; +nested_types(Depth) -> [#t_map{}, gen_union(Depth + 1), gen_tuple(Depth + 1)]. gen_atom() -> ?LET(Size, range(0, ?ATOM_SET_SIZE), @@ -158,12 +161,15 @@ gen_atom() -> 0 -> #t_atom{}; _ -> - ?LET(Set, sized_list(Size, atom()), + ?LET(Set, sized_list(Size, gen_atom_val()), begin #t_atom{elements=ordsets:from_list(Set)} end) end). +gen_atom_val() -> + ?LET(N, range($0, $~), list_to_atom([N])). + gen_binary() -> ?SHRINK(#t_bitstring{unit=range(1, 128)}, [#t_bitstring{unit=1}]). @@ -185,6 +191,25 @@ gen_tuple(Depth) -> elements=Elements} end)). +gen_union(Depth) -> + ?LAZY(oneof([gen_wide_union(Depth), gen_tuple_union(Depth)])). + +gen_wide_union(Depth) -> + ?LET({A, B, C, D}, {oneof(nested_types(Depth)), + oneof(numerical_types()), + oneof(list_types()), + oneof(other_types())}, + begin + T0 = join(A, B), + T1 = join(T0, C), + join(T1, D) + end). + +gen_tuple_union(Depth) -> + ?SIZED(Size, + ?LET(Tuples, sized_list(Size, gen_tuple(Depth)), + lists:foldl(fun join/2, none, Tuples))). + 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])). @@ -197,7 +222,6 @@ gen_element(Depth) -> _ -> true end)). - sized_list(0, _Gen) -> []; sized_list(N, Gen) -> [Gen | sized_list(N - 1, Gen)]. |