Határozott feladat-elemzés - Definite assignment analysis

A számítástechnika , határozott megbízás elemzés egy adat-flow elemzés által használt fordítóprogramok a konzervatív biztosítása érdekében, hogy a változó vagy hely mindig rendelt használat előtt.

Motiváció

A C és C ++ programokban a különösen nehezen diagnosztizálható hibák forrása a nemdeterminisztikus viselkedés, amely az inicializálatlan változók beolvasásával jár ; ez a viselkedés platformonként, felépítésenként és futás közben is változhat.

Két általános módszer létezik a probléma megoldására. Az egyik annak biztosítása, hogy minden hely megírásra kerüljön, mielőtt elolvasnák. Rice tétele megállapítja, hogy ez a probléma általában nem oldható meg minden program esetében; Lehetséges azonban konzervatív (pontatlan) elemzést készíteni, amely csak azokat a programokat fogadja el, amelyek kielégítik ezt a korlátozást, miközben elutasítanak néhány helyes programot, és a határozott hozzárendelési elemzés ilyen elemzés. A Java és a C # programozási nyelv specifikációi megkövetelik, hogy az elemző fordítási idő hibát jelentsen, ha az elemzés sikertelen. Mindkét nyelv megköveteli az elemzés egy meghatározott formáját, amelyet aprólékos részletességgel kell megfogalmazni. A Java-ban ezt az elemzést Stärk és munkatársai formalizálták, és néhány helyes programot elutasítottak, és azokat meg kell változtatni, hogy explicit felesleges hozzárendeléseket vezessenek be. A C #-ban ezt az elemzést Fruja formalizálta, és pontos, ugyanakkor megbízható is abban az értelemben, hogy az összes vezérlőáramlási útvonal mentén kiosztott minden változót határozottan megjelöltnek kell tekinteni. A ciklon nyelvhez a programokat is megköveteli egy meghatározott hozzárendelési elemzés átadása, de csak a mutatótípusú változókon, a C programok átvitele megkönnyítése érdekében.

A probléma megoldásának második módja az, hogy az összes helyet automatikusan inicializálja valamilyen rögzített, kiszámítható értékre azon a ponton, ahol meghatározzák őket, de ez új feladatokat vezet be, amelyek akadályozhatják a teljesítményt. Ebben az esetben a határozott hozzárendelési elemzés lehetővé teszi a fordító optimalizálását, ahol kiküszöbölhetők a redundáns feladatok - az olyan feladatok, amelyeket csak más feladatok követnek, lehetséges beavatkozás nélkül. Ebben az esetben egyetlen programot sem utasítanak el, de azok a programok, amelyekhez az elemzés nem ismeri fel a konkrét hozzárendelést, redundáns inicializálást tartalmazhatnak. A közös nyelvi infrastruktúra erre a megközelítésre támaszkodik.

Terminológia

Azt mondhatjuk, hogy egy változó vagy a helyzet a program bármely pontján a három állapot egyikében található:

• Határozottan hozzárendelve : A változót biztosan meg kell határozni a hozzárendelésről.
• Határozottan nem hozzárendelt : A változó biztosan ismert, hogy kiosztott.
• Ismeretlen : A változó hozzárendelhető vagy kioszthatatlan; az elemzés nem elég pontos ahhoz, hogy meghatározzuk melyiket.

Az elemzés

Az alábbiak alapulnak Fruja által a C # intraprocedural (egy módszer) határozott hozzárendelési elemzés formalizálásán, amelynek feladata annak biztosítása, hogy minden helyi változót hozzárendeljenek felhasználásuk előtt. Egyidejűleg végzi el a hozzárendelés elemzését és a logikai értékek állandó terjedését . Öt statikus függvényt definiálunk:

Olyan adatáramlási egyenleteket szolgáltatunk, amelyek ezen függvények értékeit különféle kifejezésekben és utasításokban határozzák meg, a függvények értékeinek szintaktikai feliratai alapján. Tegyük fel, hogy ebben a pillanatban, hogy nincsenek goto , törés , továbbra is , visszatérő , vagy kivételkezeléssel nyilatkozatokat. Az alábbiakban bemutatunk néhány példát ezekre az egyenletekre:

