1

Computergestützte Verifikation

21.6.2002

2

Probleme bei der Softwareverifikation

1. komplexe Datentypen und Expressions

2. Pointer und dynamische Datenstrukturen

3. Prozeduren und Rekursion

4. Bibliotheken

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)

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

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))

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”

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.

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);

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

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

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

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)

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”

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]

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

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

17

Fixpunktberechnung

nutzt nur etwas, wenn sie in endlich vielen Schrittenterminiert

Variante 1: endlicher abstrakter Verband

Variante 2: Terminierung forcieren Widening

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, ] [-, ]

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

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.

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

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]