paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Better Not Together: Staged Solving for Context-Free Language Reachability

最好不要一起:上下文无关语言可达性的分阶段求解
ISSTA Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis2024匹配度 3/10 · 论文研究CFL可达性的分阶段求解,属于程序分析与静态分析核心算法,但未涉及用户当前重点关注的LLM/Agentic程序分析、浮点程序分析或贝叶斯程序分析,也未与LLM/Agent交叉。引用 2 inbox
Chenghang Shi, Haofeng Li, Jie Lu, Lian Li
crossref: 2026-09-12

AI 速览

一句话:提出分阶段求解 CFL 可达性,将文法分解为括号匹配 CFG 与控制/数据流正则文法,大幅加速程序分析。

上下文无关语言可达性(CFL-reachability)是程序分析的基础形式化方法,但求解代价高昂,复杂度接近输入图节点数的次立方。论文提出分阶段求解:将基于 CFL 的分析所用上下文无关文法分解为用于匹配括号(如过程调用/返回、字段存储/加载)的较小 CFG L,以及刻画控制/数据流的正则文法 R。不同于标准算法整体求解两者,该方法分两阶段求解 L 可达性与 R 可达性;L 仍为上下文无关但只涉及少量边,R 可近二次时间高效计算。作者实现求解器 STG,在上下文敏感值流分析与字段敏感别名分析上评估,平均较标准次立方算法分别加速 861.59 倍和 4.1 倍,并使 POCR、PEARL 显著提速。

问题
CFL-reachability 求解计算代价高,标准算法对输入图节点数呈近次立方复杂度,难以扩展到大规模程序分析。
方法
提出分阶段求解,将分析文法分解为括号匹配的较小 CFG L 和捕获控制/数据流的正则文法 R,分别求解 L 可达性与 R 可达性,并实现求解器 STG。
评估
在上下文敏感值流分析和字段敏感别名分析两个客户端上,与标准次立方算法及 POCR、PEARL 对比,报告平均加速比。
原文摘要(Abstract)

Context-free language reachability (CFL-reachability) is a fundamental formulation for program analysis with many applications. CFL-reachability analysis is computationally expensive, with a slightly subcubic time complexity concerning the number of nodes in the input graph. This paper proposes staged solving: a new perspective on solving CFL-reachability. Our key observation is that the context-free grammar (CFG) of a CFL-based program analysis can be decomposed into (1) a smaller CFG, L, for matching parentheses, such as procedure calls/returns, field stores/loads, and (2) a regular grammar, R, capturing control/data flows. Instead of solving these two parts monolithically (as in standard algorithms), staged solving solves L-reachability and R-reachability in two distinct stages. In practice, L-reachability, though still context-free, involves only a small subset of edges, while R-reachability can be computed efficiently with close to quadratic complexity relative to the node size of the input graph. We implement our staged CFL-reachability solver, STG, and evaluate it using two clients: context-sensitive value-flow analysis and field-sensitive alias analysis. The empirical results demonstrate that STG achieves speedups of 861.59x and 4.1x for value-flow analysis and alias analysis on average, respectively, over the standard subcubic algorithm. Moreover, we also showcase that staged solving can help to significantly improve the performance of two state-of-the-art solvers, POCR and PEARL, by 74.82x (1.78x) and 37.66x (1.7x) for value-flow (alias) analysis, respectively.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot8602,
  title = {Better Not Together: Staged Solving for Context-Free Language Reachability},
  author = {Chenghang Shi and Haofeng Li and Jie Lu and Lian Li},
  booktitle = {ISSTA},
  year = {2024},
  doi = {10.1145/3650212.3680346}
}