Programmanalyse und Compileroptimierung

WS 2004/2005 Prof. Dr. Indermark

Mitgeschrieben von Timo Boettcher

Dieses Skript ist meine Mitschrift der Vorlesung Programmanalyse und Compileroptimierung im WS 2004/2005 an der RWTH Aachen (Dozent: Prof. Dr. K. Indermark). Es handelt sich nicht um eine offizielle Veröffentlichung des “Lehrstuhls Informatik II“. Ich übernehme keine Gewähr für die Fehlerfreiheit und Vollständigkeit des Skripts. Korrekturen und Ergänzungen bitte ich an timo_boettcher@post.rwth-aachen.de zu mailen. Timo Boettcher, 2. Februar 2005

Inhaltsverzeichnis

1 Einleitung 5

2 Analyse und Optimierung von Straight-Line Code 7 2.1 AE-Analyse und CS-Elimination . . . . . . . . . . . . . . . . . . 9 2.2 LV-Analyse und DC-Elimination . . . . . . . . . . . . . . . . . . 11 2.3 RD-Analyse und Konstantenfaltung . . . . . . . . . . . . . . . . 12 2.4 DAG-Darstellung von SLC-Programmen . . . . . . . . . . . . . . 13 2.5 Weitere Optimierung von SLC-Programmen . . . . . . . . . . . . 17

4 4 Datenflussanalyse und Optimierung iterativer Programme 25 4.1 Syntax von IC . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.2 Semantik von IC . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 4.3 Flussgraphen von IC-Programmen . . . . . . . . . . . . . . . . . 31 4.4 Datenflussanalyse-Systeme . . . . . . . . . . . . . . . . . . . . . . 32 4.5 AE-Analyse und CS-Elimination für IC-Programme . . . . . . . 36 4.6 RD-Analyse und Konstantenfaltung . . . . . . . . . . . . . . . . 39 4.7 Effiziente Fp-Berechnung . . . . . . . . . . . . . . . . . . . . . . . 43 4.8 Live Variable Analyse und Dead Code Elimination für IC-Programm 45

5 Kontrollflussanalyse und Schleifenoptimierung 49 5.1 Schleifenanalyse von Flussgraphen . . . . . . . . . . . . . . . . . 49 5.2 ud- und du-chains . . . . . . . . . . . . . . . . . . . . . . . . . . 52 5.3 Schleifeninvariante Berechnungen und Code Motion . . . . . . . . 53 5.4 Induktionsvariablen . . . . . . . . . . . . . . . . . . . . . . . . . 54

6 Interprozedurale Analyse 57 6.1 Syntax von ICP (Intermediate Code with Procedures . . . . . . . 57 6.2 Semantik in ICP . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 6.3 MOP-Analyse für ICP-Programme . . . . . . . . . . . . . . . . . 58 6.4 MFP-Analyse für ICP-Programme . . . . . . . . . . . . . . . . . 59

7 Analyse dynamischer Datenstrukturen 61 7.1 Erweiterung der Sprache IC . . . . . . . . . . . . . . . . . . . . . 61 7.2 Shape-Graphen . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 7.3 Die Analyse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 4 INHALTSVERZEICHNIS

Kapitel 1

Einleitung

[13.10.2004]

Ziel der Programmanalyse: Berechnung von Laufzeiteigenschaften zur Übersetzungszeit, abhängig von der Programmsemantik, Beispiel: Terminierung, i.a. nicht entscheidbare Eigenschaften. → Programmanalyse berechnet Approximationen dieser Eigenschaften Mittel: Abstrakte Interpretation Anwendungen der Programmanalyse:

• Compileroptimierung durch Programmtransformation

• Konstruktion von Software-Tools für Verfikation, Testen, Debugging

hier: Compileroptimierung Verbesserung von Programmen mit Hilfe von Programmeigenschaften Verschiedene Kostenmasse:

• Laufzeit

• Speicherbedarf der Laufzeitdaten (Grösse von Stack und Heap)

• Speicherbedarf des Codes (Programmgrösse)

Kompakter Code wichtig bei Palmtops, Mobiltelefonen, Software für eingebettete Systeme

Programmiersprachen:

• imperative:

– OO (Java: Klassenoptimierung)

– FP (Striktheitsanalyse)

– LP

[Folie: Struktur eines Compi-

Möglichkeiten für Programmanalyse und Compileroptimierung: lers]

1. Attributierte Abstrakter Syntaxbaum (Quellprogramm) erfordert Programmanalyse für strukturierte Programme 2. Zwischencode

elementare Ausdrücke, 3-Adresscode keine Kontrollstrukturen bis auf Sprungbefehle keine Datenstrukturen, Adressberechnung

3. Maschinencode Registerzuteilung, Codeselection, Instruktionsanordnung

Inhalt PACO für Zwischencode

1. Straight-line Code (ohne: Verzweigung, Iteration, Rekursion, Datenstrukturen) Wichtige Teilklasse. Schleifenrümpfe

90/10 Regel: Ein Programm benutzt 90% der Ausführungszeit für 10% seines Codes

→ lokale Analyse

2. Iterative Programme

(a) Basisblock-Darstellung und Flussgraphen → globale Analyse, intra-prozedurale Analyse Technik: Datenflussanalyse in Abstrakter Interpretation

(b) Kontrollflussanalyse und Schleifenoptimierung

3. Rekursive Programme

→ interprozedurale Analyse

4. Programme mit Datenstrukturen

statische und dynamische Datenstrukturen, Shape Analyse

Optimierungen: dead code elimination, common subexpression elimination, constant propagation/constant folding, reduction in strength, code motion Analysen: live variables, available expression, pointer, shape, alias

Analyse und Optimierung von Straight-Line Code

Programme ohne Verzweigung, Iteration, rekursion, Datenstrukturen, Ausdrücke entschachtelt Bedeutung: wiederholte Ausführung in Schleifen Ziel: Codeoptimierung (Laufzeit) Themen:

• Live Variable (LV) Analyse - Dead Code (DC) Elimination

• Available Expression (AE) Analyse - Common Subexpression (CS) Elimination

• Reaching Definition (RD) Analyse - Konstantenpropagation/-faltung

Definition 2.0.1: Syntax von SLC-Programmen V = {x, y, z, …} Variablen C = {a, b, c, …} Konstantensymbole Σ = ⋃_{r=1}^{∞} Σ^{(r)} mit |Σ| < ∞ Operationssymbole α ∈ \underline{Anw} (α ist eine Anweisung): ↶↷ α = x ← e und e ∈ {f(u_{1}, …, u_{r})|f ∈ Σ^{(r)}, u_{i} ∈ V ∪ C} V_{α} := {x} ∪ V_{e} (Variablen von α bzw. von e) x wird in α definiert, v ∈ V_{e} wird in α benutzt. β ∈ Blo (β ist ein Block) : ↶↷ β = α_{1}; α_{2}; … α_{n}, α_{i} ∈ \underline{Anw}, n ≥ 0 V_{β} := ⋃_{i=1}^{n} V_{α_{i}} (Variablen von β)

8KAPITEL 2. ANALYSE UND OPTIMIERUNG VON STRAIGHT-LINE CODE

Folgerung 2.0.1: π ∈ SLC (π ist ein SLC-Programm): ↶↷ π = (IV, β, OV), β ∈ \underline{Blo} IV ⊆ V, endlich (Eingabevariablen, var β definiert) OV ⊆ V, endlich, nicht leer (Ausgabevariablen, nach β benutzt)

[Folie: SLC-Beispielprogramm] [15.10.2004] V_{π} := ⋃_{i=1}^{n} V_{α_{i}} ∪ IV ∪ OV

Definition 2.0.2: Variablenbedingung π erfüllt die Variablenbedingung (π vollständig wohldefiniert) :↶↷ Jede Programmvariable v ∈ V_{π} wird vor ihrer Benutzung definiert

Generelle Vorraussetzung: SLC-Programme sollen die Variablenbedingung erfüllen

SLC-Programme (Semantik)

Sei π = (IV, β, OV) ∈ SLC. Sei 𝔞 = ⟨A; φ⟩ eine (Σ, C)- Algebra, d.h., A Menge, f ∈ Σ^{(r)} ↷ φ(f) = f_{𝔞} : A^{r} → A c ∈ C ↷ φ(c) = c_{𝔞} ∈ A Zustandsraum Z := {σ|σ : V_{π} → a} α ∈ Anw ↦ [[α]]_{𝔞} : Z → Z Zustandstransformation α = x ← e [[x ← e]]_{𝔞}(σ) = σ′ mit σ′(x) = [[e]]_{𝔞}(σ) ∈ A (Wert von e im Zustand σ, “Einsetzen und Ausrechnen“) und σ′(y) = σ(y) für y ≠ x β = α_{1}; …; α_{n} ↦ [[β]]_{𝔞} := [[α_{n}]] ∘ [[α_{n−1}]] ∘ … ∘ [[α_{1}]] β = Σ ↦ [β]_{𝔞} := id_{Z} IV und OV bestimmen entsprechende Teile des Zustandsraumes Z. Z_{in} = {σ_{in}|σ_{in} : IV → A} Eingabezustände Z_{out} = {σ_{out}|σ_{out} : OV → A} Ausgabezustände damit ergibt sich die Programmsemantik [[π]]_{𝔞} : Z_{in} → Z_{out} [[π]]_{𝔞}(σ_{in}) = σ_{out} σ_{in} ↦ σ_{0}(x) := σ_{in}(x) für x ∈ IV σ_{0}(y) = a ∈ A (beliebig) für y ∈ IV σ_{out}(z) = [[β]]_{𝔞}(σ_{0})(z) für z ∈ OV Beachte: π erfüllt die Variablenbedingung ↷ [[π_{𝔞}]] unabhängig von Anfangswerten für y ∈ V_{π}\IV

Definition 2.0.3: Programmäquivalenz π_{1}, π_{2} ∈ SLC. 𝔞 (Σ, C)-Algebra

• π_{1} und π_{2} 𝔞-äquivalent (π_{1} ∼_{𝔞} π_{2}) :↶↷ [[π_{1}]] = [[π_{2}]]_{𝔞}

• π_{1} und π_{2} stark-äquivalent (π_{1} ≈ π_{2}) :↶↷ [[π_{1}]] = [[π_{2}]] für jede (Σ, C)- Algebra 𝔞

Optimierung von SLC-Programmen

Sei c : SLC → ℕ eine Kostenfunktion, z.B. Zahl der Anweisungen, Zahl der Operationen, Summe der Operations-Gewichte Für π_{1}, π_{2} ∈ SLC mit π_{1} ∼_{𝔞} π_{2} (bzw π_{1} ≈ π_{2}) ist π_{1} ≤_{c} π_{2} (c-besser):↶↷ c(π_{1}) ≤ c(π_{2})

Definition 2.0.4: c-optimal π_{1} c-optimal (bzgl. 𝔞) :↶↷ π_{1} ≤_{c} π für alle π ∈ SLC mit π_{1} ≈ π (bzw. π_{1} ∼_{𝔞} π)

Ziel: Programmtransformationen zur SLC-Optimierung [Folie: Beispiel: Common Subexpression Elimination]

2.1 AE-Analyse und CS-Elimination

Beispiel 2.1.1: Folie 2.2 π ≈ π′ und c(π′) < c(π) bzgl. Op-Anzahl aber c(π′) > c(π) bzgl. Codelänge

AE-Analyse Bestimmung der für jede Anweisung verfügbaren Ausdrücke (AE = available expression) Sei π = (IV, β, OV) ∈ SLC mit β = α_{1}; …; α_{n} \underline{OpExp}_{β} := \{e|x ← e = α_{i}, e = f(u_{1}, …, u_{r})\} = \{e_{1}, …, e_{t}\} Operationsausdrücke von β Verfügbarkeit durch Bit-vektoren beschreiben: 𝔹^{t} := {(b_{1}, …, b_{t})|b_{i} ∈ {0, 1}} Bedeutung: b_{i} = 0 heisst ”e_{i} ist verfügbar“ b_{i} = 1 heisst ”e_{i} ist nicht verfügbar“ AE_{i} ∈ 𝔹^{t}: die für Ausführung von α_{i} verfügbaren Ausdrücke (i = 1, …, n) AE_{1} = (1, …, 1) α ∈ Anw ↦ t_{α} : 𝔹^{t} → 𝔹^{t} (information transformer) t_{α} beschreibt die Veränderung der Verfügbarkeit von Ausdrücken durch Ausführung von α t_{x←e} := kill_{x} ∘ gen_{e}; gen_{e}, kill_{x} : 𝔹^{t} → 𝔹^{t} gen_{e}(b_{1}, …, b_{t}) = (b′_{1}, …, b′_{t})

b′_{i} = \begin{cases}0, & falls e = e_{i} \\ b_{i}, & sonst \end{cases}

kill_{x}(b_{1}, …, b_{t}) = (b′_{1}, …, b′t)

b′_{i} = \begin{cases}1, & falls x ∈ V_{e_{i}} \\ b_{i}, & sonst \end{cases}

AE_{i+1} = t_{α_{i}}(AE_{i}) für i = 1, …, n − 1 Ergebnis: Analyseinformationen AE_{1}, …, AE_{n} [20.10.2004] Beobachtung: A_{i} = x ← x keine Veränderung von x, aber Verfügbarkeit von Ausdrücken wird i. a. reduziert.

Beispiel 2.1.2: Folie 2.2 Common Subexpression Elimination

\underline{OpExp}_{β} = \{oe_{1} = x + y, oe_{2} = z ∗ y, oe_{3} = v − z, oe_{4} = w + v\} AE_{1} = (1, 1, 1, 1) AE_{2} = (0, 1, 1, 1) AE_{3} = (0, 1, 1, 1) AE_{4} = (1, 1, 1, 1) AE_{5} = (0, 1, 1, 1) AE_{6} = (0, 1, 0, 1)

CS-Elimination Ziel: Vermeidung der wiederholten Berechnung eines Ausdrucks mit denselber Variablenwerten, weniger durchgeführte Rechenoperationen. Idee: Ausdruckswerte auf temporären Variablen zwischenspeichern, statt wiederholter Berechnung temporäre Variable verwenden. T_{CS} : SLC → SLC T_{CS}(IV, β, OV) := (IV, T_{CS}(β), OV) T_{CS}(α_{1}; …; α_{n}) := T_{CS}(α_{1}); …; T_{CS}(α_{n}) 3 Fälle für T_{CS}(α_{1})

1. α_{i} = x ← e, e ∉ \underline{OpExp}_{β} ↷ T_{CS}(α_{i}) := α_{i}

2. α_{i} = x ← oe_{j}, AE_{i}^{(j)} = 1 ↷ T_{CS}(α_{i}) := tv_{j} ← oe_{j}; x ← tv_{j}

3. α_{i} = x ← oe_{j}, AE_{i}^{(j)} = 0 ↷ T_{CS}(α_{i}) := x ← tv_{j}

mit temporären Variablen tv_{1}, …, tv_{t} für die Op-Ausdrücke oe_{1}, …, oe_{t}

Beispiel 2.1.3: Fall (1) tritt nicht auf. Die “relevanten“ Verfügbarkeitsbits sind: AE_{1}^{(1)} = 1 AE_{2}^{(2)} = 1 AE_{3}^{(1)} = 0 AE_{4}^{(1)} = 1 AE_{5}^{(3)} = 1 AE_{6}^{(4)} = 1

T_{CS}(β) = tv_{1} ← x + y;
z ← tv_{1};
tv_{2} ← z ∗ y;
z ← tv_{2};
x ← tv_{1};
tv_{1} ← x + y;
v ← tv_{1};
tv_{3} ← v − z;
w ← tv_{3};
tv_{4} ← w + v;
w ← tv_{4};

Korrektheit π ≈ T_{T C}(π) unabhängig von Interpretation Klar für die Fälle 1 und 2 Fall 3: Der verfügbare Wert von oe_{j} liegt als Wert von tv_{j} vor. Optimierung: Op − Anzahl(T_{CS}(π)) ≤ Op − Anzahl(π) aber: Codelänge(T_{CS}(π)) > Codelänge(π)

2.2 LV-Analyse und DC-Elimination

LV-Analyse π = (IV, β, OV) ∈ SLC Var. Bedingung: v ∈ V_{π} wird vor ihrer Benutzung definiert. Möglich: v ∈ V_{π} wird nach ihrer Definition nicht benutzt.

Definition 2.2.1: lebendig v ∈ V_{π} heisst lebendig in i (v ∈ LV_{i}) für i = 1, …, n falls v in α_{i+1}, α_{i+2}, …, α_{n} oder OV benutzt wird, ohne vor dieser Benutzung neu definiert zu werden.

Bestimmung der LV_{i} durch Rückwärtsanalyse: LV_{n} = OV α ∈ \underline{Anw} ↦ t_{α} : P (V_{π}) → P (V_{π}) “Rückwärtstransformation“ α = x ← e; t_{α} := gen_{e} ∘ kill_{x} kill_{x}(M) := M/{x} gen_{e}(M) := M ∪ V_{e} LV_{i−1} := t_{α_{i}}(LV_{i}) i = 1, …, n

Beispiel 2.2.2: LV_{4} = {u, v} LV_{3} = {u, x, y} LV_{2} = {x, y} LV_{1} = {x, y, u, z} LV_{0} = {x, y, z}

DC-Elimination T_{DC} : SLC → SLC Entferne α_{i} aus β = α_{1}; …; α_{n}, falls α_{i} = x ← e und x ∉ LV_{i}(i = 1, …, n) Bsp: Entferne α_{2}, nicht jedoch α_{1}: Möglichkeit: LV-Analyse wiederholen Verbesserte Analyse: NV (needed Variable)-Analyse Modifikation:

[22.10.2004] α = x ← e t̃_{α}(M) := \overline{if} x ∈ M \overline{then} M/x ∪ V_{e} \overline{else} M NV_{n} = OV NV_{i−1} := t̃_{α_{i}}(NV_{i})

Beispiel 2.2.3: NV_{4} = {u, v} NV_{3} = {u, x, y} NV_{2} = {x, y} NV_{1} = {x, y} NV_{0} = {x, y}

Korrektheit: π ≈ T_{DC}(π) ≈ T̃_{DC}(π) Optimierung: c(T̃_{DC}(π)) ≤ c(T_{DC}(π)) ≤ c(π) c: Programmlänge, Op-Anzahl

2.3 RD-Analyse und Konstantenfaltung

Ziel: partielle Auswertung von π ← SLC-Programm unter Kenntnis von Konstanten (Einfluss der Semantik); genauer: ersetze konstante Variablen und konstante Ausdrücke auf rechten Seiten von Wertzuweisungen durch ihre Werte (Propagation [Variablen] und Faltung [Ausdrücke]) RD-Analyse: π = (IV, β, OV) ∈ SLC mit β = α_{1}; …; α_{n} Interpretation 𝔞 = ⟨A; φ⟩ Bestimme für i = 1, …, n die dort gültigen, eingabeunabhängigen (konstanten) Variablenwerte. V_{π} = {v_{1}, …, v_{k}} D := (A ∪ {□})^{K} d = (d_{1}, …, d_{k}) d_{j} ∈ A bedeutet: v_{j} hat den Wert d_{j} d_{j} ∈ □ bedeutet: Wert von v_{j} unbekannt oder eingabeabhängig für j = 1, ..., k Erweiterung der Ausdrucksemantik von e: [[e]]_{𝔞}(d) ∈ A ∪ {□} [[e]]_{𝔞}(d) = □ :↶↷ ∃v_{j} ∈ V_{e} mit d_{j} = □ (Strikte Semantik: 0 ∗ □ = □) t_{x←e}(d_{1}, …, d_{k}) = d‘_{1}, …, d‘_{k})

d_{j} = \begin{cases}[[e]]_{𝔞}(d_{1}, …, d_{k}), & falls x = v_{j} \\ d_{j}, & sonst \end{cases}

RD_{1} = (□, …, □) ∈ D RD_{i+1} = t_{α_{i}}(RD_{i}) RD_{i} ∈ D = (A ∪ {□})^{k}

Beispiel 2.3.1:

V_{π} = \{\underbrace{x}_{1}, \underbrace{y}_{2}, \underbrace{z}_{3}\}

RD_{1} = (□, □, □) RD_{2} = (□, 10, □) RD_{3} = (□, 10, 2) RD_{4} = (□, 10, 20) RD_{5} = (□, □, 20) RD_{6} = (□, □, □)

Konstantenfaltung T_{CF} : SLC → SLC T_{CF} (IV, β, OV) := (IV, T_{CF} (β), OV) T_{CF} (α_{1}; …; α_{n}) := T_{CF} (α_{1}); …; T_{CF} (α_{n}) T_{CF} (α_{i}) := x_{i} ← T_{CF} (e_{i}, RD_{i}) α_{i} = x_{i} ← e_{i} T_{CF} (a, d) := a T_{CF} (v_{j}, d) := \overline{if} d_{j} ∈ A \overline{then} d_{j} \overline{else} v_{j} T_{CF} (f(u_{1}, …, u_{r}), d) := \overline{if} ∃j ∈ \{1, …, k\}T_{CF} (u_{j}, d) ∈ V_{π} \overline{then} f(T_{CF} (u_{1}, d), …, T_{CF} (u_{r}, d)) \overline{else} f_{𝔞}(T_{CF} (u_{1}, d), …, T_{CF} (u_{r}, d))

Beispiel 2.3.2: T_{CF} (α_{3}) = z ← T_{CF} (y ∗ z, (□, 10, 2)) = z ← 20 T_{CF} (α_{5}) = z ← T_{CF} (y∗z, (□, □, z)) = z ← T_{CF} (y, (□, □, 20))∗T_{CF} (z, (□, □, 20)) = Z ← y ∗ 20)

Korrektheit von T_{CF}

Offensichtlich gilt: π ∼_{𝔞} T_{CF} (π) Optimierung: Programmlänge unverändert, Op-Anzahl kann sinken Besonderer Seiteneffekt: Entstehung von Dead Code Bsp: α_{2}, α_{1}, α_{3}

2.4 DAG-Darstellung von SLC-Programmen

DAG (directed acyclic graph) nützliche Datenstruktur zur Implementierung von Transformationen auf SLC-Programmen Idee: Termdarstellung der Werte einer Berechnung

Definition 2.4.1: gerichteter (Σ, V, A)-Graph D = ⟨K, lab, suc⟩ heisst gerichteter (Σ, V, A)-Graph, wenn

• k nicht-leere, endliche Menge von Knoten • lab: K → (Σ ∪ V ∪ A) eine Markierungsfunktion

• suc: K × ℕ → K eine Nachfolgerfunktion mit der Eigenschaft suc(k, i) ist def ↶↷ \underline{lab}(k) = f ∈ Σ^{(r)} und 1 ≤ i ≤ r

[25.10.2004]

Definition 2.4.2: Ein gerichteter azyklischer (Σ, V, A)-Graph heisst (Σ, V, A)-DAG.

Beachte: Jeder Knoten k eines solchen Graphen repräsentiert einen Term t_{k} ∈ T_{Σ}(V ∪ A)

Der DAG eines SLC-Programms

Sei π = (IV, β, OV) ∈ SLC mit β = α_{1}; …; α_{n} Der DAG von π wird durch “Symbolische Programmausführung mit Konstantenfaltung“ bestimmt. Wir definieren den DAG zunächst ohne Bezug auf OV: D(IV, β) = ⟨K; \underline{lab}; \underline{suc}⟩ zusammen mit einer Bewertungsfunktion \underline{val} : IV ∪ V_{β} → K Bei der \underline{val}(x) = k, falls k den Wert von x nach Durchführung von β darstellt Idee:

• verschiedene Knoten für verschiedene Werte (sharing!)

→ CS-Elimination

• ersetzen konstanter Ausdrücke → CF-Transformation

Anschliessende Betrachtung von OV

• OV bestimmt Teilgraphen → D(π)

→ DC-Elimination

Konstruktion von D(IV, β) und val durch Induktion über die Codelänge n.

1. Induktionsanfang: n = 0 D(IV, E) := ⟨K; \underline{lab}; \underline{suc}⟩ mit K := IV \underline{lab}(x) := x für alle x ∈ IV \underline{Def}(\underline{suc}) := ∅ \underline{val}(x) := x

2. Induktion: n → n + 1 (IV, β_{n+1}) mit β_{n+1} = α_{1}; … α_{n}; α_{n+1} Nach Induktionsvorraussetzung ist für β_{n} := α_{1}; …; α_{n} bekannt D(IV, β_{n}) = ⟨K; \underline{lab}; \underline{suc}⟩ und \underline{val}(x) ∈ K für alle x ∈ IV ∪ V_{β_{n}} Konstruktion von D(IV, β_{n+1}) = ⟨K′; \underline{lab′}; \underline{suc′}⟩ und \underline{val′} : IV ∪ V_{β_{n+1}} → K′ ist bestimmt durch α_{n+1} = x ← e (a) e = y

Nach Induktionsvorraussetzung (und Variablenbedingung) \underline{val}(y) ∈ K D(IV, β_{n+1}) := D(IV, β_{n}) \underline{val‘}(x) := \underline{val}(y) (“sharing“) \underline{val‘}(x‘) := \underline{val}(x‘) für x‘ ≠ x

(b) e = a ∈ A

i. a ∈ K D(IV, β_{n+1}) := D(IV, β_{n}) und \underline{val‘}(x) = a \underline{val‘}(x‘) =

\underline{val‘}(x‘) für x‘ ≠ x ii. a ∉ K K‘ := K ∪ \{a\} \underline{lab‘}(a) = a und \underline{suc‘}(a, i) nicht

definiert für alle i \underline{suc‘}(k, i) = \underline{suc}(k, i) sonst \underline{val‘}(x) := a ∈ K‘ \underline{val‘}(x′) = \underline{val‘}(x‘) x‘ ≠ x

(c) e = f(u_{1}, …, u_{f}) mit u_{j} ∈ V ∪ A

a) Für alle j = 1, …, r gilt: u_{j} ∈ A (falls u_{j} ∉ K, neuen Knoten wie in 2b) oder u_{j} ∈ V mit \underline{val}(u_{j}) ∈ A Dann folgt: f_{𝔞}(u‘_{1}, …, u‘_{r}) =: b ∈ A

mit u‘_{j} = \begin{cases}u_{j}, & falls u_{j} ∈ A \\ \underline{val}(u_{j}), & falls u_{j} ∈ V \end{cases}

a1) b ∈ K D(IV, β_{n+1}) := D(IV, β_{n})

\underline{val‘}(x) := b \underline{val‘}(x‘) = \underline{val}(x‘) für x‘ ≠ x a2) b ∉ K Erweiterung von D(IV, β_{n}) um neuen Knoten für b

Bewertung val‘ wie in a1 b Es gibt j ∈ \{1, …, r\} mit u_{j} ∈ V und \underline{val}(u_{j}) ∉ A b1 Es gibt k ∈ k mit \underline{lab}(b) = f

und \underline{suc}(k, j) = \begin{cases}a, & falls u_{j} = a ∈ A \\ \underline{val}(u_{j}), & falls u_{j} ∈ V \end{cases}

D(IV, β_{n+1}) := D(IV, β_{n}) \underline{val‘}(x) := k und \underline{val}(x‘) = \underline{val}(x‘) für x‘ ≠ x

b2) Es gibt kein k ∈ K, welches nach b1) den Wert e repräsentiert. K‘ := K ˙∪{k‘} (neuer Knoten k‘) \underline{lab‘}(k‘) := f

\underline{suc‘}(k‘, j) := \begin{cases}a, & falls u_{j} = a ∈ A \\ \underline{val}(u_{j}), & falls u_{j} ∈ V \end{cases}

[Folie: Beispiel: DAG-Konstruktion]

[29.10.2004] π = (IV, β, OV) ∈ SLC β = α_{1}; …; α_{n}

Eigenschaften von D(IV, β):

1. Verschiedene Knoten repräsentieren verschiedene Terme:

k_{1} ≠ k_{2} ↷ t_{k_{1}} ≠ t_{k_{2}}

2. Kein Knoten repräsentiert einen konstanten Op-Term t_{k} ∈ T_{Σ}(A) ↷ t_{k} ∈ A

Folgerung:

1. unterstützt CS-Elimination

2. unterstützt CF-Transformation

Bsp:

• gemeinsame Teilausdrücke: \underline{val}(t) = \underline{val}(u)

• Konstantenfaltung: \underline{val}(z) = 4, \underline{val}(v) = \underline{val}(t) ∗ 4

D(IV, β) unterstützt mit Hilfe von OV auch die DC-Elimination k ∈ K heisst ausgaberelevant, wenn y ∈ OV existiert, so dass k von \underline{val}(y) erreichbar ist. Nicht ausgaberelevante Knoten repräsentieren Dead Code Bsp: 2⊕-Knoten und (2) Durch entfernen dieser Knoten und Einschränkung von val auf OV erhalten wir:

1. den DAG von π: D(π)

2. die Bewertungsfunktion val: OV → K

Programmoptimierung mit D(π) und \overline{val} OV → K

Konstruktion eines DAG-optimierten Programms T_{D}(π) := π_{D} := (IV, β_{D})

Fall 1 val injektiv, d.h. verschiedene Ausgabevariablen zeigen auf verschiedene Knoten

(a) \underline{val}(OV) ∩ (IV ∪ A) = ∅, d.h., Ausgabevariablen zeigen nur auf Op-Knoten Idee: Op-Knoten als Hilfsvariablen verwenden und für \underline{val}(y) = k y statt k verwenden Jeder Op-Knoten k bestimmt mit \underline{lab}(k) = f ∈ Σ^{(r)} und den Nachfolgeknoten eine Anweisung: α_{k} := K ← f(\underline{suc}(k, 1), …, \underline{suc}(k, r)) Beachte: \underline{suc}(k, j) ∈ IV ∪ A ∪ K ∪ OV Wähle eine Bottom-Up-Numerierung der Op-Knoten k_{1}, k_{2}, …, k_{s} (z.B schichtenweise von links nach rechts) so dass k_{j} ← f(… k_{i} …) ↷ i < j. Dann gilt π_{D} := (IV, β_{D}, OV) ∈ SLC mit π_{D} := α_{k_{1}}; …; α_{k_{s}} Beachte: OV ⊆ {k_{1}, …, k_{i}} und π_{D} erfüllt die Variablenbedingung. Ausserdem besitzt π_{d} die “single assignment“-Eigenschaft.

(b) \underline{val}(y) ∈ IV ∪ A

π_{D} von a) um y ← \underline{val}(y), es sei denn, dass y = \underline{val}(y).

Fall 2 \underline{val}(y_{1}) = \underline{val}(y_{2}) = … = \underline{val}(y_{n})

π_{D}-Konstruktion von Fall 1 bezüglich y_{1}, durchführen auf y_{2} ← y_{1}, …; y_{n} ←

y_{1} ergänzen
Zusammenhang zwischen DAG-Optimierung und CS-, DC-, CF- und Cp-Optimierung

Beispiel 2.4.3: T_{DC}(T_{CP} (T_{CS}(T_{CF} (π))))

T_{CF} (π) : ; u ← 2; ; w ← x + y; ; z ← 4; ; u ← x ∗ w; ; v ← 4 + w; ; v ← u + 4; ; t ← x ∗ w; ; v ← t ∗ z; ; OV: u, v  u ← 2; ; (1) w ← x + y; ; \overline{z ← 4;} ; (2) u‘ ← x ∗ w; ; \overline{u ← u‘;} ; \overline{v ← 4 + w;} ; \overline{v ← u‘ + 4;} ; \overline{t ← u‘;} ; (3) v ← u‘ ∗ 4; ; OV: u‘, v

Allgemein gilt:

1. Die DAG-Transformation ist korrekt:

π ≈ π_{D}

Beachte: Die Konstantenfaltung kann bereits ohne Interpretation durchgeführt werden. (bzw. auf Termen; Grundterme als Konstantensymbole zulassen)

2. T_{D}(π) ist optimal bzgl. T_{DC}, T_{CS}, T_{CF}, T_{CP}, d.h. keine dieser Transformationen kann T_{D}(π) weiter optimieren.

3. T_{D}(π) optimal bzgl. ≈ und Codelänge (?)

4. Vermutung: Für jedes π ∈ SLC gibt es ein n ∈ ℕ mit T_{D}(π) = [T_{DC} ∘ (T_{CP} ∘ T_{CS})^{n} ∘ T_{CF}](π) [03.11.2004]

5. T_{D} nicht auf iterative Programme übertragbar, wohl aber die anderen Transformationen T_{CS}, T_{CF}, T_{CP}, T_{DC}

2.5 Weitere Optimierung von SLC-Programmen

Berücksichtigung der Interpretation 𝔞 = ⟨A_{i}; φ⟩ als (Σ, C)-Algebra Algebraische Eigenschaften: Gleichungen

Beispiel 2.5.1: ⟨ℤ; +, −, ∗, /⟩ 18KAPITEL 2. ANALYSE UND OPTIMIERUNG VON STRAIGHT-LINE CODE

• neutrale Elemente:

\begin{matrix}0 + a = a \\ 1 ∗ a = a \\ a/1 = 1 \end{matrix}

• kommutative Operationen:

\begin{matrix}a + b = b + a \\ a ∗ b = b ∗ a \end{matrix}

• assoziative Operationen: (a + b) + c = a + (b + c)

• distributive Operationen: a ∗ (b + c) = a ∗ b + a ∗ c

Beispiel 2.5.2: ⟨𝔹; and, not, true, false⟩

• true or b = true

• false and b = false

• not not b = b

Ziel algebraischer Transformationen:

• ersetze teure Anweisungen durch billigere

• lokale, kontextunabhängige Ersetzun

• keine Gesamtanalyse von π erforderlich Peep-hole-Optimierung Idee: schiebe ein kleines Fenster über das Programm und optimiere innerhalb des Fensters Beispiel 2.5.3:

• \begin{matrix}y ← x + a \\ z ← y − a; \end{matrix}\} {y ← x + a; \atop z ← x;}

• x ← x + 0; weglassen

• u ← x + y; v ← y + z; w ← v + x; v wird nicht mehr benötigt w = (y + z) + x = (x + y) + z

u ← x + y;

w ← u + z;

Reduction in Strength

Ersetze x ← y ∗ ∗2 durch x ← y ∗ y; Ersetze x ← 2 ∗ y durch x ← y + y;

Optimalität von SLC-Programmen

Spezialfall: 𝔞 = ⟨ℤ; +, ∗⟩ keine Konstanten Kostenmass: Programmlänge Dann gilt für π ∈ SLC : es existiert ein optimales Programm π_{opt} für π d.h. π_{opt} 𝔞^{∼} π und c(π_{opt}) ≤ c(π‘) für alle π‘ mit π‘ 𝔞^{∼} π Konstruktion von π_{opt}: NP-vollständig (?) optimaler Code für arithmetische Ausdrücke Polynomberechnung [Folie: Optimierung von Po-Spezialfall: g(x) = ax^{16} + x^{8} + cx^{4} + dx^{2} + ex + f lynomen]

• DAG-optimales π mit 36 Anweisungen, 31 Multiplikationen

• möglich: 14 Anweisungen, 9 Multiplikationen 20KAPITEL 2. ANALYSE UND OPTIMIERUNG VON STRAIGHT-LINE CODE Semantik iterativer und rekursiver Programme ebenso wie Datenflussanalyse beschreibbar als Lösung von Gleichungssystemen dazu: vollständige Halbordnungen, vollständige Verbände monoton und stetige Funnktionen Fixpunktberechungen

Definition 2.5.4: Halbordnung Sei D eine Menge und ≤⊆ D × D. Dann heisst D = ⟨D, ≤⟩ eine Halbordnung mit der Halbordnungrelation ≤, falls für alle a, b, c, ∈ D gilt:

• a ≤ a (reflexiv)

• a ≤ b, b ≤ c ↷ a ≤ c (transitiv)

• a ≤ b, b ≤ a ↷ a = b (antisymmetrisch)

Sei a ∈ D und T ⊆ D. Dann heisst

• a obere Schranke von T, falls T ≤ a

• a kleinstes Element von T, falls a ∈ T und a ≤ T

• a kleinste obere Schranke von T, falls T ≤ a und (T ≤ a‘ ↷ a ≤ a‘)

Bez: a ⨆ T (“join“, “lub“ (least upperbound))

Beachte: kleinste Elemente, insbesondere ⨆, sind eindeutig bestimmt.

• Besitzt D ein kleinstes Element, so wird es durch ⊥ (“bottom“) bezeichnet

• γ : ℕ → D heisst Kette, falls γ(i) ≤ γ(i + 1) für alle i ∈ ℕ (aufsteigende ω Kette)

Bez.: (γ(i)|i ∈ ℕ) = γ

nicht verwechseln mit: {γ(i)|i ∈ ℕ}

• D heisst vollständige Halbordnung falls D ein kleinstes Element hat und jede Kette γ eine kleinste obere Schranke besitzt: ⨆ γ := ⨆{γ(i)|i ∈ ℕ}

• D heisst vollständiger Verband, falls jede Teilmenge T ⊆ D eine kleinste obere Schranke ⨆ T besitzt (Beachte: ⨆ = ⊥∅)

Schreibweise: a ⨆ b := ⨆{a, b} [05.11.2004]

Beispiel 2.5.5: Seien A und B Mengen. Die Menge der P F (A, B) := {f|f : A −−→ B} der partiellen Funktionen von A nach B ist halbgeordnet durch ≤ mit f ≤ g :↶↷ (f(a) ∈ B ↷ f(a) = g(a) für alle a ∈ A), oder: \underline{graph(f)} ⊆ \underline{graph}(g). Die “leere“ Funktion f_{∅} mit \underline{Def}(f_{∅}) = ∅ ist kleinstes Element von ⟨P F (A, B); ≤⟩ Jede Kette f_{0} ≤ f_{1} ≤ … besitzt eine kleinste obere Schranke f = ⨆{f_{i}|i ∈ ℕ}. f(a) = b ∈ B ↶↷ ∃i ∈ ℕ : f_{i}(a) = b Also ist ⟨P F (A, B); ≤⟩ eine vollständige Halbordnung (cpo = complete partial order) Spezialfall: P F (A) := P F (A, A) Anwendung: Semantik iterativer Programme

Beispiel 2.5.6: Sei A eine Menge Die Potenzmenge P (A) := {T |T ⊆ A} ist halbgeordnet durch ⊆ und bildet mit ⊆ einen vollständigen Verband: für T ⊆ P (A) gilt ⨆ T = ∪{T |T ∈ T } Anwendung: Datenflussanalyse (DFA)

Beachte: Ist D = ⟨D, ≤⟩ eine Halbordnung, so auch D‘ := ⟨D, ≥⟩, die duale Halbordnung von D

Definition und Lemma 2.5.7: Produkt von Halbordnungen Sind D_{i} = ⟨D_{i}; ≤_{i}⟩ für i = 1, 2 Halbordnung, so auch D_{1} × D_{2} := ⟨D_{1} × D_{2}; ≤⟩ mit (a_{1}, a_{2}) ≤ (b_{1}, b_{2}) :↶↷ a_{i} ≤_{i} b_{i} für i = 1, 2

Definition und Lemma 2.5.8: Funktionenraum Sei A eine Menge. Ist D = ⟨D; ≤⟩ eine Halbordnung, so auch F (A, D) := ⟨F (A, D); ≤⟩ mit F (A; D) := {f|f : A → D} und f ≤ g :↶↷ f(a) ≤ g(a) für alle a ∈ A

Folgerung 2.5.8: Sind D, D_{1} und D_{2} vollständige Halbordnungen bzw vollständige Verbände, so auch D_{1} × D_{2} und F (A, D). Insbesondere gilt für Ketten:

• ⨆{(a_{1}^{(i)}, a_{2}^{(i)})|i ∈ ℕ} = (⨆{a_{1}^{(i)}|i ∈ ℕ}, ⨆{a_{2}^{(i)}|i ∈ ℕ})

• ⨆({f^{(i)}|i ∈ ℕ})(a) = ⨆{f^{(i)}(a)|i ∈ ℕ}

und für beliebige Teilmengen

• ⨆ T = (⨆ \underline{proj}_{1}(T), ⨆ \underline{proj}_{2}(T)) mit T ⊆ D_{1} × D_{2}

• (⨆ T)(a) = ⨆ T (a) mit T ⊆ F (A, D).

Definition 2.5.9: monotone und stetige Funktionen Seien D_{i} = ⟨D_{i}; ≤_{i}⟩ für i = 1, 2 Halbordnungen und f: D_{1} → D_{2}.

• f heisst monoton, falls a ≤_{1} b ↷ f(a) ≤_{2} f(b) für alle a, b ∈ D_{1},

• f heisst stetig, falls D_{1} und D_{2} vollständig, f monoton und für jede Kette (a_{i}|i ∈ ℕ) um D_{1} gilt: f(⨆{a_{i}|i ∈ ℕ}) = ⨆{f(a_{i})|i ∈ ℕ} 2.5. WEITERE OPTIMIERUNG VON SLC-PROGRAMMEN 23 Beachte: f monoton ↷ (f(a_{i})|i ∈ ℕ) Kette. Definition 2.5.10: D besitzt die ACC-Eigenschaft (ACC = ascending chain condition), wenn gilt: Für jede Kette (a_{i}|i ∈ ℕ) ist {a_{i}|i ∈ ℕ} endlich Folgerung 2.5.10:

1. Eine HO mit ACC ist vollständig

2. Monotone Abb. auf HO mit ACC sind stetig

Definition 2.5.11: Distributivität Sind D_{1} und D_{2} vollständige Verbände, so heisst f : D_{1} → D_{2} distributiv, falls f(a ⨆ b) = f(a) ⨆ f(b) für alle a, b ∈ D_{1} Lemma 2.5.12: Seien D_{1} und D_{2} vollständige Verbände. Dann gilt: f : D_{1} → D − 2 distributiv ↷ f monoton. Beweis a ≤ b ↷ b = a ⨆ b ↷ \underline{f(b)} = f(a ⨆ b)\underline{= f(a) ⨆ f(b)} ↷ f(a) ≤ f(b) Folgerung 2.5.12: Besitzen D_{1} und D_{2} auch ACC, so gilt: f : D_{1} → D_{2} distributiv ↷ f monoton ↷ f stetig Satz 2.5.13: Fixpunktsatz Sei D = ⟨D; ≤⟩ eine vollständige HO und f : D → D stetig. Dann gilt:

1. (f^{i}(⊥)|i ∈ ℕ) ist eine Kette von D

2. a := ⨆{f^{i}(⊥)|i ∈ ℕ} ist Fixpunkt von f, d.h.: a = f(a).

3. a ist kleinster Fixpunkt von f, d.h. a = f(a), Bez: fix(f). Beweis:

1. ⊥ ≤ f(⊥) ≤ f^{2}(⊥) ≤ … (weil f monoton)

2. f(a) = f(⨆{f^{i}(⊥)|i ∈ ℕ}) = ⨆{f^{i+1}(⊥)|i ∈ ℕ} = ⨆{f(⊥)|i ∈ ℕ} = a 3. b = f(b)

⊥ ≤ b, f(⊥) ≤ b, f^{2}(⊥) ≤ b … ↷ b ist obere Schranke von {f^{i}(⊥)|i ∈ ℕ) ↷ a ≤ b 24KAPITEL 2. ANALYSE UND OPTIMIERUNG VON STRAIGHT-LINE CODE □ Folgerung 2.5.13: Ist D eine HO mit ACC und f : D → D monoton. Dann gilt: f besitzt einen kleinsten Fixpunkt \underline{fix}(f) und es existiert m ∈ ℕ, so dass \underline{fix}(f) = f^{m}(⊥)

[10.11.2004]

4 Datenflussanalyse und Optimierung iterativer Programme

Zwischencode für eine abstrakte Maschine: SLC und Verzweigung und Iteration Bedingte und unbedingte Sprünge als einzige Kontrollstrukturen Inhalt:

• Syntax und Semantik von IC (iterativer Code)

• Basisblock-Darstellung von IC-Programmen

• Abstrakte Interpretation und Datenflussanalyse (DFA)

• Verallgemeinerung der Analyse und Optimierung von SLC-Programmen auf IC-Programmen

4.1 Syntax von IC

Erweiterung von SLC V = {x, y, …} Variablen C = {c, d, …} Konstante Symbole Σ = ∪_{r≥1}Σ^{(r)}Op − Symbole (evtl.:C = Σ^{(?)}) π = ∪_{r≥0}π^{(r)} Prädikatssymbole Σ und π endlich L = {l_{i}|i ∈ ℕ} Sprungmarken (“Label“)

Definition 4.1.1: Anw Anweisungen

• Wertzuweisungen:

26KAPITEL 4. 4 DATENFLUSSANALYSE UND OPTIMIERUNG ITERATIVER PROGRAMME

v ← e mit v ∈ V und e ∈ V ∪ C ∪ {f(u_{1}, …, u_{r})|f ∈ Σ^{(r)}, u_{i} ∈ V ∪ C} • Sprunganweisungen:

\overline{goto} l mit l ∈ L, \overline{if} p(u_{1}, …, u_{r}) \overline{goto} l mit p ∈ π^{(r)}, u_{i} ∈ V ∪ C, l ∈ L

[Folie: IC-Beispielprogramm: Fakultätsberechnungen] [Folie: Beispiel: Flussdiagramm und -graph] IC-Programme π = (V list, Alist) ∈ IC :↶↷ V list = \overline{in} x_{1}, …, x_{n}; \overline{out} y_{1}, …, y_{m}; \overline{loc} z_{1}, …, z_{p}; mit

• IV := {x_{1}, …, x_{n}} Eingabevariablen (n ≥ 0)

• OV := {y_{1}, …, y_{m}} Ausgabevariablen (m ≥ 1)

• LV := {z_{1}, …, z_{p}} lokale Variablen (p ≥ 0)

• V_{π} = IV ∪ OV ∪ LV Programmvariablen

Alist = α_{1}; …; α_{q} (Anweisungsliste) mit

• α_{i} ∈ \underline{Anw}, V_{α_{i}} ⊆ V_{π}, q ≥ 0

• eindeutige Sprungziele: α_{i} = l : …, α_{j} = l‘ : …, i ≠ j ↷ l ≠ l‘

π erfüllt die Variablenbedingung: jede Programmvariable wird vor ihrer Benutzung definiert (Beachte: Variablen in bedingten Sprunganweisungen werden dort benutzt) π heisst standardmarkiert, falls α_{i} = i : α‘_{i} für i = 1, …, q und L_{q} ⊆ {1, …, q + 1} Marken von π

\overline{Bsp} Fakultät (Folie) π^{f} berechnet die Fakultät

4.2 Semantik von IC

Sei π = (V list, Alist) ∈ IC, o.B.d.A. sei π standardmarkiert Das Flussdiagram von π (Semantik der Kontrolle) Alist = 1 : α_{1}; …; q : α_{q}

[figure: •; i; i : v ← e ↦; v ← e; •; i + 1; •; i; i: goto j ↦; •; j]

[figure: •; i; i: if be goto j ↦; be; •; 1; j; •; 0; i + 1; Ferner:; in x_{1}, …, x_{n}; •; 1; und:; •; q + 1; out y_{1}, …, y_{n}]

Das Flussdiagram von π ergibt sich durch Verkleben der entsprechenden Teilgraphen (lokale Variablen ergeben sich indirekt …) Fixpunktsemantik Sei 𝔞 = ⟨A; φ⟩ eine Interpretation für π d.h. π(f^{()}) = p_{𝔞} : A^{n} → {0, 1} V_{π} := {v_{1}, …, v_{s}} Zustandsraum Z := A^{s}\overline{a} = (a_{1}, …, a_{s}) als Wert des Variablenvektor \overline{v} = (v_{1}, …, v_{s}) Für die Fortsetzungsfunktionen (“Continuations“) φ_{i} : Z → Z(i = 1, …, q + 1) die von Programmmarke i bis zum Programmende berechnet Zustandstransformation, gelten folgende Gleichungen:

• α_{i} = v_{j} ← e

[figure: •; i; i : v ← e ↦; v_{j} ← e; •; i + 1; •; q + 1] } φ_{i}

↷ φ_{i}(σ) = φ_{i+1}(σ[j/[e]σ])

• α_{i} \overline{goto} l ↷ φ_{i}(σ) = φ_{l}(σ)

• α_{i} = \overline{if} be \overline{goto} l ↷ φ(σ) = \overline{if} [be]σ \overline{then} φ_{l}(σ) \overline{else} φ_{i+1}(σ)

[12.11.2004]

Fixpunktsemantik für π ∈ IC

π = (V list, Alist) 𝔞 = ⟨A; φ⟩ V_{φ} = {v_{1}, …, v_{s}} Z := A^{s} \overline{a} = (a_{1}, …, a_{s}) ∈ Z Alist = 1 : α_{1}; …; q : α_{q} Fortsetzungsfunktionen

• α_{i} = v_{j} ← e φ_{i}(\overline{a}) = φ_{i+1}(\overline{a}[j]/[e]\overline{a})

• α_{i} = \overline{goto} l φ_{i}(\overline{a}) = φ_{e}(\overline{a})

28KAPITEL 4. 4 DATENFLUSSANALYSE UND OPTIMIERUNG ITERATIVER PROGRAMME

• α_{i} = \overline{if} be \overline{goto} l

[figure: •; i; be; •; l; 1; φ_{l}; •; i + 1; 0; φ_{i+1}] φ_{1}(\overline{a}) = \overline{if} [be]\overline{a} \overline{then} φ_{e}(\overline{a}) \overline{else} φ_{i+1}(\overline{a}) und

φ_{q+1}(\overline{a}) = \overline{a}

Die φ_{1}, …, φ_{q+1} : A^{s} → A^{s} bilden daher die Lösung eines Gleichungssystems:

• F_{i}(\overline{v} = τ_{i}(i = 1, …, q + 1) mit

t_{i} = \begin{cases}F_{i+1}(\overline{v}[v_{j}/e], & falls α_{i} = v_{j} ← e \\ F_{l}(\overline{v}, & falls α_{i} = \overline{goto} l \\ \overline{if} be \overline{then} F_{l}(\overline{v}) \overline{else} F_{i+1}(\overline{v}), & falls α_{i} = \overline{if} be \overline{goto} l \end{cases}

τ_{q+1} = \overline{v} Berücksichtigung von Ein- / Ausgabe: Sei V list = \underline{in}x_{1}, …, x_{n}; \underline{out}y_{1}, …, y_{n}; \underline{loc}z_{1}, …, z_{p}

\overline{x} = (x_{1}, …, x_{n}) (\overline{x}, \overline{a}_{0}) = \underbrace{(x_{1}, …, x_{n}, a_{0}, …, a_{0})}_{s}

\overline{y} = (y_{1}, …, y_{m}) Das Gleichungssystem (E_{π}) ist dann definiert durch

(E_{π}) \begin{cases}F (\overline{x}) = F_{1}(\overline{x}, \overline{a}_{0}) a_{0} ∈ A beliebig \\ F_{i}(\overline{v}) = τ_{i} i = 1, …, q \\ F_{q+1}(\overline{v}) = \overline{y} \end{cases}

Lösungstyp: f : A^{n} → A^{m}f_{i} : A^{s} → A^{m}

Beispiel 4.2.1: Fakultätsprogramm

(E_{π})F (x) = F_{1}(x, 12, 12)
F_{1}(x, y, z) = F_{2}(x, y, 0)
F_{2}(x, y, z) = F_{3}(x, 1, z)
F_{3}(x, y, z) = \overline{if} x = z \overline{then} F_{7}(x, y, z) \overline{else} F_{4}(x, y, z)
F_{4}(x, y, z) = F_{5}(x, y, z + 1)
F_{5}(x, y, z) = F_{6}(x, y ∗ z, z)
F_{6}(x, y, z) = F_{3}(x, y, z)
F_{7}(x, y, z) = y

→ F (x) = F_{3}(x, 1, 0) F_{3}(x, y, z) = \overline{if} x = z \overline{then} y \overline{else} F_{3}(x, y ∗ (z + 1), z + 1)

→ Endrekursive Funktionsgleichungen (“tail recursive“) Funktionsaufrufe nur in Termspitze, keine Rücksprünge

a) Reduktionssymantik (operationale Semantik)

F (3) → F_{3}(3, 1, 0) → F_{3}(3, 1, 1) → F_{3}(3, 2, 2) → F_{3}(3, 6, 3) → 6

\underline{fac}(3) = 1 ∗ 2 ∗ 3 = 6

b) Fixpunktsemantik

Der Funktionenraum (Lösungsraum) F R_{π} := P F (A^{n}, A^{m})×P F (A^{s}, A^{m})^{q+1} ist eine vollständige Halbordnung.

Die Gleichungstransformation (“Einsetzungsfunktional“) T_{π} : F R_{π} → F R_{π} ist wie folgt definiert:

für \overline{φ} = (φ, φ_{1}, …, φ_{q+1}) ∈ F R_{π} und \overline{F} = (F, F_{1}, …, F_{q+1}) bezeichne τ_{i}[\overline{F} /\overline{φ}] die Ersetzung der Funktionsvariablen aus \overline{F} durch die entsprechenden Funktionen aus \overline{φ}

Damit:

T_{π}(\overline{φ}) := (λ\overline{x}, φ_{1}(\overline{x}, \overline{a}_{0}), λ\overline{v}.τ_{1}[\overline{F} /\overline{φ}], …, λ\overline{v}.τ_{q}[\overline{F} /\overline{φ}], λ, \overline{v}, \overline{y})

Beachte: \overline{φ} ist Lösung von E_{π} gdw. \overline{φ} = T_{π}(\overline{φ})

T_{π} ist stetig und besitzt daher einen kleinsten Fixpunkt \underline{fix}(T_{π}). Seine 1. Komponente [π]_{fix} := \underline{proj}_{1}(\underline{fix}(T_{π})) : A^{n} → A^{m} = \underline{proj}_{1}(⨆\{T_{π}^{i}(⊥)|i ∈ ℕ}) ⊥ = (f_{∅}, f_{1_{∅}}, …, f_{q+1_{∅}}) heisst Fixpunktsemantik von π

[17.11.2004]

Bsp Fakultätsprogramm F (x) = G(x, 1, 0) G(x, y, z) = \overline{if} x = z \overline{then} y \overline{else} G(x, y ∗ (z + 1), z + 1) F R_{π_{f}} = P F (ℤ, ℤ) × P F (ℤ^{3}, ℤ) ⊥ = (f_{∅} = λx., g_{∅} = λ(x, y, z).) T (⊥) = (f_{∅} = λx., λ(x, y, z). \overline{if} x = z \overline{then} y) T^{2}(⊥) = (λx. \overline{if} x = 0 \overline{then} 1, λ(x, y, z). \overline{if} x = z \overline{then} y \overline{if} x = z + 1 \overline{then} y ∗ (z + 1))

T^{3}(⊥) =(λx. \overline{if} x = 0 \overline{then} 1λ(x, y, z).  \overline{if} x = z \overline{then} y
\overline{if} x = 1 \overline{then} 1)  \overline{if} x = z + 1 \overline{then} y ∗ (z + 1)
\overline{if} x = z + 2 \overline{then} y ∗ (z + 1) ∗ (z + 2)
T^{n+1}(⊥) =(λx. \overline{if} x ≤ n − 1 \overline{then} x‘,
(λ(x, y, z). \overline{if} x = z \overline{then} y
\overline{if} z + 1 \overline{then} y ∗ (z + 1)
\overline{if} z + n \overline{then} y ∗ (z + 1) ∗ (z + 2) ∗ … ∗ (z + n)

Also: [π]_{fix}(x) = \overline{if} x ≥ 0 \overline{then} x!

Folgerungen der Semantik von IC-Programmen

1. Eine Anweisung kann wiederholt werden, evtl. unendlich oft (Programmschleifen)

2. Ein Programmpfad (einen eingabeunabhängiger Pfad im Flussdiagramm vom eingabe- zum Ausgabeknoten) muss kein Berechnungspfad sein (eingabeunabhängiger Pfad einer Berechnung)

Bsp

[figure: be; 1; 0; be; 1; 0; a! R, L | a? q a b R q‘; •; q; a_{1}^{1}; a_{2}; b!; R; •; q‘]

3. TM als IC-Programme

4. Programmäquivalenz nicht entscheidbar

→ Programmanalyse: Approximation von Programmeigenschaften, Prädikate ignorieren, Programmpfade betrachten

• Menge der Programmpfade von π ∈ IC ist regulär.

• Menge der Berechnungspfade ist i. a. rekursiv aufzählbar, aber nicht entscheidbar

⇒ sichere, aber evtl. unvollständige Optimierungsinformationen.

4.3 Flussgraphen von IC-Programmen

Idee: deterministische Verzweigung durch nicht-deterministische Auswahl ersetzen; Programmpfade statt Berechnungspfade Sei π = ⟨V list, Alist⟩ ∈ IC und Alist = 1 : α_{1}; …; q : α_{q}

1. SI-Graph (SI = Single Instruction) G_{π}^{SI} = ⟨\underline{Kno}, \underline{Kan}, s⟩ \underline{Kno} := \{α_{i}|α_{i} = x ← e, 1 ≤ i ≤ q\}u ∪ \{be|α_{i} = \overline{if} be \overline{goto} j, 1 ≤ i, j ≤ q\} s = α_{1} (o.B.d.A α_{1} Wertzuweisung) Kan wie im Flussdiagramm

2. BB - Graph (BB = basic block) Ziel: Vereinfachung der Programmanalyse Idee: Zerlegung von π in maximale SLC-Blöcke Konstruktion von G_{π}^{BB} = ⟨\underline{Kno}, \underline{Kan}, s⟩ : α_{i} heisst Blockanfang, falls eine der folgenden Bedingungen gilt:

• i = 1

• i ist Sprungziel von π (kommt als goto i in π vor)

• α_{i−1} ist Sprunganweisung Ein Blockanfang α_{i} bestimmt α_{i}; α_{i+1}; …; α_{j} als längste Anweisungsfolge ohne weiteren Blockanfang. Weglassen von goto k und ersetzen von if be goto k durch be ergibt den Basisblock α_{i_{1}}‘; …, α_{i_{k}}‘ Bsp π_{f} Blockanfänge α_{1}, α_{3}, α_{4} β_{1} = α_{1}; α_{2} β_{2} = α_{3}

β_{3} = α_{4}, α_{5} [19.11.2004]

[Folie: ??? von π_{f}]

[Folie: Beispiel: BB- und SI-Graph]

Flussgraphen von IC-Programmen (Korrektur)

1. SI-Graphen π = 1 : α_{1}; …; q : α_{q} G_{π}^{SI} = ⟨\underline{Kno}, \underline{Kan}, s⟩ und lab: Kno → Wertzuweisungen ∪ Bool. Exp. ∪ {ST ART } \underline{Kno} := \{i|0 ≤ i ≤ q, α_{i} ≠ \overline{goto} j\} \underline{lab}(0) = ST ART

\underline{lab}(i) = \begin{cases}α_{i}, & falls α_{i} = x ← e \\ be, & falls α_{i} \overline{if} be \overline{goto} j \end{cases}

1 ≤ i ≤ q; s := 0 Kan folgen aus Flussdiagram von π { START → 2. BB-Regel

G_{π}^{BB} = ⟨\underline{Kno}, \underline{Kan}, s⟩

siehe letzte Vorlesung

Kno = Basisblöcke + Startblöcke

3. Flussgraphen für die Rückwärtsanalyse

GSI ; π^{←}, GBB ; π^{←} Kanten invertieren

STOP-Knoten des Flussdiagrams als Startknoten

4.4 Datenflussanalyse-Systeme

2 Komponenten:

• ein Flussgraph als Abstraktion eines Flussdiagrams (Programmpfade)

• eine abstrakte Interpretation:

Analyseinformation als Element eines vollständigen Verbands mit ACC

Informationstransformationen als monotone Abbildungen

Definition 4.4.1: Sei Kno eine nicht-leere endliche Menge von Knoten; \overline{Kan} ⊆ \overline{Kno} × \overline{Kno} eine Menge von Kanten und s ∈ \overline{Kno} ein Startknoten. Für k ∈ \overline{Kno} bezeichne \overline{Var} (k) := \{k‘ ∈ \overline{Kno} |(k‘, k) ∈ \overline{Kan}\} die Menge der (direkten) Vorgängerknoten. Für k, k‘ ∈ \overline{Kno} bezeichne \underline{P fad}[k, k‘) := \{(k_{1}, …, k_{r})|k_{1} = k, k_{r} ∈ \overline{Var}(k‘) und (k_{i}, k_{i+1}) ∈ \overline{Kan} für i = 1, …, r − 1} die Menge der Pfade von k zu einem direkten Vorgängerknoten von k‘. G = ⟨\underline{Kno}, \underline{Kan}, s⟩ heisst Flussgraph, falls \underline{V ar}(s) = ∅.

Folgerung 4.4.1:

Für π ∈ IC sind G_{π}^{SI}, G_{π}^{BB}, GSI ; π^{←}, GBB ; π^{←} Flussgraphen

Definition 4.4.2: Abstrakte Interpretation eines Flussgraphen Sei G = ⟨\underline{Kno}, \underline{Kan}, s⟩ ein Flussgraph. Sei D = ⟨D; ≤⟩ ein vollständiger Verband mit ACC d_{s} ∈ D eine Startinformation und φ : \underline{Kno} → \{f|f : D → f monoton\} mit φ(s) = \overline{id}_{D} Dann heisst ℑ = ⟨D, φ, d_{s}⟩ eine abstrakte Interpretation von G

Definition 4.4.3: DFA-System Ist G ein Flussgraph und ℑ eine abstrakte Interpretation von G, so heisst Δ = ⟨G, ℑ⟩ ein DFA-System (bei Indermark, in der Literatur: “monotone framework“) ein DFA-System bestimmt in natürlicher Weise eine MOP-Lösung (meet over all paths) sowie eine MFP-Lösung (maximal fixed-point) Nachtrag: φ_{k}(d) = φ(k)(d)

Definition 4.4.4: Die MOP-Lösung eines DFA-Systems Sei Δ = ⟨G, ℑ⟩ ein DFA-System Für k ∈ \overline{Kno} und p = (k_{1}, …, k_{r}) ∈ \overline{Pfad} [s, k) definieren wir die Analyseinformation von k bzgl. p AI_{k}^{p} := φ_{k_{r}}(φ_{k_{r−1}} … (φ_{k_{1}}(d_{s}) …) Dann ist die MOP-Lösung für k die folgende Analyseinformation AI_{R}^{MOP} := ⨆\{AI_{k}^{p}|p ∈ \overline{Pfad} [s, k)\} für k ≠ s und AI_{s}^{MOP} := d_{s} AI^{MOP} := (AI_{k}^{MOP} |k ∈ \overline{Kno}) heisst MOP-Lösung von Δ

Bem Die MOP-Lösung AI^{MOP} ist im allgemeinen nicht berechenbar.

Definition 4.4.5: Die MFP-Lösung eines DFA-Systems Sei Δ = ⟨G, ℑ⟩ ein DFA-System. Δ bestimmt ein System E_{Δ} von Datenflussgleichungen

(E_{Δ}) \begin{cases}X_{s} = d_{s} \\ X_{k} = ⨆\{φ_{i}(X_{i})|i ∈ \overline{Var} (k)\}, & k ∈ \overline{Kno} /\{s\} \end{cases}

[24.11.2004]

E_{Δ} bestimmt eine Gleichungstransformation T_{Δ} : D^{n} → D^{n} T_{Δ}(A_{1}, …, a_{n}) := (a_{s}, ⨆\{φ_{i}(a_{i})|i ∈ \overline{Var} (2), …, ⨆\{φ_{i}(a_{i})|i ∈ \overline{Var} (n)) und die MFP-Lösung von Δ AI^{MF P} := \overline{fix} (T_{Δ}) ∈ D^{n} Beachte: D = ⟨D, ≤⟩ vollständiger Verband mit ACC. φ_{i} : D → D monoton ↷ φ_{i} stetig ↷ T_{Δ} stetig und wegen ACC existiert m ∈ ℕ mit \overline{fix} (T_{Δ}) = T_{Δ}^{m}(⊥)inD^{n} Also: AI^{MF P} in endlich vielen Schritten berechenbar.

Satz 4.4.6: Correctness-Theorem In einem DFA-System Δ gilt: AI^{eigentl.} ≤ AI^{MOP} ≤ AI^{MF P} Beweis: Es genügt zu zeigen, dass für alle 1 < k ≤ n, p ∈ \overline{Pfad} [1, k) und a = (a_{1}, …, a_{n}) mit a = T_{Δ}(a) gilt: (*) AI_{r}^{p} ≤ a_{k} (*) ↷ Beh.: AI_{i}^{MOP} = d_{1} = AI_{1}^{MF P} k ≠ 1 AI_{k}^{p} ≤ AI_{k}^{MF P} nach (*) wegen Fp-Eigenschaft von AI^{MF D}, also: AI_{k}^{MOP} ≤ AI_{k}^{MF D} Beweis von (*): Aus (E_{Δ}) und a = T_{Δ}(a) (**) φ_{i}(a_{i}) ≤ a_{k} für 1 < k ≤ n und i ∈ \overline{Var} (k) Wir zeigen (*) durch Induktion über die Länge r von p r = 1: Dann muss p = 1 ∈ \overline{Var} (k), so dass nach (**)

AI_{k}^{p} = φ_{1}(a_{1}) ≤ a_{k} rr̃ + 1: Sei p ∈ \overline{Pfad} [1, k) mit Länge r + 1.

p = p‘ ∗ i mit i ∈ \overline{Var} (k), i ≠ 1 (wegen \overline{Var} (1) = ∅) und p‘ ∈ \overline{Pfad} [1, i) [Grafik] Nach IV: AI_{i}^{p‘} ≤ a_{i} und nach (**) φ_{i}(a_{i}) ≤ a_{k} Aus beiden Ungleichungen un der Monotonie von φ_{i} folgt: AI_{k}^{p} = φ_{i}(AI_{i}^{p‘}) ≤ φ_{i}(a_{i}) ≤ a_{R} [/Grafik]

□

Satz 4.4.7: Compleetness Theorem, Coincidence Theorem Sind in einem DFA-System Δ die Funktion φ_{k} : D → D distributiv (φ_{k}(a ⨆ b) = φ_{k}(a) ⨆ φ_{k}(b)), so gilt: AI^{MOP} = AI^{MF P} Beweis: Es bleibt zu zeigen, dass a = (a_{i}, …, a_{n}) := (AI_{1}^{MOP} , … AI_{n}^{MOP}) ein Fixpunkt von T_{Δ} ist: a = T_{Δ}(a) T_{Δ}(a) = (d_{s}, ⨆_{i∈ \overline{Var} (2)} φ_{i}(a_{i}), …) = (d_{s}, ⨆_{i∈ \overline{Var} (2)} φ_{i}(AI_{i}^{MOP}), …) = (d_{s}, ⨆_{i∈ \overline{Var} (2)} φ_{i}(⨆_{p∈ \overline{Pfad} [1,i)}), …) = ldots φ_{i} distr + ACC ⇒ φ(⨆ T) = ⨆ φ_{i}(T)

[26.11.2004] Nachtrag: Kleinster Fixpunkt

[figure: x = 0; x ← x − 1; 0; STOP; 1]  F (x) = \overline{if} x = 0 \overline{then} 0 \overline{else} F (x − 1)

a) oper. Semantik a ∈ ℤ:

a ≥ 0: F (a) → F (a − 1) → F (a − 2) … F (0) → 0 a < 0: F (a) → F (a − 1) → …

[π]_{op} = λx. \overline{if} x ≥ 0 \overline{then} 0 [π]_{op}(x) = \overline{if} x ≥ 0 \overline{then} 0 b) Fp-Semantik λx.

λx. \overline{if} x = 0 \overline{then} 0 λx. \overline{if} x = 0 \overline{then} 0 \overline{else} \overline{if} x = 1 \overline{then} 0 [π]_{fix} = λx. \overline{if} x ≥ 0 \overline{then} 0 Weitere Fp: λx. \overline{if} x ≥ 0 \overline{then} 0 \overline{else} A

Nachtrag zu Kap 3: Lemma 4.4.8: Sei D = ⟨D, ≤⟩ ein vollständiger Verband mit ACC und f : D → D. Dann gilt: f distributiv (f(a ⨆ b) = f(a) ⨆ f(b)) ↷ f(⨆ T) = ⨆ f(T) für alle T ⊆ D, T ≠ ∅ Beweis: Sei T ⊆ D, T ≠ ∅.

1. f distributiv ↷ f monoton ↷ f(T) ≤ f(⨆ T) ↷ ⨆ f(T) ≤ f(⨆ T)

2. Bleibt zu zeigen: f(⨆ T) ≤ ⨆ f(T)

(*) Es existiert eine endliche Teilmenge T_{e} ⊆ T mit ⨆(Z) ≤ ⨆ T_{e} Konstruktion einere Kette in D: a_{0} ≤ a_{1} ≤ … a_{0} ∈ T beliebig a_{1} → a_{n+1} :

(a) T ≤ a_{n} a_{n+1} := a_{n} (also: a_{n+k} = a_{n})

(b) T ≰ a_{n} Dann existiert b_{n} ∈ T mit b_{n} ≰ a_{n} a_{n+1} := a_{n} ⨆ b_{n}(a_{n} < a_{n+1})

ACC ↷ a_{0} < a_{1} < … < a_{n} = a_{n+1} = a_{n+2} a_{n} = a_{0} ⨆ a_{0} ⨆ b_{0} ⨆ b_{1} ⨆ … ⨆ b_{n}

und T ≤ a_{n}, somit ⨆ T ≤ a_{n} = ⨆\{\underbrace{a_{0}, b_{n}, …, b_{n}}_{=T_{e}}\}

Damit folgt die Behauptung: f(⨆ T) ≤ f(a_{n}) = f(a_{0} ⨆ b_{1} ⨆ b_{2} … ⨆ b_{n}) = f(a_{0}) ⨆ f(b_{1}) ⨆ … f(b_{n}) = ⨆{f(a_{0}), f(b_{1}), … f(b_{n})} ≤ ⨆ f(T).

Lemma 4.4.9: Doppelt indizierte Mengen D = ⟨D; ≤⟩ vollständiger Verband T = {a_{i_{j}}|i ∈ I, j ∈ J} ⊆ D ⨆_{i∈I,j∈J} a_{i_{j}} = ⨆_{i∈I} ⨆_{j∈J} a_{i_{j}} Beweis: trivial

Satz 4.4.7: (Fortsetzung)

AI_{2}^{p∗i} = φ_{i}(AI_{i}^{p}) = (d_{s}, ⨆_{i∈ \overline{Var} (2),p∈ \overline{Pfad} [1,i)} AI_{k}^{p∗i}, …) = (d_{s}, ⨆_{p‘∈ \overline{Pfad} [1,2)} AI_{k}^{p‘}, …, ⨆_{p‘∈ \overline{Pfad} [1,n)} AI_{n}^{p‘}) = (a_{1}, …, a_{n}) = a □

[Folie: Beispiel: Common Subexpression Elimination] [01.12.2004]

4.5 AE-Analyse und CS-Elimination für IC-Programme

Ziel: Vermeidung wiederholter Auswertung von Ausdrücken Beachte: Ein Ausdruck ist für eine Anweisung verfügbar, wenn er auf jedem Berechnungspfad zu diese Anweisung berechnet wird und die Werte dieser Variablen danach nicht verändert werden.

AE-Analyse Zerlegung der Analyse mit Hilfe von Basisblöcken in 1. Globale Analyse für BB-Graph

2. Lokale Analyse für Basisblöcke Aufgabe (für 1): Konstruktion eines geeigneten DFA-Systems Δ = ⟨G, ℑ⟩ zu π ∈ IC

[Folie: Beispiel: Common G = BB-Graph für π für Vorwärtsanalyse Subexpression Elimination]

ℑ = ⟨D, φ, d_{s}⟩ Programmausdrücke: \overline{OpExp}_{π} := \{e|e = f(u_{1}, …, u_{r}), α_{i} = x ← e\}∪\{be|be = p(u_{1}, …, u_{r}), α_{i} = \overline{if} be \overline{goto} …, r ≥ 1\} = \{e_{1}, … e_{t}\} D := 𝔹 zur Darstellung von Teilmengen von \underline{OpExp}_{π} \overline{b} = (b_{1}, …, b_{t})

b_{i} = \begin{cases}0, & falls e_{i} verfügbar \\ 1, & sonst \end{cases}

\overline{b} ≤ \overline{b}‘ :↶↷ b_{i} ≤ b‘_{i} i = 1, …, t (0 < 1) ⊥ = (0, …, 0) “beste Information“ ⊤ = (1, …, 1) 0 ⊔ 1 = 1 (b_{1}, …, b_{t}) ⊔ (b‘_{1}, …, b‘_{t}) = (b_{1} ⊔ b‘_{1}, …, b_{t} ⊔ b‘_{t}) — d_{s} = (1, …, 1) — 4.5. AE-ANALYSE UND CS-ELIMINATION FÜR IC-PROGRAMME 37

Konstruktion von φ : \overline{Kno} → \{f : 𝔹^{t} → 𝔹^{t}|monoton\} Zunächst für einzelne Anweisungen, dann für Blöcke: α ∈ \overline{Anw} ↦ φ_{α} : 𝔹^{t} → 𝔹^{t}

– φ_{x←e} := kill_{x} ∘ gen_{e} gen_{e}(b_{1}, …, b_{t}) := (b‘_{1}, …, b‘_{t})

b‘_{i} = \begin{cases}0, & falls e = e_{i} \\ b_{i}, & sonst \end{cases}

kill_{x}(b_{1}, …, b_{t})

b‘_{i} = \begin{cases}1, & falls x ∈ V_{e_{i}} \\ b_{i}, & sonst \end{cases}

– φ_{gotok} := \overline{id}_{𝔹^{t}}

– φ _{\overline{if} be \overline{goto} k} := gen_{be}

Beachte: φ_{α} monoton, weil alle gen- und kill-Funktionen monoton sind Konstruktion der Blocktransformationen β = α_{1}; …; α_{k} (k > 0, weil Sprungbefehle bleiben) φ_{β} := φ_{α_{k}} ∘ … ∘ φ_{α_{1}} monoton Für dieses DFA-System Δ = ⟨G, ℑ⟩ gilt: AE_{β}^{MOP} = AE_{β}^{MF P} für alle β ∈ \overline{Kno} (AE “available expression“ statt AI “Analyseinformation“) → distributive Funktionen! Grund: alle φ_{β} sind distributiv gen_{e_{i}}(b) ⊔ gen_{e_{i}}(b‘) = (b_{1}, … \frac{0}{i} … b_{t}) ⊔ (b‘_{1}, … \frac{0}{i} … b‘_{t}) gen_{i}(b ⊔ b‘) = (b_{1}, ⊔b‘_{1}, … \frac{0}{i} … b_{t} ⊔ b‘_{t}) \overline{OpExp}_{π} := \{\underbrace{x + y} 1, \underbrace{x ∗ z} 2, \underbrace{t ∗ t} 3, \underbrace{z ∗ 2} 4, \underbrace{i + 1} 5, \underbrace{z > t} 6, \underbrace{i > 0} 7\}

D = 𝔹^{7} φ_{1}(b_{1}, … b_{7}) = (b_{1}, …, b_{7}) φ_{2}(b_{1}, … b_{7}) = (0, 0, 0, 1, 1, 1, 1) φ_{3}(b_{1}, … b_{7}) = (0, 1, b_{3}, 1, b_{5}, 0, b_{7}) φ_{4}(b_{1}, … b_{7}) = (b_{1}, 0b_{3}, … b_{7}) φ_{5}(b_{1}, … b_{7}) = (b_{1}, b_{2}, 0, …, b_{7}) φ_{6}(b_{1}, … b_{7}) = (b_{1}, … b_{4}, 1, b_{6}, b_{7})

(E_{Δ}) \begin{cases}X_{1} = (1, …, 1) \\ X_{2} = X_{1} \\ X_{3} = (0, 0, 0, 1, 1, 1, 1) ⊔ φ_{6}(X_{6}) \\ X_{4} = φ_{3}(X_{3}) \\ X_{5} = φ_{3}(X_{3}) \\ X_{6} = φ_{4}(X_{4}) ⊔ φ_{5}(X_{5}) \end{cases}

Vereinfachung: X_{3} = (0, 0, 0, 1, 1, 1, 1) ⊔ φ_{6}([φ_{4} ⊔ φ_{5}]φ_{3}(X_{3}))

\underline{φ_{6}([φ_{4} ⊔ φ_{5}]φ_{3}}(b_{1}, …, b_{7}) = (0, 1, b_{3}, 1, 1, 0, 0)

Fixpunkt-Iteration für (*) beginnt mit dem besten Wert ⊥ = (0, …, 0) ∈ 𝔹^{7}

T_{(∗)}^{1}(⊥) = (0, 1, 0, 1, 1, 1, 1) = T_{(∗)}^{2}(⊥)

[08.12.2004] [Folie: Beispiel: Common Subexpression Elimination] Fixpunkt-Iteration für (*): ⊥ = (0, …, 0) ∈ 𝔹^{7} T_{(∗)}(⊥) = (0, 0, 0, 1, 1, 1, 1) ⊔ (0, 1, 0, 1, 1, 0, 0) = (0, 1, 0, 1, 1, 1, 1) T_{(∗)}(⊥) = (0, 0, 0, 1, 1, 1, 1) ⊔ (0, 1, 0, 1, 1, 0, 0) = (0, 1, 0, 1, 1, 1, 1) \overline{fix}(T_{(∗)}) = (0, 1, 0, 1, 1, 1, 1) Ergebnis: AE_{1} = (1, …, 1) AE_{2} = (1, …, 1) AE_{3} = (0, 1, 0, 1, 1, 1, 1) AE_{4} = (0, 1, 0, 1, 1, 0, 1) AE_{5} = (0, 1, 0, 1, 1, 0, 1) φ_{3}(b_{1}, …, b_{7}) = (0, 1, b_{3}, 1, b_{5}, 0, b_{7}) φ_{4}(b_{1}, …, b_{7}) = (b_{1}, 0, b_{3}, …) φ_{5}(b_{1}, …, b_{7}) = (b_{1}, b_{2}, 0, b_{4}, …) → AE_{6} = AE_{4} = (0, 1, 0, 1, 1, 0, 1)

Folgerung 4.5.0: x + y, t ∗ t verfügbar in Block 3, 4, 5, 6 z > t verfügbar in Block 4, 5, 6

Beachte:

1. Gabs schon... x ∗ z bereits füer B3 nicht verfügbar, weil B3 von B2 und B6 erreichbar (Ohne B5 wäre x ∗ z für B3 verfügbar)

2. Lokale analysen für Basisblöcke

Unterschied zur AE-Analyse an SLC-Programmen

Neue Startinformationen: nicht mehr (1, …, 1)

sondern die durch globale Analyse gewonnenen Informationen AE_{i} für Block i (i = 1, …, 6 im Beispiel)

• CS-Elimination T_{CS} : SLC → SLC übertragen Zwischenspeichern auf temporären Variablen

4.6 RD-Analyse und Konstantenfaltung

Ziel: Ersetze konstante Variablen und konstante Ausdrücke auf rechten Seiten von Wertzuweisungen und in Bedingungen durch ihre Werte (Propagation und Faltung)

Definition 4.6.1: Sei π ∈ IC mit Interpretation 𝔞 = ⟨A, φ⟩, v ∈ V_{π}, i ∈ L_{π} und a ∈ A. Dann hat v bei i den konstanten Wert a (Bez.: konst(v, i) = a), falls dies auf jedem Berechnungspfad von i gilt.

Beachte i kann auf verschiedenen Berechnungspfaden (verschiedene Eingaben) und mehrfach auf einem Berechnungspfad erreicht werden.

Satz 4.6.2: Die Konstanzeigenschaft von Variablen eines π ∈ IC ist i.a. nicht entscheidbar (i.a. bei entsprechender Wahl der Interpretation) Beweis Angenommen, die Konstanz-Eigenschaft wäre für alle Interpretationen entscheidbar. Interpretation: 𝔞 = ⟨ℕ, \underline{+1}, \underline{0}, \underline{0?}⟩ IC(𝔞) universell (jede beliebige Funktion darstellbar) Sei π ∈ IC(𝔞), IV_{π} = {x_{1}, …, x_{n}}, OV_{π} = {y_{1}, …, y_{m}}

Neues Programm: π_{const} ∈ IC(𝔞):

[figure: in x_{0}, …, x_{n}; x_{0} = 0; 0; 1; Δ list_{π}; y_{1} ← 0; y_{1} ← 1; out y_{1}, …, y_{n}]

Dann gilt: \overline{const}(y_{1}, i) = 0 ↷ π divergiert [10.12.2004] [Folie: Gleichungssystem????] [Folie: Nicht- ⊔ˆ=∩ entscheidbarkeit der Konstanzeigenschaft] const(y_{1}, 0) ↶↷ π divergiert, d.h. bei keiner Eingabe terminiert Entscheidbarkeit der Konstanzeigenschaft ↷ Entscheidbarkeit der Divergenz von π ↷ Entscheidbarkeit des Halteproblems von π

[Folie: Reaching Definitions (Modifikation von π durch Zuweisung der Eingabewerte an Eingabevariablen) Analyse und Konstantenfaltung] RD-Analyse Methode 2-stufige Berechnung

1. Bestimme für jeden Basisblock von π ∈ IC die Länge der am Blockanfang konstanten Variablen mit ihrem Wert (globale Analyse)

2. Bestimme aus dieser Information die entsprechenden Informationen für die Anweisungen der Basisblöcke

Zu (1): Konstruktion eines DFA-Systems Δ = ⟨G, ℑ⟩ Konstruktion von ℑ = ⟨D, d_{s}, φ⟩ v_{π} = {v_{1}, …, v_{k}}

Bsp: \{\underbrace{u}_{1}, \underbrace{u}_{1}, \underbrace{v}_{2}, \underbrace{x}_{3}, \underbrace{y}_{4}, \underbrace{z}_{5}\}

D = (a ∪ {⊥, ⊤}) … A d_{j} = a bedeutet: v_{j} hat den Wert d_{j} d_{j} = ⊤ bedeutet v_{j} hat mehrere Werte d_{j} = ⊥ bedeutet ? (irgendein Wert, unbekannt)

Beispiel 4.6.3: D = (ℤ, ∪{⊥, ⊤})^{5} (⊥, 4, 5, 6, 7) ⊔ (1, 4, 2, 1, 7) = (1, 4, ⊤, ⊤, 7)

d_{s} = (\underbrace{⊤, ⊤, …, ⊤}_{Eingabevar.}, \underbrace{⊥, …, ⊥}_{brigeV ar.}) Startinformation

Konstruktion der monotonen Blocktransformation φ_{i} : Â^{k} → Â Zunächst: Anweisungstransformation φ_{α} : Â^{k} → Â^{k} Dazu: erweitere Ausdrucksemantik (vgl. SLC) e ∈ V ∪ C ∪ {f(u_{1}, …, u_{r})|f ∈ Σ^{(r)}, u_{i} ∈ V ∪ C} d ∈ Â^{k} [e]_{𝔞}(d) ∈ Â wobei f_{𝔞}(…, ⊥, …) = ⊥ z.B. 3 + ⊥ = ⊥ f_{𝔞}(…, ⊤, …) = ⊤ z.B. 4 ∗ ⊤ = ⊤ f_{𝔞}(…, ⊤, …, ⊤, …) = ⊤ φ_{x←e}(d_{1}, …, d_{k}) = (d‘_{1}, …, d‘_{k})

d′_{j} = \begin{cases}[e]_{𝔞}(d_{1}, …, d_{k}), & falls x = v_{j} \\ d_{j}, & sonst \end{cases}

Blocktransformation: Komposition der Anweisungstransformationen

Beispiel 4.6.4:

V_{π} = \{\underbrace{u}_{1}, \underbrace{u}_{1}, \underbrace{v}_{2}, \underbrace{x}_{3}, \underbrace{y}_{4}, \underbrace{z}_{5}\}

φ_{1}(d_{1}, … d_{5}) = (d_{1}, …, d_{5}) φ_{2}(d_{1}, … d_{5}) = (d_{1}, d_{2}, 1, 1, 1) φ_{3}(d_{1}, … d_{5}) = (d_{1}, …, d_{5}) φ_{4}(d_{1}, … d_{5}) = (d_{3} + d_{4} + d_{5}, d_{2} … d_{5}) φ_{5}(d_{1}, … d_{5}) = (d_{1}, d_{2}, d_{4} + 2, d_{4}, d_{5}) φ_{6}(d_{1}, … d_{5}) = (d_{1}, …, d_{5}) φ_{i} monoton, weil alle erweiterten Grundfunktionen f̂_{𝔞} monoton

Bestimmung der MFP-Lösung von Δ = ⟨G, ℑ⟩ Datenflussgleichungen:

Beispiel 4.6.5:

(E_{Δ}) \begin{cases}X_{1} = d_{1} \\ X_{2} = φ_{1}(X_{1}) \\ X_{3} = φ_{2}(X_{2}) ⊔ φ_{6}(X_{6}) \\ X_{4} = φ_{3}(X_{3}) \\ X_{5} = φ_{4}(X_{4}) \\ X_{6} = φ_{4}(X_{4}) ⊔ φ_{5}(X_{5}) \end{cases}

X_{1} = (⊤, ⊤, ⊤, ⊤, ⊤) X_{2} = (⊤, ⊤, ⊤, ⊤, ⊤)

(∗)X_{3} = (⊤, ⊤, 1, 1, 1) ⊔ φ_{6}([φ_{4} ⊔ φ_{5} ∘ φ_{4}](X_{3})

X_{4} = X_{3} X_{5} = ϖ_{4}(X_{3}) X_{6} = [φ_{4} ⊔ φ_{5} ∘ φ_{4}](X_{3})

[φ_{5} ∘ φ_{4}](d_{1}, …, d_{5}) = (d_{3} + d_{4} + d_{5}, d_{2}, d_{4} + 2, d_{4}, d_{5}) φ_{4} ⊔ [φ_{5} ∘ φ_{4}](d_{1}, …, d_{5}) = (d_{3} + d_{4} + d_{5}, d_{2}, d_{3} ⊔ (d_{4} + 2), d_{4}, d_{5}) φ_{6}(φ_{4}⊔[φ_{5}∘φ_{4}])(d_{1}, …, d_{5}) = (d_{3}+d_{4}+d_{5}, (d_{3}⊔(d_{4}+2))+d_{4}, , d_{3}⊔(d_{4}+2), d_{4}, d_{5})

[08.12.2004]

[Folie: Reaching Definitions Analyse und Konstantenfaltung]

[Folie: RD^{MF P}: Transferfunktionen und Gleichungssystem] Fp-Iteration für Gleichung (*) T_{(∗)}(⊥, …, ⊥) = (⊥, …, ⊥) T_{(∗)}^{1}(⊥, …, ⊥) = (⊤, ⊤, 1, 1, 1) T_{(∗)}^{2}(⊥, …, ⊥) = (⊤, ⊤, ⊤, 1, 1) T_{(∗)}^{3}(⊥, …, ⊥) = (⊤, ⊤, ⊤, 1, 1) Also: \overline{fix}(T_{(∗)}) = (⊤, ⊤, ⊤, 1, 1) MFP-Lösung von Δ RD_{1}^{MF P} = (⊤, ⊤, …, ⊤) RD_{2}^{MF P} = (⊤, ⊤, …, ⊤) RD_{3}^{MF P} = (⊤, ⊤, ⊤, 1, 1) RD_{4}^{MF P} = (⊤, ⊤, ⊤, 1, 1) RD_{5}^{MF P} = (⊤, ⊤, ⊤, 1, 1) RD_{6}^{MF P} = (⊤, ⊤, ⊤, 1, 1)

Die Variablen y und z haben bei Eintritt in die Blöcke 3, 4, 5, 6 den konstanten Wert 1.

Lokale Analyse

SLC-Analyse von Block i mit der Startinformation RD_{i}^{MF P} (i = 1, …, k) hier k = 6 Optimierung Konstantenfaltung wie bei SLC Frage RD^{MOD} = RD^{MF P}? Knotentransformationen φ_{i} distributiv?

Satz 4.6.6: Es gibt ein π ∈ IC mit RD^{MOP} ≠ RD^{MF P}

[Folie: RD^{MOP} ≠ RD^{MF P}] Beweis: V_{π} = {x, y, z} D = ℤ̂^{3} φ_{1}(d_{1}, d_{2}, d_{3}) = (d_{1}, d_{2}, 0) φ_{2}(d_{1}, d_{2}, d_{3}) = (2, 3, d_{3}) φ_{3}(d_{1}, d_{2}, d_{3}) = (3, 2, d_{2}) φ_{4}(d_{1}, d_{2}, d_{3}) = (d_{1}, d_{2}, d_{1} + d_{2}) RD_{5}^{MOP} = (2, 3, 5) ⊔ (3, 2, 5) = (⊤, ⊤, 5)

RD^{MF P} X_{1} = (⊤, ⊤, ⊤)
X_{2} = φ_{1}(X_{1}) = (⊤, ⊤, 0)
X_{3} = φ_{1}(X_{1}) = (⊤, ⊤, 0)
X_{4} = φ_{2}(X_{2}) ⊔ φ_{3}(X_{3}) = (2, 3, 0) ⊔ (3, 2, 0) = (⊤, ⊤, 0)
X_{5} = φ_{4}(X_{4}) = (⊤, ⊤, ⊤)

Also: RD_{5}^{MF P} = (⊤, ⊤, ⊤) ≠^{>} RD_{5}^{MOP}

□ Grund: φ_{4} nicht distributiv φ_{4}(d ⊔ d‘) ≠ φ_{4}(d) ⊔ φ_{4}(d‘) für d = (2, 3, z) d‘ = (3, 2, z) Insgesamt gilt: falls Block 2 bei z = 0 Sprungziel RD_{5} = (2, 3, 5) < RD_{5}^{MOP} < RD_{5}^{MF P}

[Folie: Nicht-Entscheidbarkeit der Konstanteninformationen Rl] Satz 4.6.7: Die Pfaddefinierten Konstanteninformationen RD_{i}^{MOP} (i = 1, …, k) sind i.a. nicht entscheidbar. Beweis: Wären die Mengen RD_{i}^{MOP} immer entscheidbar, so auch das MPCP (“modifiziertes Postsches Korrespondenzproblem“) und damit das PCP. MPCP: sei Σ Alphabet, n ∈ ℕ und u_{1}, v_{1}, …, u_{n}, v_{n} ∈ Σ^{∗} Gibt es i_{1}, …, i_{m} ∈ {1, …, n}, m ≥ 1 mit i_{1} = 1 (“modifiziertes PCP“), so dass u_{i_{1}}u_{i_{2}}u_{i_{3}} … v_{i_{n}} = v_{i_{1}}v_{i_{2}} … v_{i_{m}} Es gilt (z.B. Schöning, Theoretische Informatik): Das MPCP ist nicht entscheid-

[Folie: Nicht- bar Entscheidbarkeit der Knonstanteninformationen RL] mit der Interpretation ⟨A; φ⟩

A := Σ^{∗} φ(++)(u, v) := uv
φ(=)(u, v) := \begin{cases}E falls u ≠ v \\ a falls u = v (a ∈ Σ) \end{cases}

Dann folgt: Jeder Pfad von Startknoten nach k entspricht einer Indexfolge i_{1}, …, i_{m} mit i_{1} = 1 und umgekehrt Also: RD_{k}^{MOP} (Z) = E ↶↷ MP CP (u_{1}, v_{1}, … u_{n}, v_{n}) hat keine Lösung. Somit: Entscheidbarkeit der RD_{i}^{MOP} ↷ Entscheidbarkeit von MP CP (u_{1}, v_{1}, … u_{n}, v_{n}) Widerspruch ⚡ □

Zusammenfassung:

1. RD ≤ RD^{MOP} ≤ RD^{MF P}

2. RD < RD^{MOP} < RD^{MF P}

3. RD und RD^{MOP} i.a. nicht entscheidbar

4.7 Effiziente Fp-Berechnung

Δ DFA-System T_{Δ} : D^{n} → D^{n} MFP-Lösung von Δ AI^{MF P} = \overline{fix}(T_{Δ}) ∈ D^{n} T_{Δ} stetig ↷ \overline{fix}(T_{Δ}) = ⨆_{i=0}^{∞} T_{Δ}^{i}(⊥) D = ⟨D; ≤⟩ mit acc ↷ \overline{fix}(T_{Δ}) = ⨆_{i=0}^{m} T_{Δ}^{i}(⊥) = T_{Δ}^{m}(⊥) [17.12.2004] Statt gleichmässiger Fp-Iteration komponentenweise Iteration

Definition 4.7.1: Eine Folge I = (i_{1}, i_{2}, …,) mit i_{j} ∈ {1, …, n} heisst fair, wenn für jedes j ∈ ℕ und jedes i ∈ {1, …, n} ein m ∈ ℕ existiert mit i = i_{j+m}. Mit anderen Worten: In einer fairen folge kommt jeder Index unendlich oft vor.

Beispiel 4.7.2: (1, …, n, 1, …, n, …)

Ein Index i bestimmt für T_{Δ} : D^{n} → D^{n} die Komponentenfunktion g_{i} : D^{n} → D^{n} mit g_{i}(d_{1}, …, d_{n}) = (d‘_{1}, …, d‘_{n}) wobei d‘_{i} := \overline{proj}_{i}(_{Δ}(d_{1}, …, d_{n})) und d‘_{j} := d_{j} für j ≠ i(Berechnung durch i-te Gleichung)

Satz 4.7.3: Chaotische Fp-Iteration Sei D = ⟨D, ≤⟩ein vollständiger Verband und T : D^{n} → D^{n} stetig Dann gilt für eine faire Indexfolge I = (i_{1}, i_{2}, …) mit i_{j} ∈ {1, …, n} \overline{fix}(T) = ⨆\{g_{i_{j}}(g_{i_{j}−1}, … (g_{i_{1}}(⊥)) …)|j ∈ ℕ\} Frage: Ist diese Folge monoton wachsend? Beweis des Fp-Satzes: ⊥ ≤ T (⊥) ≤ T^{2}(⊥) ≤ … kann hier nicht angewandt werden: ⊥ ≤ g_{i_{1}}(⊥)?g_{i_{2}}(g_{i_{1}}(⊥)) Beweisskizze: g_{i_{j}}(… g_{i_{1}}(⊥) …) ≤ T^{j}(⊥) ↷ ⨆\{g_{i_{j}}(… g_{i_{1}}(⊥) …)|j ∈ ℕ\} ≤ ⨆\{T^{j}(⊥)|j ∈ ℕ\} = \overline{fix}(T) Wegen Fairness: Zu jedem j ∈ ℕ existiert k_{j}, so dass in (i_{1}, …, i_{k_{j}}) jeder Index mindestens j-mal vorkommt. ↷ T^{j}(⊥) ≤ g_{i_{k_{j}}} (… (g_{i_{1}}(⊥) …) \overline{fix}(T) = ⨆\{T^{j}(⊥)|j ∈ ℕ\} ≤ ⨆ g_{i_{k_{j}}} (… g_{i_{1}}(⊥) …) □

Folgerung 4.7.3: Besitzt D die arc-Eigenschaft, dann existiert eine endliche Indexfolge i_{1}, …, i_{k}, so dass \overline{fix}(T) = g_{i_{k}}(… g_{i_{1}}(⊥) …)

Problem: Bestimmung einer möglichst kurzen Indexfolge Worklist-Algorithmus Komponentenfunktionen g_{i} : D^{n} → D^{n} weiter zerlegen: g_{i}(d_{1}, …, d_{n}) = (d‘_{1}, …, d‘_{n}) d‘_{i} = \overline{proj}_{i}(T_{Δ}(d_{1}, …, d_{k})) = ⨆\{φ_{j}(d_{j})|j ∈ \overline{Var}(i)\} d‘_{k} = d_{k} für k ≠ i Rechenschritte: φ_{j}(d_{j}) durch Flussregeln steuern Eingabe: Δ = ⟨G, ℑ⟩ mit G = ⟨\overline{Kno}, \overline{Kan}, s⟩ und ℑ = ⟨D, φ, d_{s}⟩ \overline{Kno} = \{s = 1, 2, …, n} Verfahren:

\overline{var} k, k‘: \overline{Kno};

\overline{var} AI: \overline{array}[1 .. n] \overline{of} D

\overline{var} W: \overline{list} \overline{of} \overline{Kan} %Worklist für Rechenschritt \overline{Start} AI[1] := d_{s} AI[j] := ⊥_{D}fürj = 2, …, n; W := \overline{nil}; for all (j, l) ∈ \overline{Kan} do

W := \overline{cons}((j, l), W); end for \overline{Iteration} %φ_{j} als Rechenschritt while W ≠ \overline{nil} do

k := \overline{fst}(\overline{head}(W)); k′ := \overline{snd}(\overline{head}(W)); W := \overline{tail}(W); if φ_{k}(AI[k]) ≰ AI[k‘] then

AI[k‘] := AI[k‘] ⊔ φ_{k}(AI[k]);

for all k“with(k‘, k“) ∈ Kon, but not(k‘, k“) ∈ W do

W := \overline{cons}((k‘, k“), W); end for

end if

4.8. LIVE VARIABLE ANALYSE UND DEAD CODE ELIMINATION FÜR IC-PROGRAMM45

end while Ausgabe: AI = (AI[i], …, AI[n])

Beispiel 4.7.4: AE-Analyse

\overline{OpExp}_{π} = \{\underbrace{x + y}_{1}, \underbrace{x ∗ z}_{2}, \underbrace{t ∗ t}_{3}, \underbrace{z ∗ 2}_{4}, \underbrace{i + 1}_{5}\}

D = 𝔹^{5} W = (1, 2)(2, 3)(3, 4)(3, 5)(4, 6)(5, 6)(6, 3)

W  RD[1]  RD[2]  RD[3]  RD[4]  RD[5]  RD[6]
(1, 2) … (1, …, 1) (0, …, 0) (0, …, 0)  (0, …, 0)  (0, …, 0)  (0, …, 0)
(2, 3) …  (1, …, 1) (0, 0, 0, 1, 1) (0, 1, 0, 1, 1) (0, 1, 0, 1, 1) (0, 0, 0, 1, 1)
(3, 4) …  (0, 1, 0, 1, 1) (0, 1, 0, 1, 1) (0, 1, 0, 1, 1) (0, 1, 0, 1, 1)

(3, 5) … (4, 6) … (5, 6) … (1, 2) … (1, 2) …

[22.12.2004]

4.8 Live Variable Analyse und Dead Code Elimination für IC-Programm

Definition 4.8.1: Sei π ∈ IC, x ∈ V_{π}, i ∈ L_{π}. Dann heisst x lebendig in i, falls p ∈ \overline{Pfad}[i, q + 1] existiert, so dass x auf p benutzt wird (rechte Seite einer Zuweisung oder Test oder Ausgabevariable), ohne vorher neu definiert zu werden.

Aufgabe: Bestimme für jeden Programmpunkt i ∈ L_{π} die Menge LV_{i} der lebendigen Variablen. Hier: Verbesserung (s. SLC): Bestimmung der NV_{i} (needed Variables) Beachte Wertzuwesiungen mit toter linker Seite bilden Dead Code. [Folie: Dead Code Eliminati-Konstruktion eines DFA-Systems Δ = ⟨G, ℑ⟩ on] Rückwärtsanalyse: Datenflussgraph G (“Rückwärts-BB-Graph“)

[figure: •; out; •; 2; •; 3; •; 1; •; in]

D = ⟨P (V_{π}); ⊆⟩ Blocktransformationen: φ_{i} : P (V_{π}) → P (V_{π}) in Block i: α_{1}; …; α_{k} φ_{i} := φ_{α_{1}} ∘ … ∘ φ_{α_{k}} wegen Rückwärtsanalyse. Anweisungstransformation t_{α} : P (V_{π}) → P (V_{π})

• α = v ← e t_{v←e}(M) := \overline{if} v ∈ M \overline{then} M/\{v\} ∪ V_{e} \overline{else} M

• α = \overline{if} be \overline{goto} l t_{α}(M) := M ∪ V_{be}

• α = \overline{goto} l t_{α}(M) = M

Zusätzlich für Ausgabeknoten: φ_{out}(M) := ov_{π} Startinformation: d_{s} = ∅

E_{Δ}X_{out} = d_{s}
X_{2} = φ_{(}out)(X_{out}) ⊔ φ_{3}(X_{3})
X_{3} = φ_{2}(X_{2})
X_{1} = φ_{2}(X_{2})
X_{in} = φ_{1}(X_{1})
φ_{1}(M) = M − w
− u + y  falls u ∈ M
+ x  falls v ∈ M
− v + (x, y) falls v ∈ M
= M − w
− u + y  falls u ∈ M
− v + (x, y) falls v ∈ M
φ_{2}(M) = M − z + (u, v)
φ_{3}(n) = M − z + (u, v) falls z ∈ M
− v + w  falls v ∈ M

Berechnung von NV^{MF P} nach Worklist-Algorithmus

W  NV_{out} NV_{1}  NV_{2}  NV_{3}  NV_{in}
(out, 2), (2, 3), (3, 2), (2, 1), (1, in) d_{s} = ∅ ∅  ∅  ∅  ∅
(2, 3), (3, 2), (2, 1), (1, in)  z
(3, 2), (2, 1), (1, in)  u, v
(2, 1), (1, in)  u, w, z
(3, 2), (2, 1), (1, in)  u, v, v

(3, 2), (2, 1), (1, in)

(2, 1), (1, in)  u, v, w
(1, in)  x, y

Ergebnis der globalen NV-Analyse NV_{1}^{MF P} = {u, v, w} NV_{2}^{MF P} = {u, w, z} NV_{3}^{MF P} = {u, v, w} NV_{4}^{MF P} = {x, y} φ_{i} distributiv: φ(M ∪ M‘) = φ_{i}(M) ∪ φ_{i}(M‘) ↷ NV^{MOP} = NV^{MF P} ↷ Dead Code Optimierung (vgl. SLC) [12.01.2005] 48KAPITEL 4. 4 DATENFLUSSANALYSE UND OPTIMIERUNG ITERATIVER PROGRAMME

Kontrollflussanalyse und Schleifenoptimierung

Sei π ∈ IC Ausnutzung der Schleifenstruktur des Flussgraphen. G_{π} (SI / vorwärts)

• schnellere Fp-Berechnung (Schleifen)

• Schleifenoptimierung (grosser Einfluss)

a) Code Motion (verschieben von schleifeninvarianten Anweisungen vor die Schleife)

b) Elimination von Induktionsvariablen (gleiche Wertprogression von mehreren Variablen nur auf einer Variablen durchführen)

5.1 Schleifenanalyse von Flussgraphen

Flussgraphen eines strukturierten Quellprograms [Folie: Beispiele für Flussgra-Baum mit Rücksprüngen: phen]

• while-Schleifen: 1 Eingang = Ausgang

• repeat-exit i-Schleifen: 1 Eingang - mehrere Ausgänge (Java: break, continue Anweisungen)

Flussgraph G_{1} Schleifen: {1, 2, 3}, {5, 7}, (aber nicht: {1, 5, 7, 6, 8}), {1, 5, 7, 6, 8}, {1, 2, 3, 5, 6, 7, 8} Beachte: Jede Schleife hat genau einen Anfangsknoten, welcher vom Startknoten ausserhalb der Schleife erreichbar ist. hier: 1 bzw. 5. Flussgraph G_{2} 50KAPITEL 5. KONTROLLFLUSSANALYSE UND SCHLEIFENOPTIMIERUNG

Schleifen: keine, weil {2, 3} 2 Anfangsknoten besitzt Definition 5.1.1: Sei G = ⟨\underline{Kno}, \underline{Kan}, s⟩ ein Flussgraph (Vor(s) = ∅, und Pfad[s, k] ≠ ∅ für alle k ∈ \overline{Kno}) falls gilt:

1. S ist stark zusammenhängend, d.h. für alle k, k′ ∈ S mit k ≠ k′ existiert p ∈ \overline{Kno}(p) ⊆ S, und

2. Es existiert genau ein k ∈ S, so dass \overline{Vor}(k)\S ≠ ∅. k heisst Anfang von S.

Beachte: Es muss p ∈ \overline{Pfad}[s, k) existieren mit \overline{Kno}(p) ∩ S = ∅ Aufgabe: Bestimmung der Schleifen von Flussgraphen Hilfsmittel: Dominatorrelation auf Knoten Definition 5.1.2: G = ⟨\underline{Kno}, \underline{Kan}, s⟩ ein Flussgraph und k, k′ ∈ \overline{Kno}.

• k’ dominiert k (Bezeichnung: k’ dom k) :↶↷ für jedes p ∈ \overline{Pfad}[s, k] gilt: k′ ∈ \overline{Kno}(p)

• k’ dominiert k direkt ↶↷ k’ dom k, k′ ≠ k, für alle k” gilt: k” dom k, k′′ ≠ k ↷ k” dom k’

Beispiel 5.1.3: Flussgraph G_{3}

• s dom k, k dom k für alle k ∈ \overline{Kno}

• 2 dom k ↷

• Dominatoren von 8: (s), 1, 3, 4, 7, (8)

• 4 dom 7 direkt

Folgerung 5.1.3: Jeder Knoten k, k ≠ s besitzt genau 1 direkten Dominator. Grund: Die Dominatoren von k sind linear geordnet Folgerung 5.1.3: Baumdarstellung der Dominatorenrelation: Beispiel 5.1.4: Dominatorbaum von G_{3}:

\xymatrix{ & 1 \ar[dl] \ar[dr] \\ 2 &  & 3 \ar[d] \\  &  & 4 \ar[dl] \ar[d] \ar[dr] \\  & 5 & 6 & 7 \ar[d] \\  &  &  & 8 \ar[dl] \ar[dr] \\  &  & 9 &  & 10}

Definition 5.1.5: (b, a) ∈ \overline{Kan} heisst Rückwärtskante, falls a dom b

Lemma 5.1.6: Sei (b, a) eine Rückwärtskante und S := \{k ∈ \overline{Kno} | es existiert p ∈ \overline{Pfad}[k, b] mit a ∉ \overline{Kno}(p)\} Dann ist S ∪ {a} eine Schleife mit Anfang a. Beweis: [Grafik] Sei k ∈ S und p ∈ \overline{Pfad}[a, b] mit a ≠ \overline{Kno}(p) Sei p′ ∈ \overline{Pfad}[s, k]. Also p′p ∈ \overline{Pfad}[s, b]. a dom b ↷ a ∈ \overline{Kno}(p′p) ↷ a ∈ \overline{Kno}(p′) ↷ es existiert p′′ ∈ \overline{Pfad}(a, k] mit a ∉ \overline{Kno}(p′′) so dass \overline{Kno}(p′′) ⊆ S Es folgt:

1. S ∪ {a}ist stark zusammenhängend: k, k′ ∈ S ∪ {a}

k → a → k′

2. a ist Anfang von S ∪ \{a\}: Da \overline{Var}(s) = ∅, so muss a ≠ a

Sei p ∈ \overline{Pfad}[s, a) mit a ∉ \overline{Kno}(p). Da a dom k für alle k ∈ S, so folgt \overline{Kno}(p) ∩ S = ∅ und auch die Eindeutigkeit von a, weil S unter Vorgängerabschluss abgeschlossen.

□ [14.01.2005]

[Folie: Beispiele für Flussgraphen] Bemmerkung S ∪ {a} heisst natürliche Schleife von (b, a)

Beispiel 5.1.7: G_{3} Die natürliche Schleife um (4,3) ist {3, 4, 5, 6, 7, 8, 10}

52KAPITEL 5. KONTROLLFLUSSANALYSE UND SCHLEIFENOPTIMIERUNG

Aufgabe: Bestimmung der Rückwärtskanten und ihrer natürlichen Schleifen Idee: dom-Relation ↷ Rückwärtskanten Vorgängerrelation ↷ natürliche Schleife Flussgraphen von strukturienten Programmen besitzen nur natürliche Schleifen

Definition 5.1.8: Reduzierbarer Flussgraph Ein Flussgraph G = ⟨\underline{Kno}, \underline{Kan}, s⟩ heisst reduzierbar, falls G′ = ⟨\underline{Kno}, \underline{Kan}, s⟩ mit \overline{Kan’} := \overline{Kan}\\{(a, b)|(a, b) ist Rückwärtskante\} azyklisch ist.

Beispiel 5.1.9: G_{1} und G_{3} sind reduzierbar, G_{2} nicht.

5.2 ud- und du-chains

Weitere Programminformation zur Bestimmung schleifeninvarianter Berechnungen

• use-definition-chain (ud-chain): Menge der Definitionen für die Benutzung einer Variablen

• definition-use-chain (du-chain): Menge der Benutzungen für die Definition einer Variablen

Definition 5.2.1: Sei π ∈ IC, v ∈ V_{π}, l, l_{1}, l_{2} ∈ L_{π} und p ∈ \overline{Pfad}_{π}(l_{1}, l_{2})

• v wird in l definiert: (def(v, l)): ↷ α_{l} = l : v ← e

• v wird in l benutzt: (use(v, l)): ↷ entweder α_{e} = l : v′ ← e mit v ∈ V_{e} oder α_{e} = l: if be … mit v ∈ V_{be}

• v wird auf p definiert: ↶↷ def(v, l) für ein l ∈ \overline{Kno}(p)

• clear(v, p): ↷ v wird nicht auf p definiert

• ud(v, l) := \{l′|use(v, l), def(v, l′), es existiert p ∈ \overline{Pfad}(l′, l) : clear(v, p)\}

• du(v, l) := {l′|l ∈ ud(v, l′)}

Berechnung dieser Information durch Variante der Reading-Definition-Analyse (eigentlich RD-Analyse) DFA-System Δ = ⟨G, ℑ⟩ zu π ∈ IC. G SI/vorwärts-Graph von π ℑ = ⟨D, φ, d_{s}⟩ Analyseinformation für l ∈ \overline{Kno} = l_{π} : RD_{l} = \{(v, l′)|def(v, l′) und ∃p ∈ \overline{Pfad}(l′, l) mit clear(v, p)\} Es folgt: l′ ∈ ud(v, l) ↶↷ (v, l′) ∈ RD_{l} und use(v, l) Abstrakte Interpretation ℑ:

5.3. SCHLEIFENINVARIANTE BERECHNUNGEN UND CODE MOTION53

D := P (V_{π} × (L_{π} ∪ {0})) 0 ist Definitionsmarke für v ∈ IV d′_{s} = {(v, 0)|v ∈ IV } φ_{α} : D → D

• α = i : v ← e

φ_{α}(M) := M\{(v, l)|l ∈ L_{π} ∪ {0}} ∪ {(v, i)}

• andere α

φ_{α} = id_{D} φ_{α} distributiv, so dass RD_{l}^{MF P} = RD_{l}^{MOP} [Folie: Beispiel: RD-Analyse

und ud-chains]

5.3 Schleifeninvariante Berechnungen und Code Motion

π ∈ IC mit SI/vorwärts-Graph G_{π} = ⟨\underline{Kno}, \underline{Kan}, s⟩ Schleife S ⊆ \overline{Kno} mit Anfang k ∈ S ud-chains für (v, l) ∈ V_{π} × L_{π}

a) schleifeninvariante Berechnungen

Idee: Rechenausdrücke mit festem Wert in S vor Schleifeneintritt berechnen

Beachte: mögliche Propagation fester Werte innerhalb S

Definition 5.3.1:

l ∈ S heisst s-invariant, wenn in α_{l} : x ← e oder α_{l} = l : \overline{if} be … Schleifenberechnung stets den selben Wert haben.

Bestimmung S-invarianter Knoten

Es gilt: l ∈ S ist S-invariant, falls α_{l} = l : x ← e oder α_{l} = l : \overline{if} be \overline{goto} l′ und für alle y ∈ V_{l} bzw. y ∈ V_{be} gilt:

• ud(y, l) ∩ S = ∅

• ud(y, l) = {l′} und l′ ist S-invariant [19.01.2005] [Folie: Beispiel: Illegale Codeverschiebung (Bedingung 1)] Algorithmus (Analyse): induktive Markierung S-invarianter Knoten.

Algorithmus (Optimierung): Berechnung der Ausdrücke S-invarianter Knoten vor Schleifeneintritt auf temporären Variablen (SLC)

b) Code Motion

Verschiebung einer Wertzuweisung vor den Schleifenanfang.

Sei l ∈ S S-invariant und α_{e} = l : x ← e

Dann gilt: α_{l} kann direkt vor Schleifenanfang ausgeführt werden, falls :

(a) Für jeden Ausgangsknotem k′ ∈ S, d.h. es existiert k′′ ∉ S mit (k′, k“) ∈ \overline{Kan} (“Ein Ausgangsknoten ist ein Knoten, der eine Stelle erreicht, die nicht in der Schleife liegt“), gilt:

[Folie: Bedingungen 2 und 3 ldomk′ für Codeverscheibung]

(b) Es gibt nur 1 Definition von x in S

(c) Wird x in l′ ∈ S benutzt, so folgt: ud(x, l′) = {l} Analysealgorithmus:

i. S-invariante Knoten ii. Eigenschaften 1-3 mit ud- und dom-Information prüfen

Opt: Ja

5.4 Induktionsvariablen

Induktionsvariablen: Variablen einer Schleife mit knónstanter Wertprogression

• i ← i + 1 direkte Induktion

• j ← 3 ∗ i indirekte Induktion

2 Optimierungen:

a) Strengthreduktion (Addition statt Multiplikation)

Bsp:j ← j + 3

b) Elimination von Induktionsvariablen

Entstehung von Induktionsvariablen: z.B. Zählschleifen

Definition 5.4.1: Induktionsvariablen Sei π ∈ IC(ℤ, +, ∗, <, >) und S eine Schleife im (SI/Vorwärts)-Flussgraphen von π

1. x ← V_{s} heisst Basisinduktionsvariable (x ∈ BN(S)), falls gilt:

• es existiert i ∈ S mit α_{i} = i : x ← e

• für alle i ∈ S mit α_{i}0i : x ← e gilt: e ∈ {x + c, c + x|c ∈ ℤ}

2. y ∈ V_{s} heisst abhängige Induktionsvariable (y ∈ AIV (S)) falls gilt:

• es existiert i ∈ S mit α_{i} = i : y ← e

• für alle i ∈ S mit α_{i} = i : y ← e gilt:

e ∈ {x ∗ x, x ∗ c, c + x, x + c|c ∈ ℤ, x ∈ BIV (S)} Bemerkung: Vereallgemeinerung durch verschachtelte Abhängigkeiten Folgerung 5.4.1: Für eine Schleifenberechnung gilt: konstante Wertprogression von x ∈ BN(S) überträgt sich mit einem Faktor auf die von x abhängigen y ∈ AN(S)

[Folie: Strength reduction für Beachte: verschiedene Definitionen mit unterschiedlichen Progressionen Induktionsvariablen]

a) “Strength reduction“ für Induktionsvariablen Idee: Ersetze Multiplikationen durch Additionen (Schleife!) Sei y ∈ AIV (S) und bei i ∈ S eine Definiton von y: α_{i} = i : y ← e mit V_{e} = {x}, x ∈ BN(S) Ist e ein Produkt, so ist dies wie folgt vermeidbar: Wähle neue Variable t_{i} und füge hinter jeder Definition von x eine Definition von t_{i} ein. Diese ist bestimmt durch e und die Definition von x. Falls e = d ∗ x und x ← x + c, so ist t_{i} ← t_{i} + d ∗ c Initialisierung von t_{i} vor Schleifenanfang: t_{i} ← d ∗ x

b) Elimination von Induktionsvariablen Sei y ∈ AIV (S) mit genau einer Definition. i : y ← d ∗ x, also x ∈ P N(S) x werde nur benutzt in ihren Definitionen, in der Definition von y und in Bedingungen der Form \overline{if} be \overline{goto} … Dann kann x eliminiert werden:

(a) Transformation durch Strength reduction

(b) Simulation von x in be durch t_{i} [Folie: Beispiel: Elimination von Induktionsvariablen] [21.01.2005] [Folie: ICP-Beispielprogramm: Fibonaccifunktion] 56KAPITEL 5. KONTROLLFLUSSANALYSE UND SCHLEIFENOPTIMIERUNG

Interprozedurale Analyse

bisher: intra-prozedural (π als Prozedur-rumpf) jetzt: Erweiterung von IC um rekursive Prozeduren Probleme: Abhängigkeit zwischen Aufruf und Rücksprung, Parameterbehandlung hier: keine geschachtelten Prozedurdeklarationen, nur Wert- und Ergebnisparameter

6.1 Syntax von ICP (Intermediate Code with Procedures

π = (P list, V list, Alist) ∈ ICP P list = P decl_{1}, …, P decl_{r} Liste von Prozedurdeklarationen P decl_{i} = (pid_{i}, V list_{i}, Alist_{i}), i = 1, …, r pid_{i}: Prozedurbezeichner V list_{i}; \overline{in} x_{1}, …, x_{n_{i}}; \overline{out} y_{1}, … y_{m}; \overline{loc} z_{1}, …, z_{p_{i}} Liste der formalen Parameter Alist_{i}: Anweisungsliste \underline{Anw} := \underline{Anw}(IC)∪\{pid_{i}(e_{1}, …, e_{n_{i}}, v_{1}, …, v_{m_{i}})|e_{j}einfache Rechenausdrücke als aktuelle Parameter, v_{k} ∈ V (paarweise verschieden), i = 1, …, r} Prozeduraufrufe in Alist_{0} und Alist_{1}, …, Alist_{r} → verschränkte Rekursion Variablen müssen deklariert sein: V_{Alist_{i}} ⊆ V_{V list_{i}} (i = 0, …, r)

6.2 Semantik in ICP

Eingabe als Wertparameter (call-by-value) Jeder Prozeduraufruf mit eigenem Zustandsraum. Werte der formalen Ausgabeparameter in aktuellen Ausgabeparameter übertragen Laufzeitkeller mit Aufrufframes.

Fp-Semantik als Erweiterung der Fortsetzungssemantik von IC

6.3 MOP-Analyse für ICP-Programme

[Folie: Flussdiagramm von π_{fib}] Problem 1 Pfade von π ∈ ICP

(a) Die reguläre Pfadmenge von G_{F ib} (naiver Ansatz)

G_{fib} ↦ G_{fib}^{iter} entsteht aus G_{fib} durch Hinzunahme von Aufrufkanten: (1, 3), (4, 3), (5, 3) und Rücksprungkanten (7, 2), (7, 5), (7, 7) Ferner: Weglassen der (auf der Folie gestrichelten) Kanten hinter Prozeduraufrufen (1, 2), (4, 5), (5, 7) \overline{Pfad}[1, 2] ∋ 13672, 136753672 Vorteil: DFA-Technik ist direkt übertragbar Nachteil: zu viele Pfade, Bedingungen für Analyse zu scharf Grund: kenine Bindung zu Rücksprung und Aufruf

(b) Die kontextfreie Pfadmenge von G_{fib}:

G = ⟨N, Σ, P, S⟩
Σ ={1, 2, …, 7}
N ={P [1, 2], P [2, 2], P [3, 7], P [4, 7], … P [7, 7]}
P :P [1, 2] → 1P [3, 7]P [2, 2]
P [2, 2] → 2
P [3, 7] → 3P [4, 7]|3P [6, 7]
P [4, 7] → 4P [3, 7]P [5, 7]
P [5, 7] → 5P [3, 7]P [7, 7]
P [6, 7] → 6P [7, 7]
P [1, 2]136753672

→ \overline{RPFad}[s, k)

Problem 2 Knotentransformationen für Aufruf- und Rücksprungknoten Abstrakte Interpretation von G_{π} D = ⟨D; ≤⟩ vollständiger Verband mit ACC d_{s} ∈ D Startinformation (Hauptprogramm) Knotentransformationen:

(a) Bei Zuweisungs- und Verzweigungsknoten wie bekannt aus IC: φ_{ij} : D → D

(b) Bei Stop- und Goto-Knoten φ_{ij} = id_{D} (c) Bei Aufruf und Rücksprung?

Idee: Pfadberechnung mit Kellerspeicher (analog Laufzeitkeller) Beachte: Rücksprungadressen unnötig, da Pfad vorgegeben Stack_{D} := D^{+} (leerer Keller unnötig) Spitze rechts φ_{ij} : D → D für Aufrufknoten ij zur Berechnung der Startinformation für den Aufruf aus oberstem Kellerelement φ_{i(q_{i}+1)} : D × D → D für den Rücksprungknoten zur Berechnung der Information beim Rücksprung, bestimmt durch Information von Aufruf und bei Aufrufende (die beiden obersten Kellereinträge) Jedes φ_{ij} bestimmt eine Stacktransformation φ_{ij} : \overline{Kno} → \{f|f_{S}tack_{D} → Stack_{D}}

[26.01.2005]

[Folie: Flussgraph von π − fib] für Fall (1): φ_{ij}^{st}(wd) := wφ_{ij}(d) für Fall (2): φ_{ij}^{st}(wd) := wdφ_{ij}(d) (“PUSH“) für Fall (3): φ_{k(q_{k}+1)}^{st}(wdd‘) := wφ_{ij}(d) Für k ∈ \overline{Kno} \\{s\} (s = 01) und p = (k_{1}, …, k_{q}) ∈ RP fad[s, k) definieren wir

die Analyseinformation für k bezüglich p

AI ⟨p⟩ := top(φ_{kq}(… φ_{k_{1}}(d_{1}) …)) ∈ D mit top : Stack_{D} → D (wd ↦ d) Die MOP-Lösung für k

• AI_{s}^{MOP} := d_{s}

• AI_{k}^{MOP} := ⨆{AI ⟨p⟩ |p ∈ R Pfad[s, k)}

6.4 MFP-Analyse für ICP-Programme

π = (P list, V list_{0}, Alist_{0}) ∈ ICP bestimmt die Flussgraphen G_{0}, …, G_{r} und den daraus kombinierten Flussgraphen G_{π} Unterschiedliche Kantenstruktur: α_{ij} = pid_{k}(…):

1. (ij, i(j + 1)) ∈ \overline{Kan}(G_{i})

2. (ij, k1), (k(q_{k} + 1), i(j + 1)) ∈ \overline{Kan}(G_{π})

MFP-Lösung für iterative Flussgraphen:

E \begin{cases}AI_{s} = d_{s} \\ AI_{k} = ⨆_{l∈\overline{Var}(k)} φ_{l}(AI_{l}) \end{cases}

Übertragung auf den rekursiven Fall Betrachtung von G_{0}, …, G_{r} statt G_{π} Grund: Gleichungen aus E beschreiben lokale Zusammenhänge Aufrufknoten ij mit a_{ij} = pid_{k}(…) : volle Transformationen Φ_{k} : D → D und G_{k} verwenden Neben den Gleichungen für die Analyseinformationen zusätzliche Gleichungen für die Φ_{k}(k = 1, …, r)

Dazu. duale Sicht zur Berechnung der Φ_{k} ij ↦ nicht die von dort bis i(q_{i} + 1), sondern die von i1 bis ij bestimmte Transformation. [Grafik]

• i1 Φ_{ij}

• ij

• i(q_{i} + 1)

[/Grafik]

\xymatrix{•il \ar[dr] &  & •im \ar[dl] \\  & •ij}  Φ_{ij}(d) = φ̃_{il}(Φ_{il}(a)) ⊔ φ̃_{im}(Φ_{im}(a))

φ̃_{il}, φ̃_{im} lokale Anweisungstransformationen φ̃_{il} := φ_{il} für “iterative“ Knoten (Anweisung, Verzweigung, Sprung) il Aufrufknoten mit α_{il} = pid_{R}(…)

[Grafik] [/Grafik] φ̃_{il}(d) := φ_{k(q_{k}+1)}(d, Φ_{k}(φ_{il}(d))) → rekursive Funktionsgleichungssysteme zur Bestimmung der Transformationen Φ_{1}, …, Φ_{r} F_{i}(X) = F_{i(q_{i}+q)}(X) F_{i1}(X) = X F_{ij}(X) = ⨆_{il∈\overline{Var}(ij)inG_{i}} φ̃_{il}(F_{il}(X))

wobei φ̃_{il}(X) = \begin{cases}φ_{il}(X) bei “iter. Knoten“ \\ φ_{k(q_{k}+1)}(X, F_{k}(φ_{il}(X)) \end{cases}

Die eigentlichen Gleichungssysteme E_{0}, …, E_{r} zur Berechnung der Analyseinformation AI_{ij}: AI_{01} = d_{s} AI_{i1} = ⨆_{kj mit a_{k_{j}} =pid_{i}()} φ_{ka}(AI_{kj}) AI_{ij} = ⨆_{il∈\overline{Var}(ij) im G_{i}} φ̃_{il}(AI_{il}) A_{π} := ⋃_{i=0} E_{i} ∪ ⋃_{i=1}^{r} F E_{i} Fp-Technik bestimmt die MFP-LKösung AI^{MF P} := (AI_{ij}^{MF P} |i = 0, …, r, j = 1, …, q_{i})

Satz 6.4.1: Knoop, Steffen

a) Korrektheit AI_{ij}^{MOP} ≤ AI_{ij}^{MF P}

b) Vollständigkeit AI_{ij}^{MOP} = AI_{ij}^{MF P} falls alle φ_{ij} distributiv

Analyse dynamischer Datenstrukturen

Bisher: statische Datenstrukturen (Programmvariablen ˆ= Speicherzellen) Jetzt: Zeiger(-variablen), dynamische Speicherverwaltung im Heap Ziel: Shape-Analyse = approximative Analyse der Datenstrukturen im Heap Gewonnene Informationen:

• Datentypen (→ vermeidung von Typfehlern, z.B. Dereferenzierung von nil-Zeigern)

• Sharing (Zeigervariablen mit gleichem Adressinhalt → Aliasing Effekte)

• Erreichbarkeit (→ Garbage Collection)

• Disjunkte Heapbereiche (→ Parallelisierung)

• Shape (Listen, Bäume, Zykelfreiheit etc.)

Literatur: [Nielson, Nielson, Hankin99, Set 2.6]

7.1 Erweiterung der Sprache IC

Strukturierte Heapzellen (Werte oder Zeiger) Zugriff über Selektoren: sel ∈ \overline{Sel} Zeigerausdrücke: p ∈ \overline{PExp} = V ∪ \{x.sel|x ∈ V, sel ∈ \overline{Sel}\} Wertzuweisungen: p ← e mit p ∈ \overline{PExp} und e ∈ … ∪ \overline{PExp} ∪ \overline{nil} Allokierungsanweisungen: malloc p mit p ∈ \overline{PExp} (Sprunganweisungen, Markierungen wie gehabt)

Beispiel 7.1.1: in x; out y; loc z; 62 KAPITEL 7. ANALYSE DYNAMISCHER DATENSTRUKTUREN

1. y ← \overline{nil} ;

2. \overline{if} x = \overline{nil} \overline{goto} 8;

3. z ← y;

4. y ← x;

5. x ← x.next;

6. y.next ← z;

7. tgoto2;

8. z ← \overline{nil} ;

Operationelle Semantik: siehe [NNH99, Set 2.6.1] Beispiel: siehe Folien 7.1 - 7.3

7.2 Shape-Graphen

Ziel: Abstraktion des (unbeschränkten) Heaps durch eine endliche Datenstruktur Definition 7.2.1: Ein Shape-Graph G = (S, H) besteht aus einer Menge S ⊆ \overline{Aloc} abstrakter Adressen und einem abstrakten Heap H ⊆ S × Sel × S (Notation: X^{Sel}y für (X, sel, Y) ∈ H) Hierbei sein \underline{Aloc} := p(V) Bemerkung: [Interpretation von G = (S, H)]

• Für X ∈ S bedeutet x, y ∈ X, dass die Variablen x und y auf die gleiche Heapadresse verweisen. Somit repräsentiert ∅ alle Heapadressen, die nicht direkt durch Variablen dereferenziert werden.

