南京大学《软件分析》课程

Introduction

Programming Languages三个部分:

  • 理论Theory:怎么设计语言Language design、类型系统Type system、形式语言semantics and logics
  • 环境Environment:编译器、运行时
  • 应用Application:程序分析(静态程序分析)、程序验证、程序合成

过去十多年,语言的核心部分变化得很小,语言主要三类:命令式语言函数式语言逻辑式语言;但是程序变得很复杂,如何确保程序可靠性、安全性和性能。

静态分析作用:

  • 对提高程序可靠性很有必要:空指针异常、内存泄漏等,静态分析减少这些bug;
  • 程序安全性:私有信息泄露、注入攻击等;
  • 编译优化:死代码删除;
  • 理解程序。

静态分析:在运行一个程序P之前,就要分析它的行为和聊起是否满足某些特性。

  • P是否有一些信息泄露问题
  • P是否有一些空指针
  • 所有类型转换都是安全的么
  • 两个指针指向同一块地址么
  • 一些assert是可能fail的么

莱斯定理:并不存在准确判断程序的方法。一个递归可枚举(recursively enumerable)的语言的所有不那么简单(non-trivial)的性质都是不可预测(undecidable)的。正常的语言的一些比较感兴趣的性质都不能给一个准确的答案。noon-trivial的性质约等于一些有趣(interesting)的性质。总之,一个完美的静态分析是不存在的。

将任意程序看作一个Partial Function,它描述了程序的行为,关于程序行为的任何非平凡属性,都不存在可以检查该属性的通用算法,即不可判定 。

这里平凡属性是指对所有程序都为真或者都为假的属性,非平凡就是对有些为真有些为假。特别注意莱斯定理的适用条件是关于程序行为而不是结构,并且不适用莱斯定理的也未必可判定。例如程序使用了多少个变量,就是涉及程序结构的问题,所以像[确定程序使用的变量是否多于50个]这样的问题无法用莱斯定义来说明它是不是不可判定的。

完美的静态分析满足soundcomplete的。Sound > Truth > Complete,Truth是说所有可能的行为,Sound说的是包含Truth且有其他的,Complete只有Truth中所有可能行为的一部分,Complete中爆出来的一定是Truth中的,而Sound中爆出来的不一定是Truth中的。

不存在既Sound又Complete的,只需要Useful的就好了,Useful包括:

  • Compromise Soundness:漏报
  • Compromise Completeness:误报

在静态分析中绝大多数都是Sound且不是那么准确的。但是Sound是很重要的,对其中一类的分析(编译优化)是很重要的。Sound可以翻译为全面

1
2
3
4
5
6
7
8
if (...) {
B b = new B();
a.fld = b;
} else {
C c = new C();
a.fld = c;
}
B b' = (B) a.fld;

上述程序是not safe的,这个结论需要通过分析两条指令得到,所以是Sound的,如果只分析了一个if段,则可能得到safe的结论,这个结论就是Unsound的。

越Sound越好,就越能检测出潜在的问题,力争保证Sound再提高精度。

对下面一段程序:

1
2
3
4
if(input)
x = 1;
else
x = 0;

两个分析结果:

  • input是true的时候,x = 1;否则x = 0。Sound、precise、expensive,通过上下文确定分析结果
  • x = 1 or x = 0。Sound、imprecise、cheap,

两个结果都是对的,只要结果包含了x = 1 或 x = 0,结论就是Sound的。在分析的时候确保Sound,同时也要做好分析的精度和速度的权衡。

抽象:用一些符号来归纳近似程序中的行为。一个例子:判断所有变量的正负(+、-、0),检查是否会除0,或者数组下标是否非法。v=e?1:-1是未知的,v=w/0是非法的,用两个符号表示。

近似(over-approximation):针对程序中每一个语句,给这些抽象值,定义转换规则。根据分析目标和程序中每一个语句的语义,在抽象值的基础上设计转换函数。

假设程序中有这些抽象语句,正数+正数负数+负数、等等类似的,通过分析就可以得到下边的表,而且能找到程序中的一些错误:

但是上边的分析可能会造成误报,报出来的错误比真正的错误多了。

对控制流也可进行分析,但由于输入很多种,产生控制流爆炸问题,需要对控制流进行merge。

Intermediate Representation

静态分析器需要一种程序表示格式(IR)。

编译器和静态分析器都是分析一个程序。编译器是将高级代码转换成机器能理解的机器码,类似一个翻译器,同时可以在翻译过程中报错。首先,通过Scanner做词法分析;通过Parser做语法分析,语法规则通过上下文无关文法描述,形成抽象语法树;用Type checker做语义分析;通过转换器转换为三地址码的中间表示形式(IR);最后生成机器码进行执行。通过前端将源码转换成IR中间表现形式之后才能进行静态分析。

对于:do i = i + 1; while(a[i]<v);它的AST为:

1
2
3
4
5
6
7
8
9
     do-while
/ \
body <
| / \
assign [] v
/ \ /\
i + a i
/\
i 1

树型结构转化为三地址码IR为:
1
2
3
1: i = i + 1
2: t1 = a[ i ]
3: if t1 < v goto 1

AST是高级语言结构,与语法结构很相似;基本是基于语言的,对于快速类型检查很有利,缺乏控制流信息;而IR是低级语言,与低级机器码很相似,一般是独立于语言的包含了控制流信息,但是没有冗余信息,基本被认为是静态分析的基础。

中间表示Intermediate Representation(IR)

3-Address Code(3AC):在表达式的右边最多只有一个操作符。如:
a + b + 3 ---> t1 = a + b; t2 = t1 + 3

