arXiv:1703.10179v1 [cs.LO] 29 Mar 2017

Diplomarbeit
im Fach Informatik

Über die Präzision
interprozeduraler Analysen

Dorothea Jansen

Diplomarbeit
im Fach Informatik

Über die Präzision
interprozeduraler Analysen

Dorothea Jansen
Dezember 2010

Betreuer:
Prof. Dr. Markus Müller-Olm
Institut für Informatik
Westfälische Wilhelms-Universität Münster

Inhaltsverzeichnis
1

1 Einleitung

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

3
3
12
14
16

3 Klassische Ansätze zur interprozeduralen Analyse
3.1 Der funktionale Ansatz . . . . . . . . . . . . . . . . .
3.2 Der Call-String-Ansatz . . . . . . . . . . . . . . . . .
3.3 Koinzidenz . . . . . . . . . . . . . . . . . . . . . . .
3.4 Polyederanalyse . . . . . . . . . . . . . . . . . . . . .
3.4.1 Framework und Zuweisungen . . . . . . . . . .
3.4.2 Matrizenmengen als Summary-Information . . .
3.4.3 Relationen als Summary-Information . . . . . .
3.4.4 Erreichbare Zustände . . . . . . . . . . . . . .
3.4.5 Vergleich der beiden Summary-basierten Ansätze
3.5 Terminierung des Workset-Algorithmus . . . . . . . . .

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

21
22
25
30
47
47
49
50
52
52
57

4 Abstrakte Interpretation
4.1 Galois-Verbindungen . . . . . . . . . . . . . . . . . . . . . . .
4.2 Abstrakte Interpretation von Ungleichungssystemen . . . . . . .
4.3 Abstrakte Interpretation für interprozedurale Datenflussanalysen
4.3.1 Korrekte abstrakte Interpretation . . . . . . . . . . . . .
4.3.2 Präzise abstrakte Interpretation . . . . . . . . . . . . . .
4.3.3 Kanonische abstrakte Interpretation . . . . . . . . . . .
4.4 Polyederanalyse und konvexe Hüllenbildung . . . . . . . . . . .

.
.
.
.
.
.
.

.
.
.
.
.
.
.

.
.
.
.
.
.
.

.
.
.
.
.
.
.

.
.
.
.
.
.
.

59
60
65
73
76
81
83
88

5 Widening
5.1 Workset-Algorithmus mit
5.2 Nicht-Monotonie . . . .
5.3 Nicht-Terminierung . . .
5.4 Nicht-Koinzidenz . . . .

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

99
. 99
. 104
. 108
. 111

2 Grundlagen
2.1 Vollständige Verbände und Fixpunkte
2.2 Ungleichungssysteme . . . . . . . . .
2.3 Flussgraphen . . . . . . . . . . . . .
2.4 Der Workset-Algorithmus . . . . . . .

6 Fazit

.
. . . . . . .
. . . . . . .
. . . . . . .

Widening

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

123

1 Einleitung
In der Programmanalyse wird ein Programm im Hinblick auf bestimmte Eigenschaften
untersucht. Untersuchungsgegenstand kann dabei beispielsweise die Frage sein, ob
es Ausdrücke im Programm gibt, die an einer Stelle stets den gleichen Wert haben,
oder ob das Programm überflüssige Zuweisungen enthält. Es können aber aber auch
die Werte berechnet werden, welche die Programmvariablen annehmen können, oder
Gleichungen oder Ungleichungen über diese Werte aufgestellt werden. Derartige
Programmanalysen ermöglichen zum einen Programmoptimierung, indem überflüssige
Zuweisungen eliminiert oder konstante Ausdrücke durch diese Konstanten ersetzt
werden. Andererseits kann Programmanalyse auch für Validierung benutzt werden,
indem beispielsweise überprüft wird, ob Variablen nur erlaubte“ Werte annehmen.
”
Programmanalyse geschieht zur Compile-Zeit, es ist also keine Ausführung des
Programmes notwendig.
Ein Bereich der Programmanalyse ist die sogenannte Constraint-basierte Datenflussanalyse, welche auch Gegenstand dieser Arbeit ist. Bei der Datenflussanalyse fasst
man ein Programm als ein System von Graphen auf, deren Kanten mit den Anweisungen des Programms beschriftet sind, wobei jede Prozedur des Programms einem
Graphen entspricht. Besitzt das Programm nur eine Prozedur, so wählt man zu jeder
Kante eine Transferfunktion, die auf dem zugrundeliegenden Datenraum operiert.
Durch die Kanten und diese Abbildungen wird also beschrieben, wie sich Daten
entlang verschiedener Ausführungspfade verändern. Diese Veränderungen werden
dann durch Ungleichungen, also Constraints, ausgedrückt. Anhand dieser wiederum
werden Daten für die einzelnen Programmpunkte bestimmt.
Eine solche intraprozedurale Analyse, also die Analyse eines Programmes mit nur
einer Prozedur, benötigt für jede Kante eine Transferfunktion. Besitzt ein Programm
dagegen mehrere Prozeduren, so gibt es neben solchen Basisanweisungen auch noch
Prozeduraufrufe. Solche Programme sind viel mächtiger als diejenigen mit nur einer
Prozedur, da sie Rekursion beinhalten. Um diese Programme zu analysieren, müssen
also auch Prozeduraufrufe behandelt werden. Zwei Ansätze, wie dies geschehen kann,
wurden von Sharir und Pnueli in [SP81] vorgestellt: Der funktionale Ansatz berechnet
dabei zunächst für jede Prozedur eine Transferfunktion, die den Effekt der Prozedur
beschreibt, also die Veränderung der Daten vom Start- bis zum Endknoten der Prozedur. Der Call-String-Ansatz dagegen behandelt die verschiedenen Prozeduren wie eine

2

1 Einleitung

einzige, indem konzeptionell jede Aufrufkante durch den Graphen der aufgerufenen
Prozedur ersetzt wird.
Gegenstand dieser Arbeit ist die Untersuchung, wie genau die Informationen sind, die
diese beiden Ansätze in verschiedenen Situationen liefern. In der Praxis können die
theoretisch besten Lösungen einer gegebenen Analyse oft nicht endlich dargestellt oder
berechnet werden oder es ist keine geeignete Analyse zur Betrachtung einer gegebenen
Fragestellung bekannt. Deshalb betrachten wir nicht nur die jeweils theoretisch besten
Lösungen, sondern untersuchen auch die Lösungen, wenn zusätzlich abstrakte Interpretationen oder Widening-Operatoren verwendet werden. Durch abstrakte Interpretation
wird anstelle der konkreten Information eines gegebenen Ungleichungssystems eine abstrakte Information berechnet. Damit können neue Analysen konstruiert werden, die
die gestellte Frage beantworten oder deren Lösung endlich darstellbar und berechenbar
ist. Mithilfe von Widening-Operatoren kann Terminierung des Workset-Algorithmus
erzwungen werden. Der Workset-Algorithmus ist einer Mittel zur Berechnung der
Lösung des Ungleichungssystems einer constraint-basierten Datenflussanalyse.
Nach der Einführung einiger grundlegender Begriffe und Methoden in Kapitel 2
werden wir in Kapitel 3 zunächst den funktionalen und den Call-String-Ansatz
vorstellen und ihre jeweils besten“ Lösungen miteinander verglichen. Weiter wird die
”
Analyse interprozeduraler Programme am Beispiel der Polyederanalyse von Cousot
und Halbwachs [CH78] veranschaulicht, die den funktionalen Ansatz variiert. Wir
zeigen, dass die Berechnung der Lösungen des funktionalen und des Call-StringAnsatzes mithilfe des Workset-Algorithmus nicht immer terminiert. Darum stellen
wir in Kapitel 4 und 5 zwei von Cousot und Cousot [CC76, CC77] bekannte Ansätze
vor, mit denen eine solche Terminierung erreicht werden kann: In Kapitel 4 betrachten
wir abstrakte Interpretationen und vergleichen die Lösungen des funktionalen und
des Call-String-Ansatzes unter Verwendung von abstrakter Interpretation. Außerdem
werden wir das Beispiel der Polyederanalyse fortsetzen. In Kapitel 5 untersuchen
wir anschließend Widening-Operatoren und stellen wiederum die Frage nach dem
Vergleich der Lösungen des funktionalen und des Call-String-Ansatzes. Zuletzt folgen
in Kapitel 6 eine Zusammenfassung der Ergebnisse sowie ein Ausblick auf weitere
Untersuchungen, die auf diese Arbeit aufbauen könnten.

2 Grundlagen
In diesem Kapitel werden Grundlagen zur Datenflussanalyse vorgestellt. Bei einer
Datenflussanalyse wird zu jedem Punkt eines Programms eine gesuchte Information
berechnet. Eine solche Information kann die Menge der möglichen Werte der Programmvariablen sein oder ob eine Variable in einem Punkt stets denselben Wert hat.
Wie sich eine Information durch eine Programmanweisung ändert, wird mithilfe von
Ungleichungen beschrieben. Zur Berechnung der gesuchten Informationen wird ein
Ungleichungssystem aufgestellt, das die Informationen an den verschiedenen Punkten miteinander in Verbindung setzt. Für einfache Anweisungen von Programmen
stellen wir bereits in diesem Kapitel Ungleichungen auf, während wir komplexere
Anweisungen in Kapitel 3 behandelt werden. Weiter werden wir in diesem Kapitel
eine Methode vorstellen, mit denen ein Ungleichungssystem gelöst werden kann,
den sogenannten Workset-Algorithmus. Wir werden im Folgenden meist Analyse“
”
anstelle von (constraint-basierter) Datenflussanalyse“ sagen.
”
Wir beginnen damit, einige Begriffe und theoretische Grundlagen einzuführen. Diese
basieren, sofern nicht anders gekennzeichnet, auf Nielson et al. [NNH99].

2.1 Vollständige Verbände und Fixpunkte
In der Datenflussanalyse wird jedem Programmpunkt eine Information zugeordnet.
Um mit dem Begriff der Information“ formal arbeiten zu können, fassen wir Infor”
mationen als Elemente einer geeigneten Menge L auf. Diese Informationen wollen
wir außerden im Hinblick darauf untersuchen, welche korrekte Information präziser
ist als eine andere. Ist zum Beispiel x = 2, so ist die Information Der Wert von x ist
”
eine ganze Zahl“ weniger präzise als die Information Der Wert von x ist eine gerade
”
positive Zahl“. Beide Informationen sind korrekt. Die Aussage Der Wert von x ist
”
4.“ ist wiederum präziser, aber nicht korrekt. Die präziseste korrekte Information ist
Der Wert von x ist 2.“. Von Interesse sind also nur korrekte Informationen, die dabei
”
möglichst präzise sind. Formal wird dieser Präzisionsbegriff durch eine Halbordnung
beschrieben. Eine Information heißt dann präziser, je kleiner sie bezüglich dieser
Halbordnung ist.

4

2 Grundlagen

Definition 2.1 (Halbordnung). Eine Halbordnung (L, v) ist eine Menge L zusammen
mit einer Relation v ⊆ L × L mit folgenden Eigenschaften:
• Die Relation v ist reflexiv, d.h. für alle l ∈ L ist l v l.
• Die Relation v ist transitiv, d.h. für alle l, l0 , l00 ∈ L mit l v l0 und l0 v l00 ist
l v l00 .
• Die Relation v ist antisymmetrisch, d.h. für alle l, l0 ∈ L mit l v l0 und l0 v l
ist l = l0 .
Dabei schreiben wir l v l0 für (l, l0 ) ∈ v. Ist l v l0 mit l 6= l0 , so schreiben wir auch
l @ l0 . Entsprechend schreiben wir l0 w l für l v l0 und l0 A l für l @ l0 .
Beispiel 2.2. Sei X eine Menge und L := 2X die Potenzmenge von X. Dann ist
(L, ⊆) eine Halbordnung. Dies folgt direkt aus der Definition der Teilmenge.

Ein auch im Folgenden wichtiges Beispiel ist das der Intervallanalyse aus [CC76], für
das wir nun zunächst den Verband der Intervalle einführen.
Beispiel 2.3. Wir definieren
(LInt , vInt ) := ({[l, u] | l ∈ Z ∪{−∞}, u ∈ Z ∪{+∞}, l ≤ u} ∪ {∅}, ⊆)
als die Menge der beschränkten und unbeschänkten Intervalle in den ganzen Zahlen.
Dies ist offenbar eine Halbordnung. Wir nennen (LInt , vInt ) Intervallverband.
Weiter betrachten wir (LIA , vIA ) mit (LIA , vIA ) := (Var → (LInt , vInt ), vIA ) für
eine endliche Menge Var von Variablen. Dabei ist ρ vIA ρ0 für ρ, ρ0 ∈ (LIA , vIA ),
wenn ρ(x) vInt ρ0 (x) für jede Variable x ∈ Var gilt. Man sieht leicht, dass dies eine
Halbordnung definiert. Diese nennen wir Intervallanalyseverband.

Den Begriff Verband“ werden wir in Kürze einführen und auch zeigen, dass der
”
Intervall- und der Intervallanalyseverband tatsächlich Verbände sind.
Im Rahmen der Datenflussanalyse werden für einen Programmpunkt oft verschiedene
Informationen berechnet. Da einem jeden Punkt aber eine einzige Information und
nicht eine Menge von Informationen zugeordnet werden soll, muss eine neue Information bestimmt werden. Diese muss alle Informationen der berechneten Menge enthalten,
dabei aber möglichst präzise sein. Der Vorgang, diese neue Information zu berechnen,
entspricht der Bildung der kleinsten oberen Schranke der Informationsmenge:
Definition 2.4. Seien (L, v) eine Halbordnung und A ⊆ L. Dann heißt l ∈ L
• obere Schranke von A, falls a v l für alle a ∈ A gilt.
• untere Schranke von A, falls l v a für alle a ∈ A gilt.

2.1 Vollständige Verbände und Fixpunkte

5

• kleinste obere Schranke von A, falls l eine obere Schranke von A ist und für
jede weitere obere Schranke l0 von A bereits l v l0 gilt.
• größte untere Schranke von A, falls l eine untere Schranke von A ist und für
jede weitere untere Schranke l0 von A bereits l0 v l gilt.
Sofern sie existiert,
F ist die kleinste obere Schranke von A eindeutig und wird mit
bezeichnet. Für {a, b} schreiben wir auch a t b.

F

A

Beispiel 2.5. Sei X eine Menge und L := 2X . Seien A, B ⊆ X. Dann ist A ∪ B die
kleinste obere Schranke von {A, B}: Offenbar gilt A, B ⊆ A ∪ B. Somit ist A ∪ B
eine obere Schranke. Ist S eine weitere obere Schranke, so ist A, B ⊆ S und damit
auch A ∪ B ⊆ S und damit ist A ∪ B schon die kleinste obere Schranke.
Ebenso bestimmt man
S  die kleinste obere Schranke einer beliebigen Teilmenge von L:
X
Ist A ⊆ 2 , so ist
A | A ∈ A die kleinste obere Schranke von A.
Betrachte nun den Intervallverband (LInt , vInt ). Seien I1 = [l1 , u1 ] und I2 = [l2 , u2 ]
zwei Intervalle in (LInt , vInt ). Setze l := min{l1 , l2 } und u := max{u1 , u2 }. Dann ist
I := [l, u] die kleinste obere Schranke von {I1 , I2 }: Nach Definition ist l ≤ li und
u ≥ ui für i = 1, 2. Damit ist auch [li , ui ] ⊆ [l, u] und I ist eine obere Schranke. Ist
I 0 = [l0 , u0 ] eine weitere obere Schranke, so gilt l0 ≤ li und u0 ≥ ui für i = 1, 2. Damit
ist auch l0 ≤ min{l1 , l2 } = l und u0 ≥ max{u1 , u2 } = u und so I 0 ⊇ I. Also ist I sogar
die kleinste obere Schranke von {I1 , I2 }.
Für eine beliebige Teilmenge A ⊆ (LInt , vInt ) setze
l := inf{l0 | ∃u0 ∈ Z ∪{+∞} : [l0 , u0 ] ∈ (LInt , vInt )}
u := sup{u0 | ∃l0 ∈ Z ∪{−∞} : [l0 , u0 ] ∈ (LInt , vInt )}
als das Infimum der unteren und das Supremum der oberen Intervallgrenzen. Man
zeigt nun ebenso wie für zweielementige Mengen, dass [l, u] die kleinste obere Schranke
von A ist.
Damit existieren auch obere Schranken
in (LIA , vIA ): Sei P ⊆ (LIA , vIA ). Definiere
F
ρ ∈ (LIA , vIA ) durch ρ(x) := {ρ0 (x) | ρ0 ∈ P } für jedes x ∈ Var. Dann ist ρ die
kleinste obere Schranke von P .

Im Allgemeinen existiert eine solche kleinste obere Schranke nicht für jede beliebige
Teilmenge einer Halbordnung. Um also die kleinste obere Schranke gewisser oder aller
Teilmengen bilden zu können, müssen wir weitere Forderungen an die Halbordnung
(L, v) stellen.

6

2 Grundlagen

Definition 2.6. Sei (L, v) eine Halbordnung. Eine Teilmenge K ⊆ L heißt Kette,
falls K total geordnet ist, d.h. wenn x v y oder y v x für je zwei Elemente x, y ∈ L
gilt.
Eine Halbordnung (L, v) heißt kettenvollständig, falls jede Kette K ⊆ L eine kleinste
obere Schranke besitzt.
Beispiel 2.7. Die Menge K := {[0, n] | n ∈ N} ist eine Kette in (LInt , vInt ): Seien
n, m ∈ N und ohne Beschränkung der Allgemeinheit n ≤ m. Dann ist [0, n] ⊆ [0, m].
Damit sind je zwei solche Intervalle vergleichbar.
Die Menge N := {[n, n + 1] | n ∈ N} ist dagegen keine Kette in (LInt , vInt ): Seien
wieder n < m natürliche Zahlen. Dann sind [n, n + 1] und [m, m + 1] unvergleichbar:
Angenommen, es wäre [n, n + 1] ⊆ [m, m + 1]. Dann gilt n ≥ m und n + 1 ≤ m + 1,
was n = m impliziert. Dies ist ein Widerspruch zu n < m. Ebenso widerlegt man
[n, n + 1] ⊇ [m, m + 1]. Demnach ist N keine Kette.

Bemerkung 2.8. In einer kettenvollständigen
Halbordnung gibt es ein eindeutig
F
bestimmtes kleinstes Element ⊥ = ∅.

Im Folgenden werden wir meist die stärkere Forderung stellen, dass die betrachtete
Halbordnung bereits ein vollständiger Verband ist.
Definition 2.9. Eine Halbordnung (L, v) heißt vollständiger Verband , falls jede
Teilmenge A ⊆ L eine kleinste obere Schranke besitzt.
Bemerkung 2.10. Jeder vollständige Verband ist insbesondere kettenvollständig. 
Beispiel 2.11. Sei X eine Menge und L := 2X . Dann sind (L, ⊆) sowie (LInt , vInt )
und (LIA , vIA ) vollständige Verbände. Dies folgt direkt aus den Beobachtungen in
Beispiel 2.5.

Im funktionalen Ansatz zur Analyse interprozeduraler Programme werden wir neben
einem zugrundeliegenden vollständigen Verband L auch die Menge der Abbildungen
L → L betrachten und benötigen dabei, dass auch diese wieder einen vollständigen
Verband bilden. Das dies immer der Fall ist, zeigt das folgende Beispiel.
Beispiel 2.12. Sei (L, v) ein vollständiger Verband und (L → L) die Menge aller
Abbildungen von L nach L. Es sei nun f v g genau dann, wenn f (l) v g(l) für jedes
l ∈ L gilt. Dies ist offensichtlich eine Halbordnung.
Sei weiter F eine beliebige Teilmenge von (L → L). Wir definieren eine Abbildung
g : L → L durch
G
g(l) :=
f (l) | f ∈ F .

2.1 Vollständige Verbände und Fixpunkte

7

Da (L, v) ein vollständiger Verband ist, existieren diese kleinsten oberen Schranken
und g ist wohldefiniert. Weiter gilt nach Konstruktion offenbar f v g für jedes f ∈ F.
Also ist g eine obere Schranke von F
Sei h eine weitere obere Schranke.FDann
gilt für jedes f ∈ F und jedes l ∈ L bereits

f (l) | f ∈ F für jedes l ∈ L. Damit folgt aber
f (l) v h(l). Also ist auch g(l) =
schon g v h und g ist die kleinste obere Schranke von F. Also ist ((L → L), v) ein
vollständiger Verband.

Sind die Informationen nun Elemente einer Halbordnung (L, v), so müssen wir die
Programmanweisungen b mit Transferfunktionen fb : L → L assoziieren, die den
Datenfluss gemäß dieser Anweisung beschreiben. Dabei erwarten wir, dass eine solche
Abbildung fb stets präzisionserhaltend ist. Darunter verstehen wir Folgendes: Wenn
eine Information präziser ist als eine andere Information, dann ist auch ihr Bild unter
fb präziser als das der anderen. Dies entspricht dem Begriff der Monotonie.
Definition 2.13. Eine Abbildung f : L → L0 zwischen zwei Halbordnungen (L, vL )
und (L0 , vL0 ) heißt monoton, falls für alle l1 , l2 ∈ L aus l1 vL l2 schon f (l1 ) vL0 f (l2 )
folgt.
Beispiel 2.14. Auch die Menge der monotonen Abbildungen (L →mon L) bildet
einen vollständigen Verband: Sei wieder F eine beliebige Teilmenge und g wie im
vorigen Beispiel 2.12 definiert. Es reicht nun zu zeigen, dass g wieder monoton ist.
Seien also l, l0 ∈ L mit l v l0 . Dann ist für jedes f ∈ F
f (l) v f (l0 ) =

G

f (l0 ) | f ∈ F = g(l0 )

und damit
g(l) =

G

f (l) | f ∈ F v g(l0 ).

Also ist auch ((L →mon L), v) ein vollständiger Verband.



Wir werden später die Informationen, die an den Programmpunkten gültig sind,
mithilfe von Mengen von Ungleichungen charakterisieren. Außerdem werden wir zeigen,
dass sich die Lösungen dieser Ungleichungssystemen als Präfixpunkte monotoner
Abbildungen schreiben lassen.
Definition 2.15. Sei L eine Menge und f : L → L eine Abbildung. Dann heißt l ∈ L
Fixpunkt von f , falls f (l) = l ist. Ist (L, v) eine Halbordnung, definieren wir weiter,
dass l Präfixpunkt heißt, falls f (l) v l ist, und Postfixpunkt, falls f (l) w l gilt.

8

2 Grundlagen

Von besonderem Interesse wird dabei stets der kleinste aller Fixpunkte einer monotonen Abbildung sein, da dieser der präzisesten gültigen Information entspricht, wie wir
im nächsten Abschnitt sehen werden. Die Existenz des kleinsten Fixpunktes liefert
der Fixpunktsatz von Tarski, dessen Beweis in Nielson et al. [NNH99, S. 400f.] zu
finden ist.
Satz 2.16 (Fixpunktsatz von Tarski). Seien (L, v) ein vollständiger Verband und
f : L → L monoton. Dann hat f einen kleinsten Fixpunkt lfp(f ) und einen größten
Fixpunkt gfp(f ) und es gilt
l
G
lfp(f ) =
x ∈ L | f (x) v x und gfp(f ) =
x ∈ L | s v f (x) .
Der kleinste Fixpunkt entspricht also dem kleinsten Präfixpunkt und der größte
Fixpunkt dem größten Postfixpunkt. Diese Tatsache werden wir später benötigen.
Einen weiteren nützlichen Ansatz zur Bestimmung des kleinsten Fixpunktes einer
monotonen Abbildung liefert der folgende Satz, der eine Verallgemeinerung eines
Satzes ist, der als Fixpunktsatzes von Kleene bekannt ist. Vergleiche dazu auch
[LNS82].
Satz 2.17. Sei (L, v) eine kettenvollständige Halbordnung und f : L → L monoton.
Dann hat f einen kleinsten Fixpunkt lfp(f ) und es gilt
G
lfp(f ) =
lα | α Ordinalzahl
mit
l0 := ⊥
lα+1 := f (lα ) für eine Ordinalzahl α
G
lα :=
lγ | γ < α für eine Limesordinalzahl α.
Beweis. Wir prüfen zunächst, dass diese lα wohldefiniert sind. Dazu reicht es nach
zu weisen, dass für alle Ordinalzahlen α die Menge {lγ | γ < α} eine Kette ist. Dies
wiederum folgt daraus, dass für je zwei Ordinalzahlen α und β aus α < β auch lα v lβ
folgt: Wir zeigen dies per transfiniter Induktion für jede Ordinalzahl β: Für β = 0 ist
nichts zu zeigen.
Sei nun β = β 0 + 1 für eine Ordinalzahl β 0 und gelte die Behauptung für kleinere
Ordinalzahlen. Sei α < β 0 + 1 beliebig. Da nach Induktionsvoraussetzung schon
lα v lβ 0 gilt, genügt es, lβ 0 v lβ 0 +1 nach zu weisen. Ist dabei β 0 eine Limesordinalzahl,
so gilt
G

lβ 0 +1 = f
lγ | γ < β 0

2.1 Vollständige Verbände und Fixpunkte

9

und wegen der Monotonie von f
w

G

f (lγ ) | γ < β 0

G
lγ+1 | γ < β 0
G

=
{lγ+1 | γ < β 0 } ∪ {⊥} .
=

Da γ eine Limesordinalzahl ist, folgt aus γ < β 0 auch γ + 1 < β 0 und wir erhalten
=

G
lγ | γ < β 0

= lβ 0 .
Andernfalls existiert lβ 0 −1 und nach Induktionsvoraussetzung ist lβ 0 −1 v lβ 0 und mit
der Monotonie von f dann lβ 0 = f (lβ 0 −1 ) v f (lβ 0 ) = lβ 0 +1 .
Sei zuletzt β eine Limesordinalzahl und gelte die Behauptung schon für alle kleineren
Ordinalzahlen. Dann ist für α < β bereits lα ∈ {lγ | γ < β} und damit
lα v

G

lγ | γ < β = lβ .

Hieraus folgt insbesondere, dass K := {lα | α Ordinalzahl} eine Kette ist.
Wir zeigen nun, dass, sofern f Fixpunkte besitzt und x ein beliebiger Fixpunkt von
f ist, lα v x für jede Ordinalzahl α gilt. Für α = 0 ist dies trivialerweise erfüllt, da
l0 = ⊥ v x schon für jedes Element x ∈ L gilt.
Gilt die Behauptung für eine Ordinalzahl α, so ist mit der Monotonie von f
lα+1 = f (lα ) v f (x) = x.
Ist α hingegen eine Limesordinalzahl und gilt die Behauptung für alle kleineren
Ordinalzahlen, so erhalten wir
G
G
lα = {lγ | γ < α} v {x | γ < α} = x.
Sei nun κ die Kardinalität von L. Angenommen, die Folge (lα )α∈Ord wird nie stabil.
Dann besitzt (lα )α∈Ord eine echt aufsteigende Teilfolge. Da diese aber nur aus Elementen von L besteht, wird sie spätestens ab dem κ-ten Folgenelement stabil. Dies ist
ein Widerspruch. Also wird auch (lα ) stabil. Es existiert also eine Ordinalzahl β mit
lβ = lβ+1 = f (lβ )

10

2 Grundlagen

und lβ ist ein Fixpunkt von f . Wie wir bereits gesehen haben, ist lβ aber auch kleiner
oder gleich jedem anderen Fixpunkt von f und damit der kleinste Fixpunkt von f .
Es folgt also
G
lfp(f ) = lβ =
lα | α Ordinalzahl
und das war die Behauptung.
Um später die kleinsten Fixpunkte zweier monotoner Funktionen zu vergleichen,
werden wir folgende Verallgemeinerung des Transferlemmas, welches in [LNS82] zu
finden ist, benutzen.
Satz 2.18. Seien (L, v), (L0 , v0 ) vollständige Verbände, f : L → L, g : L0 → L0
monoton und R ⊆ L × L0 eine Relation mit folgenden Eigenschaften:
a) Für alle l ∈ L, l0 ∈ L0 mit (l, l0 ) ∈ R ist auch (f (l), g(l0 )) ∈ R.
F
F
b) Für alle X ⊆ R ist ( X1 , X2 ) ∈ R. Dabei ist
X1 := {x ∈ L | ∃y ∈ L0 : (x, y) ∈ X}
und
X2 := {y ∈ L0 | ∃x ∈ L : (x, y) ∈ X}.
Dann gilt (lfp(f ), lfp(g)) ∈ R.
Beweis. Definiere induktiv
l0 := ⊥L
lα+1 :=
F f(lα )
lα :=
lβ | β < α

l00 := ⊥L0
0
0
lα+1
:=
g(l
α)

F
lα0 := 0 lβ0 | β < α

für eine Ordinalzahl α
für eine Limesordinalzahl α

Dann gilt (lα , lα0 ) ∈ R für jede Ordinalzahl α: Für α = 0 ist
G G0 
(⊥L , ⊥L0 ) =
∅,
∅ ∈R
nach Bedingung b). Ist α eine Ordinalzahl und (lα , lα0 ) ∈ R, so gilt
0
(lα+1 , lα+1
) = (f (lα ), g(lα0 )) ∈ R

aufgrund von Bedingung a). Für eine Limesordinalzahl α ist mit Induktionsvoraussetzung (lβ , lβ0 ) ∈ R für jedes β < α. Wiederum mit Bedingung b) erhalten wir
nun
G
G0 

(lα , lα0 ) =
lβ | β < α ,
lβ0 | β < α ∈ R.

2.1 Vollständige Verbände und Fixpunkte

11

Nun existieren nach Satz 2.17 Ordinalzahlen βf , βg mit lβf = lfp(f ) und lβ0 g = lfp(g).
Definiere β := max{βf , βg }. Dann gilt
(lfp(f ), lfp(g)) = (lβ , lβ0 ) ∈ R,
was den Satz beweist.
Für Datenflussanalysen benötigen wir sowohl eine Halbordnung (L, v) der Informationen als auch eine Menge monotoner Funktionen L → L, die den Datentransfer
beschreiben. Zusammen bezeichnen wir dies als monotones Framework :
Definition 2.19. Ein monotones Framework (L, v, F) besteht aus einem vollständigen Verband (L, v) und einer unter Komposition abgeschlossenen Menge
F ⊆ (L →mon L) monotoner Abbildungen, welche die Identität idL enthält. Die
Abbildungen der Menge F heißen Transferfunktionen.
Ein monotones Framework (L, v, F) heißt (positiv-/universell-)distributiv, falls jede
Abbildung f ∈ F (positiv-/universell-)distributiv ist. Dabei heißt f
• distributiv , falls f (l t l0 ) = f (l) t f (l0 ) für alle l, l0 ∈ L gilt.
F
F
• positiv-distributiv , falls f ( A) = f (A) für jede nichtleere Teilmenge A ⊆ L
gilt.
F
F
• universell-distributiv , falls f ( A) = f (A) schon für jede Teilmenge A ⊆ L
gilt.
Dabei gelten folgende Zusammenhänge: Jede universell-distributive Abbildung ist
nach Definition bereits positiv-distributiv und jede positiv-distributive Abbildung
schon distributiv. Distributive Abbildungen sind wiederum monoton: Seien dazu
f : L → L distributiv und l, l0 ∈ L mit l v l0 . Dann ist l0 = l t l0 und damit
f (l0 ) = f (l t l0 ) = f (l) t f (l0 ) w f (l)
und f ist monoton.
Der Unterschied zwischen einer positiv-distributiven und einer universell-distributiven
F
Abbildung liegt nun darin,
dass
letztere
das
kleinste
Element
⊥
=
∅ stets auf das
F
kleinste Element ⊥ = f (∅) abbildet, was für positiv-distributive Abbildungen nicht
gefordert wird.
Beispiel 2.20. Sei wieder L := 2X für eine Menge X und F die Menge aller
Abbildungen f : L → L, die universell-distributiv sind. Dann bildet (L, ⊆, F) ein
universell-distributives Framework:

12

2 Grundlagen

In Beispiel 2.11 haben wir bereits gesehen, dass (L, ⊆) ein vollständiger Verband
ist. Nach Definition von F ist jede Funktion f ∈ F universell-distributiv und damit
monoton. Die Identität idL ist offenbar universell-distributiv, also gilt idL ∈ F. Man
rechnet leicht nach, dass die Komposition universell-distributiver Funktionen wieder
universell-distributiv ist. Also ist F abgeschlossen unter Komposition. Damit ist
(L, ⊆, F) ein universell-distributives Framework.


2.2 Ungleichungssysteme
Ungleichungssysteme beschreiben Zusammenhänge von Informationen an verschiedenen Programmpunkten. Die präziseste Information, die diese Zusammenhänge erfüllt,
ist die kleinste Lösung des Ungleichungssystems. In diesem Abschnitt geben wir eine
allgemeine Beschreibung von Ungleichungssystemen und beschäftigen uns mit deren
kleinsten Lösungen.
Seien (L, v) ein vollständiger Verband und Var = {xi | i ∈ I} eine abzählbare Menge
von Variablen mit Indexmenge I, die Werte in L annehmen. Die Menge der Vektoren“
”
über L bildet zusammen mit komponentenweisem v eine Halbordnung (LI , vI ). Es
ist x vI y genau dann, wenn xi v yi für jedes i ∈ I gilt.
Definition 2.21. Ein Ungleichungssystem ist eine Menge U von Ungleichungen der
Gestalt
xj w f (x)

(2.1)

für Variablen xj ∈ Var und monotone Abbildungen f : LI → L. Dabei schreiben wir
x abkürzend für (xi )i∈I . Für jede Variable xj enthalte U dabei nur eindliche viele
Ungleichungen der Gestalt xy w f (x).
Die Menge der verwendeten Abbildungen bezeichnen wir mit FU . Solche Abbildungen
nennen wir verallgemeinerte Transferfunktionen. Für einelementige Indexmengen sind
verallgemeinerte Transferfunktion bereits Transferfunktionen.
Um ein gegebenes Ungleichungssystem zu lösen, formen wir es zunächst, wie im
Folgenden beschrieben, in ein äquivalentes Ungleichungssystem um, in welchem jede
Variable auf der linken Seite von genau einer Ungleichung auftaucht: Sind dabei
xj w f1 (x) und xj w f2 (x) zwei Ungleichungen mit gleicher linker Seite, so werden
diese ersetzt durch xj w f1 (x) t f2 (x). Dieser Vorgang wird wiederholt, bis keine zwei
Ungleichungen mit gleicher linker Seite mehr übrig sind. Für jede Variable xj ∈ Var,
für die keine Ungleichung mit linker Seite xj existiert, wird weiter xj w ⊥ hinzugefügt.
Dazu definieren wir
FU ,j := {f ∈ FU | ∃ Ungleichung xj w f (x) ∈ U}

2.2 Ungleichungssysteme

13

als die Menge derjenigen Abbildungen, die in einer Ungleichung mit linker Seite xj
benutzt werden. Weiter sei
G
Fj :=
F j : LI → L
definiert durch
Fj (x) :=

G

f (x) | f ∈ FU ,j .

Dies ist diejenige Abbildung, die für jedes Element die Informationen, die durch die
einzelnen Abbildungen des Ungleichungssystems für dieses Element berechnet werden,
zusammen fasst“. Wir erhalten nun das Ungleichungssystem
”
U I := {xj w Fj (x)}.
(2.2)
Dies liefert auch für diejenigen Variablen, die im ursprünglichen Ungleichungssystem
auf keiner linken Seite einer Ungleichung vorkommen, das Gewünschte: Existieren
im ursprünglichen UngleichungssystemFkeine Ungleichungen mit linker Seite xj , so
ist die Menge FU ,j leer. Dann ist aber FU ,j die Abbildung, die jedes x ∈ LI auf ⊥
abbildet.
Lemma 2.22. Die Lösungsmengen von U (2.1) und UI (2.2) stimmen überein.
Beweis. Dies folgt unmittelbar aus der Äquivalenz x w y ∧x w z ⇔ x w y tz: ⇒“ ist
”
offensichtlich, während ⇐“ aus der Tatsache xt(y tz) = (xty)t(xtz) = xtx = x
”
resultiert.
Das Ungleichungssystem U I ist nun offenbar äquivalent zu
x wI F (x),
wobei
F := (Fj )j∈I : LI → LI .

