为什么Dialyzer没有发现此代码错误？

Question

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

教程中提供了解释:

在使用错误的馈线调用函数之前,首先使用正确的类型调用它们.从R15B01开始,Dialyzer不会在此代码中发现错误.观察到的行为是,只要对函数体内的给定函数的调用成功,Dialyzer就会忽略同一代码单元中的后续错误.

这种行为的理由是什么？我理解成功打字背后的哲学是"从不哭狼",但在目前的情况下,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

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

Dialyzer 可以捕获的第一个：

-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()(一个会崩溃的闭包，如果不在 内调用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（无论如何它从未承诺找到所有错误），那会好得多。

警告：深奥部分如下！

之所以在第一种情况下报错误而第二种情况不报错误，与模块局部细化的进度有关。最初，该函数feed_squid/1已成功输入(fun() -> any()) -> any()。在第一种情况下，函数feed_squid/1将首先仅使用 改进，FeederRP并且肯定会返回bamboo，立即伪造规范并停止进一步分析main/0. 在第二个中，函数feed_squid/1将首先仅使用FeederSquidand进行细化，肯定会返回sperm_whale，然后使用FeederSquidandFeederRP和返回sperm_whaleOR进行细化bamboo。当然后使用FeederRP预期的返回值调用时，成功类型为sperm_whaleOR并且 Dialyzer 接受它。另一方面，论证应该是bamboo。然后规范承诺它将是sperm_whalefun() -> bamboo | sperm_whale成功类型的，fun() -> bamboo所以只剩下fun() -> bamboo. 当根据规范 ( fun() -> sperm_whale)进行检查时，Dialyzer 假定参数可能是fun() -> none()。如果您从不调用内部传递的函数feed_squid/1（Dialyzer 的类型系统不会将其作为信息保留的内容），并且您在规范中承诺您将始终返回sperm_whale，那么一切都很好！

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

Answer 2

（注意，我在这里推测了一下。我还没有详细阅读透析器代码）。

“普通”成熟的类型检查器的优点是类型检查是可判定的。我们可以询问“这个程序的类型是否正确”，并在类型检查器终止时得到“是”或“否”。对于透析器来说并非如此。它本质上是为了解决停机问题。结果是有些程序明显错误，但仍然逃脱了透析器的控制。

然而，这不是其中之一:)

问题有两个方面。成功类型表示“如果这个函数正常终止，它的类型是什么？”。在上面，我们的feed_red_panda/1函数因任何匹配fun (() -> A)任意类型的参数而终止A。我们可以打电话feed_red_panda(fun erlang:now/0)，应该也可以。因此，我们对函数 in 的两次调用main/0不会产生问题。他们都终止了。

问题的第二部分是“你违反了规范吗？”。请注意，事实上，透析器中通常不使用规格。它本身推断类型并使用推断模式而不是您的规范。每当调用函数时，都会用参数进行注释。在我们的例子中，它将用两种生成器类型进行注释：food(red_panda()), food(squid())。然后根据这些注释进行函数本地分析，以确定您是否违反了规范。由于注释中存在正确的参数，因此我们必须假设该函数在代码的某些部分中使用正确。它也被鱿鱼调用可能是代码的产物，由于其他情况而永远不会被调用。由于我们是函数局部的，所以我们不知道并且给程序员带来了怀疑的好处。

如果您更改代码以仅使用鱿鱼生成器进行错误调用，那么我们就会发现规范差异。因为我们知道唯一可能的调用站点违反了规范。如果您将错误的调用移至另一个函数，也不会找到它。因为注释仍然在函数上而不是在调用站点上。

人们可以想象透析器的未来变体，它考虑到每个呼叫站点都可以单独处理的事实。由于透析器也会随着时间的推移而发生变化，因此它可能在未来能够处理这种情况。但目前，这是容易被忽视的错误之一。

关键是要注意透析器不能用作“类型正确的检查器”。您不能使用它来强制程序的结构。你需要自己做。如果您想要更多静态检查，可能可以为 Erlang 编写一个类型检查器并在部分代码库上运行它。但你会遇到代码升级和分发的麻烦，这不好处理。