地址可以是以下几种:变量名(a、b)、常量值(3)、编译器生成的临时变量(t1、t2),不仅仅指的是内存地址。

每种指令都有特定的三地址码形式,也有一些特定形式的3AC:

  • x = y bop z:bop指的是二元操作符或者逻辑操作符
  • x = uop y:uop是一元操作符
  • x = y:赋值语句
  • goto L:跳转语句
  • if x goto L:有条件判断跳转语句
  • if x rop y goto L:有关系判断跳转语句

针对一个for循环:

1
2
3
4
5
6
7
8
public class ForLoop3AC {
public static void main(String[] args) {
int x = 0;
for( int i = 0; i < 10; i ++) {
x = x + 1;
}
}
}

三地址码如下:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
public static void main(java.lang.String[] args) {
java.lang.String[] r0;
int i1;
r0 := @parameter0: java.lang.String[]; // 这是一种标记,r0是那个传进来的参数,这种赋值符号不是真实的赋值,作为特殊的赋值标记出来。

i1 = 0;

label:
if i1 >= 10 goto label2;
i1 = i1 + 1;
goto label1;
// 三地址码中有一些label作为程序的标记
// i和x做了优化,被合并了
label2:
return;
}

然后是do-while loop:

$i0是生成的临时变量,访问的数组元素被赋值给临时变量。

调用函数:

Static Single Asssignment(SSA)

静态单赋值(static single assignment, SSA)使得3地址码(3-address code, 3AC)中的变量只有唯一一个定义,即每条语句中的变量都用不同的名字表示。在有分支控制流的情况,可以使用一个特殊的合并函数(Φ,phi-function),在控制流通过不同代码块时会有相应的取值。当考虑分支操作时,SSA引入Phi函数。比如x0=0和x1=1汇聚,引入x2=phi(x0,x1),再进行之后的操作,确保单赋值。

为什么用SSA:把流控制信息通过独特的变量名引入到程序执行中,这可能帮助设计一些分析。定义-使用组更加地明显,当要使用一些特殊的优化算法时更方便,也引入了更有效的数据存储整合。

为什么不用SSA:可能会引入很多的Φ函数。

Control Flow Analysis

通常是说构建Control Flow Graph。如下图所示:

这个图是之后的静态分析的基础,CFG的节点是一个独立的三地址码命令,或者是一个代码块(Basic Block)。基本块是最大连续的三地址码指令,满足:

  • 只能在第一条指令进入
  • 只能在最后一条指令出去

对下图的代码段,1,2满足代码块的定义,但是加上3之后可能会从从其他地方跳到3,所以1,2是一个代码块。所以如果一句代码如果作为jump的目标,则作为代码块的开始。3,4组成的代码段如果再加上5的话,就有两个出口了,所以3,4组成一个代码段。一个语句有goto的话,作为代码段的出口。

算法:

  • INPUT: A sequence of three-address instructions of P
  • OUTPUT: A list of basic blocks of P
  • METHOD:
    • (1) Determine the leaders in P
      • The first instruction in P is a leader
      • Any target instruction of a conditional or unconditional jump is a leader
      • Any instruction that immediately follows a conditional or unconditional jump is a leader
    • (2) Build BBs for P
      • A BB consists of a leader and all its subsequent instructions until the next leader

对上文中的三地址码序列,首先找出每个BB的leader,第一句是一个入口,所有jump的目标是leader,3,7,12都是leader,jump指令后边的指令是一个leader,5,11,12是leader。一个leader及其后续的直到下一个leader的所有指令是一个BB。

leader有:1,3,5,7,11,12。所以代码块有:

  • B1 {1, 2}
  • B2 {3, 4}
  • B3 {5, 6}
  • B4 {7, 8, 9, 10}
  • B5 {11}
  • B6 {12}

接下来添边,进一步构建CFG。如果从A到B有一个条件或无条件跳转,两个块AB之间有一条边。如果A紧接着就是B块,而且A最后一条指令不是无条件跳转的话,也需要添一条边。

通常再添加两个节点,Entry和Exit。与IR无关,从Entry到第一个BB的边包含第一条IR指令,从BB到Exit的边包含可能的最后一条指令。

Data Flow Analysis

数据是如何在CFG中流动的?

何种data在CFG中流动?(应用程序特定数据)首先对data做抽象(对一些operator抽象),之后做近似(对表达式抽象),数据近似在代码块、CFG中运行。

  • may analysis:最常见的静态分析,输出可能正确的信息(over-approximation,最安全,可以被称为safe-approximation);
  • must analysis:输出一定正确的信息(under-approximation)
  • 二者都是为了分析的正确性。

不同的数据流分析应用有不同的数据抽象和不同的近似策略(flow safe-approximation strategies),也有不同的转换函数和不同的控制流处理方法。

Input and Output states

每个IR指令s1的将一个input state(IN[s1])转换成一个output state(OUT[s1]),每一个input(output) state与程序的一个点(program point)关联。s2的input就是s1的output,如果有分支的话,那OUT[s1]=IN[s2]=IN[s3]。如果有汇聚,那么IN[s2]=OUT[s1] ^ OUT[s3]

在每个数据流分析应用中,将每一个程序点(program point)关联一个数据流的值(data-flow value),这个值代表了,在这个点上所有能观察到的程序状态(program states)的一个抽象(abstraction)。

换句话说,数据流分析就是对程序中所有语句的IN和OUT,通过解析一系列safe-approximation约束规则(transfer function和控制流信息),找到一个方法,给它关联一个data-flow value。

