Skip to content

Translation Validation for the QBE Compiler Backend

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.

Return to the top of the page