(2.3)

Somit können wir F an Stelle des gegebenen Ungleichungssystems (2.1) betrachten.
Lemma 2.23. Für jedes j ∈ I ist Fj monoton als Abbildung zwischen (LI , vI ) und
(L, v).
Beweis. Allgemein gilt: Für zwei vollständige Verbände (D, v) und (D0 , v0 ) und
monotone Abbildungen f, g : D → D ist die Abbildung
h : (D, v) → (D, v),
d 7→ f (d) t g(d)

14

2 Grundlagen

wiederum monoton:
Es ist a v b ⇔ a t b = b. Sei nun a v b, dann ist
h(a) t h(b) = f (a) t g(a) t f (b) t g(b) = f (b) t g(b) = h(b),
was h(a) v h(b) beweist.
F
Für j ∈ I ist nun Fj : LI → L durch Fj (x) = m
i=1 fi (x) für monotone Operatoren
fi ∈ FU ,j definiert. Da m endlich ist, folgt die Monotonie von Fj bereits aus obiger
Aussage.
Mit dem Fixpunktsatz von Tarski folgt nun:
Korollar 2.24. Die kleinste Lösung des Ungleichungssystems U (2.1) ist der kleinste
Präfixpunkt von F und dieser stimmt mit dem kleinsten Fixpunkt lfp(F ) von F
überein.
Wir werden die kleinste Lösung eines Ungleichungssystems später mit x bezeichnen.

2.3 Flussgraphen
Im vorigen Abschnitt haben wir uns mit Ungleichungssystemen und deren Lösungen befasst. In diesem Abschnitt erläutern wir einführend, wie zu einem gegebenen
Programm ein solches Ungleichungssystem gefunden werden kann, dessen Lösung
dann die gewünschten Informationen an den einzelnen Programmpunkten liefert.
Im Folgenden gehen wir davon aus, dass jedes Programm bereits als eine endliche
Menge von Flussgraphen gegeben ist. Dabei entspricht jeder Flussgraph einer Prozedur
des Programms. Mit Proc bezeichnen wir die (endliche) Menge von Prozeduren des
Programms, die sich auch rekursiv aufrufen können. Um die Darstellung einfach zu
halten, verzichten wir auf lokale Variablen und ebenso auch auf Prozedurparameter.
Das Programm habe also nur globale Variablen.
Zunächst definieren wir ein solches Flussgraphsystem. Anschließend stellen wir einige
Ungleichungen für ein Ungleichungssystem auf, dessen Lösung mit Informationen an
Programmpunkten korrespondiert.
Definition 2.25. Ein Flussgraphsystem ist eine endliche Menge G = {Gp }p∈Proc
disjunkter endlicher Flussgraphen. Jeder Flussgraph Gp besteht aus
• einer endlichen Menge Np von Knoten, die Programmpunkten entsprechen,
• einer endlichen Menge Ep ⊆ (Np × Label ×Np ) von Kanten,

2.3 Flussgraphen

15

• einem ausgezeichneten Startknoten sp ∈ Np und
• einem ausgezeichneten Endknoten rp ∈ Np der Prozedur p.
Hierbei ist Label eine Menge von Beschriftungen, die den Programmanweisungen
entsprechen. Solche Beschriftungen sind entweder sogenannte Basisanweisungen (im
Folgenden meist mit b“ bezeichnet) oder Prozeduraufrufe (im Folgenden meist p()“).
”
”
Die entsprechenden
Kanten nennen wir Basiskanten und Aufrufkanten.
Wir setzen
S
S
N := {Np | p ∈ Proc} als die Menge aller Knoten und E := {Ep | p ∈ Proc} als
die Menge aller Kanten.
Ein solches Flussgraphssystem entsteht aus einem Programm folgendermaßen: Zunächst werden die Programmpunkte einer Prozedur als Knoten aufgefasst. Dann
wird für jede Anweisung zwischen je zwei Programmpunkten eine gerichtete Kante
zwischen den zugehörigen Knoten hinzugefügt, wobei die Kante mit dieser Anweisung
beschriftet ist.
Um nun zu jedem Programmpunkt Informationen, wie beispielsweise die möglichen
Werte der Programmvariablen, bestimmen zu können, stellen wir zunächst ein Ungleichungssystem auf. Dabei sei (L, v, F) das zugrundeliegende Framework. Also ist L die
Menge der Informationen. Mit I : N → L bezeichnen wir die Abbildung, die am Ende
der Rechnung jedem Programmpunkt u die gewünschte Information I[u] zuordnet.
Als Variablen (xi )i∈I im Ungleichungssystem betrachten wir hier also (I[ν])ν∈N . Für
jede Basisanweisung b ∈ Label wählen wir eine Transferfunktion fb ∈ F.
u

I[u]
b

b
v

I[v] w fb (I[u])

Abbildung 2.1: Fluss von Informationen.
Für jede Basiskante e = (u, b, v) benötigen wir eine Ungleichung
I[v] w fe ((I[ν])ν∈N ),
wobei fe durch fe ((I[ν])ν∈N ) := fb (I[u]) definiert ist. Also hängt fe nur von der
Basisanweisung b und der eingehenden Information I[u] ab und ist nach Definition
monoton. Diese Ungleichung wird in Abbildung 2.1 illustriert. Weiter wird für den

16

2 Grundlagen

Startknoten des Programms, den wir mit smain bezeichnen, verlangt, dass er eine
Startinformation enthält. Darum enthält U eine Ungleichung
smain w init
für eine gegebene Startinformation init. Zur Gewinnung von Ungleichungen aus den
Aufrufkanten gibt es verschiedene Möglichkeiten, welche wir in Kapitel 3 betrachten
werden.
Ist zu einem Programm nun ein Ungleichungssystem U gegeben, in dem ausschließlich
monotone Funktionen verwendet werden, so können wir wie in Abschnitt 2.2 die
Funktion F bestimmen, deren kleinster Fixpunkt mit der kleinsten Lösung von U
übereinstimmt.
Bemerkung 2.26. Das hier vorgestellte Verfahren, um aus einem Programm ein
zu untersuchendes Ungleichungssystem zu gewinnen, ist eine Vorwärtsanalyse. Im
Gegensatz dazu stehen Rückwärtsanalysen: Hier wird der Endknoten rmain mit einer Startinformation init versehen und die Informationen laufen in umgekehrter
Richtung durch die Kanten. Weisen wir also wieder jeder Basisanweisung b ∈ Label
eine Transferfunktion fb zu, so definieren wir f(u,b,v) ((I[ν])ν∈N ) := fb (I[v]). Das
Ungleichungssystem besteht nun aus Ungleichungen
I[u] w fe ((I[ν])ν∈N )
für jede Basiskante e = (u, b, v) sowie
rmain w init .
Wie auch bei der Vorwärtsanalyse werden weitere Ungleichungen benötigt, die Prozeduren behandeln. Diese bestimmt man analog zur Vorwärtsanalyse. Deshalb betrachten wir in dieser Arbeit nur Vorwärtsanalysen.


2.4 Der Workset-Algorithmus
Ein Ungleichungssystem U kann mithilfe eines Worklist-Algorithmus gelöst werden.
Dieser überprüft sukzessive alle Ungleichungen. Ist eine Ungleichung nicht erfüllt,
verändert er den Wert der Variablen auf ihrer größeren“ Seite, so dass sie erfüllt
”
ist.
Ein intuitiver Ansatz für einen solchen Algorithmus ist der hier angegebene. Dabei
schreiben wir in allen folgenden Algorithmen stets x anstelle von (xi )i∈I .

2.4 Der Workset-Algorithmus

17

// initialize worklist with all inequalities of the system
of inequalities
W := ();
f o r a l l ((xi wf ( x ) ) ∈ U ) {W := W :(xi wf ( x ) )};
// initialize all variables with the minimal value ⊥ ∈ L of
the complete lattice
f o r a l l ( i∈I ) {xi :=⊥; }
// satisfy all inequalities successively ; add inequalities
to worklist , if they use manipulated variables
w h i l e W 6= () {
(xj wf ( x ) ) := head ( W ) ; W := tail ( W ) ;
t := f ( x ) ;
i f ¬( t v xj ) {
xj := xj t t ;
f o r a l l ((xk wg ( x ) ) ∈ U : g uses xj ) {W := W :(xk wg ( x ) ) ;}
}
}
Dieser Algorithmus berechnet die kleinste Lösung des Ungleichungssystems U iterativ.
Zunächst wird jeder zu berechnende Wert auf den kleinstmöglichen, also ⊥, gesetzt.
Dann wird eine Liste, die sogannte Worklist, betrachtet, die zu jedem Zeitpunkt des
Algorithmus alle potentiell unerfüllten Ungleichungen enthalten soll. Initialisiert wird
diese Liste mit allen Ungleichungen von U, da zu Beginn von keiner Ungleichung
bekannt ist, ob die Variablen sie bereits erfüllen.
Bis alle Ungleichungen erfüllt sind, geht der Algorithmus folgendermaßen vor: Zunächst erntfernt er die erste Ungleichung aus der Liste, welche die Gestalt xj w f (x)
hat, und überprüft sie. Dazu wird der Wert von f (x) mit den zu diesem Zeitpunkten
berechneten Werten der Variablen bestimmt. Falls die Ungleichung erfüllt ist, muss
nichts weiter getan werden. Andernfalls muss der Wert xj so vergrößert werden, dass
er mindestens so groß wie der Wert t ist. Anschließend müssen alle Ungleichungen,
die den Wert der Variable xj benutzen, erneut überprüft werden, und werden deshalb
an die Worklist angehängt.
Bei diesem Verfahren werden in der Tat nur diejenigen Ungleichungen erneut betrachtet, die vom Wert der Variable xj abhängen. Angehängt werden genauer

U \ (xk w f (x)) ∈ U | ∀l1 , l2 ∈ L : f (x{l1 /j}) = f (x{l2 /j}) .
Dabei definieren wir die Abbildung x{l/i} : I → L durch
(
xi für j 6= i
x{l/i}(j) :=
l
für j = i.

18

2 Grundlagen

Die neue Abbildung x{l/i} liefert für jeden Index außer i dasselbe wie x. Für den
Index i hat x{l/i} den Wert l.
Lemma 2.27. Sofern der Worklist-Algorithmus terminiert, liefert er die kleinste
Lösung des Ungleichungssystems.
Beweis. Während des Schleifendurchlaufes innerhalb des Algorithmus gelten folgende
Invarianten:
a) Die jeweils aktuell berechnete Lösung für x approximiert den kleinsten Fixpunkt
komponentenweise von unten, d.h. es gilt xi v lfp(F )i für jedes i ∈ I.
b) Jede Ungleichung, die nicht in der Worklist enthalten ist, ist aktuell erfüllt. Es
gilt also ¬(xj w f(x)) ⇒ (xj w f (x)) ∈ W.
Der Algorithmus terminiert, wenn die Worklist leer ist. Mit Gültigkeit der zweiten
Invariante ist also jede Ungleichung von U erfüllt. Also ist x in der Tat eine Lösung
des Ungleichungssystems und damit ein Präfixpunkt der Abbildung F , welche U
beschreibt. Somit gilt xi w lfp(F )i für jeden Index i ∈ I. Mit der ersten Invariante
gilt dann aber schon Gleichheit. Also stimmt x mit der kleinsten Lösung lfp(F ) von
U überein.
Wir müssen nun noch zu zeigen, dass die Invarianten tatsächlich gelten. Vor dem
ersten Schleifendurchlauf ist die erste Invariante gültig, da alle Variablen mit ⊥
initialisiert wurden. Die zweite Invariante gilt, da alle Ungleichungen und damit
insbeonsdere die nicht erfüllten in W enthalten sind.
Wir prüfen nun, dass die Invarianten beim Ausführen des Schleifenrumpfes erhalten bleiben. Zunächst einmal wird W um eine Ungleichung u verringert. Falls die
Ungleichung bereits erfüllt ist, ist nichts zu tun. Da keine Variable verändert wird,
sind auch die anderen Ungleichungen weiterhin erfüllt, die nicht in W enthalten sind.
Somit bleibt die zweite Invariante gültig.
Falls u dagegen nicht erfüllt ist, so wird die Variable der größeren“ Seite dieser
”
Ungleichung verändert. Potentiell sind danach alle Ungleichungen, die diese Variable
benutzen, nicht mehr erfüllt. Alle anderen Ungleichungen wurden nicht verändert und
sind damit weiterhin erfüllt. Da die potentiell nicht mehr gültigen Ungleichungen zu
W wieder hinzugefügt werden, enthält W nun also alle Ungleichungen, die vorher nicht
erfüllt waren, sowie alle Ungleichung, die nach Veränderung der einen Variable nicht
mehr erfüllt sein könnten. Demnach ist jede unerfüllte Ungleichung in W enthalten.
Die zweite Bedingung ist somit in der Tat invariant unter Ausführung der Schleife.
Dies gilt auch für die erste Bedingung: Sei xj w f (x) die im Schleifenrumpf betrachtete
Ungleichung u und t = f (x). Nach Annahme gilt xj v lfp(F )j . Falls xj nicht

2.4 Der Workset-Algorithmus

19

