中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
基于变量关系图和符号执行的指针相关路径分析
作者: 杨宇
答辩日期: 2003
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 静态测试 ; 指针 ; 形式规约
其他题名: Static Analysis of Pointer-related Path with Variable Relationship Graph and Symbolic Execution
摘要: 软件测试是保证软件质量的必要手段。由于基于用例运行程序进行测试低效且容易出错,人们从六十年代起就开始探索用例测试之外的其它软件质量保证手段。程序验证尝试以严格的定理证明方式确保程序正确。然而由于程序设计语言的复杂性,程序验证只用于证明一些关键的核心模块的正确性,而没有得到更广泛的应用。程序静态测试是介于程序验证和基于用例的测试之间的方法。静态测试不编译运行程序,仅依据规约或者规则对源码进行分析以检测程序中是否存在错误。静态测试不能证明程序的完全正确,但是可以作为动态测试的补充。目前关于程序静态分析的研究是软件工程研究的一个热点。对程序进行静态测试,首先需要分析理解程序的行为。指针变量和存储模型紧密相关,不能简单地作为数值型变量予以处理。分析包含指针变量的程序一直是静态测试中需要解决的一个难题。本文提出的变量关系图这一抽象模型,一方面用于抽象地描述了程序的存储结构,另一方面也描述变量间的约束关系。和其它己经提出的抽象模型相比,变量关系图能够更深刻地揭示程序中变量间的约束关系。针对包含指针以及结构类型变量的程序路径,我们提出了以变量关系图为基础,结合符号执行对其进行分析的方法。在符号执行中根据程序动作调整变量关系图的结构,同时根据程序中的条件生成相应的约束条件集合。通过考察符号执行中生成的变量关系图,可以检测程序中悬空指针引用、存储泄漏以及变量未初始化等具有一般性的错误。此外,通过对符号执行后求得的约束集合进行求解,我们还可以检查和具体程序相关的错误。具体实现方面,在己有的路径分析工具RAT的基础上进行了扩展,使之能够处理包含指针类型和结构类型变量。利用变量关系图和符号执行,我们可以精确地获取程序的存储模型及变量间约束关系的信息,可以发现一些已有的分析工具不能发现的错误。此外,我们设计一个小的规约语言并实现相应的翻译工具,使得能够较为简洁地描述程序的规约。
英文摘要: Software testing is an essential method for guaranteeing the quality of software. Since running test cases is error-prone and inefficient, people have been exploring new approaches to software quality assurance since 1960's. Program verification tries to prove correctness of programs with strict theorem proving. However, because of the complexity of programming languages, program verification's usage is rather limited. Static program testing is an approach between program verification and test case running. Instead of compiling and running the programs in case-based testing, static testing check programs against specifications and rules so as to pick bugs out. Although static testing cannot reveal all the bugs, it can be a very helpful supplement for runtime testing. Performing static testing, the first thing we should do is to understand programs' behavior. Since pointer variables have a strong tie with memory models, they cannot simply be treated as numeric variables. How to analyze programs that contain pointers is a hard problem in static testing. The thesis proposes a new abstract model, called variable relationship graph (VRG), to depict variables' relationship in the programs. Compared with other memory models that have been proposed, VRG can extract more information from the program and is more suitable for static analysis. To evaluate a program path that contains pointer variables, the thesis explores the methods of how to evaluate paths that contains pointers and structure variables. We statically simulate the execution of program paths with variable relationship graph and symbolic execution. During this process, VRG is adjusted according to action of programs. Constraint sets are generated at the same time. A constraint solver will be used to test the satisfiability of constraint sets. With this method, common errors like dangling pointers, memory leak and uninitialized variables, can be detected. In addition, more specific errors can be detected if programs are checked against specifications. As for the implementation, we extended PAT, a path analysis tool. With the help of variable relationship graph, the improved version can deal with pointer variables and user-defined structure variables. Some program errors that cannot be detected with other static analysis tools can be detected with our tool. Finally, a small specification language is designed and a translator is implemented to help the user write more concise specifications.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/5880
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW011231.pdf(2714KB)----限制开放-- 联系获取全文

Recommended Citation:
杨宇. 基于变量关系图和符号执行的指针相关路径分析[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2003-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[杨宇]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[杨宇]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace