Yuheng 的学习分享 Wiki

本页面只读。您可以查看源文件，但不能更改它。如果您觉得这是系统错误，请联系管理员。
====== 静态分析 ======

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

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

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

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

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

两个函数：

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

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

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

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

抽象加法：
<code>
#+|	?	E	O
--+-----------------------
? |	?	?	?
E |	?	E	O
O |	?	O	E
</code>

抽象乘法：
<code>
#*|	?	E	O
--+-----------------------
? |	?	E	?
E |	E	E	E
O |	?	E	O
</code>

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


{{tag>计算机科学}}