[erlang-questions] why can't dialyzer see that my spec is a lie?

[Kostis Sagonas]

Matthias Lang wrote:
> Hi,
> 
> Running the example below through dialyzer R14B01:
> 
>   143> dialyzer:run([{from, src_code}, {files, ["minimal.erl"]}]). 
>   []
> 
> I was hoping Dialyzer would complain that my spec (line 18) is a lie.
> 
> Cut down, but compilable, code below. Changing "almost anything" results
> in a good warning, e.g. if I comment out the recursive step (line 13):
> 
>   145> dialyzer:run([{from, src_code}, {files, ["minimal.erl"]}]).
>   [{warn_contract_types,{"/tmp/minimal.erl",17},
>                       {extra_range,[minimal,parse_and_execute,1,"'quit'",
>                                     "{_,_}"]}}]
> 
> What's going on? I'm stumped.

In program analysis tools one needs to choose between soundness for 
correctness (i.e., find all errors and then some) and soundness for 
defect detection (i.e., find only true discrepancies but raise no false 
alarms).

Dialyzer has opted for the latter, which means that it can occasionally 
fail to report some discrepancies between the code and its intended uses 
(as documented for example in programmer-supplied specs). That's what's 
happening here.

In your program, dialyzer infers a return type of any() for your 
parse_and_execute/1 function and cannot see that it is invalid 
(actually, even the warning you get when you do the change you suggest 
in your mail is not the "right" one).  I think this happens because it 
does not propagate information about closures across functions, esp. 
when an infinite loop is involved as in your program.

We will look at this issue (thanks for reporting it) and try to fix it 
in a future dialyzer version.

Kostis

> ----------------------------------------------------------------------
> -module(minimal).
> -export([start/0]).
> 
> -record(state, {commands}).
> 
> start() ->
>     Fun = fun() -> {quit, "string"} end,
>     server_loop(#state{commands=Fun}).
> 
> server_loop(State) ->
>     try
> 	{New_state, _} = parse_and_execute(State),
> 	server_loop(New_state)
>     catch
> 	_:_ -> ok
>     end.
> 
> -spec parse_and_execute(any()) -> {#state{}, string()} | 'quit'.
> 
> parse_and_execute(State) ->
>     Fun = State#state.commands,
>     Fun().
> 
> 
> 
> ________________________________________________________________
> erlang-questions (at) erlang.org mailing list.
> See http://www.erlang.org/faq.html
> To unsubscribe; mailto:erlang-questions-unsubscribe@REDACTED