分享

1 导言

1.1 缘起及基本发展

程序分析是一种自动推导程序运行行为的技术，起源于早期以Fortran为代表的高级语言的编译优化需求。计算机的早期发展阶段主要采用接近机器的汇编语言编程。当高级语言最初被引入时，由于当时编译器无法产生高效的代码，高级语言编程的想法曾经受到广泛的质疑，然而以程序分析为基础的编译优化技术随后得到长足发展，高级语言在大多数应用领域取代汇编语言成为人们的常识。编译优化只是程序分析的一种重要应用，程序分析基本思想现已应用到程序安全验证、软件工程、电路综合、操作系统(如微软Singularity项目)以及GPU编程等应用领域。表1.1列举了一些程序分析的应用实例。

表1.1 程序分析举例

1.2 Lingo语言

为了将后续的程序分析技术落实，这里引入一个基本的语言，定义如图1.1所示。首先符号集合的定义，n表示整数集中的元素，b是布尔值(true/false)，x表示程序变量。基本表达式操作符包括算术运算符(+,-,*,/)、关系操作符(<,<=,=,!=)和逻辑运算操作符(&&和||)。表达式包括整数或布尔常量、变量或者各种运算表达式。基本语句包括输入、赋值、NOP(Skip)、循环、选择，此外还定义了语句的组合方法(c;c)，最后一个程序(Prog)就是一个语句(Cmd)。

相对于实际的语言如C，Lingo要简单得多。注意关系操作符中没有>，另外只有两种数据类型(int和bool)，且不支持显式或隐式类型转换。变量定义默认初始化为0/false，除法假设有理想精度。后续为便于讨论各种分析技术还会增加指针和函数调用两种语言特性。

图1.1 Lingo语言定义

下图1.2给出了一个Lingo的例子程序，直观上很快就给出常量传播(程序中哪些位置的哪些变量肯定是常量?)和死代码检查(哪些语句肯定不会被执行?)的分析结果。可见程序分析来源于程序员理解程序时的经验直觉，经验和直觉只有经过升华才会成为具有一定普适性的指导原则，从后续要陆续展开的各种分析框架可以感受到这一点。写小说的强调要源于生活并高于生活，人类其他学科依然，只是演绎的基本思维元素不同。

图1.2 Lingo程序举例

1.3 程序语义模型

既然程序分析是提取和挖掘程序行为，因此首要问题是如何严格界定程序行为。有三大类程序语义模型：基于符号的(denotational)、基于抽象操作(operational)和公理化(Axiomatic)证明。符号模型和公理化证明不知为何物，抽象操作模型则相对直观，基本思想是给定一个程序，设想有一个抽象的虚拟机来执行之，依据不同的输入理论上可能得到无穷个执行轨迹(trace)，每条轨迹对应程序一种可能的运行状态，那么所有执行轨迹的状态总和就构成程序所有可能的行为。

从程序抽象执行轨迹出发来理解程序行为还被用到了其他地方。这里考察的是同一个程序因输入不同可能出现的无穷多执行轨迹，还有一个角度是考察在一台机器(SMP/Multi-core)上运行的多线程程序各个线程间指令的可能交错(interleave)情况，在线程间存在数据竞争的情况下，不同的interleave可能得到不同的执行结果，执行结果对或错的标准由内存模型来界定。尽管解决的问题不同，二者背后都利用了可以设想抽象虚拟机来枚举程序行为这一直觉。

有了虚拟机，那么给定输入，在任意程序点机器的状态就确定了。这里程序点直观上可以理解为程序中语句的位置，如图1.2示例代码中红色数字标识的位置，也就是程序计数器(PC)指向的地址。虚拟机的状态可以用给定PC位置当前所有变量和值的映射关系来描述，如图1.3的定义所示：

图1.3 给定程序点虚拟机状态

给定程序输入，抽象虚拟机模拟执行每条指令就能得到每个程序点的机器状态。图1.4给出了图1.2所示的程序执行到程序点3并推进到5的机器状态：

图1.4 机器状态求解过程示例

如果已知虚拟机在每个程序点的状态，那么每步求解过程合起来就构成了程序的执行轨迹。由这种以虚拟机为基础的操作语义出发，给定一个程序理论上可以分析出所有可能的合理(valid)执行轨迹，从而得到程序所有可能发生(may possibly do)或一定发生(must always do)的行为集合。

1.4 程序分析评价指标

对于很多应用场景，程序分析依据一组约束分析用户关注的局部程序行为，但静态程序分析结果经常是不可判定的，如图1.5所示：

图1.5 程序分析结果的不可判定

图1.5中if语句之后变量x的值是未知，因为有多条路径都可能会修改，在这种情况下程序分析时只能一定程度去近似程序的实际行为，具体有三种操作方式：

1. Sound analysis，对变量的可能取值进行保守假设(over approximation)，如指出变量x取值范围是{0,1}，尽管实际执行结果只会是0。这种情况不会出现误杀，讲究尽可能提高分析的取值范围精度；
2. Complete analysis，和sound analysis相对，力求精确分析(under approximation)，宁信其无，不信其可能有，对图1.5的程序，分析结果变量x的取值范围是{}。这种情况会有误杀情况。
3. 最后一种是不提供正确性保证，对图1.5的程序，分析结果可能是变量x为0，而实际执行结果x可能为1。

后续内容只关注sound analysis。由于这类分析关注某个变量的可能取值范围，当精确分析不可能时，可以对变量值域进行一定抽象分类来分析其取值属性，如{Zero, Non-Zero, Maybe-Zero}、{Even, Odd, Either}等等。

分享