通过选择性扩展实现高效的抽象解释

《Proceedings of the ACM on Programming Languages》：Efficient Abstract Interpretation via Selective Widening

抽象解释中基于值流循环的宽泛算子选择性优化方法，通过构建模块化值流图(MVFG)识别程序间参与值流循环的变量，仅对产生无限上升链的变量应用宽泛算子。实验表明该方法在保持分析精度的同时，减少宽泛变量数量达99.5%，且分析时间降低41.2%，尤其在大规模代码库中效果显著。

　　

摘要

抽象解释为静态分析提供了一个系统化的框架，在该框架中，扩展操作对于确保在分析无限高度格状结构上的程序时能够终止分析至关重要。当前的抽象解释器在所有被识别为需要扩展的变量（例如控制流循环头）上统一应用扩展操作和不动点检测，这导致了计算成本的增加。通过我们的实证研究，我们发现无限上升链通常仅源自参与值流循环的一部分变量，这为选择性扩展和有针对性的不动点检测提供了机会。本文介绍了一种通过基于值流分析的选择性扩展来优化非关系型域上的抽象解释的方法。我们开发了一种模块化且紧凑的值流图（MVFG），该图能够通过检测跨过程边界的值流循环来精确识别需要扩展的变量。我们的MVFG设计包含了高效的快捷边，这些快捷边总结了过程间的值流，实现了上下文敏感分析的精确性，同时保持了线性复杂度。通过将值流循环与控制流图的弱拓扑排序（WTO）对齐，我们识别出了需要扩展操作的最小变量集，并仅对参与值流回边的变量应用扩展操作。我们在大规模开源项目上的评估表明，我们的选择性扩展方法将分析时间减少了多达41.2%，同时保持了相同的精确性。该方法还将需要扩展的变量数量减少了多达99.5%，在更大的代码库中观察到了更大的效益。