Data Flow foundation

前面两节讲的是data flow analysis的示例，这一节讲的是其理论基础，包含许多编译和数学分析的知识，较为晦涩。

以defination的伪代码举例，其为forword以及采用may策略。

给定一个有𝑘k个节点的CFG，迭代算法在每轮迭代中更新每个节点n的OUT[n]。假设该数据流分析中的值域为𝑉V，我们可以定义一个k-tuple来表示每次迭代分析后的结果：

(𝑂𝑈𝑇[𝑛1], 𝑂𝑈𝑇[𝑛2], … , 𝑂𝑈𝑇[𝑛𝑘])
它是集合(𝑉1×𝑉2 … ×𝑉𝑘)中的一个元素，这个集合记做𝑉𝑘.

每轮迭代可以视作从𝑉𝑘中的一个元素到另一个新元素的映射，映射过程就是transfer functions和control-flow handling，我们将这个映射过程抽象为一个函数𝐹:𝑉𝑘→𝑉𝑘。

在上述抽象的基础上，may&forward analysis算法可以视作不断输出一系列的k-tuple（元组），直到某个k-tuple与上一个k-tuple相同：

𝑖𝑡𝑒𝑟 𝑖: (𝑣1𝑖,𝑣2𝑖, … ,𝑣𝑘𝑖)=𝑋𝑖=𝐹(𝑋𝑖−1)
𝑖𝑡𝑒𝑟 𝑖+1: (𝑣1𝑖+1,𝑣2𝑖+1, … ,𝑣𝑘𝑖+1)=𝑋𝑖+1=𝐹(𝑋𝑖)
在这时，我们可以得到以下关系：

𝑋𝑖=𝑋𝑖+1=𝐹(𝑋𝑖)
我们称满足𝑋=𝐹(𝑋)的X是一个不动点（fixed point），并称上述迭代算法到达了一个不动点（a fixed point）**。

对于这样一种算法，我们提出三个问题：

1. 这个算法能够保证一定能终止（到达不动点/有解）吗？
2. 如果上一个问题的答案是肯定的，那么只有一个解/不动点吗？如果有多个不动点，哪一个是最好的、或者说最精确的？
3. 什么时候这个算法能够到达不动点呢？

接下来我们学习一些数学知识来解答问题。

Partial Order（偏序）

偏序集有三个特性：

1、假设有偏序集P，任意的x元素满足x≼x，自反性
2、任意x,y属于P，当x≼y且y≼x时，可推出x=y，对抗性
3、任意x,y,z属于P，x≼y且y≼z，可推出x≼z，传递性

example：

整数集的偏序关系可以理解为小于等于，整数集满足偏序集定义。

String类型数据的substring方法也满足偏序关系

如图所示的字符集合也满足偏序关系。

至此，我们对偏序也有了一个大致的定义：如果A是B的“一部分”，则A偏序于B。偏序集中的元素是部分可比较的，不一定是所有元素都可以互相比较。

Upper and Lower Bounds（上界和下界）

给定一个偏序集(𝑃,≼)(P,≼)和它的子集𝑆S（𝑆⊆𝑃S⊆P），我们说𝑢∈𝑃u∈P是𝑆S的一个上界，当且仅当∀ 𝑥∈𝑆, 𝑥≼𝑢∀ x∈S, x≼u；类似地，𝑙∈𝑃l∈P是𝑆S的一个下界，当且仅当∀ 𝑥∈𝑆, 𝑙≼𝑥∀ x∈S, l≼x。

同时我们也给出了最小上界（least upper bound或join）和最大下界(greatest lower bound或meet)的定义，

最小上界（叫做lub或join），记为⌊⌋𝑆⌊⌋S，对于𝑆S的每一个上界𝑢u，有⌊⌋𝑆≼𝑢⌊⌋S≼u；

最大下界（叫做glb或meet），记为⌈⌉𝑆⌈⌉S，对于𝑆S的每一个下界𝑙l，有𝑙≼⌈⌉𝑆l≼⌈⌉S。

若𝑆S只包含两个元素𝑎a和𝑏b，我们也可以将⌊⌋𝑆⌊⌋S写为𝑎⌊⌋𝑏a⌊⌋b，将⌈⌉𝑆⌈⌉S写为𝑎⌈⌉𝑏a⌈⌉b。

特性：

Not every poset has lub or glbs 不是所有的P都有glb或lub

But if a poset has lub or glb, it will be unique 如果有lub或glb那他是唯一的

Lattice, Semilattice, Complete and Product Lattice

Lattice:给定一个偏序集(𝑃,≼)(P,≼)，∀ 𝑎,𝑏∈𝑃∀ a,b∈P，如果𝑎⌊⌋𝑏a⌊⌋b和𝑎⌈⌉𝑏a⌈⌉b均存在，那么(𝑃,≼)(P,≼)称为Lattice(格)。换句话说，一个偏序集是格，当且仅当其所有“元素对”构成的子集的最小上界和最大下界都存在。

Semilattice:放宽了格的概念：如果𝑎⌊⌋𝑏a⌊⌋b存在，该偏序集就是一个join semilattice；如果𝑎⌈⌉𝑏a⌈⌉b存在，它就是一个meet semilattice。不必同时满足两个约束。

complete lattice:加强了定义，对于给定偏序集(𝑃,≼)(P,≼)，它的任意子集𝑆S的最小上界和最大下界都存在，则(𝑃,≼)(P,≼)才能被称为完全格。幂集就是一种完全格。事实上，所有有限格（finite lattice，即𝑃P是有限集合）都是完全格。
每个完全格(𝑃,≼)(P,≼)都有一个最大元素⊤=⌊⌋𝑃⊤=⌊⌋P，称作top，一个最小元素⊥=⌈⌉𝑃⊥=⌈⌉P，称作bottom。

Product Lattice(乘积格)满足下面定义：

Data Flow Analysis Framework via Lattice

同之前一样，框架包含以下三个部分：

(D,L,F)：其中𝐷D指的是数据流的方向，包括前向和后向；𝐿L指的是由值域𝑉V和一个meet或join操作符构成的格；𝐹F指的是从𝑉V到𝑉V的一系列transfer functions。

数据流分析可以视作在格上不断迭代应用transfer functions和meet/join操作：

单调性（Monotonicity）和不动点（Fixed Point）定理

单调性

函数𝑓:𝐿→𝐿f:L→L（𝐿L是格）是单调的，当且仅当∀ 𝑥,𝑦∈𝐿∀ x,y∈L，𝑥≼𝑦⟹𝑓(𝑥)≼𝑓(𝑦)x≼y⟹f(x)≼f(y)。

不动点定理

给定一个完全格(𝐿,≼)(L,≼)，如果𝑓:𝐿→𝐿f:L→L是单调的且𝐿L是有限的，那么：

1. 𝑓f的最小不动点可以通过以下方式得到：不断迭代计算𝑓(⊥),𝑓(𝑓(⊥)), … ,𝑓𝑘(⊥))f(⊥),f(f(⊥)), … ,fk(⊥))，直到到达一个不动点。
2. 𝑓f的最大不动点可以通过类似的方式得到：不断迭代计算𝑓(⊤),𝑓(𝑓(⊤)), … ,𝑓𝑘(⊤))f(⊤),f(f(⊤)), … ,fk(⊤))，直到到达一个不动点。

证明不动点存在：

证明其是最小不动点：