Dialyzer and raise exception behavior

Fl4m3Ph03n1x

Background

I have a very minimalistic function that can return a boolean or blow up:

defmodule TestDialzer do

  @spec hello(integer) :: boolean
  def hello(n) do

    if n == 10 do
      true
    else
      raise "This is not a number!"
    end

  end
end

As you can see, this function can return a boolean. But it can also not return one. Dialyzer is not picking this up:

Starting Dialyzer
[
  check_plt: false,
  init_plt: '/home/pedro/Workplace/test_dialzer/_build/dev/dialyxir_erlang-23.3_elixir-1.12.0_deps-dev.plt',
  files: ['/home/pedro/Workplace/test_dialzer/_build/dev/lib/test_dialzer/ebin/Elixir.TestDialzer.beam'],
  warnings: [:unknown]
]
Total errors: 0, Skipped: 0, Unnecessary Skips: 0
done in 0m0.77s
done (passed successfully)

My spec is incomplete and I expected dialyzer to fail with some kind of error / warning.

Questions

Why is dialyzer not complaining? (rare thing to ask, I know)

12 comments

#dialyzer

0 1814 12

2021-06-09 09:01:38 UTC

Showing Posts 1 to 10

Show Best Posts
Show All (oldest first)
Show All (newest first)

kokolegorille

I had a similar question…

Post #1

al2o3cr

A function can be specced as no_return, but that’s only applicable if it never returns a value.

Otherwise the “can fail” is implied for all functions - for instance, :math.sqrt/1 has a spec of sqrt(number) :: float, but it gives an ArithmeticError when called with a negative input.

Post #2

Fl4m3Ph03n1x

@peerreynders did find a solution for the issue in your thread right?
However I was not able to understand it quite well …

@al2o3cr I am confused, then what is the point of having ! (bang) functions, if all of them can simply explode whenever they feel like?

Post #3

kokolegorille

The solution proposed was to have smaller functions with correct type…

For example, hello_success and hello_error, of type boolean.

Post #4

Fl4m3Ph03n1x

The solution was to “not raise” at all, correct ?

Post #5

kokolegorille

Whatever You choose to return from an error will be catched if it does not specify the right type for the error return, in the smaller function. While your hello function could not, because dialyzer assume it is correctly typed as boolean in case of success, and does not care about the error path.

Post #6

Fl4m3Ph03n1x

I am sorry but I still dont quite understand.

defmodule TestDialzer do
  @moduledoc """
  Documentation for `TestDialzer`.
  """

  @spec hello(integer) :: boolean
  def hello(n) do

    if n == 10 do
      true
    else
      raise "This is not a number!"
    end

  end

  @spec test_hello_1 :: boolean
  def test_hello_1, do: hello(10)

  @spec test_hello_2 :: boolean
  def test_hello_2, do: hello(1)
end

In this example, test_hello_2 will clearly fail. Dialyzer should be able to prove this is wrong. Yet it passes.
I don’t understand how this can be fixed…

Post #7

michallepicki

Dialyzer should be able to prove this is wrong

Should, based on what exactly?

Dialyzer doesn’t do dependent typing. And it only does a limited amount of data flow analysis, since it is highly computationally and memory intensive. Maybe in this particular case it seems easy and intuitive, but a generalized algorithm that would perform these kinds of checks is not trivial.

AFAIK individual integers (like 10, 1) are not distinguishable by Dialyzer.

Post #8

michallepicki

If you let dialyzer infer specs for your functions, it will tell you that the hello (and other functions) return true. You can enable checking of your provided specs against those by using the overspecs, underspecs or the combinded specdiffs options. But beware that this may introduce a lot of noise: warnings when you don’t want them, where dialyzer hits his limits and simplifies types, or you intentionally simplify types, e.g. for documentation purposes.

Post #9