Strange Dialyzer behavior when matching record fields with opaque types

classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Strange Dialyzer behavior when matching record fields with opaque types

Nick Marino-2
Hi all,

I recently encountered a rather strange, unexpected Dialyzer error. I'm unsure if this might be considered a Dialyzer bug, or if I'm just missing some key piece of knowledge that would help me understand what's going on here.

I took the code that generated the warning and pruned it down down to this:

-module(opaque_weirdness).
-export([public_func/0]).

-record(a, {
    d = dict:new() :: dict:dict()
}).

-record(b, {
    q = queue:new() :: queue:queue()
}).

public_func() ->
    add_element(#b{}, my_key, my_value).

add_element(#a{d = Dict}, Key, Value) ->
    dict:store(Key, Value, Dict);
add_element(#b{q = Queue}, Key, Value) ->
    queue:in({Key, Value}, Queue).

Which yields the following warning when I run it through Dialyzer:

opaque_weirdness.erl:16: The attempt to match a term of type #b{q::queue:queue(_)} against the pattern {'a', Dict} breaks the opaqueness of queue:queue(_)

It seems like this warning is somehow being triggered by the presence of the unused function clause in add_element. If I modify the code and add a line to public_func so that we use both clauses, then Dialyzer passes with no warnings.

If I modify the above code to use tagged tuples instead of records (i.e. {dict, Dict} instead of #a{d = Dict}) then it gives a completely different warning, which makes much more sense to me:

opaque_weirdness.erl:10: The pattern <{'queue', Queue}, Key, Value> can never match the type <{'dict',dict:dict(_,_)},'my_key','my_value'>

So the use of records seems to be necessary to trigger the opaqueness warning, though I can't fathom why this should matter.

In the original example code, can anyone explain why Dialyzer is giving a warning about opaqueness instead of producing a "pattern X can never match the type Y" warning? The opaqueness warning seems really bizarre to me; obviously the term will never match the pattern, so how is opaqueness being broken?

Thanks,
Nick Marino

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Strange Dialyzer behavior when matching record fields with opaque types

Kostis Sagonas-2
On 01/17/2017 11:18 PM, Nick Marino wrote:

>
> I recently encountered a rather strange, unexpected Dialyzer error. I'm
> unsure if this might be considered a Dialyzer bug, or if I'm just
> missing some key piece of knowledge that would help me understand what's
> going on here.
>
> I took the code that generated the warning and pruned it down down to this:
>
> -module(opaque_weirdness).
> -export([public_func/0]).
>
> -record(a, {
>     d = dict:new() :: dict:dict()
> }).
>
> -record(b, {
>     q = queue:new() :: queue:queue()
> }).
>
> public_func() ->
>     add_element(#b{}, my_key, my_value).
>
> add_element(#a{d = Dict}, Key, Value) ->
>     dict:store(Key, Value, Dict);
> add_element(#b{q = Queue}, Key, Value) ->
>     queue:in({Key, Value}, Queue).
>
> Which yields the following warning when I run it through Dialyzer:
>
> opaque_weirdness.erl:16: The attempt to match a term of type
> #b{q::queue:queue(_)} against the pattern {'a', Dict} breaks the
> opaqueness of queue:queue(_)
>
> It seems like this warning is somehow being triggered by the presence of
> the unused function clause in add_element. If I modify the code and add
> a line to public_func so that we use both clauses, then Dialyzer passes
> with no warnings.

Your analysis is pretty correct.  The issue is related to dead code and
the warning you get is indeed confusing and weird.  This should be fixed
in dialyzer.  Till then, you can suppress it either by commenting the
unused first clause, which is dead code in your module, or by exporting
function add_element/3.


What roughly happens here is that Dialyzer gets confused by the fact
that the first clause will not be used and marks its arguments as having
the type none(), i.e. not contributing to the inferred success typing.
Then the warning pass sees the none() in the first argument of the
clause and thinks it has been produced due to the call to add_element
being with a record with a different opaque subterm: these opacity
violations are also denoted by/resulting in the none() type.  But the
pattern matching failure is on the #a{} vs. #b{} level, not on their
subterms (fields).

Dialyzer _should_ issue a warning for this line, but the correct warning
to issue here is something along the lines of:

opaque_weirdness.erl:16: The attempt to match a term of type
#b{q::queue:queue(_)} against the pattern {'a', Dict} will not succeed

or that this clause will not be used since the success typing arguments
of this function are (#b{}, _, _)

Kostis
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Strange Dialyzer behavior when matching record fields with opaque types

Nick Marino-2
Hi Kostis,

Thanks for the quick and helpful response! Glad I'm not crazy after all :). That all makes sense, and in my original use case that uncovered this, I'm fine with just commenting out the unused code for now.

I also just uncovered a related(?) issue, in case anyone is interested: in my example code, I found that changing #b{} to #a{} in the call to add_element actually causes Dialyzer to crash. Here's the error message:

Proceeding with analysis...{"init terminating in do_boot",{function_clause,[{dialyzer,message_to_string,[{opaque_match,["pattern <{'b', Queue}, Key, Value>","<#a{d::dict:dict(_,_)},'my_key','my_value'>"]}],[{file,"dialyzer.erl"},{line,310}]},{dialyzer,format_warning,2,[{file,"dialyzer.erl"},{line,300}]},{dialyzer_cl,'-print_warnings/1-lc$^0/1-0-',2,[{file,"dialyzer_cl.erl"},{line,818}]},{dialyzer_cl,print_warnings,1,[{file,"dialyzer_cl.erl"},{line,818}]},{dialyzer_cl,return_value,2,[{file,"dialyzer_cl.erl"},{line,715}]},{dialyzer_cl,do_analysis,4,[{file,"dialyzer_cl.erl"},{line,405}]},{dialyzer,'-cl/1-fun-0-',1,[{file,"dialyzer.erl"},{line,153}]},{dialyzer,doit,1,[{file,"dialyzer.erl"},{line,243}]}]}}

I'm tempted to try and debug this myself, but I'm not sure I have the necessary skills and background to safely make changes to a tool like Dialyzer. Figured I should leave this one to the experts ;). (Though if anyone with more experience than myself would like to point me in the right direction, I suppose I could take a stab at it - I just don't want to accidentally end up breaking something I don't understand.)

Anyway, thanks again!
Nick

On Tue, Jan 17, 2017 at 6:07 PM, Kostis Sagonas <[hidden email]> wrote:
On 01/17/2017 11:18 PM, Nick Marino wrote:

I recently encountered a rather strange, unexpected Dialyzer error. I'm
unsure if this might be considered a Dialyzer bug, or if I'm just
missing some key piece of knowledge that would help me understand what's
going on here.

I took the code that generated the warning and pruned it down down to this:

-module(opaque_weirdness).
-export([public_func/0]).

-record(a, {
    d = dict:new() :: dict:dict()
}).

-record(b, {
    q = queue:new() :: queue:queue()
}).

public_func() ->
    add_element(#b{}, my_key, my_value).

add_element(#a{d = Dict}, Key, Value) ->
    dict:store(Key, Value, Dict);
add_element(#b{q = Queue}, Key, Value) ->
    queue:in({Key, Value}, Queue).

Which yields the following warning when I run it through Dialyzer:

opaque_weirdness.erl:16: The attempt to match a term of type
#b{q::queue:queue(_)} against the pattern {'a', Dict} breaks the
opaqueness of queue:queue(_)

It seems like this warning is somehow being triggered by the presence of
the unused function clause in add_element. If I modify the code and add
a line to public_func so that we use both clauses, then Dialyzer passes
with no warnings.

Your analysis is pretty correct.  The issue is related to dead code and the warning you get is indeed confusing and weird.  This should be fixed in dialyzer.  Till then, you can suppress it either by commenting the unused first clause, which is dead code in your module, or by exporting function add_element/3.


What roughly happens here is that Dialyzer gets confused by the fact that the first clause will not be used and marks its arguments as having the type none(), i.e. not contributing to the inferred success typing. Then the warning pass sees the none() in the first argument of the clause and thinks it has been produced due to the call to add_element being with a record with a different opaque subterm: these opacity violations are also denoted by/resulting in the none() type.  But the pattern matching failure is on the #a{} vs. #b{} level, not on their subterms (fields).

Dialyzer _should_ issue a warning for this line, but the correct warning to issue here is something along the lines of:

opaque_weirdness.erl:16: The attempt to match a term of type #b{q::queue:queue(_)} against the pattern {'a', Dict} will not succeed

or that this clause will not be used since the success typing arguments of this function are (#b{}, _, _)

Kostis


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Strange Dialyzer behavior when matching record fields with opaque types

Kostis Sagonas-2
On 01/18/2017 05:24 PM, Nick Marino wrote:

> Hi Kostis,
>
> Thanks for the quick and helpful response! Glad I'm not crazy after all
> :). That all makes sense, and in my original use case that uncovered
> this, I'm fine with just commenting out the unused code for now.
>
> I also just uncovered a related(?) issue, in case anyone is interested:
> in my example code, I found that changing #b{} to #a{} in the call to
> add_element actually causes Dialyzer to crash. Here's the error message:
>
> Proceeding with analysis...{"init terminating in
> do_boot",{function_clause,[{dialyzer,message_to_string,[{opaque_match,["pattern
> <{'b', Queue}, Key,
> Value>","<#a{d::dict:dict(_,_)},'my_key','my_value'>"]}],[{file,"dialyzer.erl"},{line,310}]},{dialyzer,format_warning,2,[{file,"dialyzer.erl"},{line,300}]},{dialyzer_cl,'-print_warnings/1-lc$^0/1-0-',2,[{file,"dialyzer_cl.erl"},{line,818}]},{dialyzer_cl,print_warnings,1,[{file,"dialyzer_cl.erl"},{line,818}]},{dialyzer_cl,return_value,2,[{file,"dialyzer_cl.erl"},{line,715}]},{dialyzer_cl,do_analysis,4,[{file,"dialyzer_cl.erl"},{line,405}]},{dialyzer,'-cl/1-fun-0-',1,[{file,"dialyzer.erl"},{line,153}]},{dialyzer,doit,1,[{file,"dialyzer.erl"},{line,243}]}]}}
>
> I'm tempted to try and debug this myself, but I'm not sure I have the
> necessary skills and background to safely make changes to a tool like
> Dialyzer. Figured I should leave this one to the experts ;)

Thanks again for reporting this issue, which I can reproduce.  One can
easily avoid the crash by the following patch:

================================================================
diff --git a/lib/dialyzer/src/dialyzer.erl b/lib/dialyzer/src/dialyzer.erl
index d25ffd0..d5352fd 100644
--- a/lib/dialyzer/src/dialyzer.erl
+++ b/lib/dialyzer/src/dialyzer.erl
@@ -438,6 +438,8 @@ message_to_string({opaque_guard, [Arg1, Infix, Arg2,
ArgNs]}) ->
  message_to_string({opaque_guard, [Guard, Args]}) ->
    io_lib:format("Guard test ~w~s breaks the opacity of its argument\n",
                 [Guard, Args]);
+message_to_string({opaque_match, [Pat, Term]}) ->
+  io_lib:format("The ~s can never match the term ~s\n", [Pat, Term]);
  message_to_string({opaque_match, [Pat, OpaqueType, OpaqueTerm]}) ->
    Term = if OpaqueType =:= OpaqueTerm -> "the term";
             true -> OpaqueTerm
================================================================

which produces the following warning in your example program:

opaque_weirdness.erl:13: The pattern <{'b', Queue}, Key, Value> can
never match the term <#a{d::dict:dict(_,_)},'my_key','my_value'>


However, this patch is sub-optimal.  Similarly to the previous issue you
reported the core of the problem is that dialyzer erroneously classifies
the problem as opaque-related, which is not.  It's a simple case of dead
code (a clause that will never match) and the warning should be tagged
with 'pattern_match' instead of 'opaque_match' or, better yet, simply
say that the 2nd clause is unused (cannot match).

I will leave this issue to the responsible developer at Ericsson to
handle properly.

Kostis



PS. The test case is:

-module(opaque_weirdness).
-export([public_func/0]).

-record(a, {d = dict:new() :: dict:dict()}).

-record(b, {q = queue:new() :: queue:queue()}).

public_func() ->
     add_element(#a{}, my_key, my_value).

add_element(#a{d = Dict}, Key, Value) ->
     dict:store(Key, Value, Dict);
add_element(#b{q = Queue}, Key, Value) ->
     queue:in({Key, Value}, Queue).

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions