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 1822 12

2021-06-09 09:01:38 UTC

Showing Posts 12 to 3

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

Fl4m3Ph03n1x

defmodule TestDialzer do

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

    if n == 10 do
      hello_success()
    else
      hello_error()
    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)

  @spec hello_success :: true
  defp hello_success, do: true

  # This is clearly wrong, yet no complaining =(
  @spec hello_error :: boolean
  defp hello_error, do: raise "This is not a number!"

end

I am quite lost here. Dialyzer is not picking up that hello_error has an wrong spec.

Post #12

kokolegorille

The solution @peerreynders proposed in the similar question I had was to do something like this…

  def hello(n) do

    if n == 10 do
      hello_success()
    else
      hello_error()
    end

  end

This way You can detect type error in the smaller functions.

Here is the solution he provided in my question…

   cond do
     qty < 0     ->
       create_unit_quantity_error("unit_quantity can not be negative")
     qty > 1_000 ->
       create_unit_quantity_error("unit_quantity can not be more than 1000")
     true        ->
       create_unit_quantity_success(qty)
    end

Post #11

Fl4m3Ph03n1x

Should based on the fact that I have a public function with a direct flow that causes a spec error.

I understand finding paths is computationally intensive, I am not discussing that here.

Perhaps my question can be better rephrased as: How can I make dialyzer detect there is an issue? What code changes would I need to perform?

Post #10

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

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

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

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