Abstraktne interpretatsioon

Allikas: Vikipeedia
Jump to navigation Jump to search

Abstraktne interpretatsioon (inglise keeles abstract interpretation) on informaatika teooria arvutiprogrammide semantika korrektseks lähendamiseks, põhinedes monotoonsetel funktsioonidel üle osaliselt järjestatud hulkade, eelkõige võrede. Seda võib vaadelda kui arvutiprogrammi osalist täitmist, millega kogutakse informatsiooni selle semantika (nt juhtimisvoo, andmevoo) kohta, tegemata kõiki arvutusi.

Selle teooria põhiline rakendus on formaalne staatiline analüüs, mis hangib informatsiooni programmide võimalike täitmiste kohta. Sellistel analüüsidel on kaks põhilist kasutusvaldkonda:

Abstraktse interpretatsiooni teooria formaliseerisid prantsuse informaatikud Patrick Cousot ja Radhia Cousot 1970. aastate lõpus.[2][3] Esimene suuremahuline automaatne programmianalüüs abstraktse interpretatsiooni abil teostati Ariane 5 raketi koodil pärast selle esmalennu ebaõnnestumist 1996. aastal.[4]

Abstraktsed domeenid[muuda | muuda lähteteksti]

Abstraktseks interpretatsiooniks kasutatavaid võresid nimetatakse abstraktseteks domeenideks (inglise keeles abstract domain). Domeeni elemendid on programmi konkreetsete seisundite lähendused, millel sooritatakse konkreetsetele operatsioonidele vastavaid abstraktseid operatsioone. Lähendamine ja sellega kaasnev täpsuse kaotus võib olla vajalik, et semantika oleks lahenduv (vt Rice'i teoreem, peatumisprobleem).[5]

Domeeni valik sõltub sellest, milliste programmi omaduste kohta informatsiooni otsitakse. Lisaks tuleb teha kompromiss selle täpsuse ja keerukuse vahel.

Täisarvude domeenid[muuda | muuda lähteteksti]

Täisarvuliste muutujate ja nende tehete lähendamiseks on abstraktsel interpreteerimisel mitmeid võimalusi.

Kombinatsioon intervallaritmeetikast (roheline) ja kongurentsist mod 2 (sinine) abstraktsete domeenidena, et analüüsida C programmi (punane: konkreetsed võimalike väärtuste hulgad täitmisel). Kasutades jääke (0=paaris, 1=paaritu), saab nulliga jagamise välistada

Märkide domeen[muuda | muuda lähteteksti]

Selliste muutujate puhul võib unustada täpsed väärtused, jättes alles ainult nende väärtuste märgid (+, - või 0). Mõningate aritmeetiliste tehete, näiteks korrutamise puhul selline lähendus täpsust ei kaota: kahe täisarvu korrutise märk on üheselt määratud korrutatud arvude märkidega. Teiste tehete, näiteks liitmise puhul lähendus võib kaotada täpsust: positiivse ja negatiivse arvu summa märki pole võimalik ainult liidetavate märke teades määrata.[5]

Intervallide domeen[muuda | muuda lähteteksti]

Täpsemaks analüüsiks võib kasutada näiteks arvtelje lõike, kirjeldades iga muutuja võimalikke väärtusi täisarvude intervalliga . Sellistel lähendustel on võimalik defineerida aritmeetilised tehted, moodustades intervallaritmeetika.[6] Näiteks muutujate ja , mille intervallid on vastavalt ja , korral on

  • summa intervall ,
  • vahe intervall .

Relatsionaalsed domeenid[muuda | muuda lähteteksti]

Kolmemõõtmeline kumer hulktahukas kirjeldamaks kolme muutuja võimalike väärtusi. Iga muutuja võib olla null, kuid kõik kolm ei saa korraga olla nullid. Seda omadust ei saa intervallide domeenis kirjeldada

Järgnevas programmis on muutuja z väärtus alati null:

y = x;
z = x - y;

Kasutades intervallide domeeni ja eeldades, et muutuja x väärtus on algul lõigus , leitakse, et muutuja z väärtus on lõigus . Tulemus pole vale, kuid mitte nii täpne, kui võiks tahta, sest see domeen ei arvesta lahutamisel muutujate omavahelist seost, mistõttu nimetatakse domeeni mitterelatsionaalseks.

Relatsionaalsed domeenid, mis muutujatevahelisi seoseid arvestavad, on näiteks:

Muud domeenid[muuda | muuda lähteteksti]

Lisaks täisarvuliste väärtustele võib analüüsida ka muud tüüpi andmeid ja muid programmi omadusi, näiteks:

Viited[muuda | muuda lähteteksti]

  1. 1,0 1,1 Helmut Seidl, Reinhard Wilhelm, Sebastian Hack Foundations and Intraprocedural Optimization. (2012). Compiler Design: Analysis and Transformation. Berlin, Heidelberg: Springer Berlin Heidelberg. Lk 1-114. ISBN 978-3-642-17548-0. Kasutatud 06.04.2018.
  2. Patrick Cousot, Radhia Cousot Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. (1977). Conference Record of the Fourth ACM Symposium on Principles of Programming Languages. Los Angeles, California, USA: ACM. Lk 238-252. Kasutatud 06.04.2018.
  3. Patrick Cousot, Radhia Cousot Systematic Design of Program Analysis Frameworks. (1979). Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages. San Antonio, Texas, USA: ACM. Lk 269-282. Kasutatud 06.04.2018.
  4. Christèle Faure. "PolySpace Technologies History". Vaadatud 17.03.2018.
  5. 5,0 5,1 Matt Might. "What is static program analysis?". Vaadatud 06.04.2018. Inglise.
  6. Patrick Cousot, Radhia Cousot Static determination of dynamic properties of programs. (1976). Proceedings of the Second International Symposium on Programming. Dunod, Paris, France. Lk 106-130. Kasutatud 06.04.2018.
  7. Philippe Granger Static Analysis of Arithmetical Congruences. (1989). International Journal of Computer Mathematics. Kd. 30. Lk 165-190. 
  8. Philippe Granger Static Analysis of Linear Congruence Equalities Among Variables of a Program. S. Abramsky, T.S.E. Maibaum (Toim). (1991). Proc. Int. J. Conf. on Theory and Practice of Software Development (TAPSOFT). Kd. 493. Springer. Lk 169-192. 
  9. Patrick Cousot, Nicolas Halbwachs Automatic Discovery of Linear Restraints Among Variables of a Program. (1978). Conf. Rec. 5th ACM Symp. on Principles of Programming Languages (POPL). ACM. Lk 84-97. Kasutatud 06.04.2018.
  10. Antoine Miné The Octagon Abstract Domain. (2006). Higher Order Symbol. Comput. Kd. 19 (1). Lk 31-100. Kasutatud 06.04.2018.
  11. Vesal Vojdani et al Static race detection for device drivers: the Goblint approach. (2016). Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016. ACM. Lk 391-402. Kasutatud 06.04.2018.

Välislingid[muuda | muuda lähteteksti]