|
|
Applying formal methods to analysis of semantic differences between versions of software
Nečas, František ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout integraci formálních metod pro DiffKemp, nástroj pro statickou analýzu sémantických rozdílů v rozsáhlých programech napsaných v jazyce C. Cílem tohoto rozšíření je umožnit analýzu složitějších změn, které by typicky byly analyzovatelné spíše nástroji založenými na formálních metodách, a zároveň zachovat škálovatelnost nástroje DiffKemp na velké projekty. Principem navrženého řešení je při analýze v případě nalezení možné sémantické změny zakódovat problém ekvivalence příslušných instrukcí jako instanci problému SMT. Tím je možné sémantický rozdíl potvrdit, nebo vyvrátit s pomocí SMT solveru. Navržené řešení bylo implementováno v nástroji DiffKemp a experimenty provedené na sadě programů zvané EqBench ukazují, že rozšiřuje schopnosti nástroje DiffKemp, převážně v oblasti přesné analýzy úprav aritmetických výrazů.
|
|
|
Generating Code Change Patterns from C
Kučma, Tomáš ; Pavela, Jiří (referee) ; Malík, Viktor (advisor)
Zabezpečenie sémantickej stability softvérových projektov je často nákladnou úlohou. Nástroj DiffKemp automatizuje tento proces so špeciálnym dôrazom na výkon a použiteľnosť v rozsiahlych projektoch. Cenou za jeho efektívnosť je väčšia nepresnosť oproti formálnym nástrojom. Na minimalizáciu tohto problému DiffKemp umožňuje používateľom definovať vlastné vzory zachovávajúce sémantiku, opisujúce, aké zmeny majú byť považované za ekvivalentné. V súčasnosti je táto podpora obmedzená na vzory napísané v internej reprezentácii LLVM, ktorá nie je priateľská pre používateľa. Cieľom tejto práce je rozšíriť túto podporu na vzory napísané v jazyku C, čo výrazne zjednoduší proces ich vytvárania. To zahŕňa návrh reprezentácie vzorov, ktorá musí byť schopná zakódovať všetky potrebné metainformácie, a následný návrh, implementáciu a testovanie rozšírenia DiffKemp, ktoré umožní využívať vzory zapísané v jazyku C.
|
|
|
Equivalence-Based Slicing of Programs
Malecová, Tatiana ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je navrhnúť metódu, ktorá zjednoduší dva porovnávané programy na základe výsledkov ich sémantickej analýzy. Cieľom je odstránenie čo najväčšieho množstva sémanticky ekvivalentných častí porovnávaných programov. Pre nájdenie týchto ekvivalentných častí aplikujeme vlastné riešenie problému nájdenia najväčšieho spoločného indukovaného podgrafu. Následne sme schopní zjednodušiť programy využitím spätného statického prerezávania. Aplikáciou tohto zjednodušenia získame prerezané programy, ktoré obsahujú rozdielne časti a časti programov, ktoré môžu tieto rozdiely ovplyvniť. Táto metóda je naimplementovaná ako rozšírenie nástroja DiffKemp, čo je statický analyzátor sémantických rozdielov medzi rôznymi verziami rozsiahlych programov. Experimenty vykonané na jadrách Linux-u ukazujú, že metóda je schopná veľmi efektívne vyprodukovať korektné prerezané programy (analýza sa predĺžila len o 3.2%). Navyše, vzniknuté prerezané programy sú omnoho menšie, ako originálne, čo ich činí vhodnými pre ďalšiu analýzu.
|
|
|
Automatic Forward Slicing of Programs
Patrik, Nikolas ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Táto práca popisuje návrh a implementáciu nového riešenie pre nástroj DiffKemp na automatické dopredné prerezávanie programov. Po zdĺhavej analýze súčasného riešenia, sme sa rozhodli súčasné riešenie ponechať a rozšíriť ho o zopár vylepšení. Implementovali sme rozšírenie ktoré dovoľuje DiffKempu vykonávať analýzu nad prvkami štrukturovaných typov, pridali sme k súčasnému prerezávaciemu kritériu aj hodnotu premennej a na záver pridali podporu na analýzu parametrov modulov jadra. Po implementovaní týchto vylepšení sme vykonali experimenty ktoré potvrdili zlepšenie analýzi ktorú DiffKemp vykonával.
|
|
|
Applying Code Change Patterns during Analysis of Program Equivalence
Šilling, Petr ; Fiedor, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je návrh statické analýzy pro rozpoznávání vzorů, popisujících často se vyskytující změny mezi různými verzemi nízkoúrovňového kódu. V rámci práce je navržen způsob kódování vzorů, využívající vnitřní reprezentaci LLVM, a algoritmus pro hledání vzorů založený na postupném porovnávání instrukcí podle toku řízení. Navržená analýza byla implementována jako rozšíření nástroje DiffKemp pro analýzu sémantických rozdílů různých verzí rozsáhlých projektů napsaných v jazyce C. Výsledky experimentů provedených na třech dvojicích minulých verzí linuxového jádra ukazují, že navržené rozšíření dokáže eliminovat podstatné množství falešně pozitivních či obecně nežádoucích rozdílů z výsledků porovnání nástrojem DiffKemp, které by jinak vyžadovaly manuální kontrolu.
|
|
|
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.
|
|
|
Equivalence-Based Slicing of Programs
Malecová, Tatiana ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je navrhnúť metódu, ktorá zjednoduší dva porovnávané programy na základe výsledkov ich sémantickej analýzy. Cieľom je odstránenie čo najväčšieho množstva sémanticky ekvivalentných častí porovnávaných programov. Pre nájdenie týchto ekvivalentných častí aplikujeme vlastné riešenie problému nájdenia najväčšieho spoločného indukovaného podgrafu. Následne sme schopní zjednodušiť programy využitím spätného statického prerezávania. Aplikáciou tohto zjednodušenia získame prerezané programy, ktoré obsahujú rozdielne časti a časti programov, ktoré môžu tieto rozdiely ovplyvniť. Táto metóda je naimplementovaná ako rozšírenie nástroja DiffKemp, čo je statický analyzátor sémantických rozdielov medzi rôznymi verziami rozsiahlych programov. Experimenty vykonané na jadrách Linux-u ukazujú, že metóda je schopná veľmi efektívne vyprodukovať korektné prerezané programy (analýza sa predĺžila len o 3.2%). Navyše, vzniknuté prerezané programy sú omnoho menšie, ako originálne, čo ich činí vhodnými pre ďalšiu analýzu.
|
|
|
Applying Code Change Patterns during Analysis of Program Equivalence
Šilling, Petr ; Fiedor, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je návrh statické analýzy pro rozpoznávání vzorů, popisujících často se vyskytující změny mezi různými verzemi nízkoúrovňového kódu. V rámci práce je navržen způsob kódování vzorů, využívající vnitřní reprezentaci LLVM, a algoritmus pro hledání vzorů založený na postupném porovnávání instrukcí podle toku řízení. Navržená analýza byla implementována jako rozšíření nástroje DiffKemp pro analýzu sémantických rozdílů různých verzí rozsáhlých projektů napsaných v jazyce C. Výsledky experimentů provedených na třech dvojicích minulých verzí linuxového jádra ukazují, že navržené rozšíření dokáže eliminovat podstatné množství falešně pozitivních či obecně nežádoucích rozdílů z výsledků porovnání nástrojem DiffKemp, které by jinak vyžadovaly manuální kontrolu.
|
|
|
Automatic Forward Slicing of Programs
Patrik, Nikolas ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Táto práca popisuje návrh a implementáciu nového riešenie pre nástroj DiffKemp na automatické dopredné prerezávanie programov. Po zdĺhavej analýze súčasného riešenia, sme sa rozhodli súčasné riešenie ponechať a rozšíriť ho o zopár vylepšení. Implementovali sme rozšírenie ktoré dovoľuje DiffKempu vykonávať analýzu nad prvkami štrukturovaných typov, pridali sme k súčasnému prerezávaciemu kritériu aj hodnotu premennej a na záver pridali podporu na analýzu parametrov modulov jadra. Po implementovaní týchto vylepšení sme vykonali experimenty ktoré potvrdili zlepšenie analýzi ktorú DiffKemp vykonával.
|
guest ::
