Dialyzer success type question

[Sebastian Strollo-2]

Hi

Apologizes for quoting Kostis out of context,

On 12/6/10 8:56 , Kostis Sagonas wrote:
...
 > Yes. As you see, dialyzer is not only smart but is also quite sensitive!
 > If it ever feels neglected for too long, it has a very effective way of
 > letting you know that you should never do that again ;-)

Not only that, it seems to suffer from mood swings between releases :-)

We offer up our code to Dialyzers scrutiny several times a day, and are
happy to do so. However when upgrading to R14B01 we ran into a bit of
problem with Dialyzers concept of success typing, as it seems to have
changed in R14B01?

Here is a minimal example of my problem, with two modules, first:

   -module(m1).
   -export([do_something/0]).
   do_something() ->
       io:format("doing something...\n", []),
       m2:fail(true, "Failed: ...\n", []).

and the other module:

   -module(m2).
   -export([fail/3]).
   fail(HaltP, Fmt, Args) ->
       io:format(standard_error, Fmt, Args),
       case HaltP of
           true ->
               erlang:halt(1);
           false ->
               ok
       end.

Now, if I kindly ask dialyzer to analyze this I get:

   m1.erl:3: Function do_something/0 has no local return

Which I expect, and I can turn it off if I wish by using -Wno_return (or
spec:ing that I know it doesn't return). However, I also get:

   m1.erl:5: The call m2:fail('true',"Failed: ...\n",[]) will never
return since it differs in the 1st argument from the success typing
arguments: ('false',atom() | binary() | [any()],[any()])

Which is a problem, since there is no way for me to turn it off, also it
seems a bit inconsistent, if I change the case clause in fail/3 to:

     case HaltP of
         true ->
             erlang:halt(1);
         _ ->
             ok
     end.

I do not get the above message (even though I guess dialyzer could
figure out that the "success typing" is "anything *but* true:-). It
doesn't seem to help to spec me out of this, even if I spec my intent by:

-spec fail(boolean(), string(), [any()]) -> 'ok' | no_return().

I still get the complaint (as long as I have 'false' in the case clause).

Any hints on how I can appease dialyzer and let it know that I don't
expect my fail function to return when I tell it not to?

Thanks,

/Sebastian

--
Sebastian Strollo / [hidden email]
Tail-f Systems   / www.tail-f.com


________________________________________________________________
erlang-questions (at) erlang.org mailing list.
See http://www.erlang.org/faq.html
To unsubscribe; mailto:[hidden email]

[Kostis Sagonas-2]

Sebastian Strollo wrote:
> Hi
>
> Apologizes for quoting Kostis out of context,

No problem! First of all, for a researcher it's always nice to be cited,
  but independently of this, your post is very interesting. Hence the
long reply.

> On 12/6/10 8:56 , Kostis Sagonas wrote:
> ...
>  > Yes. As you see, dialyzer is not only smart but is also quite sensitive!
>  > If it ever feels neglected for too long, it has a very effective way of
>  > letting you know that you should never do that again ;-)
>
> Not only that, it seems to suffer from mood swings between releases :-)

Well, what can I say? dialyzer has a mind of its own and it's certainly
possible that such mood swings can happen, but that's not what's
happening here. Instead, it's just that dialyzer is getting smarter ;-)

Seriously, what's happening is the following. For a long time now we are
aware that dialyzer is occasionally failing to report some warnings.
More specifically, in some cases dialyzer reports that a certain
function has no local return (meaning some call will fail/halt/exit
within its body) but does not report the culprit. When these are calls
to functions that do not have a success typing (i.e., all their paths
are throws, errors, etc.) it's obviously very easy to see the problem,
but in cases where functions return something in some control flow paths
and not in others it can be extremely frustrating to spot the reason for
the no return. We are slowly identifying/fixing these cases so that
warnings are reported in these cases.

Please, do send me cases where no local return warnings are reported
without an obvious reason.

