Shape-Analyse

Inhaltsverzeichnis

1 Grundlagen
1.1 Zeiger und Objekte auf dem Heap
1.2 Ziele der Shape-Analyse

2 Logische Strukturen
2.1 2-wertige Strukturen
2.2 3-wertige Strukturen
2.3 Zusammengefasste Knoten
2.4 Formeln
2.5 Basis- und abgeleitete Prädikate
2.6 Einbettung

3 Durchführung der Shape Analyse
3.1 Operationelle und Abstrakte Semantik
3.2 Beschreibung von Eingaben und Programmen
3.3 Prozeß
3.3.1 Fokussieren
3.3.2 Vorbedingungen auswerten
3.3.3 Update-Formeln ausführen
3.3.4 Konsistenz prüfen
3.3.5 Zusammenfassen
3.4 Ergebnisse

4 Anwendung, Probleme und Ausblicke
4.1 Anwendungsgebiete
4.2 Kritik

Zusammenfassung

Datenstrukturen, die durch Zeiger aufgebaut sind, können durch die Gestalt charakterisiert werden, die sie an bestimmten Stellen im Pro­gramm besitzen. Die Shape Analyse versucht durch eine statische Un­tersuchung des Programms diese Strukturen auf dem Heap zu analy­sieren und zu beschreiben. Die Ergebnisse werden unter anderem bei der Programmverifikation und beim Debugging eingesetzt

1 Grundlagen

1.1 Zeiger und Objekte auf dem Heap

Zeiger sind ein sehr mächtiges, aber auch gefährliches Konstrukt in impe­rativen Sprachen. Es gibt relativ wenig Analysemethoden, die sich mit der Semantik von Zeigern auseinandersetzen, da Anweisungen die Zeiger bein­halten wesentlich komplexer werden. Ein Grund dafür ist, daß bei ihrer Ver­wendung oft weitreichende Seiteneffekte auftreten können.

Aber nicht nur die Pogrammanalyse und das Programmverständnis wird durch die Benutzung von Zeigern erschwert. Es treten auch leichter Fehler im Programm auf, beispielsweise durch das Dereferenzieren von NULL-Zeigern und den Zugriff auf bereits freigegebene Speicherzellen.

Viele Datenstrukturen wie Listen oder Bäume werden jedoch unter Zu­hilfenahme von Zeigern aufgebaut. Dazu allokieren imperative Programme beim Aufbau einer solchen Struktur Speicher für neue Zellen auf dem soge­nannten Heap. Zeiger in Programmvariablen, aus dem Stack und aus anderen Heap-Zellen verknüpfen die Elemente miteinander.

Dadurch erhält man einen semantischen Zusammenhang und kann von einer Gestalt (engl, shape) der Zellen sprechen. Abbildung 1 zeigt ein einfa­ches C-Programm, daß eine Liste invertiert, sowie den Datentyp Liste.

Abbildung in dieser Leseprobe nicht enthalten

Abbildung 1: Programm zum Invertieren einer Liste und Datentyp Liste

Die Datenstruktur, die dem Programm übergeben wird, ist eine einfach verkettete Liste. Um nun den Ablauf besser zu verstehen, würden wir gerne an bestimmten Stellen im Programm - insbesondere am Ende der Prozedur - wissen, wie der Zustand der Struktur auf dem Heap ist.

1.2 Ziele der Shape-Analyse

Für die Analyse sind folgende Fragen wichtig:

- Ist ein Zeiger ein NULL-Zeiger?
- Zeigen zwei Zeiger (evtl.) auf dieselbe Zelle? (engl. May-Alias)
- Zeigen zwei Zeiger immer auf dieselbe Zelle? (engl. Must-Alias)
- Können mehr als ein Zeiger auf eine Zelle zeigen? (engl. Sharing)
- Ist eine Zelle von einer bestimmtem Variable oder einer anderen Zelle aus erreichbar? (engl. Reachability)
- Sind zwei Datenstrukturen disjunkt? (engl. Disjointness)
- Kann eine Zelle Teil eines Zyklus sein? (engl. Cyclicity)

Die NULL-Zeiger Eigenschaft und die Möglichkeit, daß zwei Zeiger auf die gleiche Zelle zeigen können, sind wertvolle Debugging-Informationen. Die anderen Fragen sind wichtiger für das Programmverstehen oder liefern In­formationen für Garbage Collection und Parallelisierung.

Antworten auf diese Fragen will die Shape Analyse liefern. Durch das Verstehen der Gestalt der Datenstrukturen und das Bestimmen der mögli­chen Zustände an verschiedenen Programmpunkten, wird dies möglich. Das Verfahren berücksichtigt hierfür nicht, welche Ergebnisse ein Programm be­rechnet. Im vorliegenden Beispiel werden also die Einträge, die sich in den Datenfeldern der Listenelemente befinden, ignoriert.

An jedem Punkt in der Programmausführung, d.h. an jedem Knoten des Kontrollflußgraphen, wird eine Obermenge der möglichen Strukturen ermit­telt. Dazu benötigt man natürlich eine Beschreibung der möglichen Eingaben und eine Möglichkeit der Abbildung der Schritte, die das Programm auf die­sen Daten ausführt.

2 Logische Strukturen

Basis für die Shape Analyse sind 2- und 3-wertige logische Strukturen, die im folgenden kurz eingeführt werden sollen.

2.1 2-wertige Strukturen

Eine 2-wertige logische Struktur S besteht aus einer Menge von Symbolen Us, dem Universum, einer Menge von Prädikaten und einer Interpretation dieser Prädikate. Die Interpretation liefert die Wahrheitswerte 0 oder 1.

Beispiel 1 Sei Us = {x,y}· Zusammen mit einem Prädikat p, dessen Interpretation ps(x, y) z.B. gleich 1 ist, hat man also eine 2-wertige Struktur definiert

Das Prädikat im Beispiel ist 2-stellig. Allgemein kann man die Interpreta­tion ps eines Prädikats mit beliebiger Steifigkeit als eine Funktion folgender Art angeben: ps : (Us)k {0,1}

2-wertige Strukturen kann man nun benutzen, um Speicherzustände zu beschreiben, indem man den Prädikaten eine geeignete Bedeutung zuweist.

Beispiel 2 Für die Shape Analyse interessieren unter anderem folgende Eigenschaften:

- Zeigt Variable x auf Zelle v? Wir beschreiben dies durch das Prädikat x. Es gilt also: x(v) = 1, falls Variable x auf Zelle v zeigt.

- Zeigt die n-Komponente von v\ auf v-ι ? Hierfür verwenden wir das Prädikat n. Demnach: n(v 1,1*2) = 1, falls die Beziehung besteht.

Für die Shape Analyse genügt es, sich auf höchstens 2-stellige Prädikate zu beschränken. Diese kann man durch gerichtete Graphen darstellen. Die Symbole aus dem Universum werden zu Knoten der Graphen. 1-stellige Prä­dikate kann man nun in einem Knoten notieren, falls sie in der Struktur den Wert 1 besitzen, anderenfalls werden sie weggelassen. 2-stellige Prädikate werden zu gerichteten Kanten, wenn sie zu 1 ausgewertet werden. Der Name des Prädikats wird als Beschriftung an die Kante geschrieben.

Abbildung 2(a) zeigt eine einfach verkettete Liste, auf dessen erstes Ele­ment die Variable x zeigt. Diese Liste könnte eine Eingabe für das obige Programm darstellen.

Abbildung in dieser Leseprobe nicht enthalten

Abbildung 2: Einfach verkettete Liste

Zur Vereinfachung werden die Prädikate, die Variablen beschreiben, als eigene Kästchen dargestellt, wie es Abbildung 2(b) zeigt.

2.2 3-wertige Strukturen

Mit den bisherigen Möglichkeiten kann man zwar bereits Speicherstrukturen darstellen, aber es fehlt noch die Möglichkeit der Abstraktion. Listen mit drei Elementen werden anders dargestellt als solche mit vier Elementen, obwohl man unter Umständen für die Analyse auf diese Unterscheidung verzichten kann, bzw. muß, um die Analyse zu beschleunigen, oder überhaupt durch­führen zu können. Zu diesem Zweck wird die 3-wertige Logik von Kleene¹ benötigt.

Abbildung in dieser Leseprobe nicht enthalten

Die Menge der Wahrheitswerte wird um den Wert 1/2 erweitert, der un­bekannt bedeutet. Tabelle 1 zeigt die Erweiterung der logischen Operatoren Λ, V und -i.

Abbildung in dieser Leseprobe nicht enthalten