verändert wird, bleibt die Bedingung offenbar erhalten. Im anderen Fall müssen wir
xj t t v lfp(F )j nachweisen. Dazu reicht, t v lfp(F )j zu zeigen. Zunächst ist
t = f (x) v f (lfp(F )),
da f monoton ist und nach Voraussetzung x vI lfp(F ) gilt. Weiter gilt nach Konstruktion f (x) v Fj (x) für alle x und damit auch
f (lfp(F )) v Fj (lfp(F )).
Mit
Fj (lfp(F )) = lfp(F )j
folgt die Invarianz der ersten Bedingung.
Lemma 2.28. Der Algorithmus terminiert, wenn L und I endlich sind.
Beweis. Der Algorithmus berechnet in jedem Schritt neue Werte für die Worklist
und die Variablen xi . Wir bezeichnen nun die Werte, die nach dem n-ten Schritt
berechnet wurden, mit (W (n) , x(n) ) ∈ 2U × LI . Dabei ist also W (n) ∈ 2U die Liste
derjenigen Ungleichungen, die nach dem n-ten Schritt potentiell nicht erfüllt sind.
Der Vektor x(n) ∈ LI beinhaltet die im n-ten Schritt berechneten Variablenwerte. Es
ist nun zu zeigen, dass es eine natürliche Zahl n ∈ N gibt, so dass W (n) leer ist.
Die (W (n) , x(n) ) entstehen folgendermaßen: Nach Initialisierung ist W (0) die Liste,
(0)
die das Ungleichungssystem U enthält, und xi = ⊥ für jedes i ∈ I. Sei für ein
n ≥ 0 bereits (W (n) , x(n) ) konstruiert, W (n) nichtleer und u = (xj w f (x)) die
nächste betrachtete Ungleichung. Dann entsteht (W (n+1) , x(n+1) ) durch einen der
beiden folgenden Fälle:
1. Die Ungleichung u ist erfüllt. Dann ist x(n+1) = x(n) und W (n+1) = tail(W (n) ).
Insbesondere ist die neue Liste kürzer als die alte, d.h. es gilt |W (n+1) | < |W (n) |.
Dabei bezeichnen wir mit |W | die Länge einer Liste W .
2. Die Ungleichung u ist nicht erfüllt. W (n+1) entsteht aus tail(W (n) ) durch Anhängen der Ungleichungen, die xj benutzen. Außerdem ist
(
(n)
xi
falls i 6= j
(n+1)
xi
=
(n)
(n)
x t f (x ) sonst.
(n+1)

(n)

Insbesondere ist x(n+1) AI x(n) : Es ist xj
w xj nach Konstruktion. Würde
(n)
(n)
(n)
schon Gleichheit gelten, so wäre xj = xj t f (x(n) ) und damit f (x(n) ) v xj .
Dies ist ein Widerspruch dazu, dass die Ungleichung u nach der n-ten Iteration
nicht erfüllt ist.

20

2 Grundlagen

Es gilt nun (W (n) , x(n) ) 6= (W (m) , x(m) ) für alle n < m: Wir unterscheiden zwei Fälle.
Sei bei der Herleitung von (W (m) , x(m) ) aus (W (n) , x(n) ) nur der Fall 1 benutzt worden.
Dann ist |W (m) | < |W (n) | und damit (W (n) , x(n) ) 6= (W (m) , x(m) ). Also sei bei der
Herleitung mindestens einmal der Fall 2 aufgetreten. Damit ist aber x(m) AI x(n) .
Auch dann ist (W (n) , x(n) ) 6= (W (m) , x(m) ).
Sei κ := |2U × LI | die Mächtigkeit von 2U × LI . Sind nun L und I endlich, so ist
auch λ := |{f : LI → L | f monoton}| < ∞ und µ := |U| ≤ |I| · λ < ∞. Es folgt
κ ≤ 2λ · |L||I| < ∞.
Da die (W (n) , x(n) ) paarweise verschieden sind, kann es nur κ verschiedene solche
Tupel geben. Also ist nach spätestens n = κ Schritten W (n) leer und der Algorithmus
terminiert.
In Abschnitt 3.2 werden wir auch Ungleichungssysteme einführen, die unendliche viele
Ungleichungen enthalten. Darum erweitern wir das Konzept des Worklist-Algorithmus.
Im Gegensatz zu einer endliche Liste von Ungleichungen kann eine Workset beliebig
viele Ungleichungen enthalten:
W := U ;
f o r a l l ( i∈I ) {xi :=⊥; }
w h i l e W 6= () {
choose u =(xj wf ( x ) ) from W ; W := W\{u};
t := f ( x ) ;
i f ¬( t v xj ) {
xj := xj t t ;
f o r a l l ((xk wg ( x ) ) ∈ U : g uses xj ) {W := W :(xk wg ( x ) ); }
}
}
Wie zuvor berechnet dies eine Lösung des Ungleichungssystems U. Enthält das
Ungleichungssystem nun unendlich viele Ungleichungen, so kann Terminierung in
endlicher Zeit nicht garantiert werden. Da aber diese Berechnungsvorschrift im Fall
endlich vieler Variablen wieder dem zuerst vorgestellten Algorithmus entspricht,
nennen wir auch diese wieder Algorithmus.

3 Klassische Ansätze zur
interprozeduralen Analyse
Im letzten Kapitel haben wir Ungleichungssysteme und deren Lösungen betrachtet. Außerdem haben wir für einfachere Anweisungen eines Programms, sogenannte
Basisanweisungen, Ungleichungen aufgestellt, die den Datenfluss durch diese Anweisung beschreiben. Gegenstand dieses Kapitels ist nun die Behandlung der übrigen
Anweisungen, der Prozeduraufrufe.
Sharir und Pnueli [SP81] haben zwei Ansätze eingeführt, mit denen Prozeduraufrufe behandelt werden können. Der funktionale Ansatz berechnet für jede Prozedur
zunächst eine Summary-Information, die den Datenfluss durch diese Prozedur beschreibt. Damit können anschließend Prozeduraufrufe sehr ähnlich zu Basisanweisungen mithilfe von Transferfunktionen behandelt werden. Die grundlegende Idee des
Call-String-Ansatzes dagegen ist, jeden Prozeduraufruf durch die Anweisungen der
aufgerufenen Prozedur zu ersetzen und so das Programm wie eine einzige Prozedur
zu behandeln. Ziel dieses Kapitels ist, diese beiden Ansätze im Hinblick darauf zu
untersuchen, wie präzise die von ihnen berechneten Informationen sind.
Dazu werden wir in diesem Kapitel zunächst den funktionalen und den Call-StringAnsatz vorstellen und deren theoretisch beste Lösungen untersuchen. Anschließend
werden wir die Polyederanalyse betrachten, die von Cousot und Halbwachs [CH78]
eingeführt wurde und den funktionalen Ansatz variiert. Dabei werden wir zwei Möglichkeiten studieren, die Summary-Informationen berechnen. Der eine Ansatz stammt
dabei ebenfalls von Cousot und Halbwachs [CH78] und benutzt Relationen, während
Seidl et al. [SFP07] die Summary-Informationen mithilfe von Matrizenmengen bestimmen.
Der funktionale und der Call-String-Ansatz definieren Ungleichungssysteme. Wir
werden uns zuletzt also der Frage zu, ob diese durch einen Workset-Algorithmus, wie
er in Abschnitt 2.4 vorgestellt wurde, gelöst werden können.
Im Folgenden sei (L, v, F) ein monotones Framework und initL ein Startwert. Wir
schreiben id und init anstelle von idL bzw. initL , falls das zugrundeliegende L aus
dem Zusammenhang eindeutig ist. Sei weiter G = {Gp }p∈Proc ein Flussgraphsystem.
Zu jeder Basisanweisung b wählen wir eine Transferfunktion fb ∈ F.

22

3 Klassische Ansätze zur interprozeduralen Analyse

3.1 Der funktionale Ansatz
Ein Ansatz zur Berechnung von Informationen für die Punkte eines Programmes
mit Prozeduren ist, zunächst den Effekt einer jeden Prozedur p ∈ Proc durch eine
Transferfunktion zu beschreiben. Dafür bestimmen wir für jeden Programmpunkt
u ∈ Np diejenige Abbildung T [u] ∈ F, die einer Information im Startpunkt der
Prozedur p die zugehörige Information in u zuordnet. Der Effekt der Prozedur, wie
sich also Daten vom Start- bis zum Endknoten verändern, ist entsprechend die
Abbildung für den Endknoten der Prozedur T [rp ].
Da vom Startknoten zu sich selbst noch keine Transformation statt findet, ist die
Identität eine mögliche Abbildung vom Startknoten zu sich selbst. Also ist T [sp ]
mindestens so groß wie die Identität. Ist e = (u, b, v) eine Basiskante, so werden
Daten bis v so transformiert, wie es der Hintereinanderschaltung der Transformation
bis u mit der Transformation fe der Kante e entspricht. Ist e dagegen eine Kante, an
der die Prozedur q aufgerufen wird, so wird hinter die Transformation bis u der Effekt
der Prozedur q geschaltet, um eine Transformation der Daten bis v zu erhalten.
p:

id v T [sp ]

sp

T [u]

u

q:

sq

T [sq ] w id

rq

T [rq ]

b/q()
fb ◦ T [u]
T [rq ] ◦ T [u]


v T [v]

v

Abbildung 3.1: Informationsfluss im Ungleichungssystem (3.1).
Zusammen ergibt sich also das Ungleichungssystem
T [sp ] w idL für p ∈ Proc
T [v] w fb ◦ T [u] für e = (u, b, v) ∈ E Basiskante
T [v] w T [rq ] ◦ T [u] für e = (u, q(), v) ∈ E Aufrufkante

(3.1)

3.1 Der funktionale Ansatz

23

Dieses wird in Abbildung 3.1 verdeutlicht. Die dabei verwendeten Abbildungen
fT,id : F N → F,
g 7→ idL
für den Startknoten einer Prozedur,
fT,(u,b,v) : F N → F,
g 7→ fb ◦ gu
für Basiskanten und
fT,(u,q(),v) (g) : F N → F,
g 7→ grq ◦ gu
für Prozeduraufrufe sind offenbar monoton. Wir schreiben später auch abkürzend
fT,· für diese Abbildungen.
Offenbar gibt es für jedes T [u] nur endlich viele Ungleichungen. Das Ungleichungssystem (3.1) hat also die in Abschnitt 2.2 geforderte Gestalt.
Die gesuchte Information in einem Programmpunkt u ∈ Np einer Prozedur p ∈ Proc
ist weiter gegeben durch die kleinste Lösung des Ungleichungssystems
R[smain ] w init
R[v] w fb (R[u]) für e = (u, b, v) ∈ E Basiskante
R[sq ] w R[u] für e = (u, q(), v) ∈ E Aufrufkante
R[v] w T [rq ](R[u]) für e = (u, q(), v) ∈ E Aufrufkante

(3.2)

wobei R[u] ∈ L für alle u ∈ N . Die Zusammenhänge zwischen den Werten der
einzelnen R[u] werden in Abbildung 3.2 dargestellt.
Wie in Abschnitt 2.3 ist im Startknoten als Information mindestens die Startinformation init enthalten. Der Startknoten einer beliebigen Prozedur enthält die
Information des Knotens, von dem aus die Prozedur aufgerufen wurde. Für jede
Kante e = (u, s, v) enthält v die Information aus u, nachdem diese entsprechend des
Effektes der Kante e verändert wurde. Im Falle einer Basiskante ist dieser Effekt fe ,
im Falle einer Aufrufkante ist es der Effekt der aufgerufenen Prozedur q, d.h. T [rq ].
Die dabei verwendeten Abbildungen
fR,init : LN → L,
S 7→ init

24

3 Klassische Ansätze zur interprozeduralen Analyse
p:

sp

R[u]

q:

sq

u

R[sq ] w R[u]

b/q()
fb (R[u])
T [rq ](R[u])


v R[v]

v

rq

Abbildung 3.2: Informationsfluss im Ungleichungssystem (3.2).
für die Startinformation,
fR,(u,b,v) : LN → L,
S 7→ fb (Su )
für Basiskanten und
fR,(u,q(),v),ent : LN → L,
S 7→ Su
sowie
fR,(u,q(),v),ret : LN → L,
S 7→ T [rq ](Su )
für Prozeduraufrufe sind offenbar ebenfalls monoton. Wie für die verallgemeinerten
Transferfunktionen des Ungleichungssystems (3.1) schreiben wir hier abkürzend fR,·
für diese Abbildungen.
Offenbar gibt es für jedes R[u] nur endlich viele Ungleichungen. Das Ungleichungssystem (3.2) hat also die in Abschnitt 2.2 geforderte Gestalt.
Mit dem in diesem Abschnitt vorgestellten funktionalen Ansatz können Programme analysiert werden, die Prozeduren enthalten. Dazu müssen allerdings zunächst
Transferfunktionen berechnet werden, die die Effekte der Prozeduren beschreiben.

3.2 Der Call-String-Ansatz

25

Den Wert in einem Rückkehrknoten nach einem Prozeduraufruf enthält man nun
nicht aus den in dieser Prozedur berechneten Werten, sondern durch Anwenden
der für die aufgerufene Prozedur berechneten Transferfunktion auf den Wert aus
dem Aufrufknoten. Dadurch werden Reihenfolgen von Prozeduraufrufen und deren
Verschachtelungen nicht explizit behandelt. Im nächsten Abschnitt führen wir eine
Analyse ein, die die Aufrufreihenfolge von Prozeduren explizit behandelt.

3.2 Der Call-String-Ansatz
Ein anderer Ansatz zur interprozeduralen Analyse ist, eine Analyse eines Programms
mit nur einer Prozedur zu simulieren. Die Idee dabei ist, im Flussgraphen der
main-Prozedur des Programms jede Aufrufkante durch eine Kopie des Flussgraphen
der aufgerufenen Prozedur zu ersetzen. Realisiert wird dies durch Identifikation
der verschiedenen Kopien mit sogenannten Call-Strings. Diese beschreiben, welche
Prozeduraufrufe dem Aufruf der betrachteten Prozedur vorangegegangen sind, und
beschreiben die Kopie dadurch eindeutig.
Anstatt vieler Flussgraphen wird also nur ein einziger betrachtet. Dieser erweiterte
Flussgraph enthält dann nicht nur Basiskanten, die mit Basisanweisungen beschriftet
sind, sondern auch Kanten, um den Eintritt und die Rückkehr aus einer Prozedur zu
behandeln. Wir erweitern dazu die Kantenmenge E um Kanten, die den Eintritt und
die Rückkehr aus einer Prozedur beschreiben. Dabei unterscheiden wir zwei Arten
von Prozeduraufrufen: Auf der einen Seite gibt es diejenigen Aufrufe, denen eine
zugehörige Rückkehr folgt. Solche Aufrufe codieren wir durch call, die zugehörige
Rückkehr wird mit ret beschrieben. Auf der anderen Seite gibt es auch Aufrufe, bei
denen der Pfad aus dieser aufgerufenen Prozedur nicht mehr zurückkehrt. Solche
Aufrufe bezeichnen wir mit enter. Somit können wir die Ausführungspfade des
Programms beschreiben als Worte über dem Alphabet
e :={e ∈ E | e Basiskante}
E
∪ {(u, call, sq ) | ∃(u, q(), v) ∈ E}
∪ {(rq , ret, v) | ∃(u, q(), v) ∈ E}
∪ {(u, enter, sq ) | ∃(u, q(), v) ∈ E}
Diese Pfade sollen wohlgeschachtelt“ sein, d.h. jede Prozedur erst dann wieder
”
verlassen werden, wenn alle in ihr aufgerufenen Prozeduren bereits beendet wurden.
Genauer bedeutet wohlgeschachtelt“, dass der Aufruf einer Prozedur p in einem
”
Pfad, auf den später im Pfad eine zugehörige Rückkehr folgt, mit call und die
entsprechende Rückkehrkante mit ret bezeichnet wird. Sollte zwischen diesen beiden
Kanten eine weitere Prozedur q augerufen werden, so erwarten wir, dass es zwischen

26

3 Klassische Ansätze zur interprozeduralen Analyse

der Aufrufkante der Prozedur q und der Rückkehrkante der Prozedur p eine Kante
gibt, die die Rückkehr aus der Prozedur q kennzeichnet. Ist dagegen p eine Prozedur,
die im Pfad aufgerufen wird, ohne dass es im Pfad eine zugehörige Rückkehr gibt,
so wird diese Aufrufkante mit enter gekennzeichnet. Diese Bedingungen implizieren
insbesondere, dass auf eine call-Kante niemals eine enter-Kante folgen kann. Die
Menge dieser Pfade werden wir in 3.3 einführen.
Eine erste Idee, um eine intraprozedurale Analyse zu simulieren, ist es, im Flussgraphen von main eine Aufrufkante einer Prozedur p durch den zu p gehörigen
Flussgraphen zu ersetzen. Da die Benennung der Knoten eines Flussgraphen eindeutig sein muss, können verschiedene Kopien des Flussgraphen von p nicht mit
denselben Knotennamen benannt werden. Die verschiedenen Kopien unterscheiden
sich jedoch genau durch die Call-Strings.
Intuitiv beschreibt ein Call-String eine Liste von denjenigen Aufrufkanten, deren
zugehörige Prozedur noch nicht wieder beendet wurden.

ε
smain

(u1 , q1 (), v1 )
u1 enter sq1
q1 ()
v1

(u1 , q1 (), v1 ) · (u2 , q2 (), v2 )
u2 enter sq2
q2 ()
v2

u3 enter . . . enter sqn

(u1 , q1 (), v1 )
·(u2 , q2 (), v2 )
· · · (un−1 , qn−1 (), vn−1 )

q3 ()
v3

u

Abbildung 3.3: Aufbau eines Call-Strings.
Für jeden Prozeduraufruf e = (u, q(), v) ∈ Ep konkatenieren wir an die Call-Strings

3.2 Der Call-String-Ansatz

27

von p die Aufrufkante e (vergleiche auch Abbildung 3.3):
CS[main] ⊇ {ε}
CS[q] ⊇ CS[p] · e für e = (u, q(), v) ∈ Ep

(3.3)

Dabei ist CS[p] ⊆ E ∗ für jedes p ∈ Proc und CS[p] · e := {π · e | π ∈ CS[p]}. Die
kleinste Lösung, die wir mit CS bezeichnen, liefert zu jeder Prozedur dann genau
die möglichen Call-Strings. Ein Tupel (u, w) ∈ Np × CS[p] beschreibt nun diejenige
Kopie“ des Knotens u, die genau durch Prozeduraufrufe auf w entsteht. Insbesondere
”
gehören die (u, ε) ∈ Nmain × CS[main] zu dem ursprünglichen“ Flussgraphen, in den
”
die anderen hineinkopiert“ werden.
”
∗
∗
Die Abbildungen fCS,ε , fCS,e : (2E )Proc → 2E , die definiert sind durch
fCS,ε (A) := {ε}
fCS,e (A) := {w · e | w ∈ Au } für ein e ∈ E
∗

für A ∈ 2E sind offensichtlich monoton.
Offenbar gibt es für jedes CS[p] nur endlich viele Ungleichungen. Das Ungleichungssystem (3.3) hat also die in Abschnitt 2.2 geforderte Gestalt.
Jede Kopie der Prozedur p korrespondiert zu einem Aufruf der Kopie p. Wird
innerhalb derselben Prozedur q ∈ Proc an verschiedenen Kanten e1 , e2 die Prozedur
p aufgerufen, so enden die Call-Strings der Kopien auf e1 bzw. e2 und sind deshalb
verschieden. Ebenso unterscheiden sich die Aufrufkanten, wenn die aufrufenden
Prozeduren verschieden sind, und mit gleichem Argument unterscheiden sich dann
auch die Call-Strings. Wird in zwei Kopien derselben Prozedur an derselben Stelle p
aufgerufen, so unterscheiden sich die Call-Strings der aufrufenden Prozeduren und
somit auch die beiden Call-Strings der Aufrufe von p.
Somit ist es ein natürlicher Ansatz, die verschiedenen Kopien durch die zugehörigen
Call-Strings zu unterscheiden. Die gesuchte Information in einem Programmpunkt
u ∈ Np bezüglich eines Call-Strings w ∈ CS[p] ist dann gegeben durch A[u, w] ∈ L.
A[smain ](ε) w init
A[v](w) w fb (A[u](w)) für e = (u, b, v) ∈ Ep Basiskante
A[sq ](w · e) w A[u](w) für e = (u, q(), v) ∈ Ep Aufrufkante
A[v](w) w A[rq ](w · e) für e = (u, q(), v) ∈ Ep Aufrufkante
für alle p ∈ Proc und w ∈ CS[p]. Dabei ist also A : NCS → L für
[
NCS := {Np × CS[p] | p ∈ Proc}.

(3.4)

28

3 Klassische Ansätze zur interprozeduralen Analyse

ε
smain

init
w

u1

enter . . . enter s
p

A[u, w]

u

call s
q

w·e
A[sq , w · e]

b/q()
fb (A[u, w])
A[rq , w · e]


v A[v, w]

v

ret

rq

A[rq , w · e]

Abbildung 3.4: Informationsfluss im Ungleichungssystem (3.4).
Die kleinste Lösung bezeichnen wir wiederum mit A. Die Zusammenhänge zwischen
den einzelnen Informationen werden in Abbildung 3.4 verdeutlicht.
Das Ungleichungssystem entsteht folgendermaßen: Wie im funktionalen Ansatz enthält
der ursprüngliche“ Flussgraph der Prozedur main im Startknoten mindestens die
”
Startinformation init, was die erste Ungleichung widerspiegelt. Die zweite Ungleichung beschreibt, dass jeder Knoten die durch eine eingehende Basiskante veränderte
Information des Vorgängerknotens enthält, und zwar auf derselben Call-String-Ebene.
Beim Aufruf einer Prozedur wird ein Call-String w um die Aufrufkante verlängert
und so zu einem Call-String w · e. Dabei wird in den Startknoten der aufgerufenen
Prozedur mit dem entsprechend verlängerten Call-String die Information des Knotens,
an dem diese Prozedur aufgerufen wird, kopiert. Bei der Rückkehr aus dieser Prozedur
wird ebenfalls Information kopiert, und zwar aus dem Endknoten der Prozedur zum
Rückkehrknoten der aufrufenden Prozedur mit entsprechend verkürztem Call-String.
Dies wird durch die letzten beiden Ungleichungen beschrieben.
Die verallgemeinerten Transferfunktionen, die das Ungleichungssystem (3.4) beschreiben, sind dann gegeben durch
fA,init,ε : LNCS → L,
S 7→ init

3.2 Der Call-String-Ansatz

29

für die Startinformation,
fA,(u,b,v),w : LNCS → L,
S 7→ fb (Su,w )
für Basiskanten und
fA,(u,q(),v),w,ent : LNCS → L,
S 7→ Su,w
sowie
fA,(u,q(),v),w·(u,q(),v),ret : LNCS → L,
S 7→ Srq ,w·(u,q,v)
für Prozeduraufrufe. Offenbar sind diese Abbildungen monoton. Wir schreiben später
auch abkürzend fA,· für diese Abbildungen.
Offenbar gibt es für jedes A[u, w] nur endlich viele Ungleichungen. Das Ungleichungssystem (3.4) hat also die in Abschnitt 2.2 geforderte Gestalt.
Um nun die gesuchte Information in einem Knoten u zu bestimmen, haben wir also
mehrere Kopien“ dieses Knotens u angelegt und können für jede dieser Kopien eine
”
Information berechnen. Die gewünschte Information in u erhalten wir durch
Â[u] :=

G

A[u, w] | w ∈ CS[p] .

In der Praxis werden oft beschränkte Call-Strings verwendet: Ist das Programm
rekursiv, so werden die Call-Strings beliebig lang. Damit enthält aber das Ungleichungssystem (3.4) unendliche viele Variablen und ist somit in endlicher Zeit nicht
lösbar. Beschränkt man dagegen die Länge der Call-Strings, so sind nur endlich viele
Ungleichungen zu lösen. Wir werden im Folgenden aber sehen, dass unbeschränkte
Call-Strings notwendig sind, damit der Call-String-Ansatz präzise Lösungen liefert.
Wir haben in diesem Abschnitt einen Ansatz vorgestellt, der mithilfe von Call-Strings
und zusätzlichen Kanten die verschiedenen Prozeduren des Programms als eine einzige
behandelt und dadurch den Programmfluss explizit behandelt. Im folgenden Abschnitt
werden wir prüfen, ob dieser und der zuvor vorgestellte funktionale Ansatz korrekte
oder sogar präzise Lösungen liefern.

30

3 Klassische Ansätze zur interprozeduralen Analyse

3.3 Koinzidenz
In den vorigen Abschnitten haben wir zwei Ansätze zur interprozeduralen Analyse
vorgestellt. Eine andere und natürliche Herangehensweise an die Berechnung gesuchter
Informationen ist die Betrachtung aller erreichenden Pfade zu einem Programmpunkt.
Dabei werden zunächst alle Pfade bestimmt, die zu einem Programmpunkt führen,
und anschließend die Basisanweisungen entlang dieser Kanten miteinander verknpüft.
Für jeden Pfad erhält man so eine in dem Programmpunkt gültige Information. Die
kleinste obere Schranke dieser Informationen ist die gesuchte. Diese Lösung wird
MOP-Lösung genannt. Dabei steht MOP für Meet Over All Paths“. Der Name
”
kommt von der Bezeichnung Meet“ für u und stammt aus den Beginnen der Analyse,
”
wo eine Information als präziser eingestuft wird, je größer sie ist. In dieser Arbeit
wäre also die Bezeichnung Join Over All Paths (für den Join“ t) passender. Wir
”
nennen eine Analyse korrekt, wenn sie diese Lösung approximiert, und präzise, wenn
sie sogar diese Lösung berechnet. In diesem Abschnitt werden wir zunächst die
MOP-Lösungen definieren und anschließend zeigen, dass der funktionale und der
Call-String-Ansatz korrekt und unter geeigneten Voraussetzungen sogar präzise ist.
Entsprechende Sätze zur Übereinstimmung der MOP- mit der kleinsten Lösung eines
(Un-)Gleichungssystems finden sich in [NNH99].
Bevor wir die MOP-Lösung definieren können, müssen wir zunächst die Pfade definieren. Wir unterscheiden zwei Arten von Pfaden: Same-Level-Pfade sind Pfade,
die mit dem Startknoten einer Prozedur beginnen und mit einem beliebigen Knoten
derselben Prozedur enden. Von Interesse sind aber auch Pfade mit Startknoten smain ,
die Konkatenationen von Same-Level-Pfaden und Prozeduraufrufen (ohne zugehörige
Rückkehr) sind. Diese beiden Sorten von Pfaden lassen sich als kleinste Lösungen
zweier Ungleichungssysteme schreiben: Das Ungleichungssystem
SLP[sp ] ⊇ {ε}
SLP[v] ⊇ SLP[u] · e für e = (u, b, v) ∈ Ep Basiskante
(3.5)
SLP[v] ⊇ SLP[u] · (u, call, sq ) · SLP[rq ] · (rq , ret, v) für e = (u, q(), v) ∈ Ep
e∗.
liefert die Same-Level-Pfade mit SLP[u] ∈ E
Der leere Pfad ε ist ein Pfad von sp nach sp . Dies motiviert die erste Ungleichung. Ist
e = (u, b, v) eine Basiskante und π ein Same-Level-Pfad nach u, so ist offenbar die
Konkatenation π · e ein Same-Level-Pfad nach v, was die zweite Ungleichung erklärt.
Ist dagegen e = (u, q(), v) ein Prozeduraufruf, π ein Same-Level-Pfad nach u und
π 0 ein Same-Level-Pfad nach rq , so erhält man einen Same-Level-Pfad nach v wie
folgt: Zunächst konkateniert man π mit einer call-Kante zum Startknoten sq der
aufgerufenen Prozedur q. Daran wird der Same-Level-Pfad π 0 zum Rückkehrknoten
rq dieser Prozedur q angehängt. Zuletzt wird die entsprechende ret-Kante nach

3.3 Koinzidenz

31

sp

u
b
v

call s
q

w

ret

rq

Abbildung 3.5: Aufbau eines Same-Leve-Pfades.
v angefügt, die den Rückkehr aus der Prozedur beschreibt. Diese Vorgehensweise
wird durch die dritte Ungleichung ausgedrückt. Ein solcher Pfad ist schematisch in
Abbildung 3.5 illustriert. Die Definition garantiert offenbar, dass Same-Level-Pfade
wohlgeschachtelt sind.
Ähnlich sind nun die Pfade von smain zu einem beliebigen Punkt gegeben durch
GP[smain ] ⊇ {ε}
GP[u] ⊇ GP[sp ] · SLP[u] für u ∈ Np
GP[sq ] ⊇ GP[u] · (u, enter, sq ) für e = (u, q(), v) ∈ Ep ,

(3.6)

e∗.
wobei wiederum GP : N → E
Die erste Ungleichung ergibt sich wie im vorigen Ungleichungssystem. Ist e = (u, q(), v)
Kante einer Prozedur p und gibt es einen Pfad nach u, so entsteht daraus ein Pfad
nach sq durch Konkatenation einer enter-Kante nach sq an den Pfad nach u. Gibt es
einen Pfad zum Startknoten sp einer Prozedur p und einen Same-Level-Pfad zu einem
Programmpunkt u ∈ Np dieser Prozedur, so erhält man durch Konkatentation dieser
beiden Pfade einen Pfad nach u. Dies erklärt die anderen beiden Ungleichungen.
Ein solcher Pfad ist schematisch in Abbildung 3.6 zu sehen. Auch diese Definition
garantiert offenbar, dass die Pfade wohlgeschachtelt sind.

32

3 Klassische Ansätze zur interprozeduralen Analyse

smain

sp

u

enter s
q

Abbildung 3.6: Aufbau eines (beliebigen) Pfades.
Für jede Basiskante e = (u, b, v) ∈ E haben wir bereits ein fb ∈ F gewählt. Dies
erweitern wir nun für Pfade: Für π = e1 . . . ek ∈ GP[u] definieren wir
fπ = fk ◦ . . . ◦ f1 ∈ F,
wobei
(
fbi
fi :=
id

für eine Basiskante ei = (ui , bi , vi ) ∈ E
sonst.

Die Abbildung fπ beschreibt also die Verknüpfung der einzelnen Transferfunktionen
entlang der Kanten in der Reihenfolge ihrer Ausführung. Weiter definieren wir
fε := id.
Alternativ könnte man auf die Unterscheidung von enter- und call-Kanten verzichten und stattdessen die Pfade entsprechend der Ausführung der Programmes sukzessiv
bilden. Dadurch können Aufrufkanten von bereits wieder verlassenen Prozeduren nicht
von denen unterschieden werden, deren Prozeduren noch nicht abgearbeitet wurden.
In unserem Ansatz, die Pfade mithilfe eines Ungleichungssystems zu berechnen, wird
diese Unterscheidung dagegen gemacht. Dies wird im Folgenden nützlich sein, da
zum einen diese Pfade in offensichtlicher Weise wohlgeschachtelt sind und es zum
anderen direkt zu der Definition eines Call-Strings korrespondiert.
Wir wollen nun Pfade mit den Call-Strings in Verbindung bringen. Dazu definieren wir
zunächst diejenigen Pfade zum Startknoten einer Prozedur, die mit einem gegebenen

3.3 Koinzidenz

33

Call-String korrespondieren. Sei dazu p ∈ Proc eine Prozedur und w ∈ CS[p] ein
Call-String der Gestalt w = (u1 , p1 (), v1 ) . . . (un , pn (), vn ) mit pn = p. Wir erhalten
nun die passenden Pfade zu einem Knoten u ∈ Np , indem wir zunächst an einen
Same-Level-Pfad zum Knoten u1 eine enter-Kante nach sp1 hängen. Daran wiederum
konkatenieren wir einen Same-Level-Pfad nach u2 und setzen dies solange fort, bis
daraus ein Pfad nach sp entstanden ist. An diesen hängen wir zuletzt einen SameLevel-Pfad nach u an. Diese Pfade sind also gegeben durch
P(u, w) := {π1 · (u1 , enter, sp1 ) · π2 · · · (un , enter, sp ) · πn+1 | πi ∈ SL[ui ]}.
Dabei sei un+1 = u. Die Menge aller möglichen Pfade nach u erhalten wir nun, indem
wir die Pfade bezüglich aller Call-Strings von p vereinigen. Dies zeigt das folgende
Lemma.
Lemma 3.1. Für jede Prozedur p ∈ Proc und jeden Knoten u ∈ Np gilt
GP[u] =

[

P(u, w) | w ∈ CS[p] .

S
Beweis. Seien p ∈ Proc, u ∈ Np und P(u) := {P(u, w) | w ∈ CS[p]} die Menge der
Pfade nach u, die zu einem Call-String korrespondieren. Um GP[u] ⊆ P(u) zu zeigen,
rechnen wir nach, dass (P(ν))ν∈N eine Lösung des Ungleichungssystem (3.6) ist.
Sei also zunächst u = smain . Es ist
P(smain ) ⊇ P(smain , ε) ⊇ {ε}
und die erste Ungleichung des Ungleichungssystems ist erfüllt.
Sei nun u ∈ Np beliebig. Zu zeigen ist P(u) ⊇ P(sp ) · SLP[u]. Sei π ∈ P(sp ). Dann
gibt es einen Call-String w mit π ∈ P(sp , w) und π hat die Gestalt
π = π1 · (u1 , enter, sp1 ) · π2 · · · (un , enter, sp ) · πn+1
wie in Abbildung 3.7 mit πi ∈ SLP[ui ] für 1 ≤ i ≤ n und πn+1 ∈ SLP[sp ]. Für einen
beliebigen Same-Level-Pfad π 0 ∈ SLP[u] ist nach Konstruktion auch
πn+1 · π 0 ∈ SLP[u].
Dann ist aber nach Definition
π · π 0 ∈ P(u, w) ⊆ P(u).
Somit gilt auch die zweite Ungleichung.

34

3 Klassische Ansätze zur interprozeduralen Analyse

smain

π1
u1 enter sp1
π2
u2

πn+1
un enter sp
π0
u

Abbildung 3.7: Beweis von Lemma 3.1, P(u) ⊇ P(sp ) · SLP[u].
Sei nun e = (u, q(), v) ∈ Ep eine Aufrufkante. Zu zeigen ist P(sq ) ⊇ P(u)·(u, enter, sq ).
Sei also π ∈ P(u). Dann gibt es einen Call-String w ∈ CS[p], so dass π ∈ P(u, w).
Der Pfad π hat also die Gestalt
π = π1 · (u1 , enter, sp1 ) · π2 · · · (un , enter, sp ) · πn+1
wie in Abbildung 3.8 mit πi ∈ SLP[ui ] für 1 ≤ i ≤ n und πn+1 ∈ SLP[u]. Nun ist
nach Definition
w · e ∈ CS[p]
und damit
π · (u, enter, sq ) ∈ P(sq , w · e).

Für die andere Inklusion seien p ∈ Proc, u ∈ Np und w ∈ CS[p] beliebig. Es genügt,
P(u, w) ⊆ P[u] zu zeigen. Dies geschieht durch vollständige Induktion nach der Länge
n des Call-Strings w.

3.3 Koinzidenz

35

smain

π1
u1 enter sp1
π2
u2

un enter sp
πn+1
u

enter s
q

Abbildung 3.8: Beweis von Lemma 3.1, P(sq ) ⊇ P(u) · (u, enter, sq ).
Sei zunächst n = 0. Dann ist der Call-String w bereits das leere Wort und wir erhalten
P(u, w) = P(u, ε) = {π · π 0 | π ∈ SLP[sp ] ∧ π 0 ∈ SLP[u]} = SLP[u] ⊆ GP[u].
Letztere Inklusion resultiert daraus, dass w = ε bereits p = main impliziert.
Gelte die Behauptung nun für alle Pfade der Länge kleiner oder gleich k. Sei w ein CallString der Länge k + 1. Dann ist w von der Form w = w
e · ee, wobei ee = (e
u, p(), ve) ∈ Nq
für eine Prozedur q ∈ Proc.
Wir können einen Pfad π ∈ P(u, w) nun schreiben als
π=π
e · (e
u, enter, sp ) · π 0
für Pfade π
e ∈ P(e
u, w)
e und π 0 ∈ SLP[u]. Betrachte dazu auch Abbildung 3.9.
Nach Induktionsvoraussetzung ist P(e
u, w)
e ⊆ GP[e
u]. Das Ungleichungssystem (3.6)
zur Definition der Pfade liefert nun, dass mit π
e ∈ GP[e
u]
π
e · (e
u, enter, sp ) ∈ GP[sp ]

36

3 Klassische Ansätze zur interprozeduralen Analyse

smain

w
e
sq

e · ee
enter s w = w
p

u
e

π0

ee
ve

u

Abbildung 3.9: Beweis von Lemma 3.1, Induktionsschritt.
und weiter
π=π
e · (e
u, enter, sp ) · π 0 ∈ GP[u]
gilt. Es folgt die Behauptung.
Wir haben nun verschiedene Pfade definiert: Zum einen Same-Level-Pfade, die vom
Startknoten einer Prozedur zu einem Knoten derselben Prozedur führen, zum anderen
beliebige Pfade, die im Startknoten des Programms beginnen und zu einem Knoten
einer beliebigen Prozedur führen. Weiter haben wir für jeden Call-String die Menge
derjenigen Pfade definiert, deren enter-Kanten zum Call-String korrespondieren.
Zuletzt haben wir in Lemma 3.1 einen Zusammenhang zwischen den beiden letzteren
Mengen hergestellt.
Wir können nun die MOP-Lösung definieren durch
MOP[u] := {fπ (init) | π ∈ GP[u]}
für u ∈ N .
Definition 3.2. Eine constraint-basierte Datenflussanalyse mit Ungleichungssystem
U heißt
• korrekt, falls MFP[u] w MOP[u] für alle u ∈ N gilt.

3.3 Koinzidenz

37

• präzise, falls MFP = MOP gilt.
Dabei bezeichnet MFP die kleinste Lösung des Ungleichungssystems U.
Wir können nun zeigen, dass der funktionale und der Call-String-Ansatz korrekt
sind. Stellen wir weiter geeignete Forderungen an die Transferfunktionen, so sind die
Ansätze sogar präzise. Insbesondere liefern sie dann dasselbe Resultat. Wir beginnen
mit dem funktionalen Ansatz.
Lemma 3.3. Für jedes u ∈ N gilt
G
T [u] w
fπ | π ∈ SLP[u] .
Ist (L, v, F) universell-distributiv oder positiv-distributiv und in letzterem Fall weiter
jeder Programmpunkt erreichbar, so gilt sogar für jedes u ∈ N
G
T [u] =
fπ | π ∈ SLP[u] .
Beweis. Wir schreiben abkürzend Mu := {fπ | π ∈ SLP[u]}.
Zunächst F
zeigen wir, dass jedes Element von Mu kleiner oder gleich T [u] ist. Daraus folgt Mu v T [u]. Für die Gleichheit müssen
F wir dann noch die umgekehrte
Ungleichung zeigen. Dazu rechnen wir nach, dass ( Mν )ν∈N eine Lösung des Ungleichungssystems (3.1) ist.
a) Wir zeigen folgende Aussage durch vollständige Induktion nach k ∈ N: Für
u ∈ N und einen Pfad π ∈ SLP[u] der Länge kleiner oder gleich k ist fπ v T [u].
Seien also u ∈ N and π ∈ SLP[u]. Falls π die Länge 0 hat, gilt π = ε und
u = sp . Damit folgt fπ = id v T [sp ].
Gelte die Behauptung für Pfade, deren Länge kleiner oder gleich k ∈ N ist. Sei π
ein Pfad der Länge k + 1, d.h. π = e1 . . . ek ek+1 , wobei ek+1 = (uk , s, u). Gemäß
der Definition von Same-Level-Pfaden kann die letzte Kante ek+1 weder eine
Eintritts- noch eine Aufrufkante sein. Also ist ek+1 entweder eine Basiskante
oder eine Rückkehrkante. Wir unterscheiden also zwei Fälle:
i. Sei ek+1 = (uk , b, u) ∈ E eine Basiskante. Dann ist π̃ := e1 . . . ek ∈ SLP[uk ]
ein Pfad nach uk der Länge k. Nach Induktionsvoraussetzung ist fπ̃ v T [uk ].
Weiter ist fk+1 = fb und damit
fπ v fb ◦ T [uk ] v T [u]
gemäß der Definition des Ungleichungssystems T .

38

3 Klassische Ansätze zur interprozeduralen Analyse

smain

π0
ui−1 call

ei

sq
π 00

u

ret
ek+1

rq

Abbildung 3.10: Beweis von Lemma 3.3, Induktionsschritt.
ii. Sei ek+1 eine Rückkehrkante, d.h. ek+1 = (rq , ret, u) für ein q ∈ Proc mit
zugehöriger Aufrufkante ei = (ui−1 , call, sq ) für ein 1 ≤ i < k, so dass π =
π 0 · ei · π 00 · ek+1 wie in Abbildung 3.10 für Pfade π 0 = e1 . . . ei−1 ∈ SLP[ui−1 ]
und π 00 = ei+1 . . . ek ∈ SLP[rq ] und eine Aufrufkante e = (ui−1 , q(), u) ∈ E.
Nach Induktionsvoraussetzung ist nun fπ0 v T [ui−1 ] und fπ00 v T [rq ]. Damit
gilt
fπ = fπ00 ◦ fπ0 v T [rq ] ◦ T [ui−1 ].
Es folgt die gewünschte Ungleichung.
F
b) Um zu zeigen, dass ( Mν )ν∈N eine Lösung von (3.1) ist, müssen wir folgende
Ungleichungen prüfen:
G

Msp

G

Mv

G

Mv

w id

(3.7)
G

w fb ◦ Mu für eine Basiskante e = (u, b, v) ∈ E
(3.8)
G
G
w Mrq ◦ Mu für eine Aufrufkante e = (u, q(), v) ∈ E. (3.9)

Es gilt für alle p ∈ Proc
G


Msp = fπ | π ∈ SLP[sp ] w fε = id

vermöge ε ∈ SLP[sp ]. Also gilt die Ungleichung (3.7).

3.3 Koinzidenz

39

Sei weiter e = (u, b, v) ∈ E eine Basiskante. Dann ist

Mv = fπ | π ∈ SLP[v]


⊇ fπ | π ∈ SLP[v] ∧ (∃π̃ ∈ SLP[u] : π = π̃ · e }

= fπ̃·e | π̃ ∈ SLP[u]

= fb ◦ fπ̃ | π̃ ∈ SLP[u] .
Damit folgt
G

Mv w

G

fb ◦ fπ̃ | π̃ ∈ SLP[u] = fb ◦

G

fπ̃ | π̃ ∈ SLP[u] = fb ◦

G

Mu ,

wobei die mittlere Gleichheit aus folgender Tatsache resultiert: Falls (L, v, F)
universell-distributiv ist, folgt sie gerade aus der Definition. Falls (L, v, F)
positiv-distributiv ist, gilt die Aussage nur, falls Mu nicht leer ist. Andererseits
ist aber Mu genau dann leer, wenn SLP[u] leer ist. Dies wiederum ist genau
dann der Fall, wenn u nicht erreichbar ist. Da wir aber im Falle der positiven
Distributivität von (L, v, F) die Erreichbarkeit eines jeden Programmpunktes
vorausgesetzt hatten, ist Mu nicht leer. Es folgt die Gültigkeit der Ungleichung
(3.8).
Sei zuletzt e = (u, q(), v) ∈ E eine Aufrufkante, dann gilt


fπ | π ∈ SLP[v]

⊇ fπ | π ∈ SLP[v] ∧ (∃π̃1 ∈ SLP[u], π̃2 ∈ SLP[rq ] :
π = π̃1 · (u, call, sq ) · π̃2 · (rq , ret, v))


= f(rq ,ret,v) ◦ fπ̃2 ◦ f(u,call,sq ) ◦ fπ̃1 | π̃1 ∈ SLP[u], π̃2 ∈ SLP[rq ]

= fπ̃2 ◦ fπ̃1 | π̃1 ∈ SLP[u], π̃2 ∈ SLP[rq ] .
Weiter ist für jedes π̂2 ∈ SLP[rq ]



fπ̃2 ◦ fπ̃1 | π̃1 ∈ SLP[u], π̃2 ∈ SLP[rq ] ⊇ fπ̂2 ◦ fπ̃1 | π̃1 ∈ SLP[u] .

Also ist
G

Mv w

G

fπ̃2 ◦ fπ̃1 | π̃1 ∈ SLP[u], π̃2 ∈ SLP[rq ]

w

G

fπ̂2 ◦ fπ̃1 | π̃1 ∈ SLP[u]

40

3 Klassische Ansätze zur interprozeduralen Analyse
für jedes π̂2 ∈ SLP[rq ]. Daraus folgt in Analogie zu obiger Argumentation mit
der jeweiligen Distributivität
G
G G 
Mv w
fπ̂2 ◦ fπ̃1 | π̃1 ∈ SLP[u] | π̃2 ∈ SLP[rq ]
G
G
=
fπ̂2 ◦
fπ̃1 | π̃1 ∈ SLP[u] | π̃2 ∈ SLP[rq ]
G
G
fπ̃1 | π̃1 ∈ SLP[u]
=
fπ̂2 | π̃2 ∈ SLP[rq ] ◦
G
G
= Mrq ◦ Mu .
Dies beweist Ungleichung (3.9) und damit die Behauptung.

Satz 3.4. Für jedes u ∈ N gilt
R[u] w MOP[u].
Ist (L, v, F) universell-distributiv oder positiv-distributiv und in letzterem Fall weiter
jeder Programmpunkt erreichbar, so gilt sogar für jedes u ∈ N
R[u] = MOP[u].
Beweis. Der Aufbau des Beweises ist analog zu dem vorangegangenen. Dazu definieren
wir Mu := {fπ (init) | π ∈ P [u]}.
a) Wir führen einen Induktionsbeweis über k ∈ N: Falls u ∈ N und π ∈ GP[u] ein
Pfad der Länge kleiner oder gleich k ∈ N ist, so gilt fπ (init) v R[u].
Seien also u ∈ N und π ∈ GP[u]. Falls π die Länge 0 hat, so ist π = ε.
Insbesondere ist u = smain und
fε (init) = init v R[smain ].
Gelte die Behauptung bereits für Pfade der Länge kleiner oder gleich k ∈ N
und sei π ∈ GP[u] ein Pfad der Länge k + 1, d.h. π = e1 . . . ek ek+1 , wobei
ek+1 = (uk , s, u). Dann ist π̃ := e1 . . . ek ∈ P [uk ] ein Pfad der Länge k und mit
der Monotonie von fk+1 erhalten wir nach Induktionsvoraussetzung
fπ (init) = fk+1 (fπ̃ (init)) v fk+1 (R[uk ]).
Nach Definition von GP[u] kann die letzte Kante ek+1 von π eine Basis-, Eintrittsoder Rückkehrkante sein. Wir unterscheiden also drei Fälle:
i. Sei ek+1 = (uk , b, u) ∈ E eine Basiskante. Dann gilt fk+1 = fb und damit
fπ (init) v fb (R[uk ]) v R[u]
nach Definition des Ungleichungssystems R.

3.3 Koinzidenz

41

ii. Sei ek+1 eine Eintrittskante, d.h. ek+1 = (uk , enter, sq ) für ein q ∈ Proc
und u = sq . Damit ist fk+1 = id, woraus
fπ (init) v R[uk ]
folgt. Weiter existiert eine Kante e = (uk , q(), v) ∈ E und somit ist nach
Definition des Ungleichungssystems R auch
R[uk ] v R[u].
Zusammen folgt
fπ (init) v R[u].
iii. Sei ek+1 eine Rückkehrkante, d.h. ek+1 = (rq , ret, u) für ein q ∈ Proc und
fk+1 = id. Dann gibt es eine zugehörige Aufrufkante ei = (ui−1 , call, sq )
für ein 1 ≤ i < k. Sei π 0 := e1 . . . ei−1 ∈ P [ui−1 ] ein Pfad der Länge
i − 1 ≤ k und π 00 := ei+1 . . . ek ∈ SLP[rq ] wie auch in Abbildung 3.10 zum
Beweis von Lemma 3.3.
Dann gilt π = π 0 · ei · π 00 · ek+1 und damit fπ = fπ00 ◦ fπ0 . Nach Induktionsvoraussetzung ist dann
fπ0 (init) v R[ui−1 ].
Mit der Monotonie von fπ00 ist
fπ (init) = fπ00 ◦ fπ0 (init)
v fπ00 (R[ui−1 ]).
Da nach Lemma 3.3 fπ00 v T [rq ] gilt, ist weiter
fπ00 (R[ui−1 ]) v T [rq ](R[ui−1 ])
v R[u].
Die letzte Ungleichung folgt dabei aus der Definition des Ungleichungssystems (3.1) zur Berechnung der Summary-Informationen. Zusammen gilt
also
fπ (init) v R[u].
Es folgt die Behauptung.

42

3 Klassische Ansätze zur interprozeduralen Analyse

b) Für die andere Richtung prüfen wir
G
Msmain
w init
G
G

Mv
w fb
Mu für eine Basiskante e = (u, b, v)
G
G
Msq
w
Mu für eine Aufrufkante e = (u, q(), v)
G
G

Mv
w T [rq ]
Mu für eine Aufrufkante e = (u, q(), v).

(3.10)
(3.11)
(3.12)
(3.13)

Es ist
Msmain = {fπ (init) | π ∈ GP[smain ]} 3 fε (init) = init
vermöge ε ∈ GP[smain ]. Damit folgt
G
Msmain w init,
also die Gültigkeit der Ungleichung (3.10).
Sei e = (u, b, v) ∈ E eine Basiskante. Dann gilt {π · e | π ∈ GP[u]} ⊆ GP[v]
und analog zum Beweis von Lemma 3.3 folgt Ungleichung (3.11) mit
G
G
G

Mv w
fb (fπ̃ (init)) | π̃ ∈ GP[u] = fb
Mu .
Sei nun (u, q(), v) ∈ E eine Aufrufkante. Dann ist
{π · (u, enter, sq ) | π ∈ GP[u]} ⊆ GP[sq ]
und
{π · (u, call, sq ) · π̃ · (rq , ret, v) | π ∈ GP[u] ∧ π̃ ∈ SLP[rq ]} ⊆ GP[v].
Damit folgt einerseits Ungleichung (3.12) aus
G
G
G
G
Msq w
fπ·(u,enter,sq ) | π ∈ GP[u] =
fπ | π ∈ GP[u] =
Mu
und andererseits Ungleichung (3.13), wobei die jeweilige Distributivitätseigenschaft wie im Beweis von Lemma 3.3 benutzt wird, mit
G
G
Mv w
fπ·(u,call,sq )·π̃·(rq ,ret,v) (init) | π ∈ GP[u] ∧ π̃ ∈ SLP[rq ]
G
=
fπ̃ ◦ fπ (init) | π ∈ GP[u] ∧ π̃ ∈ SLP[rq ]
G
G

fπ (init) | π̃ ∈ GP[u]
=
fπ̃ | π̃ ∈ SLP[rq ]
G
G

=
fπ̃ | π̃ ∈ SLP[rq ]
fπ (init) | π̃ ∈ GP[u]
G

= T [rq ]
(Mu ) .
Die letzte Gleichheit folgt dabei aus Lemma 3.3. Es folgt die Behauptung.

3.3 Koinzidenz

43

Wir betrachten nun den Call-String-Ansatz.
Lemma 3.5. Für jedes (u, w) ∈ NCS gilt
A[u, w] w

G

fπ (init) | π ∈ GP(u, w) .

Ist (L, v, F) universell-distributiv oder positiv-distributiv und in letzterem Fall weiter
jeder Programmpunkt erreichbar, so gilt sogar für jedes (u, w) ∈ NCS
A[u, w] =

G

fπ (init) | π ∈ GP(u, w) .

Beweis. Dieses Lemma beweisen wir wie die beiden vorherigen, indem wir beide
Ungleichungen zeigen. Dazu sei Mu,w := {fπ (init) | π ∈ GP(u, w)}.
a) Wir zeigen wieder durch vollständige Induktion nach k ∈ N: Falls (u, w) ∈ NCS
und π ∈ GP(u, w) ein Pfad der Länge kleiner oder gleich k ∈ N ist, so gilt
fπ (init) v A[u, w].
Sei also (u, w) ∈ NCS . Für einen Pfad π ∈ GP(u, w) der Länge k = 0 gilt π = ε.
Insbesondere ist u = smain und w = ε. Damit folgt
fε (init) = init v A[smain , ε].
Gelte die Behauptung nun für Pfade der Länge kleiner oder gleich k ∈ N und
sei π ein Pfad der Länge k + 1, d.h. π = e1 . . . ek ek+1 , wobei ek+1 = (uk , s, u).
Wiederum betrachten wir die drei Fälle, dass die letzte Kante ek+1 von π eine
Basis-, Eintritts- oder Rückkehrkante ist. Wir schreiben wieder π̃ = e1 · · · ek .
i. Sei ek+1 = (uk , b, u) ∈ E eine Basiskante. Dann ist auch π̃ ∈ GP(uk , w)
und weiter fk+1 = fb . Somit gilt fπ̃ (init) v A[uk , w] nach Induktionsvoraussetzung. Weiter ist
fπ (init) = fk+1 (fπ̃ (init)) v fb (A[uk , w]) v A[u, w]
vermöge der Definition des Ungleichungssystems A.
ii. Sei ek+1 eine Eintrittskante, d.h. ek+1 = (uk , enter, sp ), mit zugehöriger
Aufrufkante e = (uk , p(), v) ∈ Eq für ein q ∈ Proc, so dass w = w̃ · e für ein
w̃ ∈ CS[q]. Dann ist fk+1 = id und weiter nach Induktionsvoraussetzung
fπ (init) = fπ̃ (init) v A[uk , w̃] v A[sq , w̃ · e] = A[u, w]
gemäß der Definition des Ungleichungssystems A.

44

3 Klassische Ansätze zur interprozeduralen Analyse
iii. Sei ek+1 eine Rückkehrkante, d.h. ek+1 = (rq , ret, u) und es gibt eine
Kante e = (ui , q(), u) ∈ Ep für ein q ∈ Proc und 1 ≤ i ≤ k. Aus w ∈ CS[p]
folgt w · e ∈ CS[q]. Hieraus erhalten wir zusammen mit fk+1 = id und der
Induktionsvoraussetzung
fπ (init) = fπ̃ (init) v A[rq , w̃ · e] v A[u, w]
vermöge der Definition des Ungleichungssystems A. Es folgt die gewünschte
Ungleichung.

b) Wir zeigen für jedes (u, w) ∈ NCS
G
Mmain,ε
w init
G
G

Mv,w
w fe
Mu,w für eine Basiskante e = (u, b, v) ∈ Ep
G
G
Msq ,w·e
w
Mu,w für eine Aufrufkante e = (u, q(), v) ∈ Ep
G
G
Mv,w
w
Mrq ,w·e für eine Aufrufkante e = (u, q(), v) ∈ Ep

(3.14)
(3.15)
(3.16)
(3.17)

Zunächst folgt (3.14) direkt mit
Msmain ,ε = {fπ (init) | π ∈ GP(smain , ε)}
⊇ {fπ (init) | π = ε}
= {init}.
Sei nun e = (u, b, v) ∈ Ep eine Basiskante und w ∈ CS[p]. Dann folgt aus
π ∈ GP(u, w) schon π · e ∈ GP(v, w). Somit ist, wobei wir die Distributivitätseigenschaften der Transferfunktionen wie im Beweis von 3.4 benutzen,
G
G
Mv,w =
fπ (init) | π ∈ GP(v, w)
G
w
fπ̃·e (init) | π̃ ∈ GP(u, w)
G

= fb
fπ̃ (init) | π̃ ∈ GP(u, w)
= fb (Mu,w )
und Ungleichung (3.15) ist gezeigt.
Sei e = (u, q(), v) ∈ Ep eine Aufrufkante und w ∈ CS[p]. Dann ist

π̃ · (u, call, sq ) | π̃ ∈ GP(u, w) ⊆ GP(sq , w · e)
und

π̃ · (rq , ret, v) | π̃ ∈ GP(rq , w · e) ⊆ GP(v, w).

3.3 Koinzidenz

45

Somit gilt einerseits

Msq ,w·e = fπ (init) | π ∈ GP(sq , w · e)

⊇ fπ̃·(u,call,sq ) (init) | π̃ ∈ GP(u, w)

= fπ̃ (init) | π̃ ∈ GP(u, w)
= Mu,w .
Daraus folgt direkt (3.16). Andererseits ist

Mv,w = fπ (init) | π ∈ GP(v, w)

⊇ fπ̃·(rq ,ret,v) (init) | π̃ ∈ GP(rq , w · e)

= fπ̃ (init) | π̃ ∈ GP(rq , w · e)
= Mrq ,w·e
und auch Ungleichung (3.17) ist erfüllt. Es folgt die Behauptung.
Satz 3.6. Für jedes u ∈ N gilt
Â[u] w MOP[u].
Ist (L, v, F) universell-distributiv oder positiv-distributiv und in letzterem Fall weiter
jeder Programmpunkt erreichbar, so gilt sogar für jedes u ∈ N
Â[u] = MOP[u].
Beweis. Seien p ∈ Proc und u ∈ Np . Aus dem vorigen Lemma 3.5 folgt nun
G

