前言

上一节中，李樾老师讲了IR相关的内容。从本节开始的连续四节课程都是关于数据流分析（Data Flow Analysis，简称DFA）的，其中第三、四节是DFA的应用部分，第五、六节则是理论基础部分。本节课首先介绍了数据流分析，然后讲解了定义可达性分析（Reaching Definitions Analysis）这一部分。

数据流分析简介

李樾老师对于数据流分析的介绍十分易懂。Data flow analysis研究的问题就是：How data flows on CFG?

进一步扩展后是：How application-specific data flows the nodes (BBs/statements) and edges (control flows) of CFG (a program)?

第一节课曾提到，静态分析可以从两个方面把握：首先是对data做abstraction（如第一节课的“$+ - \Omicron \top \bot$”），然后做over-approximation。事实上，对于绝大多数静态分析场景来说，我们要做的都是over-approximation，也可以称为may analysis，即输出结果包含的信息可能为真。然而，还有一些场景是需要under-approximation，也可以称为must analysis，即输出结果必须包含的信息必须为真。无论如何，over-approximation和under-approximation的目的都是在各自的场景中实现safety of analysis，使结果符合该场景的需求。

对于CFG中的nodes，我们需要用transfer function来进行处理；对于edges，我们需要处理控制流，例如需要在merge处对上游分支做union。

不同的数据流分析应用（application）有着不同的数据抽象（data abstraction）和不同的流安全近似策略（flow safe-approximation strategies），即不同的transfer functions和control-flow handlings。

数据流分析基础

我们首先需要了解一下数据流分析中的输入状态和输出状态：

  • 每个IR语句的执行将一个输入状态（input state）转换成了一个新的输出状态（output state）。
  • 某个IR语句的输入（输出）状态与该语句之前（之后）的程序点（program point）关联。

下图展示了三种不同的控制流情况：

IN[s1]   │              ┌──────────┐       ┌──────────┐      ┌──────────┐
         │              │          │       │          │      │          │
    ┌────┴─────┐        │    s1    │       │    s1    │      │    s3    │
    │          │        │          │       │          │      │          │
    │    s1    │        └─────┬────┘       └────┬─────┘      └─────┬────┘
    │          │              │                 │                  │
    └────┬─────┘          ┌───┴──┐              └────────┬─────────┘
OUT[s1]  │                │      │                       │
         ▼                ▼      ▼                       ▼
    ┌──────────┐ ┌──────────┐   ┌──────────┐        ┌──────────┐
    │          │ │          │   │          │        │          │
    │    s2    │ │    s2    │   │    s3    │        │    s2    │
    │          │ │          │   │          │        │          │
    └──────────┘ └──────────┘   └──────────┘        └──────────┘

对于语句s1、s2和s3来说：

  • 左侧控制流，IN[s2] = OUT[s1]
  • 中间控制流，IN[s2] = IN[s3] = OUT[s1]
  • 右侧控制流，IN[s2] = OUT[s1] ^ OUT[s3]

^是meet operator，根据实际控制流走向取值。

在数据流分析应用（application）中，我们通常将每个program point与一个数据流值（data-flow values）关联，此data-flow value代表了在该点上可以观察到的所有可能的程序状态的抽象集合。

对于一个application来说，所有可能的data-flow values构成的集合称为该application的域（domain）。

在以上这些内容的基础上，我们可以说，数据流分析的目的就是要为一个“以safe-approximation为导向”的约束（constraints）集合，为所有语句（statements）s，在IN[s]和OUT[s]上，找到一个解（solution）。

约束体现在哪里呢？体现在两方面：

  1. 基于语句语义的约束（表示为transfer functions）。
  2. 基于控制流的约束。

对于transfer functions的约束来说，有两类分析：

  1. 前向分析（forward analysis），根据输入求输出：$OUT[s] = f_{s}(IN[s])$
  2. 后向分析（backward analysis），根据输出求输入：$IN[s] = f_{s}(OUT[s])$

在我看来，这两种分析非常像数学上的“互为反函数”的定义。

对于控制流的约束来说，也有两类情况：

  1. BB内控制流：$IN[s_{i+1}] = OUT[s_{i}],\ for\ all\ i = 1, 2, …, n-1$
  2. BB间控制流：$IN[B] = IN[s_{1}],\ OUT[B] = OUT[s_{n}]$

另外，从前向分析的角度看，BB间控制流有以下特性：

  • $OUT[B] = f_{B}(IN[B]), f_{B} = f_{s_{n}} \circ\ …\ \circ f_{s_{2}} \circ f_{s_{1}}$
  • $IN[B] = \bigwedge_{P\ a\ predecessor\ of\ B} OUT[P]$