Tabelle 1: Erweiterung der logischen Operatoren

Beispiel 3 Die Interpretation x(v) = 1/2 bedeutet in unserem Beispiel also, daß nicht bekannt ist, ob Variable x auf Zelle v zeigt.

Die Werte 0 und 1 heißen definit, 1/2 indefinit. Die Darstellung erfolgt wiederum durch gerichtete Graphen analog zur 2-wertigen Darstellung. Inde­finite Werte werden durch gestrichelte Linien symbolisiert, sofern es sich um 2-stellige Prädikate handelt. Ein 1-stelliges Prädikat p, das in einen Knoten geschrieben wird, erhält die Bezeichnung p = 1/2.

2.3 Zusammengefasste Knoten

Knoten in einer 3-wertigen Struktur, die mehr als einen echten Knoten dar­stellen, werden als zusammengefasste Knoten (engl, summary nodes) be­zeichnet. Diese Eigenschaft wird durch das unäre Prädikat sm festgehalten. Nur Elemente, bei denen der Wert von sm 1/2 beträgt, können mehrere Kno­ten repräsentieren. In der graphischen Darstellung wird das Prädikat durch eine gestrichelte Umrandung verdeutlicht.

In Abbildung 3 ist cs ein solcher Knoten. Das Prädikat n kann nun keinen

Abbildung in dieser Leseprobe nicht enthalten

definiten Wert mehr erhalten, denn von der alten Zelle c-ι ging eine Kante zu сз, nicht aber umgekehrt. Die Schlinge, die man nun erhält, fasst diese beiden Fälle zusammen. Sie könnte aber auch bedeuten, daß in der dargestellten Struktur die Zellen, die in cs vereinigt sind, zyklisch verkettet sind. Mit der erhöhten Abstraktion geht demnach ein Verlust an Information einher. Die Entscheidung, welche Knoten zusammengefasst werden und welche nicht, ist
ein kritischer Punkt bei der Shape Analyse und hat Folgen für die Präzision aber auch für die Geschwindigkeit der Analyse ⁵.

2.4 Formeln

Mit Hilfe von logischen Formeln kann man nun Eigenschaften von Strukturen auswerten. Genauer werden logische Formeln erster Ordnung mit transitiver Überdeckung und Gleichheit, aber ohne Funktionssymbole verwendet⁴.

Beispiel 4 Die Formel 3ui : (x(vi) Λ n*(vi,v)) erlaubt Aussagen über die Erreichbarkeit von Knoten ausgehend von der Variable x. Angewendet auf einen Knoten v ergibt die Formel 1, falls v\ der Knoten ist, auf den x zeigt und v über 0 oder mehr n-Kanten von v\ aus erreichbar ist. n* ist die reflexive transitive Hülle des Prädikats n.

Eine Formel ist potentiell erfüllt, falls es eine Belegung gibt, mit der die Formel zu 1 oder 1/2 ausgewertet wird.

2.5 Basis- und abgeleitete Prädikate

Für die Shape Analyse unterteilt man Prädikate in zwei disjunkte Mengen: Basis- (engl, core) und abgeleitete (engl, instrumentation) Prädikate. Ba­sisprädikate sind Teil jeder Zeigersemantik. Sie machen grundsätzliche Aus­sagen über den Speicherzustand⁵. Die Prädikate x und n aus den obigen Beispielen sind Basisprädikate.

Abgeleitete Prädikate werden mit Hilfe von Formeln über Basisprädika­ten definiert. Jedes abgeleitete Prädikat besitzt solch eine definierende For­mel.

Beispiel 5 Das abgeleitete Prädikat r für die Erreichbarkeit wird durch die Formel aus dem letzten Beispiel festgelegt: r[n,x](v) -H- 3ui : (x(vi) Λ n*(vi,v))

Natürlich ist mit der Einführung von abgeleiteten Prädikaten eine gewis­se Redundanz verbunden, denn der Wert kann im Prinzip wieder durch die Anwendung der definierenden Formel bestimmt werden. Dies ist jedoch nicht der Fall, wenn mit 3-wertiger Logik und zusammengefassten Knoten gearbei­tet wird (vgl. Abschnitt 2.3). Abbildung 4 verdeutlicht diesen Sachverhalt. Wertet man die Formel für die Erreichbarkeit für den Knoten cs aus, so er­hält man den Wert 1/2. Da aber bekannt ist, daß in der ursprüglichen Liste alle Knoten von x aus erreichbar waren, kann man das abgeleitete Prädikat r auch explizit abspeichern und sichert sich somit genauere Informationen.

