-
题名基于指向与数值抽象的带指针算术程序的分析方法
被引量:2
- 1
-
-
作者
尹帮虎
陈立前
王戟
-
机构
国防科学技术大学计算机学院并行与分布处理国防科技重点实验室
-
出处
《计算机科学》
CSCD
北大核心
2015年第7期32-37,共6页
-
基金
国家自然科学基金(61202120
91118007)
教育部博士点基金(20124307120034)资助
-
文摘
带指针算术的程序往往包含数组越界、缓冲区溢出等运行时错误。单纯的指针分析技术和数值分析技术都无法有效处理指针算术。为了将指针分析与数值分析相结合,首先提出一种新的指针内存模型,然后基于该模型设计了一个刻画指针指向关系和指针偏移量的抽象域。最后在抽象解释框架下,设计并实现了一个面向带指针算术C程序的静态分析工具原型PAA。实验结果表明,PAA能够有效地分析指针程序的指向关系和数值性质,并能够在效率和精度间取得合理的权衡。
-
关键词
静态分析
抽象解释
指向分析
数值抽象域
-
Keywords
Static analysis
Interpretation
Points-to analysis
Numerical abstract domain
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名一个面向C和Fortran数值程序的静态分析工具
被引量:1
- 2
-
-
作者
侯苏宁
陈立前
王昭飞
王戟
-
机构
并行与分布处理国防科技重点实验室
-
出处
《计算机工程与科学》
CSCD
北大核心
2011年第3期94-102,共9页
-
基金
国家自然科学基金资助项目(90818024
60803042)
-
文摘
程序的正确性验证一直以来都是计算机科学中的一个挑战性问题,抽象解释理论为程序静态分析提供了一个通用框架,可以在编译时自动地推导程序的动态性质。基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系,这对于编译优化、程序错误检查至关重要。本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具,C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式,然后基于该中间表示抽取与源程序语义等价的语义等式,最后在该语义等式上进行不动点迭代计算从而得到程序不变式。在此基础上,本文还对数组等复杂语法结构进行了建模和抽象。实验结果表明,该工具具有较高的可扩展性、精度,并能够处理大部分因数组的使用而带来的程序分析上的问题。
-
关键词
静态分析
抽象解释
值范围分析
数值抽象域
数组抽象
-
Keywords
static analysis
abstract interpretation
value range analysis
numeric abstract domain array abstraction
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-