基于浮点区间幂集抽象域的浮点程序分析

摘要

浮点变量在程序中的取值范围对浮点程序中相关性质的分析及运行时错误的检查具有重要意义。浮点运算的不精确性使得浮点变量的值范围分析具有挑战性。抽象解释理论为程序变量的值范围分析提供了一个通用的框架。在抽象解释的框架下，提出了一个新的数值抽象域——区间幂集抽象域，即使用有限个区间的析取来刻画变量的取值范围。该抽象域的表达能力强于经典的区间抽象域，能够较好地刻画大部分已有抽象域不能表达的非凸性质，从而有效提高分析精度。在此基础上，给出了区间幂集抽象域的可靠浮点实现方法，阐述了如何应用基于该抽象域的浮点实现对浮点程序进行可靠分析。基于抽象解释框架，设计实现了一个面向浮点C程序的静态分析工具原型，并使用浮点实现的区间幂集抽象域对一些浮点程序进行分析。%The value range of floating-point variables in the program is very important for analyzing properties and finding run-time errors in floating-point programs. The inexactness of floating-point computation makes it challenging to analyze value range of floating-point variables. The theory of interpretation provides a general framework to analyze the value range of program variables. Under this framework, this paper proposes a new numerical domain, namely powerset of intervals domain, which uses disjunctions of finite numbers of intervals to express the value range of a variable. It is more expressive than the classic interval domain, and can infer some non-convex properties that are beyond the ability of most numerical domains. On this basis, this paper gives a sound floating-point implementation for the new domain, and shows how to analyze floating-point programs soundly using this domain. Finally, this paper implements a static analyzer prototype for analyzing floating-point C programs based on the interpretation framework, which makes use of the floating-point implementation of the powerset of intervals domain to analyze floating-point programs.