static-analysis - 通过静态分析检测缺少 if/else 语句

Question

我正在 try catch if 语句中缺少的未处理的 expressiong 条件。

第一个示例

if (a < 5) {
    // Do something
} else {
    // handled else condition
}

第二个示例

if (a < 5) {
    // Do something
} else if (a >= 5){
    // handled else if condition
}

这两个例子都是正确的，并且处理了所有可能性。

但是我正在尝试解决诸如

之类的条件

if ((a < 5) && b > 10) {
    // Do something
} else if ((a >= 5) && (b > 10)){
    // handled else condition
} else if((a < 5) && (b <= 10)) {
    // handled else condition
}

但是这个条件并不能处理所有的可能性，并且缺少

的条件

} else if ((a >= 5) && (b <= 10)) {
   // missing condition which is not handled
}

我正在尝试通过静态分析并使用源代码的抽象语法树来查找此类漏洞。有没有针对此类问题进行研究的算法、方法或论文？

Answer 1

如果你有类似的代码

if(A) { ... }
else if (B) { ... }
else if (C) { ... }

并且您想确保处理所有可能性，那么您必须证明公式 A or B or C始终评估为 true 。如果您所做的只是检查范围，那么我会将这个公式转换为 conjunctive normal form .

经过此转换，您将得到以下形式的公式

(F1 or F2 or ...) and (G1 or G2 or G3) and (H1 or H2 or H3) ...

其中每个原子命题的形式为 (x < c) , (x ≤ c) , (x > c)或(x ≥ c) ，其中x是一个变量并且 c是一个常数。这些命题可以通过使用以下转换来组合:

1. (x < c1)与 (x > c2) 一起转换为true如果(c1 > c2)
2. (x < c1)与 (x ≥ c2) 一起转换为true如果(c1 ≥ c2)
3. (x ≤ c1)与 (x > c2) 一起转换为true如果(c1 ≥ c2)
4. (x ≤ c1)与 (x ≥ c2) 一起转换为true如果(c1 ≥ c2)

现在看看子句(F1 or F2 or ...) 。一旦您能够执行这些转换之一，那么整个子句就有效，您可以开始检查下一个子句。

如果所有子句都有效，则处理所有可能性。

通用解决方案(其中 if 语句中的条件可以是任何内容)并不是那么简单。例如，如果您想检查 if(f(x) || g(x)) ，有可能f()或g()有副作用，或执行非常复杂的计算。