基于补偿的浮点八边形抽象域

Compensation-based floating-point octagon abstract domain

为了解决抽象解释理论对浮点程序分析中的主要困难存在于构造复杂抽象域时采用实数而受限于高代价的计算量问题,针对八边形抽象域上实数运算提出了基于IEEE754的带补偿量的机器浮点表示及其运算算法,减少了浮点运算的复杂性;同时,将传统八边形抽象域扩展为可靠的浮点八边形抽象域,能够在分析的效率和精度之间取得合理的权衡.实验结果表明:用带补偿的浮点替代实数能够极大地提高八边形抽象域的效率,并且保证了分析的可靠性.

The main difficulties of floating-point programs analysis based on abstract interpretation exist in costly computation brought by the real number arithmetic when constructing the complex abstract domain.In this paper,a compensation-based floating-point number representation and relative arithmetic were proposed based on IEEE754 standard for octagon abstract domain.The method could reduce the complexity of floating-point arithmetic,and extend the traditional octagon abstract domain to sound floating-point octagon abstract domain,achieving a trade-off between efficiency and precision.Experimental results show that using the compensation-based floating-point octagon abstract domain rather than real number can significantly improve the efficiency,and ensure the reliability of analysis.