Static Analysis 00 - Theoretical Fundations
# 前言
;
# 偏序集和偏序关系
# 基本概念
定义一个 偏序集 (partial-order set, poset) 为一个二元组 ,其中 是一个集合, 是定义在 上的偏序关系。
偏序关系 (partial ordering) 是满足如下性质的二元关系:
自反性 (reflexivity) :
反对称性 (anti-symmetry) :
传递性 (transitivity) :
几个有助于理解偏序关系的示例:
设 是若干个整数构成的集合,则 是一个偏序集,而 不是。
设 是若干个字符串构成的集合,则 是一个偏序集。
设 ,则 是一个偏序集。
# 上下界
设 是一个偏序集,对于一个子集 ,我们有如下定义:
设 ,若 ,则称 是 的一个 上界 (upper bound) 。
设 ,若 ,则称 是 的一个 下界 (lower bound) 。
定义 为 的 最小上界 (least upper bound, lub, or join) ,对于 的每个上界 ,满足 。
定义 为 的 最大下界 (greatest lower bound, glb, or meet) ,对于 的每个下界 ,满足 。
若 ,例如 ,则可记其 lub 为 ,记其 glb 为 。
不是每个偏序集都有 lub 或 glb 。
如果偏序集存在 lub 或 glb ,则其 lub 或 glb 必定是唯一的。
- 设 和 都是偏序集 的 glb ,则根据定义有 ,即 。
# 格
设 是一个偏序集,若对于 , 和 都存在,则称该偏序集为 格 (lattice) 。
设 是一个偏序集,若对于 , 存在或 存在,则称该偏序集为 半格 (semi-lattice) 。
如果仅 存在,则称其为 join semi-lattice 。
如果仅 存在,则称其为 meet semi-lattice 。
设 是一个格,若对于 , 和 都存在,则称该偏序集为 全格 (complete lattice) 。静态测试通常关注全格。
所有的有限格都是全格,但全格不一定是有限格。
对于全格,记其 top 为 ,bottom 为 。
几个有助于理解格的示例:
是格,其 和 可用 和 表示。
不一定是格,例如对于 , 不存在。
是格,其 和 可用 和 表示。
不一定是全格,例如对于正整数的全集 , 不存在。
是全格。
设 是 个格,如果每个格 的 和 都存在,则定义这些格的 product lattice 为 ,其中 ,并且满足如下性质:
如果构成 product 的每个格都是全格,则 product 也是全格。
设 是一个全格,定义 的 高度 (height) 为从其 到 的最长路径的长度,记为 。
# 格与不动点
设 是一个格,对于函数 ,若 ,则称 是 单调的 (monotonic) 。
对于一个函数 ,若 ,则称 是 的一个 不动点 (fixed point) ,记为 。
- 函数的不动点可能不存在,也可能不唯一。
设 是一个全格,如果 是有限的,并且函数 是单调的,则:
不断迭代 ,直至达到某个不动点,即为 的 最大不动点 (greatest fixed point) 。
不断迭代 ,直至达到某个不动点,即为 的 最小不动点 (least fixed point) 。
的不动点是存在的,并且 的最大和最小不动点各是唯一的。
证明
以最小不动点为例,首先证明 存在不动点:
由 可知 。根据 bottom 的定义有 。
因为 是单调的,所以 ,迭代地有 。
因为 是有限的,所以 使得 的值域落在 之间。那么对于 ,根据鸽巢原理有 。
由 可知 ,即 ,因此 存在不动点 。
随后证明据此迭代得到的是 的最小不动点:
不妨设 存在另一不动点 。根据 bottom 的定义有 。
因为 是单调的,所以 ,迭代地有 。
由 的任意性可知 ,其中 是迭代达到第一个不动点时的幂数。由此可知迭代得到的是 的最小不动点。
# 数据流分析的理论框架
# 不动点理论与迭代算法
设 是一个有限的全格,我们可以令每个基本块上的值 ,则其组合 是一个 product lattice 。
随后,我们可以将每轮迭代 等价为一个函数 ,包括:
每个基本块的 transfer function 。
表示数据流交汇的 join / meet function 。
可以证明 是单调的,因此可以证明数据流分析的迭代算法能够得到“最优解”,即其所到达的不动点是最大或最小不动点。
证明
在数据流分析中定义的 函数是单调的,因此我们只需证明 和 是单调的。
对于 ,我们证明 ,即可证明 是单调的。
根据 的定义有 ,又 ,所以 。由此可知 是 的一个上界。同时, 也是 的一个上界。
而 是 和 的最小上界,所以 。
设被分析的程序的 CFG 中有 个基本块,设与之对应的格 的高度为 ,则数据流分析的迭代算法最多经过 轮迭代后停止。
- 考虑最坏情况,假设每轮迭代中只有一个基本块上的格发生了一步变换(即只有一个 bit )。
# 格与 May / Must Analysis
无论是 may analysis 还是 must analysis ,都是从 unsafe result 出发,向 safe result 前进,停留在二者之间的某个位置。
unsafe result 表示 no definitions can reach ,即什么都没有;
safe result 表示 all definitions may reach ,即什么都可能有;虽然是 safe 的,却是 useless 的。
在多数情况下,may analysis 的 unsafe result 是 。我们以 reaching definition analysis 为例:(tbd.)
# Meet-Over-All-Paths Solution
设路径 ,定义路径 的 path transfer function 为路径上每条语句的 transfer function 的组合,即 。
定义语句 的 meet-over-all-paths solution, MOP 为从 到 的所有路径的 path transfer function 的 join / meet ,即:
MOP 和迭代算法的区别(TBD)
,所以有 ,即 是 和 的一个上界。根据 lub 的定义有 。
所以 ,也就是迭代算法的精度通常低于 MOP 。
- 当 具有分配律时,有 ,此时 。
# 基于格的数据流分析框架
定义 基于格的数据流分析框架 (data flow analysis framework via lattice) 为一个三元组 ,其中:
为数据流分析的方向(前向或后向分析);
是一个格,包括值域 和 join / meet 运算符 和 ;
是定义在 上的一组 transfer functions 。
静态测试通常关注全格。
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01