Incremental Transitive Closure for Zonal Abstract Domain
Incremental Transitive Closure for Zonal Abstract Domain
复制标题
区域抽象域的增量传递闭包
DOI：
10.1007/978-3-031-06773-0_43
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Sherman, Elena
中科院分区：
文献类型：
--
作者：
Ballou, Kenny;Sherman, Elena
区域数值域是抽象解释静态分析中高效、弱关系的抽象域。与Interval域相比，Zonal域能够发现两个程序变量之间的弱关系。为了推理区域国家，必须将它们转化为规范的封闭形式。这项任务是通过传递闭包操作来完成的，该传递闭包操作通常实现为全对最短路径算法，其复杂性是程序变量的数量。在这项工作中，我们在数据流分析框架的背景下探索区域状态的封闭形式。此外，我们提出了一种增量传递闭包算法，该算法保留更新的区域状态的封闭形式。该算法将整体分析复杂度降低至。我们通过对现实世界的程序进行程序内区域分析来评估我们的方法。结果显示运行时间有所改善，尤其是在大型程序上。例如，使用传统区域实施方式运行的长达一小时的分析仪已通过建议的增量区域变体缩短为一分钟。
The Zonal numerical domain is an efficient, weakly-relational abstract domain in static analysis by abstract interpretation. Compared to the Interval domain, the Zonal domain is capable of discovering weak relations between two program variables. To reason about Zonal states, it is imperative that they are transformed into a canonical closed form. This task is accomplished through the transitive closure operation commonly implemented as the all-pairs shortest path algorithm, withcomplexity, whereis the number of program variables.In this work, we explore the closed form of Zonal states in the context of a data-flow analysis framework. Also, we present an incremental transitive closure algorithm that preserves a closed form of an updated Zonal state. The algorithm reduces the overall analysis complexity to. We evaluate our approach by performing intra-procedural Zonal analysis onreal-world programs. The results show an improvement in runtime, especially on large programs. For example, an hour-long analyzer run with the traditional Zonal implementation has been reduced to a minute with the proposed incremental Zonal variant.