区间幂集抽域及其在浮点程序分析中的应用

浮点变量在程序中的取值范围对浮点程序中相关性质的分析及运行时错误的检查具有重要意义.浮点运算的不精确性使得浮点变量的值范围分析具有挑战性.抽象解释理论为程序变量的值范围分析提供了一个通用的框架.在抽象解释的框架下,本文提出一个新的数值抽象域--区间幂集抽象域,其使用有限个区间的析取来刻画变量的取值范围.该抽象域的表达能力强于经典的区间抽象域,能够较好地刻画大部分已有抽象域不能表达的非凸性质,从而有效提高分析精度.在此基础上,本文给出了区间幂集抽象域可靠浮点实现的方法,然后阐述了如何应用基于浮点区间幂集抽象域对浮点程序进行可靠地分析.最后本文基于抽象解释框架,设计实现了一个面向浮点C程序的静态分析工具原型,并使用浮点实现的区间幂集抽象域对一些浮点程序进行分析。