为什么透析器没有发现这个代码是错误的?



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

教程中提供了说明:

在使用错误类型的馈线调用函数之前,它们是 首先用正确的类型打电话。截至R15B01,透析器不会 查找此代码的错误。观察到的行为是,只要尽快 当对给定函数的调用在函数的主体中成功时, 透析器将忽略同一代码单元中以后的错误。

这种行为的理由是什么?我知道成功打字背后的哲学是"永不狼来了",但在当前的情况下,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).

最小化示例相当多,我有两个版本:

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

-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).

透析器对它可以捕获的版本发出的警告是:

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() -> bamboofun() -> 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将首先仅用FeederSquid进行细化,并且肯定会返回sperm_whale,然后用FeederSquidFeederRP进行细化并返回sperm_whale OR bamboo。然后使用 FeederRP 调用时,成功键入的预期返回值为 sperm_whale OR bamboo 。然后规范承诺它将sperm_whale,透析器接受它。另一方面,论证应该是fun() -> bamboo | sperm_whale成功的类型,它是fun() -> bamboo的,所以只剩下fun() -> bamboo。当根据规范(fun() -> sperm_whale)进行检查时,Dialyzer假设该参数可以fun() -> none()。如果您从未在feed_squid/1内调用传递的函数(Dialyzer的类型系统不会将其保留为信息),并且您在规范中承诺将始终返回sperm_whale,那么一切都很好!

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

(注意,我在这里有点猜测。我没有详细阅读透析器代码)。

"普通"成熟的类型检查器具有类型检查是可判定的优点。我们可以询问"这个程序类型是否正确",并在类型检查器终止时得到"是"或"否"。透析器则不然。它本质上是在解决停止问题。结果是,将会有一些程序是公然错误的,但仍然从透析器的夹具中溜走。

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

问题是双重的。成功类型表示"如果此函数正常终止,其类型是什么?在上面,我们的 feed_red_panda/1 函数终止任何参数匹配fun (() -> A)任意类型 A 。我们可以打电话给feed_red_panda(fun erlang:now/0),它也应该有效。因此,我们对 main/0 函数的两次调用不会引起问题。他们都终止了。

问题的第二部分是"你违反了规范吗?请注意,通常,透析器中不使用规格。它推断类型本身并使用推理模式而不是您的规范。每当调用函数时,都会使用参数对其进行注释。在我们的例子中,它将用两种生成器类型进行注释: food(red_panda()), food(squid()) .然后根据这些注释进行函数局部分析,以确定您是否违反了规范。由于注释中存在正确的参数,因此我们必须假设该函数在代码的某些部分中正确使用。它也与鱿鱼一起调用,可能是由于其他情况而从未调用的代码的工件。因为我们是函数局部的,所以我们不知道,并给程序员怀疑的好处。

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

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

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

相关内容

  • 没有找到相关文章

最新更新