Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

4-2021

Abstract

Compilers are error-prone due to their high complexity. They are relevant for not only general purpose programming languages, but also for many domain specific languages. Bugs in compilers can potentially render all programs at risk. It is thus crucial that compilers are systematically tested, if not verified. Recently, a number of efforts have been made to formalise and standardise programming language semantics, which can be applied to verify the correctness of the respective compilers. In this work, we present a novel specification-based testing method named SpecTest to better utilise these semantics for testing. By applying an executable semantics as test oracle, SpecTest can discover deep semantic errors in compilers. Compared to existing approaches, SpecTest is built upon a novel test coverage criterion called semantic coverage which brings together mutation testing and fuzzing to specifically target less tested language features. We apply SpecTest to systematically test two compilers, i.e., the Java compiler and the Solidity compiler. SpecTest improves the semantic coverage of both compilers considerably and reveals multiple previously unknown bugs.

Keywords

Mutation testing, Compiler testing, K framework, Formal semantics, Rare language features

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

FASE 2021: 24th International Conference on Fundamental Approaches to Software Engineering, Virtual, March 27-April 1: Proceedings

Volume

12649

First Page

269

Last Page

291

ISBN

9783030715007

Identifier

10.1007/978-3-030-71500-7_14

Publisher

Springer

City or Country

Cham

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1007/978-3-030-71500-7_14

Share

COinS