2.6 Einbettung

Es bleibt nun noch die Verknüpfung zwischen 2- und 3-wertiger Logik her­zustellen. Dies leistet die Einbettung. Eine Einbettung ist eine surjektive Funktion von einer 2-wertigen in eine 3-wertige Struktur, die jeder Inter­pretation eines Prädikats entweder den gleichen Wert oder 1/2 zuordnet.

Abbildung in dieser Leseprobe nicht enthalten

Weiter oben ist die Einbettung bereits intuitiv verwendet worden. Die Liste aus Abbildung 2(a) kann in die Liste mit dem zusammengefassten Knoten aus Abbildung 3 eingebettet werden.

Das Einbettungstheorem Das Einbettungstheorem besagt, daß jede Formel, die zu einem definiten Wert in einer 3-wertigen Struktur ausgewertet wird, denselben Wert in jeder eingebetteten Struktur liefert. Das Theorem ist die Grundlage für die Verwendung 3-wertiger Logik in der statischen Analyse: es stellt sicher, daß man Formeln, die interpretiert in 2-wertiger Logik die operationeile Semantik einer Anweisung definieren, in 3-wertiger Logik reinterpretieren darf³.

3 Durchführung der Shape Analyse

3.1 Operationelle und Abstrakte Semantik

Die operationeile Semantik ist intuitiv die formale Definition eines Interpre­ters für eine Anweisung. Ziel ist es, die operationeile Semantik eines Pro­gramms mit Hilfe der 2- bzw. 3-wertigen Logik zu beschreiben. Man verwen­det hierzu die oben eingeführten logischen Formeln.

Die abstrakte Semantik eines Programms ist die Zusammenfassung des Verhaltens auf einer unendlichen Menge von Speicherzuständen. Weiter oben wurde verdeutlicht, daß man diese durch Strukturen in 3-wertiger Logik ab­bilden kann. Das Einbettungstheorem liefert den Beweis, daß das Anwenden der Formeln eine konservative Approximation der operationeilen Semantik ist. Deutlicher heißt das, daß durch die Anwendung einer Formel auf eine 3-wertige Struktur eine neue Struktur entsteht, die wiederum alle 2-wertigen Strukturen enthält, die entstanden wären, wenn man die Formel auf die ur­sprünglichen 2-wertigen Strukturen angewendet hätte.

Die Approximation ist konservativ, d.h. daß eventuell Information über die Strukturen bei diesem Prozeß verlorengeht, aber daß niemals falsche Aus­sagen getroffen werden. Das Ergebnis der Analyse kann beispielsweise sein, daß eine Variable möglicherweise auf eine Zelle zeigt (das Prädikat nimmt den Wert 1/2 an), obwohl das nicht der Fall ist. Es kann jedoch nicht pas­sieren, daß die Analyse angibt, daß eine Referenzbeziehung besteht, wenn es nicht so ist.

Auf den Prozeß wird in den Abschnitten 3.2 und 3.3.3 näher eingegangen.

3.2 Beschreibung von Eingaben und Programmen

Das Verfahren der Shape Analyse wurde bereits in einem Prototypen namens TVLA implementiert, auf den sich die folgenden Beschreibungen stützen⁴. Das Programm ist unter http://www.math.tau.ac.il/~tla frei erhältlich.

Wie bereits erwähnt, benötigt man für die Analyse eine Beschreibung der möglichen Eingaben für ein Programm, die Definition der operationeilen Semantik und das Programm selbst. Abbildung 5 zeigt die Definition der einfach verketteten Liste mit mindestens zwei Elementen, die in Abbildung 4 dargestellt ist.

Abbildung in dieser Leseprobe nicht enthalten

Abbildung 5: Definition einer einfach verketteten Liste mit mindestens zwei Elementen

Für jede Anweisung, die im Programm vorkommt, muß die operationeile Semantik definiert werden. Abbildung 6 zeigt die Beschreibung der Zuwei­sung x = x —> n. Sie enthält die Signatur der Anweisung, eine sogenannte Fokus-Formel, die im Abschnitt 3.3.1 näher erläutert wird, und Formeln für die Modifikation der Prädikate. Diese werden Update-Formeln genannt und bilden die operationeile Semantik nach.