data-flow value存在一个值域,这个值域就是之前说的“正、负、零、未定义、非法”等。

transfer function:正常的分析是按照程序执行的顺序分析。语句s对应的transfer function用fs来表示,则OUT[s] = fs(IN[s]),这句话是说,输入是执行s之前的value=IN[s],转化为s执行完之后状态OUT[s]。另一种是反向分析,逆向程序执行的顺序,则IN[s] = fs(OUT[s])

控制流的约束(control flow’s constraints):一共是n条语句,在一个代码块中的控制流,IN[s(s+1)] = OUT[s(i)], for all i = 1, 2, ..., n-1,每一个语句的IN都是上一个语句的OUT。代码块的关系:IN[B]=IN[s1] OUT[B]=OUT[sn]

一个基本块的transfer function,是其中所有语句的transfer function,即OUT[B]=fb(IN[B]), fb=fsn*...*fs2*fs1IN[B]=∩ (P: a predecessor of B) OUT[P]

Reaching Definitions Analysis定义可达性

所有data-flow都基于CFG内部过程,不涉及函数调用;不涉及别名,变量都没有别名。

程序点p中的一个定义d,如果有一条路径能够从p到达点q,且在路径上d没有被“killed”。

变量的定义definition:是对变量复制的语句。上一句可以变为,程序点p中定义v的地方称为definition d,如果能从p走到q,且v不能被重新定义,否则走到q的v就不是d定义的v了。可以用于检测可能的未定义/未初始化。

如果存在一条路径使得程序点p上的定义d能够不被阻塞/不被重定义地到达q,则称定义d可达(reaches)q。

D: v = x op y这个语句生成v的一个definition,然后‘kills’其他所有对v的定义,但是保留了对其他变量的定义。transfer function为OUT[B]=(gen B)∪(IN[B]-kill(B)),去掉其他所有定义这个变量的语句。

control flow:IN[B]=∪ (P: a predecessor of B) OUT[P],就是B所有的前驱P的OUT的并,一条结果都不放过,都考虑成B的IN。

定义可达性分析算法:

1
2
3
4
5
6
7
8
9
10
11
INPUT: CFG(kill(B) and gen(B) computed for each basic block B)
OUTPUT: IN[B] and OUT[B] for each basic block B
METHOD:
OUT[entry] = Φ
for (each basic block B\entry)
OUT[B] = Φ
while(changes to any OUT occur)
for(each basic block B\entry) {
IN[B] = ∪ (P: a predecessor of B) OUT[P]
OUT[B] = gen(B) ∪ (IN[B] - kill(B))
}

算法的输入是控制流图,输出每一个基本块B的IN和OUT。算法的第一步是把所有的OUT变为空,入口的OUT也为空。但是在for里为什么排除entry呢?因为需要对一些特殊情况适用,考虑一些边界情况。如果所有的BB中有一个BB的OUT变化了,就要执行这个while,给每一个BB执行这个约束。


有8个definition,定义不同的变量颜色不同。8个定义每个定义用一个bit表示,0表示在这一某点这个definition不可以reach到,1表示在某一点这个definition可以reach到它,一开始当然每个BB上的8个bit都是0,没有一个definition可以reach到。

B1的IN是0000 0000,根据transfer function生成B1的OUTPUT,gen(B)是对D1和D2,所以00变成11,执行完BB1之后,这个OUTPUT变成1100 0000,B2的IN是所有B2的前驱的UNION(B1和B4),所以就是(11000000)∪(00000000),所以是1100 0000作为B2的IN,输出是kill掉所有定义y的地方,所以是10110000,第一次迭代执行完结果如下:

第二次迭代执行完之后:

因为第二次遍历之后还有变化,所以还需要第三次遍历,继续迭代,第三次迭代之后就不变了,这个OUT的结果就是final result,在一个基本块的OUT,哪一位为1则哪一个definition能够到哪个基本块。

不停地使用transfer function,直到算法停止,找到一个solution。transfer function中的gen(s)和kill(s)都是不变的,这里当一些facts加入到OUT中,就不会离开了,即0只会变成1,1也只会变成1而不会变成0。因为所有的facts是有限的,所以OUT的增长是有限的,直到没有facts可以加入到OUT为止。

算法最后到达了一个fixed point,也与单调性相关。如果OUT不变,IN不会变;如果IN不变,OUT也不会变,二者相互制衡。

live variables analysis

活变量分析指明了在程序点p上的变量值v,是否可以在以p为起点的CFG路径中被使用,如果是的话,说v在p上是活的,否则是死的。如果从p到q,v被使用到了但是没有被重新定义redefined(比如一开始等于0然后在某个点等于3了),这样v就是活的。

活变量的信息可以用于寄存器分配,如果所有寄存器都满了,就要选择一个变量进行替换,这时可以通过静态分析选择一个死变量进行替换。

data应该怎么抽象:把所有的数据用bit vector记录,第i个bit表示第i个变量,如果是0表示这个变量是死的,如果是1表示这个变量是活的。

通过forward来检测这个变量v是否是存活的:如果从p点开始向下走,经过很多statement,直到走到最后才知道这个变量v是否被使用了;如果使用backward,则更方便。


对于上图,B有两个后继,如果采用backward方法进行分析,则OUT[B]=∪ (S a successor of B) IN[B],B的OUT是B的所有后继的IN的并集。v在S1中使用了。

假设在一些寄存器R中的变量v是活的,或者是否需要删掉值为3的变量v,是的话IN[B]={v},不是的话IN[B]={}。

