Original title: Statická analýza v nástroji Facebook Infer zaměřená na detekci uváznutí
Translated title: Static Analysis Using Facebook Infer Focused on Deadlock Detection
Authors: Marcin, Vladimír ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Document type: Bachelor's theses
Year: 2019
Language: cze
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [cze] [eng]
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. Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, a frequent problem of static analysers, which are reasonably precise, is their scalability. Moreover, these which are efficient and scale (e.g.: Coverity, KlockWork, etc.) are often proprietary and difficult to openly evaluate or extend. An improvement to this state of practice is brought Facebook Infer, which offers an open-source framework for compositional and incremental static analysis. In this thesis, we present our Low-Level Deadlock Detector (L2D2) extending the capabilities of Infer. Our algorithm fits the compositional analysis, based on a context independent computation of a summary for each function, which results in its high scalability. We have implemented the algorithm and evaluated it on a benchmark consisting of real-life programs derived from the Debian GNU/Linux with in total 11.4 MLOC. While neither sound nor complete, our approach is effective in practice, finding all known deadlocks and giving false alarms in less than 4% of the considered programs only.
Keywords: abstract interpretation; deadlock detection; Facebook Infer; Infer.AI framework; L2D2; static analysis; abstraktná interpretácia; detekcia uviaznutia; Facebook Infer; Infer.AI framework; L2D2; statická analýza

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/180233

Permalink: http://www.nusl.cz/ntk/nusl-592000


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses