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 = 所有定义的数量

顶部：空集：一无所知，初始值

底部：全集：所有定义都是到达定义

交操作：集合并集：降低值的层级，从一无所知到了解

简介

偏序集

格定义