一句话：提出偏斜制表策略，通过消除递归非终结符产生的冗余摘要边，加速上下文无关语言可达性求解。
上下文无关语言可达性（CFL-reachability）是程序分析的常用模型，但主流 RHS 制表会生成大量不参与最终 S 边的冗余摘要边。本文提出偏斜制表，重点消除递归非终结符导致的无效边。其核心是修改分析树：静态变换文法，或采用专用在线求解器，从而避免递归非终结符的浪费。例如将 B::=B X 与 S::=A B 转为 S::=S X，使 S 的分析树更“偏斜”。作者实现该算法并用于别名、值流和污点分析；在 SPEC 2017 上，相较 RHS 求解器，三种客户端分别加速 3.34×、1.13×、2.05×，内存减少 60.05%、20.38%、63.06%，文法变换通常少于一秒。
Context-free language reachability (CFL-reachability) is a prominent model for formulating program analysis problems. Almost all CFL-reachability algorithms are based on the Reps-Horwitz-Sagiv (RHS) tabulation. In essence, the RHS tabulation, based on normalized context-free grammars, is similar to the CYK algorithm for CFL-parsing. Consider a normalized rule S : : = A B and a CFL-reachability problem instance of computing S -edges in the input graph. The RHS tabulation obtains all summary edges ( i.e., S -, A-, and B -edges) based on the grammar rules. However, many A - and B -edges are wasted because only a subset of those edges eventually contributes to generating S -edges in the input graph. This paper proposes a new tabulation strategy for speeding up CFL-reachability by eliminating wasted and unnecessary summary edges. We particularly focus on recursive nonterminals. Our key technical insight is that the wasted edge generations and insertions caused by recursive nonterminals can be avoided by modifying the parse trees either statically (by transforming the grammar) or dynamically (using a specialized online CFL-reachability solver). For example, if a recursive nonterminal B , generated by a rule B : : = B X , appears on the right-hand side of a rule S : : = A B , we can make S recursive (by introducing a new rule S : : = S X ) and eliminate the original recursive rule ( B : : = B X ). Due to the rule S : : = S X , the shapes of the parse trees associated with the left-hand-side nonterminal S become more “skewed”. Thus, we name our approach skewed tabulation for CFL-reachability. Skewed tabulation can significantly improve the scalability of CFL-reachability by reducing wasted and unnecessary summary edges. We have implemented skewed tabulation and applied the corresponding CFL- reachability algorithm to an alias analysis, a value-flow analysis, and a taint analysis. Our extensive evaluation based on SPEC 2017 benchmarks yields promising results. For the three client analyses, CFL-reachability based on skewed tabulation can achieve 3.34×, 1.13× and 2.05× speedup over the state-of-the-art RHS-tabulation- based CFL-reachability solver and consume 60.05%, 20.38% and 63.06% less memory, respectively. Furthermore, the cost of grammar transformation for skewed tabulation is negligible, typically taking less than one second.
@article{LeiBSZ24,
title = {Context-Free Language Reachability via Skewed Tabulation},
author = {Yuxiang Lei and Camille Bossut and Yulei Sui and Qirun Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656451}
}