General Framework
Framework
Nonostante le differenze tra le analisi viste finora (Reaching
Definitions, Available Expressions, Very Busy Expressions,
Liveness), è facile osservarne le similarità
Il vantaggio di un framework unificante sta soprattutto nella
possibilità di progettare un algoritmo generico che possa essere
istanziato per ottenere le diverse analisi.
Tino Cortesi
Tecniche di Analisi di Programmi
2
Catalogare Dataflow analyses
Possible
Analysis
Forwards
Backwards
Tino Cortesi
Definite
Analysis
Reaching
definitions
Available
expressions
Live variables
Very busy
expressions
Tecniche di Analisi di Programmi
3
Reaching Definitions
i = {(x,?) | x è una variabile del programma}
i se p è il punto iniziale
RDentry(p)=
U { RDexit(q) | q precede p}
RDexit(p)= (RDentry(p) \ killRD(p) ) U genRD(p)
Tino Cortesi
Tecniche di Analisi di Programmi
4
Available Expressions
 se p è il punto iniziale
AEentry(p)=
 { AEexit(q) | (q,p) è un arco del grafo}
AEexit(p)= (AEentry(p) \ killAE(p)) U genAE(p)
Tino Cortesi
Tecniche di Analisi di Programmi
5
Very Busy Expressions
 se p è un punto finale
VBexit(p)=
 { VBentry(q) | (p,q) è un arco del grafo}
VBentry(p)= (VBexit(p) \ killVB(p)) U genVB(p)
Tino Cortesi
Tecniche di Analisi di Programmi
6
Liveness Analysis
genLV(p)= use[p]
killLV(p) = def[n]
 se p è un punto finale
LVexit(p)=
U { LVentry(q) | q segue p}
LVentry(p)= (LVexit(p) \ killLV(p) ) U genLV(p)
Tino Cortesi
Tecniche di Analisi di Programmi
7
Il pattern comune
i
se p  E
GA(p)=
 { GA(q) | q  F } altrimenti
GA(p)= f ( GA(p) )
dove:
E sono i punti iniziali o terminali del grafo
i specifica l’informazione iniziale o finale
F è l’insieme di punti del grafo successivi o precedenti
 è un’operazione insiemistica di intersezione o unione
f è la “transfer function” associata ai nodi del grafo
Tino Cortesi
Tecniche di Analisi di Programmi
8
Forward vs Backwards
i
se p  E
GA(p)=
 { GA(q) | q  F } altrimenti
GA(p)= f ( GA(p) )
•
Nelle forward analyses E è il punto iniziale, F è pred[p], GA è
GAentry e GA è GAexit
•
Nelle backward analyses E è il punto finale, F è succ[p], GA è
GAexit e GA è GAentry
Tino Cortesi
Tecniche di Analisi di Programmi
9
Possible vs Definite
i
se p  E
GA(p)=
 { GA(q) | q  F } altrimenti
