DataFlow Analysis Foundations

1. Another View to Iterative Algorithms

以Forward Analysis为例，对于给定的有 个节点的CFG，迭代算法在每一轮的迭代中依次更新所有节点的OUT[B]。

设每个节点的OUT[B]的值域为 ，则整个CFG的状态可以表示为 。每轮迭代进行的操作可以视为将当前CFG的OUT状态转换为另一个状态，也即对状态使用转移函数函数 进行变换。

当迭代算法收敛时，有 ，称 为 不动点(Fix Point) 。

2. Partial Order

偏序集(poset)可以表示为二元组 ，其中 是定义在 上的二元偏序关系，且 满足以下性质：

• 。即 自反性Reflexivity 。

• ，若有 且 ，则必有 。即 反对称性Antisymmetry 。

• ，若有 且 ，则必有 。即 传递性Transitivity 。

3. Upper and Lower Bounds

给定偏序集 ，若有 ，且 使得 ，则称 为 的 上界 。

下界 的定义类似。

最小上界 Least Upper Bound (lup, join) ：若存在 的某一个上界 ，满足对于 的任意一个上界 ，均有 ，则称 为 的最小上界，记作 。

最大下界 Greatest Lower Bound (glb, meet) 的定义类似，记作 。

若集合 中只有两个元素 ，则可以将 记为 。 glb类似。

• 不是所有偏序集都有lub和glb。

• 若偏序集有lub或glb，则该lub或glb一定唯一。（用lub/glb的定义和偏序集的自反性证明）

4. Lattice

给定偏序集 ，若 中任意一对元素 ，集合 的lub和glb都存在，则称该偏序集为 格 Lattice 。

若只有lub或只有glb都存在，则称为 半格 Semi Lattice 。

给定格 ，若对于 的任意子集 ， 的lub和glb均存在，则称该格为 完全格 Complete Lattice 。

• 若格有限，则其必定为完全格。

• 完全格不一定有限。 例如： 为 之间的实数， 为实数的小于等于，则该格的任意子集均有上下确界，为完全格，但其是无穷格。

Caution 自然数的集合和自然数的小于等于构成的偏序集并不是完全格，因为自然数没有上确界。

将完全格 中的最大元素即 记作 ，最小元素即 记作 。

若有 个格 ， ，…， ，若任意 均有lub和glb，则可以按照如下方法构造一个新的格 ，称为 Product Lattice ：

• 等价于 对于所有的 均成立。

这样得到的 Product Lattice 满足如下性质：

• glb类似

• 若 均为完全格，则 也为完全格。

5. Data Flow Analysis Framework via Lattice

一个集合的幂集以及定义在集合上的包含于关系，构成一个完全格。

数据流分析三元组 包括：

• 分析方向 ，即 Forwards or Backwards

• 格 ，包括每个节点的值域 和合并运算 或

• 转移函数族（转移函数对每个节点不同）

数据流分析可以视为迭代地对格上的值应用转移函数和meet/join操作。

6. Monotonicity and Fixed-Point Theorem

单调性 ：定义在格上的函数 ，若 均有 ，则称 是单调的 (Monotonic) 。

不动点定理 ：给定完全格 ，若存在函数 是单调的，且 是有限的，则：

• 最小不动点 Least Fixed Point 可以由 迭代地计算 直到达到第一个不动点 而得到。

• 最大不动点 Greatest Fixed Point 可以由 迭代地计算 直到达到第一个不动点 而得到。

证明：以最小不动点为例。需要证明不动点的存在性（即按照这样的方法总能找到一个不动点）和按照这样的计算方式得到的不动点是最小不动点。

先证存在性：由 的定义知， ，由 的单调性知 ， 。即 。由于 是有限的完全格，故 有上界，最终会等于某个定值，即找到了不动点 。

再证最小性：假设除了上述方法找到的不定点外还有另一不动点 使得 。下面使用数学归纳法来证明 是最小不动点：

1. 由 的单调性， ；

2. 假设 成立，则由 的单调性可得 也成立；

3. 已知 ，则有 ，即 成立。

综上，上述算法总能找到不动点且找到的不动点为最小不动点。

最大不动点的证明同理。

07 Relate Iterative Algorithm to Fixed Point Theorem

迭代算法可以看成在CFG的所有节点组成的 Product Lattice 上不断应用函数 直至达到不动点的过程。如果该 Product Lattice 为有限的完全格，且函数 是单调的，我们就可以使用不动点定理来解释迭代算法的正确性。

Product Lattice 的有限性

由于组成 Product Lattice 的每个 Lattice 都是有限的完全格，所以该 Product Lattice 也是有限的完全格

函数 的单调性

函数 可以分为两大部分：

1. Transfer Funtion ，对于gen/kill问题而言，该部分是单调的（never shrinks）。

2. Control Flow Merging 。当有多个分支合并时，可以看作每个分支和结果分支一一合并的结果（参考lab1的 meetInto ）。

由于 gen/kill 的 Transfer Function 的单调性已经证明过，这里只证明 Control Flow Merging 的单调性：

要证明 是单调的，只需要证明 ，若有 ，则必有 。

由lub的定义，有 ， ，故有 ，即 是 和 的一个上界，而 是 和 的最小上界，所以 。

要证明 是单调的，只需要证明 ，若有 ，则必有 。

由glb的定义，有 ， ，故有 ，即 是 和 的一个下界，而 是 和 的最大下界，所以 。

证明这两部分的单调性后，还需要说明 的单调性（这里李樾老师好像没有细说？直接就得到了 单调的结论），这里给出我自己的理解： Control Flow Merging 函数的输出是 Transfer Function 的输入， Transfer Function 的输出又是 Control Flow Merging 的输入，由于这两部分都是单调的，所以两个部分的复合也是单调的。

When Will the Algorithm Reach the Fixed Point

假设在每次迭代中，只有一个节点的一个0变成了1，在最坏情况下，最终状态为所有节点的分量均为1，这样一共需要 次迭代，其中 为 CFG 的节点数量， 为格的高度。

08 May and Must Analysis, from a Lattice View

这部分主要解释为什么 May Analysis 的初始化为 ，最终期望得到最小不动点；而 Must Analysis 的初始化为 ，最终期望得到最大不动点。

May Analysis

上图的右侧是 May Analysis 的示意图。我们的分析总是从 unsafe 逐步走到 safe 的。以 Reaching Definitions 为例，这个分析是用来检测是否有变量未被初始化的，其具体方法是在程序的开头为所有变量都提供一个 undefined 的定义，如果这个最早的定义 Reach 到了程序的某一点，那么这个变量在这一点就是没有被初始化的。因此，该分析的 unsafe 状态就是所有的定义都没有 reach ，也即所有的变量都初始化了，这显然是错误的结论。随着函数 的应用，我们的分析结果会在格上不断往上走，也就是分析出了越来越多的定义 reach 了，即越来越多的变量没有被初始化。以 truth 为分界线， truth 以下的点是不安全的，因为它漏报了未初始化的变量， truth 以上的点是安全的，但是越靠上的点越没用，因为报出了过多的未初始化变量（最坏情况下报出所有变量均未初始化，这显然是安全的，但是没有任何用处）。我们期望找到的点就是在 truth 以上的最低的不动点，因此要找的就是最小不动点，而这个不动点在 truth 以上是由 的设计决定的。因此在设计 时，需要保证能得到正确的分析结论，即最小不动点在 truth 之上。

Must Analysis

上图的左侧时 Must Analysis 的示意图。以 Available Expressions 为例，不安全的状态是所有的表达式都 available ，随着分析的进行，状态不断往下走，越来越多的表达式变成 unavailable ，变得越来越安全。以 truth 为分界点， truth 之上的点不安全， truth 之下的点安全，但是越靠下越没用（最坏情况下报出所有表达式都 unavailable ，这显然是安全的，但是没有任何用处）。因此我们期望找到的不动点就是 truth 之下的最大不动点。

另外，在进行 meet/join 操作时，我们取的都是 glb/lub ，也就是在格上移动最短的距离，这个角度也可以解释最小/最大不动点的由来。

09 MOP and Distributivity

MOP : Meet-Over-all-Paths ，是数据流分析的另一种方法，它将 Transfer Funtion 的作用对象由节点转变成了路径。当计算一个节点的 OUT 时，先计算从 Entry 到该节点的所有路径的 OUT ，再将这些路径的 OUT 合并。与迭代算法的区别是，迭代算法先由前驱节点的 OUT 合并成该节点的 IN ，再应用转移函数； MOP 则先对各路径应用转移函数得到不同路径的 OUT ，再将不同的 OUT 合并成该节点的 OUT 。

可以这样总结：

$$Iterative=F(x⊔ y)$$ $$MOP=F(x)⊔ F(y)$$

这两种算法中， MOP 更为精确，证明如下：

由于 ， ，所以 ， ，即 是 和 的一个上界，而 是 和 的最小上界，所以 。

当且仅当 时，这两种算法一样精确，满足这样性质的函数 称其具有 分配性 Distributivity 。

Bit-Vector 即 gen/kill 问题都是 distributive 的，但也有一些分析是 undistributive 的，如 Constant Propagation 。

10 Constant Propagation

分析的目标是，判断某个变量在某一点的值是否是一个常量，并给出该值。

CFG 中的每个节点的 OUT 由若干个二元组组成，每个二元组 中 是变量名， 是该变量的值，其构成的格如下图所示：

当 不是一个常量时， ；当 是常量是， 为其具体的数值；其他情况下 。

下面来分析前文提到的数据流分析三元组 。显然该分析应该是 Forwards 的，因为一个变量是否是常量是由之前发生的事情决定的； Lattice 的 Domain 就是上图所示的 Lattice ，我们还需要定义一个 meet/join operator ；此外，还需要设计一个转移函数。

考虑该分析的实际用途，用来在编译期间将变量优化为常量，因此不能出现非常量的变量被分析为常量的情况，所以是一个 Must Analysis ，为其设计 meet operator 如下：

• ， 其中 为任意值

• ， 其中 为任意值

• ，其中 为常量

• ， 其中 为常量且

下面对于 statement 定义 Transfer Function ：

• 若 为 “x=c;” ，其中 为常量 ，则

• 若 为 “x=y;” ，其中 为变量，则 。

• 若 为 “x=y op z” ，则 ，其中若 和 均为常量，则 ；若 和 中有一个是 NAC ，则 ；其他情况为 UNDEF 。

这里的 kill/gen 都是固定的，因此转移函数也是单调的， meet operator 显然也是单调的，符合不动点定理。

该分析就不满足 distributivity ，如下图所示：

使用迭代算法，合并 X Y 时，得到 a 和 b 均不是常量，因此 c 也不是常量；但是使用 MOP 时，两条路径得到的 c 均为 10 ，故可以得到 c 是常量的结论。

11 Worklist Algorithm

在 Iterative Algorithm 中，若一个节点的 IN 不发生变化，则它的 OUT 必然不会变化，因此我们每次迭代并不需要遍历所有的节点，而只需要考虑 IN 发生变化的节点。这类似于使用队列优化的 Bellman-Ford 算法，在求解最短路时只考虑被更新了的节点。

完结撒花🎊