在图中,如果k=n则IN[B]={v},如果k=v则IN[B]={v},如果v=2则IN[B]={},如果v=v-1则IN[B]={v},如果v=2;k=v则IN[B]={},如果k=v;v=2则IN[B]={v}。

由上,可以得到IN[B]=use(B) ∪ (OUT[B]-def(B)),前边已经知道OUT[B]了。如果变量被redefined了,就不应该在IN[B]里,如果在define之前就被use了,那就直接加进来。

定义活变量分析算法:

1
2
3
4
5
6
7
8
9
10
11
INPUT: CFG(def(B) and use(B) computed for each basic block B)
OUTPUT: IN[B] and OUT[B] for each basic block B
METHOD:
IN[exit] = Φ
for (each basic block B\entry)
IN[B] = Φ
while(changes to any IN occur)
for(each basic block B\exit) {
OUT[B] = ∪ (P: a successor of B) IN[P]
IN[B] = use(B) ∪ (OUT[B] - def(B))
}

对一个程序进行分析,跟上边的分析类似,只是是从下向上的分析。

Available Expressions Analysis可用表达式分析

一个表达式x op y,如果所有路径从入口到p都一定要计算表达式x op y,且在计算x op y之后没有x和y的重定义,则称表达式x op y在点p是活的。

  • 这个定义也说明了在程序p中,可以用x op y的结果替换掉这个表达式。
  • 这个可以用于检测全局的通用表达式

抽象:表达式可以用bit vector来表示。

对于a = x op y,使用forward分析方法,它的IN={a+b},它的OUT中应该加上x op y,因为x op y是刚执行的,被看成是gen;然后从IN中删掉所有涉及a的语句,这被看成是kill。所以,OUT[B]=gen(B)∪(IN[B]-kill(B))IN[B]=∩(P a predecessor of B)OUT[P]。这里使用了交集,因为所有从入口到p点的路径都需要通过x op y这个函数。

因为表达式是否可重用涉及到程序的正确性,因此需要under-approximation,报少,但一定要对,确保safe。

1
2
3
4
5
6
7
8
9
10
11
INPUT: CFG(kill(B) and gen(B) computed for each basic block B)
OUTPUT: IN[B] and OUT[B] for each basic block B
METHOD:
OUT[entry] = Φ
for (each basic block B\entry)
OUT[B] = Φ
while(changes to any OUT occur)
for(each basic block B\entry) {
IN[B] = ∩ (P: a predecessor of B) OUT[P]
OUT[B] = gen(B) ∪ (IN[B] - kill(B))
}

一个例子:

本节课的总结表:

foundation

假设一个有k个节点的CFG(一个程序的执行流),且这里的一个节点是一个statement,算法在每次迭代时都会更新每个节点的OUT信息。假设数据流分析中domain(所有程序里的definition作为数据流分析的值域)的值为V,可以定义一个k元组,每个node的OUT值作为这个k元组的值,(OUT[n1],OUT[n2],OUT[n3],…OUT[nk]),作为一个集合(V1×V2×…Vk)中的元素,这个集合定义为V^k,代表的是每次迭代遍历之后的分析值。所以说V^k存的是每次迭代之后每个节点分析的临时结果。每次迭代都可以作为使用函数F:V^k -> V^k,通过转换函数和控制流处理建立V^k之间的映射关系。算法输出一系列的k元组,直到两次输出的k元组相同。这是从另一个角度观察之前的算法。

每一个OUT初始化为空,之后开始遍历,第一次遍历结束之后产生一个OUT集,上标1表示第一次迭代,下标表示每个节点。一直迭代直到两次相同。每个k元组用Xi表示,每次遍历都可以表示成一个函数,比如X0作为F的输入,输出第一次迭代的结果X1,Xi=F[x(i-1)],X(i)=X(i+1)=F(xi),所以X(i)=F(xi)。

这里的Xi就是函数F的fixed point不动点,X=F(X),迭代算法达到了一个不动点Xi。

迭代算法生成了数据流分析的方案,那:

  • 算法保证能停止或者能到达一个不动点么?或者总是能找到一个解么?
  • 如果上述成立,那算法只能找到一个不动点么?我们找到的不动点是最好的么?
  • 何时能找到不动点?

偏序partial order:我们定义一个偏序集(poset)为(P,⊑),其中⊑在P上定义了一个二元偏序关系,满足:

  • 自反性(reflexivity):∀x∈P,x⊑x
  • 反对称性(antisymmetry):∀x,y∈P,x⊑y∧y⊑x ⟹ x=y
  • 传递性(transitivity):∀x,y,z∈P,x⊑y∧y⊑z ⟹ x⊑z

偏序意味着有些在P内的有些元素对是没有办法比较的。

S是整数集合,⊑是小于等于关系,S满足偏序关系:

  • 1 ≤ 1,2 ≤ 2,所以满足自反性
  • x ≤ y ∩ y ≤ x,则x = y,所以满足反对称性
  • 1 ≤ 2 ∩ 2 ≤ 3,则1 ≤ 3,所以满足传递性

上下界:给定(P,⊑)和子集S⊂P,若u∈P是S的上界,则∀x∈S,x⊑u;类似地,若l∈P是S的下界,则∀x∈S,l⊑x,如下。

最小上界/上确界(lub/join)、最大下界/下确界(glb/meet):所有S上界中最小的一个称为S的上确界,记为⊔S;所有S下界中最大的一个称为S的下确界,记为⊓S。通常,如果S只含两个元素a,b,那么上确界可被写成a⊔b(join),下确界可被写成a⊓b(meet)

