Loupe: End-to-End Learning of Loop Unrolling Heuristics for Abstract Interpretation

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.