一句话：提出一种与具体 InterDyck 可达性算法正交的图预处理简化方法，安全删除不贡献交错 Dyck 路径的边，提升精度与可扩展性。
许多程序分析问题可归约为图可达性，其中 InterDyck 可达性可同时建模上下文敏感、域敏感和指针解引用等依赖。精确 InterDyck 可达性不可判定，现有方法只能过近似。本文从简化输入图出发：若一条边不参与任何 InterDyck 路径，则可安全删除，据此设计了快速图简化算法。该技术与具体 InterDyck 形式化和过近似算法正交，可作为预处理步骤。作者将其用于 Android 污点分析图，并在三种主流 InterDyck 可达性算法上评估，结果显示可扩展性与精度均获提升，部分场景提升显著。
Many program-analysis problems can be formulated as graph-reachability problems. Interleaved Dyck language reachability ( InterDyck -reachability) is a fundamental framework to express a wide variety of program-analysis problems over edge-labeled graphs. The InterDyck language represents an intersection of multiple matched-parenthesis languages (i.e., Dyck languages). In practice, program analyses typically leverage one Dyck language to achieve context-sensitivity, and other Dyck languages to model data dependencies, such as field-sensitivity and pointer references/dereferences. In the ideal case, an InterDyck -reachability framework should model multiple Dyck languages simultaneously . Unfortunately, precise InterDyck -reachability is undecidable. Any practical solution must over-approximate the exact answer. In the literature, a lot of work has been proposed to over-approximate the InterDyck -reachability formulation. This article offers a new perspective on improving both the precision and the scalability of InterDyck -reachability: we aim at simplifying the underlying input graph G . Our key insight is based on the observation that if an edge is not contributing to any InterDyck -paths, we can safely eliminate it from G . Our technique is orthogonal to the InterDyck -reachability formulation and can serve as a pre-processing step with any over-approximating approach for InterDyck -reachability. We have applied our graph simplification algorithm to pre-processing the graphs from a recent InterDyck -reachability-based taint analysis for Android. Our evaluation of three popular InterDyck -reachability algorithms yields promising results. In particular, our graph-simplification method improves both the scalability and precision of all three InterDyck -reachability algorithms, sometimes dramatically.
@article{paperbot1617,
title = {Fast Graph Simplification for Interleaved-Dyck Reachability},
author = {Yuanbo Li and Qirun Zhang and Thomas Reps},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {2},
year = {2022},
doi = {10.1145/3492428}
}