|
|
Analysis and Notification of New ResultCloud Submissions
Iakymets, Bohdan ; Vojnar, Tomáš (referee) ; Šimková, Hana (advisor)
Software tests results have mostly the same values, therefore they do not contain any important or interesting information. Developers must spend a lot of time for looking for something interesting in tests results, thus developer require tool for analysis results and in case finding interesting information notify user about it. This tool can save a lot of time. Assignment of this bachelor work is design and implement mechanism for analyzing and notifing user about interesting changes in test results. Part of the work is to learn ResultCloud and based on acquired knowledge to extend ResultCloud.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (referee) ; Radu, Iosif (referee) ; Vojnar, Tomáš (advisor)
Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.
|
|
|
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.
|
|
|
Automatické generování šablon změn kódu
Kříž, Daniel ; Vašíček, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Cílem této bakalářské práce je navržení metody automatického generování šablon změn kódu v jazyce LLVM IR pro DiffKemp, nástroj pro analýzu sémantických rozdílů mezi verzemi rozsáhlých programů. Dále je cílem umožnit automatické parametrizování změn mezi verzemi projektu pomocí hodnot, globálních proměnných a strukturových typů. Toho bylo dosaženo pomocí nalezení společné šablony mezi změnami a následným generováním jejích variant, které se liší v použití globálních proměnných a typů. Navržené řešení je implementováno jako rozšíření nástroje DiffKemp a naše experimentování na malých programech ukázalo, že námi navržená metoda je schopná vytvořit alespoň částečně uspokojivé výsledky.
|
|
|
Visualisation of Static Comparison of Semantic Equivalence of Different Versions of Software Written in C
Petr, Lukáš ; Fiedor, Tomáš (referee) ; Vojnar, Tomáš (advisor)
The aim of this thesis is to create a more comprehensive presentation of results of the DiffKemp tool, which is used for static analysis of semantic differences in large projects written in C. Currently, DiffKemp displays all information about the found differences in an unstructured text which is often confusing for users. To solve this problem, a new output of the DiffKemp tool was created in this thesis, which provides the results in a serialized form using the YAML format. This output is subsequently processed and displayed using a newly created results browser, implemented as a web application using the React library, the Bootstrap framework, and the react-diff-view package. In the browser, we focus on providing an additional context in the form of source codes of the analyzed functions, and on facilitation of navigation and orientation in the found differences as well as in the provided information such as the call stacks. A comparison of the newly created browser with the original solution has shown that it is easier for the user to recognize changes in the provided call stacks and that the new browser allows him to navigate faster in the results as well as between relationships of the found differences and analysed parts.
|
|
|
A Decision Procedure for Strong-Separation Logic
Dacík, Tomáš ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Separační logika (SL) patří mezi nejúspěšnější nástroje pro verifikaci programů pracujících s dynamicky alokovanou pamětí. Její vysoká expresivita ovšem přináší nerozhodnutelnost pokud formule kombinují více jejích spojek, především separační implikace. Jako řešení byla navrhnuta takzvaná silně-separační logika (SSL), která díky striktnější definici sémantiky rozšiřuje rozhodnutelný fragment a přitom zůstává vhodná pro verifikaci programů. V současnosti ale neexistuje žádná implementace rozhodovací procedury pro tuto logiku. Tato práce se zaměřuje na návrh a implementaci rozhodovací procedury pro SSL založené na překladu vstupní formule na formuli v prvořádové logice, jejíž splnitelnost je poté možné ověřit pomocí specializovaných nástrojů. Experimentální výsledky na omezeném fragmentu, kde SL a SSL splývají, ukazují, že navržený nástroj je schopen efektivně řešit formule pocházející z verifikačních nástrojů a výrazně překonává všechny ostatní existující rozhodovací procedury, které jsou také založené na překladu. Během experimentů jsme také odhalili několik případů nekorektnosti heuristik použitých v rozhodovací proceduře pro SL implementované v nástroji cvc5. Na základě našich hlášení byly tyto heuristiky opraveny.
|
|
|
Chaos Testing of the Strimzi Project Using the Litmus Platform
Zrnčík, Henrich ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
Posledná dekáda v poli softwarového inžinierstva sa niesla v duchu automatizácie a abstrakcie. Vzostup nového spôsobu písania a menežovania softwaru (taktiež známeho ako architektúra mikroslužieb) so sebou taktiež priniesol nové výzvy v rámci zaručovania kvality softwaru. Beh systému v cloudovom prostredí s množstvom komponentov, ktoré sú roztrúsene po rôznych uzloch vyžaduje uvažovanie o závislostiach medzi týmito komponentami a dodatočné testovanie ktoré potvrdí odolnosť systému. Riešením je chaos inžinierstvo, často považované za logický krok po testovaní systému ako celku. Táto práca sa zaoberá riešením problému nedostatočných možností pre aplikáciu chaosu (a to prostredníctvom projektu Litmus) do produktu Apache Kafka, ktorý je nasadený na Kubernetes platforme ako súčasť projektu Strimzi. Inými slovami, aby sme mohli aplikovať chaos na projekte Strimzi, či iných systémoch ktoré ho používajú, musíme vytvoriť úplne nové časti Litmusu. Čo sa samotnej aplikácie chaosu týka, fakt že Strimzi je systém sám o sebe, avšak často súčasť iných systémov, znamená že budeme potrebovať vytvoriť rozšírenejšie riešenia. Práca je zavŕšená výslednými experimentami a potvrdením odolnosťi projektu v reálnom nasadení.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
V této práci se zabýváme regulárním model checkingem, což je technika pro analýzu programů, jejíchž stavový prostor může být nekonečný v důsledku práce například s neomezenými frontami, parametry, dynamicky propojenými datovými strukturami, rekurzivními procedurami nebo řetězci. Cílem této práce bylo implementovat vylepšení stávajícího prototypu nástroje ASMA implementujícího regulárním model checking nad knihovnou Automata of Microsoftu. Provedli jsme analýzu zdrojového kódu nástroje ASMA a zopakovaly analýzy všech dostupných srovnávacích programů. Identifikovali jsme některá úzká místa a několik z nich jsme vyřešili. Zejména jsme integrovali knihovnu obsahující další redukční algoritmy do nástroje ASMA, vytvořili několik nových verzí operace reverzní konkatenace, která se v benchmarcích ukázala jako velmi nákladná, vylepšili rozhraní příkazového řádku ASMA a implementovali některé další optimalizace. Výpočetní čas se při analýze větších programů snížil o 90 %.
|
|
|
Static Analysis Using Facebook Infer Focused on Errors in RCU-Based Synchronisation
Marek, Daniel ; Malík, Viktor (referee) ; Vojnar, Tomáš (advisor)
Read Copy Update (RCU) je synchronizační mechanismus, který se primárně používa v jádře Linuxu. Mezi jeho vyhledávané vlastnosti patří téměř nulová režie a vysoká rychlost při čtení sdílené paměti. RCU má soubor pravidel používaní, která je potřeba dodržovat, aby synchronizace fungovala správně. Náš výzkum ukázal, že neexistuje žádný analyzátor, který by pořádně kontroloval dodržování pravidel používaní RCU. K překonání tohoto problému jsme navrhli nový analyzátor, který se zaměřuje na porušování pravidel používaní RCU. Analyzátor je založen na statické analýze a implementován jako modul pro nástroj pro statickou analýzu Facebook/Meta Infer. Tato platforma byla vybrána, protože poskytuje škálovatelnost, která je potřebná při práci s tak rozsáhlým softwarem, jakým je Linuxové jádro. Navržený analyzátor je schopen detekovat více porušení pravidel používaní RCU, z nichž každé vede buď na race condition, nebo uváznutí. Je také schopen generovat varování pro situace, kdy je použito volání zastaralé funkce nebo když jsou detekována nekompatibilní primitiva RCU čtecího a zapisovacího procesu. Analyzátor je první svého druhu a může se stát základem pro budoucí vývoj analyzátorů v oblasti Read Copy Update. Kromě toho může být použit jako testovací nástroj v cyklu vývoje jádra Linuxu.
|
guest ::
