Technisches Resümee: Inferenz der Form von Data Frames in R-Programmen mittels abstrakter Interpretation

Problemstellung

Data Frames sind die grundlegende Datenstruktur für statistische Berechnungen und Datenanalysen in R. R ist jedoch eine dynamische Sprache, der es an statischen Garantien hinsichtlich der „Form“ von Data Frames mangelt (d. h. Spaltennamen, Anzahl der Spalten und Anzahl der Zeilen). Diese Dynamik erschwert das Nachvollziehen der Strukturen von Data Frames an spezifischen Punkten eines Programms, was zu subtilen Laufzeitfehlern führt, wie etwa dem Zugriff auf nicht existierende Spalten oder den Zugriff auf Zeilen außerhalb der Grenzen. Bestehende statische Analysewerkzeuge für Data Science konzentrieren sich entweder auf allgemeine Eigenschaften ohne Berücksichtigung von Form und Größe, oder sie sind auf Python (speziell die pandas-Bibliothek) beschränkt und wurden nicht an realem Code evaluiert. Zudem verlassen sich aktuelle R-spezifische Werkzeuge wie lintr auf syntaktische Muster und berücksichtigen weder Datenfluss noch Kontrollfluss, während flowR zwar Datenflussanalyse bietet, aber keine Mechanismen zur Inferenz der Datenform besitzt.

Methodik

Die Autoren schlagen eine neuartige statische Analyse bas sich auf abstrakter Interpretation vor, um die Form von Data Frames in R-Programmen zu inferieren. Der Ansatz umfasst die Definition eines abstrakten Domains, die Abbildung konkreter Operationen auf abstrakte Operationen und die Definition abstrakter Semantik, um Formeigenschaften durch die Programmausführung zu verfolgen.

1. Definition des abstrakten Domains

