2

我的代码类似于：

     if conditionA(x, y, z) then doA()
else if conditionB(x, y, z) then doB()
...
else if conditionZ(x, y, z) then doZ()
else throw ShouldNeverHappenException

我想验证两件事（使用静态分析）：

  1. 如果所有条件conditionA, conditionB, ..., conditionZ都是互斥的（即不可能同时有两个或多个条件为真）。
  2. 涵盖了所有可能的情况，即永远不会调用“else throw”语句。

你能给我推荐一个工具和/或我可以（轻松）做到这一点的方法吗？

我希望获得比“使用 Prolog”或“使用 Mathematica”更详细的信息...... ;-)

更新：

假设conditionA, conditionB, ..., conditionZ是（纯）函数，并且 x、y、z 具有“原始”类型。

4

4 回答 4

2

您想要做的第 1 项是文体问题。即使条件不是排他性的，该程序也有意义。就个人而言，作为静态分析工具的作者，我认为用户会得到足够多的误报，而不会试图强加他们的风格（而且由于另一个程序员会故意编写重叠条件，所以对于其他程序员来说，你问的将是误报） . 这就是说，有些工具是可配置的：对于其中一个，您可以编写一条规则，说明当遇到此构造时，案例必须是排他的。正如 Jeffrey 所建议的那样，您可以将代码包装在一个上下文中，在该上下文中计算一个布尔条件，如果没有重叠，则该条件为真，然后检查该条件。

第 2 项不是样式问题：您想知道是否可以引发异常。

这个问题在理论上和实践中都很困难，因此工具通常会放弃正确性（如果有问题永远不会发出警告）或完整性（永远不会警告非问题）中的至少一个。如果变量的类型是无界整数，可计算性理论会指出，分析器不可能既正确又完整，并且对所有输入程序都终止。但理论足够了。有些工具既放弃了正确性又放弃了完整性，这并不意味着它们也没有用处。

一个正确的工具示例是Frama-C的值分析：如果它说一个语句（例如 elseif 序列中的最后一个 case）不可达，你就知道它不可达。它是不完整的，所以当它没有说最后一条语句不可访问时，你不知道。

一个完整的工具示例是Cute：它使用所谓的concolic方法自动生成测试用例，旨在实现结构化覆盖（也就是说，它或多或少会试探性地尝试生成激活最后一个用例的测试。其他人已被采取）。因为它会生成测试用例（每个测试用例都是在其上实际执行代码的单个、明确的输入向量），所以它永远不会对非问题发出警告。这就是完整的意思。但是它可能无法找到导致到达最后一条语句的测试用例，即使有一个：它不正确。

于 2010-04-21T20:40:29.253 回答
1

这似乎与求解一个 NP-hard 的 3-sat 方程同构。不幸的是，静态分析器不太可能试图覆盖这个领域。

于 2010-04-21T19:25:11.243 回答
1

在一般情况下，正如@Michael Donohue 指出的那样，这是一个 NP 难题。

但是，如果您只有合理数量的条件要检查，您可以编写一个程序来检查所有条件。

for (int x = lowestX; x <= highestX; x++)
    for (int y ...)
      for (int z ...)
      {
          int conditionsMet = 0;
          if conditionA(x, y, z) then conditionsMet++;
          if conditionB(x, y, z) then  conditionsMet++;
          ... 
          if conditionZ(x, y, z) then  conditionsMet++;
          if (conditionsMet != 1)
              PrintInBlinkingRed("Found an exception!", x, y, z)
      }
于 2010-04-21T19:33:11.600 回答
1

假设您的条件是布尔值谓词 X、Y、Z 上的布尔表达式（和/或/不是），您的问题很容易通过符号布尔评估引擎解决。

关于它们是否涵盖所有情况的问题是通过对所有条件进行析取并询问是否是重言式来回答的。王的算法很好地做到了这一点。

关于它们是否相交的问题是成对回答的；对于公式 a 和 b，象征性地构造 a & b == false 并再次应用 Wang 的重言式检验。

我们使用DMS Software Reengineering Toolkit对 C 中的预处理器条件执行类似的布尔值计算（部分评估）。DMS 提供解析源代码的能力（如果您打算在大型代码库中执行此操作和/或随着时间的推移不断地修改程序），提取程序片段，象征性地组合它们，然后应用重写规则（执行布尔简化或算法，如 Wang 的）。

于 2010-04-22T07:40:11.120 回答