Original title: Advanced Static Performance Analysis Using Meta Infer
Translated title: Pokročilá statická analýza výkonnosti v nástroji Meta Infer
Authors: Pavela, Ondřej ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Document type: Master’s theses
Year: 2023
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
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. Looper is a static complexity analysis tool for inference of tight upper bounds on the exe- cution cost of programs. It is based on the previously existing Loopus tool which used abstract program model of difference constraints (inequalities of the form + ), which allows for natural abstraction of common loop counter updates = + + and = + 0. Looper was initially proposed and implemented in author’s bachelor’s thesis as a checker for the Meta Infer framework but the tool failed to meet the expectations when tested on real-world code. This master’s thesis proposes a new improved version of Looper that aims at solving the main limitations of the original tool, namely through introduction of interprocedural analysis. Additionally, various extensions target- ing improved precision of the intraprocedural analysis, such as new abstraction algorithm, handling of compound loop conditions and more, were implemented. Moreover, logging, issue reporting and collection of results has been significantly improved. Finally, through extensive experiments with the new Looper version, the ability to analyze real-world code in a more general, scalable and precise way was shown.
Keywords: Amortizovaná analýza; Analýza ceny; Analýza mezí; Analýza složitosti; Degradace složitosti; Imperativní programy; Inkrementální analýza; Interprocedurální analýza; Kompoziční analýza; Looper; Loopus; Meta Infer; Modulární analýza; Rozdílová analýza; Statická analýza; Škálovatelnost; Amortized analysis; Bound analysis; Complexity analysis; Complexity degradation; Compositional analysis; Cost Analysis; Difference constraints; Differential analysis; Imperative programs; Incremental analysis; Interprocedural analysis; Looper; Loopus; Meta Infer; Modular analysis; Scalability; Static analysis

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/211956

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


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