Analisi e Verifica di Programmi Laboratorio di AVP Corso di Laurea in Informatica AA 2009-10 Tino...

Analisi e Verifica di Programmi

Laboratorio di AVP

Corso di Laurea in InformaticaAA 2009-’10

Tino Cortesi

Tino Cortesi Analisi e Verifica di Programmi 2

Analisi e VerificaCosa

Individuare proprietà interessanti dei nostri programmi:Valori prodotti, dipendenze, uso, terminazione

Perché:Verifica, Debugging

Type checkingVerifica di asserzioni

Ottimizzazioni:Compile time garbage collectionOttimizzazioni source-to-source

ComeLe proprietà non banali dei programmi sono indecidibili o computazionalmente molto costose (NP)Approssimazioni o condizioni sufficienti


L’impatto degli errori run-time

Il 50% degli attacchi alla sicurezza dei sistemi avviene tramite buffer overruns (Microsoft Security Bulletins MS02-065, MS04-111 etc.La maggior parte dei crash in sistemi embedded è dovuta a overflow di vario tipo.


Guyana francese, 4 giugno 1996

Lancio di ARIANE 5$600 miliardi di dollari bruciati per un errore del software: un dato a 64 bit in virgola mobile venne convertito in un intero a 16 bit con segno, questa operazione causò una trap del processore:il numero in virgola mobile era troppo grande per poter essere rappresentato con un intero a 16 bit.(autodistruzione a 39 secondi dal lancio)


Marte, Mars Polar Lander si spegne il 3 dicembre 1999per una variabile non inizializzata.


Sillabo del corsoElementi di Teoria dei ReticoliInterpretazione Astratta

Correttezza dell’analisi - Connessioni di Galois - WideningApplicazioni a problemi di sicurezzaApplicazioni nell’ambito delle basi di dati

Dataflow AnalysisLiveness AnalysisReaching Definitions - Constant Folding - Available ExpressionsBasic Blocks - Value Numbering - Alias AnalysisLoop Optimizations

Model CheckingSeminari di ricerca su temi di Analisi e Verifica di ProgrammiProgetto: realizzazione guidata di codice per un’analizzatore statico


BibliografiaF.Nielson, H.R.Nielson, C. Hankin Principles of Static AnalysisSpringer Verlag, 2004

B. Berard et al. Systems and Software VerificationSpringer Verlag, 1999

B,A,Davey, H,A, Priestly; Introduction to Lattices and Orders, Cambridge, 2006

Altri testi utili:

A. W. Appel, Modern Compiler Implementation in JavaCambridge Univ. Press, 1998

Steven Mucknick, Compiler Design ImplementationMorgan Kaufmann Publ., 1997

Articoli su journals o proceedings di conferenze

Introduzione


AnalisiMetodo conoscitivo che procede dall’individuazione e dallo studio dei particolariScomposizione di un tutto organico nelle sue parti


Analisi Statica di Programmi

Tecniche automatiche per inferire a tempo di compilazione informazione approssimata sul comportamento run-time dei programmi

Applicazioni:Ottimizzazione di compilatoriVerifica automatica dei programmiCertificazione - validazione del softwareSicurezza


EsempioCosa voglio verificare: assenza di un certo tipo di errori run-time (es. overflow)

Come posso astrarre i valori numerici: Intervalli - Poliedri (disuguaglianze lineari)

Quale teoria posso usare: Interpretazione astratta


Etichettatura

input n;

m:=2;

while n>1 dom:= m * n;

n:= n-1;

output m;

(1) input n;(2) m:=2;

while (3) n>1 do

(4) m:= m * n; (5) n:= n-1;

(6) output m;


Grafo di flusso

(1) input n;(2) m:=2;

while (3) n>1 do (4) m:= m * n; (5) n:= n-1;

(6) output m;

input n

m:= 2

n > 1

m:= m*n

n:= n-1 output m

1

2

3

6

4

5


Possiamo inferire mediante analisi statica che al punto (6) il valore della variabile m sarà pari per qualsiasi valore di input n.

Per fare questo l’analisi dovrà propagare “parity information”

Possiamo assegnare ad ogni variabile uno dei tre “valori”:

Pari il valore è sicuramente pari

Dispari il valore è sicuramente dispari

Non_So il valore può essere pari oppure dispari

input n

m:= 2

n > 1

m:= m*n

n:= n-1 output m

1

2

3

6

4

5


(1) input n;

(2) m:= 2;

while (3) n>1 do

(4) m:= m * n;

(5) n:= n - 1;

(6) output m;

(1) n Non_Som Non_So

(2) n Non_Som Non_So

(3) n Non_Som Pari

(4) n Non_Som Pari

(5) n Non_Som Pari

(6) n Non_Som Pari


Questo programma, dato un intero positivo n, calcola il doppio del fattoriale: 2 * (n!)

n=1 … l’output è 2n=2 … l’output è 4n=3 … l’output è 12n=4 … l’output è 48

pari!

(1) input n;

(2) m:= 2;

while (3) n>1 do

(4) m:= m * n;

(5) n:= n - 1;

(6) output m;


Questo programma, dato un intero positivo n, calcola il fattoriale: n!In questo caso l’analisi precedente non restituisce nessuna informazione utile sulla parità di m.Questo è corretto (per n=1…)Ma nemmeno se restringiamo l’input a n pari e n>1 l’analisi è precisa: in (3) sia n che m sono Non_So.

(1) input n;

(2) m:= 1;

while (3) n>1 do

(4) m:= m * n;

(5) n:= n - 1;

(6) output m;


Precisione e CorrettezzaQuesta perdita di precisione è una caratteristica comune delle tecniche di analisi staticaLa maggior parte delle proprietà sui programmi che si vogliono inferire sono indecidibili (o NP-complete), quindi non possiamo pensare di inferirle con precisione (ed in tempi ragionevoli)Dobbiamo assicurarci che il risultato dell’analisi sia in ogni caso corretto:

Se l’analisi dice SI allora sicuramente la proprietà è verificataSe l’analisi dice NO allora può darsi che la proprietà non sia verificata


EsempioSappiamo che il problema della terminazione è indecidibile (halting problem)

programmi

programmi che terminano


programmi

programmi che sicuramente terminano

programmi che terminano

programmi che potrebbero terminare


Precisione e CorrettezzaUn’analisi di terminazione può essere quindi di due tipi:“Definite”

SI il programma sicuramente terminaNO il programma potrebbe non terminare

“Possible” SI il programma può terminareNO il programma sicuramente non termina


Precisione e CorrettezzaLe tecniche di analisi che introdurremo si dicono “semantics-based”.Questo significa che l’informazione ottenuta dall’analisi può essere dimostrata corretta rispetto alla semantica del linguaggio di programmazione


Compilatori ottimizzantiUn compilatore ottimizzante trasforma un programma per migliorare la sua efficienza senza modificarne l’output.Trasformazioni che migliorano l’efficienza:

Allocazione dei registriEliminazione delle sotto-espressioni comuni: se una espressione viene calcolata più di una volta, elimina le ripetizioniEliminazione di “dead-code”: cancella una computazione il cui risultato non viene mai usato“Constant folding”: se gli operandi di un’espressione sono costanti, il calcolo può essere fatto a tempo di compilazione.


Escape AnalysisConsideriamo queste due procedure in C:

typedef int A[10000];

typedef A* B;

void esegui1(){

int i;

B b;

b = (A*) malloc(sizeof(A));

for (i=0; i<100; i++)

(*b)[i]=0;

free(b);

}

void esegui2(){

int i;

A a;

for (i=0; i<100; i++)

a[i]=0;

}


typedef int A[10000];typedef A* B;void esegui1(){

int i;B b;b = (A*) malloc(sizeof(A));for (i=0; i<100; i++)

(*b)[i]=0;free(b);

}

B b

int i

ambiente

stack

memoria

heap

0

L’array viene allocato nello heap e poi eliminato...


A a

int i

ambiente

stack

memoria

heaptypedef int A[10000];

void esegui2(){

int i;

A a;

for (i=0; i<100; i++)

a[i]=0;

}

L’array viene allocato nello stack e poi eliminato...

0


allocare nello heap costa...for (i=0; i<1000000; i++)

esegui1(); // circa 90 sec

for (i=0; i<1000000; i++)

esegui2(); // circa 35 sec

I programmi “sembrano” uguali, ma l’allocazione nello heap fa sì che il primo sia tre volte più lento del secondo...

Se riesco a “predire” che una variabile dinamica “non esce” dalla procedura dov’è introdotta, posso sostituirla con una variabile locale.


Esiste il compilatore ottimo?

Definiamo “fully optimizing compiler” un compilatore che trasforma un programma P nel programma Opt(P) che è il più piccolo programma con lo stesso output di P.Dato un programma Q che non produce nessun output e non termina, Opt(Q) è facile da trovare: è il programma L1: goto L1;Supponiamo di avere un fully optimizing compiler. Potremmo usarlo per risolvere il problema della terminazione: per vedere se esiste un input per il quale P termina, basta vedere se Opt(P) è il programma L1: goto L1;Ma sappiamo che il problema della terminazione è indecidibile, ovvero che non esiste nessun algoritmo che lo risolve. Quindi non può esistere nemmeno un fully optimizing compiler.


Ottimizzazione del codice

Control-FlowAnalysis

AnalisiTrasformazioni

Idea: anziché chiedere al programmatore di preoccuparsi dell’efficienza del programma, si può demandare a un compilatore ottimizzanti la trasformazione di un codice inefficiente in uno (equivalente) con performances migliori


Trasformazioni ottimizzanti

Le trasformazioni che un compilatore ottimizzante può operare seguono principalmente la seguente metodologia:

Analisi: attraversa il grafo di flusso del programma e raccogli informazioni su cosa può succedere a tempo si esecuzione

Trasformazioni: modifica il programma per renderlo in qualche modo più veloce. L’informazione ottenuta dall’analisi garantisce che il risultato del nuovo programma è uguale a quello del programma originario


Tecniche di Analisi StaticaPer definire un’analisi statica dobbiamo preoccuparci di:

Come specificarlaCome implementarla efficientementeCome provarne la correttezza


Principali tecnicheAbstract InterpretationValutazione ParzialeDataflow AnalysisControl Flow AnalysisModel CheckingType Systems

Analisi e Verifica di Programmi Laboratorio di AVP Corso di Laurea in Informatica AA 2009-10 Tino...

Documents

Transcript of Analisi e Verifica di Programmi Laboratorio di AVP Corso di Laurea in Informatica AA 2009-10 Tino...