一些性质:

  • 并不是所有偏序集都有上确界或下确界;
  • 如果有的话一定唯一(反证法);
  • 界不一定在子集S中。

格(lattice):如果偏序集是格,则任两个元素对都有lub和glb。

半格(semilattice):如果任两个元素对只有一侧的确界,则称其为join/meet半格。

完全格(complete lattice):对于格的任意子集都有上下确界,那么该格称为完全格。完全格中的最大元素⊤=⊔P称为top,最小元素⊥=⊓P称为bottom。幂集依然是个完全格。结论:有限的格都是完全格。

乘积格(product lattice):如果对于格L1=(P1,⊑1),L2=(P2,⊑2),…Ln=(Pn,⊑n),如果对于所有的i,Li=(Pi,⊑i)有上下确界,那么定义乘积格L^n=(P,⊑)

  • P = P1 × P2 × … × Pn
  • (x1, …, xn) ⊑ (y1, …, yn),(x1⊑y1)∩…∩(xn⊑yn)
  • (x1, …, xn) ⊔ (y1, …, yn),(x1⊔y1, …. xn⊔yn)
  • (x1, …, xn) ⊓ (y1, …, yn),(x1⊓y1, …, xn⊓yn)

数据流分析框架(D, L, F):

  • D:数据流的方向,正向或反向
  • L:一个格,包括V的值域和上下界操作符
  • F:从V到V的一个transfer function族

左右两边建立关联,OUT[s1]={a}和OUT[s3]={b}并之后作为s2的IN={a, b},实际上就是在这个格上,数据流进行流动,OUT[s2]={a, b, c}。数据流分析可以被认为是在一个格的值域上迭代执行转换函数和meet/join操作。

对之前的三个问题:

  • 算法保证能停止或者能到达一个不动点么?或者总是能找到一个解么?这是格函数的单调性问题
  • 如果上述成立,那算法只能找到一个不动点么?我们找到的不动点是最好的么?函数可能会有多个不动点,我们这个迭代过程是不是最精确的?
  • 何时能找到不动点?

单调性(monotonicity):定义在格上的函数f:L↦L是单调的,若∀x,y∈L,x⊑y⟹f(x)⊑f(y)。

不动点定理(fixed-point theorem):给定完全格(L,⊑),若满足:(a) f:L↦L是单调的,(b) L是有限的(finite),则最小不动点可以通过迭代f(⊥), f(f(⊥)), …, fk(⊥)迭代得到,最大不动点可通过f(⊤), f(f(⊤)), …, fk(⊤)迭代得到,直到到达一个不动点。

证明:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
根据f:L↦L和⊥,有⊥⊑f(⊥)。
因为f是单调的,所以:f(⊥)⊑f(f(⊥))=f^2(⊥)
同样的,不停使用这个性质,⊥⊑f(⊥)⊑f^2(⊥)⊑...⊑f^i(⊥)
因为L是有限的,对于一个特定的k,我们有:f^fix = f^k(⊥) = f^(k+1)(⊥)
因此不动点存在。

假定有另一个不动点x,x=f(x)
因为⊥的定义,⊥⊑x

因为f是单调的,f(⊥)⊑f(x)
假定f^i(⊥)⊑f^i(x)
因为f是单调的,我们有f^(i+1)(⊥)⊑f^(i+1)(x)
通过归纳,f^i(⊥)⊑f^i(x)
因此^i(⊥)⊑f^i(x)=x,f^fix=f^k(⊥)⊑x
因此不动点是最小的。

需要把迭代算法跟不动点定理相关联,一旦关联上就可以解释上述三个问题。把整个数据流分析算法看成CFG中节点OUT的更新,直到两次迭代的OUT都一样。

每一个迭代中,定义一个函数F,给每一个节点执行这个节点上的转换函数,然后沿着CFG应用meet/join。F包括:

  • 转换函数 fi: L↦L
  • meet/join函数:⊓/⊔: L × L ↦ L

证明函数F是单调的(monotonic)。transfer function一般都是monotonic的。对于meet/join函数,只要证二元关系是单调的就行。

1
2
3
4
5
Proof:
在L上取三个元素x,y,z,x⊑y,我们希望证明 x ⊔ z ⊑ y ⊔ z,那这样的话这个关系就是单调的。y ⊑ y ⊔ z
通过⊑的传递性,x ⊑ y ⊔ z
因此y ⊔ z是x的上界,也是z的上界
x ⊔ z是x和z的最小上界,因此x ⊔ z ⊑ y ⊔ z

以上说明⊔关系是单调的。

格的高度h是从顶到底的最长的路径,这个格的高度h=3。

假设每一次迭代,只能在格上走一步(即一个node里的一位0变成1),假定一共有k个node,格的高度是h,计算最坏情况下迭代次数是i=h*k。这也是能找到不动点的最坏次数。

May and Must Analyses, a Lattice View

图中的上下界确定,假定这个格是一个乘积格

May Analyses是一个bottom,代表一个不安全的结果,算是一个下界;另外有一个上界,是安全但是不完全/没用的结果。这里中间有一个Truth,将safe和unsafe隔开。如何知道分析一定是safe的?这是由单调性决定的。May Analyses从底部一直向上走,我们向上走先接触到的是最小不动点。从最底部走到最顶部,是从精度最高走到精度最低的。所以May Analyses一般都首先初始化为空。

Must从上向下走。代表最安全的结果,也有一个Truth代表安全和不安全的分界。上边的那些存在一些不安全的结果,越向下是越安全的。同样也有一些不动点,我们求解的结果一定是最好的不动点。

