自动合成数组不变式

本文提出了一个基于抽象解释框架自动合成数组程序不变式的方法.它能够分析按照特定顺序访问一维或者多维数组的程序,然后合成不变式.该方法将性质（包括区间全称量词性质和原子性质）集合作为抽象域,通过前向迭代数据流分析合成数组性质.本文证明了该方法的正确性和收敛性,并通过一些实例展示了该方法的灵活性.我们开发了一个原型工具.该工具在各种数组程序（包括Competition on Software Verification中的array-examples benchmark）上的实验展示了方法的可行性和有效性.     

含有析取语义循环的不变式生成改进方法

抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显式和隐式含有析取语义的循环结构,提出了基于循环分解和归纳推理的不变式生成改进方法,缓解了抽象解释分析中出现的语义损失问题.实验结果表明:相比已有方法,该方法能为这种包含析取语义的循环结构生成更加精确的不变式,并且有益于一些安全性质的推理.     

基于指向与数值抽象的带指针算术程序的分析方法

带指针算术的程序往往包含数组越界、缓冲区溢出等运行时错误。单纯的指针分析技术和数值分析技术都无法有效处理指针算术。为了将指针分析与数值分析相结合,首先提出一种新的指针内存模型,然后基于该模型设计了一个刻画指针指向关系和指针偏移量的抽象域。最后在抽象解释框架下,设计并实现了一个面向带指针算术C程序的静态分析工具原型PAA。实验结果表明,PAA能够有效地分析指针程序的指向关系和数值性质,并能够在效率和精度间取得合理的权衡。     

CILinear:一个线性不变式自动构造工具

构造不变式是程序验证的重要组成部分,而开源工具Interpro。能对简单的程序设计语言构造线性不变式。基于Interproc和C程序编译工具CII,针对简化的C程序设计并实现了自动构造数值型程序变量线性不变式的工具CILinear,并与Interproc进行了比较。实验表明CILinear能有效地构造线性不变式,并且比Interproc支持的语法更多。通过实例讨论了CILinear在程序验证中的实际应用。     

基于抽象解释的可执行代码值范围分析

阐述可执行代码抽象存储空间模型的概念并给出程序运行时刻环境抽象表示技术。通过抽象解释静态逼近程序不动点语义的理论保证二进制代码数据流分析的正确性以及可计算性。基于抽象解释和单调数据流框架提出一种自动分析可执行代码变量取值范围的方法及自动获取程序循环最大迭代次数和不可执行路径,并给出数据流分析实例。     

一个基于Mathematica平台的程序安全性自动验证工具

程序安全性验证是程序验证的重要部分。基于不变式生成,将程序的安全性验证转化为验证不变式集合是否蕴含表示安全性的逻辑公式。针对简化的C程序,结合验证工具Theorema,在Mathematica平台上实现一个对程序安全性进行自动验证的工具。实验结果表明,该验证工具能够自动验证只含数值变量的C程序。     

基于抽象解释的函数内联过程间分析优化方法

分析实际程序时往往需要分析程序中函数的调用, 一般使用过程间分析来实现全程序分析.函数内联是一种最为精确、易于实现的过程间分析方法.通过函数内联, 可以使得已有过程内分析方法和工具支持包含函数调用的程序的分析.但是, 函数内联后代码的规模急剧增加, 同时将产生大量中间变量, 增加程序分析的变量维度, 导致程序分析过程时空开销大大增加.本文考虑基于抽象解释框架下函数内联过程间分析的一些不足, 并提出相应优化方法.基于抽象解释的程序分析关注自动推导程序变量之间的不变式约束关系, 因此程序变量构成的程序环境大小(即各程序点处须考虑的相关变量集合)对分析的时空开销具有重要影响.为了减少函数内联后程序分析的开销, 本文提出了面向内联函数块的程序环境降维优化方法.该方法针对内联函数后的程序代码, 分析确定不同程序点处需维护的程序环境(即相关变量集合), 而不是所有程序点共享同一全局程序环境, 从而实现程序状态的降维.详细描述了基于该方法所实现的工具DRIP (Dimension Reduction for analyzing function Inlined Program) 的架构、模块及算法细节.并在WCET Benchmarks测试集开展了分析实验, 实验结果表明: DRIP在变量消除上取得的效果良好, 甚至在某些测试集上能减少一半以上的变量, 并在一定程度上降低了分析过程的时空开销.     

单变量区间线性不等式抽象域

程序变量的值范围信息对于编译器优化、程序分析与验证等应用至关重要.抽象解释理论提供了一种通用框架为程序变量计算近似的但是可靠的值范围.然而该框架下已有的数值抽象域在表达非凸性质方面存在一定的局限性,影响了值范围分析的精度.文中基于抽象解释理论,提出一个新的数值抽象域——单变量区间线性不等式抽象域.其主要思想是使用单变量区间线性不等式约束作为域元素的约束表示方法.该抽象域的表达能力强于经典的区间抽象域,并允许表达某类非凸、非连通性质.同时,其域操作存在高效的实现算法.该抽象域具有很强的可扩展性,能够应用在实际大规模的程序分析中.     

基于语法树和JavaCC的程序题自动评分系统

为了提高程序题自动评分的准确性,及解决传统评分方法无法从语法结构和语义角度衡量错误的学生程序与正确答案之间的相似度,提出了一种基于抽象语法树匹配的程序题自动评分方法。文中以JavaCC技术为核心,首先通过词法分析、语法分析和语义分析生成错误列表和抽象语法树的中间表示,然后通过语法树切片匹配得分,最后和错误列表结合给出评分结果。文中详细论述了各个模块的设计方法,着重讨论了抽象语法树生成并匹配的细节,设计并实现了一个传统方法与语义分析结合的C＋＋程序题自动评分系统。通过对实际考试的结果进行实验,进而验证了该系统的实用性与有效性。     

