Question

1.1 静态程序的定位

静态程序分析 是 编程语言 中 应用 层面下的一个细分领域，它是一个非常重要的核心内容。

在理论部分，考虑的是如何设计一个语言的语法和语义，如何设计语言的类型系统等等问题；有了语言的语法、语义和类型系统之后，我们需要支撑语言的运行。因此，在环境部分，需要考虑如何为运行中的程序提供运行时环境——如何设计编译器，在运行时需要怎样的支持（如内存的分配管理）等等；应用部分则关注如何保证语言所写出程序的效率、安全性和可靠性，主要考虑如何对程序进行分析，验证和合成（如何自动合成一个程序）。

一句话概括静态分析：在保证正确性的前提下，在精度和速度上做平衡。

1.2 静态程序分析的应用

1. 提高程序可靠性
   1. 空指针引用与内存泄漏等
2. 提高程序安全性
   1. 隐私信息泄漏 ：多存在于移动应用安全中
   2. 注入攻击
3. 编译优化
   1. 死代码消除 ：在编译器的机器无关优化环节，将不会对程序执行结果产生影响的代码（即死代码）删除。
   2. 循环不变量的代码移动 ：在编译器的机器无关优化环节，在保证不影响程序执行结果的情况下，将循环中的特定语句移动到循环外，使得程序运行时执行的语句数减少。
4. 有助于程序理解
   1. 为集成开发环境的功能提供帮助：当你使用 VS/Idea/Clion/Eclipse/Android Studio 等等 IDE 时，将鼠标悬停在代码上，IDE 能够动态地分析并提示你所悬停对象的相关信息，背后使用的技术就是静态程序分析。

1.3 Sound & Complete

以上就是静态程序分析所希望做的一些事情，但是实际上静态分析发展至今，依旧不能完美地解决以上的问题。

Any non-trivial property of the behavior of programs in a r.e. language is undecidable.

在一个即 递归可枚举 (recursively enumerable) 语言中，任何程序行为的 non-trivial 属性都是不可解释的。 non-trivial property 指的是那些与程序运行行为有关的属性。

—— Rice’s Theorem

也就是说，Rice 理论告诉我们，世界上并不存在一种 完美的静态分析 ，可以完美地解决上文提到的那些问题。

由上图可以直观地看出，三者成包含关系，而完美的程序分析就是中间的 Truth，一个既 Sound 又 Complete 的状况，而我们正常的程序分析只能获得要么 sound 要么 complete 的结果，一种 useful 的结果。

简单来说，sound 是一种过多的输出，输出的是全部的真实报错和部分的虚假报错；而 complete 与之相反，输出的是全是真是报错，但是比 truth 少了一部分的报错。

由上可知，我们在实际使用场景中，自然是希望输出是 sound 的，也就是说可以有误报但不要有漏报。

1.4 静态程序分析的核心

1.4.1 抽象：Abstract

以符号分析为例，将待分析的具体的变量取值抽象为：正、负、零、未知和错误。

unknown 指的是，如果当前数值会因为变量改变而呈现为不同的状态，则全部定义为 unknown。

undefined 指的是经过判断肯定不符合 int 定义的，例如一个除以 0 的数或者字符等。

1.4.2 近似：Over-approximation

1.4.2.1 转移函数：Transfer function

在静态分析中，近似的核心是定义转移函数（transfer function）。

• transfer function 是针对程序中的每一个语句，在抽象值上定义转换规则。
• transfer function 的规则是根据分析的具体问题与程序语义来定义的。

如上图所示：这是针对符号分析定义的部分的转换函数，前五个和第八个一目了然，不做解释。 第六个因为除数是 0，故结果是 undefined。第七个是由于我们定义的转换函数是抽象的，进行运算的目标也是抽象出来的，因此相加结果是 unknown 的。举个例子，即使我正数是 1000，负数是 -1，经过抽象后再经过转换函数处理，得到的结果仍是 unknown，这也是 sound 的一种体现。

根据上述的转换函数，可以对程序语句进行分析，最终得到的结果如下。

1.4.2.2 控制流：Control Flow

实际上，在程序分析的过程中，近似的过程中还要考虑程序的控制流。

右图是左图的运算流展示，在不同情况下 y 会有值，而根据 sound 原则，在最后一步的 y 值只能是 unknown。

在程序分析中，不可能与枚举所有的路径，因此 flow merging （控制流的汇聚）作为一种近似，在静态分析中十分常用。