Are there subsets of C that avoid compiler bugs? | Hacker News Reader

Are there subsets of C that avoid compiler bugs?

blog.regehr.org

38 pointsgnosis21 comments

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

If you use the Clight subset with the CompCert C Compiler, the answer is yes:

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.

Compcert is not without bugs either. The very blog this post references talks about some.

Thanks 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

Cyclone 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/

That's not the kind of safety we're talking about.

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

Microsoft's take on making C and C++ safer - SAL: http://blogs.msdn.com/b/michael_howard/archive/2006/05/19/60...

They 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/

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

Hopefully we are self hosting at this point and smart enough to apply SAL and VCC to our compiler itself.

I wonder if there are compilers that don't compile an empty file correctly.

There are.

Assembly is the only language that will eliminate compiler bugs...

That and certified/proven compilers.

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

Can 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?

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

Historically, 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.

This was in the late 90's and it was an ADA compiler so you are probably correct there.

They'll only eliminate compiler bugs because there is no compiler. Assembler, linker, and loader bugs will still be there.

Reply on news.ycombinator.com