|
|
Static Analysis Using Facebook Infer Focused on Performance Analysis
Pavela, Ondřej ; Lengál, Ondřej (referee) ; Rogalewicz, Adam (advisor)
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.
|
|
|
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.
|
|
|
Static Analysis Using Facebook Infer Focused on Performance Analysis
Pavela, Ondřej ; Lengál, Ondřej (referee) ; Rogalewicz, Adam (advisor)
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.
|
guest ::
