一句话：利用 Datalog 的 choice 构造自适应剪枝关系投影，使既有声明式程序分析框架在几乎不损失完备性下大幅加速。
Datalog 的不动点求值让静态程序分析获得声明式、易维护且高性能的规约，但自底向上求值会计算所有推论，导致最坏情况下结果爆炸，即使部分答案已经足够也会使分析难以扩展。本文提出一种简单、统一且通用的解决方案：利用现代 Datalog 引擎（如 Soufflé）原生支持的 choice 构造，在关系投影超过程序员指定基数时自适应剪枝谓词求值；该构造此前用于表达函数依赖与 worklist 算法。作者将技术应用于 Doop（Java 字节码）和 Gigahorse（以太坊智能合约）的主要客户端分析，无需理解原有分析逻辑，仅做局部修改，在最难输入上获得超过 20 倍加速，完备性损失近乎可忽略。
Datalog engines for fixpoint evaluation have brought great benefits to static program analysis over the past decades. A Datalog specification of an analysis allows a declarative, easy-to-maintain specification, without sacrificing performance, and indeed often achieving significant speedups compared to hand-coded algorithms. However, these benefits come with a certain loss of control. Datalog evaluation is bottom-up, meaning that all inferences (from a set of initial facts) are performed and all their conclusions are outputs of the computation. In practice, virtually every program analysis expressed in Datalog becomes unscalable for some inputs, due to the worst-case blowup of computing all results, even when a partial answer would have been perfectly satisfactory. In this work, we present a simple, uniform, and elegant solution to the problem, with great practical effectiveness and application to virtually any Datalog-based analysis. The approach consists of leveraging the choice construct, supported natively in modern Datalog engines like Soufflé. The choice construct allows the definition of functional dependencies in a relation and has been used in the past for expressing worklist algorithms. We show a near-universal construction that allows the choice construct to flexibly limit evaluation of predicates. The technique is applicable to practically any analysis architecture imaginable, since it adaptively prunes evaluation results when a (programmer-controlled) projection of a relation exceeds a desired cardinality. We apply the technique to probably the largest, pre-existing Datalog analysis frameworks in existence: Doop (for Java bytecode) and the main client analyses from the Gigahorse framework (for Ethereum smart contracts). Without needing to understand the existing analysis logic and with minimal, local-only changes, the performance of each framework increases dramatically, by over 20x for the hardest inputs, with near-negligible sacrifice in completeness.
@article{paperbot2941,
title = {Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)},
author = {Anastasios Antoniadis and Ilias Tsatiris and Neville Grech and Yannis Smaragdakis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763129}
}