母校计算机院的李樾、谭添老师讲的课,听了第一节课就哭了,决定做一下笔记,课程网站 https://pascal-group.bitbucket.io/teaching.html。
PL知识体系
如上图所示,主要分三大块,理论部分包含语言设计、类型系统、语义和逻辑检查;环境部分包含编译器和运行时设计等;应用部分包含程序分析、程序验证和程序生成等,本课程主要关注于应用方面的程序分析。
Rice’s Theorem(莱斯定理)
停机问题
了解莱斯定理,首先证明停机问题是不可判定的:
假设存在停机问题的判定算法
bool Halt(p)
;存在恶意程序:
1
2
3
4
5
6void Evil() {
if (Halt(Evil))
while(1);
else
return;
}那么
Halt(Evil)
返回存在矛盾:- 若返回真,即evil可停机,那么Evil()走if分支,但该分支evil不可停机,矛盾;
- 若返回假,即evil不可停机,那么Evil()走else分支,但这样evil可以停机,矛盾。
内存泄露问题
内存泄露问题与之类似:
1 | void Evil() { |
Rice定理
经过上面两个问题,可以感觉到只要是一个判定问题,就可以套用上面的evil框架来反证这个框架是不可判定的,Rice定理对上面情况作了总结:
Any non-trivial property of the behavior of programs in a i.e. language is undecidable.
对递归可枚举语言来说,不存在一个完美(Sound&Complete)的,用于判定程序中non-trivial的属性的方法。
这里“non-trivial property”可以理解为程序分析的种种目的,如变量是否空指针、是否存在信息泄露等。
- 平凡(trivial)属性:对图灵机(语言)P来说,要么对全体程序都为真,要么对全体程序都为假;
- 非平凡(non-trivial)属性:不是平凡的所有属性,如停机问题、空指针、信息泄露等。
证明:
设给定函数上有非平凡性质P,假设空集(对任何输入都不输出的程序,包括不停机程序)不满足P,因为P非平凡,因此一定有满足P的程序ok_prog;
假设有判定性质P的算法 P_holds()
,编写以下程序判断程序q是否停机:1
2
3
4
5
6
7Bool halt(Program q, Input w) {
void evil(Input x) {
q(w);//如果q不停机,那么evil不满足P
ok_prog(x); //如果q停机,那么启动ok_prog,此时evil程序等同于okprog程序
}
return P_holds(evil);
}
上面程序借用了P_holds的能力来判断停机问题,关键在于evil:
如果
q(w)
不停机,那么因为不停机程序不满足P,evil()
不满足P;如果
q(w)
停机,那么evil(x)
等同于ok_prog(x)
即evil(x)
满足P
综上,只要判定evil(x)
是否满足P,就可判定停机问题,但是之前已经证明过,停机问题是不可判定问题,因此矛盾。
注意,将空集描述为满足P,也可以用类似的方法证明(设有不满足P的程序no_prog…)
可靠性和完备性(soundness&completeness)
莱斯定理说明了不可判定性,在实际分析时只能做may或者must的分析,分析时出现sound和complete情况,存在两种妥协方案:
- Compromise soundness:妥协可靠性,即接受误报(may),该方案是静态分析较常见
- Compromise completeness:妥协完备性,即接受漏报(must)
误报(False positive)与漏报(False negative)关系如下图所示:
简单的程序分析案例
分析在代码p处变量v的正负(+, -, 0)。
定义数据抽象
- $+$:正
- $-$:负
- $0$:零
- $\top$:未知
- $\perp$:未定义
定义Transfer Function
即读取一个二元操作statements,输出符号是什么,如下表:
定义Control Flow Merge
在CFG中汇聚点中要合并情况
编译器vs.静态分析器
编译器:
词法分析(产生tokens)→语法分析(产生AST)→语义分析(包括类型检查,产生Decorated AST)→翻译(产生IR)→代码生成静态分析:
静态分析基于IR
AST和IR
AST
- 符合语法结构
- 依赖于特定语言
- 适合于类型检查
- 缺失控制流信息
IR
- 接近机器代码
- 语言无关
- 含有控制流信息
三地址码
一种常用的IR:
- 右侧只有一个操作
- 每一语句最多有三个“地址”(地址可以是变量,常量)
- $z=x\text{ }op\text{ }y$
- $x=op\text{ }y$
- $x=y$
- $goto\text{ }L$
- $if\text{ }x\text{ }goto\text{ }L$
- $if\text{ }x\text{ }op\text{ }y\text{ }goto\text{ }L$
Soot 中的三地址码:
@parameter
:函数参数$x
:临时变量<method signature>
:类+返回值类型+方法名+函数参数类型<init>
:构造函数<clinit>
:类初始化函数(静态变量初始化等)invokespecial
:调用构造函数、父类方法、私有方法invokevirtual
:实例方法调用(virtual dispatch)invokeinterface
:不能优化、调用接口、检查接口实现invokestatic
:调用静态方法invokedynamic
:运行其他动态语言
SSA
一种特殊的三地址码:
- 每次赋值有新的变量名
- 每一个变量都有唯一定义
优势:
- flow-insensitive analysis更准确
- 容易做优化算法
劣势:
- 引入大量变量
- 编译时有性能问题
Control Flow Graph
Basic Block是CFG的主体。
- Basic Block:一个最长的语句序列,并保证入口只能在最开始指令且出口只能在最后一个指令
构造Basic Blocks
- Input:程序P的三地址码序列
Output:程序P的basic blocks
算法
确定leaders(每个basic block的头)
- 序列中的第一个指令
- 跳转指令的目标指令
- 跳转指令的下一条指令
- return指令
每个Basic Block包含其leader至下一个leader前的所有语句
构造CFG
- 添加边,在以下两种情况下:
- 代码块存在先后顺序,且不存在无条件跳转
- 每个跳转间
- 添加entry和exit节点