A[u, w] | w ∈ CS[p]
GG
v
{fπ (init) | π ∈ GP(u, w)} | w ∈ CS[p]
G
[
=
fπ (init) | π ∈
GP(u, w) | w ∈ CS[p]
G
=
fπ (init) | π ∈ GP[u]

Â[u] =

und daraus die erste Behauptung. Mit den entsprechenden Voraussetzung an die
Distributivität der Transferfunktionen gilt sogar überall Gleichheit.
Wir haben nun alle nötigen Aussagen beisammen, um beweisen zu können, dass
der funktionale und der Call-String-Ansatz unter geeigneten Voraussetzungen an die
verwendeten Transferfunktionen in der Tat dieselbe präziseste Information liefern:

46

3 Klassische Ansätze zur interprozeduralen Analyse

Korollar 3.7 (Koinzidenztheorem). Für jeden Knoten u ∈ N gilt
Â[u] v R[u].
Ist (L, v, F) universell-distributiv oder positiv-distributiv und in letzterem Fall weiter
jeder Programmpunkt erreichbar, so gilt
Â[u] = R[u]
für jeden Knoten u ∈ N .
Beweis. Dies folgt direkt aus Satz 3.4 und Satz 3.6.
Bemerkung 3.8. Wir haben in Abschnitt 3.2 bereits erwähnt, dass in der Praxis oft
die Länge der Call-Strings beschränkt wird. Können im Programm Call-Strings beliebiger Längen auftreten, so ist die Menge der beschränkten Call-Strings CSbeschr [p]
eine echte Teilmenge der Menge aller Call-Strings. Sind die Transferfunktionen
universell-distributiv oder positiv-distributiv und in letzterem Fall alle Programmpunkte erreichbar, so folgt aus dem Beweis von Lemma 3.6 und Satz 3.7
G
MOP[u] =
fπ (init) | π ∈ GP[u]
G
=
A[u, w] | w ∈ CS[p]
G
A
A[u, w] | w ∈ CSbeschr [p] .
Es gilt also keine Koinzidenz, wenn wir die Call-Strings beschränken. Darum werden
wir im Folgenden stets nur unbeschränkte Call-Strings betrachten.

In diesem Abschnitt haben wir zwei Ansätze zur Behandlung von Prozeduren vorgestellt: Zum einen den Call-String-Ansatz, der mithilfe von Call-Strings alle Prozeduren
eines Programms wie eine einzige behandelt, zum anderen den funktionalen Ansatz,
der die Prozeduren getrennt betrachtet und jeder Prozedur ihren Effekt zuordnet. Wir
haben gezeigt, dass beide Ansätze korrekte constraint-basierte Datenflussanalysen
sind. Zuletzt haben wir gesehen, dass unter geeigneten Annahmen an die Distributivität der verwendeten Transferfunktionen beide Ansätze gleichwertig sind: Falls
das zugrundeliegende monotone Framework universell-distributiv ist oder zumindest positiv-distributiv ist und in letzterem Fall zusätzlich alle Programmpunkte
erreichbar sind, sind sowohl der funktionale als auch der Call-String-Ansatz präzise
constraint-basierte Datenflussanalysen und beide berechnen insbesondere dasselbe
Ergebnis.
Oft ist die Transferfunktion, die als Effekt einer Prozedur berechnet wurde, nicht endlich darstellbar. Es muss also eine andere, endliche Darstellung gefunden werden. Im

3.4 Polyederanalyse

47

nächsten Abschnitt stellen wir mit der Polyederanalyse dafür ein Beispiel vor. Anstelle
von Transferfunktionen berechnen wir dort auf zwei verschiedene Arten SummaryInformationen, aus denen wir wiederum Transferfunktionen zum Beschreiben des
Effektes der Prozedur herleiten können.

3.4 Polyederanalyse
Ziel der P
Polyederanalyse ist, zu jedem Programmpunkt (affine) Ungleichungen der
Gestalt ni=1 ai xi ≥ a0 zu bestimmen, welche von den Programmvariablen erfüllt
werden. Damit kann beispielsweise überprüft werden, ob ein Index innerhalb gewisser
Array-Grenzen liegt. Geometrisch bilden die Variablenwerte, die solche Ungleichungen
erfüllen, ein konvexes Polyeder. Die Polyederanalyse ist ein Beispiel für eine interprozedurale Datenflussanalyse. Zur Berechnung gültiger affiner Ungleichungen stellen wir
in diesem Abschnitt zunächst Ungleichungssysteme zur Berechnung der erreichbaren
Werte auf. In Abschnitt 4.4 werden wir diese dann zu Ungleichungssystemen erweitern,
deren Lösungen tatsächlich affine Ungleichungen beschreiben.
Ein in dieser Hinsicht zu untersuchendes Programm habe eine endliche Menge
Proc von Prozeduren und sei im Folgenden durch ein Flussgraphsystem {Gp }p∈Proc
wie in Abschnitt 2.3 gegeben. Dabei habe das Programm n (globale) Variablen
x1 , . . . , xn , welche Werte x1 , . . . , xn in R annehmen. AlsP
einzigen Basisanweisungen
betrachten wir affine Zuweisungen der Form xj := a0 + ni=1 ai xi fürP
ein 1 ≤ j ≤ n.
n
In den kommenden Abschnitten werden wir
Pn meist t anstelle von a0 + i=1 ai xi und
entsprechend xj := t anstatt xj := a0 + i=1 ai xi schreiben.
Im Folgenden geben wir zwei Ansätze an, die ähnlich dem funktionalen Ansatz
zunächst Summary-Informationen für die Prozeduren berechnen, und vergleichen
diese: Der erste Ansatz verwendet Matrizenmengen und basiert auf [SFP07], während
der zweite Ansatz Relationen als Summary-Informationen berechnet und in [CH78]
zu finden ist.

3.4.1 Framework und Zuweisungen
Ein Zustand ist ein Vektor (1, x1 , . . . , xn ) ∈ {1} × Rn , der die Werte der Variablen
enthält. Die zusätzliche erste Komponente 1 dient dazu, die Transferfunktion einer
affinen Zuweisung mithilfe einer linearen Abbildung darstellen zu können. Wir bezeichnen mit Σ := {1} × Rn den Raum der möglichen Zustände. Die Analyse zur
Bestimmung der erreichbaren Zustände ist nun auf Mengen von solchen Zuständen
definiert, also auf dem vollständigen Verband (L, v) := (2Σ , ⊆). Zusammen mit

48

3 Klassische Ansätze zur interprozeduralen Analyse

der Menge F der universell-distributiven Abbildungen L → L ist (L, ⊆, F) also ein
universell-distributives Framework.
Wir bezeichnen mit Mat(n) die Menge der reellen n × n-Matrizen. Weiter sei
Mat(Σ) := {A ∈ Mat(n + 1) | a00 = 1 ∧ ∀1 ≤ j ≤ n. a0j = 0}
die Menge derjenigen reellen (n + 1) × (n + 1)-Matrizen, die Zustände aus Σ wieder
auf Zustände aus Σ abbilden. Man sieht leicht, dass tatsächlich jede Matrix, die alle
Elemente aus Σ wieder nach Σ abbildet, von dieser Gestalt ist. Setzen wir


Ij
0
0
Mxj :=t := a0 · · · aj−1 aj aj+1 · · · an  ,
0
0
In−j
wobei Ik ∈ Mat(k) die Einheitsmatrix für ein k ≥ 1 ist, können wir damit den Effekt
der Zuweisung xj := t durch
 
 
1
1


Ij
0
0
 x̃1 
 x1 
 
 
 ..  := a0 · · · aj−1 aj aj+1 · · · an  ·  .. 
.
.
0
0
In−j
x̃n
xn
P
ausdrücken. Es ist x̃j = a0 + ni=1 ai xi . Weiter gilt für 1 ≤ i ≤ n und i 6= j offenbar
x̃i = xi . Das beschreibt die Tatsache, dass xj die einzige veränderte Variable ist, und
diese genau gemäß der Vorschrift der Zuweisung verändert wurde.
Mit anderen Worten weisen wir einer Kante e = (u, xj := t, v) ∈ E die Transferfunktion
f(u,xj :=t,v) : LN → L,
S 7→ fxj :=t (Su )
zu. Dabei ist S = (Sν )ν∈N und
fxj :=t : L → L,
S 7→ {Mxj :=t · s | s ∈ S}.
Wir wollen nun zunächst die in einem jeden Programmpunkt erreichbaren Zustände
berechnen. Dazu bestimmen wir zunächst die Effekte der Prozeduren, um damit das
Ungleichungssystem (3.2) aufstellen und lösen zu können. Die Effekte wollen wir auf
zwei verschiedene Arten berechnen. In beiden Fällen werden wir die Abbildungen nicht
direkt aus F wählen, sondern zunächst über einem anderen Raum definieren. Die dann
berechneten Lösungen lassen sich jedoch mit Abbildungen aus F identifizieren.

3.4 Polyederanalyse

49

3.4.2 Matrizenmengen als Summary-Information
Wie im vorigen Abschnitt bereits beschrieben, lässt sich der Effekt einer affinen
Zuweisung mittels einer Matrix ausdrücken. Der Effekt zweier aufeinander folgender
Kanten ist dann genau durch das Produkt der beiden Matrizen gegeben, die die
Effekte der einzelnen Kanten beschreiben. So lässt sich auch der Effekt entlang eines
Pfades durch eine Matrix ausdrücken. Die Idee ist nun, einen Knoten mit einer solchen
Matrix zu annotieren, um damit zu beschreiben, dass vom Startknoten bis zu diesem
Knoten ein Zustand genau durch diese Matrix verändert wird.
Nun können aber auch mehrere Pfade zu einem Knoten führen. Die Effekte dieser
Pfade entsprechen also mehreren Matrizen. Somit ist es nicht möglich, den Effekt
bis zu einem Knoten allein mit einer Matrix zu beschreiben. Stattdessen werden
wir zu jedem Knoten eine Menge solcher Matrizen bestimmen. Wir definieren das
Ungleichungssystem zur Berechnung der Summary-Informationen ähnlich wie im
Ungleichungssystem (3.1), allerdings über dem vollständigen Verband
(LM , ⊆) := (2Mat(Σ) , ⊆).
Anschließend erläutern wir, wie sich eine Matrizenmenge als universell-distributive
Abbildung L → L auffassen lässt.
Dazu betrachten wir die verallgemeinerten Transferfunktionen fTM ,id , fTM ,xj :=t und
fTM ,q() : LM N → LM mit
fTM ,id (A) := {In+1 },
fTM ,(u,xj :=t,v) (A) := {Mxj :=t } ◦ Au
fTM ,(u,q(),v) (A) := Arq ◦ Au
für A ∈ LM N . Das Ungleichungssystem zur Bestimmtung der Prozedureffekte als
Transferfunktion hat also folgende Gestalt:
TM [sp ] ⊇ {In+1 }
TM [v] ⊇ {Mxj :=t } ◦ TM [u] für (u, xj := t, v) ∈ Ep Basiskante
TM [v] ⊇ TM [rq ] ◦ TM [u] für e = (u, q(), v) ∈ E Aufrufkante.

(3.18)

Dabei ist TM [u] ∈ LM = 2Mat(Σ) für jedes u ∈ Np und p ∈ Proc.
Mit ◦ bezeichnen wir dabei die elementweise Matrizenmultiplikation: Für Matrizenmengen A, B ⊆ Mat(Σ) ist A ◦ B := {A · B | A ∈ A, B ∈ B} die kanonische
Fortsetzung der Matrizenmultiplikation auf Matrizenmengen.
Wir wollen nun Matrizenmengen als Transferfunktionen auffassen. Dazu definieren
wir eine Abbildung αMat : LM → F. Diese bildet eine Matrix auf diejenige Funktion

50

3 Klassische Ansätze zur interprozeduralen Analyse

ab, die einen Zustand auf das Produkt der Matrix mit diesem Zustand abbildet,
und setzen dies fort auf Mengen von Matrizen. Konkret definieren wir also für eine
Matrizenmenge A ⊆ Mat(Σ)
αMat (A) : L → L,
S 7→ {A · s | A ∈ A, s ∈ S}.
Die Abbildung αMat ist wohldefiniert: Seien dazu A ∈ LM und S ⊆ L. Dann ist
G
 G  
αMat A
S = A·s|A∈A∧s∈
S

= A · s | A ∈ A ∧ (∃S ∈ S : s ∈ S)
[
=
{A · s | A ∈ A ∧ s ∈ S} | S ∈ S
[
=
αMat (A)(S) | S ∈ S .
Also ist αMat (A) universell-distributiv. Dies zeigt die Wohldefiniertheit von αMat .
Insbesondere gilt f(u,xj :=t,v) ((Sν )ν∈N ) = αMat ({Mxj :=t })(Su ).

3.4.3 Relationen als Summary-Information
Ein alternativer Ansatz ist, den Effekt einer Kante als Relation aufzufassen. Dabei
stehen zwei Zustände x und y in Relation zueinander, wenn y aus x durch den Effekt
dieser Kante entsteht. Genauer ordnen wir nun einem jeden Knoten eine Relation
R ⊆ Rn × Rn zu, wobei ein Tupel (x, y) genau dann in R enthalten ist, wenn es
eine Kante zu diesem Knoten gibt, die x zu y transfomiert. Speziell für eine affine
Zuweisung xj := t ist die Relation Rxj :=t , die den Effekt dieser Zuweisung beschreibt,
gegeben durch


n

n

(x, y) ∈ R × R | ∀1 ≤ i ≤ n : ((i 6= j ⇒ yi = xi ) ∧ yj = a0 +

n
X

ak x k ) .

k=1

Als zugrundeliegenden vollständigen Verband betrachen wir ähnlich wie bei den
Matrizenmengen
n

(LR , ⊆) := (2R

× Rn

, ⊆).

Zum Berechnen des Effektes einer Prozedur stellen wir wieder ein Ungleichungssystem
auf: Konkret benutzen wir dazu die verallgemeinerten Transferfunktionen fTR ,id ,
fTR ,xj :=t und fTR ,q() : LR N → LR mit
fTR ,id (R) := {(x, x) ∈ Rn × Rn },
fTR ,(u,xj :=t,v) (R) := Rxj :=t ◦ Ru
fTR ,(u,q(),v) (R) := Rrq ◦ Ru

3.4 Polyederanalyse

51

für R ∈ LR N . Das zu lösende Ungleichungssystem hat also folgende Gestalt:
TR [sp ] w {(x, x) ∈ Rn × Rn }
TR [v] w Rxj :=t ◦ TR [u] für (u, s, v) ∈ Ep Basiskante
TR [v] w TR [rq ] ◦ TR [u] für e = (u, q(), v) ∈ E Aufrufkante.
Dabei ist TR [u] ∈ 2R

n

× Rn

(3.19)

für jedes u ∈ Np und p ∈ Proc.

Mit ◦ bezeichnen wir die Verknüpfung zweier Relationen: Fasst man eine Relation
als eine Zuordnung auf und sind (x, y) ∈ R1 , (y, z) ∈ R2 , so wird also x von R1 dem
Wert y zugeordnet und der wiederum von R2 dem Wert z. Die Verknüpfung R2 ◦ R1
ordnet also dem Wert x den Wert z zu. Genauer ist
R2 ◦ R1 := {(x, z) | ∃y ∈ Rn : (x, y) ∈ R1 ∧ (y, z) ∈ R2 }.
Offenbar bildet {(x, x) ∈ Rn × Rn } das neutrale Element dieser Verknüpfung.
Wiederum identifizieren wir mithilfe einer Abbildung αRel : LR → F eine Relation mit
einer Abbildung auf Zustandsmengen, indem wir eine Relation, wie oben beschrieben,
als eine Zuordnung auffassen. Konkret ist für R ⊆ Rn × Rn dann
αRel (R) : L → L,
S 7→ {(1, y) | ∃(1, x) ∈ S : (x, y) ∈ R}.
Dabei schreiben wir abkürzend (1, x) für (1, x1 , . . . , xn ) mit x = (x1 , . . . , xn ) ∈ R.
Auch die Abbildung αRel ist wohldefiniert: Seien dazu R ∈ LR und S ⊆ L. Dann
ist
G
 G  
αRel R
S = (1, y) | ∃x ∈ Rn : (x, y) ∈ R ∧ x ∈
S

= (1, y) | ∃x ∈ Rn : (x, y) ∈ R ∧ ∃S ∈ S : x ∈ S
[
=
{(1, y) | ∃x ∈ S : (x, y) ∈ R} | S ∈ S
[
=
αRel (R)(S) | S ∈ S
Also ist αRel (R) universell-distributiv. Dies zeigt die Wohldefiniertheit von αRel .
Um später die kleinsten Lösungen T M und T R vergleichen zu können, benötigen
wir einen Zusammenhang zwischen Matrizenmengen und Relationen, den wir später
einführen werden. Speziell für {Mxj :=t } und Rxj :=t , die ja beide den Effekt derselben
affinen Zuweisung beschreiben, können wir einen solchen aber sofort herstellen:
P Es ist
(1, y) = Mxj :=t · (1, x) äquivalent zu yi = xi für alle i 6= j und yj = a0 + ni=1 ai xi ,
was nach Definition genau (x, y) ∈ Rxj :=t bedeutet. Mit anderen Worten ist also
Rxj :=t = {(x, y) ∈ Rn × Rn | (1, y) = Mxj :=t · (1, x)}.
Dies liefert also einen Zusammenhang zwischen Mxj :=t und Rxj :=t . Desweiteren
erhalten wir sofort f(u,xj :=t,v) ((Sν )ν∈N ) = αRel (Rxj :=t )(Su ).

52

3 Klassische Ansätze zur interprozeduralen Analyse

3.4.4 Erreichbare Zustände
In den vorigen Abschnitten 3.4.2 und 3.4.3 haben wir Summary-Informationen nicht
direkt als Abbildungen L → L berechnet, sondern zunächst als Matrizenmengen
bzw. Relationen ausgedrückt. Außerdem haben wir Abbildungen αMat und αRel
definiert, mit denen diese Matrizenmengen und Relationen als Abbildungen L → L
aufgefasst werden können. Derartige Abbildungen benötigen wir, um die erreichbaren
Zustände in den Programmknoten mit einem Ungleichungssystem der Gestalt (3.2)
aus dem funktionalen Ansatz zu berechnen. Für den Aufruf einer Prozedur q wird
in diesem Ungleichungssystem die Abbildung T [rq ] benötigt. Diese haben wir hier
nicht direkt zur Verfügung, da wir das Ungleichungssystem (3.1), mit dem diese
Abbildungen ausgerechnet werden, durch die Ungleichungssysteme (3.18) und (3.19)
ersetzt haben. Wir können jedoch die Abbildung T [rq ] ausdrücken durch αMat (TM [rq ])
bzw. αRel (TR [rq ]). Die entsprechenden Ungleichungssysteme bezeichnen wir mit RM
und RR und die zugehörenden verallgemeinerten Transferfunktionen nennen wir
fRM ,· : LN → L und fRR ,· : LN → L. Sie sind definieren wir durch
fRM ,init (S) := Σ
fRM ,(u,xj :=t,v) (S) := fxj :=t (Su )
fRM ,(u,q(),v),ent (S) := Su
fRM ,(u,q(),v),ret (S) := αMat (TM [rq ])(Su )
und
fRR ,init (S) := Σ
fRR ,(u,xj :=t,v) (S) := fxj :=t (Su )
fRR ,(u,q(),v),ent (S) := Su
fRR ,(u,q(),v),ret (S) := αRel (TR [rq ])(Su ).
Bis auf die Abbildungen fRM ,(u,q(),v),ret und fRR ,(u,q(),v),ret stimmen die verwendeten
Abbildungen also überein.

3.4.5 Vergleich der beiden Summary-basierten Ansätze
Im Folgenden untersuchen wir, ob die Ansätze mit Matrizenmengen bzw. Relationen
zu jedem Programmpunkt stets dieselben erreichbaren Zustände berechnen oder ob
ein Ansatz eine präzisere Lösung liefert als der andere.
Zunächst definieren wir eine Abbildung zwischen Matrizenmengen und Relationen.
Dabei ordnen wir einer Matrizenmenge diejenigen Paare zu, bei denen die zweite
Komponente aus der ersten durch Anwenden einer Matrix dieser Menge entsteht.

3.4 Polyederanalyse

53

Da die Matrizenmengen auf {1} × Rn operieren, die Relationen dagegen aus Tupeln
von Elementen aus Rn bestehen, brauchen wir zusätzlich noch eine Inklusions- und
Projektionsabbildung, um diese beide Räumen durch eine Bijektion miteinander in
Verbindung zu setzen:
ι : Rn → {1} × Rn ,
(x1 , . . . , xn ) 7→ (1, x1 , . . . , xn )

π : {1} × Rn → Rn ,
(1, x1 , . . . , xn ) 7→ (x1 , . . . , xn ).

Wir ordnen nun einer Matrix eine Relation zu mithilfe der Abbildung
n

Φ̃ : Mat(Σ) → 2R

× Rn

,

A 7→ Φ̃A := {(x, π(A · ι(x))) | x ∈ Rn }
und setzen diese kanonisch auf Matrizenmengen fort durch
n

n

Φ : 2Mat(Σ) → 2R × R ,
[

A 7→
Φ̃A | A ∈ A = (x, π(A · ι(x))) | x ∈ Rn ∧A ∈ A .
Lemma 3.9. Seien X1 , X2 ∈ Mat(Σ) and X ⊆ 2Mat(Σ) . Dann gilt:
a) ΦIn+1 = {(x, x) | x ∈ Rn },
b) ΦMxj :=t = Rxj :=t ,
c) ΦX2 ◦X1 = ΦX2 ◦ ΦX1 ,
S
d) ΦS X = {ΦX | X ∈ X }.
Hierbei bezeichnen wir mit ◦, wie in den vorigen Abschnitten definiert, die Komposition von Matrizenmengen bzw. von Relationen.
Beweis. Die Aussagen a) und b) resultieren direkt aus der Tatsache, dass Φ{A} = Φ̃A
für jede Matrix A ∈ Mat(Σ) gilt, sowie den Identitäten
π(In+1 · ι(x)) = x
und
π(Mxj :=t · ι(x)) = (x1 , . . . , xj−1 , a0 +

n
X
i=1

ai xi , xj+1 , . . . , xn ).

54

3 Klassische Ansätze zur interprozeduralen Analyse

Seien nun A ∈ X1 und B ∈ X2 . Dann ist
Φ̃B ◦ Φ̃A = {(x, z) | ∃y : (x, y) ∈ Φ̃A ∧ (y, z) ∈ Φ̃B }
= {(x, z) | ∃y : y = π(A · ι(x)) ∧ z = π(B · ι(y))}
= {(x, z) | z = π(B · ι(π(A · ι(x))))}
= {(x, z) | z = π(B · A · ι(x))}
= Φ̃BA .
Mit dieser Identität folgt nun c) aus
ΦX2 ◦X1 = Φ{BA|A∈X1 ∧B∈X2 }
[
=
Φ̃BA | A ∈ X1 ∧ B ∈ X2
[
=
Φ̃B ◦ Φ̃A | A ∈ X1 ∧ B ∈ X2
[
[
=
Φ̃B | B ∈ X2 ◦
Φ̃A | A ∈ X1
= ΦX2 ◦ ΦX1 .
Ähnlich erhalten wir für X ⊆ M
ΦS X = ΦS{X|X∈X }
[
[
Φ̃A | A ∈
X|X∈X
=
[[
Φ̃A | A ∈ X | X ∈ X
=
[
Φ̃X | X ∈ X ,
=
was d) beweist.
Wir wollen nun die kleinsten Lösungen der Ungleichungssysteme TM und TR zueinander in Verbindung setzen. Dabei ist TM [u] ∈ 2Mat(Σ) für jeden Knoten u ∈ N , also
TM ∈ (2Mat(Σ) )N . Hierbei identifizieren wir einen Vektor A mit der Abbildung
N → 2Mat(Σ) ,
u 7→ Au .
Entsprechend ist TR ∈ (2R

n

× Rn N

n

R ⊆ (2Mat(Σ) )N × (2R

) . Wir definieren also eine Relation

× Rn N

) ,

um die beiden Lösungen miteinander zu vergleichen. Genauer sei
(A, B) ∈ R :⇐⇒ ∀u ∈ N : B(u) = ΦA(u) .

3.4 Polyederanalyse

55

Satz 3.10. Es gilt (TM , TR ) ∈ R.
Beweis. Seien FM bzw. FR wiederum diejenigen Abbildungen, die die Ungleichungssysteme TM bzw. TR beschreiben. Damit ist TM = lfp(FM ) und entsprechend
TR = lfp(FR ). Also reicht es, die Bedingungen von Satz 2.18 für eben diese Abbildunn
n
gen FM und FR nachzurechnen. Offenbar sind ((2Mat(Σ) )N , ⊆N ) und ((2R × R )N , ⊆N )
vollständige Verbände und die F M und F R monoton, da sie aus monotonen Funktionen
entstehen.
n

Seien A ∈ (2Mat(Σ) )N , B ∈ (2R
muss

× Rn N

)

mit (A, B) ∈ R. Um Bedingung a) zu zeigen,

(FM (A), FR (B)) ∈ R
gezeigt werden. Konkret müssen wir also
FR (B)(u) = ΦFM (A)(u)
für jedes u ∈ N nachweisen. Nach Teil d) von Lemma 3.9 genügt es, dies für alle
Funktionen der ursprünglichen Ungleichungssysteme zu zeigen.
Für die Initialwerte folgt
(In+1 , {(x, x) ∈ Rn × Rn }) ∈ R
direkt aus Teil a) von Lemma 3.9. Seien weiter u ∈ N und TR [u] = ΦTM [u] . Mit den
Aussagen c) und b) von Lemma 3.9 folgt nun
Φ{Mxj :=t }◦TM [u] = Φ{Mxj :=t } ◦ ΦTM [u] = Rxj :=t ◦ TR [u],
was ({Mxj :=t }, Rxj :=t ) ∈ R liefert.
Sei nun u ∈ N , p ∈ Proc, TR [u] = ΦTM [u] and TR [rp ] = ΦTM [rp ] . Wiederum mit den
Teilen c) and b) von Lemma 3.9 erhalten wir
ΦTM [rp ]◦TM [u] = ΦTM [rp ] ◦ ΦTM [u] = TR [rp ] ◦ TR [u].
Damit ist auch (TM [rp ], TR [rp ]) ∈ R und Bedingung a) von Satz 2.18 ist gezeigt.
Seien also X ⊆ R und u ∈ N . Für jedes A ∈ X1 (u) gibt es also A ∈ X1 mit A = A(u)
und ein B ∈ X2 mit (A, B) ∈ R und damit ΦA = B für B := B(u). Dann ist
{ΦA | A ∈ X1 (u)} ⊆ {B | B ∈ X2 (u)}.
Die andere Inklusion zeigt man analog. Daraus erhalten wir
G
G
G
ΦF X1 (u) =
ΦA | A ∈ X1 (u) =
B | B ∈ X2 (u) =
X2 (u).
Auch Bedingung b) von Satz 2.18 ist gezeigt. Es folgt die Behauptung.

56

3 Klassische Ansätze zur interprozeduralen Analyse

Satz 3.11. Für jedes u ∈ N gilt RM [u] = RR [u].

Beweis. Die Ungleichungssysteme unterscheiden sich nur durch die Definitionen der
Abbildung fRM ,(u,q(),v),ret und fRR ,(u,q(),v),ret für diejenigen Ungleichungen, die die
Rückkehr aus einer Prozedur q ∈ Proc beschreiben. es ist
fRM ,(u,q(),v),ret = αMat (TM [rq ]) ◦ pru
und
fRR ,(u,q(),v),ret = αRel (TR [rq ]) ◦ pru
für die Projektion pru : LN → L auf die Komponente u. Darum genügt es,
αMat (TM [rq ]) = αRel (TR [rq ])
zu zeigen. Sei dazu S ∈ L. Zunächst beobachten wir
αMat (TR [rq ])(S) = {(1, ỹ) | ∃(1, x̃) ∈ S : (x̃, ỹ) ∈ TR [rq ]}
= {y | ∃x ∈ S : (π(x), π(y)) ∈ TR [rq ]}.
Nach dem vorigen Lemma wissen wir bereits TR [rq ] = ΦTM [rq ] . Somit gilt weiter
{y | ∃x ∈ S : (π(x), π(y)) ∈ TR [rq ]}
= {y | ∃x ∈ S ∃A ∈ TM [rq ] : π(y) = π(A · ι(π(x)))}
= {y | ∃x ∈ S ∃A ∈ TM [rq ] : y = A · x}
= {A · x | x ∈ S ∧ A ∈ TM [rq ]}
= αMat (TM [rq ])(S)
Es folgt die Behauptung.

Die beiden in den letzten Abschnitten vorgestellen Analysen mithilfe von Matrizenmengen bzw. Relationen als Summary-Informationen liefern also das gleiche Ergebnis.
Später werden wir überprüfen, ob dies für den nächsten Schritt der Polyederanalyse,
in dem zusätzlich konvexe Hüllen gebildet werden, immer noch gilt. Die Bildung
konvexer Hüllen ist eine abstrakte Interpretation. Mit solchen werden wir uns in
Kapitel 4 beschäftigen.

3.5 Terminierung des Workset-Algorithmus

57

3.5 Terminierung des Workset-Algorithmus
In Abschnitt 3.1 und Abschnitt 3.2 haben wir zwei Ansätze zur interprozeduralen
Datenflussanalyse vorgestellt. In beiden Ansätzen werden Ungleichungssysteme aufgestellt, deren kleinste Lösungen genau die gewünschten Informationen über das
Programm liefsern. In Abschnitt 2.4 haben als Hilfsmittel zum Lösen von Ungleichungssystemen den Workset-Algorithmus vorgestellt. Falls er terminiert, so liefert
er eine Lösung dieses Ungleichungssystems. Außerdem hatten wir gesehen, dass ein
solcher Algorithmus tatsächlich terminiert, falls der zugrundeliegende Verband und
die Menge der Ungleichungen endlich sind. Ist der Verband dagegen nicht endlich, so
kann Terminierung nicht garantiert werden, wie das folgende Beispiel zeigt.
Beispiel 3.12. Wir betrachten das Ungleichungssystem U, das gegeben ist durch
A[1] w init
A[2] w fx:=0 (A[1])
A[2] w fx:=x+1 (A[2])
A[3] w fx:=0 (A[2])
mit init := [−∞, +∞] sowie
fx:=0 (I) = {[0, 0]}
und
(
∅
fx:=x+1 (I) =
[l + 1, u + 1]

falls I = ∅
falls I = [l, u]

für I ∈ LInt .
Im Algorithmus bekommt nun A[2] aufgrund der zweiten Ungleichung den Wert [0, 0].
Durch die dritte Ungleichung wird dieser zunächst in einem ersten“ Schritt ersetzt
”
durch
[0, 0] ∪ [1, 1] = [0, 1].
Anschließend ist die dritte Ungleichung wiederum nicht erfüllt. Im zweiten“ Schritt
”
wird der Wert von A[2] also ersetzt durch
[0, 1] ∪ [1, 2] = [0, 2].
Die dritte Ungleichung ist weiterhin nicht erfüllt. Dies setzt sich fort, so dass A[2]
nach n Schritten den Wert [0, n] hat. Da die dritte Ungleichung auch für diesen Wert
nicht erfüllt ist, kann der Algorithmus in endlicher Zeit nicht terminieren.


58

3 Klassische Ansätze zur interprozeduralen Analyse

Wir haben in diesem Kapitel zwei Ansätze zur Analyse interprozeduraler Programme
untersucht. Der Call-String-Ansatz simulitert eine interprozedurale Analyse mithilfe
von Call-Strings, während der funktionale Ansatz zunächst die Effekte der Prozeduren
bestimmt und diese dann wie die Transferfunktionen für Basiskanten benutzt. Weiter
haben wir gezeigt, dass die kleinsten Lösungen beider Ansätze übereinstimmen, sofern
die verwendeten Abbildungen gewissen Distributivitätseigenschaften genügen.
Zuletzt haben wir gesehen, dass eine Berechnung der Lösung von Ungleichungssystemen durch den Workset-Algorithmus nicht unbedingt terminieren muss. Deshalb
müssen in der Praxis Strategien benutzt werden, mit deren Hilfe neue Analysen
gefunden, zu denen Lösungen in endlicher Zeit berechnet werden können. Zwei solche
Mittel sind die abstrakte Interpretation und die Verwendung eines Widening-Operators.
Diese Konzepte werden wir in den beiden kommenden Kapiteln vorstellen und dort
wiederum die Ergebnisse des funktionalen und des Call-String-Ansatzes vergleichen.

4 Abstrakte Interpretation
Abstrakte Interpretation ist ein von Cousot und Cousot [CC77] entwickeltes Mittel, um den Berechnungsaufwand in praktischen Analysen zu reduzieren. Die Idee
dabei ist, anstelle der gesuchten eine abstrakte“ Information zu berechnen. Dazu
”
abstrahiert man die verallgemeinerten Transferfunktionen des Ungleichungssystems
zu Abbildungen auf dem abstrakten Verband. Dadurch erhält man ein Ungleichungssystem, dessen kleinste Lösung unter geeigneten Voraussetzungen genau die abstrakte
Version der gesuchten Information ist. In dem Fall nennen wir das abstrahierte
Ungleichungssystem präzise. Die Lösung des abstrahierten Ungleichungssystems kann
nun im Gegensatz zu der des konkreten Ungleichungssystems endlich darstellbar und
in endlicher Zeit berechenbar sein. Darum ist abstrakte Interpretation ein starkes
Werkzeug bei der Konstruktion effizienter Analysen.
Abstrakte Interpretation kann aber auch ein Mittel zur Konstruktion neuer korrekter
oder präziser Analysen sein. Dazu wird eine gesuchte Information aus einer anderen
berechnet, zu deren Berechnung wiederum eine korrekte oder präzise Anlayse bekannt
ist. Ist eine solche Analyse gegeben und abstrahiert man diese korrekt und präzise,
so gewinnt man daraus wieder eine korrekte bzw. präzise Analyse. Die Bedingungen,
die an die abstrakte Interpretation gestellt werden, damit diese korrekt oder präzise
ist, können also dazu verwendet werden, aus einer gegebenen Analyse eine neue zu
konstruieren.
In Kapitel 3 haben wir mit dem funktionalen und dem Call-String-Ansatz zwei
Ansätze zur Analyse interprozeduraler Programme betrachtet, die unter geeigneten
Voraussetzungen dieselbe kleinste Lösung liefern. In diesem Kapitel wollen wir diese
beiden Ansätze zusätzlich abstrakt interpretieren, Eigenschaften der so abstrahierten
Ungleichungssysteme untersuchen und überprüfen, ob beide Ansätze wieder die
gleichen Lösungen liefern, wenn zusätzlich abstrakte Interpretation benutzt wird.
Dazu führen wir zunächst Abstraktionen und abstrahierte Ungleichungssysteme ein
und untersuchen letztere im Hinblick auf die sogenannte Korrektheit und Präzision
ihrer kleinsten Lösungen. Die entsprechenden Begrifflichkeiten finden sich in [CC77]
oder auch in [NNH99]. Anschließend übertragen wir diese Vorgehensweise auf die in
Kapitel 3 vorgestellten Ansätze zur interprozeduralen Analyse. Zuletzt betrachten
wir wieder die Polyederanalyse, bei der wir mithilfe der Bildung konvexer Hüllen die
Ungleichungssysteme abstrahieren wollen.

60

4 Abstrakte Interpretation

4.1 Galois-Verbindungen
Um einen konkreten“ und einen abstrakten“ vollständigen Verband miteinander in
”
”
Verbindung zu setzen, benötigen wir nicht nur eine Abstraktion, die einem konkreten
Element ein abstraktes zuordnet, sondern auch eine Konkretisierung, die zu jedem
abstrakten Element ein konkretes liefert. Solche Abbildungen erhält man durch eine
Galois-Verbindung.
Definition 4.1. Seien (L, v) und (L] , v] ) Halbordnungen und α : L → L] sowie
γ : L] → L Abbildungen. Dann heißt (α, γ) Galois-Verbindung, falls für alle x ∈ L
und y ∈ L] gilt:
α(x) v] y ⇐⇒ x v γ(y).
Dabei nennt man α Abstraktion und γ Konkretisierung.
Wir erinnern an folgendes Beispiel in [WM92].
Beispiel 4.2. Zu zeigen ist die Aussage, dass für jede ganze Zahl z ∈ Z der Ausdruck
z 2 (z + 1)2 durch 4 teilbar ist. Dazu abstrahieren wir die ganzen Zahlen, indem wir
eine Zahl mit dem Rest identifizieren, der bei Division dieser Zahl durch 4 übrig
bleibt. Wir haben also
L = Z und L] = {0̄, 1̄, 2̄, 3̄}
und definieren α = L → L] durch α(z) := r̄ für dasjenige r ∈ {0, 1, 2, 3} mit
z ≡ x mod 4.
Weiter definieren wir Abstraktionen +̄ : L] × L] → L] und ¯· : L] × L] → L] der
Addition + : L × L → L und der Multiplikation · : L × L → L durch
z¯1 +̄z¯2 := z¯1 + z¯2 und z¯1¯·z¯2 := z¯1 · z¯2
Man sieht nun leicht die Gültigkeit von
z1 + z2 = z¯1 +̄z¯2 und z1 · z2 = z¯1¯·z¯2 .
Es kann nun der Ausdruck
z 2 (z + 1)2
abstrakt interpretiert werden. Berechnet man diesen abstrakte Ausdruck für jeden
möglichen Wert z ∈ {0, 1, 2, 3}, so erhält man in jedem der vier Fälle den Wert 0̄.
Die Aussage
z 2 (z + 1)2 = 0̄
ist nun äquivalent zu der gewünschten Aussage, dass z 2 (z + 1)2 durch 4 teilbar ist. 

