5 ms·
Are there subsets of C that avoid compiler bugs?
- evangineer 15y agoIf you use the Clight subset with the CompCert C Compiler, the answer is yes: http://compcert.inria.fr/compcert-C.html#subset http://compcert.inria.fr/compcert-C.html#subset In any other case, the answer is almost certainly no. Most commonly used C compilers are sufficiently large and complicated that the chances of avoiding a compiler bug with a sufficiently large codebase is close to zero.
- mansr 15y agoCompcert is not without bugs either. The very blog this post references talks about some.
- evangineer 15y agoThanks for the heads up, I hadn't seen anything in the article about CompCert, but on doing a search I found there are quite a few mentions of it on other articles on the blog: http://blog.regehr.org/?s=compcert&searchsubmit=Search http://blog.regehr.org/?s=compcert&searchsubmit=Search
- evangineer 15y agoCyclone was an attempt at creating a safe dialect for C, it might be of some interest to people who have read the article: http://cyclone.thelanguage.org:8181/ http://cyclone.thelanguage.org:8181/
- SamReidHughes 15y agoThat's not the kind of safety we're talking about.
- evangineer 15y agoI realised that, as Pascal might put it Cyclone is a C like language designed to ensure that programs are correct. I saw it as a related form of safety others might be interested in. I already posted on Clight & CompCert which is much more salient in terms of ensuring compiler correctness and a safe subset that falls within the scope of the verified compiler's correctness.
- jimbobimbo 15y agoMicrosoft's take on making C and C++ safer - SAL: http://blogs.msdn.com/b/michael_howard/archive/2006/05/19/602077.aspx http://blogs.msdn.com/b/michael_howard/archive/2006/05/19/60...
- profquail 15y agoThey also created VCC (Verifying C Compiler), which uses their Z3 theorem prover to check for bugs (especially concurrency bugs, which can be really tough to find). http://vcc.codeplex.com/ http://vcc.codeplex.com/
- pascal_cuoq 15y agoSAL and VCC are for making C programs correct. This is related but not the same thing as making the C compiler correct. These source-level tools assume that the compiler translates the programs correctly.
- keithnoizu 15y agoHopefully we are self hosting at this point and smart enough to apply SAL and VCC to our compiler itself.
- tedunangst 15y agoSo far all the comments have focused on this issue as a C language specific problem, as if some other language won't be affected, but it's really universal to optimizers. Optimization is subtle and hard. JIT engines get burned, too.
- BruceForth 15y agoI wonder if there are compilers that don't compile an empty file correctly.
- mansr 15y agoThere are.
- chrisjsmith 15y agoAssembly is the only language that will eliminate compiler bugs...
- Peaker 15y agoThat and certified/proven compilers.
- chrisjsmith 15y agoI used to work for a large defence company. They paid for "certified" ADA compilers for PPC architecture. They had as many (if not more) bugs. Not only that, they built their stuff on FPGAs which had even buggier compilers than the compilers for the software. Certified compilers are protected only by maintenance agreements.
- Peaker 15y agoCan you explain? When a piece of software is verified with an Agda proof, that is generally a real proof. The proof may not cover all aspects, but in those aspects you really do not have bugs. Perhaps you mean non-proven certification? Or a weak certification of too few aspects?
- chrisjsmith 15y agoI think it was probably a weak certification in this case. They paid for core concerns to be covered, not necessarily the entire toolchain (which TBH is where the problems were - X working with Y properly). In fact I think it was that linker that fluffed stuff. I should modify my comment really.
- regehr 15y agoHistorically, compiler certification is a bad joke. It amounts to concerted testing at best, and wishful thinking in most cases. Few (remotely useful) compilers have been verified in any mathematical sense, and even then there is generally a wide gulf between what is proved and what we would intuitively expect a truly correct compiler to do.