Comment by tialaramex | Hacker News Reader

Comment by tialaramex | Hacker News Reader

Parent Full thread

No. There's "Implementation Defined" behaviour where the compiler vendor is expected to explain what their compiler (and maybe operating system, hardware architecture, site installation) does in these cases.

But "Undefined Behaviour" says that anything might happen. The reason to be so vague is that this frees the compiler to conclude that it can ignore this scenario. Whatever it does can't be wrong for Undefined Behaviour, so, it needn't consider any cases that trigger this. This makes it actually practical to produce reasonable object code for good programs that don't actually have Undefined Behaviour.

The practical alternative is that you can just outlaw a huge amount of stuff so that there's no problem for the compiler. For example you could say OK, my language refuses to admit that pointers are just an integer which happens to correspond to a machine address. Anything that depends on that is just removed from the language entirely. But now you can't do a lot of clever tricks, so, you abandon C and move to a language where you can get your job done.

Rust's approach is to put all that stuff that - if you get it wrong - is horribly unsafe and require its "unsafe" keyword. So in one sense it's actually two very similar languages, the safe language which you would have abandoned for a lower-level language because it can't get what you need done, and the low-level language where if you screw up everything catches fire. This would not have been practical in the 1970s but it is practical today.

The semantics of undefined behaviour are exactly the same before and after any transformation of the program, because any behaviour is a semantically reasonable implementation of your program. You screwed up, not the compiler.

Two real world examples I built:

1. In Rust I have a type named OnewayLess that insists it has equivalence (implements the Eq trait) and is totally ordered (implements the Ord trait), yet, in defiance of reason, it also insists that any of its members are less than anything when asked, even themselves.

This is incoherent nonsense, but it's safe under Rust. Rust promises that even though I am clearly a lunatic who doesn't understand what equivalence and ordering mean, my programs do not have Undefined Behaviour. If I try to sort a vector of this type, that won't reformat my hard disk, or more practically change unrelated data in the program. However, it very well might take forever (the sort keeps looking for the smallest object and never finds it) or run out of memory (the sort might try to keep references to the infinitely many "lesser" items from the vector) and that isn't undefined, that's just consequences of my reprehensible type design.

2. In our RDF storage engine written in C an older version contained a mistake in which an array of temporary pointers might get partially overwritten.

In C there is no safety checking, these are raw memory addresses, and dereferencing a pointer that now might be garbage is Undefined Behaviour so all bets are off. It could do absolutely anything. If the compiler is instead required to somehow check, when referencing them, that these are still good pointers, the performance of many C programs is ruined, even though our bug was in unrelated code.

Sure, but this does not seem to provide any insight into how, in this compiler, the preservation of semantics under optimization plays out in optimizations which assume the program will never attempt to perform UB.

I feel like that's very well covered already when I wrote:

"The semantics of undefined behaviour are exactly the same before and after any transformation of the program"

[emphasis added]

I think you've got this idea that Undefined Behaviour somehow means that the behaviour is defined but is being kept secret from you. It isn't. The behaviour really is Undefined. Doing further transformations to it is therefore always harmless.

So how does a computer cause “undefined” behavior to occur? Does it invoke the “undefined” opcode? Of course not. A computer executing a program that has entered UB will do something specific but not specified in the standard.

I don’t think you are getting that Undefined is a concept in the language specification domain, that is not literally implemented. Consequently, you don’t even see yet what my question is about. When I think of a way to make it clearer, I will follow up.

UB can not be relied upon as the compiler can do arbitrary transformations to the code. Relying on it will cause security issues or head scratching bugs down the line.

Yes, yes, yes, we all know this. That is not what this thread is about. By replying to one comment in isolation, you are completely missing the context. For clarification of what it is about, read the rest of the thread.

This compiler provably follows the semantics allowed (and defined by) the C standard. Optimiaztions have nothing to do with UB. Optimizations simply aim to produce more efficient machine code that still matches the semantics as defined by the C standard. Non-optimizing compilers (or this compiler with optimizations off) can (and often do) produce exactly the same output.

