KIT | KIT-Bibliothek | Impressum | Datenschutz

Incremental Whole-Program Analysis in Datalog with Lattices

Szabó, Tamás; Erdweg, Sebastian ORCID iD icon 1; Bergmann, Gábor
1 Institut für Programmstrukturen und Datenorganisation (IPD), Karlsruher Institut für Technologie (KIT)

Abstract (englisch):

Incremental static analyses provide up-to-date analysis results in time proportional to the size of a code change, not the entire code base. This promises fast feedback to programmers in IDEs and when checking in commits. However, existing incremental analysis frameworks fail to deliver on this promise for whole-program lattice-based data-flow analyses. In particular, prior Datalog-based frameworks yield good incremental performance only for intra-procedural analyses. In this paper, we first present a methodology to empirically test if a computation is amenable to incrementalization. Using this methodology, we find that incremental whole-program analysis may be possible. Second, we present a new incremental Datalog solver called LADDDER to eliminate the shortcomings of prior Datalog-based analysis frameworks. Our Datalog solver uses a non-standard aggregation semantics which allows us to loosen monotonicity requirements on analyses and to improve the performance of lattice aggregators considerably. Our evaluation on real-world Java code confirms that LADDDER provides up-to-date points-to, constant propagation, and interval information in milliseconds.


Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Publikationsdatum 18.06.2021
Sprache Englisch
Identifikator ISBN: 978-145038391-2
KITopen-ID: 1000188601
Erschienen in Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI); Online, 20.-25.06.2021
Veranstaltung 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (2021), Online, 20.06.2021 – 25.06.2021
Verlag Association for Computing Machinery (ACM)
Seiten 15 S.
Schlagwörter Datalog; Incremental Computing; Static Analysis
Nachgewiesen in Scopus
KIT – Die Universität in der Helmholtz-Gemeinschaft
KITopen Landing Page