3 ms·

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

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.

lisper 5y ago
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.
- mannykannot 5y ago
  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.
  - lisper 5y ago
    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.
    - tialaramex 5y ago
      I don't agree. Consider WUFFS https://github.com/google/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.
      - lisper 5y ago
        > 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".
        tialaramex 5y ago
        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.

lisper 5y ago

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.

mannykannot 5y ago
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.
- lisper 5y ago
  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.
  - tialaramex 5y ago
    I don't agree. Consider WUFFS https://github.com/google/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.
    - lisper 5y ago
      > 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".
      - tialaramex 5y ago
        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.