一类范围约束的浮点数静态分析方法

论文摘要

抽象解释理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近程序的不动点理论。它的一个重要应用是分析程序中的变量或约束表达式的值域。这些值域信息有助于进行数组和循环的界限分析,基于数组的数据依赖性分析,指针分析,循环时间分析,可执行路径分析等。抽象解释理论的特点是可靠但不完备的,即：如果验证结果表明抽象系统满足验证性质,则抽象解释理论保证原系统也满足验证性质；若验证结果表明抽象系统不满足验证性质,则原系统可能满足验证性质,可能不满足验证性质,需要更精细的抽象分析。而一个精确的抽象域能够减少这种不完备性,有利于提高验证效率。因此,设计一个精确的抽象域及定义抽象域上抽象运算是抽象解释理论研究的核心内容。本文利用抽象解释理论对浮点数表达式约束问题的值域进行了估测,主要的目标改善不完备性。其主要工作如下：首先,基于IEEE 754-1985浮点数模型规范,结合抽象解释理论中的完备格的性质,本文提出了浮点数的抽象语义。然后根据区间抽象域的一些运算特性和IEEE 754-1985浮点数模型的舍入模式,定义了这种抽象域的抽象运算。其次,为均衡浮点数表达式的计算精度和计算效率,在浮点数抽象模型以及抽象运算的基础上,本文为两个变量的浮点数线性表达式约束问题建立区间约束。为区间约束建立区间约束图,在约束图的基础上,把这类浮点数约束问题转化为区间线性方程。利用上面定义的区间运算,本文给出了这类问题的解。最后,本文提出的的算法与以往的利用加宽算子或者是收缩算子方法进行比较,发现本文算法所找到的抽象域能够更准确更有效地反映可达状态集,可以简化在这个抽象域上的抽象运算,大大地减少虚假的错误报告。

论文目录

• 摘要
• Abstract
• 插图索引
• 附表索引
• 第1章 绪论
• 1.1 研究背景和意义
• 1.2 研究现状
• 1.2.1 抽象解释理论
• 1.2.2 数值抽象域
• 1.3 研究的主要目标
• 1.4 研究的主要内容
• 1.5 本文的组织结构
• 1.6 本章小结
• 第2章 抽象解释理论
• 2.1 引言
• 2.2 抽象解释理论框架
• 2.2.1 偏序关系与完备格
• 2.2.2 Galois连接与Galois嵌入
• 2.2.3 加宽运算和收窄运算
• 2.2.4 域提炼
• 2.3 抽象解释研究的主要领域
• 2.3.1 语法
• 2.3.2 语义
• 2.3.3 证明
• 2.3.4 静态分析
• 2.3.5 类型分析
• 2.3.6 谓词抽象
• 2.3.7 反例的抽象精化
• 2.3.8 程序转换
• 2.3.9 信息隐藏
• 2.3.10 恶意软件检测
• 2.3.11 程序终止
• 2.4 本章小结
• 第3章 数据抽象域
• 3.1 引言
• 3.2 抽象域的相关理论
• 3.2.1 数据域
• 3.2.2 基于抽象解释理论的数据抽象域的设计方法
• 3.3 数据抽象域
• 3.3.1 非关系型抽象域
• 3.3.2 关系型抽象域
• 3.3.3 弱关系型抽象域
• 3.4 三种类型的抽象域的比较
• 3.5 本章小结
• 第4章 浮点数抽象
• 4.1 引言
• 4.2 浮点数的具体语义
• 4.3 浮点数模型
• 4.3.1 IEEE 754-1985浮点数模型
• 4.3.2 浮点数的舍入模式和表达式
• 4.4 浮点数的抽象语义
• 4.4.1 浮点数抽象域的原理
• 4.4.2 浮点数抽象域的基础定义
• 4.4.3 浮点数抽象域运算
• 4.4.4 浮点数表达式的区间抽象及运算
• 4.5 本章小结
• 第5章 浮点数表达式的静态分析
• 5.1 引言
• 5.2 基础知识
• 5.3 约束转化
• 5.4 约束图建立
• 5.5 无环图的解法
• 5.5.1 事例
• 5.5.2 无环图的建立
• 5.5.3 解法
• 5.6 有环图的解法
• 5.6.1 事例
• 5.6.2 有环图的建立
• 5.6.3 解法
• 5.7 交有环约束图的解法
• 5.7.1 事例
• 5.7.2 交约束有环图的建立
• 5.7.3 解法
• 5.8 方法扩展
• 5.9 结果比较及分析
• 5.9.1 结果比较
• 5.9.2 结果分析
• 5.10 本章小结
• 结论
• 参考文献
• 致谢
• 附录A （攻读硕士学位期间所发表的学术论文及参与科研项目）