[erlang-questions] Dialyzer questions

[Kostis Sagonas]

Prashanth Mundkur wrote:
> We've recently been getting the upcoming release of Disco to go through 
> the Dialyzer wringer, and it has been a very useful exercise.  Thanks to 
> Kostis' helpful wielding of the cluebat at the SF Erlang Factory!
> 
> We are trying to understand the following output (I hope the inline code 
> pasting below comes out readable):

You already figured out some answers to your questions, but let me also 
reply to them for completeness and hopefully also for more explanations.

> $ cat dial.erl
> -module(dial).
> -export([abort/2, extract/2,
>          diskspace/1, monitor_diskspace/2, refresh_tags/1, 
> monitor_launch/0]).
> 
> % We have helper functions like this:
> abort(Msg, Code) ->
>     error_logger:warning_report(Msg),
>     exit(Code).
> % which give rise to the following dialyzer message:
> %
> %   Function abort/2 only terminates with explicit exception
> % How do we interpret this message?

First of all note that you do not get this warning by default. You only 
get this warning because you explicitly enabled the -Werror_handling
option.  I quote from the manual:

   -Werror_handling ***
      Include warnings for functions
      that only return by means of an exception.

You can suppress this warning by adding a spec of the form:

    -spec abort(some_type(), some_other_type()) -> no_return().

for this function, which will notify dialyzer that it is indeed your 
intention that this function will never return a value


> % Even with a plt that includes stdlib, there is no warning for the
> % following code:
> -spec extract(binary(), nonempty_string()) -> 'ok'.
> extract(Pack, Dir) ->
>     case zip:extract(Pack, [{cwd, Dir}]) of
>         {ok, Files} ->
>             Files;
>         {error, Reason} ->
>             exit({error, Reason})
>     end.

This happens because module 'zip' does not have -spec information about 
its functions.  Without such information, dialyzer's analysis infers 
that zip:extract/2 will either return something of the form {ok, term()} 
or {error, term()}.  Note that the only thing that dialyzer can infer 
given this information is that Files will be some term().  Your spec 
promises is that this term is 'ok'.  In such cases, where dialyzer 
cannot find any reason not to trust you, it keeps its mouth shut about 
it.  (Unless you use option -Woverspecs in this case.)

Now, it's actually the case that I have a spec-ed version of zip.erl 
which has not made it into OTP yet and in that version I get the 
following warning in your code:

    Invalid type specification for function dial:extract/2.
    The success typing is (binary() | string(),binary() | string()) ->
	[binary() | string() | {binary() | string(),binary()}]

I will see whether this version can be included as in OTP or not...


> % Here, the spawn_link of monitor_diskspace in monitor_launch() gives:
> %   The created fun has no local return
> % whereas the spawn_link of refresh_tags doesn't.  If the spawn_link
> % of monitor_diskspace() function is commented out, there is no
> % warning.  It's not clear how to interpret the warning or the
> % inconsistency.
> %
> % Converting the nested list comprehension in monitor_diskspace into a
> % list:map made the warning go away, at the expense of readability and
> % perhaps even efficiency.

You are right. There is some inconsistency in the behavior of the two 
cases. But note that the funs that are created have no return -- they 
both call functions that go into an infinite loop and actually they are 
explicitly spec-ed as no returning. So the warning you get is correct. 
Still, you would like the two cases to be consistent and ideally also 
not get this warning, if possible. (So that you do not have to resort to 
calls outside this module as e.g. using lists:map/2.)

We spend some time with Stavros today looking into this and Stavros has 
come up with a way of making sure the treatment of these two cases is 
consistent and the one you want. When such specs are in place for 
functions that go into infinite loops, the warnings for uses of them in 
funs are suppressed.

Stay tuned and Stavros' patch will soon find its place to an OTP version 
near you!

Hope this explains all issues,

Kostis

> -type diskinfo() :: {non_neg_integer(), non_neg_integer()}.
> -spec diskspace(nonempty_string()) -> {'ok', diskinfo()} | {'error', 
> term()}.
> diskspace(Path) ->
>     case Path of
>         "a" -> {ok, {0,0}};
>         _ -> {error, error}
>     end.
> 
> -spec monitor_diskspace(nonempty_string(),
>                         [{diskinfo(), nonempty_string()}]) ->
>                                no_return().
> monitor_diskspace(Root, Vols) ->
>     Df = fun(VolName) ->
>                  diskspace(filename:join([Root, VolName]))
>          end,
>     NewVols = [{Space, VolName}
>                || {VolName, {ok, Space}}
>                       <- [{VolName, Df(VolName)}
>                           || {_OldSpace, VolName} <- Vols]],
>     monitor_diskspace(Root, NewVols).
> 
> -spec refresh_tags(nonempty_string()) ->
>     no_return().
> refresh_tags(Root) ->
>     {ok, _} = diskspace(Root),
>     refresh_tags(Root).
> 
> monitor_launch() ->
>     spawn_link(fun() -> refresh_tags("abc") end),
>     spawn_link(fun() -> monitor_diskspace("root", [{{0,0}, "a"}]) end).
> 
> $ dialyzer --get_warnings -Wunmatched_returns -Werror_handling dial.erl 
>   Checking whether the PLT /home/mundkur/.dialyzer_plt is up-to-date... yes
>   Proceeding with analysis...
> dial.erl:6: Function abort/2 only terminates with explicit exception
> dial.erl:66: The created fun has no local return