Team
Paul Ouellette
Mentors
Sreepathi Pai and Chen Ding
Abstract
QBE is a small optimizing compiler backend written in C. This paper applies two formal methods techniques to its verification. It leverages two existing tools — Alive2, a translation validation tool for LLVM, and the C Bounded Model Checker (CBMC). I built a translation validation tool called QBE-TV for the QBE intermediate language. QBE-TV translates QBE IL to C and then LLVM IR and uses Alive2 for translation validation. An analysis of previous QBE bugs shows that QBE-TV is able find invalid IR transformations. The paper additionally demonstrates the use of CBMC for verification of constant folding in QBE. The CBMC verification helped find two new bugs in QBE’s constant folding pass. Fixes for both bugs were contributed to QBE.