静态分析

理论上来说，静态分析问题是不可判定的（undecidable）；实际上，可以通过过度近似（over-approximation）来得到准确的单边答案，也就是可以保证假阴性和假阳性不会同时出现。

“程序状态”可以定义为：$\{label, store\_mapping\}$,也就是程序执行的位点与各个变量的值。

使 $U$ 为程序状态的全集，$B$ 为有问题的状态集合，$R$ 为可到达的状态集合。如果 $R$ 与 $B$ 不相交，那么说明该程序无法到达有问题的状态，故而没有问题。而如果有相交，则程序有问题（有 bug）。

$R$ 是不可判定的，因此无法通过静态分析确定程序是否有问题。但是可以通过计算 $R$ 的超集来“过度近似” $R$。这样，对于发现的问题，可能会出现假阳性；但如果没发现问题，可以确定肯定没有问题。

抽象解释是一种静态分析技术，它把程序内的值用抽象的描述符表示，并使用抽象的模拟器来解释运行程序。

两个函数：

• $\gamma()$ 将抽象的描述符具体化
• $\alpha()$ 将具体的值抽象化

对于一个具体的值 $c$，我们有：$\gamma(\alpha(c))\supseteq \{c\}$，这就是“过度近似”。

例子： 对于函数 $f(x,y) = (16y+3)\cdot(2x+1)$，是否存在自变量 $x, y$ 使得函数的输出值为 $51$ 或者 $10$？

我们可以将这里的值抽象为 $\{E,O,?\}$ 中的一个值，分别表示偶数、奇数与未知奇偶。基于这样的抽象，我们可以定义抽象运算规则：

抽象加法：

#+|	?	E	O
--+-----------------------
? |	?	?	?
E |	?	E	O
O |	?	O	E

抽象乘法：

#*|	?	E	O
--+-----------------------
? |	?	E	?
E |	E	E	E
O |	?	E	O

定义抽象运算后，自变量 $x, y$ 被抽象为 $?$，在经过抽象解释之后，我们可以得到 $f(x,y)=O$ 肯定是奇数。因此该函数的值不可能为 $10$，有可能是 $51$。