0%

静态程序分析课程笔记(数据流分析-应用)

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存在三种情况:

image-20200802175052488

后两种情况存在交汇(meet)操作(第二种后向分析存在)

image-20200802175345773

对于第三种情况下的前向分析,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$的路径上是否有新的定义(可以用于空指针问题)

算法设计

  1. Data Flow Values
    用bit vecotr表示集合,集合中元素表示每一到达该点的语句
    e.g. D1, D2, … , Dn=01…0 (表示D2定义在当且位置有新定义)

  2. 定义Transfer Function和Control-flow Handing

    Transfer Function:
    对于一个定义语句D: v = x op y,kill(在集合)与v相关的其他语句,并在集合中加入D,即:

    Control-flow Handing:
    当多个代码块汇聚时,合并所有的定义(may)

  3. 应用经典的数据流分析算法框架(Iterative algorithm)
    Iterative algorithm

    遍历结果

    image-20200802193730918

为什么能到不动点(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)

算法设计

  1. Data Flow Values,依然用bit vector,注意这次记录变量
    如:V1,V2,…,Vn=01…0 (V2在p上的定义被使用i.e.,不能清空V2寄存器)

  2. 定义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,依旧是∪:

  3. 不动点算法
    image-20200802203143027

    分析结果

    image-20200802202534370

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,则优化最后一次的计算,例如:
image-20200802204136008

c可以被优化,例如,将a,b,c全转化为y,最后一步则不用计算(不论走什么分支,最后的t都不用计算)

算法设计

  1. Data Flow Values
    available的表达式集合,可用bitVector表示,如:

    E1,E2,…,En=01…0(E2为available)

  2. 定义Transfer Function和Control-flow Handing

    Transfer Function:

    这里的$kill_{B}$指删除表达式,这些表达式的变量在当前块B中被重新定义。

    Control-flow Handing:

    must analysis,由“∪”变成了“∩”

  3. 算法,注意每个bb的初始化,变成了“All”,即初始状态所有表达式都是available的(反向思维,如果初始化为0,那么$\cap$后恒为0,计算无效)
    image-20200802205253641

综合比较

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算法就是上述的不动点算法。