Abbildung in dieser Leseprobe nicht enthalten

Abbildung 6: Beschreibung der Anweisung x = x —> n

Im Beispiel geschieht bei Ausführung der Aktion folgendes. Zunächst wird der Effekt der Zeigerzuweisung nachgebildet: xl zeigt auf den Knoten, der der Nachfolger von x2 ist. Im Beispiel wird der Zeiger auf x also auf x —> n zeigen. Als nächstes werden die Erreichbarkeitsprädikate aktualisiert. Erreichbar von x aus sind nun alle Knoten, die vorher schon erreichbar waren. Ausnahme ist der Knoten auf den x ursprünglich gezeigt hat, es sei denn er liegt auf einem Zyklus.

3.3 Prozeß

Der Prozeß der Shape Analyse unterteilt sich in fünf Schritte. Sind alle Schrit­te für eine Anweisung durchgeführt, so folgt die nächste Programmanwei­sung. Dieses Verfahren wird so oft für das gesamte Programm iteriert, bis keine neuen Strukturen mehr hinzukommen.

3.3.1 Fokussieren

Der erste Schritt bei der Analyse ist das Fokussieren (engl, focus) der ge­gebenen Struktur anhand einer Formel. In Abbildung 6 ist sie durch das Schlüsselsymbol %f gekennzeichnet. Es entsteht eine Menge von 3-wertigen Strukturen, die die gleichen 2-wertigen Strukturen repräsentiert, wie die Ein­gabestruktur. Der Unterschied ist, daß auf den neuen Strukturen die gegebe­ne Fokus-Formel einen definiten Wert annimmt. Ein Algorithmus für diesen Schritt wird in⁷ beschrieben.

Abbildung in dieser Leseprobe nicht enthalten

Eine Struktur, die vor der Anweisung x = x —> n auftreten kann, ist in Abbildung 7 dargestellt. Es handelt sich um die erste Iteration im Verfahren, nachdem im Programm у = x gesetzt wurde.

Abbildung 8 zeigt das Ergebnis des Fokussierens für die schon oben be­schriebene Zuweisung. Es gibt drei mögliche Strukturen, in denen die Formel einen definiten Wert annimmt, (a) die n-Komponente von ci zeigt auf kei­nes der Elemente, die durch cs repräsentiert sind; (b) n zeigt auf alle diese Elemente; (c) n zeigt nur auf einen Teil der Elemente: Der Knoten cs wird aufgespalten.

Man beachte, daß man für die Referenzbeziehung zwischen cs.i und cs,i keine genauere Aussage machen kann, als daß beide aufeinander verweisen können. Dies resultiert aus der Schlinge am ursprünglichen Knoten cs.

Man erkennt, daß die erste Struktur aufgrund der Erreichbarkeitsinfor­mationen in cs unzulässig ist. Man könnte sie also bereits an dieser Stelle wieder verwerfen. Der Shape Analyse-Algorithmus führt dies aber erst bei der Konsistenzprüfung aus.

Abbildung in dieser Leseprobe nicht enthalten

а) Ь) с)

Abbildung 8: Ergebnis der Fokus-Operation

3.3.2 Vorbedingungen auswerten

Nach dem Fokussieren werden eventuelle Vorbedingungen ausgewertet. Wei­tere Aktionen werden nur ausgeführt, wenn die Formel potentiell erfüllt ist. Man hat damit die Möglichkeit Programmbedingungen nachzubilden. Im Beispiel kann man eine Vorbedingung verwenden, um die whi/e-Schleife zu modellieren.

3.3.3 Update-Formeln ausführen

Die operationeile Semantik einer Anweisung wird wie oben beschrieben durch eine Menge von sogenannten Up date-Formeln ausgedrückt, die die Verände­rungen der Prädikate bestimmen. Abbildung 9 verdeutlicht die Anwendung der in Abschnitt 3.2 vorgestellten Formeln für die Anweisung x = x —> n. Sie werden auf jede der drei Strukturen angewendet.

3.3.4 Konsistenz prüfen