4.1 Galois-Verbindungen

61

In diesem Beispiel wurde also, anstatt eine Aussage für unendliche viele Elemente
z ∈ Z = L zu zeigen, eine äquivalente Aussage in einem endlichen Raum L] bewiesen.
Auf ähnliche Weise kann es also möglich sein, ein Ungleichungssystem über einem
unendlichen Verband (L, v) so zu abstrahieren, dass ein entsprechendes Ungleichungssystem über einem Verband (L] , v] ) definiert ist, der endlich oder unendlich mit
endlicher Kettenhöhe ist.
Das nächste Lemma zeigt, dass sich Abstraktionen und Konkretisierungen bereits
eindeutig gegenseitig festlegen.
Lemma 4.3. Sei (α, γ) eine Galois-Verbindung zwischen den vollständigen Verbänden
(L v) und (L] , v] ). Dann bestimmen α und γ sich eindeutig durch
α(x) =

l] 

γ(y) =

G

y ∈ L] | x v γ(y)

x ∈ L | α(x) v y .

Beweis. Für beliebiges x ∈ L gilt
α(x) =

l] 

y ∈ L] | α(x) v] y =

l] 

y ∈ L] | x v γ(y) .

Dabei resultiert die letzte Gleichheit aus der Äquivalenz von α(x) v] y und γ(y) v x.
Diese Darstellung definiert α bereits eindeutig. Die eindeutige Darstellung von γ
zeigt man entsprechend.
Die Konkretisierung zu einer Abstraktion ist also eindeutig. Mit dieser eindeutigen
Darstellung kann man nun leicht zeigen, dass Abstraktionen und Konkretisierungen
monoton sind.
Korollar 4.4. Sei (α, γ) eine Galois-Verbindung zwischen den vollständigen Verbänden (L v) und (L] , v] ). Dann sind α und γ monoton.
Beweis. Seien zunächst x1 , x2 ∈ L mit x1 v x2 . Dann ist offenbar


y ∈ L] | x2 v γ(y) ⊆ y ∈ L] | x1 v γ(y) .
Damit gilt nach Lemma 4.3
α(x2 ) =

l] 
l] 
y ∈ L] | x1 v γ(y) = α(x1 ).
y ∈ L] | x2 v γ(y) w]

Also ist α monoton. Die Monotonie von γ zeigt man genauso.

62

4 Abstrakte Interpretation

Wir können nun zeigen, dass eine Abbildung zwischen zwei vollständigen Verbänden
genau dann eine Abstraktion in einer Galois-Verbindung ist, wenn sie universelldistributiv ist.
Lemma 4.5. Sind (L, v) und (L] , v] ) zwei vollständige Verbände und α : L → L]
eine Abbildung, so ist α genau dann universell-distributiv, wenn α eine Abstraktion
ist.
Beweis. Sei α eine Abstraktion und γ die zugehörige Konkretisierung. Sei X ⊆ L
beliebig. Offenbar gilt für jedes x ∈ X bereits
G] 
G]
α(x) v]
α(x) | x ∈ X =
α(X)
und nach Definition einer Galois-Verbindung damit auch
G]

xvγ
α(X) .
Daraus folgt direkt
G
G]

Xvγ
α(X) ,
was wiederum äquivalent ist zu
G 
G]
α
X v]
α(X).
Nach Korollar 4.4 ist α monoton und dies impliziert die umgekehrte Ungleichung
und somit Gleichheit. Also ist α universell-distributiv.
Sei nun α universell-distributiv. Definiere wie in Lemma 4.3
γ : L] → L,
G
y 7→
Ly
für
Ly := {x ∈ L | α(x) v] y}.
F
Da (L, v) ein vollständiger Verband ist, existiert Ly und γ ist wohldefiniert. Ist
y v] y 0 , so ist offenbar Ly ⊆ Ly0 und damit γ(y) v γ(y 0 ). Also ist γ monoton. Es
bleibt zu zeigen, dass (α, γ) tatsächlich eine Galois-Verbindung ist.
Seien dazu x ∈ L und y ∈ L] . Gelte zunächst α(x) v] y. Dann ist x ∈ Ly und damit
G
xv
Ly = γ(y).

4.1 Galois-Verbindungen

63

F
Sei nun umgekehrt x v γ(y) = Ly . Mit der Monotonie und universellen Distributivität von α folgt
G  G] 
α(x) v] α
Ly =
α(x) | x ∈ Ly v] y,
wobei letzteres daraus resultiert, dass α(x) v] y für jedes x ∈ Ly . Damit folgt die
Behauptung.
Das folgende Lemma liefert eine äquivalente Beschreibung des Begriffs Galois-Verbindung, die wir im Folgenden benötigen.
Lemma 4.6. Seien (L v) und (L] , v] ) vollständige Verbände und α : L → L] und
γ : L] → L. Dann sind die folgenden Aussagen äquivalent:
a) Es ist (α, γ) ist eine Galois-Verbindung.
b) Die Abbildungen α und γ sind monoton und erfüllen α ◦ γ v idL] und γ ◦ α w idL .
Beweis. Sei zunächst (α, γ) eine Galois-Verbindung. Die Monotonie von α und γ
haben wir bereits in Korollar 4.4 gezeigt. Für beliebiges x ∈ L ist trivialerweise
α(x) v] α(x). Nach Definition der Galois-Verbindung folgt daraus x v γ ◦ α(x).
Ebenso zeigt man α ◦ γ v idL] .
Seien nun α und γ monoton und gelte α ◦ γ v idL] und γ ◦ α w idL . Sei x ∈ L und
y ∈ L] mit α(x) v] y. Nach Voraussetzung und mit der Monotonie von γ ist dann
x v γ ◦ α(x) v γ(y). Analog zeigt man, dass x v γ(y) schon α(x) v] y impliziert.
Also ist (α, γ) eine Galois-Verbindung.
Die Verknüpfungen von Abstraktion und Konkretisierung liefern also noch nicht die
Identität, approximieren diese aber. Verknüpft man die Verknüpfungen wiederum mit
der Abstraktion oder der Konkretisierung, so erhält man dabei aber die Abstraktion
bzw. die Konkretisierung. Dies zeigt das folgende Lemma.
Lemma 4.7. Sei (α, γ) eine Galois-Verbindung zwischen den vollständigen Verbänden
(L, v) und (L] , v] ). Dann gilt
α ◦ γ ◦ α = α und γ ◦ α ◦ γ = γ.
Beweis. Nach Lemma 4.6 ist α◦γ v idL] und γ◦α w idL . Damit und mit der Monotonie
von α folgt für x ∈ L
α(x) v] α ◦ (γ ◦ α)(x) = (α ◦ γ) ◦ α(x) v] α(x).
Somit gilt überall bereits Gleichheit und es folgt die erste Aussage. Die andere Aussage
zeigt man völlig analog.

64

4 Abstrakte Interpretation

Beispiel 4.8. In Kapitel 3 haben wir den funktionalen Ansatz zur interprozeduralen Datenflussanalyse untersucht, welcher Transferfunktionen als SummaryInformationen berechnet. In der Polyederanalyse in Abschnitt 3.4 haben wir diese
Summary-Informationen jedoch nicht direkt als Transferfunktionen berechnet, sondern zunächst Matrizenmengen bzw. Relationen berechnet. Diese haben wir mithilfe
von Abbildungen αMat und αRel als Transferfunktionen aufgefasst. Diese Abbildungen
sind Abstraktionen. Um dies zu sehen, reicht es nach Lemma 4.5 nachzuweisen, dass
die Abbildungen universell-distributiv sind.
Seien dazu zunächst M ⊆ LM eine Menge von Matrizenmengen und S ∈ L eine
Menge von Zuständen. Dann ist
[  
αMat
M S
[

= A·s|s∈S∧A∈
M


= A · s | s ∈ S ∧ (∃A ∈ M : A ∈ A }
[
=
{A · s | s ∈ S ∧ A ∈ A} | A ∈ M
[

=
αMat (A | A ∈ M} S .
Entsprechend ist für R ⊆ LR und S ∈ L
[  
αRel
R S
[

= (1, y) | ∃x ∈ Rn : ((1, x) ∈ S ∧ (x, y) ∈
R)
[

= (1, y) | ∃x ∈ Rn ∃R ∈
R : ((1, x) ∈ S ∧ (x, y) ∈ R)
[

= {(1, y) | ∃x ∈ Rn : ((1, x) ∈ S ∧ (x, y) ∈ R)} | R ∈
R
[

=
αRel (R | R ∈ R} S .
Also sind αMat und αRel Abstraktionen.



In Abschnitt 4.4 werden wir sogenannte konvexe Hüllen“ bilden. Dazu definieren wir
”
hier Hüllenoperatoren und zeigen, dass Hüllenoperatoren und Galois-Verbindungen
sich gegenseitig induzieren.
Definition 4.9 (Hüllenoperator). Sei (L, v) eine Halbordnung. Eine Abbildung
h : L → L heißt Hüllenoperator , falls gilt:
a) Die Abbildung h ist extensiv, d.h. für alle x ∈ L ist x v h(x).
b) Die Abbildung h ist monoton, d.h. für alle x, y ∈ L ist (x v y ⇒ h(x) v h(y)).
c) Die Abbildung h ist idempotent, d.h. für alle x v L ist h(h(x)) = h(x).

4.2 Abstrakte Interpretation von Ungleichungssystemen

65

Lemma 4.10. Seien (L, v) und (L] , v] ) zwei Halbordnungen. Dann gilt:
a) Ist (α, γ) eine Galois-Verbindung zwischen (L, v) und (L] , v] ), so ist die Abbildung h := γ ◦ α : L → L ein Hüllenoperator.
b) Ist h : L → L ein Hüllenoperator, so ist (h, id) eine Galois-Verbindung zwischen
(L, v) und (h(L), v).
Beweis. Beide Aussagen lassen sich schnell nachrechnen:
a) Setze h := γ ◦ α. Da α und γ monoton sind, ist auch h monoton. Weiter gilt
h = γ ◦ α w idL . Also ist h auch extensiv. Damit folgt weiter
h ◦ h w h ◦ id = h.
Andererseits ist aber auch α ◦ γ v] idL] und damit
h ◦ h = γ ◦ (α ◦ γ) ◦ α v] γ ◦ idL] ◦α = h.
Zusammen folgt die Idempotenz von h. Somit ist h ein Hüllenoperator.
b) Seien x ∈ L sowie y ∈ h(L) beliebig. Wir zeigen nun die Äquivalenz
h(x) v y ⇐⇒ x v id(y).
Gelte zunächst h(x) v y. Da h extensiv ist, folgt sofort
x v h(x) v y.
Sei nun x v y. Da y ∈ h(L), existiert ein x0 ∈ L mit y = h(x0 ). Mit der
Monotonie und Idempotenz von h erhalten wir nun
h(x) v h(y) = h(h(x0 )) = h(x0 ) = y.
Also ist (α, id) eine Galois-Verbindung.

4.2 Abstrakte Interpretation von
Ungleichungssystemen
In diesem Abschnitt betrachten wir abstrakte Interpretationen von Ungleichungssystemen. Wie zu Beginn des Kapitels erwähnt, soll dabei zu einem Ungleichungssystem
U über L und einer Abstraktion α : L → L] ein Ungleichungssystem U ] über L]
aufgestellt werden. Dessen kleinste Lösung soll dem abstrahierten Wert der kleinsten
Lösung von U entsprechen oder diesen zumindest approximieren.

66

4 Abstrakte Interpretation

Formal erhält man ein solches abstrahiertes Ungleichungssystem durch eine abstrakte
Interpretation, die den verallgemeinerten Transferfunktionen Abbildungen auf dem abstrakten Raum L] zuordnet. Dazu benötigen wir für eine Indexmenge I zunächst einen
Lift einer Abstraktion α : L → L] auf den Raum LI → L, der die verallgemeinerten
Transferfunktionen enthält.
Lemma 4.11. Sei (α, γ) eine Galois-Verbindung zwischen den vollständigen Verbänden (L, v) und (L] , v] ). Definiere α̂ : LI → (L] )I und γ̂ : (L] )I → LI durch
α̂((xi )i∈I ) := (α(xi ))i∈I
γ̂((yi )i∈I ) := (γ(yi ))i∈I .
Dann ist (α̂, γ̂) eine Galois-Verbindung zwischen (LI , vI ) und ((L] )I , (v] )I ).
Beweis. Seien x ∈ LI und y ∈ (L] )I . Dann gilt
α̂(x)(v] )I y ⇐⇒ ∀i ∈ I : α(xi ) v] yi
⇐⇒ ∀i ∈ I : xi v γ(yi )
⇐⇒ x vI γ̂(y).
Es folgt die Behauptung.
Wir können nun definieren, was wir unter einer abstrakten Interpretation eines
Ungleichungssystems verstehen:
Definition 4.12. Seien I eine Indexmenge und (L, v) und (L] , v] ) vollständige
Verbände. Eine abstrakte Interpretation bezüglich einer Abstraktion α : L → L] ist
eine Zuordnung (LI → L) → ((L] )I → L] ), die jeder konkreten Abbildung f : LI → L
eine abstrakte Abbildung f ] : (L] )I → L] zuordnet. Falls
α ◦ f (x) v f ] ◦ α̂(x)
für alle Abbildungen f und alle x ∈ LN gilt, nennen wir die abstrakte Interpretation
α-korrekt. Falls sogar
α ◦ f = f ] ◦ α̂
für alle Abbildungen f gilt, nennen wir die abstrakte Interpretation α-präzise.
Das abstrahierte Ungleichungssystem zu einem Ungleichungssystem U bezüglich einer
solchen abstrakten Interpretation ist definiert durch
U ] := {(xj w] f ] (x)) | (xj w f (x)) ∈ U}.

4.2 Abstrakte Interpretation von Ungleichungssystemen

67

Lemma 4.13. Die folgenden Aussagen sind äquivalent:
a) Für alle x ∈ LI gilt α ◦ f (x) v] f ] ◦ α̂(x).
b) Für alle x ∈ LI gilt f (x) v γ ◦ f ] ◦ α̂(x).
c) Für alle y ∈ (L] )I gilt f ◦ γ̂(y) v γ ◦ f ] (y).
d) Für alle y ∈ (L] )I gilt α ◦ f ◦ γ̂(y) v] f ] (x).
Beweis. Die Äquivalenz der Aussagen a) und b) bzw. c) und d) folgt jeweils sofort aus
der Definition einer Galois-Verbindung. Es genügt also zu zeigen, dass die Aussagen
b) und c) äquivalent sind.
Gelte zunächst b) und sei y ∈ (L] )I beliebig. Dann ist γ̂(y) ∈ LI und nach b) gilt
f ◦ γ̂(y) v γ ◦ f ] ◦ α̂ ◦ γ̂(y).
Da (α̂, γ̂) eine Galois-Verbindung ist, gilt nach Lemma 4.6 α̂ ◦ γ̂(y) vI y. Damit folgt
das Gewünschte.
Die andere Richtung zeigt man analog. Es folgt die Behauptung.
Seien im Folgenden eine Galois-Verbindung (α, γ) zwischen vollständigen Verbänden
(L, v) und (L] , v] ), eine Indexmenge I, ein Ungleichungssystem U, eine abstrakte
Interpretation und das zugehörige abstrahierte Ungleichungssystem U ] fixiert. Wir
nennen dann auch U das konkrete und U ] das abstrahierte Ungleichungssystem. Mit F
und F ] bezeichnen wir diejenigen Abbildungen, deren Präfixpunkte mit den Lösungen
der Ungleichungssysteme übereinstimmen.
Wie eingangs beschrieben, soll mit der abstrakten Interpretation eines Ungleichungssystems nach Möglichkeit der abstrahierter Wert der kleinsten Lösung des Ungleichungssystems berechnet oder zumindest approximiert werden. Der berechnete Wert
lfp(F ] ) soll also mindestens soviel Information enthalten wie α̂(lfp(F )). Dass dieser
abstrahierte Wert tatsächlich immer approximiert wird, wenn die benutzte abstrakte
Interpretation α-korrekt ist, ist die Aussage des folgenden Satzes. Um den abstrahierten Wert tatsächlich zu erreichen, ist sogar α-Präzision vonnöten, wie wir anschließend
zeigen werden.
Satz 4.14. Sei die zugrundeliegende abstrakte Interpretation α-korrekt. Dann gilt
lfp(F ] ) wI α̂(lfp(F )).

68

4 Abstrakte Interpretation

Beweis. Wir benutzen Satz 2.18. Dabei betrachten wir die Relation
I

I

R := {(x, y) ∈ LI × L] | α̂(x)v] y}.
Wenn wir für die Abbildungen F und F ] die Voraussetzungen von Satz 2.18 zeigen
können, so folgt (lfp(F ), lfp(F ] )) ∈ R, was genau die gewünschte Aussage ist.
Sei nun (x, y) ∈ R. Um (F (x), F ] (y)) ∈ R zu zeigen, genügt es, α(Fi (x)) v] Fi] (y) für
alle i ∈ I nach zu weisen. Für i ∈ I ist wegen der universellen Distributivität von α
G

α(Fi (x)) = α
f (x) | f ∈ Fi
G] 
=
α ◦ f (x) | f ∈ Fi
G] 
v
f ] (α̂(x)) | f ∈ Fi
= Fi] (α̂(x))
v] Fi] (y),
I

da α̂(x)v] y nach Voraussetzung und F ] monoton ist. Damit ist Voraussetzung a)
aus Satz 2.18 gezeigt.
Sei
X ⊆ R, d.h. für alle x = (x1 , x2 ) ∈ XFund für alle iF∈ I ist α̂(x1i ) v] x2i . Um
F nun
F
( X 1 , X 2 ) ∈ R zu beweisen, zeigen wir α̂( X 1 ))i v] ( ] X 2 )i für alle i ∈ I:
α̂

G

X1


i

G


X1 i
G 
=α
Xi1
G]
=
α(Xi1 )
G] 
=
α(x1i ) | x ∈ X
=α

N

Für alle x ∈ X haben wir nun α̂(x1i )v] x2i . Damit ist
von {α̂(x1i ) | x ∈ X}. Wir erhalten
α̂

G

X1


i

v]

G] 

x2i | X ∈ X =

G]

X2

F]

{x2i | x ∈ X} obere Schranke


i

und auch Voraussetzung b) aus Satz 2.18 ist erfüllt. Es folgt die Behauptung.
Satz 4.15. Sei die zugrundeliegende abstrakte Interpretation α-präzise. Dann gilt
lfp(F ] ) = α̂(lfp(F )).

4.2 Abstrakte Interpretation von Ungleichungssystemen

69

Beweis. Nach Satz 4.14 wissen wir bereits, dass lfp(F ] ) wI α̂(lfp(F )) gilt. Um die
umgekehrte Ungleichung zu zeigen, genügt es nach zu weisen, dass α̂(lfp(F )) eine
Lösung des Ungleichungssystems U ] ist. Sei dazu xj w f (x) eine beliebige Ungleichung
von U. Da lfp(F ) eine Lösung dieses Ungleichungssystems ist, gilt lfp(F )j w f (lfp(F )).
Mit den Voraussetzungen an f und f ] und der Monotonie von α folgt nun
f ] (α̂(lfp(F ))) = α(f (lfp(F ))) v α((lfp(F ))j ) = (α̂(lfp(F )))j .
Also erfüllt α̂(lfp(F )) die Ungleichung xj w] f ] (x). Es folgt die Behauptung.
Wir sagen auch, dass U ] die kleinste Lösung von U präzise abstrakt berechnet.
Später werden wir das folgende Lemma benötigen, das eine weitere Eigenschaft von
solchen präzisen abstrakt interpretierten Abbildungen liefert.
Lemma 4.16. Seien f : LI → L und f ] : (L] )I → L] monoton mit f ] ◦ α̂ = α ◦ f .
Dann gilt
α ◦ f ◦ γ̂ ◦ α̂ = α ◦ f.
Beweis. Aus der Voraussetzung für f und f ] und Lemma 4.7 folgt unmittelbar
α ◦ f = f ] ◦ α̂ = f ] ◦ α̂ ◦ γ̂ ◦ α̂ = α ◦ f ◦ γ̂ ◦ α̂
und dies ist die Behauptung.
Beispiel 4.17. In Beispiel 4.8 haben wir gesehen, dass die Abbildungen αMat und αRel ,
Matrizenmengen oder Relationen als Transferfunktionen auffassen, Abstraktionen
sind. Definiert man nun ein Ungleichungssystem T der Transferfunktionen durch
das Ungleichungssystem (3.1) aus Abschnitt 3.1, so ist dies eine präzise abstrakte
Interpretation:
Seien dazu zunächst A1 , A2 ∈ LM und S ∈ L. Dann gilt
(αMat (A2 ) ◦ αMat (A1 ))(S)
= αMat (A2 )({A · s | s ∈ S ∧ A ∈ A1 })
= αMat ({B · A · s | s ∈ S ∧ A ∈ A1 ∧ B ∈ A2 })
= αMat ({C · s | s ∈ S ∧ C ∈ A2 ◦ A1 })
= αMat (A2 ◦ A1 )(S).
Entsprechend ist für R1 , R2 ∈ LR und S ∈ L
(αRel (R2 ) ◦ αRel (R1 ))(S)
= αRel (R2 )({(1, y) | ∃x ∈ Rn : ((1, x) ∈ S ∧ (x, y) ∈ R1 )})
= ({(1, z) | ∃x, y ∈ Rn : ((1, x) ∈ S ∧ (x, y) ∈ R1 ∧ (y, z) ∈ R2 )})
= ({(1, z) | ∃x ∈ Rn : ((1, x) ∈ S ∧ (x, z) ∈ R2 ◦ R1 )})
= αRel (R2 ◦ R1 )(S).

70

4 Abstrakte Interpretation

Mit diesen Identitäten können wir nun die gewünschte Aussage leicht aus Satz 4.15
folgern. Seien dafür zunächst A ∈ (LM )N und S ∈ L. Dann gilt
αMat ◦ fTM ,id (A)(S) = αMat ({En+1 })(S)
= {En+1 · s | s ∈ S}
=S
und andererseits auch
fT,id ◦ α̂Mat (A)(S) = id(S)
= S.
Also ist αM ◦ fTM ,id = fT,id ◦ α̂M . Weiter ist mit der Rechnung zu Beginn dieses
Beispiels
αMat ◦ fTM ,(u,xj :=t,v) (A) = αMat ({Mxj :=t } ◦ Au )
= αMat ({Mxj :=t }) ◦ αMat (Au )
= fxj :=t ◦ αMat (Au )
= fT,(u,xj :=t,v) ◦ α̂Mat (A)
und damit αMat ◦ fTM ,(u,xj :=t,v) = fT,(u,xj :=t,v) ◦ α̂Mat . Ebenso wie für Zuweisungen
folgt für Prozeduraufrufe αMat ◦ fTM ,(u,q(),v) = fT,(u,q(),v) ◦ α̂Mat aus
αMat ◦ fTM ,(u,q(),v) (A) = αMat (Arq ◦ Au )
= αMat (Arq ) ◦ αM (Au )
= fT,(u,q(),v) ◦ α̂Mat (A).
Nach Satz 4.15 ist also αMat (TM [u]) = T [u] für jedes u ∈ N . Anstatt das Ungleichungssystem T in (3.1) direkt zu lösen, kann also stattdessen das Ungleichungssystem TM
in (3.18) gelöst und dessen kleinste Lösung durch αM abstrahiert werden, wie es in
Abschnitt 3.4 auch geschehen ist.
Genauso zeigt man αRel (TR [u]) = T [u] für jedes u ∈ N .



Für jede Galois-Verbindung existiert eine α-korrekte abstrakte Interpretation: Die
folgende Definition zeigt, dass sich zu Abbildungen über L in kanonischer Weise Abbildungen auf L] angeben lassen. Der anschließende Satz zeigt, dass diese Zuordnung
eine α-korrekte abstrakte Interpretation liefert.
Definition 4.18. Wir nennen die Zuordnung (LI → L) → ((L] )I → L] ) , die einem
f : LI → L die Abbildung
f + := α ◦ f ◦ γ
zuordnet, α-kanonische abstrakte Interpretation.

4.2 Abstrakte Interpretation von Ungleichungssystemen

71

Das dadurch abstrahierte Ungleichungssystem U + nennen wir entsprechend das
α-kanonisch abstrahierte Ungleichungssystem.
Satz 4.19. Sei eine beliebige abstrakte Interpretation gegeben, die jedem f ein f ]
zuordnet.
a) Die abstrakte Interpretation ist genau dann α-korrekt, wenn f + (y) v] f ] (y)
für alle f und alle y ∈ (L] )I gilt. Insbesondere ist die kanonische abstrakte
Interpretation α-korrekt und liefert von allen abstrakten Interpretation das
kleinste Ergebnis.
b) Falls es eine α-präzise abstrakte Interpretation gibt, ist die kanonische abstrakte
Interpretation ebenfalls α-präzise.

Beweis. Die gewünschte Äquivalenzaussage folgt direkt aus Lemma 4.13. Sie impliziert
sofort, dass die kanonische abstrakte Interpretation korrekt ist. Nach Konstruktion
ist nun für alle y ∈ (L] )I
Fi] (y) =

G] 

f ] (y) | f ∈ Fi
G] 
w]
f + (y) | f ∈ Fi

= Fi+ (y).
Damit ist aber auch F + (v] )I F ] und so lfp(F + )(v] )I lfp(F ] ). Dies beweist den ersten
Teil.
Gebe es nun eine α-präzise abstrakte Interpretation. Nach Lemma 4.16 ist dann
f + ◦α = α◦f ◦γ ◦α = α◦f , also liefert auch f + eine α-präzise abstrakte Interpretation.
Es folgt die Behauptung.

Eine α-präzise abstrakte Interpretation zu einer gegeben Galois-Verbindung (α, γ) und
einem gegebenen Ungleichungssystem muss nicht existieren. Dies folgt aus vorigem
Satz 4.19, wenn man zeigen kann, dass eine α-kanonische abstrakte Interpretation nicht
die gewünschte präzise Lösung liefert. Ein Beispiel dafür ist die folgende abstrakte
Interpretation.
Beispiel 4.20. Wir betrachten die vollständigen Verbände, die durch die Hasse-Diagramme in Abbildung 4.1 gegeben sind.

72

4 Abstrakte Interpretation
L=

L] =

>

>]

c

e

b

d

a

⊥]

⊥
Abbildung 4.1: Hasse-Diagramm des zugrundeliegenden Verbandes in Beispiel 4.20.

Wir definieren nun eine Galois-Verbindung (α, γ) zwischen diesen vollständigen Verbänden durch
 ]

⊥

d
α(x) :=

e


 ]
>

falls
falls
falls
falls

x=⊥
x=a
x ∈ {b, c}
x=>

und



⊥

a
γ(y) :=

c



>

falls
falls
falls
falls

y
y
y
y

= ⊥]
=d
=e
= >] .

Man sieht leicht
α ◦ γ = idL] ,
γ ◦ α|{⊥,a,c,>} = id|{⊥,a,c,>}
und
γ ◦ α(b) = c A b.
Also ist γ ◦ α w idL und nach Lemma 4.6 ist (α, γ) eine Galois-Verbindung.
Wie betrachten nun ein Ungleichungssystem, das nur eine Variable x benutzt. Die
Abbildungen, die das Ungleichungssystem definieren, sind also auf (L → L) definiert.
Wir definieren eine Abbildung f : L → L durch


⊥ falls x = ⊥
f (x) := b falls x ∈ {a, b}


> falls x ∈ {c, >}.

4.3 Abstrakte Interpretation für interprozedurale Datenflussanalysen 73
Offenbar ist f universell-distributiv. Mit F bezeichnen wir das kleinste unter Komposition abschlossene System von Abbildungen, das idL und f enthält. Da die Komposition
universell-distributiver Abbildungen wieder universell-distributiv ist, ist (L, v, F) ein
universell-distributives monotones Framework. Die zugehörige optimale Abstraktion
f + = α ◦ f ◦ γ erfüllt

]

⊥
f + (y) = e

 ]
>

falls y = ⊥]
falls y = d
falls y ∈ {e, >] }.

Wir betrachten nun ein Ungleichungssystem U, das aus den folgenden beiden Ungleichungen besteht:
x w a und x w f (x).
Dieses Ungleichungssystem wird durch die Abbildung F : L → L beschrieben, die
durch F (x) := a t f (x) definiert ist. Das zugehörige abstrahierte Ungleichungssystem
ist definiert durch
y w] d und x w] f ] (x).
und wird beschrieben durch die Abbildung F ] : L] → L] mit F ] (y) = d t] f ] (y).
Man rechnet nun leicht für die kleinsten Fixpunkte
lfp(F ) = b und lfp(F ] ) = >]
aus. Es ist aber α(b) = e 6= >] . Also ist lfp(F ] ) 6= α(lfp(F )). Die abstrakte Interpretation ist somit zwar optimal, aber nicht präzise, womit gezeigt ist, dass eine α-präzise
abstrakte Interpretation nicht existieren muss.

Wenn die α-kanonische abstrakte Interpretation also nicht das gewünschte Ergebnis
liefert, so liefert sie doch nach Satz 4.19 zumindest von allen möglichen abstrakten
Interpretationen die präziseste Lösung.

4.3 Abstrakte Interpretation für interprozedurale
Datenflussanalysen
Im letzten Abschnitt haben wir abstrakte Interpretationen von Ungleichungssystemen
betrachtet, indem wir jede der verwendeten Abbildungen durch eine abstrahierte Abbildung ersetzt haben. Wir werden in diesem Abschnitt nun die Ungleichungssysteme

74

4 Abstrakte Interpretation

abstrahieren, die wir in Kapitel 3 zur Analyse interprozeduraler Programme eingeführt haben, indem wir in den verallgemeinerten Transferfunktionen jede benutzte
Transferfunktion durch eine abstrahierte Abbildung ersetzen.
Um die so abstrahierten Ungleichungssysteme untersuchen zu können, müssen wir
eine zugrundeliegende Galois-Verbindung auf die Räume fortsetzen, über denen die
Ungleichungssystem definiert sind: Zunächst benötigen wir eine Fortsetzung der
Abstraktion auf (L → L) → (L] → L] ), um auch diejenigen Abbildungen, mit denen
Transferfunktionen berechnet werden, abstrahieren zu können.
Definition 4.21. Sei (α, γ) eine Galois-Verbindung zwischen den vollständigen Verbänden (L, v) und (L] , v] ). Wir definieren nun
α : (L →mon L) → (L] →mon L] )
f 7→ α ◦ f ◦ γ

γ : (L] →mon L] ) → (L →mon L)
g 7→ γ ◦ g ◦ α

und

als Fortsetzungen von α und γ auf Abbildungen. Diese werden in Abbildung 4.2
illustriert.
LO

f

γ

L]

α(f )

/

L


α

/ L]

L
α



L]

α(g)

/

LO
γ

g

/

L]

Abbildung 4.2: Fortsetzung von Abstraktionen für Transferfunktionen.

Das folgende Lemma zeigt, dass wir dadurch tatsächlich wieder eine Abstraktion
erhalten.
Lemma 4.22. Die Fortsetzung (α, γ) ist eine Galois-Verbindung zwischen den vollständigen Verbänden ((L →mon L), v) und ((L] →mon L] ), v] ).
Beweis. Seien dazu f : L → L und g : L] → L] beliebige monotone Abbildungen.
Gelte zunächst α(f ) v] g. Zu zeigen ist f v γ(g). Sei dazu x ∈ L beliebig. Offenbar
gilt
α(x) v] α(x).
Da (α, γ) eine Galois-Verbindung ist, ist dies äquivalent zu
x v γ(α(x)).

4.3 Abstrakte Interpretation für interprozedurale Datenflussanalysen 75
Mit der Monotonie von f gilt damit weiter
f (x) v f (γ(α(x))).
Nach Voraussetzung gilt für jedes y ∈ L]
α ◦ f ◦ γ(y) = α(f )(y) v] g(y).
Da (α, γ) eine Galois-Verbindung ist, ist dies äquivalent zu
f (γ(y)) v γ(g(y)).
Für y := α(x) gilt also
f (x) v f (γ(α(x)))
v γ(g(α(x)))
= γ(y).
Dies impliziert f v γ(g). Die umgekehrte Richtung zeigt man analog. Also ist (α, γ)
eine Galois-Verbindung.
Sei im Folgenden G = (Np , Ep , sp , rp )p∈Proc ein Flussgraphsystem, das ein Programm
mit einer endlichen Menge Proc von Prozeduren beschreibt. Sei (L, v, F) das zugrundeliegende monotone Framework, (L] , v] ) ein vollständiger Verband und (α, γ)
eine Galois-Verbindung zwischen diesen vollständigen Verbänden. Sei außerdem eine
abstrakte Interpretation F → (L] → L] ) fest ausgewählt, die einer Abbildung f eine
Abbildung f ] zuordnet.
Wir definieren nun eine abstrakte Interpretation eines Ungleichungssystems zur
Analyse des Programms, indem wir in den verallgemeinerten Transferfunktionen
fT,· , fR,· und fA,· die Abbildungen fb , die für die Basiskanten benutzt werden, ab]
]
strakt interpretieren. Die dadurch entstehenden Abbildungen nennen wir fT,·
, fR,·
]
bzw. fA,·
.
]
Die Abbildungen fT,·
: (L] → L] )N → (L] → L] ) sind gegeben durch
]
fT,id
(h) := idL] ,
]
fT,(u,b,v)
(h) := fb] ◦ hu ,
]
fT,(u,q(),v)
(h) := hrq ◦ hu

für h = (hν )ν∈N ∈ (L] → L] )N , Basiskanten (u, b, v) und Aufrufkanten (u, q(), v).

76

4 Abstrakte Interpretation

]
Die Abbildungen fR,·
: (L] )N → L] sind definiert durch
]
fR,init
(y) := init] ,
]
fR,(u,b,v)
(y) := fb] (yu ),
]
fR,(u,q(),v),ent
(y) := yu ,
]
fR,(u,q(),v),ret
(y) := T ] [rq ](yu )

für y = (yν )ν∈N ∈ (L] )N , Basiskanten (u, b, v) und Aufrufkanten (u, q(), v).
]
Zuletzt sind die Abbildungen fA,·
: (L] )NCS → L] definiert durch
]
fA,init
(y) := init]
]
fA,(u,b,v),w
(y) := fb] (y(u,w) )
]
fA,(u,q(),v),w,ent
(y) := y(u,w)
]
(y) := y(rq ,w·(u,q(),v))
fA,(u,q(),v),w·(u,q(),v),ret

wobei wiederum (u, b, v) Basiskanten und (u, q(), v) Aufrufkanten beschreiben.
Um die Lösungen der Ungleichungssysteme besser unterscheiden zu können, schreiben wir im abstrahierten Ungleichungssystem T ] [u], R] [u] und A] [u, w] anstelle von
T [u], R[u] bzw. A[u, w]. Damit wir auch wieder über die kleinsten Lösungen der
abstrahierten Ungleichungssysteme reden können, fordern wir weiter für die abstrakte
Interpretation, dass jeder monotonen Abbildung f ∈ F eine monotone Abbildung f ]
zugeordnert wird.
Wir untersuchen in den folgendenden Abschnitten, ob eine α-korrekte, α-präzise
oder α-kanonische abstrakte Interpretation der Transferfunktionen auch schon eine
entsprechende abstrakte Interpretation der verallgemeinertern Transferfunktionen
induziert. Dazu müssen wir die Abstraktion α auf die entsprechenden Verbände
fortsetzen, die bei den verschiedenen Ungleichungssystemen benutzt werden.

4.3.1 Korrekte abstrakte Interpretation
Zu Beginn dieses Abschnittes haben wir eingeführt, wie wir bezüglich einer vorgegebenen abstrakten Interpretation der Transferfunktionen auch die verallgemeinerten
Transferfunktionen des funktionalen und des Call-String-Ansatzes abstrakt interpretieren wollen. In diesem Abschnitt wollen wir untersuchen, ob eine so induzierte
abstrakte Interpretation der verallgemeinerten Transferfunktionen korrekt ist, wenn
die benutzten Transferfunktionen korrekt abstrakt interpretiert werden.