The C standard Appendix J.2 contains an incomplete list of undefined behavior causes. Note that some of them simply cannot be checked at compile time, eg "The execution of a program contains a data race (5.1.2.4)" cannot have the semantics of the resulting program defined by the compiler. C does not provide the compiler with enough information to statically prevent data races. I'm not familiar with CompCert, but it should be possible to go through appendix J.2 and find the UB causes which are detectable at compile time, and then go through CompCert and see what it does for each. What it does will likely depend on the particular program it's compiling, of course.

In the post I replied to, Userbinator gave a specific example of a case where this compiler defines explicitly what does happen when a specific type of UB does occur.

In these cases, it is important to distinguish between what the standard defines, and what the implementation does. The standard says, in effect, that we cannot assume any specific outcome from UB, but in any particular case in a specific implementation, something definite (and often deterministic, though context-dependent) will happen. This, of course, is often a source of problems, when programmers know (or think they know) what will happen, and depend on it.

This entire discussion seems more than a little silly to me. At the end of the day no one cares if the compiler is correct. What they care about is that the airplane that is controlled by the code that the compiler emitted does not crash (and I'm talking here about a literal crash with bent metal and broken bodies). If the airplane does crash, no one will be satisfied by the explanation that crashing an airplane is correct behavior in the face of a program that contained an integer overflow. The C standard itself is inadequate to meet the obvious needs of mission-critical systems, and so a compiler that is proven to adhere to this standard is likewise inadequate. Something in the standard has to change even if that something is a requirement to warn the programmer that the compiler has detected UB. At least then you stand a fighting chance. Otherwise you might not discover the problem until you have a smoking hole in the ground.

Well, the question I originally posed (and which has not been addressed yet) is about one specific aspect in what formal compiler verification can do for you in a language with extensive UB.

Yes, and I'm saying: when you have as much UB as C does it makes no sense at all to prove the compiler correct because even with a proven-correct compiler you can still have catastrophic failures in the end product. You have to define at least some of the UB in an implementation-dependent way for the proof-of-correctness to have any actual value in the real world.

I don't agree.

Consider WUFFS https://github.com/google/wuffs

WUFFS will give you a C library that can turn PNG data into raw image data and is definitely correct. It's not exactly idiomatic C, you'd assume if a person wrote this code it's probably wrong, but WUFFS promises it's correct. CompCert should turn that C library into executable code which is therefore also definitely correct.

Now, maybe you will screw up code that reads the PNG data from a disk file, or draws the image on a screen, or a million other things, but the WUFFS library components are definitely fine, not just "Bill wrote it and he's got 20 years experience" fine or "It passed the unit tests" fine but "Four Color Theorem" fine.

> WUFFS promises it's correct

With respect to what standard of correctness? If the answer is that the object code is guaranteed to behave according to the source according to the C standard that is a useless guarantee because of the possibility that there is UB in the source code, in which case the compiler could release the kraken and it would still be "correct".

I should have said "safe" rather than correct here.

WUFFs promises that you can't write unsafe things. For example you can't have arithmetic overflow in WUFFS. Every time it sees arithmetic in your code the compiler is trying to decide why this operation might overflow. If you add together two 8-bit variables and put the result in a 16-bit variable, that doesn't overflow, but if you try to put the result in another 8-bit integer variable the compiler assumes unless it can see otherwise that this is an overflow, which is forbidden, so your code doesn't compile.

Buffer overflows are the same, if you're indexing into a buffer with an 8-bit unsigned variable and the buffer has 400 entries it's cool. If it has 100 entries but the compiler has concluded this variable can only be between say, 20 and 48 then that's cool too. But if the compiler can't prove this variable isn't 100 then you've got a potential buffer overflow and the code does not compile.

The C code is an output from WUFFS. WUFFS says "This C code is definitely safe" and then CompCert says "This object code is definitely a correct implementation of your C code" so the result is WUFFS compiled by CompCert is definitely safe object code.

But I can ask the exact same question: safe by what standard?

> you can't have arithmetic overflow in WUFFS

That seems improbable. Can I write x++? Because if I can, then I can have an arithmetic overflow.

> Buffer overflows are the same

That seems improbable. Can I write *p++? Because if I can then I can overflow a buffer.

Reply on news.ycombinator.com