• Verweisen x ∈ sel und y auf die gleichen Heapadresse (x, y ∈ V, sel ∈ \overline{Sel}) und sind X, Y ∈ S mit x ∈ X und y ∈ Y, so gilt X →^{sel} Y in H

Beispiel 7.2.2: Folien 7.1 - 7.3 (beachte: Shape-Graph a (für x) ˆ= Shape-Graph e (für y) → Ein-/Ausgabe strukturell “ähnlich“) Obiger Interpretation entsprechend sollte jeder Shape-Graph G = (S, H) den folgenden Invarianten genügen:

1. Disjunktheit: X, Y ∈ S → X = Y oder X ∩ Y = ∅ (d.h. eine Variable kann nur auf eine (abstrakte) Heapadresse verweisen)

2. Determiniertheit: X →^{sel} Y und X →^{sel} Z in H → X = ∅ oder Y = Z (d.h. die über einen Selektor referenzierte Heapadresse ist eindeutig, wenn die Ausgangsadresse nicht ∅ ist)

Bemerkung: Das folgende Beispiel zeigt, dass in (2) im Fall X = ∅ Determiniertheit im allgemeinen nicht vorliegt:

Beispiel 7.2.3: Konkret

y → ∘ ←^{sel} ∘

z → ∘ ←^{sel} ∘

Abstrakt:

[figure: {z} = Z; {z} = Z; ∅]

Definition 7.2.4: Ein Shape-Graph mit (1) und (2) heisst kompatibel. Die Menge aller kompatiblen Shape-Graphen wird mit SG bezeichnet.

Bemerkung: IN [NNH99] besitzen Shape-Graphen eine weitere Komponente, die sogenannte Sharing-Information.

7.3 Die Analyse

Ansatz: Vorwärtsanalyse zur Bestimmung aller Shape-Graphen, die die mögliche Heapstruktur im entsprechenden Programmpunkt abstrahieren. Vollständiger Verband: D = ⟨p(SG), S⟩ Klar: V, Sel endlich → SG endlich → p(SG) endlich → ACC-Eigenschaft Abstrakte Interpretation: ℑ = ⟨D, φ, d_{s}⟩ Startinformationen: d_{s} = Menge aller Shape-Graphen zu den möglichen Anfangswerten aller x ∈ IV

Beispiel 7.3.1: Listenspiegelung IV = \{x\}, x (endliche) Liste → d_{s} = \{\underbrace{(∅, ∅)}_{leere}, \underbrace{\{x\}}_{ein El.}, \underbrace{\{x\} →^{next} ∅}_{zwei El.}, \underbrace{\{x\} →^{next} ∅ ⟲ next}_{≥ drei El. Eingabeliste}\}

[02.02.2005]

Transferfunktion: φ_{α} : p(SG) → p(SG) (monoton) für α ∈ \overline{Anw} Diese transformieren jeden einzelnen Shape-graphen in eine Menge solcher Graphen, d.h. φ_{α}({G_{1}, …, g_{n}}) = ∪_{i=1}^{n}Ψ_{α}(G_{i}) wobei Ψ_{α} : SG → p(SG) durch Fallunterscheidung bezgl. α definiert ist.

a) α = \overline{goto} l/ \overline{if} p(u_{1}, …, u_{r}) \overline{goto} l/x ← x Keine Modifikation des Heaps → Ψ_{α}(G) = {G}

b) α = x ← c/x ← f(u_{1}, …, u_{r})/x ← \overline{nil} evtl Verweise von x auf den Heap werden aufgehoben → Ψ_{α}(b) = {kill_{x}(G)} Wobei kill_{x}(S, H) = (S′, H′) mit S′ = {X\{x}|X ∈ S} und H′ = {(X\{x}, sel, Y \{x}|(X, selY) ∈ H} Bsp Folie 7.3, Schritt d → e (α = z ← \overline{nil} )

c) α = x ← y (mit x ≠ y) Effekt:

(a) Aufhebung der Bindung von x

(b) Weitergabe evtl. Bindungen von y an x → Ψ_{α}(G| = {gen_{x}^{y}(kill_{x}(G))} wobei gen_{x}^{y}(S, H) = (S′, H′) mit S′ = {H′ = {(g_{x}^{y}(X), sel, g_{x}^{y}(Y)|(X, sel, Y) ∈ H} für

g_{x}^{y} = \begin{cases}X ∪ \{x\}, & falls y ∈ X \\ X, & sonst \end{cases}

Bsp Folie 7.1/7.2, Schritt a3 → a4 (α = y ← x)

d) α = x ← x.sel:

wird ersetzt durch die (äquivalente) Anweisungsfolge t ← x.sel; x ← t; t ← \overline{nil} (t ∈ LV neu) → φ_{α} = φ_{t← \overline{nil}} ∘ φ_{x←t} ∘ φ_{t←x.sel}

e) x ← y.sel (x ≠ y):

Sei zunächst (S′, H′) = kill_{x}(G) Mögliche Fälle:

(a) y ∉ X für alle X ∈ S′ oder y ∈ Y für ein Y ∈ S′, aber es existiert kein Z ∈ S′ mit Y →^{sel} Z (d.h. y oder y.sel ist eine Zahl, nil, oder undefiniert)

(b) es existiert Y, Z ∈ S′ mit y ∈ Y, Z ≠ ∅ und Y →^{sel} Z (d.h. die Adresse y.sel wird auch durch andere Variablen referenziert)

(c) es existiert y ∈ S′ mit y ∈ Y und Y →^{sel} ∅ (d.h. keine andere Variable verweist auf die gleiche Adresse wie y.sel)

Entsprechende Modifikation dees Shape-Graphen:

1. Nur x entfernen:

Ψ_{α}(G) = {(S′, H′)}

2. In z einen x-Verweis ergänzen Ψ_{α}(G) = {(S′′, H′′)} mit S′′ = {h_{x}^{z}(X)|X ∈ S′} und H′′ = {h_{x}^{z}(X), sel, h_{x}^{z}(Y)|(X, sel, Y) ∈ H′}

für h_{x}^{z}(X) = \begin{cases}Z ∪ \{x\}, & falls X = Z \\ X, & sonst \end{cases}

3. Abstrakte Adresse für x einführen und alle möglichen Heapstrukturen berücksichtigen. Ψ_{α}(G) = {(S′′, H′′) ∈ SG|kill_{x}(S′′, H′′) = (S′, H′), {x} ∈ S′′, (y, sel, {x}) ∈ H′′} Bsp (Fall 3) Folie 7.4 Bem: Das Eintreten von Fall 1 bedeutet, dass im konkreten Programm möglicherweise ein nil-Zeiger derefereniert wird

4. α = x.sel ← x/x.sel ← f(u_{1}, …, u_{r})/x.sel ← \overline{nil} : ähnlich zu (e) (Fallunterscheidung bzgl. x/x.sel)

5. α = x.sel ← y:

Bsp Folie 7.2, Schritt a5 → b (α = x.next ← z)

6. α = x.sel ← y.sel′:

wird ersetzt durch t ← y.sel′, x.sel; x.sel ← t; t ← \overline{nil}

7. α = \overline{malloc}x:

Ψ_{α}(S, H) = (S′ ∪ {x}) für (S′, H′) = kill_{x}(S, H)

8. α = \overline{malloc}x.sel:

wird ersetzt durch \overline{malloc}t; x.sel ← t; t ← \overline{nil}