Hacker News Reader

Comment by mannykannot | Hacker News Reader

Am I right in thinking that all undefined behavior must have a defined outcome in the implementation? Otherwise, I would guess that "proven correct" is only relevant for the compilation of programs that cannot enter UB territory.

Given Moonchild's comment about all optimizations retaining semantics, this leaves me wondering what happens with some of the more notorious UB-with-optimization footguns, such as the elimination of a chunk of code because an unsigned variable cannot go negative. If such optimizations are performed by this compiler, does the "all optimizations retain semantics" rule mean that this code elimination would be applied before any optimization (to avoid there being a difference between the before and after semantics)? I am not saying that would be wrong, but I am curious about how these cases are handled.

View on HN

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.

Dividing by zero is undefined behaviour.

It's fairly straightforward to provide a proof, given a definition of division by zero, that 1 = 0. It's often done in first-year introduction to algebra classes.

It would be correct, then for a compiler to substitute the value 1 everywhere the programmer used the value 0 (or NULL, or '\0') and still produce a valid program with the same behaviour because 1 and 0 have been proven to be equivalent.

So no, you are not right in thinking all implementations must define undefined behaviour. Undefined is undefined. C code containing undefined behaviour is not valid C code and the compiler to only required to produce correct output when the input is valid C code.

That is a fair point about divide-by-zero [1], but the very post I was replying to gave an example of where this compiler does say explicitly what happens in one case of what falls under undefined behavior in the C standards.

To clarify, what I am interested in here is the interaction of C-standard UB with any guarantee this compiler may give with regard to semantics preservation under optimization.

[1] In reality, the hardware will do something, and deterministically in every case that I am aware of, when the divide operation is invoked with zero as the divisor. Computer division is not an exact implementation of mathematical division.

> To clarify, what I am interested in here is the interaction of C-standard UB with any guarantee this compiler may give with regard to semantics preservation under optimization.

To clarify my point: undefined behaviour has any semantics you might want it to have. Anything and everything is semantically correct even under optimization. Even if the compiler says it will do one thing and then does another: it's correct either way.

The computer may "do something" with division by zero. Or the compiler might completely elide the code and replace it with a picture of a teapot before it even gets as far as hitting a register in anger. It's still valid, semantically, because you're dividing by zero from which you can prove anything and everything.

> It's fairly straightforward to provide a proof, given a definition of division by zero, that 1 = 0.

No, it is not. It's fairly straightforward to provide a proof, given the false[0] premise that x*y/y = x, that 1 = 0.

0: Hell, I don't even need division by zero for that one:

  uint8_t x = 2;
  x = x*128;
  // x is now (uint8_t)(2<<7) == (uint8_t)256 == 0
  x = x/128;
  // x is now 0>>7 == 0
  // x is now x*y/y is 2*y/y is 2
  if(x == 2) printf("it's two\n");
  printf("it's %i\n",(int)x);

Reply on news.ycombinator.com