南京大學(xué)《軟件分析》學(xué)習(xí)筆記 1

課太好了，忍不住寫篇博客從頭推導(dǎo)一下

理論

偏序集 poset

偏序關(guān)系 偏序關(guān)系是滿足下面三個(gè)條件的二元關(guān)系：

• 自反性

• 反對(duì)稱性

• 傳遞性

偏序集 poset 偏序集定義為一個(gè)集合以及集合上的偏序關(guān)系，表示為 \((P, \sqsubseteq)\)

上界 upper bound 和下界 lower bound 給定一個(gè)偏序集 \((P, \sqsubseteq)\)，那么對(duì)于一個(gè)子集 \(S \subseteq P\)，它的上界是 \(u\) 當(dāng)且僅當(dāng) \(\forall x \in S\) 都滿足 \(x \sqsubseteq u\)。下界的定義類似。

最小上界 lub 和最大下界 mlb 給定一個(gè)偏序集 \((P, \sqsubseteq)\)，那么對(duì)于一個(gè)子集 \(S \subseteq P\)，它的最小上界 \(\sqcup S\) 滿足對(duì)于所有的上界 \(u\) 都滿足 \(\sqcup S \sqsubseteq u\)。符號(hào) \(\sqcup\) 可以叫做并 join，\(\sqcup S\) 表示并運(yùn)算作用在整個(gè)集合 \(S\) 上，并也可以當(dāng)成一個(gè)二元運(yùn)算符用 \(a \sqcup b\) 表示集合 \({a, b}\) 的最小上界。最大下界 \(\sqcap S\) 的定義類似，符號(hào) \(\sqcap\) 可以叫做交 meet。

• 不是每一個(gè)偏序集都有最小上界和最大下界。證明：很容易舉出反例。

• 最小上界和最大下界一定是唯一的。證明：反證法假設(shè)不唯一，通過(guò)反對(duì)稱性容易證偽。

格 Lattice

格 lattice （格的序理論定義）如果一個(gè)偏序集 \((P, \sqsubseteq)\) 中的 \(\forall a, b \in P\) 都滿足 \(a \sqcup b\) 和 $a \sqcap b $ 存在，那么這個(gè)偏序集叫做一個(gè)格，記作 \(L = (P, \sqsubseteq)\)

半格 semilattice 如果一個(gè)偏序集 \((P, \sqsubseteq)\) 中的 \(\forall a, b \in P\) 都滿足只有 \(a \sqcup b\) ，那么這個(gè)偏序集叫做一個(gè)并半格。

完全格 complete lattice 如果一個(gè)偏序集 \((P, \sqsubseteq)\) 的任意一個(gè)子集 \(S\) 都滿足最小上界和最大下界都存在，那么這個(gè)偏序集是一個(gè)完全格。在完全格中 \(P\) 的最小上界和最大下界分別稱為 top 和 bottom。

• 每一個(gè)有限的格都是完全格。證明：容易證明，把求一個(gè)子集的最小上界的過(guò)程拆分為多個(gè)二元運(yùn)算。

• 完全格不一定都是有限的。證明：容易舉出反例 \(([0, 1], \leq)\)。

格的笛卡爾積 product lattice 可以把多個(gè)格通過(guò)笛卡爾積組裝成一個(gè)更大的格。

• 如果每一個(gè)格都是完全格，那么笛卡爾積也是完全格。

方法

程序一定會(huì)停止運(yùn)行（達(dá)到不動(dòng)點(diǎn)）

單調(diào)性 monotonicity 格上的某個(gè)函數(shù) \(F : L \rightarrow L\) 具有單調(diào)性當(dāng)且僅當(dāng) \(\forall x, y \in L, x \sqsubseteq y\) 滿足 \(F(x) \sqsubseteq F(y)\)（數(shù)據(jù)流分析的方法大多滿足 F 為單調(diào)增，下面的篇幅都假設(shè) F 是單調(diào)增的）。

數(shù)據(jù)流分析中轉(zhuǎn)移函數(shù)的單調(diào)性 現(xiàn)在我們要證明數(shù)據(jù)流分析中的轉(zhuǎn)移函數(shù) \(F\) 是滿足單調(diào)性的。轉(zhuǎn)移函數(shù) \(F\) 有兩個(gè)函數(shù)組成：meetInto 和 transferNode

