一句话：提出 Loupe，用图神经网络从程序图表征端到端学习抽象解释中的循环展开启发式，减少误报并提升分析性能。
基于抽象解释的静态程序分析器依赖循环展开等提升精度的技术来减少误报，但其计算开销要求精心设计的选择性应用启发式。手工设计这类启发式既困难又易错，还可能导致状态爆炸。本文提出 Loupe，一种端到端自动学习静态分析循环展开启发式的新方法。与以往的数据驱动方法不同，Loupe 采用图神经网络（GNN）直接从基于图的程序表示中学习；为支持监督学习，它利用静态分析器自身自动标注训练数据。作者在开源 C 静态分析器 Frama-C/EVA 上实现了 Loupe，实验表明最佳启发式（GINE）在真实程序上优于 Frama-C/EVA 内置启发式，将误报减少 1.5 倍，同时将分析性能提升 56%。值得注意的是，GINE 能准确预测 Frama-C/EVA 专家工程师的循环展开决策，并保持可接受的假阳性率。最后，作者还展示了 Loupe 能有效为 MOPSA 等其他静态分析器学习启发式。
While static program analyzers based on abstract interpretation implement precision-improving techniques to reduce false alarms, such as loop unrolling, their computational cost requires carefully devised heuristics for selective application. Manually designing such heuristics is non-trivial and error-prone, possibly leading to state explosion.This paper presents LOUPE, a novel end-to-end approach for automatically learning loop unrolling heuristics for static program analysis. Unlike previous data-driven methods, LOUPE leverages Graph Neural Networks (GNNs) to learn directly from graph-based program representations. To enable supervised learning, we use the static analyzer itself to automatically label training data. We implement LOUPE on top of FRAMA-C/EVA, an open source C static analyzer, and demonstrate that the best performing heuristic (GINE) outperforms the FRAMA-C/EVA built-in heuristic on real-world programs, reducing false alarms by 1.5x while improving analysis performance by 56%. Remarkably, GINE accurately predicts loop unrolling decisions made by expert FRAMA-C/EVA engineers, while maintaining acceptable false-positive rates. Finally, we show that LOUPE can effectively learn heuristics for other static analyzers such as MOPSA.
@inproceedings{paperbot9414,
title = {Loupe: End-to-End Learning of Loop Unrolling Heuristics for Abstract Interpretation},
author = {Maykel Mattar and Michele Alberti and Valentin Perrelle and Salah Sadou},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00032}
}