2016 · 159 citations · 25 references
ComputingComputer EngineeringComputer ScienceCompilersFormal MethodsProgramming LanguagesCode GenerationCompiler ConstructionControl-flow AnalysisData-flow AnalysisSoftware TestingAutomated Bug FindingCode MutationDead Code AnalysisDead Code EliminationDead Code InsertionMutationMutation Testing
Validating optimizing compilers is challenging because it is hard to generate valid test programs (i.e., those that do not expose any undefined behavior). Equivalence Modulo Inputs (EMI) is an effective, promising methodology to tackle this problem. Given a test program with some inputs, EMI mutates the program to derive variants that are semantically equivalent w.r.t. these inputs. The state-of-the-art instantiations of EMI are Orion and Athena, both of which rely on deleting code from or inserting code into code regions that are not executed under the inputs. Although both have demonstrated their ability in finding many bugs in GCC and LLVM, they are still limited due to their mutation strategies that operate only on dead code regions.
25
Finding and understanding bugs in C compilers
Xuejun Yang, Yang Chen, Eric Eide et al. · 2011 · 733 citations
Formal certification of a compiler back-end or
Xavier Leroy · 2006 · 652 citations
Finding and understanding bugs in C compilers
Xuejun Yang, Yang Chen, Eric Eide et al. · ACM SIGPLAN Notices · 2011 · 586 citations
Translation validation for an optimizing compiler
George C. Necula · 2000 · 487 citations
A Formally Verified Compiler Back-end
Xavier Leroy · Journal of Automated Reasoning · 2009 · 487 citations · Full text