Optimizations have been the cause of multiple miscompilations as well. It is difficult to determine whether an optimization is correct because bugs occur in corner cases and it’s hard to test them all for each optimization. But, thanks to Alive2, we can formally check the correctness of optimizations. Many of the bugs found are related to the notion of undef and poison values in LLVM. The semantics of these values has been formalized recently, and existing optimizations are being fixed to match the semantics. For example, branching on undef is now defined as undefined behavior (UB), and several branch-related optimizations are being fixed. However, fixing some of the optimizations requires further work, mainly due to performance concerns. One representative example is loop unswitch: it is incorrect, but still unfixed because fixing it causes big regressions in some benchmarks. Our goal is to fix such miscompilations with minimal-to-no performance regression. This project will investigate what is necessary to recover slowdowns and upstream the patches to LLVM.


Hyeongyu Kim


  • Juneyoung Lee
  • Nuno Lopes