Compiler correctness
{{Short description|Branch of computer science}}
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|date=March 2009}} Techniques include developing the compiler using formal methods and using rigorous testing (often called compiler validation) on an existing compiler.
Formal verification
{{Expand section|date=March 2009}}
Two main formal verification approaches for establishing correctness of compilation are proving correctness of the compiler for all inputs and proving correctness of a compilation of a particular program (translation validation).
=Compiler correctness for all input programs=
Compiler validation with formal methods involves a long chain of formal, deductive logic.{{Cite journal | last1 = De Millo | first1 = R. A. | last2 = Lipton | first2 = R. J. | last3 = Perlis | first3 = A. J. | doi = 10.1145/359104.359106 | title = Social processes and proofs of theorems and programs | journal = Communications of the ACM | volume = 22 | issue = 5 | pages = 271–280 | year = 1979 | s2cid = 6794058 | doi-access = free }} 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 prominent example of this approach is CompCert, which is a formally verified optimizing compiler of a large subset of C99.{{Cite journal | last1 = Leroy | first1 = X. | doi = 10.1145/1111320.1111042 | title = Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant| journal = ACM SIGPLAN Notices | volume = 41 | pages = 42–54 | year = 2006 }}{{Cite journal|last=Leroy|first=Xavier|date=2009-12-01|title=A Formally Verified Compiler Back-end|journal=Journal of Automated Reasoning|language=en|volume=43|issue=4|pages=363–446|doi=10.1007/s10817-009-9155-4|issn=0168-7433|arxiv=0902.2137|s2cid=87730 }}{{Cite web|url=http://compcert.inria.fr/compcert-C.html|title=CompCert - The CompCert C compiler|website=compcert.inria.fr|access-date=2017-07-21}}
Another verified compiler was developed in CakeML project,{{Cite web|url=https://cakeml.org/|title=CakeML: A Verified Implementation of ML}}
which establishes correctness of a substantial subset of Standard ML programming language using the HOL (proof assistant).
Another approach to obtain a formally correct compiler is to use semantics-directed compiler generation.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}}
=Translation validation: compiler correctness on a given program=
In contrast to attempting to prove that a compiler is correct for all valid input programs translation validation
aims to automatically establish that a given input program is compiled correctly. Proving correct compilation of a given program is potentially easier than proving a compiler correct for all programs, but still requires symbolic reasoning, because a fixed program may still work on arbitrarily large inputs and run for arbitrarily long amount of time.
Translation validation can reuse an existing compiler implementation by generating, for a given compilation, a proof that the compilation was correct.
Translation validation can be used even with a compiler that sometimes generates incorrect code, as long as this incorrect does not manifest itself for a given program. Depending on the input program the translation validation can fail (because the generated code is wrong or the translation validation technique is too weak to show correctness). However, if translation validation succeeds, then the compiled program is guaranteed to be correct for all inputs.
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.Compilers: Principles, Techniques and Tools, infra 1986, p. 731. 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.”ibid, 2006, p. 16.
Fraser & Hanson 1995 has a brief section on regression testing; source code is available.{{cite book | author= Christopher Fraser | author2= David Hanson | title= A Retargetable C compiler: Design and Implementation | publisher= Benjamin/Cummings Publishing | year= 1995 | isbn= 978-0-8053-1670-4 | url-access= registration | url= https://archive.org/details/retargetableccom00fras }}, pp. 531–3.
A number of articles confirm that many released compilers have significant code-correctness bugs.E.g., {{cite conference |author= Christian Lindig |title= Random testing of C calling conventions |book-title= Proceedings of the Sixth International Workshop on Automated Debugging |publisher= ACM |isbn= 1-59593-050-7 |year= 2005 |url= http://quest-tester.googlecode.com/svn/trunk/doc/lindig-aadebug-2005.pdf |access-date= 2009-03-24 |archive-url= https://web.archive.org/web/20110711112027/http://quest-tester.googlecode.com/svn/trunk/doc/lindig-aadebug-2005.pdf |archive-date= 2011-07-11 |url-status= dead }}, and
{{cite conference |author= Eric Eide |author2= John Regehr |title= Volatiles are miscompiled, and what to do about it |book-title= Proceedings of the 7th ACM international conference on Embedded software |publisher= ACM |year= 2008 |isbn= 978-1-60558-468-3 |url= http://www.cs.utah.edu/~regehr/papers/emsoft08-preprint.pdf |access-date= 2009-03-24 }}
Sheridan 2007 is probably the most recent journal article on general compiler testing.{{cite journal | author= Flash Sheridan |year= 2007 |title= Practical Testing of a C99 Compiler Using Output Comparison |journal=Software: Practice and Experience |volume=37 |issue=14 |pages=1475–1488 |doi=10.1002/spe.812 |arxiv= 2202.07390 |s2cid= 9752084 |url=http://pobox.com/~flash/Practical_Testing_of_C99.pdf |access-date = 2009-03-24}} Bibliography at {{Cite web | url=http://pobox.com/~flash/compiler_testing_bibliography.html | title = Compiler Testing Bibliography|access-date= 2009-03-13}}. For most purposes, the largest body of information available on compiler testing are the Fortran{{Cite web | url=http://www.itl.nist.gov/div897/ctg/fortran_form.htm | title=Source of Fortran validation suite | access-date= 2011-09-01}} and Cobol{{Cite web | url=http://www.itl.nist.gov/div897/ctg/cobol_form.htm | title=Source of Cobol validation suite | access-date= 2011-09-01}} validation suites.
Further common techniques when testing compilers are fuzzing{{Cite book|last1=Chen|first1=Yang|last2=Groce|first2=Alex|last3=Zhang|first3=Chaoqiang|last4=Wong|first4=Weng-Keen|last5=Fern|first5=Xiaoli|last6=Eide|first6=Eric|last7=Regehr|first7=John|title=Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation |chapter=Taming compiler fuzzers |date=2013|series=PLDI '13|location=New York, NY, USA|publisher=ACM|pages=197–208|doi=10.1145/2491956.2462173|isbn=9781450320146|citeseerx=10.1.1.308.5541|s2cid=207205614 }} (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).{{Cite book|last1=Regehr|first1=John|last2=Chen|first2=Yang|last3=Cuoq|first3=Pascal|last4=Eide|first4=Eric|last5=Ellison|first5=Chucky|last6=Yang|first6=Xuejun|title=Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation |chapter=Test-case reduction for C compiler bugs |date=2012|series=PLDI '12|location=New York, NY, USA|publisher=ACM|pages=335–346|doi=10.1145/2254064.2254104|isbn=9781450312059|s2cid=1025409 }}
See also
- Compiler
- Verification and validation (software)
- Correctness (computer science)
- CompCert C compiler—Formally verified C compiler
- Reflections on Trusting Trust