第3章 控制流分析 内容概述 定义一个函数式编程语言，变量可以指称函数

Presentation on theme: "第3章 控制流分析 内容概述 定义一个函数式编程语言，变量可以指称函数"— Presentation transcript:

1 第3章 控制流分析 内容概述 定义一个函数式编程语言，变量可以指称函数
第3章 控制流分析 内容概述 定义一个函数式编程语言，变量可以指称函数 以dynamic dispatch problem为例（作为参数的函数被调用时，究竟执行的是哪个函数） 规范该控制流分析问题，定义什么是可接受的控制流分析 定义可接受分析在语义模型上的可靠性 讨论分析算法（语法制导、集合约束求解） 加上数据流分析 加上上下文信息

2 第3章 控制流分析 函数的不动点 若f(x) = x，则x是函数f 的不动点 求解含函数变量f 的方程
第3章 控制流分析 函数的不动点 若f(x) = x，则x是函数f 的不动点 求解含函数变量f 的方程 f = n. if n=0 then 1 else n  f(n  1) end 看成找下面函数的不动点 F   f. n. if n=0 then 1 else n  f(n  1) end F(阶乘函数) = 阶乘函数 该函数只有唯一的不动点 阶乘函数

3 第3章 控制流分析 函数的最小不动点 求解含函数变量f 的方程 f = n. if n=0 then 1
第3章 控制流分析 函数的最小不动点 求解含函数变量f 的方程 f = n. if n=0 then 1 else if n = 1 then f(3) else f(n  2) end 相应高阶函数有无数个不动点 当n是偶数时，结果是1 当n是奇数时，结果是a （ a可以任取 ） 最小不动点 n为偶数时, 结果是1; n为奇数时, 结果未定义

4 第3章 控制流分析 函数最小不动点的计算 例：F   f. n. if n=0 then 1 else n  f(n  1) end lfp(F) =  Fn () (n = 0, 1, …) F0 () =  (表示处处无定义的函数) F1 () = F(F0 ()) = ( f. n. if n = 0 then 1 else n  f(n  1) end )  = n. if n = 0 then 1 else n  (n  1) end = {0, 0!}

5 第3章 控制流分析 函数最小不动点的计算 例：F   f. n. if n=0 then 1 else n  f(n  1) end lfp(F) =  Fn () (n = 0, 1, …) F2 () = F(F1 ()) =( f. n. if n=0 then 1 else n  f(n 1)end)F1 () =n. if n = 0 then 1 else n  F1() (n  1) end = {0, 0!, 1, 1!} 依次逐步计算可得：, {0, 0!}, {0, 0!, 1, 1!}, {0, 0!, 1, 1!, 2, 2!}, … (构成一个上升链) lfp(F) =  Fn () = {0, 0!, 1, 1!, 2, 2!, …}

6 第3章 控制流分析 Tarski定理 令F : P(U)  P(U)是单调函数 其中U是集合，P(U)表示U的幂集 集合XU是F封闭的
第3章 控制流分析 Tarski定理 令F : P(U)  P(U)是单调函数 其中U是集合，P(U)表示U的幂集 集合XU是F封闭的 当且仅当F(X) X 集合XU是F致密的 当且仅当X  F(X) 定义X.F(X)和X.F(X) X.F(X) =  {X | F(X)  X} X.F(X) =  {X | X  F(X)}

7 第3章 控制流分析 Tarski定理 集合XU是F封闭的 当且仅当F(X) X 集合XU是F致密的 当且仅当X  F(X)
第3章 控制流分析 Tarski定理 集合XU是F封闭的 当且仅当F(X) X 集合XU是F致密的 当且仅当X  F(X) 定义X.F(X)和X.F(X) X.F(X) =  {X | F(X)  X} X.F(X) =  {X | X  F(X)} 引理 X.F(X)是最小的F封闭集合 X.F(X)是最大的F致密集合

8 第3章 控制流分析 Tarski定理 根据对偶性，只证明一种情况。首先证明引理：
第3章 控制流分析 Tarski定理 根据对偶性，只证明一种情况。首先证明引理： X.F(X) =  {X | X  F(X)}是最大F致密集合 最大是明显的 证明每个Xi都F致密，则i Xi也F致密则可 因为对每个i有Xi  F(Xi)，则i Xi  i F(Xi) 因为F单调，则对每个i有F(Xi)  F(i Xi) 由此可得iF(Xi)  F(i Xi) 由传递性，i Xi  F(i Xi)，即i Xi是F致密的