首先考慮 transferNode，對(duì)于 IR 中的一個(gè)語(yǔ)句（對(duì)應(yīng)圖上的一個(gè)結(jié)點(diǎn)），它的 gen 集和 kill 集（use 集和 def 集）僅僅取決于語(yǔ)句本身，這意味著 gen 集和 kill 集是固定不變的，對(duì)于 \(OUT = gen \cup (IN - kill)\)，如果假設(shè) \(OUT\) 是語(yǔ)句在格上的取值，那么它的單調(diào)性完全依賴于 \(IN\) 的變化，所以只要 meetInto 單調(diào)增，那么 transferNode 也單調(diào)增。

其次考慮 meetInto，對(duì)于 \(IN = \sqcup_{preprocessor} OUT\)，我們要證明 \(\sqcup\) 是單調(diào)的，即 $\forall x, y, z \in L, x \sqsubseteq y $ 都有 \(x \sqcup z \sqsubseteq y \sqcup z\)。\(y \sqsubseteq y \sqcup z\)，又因?yàn)?\(x \sqsubseteq y\)，所以 \(x \sqsubseteq y \sqcup z\)，所以 \(x \sqcup z \sqsubseteq y \sqcup z\)

所以整體的函數(shù) \(F\) 是單調(diào)增的。

不動(dòng)點(diǎn)的存在性 現(xiàn)在證明對(duì)于完全格 \(L\)，必然存在一個(gè)不動(dòng)點(diǎn)滿足 \(F(p) = p, p \in L\)

根據(jù) bottom 的定義，對(duì)于格上的值 bottom（寫作 \(\perp\)），對(duì)其使用 \(F: L \rightarrow L\)，那么 \(F(\perp) \in L\)，那么必然有 \(\perp \sqsubseteq F(\perp)\)。

又因?yàn)?\(F\) 具有單調(diào)性，那么 \(F(\perp) \sqsubseteq F(F(\perp))\)，那么 \(\perp \sqsubseteq F(\perp) \sqsubseteq F(F(\perp)) \sqsubseteq ... F^k(\perp)\)

根據(jù)鴿籠原理，當(dāng) \(k >= |L| + 1\) 時(shí)，必然有 \(F^i(\perp) = F^j(\perp)\)，證畢。

最小不動(dòng)點(diǎn) 容易證明，從 bottom 逐步應(yīng)用函數(shù) \(F\) 得到的不動(dòng)點(diǎn)一定是最小的那個(gè)不動(dòng)點(diǎn)。

不動(dòng)點(diǎn)定理 給定一個(gè)完備格，如果函數(shù) \(F\) 是單調(diào)的，那么可以通過(guò)迭代\(F(\perp), F^2(\perp), ...\)直到達(dá)到一個(gè)不動(dòng)點(diǎn)，來(lái)找到最小不動(dòng)點(diǎn)。

程序會(huì)在有限時(shí)間內(nèi)停止運(yùn)行（達(dá)到不動(dòng)點(diǎn)）

格的高度 定義格的高度為從 top 到 bottom 的最長(zhǎng)距離

迭代時(shí)間 如果格的高度為 \(k\)，對(duì)于 \(L^n\) 迭代 \(n * k\) 次肯定可以到達(dá)不動(dòng)點(diǎn)。

May Analysis 和 Must Analysis

• 怎么理解這張圖？

右邊的圖以到達(dá)定值分析方法為例，如果我們?cè)谝婚_始給所有的變量創(chuàng)造一個(gè) var = undefined 的定值，把這個(gè)定值能否到達(dá)（0，1）作為圖中結(jié)點(diǎn)的在格上的值域，那么所有的 var = undefined 都不能到達(dá)意味著這個(gè)程序竟然初始化了所有的變量。這對(duì)于分析程序來(lái)說(shuō)是不安全的。所有的 var = undefined 都到達(dá)了意味著程序可能對(duì)于所有的變量都沒有初始化，這肯定是安全的，這會(huì)讓程序員去仔細(xì)檢查自己的代碼，但是這沒啥用，體現(xiàn)不出分析程序的價(jià)值。

• 為什么不動(dòng)點(diǎn)一定是 safe 的？

一個(gè)想法是這取決于轉(zhuǎn)移函數(shù) F，如果你在 F 中對(duì)于哪些不確定的情況都做出最壞的假設(shè)（對(duì)于分析來(lái)說(shuō)就是最 safe 的），那么不動(dòng)點(diǎn)必然是 safe 的。

MOP

懶得寫了，不如貼圖算了