论文部分内容阅读
计算机软件在当今社会中发挥着越来越重要的作用。无论是在人们的日常生活中,还是在一些关键系统中——例如银行系统,飞行控制器和医疗系统——都大量地使用软件。软件运行的正确与否影响到人们的正常生活,软件的失效甚至会引发巨大的损失。作为一种重要的编程语言,C语言至今仍被大量应用于开发各种系统软件与应用软件。同其它一些语言一样,C显式地支持指针操作以及动态内存的处理,这大大地提高了语言的表达能力。但是,使用带指针的语言编程是一项容易出错的工作,有可能产生大量的内存错误。又因为有些这样的错误不易重现,难以查找诱发错误的原因,所以内存错误通常很难检测。静态检查(static checking)技术是检测软件错误的一种重要技术。它通过直接分析源代码来发现程序中的错误,而不需要实际运行。由于其具有覆盖率较高、能够在早期发现错误和易于使用的优点,因而被大量地应用于软件查错中。本文主要研究如何利用静态检查技术来查找C程序中的内存错误,并在SUIF2编译平台下实现了相应的算法。形态分析(shape analysis)是分析带有指针和动态内存分配程序之内存特性的一种重要技术,它通过静态检查技术来获取程序所分配的堆中的数据结构信息,其结果有助于对程序的理解和验证。本文提出了一种新的形态分析技术,能够处理C语言中复杂的表达式,支持对于结构域和栈变量的取址操作。从一个表达式出发,我们定义了它的抽象赋值路径(Abstract Evaluation Path, AEP),抽象赋值路径被用来对抽象形态图(Abstract Shape Graph, ASG)进行精化,从而定义语句的语义。形态分析的结果可以用来决定程序的“形态不变量”、检测内存泄漏错误、获取别名信息以及程序中内存结构的形态等。内存泄漏是C程序中一种常见的错误,它有可能耗尽系统内存,从而导致程序崩溃。基于C程序的一种流敏感、上下文敏感的指针分析方法,本文提出了一个需求驱动(demand-driven)的内存泄漏检测算法。该算法首先假设程序中的某一语句引发了内存泄漏,由此假设出发,可以得到一些初始信息,然后进行后向分析,来判断这个假设是否成立。通过指针分析,可以得到指向图(points-to graph),基于这样的指向图,计算出数据流事实(data flow fact),从而判断是否有内存泄漏发生。另一类重要的内存错误是空指针解引用(null pointer dereference)错误。访问空指针是危险的操作,有可能产生不可预见的错误,导致程序崩溃。本文提出了一种检测空指针解引用错误的算法,它利用了必然别名(must alias)和可能别名(may alias)信息来提高检测算法的精度。从一个不精确的流不敏感、上下文不敏感指针分析算法出发,我们计算出赋值语句所产生的必然别名信息。使用必然别名信息,可以提高可能别名的精度,还能够在赋值语句处更新更多的表达式,降低空指针解引用检测算法的误报率。SUIF2是一个研发编译技术的平台,支持C、C++、Fortran和Java等语言。C程序代码被编译成SUIF(Stanford University Intermediate Format)格式。它提供了模块化的环境,可以容易地开发能相互交互的遍(pass)。在SUIF2平台下,我们实现了本文中的算法,分别开发了C程序的形态分析工具,内存泄漏检测工具以及空指针解引用检测工具,并取得了预期的实验结果。