LLVM Project is a collection of modular and reusable compiler and toolchain technologies. It supports various high-level languages and hardware architectures. LLVM IR is an SSA-based intermediate representation whose design helps in the easy and efficient implementation of various compiler optimizations and transformations. Alive2 is a tool that checks whether the transformation of an instruction set into another instruction set is semantically correct or not. It is a verification framework for LLVM IR, which checks whether the source and target IR are equivalent or disproves by providing a counterexample. Alive2 can reason about a wide variety of intraprocedural optimization problems, including control flow, memory, vectors, and floating-point. Alive2 has detected some fundamental issues in the LLVM-IR, which lead to mis-compilation and unsound optimizations. In this project, I propose to solve some of these issues in the LLVM IR by making some changes to the LLVM compiler infrastructure code.


Krishna Kariya


  • Juneyoung Lee
  • Nuno Lopes