[110011]

What OP is saying is if you invoke undefined behavior in your program (like the Heartbleed bug for example) it doesn't matter that in the end the compiler is correct. And this does account for the vast majority of bugs (programmer error compared to compiler error).

[catnaroek]

> if you invoke undefined behavior in your program (like the Heartbleed bug for example) it doesn't matter that in the end the compiler is correct.

This is not true. It means that you can safely omit the compiler writer from the list of people to burn at the stake.

[kazinator]

> It means that you can safely omit the compiler writer from the list of people to burn at the stake.

Not if the problem is due to a compiler change which breaks something that has worked for decades and in other compilers too.

Say we have an open source distro full of programs, and a compiler change breaks some program that hasn't been touched in years so that it misbehaves in situations where old builds of that program do not.

This means the compiler writers aren't testing with a full distro, and possibly that they don't care.

"We can do anything we want within the limits set out by the ISO language spec, and that spec alone; let the downstream consumers sort out whatever happens."

[catnaroek]

> Not if the problem is due to a compiler change which breaks something that has worked for decades and in other compilers too.

The compiler writer is within their rights to perform any changes that don't contravene the language specification, whether it breaks other people's code or not.

> "We can do anything we want within the limits set out by the ISO language spec, and that spec alone; (...)"

Yes.

> "(...) let the downstream consumers sort out whatever happens."

It's the language user's responsibility to make sure they write meaningful programs.

[dhekir]

To complement: Leroy recently worked on a research project, Verasco, to formally verify a static analyzer for C (in the likes of Astree, Frama-C, Polyspace, etc.) that could plug that hole: if the analyzer reports "no undefined behaviors", then you are sure your program compiled with CompCert will result in a bug-free program. Turns out that it is very hard to scale such analyses, but with more research they may end up working for real-world programs.

[kazinator]

> then you are sure your program compiled with CompCert will result in a bug-free program.

That is simply not true. A UB-free program which calculates e is incorrect, if the task was to calculate pi. Anything downstream from that program which uses its output as if it were pi is going to break.

Correctness is only with respect to a specification.

Specifications can have issues. Aside from being vague or contradictory, they can neglect to include important requirements, such as being completely silent on the treatment of bad inputs. A program with an exploitable security flaw outside of its intended operation can in fact be correct, because those inputs lie outside of its requirements: i.e. just like a compiler, the program has its own undefined behaviors. Also, the requirements for a program can explicitly call for undefined behavior, like "divide a number by zero to demonstrate/test the platform-specific handling of the situation".

Calling a function outside of ISO C that is not defined in the C program itself is also undefined behavior, so these proven programs cannot use any platform libraries without relaxing what "undefined behavior" means.

[angry_octet]

That is a super pedantic nit picking response. You well knew what was meant. Everyone here knows the meaning of V&V.

[kazinator]

Problem is, some undefined behaviors are actually correct. Some are documented extensions (a concept straight out of ISO C), and some are just nonportable situations that empirically work.

These could be handled in the prover; you just need an extended language definition. Or maybe not. Depending on what is being relied upon, it could be difficult.

In any case, a prover based on equating "correct" with "strictly conforming ISO C" is going to be of severely limited use. It might be good for some module-level assurance, like that some linked list or hash table module is perfect or whatever.

[Blaisorblade0]

But you are aware real-world compilers are exploiting more and more UB and keep breaking existing software? Maybe you are, but the comment does not seem to reflect that.

Either way: The good thing is, after compiler writers start exploiting a kind of UB they add options like `-fno-strict-aliasing` and pinky swear that option preserves the UB. I agree a useful checker should support real-world relevant C dialects.