4.3 Abstrakte Interpretation für interprozedurale Datenflussanalysen 77
Zunächst betrachten wir die konkreten und die zugehörigen abstrahierten Ungleichungssysteme aus dem Ansatz zur Analyse interprozeduraler Programme, der
Summary-Informationen benutzt. Die konkreten Systeme sind durch die Ungleichungssysteme (3.1) und (3.2) für den funktionalen Ansatz und durch das Ungleichungssystem (3.4) für den Call-String-Ansatz gegeben. Um ein abstrahiertes System
zu erhalten, ersetzen wir also, wie zuvor beschrieben, jedes fb durch eine abstrahierte
Abbildung fb] . Speziell ändern wir die Initialwerte idL zu idL] und init zu init] . Dies
induziert korrekt abstrahierte Ungleichungssysteme, wie der folgende Satz zeigt.
Satz 4.23. Sei die abstrakte Interpretation der Transferfunktionen α-korrekt. Dann
ist die dadurch induzierte abstrakte Interpretation der verallgemeinerten Transferfunktionen fT,· auch α-korrekt.
Beweis. Wir beweisen die Aussage, in dem wir die verschiedenen Abbildungen fT,·
der Reihe nach untersuchen. Sei dazu h = (hν )ν∈N ∈ F N beliebig.
Nach Definition gilt
(α ◦fT,· )(h) = α(fT,· (h)) = α ◦ fT,· (h) ◦ γ
und
]
]
]
]
(α̂(h)) = fT,·
((α(hν ))ν∈N ) = fT,·
((α ◦ hν ◦ γ))ν∈N ).
(fT,·
◦ α̂)(h) = fT,·

Es ist also
]
α ◦ fT,· (h) ◦ γ v] fT,·
((α ◦ hν ◦ γ))ν∈N )

zu überprüfen.
i) Zunächst einmal ist
(α ◦ fT,id )(h) ◦ γ = α ◦ idL ◦γ = α ◦ γ.
Außerdem ist
]
fT,id
((α ◦ hν ◦ γ)ν∈N ) = idL] .

Da (α, γ) eine Galois-Verbindung ist, ist α ◦ γ v] idL] . Es gilt also stets die
gewünschte Ungleichung.
ii) Weiter ist für eine Basiskante (u, b, v) ∈ E
α ◦ fT,(u,b,v) (h) ◦ γ = α ◦ fb ◦ hu ◦ γ
und
]
fT,(u,b,v)
((α ◦ hν ◦ γ)ν∈N )) = fb] ◦ α ◦ hu ◦ γ.

Dann gilt nach Voraussetzung also bereits α ◦ fb v] fb] ◦ α und damit ist die
gewünschte Ungleichung erfüllt.

78

4 Abstrakte Interpretation

iii) Zuletzt sei (u, q(), v) ∈ E eine Aufrufkante. Für diesen ist
α ◦ fT,(u,q(),v) (h) ◦ γ = α ◦ hrq ◦ hu ◦ γ
und
]
fT,(u,q(),v)
((α ◦ hν ◦ γ)ν∈N ) = (α ◦ hrq ◦ γ) ◦ (α ◦ hu ◦ γ)

= α ◦ hrq ◦ (γ ◦ α) ◦ hu ◦ γ
Da stets idL v γ ◦ α gilt, ist die gewünschte Ungleichung immer erfüllt.
Es folgt die Behauptung.
Insbesondere gilt also für jeden Knoten u ∈ N
T ] [u] w] α(T [u]).
Wir betrachten nun das Ungleichungssystem zur Berechnung der Informationen
an den Programmpunkten. Als Initialwert des abstrahierten Ungleichungssystem
benutzen wir init] := α(init).
Satz 4.24. Sei die abstrakte Interpretation der Transferfunktionen α-korrekt. Dann
ist die dadurch induzierte abstrakte Interpretation der verallgemeinerten Transferfunktionen fR,· auch α-korrekt.
Beweis. Sei x = (xν )ν∈N ∈ LI . Wir überprüfen die Aussage wieder der Reihe nach
für alle verwendeten Abbildungen.
i) Zunächst ist
(α ◦ fR,init )(x) = α(init)
und
]
(fR,init
◦ α̂)(x) = init] .

Wegen init] = α(init) ist also sogar Gleichheit erfüllt.
ii) Für Basiskanten (u, b, v) ∈ E ist nun
(α ◦ fR,(u,b,v) )(x) = α(fb (xu ))
und
]
(fR,(u,b,v)
◦ α̂)(x) = fb] (α(xu )).

Nach Voraussetzung gilt also die gewünschte Ungleichung.

4.3 Abstrakte Interpretation für interprozedurale Datenflussanalysen 79
iii) Sei nun (u, q(), v) eine Aufrufkante. Dann ist einerseits
(α ◦ fR,(u,q(),v),ent )(x) = α(xu )
und
]
(fR,(u,q(),v),ent
◦ α̂)(x) = α(xu )

und es gilt immer Gleichheit. Andererseits ist
(α ◦ fR,(u,q(),v),ret )(x) = α(T [rq ](xu ))
und
]
(fR,(u,q(),v),ret
◦ α̂)(x) = T ] [rq ](α(xu )).

Wie wir in Satz 4.23 gesehen haben, ist die abstrakte Interpretation von T stets
korrekt. Somit erhalten wir auch hier direkt die gewünschte Ungleichung.
Es folgt die Behauptung.
Für jeden Knoten u ∈ N gilt also
R] [u] w α(R[u]).
Wir betrachten nun das Ungleichungssystem (3.4), das eine Analyse mithilfe von
Call-Strings beschreibt. Wie im funktionalen Ansatz fordern wir als Startinformation
des abstrakt interpretierten Ungleichungssystems init] = α(init).
Satz 4.25. Sei die abstrakte Interpretation der Transferfunktionen α-korrekt. Dann
ist die dadurch induzierte abstrakte Interpretation der verallgemeinerten Transferfunktionen fA,· auch α-korrekt.
Beweis. Wie zuvor betrachten wir wieder die verschiedenen Abbildungen. Sei dazu
x ∈ LNCS .
i) Zunächst ist wiederum
(α ◦ fA,init )(x) = α(init)
und
]
(fA,·
◦α
b)(x) = init]

Da init] = α(init), gilt hier wiederum sogar Gleichheit.

80

4 Abstrakte Interpretation

ii) Weiter ist für Basiskanten (u, b, v) ∈ E
(α ◦ fA,(u,b,v),w )(x) = α(fb (xu,w ))
und
]
(fA,(u,b,v),w
◦α
b)(x) = fb] (α(xu,w )).

Nach Voraussetzung gilt also die gewünschte Ungleichung.
iii) Wir betrachten nun eine Aufrufkante e = (u, q(), v) ∈ E. Dann ist
(α ◦ fA,(u,q(),v),w,ent )(y) = α(yu,w )
und
]
(fA,(u,q(),v),w,ent
◦α
b)(y) = α(yu,w )

und es gilt sogar Gleichheit. Für die Abbildung, die die Rückkehr aus einer
Prozedur beschreibt, ist
(α ◦ fA,(u,q(),v),w·e,ret )(y) = α(hrq ,w·e )
und ebenso
]
(fA,(u,q(),v),w·e,ret
◦α
b)(y) = α(hrq ,w·e ).

Auch hier gilt also stets Gleichheit.
Es folgt die Behauptung.
Für jeden Knoten u ∈ N und Call-String w ∈ CS erhalten wir also
A] [u, w] w] α(A[u, w]).
Damit ist
G] 

A] [u, w] | w ∈ CS[p]
G] 
w]
α(A[u, w]) | w ∈ CS[p]
G

=α
A[u, w] | w ∈ CS[p]

Â] [u] =

= α(Â[u]).
Die Lösung des Ungleichungssystem, das eine Analyse durch Call-Strings beschreibt,
wird also durch eine α-korrekte abstrakte Interpretation der Transferfunktionen
wieder α-korrekt abstrahiert. Im nächsten Abschnitt zeigen wir, dass auch α-Präzision
übertragen wird.

4.3 Abstrakte Interpretation für interprozedurale Datenflussanalysen 81

4.3.2 Präzise abstrakte Interpretation
In Unterabschnitt 4.3.1 haben wir Transferfunktionen korrekt abstrakt interpretiert
und dadurch in beiden Ansätzen zur interprozeduralen Datenflussanalyse korrekte
abstrakte Interpretation der Ungleichungssysteme erhalten. Wir werden nun sehen,
dass durch eine präzise abstrakte Interpretation der Transferfunktionen auch die
Ungleichungssysteme beider Ansätze präzise abstrahiert werden, wenn wir für die
Galois-Verbindung zusätzlich α ◦ γ = idL] fordern.
Diese Forderung ist natürlich: Nach Definition gilt zunächst α ◦ γ v] idL] . Ist nun für
ein y ∈ L] tatsächlich
y 0 := (α ◦ γ)(y) @ y,
so folgt mit Lemma 4.7
γ(y 0 ) = (γ ◦ α ◦ γ)(y) = γ(y).
Die beiden abstrakten Werte y und y 0 werden also demselben konkreten Wert zugeordnet. Somit können Werte im abstrakten Raum unterschieden werden, die im
konkreten Raum nicht unterschieden werden können. Dies ist unnatürlich, da der
konkrete Raum genauere Informationen liefern sollte als der abstrakte.
Satz 4.26. Sei die abstrakte Interpretation der Transferfunktionen α-präzise und
gelte α ◦ γ = idL] . Dann ist die dadurch induzierte abstrakte Interpretation der
verallgemeinerten Transferfunktionen fT,· auch α-präzise.
Beweis. Sei h = (hν )ν∈N ∈ F N beliebig. Nach dem Beweis von Satz 4.23 bleibt nun
α ◦ γ = idL] ,
für eine Basiskante (u, b, v) ∈ E
α ◦ fb ◦ hu ◦ γ = fb] ◦ α ◦ hu ◦ γ,
und für einen Prozeduraufruf (u, q(), v) ∈ E
α ◦ hrq ◦ hu ◦ γ = α ◦ hrq ◦ (γ ◦ α) ◦ hu ◦ γ
zu zeigen. Die ersten beiden Gleichungen folgen direkt aus der Voraussetzung. Die
letzte Gleichung folgt aus Lemma 4.16.
Es gilt also T ] [u] = α(T [u]) für jeden Knoten u ∈ N .
Wir betrachten nun das Ungleichungssystem zur Berechnung der eigentlichen Informationen.

82

4 Abstrakte Interpretation

Satz 4.27. Sei die abstrakte Interpretation der Transferfunktionen α-präzise und
gelte α ◦ γ = idL] . Dann ist die dadurch induzierte abstrakte Interpretation der
verallgemeinerten Transferfunktionen fR,· auch α-präzise.
Beweis. Sei x = (xν )ν∈N ∈ LI . Nach dem Beweis von Satz 4.24 muss nur noch für
Basiskanten (u, b, v) ∈ E
α(fb (xu )) = fb] (α(xu ))
und für Prozeduraufrufe (u, q(), v) ∈ E
α(T [rq ](xu )) = T ] [rq ](α(xu ))
gezeigt werden. Ersteres folgt direkt aus der Voraussetzung und letzteres aus Satz
4.26.
Es gilt also R] [u] = α(R[u]) für jeden Knoten u ∈ N .
Unter der zusätzlichen Voraussetzung α ◦ γ = idL] gewinnt man aus der präzisen
abstrakten Interpretation der Transferfunktionen bereits präzise abstrahierte Ungleichungssysteme, wie sie zum Berechnen von Informationen mithilfe von SummaryInformationen benutzt werden. Ein entsprechendes Resultat gilt auch für den CallString-Ansatz.
Satz 4.28. Sei die abstrakte Interpretation der Transferfunktionen α-präzise. Dann
ist die dadurch induzierte abstrakte Interpretation der verallgemeinerten Transferfunktionen fA,· auch α-präzise.
Beweis. Nach dem Beweis von Satz 4.25 genügt es, für Prozeduren p ∈ Proc, Basiskanten (u, b, v) ∈ Ep , Call-Strings w ∈ CS[p] und x ∈ LNCS
α(fb (yu,w )) = fb] (α(yu,w ))
zu zeigen. Dies folgt aber direkt aus der Voraussetzung.
Es gilt also A] [u, w] = α(A[u, w]) für alle (u, w) ∈ NCS . Ähnlich wie für Satz 4.25
erhalten wir nun
Â] [u] = α(Â[u]).
Die Lösung des Ungleichungssystem aus dem Call-String-Ansatz wird also durch eine
präzise abstrakte Interpretation der Transferfunktionen wieder präzise abstrahiert.
In diesem Fall liefern also beide Ansätze zur Analyse interprozeduraler Programme wieder dasselbe Ergebnis, wenn die verwendeten Transferfunktionen geeignete
Distributivitätsbedingungen erfüllen.

4.3 Abstrakte Interpretation für interprozedurale Datenflussanalysen 83
Korollar 4.29. Sei das monotone Framework (L, v, F) universell-distributiv oder
positiv-distributiv und in letzterem Fall alle Programmpunkte erreichbar. Sei die
zugrundeliegende abstrakte Interpretation der Transferfunktionen α-präzise und gelte
α ◦ γ = idL] . Dann stimmen die kleinsten Lösungen der abstrahierten Ungleichungssysteme überein, d.h. es gilt
R] = Â] .
Beweis. Dies folgt unmittelbar aus den Sätzen 4.27, 3.7 und 4.28: Für beliebiges
u ∈ N gilt
R] [u] = α(R[u]) = α(Â[u]) = Â] [u].
Dies ist die Behauptung.

4.3.3 Kanonische abstrakte Interpretation
In Unterabschnitt 4.3.1 und Unterabschnitt 4.3.2 haben wir gesehen, dass unter den
Voraussetzungen α ◦ γ = idL] und init] = α(init) eine präzise abstrakte Interpretation der verwendeten Transferfunktionen zu einer präzisen abstrakten Interpretation
der Ungleichungssysteme aus dem funktionalen und dem Call-String-Ansatz führt.
Wir werden nun zeigen, dass unter denselben Forderungen eine kanonische abstrakte
Interpretation der Transferfunktionen wieder eine kanonische abstrakte Interpretation der verallgemeinerten Transferfunktionen induziert. Sei also im Folgenden
f + = α ◦ f ◦ γ für die Transferfunktionen f ∈ F. Die dadurch abstrahierten verallge]
]
]
meinerten Transferfunktionen bezeichnen wir mit fT,·
, fR,·
und fA,·
. Die kanonisch
abstrahierten verallgemeinerten Transferfunktionen bezeichnen wir entsprechend mit
+
+
+
fT,·
, fR,·
und fA,·
. Diese sind gegeben durch
+
fT,·
:= α ◦fT,· ◦ γ̂,
+
fR,·
:= α ◦ fR,· ◦ γ̂,
+
:= α ◦fA,· ◦ γ̂.
fA,·

Wir zeigen nun, dass die kanonisch oder durch die f + abstrahierten verallgemeinerten
Transferfunktionen jeweils übereinstimmen, wenn wir zusätzlich α ◦ γ = idL] fordern.
Wir beginnen mit dem funktionalen Ansatz.
]
+
Satz 4.30. Sei α ◦ γ = idL] . Dann gilt fT,·
= fT,·
.

Beweis. Wir betrachten wiederum der Reihe nach die verschiedenen Abbildungen
]
+
+
fT,· und überprüfen fT,·
= fT,·
. Dabei ist fT,·
:= α ◦fT,· ◦ γ̂ wie in Abbildung 4.3.

84

4 Abstrakte Interpretation

FO N

fT,·

γ̂

/

(F ] )N

+
fT,·

/

F


α

F]

Abbildung 4.3: Kanonische abstrakte Interpretation der Abbildungen fT,· .
Für h = (hν )ν∈N ∈ (F ] )N ist also
+
fT,·
(h) = α(fT,· (γ̂(h))) = α ◦ (fT,· ((γ ◦ hν ◦ α)ν∈N ) ◦ γ.

Wir benutzen bei jeder der folgenden Rechnungen α ◦ γ = idL] . Zunächst gilt für die
Startinformation
+
fT,id
(h) = α ◦ fT,id ((γ ◦ hν ◦ α)ν∈N ) ◦ γ

= α ◦ idL ◦γ
=α◦γ
= idL]
]
= fT,id
(h).

Sei (u, b, v) ∈ E eine Basiskante. Dann ist
+
fT,(u,b,v)
(h) = α ◦ fT,(u,b,v) ((γ ◦ hν ◦ α)ν∈N ) ◦ γ

= α ◦ (fb ◦ (γ ◦ hu ◦ α)) ◦ γ
= (α ◦ fb ◦ γ) ◦ hu ◦ (α ◦ γ)
= fb+ ◦ hu
]
= fT,(u,b,v)
(h).

Sei nun (u, q(), v) ∈ E eine Aufrufkante. Dann gilt
+
fT,(u,q(),v)
(h) = α ◦ fT,(u,(),v) ((γ ◦ hν ◦ α)ν∈N ) ◦ γ

= α ◦ (γ ◦ hrq ◦ α) ◦ (γ ◦ hu ◦ α) ◦ γ
= (α ◦ γ) ◦ hrq ◦ (α ◦ γ) ◦ hu ◦ (α ◦ γ)
= hrq ◦ hu
]
= fT,(u,b,v)
(h).

Es folgt die Behauptung.

4.3 Abstrakte Interpretation für interprozedurale Datenflussanalysen 85
Eine entsprechende Aussage können wir auch für das Ungleichungssystem zur Berechnung der gesuchten Informationen zeigen:
]
+
Satz 4.31. Sei α ◦ γ = idL] . Dann gilt fR,·
= fR,·
.

]
+
+
Beweis. Wir überprüfen also fR,·
= fR,·
für fR,·
:= α ◦ fR,· ◦ γ̂ wie in Abbildung 4.4.

LN
O

fR,·

γ̂

/

(L] )N

+
fR,·

/

L


α

L]

Abbildung 4.4: Kanonische abstrakte Interpretation der Abbildungen fR,· .

Sei y = (yν )ν∈N ∈ (L] )N beliebig. Dann gilt für die Startinformation
+
fR,init
(y) = (α ◦ fR,init ◦ γ̂)(y)

= α(init)
= init]
]
= fR,init
(y).

Für eine Basiskante (u, b, v) ∈ E ist
+
fR,(u,b,v)
(y) = (α ◦ fR,(u,b,v) ◦ γ̂)(y)

= α(fb (γ(yu )))
= fb+ (yu )
]
= fR,(u,b,v)
(y).

Zuletzt gilt für Aufrufe (u, q(), v) ∈ E einerseits
+
fR,(u,q(),v),ent
(y) = (α ◦ fR,(u,q(),v),ent ◦ γ̂)(y)

= α(γ(yu ))
= yu
]
= fR,(u,q(),v),ent
(y).

86

4 Abstrakte Interpretation

und andererseits mit Satz 4.30
+
fR,(u,q(),v),ret
(y) = (α ◦ fR,(u,q(),v),ret ◦ γ̂)(y)

= α(T [rq ]((γ(yu )))
= α(T [rq ])(yu )
= T + [rq ](yu )
]
= fR,(u,q(),v),ret
(y).

Es folgt die Behauptung.
Im funktionalen Ansatz erhält man also eine kanonische Abstraktion der verallgemeinerten Transferfunktionen, wenn die benutzten Transferfunktionen kanonisch
abstrahiert werden. Dies gilt auch für den Call-String-Ansatz, wie der folgende Satz
zeigt.
]
+
Satz 4.32. Sei α ◦ γ = idL] . Dann gilt fA,·
= fA,·
.

]
+
+
= fA,·
für fA,·
:= α ◦fA,· ◦ γ̂ wie in Abbildung 4.5.
Beweis. Wir überprüfen also fA,·

LNO CS

fA,·

/

L

γ̂

(L] )NCS

+
fA,·

/



α

L]

Abbildung 4.5: Kanonische abstrakte Interpretation der Abbildungen fA,· .
Sei nun y ∈ (L] )NCS . Für die Abbildungen gilt allgemein

+
fA,·
(y) = (α ◦fA,· ◦ γ̂)(y) = α fA,· ((γ(yν,w ))(ν,w)∈NCS ) .
Wir betrachten nun die einzelnen Abbildungen.
Für die Startinformation gilt dann

+
fA,init
(y) = α fA,init ((γ(yν,w ))(ν,w)∈NCS )
= α(init)
= init]
]
(y).
= fA,init

4.3 Abstrakte Interpretation für interprozedurale Datenflussanalysen 87
Ist (u, b, v) ∈ Ep eine Basiskante, so ist

+
fA,(u,b,v),w
(y) = α fA,(u,b,v),w ((γ(yν,w ))(ν,w)∈NCS )

= α fb (γ(yu,w ))
= fb+ (yu,w )
]
= fA,(u,b,v),w
(y).

Entsprechend gilt für Aufrufkanten e = (u, q(), v) ∈ Ep

+
fA,(u,q(),v),ent
(y) = α fA,(u,q(),v),w,ent ((γ(yν,w ))(ν,w)∈NCS )

= α γ(yu,w )
= yu,w
]
= fA,(u,q(),v),w,ent
(y).

und

+
fA,(u,q(),v),ret
(y) = α fA,(u,q(),v),w·e,ret ((γ(yν,w ))(ν,w)∈NCS )
= α(γ(yrq ,w·e ))
= yrq ,w·e
]
= fA,(u,q(),v),w·e,ret
(y).

Es folgt die Behauptung.
In einer Situation, in der die Transferfunktionen nicht präzise abstrakt interpretiert
werden können, ist es also grundsätzlich sinnvoll, sie kanonisch zu interpretieren, da
dies nach Satz 4.19 die beste“, d.h. kleinste korrekte Lösung auf dem abstrakten
”
Verband liefert. Die vorigen Sätze 4.31 und 4.32 zeigen nun, dass dadurch auch die
verallgemeinerten Transferfunktionen kanonisch abstrahiert werden. Die zugehörigen
abstrahierten Ungleichungssysteme liefern also auch wieder die beste Lösung auf
dem abstrakten Verband. Für den funktionalen und den Call-String-Ansatz zur
interprozeduralen Datenflussanalyse ist demnach zu empfehlen, die Transferfunktionen
stets kanonisch abstrakt zu interpretieren, da dies in jedem Fall die kleinste korrekte
Lösung liefert. In Situationen, in denen es sogar präzise abstrakte Interpretationen
gibt, erhält man eine solche durch die kanonische abstrakte Interpretation.
Im folgenden Abschnitten betrachten wir wiederum die Polyederanalyse und studieren
abstrakte Interpretationen anhand der Bildung konvexer Hüllen. Die letzten beiden
Lemmata liefern ein Indiz dafür, dass die Bildung konvexer Hüllen im Rahmen der
Polyederanalyse eine korrekte oder sogar präzise abstrakte Interpretation ist.

88

4 Abstrakte Interpretation

4.4 Polyederanalyse und konvexe Hüllenbildung
Im Rahmen der Polyederanalyse
werden zu jedem Programmpunkt affine UngleiPn
chungen der Gestalt i=1 ai xi ≥ a0 bestimmt, welche für die möglichen Werte der
Variablen an diesem Programmpunkt gelten. Die Menge aller Werte, die solche
Ungleichungen erfüllen, bildet ein konvexes Polyeder.
In Abschnitt 3.4 haben wir bereits Datenflussanalysen zur Berechnung der erreichbaren Variablenwerte eingeführt. Gültige Ungleichungen über diese Variablenwerte
erhalten wir nun, indem wir die konvexen Hüllen dieser Wertemengen bestimmen.
Dabei orientieren wir uns an [SFP07]. Wir werden zeigen, dass die Bildung konvexer
Hüllen eine Abstraktion ist. Ziel ist nun, eine präzise abstrakte Interpretation der
Transferfunktionen aus Abschnitt 3.4 zu finden, so dass die konvexen Mengen direkt
berechnet werden können, ohne dafür zuerst die Ungleichungen zur Berechnung der erreichbaren Variablenwerte zu lösen. Wir werden also in diesem Abschnitt zunächst eine
abstrakte Interpretationen für die Ungleichungssysteme aus Abschnitt 3.4 einführen
und diese dann im Hinblick auf Korrektheit und Präzision untersuchen. Wir sagen im
Folgenden korrekt“ anstelle von α-korrekt“ und präzise“ anstelle von α-präzise“
”
”
”
”
für einen konkreten Hüllenoperator α. Wir werden sehen, dass wir für den Ansatz mit
Matrizenmengen eine präzise abstrakte Interpretation angeben können, wohingegeben
eine analog definierte abstrakte Interpretation für den Ansatz mit Relationen zwar
korrekt, aber im Allgemeinen nicht präzise ist. Im Gegensatz zu Abschnitt 3.4 liefern
die beiden Ansätze hier also nicht dasselbe Ergebnis.
Wir werden die Ungleichungssysteme aus Abschnitt 3.4 durch die Bildung konvexer
Hüllen abstrahieren. Um anschließende Aussagen über die Korrektheit und Präzision
einer solchen abstrakten Interpretation zu treffen, benutzen wir die folgenden beiden
Lemmata, die Aussagen über beliebige Hüllenoperatoren treffen. Das erste Lemma
zeigt dabei, dass eine abstrakte Interpretation durch Hüllenbildung bereits die kanonische abstrakte Interpretation ist. Das zweite Lemma benennt Spezialfälle für
Abbildungen, die bezüglich dieser abstrakten Interpretation schon die Gestalt haben,
wie sie in der Definition einer präzisen abstrakten Interpretation gefordert wird. Wir
erinnern daran, dass eine kanonische abstrakte Interpretation nur dann präzise ist,
wenn die zugrundeliegende Galois-Verbindung eine präzise abstrakte Interpretation
zulässt, und dass letzteres nicht immer der Fall ist. Dies haben wir durch Satz 4.19
und Beispiel 4.20 gezeigt. Das zweite Lemma ist also nicht trivial.
Lemma 4.33. Sei (L, v) ein vollständiger Verband, α : L → L ein Hüllenoperator,
f : LI → L für eine Indexmenge I und f ] := α ◦ f für jeden verwendeten Operator f .
Dann ist f ] = f + . Insbesondere ist eine solche abstrakte Interpretation α-korrekt und
sogar α-präzise, falls (α, id) eine präzise abstrakte Interpretation erlaubt.
Beweis. Dies folgt unmittelbar aus Lemma 4.10 und Satz 4.19.

4.4 Polyederanalyse und konvexe Hüllenbildung

89

Lemma 4.34. Sei (L, v) ein vollständiger Verband, α : L → L ein Hüllenoperator,
f : LI → L monoton und f ] := α ◦ f . Ist f konstant oder eine Projektion, so gilt
f ] ◦ α̂ = α ◦ f .
Beweis. Sei f zunächst konstant, d.h. für ein l ∈ L sei f (x) = l für jedes x ∈ LI .
Dann ist
f ] ◦ α̂(x) = α(f (α̂(x))) = α(l) = α(f (x)) = α ◦ f (x).
Ist f eine Projektion, das heißt f (x) = xi für ein i ∈ I und jedes x ∈ LI , so gilt
f ] ◦ α̂(x) = α(f (α̂(x))) = α(α(xi )) = α(xi ) = α(f (x)) = α ◦ f (x).
Es folgt die Behauptung.
Wir definieren nun, was eine konvexe Hülle ist.
Definition 4.35. Sei V ein R-Vektorraum. Eine Menge X ⊆ V heißt konvex , falls
λv + (1 − λ)w ∈ X für alle 0 ≤ λ ≤ 1 und v, w ∈ X.
Die konvexe Hülle einer Teilmenge X ⊆ V ist die kleinste konvexe Menge hXi, die
X enthält.
Bemerkung 4.36. Sei V ein R-Vektorraum.
a) Sei C(V ) := {C ⊆ V | C konvex} die Menge der konvexen
S von
F Teilmengen
V . Dann ist (C(V ), ⊆) ein vollständiger Verband, wobei C(V ) X = h X i für
X ⊆ C(V ).
b) Schreibe X ⊆ V als X = {xi | i ∈ I} für eine Indexmenge I. Dann ist die
konvexe Hülle von X gegeben durch
nX
o
X
hXi =
λi xi | λi ≥ 0, fast alle λi = 0,
λi = 1 .
i∈I

i∈I

c) Die Abbildung α : 2V → C(V ), X 7→ hXi ist ein Hüllenoperator und damit eine
Abstraktion.
d) Falls X ⊆ V eine konvexe Menge ist, so ist für jedes A ⊆ X auch hAi ⊆ X.
Wir können die Bildung konvexer Hüllen also einschränken zu einer Abbildung
2X → C(X).
e) Die Mengen Σ = {1} × Rn ⊆ Rn+1 , Mat(Σ) und Rn × Rn sind konvexe Teilmengen von Vektorräumen.

90

4 Abstrakte Interpretation

Sowohl für Matritzenmengen, Relationen als auch Zustandsmengen gilt also, dass die
Bildung konvexer Hüllen auf dem zugrundeliegenden Verband operiert.
Wir bezeichnen dabei die Bildung konvexer Hüllen mit
α : L → L] ,
αM : LM → L]M ,
αR : LR → L]R .
Dabei hatten wir
L = 2Σ ,
LM = 2Mat(Σ) ,
LR = 2R

n

× Rn

definiert und setzen weiter
L] := C(Σ) ⊆ L,
L]M := C(Mat(Σ)) ⊆ LM ,
L]R := C(Rn × Rn ) ⊆ LR .
als die entsprechenden Mengen konvexer Teilmengen. Nach Aussage c) und d) sind
diese Abbildungen wohldefiniert.

Wir abstrahieren nun die Ungleichungssysteme, indem wir konvexe Hüllen bilden. Die
abstrahierten Ungleichungssysteme versehen wir mit dem Symbol ] . Die abstrahierten
Abbildungen, welche diese Ungleichungssysteme definieren, sind nun gegeben durch
fT] M ,· := αM ◦ fTM ,·

fR] M ,· := α ◦ fRM ,·

fT] R ,· := αR ◦ fTR ,·

fR] R ,· := α ◦ fRR ,·

]
fA,·
:= α ◦ fA,·

für alle Ungleichungen bis auf diejenigen, die beim funktionalen Ansatz die Rückkehr
aus einer Prozedur beschreiben. Diese werden zusätzlich so geändert, dass nicht der
im Ungleichungssystem TM bzw. TR berechnete Effekt einer Prozedur verwendet wird,
]
sondern stattdessen TM
bzw. TR] :
]
fR] M ,(u,q(),v),ret := α ◦ (αMat (TM
[rq ]) ◦ pru ),

fR] R ,(u,q(),v),ret := α ◦ (αRel (TR] [rq ]) ◦ pru ).

4.4 Polyederanalyse und konvexe Hüllenbildung

91

Bemerkung 4.37. Es reicht nicht, fR] M ,(u,q(),v),ret := fT ] [rq ] ◦ pru zu betrachten, da
M
fT ] [rq ] ◦ pru nicht auf konvexen Mengen operiert: Dazu betrachten wir
M


 
1 −1
1
A=
∈ Mat(2, R), x =
∈ R2 ,
1 −1
0


 
−1 −1
0
B=
∈ Mat(2, R), y =
∈ R2 .
−1 −1
1
Für die Matrizenmenge A = {A, B} und die Zustandsmenge S = {x, y} ist dann



2λ − 1 1 − 2λ
αMat (A) =
|0≤λ≤1
2λ − 1 2λ − 1
 


1 −1
= a·
| −1 ≤ a ≤ 1
1 −1
und

α(S) =

µ
1−µ




|0≤µ≤1 .

Damit erhalten wir nun
X := αMat (αM (A))(α(S))
 


µ − (1 − µ)
= a·
| −1 ≤ a ≤ 1 ∧ 0 ≤ µ ≤ 1
µ + (1 − µ)
 


2µ − 1
= a·
| −1 ≤ a ≤ 1 ∧ 0 ≤ µ ≤ 1
1
  

b
= a·
| −1 ≤ a ≤ 1 ∧ −1 ≤ b ≤ 1 .
1
Es gilt für v ∈ X: Ist v2 = 0, so ist auch v1 = 0. Ist nämlich
v = ( ab
a ) ∈ X und

−1
v2 = a = 0, so ist auch v1 = ab = 0. Nun sind ( 11 ) und −1 ∈ X vermöge a = b = 1
bzw. a = b = −1. Andererseits gilt aber für deren Konvexkombination
 
 
 
1
1
−1
= 12
+ 21
∈
/ X.
0
1
−1
Folglich kann X nicht konvex sein. Diese Menge ist in Abbildung 4.6 dargestellt.
Setzen wir nun


 
1 0 0
1



Ã := 0
, x̃ := x1  ,
A
0
x2


 
1 0 0
1
 , ỹ := y1  ,
B̃ := 0
B
0
y2

92

4 Abstrakte Interpretation
x2
Ay 1

−1
Bx −1

Ax
x1
1
By

Abbildung 4.6: Notwendigkeit der konvexen Hüllenbildung.

so erhalten wir ein Gegenbeispiel in {1} × R2 und Mat({1} × R2 ).



Wir wollen nun untersuchen, ob die Bildung konvexer Hüllen für die in Abschnitt 3.4
eingeführten Analysen korrekt oder sogar präzise ist. Da die Ungleichungssysteme
TM und TR nicht direkt die Transferfunktionen berechnen, sind die Resultate aus
Abschnitt 4.3 hier nicht anwendbar. Wir brauchen also neue Betrachtungen, die wir
im folgenden Abschnitt präsentieren werden. Wir orientieren uns dabei erneut an
[CH78] und [SFP07].
]
]
Satz 4.38. Die Ungleichungssysteme TM , RM , TR und RR werden durch TM
, RM
,
]
]
TR und RR korrekt abstrahiert.

Beweis. Nach Lemma 4.33 wissen wir bereits, dass die abstrakten Interpretationen
]
TM
von TM und TR] von TR korrekt ist. Da αM und αR Hüllenoperatoren sind, gilt
also für jede Prozedur q ∈ Proc
]
TM
[rq ] ⊇ αM (TM [rq ]) ⊇ TM [rq ] und TR] [rq ] ⊇ αR (TR [rq ]) ⊇ TR [rq ].

In Beispiel 4.8 haben wir gesehen, dass die Abbildungen αMat und αRel Abstraktionen
und damit insbesondere monoton sind. Da auch α monoton ist, erhalten wir
]
fR] M ,(u,q(),v),ret =α ◦ (αMat (TM
[rq ]) ◦ pru )

wα ◦ (αMat (TM [rq ]) ◦ pru )
=α ◦ fRM ,(u,q(),v),ret
und ebenso
fR] R ,(u,q(),v),ret wα ◦ fRR ,(u,q(),v),ret .
]
]
Nach Satz 4.19 abstrahieren also RM
und RR
die Ungleichungssysteme RM und RR
korrekt.

4.4 Polyederanalyse und konvexe Hüllenbildung

93

]
Zunächst zeigen wir, dass TM
auch eine präzise abstrakte Interpretation von TM
beschreibt. Dazu benötigen wir die folgenden beiden technischen Hilfsmittel.

Lemma 4.39. Sei X ⊆ {1} × Rn und A, A1 , A2 ⊆ Mat(n + 1, R). Dann gelten
folgende Identitäten:
a) α(αMat (A)(X)) = α(αMat (αM (A))(α(X)))
b) αMat (A1 ◦ A2 ) = αMat (αMat (A1 ) ◦ αMat (A2 )).

Beweis. Es ist nach Definition
α(αMat (αM (A))(α(X)))
= α({Ax | x ∈ α(X) ∧ A ∈ αM (A)})

= α (λA1 + (1 − λ)A2 )x | 0 ≤ λ ≤ 1 ∧ A1 , A2 ∈ A ∧ x ∈ α(X)}

= α λA1 x + (1 − λ)A2 x | 0 ≤ λ ≤ 1 ∧ A1 , A2 ∈ A ∧ x ∈ α(X)}
= α({Ax | x ∈ α(X) ∧ A ∈ A})

= α A(λx1 + (1 − λ)x2 ) | 0 ≤ λ ≤ 1 ∧ A ∈ A ∧ x1 , x2 ∈ X}