9 第3章 控制流分析 Tarski定理 再证明本定理（仍只证明 一种情况）： 1、X.F(X)是F的最小不动点
第3章 控制流分析 Tarski定理 再证明本定理（仍只证明 一种情况）： 1、X.F(X)是F的最小不动点 2、X.F(X)是F的最大不动点 令 = X.F(X)，则是致密的，  F() 由单调性，F()  F(F())，则F()也致密 由的定义知道F()   由和F()之间的这两个不等式得 = F() 不动点都是致密的，因而都包含在中，所以是最大不动点

10 第3章 控制流分析 归纳和余归纳(coinduction) 归纳法 初始条件、迭代规则、最小化条件 字母表A上的串集A归纳定义如下
第3章 控制流分析 归纳和余归纳(coinduction) 归纳法 初始条件、迭代规则、最小化条件 字母表A上的串集A归纳定义如下 (1) A; (2)若aA且xA, 则axA ;(3)除此以外， A不含其它元素 余归纳法 迭代规则(循环条件)，最大化条件 流可以通过余归纳法来定义 (1) 若t是A上的流且aA，则(a,t)也是A上的流； (2) A上的流集是满足上述规则的最大集合

11 第3章 控制流分析 大步操作语义和小步操作语义的区别 大步操作语义 小步操作语义 S1,   1 S2, 1  2
第3章 控制流分析 大步操作语义和小步操作语义的区别 大步操作语义 小步操作语义 S1,    S2, 1  2 S1; S2,   2 S1,   S1,   S1; S2,   S1; S2,  S1,    S1; S2,   S2, 

12 第3章 控制流分析 规范s和的区别 s和的区别主要在子句[fn]、[fun]和[app]上
第3章 控制流分析 规范s和的区别 s和的区别主要在子句[fn]、[fun]和[app]上  的这些子句体现为跟踪运行情况的0-CFA分析:某个函数不被执行，则其体中信息不被收集 因递归函数会引起检查过程不终止，导致讨论余归纳和最大不动点 s 是一种语法制导的0-CFA分析，它从程序中所有函数获取信息，而不管运行时函数是否真正被 执行，因此它是所获信息的一种近似 对于e : ((fn x => x) (fn y => let z = fn … in …)) (C, )  e中的无需 z 的信息

13 第3章 控制流分析 约束求解（对照P68的算法） Step 1 初始化 所有的C(l)和r(x)都是图的结点q
第3章 控制流分析 约束求解（对照P68的算法） Step 1 初始化 所有的C(l)和r(x)都是图的结点q D[q]表示q的值(函数集合)，初值是空集 E[q]表示q和其它结点的联系，初值是空链表 Step 2 构造图（对照P69的表和P70的初值） {t}  p： 出现在函数定义规则中，t应该在p所表示的函数集合中 p1  p2：出现在变量、条件表达式和let子句等规则中，记录于E[p1]，因p1变化则p2也可能变化

14 第3章 控制流分析 约束求解（对照P68的算法） Step 2 构造图
第3章 控制流分析 约束求解（对照P68的算法） Step 2 构造图 {t}  p  p1  p2：出现在函数应用规则中，记录于E[p1]和E[p]，因p1和p变化则p2也可能变化 Step 3 迭代（对照P70的表） p1  p2：D[p1]并入D[p2]中，若(D[p1]  D[p2]) {t}  p  p1  p2：条件{t}  p成立，则D[p1]并入D[p2]中，若(D[p1]  D[p2]) P70第2列，E[C(4)]中的函数应用引起 P70第3列，E[r(x)]中，实参是函数引起

15 第3章 控制流分析 该控制流分析的回顾 先定义规范 ，是理想解的规范 理解解的讨论：最大和最小不动点、归纳和余归纳 讨论理想解的正确性
第3章 控制流分析 该控制流分析的回顾 先定义规范 ，是理想解的规范 理解解的讨论：最大和最小不动点、归纳和余归纳 讨论理想解的正确性 再定义语法制导的规范s ，是静态分析解的规范 寻找静态分析解的办法 1、将s转变成一组约束 2、求解该组约束