A Clever Way to Find Compiler Bugs
rjlipton.wordpress.com
rjlipton.wordpress.com
This is the clever idea of this paper. They assume that there are at least two compilers say {X} and {Y}. Then let {A} be the output of {X(P)} and let {B} be the output of {Y(P)}. The key insight is: If {A} is not equal to {B}, then one of the compilers is wrong.
Seriously? It's called having a reference, and comparing your fancy compiler against a reference to make sure the results match.
That's the entire insight of that article, after spending half a page discussing the order of authors in a paper.
Really weird.
Though it won't tell us who is wrong, it tells us one of the pairs is (or both).
If it's implementation-defined behavior, it won't even tell you that.
There are also false negatives: either, or both compilers are wrong, or else the test program is wrong (undefined behavior or non-portable), or some combination of these, yet by fluke the results agree.
That's no big loss; if you're fuzzing, you're generating a lot of this stuff. If this geneated program won't catch a problem, maybe another one will. Individually, the test cases are cheap.
Also if everyone implements something the same way, incorrectly according to the standard, then perhaps the standard itself is wrong. But otherwise, you just need one compiler to implement more strictly according to the standard for the bug to be suggested
Precisely.
I don't know the date, but I cited it in my 2009 dissertation: https://dwheeler.com/trusting-trust/dissertation/html/wheele...
https://web.archive.org/web/20000919193619/http://www.yendor...
https://pdfs.semanticscholar.org/fc88/1e8d0432ea8e4dd5fda497...
I built an implementation of this method around 1992-93.
Buries the lede?
Sure formal methods have a high overhead but for compilers maybe it's worth it?
Compcert is hardly an optimizing compiler compared to GCC. And bugs were found in it (just not middle end).
It's unclear to me how the defect rate really compared for equivalent performance code (which is probably -O0 or maybe -O1 gcc).
CompCert also had correctness as a headline goal in a way that other compilers have not, so because of these differences it's hard to tell how much impact formal methods were themselves have.
Though it its reason to be hopeful at least.
More important, though, is that CompCert output is not, generally, more correct than its input. So unless you are formally verifying the program source, CompCert is unlikely to make your resulting system more correct. Most of us go years without finding a bug caused by our compiler. Furthermore, unless you are formally verifying your system specification, a formally-verified program may not help much. Being definitively wrong is rarely much better than accidentally wrong.
But what do you use to verify your specification? Formal methods can verify numerous properties, but correctness is not among them. Similarly: programming language standards -- specifications -- are also not formally verified. Correctly implementing a buggy language design gets you little closer to a correct system.
Testing finds bugs in all layers, but not reliably. Bugs found in testing tend to be implementation bugs, at first, but soon testing finds mainly specification bugs.
You're making good points, but the undeniable fact that CompCert is not a panacea doesn't contradict the fact that other compilers are buggier?
It's a matter of managing expectations. How much less-buggy would systems be, if built with compilers that are less buggy? The number is probably not negative, but the space between it and zero would be hard to see.
So it is an interesting achievement, academically, but a long way from industrially useful. Another way to say it is that it is a necessary step in achieving verifiable systems, but there are many other such steps yet to be taken.
I still feel like the conclusion is wrong, so one of the axioms or deductions must be wrong, but I can't quite put my finger on it.
In any event, well met.
Or the program relies on undefined behavior.
You can still use it to test different settings on a single compiler, though. Like optimization settings or target architecture.
If your comparing between types make your casts explicit.
So first the operation is a relation expression. Both signed Char and Unsigned Char of the arithmetic type. So we will follow usual arithmetic conversions.
https://i.ibb.co/92bHJMj/1.png
So the when converting integer types the following applies. Particularly, the section I have highlighted. Both signed and unsigned char are also the same rank. So the signed char is converted to unsigned char. However, we have a problem -1 can't be represented in unsigned so we need to look a bit further.
https://i.ibb.co/jRhqd9H/2.png
If we look here we can see the 3 applies. As you can see implementation defined.
https://i.ibb.co/8XrXt34/3.png
However, if we promote to a signed int as you suggest happens; we still run into the same thing.
Your first citation is correct - we have to perform the usual arithmetic conversions.
In your second citation, though, you missed the very first paragraph in your picture:
> The integer promotions are performed on both operands, then the following rules apply:
(emphasis is mine).
Before you apply those rules you have to perform the "integer promotions"; they are defined in section 6.3.1.1 subsection 2 and they say, in part, that operands of rank smaller than int (which we have in this example) are converted to int first (which is what my original reply was pointing out).
Once both operands are converted to int, no more "usual arithmetic conversions" are needed, so the resulting operation is done on two ints, and the result has to be 0.
This is not implementation-defined.
(By the way your last citation is for extended integer types, which we are not dealing with here - we are dealing with the basic integer types here).
It is a forlorn hope: anfilt is legion.