Refinement of Path Expressions for Static Analysis
Refinement of Path Expressions for Static Analysis
复制标题
DOI：
10.1145/3290358
复制
发表时间：
2019-01-01
影响因子：
1.8
通讯作者：
Reps, Thomas
中科院分区：
文献类型：
--
作者：
Cyphert, John;Breck, Jason;Reps, Thomas
代数程序分析计算关于程序行为的信息，首先（a）计算有效路径表达式-即，识别所有可行的执行路径（通常更多）的正则表达式，然后（B）在定义分析的语义代数中解释路径表达式。有无数种不同的正则表达式可以作为有效的路径表达式，这就提出了一个问题：“我们应该选择哪一种？“虽然任何选择都会产生合理的结果，但对于许多分析来说，选择可能会对所得结果的精度产生巨大影响。本文研究了以下两个问题：（1）一个有效路径表达式比另一个有效路径表达式“更好”意味着什么？(2)我们能计算出一个“更好”的有效路径表达式吗？如果可以，如何计算？我们表明，这是不令人满意的比较两个路径表达式E-1和E-2仅仅通过它们生成的语言。与人们的直觉相反，对于L（E-1）的L（E-2）子集，E-2可能产生比E-1更不精确的分析结果，因此我们不想执行E-1 -> E2的变换。然而，排除路径，以便分析一个较小的语言的路径，正是所使用的一些先前的方法的细化criterion.在本文中，我们开发了一个算法，作为输入的有效路径表达式E，并返回一个有效的路径表达式E'，保证产生的分析结果，至少是一样好，使用E。虽然该算法有时返回E本身，但它通常不会：（i）我们证明了该算法的基本情况下的无退化结果-用于转换叶循环（即，最深嵌套的循环）;（ii）在非叶循环L处，算法将L的主体中的每个循环L'视为不可分割的原子，并且将叶循环算法应用于L;无退化结果也延续到（ii）。我们的实验表明，该技术具有实质性的影响：循环细化算法允许实现的组合递归分析证明超过25%以上的断言具有挑战性的循环微基准的集合。
Algebraic program analyses compute information about a program's behavior by first (a) computing a valid path expression-i.e., a regular expression that recognizes all feasible execution paths (and usually more) and then (b) interpreting the path expression in a semantic algebra that defines the analysis. There are an infinite number of different regular expressions that qualify as valid path expressions, which raises the question " Which one should we choose?" While any choice yields a sound result, for many analyses the choice can have a drastic effect on the precision of the results obtained. This paper investigates the following two questions:(1) What does it mean for one valid path expression to be "better" than another?(2) Can we compute a valid path expression that is "better," and if so, how?We show that it is not satisfactory to compare two path expressions E-1 and E-2 solely by means of the languages that they generate. Counter to one's intuition, it is possible for L(E-2) subset of L(E-1), yet for E-2 to produce a less-precise analysis result than E-1-and thus we would not want to perform the transformation E-1 -> E2. However, the exclusion of paths so as to analyze a smaller language of paths is exactly the refinement criterion used by some prior methods.In this paper, we develop an algorithm that takes as input a valid path expression E, and returns a valid path expression E' that is guaranteed to yield analysis results that are at least as good as those obtained using E. While the algorithm sometimes returns E itself, it typically does not: (i) we prove a no-degradation result for the algorithm's base case-for transforming a leaf loop (i.e., a most-deeply-nested loop); (ii) at a non-leaf loop L, the algorithm treats each loop L' in the body of L as an indivisible atom, and applies the leaf-loop algorithm to L; the no-degradation result carries over to (ii), as well. Our experiments show that the technique has a substantial impact: the loop-refinement algorithm allows the implementation of Compositional Recurrence Analysis to prove over 25% more assertions for a collection of challenging loop micro-benchmarks.