Definitivna analiza dodele

U teoriji kompilatora, definitivna analiza dodele (engl. Definite assignment analysis) je analiza protoka podataka koju kompilatori koriste da bi garantovano utvrdili da je promenljiva dodeljena pre upotrebe.

Motivacija

Izvor posebno teško detektovanih grešaka u C i C++ programima je nedeterminističko ponašanje programa koje se javlja pri čitanju neinicijalizovanih promenljivih. Ponašanje ovih programa se može razlikovati u različitim okruženjima, u zavisnosti od kompilacije, pa čak i od pokretanja do pokretanja.

Ovaj problem se često rešava na jedan od dva načina. Prvi je da se utvrdi da je na sve lokacije u memoriji pisano pre nego što su čitane. Rajsova teorema pokazuje da se ovaj problem ne može rešiti u opštem slučaju za sve programe, ipak može se načiniti stroga, neprecizna analiza koja odbacuje sve programe koji krše ovaj uslov, a sa njima i neke koji ga poštuju. Definitivna analiza dodele je upravo takva analiza.

Java i C# specifikacije jezika zahtevaju da kompilator javi grešku ukoliko je ovakva analiza prijavi. Kako bi se izbegle nedoumice, ove analize su definisane do pojedinosti. U slučaju Jave ovu analizu su formalizovali Šterk i drugi i ona odbacuje i neke tačne programe zbog čega je ponekad neophodno načiniti izlišne dodele kako bi kompilator prihvatio kod. U C#-u, ovu analizu je formalizovao Fruža i ona je ne samo sigurna već i precizna, odnosno sve promenljive koje su dodeljene u svim mogućim putevima izvršavanja smatraju se definitivno dodeljenim. Programski jezik Cyclone takođe zahteva definitivnu analizu dodele ali samo na pokazivačima, kako bi se olakšalo portovanje C koda. .

Drugi način rešavanja ovog problema je automatska dodela na sve lokacije neke unapred određene vrednosti prilikom definicije promenljive. Ovo može spustiti performanse usled suvišnih dodela, ali moguća je i optimizaciju kompilatora koja uklanja nepotrebne dodele koje su prepisane kasnijim dodelama između kojih nema nikakvog čitanja promenljive. U ovom slučaju svi programi smatraju se korektnim ali kompilator može ostaviti izlišne dodele ukoliko ih analiza kao takve ne prepozna. Primer ovog pristupa je opšta jezička infrastruktura, specifikacija koda za izvršni kod na .NET platformi.

Terminologija

Promenljiva ili lokacija se u datom koraku izvršavanja može nalaziti u jednom od tri stanja:

• Definitivno dodeljena: Promenljiva je sa sigurnošću dodeljena.
• Definitivno nedodeljena: Promenljiva je sa sigurnošću nedodeljena.
• Nepoznata: Može biti i dodeljena i nedodeljena, analiza nije dovoljno precizna da bi odredila.

Analiza

Ovo potpoglavlje je zasnovano na Fružinoj formalizaciji C# definitivnoj analizi dodele unutar jednog metoda koja obezbeđuje dodelu svih lokalnih promenljivih pre čitanja, istovremeno ona vrši i propagaciju konstanti Bulovog tipa. Definišemo pet funkcija.

Ime	Domen	Opis
pre	Sve naredbe i izrazi	Promenljive definitivno dodeljene pre evaluacije datog izraza ili naredbe.
posle	Sve naredbe i izrazi	Promenljive definitivno dodeljene pre evaluacije datog izraza ili naredbe, pod pretpostavkom da se ova izvrši normalno.
varijable	Sve naredbe i izrazi	Sve varijable u opsegu naredbe ili izraza.
tačno	Svi bulovi izrazi	Promenljive definitivno dodeljene posle evaluacije izraza, pod pretpostavkom da se izraz evaluira u true.
netačno	Svi bulovi izrazi	Promenljive definitivno dodeljene posle evaluacije izraza, pod pretpostavkom da se izraz evaluira u false.

Zadajemo jednačine koje definišu vrednosti ovih funkcija nad raznim izrazima i naredbama u zavisnosti od njihovih vrednosti nad njihovim podizrazima. Zanemarimo privremeno naredbe poput goto, break', continue, return i rukovanje izuzecima. Neki primeri ovih jednačina su:

• Svaki izraz ili naredba e koji ne utiče na skup definitivno dodeljenih promenljivih: posle(e) = pre(e)
• Neka je e operacija dodele loc = v. Onda pre(v) = pre(e) i posle(e) = posle(v) ∪ {loc}
• Neka je e izraz true. Onda je tačno(e) = pre(e), i netačno(e) = varijable(e), jer ako je e netačno tada su sve promenljive isprazno dodeljene jer e nikada nije netačno.
• Pošto su argumenti metoda evaluirani s leva na desno, pre(arg_{i + 1}) = posle(arg_{i + 1})
• Neka je s uslovni izraz if (e) s₁ else s₂. Onda pre(e) = pre(s), pre( s₁) = tačno(e), pre(s₂) = netačno(e), and posle(s) = posle(s₁) ∩ posle(s₂).
• Neka je s While petlja while(e) s₁. Onda pre(e) = pre(s), pre(s₁) = tačno(e), i posle(s) = netačno(e).
• I tako dalje.

Pri početku metoda, nijedna od lokalni varijabli nije definitivno dodeljena. Verifikator neprekidno iterira preko apstraktnog sintaksnog drveta i koristi analizu protoka podataka da prebaci podatke u skupove dok se ne dostigne fiksna tačka. Onda verifikator ispita pre skup svakog izraza koji koristi lokalnu varijablu ne bi li se uverio da zadrži tu varijablu.

Algoritam se komplikuje uvođenjem naredbi za upravljanje tokom kontrole poput goto, break, continue, return i hvatanja izuzetaka. Bilo koji izraz koji može biti meta jednog od tih skokova mora izračunati presek svog pre skupa sa skupom definitivno dodeljenih promenljivih na izvoru skoka. Jednom kada je ovo pravilo uvedeno, rezultujući tok podataka može imati višestruke fiksne tačke, kao u ovom C primeru:

 int i = 1;
 L:
 goto L;

Kako se izvršavanje može dospeti do segmenta označenog sa L iz dve lokacije, jednačina toka kontrole zahteva da pre (2) = posle (1) ∩ pre (3). Ali pre (3) = pre (2), tako da pre (2) = pre(1) ∩ pre(2). Za pre (2) tada postoje dve fiksne tačke: {i} i prazan skup. Ipak može se pokazati da usled monotoničkih formi jednačina toka podataka, postoji jedinstvena maksimalna fiksna tačka (fiksna tačka najveće veličine) koja nudi najviše moguće informacija o definitivno dodeljenim promenljivima. Takva maksimalna fiksna tačka može se izračunati standardnim tehnikama, videti Analiza protoka podataka.

Dodatni problem je da određeni skokovi mogu učiniti određene kontrole toka neizvodljivim, na primer u ovom komadu koda promenljiva i je definitivno dodeljena pre upotrebe:

 int i;
 if (j < 0) return; else i = j;
 print(i);

Jednačina toka podataka za if kaže da posle(2) = posle(return) ∩ posle(i = j). Kako bi ovo bilo korektno, definišemo posle(e) = promenljive(e) za sve skokove kontrole toka. Ovo je isprazno tačno u smislu u kome je fale(true) = promenljive(e) tačno, jer nije moguće da kontrola dostigne tačku odmah posle skoka.