第十讲 基于格理论的数据流分析
内 容 一、控制流图 二、活性分析 三、可用表达式 四、很忙表达式 五、可达定义 六、初始化变量 七、符号分析 八、常量分析 九、区间分析
一、控制流图 (Control Flow Graph:CFG) 类型分析主要通过语法树进行 是流不敏感的(flow insensitive) S1; S2 的分析结果与 S2; S1 的结果相同 深入的分析是流敏感的(flow sensitive) 需要结束控制流图
一个控制流图是一个有向图 结点对应于程序中的点(语句) 边对应与可能的控制流 一个 CFG 有单个的入口和单个的出口 如果 v 是 一个CFG中 的一个点,则: pred(v) 是指该点直接前面点的集合 succ(v) 是指该点直接后面点的集合
数据流分析与格 传统的数据流分析(我们要讨论的内容) 从一个 CFG 和一个具有有限高度的格 L 开始 对于 CFG 中的每个点 v, 我们赋予一个变量 [v],其取值范围 是 L 中的元素. 对于编程语言中的每个构造块, 我们定义一个数据流约束(dataflow constraint ) 该约束反映了一个点与其它点(特别是邻居)之间值的关系
对于一个CFG,我们可以抽取变量的约束的集合 如果所有的约束刚好是等式或者不等式(右边单调) 我们就可以利用不动点算法求唯一的最小解 如果所有的解对应于程序的正确信息,则数据流约束是“确定的”(sound) 因为解可能或多或少地不精确,所以分析是“保守”的(conservative) 但计算最小解将获得最大的精确度
F(x1, . . . , xn) = (F1(x1, . . . , xn), . . . , Fn(x1, . . . , xn)) 不动点算法 如果一个 CFG 具有点 V = {v1, v2, . . . , vn}, 我们可以这样构造格Ln 假定点 vi 产生数据流等式 [vi] = Fi([v1], . . . , [vn]) 我们构造联合函数 F : Ln → Ln F(x1, . . . , xn) = (F1(x1, . . . , xn), . . . , Fn(x1, . . . , xn))
计算不动点 x 的直观算法: x = (⊥, . . . , ⊥); 每个语句未利用 以前语句的结果 改进:利用以前语句的结果 do { t = x; x = F(x); } while (x t); 每个语句未利用 以前语句的结果 改进:利用以前语句的结果 x1 = ⊥; . . . ; xn = ⊥; do { t1 = x1; . . .; tn = xn; x1 = F1(x1, . . . , xn); . . . xn = Fn(x1, . . . , xn); } while (x1 t1 ∨ . . . ∨ xn tn); X1: 第i个结点结束时 的值集合 迭代时重复计算量大 许多等式已经不变!
实际使用的算法: x1 = ⊥; . . . ; xn = ⊥; q = [v1, . . . , vn]; while (q []) { assume q = [vi, . . .]; y = Fi(x1, . . . , xn); q = q.tail(); if (y xi) { for (v ∈ dep(vi)) q.append(v); xi = y; } dep(vi)是被Vi影响的点的集合
二、活性(Liveness)分析 一个变量在程序的某个点是活跃的,如果: 它的当前值在后面程序执行时可能被读取 我们的分析借助于一个幂集格(powerset lattice) 其元素是程序中的变量
考虑如下的程序: 构造格: L = (2{x,y,z},⊆) {x, y, z} {x, y} {x, z} {y, z} var x, y, z; x = input; while (x>1) { y = x/2; if (y>3) x = x-y; z = x-4; if (z>0) x = x/2; z = z-1; } output x; {x, y, z} {x, y} {x, z} {y, z} {x} {y} {z} {} What’s the meaning?
我们引入一个辅助定义: 对任何一个CFG 结点 v,我们引入一个约束变量 [v] [v] 代表在该结点前活跃的程序变量集 JOIN(v) = ∪ [w] w∈succ(v) 对于退出结点,约束为: [exit] = {} 对“条件”和“输出”语句,约束为: [v] = JOIN(v) ∪ vars(E) 对于赋值语句,约束为: [v] = JOIN(v) \ {id} ∪ vars(E) 对于变量声明,约束为: [v] = JOIN(v) \ {id1, . . . , idn} 最后,对所有其它结点,约束为: [v] = JOIN(v) 其中: vars(E) 表示出现在 E 中的变量 “\” 表示减去:原来的值不再起作用 这些约束明显是单调的(为什么?) F(x1, . . . , xn)
Program Constraints var x, y, z; [var x,y,z;] = [x=input] \ {x, y, z} while (x>1) { y = x/2; if (y>3) x = x-y; z = x-4; if (z>0) x = x/2; z = z-1; } output x; [var x,y,z;] = [x=input] \ {x, y, z} [x=input] = [x>1] \ {x} [x>1] = ([y=x/2] ∪ [output x]) ∪ {x} [y=x/2] = ([y>3] \ {y}) ∪ {x} [y>3] = [x=x-y] ∪ [z=x-4] ∪ {y} [x=x-y] = ([z=x-4] \ {x}) ∪ {x, y} [z=x-4] = ([z>0] \ {z}) ∪ {x} [z>0] = [x=x/2] ∪ [z=z-1] ∪ {z} [x=x/2] = ([z=z-1] \ {x}) ∪ {x} [z=z-1] = ([x>1] \ {z}) ∪ {z} [output x] = [exit] ∪ {x} [exit] = {}
Constraints 第一次迭代结果 [entry] = {} [entry] = {} [var x, y, z;] = {} [x=input] = {} [x>1] = {x} [y=x/2] = {x} [y>3] = {x, y} [x=x-y] = {x, y} [z=x-4] = {x} [z>0] = {x, z} [x=x/2] = {x, z} [z=z-1] = {z} [output x] = {x} [exit] = {} [entry] = {} [var x, y, z;] = {} [x=input] = {} [x>1] = {} [y=x/2] = {} [y>3] = {} [x=x-y] = {} [z=x-4] = {} [z>0] = {} [x=x/2] = {} [z=z-1] = {} [output x] = {} [exit] = {} [var x,y,z;] = [x=input] \ {x, y, z} [x=input] = [x>1] \ {x} [x>1] = ([y=x/2] ∪ [output x]) ∪ {x} [y=x/2] = ([y>3] \ {y}) ∪ {x} [y>3] = [x=x-y] ∪ [z=x-4] ∪ {y} [x=x-y] = ([z=x-4] \ {x}) ∪ {x, y} [z=x-4] = ([z>0] \ {z}) ∪ {x} [z>0] = [x=x/2] ∪ [z=z-1] ∪ {z} [x=x/2] = ([z=z-1] \ {x}) ∪ {x} [z=z-1] = ([x>1] \ {z}) ∪ {z} [output x] = [exit] ∪ {x} [exit] = {}
Constraints 第二次迭代结果 第一次迭代结果 [entry] = {} [var x, y, z;] = {} [x=input] = {} [x>1] = {x} [y=x/2] = {x} [y>3] = {x, y} [x=x-y] = {x, y} [z=x-4] = {x} [z>0] = {x, z} [x=x/2] = {x, z} [z=z-1] = {z} [output x] = {x} [exit] = {} [entry] = {} [var x, y, z;] = {} [x=input] = {} [x>1] = {x} [y=x/2] = {x} [y>3] = {x, y} [x=x-y] = {x, y} [z=x-4] = {x} [z>0] = {x, z} [x=x/2] = {x, z} [z=z-1] = {x, z} [output x] = {x} [exit] = {} [var x,y,z;] = [x=input] \ {x, y, z} [x=input] = [x>1] \ {x} [x>1] = ([y=x/2] ∪ [output x]) ∪ {x} [y=x/2] = ([y>3] \ {y}) ∪ {x} [y>3] = [x=x-y] ∪ [z=x-4] ∪ {y} [x=x-y] = ([z=x-4] \ {x}) ∪ {x, y} [z=x-4] = ([z>0] \ {z}) ∪ {x} [z>0] = [x=x/2] ∪ [z=z-1] ∪ {z} [x=x/2] = ([z=z-1] \ {x}) ∪ {x} [z=z-1] = ([x>1] \ {z}) ∪ {z} [output x] = [exit] ∪ {x} [exit] = {}
Constraints 第三次迭代结果 第二次迭代结果 [entry] = {} [entry] = {} [var x, y, z;] = {} [x=input] = {} [x>1] = {x} [y=x/2] = {x} [y>3] = {x, y} [x=x-y] = {x, y} [z=x-4] = {x} [z>0] = {x, z} [x=x/2] = {x, z} [z=z-1] = {x, z} [output x] = {x} [exit] = {} [entry] = {} [var x, y, z;] = {} [x=input] = {} [x>1] = {x} [y=x/2] = {x} [y>3] = {x, y} [x=x-y] = {x, y} [z=x-4] = {x} [z>0] = {x, z} [x=x/2] = {x, z} [z=z-1] = {x, z} [output x] = {x} [exit] = {} [var x,y,z;] = [x=input] \ {x, y, z} [x=input] = [x>1] \ {x} [x>1] = ([y=x/2] ∪ [output x]) ∪ {x} [y=x/2] = ([y>3] \ {y}) ∪ {x} [y>3] = [x=x-y] ∪ [z=x-4] ∪ {y} [x=x-y] = ([z=x-4] \ {x}) ∪ {x, y} [z=x-4] = ([z>0] \ {z}) ∪ {x} [z>0] = [x=x/2] ∪ [z=z-1] ∪ {z} [x=x/2] = ([z=z-1] \ {x}) ∪ {x} [z=z-1] = ([x>1] \ {z}) ∪ {z} [output x] = [exit] ∪ {x} [exit] = {}
从该信息,一个聪明的编译器可以发现 y 和 z 从来没有同时活跃, z = z-1 中的赋值从未被用过。 因此,该程序可以被优化: 冗余赋值! var x, y, z; x = input; while (x>1) { y = x/2; if (y>3) x = x-y; z = x-4; if (z>0) x = x/2; z = z-1; } output x; var x,yz; x = input; while (x>1) { yz = x/2; if (yz>3) x = x-yz; yz = x-4; if (yz>0) x = x/2; } output x; 节省了一个赋值语句! 寄存器分配更合理!
三、可用表达式 (Available expression) 一个重要的表达式是可用的,如果 它的当前值已经计算过 对应的幂集格,元素是程序中出现过的所有表达式 比较关系是反的(“以前”:从上到下) 程序例子: var x, y, z, a, b; z = a+b; y = a*b; while (y > a+b) { a = a+1; x = a+b; }
L = (2{a+b,a*b, y>a+b,a+1},⊇) 其中含 4 个表达式,对应的格为: L = (2{a+b,a*b, y>a+b,a+1},⊇) 重要表达式
定义: JOIN(v) = ∩[w] 对于入口,约束为: [entry] = {} w∈pred(v) 对于入口,约束为: [entry] = {} 如果 v 包含一个条件表达式 E, 约束为:[v] = JOIN(v) ∪ exps(E) 如果 v 包含输出语句 E,约束为:[v] = JOIN(v) ∪ exps(E) 如果 v 包含赋值语句 id=E, 约束为: [v] = (JOIN(v) ∪ exps(E))↓id ↓id 表示移除所有包含指向变量 id 的表达式 对所有其它结点,约束为:[v] = JOIN(v)
函数 exps 定义为: op 是任何二元操作符 对于前面的例子程序,约束为: [entry] = {} exps (intconst) = ∅ exps (id) = ∅ exps (input) = ∅ exps (E1opE2) = {E1 op E2} ∪ exps (E1) ∪ exps (E2) op 是任何二元操作符 对于前面的例子程序,约束为: var x, y, z, a, b; z = a+b; y = a*b; while (y > a+b) { a = a+1; x = a+b; } [entry] = {} [var x, y, z, a, b;] = [entry ] [z=a+b] = exps(a+b) ↓z [y=a*b] = ([x=a+b] ∪ exps(a*b)) ↓y [y>a+b] = ([y=a*b] ∩ [x=a+b]) ∪ exps(y>a+b) [a=a+1] = ([y>a+b] ∪ exps(a+1))↓a [x=a+b] = ([a=a+1] ∪ exps(a+b))↓x [exit] = [y>a+b]
which confirms our assumptions about a+b. 运用不动点算法,可以得到: [entry] = {} [var x,y,z,a,b;] = {} [z=a+b] = {a+b} [y=a*b] = {a+b, a*b} [y>a+b] = {a+b, a*b, y>a+b} [a=a+1] = {} [x=a+b] = {a+b} [exit] = {a+b} which confirms our assumptions about a+b.
优化程序: var x,y,z,a,b; z = a+b; y = a*b; while (y > a+b) { a = a+1; x = a+b; } var x, y, z, a, b, aplusb; aplusb = a+b; z = aplusb; y = a*b; while (y > aplusb) { a = a+1; x = aplusb; }
四、很忙表达式(Very Busy Expression) 一个表达式“很忙”,如果: 它的值改变之前被再次计算 定义的格与“可用表达式”相同。 对于图中的点 v, [v] 表示那些在该点前忙的表达式
定义: JOIN(v) = ∩[w] w∈succ(v) 出口点的约束为: [exit] = {} 条件与输出语句的约束为:[v] = JOIN(v) ∪ exps(E) 赋值语句的约束为: [v] = JOIN(v) ↓ id ∪ exps(E) 其它语句的约束为: [v] = JOIN(v)
例子: var x, a, b; var x, a, b, atimesb; x = input; x = input; a = x-1; while (x>0) { output a*b - x; x = x-1; } output a*b; var x, a, b, atimesb; x = input; a = x-1; b = x-2; atimesb = a*b; while (x>0) { output atimesb - x; x = x-1; } output atimesb; 分析揭示:a*b 在循环中很忙
五、到达定义(Reaching Definitions) 给定一个程序点,“到达定义”是可能定义了当前变量值的那些赋值语句 需要的幂集格中,元素是所有的赋值语句
L = (2{x=input,y=x/2,x=x-y,z=x-4,x=x/2,z=z-1},⊆) 例子: var x, y, z; x = input; while (x>1) { y = x/2; if (y>3) x = x-y; z = x-4; if (z>0) x = x/2; z = z-1; } output x; 对应的格: L = (2{x=input,y=x/2,x=x-y,z=x-4,x=x/2,z=z-1},⊆)
定义: JOIN(v) = ∪ [w] w∈pred(v) 对于赋值语句,约束为: [v] = JOIN(v)↓id ∪ {v} 其它语句的约束为: [v] = JOIN(v) 其中,↓id 移除所有给变量 id 的赋值. 可以用来构造变量的定义-使用图 (CFG的子图) 用来进一步分析 dead code, code moion
定义-使用图 var x, y, z; x = input; while (x>1) { y = x/2; if (y>3) x = x-y; z = x-4; if (z>0) x = x/2; z = z-1; } output x;
对四类经典分析的总结 前向 后向 可能 可达定义 活性 一定 可用表达式 很忙表达式
前向与后向 正向分析 对每个程序点,计算过去的行为信息 可用表达式 可达定义 反向分析 对每个程序点,计算将来的行为信息 活性 很忙表达式
可能与必须 可能分析 描述可能为真的信息:计算上限近似 活性 可达定义 必须分析 描述一定为真的信息:计算下限近似 可用表达式 很忙表示式
六、初始化变量(Initialized Variables) 对于每个程序点,保证已初始化的变量集合 格是程序中变量的集合 初始化是过去的属性,需要用正向分析 是“必须”
对于每一个变量的使用,检查是否在“已初始化”的集合中 在入口点的约束为: [entry] = {} 辅值语句的约束为: [v] = ∩ [w] ∪ {id} w∈pred(v) 其它语句的约束为: [v] = ∩ [w] 对于每一个变量的使用,检查是否在“已初始化”的集合中
七、符号分析( Sign Analysis ) 如何决定各个表达式的符号 (+,0,-)? 可以解决的例子:是否除数是0 构造符号格: ? + 0 – ⊥ 其中: ? 表示符号值不是常量(已知道) ⊥表示值未知 The full lattice for our analysis is the map lattice: Vars |→ Sign where Vars is the set of variables occurring in the given program.
eval (α, intconst) = sign(intconst) 对每一个 CFG 结点 v,令 [v] 代表在该点所有变量的符号(-,0,+) 对于变量声明,我们引入常数映射,并返回?: [v] = [id1 |→ ?, . . . , idn |→ ?] 对于赋值语句,约束为: [v] = JOIN(v) [id |→ eval (JOIN(v), E)] 其它语句约束为: [v] = JOIN(v) 其中: JOIN(v) = ⊔ [w] w∈pred(v) eval 对表达式进行抽象估计: eval (α, id) = (id) eval (α, intconst) = sign(intconst) eval (α,E1 op E2) = opp’(eval (α,E1), eval (α,E2)) 其中, sign 给出整数的符号 opp’ 给出一个操作的抽象估计(见下页)
不同操作符的抽象估计
例如,表达式 (2>0)= =1 的分析结果是 ? +/+ 的分析结果是 ? 而不是 +,因为 1/2 被归到 0 中 有时候还可以提高精度 例如,表达式 (2>0)= =1 的分析结果是 ? +/+ 的分析结果是 ? 而不是 +,因为 1/2 被归到 0 中 我们可以在格中引入新元素 1, +0, 以及 -0 以获得精确的抽象值 这样,抽象表需要是 8 × 8 ? +0 -0 + 0 - 1 ⊥
八、常量传播( Constant Propagation) 在任何一个程序点,计算变量的值是否是确定的 分析过程与符号分析类似,基本格换为: ? -3 -2 -1 0 1 2 3 ⊥ 操作符的抽象方式: 以加法为例:λn λm. if (n ? ∧ m ?) {n + m} else {?}
分析例子: var x,y,z; x = 27; y = input; z = 2*x+y; if (x < 0) else { y = 12; } output y; var x,y,z; x = 27; y = input; z = 54+y; if (0) { y = z-3; } else { y = 12; } output y; var y; y = input; output 12;
九、区间分析(Interval Analysis) 区间分析为整数变量分析取值范围:下限和上限 格描述单个变量的取值范围: Interval = lift({[l, h] | l, h ∈ N ∧ l ≤ h}) 其中: N = {−∞, . . . ,−2,−1, 0, 1, 2, . . . ,∞} 是含无限点的整数集合,区间顺序定义为: [l1, h1] ⊑ [l2, h2] ⇔ l2 ≤ l1 ∧ h1 ≤ h2 全部是闭区间
对应的格: 很明显,这是一个高度无限的格
[v] = JOIN(v) [id |→ eval (JOIN(v), E)] 对于入口结点,应用常量函数(返回⊤ ): [entry] = λ x.[−∞,∞] 对于赋值语句,约束为: [v] = JOIN(v) [id |→ eval (JOIN(v), E)] 其它语句的约束为: [v] = JOIN(v) 其中: JOIN(v) = ⊔ [w] w∈pred(v)
eval 进行表达式的抽象估计: eval (α, id) = (id) eval (α, intconst) = [intconst, intconst] eval (α,E1 opE2) = opp’(eval (α, E1), eval (α, E2)) 抽象算术操作定位为: opp’([l1, h1], [l2, h2]) = 抽象比较操作定位为: opp’([l1, h1], [l2, h2]) = [0, 1]
w([l, h]) = [max{i ∈ B | i ≤ l}, min{i ∈ B | h ≤ i}] 格的高度无限,因此不能用单调框架(算法可能不终止) 应用“加宽”( widening )技术: 引入函数 w : Ln → Ln 使得: (F ◦ w)i (⊥, . . . ,⊥) 收敛在一个不动点上 从而给出一个关于程序的确定信息 如何“加宽”? w将区间映射到一个有限子集“B”: B ⊂ N,且包含−∞ 与 ∞ 典型地,B 的初值是出现在给定程序的所有整数常数 也可以使用一些启发式方法 对于一个单个区间: w([l, h]) = [max{i ∈ B | i ≤ l}, min{i ∈ B | h ≤ i}]
fix = ⊔ Fi(⊥, . . . ,⊥) fixw = ⊔ (F ◦ w)i(⊥, . . . ,⊥) “加宽”( Widening )用于解决“无限”的问题 “收缩” (narrowing)用于改进结果 定义: fix = ⊔ Fi(⊥, . . . ,⊥) fixw = ⊔ (F ◦ w)i(⊥, . . . ,⊥) 则: fix ⊑ fixw 不仅如此:fix ⊑ F(fixw) ⊑ fixw 对 F 的应用可以精化结果,且仍然是“确定的” (sound) 该技术被成为“收缩”技术,且可以被迭代使用 fix ⊑ Fi+1(fixw) ⊑ Fi(fixw) ⊑ fixw
如果没有“加宽”,下面的分析将是发散的: 应用“加宽”, 构造集合 B = {−∞, 0, 1, 7,∞} 可以得到收敛结果: y = 0; while (input) { x = 7; x = x+1; y = y+1; } [x |→ ⊥, y |→ ⊥] [x |→ [8, 8], y |→ [0, 1]] [x |→ [8, 8], y |→ [0, 2]] [x |→ [8, 8], y |→ [0, 3]] ... 应用“加宽”, 构造集合 B = {−∞, 0, 1, 7,∞} 可以得到收敛结果: [x |→ ⊥, y |→ ⊥] [x |→ [7,∞], y |→ [0, 1]] [x |→ [7,∞], y |→ [0, 7]] [x |→ [7,∞], y |→ [0,∞]]
注意: fixw ⊒ F ( fixw) ⊒ F2( fixw) ⊒ F3( fixw) . . . 不保证收敛 应用“收缩”,可以得到: [x |→ [8, 8], y |→ [0,∞]] 注意: fixw ⊒ F ( fixw) ⊒ F2( fixw) ⊒ F3( fixw) . . . 不保证收敛 必须应用启发方法决定“收缩”多少次 [x |→ ⊥, y |→ ⊥] [x |→ [7,∞], y |→ [0, 1]] [x |→ [7,∞], y |→ [0, 7]] [x |→ [7,∞], y |→ [0,∞]]