Скачать или смотреть [OOPSLA'25] Universal Scalability in Declarative Program Analysis (with Choice-Based Combination(…)

Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning) (Video, OOPSLA2 2025)
Anastasios Antoniadis, Ilias Tsatiris, Neville Grech, and Yannis Smaragdakis
(University of Athens, Greece; Dedaub, Greece; University of Malta, Malta / Dedaub, Malta; University of Athens, Greece / Dedaub, Greece)

Abstract: 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 Souffle. 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: https://doi.org/10.1145/3763129

Supplementary archive: https://doi.org/10.5281/zenodo.15723754 (Badges: Artifacts Available, Artifacts Evaluated — Functional, Results Reproduced)

ORCID: https://orcid.org/0009-0004-1605-967X, https://orcid.org/0000-0002-1788-053X, https://orcid.org/0000-0002-6790-2872, https://orcid.org/0000-0002-0499-0182

Video Tags: Static analysis, program analysis, logic programming, datalog, optimization, oopslab25main-p613-p, doi:10.1145/3763129, doi:10.5281/zenodo.15723754, orcid:0009-0004-1605-967X, orcid:0000-0002-1788-053X, orcid:0000-0002-6790-2872, orcid:0000-0002-0499-0182, Artifacts Available, Artifacts Evaluated — Functional, Results Reproduced

Presentation at the OOPSLA2 2025 conference, October 13–15, https://2025.splashcon.org/track/OOPSLA
Sponsored by ACM SIGPLAN,