Abstraktní interpretace - Abstract interpretation

Ve vědě o počítačích , abstraktní interpretace je teorie zvukové sbližování ze sémantiky počítačových programů , založené na monotónní funkce přes uspořádaných množin , zejména mříže . To lze považovat za částečné provedení části počítačového programu , který získává informace o jeho sémantiky (například kontrola-flow , datový tok ) bez provádění všech výpočtů .

Jeho hlavní konkrétní aplikací je formální statická analýza , automatická extrakce informací o možných provedeních počítačových programů; takové analýzy mají dvě hlavní použití:

Abstraktní interpretaci formalizoval francouzský počítačový vědecký pracovní pár Patrick Cousot a Radhia Cousot na konci 70. let minulého století.

Intuice

Tato část ilustruje abstraktní interpretaci pomocí reálných, nepočítajících příkladů.

Zvažte lidi v konferenční místnosti. Předpokládejte jedinečný identifikátor pro každou osobu v místnosti, jako je číslo sociálního zabezpečení ve Spojených státech. Abyste dokázali, že někdo není přítomen, stačí, když zjistíte, zda jeho číslo sociálního pojištění není na seznamu. Protože dva různí lidé nemohou mít stejné číslo, je možné přítomnost účastníka prokázat nebo vyvrátit pouhým vyhledáním jeho čísla.

Je však možné, že byla zaregistrována pouze jména účastníků. Pokud jméno osoby v seznamu není, můžeme bezpečně usoudit, že tato osoba nebyla přítomna; ale pokud ano, nemůžeme s konečnou platností uzavřít bez dalších šetření, kvůli možnosti homonym (například dva lidé jménem John Smith). Všimněte si, že tyto nepřesné informace budou pro většinu účelů stále dostačující, protože homonyma jsou v praxi vzácná. Se vší přísností však nemůžeme s jistotou říci, že v místnosti někdo byl; můžeme jen říci, že on nebo ona tu možná byla . Pokud je osoba, ke které vzhlížíme, zločinec, vydáme poplach ; ale samozřejmě existuje možnost vydat falešný poplach . Podobné jevy nastanou při analýze programů.

Pokud nás zajímají jen některé konkrétní informace, řekněme „byla v místnosti osoba ve věku n ?“, Není nutné vést seznam všech jmen a dat narození. Můžeme se bezpečně a beze ztráty přesnosti omezit na vedení seznamu věků účastníků. Pokud je to už příliš manipulovat, můžeme udržet jen věk nejmladší, m a nejstarší osobou, M . Pokud se otázka týká věku přísně nižšího než m nebo přísně vyššího než M , pak můžeme bezpečně odpovědět, že žádný takový účastník nebyl přítomen. V opačném případě můžeme být schopni pouze říci, že nevíme.

V případě výpočetní techniky konkrétní přesné informace obecně nelze spočítat v konečném čase a paměti (viz Riceova věta a problém se zastavením ). Abstrakce se používá k umožnění generalizovaných odpovědí na otázky (například odpověď „možná“ na otázku ano/ne, což znamená „ano nebo ne“, když my (algoritmus abstraktní interpretace) nedokážeme přesně vypočítat přesnou odpověď); to problémy zjednodušuje a umožňuje jejich automatická řešení. Jedním z klíčových požadavků je přidat dostatek neurčitosti, aby byly problémy zvládnutelné a přitom si zachovat dostatečnou přesnost pro zodpovězení důležitých otázek (například „mohl by program spadnout?“).

Abstraktní interpretace počítačových programů

Vzhledem k programovacímu nebo specifikačnímu jazyku abstraktní interpretace spočívá v poskytnutí několika sémantik propojených vztahy abstrakce. Sémantika je matematická charakteristika možného chování programu. Nejpřesnější sémantika, která velmi přesně popisuje skutečné provedení programu, se nazývá konkrétní sémantika . Například konkrétní sémantika imperativního programovacího jazyka může ke každému programu přidružit sadu stop provádění, které může vytvářet - stopa provádění je posloupnost možných po sobě jdoucích stavů provádění programu; stav se obvykle skládá z hodnoty čítače programu a umístění paměti (globály, zásobník a halda). Poté se odvozuje abstraktnější sémantika; například lze při provádění brát v úvahu pouze množinu dosažitelných stavů (což znamená zvažovat poslední stavy v konečných stopách).

Cílem statické analýzy je v určitém okamžiku odvodit vypočítatelnou sémantickou interpretaci. Například se můžeme rozhodnout reprezentovat stav programu manipulujícího s celočíselnými proměnnými zapomenutím skutečných hodnot proměnných a ponecháním pouze jejich znaků (+, - nebo 0). U některých elementárních operací, jako je násobení , neztrácí taková abstrakce žádnou přesnost: k získání znaku produktu stačí znát znak operandů. U některých jiných operací může abstrakce ztratit přesnost: například není možné znát znaménko součtu, jehož operandy jsou kladné a záporné.

Někdy je nutná ztráta přesnosti, aby byla sémantika rozhodnutelná (viz Riceova věta a problém zastavení ). Obecně existuje kompromis mezi přesností analýzy a její rozhodnutelností ( vyčíslitelností ) nebo sledovatelností ( výpočetní náklady ).

V praxi jsou definované abstrakce přizpůsobeny jak vlastnostem programu, které si přeje analyzovat, tak sadě cílových programů. První rozsáhlá automatizovaná analýza počítačových programů s abstraktní interpretací byla motivována nehodou, která vedla ke zničení prvního letu rakety Ariane 5 v roce 1996.

Formalizace

Příklad: abstrakce celočíselných množin (červená) k znakovým sadám (zelená)

