3 ms·

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 whic

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.

tialaramex 5y ago
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.
- mannykannot 5y ago
  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.
  - bobthebuilders 5y ago
    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.
    - mannykannot 5y ago
      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.
SAI_Peregrinus 5y ago
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.

tialaramex 5y ago

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.

mannykannot 5y ago
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.
- bobthebuilders 5y ago
  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.
  - mannykannot 5y ago
    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.

SAI_Peregrinus 5y ago

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.