断断续续看了南京大学的静态分析课程,总结一下,先贴一些资源
课程链接:
https://pascal-group.bitbucket.io/teaching.html。
作业内容:
https://tai-e.pascal-lab.net/en/pa1.html#_1-assignment-objectives
作业工程:
https://github.com/pascal-lab/Tai-e-assignments
关于Soot的资料:
https://www.brics.dk/SootGuide/sootsurvivorsguide.pdf
https://github.com/soot-oss/soot/wiki/Tutorials
Soot官方:
https://github.com/soot-oss/soot
下载soot jar包:
https://soot-build.cs.uni-paderborn.de/public/origin/master/soot/soot-master/
国内关于Soot的应用:
https://github.com/wh1t3p1g/tabby
简单理解静态分析就是在不运行程序的情况下对程序进行分析。静态分析的作用包括判断程序是否安全(空指针引用、内存泄漏、信息泄漏等)、增强对项目的理解(调用层次结构)、编译器优化(死代码消除)等。但是静态分析并不能给出具体的答案:是或否。也就是它不能肯定一定安全、一定不存在死代码等(赖斯定理)。静态分析可以给出的是可靠性(soundness)或完整性(completeness),对应的是漏报率(false negatives)或误报率(false positives)。这也涉及到在确保可靠性的同时,在分析精度和分析速度之间做平衡。
另外,课程用两个词来概括大多数的静态分析:Abstraction + Over-approximation
。中文翻译就是:抽象、过度近似。Abstraction把具体值抽象成了符号表示。
Over-approximation主要包括两部分:Transfer functions、Control flows。Transfer functions翻译过来即传递函数/转换函数,定义如何在抽象值上计算不同的语句。Control flows则把控制流过程中的变量用抽象值进行计算。
Transfer functions Control Flows
1. IR
IR(Intermediate Representation,中间表示),表示了高级语言的全部信息。所谓的编译过程是将高级语言转换成机器指令的过程,大致如下:
Source Code -> Scanner —(Tokens)—> Parser —(AST)—> Type Checker —(Decorated AST)—> Translator —(IR)—> Code Generator -> Machine Code
Scanner
阶段为词法分析(Lexical Analysis
),通过正则表达式(Regular Expression
)
Parser
阶段为语法分析(Syntax Analysis
),通过上下文无关文法(Context-Free Grammar
)
Type Checker
阶段为语义分析(Semantic Analysis
),通过属性文法(Attribute Grammar
)
经过上述过程,会将源代码转换成IR
的形式。IR之前的步骤被称为前端frontend。可以看到IR和AST阶段相比,更贴近机器码的形式,并且包含控制流信息,所以IR阶段是更适合进行静态分析的阶段。
3AC
IR的基本格式是三地址码格式(3-Address Code ,3AC)。三地址码的要求是:在一条指令的右边最多有一个操作符。“地址”可以理解为元素,每个指令里面包含三种元素:Name、Constant、Compiler-generated temporary
,即名称、常量和临时变量。
t2 = a + b + 3 // 不符合三地址码要求
// 三地址码格式
t1 = a + b // Name: a,b
t2 = t1 + 3 // Constant:3; Compiler-generated temporary:t1, t2
// 其他常见三地址码, x,y,z (地址,可以是三种元素之一);
x = y bop z //bop:二进制算术或逻辑运算
x= uop y // uop:一元运算(减、反、转换)
goto L // L:表示程序位置的标签
if x goto L // 跳转
if x rop y goto L // rop:关系操作符(>,<,==,>=,<=等)
IR是语言无关的,课程中采用的IR的实现是Jimple。Soot中的IR实现包括:Baf, Jimple, Shimple和Grimp。简单来看一个Jimple例子
// 源代码形式
public static void main(String[] args){
int x=0;
for(int i=0; i<10; i++){ x=x+1; }
}
// Jimple三地址码形式
public static void main(String[] args){
java.lang.String[] r0;
int i1;
r0 :=@parameter0: java.lang.String[];
i1=0;
label1:
if i1>=10 goto label2;
i1=i1+1;
goto label1;
label2:
return;
}
// 方法调用源代码形式
package org.examples;
public class MC{
String foo(String para1, String para2){
return para1 + " " +para2;
}
}
// 方法调用的3AC
java.lang.String foo(java.lang.String, java.lang.String){
org.example.MC r0;
java.lang.String r1,r2,$r7;
java.lang.StringBuilder $r3, $r4, $r5, $r6; // $代表临时变量
r0 :=@this: org.examples.MC;
r1 :=@parameter0: java.lang.String;
r2 :=@parameter0: java.lang.String;
$r3 = new java.lang.StringBuilder;
specialinvoke $r3.<java.lang.StringBuilder: void <init>()>(); // specialinvoke:call constructor\superclass method\private methods
$r4 = virtualinvoke $r3.<java.lang.StringBuilder: java.lang.StringBuilder append(java.lang.String)>(r1); // virtualinvoke: instance methods call
$r5 = virtualinvoke $r4.<java.lang.StringBuilder: java.lang.StringBuilder append(java.lang.String)>(" ");
$r6 = virtualinvoke $r5.<java.lang.StringBuilder: java.lang.StringBuilder append(java.lang.String)>(r2);
$r7 = virtualinvoke $r6.<java.lang.StringBuilder: java.lang.StringBuilder toString()>();
return $r7;
}
interfaceinvoke:cannot optimization, checking interface implementation
staticinvoke: call static methods
// 方法声明
method signture: class name\return type\method name(parameter types)
除3AC三地址码格式,还有一种IR的格式称为SSA(Static Single Assignment,静态单一任务)。
SSA中的所有赋值都是给具有不同名称的变量。它和3AC不同的是,每个变量都只有一个定义,每个定义都有一个新的名称。这种相对于3AC会提升一定的精度,但是会导致翻译成机器码时效率下降
// 3AC vs SSA
p=a+b p1=a+b
q=p-c q1=p1-c
p=q*d p2=q1*d
这部分内容可以在本地写一个类文件,如Test.class。然后从https://soot-build.cs.uni-paderborn.de/public/origin/master/soot/soot-master/下载对应版本的jar包,类和jar文件放在同一目录下,然后用如下命令生成Jimple文件。
java -cp sootclasses-trunk-jar-with-dependencies-4.1.0.jar soot.Main -f J -pp -cp . Test
2. Data Flow Analysis
CFG
CFG(Control Flow Graph,控制流图),是静态分析的基本结构。它其中的节点是一个个3AC的指令,或者一个BB(Basic Block,基础块)。
BB是连续三地址指令的最大序列,它需要满足的要求是:BB块中的第一个指令是该块的唯一入口,最后一个指令是唯一出口。构建BB的算法如下。
(1)3AC中的第一条指令是header
(2)条件或无条件跳转的目标是header
(3)紧随条件跳转的指令是header
把3AC指令转换成BB的Demo如下,根据构建BB的算法,一共12条3AC指令。首先3AC中的第一条指令,即1是header。其次,条件或无条件跳转(return)的目标包括7,12,3。这三条也是header。然后,包含条件跳转的指令是4,10,11。所以5,11,12作为紧随条件跳转的指令也是header。总结起来,header包括:1,3,5,7,11,12。然后将leader和它的所有后续指令(直到下一个header)组成BB。
3AC转换成BB,再转换成CFG
构建CFG
CFG的节点是BB,BB转换成CFG则是在BB之间添加边:对于顺序指令、条件跳转的情况,添加边,但是如果BB对应了无条件跳转,其后的BB不加边(例如B5和B6)。如上图右侧。边的BB之间就形成了前身(predecessor)和后继(successor)。另外,在构建CFG的时候会添加两个节点,入口Entry和出口Exit。它们不属于可执行IR。
数据流分析可以理解为数据如何在CFG上传递。主要的三种包括:(1)Reaching Definitions Analysis、(2)Live Variables Analysis、(3)Available Expressions Analysis
在理解数据流分析之前,先要了解一些基本概念:(1)输入输出状态State:每次IR语句的执行都将输入状态转换为新的输出状态。但是分析的时候根据控制流的方向不同可以分为:前向分析Forward Analysis和后向分析Backward Analysis。前向分析的符号表示为OUT[s] = fs(IN[s])
,后向分析为IN[s] = fs(OUT[s])
CFG是由BB连接起来的,每个BB可能包含多条statement。对于单个BB来说,
B=[S1,S2,...Sn]
,其控制流状态即为IN[si+1]=OUT[si],i=1,2,...,n-1
。对于多个BB之间来说IN[B]=IN[s1],OUT[B]=OUT[sn]
,图示如下Notations for Control Flow’s Constraints
Reaching Definitions Analysis
Reaching Definitions定义如下,也就是在p点定义了变量v,v=xxx
,在从p到q的路径中,v没有被重新定义("kill"),就认为v到达了q。可以表示为D: v = x op y
。
两个约束:它的Transfer Function(传递函数)可以定义为OUT[B] = genB U (IN[B] - killB)
;Control Flow控制流可以定义为IN[B] = Up a predecessor of B OUT[P]
。所谓gen
就是当前BB中定义的变量,kill
是此变量在其他BB中对应的Definition。示例如下:
在B1块中,gen
的变量是i,j,a
,对应的就是d1,d2,d3
。kill
的就是其他具有i,j,a
的地方,其他具有i
:d4,d7
;其他具有j
:d5
;其他具有a
:d6
。所以kill
的集合是d4,d5,d6,d7
。
在B2块中,gen
的变量是i,j
,其他具有i
:d1,d7
,其他具有j
:d2
,所以kill
的集合是d1,d2,d7
。以此类推。
Reaching Definitions Analysis算法如下
Reaching Definitions Analysis算法
算法Demo
Reaching Definitions Analysis算法Demo
同一个变量用相同的颜色表示,例如D2和D4都是红色代表y。每个变量Definition初始设为0
D1 D2 D3 D4 D5 D6 D7 D8
0 0 0 0 0 0 0 0
根据算法,每一个OUT[B]都初始化为空,也就是每个BB的OUT都设为00000000
。
(1)B1
然后开始计算B1的OUT[B1],根据Transfer Function的定义OUT[B] = genB U (IN[B] - killB)
进行计算,此时的IN为0000000
,genB为11000000
(因为此时D1、D2有定义),killB应该kill包含x,y的Definition,如D4,D5,D7,但是这三个目前的Definition都为0,kill后还是为0,所以killB还是0000000
。最终得到的OUT[B1]=11000000 U 00000000
=11000000
。U
为或运算。
(2)B2
先算B2的IN,根据定义IN[B] = Up a predecessor of B OUT[P]
,先找到B2所有的前驱进行U
操作。B2的前驱包含B1和B4,二者的OUT进行U
操作,即11000000 U 00000000
。此时的IN[B]=11000000。
为了计算OUT,先算一下killB,B2的m和y,只在D2中有。所以要在IN[B]的基础上kill D2,即变为10000000
,再genB00110000
,二者进行或运算,最终OUT[B2]结果为10110000
。因为B3和B4的前驱都只有B2,所以IN[B3]和IN[B4]的值就为OUT[B2]
(3)B3
计算B3的OUT要先从IN的10110000
中Kill掉具有x的D1、D5,IN中的D5本身就是0,只killD1就可以了,即变成00110000
,再与D7做或运算,得到OUT[B3]=00110010
(4)B4
其他具有x,z的:D1、D7、D8。IN是B2的OUT,从IN中kill D1、D7、D8,得到00110000
。再与D5、D6做或运算,得到OUT[B4]=00111100
(5)B5
B5的前驱包含了B4和B3,需要先对前驱的OUT做或操作。也就是00111100 U 00110010
,得到IN为00111110
,然后kill掉z对应的D6,得到00111010
,再gen D8,00111011
至此,完成了第一轮的遍历。
根据算法要求,如果有任何的BB的OUT发生了变化,就需要再进行遍历。最终进行了三轮遍历。
所有绿色的都是Final analysis result。这个序列代表哪个D能到达BB,例如B1最终结果是D1,D2能够到达。B3是D3,D4,D6,D7能够到达。每个应用点都关联了一个data-flow value(D序列),它代表了能否到达这个点的抽象。
迭代算法为什么最后会停止?首先gen和kill是固定不变的。在第二轮的时候,IN可能发生变化(more facts):0->1 , 1->1
,不可能1->0,因为要kill的在第一轮就会kill,也就是OUT只会增长,不会变小。所以最极端的情况,就是所有的位都变成了1,那么也会停下来。
Live Variables Analysis
Live Variables Analysis直译过来为存活变量分析。简单来说就是判断变量v在程序的某一点是否是Live的。图示如下:
Live Variables Analysis
在一条路径上有使用变量v的地方,并且在使用前v没有被重定义,就认为v在程序点p是live的。Live Variables的应用之一就是编译优化,比如可用于寄存器分配。即在某些情况下,所有寄存器都已满,我们需要使用一个寄存器,那么我们应该倾向于使用具有dead value的寄存器。
这种方式针对的是程序中的Variables而不再是Definition。这种方法适用于逆推,首先找到use(v)的地方,即下图中的S1,然后向上寻找v被定义的P。很容易看出OUT[B]应该是IN[S]的集合,但是IN[B]的算法,就要分场景来看:
(1)v被重新定义了 -> IN[B]={ }
(2)B中用到了v -> IN[B]={ v }
(3)B中用到了v并且v也被重新定义了 ->看是先使用v还是先进行了重定义 -> IN[B]={ v }或IN[B]={ }
但是在下图的IN[B]计算公式可以和Reaching Definition Analysis进行比较。Reaching Definition Analysis是正向的推导OUT[B] = genB U (IN[B] - killB)
。Live Variables Analysis是逆向的推导IN[B]=useB U (OUT[B] - defB)
。二者极为类似,都是先用集合去除要kill的或重定义的,然后并上用到的。
对应的算法代码如下,同为may analysis,初始化都为空。存活变量分析算法是逆推算法,所以设IN[exit]为空
Live Variables Analysis算法
Demo如下,此处的变量序列如下。存活变量分析中所有的变量都会被纳入序列中。但是Reaching Definitions Analysis
只会把等号前被定义的变量放入序列。
x y z p q m k
0 0 0 0 0 0 0
Live Variables Analysis Demo
(1)B5
第一轮,Exit初始化为空,先逆推B5。根据逆推公式,
IN[B5]=UseB U (OUT[B] -def[B])
,此时的OUT[B5]是空,Use是p,def是z,只需要和UseB的p做或运算。得到001000
。(2)B3
B3的OUT是B5,即
001000
,use的是x,def的也是x。先减去def的x,再和use做或运算,得到IN[B]:1001000
(3)B4
OUT[B4]是IN[B5]和IN[B2]的集合,因为这两个都是它的后继。此时的IN[B2]还是空,那么此时的OUT[B4]就是IN[B5]的值
0001000
,use的是y,def的是x、q,即减去x,q,和y做或运算得到0101000
。(4)B2
OUT[B2]要对IN[B3]和IN[B4]做或运算,即
1001000 U 0101000
=1101000
。B2中要def的是m和y。use的是k。但是在变量中为什么没有use m?这个在前面的定义中提到过,需要看变量是先使用还是先定义。此处的m是在先重新定义再使用的,所以不算use。得到IN[B2]
1001001
(5)B1
OUT[B1]即为IN[B2]的值
1001001
,def的是x,y,use的是p,q,z,计算得到0011101
。第一轮到此计算完成
有任意的BB的IN发生了变化就需要再次进行遍历。显然每个BB和初始化的0都不同了,就需要开始第二轮。最终的三轮结果如下。
三轮结果Available Expressions Analysis
Available Expressions Analysis直译为可用表达式分析。定义是:如果(1)从入口到p的所有路径都必须经过x op y
的计算,并且(2)在x op y
的最后一次计算之后,没有对x或y的重新定义,则表达式x op y
在程序点p处可用。Available Expressions Analysis可以用于检测全局表达式。
Available Expressions Analysis图示如下:表达式整体作为向量,IN的时候表达式是a+b
,但是在BB中,a被重新定义了,按照规则需要删除任何包括a变量的表达式,即删除a+b
。gen的是x op y
,最后求并集OUT即为x op y
课件中给了一个小例子来判断表达式是否是Available的,直觉上左边的path,x被重定义过了,像是Unavailable的。但是根据上面Available Expressions Analysis的定义:在x op y
的最后一次计算后,没有对x进行重新定义(此处的重定义是在计算前的,符合定义)。并且由于定义要求所有路径都必须经过x op y的计算,所以路径最终要取交集,而不是前面两种分析的并集。由于左右两条路都是Available的,那么认为该汇聚点是Available的。
Available Expressions Analysis算法如下
这里有一点不同:所有OUT[B]都初始化为1。
U
符号代表All。前两个分析都是may分析,但Available Expressions Analysis是must类的分析。must的初始化为1。算法demo如下:
Available Expressions Analysis算法Demo
(1)B1
B1的IN是00000
,kill含y的表达式。然后和p-1
取并集。得到10000
(2)B2
B2的前驱包含B110000
和B411111
,二者取交集(与)得到10000
。kill含k和p的表达式,genz/5
和e7*x
。操作得到01010
继续运算,直到各个B的OUT不再变化。
这三个数据流分析的方法,以x=p+q
为例。一个针对Definition,即x;一个针对Variable,其中的p,q;一个针对Expression,即p+q
。
数据流分析理论
课程的第五讲和第六讲主要是讲了数据流分析中的理论,包括迭代算法、偏序、上下界、格、单调性与不动点定理、MOP、常量传播、Worklist算法等内容。
迭代算法
一个May&Forward分析的算法如下图左上所示。简单来说就是一个CFG拥有k个节点,每一次迭代都更新每个节点的OUT。这样所有的节点就形成了一个K元组(OUT[n1], OUT[n2], ..., OUT[nk])
。或抽象成(V1 ×V2 ...×Vk)
,那么每一轮利用传递函数和控制流处理,将Vk中的一个元素抽象为Vk中的一个新元素(函数F: Vk→Vk
)。直到两个连续的K元组相同时迭代结束。
Xi=F(Xi)
时就认为X是一个不动点,整个迭代算法也达到了不动点。
由此也有了一系列疑问:算法是否一定能终止迭代(或者说到达不动点)?如果有不动点是只有一个还是不止一个?我们的解决方法是最好或最准确的么?算法会在什么时候达到不动点?回答这一系列问题前,就涉及到一些数学知识。
偏序(Partial Order)
偏序集(poset)被定义为一对(P,⊑)
,其中⊑
是一个二元关系,定义了P上的部分排序,⊑
具有以下属性:
(1)自反性Reflexivity: ∀a∈S,有a≤a;
(2)反对称性Antisymmetry:∀a,b∈S,a≤b且b≤a,则a=b;
(3)传递性Transitivity:∀a,b,c∈S,a≤b且b≤c,则a≤c;
所谓的二元关系,是两种事物之间的联系,例如算术中的大于、等于;或者几何学中的子集。自反性可以简单理解为等于、小于等于、大于等于、整除等(a≤a);反对称性,简单理解为a≤b且b≤a,则a=b
;传递性比较好理解,a≤b且b≤c,则a≤c
。
课程中给了几个例子
(1)例子1,假如偏序代表<
小于号,S是整数集合,问S是否为偏序集。答案是不是,首先就不满足自反性,1<1
是不成立的。
(2)例子2,假如偏序代表子集,S是英文单词的集合,如下左图。问S是不是偏序集。对于自反性,可以理解为对于每一个字符串,是不是自己子集的字符串。反对称性,可以理解为A、B两个字符串互为彼此的子集,那么两个字符串是相等的。下面这个例子也说明了偏序只是需要部分满足,不要求所有元素都满足。比如sin和singing是满足条件的,pin和sin不满足条件。但只要有部分满足就符合偏序。
(3)例子3,假如偏序代表子集,S是一个power set幂集(原集合中所有的子集(包括全集和空集)构成的集)。如下右图。所以例子2、3都满足偏序。
上界和下界(Upper and Lower Bounds)
least upper bound(最小上界,缩写为:lub,也称为join),可以写为⊔S
;greatest lower bound(最大下届,缩写为:glb,也称为meet),可以写为⊓S
。如果S中包含两个元素a,b,那么最小上界可以写为a ⊔ b
,即the join of a and b。同样,最大下届可以写为a ⊓ b
,即the meet of a and b。图示如下:
PS:不是每个poset都有最小上界和最大下界,如果有的话一定是唯一的。以上图的S自身为例,就没有glb(最大下界),因为空集并不在S中。证明唯一性可以利用反证法,假设g1,g2都是最大下界,那么按照偏序集定义,g1⊑(g2 =⊓P) and g2⊑(g1 =⊓P)
,那么g1=g2,也就是唯一。
Lattice(格)
格:如果偏序集的每一对元素都有最小上界和最大下界,则该偏序集就是格。如果对上述偏序中的三个例子进行是否为Lattice的判断。例子1是,例子2不是。例子3是。因为在例子2中,pin和sin就不存在最小上界,不满足每一对元素都有最小上界和最大下界的条件。
Semilattice半格:只存在最小上界或最大下界中的一个。如果存在最小上界,就称为join semilattice。如果存在最大下界,就称为meet semilattice
Complete Lattice全格:对于一个格,其任意子集的最小上界和最大下界都存在。Lattice是任意两个元素,而Complete Lattice是任意子集。后者要求更严格。对于上述偏序中的三个例子来说,例子1不是,例子2不是,例子3是。例子1中定义的是整数集合,而整数的个数可能是无穷的,所以想求上界的时候可能也是无穷的,不满足存在最小上界的要求。例子3是。对于全格来说,它有一个最大元素T
被称做top和一个最小元素⊥
被称作bottom。
每个有限格(元素有穷)都是一个全格,但一个全格不一定是有限格。一般程序中用到的是Complete Lattice全格。
Product Lattice:对于给定格,L1 = (P1,⊑1),L2 = (P2,⊑2),…, Ln = (Pn,⊑n)
,如果对于所有i, (Pi,⊑i)
有⊔i
(最小上界)和⊓i
(最大下界),那么我们可以有一个积格Ln = (P,⊑)。相关性质如下:
P=P1×...×Pn
(x1,...,xn)⊑(y1,...,yn)⟺(x1 ⊑y1)∧...∧(xn ⊑yn)
(x1,...,xn)⊔(y1,...,yn) = (x1 ⊔1 y1,...,xn ⊔n yn)
(x1,...,xn)⊓(y1,...,yn) = (x1 ⊓1 y1,...,xn⊓n yn)
如果Product Lattice中的每一个Lattice都是全格,那么这个Product Lattice也是全格
Data Flow Analysis Framework via Lattice
Data Flow Analysis Framework via Lattice这个图的形容是:Data flow analysis can be seen as iteratively applying transfer functions and meet/join operations on the values of a lattice。可以看出从s1到s2,是从Lattice的Bottom向上走的,经过join操作的到Lattice的{a,b},再经过transfer functions,得到Lattice的最小上界。所以数据流分析可以认为是在Lattice上应用Transfer functions和meet/join操作。
有了这些数学知识,就回到介绍偏序之前的那些问题,(1)算法是否一定能终止迭代(或者说到达不动点)?如果有不动点是只有一个还是不止一个?我们的解决方法是最好或最准确的么?算法会在什么时候达到不动点?
对于第(1)个问题。在上面介绍算法的时候提到OUT中的0可能变成1,但1不会变成0。所以最后有终点。如果要更通用的来看这个问题,则要用单调性monotonicity来解释。对于第(2)个问题,x=f(x)的时候,函数能达到不动点。但是不动点可以有多个。即x=f(x)有多个x满足条件。如下图。
不动点
那么想要回答第(3)个问题,就需要了解单调性和不动点定理。
Monotonicity 单调性
如果格是单调的,那么x ⊑ y ⟹ f(x) ⊑ f(y)
,简单理解就是x<=y的话,f(x)<=f(y)
Fixed Point Theorem 不动点定理
Fixed-Point Theorem如果Complete Lattice是单调的,并且Lattice是有限的(finite,那么这个肯定个是全格,但全格不一定是有限的)。去寻找最小不动点的方法是:
先找到bottom,然后不断通过f()去迭代bottom,那么达到不动点的那一刻就是最小不动点。同样,先找top,然后不断迭代,达到不动点那一刻就是最大不动点。
这个方法可以用如下的方式来证明是正确的。要证明首先(1)不动点存在,其次(2)不动点是最小/最大的,即是最优的。对于(1)的证明:每个Lattice都有bottom和top。以bottom为例,f(bottom)也是Lattice上的值,而bottom是Lattice上的最小值,所以bottom⊑f(bottom)。然后根据单调性,f(bottom)是不断增大的,但由于有限性,Lattice存在一个边界,最终证明不动点。
Fixed-Point Theorem (Existence of Fixed Point)对于(2)的证明,既然要证明最小,就可以假设有一个其他的不动点存在。利用数学归纳法(Induction)来证明。数学归纳法的证明步骤大致为:先设置初始条件,例如f(1)=xx,然后假设在第i次时成立,然后证明i+1次也成立。证明如下
Fixed-Point Theorem (Least Fixed Point)
那么再回答第(3)个问题的时候,如果不动点不止一个,怎么判断我们的解决方法是否为最好的,那么就要看我们的是否为greatest或least的不动点。
那么如何把算法和不动点定理关联起来?图示如下
算法到达不动点从Lattice的角度来看May和Must Analysis。如下图。对于May来说,最开始认为所有的Definitions都不可达,此时是unsafe的,但是如果达到了top,虽然变安全了,但是越来越不准,因为认为所有都可达,相当于没有计算。对于不同类型,May、Must Analysis来说,最准的点也不同。基于May来说是Least Fixed Point,对于Must来说,是Greatest Fixed Point。
May and Must Analysis in Lattice view从Entry到Si可能有很多条path,每条path可以被写为P=Entry-> S1 -> S2 ->...-> Si
。如果要定义整个Path的Transfer function,fsi-1的OUT就是si的IN,也是这条path的Transfer function的结果。MOP则是枚举Entry到Si的所有path。把三条Fp(Transfer function的结果)进行meet/join操作。所以MOP认为是在每个路径的末尾计算数据流值,并进行meet/join找到最小上界lub/最大下界glb。
静态分析虽然考虑了所有的可能路径,但是在实际执行过程中,有些路径是永远不会被执行的,也就是not executable的。但是静态分析会把所有的path结果都meet/join,所以认为是not fully precise(不完全准确的)。假设路径中还包括循环,静态分析可能是Unbounded(无限循环)或者not enumerable(不可枚举的),这就认为是impractical(不实际的)
我们之前用的算法是在所有汇合点都用join,但是MOP则是在最终点才会将结果join。算法和MOP之间的比较如下
与MOP的比较
根据最小上界的定义,所以x U y即是x的上界也是y的上界。由于F是单调的,那么x<y的话,f(x)<f(y)。根据这个推导,具体的比较如下。也就是当F是单调的时候,MOP是比我们的算法要精准的。当F是distributive的时候,是一样准的。前面提到的需要kill/gen的都是distributive的分析方法。但是有的就不是,比如Constant Propagation
算法和MOP的比较
常量传播(Constant Propagation)
给定在程序点p处的变量x,确定x是否保证在p处保持恒定值(常量)。是个must型的分析。CFG中每个节点的OUT包含一组对(x, v),其中x是一个变量,v是该节点后x所持有的值。根据上面提到的data flow analysis framework(D,L,F),生成一个Lattice包括Values和operator(⊓ or ⊔ ),并且要定义一个Transfer Function。示例如下:
Constant Propagation – Lattice首先是生成Lattice。NAC:not a Constant(不是常量)。UNDEF:undefined。v:值。c:常量。如果左边来个一个x=1,右边也是一个x=1,汇聚到一起就是常量。即c ⊓ c=c
。但如果左边是x=1,右边是x=2,汇聚到一起就变了不是一个常量。所以c1 ⊓ c2 = NAC
然后是定义Transfer Function,{Variable,Variable的值}
,_
代表通配符。val(x)
代表对变量x进行取值。x=y op z
,用f(y,z)来算这个值。判断这个是否为常量,需要分情况讨论,如果val(y)和val(z)都是常量,那么计算结果为常量。如果其中一个是NAC,那么结果就是NAC。如果有一个是UNDEF,那么结果就是UNDEF。
上面提到如果算法是distributivity的,那么我们的算法和MOP结果是一致的,如果是nondistributivity,那么结果就不一致。二者的计算区别在于是否先meet/join。以下面的例子来说,在c这个点,我们的算法,先meet/join。那么a就是1和9进行meet。根据Constant Propagation – Lattice的图示,c1 ⊓ c2 = NAC
,当a进行meet的两个值不同时得到的是NAC。b同理。那么c=a+b
,根据上面Constant Propagation – Transfer Function的图示,对于x=y op z
来说,如果有y和z有一个是NAC,那么x就是NAC。所以此时的c也是NAC。MOP则是要先对值计算完了,再进行meet。那么就是10和10进行meet。结果认为是常量10。
Worklist Algorithm
工作列表算法(Worklist Algorithm)是迭代算法Iterative Algorithm的优化。它只遍历有变化的Function进行遍历。而不是只要OUT有一个变了就要把所有的BB进行迭代。算法一开始把所有的BB都放入到Worklist中,计算出的新的OUT和旧的OUT进行比较,如果产生了变化,就把B的后继successor加入到Worklist中。
Worklist Algorithm
过程间分析 Interprocedural Analysis
上述算法研究的都是过程内的分析,以下面这个例子来说,x的来源会认为是NAC,并且y=NAC,n=NAC。但是如果能将x=42真实地带入到bar方法中。就可以得到精确的值:x=42,y=43,n=10
。这就涉及到方法之间的调用,来保证方法之间传递数据的精确度。
void foo(){
int n= bar(42);
}
int bar(int x){
int y=x+1;
return 10;
}
程序间的调用关系用调用图来表示,它是一组从调用点(call-sites)到目标方法(target methods,callees)的调用边的集合。
Call Graph控制流图是程序分析、调试的基础。调用图构造有四种主要方法:Class hierarchy analysis
(CHA,类层次分析)、Rapid type analysis
(RTA,快速型分析)、Variable type analysis
(VTA,变量分析)、Pointer analysis
(k-CFA,指针分析)(从左到右,速度逐渐变慢,精确度逐渐变高)。
Java主要有三种调用方法。3AC部分提到过,Static call是调用静态方法,Special call包括构造方法、私有方法和父类方法。其他的方法都被称为Virtual call。Virtual Call的方法调度是基于(1)接收对象的类型 (2)方法签名(Signature,标示符)。
• Signature = class type + method name + descriptor
• Descriptor = return type + parameter types
Method Calls
Method Dispatch of Virtual Calls
Method Dispatch(方法调度)是指在面向对象编程中,如何决定在调用一个方法时哪个实现(implementation)会被执行的过程。Virtual Calls只有在运行时才能得到准确的信息。例如o.foo(...)
,需要知道o
的具体类型,和foo()
的method signature。所谓的signature包括如下:方法的class类型、方法名、返回类型和参数类型。
Method Dispatch
函数Dispatch(𝑐,𝑚)
用来模拟运行时Method Dispatch过程。Dispatch的目的是找到一个能被调用的目标函数。但面向对象语言中,方法能被调用的前提是方法是非抽象(non-abstract)的。
(1)如果类c中包含一个non-abstract方法m'
,且m'
和m具有相同的name、descriptor。那么就相当于找到了要被调用的函数,返回m'
(2)如果类c中没有找到对应方法,就在c的父类c'
中寻找,如果还没有找到就在c'
的父类中寻找。依次类推直到找到对应方法。
下面有个例子来熟悉Dispatch(𝑐,𝑚)
,A、B、C之间是父类的关系。
class A{
void foo(){...}
}
class B extends A{}
class C extends B{
void foo(){...}
}
void dispatch(){
A x=new B();
x.foo(); // Dispatch(B, A.foo())=A.foo(),B中没有foo方法,所以调用父类A中的方法方法
A y=new C();
y.foo(); // Dispatch(C, A.foo())=C.foo(),C中有同name和descriptor的方法,所以调用C中的方法
}
Class hierarchy analysis类层次分析
CHA的特点是需要整个程序的类层次结构信息(继承结构)。然后根据declared type和receiver variable来处理Virtual Call。
A a=... //声明变量的类型是A,即使A a=new B();,声明变量的类型也还是A
a.foo(); // a就是receiver variable
a可能指向a或a所有子类的对象,需要通过查找A的类层次结构来解析目标方法。CHA的具体解析方法是:定义Resolve(cs)
来解析可能的目标方法。cs表示call-site调用点。
CHA分别考虑static call、special call、virtual call三种调用方法的处理。static直接是m。另外,上面Method Calls中提到special call要处理三种情况:构造方法、private方法、父类方法。对于构造方法和private方法来说,Dispatch结果其实就是m。但是对于父类方法来说不是。所以处理special call还是采用了Dispatch方法来涵盖这两种情况。对于virtual call来说,需要对它自身,子类,和子类的子类等进行Dispatch!!。
这里需要注意是进行Dispatch,而不是查找(因为查找只在当前类)。Dispatch在上面提到如果当前类中没找到对应方法,会去父类寻找。
// (1) static call
class C{
static T foo(P p, Q q){...}
}
C.foo(x, y); // cs:C.foo(x,y); m: <C: T foo(P,Q)>
// (2) special call 父类方法
class C extends B{
T foo(P p, Q q){
...super.foo(p,q); // cs:super.foo(p,q); m:<B: T foo(P,Q)>
}
}
// (3) special call private方法
class C extends B {
T foo(P p, Q q) {
...
this.bar(); // 类似static call
}
private T bar()
}
// (4) special call 构造方法
C c = new C(); // 类似static call
// (5) virtual call
class A{
T foo(P p, Q q){...}
}
A a=...
a.foo(x,y); // cs: a.foo(x,y); m:<A T foo(P,Q)> c:A
一个CHA的具体例子:
class A{
void foo(){...}
}
class B extends A{}
class C extends B{
void foo(){...}
}
class D extends B{
void foo(){...}
}
void resolve(){
C c=...
c.foo(); // Resolve(c.foo())={C.foo()} 因为当前类C存在foo方法,并且C没有子类
A a=...
a.foo(); // Resolve(a.foo())={A.foo(), C.foo(), D.foo()},A存在foo,且其子类C,D也存在foo。
B b=new B();
b.foo(); // Resolve(b.foo())={A.foo(), C.foo(), D.foo()},B不存在foo,所以在进行Dispatch时会查找父类
}
Dispatch时如果当前声明类有对应方法,就输出当前类的方法,没有找到才会去父类查找方法。而且由于CHA是根据声明类来查找,所以B b=new B
和B b=new C()
没有区别,都是要根据声明变量B类型来查找。所以它的劣势是不精准,容易引入这种伪目标方法。但是优势是速度快,只需要考虑声明变量的类型,忽略数据流和控制流信息。
PS:IDEA就是用CHA的方法来解析目标方法,长见识了!
IDEA与CHA
如何用CHA构造程序调用图?
上面说的是如何用CHA来构造一个调用点。而CHA来构造调用图是从入口方法开始(重点关注main方法),调用过程中的可达方法(对应调用边),对每个可达方法利用CHA来解析call-site(Resolve(cs)
),直到没有新的方法被发现。具体的CHA构造调用图的算法如下
WL代表Worklist,代表需要被处理的方法。CG是调用图集合所有的边。RM是可达方法的集合(也就是该方法分析过了不用再分析了)。先对这三者进行初始化,只要WL不为空就一直循环:从WL取一个方法出来,如果该方法不在RM集合中,也就是个新方法,首先将方法加入到RM集合,然后遍历这个方法中的每一个call-site调用点,用Resolve(cs)来处理得到目标方法m'
的集合T。然后再对T进行遍历,将其中的调用边加入到调用图中,并且将m'
加入到WL。
一个例子如下:
(1)WL先把main方法取出来,里面方法m是A.foo()。由于foo是一个静态方法,所以处理直接得到m,即
Resolve(A.foo())={A.foo()}
。然后把A.foo()
也加入WL。(2)下轮循环时从WL取出
A.foo()
。里面方法是a.bar()
。bar()是一个virtual call,那么对当前类和子类进行Dispatch的到Resolve(a.bar())={A.bar(),B.bar(),C.bar()}
,将三者放入WL。并且将a.bar()
和A.bar()、B.bar()、C.bar()
的边连接起来。(3)下轮循环时取出
A.bar()
,里面方法是c.bar()
,声明类型C具备foo方法且没有子类,所以Resolve(c.bar())
得到的就是C.bar()
,加入到WL。此时的WL变成{B.bar(),C.bar(),C.bar()}(4)下轮循环时取出B.bar(),但是B.bar()中是个空,没有方法。直接取WL的下一个值,C.bar()
(5)取出C.bar(),里面方法是
A.foo()
,由于foo是静态方法,Resolve直接得到A.foo(),放入WL,此时WL变成{C.bar(),A.foo()}(6)取出C.bar(),上一轮已经处理过了,即存在于RM了。直接取WL的下一个
(7)取出A.foo(),之前也处理过了,这轮循环也直接跳过,那么WL已经为空了,算法结束。最终得到的调用图如上图所示。
Interprocedural Control-Flow Graph过程间控制流图
CFG表示单个方法的结构,ICFG表示整个程序的结构。通过ICFG,我们可以进行程序间分析。ICFG = CFGs + call edges & return edges
。这两种edges的信息来自调用图call graph。
call edges(调用边):从调用点到被调用点的入口节点
return edges(返回边):从被调用方的退出节点到其调用点后面的语句
void foo() {
bar(...); // call site:调用方法的语句
int n = 3; // return site:紧跟着调用语句的叫return site。那么return edge就是从bar的返回语句连到int n=3
}
一个ICFG的例子如下,黑色的是cfg。蓝色的是call edges,红色的是return edges。
main中涉及的调用点:addOne、ten。这两个是call site。
b=addOne(a)
的下一句c=b-3
就是return site。连接到对应的方法后,方法结束时连回到return site。b=addOne(a)
和c=b-3
之间的直连边叫做call-to-return edges
,用于传递本地数据流(main方法中的变量是local的)。根据下图可以看出如果二者之间没有连线,那么a就需要随addOne进行了一圈传递,但实际上local的变量并不需要进行多次传递。这种设计更为高效
Interprocedural Data-Flow Analysis过程间数据流分析
顾名思义就是:基于程序间控制流图(ICFG)的方法调用分析整个程序。
Intraprocedural 过程内 | Interprocecdural 过程间 | |
---|---|---|
Program representation | CFG | ICFG = CFGs + call & return edges |
Transfer functions | Node transfer | Node transfer + edge transfer |
相比而言,只是比CFG多了Edge transfer。它分为两种:
• Call edge transfer: 将数据流从调用点转移到被调用的入口节点(传参数)
• Return edge transfer: 将数据流从被调用方的出口节点转移到返回点(传返回值)
• Node transfer: 和过程内类似,但是对于方法调用节点b=addOne(a)
,要kill左值b
,因为真正值是从addOne(a)的结果流回来的。
过程间数据流分析示例如下(以常量传播为例):
过程间数据流分析示例
b=ten()的OUT需要kill b,理由是b的值会随着return 10返回。如果没有killb,也就是保留b=7,那么在b=ten()和return 10交汇的时候会对7和10进行meet。那么会认为b不是一个常量。但实际上b=10就是一个Constant。所以在OUT时先kill b。避免精度上的损失。这个例子解释了两个问题,(1)b=addOne(a)和c=b-3之间的cfg边为什么要保留 (2)为什么OUT时要kill b。
通过例子也可以看出过程内分析是很保守的,对于b=addOne(a)会认为b是NAC,即认为不是常量。那么c=b-3也会因为b是NAC,而导致c也是NAC。而过程间分析则较为精确。
网友评论