PTE: Axiomatic Semantics based Compiler Testing
CoRR(2024)
摘要
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 (precondition, transformation,
expectation) 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要