dialyzer: Unfold cerl patterns containing maps

Dialyzer relies heavily on the assumption that the type of a literal
that is used as a pattern is the type of any value that can match that
pattern. For maps, that is not true, and it was causing bad analysis
results. A new help function dialyzer_utils:refold_pattern/1 identifies
maps in literal patterns, and unfolds and labels them, allowing them to
be properly analysed.

3 files changed, 84 insertions, 9 deletions

diff --git a/lib/dialyzer/src/dialyzer_dataflow.erl b/lib/dialyzer/src/dialyzer_dataflow.erl
index a3b3e3291c..9827fda6e3 100644
--- a/lib/dialyzer/src/dialyzer_dataflow.erl
+++ b/lib/dialyzer/src/dialyzer_dataflow.erl
@@ -1482,7 +1482,9 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
   {NewMap, TypeOut} =
     case cerl:type(Pat) of
       alias ->
-	AliasPat = cerl:alias_pat(Pat),
+	%% Map patterns are more allowing than the type of their literal. We
+	%% must unfold AliasPat if it is a literal.
+	AliasPat = dialyzer_utils:refold_pattern(cerl:alias_pat(Pat)),
 	Var = cerl:alias_var(Pat),
 	Map1 = enter_subst(Var, AliasPat, Map),
 	{Map2, [PatType]} = bind_pat_vars([AliasPat], [Type], [],
@@ -1523,11 +1525,20 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	    {Map1, t_cons(HdType, TlType)}
 	end;
       literal ->
-	Literal = literal_type(Pat),
-	case t_is_none(t_inf(Literal, Type, Opaques)) of
+	Pat0 = dialyzer_utils:refold_pattern(Pat),
+	case cerl:is_literal(Pat0) of
 	  true ->
-	    bind_opaque_pats(Literal, Type, Pat, State);
-	  false -> {Map, Literal}
+	    Literal = literal_type(Pat),
+	    case t_is_none(t_inf(Literal, Type, Opaques)) of
+	      true ->
+		bind_opaque_pats(Literal, Type, Pat, State);
+	      false -> {Map, Literal}
+	    end;
+	  false ->
+	    %% Retry with the unfolded pattern
+	    {Map1, [PatType]}
+	      = bind_pat_vars([Pat0], [Type], [], Map, State, Rev),
+	    {Map1, PatType}
 	end;
       map ->
 	MapT = t_inf(Type, t_map(), Opaques),
@@ -2742,8 +2753,9 @@ store_map(Key, Val, #map{dict = Dict, ref = undefined} = Map) ->
 store_map(Key, Val, #map{dict = Dict, modified = Mod} = Map) ->
   Map#map{dict = dict:store(Key, Val, Dict), modified = [Key | Mod]}.
 
-enter_subst(Key, Val, #map{subst = Subst} = MS) ->
+enter_subst(Key, Val0, #map{subst = Subst} = MS) ->
   KeyLabel = get_label(Key),
+  Val = dialyzer_utils:refold_pattern(Val0),
   case cerl:is_literal(Val) of
     true ->
       store_map(KeyLabel, literal_type(Val), MS);
diff --git a/lib/dialyzer/src/dialyzer_typesig.erl b/lib/dialyzer/src/dialyzer_typesig.erl
index 12d6673d28..810b7c55e9 100644
--- a/lib/dialyzer/src/dialyzer_typesig.erl
+++ b/lib/dialyzer/src/dialyzer_typesig.erl
@@ -393,8 +393,18 @@ traverse(Tree, DefinedVars, State) ->
       {State2, _} = traverse_list(Funs, DefinedVars1, State1),
       traverse(Body, DefinedVars1, State2);
     literal ->
-      Type = t_from_term(cerl:concrete(Tree)),
-      {State, Type};
+      %% Maps are special; a literal pattern matches more than just the value
+      %% constructed by the literal. For example #{} constructs the empty map,
+      %% but matches every map.
+      case state__is_in_match(State) of
+	true ->
+	  Tree1 = dialyzer_utils:refold_pattern(Tree),
+	  case cerl:is_literal(Tree1) of
+	    false -> traverse(Tree1, DefinedVars, State);
+	    true -> {State, t_from_term(cerl:concrete(Tree))}
+	  end;
+	_ -> {State, t_from_term(cerl:concrete(Tree))}
+      end;
     module ->
       Defs = cerl:module_defs(Tree),
       Funs = [Fun || {_Var, Fun} <- Defs],
@@ -1110,7 +1120,9 @@ bitstr_val_constr(SizeType, UnitVal, Flags) ->
       end
   end.
 
-get_safe_underapprox_1([Pat|Left], Acc, Map) ->
+get_safe_underapprox_1([Pat0|Left], Acc, Map) ->
+  %% Maps should be treated as patterns, not as literals
+  Pat = dialyzer_utils:refold_pattern(Pat0),
   case cerl:type(Pat) of
     alias ->
       APat = cerl:alias_pat(Pat),
diff --git a/lib/dialyzer/src/dialyzer_utils.erl b/lib/dialyzer/src/dialyzer_utils.erl
index 5fc1c0e691..b3505f5197 100644
--- a/lib/dialyzer/src/dialyzer_utils.erl
+++ b/lib/dialyzer/src/dialyzer_utils.erl
@@ -49,6 +49,7 @@
 	 process_record_remote_types/1,
          sets_filter/2,
 	 src_compiler_opts/0,
+	 refold_pattern/1,
 	 parallelism/0,
          family/1
 	]).
@@ -834,6 +835,56 @@ pp_atom(Atom) ->
 
 %%------------------------------------------------------------------------------
 
+-spec refold_pattern(cerl:cerl()) -> cerl:cerl().
+
+refold_pattern(Pat) ->
+  %% Avoid the churn of unfolding and refolding
+  case cerl:is_literal(Pat) andalso find_map(cerl:concrete(Pat)) of
+    true ->
+      Tree = refold_concrete_pat(cerl:concrete(Pat)),
+      [{label, Label}] = cerl:get_ann(Tree),
+      cerl:set_ann(Tree, [{label, Label}|cerl:get_ann(Pat)]);
+    false -> Pat
+  end.
+
+find_map(#{}) -> true;
+find_map(Tuple) when is_tuple(Tuple) -> find_map(tuple_to_list(Tuple));
+find_map([H|T]) -> find_map(H) orelse find_map(T);
+find_map(_) -> false.
+
+refold_concrete_pat(Val) ->
+  case Val of
+    _ when is_tuple(Val) ->
+      Els = lists:map(fun refold_concrete_pat/1, tuple_to_list(Val)),
+      case lists:all(fun cerl:is_literal/1, Els) of
+	true -> cerl:abstract(Val);
+	false -> label(cerl:c_tuple_skel(Els))
+      end;
+    [H|T] ->
+      case  cerl:is_literal(HP=refold_concrete_pat(H))
+	and cerl:is_literal(TP=refold_concrete_pat(T))
+      of
+	true -> cerl:abstract(Val);
+	false -> label(cerl:c_cons_skel(HP, TP))
+      end;
+    M when is_map(M) ->
+      %% Map patterns are not generated by the parser(!), but they have a
+      %% property we want, namely that they are never folded into literals.
+      %% N.B.: The key in a map pattern is an expression, *not* a pattern.
+      label(cerl:c_map_pattern([cerl:c_map_pair_exact(cerl:abstract(K),
+						      refold_concrete_pat(V))
+				|| {K, V} <- maps:to_list(M)]));
+    _ ->
+      cerl:abstract(Val)
+  end.
+
+label(Tree) ->
+      %% Sigh
+      Label = -erlang:unique_integer([positive]),
+      cerl:set_ann(Tree, [{label, Label}]).
+
+%%------------------------------------------------------------------------------
+
 -spec parallelism() -> integer().
 
 parallelism() ->