$\bigwedge\ $符号用于表示B的所有前驱对B的贡献的综合结果。

从后向分析的角度看，BB间控制流有以下特性：

  • $IN[B] = f_{B}(OUT[B]), f_{B} = f_{s_{1}} \circ\ …\ \circ f_{s_{n-1}} \circ f_{s_{n}}$
  • $OUT[B] = \bigwedge_{S\ a\ successor\ of\ B} IN[S]$

Reaching Definitions Analysis

接下来就是可达性分析了。在具体讲解之前，我们需要排除一下本节不会考虑到的一些问题：

  • 函数调用，涉及到跨过程的CFG。
  • 别名（Aliases），目前我们处理的都是没有别名的变量。

OK，首先看一下“定义可达性”这个概念：

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.

对变量v的定义，指的是一个对v赋值的语句。因此，我们可以借助变量v来进一步阐释上述定义：program point p处对变量v的定义在q可达，指的是从p到q有一条路径，而且这条路径上没有其他对v的定义语句。

定义可达性分析可以用来检测源代码中的未定义变量。思路是，在CFG入口处为源代码中的所有变量引入一个dummy definition，如果最终某个变量v的dummy definition能够达到该变量被使用的program point，那么变量v就是一个未定义的变量。

前面我们提到，不同的数据流分析应用有着不同的data abstraction和不同的flow safe-approximation strategies，即不同的transfer functions和control-flow handlings。这句话很重要。现在，我们来考虑定义可达性分析的data abstraction和safe-approximation。

对于定义可达性分析的来说，数据流中的值是一个程序中的所有变量的定义，它们可以用bit vector来表示。例如，如果$D_{1}$到$D_{100}$表示程序中所有的100个变量定义，那么我们可以用一个长度为100的bit vector来表示它。在program point p处，$D_{i}$被置1，当且仅当$D_{i}$处的变量定义能够到达p。

接下来考虑transfer functions和control-flow。我们用下面这个抽象语句来明确一下定义$D$： $$ D:\ v\ =\ x\ op\ y $$ 上述语句将为变量v“生成”一个定义$D$，并kill掉程序中所有其他地方的变量v的定义。注意，是所有其他地方，不仅仅是之前的control flow，因为程序control flow可能存在环，我们不能确定运行时真正的执行先后顺序。即使kill掉了无环执行流的下游的定义也没有关系，后面再重新定义即可。

基于此，我们可以得出BB级的transfer function： $$ OUT[B] = gen_{B} \cup (IN[B] - kill_{B}) $$ 下图展示了一个CFG中BBs的$gen$和$kill$：

Xnip2023-03-06_10-38-47

我们同样可以得出control flow handling： $$ IN[B] = \bigcup_{P\ a\ predecessor\ of\ B}OUT[P] $$ 接下来就是定义可达性分析的算法了。算法初看起来比较复杂，但是后面李樾老师用一个例子把它讲得非常清楚，十分精彩。首先来看一下算法：

image-20230306112148922

上述算法中有两个值得讨论的点：

  1. 为什么 $OUT[entry] = \empty$ 被单独拎出来了，没有和下面的for循环合并？
  2. 为什么我们能确定while循环一定会终止？

第一个问题比较简单，因为这么写在修改时更方便。在一些其他的分析中，可能entry之外的其他BB的初始化值并非空集，此时只需要修改for循环内部的赋值语句即可。

第二个问题稍微复杂一些，借助后面的例子能够更好地理解。这里我们先回答一下：一个程序中的definitions是有限的，即bit vector的长度是有限的，每个BB的$OUT[B]$实际上只与$IN[B]$有关（因为$gen_{B}$和$kill_{B}$总是保持不变），且按照算法来看，$OUT[B]$置1数一定不会比$IN[B]$小。而$IN[B]$又是基于前驱$OUT[P]$产生的，因此每个循环后的$IN[B]$一定不会减小。该算法是单调递增的，并且有一个上界（bit vector全部置1），因此最终一定会停止。

OK，接下来看一个例子：

Xnip2023-03-06_12-53-30

除了初始化过程外，这个分析进行了三轮。第三轮中，bit vector没有发生变化，循环终止。最终得到的不同program point处的bit vector就是定义可达性的分析结果。

关于这个算法在该例子上执行的具体过程，推荐去看李樾老师的授课视频或课件，非常详细清楚。

事实上，最后求出的解是数学上的“不动点”。

总结与思考

本节课，李樾老师介绍了数据流分析的基础知识，然后介绍了第一个数据流分析的应用——定义可达性分析。

有趣有料，继续前行吧。