File 2036-dialyzer_typesig-Ensure-that-unification-a... of Package erlang

Overview Repositories Revisions Requests Users Attributes Meta

File 2036-dialyzer_typesig-Ensure-that-unification-always-make.patch of Package erlang

From b98ebc672effaf44086a519aefd4d248297f40c2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?John=20H=C3=B6gberg?= <john@erlang.org>
Date: Mon, 20 Sep 2021 19:25:53 +0200
Subject: [PATCH 6/7] dialyzer_typesig: Ensure that unification always makes
 progress

Prior to this change we'd always overwrite the stored types of
variables after unification. This worked for the most part but
would enter an endless loop whenever a bound variable
countermanded (but _NOT_ contradicted) another constraint, such
as in this sequence:

```
Solving: {var(309),var(310)} :: {'any', ...} | {'none', ...}
            eq
         var(39) :: {'any', ...} | {'none', ...}
  Inf: {'any', ...} | {'none', ...}
Entering var(309) :: 'any' | 'none'
Storing 309 :: 'any' | 'none'

... ... ...

Solving: var(21) :: erl_types:erl_type()
            eq
         var(309) :: 'any' | 'none'
  Inf: erl_types:erl_type()
Entering var(21) :: erl_types:erl_type()
Entering var(309) :: erl_types:erl_type()
Storing 309 :: erl_types:erl_type()
```

While we're at it, remove the unused (and untested) t_unify/2.
---
 lib/dialyzer/src/dialyzer_typesig.erl |  74 +++++++-----
 lib/dialyzer/src/erl_types.erl        | 158 +++-----------------------
 2 files changed, 59 insertions(+), 173 deletions(-)

