1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe...

22
1 Computergestützte Verifikation 21.6.2002

Transcript of 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe...

Page 1: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

1

Computergestützte Verifikation

21.6.2002

Page 2: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

2

Probleme bei der Softwareverifikation

1. komplexe Datentypen und Expressions

2. Pointer und dynamische Datenstrukturen

3. Prozeduren und Rekursion

4. Bibliotheken

Page 3: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

3

Abstrakte Zustände

a¬ b

¬ a b

¬ a¬ b

a b

c d

¬ c dc¬d

¬ c¬ d

(¬ b ¬ d)(¬ a ¬ c¬ d)

Praxis: z.B. Repräsentation abstrakter Zustände als BDD

oder: Restriktion auf einfache Konjunktionen (im Beispiel: ¬ d)

Page 4: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

4

Abstrakter Nachfolger

geg.: Abstrakter Zustand a, guarded command g: x1..n:=T1..n

ges.: a’ so daß - jeder konkrete Zustand, der von einem von a repr. Zustand aus per g entsteht, von a’ repr. wird - a’ mglst. stark

a’: - false, falls a[bii]i=1..n ¬

Berechnung von a’ im allg. schwer, für Konjunktionen leichter:

- j = 1

n bj falls a[bii]i=1..n j [ xiTi]i=1..n

¬bj falls a[bii]i=1..n ¬j [ xiTi]i=1..n

true, sonst

Theorembeweiser

Page 5: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

5

Beispieltypedef struct cell{ int val; struct cell* next;} * list;

list partition(list *l, int v) { list curr, prev, newl, nextCurr;

curr = * l; prev = NULL; newl = NULL; while( curr != NULL) { nextCurr = curr -> next; if(curr -> val > v) { if(prev != NULL) { prev -> next = nextCurr; } if(curr == *l) { *l = nextCurr; } curr -> next = newl;L: newl = curr; } else { prev = curr; } curr = nextCurr; } return newl;}

void partition() {bool b1,b2,b3,b4;

b1 = unknown();b3 = unknown();b2 = true;b4 = unknown();skip;while(*) { assume(!b1); skip; if(*) { assume(b3) if(*) { assume(!b2); skip; } if(*) { skip; } skip;L: skip; } else { assume(!b3); b2 = b1; b4 = b3; } b1 = unknown(); b3 = unknown(); } assume(b1);}

b1: curr==NULLb2: prev==NULLb3: curr->val>vb4: prev->val>v

AG(@L curr!=NULL AND curr->val>v AND (prev->val<=v OR prev=NULL))AG(@L !b1 AND b3 AND (!b4 OR b2))

Page 6: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

6

Pointer

bisher: wpre(x := E,) = [ x E]

stimmt nicht, wenn Pointer beteiligt sind:

Beispiel: Sei p = & x; wpre(x = 3, *p > 5) != *p > 5

(für einen potentiellen Alias y) wpre(x := E, ) = ( ( &x = &y [y E]) ( &x != &y ) )

Nichtdeterminismus, es sei denn, Alias-Analyse kann eineAlternative ausschließen: “may point to”, “may not point to”

Page 7: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

7

Bedingungen

IF B THEN T ELSE E END

IF * THEN assume(X); T ELSE assume(Y); END

X: das stärkste Prädikat (über den gegebenen Prädikaten) das von B impliziert wird

Y: das stärkste Prädikat (über den gegebenen Prädikaten) das von ¬B impliziert wird

zwischen X und Y kann Lücke klaffen Nichtdet.

Page 8: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

8

ProzedurenBeispiel

int bar(int * q, int y) { int l1,l2; .... return l1;}

void foo(int * p, int x) { int r; ..... r = bar(p,x);}

Prädikate

bar:b1: y >= 0b2: *q <=yb3: y == l1b4: y > l2

foo:b5: *p <= 0b6: x == 0b7: r == 0

form. parrück + ref

[bool,bool] bar(b1,b2){

bool b3,b4;...return [b2,b3];

}

void foo(b5,b6){ bool b7,t1,t2,t3,t4; ... t1 = t2 = [t3,t4] = bar(t1,t2); b5 = b7 =}

bool choose(b1,b2) {if(b1) return true;

if(b2) return false;return unknown();

}

x==0 y>=0x==0 *p<=0 *q<=yx==0 ! *p<=0 ! *q<=y

choose(b6,false);choose(b6b5,b6!b5);

(y==)x==0 *q<=y *p<=0(y==)x==0 ! *q<=y ! *p<=0(y==)x==0 y==l1 r==0(y==)x==0 ! y==l1 ! r==0

choose(t3b6,t3!b6);choose(t4b6,t4!b6);

Page 9: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

9

Prozeduren

Also: anfangs Prädikate der rufenden Prozeduren in Prädikate der gerufenen Prozedur übersetzen, am Ende umgekehrt

Alternativen: - Inlining (mit Tiefenbegrenzung bei Rekursion) - Fixpunktberechnung 8.2

Page 10: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

10

8.2 Abstract InterpretationConcrete Interpretation = Menge der Variablenbelegungen,die an einer geg. PC-Position im Laufe des Programmsvorkommen können.

M x := E { ( \ {[x,(x)]}) {[x,(E)]}| M}

M IF B THEN M B .... M1 ELSE M ¬ B .... M2 END M1 M2

M WHILE B DO X ..... F(X) END

F’(Y) := (MF(Y)) B(M F(MB)) B.....

i=0 F’i(Ø) kleinster Fixpunkt von F’ (F’(Z) = Z)

Ø

MB

Page 11: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

11

Wichtige Rechenoperationen

, und “kleinster Fixpunkt” = unendliche Vereinigung

= Rechnen auf vollständigem Verband