= α λAx1 + (1 − λ)Ax2 | 0 ≤ λ ≤ 1 ∧ A ∈ A ∧ x1 , x2 ∈ X}
= α({Ax | x ∈ X ∧ A ∈ A})
= α(αMat (A)(X))
und
αM (αM (A1 ) ◦ αM (A2 ))
= αM ({A1 A2 | A1 ∈ αM (A1 ), A2 ∈ αM (A2 )})


= αM (λA11 + (1 − λ)A21 )A2 | 0 ≤ λ ≤ 1, A11 , A21 ∈ A1 , A2 ∈ αM (A2 )


= αM λA11 A2 + (1 − λ)A21 A2 | 0 ≤ λ ≤ 1, A11 , A21 ∈ A1 , A2 ∈ αM (A2 )

= αM ({A1 A2 | A1 ∈ A1 , A2 ∈ αM (A2 )


= αM A1 (λA12 + (1 − λ)A22 ) | 0 ≤ λ ≤ 1, A1 ∈ A1 , A12 , A22 ∈ A2


= αM λA1 A12 + (1 − λ)A1 A22 | 0 ≤ λ ≤ 1, A1 ∈ A1 , A12 , A22 ∈ A2
= αM ({A1 A2 | Ai ∈ Ai })
= αM (A1 ◦ A2 ).
Es folgt die Behauptung.
Korollar 4.40. Es gilt α ◦ (fxj :=t ◦ pru ) ◦ α̂ = α ◦ (fxj :=t ◦ pru ).

94

4 Abstrakte Interpretation

Beweis. Sei S ∈ L, dann ist nach Lemma 4.39
α ◦ fxj :=t (S) = α({Mxj :=t · s | s ∈ S})
= α({Mxj :=t · s | s ∈ α(S)})
= α ◦ fxj :=t ◦ α(S).
Damit und mit der Identität α ◦ pru ◦ α̂ = α ◦ pru ist
α ◦ fxj :=t ◦ pru ◦ α̂ = α ◦ fxj :=t ◦ α ◦ pru ◦ α̂
= α ◦ fxj :=t ◦ α ◦ pru
= α ◦ fxj :=t ◦ pru ,
wobei letzte Gleichheit vermöge α ◦ fxj :=t ◦ α = α ◦ fxj :=t gilt.
]
]
Satz 4.41. Die abstrakte Interpretationen TM
und RM
von TM bzw. RM sind präzise.

Beweis. Nach Definition ist fT] M ,· ◦ α̂M = αM ◦ fTM ,· und fR] M ,· ◦ α̂R = αR ◦ fRM ,· zu
zeigen.
Da fTM ,id und fRM ,init konstante Abbildungen sind und fRM ,(u,q(),v),ent = pru eine
Projektion ist, folgt hierfür die gewünschte Gleichheit schon nach Korollar 4.34. Für
fTM ,xj :=t = fxj :=t ◦ pru und fRM ,(u,xj :=t,v) = fxj :=t ◦ pru erhalten wir die Gleichheit
mit Korollar 4.40. Nach Lemma 4.39 gilt nun
fT] M ,q() ◦ α̂M (A) = αM (Arq ◦ αM (Au ))
= αM (Arq ◦ Au )
= αM (fTM ,q() (A)).
Die Bildung konvexer Hüllen ist also bei der Berechnung von Matrizenmengen zur
]
Bildung von Summary-Informationen präzise. Insbesondere gilt αM (TM [rq ]) = TM
[rq ]
für jede Prozedur q ∈ Proc. Daraus folgt nun, wiederum mit Lemmma 4.39,
]
[rq ])(α(Su ))
fR] M ,(u,q(),v),ret ◦ α̂(S) = α(αMat (TM

= α(αMat (αM (TM [rq ]))(α(Su ))
= α(αMat (TM [rq ])(Su )
= fRM ,(u,q(),v),ret (S).
Somit ist auch die Bildung konvexer Hüllen bei den erreichbaren Zuständen eine
präzise abstrakte Interpretation, wenn die Summary-Informationen mithilfe von
Matrizenmengen berechnet werden.

4.4 Polyederanalyse und konvexe Hüllenbildung

95

Verwendet man anstelle von Matrizenmengen dagegen Relationen, um Summary-Informationen zu berechnen, so ist die Bildung konvexer Hüllen keine präzise abstrakte
Interpretation.
]
Satz 4.42. Die abstrakten Interpretationen TR] und RR
von TR bzw. RR sind im
Allgemeinen nicht präzise.

Beweis. Es genügt, ein Beispiel zu finden, bei dem konvexe Hüllenbildung nicht
präzise ist. Betrachte dazu den Flussgraphen aus Abbildung 4.7. Es ist
main:

0

p:
x := 0

1

3
p()

2

x := x

x := 0
4

Abbildung 4.7: Die Bildung konvexer Hüllen für Relationen als Summary-Information
kann unpräzise sein.
T [4] = {(x, x) | x ∈ R} ∪ {(x, 0) | x ∈ R}
und
R[0] = R
R[1] = {0}
R[2] = {0} ∪ {0} = {0}.
Andererseits haben wir
T ] [4] = h{(x, x) | x ∈ R} ∪ {(x, 0) | x ∈ R}i
= {λ(x, x) + (1 − λ)(y, 0) | 0 ≤ λ ≤ 1, x, y ∈ R}
= {(z, x) | x, z ∈ R}
= R×R

96

4 Abstrakte Interpretation

sowie
R] [0] = R
R] [1] = {0}
R] [2] = R ) {0} = hR[2]i.
Die abstrakte Interpretation ist also nicht präzise.
In dem Schritt der Berechnung, in dem konvexe Hüllen gebildet werden, liefert
der Ansatz mit Matrizenmengen, im Gegensatz zu dem relationalen Ansatz, ein
präzises Ergebnis. Zur Berechnung gültiger Ungleichungen in einem Programmpunkt
ist demnach die Verwendung von Matrizenmengen als Summary-Information der
bessere Ansatz.
Das folgende Beispiel zeigt, dass die Bildung konvexer Hüllen noch keine Terminierung
garantiert.
Beispiel 4.43. Betrachte das Programm aus Abbildung 4.8.
main:

p:

s

u
p()
x := x + 1

r

Abbildung 4.8: Konvexe Hüllenbildung garantiert keine Terminierung.
Das zugehörige Ungleichungssystem zur Berechnung konvexer Matrizenmengen besteht für die Prozedur p aus den beiden Ungleichungen
]
]
]
TM
[u] ⊇ {E2 } und TM
[u] ⊇ αM ({M } ◦ TM
[u])

für die Matrix


1 0
M=
.
1 1
Da im Workset-Algorithmus die Berechnung einer kleinsten Lösung für den Programmpunkt u unabhängig von den Werten in den Programmpunkten s und r ist,

4.4 Polyederanalyse und konvexe Hüllenbildung

97

können wir die Ungleichungen für diese Punkte vernachlässigen. Für u produziert
]
der Workset-Algorithmus folgende Werte: Zunächst erhält TM
[u] den Wert {E2 } und
die Workset enthält die zweite Ungleichung. Dann wird
αM ({M } ◦ {E2 }) = αM ({M }) = {M }
]
als neuer Wert berechnet, den TM
[u] mindestens haben muss. Da {E2 } 6⊇ {M }, erhält
]
also TM [u] als neuen Wert

αM ({E2 } ∪ {M }) = Mt | 0 ≤ t ≤ 1

für


1 0
Mt :=
t 1
und die Workset enthält wiederum die zweite Ungleichung. Im dritten Schritt wird
entsprechend zunächst
{M } ◦ {Mt | 0 ≤ t ≤ 1} = {Mt | 1 ≤ t ≤ 2}
berechnet. Die zweiten Ungleichung ist also weiterhin unerfüllt und es wird
]
TM
[u] = αM ({Mt | 0 ≤ t ≤ 1} ∪ {M } ◦ {Mt | 0 ≤ t ≤ 1}) = {Mt | 0 ≤ t ≤ 2}

gesetzt. Analog erhält man im n-ten Schritt der Berechnung
]
TM
[u] = {Mt | 0 ≤ t ≤ n − 1}.

Die zweite Ungleichung ist wiederum nicht erfüllt. Also terminiert die Berechnung
nicht.

Wir haben in diesem Kapitel eingeführt, wie wir die in Kapitel 3 eingeführten Ansätze
zur Analyse interprozeduraler Programme abstrakt interpretieren. Diese abstrakte
Interpretation hängt allein von einer zuvor festgelegten abstrakten Interpretation
der Transferfunktionen des monotonen Frameworks ab. Wir haben gezeigt, dass die
abstrakte Interpretation korrekt, präzise bzw. kanonisch ist, wenn die abstrakte Interpretation der Transferfunktionen die entsprechende Eigenschaft hat. Weiter haben
wir gesehen, dass die kanonische Interpretation von allen korrekten die bestmögliche
Lösung liefert. Falls die zugrundeliegende Galois-Verbindung präzise abstrakte Interpretationen zulässt, so ist die kanonische abstrakte Interpretation sogar präzise. Die
bestmögliche abstrakte Interpretation erhält man also im funktionalen wie auch im
Call-String-Ansatz durch die kanonische abstrakte Interpretation der Transferfunktionen. Außerdem haben wir gesehen, dass die beiden Ansätze der Polyederanalyse
verschiedene Ergebnisse liefern: Der Ansatz mit Matritzenmengen liefert präzise

98

4 Abstrakte Interpretation

Werte, während der Ansatz mit Relationen zwar korrekte, aber nicht unbedingt
präzise Werte berechnet.
Zudem haben wir gesehen, dass das Abstrahieren von Ungleichungssystemen keine
Terminierung garantiert. Ein weiteres Mittel, das Terminierung erreichen kann, ist
die Verwendung eines sogenannten Widening-Operators im Workset-Algorithmus.
Dieses werden wir im kommenden Kapitel untersuchen.

5 Widening
In Kapitel 3 haben wir zwei verschiedene Ansätze zur Analyse interprozeduraler
Programme vorgestellt und im Hinblick auf ihre Präzision ihrer Ergebnisse verglichen. Eine solches Ergebnis kann mithilfe eines sogenannnten Workset-Algorithmus
bestimmt werden, der aber nicht terminieren muss.
Ein von Cousot und Cousot in [CC76] vorgestellter Ansatz, um Terminierung des
Workset-Algorithmus zu erreichen, ist die Verwendung eines Widening-Operators im
Workset-Algorithmus. In diesem Kapitel werden wir zunächst Widening-Operatoren
allgemein vorstellen. Weiter werden wir feststellen, dass durch die Verwendung eines
Widening-Operators im Workset-Algorithmus keine eindeutige Lösung berechnet wird
und dass - im Gegensatz zu Analysen mit nur einer Prozedur - noch immer keine
Terminierung garantiert werden kann. Zuletzt werden wir sehen, dass die Lösungen,
die der Workset-Algorithmus mit Widening-Operatoren für den funktionalen und
den Call-String-Ansatz berechnet, im Allgemeinen unvergleichbar sind.

5.1 Workset-Algorithmus mit Widening
In Abschnitt 3.5 haben wir gesehen, dass ein Workset-Algorithmus schon für ein
endliches Ungleichungssystem nicht terminieren muss, wenn der zugrundeliegende
vollständige Verband unendliche echt aufsteigende Ketten enthält: Die Werte, die
der Algorithmus für eine Variable berechnet, bilden eine aufsteigende Kette. Die
Berechnung eines Wertes für die Variable terminiert also nur, wenn die Folge, die
aus dieser Kette besteht, stabil wird. Enthält der Verband aber unendliche echt
aufsteigende Ketten, so ist dies nicht gewährleistet. Um dem Abhilfe zu schaffen,
wird bei der Berechnung eines neuen Wertes nicht mehr die kleinste obere Schranke
der eingehenden Werte bestimmt, sondern ein Widening-Operator verwendet.
Definition 5.1. Eine Abbildung O : L × L → L heißt Extrapolationsoperator , falls
xOy w x t y
für alle x, y ∈ L gilt.

100

5 Widening

Ein Extrapolationsoperator heißt Widening-Operator , falls für jede Folge (xn )n∈N in
L die Folge (ln )n∈N mit l0 := x0 und ln+1 := ln Oxn+1 stabil wird, d.h. es ein N ∈ N
gibt, so dass lN +i = lN für jedes i ≥ 0 gilt.
Verwendet man nun anstelle der kleinsten oberen Schranke bei der Berechnung der
neuen Werte im Workset-Algorithmus einen Extrapolationsoperator, so ist eine so
berechnete Lösung noch immer korrekt. Dies sieht man analog zum Beweis von Lemma
2.27, in dem gezeigt wurde, dass der Worklist-Algorithmus, sofern er terminiert, die
kleinste Lösung des betrachteten Ungleichungssystems liefert. Betrachten wir dazu
eine feste Variable. Mit xn bezeichnen wir den n-ten Wert, der für diese Variable
berechnet wird. Das im n-ten Schritt berechnete t“ bezeichnen wir mit ln . Dann
”
entstehen die ln aus den xn durch ln+1 := ln t xn+1 . Verwendet man anstelle von t
einen Widening-Operator O, so wird die Folge (ln )n∈N stabil. Die Berechnung eines
Wertes für diese Variable terminiert also.
Bemerkung 5.2. Ist (L, v) ein vollständiger Verband ohne unendliche echt aufsteigende Ketten und O : L × L → L ein Extrapolationsoperator, so ist O bereits ein
Widening-Operator. Dies folgt direkt daraus, dass die Folge (ln )n≥0 aus der Definition
von Widening-Operatoren eine Kette bildet.
Insbesondere ist also auf endlichen vollständigen Verbänden jeder Extrapolationsoperator bereits ein Widening-Operator.

