0%

# Iterative Algorithm

• 对于一个含 $k$ 个节点的CFG，每个迭代算法对于每个node $n$ 更新$\mathrm{OUT}[n]$。

• 假设迭代算法的研究对象（domain）是$V$，定义一个k元组
$V^k=\left(\mathrm{OUT}\left[\mathrm{n}_{1}\right], \mathrm{OUT}\left[\mathrm{n}_{2}\right], \ldots, \mathrm{OUT}\left[\mathrm{n}_{\mathrm{k}}\right]\right)，V^k\in(V_1 \times V_2 \times \dots \times V_k)$
$V^k$ 即一次迭代产生的输出，每次迭代会更新$V^k$，可以将每次迭代经过transfer functions和control-flow handing的过程抽象为$F: V^k\rightarrow {V^{k}}’$

• 当$V^k\rightarrow {V^{k}}’$时，即$X=F(X)$ ，称$F(x)$在$X$处到达了不动点，$X$为$F(x)$的不动点，

# Poset & partial order（偏序集和偏序）

We define poset as a pair (P, ⊑) where ⊑ is a binary relation that defines a partial ordering over P, and ⊑ has the following properties:

(1) $\forall x \in P, x \sqsubseteq x$ (Reflexivity, 自反性)
(2) $\forall x, y \in P, x \sqsubseteq y \wedge y \sqsubseteq x \Rightarrow x=y \quad$ (Antisymmetry，反对称性)
(3) $\forall x,y,z \in P, x \sqsubseteq y \wedge y \sqsubseteq z \Rightarrow x \sqsubseteq z$ (Transitivity，传递性)

# Uppper and Lower Bounds（上界和下界）

Given a poset (P, ⊑) and its subset $S$ that $S\subseteq P$, we say that $u\in P$ is an upper bound of $S$, if $\forall x \in P, x\sqsubseteq u$. Similarly, $l∈P$ is an lower bound of $S$, if $\forall x \in P, l\sqsubseteq u$.

## 最小上界、最大下界

We define the least upper bound (lub or join) of $S$, written $⊔S$, if for every upper bound of $S$, say $u, ⊔S⊑u$. Similarly, We define the greatest lower bound (glb or meet) of $S$, written $⊓S$, if for every lower bound of $S$, say $l, l⊑⊓S$.

• 不是所有偏序集均存在lub或者glb（如先前灰色的集合就不含lub）
• 如果一个偏序集存在lub和glb，那么它是唯一的
• 证明： 设$g_1$ 和$g_2$ 同为 P 的glb，那么根据定义 $g_1\sqsubseteq (g_2 = \sqcap P)$ 并且$g_2\sqsubseteq (g_1 = \sqcap P)$，又因为反对称性，所以$g_1=g_2$

# Lattice, Semilattice, Complete and Product Lattice

## Lattice（格）

Given a poset $(P, ⊑), ∀a,b∈P$, if $a⊔b$ and $a⊓b$ exist, then $(P,⊑)$ is called a lattice.

## Complete Lattice，top & bottom（全格，$\top$ 和 $\perp$）*

Given a lattice $(P,⊑)$, for arbitrary subset $S$ of $P$, if $⊔S$ and $⊓S$ exist, then $(P,⊑)$ is called a complete lattice.

## Product Lattice

Given lattices $L_1=(P_1,⊑_1),L_2=(P_2,⊑_2),…,L_n=(P_n,⊑)n)$, if for all $i$, $(P_i,⊑_i)$ has $⊔i$(least upper bound) and $⊓_i$(greatest lower bound), then we can have a product lattice $L^n=(P,⊑)$ that is defined by:

• $P=P_{1} \times \ldots \times P_{n}$
• $\left(x_{1}, \ldots, x_{n}\right) \sqsubseteq\left(y_{1}, \ldots, y_{n}\right) \Leftrightarrow\left(x_{1} \sqsubseteq y_{1}\right) \wedge \ldots \wedge\left(x_{n} \sqsubseteq y_{n}\right)$
• $\left(x_{1}, \ldots, x_{n}\right) \sqcup\left(y_{1}, \ldots, y_{n}\right)=\left(x_{1} \sqcup_{1} y_{1}, \ldots, x_{n} \cup_{n} y_{n}\right)$
• $\left(x_{1}, \ldots, x_{n}\right) \sqcap\left(y_{1}, \ldots, y_{n}\right)=\left(x_{1} \sqcap_{1} y_{1}, \ldots, x_{n} \sqcap_{n} y_{n}\right)$

