文章目錄

• 三、
• • 格理論
  • • 函數不動點
    • 偏序（Partial Order）
    • 上界和下界
    • 最小上界和最大下界
    • glb 和 lub的屬性
    • 格（lattice）、半格、完備格、乘積格
    • 數據流分析框架
    • 單調性和不動點原理
    • 對前面問題的回答
    • 從格的角度來看 may 、must analysis
  • MOP 和迭代算法的精度
  • 工作集算法（Worklist Algorithm）
• 總結

---

三、

格理論

函數不動點

??????函數不動點用初等數學可以這么理解：連續映射 f 的定義域包含值域，則存在一個 x 使得 f(x) = x 。其中點 (x , f(x)）為函數的不動點。

??????下面對前面三個示例采用的迭代算法進行分析，以前向分析 & may analysis 為例：

??????假設給定一個 CFG，節點數量為 k ，抽象域容量為 V。k 是程序中的基本塊數量，V 在 RDA 中是程序中的 definition 數量。一次迭代需要更新 k 個 V，描述為集合（V1 × V2 … × Vk），表示為Vk（V 的 k 次方）。Vk是一個 k 元組，里面的每一個元素都是一個抽象域。

??????所以每一輪迭代可以看做是應用轉換函數和控制流處理之后，從舊的Vk到新的Vk之間的轉換，這里用函數 F：Vk → Vk 來表示。算法的停止條件是舊的 Vk 和新的 Vk 相同的時候。對應于當所有的 OUT 不發生變化時。

??????假設第 i 次迭代之后的結果為 Xi，并且有 Xi+1 = F(Xi)。如果 Xi+1 = Xi ，那么表示在第 i+1 次迭代時算法停止（所有 OUT 不發生變化了），做一個簡單的代換可以得到：Xi = F(Xi) 。那么按照函數不動點的定義，認為此時達到了迭代算法的不動點（fixed point）。

??????在數據流分析中，通過采用迭代算法產生了一個解決方案。所以產生了三個問題：

??????問題1：算法能夠保證一定會停止嗎或者一定能夠達到不動點嗎？即迭代算法真的能產生一個解決方案嗎？

??????問題2：如果問題1的回答是肯定的話，那是否只有一個不動點或一個解決方案？如果解決方案多于一個的話，迭代算法得到的會是最優的嗎？

??????問題3：什么時候迭代算法能夠達到不動點，即什么時候能夠得到解決方案？

偏序（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) ?x ∈ P, x ? x (Reflexivity)
??????(2) ?x, y ∈ P, x ? y ∧ y ? x ? x = y (Antisymmetry)
??????(3) ?x, y, z ∈ P, x ? y ∧ y ? z ? x ? z (Transitivity)

?????? ? 是集合 P 上的一個二元關系 ，并且滿足上面三個屬性：自反、反對稱和傳遞，稱 ? 定義了在 P 上的偏序關系，(P, ?) 是一個偏序集。

??????例如：
??????1，當 P 為整數集合，? 為小于等于關系時。(P, ?) 是一個偏序集。
??????2，當 P 為整數集合，? 為小于關系時。(P, ?) 不是一個偏序集。因為不滿足自反性。
??????3，當 P 為英文單詞集合，? 為一個單詞是另一個單詞的子串關系時（比如 a ? b ,意味著單詞 a 是單詞 b 的子串）。(P, ?) 是一個偏序集。

??????偏序集中的偏序指的是什么意思呢？

??????在上圖中，下方的英文單詞集合便是一個偏序集。偏序指的是允許集合中的任意兩個元素不存在可比性，比如單詞 pin 和 sin 之間不存在子串關系。也就是說：沒有必要讓集合中的任意兩個元素滿足 ?。
??????4，當 P 為集合 {a ,b ,c} 的冪集，? 為一個集合是另一個集合的子集關系時。(P, ?) 是一個偏序集。

上界和下界

??????定義如下：Given a poset (P, ?) and its subset S that S ? P, we say that
????????????????????????u ∈ P is an upper bound of S, if ?x ∈ S, x ? u. Similarly,
????????????????????????l ∈ P is an lower bound of S, if ?x ∈ S, l ? x.

??????注意：這里上界和下界針對的是偏序集 P 的子集 S。

最小上界和最大下界

??????定義如下：We define the least upper bound (lub or join) of S, written ?S,if for every upper bound of S, say u, ?S ? u.
????????????????????????We define the greatest lower bound (glb, or meet) of S, written ?S, if for every lower bound of S, say l, l ? ?S.

??????下圖以冪集為例來說明這幾個概念之間的區別：

