Korrekte, Effiziente und Flexible Fixpunkt-Algorithmen für Big-Step Abstrakte Interpreter

• Antragsteller: Professor Dr. Sebastian Erdweg
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung seit 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 451545561

Statische Programmanalysen untersuchen Quelltext und sind entscheidend für die Generierung von Programmier-Feedback, für die Validierung von Korrektheitseigenschaften, sowie für die Aktivierung von Compileroptimierungen. Bislang wurden korrekte („sound“) Analysen häufig als small-step abstrakte Interpreter definiert, wobei die abstrakte Semantik als Zustandsübergangssystem beschrieben wird. Der PI und andere Wissenschaftler haben kürzlich untersucht, wie sich abstrakte Interpreter im big-step Stil beschreiben lassen, wobei die abstrakte Semantik einfach als rekursive Funktion in einer Metasprache wie Haskell erstellt wird. Dies vereinfacht sowohl die Definition als auch die Wartung von big-step abstrakten Interpretern. Die Skalierbarkeit von abstrakten Interpretern hängt allerdings von deren Fixpunkt-Algorithmus ab. Leider sind existierende Fixpunkt-Algorithmen von small-step abstrakten Interpretern nicht auf big-step abstrakte Interpreter übertragbar, sodass es zurzeit keine effizienten big-step Fixpunkt-Algorithmen gibt.In diesem Projekt werden wir eine Familie von Fixpunkt-Algorithmen für big-step abstrakte Interpreter entwickeln. Um die Terminierung zu gewährleisten müssen die Fixpunkt-Algorithmen neue Herausforderungen bewältigen die für die big-step Auswertung spezifisch sind. Neben der Terminierung werden wir drei wichtige Belange adressieren. Erstens müssen unsere Fixpunk-Algorithmen korrekt sein und den kleinsten, meist unberechenbaren Fixpunkt überapproximieren. Wir werden die formale Theorie von big-step Fixpunk-Algorithmen erforschen um damit die Korrektheit beweisbar zu machen. Zweitens müssen unsere Fixpunkt-Algorithmen effizient sein und die Skalierung von Analysen auf realistische Softwaresysteme ermöglichen. Dazu werden die Anwendung unserer Algorithmen auf interprozedurale Java Bytecode Analysen erkunden, wobei wir davon ausgehen, dass die Performanz des initialen Designs unzureichend ist. Um diese Engpässe zu überwinden müssen unsere Fixpunkt-Algorithmen, drittens, flexibel sein, sodass Analyseentwickler auswählen können wie sie Präzision und Performanz abwägen möchten. Dazu werden wir erforschen wie big-step Fixpunkt-Algorithmen Kontextsensitivität und Method-Summaries unterstützen können. Durch das Design von effizienten, korrekten und flexiblen big-step Fixpunkt-Algorithmen wird dieses Projekt die Entwicklung von leicht verständlichen und gut skalierbaren big-step abstrakten Interpretern ermöglichen.

• DFG-Verfahren: Sachbeihilfen