静态程序分析学习笔记(1)

1. 简介

静态程序分析（静态分析）是指在不实际运行程序的情况下推理其行为的技术。

目前主要用于自动化保障软件质量，相关技术也可用于编译器后端优化，IDE工具。

• 程序优化相关：死代码检测、循环不变式提取、常量分析等

• 程序正确性相关：空指针解引用、除零、算术溢出、变量初始化、数组越界、停机分析

• 程序分析相关：函数调用点、变量赋值路径、类型推断

2. 原理

莱斯定理（Rice's theorem）：递归可枚举语言的所有非平凡（nontrival）性质都是不可判定的。

递归可枚举语言：指那些可以被图灵机识别的语言。换句话说，如果某个字符串属于这个语言，图灵机会在有限时间内接受它；如果不属于，图灵机可能会一直运行下去而不会给出结果。

非平凡性质：对某些递归可枚举语言成立，但对另一些递归可枚举语言不成立。例如，"这个语言是否包含某个特定的字符串"就是一个非平凡性质，因为对于某些递归可枚举语言，它包含这个字符串，而对另一些递归可枚举语言，它不包含这个字符串。

以上定理的结论，基本等同于对于一个主流编程语言，关于程序输入/输出行为的极大部分问题都是不可判定的

因此，若想对程序行为进行静态分析，我们必须进行近似分析

另一个结论是，即使分析仅需对所有输入都能停止的程序工作，也不可能构建一个静态程序分析器来判断给定程序在执行时是否可能失败。一个例子即为Collatz猜想

考拉兹猜想（Collatz conjecture）：指对于每一个正整数，如果它是奇数，则对它乘3再加1，如果它是偶数，则对它除以2，如此循环，最终都能够得到1。

while (n > 1) {
    if (n % 2 == 0) // 如果n是偶数，则将其除以二
        n = n / 2;
    else // 如果n是奇数，则将其乘以三并加一
        n = 3 * n + 1;
}