（计算机科学与技术专业论文）空指针解引用静态检测方法研究.pdf

国防科学技术大学研究生院工学硕士学位论文 摘要 c 语言中的指针机制使程序员可以直接访问内存地址，具有很高的灵活性。但 是由于指针操作不当而引起的动态内存错误也有很多，空指针解引用就是其中的 一类。这些错误的存在导致了软件质量和可靠性的下降，而且采用传统的测试方 法进行检测很难奏效。 静态分析方法不需要运行程序，而是通过对程序代码的分析检查程序中隐藏 的错误。本文采用静态分析技术对c 程序中的空指针解引用错误进行检测。我们 首先基于一种流敏感、上下文敏感的指针分析算法给出了一个表达式左值的计算 方法。根据这一方法，我们可以判断任意给定的两个表达式是否为别名。 然后，结合上述流敏感、上下文敏感的别名分析，本文针对c 程序中的空指 针解引用错误给出了一种需求驱动的后向数据流分析算法。算法首先假设已知程 序中的某处发生了空指针解引用错误，然后从该结点出发，逆着控制流的方向追 踪空值的赋值过程，最终通过错误表达式集合是否为空来判断初始结点处是否发 生了错误。我们根据这一过程构造后向的数据流分析方程，最后通过不动点计算 理论计算数据流方程的解。在求解过程中，本文使用传统的w o r k l i s t 算法框架对不 动点进行迭代计算。 我们在s u i f 2 编译平台上实现了这一算法，并对一些c 程序进行了分析，实 验结果表明算法具有较高的检测精度。 主题词：空指针解引用，后向分析，指针分析，需求驱动 第i 页 国防科学技术大学研究生院工学硕士学位论文 a b s t r a c t u s i n gt h ep o i n t e rm e c h a n i s m ，cp r o g r a m sc a l ld i r e c t l ya c c e s st h em e m o r y l o c a t i o n sw h i c hm a k e sca v e r yf l e x i b l el a n g u a g e b u tt h e r ea r em a n yd y n a m i cm e m o r y e r r o r st h a ta r i s ef r o mw r o n gp o i n t e ro p e r a t i o n ，s u c ha sn u l lp o i n t e rd e r e f e r e n c e t h e s e d y n a m i ce r r o r sd e b a s et h eq u a l i t yo ft h es o f t w a r e i ti sd i f f i c u l tt of i n dt h e s ee r r o r sv i a t r a d i t i o n a lm e t h o d s t h es t a t i ca n a l y s i sf i n d sb u g sv i aa n a l y z i n gt h ec o d eo ft h ep r o g r a mw i t h o u t r u n n i n gi t i nt h i sp a p e r , w et r yt od e t e c tt h en u l ld e r e f e r e n c ee r r o r sb yu s i n gt e c h n i q u e s o fs t a t i ca n a l y s i s w ep r e s e n tam e t h o dt oc o m p u t et h el - v a l u eo fa p o i n t e re x p r e s s i o n w h i c hi sb a s e do n af l o w a n dc o n t e x t s e n s i t i v ep o i n t e ra n a l y s i s w i t ht h i sm e t h o d w e c a nc h e c ki ft h eg i v e nt w op o i n t e re x p r e s s i o n sa r ea l i a s c o m b i n e dw i t hf l o w - a n dc o n t e x t - s e n s i t i v ea l i a s a n a l y s i s ，w ep r e s e n t a d e m a n d - d r i v e nb a c k w a r d sd a t a f l o wa n a l y s i sf o rd e t e c t i n gn u l lp o i n t e rd e r e f e r e n c e si nc p r o g r a m s i tf i r s t l yg e t st h ea l i a si n f o r m a t i o nf r o mt h ep o i n t e ra n a l y s i s ，a n dt h e nm a k e s ab a c k w a r d sd a t a f l o wa n a l y s i st ot r a c kt h eo r i g i no ft h ev a l u eo fi n t e r e s t t h i sp r o c e s s c a nb ef o r m e da sad a t af l o we q u a t i o ns y s t e m f i n a l l yw eg e tt h es o l u t i o no ft h i s e q u a t i o ns y s t e mb yc o m p u t i n gi t sf i xp o i n t w h e nc o m p u t i n gt h ef i xp o i n t ，w eu s ea v a r i a n to ft h et r a d i t i o n a lw o r k l i s ta l g o r i t h m w eh a v ei m p l e m e n t e do u ra l g o r i t h mi ns u i f 2c o m p i l e ri n f r a s t r u c t u r ea n d a n a l y z e ds o m ecp r o g r a m s e x p e r i m e n t a lr e s u l t ss h o wt h a to u ra l g o r i t h mh a sah i g h p r e c i s i o n k e yw o r d s ：n u l lp o i n t e rd e r e f e r e n c e ，b a c k w a r d sa n a l y s i s ，p o i n t e ra n a l y s i s ， d e m a n d d r i v e n 第i i 页 国防科学技术大学研究生院工学硕士学位论文 表目录 表4 1 与空指针解引用属性相关的代码形式3 2 表4 2 检测效率测试：4 2 表4 3 检测精度测试4 2 第1 u 页 国防科学技术大学研究生院工学硕士学位论文 图目录 图1 1 空指针引用错误示例2 图1 2 动态内存故障模型3 图1 3 研究框架示意图7 图2 1 一段代码及其i c f g 9 图2 2 过程调用示例1 0 图2 3 数据流分析示例1 3 图2 - 4w o r k l i s t 算法框架1 4 图3 1 指针别名对分析的影响1 6 图3 2s t o r eb a s e d 表示方法示例。17 图3 3 流不敏感的分析结果18 图3 4 调用上下文比较代码示例19 图3 5 一段代码及在不同语句处的指向图。2 2 图3 - 6 静态分析工具的系统流程图2 5 图3 7 相同变量名的代码示例。2 5 图3 8 符号处理算法。2 6 图3 - 9 表达式左值计算算法。2 8 图4 1 一个空指针分析示例2 9 图4 2 类型状态规约自动机3 0 图4 3 类型状态规约逆自动机3l 图4 - 4 简单的指针语言规约3 2 图4 5 结点与函数的映射3 3 图4 - 6 数据流方程3 5 图4 7 总结函数计算示例3 6 图4 8 循环结构的数据流事实计算3 7 图4 9 更新函数的定义3 8 图4 1 0 包含f 条语句的基本块3 9 图4 1 1 空指针解引用的w o r k l i s t 算法4 0 图4 1 2 一段代码及两种算法的分析结果比较4 3 第页 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得的研 究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已 经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它教育机构的学 位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文 中作了明确的说明并表示谢意。 学位论文题目：空指鱼蟹曼f 旦登奎捡型左洼盟窀 学位论文作者签名：幺聿名舡 日期：扫堪年2 月砷日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定。本人授权国 防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子文档，允 许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据库进行检索， 可以采用影印、缩印或扫描等复制手段保存，汇编学位论文 ( 保密学位论文在解密后适用本授权书。) 学位论文题目： 空指钍缝曼l 周登查拴型友洼盈壅 学位论文作者签名： 作者指导教师签名： 日期：硼p 年2b 夸日 日期：。跏鲁年i 二月砷日 国防科学技术大学研究生院工学硕士学位论文 第一章绪论 计算机软件是人类创造的复杂的逻辑实体。随着科学技术的进步，需求的不 断增多，计算机软件也在飞速发展，其规模和数量都呈现出明显的上升趋势。与 此同时，人们对软件的质量也提出了更高的要求。如何提高软件的可靠性被人们 广为关注。 c 和c + + 语言中采用的指针机制使得编程人员可以自由访问和支配内存单元， 具有很高的灵活性，为程序设计提供了方便，也提高了程序的执行效率【l j 。但是动 态内存的手动管理也给程序带来了安全隐患，如空指针解引用错误就是动态内存 错误的一类。而且传统的测试方法对这些动态内存错误的检测往往难以奏效。本 文主要研究如何利用静态分析的方法检查c 程序中的空指针解引用错误。我们在 系统研究和比较当前的数据流分析算法和指针分析算法的基础上，结合指针分析 ( p o i n t e ra n a l y s i s ) 和后向数据流分析( b a c k w a r d sd a t a f l o wa n a l y s i s ) 给出了一种需求 驱动的空指针解引用检测方法，并在s u i f 2 平台上实现了这一算法。 1 1 研究背景 随着科技的发展，信息化程度的提高，计算机被应用到社会中的各行各业， 作为其灵魂的计算机软件也越来越发挥着更加重要的作用，成为日常生活和工业 生产中不可或缺的一部分。早期的软件规模较小，功能也相对简单，承担的通常 都是工程中的非核心任务。但是随着需求的增多，软件承担的任务也越来越重， 规模和复杂度不断提升。目前，计算机软件已被广泛地应用于航天、航空、工业 控制、金融、医疗、交通等领域。在这些特殊领域，软件的构造相当复杂，一旦 发生错误往往会造成巨大的损失，危及人员生命。因此这些软件被称为安全攸关 软件( s a f e t y c r i t i c a ls o f t w a r e ) t 2 】【3 】【4 1 。由于软件的规模增大，复杂度提高，软件产生 错误的几率也随之升高。据统计，即使经过编译和测试的程序每千行代码仍包含 l o 到2 0 个错误【5 】。在软件的开发应用中，软件测试的所占成本的比例在逐渐增大。 例如微软的开发人员和测试人员的比例达到1 ：1 。而且，即使投入如此大量的精力， 在软件投入使用之后依然不时有错误发生。如何提高软件的可靠性已成为一个亟 待解决的问题。 c 语言是被人们广泛使用的一种灵活高效的编程语言。它之所以高效，很重要 的原因是采用了指针机制，能够对物理内存进行直接地操作。目前人们使用的很 第1 页 国防科学技术大学研究生院工学硕士学位论文 多软件都是采用c 语言编写的，尤其是系统级的软件和一些软件中的关键构件， 这是因为此类软件通常需要较高的运行效率。非但如此，这些软件还必须具备另 一个重要的特性可靠性。 c 语言中采用的指针机制给程序带来了很高的执行效率，但是由于动态内存管 理的“手工性，导致c 程序中普遍存在动态内存错误。c 语言中的内存错误主要 有内存泄漏( m e m o r yl e a k ) 、内存的重复释放、空指针解引用( n u l l p o i n t e r d e r e f e r e n c e ) 等【6 】【7 】嗍。这些错误的存在会导致系统的失效甚至崩溃，从而降低了程 序的可靠性。而且指针操作错误对程序的影响常常是致命的，很容易导致执行中 的程序崩溃。所谓空指针解引用州u l lp o i n t e rd e r e f e r e n c e ) 是指对一个指向空地址单 元的指针表达式进行解引用操作( d e r e f e r e n c e ) 而引起的错误。一个空指针解引用的 例子如图1 1 所示：语句3 执行后指针变元p 驴的值为空，语句4 再对p 护进行解 引用，此时便产生了空指针解引用错误。 1i n t m a i n 2 i n t 木p t r ； 3 p t r = n u l l ； 4 p t r = 5 ； 5r e t u r n0 ； 6 ) 图l 一1 空指针引用错误不例 t o d dm a u s t i n 等人研究表明，c 程序中5 0 的软件故障与动态内存的分配管 理有关【6 】。虽然内存错误在c 程序中普遍存在，但是传统的黑盒、白盒测试很难 发现这些错误。特别对于空指针解引用错误，采用动态的方法很难检测，因为一 旦发生此类错误就会导致程序崩溃，动态方法难以跟踪。因此，对c 程序中的空 指针解引用检测进行研究是一项重要和有意义的工作。 1 2 研究现状 1 2 1 空指针解引用故障模型分析 空指针解引用错误是c 程序中动态内存错误的一种，是由于动态内存手动管 理不善而引起的。c 程序中的动态内存是一个自由的存储区域，编程人员可以根据 需要，对这块内存进行手动的管理，如分配、释放( 回收) 、访问等，如果在这些过 第2 页 国防科学技术大学研究生院工学硕士学位论文 程中出现差错，就会发生动态内存错误。文 9 】对动态内存错误进行了研究，对产 生动态内存错误的各个阶段进行了分析，在此基础上提出了动态内存错误的故障 模型，如图1 2 所示。图中的连线表示在这一过程产生了动态内存错误，箭尾表示 当前内存状态，箭头表示请求的操作。我们将与空指针相关的基本谓词做如下的 定义： a l l o c a t e ( p ) ：为指针p 分配堆地址内存： p o i n t ( p ，h e a p ) ：指针p 指向堆地址h e a p ； f r e e ( p ) ：释放指针p 指向的内存； c h e c k ( p ) ：检查指针p 指向的内存是否非空； a c c e s s ( p ) 访问指针p 。 图1 2 动态内存故障模型 图中的连线3 和9 表示了空指针解引用错误的产生过程。连线3 表示在对动 态内存访问之前没有对内存分配情况进行检测，这时访问的内存可能为n u l l ；过 程9 则表示对已经被释放了的动态内存单元进行访问。这两种不合法操作都造成 了空指针解引用错误。根据图中状态变化，空指针解引用错误的语义描述如下： v p ( ( b a l l o c a t e ( p ) 人- - , c h e c kaa c c e s s ( p ) v ( b a l l o c a t e ( p ) f r e e ( p ) a c c e s s ( p ) ) ) jn u l lp o i n t e r d e r e f e r e n c e 这一定义主要考虑了动态内存的状态迁移过程，在本文的工作中，我们更关 心的是一个指针表达式或指针变元的值的变化。从值的变化的角度出发我们将空 指针解引用的语义描述为： v p ( p o i n t ( p ，n u l l ) a c c e s s ( p ) ) n u l lp o i n t e rd e r e f e r e n c e 即，对值为空的指针表达式或指针变元进行访问所产生的错误称为空指针解引用。 第3 页 国防科学技术大学研究生院工学硕士学位论文 1 2 2 动态内存错误检测方法 在软件开发周期中，错误检查( e r r o r d e t e c t i o n ) 是最消耗时间的一个步骤。考察 软件排错的技术和工具的依据主要有四个方面l lo j ： 错误覆盖率：即检测工具和方法可以覆盖多少程序的执行路径和数据值等。 自动化程度：即在检查过程中是否需要手工操作及其手工参与的程度。 检测精度：检查结果是否精确，误报率的是否控制在可接受的范围内。 检查的规模：即可检查程序的规模，可检查的最大代码行数。 常用的错误检测技术有动态检测、模型检验、定理证明和静态分析等。 传统的软件测试技术即动态检测方法，需要运行所检查的程序，通过输入和 输出观察是否产生错误，因此它的测试结果是与测试输入的质量相关的。动态检 测具有精确的检测结果，且能检测规模很大的程序。但是动态检测覆盖率较低， 随着程序规模的增大，覆盖率呈降低的趋势。p u r i f y 是一个动态的内存单元测试工 具，它通过在程序中加入代码动态地监测程序的运行状态i l 。p u r i f y 主要用于测试 程序中的内存泄漏错误，对于其他的动态内存错误如空指针解引用等则无能为力。 作为一种动态的测试工具，p u r i f y 必须在程序运行起来以后对程序进行检测。对于 大规模的软件，由于大量分支的存在，动态测试工具很难覆盖到程序中的所有路 径，这便产生了漏报。因此，对于动态测试工具，错误检测的漏报是一个难以解 决的问题，从理论上来说，动态测试必然存在漏报。对于空指针解引用错误，动 态检测方法更难以适用，因为一旦发生空指针解引用错误程序就会崩溃，采用动 态方法难以跟踪。 模型检验( m o d e lc h e c k i n g ) t 1 2 】是一种完全自动化的形式化验证技术，其基本思 想是对系统行为的状态空间构造有穷模型，然后通过遍历验证模型的某些性质。 模型检验的优点是自动化程度很高，如果检验的性质不成立可以给出反例。但是 模型检验常常要面临状态空间爆炸的难题，兼顾精度和检验规模是一项困难的事 情。有一些模型检验的工具如s p i n i l 3 】等是面向代码的，能够自动从代码中抽取模 型进行验证，但是验证的规模较小；s l a m l l 4 】等检验工具基于抽取的模型进行检验， 改进了检验的规模，但是损失了精度。要想对模型进行细化以重新获得精度又会 遇到规模上的限制。 定理证明技术将软件性质规约为逻辑公式，然后依据形式系统中的公理和推 理规则，采用类似数学中的定理证明方法来证明软件系统是否具有期望的性质【1 5 1 。 例如对于一组合取公式p l = q 1 a a p m = a m a r l 搿l a a 凡确，需要首先根 据该合式公式构造一个图，图中的每个结点表示合取式中的一个条件。然后将等 式条件的两边进行合并，合并过程中检查是否所有的不等式条件成立，如果不成 第4 页 国防科学技术大学研究生院工学硕士学位论文 立则认为该合取式是不可满足的。定理证明的优点是可以基于无穷域上的归纳法 处理无穷状态空间，有一些定理证明工具能够支持代码的自动生成。缺点是自动 化程度不高，证明过程需要人工干预，不能在证明失败后给出易于理解的反例。 静态检测方法通过对程序代码的分析检查程序中隐藏的错误，它不需要运行 程序。采用静态分析方法检测程序中的动态内存错误是目前软件工程中的热点之 一。常用的方法主要有以下几种： 1 类型推导 类型推导是指由机器自动地推导出程序中变量和函数的类型【16 】【1 7 】【1 8 】。程序中 的数据可以按照一定的规则划分为不同的集合，把一个集合作为一种数据类型， 然后利用类型理论中的算法进行计算。一个程序可以看作一个有向图，图中的结 点为包含了变量值的集合，结点间的有向边则记录了变量值变化时的数据流信息。 类型推导具有良好的可扩展性，能够处理大规模的程序，但是不适用于控制流相 关的分析。在处理控制流相关的信息时，需要引入子类型( s u b t y p i n g ) 的概念。 2 抽象解释 抽象解释( a b s t r a c ti n t e r p r e t a t i o n ) 【1 9 】【2 0 】首先是由p c o u s o t 和r c o u s o t 于19 7 7 年提出的用于构造和逼近程序不动点的理论。程序语言描述了所有用该语言编写 的程序的语义，程序语义则描述了对象域上的计算过程和结果。如果一个程序的 语义可以由函数f 描述，则我们可以通过求解不动点方程释r 的来研究程序的性 质。抽象解释的本质是在计算效率和计算精度之间进行权衡，通过损失计算精度 取得计算的可行性，再通过迭代提高计算的精度【2 1 1 。 当找到合适的方法对程序具体域进行抽象以后，得到的抽象域的规模大大减 小，达到可以计算的范围。再通过计算找到抽象的不动点集合，并将其映射到具 体域中。这样得到的不动点集合通常要比实际的不动点集合大，是实际不动点集 合的近似。因此抽象解释的主要问题是如何针对某些性质找到合适的语义函数， 计算得到抽象的不动点集合，并且使得精度在可接受的范围内。 3 符号执行 符号执行( s y m b o l i ce x e c u t i o n ) 2 2 l 简单来说是一种增强的程序测试技术。但是， 符号执行不是将程序运行起来测试一组输入，而是用抽象的符号表示程序中的一 变量的值，以符号化的形式，模拟程序的执行。一个符号执行的结果可能等价于 一组通常的程序测试用例。符号执行中测试输入的分类是由程序控制流与输入的 相关性决定的。如果输入的变元与程序的控制流是完全无关的，则仅需一次符号 执行就可以检测程序所有可能执行；如果输入与控制流相关，则需要对输入进行 分析归类。 第5 页 国防科学技术大学研究生院工学硕士学位论文 符号执行常与约束求解结合使用，优点在于可以精确地静态模拟程序的执行， 可以发现程序中的细微错误。但是由于程序的执行路径会随着程序规模而成指数 级的增长，这时用符号执行进行检查时就需要选取一定数量的路径进行分析。 基于上述方法的程序静态分析工具有很多，而且这些工具大都结合了多种检 测方法。如e s p 2 3 】是一种基于规则的系统，它使用了多种策略，包括保守的别名 分析、数据流分析以及路径敏感的符号执行等。总之，静态分析中的分析精度和 分析代码的规模是互相制约的两个方面，上述静态分析技术和工具也都试图在精 度和效率之间做出权衡，以满足特定的需求。 1 3 课题研究的主要内容和框架 1 3 1 课题研究主要内容 本课题主要研究如何利用静态分析的方法检查c 程序中的一种动态内存错误 一空指针解引用。主要工作和研究内容包括： 1 研究分析当前c 程序中动态内存错误检测的常用方法和工具，比较了这些 方法和工具的优缺点。研究采用何种策略提高空指针解引用错误检测的精度和效 率。 2 在很多静态分析方法中，别名分析是一个重要的组成部分。本文研究了指 针分析和别名分析的相关理论方法，并在一种流敏感、上下文敏感的指针分析基 础上实现了一种表达式别名分析算法。 3 本文结合流敏感、上下文敏感的别名分析和后向数据流分析( b a c k w a r d sd a t a f l o wa n a l y s i s ) ，提出了一种需求驱动( d e m a n d d r i v e n ) 的c 程序空指针解引用检测 方法。该方法从错误的源头出发，逆着控制流的方向做错误表达式集的推导，最 终通过错误集是否为空来判断该处是否产生了错误。推导过程中需要查询别名分 析数据库，这使用到了我们前面实现的别名分析方法。 4 我们在s u i f 2 ( s t a n f o r du n i v e r s i t yi n t e r m e d i a t ef o r m a t ) 平台上实现了这一空 指针解引用错误检测算法，并应用该算法对一些c 程序进行了分析。实验结果表 明我们的算法具有较高的检测精度。 1 3 2 研究框架 图1 3 描述了本文所提出的算法的基本框架和流程。首先用户将程序源码输入 到s u i f 编译平台，经s u i f 平台编译后生成s p d 后缀文件，s p d 是s u i f l 中的中 第6 页 国防科学技术大学研究生院工学硕士学位论文 间表示形式，由于后面使用的s p a n 算法只能处理s p d 文件，因此需要先转换成 s p d 格式；然后使用s p a n 算法对程序进行指针分析，生成s p a n 后缀文件，s p a n 文件中包含了指针分析的结果，并以指向图的形式表示；再将s p a n 文件转化为s u i f 文件。最后，使用本文提出的空指针解引用错误检测算法对得到的s u i f 文件进行 空指针解引用错误分析，在这个过程中需要经常用到别名分析，这就需要与别名 分析模块进行数据交互。图中的别名分析模块和n d a l g 算法模块是本课题的主要 工作，本文在后续的章节中会详细地叙述。框架中的s p a n 2 4 】算法是由r u g i n a 等人 提出的一种流敏感、上下文敏感的指针分析算法，它可以在程序的每条语句处生 成一个指针指向图。 输入 翌h 、竿 输入i 匈( 攀h 辈兰 程序源码i 析数据 ri “”“ 一查询返孑 生成i 告 1 4 本文的组织结构 本文的章节安排和每章的主要内容如下： 第一章为绪论，主要阐述本课题研究的背景和研究意义，简述当前流行的各 种动态内存错误检测方法及现有的工具等，并指明本课题的主要工作和研究内容。 第二章为空指针解引用错误检测的背景知识，介绍一些基本的概念、原理和 方法，如程序的控制流分析和数据流分析等，并对各种方法的优缺点进行分析比 较。 第7 页 国防科学技术大学研究生院r t 学硕士学位论文 第三章研究了指针分析和别名分析的相关内容，并在一种流敏感、上下文敏 感的指针分析基础上给出了一种判断表达式别名的方法。 第四章结合别名分析和后向数据流分析给出了一种需求驱动的空指针解引用 错误静态分析方法，应用这一方法对一些程序进行了检测，对该方法的检测效率 和精度等进行了比较分析。 最后为结束语，总结了本文的工作，提出需要改进和进一步完善的部分，对 以后的工作做了展望。 第8 页 国防科学技术大学研究生院工学硕士学位论文 第二章空指针解引用检测相关研究 本章主要介绍空指针解引用错误静态检测的相关知识，本文在前面已经说明 空指针解引用错误是动态内存错误的一种，因此空指针解引用错误的检测方法是 动态内存错误分析方法的子集。本章主要内容包括控制流分析、数据流分析等， 阐述与本文的研究相关的基本术语、原理和算法，对这些算法进行分析和比较， 指明本文提出的算法之所以采用这些策略的缘由。 2 1 程序静态分析概述 程序的静态分析是指不需要运行程序，而是通过编译时的静态分析达成优化 程序结构、排除隐藏错误的技术。程序分析实质上是基于程序语义的分析，其正 确性可以根据程序的某种语义得到证明。 2 1 1 程序控制流分析术语 图2 - 1 一段代码及其i c f g 控制流反映了程序的执行顺序，是研究程序性质的重要手段。程序中的过程 可以表示为一个控制流图( c o i l 仃o lf l o wg r a p h ) 。控制流图表示了一个过程内所有基 本块执行的可能流向和每个基本块所对应的语句表。一个过程p 内的控制流图g 第9 页 国防科学技术大学研究生院工学硕士学位论文 可以是一个四元组仁 i l ，i 2 。依据过程