Data Flow Analysis Foundations
DataFlow Analysis Foundations
1. Another View to Iterative Algorithms
以Forward Analysis为例,对于给定的有
设每个节点的OUT[B]的值域为
当迭代算法收敛时,有
2. Partial Order
偏序集(poset)可以表示为二元组
。即 自反性Reflexivity 。 ,若有 且 ,则必有 。即 反对称性Antisymmetry 。 ,若有 且 ,则必有 。即 传递性Transitivity 。
3. Upper and Lower Bounds
给定偏序集
下界 的定义类似。
最小上界 Least Upper Bound (lup, join) :若存在
最大下界 Greatest Lower Bound (glb, meet) 的定义类似,记作
若集合
不是所有偏序集都有lub和glb。
若偏序集有lub或glb,则该lub或glb一定唯一。(用lub/glb的定义和偏序集的自反性证明)
4. Lattice
给定偏序集
若只有lub或只有glb都存在,则称为 半格 Semi Lattice 。
给定格
若格有限,则其必定为完全格。
完全格不一定有限。 例如:
为 之间的实数, 为实数的小于等于,则该格的任意子集均有上下确界,为完全格,但其是无穷格。
Caution 自然数的集合和自然数的小于等于构成的偏序集并不是完全格,因为自然数没有上确界。
将完全格
若有
等价于 对于所有的 均成立。
这样得到的 Product Lattice 满足如下性质:
glb类似
若
均为完全格,则 也为完全格。
5. Data Flow Analysis Framework via Lattice
一个集合的幂集以及定义在集合上的包含于关系,构成一个完全格。
数据流分析三元组
分析方向
,即 Forwards or Backwards 格
,包括每个节点的值域 和合并运算 或 转移函数族(转移函数对每个节点不同)
数据流分析可以视为迭代地对格上的值应用转移函数和meet/join操作。
6. Monotonicity and Fixed-Point Theorem
单调性 :定义在格上的函数
不动点定理 :给定完全格
最小不动点 Least Fixed Point 可以由 迭代地计算
直到达到第一个不动点 而得到。 最大不动点 Greatest Fixed Point 可以由 迭代地计算
直到达到第一个不动点 而得到。
证明:以最小不动点为例。需要证明不动点的存在性(即按照这样的方法总能找到一个不动点)和按照这样的计算方式得到的不动点是最小不动点。
先证存在性:由
的定义知, ,由 的单调性知 , 。即 。由于 是有限的完全格,故 有上界,最终会等于某个定值,即找到了不动点 。 再证最小性:假设除了上述方法找到的不定点外还有另一不动点
使得 。下面使用数学归纳法来证明 是最小不动点:
由
的单调性, ; 假设
成立,则由 的单调性可得 也成立; 已知
,则有 ,即 成立。 综上,上述算法总能找到不动点且找到的不动点为最小不动点。
最大不动点的证明同理。
07 Relate Iterative Algorithm to Fixed Point Theorem
迭代算法可以看成在CFG的所有节点组成的 Product Lattice 上不断应用函数
Product Lattice 的有限性
由于组成 Product Lattice 的每个 Lattice 都是有限的完全格,所以该 Product Lattice 也是有限的完全格
函数 的单调性
函数
Transfer Funtion
,对于gen/kill问题而言,该部分是单调的(never shrinks)。 Control Flow Merging
。当有多个分支合并时,可以看作每个分支和结果分支一一合并的结果(参考lab1的 meetInto )。
由于 gen/kill 的 Transfer Function 的单调性已经证明过,这里只证明 Control Flow Merging 的单调性:
要证明
是单调的,只需要证明 ,若有 ,则必有 。 由lub的定义,有
, ,故有 ,即 是 和 的一个上界,而 是 和 的最小上界,所以 。 要证明
是单调的,只需要证明 ,若有 ,则必有 。 由glb的定义,有
, ,故有 ,即 是 和 的一个下界,而 是 和 的最大下界,所以 。
证明这两部分的单调性后,还需要说明
When Will the Algorithm Reach the Fixed Point
假设在每次迭代中,只有一个节点的一个0变成了1,在最坏情况下,最终状态为所有节点的分量均为1,这样一共需要
08 May and Must Analysis, from a Lattice View
这部分主要解释为什么 May Analysis 的初始化为
May Analysis
上图的右侧是 May Analysis 的示意图。我们的分析总是从 unsafe 逐步走到 safe 的。以 Reaching Definitions 为例,这个分析是用来检测是否有变量未被初始化的,其具体方法是在程序的开头为所有变量都提供一个 undefined 的定义,如果这个最早的定义 Reach 到了程序的某一点,那么这个变量在这一点就是没有被初始化的。因此,该分析的 unsafe 状态就是所有的定义都没有 reach ,也即所有的变量都初始化了,这显然是错误的结论。随着函数
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 。
可以这样总结:
这两种算法中, MOP 更为精确,证明如下:
由于
, ,所以 , ,即 是 和 的一个上界,而 是 和 的最小上界,所以 。
当且仅当
Bit-Vector 即 gen/kill 问题都是 distributive 的,但也有一些分析是 undistributive 的,如 Constant Propagation 。
10 Constant Propagation
分析的目标是,判断某个变量在某一点的值是否是一个常量,并给出该值。
CFG 中的每个节点的 OUT 由若干个二元组组成,每个二元组
当
下面来分析前文提到的数据流分析三元组
考虑该分析的实际用途,用来在编译期间将变量优化为常量,因此不能出现非常量的变量被分析为常量的情况,所以是一个 Must Analysis ,为其设计 meet operator 如下:
, 其中 为任意值 , 其中 为任意值 ,其中 为常量 , 其中 为常量且
下面对于 statement
若
为 “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 算法,在求解最短路时只考虑被更新了的节点。
完结撒花🎊
- Post title:Data Flow Analysis Foundations
- Post author:Franky
- Create time:2023-08-15 21:18:28
- Post link:https://franky.pro/2023/08/15/Data-Flow-Analysis-Foundations/
- Copyright Notice:All articles in this blog are licensed under BY-NC-SA unless stating additionally.