Sign Up
Log In
Log In
or
Sign Up
Places
All Projects
Status Monitor
Collapse sidebar
home:Ledest:erlang:23
erlang
4365-erl_types-Ignore-opaque-type-arguments.patch
Overview
Repositories
Revisions
Requests
Users
Attributes
Meta
File 4365-erl_types-Ignore-opaque-type-arguments.patch of Package erlang
From facb47b03d4389c966ebc0857cfd45306aa210d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?John=20H=C3=B6gberg?= <john@erlang.org> Date: Mon, 20 Sep 2021 11:17:48 +0200 Subject: [PATCH 5/7] erl_types: Ignore opaque type arguments TL;DR: Opaque types are rather convoluted, this commit removes one of the hairiest parts. ---- It is not commonly known that opaque types are invariant on their type parameters: an opaque type `foo:bar(gurka | gaffel)` _IS NOT_ a subtype of `foo:bar(atom())`, nor is it a supertype of `foo:bar(gurka)`. For an opaque type to be compatible with another instance of the same type, their type parameters have to be exactly equal. This may seem a bit strict but is required for correctness: while it's trivial to see that one can pass an `[integer()]` to a function expecting `[number()]` since the list type is covariant on the element type, we don't have a way to express whether an opaque type parameter is covariant, contravariant, or invariant. Nor can we infer it beyond toy cases. The easiest way to keep the type system sound in the face of that is to treat all type parameters as invariant. It's perhaps a bit surprising but there's nothing wrong with it. So far so good. Then we hit this marvel in `gb_sets`: ```erlang -spec add(Element, Set1) -> Set2 when Set1 :: set(Element), Set2 :: set(Element). ``` A strict reading of this says that it accepts a set containing a singleton `Element`, and produces a set containing `Element` alone. If we were to pass a set produced by this function to one that expects `gb_sets:set(atom())`, we would get a type error unless `Element` had already collapsed to `atom()`. (Other funny consequences are left as an exercise to the reader) Yet that works at the moment. Huh?! 1. dialyzer just throws away type variables in specs, replacing them with `term()` and removing all relations between them. Trying to fix that is how I noticed this wonderful quirk. 2. dialyzer considers `any()` in type variables to be quasi-equal to all other types. That is, `gb_sets:set(any())` is okay in functions that expect (say) `gb_sets:set(atom())` and vice versa. The former is awkward but the latter is where things go off the rails. We may pass `any()`d and more strictly typed opaques around interchangeably, but since type parameters are invariant there's no way for us to tell which is the subtype and which is the supertype! This effectively breaks the type lattice and sends dialyzer into infinite loops often enough that adding a test case to this commit is rather pointless: you can hardly even begin building a PLT of OTP before hitting it. Since we can't do anything about this without inventing a new notation and requiring people to rewrite their specs with it, I've decided to ignore type parameters altogether in this commit. It makes dialyzer less useful, but I believe it's worth it to ensure that the results are correct. --- lib/dialyzer/src/erl_types.erl | 166 +++--------------- .../test/map_SUITE_data/results/opaque_key | 4 +- .../test/opaque_SUITE_data/results/para | 32 ++-- 3 files changed, 39 insertions(+), 163 deletions(-) diff --git a/lib/hipe/cerl/erl_types.erl b/lib/hipe/cerl/erl_types.erl index 37b7793d56..b9af689ea7 100644 --- a/lib/hipe/cerl/erl_types.erl +++ b/lib/hipe/cerl/erl_types.erl @@ -319,11 +319,9 @@ -record(int_set, {set :: [integer()]}). -record(int_rng, {from :: rng_elem(), to :: rng_elem()}). -%% Note: the definition of #opaque{} was changed to 'mod' and 'name'; -%% it used to be an ordsets of {Mod, Name} pairs. The Dialyzer version -%% was updated to 2.7 due to this change. + -record(opaque, {mod :: module(), name :: atom(), - args = [] :: [erl_type()], struct :: erl_type()}). + arity = 0 :: arity(), struct :: erl_type()}). -define(atom(Set), #c{tag=?atom_tag, elements=Set}). -define(bitstr(Unit, Base), #c{tag=?binary_tag, elements=[Unit,Base]}). @@ -435,7 +433,7 @@ t_is_none(_) -> false. -spec t_opaque(module(), atom(), [_], erl_type()) -> erl_type(). t_opaque(Mod, Name, Args, Struct) -> - O = #opaque{mod = Mod, name = Name, args = Args, struct = Struct}, + O = #opaque{mod = Mod, name = Name, arity = length(Args), struct = Struct}, ?opaque(set_singleton(O)). -spec t_is_opaque(erl_type(), [erl_type()]) -> boolean(). @@ -2327,7 +2325,6 @@ t_has_var(?map(_, DefK, _)= Map) -> t_has_var_list(map_all_values(Map)) orelse t_has_var(DefK); t_has_var(?opaque(Set)) -> - %% Assume variables in 'args' are also present i 'struct' t_has_var_list([O#opaque.struct || O <- set_to_list(Set)]); t_has_var(?union(List)) -> t_has_var_list(List); @@ -2367,7 +2364,6 @@ t_collect_var_names(?map(_, DefK, _) = Map, Acc0) -> Acc = t_collect_vars_list(map_all_values(Map), Acc0), t_collect_var_names(DefK, Acc); t_collect_var_names(?opaque(Set), Acc) -> - %% Assume variables in 'args' are also present i 'struct' t_collect_vars_list([O#opaque.struct || O <- set_to_list(Set)], Acc); t_collect_var_names(?union(List), Acc) -> t_collect_vars_list(List, Acc); @@ -2714,8 +2710,8 @@ sup_opaque(List) -> ?opaque(ordsets:from_list(L)). sup_opaq(L0) -> - L1 = [{{Mod,Name,Args}, T} || - #opaque{mod = Mod, name = Name, args = Args}=T <- L0], + L1 = [{{Mod,Name,Arity}, T} || + #opaque{mod = Mod, name = Name, arity = Arity}=T <- L0], F = family(L1), [supl(Ts) || {_, Ts} <- F]. @@ -3163,121 +3159,13 @@ compatible_opaque_types(?opaque(Es1), ?opaque(Es2)) -> [{O1, O2} || O1 <- Es1, O2 <- Es2, is_compat_opaque_names(O1, O2)]. is_compat_opaque_names(Opaque1, Opaque2) -> - #opaque{mod = Mod1, name = Name1, args = Args1} = Opaque1, - #opaque{mod = Mod2, name = Name2, args = Args2} = Opaque2, - case {{Mod1, Name1, Args1}, {Mod2, Name2, Args2}} of - {ModNameArgs, ModNameArgs} -> true; - {{Mod, Name, Args1}, {Mod, Name, Args2}} -> - is_compat_args(Args1, Args2); + #opaque{mod = Mod1, name = Name1, arity = Arity1} = Opaque1, + #opaque{mod = Mod2, name = Name2, arity = Arity2} = Opaque2, + case {{Mod1, Name1, Arity1}, {Mod2, Name2, Arity2}} of + {ModNameArity, ModNameArity} -> true; _ -> false end. -is_compat_args([A1|Args1], [A2|Args2]) -> - is_compat_arg(A1, A2) andalso is_compat_args(Args1, Args2); -is_compat_args([], []) -> true; -is_compat_args(_, _) -> false. - --spec is_compat_arg(erl_type(), erl_type()) -> boolean(). - -%% The intention is that 'true' is to be returned iff one of the -%% arguments is a specialization of the other argument in the sense -%% that every type is a specialization of any(). For example, {_,_} is -%% a specialization of any(), but not of tuple(). Does not handle -%% variables, but any() and unions (sort of). However, the -%% implementation is more relaxed as any() is compatible to anything. - -is_compat_arg(T, T) -> true; -is_compat_arg(_, ?any) -> true; -is_compat_arg(?any, _) -> true; -is_compat_arg(?function(Domain1, Range1), ?function(Domain2, Range2)) -> - (is_compat_arg(Domain1, Domain2) andalso - is_compat_arg(Range1, Range2)); -is_compat_arg(?list(Contents1, Termination1, Size1), - ?list(Contents2, Termination2, Size2)) -> - (Size1 =:= Size2 andalso - is_compat_arg(Contents1, Contents2) andalso - is_compat_arg(Termination1, Termination2)); -is_compat_arg(?product(Types1), ?product(Types2)) -> - is_compat_list(Types1, Types2); -is_compat_arg(?map(Pairs1, DefK1, DefV1), ?map(Pairs2, DefK2, DefV2)) -> - {Ks1, _, Vs1} = lists:unzip3(Pairs1), - {Ks2, _, Vs2} = lists:unzip3(Pairs2), - Key1 = t_sup([DefK1 | Ks1]), - Key2 = t_sup([DefK2 | Ks2]), - case is_compat_arg(Key1, Key2) of - true -> - Value1 = t_sup([DefV1 | Vs1]), - Value2 = t_sup([DefV2 | Vs2]), - is_compat_arg(Value1, Value2); - false -> - false - end; -is_compat_arg(?tuple(?any, ?any, ?any), ?tuple(_, _, _)) -> false; -is_compat_arg(?tuple(_, _, _), ?tuple(?any, ?any, ?any)) -> false; -is_compat_arg(?tuple(Elements1, Arity, _), - ?tuple(Elements2, Arity, _)) when Arity =/= ?any -> - is_compat_list(Elements1, Elements2); -is_compat_arg(?tuple_set([{Arity, List}]), - ?tuple(Elements2, Arity, _)) when Arity =/= ?any -> - is_compat_list(sup_tuple_elements(List), Elements2); -is_compat_arg(?tuple(Elements1, Arity, _), - ?tuple_set([{Arity, List}])) when Arity =/= ?any -> - is_compat_list(Elements1, sup_tuple_elements(List)); -is_compat_arg(?tuple_set(List1), ?tuple_set(List2)) -> - try - is_compat_list_list([sup_tuple_elements(T) || {_Arity, T} <- List1], - [sup_tuple_elements(T) || {_Arity, T} <- List2]) - catch _:_ -> false - end; -is_compat_arg(?opaque(_) = T1, T2) -> - is_compat_arg(t_opaque_structure(T1), T2); -is_compat_arg(T1, ?opaque(_) = T2) -> - is_compat_arg(T1, t_opaque_structure(T2)); -is_compat_arg(?union(List1)=T1, ?union(List2)=T2) -> - case is_compat_union2(T1, T2) of - {yes, Type1, Type2} -> is_compat_arg(Type1, Type2); - no -> is_compat_list(List1, List2) - end; -is_compat_arg(?union(List), T2) -> - case unify_union(List) of - {yes, Type} -> is_compat_arg(Type, T2); - no -> false - end; -is_compat_arg(T1, ?union(List)) -> - case unify_union(List) of - {yes, Type} -> is_compat_arg(T1, Type); - no -> false - end; -is_compat_arg(?var(_), _) -> exit(error); -is_compat_arg(_, ?var(_)) -> exit(error); -is_compat_arg(?none, _) -> false; -is_compat_arg(_, ?none) -> false; -is_compat_arg(?unit, _) -> false; -is_compat_arg(_, ?unit) -> false; -is_compat_arg(#c{}, #c{}) -> false. - -is_compat_list_list(LL1, LL2) -> - length(LL1) =:= length(LL2) andalso is_compat_list_list1(LL1, LL2). - -is_compat_list_list1([], []) -> true; -is_compat_list_list1([L1|LL1], [L2|LL2]) -> - is_compat_list(L1, L2) andalso is_compat_list_list1(LL1, LL2). - -is_compat_list(L1, L2) -> - length(L1) =:= length(L2) andalso is_compat_list1(L1, L2). - -is_compat_list1([], []) -> true; -is_compat_list1([T1|L1], [T2|L2]) -> - is_compat_arg(T1, T2) andalso is_compat_list1(L1, L2). - -is_compat_union2(?union(List1)=T1, ?union(List2)=T2) -> - case {unify_union(List1), unify_union(List2)} of - {{yes, Type1}, {yes, Type2}} -> {yes, Type1, Type2}; - {{yes, Type1}, no} -> {yes, Type1, T2}; - {no, {yes, Type2}} -> {yes, T1, Type2}; - {no, no} -> no - end. - -spec t_inf_lists([erl_type()], [erl_type()]) -> [erl_type()]. t_inf_lists(L1, L2) -> @@ -3492,9 +3380,8 @@ t_subst_aux(?map(Pairs, DefK, DefV), Map) -> t_map([{K, MNess, t_subst_aux(V, Map)} || {K, MNess, V} <- Pairs], t_subst_aux(DefK, Map), t_subst_aux(DefV, Map)); t_subst_aux(?opaque(Es), Map) -> - List = [Opaque#opaque{args = [t_subst_aux(Arg, Map) || Arg <- Args], - struct = t_subst_aux(S, Map)} || - Opaque = #opaque{args = Args, struct = S} <- set_to_list(Es)], + List = [Opaque#opaque{struct = t_subst_aux(S, Map)} || + Opaque = #opaque{struct = S} <- set_to_list(Es)], ?opaque(ordsets:from_list(List)); t_subst_aux(?union(List), Map) -> ?union([t_subst_aux(E, Map) || E <- List]); @@ -3748,18 +3635,18 @@ unify_union(List) -> is_opaque_type(?opaque(Elements), Opaques) -> lists:any(fun(Opaque) -> is_opaque_type2(Opaque, Opaques) end, Elements). -is_opaque_type2(#opaque{mod = Mod1, name = Name1, args = Args1}, Opaques) -> +is_opaque_type2(#opaque{mod = Mod1, name = Name1, arity = Arity1}, Opaques) -> F1 = fun(?opaque(Es)) -> - F2 = fun(#opaque{mod = Mod, name = Name, args = Args}) -> - is_type_name(Mod1, Name1, Args1, Mod, Name, Args) + F2 = fun(#opaque{mod = Mod, name = Name, arity = Arity}) -> + is_type_name(Mod1, Name1, Arity1, Mod, Name, Arity) end, lists:any(F2, Es) end, lists:any(F1, Opaques). -is_type_name(Mod, Name, Args1, Mod, Name, Args2) -> - length(Args1) =:= length(Args2); -is_type_name(_Mod1, _Name1, _Args1, _Mod2, _Name2, _Args2) -> +is_type_name(Mod, Name, Arity, Mod, Name, Arity) -> + true; +is_type_name(_Mod1, _Name1, _Arity1, _Mod2, _Name2, _Arity2) -> false. %% Two functions since t_unify is not symmetric. @@ -4476,8 +4363,8 @@ t_to_string(?identifier(Set), _RecDict) -> flat_join([flat_format("~w()", [T]) || T <- set_to_list(Set)], " | ") end; t_to_string(?opaque(Set), RecDict) -> - flat_join([opaque_type(Mod, Name, Args, S, RecDict) || - #opaque{mod = Mod, name = Name, struct = S, args = Args} + flat_join([opaque_type(Mod, Name, Arity, S, RecDict) || + #opaque{mod = Mod, name = Name, struct = S, arity = Arity} <- set_to_list(Set)], " | "); t_to_string(?matchstate(Pres, Slots), RecDict) -> @@ -4650,19 +4537,18 @@ union_sequence(Types, RecDict) -> flat_join(List, " | "). -ifdef(DEBUG). -opaque_type(Mod, Name, _Args, S, RecDict) -> - ArgsString = comma_sequence(_Args, RecDict), +opaque_type(Mod, Name, Arity, S, RecDict) -> String = t_to_string(S, RecDict), - opaque_name(Mod, Name, ArgsString) ++ "[" ++ String ++ "]". + opaque_name(Mod, Name, Arity) ++ "[" ++ String ++ "]". -else. -opaque_type(Mod, Name, Args, _S, RecDict) -> - ArgsString = comma_sequence(Args, RecDict), - opaque_name(Mod, Name, ArgsString). +opaque_type(Mod, Name, Arity, _S, _RecDict) -> + opaque_name(Mod, Name, Arity). -endif. -opaque_name(Mod, Name, Extra) -> +opaque_name(Mod, Name, Arity) -> S = mod_name(Mod, Name), - flat_format("~ts(~ts)", [S, Extra]). + Args = lists:join($,, lists:duplicate(Arity, $_)), + flat_format("~ts(~ts)", [S, Args]). mod_name(Mod, Name) -> flat_format("~w:~tw", [Mod, Name]). diff --git a/lib/dialyzer/test/map_SUITE_data/results/opaque_key b/lib/dialyzer/test/map_SUITE_data/results/opaque_key index b3a2d2b78c..b70157f1af 100644 --- a/lib/dialyzer/test/map_SUITE_data/results/opaque_key +++ b/lib/dialyzer/test/map_SUITE_data/results/opaque_key @@ -4,8 +4,8 @@ opaque_key_adt.erl:41:2: Invalid type specification for function opaque_key_adt: opaque_key_adt.erl:44: Invalid type specification for function opaque_key_adt:s5/0. The success typing is () -> #{2:=3} opaque_key_adt.erl:56: Invalid type specification for function opaque_key_adt:smt1/0. The success typing is () -> #{3:='a'} opaque_key_adt.erl:59: Invalid type specification for function opaque_key_adt:smt2/0. The success typing is () -> #{1:='a'} -opaque_key_use.erl:13: The test opaque_key_use:t() =:= opaque_key_use:t(integer()) can never evaluate to 'true' -opaque_key_use.erl:24: Attempt to test for equality between a term of type opaque_key_adt:t(integer()) and a term of opaque type opaque_key_adt:t() +opaque_key_use.erl:13: The test opaque_key_use:t() =:= opaque_key_use:t(_) can never evaluate to 'true' +opaque_key_use.erl:24: Attempt to test for equality between a term of type opaque_key_adt:t(_) and a term of opaque type opaque_key_adt:t() opaque_key_use.erl:37: Function adt_mm1/0 has no local return opaque_key_use.erl:40: The attempt to match a term of type opaque_key_adt:m() against the pattern #{A:=R} breaks the opacity of the term opaque_key_use.erl:48: Function adt_mu1/0 has no local return diff --git a/lib/dialyzer/test/opaque_SUITE_data/results/para b/lib/dialyzer/test/opaque_SUITE_data/results/para index d0ddab7b66..0ba2a24996 100644 --- a/lib/dialyzer/test/opaque_SUITE_data/results/para +++ b/lib/dialyzer/test/opaque_SUITE_data/results/para @@ -1,34 +1,24 @@ -para1.erl:18: The test para1:t(atom()) =:= para1:t(integer()) can never evaluate to 'true' -para1.erl:23: The test para1:t(atom()) =:= para1:t() can never evaluate to 'true' -para1.erl:28: The test para1:t() =:= para1:t(integer()) can never evaluate to 'true' +para1.erl:18: The test para1:t(_) =:= para1:t(_) can never evaluate to 'true' +para1.erl:23: The test para1:t(_) =:= para1:t() can never evaluate to 'true' +para1.erl:28: The test para1:t() =:= para1:t(_) can never evaluate to 'true' para1.erl:33: The test {3,2} =:= {'a','b'} can never evaluate to 'true' -para1.erl:38: Attempt to test for equality between a term of type para1_adt:t(integer()) and a term of opaque type para1_adt:t(atom()) -para1.erl:43: Attempt to test for equality between a term of type para1_adt:t() and a term of opaque type para1_adt:t(atom()) -para1.erl:48: Attempt to test for equality between a term of type para1_adt:t(integer()) and a term of opaque type para1_adt:t() +para1.erl:38: The test para1_adt:t(_) =:= para1_adt:t(_) can never evaluate to 'true' +para1.erl:43: Attempt to test for equality between a term of type para1_adt:t() and a term of opaque type para1_adt:t(_) +para1.erl:48: Attempt to test for equality between a term of type para1_adt:t(_) and a term of opaque type para1_adt:t() para1.erl:53: The test {3,2} =:= {'a','b'} can never evaluate to 'true' -para2.erl:103: Attempt to test for equality between a term of type para2_adt:circ(integer(),integer()) and a term of opaque type para2_adt:circ(integer()) -para2.erl:117: Attempt to test for equality between a term of type para2_adt:un(atom(),integer()) and a term of opaque type para2_adt:un(integer(),atom()) +para2.erl:103: Attempt to test for equality between a term of type para2_adt:circ(_,_) and a term of opaque type para2_adt:circ(_) para2.erl:31: The test 'a' =:= 'b' can never evaluate to 'true' para2.erl:61: Attempt to test for equality between a term of type para2_adt:c2() and a term of opaque type para2_adt:c1() para2.erl:66: The test 'a' =:= 'b' can never evaluate to 'true' -para2.erl:88: The test para2:circ(integer()) =:= para2:circ(integer(),integer()) can never evaluate to 'true' +para2.erl:88: The test para2:circ(_) =:= para2:circ(_,_) can never evaluate to 'true' para3.erl:28: Invalid type specification for function para3:ot2/0. The success typing is () -> 'foo' para3.erl:36: The pattern {{{17}}} can never match the type {{{{{{_,_,_,_,_}}}}}} para3.erl:55: Invalid type specification for function para3:t2/0. The success typing is () -> 'foo' para3.erl:65: The attempt to match a term of type {{{{{para3_adt:ot1(_,_,_,_,_)}}}}} against the pattern {{{{{17}}}}} breaks the opacity of para3_adt:ot1(_,_,_,_,_) para3.erl:68: The pattern {{{{17}}}} can never match the type {{{{{para3_adt:ot1(_,_,_,_,_)}}}}} -para3.erl:74: The specification for para3:exp_adt/0 has an opaque subtype para3_adt:exp1(para3_adt:exp2()) which is violated by the success typing () -> 3 -para4.erl:21: Invalid type specification for function para4:a/1. The success typing is (para4:d_all() | para4:d_atom()) -> [{atom() | integer(),atom() | integer()}] -para4.erl:26: Invalid type specification for function para4:i/1. The success typing is (para4:d_all() | para4:d_integer()) -> [{atom() | integer(),atom() | integer()}] +para3.erl:74: The specification for para3:exp_adt/0 has an opaque subtype para3_adt:exp1(_) which is violated by the success typing () -> 3 para4.erl:31: Invalid type specification for function para4:t/1. The success typing is (para4:d_all() | para4:d_tuple()) -> [{atom() | integer(),atom() | integer()}] -para4.erl:59: Attempt to test for equality between a term of type para4_adt:t(atom() | integer()) and a term of opaque type para4_adt:t(integer()) -para4.erl:64: Attempt to test for equality between a term of type para4_adt:t(atom() | integer()) and a term of opaque type para4_adt:t(atom()) -para4.erl:69: Attempt to test for equality between a term of type para4_adt:int(1 | 2 | 3 | 4) and a term of opaque type para4_adt:int(1 | 2) -para4.erl:74: Attempt to test for equality between a term of type para4_adt:int(2 | 3 | 4) and a term of opaque type para4_adt:int(1 | 2) -para4.erl:79: Attempt to test for equality between a term of type para4_adt:int(2 | 3 | 4) and a term of opaque type para4_adt:int(5 | 6 | 7) -para4.erl:84: Attempt to test for equality between a term of type para4_adt:un(3 | 4) and a term of opaque type para4_adt:un(1 | 2) -para4.erl:89: Attempt to test for equality between a term of type para4_adt:tup({_,_}) and a term of opaque type para4_adt:tup(tuple()) -para4.erl:94: Attempt to test for equality between a term of type para4_adt:t(#{1=>'a'}) and a term of opaque type para4_adt:t(#{2=>'b'}) -para5.erl:13: Attempt to test for inequality between a term of type para5_adt:dd(atom()) and a term of opaque type para5_adt:d() +para4.erl:79: The test para4_adt:int(_) =:= para4_adt:int(_) can never evaluate to 'true' +para5.erl:13: Attempt to test for inequality between a term of type para5_adt:dd(_) and a term of opaque type para5_adt:d() para5.erl:8: The test para5_adt:d() =:= para5_adt:d() can never evaluate to 'true' -- 2.31.1
Locations
Projects
Search
Status Monitor
Help
OpenBuildService.org
Documentation
API Documentation
Code of Conduct
Contact
Support
@OBShq
Terms
openSUSE Build Service is sponsored by
The Open Build Service is an
openSUSE project
.
Sign Up
Log In
Places
Places
All Projects
Status Monitor