Nechť L je uspořádaná množina, nazývaná konkrétní množina, a L 'je další uspořádaná množina, nazývaná abstraktní množina . Tyto dvě sady spolu souvisí definováním celkových funkcí, které mapují prvky z jedné na druhou.

Funkce α se nazývá abstrakční funkcí, pokud mapuje prvek x v konkrétní sadě L na prvek α ( x ) v abstraktní sadě L ′. To znamená, že prvek α ( x ), v L 'je abstrakce o x v L .

Funkce γ se nazývá funkce konkretizace pokud mapuje prvek x "v abstraktním nastavené L 'na prvek y ( x '), v sadě betonu L . To znamená, že prvek γ ( x '), v L je konkretizace o x ' v L ".

Nechte L 1 , L 2 , L ' 1 a L ' 2 uspořádané sady. Sémantika betonu f je monotónní funkcí od L 1 do L 2 . Funkce f "od L ' 1 k L ' 2, se říká, že je platný abstrakce z f -li pro všechny x " v L ' 1 , ( f ∘ γ) ( x ") ≤ (γ ∘ f ') ( X " ).

Sémantika programu je obecně popsána pomocí pevných bodů za přítomnosti smyček nebo rekurzivních procedur. Dejme tomu, že L je úplný svaz a nechť f být monotónní funkcí z L do L . Potom jakékoli x ′ takové, že f ( x ′) ≤ x ′ je abstrakcí nejméně pevného bodu f , který existuje, podle Knasterovy-Tarskiho věty .

Nyní je obtížné získat takové x '. Pokud má L 'konečnou výšku nebo alespoň ověřuje vzestupnou řetězovou podmínku (všechny vzestupné sekvence jsou nakonec nehybné), pak takové x ' lze získat jako stacionární limit vzestupné sekvence x ′ n definovanou indukcí takto: x ′ 0 = ⊥ (nejmenší prvek L ′) a x ′ n +1 = f ′ ( x ′ n ).

V jiných případech, že je stále možné získat takový x "přes rozšiřující se operátor ∇: pro všechny x a y , x ∇ y by měl být větší nebo rovna než oba x a y , a pro každý sekvenční y ' n , sekvenci definováno x ′ 0 = ⊥ a x ′ n +1 = x ′ n ∇ y ′ n je nakonec nehybné. Potom můžeme vzít y ' n = f ' ( x ' n ).

V některých případech je možné definovat pomocí abstrakce Galois spojení (a, y), kde α je z L na L 'a γ je z L ' a L . To předpokládá existenci nejlepších abstrakcí, což nemusí nutně platit. Pokud například abstrahujeme množiny párů ( x , y ) reálných čísel uzavřením konvexní mnohostěny , neexistuje optimální abstrakce na disk definovaný x 2 + y 2 ≤ 1.

Příklady abstraktních domén

Ke každé proměnné x dostupné v daném bodě programu lze přiřadit interval [ L x , H x ]. Stav přiřazující hodnotu v ( x ) proměnné x bude konkretizací těchto intervalů, pokud pro všechna x je v ( x ) v [ L x , H x ]. Z intervalů [ L x , H x ] a [ L y , H y ] pro proměnné x a y lze snadno získat intervaly pro x + y ([ L x + L y , H x + H y ]) a pro x - y ([ L x - H y , H x - L y ]); všimněte si, že se jedná o přesné abstrakce, protože množina možných výsledků, řekněme, x + y , je přesně interval ([ L x + L y , H x + H y ]). Složitější vzorce lze odvodit pro násobení, dělení atd., Čímž se získá takzvaná intervalová aritmetika .

Podívejme se nyní na následující velmi jednoduchý program: 

y = x;
z = x - y;
Kombinace intervalové aritmetiky ( zelená ) a kongruence mod 2 na celých číslech ( azurová ) jako abstraktní domény k analýze jednoduchého kusu kódu C ( červená : konkrétní sady možných hodnot za běhu). Pomocí informací o shodě ( 0 = sudý, 1 = lichý) lze vyloučit nulové dělení . (Jelikož se jedná pouze o jednu proměnnou, není zde relační vs. nerelační doména problém.)
Trojrozměrný konvexní příklad mnohostěnu popisující možné hodnoty 3 proměnných v určitém programovém bodě. Každá z proměnných může být nula, ale všechny tři nemohou být nulové současně. Poslední vlastnost nelze popsat v doméně intervalové aritmetiky.

Při rozumných aritmetických typech výsledek pro zby měla být nula. Ale pokud uděláme intervalovou aritmetiku odX v [0, 1], jeden dostane zv [−1, +1]. Zatímco každá z operací jednotlivě byla přesně abstrakta, jejich složení není.

Problém je evidentní: nesledovali jsme vztah rovnosti mezi X a y; ve skutečnosti tato doména intervalů nebere v úvahu žádné vztahy mezi proměnnými, a je tedy nerelační doménou . Non-relační domény mají tendenci být rychle a snadno implementovatelné, ale nepřesné.

Některé příklady relačních numerických abstraktních domén jsou:

  • kongruenční vztahy na celých číslech
  • konvexní mnohostěn (viz obrázek vlevo) - s vysokými výpočetními náklady
  • rozdílově vázané matice
  • "osmiúhelníky"
  • lineární rovnosti

a jejich kombinace (jako je redukovaný produkt, viz pravý obrázek).

Když si člověk vybere abstraktní doménu, musí obvykle dosáhnout rovnováhy mezi udržováním jemnozrnných vztahů a vysokými výpočetními náklady.

Viz také

Reference

externí odkazy

Poznámky k výuce