Combining Widening and Acceleration in Linear Relation Analysis
Combining Widening and Acceleration in Linear Relation Analysis
复制标题
在线性关系分析中结合加宽和加速
DOI：
10.1007/11823230_10
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
N. Halbwachs
中科院分区：
文献类型：
--
作者：
L. Gonnord;N. Halbwachs
线性关系分析[CH78， Hal79]是第一个，但仍然是最强大的，在无限晶格中工作的抽象解释之一。因此，它利用一个扩展算子来加强不动点计算的收敛性。虽然可以通过延迟加宽的应用来任意地改进由加宽引起的近似，但随着延迟的增加，分析很快变得过于昂贵。以前提高加宽精度的尝试并不完全令人满意，因为它们都不能保证提高结果的精度，而且它们会增加分析的成本。在本文中，我们研究了线性关系分析的改进，包括在可能的情况下计算环路的确切（抽象）效应。该技术与扩展的使用完全兼容，并且无论何时应用，它都可以提高分析的精度和性能。
Linear Relation Analysis [CH78, Hal79] is one of the first, but still one of the most powerful, abstract interpretations working in an infinite lattice. As such, it makes use of a widening operator to enforce the convergence of fixpoint computations. While the approximation due to widening can be arbitrarily refined by delaying the application of widening, the analysis quickly becomes too expensive with the increase of delay. Previous attempts at improving the precision of widening are not completely satisfactory, since none of them is guaranteed to improve the precision of the result, and they can nevertheless increase the cost of the analysis. In this paper, we investigate an improvement of Linear Relation Analysis consisting in computing, when possible, the exact (abstract) effect of a loop. This technique is fully compatible with the use of widening, and whenever it applies, it improves both the precision and the performance of the analysis.