Dialyzer does not report errors when module having abstraction violation on opaque type.

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

Dialyzer does not report errors when module having abstraction violation on opaque type.

by
Hi,

I am trying to do some exercises on opaque type, the dialyzer should report error on below code, but it does not.

%% opaque1.erl
-module(opaque1).

-export_type([test_text/0]).

-opaque test_text() :: [{atom(), number()}].

-export([make_text/0]).

-spec make_text() -> test_text().

make_text() ->
    [{a,1}, {c,3}].

%% opaque2.erl
-module(opaque2).

-export([test/0]).

test() ->
    X = opaque1:make_text(),
    [F || {F, _} <- X]. % This violates the abstraction of opaque type from module opaque1.

Run dialyzer on these two modules will produce:
%%%%
MacBookPro:dialyzer by$ dialyzer opaque1.erl 
  Checking whether the PLT /Users/by/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis... done in 0m0.12s
done (passed successfully)
MacBookPro:dialyzer by$ 
%%%%

%%%%
MacBookPro:dialyzer by$ dialyzer opaque2.erl 
  Checking whether the PLT /Users/by/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
Unknown functions:
  opaque1:make_text/0
 done in 0m0.13s
done (passed successfully)
MacBookPro:dialyzer by$ 
%%%%

My Erlang/OTP version is: OTP-22.1.4

Am I missing something?

Kind Regards,
Yao
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer does not report errors when module having abstraction violation on opaque type.

zxq9-2
On 2019/12/28 16:25, by wrote:
 > %% opaque1.erl
 > -module(opaque1).
 > -export_type([test_text/0]).
 > -opaquetest_text() :: [{atom(), number()}].
 > -export([make_text/0]).
 >
 > -spec make_text() ->test_text().
 >
 > make_text() ->
 >      [{a,1}, {c,3}].

[snip]

 > %% opaque2.erl
 > -module(opaque2).
 > -export([test/0]).
 >
 > test() ->
 >     X = opaque1:make_text(),
 >     [F||{F, _} <- X]. % This violates the abstraction
 >
 > Run dialyzer on these two modules will produce:
 > %%%%
 > MacBookPro:dialyzer by$ dialyzer opaque1.erl
 >    Checking whether the PLT /Users/by/.dialyzer_plt is up-to-date... yes
 >    Proceeding with analysis... done in 0m0.12s
 > done (passed successfully)
 > MacBookPro:dialyzer by$
 > %%%%
 >
 > %%%%
 > MacBookPro:dialyzer by$ dialyzer opaque2.erl
 >    Checking whether the PLT /Users/by/.dialyzer_plt is up-to-date... yes
 >    Proceeding with analysis...
 > Unknown functions:
 >    opaque1:make_text/0
 >   done in 0m0.13s
 > done (passed successfully)
 > MacBookPro:dialyzer by$
 > %%%%
 >
 > Am I missing something?
Two things:
1- You need to dialyze BOTH modules in the same run or else Dialyzer
cannot see the typespecs in opaque1.erl while it is evaluating opaque2.erl
2- You can write code that violates opaque types, though I believe
Dialyzer will issue a warning about it if you evaluate both at once.

-Craig
by
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer does not report errors when module having abstraction violation on opaque type.

by
Yes, you are right.

I get the warning after evaluate both modules at the same time.

The warning is:
%%%%
MacBookPro:dialyzer by$ dialyzer opaque1.erl opaque2.erl 
  Checking whether the PLT /Users/by/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
opaque2.erl:5: Function test/0 has no local return
opaque2.erl:7: The created fun has no local return
opaque2.erl:7: The attempt to match a term of type 
          opaque1:test_text() against the pattern 
          [{F, _} | _] breaks the opacity of the term
opaque2.erl:7: The attempt to match a term of type 
          opaque1:test_text() against the pattern 
          [] breaks the opacity of the term
opaque2.erl:7: Fun application with arguments 
         (X :: opaque1:test_text()) will never return since it differs in the 1st argument from the success typing arguments: 
         ([any()])
 done in 0m0.17s
done (warnings were emitted)
MacBookPro:dialyzer by$ 
%%%%

Thank you!

Kind Regards,
Yao

在 2019年12月28日,16:43,zxq9 <[hidden email]> 写道:

On 2019/12/28 16:25, by wrote:

> %% opaque1.erl
> -module(opaque1).
> -export_type([test_text/0]).
> -opaquetest_text() :: [{atom(), number()}].
> -export([make_text/0]).
>
> -spec make_text() ->test_text().
>
> make_text() ->
>      [{a,1}, {c,3}].

[snip]

> %% opaque2.erl
> -module(opaque2).
> -export([test/0]).
>
> test() ->
>     X = opaque1:make_text(),
>     [F||{F, _} <- X]. % This violates the abstraction
>
> Run dialyzer on these two modules will produce:
> %%%%
> MacBookPro:dialyzer by$ dialyzer opaque1.erl
>    Checking whether the PLT /Users/by/.dialyzer_plt is up-to-date... yes
>    Proceeding with analysis... done in 0m0.12s
> done (passed successfully)
> MacBookPro:dialyzer by$
> %%%%
>
> %%%%
> MacBookPro:dialyzer by$ dialyzer opaque2.erl
>    Checking whether the PLT /Users/by/.dialyzer_plt is up-to-date... yes
>    Proceeding with analysis...
> Unknown functions:
>    opaque1:make_text/0
>   done in 0m0.13s
> done (passed successfully)
> MacBookPro:dialyzer by$
> %%%%
>
> Am I missing something?
Two things:
1- You need to dialyze BOTH modules in the same run or else Dialyzer cannot see the typespecs in opaque1.erl while it is evaluating opaque2.erl
2- You can write code that violates opaque types, though I believe Dialyzer will issue a warning about it if you evaluate both at once.

-Craig