??????Usually, if S contains only two elements a and b (S = {a, b}), then
?S can be written a ? b (the join of a and b)
?S can be written a ? b (the meet of a and b)

glb 和 lub的屬性

??????一共有兩個屬性，見下圖：

格（lattice）、半格、完備格、乘積格

??????格的定義：Given a poset (P, ?), ?a, b ∈ P, if a ? b and a ? b exist, then (P, ?) is called a lattice .

??????也就是說：對于一個偏序集，如果任意兩個元素對存在 lub 和 glb，它就是一個格。

??????例如：
??????1，當 P 為整數集合，? 為小于等于關系時。(P, ?) 是一個格。
??????2，當 P 為英文單詞集合，? 為一個單詞是另一個單詞的子串關系時（比如 a ? b ,意味著單詞 a 是單詞 b 的子串）參見上圖。(P, ?) 不是一個格。 因為對于單詞 pin 和 sin ，它們的 lub 在 P 中不存在。
??????3，當 P 為集合 {a ,b ,c} 的冪集，? 為一個集合是另一個集合的子集關系時。(P, ?) 是一個格。

---

??????半格的定義：Given a poset (P, ?), ?a, b ∈ P,
??????????????????????????????if only a ? b exists, then (P, ?) is called a join semilattice
??????????????????????????????if only a ? b exists, then (P, ?) is called a meet semilattice

---

??????完備格的定義：Given a lattice (P, ?), for arbitrary subset S of P, if ?S and ?S exist, then (P, ?) is called a complete lattice.

??????例如：
??????1，當 P 為整數集合，? 為小于等于關系時。(P, ?) 不是一個完備格。因為對于所有正整數構成的子集，它不存在上界，也就不存在 ?S。
??????2，當 P 為集合 {a ,b ,c} 的冪集，? 為一個集合是另一個集合的子集關系時。(P, ?) 是一個完備格。

---

??????乘積格的定義：Given lattices L1 = (P1, ?1), L2 = (P2, ?2), …, Ln = (Pn, ?n), if for all i, (Pi , ?i) has ?i (least upper bound) and ?i (greatest lower bound), then we can have a product lattice Ln = (P, ?) that is defined by:

? P = P1 × … × Pn
? (x1, …, xn) ? (y1, …, yn) ? (x1 ? y1) ∧ … ∧ (xn ? yn) （乘積格中兩個元素滿足偏序關系，等價于對應于每一個格中的兩個元素滿足偏序關系的交集）
? (x1, …, xn) ? (y1, …, yn) = (x1 ?1 y1, …, xn ?n yn)（乘積格中兩個元素的 lub，等價于對應于每一個格中的兩個元素的 lub 的集合）
? (x1, …, xn) ? (y1, …, yn) = (x1 ?1 y1, …, xn ?n yn)（乘積格中兩個元素的 glb，等價于對應于每一個格中的兩個元素的 glb 的集合）

??????并且有：乘積格是一個格。 如果一個乘積格是完備格的乘積，那么這個乘積格也是一個完備格。

數據流分析框架

??????見圖：

??????對上圖的說明：

??????其中 L 是包含抽象域 V 的一個格，并且具有一個 meet ? o或者 join ? 操作，在數據流分析中，一般取 lub 和 glb 中的一個，比如在 may analysis 中，采用 join ?，取 lub；在 must analysis 中，采用 meet ?，取 glb。

??????左下方采用 RDA 來說明，右下方為一個格，其中的每一個元素都是一個抽象域 V 。可以看到對 OUT[s1] 的值 {a} 和 OUT[s3] 的值 {b} 取 ?得到的結果為 {a，b}，在 s2 上的轉換函數令 IN[s2] = {a，b} 變為 OUT[s2] = {a，b，c}，當然 OUT[s2] 也可以為 {a，b}。結合右下方的格來看，may analysis 的初始化為空，即 bottom，通過采用 join ? 操作，不斷地往 top 方向上靠攏。

單調性和不動點原理

??????在格上函數的單調性定義：A function f: L → L (L is a lattice) is monotonic if ?x, y ∈ L, x ? y ? f(x) ? f(y) 。

??????不動點原理（定理）：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(⊥)), …, fk(⊥) until a fixed point is reached
????????????the greatest fixed point of f can be found by iterating
??????????????????f(T), f(f(T)), …, fk(T) until a fixed point is reached

??????這里簡單提一句：對于 may analysis ，它是從 bottom 向 top 變化的，不動點原理告訴我們從 ⊥ 出發不斷的迭代函數 f ，最后得到的不動點是最小不動點，也就是最優的一個不動點。對于 may analysis ，它一定存在一個最大的不動點 T，在前面的示例中為 11111…111。must analysis 剛好相反，它一定存在一個最小的不動點 ⊥，在前面的示例中為 0000…000。

