Název: Advanced Static Performance Analysis Using Meta Infer
Překlad názvu: Pokročilá statická analýza výkonnosti v nástroji Meta Infer
Autoři: Pavela, Ondřej ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Typ dokumentu: Diplomové práce
Rok: 2023
Jazyk: eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [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.
Klíčová slova: 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; 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

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: http://hdl.handle.net/11012/211956

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-530221


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Diplomové práce