[M, , ] ist Verband, falls – beide Operationen komm., ass. - Absorption

ggf. neutrale Elemente

vollständig = abgeschlossen geg. unendliche Vereinigung

Verband induziert Halbordnung: x y gdw. x y = x (gdw. x y = y)

ist gr. untere Schranke, ist kl. obere Schranke von

Page 12: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

12

Idee von Abstract Interpretation

Rechnen im konkretem Verband Rechnen in einem “passenden” abstrakten Verband

Beispiele für abstrakte Verbände:

Zahlenintervalle [a,c][b,d] = [max(a,b),min(c,d)] [a,c][b,d] = [min(a,b),max(c,d)]

Boolesche Funktionen mit ,

Zonen mit Schnitt und konvexer Hülle der Vereinigung

Kreuzprodukte beliebiger Verbände (, komponentenweise)

Page 13: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

13

“passend” = Galois-Verbindung

Konkret: [C,,] Abstrakt: [A,,]

Abstraktionsfunktion : C AKonkretisierungsfunktion : A C

() ist Galoisverbindung, wenn (x) Y gdw. x (Y)

Insbesondere: z ((z)) (x := z, Y := (z) ) ((Z)) Z (x := (Z)), Y := Z )

– “präziseste Abstraktion” – “liberalste Interpretation”

Page 14: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

14

Beispiel für Galois-Verbindung

C = Mengen ganzer Zahlen A = Intervalle reeller Zahlen

(M) := [min(M),max(M)] (Ø) = (I) := I Z

({1,2,5}) = [1,5] ([1,5]) = {1,2,3,4,5}([-,]) = {-3,-2,-1,0,1,2,3} = [-3,3]

Page 15: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

15

Approximation von Funktionen

geg.: F: C C F*: A A

F* approximiert F wenn für alle x in C: F(x) (F*((x)))

Satz: Seien F, F* monoton, F* approximiert F. Sei Z kleinster Fixpunkt von F Z* kleinster Fixpunkt von F*Dann: Z (Z*)

Rechnen in einem Galois-verbundenen abstrakten Verband approximiert alle entsprechenden Rechnungen im konkreten Verband korrekt

Page 16: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

16

Beispiel für abstrakte Interpretation

x = x / 2;

while(x<7) {

x = x + 3;

x = 2 * x;

}

[0,5]

[0,2]

[0,2] [0,6] [0,6]

[3,5] [3,9]

[6,10] [6,18]

[7,18]

(8,10,18) in konkreter Interpretation

wichtiger Unterschied zuModel Checking:

pro PC jederzeit nur ein Objekt

Page 17: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

17

Fixpunktberechnung

nutzt nur etwas, wenn sie in endlich vielen Schrittenterminiert

Variante 1: endlicher abstrakter Verband

Variante 2: Terminierung forcieren Widening

Page 18: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

18

Widening

= Zwischenergebnis bei Fixpunktberechnung bewußt vergrößern

Vorteil: Terminierung in endlich vielen Schritten

Nachteil: berechneter Fixpunkt ist nicht notwendigerweise der kleinste

Beispiel: Widening: instabile Grenzen auf min(- 0,1)/max(0,1,)

[64,70] [32,71] [1, ] [0, ] [64,70] [63,71] [1, ] [0, ] [-, ]

Page 19: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

19

Widening formal

: A A heißt Widening falls - X X Y (alle X,Y) - Y X Y (alle X,Y)

und für keine mon. wachsende Folge X0, X1, ...ist die Folge Y0 := X0 Yi+1 := Yi Xi+1stark monoton

Satz: Für jeden monotonen Operator F liefert die folgendeIteration nach endlich vielen Schritten einen Fixpunkt:X0 := , Xi+1 := Xi falls F(Xi) Xi, := Xi F(Xi) sonst

Page 20: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

20

Narrowing

= den durch Widening entstandenen Schaden begrenzen:

Def.: ist Narrowing falls

x y x y x y und für keine monoton fallende Kettex0, x1, ..., ist die Folgey0 := x0, yi+1 := yi x i+1 stark monoton fallend.

Page 21: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

21

Beispiel für Widening/Narrowing

int i

i = 1;[1,1]while (i < 101) {

i = i +1;

}

[a,b] [c,d] = [if c<a then - else a, if d>b then else b][a,b] [c,d] = [if a = - then c else a, if b = then d else b]

{X}X0 = X1 =X0 (( [1,1] X0 [1,1]) [- ,100]) = (( [1,1] [1,1]) [- ,100]) = [1,1]X2 = X1 (( [1,1] X1 [1,1]) [- ,100]) = [1,1] (( [1,1] [1,1] [1,1]) [- ,100]) = [1,1] [1,2] = [1, ]X3 = [1, ] (( [1,1] [1, ] [1,1]) [- ,100]) = [1, ] [1,100] = [1, ] X2

Page 22: 1 Computergestützte Verifikation 21.6.2002. 2 Probleme bei der Softwareverifikation 1.komplexe Datentypen und Expressions 2.Pointer und dynamische Datenstrukturen.

22

Beispiel für Widening/Narrowing

int i

i = 1;[1,1]while (i < 101) {

i = i +1;

}

[a,b] [c,d] = [if c<a then - else a, if d>b then else b][a,b] [c,d] = [if a = - then c else a, if b = then d else b]

{X}Y0 = X2 = [1, ]Y1 = Y0 (( [1,1] ( Y0 [1,1])) [- ,100]) = [1, ] [1,100] = [1,100]Y2 = Y1 (( [1,1] ( Y1 [1,1])) [- ,100]) = [1, 100 ] [1,100] = [1,100] = Y1

ultimativer Fixpunkt nach Widening und Narrowing = [1,100]