【静态分析】数据流分析-Part I

前言

这阵子在学习静态分析，找了许多学习材料，但讲的都晦涩难懂，无意间在神奇的bilibili 刷到了一位南京大学Yue Li老师的静态分析课程1，不得不说，老师讲的太棒了，让我对静态分析的知识有了基本的了解，算是做了一个简单的入门。

本文，是静态分析中数据流分析的Part I ，主要讲解Reaching Definition Analysis ，主要内容包括：

  • 前置知识

  • Reaching Definition Analysis的定义和理解

  • Reaching Definition Analysis算法与详解
  • 举个栗子
  • 总结

读完本文会对数据流分析Reaching Definition Analysis 内容有一个初步的了解，解答包括是什么，怎么做，效果体现三方面的问题，废话不多说，Let's start!

前置知识

在进行Reaching Definition Analysis 之前，先需要对一些基础术语和定义有基本的了解：

  • CFG, Control Flow Graph (控制流图)：这个概念在静态分析中经常被提及，也十分地重要，它定义了程序执行的过程和走向，如果把数据流比作水流，控制流图就是一系列组合的管道，它控制了水能够经过的地方，这个内容我会单独在后面单独写一篇文章讲解，这里先按下不表。
  • BB, Basic Block(基本程序块)：是CFG 的重要组成部分，可以看作各个结点，由一条或多条基本指令组成，这个内容同样在CFG的文章中讲解
  • Input and Output States(输入输出状态)：我们知道，指令s执行过后，程序的状态就发生了改变（例如某个变量被赋值），为了描述改变前后的状态，我们用符号IN[s],OUT[s]表示，前者也表示指令的状态输入，后者也表示指令的状态输出，如下图所示：

Input Output States

注意到图中还有一个program point ，这和IN[s],OUT[s]是相关联的，表示为程序执行到的点，很显然假设s2 是s1的后继，必然有IN[s2]=OUT[s1]，图中还列举了另外两种分散和聚合的情况，分散的情况中IN[s2]=IN[s3]=OUT[s1]，聚合的情况中，IN[s2]就和OUT[s1],OUT[s3]两者有关了，但具体是什么关系要根据具体的分析情况，这里用一个^(meet)符号表示，它可以是∩(交集)，也可以是∪（并集），甚至是其他的一些联合操作。

  • 基于BB的States： 在静态分析的过程中，我们都是以BB为单位进行分析的，因此我们需要对IN[B],OUT[B]做出定义，回顾BB是由多条指令s组成的，因此我们很容易有如下的定义：

    image-20210325211432294

这个图对IN[B]、OUT[B]诠释地很全面了，这里简单说明一下，IN[s[i+1]]=OUT[s[i]]（因为它们是顺序执行关系）,IN[B]=IN[s1]（整个BB的状态输入来源于第一条指令的输入）,OUT[B]=OUT[s[n]]（整个BB的状态输出最终通过s[n]体现）

  • BBs 状态转换：在我们定义了IN[B],OUT[B]之后，对于不同控制流中块到块之间，IN[B],OUT[B]会如何变化？这里又有两个概念：Transfer Function, Control Flow（转移函数，控制流），Transfer Function是针对块而言的，对于BB 中指令的操作，我们可以封装理解为一个函数式（该函数有输入IN[B]，输出OUT[B]），那么从IN[B]转移到OUT[B]，我们就可以定义为

image-20210325213322647

其中$f_B$表示经过BB的Transfer Function，后面是函数嵌套，而从OUT[P]怎么转换到IN[B]呢？实际上就是和我们之间定义的聚合情况中指令类似，只要将每个BB的OUT 做^(meet)操作即可（注意meet不一定是交集），而这里为什么还有P a predecessor of B (P是B的一个前驱)？这是因为分析的过程包含forward和backward两种方式，在本文中采用了forward 的分析方法，在后面会讲到backward的方式。

最终有如下图示：

image-20210325214236514

