In this work, we present a simple, uniform, and elegant solution to the problem, with stunning 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\'e. 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.

翻译：本文提出了一种针对该问题的简洁、统一且优雅的解决方案，其具有惊人的实际效能，并适用于几乎所有基于Datalog的分析。该方法的核心在于利用现代Datalog引擎（如Soufflé）原生支持的choice构造。choice构造允许在关系中定义函数依赖，过去曾用于表达工作列表算法。我们展示了一种近乎通用的构建方法，使得choice构造能够灵活地限制谓词的求值。该技术几乎可应用于任何可设想的分析架构，因为它能在关系（由程序员控制的）投影超过期望基数时，自适应地剪枝求值结果。我们将该技术应用于目前可能规模最大的既有Datalog分析框架：Doop（用于Java字节码）以及Gigahorse框架（用于以太坊智能合约）中的主要客户端分析。在无需理解现有分析逻辑且仅进行最小化局部修改的情况下，每个框架的性能均得到显著提升，对于最复杂的输入性能提高超过20倍，而完整性损失几乎可忽略不计。