Als letzter Schritt der eigentlichen Berechnung wird die Konsistenz geprüft. Er wird im englischen auch mit coerce bezeichnet. Mit Hilfe einer gegebenen Menge von Konsistenzregeln werden Strukturen, die wiedersprüchliche Ei­genschaften besitzen, verworfen. Die Konsistenzregeln können teilweise vom System selbst aus den abgeleiteten Prädikaten bestimmt werden⁷.

Im Beispiel ergeben sich einige Veränderungen (vgl. Abbildung 10). Die Struktur (a) kann verworfen werden, da cs aufgrund des Prädikats r von у aus erreichbar sein müsste.

Abbildung in dieser Leseprobe nicht enthalten

Abbildung 9: Ergebnis der Update-Operation

Um weitere Eigenschaften von Zeigern zu verwerten, verwendet man Me­thoden, die schon aus dem Datenbankbereich bekannt sind. So sind Zeiger, und damit die unären Prädikate im Beispiel, als unique deklariert, d.h. sie können nur auf ein Element zeigen. In der Struktur (b) muß deshalb cs ein echter Knoten sein und kann nicht den Wert 1 /2 für das Prädikat sm behal­ten. Das gleiche gilt für cs.i in Struktur (c).

Ein weiteres Prädikat, daß für die Analyse der Beispiels eingeführt wur­de, ist is ^shared. Es markiert Knoten, auf die mehrere Zeiger verweisen. Dies wäre beispielsweise bei doppelt verketteten Listen der Fall. In unserem Beispiel ist das Prädikat jedoch für alle Knoten 0, weshalb man noch die Schlingen für Knoten cs, bzw. cs.i in den beiden Strukturen und den Verweis von cs 2 auf cs.i in Struktur (c) eliminieren kann (vgl.⁴ ).

3.3.5 Zusammenfassen

Die Anzahl der möglichen Strukturen, die bei der Analyse entstehen kön­nen muß endlich sein, da das Verfahren anderenfalls nicht terminiert, wenn Programme Schleifen enthalten. Dafür gibt es eine Menge von sogenannten Abstraktionsprädikaten, die für das Zusammenfassen von Knoten verwen­det werden. Man kombiniert alle Knoten, deren Abstraktionsprädikate den gleichen Wert besitzen. Im einfachsten Fall sind alle unären Prädikate Ab­straktionsprädikate. Im Beispiel gibt sich hier keine Veränderung, da sich alle Knoten im Prädikat x, bzw. у unterscheiden.

Abbildung in dieser Leseprobe nicht enthalten

Abbildung 10: Ergebnis der Konsistenzüberprüfung

3.4 Ergebnisse

Das Verfahren wird nun so oft iterativ für das gesamte Programm wiederholt, bis die sich ergebenden Strukturen isomorph zu den vorhergehenden sind. Da die Anzahl der möglichen Strukturen durch die Abstraktionsprädikate begrenzt ist, terminiert das Verfahren³.

Im Beispiel wurde zusätzlich zu der bereits vorgegebenen Liste mit mehr als zwei Elementen noch eine einelementige Liste als möglich Eingabe ange­geben. Man erhält als Ergebnis, daß nach Ablauf des Programms y auf eine einfach verkettete Liste mit mindestens einem Element zeigt.

4 Anwendung, Probleme und Ausblicke

4.1 Anwendungsgebiete

Es gibt merere Anwendungsgebiete für die Shape Analyse, wobei die wich­tigsten wohl die Programmverifikation und das Debugging sind. Einer der größten Stolpersteine bei der Verifikation ist das Finden von Schleifeninvari­anten, wodurch eine endliche Repräsentation der Programme erreicht werden kann.

Bei der Shape Analyse entfällt diese Aufgabe. Es gelang mit der Sha­pe Analyse die partielle Korrektheit von Sortieralgorithmen zu überprüfen, indem man durch geeignete abgeleitete Prädikate sicherstellte, daß die resul­tierende Liste tatsächlich sortiert war³.

Interessant ist auch die Anwendung beim Debugging. In ³ werden ver­schiedene Szenarien anhand von Bubblesort und Insertion Sort durchgespielt. Informationen extrahiert man wiederum durch das Einführen neuer Prädi­kate. Durch die Verwendung eines Prädikats inorder kann man z.B. fehler­hafte Sortieralgorithmen erkennen. In der Ergebnisstruktur muß das inorder­Prädikat gleich 1 für alle Knoten sein. Ein inkorrekter Algorithmus, der das erste Element der Liste ignorierte konnte daran erkannt werden, daß in der Ergebnisliste inorder für das erste Element gleich 1 /2 war.