GA(p)= f ( GA(p) )
•
Quando  è l’intersezione, richiediamo l’insieme più grande
che soddisfa le equazioni su tutti i cammini di esecuzione: si
tratta quindi di definite analysis
•
Quando  è l’unione, richiediamo l’insieme più piccolo che
soddisfa le equazioni su almeno un cammino di esecuzione: si
tratta quindi di possible analysis
Tino Cortesi
Tecniche di Analisi di Programmi
10
Esercizio
Utilizzare l’analizzatore statico disponibile nel sito
http://pag.cs.uni-sb.de/
per sperimentare le quattro tipologie di analisi viste a lezione su
diversi programmi.
Tino Cortesi
Tecniche di Analisi di Programmi
11
Esercizio
La upwards exposed uses analysis è l’analisi duale della
reaching definitions analysis:
associa ad ogni punto p del grafo i punti del grafo nei quali la
dichiarazione contenuta nel punto p potrebbe essere utilizzata.
E’ un’analisi forward o backward? E’ un’analisi “possible” o
“definite”?
Formalizzare l’analisi utilizzando RD
Tino Cortesi
Tecniche di Analisi di Programmi
12
General Framework
Terminazione e Correttezza di un
Algoritmo Generico
Spazio delle proprietà
Qual’è l’insieme usato per descrivere l’informazione che si vuole derivare?
Si richiede che tale insieme di valori sia un reticolo completo
Es.: Reaching Definition Analysis:
L = (Var  Lab?)
=
lub = 
(inclusione tra insiemi)
Es.: Per la Available Expression Analysis:
L = (AExp)
(espressioni aritmetiche)
=
(inclusione tra insiemi)
lub = 
Tino Cortesi
Tecniche di Analisi di Programmi
14
Funzioni di transfer
E’ necessario un insieme di funzioni di transfer
f l: L  L
l  Lab
Tali funzioni devono essere monotone
l  l’  fl(l)  fl(l’)
se si aumenta la conoscenza sull’input, anche la conoscenza
sull’output deve aumentare
Deve esistere un insieme F di funzioni monotone L  L tale che
F contiene tutte le funzioni di transfer fl
F contiene la funzione identità
F è chiuso rispetto alla composizione di funzioni
Tino Cortesi
Tecniche di Analisi di Programmi
15
General Framework
Riassumendo, un Framework Monotono per Analisi Dataflow
costituito da:
1.
2.
un reticolo completo L che soddisfa la condizione sulle catene
ascendenti
un insieme F di funzioni monotone da L a L che contiene
l’identità ed è chiuso sotto composizione
Nelle 4 analisi viste, l’insieme F può essere in tutti e 4 i casi
definito come
F = { f: L  L | " l L $ lk,lg  L: f(l)=(l - lk)  lg }
Tino Cortesi
Tecniche di Analisi di Programmi
16
General Framework
3.
Una relazione di flusso F (ad esempio succ[] o pred[],...)
4.
Un insieme delle etichette iniziali E (ad esempio i punti iniziali
del grafo di flusso o le sue foglie)
5.
Un valore iniziale i per le etichette iniziali in E
6.
Una funzione f che mappa le etichette dei nodi in F o in E nelle
corrispondenti funzioni di transfer in F
Tino Cortesi
Tecniche di Analisi di Programmi
17
Equazioni dell’Analisi
i
se l  E
GA(l)=
lub { GA(l’) | (l’, l)  F } altrimenti
GA(l)= fl ( GA(l) )
dove:
E sono i punti iniziali o terminali del grafo
i specifica l’informazione iniziale o finale
F è l’insieme di archi del grafo successivi o precedenti
fl è la transfer function di F associata al nodo
Tino Cortesi
Tecniche di Analisi di Programmi
l del grafo
18
Algoritmo Generico
L’algoritmo ha in input un’istanza del General Framework.
Utilizza un array (Analysis) indicizzato sulle etichette del grafo,
che contiene l’informazione in entrata (o uscita, nel caso di
analisi backward) di ogni punto del programma. Tale
informazione sarà un elemento del dominio L.
L’algoritmo fa uso di una lista ausiliaria W. W è una lista di
coppie: ogni coppia è un elemento della relazione di flusso F.
la presenza di una coppia (l, l’) nella lista W indica che
l’analisi ha modificato l’informazione in uscita (o in entrata,
nel caso si analisi backward) del punto l, e che quindi
bisognerà ricalcolare l’analisi dell’entrata del punto l’ (o
dell’uscita, nel caso si analisi backward).
Tino Cortesi
Tecniche di Analisi di Programmi
19
Algoritmo Generico
input: un’istanza del
framework
(L, F , F, E, i, f)
output: GA, GA
metodo:
passo 1 (inizializzazione)
W:= nil
for all (l, l’) in F do
W:= cons((l, l’),W)
for all l in F or E do
if l  E Analysis[l]:=i
else Analysis[l]:= ^L
Tino Cortesi
passo 2 (iterazione)
while W  nil do
l := fst(head(W))
l’ := snd(head(W))
W:= tail(W)
if not fl(Analysis[l])  Analysis[l’]
Analysis[l’] =
lub(Analysis[l’], fl(Analysis[l]))
for all l” con (l’, l”) in F do
W:= cons((l’, l”),W)
passo 3 (risultato)
per ogni l in F o E do
GA(l) = Analysis[l]
GA(l) = fl(Analysis[l])
Tecniche di Analisi di Programmi
20
Terminazione
Cosa ci garantisce che l’algoritmo termini sempre?
Due condizioni:
1.
le operazioni (in particolare la funzione di transfer)
devono essere monotone:
x  y  f(x)  f(y)
2.
il dominio è un reticolo completo senza catene
ascendenti infinite
Teorema: una funzione monotona, su un reticolo completo
senza catene ascendenti infinite, converge in un numero finito
di passi.
Tino Cortesi
Tecniche di Analisi di Programmi
21
Terminazione
Per verificare che l’algoritmo termina
Tutte le variabili sono inizializzate all’insieme vuoto
Ad ogni iterazione, gli insiemi costruiti possono solo crescere
Per induzione sul numero di iterazioni, usando la
monotonia delle funzioni in F.
Gli insiemi non possono crescere all’infinito (il numero di
possibili elementi della catena è finito)
Tino Cortesi
Tecniche di Analisi di Programmi
22
Correttezza
Siano Analysis e Analysis le soluzioni minime dell’istanza del
General Framework in input
La prova di correttezza dell’algoritmo segue 4 passi successivi:
1.
ad ogni iterazione i valori nell’array Analysis sono contenuti nei
valori corrispondenti in Analysis ovvero nel loop vale il seguente
invariante:
" l : Analysis[l]  Analysis(l)
2.
quando il loop termina
" (l, l’)  F : fl(Analysis[l])  Analysis[l’]
3.
quando il passo 2 termina
" l : Analysis[l]  i
" l : Analysis[l]  lub{ fl’(Analysis[l’]) | (l, l’)  F}
4.
dalla definizione di Analysis e dal teorema di Tarski segue che
Analysis(l) = lub (lub{ fl’(Analysis[l’]) | (l, l’)  F}, i)
5.
dal punto 4 e dalla def. di GA(l):
e quindi per 1:
Tino Cortesi
Tecniche di Analisi di Programmi
" l : GA(l)  Analysis[l]
" l : GA(l) = Analysis[l]
23
CFA di problemi distributivi e
di problemi non distributivi
Problemi Dataflow Distributivi
La monotonicità di una funzione f su insiemi implica che
f(x  y)  f(x)  f(y)
Un problema dataflow si dice distributivo se la funzione
corrispondente soddisfa una condizione più forte:
f(x  y) = f(x)  f(y)
In generale, un problema dataflow si dice distributivo se
f(lub(x,y)) = lub(f(x), f(y))
Tino Cortesi
Tecniche di Analisi di Programmi
25
Esempio di f distributiva
{1,2,3}
{1,2}
{1}
{1,3}
{2}
{1,2,3}
{2,3}
{1,2}
{3}
{1}
{2}
{2,3}
{3}


Tino Cortesi
{1,3}
Tecniche di Analisi di Programmi
26
Esempio di f non distributiva
{1,2,3}
{1,2}
{1}
{1,3}
{2}
{1,2,3}
{2,3}
{1,2}
{3}
{1}

Tino Cortesi
{1,3}
{2}
{2,3}
{3}

Tecniche di Analisi di Programmi
27
Esempio
f
g
h
k
k(h(f(0) U g(0))) =
k(h(f(0)) U h(g(0))) =
k(h(f(0))) U k(h(g(0)))
Tino Cortesi
Tecniche di Analisi di Programmi
L’analisi del grafo è
equivalente alla
combinazione del
risultato dell’analisi di
tutti i cammini.
28
DFA di un problema distributivo
Se un problema è distributivo, allora la (minima) soluzione al
sistema di equazioni che lo definisce è equivalente alla
combinazione dei risultati dell’analisi di tutti i cammini
(includendo quelli infiniti).
In questo caso l’unione non causa nessuna perdita di
informazione
Tino Cortesi
Tecniche di Analisi di Programmi
29
Quali problemi sono distributivi?
I problemi distributivi sono quelli “facili”...
Molte analisi che riguardano la struttura del programma sono
distributive
Ad es., live variables, available expressions, reaching
definitions, very busy expressions
Sono tutte proprietà che riguardano COME il programma
esegue la computazione.
Tino Cortesi
Tecniche di Analisi di Programmi
30
Problemi non distributivi
Sono tipicamente problemi non distributivi quelli legati all’analisi
di COSA il programma calcola.
Es.: l’output è una costante, un valore positivo, ecc.
Esempio: Constant Propagation Analysis
Per ogni punto del programma determinare se una variabile ha
esattamente lo stesso valore costante ogniqualvolta l’esecuzione
raggiunge quel punto
Si tratta di una analisi forward e definite.
Tino Cortesi
Tecniche di Analisi di Programmi
31
Constant Propagation Analysis
Lo spazio della proprietà oggetto dell’analisi è: (Var  ZT)^
dove:
Var è l’insieme delle variabili che occorrono nel programma
ZT= Z  {T} è parzialmente ordinato da:
"nZ:
" n1, n2  Z :
Tino Cortesi
z CP T
(n1 CP n2)  (n1 = n2)
Tecniche di Analisi di Programmi
32
Z
T
T
-4
-3
-2
-1
0
1
2
3
4
L= Z  {T}
"n Z : n T
Tino Cortesi
Tecniche di Analisi di Programmi
33
Il reticolo (Var  Z )^
T
In ZT , l’elemento massimo T serve a indicare che una variabile
non ha un valore costante
Un elemento s: Var  ZT è una funzione (parziale):
data una variabile x, s(x) dice se x è o meno una costante, e in
caso positivo (se s(x) è diverso da T) qual’è tale valore.
Il reticolo è completato con l’aggiunta di un elemento minimo ^
Tino Cortesi
Tecniche di Analisi di Programmi
34
L’ordine nel reticolo (Var  Z )^
T
L’ordine parziale nel reticolo (Var  ZT)^ è definito da:
" s  (Var  ZT)^ :
^s
" s1, s2  (Var  ZT)^: (s1  s2)  ( "xdom(s1) : s1(x) CP s2(x) )
Il least upper bound è definito da:
" s  (Var  ZT)^ : lub(^, s) = lub(s, ^) = s
" s1, s2  (Var  ZT)^
"xVar : lub(s1,s2)(x) = lub(s1(x) ,s2(x))
Tino Cortesi
Tecniche di Analisi di Programmi
è l’uguaglianza se
si(x) sono numeri!
35
({x,y}  ZT)^
T
{(x,1), (y,4)}
{(x,1), (y,2)}
{(y,4)}
{(x,1)}
{(y,7)}

