Loop Analysis for LLVM IR Translation Validation Framework
| Název práce v češtině: | Analýza cyklů ve verifikačním frameworku pro LLVM IR |
|---|---|
| Název v anglickém jazyce: | Loop Analysis for LLVM IR Translation Validation Framework |
| Akademický rok vypsání: | 2022/2023 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | doc. RNDr. Jan Kofroň, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 17.03.2023 |
| Datum zadání: | 24.03.2023 |
| Datum potvrzení stud. oddělením: | 11.04.2023 |
| Oponenti: | doc. RNDr. Pavel Parízek, Ph.D. |
| Konzultanti: | Mgr. Martin Blicha, Ph.D. |
| Zásady pro vypracování |
| Alive2 [1] is an open-source translation validation framework primarily used by LLVM [2] developers to verify the correctness of compiler optimizations. Alive2 strives to eliminate false positives, but sometimes, it fails to do so with certain types of loops [3].
The goal of this bachelor thesis is to research and possibly design and implement a method of improving the loop analysis algorithm in Alive2 to eliminate or significantly reduce the frequency of the these false alarms. Should it become apparent that there exists one best way to fix the current deficiencies (as described above), the student should attempt to implement a production-ready version of the algorithm and, as an optional goal, integrate it into Alive2. Otherwise, at least some of the considered methods should be implemented as a prototype and experimentally evaluated. A substantial effort will be required to study basic compiler concepts like control-flow graph and dominators as well as more advanced ones, like irreducible loops and static single assignment form, especially in the context of LLVM and Alive2. Furthermore, the student should grasp the necessary background in translation validation, especially the role of loop unrolling in verification of programs, which are necessary prerequisites for successful implementation of the developed algorithm. Finally, the student must be able to dive into large and complex codebases like LLVM. |
| Seznam odborné literatury |
| [1] Alive2 – https://github.com/AliveToolkit/alive2
[2] LLVM – https://llvm.org/ [3] Issues with analysis of certain types of loops – https://github.com/AliveToolkit/alive2/issues/748 |