Ein Bubblesort-Algorithmus, bei dem der Test vor dem Vertauschen zwei­er Elemente nur auf < ausgeführt wird, terminiert nicht, sobald Listen mit gleichen Elementen als Eingabe verwendet werden. Ein abgeleitetes Prädi­kat datalsEqual, daß für diesen Fall eingeführt wurde, war nach der Analyse gleich 0 für alle Knoten, so daß auch dieses Problem erkannt werden kann. Ähnlich kann man testen, ob die Ergebnisstruktur eine Permutation der Aus­gangselemente enthält.

4.2 Kritik

Die Shape Analyse stellt eine sehr elegante Möglichkeit dar, Programme zu beschreiben, zu analysieren und zu verstehen. Im Gegensatz zur herkömmli­chen Verifikation kommt sie auch ohne Invarianten aus. Der Programmierer muß lediglich eine Beschreibung der Semantik des Programms liefern.

Es ist dennoch eine anspruchsvolle Aufgabe, die Semantik richtig durch Formeln zu beschreiben, und zu zeigen, daß die Formeln das Programm genau abbilden. Das größte Problem ist aber das Finden geeigneter abgeleiteter Prädikate. Sie haben einen sehr großen Einfluß auf die Ablaufgeschwindigkeit und die Genauigkeit der Analyse. Im konkreten Experiment war es sogar oft so, daß die Ablaufgeschwindigkeit durch eine größere Anzahl von abgeleiteten Prädikaten noch erhöht werden konnte, da mit deren Hilfe weniger unnötige Strukturen erzeugt wurden. Ein weiterer Kritikpunkt ist, daß die Analyse bislang nur intraprozedural verläuft, was aber laut den Autoren Gegenstand weiterer Forschung ist.

Literatur

[...]

---

¹ Kleene S.C, Introduction to Metamathematics, North-Holland, second edition, 1987.

² Wilhelm R., Sagiv M., Reps T., Shape Analysis, Compiler Construction, 2000

³ Sagiv M., Reps T., Wilhelm R., Parametric Shape Analysis via 3-Valued Logic, Symposium on Principles of Programming Languages, 1999.

⁴ Lev-Ami T., Sagiv M., TVLA: A System for Implementing Static Analyses Static Analysis Symposium, 2000

⁵ Lev-Ami T., Reps T., Sagiv M., Wilhelm R., Putting Static Analysis to Work for Verihcation: A Case Study, International Symposium on Software Testing and Analysis, 2000.

⁶ Sagiv M., Reps T., Wilhelm R., Solving Shape-Analysis Problems in Lan­guages with Destructive Updating Symposium on Principles of Programming Languages, 1996, New York

Häufig gestellte Fragen

Worum geht es in dieser Shape-Analyse?

Diese Shape-Analyse beschäftigt sich mit der statischen Untersuchung von Datenstrukturen im Heap, die durch Zeiger aufgebaut sind. Ziel ist es, diese Strukturen zu analysieren und zu beschreiben, um sie beispielsweise für die Programmverifikation oder das Debugging zu verwenden. Die Analyse berücksichtigt die Gestalt der Datenstrukturen, unabhängig von den konkreten Daten, die in den Elementen gespeichert sind.

Was sind die Ziele der Shape-Analyse?

Die Shape-Analyse zielt darauf ab, Antworten auf Fragen wie diese zu liefern: Ist ein Zeiger ein NULL-Zeiger? Zeigen zwei Zeiger auf dieselbe Zelle? Können mehrere Zeiger auf eine Zelle zeigen? Ist eine Zelle von einer bestimmten Variable aus erreichbar? Kann eine Zelle Teil eines Zyklus sein? Diese Informationen sind nützlich für Debugging, Programmverstehen, Garbage Collection und Parallelisierung.

Was sind logische Strukturen im Kontext der Shape-Analyse?

Die Shape-Analyse basiert auf 2- und 3-wertigen logischen Strukturen. 2-wertige Strukturen bestehen aus einem Universum von Symbolen, einer Menge von Prädikaten und einer Interpretation dieser Prädikate (Wahrheitswerte 0 oder 1). 3-wertige Strukturen erweitern dies um den Wert 1/2 (unbekannt), um Abstraktionen zu ermöglichen, beispielsweise um Listen unterschiedlicher Länge gleichartig zu behandeln.

