Overview & Preliminaries
两类分析:
- may Analysis:over-approximation
- must Analysis:under-approximation
实际上都是为了safety of analysis。
对数据流分析的几种解释
解释一:
An analysis to figure out “how application-specific Data Flows through the Nodes(BBs/statements) and Edges(control flows) of CFG(a program)?”
对于application-specific data,由对变量或表达式抽象(Abstraction)表示;对于Nodes,由Transfer function处理;对于Edges,有Control-flow handing处理。
Abstraction、Transfer function和Control-flow handing是设计一个数据流分析的三个关键要素。
解释二:
In each data-flow analysis application, we associate with every program point a data-flow value that represents an abstraction of the set of all possible program states that can be observed for that point.
控制流分析即给出每一个程序点一个控制流的值,该值是表示在该点能分析到的所有可能结果的抽象表示。
解释三:
Data-flow analysis is to find a solution to a set of safe-approximation-directed constraints on the IN[s]’s and OUT[s]’s, for all statements $s$.
控制流分析即在safe-approximation规则(may or mast)约束下,解出每一个statements的IN和OUT。
这里的IN和OUT指每一个语句的输入和输出。
这里的约束包含了语义(转换函数)和控制流信息(Control-flow Handing)。
转换函数(transfer function)
分析单个BB的函数,存在前向分析和后向分析:
前向分析(Forward Analysis)
$Out[s]=f_s(IN[s])$后向分析(Backward Analysis),将CFG反向等于Forward
$In[s]=f_s(OUT[s])$
控制流信息处理(Control-flow Handling)
定义数据流在BBs间的流动方式,控制流中的BBs存在三种情况:
后两种情况存在交汇(meet)操作(第二种后向分析存在)
对于第三种情况下的前向分析,B的IN是所有入向的代码块OUT的meet;对于第二种情况下的后向分析,B的OUT是所有出向代码块IN的meet。
Reaching Definitions Analysis
A definition $d$ at program point $p$ reaches a point $q$ if there is a path from $p$ to $q$ such that $d$ is not “killed” along that path.
对于在程序点 $p$ 处变量v的定义d,检测其在$ p\sim q$的路径上是否有新的定义(可以用于空指针问题)
算法设计
Data Flow Values
用bit vecotr表示集合,集合中元素表示每一到达该点的语句
e.g. D1, D2, … , Dn=01…0 (表示D2定义在当且位置有新定义)定义Transfer Function和Control-flow Handing
Transfer Function:
对于一个定义语句D: v = x op y
,kill(在集合)与v相关的其他语句,并在集合中加入D,即:Control-flow Handing:
当多个代码块汇聚时,合并所有的定义(may)应用经典的数据流分析算法框架(Iterative algorithm)
遍历结果
为什么能到不动点(fixed point)
再次考虑Transfer Function:
- 因为 gen和kill是不变的
- 当新的变化进来时,经过kills,存在$survivor_s$加入OUT[S]
- 因此那些加入到OUT[S]的新变化,要么来自于gen,要么来自于$survivor_s$,而这些变化将永远保留(集合中永远存在这些位置)
- 因此OUT的变化是单调增的(只会0->1,1->1)
总结下来,每个BB的Transfer Function是一个单调增函数,又因为值域是有上限的(最大不动点),因此算法最终会停止。
Live Variable Analysis
Live variables analysis tells whether the value of variable $v$ at program point $p$ could be used along some path in CFG starting at $p$. If so , $v$ is live at $p$; otherwise, $v$ is dead at $p$.
对于在CFG语句 $p$上定义的变量 $v$ ,在$p$语句执行前变量$v$的值在后续执行中还被读取($v$ 在使用前不被重新定义),那么称 $v$ 在 $p$ 上是活跃变量。
(使用场景:寄存器用完之后,检查哪个寄存器可以被清除——若寄存器中的变量dead)
算法设计
Data Flow Values,依然用bit vector,注意这次记录变量
如:V1,V2,…,Vn=01…0 (V2在p上的定义被使用i.e.,不能清空V2寄存器)定义Transfer Function和Control-flow Handing
讨论forward还是backward,把变量当寄存器想,当决定一个寄存器是否可以清空的时候,需要往后看,后面的程序是否用到这个寄存器,因此用backward。
Transfer Function:
其中,$IN[B]$指v在B中重定义前被使用,$OUT[B]$指v在B代码块中没有重定义,$def_B$指v在B中被重定义。
Control-flow Handing:
may analysis,依旧是∪:
不动点算法
分析结果
Avaliable Expression Analysis
An expression $x \text{ op } y$ is available at program point $p$ if (1) all paths from the entry to $p$ must passthrough the evaluation of , $x \text{ op } y$and (2) after the last evaluation of $x \text{ op } y$, there is no redefinition of $x \text{ op } y$.
表达式 $x \text{ op } y$ 为availbable 当且仅当 (1)所有路径都经过 $x \text{ op } y$ (2)最后一个计算 $x \text{ op } y$ 后,不再有 $x$ 和$y$ 的重新赋值。
如果表达式available,则优化最后一次的计算,例如:
c可以被优化,例如,将a,b,c全转化为y,最后一步则不用计算(不论走什么分支,最后的t都不用计算)
算法设计
Data Flow Values
available的表达式集合,可用bitVector表示,如:E1,E2,…,En=01…0(E2为available)
定义Transfer Function和Control-flow Handing
Transfer Function:
这里的$kill_{B}$指删除表达式,这些表达式的变量在当前块B中被重新定义。
Control-flow Handing:
must analysis,由“∪”变成了“∩”
算法,注意每个bb的初始化,变成了“All”,即初始状态所有表达式都是available的(反向思维,如果初始化为0,那么$\cap$后恒为0,计算无效)
综合比较
Reaching Definitions | Live Variables | Available | |
---|---|---|---|
Domain(研究对象的集合) | 定义集合 | 变量集合 | 表达式集合 |
Direction(数据状态的依赖关系) | Forwards | Backwards | Forwards |
May/Must(应用场景) | May | May | Must |
Boundary(Direction&May/Must) | $\mathrm{OUT}[entry]=\emptyset$ | $\mathrm{IN}[exit]=\emptyset$ | $\mathrm{OUT}[entry]=\emptyset$ |
Initialization(Direction&May/Must) | $\mathrm{B}[entry]=\emptyset$ | $\mathrm{In}[B]=\emptyset$ | $\mathrm{OUT}[B]=\emptyset$ |
Transfer function | $\mathrm{OUT}=gen \cup (\mathrm{IN}-kill)$ | - | - |
Meet(May/Must) | $\cup$ | $\cup$ | $\cap$ |
对于数据流分析解释三的理解
数据流的transfer和control-flow handing定义了一组方程:
- $\mathrm{D}_{\mathrm{v}_{1}}=\mathrm{F}_{\mathrm{v}_{1}}\left(\mathrm{D}_{\mathrm{v}_{1}}, \mathrm{D}_{\mathrm{v}_{2}}, \ldots, \mathrm{D}_{\mathrm{v}_{\mathrm{n}}}\right)$
- $\mathrm{D}_{\mathrm{v}_{2}}=\mathrm{F}_{\mathrm{v}_{2}}\left(\mathrm{D}_{\mathrm{v}_{1}}, \mathrm{D}_{\mathrm{v}_{2}}, \ldots, \mathrm{D}_{\mathrm{v}_{\mathrm{n}}}\right)$
- …
- $D_{v_{n}}=F_{v_{n}}\left(D_{v_{1}}, D_{v_{2}}, \ldots, D_{v_{n}}\right)$
其中:
- $F_{v_{1}}\left(\mathrm{D}_{\mathrm{v}_{1}}, \mathrm{D}_{\mathrm{v}_{2}}, \ldots, \mathrm{D}_{\mathrm{v}_{\mathrm{n}}}\right)=f_{v_{1}}(I)$
- $F_{v_{i}}\left(\mathrm{D}_{\mathrm{v}_{1}}, \mathrm{D}_{\mathrm{v}_{2}}, \ldots, \mathrm{D}_{\mathrm{v}_{\mathrm{n}}}\right)=f_{v_{i}}\left(\sqcap_{j \in \operatorname{pred}(i)} D_{v_{j}}\right)$
数据流分析即使求该方程的最大解(Unification算法),对于单调函数和有限格,Unification算法就是上述的不动点算法。