ROSE 編譯器框架/格

簡介

格是數學結構。它們可以用作表達物件之間順序的通用方法。這些資料可以在資料流分析中得到利用。

格可以描述基本塊對資料流值的影響轉換，也稱為流函式。

格可以描述資料流框架，當它們被例項化為包含一組資料流值、一組流函式和一個合併運算子的代數結構時。

偏序集

偏序： $\leq$

偏序是在集合 P 上的自反、反對稱和傳遞的二元關係 $\leq$ ，即

自反 x<=x
反對稱，如果 $x\leq y,y\leq x$ 則 x=y
傳遞：如果 $x\leq y,y\leq z$ 則 $x\leq z$

偏序不應與全序混淆。全序是偏序，但反之則不然。在全序中，集合 P 中的任何兩個元素都可以比較。這在偏序中不是必需的。可以比較的兩個元素被稱為可比

偏序集，也稱為poset，是指具有偏序的集合。

給定一個 poset，可能存在下確界或上確界。但是，並非所有 poset 都包含這些。

給定一個 poset P，具有集合 X 和順序 $\leq$

集合 X 的子集 S 的下確界是 X 中的元素 a，使得

$a\leq x$ 對於 S 中的所有 x 以及
對於 X 中的所有 y，如果對於 S 中的所有 x， $y\leq x$ 則 $y\leq a$

這個概念的對偶是上確界，它具有將 $\leq$ 與 $\geq$ 互換時下確界的定義。

如果我們只是選擇滿足第一個條件的 X 中的元素，我們就會得到一個下界。第二個條件確保我們具有（如果存在）唯一的最大下界。對上確界也是如此。

格是特定型別的 poset。特別地，格 L 是 poset P(X, $\leq$ ，其中對於格中的任何兩個元素 a 和 b，集合 {a, b} 具有並和交

並和交運算必須滿足以下條件

1) 並和交必須滿足交換律
2) 並和交必須滿足結合律
3) 並和交必須滿足冪等律，也就是說，x 與自身的並或 x 與自身的交都為 x。

如果格包含一個交，則它是一個交半格；如果格包含一個並，則它是一個並半格；類似地，存在交半格

（從維基百科獲得的定義，經過最小的修改）

格定義

格的定義（L, $\land$ , $\lor$ )

L 是在 $\leq$ $\leq$ 下的 poset，使得
- 每對元素都有唯一的最大下界（交）和最小上界（並）
- 並非所有 poset 都是格：poset 中可能不存在最大下界和最小上界。

無限格與有限格

無限格：無限格不包含 0（底）或 1（頂）元素，即使每一對元素在整個底層集合上都包含最大下界和最小上界。根據無界或無限集合的定義，我們知道，給定一個無界集合 X，對於 X 中的任意 x，我們都可以找到一個大於 x 的 x'（在某種排序下，在本例中為格）。最小下界也是如此。
有限格/有界格：底層集合本身具有最大下界和最小上界。目前我們將最大下界稱為 0，最小上界稱為 1。
- 如果 a $\leq$ x，對於 L 中的所有 x，則 a 是 L 的 0 元素， $\bot$ ，請記住這是一個唯一的元素
- 如果 a $\geq$ x，對於 L 中的所有 x，則 a 是 L 的 1 元素， $\top$

交集 $\land$ 是一個二元運算，使得 a $\land$ b 取集合的最大下界（這是格定義所保證的）。

類似地，並集 $\lor$ 返回集合的最小上界，由格的定義保證存在。

概括地說，格 L 是一個三元組 {X， $\land$ ， $\lor$ }，由一個集合、一個交集函式和一個並集函式組成。

交集和 $\land$ 的屬性。

我們將 $\lor$ 稱為 J，將 $\land$ 稱為 M。
封閉性：如果 x 和 y 屬於 L，則存在 L 中的唯一 z 和唯一 w，使得 x $\lor$ y = z，以及 x $\land$ y = w
交換律：對於 L 中的所有 x、y，x $\lor$ y = y meet x，x $\land$ y = y $\land$ x
結合性: (x $\lor$ y) $\lor$ z = x $\lor$ (y $\lor$ z), 同樣在 $\land$ 操作中
L 中有兩個獨特的元素，稱為底部 (_|_ ) 和頂部 (T)，使得對於所有 x，x $\lor$ _|_ = _|_ 且 x $\land$ T = T
許多格，除了少數例外（特別是對應於常量傳播的格），也是分配的：x $\lor$ y $\land$ z = (x $\land$ z) $\lor$ (y $\land$ z)

格和偏序

$x\sqsubseteq y$ 當且僅當 $x\sqcap y=x$

一個嚴格遞增鏈是集合 X 的元素序列，使得對於 x_i 在 X 中， $x_{1},x_{2},...,x_{n}$ 具有性質 $\bot =x_{1}\sqsubset x_{2}\sqsubset ...\sqsubset x_{n}=\top$ 。最長的鏈是最終索引為 n 的鏈，其中 n 是所有嚴格遞增鏈中最大的最終索引。