^
Tino Cortesi
Tecniche di Analisi di Programmi
36
Analizzare le espressioni
Per specificare le funzioni di transfer è necessaria la seguente
funzione per analizzare le espressioni algebriche presenti nel
programma a partire da uno stato s in (Var  ZT)^
A: ( AExp  (Var  ZT)^ )  ZT^
A(x,s) = ^
s(x)
se s = ^
altrimenti
A(n,s) = ^
n
se s = ^
altrimenti
A(a1 op a2, s) = A(a1,s) op A(a2,s)
(dove op è l’interpretazione di op su ZT^: es. 4 op 2 = 8)
Tino Cortesi
Tecniche di Analisi di Programmi
37
Le funzioni di transfer
L’insieme di funzioni monotone, nel caso della Constant
Propagation Analysis è
F = { f : (Var  ZT)^  (Var  ZT)^ | f è monotona}
Le funzioni di transfer fl sono definite da:
se l è l’etichetta di un assegnamento [x:= a]l
fl(s) = ^
se s = ^
s[x  A(a,s)] altrimenti
se l è l’etichetta di un altro comando: fl(s) = s
Tino Cortesi
Tecniche di Analisi di Programmi
38
Esempio
Il programma
[x:=10]1; [y:=x+10]2; ([while x<y]3 [y:=y-1]4); [z:=x-1]5
La minima soluzione della Constant Propagation Analysis di questo
programma è:
CPentry(1) = 
CPexit(1) = {(x10)}
CPentry(2) = {(x10)}
CPexit(2) = {(x10), (y20)}
CPentry(3) = CPexit(3) = CPentry(4) = CPexit(4) = {(x10), (yT)}
CPentry(5) = {(x10), (yT)}
CPexit(5) = {(x10), (yT), (z9)}
Tino Cortesi
Tecniche di Analisi di Programmi
39
Non distributività
Per dimostrare che la Constant Propagation Analysis è non
distributiva, è sufficiente considerare il comportamento delle
funzioni di transfer fl sul comando [y:= x*x]l
si considerino due stati s1(x) = 1 e s2(x) = -1
in questo caso:
lub(s1,s2)(x) = T
e quindi
fl (lub(s1,s2))(y) = T
mentre
fl (s1)(y) = 1 = fl (s2)(y)
ovvero lub(fl (s1), fl (s2)) # fl (lub(s1,s2))
Tino Cortesi
Tecniche di Analisi di Programmi
40