Dialyzer should not throw away spec information because of overspec

[richcarl]

This fixes a problem where Dialyzer did not warn about the following situation, because it discarded information unnecessarily:

-spec f(integer()) -> ook | error.
f(1) -> ok;
f(2) -> error.

t(X) when is_integer(X) ->
    ok = f(X).  % quietly accepted

If the spec was simply missing an entry, you got a warning even without this fix:

-spec f(integer()) -> error.  % forgot to mention that 'ok' is valid
f(1) -> ok;
f(2) -> error.

t(X) when is_integer(X) ->
    ok = f(X).  % warns about invalid match

The extraneous information in the first case simply made Dialyzer forget that there was any spec at all.

[CLAassistant]

All committers have signed the CLA.

[richcarl]

Note that the changes to the test file chars.erl were necessary because with this patch, Dialyzer discovered that the example code in that module was totally bogus. :-)

(The chars.erl test file was introduced in https://bugs.erlang.org/browse/ERL-313)

[kostis]

This is clearly a step in the right direction, but the patch is not yet there, I think.

In dialyzer, there is a very fine line between something that is a clear improvement vs something that might be confusing (at least to some users) under some circumstances. Take a look at the warnings that dialyzer produces for beam_asm, for example. The current warnings are correct alright, but, if I am not mistaken --sorry, it has been a long day-- they fail to mention that it's actually the range of the beam_asm:encode/1 function that is not OK in the spec (as well as the type of the second argument), which is what triggered the two extra warnings with this patch. In such situations, I believe it's better for dialyzer to keep silent instead of presenting only half the truth, which may explain the rationale for the previous behavior. For example, the problems in the spec of this function are not fixed just by changing its second argument to integer() instead of pos_integer(). At least one more change/iteration is needed, right?

[richcarl]

It looks to me that the beam_asm warnings worked exactly as intended. The code has a problem: encode/2 is specced as taking a strictly positive integer in the second argument, but is in fact called with constants 0 from two call sites (and encode/2 even has a clause for handling negative inputs) - but Dialyzer previously missed reporting this, because it had thrown away the spec for the unrelated reason that encode/2 can return a naked integer in the second clause, which is outside the declared iodata() return type (not in itself worth a warning by default). So the warnings are not "triggered" by the range discrepancy - they were just previously being weirdly suppressed by it, and that if anything is the surprise to the user.

I'll fix the spec in beam_asm. The patch to dialyzer_contracts is not optimal, but I don't have time to make a bigger refactoring. The real issue is that the function check_contract/3 only answers a yes/no question, but is called in two different situations: to tell whether or not to warn about some aspect of a spec (the result of which is then filtered depending on user options), and to tell whether or not a spec may be used at all or is considered broken. The answers do not overlap completely, and the function should preferably have a more expressive api, rather than making the caller filter out particular known not-really-broken cases.

[uabboli]

We'll need a day or two to understand and fix the warnings in SSL. There is also a warning in os_mon (easily fixed).

[kostis]

It looks to me that the beam_asm warnings worked exactly as intended. The code has a problem: encode/2 is specced as taking a strictly positive integer in the second argument, but is in fact called with constants 0 from two call sites (and encode/2 even has a clause for handling negative inputs) - but Dialyzer previously missed reporting this, because it had thrown away the spec for the unrelated reason that encode/2 can return a naked integer in the second clause, which is outside the declared iodata() return type (not in itself worth a warning by default). So the warnings are not "triggered" by the range discrepancy - they were just previously being weirdly suppressed by it, and that if anything is the surprise to the user.

I disagree. I am almost certain that the warnings are triggered by the range discrepancy, because dialyzer discovers (or at least should discover) that this function does not return iodata() :: iolist() | binary() but just iolist().

This is exactly what I meant that there is some warning which is missing here, i.e. one that informs the user about the real discrepancy that triggered the extra (correct in this case) warnings. Your fixing the spec of this function erroneously in some sense (i.e., suboptimally) confirms my position, I would argue.

Please do not misunderstand me. As I wrote, this is a change in the right direction, but I do not think it's there yet. Unfortunately, I do not have time right now to look into how it can be improved.

[kostis]

Why merge? This is clearly incomplete! Even the spec of beam_asm was not fixed properly...