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.

翻译：编译器的正确性会影响用该语言编写的每个程序的正确性，因此必须进行彻底评估。然而，现有的自动编译器测试方法要么依赖弱预言（例如，如果仅修改死代码，程序行为保持不变），要么需要大量的初始投入（例如，拥有完整的操作语言语义）。前者无法实现全面的正确性评估，后者则使这些方法在实践中不具实用性。在这项工作中，我们提出了一种基于公理语义的编译器测试方法，称为PTE。其核心思想是逐步开发一组“公理”，以（**前**条件、**变**换、**期**望）三元组的形式捕获语言语义的片段，从而能够自动测试编译器。这些公理用待测编译器所使用的语言编写，既可根据语言规范开发，也可通过泛化错误报告构建。PTE已应用于一个新开发的编译器（即仓颉）和一个成熟的编译器（即Java），并成功识别了42个实现错误和9个潜在语言设计问题。