Wir betrachten nun ein Beispiel für einen Widening-Operator für die Intervallanalyse. Der Widening-Operator wurde ebenfalls von Cousot und Cousot in [CC76]
eingeführt.
Beispiel 5.3. Definiere O : LInt × LInt → LInt durch [l1 , u1 ]O[l2 , u2 ] = [l, u] mit
(
(
l1
falls l1 ≤ l2
u1
falls u1 ≥ u2
l :=
und
u :=
−∞ sonst
+∞ sonst.
sowie
∅OI := I
und
IO∅ := I
für jedes I ∈ LInt . Ist die untere Grenze des ersten Intervalles im zweiten enthalten, so
bildet dies auch die unteren Grenzen des neuen Intervalles. Ansonsten wird die Grenze
auf −∞ gesetzt. Entsprechend ist die neue obere Grenze die des ersten Intervalles
oder +∞. Dies ist ein Widening-Operator:

5.1 Workset-Algorithmus mit Widening

101

Seien [l1 , u1 ] und [l2 , u2 ] beliebige Intervalle und [l, u] = [l1 , u1 ]O[l2 , u2 ]. Falls l1 ≤ l2 ,
so ist l = l1 ≤ l2 . Andernfalls ist l = −∞ ≤ l2 ≤ l1 . In beiden Fällen erhalten wir also
l1 , l2 ≥ l. Ebenso zeigt man u1 , u2 ≤ u. Zusammen folgt [li , ui ] ⊆ [l, u] für i = 1, 2.
Damit ist O ein Extrapolationsoperator.
0
Sei nun (In )n∈N eine Folge in LInt . Definiere I00 := I0 und In+1
:= In0 OIn+1 . Da O ein
Extrapolationsoperator ist, ist die Folge (In0 )n∈N aufsteigend. Angenommen, diese
Folge wird nicht stabil. Dann gibt es eine echt aufsteigende Teilfolge, die wir wieder
mit (In0 )n∈N bezeichnen. Schreibe In = [ln , un ] und In0 = [ln0 , u0n ].

Angenommen, die Folge (ln0 )n≥0 ist nicht konstant. Dann gibt es einen Index m ≥ 0
0
0
0
mit lm+1
@ lm
. Nach Konstruktion ist dann lm+1
= −∞. Insbesondere ist ln0 = −∞
für alle n ≥ m + 1. Also muss (u0n )n≥m+1 echt aufsteigend sein. Insbesondere ist
u0m+2 A u0m+1 und nach Konstruktion wiederum u0n = +∞ für alle n ≥ m + 2.
Also ist die Folge (In0 )n≥m+2 konstant. Dies ist ein Widerspruch. Also muss (ln0 )n≥0
konstant sein. Es gilt demnach ln0 = l0 für alle n ≥ 0. Analog zeigt man u0n = u0
für alle n ≥ 0. Damit ist (In0 )n∈N konstant. Dies ist ein Widerspruch. Also ist O ein
Widening-Operator.

Wir geben nun einen Workset-Algorithmus an, der Widening benutzt. Zusätzlich
fordern wir, dass die Strategie, nach der Ungleichungen aus der Workset ausgewählt
werden, in einem gewissen Sinne fair ist: Für jede Ungleichung und jeden Zeitpunkt
t soll gelten, dass, wenn sich die Ungleichung zum Zeitpunkt t in der Workset
befindet, sie zu einem späteren Zeitpunkt betrachtet wird. Dies garantiert, dass
keine Ungleichung gewissermaßen verhungert“, sondern alle Ungleichungen immer
”
wieder betrachtet werden. Diesen Algorithmus nennen wir Workset-Algorithmus mit
”
Widening und Fairness“.
W := U ;
f o r a l l ( i∈I ) {xi :=⊥; }
w h i l e W 6= () {
choose u =(xj wf ( x ) ) fairly from W ; W := W\{u};
t := f ( x ) ;
i f ¬( t v xj ) {
// compute new value using O
xj := xj O t ;
f o r a l l ((xk wg ( x ) ) ∈ U : g uses xj ) {W := W :(xk wg ( x ) ) ;}
}
}
Lemma 5.4. Für jede Variable garantiert der Workset-Algorithmus mit Widening
und Fairness Terminierung.

102

5 Widening

Beweis. Sei i ∈ I ein beliebiger Index. Wir zeigen nun, dass für die Variable xi in
endlicher Zeit ein Wert berechnet wird.
Wie bei der Betrachtung des Workset-Algorithmus ohne Widening in Abschnitt 2.4
(n)
(n)
(m)
betrachten wir die Folgen (xi )n∈N . Es gilt wieder xi v xi für n ≤ m. Wir konstruieren daraus eine echt aufsteigende Teilfolge, indem wir alle diejenigen Folgenglieder
weglassen, die mit dem vorherigen übereinstimmen:
(n0 )

:= xi

(nk+1 )

:= xi

xi
xi

(0)
(j)

(l)

(nk )

mit j = min{l | xi A xi

}

Nach dem nk -ten Schritt ist also der j-te Schritt der nächste, in dem der Wert der
Variablen xi verändert wird. Dieser Index existiert, da die Ungleichungen fair aus
der Workset herausgenommen werden. Also wird jede Ungleichung, auf deren linker
Seite die Variable xi steht und die in der Workset enthalten ist, irgendwann nach
(j−1)
(n )
dem nk -ten Schritt wieder betrachtet. Insbesondere gilt also xi
= xi k .
(j)

Nach Konstruktion entsteht xi aus x(j−1) durch Betrachten einer unerfüllten Ungleichung xi v f (x). Damit ist dann
(nk+1 )

xi

(j)

(j−1)

= xi = xi

Of (x(j−1) ).

Nach Definition eines Widening-Operators wird diese Teilfolge ab einem Index mi
(n)
stabil. Damit wird aber auch (xi ) ab mi stabil.
Korollar 5.5. Wenn das betrachtete Ungleichungssystem endlich ist, garantiert der
Workset-Algorithmus mit Widening und Fairness Terminierung.
(n)

Beweis. Wie in Lemma 5.4 betrachten wir die Folgen (xi )n∈N der für eine Variable
xi durch den Workset-Algorithmus mit Widening und Fairness berechnete Werte.
Wir haben im Beweis von Lemma 5.4 gezeigt, dass ein endlicher Indes mi existiert,
ab dem diese Folge stabil wird.
Dies gilt für jedes i ∈ I. Also wird (x(n) ) stabil ab m := max{mi | i ∈ I}. Ab dem
Index m ist dann jede Ungleichung erfüllt. Wie für den Workset-Algorithmus ohne
Widening gilt, dass jede nichterfüllte Ungleichung auf der Workset enthalten ist. Wir
zeigen nun W (n+1) = tail(W (n) ) für alle n ≥ m, für die die Workset nicht leer ist.
Sei also u ∈ W (n) von der Gestalt xj w f (x). Wäre u nicht erfüllt, so würde als neuer
Wert
(n+1)

xj

(n)

= xj Of (x(n) )
(n)

berechnet. Da (xj ) ab m stabil ist, gilt aber auch
(n+1)

xj

(n)

= xj .

5.1 Workset-Algorithmus mit Widening
(n)

Aus xj

(n)

= xj Of (x(n) ) folgt aber

(n)

xj

103

w f (x(n) )

und dies ist ein Widerspruch. Also ist u erfüllt und die neue Workset entsteht aus der
alten durch Herausnehmen von u. Nach m Schritten ist also (x(n) ) stabil und nach
weitern |W (m) | Schritten die Workset leer. Somit terminiert der Algorithmus.
Diese Lösung muss aber nicht minimal sein, wie das folgende Beispiel zeigt.
Beispiel 5.6. Wir betrachten wiederum eine Intervallanalyse. Das Ungleichungssystem sei
x w [0, 1]
x w [0, 2].
Zunächst wird x mit ∅ und W mit {(x w [0, 1]), (x w [0, 2])} initialisiert. Nun wird
die erste Ungleichung betrachtet. Da ∅ 6w [0, 1], wird nun x := ∅O[0, 1] = [0, 1] gesetzt.
W wird um die erste Ungleichung verringert.
Auch die zweite Ungleichung ist nicht erfüllt und x erhält den neuen Wert
x = [0, 1]O[0, 2] = [0, ∞].
Nun ist W leer und der Algorithmus terminiert mit x = [0, ∞]. Die kleinste Lösung
des Ungleichungssystems ist dagegen
x = [0, 1] t [0, 2] = [0, 2].
Also ist der für x berechnete Wert nicht minimal.



Ist dagegen I nicht endlich, so terminiert der Algorithmus nicht. Allerdings werden
für jede Variable nur endlich viele Schritte benötigt, bis für sie ein endgültiger
Wert berechnet ist. Die Fairness garantiert nun, dass die Ungleichungen, durch die
diese Variable verändert wird, oft genug betrachtet werden. So kann zwar nicht in
endlicher Zeit eine Lösung für alle Variablen berechnet werden, aber für jede einzelne
Variable liefert der Algorithmus nach endlicher Zeit einen richtigen Wert. Somit
kann der Workset-Algorithmus mit Widening zwar nicht unbedingt zum Lösen von
unendlichen Ungleichungssystemen benutzt werden, wir werden ihn aber dennoch
in den folgenden Abschnitten als Referenzpunkt zum Vergleichen verschiedener
Analyseansätze benutzen. Zunächst werden wir uns jedoch einige Eigenschaften von
Widening-Operatoren genauer ansehen.

104

5 Widening

5.2 Nicht-Monotonie
In Abschnitt 3.3 haben wir zum Vergleich der kleinsten Fixpunkte der Ungleichungssysteme wesentlich die Monotonie der verwendeten Abbildungen und sogar geeignete
Distributivitätseigenschaften benutzt. Dies ist hier nicht möglich: Wie wir im Folgenden zeigen werden, ist ein Widening-Operator im Allgemeinen nicht monoton
und damit auch nicht distributiv. Wir werden nun an die Definition von Monotonie
erinnern und anschließend monotone Widening-Operatoren untersuchen.
Definition 5.7. Sei (L, v) ein vollständiger Verband und O : L × L → L ein
Extrapolationsoperator. Dieser heißt monoton, falls xOy v x0 Oy 0 für alle x v x0 und
y v y 0 gilt. Weiter heißt O idempotent, falls xOx = x für jedes x ∈ L gilt.
Beispiel 5.8. Wir betrachten erneut den Widening-Operator O des Intervallverbandes. Dieser Widening-Operator ist nach Konstruktion idempontent. Aber er ist nicht
monoton: Es ist [0, 1] v [0, 2], aber [0, 1]O[0, 2] = [0, ∞] 6v [0, 2] = [0, 2]O[0, 2].

Satz 5.9. Sei (L, v) ein vollständiger Verband und O : L × L → L ein idempotenter
und monotoner Extrapolationsoperator. Dann gilt bereits O = t.
Beweis. Seien x, y ∈ L beliebig. Dann gilt mit der Monotonie und der Idempotenz
von O und zuletzt mit der Tatsache, dass O ein Extrapolationsoperator ist
xOy v (x t y)O(x t y) = x t y v xOy.
Somit gilt in obigen Ungleichungen bereits Gleichheit. Es folgt die Behauptung.
Im Workset-Algorithmus wird der Widening-Operator innerhalb einer Fallunterscheidung benutzt. Diese können wir durch eine Abbildung Oidp kodieren. Sie ist
idempotent, wie der folgendende Satz zeigt. Wir sagen auch, der Widening-Operator
werde in idempotenter Weise verwendet“.
”
Satz 5.10. Sei (L, v) ein vollständiger Verband und O : L × L → L ein Extrapolationsoperator. Definiere Oidp : L × L → L durch
(
x
falls y v x
xOidp y =
xOy sonst
für x, y ∈ L. Dann ist Oidp idempotent.
Beweis. Dies gilt offenbar nach Definition.
Wir können den Workset-Algorithmus nun äquivalent schreiben als

5.2 Nicht-Monotonie

105

W := U ;
f o r a l l ( i∈I ) {xi :=⊥; }
w h i l e W 6= () {
choose u =(xj wf ( x ) ) fairly from W ; W := W\{u};
t := f ( x ) ;
i f ¬( t v xj ) {
xj := xj Oidp t ;
f o r a l l ((xk wg ( x ) ) ∈ U : g uses xj ) {W := W :(xk wg ( x ) ) ;}
}
}
Der Widening-Operator wird also in idempotenter Weise verwendet. In einer Situation,
in der das Bilden der kleinsten oberen Schranke durch t keine Terminierung garantiert,
kann die Verwendung eines Widening-Operators also nicht monoton sein. Da es in
anderen Situationen unnötig ist, einen Widening-Operator zu verwenden, gehen wir
im Folgenden von einer nicht-monotonen Verwendung von Widening-Operatoren
aus.
Dadurch entstehen weitere Probleme. Sind die verwendeten Abbildungen alle monoton,
so liefert der normale“ Workset-Algorithmus eine eindeutige Lösung. Wird dagegen
”
ein Widening-Operator im Workset-Algorithmus verwendet, so ist dies nicht mehr
der Fall:
Beispiel 5.11. Wir betrachten das Programm aus Abbildung 5.1 und machen wieder
eine Intervallanalyse.
Es ist Var = {x} und N = {s, u, v1 , v2 , r}. Für eine natürliche Zahl n ordnen wir der
Zuweisung x:=n die Transferfunktion fx:=n : LIA → LIA mit fx:=n (ρ)(x) = [n, n] zu.
Nach Ausführen der Zuweisung hat die Variable x also genau den ihr soeben zugewiesenen Wert. Die Basisanweisung skip besagt, dass die Variablenwerte unverändert
bleiben. Dazu korrespondiert die Identität id : LIA → LIA als Transferfunktion. Da
zu Beginn der Ausführung noch nichts über den Wert von x bekannt ist, ordnen wir
jeder Variable im Startpunkt als Initialwert das größtmögliche Intervall zu. Dieses ist
[−∞, +∞]. Wir erhalten damit als Ungleichungssystem U
I[s](x) ⊇ [−∞, +∞]
I[u](x) ⊇ fx:=0 (I[s]) = [0, 0]
I[v1 ](x) ⊇ fx:=17 (I[u]) = [17, 17]
I[v2 ](x) ⊇ fx:=42 (I[u]) = [42, 42]
I[r](x) ⊇ fskip (I[v1 ]) = I[v1 ]
I[r](x) ⊇ fskip (I[v2 ]) = I[v2 ]
Als Widening-Operator betrachten wir wieder den Operator aus Beispiel 5.3.

(u1 )
(u2 )
(u3 )
(u4 )
(u5 )
(u6 )

106

5 Widening

s
x:=0
u
x:=17

x:=42

v1

v2

skip

skip
r

Abbildung 5.1: Flussgraph zu S = x:=0;(x:=17|x:=42).
Wir berechnen nun eine Lösung des Ungleichungssystems U, indem wir einen WorksetAlgorithmus mithilfe des Widening-Operators O ausführen. Dazu initialisieren wir die
Workset W mit dem Ungleichungssystem und die Variablen in jedem Programmpunkt
mit dem minimalen Element ∅ von LInt . Es gilt also W = U und I[ν](x) = ∅ für alle
ν ∈ N.
Wir betrachten nun zunächst die ersten vier Ungleichungen. Zu Ungleichung (u1 )
setzen wir zunächst t := [−∞, +∞]. Es ist nun ∅ 6⊇ [−∞, +∞] und die Ungleichung ist
nicht erfüllt. Wir berechnen also als neuen Wert I[s](x) = ∅O[−∞, +∞] = [−∞, +∞]
und erhalten
(
[−∞, +∞] für ν = s
W = {u2 , . . . , u6 } und I[ν](x) =
∅
sonst.
Ebenso ist Ungleichung (u2 ) nicht erfüllt. Somit berechnen wir im Programmpunkt u
als neuen Wert I[u](x) = ∅O[0, 0] = [0, 0] und erhalten


[−∞, +∞] für ν = s
W = {u3 , . . . , u6 } und I[ν](x) = [0, 0]
für ν = u


∅
sonst.

5.2 Nicht-Monotonie

107

Die Ungleichungen (u3 ) und (u4 ) sind ebenfalls nicht erfüllt. Mit analogen Rechnungen
wie in den ersten beiden Schritten erhalten wir zunächst

[−∞, +∞]



[0, 0]
W = {u4 , u5 , u6 } und I[ν](x) =

[17, 17]



∅

für ν = s
für ν = u
für ν = v1
sonst

und dann


[−∞, +∞]





[0, 0]
W = {u5 , u6 } und I[ν](x) = [17, 17]



[42, 42]



∅

für
für
für
für
für

ν
ν
ν
ν
ν

=s
=u
= v1
= v2
= r.

Die nächsten beiden Ungleichungen betrachten wir nun in verschiedenen Reihenfolgen.
Zunächst beginnen wir mit Ungleichung (u5 ). Auch diese ist nicht erfüllt und wir
erhalten analog zu oben


[−∞, +∞]




[0, 0]

W = {u6 } und I[ν](x) = [17, 17]


[42, 42]



[17, 17]

für
für
für
für
für

ν
ν
ν
ν
ν

=s
=u
= v1
= v2
= r.

Auch die letzte Ungleichung ist nicht erfüllt und wir berechnen
I[r](x) = [17, 17]O[42, 42] = [17, ∞].
Damit erhalten wir


[−∞, +∞]





[0, 0]
W = ∅ und I[ν](x) = [17, 17]



[42, 42]



[17, ∞]

für
für
für
für
für

ν
ν
ν
ν
ν

=s
=u
= v1
= v2
= r.

108

5 Widening

Falls wir umgekehrt zunächst (u6 ) betrachten, erhalten wir


[−∞, +∞]





[0, 0]
W = {u5 } und I[ν](x) = [17, 17]



[42, 42]



[42, 42]

für
für
für
für
für

ν
ν
ν
ν
ν

=s
=u
= v1
= v2
= r.

ν
ν
ν
ν
ν

=s
=u
= v1
= v2
= r.

und nach Betrachtung von Ungleichung (u5 ) schließlich


[−∞, +∞]





[0, 0]
W = ∅ und I[ν](x) = [17, 17]



[42, 42]



[−∞, 42]

für
für
für
für
für

Die berechneten Werte im Programmpunkt r unterscheiden sich also und sind sogar
unvergleichbar. Somit hängt das Ergebnis des Workset-Algorithmus von der Strategie
ab, nach der die Ungleichungen der Workset betrachtet werden.

Dieses Problem kann dadurch gelöst werden, dass man anstatt einer Lösung die
gesamte Lösungsmenge berechnet und anschließend die Lösungsmengen der Ungleichungssysteme des funktionalen und des Call-String-Ansatzes vergleicht. Mögliche
Ergebnisse dabei könnten sein, dass die eine Menge die andere enthält oder dass zu
jedem Element der einen Menge ein kleineres in der anderen existiert.

5.3 Nicht-Terminierung
In Abschnitt 5.2 haben wir festgestellt, dass Widening-Operatoren im Workset-Algorithmus im Allgemeinen in einer nicht-monotonen Weise verwendet werden. Dies
führte dazu, dass die berechnete Lösung nicht eindeutig sein muss. Deshalb wollen
wir die Mengen solcher Lösungen betrachten. Beim Berechnen dieser Lösungsmengen
gibt es aber weitere Probleme, die wir im Folgenden untersuchen werden.
Wie in Abschnitt 2.4 bereits gesehen, terminiert der Workset-Algorithmus nicht,
wenn das betrachtete Ungleichungssystem unendlich viele Ungleichungen enthält. Im
Allgemeinen werden für ein Programm unendlich viele Call-Strings berechnet. Das
Ungleichungssystem (3.4) aus dem funktionalen Ansatz enthält dann unendlich viele
Ungleichungen und kann mit einem Workset-Algorithmus nicht gelöst werden.

5.3 Nicht-Terminierung

109

In Lemma 5.4 haben wir aber gesehen, dass für jede Variable in endlicher Zeit ein Wert
berechnet wird, wenn wir im Workset-Algorithmus einen Widening-Operator und
Fairness benutzen. Somit kann zwar in endlicher Zeit keine Lösung mehr berechnet
werden, aber aus theoretischer Sicht ist dennoch vertretbar, auch für Call-String
einen Workset-Algorithmus mit Widening und Fairness zu benutzten, wenn dieser
als Referenzpunkt zum Vergleich der Lösungen des funktionalen und des Call-StringAnsatzes benutzt werden soll.
Auch die Ungleichungssysteme, die Transferfunktionen als Summary-Informationen
berechnen bzw. benutzen, sind nicht direkt lösbar. Um deren Lösung sinnvoll mit der
des Ungleichungssystems aus dem Call-String-Ansatz vergleichen zu können, muss in
beiden Fällen derselbe Widening-Operator im Workset-Algorithmus benutzt werden.
Dazu wählt man zunächst einen Widening-Operator O : L × L → L, um mit diesem
die beiden Ungleichungssysteme (3.2) und (3.4) zu lösen, welche die eigentlichen
Informationen berechnen. Zunächst muss jedoch das Ungleichungssystem (3.1) zur
Berechnung der Summary-Informationen gelöst werden. Dieses benötigt nun einen
Widening-Operator O∗ : (L → L) × (L → L) → (L → L). Der kanonische Lift von O
zu einem Operator auf (L → L) ist aber im Allgemeinen kein Widening-Operator,
wie das folgende Lemma zeigt.
Lemma 5.12. Sei O : L × L → L ein Widening-Operator und
O∗ : (L → L) × (L → L) → (L → L)
mit
(f O∗ g)(l) := f (l)Og(l)
der natürliche Lift von O auf (L → L). Dann ist O∗ ein Extrapolationsoperator.
Außerdem ist O∗ genau dann ein Widening-Operator, wenn für jede Folge (fn )n∈N
gilt:
m0 := sup{ml | l ∈ L} < ∞.
Dabei sei
(
f1
hn :=
hn−1 O∗ fn

n=1
sonst

und ml := min{n ∈ N | ∀i ≥ 0 : hn+i (l) = hn (l)}.
Beweis. Offenbar ist für jedes x ∈ L
f (x) v f (x)Og(x) = (f O∗ g)(x).

110

5 Widening

Ebenso ist g(x) v (f O∗ g)(x) für jedes x ∈ L. Also ist O∗ ein Extrapolationsoperator.
Sei nun (fn )n∈N beliebige Folge in (L → L) und (hn )n∈N wie oben definiert. Der
geliftete Operator O∗ ist also ein Widening-Operator, wenn (hn )n∈N irgendwann stabil
wird. Dies wiederum ist genau dann der Fall, wenn
mh := inf{m ∈ N | ∀i ≥ 0 : hm+i = hm } < ∞.
Ist mh unendlich, so wird die Folge nicht stabil. Andernfalls ist mh der Index, ab
dem (hn )n∈N stabil ist.
Nach Definition ist
hn+1 (l) = hn (l)Ofn+1 (l).
Da O ein Widening-Operator ist, wird die so definierte Folge stabil. Also existiert
ml = min{n ∈ N | ∀i ≥ 0 : hn+i (l) = hn (l)}
und ml ist der Index, ab dem die Folge (hn (l))l∈L stabil wird. Die Idee ist nun, dass
die Folge (hn )n∈N stabil wird, wenn (hn (l))n∈N für jedes l ∈ L stabil ist. Letzteres ist
der Fall, wenn m0 = sup{ml | l ∈ L} endlich ist, ersteres, wenn mh endlich ist. Dies
motiviert die Äquivalenz. Diese zeigen wir nun formal, in dem wir sogar mh = m0
zeigen.
Nach Definition von m0 gilt ml ≤ m0 für jedes l ∈ L. Es gilt also
hm0 +i (l) = hm0 (l)
für alle l ∈ L und i ≥ 0. Es folgt m0 ≥ mh .
Andererseits gilt auch ml ≤ mh für alle l ∈ L. Also ist mh eine obere Schranke der
Menge {ml | l ∈ L} und es folgt m0 ≤ mh .

Ist der geliftete Operator O∗ kein Widening-Operator, so muss ein von O unabhängiger
Operator O∗ gewählt werden, um das Ungleichungssystem zu lösen. Dann ist aber
im Allgemeinen nicht zu erwarten, die Lösungsmengen vom funktionalen und vom
Call-String-Ansatz vergleichen zu können. Alternativ könnte zum Lösen dieses Ungleichungssystems kein Widening-Operator verwendet werden. In dem Fall muss
allerdings im Allgemeinen auch auf Terminierung verzichtet werden.

5.4 Nicht-Koinzidenz

111

5.4 Nicht-Koinzidenz
In Kapitel 3 haben wir zwei Ansätze zur Analyse interprozeduraler Programme vorgestellt und gezeigt, dass diese die gleiche Lösung liefern, wenn die verwendeten Abbildungen gewissen Distributivitätseigenschaften genügen. Nun wäre wünschenswert, ein
entsprechendes Resultat zu haben, wenn die Ungleichungssysteme mit einem WorksetAlgorithmus mit Widening gelöst werden. Zur Herleitung des Koinzidenzresultates in
Kapitel 3 haben wir wesentlich die Monotonie der verwendeten Abbildungen benutzt.
Dies geht nun nicht mehr, da ein Widening-Operator nicht monoton sein muss. So
könnte beispielsweise im Rahmen der Intervallanalyse für einen dieser beiden Ansätze
[0, 1]O[0, 2] = [0, ∞] berechnet werden. Der andere Ansatz berechnet aber eventuell
an einer entsprechenden Stelle den Wert [0, 2]O[0, 2] = [0, 2]. Es ist also nicht möglich,
so zu argumentieren, dass der eine Ansatz für eine Variable eine Kette berechnet, in
der die Werte immer oberhalb der entsprechenden Kette im anderen Ansatz liegen.
Diese Sprünge“ des Widening-Operators lassen also vermuten, dass es vielleicht
”
unmöglich ist, wieder ein Koinzidenztheorem zu gewinnen. Wir werden im Folgenden
zeigen, dass diese Vermutung stimmt. Weiterhin werden wir sehen, dass es auch
unmöglich ist zu zeigen, dass die Lösungsmenge des einen Ansatzes immer in der des
anderen enthalten ist. Dazu geben wir zwei einfache Beispiele an, die gleichzeitig alle
der im Folgenden aufgelisteten Aussagen widerlegen.
Seien LR bzw. LA die Lösungsmengen des funktionalen bzw. des Call-String-Ansatzes,
die vom Workset-Algorithmus mit Widening für ein zugrundeliegendes Framework
(L, v, F), ein Programm G und einen Widening-Operator O berechnet werden.
Koinzidenz:
(A) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
LA = LR .
Inklusion: Die Lösungen des einen Ansatzes enthalten die des anderen.
(B) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
LA ⊇ LR .
(C) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
LR ⊇ LA .

112

5 Widening

Der eine Ansatz liefert nur bessere oder genauso gute Lösungen wie der andere.
(D) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
∀x ∈ LA ∀y ∈ LR : x v y.
(E) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
∀x ∈ LR ∀y ∈ LA : x v y.
Der eine Ansatz liefert eine Lösung, die besser ist oder genauso gut wie alle Lösungen
des anderen.
(F) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
∃x ∈ LA ∀y ∈ LR : x v y.
(G) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
∃x ∈ LR ∀y ∈ LA : x v y.
Für jede Lösung des anderen findet der eine Ansatz eine Lösung, die besser oder
genauso gut ist.
(H) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
∀y ∈ LA ∃x ∈ LR : x v y.
(I) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
∀y ∈ LR ∃x ∈ LA : x v y.
Für jede Lösung des einen Ansatzes gibt es im anderen eine Lösung, so dass die des
ersten besser oder genauso gut ist.
(J) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
∀x ∈ LR ∃y ∈ LA : x v y.

5.4 Nicht-Koinzidenz

113

(K) Für alle monotonen Frameworks (L, v, F), Widening-Operatoren O und Flussgraphsysteme G gilt
∀x ∈ LA ∃y ∈ LR : x v y.
In jedem dieser Fälle wäre der eine“ Ansatz dem anderen“ vorzuziehen.
”
”
Das erste Beispiel zeigt, dass es ein Programm, ein universell-distributives Framework
und einen Widening-Operator gibt, so dass der Call-String Ansatz eine Lösung liefert,
die zu allen Lösungen des funktionalen Ansatzes unvergleichbar ist. Dabei nutzen wir
aus, dass zum Berechnen des Effektes einer Prozedur einmalig entschieden wird, in
welcher Reihenfolge die entsprechenden Ungleichungen gelöst werden. Diese Ungleichungen korrespondieren, bis auf Prozeduraufrufe, mit denen vom Call-String-Ansatz.
Gibt es nun mehrere Prozeduraufrufe, so berechnet der Call-String-Ansatz Informationen für die verschiedenen Kopien. Dabei können die Ausführungsreihenfolgen
unabhängig voneinander gewählt werden. Werden sie in den einzelnen Kopien nun
verschieden gewählt, so kann dies durch die Summary-Information der Prozedur nicht
nachgebildet werden, da diese nur zu einer der möglichen Reihenfolgen korrespondiert.
Beispiel 5.13. Wir betrachten den vollständigen Verband (L, v), der durch das
Hasse-Diagramm in Abbildung 5.2 gegeben ist.
>

L=
l7

l8
l6

l4

l5
l3
l2
l1
⊥

Abbildung 5.2: Hasse-Diagramm des zugrundeliegenden Verbandes in Beispiel 5.13.

114

5 Widening

Definiere nun f, g : L → L durch

⊥



l
1
f (l) =

l4



>

falls l = ⊥
falls l = l1
falls l = l2 , l3
sonst

bzw.



⊥





l2
g(l) = l3



l5



>

falls l = ⊥
falls l = l1
falls l = l2
falls l = l3
sonst.

Diese Abbildungen sind offenbar universell-distributiv. Mit F bezeichnen wir das
kleinste unter Komposition abschlossene System von Abbildungen, das idL , f und g
enthält. Da die Komposition universell-distributiver Abbildungen wieder universelldistributiv ist, ist (L, v, F) ein universell-distributives monotones Framework.
Zuletzt definiere O : L × L → L durch


l3
falls (x, y) = (l1 , l2 )




l7
falls (x, y) = (l3 , l4 )

xOy = l7
falls (x, y) = (l4 , l5 )



l8
falls (x, y) = (l5 , l4 )



x t y sonst.
Dies ist offenbar ein Extrapolationsoperator. Da L endlich ist, ist O sogar ein WideningOperator. Außerdem ist xOy = x für y v x erfüllt. Also stimmt O mit seiner
idempotenten Variante Oidp überein. Außerdem ist nach Lemma 5.12 der Lift O∗ von
O auf (L → L) wieder ein Widening-Operator.
Sei nun Var = {x} und das Programm gegeben als das Flussgraphsystem aus
Abbildung 5.3.
Wir stellen die zugehörigen Ungleichungssysteme auf, die den Wert von x in den
Programmpunkten bestimmen. Dabei sei init = l1 . Weiter setzen wir e1 := (s, p(), u)
und e2 := (u, p(), r). Das Ungleichungssystem zur Berechnung der Call-Strings hat
folgende Gestalt:
CS[main] ⊇ {ε}
CS[p] ⊇ {e1 }
CS[p] ⊇ {e2 }
Dies hat als Lösung
CS[main] ⊇ {ε} und CS[p] ⊇ {e1 , e2 }.

5.4 Nicht-Koinzidenz

115

main:

p:

s

sp
p()

x := f(x)

x := g(x)
rp

u
p()
r

Abbildung 5.3: Flussgraphsystem in Beispiel 5.13.
Das Ungleichungssystem zur Bestimmung des Wertes von x in den Programmpunkten
ist nun
A[s, ε] w init
A[sp , e1 ] w A[s, ε]
A[rp , e1 ] w f (A[sp , e1 ])
A[rp , e1 ] w g(A[sp , e1 ])
A[u, ε] w A[rp , e1 ]
A[sp , e2 ] w A[u, ε]
A[rp , e2 ] w f (A[sp , e2 ])
A[rp , e2 ] w g(A[sp , e2 ])
A[r, ε] w A[rp , e2 ]

(a1)
(a2)
(a3)
(a4)
(a5)
(a6)
(a7)
(a8)
(a9)

Eine mögliche Ausführung des Workset-Algorithmus mit Widening ist die folgende:
• Zunächst wird jeder Programmpunkt mit ⊥ initialisiert. Die Workset ist nun
W = {(a1), . . . , (a9)}.
• Dann wird Ungleichung (a1) betrachtet. Diese ist nicht erfüllt, also wird A[s, ε]
auf den Wert ⊥ t init = l1 gesetzt. Dann ist W = {(a2), . . . , (a9)}.
• Nun ist Ungleichung (a2) unerfüllt. Also wird A[sp , e1 ] auf den Wert ⊥ t l1 = l1
gesetzt. Es ist W = {(a3), . . . , (a9)}.

116

5 Widening

• Als nächstes wird Ungleichung (a3) betrachtet. Also wird A[rp , e1 ] auf den Wert
⊥ t f (l1 ) = l1 gesetzt. Es ist W = {(a4), . . . , (a9)}.
• Ebenso ist Ungleichung (a4) unerfüllt. Also wird für A[rp , e1 ] als neuer Wert
l1 Og(l1 ) = l1 Ol2 = l3 berechnet. Damit ist W = {(a5), . . . , (a9)}.
• Anschließend wird Ungleichung (a5) betrachtet, die nicht erfüllt ist. Dann wird
A[u, ε] auf l3 gesetzt und es ist W = {(a6), . . . , (a9)}.
• Damit ist Ungleichung (a6) unerfüllt und es wird auch A[sp , e2 ] auf l3 gesetzt.
Es ist W = {(a7), (a8), (a9)}.
• Nun sind die Ungleichungen (a7) und (a8) unerfüllt. Wir betrachten diese in
umgekehrter Reihenfolge wie für die erste Kopie und beginnen also mit der
letzteren. Damit erhält A[rp , e2 ] den Wert g(l3 ) = l5 und es ist W = {(a7), (a9)}.
• Danach wird (a7) betrachtet. Auch diese Ungleichung ist nicht erfüllt. Also
wird A[rp , e2 ] zu l5 Of (l3 ) = l5 Ol4 = l8 berechnet und es ist W = {(a9)}.
• Zuletzt wird also (a9) betrachtet. Da diese Ungleichung wiederum nicht erfüllt
ist, wird A[r, ε] auf den Wert l8 gesetzt und die Workset ist leer.
Nun wird die Lösung Â berechnet. Dazu wird für jeden Programmpunkt die kleinste
obere Schranke derjenigen Werte bestimmt, die in den einzelnen Kopien berechnet
wurden. Dann ist Â gegeben durch
Â[s] = l1

Â[sp ] = l1 t l3 = l3

Â[u] = l3

Â[rp ] = l1 t l8 = l8

Â[r] = l8 .

Als nächstes betrachten wir den funktionalen Ansatz. Die beiden Ungleichungssysteme
hierzu sind gegeben durch
T [s] w id
T [u] w T [rp ] ◦ T [s]
T [r] w T [rp ] ◦ T [u]
T [sp ] w id
T [rp ] w f ◦ T [sp ]
T [rp ] w g ◦ T [sp ]

(t1)
(t2)
(t3)
(t4)
(t5)
(t6)

5.4 Nicht-Koinzidenz

117

sowie
R[s] w init
R[u] w T [rp ](R[s])
R[r] w T [rp ](R[u])
R[sp ] w R[s]
R[sp ] w R[u]
R[rp ] w f (R[sp ])
R[rp ] w g(R[sp ]).

(r1)
(r2)
(r3)
(r4)
(r5)
(r6)
(r7)

Wir lösen zuerst das Ungleichungssystem zur Bestimmung der Transferfunktionen.
Da genauer nur der Wert T [rp ] zum Lösen des zweiten Ungleichungssystems relevant
ist, beschränken wir uns darauf, die hier möglichen Werte zu berechnen.
• Zunächst wird jede Variable mit der Abbildung initialisiert, die konstant
den Wert ⊥ liefert. Die Workset enthält alle Ungleichungen, also ist W =
{(t1), . . . , (t6)}.
• Unabhängig von der Ausführungsreihenfolge wird (t4) nur einmal betrachtet:
Da diese Ungleichung zu Beginn nicht erfüllt ist, muss sie mindestens einmal
betrachtet werden. Dabei wird sie aus der Workset herausgenommen. Da die
Ungleichung auf der rechten Seite keine Variable benutzt, wird sie zu keinem
Zeitpunkt erneut der Workset hinzugefügt. Also wird sie genau einmal betrachtet
und erhält den Wert T [sp ] = id.
• Anschließend sind die Ungleichungen (t5) und (t6) nicht erfüllt. Diese werden
ebenfalls genau einmal betrachtet. Im ersten Schritt ist T [rp ] = f oder T [rp ] = g
und es bleibt, die jeweilige andere Ungleichung zu betrachten.
• Somit ist zuletzt T [rp ] ∈ {f O∗ g, gO∗ f }.
Wir wenden uns nun dem Ungleichungssystem zur Bestimmung des Wertes von x
in den Programmpunkten zu. Sei R eine Lösung, die vom Workset-Algorithmus mit
Widening berechnet wurde. Wir zeigen nun, dass R[r] und Â[r] stets unvergleichbar
sind:
Zu Beginn wird wieder jede Variable mit ⊥ und die Workset mit der Menge aller
Ungleichungen initialisiert. Nun ist (r1) die einzige nicht erfüllte Ungleichung und R[s]
enthält den Wert ⊥O init = l1 . Mit derselben Argumentation wie zuvor folgt, dass
diese Ungleichung nie wieder betrachtet wird. Anschließend ist die Ungleichung (r2)
unerfüllt. Also wird R[u] = T [rp ](l1 ) berechnet. Da diese Ungleichung nur die Variable
R[s] benutzt, diese aber nur in Ungleichung (r1) auf der linken Seite vorkommt und
letztere Ungleichung nach voriger Argumentation nie wieder betrachtet wird, wird
auch (r2) nie wieder betrachtet. Ebenso wird (r3) genau einmal betrachtet. Damit

118

5 Widening

ist dann R[r] = T [rp ](T [rp ](l1 )). Wir berechnen nun die möglichen Werte: Falls
T [rp ] = f O∗ g, so ist
R[r] = (f O∗ g)(f (l1 )Og(l1 )) = (f O∗ g)(l1 Ol2 ) = (f O∗ g)(l3 ) = l4 Ol5 = l7 .
Andernfalls ist T [rp ] = gO∗ f . Dann ist
R[r] = (gO∗ f )(g(l1 )Of (l1 )) = (gO∗ f )(l2 Ol1 ) = (gO∗ f )(l2 ) = l3 Ol4 = l7 .
In beiden Fällen ist also R[r] = l7 . Dies ist unvergleichbar zu l8 = Â[r].



In dem Beispiel haben wir benutzt, dass der funktionale Ansatz einmalig den Effekt
einer Prozedur festlegt und mit diesem dann Werte in Knoten der main-Prozedur
berechnet, während im Call-String-Ansatz Werte durch Propagation durch die Knoten
der entsprechenden Prozedur bestimmt werden und dort die Ausführungsreihenfolgen
voneinander verschieden gewählt werden konnten. Somit konnten wir unvergleichbare
Werte im Endknoten der Prozedur main erzeugen.
Das folgende Beispiel zeigt, dass es ein Programm, ein universell-distributives Framework und einen Widening-Operator gibt, so dass der funktionale Ansatz eine
Lösung liefert, die zu allen Lösungen des Call-String-Ansatzes unvergleichbar ist.
Dazu finden wir eine Lösung des funktionalen Ansatzes, die mit keiner Lösung des
Call-String-Ansatzes vergleichbar ist. Konkret werden wir dazu unvergleichbare Werte
im Endknoten einer Prozedur p berechnen. Dazu müssen wir ausnutzen, dass die
Informationen an den Knoten der aufgerufenen Prozedur in beiden Ansätzen auf
verschiedene Weisen berechnet wird: Der Call-String-Ansatz betrachtet für jeden
Aufruf eine eigene Kopie und initialisiert den Startknoten der Prozedur mit dem
jeweiligen Wert des Knotens, von dem aus die Prozedur aufgerufen wird. Im funktionalen Ansatz dagegen gibt es keine verschiedenen Kopien und der Startknoten dieser
Prozedur muss mit den Werten aller aufrufenden Knoten initalisiert werden.
Beispiel 5.14. Wir betrachten den vollständigen Verband (L, v), der durch das
Hasse-Diagramm in Abbildung 5.4 definiert ist.
Definiere weiter fj : L → L durch
(
⊥ falls l = ⊥
fj (l) :=
lj
sonst
für 1 ≤ j ≤ 3. Diese Abbildungen sind offenbar universell-distributiv. Mit F bezeichnen wir das kleinste unter Komposition abschlossene System von Abbildungen, das
idL , h1 , h2 und h3 enthält. Da die Komposition universell-distributiver Abbildungen
wieder universell-distributiv ist, ist (L, v, F) ein universell-distributives monotones
Framework.

5.4 Nicht-Koinzidenz

119
>

L=
l5

l6
l4

l3

l2

l1

⊥
Abbildung 5.4: Hasse-Diagramm des zugrundeliegenden Verbandes in Beispiel 5.14.

Ebenso ist die Abbildung O : L × L → L mit


falls (x, y) ∈ {(l1 , l3 ), (l3 , l1 ), (l2 , l3 ), (l3 , l2 )}
l5
xOy = l6
falls (x, y) ∈ {(l1 , l2 ), (l2 , l1 )}


x t y sonst
offenbar ein Extrapolationsoperator. Da L endlich ist, ist O sogar ein WideningOperator. Weiter ist O symmetrisch und erfüllt xOy = x, falls y v x. Also ist
Oidp = O. Da L endlich ist, ist nach Lemma 5.12 auch der Lift O∗ von O auf (L → L)
ein Widening-Operator.
Sei nun Var = {x}. Wir betrachten das Flussgraphsystem aus Abbildung 5.5.
main:

p:

s

sp

x := f1 (x)

x := f2 (x)
x := x

x := f3 (x)
u

v

rp

p()

p()
r

Abbildung 5.5: Flussgraphsystem in Beispiel 5.14.

120

5 Widening

Wir stellen nun die zugehörigen Ungleichungssysteme auf, die den Wert von x in den
Programmpunkten bestimmen. Dabei sei init = >. Schreibe im Folgenden kurz e1
für (u, p(), r) und e2 für (v, p(), r).
Die Ungleichungssysteme zum funktionalen Ansatz haben die folgende Gestalt:
T [s] w id
T [u] w f1 ◦ T [s]
T [v] w f2 ◦ T [s]
T [r] w T [rq ] ◦ T [u]
T [r] w T [rq ] ◦ T [v]

T [sp ] w id
T [rp ] w f3 (T [sp ])
T [rp ] w T [sp ]

und als Lösung des letzteren Ungleichungssystems wählen wir
R[s] w init
R[u] w f1 (R[s])
R[v] w f2 (R[s])
R[r] w T [rq ](R[u])
R[r] w T [rq ](R[v]).

R[sp ] w R[u]
R[sp ] w R[v]
R[rp ] w f3 (R[sp ])
R[rp ] w R[sp ]

Sei T eine vom Workset-Algorithmus mit Widening berechnete Lösung des ersteren
Ungleichungssystems. Dabei sei
T [rp ] = f3 O∗ id
und
R[s] = init = >
R[u] = l1
R[v] = l2
R[sp ] = l1 Ol2 = l6
R[rp ] = f3 (l6 )Ol6 = l3 Ol6 = l6
R[r] = ((f3 O∗ id)(l1 ))O((f3 O∗ id)(l2 ))) = (l3 Ol1 )O(l3 Ol2 ) = l5 Ol5 = l5 .
Wir müssen nun die Lösungen des entsprechenden Workset-Algorithmus des CallString-Ansatzes betrachten. Das Ungleichungssystem zur Berechnung der Call-Strings
einer Prozedur hat folgende Gestalt:
CS[main] ⊇ {ε}
CS[p] ⊇ {e1 }
CS[p] ⊇ {e2 }.

5.4 Nicht-Koinzidenz

121

Dies hat als Lösung
CS[main] = {ε} und CS[p] = {e1 , e2 }.
Weiter ist
A[s, ε] w init
A[u, ε] w f1 (A[s, ε])
A[v, ε] w f2 (A[s, ε])
A[r, ε] w A[rp , e1 ]
A[r, ε] w A[rp , e2 ]

A[sp , e1 ] w A[u, ε]
A[rp , e1 ] w f3 (A[sp , e1 ])
A[rp , e1 ] w A[sp , e1 ]
A[sp , e2 ] w A[v, ε]
A[rp , e2 ] w f3 (A[sp , e1 ])
A[rp , e2 ] w A[sp , e2 ].

Sei A eine Lösung, die der Workset-Algorithmus mit Widening berechnet hat. Wir
zeigen nun A[rp ](ei ) = l5 für 1 ≤ i ≤ 2. Jede Ausführung des Workset-Algorithmus
liefert zunächst
A[s, ε] = >
A[u, ε] = l1
A[v, ε] = l2
A[sp , e1 ] = l1
A[sp , e2 ] = l2 .
Da O symmetrisch ist, ist irrelevant, in welcher Reihenfolge die Information an den
Endknoten der Prozedur p beim jeweiligen Aufruf propagiert wird. Damit ist
A[rp , e1 ] = f3 (l1 )Ol1 = l3 Ol1 = l5
und
A[rp , e2 ] = f3 (l2 )Ol2 = l3 Ol2 = l5 .
Es folgt Â[rp ] = A[rp , e1 ] t A[rp , e2 ] = l5 t l5 = l5 , was unvergleichbar ist zu l6 = R[rp ].
Also ist R unvergleichbar zu allen möglichen Lösungen Â.

Diese Beispiele sind einfach, da die betrachteten Programme und vollständigen
Verbände sehr klein sind. Umso erstaunlicher ist es, dass die hier nicht zwingend
notwendige Verwendung eines Widening-Operators schon zu Unvergleichbarkeit der
Lösungenmengen des funktionalen bzw. des Call-String-Ansatzes führt. Die angegebenen Programme und universell-distributiven Frameworks können auch auf einfache

122

5 Widening

Weise so abgeändert werden, dass der Workset-Algorithmus ohne Widening nicht
terminiert.
Dazu erweitern wir den Verband um Elemente λn für n ∈ N0 . Dabei ersetzen“
”
wir das Element > durch λ0 und erweitern die Ordnung um λn A λn+1 für jedes
n ∈ N. Wir fügen wiederum > als ein größtes Element hinzu. Wir erweitern die
Variablenmenge um eine frische Variable y und fügen eine Prozedur q hinzu, die aus
den aufeinanderfolgenden Anweisungen y := k(y) und q() besteht. Dabei sei k(l) = ⊥
für Elemente aus dem alten“ Verband und sonst k(λn ) = λn+1 . Außerdem verändern
”
wir die Prozedur main, indem wir an den Knoten r eine mit y := 0 beschriftete Kante
und daran eine mit dem Aufruf q() beschriftete Kante anhängen. Der Knoten, zu
dem diese Kanten führen, ist dann der neue Endknoten der Prozedur main. Den
Widening-Operator setzen wir folgendermaßen fort: Für die Elemente aus dem alten“
”
Verband und λ0 sei der Operator wie zuvor definiert, wobei λ0 die Rolle von >
übernimmt. Sei nun x beliebig und y = λn für ein n > 0 oder y = >. Ist x w y, so
sei xOy = x. Andernfalls sei xOy = >. Dies ist offenbar ein Widening-Operator.
Will man nun zu einem so erweiterten Programm Informationen mit dem WorksetAlgorithmus berechnen, so terminiert die Berechnung für y ohne Widening-Operatoren
nicht. Um eine Lösung zu berechnen, ist also ein Widening-Operator nötig. Damit
wird für y der Wert > berechnet. Für x wird derselbe Wert wir im ursprünglichen
Programm berechnet. Damit erhalten wir eine entsprechende Unvergleichbarkeit also
auch in Situationen, in denen Widening nötig ist.
Insbesondere zeigen diese Beispiele also, dass die zu Beginn des Abschnittes formulierten Aussagen (A) bis (K) in dieser Allgemeinheit falsch sind.

6 Fazit
In dieser Arbeit wurden zwei Ansätze zur Analyse interprozeduraler Programme
vorgestellt, die von Sharir und Pnueli in [SP81] entwickelt wurden: Dies ist zum
einen der funktionale Ansatz, der zunächst für jede Prozedur eine Transferfunktion
als Summary-Information berechnet und damit für jeden Programmknoten eine
Information bestimmt. Zum anderen haben wir den Call-String-Ansatz vorgestellt, der
eine Analyse eines Programms mit nur einer Prozedur simuliert, indem Aufrufkanten
durch die aufgerufenen Prozeduren ersetzt“ und diese verschiedenen Kopien“ der
”
”
Prozeduren durch Call-Strings unterschieden werden.
Dazu haben wir zunächst Ungleichungssysteme definiert und gezeigt, dass deren
Lösungen sich als Präfixpunkte einer geeigneten Abbildung schreiben lassen und die
beste“ Lösung dem kleinsten Fixpunkt dieser Abbildung entspricht. Außerdem haben
”
wir Flussgraphsysteme eingeführt, mit denen wir Programme darstellen, und mit
dem Workset-Algorithmus ein Mittel bereit gestellt, mit dem Ungleichungssysteme
gelöst werden können.
Anschließend haben wir den funktionalen und den Call-String-Ansatz vorgestellt und
gezeigt, dass es sich dabei um korrekte Analysen handelt. Wir haben außerdem gezeigt,
dass die Ansätze präzise Analysen beschreiben, wenn die verwendeten Abbildungen
universell-distributiv oder zumindest positiv-distributiv sind und in letzterem Fall
zusätzlich jeder Programmpunkt erreichbar ist. In diesem Fall liefern beide Ansätze
dasselbe Ergebnis und sind in diesem Sinne gleichwertig. Weiter haben wir mit der
Betrachtung der Polyederanalyse aus [CH78] begonnen, die den funktionalen Ansatz
variiert, indem die Summary-Informationen nicht als Transferfunktionen, sondern in
einer anderen Darstellung berechnet werden. Dabei wurden einerseits Matrizenmengen
wie in [SFP07] und andererseits Relationen wie in [CH78] als Summary-Informationen
benutzt. Diese wiederum haben wir als Transferfunktionen aufgefasst und damit
jeweils ein Ungleichungssystem zur Berechnung die erreichbaren Variablenwerte in
jedem Programmpunkt aufgestellt. Wir haben gezeigt, dass diese beiden Ungleichungssysteme das gleiche Ergebnis liefern und somit gleichwertig sind. Zuletzt haben
wir eine Berechnung eines Ungleichungssystems mithilfe des Workset-Algorithmus
betrachtet und festgestellt, dass diese nicht unbedingt terminieren muss.
Darum haben wir weiter mit der abstrakten Interpretation ein von Cousot und Cousot in [CC76] vorgestelltes Mittel betrachtet, mit dem neue korrekte oder präzise

124

6 Fazit

Analysen konstruiert werden können, bei denen die Berechnung der Lösung durch
den Workset-Algorithmus terminieren kann. Dazu haben wir zunächst allgemein
Galois-Verbindungen und abstrakte Interpretationen von Ungleichungssystemen studiert. Diese haben wir anschließend auf den funktionalen und den Call-String-Ansatz
übertragen, indem wir die in den beiden Ansätzen verwendeten Transferfunktionen
für Basisanweisungen abstrakt interpretiert haben. Wir haben außerdem gezeigt, dass
eine korrekt, präzise oder kanonische abstrakte Interpretation dieser Transferfunktionen eine korrekte, präzise bzw. kanonische abstrakte Interpretation der beiden
Ansätze induziert. Dabei hängt die kanonische abstrakte Interpretation nur von der
zugrundeliegenden Galois-Verbindung ab und ist die präziseste korrekte abstrakte
Interpretation. Außerdem ist sie genau dann präzise, wenn die Galois-Verbindung
präzise abstrakte Interpretationen zulässt. Wir haben gesehen, dass dies nicht immer
der Fall ist. Somit konnten wir abschließend feststellen, dass die kanonische die beste
abstrakte Interpretation ist. Ist sie präzise und gelten die Anforderungen an die
Distributivität der verwendeten Abbildungen wie zuvor, so liefern die kanonischen
abstrakten Interpretationen des funktionalen und des Call-String-Ansatzes dasselbe
Ergebnis und sind wiederum gleichwertig.
Weiter haben wir wieder die Polyederanalyse untersucht. Dabei haben wir zunächst
rückblickend festgestellt, dass das Auffassen einer Matrizenmenge oder einer Relation
als Transferfunktion eine präzise abstrakte Interpretation ist. Außerdem haben wir
die Polyederanalyse weitergeführt, indem wir zusätzlich konvexe Hüllen gebildet
haben, um anstelle der erreichbaren Variablenwerte konvexe Polyeder zu berechnen,
in denen die erreichbaren Variablenwerte enthalten sind. Dabei haben wir gesehen, dass dies eine präzise abstrakte Interpretation ist, wenn Matrizenmengen als
Summary-Informationen verwendet werden, wohingegen die Bildung konvexer Hüllen
bei Relationen als Summary-Informationen zwar eine korrekte, aber nicht unbedingt
präzise abstrakte Interpretation ist. Die Ansätze sind also nicht gleichwertig und
der Ansatz mit Matrizenmengen ist dem mit Relationen vorzuziehen. Zuletzt haben wir gesehen, dass eine solche abstrakte Interpretation noch keine Terminierung
garantieren muss.
Zuletzt haben wir darum ein weiteres Mittel untersucht, das Terminierung des WorksetAlgorithmus erzwingen soll. Dieses Mittel ist die Verwengun der von Cousout und
Cousot in [CC77] eingeführten Widening-Operatoren im Workset-Algorithmus. Dabei
wird Terminierung garantiert, wenn das betrachtete Ungleichungssystem nur endlich
viele Variablen enthält. Werden dagegen unendlich viele Ungleichungen betrachtet, berechnet der Algorithmus unter der zusätzlichen Voraussetzung von Fairness
für jede Variable in endlicher Zeit ein Ergebnis, terminiert aber nicht. Somit kann
der Workset-Algorithmus für den Call-String-Ansatz, der im Allgemeinen unendlich
viele Ungleichungen betrachtet, nicht zum Lösen, sondern nur als Referenzpunkt
betrachtet werden. Außerdem haben wir gesehen, dass der Workset-Algorithmus
mit Widening auch für den funktionalen Ansatz keine Terminierung garantiert, da

125
im Allgemeinen aus einem Widening-Operator für den zugrundeliegenden Verband
kein kanonischer Widening-Operator für die Berechnung der Transferfunktionen
als Summary-Informationen gewonnen werden kann. Außerdem haben wir gezeigt,
dass im Allgemeinen der Widening-Operator im Workset-Algorithmus in einer nichtmonotonen Weise verwendet ist und somit keine eindeutige kleinste Lösung existiert.
Somit mussten anstelle von kleinsten Lösungen die gesamten Lösungsmengen verglichen werden. Wir haben aber gezeigt, dass die Lösungsmengen, die vom WorksetAlgorithmus mit Widening für den funktionalen bzw. den Call-String-Ansatz berechnet
werden, im Allgemeinen nicht vergleichbar sind. Eine Koinzidenzaussage wie zuvor
ist also nicht möglich. Ein Workset-Algorithmus mit Widening kann demnach in
manchen Situationen zwar helfen, ein Ungleichungssystem zu lösen, aber es ist nicht
möglich, Aussagen über die Präzision dieser Lösungen zu treffen.
Es sind mehrere Möglichkeiten denkbar, auf diese Arbeit aufzubauen. Zunächst einmal
könnten weitere Anweisungen wie nicht-deterministische Zuweisungen der Gestalt
x :=? und affine bedingte Verzweigungen wie in [SFP07] betrachtet werden. Es könnte
dann überprüft werden, ob mit diesen zusätzlichen Anweisungen der Ansatz mit
Matrizenmengen wieder das präzisere Ergebnis liefert. Außerdem wird in [SFP07]
ein Widening-Operator vorgestellt, um die berechneten konvexen Matrizenmengen
endlich darstellen zu können. Dieser könnte näher untersucht werden.
Aber auch allgemein wäre eine weitere Untersuchung von Widening-Operatoren
interessant. Die Bedingungen, die in dieser Arbeit an Widening-Operatoren gestellt
wurden, sind für eine Aussage über die Vergleichbarkeit des funktionalen und des
Call-String-Ansatzes zu allgemein. Es könnte also untersucht werden, ob und welche
Eigenschaften von Widening-Operatoren es gibt, die eine solche Vergleichbarkeit
garantieren. Alternativ könnten andere Mittel als der Workset-Algorithmus zur
Berechnung der Lösungen eines Ungleichungssystems untersucht und dabei wiederum
die Ergebnisse des funktionalen und des Call-String-Ansatzes verglichen werden.

Literaturverzeichnis
[CC76]

Patrick Cousot and Radhia Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium
on Programming, pages 106–130. Dunod, Paris, France, 1976.

[CC77]

Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice
model for static analysis of programs by construction or approximation of
fixpoints. In Conference Record of the Fourth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 238–
252, Los Angeles, California, 1977. ACM Press, New York, NY.

[CH78]

Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear
restraints among variables of a program. In Conference Record of the Fifth
Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 84–97, Tucson, Arizona, 1978. ACM Press, New
York, NY.

[LNS82] J.-L. Lassez, V. L. Nguyen, and E. A. Sonenberg. Fixed point theorems
and semantics: A folk tale. Information Processing Letters, 14(3):112–116,
1982.
[NNH99] Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of
Program Analysis. Springer-Verlag New York, Inc., 1999.
[SFP07] Helmut Seidl, Andrea Flexeder, and Michael Petter. Interprocedurally analysing linear inequality relations. In Programming Languages and Systems,
volume Volume 4421/2007 of Lecture Notes in Computer Science, pages
284–299. Springer Berlin / Heidelberg, 2007.
[SP81]

Micha Sharir and Amir Pnueli. Two approaches of interprocedural data
flow analysis. In Steven S. Muchnick and Neil D. Jones, editors, Program
flow analysis: theory and applications, chapter 7, pages 189–233. Prentice
Hall, Englewood Cliffs, New Jersey, 1981.

[WM92] Reinhard Wilhelm and Dieter Maurer. Übersetzerbau - Theorie, Konstruktion, Generierung. Springer, 1992.

Hiermit erkläre ich, dass ich die vorliegende Diplomarbeit selbständig verfasst und
keine anderen als die angegebenen Quellen und Hilfsmittel benutzt sowie alle Stellen,
die wörtlich oder sinngemäß aus Veröffentlichungen entnommen worden sind, als
solche kenntlich gemacht habe.

Münster, im Dezember 2010
Dorothea Jansen

