Inconsistency between dialyzer's results when a module is in the PLT vs when it is included in the analysis

Question

Inconsistency between dialyzer's results when a module is in the PLT vs when it is included in the analysis

Opened this issue 9 years ago · 3 comments

On Friday, June 17, 2016 @kostis reported to @aronisstav and @uabboli an inconsistency between dialyzer's results when a module is in the plt vs when it is included in the analysis, detected when working with a branch that

"is essentially the current [no longer] 'master' which also adds some type declarations in the records of 'core_parse.hrl' and then uses these types in 'cerl.erl'. These two are the only files that differ. I am pretty sure all these type declarations are correct, but even if they are not, it is besides the point of the following."

I have rebased his branch on top of OTP-19.0 and pushed it at aronisstav/core_parse-types (currently at 6e5cd3f).

After some preliminary minimization, to see the issue follow these steps:

$ dialyzer --build_plt lib/hipe/ebin/erl_*types.beam lib/compiler/ebin/cerl.beam --apps stdlib
[...]
$ dialyzer --apps dialyzer
[...]
dialyzer_dataflow.erl:237: The pattern 'true' can never match the type 'false'
dialyzer_dataflow.erl:1265: The pattern 'true' can never match the type 'false'
dialyzer_dataflow.erl:3039: Function state__renew_race_list/3 has no local return
dialyzer_dataflow.erl:3041: The attempt to match a term of type dialyzer_races:races() against the variable _ breaks the opaqueness of the term
[...]
$ dialyzer --apps dialyzer stdlib
[...]
dialyzer_dataflow.erl:237: The pattern 'true' can never match the type 'false'
dialyzer_dataflow.erl:1265: The pattern 'true' can never match the type 'false'
dialyzer_dataflow.erl:3039: Function state__renew_race_list/3 has no local return
dialyzer_dataflow.erl:3041: The attempt to match a term of type dialyzer_races:races() against the variable _ breaks the opaqueness of the term
dialyzer_races.erl:208: The attempt to match a term of type dialyzer_dataflow:state() against the variable CleanState breaks the opaqueness of the term
dialyzer_races.erl:222: The attempt to match a term of type dialyzer_dataflow:state() against the variable CleanState breaks the opaqueness of the term
dialyzer_races.erl:248: The attempt to match a term of type dialyzer_dataflow:state() against the variable CleanState breaks the opaqueness of the term
dialyzer_races.erl:2375: The call dialyzer_dataflow:format_args(Args::['bypassed' | 'no_arg' | {'c_binary' | 'c_catch' | 'c_literal' | 'c_tuple' | 'c_values' | 'c_var',[any()],_} | {'c_alias' | 'c_apply' | 'c_case' | 'c_cons' | 'c_fun' | 'c_letrec' | 'c_primop' | 'c_seq',[any()],_,_} | {'c_call' | 'c_clause' | 'c_let' | 'c_map' | 'c_map_pair' | 'c_receive',_,_,_,_} | {'c_module',[any()],{'c_literal',[any()],atom() | bitstring() | [atom() | bitstring() | [any()] | number() | tuple() | map()] | number() | tuple() | map()},[{'c_var',[any()],atom() | integer() | {atom(),byte()}}],[{{'c_literal',[any()],atom() | bitstring() | [atom() | bitstring() | [any()] | number() | tuple() | map()] | number() | tuple() | map()},{'c_literal',[any()],atom() | bitstring() | [atom() | bitstring() | [any()] | number() | tuple() | map()] | number() | tuple() | map()}}],[{{'c_var',[any()],atom() | integer() | {atom(),byte()}},{'c_fun',[any()],[{'c_var',[any()],atom() | integer() | {atom(),byte()}}],_}}]} | {'c_bitstr',_,_,_,_,_,_} | {'c_try',_,_,_,_,_,_}],ArgTypes::[erl_types:erl_type()],State::dialyzer_dataflow:state()) does not have an opaque term of type dialyzer_dataflow:state() as 3rd argument
[...]

Since stdlib is included in the PLT, there shouldn't be a difference in the warnings one gets for dialyzer's files.

I am currently working on minimizing this further, by including less modules from stdlib.

Answer 1 · 2016-06-23T12:05:57.000Z

