DA: Entwurf und Implementierung einer Bibliothek für Abstrakte Interpretation

Abstrakte Interpretationen ermöglichen die Feststellung von Programmeigenschaften zur Übersetzungszeit und bilden somit eine Grundlage für verbesserte Codeerzeugung in Compilern. Bei der Entwicklung eines konkreten Compilers muß somit die Abstrakte Interpretation als logische Phase integriert werden. Dabei sind mehrere Ziele erstrebenswert: Einerseits soll die Umsetzung in möglichst einfacher und portabler Weise geschehen, um Modifikationen und Erweiterungen der Ausgangssprache gegenüber flexibler zu sein. Andererseits soll eine gute Effizienz erreicht werden können, damit der Übersetzungsprozeß nicht übermäßig verlangsamt wird. Darüberhinaus ist es wünschenswert, wiederverwertbare Teile zu identifizieren, die von der konkreten Quellsprache und/oder der konkreten Abstrakten Interpretation unabhängig sind. Solche Komponenten können dann in anderen Compilern oder bei anderen Abstrakten Interpretationen erneut Verwendung finden.

Es liegt daher nahe eine allgemeine Bibliothek zu entwerfen, die es ermöglicht eine (möglichst große) Klasse von Abstrakten Interpretationen in Compilern zu integrieren. Diese Bibliothek sollte die Darstellung der Abstrakten Werte und Funktionen sowie die Berechnung der Fixpunktes verkapseln und somit einen sicheren Wechsel von Darstellung und Algorithmen erlauben. Damit wäre es möglich mit verschiedenen allgemeinen Ansätzen zur Effizienzsteigerung wie etwa BDDs [Mau94], chaotische Fixpunktberechnung [CC92,VWL94] oder Frontiers [HH91] zu experimentieren.

In dieser Arbeit soll nun eine solche Bibliothek entworfen und implementiert werden. Dabei soll zunächst von endlichen Bereichen mit Bitvektordarstellung ausgegangen werden, womit insbesondere die Halbordnungen als bitweiser Vergleich festgelegt sind. Desweiteren sollen zunächst nur monomorphe Abstrakte Interpretationen betrachtet werden. Für den weiteren Aufbau einer Abstrakten Interpretation sollte die Bibliothek Möglichkeiten enthalten den strukturellen Aufbau von Termen und Funktionen nachzubilden. Als Fallbeispiel soll zumindest die Abstrakte Interpretation zur Ermittlung von Vererbungsinformationen aus [Moh95b,Moh95a] mit Hilfe der Bibliothek implementiert werden. Allerdings soll eine generelle Benutzbarkeit der Bibliothek angestrebt werden.

Mögliche Erweiterungen wären der Übergang zu endlichen Bereichen mit komplexeren Halbordnungen oder polymorphen Funktionen.

In dieser Diplomarbeit sind nun die folgenden Punkte zu bearbeiten:

• Entwurf und Implementierung einer Bibliothek,
• Untersuchung von alternativen Implementierungstechniken, insbesondere internen Darstellungen und Fixpunktalgorithmen,
• Untersuchung der Effizienz,
• zumindest Anwendung der Ergebnisse auf die Abstrakte Interpretation aus [Moh95b,Moh95a]. Ein weiteres Anwendunggebiet könnte die Uniqueness-Analyse aus [DS95] oder [Kuc95] sein.