声明式程序分析中的通用可扩展性（基于选择的组合剪枝）
软件工程
2025-03-11 v1
摘要
在本工作中，我们针对该问题提出了一种简单、统一且优雅的解决方案，具有惊人的实际有效性，且适用于几乎任何基于 Datalog 的分析。该方法利用了现代 Datalog 引擎（如 Soufflé）原生支持的 choice 构造。choice 构造允许在关系中定义函数依赖，并在过去被用于表达工作列表算法。我们展示了一种近乎通用的构造，允许 choice 构造灵活地限制谓词的求值。该技术适用于几乎任何可以想象的分析架构，因为当关系的（程序员控制的）投影超过所需基数时，它会自适应地剪枝求值结果。我们将该技术应用于现存可能最大的既有 Datalog 分析框架：Doop（用于 Java 字节码）和 Gigahorse 框架的主要客户端分析（用于以太坊智能合约）。无需理解现有的分析逻辑且仅需极少的局部修改，每个框架的性能都得到了显著提升，对于最困难的输入提升超过 20 倍，而完整性的牺牲几乎可以忽略不计。
引用
@article{arxiv.2503.05945,
title = {Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)},
author = {Anastasios Antoniadis and Ilias Tsatiris and Nevill Grech and Yannis Smaragdakis},
journal= {arXiv preprint arXiv:2503.05945},
year = {2025}
}