erlang - 为什么 Dialyzer 没有发现这段代码错误？

Question

我根据 this 创建了下面的代码片段教程。最后两行(feed_squid(FeederRP) 和 feed_red_pa​​nda(FeederSquid))显然违反了定义的约束，但 Dialyzer 发现它们没问题。这非常令人失望，因为这正是我想用执行静态分析的工具捕获的错误类型。

教程中提供了解释:

Before the functions are called with the wrong kind of feeder, they're first called with the right kind. As of R15B01, Dialyzer would not find an error with this code. The observed behaviour is that as soon as a call to a given function succeeds within the function's body, Dialyzer will ignore later errors within the same unit of code.

这种行为的理由是什么？我知道成功输入背后的理念是“永远不要喊狼来了”，但在当前场景中，Dialyzer 明显忽略了有意定义的函数规范(在它看到函数之前已被正确调用之后)。据我所知，该代码不会导致运行时崩溃。我能否以某种方式强制 Dialyzer 始终认真对待我的功能规范？如果没有，有没有工具可以做到这一点？

-module(zoo).
-export([main/0]).

-type red_panda() :: bamboo | birds | eggs | berries.
-type squid() :: sperm_whale.
-type food(A) :: fun(() -> A).

-spec feeder(red_panda) -> food(red_panda());
            (squid) -> food(squid()).
feeder(red_panda) ->
    fun() ->
            element(random:uniform(4), {bamboo, birds, eggs, berries})
    end;
feeder(squid) ->
    fun() -> sperm_whale end.

-spec feed_red_panda(food(red_panda())) -> red_panda().
feed_red_panda(Generator) ->
    Food = Generator(),
    io:format("feeding ~p to the red panda~n", [Food]),
    Food.

-spec feed_squid(food(squid())) -> squid().
feed_squid(Generator) ->
    Food = Generator(),
    io:format("throwing ~p in the squid's aquarium~n", [Food]),
    Food.

main() ->
    %% Random seeding
    <<A:32, B:32, C:32>> = crypto:rand_bytes(12),
    random:seed(A, B, C),
    %% The zoo buys a feeder for both the red panda and squid
    FeederRP = feeder(red_panda),
    FeederSquid = feeder(squid),
    %% Time to feed them!
    feed_squid(FeederSquid),
    feed_red_panda(FeederRP),
    %% This should not be right!
    feed_squid(FeederRP),
    feed_red_panda(FeederSquid).

Answer 1

将示例最小化，我有这两个版本:

透析器可以捕获的第一个:

-module(zoo).
-export([main/0]).

-type red_panda_food() :: bamboo.
-type squid_food()     :: sperm_whale.

-spec feed_squid(fun(() -> squid_food())) -> squid_food().
feed_squid(Generator) -> Generator().

main() ->
    %% The zoo buys a feeder for both the red panda and squid
    FeederRP = fun() -> bamboo end,
    FeederSquid = fun() -> sperm_whale end,
    %% CRITICAL POINT %%
    %% This should not be right!
    feed_squid(FeederRP),
    %% Time to feed them!
    feed_squid(FeederSquid)

然后是没有警告的:

    [...]
    %% CRITICAL POINT %%
    %% Time to feed them!
    feed_squid(FeederSquid)
    %% This should not be right!
    feed_squid(FeederRP).

Dialyzer 对于它可以捕获的版本的警告是:

zoo.erl:7: The contract zoo:feed_squid(fun(() -> squid_food())) -> squid_food() cannot be right because the inferred return for feed_squid(FeederRP::fun(() -> 'bamboo')) on line 15 is 'bamboo'
zoo.erl:10: Function main/0 has no local return

...这是一个更愿意相信自己的判断而不是用户更严格的规范的情况。

对于它没有捕获的版本，Dialyzer 假定 feed_squid/1参数类型 fun() -> bamboo是 fun() -> none() 的父类(super class)型(一个会崩溃的闭包，如果不在 feed_squid/1 内调用，它仍然是一个有效的参数)。推断出类型后，Dialyzer 无法知道传递的闭包是否实际上在函数内被调用。

如果选项-Woverspecs，透析器仍会发出警告使用:

zoo.erl:7: Type specification zoo:feed_squid(fun(() -> squid_food())) -> squid_food() is a subtype of the success typing: zoo:feed_squid(fun(() -> 'bamboo' | 'sperm_whale')) -> 'bamboo' | 'sperm_whale'

...警告没有任何东西可以阻止此函数处理其他馈线或任何给定的馈线!如果该代码确实检查了闭包的预期输入/输出，而不是通用的，那么我很确定 Dialyzer 会捕获滥用行为。从我的角度来看，如果您的实际代码检查错误输入，而不是依赖类型规范和 Dialyzer(无论如何它从未 promise 找到所有错误)，那就更好了。

警告:深奥的部分如下!

第一种情况报错而第二种情况不报错的原因与模块局部细化的进度有关。最初的功能feed_squid/1已成功输入(fun() -> any()) -> any() 。在第一种情况下，函数 feed_squid/1首先将仅使用 FeederRP 进行细化并且一定会返回bamboo ，立即伪造规范并停止对 main/0 的进一步分析。在第二个中，函数 feed_squid/1首先将仅使用 FeederSquid 进行细化并且一定会返回sperm_whale ，然后用 FeederSquid 进行细化和FeederRP并返回sperm_whale或bamboo 。然后用 FeederRP 调用时成功输入的预期返回值是 sperm_whale或bamboo 。然后规范 promise 它将是 sperm_whale透析器接受它。另一方面，参数应该是 fun() -> bamboo | sperm_whale就成功打字而言，它是 fun() -> bamboo这样就只剩下 fun() -> bamboo 。当根据规范( fun() -> sperm_whale )进行检查时，Dialyzer 假定参数可能是 fun() -> none() 。如果您从未在 feed_squid/1 内调用传递的函数(Dialyzer 的类型系统不会将其保留为信息)，并且您在规范中 promise 将始终返回 sperm_whale ，一切都很好!

可以“修复”的是类型系统可以扩展为在调用中实际使用作为参数传递的闭包时进行注释，并在“生存”某些部分的唯一方法的情况下发出警告类型推断为 fun(...) -> none() .