Currently working with this PLT:

$ dialyzer --build_plt lib/hipe/ebin/erl_*types.beam lib/compiler/ebin/cerl.beam

And running dialyzer like:

$ dialyzer lib/dialyzer/ebin/dialyzer_{dataflow,races}.beam lib/stdlib/ebin/<some>.beam

If <some> is * then the second sets of warnings comes up. Now trying to trigger it with less.

Answer 2 · 2016-06-23T12:16:57.000Z

Smallest set that produces the warnings:

$ dialyzer lib/dialyzer/ebin/dialyzer_{dataflow,races}.beam lib/stdlib/ebin/{dict,erl_parse,erl_anno}.beam

Answer 3 · 2016-06-23T12:21:10.000Z

Reproduced original issue with smaller PLT:

$ dialyzer --build_plt lib/hipe/ebin/erl_*types.beam lib/compiler/ebin/cerl.beam lib/stdlib/ebin/{dict,erl_parse,erl_anno}.beam
[...]
$ dialyzer lib/dialyzer/ebin/dialyzer_{dataflow,races}.beam
[...]
dialyzer_dataflow.erl:237: The pattern 'true' can never match the type 'false'
dialyzer_dataflow.erl:1265: The pattern 'true' can never match the type 'false'
dialyzer_dataflow.erl:3039: Function state__renew_race_list/3 has no local return
dialyzer_dataflow.erl:3041: The attempt to match a term of type dialyzer_races:races() against the variable _ breaks the opaqueness of the term
[...]
$ dialyzer lib/dialyzer/ebin/dialyzer_{dataflow,races}.beam lib/stdlib/ebin/erl_anno.beam
[...]
dialyzer_dataflow.erl:237: The pattern 'true' can never match the type 'false'
dialyzer_dataflow.erl:1265: The pattern 'true' can never match the type 'false'
dialyzer_dataflow.erl:3039: Function state__renew_race_list/3 has no local return
dialyzer_dataflow.erl:3041: The attempt to match a term of type dialyzer_races:races() against the variable _ breaks the opaqueness of the term
dialyzer_races.erl:208: The attempt to match a term of type dialyzer_dataflow:state() against the variable CleanState breaks the opaqueness of the term
dialyzer_races.erl:222: The attempt to match a term of type dialyzer_dataflow:state() against the variable CleanState breaks the opaqueness of the term
dialyzer_races.erl:248: The attempt to match a term of type dialyzer_dataflow:state() against the variable CleanState breaks the opaqueness of the term
dialyzer_races.erl:2375: The call dialyzer_dataflow:format_args(Args::['bypassed' | 'no_arg' | {'c_binary' | 'c_catch' | 'c_literal' | 'c_tuple' | 'c_values' | 'c_var',[any()],_} | {'c_alias' | 'c_apply' | 'c_case' | 'c_cons' | 'c_fun' | 'c_letrec' | 'c_primop' | 'c_seq',[any()],_,_} | {'c_call' | 'c_clause' | 'c_let' | 'c_map' | 'c_map_pair' | 'c_receive',_,_,_,_} | {'c_module',[any()],{'c_literal',[any()],atom() | bitstring() | [atom() | bitstring() | [any()] | number() | tuple() | map()] | number() | tuple() | map()},[{'c_var',[any()],atom() | integer() | {atom(),byte()}}],[{{'c_literal',[any()],atom() | bitstring() | [atom() | bitstring() | [any()] | number() | tuple() | map()] | number() | tuple() | map()},{'c_literal',[any()],atom() | bitstring() | [atom() | bitstring() | [any()] | number() | tuple() | map()] | number() | tuple() | map()}}],[{{'c_var',[any()],atom() | integer() | {atom(),byte()}},{'c_fun',[any()],[{'c_var',[any()],atom() | integer() | {atom(),byte()}}],_}}]} | {'c_bitstr',_,_,_,_,_,_} | {'c_try',_,_,_,_,_,_}],ArgTypes::[erl_types:erl_type()],State::dialyzer_dataflow:state()) does not have an opaque term of type dialyzer_dataflow:state() as 3rd argument
[...]

Notice that for the full set to appear only erl_anno.beam needs to be analyzed together with dialyzer's files.