声明式程序分析中的通用可扩展性（基于选择组合剪枝技术）

《Proceedings of the ACM on Programming Languages》：Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)

Datalog引擎在静态程序分析中的应用及其优化，通过引入choice构造限制谓词评估，动态剪枝提升Doop（Java）和Gigahorse（以太坊）框架性能达20倍以上，保持高完整性。

　　

摘要

在过去几十年中，用于固定点计算的Datalog引擎为静态程序分析带来了巨大的好处。使用Datalog进行程序分析可以编写出声明性强、易于维护的规范，同时不会牺牲性能，实际上通常比手工编写的算法更快。

然而，这些好处也伴随着一定程度的控制权丧失。Datalog的计算是自底向上的，这意味着所有推理（从一组初始事实开始）都会被执行，并且所有推理结果都是计算的输出。实际上，几乎所有用Datalog表示的程序分析在面对某些输入时都会变得不可扩展，因为需要计算所有结果，即使部分答案就已经足够满足需求。

在这项工作中，我们提出了一种简单、统一且优雅的解决方案，具有很高的实际效果，几乎可以应用于任何基于Datalog的分析。该方法利用了现代Datalog引擎（如Souffle）中内置的“选择”（choice）构造。这种构造允许在关系中定义函数依赖关系，并且过去曾被用于表达工作列表算法。我们展示了一种近乎通用的方法，使得“选择”构造能够灵活地限制谓词的评估范围。该技术适用于几乎所有可以想象的分析架构，因为它能够在关系经过（程序员控制的）投影后，根据所需的基数自动剪枝评估结果。

我们将该技术应用于目前存在的最大规模的Datalog分析框架：Doop（用于Java字节码）以及Gigahorse框架中的主要客户端分析（用于以太坊智能合约）。无需理解现有的分析逻辑，只需进行少量局部修改，每个框架的性能都得到了显著提升——对于最复杂的输入，性能提高了20倍以上，而完整性的损失几乎可以忽略不计。