代码之家 › 专栏 › 技术社区 › kopper

多个if语句(条件)的静态分析

boolean-logic static-analysis math language-agnostic

2

kopper · 技术社区 · 15 年前

我的代码类似于:

     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

我想验证两件事(使用静态分析):

如果所有条件 conditionA, conditionB, ..., conditionZ 相互排斥(即两个或多个条件不可能同时成立)。
所有可能的情况都包括在内,即“else throw”语句永远不会被调用。

你能给我推荐一个工具和/或一种我能(容易)做到的方法吗?

我希望比“使用prolog”或“使用mathematica”更详细的信息…;-)

更新:

假设 条件A,条件B,…,条件Z are(纯)函数和x,y,z有“原始”类型。

4 回复 | 直到 15 年前

1

2

Pascal Cuoq 15 年前

项目1。你想做的是一个文体问题。即使条件不是唯一的,程序也有意义。就我个人而言,作为静态分析工具的作者,我认为用户在不强制样式的情况下得到足够多的假警报(而且由于另一个程序员会故意编写重叠条件,所以您所要求的是假警报)。这就是说,有些工具是可配置的:对于其中一个工具,您可以编写一个规则,说明遇到此构造时,案例必须是排他的。根据jeffrey的建议,可以将代码包装在一个上下文中,在该上下文中计算一个布尔条件,如果没有重叠,则为true,并检查该条件。

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

这个问题在理论和实践上都很难解决,所以工具通常会放弃至少一个 正确性 (如果存在问题,请务必发出警告)或 完备性 (不要警告没有问题)。如果变量的类型是无界整数,可计算性理论将指出,对于所有输入程序,分析器不能既正确又完整,并且不能终止。但理论已经足够了。有些工具放弃了正确性和完整性,这并不意味着它们也没有用处。

正确的工具示例如下 Frama-C 价值分析:如果它说一个语句(比如elseif序列中的最后一个case)是不可到达的,那么您知道它是不可到达的。它不是完整的,所以当它没有说最后一个语句是不可达的,你就不知道了。

一个完整的工具示例是 Cute :它使用所谓的 concolic 自动生成测试用例的方法,以结构覆盖为目标(也就是说,它或多或少会尝试生成在所有其他用例都被执行后激活最后一个用例的测试)。因为它生成测试用例(每个测试用例都是执行代码的一个确定的输入向量),所以它从不警告没有问题。这就是完整的意义。但是它可能找不到导致最后一条语句到达的测试用例,即使有一条语句:它是不正确的。

2

1

Michael Donohue Reno 15 年前

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

3

1

Jeffrey L Whitledge 15 年前

在一般情况下,这是一个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)
      }

4

1

Ira Baxter 15 年前

假设您的条件是布尔值谓词x、y、z上的布尔表达式(和/或不是),那么您的问题很容易用符号布尔求值引擎解决。

关于它们是否涵盖所有情况的问题,答案是对所有条件进行析取,并询问是否是重言式。王的算法做得很好。

关于它们是否相交的问题是成对回答的;对于公式A和B, 象征性地构造a&b==false并再次应用王的重言式测试。

我们用了 DMS Software Reengineering Toolkit 为了在c.dms中的预处理器条件上执行类似的布尔值计算(部分求值),可以解析源代码(如果您打算跨大型代码库和/或随着时间的推移反复修改程序,则这一点很重要),提取程序fragments,象征性地组合它们,然后应用重写规则(执行布尔简化或像wang的算法)。