PTE: Axiomatic Semantics based Compiler Testing
Guoliang Dong, Jun Sun, Richard Schumi, Bo Wang, Xinyu Wang
TL;DR
PTE introduces an axiomatic-semantics-based framework for compiler testing that encodes language anecdotes as precondition–transformation–expectation triples (PTERules) written in the target language. The approach uses a lightweight, modular rule interface to test compilers incrementally without requiring full formal language semantics, enabling scalable rule creation and maintenance. Empirical evaluation on the Cangjie and Java compilers shows PTE discovers numerous bugs and design issues, with many fixes and confirmations from respective teams, and demonstrates the practicality of rule-driven metamorphic testing across evolving languages. By decoupling the oracle from the testing engine and enabling rule-driven transformations, PTE offers a practical path toward more comprehensive and sustainable compiler validation in real-world development settings.
Abstract
The correctness of a compiler affects the correctness of every program written in the language, and thus must be thoroughly evaluated. Existing automatic compiler testing methods however either rely on weak oracles (e.g., a program behaves the same if only dead code is modified), or require substantial initial effort (e.g., having a complete operational language semantics). While the former prevents a comprehensive correctness evaluation, the latter makes those methods irrelevant in practice. In this work, we propose an axiomatic semantics based approach for testing compilers, called PTE. The idea is to incrementally develop a set of ``axioms'' capturing anecdotes of the language semantics in the form of \emph{(\textbf{p}recondition, \textbf{t}ransformation, \textbf{e}xpectation) triples, which allows us to test the compiler automatically.} Such axioms are written in the same language whose compiler is under test, and can be developed either based on the language specification, or by generalizing the bug reports. PTE has been applied to a newly developed compiler (i.e., Cangjie) and a mature compiler (i.e., Java), and successfully identified 42 implementation bugs and 9 potential language design issues.