Compiler correctness

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

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.[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.

The most complete example of this approach is CompCert, which is a formally verified optimizing compiler of a large a subset of C99.[2][3][4]

Methods include model checking, formal verification, and provably correct semantics-directed compiler generation.[5]


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

Further common techniques when testing compilers are fuzzing[17] (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).[18]

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