【作者】 陈立前；

【导师】 王戟；

【作者基本信息】 国防科学技术大学 ， 计算机科学与技术， 2010， 博士

【摘要】 软件的可信性已成为现代软件质量问题的焦点。发现并排除软件缺陷是构建可信软件的重要途径，这对于航天、国防、汽车等安全攸关应用尤其重要。科学与工程应用相关程序，特别是一些安全攸关嵌入式软件，一般与数学和物理有着紧密的联系，从而不可避免地会包含大量数值计算。因此，许多程序缺陷往往和程序中的数值性质密切相关，比如除零错、算术溢出、数组越界等运行时错误。抽象解释是一种对程序语义进行近似(或抽象)的通用理论，并为静态分析提供了一个通用的框架。而抽象域则是抽象解释框架下的核心要素，通过选择特定的语义表示和操作算法来发现所关注的性质。数值抽象域可用来自动发现程序中的数值性质，即程序变量间的数值关系。经过数十年的发展，在基于抽象解释的数值程序分析领域，出现了许多面向不同数值性质、表达能力多样的数值抽象域。然而，大部分已有数值抽象域(尤其是关系型抽象域)都是采用多精度有理数来实现以保证可靠性，时空开销较大，从而影响到分析的计算效率和可扩展性；而且，大部分已有数值抽象域在表达能力方面存在凸性局限性，对析取的处理能力较弱；此外，已有数值抽象域尚不支持实际程序分析中常出现的区间系数。本文主要研究数值抽象域的设计和实现。研究目标包括：探索数值抽象域的可靠浮点构造方法，以通过浮点实现来提高计算效率；设计新的数值抽象域使其能够表达非凸性质并支持区间系数，以通过增强表达能力来提高分析精度。本文主要工作如下：1)提出了浮点多面体抽象域，作为经典凸多面体域的一种可靠浮点构造方法。凸多面体域是目前表达能力最强、应用最广泛的数值抽象域之一，但是其基于多精度有理数的实现在可扩展性和易处理性方面受到限制。本文仅基于凸多面体的约束表示(无需生成子表示)并采用浮点系数，给出了凸多面体抽象域的一种可靠浮点实现方法，以通过浮点实现来提高凸多面体域的计算效率和处理能力。由于基于约束的多面体域的复杂度主要源于其高代价的接合操作(即凸闭包)，本文还提出了一系列低代价的弱接合操作。2)把区间线性代数引入到程序分析中，提出了一系列支持区间系数的区间线性抽象域。区间(算术)为构造可靠的浮点抽象域提供了一种自然且有效的途径，并且在实现浮点多面体域过程中也产生了凸多面体表达能力之外的区间线性约束。本文提出了区间多面体抽象域，用以推导程序中变量间的区间线性不等式关系。该域可以看作是经典凸多面体域的区间系数扩展版本。作为一种受限情形，本文还提出了行阶梯形区间线性等式抽象域，用以推导区间线性等式关系。其表示方法基于区间线性等式系统的行阶梯形式，使得该域具有多项式的时空复杂度。该域可以看作是经典仿射等式抽象域的区间系数扩展版本。通过采用区间线性系统的弱解语义，这些区间线性抽象域能够天然地表达某类拓扑非凸(甚至非连通)性质。本文采用浮点数并基于向外舍入的区间算术可靠地实现了这些抽象域。3)提出了一系列可表达非凸性质的线性绝对值抽象域。绝对值是数学中的一个基本概念，常用来描述数学或物理模型中的分段线性特征，并且可以表达非凸性质。本文给出并证明了线性绝对值不等式系统、区间线性不等式系统、广义线性互补问题(系统)三者之间的等价性，以及线性绝对值等式系统、水平线性互补问题(系统)两者之间的等价性。基于凸多面体的双重描述法，给出了广义线性互补问题(系统)的双重描述法，并作为其应用还给出了一种求解绝对值线性规划问题的新方法。在此基础上，本文提出了线性绝对值不等式抽象域(用来推导线性绝对值不等式／区间线性不等式／广义线性互补不等式关系)和线性绝对值等式抽象域(用来推导线性绝对值等式／水平线性互补等式关系)。线性绝对值不等式域是经典多面体域的一般化，虽然表达能力与区间多面体域相同，但是其域操作都是具体域上对应操作的最佳抽象。而线性绝对值等式域是经典仿射等式域的一般化。基于广义线性互补系统的双重描述法并采用多精度有理数实现了这两个抽象域。本文提出的数值抽象域在分析精度和计算效率间进行了不同的权衡，可以面向不同的应用。这些抽象域都在数值抽象域库APRON中得以实现，并且实验结果令人鼓舞。更多还原

