Loop Analysis for LLVM IR Translation Validation Framework
| Thesis title in Czech: | Analýza cyklů ve verifikačním frameworku pro LLVM IR |
|---|---|
| Thesis title in English: | Loop Analysis for LLVM IR Translation Validation Framework |
| Key words: | překladače|LLVM|translation validation|formální verifikace |
| English key words: | compilers|LLVM|translation validation|formal verification |
| Academic year of topic announcement: | 2022/2023 |
| Thesis type: | Bachelor's thesis |
| Thesis language: | angličtina |
| Department: | Department of Distributed and Dependable Systems (32-KDSS) |
| Supervisor: | doc. RNDr. Jan Kofroň, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 17.03.2023 |
| Date of assignment: | 24.03.2023 |
| Confirmed by Study dept. on: | 11.04.2023 |
| Date of electronic submission: | 08.05.2024 |
| Opponents: | doc. RNDr. Pavel Parízek, Ph.D. |
| Advisors: | Mgr. Martin Blicha, Ph.D. |
| Guidelines |
| 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. |
| References |
| [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 |