格的高度定義為其包含的最長嚴格遞增鏈的長度。

如果資料流分析格具有有限的高度和單調流函式，那麼我們知道相關的dataflow分析演算法將終止。

例如：如果格 L 的最長嚴格遞增鏈是有限的，並且到達頂端需要有限的步驟，我們可以推斷相關的dataflow演算法會終止。

(維基百科用於定義)

例如：位向量格

集合的元素是位向量
底部是 0 向量
頂部是 1 向量
交是按位與
並是按位或

$BV^{n}$ 表示長度為 n 的位向量格。

從多個不太複雜的格構建複雜的格

例如：按元素組合（連線）格的乘積運算
- 兩個具有交運算子 M1、M2 的格 L1 和 L2 的乘積：L1 x L2
- 格中的元素：{<x1, x2> | x1 來自 L1，x2 來自 L2}
交運算子：<x1, x2> M <y1, y2> = <x1 M y1, x2 M y2>
並運算子：<x1, x2> J <y1, y2> = <x1 J y1, x2 J y2>

例子
- BV^n 是 n 個底部為 0、頂部為 1 的簡單位向量格 BV^1 的乘積。

圖形表示 BV^3

          111
     /     |    \
110       101      011
 |    x        x   \
100       010      001
    \     |     /
          000

這裡交運算子和並運算子在格元素上產生了偏序。

x 小於或等於 (<=) y，當且僅當 x M y = x。

對於 BV^3：000 <= 010 <= 101 <= 111

格上的偏序關係是

傳遞性：如果 x <= y 且 y <= z，則 x <= z
反對稱性：如果 x <= y 且 y <= x，則 x = y
自反性：對於所有 x：x <= x

格的高度是其最長嚴格遞增鏈的長度

最大的 n，使得存在一個嚴格遞增鏈 x1、x2、...、xn，使得
底部 = x1 < x2 < xn = 頂部

對於 BV^3 格，高度 = 4

單調函式

單調函式是一個保持順序的函式。

示例

一個從 L 到自身的函式 f，f: L -> L，如果對於所有來自 L 的 x、y，x<=y ==> f(x)<=f(y)，則它是單調的

f: BV^3 -> BV^3: f (<x1 x2 x3>) -> <x1 1 x3>

格元組

簡單的分析可能需要複雜的格。

問題
- 到達常量：V 2^(v*c)，其中 v 是變數數量，c 是常量

解決方案
- 構造一個格元組，其中每個格對應一個變數

V = 常量 U {頂部，底部}

整數值：ICP

這用於常量傳播。元素：頂部、底部、整數、布林值

n M 底部 = 底部
n J 頂部 = 頂部
n J n = n M n = n
整數和布林值 m、n，如果 m != n，則 m M n = 底部，m J n = 頂部
- 格有三個層級：頂部元素、所有其他元素、底部元素
- 連線操作：從更高層級到更低層級
- 交操作：從更低層級到更高層級

與資料流分析的相關性

格為特定資料流分析提供一組流值。

格用於論證透過不動點迭代獲得的解的存在性

在每個程式點，格代表一個 IN[p] 或 OUT[p] 集（流值）
交：合併流值，例如集合並集，處理控制流分支合併
頂部通常代表最佳資訊（初始流值）。注意人們也可以使用頂部來代表最差基線資訊！！
底部值代表最差基線資訊
如果 BOTTOM <= x <= y <= TOP，則 x 是 y 的保守近似值。例如 x 是一個超集

例如活躍性分析

所有變數 x_1、x_2、...、x_n 的位向量

第一步：設計格值

頂部值：空集 {}，初始值，一無所知
底部值：全集 {x_1、x_2、...、x_n}：最大可能值，知道每個變數都是活躍的

n = 3，3 個變數情況：流值 ==> 某個點處的活躍變數集

S = {v1、v2、v3}

值集：2^3 = { 空集，{v1}，{v2}，{v3}，{v1、v2}，{v1、v3}，{v2、v3}，{v1、v2、ve} }

設計格

頂部值，最佳情況：無活躍 { T } // 頂部
底部值，最差情況：全部活躍 {v1、v2、v3}

設計交：集合並集（或操作）：將值降低到底部，與上下文無關

設計偏序關係 <= --> $\supseteq$

介於兩者之間，偏序關係：劣等/保守的解決方案在格中更低

         Top
      /    |   \
   {v1}   {v2}  {v3}
    |    x      x   |  
{v1, v2}  {v1,v3}  {v2,v3}
      \     |      /
      {v1, v2, v3} = Bottom

流函式 F： $f_{n}(X)=Gen_{n}\cup (X-Kill_{n}),\forall _{n}$ }

到達定義

值：2^n n = 所有定義的數量

頂部：空集：一無所知，初始值

底部：全集：所有定義都是到達定義

交操作：集合並集：降低值的層級，從一無所知到了解

簡介

偏序集

格定義