Coverity 无法报告无限循环缺陷

Question

如果我传入值为 0 的除数，我将遵循具有潜在无限循环的 Java 代码。但是 Coverity 不能为我报告这个错误。

class InfinityLoopExample {
  public int div(final int dividend, final int divisor)  {
    int ret = 0;
    int x = dividend;
    while (x > divisor) {
      x = x - divisor;
      ret++;
    }
    return ret;
  }
}

//And following code to actually call that method i.e. in main.
//This will make sure infinite loop real happens
final InfinityLoopExample infinityLoopExample = new InfinityLoopExample();
final int ret1 = infinityLoopExample.div(3,0);
System.out.println("infinityLoopExample.div:" + ret1);

从以下coverity 链接可以清楚地看出，coverity 可以在其静态代码分析期间报告此类错误： https://cwe.mitre.org/data/definitions/835.html

我对上面的 Java 代码运行了覆盖代码扫描，它不能报告无限循环问题。有没有人对 Java 项目进行过覆盖代码扫描可以提供一些启示？

P.S 我有大小为 151K 的覆盖构建日志文件。如果需要，我可以发布。

Answer 1

作为最初在 2010 年左右我为 Coverity 工作时设计 INFINITE_LOOP 检查器的两个人之一（我不再这样做了），我可以说一下为什么这可能不会被报告，尽管我不能详细介绍，因为这涉及 Coverity（现为 Synopsys）的专有知识产权。

首先，必须认识到 Coverity 不会报告任何给定缺陷类型的所有实例。这与halting problem 的不确定性有关；全自动静态分析在数学上不可能完全准确。此外，大多数 Coverity 检查器旨在报告不超过 20% 的误报，为此，它要求代码在愿意报告之前包含相当有力的问题证据。

函数div 没有包含足够有力的问题证据，因为divisor 不应该作为零传入是合理的。相反，如果它包含类似if (divisor==0) {...} 的内容，那将成为应该容忍零参数的有力证据。当然，这不是该工具识别的唯一证据。如果您添加了这样的代码，其中包含逻辑内部矛盾的明确证据，而检查器仍然没有报告，那么我建议将该示例报告给 Coverity 支持团队。

现在，除了div，您的示例还包括一个呼叫站点：

final int ret1 = infinityLoopExample.div(3,0);

基于此，divisor 显然可以为零，对吧？是的——但现在您可能遇到了这个特定检查器的限制。

让我们暂时转移一下，与另一个检查器 FORWARD_NULL 进行比较，它是负责报告 null 取消引用问题的主要检查器。 FORWARD_NULL 不会报告这个：

int deref(MyClass c) { return c.someField; }

如果c 为空，方法deref 将抛出NullPointerException，但我们没有证据表明c 曾经为空。但是，FORWARD_NULL 认识到了这种可能性，因此它记得deref 无条件地取消引用它的参数。稍后如果它看到如下调用站点：

deref(null);

然后它将报告该呼叫站点。

但是，INFINITE_LOOP 没有，或者至少在最初设计时没有类似的机制。如果它找不到足够的理由来报告包含函数内的循环，那么它不会报告，无论调用站点可能发生什么。

向 Coverity 团队提出增强请求，以这种方式扩展 INFINITE_LOOP 的检测能力并非没有道理。但是，如果您这样做，我强烈建议您提交调用代码更真实的代码。 Coverity 是否遗漏了您的实际生产代码中的真正缺陷？提交那个。 Coverity 设计理念的另一个元素是强调真实代码的准确性，而不是人为的示例，因为两者有许多重要的差异，分析非常敏感。