基于抽象域和数值熵协同的数值程序分析

在软件日益丰富的信息时代,程序的正确性验证问题需要深入地研究。提出了基于抽象解释和数值熵协同的数值程序正确性分析方法。利用抽象解释理论框架对数值程序进行抽象解释分析,提取不变量的抽象域区间;在抽象域区间上进行数值熵运算;运行程序获取数值变量的实际取值,计算数值熵;将抽象域区间数值熵和实际数值熵信息进行对比分析,准确地判断程序的正确性等性质。单纯的抽象解释分析只可以近似得到数值变量的取值范围,而引入数值熵算法,在取值范围的基础上对程序静态分析的准确性进一步检验,同时也做到了对程序的正确性验证。通过C语言程序实例,对抽象解释基础上的熵值分析方法进行了验证,证明了该分析方法的可行性和正确性。     

一种基于抽象解释和通用单调数据流框架的值范围分析方法

安全而又精确的值范围分析对编译器优化至关重要．系统地提出了一个基于抽象解释和通用单调数据流框架的值范围分析框架，包括精确的定叉、分析和完整的正确性证明．与一般的值范围分析方法不同，该框架不仅包括抽象解释，还包括与之对应的具体解释，以及相应的正确性证明．     

PAST: accurate instrumentation on fully optimized program

Instrumentation is a powerful technique for monitoring, profiling, debugging, logging and tracing the software. In order to determine the instrumentation location, the user needs to know where the current executed location is in the source code. Previous instrumentation approaches rely on debugging information to find the location in the source code. For fully optimized programs, debugging information is not complete, which limits the application of those approaches. In this paper, we present pattern‐based abstract syntax tree (PAST) instrumentation, an ideal instrumentation methodology that accurately instruments the fully optimized program. The instrumentation location is specified in an intuitive way that matches the source code at the abstract syntax tree level. The program can be instrumented either at the compile time using the ordinary compiling or when it is running using the just‐in‐time compiling. Experimental results show that PAST can accurately instrument the target program. There is negligible run time overhead when the running program is instrumented without any operation. We have implemented PAST on both x86‐32 and x86‐64 to show that PAST is easily portable across different architecture. Copyright © 2015 John Wiley & Sons, Ltd.     

基于抽象符号表的内存模型

符号执行技术在软件测试和程序验证中发挥着重要作用。如何抽象和处理程序中各种数据类型和语法成分是符号执行必须解决的问题。本文提出抽象符号表的概念,以及基于抽象符号表建模内存的方法。抽象符号表记录可寻址对象的名称、类型、抽象地址和符号值,是一种简单、精确的内存抽象机制。内存模型是所有使用符号执行的技术的前提,本文系统给出了一个面向符号执行的内存模型。基于抽象符号表的内存模型能够统一处理各种数据类型和语法成分,包括函数和类,能够直接处理指针别名问题,不需要额外的别名分析算法。经过一些性能优化处理,基于抽象符号表的内存模型具有较好的性能。     

基于JavaCC的抽象语法树生成错误处理技术研究

随着C++语言标准的不断演进,词法语法解析工具如JavaCC等对于很多扩充的新特性以及复杂的语法结构不能做到完全支持,这可能会导致抽象语法树生成错误且不完整;针对这一问题,提出一个针对抽象语法树生成错误的处理框架;首先,通过对JavaCC的扩充,实现一套可以解析C++语言的词法语法分析器,生成抽象语法树并记录报错行;其次,根据报错行寻找所在函数区间即不支持或不匹配的语法片段;最后,通过注释函数区间的方式来跳过不支持或不匹配的语法片段进行错误处理并迭代生成抽象语法树;实验结果表明,对抽象语法树生成进行错误处理后可以更全面的分析代码,抽象语法树完成率上升37.8%,分析行数提高3.9倍。     

Program Behavior at the Symbolic Level

No application programmer writes machine-language programs–i.e., strings of ones and zeroes. That primitive pursuit has long been reserved for those few who create the very first modules of a software system for new hardware. Instead, programmers make use of a wide spectrum of symbolic programming languages, ranging from assembly code to high-level languages such as Fortran, Cobol, and the Algol family. Every programming language has semantics which define some abstract machine. For the assembly-language programmer this machine bears a great resemblance to the actual hardware on which the program will be interpreted, but even here the programmer will frequently use system-defined subroutines or macros which represent extensions of the base hardware facilities. The high-level language programmer's abstract machine reflects the control mechanisms and data structures characteristic of the language. The Fortran programmer, for example, can think in terms of multidimensional array structures, DO loops, subprogram facilities, and so on. In principle he need never be concerned with the manner in which his abstract Fortran machine is to be realized by a particular hardware and software system. The user of a modern electronic hand calculator needs no knowledge of the works inside the box, and a modern high-level language system should present to its users an equally consistent environment, completely defined in terms of the syntax and semantics of the source language.     

基于静态检测的C++内存泄漏分析

C++是一种非常流行的计算机编程语言,在使用的过程中容易出现内存泄漏问题,而该问题往往难以识别。给出了一种对C++内存泄漏问题进行分析的方法,该方法得到C++源代码的抽象语法树,从抽象语法树中提取程序控制流图,然后将类的构造函数、普通成员函数以及析构函数的程序控制流图相互连接形成新的程序控制流图,并设计算法对控制流图进行检测。最后通过一些内存泄漏的典型实例进行测试,实验表明本方法有效。