到此，我们把必要的前置知识说明完毕，这部分如果不理解建议去看一下b站的视频，老师讲的十分详细。

Reaching Definition Analysis

光从名字就知道这是一个针对定义的分析，但Reaching又是什么意思呢？这里又要设计到一些定义：

  • definition ：说直白点就是变量的赋值语句，例如v=3,v=k
  • reaching ：先官方解释一下，变量v 从program point p reachingprogram point q的前提是存在一条从p到q的路径且在该路径中v没有被重新定义，图示如下：

image-20210326190555912

换成人话就是两程序执行点之间没有新的关于v的赋值语句，这个也就表示了最开始v的定义到了q依然是有效的，例如:

v = 3
v = 5  # 本语句重新定义了v，使得v=3失效
k = v

下面就到了另一个问题，为什么要做reaching definition analysis，一个直观的作用就是用于检测undefined variables，在程序中所有出现的变量都有一个初始状态，即undefined，假设在某一条路径上变量v被使用了k = v，但此时v的状态依然是undefined,就发生了使用未定义变量的错误。

知道了reaching definition anlysis的定义和目的后，就要设计分析的过程了，这个设计过程是静态分析过程中非常经典的，后面另外的两种分析方式也采用一样的设计模式，具体来说包括三步：

  1. Abstraction ：对要分析的对象进行抽象，这有利于我们后面的表示
  2. Transfer Function：定义经过程序执行过后的状态变化
  3. Control Flow: 定义不同程序块汇聚时候的策略，为什么单独针对汇聚的情况？是因为在汇聚的时候输出的结果有不同的组合方式进入输入，这个要根据实际分析而定

Abstraction

在本文的分析中，我们关注的对象是definition，更一般地，是definition是否可reach，考虑到程序中可能有非常多的definition（因为有很多变量的赋值语句），我们采用一种bit vector的方式进行定义，假设程序有D1,D2,...,Dn定义，用1表示reach，0表示不可reach，那么容易得到一组向量00000..00(初始化的时候都不可reach)

Transfer Function

转移函数取决于程序中执行的指令，在设计Transfer Function的时候就要结合定义思考：pq之间不能有新的对于v的定义

  1. pq之间不存在对于v的赋值语句，此时输入与输出一致没变化
  2. pq之间存在v的赋值语句(v=3)，这时候有两个操作：
    • 因为有新的赋值语句，所以该处定义被激活
    • 因为该处定义被激活，导致其他所有与该定义的v相关的语句失效

上面的说法可能比较抽象，看个图就明白了：

image-20210326194634046

上图中针对不同的BB，定义了两种集合,$gen_B,kill_B$，前者表示，经过该BB，对应被激活的definition集合，后者表示，经过该BB，对应失效的definition集合，例如在B1执行后，涉及的被定义变量有i,j,a，那么这三句定义生效，所有其他对i,j,a进行定义的definition失效，即$d_4,d_5,d_6,d_7$

考虑到还有输入的状态（因为输入包含之前被激活的情况），所以得到如下的Transfer Function：

image-20210326195147092

从输入中去除那些失效的，加上新被激活的就得到了输出

Control Flow

设想一下，假设如图下的情况，在P1中包含对v的定义，P2中没有，那么B中v的定义是否可达？

image-20210326195400882

反过来想，如果我们认为在B中v的定义不可达（也就是没有定义），当程序执行的路径经过P1时，v出现了定义，而到下一个BB，v又没有定义了，这显然是不成立的。

换言之，只要B的前驱程序块中有一个块对v的定义是可达的，那么在B中就是可达的。

Reaching Definition Analysis 算法设计

做好了一系列前置准备工作后，我们就需要定义分析的流程，这里先不着急直接看算法，先思考几个点：

  1. 最开始的时候所有变量都没有定义
  2. 当程序块执行过后，某些变量会被定义，即某些definition会被激活，同时某些也会失效
  3. 在汇聚（merge）的时候后继的输入与前驱的输出有关，而某些情况下，后面的BB由于状态更新后产生了变化，同时该块又是前面已执行块的前驱（常见于goto），这时候我们就又要对前面的块结果进行更新，因此算法必然是多次循环遍历程序块的
  4. 循环遍历的终点应该在于所有块的状态都不发生变化了，因此我们需要监测块的前后状态情况

