Analisi e Verifica di Programmi
Laboratorio di AVP
Corso di Laurea in Informatica
AA 2004-’05
Tino Cortesi
Analisi e Verifica
Cosa
Individuare proprietà interessanti dei nostri programmi:
Valori prodotti, dipendenze, uso, terminazione
Perché:
Verifica, Debugging
Type checking
Verifica di asserzioni
Ottimizzazioni:
Compile time garbage collection
Ottimizzazioni source-to-source
Come
Le proprietà non banali dei programmi sono indecidibili o
computazionalmente molto costose (NP)
Approssimazioni o condizioni sufficienti
Tino Cortesi
Analisi e Verifica di Programmi
2
Guyana francese, 4 giugno 1996
$600 miliardi di dollari bruciati per
un errore del software
Tino Cortesi
Analisi e Verifica di Programmi
3
Marte, 3 dicembre 1999
Crashed due to uninitialized
Tino Cortesi
Analisi e Verifica di Programmi
variable
4
Sillabo del corso
Introduzione
Interpretazione Astratta
Correttezza dell’analisi - Connessioni di Galois - Widening
Domini astratti per l’analisi di linguaggi dichiarativi
Domini astratti per l’analisi di linguaggi ad oggetti
Dataflow Analysis
Liveness Analysis
Reaching Definitions - Constant Folding - Available Expressions
Basic Blocks - Value Numbering - Alias Analysis
Loop Optimizations
Model Checking
Type Systems
Tino Cortesi
Analisi e Verifica di Programmi
5
Bibliografia
F.Nielson, H.R.Nielson, C. Hankin
Principles of Static Analysis
Springer Verlag, 1999
A. W. Appel
Modern Compiler Implementation in Java
Cambridge Univ. Press, 1998
Steven Mucknick
Compiler Design Implementation
Morgan Kaufmann Publ., 1997
Articoli su journals o proceedings di conferenze
Tino Cortesi
Analisi e Verifica di Programmi
6
Introduzione
Analisi
Metodo conoscitivo che procede dall’individuazione e
dallo studio dei particolari
Scomposizione di un tutto organico nelle sue parti
Tino Cortesi
Analisi e Verifica di Programmi
8
Analisi di Programmi
Tecniche automatiche per inferire a tempo di
compilazione informazione approssimata sul
comportamento run-time dei programmi
Applicazioni:
Ottimizzazione di compilatori
Verifica automatica dei programmi
Certificazione - validazione del software
Sicurezza
Tino Cortesi
Analisi e Verifica di Programmi
9
Etichettatura
input n;
m:=2;
while n>1 do
m:= m * n;
n:= n-1;
output m;
Tino Cortesi
(1) input n;
(2) m:=2;
while (3) n>1 do
(4) m:= m * n;
(5) n:= n-1;
(6) output m;
Analisi e Verifica di Programmi
10
Grafo di flusso
1
input n
(1) input n;
(2) m:=2;
while (3) n>1 do
(4) m:= m * n;
(5) n:= n-1;
(6) output m;
2
m:= 2
3
n>1
4
m:= m*n
5
n:= n-1
Tino Cortesi
Analisi e Verifica di Programmi
6
output m
11
Possiamo inferire mediante analisi statica
che al punto (6) il valore della variabile m
sarà pari per qualsiasi valore di input n.
1
input n
2
Per fare questo l’analisi dovrà propagare
“parity information”
m:= 2
3
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
Tino Cortesi
Analisi e Verifica di Programmi
n>1
4
m:= m*n
5
n:= n-1
6
output m
12
(1) n Non_So
(1) input n;
(2)
(2) m:= 2;
while (3) n>1 do
(3)
(4) m:= m * n;
(4)
(5) n:= n - 1;
(5)
(6) output m;
(6)
Tino Cortesi
Analisi e Verifica di Programmi
m
n
m
n
m
n
m
n
m
n
m
Non_So
Non_So
Non_So
Non_So
Pari
Non_So
Pari
Non_So
Pari
Non_So
Pari
13
Questo programma, dato un
intero positivo n, calcola il
doppio del fattoriale: 2 * (n!)
(1) input n;
(2) m:= 2;
while (3) n>1 do
(4) m:= m * n;
n=1
n=2
n=3
n=4
(5) n:= n - 1;
(6) output m;
…
…
…
…
l’output
l’output
l’output
l’output
è
è
è
è
2
4
12
48
pari!
Tino Cortesi
Analisi e Verifica di Programmi
14
(1) input n;
(2) m:= 1;
while (3) n>1 do
(4) m:= m * n;
(5) n:= n - 1;
(6) output m;
Tino Cortesi
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.
Analisi e Verifica di Programmi
15
Precisione e Correttezza
Questa perdita di precisione è una caratteristica comune delle
tecniche di analisi statica
La 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à è verificata
Se l’analisi dice NO allora può darsi che la proprietà non sia
verificata
Tino Cortesi
Analisi e Verifica di Programmi
16
Esempio
Sappiamo che il problema della terminazione è
indecidibile (halting problem)
programmi
programmi che
terminano
Tino Cortesi
Analisi e Verifica di Programmi
17
programmi che
potrebbero terminare
programmi che
sicuramente terminano
programmi
programmi che
terminano
Tino Cortesi
Analisi e Verifica di Programmi
18
Precisione e Correttezza
Un’analisi di terminazione può essere quindi di due
tipi:
“Definite”
SI
il programma sicuramente termina
NO
il programma potrebbe non terminare
“Possible”
SI
il programma può terminare
NO
il programma sicuramente non termina
Tino Cortesi
Analisi e Verifica di Programmi
19
Precisione e Correttezza
Le 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
Tino Cortesi
Analisi e Verifica di Programmi
20
Compilatori ottimizzanti
Un compilatore ottimizzante trasforma un programma
per migliorare la sua efficienza senza modificarne
l’output.
Trasformazioni che migliorano l’efficienza:
Allocazione dei registri
Eliminazione delle sotto-espressioni comuni: se una
espressione viene calcolata più di una volta, elimina le
ripetizioni
Eliminazione 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.
Tino Cortesi
Analisi e Verifica di Programmi
21
Escape Analysis
Consideriamo 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);
}
Tino Cortesi
Analisi e Verifica di Programmi
void esegui2(){
int i;
A a;
for (i=0; i<100; i++)
a[i]=0;
}
22
ambiente
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);
}
int
i
B
b
memoria
stack
heap
0
L’array viene allocato nello heap e poi eliminato...
Tino Cortesi
Analisi e Verifica di Programmi
23
ambiente
typedef int A[10000];
int
i
A
a
memoria
stack
heap
0
void esegui2(){
int i;
A a;
for (i=0; i<100; i++)
a[i]=0;
}
L’array viene allocato nello stack e poi eliminato...
Tino Cortesi
Analisi e Verifica di Programmi
24
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.
Tino Cortesi
Analisi e Verifica di Programmi
25
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.
Tino Cortesi
Analisi e Verifica di Programmi
26
Ottimizzazione del codice
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
Control-Flow
Analysis
Tino Cortesi
Analisi
Analisi e Verifica di Programmi
Trasformazioni
27
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
Tino Cortesi
Analisi e Verifica di Programmi
28
Tecniche di Analisi Statica
Per definire un’analisi statica dobbiamo preoccuparci
di:
Come specificarla
Come implementarla efficientemente
Come provarne la correttezza
Tino Cortesi
Analisi e Verifica di Programmi
29
Principali tecniche
Abstract Interpretation
Valutazione Parziale
Dataflow Analysis
Control Flow Analysis
Model Checking
Type Systems
Tino Cortesi
Analisi e Verifica di Programmi
30