• Bármilyen kifejezés vagy kijelentés e , amely nem érinti a beállított változók egyértelműen hozzárendelt: miután ( e ) = előtt ( e )
• Legyen e a loc = v hozzárendelési kifejezés . Ezután előtt ( V ) = előtt ( e ), és után ( e ) = után ( V ) U {loc}.
• Legyen e a kifejezés igaz . Akkor igaz ( e ) = előtte ( e ) és hamis ( e ) = vars ( e ). Más szóval, ha e értékelődik hamis , az összes változó ( üresen, ) biztosan rendelt, mert e nem értékeli, hogy hamis.
• Mivel a módszer érveit balról jobbra értékelik, előtte ( arg _{i  + 1} ) = után ( arg _i ). Miután egy módszer befejeződött, a paramétereket határozottan hozzá kell rendelni.
• Legyen s feltételes állítás, ha ( e ) s ₁ másik s ₂ . Aztán , mielőtt ( e ) = előtt ( s ), mielőtt (s ₁ ) = true ( e ), mielőtt ( s ₂ ) = false ( e ) és után ( s ) = után ( s ₁ ) metszik után ( s ₂ ) .
• Legyen s míg a ciklus utasítás, míg ( e ) s ₁ . Aztán ( e ) = előtt ( s ), előtt ( s ₁ ) = true ( e ), és után ( s ) = false ( e ).
• Stb.

A módszer elején semmilyen helyi változót nem rendelnek hozzá. A hitelesítő többször ismétli az absztrakt szintaxisfát, és az adatáram egyenleteket használja az információk migrálására a halmazok között, amíg egy rögzített pont elérhető. Ezután a hitelesítő megvizsgálja minden kifejezés előző halmazát, amely helyi változót használ annak biztosítására, hogy tartalmazza-e ezt a változót.

Az algoritmust bonyolítja az olyan vezérlőáramlás-ugrások bevezetése, mint a goto , break , folytatás , visszatérés és kivételkezelés. Bármely kijelentésnek, amely ezen ugrások egyikének célpontja lehet, kereszteznie kell azt, mielőtt beállítja a feltétlenül hozzárendelt változók halmazával az ugrás forrásán. Amikor ezeket bevezetik, a kapott adatáramlás több rögzített ponttal is rendelkezhet, mint az ebben a példában:

1  int i = 1;
2  L:
3  goto L;

Mivel a címke L érhető el két helyről, a kontroll-áramlási egyenleten Goto diktálja, hogy mielőtt (2) = után (1) metszik előtt (3). De előtte (3) = előtt (2), tehát előtt (2) = után (1) keresztezik előtt (2). Ennek két rögzített pontja van az előző (2), {i} és az üres halmaz számára. Megmutatható azonban, hogy az adatáramlási egyenletek monoton formája miatt van egy egyedi maximális rögzített pont (a legnagyobb méretű rögzített pont), amely a lehető legtöbb információt nyújtja a határozottan kiosztott változókról. Egy ilyen maximális (vagy maximális) rögzített pont standard technikákkal kiszámítható; lásd az adatáramlás elemzését .

További probléma az, hogy a vezérlőáramlás-ugrás bizonyos vezérlőáramlásokat lehetetlenné teheti; Például ebben a kódrészletben az i változó használata előtt mindenképpen hozzá van rendelve:

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

Az adatok-áramlási egyenleten , ha azt mondja, hogy után (2) = után ( hozam ) metszik után ( i = j ). Annak érdekében, hogy ez helyesen működjön, az ( e ) = vars ( e ) után definiáljuk az összes vezérlőáramlás-ugrást; ez nyilvánvalóan érvényes abban az értelemben, hogy a false ( true ) = vars ( e ) egyenlet érvényes, mivel a vezérlés nem tudja közvetlenül elérni egy pontot a kontroll-flow folytatás után.

Irodalom