Detail práce
Statická analýza v nástroji Facebook Infer zaměřená na detekci uváznutí
Statická analýza dnes patrí medzi najpopulárnejšie metódy na odhaľovanie chýb v modernom softvéri, no častým problémom dostatočne presných statických analyzátorov je ich škálovateľnosť. Mnohé efektívne analyzátory (napr.:Coverity, KlockWork, atď.) sú navyše proprietárne, čím sa ich ďalšia rozšíriteľnosť a použitie stávajú obťažnými. Pokrok v tejto oblasti prináša Facebook Infer, ktorý ponúka open-source framework na tvorbu kompozičných a inkrementálnych statických analýz. V tejto práci predstavujeme vlastný Low-Level Deadlock Detector (L2D2), ktorý rozširuje funkcionalitu Inferu. Náš algoritmus spĺňa princípy kompozičnej analýzy, založenej na kontextovo nezávislom výpočte súhrnu pre každú funkciu, čo má za následok jeho vysokú škálovateľnosť. Algoritmus sme implementovali a overili na sade príkladov z Debian GNU/Linux, ktorá pozostávala z 11.4 MLOC. Aj keď náš prístup nie je ani presný ani úplný, ukazuje sa ako efektívny. Okrem toho, že dokázal odhaliť všetky známe uviaznutia, hlásil falošné pozitíva v menej ako 4% z testovaných programov.
statická analýza, abstraktná interpretácia, Facebook Infer, detekcia uviaznutia, Infer.AI framework, L2D2
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm "A".
- Jak složité by bylo přidat podporu zámků dle normy C11?
- V současné době nástroj hledá potenciální deadloky bez ohledu na to, jestli jednotlivé funkce mohou být opravdu spuštěny paralelně. Bylo by možné váš nástroj rozšířit o možnost analýzy, které funkce jsou opravdu spuštěny paralelně?
Grézl František, Ing., Ph.D. (UPGM FIT VUT), člen
Honzík Jan M., prof. Ing., CSc. (UIFS FIT VUT), člen
Kořenek Jan, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT), člen
@bachelorsthesis{FITBT21920,
author = "Vladim\'{i}r Marcin",
type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
title = "Statick\'{a} anal\'{y}za v n\'{a}stroji Facebook Infer zam\v{e}\v{r}en\'{a} na detekci uv\'{a}znut\'{i}",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2019,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/21920/"
}