Abstract: LLVM's backends translate its intermediate representation to assembly or object code. In effect, these compiler backends are highly optimizing compilers in their own right, and they contain bugs. As a step towards gaining confidence in the correctness of work done by LLVM backends, we have created arm-tv and riscv-tv, which formally verify translations between LLVM IR and 64-bit ARM and RISC-V code. Ours is not the first translation validation work for LLVM, but we have advanced the state of the art along multiple fronts: we enforce various ABI rules; we have extended Alive2 (which we reuse as a verification backend) to deal with unstructured mixes of pointers and integers that are typical of assembly code; we investigate the tradeoffs between hand-written AArch64 semantics and those derived mechanically from ARM's published formal semantics; and, we have discovered 46 previously unknown miscompilation bugs in LLVM backends many of which affected multiple targets and most of which are now fixed in upstream LLVM.
Bio: John Regehr has been on the computer science faculty at the University of Utah since 2003. All of his recent work is on making compilers less buggy, easier to engineer, and more highly optimizing. When not working, he tries to spend as much time as possible outdoors.