Day 4 Data Flow Analysis-Foundations

视频地址

南京大学《软件分析》课程05（Data Flow Analysis - Foundations I）

南京大学《软件分析》课程06（Data Flow Analysis - Foundations II）

Content

另一角度来看迭代算法
偏序
上界下界
格，半格，
通过格来表述数据流分析框架
单调性和不动点理论
由迭代算法到不动点理论
从格来看may和must analysis
可分配性和MOP比较
常量传播（不可分配）
worklist algorithm（迭代算法的一个优化）

Iterative Algorithm，Another View

迭代算法就是产生了数据流分析的结果，而从另一个角度看：

该算法就是在每次遍历时更新结点的out信息，用一个元组来表示值，不断应用函数，直到两次输出的元组一样算法停止。

当X = F(X)时，X为不动点，算法到达了不动点

问题？

算法一定会达到不动点吗？
如果能达到不动点，只有一个不动点吗？我们求的是最好的不动点吗？
什么时候能到达不动点

Parital Order

定义

偏序说明集合里两个元素可能是不可比较的

Upper and Lower Bounds

定义

一些性质
- 并不是所有偏序集都有lub或者glb
- 如果一个偏序集有lub或glb，它肯定是唯一的

Lattice

定义：偏序集中任意两个元素它的lub和glb都存在，那它就是一个格

半格(Semlattice)

其实就是只存在一个

全格(Complete Lattice)

定义：格中任意子集的lub和glb都存在，则称为全格

top和bottom

有穷的格都是全格（反过来不一定）

Product Lattice

Data Flow Analysis Framework via Lattice

D：数据流分析方向
L：包含了域值和操作符（meet or join）的格
F：转换函数

数据流分析可以看作不断地在格的值域上应用转换函数和meet或join的操作符，回顾上述的问题

一定会停吗？------> 单调性
只有一个不动点吗？最好的不动点？ ------>不动点定理

Monotonicity

f：L->L（L是格）是单调的：

x<=y ------> f(x)<=f(y)

Fixed-Point Theorem

全格是单调有界的，则不动点可以通过迭代应用函数得到

Existence of Fixed Point

bottom <= f(bottom)：显然
f(bottom) <= f(f(bottom))：单调性
继续套娃
L又是有限的，所以会到不动点

Best Fixed Point

假设另一个不动点，数据归纳去证

Relate Iterative Algorithm to Fixed-Point Theorem

将两者关联，不动点定理的结论才能使用

F也是单调的：
- Out never shrinks
- 证明join和meet运算符的单调性

When will the algorithm reach the fixed point

最坏情况：（h*k）：h代表高度，k代表CFG中k个结点
- 每次只变化一个（一个node的一个值）：000 —> 001

May and Must Analyses，a Lattice View

important 图

无论是may还是must，都是unsafe result -> safe result

How Precise is Out Solution

MOP

对所有的path应用path的F，在将结果meet（join或union）一下

有一些path不会执行：先x=10，后if（x>10）
没有边界的（while），不可枚举的（大程序），其实是概念上的

ours vs MOP

易证出：MOP<=ours ------> MOP更加准确

当F是可分配的的时候：F（x U y）= F（x）U F（y）：ours和MOP是一样准确的

Bit-vector or Gen/kill problems（集合的交、并）都是可分配的

Constant Propagation - not distributive

定义：x在程序某个点时是否一定指向一个常量（所有的path，x都应为一个值）

Direction：forwards
Lattice：

Transfer Function
- _代表通配符
- 只关注赋值

为什么是不可分配的：

Worklist Algorithm，an optimization of Iterative Algorithm

核心：只计算in变化的block