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_(注意_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 op y_ is available at program point _p_ if (1) all paths from the entry to _p_ must passthrough the evaluation of _x op y_, and (2) after the last evaluation of _x op y_, there is no redefinition of _x or y_.

表达式_x op y_为availbable 当且仅当 (1)所有路径都经过_x op y_ (2)最后一个计算 _x 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]=\empty$ $\mathrm{IN}[exit]=\empty$ $\mathrm{OUT}[entry]=\empty$
Initialization(Direction&May/Must) $\mathrm{B}[entry]=\empty$ $\mathrm{In}[B]=\empty$ $\mathrm{OUT}[B]=\empty$
Transfer function $\mathrm{OUT}=gen \cup (\mathrm{IN}-kill)$ - -
Meet(May/Must) $\cup$ $\cup$ $\cap$