控制敏感性对于推理由程序中的分支引起的关系属性是不足够的。以下是一个典型的例子:
if (condition) {
open();
flag = 1;
} else {
flag = 0;
}
...
if (flag) {
close();
}
在这里,我们假设open和close是用于打开和关闭特定文件的内置函数。(使用第11章介绍的技术可以处理涉及多个文件的更实际的情况。)文件最初是关闭的,condition是一些复杂的表达式,“...”由不调用open或close或修改flag的语句组成。我们希望设计一种分析,可以检查只有在文件当前处于打开状态时才调用close,只有在文件当前处于关闭状态时才调用open,并且在程序退出时文件肯定是关闭的。在这个示例程序中,关键属性是只有在先前执行中包含调用open的分支被执行后,才会执行包含调用close的分支。
作为上述分析的开始,我们用如下的集合的幂集合元素作为格的元素,从而对open/close进行建模:
$$ L = \mathcal{P}(\{ \text{open},\text{closed} \}) $$
格的偏序关系是集合的$\subseteq$ 关系。例如,格的元素"{open}"表示文件肯定没有关闭,而"{open; closed}"表示文件的状态未知。对于每个控制流图节点v,变量$[[v]]$表示节点后程序点处文件的可能状态。对于open和close语句,约束条件如下:
$$ [[\text{open()}]] = \text{\{open\}} $$
$$ [[\text{close()}]] = \text{\{closed\}} $$
对于入口节点,
$$ [[entry]] = \text{\{closed\}} $$
对于每一个其他的节点,因为都没有改变文件的状态,因此约束就是之前的JOIN
$$ JOIN(v) = \bigcup_{w \in pred(v)}~[[w]] $$
在示例程序中,close函数显然只有在open被调用的情况下才会被调用,但当前的分析未能发现这一点。
上述程序具有所需的属性显然涉及到标志变量,而上面的格并没有考虑。因此,我们可以尝试使用一个稍微复杂的格子 - 一个由两个幂集格的乘积格组成,用于跟踪文件的状态和标志的值:
格的偏序关系隐含地定义为两个幂集的分量子集排序。例如,右侧子格中的格元素$\{flag \neq 0\}$表示标志绝对不是0,$\{flag \neq 0, flag = 0\}$表示标志的值是未知的。此外,我们需要插入assert语句来模拟条件:
if (condition) {
assert(condition);
open();
flag = 1;
} else {
assert(!condition);
flag = 0;
}
...
if (flag) {
assert(flag);
close();
} else {
assert(!flag);
}
然而,这样也不够。在第一个if-else语句结束的位置,分析的结果是open可能被调用,flag的值可能为0。
当前的分析也被称为独立属性分析,因为文件的抽象值与布尔标志的抽象值无关。我们需要的是一种可以跟踪变量之间关系的关系分析。实现这一点的一种方法是通过将分析推广到每个程序点维护多个抽象状态。如果L是如上定义的原始格,那么我们将其替换为映射格: