Seminar Programmanalyse

Kontrollflussanalyse I

Joschka Rinke

23. Juni 2009

Abstrakte Kontrollflussanalyse: Einleitung

Wohin führen elementare Programmblöcke? Welche Funktionen werden für welche Applikation ausgeführt? Jeder Programmblock wird gelabelt! Es gibt keine Seiteneffekte! Die CFA wird durch ein Paar spezifiziert: (Ĉ,ρ̂), wobei dann:

Ĉ(l) enthält die Werte, die der Programmblock mit Label l errechnen kann. ρ̂(x) enthält die Werte, an die die Variable x gebunden werden kann.

Dabei gilt dann: ρ̂ ⊆ Ĉ

Syntax der FUN language

Ein Programmteil mit einem Label ist ein Ausdruck:

e ∈ Exp Ausdruck (oder gelabelter Term)

Ein Programmteil ohne Label ist ein Term:

t ∈ Term Term (oder nicht gelabelte Expression)

fn x → Exp definiert eine Funktion fun f x → Exp definiert eine rekursive Funktion let x = e_{1} in e_{2} ist äquivalent zu (fn x → e_{2})(e_{1}) Wir haben also die abstrakte Syntax der Sprache wie folgt gegeben: e ::= t^{l} t ::= c | x | fn x → e_{0}| fun f x → e_{0}|e_{1}e_{2} | if e_{0} then e_{1} else e_{2} | let x = e_{1} in e_{2} | e_{1} op e_{2}

0-CFA Analyse

Ergebnis ist die Kontrollflussinformation(Ĉ,ρ̂), wobei Ĉ ist abstrakter Cache Lab → V̂al ρ̂ ist abstrakte Umgebung Var → V̂al

Weiter gibt es:

v̂ ∈ V̂al = P(Term) abstrakte Werte(Values)

Da 0-CFA keinen Datenfluss betrachtet können semantisch identische Programme unterschiedliche Analyseergebnisse haben.

Beispiel

J.Rinke Seminar Programmanalyse

Die “Acceptable“-Relation

⊨ : (Cache x Env x Exp) → {true, false} Die die “Acceptable“-Relation definierenden Klauseln:

Die “Acceptable“-Relation (Fortsetzung)

J.Rinke Seminar Programmanalyse

Die Klauseln [con], [var], [fn] und [fun]

[con]: Da 0-CFA keine Werte betrachtet gilt

(Ĉ,ρ̂)⊨c^{l} iff ∅⊆Ĉ(l)

[var]: Bindung der abstrakten Umgebung an den abstrakten Cache.

[fn] und [fun]: Funktionsterm muss in Ĉ(l) enthalten sein.

J.Rinke Seminar Programmanalyse

Die Klauseln [let] und [if]

[let] und [if] enthalten rekursive Aufrufe und fordern daher auch eine Analyse der Unterausdrücke. Die Klausel [let] verbildlicht:

Die Klausel [app]

[app] enthält auch rekursive Aufrufe und setzt daher einige Verlinkungen vorraus.

Wohldefiniertheit der Analyse

Die Klausel [app] erlaubt uns für (Ĉ,ρ̂)⊨e keine strukturelle Induktion über e, daher wird “⊨“ coinduktiv definiert: Q:((Cache x Env x Exp)→{true,false}) →((Cache x Env x Exp)→{true,false}) daraus folgt nach den eingeführten “Acceptable“-Relationen: ((Cache x Env x Exp) → {true,false},⊑) wobei ⊑ wie folgt definiert wird: Q_{1} ⊑ Q_{2} iff ∀(Ĉ,ρ̂,e):(Q_{1}(...) = true) → (Q_{2}(...) = true) woraus ersichtlich wird, dass “⊨“ der größte Fixpunkt von Q ist.

Strukturelle Operationale Semantik

Schritt: Zeigen, dass die Informationen aus der Analyse tatsächlich eine korrekte Beschreibung der Vorgänge bei der Ausführung des Programms sind. Vorgehensweise: Binden der Variablen an ihre Werte. dafür: FUN erweitern um die folgenen Kategorien

v ∈ Val

ρ ∈ Env

definiert durch

v ::= c | close t in ρ ρ ::= [] | ρ[x →v]

Zwischenausdrücke und Zwischenterme