---

??????關于不動點原理的證明，一是要證明不動點原理的存在，二是要證明所得的不動點為最優的一個。下面僅證明從 ⊥ 出發的紅色語句。

??????最小不動點的證明中：因為通過不動點原理假設在 k 次迭代得到的不動點小于任意存在的一個不動點（ fFix = fk(⊥) ? x ），所以得證。

對前面問題的回答

??????問題1：算法能夠保證一定會停止嗎或者一定能夠達到不動點嗎？即迭代算法真的能產生一個解決方案嗎？
??????可以，回憶之前提到的 OUT 的增長是單調的，總會存在一個極限。 may 最大為 T， must 最小為 ⊥。

??????問題2：如果問題1的回答是肯定的話，那是否只有一個不動點或一個解決方案？如果解決方案多于一個的話，迭代算法得到的會是最優的嗎？
??????對于一個函數來講，只要滿足 x = f(x) 即可稱 x 為不動點，所以不動點并不唯一。目前我們知道的是根據不動點原理得到的不動點是最優的，而迭代算法是單調的，并且抽象域的大小是有限的，它滿足不動點原理的應用條件，所以迭代算法得到的結果是最優的。

??????問題3：什么時候迭代算法能夠達到不動點，即什么時候能夠得到解決方案？

??????上面得到的結論是迭代次數的最大值，即最多迭代 i 次就可以達到不動點。其中節點數量 k 很好理解，而格的高度 h 在數據流分析指的是抽象域的大小，上圖中冪集格對應的就是抽象域的大小為 3 的數據流分析。

從格的角度來看 may 、must analysis

??????寶藏圖片如下，這個圖片詳細介紹了兩種數據流分析的特點：

??????右邊的 may analysis 是 reach definition analysis，最下方為初始化值 ⊥ ，表示在每一個程序點沒有一個 definition 能夠達到，這是一個不安全的結論（或者說是錯誤的結論）；最上方為 T ，表示在每一個程序點每一個 definition 都可能達到，這是一個安全但是無用的結論（正確但無用）。而迭代算法需要從 unsafe → safe，在 safe 中有多個不動點，其中最小不動點處精度最高，而迭代算法到達的便是最小不動點。 must analysis 類似。

??????另一種角度來解釋最小、最大不動點。以 may 的最小不動點為例，算法迭代意味著一次次地執行控制流處理和轉換函數，其中，轉換函數是比較固定的，因為每一個基本塊的 genB 和 killB 是不變的。而控制流處理在 may 中采用的 join U ，執行結果為兩個元素的最小上界。例如：000 U 001 = 001, 010 U 100 =110 … 而不會一下子就得到 111 。因為在迭代中，我們每次取的都是最小的一步，所以最后達到的不動點必然是最小不動點。

MOP 和迭代算法的精度

??????Meet-Over-All-Paths Solution (MOP)指的是分別在 entry 到 exit 之間的每一條路徑上執行轉換函數，然后將每一條路徑的最終結果進行控制流處理。在某些路徑不執行的情況下仍進行控制流處理是不精確的，在碰到循環時無法確定邊界，在大型程序中路徑的數量很多的，不可枚舉，所以它不太實用。見下圖：

??????在下面的例子上看看迭代算法和 MOP 的差別：

??????證明如下：

??????采用比特位向量或者用 與和或 來代替 join和meet的 Gen/Kill 問題，是可分配的（distributive）。

工作集算法（Worklist Algorithm）

??????工作集算法是對迭代算法的優化，在迭代算法的一次迭代中，可以發現，如果某個 OUT[B] 在上一次迭代之后沒有變化，那么在下一次迭代中仍然會重復計算 OUT[B]。為了減少這種不必要的運算，引入了工作集算法，算法的思路比較簡單，就不談了。算法如下：

總結

??????本文主要介紹了格理論的相關知識，并應用到了數據流分析的迭代算法中，從理論上證明了迭代算法的一些優良特性。從格的視角總結了 may、must analysis的差異性，并對迭代算法的進一步優化產生了工作集算法。后面會單獨介紹常量傳播分析（Constant Propagation Analysis），這會是一個在格上進行數據流分析的不錯的練習。未完待續~

??????分享一首小阿七的歌曲《酒家》：https://www.bilibili.com/medialist/play/ml1297618174/BV1Z5411b7YX

總結

以上是生活随笔為你收集整理的静态程序分析chapter4 - 基于格（Lattice）理论的数据流分析的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。