基于可达性的抽象解释无环性分析
Reachability-based Acyclicity Analysis by Abstract Interpretation
摘要：
在具有存储器的动态使用的程序设计语言（诸如Java）中，知道引用变量x指向非循环数据结构对于终止和资源使用的分析是有价值的（例如，执行时间或存储器消耗）。例如，对于x的任何字段f，该信息保证x所指向的数据结构的深度大于x.f所指向的数据结构的深度。这反过来又允许限制循环的迭代次数，该循环通过其深度遍历结构，这对于证明终止或推断循环的资源使用是必不可少的。本文提出了一种基于抽象解释的静态分析的形式化方法，用于推断非循环性，该方法基于两个抽象域的约简积：可达性，它模拟了变量w所指向的位置可以通过解引用另一个变量v而到达的性质（在这种情况下，v被称为到达w）;以及循环性，对v可以指向循环数据结构的属性进行建模。分析被证明是健全的和最佳的相对于所选择的抽象。
英文摘要：
In programming languages with dynamic use of memory, such as Java, knowing that a reference variable x points to an acyclic data structure is valuable for the analysis of termination and resource usage (e.g., execution time or memory consumption). For instance, this information guarantees that the depth of the data structure to which x points is greater than the depth of the data structure pointed to by x.f for any field f of x. This, in turn, allows bounding the number of iterations of a loop which traverses the structure by its depth, which is essential in order to prove the termination or infer the resource usage of the loop. The present paper provides an Abstract-Interpretation-based formalization of a static analysis for inferring acyclicity, which works on the reduced product of two abstract domains: reachability, which models the property that the location pointed to by a variable w can be reached by dereferencing another variable v (in this case, v is said to reach w); and cyclicity, modeling the property that v can point to a cyclic data structure. The analysis is proven to be sound and optimal with respect to the chosen abstraction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
