General Framework. Tino CortesiTecniche di Analisi di Programmi 2 Framework Nonostante le differenze...

General Framework

Tino Cortesi Tecniche di Analisi di Programmi 2

FrameworkNonostante 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.


Catalogare Dataflow analyses

PossibleAnalysis

DefiniteAnalysis

Forwards Reaching definitions

Available expressions

Backwards Live variables Very busy expressions


Reaching Definitions = {(x,?) | x è una variabile del programma}

se p è il punto iniziale

RDentry(p)=

U { RDexit(q) | q precede p}

RDexit(p)= (RDentry(p) \ killRD(p) ) U genRD(p)


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)


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)


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)

Liveness Analysis


Il pattern comune

se p E

GA(p)=

{ GAœ(q) | q F } altrimenti

GAœ(p)= f ( GA(p) )

dove:E sono i punti iniziali o terminali del grafospecifica l’informazione iniziale o finaleF è l’insieme di punti del grafo successivi o

precedentiè un’operazione insiemistica di intersezione o

unionef è la “transfer function” associata ai nodi del grafo


Forward vs Backwards se p E

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


Possible vs Definite se p E

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


EsercizioUtilizzare 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.


EsercizioLa 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

General FrameworkTerminazione 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?)= (inclusione tra insiemi)lub =

Es.: Per la Available Expression Analysis:L = (AExp) (espressioni aritmetiche)= (inclusione tra insiemi)lub =


Funzioni di transferE’ necessario un insieme di funzioni di transfer

fl: 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


General Framework Riassumendo, un Framework Monotono per Analisi Dataflow costituito da:

1. un reticolo completo L che soddisfa la condizione sulle catene ascendenti

2. 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 | lL lk,lg L: f(l)=(l - lk) lg }


General Framework3. 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 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


Equazioni dell’Analisi

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 grafospecifica l’informazione iniziale o finaleF è l’insieme di archi del grafo successivi o

precedenti

fl è la transfer function di F associata al nodo l del grafo


Algoritmo GenericoL’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).


Algoritmo Genericoinput: un’istanza del

framework(L, F , F, E, , f)

output: GA, GAœ

metodo: passo 1 (inizializzazione)

W:= nilfor all (l, l’) in F do

W:= cons((l, l’),W)for all l in F or E do

if l E Analysis[l]:=else Analysis[l]:= L

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


TerminazioneCosa 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.


TerminazionePer verificare che l’algoritmo termina

Tutte le variabili sono inizializzate all’insieme vuotoAd 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)


CorrettezzaSiano Analysis e Analysisœ le soluzioni minime dell’istanza del General Framework in inputLa prova di correttezza dell’algoritmo segue 4 passi successivi:

1. ad ogni iterazione i valori nell’array Analysis sono contenuti nei valori corrispondenti in Analysisovvero 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] l : Analysis[l] lub{ fl’(Analysis[l’]) | (l, l’) F}

4. dalla definizione di Analysise dal teorema di Tarski segue che Analysis(l) = lub (lub{ fl’(Analysis[l’]) | (l, l’) F}, )

5. dal punto 4 e dalla def. di GA(l): l : GA(l) Analysis[l] e quindi per 1: l : GA(l) Analysis[l]

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 sef(lub(x,y)) = lub(f(x), f(y))


Esempio di f distributiva

{3}{2}{1}

{2,3}{1,3}{1,2}

{1,2,3}

{3}{2}{1}

{2,3}{1,3}{1,2}

{1,2,3}


Esempio di f non distributiva

{3}{2}{1}

{2,3}{1,3}{1,2}

{1,2,3}

{3}{2}{1}

{2,3}{1,3}{1,2}

{1,2,3}


Esempio

h

gf

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

L’analisi del grafo è equivalente alla combinazione del risultato dell’analisi di tutti i cammini.


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


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 expressionsSono tutte proprietà che riguardano COME il programma esegue la computazione.


Problemi non distributiviSono 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.


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 : z CPT

n1, n2 Z : (n1 CP n2) (n1 n2)


ZT

2 3 4 1 0 -1 -2 -3 -4

T

L= Z {T}

n Z : n T


Il reticolo (Var ZT)

In ZT , l’elemento massimo T serve a indicare che una variabile non ha un valore costante

Un elemento : Var ZT è una funzione (parziale): data una variabile x, xdice se x è o meno una costante, e in caso positivo (se xè diverso da T) qual’è tale valore.

Il reticolo è completato con l’aggiunta di un elemento minimo


L’ordine nel reticolo (Var ZT)

L’ordine parziale nel reticolo (Var ZT)è definito da:

(Var ZT) : 1, 2 (Var ZT): (1 2) ( xdom(1) : 1(x) CP 2(x) )

Il least upper bound è definito da:

(Var ZT) : lub(,) = lub(,) = 1, 2 (Var ZT)

xVar : lub(1,2)(x) = lub(1(x) ,2(x))

è l’uguaglianza se i(x) sono numeri!


({x,y} ZT)

T

{(x,1)}

{(x,1), (y,2)}

{(y,7)}

{(x,1), (y,4)}

{(y,4)}


Analizzare le espressioniPer specificare le funzioni di transfer è necessaria la seguente funzione per analizzare le espressioni algebriche presenti nel programma a partire da uno stato in (Var ZT)

A: ( AExp (Var ZT)) ZT

A(x,) = se = (x) altrimenti

A(n,) = se = n altrimenti

A(a1 op a2, ) = A(a1,)op A(a2,)

(dove op è l’interpretazione di op su ZT: es. 4 op 2 = 8)


Le funzioni di transferL’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() = se = [x A(a,)] altrimenti

se l è l’etichetta di un altro comando: fl() =


EsempioIl 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) = {(x10)}

CPentry(2) = {(x10)}

CPexit(2) = {(x10), (y20)}

CPentry(3) = CPexit(3) = CPentry(4) = CPexit(4) = {(x10), (yT)}

CPentry(5) = {(x10), (yT)}

CPexit(5) = {(x10), (yT), (z9)}


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 1(x) = 1 e 2(x) = -1in questo caso:

lub(1,2)(x) = Te quindi

fl (lub(1,2))(y) = Tmentre

fl (1)(y) = 1 = fl (2)(y)

ovvero lub(fl (1), fl (2)) # fl (lub(1,2))

General Framework. Tino CortesiTecniche di Analisi di Programmi 2 Framework Nonostante le differenze...

Documents

Transcript of General Framework. Tino CortesiTecniche di Analisi di Programmi 2 Framework Nonostante le differenze...