【Abstract】 Trustworthiness of software has become the center of attention when consider-ing modern software quality. Finding bugs before release is fundamental to buildtrustworthy software, which is extremely important for safety-critical applicationssuch as aerospace, defense and automotive. Scienti?c and engineering programs es-pecially safety-critical embedded software are usually related to mathematics andphysics, and thus often involve a lot of numerical computations. Hence, many pro-gram bugs including division by zero, arithmetic over?ows and array out-of-bounds,are closely related to numerical properties in the program.Abstract interpretation is a theory of semantics approximation, allowing thedesign of sound and e?cient static analyses. Abstract domains are a key ingredi-ent in this framework: They enable semantic choices (what properties to infer) andalgorithmic choices (how to compute). In this thesis, we focus on design and im-plementation of numerical abstract domains that are used to automatically discovernumerical properties over program variables. Over the past decades, a wide variety ofnumerical abstract domains have been proposed. However, most existing abstractdomains (especially relational ones) need arbitrary precision rational numbers tobuild implementations, which may degrade the time and memory e?ciency. Mostof them can only represent convex properties, and hence have limitations in deal-ing with disjunctions. Besides, currently there is no abstract domain that supportsinterval variable coe?cients which appear naturally in real-life program analysis.The goal of this thesis is to explore more e?cient numerical abstract domains,using sound ?oating-point constructions, and to design more precise ones, allowingnon-convex properties and interval coe?cients.Major contributions of this thesis are listed as follows.1) We present a so-called ?oating-point polyhedra abstract domain. The clas-sical convex polyhedra domain is one of the most powerful and commonly used ab-stract domains in the ?eld, but rational implementations may su?er from scalabilityproblems. To solve this issue, we present an implementation using ?oating-pointarithmetic without sacri?cing soundness, based on a constraint-only representation using ?oating-point coe?cients. Since its complexity mainly comes from the costlyjoin operation (i.e., polyhedral convex hull), a series of cheap weak join operationsare then proposed.2) We introduce interval linear algebra to static analysis and propose intervallinear abstract domains that support interval coe?cients. Intervals are naturallysuited to construct sound ?oating-point abstract domains. First, a so-called intervalpolyhedra domain is proposed to infer interval linear inequalities. Then, a restrictedabstract domain is proposed based on a system of interval linear equalities in rowechelon form, polynomial in time and memory. The two domains can be consid-ered as interval extensions of the existing convex polyhedra domain and the a?neequality domain respectively. By interpreting solutions as weak solutions of intervallinear systems, both domains can express certain non-convex (even unconnected)properties. They are soundly implemented using ?oating-point numbers based oninterval arithmetic with outward rounding.3) We present linear absolute value abstract domains that natively allow toexpress non-convex properties. Absolute value (AV) is fundamental in mathematicsand often used to describe piecewise linear behavior. The equivalence among linearAV inequality systems, interval linear inequality systems and extended linear com-plementarity problem (XLCP) systems is stated. We construct a double descriptionmethod for XLCP on top of that for polyhedra, based on which a new method forsolving AV linear programming problems is shown. On this basis, we propose anabstract domain of linear AV equalities, and an abstract domain of linear AV in-equalities that has the same expressiveness as interval polyhedra domain but enjoysoptimal transfer functions. They are implemented using rational numbers based onthe double description method for XLCP.The numerical abstract domains presented in this thesis provide di?erent trade-o?s between precision and e?ciency, and can be applied to di?erent problems. Theyare implemented in the APRON library, and experimental results are encouraging.更多还原