多个if语句（条件）的静态分析

Question

我的代码类似于：

     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 具有“原始”类型。

Answer 1

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

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

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

正确的工具示例是 Frama-C 的价值分析：如果它说某个陈述（例如由于 elseifs) 序列中的最后一个情况无法访问，因此您知道它无法访问。它不完整，所以当它没有说最后一条语句不可达时，你就不知道。

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

Answer 2

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

Answer 3

在一般情况下，正如 @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)
      }

Answer 4

假设您的条件是布尔值谓词 X、Y、Z 上的布尔表达式（和/或/不是），则可以使用符号布尔求值引擎轻松解决您的问题。

关于它们是否涵盖所有情况的问题可以通过对所有条件进行析取并询问是否是同义反复来回答。 Wang 的算法很好地做到了这一点。

关于它们是否相交的问题是成对回答的；对于公式a和b，
象征性地构造 a & b == false 并再次应用 Wang 的同义反复测试。

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