Original title: Statická analýza v nástroji Facebook Infer zaměřená na analýzu výkonnosti
Translated title: Static Analysis Using Facebook Infer Focused on Performance Analysis
Authors: Pavela, Ondřej ; Lengál, Ondřej (referee) ; Rogalewicz, Adam (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 se v současnosti dostává do popředí v oblasti technik pro odhalování chyb v moderním software. Nedostatečná škálovatelnost, především v kombinaci se zachováním potřebné přesnosti, je však přetrvávající problém u většiny současných nástrojů pro statickou analýzu, což je činí nepoužitelnými v případě rozsáhlého a často se měnícího kódu. Efektivní statické analyzátory, jako například Coverity nebo Code Sonar, jsou navíc často proprietární a není tedy možné je jednoduše rozšířit nebo srovnávat jejich výsledky. Oproti tomu Facebook Infer nabízí open source rámec s důrazem na kompoziční, inkrementální, a v důsledku i škálovatelnou inter-procedurální statickou analýzu. Tato práce představuje Looper --- nový analyzátor zaměřující se na analýzu výkonnosti, přesněji na analýzu mezí, rozšiřující rámec nástroje Facebook Infer. Implementace našeho analyzátoru je založena na existujícím nástroji Loopus, který se zaměřuje na přesnou analýzu mezí. Výsledný prototyp jsme otestovali na dvou různých testovacích sadách a povzbudivé výsledky srovnali s existujícím analyzátorem Cost, který je vyvíjen Infer týmem. Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, reasonably precise static analysis tools still often struggle to scale well on large and quickly changing codebases. Efficient static analysers, such as Coverity or Code Sonar, are usually proprietary and difficult to openly evaluate or extend. On the contrary, Facebook Infer offers an open source static analysis framework with the emphasis on compositional, incremental and consequently highly scalable inter-procedural analysis. This thesis presents Looper --- a new performance oriented resource bounds analyser which extends the capabilities of Facebook Infer. We have based our implementation on an existing resource bounds analyser Loopus and evaluated it on two different test suites, showing encouraging results in comparison with the existing Cost analyser developed by the Infer team.
Keywords: abstract interpretation; amortized complexity; Loopus; OCaml; performance analysis; resource bounds analysis; static analysis; abstraktní interpretace; amortizovaná složitost; analýza mezí; Loopus; OCaml; statická analýza; výkonnostní 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/180232

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


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