In computing, compiler correctness is the branch of computer science that deals with trying to show that a compiler behaves according to its language specification. Techniques include developing the compiler using formal methods and using rigorous testing (often called compiler validation) on an existing compiler.
|This section needs expansion. You can help by adding to it. (March 2009)|
Compiler validation with formal methods involves a long chain of formal, deductive logic. However, since the tool to find the proof (theorem prover) is implemented in software and is complex, there is a high probability it will contain errors. One approach has been to use a tool that verifies the proof (a proof checker) which because it is much simpler than a proof-finder is less likely to contain errors.
Testing represents a significant portion of the effort in shipping a compiler, but receives comparatively little coverage in the standard literature. The 1986 edition of Aho, Sethi, & Ullman has a single-page section on compiler testing, with no named examples. The 2006 edition omits the section on testing, but does emphasize its importance: “Optimizing compilers are so difficult to get right that we dare say that no optimizing compiler is completely error-free! Thus, the most important objective in writing a compiler is that it is correct.” Fraser & Hanson 1995 has a brief section on regression testing; source code is available. Bailey & Davidson 2003 cover testing of procedure calls A number of articles confirm that many released compilers have significant code-correctness bugs. Sheridan 2007 is probably the most recent journal article on general compiler testing. Commercial compiler compliance validation suites are available from ACE, Perennial, and Plum-Hall. For most purposes, the largest body of information available on compiler testing are the Fortran and Cobol validation suites.
Further common techniques when testing compilers are fuzzing (which generates random programs to try to find bugs in a compiler) and test case reduction (which tries to minimize a found test case to make it easier to understand).
- Verification and validation (software)
- Correctness (computer science)
- CompCert C compiler—Formally verified C compiler
- Reflections on Trusting Trust
- De Millo, R. A.; Lipton, R. J.; Perlis, A. J. (1979). "Social processes and proofs of theorems and programs". Communications of the ACM. 22 (5): 271–280. doi:10.1145/359104.359106.
- Leroy, X. (2006). "Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant". ACM SIGPLAN Notices. 41: 42–54. doi:10.1145/1111320.1111042.
- Leroy, Xavier (2009-12-01). "A Formally Verified Compiler Back-end". Journal of Automated Reasoning. 43 (4): 363. ISSN 0168-7433. doi:10.1007/s10817-009-9155-4.
- "CompCert - The CompCert C compiler". compcert.inria.fr. Retrieved 2017-07-21.
- Stephan Diehl, Natural Semantics Directed Generation of Compilers and Abstract Machines,Formal Aspects of Computing, Vol. 12 (2), Springer Verlag, 2000. doi:10.1007/PL00003929
- Compilers: Principles, Techniques and Tools, infra 1986, p. 731.
- ibid, 2006, p. 16.
- Christopher Fraser; David Hanson (1995). A Retargetable C compiler: Design and Implementation. Benjamin/Cummings Publishing. ISBN 0-8053-1670-1., pp. 531–3.
- Mark W. Bailey; Jack W. Davidson (2003). "Automatic Detection and Diagnosis of Faults in Generated Code for Procedure Calls" (PDF). IEEE Transactions on Software Engineering. 29 (11): 1031–1042. doi:10.1109/tse.2003.1245304. Retrieved 2009-03-24., p. 1040.
- E.g., Christian Lindig (2005). "Random testing of C calling conventions" (PDF). Proceedings of the Sixth International Workshop on Automated Debugging. ACM. ISBN 1-59593-050-7. Retrieved 2009-03-24., and Eric Eide; John Regehr (2008). "Volatiles are miscompiled, and what to do about it" (PDF). Proceedings of the 7th ACM international conference on Embedded software. ACM. ISBN 978-1-60558-468-3. Retrieved 2009-03-24.
- Flash Sheridan (2007). "Practical Testing of a C99 Compiler Using Output Comparison" (PDF). Software: Practice and Experience. 37 (14): 1475–1488. doi:10.1002/spe.812. Retrieved 2009-03-24. Bibliography at "http://pobox.com/~flash/compiler_testing_bibliography.html". Retrieved 2009-03-13. External link in
- "http://www.ace.nl/compiler/supertest.html". Retrieved 2011-01-15. External link in
- "http://peren.com/pages/products_set.htm". Retrieved 2009-03-13. External link in
- "http://plumhall.com/suites.html". Retrieved 2009-03-13. External link in
- "Source of Fortran validation suite". Retrieved 2011-09-01.
- "Source of Cobol validation suite". Retrieved 2011-09-01.
- Chen, Yang; Groce, Alex; Zhang, Chaoqiang; Wong, Weng-Keen; Fern, Xiaoli; Eide, Eric; Regehr, John (2013). "Taming Compiler Fuzzers". Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '13. New York, NY, USA: ACM: 197–208. ISBN 9781450320146. doi:10.1145/2491956.2462173.
- Regehr, John; Chen, Yang; Cuoq, Pascal; Eide, Eric; Ellison, Chucky; Yang, Xuejun (2012). "Test-case Reduction for C Compiler Bugs". Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '12. New York, NY, USA: ACM: 335–346. ISBN 9781450312059. doi:10.1145/2254064.2254104.
|This programming-language-related article is a stub. You can help Wikipedia by expanding it.|