基于以上思考，得到如下算法：

image-20210326202252744

  • 输入：CFG、gen和kill的集合，因为一旦程序块确定了，那么每个块的gen和kill是个定值
  • 输出：IN[B],OUT[B]，这里输出的状态实际上就是前面对definition的抽象表示，例如有D1,D2,D3，那么状态表示就是000，当D1被激活，则状态转变为100
  • 方法：
    1. 第一步初始化所有$OUT[entry]=\phi$ ，即代表一开始所有定义都是undefined
    2. 第二步针对所有BB，讲输出设为$\phi$ ，这也很显然，唯一要说明的是两者都是要置空，为什么要分开来，这个其实是为了划分边界，因为有的算法与之类似，但边界的初始化和其他基本块不同，这里划分开，就让两种算法在结构上保持了一致
    3. 第三步是循环，终止条件是所有输出块没有发生变化，同时对所有的BB，按照之前定义的Transfer Function, Control Flow实现更新

有一点值得思考的在于算法能否终止，其中最核心的地方就是IN[B],OUT[B]，IN[B]取决于所有的OUT[P]，而OUT[B]又取决于IN[B](gen,kill是固定值)，也就是说一旦IN,OUT有一个不变，另一个就不会再变化，所以我们只需要看一个块就好，对于一个BB,由于kill是固定的，相当于经过这个块被kill的状态恒为0，而kill是唯一使得1->0的变化，所以说一个块的状态只能从0->1,1->1，经过若干次变化后，必然会停止（最坏情况都是1），也即BB最终趋于不变，这时候循环就结束了。

举个栗子

说了那么多，不如实际跟着一个例子走一遍，由于视频中采用动图，如果将每一张一一展开叙述，实在太费笔墨，这里直接以起始和结束两图为例：

  • 起始：假设某CFG如下：

image-20210326204625309

左边为框架对应的程序源码（缩略版），其中不同颜色标注的定义代表了不同变量

  • 结束：

    image-20210326204800573

B1 B2 B3 B4 B5
gen D1,D2 D3,D4 D7 D5,D6 D8
kill D5,D7,D4 D2 D1,D5 D1,D7,D8 D6

简单对图中运行过程进行说明：左上角是状态的定义（一共有8个definition）和所用的迭代次数，不同颜色代表了不同的迭代轮次，例如黑色就表示初始化，所有状态都是0000 0000，然后是红色（为第一次迭代后状态的变化结果），这部分只要结合算法一步步过下来即可。建议自己在纸上运算一遍，再和结果对照。上面我还给出了每个BB的gen和kill，通过查表可以加速计算的过程。

总结

本文着重讲解了数据流分析中的Reaching Definition Analysis，包括其定义与理解，分析过程（算法），实际例子，对一些基础的概念也进行了详细的阐述，但还是有许多没能讲解透彻的地方，如果真的对这块内容有兴趣的话，建议去B站看一遍老师的视频，会有不同的感悟和理解。这堂课带给我最大的启发，主要有几点：

  1. 专业性的知识：数据流分析要分析什么，为什么分析，如何分析
  2. 如何将一个分析问题具象到对定义和分析过程的设计：像本文就是为了知道在程序执行过后，每个定义语句的有效性，以便找出undefined variables,要达到这个目的，要知道程序块执行后对定义产生了什么影响，以及数据流汇聚时候的处理
  3. 设计分析过程（算法）的巧妙之处，包括特殊的边界处理和对算法终止的判断

其他更多的内容待以后有新的感悟之后再添加进来。

参考

1 : 南京大学《软件分析》课程03（Data Flow Analysis I）_哔哩哔哩 (゜-゜)つロ 干杯~-bilibili