程序静态分析
程序静态分析是在不执行程序的情况下对其进行分析的技术,简称为静态分析。而程序动态分析则是另外一种程序分析策略,需要实际执行程序。大多数情况下,静态分析的输入都是源程序代码,只有极少数情况会使用目标代码。静态分析这一术语一般用来形容自动化工具的分析,而人工分析则往往叫做程序理解。
静态分析越来越多地被应用到程序优化、软件错误检测等领域。Coverity Inc.的软件质量检测产品就是利用静态分析技术进行错误检测的成功代表。
形式化方法
程序分析中的形式化方法一般指利用纯粹严格的数学方法对软件、硬件进行分析的理论及技术。这些数学方法包括符号语义、公理语义、操作语义和抽象解释。
1952年提出的Rice定理指出,任何关于程序分析的问题都是不可判定的。因此,不存在任何一种机械化的方法能够证明程序的完全正确性。然而,针对大多数的不可判定问题,仍然可以试图找到它们的一些近似解。
形式化静态分析中用到的实现技术有:
模型检查假设系统是有限状态的、或者可以通过抽象归结为有限状态。
抽象解释将每条语句的影响模型化为一个抽象机器的状态。相比实际系统,抽象机器更简单更容易分析,但其代价是丧失了分析的完备性(并不是原始系统中的每种性质在抽象机器中都是保留的)。抽象解释当且仅当抽象机器中的每一个性质都能与原始系统中的性质正确映射时,才被称作可靠(sound)的。
断言在霍恩逻辑中首次被提出。目前存在一些针对特定程序设计语言的工具,例如ESC/JAVA和ESC/JAVA2中分别使用的SPARK语言和JML语言。
著名的静态分析工具
Meta-Compilation
由Standford大学的Dawson Engler教授等研究开发,该静态分析工具允许用户使用一种称作metal的状态机语言编写自定义的时序规则,从而实现了静态分析工具的可扩展性。MC的实际效果非常优秀,号称在Linux内核中找出来数百个安全漏洞。MC目前已经商业化,属于Coverity Inc.
mygcc由一个法国人N. Volanschi开发,其思想来源于MC,试图将自定义的错误检测集成到编译时。
代码静态分析相关工具及一些使用简介
在代码构建过程中使用静态分析工具有助于发现代码缺陷,并提高代码的质量。本节关注三个代码静态分析工具的使用:Findbugs、PMD和Checkstyle。这三个工具各有不同的特点,联合使用有助于减少误报错误,提高报告的准确率。
使用目的这三个工具检查的侧重点各有不同:
工具
目的
主要检查内容
FindBugs
基于Bug Patterns概念,查找java bytecode中的潜在bug。在目前版本中,它不检查java源文件。
主要检查bytecode中的bug patterns,也允许用户自定义特定的bug patterns。
PMD
检查java源文件中的潜在问题。
主要包括:
² 空try/catch/finally/switch语句块
² 未使用的局部变量、参数和private方法
² 空if/while语句
² 过于复杂的表达式,如不必要的if语句等
² 复杂类
CheckStyle
检查java源文件是否与代码规范相符
主要包括
² Javadoc注释
² 命名规范
² Headers
² Imports
² Size冲突和度量,如过长的方法
² Whitespace
² Modifiers
² Blocks
² Coding Problems
² Class Design
² 重复代码
² Miscellaneous Checks
² Optional Checks
本文中三个工具各自的版本分别是:FindBugs 0.85、PMD 2.0和CheckStyle 3.3。这三个工具都可以从sourceforge下载,而且它们都为Eclipse提供了相应的plugin。
用法关于IDE以及plugin如何使用在此不做介绍,本文主要关注它们如何与ant配合使用,使这些工具成为每次构建过程中的有机组成。
FindBugsFindBugs的运行环境可能是这三个工具之中最苛刻的了。它工作在j2se1.4.0或以后的版本中,需要至少256MB内存。它的安装非常简单,下载之后简单的解压即可。为了与ant配合使用,它提供了对应的ant task。它的使用:
1. findbugs复制到项目的classpath中,并删除将这些文件纳入开发管理中很容易在另一台机器上重建构建环境。不建议向手册中所说的仅仅将findbugs-ant.jar复制到ANT_HOME/lib下。
2. 修改build.xml:
<!-- 定义findbugs所在目录,建议直接将findbugs复制到classpath中 -->
<property name="findbugs.home" value="lib/findbugs" />
<!-- 定义findbugs任务,以及所在的jar文件 -->
<taskdef name="findbugs" classname="edu.umd.cs.findbugs.anttask.FindBugsTask"
classpath="${findbugs.home }/lib/findbugs-ant.jar"/>
<target name="findbugs">
<!-- 使用,所用参数介绍见后 -->
<findbugs home="${findbugs.home}"
output="html"
outputFile="findbugs.html" >
<!-- fog.jar所依赖的classpath引用 -->
<auxClasspath refid="classpath"/>
<!-- fog.jar对应的源文件 -->
<sourcePath path="src" />
<!-- 要分析的bytecode文件 -->
<class location="bin/lib/fog.jar" />
</findbugs>
</target>
3. 运行:ant findbugs。
4. 参数说明:
属性:
- home属性,指出findbugs的安装目录
- quietErrors属性,如果为true,那么严重分析错误和丢失类信息不会出现在输出中。缺省为false。
- reportLevel属性,指明报告输出bug的级别。”low”,所有bug全部输出;”medium”(缺省),输出中级和高级bug;”high”,只输出高级bug。
- output和outputFile属性,指明输出格式和文件名。
- sort属性,如果为true(缺省),输出按类名排序。
- debug属性,是否输出findbugs的调试信息,缺省为false。在自定义bug检测器时使用进行调试。
- visitors属性,用逗号分隔的类名,指明哪些bug检测器可以运行。缺省是所有。
- omitVisitors属性,相当于visitors属性取反,指明哪些bug检测器不能运行。
- excludeFilter和includeFilter属性,指明排除和包含的过滤器(即定义它的文件名)。
- projectFile属性,与findbug gui相关,略。
- jvmargs属性,指明需要传递给jvm的参数。
- timeout属性,超时设置,以毫秒为单位。缺省是600000ms,是10分钟。
- failOnError属性,为true时,如果有findbugs运行中出错,中止构建过程。缺省为false。
- workHard属性,用于将低输出的错误率,但是运行也最慢。缺省为false。
内嵌元素:
- class元素,要分析的bytecode。
- auxClasspath元素,class元素依赖的类。
- sourcePath元素,class元素对应的源文件,它用来指出findbugs输出内容所对应的源文件信息。
- systemProperty元素,定义系统属性。
使用过滤器。过滤器用来包含或排除特殊的bug报告。这样做有助于在特定的时间段内,聚焦我们的关注点。过滤器实际是在一个xml文件定义的,它的典型格式:
<FindBugsFilter>
<!-- 所有的bug检测器都与这个类匹配 -->
<Match class="com.foobar.ClassNotToBeAnalyzed" />
<!-- bugcode为DE,UrF,SIC与这个类匹配 -->
<Match class="com.foobar.ClassWithSomeBugsMatched">
<BugCode name="DE,UrF,SIC" />
</Match>
<!-- bugcode为XYZ的匹配所有的类 -->
<Match classregex=".*" >
<BugCode name="XYZ" />
</Match>
<!-- bugcode为DC的匹配这个类的这些方法 -->
<Match class="com.foobar.AnotherClass">
<Or>
<Method name="nonOverloadedMethod" />
<Method name="frob" params="int,java.lang.String" returns="void" />
<Method name="blat" params="" returns="boolean" />
</Or>
<BugCode name="DC" />
</Match>
</FindBugsFilter>
通过task的excludeFilter和includeFilter属性,可以在findbugs的输出报告中包含或排除匹配它们。具体每个bug检测器的bugcode,可以在plugin/coreplugin.jar/messages.xml中找到。其中messages.xml中的bugcode实际是findbugs.xml(也在coreplugin.jar中)每个Detector元素的reports属性的第一个缩写。如:reports属性为VO_VOLATILE_REFERENCE_TO_ARRAY,对应的bugcode=”VO”。
从使用来看,findbug还是相当简单的。但要用好,使用者还需要了解bug patterns的相关知识,如覆盖equals的同时需要覆盖hashcode。而且,findbugs也允许我们自定义bug patterns,使之方便的扩展。关于这部分内容,请参见developerworks上的文章《FindBugs,第 2 部分:编写自定义检测器》。
PMDPMD的运行环境是j2se1.3或以后版本,安装过程同样也是解压即可。对应ant task的使用:
1. 把lib中所有的jar复制到项目的classpath中。
2. 将pmd-2.0.jar中的rulesets解压到指定目录,这里面定义了分析所需要的规则集合。
3. 修改build.xml文件。在这一版本中,提供了2个ant task。一个是pmd使用规则集合进行分析;另一个是检查代码中Copy & Paste代码。这2个任务对应的ant task使用:
PMD任务:
<target name="pmd">
<!-- 定义任务和任务所属类所在的classpath引用 -->
<taskdef name="pmd" classname="net.sourceforge.pmd.ant.PMDTask"
classpathref="classpath"/>
<!-- 检查使用的规则文件 -->
<pmd rulesetfiles="junit_lib/rulesets/imports.xml">
<!-- 输出格式和文件名 -->
<formatter type="html" toFile="pmd_report.html"/>
<!-- pmd所需要依赖包的classpath引用 -->
<classpath refid="classpath"/>
<!-- 要检查的项目源文件根目录 -->
<fileset dir="src">
<include name="**/*.java"/>
</fileset>
</pmd>
</target>
CPD任务:
<target name="cpd">
<!-- 定义任务和任务所属类所在的classpath -->
<taskdef name="cpd" classname="net.sourceforge.pmd.cpd.CPDTask"
classpathref="classpath"/>
<!-- 指明输出文件和判断属于copy & paste的标准 -->
<cpd minimumTokenCount="100" outputFile="cpd.txtl">
<!-- 要检查的项目源文件根目录 -->
<fileset dir="src">
<include name="**/*.java"/>
</fileset>
</cpd>
</target>
4. 运行ant pmd和ant cpd即可。
5. 参数说明:
- formatter,指明输出格式和文件。
- rulesetfiles,指明分析所需的规则文件,不同文件使用逗号分隔。
- failonerror,pmd执行出错是否中止构建过程。
- failOnRuleViolation,如果与规则冲突,是否中止构建过程。
- classpath,pmd所需的classpath。
- printToConsole,在发现问题时是否打印到ant log或控制台。
- shortFilenames,在输出报告中是否使用短文件名。
- targetjdk13,是否把目标定为jdk13,如不能使用assert。
- failuresPropertyName,在任务结束时,插入违反规则的号码
- encoding,读源文件时所采用的编码,如utf-8。
关于规则集合的说明,以及如何自定义规则请参见pmd的文档,文档中已说得相当清楚。
CheckStyle使用ant task:
1. 复制checkstyle-all-3.3.jar到项目的classpath中。
2. 修改build.xml文件:
<taskdef resource="checkstyletask.properties"
classpath="${weblib.dir}/checkstyle-all-3.3.jar"/>
<target name="checkstyle" depends="init">
<!-- 指明checkstyle的分析所需的规则文件 -->
<checkstyle config="checkstyle33.xml">
<!-- 要检查的文件 -->
<fileset dir="${src.code}" includes="**/*.java"/>
<!-- 指明输出格式和文件名 -->
<formatter type="xml" toFile="report.xml"/>
</checkstyle>
<!-- 将xml文件转换成html文件 -->
<style in="report.xml" out="report.html" style="checkstyle-frames"/>
</target>
3. 运行ant checkstyle即可。
checkstyle的规则文件,即项目的代码规范,建议不要手工书写。可以使用checkstyle plug in在Eclipse配置后再导出。Checkstyle提供了缺省的xslt,用来进行xml的格式转换。它们都放在contrib目录中。Checkstyle同样也提供了自定义的check,但与PMD相比,书写要复杂。详细情况请参见checkstyle的文档。
检查表- 为每个工具建立自己的目录和classpath变量。由于这些工具大多都使用了相同的开源软件,很容易会因为使用相同软件包的不同版本而相互干扰。这种问题非常隐蔽,在这种问题上花费时间和精力是非常不值得的。通过建立不同的目录和classpath,然后在对应的ant task中引用各自的classpath,可以有效的避免它。
- 将这些工具纳入项目的配置管理库中。这样可以方便而迅速的在另一台机器上重建构建环境,有效的保证了项目组中统一的构建环境。
- 重视这些输出,但是不要因为输出而困扰。它们仅仅是工具,要学会正确的对待它们。
- 三个工具都提供了自定义规则的接口,相比而言pmd书写最简单,findbugs功能最强。它们涉及AST(抽象语法树)和byte code相关的知识。