Compiler correctness

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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[edit]

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, formal verification, and provably correct semantics-directed compiler generation.[3]


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

See also[edit]


  1. ^ 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. 
  2. ^ 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. 
  3. ^ 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
  4. ^ Compilers: Principles, Techniques and Tools, infra 1986, p. 731.
  5. ^ ibid, 2006, p. 16.
  6. ^ Christopher Fraser; David Hanson (1995). A Retargetable C compiler: Design and Implementation. Benjamin/Cummings Publishing. ISBN 0-8053-1670-1. , pp. 531–3.
  7. ^ 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.
  8. ^ 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. 
  9. ^ 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 "". Retrieved 2009-03-13.  External link in |title= (help).
  10. ^ "". Retrieved 2011-01-15.  External link in |title= (help)
  11. ^ "". Retrieved 2009-03-13.  External link in |title= (help)
  12. ^ "". Retrieved 2009-03-13.  External link in |title= (help)
  13. ^ "Source of Fortran validation suite". Retrieved 2011-09-01. 
  14. ^ "Source of Cobol validation suite". Retrieved 2011-09-01.