Titelaufnahme
Titelaufnahme
- TitelScalable data-flow analysis through sparsification and precise call graphs / Kadiray Karakaya ; Advisor Prof. Dr. Eric Bodden
- Autor
- Gutachter
- Erschienen
- Umfang1 Online-Ressource (xi, 117 Seiten) : Illustrationen, Diagramme
- Hochschulschriftkumulative Dissertation Universität Paderborn, Dissertation, 2025
- AnmerkungTag der Verteidigung: 05.11.2025
- Verteidigung2025-11-05
- SpracheEnglisch
- DokumenttypDissertation
- Schlagwörter (GND)
- URN
- DOI
Links
- Social MediaShare
- Nachweis
- IIIF
Dateien
Klassifikation
Zusammenfassung
Die statische Datenflussanalyse zielt darauf ab, fehlerfreie, sichere und hochwertige Software zu gewährleisten, indem sie alle möglichen Ausführungen eines Zielprogramms berücksichtigt. Aufgrund von Skalierbarkeitsbeschränkungen führt dies häufig zu starken Überapproximationen, die die Präzision der Analyse beeinträchtigen. Andererseits verbessert Sparsifizierung, eine Optimierungstechnik, die Daten-flussanalysen auf analysenrelevante Programmstatements beschränkt, die Skalierbarkeit der Datenflussanalyse und bewahrt gleichzeitig deren Präzision.Diese Arbeit stellt SPARSEIDE vor, ein neuartiges Framework, das eine (Datenfluss-)Fakt-spezifische Sparsifizierung für jede Datenflussanalyse realisiert, die im IDE-Framework (Interprocedural Distributive Environments) realisiert wird. ObwohlIDE-Analysen nur in Bezug auf Symbole und nicht auf Werte sparsifiziert werdenkönnen, erzielt SPARSEIDE deutlich geringere Laufzeiten und einen geringeren Spe-icherverbrauch als das ursprüngliche IDE.Ansätze zur Verbesserung der Skalierbarkeit aus der Literatur, darunter SPARSEIDE,verwenden einen festen Call-Graph-Algorithmus, ohne dessen Auswirkungen auf die nachgelagerte Datenflussanalyse zu berücksichtigen. Anhand einer umfassendenempirischen Bewertung zeigt diese Arbeit, wie präzise kontextsensitive Call-Graphendie Laufzeiten der Datenflussanalyse erheblich reduzieren.Präzise Datenflussanalysen analysieren den Heap anhand von Pointer-Analysen, die ebenfalls schwer zu skalieren sind. Diese Arbeit stellt SPARSEBOOMERANG als Anwendung der Fakt-spezifischen Sparsifizierung auf die bedarfsorientierte Pointersanalyse vor. SPARSEBOOMERANG realisiert zwei verschiedene Sparsifizierung-Strategien,die die Eigenschaften der Pointeranalyse-Domäne nutzen: eine type-aware Sparsifizierung und eine alias-aware Sparsifizierung. Interprocedural Datenflussanalysen umfassen einen Datenfluss-Solver, einen Call-Graph und eine Pointer-Analyse. Diese Arbeit zeigt, wie präzise Datenflussanalysen skaliert werden können, indem alle drei Komponenten unter dem Gesichtspunkt der Sparsifizierung betrachtet werden. Eine Fakt-spezifische Sparsifizierung reduziert die Arbeitslast des Datenfluss-Solvers. Als orthogonale Komponente hat die Wahl des Call-Graphen einen erheblichen Einfluss auf die Skalierbarkeit der Datenflussanalyse.Die Pointer-Analyse, die bekanntermaßen ein nicht-distributives Problem darstellt,profitiert ebenfalls von einer Fakt-spezifischen Sparsifizierung, wenn sie innerhalb eines distributiven Datenflussanalyse-Frameworks formuliert wird.
Abstract
Static data-flow analysis aims to ensure bug-free, secure, and quality software by accounting for all possible executions of a target program. Due to scalability constraints, this often entails sound over-approximations that compromise analysis precision. On the other hand, sparsification, an optimization technique that restricts data-flow analyses to analysis-relevant program statements, improves scalability while at the same time maintaining precision. This thesis presents SPARSEIDE, a novel framework that realizes (data-flow) fact-specific sparsification for any data-flow analysis that fits the IDE (Interprocedural Distributive Environments) framework. Although IDE analyses can only be sparsified with respect to static symbols and not dynamic values, SPARSEIDE yields significantly lower runtimes and memory consumptions than the original IDE framework. Scalability-improving approaches from the literature, including SPARSEIDE, use a fixed call-graph algorithm, without considering its impact on the downstream data-flow analysis. Through extensive empirical evaluation, this thesis shows how precise context-sensitive call graphs significantly reduce data-flow analysis runtimes. Precise data-flow analyses reason about the heap through pointer analyses, which are also hard to scale. This thesis also presents SPARSEBOOMERANG as an application of fact-specific sparsification to demand-driven pointer analysis. SPARSEBOOMERANG realizes two different sparsification strategies that exploit the characteristics of the pointer analysis domain: a type-aware sparsification and an alias-aware sparsification. Interprocedural data-flow analyses comprise a data-flow solver, a call graph, and a pointer analysis. This thesis shows how to scale precise data-flow analyses by considering all three components from the perspective of sparsification. Fact-specific sparsification reduces the data-flow solver’s workload. As an orthogonal component, the choice of call graph significantly influences data-flow analysis scalability. Pointer analysis, which is known to be a non-distributive problem, also benefits from fact-specific sparsification when formulated within a distributive data-flow analysis framework.
Inhalt
Lizenz-/Rechtehinweis