Was sind zusammengefasste Knoten (Summary Nodes)?

Zusammengefasste Knoten in 3-wertigen Strukturen repräsentieren mehr als einen eigentlichen Knoten. Sie werden durch das unäre Prädikat `sm` gekennzeichnet und ermöglichen die Abstraktion von Speicherstrukturen, indem mehrere Knoten zu einem einzigen zusammengefasst werden. Dies führt zu einem Informationsverlust, kann aber die Analyse beschleunigen.

Was sind Basis- und abgeleitete Prädikate?

Prädikate werden in Basis- (core) und abgeleitete (instrumentation) Prädikate unterteilt. Basisprädikate (z.B. ob eine Variable auf eine Zelle zeigt oder ob eine Zelle auf eine andere zeigt) sind grundlegende Aussagen über den Speicherzustand. Abgeleitete Prädikate werden mit Hilfe von Formeln über Basisprädikate definiert und ermöglichen es, komplexere Eigenschaften (z.B. Erreichbarkeit) auszudrücken und die Genauigkeit der Analyse zu verbessern.

Wie funktioniert die Einbettung?

Die Einbettung ist eine surjektive Funktion von einer 2-wertigen in eine 3-wertige Struktur. Sie ordnet jeder Interpretation eines Prädikats entweder den gleichen Wert oder 1/2 zu. Das Einbettungstheorem besagt, dass jede Formel, die zu einem definiten Wert in einer 3-wertigen Struktur ausgewertet wird, denselben Wert in jeder eingebetteten Struktur liefert. Dies ist die Grundlage für die Verwendung 3-wertiger Logik in der statischen Analyse.

Wie läuft die Shape-Analyse ab?

Der Prozess der Shape-Analyse gliedert sich in fünf Schritte: Fokussieren (focus), Auswerten von Vorbedingungen, Ausführen von Update-Formeln, Konsistenzprüfung (coerce) und Zusammenfassen. Diese Schritte werden iterativ für jede Anweisung im Programm wiederholt, bis keine neuen Strukturen mehr hinzukommen.

Was ist Fokussieren (Focus)?

Fokussieren ist der erste Schritt, bei dem die gegebene Struktur anhand einer Formel in eine Menge von 3-wertigen Strukturen transformiert wird. Diese neuen Strukturen repräsentieren die gleichen 2-wertigen Strukturen wie die Eingabestruktur, haben aber die Eigenschaft, dass die gegebene Fokus-Formel einen definiten Wert annimmt.

Was sind Update-Formeln?

Update-Formeln drücken die operationelle Semantik einer Anweisung aus und bestimmen die Veränderungen der Prädikate. Sie werden auf jede Struktur angewendet, die durch das Fokussieren entstanden ist.

Was ist die Konsistenzprüfung (Coerce)?

Die Konsistenzprüfung ist ein Schritt, bei dem Strukturen mit widersprüchlichen Eigenschaften verworfen werden. Dies geschieht mit Hilfe einer Menge von Konsistenzregeln, die teilweise vom System selbst aus den abgeleiteten Prädikaten bestimmt werden können.

Was sind Anwendungsgebiete der Shape-Analyse?

Wichtige Anwendungsgebiete der Shape-Analyse sind die Programmverifikation und das Debugging. Sie ermöglicht die Überprüfung der partiellen Korrektheit von Algorithmen, z.B. von Sortieralgorithmen, und kann beim Debugging helfen, Fehler in Algorithmen zu erkennen.

Welche Kritik gibt es an der Shape-Analyse?

Eine Herausforderung ist die korrekte Beschreibung der Semantik des Programms durch Formeln. Das Finden geeigneter abgeleiteter Prädikate ist ein weiteres Problem, da diese einen großen Einfluss auf die Ablaufgeschwindigkeit und Genauigkeit der Analyse haben. Bisher ist die Analyse meist intraprozedural, was die Anwendbarkeit einschränkt.

Details

• Hochschule: Universität Passau
• Autor: Andreas Gärtner (Autor:in)
• Erscheinungsjahr: 2000
• Seiten: 15
• Katalognummer: V98939
• ISBN (eBook): 9783638973892
• Sprache: Deutsch
• Schlagworte: Shape-Analyse