Die Autoren definieren den Data-Frame-Form-Domain ($\mathcal{DF}^\#$) als ein teilweise reduziertes Produkt-Domain, bestehend aus drei Sub-Domains:

• Spaltennamen ($\mathcal{N}^\#$): Modelliert mittels eines Set-Range-Domains. Die Spaltennamen eines Data Frames werden durch ein Paar $(A, B)$ repräsentiert, wobei $A$ die Menge der Spaltennamen ist, die existieren müssen (Minimalmenge) und $B$ die Menge der Spaltennamen ist, die existieren könnten (Maximalmenge).
• Anzahl der Spalten ($\mathcal{C}^\#$) und Zeilen ($\mathcal{R}^\#$): Modelliert mittels eines positiven Intervall-Domains $[a, b]$, wobei $a$ die untere Schranke und $b$ die obere Schranke (potenziell unendlich) ist.

Um die Präzision zu verbessern, führen die Autoren eine Reduktionsfunktion ($\rho_{\mathcal{DF}}$) ein, die das Produkt-Domain verfeinert. Wenn die inferierte Anzahl der Spalten (aus dem Intervall-Domain) mit der Größe der minimalen Spaltennamen-Menge übereinstimmt, wird die maximale Menge auf die minimale Menge reduziert. Umgekehrt werden die Spaltennamen-Mengen entsprechend angepasst, wenn das Spaltenanzahl-Intervall eingeschränkt wird.

2. Abstrakte Semantik und Operationen-Mapping

Die Analyse identifiziert die 20 am häufigsten verwendeten Data-Frame-Funktionen in R (z. B. data.frame, read.csv, filter, mutate, select) und bildet diese auf abstrakte Operationen ab.

• Erstellung: Funktionen wie data.frame und read.csv bilden auf eine create-Operation ab, welche die Spaltennamen-Mengen und Zeilen-/Spalten-Intervalle basierend auf den Argumenten initialisiert.
• Transformation:
  • filter bildet auf filterRows ab, was die Zeilenanzahl fundiert überapproximiert (potenziell die untere Schranke auf 0 reduzierend), während die Spaltennamen erhalten bleiben.
  • mutate bildet auf mutateCols ab, was neue Spaltennamen zur maximalen Menge hinzufügt und potenziell das Spaltenanzahl-Intervall erhöht.
  • select (oder subset) bildet auf subsetCols ab, was die aktuellen Spaltennamen-Mengen mit den ausgewählten Spalten schneidet und das Spaltenanzahl-Intervall anpasst.
• Zugriff: Spalten- und Zeilenzugriffe (via $, [ oder [[) werden auf accessCols und accessRows abgebildet. Die Analyse prüft, ob der aufgerufene Name oder Index innerhalb der inferierten abstrakten Form liegt.

Die Analyse ist als Visitor auf dem Kontrollflussgraphen (CFG) implementiert, der durch flowR, einen statischen Datenflussanalysator für R, generiert wird. Sie führt eine Fixpunkt-Iteration mit verzögertem Widening an Loop-Heads durch, um die Terminierung zu gewährleisten. Für Data Frames, die aus externen Dateien (z. B. CSV) gelesen werden, versucht die Analyse, konkrete Forminformationen aus den Datei-Headern und Inhalten zu extrahieren, sofern diese Dateien lokal verfügbar sind.

Kernbeiträge

1. Formale Definition: Eine formale Definition eines abstrakten Domains für Data-Frame-Formen unter Verwendung eines teilweise reduzierten Produkts aus Set-Ranges und Intervallen.
2. Implementierung: Eine begleitende Implementierung basierend auf flowR, die eine Linter-Regel enthält, um ungültige Data-Frame-Zugriffe zu melden (z. B. Zugriff auf eine Spalte, die durch eine vorangehende select-Operation entfernt wurde).
3. Evaluierung auf realem Code: Der erste Ansatz zur Analyse von Data-Frame-Formen in R, der auf einem großen Datensatz realer Skripte evaluiert wurde, womit über Proof-of-Concept-Evaluierungen auf synthetischem Code hinausgegangen wird.

Ergebnisse

Die Autoren evaluierten den Ansatz auf zwei Datensätzen:

1. Korrektheits-Evaluierung (78 Skripte):

   • Die Analyse identifizierte erfolgreich 72 % der tatsächlichen Data-Frame-Variablen.
   • Soundness (Korrektheit): Die Analyse hat die tatsächliche Form nie unterapproximiert (d. h. sie behauptete nie, eine Spalte existiere, obwohl sie nicht existierte, oder eine Zeilenanzahl sei niedriger als die Realität).
   • Präzision: 8 % der detektierten Data Frames wiesen exakte Form-Übereinstimmungen auf. 92 % waren Überapproximationen (meist top oder unendliche Schranken), was bei dynamischen Filter-Operationen, bei denen die exakte Zeilenanzahl von Laufzeitwerten abhängt, zu erwarten ist.

2. Effektivitäts-Evaluierung (33.314 Skripte):

   • Constraint-Inferenz: Die Analyse inferierte konkrete (nicht-top) Form-Constraints für 42,1 % der Data-Frame-Operationen und exakte Formen für 0,9 %.
   • Einfluss der Datenverfügbarkeit: Wenn alle von den Skripten gelesenen Datensätze lokal verfügbar waren, verbesserten sich diese Zahlen auf 5,8,7 % (konkret) und 4,2 % (exakt).
   • Fehlererkennung: Die Analyse identifizierte 40 Skripte, die potenzielle ungültige Data-Frame-Zugriffe enthalten (z. B. Zugriff auf eine Spalte, die durch eine vorherige Operation entfernt wurde). Obwohl viele Meldungen aufgrund nicht unterstützter Edge-Cases (z. B. Platzhalter in Pipes) False Positives waren, repräsentieren die 40 Skripte potenzielle reale Bugs.
   • Performance: Die durchschnittliche Gesamtlaufzeit pro Skript betrug 826 ms (Median 456 ms), wobei der Schritt der Form-Inferenz im Durchschnitt 163 ms dauerte. Diese Performance wird als ausreichend für die interaktive Nutzung erachtet.

Bedeutung und Ansprüche

Das Paper behauptet, empirische Belege dafür zu liefern, dass die Form von Data Frames in realen R-Programmen mittels abstrakter Interpretation sound inferiert werden kann. Die Bedeutung liegt in:

• Statischen Garantien: Eine Möglichkeit zu bieten, über die Formen von Data Frames in einer dynamischen Sprache nachzudenken, was potenziell Laufzeitfehler vor der Ausführung verhindert.
• Praktischer Nutzen: Der Nachweis, dass die Analyse im großen Maßstab auf realen Forschungs-Code angewendet werden kann, wobei sie für einen signifikanten Teil der Operationen konkrete Form-Constraints identifiziert.
• Fundament für zukünftige Werkzeuge: Die inferierten Formen können als statische Verträge für Data-Science-Code dienen, was Aufgaben wie die Ableitung von Vorbedingungen für externe Inputs, die Optimierung von Datentransformationen und eine präzisere Inhaltsanalyse unterstützt.

Die Autoren bleiben bescheiden hinsichtlich der Präzision der Zeilenanzahl-Inferenz (oft überapproximiert aufgrund von Filtern) und räumen Einschränkungen beim Umgang mit benutzerdefinierten Funktionen und bestimmten dynamischen Merkmalen ein, was sie als Möglichkeiten für zukünftige Arbeiten darstellen.