已经证明过不动点原理,一定达到最小/大不动点,may为什么是最小不动点呢?每一次走一步就按照transfer function向上走,达到一个least bound,每次迭代都是一个min step,最终达到最小上界。

How Precise is our solution

Meet-Over-All-Paths Solution(MOP):用着一个meet把meet/join合并,所有的path合并到一点的时候,用meet/join合并。一个Path是从entry到Si的路径,P=Entry->S1->S2->…->Si。路径P的的transfer function记作FP,是这个路径上所有节点的transfer function的组合。

MOP就是枚举从Entry到Si所有的Path,然后把三条路径的FP结果join/meet起来,公式是:MOP[Si] = ⊔/⊓ FP(OUT[Entry]), A path P from Entry to Si,所有path应用transfer function之后进行meet/join,找到确界。有一些path是不可能走到的,所以这是不精确的。

我们的迭代算法和MOP:对于这样一个CFG:

使用迭代算法:

内部的join是S3的输入。如果用MOP的话,不是每个节点算完之后取join,而是一条path算完之后取一个join,是两个S3的OUT进行join:

如果用x和y进行替代,则Ours=F(x⊔y), MOP=F(x)⊔F(y),这两个function之间有什么关系:

1
2
3
4
5
6
7
8
因为x ⊑ x ⊔ y 且 y ⊑ x ⊔ y
且transfer function是单调的,有:
F(x) ⊑ F(x⊔y)且F(y) ⊑ F(x⊔y)
这就意味着F(x⊔y)是一个F(x)和F(y)的上界

因为F(x) ⊔ F(y)是F(x)和F(y)的上确界(lub),我们有:
F(x) ⊔ F(y) ⊑ F(x⊔y)
MOP ⊑ Ours

满足一个偏序关系,所以MOP更准,Ours比MOP更不准。

当F是可分配的(distributive),F(x) ⊔ F(y) = F(x⊔y),则两个相同。位向量(bit-vector)或者Gen/kill问题都是distributive的。

Constant Propagation

在程序某点p,给定变量x,判断x在p点是不是保证指向一个常量。

在CFG中每个节点的OUT是一组pair(x, v),x是一个变量,v是在这个节点之后x所拥有的值。这个分析是一个forward形式的。他的格:值V的定义域很简单:

越往下走越都不是常量,越安全但是越不精确。它的meet操作符(NAC表示not a constant):

  • NAC ⊓ v = NAC
  • UNDEF ⊓ v = v
  • c(常量) ⊓ v(任意一个值)
    • c ⊓ c = c
    • c1 ⊓ c2 = NAC

transfer function:给定一个语句s: x=...,定义transfer function F为:F: OUT[s] = gen ∪ (IN[s] - {(x, _)}),其中
_是通配符,x无论值是什么,都有一个新的值,就把原来的值干掉。我们使用val(x)代表变量x指向的值。

  • s: x = c; // c is a constant gen = {(x, c)}
  • s: x = y; gen = {(x, val(y))}
  • s: x = y op z; gen = {(x, f(y, z))}

如果y和z的值都是常量的话,x就是val(y) op val(z),如果val(y)或val(z)有一个是NAC,则x是NAC,其他情况下都是UNDEF。

但是它不是distributivity的,比如:

通过constant propagation求c,因为F(x) ⊓ F(y) = {(a, NAC), (b, NAC), (c, 10)},这里c已经通过path算出来了,但是F(x⊓y) = {(a, NAC), (b, NAC), (c, NAC)},所以是不一样的,F(x⊓y) ⊑ F(x) ⊓ F(y)。

worklist algorithm

是对迭代算法的优化。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
INPUT: CFG(kill(B) and gen(B) computed for each basic block B)
OUTPUT: IN[B] and OUT[B] for each basic block B
METHOD:
OUT[entry] = Φ
for (each basic block B\entry)
OUT[B] = Φ
Worklist <- all basic blocks
while(worklist is not empty)
Pick a basic block B from Worklist
old_OUT = OUT[B]
IN[B] = ∪ (P: a predecessor of B) OUT[P]
OUT[B] = gen(B) ∪ (IN[B] - kill(B))
if (old_OUT ≠ OUT[B])
Add all successors of B to Worklist

如果B的OUT变了,那么所有的后继的输入IN就变了,那么只把IN变了的basic block加进worklist中。这样避免了大量的重复计算。

Inter-procedural Analysis

目前的分析都是过程内的分析,不处理函数调用。过程间分析会顺着call graph传递数据流,避免过于保守的假设造成的损失。做过程间分析需要的必要的是call graph。如何构造程序调用图?调用图是调用关系的表示,每个调用边从调用点指向调用的函数。对程序的优化、理解都有作用。

四个比较有代表性的算法,越往下就精度越高,越往上速度越快:

  • class hierarchy analysis(CHA)
  • rapid type analysis
  • variable type analysis
  • pointer analysis(k-CFA)


上图是Java的函数调用的种类,只有virtual call比较特殊,在执行的时候才知道调用的具体位置。virtual call中有个method dispatch,在执行使,一个virtual call取决于:

  • 方法的签名signature,通过签名可以唯一的确定一个标识符。
  • 调用者的类型。

