4 ms·

It's true that I like to be technically correct. I don't consider this a problem itself. In fact, it can be quite important for programmers and mathematicians t

It's true that I like to be technically correct. I don't consider this a problem itself. In fact, it can be quite important for programmers and mathematicians to be technically correct, as this bug in Cap'n Proto illustrates quite nicely. However, this is not the only reason I'm pointing out that this is not a compiler bug. The other reason is that there are certain implications: 1. The compiler developers are likely to declare that this is not their problem. 2. The problem may exist for other compilers as well: even if it complies to the standard it may do this. Even worse, it may only show up in a new version of the compiler, or in specific situations. I am not saying that this is a good situation and programmers should just be more careful. Everybody makes mistakes. The root of the problem is at the specification. Ideally, there would be no undefined behavior. From an optimizer's point of view it is very sensible to assume that the programmer will not invoke undefined behavior and use optimizations based on this principle. People surely love a compiler which produces fast code, so it may not be desirable to totally eradicate undefined behavior (and end this kind of optimizations). The most practical remedy I see is to add a debug flag which crashes or somehow indicates undefined behavior. Indeed, GCC has done this. So ultimately, we seem to agree that the compilers should change to improve this situation.

mannykannot 9y ago
Agreed - I do not think the issue is with being technically correct, but in thinking that it always settles the matter and ends the discussion. It would seem particularly unfortunate if a compiler were to do static analysis for undefined behavior, but only use it in optimization. From a cursory search, I found this blog post [1] explaining why LLVM does not warn about such things (at least in 2011, when it was written - attitudes may have changed, and the Clang project now has the UndefinedBehaviorSanitizer [2]). One of the arguments is that it is difficult to explain what the problem is, but in my view, that is an argument for making doing so a priority. [1] http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_21.html http://blog.llvm.org/2011/05/what-every-c-programmer-should-... [2] http://releases.llvm.org/3.8.0/tools/clang/docs/UndefinedBehaviorSanitizer.html http://releases.llvm.org/3.8.0/tools/clang/docs/UndefinedBeh...
- kutkloon7 9y ago
  IMHO, more work should be done on proving properties of programs. If one could make a programming language like Dafny [1] less quirky but more developer-friendly, you can have programs which are both good-performing and proven to be consistent with their specification (but again, quirks in the specification may cause troubles).
  - mannykannot 9y ago
    Thanks for bringing Dafny to my attention. I agree with your first sentence, which is why I think it is a big deal that it can be a great deal harder, in practice, to reason about the behavior of a C program, if optimized, than the same program un-optimized. For one thing, unless you successfully reason about what the optimized code does when deploying an optimized build, then you are not deploying the program that you analyzed or inspected. I think there is a sort of analogy with a large black hole here [1]: you can slip across the "event horizon" into undefined behavior without noticing, but, especially if you are using an optimizing compiler, there may be no escape. [1] Maybe not, if the black-hole firewall hypothesis is correct.
  - bluejekyll 9y ago
    I'm totally unfamiliar with Dafny, the front page didn't do much more than specicify the goals. Any chance you could briefly compare it to Rust or another systems level language trying to remove undefined behavior?
    - nickpsecurity 9y ago
      It's more like SPARK Ada. It's a limited language designed for easy analysis by an automated prover. You can do preconditions, postconditions, and invariants in it. It was used in ExpressOS for mobile and I think IronClad Apps, too.
      - bluejekyll 9y ago
        Are those pre and post conditions always executed? Or are they optional assertions that can be enabled/disabled?
GTP 9y ago
Thanks! I didn't knew about this GCC's feature.

mannykannot 9y ago

Agreed - I do not think the issue is with being technically correct, but in thinking that it always settles the matter and ends the discussion. It would seem particularly unfortunate if a compiler were to do static analysis for undefined behavior, but only use it in optimization. From a cursory search, I found this blog post [1] explaining why LLVM does not warn about such things (at least in 2011, when it was written - attitudes may have changed, and the Clang project now has the UndefinedBehaviorSanitizer [2]). One of the arguments is that it is difficult to explain what the problem is, but in my view, that is an argument for making doing so a priority. [1] http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_21.html http://blog.llvm.org/2011/05/what-every-c-programmer-should-... [2] http://releases.llvm.org/3.8.0/tools/clang/docs/UndefinedBehaviorSanitizer.html http://releases.llvm.org/3.8.0/tools/clang/docs/UndefinedBeh...

kutkloon7 9y ago
IMHO, more work should be done on proving properties of programs. If one could make a programming language like Dafny [1] less quirky but more developer-friendly, you can have programs which are both good-performing and proven to be consistent with their specification (but again, quirks in the specification may cause troubles).
- mannykannot 9y ago
  Thanks for bringing Dafny to my attention. I agree with your first sentence, which is why I think it is a big deal that it can be a great deal harder, in practice, to reason about the behavior of a C program, if optimized, than the same program un-optimized. For one thing, unless you successfully reason about what the optimized code does when deploying an optimized build, then you are not deploying the program that you analyzed or inspected. I think there is a sort of analogy with a large black hole here [1]: you can slip across the "event horizon" into undefined behavior without noticing, but, especially if you are using an optimizing compiler, there may be no escape. [1] Maybe not, if the black-hole firewall hypothesis is correct.
- bluejekyll 9y ago
  I'm totally unfamiliar with Dafny, the front page didn't do much more than specicify the goals. Any chance you could briefly compare it to Rust or another systems level language trying to remove undefined behavior?
  - nickpsecurity 9y ago
    It's more like SPARK Ada. It's a limited language designed for easy analysis by an automated prover. You can do preconditions, postconditions, and invariants in it. It was used in ExpressOS for mobile and I think IronClad Apps, too.
    - bluejekyll 9y ago
      Are those pre and post conditions always executed? Or are they optional assertions that can be enabled/disabled?

GTP 9y ago

Thanks! I didn't knew about this GCC's feature.