Product Lattice仍是Lattice，若每个子格为全格，那么乘积也是全格。

# Data Flow Analysis Framework via Lattice

• D：指数据流分析的方向，i.e., forward or backward；
• L：指lattice，该格表示所有domain值域，以及meet（$\sqcap$）或join（$\sqcup$）操作；
• F：一组transfer function。

# Monotonicity and Fixed Point Theorem

## Monotonicity（单调性）

A function $f: L→L$ ($L$ is a lattice) is monotonic if $∀x,y∈L$, $x⊑y⟹f(x)⊑f(y)$

## Fixed-Point Theorem

Given a complete lattice ($L,⊑$), if (1) $f:L→L$ is monotonic and (2) $L$ is finite, then the least fixed point of $f$ can be found by iterating $f(⊥), f(f(⊥)), \dots, f^k(⊥)$ until a fixed point is reached the greatest fixed point of $f$ can be found by iterating $f(\top),f(f(\top)),\dots, f^k(\top)$ until a fixed point is reached.

(1) Existence

（2）Least Fixed Point（数归法，证明最小）

# Relate lterative Algorithm to Fixed Point Theorem

1. 程序中每一个状态为一个product lattice
2. Transfer function和join/meet fucntion可以视为F

1. Transfer function是单调的，因为通过之前分析，所有Gen/Kill的函数都是单调的；

2. Join/meet function是单调的，证明如下

要证Join/meet function，就是要证$\forall x, y, z \in L, x \sqsubseteq y \Rightarrow x\sqcup z \sqsubseteq y \sqcup z$

由 $\sqcup$ 定义可得，$y \sqsubseteq y \sqcup z$，

由于$\sqsubseteq$传递性，$x \sqsubseteq y$，因此$x \sqsubseteq y \sqcup z$，因此 $y \sqcup z$ 是 $x$ 的上界，

注意到 $y \sqcup z$ 也是 $z$ 的上界，而$x\sqcup z$ 是 $x$ 和 $z$ 的最小上界，

因此 $x \sqsubseteq y \Rightarrow x\sqcup z \sqsubseteq y \sqcup z$

The height of a lattice $h$ is the length of the longest path from Top to Bottom in the lattice.

# May/Must Analysis, A Lattice View*

Must和May分析的示意图如上图所示，对于Must分析，每个代码块都是从 $\top$ 开始的，因为在程序一开始，算法认为所有的待分析对象都是“合格”的（例如存活表达式分析中，算法认为每个表达式都是成活的）——这是一个不安全的状态，经过不断迭代，算法逐渐下降到最大不动点，虽然已经过了truth点（漏报），但是这已经是最好情况了（越往下走越safe但是结果也没意义了），对这些结果做优化能确保程序不出错（safe）。

# Distributivity（分配性） and MOP

## Iterative Algorithm v.s. MOP

MOP比Iterative分析更精确，也就是说路径敏感比敏感更精确，下面为证明（这里只需证明两条路径的情况，其它数归即可）：

BitVector或是Gen/Kill问题（set union/intersection for join/meet）都是满足分配率的

# Constant Propagation

Given a variable $x$ at program point p, determine whether $x$ is guaranteed to hold a constant value at $p$

## Lattice

Domain： UNDEF → {…, -2, -1, 0, 1, 2, …} → NAC ，→ 表示 $\sqsubseteq$ 关系

Meet Operator $\sqcap$：

• $\mathrm{NAC} \sqcap v= \mathrm{NAC}$
• $\mathrm{UNDEF} \sqcap v= v$
• $c \sqcap v= \mathrm{NAC}$ （c 为一常量）
• $c \sqcap c= c$
• $c_1 \sqcap c_2 = \mathrm{NAC}$

## Transfer Function

• s: x=c; $gen=\{(x,c)\}$
• s: x=y; $gen=\{(x, val(y))\}$
• s: x=y op z; $gen=\{(x, f(x,z))\}$

# Worklist Algorithm

Iterative Algorithm的优化，Iterative 存在冗余的计算，而Worklist只计算有变化的node：

# 分析特性

• 流敏感：程序语句随意调换位置，分析结果不变为流非敏感，否则为流敏感；
• 路径敏感：考虑程序中路径的可行性；