Compiler correctness

In computing, compiler correctness is the branch of software engineering that deals with trying to show that a compiler behaves according to its language specification^{[citation needed]}. Techniques include developing the compiler using formal methods and using rigorous testing (often called compiler validation) on an existing compiler.

Formal methods

Compiler validation with formal methods involves a long chain of formal, deductive logic.^[1] 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.

A language described as a subset of C has been formally verified (although no proof was given of its connection to the C Standard), and the proof has been machine checked.^[2]

Methods include model checking and formal verification.

Testing

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.^[3] 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.”^[4] Fraser & Hanson 1995 has a brief section on regression testing; source code is available.^[5] Bailey & Davidson 2003 cover testing of procedure calls^[6] A number of articles confirm that many released compilers have significant code-correctness bugs.^[7] Sheridan 2007 is probably the most recent journal article on general compiler testing.^[8] Commercial compiler compliance validation suites are available from ACE ^[9], Perennial^[10], and Plum-Hall,^[11]. For most purposes, the largest body of information available on compiler testing are the Fortran^[12] and Cobol^[13] validation suites.

See also

• Compiler
• Verification and Validation (software)

References

1. ^ doi:10.1145/359104.359106
2. ^ doi:10.1145/1111320.1111042
3. ^ Compilers: Principles, Techniques and Tools, infra 1986, p. 731.
4. ^ ibid, 2006, p. 16.
5. ^ Christopher Fraser; David Hanson (1995). A Retargetable C compiler: Design and Implementation. Benjamin/Cummings Publishing. ISBN 0-8053-1670-1. , pp. 531–3.
6. ^ Mark W. Bailey; Jack W. Davidson (2003). "Automatic Detection and Diagnosis of Faults in Generated Code for Procedure Calls". IEEE Transactions on Software Engineering 29 (11). http://big-oh.cs.hamilton.edu/~bailey/pubs/techreps/TR-2001-1.pdf. Retrieved 2009-03-24. , p. 1040.
7. ^ E.g., Christian Lindig (2005). "Random testing of C calling conventions". Proceedings of the Sixth International Workshop on Automated Debugging. ACM. ISBN 1-59593-050-7. http://quest-tester.googlecode.com/svn/trunk/doc/lindig-aadebug-2005.pdf. Retrieved 2009-03-24. , and Eric Eide; John Regehr (2008). "Volatiles are miscompiled, and what to do about it". Proceedings of the 7th ACM international conference on Embedded software. ACM. ISBN 978-1-60558-468-3. http://www.cs.utah.edu/~regehr/papers/emsoft08-preprint.pdf. Retrieved 2009-03-24. 
8. ^ Flash Sheridan (2007). "Practical Testing of a C99 Compiler Using Output Comparison". Software: Practice and Experience 37 (14): 1475–1488. doi:10.1002/spe.812. http://pobox.com/~flash/Practical_Testing_of_C99.pdf. Retrieved 2009-03-24.  Bibliography at "http://pobox.com/~flash/compiler_testing_bibliography.html". http://pobox.com/~flash/compiler_testing_bibliography.html. Retrieved 2009-03-13. .
9. ^ "http://www.ace.nl/compiler/supertest.html". http://www.ace.nl/compiler/supertest.html. Retrieved 2011-01-15. 
10. ^ "http://peren.com/pages/products_set.htm". http://peren.com/pages/products_set.htm. Retrieved 2009-03-13. 
11. ^ "http://plumhall.com/suites.html". http://plumhall.com/suites.html. Retrieved 2009-03-13. 
12. ^ "Source of Fortran validation suite". http://www.itl.nist.gov/div897/ctg/fortran_form.htm. Retrieved 2011-09-01. 
13. ^ "Source of Cobol validation suite". http://www.itl.nist.gov/div897/ctg/cobol_form.htm. Retrieved 2011-09-01.