Alive2 is a practical oracle for determining whether a transformation on LLVM IR is a refinement -- that is, whether it is valid under the rules for LLVM optimizations. In this talk I'll describe an analogous translation validation solution for LLVM's AArch64 backend that we've used to find 42 miscompilation bugs, many of which were in architecture-neutral code and hence could have also affected other backends. Our tool, arm-tv, reuses Alive2 as a source of LLVM semantics and offers a choice of two AArch64 semantics, one that we wrote by hand and the other derived from ARM's machine readable specification of their ISA.
*John Regehr* is a computer science professor at the University of Utah, USA. He liked to build tools for compiler developers to use, and then write papers about them.
If you want to attend the compiler social, please remember to sign up: https://grosser.science/compiler-social-2025-06-05/
