资源描述：
《程序静态分析技术与工具》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、计算机科学··附程序静态分析技术与工具‘杨宇张健中国科学院软件研究所计算机科学重点实验室北京,。本,摘要铮态分析对于保证程序质童提高软件生产率有重要的意义文综述了静态分析常用的策略介绍了当前,比较了。睁态分析的研究现状目前已有的静态程序分析工具,铮态关键词程序正确性分析,,段,,,,,点,也幻已经有一些产品面世本文首先介绍静态分析的主引言要方法,然后介绍目前,已经实现的几个典型系统并对它们作,。长期以来,程序正确性一直受到计算机科学界和工业界一些比较最后说明静态分析的局限以及我们的展望。的关注自世纪
2、。年代起就有很多计算机科学家对程序验,。,程序静态分析的方法和理论证进行了研究提出了各种理论和方法一般说来程序验证要求通过推理或者穷举的手段来判定程序的行为是否符合规本节简要介绍在程序静态分析工具的构建中常用的方。,约。由于要涵盖所有可能情况,而程序设计语言的复杂性使得法这些方法并不完全相互独立一个静态分析工具常常需要程序的复杂性随着程序,使用多种方法以取得最佳效果尺寸的增大呈指数级增长同时证明·任一程序,因此程序验证符号执行正确与否本身是一个不可判定问题目前只用于证明一些关键的核心模块的正确性而没
3、有得到更符号执行的基本思想是,用抽象的符号表示程序中变,广泛的应用。就目前而言,程序验证方法虽然可以保证软件质的值来模拟程序的执行该方法很好地克服了在静态侧试量,但是往往需要有一定经验的用户花费相当多的时间,因而时不能确定程序中变量的值的问题符号执行常常在对路径敏感的程序分析中使用。用符号执行加约束求解进行程序分并不一定能提高软件的生产率,另一方面,在现实的软件开发中大量的时间被用于发现析的基本思想是用逻辑可以将程序表示成,和消除软件中的错误,也就是软件测试。除了一些大公司在大其中是执行程序前需要满
4、足的条件是程序执行后孺要,型软件系统开发中使用了一些自动测试手段,在很多情况满足的条件在程序的符号执行过程中由出发结合程序,。,下,软件测试仍然停留在手工测试阶段。手工测试不仅效率很中的约束条件可以推导出新的约束条件。、⋯因。,而且容易。,、此有,⋯可以对约束条件,⋯低出错测试任务往往很繁重在资源有限时间紧。。。,迫的情况下测试任务常常不能充分完成。测试和调试手段的,求解如果有一组解满足这一约束说明存在一组输入使运行程序的结果和规约不符如果程序的规约正确,则匾乏己经成为制约软件生产率和软件质量的一个
5、瓶颈。测试可分为动态测试和静态测试两大类。动态测试就是程序中必定包含错误执行程序,再观察其行为是否满足要求。既可以由用户直接观约束求解工具接受的约束条件的集合以及求解能力决定,察,也可以使用一定的辅助工具。例如,等通过在了分析工具发现错误的能力和效率从理论上讲很多约束间题是不,程序中加入代码来动态地监视程序的运行状态可解的或者虽然可解但具有指数级的时间复杂度尽,,静态测试,而是通过对程序源代码进行管如此对于实际中的很多问题实例来说高效率的约束求解不编译运行程序。工具可以在用户可接受的时间内找到解或者
6、断定解不存在分析以发现其中的错误程序静态分析的目标不是证明程序完全正确,而是作为动态侧试的补充,在程序运行前尽可能多符号执行和约束求解方法的优点在于它可以精确地静态,。模,因此能地发现其中隐含的错臭提高程序的可靠性和健壮性事实拟程序的执行由于它跟踪了变量的所有可能取值。,上,很多相当成熟的系统中还包含着错误。只凭测试人员手工够发现程序中细微的逻辑错误但是在处理大程序时程序执测试很难找,行的可能的路径数目随着程序尺寸的增大而呈指数级增长出这些错误而通过静态测试则已经发现了现存,“。系统中的很多错误〔卜
7、〕在这种情况下就需要对路径进行选择选取一定数量的路径目前关于程序静态分析的研究是软件工程研究的一个热进行分析。,本文工作得到国家杰出青年科学基金和九七三计划的支持定理证明域中,作为具体域的函数的最小不动点的近似。虽然这样得出自动定理证明是基于语义的程序分析特别是程序验证中的结果集合常常比实际的最小不动点集合要大但是用于静。。常用到的技术但是采用消解原理的定理证明器一般并不适态分析己经可以接受合干程序分析因为它不太方便处理整数域、有理数域上的运基于规则的检查算。在这种情况下、人们常用各种判定过程在面向
8、不同应用的程序中,常常隐含着各种不同的编程。,。盯来判别公式是否为定理当然判别的方法和公规则例如在多线程程序中要求在使用某一共享变量时遵守。’,,一“,一“,八厂、,、二八“”式的形式有关对于形如八⋯八并肠使用前先加锁使用后解锁的规则操作系统的内核处理程护、的一组等式以及不等式的合取,判定的基本方法是首先序在屏蔽中断进行原子操作后必须打开中断屏蔽等。因此从由该合取式构造成一个图,合取式中的每一个条件对应于图经验的角度出发,人们提出了基于规则对程序进行分析的方中的一个结