diff --git a/lib/dialyzer/src/dialyzer_typesig.erl b/lib/dialyzer/src/dialyzer_typesig.erl
index dea9b2007d..ca7f46d086 100644
--- a/lib/dialyzer/src/dialyzer_typesig.erl
+++ b/lib/dialyzer/src/dialyzer_typesig.erl
@@ -2242,27 +2242,50 @@ solve_one_c(#constraint{lhs = Lhs, rhs = Rhs, op = Op}, Map) ->
   end.
 
 solve_subtype(Type, Inf, Map) ->
-  %% case cerl:is_literal(Type) of
-  %%   true ->
-  %%     case t_is_subtype(t_from_term(cerl:concrete(Type)), Inf) of
-  %%	true -> {ok, Map};
-  %%	false -> error
-  %%     end;
-  %%   false ->
-      %% t_unify_table_only() is somewhat faster than t_unify(). The
-      %% fact that all variables occur in Type (no variables in Inf)
-      %% is not used in any way.
-      %% try t_unify(Type, Inf) of
-      %%   {_, List} -> {ok, enter_type_list(List, Map)}
-      try t_unify_table_only(Type, Inf) of
-          List -> {ok, enter_type_list(List, Map)}
-      catch
-	throw:{mismatch, _T1, _T2} ->
-	  ?debug("Mismatch between ~ts and ~ts\n",
-		 [format_type(_T1), format_type(_T2)]),
-	  error
-      end.
-  %% end.
+  try t_unify_table_only(Type, Inf) of
+    Bindings ->
+      refine_bindings(maps:to_list(Bindings), Map, [])
+  catch
+    throw:{mismatch, _T1, _T2} ->
+      ?debug("Mismatch between ~ts and ~ts\n",
+             [format_type(_T1), format_type(_T2)]),
+      error
+  end.
+
+%% Similar to enter_type/3 over a list, but refines known types rather than
+%% replaces them.
+refine_bindings([{Key, Val} | Tail], Map, U0) ->
+  ?debug("Unifying ~ts :: ~ts\n",
+         [format_type(t_var(Key)), format_type(Val)]),
+  %% It's important to keep opaque types whose internal structure is any(),
+  %% hence the equality check on t_any() rather than t_is_any/1.
+  case t_is_equal(Val, t_any()) of
+    true ->
+      refine_bindings(Tail, maps:remove(Key, Map), U0);
+    false ->
+      LimitedVal = t_limit(Val, ?INTERNAL_TYPE_LIMIT),
+      case Map of
+        #{ Key := Old } ->
+          LimitedInf = t_inf(Old, LimitedVal),
+          case t_is_none(LimitedInf) of
+            true ->
+              error;
+            false ->
+              case t_is_equal(Old, LimitedInf) of
+                true ->
+                  refine_bindings(Tail, Map, U0);
+                false ->
+                  U = ordsets:add_element(Key, U0),
+                  refine_bindings(Tail, Map#{ Key => LimitedInf }, U)
+              end
+          end;
+        #{} ->
+          U = ordsets:add_element(Key, U0),
+          refine_bindings(Tail, Map#{ Key => LimitedVal }, U)
+      end
+  end;
+refine_bindings([], Map, U) ->
+  {ok, {Map, U}}.
 
 report_failed_constraint(_C, _Map) ->
   ?debug("+++++++++++\nFailed: ~ts :: ~ts ~w ~ts :: ~ts\n+++++++++++\n",
@@ -2335,15 +2358,6 @@ enter_type_lists([Key|KeyTail], [Val|ValTail], Map) ->
 enter_type_lists([], [], Map) ->
   Map.
 
-enter_type_list(KeyVals, Map) ->
-  enter_type_list(KeyVals, Map, []).
-
-enter_type_list([{Key, Val}|Tail], Map, U0) ->
-  {Map1,U1} = enter_type2(Key, Val, Map),
-  enter_type_list(Tail, Map1, U1++U0);
-enter_type_list([], Map, U) ->
-  {Map, ordsets:from_list(U)}.
-
 enter_type2(Key, Val, Map) ->
   Map1 = enter_type(Key, Val, Map),
   {Map1, [Key || not is_same(Key, Map, Map1)]}.
diff --git a/lib/dialyzer/src/erl_types.erl b/lib/dialyzer/src/erl_types.erl
index b9af689ea7..f82251d1f0 100644
--- a/lib/dialyzer/src/erl_types.erl
+++ b/lib/dialyzer/src/erl_types.erl
@@ -202,7 +202,7 @@
 	 t_tuple_sizes/1,
 	 t_tuple_subtypes/1,
          t_tuple_subtypes/2,
-	 t_unify_table_only/2, t_unify/2,
+	 t_unify_table_only/2,
 	 t_unit/0,
 	 t_unopaque/1, t_unopaque/2,
 	 t_var/1,
@@ -370,7 +370,8 @@
 -type type_table() :: #{record_key() | type_key() =>
                         record_value() | type_value()}.
 
--opaque var_table() :: #{atom() => erl_type()}.
+-type var_name() :: atom() | integer().
+-type var_table() :: #{ var_name() => erl_type() }.
 
 %%-----------------------------------------------------------------------------
 %% Unions
@@ -3392,30 +3393,27 @@ t_subst_aux(T, _Map) ->
 %% Unification
 %%
 
--spec t_unify_table_only(erl_type(), erl_type()) -> [{_, erl_type()}].
+-spec t_unify_table_only(erl_type(), erl_type()) -> var_table().
 
 %% A simplified version of t_unify/2 which returns the variable
 %% bindings only. It is faster, mostly because t_subst() is not
 %% called.
 
 t_unify_table_only(T1, T2) ->
-  VarMap = t_unify_table_only(T1, T2, #{}),
-  lists:keysort(1, maps:to_list(VarMap)).
+  t_unify_table_only(T1, T2, #{}).
 
 t_unify_table_only(?var(Id), ?var(Id), VarMap) ->
   VarMap;
-t_unify_table_only(?var(Id1) = T, ?var(Id2), VarMap) ->
-  case maps:find(Id1, VarMap) of
-    error ->
-      case maps:find(Id2, VarMap) of
-	error -> VarMap#{Id2 => T};
-	{ok, Type} -> t_unify_table_only(T, Type, VarMap)
-      end;
-    {ok, Type1} ->
-      case maps:find(Id2, VarMap) of
-	error -> VarMap#{Id2 => T};
-	{ok, Type2} -> t_unify_table_only(Type1, Type2, VarMap)
-      end
+t_unify_table_only(?var(Id1) = LHS, ?var(Id2) = RHS, VarMap) ->
+  case VarMap of
+    #{ Id1 := Type1, Id2 := Type2} ->
+        t_unify_table_only(Type1, Type2, VarMap);
+    #{ Id1 := Type } ->
+        t_unify_table_only(Type, RHS, VarMap);
+    #{ Id2 := Type } ->
+        t_unify_table_only(LHS, Type, VarMap);
+    #{} ->
+        VarMap#{ Id1 => LHS, Id2 => RHS }
   end;
 t_unify_table_only(?var(Id), Type, VarMap) ->
   case maps:find(Id, VarMap) of
@@ -3505,106 +3503,6 @@ unify_lists_table_only([T1|Left1], [T2|Left2], VarMap) ->
 unify_lists_table_only([], [], VarMap) ->
   VarMap.
 
--type t_unify_ret() :: {erl_type(), [{_, erl_type()}]}.
-
--spec t_unify(erl_type(), erl_type()) -> t_unify_ret().
-
-t_unify(T1, T2) ->
-  {T, VarMap} = t_unify(T1, T2, #{}),
-  {t_subst(T, VarMap), lists:keysort(1, maps:to_list(VarMap))}.
-
-t_unify(?var(Id) = T, ?var(Id), VarMap) ->
-  {T, VarMap};
-t_unify(?var(Id1) = T, ?var(Id2), VarMap) ->
-  case maps:find(Id1, VarMap) of
-    error ->
-      case maps:find(Id2, VarMap) of
-	error -> {T, VarMap#{Id2 => T}};
-	{ok, Type} -> t_unify(T, Type, VarMap)
-      end;
-    {ok, Type1} ->
-      case maps:find(Id2, VarMap) of
-	error -> {Type1, VarMap#{Id2 => T}};
-	{ok, Type2} -> t_unify(Type1, Type2, VarMap)
-      end
-  end;
-t_unify(?var(Id), Type, VarMap) ->
-  case maps:find(Id, VarMap) of
-    error -> {Type, VarMap#{Id => Type}};
-    {ok, VarType} -> t_unify(VarType, Type, VarMap)
-  end;
-t_unify(Type, ?var(Id), VarMap) ->
-  case maps:find(Id, VarMap) of
-    error -> {Type, VarMap#{Id => Type}};
-    {ok, VarType} -> t_unify(VarType, Type, VarMap)
-  end;
-t_unify(?function(Domain1, Range1), ?function(Domain2, Range2), VarMap) ->
-  {Domain, VarMap1} = t_unify(Domain1, Domain2, VarMap),
-  {Range, VarMap2} = t_unify(Range1, Range2, VarMap1),
-  {?function(Domain, Range), VarMap2};
-t_unify(?list(Contents1, Termination1, Size),
-	?list(Contents2, Termination2, Size), VarMap) ->
-  {Contents, VarMap1} = t_unify(Contents1, Contents2, VarMap),
-  {Termination, VarMap2} = t_unify(Termination1, Termination2, VarMap1),
-  {?list(Contents, Termination, Size), VarMap2};
-t_unify(?product(Types1), ?product(Types2), VarMap) ->
-  {Types, VarMap1} = unify_lists(Types1, Types2, VarMap),
-  {?product(Types), VarMap1};
-t_unify(?tuple(?any, ?any, ?any) = T, ?tuple(?any, ?any, ?any), VarMap) ->
-  {T, VarMap};
-t_unify(?tuple(Elements1, Arity, _),
-	?tuple(Elements2, Arity, _), VarMap) when Arity =/= ?any ->
-  {NewElements, VarMap1} = unify_lists(Elements1, Elements2, VarMap),
-  {t_tuple(NewElements), VarMap1};
-t_unify(?tuple_set([{Arity, _}]) = T1,
-	?tuple(_, Arity, _) = T2, VarMap) when Arity =/= ?any ->
-  unify_tuple_set_and_tuple1(T1, T2, VarMap);
-t_unify(?tuple(_, Arity, _) = T1,
-	?tuple_set([{Arity, _}]) = T2, VarMap) when Arity =/= ?any ->
-  unify_tuple_set_and_tuple2(T1, T2, VarMap);
-t_unify(?tuple_set(List1) = T1, ?tuple_set(List2) = T2, VarMap) ->
-  try
-    unify_lists(lists:append([T || {_Arity, T} <- List1]),
-                lists:append([T || {_Arity, T} <- List2]), VarMap)
-  of
-    {Tuples, NewVarMap} -> {t_sup(Tuples), NewVarMap}
-  catch _:_ -> throw({mismatch, T1, T2})
-  end;
-t_unify(?map(_, ADefK, ADefV) = A, ?map(_, BDefK, BDefV) = B, VarMap0) ->
-  {DefK, VarMap1} = t_unify(ADefK, BDefK, VarMap0),
-  {DefV, VarMap2} = t_unify(ADefV, BDefV, VarMap1),
-  {Pairs, VarMap} =
-    map_pairwise_merge_foldr(
-      fun(K, MNess, V1, MNess, V2, {Pairs0, VarMap3}) ->
-	  %% We know that the keys unify and do not contain variables, or they
-	  %% would not be singletons
-	  %% TODO: Should V=?none (known missing keys) be handled special?
-	  {V, VarMap4} = t_unify(V1, V2, VarMap3),
-	  {[{K,MNess,V}|Pairs0], VarMap4};
-	 (K, _, V1, _, V2, {Pairs0, VarMap3}) ->
-	  %% One mandatory and one optional; what should be done in this case?
-	  {V, VarMap4} = t_unify(V1, V2, VarMap3),
-	  {[{K,?mand,V}|Pairs0], VarMap4}
-      end, {[], VarMap2}, A, B),
-  {t_map(Pairs, DefK, DefV), VarMap};
-t_unify(?opaque(_) = T1, ?opaque(_) = T2, VarMap) ->
-  t_unify(t_opaque_structure(T1), t_opaque_structure(T2), VarMap);
-t_unify(T1, ?opaque(_) = T2, VarMap) ->
-  t_unify(T1, t_opaque_structure(T2), VarMap);
-t_unify(?opaque(_) = T1, T2, VarMap) ->
-  t_unify(t_opaque_structure(T1), T2, VarMap);
-t_unify(T, T, VarMap) ->
-  {T, VarMap};
-t_unify(?union(_)=T1, ?union(_)=T2, VarMap) ->
-  {Type1, Type2} = unify_union2(T1, T2),
-  t_unify(Type1, Type2, VarMap);
-t_unify(?union(_)=T1, T2, VarMap) ->
-  t_unify(unify_union1(T1, T1, T2), T2, VarMap);
-t_unify(T1, ?union(_)=T2, VarMap) ->
-  t_unify(T1, unify_union1(T2, T1, T2), VarMap);
-t_unify(T1, T2, _) ->
-  throw({mismatch, T1, T2}).
-
 unify_union2(?union(List1)=T1, ?union(List2)=T2) ->
   case {unify_union(List1), unify_union(List2)} of
     {{yes, Type1}, {yes, Type2}} -> {Type1, Type2};
@@ -3649,32 +3547,6 @@ is_type_name(Mod, Name, Arity, Mod, Name, Arity) ->
 is_type_name(_Mod1, _Name1, _Arity1, _Mod2, _Name2, _Arity2) ->
   false.
 
-%% Two functions since t_unify is not symmetric.
-unify_tuple_set_and_tuple1(?tuple_set([{Arity, List}]),
-                           ?tuple(Elements2, Arity, _), VarMap) ->
-  %% Can only work if the single tuple has variables at correct places.
-  %% Collapse the tuple set.
-  {NewElements, VarMap1} =
-    unify_lists(sup_tuple_elements(List), Elements2, VarMap),
-  {t_tuple(NewElements), VarMap1}.
-
-unify_tuple_set_and_tuple2(?tuple(Elements2, Arity, _),
-                           ?tuple_set([{Arity, List}]), VarMap) ->
-  %% Can only work if the single tuple has variables at correct places.
-  %% Collapse the tuple set.
-  {NewElements, VarMap1} =
-    unify_lists(Elements2, sup_tuple_elements(List), VarMap),
-  {t_tuple(NewElements), VarMap1}.
-
-unify_lists(L1, L2, VarMap) ->
-  unify_lists(L1, L2, VarMap, []).
-
-unify_lists([T1|Left1], [T2|Left2], VarMap, Acc) ->
-  {NewT, NewVarMap} = t_unify(T1, T2, VarMap),
-  unify_lists(Left1, Left2, NewVarMap, [NewT|Acc]);
-unify_lists([], [], VarMap, Acc) ->
-  {lists:reverse(Acc), VarMap}.
-
 %%t_assign_variables_to_subtype(T1, T2) ->
 %%  try
 %%    Dict = assign_vars(T1, T2, dict:new()),
-- 
2.31.1

Places

File 2036-dialyzer_typesig-Ensure-that-unification-always-make.patch of Package erlang

Places