静态分析与抽象解释

好久没有写东西了，呵呵。前些天看了几篇文章，是关于程序的分析技术的。程序的分析，对于优化编译器而言十分重要。它可以知道优化的进行，保证优化的正确性。
其中，关于抽象解释的那篇经典文章很不好读，看了两遍还是似懂不懂的。抽象解释大概是这样的：程序，代表的是某个数据域上的一系列计算，如果我们只关心程序执行的某一个方面的属性，那么，就可以在另外一个数据域（这个数据域中的点用于表示我们所关心的属性）上执行程序中的计算，当然，每一种计算都在新的数据域上被赋予了新的语义。例如-1717 × 15这个计算，如果我们只关心计算结果的符号，那么就可以定义数据域{+，-，？}，于是上面的运算就变成了-（+） × （+），乘法的运算语义就变成了“同为正，异为负”，上面计算的结果就是“-”。而对于-1717 + 15 =》 -（+） + （+） = ？结果是可正可负的。
这样做的原因是，我们感兴趣的非平凡的程序执行时属性，一般而言都是图令不可判定的，但是，可以通过抽象解释的方法得到一些近似的结果，而这些近似的结果对于某些程序的变换、优化是足够的。
于是，问题就变成了如何求得这些近似的结果。在抽象解释中，利用程序语言的局部抽象语义（单条语句的抽象语义）定义出来程序的整体的某个属性满足的一组方程组，而对该属性的最佳近似就是这个方程组的最小不动点或最大不动点。在求解这个不动点的过程中，使用迭代的方法。
为了保证这种迭代最终会停止并得到不动点，在抽象解释里面，会将正在求的属性的可能值组成一个格，并且保证方程组中的方程都是单调的。借助格的属性来保证过程有穷并收敛。例如，对于高度有限的格求最大不动点，一定可以得到。
当然，求解的另外一个约束是，求得的近似解必须是保守的，这样才能保证正确性。

而静态分析，基本上就是抽象解释的一种具体化。在对程序的静态分析中，大量地使用了抽象解释的思想和方法。最为典型的一个就是数据流分析了。另外，对于编译器中使用的一些常用的分析技术，都可以归纳位抽象解释。比如，控制流分析，指向/别名分析、类型分析、活性分析等等。
使用抽象解释进行静态分析的基本流程是：
1、定义一个抽象域，这个域中的值是所关心的属性的所有可能取值，并在这个域上定义一个偏序（常常是集合包含），通过添加顶元素和底元素，在域上形成一个格。
2、为程序设计语言的每一个语句规定一个抽象语义，该抽象语义是对1中抽象域中的值的操作。
3、用2中的抽象语义为目标程序的全局属性建立一组等式方程组，并将这个方程组改写成F(x)=x的形式。
4、通过在程序中进行迭代求解，找出3中方程的最小不动点（最大不动点）。
   在这个过程中，需要注意两点，首先，必须保证迭代求解过程是有限的，第二，必须保证找到的解是精确解的保守近似。对于第一点，如果能够构造一个有限高度的格，并保证F单调，就一定满足要求，如果格的高度不是有限的，可以通过Widing技术使它近似成有限的。对于第二点，需要保证在2中定义的抽象语义以及3中的方程都是保守近似的。具体例子可以参考任何一种数据流分析算法。