一句话：用图神经网络从 Datalog 求解计算构图并为抽象参数打分，缩减 CEGAR 约束求解空间，提升大规模程序分析的可扩展性。
反例引导的抽象精化（CEGAR）能以高精度与低时间开销自动选择抽象，但现有方法将其转化为约束求解问题，问题复杂导致难以扩展到大型程序或复杂分析。本文提出一种新方法：直接从 Datalog 求解器的计算过程构建图，再用图神经网络依据图中的信息为抽象参数打分；随后改写约束问题，使约束求解器忽略低分参数，从而缩小解空间与约束规模。由于图直接从 Datalog 计算构造、无需人工介入，该方法可适用于用 Datalog 实现的各类参数化静态分析。作者在指针分析与 typestate 分析上评估，在大型程序上分别比基线多回答 2.83 倍与 1.5 倍的查询。
Counterexample-guided abstraction refinement (CEGAR) is a popular approach for automatically selecting abstractions with high precision and low time costs. Existing works cast abstraction refinements as constraintsolving problems. Due to the complexity of these problems, they cannot be scaled to large programs or complex analyses. We propose a novel approach that applies graph neural networks to improve the scalability of CEGAR for Datalog-based program analyses. By constructing graphs directly from the Datalog solver’s calculations, our method then uses a neural network to score abstraction parameters based on the information in these graphs. Then we reform the constraint problems such that the constraint solver ignores parameters with low scores. This in turn reduces the solution space and the size of the constraint problems. Since our graphs are directly constructed from Datalog computation without human effort, our approach can be applied to a broad range of parametric static analyses implemented in Datalog. We evaluate our approach on a pointer analysis and a typestate analysis and our approach can answer 2.83× and 1.5× as many queries as the baseline approach on large programs for the pointer analysis and the typestate analysis, respectively.
@article{YanZD24,
title = {Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural Networks},
author = {Zhenyu Yan and Xin Zhang and Peng Di},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689765}
}