ie ∈ IExp it ∈ ITerm dadurch wird unsere Syntax wie folgt erweitert: ie ::= it^{l} it ::= c | ... | bind ρ in ie | close t in ρ

Transitionen Teil 1

J.Rinke Seminar Programmanalyse

Transitionen Teil 2

J.Rinke Seminar Programmanalyse

Beispiel

J.Rinke Seminar Programmanalyse

Die [app]-Klauseln

[app_{1}]: Operator auswerten [app_{2}]: Operand auswerten [app_{fn}]: Binden des aktuellen Parameters an den formalen Parameter [app_{fun}]: ...und die rekursive Funktion ausführen

Korrektheit der Kontrollflussanalyse

Ziel: Subject reduction result Vorgehensweise: Abstraktion des Programms zu einem Zeitpunkt muss auch in der Analyse vorhanden sein. dafür: Erweiterung um intermediate Expressions

Korrektheitsrelation und die Klauseln [bind] und [close]

→ Die Klauseln werden um eine Relation R erweitert unter der gilt, dass

[bind]: das Ergebnis der Ausführung der Klausel auch ein Wert des Konstruktes ist. [close]: der Term von [close] auch ein möglicher Wert des Konstruktes ist.

Theorem

Existiert eine Ausführung eines Programms der Art, dass dazu eine Abstraktion vorhanden ist, so ist diese Abstraktion Teil der Analyse.

Beweis am Beispiel [app_{fn}]

ρ ⊢((close(fn x→ t_{0}^{l_{0}})in ρ_{1})^{l_{1}}v_{2}^{l_{2}})^{l} → (bind ρ_{1}[x → x_{2}] in t_{0}^{l_{0}})^{l}

Aus (Ĉ,ρ̂)⊨ie folgt (Ĉ,ρ̂)⊨(close ... ), was beinhaltet, dass:

(fn x→ t_{0}^{l_{0}})∈Ĉ(l_{1}) und ρ_{1}Rρ̂

Weiter haben wir dann (Ĉ,ρ̂)⊨ t_{2}^{l_{2}} wobei für v_{2}=e ersichtlich ist, dass:

v_{2}V (Ĉ(l_{2}),ρ̂)

Im Fall, dass v_{2}=close t_{2} in ρ_{2} folgt nach Definition (Ĉ,ρ̂)⊨v_{2}^{l_{2}}. Aus der Analyse ablesbar folgt dann:

(Ĉ,ρ̂)⊨ t_{0}^{l_{0}}, Ĉ(l_{0})⊆Ĉ(l) und (ρ_{1}[x→v_{2}])Rρ̂ und man erhält das gewünschte (Ĉ,ρ̂)⊨ie´

Beispiel

Unter Verwendung der Klauseln [bind] und [close] kann man leicht sehen, dass das wirklich der Fall ist.

J.Rinke Seminar Programmanalyse

Die Existenz von Lösungen

Existiert für jedes e eine (Ĉ,ρ̂), so dass (Ĉ,ρ̂)⊨e? Existiert für jedes e eine kleinste CFA? z.B.: Existiert ein (Ĉ_{0},ρ̂_{0}), so dass(Ĉ_{0},ρ̂_{0})⊨e und jedesmal, wenn (Ĉ,ρ̂)⊨e dann (Ĉ_{0},ρ̂_{0}) kleiner als (Ĉ,ρ̂) ist?

Moore Family

(Ĉ,ρ̂)|(Ĉ,ρ̂)⊨ie ist für alle ie ∈ IExp eine Moore Family.

J.Rinke Seminar Programmanalyse

Beispiel

J.Rinke Seminar Programmanalyse

Coinduktion vs. Induktion, oder warum Coinduktion?

Elementare Vorraussetzung für CFA ist Coinduktive-Definition der “Acceptable“-Relation:

⊨ als größten Fixpunkt eines Funktionals Q

Alternativ könnte man die “Acceptable“-Relation auch induktiv definieren:

⊨´ als kleinsten Fixpunkt eines Funktionals Q

Dann gilt aber: Es existiert ein ie_{∗} ∈ IExp, so dass (Ĉ,ρ̂)|(Ĉ,ρ̂)⊨´ ie_{∗} nicht Moore Family ist.

Zusammenfassung

Analyse statischer Informationen über den Kontrollfluss zur Compile-Zeit möglich Subject Reduction als erster Schritt für Kontrollfluss zur Laufzeit