> We offer up our code to Dialyzers scrutiny several times a day, and are
> happy to do so. However when upgrading to R14B01 we ran into a bit of
> problem with Dialyzers concept of success typing, as it seems to have
> changed in R14B01?
>
> Here is a minimal example of my problem, with two modules, first:
>
>   -module(m1).
>   -export([do_something/0]).
>   do_something() ->
>       io:format("doing something...\n", []),
>       m2:fail(true, "Failed: ...\n", []).
>
> and the other module:
>
>   -module(m2).
>   -export([fail/3]).
>   fail(HaltP, Fmt, Args) ->
>       io:format(standard_error, Fmt, Args),
>       case HaltP of
>           true ->
>               erlang:halt(1);
>           false ->
>               ok
>       end.
>
> Now, if I kindly ask dialyzer to analyze this I get:
>
>   m1.erl:3: Function do_something/0 has no local return
>
> Which I expect, and I can turn it off if I wish by using -Wno_return (or
> spec:ing that I know it doesn't return). However, I also get:
>
>   m1.erl:5: The call m2:fail('true',"Failed: ...\n",[]) will never
> return since it differs in the 1st argument from the success typing
> arguments: ('false',atom() | binary() | [any()],[any()])
>
> Which is a problem, since there is no way for me to turn it off, also it
> seems a bit inconsistent, if I change the case clause in fail/3 to:
>
>     case HaltP of
>         true ->
>             erlang:halt(1);
>         _ ->
>             ok
>     end.
>
> I do not get the above message (even though I guess dialyzer could
> figure out that the "success typing" is "anything *but* true:-).

Aside: you are very much right in this, but dialyzer does not have a
notion of "negative types", at least not yet.

> It doesn't seem to help to spec me out of this, even if I spec my intent by:
>
> -spec fail(boolean(), string(), [any()]) -> 'ok' | no_return().
>
> I still get the complaint (as long as I have 'false' in the case clause).
>
> Any hints on how I can appease dialyzer and let it know that I don't
> expect my fail function to return when I tell it not to?

Before I answer your question, allow me one more comment regarding the
spec. The return type 'ok' | no_return() does not make much sense. (It
is anyway equivalent to 'ok'.) Also, as you can see, in this case
dialyzer *knows* that this function will only return given 'false' in
its first argument, so putting boolean() in the spec will not fool dialyzer.


Here is what you can do. Of course I do not know the big picture of your
application, but to me it does not make much sense to have a hard-coded
'true' in the first argument of the call to this function.

I would instead create these two functions:

   fail_and_halt(Fmt, Args) ->
       io:format(standard_error, Fmt, Args),
       erlang:halt(1).

   fail_no_halt(Fmt, Args) ->
       io:format(standard_error, Fmt, Args),
       ok.

in the m2 module and change the call m2:fail(true, "Failed: ...\n", [])
to read m2:fail_and_halt("Failed: ...\n", []) instead. Now there is no
call to a function that sometimes returns (i.e. has a success typing)
and sometimes doesn't.


Kostis

________________________________________________________________
erlang-questions (at) erlang.org mailing list.
See http://www.erlang.org/faq.html
To unsubscribe; mailto:[hidden email]

[Gordon Guthrie-2]

Kostis

I am wrestling with dialyzer warnings at the moment.

> specifically, in some cases dialyzer reports that a certain function has no
> local return (meaning some call will fail/halt/exit within its body) but
> does not report the culprit.

With this warning Dialyzer 'seems' to be telling me that some function
calls will always fail, but when I run the actual code it passes...

> When these are calls to functions that do not
> have a success typing (i.e., all their paths are throws, errors, etc.)

Part of the problem is that I don't know what a 'sucess typing' is...

> but in cases where functions return
> something in some control flow paths and not in others it can be extremely
> frustrating to spot the reason for the no return. We are slowly
> identifying/fixing these cases so that warnings are reported in these cases.

> Please, do send me cases where no local return warnings are reported without
> an obvious reason.

I have tried tracking down a couple of these but it tends to get deep
in stack traces...

How much context would you need?

Gordon

On 15 December 2010 15:47, Kostis Sagonas <[hidden email]> wrote:

> Sebastian Strollo wrote:
>>
>> Hi
>>
>> Apologizes for quoting Kostis out of context,
>
> No problem! First of all, for a researcher it's always nice to be cited,
>  but independently of this, your post is very interesting. Hence the long
> reply.
>
>> On 12/6/10 8:56 , Kostis Sagonas wrote:
>> ...
>>  > Yes. As you see, dialyzer is not only smart but is also quite
>> sensitive!
>>  > If it ever feels neglected for too long, it has a very effective way of
>>  > letting you know that you should never do that again ;-)
>>
>> Not only that, it seems to suffer from mood swings between releases :-)
>
> Well, what can I say? dialyzer has a mind of its own and it's certainly
> possible that such mood swings can happen, but that's not what's happening
> here. Instead, it's just that dialyzer is getting smarter ;-)
>
> Seriously, what's happening is the following. For a long time now we are
> aware that dialyzer is occasionally failing to report some warnings. More
> specifically, in some cases dialyzer reports that a certain function has no
> local return (meaning some call will fail/halt/exit within its body) but
> does not report the culprit. When these are calls to functions that do not
> have a success typing (i.e., all their paths are throws, errors, etc.) it's
> obviously very easy to see the problem, but in cases where functions return
> something in some control flow paths and not in others it can be extremely
> frustrating to spot the reason for the no return. We are slowly
> identifying/fixing these cases so that warnings are reported in these cases.
>
> Please, do send me cases where no local return warnings are reported without
> an obvious reason.
>
>> We offer up our code to Dialyzers scrutiny several times a day, and are
>> happy to do so. However when upgrading to R14B01 we ran into a bit of
>> problem with Dialyzers concept of success typing, as it seems to have
>> changed in R14B01?
>>
>> Here is a minimal example of my problem, with two modules, first:
>>
>>  -module(m1).
>>  -export([do_something/0]).
>>  do_something() ->
>>      io:format("doing something...\n", []),
>>      m2:fail(true, "Failed: ...\n", []).
>>
>> and the other module:
>>
>>  -module(m2).
>>  -export([fail/3]).
>>  fail(HaltP, Fmt, Args) ->
>>      io:format(standard_error, Fmt, Args),
>>      case HaltP of
>>          true ->
>>              erlang:halt(1);
>>          false ->
>>              ok
>>      end.
>>
>> Now, if I kindly ask dialyzer to analyze this I get:
>>
>>  m1.erl:3: Function do_something/0 has no local return
>>
>> Which I expect, and I can turn it off if I wish by using -Wno_return (or
>> spec:ing that I know it doesn't return). However, I also get:
>>
>>  m1.erl:5: The call m2:fail('true',"Failed: ...\n",[]) will never return
>> since it differs in the 1st argument from the success typing arguments:
>> ('false',atom() | binary() | [any()],[any()])
>>
>> Which is a problem, since there is no way for me to turn it off, also it
>> seems a bit inconsistent, if I change the case clause in fail/3 to:
>>
>>    case HaltP of
>>        true ->
>>            erlang:halt(1);
>>        _ ->
>>            ok
>>    end.
>>
>> I do not get the above message (even though I guess dialyzer could figure
>> out that the "success typing" is "anything *but* true:-).
>
> Aside: you are very much right in this, but dialyzer does not have a notion
> of "negative types", at least not yet.
>
>> It doesn't seem to help to spec me out of this, even if I spec my intent
>> by:
>>
>> -spec fail(boolean(), string(), [any()]) -> 'ok' | no_return().
>>
>> I still get the complaint (as long as I have 'false' in the case clause).
>>
>> Any hints on how I can appease dialyzer and let it know that I don't
>> expect my fail function to return when I tell it not to?
>
> Before I answer your question, allow me one more comment regarding the spec.
> The return type 'ok' | no_return() does not make much sense. (It is anyway
> equivalent to 'ok'.) Also, as you can see, in this case dialyzer *knows*
> that this function will only return given 'false' in its first argument, so
> putting boolean() in the spec will not fool dialyzer.
>
>
> Here is what you can do. Of course I do not know the big picture of your
> application, but to me it does not make much sense to have a hard-coded
> 'true' in the first argument of the call to this function.
>
> I would instead create these two functions:
>
>  fail_and_halt(Fmt, Args) ->
>      io:format(standard_error, Fmt, Args),
>      erlang:halt(1).
>
>  fail_no_halt(Fmt, Args) ->
>      io:format(standard_error, Fmt, Args),
>      ok.
>
> in the m2 module and change the call m2:fail(true, "Failed: ...\n", []) to
> read m2:fail_and_halt("Failed: ...\n", []) instead. Now there is no call to
> a function that sometimes returns (i.e. has a success typing) and sometimes
> doesn't.
>
>
> Kostis
>
> ________________________________________________________________
> erlang-questions (at) erlang.org mailing list.
> See http://www.erlang.org/faq.html
> To unsubscribe; mailto:[hidden email]
>
>

--
Gordon Guthrie
CEO hypernumbers

http://hypernumbers.com
t: hypernumbers
[phone]

________________________________________________________________
erlang-questions (at) erlang.org mailing list.
See http://www.erlang.org/faq.html
To unsubscribe; mailto:[hidden email]