vorlesung modellierung, analyse, veri kation ......vorlesung modellierung, analyse, veri kation...
Post on 31-Dec-2019
19 Views
Preview:
TRANSCRIPT
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Vorlesung Modellierung, Analyse, VerifikationWintersemester 2019/20
Prof. Barbara KonigUbungsleitung: Christina Mika-Michalski
Barbara Konig Modellierung, Analyse, Verifikation 1
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Analyse verfugbarer Ausdrucke
Wir wollen nun fur den Eingang und Ausgang jedes Blocksfolgende Menge bestimmen:
Die Menge aller nicht-trivialen arithmetischen Ausdrucke,die auf allen Pfaden bis zu diesem Programmpunkt be-reits berechnet wurden und nicht zwischendurch modifi-ziert wurden.
Anmerkung: Ein arithmetischer Ausdruck ist nicht-trivial, wenn erverschieden von einer Variable und verschieden von einer ganzenZahl ist.
Barbara Konig Modellierung, Analyse, Verifikation 25
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Erwunschtes Analyseergebnis
` A◦(`) A•(`)
1 ∅ {a+b}2 {a+b} {a+b, a*b}3 {a+b} {a+b}4 {a+b} ∅5 ∅ {a+b}6 {a+b} {a+b}
[x:=a+b]1 [y:=a*b]2
[a:=a+1]4
yes [y>a+b]3no
[z:=x]6[x:=a+b]5
Barbara Konig Modellierung, Analyse, Verifikation 26
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Berechnung des Analyseergebnisses
kill- und gen-Funktionen
kill(`) =
{a′ ∈ AExp∗ | x ∈ Var(a′)}
falls block(`) = (x:=a)∅ sonst
gen(`) =
{a′ ∈ AExp(a) | x 6∈ Var(a′)}
falls block(`) = (x:=a)∅ falls block(`) = skip
AExp(b) falls block(`) = b
A•(`) = A◦(`)\kill(`) ∪ gen(`)
Barbara Konig Modellierung, Analyse, Verifikation 27
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Datenflussanalyse: Gleichungssystem
A◦(1) = ∅A◦(2) = A•(1)
A◦(3) = A•(2)
∩ A•(5)
A◦(4) = A•(3)
A◦(5) = A•(4)
A◦(6) = A•(3)
A•(1) = A◦(1) ∪ {a + b}A•(2) = A◦(2) ∪ {a ∗ b}A•(3) = A◦(3) ∪ {a + b}A•(4) = A◦(4)
\{a + b, a ∗ b, a + 1}A•(5) = A◦(5) ∪ {a + b}A•(6) = A◦(6)
Barbara Konig Modellierung, Analyse, Verifikation 28
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Ordnungen
Eine Ordnung (partielle Ordnung) auf einer Menge L ist eineRelation v ⊆ L× L, fur die gilt:
1 v ist reflexiv: ∀l ∈ L : (l v l).
2 v ist transitiv: ∀l1, l2, l3 ∈ L : (l1 v l2, l2 v l3 ⇒ l1 v l3).
3 v ist antisymmetrisch: ∀l1, l2 ∈ L : (l1 v l2, l2 v l1 ⇒ l1 = l2).
Barbara Konig Modellierung, Analyse, Verifikation 29
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Obere Schranken, maximale Elemente
Gegeben: Menge L mit Ordnung v.
Obere Schranke von Y ⊆ L: Element s ∈ L mit ∀l ∈ Y : l v s.
Kleinste obere Schranke/Supremum von Y : Element s fur dasgilt:
s ist eine obere Schranke von Y undfur jede andere obere Schranke s ′ von Y gilt s v s ′.
Maximales Element: m ∈ Y ist ein maximales Element von Y ,wenn fur jedes Element l ∈ Y mit m v l folgt, dass m = l .
Barbara Konig Modellierung, Analyse, Verifikation 30
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Untere Schranken, minimale Elemente, Notation
Analog: Definition von unterer Schranke, großter unterer Schranke(Infimum), minimalem Element
Notation:
Supremum von Y :⊔Y bzw. l1 t l2 =
⊔{l1, l2}
Infimum von Y :d
Y bzw. l1 u l2 =d{l1, l2}
Barbara Konig Modellierung, Analyse, Verifikation 31
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Vollstandiger Verband
Ein geordnete Menge (L,v) heißt vollstandiger Verband, wenn
jede Teilmenge Y von L eine kleinste obere und eine großteuntere Schranke hat.
Dies gilt auch fur Y = ∅ und Y = L. Man definiert:
⊥ =d
L (bottom, kleinstes Element im Verband)
> =⊔
L (top, großtes Element im Verband)
Barbara Konig Modellierung, Analyse, Verifikation 32
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Eigenschaften von Ordnungen, Ketten
Eine Ordnung v heißt total, wenn fur zwei Element l1, l2 ∈ Limmer l1 v l2 oder l2 v l1 gilt.
Y ⊆ L heißt Kette, wenn v eingeschrankt auf Y ×Y total ist.
Aufsteigende Kette: endliche oder unendliche Folgel0, l1, l2, l3, . . . mit li v li+1 fur alle i ∈ N0.Man schreibt auch (ln)n∈N0
.
v erfullt die Ascending Chain Condition, wenn es fur jedeunendliche aufsteigende Kette (ln)n einen Index m gibt mitlj = lj+1 fur j ≥ m.
Barbara Konig Modellierung, Analyse, Verifikation 33
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Eigenschaften von Funktionen
Gegeben: geordnete Mengen (L1,v1), (L2,v2)
Eine Funktion f : L1 → L2 heißt
monoton, falls fur alle l1, l2 ∈ L1 gilt: aus l1 v1 l2 folgt stetsf (l1) v2 f (l2).
additiv, falls fur l ,m ∈ L1 stets f (l tm) = f (l) t f (m) gilt.
multiplikativ, falls fur l ,m ∈ L1 stets f (l um) = f (l) u f (m)gilt.
In den letzten beiden Fallen muss man voraussetzen, dass (L1,v1)und (L2,v2) Verbande sind, damit die Definition Sinn macht.
Barbara Konig Modellierung, Analyse, Verifikation 34
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Fixpunkte
Gegeben: f : L→ L, wobei (L,v) ein vollstandiger Verband ist.
Menge aller Fixpunkte: Fix(f ) = {l ∈ L | f (l) = l}Menge aller Prafixpunkte: Pre(f ) = {l ∈ L | f (l) v l}Menge aller Postfixpunkte: Post(f ) = {l ∈ L | f (l) w l}
Außerdem definieren wir:
lfp(f ) =d
Fix(f )
gfp(f ) =⊔
Fix(f )
Achtung: lfp/gfp soll zwar fur least fixed-point/greatest fixed-pointstehen, aber es ist noch nicht klar, ob diese Elemente tatsachlichFixpunkte sind.
Barbara Konig Modellierung, Analyse, Verifikation 35
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Satz von Knaster-Tarski
Sei (L,v) ein vollstandiger Verband und f : L→ L eine monotoneFunktion. Dann gilt:
lfp(f ) =l
Pre(f ) ∈ Fix(f )
gfp(f ) =⊔
Post(f ) ∈ Fix(f ).
Folgerung: Eine monotone Funktion f auf einem vollstandigenVerband hat einen großten und einen kleinsten Fixpunkt (diemoglicherweise ubereinstimmen).
Frage: Wie konnen diese Fixpunkte bestimmt werden?
Barbara Konig Modellierung, Analyse, Verifikation 36
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Satz von Kleene
Sei (L,v) ein vollstandiger Verband, f : L→ L eine monotoneFunktion.Falls f stetig ist, das heißt fur jede aufsteigende Kette (ln)n gilt:
f (∞⊔n=0
ln) =∞⊔n=0
f (ln),
dann folgt lfp(f ) =∞⊔n=0
f n(⊥).
Verband erfullt die Ascending Chain Condition Verfahren zurBestimmung von Fixpunkten:
Berechne f (⊥), f (f (⊥)), f 3(⊥), . . . bis die Folge stationarwird, d.h., f i (⊥) = f i+1(⊥). Man erhalt dadurch denkleinsten Fixpunkt.
Barbara Konig Modellierung, Analyse, Verifikation 37
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Wiederholung: Fixpunkttheorie
Sei (L,v) ein vollstandiger Verband und f : L→ L eine monotoneFunktion. Dann gilt:
Großter und kleinster Fixpunkt:Die Funktion f besitzt einen kleinsten Fixpunkt lfp(f ) undeinen großten Fixpunkt gfp(f ).
Fixpunktiteration:Falls f stetig ist, d.h., fur jede aufsteigende Kette (ln)n gilt:f (⊔∞
n=0 ln) =⊔∞
n=0 f (ln), so folgt
lfp(f ) =∞⊔n=0
f n(⊥).
Analoges gilt fur den großten Fixpunkt.
Barbara Konig Modellierung, Analyse, Verifikation 38
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Datenflussanalyse: Gleichungssystem
A◦(1) = ∅A◦(2) = A•(1)
A◦(3) = A•(2)
∩ A•(5)
A◦(4) = A•(3)
A◦(5) = A•(4)
A◦(6) = A•(3)
A•(1) = A◦(1) ∪ {a + b}A•(2) = A◦(2) ∪ {a ∗ b}A•(3) = A◦(3) ∪ {a + b}A•(4) = A◦(4)
\{a + b, a ∗ b, a + 1}A•(5) = A◦(5) ∪ {a + b}A•(6) = A◦(6)
F (N1, . . . ,N6,X1, . . . ,X6) = (∅,X1,X2 ∩ X5,X3,X4,X3,
N1 ∪ {a + b},N2 ∪ {a ∗ b},N3 ∪ {a + b},N4\{a + b, a ∗ b, a + 1},N5 ∪ {a + b},N6)
Barbara Konig Modellierung, Analyse, Verifikation 39
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Fixpunktiteration (I)
F 0(AExp∗, . . . ) = (AExp∗, . . . ,AExp∗)
F 1(AExp∗, . . . ) = (∅,AExp∗,AExp∗,AExp∗,AExp∗,AExp∗,AExp∗,AExp∗,AExp∗, ∅,AExp∗,AExp∗)
F 2(AExp∗, . . . ) = (∅,AExp∗,AExp∗,AExp∗, ∅,AExp∗,{a + b},AExp∗,AExp∗, ∅,AExp∗,AExp∗)
F 3(AExp∗, . . . ) = (∅, {a + b},AExp∗,AExp∗, ∅,AExp∗,{a + b},AExp∗,AExp∗, ∅, {a + b},AExp∗)
F 4(AExp∗, . . . ) = (∅, {a + b}, {a + b},AExp∗, ∅,AExp∗,{a + b}, {a + b, a ∗ b},AExp∗, ∅, {a + b},AExp∗)
F 5(AExp∗, . . . ) = (∅, {a + b}, {a + b},AExp∗, ∅,AExp∗,{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b},AExp∗)
Barbara Konig Modellierung, Analyse, Verifikation 40
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Fixpunktiteration (II)
F 5(AExp∗, . . . ) = (∅, {a + b}, {a + b},AExp∗, ∅,AExp∗,{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b},AExp∗)
F 6(AExp∗, . . . ) = (∅, {a + b}, {a + b}, {a + b}, ∅, {a + b},{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b},AExp∗)
F 7(AExp∗, . . . ) = (∅, {a + b}, {a + b}, {a + b}, ∅, {a + b},{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b}, {a + b})
F 8(AExp∗, . . . ) = (∅, {a + b}, {a + b}, {a + b}, ∅, {a + b},{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b}, {a + b})
Barbara Konig Modellierung, Analyse, Verifikation 41
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Erwunschtes Analyseergebnis
F 8(AExp∗, . . . ) = (∅, {a + b}, {a + b}, {a + b}, ∅, {a + b},{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b}, {a + b})
` AE◦(`) AE•(`)
1 ∅ {a+b}2 {a+b} {a+b, a*b}3 {a+b} {a+b}4 {a+b} ∅5 ∅ {a+b}6 {a+b} {a+b}
[x:=a+b]1 [y:=a*b]2
[a:=a+1]4
yes [y>a+b]3no
[z:=x]6[x:=a+b]5
Barbara Konig Modellierung, Analyse, Verifikation 42
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Analyse lebendiger Variablen
Eine Variable heißt lebendig am Ausgang eines Blocks, wenn esmoglicherweise einen Pfad von diesem Block zu einem anderenBlock gibt, der diese Variable in einer Bedingung oder auf derrechten Seite einer Zuweisung benutzt, ohne dass die Variablevorher neu definiert wird.
Beispielprogramm: [x:=2]1;[y:=4]2;[x:=1]3;if [y>x]4
then [z:=2*x]5
else [z:=y*y]6
fi;
[x:=z]7
Barbara Konig Modellierung, Analyse, Verifikation 43
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Analyse lebendiger Variablen
Idee: Ruckwartsanalyse mit Vereinigung
Verband: (P(Var∗),⊆)
kill- und gen-Funktionen:
kill(`) =
{{x} falls block(`) = (x:=a)∅ sonst
gen(`) =
Var(a) falls block(`) = (x:=a)Var(b) falls block(`) = b∅ sonst
Barbara Konig Modellierung, Analyse, Verifikation 44
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Parameter bei der Datenflussanalyse (I)
Vorwartsanalyse Ruckwartsanalyse
Schnitt Verfugbare Ausdrucke ?
Vereinigung ? lebendige Variable
Auf jeden Fall in der Vergangenheit . . . Schnitt + Vorwartsanalyse
Auf jeden Fall in der Zukunft . . . Schnitt + Ruckwartsanalyse
Moglicherweise in der Vergangenheit . . . Vereinigung + Vorwartsanalyse
Moglicherweise in der Zukunft . . . Vereinigung + Ruckwartsanalyse
Barbara Konig Modellierung, Analyse, Verifikation 45
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Parameter bei der Datenflussanalyse (II)
Weitere Parameter:
Obermenge aller Analyseergebnisse (Vollstandiger Verband)
Initialer Analysewert
kill-/gen-Funktionen (allgemein: Transferfunktionen)
Flussrelation mit initialen bzw. finalen Labels
Barbara Konig Modellierung, Analyse, Verifikation 46
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Monotone Frameworks
Monotoner Framework (L,F)
(L,v) ist ein vollstandiger Verband
F ist eine Menge von monotonen Funktionen von L nach LF enthalt die Identitat und ist unter Funktionskompositionabgeschlossen.
Barbara Konig Modellierung, Analyse, Verifikation 47
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Instanz eines monotonen Frameworks
Instanz eines monotonen Frameworks (L,F): (L,F ,Lab,F ,E , ι, f·)
(L,v) ist ein vollstandiger Verband
F ist eine Menge von monotonen Funktionen(+ zusatzliche Eigenschaften)
Lab ist eine endliche Menge von Labels
F ⊆ Lab× Lab ist die Flussrelation
E ⊆ Lab ist eine Menge von sogenannten extremalen Labels
ι ∈ L ist der Wert, der jedem extremalen Label zugeordnetwird
f· bildet jedes Label ` ∈ Lab auf eine Funktion f` ∈ F ab.
Barbara Konig Modellierung, Analyse, Verifikation 48
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Gleichungssystem
Gleichungssystem zur Datenflussanalyse:
(2.1) A◦(`) =⊔{A•(`′) | (`′, `) ∈ F} t ι`E
wobei ι`E =
{ι falls ` ∈ E⊥ sonst
(2.2) A•(`) = f`(A◦(`))
Barbara Konig Modellierung, Analyse, Verifikation 49
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Reichweite von Zuweisungen
Fur jeden Block des Programms und fur jede Variable sollen alleStellen bestimmt werden, an denen dieser Variable zuletzt ein Wertzugewiesen worden sein konnte.
(x, `): x konnte zuletzt in Block ` ein Wert zugewiesen worden sein(x, ?): x wurde evtl. noch gar kein Wert zugewiesen.
Beispielprogramm:
[y := x]1;[z := 1]2;while [y>1]3 do
[z := z*y]4;[y := y-1]5
od;
[y:=0]6
Barbara Konig Modellierung, Analyse, Verifikation 50
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Reichweite von Zuweisungen
Idee: Vorwartsanalyse mit Vereinigung
Verband: (P(Var∗ × (Lab∗ ∪ {?})),⊆)
Initialer Analysewert: {(x, ?) | x ∈ Var∗}Transferfunktion:
kill(`) =
{{(x, ?)} ∪ {(x, `′) | `′ ∈ Lab∗} falls block(`) = (x:=a)∅ sonst
gen(`) =
{{(x, `)} falls block(`) = (x:=a)∅ sonst
Barbara Konig Modellierung, Analyse, Verifikation 51
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Benotigte Ausdrucke
Zu einem Block ` sollen arithmetische Ausdrucke bestimmtwerden, die auf jedem von ` ausgehenden Pfad benutzt werden,ohne vorher verandert zu werden.
Beispielprogramm:
if [x=1]1
then [y := a+b*c]2
else [y := b*c]3
fi
Barbara Konig Modellierung, Analyse, Verifikation 52
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Benotigte Ausdrucke
Idee: Ruckwartsanalyse mit Schnitt
Verband: (P(AExp∗),⊇)
Initialer Analysewert: ∅Transferfunktion:
kill(`) =
{{a′ ∈ AExp∗ | x ∈ Var(a′)} falls block(`) = (x:=a)∅ sonst
gen(`) =
AExp(a) falls block(`) = (x:=a)AExp(b) falls block(`) = b∅ sonst
Barbara Konig Modellierung, Analyse, Verifikation 53
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Monotone Frameworks (Zusammenfassung)
Verfugbare Reichweite von Benotigte Lebendige
Ausdrucke Zuweisungen Ausdrucke Variable
L P(AExp∗) P(Var∗ × (Lab∗ ∪ {?})) P(AExp∗) P(Var∗)
v ⊇ ⊆ ⊇ ⊆t ∩ ∪ ∩ ∪⊥ AExp∗ ∅ AExp∗ ∅ι ∅ {(x, ?) | x ∈ Var(S)} ∅ variabel
E {init(S)} {init(S)} final(S) final(S)
F flow(S) flow(S) flowR(S) flowR(S)
F {f : L→ L | f monoton}f` f`(A) = A\kill(`) ∪ gen(`)
Barbara Konig Modellierung, Analyse, Verifikation 54
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (I)
Eingabe: Instanz eines monotonen Frameworks
Ausgabe: MFP◦, MFP•
Schritt 1 (Initialisierung)W := F ;for all ` ∈ Lab do
if ` ∈ Ethen A[`] := ιelse A[`] := ⊥
fiod
Barbara Konig Modellierung, Analyse, Verifikation 55
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (II)
Schritt 2 (Iteration)while W 6= ∅ do
choose (`′, `) from W;W := W\{(`′, `)};if f`′(A[`′]) 6v A[`] then
A[`] := A[`] t f`′(A[`′]);for all `′′ with (`, `′′) ∈ F do
W := W ∪{(`, `′′)}od
fiod
Barbara Konig Modellierung, Analyse, Verifikation 56
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (III)
Schritt 3 (Ausgabe)for all ` ∈ Lab do
MFP◦(`) := A[`];MFP•(`) := f`(A[`])
od
Barbara Konig Modellierung, Analyse, Verifikation 57
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
Beispielprogramm:
[y := x]1;[z := 1]2;while [y>1]3 do
[z := z*y]4;[y := y-1]5
od;
[y:=0]6
Analyse der Reichweite von Zuweisungen
Barbara Konig Modellierung, Analyse, Verifikation 58
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y>1]3
[y:=0]6
[y:=y-1]5
∅
∅
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
Worklist:W = {(1, 2), (2, 3), (3, 6),(3, 4), (4, 5), (5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y:=y-1]5
[y:=0]6
[y>1]3
∅
∅
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
Worklist:W = {(1, 2), (2, 3), (3, 6),(3, 4), (4, 5), (5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y:=y-1]5
[y:=0]6
[y>1]3
∅
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
Worklist:W = {(2, 3), (3, 6), (3, 4),(4, 5), (5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y:=y-1]5
[y:=0]6
[y>1]3
∅
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
Worklist:W = {(2, 3), (3, 6), (3, 4),(4, 5), (5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y:=y-1]5
[y:=0]6
[y>1]3
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}Worklist:W = {(3, 6), (3, 4), (4, 5),(5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y:=y-1]5
[y>1]3
[y:=0]6
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}Worklist:W = {(3, 6), (3, 4), (4, 5),(5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
∅
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
∅
{(x, ?), (y, 1), (z, 2)}
Worklist:W = {(3, 4), (4, 5), (5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
∅
{(x, ?), (y, 1), (z, 2)}
∅
Worklist:W = {(3, 4), (4, 5), (5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
∅
{(x, ?), (y, 1), (z, 2)}
Worklist:W = {(4, 5), (5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
∅
Worklist:W = {(4, 5), (5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 4)}
Worklist:W = {(5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (z, 2)}
Worklist:W = {(5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[z:=z*y]4
[y>1]3
neu!
neu!
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}Worklist:W = {(3, 6), (3, 4)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (z, 2)}
Worklist:W = {(3, 6), (3, 4)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
Worklist:W = {(3, 4)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (z, 2)}
Worklist:W = {(3, 4)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
neu!
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
Worklist:W = {(4, 5)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (z, 4)}
Worklist:W = {(4, 5)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
neu!
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 4)}
Worklist:W = {(5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
Worklist:W = {(5, 3)}
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
Worklist:W = ∅
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Gleichungssystem
Gleichungssystem zur Datenflussanalyse:
(3.1) A◦(`) =⊔{A•(`′) | (`′, `) ∈ F} t ι`E
wobei ι`E =
{ι falls ` ∈ E⊥ sonst
(3.2) A•(`) = f`(A◦(`))
Kombiniert:
A◦(`) =⊔{f`′(A◦(`
′)) | (`′, `) ∈ F} t ι`E
Barbara Konig Modellierung, Analyse, Verifikation 60
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Werkzeuge, die Datenflussanalyse einsetzen
Eine unvollstandige Auswahl:
Compiler (C-Compiler, etc.)
Java Virtual Machine (Java Bytecode Verifier)
Programmanalyse-Generator mit WWW-Interface:PAG/WWW
Kommerzielle Anbieter von Programmanalyse-Software:
AbsInt – http://www.absint.com
PolySpace –http://www.mathworks.com/products/polyspace/
Barbara Konig Modellierung, Analyse, Verifikation 61
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Demo: Optimierung im GNU C Compiler
Verwendung des Stacks in ubersetzten Programmen beimMethodenaufruf:
Parameter k
...
Parameter 1
Lokale
Variable
Administra-
tiver Teil
Stack
Arbeits-
StackPointer
Pointer
%esp
%ebp
Administrativer Teil:Gesicherter Base-Pointer,Rucksprungadresse, etc.
Base
RichtungdesStack-Wachstums
Kleinere Adressen
Großere Adressen
In modernenRechnerarchitekturenwerden die Parameteraus Effizienzgrundeninzwischen vorrangig inRegistern ubergeben.
Barbara Konig Modellierung, Analyse, Verifikation 62
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Ausblick
Weitere Fragestellungen bei Datenflussanalyse:
Interprozedurale Analyse (Prozeduraufrufe,Parameterubergabe, Laufzeitstack)bisher: Intraprozedurale Analyse
Analyse von Pointer-Strukturen bzw. Objektstrukturen
Points-to-AnalyseAlias AnalysisShape Analysis
Barbara Konig Modellierung, Analyse, Verifikation 63
top related