|
|
Static Analysis Using Facebook Infer to Find Atomicity Violations
Harmim, Dominik ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The goal of this thesis is to propose a static analyser that detects atomicity violations. The proposed analyser Atomer is implemented as a module of Facebook Infer, which is an open-source and extendable static analysis framework that promotes efficient modular and incremental analysis. The analyser works on the level of sequences of function calls. The proposed solution is based on the assumption that sequences executed atomically once should probably be executed always atomically. The implemented analyser has been successfully verified and evaluated on both smaller programs created for testing purposes as well as publicly available benchmarks derived from real-life low-level programs.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje.
|
|
|
Practical Application of Facebook Infer on Systems Code
Beránek, Tomáš ; Malík, Viktor (referee) ; Vojnar, Tomáš (advisor)
Statická analýza je dnes často využívána ve vývojovém procesu pro hledání defektů v produkovaném softwaru. I když nástroje na statickou analýzu dokáží hledat defekty v softwarech o miliónech řádků kódu, mají také řadu nevýhod. Hlavními nevýhodami jsou náročnost nasazení nástroj na vyvíjený projekt, vysoký počet falešných hlášení a časové i paměťové požadavky. Tato práce se zaměřuje na zmírnění těchto negativních vlastností u nástroje Facebook Infer, zejména pro analýzu Linuxových nástrojů v podobě SRPM balíčků. Pro zjednodušení nasazení byl vytvořen modul pro nástroj csmock, který umožňuje automaticky spouštět statické analyzátory nad balíčky pro CentOS a Fedoru. Pro snížení počtu falešných hlášení byl vytvořen filtr, který filtruje výstup Inferu podle heuristik, které byly navrženy na základě zkušeností získaných kontrolou hlášení z Inferu. Filtr byl také zapojen do modulu pro csmock a otestován na řadě balíčků. Na analyzovaných balíčcích filtr dokázal odstranit 60 % falešných hlášení se ztrátou 2.5 % skutečných defektů. Doba potřebná pro běh analýzy může být zkrácena použitím inkrementální analýzy. U inkrementální analýzy Inferu byly experimentálně zjištěny nedostatky, proto se tato práce věnuje také vytvoření nástavby nad Inferem, která nahrazuje inkrementální analýzu v Inferu.
|
|
|
Statická analýza v nástroji Meta Infer zaměřená na detekci souběhu nad daty
Svobodová, Lucie ; Fiedor, Jan (referee) ; Vojnar, Tomáš (advisor)
Vícevláknové programy jsou v moderních softwarových systémech využívány ke zlepšení výkonu a zvýšení efektivity. Zajištění spolehlivosti a bezpečnosti takových programů však může být náročné kvůli zvýšenému množství chyb, které se v nich vyskytují, včetně souběhu nad daty. V této práci představujeme nový statický detektor souběhu nad daty, DarC, navržený k analýze programů napsaných v jazyce C využívajících knihovnu Pthreads. Navrhovaný nástroj byl implementován jako zásuvný modul prostředí Meta Infer, což je nástroj pro statickou analýzu programů, který klade důraz na kompoziční, inkrementální a díky tomu i vysoce škálující analýzu programů. Nový analyzátor zaznamenává množinu přístupů ke sdíleným proměnným, ke kterým v analyzovaném programu došlo, spolu s informací o množině zámků uzamknutých při jednotlivých přístupech. Množina přístupů je dále použita k identifikaci dvojic přístupů, mezi nimiž by k souběhu nad daty mohlo dojít. Nástroj byl úspěšně ověřen na sadě testovacích vícevláknových programů, stejně tak jako na několika programech běžně využívaných v praxi, čímž byl ukázán jeho potenciál pro efektivní detekci souběhu nad daty v programech napsaných v programovacím jazyce C.
|
|
|
Pokročilá statická analýza výkonnosti v nástroji Meta Infer
Pavela, Ondřej ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Statický analyzátor složitosti Looper slouží pro odvozování přesných horních mezí ceny vykonání programů. Jako teoretický základ byl využit dříve existující nástroj Loopus a jeho abstraktní programový model využívající tzv. difference constraints (nerovnosti typu + ), které umožňují přirozeným způsobem modelovat typické modifikace počítadel cyklů = + + a = + 0. Looper byl původně navržen a implementován v rámci autorovy bakalářské práce jako zásuvný modul aplikačního rámce Meta Infer. Výsledný nástroj nicméně nenaplnil očekávání při pokusech o jeho nasazení na reálné programy. Tato diplomová práce představuje návrh nové verze, která si dává za cíl odstranit hlavní limitace původního nástroje Looper, zejména díky nově podporované in- terprocedurální analýze. Dále byla implementována řada rozšíření, které cílily na zvýšení přesnosti intraprocedurální analýzy, jako např. nový abstrakční algoritmus, podpora pro složené podmínky v hlavičkách smyček a další. Kromě toho bylo také výrazně vylepšeno logování, hlášení chyb a sběr výsledků analýzy. Na závěr byla skrze skrze rozsáhlé exper- imenty demonstrována schopnost nové verze nástroje Looper analyzovat reálný kód obec- nějším, škálovatelnějším a přesnějším způsobem.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje.
|
|
|
Practical Application of Facebook Infer on Systems Code
Beránek, Tomáš ; Malík, Viktor (referee) ; Vojnar, Tomáš (advisor)
Statická analýza je dnes často využívána ve vývojovém procesu pro hledání defektů v produkovaném softwaru. I když nástroje na statickou analýzu dokáží hledat defekty v softwarech o miliónech řádků kódu, mají také řadu nevýhod. Hlavními nevýhodami jsou náročnost nasazení nástroj na vyvíjený projekt, vysoký počet falešných hlášení a časové i paměťové požadavky. Tato práce se zaměřuje na zmírnění těchto negativních vlastností u nástroje Facebook Infer, zejména pro analýzu Linuxových nástrojů v podobě SRPM balíčků. Pro zjednodušení nasazení byl vytvořen modul pro nástroj csmock, který umožňuje automaticky spouštět statické analyzátory nad balíčky pro CentOS a Fedoru. Pro snížení počtu falešných hlášení byl vytvořen filtr, který filtruje výstup Inferu podle heuristik, které byly navrženy na základě zkušeností získaných kontrolou hlášení z Inferu. Filtr byl také zapojen do modulu pro csmock a otestován na řadě balíčků. Na analyzovaných balíčcích filtr dokázal odstranit 60 % falešných hlášení se ztrátou 2.5 % skutečných defektů. Doba potřebná pro běh analýzy může být zkrácena použitím inkrementální analýzy. U inkrementální analýzy Inferu byly experimentálně zjištěny nedostatky, proto se tato práce věnuje také vytvoření nástavby nad Inferem, která nahrazuje inkrementální analýzu v Inferu.
|
|
|
Static Analysis Using Facebook Infer to Find Atomicity Violations
Harmim, Dominik ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The goal of this thesis is to propose a static analyser that detects atomicity violations. The proposed analyser Atomer is implemented as a module of Facebook Infer, which is an open-source and extendable static analysis framework that promotes efficient modular and incremental analysis. The analyser works on the level of sequences of function calls. The proposed solution is based on the assumption that sequences executed atomically once should probably be executed always atomically. The implemented analyser has been successfully verified and evaluated on both smaller programs created for testing purposes as well as publicly available benchmarks derived from real-life low-level programs.
|
guest ::
