第十讲 基于格理论的数据流分析.

Slides:



Advertisements
Similar presentations
版 画 制 作版 画 制 作 版 画 种 类版 画 种 类 版 画 作 品版 画 作 品 刘承川.
Advertisements

2.5 微分及其应用. 三、可微的条件 一、问题的提出 二、微分的定义 六、微分的形式不变性 四、微分的几何意义 五、微分的求法 八、小结 七、微分在近似计算中的应用.
人的性别遗传 合肥市第四十九中学 丁 艳. 男女成对染色体排序图 1 、男性和女性各 23 对染色体有何异同 ? 哪 一对被称为性染色体 ? 2 、这两幅图中,哪幅 图显示的是男性的染色 体?哪幅图显示的是女 性染色体? 3 、图中哪条染色体是 Y 染色体?它与 X 染色体 在形态上的主要区别是.
XX啤酒营销及广告策略.
专题培训 企业所得税汇算清缴 (2015年度).
第四章:长期股权投资 长期股权投资效果 1、控制:50%以上 有权决定对方财务和经营.
1、一般地说,在生物的体细胞中, 和 都是成对存在的。
辨性别 A B. 辨性别 A B 第三节人类染色体与性别决定 昌邑市龙池初中 杨伟红 学习目标 1.理解人的染色体组成和传递规律。 2.解释人类性别决定的原理。 3.通过探究活动,解读数据了解生男生女的比例。
性别决定与伴性遗传 性别决定 伴性遗传 巩固练习.
97年度推展精進教師課堂教學能力計畫 基測命題趨勢分析與改進教學實務 五權國中謝惠萍.
第八讲 静态代码质量分析技术.
第十二章 小组评估 本章重点问题: 评估的设计 测量工具的选择和资料的收集 与分析.
二次函數 高士欽 林國源.
高考地理复习应注意的问题 构建知识网络 培养读图技能 掌握答题规律.
《老年人权益保障》 --以婚姻法.继承法为视角
十二年國民基本教育 年度中投區免試入學 超額比序與志願選填宣導說明
巧用叠词,妙趣横生.
*線性代數* Chapter.2 線性方程組.
欢迎大家来到生命科学课堂.
初中语文总复习 说明文 阅读专题 西安市第六十七中学 潘敏.
自考英语二.
胚胎学总论 (I) 制作:皖南医学院组胚教研室.
清仓处理 跳楼价 满200返160 5折酬宾.
研究方向: 多媒体环境下课堂教学模式研究.
第六章 中间代码生成 赵建华 南京大学计算机系.
致亲爱的同学们 天空的幸福是穿一身蓝 森林的幸福是披一身绿 阳光的幸福是如钻石般耀眼 老师的幸福是因为认识了你们 愿你们努力进取,永不言败.
命题的四种形式 高二数学.
1.1.2 四 种 命 题.
增值评价 2014级 初中起点报告 解读培训 辽宁省基础教育质量监测与评价中心.
培训教案 公司审计部
色 弱 與 色 盲.
遺傳 龍生龍,鳳生鳳 老鼠的兒子會打洞.
第五章 定积分及其应用.
高中数学知识网络 2017年9月9日星期六.
第四节 统计初步和数据整理 在这一节中我们将介绍统计学的基本知识。统计学是一门古老而又年轻的学科,例如为了征兵和收税的早期的人口统计,甚至在公元前就出现了。但是近代数理统计学,却主要是从20世纪初开始发展的。其主要特征是运用概率论的知识进行统计推断。即从所研究的全部对象中抽取部分个体,并通过对这部分个体的观察和分析,对全部对象的有关问题作出推断。数理统计学已经建立了一套系统的理论,有着广泛的应用。下面先介绍统计学中最基本的概念。
宠物之家 我的宠物性别? 雌(♀) or 雄(♂) 第一阶段:我的宠物我做主 第二阶段:宠物“相亲记” 第三阶段:家族诞生
第20章 生物的遗传和变异 第四节 性别和性别决定 淮南二十六中 鲍娟娟. 第20章 生物的遗传和变异 第四节 性别和性别决定 淮南二十六中 鲍娟娟.
课标教材下教研工作的 实践与思考 山东临沂市教育科学研究中心 郭允远.
北师大版七年级数学 5.5 应用一元一次方程 ——“希望工程”义演 枣庄市第三十四中学 曹馨.
第一眼印象 —— 一个高端项目. 第一眼印象 —— 一个高端项目 后来,我们在荔湖城又转了转……
海洋存亡 匹夫有责 ——让我们都来做环保小卫士 XX小学三(3)班.
XX信托 ·天鑫 9号集合资金信托计划 扬州广陵
第8章 回归分析 本章教学目标: 了解回归分析在经济与管理中的广泛应用; 掌握回归分析的基本概念、基本原理及其分析应用的基本步骤;
选课网址:(必须用谷歌浏览器) 选课时间:星期天上午10点之后
劳动关系 第十二讲 主讲教师:于米          学时:32.
你一定要認識的數學家.
第四章 语法分析.
第2次课 上下文无关文法
電腦解題─流程圖簡介 臺北市立大同高中 蔡志敏老師.
第12章 shell编程基础 本章主要介绍shell编程的基础知识。shell脚本的执行类似于Linux下的任何其他命令,脚本可以包含复杂的逻辑,也可以包含一系列Linux命令行指令。在一个shell程序内可以运行其他shell脚本。通过本章的学习,读者可以学到如何使用bash(最流行的Linux.
中间代码生成.
导数的应用 ——函数的单调性与极值.
二元一次聯立方程式 代入消去法 加減消去法 自我評量.
第六章 语法制导的翻译 本章内容 介绍一种语义描述方法:语法制导的翻译,介绍语法制导的翻译的实现方法。
第七章  事业单位支出的核算      §第一节  支出概述     §第二节  拨出款项     §第三节  各项支出     §第四节  成本费用.
软件测试技术-白盒测试 张志强 2006.
7.4解一元一次不等式(1).
第7章 回归分析.
课前注意 课前注意 大家好!欢迎加入0118班! 请注意以下几点: 1.服务:卡顿、听不清声音、看不见ppt—管家( ) 2.课堂秩序:公共课堂,勿谈与课堂无关或消极的话题。 3.答疑:上课听讲,课后答疑,微信留言。 4.联系方式:提示老师手机/微信: QQ:
分 解 因 式 保定市第二十六中学 刘彦莉.
导数的几何意义及其应用 滨海中学  张乐.
两个变量的线性相关 琼海市嘉积中学 梅小青.
基本不等式.
第1章 数据结构基础概论 本章主要介绍以下内容 数据结构研究的主要内容 数据结构中涉及的基本概念 算法的概念、描述方法以及评价标准.
合情推理与演绎推理 ----类比推理.
线性回归.
第八章 服務部門成本分攤.
1.8 完全平方公式(一) 锦州市实验学校 数学组(3).
第六章 程序设计初步 一、程序设计的基本方法.
第二章 一元一次不等式和一元一次不等式组 回顾与复习(一).
Presentation transcript:

第十讲 基于格理论的数据流分析

内 容 一、控制流图 二、活性分析 三、可用表达式 四、很忙表达式 五、可达定义 六、初始化变量 七、符号分析 八、常量分析 九、区间分析

一、控制流图 (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,∞]]