6

我根据本教程创建了下面的代码片段。最后两行 (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).
4

2 回答 2

5

尽量减少这个例子，我有这两个版本：

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 无法知道传递的闭包是否在函数中实际被调用。

如果使用该选项，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（它们从未承诺会找到所有错误）会好得多。

警告：以下是深奥的部分！

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

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

于 2012-08-10T10:40:03.363 回答
3

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

“Normal”成熟的类型检查器的优点是类型检查是可确定的。当类型检查器终止时，我们可以询问“这个程序的类型是否正确”并返回是或否。透析器不是这样。它本质上是在解决停机问题。结果是会有一些明显错误的程序，但仍然会从透析器的控制中溜走。

但是，这不是其中一种情况:)

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

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

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

可以想象透析器的未来变体，它解释了每个呼叫站点都可以单独处理的事实。由于透析器会随着时间的推移而发生变化，因此将来它可能能够处理这种情况。但目前，这是会漏掉的错误之一。

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

于 2012-08-08T09:42:44.640 回答