定义一个函数dispatch(c, m),来模拟这个调用过程,如果c包含了一个非抽象方法m’,且与m有相同的签名和名字,则返回m’,否则的话,返回的是dispatch(c', m),这里c’是c的父类。

下图中dispatch的结果是Dispatch(B, A.foo()) = A.foo()Dispatch(C, A.foo()) = C.foo()

class hierarchy analysis(CHA)

需要整个程序的类的继承信息,根据类型求解目标方法。假定变量a可以指向所有的类A及其所有子类。

定义函数Resolve(cs),其中cs表示call site,来求解所有可能的目标方法。如果是static call,就是写在调用中的方法。如果是special call,则需要处理构造函数、私有方法、父类方法三种情况,构造函数和私有方法两种情况就是写在调用中的方法,但是为了兼容父类方法这种情况,所以统一使用dispatch函数。如果是virtual call,首先取出变量c的声明类型C,对C和C继承树上所有的子类都调用dispatch,把它加入到目标方法中。

取出C和C所有的子类,这里对B及其子类C、D做dispatch,而且B没有foo方法,所以要去A中找foo方法,所以就是A.foo(), C.foo(), D.foo()。根据声明类型去找子类。

CHA很快,只考虑了声明类型及其继承关系,忽略了数据流和控制流信息。它的不足是很不精确。在IDE中很常用。

用CHA构造call graph,对每个可到达的方法m,解所有的可调用方法。直到没有方法可达。生成调用图之后有的方法可能是不可达的。

第一行算法做了初始化,WL是worklist,存了需要被处理的方法,CG是调用边,RM是可达方法的集合,进入RM之后就不需要被处理了。整个算法是一个大的while循环,循环内部从WL去一个方法,如果在RM中就不处理;否则对于这个方法m,执行Resolve方法,把每个方法加入到CG中,把新发现的方法加入到WL中,后边把新发现的方法继续处理,最后返回CG。

下图是个例子:

interprocedural control-flow graph

ICFG表示整个程序的结构,可以做过程间的分析,由每个方法的CFG和两种额外的边组成:

  • call edges: 从call sites到被调用者的入口
  • return edges: 从被调用者的返回语句指回向call sites
1
2
3
4
void foo() {
bar(...); // call site
int n = 3; // return site
}

ICFG的例子,整个程序的控制流图,需要保留call edge和return edge之间的边

我们需要edge transfer,进行数据流的转换,这个转换是顺着边的。call edge transfer传参数,return edge transfer传返回值。node transfer要处理等式运算。对于一个调用节点中的式子的左边的值,要把它kill掉,因为它的值回通过return edge流到下边的返回点。

对于调用,要把左值去掉,否则会与函数返回值冲突,因此b不在流中;接下来处理call edge,处理传参,参数传过来之后,x=6, y=7,最后return edge传输的是b=val(y)

图中可以发现,call site到return site的边叫做call-to-return edge,使得可以传播本地数据流(函数内部的数据流,在这里a=6是可以通过这个边传递的,如果没有的话,就不能传播了)。如果删掉了,则要把调用者自己的数据再传输到被调用函数中,如第二张图


Pointer Analysis

motivation

CHA建立call graph,foo中调用了get方法,以下三个类实现了接口Number中的get方法。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
void foo() {
Number n = new One();
int x = n.get();
}

interface Number {
int get();
}
class Zero implements Number {
public int get() {return 0;}
}
class One implements Number {
public int get() {return 1;}
}
class Two implements Number {
public int get() {return 2;}
}

如果用CHA解n的get方法的话,有3个目标函数,根据变量的类型,有三个子类。如果做constant propagation的话,有三个函数会返回给x,x就会被赋值为NAC,但是实际上根据类型,n只会指向One类型的变量,只有一个可能。

指针分析会根据变量指向的对象建图,只会对One类型做dispatch,得到的调用图是更准确的,解决了CHA引入更多可能的问题。

introduction

指针分析解决了程序中的指针可以指向哪个变量地址的问题,一个指针指向程序中的哪些对象,计算出来的结果会比实际上指向的对象更多。

1
2
3
4
5
6
7
8
9
10
11
void foo() {
A a = new A();
B x = new B();
a.setB(x);
B y = a.getB();
}
class A {
B b;
void setB(B b) { this.b = b; }
B getB() { return this.b; }
}

创建了两个对象,调用了set方法和get方法,对其进行指针分析,得到指向关系setB方法中的this是A类型,b是B类型。getB方法左边的y指向B类型。

别名分析与指针分析关系紧密但是有区别,指针分析回答了程序中的指针可以指向哪个对象;而别名分析指明了两个指针是否可以指向同一个对象。两个指针指向了同一个对象,则是别名:q和p是别名,x和y不是别名。别名可以通过指针分析得到,对于优化、调bug的基础。

1
2
3
4
p = new C();
q = p;
x = new X();
y = new Y();

key factors of pointer analysis

指针分析的要素:

  • 是一个复杂系统
  • 许多要素会影响精度和效率,下图是最关键的四个要素
    • 堆内存、上下文、控制流等

堆抽象

执行时堆内存的数量理论上是无限的,把程序动态分配出来的无穷无尽的堆对象抽象成为有限的抽象对象,这样使指针分析能够结束,限制静态分析处理对象的个数,下图中把左图中堆内存中分配的多个对象或有某些共性的对象合并成一个对象。

堆分析有很多内容,有两大流派,一个是store based model,一个是store less model。

只学习allocation-site abstraction,这种技术在分配点进行给动态对象建模的方式,用抽象的对象表示所有在这个创建点创建的对象。

1
2
3
for (i = 0; i < 3; i ++) {
a = new A();
}

这里的程序在第二行有一个创建点,动态创建三个对象,o2表示创建点,在这个创建点创建了三个对象,使用这个方法创建的话,只会创建一个抽象的对象来表示这三个具体的对象。有几个new就会创建几个抽象点。

上下文敏感

它回答了指针分析中如何对上下文进行建模,通常有上下文敏感上下文不敏感两种方式。每次调用都会产生不同的上下文,相应的形参也会不一样,是否将两次不同上下文的调用分开,上下不敏感会把不同的调用混合到一处,会降低精度。因此以上下文敏感为主。

流敏感

如何对程序的控制流进行建模,有两大类做法:敏感or不敏感。目前学到的所有分析方法都是敏感的。对一段程序做流敏感/不敏感的指针分析。

敏感的分析在程序的每一点都维护指向关系映射,都会检查指针指向的变化。不敏感的分析只维护一个指向映射,会保存所有的可能结果,为了保证结果的正确性,必须把所有可能的结果都保存下来,下图中右侧的s结果说明了这一点,它把x和y都放到了结果中,因为不知道c.f可能会指向什么。

analysis scope

回答了指针分析过程中需要分析哪些部分,全程序分析或者需求驱动的分析。全程序分析计算了所有指针指向的所有信息,如果感兴趣的只是第五行,那么可能只需要分析z就好了,这时需求驱动的分析更好。

concerned statements

只关注直接影响指针指向的语句,有一些类型的指针。

  • 局部变量指针
  • static field:类、class的指针,可以是global variable
  • instance field:建模为一个x指向的object;
  • array element:忽略数组的下标,看作一个对象;

pointer-affecting statements:能够影响指针的语句

  • New: x = new T();
  • assign: x = y;
  • store: x.f = y;
  • load: y = x.f;
  • call: r = x.k(a, …);

额外的:

  • 如果有复杂的调用,如a.b.c.d,可以分解为三地址码
  • 指针分析中virtual call是最复杂的,首先关注这个

pointer analysis Rules

指针分析中的域及其记法:

instance fields用O和F的乘积表示。pointer-to关系是一个映射,吧指针映射到指针集(O的幂集,原集合中所有的子集),就是方框中表示的。

对于new语句,创建一个对象,用oi表示创建出来的对象,让x指向oi。只要碰到这个语句,就把oi加入到pt(x)中。

assign的话,如果oi属于pt(y)的话,也让它属于pt(x)。

store:如果x指向一个语句oi,y指向另一个语句oj:

load:x.f指向oi了,oi的f域指向oj了,则让y指向oj

下图可以看到,对每一条Rule,横线上边的是前提,横线下边的是结论,下下图是汇总:

how to implement pointer analysis

指针分析用来生成指针的指向信息。类似下图中红线箭头的指向性信息,而且当指针变了的时候,指向性信息也会跟着变化。我们使用图将相关的指针联系起来,当pt(x)改变了的时候,将改变的部分同x的后继联系起来,将变化传播到x的后继。

pointer analysis algorithms

Pointer Flow Graph(PFG)是一个有向图,指明了对象间的指针指向关系。节点n代表了一个抽象对象或者变量,边e:x -> y表示指针x指向的对象可能会流向指针y(也由指针y指向),如下表所示,如果把y的值赋值给了x,那么就有一条边是从y指向x的。

下图便是一个画PFG的图,根据上边的定义,应该很好懂。通过PFG可以计算一个传递闭包,从而进行指针分析,比如e可以通过b到达,即e指向的对象也可以通过b指向。顺便加上了对b的初始化,这样更容易看出,pt(b)={oj}=pt(e)

实现指针分析算法有两个步骤:

  • 构建PFG
  • 将指针指向信息整合进PFG

下图是算法,可以看到也使用了worklist算法。worklist中包含了需要被处理的指针指向信息,WL∈<Pointer, P(0)>,每个worklist入口<n, pts>,是“指针,指向集”对。

下图将分析整个算法:



这里使用了一个差分的方法,解决了冗余的存在。

对于下面的程序:

1
2
3
4
5
6
7
1: b = new C();
2: a = b;
3: c = new C();
4: c.f = a;
5: d = c;
6: c.f = d;
7: e = d.f;

第一步对于其中所有的x = new T(),把[<b, {o1}>, <c, {o3}>]加入到WL中,然后对于所有的x = y形式的语句,构造边,加入PFG。

对于WL中的所有元素,首先把其中一个元素从WL中移除,第一个处理的是<b, {o1}>,调用Propagate函数,对b,pt(b)加入pts中的元素,再在WL中加上<a, {o1}>。对于c也是如此。

之后再处理c.f相关的边,直接加上。生成的PFG如下:

pointer analysis with methods calls

过程间分析需要call graph,对于函数调用的Rule:

调用图call graph构成了一个“reachable world”,从一开始入口函数就是可达的,其他的可达方法在分析的时候被逐步发现,只有可达的方法会被分析。总体算法:

addReachable方法扩展了reachable world。

ProcessCall的调用:

例子:对以下程序:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
class A {
static void main() {
A a = new A();
A b = new B();
A c = b.foo(a);
}
A foo(A x) { ... }
}
class B extends A {
A foo(A y) {
A r = new A();
return r;
}
}

一开始的时候WL为空,RM为空,CG为空。首先调用AddReachable函数把入口函数加入到可达图中,此时RM为{A.main()},在AddReachable仍需把main函数中的x = new T()形式的语句加入到WL中,WL中变为[<a, {o3}>, <b, {o4}>],再根据上边的指针分析算法进行分析。

CFL-Reachability and IFDS

Soundness and Soundines

Modern Pointer Analysis

Static Analysis for Security

Datalog-Based Analysis

Abstract Interpretation